Add recursive functions to Strata Core

Strata/DDM/AST.lean

@@ -588,6 +588,14 @@ def scopeDatatypeIndex (metadata : Metadata) : Option (Nat × Nat) :=
   | some #[.catbvar nameIdx, .catbvar typeParamsIdx] => some (nameIdx, typeParamsIdx)
   | some _ => panic! s!"Unexpected argument count to scopeDatatype"
 
+/-- Returns (nameIndex, argsIndex, typeIndex) if @[scopeSelf] is present.
+    Used to bring a function's own name into scope within its body. -/
+def scopeSelfIndex (metadata : Metadata) : Option (Nat × Nat × Nat) :=
+  match metadata[q`StrataDDL.scopeSelf]? with
+  | none => none
+  | some #[.catbvar n, .catbvar a, .catbvar t] => some (n, a, t)
+  | some _ => panic! s!"Unexpected argument count to scopeSelf"
+
 /-- Returns the name index if @[declareTVar] is present.
     Used for operations that introduce a type variable (creates .tvar binding in result context). -/
 def declareTVarIndex (metadata : Metadata) : Option Nat :=
@@ -821,6 +829,22 @@ def argScopeDatatypeLevel (argDecls : ArgDecls) (level : Fin argDecls.size) : Op
     else
       panic! s!"scopeDatatype name index {nameIdx} out of bounds ({level.val})"
 
+/-- Returns (nameLevel, argsLevel, typeLevel) if @[scopeSelf] is present. -/
+def argScopeSelfLevel (argDecls : ArgDecls) (level : Fin argDecls.size)
+    : Option (Fin level.val × Fin level.val × Fin level.val) :=
+  match argDecls[level].metadata.scopeSelfIndex with
+  | none => none
+  | some (nIdx, aIdx, tIdx) =>
+    if h1 : nIdx < level.val then
+      if h2 : aIdx < level.val then
+        if h3 : tIdx < level.val then
+          some (⟨level.val - (nIdx + 1), by omega⟩,
+                ⟨level.val - (aIdx + 1), by omega⟩,
+                ⟨level.val - (tIdx + 1), by omega⟩)
+        else panic! s!"scopeSelf type index {tIdx} out of bounds ({level.val})"
+      else panic! s!"scopeSelf args index {aIdx} out of bounds ({level.val})"
+    else panic! s!"scopeSelf name index {nIdx} out of bounds ({level.val})"
+
 end ArgDecls
 
 /--

Strata/DDM/BuiltinDialects/StrataDDL.lean

@@ -174,6 +174,7 @@ def StrataDDL : Dialect := BuiltinM.create! "StrataDDL" #[initDialect] do
    used for recursive datatype definitions where the datatype name must be visible when parsing constructor field types (e.g., `tail: List` in
    `Cons(head: int, tail: List)`) -/
   declareMetadata { name := "scopeDatatype", args := #[.mk "name" .ident, .mk "typeParams" .ident] }
+  declareMetadata { name := "scopeSelf", args := #[.mk "name" .ident, .mk "args" .ident, .mk "type" .ident] }
 
 end Strata
 end

Strata/DDM/Elab/Core.lean

@@ -1051,8 +1051,7 @@ partial def runSyntaxElaborator
     let tctx ←
       /- Recursive datatypes make this a bit complicated, since we need to make
       sure the type is resolved as an fvar even while processing it. -/
-      match ae.datatypeScope with
-      | some (nameLevel, typeParamsLevel) =>
+      if let some (nameLevel, typeParamsLevel) := ae.datatypeScope then
         let nameTree := trees[nameLevel]
         let typeParamsTree := trees[typeParamsLevel]
         match nameTree, typeParamsTree with
@@ -1084,7 +1083,32 @@ partial def runSyntaxElaborator
             ctx.push { ident := name, kind := .tvar loc name }
           pure tctx
         | _, _ => continue
-      | none =>
+      else if let some (nameLevel, argsLevel, typeLevel) := ae.scopeSelf then
+        -- @[scopeSelf(name, args, type)] — adds function name as expression binding
+        -- Push function name BEFORE params so params keep their expected bvar indices.
+        -- This subsumes @[scope] — we push both self and params here.
+        match trees[nameLevel], trees[argsLevel], trees[typeLevel] with
+          | some nameT, some argsT, some typeT =>
+            let fnName :=
+              match nameT.info with
+              | .ofIdentInfo info => info.val
+              | _ => panic! "scopeSelf: expected identifier for function name"
+            let inheritedCount := tctx0.bindings.size
+            let paramBindings := argsT.resultContext.bindings.toArray.extract inheritedCount argsT.resultContext.bindings.size
+            let params := paramBindings.filterMap fun b =>
+              match b.kind with
+              | .expr tp => some (b.ident, tp)
+              | _ => none
+            let retType :=
+              match typeT.info with
+              | .ofTypeInfo info => info.typeExpr
+              | _ => panic! "scopeSelf: expected type for return type"
+            let fnType := TypeExprF.mkFunType typeT.info.loc params retType
+            -- Push self-binding, then all param bindings on top
+            let tctx := tctx0.push { ident := fnName, kind := .expr fnType }
+            pure (paramBindings.foldl (init := tctx) fun ctx b => ctx.push b)
+          | _, _, _ => continue
+      else
         match ae.contextLevel with
         | some idx =>
           match trees[idx] with

Strata/DDM/Elab/SyntaxElab.lean

@@ -28,6 +28,9 @@ structure ArgElaborator where
   -- Datatype scope: (nameLevel, typeParamsLevel) for recursive datatype definitions
   -- When set, the datatype name is added to the typing context as a type
   datatypeScope : Option (Fin argLevel × Fin argLevel) := .none
+  -- Self scope: (nameLevel, argsLevel, typeLevel) for recursive function definitions
+  -- When set, the function name is added to the typing context as an expression
+  scopeSelf : Option (Fin argLevel × Fin argLevel × Fin argLevel) := .none
 deriving Inhabited, Repr
 
 abbrev ArgElaboratorArray (sc : Nat) :=
@@ -64,6 +67,7 @@ private def push (as : ArgElaborators)
     argLevel := argLevel.val
     contextLevel := argDecls.argScopeLevel argLevel
     datatypeScope := argDecls.argScopeDatatypeLevel argLevel
+    scopeSelf := argDecls.argScopeSelfLevel argLevel
   }
   have scp : sc < sc + 1 := by grind
   { as with argElaborators := as.argElaborators.push ⟨newElab, scp⟩ }
@@ -109,6 +113,7 @@ private def mkSyntaxElab! (argDecls : ArgDecls) (stx : SyntaxDef) (opMd : Metada
       argLevel := 0
       contextLevel := argDecls.argScopeLevel ⟨0, h⟩
       datatypeScope := argDecls.argScopeDatatypeLevel ⟨0, h⟩
+      scopeSelf := argDecls.argScopeSelfLevel ⟨0, h⟩
     }
     {
       syntaxCount := 1

Strata/DDM/Format.lean

@@ -437,6 +437,21 @@ private partial def formatArguments (c : FormatContext) (initState : FormatState
                 | some ⟨alvl, aisLt⟩  =>
                   have _ : alvl < a.size := by simp at aisLt; omega
                   a[alvl].snd
+          -- If @[scopeSelf] is present, insert the function name before the param bindings.
+          -- scopeSelf subsumes @[scope]: we get params from argsLevel directly.
+          let s :=
+                match argDecls.argScopeSelfLevel ⟨lvl, h⟩ with
+                | none => s
+                | some (⟨nameLvl, nameIsLt⟩, ⟨argsLvl, argsIsLt⟩, _) =>
+                  have _ : nameLvl < a.size := by simp at nameIsLt; omega
+                  have _ : argsLvl < a.size := by simp at argsIsLt; omega
+                  match args[nameLvl] with
+                  | .ident _ name =>
+                    let paramBindings := a[argsLvl].snd.bindings
+                    let scopeStart := initState.bindings.size
+                    let paramOnly := paramBindings.extract scopeStart paramBindings.size
+                    { s with bindings := s.bindings ++ #[name] ++ paramOnly }
+                  | _ => s
           aux (a.push (args[lvl].mformatM c s))
         else
           a

Strata/DL/Lambda/Factory.lean

@@ -71,12 +71,13 @@ abbrev LFunc (T : LExprParams) := Func (T.Identifier) (LExpr T.mono) LMonoTy T.M
 Helper constructor for LFunc to maintain backward compatibility.
 -/
 def LFunc.mk {T : LExprParams} (name : T.Identifier) (typeArgs : List TyIdentifier := [])
-    (isConstr : Bool := false) (inputs : ListMap T.Identifier LMonoTy) (output : LMonoTy)
+    (isConstr : Bool := false) (isRecursive : Bool := false) (decreases : Option (LExpr T.mono) := none)
+    (inputs : ListMap T.Identifier LMonoTy) (output : LMonoTy)
     (body : Option (LExpr T.mono) := .none) (attr : Array Strata.DL.Util.FuncAttr := #[])
     (concreteEval : Option (T.Metadata → List (LExpr T.mono) → Option (LExpr T.mono)) := .none)
     (axioms : List (LExpr T.mono) := [])
     (preconditions : List (FuncPrecondition (LExpr T.mono) T.Metadata) := []) : LFunc T :=
-  Func.mk name typeArgs isConstr inputs output body attr concreteEval axioms preconditions
+  Func.mk name typeArgs isConstr isRecursive decreases inputs output body attr concreteEval axioms preconditions
 
 instance [Inhabited T.Metadata] [Inhabited T.IDMeta] : Inhabited (LFunc T) where
   default := { name := Inhabited.default, inputs := [], output := LMonoTy.bool }

Strata/DL/Lambda/LExprEval.lean

@@ -208,14 +208,8 @@ def evalIte (n' : Nat) (σ : LState TBase) (m: TBase.Metadata) (c t f : LExpr TB
   | .true _ => eval n' σ t
   | .false _ => eval n' σ f
   | _ =>
-    -- It's important to at least substitute `.fvar`s in both branches of the
-    -- `ite` here so that we can replace the variables by the values in the
-    -- state; these variables can come from an imperative dialect.
-    -- (TODO): Is it worth it to evaluate these branches instead?
-    -- let t' := eval n' σ t
-    -- let f' := eval n' σ f
-    let t' := substFvarsFromState σ t
-    let f' := substFvarsFromState σ f
+    let t' := eval n' σ t
+    let f' := eval n' σ f
     .ite m c' t' f'
 
 def evalEq (n' : Nat) (σ : LState TBase) (m: TBase.Metadata) (e1 e2 : LExpr TBase.mono) : LExpr TBase.mono :=

Strata/DL/Lambda/RecursiveAxioms.lean

@@ -0,0 +1,117 @@
+/-
+  Copyright Strata Contributors
+
+  SPDX-License-Identifier: Apache-2.0 OR MIT
+-/
+
+import Strata.DL.Lambda.Factory
+import Strata.DL.Lambda.TypeFactory
+import Strata.DL.Util.List
+
+/-!
+## Axiom Generation for Recursive Functions
+
+Given a recursive function with a `decreases` parameter over an algebraic datatype,
+generates per-constructor axioms. Each axiom is a quantified equation:
+
+  ∀ (other_params..., fields...). f(..., C(fields...), ...) = PE(f(..., C(fields...), ...))
+
+The LHS is left unevaluated (it serves as the trigger pattern). The RHS is obtained by
+passing the LHS to the partial evaluator, which inlines the function (since the recursive
+argument is a constructor application) and reduces.
+-/
+
+namespace Lambda
+
+open Std (Format format)
+open Strata.DL.Util (FuncAttr)
+
+/-- Check well-formedness of a recursive function and extract the components
+    needed for axiom generation: recParam index and datatype.
+    The `inlineIfConstr` attribute must have been previously set by `addFactoryFunc`
+    (which resolves the `decreases` expression to a parameter index). -/
+def checkRecursiveFunc [DecidableEq T.IDMeta]
+    (func : LFunc T) (tf : @TypeFactory T.IDMeta)
+    : Except Format (Nat × LDatatype T.IDMeta) := do
+  if func.inputs.isEmpty then
+    .error f!"Recursive function {func.name} must have at least one parameter"
+  let recIdx ← FuncAttr.findInlineIfConstr func.attr |>.elim
+    (.error f!"Recursive function {func.name} has no inlineIfConstr attribute") .ok
+  let inputTys := func.inputs.values
+  let recTy ← inputTys[recIdx]? |>.elim
+    (.error f!"Recursive function {func.name}: recParam index {recIdx} out of bounds") .ok
+  let dtName ← match recTy with
+    | LMonoTy.tcons n _ => .ok n
+    | _ => .error f!"Recursive function {func.name}: decreases parameter type is not a datatype"
+  let dt ← tf.getType dtName |>.elim
+    (.error f!"Recursive function {func.name}: datatype {dtName} not found") .ok
+  return (recIdx, dt)
+
+/-- Generate per-constructor axiom LExprs for a recursive function.
+    Assumes the function is well-formed (use `checkRecursiveFunc` first).
+    The PE must have the function in its factory with `inlineIfConstr`. -/
+def mkRecursiveAxioms [Inhabited T.Metadata] [DecidableEq T.Metadata] [DecidableEq T.IDMeta]
+    (func : LFunc T) (recIdx : Nat) (dt : LDatatype T.IDMeta)
+    (pe : LExpr T.mono → LExpr T.mono) (m : T.Metadata)
+    : Except Format (List (LExpr T.mono)) :=
+  let formals := func.inputs.keys
+  let inputTys := func.inputs.values
+  dt.constrs.mapM fun c => do
+    let numFields := c.args.length
+    let totalBvs := numFields + formals.length - 1
+    /-
+    De Bruijn indices (bvar 0 = innermost binder).
+    Binding order outer→inner: other params (excl. recIdx), then fields.
+      field i       → bvar (numFields - 1 - i)
+      other formal  → bvar (totalBvs - 1 - otherIdx idx)
+        where otherIdx skips recIdx: idx if idx < recIdx, else idx - 1
+
+    E.g. f(a:int, xs:IntList, b:bool), recIdx=1, Cons(hd, tl):
+      ∀ a. ∀ b. ∀ hd. ∀ tl. f(a=%3, Cons(hd=%1, tl=%0), b=%2) = ...
+    -/
+    let dtTy : LMonoTy := .tcons dt.name []
+    let constrTy := c.args.foldr (fun (_, argTy) acc => .arrow argTy acc) dtTy
+    let constrApp := c.args.foldlIdx (fun acc i _ =>
+      .app m acc (.bvar m (numFields - 1 - i))
+    ) (.op m c.name (.some constrTy) : LExpr T.mono)
+    let otherIdx (idx : Nat) : Nat := if idx < recIdx then idx else idx - 1
+    let formalExpr (idx : Nat) : LExpr T.mono :=
+      if idx == recIdx then constrApp
+      else .bvar m (totalBvs - 1 - otherIdx idx)
+    -- LHS: f(bvars..., C(fields...), bvars...) — not PE'd (serves as trigger)
+    let lhs := formals.foldlIdx (fun acc idx _ =>
+      .app m acc (formalExpr idx)
+    ) (LFunc.opExpr func)
+    -- RHS: PE inlines the function since the recursive arg is a constructor
+    let rhs := pe lhs
+    if lhs == rhs then
+      .error f!"Recursive function {func.name}: PE did not reduce axiom for \
+               constructor {c.name}. Ensure the function is in the factory \
+               and that the function body can be partially evaluated when \
+               the recursive parameter is a constructor."
+    let eq : LExpr T.mono := .eq m lhs rhs
+    /-
+    Quantifiers are wrapped innermost-first: field types (reversed so the
+    last field becomes bvar 0), then other param types (also reversed).
+    The innermost quantifier carries the LHS as a trigger pattern for SMT;
+    the rest use noTrigger.
+    -/
+    let allTys := (c.args.map (·.snd)).reverse ++ (inputTys.eraseIdx recIdx).reverse
+    match allTys with
+    | [] => .ok eq
+    | ty :: rest =>
+      let inner := LExpr.quant m .all (.some ty) lhs eq
+      .ok (rest.foldl (fun body ty =>
+        .quant m .all (.some ty) (LExpr.noTrigger m) body
+      ) inner)
+
+/-- Generate per-constructor axiom LExprs for a recursive function,
+    including well-formedness checking. -/
+def genRecursiveAxioms [Inhabited T.Metadata] [DecidableEq T.Metadata] [DecidableEq T.IDMeta]
+    (func : LFunc T) (tf : @TypeFactory T.IDMeta)
+    (pe : LExpr T.mono → LExpr T.mono) (m : T.Metadata)
+    : Except Format (List (LExpr T.mono)) := do
+  let (recIdx, dt) ← checkRecursiveFunc func tf
+  mkRecursiveAxioms func recIdx dt pe m
+
+end Lambda

Strata/DL/Lambda/Semantics.lean

@@ -73,16 +73,12 @@ inductive Step (F:@Factory Tbase) (rf:Env Tbase)
     Step F rf e1 e1' →
     Step F rf (.app m e1 e2) (.app m' e1' e2)
 
-/-- Lazy evaluation of `ite`: condition is true. To evaluate `ite x e1 e2`, do
-not first evaluate `e1` and `e2`. In other words, `ite x e1 e2` is interpreted
-as `ite x (λ.e1) (λ.e2)`.  -/
+/-- Evaluation of `ite`: condition is true, select "then" branch. -/
 | ite_reduce_then:
   ∀ (ethen eelse:LExpr Tbase.mono),
     Step F rf (.ite m (.const mc (.boolConst true)) ethen eelse) ethen
 
-/-- Lazy evaluation of `ite`: condition is false. To evaluate `ite x e1 e2`, do
-not first evaluate `e1` and `e2`. In other words, `ite x e1 e2` is interpreted
-as `ite x (λ.e1) (λ.e2)`.  -/
+/-- Evaluation of `ite`: condition is false, select "else" branch. -/
 | ite_reduce_else:
   ∀ (ethen eelse:LExpr Tbase.mono),
     Step F rf (.ite m (.const mc (.boolConst false)) ethen eelse) eelse
@@ -93,6 +89,18 @@ as `ite x (λ.e1) (λ.e2)`.  -/
     Step F rf econd econd' →
     Step F rf (.ite m econd ethen eelse) (.ite m' econd' ethen eelse)
 
+/-- Evaluation of `ite` "then" branch (when condition is not yet resolved). -/
+| ite_reduce_then_branch:
+  ∀ (econd ethen ethen' eelse:LExpr Tbase.mono),
+    Step F rf ethen ethen' →
+    Step F rf (.ite m econd ethen eelse) (.ite m' econd ethen' eelse)
+
+/-- Evaluation of `ite` "else" branch (when condition is not yet resolved). -/
+| ite_reduce_else_branch:
+  ∀ (econd ethen eelse eelse':LExpr Tbase.mono),
+    Step F rf eelse eelse' →
+    Step F rf (.ite m econd ethen eelse) (.ite m' econd ethen eelse')
+
 /-- Evaluation of equality. Reduce after both operands evaluate to values. -/
 | eq_reduce:
   ∀ (e1 e2 eres:LExpr Tbase.mono)

Strata/DL/SMT/DDMTransform/Translate.lean

@@ -115,21 +115,40 @@ private def translateFromTermType (t:SMT.TermType):
     else
       return .smtsort_param srnone (mkIdentifier id) (Ann.mk srnone argtys_array)
 
+-- Helper: convert an SMTSort to an SExpr for use in pattern attributes
+private def sortToSExpr (s : SMTDDM.SMTSort SourceRange)
+    : Except String (SMTDDM.SExpr SourceRange) := do
+  let srnone := SourceRange.none
+  match s with
+  | .smtsort_ident _ (.iden_simple _ sym) => return .se_symbol srnone sym
+  | .smtsort_param _ (.iden_simple _ sym) args =>
+    let argsSExpr ← args.val.toList.mapM sortToSExpr
+    return .se_ls srnone (Ann.mk srnone ((.se_symbol srnone sym :: argsSExpr).toArray))
+  | _ => throw s!"Doesn't know how to convert sort {repr s} to SMTDDM.SExpr"
+  termination_by SizeOf.sizeOf s
+  decreasing_by cases args; simp_all; term_by_mem
+
+
+-- Helper: convert a QualIdentifier to an SExpr for use in pattern attributes
+private def qiToSExpr (qi : SMTDDM.QualIdentifier SourceRange)
+    : Except String (SMTDDM.SExpr SourceRange) := do
+  let srnone := SourceRange.none
+  match qi with
+  | .qi_ident _ (.iden_simple _ sym) => pure (.se_symbol srnone sym)
+  | .qi_isort _ (.iden_simple _ sym) sort =>
+    let sortSExpr ← sortToSExpr sort
+    let asSym := SMTDDM.SExpr.se_symbol srnone (mkSymbol "as")
+    pure (.se_ls srnone (Ann.mk srnone #[asSym, .se_symbol srnone sym, sortSExpr]))
+  | _ => throw s!"Doesn't know how to convert QI {repr qi} to SMTDDM.SExpr"
+
 -- Helper function to convert a SMTDDM.Term to SExpr for use in pattern attributes
 def termToSExpr (t : SMTDDM.Term SourceRange)
     : Except String (SMTDDM.SExpr SourceRange) := do
   let srnone := SourceRange.none
   match t with
-  | .qual_identifier _ qi =>
-      match qi with
-      | .qi_ident _ (.iden_simple _ sym) => return .se_symbol srnone sym
-      | _ => throw s!"Doesn't know how to convert {repr t} to SMTDDM.SExpr"
+  | .qual_identifier _ qi => qiToSExpr qi
   | .qual_identifier_args _ qi args =>
-      -- Function application in pattern: convert to nested S-expr
-      let qiSExpr ← match qi with
-        | .qi_ident _ (.iden_simple _ sym) => pure (SMTDDM.SExpr.se_symbol srnone sym)
-        | _ => throw s!"Doesn't know how to convert {repr t} to SMTDDM.SExpr"
-      -- Convert args array to SExpr list
+      let qiSExpr ← qiToSExpr qi
       let argsSExpr ← args.val.mapM termToSExpr
       return .se_ls srnone (Ann.mk srnone ((qiSExpr :: argsSExpr.toList).toArray))
   | .spec_constant_term _ s => return .se_spec_const srnone s

Strata/DL/Util/Func.lean

@@ -66,6 +66,8 @@ structure Func (IdentT : Type) (ExprT : Type) (TyT : Type) (MetadataT : Type) wh
   name     : IdentT
   typeArgs : List TyIdentifier := []
   isConstr : Bool := false --whether function is datatype constructor
+  isRecursive : Bool := false
+  decreases : Option ExprT := none
   inputs   : ListMap IdentT TyT
   output   : TyT
   body     : Option ExprT := .none
@@ -93,8 +95,9 @@ def Func.format {IdentT ExprT TyT MetadataT : Type} [ToFormat IdentT] [ToFormat
   let precondsStr := if preconds.isEmpty then f!"" else Format.line ++ Format.joinSep preconds Format.line
   let sep := if f.body.isNone then f!";" else f!" :="
   let body := if f.body.isNone then f!"" else Std.Format.indentD f!"({f.body.get!})"
+  let recPrefix := if f.isRecursive then f!"recursive " else f!""
   f!"{attr}\
-     func {f.name} : {type}{precondsStr}{sep}\
+     {recPrefix}func {f.name} : {type}{precondsStr}{sep}\
      {body}"
 
 instance {IdentT ExprT TyT MetadataT : Type} [ToFormat IdentT] [ToFormat ExprT] [ToFormat TyT] [Inhabited ExprT] : ToFormat (Func IdentT ExprT TyT MetadataT) where