------------------
--- FUN Syntax ---
------------------

fmod QID# is
  including QID * (
  op _+_ to _#+#_,op _-_ to _#-#_,op _*_ to _#*#_,op _/_ to _#/#_,
  op _<_ to _#<#_,op _<=_ to _#<=#_,op _>_ to _#>#_,op _>=_ to _#>=#_
  ) .
endfm

fmod INT# is
  including INT * (
  op _+_ to _#+#_,op _-_ to _#-#_,op _*_ to _#*#_,op _/_ to _#/#_,
  op _<_ to _#<#_,op _<=_ to _#<=#_,op _>_ to _#>#_,op _>=_ to _#>=#_
  ) .
endfm

fmod NAME is
  including QID# .
  sort Name .
  subsort Qid < Name .
  ops a b c d e f g h i j k l m n o p q r s t u v x y z w : -> Name .
endfm

fmod NAME-LIST is
  including NAME .
  sort NameList .
  subsort Name < NameList .
  op `(`) : -> NameList .
  op _,_ : NameList NameList -> NameList [assoc id: ()] .
endfm

fmod GENERIC-EXP-SYNTAX is
  including NAME .
  including INT# .
  sort Exp .
  subsorts Int Name < Exp .
endfm

fmod EXP-LIST is
  including GENERIC-EXP-SYNTAX .
  including NAME-LIST .
  sort ExpList .
  subsorts Exp NameList < ExpList .
  op _,_ : ExpList ExpList -> ExpList [ditto] .
endfm

fmod ARITHMETIC-EXP-SYNTAX is
  including GENERIC-EXP-SYNTAX .
  ops _+_ _-_ : Exp Exp -> Exp [prec 33 gather (E e)] .
  ops _*_ _/_ _%_ : Exp Exp -> Exp [prec 31 gather (E e)] .
endfm

fmod BOOLEAN-EXP-SYNTAX is
  including GENERIC-EXP-SYNTAX .
  ops true false : -> Exp .
  ops _==_ _<=_ _>=_ _and_ _or_ : Exp Exp -> Exp .
  op not_ : Exp -> Exp .
endfm

fmod IF-SYNTAX is
  including GENERIC-EXP-SYNTAX .
  op if_then_else_ : Exp Exp Exp -> Exp .
endfm

fmod FUNCTION-SYNTAX is
  including EXP-LIST .
  op fun_->_ : NameList Exp -> Exp .
  op __ : Exp ExpList -> Exp [prec 0] .
endfm

fmod BINDING-SYNTAX is
  including GENERIC-EXP-SYNTAX .
  including NAME-LIST .
  sorts Binding Bindings .
  subsort Binding < Bindings .
  op _=_ : Exp Exp -> Binding .
  op _and_ : Bindings Bindings -> Bindings [assoc prec 100] .
endfm

fmod LET-SYNTAX is
  including BINDING-SYNTAX .
  op let_in_ : Bindings Exp -> Exp .
endfm

