(core) Add jump/where expressions - #1005
Draft
dc-mak wants to merge 35 commits into
Draft
Conversation
Ewhere is a scoped version of Esave: it defines a block of mutually recursive labeled continuations (each with its own sym, core_base_type and parameter list), all in scope for a single body expression. Ejump is structurally equivalent to Erun but kept as a distinct constructor so that the typing and reduction rules can treat jumps into Ewhere-defined labels differently from Erun into Esave-defined labels. Erun/Esave and Ejump/Ewhere are intended to be mutually exclusive in any given program: a future Core rewriter will transform the latter into the former. All pattern-match sites (Lem sources, non-generated OCaml, parser, pipeline) updated with error stubs so the build passes. core_rewrite2 gets the alg_type record fields required by its type. Assisted-By: Claude Sonnet 4.6 <noreply@anthropic.com>
Ejump returns expr_ unchanged, same as Erun — there are no unsequenced subexpressions to flatten. Ewhere recurses into its body expression and each label's body. Assisted-By: Claude Sonnet 4.6 <noreply@anthropic.com>
explode_expr is dead code (explode_file is never called from the pipeline). The Esave case appears incomplete or incorrect — its arguments are always pointers to local variables, which could be struct pointers, yet it returns expr unchanged. Ejump mirrors Erun; Ewhere mirrors Esave for consistency. Assisted-By: Claude Sonnet 4.6 <noreply@anthropic.com>
Changes for commits 2-4 from the original plan. Assisted-By: Claude Sonnet 4.6 <noreply@anthropic.com>
core_rewrite.lem contains Core expression rewriting passes called via Core_rewrite.rewrite_file from the pipeline. rewrite_expr currently applies only flatten_seqs and pure_propagation2; the other six functions (remove_skips, remove_unseqs, remove_dead_aux, remove_conv_int, sequentialise_creates_kills, simpl_case) are dead (commented out). For all 8: Ejump is treated like Erun (pass-through, or map remove_conv_int_pexpr over its pexpr list for remove_conv_int). Ewhere recurses into its main expression and each label body, like Esave recurses into its body. For remove_dead_aux, Ejump is Left (like Erun) and Ewhere's Left/Right is determined by its main expression e, with label bodies also traversed. Assisted-By: Claude Sonnet 4.6 <noreply@anthropic.com>
core_rewrite2.lem provides a fold-based rewriting framework, but the whole file is dead: Core_rewrite2.rw_file is commented out in pipeline.ml and nothing else calls fold_expr, id_expr_alg, or pfp_expr_alg. Implements three locations: - fold_expr: Ewhere folds the main expression and each label body then calls alg.a_Ewhere; Ejump maps fold_pexpr over its pexpr list then calls alg.a_Ejump (matching Esave/Erun). - id_expr_alg and pfp_expr_alg: identity implementations that reconstruct the node, matching all other constructors. Assisted-By: Claude Sonnet 4.6 <noreply@anthropic.com>
dc-mak
force-pushed
the
where-expr
branch
5 times, most recently
from
May 27, 2026 18:14
83829b7 to
7ea611a
Compare
core_aux.lem provides Core expression utilities used throughout the pipeline. All 9 pattern-match sites are implemented: - subst_sym_expr / unsafe_subst_sym_expr: Ejump maps over its pexpr list like Erun; Ewhere substitutes into e and each label body, skipping bodies where the param list shadows the sym (matching how Esave handles its binding). - to_pure: Nothing for both, like Erun/Esave. - subst_wait: Ejump unchanged like Erun; Ewhere recurses into e and each label body like Esave. - find_labeled_continuation, find_labeled_continuation2_aux, collect_labeled_continuations, m_collect_saves_aux: all raise an error, but could return the "no match" value (Nothing / acc / Map.empty / st) if need be. These functions search for Esave/Erun label bindings; since Ejump/Ewhere are intended to be mutually exclusive with Erun/Esave in any given program, no matches are expected. - collect_saves_aux returns the "no match" value (st), since it's used on the path to core_reduction.lem Assisted-By: Claude Sonnet 4.6 <noreply@anthropic.com> squash for core_aux
dc-mak
force-pushed
the
where-expr
branch
6 times, most recently
from
May 28, 2026 10:31
4f3d133 to
159ca35
Compare
pp_core.ml is the Core IR pretty-printer, used by --pp core and debug output. Ejump prints as "jump sym(pes)", mirroring Erun. Ewhere prints like OCaml's let-rec-and: the first label uses "where" as its keyword (indented on a new line), subsequent labels use "and", and each body is indented from its header.
pp_core_ast.ml prints Core IR as a structured debug tree. Ejump/Ewhere previously fell through to the TODO_expr catch-all. Ejump is a leaf showing the target sym; Ewhere is a node containing the main expression followed by one labelled child per definition. Assisted-By: Claude Sonnet 4.6 <noreply@anthropic.com>
core_rewriter.ml is a generic monadic rewriter over Core exprs, used by remove_unspecs and core_peval. Ejump maps aux_pexpr over its pexpr list, like Erun. Ewhere maps aux over each label body and the main expression, like Esave. Assisted-By: Claude Sonnet 4.6 <noreply@anthropic.com>
Changes for commits 5-11 from the original plan. Assisted-By: Claude Sonnet 4.6 <noreply@anthropic.com>
Ejump is like Erun: map pp over pexprs. Ewhere propagates through e and each label body with env passed unchanged, mirroring the existing Esave case. A comment and assert on Esave explain the subtle invariant: elaboration re-uses local var syms across Esave binder boundaries but never re-binds them to a different value, so Esave params are never in env. Ewhere applies the same reasoning with its own assert, though whether the invariant holds for Ewhere label params is not yet fully confirmed. Assisted-By: Claude Sonnet 4.6 <noreply@anthropic.com>
subst_sym_expr2 substitutes a sym for another in a Core expression. Ejump mirrors Erun: map subst_sym_pexpr2 over pexprs. Ewhere mirrors Esave: substitute into e and each label body, skipping a body if sym is shadowed by that def's params. Unlike Esave, Ewhere params carry no pexprs so there is nothing to substitute in them. core_peval is only used by the playground binary, not the main pipeline. Assisted-By: Claude Sonnet 4.6 <noreply@anthropic.com>
Ejump/Ewhere and Esave/Erun are mutually exclusive in any given program. Replace the separate Ejump pass-through and Ewhere TODO stub with a single combined case that fails with a clear invariant-violation message in remove_save. Assisted-By: Claude Sonnet 4.6 <noreply@anthropic.com>
Parse and pretty-print Ewhere/Ejump so that --pp core output round-trips through the parser. Ewhere grammar closes with END (reuses existing token) to eliminate the AND-nested SR ambiguity; no new conflicts. pp_core.ml: append "end" keyword after defs list to match. - symbolify_expr: Ewhere uses under_scope + register_sym for mutual-recursion scoping; Ejump uses lookup_sym (not lookup_label) since where-labels live in sym_scopes. - register_labels: Ewhere recurses into e and each body with a TODO note that save/run and jump/where should not coexist. Assisted-By: Claude Sonnet 4.6 <noreply@anthropic.com>
Ejump mirrors Erun: keep annotation, map untype_pexpr over args. Ewhere recurses into e and each body; params have no pexprs so are copied unchanged. Assisted-By: Claude Sonnet 4.6 <noreply@anthropic.com>
Globals cannot contain Esave/Erun, so Ejump/Ewhere are treated similarly. Assisted-By: Claude Sonnet 4.6 <noreply@anthropic.com>
add_to_sb/add_to_asw: Ejump mirrors Erun (merge annotation set into sb_before/asw_before); Ewhere recurses into e and each body (params have no sub-expressions). convert_expr: Ejump mirrors Erun (empty_annotation); Ewhere recurses into e and each body, params copied unchanged. Assisted-By: Claude Sonnet 4.6 <noreply@anthropic.com>
Core_run.core_thread_step2 has cases for Ejump/Ewhere, but these are left as erroring with a message saying that the code is/was dead at the time of them being added.
Ewhere(e, defs) is an evaluation context for e, so add Cwhere
to Core_run_aux.context alongside Csseq, Cwseq, etc.
Update all helpers that exhaustively match on context.
- `apply_ctx` and `get_ctx` are straightforward
- `has_ccall` and `is_unseq_with_ccall_aux` (latter calls former) cases
are also straightforward, but should be impossible for a C program (no
wheres inside an unseq) and so are commented as such
- Remainders are simple context traversals: recurse and reconstruct
- `break_at_sseq`: locates the innermost `Csseq` in a context chain
- `break_at_bound_and_sseq`: uses `break_at_seq`, locates the nearest
`Cbound` and optionally a `Csseq` within it
- `pull_dyn_annotations` is dead: strips `Cannot` nodes from the
context, returning the annotations and a cleaned context
- `add_exclusion`: adds an exclusion ID to every `Cannot` node in the
context. Should also be impossible for a C program (no `where`
inside `bound`, and exclusions are only added inside `bound`s)
Assisted-By: Claude Sonnet 4.6 <noreply@anthropic.com>
Ewhere(e, defs) and Esseq(pat, Ejump, e2) are one-level
patterns handled in one_step, just like Esseq(pat, pure(v), e2).
Adjust get_ctx so it treats Ewhere(Ejump) and Esseq(Ejump)
as atomic redexes (ctx = CTX).
Four rules (plus context reduction):
[Where-Pure]
------------------------------
pure(v) where defs --> pure(v)
[Jump-Sub]
( defs(l) = x . E )
----------------------------------------------
jump l(pe) where defs --> {val/x} E where defs
[Jump-Where]
(l not in defs)
------------------------------------
jump l(pe) where defs --> jump l(pe)
[Jump-Let]
---------------------------------------
lets _ = jump l(pe) in E --> jump l(pe)
Semantics are reminiscent of checked exceptions: Ejump
propagates out through Esseq continuations until caught
by an enclosing Ewhere.
Minor caveat: all have to take into account annot(jump l(args)) case.
Ejump mirrors Erun: look up sym in env.labs, zip the stored param types with the argument pexprs, and typecheck each argument. The return-type annotation is not checked, consistent with Erun. Ewhere: fold the defs to build labs_env (env extended with each label and its param types in labs), typecheck each def body against its own declared bTy with labs_env extended by that def's params in decls, and typecheck the main body e against expected_bTy. Assisted-By: Claude Sonnet 4.6 <noreply@anthropic.com>
Add check_label_style, called before collect_labels on every procedure body and global definition. Two invariants are enforced: - No mixing: a body may not contain both Erun/Esave and Ejump/Ewhere. - Context restriction: save-style constructs (Erun, Esave) must have only Eif, Esseq, or Esave as ancestors; where-style constructs (Ejump, Ewhere) only Eif, Esseq, or Ewhere. Erun/Ejump can also occur inside Ecase. check_label_style returns the detected style; call sites skip collect_labels for where-style bodies since Ewhere labels are registered locally in typecheck_expr rather than by a pre-pass. Assisted-By: Claude Sonnet 4.6 <noreply@anthropic.com>
Replace CoreTyping_TODO usages in core_typing.lem with dedicated constructors: UndeclaredLabel (jump to unknown label), MixedLabelStyles (mixing Erun/Esave with Ejump/Ewhere), and LabelOutsideContext (label construct outside its allowed Eif/Esseq/Esave or Ewhere context). Also simplify check_label_style_aux by dropping the unused top_e parameter now that error messages no longer include an expression dump. Assisted-By: Claude Sonnet 4.6 <noreply@anthropic.com>
Add SW_save_to_where switch (switches.ml/mli), a no-op save_to_where.ml rewriter, the pipeline wiring in the pipeline, and a CI script. The pass will transform procedures from Esave/Erun style to Ewhere/Ejump style; this commit just establishes the hook so the pipeline compiles and the switch is recognised. Assisted-By: Claude Sonnet 4.6 <noreply@anthropic.com>
This commit defines a bottom-up function which annotates each expression with a map from symbols to number of children which contain a run/save to that label. The annotation can't be done on the Core.generic_expr type directly, so it also defines an auxilliary type to store the information. It does the transformation and discards the result so that I can check the safety of the code so far by running it with the run tests/run-save-to-where.sh script.
Went a little crazy with debug printing, but it is quite helpful to see and explain what's going on (even if the code looks to be working right on the first go).
Using the results of the bottom up run/save count, we can do a top-down pass and annotate the dominator context of a used label: the first node which (a) isn't already dominated and (b) has the label used by more than one of its children. If the label is unused, then we reach the save node with neither of those conditions holding - this is still the correct place for a dominator context, but a redundant one, so it's added as unused. I annotate each node with a map from labels to Used or Unused. A simple set would suffice, but tracking whether a label is used will help later stages simplify away unused auto-generated Core labels.
This commit uses the dominator context computation to transform run/saves to jump/wheres. The pass is a bottom-up which maps runs to jumps directly. The function can be thought of first transforming saves as follows: save l (x := pe) in E ~> jump l(pe) where l(x) := E end and then bubbling this outward, capturing (moving inside a label definiton) the continuation (layers of enclosing let strong pat = _ in E) of that expression until it reaches the dominating context of l. In reality, labels may overlap this happens when we goto _inside_ C blocks, so more than one label may be "live" (capturing) at the same time. To handle this we need to keep track of not just the labels definitions, but also the "live" labels being captured. Loops and gotos which only jump out of scopes will only capture the continuation of exactly one label at a time (and would not need to track "live" labels). Labels are removed from the live set when the expression bubbling outwards crosses its dominating context. When the set of live labels is empty, we stop capturing and bubbling outwards and place the where expression there.
Collaborator
Author
|
FYI, this PR I made a special effort to have it be reviewable one commit at a time, so hope that helps. |
This commit annotates each node of the constructed jump/where expression with a set of labels jumped to within it.
There are cases in which the exit label of a where-expr ends up
capturing a continuation longer than seems necessary. This happens for
the below case, when E1 and E2 mention the where labels, but E3 does
not. Note that it's perfectly fine for E3 to mention labels outside the
defs (e.g. return labels).
E_body
where exit(x) : bty3 :=
let strong pat1 : bty1 = E1 in
let strong pat2 : bty2 = E2 in
E3
and ... end
In this case, we can rewrite the program to the following
let strong pat2 : bty2 =
E_body
where exit(x) : bty2 :=
let strong pat1 : bty2 = E1 in
E2
and .. end in
E3
In fact, we can even recurse into E2 and do the same thing again,
unwrapping and hoisting out multiple layers of continuations which don't
mention any (immediately enclosing) where labels.
But we have to be careful that E3 doesn't mention parameters x, or
variables from pat1. This commit introduces a flawed rewrite which does
the transformation without tracking free variables. Though it works
mostly, it can occasionally produce ill-scoped programs.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This series of commits adds two new constructors to Core, jump/where as a better-behaved, compositional alternative to run/save. jump is identical to run, but I've added it to keep the code simple.
A separate PR, to translate run/save Core programs to jump/where programs, will come later.
The semantics are described with just four rules, plus context reduction,
C ::= .. | where(__, defs):Semantics are reminiscent of checked exceptions: Ejump
propagates out through Esseq continuations until caught
by an enclosing Ewhere.