(* 
 * Translation of Lambda-lad to Lambda-low
 * Author: Lea Wittie
 * Copyright (c) 2007 Bucknell University
 *
 * Permission is hereby granted, free of charge, to any individual or
 * institution obtaining a copy of this software and associated
 * documentation files (the "Software"), to use, copy, modify, and
 * distribute without restriction, provided that this copyright and
 * permission notice is maintained, intact, in all copies and supporting
 * documentation.
 *
 * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
 * EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
 * MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT.
 * IN NO EVENT SHALL BUCKNELL UNIVERSITY BE LIABLE FOR ANY CLAIM, DAMAGES
 * OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR
 * OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE
 * OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
 *)

(* Version 4:
 *
 * We model registers and state components as memory locations since Lambda-low
 * has only one (linear 0-word) capability, Mem.
 *
 * To allow access to individual fields of a register, we break the register
 * and the read/written value into individual bits. The register therefore 
 * has a Mem for each bit. (We don't do this for state components since their
 * bits cannot be accesssed seperately). N-bit numbers are therefore modeled
 * as bit vectors <b(n-1)..b0> of n booleans. Numbers in driver code are 
 * all unsigned so there is no sign bit.
 *
 * Vector -> field    Get <b31 .. b0> i --> if bi then 1 else 0
 * Vector -> Number   Sum <b31 .. b0> --> b0*2^0 + .. + bn*2^n + .. + b31*2^31
 *				   
 * A spec is made of read/write, port number, a set of states, 
 * preconditions, postconditions.

 * Where things are in memory:
 * The state locations in M (memory) are hardcoded to prevent someone 
 * from using random states. (That required the spec take the full set 
 * of states so multiple specs would use the same indexing).
 * The port locations in M (memory) are hardcoded to prevent someone 
 * from using a random port. We'll let the base address be 0 (the actual
 * IO address is base address + port address). We'll pretend memory is 
 * 1000 words so we'll put the state components after that. (The states
 * take up no space in reality so this makes sense).
 *

 * There was more than one way to code a spec in \-low. My choice was for 
 * simplicity. Occaisionally the functions will require a dud type value 
 * just so they can have a boolean expression.

 * If a condition occurs in both the pre and post the repeated state may 
 * have two identical ForAll statements:
 * {val<=3} write {val<=3} ---> (all val; val<= 3. (all val; val<= 3...


 * -----------------------Basic translation-------------------

 * Lambda-laddie code: Read/Write (offset N, preconditions P, postconditions Q)

 * Lambda-low code: 
 * (All P states; P. 
 * (All Q states and value; Q.
 * \stateMem --> \statePtr -->  
 * \portMem --> \portPtr --> 
 * \value iff write -->
 * \Q-relevant values (the side effect hacks) -->
 * lin<state mems or store(mem,hack), load/store(port,value)>

 * Issue: 
 * trans (Write (0, [], True, Lte (Value,Const 3))) 
 *    The postcondition should really be a precondition and 
 *    there is no reason (existential variable) to print the postcondition.
 * Reason:
 *    Fields or constants or old states in a write postcondition do not cause
 *    existentials or constraints to be formed. (States do cause it tho).
 * Thoughts:
 *    Really, these things should be in a precondition, not a postcondition.
 * Options:
 *    1) Let them stay gone
 *    2) Transfer them to the precondition where they belong old(S)-->S
 *    3) Make up a dud existential with this constraint
 *    4) Static semantic error: that should be in a precondition
 * Currently: option 1 in Laddie, option 3 here.
 *
 * I dont like option 1 because it makes constraints go poof. I don't 
 * like option 4 because it would allow silly constraints when real ones 
 * were present but not on their own. I'm not sure about option 2 because
 * the constraints would only get moved when alone..seems like a bad precedent.
 * However, it wouldn't change the intended action of the constraints to move
 * them. If value isnt used in ae and I can test that ae is empty but a isn't
 * then i'd know to use a dud. Can the compiler implement this as well? If 
 * I use option 3, I'd like to generate a warning but not an error.
 *)

exception Failure
exception Impossible

(* Lambda-Laddie syntax *)

datatype term = 
	 Const of int                      (* <f f .. t f>   (2) *)
       | Value                             (* value              *)
       | Get of int                        (* value[i]           *)
       | Var of string                     (* x         (window) *)
       | Old of string                     (* old(x)             *)
       | Add of term * term                (* term iop term      *)
       | Sub of term * term
       | Mul of term * term

