Lean.Elab.Match

source

def Lean.Elab.Term.isAuxDiscrName (n : Lean.Name) :

Bool

Equations

Lean.Elab.Term.isAuxDiscrName n = (Lean.Name.hasMacroScopes n && Lean.Name.eraseMacroScopes n == `_discr)

source

def Lean.Elab.Term.isAtomicDiscr? (discr : Lean.Syntax) :

Lean.Elab.TermElabM (Option Lean.Expr)

Equations

Lean.Elab.Term.isAtomicDiscr? discr = let discr := discr; cond (Lean.Syntax.isOfKind discr `ident) (let x := discr; Lean.Elab.Term.isLocalIdent? x) (let discr := discr; if Lean.Syntax.isOfKind discr `Lean.Parser.Term.explicit = true then let discr_1 := Lean.Syntax.getArg discr 0; let discr_2 := Lean.Syntax.getArg discr 1; cond (Lean.Syntax.isOfKind discr_2 `ident) (let x := discr_2; Lean.Elab.Term.isLocalIdent? x) (let discr := Lean.Syntax.getArg discr 1; if Lean.Syntax.isMissing discr = true then Lean.Elab.throwAbortTerm else pure none) else let discr := discr; if Lean.Syntax.isMissing discr = true then Lean.Elab.throwAbortTerm else pure none)

source

structure Lean.Elab.Term.ElabMatchTypeAndDiscrsResult :

Type

discrs : Array Lean.Expr
matchType : Lean.Expr
isDep : Bool
alts : Array Lean.Elab.Term.MatchAltView

source

def Lean.Elab.Term.expandMacrosInPatterns (matchAlts : Array Lean.Elab.Term.MatchAltView) :

Lean.MacroM (Array Lean.Elab.Term.MatchAltView)

Equations

Lean.Elab.Term.expandMacrosInPatterns matchAlts = Array.mapM (fun matchAlt => do let patterns ← Array.mapM Lean.expandMacros matchAlt.patterns pure { ref := matchAlt.ref, patterns := patterns, rhs := matchAlt.rhs }) matchAlts

source

def Lean.Elab.Term.elabMVarWithIdKind :

Lean.Elab.Term.TermElab

Equations

Lean.Elab.Term.elabMVarWithIdKind stx expectedType? = pure (Lean.mkInaccessible (Lean.mkMVar (Lean.Elab.Term.getMVarSyntaxMVarId stx)))

source

def Lean.Elab.Term.elabInaccessible :

Lean.Elab.Term.TermElab

Equations

Lean.Elab.Term.elabInaccessible stx expectedType? = do let e ← Lean.Elab.Term.elabTerm (Lean.Syntax.getOp stx 1) expectedType? true true pure (Lean.mkInaccessible e)

source

def Lean.Elab.Term.precheckMatch :

Lean.Elab.Term.Quotation.Precheck

Equations

