From 90774ba2b29cb4ab27efcc43135a8aff0ae9f065 Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Wed, 18 Mar 2026 16:46:44 -0700 Subject: [PATCH 1/6] fix type checking bugs --- .../Laurel/HeapParameterization.lean | 8 +++- Strata/Languages/Python/PythonToLaurel.lean | 46 +++++++++++++++---- 2 files changed, 43 insertions(+), 11 deletions(-) diff --git a/Strata/Languages/Laurel/HeapParameterization.lean b/Strata/Languages/Laurel/HeapParameterization.lean index 225668872..9f10f769b 100644 --- a/Strata/Languages/Laurel/HeapParameterization.lean +++ b/Strata/Languages/Laurel/HeapParameterization.lean @@ -178,7 +178,8 @@ def boxDestructorName (model : SemanticModel) (ty : HighType) : Identifier := | .UserDefined name => if isDatatype model name then s!"Box..{name.text}Val!" else "Box..compositeVal!" - | _ => dbg_trace "BUG, boxDestructorName bad type "; "boxDestructorNameError" + | .TCore name => s!"Box..{name}Val" + | _ => dbg_trace f!"BUG, boxDestructorName bad type {ty}"; "boxDestructorNameError" /-- Get the Box constructor name for a given Laurel HighType. For UserDefined datatypes, uses "Box.."; @@ -192,6 +193,7 @@ def boxConstructorName (model : SemanticModel) (ty : HighType) : Identifier := | .UserDefined name => if isDatatype model name then s!"Box..{name.text}" else "BoxComposite" + | .TCore name => s!"Box..{name}" | _ => dbg_trace "BUG, boxConstructorName bad type"; "boxConstructorNameError" /-- Build the DatatypeConstructor for a Box variant from a HighType, for datatype generation -/ @@ -206,6 +208,8 @@ private def boxConstructorDef (model : SemanticModel) (ty : HighType) : Option D some { name := s!"Box..{name.text}", args := [{ name := s!"{name.text}Val", type := ⟨.UserDefined name, #[]⟩ }] } else some { name := "BoxComposite", args := [{ name := "compositeVal", type := ⟨.UserDefined "Composite", #[]⟩ }] } + | .TCore name => + some { name := s!"Box..{name}", args := [{ name := s!"{name}Val", type := ⟨.TCore name, #[]⟩ }] } | _ => dbg_trace "BUG, boxConstructorDef bad type"; none /-- Record a Box constructor use in the transform state -/ @@ -267,7 +271,7 @@ where if calleeWritesHeap then if valueUsed then let freshVar ← freshVarName - let varDecl := mkMd (.LocalVariable freshVar ⟨.TInt, #[]⟩ none) + let varDecl := mkMd (.LocalVariable freshVar (computeExprType model exprMd) none) let callWithHeap := ⟨ .Assign [mkMd (.Identifier heapVar), mkMd (.Identifier freshVar)] (⟨ .StaticCall callee (mkMd (.Identifier heapVar) :: args'), md ⟩), md ⟩ diff --git a/Strata/Languages/Python/PythonToLaurel.lean b/Strata/Languages/Python/PythonToLaurel.lean index df0572e01..546aa391b 100644 --- a/Strata/Languages/Python/PythonToLaurel.lean +++ b/Strata/Languages/Python/PythonToLaurel.lean @@ -759,10 +759,11 @@ partial def translateCall (ctx : TranslationContext) else [trans_kwords] match f with | .Name _ _ _ => return mkStmtExprMd (StmtExpr.StaticCall funcName (trans_args ++ trans_kwords_exprs)) - | .Attribute _ val attr _ => - let target_trans ← translateExpr ctx val + | .Attribute _ val _attr _ => + let _target_trans ← translateExpr ctx val if opt_firstarg.isSome then - return mkStmtExprMd (StmtExpr.InstanceCall target_trans attr.val (trans_args ++ trans_kwords_exprs)) + return mkStmtExprMd (.Hole) + --return mkStmtExprMd (StmtExpr.InstanceCall target_trans attr.val (trans_args ++ trans_kwords_exprs)) else return mkStmtExprMd (StmtExpr.StaticCall funcName (trans_args ++ trans_kwords_exprs)) | _ => throw (.unsupportedConstruct "Invalid call construct" (toString (repr f))) @@ -908,7 +909,8 @@ partial def translateStmt (ctx : TranslationContext) (s : Python.stmt SourceRang | .Hole => -- Hoist Hole to fresh variable let freshVar := s!"cond_{test.toAst.ann.start.byteIdx}" - let varType := mkHighTypeMd .TBool -- Conditions are bools + --let varType := mkHighTypeMd .TBool -- Conditions are bools + let varType := AnyTy let varDecl := mkStmtExprMd (StmtExpr.LocalVariable freshVar varType (some condExpr)) let varRef := mkStmtExprMd (StmtExpr.Identifier freshVar) ([varDecl], varRef, { ctx with variableTypes := ctx.variableTypes ++ [(freshVar, "Bool")] }) @@ -994,6 +996,9 @@ partial def translateStmt (ctx : TranslationContext) (s : Python.stmt SourceRang return (condCtx, [result]) + --Ignore comments in source code + | .Expr _ (.Constant _ (.ConString _ _) _) => return (ctx, []) + -- Expression statement (e.g., function call) | .Expr _ value => do let expr ← translateExpr ctx value @@ -1019,9 +1024,19 @@ partial def translateStmt (ctx : TranslationContext) (s : Python.stmt SourceRang let tryLabel := "try_end" let handlerLabel := "exception_handlers" + let errorVars: List String := ((handlers.val.toList.filterMap (λ h => match h with + | .ExceptHandler _ _ errname _ => errname.val)).map (λ h => h.val)).dedup.filter + (λ e => e ∉ ctx.variableTypes.unzip.fst) + let errorTy := mkHighTypeMd (.UserDefined {text:= "PythonError"}) + let errorVarDecls := errorVars.map (λ e => mkStmtExprMd (.LocalVariable {text:=e} errorTy none)) + let ctx := {ctx with variableTypes:= ctx.variableTypes ++ errorVars.map (λ e => (e, "PythonError"))} + -- Translate try body let (bodyCtx, bodyStmts) ← translateStmtList ctx body.val.toList + let varDecls := bodyStmts.filter (λ stmt => match stmt.val with |.LocalVariable .. => true | _ => false) + let bodyStmts := bodyStmts.filter (λ stmt => match stmt.val with |.LocalVariable .. => false | _ => true) + -- Insert exception checks after each statement in try body let bodyStmtsWithChecks := bodyStmts.flatMap fun stmt => -- Check if maybe_except is an exception and exit to handlers if so @@ -1039,12 +1054,15 @@ partial def translateStmt (ctx : TranslationContext) (s : Python.stmt SourceRang let (_, hStmts) ← translateStmtList bodyCtx handlerBody.val.toList handlerStmts := handlerStmts ++ hStmts + let handlersVarDecls := handlerStmts.filter (λ stmt => match stmt.val with |.LocalVariable .. => true | _ => false) + handlerStmts := handlerStmts.filter (λ stmt => match stmt.val with |.LocalVariable .. => false | _ => true) -- Create handler block let handlerBlock := mkStmtExprMd (StmtExpr.Block handlerStmts (some handlerLabel)) + let varDecls:= varDecls ++ errorVarDecls ++ handlersVarDecls -- Wrap in try block let tryBlock := mkStmtExprMdWithLoc (StmtExpr.Block (bodyStmtsWithChecks ++ [handlerBlock]) (some tryLabel)) md - return (bodyCtx, [tryBlock]) + return (bodyCtx, varDecls ++ [tryBlock]) | .Raise _ _ _ => return (ctx, [mkStmtExprMd .Hole]) @@ -1068,9 +1086,12 @@ partial def translateStmt (ctx : TranslationContext) (s : Python.stmt SourceRang match optVars.val with | some varExpr => let varName := pyExprToString varExpr - let varDecl := mkStmtExprMd (StmtExpr.LocalVariable varName AnyTy (some enterCall)) - currentCtx := {currentCtx with variableTypes := currentCtx.variableTypes ++ [(varName, PyLauType.Any)]} - setupStmts := setupStmts ++ [mgrDecl, varDecl] + if varName ∈ currentCtx.variableTypes.unzip.fst then + setupStmts := setupStmts ++ [mgrDecl] + else + let varDecl := mkStmtExprMd (StmtExpr.LocalVariable varName AnyTy (some enterCall)) + currentCtx := {currentCtx with variableTypes := currentCtx.variableTypes ++ [(varName, PyLauType.Any)]} + setupStmts := setupStmts ++ [mgrDecl, varDecl] | none => setupStmts := setupStmts ++ [mgrDecl, enterCall] cleanupStmts := cleanupStmts ++ [mkStmtExprMd (StmtExpr.InstanceCall mgrRef "__exit__" [])] @@ -1564,8 +1585,15 @@ def pythonToLaurel' (info : PreludeInfo) | _ => none | _ => [] + let pyErrorTy : CompositeType := { + name := {text := "PythonError"} + extending := [] -- No inheritance support for now + fields := [{name:= "response", isMutable:= false, type:= AnyTy}] + instanceProcedures := [] + } + -- FIRST PASS: Collect all class definitions and field type info - let mut compositeTypes : List CompositeType := [] + let mut compositeTypes : List CompositeType := [pyErrorTy] let mut compositeTypeNames := info.compositeTypes let mut classFieldHighType : Std.HashMap String (Std.HashMap String HighType) := {} for stmt in body.val do From 77318d1f8b70862d42576f145e1007cd84049a4e Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Thu, 19 Mar 2026 09:19:21 -0700 Subject: [PATCH 2/6] merge conflict + remove .Hole processing in if, while, assert condition --- Strata/Languages/Python/PythonToLaurel.lean | 103 +++----------------- 1 file changed, 15 insertions(+), 88 deletions(-) diff --git a/Strata/Languages/Python/PythonToLaurel.lean b/Strata/Languages/Python/PythonToLaurel.lean index 50e39f637..4501fe230 100644 --- a/Strata/Languages/Python/PythonToLaurel.lean +++ b/Strata/Languages/Python/PythonToLaurel.lean @@ -913,21 +913,7 @@ partial def translateStmt (ctx : TranslationContext) (s : Python.stmt SourceRang -- If statement | .If _ test body orelse => do let condExpr ← translateExpr ctx test - -- Check if condition contains a Hole - if so, hoist to variable to avoid free variable errors - let (condStmts, finalCondExpr, condCtx) := - match condExpr.val with - | .Hole => - -- Hoist Hole to fresh variable - let freshVar := s!"cond_{test.toAst.ann.start.byteIdx}" - --let varType := mkHighTypeMd .TBool -- Conditions are bools - let varType := AnyTy - let varDecl := mkStmtExprMd (StmtExpr.LocalVariable freshVar varType (some condExpr)) - let varRef := mkStmtExprMd (StmtExpr.Identifier freshVar) - ([varDecl], varRef, { ctx with variableTypes := ctx.variableTypes ++ [(freshVar, "Bool")] }) - | _ => ([], condExpr, ctx) - - -- Translate body (list of statements) - let (bodyCtx, bodyStmts) ← translateStmtList condCtx body.val.toList + let (bodyCtx, bodyStmts) ← translateStmtList ctx body.val.toList let bodyBlock := mkStmtExprMd (StmtExpr.Block bodyStmts none) -- Translate else branch if present let elseBlock ← if orelse.val.isEmpty then @@ -935,46 +921,22 @@ partial def translateStmt (ctx : TranslationContext) (s : Python.stmt SourceRang else do let (_, elseStmts) ← translateStmtList bodyCtx orelse.val.toList .ok (some (mkStmtExprMd (StmtExpr.Block elseStmts none))) - let ifStmt := mkStmtExprMdWithLoc (StmtExpr.IfThenElse (Any_to_bool finalCondExpr) bodyBlock elseBlock) md - - -- Wrap in block if we hoisted condition - let result := if condStmts.isEmpty then - ifStmt - else - mkStmtExprMdWithLoc (StmtExpr.Block (condStmts ++ [ifStmt]) none) md + let ifStmt := mkStmtExprMdWithLoc (StmtExpr.IfThenElse (Any_to_bool condExpr) bodyBlock elseBlock) md - return (bodyCtx, [result]) + return (bodyCtx, [ifStmt]) -- While loop | .While _ test body _orelse => do -- Note: Python while-else not supported yet let condExpr ← translateExpr ctx test - -- Check if condition contains a Hole - if so, hoist to variable - let (condStmts, finalCondExpr, condCtx) := - match condExpr.val with - | .Hole => - let freshVar := s!"while_cond_{test.toAst.ann.start.byteIdx}" - let varType := mkHighTypeMd .TBool - let varDecl := mkStmtExprMd (StmtExpr.LocalVariable freshVar varType (some condExpr)) - let varRef := mkStmtExprMd (StmtExpr.Identifier freshVar) - ([varDecl], varRef, { ctx with variableTypes := ctx.variableTypes ++ [(freshVar, "bool")] }) - | _ => ([], condExpr, ctx) - let breakLabel := s!"loop_break_{test.toAst.ann.start.byteIdx}" let continueLabel := s!"loop_continue_{test.toAst.ann.start.byteIdx}" - let loopCtx := { condCtx with loopBreakLabel := some breakLabel, loopContinueLabel := some continueLabel } + let loopCtx := { ctx with loopBreakLabel := some breakLabel, loopContinueLabel := some continueLabel } let (_, bodyStmts) ← translateStmtList loopCtx body.val.toList let bodyBlock := mkStmtExprMd (StmtExpr.Block bodyStmts (some continueLabel)) - let whileStmt := mkStmtExprMd (StmtExpr.While (Any_to_bool finalCondExpr) [] none bodyBlock) + let whileStmt := mkStmtExprMd (StmtExpr.While (Any_to_bool condExpr) [] none bodyBlock) let whileWrapped := mkStmtExprMdWithLoc (StmtExpr.Block [whileStmt] (some breakLabel)) md - - -- Wrap in block if we hoisted condition - let result := if condStmts.isEmpty then - whileWrapped - else - mkStmtExprMdWithLoc (StmtExpr.Block (condStmts ++ [whileWrapped]) none) md - - return (loopCtx, [result]) + return (loopCtx, [whileWrapped]) -- Return statement | .Return _ value => do @@ -989,26 +951,8 @@ partial def translateStmt (ctx : TranslationContext) (s : Python.stmt SourceRang -- Assert statement | .Assert _ test _msg => do let condExpr ← translateExpr ctx test - -- Check if condition contains a Hole - if so, hoist to variable - let (condStmts, finalCondExpr, condCtx) := - match condExpr.val with - | .Hole => - let freshVar := s!"assert_cond_{test.toAst.ann.start.byteIdx}" - let varType := mkHighTypeMd .TBool - let varDecl := mkStmtExprMd (StmtExpr.LocalVariable freshVar varType (some condExpr)) - let varRef := mkStmtExprMd (StmtExpr.Identifier freshVar) - ([varDecl], varRef, { ctx with variableTypes := ctx.variableTypes ++ [(freshVar, "bool")] }) - | _ => ([], condExpr, ctx) - - let assertStmt := mkStmtExprMdWithLoc (StmtExpr.Assert (Any_to_bool finalCondExpr)) md - - -- Wrap in block if we hoisted condition - let result := if condStmts.isEmpty then - assertStmt - else - mkStmtExprMdWithLoc (StmtExpr.Block (condStmts ++ [assertStmt]) none) md - - return (condCtx, [result]) + let assertStmt := mkStmtExprMdWithLoc (StmtExpr.Assert (Any_to_bool condExpr)) md + return (ctx, [assertStmt]) --Ignore comments in source code | .Expr _ (.Constant _ (.ConString _ _) _) => return (ctx, []) @@ -1048,32 +992,27 @@ partial def translateStmt (ctx : TranslationContext) (s : Python.stmt SourceRang | .Assign _ targets _ _ => targets.val.toList.head?.map (fun t => (pyExprToString t, PyLauType.Any)) | _ => none let bodyDecls := collectDeclaredNamesAndTypes body.val.toList + + let errorVarDecls: List (String × String) := (handlers.val.toList.filterMap (λ h => match h with + | .ExceptHandler _ _ errname _ => errname.val)).map (λ h => (h.val, "PythonError")) + let handlerDecls := handlers.val.toList.flatMap fun h => match h with | .ExceptHandler _ _ _ hBody => collectDeclaredNamesAndTypes hBody.val.toList - let allNewDecls := (bodyDecls ++ handlerDecls).foldl (fun acc (n, ty) => + let allNewDecls := (bodyDecls ++ errorVarDecls ++ handlerDecls).foldl (fun acc (n, ty) => if acc.any (fun (an, _) => an == n) || ctx.variableTypes.any (fun (vn, _) => vn == n) then acc else acc ++ [(n, ty)]) [] let hoistedDecls : List StmtExprMd := allNewDecls.map fun (name, tyStr) => - let ty := if tyStr ∈ ctx.compositeTypeNames then + let ty := if tyStr ∈ ctx.compositeTypeNames || tyStr == "PythonError" then mkHighTypeMd (.UserDefined tyStr) else AnyTy mkStmtExprMd (StmtExpr.LocalVariable (name : String) ty (some (mkStmtExprMd .Hole))) let hoistedCtx := { ctx with variableTypes := ctx.variableTypes ++ (allNewDecls.map fun (n, ty) => - if ty ∈ ctx.compositeTypeNames then (n, ty) else (n, PyLauType.Any)) } + if ty ∈ ctx.compositeTypeNames || ty == "PythonError" then (n, ty) else (n, PyLauType.Any)) } -- Translate try body (with hoisted context so inner decls become assigns) let (bodyCtx, bodyStmts) ← translateStmtList hoistedCtx body.val.toList - let errorVars: List String := ((handlers.val.toList.filterMap (λ h => match h with - | .ExceptHandler _ _ errname _ => errname.val)).map (λ h => h.val)).dedup.filter - (λ e => e ∉ ctx.variableTypes.unzip.fst) - let errorTy := mkHighTypeMd (.UserDefined {text:= "PythonError"}) - let errorVarDecls := errorVars.map (λ e => mkStmtExprMd (.LocalVariable {text:=e} errorTy none)) - let ctx := {ctx with variableTypes:= ctx.variableTypes ++ errorVars.map (λ e => (e, "PythonError"))} - - -- Translate try body - let (bodyCtx, bodyStmts) ← translateStmtList ctx body.val.toList -- Translate exception handlers let mut handlerCtx := bodyCtx let mut handlerStmts : List StmtExprMd := [] @@ -1084,9 +1023,6 @@ partial def translateStmt (ctx : TranslationContext) (s : Python.stmt SourceRang handlerCtx := hCtx handlerStmts := handlerStmts ++ hStmts - let varDecls := bodyStmts.filter (λ stmt => match stmt.val with |.LocalVariable .. => true | _ => false) - let bodyStmts := bodyStmts.filter (λ stmt => match stmt.val with |.LocalVariable .. => false | _ => true) - -- Insert exception checks after each statement in try body let bodyStmtsWithChecks := bodyStmts.flatMap fun stmt => let isException := mkStmtExprMd (StmtExpr.StaticCall "isError" @@ -1098,15 +1034,6 @@ partial def translateStmt (ctx : TranslationContext) (s : Python.stmt SourceRang -- Normal completion: exit the try block, skipping handlers let exitTry := mkStmtExprMd (StmtExpr.Exit tryLabel) - let handlersVarDecls := handlerStmts.filter (λ stmt => match stmt.val with |.LocalVariable .. => true | _ => false) - handlerStmts := handlerStmts.filter (λ stmt => match stmt.val with |.LocalVariable .. => false | _ => true) - -- Create handler block - let handlerBlock := mkStmtExprMd (StmtExpr.Block handlerStmts (some handlerLabel)) - - let varDecls:= varDecls ++ errorVarDecls ++ handlersVarDecls - -- Wrap in try block - let tryBlock := mkStmtExprMdWithLoc (StmtExpr.Block (bodyStmtsWithChecks ++ [handlerBlock]) (some tryLabel)) md - return (bodyCtx, varDecls ++ [tryBlock]) -- catchers block: body + exit try (normal path) let catchersBlock := mkStmtExprMd (StmtExpr.Block (bodyStmtsWithChecks ++ [exitTry]) (some catchersLabel)) From e2ed383c3d0727962592d177815579eb98e4d579 Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Thu, 19 Mar 2026 11:23:31 -0700 Subject: [PATCH 3/6] Update Strata/Languages/Laurel/HeapParameterization.lean Co-authored-by: Joe Hendrix --- Strata/Languages/Laurel/HeapParameterization.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Strata/Languages/Laurel/HeapParameterization.lean b/Strata/Languages/Laurel/HeapParameterization.lean index e5286675d..ec919b9a3 100644 --- a/Strata/Languages/Laurel/HeapParameterization.lean +++ b/Strata/Languages/Laurel/HeapParameterization.lean @@ -178,7 +178,7 @@ def boxDestructorName (model : SemanticModel) (ty : HighType) : Identifier := | .UserDefined name => if isDatatype model name then s!"Box..{name.text}Val!" else "Box..compositeVal!" - | .TCore name => s!"Box..{name}Val" + | .TCore name => s!"Box..{name}Val!" | _ => dbg_trace f!"BUG, boxDestructorName bad type {ty}"; "boxDestructorNameError" /-- Get the Box constructor name for a given Laurel HighType. From a7b4f1cc419c05d13378b548b9c758032528690d Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Thu, 19 Mar 2026 11:23:42 -0700 Subject: [PATCH 4/6] Update Strata/Languages/Python/PythonToLaurel.lean Co-authored-by: Joe Hendrix --- Strata/Languages/Python/PythonToLaurel.lean | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/Strata/Languages/Python/PythonToLaurel.lean b/Strata/Languages/Python/PythonToLaurel.lean index 4501fe230..d40644a8a 100644 --- a/Strata/Languages/Python/PythonToLaurel.lean +++ b/Strata/Languages/Python/PythonToLaurel.lean @@ -1070,7 +1070,9 @@ partial def translateStmt (ctx : TranslationContext) (s : Python.stmt SourceRang | some varExpr => let varName := pyExprToString varExpr if varName ∈ currentCtx.variableTypes.unzip.fst then - setupStmts := setupStmts ++ [mgrDecl] + let assignStmt := mkStmtExprMd (StmtExpr.Assign + [mkStmtExprMd (StmtExpr.Identifier varName)] enterCall) + setupStmts := setupStmts ++ [mgrDecl, assignStmt] else let varDecl := mkStmtExprMd (StmtExpr.LocalVariable varName AnyTy (some enterCall)) currentCtx := {currentCtx with variableTypes := currentCtx.variableTypes ++ [(varName, PyLauType.Any)]} From 5e0f3ea00ecac43430e0a1061e4dd87ae0590263 Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Thu, 19 Mar 2026 11:23:53 -0700 Subject: [PATCH 5/6] Update Strata/Languages/Python/PythonToLaurel.lean Co-authored-by: Joe Hendrix --- Strata/Languages/Python/PythonToLaurel.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Strata/Languages/Python/PythonToLaurel.lean b/Strata/Languages/Python/PythonToLaurel.lean index d40644a8a..670e08c21 100644 --- a/Strata/Languages/Python/PythonToLaurel.lean +++ b/Strata/Languages/Python/PythonToLaurel.lean @@ -1588,7 +1588,7 @@ def pythonToLaurel' (info : PreludeInfo) -- FIRST PASS: Collect all class definitions and field type info let mut compositeTypes : List CompositeType := [pyErrorTy] - let mut compositeTypeNames := info.compositeTypes + let mut compositeTypeNames := info.compositeTypes.insert "PythonError" let mut classFieldHighType : Std.HashMap String (Std.HashMap String HighType) := {} for stmt in body.val do match stmt with From 4b0ccfb281df6ef53c4cb99541662824e0c76e03 Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Thu, 19 Mar 2026 12:55:58 -0700 Subject: [PATCH 6/6] swap pythonPrelude and laurelPrelude position --- Strata/Languages/Python/PySpecPipeline.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/Strata/Languages/Python/PySpecPipeline.lean b/Strata/Languages/Python/PySpecPipeline.lean index d1fbadf17..ae657e3b4 100644 --- a/Strata/Languages/Python/PySpecPipeline.lean +++ b/Strata/Languages/Python/PySpecPipeline.lean @@ -256,7 +256,8 @@ public def combinePySpecLaurel (info : Python.PreludeInfo) translation. -/ private def prependPrelude (coreFromLaurel : Core.Program) : Core.Program := let (preludeDecls, userDecls) := coreFromLaurel.decls.span (fun d => toString d.name != "FIRST_END_MARKER") - { decls := preludeDecls ++ Python.coreOnlyFromRuntimeCorePart ++ userDecls } + let (laurelPreludeDecls, pythonPreludeDecls) := preludeDecls.span (fun d => toString d.name != "Error") + { decls := pythonPreludeDecls ++ laurelPreludeDecls ++ Python.coreOnlyFromRuntimeCorePart ++ userDecls } /-- Translate a combined Laurel program to Core and prepend the full runtime prelude. Resolution errors are suppressed because PySpec