datatype predicate = 
	 True                         (* b                  *)
       | Not of predicate             (* !pred              *)
       | And of predicate * predicate (* pred bop pred      *)
       | Lte of term * term           (* term cmp term      *)
		   
(* The missing bop and cmp operators can be made from the included ones *)

datatype spec = 
	 Read of int * (string list) * predicate * predicate 
       | Write of int * (string list) * predicate * predicate 

(* Lambda-low syntax *)

datatype int_exp (* I *) = 
	 IVar of string               (* a *)
       | IInt of int                  (* i *)
       | IAdd of int_exp * int_exp    (* I iop I *)
       | ISub of int_exp * int_exp
       | IMul of int_exp * int_exp
			   
datatype bool_exp (* B *) = 
	 (* B? of string    a ??? *)
	 BTrue                        (* b *)
       | BNot of bool_exp             (* !B *)
       | BAnd of bool_exp * bool_exp  (* B bop B *)
       | BLte of int_exp * int_exp    (* I cmp I *)

(* The missing bop and cmp operators can be made from the included ones *)

datatype tipe = 
	 TSing of int_exp             (* Int(I) *)
       | TFun of tipe * tipe          (* t --> t *)
       | TTuple of tipe list          (* lin<t, t, ...> *)
       (* | Ta of string           a *)
       | TAll of string * bool_exp * tipe  (* All a:int;B.t  *)
       | TSome of string * bool_exp * tipe (* Some a:int;B.t *)
       | TMem of int_exp * tipe       (* Mem(I,t)         *)
		 
(* --------------- helper functions ----------------- *)

(* Boolean test is x is a member of a set *)
infix mem;
fun (x mem []) = false
  | (x mem (y::l)) = (x=y) orelse (x mem l);

(* inserts an element into a list if it isnt a duplicate *)
fun newmem (x,xs) =  if x mem xs then xs else x::xs;

(* Turns a list into a set by eliminating duplicates *)
fun setof [] = []
  | setof (x::xs) = newmem(x,setof xs);

(* takes the union of two sets *)
fun union([],ys) = ys
  | union(x::xs,ys) = newmem(x,union(xs,ys));

(* remove element y from set xs *)
fun remove([],y) = []
  | remove(x::xs,y) = if (x=y) then xs else x :: (remove (xs,y))
; 

(* finds the items that are in the first set but not in the second *)
fun disjoint(xs,[]) = xs
  | disjoint(xs,y::ys) = disjoint (remove (xs,y), ys)
;

fun size [] = 0
  | size (x::xs) = 1 + (size xs)
;

(* Warning: index are 1..n, returns n+1 if not found *)
fun getIndex ([],y) = 1
  | getIndex (x::xs,y) = if (x=y) then 1 else 1 + getIndex (xs,y)
;

fun pow2(k:int) = if (k=0) then 1
		  else 2 * pow2(k-1)
;

(* -------------------------- Well formedness check ------------------------ *)

(* values do not occur in the before of a read.
 * old only occurs in afters
 * you cant do old(value)
 * var and old must be among the states (t)
 * get only takes integers 0..7. (0..31 for 32 bits)
 * t is the states
 * address are 0...1000
 *)
