- ref : Lean.Syntax
- modifiers : Lean.Elab.Modifiers
- kind : Lean.Elab.DefKind
- shortDeclName : Lean.Name
- declName : Lean.Name
- levelNames : List Lean.Name
- binderIds : Array Lean.Syntax
- numParams : Nat
- type : Lean.Expr
- valueStx : Lean.Syntax
Equations
- Lean.Elab.instInhabitedDefViewElabHeader = { default := { ref := default, modifiers := default, kind := default, shortDeclName := default, declName := default, levelNames := default, binderIds := default, numParams := default, type := default, valueStx := default } }
@[inline]
- usedFVarsMap : Lean.Elab.Term.MutualClosure.UsedFVarsMap
- modified : Bool
@[inline]
def
Lean.Elab.Term.MutualClosure.FixPoint.run
(letRecFVarIds : List Lean.FVarId)
(usedFVarsMap : Lean.Elab.Term.MutualClosure.UsedFVarsMap)
:
Equations
- Lean.Elab.Term.MutualClosure.FixPoint.run letRecFVarIds usedFVarsMap = let x := StateT.run (ReaderT.run (Lean.Elab.Term.MutualClosure.FixPoint.fixpoint ()) letRecFVarIds) { usedFVarsMap := usedFVarsMap, modified := false }; match x with | (x, s) => s.usedFVarsMap
@[inline]
- newLocalDecls : Array Lean.LocalDecl
- localDecls : Array Lean.LocalDecl
- newLetDecls : Array Lean.LocalDecl
- exprArgs : Array Lean.Expr
- ref : Lean.Syntax
- localDecls : Array Lean.LocalDecl
- closed : Lean.Expr
- toLift : Lean.Elab.Term.LetRecToLift
@[inline]
def
Lean.Elab.Term.MutualClosure.insertReplacementForMainFns
(r : Lean.Elab.Term.MutualClosure.Replacement)
(sectionVars : Array Lean.Expr)
(mainHeaders : Array Lean.Elab.DefViewElabHeader)
(mainFVars : Array Lean.Expr)
:
Equations
- Lean.Elab.Term.MutualClosure.insertReplacementForMainFns r sectionVars mainHeaders mainFVars = Nat.fold (fun i r => Std.RBMap.insert r (Lean.Expr.fvarId! (Array.getOp mainFVars i)) (Lean.mkAppN (Lean.mkConst (Array.getOp mainHeaders i).declName) sectionVars)) (Array.size mainFVars) r
def
Lean.Elab.Term.MutualClosure.insertReplacementForLetRecs
(r : Lean.Elab.Term.MutualClosure.Replacement)
(letRecClosures : List Lean.Elab.Term.MutualClosure.LetRecClosure)
:
Equations
- Lean.Elab.Term.MutualClosure.insertReplacementForLetRecs r letRecClosures = List.foldl (fun r c => Std.RBMap.insert r c.toLift.fvarId c.closed) r letRecClosures
def
Lean.Elab.Term.MutualClosure.Replacement.apply
(r : Lean.Elab.Term.MutualClosure.Replacement)
(e : Lean.Expr)
:
Equations
- Lean.Elab.Term.MutualClosure.Replacement.apply r e = Lean.Expr.replace (fun e => match e with | Lean.Expr.fvar fvarId x => match Std.RBMap.find? r fvarId with | some c => some c | x => none | x => none) e
def
Lean.Elab.Term.MutualClosure.pushMain
(preDefs : Array Lean.Elab.PreDefinition)
(sectionVars : Array Lean.Expr)
(mainHeaders : Array Lean.Elab.DefViewElabHeader)
(mainVals : Array Lean.Expr)
:
Equations
- Lean.Elab.Term.MutualClosure.pushMain preDefs sectionVars mainHeaders mainVals = Nat.foldM (fun i preDefs => let header := Array.getOp mainHeaders i; do let val ← liftM (Lean.Meta.mkLambdaFVars sectionVars (Array.getOp mainVals i) false true) let type ← liftM (Lean.Meta.mkForallFVars sectionVars header.type false true) pure (Array.push preDefs { ref := Lean.Elab.getDeclarationSelectionRef header.ref, kind := header.kind, levelParams := [], modifiers := header.modifiers, declName := header.declName, type := type, value := val })) preDefs (Array.size mainHeaders)
def
Lean.Elab.Term.MutualClosure.pushLetRecs
(preDefs : Array Lean.Elab.PreDefinition)
(letRecClosures : List Lean.Elab.Term.MutualClosure.LetRecClosure)
(kind : Lean.Elab.DefKind)
(modifiers : Lean.Elab.Modifiers)
:
Equations
- Lean.Elab.Term.MutualClosure.pushLetRecs preDefs letRecClosures kind modifiers = List.foldl (fun preDefs c => let type := Lean.Meta.Closure.mkForall c.localDecls c.toLift.type; let val := Lean.Meta.Closure.mkLambda c.localDecls c.toLift.val; Array.push preDefs { ref := c.ref, kind := kind, levelParams := [], modifiers := { docString? := modifiers.docString?, visibility := modifiers.visibility, isNoncomputable := modifiers.isNoncomputable, recKind := modifiers.recKind, isUnsafe := modifiers.isUnsafe, attrs := c.toLift.attrs }, declName := c.toLift.declName, type := type, value := val }) preDefs letRecClosures
def
Lean.Elab.Term.MutualClosure.getKindForLetRecs
(mainHeaders : Array Lean.Elab.DefViewElabHeader)
:
Equations
- Lean.Elab.Term.MutualClosure.getKindForLetRecs mainHeaders = if Array.any mainHeaders (fun h => Lean.Elab.DefKind.isTheorem h.kind) 0 (Array.size mainHeaders) = true then Lean.Elab.DefKind.theorem else Lean.Elab.DefKind.def
def
Lean.Elab.Term.MutualClosure.getModifiersForLetRecs
(mainHeaders : Array Lean.Elab.DefViewElabHeader)
:
Equations
- Lean.Elab.Term.MutualClosure.getModifiersForLetRecs mainHeaders = { docString? := none, visibility := Lean.Elab.Visibility.regular, isNoncomputable := Array.any mainHeaders (fun h => h.modifiers.isNoncomputable) 0 (Array.size mainHeaders), recKind := if Array.any mainHeaders (fun h => Lean.Elab.Modifiers.isPartial h.modifiers) 0 (Array.size mainHeaders) = true then Lean.Elab.RecKind.partial else Lean.Elab.RecKind.default, isUnsafe := Array.any mainHeaders (fun h => h.modifiers.isUnsafe) 0 (Array.size mainHeaders), attrs := #[] }
def
Lean.Elab.Term.MutualClosure.main
(sectionVars : Array Lean.Expr)
(mainHeaders : Array Lean.Elab.DefViewElabHeader)
(mainFVars : Array Lean.Expr)
(mainVals : Array Lean.Expr)
(letRecsToLift : List Lean.Elab.Term.LetRecToLift)
:
Equations
- Lean.Elab.Term.MutualClosure.main sectionVars mainHeaders mainFVars mainVals letRecsToLift = let mainFVarIds := Array.map Lean.Expr.fvarId! mainFVars; let recFVarIds := Array.map (fun toLift => toLift.fvarId) (List.toArray letRecsToLift) ++ mainFVarIds; do let mctx ← Lean.getMCtx let freeVarMap : Lean.Elab.Term.MutualClosure.FreeVarMap := Lean.Elab.Term.MutualClosure.mkFreeVarMap mctx sectionVars mainFVarIds recFVarIds letRecsToLift liftM Lean.Meta.resetZetaFVarIds Lean.Meta.withTrackingZeta do List.forM letRecsToLift fun toLift => Lean.Meta.withLCtx toLift.lctx toLift.localInstances do liftM (Lean.Meta.check toLift.type) liftM (Lean.Meta.check toLift.val) let letRecClosures ← Lean.Elab.Term.MutualClosure.mkLetRecClosures letRecsToLift freeVarMap let mainVals ← Array.mapM (fun a => liftM (Lean.Meta.instantiateMVars a)) mainVals let mainHeaders ← Array.mapM Lean.Elab.Term.instantiateMVarsAtHeader mainHeaders let letRecClosures ← List.mapM (fun closure => do let a ← Lean.Elab.Term.instantiateMVarsAtLetRecToLift closure.toLift pure { ref := closure.ref, localDecls := closure.localDecls, closed := closure.closed, toLift := a }) letRecClosures let r : Lean.Elab.Term.MutualClosure.Replacement := Lean.Elab.Term.MutualClosure.insertReplacementForMainFns ∅ sectionVars mainHeaders mainFVars let r : Lean.Elab.Term.MutualClosure.Replacement := Lean.Elab.Term.MutualClosure.insertReplacementForLetRecs r letRecClosures let mainVals : Array Lean.Expr := Array.map (Lean.Elab.Term.MutualClosure.Replacement.apply r) mainVals let mainHeaders : Array Lean.Elab.DefViewElabHeader := Array.map (fun h => { ref := h.ref, modifiers := h.modifiers, kind := h.kind, shortDeclName := h.shortDeclName, declName := h.declName, levelNames := h.levelNames, binderIds := h.binderIds, numParams := h.numParams, type := Lean.Elab.Term.MutualClosure.Replacement.apply r h.type, valueStx := h.valueStx }) mainHeaders let letRecClosures : List Lean.Elab.Term.MutualClosure.LetRecClosure := List.map (fun c => { ref := c.ref, localDecls := c.localDecls, closed := c.closed, toLift := let src := c.toLift; { ref := src.ref, fvarId := src.fvarId, attrs := src.attrs, shortDeclName := src.shortDeclName, declName := src.declName, lctx := src.lctx, localInstances := src.localInstances, type := Lean.Elab.Term.MutualClosure.Replacement.apply r c.toLift.type, val := Lean.Elab.Term.MutualClosure.Replacement.apply r c.toLift.val, mvarId := src.mvarId } }) letRecClosures let letRecKind : Lean.Elab.DefKind := Lean.Elab.Term.MutualClosure.getKindForLetRecs mainHeaders let letRecMods : Lean.Elab.Modifiers := Lean.Elab.Term.MutualClosure.getModifiersForLetRecs mainHeaders Lean.Elab.Term.MutualClosure.pushMain (Lean.Elab.Term.MutualClosure.pushLetRecs #[] letRecClosures letRecKind letRecMods) sectionVars mainHeaders mainVals
Equations
- Lean.Elab.Term.processDefDeriving className declName = do let r ← tryCatch (do let discr ← Lean.getConstInfo declName match discr with | Lean.ConstantInfo.defnInfo info => do let discr ← liftM (Lean.Elab.Term.mkInst? className info.value) match discr with | some result => let instTypeNew := Lean.mkApp (Lean.Expr.appFn! result.instType) (Lean.mkConst declName (List.map Lean.mkLevelParam info.toConstantVal.levelParams)); do liftM (Lean.Meta.check instTypeNew) let instName ← Lean.Elab.liftMacroM (Lean.Elab.mkUnusedBaseName (Lean.Name.appendAfter (Lean.Name.appendBefore declName "inst") (Lean.Name.getString! className))) let a ← liftM (Lean.Meta.instantiateMVars instTypeNew) let a_1 ← liftM (Lean.Meta.instantiateMVars result.instVal) Lean.addAndCompile (Lean.Declaration.defnDecl { toConstantVal := { name := instName, levelParams := info.toConstantVal.levelParams, type := a }, value := a_1, hints := info.hints, safety := info.safety }) liftM (Lean.Meta.addInstance instName Lean.AttributeKind.global 1000) pure true | x => pure false | x => pure false) fun ex => pure false pure r
Equations
- Lean.Elab.Term.eraseAuxDiscr e = Lean.Core.transform e (fun e => match e with | Lean.Expr.letE n x v b x_1 => if Lean.Elab.Term.isAuxDiscrName n = true then pure (Lean.TransformStep.visit (Lean.Expr.instantiate1 b v)) else pure (Lean.TransformStep.visit e) | e => pure (Lean.TransformStep.visit e)) fun e => pure (Lean.TransformStep.done e)
def
Lean.Elab.Term.elabMutualDef
(vars : Array Lean.Expr)
(views : Array Lean.Elab.DefView)
(hints : Lean.Elab.TerminationHints)
:
Equations
- Lean.Elab.Term.elabMutualDef vars views hints = (fun go processDeriving => if Lean.Elab.Term.isExample views = true then Lean.withoutModifyingEnv go else go) (Lean.Elab.Term.elabMutualDef.go vars views hints) (Lean.Elab.Term.elabMutualDef.processDeriving views)
def
Lean.Elab.Term.elabMutualDef.go
(vars : Array Lean.Expr)
(views : Array Lean.Elab.DefView)
(hints : Lean.Elab.TerminationHints)
:
Equations
- Lean.Elab.Term.elabMutualDef.go vars views hints = do let scopeLevelNames ← Lean.Elab.Term.getLevelNames let headers ← Lean.Elab.Term.elabHeaders views let headers ← Lean.Elab.Term.levelMVarToParamHeaders views headers let allUserLevelNames : List Lean.Name := Lean.Elab.Term.getAllUserLevelNames headers Lean.Elab.Term.withFunLocalDecls headers fun funFVars => do let values ← Lean.Elab.Term.elabFunValues headers Lean.Elab.Term.synthesizeSyntheticMVarsNoPostponing false let values ← Array.mapM (fun a => liftM (Lean.Meta.instantiateMVars a)) values let headers ← Array.mapM Lean.Elab.Term.instantiateMVarsAtHeader headers let letRecsToLift ← Lean.Elab.Term.getLetRecsToLift let letRecsToLift ← List.mapM Lean.Elab.Term.instantiateMVarsAtLetRecToLift letRecsToLift Lean.Elab.Term.checkLetRecsToLiftTypes funFVars letRecsToLift Lean.Elab.Term.withUsed vars headers values letRecsToLift fun vars => do let preDefs ← Lean.Elab.Term.MutualClosure.main vars headers funFVars values letRecsToLift let r ← forIn preDefs PUnit.unit fun preDef r => let cls := `Elab.definition; do let a ← Lean.isTracingEnabledFor cls if a = true then do Lean.addTrace cls (Lean.toMessageData "" ++ Lean.toMessageData preDef.declName ++ Lean.toMessageData " : " ++ Lean.toMessageData preDef.type ++ Lean.toMessageData " :=\n" ++ Lean.toMessageData preDef.value ++ Lean.toMessageData "") pure (ForInStep.yield PUnit.unit) else do pure PUnit.unit pure (ForInStep.yield PUnit.unit) let x : PUnit := r let preDefs ← Lean.Elab.levelMVarToParamPreDecls preDefs let preDefs ← Lean.Elab.instantiateMVarsAtPreDecls preDefs let preDefs ← Lean.Elab.fixLevelParams preDefs scopeLevelNames allUserLevelNames let preDefs ← Array.mapM (fun preDef => if (Lean.Elab.DefKind.isTheorem preDef.kind || Lean.Elab.DefKind.isExample preDef.kind) = true then pure preDef else do let a ← liftM (Lean.Elab.Term.eraseAuxDiscr preDef.value) pure { ref := preDef.ref, kind := preDef.kind, levelParams := preDef.levelParams, modifiers := preDef.modifiers, declName := preDef.declName, type := preDef.type, value := a }) preDefs Lean.Elab.addPreDefinitions preDefs hints Lean.Elab.Term.elabMutualDef.processDeriving views headers
def
Lean.Elab.Term.elabMutualDef.processDeriving
(views : Array Lean.Elab.DefView)
(headers : Array Lean.Elab.DefViewElabHeader)
:
Equations
- Lean.Elab.Term.elabMutualDef.processDeriving views headers = let s := toStream views; do let r ← forIn headers s fun header r => let s := r; match Stream.next? s with | none => pure (ForInStep.done s) | some (view, s') => let s := s'; match view.deriving? with | some classNamesStx => do let r ← forIn classNamesStx PUnit.unit fun classNameStx r => do let className ← Lean.resolveGlobalConstNoOverload classNameStx Lean.withRef classNameStx do let a ← Lean.Elab.Term.processDefDeriving className header.declName if a = true then pure PUnit.unit else Lean.throwError (Lean.toMessageData "failed to synthesize instance '" ++ Lean.toMessageData className ++ Lean.toMessageData "' for '" ++ Lean.toMessageData header.declName ++ Lean.toMessageData "'") pure (ForInStep.yield PUnit.unit) let x : PUnit := r pure PUnit.unit pure (ForInStep.yield s) | x => do pure PUnit.unit pure (ForInStep.yield s) let x : Subarray Lean.Elab.DefView := r let s : Subarray Lean.Elab.DefView := x pure PUnit.unit
Equations
- Lean.Elab.Command.elabMutualDef ds hints = do let views ← Array.mapM (fun d => do let modifiers ← Lean.Elab.elabModifiers (Lean.Syntax.getOp d 0) let _do_jp : PUnit → Lean.Elab.Command.CommandElabM Lean.Elab.DefView := fun y => Lean.Elab.Command.mkDefView modifiers (Lean.Syntax.getOp d 1) if (decide (Array.size ds > 1) && Lean.Elab.Modifiers.isNonrec modifiers) = true then do let y ← Lean.throwErrorAt d (Lean.toMessageData "invalid use of 'nonrec' modifier in 'mutual' block") _do_jp y else do let y ← pure PUnit.unit _do_jp y) ds Lean.Elab.Command.runTermElabM none fun vars => Lean.Elab.Term.elabMutualDef vars views hints