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

Boolean expressions

• tt : P.Expr
• ff : P.Expr
• tt_is_not_ff : tt ≠ ff
• boolTy : P.Ty

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

• tt : P.Expr
• ff : P.Expr
• tt_is_not_ff : tt ≠ ff
• boolTy : P.Ty
• not : P.Expr → P.Expr

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

• tt : P.Expr
• ff : P.Expr
• tt_is_not_ff : tt ≠ ff
• boolTy : P.Ty
• and : P.Expr → P.Expr → P.Expr

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

• tt : P.Expr
• ff : P.Expr
• tt_is_not_ff : tt ≠ ff
• boolTy : P.Ty
• imp : P.Expr → P.Expr → P.Expr

class Imperative.HasIntOrder (P : PureExpr) : Type

Integer ordering primitives. zero is the lower-bound constant for well-foundedness (measure ≥ 0). intTy is the type of integer expressions, for variable declarations. ge is derivable as HasNot.not (lt b a) and is therefore omitted.

• eq : P.Expr → P.Expr → P.Expr
• lt : P.Expr → P.Expr → P.Expr
• zero : P.Expr
• intTy : P.Ty

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

• value : P.Expr → Prop

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

• bool_is_val : HasVal.value HasBool.tt ∧ HasVal.value HasBool.ff

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