Lean.Meta.Match.MatcherInfo

Lean.Meta.Match.Extension.instInhabitedState = { default := { map := { stage₁ := true, map₁ := ∅, map₂ := { root := Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray, size := 0 } } } }

source

def Lean.Meta.Match.Extension.State.addEntry (s : Lean.Meta.Match.Extension.State) (e : Lean.Meta.Match.Extension.Entry) :

Lean.Meta.Match.Extension.State

Equations

Lean.Meta.Match.Extension.State.addEntry s e = { map := Lean.SMap.insert s.map e.name e.info }

source

def Lean.Meta.Match.Extension.State.switch (s : Lean.Meta.Match.Extension.State) :

Lean.Meta.Match.Extension.State

Equations

Lean.Meta.Match.Extension.State.switch s = { map := Lean.SMap.switch s.map }

source

constant Lean.Meta.Match.Extension.extension :

Lean.SimplePersistentEnvExtension Lean.Meta.Match.Extension.Entry Lean.Meta.Match.Extension.State

source

def Lean.Meta.Match.Extension.addMatcherInfo (env : Lean.Environment) (matcherName : Lean.Name) (info : Lean.Meta.MatcherInfo) :

Lean.Environment

Equations

Lean.Meta.Match.Extension.addMatcherInfo env matcherName info = Lean.PersistentEnvExtension.addEntry Lean.Meta.Match.Extension.extension env { name := matcherName, info := info }

source

def Lean.Meta.Match.Extension.getMatcherInfo? (env : Lean.Environment) (declName : Lean.Name) :

Option Lean.Meta.MatcherInfo

Equations

Lean.Meta.Match.Extension.getMatcherInfo? env declName = Lean.SMap.find? (Lean.SimplePersistentEnvExtension.getState Lean.Meta.Match.Extension.extension env).map declName

source

def Lean.Meta.Match.addMatcherInfo (matcherName : Lean.Name) (info : Lean.Meta.MatcherInfo) :

Lean.MetaM Unit

Equations

Lean.Meta.Match.addMatcherInfo matcherName info = Lean.modifyEnv fun env => Lean.Meta.Match.Extension.addMatcherInfo env matcherName info

source

def Lean.Meta.getMatcherInfoCore? (env : Lean.Environment) (declName : Lean.Name) :

Option Lean.Meta.MatcherInfo

Equations

Lean.Meta.getMatcherInfoCore? env declName = Lean.Meta.Match.Extension.getMatcherInfo? env declName

source

def Lean.Meta.getMatcherInfo? {m : Type → Type} [inst : Monad m] [inst : Lean.MonadEnv m] (declName : Lean.Name) :

m (Option Lean.Meta.MatcherInfo)

Equations

Lean.Meta.getMatcherInfo? declName = do let a ← Lean.getEnv pure (Lean.Meta.getMatcherInfoCore? a declName)

source

def Lean.Meta.isMatcherCore (env : Lean.Environment) (declName : Lean.Name) :

Bool

Equations

Lean.Meta.isMatcherCore env declName = Option.isSome (Lean.Meta.getMatcherInfoCore? env declName)

source

def Lean.Meta.isMatcher {m : Type → Type} [inst : Monad m] [inst : Lean.MonadEnv m] (declName : Lean.Name) :

m Bool

Equations

Lean.Meta.isMatcher declName = do let a ← Lean.getEnv pure (Lean.Meta.isMatcherCore a declName)

source

def Lean.Meta.isMatcherAppCore? (env : Lean.Environment) (e : Lean.Expr) :

Option Lean.Meta.MatcherInfo

Equations

Lean.Meta.isMatcherAppCore? env e = let fn := Lean.Expr.getAppFn e; if Lean.Expr.isConst fn = true then match Lean.Meta.getMatcherInfoCore? env (Lean.Expr.constName! fn) with | some matcherInfo => if Lean.Expr.getAppNumArgs e ≥ Lean.Meta.Match.MatcherInfo.arity matcherInfo then some matcherInfo else none | x => none else none

source

def Lean.Meta.isMatcherAppCore (env : Lean.Environment) (e : Lean.Expr) :

Bool

Equations

Lean.Meta.isMatcherAppCore env e = Option.isSome (Lean.Meta.isMatcherAppCore? env e)

source

def Lean.Meta.isMatcherApp {m : Type → Type} [inst : Monad m] [inst : Lean.MonadEnv m] (e : Lean.Expr) :

m Bool

Equations

Lean.Meta.isMatcherApp e = do let a ← Lean.getEnv pure (Lean.Meta.isMatcherAppCore a e)

source

structure Lean.Meta.MatcherApp :

Type

matcherName : Lean.Name
matcherLevels : Array Lean.Level
uElimPos? : Option Nat
params : Array Lean.Expr
motive : Lean.Expr
discrs : Array Lean.Expr
altNumParams : Array Nat
alts : Array Lean.Expr
remaining : Array Lean.Expr

source

def Lean.Meta.matchMatcherApp? {m : Type → Type} [inst : Monad m] [inst : Lean.MonadEnv m] (e : Lean.Expr) :

m (Option Lean.Meta.MatcherApp)

Equations

Lean.Meta.matchMatcherApp? e = match Lean.Expr.getAppFn e with | Lean.Expr.const declName declLevels x => do let a ← Lean.Meta.getMatcherInfo? declName match a with | none => pure none | some info => let args := Lean.Expr.getAppArgs e; if Array.size args < Lean.Meta.Match.MatcherInfo.arity info then pure none else pure (some { matcherName := declName, matcherLevels := List.toArray declLevels, uElimPos? := info.uElimPos?, params := Array.extract args 0 info.numParams, motive := Array.getOp args (Lean.Meta.Match.MatcherInfo.getMotivePos info), discrs := Array.ofSubarray (Array.toSubarray args (info.numParams + 1) (info.numParams + 1 + info.numDiscrs)), altNumParams := info.altNumParams, alts := Array.ofSubarray (Array.toSubarray args (info.numParams + 1 + info.numDiscrs) (info.numParams + 1 + info.numDiscrs + Lean.Meta.Match.MatcherInfo.numAlts info)), remaining := Array.ofSubarray (Array.toSubarray args (info.numParams + 1 + info.numDiscrs + Lean.Meta.Match.MatcherInfo.numAlts info) (Array.size args)) }) | x => pure none

source

def Lean.Meta.MatcherApp.toExpr (matcherApp : Lean.Meta.MatcherApp) :

Lean.Expr

Equations

Lean.Meta.MatcherApp.toExpr matcherApp = let result := Lean.mkAppN (Lean.mkConst matcherApp.matcherName (Array.toList matcherApp.matcherLevels)) matcherApp.params; let result := Lean.mkApp result matcherApp.motive; let result := Lean.mkAppN result matcherApp.discrs; let result := Lean.mkAppN result matcherApp.alts; Lean.mkAppN result matcherApp.remaining