/* For inclusion by a Tvp program
*/

// **********************************************************************
// **********************************************************************
// FUNCTION DEFINITIONS
// **********************************************************************
// **********************************************************************

// ======================================================================
// Interprocedural & Tests & Misc
// ======================================================================

#include "functionInterprocedural.tvp"


// ======================================================================
// Assignements
// ======================================================================

// ----------------------------------------------------------------------
// Assignment of a variable
// ----------------------------------------------------------------------

//
// x := nil
//
%function AssignVarNull[xx](X)
     %t xx + " = NULL"
{
  let Y = transform(X,
		 update:{
xx(v) = 0
foreach (m in Mode){
  foreach (ff in Fields){
    r[ff,m,xx](v) = 0
#ifdef ANCESTOR
    a[ff,m,xx](v) = 0
#endif
  }
}
// Equality for everything not involving xx
foreach (m in Mode){
  foreach (g in Fields){
    foreach (p in InstrumField1){ p[g,m](v) = p[g,m](v) }
    foreach (p in InstrumField2){ p[g,m](v_1,v_2) = p[g,m](v_1,v_2) }
    foreach (zz in VarAllFPR - {xx}){
      foreach (p in InstrumFieldVar1){ p[g,m,zz](v) = p[g,m,zz](v) }
      foreach (p in InstrumFieldVar2){ p[g,m,zz](v_1,v_2) = p[g,m,zz](v_1,v_2) }
    }
  }
  foreach (p in InstrumMode1){ p[m](v) = p[m](v) }
  foreach (p in InstrumMode2){ p[m](v_1,v_2) = p[m](v_1,v_2) }
  foreach (zz in VarAllFPR - {xx}){
    foreach (p in InstrumModeVar1){ p[m,zz](v) = p[m,zz](v) }
    foreach (p in InstrumModeVar2){ p[m,zz](v_1,v_2) = p[m,zz](v_1,v_2) }
  }
}
foreach (m1 in Mode){
  foreach (m2 in Mode-{m1}){
    foreach (p in CrossInstrum1){ p[m1,m2](v) = p[m1,m2](v) }
    foreach (p in CrossInstrum2){ p[m1,m2](v_1,v_2) = p[m1,m2](v_1,v_2) }
    foreach (g in Fields){
      foreach (p in CrossInstrumField1){ p[g,m1,m2](v) = p[g,m1,m2](v) }
      foreach (p in CrossInstrumField2){ p[g,m1,m2](v_1,v_2) = p[g,m1,m2](v_1,v_2) }
    }
  }
}
})
  in begin
    coerce(Y);
    Y
  end
}

//
// y := x
//
%function AssignVarVar[yy,xx](X)
     %t yy + " = " + xx
{
  begin
    focus(X,{ xx(v) });
    let Y = transform(X,
		   update:{
yy(v) = xx(v)
foreach(m in Mode){
  foreach (f in Fields){
    foreach (p in InstrumFieldVar1){ p[f,m,yy](v) = p[f,m,xx](v) }
    foreach (p in InstrumFieldVar2){ p[f,m,yy](v_1,v_2) = p[f,m,xx](v_1,v_2) }
  }
  foreach (p in InstrumModeVar1){ p[m,yy](v) = p[m,xx](v) }
  foreach (p in InstrumModeVar2){ p[m,yy](v_1,v_2) = p[m,xx](v_1,v2) }
}
// Equality for everything not involving yy
foreach (m in Mode){
  foreach (g in Fields){
    foreach (p in InstrumField1){ p[g,m](v) = p[g,m](v) }
    foreach (p in InstrumField2){ p[g,m](v_1,v_2) = p[g,m](v_1,v_2) }
    foreach (zz in VarAllFPR - {yy}){
      foreach (p in InstrumFieldVar1){ p[g,m,zz](v) = p[g,m,zz](v) }
      foreach (p in InstrumFieldVar2){ p[g,m,zz](v_1,v_2) = p[g,m,zz](v_1,v_2) }
    }
  }
  foreach (p in InstrumMode1){ p[m](v) = p[m](v) }
  foreach (p in InstrumMode2){ p[m](v_1,v_2) = p[m](v_1,v_2) }
  foreach (zz in VarAllFPR - {yy}){
    foreach (p in InstrumModeVar1){ p[m,zz](v) = p[m,zz](v) }
    foreach (p in InstrumModeVar2){ p[m,zz](v_1,v_2) = p[m,zz](v_1,v_2) }
  }
}
foreach (m1 in Mode){
  foreach (m2 in Mode-{m1}){
    foreach (p in CrossInstrum1){ p[m1,m2](v) = p[m1,m2](v) }
    foreach (p in CrossInstrum2){ p[m1,m2](v_1,v_2) = p[m1,m2](v_1,v_2) }
    foreach (g in Fields){
      foreach (p in CrossInstrumField1){ p[g,m1,m2](v) = p[g,m1,m2](v) }
      foreach (p in CrossInstrumField2){ p[g,m1,m2](v_1,v_2) = p[g,m1,m2](v_1,v_2) }
    }
  }
}
})
    in begin
    coerce(Y);
    Y
    end
  end
}

