Lambda's Factory

This module formalizes Lambda's factory, which is a mechanism to extend the type checker (see Strata.DL.Lambda.LExprT) and partial evaluator (see Strata.DL.Lambda.LExprEval) by providing a map from operations to their types and optionally, denotations. The factory allows adding type checking and evaluation support for new operations without modifying the implementation of either or any core ASTs.

Also see Strata.DL.Lambda.IntBoolFactory for a concrete example of a factory.

@[reducible, inline]

abbrev Lambda.Signature (IDMeta Ty : Type) : Type

A signature is a map from variable identifiers to types.

Equations

• Lambda.Signature IDMeta Ty = ListMap (Lambda.Identifier IDMeta) Ty

def Lambda.Signature.format {IDMeta Ty : Type} (ty : Signature IDMeta Ty) [Std.ToFormat Ty] : Std.Format

Equations

• Lambda.Signature.format [] = Std.Format.text ""
• Lambda.Signature.format [(k, v)] = Std.format "(" ++ Std.format k ++ Std.format " : " ++ Std.format v ++ Std.format ")"
• Lambda.Signature.format ((k, v) :: rest) = Std.format "(" ++ Std.format k ++ Std.format " : " ++ Std.format v ++ Std.format ") " ++ Lambda.Signature.format rest

@[reducible, inline]

abbrev Lambda.LMonoTySignature {IDMeta : Type} : Type

Equations

• Lambda.LMonoTySignature = Lambda.Signature IDMeta Lambda.LMonoTy

@[reducible, inline]

abbrev Lambda.LTySignature {IDMeta : Type} : Type

Equations

• Lambda.LTySignature = Lambda.Signature IDMeta Lambda.LTy

@[reducible, inline]

abbrev Lambda.LFunc (T : LExprParams) : Type

A Lambda factory function - instantiation of Func for Lambda expressions.

Universally quantified type identifiers, if any, appear before this signature and can quantify over the type identifiers in it.

Equations

• Lambda.LFunc T = Strata.DL.Util.Func T.Identifier (Lambda.LExpr T.mono) Lambda.LMonoTy T.Metadata

def Lambda.LFunc.mk {T : LExprParams} (name : T.Identifier) (typeArgs : List TyIdentifier := []) (isConstr isRecursive : Bool := false) (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 (Strata.DL.Util.FuncPrecondition (LExpr T.mono) T.Metadata) := []) (measure : Option (LExpr T.mono) := none) : LFunc T

Helper constructor for LFunc to maintain backward compatibility.

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Lambda.instInhabitedLFunc {T : LExprParams} [Inhabited T.Metadata] [Inhabited T.IDMeta] : Inhabited (LFunc T)

Equations

• Lambda.instInhabitedLFunc = { default := { name := default, inputs := [], output := Lambda.LMonoTy.bool } }

@[implicit_reducible]

instance Lambda.instToFormatLFuncOfInhabited {T : LExprParams} [Std.ToFormat T.IDMeta] [Inhabited T.Metadata] : Std.ToFormat (LFunc T)

Equations

• Lambda.instToFormatLFuncOfInhabited = { format := Strata.DL.Util.Func.format }

def Lambda.LFunc.type {T : LExprParams} [DecidableEq T.IDMeta] (f : LFunc T) : Except Std.Format LTy

Equations

• One or more equations did not get rendered due to their size.

theorem Lambda.LFunc.type_inputs_nodup {T : LExprParams} [DecidableEq T.IDMeta] (f : LFunc T) (ty : LTy) : f.type = Except.ok ty → f.inputs.keys.Nodup

def Lambda.LFunc.opExpr {T : LExprParams} [Inhabited T.Metadata] (f : LFunc T) : LExpr T.mono

Equations

• f.opExpr = Lambda.LExpr.op default f.name (some (match f.inputs.values with | [] => f.output | ity :: irest => ity.mkArrow (irest ++ f.output.destructArrow)))

def Lambda.LFunc.inputPolyTypes {T : LExprParams} (f : LFunc T) : LTySignature

Equations

• f.inputPolyTypes = List.map (fun (x : T.Identifier × Lambda.LMonoTy) => match x with | (id, mty) => (id, Lambda.LTy.forAll f.typeArgs mty)) f.inputs

def Lambda.LFunc.outputPolyType {T : LExprParams} (f : LFunc T) : LTy

Equations

• f.outputPolyType = Lambda.LTy.forAll f.typeArgs f.output

def Lambda.LFunc.eraseTypes {T : LExprParams} (f : LFunc T) : LFunc T

Equations

• One or more equations did not get rendered due to their size.

