structure Imperative.PureExpr : Type (u + 1)

Expected interface for pure expressions that can be used to specialize the Imperative dialect.

• Ident : Type

  Kinds of identifiers allowed in expressions. We expect identifiers to have decidable equality; see EqIdent.

• EqIdent : DecidableEq self.Ident

  Decidable equality on identifiers.

• Expr : Type

  Expressions

• Ty : Type

  Types

• ExprMetadata : Type

  Expression metadata type (for use in function declarations, etc.)

• TyEnv : Type

  Typing environment, expected to contain a map of variables to their types, type substitution, etc.

• TyContext : Type

  Typing context, expected to contain information that does not change during type checking/inference (e.g., known types and known functions.)

• Factory : Type u

  Factory for function/operator resolution. A factory may also carry a semantic model (as Core's runtime factory does), which is why it lives in an arbitrary universe.

• Val : Type u

  Runtime values held by variable stores and produced by eval. A value may record the model it was produced in; HasVal.value says which values belong to a given factory.

• eval : self.Factory → (self.Ident → Option self.Val) → self.Expr → Option self.Val

  The expression evaluator. Takes a factory, a variable store, and an expression, and returns an optional value.

@[reducible, inline]

abbrev Imperative.PureExpr.TypedIdent (P : PureExpr) : Type

Equations

• P.TypedIdent = (P.Ident × P.Ty)

@[reducible, inline]

abbrev Imperative.PureExpr.TypedExpr (P : PureExpr) : Type

Equations

• P.TypedExpr = (P.Expr × P.Ty)

@[instance_reducible]

instance Imperative.instDecidableEqIdent (P : PureExpr) : DecidableEq P.Ident

[DecidableEq P.Ident] resolves to the bundled PureExpr.EqIdent field, keeping the term on a single instance across a proof.

Equations

• Imperative.instDecidableEqIdent P = P.EqIdent

Type Classes for Expressions

class Imperative.HasIdent (P : PureExpr) : Type

• ident : String → P.Ident

class Imperative.LawfulHasIdent (P : PureExpr) [HasIdent P] : Prop

Lawfulness of HasIdent: the canonical identifier-injection is injective.

• ident_inj : Function.Injective HasIdent.ident

class Imperative.HasFvar (P : PureExpr) : Type

• mkFvar : P.Ident → P.Expr
• mkTypedFvar : P.Ident → P.Ty → P.Expr

  A free variable carrying its type. A pass that introduces a variable after type checking has run must annotate it itself, since nothing downstream will.

• getFvar : P.Expr → Option P.Ident

class Imperative.HasOps (P : PureExpr) : Type

Returns ALL operator/function names referenced in an expression (e.g., .op constructs in Lambda).

• getOps : P.Expr → List P.Ident

class Imperative.LawfulHasFvar (P : PureExpr) [HasFvar P] [HasOps P] : Prop

Lawfulness of HasFvar: variable constructors round-trip through getFvar and a typed variable contains no operator references.

• getFvar_mkFvar (x : P.Ident) : HasFvar.getFvar (HasFvar.mkFvar x) = some x
• getFvar_mkTypedFvar (x : P.Ident) (ty : P.Ty) : HasFvar.getFvar (HasFvar.mkTypedFvar x ty) = some x

  The annotation does not change which variable the expression is.

• getOps_mkTypedFvar (x : P.Ident) (ty : P.Ty) : HasOps.getOps (HasFvar.mkTypedFvar x ty) = []

  A typed variable has no operator or function references.

class Imperative.HasFvars (P : PureExpr) : Type

Multi-variable version of HasFvar.getFvar: returns ALL free variables in a (possibly compound) expression. HasFvar.getFvar only returns Some when the expression is a single fvar atom; HasFvars.getFvars recurses into compounds.

• getFvars : P.Expr → List P.Ident
• getTypedFvars : P.Expr → List (P.Ident × P.Ty)

  The free-variable occurrences of an expression that carry a type annotation, with their annotations. There is no default: a language whose expressions carry no annotations says so with fun _ => [].

class Imperative.LawfulHasFvars (P : PureExpr) [HasFvar P] [HasFvars P] : Prop

Lawfulness of HasFvars against HasFvar: the free-variable list of an mkFvar x expression, as computed by the HasFvars.getFvars extractor, is a subset of [x].

• mkFvar_getFvars (x : P.Ident) : HasFvars.getFvars (HasFvar.mkFvar x) ⊆ [x]
• mkTypedFvar_getFvars (x : P.Ident) (ty : P.Ty) : HasFvars.getFvars (HasFvar.mkTypedFvar x ty) ⊆ [x]

  The annotation contributes no free variables of its own.

• mem_getFvars_of_typed (e : P.Expr) (x : P.Ident) (ty : P.Ty) : (x, ty) ∈ HasFvars.getTypedFvars e → x ∈ HasFvars.getFvars e

  An annotated occurrence is a free variable.

• mkFvar_getTypedFvars (x : P.Ident) : HasFvars.getTypedFvars (HasFvar.mkFvar x) = []

  A bare variable carries no annotation.

• mkTypedFvar_getTypedFvars (x : P.Ident) (ty : P.Ty) : HasFvars.getTypedFvars (HasFvar.mkTypedFvar x ty) ⊆ [(x, ty)]

  A typed variable carries only its own annotation.

class Imperative.HasVal (P : PureExpr) : Type u_1

Predicates on runtime values (P.Val): which values belong to a factory (and so may be held by its stores), and which values inhabit a type.

• value : P.Factory → P.Val → Prop

  v is a runtime value of factory f.

• valueOfTy : P.Factory → P.Val → P.Ty → Prop

  v is a value of the monomorphic type ty.

class Imperative.LawfulHasVal (P : PureExpr) [HasVal P] : Prop

Laws for the abstract typed-value predicate.

• valueOfTy_isVal (f : P.Factory) (v : P.Val) (ty : P.Ty) : HasVal.valueOfTy f v ty → HasVal.value f v

  Every typed value is a value.

• value_typed (f : P.Factory) (v : P.Val) : HasVal.value f v → ∃ (ty : P.Ty), HasVal.valueOfTy f v ty

  Every value has a type.

• valueOfTy_congr (f : P.Factory) (a b : P.Val) (ty₁ ty₂ : P.Ty) : HasVal.valueOfTy f a ty₁ → HasVal.valueOfTy f a ty₂ → HasVal.valueOfTy f b ty₂ → HasVal.valueOfTy f b ty₁

  Typed-value membership is congruent across the shared type of a witness: if some value a has both types ty₁ and ty₂, then any value of type ty₂ is also a value of type ty₁.

class Imperative.HasBool (P : PureExpr) extends Imperative.HasVal P : Type u_1

Boolean expressions and values. Extends HasVal P. The expression constants tt/ff are syntax; ttVal f/ffVal f are the runtime values of factory f they evaluate to (see WellFormedSemanticEvalVal).

• value : P.Factory → P.Val → Prop
• valueOfTy : P.Factory → P.Val → P.Ty → Prop
• tt : P.Expr
• ff : P.Expr
• tt_is_not_ff : tt ≠ ff
• boolTy : P.Ty
• ttVal : P.Factory → P.Val

  The runtime value true of a factory.

• ffVal : P.Factory → P.Val

  The runtime value false of a factory.

• ttVal_ne_ffVal (f : P.Factory) : ttVal f ≠ ffVal f

  The Boolean values are distinct.

• boolIsValOfTy (f : P.Factory) : HasVal.valueOfTy f (ttVal f) boolTy ∧ HasVal.valueOfTy f (ffVal f) boolTy

  Boolean values have the Boolean type.

def Imperative.HasBool.boolIsVal {P : PureExpr} [HasBool P] [LawfulHasVal P] (f : P.Factory) : HasVal.value f (ttVal f) ∧ HasVal.value f (ffVal f)

Boolean values are values, induced by their typed-value proofs.

Equations

• ⋯ = ⋯

def Imperative.HasFvar.mkVar {P : PureExpr} [HasFvar P] (x : P.Ident) (ty : Option P.Ty) : P.Expr

A variable reference, annotated with ty when given.

Equations

• Imperative.HasFvar.mkVar x (some t) = Imperative.HasFvar.mkTypedFvar x t
• Imperative.HasFvar.mkVar x none = Imperative.HasFvar.mkFvar x

def Imperative.HasFvar.mkBoolVar {P : PureExpr} [HasBool P] [HasFvar P] (x : P.Ident) : P.Expr

A Boolean variable reference.

Equations

• Imperative.HasFvar.mkBoolVar x = Imperative.HasFvar.mkVar x (some Imperative.HasBool.boolTy)

class Imperative.LawfulHasBool (P : PureExpr) [HasBool P] [HasFvars P] : Prop

Laws for the Boolean expression constants: they read no variables.

• tt_getFvars : HasFvars.getFvars HasBool.tt = []
• ff_getFvars : HasFvars.getFvars HasBool.ff = []

class Imperative.HasBoolOps (P : PureExpr) extends Imperative.HasBool P : Type u_1

Boolean operations: not, and, imp.

• value : P.Factory → P.Val → Prop
• valueOfTy : P.Factory → P.Val → P.Ty → Prop
• tt : P.Expr
• ff : P.Expr
• tt_is_not_ff : tt ≠ ff
• boolTy : P.Ty
• ttVal : P.Factory → P.Val
• ffVal : P.Factory → P.Val
• ttVal_ne_ffVal (f : P.Factory) : ttVal f ≠ ffVal f
• boolIsValOfTy (f : P.Factory) : HasVal.valueOfTy f (ttVal f) boolTy ∧ HasVal.valueOfTy f (ffVal f) boolTy
• not : P.Expr → P.Expr
• and : P.Expr → P.Expr → P.Expr
• imp : P.Expr → P.Expr → P.Expr

Typing of expressions

The command semantics only steps when expressions evaluate, and an evaluator may fail on ill-typed expressions (Core's denotational evaluator does). These definitions state the typing assumption under which evaluation cannot fail; their consequences for commands are in Strata.DL.Imperative.CmdSemanticsProps.

@[reducible, inline]

abbrev Imperative.VarTyping (P : PureExpr) : Type

The types assigned to variables, as computed by a type checker.

Equations

• Imperative.VarTyping P = (P.Ident → Option P.Ty)

class Imperative.HasTyping (P : PureExpr) : Type u_1

The typing judgment for expressions.

• HasType : P.Factory → VarTyping P → P.Expr → P.Ty → Prop

  e has type ty under factory f when each free variable x has the type Γ x.

def Imperative.StoreHasTyping {P : PureExpr} [HasVal P] (f : P.Factory) (σ : P.Ident → Option P.Val) (Γ : VarTyping P) : Prop

The store σ (a SemanticStore P) conforms to the typing Γ: every variable that Γ types holds a value of that type.

Equations

• Imperative.StoreHasTyping f σ Γ = ∀ (x : P.Ident) (ty : P.Ty), Γ x = some ty → ∃ (v : P.Val), σ x = some v ∧ Imperative.HasVal.valueOfTy f v ty

def Imperative.VarTyping.extend {P : PureExpr} (Γ : VarTyping P) (defs : List (P.Ident × P.Ty)) : VarTyping P

Extend the typing Γ with the typed definitions defs; the first definition of a name wins.

Equations

• Γ.extend defs y = match List.find? (fun (d : P.Ident × P.Ty) => d.fst == y) defs with | some d => some d.snd | none => Γ y

class Imperative.LawfulHasTyping (P : PureExpr) [HasBool P] [HasTyping P] : Prop

Type soundness of the evaluator against the typing judgment.

• eval_of_hasType (f : P.Factory) (Γ : VarTyping P) (σ : P.Ident → Option P.Val) (e : P.Expr) (ty : P.Ty) : HasTyping.HasType f Γ e ty → StoreHasTyping f σ Γ → ∃ (v : P.Val), P.eval f σ e = some v ∧ HasVal.valueOfTy f v ty

  A well-typed expression evaluates, in a store conforming to its typing, to a value of its type.

• valueOfTy_bool (f : P.Factory) (v : P.Val) : HasVal.valueOfTy f v HasBool.boolTy → v = HasBool.ttVal f ∨ v = HasBool.ffVal f

  The values of the Boolean type are the two Boolean values.

class Imperative.HasInt (P : PureExpr) [HasVal P] [HasFvars P] : Type u_1

Integer constants and the integer type.

• zero : P.Expr
• intTy : P.Ty
• isNumeral : P.Expr → Bool
• isNumeralVal : P.Val → Bool

  The runtime values that are integer numerals.

• zeroIsNumeral : isNumeral zero = true
• numeralHasNoFvars (n : P.Expr) : isNumeral n = true → HasFvars.getFvars n = []

class Imperative.HasIntOps (P : PureExpr) [HasBool P] [HasFvars P] [HasInt P] : Type

Integer arithmetic / comparison primitives.

• eq : P.Expr → P.Expr → P.Expr
• lt : P.Expr → P.Expr → P.Expr

class Imperative.HasSubstFvar (P : PureExpr) : Type

Substitution of free variables in expressions. Used for closure capture in function declarations.

• substFvar : P.Expr → P.Ident → P.Expr → P.Expr

  Substitute a single free variable with an expression

• substFvars : P.Expr → List (P.Ident × P.Expr) → P.Expr

  Simultaneously substitute multiple free variables with expressions. Replaces all variables in a single pass, avoiding capture between substitutions.

• renameFvars : P.Expr → List (P.Ident × P.Ident) → P.Expr

  Simultaneously rename free variables by NAME, in a single pass with first-match semantics (a ↦ b for the first (a, b) in the list, else unchanged). Unlike substFvars, this rewrites a free variable's name in place and preserves everything else about the occurrence — in particular any type annotation it carries — so renaming never drops type information the way substituting a freshly-built bare free variable would.

@[reducible, inline]

abbrev Imperative.PureFunc (P : PureExpr) : Type

A function declaration for use with PureExpr - instantiation of Func for any expression system that implements the PureExpr interface.

Equations

• Imperative.PureFunc P = Strata.DL.Util.Func P.Ident P.Expr P.Ty P.ExprMetadata