//
// y := x->f
//
%function AssignVarNext[yy,xx,f](X)
     %t yy + " = " + xx + "->" + f
{
  begin
    focus(X, {
      xx(v),
      E(v_1) xx(v_1) & f[out](v_1,v)
    });
    let Y = transform(X,
		   update:{
yy(v) = E(v_1) xx(v_1) & f[out](v_1,v)
r[f,out,yy](v) = r[f,out,xx](v) & 
		 (!xx(v) | c[f,out](v))
r[f,inp,yy](v) = 
( (E(v_1,v_2) xx(v_1) & f[out](v_1,v_2) & id_succ[f,out,inp](v_1)) ?
  (r[f,inp,xx](v) & (!xx(v) | c[f,inp](v))) :
  (E(v_1,v_2) xx(v_1) & f[out](v_1,v_2) & Star[f,inp](v_2,v))
)
r[f,ext,yy](v) = 1/2

#ifdef ANCESTOR
a[f,out,yy](v) = a[f,out,xx](v) | yy(v) | 
		 (E(v_1,v_2) xx(v_1) & f[out](v_1,v_2) & is[f,out](v_2) & Star[f,out](v,v_2))
a[f,inp,yy](v) = ( (E(v_1,v_2) xx(v_1) & f[out](v_1,v_2) & id_succ[f,out,inp](v_1) & !is[f,inp](v_2)) ?
	(a[f,inp,xx](v) | yy(v)) :
	(E(v_1) yy(v_1) & Star[f,inp](v_1,v)) )
a[f,ext,yy](v) = 1/2
#endif

// Equality for everything not involving yy
foreach (m in Mode){
  foreach (g in Fields){
    foreach (p in InstrumField1){ p[g,m](v) = p[g,m](v) }
    foreach (p in InstrumField2){ p[g,m](v_1,v_2) = p[g,m](v_1,v_2) }
    foreach (zz in VarAllFPR - {yy}){
      foreach (p in InstrumFieldVar1){ p[g,m,zz](v) = p[g,m,zz](v) }
      foreach (p in InstrumFieldVar2){ p[g,m,zz](v_1,v_2) = p[g,m,zz](v_1,v_2) }
    }
  }
  foreach (p in InstrumMode1){ p[m](v) = p[m](v) }
  foreach (p in InstrumMode2){ p[m](v_1,v_2) = p[m](v_1,v_2) }
  foreach (zz in VarAllFPR - {yy}){
    foreach (p in InstrumModeVar1){ p[m,zz](v) = p[m,zz](v) }
    foreach (p in InstrumModeVar2){ p[m,zz](v_1,v_2) = p[m,zz](v_1,v_2) }
  }
}
foreach (m1 in Mode){
  foreach (m2 in Mode-{m1}){
    foreach (p in CrossInstrum1){ p[m1,m2](v) = p[m1,m2](v) }
    foreach (p in CrossInstrum2){ p[m1,m2](v_1,v_2) = p[m1,m2](v_1,v_2) }
    foreach (g in Fields){
      foreach (p in CrossInstrumField1){ p[g,m1,m2](v) = p[g,m1,m2](v) }
      foreach (p in CrossInstrumField2){ p[g,m1,m2](v_1,v_2) = p[g,m1,m2](v_1,v_2) }
    }
  }
}
})
    in begin
    coerce(Y);
    Y
    end
  end
}

// ----------------------------------------------------------------------
// Assignement of a field
// ----------------------------------------------------------------------

