summaryrefslogtreecommitdiff
path: root/plugins/funind/functional_principles_proofs.ml
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/funind/functional_principles_proofs.ml')
-rw-r--r--plugins/funind/functional_principles_proofs.ml123
1 files changed, 71 insertions, 52 deletions
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index c8214ada..4a832435 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -7,7 +7,6 @@ open Context
open Namegen
open Names
open Declarations
-open Declareops
open Pp
open Tacmach
open Proof_type
@@ -16,7 +15,6 @@ open Tactics
open Indfun_common
open Libnames
open Globnames
-open Misctypes
(* let msgnl = Pp.msgnl *)
@@ -46,18 +44,20 @@ let observe_tac s tac g = observe_tac_stream (str s) tac g
let debug_queue = Stack.create ()
-let rec print_debug_queue b e =
+let rec print_debug_queue e =
if not (Stack.is_empty debug_queue)
then
begin
let lmsg,goal = Stack.pop debug_queue in
- if b then
- Pp.msg_debug (lmsg ++ (str " raised exception " ++ Errors.print e) ++ str " on goal " ++ goal)
- else
- begin
- Pp.msg_debug (str " from " ++ lmsg ++ str " on goal " ++ goal);
- end;
- print_debug_queue false e;
+ let _ =
+ match e with
+ | Some e ->
+ Pp.msg_debug (lmsg ++ (str " raised exception " ++ Errors.print e) ++ str " on goal " ++ goal)
+ | None ->
+ begin
+ Pp.msg_debug (str " from " ++ lmsg ++ str " on goal " ++ goal);
+ end in
+ print_debug_queue None ;
end
let observe strm =
@@ -70,13 +70,13 @@ let do_observe_tac s tac g =
let lmsg = (str "observation : ") ++ s in
Stack.push (lmsg,goal) debug_queue;
try
- let v = tac g in
+ let v = tac g in
ignore(Stack.pop debug_queue);
v
with reraise ->
let reraise = Errors.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 (Some (fst (Cerrors.process_vernac_interp_error reraise)));
iraise reraise
let observe_tac_stream s tac g =
@@ -943,13 +943,13 @@ let revert idl =
(generalize (List.map mkVar idl))
(thin idl)
-let generate_equation_lemma fnames f fun_num nb_params nb_args rec_args_num =
+let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num =
(* observe (str "nb_args := " ++ str (string_of_int nb_args)); *)
(* observe (str "nb_params := " ++ str (string_of_int nb_params)); *)
(* observe (str "rec_args_num := " ++ str (string_of_int (rec_args_num + 1) )); *)
let f_def = Global.lookup_constant (fst (destConst f)) in
let eq_lhs = mkApp(f,Array.init (nb_params + nb_args) (fun i -> mkRel(nb_params + nb_args - i))) in
- let f_body = Option.get (Global.body_of_constant_body f_def)in
+ let f_body = Option.get (Global.body_of_constant_body f_def) in
let params,f_body_with_params = decompose_lam_n nb_params f_body in
let (_,num),(_,_,bodies) = destFix f_body_with_params in
let fnames_with_params =
@@ -962,41 +962,48 @@ let generate_equation_lemma fnames f fun_num nb_params nb_args rec_args_num =
let f_body_with_params_and_other_fun = substl fnames_with_params bodies.(num) in
(* observe (str "f_body_with_params_and_other_fun " ++ pr_lconstr f_body_with_params_and_other_fun); *)
let eq_rhs = nf_betaiotazeta (mkApp(compose_lam params f_body_with_params_and_other_fun,Array.init (nb_params + nb_args) (fun i -> mkRel(nb_params + nb_args - i)))) in
-(* observe (str "eq_rhs " ++ pr_lconstr eq_rhs); *)
- let type_ctxt,type_of_f = decompose_prod_n_assum (nb_params + nb_args)
- (Typeops.type_of_constant_type (Global.env ()) (*FIXME*)f_def.const_type) in
+ (* observe (str "eq_rhs " ++ pr_lconstr eq_rhs); *)
+ let (type_ctxt,type_of_f),evd =
+ let evd,t = Typing.e_type_of ~refresh:true (Global.env ()) evd f
+ in
+ decompose_prod_n_assum
+ (nb_params + nb_args) t,evd
+ in
let eqn = mkApp(Lazy.force eq,[|type_of_f;eq_lhs;eq_rhs|]) in
let lemma_type = it_mkProd_or_LetIn eqn type_ctxt in
+ (* Pp.msgnl (str "lemma type " ++ Printer.pr_lconstr lemma_type ++ fnl () ++ str "f_body " ++ Printer.pr_lconstr f_body); *)
let f_id = Label.to_id (con_label (fst (destConst f))) in
let prove_replacement =
tclTHENSEQ
[
tclDO (nb_params + rec_args_num + 1) (Proofview.V82.of_tactic intro);
- (* observe_tac "" *) (fun g ->
+ observe_tac "" (fun g ->
let rec_id = pf_nth_hyp_id g 1 in
tclTHENSEQ
- [(* observe_tac "generalize_non_dep in generate_equation_lemma" *) (generalize_non_dep rec_id);
- (* observe_tac "h_case" *) (Proofview.V82.of_tactic (simplest_case (mkVar rec_id)));
+ [observe_tac "generalize_non_dep in generate_equation_lemma" (generalize_non_dep rec_id);
+ observe_tac "h_case" (Proofview.V82.of_tactic (simplest_case (mkVar rec_id)));
(Proofview.V82.of_tactic intros_reflexivity)] g
)
]
in
+ (* Pp.msgnl (str "lemma type (2) " ++ Printer.pr_lconstr_env (Global.env ()) evd lemma_type); *)
Lemmas.start_proof
(*i The next call to mk_equation_id is valid since we are constructing the lemma
Ensures by: obvious
i*)
(mk_equation_id f_id)
- (Decl_kinds.Global, false, (Decl_kinds.Proof Decl_kinds.Theorem))
- Evd.empty
+ (Decl_kinds.Global, Flags.is_universe_polymorphism (), (Decl_kinds.Proof Decl_kinds.Theorem))
+ evd
lemma_type
(Lemmas.mk_hook (fun _ _ -> ()));
ignore (Pfedit.by (Proofview.V82.tactic prove_replacement));
- Lemmas.save_proof (Vernacexpr.Proved(false,None))
+ Lemmas.save_proof (Vernacexpr.(Proved(Transparent,None)));
+ evd
-let do_replace params rec_arg_num rev_args_id f fun_num all_funs g =
+let do_replace (evd:Evd.evar_map ref) params rec_arg_num rev_args_id f fun_num all_funs g =
let equation_lemma =
try
let finfos = find_Function_infos (fst (destConst f)) (*FIXME*) in
@@ -1007,7 +1014,7 @@ let do_replace params rec_arg_num rev_args_id f fun_num all_funs g =
Ensures by: obvious
i*)
let equation_lemma_id = (mk_equation_id f_id) in
- generate_equation_lemma all_funs f fun_num (List.length params) (List.length rev_args_id) rec_arg_num;
+ evd := generate_equation_lemma !evd all_funs f fun_num (List.length params) (List.length rev_args_id) rec_arg_num;
let _ =
match e with
| Option.IsNone ->
@@ -1020,9 +1027,16 @@ let do_replace params rec_arg_num rev_args_id f fun_num all_funs g =
)
}
| _ -> ()
-
in
- Constrintern.construct_reference (pf_hyps g) equation_lemma_id
+ (* let res = Constrintern.construct_reference (pf_hyps g) equation_lemma_id in *)
+ let evd',res =
+ Evd.fresh_global
+ (Global.env ()) !evd
+ (Constrintern.locate_reference (qualid_of_ident equation_lemma_id))
+ in
+ let evd',_ = Typing.e_type_of ~refresh:true (Global.env ()) evd' res in
+ evd:=evd';
+ res
in
let nb_intro_to_do = nb_prod (pf_concl g) in
tclTHEN
@@ -1031,13 +1045,17 @@ let do_replace params rec_arg_num rev_args_id f fun_num all_funs g =
fun g' ->
let just_introduced = nLastDecls nb_intro_to_do g' in
let just_introduced_id = List.map (fun (id,_,_) -> id) just_introduced in
- tclTHEN (Proofview.V82.of_tactic (Equality.rewriteLR equation_lemma)) (revert just_introduced_id) g'
+ tclTHEN (Proofview.V82.of_tactic (Equality.rewriteLR equation_lemma))
+ (revert just_introduced_id) g'
)
g
-let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams : tactic =
+let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnames all_funs _nparams : tactic =
fun g ->
- let princ_type = pf_concl g in
+ let princ_type = pf_concl g in
+ (* Pp.msgnl (str "princ_type " ++ Printer.pr_lconstr princ_type); *)
+ (* Pp.msgnl (str "all_funs "); *)
+ (* Array.iter (fun c -> Pp.msgnl (Printer.pr_lconstr c)) all_funs; *)
let princ_info = compute_elim_sig princ_type in
let fresh_id =
let avoid = ref (pf_ids_of_hyps g) in
@@ -1101,17 +1119,17 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams :
f_body
)
in
-(* observe (str "full_params := " ++ *)
-(* prlist_with_sep spc (fun (na,_,_) -> Ppconstr.pr_id (Nameops.out_name na)) *)
-(* full_params *)
-(* ); *)
-(* observe (str "princ_params := " ++ *)
-(* prlist_with_sep spc (fun (na,_,_) -> Ppconstr.pr_id (Nameops.out_name na)) *)
-(* princ_params *)
-(* ); *)
-(* observe (str "fbody_with_full_params := " ++ *)
-(* pr_lconstr fbody_with_full_params *)
-(* ); *)
+ observe (str "full_params := " ++
+ prlist_with_sep spc (fun (na,_,_) -> Ppconstr.pr_id (Nameops.out_name na))
+ full_params
+ );
+ observe (str "princ_params := " ++
+ prlist_with_sep spc (fun (na,_,_) -> Ppconstr.pr_id (Nameops.out_name na))
+ princ_params
+ );
+ observe (str "fbody_with_full_params := " ++
+ pr_lconstr fbody_with_full_params
+ );
let all_funs_with_full_params =
Array.map (fun f -> applist(f, List.rev_map var_of_decl full_params)) all_funs
in
@@ -1191,7 +1209,8 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams :
(List.rev princ_info.predicates)
in
pte_to_fix,List.rev rev_info
- | _ -> Id.Map.empty,[]
+ | _ ->
+ Id.Map.empty,[]
in
let mk_fixes : tactic =
let pre_info,infos = list_chop fun_num infos in
@@ -1205,7 +1224,10 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams :
in
if List.is_empty other_fix_infos
then
- (* observe_tac ("h_fix") *) (fix (Some this_fix_info.name) (this_fix_info.idx +1))
+ if this_fix_info.idx + 1 = 0
+ then tclIDTAC (* Someone tries to defined a principle on a fully parametric definition declared as a fixpoint (strange but ....) *)
+ else
+ observe_tac_stream (str "h_fix " ++ int (this_fix_info.idx +1) ) (fix (Some this_fix_info.name) (this_fix_info.idx +1))
else
Tactics.mutual_fix this_fix_info.name (this_fix_info.idx + 1)
other_fix_infos 0
@@ -1213,10 +1235,10 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams :
in
let first_tac : tactic = (* every operations until fix creations *)
tclTHENSEQ
- [ (* observe_tac "introducing params" *) Proofview.V82.of_tactic (intros_using (List.rev_map id_of_decl princ_info.params));
- (* observe_tac "introducing predictes" *) Proofview.V82.of_tactic (intros_using (List.rev_map id_of_decl princ_info.predicates));
- (* observe_tac "introducing branches" *) Proofview.V82.of_tactic (intros_using (List.rev_map id_of_decl princ_info.branches));
- (* observe_tac "building fixes" *) mk_fixes;
+ [ observe_tac "introducing params" (Proofview.V82.of_tactic (intros_using (List.rev_map id_of_decl princ_info.params)));
+ observe_tac "introducing predictes" (Proofview.V82.of_tactic (intros_using (List.rev_map id_of_decl princ_info.predicates)));
+ observe_tac "introducing branches" (Proofview.V82.of_tactic (intros_using (List.rev_map id_of_decl princ_info.branches)));
+ observe_tac "building fixes" mk_fixes;
]
in
let intros_after_fixes : tactic =
@@ -1250,8 +1272,8 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams :
in
tclTHENSEQ
[
-(* observe_tac "do_replace" *)
- (do_replace
+ observe_tac "do_replace"
+ (do_replace evd
full_params
(fix_info.idx + List.length princ_params)
(args_id@(List.map (fun (id,_,_) -> Nameops.out_name id ) princ_params))
@@ -1259,9 +1281,6 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams :
fix_info.num_in_block
all_funs
);
-(* observe_tac "do_replace" *)
-(* (do_replace princ_info.params fix_info.idx args_id *)
-(* (List.hd (List.rev pte_args)) fix_body); *)
let do_prove =
build_proof
interactive_proof
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-15 10:37:37 +0000