Exception Support Prototype

Strata/Languages/Laurel/CoreDefinitionsForLaurel.lean

@@ -49,6 +49,45 @@ def coreDefinitionsForLaurel : Program :=
   | .ok program => program
   | .error e => dbg_trace s!"BUG: CoreDefinitionsForLaurel parse error: {e}"; default
 
+/--
+E1: the exceptional-channel root for exception handling.
+See `docs/design/laurel_extensions.md` (extension E1).
+
+`BaseException` is the root of every value that travels on the exceptional
+channel; `throw`'s operand, a `catch` binding, and the `onThrow` binder are all
+typed `BaseException` (or a declared subtype). The prelude defines only the
+root: any catchable-vs-fatal tiering above it is front-end policy, expressed by
+which parent a front-end type `extends` plus the catch predicate.
+
+Unlike `coreDefinitionsForLaurel` (datatypes/functions that are "free" for SMT),
+`BaseException` is a *composite* and therefore participates in the heap model.
+Injecting it into every program would perturb SMT heap reasoning for programs
+that do not use exceptions, so it is kept separate and prepended **only when a
+program references it** (see the pipeline's gating on `baseExceptionTypeName`).
+-/
+def exceptionDefinitionsForLaurelDDM :=
+#strata
+program Laurel;
+
+composite BaseException {
+  var message: string
+}
+
+datatype Result<Val, Err> {
+  Good(value: Val),
+  Bad(err: Err)
+}
+
+#end
+
+/--
+The E1 exception prelude as a `Laurel.Program`, parsed at compile time.
+-/
+def exceptionDefinitionsForLaurel : Program :=
+  match TransM.run none (parseProgram exceptionDefinitionsForLaurelDDM) with
+  | .ok program => program
+  | .error e => dbg_trace s!"BUG: ExceptionDefinitionsForLaurel parse error: {e}"; default
+
 end -- public section
 
 end Strata.Laurel

Strata/Languages/Laurel/FilterPrelude.lean

@@ -121,6 +121,20 @@ private partial def collectExprNames (expr : StmtExprMd) : CollectM Unit := do
     collectExprNames body
   | .Assert cond => collectExprNames cond.condition
   | .Assume cond => collectExprNames cond
+  -- A `throw` uses the exceptional channel, whose root `BaseException` must be
+  -- in scope wherever it appears. Recording it as a type reference drives both
+  -- the prelude gating and this dependency closure to include the exception
+  -- prelude for any program containing a `throw`.
+  | .Throw value => addTypeName baseExceptionTypeName; collectExprNames value
+  -- A `try`/`catch` likewise uses the exceptional channel (the catch binding is
+  -- typed `BaseException`), so record the root and recurse into every arm.
+  | .Try body catches finally? =>
+    addTypeName baseExceptionTypeName
+    collectExprNames body
+    catches.forM (fun c => do
+      c.predicate.forM collectExprNames
+      collectExprNames c.body)
+    finally?.forM collectExprNames
   | .Return val => val.forM collectExprNames
   | .Old val | .Fresh val | .Assigned val => collectExprNames val
   | .ProveBy val proof => collectExprNames val; collectExprNames proof
@@ -148,6 +162,14 @@ private def collectProcDeps (proc : Procedure) : CollectM Unit := do
   proc.preconditions.forM (collectExprNames ·.condition)
   proc.decreases.forM collectExprNames
   proc.invokeOn.forM collectExprNames
+  -- E4 exceptional contract: a declared `throws` type or any `onThrow` clause
+  -- uses the exceptional channel, whose root `BaseException` must be in scope;
+  -- recording it (and the throws type / onThrow predicate names) gates the
+  -- exception prelude in and keeps the relevant declarations.
+  if proc.throwsType.isSome || !proc.onThrow.isEmpty then
+    addTypeName baseExceptionTypeName
+  proc.throwsType.forM collectHighTypeNames
+  proc.onThrow.forM (collectExprNames ·.predicate)
   collectBodyNames proc.body
 
 /-- Collect all names referenced by a type definition. -/
@@ -264,6 +286,18 @@ private def collectProgramRefs (prog : Laurel.Program) : CollectState :=
     prog.staticProcedures.forM collectProcDeps
     prog.types.forM collectTypeDefDeps
 
+/-- The set of all names (procedure-call targets and type references) that a
+    user program refers to. Exposed so the compilation pipeline can decide
+    whether an optional, heap-participating prelude fragment (e.g. the E1
+    exception root `BaseException`) needs to be prepended — a fragment that
+    perturbs SMT heap reasoning when injected into programs that never use it.
+
+    Detecting a bare *subtype* reference works for free: the prelude defines only
+    the root, so any subtype is defined in the user program with an `extends`
+    chain that names the root, and `extends` targets are collected here. -/
+public def referencedNames (prog : Laurel.Program) : Std.HashSet String :=
+  (collectProgramRefs prog).allNames
+
 /-- Filter a prelude Laurel program to only include declarations
     transitively needed by the user program. -/
 public def filterPrelude (prelude user : Laurel.Program)

Strata/Languages/Laurel/Grammar/AbstractToConcreteTreeTranslator.lean

@@ -51,10 +51,13 @@ partial def highTypeValToArg : HighType → Arg
   | .TVoid => laurelOp "compositeType" #[ident "void"]
   -- 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;
-    -- emit the base type as a best-effort approximation
-    highTypeToArg base
+  | .Applied base args =>
+    -- Generic type application, e.g. `Option<int>`. Representable only when the
+    -- base is a named type (which is the only form the grammar produces).
+    match base.val with
+    | .UserDefined name =>
+      laurelOp "appliedType" #[ident name.text, commaSep (args.map highTypeToArg |>.toArray)]
+    | _ => highTypeToArg base
   | .Pure base => highTypeToArg base
   | .Intersection types =>
     match types with
@@ -167,6 +170,13 @@ where
         laurelOp "errorSummary" #[.strlit sr msg])
       laurelOp "assert" #[stmtExprToArg cond.condition, errOpt]
     | .Assume cond => laurelOp "assume" #[stmtExprToArg cond]
+    | .Throw value => laurelOp "throw" #[stmtExprToArg value]
+    | .Try body catches finally? =>
+      let catchArgs := catches.map (fun c =>
+        let guardArg := optionArg (c.predicate.map fun p => laurelOp "catchGuard" #[stmtExprToArg p])
+        laurelOp "catchClause" #[ident c.binding.text, guardArg, stmtExprToArg c.body]) |>.toArray
+      let finallyArg := optionArg (finally?.map fun f => laurelOp "finallyClause" #[stmtExprToArg f])
+      laurelOp "tryCatch" #[stmtExprToArg body, seqArg catchArgs, finallyArg]
     | .New name => laurelOp "new" #[ident name.text]
     | .This => laurelOp "identifier" #[ident "this"]
     | .IsType target ty =>
@@ -248,6 +258,14 @@ private def procedureToOp (proc : Procedure) : StrataDDM.Operation :=
       if proc.outputs.isEmpty then optionArg none
       else optionArg (some (laurelOp "returnParameters" #[commaSep (proc.outputs.map parameterToArg |>.toArray)]))
   let requiresArgs := proc.preconditions.map requiresClauseToArg |>.toArray
+  let throwsArg := optionArg (proc.throwsType.map fun t =>
+    laurelOp "throwsClause" #[highTypeToArg t])
+  let onThrowArgs := proc.onThrow.map (fun c =>
+    laurelOp "onThrowClause" #[ident c.binding.text, stmtExprToArg c.predicate]) |>.toArray
+  let onThrowsArgs := proc.onThrows.map (fun c =>
+    laurelOp "onThrowsClause" #[stmtExprToArg c.condition, ident c.binding.text, stmtExprToArg c.postcondition]) |>.toArray
+  let onThrowModifiesArgs := if proc.onThrowModifies.isEmpty then #[]
+    else #[laurelOp "onThrowModifiesClause" #[commaSep (proc.onThrowModifies.map stmtExprToArg |>.toArray)]]
   let invokeOnArg := optionArg (proc.invokeOn.map fun e =>
     laurelOp "invokeOnClause" #[stmtExprToArg e])
   let (opaqueSpecArg, bodyArg) := match proc.body with
@@ -271,8 +289,12 @@ private def procedureToOp (proc : Procedure) : StrataDDM.Operation :=
       returnTypeArg,
       returnParamsArg,
       seqArg requiresArgs,
+      throwsArg,
+      seqArg onThrowArgs,
+      seqArg onThrowsArgs,
       invokeOnArg,
       opaqueSpecArg,
+      seqArg onThrowModifiesArgs,
       bodyArg
     ] }
 
@@ -304,10 +326,12 @@ private def datatypeConstructorToArg (c : DatatypeConstructor) : Arg :=
 private def datatypeToOp (dt : DatatypeDefinition) : StrataDDM.Operation :=
   let ctors := dt.constructors.map datatypeConstructorToArg |>.toArray
   let ctorList := laurelOp "datatypeConstructorList" #[commaSep ctors]
+  let typeParamsArg := optionArg (if dt.typeArgs.isEmpty then none
+    else some (laurelOp "typeParams" #[commaSep (dt.typeArgs.map (fun p => ident p.text) |>.toArray)]))
   let datatypeOp : StrataDDM.Operation :=
     { ann := sr
       name := { dialect := "Laurel", name := "datatype" }
-      args := #[ident dt.name.text, ctorList] }
+      args := #[ident dt.name.text, typeParamsArg, ctorList] }
   { ann := sr
     name := { dialect := "Laurel", name := "datatypeCommand" }
     args := #[.op datatypeOp] }

Strata/Languages/Laurel/Grammar/ConcreteToAbstractTreeTranslator.lean

@@ -111,6 +111,12 @@ partial def translateHighType (arg : Arg) : TransM HighTypeMd := do
     | q`Laurel.compositeType, #[nameArg] =>
       let name ← translateIdent nameArg
       return mkHighTypeMd (.UserDefined name) src
+    | q`Laurel.appliedType, #[baseArg, argsArg] =>
+      let base ← translateIdent baseArg
+      let args ← match argsArg with
+        | .seq _ .comma args => args.toList.mapM translateHighType
+        | singleArg => do let a ← translateHighType singleArg; pure [a]
+      return mkHighTypeMd (.Applied (mkHighTypeMd (.UserDefined base) src) args) src
     | _, _ => TransM.error s!"translateHighType: unsupported type operator {repr op.name}"
   | _ => TransM.error s!"translateHighType expects operation"
 
@@ -203,6 +209,32 @@ partial def translateStmtExpr (arg : Arg) : TransM StmtExprMd := do
     | q`Laurel.assume, #[arg0] =>
       let cond ← translateStmtExpr arg0
       return mkStmtExprMd (.Assume cond) src
+    | q`Laurel.throw, #[arg0] =>
+      let value ← translateStmtExpr arg0
+      return mkStmtExprMd (.Throw value) src
+    | q`Laurel.tryCatch, #[bodyArg, catchSeqArg, finallyArg] =>
+      let body ← translateStmtExpr bodyArg
+      let catches ← match catchSeqArg with
+        | .seq _ _ clauses => clauses.toList.mapM fun arg => match arg with
+            | .op cOp => match cOp.name, cOp.args with
+              | q`Laurel.catchClause, #[bindingArg, guardArg, cBodyArg] => do
+                let binding ← translateIdent bindingArg
+                let predicate ← match guardArg with
+                  | .option _ (some (.op gOp)) => match gOp.name, gOp.args with
+                    | q`Laurel.catchGuard, #[pArg] => translateStmtExpr pArg >>= (pure ∘ some)
+                    | _, _ => pure none
+                  | _ => pure none
+                let cBody ← translateStmtExpr cBodyArg
+                pure ({ binding := binding, predicate := predicate, body := cBody } : CatchClause)
+              | _, _ => TransM.error "Expected catchClause"
+            | _ => TransM.error "Expected operation"
+        | _ => pure []
+      let finally? ← match finallyArg with
+        | .option _ (some (.op fOp)) => match fOp.name, fOp.args with
+          | q`Laurel.finallyClause, #[fBodyArg] => translateStmtExpr fBodyArg >>= (pure ∘ some)
+          | _, _ => pure none
+        | _ => pure none
+      return mkStmtExprMd (.Try body catches finally?) src
     | q`Laurel.block, #[arg0] =>
       let stmts ← translateSeqCommand arg0
       return mkStmtExprMd (.Block stmts none) src
@@ -504,9 +536,9 @@ def parseProcedure (arg : Arg) : TransM Procedure := do
 
   match op.name, op.args with
   | q`Laurel.procedure, #[nameArg, paramArg, returnTypeArg, returnParamsArg,
-      requiresArg, invokeOnArg, opaqueSpecArg, bodyArg]
+      requiresArg, throwsArg, onThrowArg, onThrowsArg, invokeOnArg, opaqueSpecArg, onThrowModifiesArg, bodyArg]
   | q`Laurel.function, #[nameArg, paramArg, returnTypeArg, returnParamsArg,
-      requiresArg, invokeOnArg, opaqueSpecArg, bodyArg] =>
+      requiresArg, throwsArg, onThrowArg, onThrowsArg, invokeOnArg, opaqueSpecArg, onThrowModifiesArg, bodyArg] =>
     let name ← translateIdent nameArg
     let parameters ← translateParameters paramArg
     -- Either returnTypeArg or returnParamsArg may have a value, not both
@@ -528,6 +560,51 @@ def parseProcedure (arg : Arg) : TransM Procedure := do
       | _ => TransM.error s!"Expected optionalReturnType operation, got {repr returnTypeArg}"
     -- Parse preconditions (requires clauses - zero or more)
     let preconditions ← translateRequiresClauses requiresArg
+    -- Parse optional `throws` type (E4)
+    let throwsType ← match throwsArg with
+      | .option _ (some (.op throwsOp)) => match throwsOp.name, throwsOp.args with
+        | q`Laurel.throwsClause, #[tyArg] => translateHighType tyArg >>= (pure ∘ some)
+        | _, _ => TransM.error s!"Expected throwsClause, got {repr throwsOp.name}"
+      | _ => pure none
+    -- Parse `onThrow` exceptional postconditions (E4 - zero or more)
+    let onThrow ← match onThrowArg with
+      | .seq _ _ clauses => clauses.toList.mapM fun arg => match arg with
+          | .op cOp => match cOp.name, cOp.args with
+            | q`Laurel.onThrowClause, #[bindingArg, predArg] => do
+              let binding ← translateIdent bindingArg
+              let predicate ← translateStmtExpr predArg
+              pure ({ binding := binding, predicate := predicate } : OnThrowClause)
+            | _, _ => TransM.error s!"Expected onThrowClause, got {repr cOp.name}"
+          | _ => TransM.error "Expected operation in onThrow sequence"
+      | _ => pure []
+    -- Parse `when C throws (e) P` exceptional behavior cases (E4 - zero or more)
+    let onThrows ← match onThrowsArg with
+      | .seq _ _ clauses => clauses.toList.mapM fun arg => match arg with
+          | .op cOp => match cOp.name, cOp.args with
+            | q`Laurel.onThrowsClause, #[condArg, bindingArg, postArg] => do
+              let condition ← translateStmtExpr condArg
+              let binding ← translateIdent bindingArg
+              let postcondition ← translateStmtExpr postArg
+              pure ({ condition := condition, binding := binding,
+                      postcondition := postcondition } : OnThrowsClause)
+            | _, _ => TransM.error s!"Expected onThrowsClause, got {repr cOp.name}"
+          | _ => TransM.error "Expected operation in onThrows sequence"
+      | _ => pure []
+    -- Parse `onThrow modifies …` exceptional-frame clauses (E4 - zero or more);
+    -- collect all their comma-separated refs into a single list.
+    let onThrowModifies ← match onThrowModifiesArg with
+      | .seq _ _ clauses => do
+        let mut all : List StmtExprMd := []
+        for arg in clauses do
+          match arg with
+          | .op cOp => match cOp.name, cOp.args with
+            | q`Laurel.onThrowModifiesClause, #[refsArg] =>
+              let refs ← translateModifiesExprs refsArg
+              all := all ++ refs
+            | _, _ => TransM.error s!"Expected onThrowModifiesClause, got {repr cOp.name}"
+          | _ => TransM.error "Expected operation in onThrowModifies sequence"
+        pure all
+      | _ => pure []
     -- Parse optional invokeOn clause
     let invokeOn ← match invokeOnArg with
       | .option _ (some (.op invokeOnOp)) => match invokeOnOp.name, invokeOnOp.args with
@@ -574,11 +651,15 @@ def parseProcedure (arg : Arg) : TransM Procedure := do
       decreases := none
       isFunctional := op.name == q`Laurel.function
       invokeOn := invokeOn
+      throwsType := throwsType
+      onThrow := onThrow
+      onThrows := onThrows
+      onThrowModifies := onThrowModifies
       body := procBody
     }
   | q`Laurel.procedure, args
   | q`Laurel.function, args =>
-    TransM.error s!"parseProcedure expects 8 arguments, got {args.size}"
+    TransM.error s!"parseProcedure expects 12 arguments, got {args.size}"
   | _, _ =>
     TransM.error s!"parseProcedure expects procedure or function, got {repr op.name}"
 
@@ -653,8 +734,16 @@ def parseDatatype (arg : Arg) : TransM TypeDefinition := do
   let .op op := arg
     | TransM.error s!"parseDatatype expects operation"
   match op.name, op.args with
-  | q`Laurel.datatype, #[nameArg, constructorsArg] =>
+  | q`Laurel.datatype, #[nameArg, typeParamsArg, constructorsArg] =>
     let name ← translateIdent nameArg
+    let typeArgs ← match typeParamsArg with
+      | .option _ (some (.op tpOp)) => match tpOp.name, tpOp.args with
+        | q`Laurel.typeParams, #[paramsArg] =>
+          match paramsArg with
+          | .seq _ .comma args => args.toList.mapM translateIdent
+          | singleArg => do let p ← translateIdent singleArg; pure [p]
+        | _, _ => TransM.error s!"Expected typeParams, got {repr tpOp.name}"
+      | _ => pure []
     let constructors ← match constructorsArg with
       | .op listOp => match listOp.name, listOp.args with
         | q`Laurel.datatypeConstructorList, #[csArg] =>
@@ -663,7 +752,7 @@ def parseDatatype (arg : Arg) : TransM TypeDefinition := do
           | singleArg => do let c ← parseDatatypeConstructor singleArg; pure [c]
         | _, _ => TransM.error s!"Expected datatypeConstructorList, got {repr listOp.name}"
       | _ => TransM.error s!"Expected datatypeConstructorList operation"
-    return .Datatype { name := name, typeArgs := [], constructors := constructors }
+    return .Datatype { name := name, typeArgs := typeArgs, constructors := constructors }
   | _, _ =>
     TransM.error s!"parseDatatype expects datatype, got {repr op.name}"
 

Strata/Languages/Laurel/Grammar/LaurelGrammar.lean

@@ -12,7 +12,7 @@ module
 -- Laurel dialect definition, loaded from LaurelGrammar.st
 -- NOTE: Changes to LaurelGrammar.st are not automatically tracked by the build system.
 -- Update this file (e.g. this comment) to trigger a recompile after modifying LaurelGrammar.st.
--- Last grammar change: renamed strConcat token to `^`; added preIncr/preDecr/postIncr/postDecr; `return` value is now Option StmtExpr (supports a valueless return).
+-- Last grammar change: `onThrow modifies …` exceptional-frame clause placed after the `opaque` block (next to the normal `modifies`).
 public import StrataDDM.AST
 import StrataDDM.BuiltinDialects.Init
 import StrataDDM.Integration.Lean.HashCommands