//
// x->f := nil
//
%function AssignNextNull[xx,f](X)
     %t xx + "->" + f + " = null"
{
  begin
    focus(X, {
      xx(v),
      E(v_1) xx(v_1) & f[out](v_1,v)
      ,	
      c[f,out](v)
    });
    let Y = transform(X,
                   halt: ( E(v) c[f,out](v)),
		   update:{
f[out](v_1, v_2) = f[out](v_1, v_2) & !xx(v_1)

Star[f,out](v_1,v_2) = Star[f,out](v_1,v_2) &
	( ( E(v_3,v_4) Star[f,out](v_1,v_3) & xx(v_3) & f[out](v_3,v_4) & Star[f,out](v_4,v_2) ) ? 0 : Star[f,out](v_1,v_2) )

r[f,out,xx](v) = xx(v)

foreach (zz in VarAllFPR-{xx}){
  r[f,out,zz](v) = ( (c[f,out](v) & r[f,out,xx](v)) ?
                     ( zz(v) | E(v_1) zz(v_1) & TC (v_1,v)(v_3,v_4) (f[out](v_3, v_4) & !xx(v_3))) :
                     r[f,out,zz](v) & ! (E(v_1)  xx(v_1) & r[f,out,zz](v_1) & r[f,out,xx](v) & !xx(v)))
}

#ifdef ANCESTOR
a[f,out,xx](v) = a[f,out,xx](v)
foreach (zz in VarAllFPR-{xx}){
  a[f,out,zz](v) = ( (c[f,out](v) & r[f,out,xx](v)) ?
                     ( zz(v) | E(v_1) zz(v_1) & TC (v,v_1)(v_3,v_4) (f[out](v_3, v_4) & !xx(v_3))) :
                     ( a[f,out,zz](v) & ! (E(v_1)  xx(v_1) & a[f,out,zz](v_1) & a[f,out,xx](v))) )

}
#endif

c[f,out](v) = c[f,out](v) & (!r[f,out,xx](v) | !(E(v_1) xx(v_1) & c[f,out](v_1)))
is[f,out](v) = is[f,out](v) & 
               ( !(E(v_1) xx(v_1) & f[out](v_1,v)) |
                 (E(v_1,v_2) v_1!=v_2 & f[out](v_1, v) & !xx(v_1) & f[out](v_2, v) & !xx(v_2)) )

// Input and Ext left identical
foreach (m in Mode-{out}){
  // Arity 1&2
  foreach (g in Fields){
    foreach (p in InstrumField1){ p[g,m](v) = p[g,m](v) }
    foreach (p in InstrumField2){ p[g,m](v_1,v_2) = p[g,m](v_1,v_2) }
    foreach (zz in VarAllFPR){
      foreach (p in InstrumFieldVar1){ p[g,m,zz](v) = p[g,m,zz](v) }
      foreach (p in InstrumFieldVar2){ p[g,m,zz](v_1,v_2) = p[g,m,zz](v_1,v_2) }
    }
  }
  foreach (p in InstrumMode1){ p[m](v) = p[m](v) }
  foreach (p in InstrumMode2){ p[m](v_1,v_2) = p[m](v_1,v_2) }
  foreach (zz in VarAllFPR){
    foreach (p in InstrumModeVar1){ p[m,zz](v) = p[m,zz](v) }
    foreach (p in InstrumModeVar2){ p[m,zz](v_1,v_2) = p[m,zz](v_1,v_2) }
  }
}
// Out
foreach (g in Fields - {f}){
  foreach (p in InstrumField1){ p[g,out](v) = p[g,out](v) }
  foreach (p in InstrumField2){ p[g,out](v_1,v_2) = p[g,out](v_1,v_2) }
  foreach (zz in VarAllFPR){
    foreach (p in InstrumFieldVar1){ p[g,out,zz](v) = p[g,out,zz](v) }
    foreach (p in InstrumFieldVar2){ p[g,out,zz](v_1,v_2) = p[g,out,zz](v_1,v_2) }
  }
}
// Cross Instrumentation
foreach (m1 in Mode - {out}){
  foreach (m2 in Mode-{m1,out}){
    foreach (p in CrossInstrum1){ p[m1,m2](v) = p[m1,m2](v) }
    foreach (p in CrossInstrum2){ p[m1,m2](v_1,v_2) = p[m1,m2](v_1,v_2) }
    foreach (g in Fields){
      foreach (p in CrossInstrumField1){ p[g,m1,m2](v) = p[g,m1,m2](v) }
      foreach (p in CrossInstrumField2){ p[g,m1,m2](v_1,v_2) = p[g,m1,m2](v_1,v_2) }
    }
  }
  foreach (g in Fields - {f}){
    foreach (p in CrossInstrumField1){
      p[g,m1,out](v) = p[g,m1,out](v)
      p[g,out,m1](v) = p[g,out,m1](v)
    }
    foreach (p in CrossInstrumField2){
      p[g,m1,out](v_1,v_2) = p[g,m1,out](v_1,v_2)
      p[g,out,m1](v_1,v_2) = p[g,out,m1](v_1,v_2)
    }
  }
}
})
    in begin
    coerce(Y);
    Y
    end
  end
}

