Single Body Instances

kmir/pyproject.toml

@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kmir"
-version = "0.3.103"
+version = "0.3.104"
 description = ""
 authors = [
     "Runtime Verification, Inc. <contact@runtimeverification.com>",

kmir/src/kmir/__init__.py

@@ -1,3 +1,3 @@
 from typing import Final
 
-VERSION: Final = '0.3.103'
+VERSION: Final = '0.3.104'

kmir/src/kmir/kdist/mir-semantics/body.md

@@ -5,7 +5,7 @@ requires "ty.md"
 module BODY-SORTS
 
 syntax Body
-syntax Bodies
+syntax MaybeBody
 syntax DefId
 syntax MaybeInt
 syntax MIRBool
@@ -355,10 +355,10 @@ syntax VarDebugInfo ::= varDebugInfo(name: Symbol, sourceInfo: SourceInfo, compo
 syntax VarDebugInfos ::= List {VarDebugInfo, ""}
                          [group(mir-list), symbol(VarDebugInfos::append), terminator-symbol(VarDebugInfos::empty)]
 
+syntax MaybeBody ::= someBody(Body) [group(mir-option)]
+                    | "noBody"      [group(mir-option)]
 syntax Body ::= body(blocks: BasicBlocks, locals: LocalDecls, argCount: MIRInt, varDebugInfo: VarDebugInfos, spreadArg: MaybeLocal, span: Span)
                 [group(mir---blocks--locals--arg-count--var-debug-info--spread-arg--span)]
-syntax Bodies ::= List {Body, ""}
-                  [group(mir-list), symbol(Bodies::append), terminator-symbol(Bodies::empty)]
 
 endmodule
 ```

kmir/src/kmir/kdist/mir-semantics/kmir.md

@@ -219,7 +219,7 @@ be known to populate the `currentFunc` field.
   rule <k> #execFunction(
               monoItem(
                 SYMNAME,
-                monoItemFn(_, _, body((FIRST:BasicBlock _) #as BLOCKS,LOCALS, _, _, _, _) .Bodies)
+                monoItemFn(_, _, someBody(body((FIRST:BasicBlock _) #as BLOCKS,LOCALS, _, _, _, _)))
               ),
               FUNCTIONNAMES
             )
@@ -450,11 +450,10 @@ NB that a stack height of `0` cannot occur here, because the compiler prevents l
   rule #getBlocks(FUNCS, ID) => #getBlocksAux({FUNCS[ID]}:>MonoItemKind)
     requires ID in_keys(FUNCS)
 
-  // returns blocks from the _first_ body if there are several
-  // TODO handle cases with several blocks
-  rule #getBlocksAux(monoItemFn(_, _, .Bodies)) => .List
-  rule #getBlocksAux(monoItemFn(_, _, body(BLOCKS, _, _, _, _, _) _)) => toKList(BLOCKS)
-  // other item kinds are not expected or supported
+  // returns blocks from the body
+  rule #getBlocksAux(monoItemFn(_, _, noBody)) => .List
+  rule #getBlocksAux(monoItemFn(_, _, someBody(body(BLOCKS, _, _, _, _, _)))) => toKList(BLOCKS)
+  // other item kinds are not expected or supported FIXME: Just getting stuck for now
   rule #getBlocksAux(monoItemStatic(_, _, _)) => .List // should not occur in calls at all
   rule #getBlocksAux(monoItemGlobalAsm(_)) => .List // not supported. FIXME Should error, maybe during #init
 ```
@@ -533,7 +532,7 @@ An operand may be a `Reference` (the only way a function could access another fu
 
   // reserve space for local variables and copy/move arguments from old locals into their place
   rule <k> #setUpCalleeData(
-              monoItemFn(_, _, body((FIRST:BasicBlock _) #as BLOCKS, NEWLOCALS, _, _, _, _) _:Bodies),
+              monoItemFn(_, _, someBody(body((FIRST:BasicBlock _) #as BLOCKS, NEWLOCALS, _, _, _, _))),
               ARGS
               )
          =>
@@ -551,6 +550,7 @@ An operand may be a `Reference` (the only way a function could access another fu
          // assumption: arguments stored as _1 .. _n before actual "local" data
          ...
        </currentFrame>
+  // TODO: Haven't handled "noBody" case
 
   syntax KItem ::= #setArgsFromStack ( Int, Operands)
                  | #setArgFromStack ( Int, Operand)

kmir/src/kmir/kdist/mir-semantics/mono.md

@@ -22,7 +22,7 @@ syntax StaticDef ::= staticDef(Int) [group(mir-int)] // imported from crate
 syntax MaybeAllocation ::= someAllocation(Allocation) [group(mir-option)]
                          | "noAllocation"             [group(mir-option)]
 
-syntax MonoItemKind ::= monoItemFn(name: Symbol, id: DefId, body: Bodies)
+syntax MonoItemKind ::= monoItemFn(name: Symbol, id: DefId, body: MaybeBody)
                           [ group(mir-enum---name--id--body)
                           , symbol(MonoItemKind::MonoItemFn)
                           ]

kmir/src/kmir/parse/notes.md

@@ -36,7 +36,7 @@ json: an array of integer values between 0 and 255
 syntax Elems ::= List {Elem, ""} [group(mir-list), ...]
 ```
 json: a homogeneous list, e.g. `[e1, e2, e3, ...]`, where all elements correspond to syntactic productions for the sort `Elem`.
-As per naming convention, the list sort `Elems` (plural) should contain elements of sort `Elem` (singular). Usual plural formation rules (`Body -> Bodies`, `Branch -> Branches`) are respected.
+As per naming convention, the list sort `Elems` (plural) should contain elements of sort `Elem` (singular). Usual plural formation rules (`Branch -> Branches`) are respected.
 
 #### mir-klist-ElementSort
 ```

kmir/src/kmir/parse/parser.py

@@ -113,7 +113,7 @@ def _list_symbols(sort: str) -> tuple[str, str]:
 # Given a list Sort, return the element sort.
 def _element_sort(sort: KSort) -> KSort:
     name = sort.name
-    if name.endswith('ies'):  # Bodies, Entries, ...
+    if name.endswith('ies'):  # Entries, ...
         return KSort(name[:-3] + 'y')
     elif (  # -es for words ending in 's', 'ch', 'sh', 'ss', 'x' or 'z'
         name.endswith('ses')