Lean.Meta.Match.Match

Lean.Meta.Match.processInaccessibleAsCtor alt ctorName = do let env ← Lean.getEnv match alt.patterns with | p@h:(Lean.Meta.Match.Pattern.inaccessible e) :: ps => let cls := `Meta.Match.match; do let a ← Lean.isTracingEnabledFor cls let _do_jp : Unit → Lean.MetaM (Option Lean.Meta.Match.Alt) := fun y => Lean.Meta.withExistingLocalDecls alt.fvarDecls do let e ← Lean.Meta.whnfD e match Lean.Expr.constructorApp? env e with | some (ctorVal, ctorArgs) => if (ctorVal.toConstantVal.name == ctorName) = true then let fields := Array.extract ctorArgs ctorVal.numParams (Array.size ctorArgs); let fields := List.map Lean.Meta.Match.Pattern.inaccessible (Array.toList fields); pure (some { ref := alt.ref, idx := alt.idx, rhs := alt.rhs, fvarDecls := alt.fvarDecls, patterns := fields ++ ps }) else pure none | x => Lean.throwErrorAt alt.ref (Lean.toMessageData "dependent match elimination failed, inaccessible pattern found" ++ Lean.toMessageData (Lean.indentD (Lean.Meta.Match.Pattern.toMessageData p)) ++ Lean.toMessageData "\nconstructor expected") if a = true then do let y ← Lean.addTrace cls (Lean.toMessageData "inaccessible in ctor step " ++ Lean.toMessageData e ++ Lean.toMessageData "") _do_jp y else do let y ← pure PUnit.unit _do_jp y | x => panicWithPosWithDecl "Lean.Meta.Match.Match" "Lean.Meta.Match.processInaccessibleAsCtor" 341 9 "unreachable code has been reached"

source

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

Lean.MetaM Bool

Equations

Lean.Meta.Match.isCurrVarInductive p = match p.vars with | [] => pure false | x :: x_1 => Lean.Meta.Match.withGoalOf p do let val? ← Lean.Meta.Match.getInductiveVal? x pure (Option.isSome val?)

source

constant Lean.Meta.Match.bootstrap.genMatcherCode :

Lean.Option Bool

source

constant Lean.Meta.Match.matcherExt :

Lean.EnvExtension (Std.PHashMap (Lean.Expr × Bool) Lean.Name)

source

def Lean.Meta.Match.mkMatcherAuxDefinition (name : Lean.Name) (type : Lean.Expr) (value : Lean.Expr) :

Lean.MetaM (Lean.Expr × Option (Lean.Meta.MatcherInfo → Lean.MetaM Unit))

Equations

Lean.Meta.Match.mkMatcherAuxDefinition name type value = let cls := `Meta.debug; do let a ← Lean.isTracingEnabledFor cls let _do_jp : Unit → Lean.MetaM (Lean.Expr × Option (Lean.Meta.MatcherInfo → Lean.MetaM Unit)) := fun y => do let a ← Lean.getOptions let compile : Bool := Lean.Option.get a Lean.Meta.Match.bootstrap.genMatcherCode let result ← Lean.Meta.Closure.mkValueTypeClosure type value false let env ← Lean.getEnv let mkMatcherConst : Lean.Name → Lean.Expr := fun name => Lean.mkAppN (Lean.mkConst name (Array.toList result.levelArgs)) result.exprArgs match Std.PersistentHashMap.find? (Lean.EnvExtension.getState Lean.Meta.Match.matcherExt env) (result.value, compile) with | some nameNew => pure (mkMatcherConst nameNew, none) | none => let decl := Lean.Declaration.defnDecl { toConstantVal := { name := name, levelParams := Array.toList result.levelParams, type := result.type }, value := result.value, hints := Lean.ReducibilityHints.abbrev, safety := if (Lean.Environment.hasUnsafe env result.type || Lean.Environment.hasUnsafe env result.value) = true then Lean.DefinitionSafety.unsafe else Lean.DefinitionSafety.safe }; let cls := `Meta.debug; do let a ← Lean.isTracingEnabledFor cls let _do_jp : Unit → Lean.MetaM (Lean.Expr × Option (Lean.Meta.MatcherInfo → Lean.MetaM Unit)) := fun y => let addMatcher := fun mi => do Lean.addDecl decl Lean.modifyEnv fun env => Lean.EnvExtension.modifyState Lean.Meta.Match.matcherExt env fun s => Std.PersistentHashMap.insert s (result.value, compile) name Lean.Meta.Match.addMatcherInfo name mi Lean.Meta.setInlineAttribute name Lean.Compiler.InlineAttributeKind.inline if compile = true then Lean.compileDecl decl else pure PUnit.unit; pure (mkMatcherConst name, some addMatcher) if a = true then do let y ← Lean.addTrace cls (Lean.toMessageData "" ++ Lean.toMessageData name ++ Lean.toMessageData " : " ++ Lean.toMessageData result.type ++ Lean.toMessageData " := " ++ Lean.toMessageData result.value ++ Lean.toMessageData "") _do_jp y else do let y ← pure PUnit.unit _do_jp y if a = true then do let y ← Lean.addTrace cls (Lean.toMessageData "" ++ Lean.toMessageData name ++ Lean.toMessageData " : " ++ Lean.toMessageData type ++ Lean.toMessageData " := " ++ Lean.toMessageData value ++ Lean.toMessageData "") _do_jp y else do let y ← pure PUnit.unit _do_jp y

source

structure Lean.Meta.Match.MkMatcherInput :

Type

matcherName : Lean.Name
matchType : Lean.Expr
numDiscrs : Nat
lhss : List Lean.Meta.Match.AltLHS

source

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

Lean.MetaM Lean.Meta.Match.MatcherResult

Equations

Lean.Meta.Match.mkMatcher input = let x := input; match x with | { matcherName := matcherName, matchType := matchType, numDiscrs := numDiscrs, lhss := lhss } => Lean.Meta.forallBoundedTelescope matchType (some numDiscrs) fun majors matchTypeBody => do Lean.Meta.Match.checkNumPatterns majors lhss let uElim ← Lean.Meta.getLevel matchTypeBody let _do_jp : Lean.Level → Lean.MetaM Lean.Meta.Match.MatcherResult := fun uElimGen => do let motiveType ← Lean.Meta.mkForallFVars majors (Lean.mkSort uElimGen) false true Lean.Meta.withLocalDeclD `motive motiveType fun motive => let cls := `Meta.Match.debug; do let a ← Lean.isTracingEnabledFor cls let _do_jp : Unit → Lean.MetaM Lean.Meta.Match.MatcherResult := fun y => let mvarType := Lean.mkAppN motive majors; let cls := `Meta.Match.debug; do let a ← Lean.isTracingEnabledFor cls let _do_jp : Unit → Lean.MetaM Lean.Meta.Match.MatcherResult := fun y => Lean.Meta.Match.withAlts motive lhss fun alts minors => do let mvar ← Lean.Meta.mkFreshExprMVar (some mvarType) Lean.MetavarKind.natural Lean.Name.anonymous let examples : List Lean.Meta.Match.Example := List.map (fun major => Lean.Meta.Match.Example.var (Lean.Expr.fvarId! major)) (Array.toList majors) let discr ← StateRefT'.run (Lean.Meta.Match.process { mvarId := Lean.Expr.mvarId! mvar, vars := Array.toList majors, alts := alts, examples := examples }) { used := ∅, counterExamples := [] } let x : Unit × Lean.Meta.Match.State := discr match x with | (x, s) => let args := #[motive] ++ majors ++ Array.map Prod.fst minors; do let type ← Lean.Meta.mkForallFVars args mvarType false true let val ← Lean.Meta.mkLambdaFVars args mvar false true let cls : Lean.Name := `Meta.Match.debug let a ← Lean.isTracingEnabledFor cls let _do_jp : Unit → Lean.MetaM Lean.Meta.Match.MatcherResult := fun y => do let discr ← Lean.Meta.Match.mkMatcherAuxDefinition matcherName type val let x : Lean.Expr × Option (Lean.Meta.MatcherInfo → Lean.MetaM Unit) := discr match x with | (matcher, addMatcher) => let cls := `Meta.Match.debug; do let a ← Lean.isTracingEnabledFor cls let _do_jp : Unit → Lean.MetaM Lean.Meta.Match.MatcherResult := fun y => do let uElimPos? ← Lean.Meta.Match.getUElimPos? (Lean.Expr.constLevels! (Lean.Expr.getAppFn matcher)) uElimGen discard (Lean.Meta.isLevelDefEq uElimGen uElim) let addMatcher : Lean.MetaM Unit := match addMatcher with | some addMatcher => addMatcher { numParams := Lean.Expr.getAppNumArgs matcher, numDiscrs := numDiscrs, altNumParams := Array.map Prod.snd minors, uElimPos? := uElimPos? } | none => pure () let cls : Lean.Name := `Meta.Match.debug let a ← Lean.isTracingEnabledFor cls let _do_jp : Unit → Lean.MetaM Lean.Meta.Match.MatcherResult := fun y => let unusedAltIdxs := Nat.fold (fun i r => if Std.HashSet.contains s.used i = true then r else i :: r) (List.length lhss) []; pure { matcher := matcher, counterExamples := s.counterExamples, unusedAltIdxs := List.reverse unusedAltIdxs, addMatcher := addMatcher } if a = true then do let y ← Lean.addTrace cls (Lean.toMessageData "matcher: " ++ Lean.toMessageData matcher ++ Lean.toMessageData "") _do_jp y else do let y ← pure PUnit.unit _do_jp y if a = true then do let y ← Lean.addTrace cls (Lean.toMessageData "matcher levels: " ++ Lean.toMessageData (Lean.Expr.constLevels! (Lean.Expr.getAppFn matcher)) ++ Lean.toMessageData ", uElim: " ++ Lean.toMessageData uElimGen ++ Lean.toMessageData "") _do_jp y else do let y ← pure PUnit.unit _do_jp y if a = true then do let y ← Lean.addTrace cls (Lean.toMessageData "matcher value: " ++ Lean.toMessageData val ++ Lean.toMessageData "\ntype: " ++ Lean.toMessageData type ++ Lean.toMessageData "") _do_jp y else do let y ← pure PUnit.unit _do_jp y if a = true then do let y ← Lean.addTrace cls (Lean.toMessageData "target: " ++ Lean.toMessageData mvarType ++ Lean.toMessageData "") _do_jp y else do let y ← pure PUnit.unit _do_jp y if a = true then do let y ← Lean.addTrace cls (Lean.toMessageData "motiveType: " ++ Lean.toMessageData motiveType ++ Lean.toMessageData "") _do_jp y else do let y ← pure PUnit.unit _do_jp y if (uElim == Lean.levelZero) = true then do let y ← pure Lean.levelZero _do_jp y else do let y ← Lean.Meta.mkFreshLevelMVar _do_jp y

