498 lines
15 KiB
Text
498 lines
15 KiB
Text
|
------------------
|
||
|
|
--- 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
|
||
|
|
|