(* Denotational semantics of IMP *)

(* Abstract syntax *)

type 
  Loc = string  ;

datatype 
  Aexp = num of int 
       | loc of Loc 
       | plus of Aexp * Aexp 
       | minus of Aexp * Aexp 
       | mult of Aexp * Aexp  ;

datatype 
  Bexp = tt 
       | ff 
       | neg of Bexp 
       | conj of Bexp * Bexp 
       | disj of Bexp * Bexp 
       | eq of Aexp * Aexp 
       | gt of Aexp * Aexp  ;

datatype
  Comm = skip 
       | assign of Loc * Aexp 
       | cond of Bexp * Comm * Comm 
       | seq of Comm * Comm
       | whi of Bexp * Comm  ;

(* Semantic functions for expressions *)

fun Asem ( num n ) = ( fn s => n )
  | Asem ( loc l ) = ( fn s => s l )
  | Asem ( plus(a1,a2) ) = ( fn s => (Asem a1 s) + (Asem a2 s) )
  | Asem ( minus(a1,a2) ) = ( fn s => (Asem a1 s) - (Asem a2 s) )
  | Asem ( mult(a1,a2) ) = ( fn s => (Asem a1 s) * (Asem a2 s) )  ;

fun Bsem ( tt ) = ( fn s => true )
  | Bsem ( ff ) = ( fn s => false )
  | Bsem ( neg b ) = ( fn s => not (Bsem b s) )
  | Bsem ( conj(b1,b2) ) = ( fn s => (Bsem b1 s) andalso (Bsem b2 s) )
  | Bsem ( disj(b1,b2) ) = ( fn s => (Bsem b1 s) orelse (Bsem b2 s) )
  | Bsem ( eq(a1,a2) ) = ( fn s => (Asem a1 s) = (Asem a2 s) )
  | Bsem ( gt(a1,a2) ) = ( fn s => (Asem a1 s) > (Asem a2 s) )  ;

(* Typed call-by-value fix *)

datatype ('a,'b) F = fold of ('a,'b) F -> 'a -> 'b  ;

fun unfold (fold x) = x  ;

val fix 
  = fn f => 
      let 
        val D = fn x => fn y => f ( (unfold x) x ) y 
      in 
        D (fold D)
      end ;

(* Semantic function for commands *)

fun Csem ( skip ) = ( fn s => s )
  | Csem ( assign(x,a) ) 
      = ( fn s => fn l => if l=x then Asem a s else s l )
  | Csem ( cond(b,c1,c2) )
      = ( fn s => if (Bsem b s) 
                  then ( Csem c1 s ) 
                  else ( Csem c2 s ) )
  | Csem ( seq(c1,c2) )
      = ( fn s => Csem c2 (Csem c1 s) )
  | Csem ( whi(b,c) )
      = fix( fn w => fn s => if (Bsem b s) then w( Csem c s ) else s )  ;

(* Factorial *)

val fact
  = whi( gt(loc"X",num 0) ,
        seq( assign( "Y",mult(loc"X",loc"Y") ) ,
             assign( "X",minus(loc"X",num 1) ) ) )  ;

fun store [] = ( fn l => 0 )
  | store ( (l,x)::t ) 
      = ( fn k => if k=l then x else store t k )  ;

Csem fact ( store [("X",5),("Y",3)] ) "Y"  ;

Csem fact ( store [("X",6),("Y",~1)] ) "Y"  ;

Csem ( whi( tt, skip ) ) ;