|
| 1 | +/- |
| 2 | + Copyright Strata Contributors |
| 3 | +
|
| 4 | + SPDX-License-Identifier: Apache-2.0 OR MIT |
| 5 | +-/ |
| 6 | +module |
| 7 | + |
| 8 | +public import Strata.Languages.Laurel.MapStmtExpr |
| 9 | +public import Strata.Languages.Laurel.Resolution |
| 10 | +public import Strata.Languages.Laurel.LaurelPass |
| 11 | + |
| 12 | +/-! |
| 13 | +# Lift Instance Procedures |
| 14 | +
|
| 15 | +A Laurel-to-Laurel pass that lifts every instance procedure (a procedure |
| 16 | +defined inside a `composite` block) to a top-level static procedure with a |
| 17 | +mangled name `<CompositeName>$<methodName>`, then rewrites every call site |
| 18 | +that resolved to such an instance procedure to use the lifted name. |
| 19 | +
|
| 20 | +After this pass: |
| 21 | +- `CompositeType.instanceProcedures` is empty for every composite. |
| 22 | +- `program.staticProcedures` contains the lifted procedures. |
| 23 | +- Every `InstanceCall` (from `obj#method(args)` surface syntax) points |
| 24 | + at the lifted name. For `InstanceCall`, the receiver is prepended to |
| 25 | + the argument list to match the lifted procedure's `self : <CompositeName>` |
| 26 | + parameter. |
| 27 | +-/ |
| 28 | + |
| 29 | +namespace Strata.Laurel |
| 30 | + |
| 31 | +/-! ## Lifting + call-site rewriting |
| 32 | +
|
| 33 | +Lift instance procedures to static scope (e.g., procedure `proc` |
| 34 | +of composite type `T` will be lifted to `T$proc`). |
| 35 | +Then, rewrite caller-side of `obj#proc` to call the lifted procedure |
| 36 | +
|
| 37 | +-/ |
| 38 | + |
| 39 | +/-- Top-level name produced for a lifted instance procedure. -/ |
| 40 | +def liftedProcName (typeName methodName : Identifier) : Identifier := |
| 41 | + mkId s!"{typeName.text}${methodName.text}" |
| 42 | + |
| 43 | +/-- Rewrite a single node so that any callee resolving to an instance procedure |
| 44 | + is replaced by its lifted name. -/ |
| 45 | +private def rewriteCallNode (model : SemanticModel) (expr : StmtExprMd) : StmtExprMd := |
| 46 | + match expr.val with |
| 47 | + | .StaticCall callee args => |
| 48 | + match model.get? callee with |
| 49 | + | some (.instanceProcedure typeName _) => |
| 50 | + let lifted := liftedProcName typeName callee |
| 51 | + { expr with val := .StaticCall lifted args } |
| 52 | + | _ => expr |
| 53 | + | .InstanceCall target callee args => |
| 54 | + -- `obj#method(args)` surface syntax parses to InstanceCall. Flatten it to |
| 55 | + -- a static call against the lifted name, prepending the receiver as the |
| 56 | + -- first argument to match the lifted procedure's `self` parameter. |
| 57 | + match model.get? callee with |
| 58 | + | some (.instanceProcedure typeName _) => |
| 59 | + let lifted := liftedProcName typeName callee |
| 60 | + { expr with val := .StaticCall lifted (target :: args) } |
| 61 | + | _ => expr |
| 62 | + | _ => expr |
| 63 | + |
| 64 | +/-- Apply call-site rewriting to every expression in a procedure. -/ |
| 65 | +private def rewriteCallsInProc (model : SemanticModel) (proc : Procedure) : Procedure := |
| 66 | + let f := mapStmtExpr (rewriteCallNode model) |
| 67 | + let resolveBody : Body → Body := fun body => match body with |
| 68 | + | .Transparent b => .Transparent (f b) |
| 69 | + | .Opaque ps impl modif => |
| 70 | + .Opaque (ps.map (·.mapCondition f)) (impl.map f) (modif.map f) |
| 71 | + | .Abstract ps => .Abstract (ps.map (·.mapCondition f)) |
| 72 | + | .External => .External |
| 73 | + { proc with |
| 74 | + body := resolveBody proc.body |
| 75 | + preconditions := proc.preconditions.map (·.mapCondition f) |
| 76 | + decreases := proc.decreases.map f |
| 77 | + invokeOn := proc.invokeOn.map f } |
| 78 | + |
| 79 | +/-- Apply call-site rewriting to a constrained type's constraint and witness. -/ |
| 80 | +private def rewriteCallsInType (model : SemanticModel) (td : TypeDefinition) : TypeDefinition := |
| 81 | + match td with |
| 82 | + | .Constrained ct => |
| 83 | + let f := mapStmtExpr (rewriteCallNode model) |
| 84 | + .Constrained { ct with constraint := f ct.constraint, witness := f ct.witness } |
| 85 | + | _ => td |
| 86 | + |
| 87 | +public section |
| 88 | + |
| 89 | +/-- |
| 90 | +Lift every `proc ∈ ct.instanceProcedures` to a top-level static procedure |
| 91 | +named via `liftedProcName`, rewrite call sites that resolved to an instance |
| 92 | +procedure, and clear `instanceProcedures` on every composite. |
| 93 | +-/ |
| 94 | +def liftInstanceProcedures (model : SemanticModel) (program : Program) : Program := |
| 95 | + -- Step 1: collect lifted clones |
| 96 | + let liftedProcs : List Procedure := |
| 97 | + program.types.foldl (init := []) fun acc td => |
| 98 | + match td with |
| 99 | + | .Composite ct => |
| 100 | + acc ++ ct.instanceProcedures.map fun proc => |
| 101 | + { proc with name := liftedProcName ct.name proc.name } |
| 102 | + | _ => acc |
| 103 | + |
| 104 | + if liftedProcs.isEmpty then program else |
| 105 | + |
| 106 | + -- Step 2: rewrite call sites in procedure bodies and constrained-type |
| 107 | + let rewrittenStaticProcs := program.staticProcedures.map (rewriteCallsInProc model) |
| 108 | + let rewrittenLiftedProcs := liftedProcs.map (rewriteCallsInProc model) |
| 109 | + let rewrittenTypes := program.types.map (rewriteCallsInType model) |
| 110 | + |
| 111 | + -- Step 3: clear instanceProcedures on every composite. |
| 112 | + let cleanedTypes := rewrittenTypes.map fun td => |
| 113 | + match td with |
| 114 | + | .Composite ct => .Composite { ct with instanceProcedures := [] } |
| 115 | + | _ => td |
| 116 | + |
| 117 | + -- Step 4: append lifted procs. |
| 118 | + { program with |
| 119 | + staticProcedures := rewrittenStaticProcs ++ rewrittenLiftedProcs |
| 120 | + types := cleanedTypes } |
| 121 | + |
| 122 | +end -- public section |
| 123 | + |
| 124 | +/-- Pipeline pass: lift instance procedures to top-level static procedures |
| 125 | + and rewrite call sites to use the lifted names. -/ |
| 126 | +public def liftInstanceProceduresPass : LaurelPass where |
| 127 | + name := "LiftInstanceProcedures" |
| 128 | + documentation := "Lifts every procedure declared inside a `composite` block to a top-level static procedure named `<CompositeName>$<methodName>` and rewrites call sites resolved to an instance procedure (including `obj#method(args)` surface syntax) to point at the lifted name. Clears `instanceProcedures` on every composite. Must run before HeapParameterization." |
| 129 | + needsResolves := true |
| 130 | + run := fun p m => (liftInstanceProcedures m p, [], {}) |
| 131 | + |
| 132 | +end Strata.Laurel |
0 commit comments