let rec ------------------------------------------- semantic types ------------
    type Val = IntVal  Int +                     -- Int
               BoolVal Bool +                    -- Bool
               ListVal Val Val + NilVal +        -- Lists
               FnVal   (Val->Kont->State->Val) + -- Abstractions
               Thunk   (Kont->State->Val) +      -- params, bindings

               LogicVar Locn +                   -- see Store
               unground +                        -- unground LogicVar's value
               Wrong   String                    -- error

and type Env == Ide -> Val        -- rho :Env, maps Identifiers to their values
    and rho0 x = Wrong("undeclared: " @ x)    -- empty, initial environment

and type Locn == Int                      -- "addresses" of logic variables
and type Store == Locn -> Val             -- gives Vals of logic vars if known
    and  s0 addr = unground
and type State = st Locn Store            -- freeCounter # Store
    and  st0 = st 0 s0
and type Kont == Val -> State -> Val      -- Expression Kontinuations
    and  k0 = Copy 0

and deref (LogicVar n) k (st f s) =
       let v = s n
       in case v in unground  : k (LogicVar n) (st f s) ||
                    LogicVar m: deref (LogicVar m) k (st f s) ||
                    v         : deref v k (st f s)
          end ||
    deref (Thunk t) k s = let  k2 v = deref v k  in  t k2 s ||
    deref  v k s = k v s

and ShowVal (IntVal n)    = itos n ||
    ShowVal (BoolVal b)   = if b then "T" else "F" ||
    ShowVal (ListVal h t) = "(" @ (ShowVal h) @ "::" @ (ShowVal t) @ ")" ||
    ShowVal  NilVal       = "Nil" ||
    ShowVal (FnVal f)     = "function()" ||
    ShowVal (Thunk _)     = "thunk" ||
    ShowVal (LogicVar n)  = "LV_" @ (itos n) ||
    ShowVal  unground     = "unground" ||
    ShowVal (Wrong s)     = "Wrong: " @ s

and Copy f (LogicVar n) s =
       let k (LogicVar n) s &(n>=f) = unground   || -- a "local" unground one
           k (LogicVar n) s         = LogicVar n || -- non-local unground
           k v s = Copy f v s                       -- ground to v
       in deref (LogicVar n) k s ||
    Copy f (ListVal h t) s = ListVal (Copy f h s) (Copy f t s) ||
    Copy f (Thunk t) s = t (Copy f) s ||
    Copy f v _ = v

and append  NilVal       L = L ||
    append (ListVal h t) L = ListVal h (append t L)

and update f x v y = if x=y then v else f y  -- esp' f is Store or Env

in let rec --------------------------------------------------------------------
--  E : Exp -> Env -> Kont -> State -> Val
    E (Ident x)   rho k s = deref (rho x) k s ||
    E (Num n)     _   k s = k(IntVal n) s     ||
    E (Boolean b) _   k s = k(BoolVal b) s    ||
    E NIL         _   k s = k(NilVal) s       ||

    E (LogicExp x C) rho k (st f s) =            -- list of x s.t. constraint C
       let rho2 = update rho x (LogicVar f)
       and st2  = st (f+1) s
       in let k2 (BoolVal b) st3 =
              if b then
                 let k3 v s = ListVal (Copy f v st3) NilVal
                 in E (Ident x) rho2 k3 st3        -- one soln
              else NilVal                          -- no  solution
       in k( E C rho2 k2 st2 ) (st f s)        ||

    E (Block isRec Local Body) rho k s = E Body (D isRec Local rho) k s ||

    E (Apply Fn Actual) rho k s =
       let k2 (FnVal f) s = f (Thunk(E Actual rho)) k s in  E Fn rho k2 s  ||

    E (LambdaExp x Body) rho k s =
       let  f v = E Body (update rho x v) in  k (FnVal f) s  ||

    E (IfExp Se Te Fe) rho k s =
       let k2 (BoolVal b) = E (if b then Te else Fe) rho k
       in  E Se rho k2 s  ||

    E (UExp Opr Argh) rho k s =
       let  k2 v = let k3 v = U Opr v k
                   in deref v k3
       in  E Argh rho k2 s ||

    E (BExp consSy A1 A2) rho k s =
       B consSy (Thunk(E A1 rho)) (Thunk(E A2 rho)) k s  || -- cons lazy

    E (BExp Opr A1 A2) rho k s =
       let k1 v1 =
           let k1b v1 =
               let k2 v2 =
                   let k2b v2 = B Opr v1 v2 k
                   in  deref v2 k2b
               in  E A2 rho k2
           in  deref v1 k1b
       in  E A1 rho k1 s

