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

Equations

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

instance Lean.Meta.RefinedDiscrTree.instBEqDTExpr : BEq DTExpr

Equations

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

instance Lean.Meta.RefinedDiscrTree.instReprDTExpr : Repr DTExpr

Equations

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

instance Lean.Meta.RefinedDiscrTree.instToFormatDTExpr : ToFormat DTExpr

Equations

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

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.

Equations

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

@[irreducible]

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

Equations

• One or more equations did not get rendered due to their size.
• Lean.Meta.RefinedDiscrTree.DTExpr.eqv.go Lean.Meta.RefinedDiscrTree.DTExpr.opaque Lean.Meta.RefinedDiscrTree.DTExpr.opaque = pure true
• Lean.Meta.RefinedDiscrTree.DTExpr.eqv.go (Lean.Meta.RefinedDiscrTree.DTExpr.lit li₁) (Lean.Meta.RefinedDiscrTree.DTExpr.lit li₂) = pure (li₁ == li₂)
• Lean.Meta.RefinedDiscrTree.DTExpr.eqv.go Lean.Meta.RefinedDiscrTree.DTExpr.sort Lean.Meta.RefinedDiscrTree.DTExpr.sort = pure true
• Lean.Meta.RefinedDiscrTree.DTExpr.eqv.go b₁.lam b₂.lam = Lean.Meta.RefinedDiscrTree.DTExpr.eqv.go b₁ b₂
• Lean.Meta.RefinedDiscrTree.DTExpr.eqv.go (d₁.forall b₁) (d₂.forall b₂) = (Lean.Meta.RefinedDiscrTree.DTExpr.eqv.go d₁ d₂ <&&> Lean.Meta.RefinedDiscrTree.DTExpr.eqv.go b₁ b₂)
• Lean.Meta.RefinedDiscrTree.DTExpr.eqv.go (Lean.Meta.RefinedDiscrTree.DTExpr.star none) (Lean.Meta.RefinedDiscrTree.DTExpr.star none) = pure true
• Lean.Meta.RefinedDiscrTree.DTExpr.eqv.go a b = pure false

@[irreducible]

def Lean.Meta.RefinedDiscrTree.DTExpr.eqv.goArray (as bs : Array DTExpr) : StateM (Std.HashMap MVarId 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 : DTExpr) (initCapacity : ℕ := 16) : Array 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) { }

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.

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 : Expr) : 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 : 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 : Expr) (args : Array Expr) : 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 : Expr) (binderInfo : BinderInfo) : 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 : 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✝

Equations

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

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

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 : 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.

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 : 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 * * *".

Equations

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

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.

Equations

• Lean.Meta.RefinedDiscrTree.mkDTExpr e fvarInContext = Lean.Meta.withReducible ((Lean.Meta.RefinedDiscrTree.MkDTExpr.mkDTExprAux e true).run { fvarInContext := fvarInContext })

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.

Equations

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