From 711d1754a692b67cf8fc24862dc1dbdbaccbe5ef Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 17 Jan 2021 07:24:35 -0800 Subject: [PATCH] chore: improve error message closes #276 --- src/Lean/AuxRecursor.lean | 23 +++++++++++++++++++---- src/Lean/Meta/RecursorInfo.lean | 10 ---------- src/Lean/MonadEnv.lean | 29 ++++++++++++++++++++++++++--- tests/lean/276.lean | 13 +++++++++++++ tests/lean/276.lean.expected.out | 2 ++ 5 files changed, 60 insertions(+), 17 deletions(-) create mode 100644 tests/lean/276.lean create mode 100644 tests/lean/276.lean.expected.out diff --git a/src/Lean/AuxRecursor.lean b/src/Lean/AuxRecursor.lean index 680a7ab2ae..cd969ae410 100644 --- a/src/Lean/AuxRecursor.lean +++ b/src/Lean/AuxRecursor.lean @@ -7,15 +7,30 @@ import Lean.Environment namespace Lean +def casesOnSuffix := "casesOn" +def recOnSuffix := "recOn" +def brecOnSuffix := "brecOn" +def binductionOnSuffix := "binductionOn" + +def mkCasesOnName (indDeclName : Name) : Name := Name.mkStr indDeclName casesOnSuffix +def mkRecOnName (indDeclName : Name) : Name := Name.mkStr indDeclName recOnSuffix +def mkBRecOnName (indDeclName : Name) : Name := Name.mkStr indDeclName brecOnSuffix +def mkBInductionOnName (indDeclName : Name) : Name := Name.mkStr indDeclName binductionOnSuffix + builtin_initialize auxRecExt : TagDeclarationExtension ← mkTagDeclarationExtension `auxRec @[export lean_mark_aux_recursor] -def markAuxRecursor (env : Environment) (n : Name) : Environment := - auxRecExt.tag env n +def markAuxRecursor (env : Environment) (declName : Name) : Environment := + auxRecExt.tag env declName @[export lean_is_aux_recursor] -def isAuxRecursor (env : Environment) (n : Name) : Bool := - auxRecExt.isTagged env n +def isAuxRecursor (env : Environment) (declName : Name) : Bool := + auxRecExt.isTagged env declName + +def isCasesOnRecursor (env : Environment) (declName : Name) : Bool := + match declName with + | Name.str _ s _ => s == casesOnSuffix && isAuxRecursor env declName + | _ => false builtin_initialize noConfusionExt : TagDeclarationExtension ← mkTagDeclarationExtension `noConf diff --git a/src/Lean/Meta/RecursorInfo.lean b/src/Lean/Meta/RecursorInfo.lean index 6c61fb0e81..9b3ca0cba0 100644 --- a/src/Lean/Meta/RecursorInfo.lean +++ b/src/Lean/Meta/RecursorInfo.lean @@ -9,16 +9,6 @@ import Lean.Meta.ExprDefEq namespace Lean.Meta -def casesOnSuffix := "casesOn" -def recOnSuffix := "recOn" -def brecOnSuffix := "brecOn" -def binductionOnSuffix := "binductionOn" - -def mkCasesOnName (indDeclName : Name) : Name := Name.mkStr indDeclName casesOnSuffix -def mkRecOnName (indDeclName : Name) : Name := Name.mkStr indDeclName recOnSuffix -def mkBRecOnName (indDeclName : Name) : Name := Name.mkStr indDeclName brecOnSuffix -def mkBInductionOnName (indDeclName : Name) : Name := Name.mkStr indDeclName binductionOnSuffix - inductive RecursorUnivLevelPos where | motive -- marks where the universe of the motive should go | majorType (idx : Nat) -- marks where the #idx universe of the major premise type goes diff --git a/src/Lean/MonadEnv.lean b/src/Lean/MonadEnv.lean index e0ae9545cb..8cc55614bf 100644 --- a/src/Lean/MonadEnv.lean +++ b/src/Lean/MonadEnv.lean @@ -5,6 +5,9 @@ Authors: Leonardo de Moura -/ import Lean.Environment import Lean.Exception +import Lean.Declaration +import Lean.Util.FindExpr +import Lean.AuxRecursor namespace Lean @@ -16,11 +19,14 @@ def isInductive [Monad m] [MonadEnv m] (declName : Name) : m Bool := do | some (ConstantInfo.inductInfo ..) => return true | _ => return false -def isRec [Monad m] [MonadEnv m] (declName : Name) : m Bool := do - match (← getEnv).find? declName with +def isRecCore (env : Environment) (declName : Name) : Bool := + match env.find? declName with | some (ConstantInfo.recInfo ..) => return true | _ => return false +def isRec [Monad m] [MonadEnv m] (declName : Name) : m Bool := + return isRecCore (← getEnv) declName + @[inline] def withoutModifyingEnv [Monad m] [MonadEnv m] [MonadFinally m] {α : Type} (x : m α) : m α := do let env ← getEnv try x finally setEnv env @@ -99,10 +105,27 @@ def addDecl [Monad m] [MonadEnv m] [MonadError m] [MonadOptions m] (decl : Decla | Except.ok env => setEnv env | Except.error ex => throwKernelException ex +private def supportedRecursors := + #[``Empty.rec, ``False.rec, ``Eq.rec, ``Eq.recOn, ``Eq.casesOn, ``False.casesOn, ``Empty.casesOn, ``And.rec, ``And.casesOn] + +private def checkUnsupported [Monad m] [MonadEnv m] [MonadError m] (decl : Declaration) : m Unit := do + let env ← getEnv + decl.forExprM fun e => + let unsupportedRecursor? := e.find? fun + | Expr.const declName .. => + ((isAuxRecursor env declName && !isCasesOnRecursor env declName) || isRecCore env declName) + && !supportedRecursors.contains declName + | _ => false + match unsupportedRecursor? with + | some (Expr.const declName ..) => throwError! "code generator does not support recursor '{declName}' yet, consider using 'match ... with' and/or structural recursion" + | _ => pure () + def compileDecl [Monad m] [MonadEnv m] [MonadError m] [MonadOptions m] (decl : Declaration) : m Unit := do match (← getEnv).compileDecl (← getOptions) decl with | Except.ok env => setEnv env - | Except.error ex => throwKernelException ex + | Except.error ex => + checkUnsupported decl -- Generate nicer error message for unsupported recursors + throwKernelException ex def addAndCompile [Monad m] [MonadEnv m] [MonadError m] [MonadOptions m] (decl : Declaration) : m Unit := do addDecl decl; diff --git a/tests/lean/276.lean b/tests/lean/276.lean new file mode 100644 index 0000000000..18cc0cdc79 --- /dev/null +++ b/tests/lean/276.lean @@ -0,0 +1,13 @@ +universes u v + +-- `Type u` version can be defined without this option, but I get the same error +set_option bootstrap.inductiveCheckResultingUniverse false in +inductive PEmpty : Sort u + +-- `#check` works +set_option pp.all true in +#check fun {α : Sort v} => PEmpty.rec (fun _ => α) + +-- but `def` doesn't work +-- error: (kernel) compiler failed to infer low level type, unknown declaration 'PEmpty.rec' +def PEmpty.elim {α : Sort v} := PEmpty.rec (fun _ => α) diff --git a/tests/lean/276.lean.expected.out b/tests/lean/276.lean.expected.out new file mode 100644 index 0000000000..4ece2a454d --- /dev/null +++ b/tests/lean/276.lean.expected.out @@ -0,0 +1,2 @@ +fun {α} => PEmpty.rec.{v, u_1} fun x => α : {α : Sort v} → PEmpty.{u_1} → α +276.lean:13:4-13:8: error: code generator does not support recursor 'PEmpty.rec' yet, consider using 'match ... with' and/or structural recursion