--  D : Bool -> Dec -> Env -> Env
and D  isRec    L   oldRho =
    let rec
        newRho = DD L (if isRec then newRho else oldRho) oldRho
    and DD (Decs d1 ds) useRho grow = DD d1 useRho (DD ds useRho grow) ||
        DD (Bind x e)   useRho grow =
           let eVal = Thunk(E e useRho)
           in  update grow x eVal
    in newRho

--------------------------------------------------------------------- Operators

and setHT n (st f s) =  -- bind H::T to n where H, T new logic vars
       let H=LogicVar f and T=LogicVar(f+1)            -- new Locns
       in  st (f+2) (update s n (ListVal H T))         -- n := H::T

and U plusSy  (IntVal n)    k s = k(IntVal  n) s       ||
    U minusSy (IntVal n)    k s = k(IntVal  (-n)) s    ||

    U notSy   (BoolVal b)   k s = k(BoolVal (~b)) s    ||

    U nullSy  (ListVal _ _) k s = k(BoolVal false) s   ||
    U nullSy   NilVal       k s = k(BoolVal true) s    ||
    U nullSy  (LogicVar n)  k (st f s) =
       append (k (BoolVal true)  (st f (update s n NilVal)))  -- nil  or ...
              (k (BoolVal false) (setHT n (st f s)))   ||     -- ... not nil

    U hdSy    (ListVal h t) k s =  k h s        ||
    U tlSy    (ListVal h t) k s =  k t s        ||
    U hdSy    (LogicVar n)  k (st f s) = k (LogicVar f) (setHT n (st f s)) ||
    U tlSy    (LogicVar n)  k (st f s) = k (LogicVar (f+1)) (setHT n (st f s))

-------------------------------------------------------------------------------
and
    B eqSy (LogicVar n) v k (st f s) =                           -- Unification
       append (k(BoolVal true )(st f (update s n v)))
              (k(BoolVal false)(st f s))   ||      -- ??? should constrain n<>v
    B eqSy v (LogicVar n) k s = B eqSy (LogicVar n) v k s ||  -- switch

    B consSy h t k s = k (ListVal h t) s ||

    B opr (IntVal m) (IntVal n) k s =
       case opr in plusSy  : k(IntVal( m+n )) s    ||
                   minusSy : k(IntVal( m-n )) s    ||
                   timesSy : k(IntVal( m*n )) s    ||
                   divSy   : k(IntVal( m%n )) s    ||
                   eqSy    : k(BoolVal( m=n)) s    ||
                   neSy    : k(BoolVal( m~=n)) s   ||
                   leSy    : k(BoolVal( m<=n )) s  ||
                   ltSy    : k(BoolVal( m<n )) s   ||
                   geSy    : k(BoolVal( m>=n )) s  ||
                   gtSy    : k(BoolVal( m>n )) s
       end  ||

    B opr (BoolVal p) (BoolVal q) k s =
       case opr in orSy  : k(BoolVal( p|q )) s     ||
                   andSy : k(BoolVal( p&q )) s
       end

-------------------------------------------------------------------------------
-- Executable Denotational Semantics of Lambda Calculus / FP
-- Continuation Style
-- (c) L. Allison 1994