fmod LETREC-SYNTAX is
  including BINDING-SYNTAX .
  op let`rec_in_ : Bindings Exp -> Exp .
endfm

fmod LIST-SYNTAX is
  including EXP-LIST .
  op [] : -> Exp .
  op [_] : ExpList -> Exp .
  ops car cdr null? : Exp -> Exp .
  op cons : Exp Exp -> Exp .
endfm

fmod POINTER-SYNTAX is
  including GENERIC-EXP-SYNTAX .
  ops &_ *_ : Name -> Exp .
endfm

fmod ASSIGNMENT-SYNTAX is
  including GENERIC-EXP-SYNTAX .
  op _:=_ : Exp Exp -> Exp .
endfm

fmod SEQ-COMP-SYNTAX is
  including GENERIC-EXP-SYNTAX .
  op _;_ : Exp Exp -> Exp [assoc prec 50] .
endfm

fmod BLOCK-SYNTAX is
  including SEQ-COMP-SYNTAX .
  op {} : -> Exp .
  op {_} : Exp -> Exp .
endfm

fmod LOOP-SYNTAX is
  including GENERIC-EXP-SYNTAX .
  op while__ : Exp Exp -> Exp .
  op for(_;_;_)_ : Exp Exp Exp Exp -> Exp .
endfm

fmod FUN-SYNTAX is
  including ARITHMETIC-EXP-SYNTAX .
  including BOOLEAN-EXP-SYNTAX .
  including IF-SYNTAX .
  including FUNCTION-SYNTAX .
  including LET-SYNTAX .
  including LETREC-SYNTAX .
  including LIST-SYNTAX .
  including ASSIGNMENT-SYNTAX .
  including SEQ-COMP-SYNTAX .
  including BLOCK-SYNTAX .
  including LOOP-SYNTAX .
  including POINTER-SYNTAX .
endfm


---------------------
--- Fun Semantics ---
---------------------

fmod LOCATION is
  including INT# .
  sort Location .
  op loc : Nat -> Location .
endfm

fmod LOCATION-LIST is
  including LOCATION .
  sort LocationList .
  subsort Location < LocationList .
  op nil : -> LocationList .
  op _,_ : LocationList LocationList -> LocationList [assoc id: nil] .
  op locs : Nat Nat -> LocationList .
  vars N # : Nat .
  eq locs(N, 0) = nil .
  eq locs(N, #) = loc(N), locs(N #+# 1, # #-# 1) .
endfm

fmod ENVIRONMENT is
  including NAME-LIST .
  including LOCATION-LIST .
  sort Env .
  op empty : -> Env .
  op [_,_] : Name Location -> Env .
  op __ : Env Env -> Env [assoc comm id: empty] .
  op _[_] : Env Name -> [Location] .
  op _[_<-_] : Env NameList LocationList -> [Env] .
  vars X X' : Name .  vars Env : Env .  vars L L' : Location .
  var Xl : NameList .  var Ll : LocationList .
  eq ([X,L] Env)[X] = L .
  eq ([X',L'] Env)[X <- L] = if X == X' then [X',L] Env else [X',L'] (Env[X <- L]) fi .
  eq empty[X <- L] = [X,L] .
  eq Env[X,Xl <- L,Ll] = Env[X <- L][Xl <- Ll] .
  eq Env[() <- nil] = Env .
endfm

fmod VALUE is
  sort Value .
  op nothing : -> Value .
endfm

fmod VALUE-LIST is
  including VALUE .
  sort ValueList .
  subsort Value < ValueList .
  op nil : -> ValueList .
  op _,_ : ValueList ValueList -> ValueList [assoc id: nil] .
endfm

fmod STORE is
  including LOCATION-LIST .
  including VALUE-LIST .
  sort Store .
  op empty : -> Store .
  op [_,_] : Location Value -> Store .
  op __ : Store Store -> Store [assoc comm id: empty] .
  op _[_] : Store Location -> [Value] .
  op _[_<-_] : Store LocationList ValueList -> [Store] .
  vars L L' : Location .  var Mem : Store .  vars V V' : Value .
  var Ll : LocationList .  var Vl : ValueList .
  eq ([L,V] Mem)[L] = V .
  eq ([L',V'] Mem)[L <- V] = if L == L' then [L',V] Mem else [L',V'] (Mem[L <- V]) fi .
  eq empty[L <- V] = [L,V] .
  eq Mem[L,Ll <- V,Vl] = Mem[L <- V][Ll <- Vl] .
  eq Mem[nil <- nil] = Mem .
endfm

fmod CONTINUATION is
  sorts Continuation ContinuationItem .
  op stop : -> Continuation .
  op _->_ : ContinuationItem Continuation -> Continuation .
endfm

fmod FUN-STATE is
  sorts PLStateAttribute PLState .
  subsort PLStateAttribute < PLState .
  including ENVIRONMENT .
  including STORE .
  including CONTINUATION .
  op empty : -> PLState .
  op __ : PLState PLState -> PLState [assoc comm id: empty] .
  op nextLoc : Nat -> PLStateAttribute .
  op mem : Store -> PLStateAttribute .
  op k : Continuation -> PLStateAttribute .
  op x : Continuation -> PLStateAttribute .
endfm

fmod FUN-HELPING-OPERATIONS is
  including NAME-LIST .
  including EXP-LIST .
  including FUN-STATE .

  var X : Name .  vars E E' : Exp .  var El : ExpList .  var K : Continuation .
  vars V : Value .  var Vl : ValueList .  var Xl : NameList .
  var Env : Env .  var Mem : Store .  var N : Nat .  var Ll : LocationList .

  op exp : ExpList Env -> ContinuationItem .
  op val_ : ValueList -> ContinuationItem .
  eq k(exp((), Env) -> K) = k(val(nil) -> K) .
  eq k(exp((E,E',El), Env) -> K) = k(exp(E, Env) -> exp((E',El), Env) -> K) .
  eq k(val(V) -> exp(El, Env) -> K) = k(exp(El, Env) -> val(V) -> K) .
  eq k(val(Vl) -> val(V) -> K) = k(val(V,Vl) -> K) .

  op bindTo : NameList Env -> ContinuationItem .
  op bindTo : NameList Env LocationList -> ContinuationItem .
  eq bindTo(Xl,Env) = bindTo(Xl, Env, nil) .
  eq k(val(V,Vl) -> bindTo((X,Xl), Env, Ll) -> K)
     mem(Mem) nextLoc(N)
   = k(val(Vl) -> bindTo(Xl, Env[X <- loc(N)], (Ll,loc(N))) -> K)
     mem(Mem [loc(N),V]) nextLoc(N #+# 1) .
  eq k(val(nil) -> bindTo((), Env, Ll) -> K) = k(pair(Env, Ll) -> K) .
  eq k(bindTo((X,Xl), Env, Ll) -> K) nextLoc(N)
   = k(bindTo(Xl, Env[X <- loc(N)], (Ll,loc(N))) -> K) nextLoc(N #+# 1) .
  eq k(bindTo((), Env, Ll) -> K) = k(pair(Env,Ll) -> K) .

  op writeTo_ : LocationList -> ContinuationItem .
  eq k(val(Vl) -> writeTo(Ll) -> K) mem(Mem)
   = k(K) mem(Mem[Ll <- Vl]) .

  op pair : Env LocationList -> ContinuationItem .
  ops exp exp* : ExpList -> ContinuationItem .
  op writeTo : -> ContinuationItem .
  eq pair(Env,Ll) -> exp(El) -> K = exp(El, Env) -> pair(Env, Ll) -> K .
  eq pair(Env,Ll) -> writeTo -> K = writeTo(Ll) -> pair(Env,Ll) -> K .
  eq pair(Env,Ll) -> exp*(E) -> K = exp(E, Env) -> K .

  op discard : -> ContinuationItem .
  eq k(val(Vl) -> discard -> K) = k(K) .
endfm

fmod GENERIC-EXP-SEMANTICS is
  including FUN-HELPING-OPERATIONS .
  op int : Int -> Value .
  var I : Int .  var X : Name .  var L : Location .  var V : Value .
  var K : Continuation .  var Env : Env .  var Mem : Store .

  eq k(exp(I, Env) -> K) = k(val(int(I)) -> K) .
  eq k(exp(X, ([X,L] Env)) -> K) mem(Mem)
   = k(val(Mem[L]) -> K) mem(Mem) .
endfm

fmod ARITHMETIC-EXP-SEMANTICS is
  including ARITHMETIC-EXP-SYNTAX .
  including GENERIC-EXP-SEMANTICS .
  vars E E' : Exp .  var K : Continuation .  vars I I' : Int .  var Env : Env .
  ops + - * / % : -> ContinuationItem .
  eq k(exp(E + E', Env) -> K) = k(exp((E,E'),Env) -> + -> K) .
  eq k(val(int(I),int(I')) -> + -> K) = k(val(int(I #+# I')) -> K) .
  eq k(exp(E - E', Env) -> K) = k(exp((E,E'), Env) -> - -> K) .
  eq k(val(int(I),int(I')) -> - -> K) = k(val(int(I #-# I')) -> K) .
  eq k(exp(E * E', Env) -> K) = k(exp((E,E'), Env) -> * -> K) .
  eq k(val(int(I),int(I')) -> * -> K) = k(val(int(I #*# I')) -> K) .
  eq k(exp(E / E', Env) -> K) = k(exp((E,E'), Env) -> / -> K) .
  ceq k(val(int(I),int(I')) -> / -> K) = k(val(int(I quo I')) -> K) 
  if I' =/= 0 .
  eq k(exp(E % E', Env) -> K) = k(exp((E,E'), Env) -> % -> K) .
  ceq k(val(int(I),int(I')) -> % -> K) = k(val(int(I rem I')) -> K) 
  if I' =/= 0 .
endfm

fmod BOOLEAN-EXP-SEMANTICS is
  including BOOLEAN-EXP-SYNTAX .
  including GENERIC-EXP-SEMANTICS .
  op bool : Bool -> Value .
  ops == <= >= and or not : -> ContinuationItem .
  vars E E' : Exp .  var K : Continuation .
  vars I I' : Int .  vars B B' : Bool .  var Env : Env .
  eq k(exp(true, Env) -> K) = k(val(bool(true)) -> K) .
  eq k(exp(false, Env) -> K) = k(val(bool(false)) -> K) .
  eq k(exp(E == E', Env) -> K) = k(exp((E,E'), Env) -> == -> K) .
  eq k(val(int(I),int(I')) -> == -> K) = k(val(bool(I == I')) -> K) .
  eq k(exp(E <= E', Env) -> K) = k(exp((E,E'), Env) -> <= -> K) .
  eq k(val(int(I),int(I')) -> <= -> K) = k(val(bool(I #<=# I')) -> K) .
  eq k(exp(E >= E', Env) -> K) = k(exp((E,E'), Env) -> >= -> K) .
  eq k(val(int(I),int(I')) -> >= -> K) = k(val(bool(I #>=# I')) -> K) .
  eq k(exp(E and E', Env) -> K) = k(exp((E,E'), Env) -> and -> K) .
  eq k(val(bool(B),bool(B')) -> and -> K) = k(val(bool(B and B')) -> K) .
  eq k(exp(E or E', Env) -> K) = k(exp((E,E'), Env) -> or -> K) .
  eq k(val(bool(B),bool(B')) -> or -> K) = k(val(bool(B or B')) -> K) .
  eq k(exp(not E, Env) -> K) = k(exp(E, Env) -> not -> K) .
  eq k(val(bool(B)) -> not -> K) = k(val(bool(not B)) -> K) .
endfm

fmod IF-SEMANTICS is
  including IF-SYNTAX .
  including BOOLEAN-EXP-SEMANTICS .
  vars BE E E' : Exp .  var K : Continuation .
  var B : Bool .  var Env : Env .
  op if : Exp Exp Env -> ContinuationItem .
  eq k(exp(if BE then E else E', Env) -> K)
   = k(exp(BE,Env) -> if(E,E',Env) -> K) .
  eq k(val(bool(B)) -> if(E,E',Env) -> K)
   = k(exp(if B then E else E' fi, Env) -> K) .
endfm

fmod FUNCTION-SEMANTICS is
  including GENERIC-EXP-SEMANTICS .
  including FUNCTION-SYNTAX .
  op closure : NameList Exp Env -> Value .
  op apply : -> ContinuationItem .
  var Xl : NameList .  vars F Body : Exp .  var K : Continuation .
  var Env : Env .  var El : ExpList .  var Vl : ValueList .
  eq k(exp(fun Xl -> Body, Env) -> K) = k(val(closure(Xl, Body, Env)) -> K) .
  eq k(exp(F(El), Env) -> K) = k(exp((F,El), Env) -> apply -> K) .
  eq k(val(closure(Xl, Body, Env),Vl) -> apply -> K)
   = k(val(Vl) -> bindTo(Xl, Env) -> exp*(Body) -> K) .
endfm

fmod BINDING-SEMANTICS is
  including BINDING-SYNTAX .
  including FUNCTION-SEMANTICS .
  op `(_,_`) : NameList ExpList -> Bindings .
  var X : Name .  vars Xl Xl' : NameList .
  var E : Exp .  vars El El' : ExpList .
  eq (X(Xl) = E) = (X = fun Xl -> E) .
  eq (X = E) = (X, E) .
  eq (Xl, El) and (Xl', El') = ((Xl,Xl'), (El,El')) .
endfm

fmod LET-SEMANTICS is
  including LET-SYNTAX .
  including BINDING-SEMANTICS .
  var Xl : NameList .  var El : ExpList .  var E : Exp .
  var K : Continuation .  var Env : Env .
  eq k(exp(let (Xl,El) in E, Env) -> K)
   = k(exp(El, Env) -> bindTo(Xl, Env) -> exp*(E) -> K) .
endfm

fmod LETREC-SEMANTICS is
  including LETREC-SYNTAX .
  including BINDING-SEMANTICS .
  var Xl : NameList .  var K : Continuation .
  var El : ExpList .  var E : Exp .  var Env : Env .
  eq k(exp(let rec (Xl,El) in E, Env) -> K)
   = k(bindTo(Xl,Env) -> exp(El) -> writeTo -> exp*(E) -> K) .
endfm

fmod LIST-SEMANTICS is
  including LIST-SYNTAX .
  including BOOLEAN-EXP-SEMANTICS .
  op [_] : ValueList -> Value .
  ops mkList car cdr cons null? : -> ContinuationItem .
  vars E E' : Exp .  var El : ExpList .  var Env : Env .
  var K : Continuation .  var V : Value .  var Vl : ValueList .
  eq k(exp([], Env) -> K) = k(val([nil]) -> K) .
  eq k(exp([El], Env) -> K) = k(exp(El, Env) -> mkList -> K) .
  eq k(val(Vl) -> mkList -> K) = k(val([Vl]) -> K) .
  eq k(exp(car(E), Env) -> K) = k(exp(E, Env) -> car -> K) .
  eq k(val([V,Vl]) -> car -> K) = k(val(V) -> K) .
  eq k(exp(cdr(E), Env) -> K) = k(exp(E, Env) -> cdr -> K) .
  eq k(val([V,Vl]) -> cdr -> K) = k(val([Vl]) -> K) .
  eq k(exp(cons(E,E'), Env) -> K) = k(exp((E,E'), Env) -> cons -> K) .
  eq k(val(V,[Vl]) -> cons -> K) = k(val([V,Vl]) -> K) .
  eq k(exp(null?(E), Env) -> K) = k(exp(E, Env) -> null? -> K) .
  eq k(val([Vl]) -> null? -> K) = k(val(bool(Vl == nil)) -> K) .
endfm

fmod ASSIGNMENT-SEMANTICS is
  including ASSIGNMENT-SYNTAX .
  including GENERIC-EXP-SEMANTICS .
  var X : Name .  var E : Exp .  var K : Continuation .
  var Env : Env .  var L : Location .
  eq k(exp(X := E, ([X,L] Env)) -> K)
   = k(exp(E, ([X,L] Env)) -> writeTo(L) -> val(nothing) -> K) .
endfm

fmod SEQ-COMP-SEMANTICS is
  including SEQ-COMP-SYNTAX .
  including GENERIC-EXP-SEMANTICS .
  vars E E' : Exp .  var K : Continuation .  var V : Value .  var Env : Env .
  eq k(exp(E ; E', Env) -> K)
   = k(exp(E, Env) -> discard -> exp(E', Env) -> K) .
endfm

fmod BLOCK-SEMANTICS is
  including BLOCK-SYNTAX .
  including GENERIC-EXP-SEMANTICS .
  var E : Exp .  var K : Continuation .  var Env : Env .
  eq k(exp({}, Env) -> K) = k(val(nothing) -> K) .
  eq k(exp({E}, Env) -> K) = k(exp(E, Env) -> K) .
endfm

fmod LOOP-SEMANTICS is
  including LOOP-SYNTAX .
  including IF-SEMANTICS .
  including BLOCK-SEMANTICS .
  including SEQ-COMP-SEMANTICS .
  vars Start Cond Step Body : Exp .  var K : Continuation .  var Env : Env .
  eq for(Start ; Cond ; Step) Body = Start ; while Cond {Body ; Step} .
  eq k(exp(while Cond Body, Env) -> K)
   = k(exp(Cond, Env) -> if(Body ; while Cond Body, {}, Env) -> K) .
endfm

fmod POINTER-SEMANTICS is
  including POINTER-SYNTAX .
  including ASSIGNMENT-SYNTAX .
  including FUN-HELPING-OPERATIONS .
  op pointer : Location -> Value .
  var E : Exp .
  var X : Name .
  var V : Value .
  var Env : Env .
  var Mem : Store .
  var L1 L2 : Location .
  var K : Continuation .

  eq k(exp(& X, Env) -> K) = k(val(pointer(Env[X])) -> K) .
  eq k(exp(* X, ([X,L1] Env)) -> K) mem([L1,pointer(L2)] [L2,V] Mem)
    = k(val(V) -> K) mem([L1,pointer(L2)] [L2,V] Mem) .
  eq k(exp(* X := E, ([X,L1] Env)) -> K) mem([L1,pointer(L2)] Mem)
    = k(exp(E, ([X,L1] Env)) -> writeTo(L2) -> val(nothing) -> K) mem([L1,pointer(L2)] Mem) .
endfm


fmod FUN-SEMANTICS is
  including FUN-SYNTAX .
  including ARITHMETIC-EXP-SEMANTICS .
  including BOOLEAN-EXP-SEMANTICS .
  including IF-SEMANTICS .
  including FUNCTION-SEMANTICS .
  including LET-SEMANTICS .
  including LETREC-SEMANTICS .
  including LIST-SEMANTICS .
  including ASSIGNMENT-SEMANTICS .
  including SEQ-COMP-SEMANTICS .
  including BLOCK-SEMANTICS .
  including LOOP-SEMANTICS .
  including POINTER-SEMANTICS .

  ops eval eval* : Exp -> [Value] .
  op  [_]  : PLState -> [Value] .
  op *[_]* : PLState -> [Value] .

  var E : Exp .  var V : Value .  var S : PLState .
  var N : Nat .  var Mem : Store .

  eq eval(E) = [k(exp(E, (empty).Env) -> stop) nextLoc(0) mem(empty)] .
  eq [k(val(V) -> stop) S] = V .

  eq eval*(E) = *[k(exp(E, (empty).Env) -> stop) nextLoc(0) mem(empty)]* .
  eq *[k(val(V) -> stop) nextLoc(N) mem(Mem)]* = V .
endfm

--------------------
--- FUN Examples ---
--------------------

mod FUN-TEST is
  including FUN-SEMANTICS .
endm