Lean.Elab.Term.precheckMatch x = let discr := x; if Lean.Syntax.isOfKind discr `Lean.Parser.Term.match = true then let discr_1 := Lean.Syntax.getArg discr 0; let discr_2 := Lean.Syntax.getArg discr 1; if Lean.Syntax.matchesNull discr_2 0 = true then let discr_3 := Lean.Syntax.getArg discr 2; match OptionM.run (Array.sequenceMap (Array.getSepElems (Lean.Syntax.getArgs discr_3)) fun x => let discr := x; if Lean.Syntax.isOfKind discr `Lean.Parser.Term.matchDiscr = true then let discr_4 := Lean.Syntax.getArg discr 0; if Lean.Syntax.matchesNull discr_4 0 = true then let discr := Lean.Syntax.getArg discr 1; let discrs := discr; some discrs else let discr_5 := Lean.Syntax.getArg discr 0; let discr := Lean.Syntax.getArg discr 1; none else let discr := x; none) with | some discrs => let discr_4 := Lean.Syntax.getArg discr 3; if Lean.Syntax.matchesNull discr_4 0 = true then let discr_5 := Lean.Syntax.getArg discr 4; let discr_6 := Lean.Syntax.getArg discr 5; if Lean.Syntax.isOfKind discr_6 `Lean.Parser.Term.matchAlts = true then let discr := Lean.Syntax.getArg discr_6 0; match OptionM.run (Array.sequenceMap (Lean.Syntax.getArgs discr) fun x => let discr := x; if Lean.Syntax.isOfKind discr `Lean.Parser.Term.matchAlt = true then let discr_7 := Lean.Syntax.getArg discr 0; let discr_8 := Lean.Syntax.getArg discr 1; match OptionM.run (Array.sequenceMap (Array.getSepElems (Lean.Syntax.getArgs discr_8)) fun x => let discr := x; let patss := discr; some patss) with | some patss => let discr_9 := Lean.Syntax.getArg discr 2; let discr := Lean.Syntax.getArg discr 3; let rhss := discr; some (patss, rhss) | none => let discr_9 := Lean.Syntax.getArg discr 1; let discr_10 := Lean.Syntax.getArg discr 2; let discr := Lean.Syntax.getArg discr 3; none else let discr := x; none) with | some tuples => let rhss := Array.map (fun x => match x with | (patss, rhss) => rhss) tuples; let patss := Array.map (fun x => match x with | (patss, rhss) => patss) tuples; do Array.forM Lean.Elab.Term.Quotation.precheck discrs 0 (Array.size discrs) let r ← let col := Array.zip patss rhss; forIn col { fst := none, snd := PUnit.unit } fun x r => match x with | (pats, rhs) => let r := r.snd; let _do_jp := fun vars => do Lean.Elab.Term.Quotation.withNewLocals (Lean.Elab.Term.getPatternVarNames vars) (Lean.Elab.Term.Quotation.precheck rhs) pure (ForInStep.yield { fst := none, snd := PUnit.unit }); do let r ← tryCatch (do let y ← liftM (Lean.Elab.Term.getPatternsVars pats) pure (DoResultPR.pure y PUnit.unit)) fun ex => match ex with | x => pure (DoResultPR.return PUnit.unit PUnit.unit) match r with | DoResultPR.pure a u => let x := u; do let y ← pure a _do_jp y | DoResultPR.return b u => let x := u; pure (ForInStep.done { fst := some b, snd := PUnit.unit }) let x : PUnit := r.snd match r.fst with | none => pure PUnit.unit | some a => pure a | none => let discr := Lean.Syntax.getArg discr_6 0; Lean.Elab.throwUnsupportedSyntax else let discr := Lean.Syntax.getArg discr 5; Lean.Elab.throwUnsupportedSyntax else let discr_5 := Lean.Syntax.getArg discr 3; let discr_6 := Lean.Syntax.getArg discr 4; let discr := Lean.Syntax.getArg discr 5; Lean.Elab.throwUnsupportedSyntax | none => let discr_4 := Lean.Syntax.getArg discr 2; let discr_5 := Lean.Syntax.getArg discr 3; let discr_6 := Lean.Syntax.getArg discr 4; let discr := Lean.Syntax.getArg discr 5; Lean.Elab.throwUnsupportedSyntax else let discr_3 := Lean.Syntax.getArg discr 1; let discr_4 := Lean.Syntax.getArg discr 2; let discr_5 := Lean.Syntax.getArg discr 3; let discr_6 := Lean.Syntax.getArg discr 4; let discr := Lean.Syntax.getArg discr 5; Lean.Elab.throwUnsupportedSyntax else let discr := x; Lean.Elab.throwUnsupportedSyntax

source

inductive Lean.Elab.Term.PatternVarDecl :

Type

anonymousVar: Lean.MVarId → Lean.FVarId → Lean.Elab.Term.PatternVarDecl
localVar: Lean.FVarId → Lean.Elab.Term.PatternVarDecl

source

structure Lean.Elab.Term.PatternElabException :

Type

ex : Lean.Exception
patternIdx : Nat
pathToIndex : List Nat

source

def Lean.Elab.Term.finalizePatternDecls (patternVarDecls : Array Lean.Elab.Term.PatternVarDecl) :

Lean.Elab.TermElabM (Array Lean.LocalDecl)

Equations

