Remove functions

Strata/Languages/Laurel/ConstrainedTypeElim.lean

@@ -71,9 +71,9 @@ def constraintCallFor (ptMap : ConstrainedTypeMap) (ty : HighType)
     (varName : Identifier) (src : Option FileRange := none) : Option StmtExprMd :=
   constraintCallForExpr ptMap ty ⟨.Var (.Local varName), src⟩ src
 
-/-- Generate a constraint function for a constrained type.
-    For nested types, the function calls the parent's constraint function. -/
-def mkConstraintFunc (ptMap : ConstrainedTypeMap) (ct : ConstrainedType) : Procedure :=
+/-- Generate a constraint procedure for a constrained type.
+    For nested types, the procedure calls the parent's constraint procedure. -/
+def mkConstraintProc (ptMap : ConstrainedTypeMap) (ct : ConstrainedType) : Procedure :=
   let baseType := resolveType ptMap ct.base
   let bodyExpr: StmtExprMd := match ct.base.val with
     | .UserDefined parent =>
@@ -90,7 +90,6 @@ def mkConstraintFunc (ptMap : ConstrainedTypeMap) (ct : ConstrainedType) : Proce
     inputs := [{ name := ct.valueName, type := baseType }]
     outputs := [{ name := mkId "result", type := { val := .TBool, source := none } }]
     body := .Transparent { val := .Return bodyExpr, source := none }
-    isFunctional := true
     decreases := none
     preconditions := [] }
 
@@ -166,16 +165,15 @@ def elimProc (ptMap : ConstrainedTypeMap) (model : SemanticModel) (proc : Proced
   let inputRequires : List Condition := proc.inputs.filterMap fun p =>
     (constraintCallFor ptMap p.type.val p.name (src := p.type.source)).map
       fun c => { condition := c }
-  let outputEnsures : List Condition := if proc.isFunctional then [] else proc.outputs.filterMap fun p =>
+  let outputEnsures : List Condition := proc.outputs.filterMap fun p =>
     (constraintCallFor ptMap p.type.val p.name (src := p.type.source)).map
       fun c => { condition := ⟨c.val, p.type.source⟩ }
   let body' := match proc.body with
   | .Transparent bodyExpr =>
     let body := elimStmts ptMap model bodyExpr
     if outputEnsures.isEmpty then .Transparent body
     else
-      let retBody := if proc.isFunctional then ⟨.Return (some body), bodyExpr.source⟩ else body
-      .Opaque outputEnsures (some retBody) []
+      .Opaque outputEnsures (some body) []
   | .Opaque postconds impl modif =>
     let impl' := impl.map (elimStmts ptMap model)
     .Opaque (postconds ++ outputEnsures) impl' modif
@@ -206,7 +204,6 @@ private def mkWitnessProc (ptMap : ConstrainedTypeMap) (ct : ConstrainedType) :
     outputs := []
     body := .Opaque [] (some ⟨.Block [witnessInit, assert] none, src⟩) []
     preconditions := []
-    isFunctional := false
     decreases := none }
 
 /-- Eliminate constrained types within a composite type definition: resolve
@@ -227,21 +224,17 @@ public def constrainedTypeElim (model : SemanticModel) (program : Program)
   let ptMap := buildConstrainedTypeMap program.types
   if ptMap.isEmpty then (program, []) else
   let constraintFuncs := program.types.filterMap fun
-    | .Constrained ct => some (mkConstraintFunc ptMap ct) | _ => none
+    | .Constrained ct => some (mkConstraintProc ptMap ct) | _ => none
   let witnessProcedures := program.types.filterMap fun
     | .Constrained ct => some (mkWitnessProc ptMap ct) | _ => none
-  let funcDiags := program.staticProcedures.foldl (init := []) fun acc proc =>
-    if proc.isFunctional && proc.outputs.any (fun p => isConstrainedType ptMap p.type.val) then
-      acc.cons (diagnosticFromSource proc.name.source "constrained return types on functions are not yet supported")
-    else acc
   ({ program with
     staticProcedures := constraintFuncs ++ program.staticProcedures.map (elimProc ptMap model)
                         ++ witnessProcedures
     types := program.types.filterMap fun
       | .Constrained _ => none
       | .Composite ct => some (.Composite (elimCompositeType ptMap model ct))
       | other => some other },
-   funcDiags)
+   [])
 
 /-- Pipeline pass: constrained type elimination. -/
 public def constrainedTypeElimPass : LoweringPass where

