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

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

• tt : P.Expr
• ff : P.Expr
• not : P.Expr → P.Expr

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

• tt : P.Expr
• ff : P.Expr
• and : P.Expr → P.Expr → P.Expr

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

• tt : P.Expr
• ff : P.Expr
• imp : P.Expr → P.Expr → P.Expr

class Imperative.HasEq (P : PureExpr) : Type

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

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

def Imperative.HasSubstFvar.substFvars {P : PureExpr} [HasSubstFvar P] (e : P.Expr) (substs : List (P.Ident × P.Expr)) : P.Expr

Substitute multiple free variables with expressions

Equations

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

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