Lean.Elab.Term.finalizePatternDecls patternVarDecls = let decls := #[]; do let r ← forIn patternVarDecls decls fun pdecl r => let decls := r; match pdecl with | Lean.Elab.Term.PatternVarDecl.localVar fvarId => do let decl ← liftM (Lean.Meta.getLocalDecl fvarId) let decl ← liftM (Lean.Meta.instantiateLocalDeclMVars decl) let decls : Array Lean.LocalDecl := Array.push decls decl pure PUnit.unit pure (ForInStep.yield decls) | Lean.Elab.Term.PatternVarDecl.anonymousVar mvarId fvarId => do let e ← liftM (Lean.Meta.instantiateMVars (Lean.mkMVar mvarId)) let cls : Lean.Name := `Elab.match let a ← Lean.isTracingEnabledFor cls let _do_jp : Array Lean.LocalDecl → Unit → Lean.Elab.TermElabM (ForInStep (Array Lean.LocalDecl)) := fun decls y => match e with | Lean.Expr.mvar newMVarId x => do liftM (Lean.Meta.assignExprMVar newMVarId (Lean.mkFVar fvarId)) let cls : Lean.Name := `Elab.match let a ← Lean.isTracingEnabledFor cls let _do_jp : Array Lean.LocalDecl → Unit → Lean.Elab.TermElabM (ForInStep (Array Lean.LocalDecl)) := fun decls y => do let decl ← liftM (Lean.Meta.getLocalDecl fvarId) let decl ← liftM (Lean.Meta.instantiateLocalDeclMVars decl) let decls : Array Lean.LocalDecl := Array.push decls decl pure PUnit.unit pure (ForInStep.yield decls) if a = true then do let y ← Lean.addTrace cls (Lean.toMessageData "finalizePatternDecls: " ++ Lean.toMessageData (Lean.mkMVar newMVarId) ++ Lean.toMessageData " := " ++ Lean.toMessageData (Lean.mkFVar fvarId) ++ Lean.toMessageData "") _do_jp decls y else do let y ← pure PUnit.unit _do_jp decls y | x => do pure () pure (ForInStep.yield decls) if a = true then do let y ← Lean.addTrace cls (Lean.toMessageData "finalizePatternDecls: mvarId: " ++ Lean.toMessageData mvarId.name ++ Lean.toMessageData " := " ++ Lean.toMessageData e ++ Lean.toMessageData ", fvar: " ++ Lean.toMessageData (Lean.mkFVar fvarId) ++ Lean.toMessageData "") _do_jp decls y else do let y ← pure PUnit.unit _do_jp decls y let x : Array Lean.LocalDecl := r let decls : Array Lean.LocalDecl := x liftM (Lean.Meta.sortLocalDecls decls)

source

structure Lean.Elab.Term.ToDepElimPattern.State :

Type

found : Lean.FVarIdSet
localDecls : Array Lean.LocalDecl
newLocals : Lean.FVarIdSet

source

@[inline]

abbrev Lean.Elab.Term.ToDepElimPattern.M (α : Type) :

Type

Equations

Lean.Elab.Term.ToDepElimPattern.M = StateRefT' IO.RealWorld Lean.Elab.Term.ToDepElimPattern.State Lean.Elab.TermElabM

source

partial def Lean.Elab.Term.ToDepElimPattern.main (e : Lean.Expr) :

Lean.Elab.Term.ToDepElimPattern.M Lean.Meta.Match.Pattern

source

def Lean.Elab.Term.withDepElimPatterns {α : Type} (localDecls : Array Lean.LocalDecl) (ps : Array Lean.Expr) (k : Array Lean.LocalDecl → Array Lean.Meta.Match.Pattern → Lean.Elab.TermElabM α) :

Lean.Elab.TermElabM α

Equations

Lean.Elab.Term.withDepElimPatterns localDecls ps k = do let discr ← StateRefT'.run (Array.mapM Lean.Elab.Term.ToDepElimPattern.main ps) { found := ∅, localDecls := localDecls, newLocals := ∅ } let x : Array Lean.Meta.Match.Pattern × Lean.Elab.Term.ToDepElimPattern.State := discr match x with | (patterns, s) => do let localDecls ← Array.mapM (fun d => liftM (Lean.Meta.instantiateLocalDeclMVars d)) s.localDecls let lctx ← Lean.getLCtx let lctx : Lean.LocalContext := Array.foldl (fun lctx d => Lean.LocalContext.erase lctx (Lean.LocalDecl.fvarId d)) lctx localDecls 0 (Array.size localDecls) let lctx : Lean.LocalContext := Array.foldl (fun lctx d => Lean.LocalContext.addDecl lctx d) lctx localDecls 0 (Array.size localDecls) withTheReader Lean.Meta.Context (fun ctx => { config := ctx.config, lctx := lctx, localInstances := ctx.localInstances, defEqCtx? := ctx.defEqCtx?, synthPendingDepth := ctx.synthPendingDepth, canUnfold? := ctx.canUnfold? }) (k localDecls patterns)

source

def Lean.Elab.Term.mkMatcher (input : Lean.Meta.Match.MkMatcherInput) :

Lean.Elab.TermElabM Lean.Meta.Match.MatcherResult

Equations

Lean.Elab.Term.mkMatcher input = liftM (Lean.Meta.Match.mkMatcher input)