Strata/Languages/Laurel/ContractPass.lean

@@ -67,7 +67,6 @@ private def mkConditionProc (name : String) (params : List Parameter)
     outputs := [⟨mkId "$result", { val := .TBool, source := none }⟩]
     preconditions := []
     decreases := none
-    isFunctional := true
     body := .Transparent condition.condition }
 
 /-- Suffix appended to a procedure's output-parameter names when they are lowered
@@ -123,7 +122,6 @@ private def mkPostConditionProc (name : String) (inputs outputs : List Parameter
     outputs := [⟨mkId "$result", { val := .TBool, source := none }⟩]
     preconditions := []
     decreases := none
-    isFunctional := true
     body := .Transparent (renameOutputsInPostExpr outputNames condition.condition) }
 
 /-- Information about a procedure's contracts. -/
@@ -142,7 +140,7 @@ private def collectContractInfo (procs : List Procedure) : Std.HashMap String Co
     let postconds := getPostconditions proc.body
     let hasPre := !proc.preconditions.isEmpty
     let hasPost := !postconds.isEmpty
-    if !proc.isFunctional && (hasPre || hasPost) then
+    if hasPre || hasPost then
       let preNames := proc.preconditions.zipIdx.map fun (c, i) =>
         (preCondProcName proc.name.text i, c.summary)
       let postNames := postconds.zipIdx.map fun (c, i) =>
@@ -162,19 +160,19 @@ private def transformProcBody (proc : Procedure) (info : ContractInfo) : Body :=
   let preAssumes : List StmtExprMd :=
     proc.preconditions.zip info.preNames |>.map fun (pc, name, _) =>
       ⟨.Assume (mkCall name inputArgs), pc.condition.source⟩
+  let postAsserts : List StmtExprMd :=
+    postconds.zip info.postNames |>.map fun (pc, _name, _summary) =>
+      let summary := pc.summary.getD "postcondition"
+      ⟨.Assert { condition := pc.condition, summary := some summary }, pc.condition.source⟩
   match proc.body with
   | .Transparent body =>
-    let postAsserts : List StmtExprMd :=
-      postconds.zip info.postNames |>.map fun (pc, _name, _summary) =>
-        let summary := pc.summary.getD "postcondition"
-        ⟨.Assert { condition := pc.condition, summary := some summary }, pc.condition.source⟩
     .Transparent ⟨.Block (preAssumes ++ [body] ++ postAsserts) none, body.source⟩
   | .Opaque _ (some impl) _ =>
-    .Opaque postconds (some ⟨.Block (preAssumes ++ [impl]) none, impl.source⟩) []
+    .Opaque [] (some ⟨.Block (preAssumes ++ [impl] ++ postAsserts) none, impl.source⟩) []
   | .Opaque _ none mods =>
-    .Opaque postconds none mods
+    .Opaque [] none mods
   | .Abstract _ =>
-    .Abstract postconds
+    .Abstract []
   | b => b
 
 /-- Monad used by the contract-pass rewriter; carries a global counter for
@@ -206,15 +204,12 @@ private def mkTempAssignments (args : List StmtExprMd)
   return (decls, refs)
 
 /-- Generate precondition checks (one per precondition) for a call site. -/
-private def mkPreChecks (info : ContractInfo) (isFunctional : Bool)
+private def mkPreChecks (info : ContractInfo)
     (tempRefs : List StmtExprMd) (src : Option FileRange) : List StmtExprMd :=
   if !info.hasPreCondition then []
   else info.preNames.map fun (name, summary) =>
     let call := mkCall name tempRefs
-    if isFunctional then
-      ⟨.Assume call, src⟩
-    else
-      ⟨.Assert { condition := call, summary := some (summary.getD "precondition") }, src⟩
+    ⟨.Assert { condition := call, summary := some (summary.getD "precondition") }, src⟩
 
 /-- Generate postcondition assumes (one per postcondition) for a call site. -/
 private def mkPostAssumes (info : ContractInfo)