fun check_b' (t,Var s,_):bool = if (s mem t) then true else false
  | check_b' (t,Const _,_) = true
  | check_b' (t,Add (t1,t2),r) = (check_b' (t,t1,r)) andalso (check_b' (t,t2,r))
  | check_b' (t,Sub (t1,t2),r) = (check_b' (t,t1,r)) andalso (check_b' (t,t2,r))
  | check_b' (t,Mul (t1,t2),r) = (check_b' (t,t1,r)) andalso (check_b' (t,t2,r))
  | check_b' (t,Value,r) = if (r) then false else true  (* no values w/ read *)
  | check_b' (t,Old _,r) = false    (* old only occurs in afters *)
  | check_b' (t,Get i,_) = 0<=i andalso i<=7
;
fun check_b (t,Lte (t1,t2),r) = (check_b' (t,t1,r)) andalso (check_b' (t,t2,r))
  | check_b (t,And (p1,p2),r) = (check_b (t,p1,r)) andalso (check_b (t,p2,r))
  | check_b (t,Not p,r) = check_b (t,p,r)
  | check_b (t,True,_) = true
;

fun check_a' (t,Var s):bool = if (s mem t) then true else false
  | check_a' (t,Const c) = true
  | check_a' (t,Add (t1,t2)) = (check_a' (t,t1)) andalso (check_a' (t,t2))
  | check_a' (t,Sub (t1,t2)) = (check_a' (t,t1)) andalso (check_a' (t,t2))
  | check_a' (t,Mul (t1,t2)) = (check_a' (t,t1)) andalso (check_a' (t,t2))
  | check_a' (t,Value) = true
  | check_a' (t,Old s) = if (s="value") then false 
			 else if (s mem t) then true else false
  | check_a' (t,Get i) = 0<=i andalso i<=7
;
fun check_a (t,Lte (t1,t2)) = (check_a' (t,t1)) andalso (check_a' (t,t2))
  | check_a (t,And (p1,p2)) = (check_a (t,p1)) andalso (check_a (t,p2))
  | check_a (t,Not p) = check_a (t,p)
  | check_a (t,True) = true
;

fun check (Read (n,t,b,a)) = n>=0 andalso n<=1000 andalso 
			     (check_b (t,b,true)) andalso (check_a (t,a))
  | check (Write (n,t,b,a)) = n>=0 andalso n<=1000 andalso 
			     (check_b (t,b,false)) andalso (check_a (t,a))
;

(* -------------------------- Environment Formation ------------------------ *)

(* Make a list of constrained states.
 * There wont be any olds in a before constraint.
 * Olds in an after constraint are not locally constrained.
 * Includes values as value (the whole value) and IvalueN (value[N])
 * d means old: we want the "olds" environment
 * v: I do want values in be, I don't want values in ae
 *)
fun getStates' (Var s,d,v):string list = if (d) then [] else s::[]
  | getStates' (Const c,d,v) = []
  | getStates' (Add (t1,t2),d,v) = (getStates' (t1,d,v)) @ (getStates' (t2,d,v))
  | getStates' (Sub (t1,t2),d,v) = (getStates' (t1,d,v)) @ (getStates' (t2,d,v))
  | getStates' (Mul (t1,t2),d,v) = (getStates' (t1,d,v)) @ (getStates' (t2,d,v))
  | getStates' (Value,d,v) = if (d orelse not v) then [] else 
			   "value0"::"value1"::"value2"::"value3"::
			   "value4"::"value5"::"value6"::"value7"::[]
  | getStates' (Old s,d,v) = if (d) then s::[] else []
  | getStates' (Get i,d,v) = if (d orelse not v) 
			     then [] else ("value"^Int.toString(i))::[]
;
fun getStates (Lte (t1,t2),d,v) = (getStates' (t1,d,v)) @ (getStates' (t2,d,v))
  | getStates (And (p1,p2),d,v) = (getStates (p1,d,v)) @ (getStates (p2,d,v))
  | getStates (Not p,d,v) = getStates (p,d,v)
  | getStates (True,d,v) = [] 
;

(* -------------------------- Translation: Lambda-lad to Lambda-low ------- *)

(* Turn a bit vector into an integer *)
fun sum(s,n) = if (n=7) (* or 31 *) 
	       then IMul (IVar (s^Int.toString(n)), IInt (pow2 n))
	       else IAdd (IMul (IVar (s^Int.toString(n)), IInt (pow2 n)), 
			  sum(s,n+1))
;

(* The after constraints *)
fun postcondition'' (Var s,_,be): int_exp = IVar ("aPost"^s)
  | postcondition'' (Const c,_,be) = IInt c
  | postcondition'' (Add (t1,t2),r,be) = 
    IAdd (postcondition'' (t1,r,be), postcondition'' (t2,r,be))
  | postcondition'' (Sub (t1,t2),r,be) = 
    ISub (postcondition'' (t1,r,be), postcondition'' (t2,r,be))
  | postcondition'' (Mul (t1,t2),r,be) = 
    IMul (postcondition'' (t1,r,be), postcondition'' (t2,r,be))
  | postcondition'' (Value,r,be) = 
    if (r) then sum ("Ireg",0) 
    else if ("value0" mem be) (* all values will be if any are *)
         then (* a *) sum ("aPrevalue",0)
         else (* I *) sum ("Ivalue",0)
  | postcondition'' (Get i,r,be) = 
    if (r) then IVar ("Ireg"^Int.toString(i))
    else if ("value"^Int.toString(i) mem be)
         then (* a *) IVar ("aPrevalue"^Int.toString(i))
         else (* I *) IVar ("Ivalue"^Int.toString(i))
  | postcondition'' (Old s,_,be) = 
    if (s mem be) then IVar ("aPre"^s) else IVar ("I"^s)
;
fun postcondition' (Lte (t1,t2),r,be): bool_exp = 
    BLte (postcondition'' (t1,r,be), postcondition'' (t2,r,be))
  | postcondition' (And (p1,p2),r,be) = 
    BAnd (postcondition' (p1,r,be), postcondition' (p2,r,be))
  | postcondition' (Not p,r,be) = BNot (postcondition' (p,r,be))
  | postcondition' (True,_,be) = BTrue