source

def Lean.Meta.Match.getMkMatcherInputInContext (matcherApp : Lean.Meta.MatcherApp) :

Lean.MetaM Lean.Meta.Match.MkMatcherInput

Equations

Lean.Meta.Match.getMkMatcherInputInContext matcherApp = let matcherName := matcherApp.matcherName; do let discr ← Lean.Meta.getMatcherInfo? matcherName match discr with | some matcherInfo => do let matcherConst ← Lean.getConstInfo matcherName let matcherType ← Lean.Meta.instantiateForall (Lean.ConstantInfo.type matcherConst) (matcherApp.params ++ #[matcherApp.motive]) let _do_jp : Lean.Expr → Lean.MetaM Lean.Meta.Match.MkMatcherInput := fun matchType => do let matcherType ← Lean.Meta.instantiateForall matcherType matcherApp.discrs let a ← Lean.Meta.forallBoundedTelescope matcherType (some (Array.size matcherApp.alts)) fun alts x => Array.mapM (fun alt => do let ty ← Lean.Meta.inferType alt Lean.Meta.forallTelescope ty fun xs body => do let xs ← Array.filterM (fun x => Lean.Meta.dependsOn body (Lean.Expr.fvarId! x)) xs 0 (Array.size xs) Lean.Expr.withApp body fun f args => do let ctx ← Lean.getLCtx let localDecls : Array Lean.LocalDecl := Array.map (Lean.LocalContext.getFVar! ctx) xs let patterns ← Array.mapM Lean.Meta.Match.toPattern args pure { ref := Lean.Syntax.missing, fvarDecls := Array.toList localDecls, patterns := Array.toList patterns }) alts let lhss : List Lean.Meta.Match.AltLHS := Array.toList a pure { matcherName := matcherName, matchType := matchType, numDiscrs := Array.size matcherApp.discrs, lhss := lhss } let u : Lean.Level := match matcherInfo.uElimPos? with | some idx => Lean.mkLevelParam (Array.getOp (List.toArray (Lean.ConstantInfo.levelParams matcherConst)) idx) | x => Lean.levelZero let y ← Lean.Meta.forallBoundedTelescope matcherType (some matcherInfo.numDiscrs) fun discrs t => Lean.Meta.mkForallFVars discrs (Lean.mkConst `PUnit [u]) false true _do_jp y | x => Lean.throwError (Lean.toMessageData "not a matcher: " ++ Lean.toMessageData matcherName ++ Lean.toMessageData "")

source

def Lean.Meta.Match.withMkMatcherInput {α : Type} (matcherName : Lean.Name) (k : Lean.Meta.Match.MkMatcherInput → Lean.MetaM α) :

Lean.MetaM α

Equations

Lean.Meta.Match.withMkMatcherInput matcherName k = do let discr ← Lean.Meta.getMatcherInfo? matcherName match discr with | some matcherInfo => do let matcherConst ← Lean.getConstInfo matcherName Lean.Meta.forallBoundedTelescope (Lean.ConstantInfo.type matcherConst) (some (Lean.Meta.Match.MatcherInfo.arity matcherInfo)) fun xs t => do let matcherApp ← Lean.mkConstWithLevelParams (Lean.ConstantInfo.name matcherConst) let matcherApp : Lean.Expr := Lean.mkAppN matcherApp xs let discr ← Lean.Meta.matchMatcherApp? matcherApp match discr with | some matcherApp => do let mkMatcherInput ← Lean.Meta.Match.getMkMatcherInputInContext matcherApp k mkMatcherInput | x => Lean.throwError (Lean.toMessageData "not a matcher app: " ++ Lean.toMessageData matcherApp ++ Lean.toMessageData "") | x => Lean.throwError (Lean.toMessageData "not a matcher: " ++ Lean.toMessageData matcherName ++ Lean.toMessageData "")

source

def Lean.Meta.MatcherApp.addArg (matcherApp : Lean.Meta.MatcherApp) (e : Lean.Expr) :

Lean.MetaM Lean.Meta.MatcherApp

Equations

Lean.Meta.MatcherApp.addArg matcherApp e = Lean.Meta.lambdaTelescope matcherApp.motive fun motiveArgs motiveBody => let _do_jp := fun y => do let eType ← Lean.Meta.inferType e let eTypeAbst ← Nat.foldRevM (fun i eTypeAbst => let motiveArg := Array.getOp motiveArgs i; let discr := Array.getOp matcherApp.discrs i; do let eTypeAbst ← Lean.Meta.kabstract eTypeAbst discr Lean.Occurrences.all pure (Lean.Expr.instantiate1 eTypeAbst motiveArg)) eType (Array.size matcherApp.discrs) let motiveBody ← Lean.Meta.mkArrow eTypeAbst motiveBody let _do_jp : Array Lean.Level → Lean.MetaM Lean.Meta.MatcherApp := fun matcherLevels => do let motive ← Lean.Meta.mkLambdaFVars motiveArgs motiveBody false true let aux : Lean.Expr := Lean.mkAppN (Lean.mkConst matcherApp.matcherName (Array.toList matcherLevels)) matcherApp.params let aux : Lean.Expr := Lean.mkApp aux motive let aux : Lean.Expr := Lean.mkAppN aux matcherApp.discrs Lean.Meta.check aux let a ← Lean.Meta.isTypeCorrect aux let _do_jp : PUnit → Lean.MetaM Lean.Meta.MatcherApp := fun y => do let auxType ← Lean.Meta.inferType aux let discr ← Lean.Meta.updateAlts auxType matcherApp.altNumParams matcherApp.alts 0 let x : Array Nat × Array Lean.Expr := discr match x with | (altNumParams, alts) => pure { matcherName := matcherApp.matcherName, matcherLevels := matcherLevels, uElimPos? := matcherApp.uElimPos?, params := matcherApp.params, motive := motive, discrs := matcherApp.discrs, altNumParams := altNumParams, alts := alts, remaining := #[e] ++ matcherApp.remaining } if a = true then do let y ← pure PUnit.unit _do_jp y else do let y ← Lean.throwError (Lean.toMessageData "failed to add argument to matcher application, type error when constructing the new motive") _do_jp y match matcherApp.uElimPos? with | none => do let y ← pure matcherApp.matcherLevels _do_jp y | some pos => do let uElim ← Lean.Meta.getLevel motiveBody let y ← pure (Array.set! matcherApp.matcherLevels pos uElim) _do_jp y; if (Array.size motiveArgs == Array.size matcherApp.discrs) = true then do let y ← pure PUnit.unit _do_jp y else do let y ← Lean.throwError (Lean.toMessageData "unexpected matcher application, motive must be lambda expression with #" ++ Lean.toMessageData (Array.size matcherApp.discrs) ++ Lean.toMessageData " arguments") _do_jp y