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

• EvalEnv : Type

  Evaluation environment

@[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.HasFvar (P : PureExpr) : Type

• mkFvar : P.Ident → P.Expr
• getFvar : P.Expr → Option P.Ident

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.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.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.Expr → Prop
• tt : P.Expr
• ff : P.Expr
• tt_is_not_ff : tt ≠ ff
• boolTy : P.Ty
• boolIsVal : HasVal.value tt ∧ HasVal.value ff

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

Boolean operations: not, and, imp.

• value : P.Expr → Prop
• tt : P.Expr
• ff : P.Expr
• tt_is_not_ff : tt ≠ ff
• boolTy : P.Ty
• boolIsVal : HasVal.value tt ∧ HasVal.value 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 (n : P.Expr) : isNumeral n = true → HasVal.value 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