;
fun postcondition (rw,a,be): bool_exp = if (rw = "read") 
				 then postcondition' (a,true,be)
				 else postcondition' (a,false,be)
;

fun isNotValue (x:string, p:int) : bool = if (p=0-1) then true
  else if (x="value"^Int.toString(p)) then false else isNotValue(x, p-1)
;

(* The precondition *)
fun precondition' (Var s):int_exp = IVar ("aPre"^s)
  | precondition' (Const c) = IInt c
  | precondition' (Add (t1,t2)) = 
    IAdd (precondition' (t1), precondition' (t2))
  | precondition' (Sub (t1,t2)) = 
    ISub (precondition' (t1), precondition' (t2))
  | precondition' (Mul (t1,t2)) = 
    IMul (precondition' (t1), precondition' (t2))
  | precondition' (Value) = sum("aPrevalue",0)
  | precondition' (Get i) = IVar ("aPrevalue"^Int.toString(i)) 
  (* we knows it's value .. minor change to allow more *)
  | precondition' (Old _) = raise Impossible
;
fun precondition (Lte (t1,t2)): bool_exp = 
    BLte (precondition' (t1), precondition' (t2))
  | precondition (And (p1,p2)) = BAnd (precondition (p1), precondition (p2))
  | precondition (Not p) = BNot (precondition (p))
  | precondition (True) = BTrue
;

(* Output value (on read)
 * Case: p < 0
 *  => moving on
 * Case: p >= 0
 *  valuep in precondition => TFun Int(avaluep) more value
 *  else                   => TFun Int(Ivaluep) more value
 *)
fun outputValue' (rw,n,t,b,a,be,ae,oe,p) =
   if (p=0-1) 
   then nextOutput(rw,n,t,b,a,be,ae,oe,"outputValue")
  
   else (* if ("value"^Int.toString(p) mem ae)
   then TSing (IVar ("aPostvalue"^Int.toString(p))) ::
	outputValue' (rw,n,t,b,a,be,ae,oe,p-1)
   else *) TSing (IVar ("Ireg"^Int.toString(p))) ::
	outputValue' (rw,n,t,b,a,be,ae,oe,p-1)

(* working environment = highest bit number (32-bit => 31) *)
and outputValue (rw:string, n:int, t:string list, b:predicate, a:predicate,
		be:string list, ae:string list, oe:string list) : tipe list =
    if (rw="read")
    then outputValue' (rw,n,t,b,a,be,ae,oe,7)
    else nextOutput(rw,n,t,b,a,be,ae,oe,"outputValue")

(* Output register capability
 * Case: p < 0 => moving on
 * Case p >= 0
 *   read => TMem (TVar n+p, TSing TVar Iregp) :: more register
 *   write => valuep in pre => aPrevaleup
 *            else          => Ivaluep
*)
and outputRegister'(rw,n,t,b,a,be,ae,oe,p) =
    if (p=0-1)
    then nextOutput(rw,n,t,b,a,be,ae,oe,"outputRegister")

    else if (rw="read")
    then TMem (IInt (n+p), TSing (IVar ("Ireg"^Int.toString(p)))) ::
	 outputRegister' (rw,n,t,b,a,be,ae,oe,p-1)
    else if ("value"^Int.toString(p) mem be)
	 then TMem (IInt (n+p), TSing (IVar ("aPrevalue"^Int.toString(p)))) ::
	      outputRegister' (rw,n,t,b,a,be,ae,oe,p-1)
         else TMem (IInt (n+p), TSing (IVar ("Ivalue"^Int.toString(p)))) ::
	      outputRegister' (rw,n,t,b,a,be,ae,oe,p-1)

(* working environment = highest bit number (32-bit => 31) *)
and outputRegister (rw:string, n:int, t:string list, b:predicate, a:predicate,
		    be:string list, ae:string list, oe:string list) 
    : tipe list = outputRegister' (rw,n,t,b,a,be,ae,oe,7)

(* Output state capabilities
 * Case: empty env => moving on
 * Case: in post => aPostx
 *       in pre => aPrex
 *       else   => Ix 
 *)
and outputStates' (rw,n,t,b,a,be,ae,oe,[]) =
    nextOutput (rw,n,t,b,a,be,ae,oe,"outputStates")
  | outputStates' (rw,n,t,b,a,be,ae,oe,x::xs) =
    if (x mem ae)
    then TMem (IInt (1000+getIndex(t,x)), TSing (IVar ("aPost"^x))) ::
	 outputStates' (rw,n,t,b,a,be,ae,oe,xs)
    else if (x mem be)
    then TMem (IInt (1000+getIndex(t,x)), TSing (IVar ("aPre"^x))) ::
	 outputStates' (rw,n,t,b,a,be,ae,oe,xs)
    else TMem (IInt (1000+getIndex(t,x)), TSing (IVar ("I"^x))) ::
	 outputStates' (rw,n,t,b,a,be,ae,oe,xs)

(* working environment = states *)
and outputStates(rw:string, n:int, t:string list, b:predicate, a:predicate,
		    be:string list, ae:string list, oe:string list) 
    : tipe list = outputStates' (rw,n,t,b,a,be,ae,oe,t)
    
(* Postcondition
 * Case: empty postcondition environment
 *    moving on
 * Case: one thing in postcondition environment
 *    Some axPost * postcondition * moving on    
 * Case: more things in postcondition environment
 *    Some axPost * true * more universal 
 * Dont include values on write
 *)
and existential' (rw,n,t,b,a,be,ae,oe,[]) = 
    next(rw,n,t,b,a,be,ae,oe,"existential")
  | existential' (rw,n,t,b,a,be,ae,oe,[x]) =
    TSome("aPost"^x, postcondition (rw,a,be), 
	       next(rw,n,t,b,a,be,ae,oe,"existential"))
  | existential' (rw,n,t,b,a,be,ae,oe,x::xs) = 
    TSome ("aPost"^x, BTrue, existential' (rw,n,t,b,a,be,ae,oe,xs))

(* working environment = postcondition ae (no olds, no values)
 * If the ae is empty but the postcondition isn't, then we need a dud *)
and existential (rw,n,t,b,True,be,[],oe) = 
    existential' (rw,n,t,b,True,be,[],oe,[])
  | existential (rw,n,t,b,a,be,[],oe) = 
    existential' (rw,n,t,b,a,be,[],oe,["dud"])
  | existential (rw,n,t,b,a,be,ae,oe) = existential' (rw,n,t,b,a,be,ae,oe,ae)

(* Input value (on write)
 * Case: p < 0
 *  => moving on
 * Case: p >= 0
 *  valuep in precondition => TFun Int(avaluep) more value
 *  else                   => TFun Int(Ivaluep) more value
 *)
and inputValue' (rw,n,t,b,a,be,ae,oe,p) = 
    if (p=0-1) then next(rw,n,t,b,a,be,ae,oe, "inputValue")

    else if (("value"^Int.toString(p)) mem be)
    then TFun (TSing (IVar ("aPrevalue"^Int.toString(p))), 
	       inputValue' (rw,n,t,b,a,be,ae,oe,p-1))
    else TFun (TSing (IVar ("Ivalue"^Int.toString(p))), 
	       inputValue' (rw,n,t,b,a,be,ae,oe,p-1))

(* working environment = highest bit number (32-bit => 31) *)
and inputValue (rw:string, n:int, t:string list, b:predicate, a:predicate,
		be:string list, ae:string list, oe:string list): tipe = 
    if (rw="read")
    then next (rw,n,t,b,a,be,ae,oe, "inputValue")
    else inputValue' (rw,n,t,b,a,be,ae,oe,7)

(* Input register memory capability
 * Case: p < 0
 *  => moving on
 * Case: p >= 0
 *  => TFun TMem(n+p,Iregp) more register
 * bit p of port n is loc n+p
 *)
and inputRegister' (rw,n,t,b,a,be,ae,oe,p) =
    if (p=0-1) then next (rw,n,t,b,a,be,ae,oe,"inputRegister")

    else TFun (TMem (IInt (n+p), TSing (IVar ("Ireg"^Int.toString(p)))), 
          inputRegister' (rw,n,t,b,a,be,ae,oe,p-1))

(* working environment = highest bit number (32-bit => 31) *)
and inputRegister (rw:string, n:int, t:string list, b:predicate, a:predicate,
		   be:string list, ae:string list, oe:string list): tipe =
    inputRegister' (rw,n,t,b,a,be,ae,oe,7)

(* Input state capabilities
 * Case: empty enviroment
 *   => moving on
 * Case: one or more states
 *   x in precondition => TFun TMem(axPre) more states
 *   else              => TFun TMem(Ix) more states
*)
and inputStates' (rw,n,t,b,a,be,ae,oe,[]) = 
    next (rw,n,t,b,a,be,ae,oe, "inputStates")
  | inputStates' (rw,n,t,b,a,be,ae,oe,x::xs)   =
    if (x mem be)
    then TFun (TMem (IInt (1000+getIndex(t,x)), TSing (IVar ("aPre"^x))),
               inputStates' (rw,n,t,b,a,be,ae,oe,xs))
    else TFun (TMem (IInt (1000+getIndex(t,x)), TSing (IVar ("I"^x))),
               inputStates' (rw,n,t,b,a,be,ae,oe,xs))

(* working environment = all states *)
and inputStates (rw:string, n:int, t:string list, b:predicate, a:predicate,
		 be:string list, ae:string list, oe:string list) = 
    inputStates'(rw,n,t,b,a,be,ae,oe, t)

(* The All for each used state (no value) 
 * Case: empty precondition environment
 *    moving on
 * Case: one thing in precondition environment
 *    All axPre * precondition * moving on    
 * Case: more things in precondition environment
 *    All axPre * true * more universal 
*)
and universal' (rw,n,t,b,a,be,ae,oe,[]) = next(rw,n,t,b,a,be,ae,oe,"universal")
  | universal' (rw,n,t,b,a,be,ae,oe,[x]) = 
    TAll ("aPre"^x, precondition b, next(rw,n,t,b,a,be,ae,oe,"universal"))
  | universal' (rw,n,t,b,a,be,ae,oe,x::xs) = 
    TAll ("aPre"^x, BTrue, universal' (rw,n,t,b,a,be,ae,oe,xs))

(* working environment is be *)
and universal (rw,n,t,b,a,be,ae,oe) = universal' (rw,n,t,b,a,be,ae,oe,be)

and nextOutput (rw,n,t,b,a,be,ae,oe,"start") : tipe list = 
    outputStates (rw,n,t,b,a,be,ae,oe)
  | nextOutput (rw,n,t,b,a,be,ae,oe,"outputStates") = 
    outputRegister (rw,n,t,b,a,be,ae,oe)
  | nextOutput (rw,n,t,b,a,be,ae,oe,"outputRegister") = 
    outputValue (rw,n,t,b,a,be,ae,oe)
  | nextOutput (rw,n,t,b,a,be,ae,oe,"outputValue") = []
  | nextOutput (rw,n,t,b,a,be,ae,oe,_) = raise Impossible

and next (rw,n,t,b,a,be,ae,oe,"start") : tipe = 
    universal (rw,n,t,b,a,be,ae,oe)
  | next (rw,n,t,b,a,be,ae,oe,"inputStates") = 
    inputRegister (rw,n,t,b,a,be,ae,oe)
  | next (rw,n,t,b,a,be,ae,oe,"inputRegister") = 
    inputValue (rw,n,t,b,a,be,ae,oe)
  | next (rw,n,t,b,a,be,ae,oe,"inputValue") = 
    existential (rw,n,t,b,a,be,ae,oe)
  | next (rw,n,t,b,a,be,ae,oe,"universal") = 
    inputStates (rw,n,t,b,a,be,ae,oe)
  | next (rw,n,t,b,a,be,ae,oe,"existential") = 
    TTuple (nextOutput (rw,n,t,b,a,be,ae,oe, "start"))
  | next (rw,n,t,b,a,be,ae,oe,_) = raise Impossible
;

(* Output format:
 *   (All precondition . 
 *   (\ inputStates -> 
 *   (\ inputPort -> 
 *   (\ inputValue (write only) ->
 *   (Some postcondition .
 *   lin<outputStates, outputPort, outputValue (read only)>)))))
 *)

(* Parameters:
 *   rw=read/write, n=Iaddr, t=states, b=pre, a=post
 *   be=pre env (states in pre), ae=post env (states in post)
 *   oe=old env (old states in post) 
 *)

(* --------------- makeString: for printing output ---------------------- *)

fun makeString_list ([]: tipe list):string = ""
  | makeString_list (x::xs) = ", "^(makeString x)^(makeString_list xs)

and makeString_ie (IVar s:int_exp):string = s
  | makeString_ie (IInt i) = Int.toString(i)
  | makeString_ie (IAdd (ie1,ie2)) =
    "("^(makeString_ie ie1)^" + "^(makeString_ie ie2)^")"
  | makeString_ie (ISub (ie1,ie2)) =
    "("^(makeString_ie ie1)^" - "^(makeString_ie ie2)^")"
  | makeString_ie (IMul (ie1,ie2)) =
    "("^(makeString_ie ie1)^" * "^(makeString_ie ie2)^")"

and makeString_be (BNot be:bool_exp):string = "! "^(makeString_be be)
  | makeString_be (BAnd (be1,be2)) =
    "("^(makeString_be be1)^" && "^(makeString_be be2)^")"
  | makeString_be (BLte (ie1,ie2)) =
    "("^(makeString_ie ie1)^" <= "^(makeString_ie ie2)^")"
  | makeString_be (BTrue) = "true"

and makeString (TSing ie:tipe):string = "Int("^(makeString_ie ie)^")"
  | makeString (TFun (t1,t2)) = 
    "("^(makeString t1)^" -->\n"^(makeString t2)^")"
  | makeString (TTuple []) = raise Impossible
  | makeString (TTuple (x::xs)) = 
    "lin<"^(makeString x)^(makeString_list xs)^">"
  | makeString (TAll (a,b,t)) = 
    "(All "^a^":int; "^(makeString_be b)^".\n"^(makeString t)^")"
  | makeString (TSome (a,b,t)) = 
    "(Some "^a^":int; "^(makeString_be b)^".\n"^(makeString t)^")"
  | makeString (TMem (ie,t)) = 
    "Mem("^(makeString_ie ie)^", "^(makeString t)^")"

;

(* --------------- main --------------------------------------------------- *)

(* Semantic checking, then translation *)

fun trans' (rw,n,t,b,a):tipe = 
    next (rw,n,t,b,a,
	  setof(getStates (b,false,true)), (* yes val*) 
	  setof(getStates (a,false,false)), (* no old,val *)
	  setof(getStates (a,true,false)), (* yes old *)
	  "start") 
;
fun trans (Read (n,t,b,a)):tipe = if check (Read (n,t,b,a))
				 then trans' ("read",n,t,b,a) else raise Failure
  | trans (Write (n,t,b,a)) = if check (Write (n,t,b,a))
			      then trans' ("write",n,t,b,a) else raise Failure
;

(* -------------------- sample Lambda-lad specifications ------------------------ 
 * Those marked "Failed Semantic Check" were testing the well-formedness checking.
 *)
fun runme () =
    let
	(* Basics: no constraints *)
	val test1a = trans (Read (0, [], True, True))
	val test1b = trans (Write (0, [], True, True))
	(* val test1c = trans (Write (0, [], Lte (Var "win", Const 3), True)) Failed Semantic Check *)

	(* Input state constraint *)
	val test2a = trans (Read (0, ["win"], Lte (Var "win", Const 3), True))
	val test2b = trans (Write (0, ["win"], Lte (Var "win", Const 3), True))

	(* Output state constraint *)
	val test3a = trans (Read (0, ["win"], True, Lte (Var "win", Const 3)))
	val test3b = trans (Write (0, ["win"], True, Lte (Var "win", Const 3)))

	(* I and O constraints *)
	val test3c = trans (Read (0, "win"::["blah","foo"], 
				  Lte (Var "foo", Const 5), Lte (Var "win", Const 3)))
	val test3d = trans (Write (0, "win"::["foo"], 
				   Lte (Var "foo", Const 5), Lte (Var "win", Const 3)))

	(* Value constrained *)
	(* val test4a = trans (Read (0, [], Lte (Value,Const 3), True)) Failed Semantic Check *)
	val test4b = trans (Read (0, [], True, Lte (Value,Const 3))) 
	val test4c = trans (Write (0, [], Lte (Value,Const 3), True))
	val test4e = trans (Read (0, ["win"], True, Lte (Value,Var "win")))
	val test4f = trans (Write (0, ["win"], Lte (Value,Var "win"), True))
	val test4g = trans (Write (0, ["win"], True, Lte (Value,Var "win")))

	(* Testing: Var, Const, Add, Value, Old, Lte, And, Not, True *)

	(* Var: see tests 2 and 3 *)

	(* Const: see tests 2 and 3 *)

	(* Add *)
	val test5a = trans(Read (0, "win"::["foo"], 
				 Lte (Add (Var "win",Const 5), Var "foo"), True))
	val test5b = trans(Read (0, "win"::["foo"], True, 
				 Lte (Add (Var "win",Const 5), Var "foo")))

	(* Subtract *)
	val test5c = trans(Read (0, "win"::["foo"], 
				 Lte (Sub (Var "win",Const 5), Var "foo"), True))
	val test5d = trans(Read (0, "win"::["foo"], 
				 True, Lte (Sub (Var "win",Const 5), Var "foo")))

	(* Value: see test 4 *)

	(* Old *)
	(* val test5e = trans(Read (0, ["win"], Lte (Old "win", Const 3), True)) Failed Semantic Check *)
	val test5f = trans(Read (0, ["win","foo"], True, Lte (Old "win", Var "foo")))
	(* val test5g = trans(Read (0, [], True, Lte (Old Value, Const 3)))   Failed Syntax Check *)
	(* val test5h = trans(Write (0, [], True, Lte (Old Value, Const 3)))  Failed Syntax Check *)
	(* val test5i = trans(Write (0, [], Lte (Old Value, Const 3), True))  Failed Syntax Check *)

	(* Lte: see tests 2 and 3 *)

	(* And Not OR *)
	val test5j = trans(Read (0, "win"::["foo"], 
				 And (Lte (Var "win", Const 3), Lte (Var "foo", Const 5)), True))
	val test5k = trans(Read (0, "win"::["foo"], True, 
				 And (Lte (Var "win", Const 3), Lte (Var "foo", Const 5))))
	val test5l = trans(Read (0, ["win"], Not (Lte (Var "win", Const 3)), True))
	val test5m = trans(Read (0, ["win"], True, Not (Lte (Var "win", Const 3))))
	val test5n = trans(Read (0, "win"::["foo"], 
				 Not (And (Not (Lte (Var "win", Const 3)), Not (Lte (Var "foo", Const 5)))), True)) 

	(* True: see test 1 *)

	(* Mul *)
	val test5o = trans(Read (0, "win"::["foo"], 
				 Lte (Mul (Var "win",Const 5), Var "foo"), True))
	val test5p = trans(Read (0, "win"::["foo"], True, 
				 Lte (Mul (Var "win",Const 5), Var "foo")))
	val test5q = trans(Read (0, "win"::["foo"], True, 
				 Lte (Mul (Var "win",Var "foo"), Var "foo")))
(* Note: The Clay compiler requires on oerand of the mult to be a constant *)
	(* Sub *)
	val test5r = trans(Read (0, "win"::["foo"], 
				 Lte (Sub (Var "win",Var "foo"), Var "foo"), True))
	val test5s = trans(Read (0, "win"::["foo"], True, 
				 Lte (Sub (Var "win",Var "foo"), Var "foo")))

	(* wierd cases *)
	val test6a = trans(Write (0, [], Lte (Value ,Const 5), Lte (Value,Const 5)))
	val test6b = trans(Read (0, ["win"], Lte (Var "win" ,Const 5), Lte (Var "win",Const 5)))

	(* more states than used *)
	val test6c = trans (Read (0, ["foo","win"], Lte (Var "win", Const 3), True))
	val test6d = trans (Write (0, ["foo","win"], Lte (Var "win", Const 3), True))
	val test6e = trans (Read (0, ["foo","win"], True, Lte (Var "win", Const 3)))
	val test6f = trans (Write (0, ["foo","win"], True, Lte (Var "win", Const 3)))

	(* Get *)
	val test7a = trans (Write (0, ["foo","win"], Lte (Get 2, Const 5), True))
	(* val test7b = trans (Write (0, ["foo","win"], Lte (Get 50, Const 5), True)) Failed Semantic Check *)
	
	val test7d = trans (Write (0, ["foo","win"], True, Lte (Get 2, Const 5)))
	val test7e = trans (Read (0, ["foo","win"], True, Lte (Get 2, Const 5)))

    in
	
	(* To print the results of a specific case, use the name of the case here *)
	print ((makeString test2b)^"\n")
    end
    handle Failure => print "Failed Semantic Check\n"
	 | Impossible => print "This should not have happened\n"
;

runme ()