Define Python Prelude in Laurel instead of Core

Examples/StringTest.laurel.st

@@ -3,7 +3,7 @@ returns (result: string)
 requires true
 {
   var message: string := "Hello, World!";
-  return message;
+  return message
 };
 
 procedure testStringConcat()
@@ -12,5 +12,5 @@ requires true
 {
   var hello: string := "Hello";
   var world: string := "World";
-  return hello;
+  return hello
 };

Strata/DDM/AST.lean

@@ -190,6 +190,7 @@ inductive SepFormat where
 | space          -- Space separator (SpaceSepBy)
 | spacePrefix    -- Space before each element (SpacePrefixSepBy)
 | newline        -- Newline separator (NewlineSepBy)
+| semicolon      -- Semicolon separator (SemicolonSepBy)
 deriving Inhabited, Repr, BEq
 
 namespace SepFormat
@@ -200,13 +201,15 @@ def toString : SepFormat → String
   | .space => "spaceSepBy"
   | .spacePrefix => "spacePrefixSepBy"
   | .newline => "newlineSepBy"
+  | .semicolon => "semicolonSepBy"
 
 def fromCategoryName? : QualifiedIdent → Option SepFormat
   | q`Init.Seq => some .none
   | q`Init.CommaSepBy => some .comma
   | q`Init.SpaceSepBy => some .space
   | q`Init.SpacePrefixSepBy => some .spacePrefix
   | q`Init.NewlineSepBy => some .newline
+  | q`Init.SemicolonSepBy => some .semicolon
   | _ => none
 
 instance : ToString SepFormat where

Strata/DDM/BuiltinDialects/Init.lean

