Sterling Example: modelingMSOS:vars

File: vars.sos

[Reduce File] [Raw File]

Module modelingMSOS:vars

Builds on modelingMSOS:host

/*MSOS paper includes vars in initial language, but it really doesn't
  have to do so; they work as an extension/addition along with let*/

e ::= ...
    | var(string)
    | let(string, e, e)

-------------------------- [P-Var]
|{e}- var(X) ~~> intlit(0)


------------------------------------------ [P-Let]
|{e}- let(X, E1, E2) ~~> bOp(E1, plus, E2)



c ::= ...
    | decl(string, e)
/*note this declares a constant that cannot be updated*/

------------------------- [P-Decl]
|{c}- decl(X, E) ~~> nill



ctxElem ::= ...
          | env([(string, e)])

---------------------------------- [P-Env]
|{ctxElem}- env(G) ~~> placeholder




getEnv Ctx G
lookup G X V
------------------- [E-Var]
ev Ctx var(X) V Ctx


ev Ctx E1 E11 Ctx1
------------------------------------------ [E-Let-Step]
ev Ctx let(X, E1, E2) let(X, E11, E2) Ctx1


value E1
/*update binding for X to eval E2*/
getEnv Ctx G
replaceEnv Ctx (X, E1)::G Ctx1
/*eval E2*/
ev Ctx1 E2 E21 Ctx2
/*undo update, but taking any non-env changes from E2*/
replaceEnv Ctx2 G Ctx3
------------------------------------------ [E-Let]
ev Ctx let(X, E1, E2) let(X, E1, E21) Ctx3


value E2
---------------------------- [E-Let-End]
ev Ctx let(X, E1, E2) E2 Ctx



ev Ctx E E1 Ctx1
------------------------------------ [E-Decl-Step]
ev_c Ctx decl(X, E) decl(X, E1) Ctx1


value E
getEnv Ctx G
replaceEnv Ctx (X, E)::G Ctx1
----------------------------- [E-Decl-End]
ev_c Ctx decl(X, E) nill Ctx1
/*becomes nill because no more computation remains*/



/*Find/Replace *an* env in the context
  May not be first one, so should be only one for well-formedness*/
Fixed Judgment getEnv : [ctxElem] [(string, e)]
Fixed Judgment replaceEnv : [ctxElem] [(string, e)] [ctxElem]

===================== [GE-First]
getEnv env(G)::Rest G


getEnv Rest G
================= [GE-Later]
getEnv CE::Rest G



======================================= [RE-First]
replaceEnv env(G0)::Rest G env(G)::Rest


replaceEnv Rest G Rest1
=============================== [RE-Later]
replaceEnv CE::Rest G CE::Rest1