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

def Lambda.inline_attr : String

Equations

• Lambda.inline_attr = "inline"

def Lambda.inline_if_constr_attr : String

Equations

• Lambda.inline_if_constr_attr = "inline_if_constr"

def Lambda.eval_if_constr_attr : String

Equations

• Lambda.eval_if_constr_attr = "eval_if_constr"

@[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 : Bool := false) (inputs : ListMap T.Identifier LMonoTy) (output : LMonoTy) (body : Option (LExpr T.mono) := none) (attr : Array String := #[]) (concreteEval : Option (T.Metadata → List (LExpr T.mono) → Option (LExpr T.mono)) := none) (axioms : List (LExpr T.mono) := []) : LFunc T

Helper constructor for LFunc to maintain backward compatibility.

Equations

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

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

Equations

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

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

Equations

• Lambda.instToFormatLFuncOfIDMetaOfInhabitedMetadata = { 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.

def 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.

Equations

• Lambda.Factory T = Array (Lambda.LFunc T)

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

Equations

• Lambda.Factory.default = #[]

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

Equations

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

instance Lambda.instMembershipLFuncFactory {T : LExprParams} : Membership (LFunc T) (Factory T)

Equations

• Lambda.instMembershipLFuncFactory = { mem := fun (x : Lambda.Factory T) (f : Lambda.LFunc T) => Array.Mem x f }

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

def Lambda.Factory.getFactoryLFunc {T : LExprParams} (F : Factory T) (name : String) : Option (LFunc T)

Equations

• F.getFactoryLFunc name = Array.find? (fun (fn : Lambda.LFunc T) => fn.name.name == name) F

def Lambda.Factory.addFactoryFunc {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.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 = Array.foldlM (fun (factory : Lambda.Factory T) (func : Lambda.LFunc T) => factory.addFactoryFunc func) F newF

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