aboutsummaryrefslogtreecommitdiff
path: root/plugins/funind
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/funind')
-rw-r--r--plugins/funind/functional_principles_proofs.ml60
-rw-r--r--plugins/funind/functional_principles_types.ml22
-rw-r--r--plugins/funind/g_indfun.ml445
-rw-r--r--plugins/funind/glob_term_to_relation.ml67
-rw-r--r--plugins/funind/glob_termops.ml8
-rw-r--r--plugins/funind/indfun.ml85
-rw-r--r--plugins/funind/indfun.mli4
-rw-r--r--plugins/funind/indfun_common.ml18
-rw-r--r--plugins/funind/invfun.ml42
-rw-r--r--plugins/funind/merge.ml28
-rw-r--r--plugins/funind/recdef.ml72
-rw-r--r--plugins/funind/recdef_plugin.mlpack (renamed from plugins/funind/recdef_plugin.mllib)1
12 files changed, 245 insertions, 207 deletions
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 52094cf085..527f4f0b12 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -1,5 +1,5 @@
open Printer
-open Errors
+open CErrors
open Util
open Term
open Vars
@@ -16,6 +16,8 @@ open Libnames
open Globnames
open Context.Rel.Declaration
+module RelDecl = Context.Rel.Declaration
+
(* let msgnl = Pp.msgnl *)
(*
@@ -27,7 +29,7 @@ let observe strm =
let do_observe_tac s tac g =
try let v = tac g in (* msgnl (goal ++ fnl () ++ (str s)++(str " ")++(str "finished")); *) v
with e ->
- let e = Cerrors.process_vernac_interp_error e in
+ let e = ExplainErr.process_vernac_interp_error e in
let goal = begin try (Printer.pr_goal g) with _ -> assert false end in
msg_debug (str "observation "++ s++str " raised exception " ++
Errors.print e ++ str " on goal " ++ goal );
@@ -52,7 +54,7 @@ let rec print_debug_queue e =
let _ =
match e with
| Some e ->
- Feedback.msg_debug (hov 0 (lmsg ++ (str " raised exception " ++ Errors.print e) ++ str " on goal" ++ fnl() ++ goal))
+ Feedback.msg_debug (hov 0 (lmsg ++ (str " raised exception " ++ CErrors.print e) ++ str " on goal" ++ fnl() ++ goal))
| None ->
begin
Feedback.msg_debug (str " from " ++ lmsg ++ str " on goal" ++ fnl() ++ goal);
@@ -74,9 +76,9 @@ let do_observe_tac s tac g =
ignore(Stack.pop debug_queue);
v
with reraise ->
- let reraise = Errors.push reraise in
+ let reraise = CErrors.push reraise in
if not (Stack.is_empty debug_queue)
- then print_debug_queue (Some (fst (Cerrors.process_vernac_interp_error reraise)));
+ then print_debug_queue (Some (fst (ExplainErr.process_vernac_interp_error reraise)));
iraise reraise
let observe_tac_stream s tac g =
@@ -141,7 +143,7 @@ let is_trivial_eq t =
eq_constr t1 t2 && eq_constr a1 a2
| _ -> false
end
- with e when Errors.noncritical e -> false
+ with e when CErrors.noncritical e -> false
in
(* observe (str "is_trivial_eq " ++ Printer.pr_lconstr t ++ (if res then str " true" else str " false")); *)
res
@@ -167,7 +169,7 @@ let is_incompatible_eq t =
(eq_constr u1 u2 &&
incompatible_constructor_terms t1 t2)
| _ -> false
- with e when Errors.noncritical e -> false
+ with e when CErrors.noncritical e -> false
in
if res then observe (str "is_incompatible_eq " ++ Printer.pr_lconstr t);
res
@@ -223,8 +225,8 @@ let isAppConstruct ?(env=Global.env ()) t =
let nf_betaiotazeta = (* Reductionops.local_strong Reductionops.whd_betaiotazeta *)
let clos_norm_flags flgs env sigma t =
- Closure.norm_val (Closure.create_clos_infos flgs env) (Closure.inject (Reductionops.nf_evar sigma t)) in
- clos_norm_flags Closure.betaiotazeta Environ.empty_env Evd.empty
+ CClosure.norm_val (CClosure.create_clos_infos flgs env) (CClosure.inject (Reductionops.nf_evar sigma t)) in
+ clos_norm_flags CClosure.betaiotazeta Environ.empty_env Evd.empty
@@ -254,7 +256,7 @@ let change_eq env sigma hyp_id (context:Context.Rel.t) x t end_of_type =
then
(jmeq_refl (),(args.(1),args.(0)),(args.(3),args.(2)),args.(0))
else nochange "not an equality"
- with e when Errors.noncritical e -> nochange "not an equality"
+ with e when CErrors.noncritical e -> nochange "not an equality"
in
if not ((closed0 (fst t1)) && (closed0 (snd t1)))then nochange "not a closed lhs";
let rec compute_substitution sub t1 t2 =
@@ -281,7 +283,7 @@ let change_eq env sigma hyp_id (context:Context.Rel.t) x t end_of_type =
List.fold_left2 compute_substitution sub args1 args2
end
else
- if (eq_constr t1 t2) then sub else nochange ~t':(make_refl_eq constructor (Reduction.whd_betadeltaiota env t1) t2) "cannot solve (diff)"
+ if (eq_constr t1 t2) then sub else nochange ~t':(make_refl_eq constructor (Reduction.whd_all env t1) t2) "cannot solve (diff)"
in
let sub = compute_substitution Int.Map.empty (snd t1) (snd t2) in
let sub = compute_substitution sub (fst t1) (fst t2) in
@@ -307,7 +309,7 @@ let change_eq env sigma hyp_id (context:Context.Rel.t) x t end_of_type =
try
let witness = Int.Map.find i sub in
if is_local_def decl then anomaly (Pp.str "can not redefine a rel!");
- (Termops.pop end_of_type,ctxt_size,mkLetIn (get_name decl, witness, get_type decl, witness_fun))
+ (Termops.pop end_of_type,ctxt_size,mkLetIn (RelDecl.get_name decl, witness, RelDecl.get_type decl, witness_fun))
with Not_found ->
(mkProd_or_LetIn decl end_of_type, ctxt_size + 1, mkLambda_or_LetIn decl witness_fun)
)
@@ -625,8 +627,8 @@ let treat_new_case ptes_infos nb_prod continue_tac term dyn_infos =
let my_orelse tac1 tac2 g =
try
tac1 g
- with e when Errors.noncritical e ->
-(* observe (str "using snd tac since : " ++ Errors.print e); *)
+ with e when CErrors.noncritical e ->
+(* observe (str "using snd tac since : " ++ CErrors.print e); *)
tac2 g
let instanciate_hyps_with_args (do_prove:Id.t list -> tactic) hyps args_id =
@@ -938,8 +940,8 @@ let generalize_non_dep hyp g =
((* observe_tac "thin" *) (thin to_revert))
g
-let id_of_decl decl = Nameops.out_name (get_name decl)
-let var_of_decl decl = mkVar (id_of_decl decl)
+let id_of_decl = RelDecl.get_name %> Nameops.out_name
+let var_of_decl = id_of_decl %> mkVar
let revert idl =
tclTHEN
(Proofview.V82.of_tactic (generalize (List.map mkVar idl)))
@@ -1025,7 +1027,7 @@ let do_replace (evd:Evd.evar_map ref) params rec_arg_num rev_args_id f fun_num a
{finfos with
equation_lemma = Some (match Nametab.locate (qualid_of_ident equation_lemma_id) with
ConstRef c -> c
- | _ -> Errors.anomaly (Pp.str "Not a constant")
+ | _ -> CErrors.anomaly (Pp.str "Not a constant")
)
}
| _ -> ()
@@ -1072,7 +1074,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
(Name new_id)
)
in
- let fresh_decl = map_name fresh_id in
+ let fresh_decl = RelDecl.map_name fresh_id in
let princ_info : elim_scheme =
{ princ_info with
params = List.map fresh_decl princ_info.params;
@@ -1085,7 +1087,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
match Global.body_of_constant const with
| Some body ->
Tacred.cbv_norm_flags
- (Closure.RedFlags.mkflags [Closure.RedFlags.fZETA])
+ (CClosure.RedFlags.mkflags [CClosure.RedFlags.fZETA])
(Global.env ())
(Evd.empty)
body
@@ -1119,11 +1121,11 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
)
in
observe (str "full_params := " ++
- prlist_with_sep spc (fun decl -> Ppconstr.pr_id (Nameops.out_name (get_name decl)))
+ prlist_with_sep spc (RelDecl.get_name %> Nameops.out_name %> Ppconstr.pr_id)
full_params
);
observe (str "princ_params := " ++
- prlist_with_sep spc (fun decl -> Ppconstr.pr_id (Nameops.out_name (get_name decl)))
+ prlist_with_sep spc (RelDecl.get_name %> Nameops.out_name %> Ppconstr.pr_id)
princ_params
);
observe (str "fbody_with_full_params := " ++
@@ -1165,7 +1167,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
let pte_to_fix,rev_info =
List.fold_left_i
(fun i (acc_map,acc_info) decl ->
- let pte = get_name decl in
+ let pte = RelDecl.get_name decl in
let infos = info_array.(i) in
let type_args,_ = decompose_prod infos.types in
let nargs = List.length type_args in
@@ -1277,7 +1279,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
(do_replace evd
full_params
(fix_info.idx + List.length princ_params)
- (args_id@(List.map (fun decl -> Nameops.out_name (get_name decl)) princ_params))
+ (args_id@(List.map (RelDecl.get_name %> Nameops.out_name) princ_params))
(all_funs.(fix_info.num_in_block))
fix_info.num_in_block
all_funs
@@ -1556,7 +1558,7 @@ let prove_principle_for_gen
| _ -> assert false
in
(* observe (str "rec_arg_id := " ++ pr_lconstr (mkVar rec_arg_id)); *)
- let subst_constrs = List.map (fun decl -> mkVar (Nameops.out_name (get_name decl))) (pre_rec_arg@princ_info.params) in
+ let subst_constrs = List.map (get_name %> Nameops.out_name %> mkVar) (pre_rec_arg@princ_info.params) in
let relation = substl subst_constrs relation in
let input_type = substl subst_constrs rec_arg_type in
let wf_thm_id = Nameops.out_name (fresh_id (Name (Id.of_string "wf_R"))) in
@@ -1584,7 +1586,7 @@ let prove_principle_for_gen
)
g
in
- let args_ids = List.map (fun decl -> Nameops.out_name (get_name decl)) princ_info.args in
+ let args_ids = List.map (get_name %> Nameops.out_name) princ_info.args in
let lemma =
match !tcc_lemma_ref with
| None -> error "No tcc proof !!"
@@ -1631,7 +1633,7 @@ let prove_principle_for_gen
[
observe_tac "start_tac" start_tac;
h_intros
- (List.rev_map (fun decl -> Nameops.out_name (get_name decl))
+ (List.rev_map (get_name %> Nameops.out_name)
(princ_info.args@princ_info.branches@princ_info.predicates@princ_info.params)
);
(* observe_tac "" *) Proofview.V82.of_tactic (assert_by
@@ -1669,7 +1671,7 @@ let prove_principle_for_gen
in
let acc_inv = lazy (mkApp(Lazy.force acc_inv, [|mkVar acc_rec_arg_id|])) in
let predicates_names =
- List.map (fun decl -> Nameops.out_name (get_name decl)) princ_info.predicates
+ List.map (get_name %> Nameops.out_name) princ_info.predicates
in
let pte_info =
{ proving_tac =
@@ -1685,7 +1687,7 @@ let prove_principle_for_gen
is_mes acc_inv fix_id
(!tcc_list@(List.map
- (fun decl -> (Nameops.out_name (get_name decl)))
+ (get_name %> Nameops.out_name)
(princ_info.args@princ_info.params)
)@ ([acc_rec_arg_id])) eqs
)
@@ -1714,7 +1716,7 @@ let prove_principle_for_gen
(* observe_tac "instanciate_hyps_with_args" *)
(instanciate_hyps_with_args
make_proof
- (List.map (fun decl -> Nameops.out_name (get_name decl)) princ_info.branches)
+ (List.map (get_name %> Nameops.out_name) princ_info.branches)
(List.rev args_ids)
)
gl'
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 5b4fb25955..cc699e5d3d 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -1,5 +1,5 @@
open Printer
-open Errors
+open CErrors
open Util
open Term
open Vars
@@ -14,6 +14,8 @@ open Functional_principles_proofs
open Misctypes
open Sigma.Notations
+module RelDecl = Context.Rel.Declaration
+
exception Toberemoved_with_rel of int*constr
exception Toberemoved
@@ -38,7 +40,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
| Name x ->
let id = Namegen.next_ident_away x avoid in
Hashtbl.add tbl id x;
- set_name (Name id) decl :: change_predicates_names (id::avoid) predicates
+ RelDecl.set_name (Name id) decl :: change_predicates_names (id::avoid) predicates
| Anonymous -> anomaly (Pp.str "Anonymous property binder "))
in
let avoid = (Termops.ids_of_context env_with_params ) in
@@ -51,7 +53,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
(* observe (str "princ_infos : " ++ pr_elim_scheme princ_type_info); *)
let change_predicate_sort i decl =
let new_sort = sorts.(i) in
- let args,_ = decompose_prod (get_type decl) in
+ let args,_ = decompose_prod (RelDecl.get_type decl) in
let real_args =
if princ_type_info.indarg_in_concl
then List.tl args
@@ -358,7 +360,7 @@ let generate_functional_principle (evd: Evd.evar_map ref)
Don't forget to close the goal if an error is raised !!!!
*)
save false new_princ_name entry g_kind hook
- with e when Errors.noncritical e ->
+ with e when CErrors.noncritical e ->
begin
begin
try
@@ -370,7 +372,7 @@ let generate_functional_principle (evd: Evd.evar_map ref)
then Pfedit.delete_current_proof ()
else ()
else ()
- with e when Errors.noncritical e -> ()
+ with e when CErrors.noncritical e -> ()
end;
raise (Defining_principle e)
end
@@ -400,7 +402,7 @@ let get_funs_constant mp dp =
match Global.body_of_constant const with
| Some body ->
let body = Tacred.cbv_norm_flags
- (Closure.RedFlags.mkflags [Closure.RedFlags.fZETA])
+ (CClosure.RedFlags.mkflags [CClosure.RedFlags.fZETA])
(Global.env ())
(Evd.from_env (Global.env ()))
body
@@ -510,7 +512,7 @@ let make_scheme evd (fas : (pconstant*glob_sort) list) : Safe_typing.private_con
0
(prove_princ_for_struct evd false 0 (Array.of_list (List.map fst funs)))
(fun _ _ _ -> ())
- with e when Errors.noncritical e ->
+ with e when CErrors.noncritical e ->
begin
begin
try
@@ -522,7 +524,7 @@ let make_scheme evd (fas : (pconstant*glob_sort) list) : Safe_typing.private_con
then Pfedit.delete_current_proof ()
else ()
else ()
- with e when Errors.noncritical e -> ()
+ with e when CErrors.noncritical e -> ()
end;
raise (Defining_principle e)
end
@@ -609,7 +611,7 @@ let build_scheme fas =
try
Smartlocate.global_with_alias f
with Not_found ->
- errorlabstrm "FunInd.build_scheme"
+ user_err ~hdr:"FunInd.build_scheme"
(str "Cannot find " ++ Libnames.pr_reference f)
in
let evd',f = Evd.fresh_global (Global.env ()) !evd f_as_constant in
@@ -643,7 +645,7 @@ let build_case_scheme fa =
let (_,f,_) = fa in
try fst (Universes.unsafe_constr_of_global (Smartlocate.global_with_alias f))
with Not_found ->
- errorlabstrm "FunInd.build_case_scheme"
+ user_err ~hdr:"FunInd.build_case_scheme"
(str "Cannot find " ++ Libnames.pr_reference f) in
let first_fun,u = destConst funs in
let funs_mp,funs_dp,_ = Names.repr_con first_fun in
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index c63527deaf..6603a95a84 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -14,11 +14,11 @@ open Constrexpr
open Indfun_common
open Indfun
open Genarg
-open Constrarg
+open Stdarg
open Misctypes
open Pcoq.Prim
open Pcoq.Constr
-open Pcoq.Tactic
+open Pltac
DECLARE PLUGIN "recdef_plugin"
@@ -90,7 +90,7 @@ let pr_intro_as_pat _prc _ _ pat =
let out_disjunctive = function
| loc, IntroAction (IntroOrAndPattern l) -> (loc,l)
- | _ -> Errors.error "Disjunctive or conjunctive intro pattern expected."
+ | _ -> CErrors.error "Disjunctive or conjunctive intro pattern expected."
ARGUMENT EXTEND with_names TYPED AS intropattern_opt PRINTED BY pr_intro_as_pat
| [ "as" simple_intropattern(ipat) ] -> [ Some ipat ]
@@ -123,12 +123,12 @@ TACTIC EXTEND snewfunind
END
-let pr_constr_coma_sequence prc _ _ = prlist_with_sep pr_comma prc
+let pr_constr_comma_sequence prc _ _ = prlist_with_sep pr_comma prc
-ARGUMENT EXTEND constr_coma_sequence'
+ARGUMENT EXTEND constr_comma_sequence'
TYPED AS constr_list
- PRINTED BY pr_constr_coma_sequence
-| [ constr(c) "," constr_coma_sequence'(l) ] -> [ c::l ]
+ PRINTED BY pr_constr_comma_sequence
+| [ constr(c) "," constr_comma_sequence'(l) ] -> [ c::l ]
| [ constr(c) ] -> [ [c] ]
END
@@ -137,13 +137,13 @@ let pr_auto_using prc _prlc _prt = Pptactic.pr_auto_using prc
ARGUMENT EXTEND auto_using'
TYPED AS constr_list
PRINTED BY pr_auto_using
-| [ "using" constr_coma_sequence'(l) ] -> [ l ]
+| [ "using" constr_comma_sequence'(l) ] -> [ l ]
| [ ] -> [ [] ]
END
module Gram = Pcoq.Gram
module Vernac = Pcoq.Vernac_
-module Tactic = Pcoq.Tactic
+module Tactic = Pltac
type function_rec_definition_loc_argtype = (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) Loc.located
@@ -162,6 +162,11 @@ GEXTEND Gram
END
+let () =
+ let raw_printer _ _ _ (loc,body) = Ppvernac.pr_rec_definition body in
+ let printer _ _ _ _ = str "<Unavailable printer for rec_definition>" in
+ Pptactic.declare_extra_genarg_pprule wit_function_rec_definition_loc raw_printer printer printer
+
(* TASSI: n'importe quoi ! *)
VERNAC COMMAND EXTEND Function
["Function" ne_function_rec_definition_loc_list_sep(recsl,"with")]
@@ -190,18 +195,16 @@ END
let warning_error names e =
- let (e, _) = Cerrors.process_vernac_interp_error (e, Exninfo.null) in
+ let (e, _) = ExplainErr.process_vernac_interp_error (e, Exninfo.null) in
match e with
| Building_graph e ->
- Feedback.msg_warning
- (str "Cannot define graph(s) for " ++
- h 1 (pr_enum Libnames.pr_reference names) ++
- if do_observe () then (spc () ++ Errors.print e) else mt ())
+ let names = pr_enum Libnames.pr_reference names in
+ let error = if do_observe () then (spc () ++ CErrors.print e) else mt () in
+ warn_cannot_define_graph (names,error)
| Defining_principle e ->
- Feedback.msg_warning
- (str "Cannot define principle(s) for "++
- h 1 (pr_enum Libnames.pr_reference names) ++
- if do_observe () then Errors.print e else mt ())
+ let names = pr_enum Libnames.pr_reference names in
+ let error = if do_observe () then CErrors.print e else mt () in
+ warn_cannot_define_principle (names,error)
| _ -> raise e
@@ -224,15 +227,15 @@ VERNAC COMMAND EXTEND NewFunctionalScheme
;
try Functional_principles_types.build_scheme fas
with Functional_principles_types.No_graph_found ->
- Errors.error ("Cannot generate induction principle(s)")
- | e when Errors.noncritical e ->
+ CErrors.error ("Cannot generate induction principle(s)")
+ | e when CErrors.noncritical e ->
let names = List.map (fun (_,na,_) -> na) fas in
warning_error names e
end
| _ -> assert false (* we can only have non empty list *)
end
- | e when Errors.noncritical e ->
+ | e when CErrors.noncritical e ->
let names = List.map (fun (_,na,_) -> na) fas in
warning_error names e
end
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index c424fe1226..de2e5ea4e2 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -7,11 +7,14 @@ open Glob_term
open Glob_ops
open Globnames
open Indfun_common
-open Errors
+open CErrors
open Util
open Glob_termops
open Misctypes
+module RelDecl = Context.Rel.Declaration
+module NamedDecl = Context.Named.Declaration
+
let observe strm =
if do_observe ()
then Feedback.msg_debug strm
@@ -333,19 +336,20 @@ let raw_push_named (na,raw_value,raw_typ) env =
match na with
| Anonymous -> env
| Name id ->
- let value = Option.map (fun x-> fst (Pretyping.understand env (Evd.from_env env) x)) raw_value in
- let typ,ctx = Pretyping.understand env (Evd.from_env env) ~expected_type:Pretyping.IsType raw_typ in
- let open Context.Named.Declaration in
- Environ.push_named (of_tuple (id,value,typ)) env
+ let typ,_ = Pretyping.understand env (Evd.from_env env) ~expected_type:Pretyping.IsType raw_typ in
+ (match raw_value with
+ | None ->
+ Environ.push_named (NamedDecl.LocalAssum (id,typ)) env
+ | Some value ->
+ Environ.push_named (NamedDecl.LocalDef (id, value, typ)) env)
let add_pat_variables pat typ env : Environ.env =
let rec add_pat_variables env pat typ : Environ.env =
- let open Context.Rel.Declaration in
observe (str "new rel env := " ++ Printer.pr_rel_context_of env (Evd.from_env env));
match pat with
- | PatVar(_,na) -> Environ.push_rel (LocalAssum (na,typ)) env
+ | PatVar(_,na) -> Environ.push_rel (RelDecl.LocalAssum (na,typ)) env
| PatCstr(_,c,patl,na) ->
let Inductiveops.IndType(indf,indargs) =
try Inductiveops.find_rectype env (Evd.from_env env) typ
@@ -353,7 +357,7 @@ let add_pat_variables pat typ env : Environ.env =
in
let constructors = Inductiveops.get_constructors env indf in
let constructor : Inductiveops.constructor_summary = List.find (fun cs -> eq_constructor c (fst cs.Inductiveops.cs_cstr)) (Array.to_list constructors) in
- let cs_args_types :types list = List.map get_type constructor.Inductiveops.cs_args in
+ let cs_args_types :types list = List.map RelDecl.get_type constructor.Inductiveops.cs_args in
List.fold_left2 add_pat_variables env patl (List.rev cs_args_types)
in
let new_env = add_pat_variables env pat typ in
@@ -361,20 +365,28 @@ let add_pat_variables pat typ env : Environ.env =
fst (
Context.Rel.fold_outside
(fun decl (env,ctxt) ->
- let _,v,t = Context.Rel.Declaration.to_tuple decl in
- match Context.Rel.Declaration.get_name decl with
- | Anonymous -> assert false
- | Name id ->
+ let open Context.Rel.Declaration in
+ match decl with
+ | LocalAssum (Anonymous,_) | LocalDef (Anonymous,_,_) -> assert false
+ | LocalAssum (Name id, t) ->
+ let new_t = substl ctxt t in
+ observe (str "for variable " ++ Ppconstr.pr_id id ++ fnl () ++
+ str "old type := " ++ Printer.pr_lconstr t ++ fnl () ++
+ str "new type := " ++ Printer.pr_lconstr new_t ++ fnl ()
+ );
+ let open Context.Named.Declaration in
+ (Environ.push_named (LocalAssum (id,new_t)) env,mkVar id::ctxt)
+ | LocalDef (Name id, v, t) ->
let new_t = substl ctxt t in
- let new_v = Option.map (substl ctxt) v in
+ let new_v = substl ctxt v in
observe (str "for variable " ++ Ppconstr.pr_id id ++ fnl () ++
str "old type := " ++ Printer.pr_lconstr t ++ fnl () ++
str "new type := " ++ Printer.pr_lconstr new_t ++ fnl () ++
- Option.fold_right (fun v _ -> str "old value := " ++ Printer.pr_lconstr v ++ fnl ()) v (mt ()) ++
- Option.fold_right (fun v _ -> str "new value := " ++ Printer.pr_lconstr v ++ fnl ()) new_v (mt ())
+ str "old value := " ++ Printer.pr_lconstr v ++ fnl () ++
+ str "new value := " ++ Printer.pr_lconstr new_v ++ fnl ()
);
let open Context.Named.Declaration in
- (Environ.push_named (of_tuple (id,new_v,new_t)) env,mkVar id::ctxt)
+ (Environ.push_named (LocalDef (id,new_v,new_t)) env,mkVar id::ctxt)
)
(Environ.rel_context new_env)
~init:(env,[])
@@ -402,8 +414,7 @@ let rec pattern_to_term_and_type env typ = function
in
let constructors = Inductiveops.get_constructors env indf in
let constructor = List.find (fun cs -> eq_constructor (fst cs.Inductiveops.cs_cstr) constr) (Array.to_list constructors) in
- let open Context.Rel.Declaration in
- let cs_args_types :types list = List.map get_type constructor.Inductiveops.cs_args in
+ let cs_args_types :types list = List.map RelDecl.get_type constructor.Inductiveops.cs_args in
let _,cstl = Inductiveops.dest_ind_family indf in
let csta = Array.of_list cstl in
let implicit_args =
@@ -602,10 +613,9 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
let v_as_constr,ctx = Pretyping.understand env (Evd.from_env env) v in
let v_type = Typing.unsafe_type_of env (Evd.from_env env) v_as_constr in
let new_env =
- let open Context.Named.Declaration in
match n with
Anonymous -> env
- | Name id -> Environ.push_named (of_tuple (id,Some v_as_constr,v_type)) env
+ | Name id -> Environ.push_named (NamedDecl.LocalDef (id,v_as_constr,v_type)) env
in
let b_res = build_entry_lc new_env funnames avoid b in
combine_results (combine_letin n) v_res b_res
@@ -621,7 +631,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
let (ind,_) =
try Inductiveops.find_inductive env (Evd.from_env env) b_typ
with Not_found ->
- errorlabstrm "" (str "Cannot find the inductive associated to " ++
+ user_err (str "Cannot find the inductive associated to " ++
Printer.pr_glob_constr b ++ str " in " ++
Printer.pr_glob_constr rt ++ str ". try again with a cast")
in
@@ -653,7 +663,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
let (ind,_) =
try Inductiveops.find_inductive env (Evd.from_env env) b_typ
with Not_found ->
- errorlabstrm "" (str "Cannot find the inductive associated to " ++
+ user_err (str "Cannot find the inductive associated to " ++
Printer.pr_glob_constr b ++ str " in " ++
Printer.pr_glob_constr rt ++ str ". try again with a cast")
in
@@ -921,7 +931,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
observe (str "computing new type for eq : " ++ pr_glob_constr rt);
let t' =
try fst (Pretyping.understand env (Evd.from_env env) t)(*FIXME*)
- with e when Errors.noncritical e -> raise Continue
+ with e when CErrors.noncritical e -> raise Continue
in
let is_in_b = is_free_in id b in
let _keep_eq =
@@ -976,8 +986,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
(fun acc var_as_constr arg ->
if isRel var_as_constr
then
- let open Context.Rel.Declaration in
- let na = get_name (Environ.lookup_rel (destRel var_as_constr) env) in
+ let na = RelDecl.get_name (Environ.lookup_rel (destRel var_as_constr) env) in
match na with
| Anonymous -> acc
| Name id' ->
@@ -1189,7 +1198,7 @@ let rec compute_cst_params relnames params = function
| GSort _ -> params
| GHole _ -> params
| GIf _ | GRec _ | GCast _ ->
- raise (UserError("compute_cst_params", str "Not handled case"))
+ raise (UserError(Some "compute_cst_params", str "Not handled case"))
and compute_cst_params_from_app acc (params,rtl) =
match params,rtl with
| _::_,[] -> assert false (* the rel has at least nargs + 1 arguments ! *)
@@ -1223,7 +1232,7 @@ let compute_params_name relnames (args : (Name.t * Glob_term.glob_constr * bool)
l := param::!l
)
rels_params.(0)
- with e when Errors.noncritical e ->
+ with e when CErrors.noncritical e ->
()
in
List.rev !l
@@ -1460,7 +1469,7 @@ let do_build_inductive
str "while trying to define"++ spc () ++
Ppvernac.pr_vernac (Vernacexpr.VernacInductive(false,Decl_kinds.Finite,repacked_rel_inds))
++ fnl () ++
- Errors.print reraise
+ CErrors.print reraise
in
observe msg;
raise reraise
@@ -1476,7 +1485,7 @@ let build_inductive evd funconstants funsargs returned_types rtl =
do_build_inductive evd funconstants funsargs returned_types rtl;
Detyping.print_universes := pu;
Constrextern.print_universes := cu
- with e when Errors.noncritical e ->
+ with e when CErrors.noncritical e ->
Detyping.print_universes := pu;
Constrextern.print_universes := cu;
raise (Building_graph e)
diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml
index 291f835ee7..4e561fc7e5 100644
--- a/plugins/funind/glob_termops.ml
+++ b/plugins/funind/glob_termops.ml
@@ -1,6 +1,6 @@
open Pp
open Glob_term
-open Errors
+open CErrors
open Util
open Names
open Decl_kinds
@@ -406,7 +406,7 @@ let is_free_in id =
| GIf(_,cond,_,br1,br2) ->
is_free_in cond || is_free_in br1 || is_free_in br2
- | GRec _ -> raise (UserError("",str "Not handled GRec"))
+ | GRec _ -> raise (UserError(None,str "Not handled GRec"))
| GSort _ -> false
| GHole _ -> false
| GCast (_,b,(CastConv t|CastVM t|CastNative t)) -> is_free_in b || is_free_in t
@@ -502,7 +502,7 @@ let replace_var_by_term x_id term =
replace_var_by_pattern lhs,
replace_var_by_pattern rhs
)
- | GRec _ -> raise (UserError("",str "Not handled GRec"))
+ | GRec _ -> raise (UserError(None,str "Not handled GRec"))
| GSort _ -> rt
| GHole _ -> rt
| GCast(loc,b,c) ->
@@ -655,7 +655,7 @@ let zeta_normalize =
zeta_normalize_term lhs,
zeta_normalize_term rhs
)
- | GRec _ -> raise (UserError("",str "Not handled GRec"))
+ | GRec _ -> raise (UserError(None,str "Not handled GRec"))
| GSort _ -> rt
| GHole _ -> rt
| GCast(loc,b,c) ->
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 0cacb003d8..99b04898ba 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -1,5 +1,4 @@
-open Context.Rel.Declaration
-open Errors
+open CErrors
open Util
open Names
open Term
@@ -13,11 +12,13 @@ open Misctypes
open Decl_kinds
open Sigma.Notations
+module RelDecl = Context.Rel.Declaration
+
let is_rec_info scheme_info =
let test_branche min acc decl =
acc || (
let new_branche =
- it_mkProd_or_LetIn mkProp (fst (decompose_prod_assum (get_type decl))) in
+ it_mkProd_or_LetIn mkProp (fst (decompose_prod_assum (RelDecl.get_type decl))) in
let free_rels_in_br = Termops.free_rels new_branche in
let max = min + scheme_info.Tactics.npredicates in
Int.Set.exists (fun i -> i >= min && i< max) free_rels_in_br
@@ -42,7 +43,7 @@ let functional_induction with_clean c princl pat =
let finfo = (* we first try to find out a graph on f *)
try find_Function_infos c'
with Not_found ->
- errorlabstrm "" (str "Cannot find induction information on "++
+ user_err (str "Cannot find induction information on "++
Printer.pr_lconstr (mkConst c') )
in
match Tacticals.elimination_sort_of_goal g with
@@ -70,11 +71,11 @@ let functional_induction with_clean c princl pat =
(b,a)
(* mkConst(const_of_id princ_name ),g (\* FIXME *\) *)
with Not_found -> (* This one is neither defined ! *)
- errorlabstrm "" (str "Cannot find induction principle for "
+ user_err (str "Cannot find induction principle for "
++Printer.pr_lconstr (mkConst c') )
in
(princ,NoBindings, Tacmach.pf_unsafe_type_of g' princ,g')
- | _ -> raise (UserError("",str "functional induction must be used with a function" ))
+ | _ -> raise (UserError(None,str "functional induction must be used with a function" ))
end
| Some ((princ,binding)) ->
princ,binding,Tacmach.pf_unsafe_type_of g princ,g
@@ -132,6 +133,7 @@ let rec abstract_glob_constr c = function
| Constrexpr.LocalRawAssum (idl,k,t)::bl ->
List.fold_right (fun x b -> Constrexpr_ops.mkLambdaC([x],k,t,b)) idl
(abstract_glob_constr c bl)
+ | Constrexpr.LocalPattern _::bl -> assert false
let interp_casted_constr_with_implicits env sigma impls c =
Constrintern.intern_gen Pretyping.WithoutTypeConstraint env ~impls
@@ -174,7 +176,7 @@ let build_newrecursive l =
match body_opt with
| Some body ->
(fixna,bll,ar,body)
- | None -> user_err_loc (Loc.ghost,"Function",str "Body of Function must be given")
+ | None -> user_err ~hdr:"Function" (str "Body of Function must be given")
) l
in
build_newrecursive l'
@@ -215,6 +217,7 @@ let rec local_binders_length = function
| [] -> 0
| Constrexpr.LocalRawDef _::bl -> 1 + local_binders_length bl
| Constrexpr.LocalRawAssum (idl,_,_)::bl -> List.length idl + local_binders_length bl
+ | Constrexpr.LocalPattern _::bl -> assert false
let prepare_body ((name,_,args,types,_),_) rt =
let n = local_binders_length args in
@@ -223,7 +226,12 @@ let prepare_body ((name,_,args,types,_),_) rt =
(fun_args,rt')
let process_vernac_interp_error e =
- fst (Cerrors.process_vernac_interp_error (e, Exninfo.null))
+ fst (ExplainErr.process_vernac_interp_error (e, Exninfo.null))
+
+let warn_funind_cannot_build_inversion =
+ CWarnings.create ~name:"funind-cannot-build-inversion" ~category:"funind"
+ (fun e' -> strbrk "Cannot build inversion information" ++
+ if do_observe () then (fnl() ++ CErrors.print e') else mt ())
let derive_inversion fix_names =
try
@@ -265,16 +273,22 @@ let derive_inversion fix_names =
functional_induction
fix_names_as_constant
lind;
- with e when Errors.noncritical e ->
- let e' = process_vernac_interp_error e in
- Feedback.msg_warning
- (str "Cannot build inversion information" ++
- if do_observe () then (fnl() ++ Errors.print e') else mt ())
- with e when Errors.noncritical e ->
+ with e when CErrors.noncritical e ->
let e' = process_vernac_interp_error e in
- Feedback.msg_warning
- (str "Cannot build inversion information (early)" ++
- if do_observe () then (fnl() ++ Errors.print e') else mt ())
+ warn_funind_cannot_build_inversion e'
+ with e when CErrors.noncritical e ->
+ let e' = process_vernac_interp_error e in
+ warn_funind_cannot_build_inversion e'
+
+let warn_cannot_define_graph =
+ CWarnings.create ~name:"funind-cannot-define-graph" ~category:"funind"
+ (fun (names,error) -> strbrk "Cannot define graph(s) for " ++
+ h 1 names ++ error)
+
+let warn_cannot_define_principle =
+ CWarnings.create ~name:"funind-cannot-define-principle" ~category:"funind"
+ (fun (names,error) -> strbrk "Cannot define induction principle(s) for "++
+ h 1 names ++ error)
let warning_error names e =
let e = process_vernac_interp_error e in
@@ -282,37 +296,33 @@ let warning_error names e =
match e with
| ToShow e ->
let e = process_vernac_interp_error e in
- spc () ++ Errors.print e
+ spc () ++ CErrors.print e
| _ ->
if do_observe ()
then
let e = process_vernac_interp_error e in
- (spc () ++ Errors.print e)
+ (spc () ++ CErrors.print e)
else mt ()
in
match e with
| Building_graph e ->
- Feedback.msg_warning
- (str "Cannot define graph(s) for " ++
- h 1 (prlist_with_sep (fun _ -> str","++spc ()) Ppconstr.pr_id names) ++
- e_explain e)
+ let names = prlist_with_sep (fun _ -> str","++spc ()) Ppconstr.pr_id names in
+ warn_cannot_define_graph (names,e_explain e)
| Defining_principle e ->
- Feedback.msg_warning
- (str "Cannot define principle(s) for "++
- h 1 (prlist_with_sep (fun _ -> str","++spc ()) Ppconstr.pr_id names) ++
- e_explain e)
+ let names = prlist_with_sep (fun _ -> str","++spc ()) Ppconstr.pr_id names in
+ warn_cannot_define_principle (names,e_explain e)
| _ -> raise e
let error_error names e =
let e = process_vernac_interp_error e in
let e_explain e =
match e with
- | ToShow e -> spc () ++ Errors.print e
- | _ -> if do_observe () then (spc () ++ Errors.print e) else mt ()
+ | ToShow e -> spc () ++ CErrors.print e
+ | _ -> if do_observe () then (spc () ++ CErrors.print e) else mt ()
in
match e with
| Building_graph e ->
- errorlabstrm ""
+ user_err
(str "Cannot define graph(s) for " ++
h 1 (prlist_with_sep (fun _ -> str","++spc ()) Ppconstr.pr_id names) ++
e_explain e)
@@ -376,13 +386,13 @@ let generate_principle (evd:Evd.evar_map ref) pconstants on_error
Array.iter (add_Function is_general) funs_kn;
()
end
- with e when Errors.noncritical e ->
+ with e when CErrors.noncritical e ->
on_error names e
let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) =
match fixpoint_exprl with
| [(((_,fname),pl),_,bl,ret_type,body),_] when not is_rec ->
- let body = match body with | Some body -> body | None -> user_err_loc (Loc.ghost,"Function",str "Body of Function must be given") in
+ let body = match body with | Some body -> body | None -> user_err ~hdr:"Function" (str "Body of Function must be given") in
Command.do_definition
fname
(Decl_kinds.Global,(Flags.is_universe_polymorphism ()),Decl_kinds.Definition) pl
@@ -466,7 +476,7 @@ let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas
functional_ref eq_ref rec_arg_num rec_arg_type nb_args relation
);
derive_inversion [fname]
- with e when Errors.noncritical e ->
+ with e when CErrors.noncritical e ->
(* No proof done *)
()
in
@@ -621,7 +631,7 @@ let do_generate_principle pconstants on_error register_built interactive_proof
| _ -> assert false
in
let fixpoint_exprl = [fixpoint_expr] in
- let body = match body with | Some body -> body | None -> user_err_loc (Loc.ghost,"Function",str "Body of Function must be given") in
+ let body = match body with | Some body -> body | None -> user_err ~hdr:"Function" (str "Body of Function must be given") in
let recdefs,rec_impls = build_newrecursive fixpoint_exprl in
let using_lemmas = [] in
let pre_hook pconstants =
@@ -647,7 +657,7 @@ let do_generate_principle pconstants on_error register_built interactive_proof
let fixpoint_exprl = [fixpoint_expr] in
let recdefs,rec_impls = build_newrecursive fixpoint_exprl in
let using_lemmas = [] in
- let body = match body with | Some body -> body | None -> user_err_loc (Loc.ghost,"Function",str "Body of Function must be given") in
+ let body = match body with | Some body -> body | None -> user_err ~hdr:"Function" (str "Body of Function must be given") in
let pre_hook pconstants =
generate_principle
(ref (Evd.from_env (Global.env ())))
@@ -825,9 +835,9 @@ let make_graph (f_ref:global_reference) =
| ConstRef c ->
begin try c,Global.lookup_constant c
with Not_found ->
- raise (UserError ("",str "Cannot find " ++ Printer.pr_lconstr (mkConst c)) )
+ raise (UserError (None,str "Cannot find " ++ Printer.pr_lconstr (mkConst c)) )
end
- | _ -> raise (UserError ("", str "Not a function reference") )
+ | _ -> raise (UserError (None, str "Not a function reference") )
in
(match Global.body_of_constant_body c_body with
| None -> error "Cannot build a graph over an axiom !"
@@ -861,6 +871,7 @@ let make_graph (f_ref:global_reference) =
(fun (loc,n) ->
CRef(Libnames.Ident(loc, Nameops.out_name n),None))
nal
+ | Constrexpr.LocalPattern _ -> assert false
)
nal_tas
)
diff --git a/plugins/funind/indfun.mli b/plugins/funind/indfun.mli
index e720691406..1c27bdface 100644
--- a/plugins/funind/indfun.mli
+++ b/plugins/funind/indfun.mli
@@ -1,5 +1,9 @@
open Misctypes
+val warn_cannot_define_graph : ?loc:Loc.t -> Pp.std_ppcmds * Pp.std_ppcmds -> unit
+
+val warn_cannot_define_principle : ?loc:Loc.t -> Pp.std_ppcmds * Pp.std_ppcmds -> unit
+
val do_generate_principle :
bool ->
(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list ->
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 2449678a13..a45effb167 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -49,7 +49,7 @@ let locate_constant ref =
let locate_with_msg msg f x =
try f x
- with Not_found -> raise (Errors.UserError("", msg))
+ with Not_found -> raise (CErrors.UserError(None, msg))
let filter_map filter f =
@@ -73,7 +73,7 @@ let chop_rlambda_n =
| Glob_term.GLambda(_,name,k,t,b) -> chop_lambda_n ((name,t,false)::acc) (n-1) b
| Glob_term.GLetIn(_,name,v,b) -> chop_lambda_n ((name,v,true)::acc) (n-1) b
| _ ->
- raise (Errors.UserError("chop_rlambda_n",
+ raise (CErrors.UserError(Some "chop_rlambda_n",
str "chop_rlambda_n: Not enough Lambdas"))
in
chop_lambda_n []
@@ -85,7 +85,7 @@ let chop_rprod_n =
else
match rt with
| Glob_term.GProd(_,name,k,t,b) -> chop_prod_n ((name,t)::acc) (n-1) b
- | _ -> raise (Errors.UserError("chop_rprod_n",str "chop_rprod_n: Not enough products"))
+ | _ -> raise (CErrors.UserError(Some "chop_rprod_n",str "chop_rprod_n: Not enough products"))
in
chop_prod_n []
@@ -110,7 +110,7 @@ let const_of_id id =
in
try Constrintern.locate_reference princ_ref
with Not_found ->
- Errors.errorlabstrm "IndFun.const_of_id"
+ CErrors.user_err ~hdr:"IndFun.const_of_id"
(str "cannot find " ++ Nameops.pr_id id)
let def_of_const t =
@@ -344,7 +344,7 @@ let pr_info f_info =
(try
Printer.pr_lconstr
(Global.type_of_global_unsafe (ConstRef f_info.function_constant))
- with e when Errors.noncritical e -> mt ()) ++ fnl () ++
+ with e when CErrors.noncritical e -> mt ()) ++ fnl () ++
str "equation_lemma := " ++ pr_ocst f_info.equation_lemma ++ fnl () ++
str "completeness_lemma :=" ++ pr_ocst f_info.completeness_lemma ++ fnl () ++
str "correctness_lemma := " ++ pr_ocst f_info.correctness_lemma ++ fnl () ++
@@ -371,7 +371,7 @@ let in_Function : function_info -> Libobject.obj =
let find_or_none id =
try Some
- (match Nametab.locate (qualid_of_ident id) with ConstRef c -> c | _ -> Errors.anomaly (Pp.str "Not a constant")
+ (match Nametab.locate (qualid_of_ident id) with ConstRef c -> c | _ -> CErrors.anomaly (Pp.str "Not a constant")
)
with Not_found -> None
@@ -399,7 +399,7 @@ let add_Function is_general f =
and prop_lemma = find_or_none (Nameops.add_suffix f_id "_ind")
and graph_ind =
match Nametab.locate (qualid_of_ident (mk_rel_id f_id))
- with | IndRef ind -> ind | _ -> Errors.anomaly (Pp.str "Not an inductive")
+ with | IndRef ind -> ind | _ -> CErrors.anomaly (Pp.str "Not an inductive")
in
let finfos =
{ function_constant = f;
@@ -476,13 +476,13 @@ let jmeq () =
try
Coqlib.check_required_library Coqlib.jmeq_module_name;
Coqlib.gen_constant "Function" ["Logic";"JMeq"] "JMeq"
- with e when Errors.noncritical e -> raise (ToShow e)
+ with e when CErrors.noncritical e -> raise (ToShow e)
let jmeq_refl () =
try
Coqlib.check_required_library Coqlib.jmeq_module_name;
Coqlib.gen_constant "Function" ["Logic";"JMeq"] "JMeq_refl"
- with e when Errors.noncritical e -> raise (ToShow e)
+ with e when CErrors.noncritical e -> raise (ToShow e)
let h_intros l =
tclMAP (fun x -> Proofview.V82.of_tactic (Tactics.Simple.intro x)) l
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 94530bfde2..c8b4e48337 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -8,7 +8,7 @@
open Tacexpr
open Declarations
-open Errors
+open CErrors
open Util
open Names
open Term
@@ -23,6 +23,8 @@ open Misctypes
open Termops
open Context.Rel.Declaration
+module RelDecl = Context.Rel.Declaration
+
(* Some pretty printing function for debugging purpose *)
let pr_binding prc =
@@ -65,16 +67,16 @@ let observe strm =
let do_observe_tac s tac g =
let goal =
try Printer.pr_goal g
- with e when Errors.noncritical e -> assert false
+ with e when CErrors.noncritical e -> assert false
in
try
let v = tac g in
msgnl (goal ++ fnl () ++ s ++(str " ")++(str "finished")); v
with reraise ->
- let reraise = Errors.push reraise in
- let e = Cerrors.process_vernac_interp_error reraise in
+ let reraise = CErrors.push reraise in
+ let e = ExplainErr.process_vernac_interp_error reraise in
observe (hov 0 (str "observation "++ s++str " raised exception " ++
- Errors.iprint e ++ str " on goal" ++ fnl() ++ goal ));
+ CErrors.iprint e ++ str " on goal" ++ fnl() ++ goal ));
iraise reraise;;
@@ -90,7 +92,7 @@ let observe_tac s tac g =
(* [nf_zeta] $\zeta$-normalization of a term *)
let nf_zeta =
- Reductionops.clos_norm_flags (Closure.RedFlags.mkflags [Closure.RedFlags.fZETA])
+ Reductionops.clos_norm_flags (CClosure.RedFlags.mkflags [CClosure.RedFlags.fZETA])
Environ.empty_env
Evd.empty
@@ -137,7 +139,7 @@ let generate_type evd g_to_f f graph i =
let fun_ctxt,res_type =
match ctxt with
| [] | [_] -> anomaly (Pp.str "Not a valid context")
- | decl :: fun_ctxt -> fun_ctxt, get_type decl
+ | decl :: fun_ctxt -> fun_ctxt, RelDecl.get_type decl
in
let rec args_from_decl i accu = function
| [] -> accu
@@ -148,7 +150,7 @@ let generate_type evd g_to_f f graph i =
args_from_decl (succ i) (t :: accu) l
in
(*i We need to name the vars [res] and [fv] i*)
- let filter = fun decl -> match get_name decl with
+ let filter = fun decl -> match RelDecl.get_name decl with
| Name id -> Some id
| Anonymous -> None
in
@@ -269,7 +271,7 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes
(fun decl ->
List.map
(fun id -> Loc.ghost, IntroNaming (IntroIdentifier id))
- (generate_fresh_id (Id.of_string "y") ids (List.length (fst (decompose_prod_assum (get_type decl)))))
+ (generate_fresh_id (Id.of_string "y") ids (List.length (fst (decompose_prod_assum (RelDecl.get_type decl)))))
)
branches
in
@@ -365,7 +367,7 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes
observe_tac("h_intro_patterns ") (let l = (List.nth intro_pats (pred i)) in
match l with
| [] -> tclIDTAC
- | _ -> Proofview.V82.of_tactic (intro_patterns l));
+ | _ -> Proofview.V82.of_tactic (intro_patterns false l));
(* unfolding of all the defined variables introduced by this branch *)
(* observe_tac "unfolding" pre_tac; *)
(* $zeta$ normalizing of the conclusion *)
@@ -399,7 +401,7 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes
| hres::res::decl::ctxt ->
let res = Termops.it_mkLambda_or_LetIn
(Termops.it_mkProd_or_LetIn concl [hres;res])
- (LocalAssum (get_name decl, get_type decl) :: ctxt)
+ (LocalAssum (RelDecl.get_name decl, RelDecl.get_type decl) :: ctxt)
in
res
)
@@ -415,7 +417,7 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes
let params_bindings,avoid =
List.fold_left2
(fun (bindings,avoid) decl p ->
- let id = Namegen.next_ident_away (Nameops.out_name (get_name decl)) avoid in
+ let id = Namegen.next_ident_away (Nameops.out_name (RelDecl.get_name decl)) avoid in
p::bindings,id::avoid
)
([],pf_ids_of_hyps g)
@@ -425,7 +427,7 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes
let lemmas_bindings =
List.rev (fst (List.fold_left2
(fun (bindings,avoid) decl p ->
- let id = Namegen.next_ident_away (Nameops.out_name (get_name decl)) avoid in
+ let id = Namegen.next_ident_away (Nameops.out_name (RelDecl.get_name decl)) avoid in
(nf_zeta p)::bindings,id::avoid)
([],avoid)
princ_infos.predicates
@@ -585,7 +587,7 @@ let rec reflexivity_with_destruct_cases g =
observe_tac "reflexivity_with_destruct_cases" reflexivity_with_destruct_cases
]
| _ -> Proofview.V82.of_tactic reflexivity
- with e when Errors.noncritical e -> Proofview.V82.of_tactic reflexivity
+ with e when CErrors.noncritical e -> Proofview.V82.of_tactic reflexivity
in
let eq_ind = make_eq () in
let discr_inject =
@@ -682,7 +684,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
(fun decl ->
List.map
(fun id -> id)
- (generate_fresh_id (Id.of_string "y") ids (nb_prod (get_type decl)))
+ (generate_fresh_id (Id.of_string "y") ids (nb_prod (RelDecl.get_type decl)))
)
branches
in
@@ -998,7 +1000,7 @@ let invfun qhyp f =
let f =
match f with
| ConstRef f -> f
- | _ -> raise (Errors.UserError("",str "Not a function"))
+ | _ -> raise (CErrors.UserError(None,str "Not a function"))
in
try
let finfos = find_Function_infos f in
@@ -1043,19 +1045,19 @@ let invfun qhyp f g =
functional_inversion kn hid f2 f_correct g
with
| Failure "" ->
- errorlabstrm "" (str "Hypothesis " ++ Ppconstr.pr_id hid ++ str " must contain at least one Function")
+ user_err (str "Hypothesis " ++ Ppconstr.pr_id hid ++ str " must contain at least one Function")
| Option.IsNone ->
if do_observe ()
then
error "Cannot use equivalence with graph for any side of the equality"
- else errorlabstrm "" (str "Cannot find inversion information for hypothesis " ++ Ppconstr.pr_id hid)
+ else user_err (str "Cannot find inversion information for hypothesis " ++ Ppconstr.pr_id hid)
| Not_found ->
if do_observe ()
then
error "No graph found for any side of equality"
- else errorlabstrm "" (str "Cannot find inversion information for hypothesis " ++ Ppconstr.pr_id hid)
+ else user_err (str "Cannot find inversion information for hypothesis " ++ Ppconstr.pr_id hid)
end
- | _ -> errorlabstrm "" (Ppconstr.pr_id hid ++ str " must be an equality ")
+ | _ -> user_err (Ppconstr.pr_id hid ++ str " must be an equality ")
end)
qhyp
end
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index 99a165044c..19c2ed4178 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -11,7 +11,7 @@
open Globnames
open Tactics
open Indfun_common
-open Errors
+open CErrors
open Util
open Constrexpr
open Vernacexpr
@@ -26,6 +26,8 @@ open Glob_termops
open Decl_kinds
open Context.Rel.Declaration
+module RelDecl = Context.Rel.Declaration
+
(** {1 Utilities} *)
(** {2 Useful operations on constr and glob_constr} *)
@@ -57,8 +59,8 @@ let understand = Pretyping.understand (Global.env()) Evd.empty
let id_of_name = function
Anonymous -> Id.of_string "H"
| Name id -> id;;
-let name_of_string str = Name (Id.of_string str)
-let string_of_name nme = Id.to_string (id_of_name nme)
+let name_of_string = Id.of_string %> Name.mk_name
+let string_of_name = id_of_name %> Id.to_string
(** [isVarf f x] returns [true] if term [x] is of the form [(Var f)]. *)
let isVarf f x =
@@ -73,13 +75,13 @@ let ident_global_exist id =
let ans = CRef (Libnames.Ident (Loc.ghost,id), None) in
let _ = ignore (Constrintern.intern_constr (Global.env()) ans) in
true
- with e when Errors.noncritical e -> false
+ with e when CErrors.noncritical e -> false
(** [next_ident_fresh id] returns a fresh identifier (ie not linked in
global env) with base [id]. *)
let next_ident_fresh (id:Id.t) =
let res = ref id in
- while ident_global_exist !res do res := Nameops.lift_subscript !res done;
+ while ident_global_exist !res do res := Nameops.increment_subscript !res done;
!res
@@ -137,7 +139,7 @@ let showind (id:Id.t) =
let mib1,ib1 = Inductive.lookup_mind_specif (Global.env()) (fst ind1) in
List.iter (fun decl ->
print_string (string_of_name (Context.Rel.Declaration.get_name decl) ^ ":");
- prconstr (get_type decl); print_string "\n")
+ prconstr (RelDecl.get_type decl); print_string "\n")
ib1.mind_arity_ctxt;
Printf.printf "arity :"; prconstr (Inductiveops.type_of_inductive (Global.env ()) ind1);
Array.iteri
@@ -460,12 +462,12 @@ let shift_linked_params mib1 mib2 (lnk1:linked_var array) (lnk2:linked_var array
let recprms2,otherprms2,args2,funresprms2 = bldprms (List.rev oib2.mind_arity_ctxt) mlnk2 in
let _ = prstr "\notherprms1:\n" in
let _ =
- List.iter (fun decl -> prstr (string_of_name (get_name decl) ^ " : ");
- prconstr (get_type decl); prstr "\n")
+ List.iter (fun decl -> prstr (string_of_name (RelDecl.get_name decl) ^ " : ");
+ prconstr (RelDecl.get_type decl); prstr "\n")
otherprms1 in
let _ = prstr "\notherprms2:\n" in
let _ =
- List.iter (fun decl -> prstr (string_of_name (get_name decl) ^ " : "); prconstr (get_type decl); prstr "\n")
+ List.iter (fun decl -> prstr (string_of_name (RelDecl.get_name decl) ^ " : "); prconstr (RelDecl.get_type decl); prstr "\n")
otherprms2 in
{
ident=id;
@@ -785,10 +787,10 @@ let merge_inductive_body (shift:merge_infos) avoid (oib1:one_inductive_body)
let params1 =
try fst (glob_decompose_prod_n shift.nrecprms1 (List.hd lcstr1))
- with e when Errors.noncritical e -> [] in
+ with e when CErrors.noncritical e -> [] in
let params2 =
try fst (glob_decompose_prod_n shift.nrecprms2 (List.hd lcstr2))
- with e when Errors.noncritical e -> [] in
+ with e when CErrors.noncritical e -> [] in
let lcstr1 = List.combine (Array.to_list oib1.mind_consnames) lcstr1 in
let lcstr2 = List.combine (Array.to_list oib2.mind_consnames) lcstr2 in
@@ -827,7 +829,7 @@ let merge_rec_params_and_arity prms1 prms2 shift (concl:constr) =
List.fold_left
(fun (acc,env) decl ->
let nm = Context.Rel.Declaration.get_name decl in
- let c = get_type decl in
+ let c = RelDecl.get_type decl in
let typ = Constrextern.extern_constr false env Evd.empty c in
let newenv = Environ.push_rel (LocalAssum (nm,c)) env in
CProdN (Loc.ghost, [[(Loc.ghost,nm)],Constrexpr_ops.default_binder_kind,typ] , acc) , newenv)
@@ -901,7 +903,7 @@ let find_Function_infos_safe (id:Id.t): Indfun_common.function_info =
locate_constant f_ref in
try find_Function_infos (kn_of_id id)
with Not_found ->
- errorlabstrm "indfun" (Nameops.pr_id id ++ str " has no functional scheme")
+ user_err ~hdr:"indfun" (Nameops.pr_id id ++ str " has no functional scheme")
(** [merge id1 id2 args1 args2 id] builds and declares a new inductive
type called [id], representing the merged graphs of both graphs
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 80866e8b8c..e00fa528ad 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -16,7 +16,7 @@ open Names
open Libnames
open Globnames
open Nameops
-open Errors
+open CErrors
open Util
open Tacticals
open Tacmach
@@ -78,8 +78,10 @@ let def_of_const t =
let type_of_const t =
match (kind_of_term t) with
- Const sp -> Typeops.type_of_constant (Global.env()) sp
- |_ -> assert false
+ | Const sp ->
+ (* FIXME discarding universe constraints *)
+ Typeops.type_of_constant_in (Global.env()) sp
+ |_ -> assert false
let constr_of_global x =
fst (Universes.unsafe_constr_of_global x)
@@ -92,15 +94,15 @@ let const_of_ref = function
let nf_zeta env =
- Reductionops.clos_norm_flags (Closure.RedFlags.mkflags [Closure.RedFlags.fZETA])
+ Reductionops.clos_norm_flags (CClosure.RedFlags.mkflags [CClosure.RedFlags.fZETA])
env
Evd.empty
let nf_betaiotazeta = (* Reductionops.local_strong Reductionops.whd_betaiotazeta *)
let clos_norm_flags flgs env sigma t =
- Closure.norm_val (Closure.create_clos_infos flgs env) (Closure.inject (Reductionops.nf_evar sigma t)) in
- clos_norm_flags Closure.betaiotazeta Environ.empty_env Evd.empty
+ CClosure.norm_val (CClosure.create_clos_infos flgs env) (CClosure.inject (Reductionops.nf_evar sigma t)) in
+ clos_norm_flags CClosure.betaiotazeta Environ.empty_env Evd.empty
@@ -161,7 +163,7 @@ let rec n_x_id ids n =
let simpl_iter clause =
reduce
(Lazy
- {rBeta=true;rIota=true;rZeta= true; rDelta=false;
+ {rBeta=true;rMatch=true;rFix=true;rCofix=true;rZeta=true;rDelta=false;
rConst = [ EvalConstRef (const_of_ref (delayed_force iter_ref))]})
clause
@@ -214,7 +216,7 @@ let print_debug_queue b e =
begin
let lmsg,goal = Stack.pop debug_queue in
if b then
- Feedback.msg_debug (hov 1 (lmsg ++ (str " raised exception " ++ Errors.print e) ++ str " on goal" ++ fnl() ++ goal))
+ Feedback.msg_debug (hov 1 (lmsg ++ (str " raised exception " ++ CErrors.print e) ++ str " on goal" ++ fnl() ++ goal))
else
begin
Feedback.msg_debug (hov 1 (str " from " ++ lmsg ++ str " on goal"++fnl() ++ goal));
@@ -238,9 +240,9 @@ let do_observe_tac s tac g =
ignore(Stack.pop debug_queue);
v
with reraise ->
- let reraise = Errors.push reraise in
+ let reraise = CErrors.push reraise in
if not (Stack.is_empty debug_queue)
- then print_debug_queue true (fst (Cerrors.process_vernac_interp_error reraise));
+ then print_debug_queue true (fst (ExplainErr.process_vernac_interp_error reraise));
iraise reraise
let observe_tac s tac g =
@@ -307,7 +309,7 @@ let check_not_nested forbidden e =
| Rel _ -> ()
| Var x ->
if Id.List.mem x forbidden
- then errorlabstrm "Recdef.check_not_nested"
+ then user_err ~hdr:"Recdef.check_not_nested"
(str "check_not_nested: failure " ++ pr_id x)
| Meta _ | Evar _ | Sort _ -> ()
| Cast(e,_,t) -> check_not_nested e;check_not_nested t
@@ -327,7 +329,7 @@ let check_not_nested forbidden e =
try
check_not_nested e
with UserError(_,p) ->
- errorlabstrm "_" (str "on expr : " ++ Printer.pr_lconstr e ++ str " " ++ p)
+ user_err ~hdr:"_" (str "on expr : " ++ Printer.pr_lconstr e ++ str " " ++ p)
(* ['a info] contains the local information for traveling *)
type 'a infos =
@@ -377,7 +379,7 @@ type journey_info =
let rec add_vars forbidden e =
match kind_of_term e with
| Var x -> x::forbidden
- | _ -> fold_constr add_vars forbidden e
+ | _ -> Term.fold_constr add_vars forbidden e
let treat_case forbid_new_ids to_intros finalize_tac nb_lam e infos : tactic =
@@ -441,16 +443,16 @@ let rec travel_aux jinfo continuation_tac (expr_info:constr infos) =
try
check_not_nested (expr_info.f_id::expr_info.forbidden_ids) expr_info.info;
jinfo.otherS () expr_info continuation_tac expr_info
- with e when Errors.noncritical e ->
- errorlabstrm "Recdef.travel" (str "the term " ++ Printer.pr_lconstr expr_info.info ++ str " can not contain a recursive call to " ++ pr_id expr_info.f_id)
+ with e when CErrors.noncritical e ->
+ user_err ~hdr:"Recdef.travel" (str "the term " ++ Printer.pr_lconstr expr_info.info ++ str " can not contain a recursive call to " ++ pr_id expr_info.f_id)
end
| Lambda(n,t,b) ->
begin
try
check_not_nested (expr_info.f_id::expr_info.forbidden_ids) expr_info.info;
jinfo.otherS () expr_info continuation_tac expr_info
- with e when Errors.noncritical e ->
- errorlabstrm "Recdef.travel" (str "the term " ++ Printer.pr_lconstr expr_info.info ++ str " can not contain a recursive call to " ++ pr_id expr_info.f_id)
+ with e when CErrors.noncritical e ->
+ user_err ~hdr:"Recdef.travel" (str "the term " ++ Printer.pr_lconstr expr_info.info ++ str " can not contain a recursive call to " ++ pr_id expr_info.f_id)
end
| Case(ci,t,a,l) ->
begin
@@ -478,7 +480,7 @@ let rec travel_aux jinfo continuation_tac (expr_info:constr infos) =
jinfo.apP (f,args) expr_info continuation_tac in
travel_args jinfo
expr_info.is_main_branch new_continuation_tac new_infos
- | Case _ -> errorlabstrm "Recdef.travel" (str "the term " ++ Printer.pr_lconstr expr_info.info ++ str " can not contain an applied match (See Limitation in Section 2.3 of refman)")
+ | Case _ -> user_err ~hdr:"Recdef.travel" (str "the term " ++ Printer.pr_lconstr expr_info.info ++ str " can not contain an applied match (See Limitation in Section 2.3 of refman)")
| _ -> anomaly (Pp.str "travel_aux : unexpected "++ Printer.pr_lconstr expr_info.info)
end
| Cast(t,_,_) -> travel jinfo continuation_tac {expr_info with info=t}
@@ -645,7 +647,7 @@ let terminate_letin (na,b,t,e) expr_info continuation_tac info =
try
check_not_nested (expr_info.f_id::expr_info.forbidden_ids) b;
true
- with e when Errors.noncritical e -> false
+ with e when CErrors.noncritical e -> false
in
if forbid
then
@@ -704,7 +706,7 @@ let terminate_case next_step (ci,a,t,l) expr_info continuation_tac infos g =
try
check_not_nested (expr_info.f_id::expr_info.forbidden_ids) a;
false
- with e when Errors.noncritical e ->
+ with e when CErrors.noncritical e ->
true
in
let a' = infos.info in
@@ -723,8 +725,8 @@ let terminate_case next_step (ci,a,t,l) expr_info continuation_tac infos g =
(List.map_i (fun i e -> observe_tac (str "do treat case") (treat_case f_is_present to_thin_intro (next_step continuation_tac) ci.ci_cstr_ndecls.(i) e new_info)) 0 (Array.to_list l)
))
with
- | UserError("Refiner.thensn_tac3",_)
- | UserError("Refiner.tclFAIL_s",_) ->
+ | UserError(Some "Refiner.thensn_tac3",_)
+ | UserError(Some "Refiner.tclFAIL_s",_) ->
(observe_tac (str "is computable " ++ Printer.pr_lconstr new_info.info) (next_step continuation_tac {new_info with info = nf_betaiotazeta new_info.info} )
))
g
@@ -1281,12 +1283,12 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp
| Some s -> s
| None ->
try add_suffix current_proof_name "_subproof"
- with e when Errors.noncritical e ->
+ with e when CErrors.noncritical e ->
anomaly (Pp.str "open_new_goal with an unamed theorem")
in
let na = next_global_ident_away name [] in
if Termops.occur_existential gls_type then
- Errors.error "\"abstract\" cannot handle existentials";
+ CErrors.error "\"abstract\" cannot handle existentials";
let hook _ _ =
let opacity =
let na_ref = Libnames.Ident (Loc.ghost,na) in
@@ -1422,7 +1424,7 @@ let start_equation (f:global_reference) (term_f:global_reference)
(cont_tactic:Id.t list -> tactic) g =
let ids = pf_ids_of_hyps g in
let terminate_constr = constr_of_global term_f in
- let nargs = nb_prod (fst (type_of_const terminate_constr)) (*FIXME*) in
+ let nargs = nb_prod (type_of_const terminate_constr) in
let x = n_x_id ids nargs in
observe_tac (str "start_equation") (observe_tclTHENLIST (str "start_equation") [
h_intros x;
@@ -1516,29 +1518,31 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
let functional_id = add_suffix function_name "_F" in
let term_id = add_suffix function_name "_terminate" in
let functional_ref = declare_fun functional_id (IsDefinition Decl_kinds.Definition) ~ctx:(snd (Evd.universe_context evm)) res in
+ (* Refresh the global universes, now including those of _F *)
+ let evm = Evd.from_env (Global.env ()) in
let env_with_pre_rec_args = push_rel_context(List.map (function (x,t) -> LocalAssum (x,t)) pre_rec_args) env in
- let relation =
- fst (*FIXME*)(interp_constr
- env_with_pre_rec_args
- (Evd.from_env env_with_pre_rec_args)
- r)
+ let relation, evuctx =
+ interp_constr env_with_pre_rec_args evm r
in
+ let evm = Evd.from_ctx evuctx in
let tcc_lemma_name = add_suffix function_name "_tcc" in
let tcc_lemma_constr = ref None in
(* let _ = Pp.msgnl (str "relation := " ++ Printer.pr_lconstr_env env_with_pre_rec_args relation) in *)
let hook _ _ =
let term_ref = Nametab.locate (qualid_of_ident term_id) in
let f_ref = declare_f function_name (IsProof Lemma) arg_types term_ref in
- let _ = Table.extraction_inline true [Ident (Loc.ghost,term_id)] in
+ let _ = Extraction_plugin.Table.extraction_inline true [Ident (Loc.ghost,term_id)] in
(* message "start second proof"; *)
let stop =
try com_eqn (List.length res_vars) equation_id functional_ref f_ref term_ref (subst_var function_name equation_lemma_type);
false
- with e when Errors.noncritical e ->
+ with e when CErrors.noncritical e ->
begin
if do_observe ()
- then Feedback.msg_debug (str "Cannot create equation Lemma " ++ Errors.print e)
- else anomaly (Pp.str "Cannot create equation Lemma")
+ then Feedback.msg_debug (str "Cannot create equation Lemma " ++ CErrors.print e)
+ else CErrors.user_err ~hdr:"Cannot create equation Lemma"
+ (str "Cannot create equation lemma." ++ spc () ++
+ str "This may be because the function is nested-recursive.")
;
true
end
diff --git a/plugins/funind/recdef_plugin.mllib b/plugins/funind/recdef_plugin.mlpack
index ec1f5436ca..2b443f2a1b 100644
--- a/plugins/funind/recdef_plugin.mllib
+++ b/plugins/funind/recdef_plugin.mlpack
@@ -8,4 +8,3 @@ Invfun
Indfun
Merge
G_indfun
-Recdef_plugin_mod
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-29 22:27:20 +0000