Encoding an Expr as a sequence of Keys

inductive Lean.Meta.RefinedDiscrTree.DTExpr : Type

DTExpr is a simplified form of Expr. It is the intermediate step for converting from Expr to Array Key.

• star : Option MVarId → DTExpr

  A metavariable. It optionally stores an MVarId.

• opaque : DTExpr

  An opaque variable or a let-expression in the case WhnfCoreConfig.zeta := false.

• const : Name → Array DTExpr → DTExpr

  A constant. It stores the name and the arguments.

• fvar : FVarId → Array DTExpr → DTExpr

  A free variable. It stores the FVarId and the arguments

• bvar : ℕ → Array DTExpr → DTExpr

  A bound variable. It stores the De Bruijn index and the arguments

• lit : Literal → DTExpr

  A literal.

• sort : DTExpr

  A sort.

• lam : DTExpr → DTExpr

  A lambda function. It stores the body.

• forall : DTExpr → DTExpr → DTExpr

  A dependent arrow. It stores the domain and body.

• proj : Name → ℕ → DTExpr → Array DTExpr → DTExpr

  A projection. It stores the structure name, projection index, struct body and arguments.

instance Lean.Meta.RefinedDiscrTree.instInhabitedDTExpr : Inhabited DTExpr

instance Lean.Meta.RefinedDiscrTree.instBEqDTExpr : BEq DTExpr

instance Lean.Meta.RefinedDiscrTree.instReprDTExpr : Repr DTExpr

instance Lean.Meta.RefinedDiscrTree.instToFormatDTExpr : ToFormat DTExpr

partial def Lean.Meta.RefinedDiscrTree.DTExpr.size : DTExpr → ℕ

Return the size of the DTExpr. This is used for calculating the matching score when two expressions are equal. The score is not incremented at a lambda, which is so that the expressions ∀ x, p[x] and ∃ x, p[x] get the same size.

def Lean.Meta.RefinedDiscrTree.DTExpr.eqv (a b : DTExpr) : Bool

Determine if two DTExprs are equivalent.

@[irreducible]

def Lean.Meta.RefinedDiscrTree.DTExpr.eqv.go (a b : DTExpr) : StateM (Std.HashMap MVarId MVarId) Bool

@[irreducible]

def Lean.Meta.RefinedDiscrTree.DTExpr.eqv.goArray (as bs : Array DTExpr) : StateM (Std.HashMap MVarId MVarId) Bool

Encoding an Expr

def Lean.Meta.RefinedDiscrTree.DTExpr.flatten (e : DTExpr) (initCapacity : ℕ := 16) : Array Key

Given a DTExpr, return the linearized encoding in terms of Key, which is used for RefinedDiscrTree indexing.

partial def Lean.Meta.RefinedDiscrTree.reduce (e : Expr) : MetaM Expr

Reduction procedure for the RefinedDiscrTree indexing.

@[specialize #[]]

partial def Lean.Meta.RefinedDiscrTree.lambdaTelescopeReduce {α : Type} {m : Type → Type u_1} [Monad m] [MonadLiftT MetaM m] [MonadControlT MetaM m] [Nonempty α] (e : Expr) (fvars : List FVarId) (k : Expr → List FVarId → m α) : m α

Repeatedly apply reduce while stripping lambda binders and introducing their variables

def Lean.Meta.RefinedDiscrTree.isStar : Expr → Bool

Check whether the expression is represented by Key.star.

def Lean.Meta.RefinedDiscrTree.isStarWithArg (arg : Expr) : Expr → Bool

Check whether the expression is represented by Key.star and has arg as an argument.

def Lean.Meta.RefinedDiscrTree.DTExpr.hasLooseBVars (e : DTExpr) : Bool

Return true if e contains a loose bound variable.

def Lean.Meta.RefinedDiscrTree.MkDTExpr.getIgnores (fn : Expr) (args : Array Expr) : MetaM (Array Bool)

Return for each argument whether it should be ignored.

def Lean.Meta.RefinedDiscrTree.MkDTExpr.getIgnores.isIgnoredArg (arg domain : Expr) (binderInfo : BinderInfo) : MetaM Bool

Return whether the argument should be ignored.

partial def Lean.Meta.RefinedDiscrTree.MkDTExpr.mkDTExprAux (e : Expr) (root : Bool) : ReaderT Lean.Meta.RefinedDiscrTree.MkDTExpr.Context✝ MetaM DTExpr

Return the encoding of e as a DTExpr. If root = false, then e is a strict sub expression of the original expression.

instance Lean.Meta.RefinedDiscrTree.MkDTExpr.instMonadCacheExprDTExprM : MonadCache Expr DTExpr Lean.Meta.RefinedDiscrTree.MkDTExpr.M✝

@[specialize #[]]

def Lean.Meta.RefinedDiscrTree.MkDTExpr.etaPossibilities {α : Type} (e : Expr) (lambdas : List FVarId) (k : Expr → List FVarId → Lean.Meta.RefinedDiscrTree.MkDTExpr.M✝ α) : Lean.Meta.RefinedDiscrTree.MkDTExpr.M✝ α

Return all pairs of body, bound variables that could possibly appear due to η-reduction

@[specialize #[]]

def Lean.Meta.RefinedDiscrTree.MkDTExpr.cacheEtaPossibilities (e original : Expr) (lambdas : List FVarId) (k : Expr → List FVarId → Lean.Meta.RefinedDiscrTree.MkDTExpr.M✝ DTExpr) : Lean.Meta.RefinedDiscrTree.MkDTExpr.M✝ DTExpr

run etaPossibilities, and cache the result if there are multiple possibilities.

partial def Lean.Meta.RefinedDiscrTree.MkDTExpr.mkDTExprsAux (original : Expr) (root : Bool) : Lean.Meta.RefinedDiscrTree.MkDTExpr.M✝ DTExpr

Return all encodings of e as a DTExpr, taking possible η-reductions into account. If root = false, then e is a strict sub expression of the original expression.

def Lean.Meta.RefinedDiscrTree.DTExpr.isSpecific : DTExpr → Bool

Returns true if the DTExpr is not of the form * or Eq * * *".

def Lean.Meta.RefinedDiscrTree.mkDTExpr (e : Expr) (fvarInContext : FVarId → Bool := fun (x : FVarId) => false) : MetaM DTExpr

Return the encoding of e as a DTExpr.

Warning: to account for potential η-reductions of e, use mkDTExprs instead.

The argument fvarInContext allows you to specify which free variables in e will still be in the context when the RefinedDiscrTree is being used for lookup. It should return true only if the RefinedDiscrTree is built and used locally.

def Lean.Meta.RefinedDiscrTree.mkDTExprs (e : Expr) (onlySpecific : Bool) (fvarInContext : FVarId → Bool := fun (x : FVarId) => false) : MetaM (List DTExpr)

Similar to mkDTExpr. Return all encodings of e as a DTExpr, taking potential further η-reductions into account.