structure Imperative.PureExpr : Type 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

  Factory for function/operator resolution

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

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

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

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.LawfulHasFvar (P : PureExpr) [HasFvar P] : Prop

Lawfulness of HasFvar: the round-trip getFvar (mkFvar x) = some x.

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

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

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.

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.HasVal (P : PureExpr) : Type

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

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

Boolean expressions. Extends HasVal P (folding in the former HasBoolVal). boolIsVal ensures tt/ff are values.

• value : P.Factory → P.Expr → Prop
• tt : P.Expr
• ff : P.Expr
• tt_is_not_ff : tt ≠ ff
• boolTy : P.Ty
• boolIsVal (f : P.Factory) : HasVal.value f tt ∧ HasVal.value f ff

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

Boolean operations: not, and, imp.

• value : P.Factory → P.Expr → Prop
• tt : P.Expr
• ff : P.Expr
• tt_is_not_ff : tt ≠ ff
• boolTy : P.Ty
• boolIsVal (f : P.Factory) : HasVal.value f tt ∧ HasVal.value f ff
• not : P.Expr → P.Expr
• and : P.Expr → P.Expr → P.Expr
• imp : P.Expr → P.Expr → P.Expr

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

Integer constants and the integer type.

• zero : P.Expr
• intTy : P.Ty
• isNumeral : P.Expr → Bool
• numeralIsValue (f : P.Factory) (n : P.Expr) : isNumeral n = true → HasVal.value f n
• 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.

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