aboutsummaryrefslogtreecommitdiff
path: root/plugins/funind
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/funind')
-rw-r--r--plugins/funind/functional_principles_proofs.ml24
-rw-r--r--plugins/funind/functional_principles_proofs.mli3
-rw-r--r--plugins/funind/g_indfun.ml41
-rw-r--r--plugins/funind/indfun.ml6
-rw-r--r--plugins/funind/indfun_common.ml15
-rw-r--r--plugins/funind/indfun_common.mli5
-rw-r--r--plugins/funind/invfun.ml11
-rw-r--r--plugins/funind/merge.ml1
-rw-r--r--plugins/funind/recdef.ml23
-rw-r--r--plugins/funind/recdef.mli2
10 files changed, 42 insertions, 49 deletions
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 48c0f5f04c..55d361e3d2 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -19,12 +19,6 @@ open Context.Rel.Declaration
module RelDecl = Context.Rel.Declaration
-let local_assum (na, t) =
- RelDecl.LocalAssum (na, EConstr.Unsafe.to_constr t)
-
-let local_def (na, b, t) =
- RelDecl.LocalDef (na, EConstr.Unsafe.to_constr b, EConstr.Unsafe.to_constr t)
-
(* let msgnl = Pp.msgnl *)
(*
@@ -235,12 +229,13 @@ let nf_betaiotazeta = (* Reductionops.local_strong Reductionops.whd_betaiotazeta
Reductionops.clos_norm_flags CClosure.betaiotazeta Environ.empty_env Evd.empty
+exception NoChange
let change_eq env sigma hyp_id (context:rel_context) x t end_of_type =
let nochange ?t' msg =
begin
observe (str ("Not treating ( "^msg^" )") ++ pr_leconstr t ++ str " " ++ match t' with None -> str "" | Some t -> Printer.pr_leconstr t );
- failwith "NoChange";
+ raise NoChange;
end
in
let eq_constr c1 c2 = Evarconv.e_conv env (ref sigma) c1 c2 in
@@ -299,7 +294,7 @@ let change_eq env sigma hyp_id (context:rel_context) x t end_of_type =
Can be safely replaced by the next comment for Ocaml >= 3.08.4
*)
let sub = Int.Map.bindings sub in
- List.fold_left (fun end_of_type (i,t) -> lift 1 (substnl [t] (i-1) end_of_type))
+ List.fold_left (fun end_of_type (i,t) -> liftn 1 i (substnl [t] (i-1) end_of_type))
end_of_type_with_pop
sub
in
@@ -542,7 +537,7 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma =
tclTHEN
tac
(scan_type new_context new_t')
- with Failure "NoChange" ->
+ with NoChange ->
(* Last thing todo : push the rel in the context and continue *)
scan_type (LocalAssum (x,t_x) :: context) t'
end
@@ -1401,8 +1396,8 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
let prove_with_tcc tcc_lemma_constr eqs : tactic =
match !tcc_lemma_constr with
- | None -> anomaly (Pp.str "No tcc proof !!")
- | Some lemma ->
+ | Undefined -> anomaly (Pp.str "No tcc proof !!")
+ | Value lemma ->
fun gls ->
(* let hid = next_ident_away_in_goal h_id (pf_ids_of_hyps gls) in *)
(* let ids = hid::pf_ids_of_hyps gls in *)
@@ -1420,7 +1415,7 @@ let prove_with_tcc tcc_lemma_constr eqs : tactic =
Proofview.V82.of_tactic (Eauto.gen_eauto (false,5) [] (Some []))
]
gls
-
+ | Not_needed -> tclIDTAC
let backtrack_eqs_until_hrec hrec eqs : tactic =
fun gls ->
@@ -1599,8 +1594,9 @@ let prove_principle_for_gen
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 !!"
- | Some lemma -> EConstr.of_constr lemma
+ | Undefined -> error "No tcc proof !!"
+ | Value lemma -> EConstr.of_constr lemma
+ | Not_needed -> EConstr.of_constr (Coqlib.build_coq_I ())
in
(* let rec list_diff del_list check_list = *)
(* match del_list with *)
diff --git a/plugins/funind/functional_principles_proofs.mli b/plugins/funind/functional_principles_proofs.mli
index 769d726d70..61752aa339 100644
--- a/plugins/funind/functional_principles_proofs.mli
+++ b/plugins/funind/functional_principles_proofs.mli
@@ -1,5 +1,4 @@
open Names
-open Term
val prove_princ_for_struct :
Evd.evar_map ref ->
@@ -9,7 +8,7 @@ val prove_princ_for_struct :
val prove_principle_for_gen :
constant*constant*constant -> (* name of the function, the functional and the fixpoint equation *)
- constr option ref -> (* a pointer to the obligation proofs lemma *)
+ Indfun_common.tcc_lemma_value ref -> (* a pointer to the obligation proofs lemma *)
bool -> (* is that function uses measure *)
int -> (* the number of recursive argument *)
EConstr.types -> (* the type of the recursive argument *)
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index 0dccd25d75..b5eacee818 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -8,7 +8,6 @@
(*i camlp4deps: "grammar/grammar.cma" i*)
open Ltac_plugin
open Util
-open Term
open Pp
open Constrexpr
open Indfun_common
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index ebeddf5f65..d335836dfc 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -156,7 +156,7 @@ let build_newrecursive
let (rec_sign,rec_impls) =
List.fold_left
(fun (env,impls) (((_,recname),_),bl,arityc,_) ->
- let arityc = Constrexpr_ops.prod_constr_expr arityc bl in
+ let arityc = Constrexpr_ops.mkCProdN Loc.ghost bl arityc in
let arity,ctx = Constrintern.interp_type env0 sigma arityc in
let evdref = ref (Evd.from_env env0) in
let _, (_, impls') = Constrintern.interp_context_evars env evdref bl in
@@ -453,7 +453,7 @@ let generate_correction_proof_wf f_ref tcc_lemma_ref
let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas args ret_type body
pre_hook
=
- let type_of_f = Constrexpr_ops.prod_constr_expr ret_type args in
+ let type_of_f = Constrexpr_ops.mkCProdN Loc.ghost args ret_type in
let rec_arg_num =
let names =
List.map
@@ -484,7 +484,7 @@ let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas
Constrexpr.CApp (Loc.ghost,(None,Constrexpr_ops.mkRefC (Qualid (Loc.ghost,(qualid_of_string "Logic.eq")))),
[(f_app_args,None);(body,None)])
in
- let eq = Constrexpr_ops.prod_constr_expr unbounded_eq args in
+ let eq = Constrexpr_ops.mkCProdN Loc.ghost args unbounded_eq in
let hook ((f_ref,_) as fconst) tcc_lemma_ref (functional_ref,_) (eq_ref,_) rec_arg_num rec_arg_type
nb_args relation =
try
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 20da12f395..848b44a603 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -21,12 +21,9 @@ let get_name avoid ?(default="H") = function
| Name n -> Name n
let array_get_start a =
- try
- Array.init
- (Array.length a - 1)
- (fun i -> a.(i))
- with Invalid_argument "index out of bounds" ->
- invalid_arg "array_get_start"
+ Array.init
+ (Array.length a - 1)
+ (fun i -> a.(i))
let id_of_name = function
Name id -> id
@@ -508,7 +505,6 @@ let list_rewrite (rev:bool) (eqs: (EConstr.constr*bool) list) =
(if rev then (List.rev eqs) else eqs) (tclFAIL 0 (mt())));;
let decompose_lam_n sigma n =
- let open EConstr in
if n < 0 then CErrors.error "decompose_lam_n: integer parameter must be positive";
let rec lamdec_rec l n c =
if Int.equal n 0 then l,c
@@ -543,3 +539,8 @@ let prodn n env b =
(* compose_prod [xn:Tn;..;x1:T1] b = (x1:T1)..(xn:Tn)b *)
let compose_prod l b = prodn (List.length l) l b
+
+type tcc_lemma_value =
+ | Undefined
+ | Value of Constr.constr
+ | Not_needed
diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli
index 5c3e73e9d7..5ef8f05bb7 100644
--- a/plugins/funind/indfun_common.mli
+++ b/plugins/funind/indfun_common.mli
@@ -119,3 +119,8 @@ val decompose_lam_n : Evd.evar_map -> int -> EConstr.t ->
(Names.Name.t * EConstr.t) list * EConstr.t
val compose_lam : (Names.Name.t * EConstr.t) list -> EConstr.t -> EConstr.t
val compose_prod : (Names.Name.t * EConstr.t) list -> EConstr.t -> EConstr.t
+
+type tcc_lemma_value =
+ | Undefined
+ | Value of Constr.constr
+ | Not_needed
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 94ec0a898a..6c0c28905e 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -7,7 +7,6 @@
(************************************************************************)
open Ltac_plugin
-open Tacexpr
open Declarations
open CErrors
open Util
@@ -1026,7 +1025,7 @@ let invfun qhyp f =
| Not_found -> error "No graph found"
| Option.IsNone -> error "Cannot use equivalence with graph!"
-
+exception NoFunction
let invfun qhyp f g =
match f with
| Some f -> invfun qhyp f g
@@ -1041,23 +1040,23 @@ let invfun qhyp f g =
begin
let f1,_ = decompose_app sigma args.(1) in
try
- if not (isConst sigma f1) then failwith "";
+ if not (isConst sigma f1) then raise NoFunction;
let finfos = find_Function_infos (fst (destConst sigma f1)) in
let f_correct = mkConst(Option.get finfos.correctness_lemma)
and kn = fst finfos.graph_ind
in
functional_inversion kn hid f1 f_correct g
- with | Failure "" | Option.IsNone | Not_found ->
+ with | NoFunction | Option.IsNone | Not_found ->
try
let f2,_ = decompose_app sigma args.(2) in
- if not (isConst sigma f2) then failwith "";
+ if not (isConst sigma f2) then raise NoFunction;
let finfos = find_Function_infos (fst (destConst sigma f2)) in
let f_correct = mkConst(Option.get finfos.correctness_lemma)
and kn = fst finfos.graph_ind
in
functional_inversion kn hid f2 f_correct g
with
- | Failure "" ->
+ | NoFunction ->
user_err (str "Hypothesis " ++ Ppconstr.pr_id hid ++ str " must contain at least one Function")
| Option.IsNone ->
if do_observe ()
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index f1ca575856..0af0898a0a 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -19,7 +19,6 @@ open Pp
open Names
open Term
open Vars
-open Termops
open Declarations
open Glob_term
open Glob_termops
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 5460d6fb73..bd30f11596 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -45,12 +45,6 @@ open Indfun_common
open Sigma.Notations
open Context.Rel.Declaration
-let local_assum (na, t) =
- LocalAssum (na, EConstr.Unsafe.to_constr t)
-
-let local_def (na, b, t) =
- LocalDef (na, EConstr.Unsafe.to_constr b, EConstr.Unsafe.to_constr t)
-
(* Ugly things which should not be here *)
let coq_constant m s =
@@ -1231,6 +1225,7 @@ let get_current_subgoals_types () =
let { Evd.it=sgs ; sigma=sigma } = Proof.V82.subgoals p in
sigma, List.map (Goal.V82.abstract_type sigma) sgs
+exception EmptySubgoals
let build_and_l sigma l =
let and_constr = Coqlib.build_coq_and () in
let conj_constr = coq_conj () in
@@ -1252,7 +1247,7 @@ let build_and_l sigma l =
in
let l = List.sort compare l in
let rec f = function
- | [] -> failwith "empty list of subgoals!"
+ | [] -> raise EmptySubgoals
| [p] -> p,tclIDTAC,1
| p1::pl ->
let c,tac,nb = f pl in
@@ -1323,7 +1318,7 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp
| _ -> anomaly ~label:"equation_lemma" (Pp.str "not a constant")
in
let lemma = mkConst (Names.Constant.make1 (Lib.make_kn na)) in
- ref_ := Some (EConstr.Unsafe.to_constr lemma);
+ ref_ := Value (EConstr.Unsafe.to_constr lemma);
let lid = ref [] in
let h_num = ref (-1) in
let env = Global.env () in
@@ -1411,7 +1406,7 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp
let com_terminate
tcc_lemma_name
- (tcc_lemma_ref : Constr.t option ref)
+ tcc_lemma_ref
is_mes
fonctional_ref
input_type
@@ -1438,8 +1433,9 @@ let com_terminate
using_lemmas tcc_lemma_ref
(Some tcc_lemma_name)
(new_goal_type);
- with Failure "empty list of subgoals!" ->
+ with EmptySubgoals ->
(* a non recursive function declared with measure ! *)
+ tcc_lemma_ref := Not_needed;
defined ()
@@ -1515,7 +1511,6 @@ let (com_eqn : int -> Id.t ->
(* Pp.msgnl (str "eqn finished"); *)
);;
-
let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num eq
generate_induction_principle using_lemmas : unit =
let open Term in
@@ -1561,7 +1556,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
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 tcc_lemma_constr = ref Undefined 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
@@ -1590,8 +1585,8 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
and eq_ref = destConst (constr_of_global eq_ref) in
generate_induction_principle f_ref tcc_lemma_constr
functional_ref eq_ref rec_arg_num (EConstr.of_constr rec_arg_type) (nb_prod evm (EConstr.of_constr res)) (EConstr.of_constr relation);
- if Flags.is_verbose ()
- then msgnl (h 1 (Ppconstr.pr_id function_name ++
+ Flags.if_verbose
+ msgnl (h 1 (Ppconstr.pr_id function_name ++
spc () ++ str"is defined" )++ fnl () ++
h 1 (Ppconstr.pr_id equation_id ++
spc () ++ str"is defined" )
diff --git a/plugins/funind/recdef.mli b/plugins/funind/recdef.mli
index 9c1081b9d2..80f02e01c4 100644
--- a/plugins/funind/recdef.mli
+++ b/plugins/funind/recdef.mli
@@ -13,7 +13,7 @@ bool ->
Constrexpr.constr_expr ->
Constrexpr.constr_expr ->
int -> Constrexpr.constr_expr -> (Term.pconstant ->
- Term.constr option ref ->
+ Indfun_common.tcc_lemma_value ref ->
Term.pconstant ->
Term.pconstant -> int -> EConstr.types -> int -> EConstr.constr -> 'a) -> Constrexpr.constr_expr list -> unit
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 08:29:02 +0000