@@ -249,12 +244,12 @@ private def mkCallArgs (info : ContractInfo) (origArgs tempRefs : List StmtExprM
 
 /-- Rewrite call sites in a statement/expression tree. -/
 private def rewriteCallSites (contractInfoMap : Std.HashMap String ContractInfo)
-    (isFunctional : Bool) (expr : StmtExprMd) : ContractM StmtExprMd := do
+    (expr : StmtExprMd) : ContractM StmtExprMd := do
   let rewriteStaticCall (callee : Identifier) (args : List StmtExprMd)
       (info : ContractInfo) (src : Option FileRange)
       : ContractM (List StmtExprMd) := do
     let (tempDecls, tempRefs) ← mkTempAssignments args info.inputParams src
-    let preCheck := mkPreChecks info isFunctional tempRefs src
+    let preCheck := mkPreChecks info tempRefs src
     let (callStmt, postAssume, returnValue) ←
       if info.hasPostCondition && !info.outputParams.isEmpty then do
         let mut outputTempDecls : List VariableMd := []
@@ -295,7 +290,7 @@ private def rewriteCallSites (contractInfoMap : Std.HashMap String ContractInfo)
             let (tempDecls, tempRefs) ← mkTempAssignments args' info.inputParams src
             let callArgs := mkCallArgs info args' tempRefs
             let callWithTemps : StmtExprMd := ⟨.Assign targets ⟨.StaticCall callee callArgs, callSrc⟩, src⟩
-            let preCheck := mkPreChecks info isFunctional tempRefs src
+            let preCheck := mkPreChecks info tempRefs src
             let outputArgs := targets.filterMap fun t =>
               match t.val with
               | .Local name => some (mkMd (.Var (.Local name)))
@@ -320,7 +315,7 @@ private def rewriteCallSites (contractInfoMap : Std.HashMap String ContractInfo)
 /-- Rewrite call sites in all bodies of a procedure. -/
 private def rewriteCallSitesInProc (contractInfoMap : Std.HashMap String ContractInfo)
     (proc : Procedure) : ContractM Procedure := do
-  let rw := rewriteCallSites contractInfoMap proc.isFunctional
+  let rw := rewriteCallSites contractInfoMap
   match proc.body with
   | .Transparent body =>
     let body' ← rw body
@@ -412,7 +407,7 @@ def lowerContracts (program : Program) : Program × List DiagnosticModel :=
   let diagnostics := program.staticProcedures.filterMap invokeOnOutputRefError
 
   -- Generate helper procedures for all procedures with contracts
-  let helperProcs := (program.staticProcedures.filter (fun proc => !proc.isFunctional)).flatMap fun proc =>
+  let helperProcs := program.staticProcedures.flatMap fun proc =>
     let postconds := getPostconditions proc.body
     let preProcs := proc.preconditions.zipIdx.map fun (c, i) =>
       mkConditionProc (preCondProcName proc.name.text i) proc.inputs c
@@ -423,28 +418,25 @@ def lowerContracts (program : Program) : Program × List DiagnosticModel :=
   -- Transform procedures: strip contracts, add assume/assert, rewrite call sites
   -- Run all call-site rewriting in a single ContractM to share the global counter.
   let (transformedProcs, _) := (program.staticProcedures.mapM fun (proc : Procedure) => do
-    if proc.isFunctional then
-      return proc
-    else
-      let proc : Procedure := match proc.invokeOn with
-        | some trigger =>
-          let postconds := getPostconditions proc.body
-          if postconds.isEmpty then { proc with invokeOn := none }
-          else if invokeOnOutputRefError proc |>.isSome then
-            -- Skip axiom generation; diagnostic already emitted
-            { proc with invokeOn := none }
-          else { proc with
-            axioms := [mkInvokeOnAxiom proc.inputs trigger proc.preconditions postconds]
-            invokeOn := none }
-        | none => proc
-      let proc : Procedure := match contractInfoMap.get? proc.name.text with
-        | some info =>
-          { proc with
-            preconditions := []
-            body := transformProcBody proc info }
-        | none => proc
-      -- Rewrite call sites in the procedure body
-      rewriteCallSitesInProc contractInfoMap proc).run 0
+    let proc : Procedure := match proc.invokeOn with
+      | some trigger =>
+        let postconds := getPostconditions proc.body
+        if postconds.isEmpty then { proc with invokeOn := none }
+        else if invokeOnOutputRefError proc |>.isSome then
+          -- Skip axiom generation; diagnostic already emitted
+          { proc with invokeOn := none }
+        else { proc with
+          axioms := [mkInvokeOnAxiom proc.inputs trigger proc.preconditions postconds]
+          invokeOn := none }
+      | none => proc
+    let proc : Procedure := match contractInfoMap.get? proc.name.text with
+      | some info =>
+        { proc with
+          preconditions := []
+          body := transformProcBody proc info }
+      | none => proc
+    -- Rewrite call sites in the procedure body
+    rewriteCallSitesInProc contractInfoMap proc).run 0
 
   ({ program with staticProcedures := helperProcs ++ transformedProcs }, diagnostics)
 

