Lean.Meta.Match.Basic

source

inductive Lean.Meta.Match.Pattern :

Type

inaccessible: Lean.Expr → Lean.Meta.Match.Pattern
var: Lean.FVarId → Lean.Meta.Match.Pattern
ctor: Lean.Name → List Lean.Level → List Lean.Expr → List Lean.Meta.Match.Pattern → Lean.Meta.Match.Pattern
val: Lean.Expr → Lean.Meta.Match.Pattern
arrayLit: Lean.Expr → List Lean.Meta.Match.Pattern → Lean.Meta.Match.Pattern
as: Lean.FVarId → Lean.Meta.Match.Pattern → Lean.FVarId → Lean.Meta.Match.Pattern

source

instance Lean.Meta.Match.instInhabitedPattern :

Inhabited Lean.Meta.Match.Pattern

Equations

Lean.Meta.Match.instInhabitedPattern = { default := Lean.Meta.Match.Pattern.inaccessible default }

source

partial def Lean.Meta.Match.Pattern.toMessageData :

Lean.Meta.Match.Pattern → Lean.MessageData

source

def Lean.Meta.Match.Pattern.toExpr (p : Lean.Meta.Match.Pattern) (annotate : optParam Bool false) :

Lean.MetaM Lean.Expr

Equations

Lean.Meta.Match.Pattern.toExpr p annotate = (fun visit => visit p) (Lean.Meta.Match.Pattern.toExpr.visit annotate)

source

partial def Lean.Meta.Match.Pattern.toExpr.visit (annotate : optParam Bool false) (p : Lean.Meta.Match.Pattern) :

Lean.MetaM Lean.Expr

source

partial def Lean.Meta.Match.Pattern.applyFVarSubst (s : Lean.Meta.FVarSubst) :

Lean.Meta.Match.Pattern → Lean.Meta.Match.Pattern

source

def Lean.Meta.Match.Pattern.replaceFVarId (fvarId : Lean.FVarId) (v : Lean.Expr) (p : Lean.Meta.Match.Pattern) :

Lean.Meta.Match.Pattern

Equations

Lean.Meta.Match.Pattern.replaceFVarId fvarId v p = let s := { map := ∅ }; Lean.Meta.Match.Pattern.applyFVarSubst (Lean.Meta.FVarSubst.insert s fvarId v) p

source

partial def Lean.Meta.Match.Pattern.hasExprMVar :

Lean.Meta.Match.Pattern → Bool

source

partial def Lean.Meta.Match.instantiatePatternMVars :

Lean.Meta.Match.Pattern → Lean.MetaM Lean.Meta.Match.Pattern

source

structure Lean.Meta.Match.AltLHS :

Type

source

def Lean.Meta.Match.instantiateAltLHSMVars (altLHS : Lean.Meta.Match.AltLHS) :

Lean.MetaM Lean.Meta.Match.AltLHS

Equations

Lean.Meta.Match.instantiateAltLHSMVars altLHS = do let a ← List.mapM Lean.Meta.instantiateLocalDeclMVars altLHS.fvarDecls let a_1 ← List.mapM Lean.Meta.Match.instantiatePatternMVars altLHS.patterns pure { ref := altLHS.ref, fvarDecls := a, patterns := a_1 }

source

structure Lean.Meta.Match.Alt :

Type

ref : Lean.Syntax
idx : Nat
rhs : Lean.Expr
fvarDecls : List Lean.LocalDecl
patterns : List Lean.Meta.Match.Pattern

source

instance Lean.Meta.Match.instInhabitedAlt :

Inhabited Lean.Meta.Match.Alt

Equations

Lean.Meta.Match.instInhabitedAlt = { default := { ref := default, idx := default, rhs := default, fvarDecls := default, patterns := default } }

source

def Lean.Meta.Match.Alt.toMessageData (alt : Lean.Meta.Match.Alt) :

Lean.MetaM Lean.MessageData

Equations

