diff options
| author | Hugo Herbelin | 2015-07-27 10:50:04 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2015-07-27 14:20:44 +0200 |
| commit | cb6c3ec2e66e3019cb9ee881b1e222e6e3691463 (patch) | |
| tree | 40d68c6bbc43e6794a1eb1d836d985de35eb4ffb | |
| parent | cb145fa37d463210832c437f013231c9f028e1aa (diff) | |
Fixing bug #3736 (anomaly instead of error/warning/silence on
decidability scheme).
Not clear to me why it is not a warning (in verbose mode) rather than
silence when a scheme supposed to be built automatically cannot be
built, as in:
Set Decidable Equality Schemes.
Inductive a := A with b := B.
which could explain why a_beq and a_eq_dec as well as b_beq and
b_eq_dec are not built.
| -rw-r--r-- | test-suite/bugs/closed/3736.v | 8 | ||||
| -rw-r--r-- | toplevel/auto_ind_decl.ml | 3 | ||||
| -rw-r--r-- | toplevel/auto_ind_decl.mli | 1 | ||||
| -rw-r--r-- | toplevel/indschemes.ml | 3 |
4 files changed, 14 insertions, 1 deletions
diff --git a/test-suite/bugs/closed/3736.v b/test-suite/bugs/closed/3736.v new file mode 100644 index 0000000000..637b77cc58 --- /dev/null +++ b/test-suite/bugs/closed/3736.v @@ -0,0 +1,8 @@ +(* Check non-error failure in case of unsupported decidability scheme *) +Local Set Decidable Equality Schemes. + +Inductive a := A with b := B. + +(* But fails with error if explicitly asked for the scheme *) + +Fail Scheme Equality for a. diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml index f905080905..d1452fca21 100644 --- a/toplevel/auto_ind_decl.ml +++ b/toplevel/auto_ind_decl.ml @@ -55,6 +55,7 @@ exception InductiveWithProduct exception InductiveWithSort exception ParameterWithoutEquality of constant exception NonSingletonProp of inductive +exception DecidabilityMutualNotSupported let dl = Loc.ghost @@ -921,7 +922,7 @@ let compute_dec_tact ind lnamesparrec nparrec = let make_eq_decidability mind = let mib = Global.lookup_mind mind in if not (Int.equal (Array.length mib.mind_packets) 1) then - anomaly (Pp.str "Decidability lemma for mutual inductive types not supported"); + raise DecidabilityMutualNotSupported; let ind = (mind,0) in let nparams = mib.mind_nparams in let nparrec = mib.mind_nparams_rec in diff --git a/toplevel/auto_ind_decl.mli b/toplevel/auto_ind_decl.mli index 807872988b..20a3d5d74f 100644 --- a/toplevel/auto_ind_decl.mli +++ b/toplevel/auto_ind_decl.mli @@ -23,6 +23,7 @@ exception InductiveWithProduct exception InductiveWithSort exception ParameterWithoutEquality of constant exception NonSingletonProp of inductive +exception DecidabilityMutualNotSupported val beq_scheme_kind : mutual scheme_kind val build_beq_scheme : mutual_scheme_object_function diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml index fbc45b4ae3..f8f062dad6 100644 --- a/toplevel/indschemes.ml +++ b/toplevel/indschemes.ml @@ -180,6 +180,9 @@ let try_declare_scheme what f internal names kn = (strbrk "Required constant " ++ str s ++ str " undefined.") | AlreadyDeclared msg -> alarm what internal (msg ++ str ".") + | DecidabilityMutualNotSupported -> + alarm what internal + (str "Decidability lemma for mutual inductive types not supported.") | e when Errors.noncritical e -> alarm what internal (str "Unknown exception during scheme creation: "++ |