//
// xy->f := x
//
%function AssignNextVar[yy,f,xx](X)
     %t yy + "->" + f + " = " + xx
{
    begin
      focus(X, {
	xx(v), yy(v)
        ,
	c[f,out](v)
 });
      let Y = transform(X,
                   halt: ( E(v) c[f,out](v)),
		   update:
	{

f[out](v_1,v_2) = f[out](v_1, v_2) | (yy(v_1) & xx(v_2))

Star[f,out](v_1,v_2) = 
	( E(v_3,v_4) yy(v_3) & xx(v_4) & Star[f,out](v_1,v_3) & Star[f,out](v_4,v_2) ?
	  1 :
	  Star[f,out](v_1,v_2) )

foreach (zz in VarAllFPR){
  r[f,out,zz](v) = r[f,out,zz](v) | E(v_1) yy(v_1) & r[f,out,zz](v_1) & r[f,out,xx](v)
}

#ifdef ANCESTOR
a[f,out,yy](v) = a[f,out,yy](v)
a[f,out,xx](v) = a[f,out,xx](v) | a[f,out,yy](v)
foreach (zz in VarAllFPR - {xx,yy}){
  a[f,out,zz](v) = a[f,out,zz](v) | E(v_1) xx(v_1) & a[f,out,zz](v_1) & a[f,out,yy](v)
}
#endif
is[f,out](v) = is[f,out](v) | (xx(v) & E(v_1) f[out](v_1,v))
c[f,out](v) = c[f,out](v) | r[f,out,xx](v) & (E(v_1) yy(v_1) & r[f,out,xx](v_1))

// Input and Ext left identical
foreach (m in Mode-{out}){
  // Arity 1&2
  foreach (g in Fields){
    foreach (p in InstrumField1){ p[g,m](v) = p[g,m](v) }
    foreach (p in InstrumField2){ p[g,m](v_1,v_2) = p[g,m](v_1,v_2) }
    foreach (zz in VarAllFPR){
      foreach (p in InstrumFieldVar1){ p[g,m,zz](v) = p[g,m,zz](v) }
      foreach (p in InstrumFieldVar2){ p[g,m,zz](v_1,v_2) = p[g,m,zz](v_1,v_2) }
    }
  }
  foreach (p in InstrumMode1){ p[m](v) = p[m](v) }
  foreach (p in InstrumMode2){ p[m](v_1,v_2) = p[m](v_1,v_2) }
  foreach (zz in VarAllFPR){
    foreach (p in InstrumModeVar1){ p[m,zz](v) = p[m,zz](v) }
    foreach (p in InstrumModeVar2){ p[m,zz](v_1,v_2) = p[m,zz](v_1,v_2) }
  }
}
foreach (g in Fields - {f}){
  foreach (p in InstrumField1){ p[g,out](v) = p[g,out](v) }
  foreach (p in InstrumField2){ p[g,out](v_1,v_2) = p[g,out](v_1,v_2) }
  foreach (zz in VarAllFPR){
    foreach (p in InstrumFieldVar1){ p[g,out,bb](v) = p[g,out,bb](v) }
    foreach (p in InstrumFieldVar2){ p[g,out,zz](v_1,v_2) = p[g,out,zz](v_1,v_2) }
  }
}
// Cross Instrumentation
foreach (m1 in Mode - {out}){
  foreach (m2 in Mode-{m1,out}){
    foreach (p in CrossInstrum1){ p[m1,m2](v) = p[m1,m2](v) }
    foreach (p in CrossInstrum2){ p[m1,m2](v_1,v_2) = p[m1,m2](v_1,v_2) }
    foreach (g in Fields){
      foreach (p in CrossInstrumField1){ p[g,m1,m2](v) = p[g,m1,m2](v) }
      foreach (p in CrossInstrumField2){ p[g,m1,m2](v_1,v_2) = p[g,m1,m2](v_1,v_2) }
    }
  }
  foreach (g in Fields - {f}){
    foreach (p in CrossInstrumField1){
      p[g,m1,out](v) = p[g,m1,out](v)
      p[g,out,m1](v) = p[g,out,m1](v)
    }
    foreach (p in CrossInstrumField2){
      p[g,m1,out](v_1,v_2) = p[g,m1,out](v_1,v_2)
      p[g,out,m1](v_1,v_2) = p[g,out,m1](v_1,v_2)
    }
  }
}
	}
      )
      in begin
	coerce(Y);
	Y
      end
    end
}

