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 Lean.MVarId → Lean.Meta.RefinedDiscrTree.DTExpr

  A metavariable. It optionally stores an MVarId.

• opaque : Lean.Meta.RefinedDiscrTree.DTExpr

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

• const : Lean.Name → Array Lean.Meta.RefinedDiscrTree.DTExpr → Lean.Meta.RefinedDiscrTree.DTExpr

  A constant. It stores the name and the arguments.

• fvar : Lean.FVarId → Array Lean.Meta.RefinedDiscrTree.DTExpr → Lean.Meta.RefinedDiscrTree.DTExpr

  A free variable. It stores the FVarId and the arguments

• bvar : ℕ → Array Lean.Meta.RefinedDiscrTree.DTExpr → Lean.Meta.RefinedDiscrTree.DTExpr

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

• lit : Lean.Literal → Lean.Meta.RefinedDiscrTree.DTExpr

  A literal.

• sort : Lean.Meta.RefinedDiscrTree.DTExpr

  A sort.

• lam : Lean.Meta.RefinedDiscrTree.DTExpr → Lean.Meta.RefinedDiscrTree.DTExpr

  A lambda function. It stores the body.

• forall : Lean.Meta.RefinedDiscrTree.DTExpr → Lean.Meta.RefinedDiscrTree.DTExpr → Lean.Meta.RefinedDiscrTree.DTExpr

  A dependent arrow. It stores the domain and body.

• proj : Lean.Name → ℕ → Lean.Meta.RefinedDiscrTree.DTExpr → Array Lean.Meta.RefinedDiscrTree.DTExpr → Lean.Meta.RefinedDiscrTree.DTExpr

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

instance Lean.Meta.RefinedDiscrTree.instInhabitedDTExpr : Inhabited Lean.Meta.RefinedDiscrTree.DTExpr

Equations

• Lean.Meta.RefinedDiscrTree.instInhabitedDTExpr = { default := Lean.Meta.RefinedDiscrTree.DTExpr.star default }

instance Lean.Meta.RefinedDiscrTree.instBEqDTExpr : BEq Lean.Meta.RefinedDiscrTree.DTExpr

Equations

• Lean.Meta.RefinedDiscrTree.instBEqDTExpr = { beq := Lean.Meta.RefinedDiscrTree.beqDTExpr✝ }

instance Lean.Meta.RefinedDiscrTree.instReprDTExpr : Repr Lean.Meta.RefinedDiscrTree.DTExpr

Equations

• Lean.Meta.RefinedDiscrTree.instReprDTExpr = { reprPrec := Lean.Meta.RefinedDiscrTree.reprDTExpr✝ }

instance Lean.Meta.RefinedDiscrTree.instToFormatDTExpr : Std.ToFormat Lean.Meta.RefinedDiscrTree.DTExpr

Equations

• Lean.Meta.RefinedDiscrTree.instToFormatDTExpr = { format := Lean.Meta.RefinedDiscrTree.DTExpr.format✝ }

partial def Lean.Meta.RefinedDiscrTree.DTExpr.size : Lean.Meta.RefinedDiscrTree.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 : Lean.Meta.RefinedDiscrTree.DTExpr) : Bool

Determine if two DTExprs are equivalent.

Equations

• a.eqv b = StateT.run' (Lean.Meta.RefinedDiscrTree.DTExpr.eqv.go a b) ∅

@[irreducible]

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

@[irreducible]

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

Equations

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

Encoding an Expr

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

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

Equations

• e.flatten initCapacity = StateT.run' (Lean.Meta.RefinedDiscrTree.DTExpr.flattenAux✝ (Array.mkEmpty initCapacity) e) { stars := #[] }

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

Reduction procedure for the RefinedDiscrTree indexing.

@[specialize #[]]

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

Repeatedly apply reduce while stripping lambda binders and introducing their variables

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

Check whether the expression is represented by Key.star.

Equations

• Lean.Meta.RefinedDiscrTree.isStar (Lean.Expr.mvar mvarId) = true
• Lean.Meta.RefinedDiscrTree.isStar (f.app arg) = Lean.Meta.RefinedDiscrTree.isStar f
• Lean.Meta.RefinedDiscrTree.isStar x✝ = false

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

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

Equations

• Lean.Meta.RefinedDiscrTree.isStarWithArg arg (f.app a) = if (a == arg) = true then Lean.Meta.RefinedDiscrTree.isStar f else Lean.Meta.RefinedDiscrTree.isStarWithArg arg f
• Lean.Meta.RefinedDiscrTree.isStarWithArg arg x✝ = false

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

Return true if e contains a loose bound variable.

Equations

• e.hasLooseBVars = Lean.Meta.RefinedDiscrTree.DTExpr.hasLooseBVarsAux✝ 0 e

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

Return for each argument whether it should be ignored.

Equations

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

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

Return whether the argument should be ignored.

Equations

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

partial def Lean.Meta.RefinedDiscrTree.MkDTExpr.mkDTExprAux (e : Lean.Expr) (root : Bool) : ReaderT Lean.Meta.RefinedDiscrTree.MkDTExpr.Context✝ Lean.MetaM Lean.Meta.RefinedDiscrTree.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 : Lean.MonadCache Lean.Expr Lean.Meta.RefinedDiscrTree.DTExpr Lean.Meta.RefinedDiscrTree.MkDTExpr.M✝

Equations

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

@[specialize #[]]

def Lean.Meta.RefinedDiscrTree.MkDTExpr.etaPossibilities {α : Type} (e : Lean.Expr) (lambdas : List Lean.FVarId) (k : Lean.Expr → List Lean.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

Equations

• One or more equations did not get rendered due to their size.
• Lean.Meta.RefinedDiscrTree.MkDTExpr.etaPossibilities e lambdas k = (k e lambdas <|> failure)

@[specialize #[]]

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

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

Equations

• One or more equations did not get rendered due to their size.
• Lean.Meta.RefinedDiscrTree.MkDTExpr.cacheEtaPossibilities e original lambdas k = k e lambdas

partial def Lean.Meta.RefinedDiscrTree.MkDTExpr.mkDTExprsAux (original : Lean.Expr) (root : Bool) : Lean.Meta.RefinedDiscrTree.MkDTExpr.M✝ Lean.Meta.RefinedDiscrTree.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 : Lean.Meta.RefinedDiscrTree.DTExpr → Bool

Equations

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

def Lean.Meta.RefinedDiscrTree.mkDTExpr (e : Lean.Expr) (fvarInContext : Lean.FVarId → Bool := fun (x : Lean.FVarId) => false) : Lean.MetaM Lean.Meta.RefinedDiscrTree.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.

Equations

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

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

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

Equations

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