structure Lambda.Factory (T : LExprParams) : Type

The type checker and partial evaluator for Lambda is parameterizable by a user-provided Factory.

We don't have any "built-in" functions like +, -, etc. in (LExpr IDMeta) -- lambdas are our only tool. Factory gives us a way to add support for concrete/symbolic evaluation and type checking for FunFactory functions without actually modifying any core logic or the ASTs.

• toArray : Array (LFunc T)

  The underlying array of factory functions.

• nameMap : Std.HashMap String Nat
• toArrayDefined (i : Fin self.toArray.size) : (Lambda.Factory.nameMap✝ self)[self.toArray[i].name.name]? = do let a ← some i pure ↑a
• nameMapValid {k : String} (p : k ∈ Lambda.Factory.nameMap✝ self) : (Lambda.Factory.nameMap✝¹ self)[k] < self.toArray.size
• nameMapConsistent {k : String} (p : k ∈ Lambda.Factory.nameMap✝ self) : self.toArray[(Lambda.Factory.nameMap✝¹ self)[k]].name.name = k

theorem Lambda.Factory.name_nodup {T : LExprParams} (f : Factory T) : (List.map (fun (x : LFunc T) => x.name.name) f.toArray.toList).Nodup

The function names in a factory are unique.

def Lambda.Factory.mem {T : LExprParams} (f : Factory T) (name : String) : Prop

Equations

• f.mem name = (name ∈ Lambda.Factory.nameMap✝ f)

def Lambda.Factory.instMemDecidable {T : LExprParams} (f : Factory T) (name : String) : Decidable (f.mem name)

Equations

• f.instMemDecidable name = inferInstance

@[implicit_reducible]

instance Lambda.Factory.instMem {T : LExprParams} : Membership String (Factory T)

Equations

• Lambda.Factory.instMem = { mem := Lambda.Factory.mem }

@[implicit_reducible]

instance Lambda.Factory.instMembershipDecidable {T : LExprParams} (f : Factory T) (name : String) : Decidable (name ∈ f)

Equations

• f.instMembershipDecidable name = f.instMemDecidable name

def Lambda.Factory.get {T : LExprParams} (f : Factory T) (name : String) (p : name ∈ f) : LFunc T

Equations

• f.get name p = f.toArray[(Lambda.Factory.nameMap✝ f)[name]]

def Lambda.Factory.get? {T : LExprParams} (f : Factory T) (name : String) : Option (LFunc T)

Equations

• f.get? name = match h : (Lambda.Factory.nameMap✝ f)[name]? with | none => none | some idx => have idx_lt := ⋯; some f.toArray[idx]

@[implicit_reducible]

instance Lambda.Factory.instGetElem? {T : LExprParams} : GetElem? (Factory T) String (LFunc T) Membership.mem

Equations

• Lambda.Factory.instGetElem? = { getElem := Lambda.Factory.get, getElem? := Lambda.Factory.get? }

def Lambda.Factory.default {T : LExprParams} : Factory T

Equations

