- terminationBy? : Option Lean.Syntax
- decreasingBy? : Option Lean.Syntax
Equations
- Lean.Elab.instInhabitedTerminationHints = { default := { terminationBy? := default, decreasingBy? := default } }
def
Lean.Elab.addPreDefinitions
(preDefs : Array Lean.Elab.PreDefinition)
(hints : Lean.Elab.TerminationHints)
:
Equations
- Lean.Elab.addPreDefinitions preDefs hints = Lean.Meta.withLCtx { fvarIdToDecl := { root := Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, decls := { root := Std.PersistentArrayNode.node (Array.mkEmpty (USize.toNat Std.PersistentArray.branching)), tail := Array.mkEmpty (USize.toNat Std.PersistentArray.branching), size := 0, shift := Std.PersistentArray.initShift, tailOff := 0 } } ∅ do let r ← forIn preDefs PUnit.unit fun preDef r => let cls := `Elab.definition.body; 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 ← Array.mapM Lean.Elab.ensureNoUnassignedMVarsAtPreDef preDefs let cliques ← pure (Lean.Elab.partitionPreDefs preDefs) let terminationBy ← Lean.Elab.liftMacroM (Lean.Elab.WF.expandTerminationBy hints.terminationBy? (Array.map (fun ds => Array.map (fun a => a.declName) ds) cliques)) let decreasingBy ← Lean.Elab.liftMacroM (Lean.Elab.WF.expandTerminationHint hints.decreasingBy? (Array.map (fun ds => Array.map (fun a => a.declName) ds) cliques)) let r ← forIn cliques { fst := terminationBy, snd := decreasingBy } fun preDefs r => let terminationBy := r.fst; let decreasingBy := r.snd; let cls := `Elab.definition.scc; do let a ← Lean.isTracingEnabledFor cls let _do_jp : Lean.Elab.WF.TerminationBy → Lean.Elab.WF.TerminationHint → Unit → Lean.Elab.TermElabM (ForInStep (MProd Lean.Elab.WF.TerminationBy Lean.Elab.WF.TerminationHint)) := fun terminationBy decreasingBy y => if (Array.size preDefs == 1 && Lean.Elab.isNonRecursive (Array.getOp preDefs 0)) = true then let preDef := Array.getOp preDefs 0; if preDef.modifiers.isNoncomputable = true then do Lean.Elab.addNonRec preDef true pure (ForInStep.yield { fst := terminationBy, snd := decreasingBy }) else do Lean.Elab.addAndCompileNonRec preDef pure (ForInStep.yield { fst := terminationBy, snd := decreasingBy }) else if Array.any preDefs (fun a => a.modifiers.isUnsafe) 0 (Array.size preDefs) = true then do Lean.Elab.addAndCompileUnsafe preDefs Lean.DefinitionSafety.unsafe pure (ForInStep.yield { fst := terminationBy, snd := decreasingBy }) else if Array.any preDefs (fun a => Lean.Elab.Modifiers.isPartial a.modifiers) 0 (Array.size preDefs) = true then do let r ← forIn preDefs PUnit.unit fun preDef r => do let a ← liftM (Lean.Meta.whnfD preDef.type) if (Lean.Elab.Modifiers.isPartial preDef.modifiers && !Lean.Expr.isForall a) = true then do Lean.withRef preDef.ref (Lean.throwError (Lean.toMessageData "invalid use of 'partial', '" ++ Lean.toMessageData preDef.declName ++ Lean.toMessageData "' is not a function" ++ Lean.toMessageData (Lean.indentExpr preDef.type) ++ Lean.toMessageData "")) pure (ForInStep.yield PUnit.unit) else do pure PUnit.unit pure (ForInStep.yield PUnit.unit) let x : PUnit := r Lean.Elab.addAndCompilePartial preDefs pure (ForInStep.yield { fst := terminationBy, snd := decreasingBy }) else let wf? := none; let decrTactic? := none; let _do_jp := fun decrTactic? wf? terminationBy decreasingBy y => let _do_jp := fun decrTactic? decreasingBy y => if (Option.isSome wf? || Option.isSome decrTactic?) = true then do Lean.Elab.wfRecursion preDefs wf? decrTactic? pure (ForInStep.yield { fst := terminationBy, snd := decreasingBy }) else do Lean.withRef (Array.getOp preDefs 0).ref (Lean.Meta.mapError (Lean.Meta.orelseMergeErrors (Lean.Elab.structuralRecursion preDefs) (Lean.Elab.wfRecursion preDefs none none) fun r₁ r₂ => r₁) fun msg => let preDefMsgs := List.map (fun a => Lean.MessageData.ofExpr (Lean.mkConst a.declName)) (Array.toList preDefs); Lean.toMessageData "fail to show termination for" ++ Lean.toMessageData (Lean.indentD (Lean.MessageData.joinSep preDefMsgs (Lean.MessageData.ofFormat Lean.Format.line))) ++ Lean.toMessageData "\nwith errors\n" ++ Lean.toMessageData msg ++ Lean.toMessageData "") pure (ForInStep.yield { fst := terminationBy, snd := decreasingBy }); match Lean.Elab.WF.TerminationHint.find? decreasingBy (Array.map (fun a => a.declName) preDefs) with | some { ref := ref, value := decrTactic } => do let a ← Lean.withRef ref do let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.byTactic #[Lean.Syntax.atom info "by", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Tactic.tacticSeq #[decrTactic]]) let decrTactic? : Option Lean.Syntax := some a let decreasingBy : Lean.Elab.WF.TerminationHint := Lean.Elab.WF.TerminationHint.markAsUsed decreasingBy (Array.map (fun a => a.declName) preDefs) let y ← pure PUnit.unit _do_jp decrTactic? decreasingBy y | x => do let y ← pure PUnit.unit _do_jp decrTactic? decreasingBy y; match Lean.Elab.WF.TerminationBy.find? terminationBy (Array.map (fun a => a.declName) preDefs) with | some wf => let wf? := some wf; let terminationBy := Lean.Elab.WF.TerminationBy.markAsUsed terminationBy (Array.map (fun a => a.declName) preDefs); do let y ← pure PUnit.unit _do_jp decrTactic? wf? terminationBy decreasingBy y | x => do let y ← pure PUnit.unit _do_jp decrTactic? wf? terminationBy decreasingBy y if a = true then do let y ← Lean.addTrace cls (Lean.toMessageData "" ++ Lean.toMessageData (Array.map (fun a => a.declName) preDefs) ++ Lean.toMessageData "") _do_jp terminationBy decreasingBy y else do let y ← pure PUnit.unit _do_jp terminationBy decreasingBy y let x : MProd Lean.Elab.WF.TerminationBy Lean.Elab.WF.TerminationHint := r match x with | { fst := terminationBy, snd := decreasingBy } => do Lean.Elab.liftMacroM (Lean.Elab.WF.TerminationBy.ensureAllUsed terminationBy) Lean.Elab.liftMacroM (Lean.Elab.WF.TerminationHint.ensureAllUsed decreasingBy)