Equations
- Lean.Elab.WF.instInhabitedTerminationHintValue = { default := { ref := default, value := default } }
Equations
def
Lean.Elab.WF.expandTerminationHint
(terminationHint? : Option Lean.Syntax)
(cliques : Array (Array Lean.Name))
:
Equations
- Lean.Elab.WF.expandTerminationHint terminationHint? cliques = match terminationHint? with | some terminationHint => let ref := terminationHint; let terminationHint := Lean.Syntax.getOp terminationHint 1; if (Lean.Syntax.getKind terminationHint == `Lean.Parser.Command.terminationHint1) = true then pure (Lean.Elab.WF.TerminationHint.one { ref := ref, value := Lean.Syntax.getOp terminationHint 0 }) else if (Lean.Syntax.getKind terminationHint == `Lean.Parser.Command.terminationHintMany) = true then do let m ← Array.foldlM (fun m arg => let declName? := Array.findSome? cliques fun clique => Array.findSome? clique fun declName => if Lean.Name.isSuffixOf (Lean.Syntax.getId (Lean.Syntax.getOp arg 0)) declName = true then some declName else none; match declName? with | none => Lean.Macro.throwErrorAt (Lean.Syntax.getOp arg 0) (toString "function '" ++ toString (Lean.Syntax.getId (Lean.Syntax.getOp arg 0)) ++ toString "' not found in current declaration") | some declName => pure (Lean.NameMap.insert m declName { ref := arg, value := Lean.Syntax.getOp arg 2 })) ∅ (Lean.Syntax.getArgs (Lean.Syntax.getOp terminationHint 0)) 0 (Array.size (Lean.Syntax.getArgs (Lean.Syntax.getOp terminationHint 0))) let r ← forIn cliques PUnit.unit fun clique r => let found? := none; do let r ← forIn clique found? fun declName r => let found? := r; match Lean.NameMap.find? m declName with | some { ref := ref, value := x } => let _do_jp := fun found? y => let found? := some declName; do pure PUnit.unit pure (ForInStep.yield found?); match found? with | some found => do let y ← Lean.Macro.throwErrorAt ref (toString "invalid termination hint element, '" ++ toString declName ++ toString "' and '" ++ toString found ++ toString "' are in the same clique") _do_jp found? y | x => do let y ← pure PUnit.unit _do_jp found? y | x => do pure PUnit.unit pure (ForInStep.yield found?) let x : Option Lean.Name := r let found? : Option Lean.Name := x pure PUnit.unit pure (ForInStep.yield PUnit.unit) let x : PUnit := r pure (Lean.Elab.WF.TerminationHint.many m) else Lean.Macro.throwUnsupported | x => pure Lean.Elab.WF.TerminationHint.none
def
Lean.Elab.WF.TerminationHint.markAsUsed
(t : Lean.Elab.WF.TerminationHint)
(clique : Array Lean.Name)
:
Equations
- Lean.Elab.WF.TerminationHint.markAsUsed t clique = match t with | Lean.Elab.WF.TerminationHint.none => Lean.Elab.WF.TerminationHint.none | Lean.Elab.WF.TerminationHint.one x => Lean.Elab.WF.TerminationHint.none | Lean.Elab.WF.TerminationHint.many m => Id.run do let r ← forIn clique { fst := none, snd := PUnit.unit } fun declName r => let r := r.snd; if Lean.NameMap.contains m declName = true then let m := Std.RBMap.erase m declName; let m := Std.RBMap.erase m declName; if Std.RBMap.isEmpty m = true then pure (ForInStep.done { fst := some Lean.Elab.WF.TerminationHint.none, snd := PUnit.unit }) else pure (ForInStep.done { fst := some (Lean.Elab.WF.TerminationHint.many m), snd := PUnit.unit }) else do pure PUnit.unit pure (ForInStep.yield { fst := none, snd := PUnit.unit }) let x : PUnit := r.snd let _do_jp : PUnit → Id Lean.Elab.WF.TerminationHint := fun y => pure t match r.fst with | none => do let y ← pure PUnit.unit _do_jp y | some a => pure a
def
Lean.Elab.WF.TerminationHint.find?
(t : Lean.Elab.WF.TerminationHint)
(clique : Array Lean.Name)
:
Equations
- Lean.Elab.WF.TerminationHint.find? t clique = match t with | Lean.Elab.WF.TerminationHint.none => none | Lean.Elab.WF.TerminationHint.one v => some v | Lean.Elab.WF.TerminationHint.many m => Array.findSome? clique (Lean.NameMap.find? m)
Equations
- Lean.Elab.WF.TerminationHint.ensureAllUsed t = match t with | Lean.Elab.WF.TerminationHint.one v => Lean.Macro.throwErrorAt v.ref "unused termination hint element" | Lean.Elab.WF.TerminationHint.many m => Std.RBMap.forM (fun x v => Lean.Macro.throwErrorAt v.ref "unused termination hint element") m | x => pure ()
- ref : Lean.Syntax
- declName : Lean.Name
- vars : Array Lean.Syntax
- body : Lean.Syntax
- implicit : Bool
Equations
- Lean.Elab.WF.instInhabitedTerminationByElement = { default := { ref := default, declName := default, vars := default, body := default, implicit := default } }
- elements : Array Lean.Elab.WF.TerminationByElement
- used : Bool
Equations
- Lean.Elab.WF.instInhabitedTerminationBy = { default := Lean.Elab.WF.TerminationBy.core default }
def
Lean.Elab.WF.expandTerminationBy
(hint? : Option Lean.Syntax)
(cliques : Array (Array Lean.Name))
:
Equations
- Lean.Elab.WF.expandTerminationBy hint? cliques = match hint? with | some hint => if Lean.Syntax.isOfKind hint `Lean.Parser.Command.terminationByCore = true then do let a ← Lean.Elab.WF.expandTerminationHint hint? cliques pure (Lean.Elab.WF.TerminationBy.core a) else if Lean.Syntax.isOfKind hint `Lean.Parser.Command.terminationBy = true then Lean.Elab.WF.expandTerminationByNonCore hint cliques else Lean.Macro.throwUnsupported | x => pure (Lean.Elab.WF.TerminationBy.core Lean.Elab.WF.TerminationHint.none)
def
Lean.Elab.WF.TerminationBy.markAsUsed
(t : Lean.Elab.WF.TerminationBy)
(cliqueNames : Array Lean.Name)
:
Equations
- Lean.Elab.WF.TerminationBy.markAsUsed t cliqueNames = match t with | Lean.Elab.WF.TerminationBy.core hint => Lean.Elab.WF.TerminationBy.core (Lean.Elab.WF.TerminationHint.markAsUsed hint cliqueNames) | Lean.Elab.WF.TerminationBy.ext cliques => Lean.Elab.WF.TerminationBy.ext (Array.map (fun clique => if Array.any cliqueNames (fun name => Array.any clique.elements (fun elem => elem.declName == name) 0 (Array.size clique.elements)) 0 (Array.size cliqueNames) = true then { elements := clique.elements, used := true } else clique) cliques)
def
Lean.Elab.WF.TerminationBy.find?
(t : Lean.Elab.WF.TerminationBy)
(cliqueNames : Array Lean.Name)
:
Equations
- Lean.Elab.WF.TerminationBy.find? t cliqueNames = match t with | Lean.Elab.WF.TerminationBy.core hint => Option.map (fun v => Lean.Elab.WF.TerminationWF.core v.value) (Lean.Elab.WF.TerminationHint.find? hint cliqueNames) | Lean.Elab.WF.TerminationBy.ext cliques => Array.findSome? cliques fun clique => if Array.any cliqueNames (fun name => Array.any clique.elements (fun elem => elem.declName == name) 0 (Array.size clique.elements)) 0 (Array.size cliqueNames) = true then some (Lean.Elab.WF.TerminationWF.ext clique.elements) else none
Equations
- Lean.Elab.WF.TerminationByClique.allImplicit c = Array.all c.elements (fun elem => elem.implicit) 0 (Array.size c.elements)
Equations
- Lean.Elab.WF.TerminationByClique.getExplicitElement? c = Array.find? c.elements fun a => !a.implicit
Equations
- Lean.Elab.WF.TerminationBy.ensureAllUsed t = match t with | Lean.Elab.WF.TerminationBy.core hint => Lean.Elab.WF.TerminationHint.ensureAllUsed hint | Lean.Elab.WF.TerminationBy.ext cliques => let hasUsedAllImplicit := Array.any cliques (fun c => Lean.Elab.WF.TerminationByClique.allImplicit c && c.used) 0 (Array.size cliques); let reportedAllImplicit := true; do let r ← forIn cliques reportedAllImplicit fun clique r => let reportedAllImplicit := r; if clique.used = true then do pure PUnit.unit pure (ForInStep.yield reportedAllImplicit) else match Lean.Elab.WF.TerminationByClique.getExplicitElement? clique with | some explicitElem => do Lean.Macro.throwErrorAt explicitElem.ref "unused termination hint element" pure (ForInStep.yield reportedAllImplicit) | x => if (!hasUsedAllImplicit) = true then if reportedAllImplicit = true then do pure PUnit.unit pure (ForInStep.yield reportedAllImplicit) else let reportedAllImplicit := true; do Lean.Macro.throwErrorAt (Array.getOp clique.elements 0).ref "unused termination hint element" pure (ForInStep.yield reportedAllImplicit) else do pure PUnit.unit pure (ForInStep.yield reportedAllImplicit) let x : Bool := r let reportedAllImplicit : Bool := x pure PUnit.unit