• Lambda.Factory.default = { toArray := #[], nameMap := ∅, toArrayDefined := ⋯, nameMapValid := ⋯, nameMapConsistent := ⋯ }

theorem Lambda.Factory.default_empty {T : LExprParams} (x : String) : ¬x ∈ Factory.default

@[implicit_reducible]

instance Lambda.Factory.instInhabited {T : LExprParams} : Inhabited (Factory T)

Equations

• Lambda.Factory.instInhabited = { default := Lambda.Factory.default }

def Lambda.Factory.push {T : LExprParams} (F : Factory T) (fn : LFunc T) (is_new : ¬fn.name.name ∈ F) : Factory T

Equations

• F.push fn is_new = { toArray := F.toArray.push fn, nameMap := (Lambda.Factory.nameMap✝ F).insert fn.name.name F.toArray.size, toArrayDefined := ⋯, nameMapValid := ⋯, nameMapConsistent := ⋯ }

def Lambda.Factory.pushIfNew {T : LExprParams} (f : Factory T) (fn : LFunc T) : Factory T

Insert fn into the factory if no function with the same name already exists.

Equations

• f.pushIfNew fn = if p : fn.name.name ∈ f then f else f.push fn p

def Lambda.Factory.append {T : LExprParams} (F : Factory T) (a : Array (LFunc T)) : Factory T

Equations

• F.append a = Array.foldl Lambda.Factory.pushIfNew F a

def Lambda.Factory.ofArray {T : LExprParams} (a : Array (LFunc T)) : Factory T

Equations

• Lambda.Factory.ofArray a = Lambda.Factory.default.append a

theorem Lambda.Factory.ofArray_mem {T : LExprParams} {a : Array (LFunc T)} {fn : LFunc T} (p : fn ∈ (ofArray a).toArray) : fn ∈ a

@[simp]

theorem Lambda.Factory.toArray_default {T : LExprParams} : Factory.default.toArray = #[]

@[simp]

theorem Lambda.Factory.default_mem_is_false (T : LExprParams) (name : String) : name ∈ Factory.default ↔ False

theorem Lambda.Factory.push_mem_iff {T : LExprParams} (f : Factory T) (fn : LFunc T) (h : ¬fn.name.name ∈ f) (name : String) : name ∈ f.push fn h ↔ name = fn.name.name ∨ name ∈ f

theorem Lambda.Factory.mem_iff_mem_names {T : LExprParams} (f : Factory T) (s : String) : s ∈ f ↔ s ∈ Array.map (fun (x : LFunc T) => x.name.name) f.toArray

theorem Lambda.Factory.push_mem_match {T : LExprParams} (f : Factory T) (fn : LFunc T) (h : ¬fn.name.name ∈ f) (name : String) : (f.push fn h)[name]? = if name = fn.name.name then some fn else f[name]?

theorem Lambda.Factory.getElem?_is_some_implies_mem {T : LExprParams} {f : Factory T} {name : String} {fn : LFunc T} (eq : f[name]? = some fn) : fn ∈ f.toArray

theorem Lambda.Factory.getElem?_some_implies_mem {T : LExprParams} {f : Factory T} {name : String} {fn : LFunc T} (eq : f[name]? = some fn) : name ∈ f

theorem Lambda.Factory.getElem?_some_getElem {T : LExprParams} {f : Factory T} {name : String} {fn : LFunc T} (eq : f[name]? = some fn) : f[name] = fn

theorem Lambda.Factory.mem_name_eq_getElem {T : LExprParams} {F : Factory T} {fn : LFunc T} {s : String} (hmem : fn ∈ F.toArray) (hname : fn.name.name = s) : ∃ (hs : s ∈ F), F[s] = fn

If fn ∈ F.toArray and fn.name.name = s, then s ∈ F and F[s] = fn.

def Lambda.Factory.getFunctionNames {T : LExprParams} (F : Factory T) : Array T.Identifier

Equations

• F.getFunctionNames = Array.map (fun (f : Lambda.LFunc T) => f.name) F.toArray

def Lambda.Factory.tryPush {T : LExprParams} [Inhabited T.Metadata] [Std.ToFormat T.IDMeta] (F : Factory T) (func : LFunc T) : Except Strata.DiagnosticModel (Factory T)

Add a function func to the factory F. Redefinitions are not allowed.

Equations

• One or more equations did not get rendered due to their size.

def Lambda.Factory.tryAddAll {T : LExprParams} [Inhabited T.Metadata] [Std.ToFormat T.IDMeta] (F : Factory T) (newF : Array (LFunc T)) : Except Strata.DiagnosticModel (Factory T)

Append a factory newF to an existing factory F, checking for redefinitions along the way.

Equations

• F.tryAddAll newF = Array.foldlM (fun (x1 : Lambda.Factory T) (x2 : Lambda.LFunc T) => x1.tryPush x2) F newF

def Lambda.Factory.addFactory {T : LExprParams} [Inhabited T.Metadata] [Std.ToFormat T.IDMeta] (F newF : Factory T) : Except Strata.DiagnosticModel (Factory T)

Append a factory newF to an existing factory F, checking for redefinitions along the way.

Equations

• F.addFactory newF = F.tryAddAll newF.toArray

def Lambda.getLFuncCall {T : LExprParams} {GenericTy : Type} (e : LExpr { base := T, TypeType := GenericTy }) : LExpr { base := T, TypeType := GenericTy } × List (LExpr { base := T, TypeType := GenericTy })

Equations

• Lambda.getLFuncCall e = Lambda.getLFuncCall.go e []

def Lambda.getLFuncCall.go {T : LExprParams} {GenericTy : Type} (e : LExpr { base := T, TypeType := GenericTy }) (acc : List (LExpr { base := T, TypeType := GenericTy })) : LExpr { base := T, TypeType := GenericTy } × List (LExpr { base := T, TypeType := GenericTy })

Equations

• Lambda.getLFuncCall.go (Lambda.LExpr.app m (Lambda.LExpr.app m_1 e' arg1) arg2) acc = Lambda.getLFuncCall.go e' ([arg1, arg2] ++ acc)
• Lambda.getLFuncCall.go (Lambda.LExpr.app m (Lambda.LExpr.op m_1 fn fnty) arg1) acc = (Lambda.LExpr.op m_1 fn fnty, [arg1] ++ acc)
• Lambda.getLFuncCall.go e acc = (e, acc)

def Lambda.getConcreteLFuncCall {T : LExprParams} {GenericTy : Type} (e : LExpr { base := T, TypeType := GenericTy }) : LExpr { base := T, TypeType := GenericTy } × List (LExpr { base := T, TypeType := GenericTy })

Equations

• Lambda.getConcreteLFuncCall e = match Lambda.getLFuncCall e with | (op, args) => if args.all Lambda.LExpr.isConst = true then (op, args) else (e, [])

def Lambda.Factory.callOfLFunc {T : LExprParams} {GenericTy : Type} (F : Factory T) (e : LExpr { base := T, TypeType := GenericTy }) (allowPartialApp : Bool := false) : Option (LExpr { base := T, TypeType := GenericTy } × List (LExpr { base := T, TypeType := GenericTy }) × LFunc T)

If e is a call of a factory function, get the operator (.op), a list of all the actuals, and the (LFunc IDMeta).

Equations

• One or more equations did not get rendered due to their size.

theorem Lambda.callOfLFunc_eq_some {T : LExprParams} {GenericTy : Type} {F : Factory T} {e callee : LExpr { base := T, TypeType := GenericTy }} {args : List (LExpr { base := T, TypeType := GenericTy })} {fn : LFunc T} (hcall : F.callOfLFunc e = some (callee, args, fn)) : ∃ (m : { base := T, TypeType := GenericTy }.base.Metadata), ∃ (name : Identifier { base := T, TypeType := GenericTy }.base.IDMeta), ∃ (ty : Option { base := T, TypeType := GenericTy }.TypeType), callee = LExpr.op m name ty ∧ F[name.name]? = some fn ∧ args.length = List.length fn.inputs

theorem Lambda.callOfLFunc_getLFuncCall {T : LExprParams} {GenericTy : Type} {F : Factory T} {e callee : LExpr { base := T, TypeType := GenericTy }} {args : List (LExpr { base := T, TypeType := GenericTy })} {fn : LFunc T} {aPA : Bool} (hcall : F.callOfLFunc e aPA = some (callee, args, fn)) : getLFuncCall e = (callee, args)

theorem Lambda.getLFuncCall.go_size {T : LExprParamsT} {e : LExpr T} {op : LExpr { base := T.base, TypeType := T.TypeType }} {args acc : List (LExpr { base := T.base, TypeType := T.TypeType })} : go e acc = (op, args) → op.sizeOf + (List.map LExpr.sizeOf args).sum ≤ e.sizeOf + (List.map LExpr.sizeOf acc).sum

theorem Lambda.LExpr.sizeOf_pos {T : LExprParamsT} (e : LExpr T) : 0 < e.sizeOf

theorem Lambda.List.sum_size_le {α : Type u_1} (f : α → Nat) {l : List α} {x : α} (x_in : x ∈ l) : f x ≤ (List.map f l).sum

theorem Lambda.getLFuncCall_smaller {T : LExprParamsT} {e : LExpr T} {op : LExpr { base := T.base, TypeType := T.TypeType }} {args : List (LExpr { base := T.base, TypeType := T.TypeType })} : getLFuncCall e = (op, args) → ∀ (a : LExpr { base := T.base, TypeType := T.TypeType }), a ∈ args → a.sizeOf < e.sizeOf

theorem Lambda.Factory.callOfLFunc_smaller {T : LExprParamsT} {F : Factory T.base} {e : LExpr T} {op : LExpr { base := T.base, TypeType := T.TypeType }} {args : List (LExpr { base := T.base, TypeType := T.TypeType })} {F' : LFunc T.base} {allowPartialMatch : Bool} : F.callOfLFunc e allowPartialMatch = some (op, args, F') → ∀ (a : LExpr { base := T.base, TypeType := T.TypeType }), a ∈ args → a.sizeOf < e.sizeOf

theorem Lambda.Factory.getElem?_name {T : LExprParams} {F : Factory T} {s : String} {fn : LFunc T} (h : F[s]? = some fn) : fn.name.name = s

If F[s]? finds a function, its name matches the query.

theorem Lambda.Factory.callOfLFunc_arity {T : LExprParams} {F : Factory T} {e callee : LExpr T.mono} {args : List (LExpr T.mono)} {fn : LFunc T} (hcall : F.callOfLFunc e = some (callee, args, fn)) : args.length = List.length fn.inputs

callOfLFunc ensures the number of args equals the number of inputs.

theorem Lambda.Factory.callOfLFunc_getElem? {T : LExprParams} {F : Factory T} {e callee : LExpr T.mono} {args : List (LExpr T.mono)} {fn : LFunc T} {aPA : Bool} (hcall : F.callOfLFunc e aPA = some (callee, args, fn)) : ∃ (m : T.mono.base.Metadata), ∃ (name : Identifier T.mono.base.IDMeta), ∃ (ty : Option T.mono.TypeType), callee = LExpr.op m name ty ∧ F[name.name]? = some fn

The callee of callOfLFunc is an .op whose name resolves to fn via F[_]?.

theorem Lambda.callOfLFunc_func_mem {T : LExprParams} (F : Factory T) (e op : LExpr T.mono) (args : List (LExpr T.mono)) (func : LFunc T) (aPA : Bool) (h : F.callOfLFunc e aPA = some (op, args, func)) : func ∈ F.toArray

If callOfLFunc returns a triple, the function is a member of the factory array.

def Lambda.LExpr.applySubst {T : LExprParams} (e : LExpr T.mono) (S : Subst) : LExpr T.mono

Apply type substitution S to all type annotations in an LExpr. This is only for user-defined types, not metadata-stored resolved types. If e is an LExprT whose metadata contains type information, use applySubstT.

Equations

• e.applySubst S = if S.hasEmptyScopes = true then e else e.replaceUserProvidedType (Lambda.LMonoTy.subst S)

theorem Lambda.LExpr.applySubst_eq_replaceUserProvidedType {T : LExprParams} (e : LExpr T.mono) (S : Subst) : e.applySubst S = e.replaceUserProvidedType (LMonoTy.subst S)

def Lambda.LExpr.typeOf {T : LExprParams} : LExpr T.mono → Option LMonoTy

Best-effort type extraction from an LExpr without a typing context. Returns none when the type cannot be determined syntactically.

Equations

• (Lambda.LExpr.const m c).typeOf = some c.ty
• (Lambda.LExpr.op m o ty).typeOf = ty
• (Lambda.LExpr.bvar m deBruijnIndex).typeOf = none
• (Lambda.LExpr.fvar m name ty).typeOf = ty
• (Lambda.LExpr.abs m prettyName (some argTy) e).typeOf = Option.map (fun (x : Lambda.LMonoTy) => Lambda.LMonoTy.arrow argTy x) e.typeOf
• (Lambda.LExpr.abs m prettyName none e).typeOf = none
• (Lambda.LExpr.quant m k prettyName ty trigger e).typeOf = some Lambda.LMonoTy.bool
• (Lambda.LExpr.app m fn e).typeOf = fn.typeOf.bind fun (x : Lambda.LMonoTy) => match x with | Lambda.LMonoTy.tcons "arrow" [head, ret] => some ret | x => none
• (Lambda.LExpr.ite m c t e).typeOf = t.typeOf
• (Lambda.LExpr.eq m e1 e2).typeOf = some Lambda.LMonoTy.bool

def Lambda.LFunc.opTypeSubst {T : LExprParams} (fn : LFunc T) (callee : LExpr T.mono) : Option Subst

Derive a type substitution from the .op type annotation alone, by unifying it against the function's generic type. On annotated terms (i.e., terms that have undergone type inference), the .op node always carries a type annotation, so this suffices.

Returns some Subst.empty when fn.typeArgs is empty (monomorphic — no-op). Returns none if the callee is not annotated or unification fails.

Equations

• One or more equations did not get rendered due to their size.
• fn.opTypeSubst callee = if fn.typeArgs.isEmpty = true then some Lambda.Subst.empty else none

def Lambda.LFunc.computeTypeSubst {T : LExprParams} (fn : LFunc T) (callee : LExpr T.mono) (args : List (LExpr T.mono)) : Option Subst

Derive a type substitution by unifying the instantiated operator type against the function's generic type. Used when inlining a polymorphic function body to instantiate type variables.

Prefers the .op annotation (via opTypeSubst). Falls back to a best-effort approach using argument types when the .op is not annotated. On annotated terms (after type inference), the .op always carries a type annotation, so the fallback is never needed.

Returns some Subst.empty when fn.typeArgs is empty (monomorphic — no-op). Returns none if the type substitution cannot be derived.

Equations

• One or more equations did not get rendered due to their size.

theorem Lambda.LFunc.computeTypeSubst_of_opTypeSubst {T : LExprParams} {fn : LFunc T} {callee : LExpr T.mono} {args : List (LExpr T.mono)} {s : Subst} (h : fn.opTypeSubst callee = some s) : fn.computeTypeSubst callee args = some s

When opTypeSubst succeeds, computeTypeSubst agrees with it.