diff options
Diffstat (limited to 'toplevel/indschemes.ml')
| -rw-r--r-- | toplevel/indschemes.ml | 57 |
1 files changed, 41 insertions, 16 deletions
diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml index c4ac0e41..e8ea617f 100644 --- a/toplevel/indschemes.ml +++ b/toplevel/indschemes.ml @@ -15,7 +15,7 @@ declaring new schemes *) open Pp -open Errors +open CErrors open Util open Names open Declarations @@ -38,6 +38,7 @@ open Ind_tables open Auto_ind_decl open Eqschemes open Elimschemes +open Context.Rel.Declaration (* Flags governing automatic synthesis of schemes *) @@ -149,16 +150,18 @@ let alarm what internal msg = | UserAutomaticRequest | InternalTacticRequest -> (if debug then - msg_warning - (hov 0 msg ++ fnl () ++ what ++ str " not defined.")) - | _ -> errorlabstrm "" msg + Feedback.msg_debug + (hov 0 msg ++ fnl () ++ what ++ str " not defined.")); None + | _ -> Some msg let try_declare_scheme what f internal names kn = try f internal names kn - with + with e -> + let e = CErrors.push e in + let msg = match fst e with | ParameterWithoutEquality cst -> alarm what internal - (str "Boolean equality not found for parameter " ++ pr_con cst ++ + (str "Boolean equality not found for parameter " ++ Printer.pr_global cst ++ str".") | InductiveWithProduct -> alarm what internal @@ -183,9 +186,14 @@ let try_declare_scheme what f internal names kn = | DecidabilityMutualNotSupported -> alarm what internal (str "Decidability lemma for mutual inductive types not supported.") - | e when Errors.noncritical e -> + | e when CErrors.noncritical e -> alarm what internal - (str "Unexpected error during scheme creation: " ++ Errors.print e) + (str "Unexpected error during scheme creation: " ++ CErrors.print e) + | _ -> iraise e + in + match msg with + | None -> () + | Some msg -> iraise (UserError ("", msg), snd e) let beq_scheme_msg mind = let mib = Global.lookup_mind mind in @@ -209,7 +217,11 @@ let declare_beq_scheme = declare_beq_scheme_with [] let declare_one_case_analysis_scheme ind = let (mib,mip) = Global.lookup_inductive ind in let kind = inductive_sort_family mip in - let dep = if kind == InProp then case_scheme_kind_from_prop else case_dep_scheme_kind_from_type in + let dep = + if kind == InProp then case_scheme_kind_from_prop + else if not (Inductiveops.has_dependent_elim mib) then + case_scheme_kind_from_type + else case_dep_scheme_kind_from_type in let kelim = elim_sorts (mib,mip) in (* in case the inductive has a type elimination, generates only one induction scheme, the other ones share the same code with the @@ -229,15 +241,23 @@ let kinds_from_type = InProp,ind_dep_scheme_kind_from_type; InSet,rec_dep_scheme_kind_from_type] +let nondep_kinds_from_type = + [InType,rect_scheme_kind_from_type; + InProp,ind_scheme_kind_from_type; + InSet,rec_scheme_kind_from_type] + let declare_one_induction_scheme ind = let (mib,mip) = Global.lookup_inductive ind in let kind = inductive_sort_family mip in let from_prop = kind == InProp in + let depelim = Inductiveops.has_dependent_elim mib in let kelim = elim_sorts (mib,mip) in let elims = List.map_filter (fun (sort,kind) -> if Sorts.List.mem sort kelim then Some kind else None) - (if from_prop then kinds_from_prop else kinds_from_type) in + (if from_prop then kinds_from_prop + else if depelim then kinds_from_type + else nondep_kinds_from_type) in List.iter (fun kind -> ignore (define_individual_scheme kind UserAutomaticRequest None ind)) elims @@ -270,7 +290,7 @@ let try_declare_eq_decidability kn = let declare_eq_decidability = declare_eq_decidability_scheme_with [] let ignore_error f x = - try ignore (f x) with e when Errors.noncritical e -> () + try ignore (f x) with e when CErrors.noncritical e -> () let declare_rewriting_schemes ind = if Hipattern.is_inductive_equality ind then begin @@ -287,15 +307,20 @@ let declare_rewriting_schemes ind = (define_individual_scheme rew_l2r_forward_dep_scheme_kind UserAutomaticRequest None) ind end +let warn_cannot_build_congruence = + CWarnings.create ~name:"cannot-build-congruence" ~category:"schemes" + (fun () -> + strbrk "Cannot build congruence scheme because eq is not found") + let declare_congr_scheme ind = if Hipattern.is_equality_type (mkInd ind) then begin if try Coqlib.check_required_library Coqlib.logic_module_name; true - with e when Errors.noncritical e -> false + with e when CErrors.noncritical e -> false then ignore (define_individual_scheme congr_scheme_kind UserAutomaticRequest None ind) else - msg_warning (strbrk "Cannot build congruence scheme because eq is not found") + warn_cannot_build_congruence () end let declare_sym_scheme ind = @@ -379,7 +404,6 @@ let do_mutual_induction_scheme lnamedepindsort = let sigma, listdecl = Indrec.build_mutual_induction_scheme env0 sigma lrecspec in let declare decl fi lrecref = let decltype = Retyping.get_type_of env0 sigma decl in - (* let decltype = refresh_universes decltype in *) let proof_output = Future.from_val ((decl,Univ.ContextSet.empty),Safe_typing.empty_private_constants) in let cst = define fi UserIndividualRequest sigma proof_output (Some decltype) in ConstRef cst :: lrecref @@ -463,7 +487,7 @@ let build_combined_scheme env schemes = in let ctx, _ = list_split_rev_at prods - (List.rev_map (fun (x, y) -> x, None, y) ctx) in + (List.rev_map (fun (x, y) -> LocalAssum (x, y)) ctx) in let typ = it_mkProd_wo_LetIn concl_typ ctx in let body = it_mkLambda_or_LetIn concl_bod ctx in (body, typ) @@ -489,7 +513,8 @@ let map_inductive_block f kn n = for i=0 to n-1 do f (kn,i) done let declare_default_schemes kn = let mib = Global.lookup_mind kn in let n = Array.length mib.mind_packets in - if !elim_flag && (mib.mind_finite <> BiFinite || !bifinite_elim_flag) then + if !elim_flag && (mib.mind_finite <> BiFinite || !bifinite_elim_flag) + && mib.mind_typing_flags.check_guarded then declare_induction_schemes kn; if !case_flag then map_inductive_block declare_one_case_analysis_scheme kn n; if is_eq_flag() then try_declare_beq_scheme kn; |