Lean.Meta.Match.Alt.toMessageData alt = Lean.Meta.withExistingLocalDecls alt.fvarDecls (let msg := List.map (fun d => Lean.toMessageData "" ++ Lean.toMessageData (Lean.LocalDecl.toExpr d) ++ Lean.toMessageData ":(" ++ Lean.toMessageData (Lean.LocalDecl.type d) ++ Lean.toMessageData ")") alt.fvarDecls; let msg := Lean.toMessageData "" ++ Lean.toMessageData msg ++ Lean.toMessageData " |- " ++ Lean.toMessageData (List.map Lean.Meta.Match.Pattern.toMessageData alt.patterns) ++ Lean.toMessageData " => " ++ Lean.toMessageData alt.rhs ++ Lean.toMessageData ""; Lean.addMessageContext msg)

source

def Lean.Meta.Match.Alt.applyFVarSubst (s : Lean.Meta.FVarSubst) (alt : Lean.Meta.Match.Alt) :

Lean.Meta.Match.Alt

Equations

Lean.Meta.Match.Alt.applyFVarSubst s alt = { ref := alt.ref, idx := alt.idx, rhs := Lean.Expr.applyFVarSubst s alt.rhs, fvarDecls := List.map (fun d => Lean.LocalDecl.applyFVarSubst s d) alt.fvarDecls, patterns := List.map (fun p => Lean.Meta.Match.Pattern.applyFVarSubst s p) alt.patterns }

source

def Lean.Meta.Match.Alt.replaceFVarId (fvarId : Lean.FVarId) (v : Lean.Expr) (alt : Lean.Meta.Match.Alt) :

Lean.Meta.Match.Alt

Equations

Lean.Meta.Match.Alt.replaceFVarId fvarId v alt = { ref := alt.ref, idx := alt.idx, rhs := Lean.Expr.replaceFVarId alt.rhs fvarId v, fvarDecls := let decls := List.filter (fun d => Lean.LocalDecl.fvarId d != fvarId) alt.fvarDecls; List.map (Lean.replaceFVarIdAtLocalDecl fvarId v) decls, patterns := List.map (fun p => Lean.Meta.Match.Pattern.replaceFVarId fvarId v p) alt.patterns }

source

def Lean.Meta.Match.Alt.checkAndReplaceFVarId (fvarId : Lean.FVarId) (v : Lean.Expr) (alt : Lean.Meta.Match.Alt) :

Lean.MetaM Lean.Meta.Match.Alt

Equations

Lean.Meta.Match.Alt.checkAndReplaceFVarId fvarId v alt = match List.find? (fun fvarDecl => Lean.LocalDecl.fvarId fvarDecl == fvarId) alt.fvarDecls with | none => Lean.throwErrorAt alt.ref (Lean.toMessageData "unknown free pattern variable") | some fvarDecl => do let vType ← Lean.Meta.inferType v let a ← Lean.Meta.isDefEqGuarded (Lean.LocalDecl.type fvarDecl) vType let _do_jp : PUnit → Lean.MetaM Lean.Meta.Match.Alt := fun y => pure (Lean.Meta.Match.Alt.replaceFVarId fvarId v alt) if a = true then do let y ← pure PUnit.unit _do_jp y else do let y ← Lean.Meta.withExistingLocalDecls alt.fvarDecls do let discr ← Lean.Meta.addPPExplicitToExposeDiff vType (Lean.LocalDecl.type fvarDecl) let x : Lean.Expr × Lean.Expr := discr match x with | (expectedType, givenType) => Lean.throwErrorAt alt.ref (Lean.toMessageData "type mismatch during dependent match-elimination at pattern variable '" ++ Lean.toMessageData (Lean.mkFVar (Lean.LocalDecl.fvarId fvarDecl)) ++ Lean.toMessageData "' with type" ++ Lean.toMessageData (Lean.indentExpr givenType) ++ Lean.toMessageData "\nexpected type" ++ Lean.toMessageData (Lean.indentExpr expectedType) ++ Lean.toMessageData "") _do_jp y

source

inductive Lean.Meta.Match.Example :

Type

var: Lean.FVarId → Lean.Meta.Match.Example
underscore: Lean.Meta.Match.Example
ctor: Lean.Name → List Lean.Meta.Match.Example → Lean.Meta.Match.Example
val: Lean.Expr → Lean.Meta.Match.Example
arrayLit: List Lean.Meta.Match.Example → Lean.Meta.Match.Example