Strata/Languages/Laurel/CoreDefinitionsForLaurel.lean

@@ -35,13 +35,13 @@ datatype LaurelUnit { MkLaurelUnit() }
 // And remove the hacky filter in HeapParameterization
 datatype Box { MkBox() }
 
-function select(map: int, key: int) : Box
+procedure select(map: int, key: int) : Box
   external;
 
-function update(map: int, key: int, value: int) : Box
+procedure update(map: int, key: int, value: int) : Box
   external;
 
-function const(value: int) : Box
+procedure const(value: int) : Box
   external;
 
 #end

Strata/Languages/Laurel/CoreGroupingAndOrdering.lean

@@ -203,8 +203,14 @@ open Std (Format ToFormat)
 
 public section
 
+/-- Format a procedure as a function, replacing the leading "procedure" keyword with "function". -/
+private def formatAsFunction (proc : Procedure) : Format :=
+  let s := (ToFormat.format proc).pretty 100
+  let s := if s.startsWith "procedure" then "function" ++ s.drop "procedure".length else s
+  Format.text s
+
 def formatOrderedDecl : OrderedDecl → Format
-  | .funcs funcs _ => Format.joinSep (funcs.map ToFormat.format) "\n\n"
+  | .funcs funcs _ => Format.joinSep (funcs.map formatAsFunction) "\n\n"
   | .procedure proc => ToFormat.format proc
   | .datatypes dts => Format.joinSep (dts.map ToFormat.format) "\n\n"
   | .constant c => ToFormat.format c

Strata/Languages/Laurel/DesugarShortCircuit.lean

@@ -50,7 +50,8 @@ private def desugarShortCircuitNode (imperativeCallees : List String) (expr : St
 
 /-- Desugar short-circuit operators in a program. -/
 def desugarShortCircuit (program : Program) : Program :=
-  let imperativeCallees := (program.staticProcedures.filter (!·.isFunctional)).map (·.name.text)
+  let imperativeCallees := program.staticProcedures.map (·.name.text)
+  -- TODO shouldn't imperativeCallees always be empty here?
   mapProgram (mapStmtExpr (desugarShortCircuitNode imperativeCallees)) program
 
 end -- public section

Strata/Languages/Laurel/EliminateDeterministicHoles.lean

@@ -34,7 +34,7 @@ structure ElimHoleState where
 
 private abbrev ElimHoleM := StateM ElimHoleState
 
-/-- Generate a fresh uninterpreted function for a typed hole and return a call to it. -/
+/-- Generate a fresh uninterpreted procedure for a typed hole and return a call to it. -/
 private def mkHoleCall (source : Option FileRange) (holeType : HighTypeMd) : ElimHoleM StmtExprMd := do
   let s ← get
   let n := s.counter
@@ -47,7 +47,6 @@ private def mkHoleCall (source : Option FileRange) (holeType : HighTypeMd) : Eli
     outputs := [{ name := "$result", type := holeType }]
     preconditions := []
     decreases := none
-    isFunctional := true
     body := .Opaque [] none []
   }
   modify fun s => { s with generatedFunctions := s.generatedFunctions ++ [holeProc] }

Strata/Languages/Laurel/EliminateReturnStatements.lean

@@ -24,10 +24,8 @@ namespace Strata.Laurel
 
 public section
 
-private def returnLabel : String := "$return"
-
-
-
+@[expose, match_pattern]
+public def returnLabel : String := "$return"
 
 /-- Transform a single procedure: wrap body in a labelled block and replace returns. -/
 private def eliminateReturnStmts (proc : Procedure) : Procedure :=

Strata/Languages/Laurel/EliminateValueInReturns.lean

@@ -56,7 +56,7 @@ def hasValuedReturn (stmt : StmtExprMd) : Bool :=
 
 /-- Apply value-return elimination to a single procedure. Rewrites `return expr`
     into `outParam := expr; return` for any procedure with exactly one output
-    parameter (functional and non-functional alike).
+    parameter.
     Emits an error if a valued return is used with zero or multiple output parameters. -/
 def eliminateValueReturnsInProc (proc : Procedure) : Procedure :=
   match proc.outputs with

Strata/Languages/Laurel/Grammar/AbstractToConcreteTreeTranslator.lean