source

constant Lean.Elab.Term.match.ignoreUnusedAlts :

Lean.Option Bool

source

def Lean.Elab.Term.reportMatcherResultErrors (altLHSS : List Lean.Meta.Match.AltLHS) (result : Lean.Meta.Match.MatcherResult) :

Lean.Elab.TermElabM Unit

Equations

Lean.Elab.Term.reportMatcherResultErrors altLHSS result = let _do_jp := fun y => do let a ← Lean.getOptions if (Lean.Option.get a Lean.Elab.Term.match.ignoreUnusedAlts || List.isEmpty result.unusedAltIdxs) = true then pure PUnit.unit else let i := 0; do let r ← forIn altLHSS i fun alt r => let i := r; let _do_jp := fun i y => let i := i + 1; do pure PUnit.unit pure (ForInStep.yield i); if List.contains result.unusedAltIdxs i = true then do let y ← Lean.withRef alt.ref (Lean.Elab.logError (Function.comp Lean.MessageData.ofFormat Lean.format "redundant alternative")) _do_jp i y else do let y ← pure PUnit.unit _do_jp i y let x : Nat := r let i : Nat := x pure PUnit.unit; if List.isEmpty result.counterExamples = true then do let y ← pure PUnit.unit _do_jp y else do let y ← Lean.withHeadRefOnly (Lean.Elab.logError (Lean.toMessageData "missing cases:\n" ++ Lean.toMessageData (Lean.Meta.Match.counterExamplesToMessageData result.counterExamples) ++ Lean.toMessageData "")) _do_jp y

source

def Lean.Elab.Term.elabMatch :

Lean.Elab.Term.TermElab

Equations