source

partial def Lean.Meta.Match.Example.replaceFVarId (fvarId : Lean.FVarId) (ex : Lean.Meta.Match.Example) :

Lean.Meta.Match.Example → Lean.Meta.Match.Example

source

partial def Lean.Meta.Match.Example.applyFVarSubst (s : Lean.Meta.FVarSubst) :

Lean.Meta.Match.Example → Lean.Meta.Match.Example

source

partial def Lean.Meta.Match.Example.varsToUnderscore :

Lean.Meta.Match.Example → Lean.Meta.Match.Example

source

partial def Lean.Meta.Match.Example.toMessageData :

Lean.Meta.Match.Example → Lean.MessageData

source

def Lean.Meta.Match.examplesToMessageData (cex : List Lean.Meta.Match.Example) :

Lean.MessageData

Equations

Lean.Meta.Match.examplesToMessageData cex = Lean.MessageData.joinSep (List.map (Lean.Meta.Match.Example.toMessageData ∘ Lean.Meta.Match.Example.varsToUnderscore) cex) (Function.comp Lean.MessageData.ofFormat Lean.format ", ")

source

structure Lean.Meta.Match.Problem :

Type

source

instance Lean.Meta.Match.instInhabitedProblem :

Inhabited Lean.Meta.Match.Problem

Equations

Lean.Meta.Match.instInhabitedProblem = { default := { mvarId := default, vars := default, alts := default, examples := default } }

source

def Lean.Meta.Match.withGoalOf {α : Type} (p : Lean.Meta.Match.Problem) (x : Lean.MetaM α) :

Lean.MetaM α

Equations

Lean.Meta.Match.withGoalOf p x = Lean.Meta.withMVarContext p.mvarId x

source

def Lean.Meta.Match.Problem.toMessageData (p : Lean.Meta.Match.Problem) :

Lean.MetaM Lean.MessageData

Equations

Lean.Meta.Match.Problem.toMessageData p = Lean.Meta.Match.withGoalOf p do let alts ← List.mapM Lean.Meta.Match.Alt.toMessageData p.alts let vars ← List.mapM (fun x => do let xType ← Lean.Meta.inferType x pure (Lean.toMessageData "" ++ Lean.toMessageData x ++ Lean.toMessageData ":(" ++ Lean.toMessageData xType ++ Lean.toMessageData ")")) p.vars pure (Lean.toMessageData "remaining variables: " ++ Lean.toMessageData vars ++ Lean.toMessageData "\nalternatives:" ++ Lean.toMessageData (Lean.indentD (Lean.MessageData.joinSep alts (Lean.MessageData.ofFormat Lean.Format.line))) ++ Lean.toMessageData "\nexamples:" ++ Lean.toMessageData (Lean.Meta.Match.examplesToMessageData p.examples) ++ Lean.toMessageData "\n")

source

@[inline]

abbrev Lean.Meta.Match.CounterExample :

Type

Equations

Lean.Meta.Match.CounterExample = List Lean.Meta.Match.Example

source

def Lean.Meta.Match.counterExampleToMessageData (cex : Lean.Meta.Match.CounterExample) :

Lean.MessageData

Equations

Lean.Meta.Match.counterExampleToMessageData cex = Lean.Meta.Match.examplesToMessageData cex

source

def Lean.Meta.Match.counterExamplesToMessageData (cexs : List Lean.Meta.Match.CounterExample) :

Lean.MessageData

Equations

Lean.Meta.Match.counterExamplesToMessageData cexs = Lean.MessageData.joinSep (List.map Lean.Meta.Match.counterExampleToMessageData cexs) (Lean.MessageData.ofFormat Lean.Format.line)

source

structure Lean.Meta.Match.MatcherResult :

Type

matcher : Lean.Expr
counterExamples : List Lean.Meta.Match.CounterExample
unusedAltIdxs : List Nat
addMatcher : Lean.MetaM Unit

source

partial def Lean.Meta.Match.toPattern (e : Lean.Expr) :

Lean.MetaM Lean.Meta.Match.Pattern