diff --git a/src/Lean/Elab/PreDefinition/Main.lean b/src/Lean/Elab/PreDefinition/Main.lean index 5dba30780a..6a7270b389 100644 --- a/src/Lean/Elab/PreDefinition/Main.lean +++ b/src/Lean/Elab/PreDefinition/Main.lean @@ -89,10 +89,10 @@ def addPreDefinitions (preDefs : Array PreDefinition) (hints : TerminationHints) let mut decrTactic? := none if let some wf := terminationBy.find? (preDefs.map (·.declName)) then wf? := some wf - terminationBy := terminationBy.erase (preDefs.map (·.declName)) + terminationBy := terminationBy.markAsUsed (preDefs.map (·.declName)) if let some { ref, value := decrTactic } := decreasingBy.find? (preDefs.map (·.declName)) then decrTactic? := some (← withRef ref `(by $decrTactic)) - decreasingBy := decreasingBy.erase (preDefs.map (·.declName)) + decreasingBy := decreasingBy.markAsUsed (preDefs.map (·.declName)) if wf?.isSome || decrTactic?.isSome then wfRecursion preDefs wf? decrTactic? else @@ -103,8 +103,8 @@ def addPreDefinitions (preDefs : Array PreDefinition) (hints : TerminationHints) (fun msg => let preDefMsgs := preDefs.toList.map (MessageData.ofExpr $ mkConst ·.declName) m!"fail to show termination for{indentD (MessageData.joinSep preDefMsgs Format.line)}\nwith errors\n{msg}") - liftMacroM <| terminationBy.ensureIsEmpty - liftMacroM <| decreasingBy.ensureIsEmpty + liftMacroM <| terminationBy.ensureAllUsed + liftMacroM <| decreasingBy.ensureAllUsed builtin_initialize registerTraceClass `Elab.definition.body diff --git a/src/Lean/Elab/PreDefinition/WF/Rel.lean b/src/Lean/Elab/PreDefinition/WF/Rel.lean index 09e0b16833..1415e62129 100644 --- a/src/Lean/Elab/PreDefinition/WF/Rel.lean +++ b/src/Lean/Elab/PreDefinition/WF/Rel.lean @@ -21,6 +21,8 @@ def elabWFRel (unaryPreDef : PreDefinition) (wf? : Option TerminationWF) : TermE let pendingMVarIds ← getMVars wfRel discard <| logUnassignedUsingErrorInfos pendingMVarIds return wfRel + | some (TerminationWF.ext clique) => + throwError "`termination_by` syntax is being modified/simplified. To use the old syntax, please use `termination_by'` instead" | none => -- TODO: try to synthesize some default relation throwError "'termination_by' modifier missing" diff --git a/src/Lean/Elab/PreDefinition/WF/TerminationHint.lean b/src/Lean/Elab/PreDefinition/WF/TerminationHint.lean index 5f451a34a6..8272671561 100644 --- a/src/Lean/Elab/PreDefinition/WF/TerminationHint.lean +++ b/src/Lean/Elab/PreDefinition/WF/TerminationHint.lean @@ -7,6 +7,8 @@ import Lean.Parser.Command namespace Lean.Elab.WF +/- Support for `decreasing_by` and `termination_by'` notations -/ + structure TerminationHintValue where ref : Syntax value : Syntax @@ -44,7 +46,7 @@ def expandTerminationHint (terminationHint? : Option Syntax) (cliques : Array (A else return TerminationHint.none -def TerminationHint.erase (t : TerminationHint) (clique : Array Name) : TerminationHint := +def TerminationHint.markAsUsed (t : TerminationHint) (clique : Array Name) : TerminationHint := match t with | TerminationHint.none => TerminationHint.none | TerminationHint.one .. => TerminationHint.none @@ -65,37 +67,131 @@ def TerminationHint.find? (t : TerminationHint) (clique : Array Name) : Option T | TerminationHint.one v => some v | TerminationHint.many m => clique.findSome? m.find? -def TerminationHint.ensureIsEmpty (t : TerminationHint) : MacroM Unit := do +def TerminationHint.ensureAllUsed (t : TerminationHint) : MacroM Unit := do match t with | TerminationHint.one v => Macro.throwErrorAt v.ref "unused termination hint element" | TerminationHint.many m => m.forM fun _ v => Macro.throwErrorAt v.ref "unused termination hint element" | _ => pure () +/- Support for `termination_by` notation -/ + +structure TerminationByElement where + ref : Syntax + declName : Name + vars : Array Syntax + body : Syntax + implicit : Bool + deriving Inhabited + +structure TerminationByClique where + elements : Array TerminationByElement + used : Bool := false + inductive TerminationBy where | core (hint : TerminationHint) + | ext (cliques : Array TerminationByClique) + deriving Inhabited inductive TerminationWF where | core (stx : Syntax) + | ext (clique : Array TerminationByElement) + +/- +``` +def terminationByElement := leading_parser ppLine >> (ident <|> "_") >> many (ident <|> "_") >> " => " >> termParser >> optional ";" +def terminationBy := leading_parser ppLine >> "termination_by " >> many1chIndent terminationByElement +``` +-/ +private def expandTerminationByNonCore (hint : Syntax) (cliques : Array (Array Name)) : MacroM TerminationBy := do + let elementStxs := hint[1].getArgs + let mut alreadyFound : NameSet := {} + let mut elseElemStx? := none + for elementStx in elementStxs do + let declStx := elementStx[0] + let vars := elementStx[1].getArgs + if declStx.isIdent then + let declSuffix := declStx.getId + if alreadyFound.contains declSuffix then + withRef elementStx <| Macro.throwError s!"invalid `termination_by` syntax, `{declSuffix}` case has already been provided" + alreadyFound := alreadyFound.insert declSuffix + if cliques.all fun clique => clique.all fun declName => !declSuffix.isSuffixOf declName then + withRef elementStx <| Macro.throwError s!"function '{declSuffix}' not found in current declaration" + else if elseElemStx?.isSome then + withRef elementStx <| Macro.throwError "invalid `termination_by` syntax, the else-case (i.e., `_ ... => ...`) has already been specified" + else + elseElemStx? := some elementStx + let toElement (declName : Name) (elementStx : Syntax) : TerminationByElement := + let vars := elementStx[1].getArgs + let implicit := !elementStx[0].isIdent + let body := elementStx[3] + { ref := elementStx, declName, vars, implicit, body } + let mut result := #[] + let mut usedElse := false + for clique in cliques do + let mut elements := #[] + for declName in clique do + if let some elementStx := elementStxs.find? fun elementStx => elementStx[0].isIdent && elementStx[0].getId.isSuffixOf declName then + elements := elements.push (toElement declName elementStx) + else if let some elseElemStx := elseElemStx? then + elements := elements.push (toElement declName elseElemStx) + usedElse := true + unless elements.isEmpty do + if let some missing := clique.find? fun declName => elements.find? (·.declName == declName) |>.isNone then + withRef elements[0].ref <| Macro.throwError s!"invalid `termination_by` syntax, missing case for function '{missing}'" + result := result.push { elements } + unless usedElse do + withRef elseElemStx?.get! <| Macro.throwError s!"invalid `termination_by` syntax, unnecessary else-case" + return TerminationBy.ext result def expandTerminationBy (hint? : Option Syntax) (cliques : Array (Array Name)) : MacroM TerminationBy := if let some hint := hint? then if hint.isOfKind ``Parser.Command.terminationByCore then return TerminationBy.core (← expandTerminationHint hint? cliques) + else if hint.isOfKind ``Parser.Command.terminationBy then + expandTerminationByNonCore hint cliques else - withRef hint <| Macro.throwError "`termination_by` syntax is being modified/simplified. To use the old syntax, please use `termination_by'` instead" + Macro.throwUnsupported else return TerminationBy.core TerminationHint.none -def TerminationBy.erase (t : TerminationBy) (clique : Array Name) : TerminationBy := +def TerminationBy.markAsUsed (t : TerminationBy) (cliqueNames : Array Name) : TerminationBy := match t with - | core hint => core (hint.erase clique) + | core hint => core (hint.markAsUsed cliqueNames) + | ext cliques => ext <| cliques.map fun clique => + if cliqueNames.any fun name => clique.elements.any fun elem => elem.declName == name then + { clique with used := true } + else + clique -def TerminationBy.find? (t : TerminationBy) (clique : Array Name) : Option TerminationWF := +def TerminationBy.find? (t : TerminationBy) (cliqueNames : Array Name) : Option TerminationWF := match t with - | core hint => hint.find? clique |>.map fun v => TerminationWF.core v.value + | core hint => hint.find? cliqueNames |>.map fun v => TerminationWF.core v.value + | ext cliques => + cliques.findSome? fun clique => + if cliqueNames.any fun name => clique.elements.any fun elem => elem.declName == name then + some <| TerminationWF.ext clique.elements + else + none -def TerminationBy.ensureIsEmpty (t : TerminationBy) : MacroM Unit := +def TerminationByClique.allImplicit (c : TerminationByClique) : Bool := + c.elements.all fun elem => elem.implicit + +def TerminationByClique.getExplicitElement? (c : TerminationByClique) : Option TerminationByElement := + c.elements.find? (!·.implicit) + +def TerminationBy.ensureAllUsed (t : TerminationBy) : MacroM Unit := match t with - | core hint => hint.ensureIsEmpty + | core hint => hint.ensureAllUsed + | ext cliques => do + let hasUsedAllImplicit := cliques.any fun c => c.allImplicit && c.used + let mut reportedAllImplicit := true + for clique in cliques do + unless clique.used do + if let some explicitElem := clique.getExplicitElement? then + Macro.throwErrorAt explicitElem.ref "unused termination hint element" + else if !hasUsedAllImplicit then + unless reportedAllImplicit do + reportedAllImplicit := true + Macro.throwErrorAt clique.elements[0].ref "unused termination hint element" end Lean.Elab.WF diff --git a/src/Lean/Parser/Command.lean b/src/Lean/Parser/Command.lean index 828db7451a..3a0bdfa656 100644 --- a/src/Lean/Parser/Command.lean +++ b/src/Lean/Parser/Command.lean @@ -33,7 +33,7 @@ def terminationHint (p : Parser) := terminationHintMany p <|> terminationHint1 p def terminationByCore := leading_parser "termination_by' " >> terminationHint termParser def decreasingBy := leading_parser "decreasing_by " >> terminationHint Tactic.tacticSeq -def terminationByElement := leading_parser ppLine >> many (ident <|> "_") >> " => " >> termParser >> optional ";" +def terminationByElement := leading_parser ppLine >> (ident <|> "_") >> many (ident <|> "_") >> " => " >> termParser >> optional ";" def terminationBy := leading_parser ppLine >> "termination_by " >> many1Indent terminationByElement def terminationSuffix := optional (terminationBy <|> terminationByCore) >> optional decreasingBy diff --git a/tests/lean/termination_by2.lean b/tests/lean/termination_by2.lean new file mode 100644 index 0000000000..cc801d0452 --- /dev/null +++ b/tests/lean/termination_by2.lean @@ -0,0 +1,61 @@ +mutual + def f (n : Nat) := + if n == 0 then 0 else f (n / 2) + 1 + termination_by _ => n +end + +def g' (n : Nat) := + match n with + | 0 => 1 + | n+1 => g' n * 3 +termination_by + g' n => n + _ n => n + +mutual + def isEven : Nat → Bool + | 0 => true + | n+1 => isOdd n + def isOdd : Nat → Bool + | 0 => false + | n+1 => isEven n +end +termination_by + isEven x => x -- Error + +mutual + def isEven : Nat → Bool + | 0 => true + | n+1 => isOdd n + def isOdd : Nat → Bool + | 0 => false + | n+1 => isEven n +end +termination_by + isEven x => x + isOd x => x -- Error + +mutual + def isEven : Nat → Bool + | 0 => true + | n+1 => isOdd n + def isOdd : Nat → Bool + | 0 => false + | n+1 => isEven n +end +termination_by + isEven x => x + isEven y => y -- Error + +mutual + def isEven : Nat → Bool + | 0 => true + | n+1 => isOdd n + def isOdd : Nat → Bool + | 0 => false + | n+1 => isEven n +end +termination_by + isEven x => x + _ x => x + _ x => x + 1 -- Error diff --git a/tests/lean/termination_by2.lean.expected.out b/tests/lean/termination_by2.lean.expected.out new file mode 100644 index 0000000000..c11d40cda0 --- /dev/null +++ b/tests/lean/termination_by2.lean.expected.out @@ -0,0 +1,6 @@ +termination_by2.lean:4:1-4:22: error: invalid 'termination_by' in 'mutual' block, it must be used after the 'end' keyword +termination_by2.lean:13:2-13:10: error: invalid `termination_by` syntax, unnecessary else-case +termination_by2.lean:24:3-24:16: error: invalid `termination_by` syntax, missing case for function 'isOdd' +termination_by2.lean:36:3-36:14: error: function 'isOd' not found in current declaration +termination_by2.lean:48:3-48:16: error: invalid `termination_by` syntax, `isEven` case has already been provided +termination_by2.lean:61:3-61:15: error: invalid `termination_by` syntax, the else-case (i.e., `_ ... => ...`) has already been specified