Skip to content

Bug fix: Put the datatypes defined inside Python prelude on the top of Laurel Prelude. #618

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
thanhnguyen-aws wants to merge 12 commits into from
Closed

Bug fix: Put the datatypes defined inside Python prelude on the top of Laurel Prelude. #618

Changes from all commits
Commits
Show all changes
12 commits
Select commit Hold shift + click to select a range
90774ba
fix type checking bugs
thanhnguyen-aws Mar 18, 2026
f9f12c7
Merge branch 'main' into ignorecomment
thanhnguyen-aws Mar 19, 2026
80b67b4
Merge branch 'main' into ignorecomment
aqjune-aws Mar 19, 2026
aa07beb
Merge branch 'main' into ignorecomment
thanhnguyen-aws Mar 19, 2026
77318d1
merge conflict + remove .Hole processing in if, while, assert condition
thanhnguyen-aws Mar 19, 2026
3cc2502
merge conflict
thanhnguyen-aws Mar 19, 2026
e2ed383
Update Strata/Languages/Laurel/HeapParameterization.lean
thanhnguyen-aws Mar 19, 2026
a7b4f1c
Update Strata/Languages/Python/PythonToLaurel.lean
thanhnguyen-aws Mar 19, 2026
5e0f3ea
Update Strata/Languages/Python/PythonToLaurel.lean
thanhnguyen-aws Mar 19, 2026
4b0ccfb
swap pythonPrelude and laurelPrelude position
thanhnguyen-aws Mar 19, 2026
7d175b7
Merge branch 'main' into swapprelude
thanhnguyen-aws Mar 19, 2026
f7bb93d
Merge branch 'main' into swapprelude
thanhnguyen-aws Mar 20, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 2 additions & 1 deletion Strata/Languages/Python/PySpecPipeline.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
Loading