@@ -21,6 +21,7 @@ def SyntaxCat.mkCommaSepBy (c:SyntaxCat) : SyntaxCat := { ann := .none, name :=
 def SyntaxCat.mkSpaceSepBy (c:SyntaxCat) : SyntaxCat := { ann := .none, name := q`Init.SpaceSepBy, args := #[c] }
 def SyntaxCat.mkSpacePrefixSepBy (c:SyntaxCat) : SyntaxCat := { ann := .none, name := q`Init.SpacePrefixSepBy, args := #[c] }
 def SyntaxCat.mkNewlineSepBy (c:SyntaxCat) : SyntaxCat := { ann := .none, name := q`Init.NewlineSepBy, args := #[c] }
+def SyntaxCat.mkSemicolonSepBy (c:SyntaxCat) : SyntaxCat := { ann := .none, name := q`Init.SemicolonSepBy, args := #[c] }
 
 def initDialect : Dialect := BuiltinM.create! "Init" #[] do
   let Ident : ArgDeclKind := .cat <| .atom .none q`Init.Ident
@@ -59,6 +60,8 @@ def initDialect : Dialect := BuiltinM.create! "Init" #[] do
 
   declareCat q`Init.NewlineSepBy #["a"]
 
+  declareCat q`Init.SemicolonSepBy #["a"]
+
   let QualifiedIdent := q`Init.QualifiedIdent
   declareCat QualifiedIdent
   declareOp {

Strata/DDM/Elab/Core.lean

@@ -1059,6 +1059,7 @@ private def scopeSepFormat (name : QualifiedIdent)
   match name with
   | q`Init.Seq              => some (.none, Syntax.getArgs)
   | q`Init.CommaSepBy       => some (.comma, Syntax.getSepArgs)
+  | q`Init.SemicolonSepBy   => some (.semicolon, Syntax.getSepArgs)
   | q`Init.SpaceSepBy       => some (.space, Syntax.getSepArgs)
   | q`Init.SpacePrefixSepBy => some (.spacePrefix, Syntax.getArgs)
   | _ => none
@@ -1540,6 +1541,8 @@ partial def catElaborator (c : SyntaxCat) : TypingContext → Syntax → ElabM T
     elabSeqWith c .none "seq" (·.getArgs)
   | q`Init.CommaSepBy =>
     elabSeqWith c .comma "commaSepBy" (·.getSepArgs)
+  | q`Init.SemicolonSepBy =>
+    elabSeqWith c .semicolon "semicolonSepBy" (·.getSepArgs)
   | q`Init.SpaceSepBy =>
     elabSeqWith c .space "spaceSepBy" (·.getArgs)
   | q`Init.SpacePrefixSepBy =>

Strata/DDM/Format.lean

@@ -423,6 +423,13 @@ private partial def ArgF.mformatM {α} : ArgF α → FormatM PrecFormat
       let f i q s := return s ++ "\n" ++ (← entries[i].mformatM).format
       let a := (← entries[0].mformatM).format
       .atom <$> entries.size.foldlM f (start := 1) a
+  | .semicolon =>
+    if z : entries.size = 0 then
+      pure (.atom .nil)
+    else do
+      let f i q s := return s ++ "; " ++ (← entries[i].mformatM).format
+      let a := (← entries[0].mformatM).format
+      .atom <$> entries.size.foldlM f (start := 1) a
 
 private partial def ppArgs (f : StrataFormat) (rargs : Array Arg) : FormatM PrecFormat :=
   if rargs.isEmpty then

Strata/DDM/Integration/Java/Gen.lean

@@ -125,7 +125,7 @@ partial def syntaxCatToJavaType (cat : SyntaxCat) : JavaType :=
     match cat.args[0]? with
     | some inner => .optional (syntaxCatToJavaType inner)
     | none => panic! "Init.Option requires a type argument"
-  | q`Init.Seq | q`Init.CommaSepBy | q`Init.NewlineSepBy | q`Init.SpaceSepBy | q`Init.SpacePrefixSepBy =>
+  | q`Init.Seq | q`Init.CommaSepBy | q`Init.NewlineSepBy | q`Init.SpaceSepBy | q`Init.SpacePrefixSepBy | q`Init.SemicolonSepBy =>
     match cat.args[0]? with
     | some inner => .list (syntaxCatToJavaType inner)
     | none => panic! "List category requires a type argument"
@@ -146,7 +146,7 @@ partial def syntaxCatToQualifiedName (cat : SyntaxCat) : Option QualifiedIdent :
   else if abstractCategories.contains cat.name then some cat.name
   else match cat.name with
   | q`Init.Option | q`Init.Seq | q`Init.CommaSepBy
-  | q`Init.NewlineSepBy | q`Init.SpaceSepBy | q`Init.SpacePrefixSepBy =>
+  | q`Init.NewlineSepBy | q`Init.SpaceSepBy | q`Init.SpacePrefixSepBy | q`Init.SemicolonSepBy =>
     cat.args[0]?.bind syntaxCatToQualifiedName
   | ⟨"Init", _⟩ => none
   | qid => some qid

Strata/DDM/Integration/Lean/Gen.lean

@@ -706,6 +706,9 @@ partial def genCatTypeTerm (annType : Ident) (c : SyntaxCat)
   | q`Init.NewlineSepBy, 1 =>
     let inner := mkCApp ``Array #[args[0]]
     return if addAnn then mkCApp ``Ann #[inner, annType] else inner
+  | q`Init.SemicolonSepBy, 1 =>
+    let inner := mkCApp ``Array #[args[0]]
+    return if addAnn then mkCApp ``Ann #[inner, annType] else inner
   | q`Init.Option, 1 =>
     let inner := mkCApp ``Option #[args[0]]
     return if addAnn then mkCApp ``Ann #[inner, annType] else inner
@@ -909,6 +912,8 @@ partial def toAstApplyArg (vn : Name) (cat : SyntaxCat)
     ``($toAst $v)
   | q`Init.CommaSepBy => do
     toAstApplyArgSeq v cat ``SepFormat.comma
+  | q`Init.SemicolonSepBy => do
+    toAstApplyArgSeq v cat ``SepFormat.semicolon
   | q`Init.SpaceSepBy => do
     toAstApplyArgSeq v cat ``SepFormat.space
   | q`Init.SpacePrefixSepBy => do
@@ -1171,6 +1176,8 @@ partial def genOfAstArgTerm (varName : String) (cat : SyntaxCat)
     pure <| mkApp ofAst #[e]
   | q`Init.CommaSepBy => do
     genOfAstSeqArgTerm varName cat e ``SepFormat.comma
+  | q`Init.SemicolonSepBy => do
+    genOfAstSeqArgTerm varName cat e ``SepFormat.semicolon
   | q`Init.SpaceSepBy => do
     genOfAstSeqArgTerm varName cat e ``SepFormat.space
   | q`Init.SpacePrefixSepBy => do
@@ -1463,7 +1470,7 @@ Generates an `Inhabited` instance for a category if possible, and adds it to the
 
 This function attempts to find a constructor whose arguments are all inhabited types.
 A type is considered inhabited if:
-- It's a sequence type (`Init.Seq`, `Init.CommaSepBy`, `Init.SpaceSepBy`, `Init.SpacePrefixSepBy`)
+- It's a sequence type (`Init.Seq`, `Init.CommaSepBy`, `Init.SpaceSepBy`, `Init.SpacePrefixSepBy`, `Init.SemicolonSepBy`)
   which are always inhabited via empty arrays
 - It's an `Init.Option` type which is always inhabited via `none`
 - It's already in the `InhabitedSet` from previous processing
@@ -1490,6 +1497,7 @@ def tryMakeInhabited (cat : QualifiedIdent) (ops : Array DefaultCtor)
         match arg.cat.name with
         | q`Init.Seq => true
         | q`Init.CommaSepBy => true
+        | q`Init.SemicolonSepBy => true
         | q`Init.SpaceSepBy => true
         | q`Init.SpacePrefixSepBy => true
         | q`Init.NewlineSepBy => true

Strata/DDM/Integration/Lean/ToExpr.lean

@@ -41,6 +41,7 @@ instance : ToExpr SepFormat where
     | .space => mkConst ``SepFormat.space
     | .spacePrefix => mkConst ``SepFormat.spacePrefix
     | .newline => mkConst ``SepFormat.newline
+    | .semicolon => mkConst ``SepFormat.semicolon
 
 end SepFormat
 

Strata/DDM/Ion.lean

@@ -90,13 +90,15 @@ def toIonName : SepFormat → String
   | .space => "spaceSepList"
   | .spacePrefix => "spacePrefixedList"
   | .newline => "newlineSepList"
+  | .semicolon => "semicolonSepList"
 
 def fromIonName? : String → Option SepFormat
   | "seq" => some .none
   | "commaSepList" => some .comma
   | "spaceSepList" => some .space
   | "spacePrefixedList" => some .spacePrefix
   | "newlineSepList" => some .newline
+  | "semicolonSepList" => some .semicolon
   | _ => none
 
 theorem fromIonName_toIonName_roundtrip (sep : SepFormat) :
@@ -573,6 +575,7 @@ private protected def ArgF.toIon {α} [ToIon α]
           | .space       => ionSymbol! "spaceSepList"
           | .spacePrefix => ionSymbol! "spacePrefixedList"
           | .newline     => ionSymbol! "newlineSepList"
+          | .semicolon   => ionSymbol! "semicolonSepList"
         let args : Array (Ion _) := #[ symb, annIon ]
         let args ← l.attach.mapM_off (init := args)
           fun ⟨v, _⟩ => ArgF.toIon refs (.inl v)

Strata/DDM/Parser.lean

@@ -774,6 +774,7 @@ def checkLeftRec (thisCatName : QualifiedIdent) (argDecls : ArgDecls) (as : List
                           cat.name == q`Init.SpaceSepBy ||
                           cat.name == q`Init.SpacePrefixSepBy ||
                           cat.name == q`Init.Seq ||
+                          cat.name == q`Init.SemicolonSepBy ||
                           cat.name == q`Init.Option
     if isListCategory then
       assert! cat.args.size = 1
@@ -893,13 +894,24 @@ private def commaSepByParserHelper (nonempty : Bool) (p : Parser) : Parser :=
   else
     sepByParser p (symbolNoAntiquot ",")
 
+/-- Helper to choose between sepByParser and sepBy1Parser for semicolon-separated lists -/
+private def semicolonSepByParserHelper (nonempty : Bool) (p : Parser) : Parser :=
+  if nonempty then
+    sepBy1Parser p (symbolNoAntiquot ";")
+  else
+    sepByParser p (symbolNoAntiquot ";")
+
 /-- Parser function for given syntax category -/
 partial def catParser (ctx : ParsingContext) (cat : SyntaxCat) (metadata : Metadata := {}) : Except SyntaxCat Parser :=
   match cat.name with
   | q`Init.CommaSepBy =>
     assert! cat.args.size = 1
     let isNonempty := q`StrataDDL.nonempty ∈ metadata
     commaSepByParserHelper isNonempty <$> catParser ctx cat.args[0]!
+  | q`Init.SemicolonSepBy =>
+    assert! cat.args.size = 1
+    let isNonempty := q`StrataDDL.nonempty ∈ metadata
+    semicolonSepByParserHelper isNonempty <$> catParser ctx cat.args[0]!
   | q`Init.SpaceSepBy | q`Init.SpacePrefixSepBy | q`Init.NewlineSepBy | q`Init.Seq =>
     assert! cat.args.size = 1
     let isNonempty := q`StrataDDL.nonempty ∈ metadata

Strata/Languages/Laurel/CoreDefinitionsForLaurel.lean

@@ -38,8 +38,7 @@ function const(value: int) : int
 The core map operation definitions as a `Laurel.Program`, parsed at compile time.
 -/
 def coreDefinitionsForLaurel : Program :=
-  let uri := Strata.Uri.file "Strata/Languages/Laurel/CoreDefinitionsForLaurel.lean"
-  match TransM.run uri (parseProgram coreDefinitionsForLaurelDDM) with
+  match TransM.run none (parseProgram coreDefinitionsForLaurelDDM) with
   | .ok program => program
   | .error e => panic! s!"CoreDefinitionsForLaurel parse error: {e}"
 

Strata/Languages/Laurel/EliminateReturnsInExpression.lean

@@ -79,7 +79,6 @@ def lastStmtToExpr (stmt : StmtExprMd) : StmtExprMd :=
       have := List.mem_of_getLast? h_last
       let lastExpr := lastStmtToExpr last
       let dropped := stmts.dropLast
-      -- have := List.dropLast_subset stmts
       have h : sizeOf stmts.dropLast < sizeOf stmts :=
         List.sizeOf_dropLast_lt (by intro h; simp [h] at h_last)
       stmtsToExpr dropped lastExpr md