diff --git a/Strata/Languages/Laurel/CoreGroupingAndOrdering.lean b/Strata/Languages/Laurel/CoreGroupingAndOrdering.lean index 8a84b0c545..2cb6b89d46 100644 --- a/Strata/Languages/Laurel/CoreGroupingAndOrdering.lean +++ b/Strata/Languages/Laurel/CoreGroupingAndOrdering.lean @@ -33,7 +33,6 @@ def collectTypeRefs : HighTypeMd → List String | ⟨.UserDefined name, _⟩ => [name.text] | ⟨.TSet elem, _⟩ => collectTypeRefs elem | ⟨.TMap k v, _⟩ => collectTypeRefs k ++ collectTypeRefs v - | ⟨.TTypedField vt, _⟩ => collectTypeRefs vt | ⟨.Applied base args, _⟩ => collectTypeRefs base ++ args.flatMap collectTypeRefs | ⟨.Pure base, _⟩ => collectTypeRefs base diff --git a/Strata/Languages/Laurel/FilterPrelude.lean b/Strata/Languages/Laurel/FilterPrelude.lean index 8eb64060b3..18bbca462b 100644 --- a/Strata/Languages/Laurel/FilterPrelude.lean +++ b/Strata/Languages/Laurel/FilterPrelude.lean @@ -71,14 +71,13 @@ private partial def collectHighTypeNames (ty : HighTypeMd) : CollectM Unit := do match ty.val with | .UserDefined name => addTypeName name.text | .TCore _ => pure () - | .TTypedField vt => collectHighTypeNames vt | .TSet et => collectHighTypeNames et | .TMap kt vt => collectHighTypeNames kt; collectHighTypeNames vt | .Applied base args => collectHighTypeNames base; args.forM collectHighTypeNames | .Pure base => collectHighTypeNames base | .Intersection types => types.forM collectHighTypeNames - | .TVoid | .TBool | .TInt | .TFloat64 | .TReal | .TString | .THeap + | .TVoid | .TBool | .TInt | .TFloat64 | .TReal | .TString | .TBv _ | .Unknown | .MultiValuedExpr _ => pure () /-- Collect all referenced names (procedure calls, type references) from a StmtExpr tree. -/ diff --git a/Strata/Languages/Laurel/Grammar/AbstractToConcreteTreeTranslator.lean b/Strata/Languages/Laurel/Grammar/AbstractToConcreteTreeTranslator.lean index 414bf1451f..2595594f48 100644 --- a/Strata/Languages/Laurel/Grammar/AbstractToConcreteTreeTranslator.lean +++ b/Strata/Languages/Laurel/Grammar/AbstractToConcreteTreeTranslator.lean @@ -49,9 +49,7 @@ partial def highTypeValToArg : HighType → Arg | .UserDefined name => laurelOp "compositeType" #[ident name.text] | .TCore s => laurelOp "coreType" #[ident s] | .TVoid => laurelOp "compositeType" #[ident "void"] - | .THeap => laurelOp "compositeType" #[ident "Heap"] - -- Type parameters discarded; the grammar cannot represent Field[T] or Set[T] - | .TTypedField _vt => laurelOp "compositeType" #[ident "Field"] + -- Type parameters discarded; the grammar cannot represent Set[T] | .TSet _et => laurelOp "compositeType" #[ident "Set"] | .Applied base _args => -- Applied types are not directly representable in the grammar; diff --git a/Strata/Languages/Laurel/HeapParameterization.lean b/Strata/Languages/Laurel/HeapParameterization.lean index 3b266a9fff..f228d6c477 100644 --- a/Strata/Languages/Laurel/HeapParameterization.lean +++ b/Strata/Languages/Laurel/HeapParameterization.lean @@ -25,12 +25,12 @@ and a `nextReference: int` for allocating new objects. Box is a sum type with co primitive type (BoxInt, BoxBool, BoxFloat64, BoxComposite). Composite is a type synonym for int. 1. Procedures that write the heap get an inout heap parameter - - Input: `heap : THeap` - - Output: `heap : THeap` + - Input: `heap : Heap` + - Output: `heap : Heap` - Field writes become: `heap := updateField(heap, obj, field, BoxT(value))` 2. Procedures that only read the heap get an in heap parameter - - Input: `heap : THeap` + - Input: `heap : Heap` - Field reads become: `Box..tVal(readField(heap, obj, field))` 3. Procedure calls are transformed: @@ -480,8 +480,11 @@ def heapTransformProcedure (model: SemanticModel) (proc : Procedure) : Transform if writesHeap then -- This procedure writes the heap - add $heap_in as input and $heap as output -- At the start, assign $heap_in to $heap, then use $heap throughout - let heapInParam : Parameter := { name := heapInName, type := ⟨.THeap, none⟩ } - let heapOutParam : Parameter := { name := heapName, type := ⟨.THeap, none⟩ } + -- Type the heap parameters as the prelude `Heap` datatype so they stay + -- consistent with the generated heap functions (`readField`, `updateField`, + -- `increment`, `Heap..nextReference!`), all of which are declared over `Heap`. + let heapInParam : Parameter := { name := heapInName, type := ⟨.UserDefined "Heap", proc.name.source⟩ } + let heapOutParam : Parameter := { name := heapName, type := ⟨.UserDefined "Heap", proc.name.source⟩ } let inputs' := heapInParam :: proc.inputs let outputs' := heapOutParam :: proc.outputs @@ -519,8 +522,10 @@ def heapTransformProcedure (model: SemanticModel) (proc : Procedure) : Transform body := body' } else if readsHeap then - -- This procedure only reads the heap - add $heap as input only - let heapParam : Parameter := { name := heapName, type := ⟨.THeap, none⟩ } + -- This procedure only reads the heap - add $heap as input only. + -- Use the prelude `Heap` datatype for the parameter type (see the + -- writes-heap branch above for rationale). + let heapParam : Parameter := { name := heapName, type := ⟨.UserDefined "Heap", proc.name.source⟩ } let inputs' := heapParam :: proc.inputs let preconditions' ← proc.preconditions.mapM (·.mapM (heapTransformExpr heapName model)) @@ -578,7 +583,7 @@ def heapParameterization (model: SemanticModel) (program : Program) : Program := public def heapParameterizationPass : LaurelPass where name := "HeapParameterization" documentation := "Transforms procedures that interact with the heap by adding explicit heap parameters. The heap is modeled as `Map Composite (Map Field Box)`. Procedures that write the heap receive both an input and output heap parameter; procedures that only read the heap receive an input heap parameter. Field reads and writes are rewritten to use `readField` and `updateField` functions." - needsResolves := true + needsResolves := false -- Only resolve again after completing HeapParam, ModifiesClauses and TypeHierarchy. These are logically one pass. run := fun p m => (heapParameterization m p, [], {}) comesBefore := [ diff --git a/Strata/Languages/Laurel/LaurelAST.lean b/Strata/Languages/Laurel/LaurelAST.lean index bbaec0fdfa..1574b210cc 100644 --- a/Strata/Languages/Laurel/LaurelAST.lean +++ b/Strata/Languages/Laurel/LaurelAST.lean @@ -135,8 +135,7 @@ structure AstNode (t : Type) : Type where The type system for Laurel programs. `HighType` covers primitive types (`TVoid`, `TBool`, `TInt`, `TReal`, `TFloat64`, -`TString`), internal types used by the heap parameterization pass (`THeap`, -`TTypedField`), collection types (`TSet`), user-defined types (`UserDefined`), +`TString`), collection types (`TSet`), user-defined types (`UserDefined`), generic applications (`Applied`), value types (`Pure`), and intersection types (`Intersection`). -/ @@ -153,10 +152,6 @@ inductive HighType : Type where | TReal /-- String type for text data. -/ | TString - /-- Internal type representing the heap. Introduced by the heap parameterization pass; not accessible via grammar. -/ - | THeap - /-- Internal type for a field constant with a known value type. Introduced by the heap parameterization pass; not accessible via grammar. -/ - | TTypedField (valueType : AstNode HighType) /-- Set type, e.g. `Set int`. -/ | TSet (elementType : AstNode HighType) /-- Map type. -/ @@ -527,9 +522,7 @@ def highEq (a : HighTypeMd) (b : HighTypeMd) : Bool := match _a: a.val, _b: b.va | HighType.TFloat64, HighType.TFloat64 => true | HighType.TReal, HighType.TReal => true | HighType.TString, HighType.TString => true - | HighType.THeap, HighType.THeap => true | HighType.TBv n1, HighType.TBv n2 => n1 == n2 - | HighType.TTypedField t1, HighType.TTypedField t2 => highEq t1 t2 | HighType.TSet t1, HighType.TSet t2 => highEq t1 t2 | HighType.TMap k1 v1, HighType.TMap k2 v2 => highEq k1 k2 && highEq v1 v2 | HighType.UserDefined r1, HighType.UserDefined r2 => r1.text == r2.text @@ -630,7 +623,7 @@ def isSubtype (ctx : TypeLattice) (sub sup : HighTypeMd) : Bool := /- ### Variance policy (covers `isSubtype` and `isConsistent`) All child-carrying constructors are INVARIANT by design: `isConsistent` bottoms out in `highEq` (structural equality) for `TSet`, `TMap`, - `TTypedField`, `Applied`, `Pure`, and `Intersection`. So `TSet Unknown ~ + `Applied`, `Pure`, and `Intersection`. So `TSet Unknown ~ TSet TInt` is FALSE — `Unknown` is a wildcard only at the TOP of a type, never under a constructor. This is intentional: `TSet` / `TMap` are MUTABLE collections, where covariance would be unsound; if you don't know the diff --git a/Strata/Languages/Laurel/LaurelCompilationPipeline.lean b/Strata/Languages/Laurel/LaurelCompilationPipeline.lean index e0f2c7137f..fb47f63def 100644 --- a/Strata/Languages/Laurel/LaurelCompilationPipeline.lean +++ b/Strata/Languages/Laurel/LaurelCompilationPipeline.lean @@ -145,12 +145,12 @@ private def runLaurelPasses -- Initial resolution let result := resolve program - let resolutionErrors : List DiagnosticModel := result.errors.toList + let resolutionErrors : Std.HashSet DiagnosticModel := Std.HashSet.ofArray result.errors let (program, model) := (result.program, result.model) let mut program := program let mut model := model - let mut allDiags : List DiagnosticModel := resolutionErrors + let mut allDiags : List DiagnosticModel := result.errors.toList let mut allStats : Statistics := {} for pass in laurelPipeline do @@ -163,7 +163,13 @@ private def runLaurelPasses let result := resolve program (some model) let newErrors := result.errors.filter fun e => !resolutionErrors.contains e if !newErrors.isEmpty then + let newDiags := newErrors.toList.map fun d => + { d with + message := + s!"Internal error: resolution after '{pass.name}' introduced this diagnostic: {d.message}" + type := .StrataBug } emit pass.name "laurel.st" program + return (program, model, allDiags ++ newDiags, allStats) program := result.program model := result.model emit pass.name "laurel.st" program diff --git a/Strata/Languages/Laurel/LaurelToCoreTranslator.lean b/Strata/Languages/Laurel/LaurelToCoreTranslator.lean index 5948aa1d9e..5797395ed9 100644 --- a/Strata/Languages/Laurel/LaurelToCoreTranslator.lean +++ b/Strata/Languages/Laurel/LaurelToCoreTranslator.lean @@ -79,13 +79,10 @@ def translateType (ty : HighTypeMd) : TranslateM LMonoTy := do | .TString => return LMonoTy.string | .TBv n => return LMonoTy.bitvec n | .TVoid => return LMonoTy.bool -- Using bool as placeholder for void - | .THeap => return .tcons "Heap" [] - | .TTypedField _ => return .tcons "Field" [] | .TSet elementType => return Core.mapTy (← translateType elementType) LMonoTy.bool | .TMap keyType valueType => return Core.mapTy (← translateType keyType) (← translateType valueType) | .UserDefined name => match model.get? name with - | some (.compositeType _) => return .tcons "Composite" [] | some (.datatypeDefinition dt) => return .tcons dt.name.text [] | some (.datatypeConstructor typeName _) => return .tcons typeName.text [] | _ => do -- resolution should have already emitted a diagnostic @@ -287,6 +284,8 @@ def translateExpr (expr : StmtExprMd) throwExprDiagnostic $ diagnosticFromSource expr.source s!"FieldSelect should have been eliminated by heap parameterization: {Std.ToFormat.format target}#{fieldId.text}" DiagnosticType.StrataBug | .Block (⟨ .Assign _ _, assignSource⟩ :: tail) _ => disallowed assignSource "destructive assignments are not supported in transparent bodies or contracts" + | .Block (⟨ .While _ _ _ _, whileSource⟩ :: tail) _ => + disallowed whileSource "loops are not supported in functions or contracts" | .Block (head :: tail) _ => throwExprDiagnostic $ diagnosticFromSource expr.source s!"block expression starting with {head.val.constructorName} should have been lowered in a separate pass" DiagnosticType.StrataBug | .Block [] _ => diff --git a/Strata/Languages/Laurel/LiftImperativeExpressions.lean b/Strata/Languages/Laurel/LiftImperativeExpressions.lean index 20cd25d908..2d15f56c2f 100644 --- a/Strata/Languages/Laurel/LiftImperativeExpressions.lean +++ b/Strata/Languages/Laurel/LiftImperativeExpressions.lean @@ -439,7 +439,7 @@ def transformStmt (stmt : StmtExprMd) : LiftM (List StmtExprMd) := do -- If the RHS is a direct imperative StaticCall, don't lift it — -- translateStmt handles Assign + StaticCall directly as a call statement. match _: valueMd with - | AstNode.mk value _ => + | AstNode.mk value callSource => match _: value with | .StaticCall callee args => let model := (← get).model @@ -452,7 +452,7 @@ def transformStmt (stmt : StmtExprMd) : LiftM (List StmtExprMd) := do let seqArgs ← args.mapM transformExpr let argPrepends ← takePrepends modify fun s => { s with subst := [] } - return argPrepends ++ [⟨.Assign targets ⟨.StaticCall callee seqArgs, source⟩, source⟩] + return argPrepends ++ [⟨.Assign targets ⟨.StaticCall callee seqArgs, callSource⟩, source⟩] | _ => let seqValue ← transformExpr valueMd let prepends ← takePrepends diff --git a/Strata/Languages/Laurel/MapStmtExpr.lean b/Strata/Languages/Laurel/MapStmtExpr.lean index f39cbfb621..47da17b591 100644 --- a/Strata/Languages/Laurel/MapStmtExpr.lean +++ b/Strata/Languages/Laurel/MapStmtExpr.lean @@ -137,5 +137,107 @@ def mapProgramM [Monad m] (f : StmtExprMd → m StmtExprMd) (program : Program) def mapProgram (f : StmtExprMd → StmtExprMd) (program : Program) : Program := mapProgramM (m := Id) f program +/-! ## Type-annotation traversals + +`mapStmtExprHighTypesM` and friends apply a `HighType → HighType` rewrite to +*every* type annotation reachable from a node / procedure / program, reusing +`mapStmtExprM` for the structural recursion. This is the single source of truth +for "rewrite all type references", so passes don't have to enumerate the +type-carrying constructors by hand (and silently miss one). The supplied `f` is +responsible for recursing into compound types (`TSet`/`TMap`/`Applied`/…). -/ + +/-- Rewrite the declared type carried by a `Variable` (only `Declare` carries one). -/ +def mapVariableHighTypesM [Monad m] (f : HighTypeMd → m HighTypeMd) (v : Variable) : m Variable := do + match v with + | .Declare param => pure (.Declare { param with type := ← f param.type }) + | .Local _ | .Field _ _ => pure v + +/-- +Apply `f` to every `HighType` annotation carried *directly* by a single +`StmtExpr` node: local declarations (in `Var`, `Assign` targets, and `IncrDecr` +targets), quantifier binders, `AsType`/`IsType` type arguments, and typed +`Hole`s. Does **not** recurse into child expressions — compose with +`mapStmtExprM` (see `mapStmtExprHighTypesM`) for a whole-tree traversal. +-/ +def mapNodeHighTypesM [Monad m] (f : HighTypeMd → m HighTypeMd) (expr : StmtExprMd) : m StmtExprMd := do + let source := expr.source + match expr.val with + | .Var v => pure ⟨.Var (← mapVariableHighTypesM f v), source⟩ + | .Assign targets value => + let targets' ← targets.mapM (fun t => do pure (⟨← mapVariableHighTypesM f t.val, t.source⟩ : VariableMd)) + pure ⟨.Assign targets' value, source⟩ + | .IncrDecr mode op target => + pure ⟨.IncrDecr mode op ⟨← mapVariableHighTypesM f target.val, target.source⟩, source⟩ + | .Quantifier mode param trigger body => + pure ⟨.Quantifier mode { param with type := ← f param.type } trigger body, source⟩ + | .AsType target ty => pure ⟨.AsType target (← f ty), source⟩ + | .IsType target ty => pure ⟨.IsType target (← f ty), source⟩ + | .Hole det (some ty) => pure ⟨.Hole det (some (← f ty)), source⟩ + | _ => pure expr + +/-- Apply `f` to every `HighType` annotation appearing anywhere in a `StmtExprMd`. -/ +def mapStmtExprHighTypesM [Monad m] (f : HighTypeMd → m HighTypeMd) (expr : StmtExprMd) : m StmtExprMd := + mapStmtExprM (mapNodeHighTypesM f) expr + +/-- Pure version of `mapStmtExprHighTypesM`. -/ +def mapStmtExprHighTypes (f : HighTypeMd → HighTypeMd) (expr : StmtExprMd) : StmtExprMd := + mapStmtExprHighTypesM (m := Id) f expr + +/-- Apply `f` to every `HighType` annotation in a procedure: parameter types, + body, preconditions, decreases measure, and auto-invocation trigger. -/ +def mapProcedureHighTypesM [Monad m] (f : HighTypeMd → m HighTypeMd) (proc : Procedure) : m Procedure := do + let mapExpr := mapStmtExprHighTypesM f + let mapParam (p : Parameter) : m Parameter := do pure { p with type := ← f p.type } + let body' ← match proc.body with + | .Transparent b => pure (.Transparent (← mapExpr b)) + | .Opaque ps impl mods => + pure (.Opaque (← ps.mapM (·.mapM mapExpr)) (← impl.mapM mapExpr) (← mods.mapM mapExpr)) + | .Abstract ps => pure (.Abstract (← ps.mapM (·.mapM mapExpr))) + | .External => pure .External + return { proc with + inputs := ← proc.inputs.mapM mapParam + outputs := ← proc.outputs.mapM mapParam + body := body' + preconditions := ← proc.preconditions.mapM (·.mapM mapExpr) + decreases := ← proc.decreases.mapM mapExpr + invokeOn := ← proc.invokeOn.mapM mapExpr } + +/-- Apply `f` to every `HighType` annotation in a type definition: composite + fields and instance procedures, constrained base/constraint/witness, + datatype constructor argument types, and alias targets. -/ +def mapTypeDefinitionHighTypesM [Monad m] (f : HighTypeMd → m HighTypeMd) (td : TypeDefinition) : m TypeDefinition := do + match td with + | .Composite ct => + pure (.Composite { ct with + fields := ← ct.fields.mapM (fun fld => do pure { fld with type := ← f fld.type }) + instanceProcedures := ← ct.instanceProcedures.mapM (mapProcedureHighTypesM f) }) + | .Constrained ct => + pure (.Constrained { ct with + base := ← f ct.base + constraint := ← mapStmtExprHighTypesM f ct.constraint + witness := ← mapStmtExprHighTypesM f ct.witness }) + | .Datatype dt => + pure (.Datatype { dt with + constructors := ← dt.constructors.mapM (fun ctor => do + pure { ctor with args := ← ctor.args.mapM (fun p => do pure { p with type := ← f p.type }) }) }) + | .Alias ta => pure (.Alias { ta with target := ← f ta.target }) + +/-- Apply `f` to a constant's declared type and (optional) initializer. -/ +def mapConstantHighTypesM [Monad m] (f : HighTypeMd → m HighTypeMd) (c : Constant) : m Constant := do + pure { c with type := ← f c.type, initializer := ← c.initializer.mapM (mapStmtExprHighTypesM f) } + +/-- Apply `f` to every `HighType` annotation anywhere in a program: procedures, + static fields, type definitions, and constants. -/ +def mapProgramHighTypesM [Monad m] (f : HighTypeMd → m HighTypeMd) (program : Program) : m Program := do + return { program with + staticProcedures := ← program.staticProcedures.mapM (mapProcedureHighTypesM f) + staticFields := ← program.staticFields.mapM (fun fld => do pure { fld with type := ← f fld.type }) + types := ← program.types.mapM (mapTypeDefinitionHighTypesM f) + constants := ← program.constants.mapM (mapConstantHighTypesM f) } + +/-- Pure version of `mapProgramHighTypesM`. -/ +def mapProgramHighTypes (f : HighTypeMd → HighTypeMd) (program : Program) : Program := + mapProgramHighTypesM (m := Id) f program + end -- public section end Strata.Laurel diff --git a/Strata/Languages/Laurel/ModifiesClauses.lean b/Strata/Languages/Laurel/ModifiesClauses.lean index f2fcc0a791..d162e764ff 100644 --- a/Strata/Languages/Laurel/ModifiesClauses.lean +++ b/Strata/Languages/Laurel/ModifiesClauses.lean @@ -126,7 +126,7 @@ def buildModifiesEnsures (proc: Procedure) (model: SemanticModel) (modifiesExprs -- Build: antecedent ==> heapUnchanged let implBody := mkMd <| .PrimitiveOp .Implies [antecedent, heapUnchanged] -- Build: forall $obj: Composite, $fld: Field => ... - let innerForall := mkMd <| .Quantifier .Forall ⟨ fldName, { val := .TTypedField { val := .TInt, source := none }, source := none } ⟩ none implBody + let innerForall := mkMd <| .Quantifier .Forall ⟨ fldName, { val := .UserDefined "Field", source := none } ⟩ none implBody let outerForall : StmtExprMd := { val := .Quantifier .Forall ⟨ objName, { val := .UserDefined "Composite", source := none } ⟩ none innerForall, source := proc.name.source } some outerForall diff --git a/Strata/Languages/Laurel/Resolution.lean b/Strata/Languages/Laurel/Resolution.lean index 7f81346fd1..cf32780f2b 100644 --- a/Strata/Languages/Laurel/Resolution.lean +++ b/Strata/Languages/Laurel/Resolution.lean @@ -338,9 +338,6 @@ def resolveHighType (ty : HighTypeMd) : ResolveM HighTypeMd := do | none => false -- name not defined: resolveRef already reported it if kindOk then pure (HighType.UserDefined ref') else pure HighType.Unknown - | .TTypedField vt => - let vt' ← resolveHighType vt - pure (.TTypedField vt') | .TSet et => let et' ← resolveHighType et pure (.TSet et') @@ -582,30 +579,26 @@ That list is bound on entry to a procedure body (by every other rule is independent of it. Several constructs are *statements*: their job is to have an effect, -not to produce a value. Their check rules accept whatever type the -surrounding context expects — the rule is written with the expected -type `A` left as a free variable (we call this **check at any `A`**), -which just means the rule does not look at `A` at all. There are two -reasons a construct ignores `A`: - -- It is a **control-flow terminator** (`Exit`, `Return`): it jumps - somewhere else and never hands a value back, so whatever the - context wanted, the jump satisfies it vacuously. `if c then 5 else - return` is fine in an `Int` context because the `else` branch never - produces anything at all. -- It runs and then **falls through without a value** (`Assert`, - `Assume`, `While`, `Var-Declare`). These conceptually have the unit - type `TVoid`; accepting any `A` is a slight over-acceptance that is - harmless in practice because such statements only ever appear in - non-last (discard) position, which is checked at `TVoid` anyway. +not to produce a value. They are handled by `Synth.resolveStmtExpr` +and synthesize `TVoid`: + +- **Control-flow terminators** (`Exit`, `Return`): they jump somewhere + else and never hand a value back. +- **Effect-only forms** (`Assert`, `Assume`, `While`, `Var-Declare`): + they run and fall through without producing a value. + +In either case, `Check.statement` (the `⋄` judgment) simply +synthesizes and discards the type, so any expression — including +value-producing ones like calls — is admitted in statement position. `Assign` is the one statement that *does* produce a value: it synthesizes the type of its right-hand side (so `x := e` can be used where that type is expected), and its check rule skips the \[⇐\] Sub boundary check only when the expected type is `TVoid` — i.e. when the assignment is used purely for effect. `Block` routes the surrounding -expected type to its last statement (the block's value), not to the -non-last statements (which are effects, checked at `TVoid`). +expected type to its last statement (the block's value); non-last +statements are in effect position (synthesized and discarded via +`Check.statement`). Each typing rule is implemented as its own helper inside the mutual block below. Helpers are grouped by section to mirror the *Typing @@ -629,9 +622,7 @@ rules* index in `LaurelDoc.lean`: - Holes — `Check.holeSome`, `Check.holeNone` The dispatch functions `Synth.resolveStmtExpr` and `Check.resolveStmtExpr` -pattern-match on the constructor and delegate to the corresponding helper. -`Synth.resolveStmtExpr` is non-total: constructors without a synthesis rule -hit a wildcard arm that emits a diagnostic and returns `Unknown`. -/ +pattern-match on the constructor and delegate to the corresponding helper. -/ namespace Resolution @@ -652,10 +643,8 @@ mutual /-- Synth-mode resolution: resolve `e` and synthesize its `HighType`, written `Γ ⊢ e ⇒ T`. Each constructor with a synthesis rule delegates - to its rule's helper; constructors without one (statement-shaped - constructs like `While`, `Exit`, `Return`, …) hit - a wildcard arm that emits a `typeMismatch` diagnostic and - returns `Unknown` to suppress cascading errors. + to its rule's helper. Statement-shaped constructs (`While`, `Exit`, + `Return`, `Assert`, `Assume`, `Var-Declare`) synthesize `TVoid`. Synthesis returns a type inferred from the expression itself; checking (`Check.resolveStmtExpr`) verifies that the expression has @@ -725,12 +714,24 @@ def Synth.resolveStmtExpr (exprMd : StmtExprMd) : ResolveM (StmtExprMd × HighTy | .Hole det (some ty) => let ty' ← resolveHighType ty pure (.Hole det (some ty'), ty') - | _ => - let unknown : HighTypeMd := { val := .Unknown, source := source } - typeMismatch source (some expr) - "this expression's type cannot be synthesized; try to annotate it or use it in a context where there is an expected type" - unknown - pure (expr, unknown) + | .Var (.Declare param) => do + let r ← Check.varDeclare param source + return (r, ⟨ .TVoid, source ⟩) + | .While cond invs dec body => do + let r ← Check.while exprMd cond invs dec body source (by rw [h_node]) + return (r, ⟨ .TVoid, source ⟩) + | .Exit target => do + let r ← Check.exit target source + return (r, ⟨ .TVoid, source ⟩) + | .Return val => do + let r ← Check.return exprMd val source (by rw [h_node]) + return (r, ⟨ .TVoid, source ⟩) + | .Assert ⟨condExpr, summary, free⟩ => do + let r ← Check.assert exprMd condExpr summary free source (by rw [h_node]) + return (r, ⟨ .TVoid, source ⟩) + | .Assume cond => do + let r ← Check.assume exprMd cond source (by rw [h_node]) + return (r, ⟨ .TVoid, source ⟩) return ({ val := val', source := source }, ty) termination_by (exprMd, 2) decreasing_by all_goals first @@ -779,16 +780,6 @@ def Check.resolveStmtExpr (exprMd : StmtExprMd) (expected : HighTypeMd) : Resolv Check.assign exprMd targets value expected source (by rw [h_node]) | .Hole det none => pure (Check.holeNone det expected source) | .Hole det (some ty) => Check.holeSome det ty expected source - | .Var (.Declare param) => Check.varDeclare param source - | .While cond invs dec body => - Check.while exprMd cond invs dec body source (by rw [h_node]) - | .Exit target => Check.exit target source - | .Return val => - Check.return exprMd val source (by rw [h_node]) - | .Assert ⟨condExpr, summary, free⟩ => - Check.assert exprMd condExpr summary free source (by rw [h_node]) - | .Assume cond => - Check.assume exprMd cond source (by rw [h_node]) | .Old val => Check.old exprMd val expected source (by rw [h_node]) | .ProveBy val proof => @@ -911,14 +902,13 @@ def Synth.varField (exprMd : StmtExprMd) /-- (Var-Declare) ``` x ∉ dom(Γ) - ──────────────────────────────────────────── - Γ ⊢ Var (.Declare ⟨x, T_x⟩) ⇐ A ⊣ Γ, x : T_x + ──────────────────────────────────────────────────── + Γ ⊢ Var (.Declare ⟨x, T_x⟩) ⇒ TVoid ⊣ Γ, x : T_x ``` `⊣ Γ, x : T_x` records that the surrounding scope is extended with the new binding for the remainder of the enclosing block. The declaration itself does no work other than registering `x : T_x`, - and yields no value, so its rule accepts whatever type `A` the - context expects (the rule ignores `A`). + and yields no value, so it synthesizes `TVoid`. `x ∉ dom(Γ)` is a soft side condition, not a hard premise: when `x` is already bound in the current scope, `defineNameCheckDup` emits a @@ -942,15 +932,14 @@ def Check.varDeclare (param : Parameter) (source : Option FileRange) : Numeric U Γ ⊢ body ⇐ Unknown ───────────────────────────────────────────────── - Γ ⊢ While cond invs decreases body ⇐ A + Γ ⊢ While cond invs decreases body ⇒ TVoid ``` `cond` is checked against `TBool`, and each invariant against `TBool`. The body's *value type* is discarded — control either re-enters the loop or falls through, so the body is checked at `Unknown` (the gradual wildcard) and any value the body's tail might produce is ignored. A loop is a statement: it yields no - value, so its rule accepts whatever type `A` the context expects - (the rule ignores `A`). + value, so it synthesizes `TVoid`. The optional `decreases` clause is synthesized and required to have a numeric type, via the same `Numeric U` predicate @@ -989,15 +978,11 @@ def Check.while (exprMd : StmtExprMd) ``` l ∈ Γ_lbl ─────────────────── - Γ ⊢ Exit l ⇐ A + Γ ⊢ Exit l ⇒ TVoid ``` `exit` is a control-flow terminator — an unconditional jump out of the enclosing labeled block. Because it never falls through, it - never delivers a value, so the rule accepts whatever type `A` the - context expects (the rule ignores `A`): an `exit` slots into any - position, even one expecting a value, since control leaves before - any value would be needed. Anything after `exit l` in the same - block is dead code, flagged by `Resolution.Check.block`. + never delivers a value, so it synthesizes `TVoid`. The premise `l ∈ Γ_lbl` requires the target label to name an enclosing labeled block; labels live in their own namespace @@ -1021,19 +1006,19 @@ def Check.exit (target : String) (source : Option FileRange) : ``` T_o-bar = [] (Return-None-Void) ───────────────────────── - Γ ⊢ Return none ⇐ A + Γ ⊢ Return none ⇒ TVoid - T_o-bar = [T] TVoid <:~ T (Return-None-Single) + T_o-bar = [T] (Return-None-Single) ────────────────────────────────── - Γ ⊢ Return none ⇐ A + Γ ⊢ Return none ⇒ TVoid T_o-bar = [T_1;…;T_n] n ≥ 2 (Return-None-Multi) ────────────────────────────────── - Γ ⊢ Return none ⇐ A + Γ ⊢ Return none ⇒ TVoid T_o-bar = [T] Γ ⊢ e ⇐ T (Return-Some) ────────────────────────────────── - Γ ⊢ Return (some e) ⇐ A + Γ ⊢ Return (some e) ⇒ TVoid T_o-bar = [] (Return-Void-Error) ─────────────────────────────────────────────────────────── @@ -1044,27 +1029,22 @@ def Check.exit (target : String) (source : Option FileRange) : Γ ⊢ Return (some e) ↝ "multi-output procedure cannot use 'return e'; assign to named outputs instead" ``` `return` is the *only* rule whose premises depend on the enclosing - procedure's declared outputs. Like `Exit`, it is a control-flow - terminator: it transfers control out of the enclosing procedure and - never falls through to the surrounding block, so the rule accepts - whatever type `A` the context expects (the rule ignores `A`). The - returned value, if any, is checked against the procedure's declared - output rather than against `A`. Anything after `return` in the same - block is dead code, flagged by `Resolution.Check.block`. + procedure's declared outputs. It is a control-flow terminator: it + transfers control out of the enclosing procedure and never falls + through, so it synthesizes `TVoid`. The returned value, if any, is + checked against the procedure's declared output. Anything after + `return` in the same block is dead code, flagged by + `Resolution.Check.block`. When `answerType = none` we are not inside any procedure body (e.g. resolving a constant initializer), so all `Return` checks are skipped — `Return` should not occur there in well-formed input. - `return;` synthesizes the missing payload as `TVoid`. In a - single-output procedure it is then required to subtype the declared - output (Return-None-Single's `TVoid <:~ T` premise) — accepted in - void-returning procedures, rejected in `int`/`bool`/etc. ones, - closing the soundness gap that the Dafny-style early-exit shorthand - used to leave open. In a void-output procedure it is unconditionally - accepted (Return-None-Void); in a multi-output procedure it is also - accepted (Return-None-Multi) and acts as an early-exit shorthand — - each declared output retains whatever was last assigned to it via + `return;` (no payload) is unconditionally accepted in all cases: + void-output procedures (Return-None-Void), single-output procedures + (Return-None-Single), and multi-output procedures (Return-None-Multi). + In the multi-output case it acts as an early-exit shorthand — each + declared output retains whatever was last assigned to it via named-output assignment. `return e` is checked against the declared output type in the @@ -1089,10 +1069,7 @@ def Check.return (exprMd : StmtExprMd) | _ => let (e', _) ← Synth.resolveStmtExpr a.val; pure e') match val, expectedReturn with | none, some [] => pure () - | none, some [singleOutput] => - -- `return;` synthesizes the missing payload as `TVoid`; require it to - -- be a consistent subtype of the declared output. - checkSubtype source singleOutput { val := .TVoid, source := source } + | none, some [singleOutput] => pure () | none, some _ => pure () | some _, some [] => let diag := diagnosticFromSource source @@ -1127,7 +1104,7 @@ def Check.return (exprMd : StmtExprMd) The empty block has a fixed type `TVoid`. This is the only block-level rule that synthesizes unconditionally: non-empty blocks are typed structurally by `Resolution.Check.block` (last statement - carries the value, non-last positions `⇐ TVoid` or Discard-Call), + carries the value, non-last positions via `Check.statement`), which always splits off a last statement and so never reaches an empty list. When an empty block appears in check position, `Resolution.Check.resolveStmtExpr`'s wildcard arm synth-then-subsumes @@ -1135,40 +1112,33 @@ def Check.return (exprMd : StmtExprMd) def Synth.emptyBlock (source : Option FileRange) : HighTypeMd := { val := .TVoid, source := source } -/-- (Discard) Check a statement in *effect position*, written `Γ ⊢ s ⋄`. +/-- (Synth-Discard) Check a statement in *effect position*, written `Γ ⊢ s ⋄`. Laurel has no syntactic statement/expression split — everything is a `StmtExpr` — so "what may appear where its value is discarded" is - defined by this rule rather than by the grammar. A statement `s` is - admitted in effect position iff one of: - - * **`Γ ⊢ s ⇐ TVoid`** — `s` checks against `TVoid`. Every - statement-shaped form lands here: `Var-Declare`, `Assign`, `Assert`, - `Assume`, `While`, the terminators `Exit`/`Return` (whose check - rules are polymorphic in the expected type), an `IfThenElse` with - void branches, and a nested void `Block`. A stranded *value* — a - literal `5`, a variable load `x`, a comparison `a < b`, a `new`, a - value-producing `IfThenElse` — fails this check (its type is not - consistent with `TVoid`) and is reported as dead code. - - * **Discard-Call / Discard-IncrDecr** — `s` is a call - (`StaticCall`/`InstanceCall`) or an `IncrDecr` (`x++`/`--x`). The - expression is synthesized and its result dropped, so the - `list.add(x);` idiom type-checks even when the callee returns a - value, and a bare `x++;` is admitted even though `++` synthesizes - the (non-void) target type. These are the value-producing forms - admitted in effect position: their effects are the point and their - results are incidental. + defined by this rule rather than by the grammar. Every expression in + statement position is synthesized and its type discarded: + + ``` + Γ ⊢ s ⇒ _ + ────────────── + Γ ⊢ s ⋄ + ``` + + Statement-shaped forms (`Var-Declare`, `Assign`, `Assert`, `Assume`, + `While`, `Exit`, `Return`) synthesize `TVoid`; value-producing forms + (calls, `IncrDecr`, literals, etc.) synthesize their natural type, + which is then discarded. This means any expression is accepted in + statement position — the `f(x);` idiom works regardless of `f`'s + return type, and `x++;` is admitted even though `++` synthesizes the + target's type. This is the single definition of "what counts as a statement". It is used by `Check.block` for every non-last statement, and for the last statement when the block itself sits in statement position (`expected = TVoid`). -/ def Check.statement (s : StmtExprMd) : ResolveM StmtExprMd := do - match s.val with - | .StaticCall .. | .InstanceCall .. | .IncrDecr .. => - let (s', _) ← Synth.resolveStmtExpr s; pure s' - | _ => Check.resolveStmtExpr s { val := .TVoid, source := s.source } + let (s', _) ← Synth.resolveStmtExpr s; pure s' termination_by (s, 4) decreasing_by all_goals (apply Prod.Lex.right; decide) @@ -1179,25 +1149,19 @@ def Check.statement (s : StmtExprMd) : ResolveM StmtExprMd := do statement list into `[s₁; … ; sₙ]` (all but the last) and `last`, handling each part as follows: - * **non-last — `Γ ⊢ s ⇐ TVoid`.** A non-last statement is a pure - effect, so it is checked at `TVoid`. This admits every statement - form (`Var-Declare`, `Assign`, `Assert`, `Assume`, `While`, - `Exit`, `Return`, `IfThenElse`), since each either yields no - value or — for the terminators `Exit`/`Return` — accepts any - expected type, and rejects a stranded value expression like `5;`, - whose `TInt` is not consistent with `TVoid`. The one - **Discard-Call** carve-out: a call (`StaticCall`/`InstanceCall`) - is synthesized and its result dropped, so the standard - `list.add(x);` discard idiom is allowed even when the callee - returns a value. + * **non-last — `Γ ⊢ s ⋄`.** A non-last statement is in effect + position: it is synthesized and its type discarded (see + `Check.statement`). Any expression is accepted — statement-shaped + forms synthesize `TVoid`, value-producing forms (calls, + `IncrDecr`, etc.) synthesize their natural type which is then + discarded. * **last — `Γ ⊢ last ⇐ T`.** The surrounding expected type `T` is routed to the last statement, so a check-only trailing form (`IfThenElse`, a nested `Block`, `Hole`, `Return`, …) still - receives its expected type. The same Discard-Call carve-out - applies when `T = TVoid` (a trailing `foo()` in statement - position discards its result, so `{ …; foo() }` type-checks as a - statement even when `foo` returns a value). + receives its expected type. When `T = TVoid` (the block is in + statement position), the last statement is also in effect position + and goes through `Check.statement`. A block most often occurs in check position (procedure bodies, branches, loop bodies, assignment RHS, and call arguments all supply @@ -1216,13 +1180,13 @@ def Check.block (exprMd : StmtExprMd) (expected : HighTypeMd) (source : Option FileRange) (h : exprMd.val = .Block stmts label) : ResolveM StmtExprMd := do -- A non-last statement is in effect position: admitted by `Check.statement` - -- (`Γ ⊢ s ⋄` — checks at `TVoid`, with the Discard-Call carve-out for calls). + -- (`Γ ⊢ s ⋄` — synthesized and the type discarded). let checkNonLast (s : StmtExprMd) (_h_mem : s ∈ stmts) : ResolveM StmtExprMd := Check.statement s -- The last statement carries the block's value: push `expected` in (so -- check-only forms are reachable). When the block itself sits in statement -- position (`expected = TVoid`), the last statement is also in effect - -- position and goes through `Check.statement` (same Discard-Call carve-out). + -- position and goes through `Check.statement`. let checkLast (s : StmtExprMd) (_h_mem : s ∈ stmts) : ResolveM StmtExprMd := do match expected.val with | .TVoid => Check.statement s @@ -1388,13 +1352,12 @@ def Synth.ifThenElse (exprMd : StmtExprMd) ``` Synth-mode rule for a non-empty block used where no expected type is available (e.g. `{ x := 1; x } == y`). Mirrors `Check.block`'s - structure — fresh scope, optional label, non-last statements checked - in effect position (`Check.statement`, i.e. at `TVoid` with the - Discard-Call carve-out), dead-code-after-terminator diagnostic — but - *synthesizes* the last statement instead of checking it against an - expected type, and returns that synthesized type as the block's value - type. The empty block is handled by `Synth.emptyBlock` at the - dispatch site; this rule only runs on a non-empty block. -/ + structure — fresh scope, optional label, non-last statements in + effect position (`Check.statement`), dead-code-after-terminator + diagnostic — but *synthesizes* the last statement instead of checking + it against an expected type, and returns that synthesized type as the + block's value type. The empty block is handled by `Synth.emptyBlock` + at the dispatch site; this rule only runs on a non-empty block. -/ def Synth.block (exprMd : StmtExprMd) (stmts : List StmtExprMd) (label : Option String) (source : Option FileRange) @@ -1444,11 +1407,10 @@ def Synth.block (exprMd : StmtExprMd) ``` Γ ⊢ cond ⇐ TBool ────────────────────────────────── - Γ ⊢ Assert cond ⇐ A + Γ ⊢ Assert cond ⇒ TVoid ``` `cond` is checked against `TBool`. `assert` is a statement: it - yields no value, so the rule accepts whatever type `A` the context - expects (the rule ignores `A`). -/ + yields no value, so it synthesizes `TVoid`. -/ def Check.assert (exprMd : StmtExprMd) (condExpr : StmtExprMd) (summary : Option String) (free : Bool) (source : Option FileRange) @@ -1468,11 +1430,10 @@ def Check.assert (exprMd : StmtExprMd) ``` Γ ⊢ cond ⇐ TBool ────────────────────────────────── - Γ ⊢ Assume cond ⇐ A + Γ ⊢ Assume cond ⇒ TVoid ``` `cond` is checked against `TBool`. `assume` is a statement: it - yields no value, so the rule accepts whatever type `A` the context - expects (the rule ignores `A`). -/ + yields no value, so it synthesizes `TVoid`. -/ def Check.assume (exprMd : StmtExprMd) (cond : StmtExprMd) (source : Option FileRange) (h : exprMd.val = .Assume cond) : @@ -1693,6 +1654,32 @@ def Synth.staticCall (exprMd : StmtExprMd) (callee : Identifier) (args : List StmtExprMd) (source : Option FileRange) (h : exprMd.val = .StaticCall callee args) : ResolveM (StmtExpr × HighTypeMd) := do + + -- Hack because we use these polymorphic map primitives but Laurel does not + -- support polymorphism yet, so they cannot be type-checked against their + -- placeholder `int` signatures. Instead we resolve the arguments and infer the + -- result type structurally from them, keeping a concrete `HighType` flowing into + -- Core translation: + -- * `select(map, key)` ⇒ the map's value type + -- * `update(map, key, val)` ⇒ the map type itself + -- * `const(val)` ⇒ `Map _ (typeof val)` (key type is not recoverable) + if callee == "select" || callee == "update" || callee == "const" then + let resolved ← args.attach.mapM (fun ⟨a, hMem⟩ => do + have := hMem + Synth.resolveStmtExpr a) + let args' := resolved.map (·.1) + let argTys := resolved.map (·.2) + let resultTy : HighTypeMd ← + match callee, argTys with + | "select", mapTy :: _ => + match mapTy.val with + | .TMap _ valueTy => pure valueTy + | _ => pure ⟨ .Unknown, source ⟩ + | "update", mapTy :: _ => pure mapTy + | "const", valTy :: _ => pure ⟨ .TMap ⟨.UserDefined "TypeTag", source⟩ valTy, source ⟩ + | _, _ => pure ⟨ .Unknown, source ⟩ + return (.StaticCall callee args', resultTy) + let callee' ← resolveRef callee source (expected := #[.parameter, .staticProcedure, .datatypeConstructor, .datatypeDestructor, .constant]) let (retTy, paramTypes) ← getCallInfo callee @@ -1719,12 +1706,13 @@ def Synth.staticCall (exprMd : StmtExprMd) pure (.StaticCall callee' args', retTy) termination_by (exprMd, 1) decreasing_by - apply Prod.Lex.left - have hsz := exprMd.sizeOf_val_lt - rw [h] at hsz - simp only [StmtExpr.StaticCall.sizeOf_spec] at hsz - have := List.sizeOf_lt_of_mem ‹_ ∈ args› - omega + all_goals + apply Prod.Lex.left + have hsz := exprMd.sizeOf_val_lt + rw [h] at hsz + simp only [StmtExpr.StaticCall.sizeOf_spec] at hsz + have := List.sizeOf_lt_of_mem ‹_ ∈ args› + omega /-- Cases on the arity of the callee's declared outputs. ``` @@ -2615,58 +2603,37 @@ def resolveParameter (param : Parameter) : ResolveM Parameter := do let name' ← defineNameCheckDup param.name (.parameter ⟨param.name, ty'⟩) return ⟨name', ty'⟩ -/-- Resolve a procedure body, checking its impl block (if any) against - `expected`. The expected type comes from the procedure's declared - output: a single output `T` for single-output functional procedures, - `Unknown` otherwise. Bodies without an impl block (`Abstract`, `External`) ignore - `expected`. -/ -def resolveBody (body : Body) (expected : HighTypeMd) : ResolveM Body := do +/-- Resolve a procedure body by synthesizing its impl block (if any). + Bodies without an impl block (`Abstract`, `External`) resolve + postconditions only. -/ +def resolveBody (body : Body) : ResolveM Body := do match body with | .Transparent b => - let b' ← Check.resolveStmtExpr b expected + let (b', _) ← Synth.resolveStmtExpr b return .Transparent b' | .Opaque posts impl mods => let posts' ← posts.mapM (·.mapM resolveStmtExpr) - let impl' ← impl.mapM (Check.resolveStmtExpr · expected) + let impl' ← impl.mapM Synth.resolveStmtExpr let mods' ← mods.mapM resolveStmtExpr - return .Opaque posts' impl' mods' + return .Opaque posts' (impl'.map (fun t => t.1)) mods' | .Abstract posts => let posts' ← posts.mapM (·.mapM resolveStmtExpr) return .Abstract posts' | .External => return .External -/-- Compute the expected *value type* `A` for a procedure body, i.e. - the `A` in `Γ ⊢ body ⇐ A`. Functional procedures with a single - output `T` expect `A = T`: the body's last statement is the result - and must produce a `T`. Non-functional procedures expect - `A = Unknown`: their body is run as a statement and the last - statement's value (if any) is discarded — outputs are observed via - `return e` (whose payload is matched against the procedure's - declared outputs by `Resolution.Check.return`) or via named-output - assignment. - - This computes only the body's value type. The procedure's declared - output list is bound separately by the procedure rule - (`resolveProcedure` / `resolveInstanceProcedure`) into - `ResolveState.answerType`. -/ -private def procedureBodyType (isFunctional : Bool) (outputs : List Parameter) - (source : Option FileRange) : HighTypeMd := - match isFunctional, outputs with - | true, [singleOutput] => singleOutput.type - | _, _ => { val := .Unknown, source := source } - /-- (Procedure) ``` - T_o-bar = proc.outputs.types A = procedureBodyType proc - Γ_global, params(proc) ⊢ proc.body ⇐ A + T_o-bar = proc.outputs.types + Γ_global, params(proc) ⊢ proc.body ⇒ _ ────────────────────────────────────────────────────────── Γ_global ⊢ Procedure proc ``` - The body is resolved under a scope that includes the procedure's - input and output parameters, and is checked against the value type - `A` computed by `procedureBodyType`. The Return rules consult the - procedure's declared output list `T_o-bar` (stored on - `ResolveState.answerType`, set on entry and restored on exit). -/ + The body is synthesized (not checked against a computed expected + type) under a scope that includes the procedure's input and output + parameters. Outputs are matched only via `return e` (checked against + the declared output by `Check.return`) or via named-output + assignment. The procedure's declared output list `T_o-bar` is stored + on `ResolveState.answerType`, set on entry and restored on exit. -/ def resolveProcedure (proc : Procedure) : ResolveM Procedure := do let procName' ← resolveRef proc.name withScope do @@ -2676,12 +2643,11 @@ def resolveProcedure (proc : Procedure) : ResolveM Procedure := do let dec' ← proc.decreases.mapM resolveStmtExpr let savedAnswer := (← get).answerType modify fun s => { s with answerType := some (outputs'.map (·.type)) } - let bodyExpected := procedureBodyType proc.isFunctional outputs' proc.name.source -- Pre-register the implicit `bodyLabel` block that the LaurelToCore -- translator wraps every body in (`Core.Statement.block bodyLabel …`), -- so that frontends emitting `Exit bodyLabel` for early-return lowering -- (e.g. PythonToLaurel) don't trip Check.exit's label-scope check. - let body' ← withLabel (some bodyLabel) <| resolveBody proc.body bodyExpected + let body' ← withLabel (some bodyLabel) <| resolveBody proc.body modify fun s => { s with answerType := savedAnswer } -- Transparent (static) procedure bodies are supported (#1215): the -- TransparencyPass derives a functional `$asFunction` copy, and the @@ -2720,9 +2686,8 @@ def resolveInstanceProcedure (typeName : Identifier) (proc : Procedure) : Resolv let dec' ← proc.decreases.mapM resolveStmtExpr let savedAnswer := (← get).answerType modify fun s => { s with answerType := some (outputs'.map (·.type)) } - let bodyExpected := procedureBodyType proc.isFunctional outputs' proc.name.source -- See `resolveProcedure` for the rationale on `bodyLabel`. - let body' ← withLabel (some bodyLabel) <| resolveBody proc.body bodyExpected + let body' ← withLabel (some bodyLabel) <| resolveBody proc.body modify fun s => { s with answerType := savedAnswer } if !proc.isFunctional && body'.isTransparent && !proc.name.text.any (· == '$') then let diag := diagnosticFromSource proc.name.source @@ -2815,7 +2780,6 @@ private def collectHighType (map : Std.HashMap Nat ResolvedNode) (ty : HighTypeM match ty with | AstNode.mk val _ => match val with - | .TTypedField vt => collectHighType map vt | .TSet et => collectHighType map et | .TMap kt vt => let map := collectHighType map kt diff --git a/Strata/Languages/Laurel/TypeAliasElim.lean b/Strata/Languages/Laurel/TypeAliasElim.lean index 1aa069e5f0..36c5426613 100644 --- a/Strata/Languages/Laurel/TypeAliasElim.lean +++ b/Strata/Languages/Laurel/TypeAliasElim.lean @@ -39,7 +39,6 @@ partial def resolveAliasType (amap : AliasMap) (ty : HighTypeMd) else match amap.get? name.text with | some target => resolveAliasType amap target (visited.insert name.text) | none => ty - | .TTypedField vt => { val := .TTypedField (resolveAliasType amap vt visited), source := ty.source } | .TSet et => { val := .TSet (resolveAliasType amap et visited), source := ty.source } | .TMap kt vt => { val := .TMap (resolveAliasType amap kt visited) (resolveAliasType amap vt visited), source := ty.source } @@ -52,69 +51,14 @@ partial def resolveAliasType (amap : AliasMap) (ty : HighTypeMd) { val := .Intersection (tys.map (resolveAliasType amap · visited)), source := ty.source } | _ => ty -def resolveAliasVariable (amap : AliasMap) (v : VariableMd) : VariableMd := - match v.val with - | .Declare param => ⟨.Declare { param with type := resolveAliasType amap param.type }, v.source⟩ - | _ => v - -/-- Resolve aliases in expression type positions. -/ -def resolveAliasExprNode (amap : AliasMap) (expr : StmtExprMd) : StmtExprMd := - match expr.val with - | .Assign targets value => - ⟨.Assign (targets.map (resolveAliasVariable amap)) value, expr.source⟩ - | .Var (.Declare param) => - ⟨.Var (.Declare { param with type := resolveAliasType amap param.type }), expr.source⟩ - | .Quantifier mode param trigger body => - { val := .Quantifier mode { param with type := resolveAliasType amap param.type } trigger body, source := expr.source } - | .AsType t ty => { val := .AsType t (resolveAliasType amap ty), source := expr.source } - | .IsType t ty => { val := .IsType t (resolveAliasType amap ty), source := expr.source } - | _ => expr - -def resolveAliasInProc (amap : AliasMap) (proc : Procedure) : Procedure := - let resolve := mapStmtExpr (resolveAliasExprNode amap) - let resolveBody : Body → Body := fun body => match body with - | .Transparent b => .Transparent (resolve b) - | .Opaque ps impl modif => .Opaque (ps.map (·.mapCondition resolve)) (impl.map resolve) (modif.map resolve) - | .Abstract ps => .Abstract (ps.map (·.mapCondition resolve)) - | .External => .External - { proc with - body := resolveBody proc.body - inputs := proc.inputs.map fun p => { p with type := resolveAliasType amap p.type } - outputs := proc.outputs.map fun p => { p with type := resolveAliasType amap p.type } - preconditions := proc.preconditions.map (·.mapCondition resolve) - decreases := proc.decreases.map resolve - invokeOn := proc.invokeOn.map resolve } - -def resolveAliasInType (amap : AliasMap) (td : TypeDefinition) : TypeDefinition := - match td with - | .Composite ct => - .Composite { ct with - fields := ct.fields.map fun f => { f with type := resolveAliasType amap f.type } - instanceProcedures := ct.instanceProcedures.map (resolveAliasInProc amap) } - | .Constrained ct => - let resolve := mapStmtExpr (resolveAliasExprNode amap) - .Constrained { ct with - base := resolveAliasType amap ct.base - constraint := resolve ct.constraint - witness := resolve ct.witness } - | .Datatype dt => - .Datatype { dt with - constructors := dt.constructors.map fun ctor => - { ctor with args := ctor.args.map fun p => { p with type := resolveAliasType amap p.type } } } - | .Alias _ => td -- will be removed - -/-- Eliminate all type aliases from a program. Replaces `UserDefined` references - with the alias target (transitively) and removes `.Alias` entries from `program.types`. -/ +/-- Eliminate all type aliases from a program. Replaces every `UserDefined` + reference (in any type position, via `mapProgramHighTypes`) with the alias + target (transitively) and removes `.Alias` entries from `program.types`. -/ public def typeAliasElim (_model : SemanticModel) (program : Program) : Program := let amap := buildAliasMap program.types if amap.isEmpty then program else - { program with - staticProcedures := program.staticProcedures.map (resolveAliasInProc amap) - staticFields := program.staticFields.map fun f => { f with type := resolveAliasType amap f.type } - types := (program.types.filter fun | .Alias _ => false | _ => true).map (resolveAliasInType amap) - constants := program.constants.map fun c => { c with - type := resolveAliasType amap c.type - initializer := c.initializer.map (mapStmtExpr (resolveAliasExprNode amap)) } } + let program := mapProgramHighTypes (resolveAliasType amap) program + { program with types := program.types.filter fun | .Alias _ => false | _ => true } /-- Pipeline pass: type alias elimination. -/ public def typeAliasElimPass : LaurelPass where diff --git a/Strata/Languages/Laurel/TypeHierarchy.lean b/Strata/Languages/Laurel/TypeHierarchy.lean index 599fc40492..7ada70ac30 100644 --- a/Strata/Languages/Laurel/TypeHierarchy.lean +++ b/Strata/Languages/Laurel/TypeHierarchy.lean @@ -123,6 +123,26 @@ private def rewriteTypeHierarchyNode (exprMd : StmtExprMd) : THM StmtExprMd := d | .IsType target ty => return lowerIsType target ty exprMd.source | _ => return exprMd +/-- +Rewrite a type so that every reference to a composite type (a name in +`composites`) becomes the flattened `Composite` datatype. After the type +hierarchy pass all composite values are represented by `Composite` references, +so their *static* types must follow suit; otherwise re-resolution sees a +`Pixel`-typed value flowing into a `Composite`-typed slot (`readField`, +`Composite..ref!`, an allocation `new C`, …). Recurses through compound types. -/ +partial def compositeRefToComposite (composites : Std.HashSet String) (ty : HighTypeMd) : HighTypeMd := + match ty.val with + | .UserDefined name => + if composites.contains name.text then { ty with val := .UserDefined "Composite" } else ty + | .TSet et => { ty with val := .TSet (compositeRefToComposite composites et) } + | .TMap kt vt => + { ty with val := .TMap (compositeRefToComposite composites kt) (compositeRefToComposite composites vt) } + | .Applied base args => + { ty with val := .Applied (compositeRefToComposite composites base) (args.map (compositeRefToComposite composites ·)) } + | .Pure base => { ty with val := .Pure (compositeRefToComposite composites base) } + | .Intersection tys => { ty with val := .Intersection (tys.map (compositeRefToComposite composites ·)) } + | _ => ty + /-- Type hierarchy transformation pass (Laurel → Laurel). @@ -152,16 +172,25 @@ def typeHierarchyTransform (model: SemanticModel) (program : Program) : Program else c } else td | _ => td - { program with - staticProcedures := procs', - types := [typeTagDatatype] ++ remainingTypes, - constants := program.constants ++ typeHierarchyConstants } + let transformed : Program := + { program with + staticProcedures := procs', + types := [typeTagDatatype] ++ remainingTypes, + constants := program.constants ++ typeHierarchyConstants } + -- Now that `New`/`IsType` have been lowered (they needed the original + -- composite names), flatten every remaining composite reference type to the + -- `Composite` datatype so the program re-resolves consistently. The + -- program-wide `HighType` traversal lives in `MapStmtExpr` so that every + -- type position is covered uniformly. + let compositeSet : Std.HashSet String := + compositeNames.foldl (init := {}) (·.insert ·) + mapProgramHighTypes (compositeRefToComposite compositeSet) transformed /-- Pipeline pass: type hierarchy transform. -/ public def typeHierarchyTransformPass : LaurelPass where name := "TypeHierarchyTransform" documentation := "Encodes the object-oriented type hierarchy (inheritance, dynamic dispatch, type tests, and casts) into explicit operations on a flat representation. Composite types with parents are flattened, and dynamic dispatch is resolved through type-test chains." - needsResolves := true + needsResolves := false -- Only resolve again after completing HeapParam, ModifiesClauses and TypeHierarchy. These are logically one pass. run := fun p m => (typeHierarchyTransform m p, [], {}) diff --git a/Strata/Util/FileRange.lean b/Strata/Util/FileRange.lean index ce6da121ea..cea135549b 100644 --- a/Strata/Util/FileRange.lean +++ b/Strata/Util/FileRange.lean @@ -18,7 +18,7 @@ abbrev SourceRange.none := StrataDDM.SourceRange.none inductive Uri where | file (path: String) - deriving DecidableEq, Repr, Inhabited + deriving DecidableEq, Repr, Inhabited, Hashable instance : Std.ToFormat Uri where format fr := private match fr with | .file path => path @@ -26,7 +26,7 @@ instance : Std.ToFormat Uri where structure FileRange where file: Uri range: SourceRange - deriving DecidableEq, Repr, Inhabited + deriving DecidableEq, Repr, Inhabited, Hashable instance : Std.ToFormat FileRange where format fr := private f!"{fr.file}:{fr.range}" @@ -76,7 +76,7 @@ def FileRange.format (fr : FileRange) (fileMap : Option Lean.FileMap) (includeEn f!"{baseName}({fr.range.start}-{fr.range.stop})" inductive DiagnosticType where | Warning | UserError | NotYetImplemented | StrataBug - deriving Repr, BEq, Inhabited, Lean.ToExpr + deriving Repr, BEq, Inhabited, Lean.ToExpr, Hashable /-- A diagnostic model that holds a file range and a message. This can be converted to a formatted string using a FileMap. -/ @@ -84,7 +84,7 @@ structure DiagnosticModel where fileRange : FileRange message : String type : DiagnosticType - deriving Repr, BEq, Inhabited + deriving Repr, BEq, Inhabited, Hashable instance : Inhabited DiagnosticModel where default := { fileRange := FileRange.unknown, message := "", type := .UserError } diff --git a/StrataDDM/StrataDDM/Util/SourceRange.lean b/StrataDDM/StrataDDM/Util/SourceRange.lean index e1107f82f9..78bcd84efb 100644 --- a/StrataDDM/StrataDDM/Util/SourceRange.lean +++ b/StrataDDM/StrataDDM/Util/SourceRange.lean @@ -25,7 +25,7 @@ structure SourceRange where start : String.Pos.Raw /-- One past the end of the range. -/ stop : String.Pos.Raw -deriving DecidableEq, Inhabited, Repr +deriving DecidableEq, Inhabited, Repr, Hashable namespace SourceRange diff --git a/StrataPython/StrataPython/PythonToLaurel.lean b/StrataPython/StrataPython/PythonToLaurel.lean index a8cdbc64aa..199963fa40 100644 --- a/StrataPython/StrataPython/PythonToLaurel.lean +++ b/StrataPython/StrataPython/PythonToLaurel.lean @@ -2731,8 +2731,6 @@ def getHighTypeName : Laurel.HighType → String | .TString => "string" | .TVoid => "void" | .TFloat64 => "real" - | .THeap => "Heap" - | .TTypedField _ => "Field" | .TCore s => s | .UserDefined name => name.text | .TSet _ => "Map" diff --git a/StrataPython/StrataPythonTest/ToLaurelTest.lean b/StrataPython/StrataPythonTest/ToLaurelTest.lean index cb693b450b..f44e423ba5 100644 --- a/StrataPython/StrataPythonTest/ToLaurelTest.lean +++ b/StrataPython/StrataPythonTest/ToLaurelTest.lean @@ -64,8 +64,6 @@ private def fmtHighType : HighType → String | .TReal => "TReal" | .TFloat64 => "TFloat64" | .TString => "TString" - | .THeap => "THeap" - | .TTypedField _ => "TTypedField" | .TSet _ => "TSet" | .TMap _ _ => "TMap" | .UserDefined name => s!"UserDefined({name})" diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressionsError.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressionsError.lean index 41e05dc33c..d1e67ff6f6 100644 --- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressionsError.lean +++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressionsError.lean @@ -34,8 +34,9 @@ function functionWithMutatingAssignment(x: int): int function functionWithWhile(x: int): int { - while(false) {} + while(false) {}; //^^^^^^^^^^^^^^^ error: loops are not supported in functions or contracts + 3 }; function functionCallingHasMutationAssignment(x: int): int { diff --git a/StrataTest/Languages/Laurel/ResolutionTypeCheckTests.lean b/StrataTest/Languages/Laurel/ResolutionTypeCheckTests.lean index dfb6e79568..e3888db451 100644 --- a/StrataTest/Languages/Laurel/ResolutionTypeCheckTests.lean +++ b/StrataTest/Languages/Laurel/ResolutionTypeCheckTests.lean @@ -16,6 +16,18 @@ open Strata /-! ## Non-boolean conditions -/ +#eval testLaurelResolution <| +#strata +program Laurel; + +procedure voidReturn(x: int) + returns (r: int) +{ + r := 1; + return +}; +#end + #eval testLaurelResolution <| #strata program Laurel; @@ -82,20 +94,20 @@ function cmp(x: string, y: int): bool { #eval testLaurelResolution <| #strata program Laurel; -procedure foo() opaque { +procedure invalidAssignment() opaque { var x: int := true // ^^^^ error: expected 'int', got 'bool' }; #end -/-! ## Function return type checks -/ +/-! ## Procedure return type checks -/ #eval testLaurelResolution <| #strata program Laurel; -function foo(): int { - true -//^^^^ error: expected 'int', got 'bool' +procedure foo(): int { + return true +// ^^^^ error: expected 'int', got 'bool' }; #end diff --git a/StrataTest/Util/TestLaurel.lean b/StrataTest/Util/TestLaurel.lean index 577c3b47e2..933f320c11 100644 --- a/StrataTest/Util/TestLaurel.lean +++ b/StrataTest/Util/TestLaurel.lean @@ -262,6 +262,16 @@ def testLaurel (block : SourcedProgram) (options : LaurelVerifyOptions := defaultLaurelTestOptions) : IO Unit := runAndCheck block (runLaurelPipelineRaw · options) +/-- Path to the directory for intermediate files, inside the build directory. + Resolved from the current working directory so it works on any machine. -/ +def buildDir : IO String := do + let cwd ← IO.currentDir + return s!"{cwd}/.lake/build/intermediatePrograms/" + +def testLaurelKeepIntermediates (block : SourcedProgram) : IO Unit := do + let dir ← buildDir + runAndCheck block (runLaurelPipelineRaw · { translateOptions := { keepAllFilesPrefix := dir}}) + /-- Like `testLaurel` but skips SMT verification (translate + resolve only). Use when the test only cares about resolution, not the verifier — e.g. "shadowing in nested blocks is OK", or asserting a specific resolution diff --git a/docs/verso/LaurelDoc.lean b/docs/verso/LaurelDoc.lean index 891eef33a7..eedf40093d 100644 --- a/docs/verso/LaurelDoc.lean +++ b/docs/verso/LaurelDoc.lean @@ -228,7 +228,7 @@ implementation introduces that have no surface syntax. The {name Strata.Laurel.HighType}`HighType` type enumerates every type Laurel tracks. Alongside the user-writable types it also includes internal constructors -(such as `THeap`, `Unknown`, and `MultiValuedExpr`) that the compiler introduces +(such as `Unknown` and `MultiValuedExpr`) that the compiler introduces during resolution and later passes; these have no surface syntax. {docstring Strata.Laurel.HighType} @@ -379,15 +379,15 @@ The Index below links to each construct's subsection. - {ref "rules-subsumption"}[*Subsumption*] — \[⇐\] Sub - {ref "rules-literals"}[*Literals*] — \[⇒\] Lit-Int, \[⇒\] Lit-Bool, \[⇒\] Lit-String, \[⇒\] Lit-Decimal -- {ref "rules-variables"}[*Variables*] — \[⇒\] Var-Local, \[⇒\] Var-Field, \[⇐\] Var-Declare +- {ref "rules-variables"}[*Variables*] — \[⇒\] Var-Local, \[⇒\] Var-Field, \[⇒\] Var-Declare - {ref "rules-control-flow"}[*Control flow*] — \[⇐\] If, \[⇐\] If-NoElse, \[⇒\] If-Synth, \[⇒\] If-Synth-NoElse; - \[⇐\] Block, \[⇒\] Block-Synth, \[⋄\] Stmt, \[⋄\] Discard-Call, - \[⇒\] Empty-Block; \[⇐\] Exit; - \[⇐\] Return-None-Void, \[⇐\] Return-None-Single, \[⇐\] Return-None-Multi, - \[⇐\] Return-Some, \[⇐\] Return-Void-Error, - \[⇐\] Return-Multi-Error; \[⇐\] While -- {ref "rules-verification-statements"}[*Verification statements*] — \[⇐\] Assert, \[⇐\] Assume + \[⇐\] Block, \[⇒\] Block-Synth, \[⋄\] Synth-Discard, + \[⇒\] Empty-Block; \[⇒\] Exit; + \[⇒\] Return-None-Void, \[⇒\] Return-None-Single, \[⇒\] Return-None-Multi, + \[⇒\] Return-Some, \[⇒\] Return-Void-Error, + \[⇒\] Return-Multi-Error; \[⇒\] While +- {ref "rules-verification-statements"}[*Verification statements*] — \[⇒\] Assert, \[⇒\] Assume - {ref "rules-assignment"}[*Assignment*] — \[⇒\] Assign, \[⇐\] Assign - {ref "rules-calls"}[*Calls*] — \[⇒\] Static-Call, \[⇒\] Static-Call-Multi, \[⇒\] Instance-Call, \[⇒\] Instance-Call-Multi @@ -447,7 +447,7 @@ $$`\frac{\Gamma \vdash e \Rightarrow \_ \quad \Gamma(f) = T_f}{\Gamma \vdash \ma {docstring Strata.Laurel.Resolution.Synth.varField} -$$`\frac{x \notin \mathrm{dom}(\Gamma)}{\Gamma \vdash \mathsf{Var}\;(\mathsf{.Declare}\;\langle x, T_x\rangle) \Leftarrow A \quad \dashv \quad \Gamma, x : T_x} \quad \text{([⇐] Var-Declare)}` +$$`\frac{x \notin \mathrm{dom}(\Gamma)}{\Gamma \vdash \mathsf{Var}\;(\mathsf{.Declare}\;\langle x, T_x\rangle) \Rightarrow \mathsf{TVoid} \quad \dashv \quad \Gamma, x : T_x} \quad \text{([⇒] Var-Declare)}` $`x \notin \mathrm{dom}(\Gamma)` is a soft side condition rather than a hard premise: when $`x` is already bound in the current scope the rule still @@ -519,25 +519,19 @@ $`\mathit{last}\;\diamond` rather than $`\mathit{last} \Leftarrow $`\{\ldots;\,\mathit{foo}()\}` type-checks as a statement even when `foo` returns a non-void type. -The effect-position judgment $`\Gamma \vdash s\;\diamond` admits a -statement in one of two ways: +The effect-position judgment $`\Gamma \vdash s\;\diamond` synthesizes +the statement and discards the result: -$$`\frac{\Gamma \vdash s \Leftarrow \mathsf{TVoid} \;\dashv\; \Gamma'}{\Gamma \vdash s \;\diamond \;\dashv\; \Gamma'} \quad \text{([⋄] Stmt)}` +$$`\frac{\Gamma \vdash s \Rightarrow \_ \;\dashv\; \Gamma'}{\Gamma \vdash s \;\diamond \;\dashv\; \Gamma'} \quad \text{([⋄] Synth-Discard)}` -$$`\frac{s = \mathsf{StaticCall}\;\ldots \lor s = \mathsf{InstanceCall}\;\ldots \quad \Gamma \vdash s \Rightarrow \_}{\Gamma \vdash s \;\diamond \;\dashv\; \Gamma} \quad \text{([⋄] Discard-Call)}` - -\[⋄\] Stmt admits every statement form (`Var-Declare`, `Assign`, -`Assert`, `Assume`, `While`, `Exit`, `Return`, `IfThenElse`): each -either yields no value — so $`\mathsf{TVoid}` is exactly right — or, for -the terminators `Exit`/`Return`, accepts *any* expected type (their -rules leave the value type free — see \[⇐\] Exit and the Return rules -below — because control leaves before any value is needed). A stranded -value such as `5;` fails it, since $`\mathsf{TInt}` is not consistent -with $`\mathsf{TVoid}`. \[⋄\] Discard-Call is the one carve-out for a -value-producing form: a call is synthesized and its result dropped, so -the standard `f(x);` idiom is allowed even when `f` returns a value. -These two are the only block-level cases that aren't already -consequences of the rules for the individual statement forms. +Every expression in statement position is synthesized and its type +discarded. Statement-shaped forms (`Var-Declare`, `Assign`, `Assert`, +`Assume`, `While`, `Exit`, `Return`) synthesize $`\mathsf{TVoid}`; +value-producing forms (calls, `IncrDecr`, literals, etc.) synthesize +their natural type, which is then discarded. This means any expression +is accepted in statement position — the `f(x);` idiom works regardless +of `f`'s return type, and `x++;` is admitted even though `++` +synthesizes the target's type. Only `Var (.Declare …)` actually extends the scope $`\Gamma_i`; every other statement leaves it unchanged. The block opens a fresh nested @@ -569,21 +563,18 @@ $`\mathsf{TVoid} <: \mathit{expected}`). {docstring Strata.Laurel.Resolution.Check.block} -The $`\Gamma \vdash s\;\diamond` judgment — the \[⋄\] Stmt / \[⋄\] -Discard-Call carve-out above — is the single definition of what counts -as a statement in effect position, factored out into +The $`\Gamma \vdash s\;\diamond` judgment — the \[⋄\] Synth-Discard +rule above — is the single definition of what counts as a statement in +effect position, factored out into {name Strata.Laurel.Resolution.Check.statement}`Check.statement`: {docstring Strata.Laurel.Resolution.Check.statement} -$$`\frac{l \in \Gamma_{\mathrm{lbl}}}{\Gamma \vdash \mathsf{Exit}\;l \Leftarrow A} \quad \text{([⇐] Exit)}` +$$`\frac{l \in \Gamma_{\mathrm{lbl}}}{\Gamma \vdash \mathsf{Exit}\;l \Rightarrow \mathsf{TVoid}} \quad \text{([⇒] Exit)}` `exit` is an unconditional jump out of the enclosing labeled block. -Because control leaves before any value is needed, the rule accepts -*any* expected value type $`A` — it leaves $`A` free, with no -$`\mathsf{TVoid}` side condition — so an `exit` slots into any -position, even one expecting a value. Labels live in their own -namespace $`\Gamma_{\mathrm{lbl}}`, populated by the surrounding +It synthesizes $`\mathsf{TVoid}` unconditionally. Labels live in their +own namespace $`\Gamma_{\mathrm{lbl}}`, populated by the surrounding `Block` rule when its $`\mathit{label}` is `some l`. An $`\mathsf{Exit}\;l` targeting a label not in $`\Gamma_{\mathrm{lbl}}` is rejected. @@ -594,40 +585,37 @@ In the Return rules below, $`\overline{T_o}` denotes the declared output-parameter type list of the enclosing procedure (an implicit parameter of the rules — the procedure binds it once on entry). -$$`\frac{\overline{T_o} = []}{\Gamma \vdash \mathsf{Return}\;\mathsf{none} \Leftarrow A} \quad \text{([⇐] Return-None-Void)}` +$$`\frac{\overline{T_o} = []}{\Gamma \vdash \mathsf{Return}\;\mathsf{none} \Rightarrow \mathsf{TVoid}} \quad \text{([⇒] Return-None-Void)}` -$$`\frac{\overline{T_o} = [T] \quad \mathsf{TVoid} <:_\sim T}{\Gamma \vdash \mathsf{Return}\;\mathsf{none} \Leftarrow A} \quad \text{([⇐] Return-None-Single)}` +$$`\frac{\overline{T_o} = [T]}{\Gamma \vdash \mathsf{Return}\;\mathsf{none} \Rightarrow \mathsf{TVoid}} \quad \text{([⇒] Return-None-Single)}` -$$`\frac{\overline{T_o} = [T_1; \ldots; T_n] \quad (n \ge 2)}{\Gamma \vdash \mathsf{Return}\;\mathsf{none} \Leftarrow A} \quad \text{([⇐] Return-None-Multi)}` +$$`\frac{\overline{T_o} = [T_1; \ldots; T_n] \quad (n \ge 2)}{\Gamma \vdash \mathsf{Return}\;\mathsf{none} \Rightarrow \mathsf{TVoid}} \quad \text{([⇒] Return-None-Multi)}` -$$`\frac{\overline{T_o} = [T] \quad \Gamma \vdash e \Leftarrow T}{\Gamma \vdash \mathsf{Return}\;(\mathsf{some}\;e) \Leftarrow A} \quad \text{([⇐] Return-Some)}` +$$`\frac{\overline{T_o} = [T] \quad \Gamma \vdash e \Leftarrow T}{\Gamma \vdash \mathsf{Return}\;(\mathsf{some}\;e) \Rightarrow \mathsf{TVoid}} \quad \text{([⇒] Return-Some)}` -$$`\frac{\overline{T_o} = []}{\Gamma \vdash \mathsf{Return}\;(\mathsf{some}\;e) \rightsquigarrow \text{error: “void procedure cannot return a value”}} \quad \text{([⇐] Return-Void-Error)}` +$$`\frac{\overline{T_o} = []}{\Gamma \vdash \mathsf{Return}\;(\mathsf{some}\;e) \rightsquigarrow \text{error: “void procedure cannot return a value”}} \quad \text{([⇒] Return-Void-Error)}` -$$`\frac{\overline{T_o} = [T_1; \ldots; T_n] \quad (n \ge 2)}{\Gamma \vdash \mathsf{Return}\;(\mathsf{some}\;e) \rightsquigarrow \text{error: “multi-output procedure cannot use 'return e'; assign to named outputs instead”}} \quad \text{([⇐] Return-Multi-Error)}` +$$`\frac{\overline{T_o} = [T_1; \ldots; T_n] \quad (n \ge 2)}{\Gamma \vdash \mathsf{Return}\;(\mathsf{some}\;e) \rightsquigarrow \text{error: “multi-output procedure cannot use 'return e'; assign to named outputs instead”}} \quad \text{([⇒] Return-Multi-Error)}` `return` is the only rule whose premises depend on the enclosing -procedure's declared outputs. The conclusion's value type $`A` is left -free — the rule accepts any expected type — because `return` is a -control-flow terminator: it never falls through, so it can stand in -any position, even one expecting a value. The returned value (if any) -is checked against the procedure's declared output, not against $`A`. -The error arms fire when $`\overline{T_o}`'s arity does not match the -syntactic shape of `return e`. +procedure's declared outputs. The rule synthesizes $`\mathsf{TVoid}` +because `return` is a control-flow terminator: it never falls through +and produces no value for the surrounding context. The returned value +(if any) is checked against the procedure's declared output. The error +arms fire when $`\overline{T_o}`'s arity does not match the syntactic +shape of `return e`. Regardless of which arm fires, $`e` is always elaborated — it is checked against the declared output in the single-output case, otherwise synthesized — so any errors inside $`e` are reported in addition to the arity diagnostic. -The three Return-None rules treat the missing payload as having type -$`\mathsf{TVoid}`. Void-output procedures accept it unconditionally -(Return-None-Void); single-output procedures require -$`\mathsf{TVoid} <:_\sim T` (Return-None-Single), accepting void -returns and rejecting `return;` in an `int`/`bool`/etc. procedure; -multi-output procedures accept it as an early-exit shorthand that -leaves the named outputs at whatever they were last assigned to -(Return-None-Multi). +The three Return-None rules all accept `return;` unconditionally. +Void-output procedures accept it naturally (Return-None-Void); +single-output procedures accept it without a subtype check +(Return-None-Single); multi-output procedures accept it as an +early-exit shorthand that leaves the named outputs at whatever they +were last assigned to (Return-None-Multi). When the surrounding context has no enclosing procedure body (e.g. inside a constant initializer), `answerType = none` and all Return @@ -635,13 +623,12 @@ checks are skipped; well-formed input never produces this case. {docstring Strata.Laurel.Resolution.Check.return} -$$`\frac{\Gamma \vdash \mathit{cond} \Leftarrow \mathsf{TBool} \quad \Gamma \vdash \mathit{invs}_i \Leftarrow \mathsf{TBool} \quad \Gamma \vdash \mathit{decreases} \Rightarrow U \quad \mathsf{Numeric}\;U \quad \Gamma \vdash \mathit{body} \Leftarrow \mathsf{Unknown}}{\Gamma \vdash \mathsf{While}\;\mathit{cond}\;\mathit{invs}\;\mathit{decreases}\;\mathit{body} \Leftarrow A} \quad \text{([⇐] While)}` +$$`\frac{\Gamma \vdash \mathit{cond} \Leftarrow \mathsf{TBool} \quad \Gamma \vdash \mathit{invs}_i \Leftarrow \mathsf{TBool} \quad \Gamma \vdash \mathit{decreases} \Rightarrow U \quad \mathsf{Numeric}\;U \quad \Gamma \vdash \mathit{body} \Leftarrow \mathsf{Unknown}}{\Gamma \vdash \mathsf{While}\;\mathit{cond}\;\mathit{invs}\;\mathit{decreases}\;\mathit{body} \Rightarrow \mathsf{TVoid}} \quad \text{([⇒] While)}` The body is checked at $`\mathsf{Unknown}`: control either re-enters the loop or falls through, so the body's value type is never observed by the surrounding context. A loop is a statement and yields no value, -so the rule accepts any expected type $`A` (it leaves $`A` free), -exactly like the other statement forms. +so the rule synthesizes $`\mathsf{TVoid}`. The optional $`\mathit{decreases}` clause is synthesized and required to have a numeric type via the same $`\mathsf{Numeric}` predicate @@ -658,11 +645,11 @@ the clause runs in synth mode rather than check mode. tag := "rules-verification-statements" %%% -$$`\frac{\Gamma \vdash \mathit{cond} \Leftarrow \mathsf{TBool}}{\Gamma \vdash \mathsf{Assert}\;\mathit{cond} \Leftarrow A} \quad \text{([⇐] Assert)}` +$$`\frac{\Gamma \vdash \mathit{cond} \Leftarrow \mathsf{TBool}}{\Gamma \vdash \mathsf{Assert}\;\mathit{cond} \Rightarrow \mathsf{TVoid}} \quad \text{([⇒] Assert)}` {docstring Strata.Laurel.Resolution.Check.assert} -$$`\frac{\Gamma \vdash \mathit{cond} \Leftarrow \mathsf{TBool}}{\Gamma \vdash \mathsf{Assume}\;\mathit{cond} \Leftarrow A} \quad \text{([⇐] Assume)}` +$$`\frac{\Gamma \vdash \mathit{cond} \Leftarrow \mathsf{TBool}}{\Gamma \vdash \mathsf{Assume}\;\mathit{cond} \Rightarrow \mathsf{TVoid}} \quad \text{([⇒] Assume)}` {docstring Strata.Laurel.Resolution.Check.assume} @@ -928,21 +915,19 @@ $$`\frac{}{\Gamma \vdash \mathsf{Hole}\;d\;(\mathsf{some}\;T_h) \Rightarrow T_h} tag := "rules-procedure" %%% -A procedure body is checked against an expected type $`A` and is -resolved under a scope that includes the procedure's input and output -parameters. The Return rules above refer to the same output list -$`\overline{T_o}` that the procedure binds here. +A procedure body is synthesized (not checked against a computed +expected type) and is resolved under a scope that includes the +procedure's input and output parameters. The Return rules above refer +to the same output list $`\overline{T_o}` that the procedure binds +here. -$$`\frac{\overline{T_o} = \mathit{proc}.\mathit{outputs}.\mathit{types} \quad A = \mathsf{procedureBodyType}(\mathit{proc}) \quad \Gamma_\mathit{global},\,\mathit{params}(\mathit{proc}) \vdash \mathit{proc}.\mathit{body} \Leftarrow A}{\Gamma_\mathit{global} \vdash \mathsf{Procedure}\;\mathit{proc}} \quad \text{(Procedure)}` +$$`\frac{\overline{T_o} = \mathit{proc}.\mathit{outputs}.\mathit{types} \quad \Gamma_\mathit{global},\,\mathit{params}(\mathit{proc}) \vdash \mathit{proc}.\mathit{body} \Rightarrow \_}{\Gamma_\mathit{global} \vdash \mathsf{Procedure}\;\mathit{proc}} \quad \text{(Procedure)}` -The body's value type $`A` is computed by `procedureBodyType`: a -single-output functional procedure expects $`A = T` (its body's last -statement is the result), while every other procedure expects -$`A = \mathsf{Unknown}` (its body is run as a statement and the last -statement's value is discarded; outputs are observed via `return e`, -matched against $`\overline{T_o}` by -{name Strata.Laurel.Resolution.Check.return}`Check.return`, or via -named-output assignment). +The body is synthesized and its type is discarded — there is no +constraint from the output list pushed into the body. Outputs are +matched only via `return e` (checked against $`\overline{T_o}` by +{name Strata.Laurel.Resolution.Check.return}`Check.return`) or via +named-output assignment. {docstring Strata.Laurel.resolveProcedure}