@@ -233,7 +233,6 @@ private def modifiesClausesToArgs (modifies : List StmtExprMd) : Array Arg :=
   wildcardArgs ++ specificArgs
 
 private def procedureToOp (proc : Procedure) : StrataDDM.Operation :=
-  let opName := if proc.isFunctional then "function" else "procedure"
   let params := proc.inputs.map parameterToArg |>.toArray
   let returnTypeArg : Arg :=
     match proc.outputs with
@@ -256,14 +255,7 @@ private def procedureToOp (proc : Procedure) : StrataDDM.Operation :=
     laurelOp "invokeOnClause" #[stmtExprToArg e])
   let (opaqueSpecArg, bodyArg) := match proc.body with
     | .Transparent body =>
-      -- For functions, the body is implicitly wrapped in a Return by ConcreteToAbstract;
-      -- unwrap it here so the concrete output doesn't show an explicit `return`.
-      let emitBody := if proc.isFunctional then
-        match body.val with
-        | .Return (some inner) => inner
-        | _ => body
-      else body
-      (optionArg none, optionArg (some (laurelOp "body" #[stmtExprToArg emitBody])))
+      (optionArg none, optionArg (some (laurelOp "body" #[stmtExprToArg body])))
     | .Opaque postconds impl modifies =>
       let ens := postconds.map ensuresClauseToArg |>.toArray
       let mods := if modifies.isEmpty then #[] else modifiesClausesToArgs modifies
@@ -275,7 +267,7 @@ private def procedureToOp (proc : Procedure) : StrataDDM.Operation :=
     | .External =>
       (optionArg none, optionArg (some (laurelOp "externalBody")))
   { ann := sr
-    name := { dialect := "Laurel", name := opName }
+    name := { dialect := "Laurel", name := "procedure" }
     args := #[
       ident proc.name.text,
       commaSep params,

Strata/Languages/Laurel/Grammar/ConcreteToAbstractTreeTranslator.lean

@@ -150,7 +150,6 @@ instance : Inhabited Procedure where
     outputs := []
     preconditions := []
     decreases := none
-    isFunctional := false
     invokeOn := none
     body := .Transparent { val := .LiteralBool true, source := none }
   }
@@ -354,15 +353,15 @@ partial def translateStmtExpr (arg : Arg) : TransM StmtExprMd := do
       let cond ← translateStmtExpr condArg
       let invariants ← translateInvariantClauses translateStmtExpr invSeqArg
       let body ← translateStmtExpr bodyArg
-      return mkStmtExprMd (.While cond invariants none body) src
+      return mkStmtExprMd (.While cond invariants none body false) src
     | q`Laurel.forLoop, #[initArg, condArg, stepArg, invSeqArg, bodyArg] =>
       let init ← translateStmtExpr initArg
       let cond ← translateStmtExpr condArg
       let step ← translateStmtExpr stepArg
       let invariants ← translateInvariantClauses translateStmtExpr invSeqArg
       let body ← translateStmtExpr bodyArg
       let whileBody := mkStmtExprMd (.Block [body, step] none) src
-      let whileStmt := mkStmtExprMd (.While cond invariants none whileBody) src
+      let whileStmt := mkStmtExprMd (.While cond invariants none whileBody false) src
       return mkStmtExprMd (.Block [init, whileStmt] none) src
     | q`Laurel.doWhile, #[bodyArg, condArg, invSeqArg] =>
       -- A `do … while` is a post-test `While`. The `EliminateDoWhile` pass
@@ -568,11 +567,6 @@ def parseProcedure (arg : Arg) : TransM Procedure := do
         | _, _ => TransM.error s!"Expected body or externalBody operation, got {repr bodyOp.name}"
       | .option _ none => pure none
       | _ => TransM.error s!"Expected body, got {repr bodyArg}"
-    -- For functions, wrap the body in a Return so the last expression
-    -- is treated as the return value by downstream passes.
-    let body := if op.name == q`Laurel.function then
-      body.map fun b => ⟨.Return (some b), b.source⟩
-    else body
     -- Determine procedure body kind
     let procBody :=
       if isExternal then Body.External
@@ -586,7 +580,6 @@ def parseProcedure (arg : Arg) : TransM Procedure := do
       outputs := returnParameters
       preconditions := preconditions
       decreases := none
-      isFunctional := op.name == q`Laurel.function
       invokeOn := invokeOn
       body := procBody
     }