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.LFuncDefined (T : LExprParams) : Type

The AST-facing Lambda function structure - instantiation of the base Func for Lambda expressions. It is used for functions that appear in the Strata AST (e.g. Core.Function, funcDecl), and carries only plain data — the base Func excludes the function-typed concreteEval, so it has decidable equality.

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

Equations

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

structure Lambda.LFunc (T : LExprParams) extends Strata.DL.Util.Func T.Identifier (Lambda.LExpr T.mono) Lambda.LMonoTy T.Metadata : Type

A Lambda factory function - the full, evaluator/factory-facing function structure. It extends the AST-facing Func with the partial-evaluator hook concreteEval. All other fields live on the base Func.

A optional evaluation function can be provided in the concreteEval field for each factory function to allow the partial evaluator to do constant propagation when all the arguments of a function are concrete. Such a function should take two inputs: a function call expression and also -- somewhat redundantly, but perhaps more conveniently -- the list of arguments in this expression. Here's an example of a concreteEval function for Int.Add:

(fun e args => match args with
               | [e1, e2] =>
                 let e1i := LExpr.denoteInt e1
                 let e2i := LExpr.denoteInt e2
                 match e1i, e2i with
                 | some x, some y => (.const (toString (x + y)) mty[int])
                 | _, _ => e
               | _ => e)

Note that if there is an arity mismatch or if the arguments are not concrete/constants, this fails and it returns .none. If LFunc already has body, it must not have concreteEval, and vice versa.

• mk' :: (
• name : T.Identifier
• typeArgs : List TyIdentifier
• isConstr : Bool
• isRecursive : Bool
• inputs : ListMap T.Identifier Lambda.LMonoTy
• output : Lambda.LMonoTy
• body : Option (Lambda.LExpr T.mono)
• attr : Array FuncAttr
• axioms : List (Lambda.LExpr T.mono)
• preconditions : List (FuncPrecondition (Lambda.LExpr T.mono) T.Metadata)
• measure : Option (Lambda.LExpr T.mono)
• concreteEval : Option (T.Metadata → List (LExpr T.mono) → Option (LExpr T.mono))
• )

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.

def Lambda.LFuncDefined.toLFunc {T : LExprParams} (f : LFuncDefined T) (concreteEval : Option (T.Metadata → List (LExpr T.mono) → Option (LExpr T.mono)) := none) : LFunc T

Lift an AST-facing LFuncDefined (base Func) into the full LFunc, optionally attaching concreteEval at the evaluator boundary. All other data carries over unchanged via toFunc.

Equations

• f.toLFunc concreteEval = { toFunc := f, concreteEval := concreteEval }

@[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.instToFormatLFuncOfLExpr {T : LExprParams} [Std.ToFormat T.IDMeta] [Inhabited T.Metadata] [Std.ToFormat (LExpr T.mono)] : Std.ToFormat (LFunc T)

Equations

• Lambda.instToFormatLFuncOfLExpr = { format := fun (f : Lambda.LFunc T) => f.format }

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

Equations

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

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

def Lambda.LFuncDefined.opExpr {T : LExprParams} [Inhabited T.Metadata] (f : LFuncDefined 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.LFuncDefined.inputPolyTypes {T : LExprParams} (f : LFuncDefined 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.LFuncDefined.inputMonoSignature {T : LExprParams} (f : LFuncDefined T) : LTySignature

Equations

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

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

Equations

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

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

Equations

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

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

Equations

• f.type = Lambda.LFuncDefined.type f.toFunc

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

Equations

• f.opExpr = Lambda.LFuncDefined.opExpr f.toFunc

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

Equations

• f.inputPolyTypes = Lambda.LFuncDefined.inputPolyTypes f.toFunc

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

Equations

• f.inputMonoSignature = Lambda.LFuncDefined.inputMonoSignature f.toFunc

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

Equations

• f.outputPolyType = Lambda.LFuncDefined.outputPolyType f.toFunc

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

Equations

• f.eraseTypes = { toFunc := Lambda.LFuncDefined.eraseTypes f.toFunc, concreteEval := f.concreteEval }

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

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

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.Message (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.Message (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.Message (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.

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)

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.