Skip to content

Instantly share code, notes, and snippets.

@prepor

prepor/oam.k

Created February 16, 2018 13:46
Show Gist options
  • Save prepor/3e8885c2495ed1c921c5c707a152f38a to your computer and use it in GitHub Desktop.
Save prepor/3e8885c2495ed1c921c5c707a152f38a to your computer and use it in GitHub Desktop.
Download ZIP
Raw
oam.k
module OAM-SYNTAX
syntax Ints ::= List{Int,","}
syntax Op ::= "#parallel" Int Int
| "#otherwise" Int Int
| "#pruning" Int Int Int
| "#sequential" Int Int Int
| "#callFun" Int "[" Ints "]"
| "#callDynamic" Int "[" Ints "]"
| "#ffi" Int "[" Ints "]"
| "#coeffect" Int
| "#stop"
| "#constInt" Int
| "#constBool" Bool
| "#constString" String
| "#closure" Int Int
| "#label" Int
syntax SourceOp ::= Int ":" Op
syntax SourceOps ::= List{SourceOp, " "}
syntax SourceFun ::= Int Int "{" SourceOps "}"
syntax SourceFuns ::= List{SourceFun, " "}
syntax SourceFFI ::= Int String
syntax SourceFFIs ::= List{SourceFFI, " "}
syntax Source ::= "ffi" "{" SourceFFIs "}" SourceFuns
endmodule
module OAM
imports OAM-SYNTAX
syntax Stack ::= stack(List)
syntax Op ::= "#ffiReady" Int
| "#tickWait" Int
syntax List ::= #reverseList(List, List) [function]
rule #reverseList(Res, .List) => Res
rule #reverseList((.List => ListItem(I)) _, (ListItem(I) => .List) _)
syntax Stack ::= #incrementInstances(List, List)
rule <stack>
#incrementInstances(Acc, .List) => stack(#reverseList(.List, Acc))
</stack>
rule <stack>
#incrementInstances(Acc,
(ListItem(fOtherwise(Id, Fun, Op))) XS)
=> stack(#reverseList(.List, Acc) ListItem(fOtherwise(Id, Fun, Op)) XS)
</stack>
<instances>... Id |-> (I => I +Int 1) ...</instances>
rule <stack>
(#incrementInstances(Acc,
(ListItem(fPruning(Id))) XS)
=> stack(#reverseList(.List, Acc) ListItem(fPruning(Id)) XS))
</stack>
<instances>... Id |-> (I => I +Int 1) ...</instances>
rule <stack>
(#incrementInstances(Acc,
(ListItem(fSequential(Id, Param, Fun, Op))) XS)
=> stack(#reverseList(.List, Acc) ListItem(fSequential(Id, Param, Fun, Op)) XS))
</stack>
<instances>... Id |-> (I => I +Int 1) ...</instances>
rule <stack>
#incrementInstances((.List => ListItem(fCall(Env))) _,
(ListItem(fCall(Env)) => .List) _)
</stack>
rule <stack>
#incrementInstances((.List => ListItem($fResult)) _,
(ListItem($fResult) => .List) _)
</stack>
syntax PendValue ::= "pendStopped"
| "pend"
syntax Frame ::= fPruning(Int)
| fOtherwise(Int, Int, Int)
| fSequential(Int, Int, Int, Int)
| fCall(Int)
| "$fResult"
syntax RealVal ::= Int
| Bool
| String
| List
| Map
| "signal"
| closure(Int, Int, Int)
| label(Int)
syntax Val ::= pending(Int) | val(RealVal)
syntax OrcToken ::= OrcToken(Int, Int, Map, Stack)
syntax KResult ::= Val
syntax Stage ::= "INIT" | "RUNNING" | "STOPPED"
configuration <T>
<stage>INIT</stage>
<threads>
<thread multiplicity="*">
<currentFun>0</currentFun>
<pc>-1</pc>
<k>.:Op</k>
<result>.:Val</result>
<stack>stack(.List)</stack>
<currentEnv>0</currentEnv>
<waitEnv>.Map</waitEnv>
<waitEnvKey>0</waitEnvKey>
</thread>
</threads>
<values>.List</values>
<tick>0</tick>
<instances>.Map</instances>
<firstValues>.Map</firstValues>
<pendingValues>.Map</pendingValues>
<envs>
<env multiplicity="*">
<envId>0</envId>
<envContent>.Map</envContent>
</env>
</envs>
<ops>
<op multiplicity="*">
<opFunId>0</opFunId>
<opId>0</opId>
<body>#stop</body>
</op>
</ops>
<initOps>.Map</initOps>
<ffi>.Map</ffi>
<source>$PGM:Source</source>
</T>
rule <source>ffi { _ } Id _ { (OpId : Body) XS => XS } _</source>
<ops>
... (.Bag =>
<op>
<opFunId>Id</opFunId>
<opId>OpId</opId>
<body>Body</body>
</op>)
...</ops>
rule <source>ffi { _ } (Id (InitId => -1) { _ }) _</source>
<initOps>... .Map => Id |-> InitId ...</initOps>
requires InitId =/=Int -1
rule <source>ffi { Id Def:String XS => XS } _</source>
<ffi>... .Map => Id |-> Def ...</ffi>
rule <source>ffi { _ } (_ -1 { .SourceOps } XS:SourceFuns => XS)</source>
rule <source>ffi { .SourceFFIs } .SourceFuns => .:Source</source>
// Main thread
rule <threads>
.Bag => <thread>
<currentFun>0</currentFun>
<pc>-1</pc>
<k>.:Op</k>
<result>.:Val</result>
<stack>stack(ListItem($fResult))</stack>
<currentEnv>!EnvId:Int</currentEnv>
<waitEnv>.Map</waitEnv>
<waitEnvKey>0</waitEnvKey>
</thread>
</threads>
<envs>...
(.Bag =>
<env><envId>!EnvId</envId><envContent>.Map</envContent></env>)
...</envs>
<stage>INIT => RUNNING</stage>
rule <threads>.Bag</threads>
<stage>RUNNING => STOPPED</stage>
// Init op
rule <thread>...
<currentFun>FunId:Int</currentFun>
<pc>-1 => OpId</pc>
...</thread>
<initOps>... FunId |-> OpId ...</initOps>
// Place actual op
rule <thread>...
<pc>OpId</pc>
<currentFun>FunId</currentFun>
<k>. => Body</k>
...</thread>
<op>...
<opFunId>FunId</opFunId>
<opId>OpId</opId>
<body>Body</body>
...</op>
// Tick
// const
rule <thread>...
<k>#constInt I</k>
<result>.:Val => val(I)</result>
...</thread>
rule <thread>...
<k>#constBool V</k>
<result>.:Val => val(V)</result>
...</thread>
rule <thread>...
<k>#constString S</k>
<result>.:Val => val(S)</result>
...</thread>
// parallel
rule <threads>...
<thread>...
<currentFun>Fun</currentFun>
<pc>_ => Op1</pc>
<k>#parallel Op1 Op2 => .</k>
<stack> stack(Stack) => #incrementInstances(.List, Stack)</stack>
<currentEnv>Env</currentEnv>
...</thread>
(.Bag => <thread>
<currentFun>Fun</currentFun>
<pc>Op2</pc>
<k>.:Op</k>
<result>.:Val</result>
<stack>stack(Stack)</stack>
<currentEnv>!NewEnv</currentEnv>
<waitEnv>.Map</waitEnv>
<waitEnvKey>0</waitEnvKey>
</thread>)
...</threads>
<envs>...
<env><envId>Env</envId><envContent>EnvContent</envContent></env>
(.Bag => <env><envId>!NewEnv:Int</envId><envContent>EnvContent</envContent></env>)
...</envs>
// pruning
rule <threads>...
<thread>...
<currentFun>Fun</currentFun>
<pc>_ => Op1</pc>
<k>#pruning Op1 Param Op2 => .</k>
<stack> stack(Stack) => #incrementInstances(.List, Stack)</stack>
<currentEnv>Env</currentEnv>
...</thread>
(.Bag => <thread>
<currentFun>Fun</currentFun>
<pc>Op2</pc>
<k>.:Op</k>
<result>.:Val</result>
<stack>stack(ListItem(fPruning(!Id)) Stack)</stack>
<currentEnv>Env</currentEnv>
<waitEnv>.Map</waitEnv>
<waitEnvKey>0</waitEnvKey>
</thread>)
...</threads>
<instances>... .Map => !Id |-> 1 ...</instances>
<pendingValues>... .Map => !Id |-> pend ...</pendingValues>
<envs>...
<env>
<envId>Env</envId>
<envContent>M => M[Param <- pending(!Id)]</envContent>
</env>
...</envs>
requires Param =/=Int -1
// Otherwise
rule <thread>...
<currentFun>Fun</currentFun>
<pc>_ => Op1</pc>
<k>#otherwise Op1 Op2 => .</k>
<stack>stack(Stack => ListItem(fOtherwise(!Id, Fun, Op2)) Stack)</stack>
...</thread>
<instances>... .Map => !Id |-> 1 ...</instances>
<firstValues>... .Map => !Id |-> false ...</firstValues>
// Sequential
rule <thread>...
<currentFun>Fun</currentFun>
<pc>_ => Op1</pc>
<k>#sequential Op1 Param Op2 => .</k>
<stack>stack(Stack => ListItem(fSequential(!Id, Param, Fun, Op2)) Stack)</stack>
...</thread>
<instances>... .Map => !Id |-> 1 ...</instances>
// Call
rule <thread>...
<k>#callFun Fun [ Param, _ ]</k>
<currentEnv>Env</currentEnv>
...</thread>
<pendingValues>... Id |-> val(Val) ...</pendingValues>
<envs>...
<env>
<envId>Env</envId>
<envContent>... Param |-> (pending(Id) => val(Val)) ...</envContent>
</env>
...</envs>
rule <thread>...
<k>#callFun Fun [ Param, Params => Params ]</k>
<currentEnv>Env</currentEnv>
<waitEnv>... .Map => WaitEnvKey |-> val(Val) ...</waitEnv>
<waitEnvKey>WaitEnvKey => WaitEnvKey +Int 1</waitEnvKey>
...</thread>
<envs>...
<env>
<envId>Env</envId>
<envContent>... Param |-> val(Val) ...</envContent>
</env>
...</envs>
rule <thread>...
<currentFun>_ => Fun</currentFun>
<pc> _ => -1</pc>
<k>#callFun Fun [ .Ints ] => .:Op</k>
<currentEnv>Env => !NewEnv</currentEnv>
<waitEnv>NewEnvContent => .Map</waitEnv>
<waitEnvKey>_ => 0</waitEnvKey>
<stack>stack(Stack) => stack(ListItem(fCall(Env)) Stack)</stack>
...</thread>
<envs>...
(.Bag => <env>
<envId>!NewEnv:Int</envId>
<envContent>NewEnvContent</envContent>
</env>)
...</envs>
// Dynamic Call
rule <thread>...
<k>#callDynamic Target [ _ ]</k>
<currentEnv>Env</currentEnv>
...</thread>
<pendingValues>... Id |-> val(Val) ...</pendingValues>
<envs>...
<env>
<envId>Env</envId>
<envContent>... Target |-> (pending(Id) => val(Val)) ...</envContent>
</env>
...</envs>
rule <thread>...
<k>#callDynamic Target [ Params ] => #callFun Fun [ Params ]</k>
<currentEnv>Env</currentEnv>
...</thread>
<envs>...
<env>
<envId>Env</envId>
<envContent>... Target |-> val(label(Fun)) ...</envContent>
</env>
...</envs>
rule <thread>...
<k>#callDynamic Target [ _ ]</k>
<currentEnv>Env</currentEnv>
<waitEnv>... .Map => Key |-> Val ...</waitEnv>
<waitEnvKey>Key => Key +Int 1</waitEnvKey>
...</thread>
<envs>...
<env>
<envId>Env</envId>
<envContent>...
Target |-> val(closure(Fun, ToCopy => ToCopy -Int 1, ClosureEnv))
...</envContent>
</env>
<env>
<envId>ClosureEnv</envId>
<envContent>... Key |-> Val ...</envContent>
</env>
...</envs>
requires ToCopy >Int 0
// Special case when closure env and caller env are same
rule <thread>...
<k>#callDynamic Target [ _ ]</k>
<currentEnv>Env</currentEnv>
<waitEnv>... .Map => Key |-> Val ...</waitEnv>
<waitEnvKey>Key => Key +Int 1</waitEnvKey>
...</thread>
<envs>...
<env>
<envId>Env</envId>
<envContent>...
Target |-> val(closure(Fun, ToCopy => ToCopy -Int 1, Env))
Key |-> Val
...</envContent>
</env>
...</envs>
requires ToCopy >Int 0
rule <thread>...
<k>#callDynamic Target [ Params ] => #callFun Fun [ Params ]</k>
<currentEnv>Env</currentEnv>
...</thread>
<envs>...
<env>
<envId>Env</envId>
<envContent>...
Target |-> val(closure(Fun, ToCopy, _))
Key |-> Val
...</envContent>
</env>
...</envs>
requires ToCopy =Int 0
// Closure
rule <thread>...
<k>#closure Fun ToCopy</k>
<currentEnv>Env</currentEnv>
<result>.:Val => val(closure(Fun, ToCopy, Env))</result>
...</thread>
// FFI
rule <thread>...
<k>#ffi _ [ Param, Params => Params ]</k>
<currentEnv>Env</currentEnv>
<waitEnv>... .Map => WaitEnvKey |-> val(Val)</waitEnv>
<waitEnvKey>WaitEnvKey => WaitEnvKey +Int 1</waitEnvKey>
...</thread>
<envs>...
<env>
<envId>Env</envId>
<envContent>... Param |-> val(Val) ...</envContent>
</env>
...</envs>
rule <thread>...
<k>#ffi _ [ Param, Params => Params ]</k>
<currentEnv>Env</currentEnv>
<waitEnv>... .Map => WaitEnvKey |-> val(Val)</waitEnv>
<waitEnvKey>WaitEnvKey => WaitEnvKey +Int 1</waitEnvKey>
...</thread>
<pendingValues>... Id |-> val(Val) ...</pendingValues>
<envs>...
<env>
<envId>Env</envId>
<envContent>... Param |-> pending(Id) ...</envContent>
</env>
...</envs>
rule <thread>...
<k>#ffi Id [ .Ints ] => #ffiReady Id</k>
<waitEnv>Content => .Map</waitEnv>
<waitEnvKey>_ => 0</waitEnvKey>
<currentEnv>_ => !Env:Int</currentEnv>
...</thread>
<envs>...
(.Bag => <env>
<envId>!Env</envId>
<envContent>Content</envContent>
</env>)
...</envs>
// Coeffect
rule <thread>...
<k>#coeffect Param</k>
<currentEnv>Env</currentEnv>
...</thread>
<envs>...
<env>
<envId>Env</envId>
<envContent>... Param |-> (pending(Id) => val(Val)) ...</envContent>
</env>
...</envs>
<pendingValues>... Id |-> val(Val) ...</pendingValues>
// Publish
rule <thread>...
<result>val(V)</result>
<stack>stack(ListItem($fResult) XS => XS)</stack>
...</thread>
<values>.List => ListItem(V) ...</values>
requires V =/=K .:Val
rule <thread>...
<result>pending(Id) => val(Val)</result>
<stack>stack(ListItem($fResult) XS)</stack>
...</thread>
<pendingValues>... Id |-> val(Val) ...</pendingValues>
rule <thread>...
<result>V</result>
<stack>stack(ListItem(fPruning(Id)) XS => .List)</stack>
...</thread>
<pendingValues>... Id |-> (pend => V) ...</pendingValues>
<instances>... Id |-> (I => I -Int 1) ...</instances>
requires V =/=K .:Val [pruningTransition]
rule <thread>...
<result>V</result>
<stack>stack(ListItem(fPruning(Id)) XS => .List)</stack>
...</thread>
<pendingValues>... Id |-> val(_) ...</pendingValues>
<instances>... Id |-> (I => I -Int 1) ...</instances>
requires V =/=K .:Val
rule <thread>...
<result>V</result>
<stack>stack(ListItem(fOtherwise(Id, _, _)) XS => XS)</stack>
...</thread>
<firstValues>... Id |-> (_ => true) ...</firstValues>
<instances>... Id |-> (I => I -Int 1) ...</instances>
requires V =/=K .:Val
rule <thread>...
<currentFun>_ => Fun</currentFun>
<pc>_ => Op</pc>
<k>_ => .:Op</k>
<result>V:Val => .</result>
<stack>stack(ListItem(fSequential(Id, Param, Fun, Op)) XS => XS)</stack>
<currentEnv>Env</currentEnv>
...</thread>
<envs>...
<env>
<envId>Env</envId>
<envContent>M => M[Param <- V]</envContent>
</env>
...</envs>
requires V =/=K .:Val
rule <thread>...
<result>V</result>
<stack>stack(ListItem(fCall(Env)) XS => XS)</stack>
<currentEnv>_ => Env</currentEnv>
...</thread>
requires V =/=K .:Val
rule <threads>...
<thread>...
<stack>stack(.List)</stack>
...</thread> => .Bag
</threads>
// Stop
rule <thread>...
<k>#stop</k>
<stack>stack(ListItem(fCall(Env)) XS => XS)</stack>
...</thread>
rule <thread>...
<k>#stop</k>
<stack>stack(ListItem($fResult) XS => XS)</stack>
...</thread>
rule <thread>...
<k>#stop</k>
<stack>stack(ListItem(fPruning(Id)) XS) => .</stack>
...</thread>
<pendingValues>... Id |-> (pend => pendStopped) ...</pendingValues>
<instances>... Id |-> 1 ...</instances>
rule <thread>...
<k>#stop</k>
<stack>stack(ListItem(fPruning(Id)) XS) => .</stack>
...</thread>
<instances>... Id |-> (I => I -Int 1)...</instances>
requires I >Int 1
rule <thread>...
<k>#stop</k>
<stack>stack(ListItem(fSequential(Id, _, _, _)) XS => XS)</stack>
...</thread>
<instances>... Id |-> 1 ...</instances>
rule <thread>...
<k>#stop</k>
<stack>stack(ListItem(fSequential(Id, _, _, _)) XS) => .</stack>
...</thread>
<instances>... Id |-> (I => I -Int 1)...</instances>
requires I >Int 1
rule <threads>...
<thread>...
<k>#stop</k>
<stack>stack(ListItem(fOtherwise(Id, Fun, Op)) Stack => .List)</stack>
<currentEnv>Env</currentEnv>
...</thread>
(.Bag => <thread>
<currentFun>Fun</currentFun>
<pc>Op</pc>
<k>.:Op</k>
<result>.:Val</result>
<stack>stack(Stack)</stack>
<currentEnv>Env</currentEnv>
</thread>)
...</threads>
<firstValues>... Id |-> false ...</firstValues>
<instances>... Id |-> 1 ...</instances>
rule <thread>...
<k>#stop</k>
<stack>stack(ListItem(fOtherwise(Id, _, _)) _ => .List)</stack>
...</thread>
<firstValues>... Id |-> false ...</firstValues>
<instances>... Id |-> (I => I -Int 1)...</instances>
requires I >Int 1
rule <thread>...
<k>#stop</k>
<stack>stack(ListItem(fOtherwise(Id, _, _)) XS => XS)</stack>
...</thread>
<firstValues>... Id |-> false ...</firstValues>
<instances>... Id |-> I...</instances>
requires I =Int 1
// Prims
// "core.let"
rule <thread>...
<k>#ffiReady Id</k>
<result>.:Val => Val</result>
<currentEnv>Env</currentEnv>
...</thread>
<ffi>... Id |-> "core.let" ...</ffi>
<env><envId>Env</envId><envContent>0 |-> Val</envContent></env>
// "core.add"
rule <thread>...
<k>#ffiReady Id</k>
<result>.:Val => val(X +Int Y) </result>
<currentEnv>Env</currentEnv>
...</thread>
<ffi>... Id |-> "core.add" ...</ffi>
<env>
<envId>Env</envId>
<envContent>0 |-> val(X:Int) 1 |-> val(Y:Int)</envContent>
</env>
// "core.sub"
rule <thread>...
<k>#ffiReady Id</k>
<result>.:Val => val(X -Int Y) </result>
<currentEnv>Env</currentEnv>
...</thread>
<ffi>... Id |-> "core.sub" ...</ffi>
<env>
<envId>Env</envId>
<envContent>0 |-> val(X:Int) 1 |-> val(Y:Int)</envContent>
</env>
// "core.mult"
rule <thread>...
<k>#ffiReady Id</k>
<result>.:Val => val(X *Int Y) </result>
<currentEnv>Env</currentEnv>
...</thread>
<ffi>... Id |-> "core.mult" ...</ffi>
<env>
<envId>Env</envId>
<envContent>0 |-> val(X:Int) 1 |-> val(Y:Int)</envContent>
</env>
// "core.div"
rule <thread>...
<k>#ffiReady Id</k>
<result>.:Val => val(X /Int Y) </result>
<currentEnv>Env</currentEnv>
...</thread>
<ffi>... Id |-> "core.div" ...</ffi>
<env>
<envId>Env</envId>
<envContent>0 |-> val(X:Int) 1 |-> val(Y:Int)</envContent>
</env>
// "core.eq"
rule <thread>...
<k>#ffiReady Id</k>
<result>.:Val => val(X ==K Y) </result>
<currentEnv>Env</currentEnv>
...</thread>
<ffi>... Id |-> "core.eq" ...</ffi>
<env>
<envId>Env</envId>
<envContent>0 |-> val(X) 1 |-> val(Y)</envContent>
</env>
// "core.not-eq"
rule <thread>...
<k>#ffiReady Id</k>
<result>.:Val => val(X =/=K Y) </result>
<currentEnv>Env</currentEnv>
...</thread>
<ffi>... Id |-> "core.not-eq" ...</ffi>
<env>
<envId>Env</envId>
<envContent>0 |-> val(X) 1 |-> val(Y)</envContent>
</env>
// "core.gt"
rule <thread>...
<k>#ffiReady Id</k>
<result>.:Val => val(X >Int Y) </result>
<currentEnv>Env</currentEnv>
...</thread>
<ffi>... Id |-> "core.gt" ...</ffi>
<env>
<envId>Env</envId>
<envContent>0 |-> val(X:Int) 1 |-> val(Y:Int)</envContent>
</env>
// "core.gte"
rule <thread>...
<k>#ffiReady Id</k>
<result>.:Val => val(X >=Int Y) </result>
<currentEnv>Env</currentEnv>
...</thread>
<ffi>... Id |-> "core.gte" ...</ffi>
<env>
<envId>Env</envId>
<envContent>0 |-> val(X:Int) 1 |-> val(Y:Int)</envContent>
</env>
// "core.lt"
rule <thread>...
<k>#ffiReady Id</k>
<result>.:Val => val(X <Int Y) </result>
<currentEnv>Env</currentEnv>
...</thread>
<ffi>... Id |-> "core.lt" ...</ffi>
<env>
<envId>Env</envId>
<envContent>0 |-> val(X:Int) 1 |-> val(Y:Int)</envContent>
</env>
// "core.lte"
rule <thread>...
<k>#ffiReady Id</k>
<result>.:Val => val(X <=Int Y) </result>
<currentEnv>Env</currentEnv>
...</thread>
<ffi>... Id |-> "core.lte" ...</ffi>
<env>
<envId>Env</envId>
<envContent>0 |-> val(X:Int) 1 |-> val(Y:Int)</envContent>
</env>
// "core.and"
rule <thread>...
<k>#ffiReady Id</k>
<result>.:Val => val(X andBool Y) </result>
<currentEnv>Env</currentEnv>
...</thread>
<ffi>... Id |-> "core.and" ...</ffi>
<env>
<envId>Env</envId>
<envContent>0 |-> val(X:Bool) 1 |-> val(Y:Bool)</envContent>
</env>
// "core.or"
rule <thread>...
<k>#ffiReady Id</k>
<result>.:Val => val(X orBool Y) </result>
<currentEnv>Env</currentEnv>
...</thread>
<ffi>... Id |-> "core.or" ...</ffi>
<env>
<envId>Env</envId>
<envContent>0 |-> val(X:Bool) 1 |-> val(Y:Bool)</envContent>
</env>
// "core.not"
rule <thread>...
<k>#ffiReady Id</k>
<result>.:Val => val(notBool X) </result>
<currentEnv>Env</currentEnv>
...</thread>
<ffi>... Id |-> "core.not" ...</ffi>
<env>
<envId>Env</envId>
<envContent>0 |-> val(X:Bool)</envContent>
</env>
// "core.ift"
rule <thread>...
<k>#ffiReady Id</k>
<result>.:Val => val(signal) </result>
<currentEnv>Env</currentEnv>
...</thread>
<ffi>... Id |-> "core.ift" ...</ffi>
<env>
<envId>Env</envId>
<envContent>0 |-> val(true)</envContent>
</env>
rule <thread>...
<k>#ffiReady Id => #stop</k>
<currentEnv>Env</currentEnv>
...</thread>
<ffi>... Id |-> "core.ift" ...</ffi>
<env>
<envId>Env</envId>
<envContent>0 |-> val(false)</envContent>
</env>
// "core.iff"
rule <thread>...
<k>#ffiReady Id</k>
<result>.:Val => val(signal) </result>
<currentEnv>Env</currentEnv>
...</thread>
<ffi>... Id |-> "core.iff" ...</ffi>
<env>
<envId>Env</envId>
<envContent>0 |-> val(false)</envContent>
</env>
rule <thread>...
<k>#ffiReady Id => #stop</k>
<currentEnv>Env</currentEnv>
...</thread>
<ffi>... Id |-> "core.iff" ...</ffi>
<env>
<envId>Env</envId>
<envContent>0 |-> val(true)</envContent>
</env>
// "core.make-record"
syntax RealVal ::= #makeRecord(Map, Int, Map) [function]
rule #makeRecord(Res, _, .Map) => Res
rule #makeRecord(Res => Res[Env[I] <- Env[I +Int 1]], I => I +Int 2, Env => removeAll(Env, SetItem(I) SetItem(I +Int 1)))
requires Env =/=K .Map
rule <thread>...
<k>#ffiReady Id</k>
<result>.:Val => val(#makeRecord(.Map, 0, Content)) </result>
<currentEnv>Env</currentEnv>
...</thread>
<ffi>... Id |-> "core.make-record" ...</ffi>
<env>
<envId>Env</envId>
<envContent>Content</envContent>
</env>
// coeffects
rule <thread>...
<k>#coeffect Param => #tickWait (Tick +Int Timeout)</k>
<result>.:Val </result>
<currentEnv>Env</currentEnv>
...</thread>
<tick>Tick</tick>
<env>
<envId>Env</envId>
<envContent>... Param |-> val(val("kind") |-> val("rwait") val("timeout") |-> val(Timeout) _) ...</envContent>
</env>
rule <thread>...
<k>#tickWait Tick</k>
<result>.:Val => val(signal)</result>
...</thread>
<tick>Tick</tick>
rule <thread>...
<k>#tickWait Tick</k>
...</thread>
<tick>CurrentTick => CurrentTick +Int 1</tick>
requires Tick =/=Int CurrentTick
endmodule
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment