From 3f0cc1d2ecca9a614ae009adce8f3fcf8a59417a Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 24 Oct 2020 18:50:34 -0700 Subject: [PATCH] fix: `library/constructions` primitives crash at `kernel_exception` --- src/Lean/Declaration.lean | 2 +- src/Lean/Elab/Inductive.lean | 14 +++++----- src/Lean/Elab/PreDefinition/Structural.lean | 8 +++--- src/Lean/Elab/Structure.lean | 6 ++--- src/Lean/Elab/Tactic/Induction.lean | 2 +- src/Lean/Meta/RecursorInfo.lean | 10 +++---- src/Lean/Meta/Tactic/Cases.lean | 2 +- src/Lean/Util/Constructions.lean | 30 ++++++++++++++++----- src/library/constructions/brec_on.cpp | 26 ++++-------------- src/library/constructions/cases_on.cpp | 7 ++--- src/library/constructions/no_confusion.cpp | 7 ++--- src/library/constructions/rec_on.cpp | 7 ++--- 12 files changed, 56 insertions(+), 65 deletions(-) diff --git a/src/Lean/Declaration.lean b/src/Lean/Declaration.lean index c9d82c33d8..c86d1bf26c 100644 --- a/src/Lean/Declaration.lean +++ b/src/Lean/Declaration.lean @@ -352,7 +352,7 @@ constant instantiateValueLevelParams (c : @& ConstantInfo) (ls : @& List Level) end ConstantInfo -def mkRecFor (declName : Name) : Name := +def mkRecName (declName : Name) : Name := mkNameStr declName "rec" end Lean diff --git a/src/Lean/Elab/Inductive.lean b/src/Lean/Elab/Inductive.lean index 15878b1fcd..f7064c88fc 100644 --- a/src/Lean/Elab/Inductive.lean +++ b/src/Lean/Elab/Inductive.lean @@ -405,15 +405,15 @@ let hasUnit := env.contains `PUnit let hasProd := env.contains `Prod for view in views do let n := view.declName - modifyEnv fun env => mkRecOn env n - if hasUnit then modifyEnv fun env => mkCasesOn env n - if hasUnit && hasEq && hasHEq then modifyEnv fun env => mkNoConfusion env n - if hasUnit && hasProd then modifyEnv fun env => mkBelow env n - if hasUnit && hasProd then modifyEnv fun env => mkIBelow env n + mkRecOn n + if hasUnit then mkCasesOn n + if hasUnit && hasEq && hasHEq then mkNoConfusion n + if hasUnit && hasProd then mkBelow n + if hasUnit && hasProd then mkIBelow n for view in views do let n := view.declName; - if hasUnit && hasProd then modifyEnv fun env => mkBRecOn env n - if hasUnit && hasProd then modifyEnv fun env => mkBInductionOn env n + if hasUnit && hasProd then mkBRecOn n + if hasUnit && hasProd then mkBInductionOn n private def mkInductiveDecl (vars : Array Expr) (views : Array InductiveView) : TermElabM Unit := do let view0 := views[0] diff --git a/src/Lean/Elab/PreDefinition/Structural.lean b/src/Lean/Elab/PreDefinition/Structural.lean index ce1b50073e..f1d5252ad7 100644 --- a/src/Lean/Elab/PreDefinition/Structural.lean +++ b/src/Lean/Elab/PreDefinition/Structural.lean @@ -75,9 +75,9 @@ private partial def findRecArg {α} (numFixed : Nat) (xs : Array Expr) (k : RecA else let xType ← whnfD localDecl.type matchConstInduct xType.getAppFn (fun _ => loop (i+1)) fun indInfo us => do - if !(← hasConst (mkBRecOnFor indInfo.name)) then + if !(← hasConst (mkBRecOnName indInfo.name)) then loop (i+1) - else if indInfo.isReflexive && !(← hasConst (mkBInductionOnFor indInfo.name)) then + else if indInfo.isReflexive && !(← hasConst (mkBInductionOnName indInfo.name)) then loop (i+1) else let indArgs := xType.getAppArgs @@ -308,9 +308,9 @@ private def mkBRecOn (recFnName : Name) (recArgInfo : RecArgInfo) (value : Expr) trace[Elab.definition.structural]! "brecOn motive: {motive}" let brecOn := if useBInductionOn then - Lean.mkConst (mkBInductionOnFor recArgInfo.indName) recArgInfo.indLevels + Lean.mkConst (mkBInductionOnName recArgInfo.indName) recArgInfo.indLevels else - Lean.mkConst (mkBRecOnFor recArgInfo.indName) (brecOnUniv :: recArgInfo.indLevels) + Lean.mkConst (mkBRecOnName recArgInfo.indName) (brecOnUniv :: recArgInfo.indLevels) let brecOn := mkAppN brecOn recArgInfo.indParams let brecOn := mkApp brecOn motive let brecOn := mkAppN brecOn recArgInfo.indIndices diff --git a/src/Lean/Elab/Structure.lean b/src/Lean/Elab/Structure.lean index ccd6236681..45b47ac9ed 100644 --- a/src/Lean/Elab/Structure.lean +++ b/src/Lean/Elab/Structure.lean @@ -431,9 +431,9 @@ private def mkAuxConstructions (declName : Name) : TermElabM Unit := do let hasUnit := env.contains `PUnit let hasEq := env.contains `Eq let hasHEq := env.contains `HEq - modifyEnv fun env => mkRecOn env declName - if hasUnit then modifyEnv fun env => mkCasesOn env declName - if hasUnit && hasEq && hasHEq then modifyEnv fun env => mkNoConfusion env declName + mkRecOn declName + if hasUnit then mkCasesOn declName + if hasUnit && hasEq && hasHEq then mkNoConfusion declName private def addDefaults (lctx : LocalContext) (defaultAuxDecls : Array (Name × Expr × Expr)) : TermElabM Unit := do let localInsts ← getLocalInstances diff --git a/src/Lean/Elab/Tactic/Induction.lean b/src/Lean/Elab/Tactic/Induction.lean index 51fd809dd1..3f46aa967d 100644 --- a/src/Lean/Elab/Tactic/Induction.lean +++ b/src/Lean/Elab/Tactic/Induction.lean @@ -148,7 +148,7 @@ match ← getRecFromUsingLoop baseRecName (← inferType major) with /- Create `RecInfo` assuming builtin recursor -/ private def getRecInfoDefault (major : Expr) (withAlts : Syntax) (allowMissingAlts : Bool) : TacticM (RecInfo × Array Name) := do let indVal ← getInductiveValFromMajor major -let recName := mkRecFor indVal.name +let recName := mkRecName indVal.name if withAlts.isNone then pure ({ recName := recName }, #[]) else diff --git a/src/Lean/Meta/RecursorInfo.lean b/src/Lean/Meta/RecursorInfo.lean index 3b17f0fdbd..1072a407ec 100644 --- a/src/Lean/Meta/RecursorInfo.lean +++ b/src/Lean/Meta/RecursorInfo.lean @@ -15,10 +15,10 @@ def recOnSuffix := "recOn" def brecOnSuffix := "brecOn" def binductionOnSuffix := "binductionOn" -def mkCasesOnFor (indDeclName : Name) : Name := mkNameStr indDeclName casesOnSuffix -def mkRecOnFor (indDeclName : Name) : Name := mkNameStr indDeclName recOnSuffix -def mkBRecOnFor (indDeclName : Name) : Name := mkNameStr indDeclName brecOnSuffix -def mkBInductionOnFor (indDeclName : Name) : Name := mkNameStr indDeclName binductionOnSuffix +def mkCasesOnName (indDeclName : Name) : Name := mkNameStr indDeclName casesOnSuffix +def mkRecOnName (indDeclName : Name) : Name := mkNameStr indDeclName recOnSuffix +def mkBRecOnName (indDeclName : Name) : Name := mkNameStr indDeclName brecOnSuffix +def mkBInductionOnName (indDeclName : Name) : Name := mkNameStr indDeclName binductionOnSuffix inductive RecursorUnivLevelPos | motive -- marks where the universe of the motive should go @@ -112,7 +112,7 @@ else do if s != recOnSuffix && s != casesOnSuffix && s != brecOnSuffix then pure none else do - let val ← getConstInfoRec (mkRecFor p) + let val ← getConstInfoRec (mkRecName p) pure $ some (val.nparams + val.nindices + (if s == casesOnSuffix then 1 else val.nmotives)) | _ => pure none diff --git a/src/Lean/Meta/Tactic/Cases.lean b/src/Lean/Meta/Tactic/Cases.lean index 3aaeaa8d16..e1ddabf2f9 100644 --- a/src/Lean/Meta/Tactic/Cases.lean +++ b/src/Lean/Meta/Tactic/Cases.lean @@ -254,7 +254,7 @@ private def inductionCasesOn (mvarId : MVarId) (majorFVarId : FVarId) (givenName withMVarContext mvarId do let majorType ← inferType (mkFVar majorFVarId) let (us, params) ← getInductiveUniverseAndParams majorType - let casesOn := mkCasesOnFor ctx.inductiveVal.name + let casesOn := mkCasesOnName ctx.inductiveVal.name let ctors := ctx.inductiveVal.ctors.toArray let s ← induction mvarId majorFVarId casesOn givenNames useUnusedNames pure $ toCasesSubgoals s ctors majorFVarId us params diff --git a/src/Lean/Util/Constructions.lean b/src/Lean/Util/Constructions.lean index 874a1ca24a..01f1d11208 100644 --- a/src/Lean/Util/Constructions.lean +++ b/src/Lean/Util/Constructions.lean @@ -5,15 +5,31 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ import Lean.Environment +import Lean.MonadEnv namespace Lean -@[extern "lean_mk_cases_on"] constant mkCasesOn (env : Environment) (name : @& Name) : Environment := env -@[extern "lean_mk_rec_on"] constant mkRecOn (env : Environment) (name : @& Name) : Environment := env -@[extern "lean_mk_no_confusion"] constant mkNoConfusion (env : Environment) (name : @& Name) : Environment := env -@[extern "lean_mk_below"] constant mkBelow (env : Environment) (name : @& Name) : Environment := env -@[extern "lean_mk_ibelow"] constant mkIBelow (env : Environment) (name : @& Name) : Environment := env -@[extern "lean_mk_brec_on"] constant mkBRecOn (env : Environment) (name : @& Name) : Environment := env -@[extern "lean_mk_binduction_on"] constant mkBInductionOn (env : Environment) (name : @& Name) : Environment := env +@[extern "lean_mk_cases_on"] constant mkCasesOnImp (env : Environment) (declName : @& Name) : Except KernelException Environment +@[extern "lean_mk_rec_on"] constant mkRecOnImp (env : Environment) (declName : @& Name) : Except KernelException Environment +@[extern "lean_mk_no_confusion"] constant mkNoConfusionImp (env : Environment) (declName : @& Name) : Except KernelException Environment +@[extern "lean_mk_below"] constant mkBelowImp (env : Environment) (declName : @& Name) : Except KernelException Environment +@[extern "lean_mk_ibelow"] constant mkIBelowImp (env : Environment) (declName : @& Name) : Except KernelException Environment +@[extern "lean_mk_brec_on"] constant mkBRecOnImp (env : Environment) (declName : @& Name) : Except KernelException Environment +@[extern "lean_mk_binduction_on"] constant mkBInductionOnImp (env : Environment) (declName : @& Name) : Except KernelException Environment + +variables {m} [Monad m] [MonadEnv m] [MonadExceptOf Exception m] [Ref m] [AddErrorMessageContext m] [MonadOptions m] + +@[inline] private def adaptFn (f : Environment → Name → Except KernelException Environment) (declName : Name) : m Unit := do + match f (← getEnv) declName with + | Except.ok env => modifyEnv fun _ => env + | Except.error ex => throwKernelException ex + +def mkCasesOn (declName : Name) : m Unit := adaptFn mkCasesOnImp declName +def mkRecOn (declName : Name) : m Unit := adaptFn mkRecOnImp declName +def mkNoConfusion (declName : Name) : m Unit := adaptFn mkNoConfusionImp declName +def mkBelow (declName : Name) : m Unit := adaptFn mkBelowImp declName +def mkIBelow (declName : Name) : m Unit := adaptFn mkIBelowImp declName +def mkBRecOn (declName : Name) : m Unit := adaptFn mkBRecOnImp declName +def mkBInductionOn (declName : Name) : m Unit := adaptFn mkBInductionOnImp declName end Lean diff --git a/src/library/constructions/brec_on.cpp b/src/library/constructions/brec_on.cpp index ce5e5a9e10..3ef5f3476c 100644 --- a/src/library/constructions/brec_on.cpp +++ b/src/library/constructions/brec_on.cpp @@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #include +#include "kernel/kernel_exception.h" #include "kernel/environment.h" #include "kernel/instantiate.h" #include "kernel/abstract.h" @@ -357,35 +358,18 @@ environment mk_binduction_on(environment const & env, name const & n) { } extern "C" object * lean_mk_below(object * env, object * n) { - try { - return mk_below(environment(env), name(n, true)).steal(); - } catch (exception &) { - return env; - } + return catch_kernel_exceptions([&]() { return mk_below(environment(env), name(n, true)); }); } extern "C" object * lean_mk_ibelow(object * env, object * n) { - try { - return mk_ibelow(environment(env), name(n, true)).steal(); - } catch (exception &) { - return env; - } + return catch_kernel_exceptions([&]() { return mk_ibelow(environment(env), name(n, true)); }); } extern "C" object * lean_mk_brec_on(object * env, object * n) { - try { - return mk_brec_on(environment(env), name(n, true)).steal(); - } catch (exception &) { - return env; - } + return catch_kernel_exceptions([&]() { return mk_brec_on(environment(env), name(n, true)); }); } extern "C" object * lean_mk_binduction_on(object * env, object * n) { - try { - return mk_binduction_on(environment(env), name(n, true)).steal(); - } catch (exception &) { - return env; - } + return catch_kernel_exceptions([&]() { return mk_binduction_on(environment(env), name(n, true)); }); } - } diff --git a/src/library/constructions/cases_on.cpp b/src/library/constructions/cases_on.cpp index 3a407b1abe..0d1c3ac30a 100644 --- a/src/library/constructions/cases_on.cpp +++ b/src/library/constructions/cases_on.cpp @@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #include +#include "kernel/kernel_exception.h" #include "kernel/environment.h" #include "kernel/instantiate.h" #include "kernel/abstract.h" @@ -188,10 +189,6 @@ environment mk_cases_on(environment const & env, name const & n) { } extern "C" object * lean_mk_cases_on(object * env, object * n) { - try { - return mk_cases_on(environment(env), name(n, true)).steal(); - } catch (exception &) { - return env; - } + return catch_kernel_exceptions([&]() { return mk_cases_on(environment(env), name(n, true)); }); } } diff --git a/src/library/constructions/no_confusion.cpp b/src/library/constructions/no_confusion.cpp index 2bfb963e7f..92da2f12b4 100644 --- a/src/library/constructions/no_confusion.cpp +++ b/src/library/constructions/no_confusion.cpp @@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #include +#include "kernel/kernel_exception.h" #include "kernel/environment.h" #include "kernel/instantiate.h" #include "kernel/abstract.h" @@ -237,10 +238,6 @@ environment mk_no_confusion(environment const & env, name const & n) { } extern "C" object * lean_mk_no_confusion(object * env, object * n) { - try { - return mk_no_confusion(environment(env), name(n, true)).steal(); - } catch (exception &) { - return env; - } + return catch_kernel_exceptions([&]() { return mk_no_confusion(environment(env), name(n, true)); }); } } diff --git a/src/library/constructions/rec_on.cpp b/src/library/constructions/rec_on.cpp index f39f28beec..70a896ab49 100644 --- a/src/library/constructions/rec_on.cpp +++ b/src/library/constructions/rec_on.cpp @@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #include +#include "kernel/kernel_exception.h" #include "kernel/environment.h" #include "kernel/instantiate.h" #include "kernel/abstract.h" @@ -62,10 +63,6 @@ environment mk_rec_on(environment const & env, name const & n) { } extern "C" object * lean_mk_rec_on(object * env, object * n) { - try { - return mk_rec_on(environment(env), name(n, true)).steal(); - } catch (exception &) { - return env; - } + return catch_kernel_exceptions([&]() { return mk_rec_on(environment(env), name(n, true)); }); } }