// ----------------------------------------------------------------------
// Assignement of a Boolean field
// ----------------------------------------------------------------------

%function AssignBoolFalse[xx,b](X)
     %t xx + "->" + b + " = 0"
{
  begin
    focus(X, { xx(v) });
    let Y = transform(X,
		   update:
	{
b[out](v) = b[out](v) & !xx(v)
// Equality for everything not involving b
foreach (m in Mode){
  foreach (g in Fields){
    foreach (p in InstrumField1){ p[g,m](v) = p[g,m](v) }
    foreach (p in InstrumField2){ p[g,m](v_1,v_2) = p[g,m](v_1,v_2) }
    foreach (zz in VarAllFPR){
      foreach (p in InstrumFieldVar1){ p[g,m,zz](v) = p[g,m,zz](v) }
      foreach (p in InstrumFieldVar2){ p[g,m,zz](v_1,v_2) = p[g,m,zz](v_1,v_2) }
    }
  }
  foreach (p in InstrumMode1){ p[m](v) = p[m](v) }
  foreach (p in InstrumMode2){ p[m](v_1,v_2) = p[m](v_1,v_2) }
  foreach (zz in VarAllFPR){
    foreach (p in InstrumModeVar1){ p[m,zz](v) = p[m,zz](v) }
    foreach (p in InstrumModeVar2){ p[m,zz](v_1,v_2) = p[m,zz](v_1,v_2) }
  }
}
foreach (m1 in Mode){
  foreach (m2 in Mode-{m1}){
    foreach (p in CrossInstrum1){ p[m1,m2](v) = p[m1,m2](v) }
    foreach (p in CrossInstrum2){ p[m1,m2](v_1,v_2) = p[m1,m2](v_1,v_2) }
    foreach (g in Fields){
      foreach (p in CrossInstrumField1){ p[g,m1,m2](v) = p[g,m1,m2](v) }
      foreach (p in CrossInstrumField2){ p[g,m1,m2](v_1,v_2) = p[g,m1,m2](v_1,v_2) }
    }
  }
}
})
    in begin
    coerce(Y);
    Y
    end
  end
}

%function AssignBoolTrue[xx,b](X)
     %t xx + "->" + b + " = true"
{
  begin
    focus(X, { xx(v) });
    let Y = transform(X,
		   update:
	{
b[out](v) = b[out](v) | xx(v)
// Equality for everything not involving b
foreach (m in Mode){
  foreach (g in Fields){
    foreach (p in InstrumField1){ p[g,m](v) = p[g,m](v) }
    foreach (p in InstrumField2){ p[g,m](v_1,v_2) = p[g,m](v_1,v_2) }
    foreach (zz in VarAllFPR){
      foreach (p in InstrumFieldVar1){ p[g,m,zz](v) = p[g,m,zz](v) }
      foreach (p in InstrumFieldVar2){ p[g,m,zz](v_1,v_2) = p[g,m,zz](v_1,v_2) }
    }
  }
  foreach (p in InstrumMode1){ p[m](v) = p[m](v) }
  foreach (p in InstrumMode2){ p[m](v_1,v_2) = p[m](v_1,v_2) }
  foreach (zz in VarAllFPR){
    foreach (p in InstrumModeVar1){ p[m,zz](v) = p[m,zz](v) }
    foreach (p in InstrumModeVar2){ p[m,zz](v_1,v_2) = p[m,zz](v_1,v_2) }
  }
}
foreach (m1 in Mode){
  foreach (m2 in Mode-{m1}){
    foreach (p in CrossInstrum1){ p[m1,m2](v) = p[m1,m2](v) }
    foreach (p in CrossInstrum2){ p[m1,m2](v_1,v_2) = p[m1,m2](v_1,v_2) }
    foreach (g in Fields){
      foreach (p in CrossInstrumField1){ p[g,m1,m2](v) = p[g,m1,m2](v) }
      foreach (p in CrossInstrumField2){ p[g,m1,m2](v_1,v_2) = p[g,m1,m2](v_1,v_2) }
    }
  }
}
})
    in begin
    coerce(Y);
    Y
    end
  end
}