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
              | "#coeffect" Int
              | "#stop"
              | "#constInt" Int
              | "#closure" Int Int
              | "#label" Int

  syntax Val ::= Int

  syntax SourceOp ::= Int ":" Op
  syntax SourceOps ::= List{SourceOp, " "}

  syntax SourceFun ::= Int Int "{" SourceOps "}"
  syntax SourceFuns ::= List{SourceFun, " "}

endmodule

module OAM
  imports OAM-SYNTAX

  syntax Env ::= env(Map)
  syntax Stack ::= stack(List)

  syntax PendValue ::= pendVal(Val)
                     | "pendStopped"
                     | "pend"

  syntax Pending ::= pending(PendValue, List)

  syntax Frame ::= fPruning(Int, Pending)
                 | fOtherwise(Bool, Int, Int, Int)
                 | fSequential(Int, Int, Int)

  syntax Val ::= closure(Int, Int, Env)

  syntax OrcToken ::= OrcToken(Int, Int, Env, Stack)

  syntax KResult ::= Val

  configuration <T>
    <threads>
      <thread multiplicity="*">
        <currentFun>0</currentFun>
        <pc>-1</pc>
        <k>.:Op</k>
        <result>.:Val</result>
        <stack>.List</stack>
      </thread>
    </threads>
    <queue>.List</queue>
    <values>.List</values>
    <instance>
      <currentCoeffect>0</currentCoeffect>
      <blocks>.List</blocks>
    </instance>
    <code>
     <fun multiplicity="*">
       <funId>0</funId>
       <initOp>0</initOp>
       <ops>
         <op multiplicity="*">
           <opId>0</opId>
           <body>#stop</body>           
         </op>         
       </ops>
       <funSource>.SourceOps</funSource>
     </fun>
    </code>
    <source>$PGM:SourceFuns</source>
  </T>

  rule <source> (Id InitOp { Ops:SourceOps }) XS:SourceFuns => XS</source>
       <code>
       ... (.Bag =>
                 <fun>
                   <funId>Id</funId>
                   <initOp>InitOp</initOp>
                   <ops>.Bag</ops>
                   <funSource> Ops </funSource>
                 </fun>)
       ...</code>

  rule <fun>
         ...
         <ops>...
           (.Bag =>
             <op>
               <opId>Id</opId>
               <body>Body</body>
             </op>)
         ...</ops>
         <funSource> (Id : Body) XS => XS </funSource>
       </fun>

  // Main thread
  rule <threads>
    .Bag => <thread>
        <currentFun>0</currentFun>
        <pc>-1</pc>
        <k>.:Op</k>
        <result>.:Val</result>
        <stack>.List</stack>
      </thread>
    </threads>
  // Init op
  rule <currentFun>FunId:Int</currentFun>
       <pc>-1 => OpId</pc>
       <funId>FunId</funId>
       <initOp>OpId</initOp>

  // Place actual op
  rule <thread>...
         <pc>OpId</pc>
         <currentFun>FunId</currentFun>
         <k>. => Body</k>
       ...</thread>
       <fun>...
         <funId>FunId</funId>
         <ops>...
           <op>
             <opId>OpId</opId>
             <body>Body</body>
           </op>
         ...</ops>
       ...</fun>
  requires OpId =/=Int -1
endmodule