Lean.Elab.Term.elabMatch = (fun elabMatchDefault stx expectedType? => let discr := stx; if Lean.Syntax.isOfKind discr `Lean.Parser.Term.match = true then let discr_1 := Lean.Syntax.getArg discr 0; let discr_2 := Lean.Syntax.getArg discr 1; if Lean.Syntax.matchesNull discr_2 0 = true then let discr_3 := Lean.Syntax.getArg discr 2; if Lean.Syntax.matchesNull discr_3 1 = true then let discr_4 := Lean.Syntax.getArg discr_3 0; if Lean.Syntax.isOfKind discr_4 `Lean.Parser.Term.matchDiscr = true then let discr_5 := Lean.Syntax.getArg discr_4 0; if Lean.Syntax.matchesNull discr_5 0 = true then let discr_6 := Lean.Syntax.getArg discr_4 1; let discr_7 := Lean.Syntax.getArg discr 3; if Lean.Syntax.matchesNull discr_7 0 = true then let discr_8 := Lean.Syntax.getArg discr 4; let discr_9 := Lean.Syntax.getArg discr 5; if Lean.Syntax.isOfKind discr_9 `Lean.Parser.Term.matchAlts = true then let discr := Lean.Syntax.getArg discr_9 0; if Lean.Syntax.matchesNull discr 1 = true then let discr_10 := Lean.Syntax.getArg discr 0; if Lean.Syntax.isOfKind discr_10 `Lean.Parser.Term.matchAlt = true then let discr := Lean.Syntax.getArg discr_10 0; let discr := Lean.Syntax.getArg discr_10 1; if Lean.Syntax.matchesNull discr 1 = true then let discr_11 := Lean.Syntax.getArg discr 0; cond (Lean.Syntax.isOfKind discr_11 `ident) (let discr := Lean.Syntax.getArg discr_10 2; let discr := Lean.Syntax.getArg discr_10 3; let rhs := discr; let y := discr_11; let discr := discr_6; do let a ← Lean.Elab.Term.isPatternVar y if a = true then Lean.Elab.Term.expandSimpleMatch stx discr y rhs expectedType? else elabMatchDefault stx expectedType?) (let discr := Lean.Syntax.getArg discr 0; let discr := Lean.Syntax.getArg discr_10 2; let discr := Lean.Syntax.getArg discr_10 3; elabMatchDefault stx expectedType?) else let discr := Lean.Syntax.getArg discr_10 1; let discr := Lean.Syntax.getArg discr_10 2; let discr := Lean.Syntax.getArg discr_10 3; elabMatchDefault stx expectedType? else let discr := Lean.Syntax.getArg discr 0; elabMatchDefault stx expectedType? else let discr := Lean.Syntax.getArg discr_9 0; elabMatchDefault stx expectedType? else let discr := Lean.Syntax.getArg discr 5; elabMatchDefault stx expectedType? else let discr_8 := Lean.Syntax.getArg discr 3; let discr_9 := Lean.Syntax.getArg discr 4; let discr := Lean.Syntax.getArg discr 5; elabMatchDefault stx expectedType? else let discr_6 := Lean.Syntax.getArg discr_4 0; let discr_7 := Lean.Syntax.getArg discr_4 1; let discr_8 := Lean.Syntax.getArg discr 3; let discr_9 := Lean.Syntax.getArg discr 4; let discr := Lean.Syntax.getArg discr 5; elabMatchDefault stx expectedType? else let discr_5 := Lean.Syntax.getArg discr_3 0; let discr_6 := Lean.Syntax.getArg discr 3; let discr_7 := Lean.Syntax.getArg discr 4; let discr := Lean.Syntax.getArg discr 5; elabMatchDefault stx expectedType? else let discr_4 := Lean.Syntax.getArg discr 2; let discr_5 := Lean.Syntax.getArg discr 3; let discr_6 := Lean.Syntax.getArg discr 4; let discr := Lean.Syntax.getArg discr 5; elabMatchDefault stx expectedType? else let discr_3 := Lean.Syntax.getArg discr 1; let discr_4 := Lean.Syntax.getArg discr 2; let discr_5 := Lean.Syntax.getArg discr 3; let discr_6 := Lean.Syntax.getArg discr 4; let discr := Lean.Syntax.getArg discr 5; elabMatchDefault stx expectedType? else let discr := stx; elabMatchDefault stx expectedType?) Lean.Elab.Term.elabMatch.elabMatchDefault

source

def Lean.Elab.Term.elabMatch.elabMatchDefault (stx : Lean.Syntax) (expectedType? : Option Lean.Expr) :

Lean.Elab.TermElabM Lean.Expr

Equations

Lean.Elab.Term.elabMatch.elabMatchDefault stx expectedType? = do let a ← Lean.Elab.Term.expandNonAtomicDiscrs? stx match a with | some stxNew => Lean.Elab.Term.withMacroExpansion stx stxNew (Lean.Elab.Term.elabTerm stxNew expectedType? true true) | none => let discrs := Lean.Elab.Term.getDiscrs stx; let matchOptType := Lean.Elab.Term.getMatchOptType stx; let _do_jp := fun y => Lean.Elab.Term.elabMatchCore stx expectedType?; if (!Lean.Syntax.isNone matchOptType && Array.any discrs (fun d => !Lean.Syntax.isNone (Lean.Syntax.getOp d 0)) 0 (Array.size discrs)) = true then do let y ← Lean.throwErrorAt matchOptType (Lean.toMessageData "match expected type should not be provided when discriminants with equality proofs are used") _do_jp y else do let y ← pure PUnit.unit _do_jp y

source

def Lean.Elab.Term.elabNoMatch :

Lean.Elab.Term.TermElab

Equations

Lean.Elab.Term.elabNoMatch stx expectedType? = let discr := stx; if Lean.Syntax.isOfKind discr `Lean.Parser.Term.nomatch = true then let discr_1 := Lean.Syntax.getArg discr 0; let discr := Lean.Syntax.getArg discr 1; let discrExpr := discr; do let a ← Lean.Elab.Term.isLocalIdent? discrExpr match a with | some x => do let expectedType ← Lean.Elab.Term.waitExpectedType expectedType? let discr : Lean.Syntax := Lean.mkNode `Lean.Parser.Term.matchDiscr #[Lean.mkNullNode, discrExpr] Lean.Elab.Term.elabMatchAux none #[discr] #[] Lean.mkNullNode expectedType | x => do let stxNew ← do let info ← Lean.MonadRef.mkInfoFromRefPos let scp ← Lean.getCurrMacroScope let mainModule ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.let #[Lean.Syntax.atom info "let", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.letDecl #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.letIdDecl #[Lean.Syntax.ident info (String.toSubstring "_discr") (Lean.addMacroScope mainModule `_discr scp) [], Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.atom info ":=", discrExpr]], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.atom info ";"], Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.nomatch #[Lean.Syntax.atom info "nomatch", Lean.Syntax.ident info (String.toSubstring "_discr") (Lean.addMacroScope mainModule `_discr scp) []]]) Lean.Elab.Term.withMacroExpansion stx stxNew (Lean.Elab.Term.elabTerm stxNew expectedType? true true) else let discr := stx; Lean.Elab.throwUnsupportedSyntax