(* A demonstartion of how to express mathematical semantics in SML
   as directly as possible.

   (1) Forget about parsing, if at all possible, or delay it
	Think of this as providing "Syntactic Sugar" for the user.
   (2) Define Abstract syntax as an ML datatype
   (3) Define compositional semantics using ML functions

   Example.   The Abstract Syntax of While
	We will fake Num!
*)
datatype Aexp= Num of int 
	| Sum of Aexp * Aexp 
	| Diff of Aexp * Aexp 
	| Prod of Aexp * Aexp
	| Var of string;

datatype Bval= True | False ;

datatype Bexp= V of Bval 
	| And of Bexp * Bexp 
	| Not of Bexp
	| Eq of Aexp * Aexp 
	| Lt of Aexp * Aexp;
(* for Store = Var->Val.... see mapping.sml *)

(* fun A:Aexp*Store->Val...*)
(* fun B:Bexp*Store->bool *)
	(* Hiroki I. spotted the omission of Store from these...
	   An alternative is to hide a sto:Store in a data type...
	*)

datatype Stm= Skip 
	| Ass of string * Aexp
	| Comp of Stm * Stm
	| If of Bexp * Stm * Stm
	| While of Bexp * Stm;

(* fun S_NS: Stm * Store -> Store  OR S_SOS:Stm*Store->Store 
	because we know that S_NS and S_SOS are deterministic on While
	we know that we have semantic function which can therefore
	be programmed as an SML function.
Note.
  However, if we had non-deterministic semantics then we would have
  the problem of coding either <S,s>->s' or <S1,s1>-><S2,s2>
  and these would be code (in SML) as
   fun S_NS: Stm*Store*Store->bool OR S_SOS:Stm*Store*Stm*Store->bool
*)

Sum( Num(1), Num 2 );

While( V True, Skip);

Ass( "x", Num 1);

If( Not( Lt ( Var "x", Var "y")), Ass("z", Var "x"), Ass("z", Var "y"));

Comp(Comp( Ass ("z", Var "x"), Ass("x", Var "y")), Ass("y", Var "z"));