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

A concrete evaluator for a factory function (see LFunc.concreteEval). It takes the metadata to attach to the result, the type annotation of the function's operator at the call (none when the operator is not annotated), and the arguments of the call. It returns the result of the call, or none when it does not apply (e.g. the arguments are not literals). The operator's type gives the evaluator the instantiation of the function's type parameters, which it needs to build a literal of a type that is not determined by the arguments (e.g. the empty sequence).

The soundness obligations on an evaluator (LFunc.InterpConsistentEval, Factory.EvalWellTyped, LFunc.EvalSound) constrain its result only when the annotation is the function's type instantiated by the call's type substitution (LFunc.instTy), which is the annotation of the operator of a well-typed call. No theorem covers its result at other annotations: none, which LExpr.eval passes for an unannotated operator and Core's model (gatherEval) always passes, or a type with type variables. So an evaluator that reads the annotation returns none unless the annotation is a ground type; an evaluator that ignores the annotation is covered at every annotation.

Equations

• Lambda.ConcreteEval T = (T.Metadata → Option Lambda.LMonoTy → List (Lambda.LExpr T.mono) → Option (Lambda.LExpr T.mono))

def Lambda.LExpr.opTy? {T : LExprParamsT} : LExpr T → Option T.TypeType

The type annotation of an operator, and none for any other expression.

Equations

• (Lambda.LExpr.op m o ty).opTy? = ty
• x✝.opTy? = none

@[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), 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; its type is ConcreteEval. Here's an example of a concreteEval function for Int.Add:

(fun md _ args => match args with
  | [e1, e2] =>
    match LExpr.denoteInt e1, LExpr.denoteInt e2 with
    | some x, some y => some (.intConst md (x + y))
    | _, _ => none
  | _ => none)

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)
• lemmas : List String
• concreteEval : Option (ConcreteEval T)
• )

def Lambda.LFunc.instTy {T : LExprParams} (f : LFunc T) (S : Subst) : LMonoTy

The type of the function f instantiated by the type substitution S: the arrow from its input types to its output type, each under S. The operator of a call of f well typed at the instance S is annotated with it, and the soundness obligations on concrete evaluators are stated at it (see ConcreteEval).

Equations

• f.instTy S = (Lambda.LMonoTy.subst S f.output).mkArrow' (List.map (Lambda.LMonoTy.subst S) (List.map Prod.snd f.inputs))

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 (ConcreteEval T) := 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 (ConcreteEval T) := 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 }

@[instance_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 } }

@[instance_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.exprs {T : LExprParams} (f : LFunc T) : List (LExpr T.mono)

Every expression f carries: its body, its axioms, its preconditions and its measure. The LFunc fields it reads are Func's, so this is that function's list.

Equations

• f.exprs = f.exprs

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) : (nameMap self)[self.toArray[i].name.name]? = do let a ← some i pure ↑a
• nameMapValid {k : String} (p : k ∈ nameMap self) : (nameMap self)[k] < self.toArray.size
• nameMapConsistent {k : String} (p : k ∈ nameMap self) : self.toArray[(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

@[instance_reducible]

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

Equations

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

@[instance_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]

@[instance_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

@[instance_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.map {T : LExprParams} (F : Factory T) (g : LFunc T → LFunc T) (hg : ∀ (f : LFunc T), (g f).name.name = f.name.name) : Factory T

F with every function f replaced by g f, for a g that keeps function names.

Equations

• F.map g hg = { toArray := Array.map g F.toArray, nameMap := Lambda.Factory.nameMap✝ F, toArrayDefined := ⋯, nameMapValid := ⋯, nameMapConsistent := ⋯ }

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.