summaryrefslogtreecommitdiff
path: root/contrib/funind
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/funind')
-rw-r--r--contrib/funind/Recdef.v48
-rw-r--r--contrib/funind/functional_principles_proofs.ml88
-rw-r--r--contrib/funind/functional_principles_types.ml25
-rw-r--r--contrib/funind/g_indfun.ml4 (renamed from contrib/funind/indfun_main.ml4)67
-rw-r--r--contrib/funind/indfun.ml114
-rw-r--r--contrib/funind/indfun_common.ml57
-rw-r--r--contrib/funind/invfun.ml76
-rw-r--r--contrib/funind/merge.ml514
-rw-r--r--contrib/funind/rawterm_to_relation.ml41
-rw-r--r--contrib/funind/rawtermops.ml142
-rw-r--r--contrib/funind/rawtermops.mli8
-rw-r--r--contrib/funind/recdef.ml1430
-rw-r--r--contrib/funind/tacinv.ml4872
-rw-r--r--contrib/funind/tacinvutils.ml284
-rw-r--r--contrib/funind/tacinvutils.mli80
15 files changed, 2188 insertions, 1658 deletions
diff --git a/contrib/funind/Recdef.v b/contrib/funind/Recdef.v
new file mode 100644
index 00000000..2d206220
--- /dev/null
+++ b/contrib/funind/Recdef.v
@@ -0,0 +1,48 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+Require Compare_dec.
+Require Wf_nat.
+
+Section Iter.
+Variable A : Type.
+
+Fixpoint iter (n : nat) : (A -> A) -> A -> A :=
+ fun (fl : A -> A) (def : A) =>
+ match n with
+ | O => def
+ | S m => fl (iter m fl def)
+ end.
+End Iter.
+
+Theorem SSplus_lt : forall p p' : nat, p < S (S (p + p')).
+ intro p; intro p'; change (S p <= S (S (p + p')));
+ apply le_S; apply Gt.gt_le_S; change (p < S (p + p'));
+ apply Lt.le_lt_n_Sm; apply Plus.le_plus_l.
+Qed.
+
+
+Theorem Splus_lt : forall p p' : nat, p' < S (p + p').
+ intro p; intro p'; change (S p' <= S (p + p'));
+ apply Gt.gt_le_S; change (p' < S (p + p')); apply Lt.le_lt_n_Sm;
+ apply Plus.le_plus_r.
+Qed.
+
+Theorem le_lt_SS : forall x y, x <= y -> x < S (S y).
+intro x; intro y; intro H; change (S x <= S (S y));
+ apply le_S; apply Gt.gt_le_S; change (x < S y);
+ apply Lt.le_lt_n_Sm; exact H.
+Qed.
+
+Inductive max_type (m n:nat) : Set :=
+ cmt : forall v, m <= v -> n <= v -> max_type m n.
+
+Definition max : forall m n:nat, max_type m n.
+intros m n; case (Compare_dec.le_gt_dec m n).
+intros h; exists n; [exact h | apply le_n].
+intros h; exists m; [apply le_n | apply Lt.lt_le_weak; exact h].
+Defined.
diff --git a/contrib/funind/functional_principles_proofs.ml b/contrib/funind/functional_principles_proofs.ml
index 975cf60b..3d80bd00 100644
--- a/contrib/funind/functional_principles_proofs.ml
+++ b/contrib/funind/functional_principles_proofs.ml
@@ -47,7 +47,7 @@ let observe_tac_stream s tac g =
let observe_tac s tac g = observe_tac_stream (str s) tac g
(* let tclTRYD tac = *)
-(* if !Options.debug || do_observe () *)
+(* if !Flags.debug || do_observe () *)
(* then (fun g -> try (\* do_observe_tac "" *\)tac g with _ -> tclIDTAC g) *)
(* else tac *)
@@ -140,7 +140,7 @@ let change_hyp_with_using msg hyp_id t tac : tactic =
[tclTHENLIST
[
(* observe_tac "change_hyp_with_using thin" *) (thin [hyp_id]);
- (* observe_tac "change_hyp_with_using rename " *) (h_rename prov_id hyp_id)
+ (* observe_tac "change_hyp_with_using rename " *) (h_rename [prov_id,hyp_id])
]] g
exception TOREMOVE
@@ -573,7 +573,7 @@ let instanciate_hyps_with_args (do_prove:identifier list -> tactic) hyps args_id
tclTHENLIST[
forward None (Genarg.IntroIdentifier prov_hid) (mkApp(mkVar hid,args));
thin [hid];
- (h_rename prov_hid hid)
+ h_rename [prov_hid,hid]
] g
)
( (*
@@ -637,7 +637,7 @@ let build_proof
[
h_generalize (term_eq::(List.map mkVar dyn_infos.rec_hyps));
thin dyn_infos.rec_hyps;
- pattern_option [[-1],t] None;
+ pattern_option [(false,[1]),t] None;
h_simplest_case t;
(fun g' ->
let g'_nb_prod = nb_prod (pf_concl g') in
@@ -882,7 +882,7 @@ let generate_equation_lemma fnames f fun_num nb_params nb_args rec_args_num =
let f_def = Global.lookup_constant (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 =
- force (out_some f_def.const_body)
+ force (Option.get f_def.const_body)
in
let params,f_body_with_params = decompose_lam_n nb_params f_body in
let (_,num),(_,_,bodies) = destFix f_body_with_params in
@@ -910,7 +910,7 @@ let generate_equation_lemma fnames f fun_num nb_params nb_args rec_args_num =
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" *) (h_case (mkVar rec_id,Rawterm.NoBindings));
+ (* observe_tac "h_case" *) (h_case false (mkVar rec_id,Rawterm.NoBindings));
intros_reflexivity] g
)
]
@@ -933,8 +933,8 @@ let do_replace params rec_arg_num rev_args_id f fun_num all_funs g =
let equation_lemma =
try
let finfos = find_Function_infos (destConst f) in
- mkConst (out_some finfos.equation_lemma)
- with (Not_found | Failure "out_some" as e) ->
+ mkConst (Option.get finfos.equation_lemma)
+ with (Not_found | Option.IsNone as e) ->
let f_id = id_of_label (con_label (destConst f)) in
(*i The next call to mk_equation_id is valid since we will construct the lemma
Ensures by: obvious
@@ -943,7 +943,7 @@ let do_replace params rec_arg_num rev_args_id f fun_num all_funs g =
generate_equation_lemma all_funs f fun_num (List.length params) (List.length rev_args_id) rec_arg_num;
let _ =
match e with
- | Failure "out_some" ->
+ | Option.IsNone ->
let finfos = find_Function_infos (destConst f) in
update_Function
{finfos with
@@ -1141,7 +1141,7 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams :
then
(* observe_tac ("h_fix") *) (h_fix (Some this_fix_info.name) (this_fix_info.idx +1))
else
- h_mutual_fix this_fix_info.name (this_fix_info.idx + 1)
+ h_mutual_fix false this_fix_info.name (this_fix_info.idx + 1)
other_fix_infos
| _ -> anomaly "Not a valid information"
in
@@ -1246,7 +1246,7 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams :
in
let fname = destConst (fst (decompose_app (List.hd (List.rev pte_args)))) in
tclTHENSEQ
- [unfold_in_concl [([],Names.EvalConstRef fname)];
+ [unfold_in_concl [(all_occurrences,Names.EvalConstRef fname)];
let do_prove =
build_proof
interactive_proof
@@ -1347,19 +1347,27 @@ let build_clause eqs =
{
Tacexpr.onhyps =
Some (List.map
- (fun id -> ([],id),Tacexpr.InHyp)
+ (fun id -> (Rawterm.all_occurrences_expr,id),Tacexpr.InHyp)
eqs
);
- Tacexpr.onconcl = false;
- Tacexpr.concl_occs = []
+ Tacexpr.concl_occs = Rawterm.no_occurrences_expr
}
let rec rewrite_eqs_in_eqs eqs =
match eqs with
| [] -> tclIDTAC
| eq::eqs ->
+
tclTHEN
- (tclMAP (fun id -> tclTRY (Equality.general_rewrite_in true id (mkVar eq))) eqs)
+ (tclMAP
+ (fun id gl ->
+ observe_tac
+ (Format.sprintf "rewrite %s in %s " (string_of_id eq) (string_of_id id))
+ (tclTRY (Equality.general_rewrite_in true all_occurrences id (mkVar eq) false))
+ gl
+ )
+ eqs
+ )
(rewrite_eqs_in_eqs eqs)
let new_prove_with_tcc is_mes acc_inv hrec tcc_hyps eqs : tactic =
@@ -1373,21 +1381,26 @@ let new_prove_with_tcc is_mes acc_inv hrec tcc_hyps eqs : tactic =
[ tclTHENSEQ
[
keep (tcc_hyps@eqs);
-
apply (Lazy.force acc_inv);
(fun g ->
if is_mes
then
- unfold_in_concl [([], evaluable_of_global_reference (delayed_force ltof_ref))] g
+ unfold_in_concl [(all_occurrences, evaluable_of_global_reference (delayed_force ltof_ref))] g
else tclIDTAC g
);
observe_tac "rew_and_finish"
(tclTHENLIST
[tclTRY(Recdef.list_rewrite false (List.map mkVar eqs));
- rewrite_eqs_in_eqs eqs;
- (observe_tac "finishing"
- (tclCOMPLETE (
- Eauto.gen_eauto false (false,5) [] (Some []))
+ observe_tac "rewrite_eqs_in_eqs" (rewrite_eqs_in_eqs eqs);
+ (observe_tac "finishing using"
+ (
+ tclCOMPLETE(
+ Eauto.eauto_with_bases
+ false
+ (true,5)
+ [Lazy.force refl_equal]
+ [empty_transparent_state, Auto.Hint_db.empty]
+ )
)
)
]
@@ -1445,7 +1458,7 @@ let prove_principle_for_gen
let wf_tac =
if is_mes
then
- (fun b -> Recdef.tclUSER_if_not_mes b None)
+ (fun b -> Recdef.tclUSER_if_not_mes tclIDTAC b None)
else fun _ -> prove_with_tcc tcc_lemma_ref []
in
let real_rec_arg_num = rec_arg_num - princ_info.nparams in
@@ -1502,16 +1515,16 @@ let prove_principle_for_gen
| None -> anomaly ( "No tcc proof !!")
| Some lemma -> lemma
in
- let rec list_diff del_list check_list =
- match del_list with
- [] ->
- []
- | f::r ->
- if List.mem f check_list then
- list_diff r check_list
- else
- f::(list_diff r check_list)
- in
+(* let rec list_diff del_list check_list = *)
+(* match del_list with *)
+(* [] -> *)
+(* [] *)
+(* | f::r -> *)
+(* if List.mem f check_list then *)
+(* list_diff r check_list *)
+(* else *)
+(* f::(list_diff r check_list) *)
+(* in *)
let tcc_list = ref [] in
let start_tac gls =
let hyps = pf_ids_of_hyps gls in
@@ -1527,7 +1540,7 @@ let prove_principle_for_gen
Elim.h_decompose_and (mkVar hid);
(fun g ->
let new_hyps = pf_ids_of_hyps g in
- tcc_list := list_diff new_hyps (hid::hyps);
+ tcc_list := List.rev (list_subtract new_hyps (hid::hyps));
if !tcc_list = []
then
begin
@@ -1593,14 +1606,15 @@ let prove_principle_for_gen
(* msgnl (str "eqs := "++ prlist_with_sep spc Ppconstr.pr_id eqs); *)
(* observe_tac "new_prove_with_tcc" *)
- (new_prove_with_tcc
+ (new_prove_with_tcc
is_mes acc_inv fix_id
- !tcc_list
- ((List.map
+
+ (!tcc_list@(List.map
(fun (na,_,_) -> (Nameops.out_name na))
(princ_info.args@princ_info.params)
- )@ (acc_rec_arg_id::eqs))
+ )@ ([acc_rec_arg_id])) eqs
)
+
);
is_valid = is_valid_hypothesis predicates_names
}
diff --git a/contrib/funind/functional_principles_types.ml b/contrib/funind/functional_principles_types.ml
index 8ad2e72b..16076479 100644
--- a/contrib/funind/functional_principles_types.ml
+++ b/contrib/funind/functional_principles_types.ml
@@ -115,7 +115,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
it_mkProd_or_LetIn
~init:
(it_mkProd_or_LetIn
- ~init:(option_fold_right
+ ~init:(Option.fold_right
mkProd_or_LetIn
princ_type_info.indarg
princ_type_info.concl
@@ -384,7 +384,7 @@ let generate_functional_principle
{ const_entry_body = value;
const_entry_type = None;
const_entry_opaque = false;
- const_entry_boxed = Options.boxed_definitions()
+ const_entry_boxed = Flags.boxed_definitions()
}
in
ignore(
@@ -394,7 +394,7 @@ let generate_functional_principle
Decl_kinds.IsDefinition (Decl_kinds.Scheme)
)
);
- Options.if_verbose
+ Flags.if_verbose
(fun id -> Pp.msgnl (Ppconstr.pr_id id ++ str " is defined"))
name;
names := name :: !names
@@ -561,6 +561,15 @@ let make_scheme (fas : (constant*Rawterm.rawsort) list) : Entries.definition_ent
(fun _ _ _ -> ())
in
incr i;
+ let opacity =
+ let finfos = find_Function_infos this_block_funs.(0) in
+ try
+ let equation = Option.get finfos.equation_lemma in
+ (Global.lookup_constant equation).Declarations.const_opaque
+ with Option.IsNone -> (* non recursive definition *)
+ false
+ in
+ let const = {const with const_entry_opaque = opacity } in
(* The others are just deduced *)
if other_princ_types = []
then
@@ -642,10 +651,12 @@ let build_scheme fas =
in
List.iter2
(fun (princ_id,_,_) def_entry ->
- ignore (Declare.declare_constant
- princ_id
- (Entries.DefinitionEntry def_entry,Decl_kinds.IsProof Decl_kinds.Theorem));
- Options.if_verbose (fun id -> Pp.msgnl (Ppconstr.pr_id id ++ str " is defined")) princ_id
+ ignore
+ (Declare.declare_constant
+ princ_id
+ (Entries.DefinitionEntry def_entry,Decl_kinds.IsProof Decl_kinds.Theorem));
+ Flags.if_verbose
+ (fun id -> Pp.msgnl (Ppconstr.pr_id id ++ str " is defined")) princ_id
)
fas
bodies_types
diff --git a/contrib/funind/indfun_main.ml4 b/contrib/funind/g_indfun.ml4
index 9cee9edc..dae76f2d 100644
--- a/contrib/funind/indfun_main.ml4
+++ b/contrib/funind/g_indfun.ml4
@@ -29,20 +29,37 @@ let pr_bindings prc prlc = function
Util.prlist_with_sep spc (fun b -> str"(" ++ pr_binding prlc b ++ str")") l
| Rawterm.NoBindings -> mt ()
-
let pr_with_bindings prc prlc (c,bl) =
prc c ++ hv 0 (pr_bindings prc prlc bl)
-
let pr_fun_ind_using prc prlc _ opt_c =
match opt_c with
| None -> mt ()
| Some (p,b) -> spc () ++ hov 2 (str "using" ++ spc () ++ pr_with_bindings prc prlc (p,b))
+(* Duplication of printing functions because "'a with_bindings" is
+ (internally) not uniform in 'a: indeed constr_with_bindings at the
+ "typed" level has type "open_constr with_bindings" instead of
+ "constr with_bindings"; hence, its printer cannot be polymorphic in
+ (prc,prlc)... *)
+
+let pr_with_bindings_typed prc prlc (c,bl) =
+ prc c ++
+ hv 0 (pr_bindings (fun c -> prc (snd c)) (fun c -> prlc (snd c)) bl)
+
+let pr_fun_ind_using_typed prc prlc _ opt_c =
+ match opt_c with
+ | None -> mt ()
+ | Some (p,b) -> spc () ++ hov 2 (str "using" ++ spc () ++ pr_with_bindings_typed prc prlc (p,b))
+
ARGUMENT EXTEND fun_ind_using
TYPED AS constr_with_bindings_opt
- PRINTED BY pr_fun_ind_using
+ PRINTED BY pr_fun_ind_using_typed
+ RAW_TYPED AS constr_with_bindings_opt
+ RAW_PRINTED BY pr_fun_ind_using
+ GLOB_TYPED AS constr_with_bindings_opt
+ GLOB_PRINTED BY pr_fun_ind_using
| [ "using" constr_with_bindings(c) ] -> [ Some c ]
| [ ] -> [ None ]
END
@@ -131,7 +148,7 @@ END
VERNAC ARGUMENT EXTEND binder2
[ "(" ne_ident_list(idl) ":" lconstr(c) ")"] ->
[
- LocalRawAssum (List.map (fun id -> (Util.dummy_loc,Name id)) idl,c) ]
+ LocalRawAssum (List.map (fun id -> (Util.dummy_loc,Name id)) idl,Topconstr.default_binder_kind,c) ]
END
@@ -152,7 +169,7 @@ VERNAC ARGUMENT EXTEND rec_definition2
| Struct id -> id | Wf(_,Some id,_) -> id | Mes(_,Some id,_) -> id
| Wf(_,None,_) | Mes(_,None,_) -> failwith "check_exists_args"
in
- (try ignore(Util.list_index (Name id) names - 1); annot
+ (try ignore(Util.list_index0 (Name id) names); annot
with Not_found -> Util.user_err_loc
(Util.dummy_loc,"Function",
Pp.str "No argument named " ++ Nameops.pr_id id)
@@ -166,7 +183,7 @@ VERNAC ARGUMENT EXTEND rec_definition2
| Some an ->
check_exists_args an
in
- (id, ni, bl, type_, def) ]
+ ((Util.dummy_loc,id), ni, bl, type_, def) ]
END
@@ -300,7 +317,7 @@ let mkEq typ c1 c2 =
let poseq_unsafe idunsafe cstr gl =
let typ = Tacmach.pf_type_of gl cstr in
tclTHEN
- (Tactics.letin_tac true (Name idunsafe) cstr allClauses)
+ (Tactics.letin_tac None (Name idunsafe) cstr allClauses)
(tclTHENFIRST
(Tactics.assert_as true IntroAnonymous (mkEq typ (mkVar idunsafe) cstr))
Tactics.reflexivity)
@@ -446,25 +463,23 @@ VERNAC COMMAND EXTEND Showindinfo
END
VERNAC COMMAND EXTEND MergeFunind
- [ "Mergeschemes" lconstr(c) "with" lconstr(c') "using" ident(id) ] ->
+ [ "Mergeschemes" "(" ident(id1) ne_ident_list(cl1) ")"
+ "with" "(" ident(id2) ne_ident_list(cl2) ")" "using" ident(id) ] ->
[
- let c1 = Constrintern.interp_constr Evd.empty (Global.env()) c in
- let c2 = Constrintern.interp_constr Evd.empty (Global.env()) c' in
- let id1,args1 =
- try
- let hd,args = destApp c1 in
- if Term.isInd hd then hd , args
- else raise (Util.error "Ill-formed (fst) argument")
- with Invalid_argument _
- -> Util.error ("Bad argument form for merging schemes") in
- let id2,args2 =
- try
- let hd,args = destApp c2 in
- if isInd hd then hd , args
- else raise (Util.error "Ill-formed (snd) argument")
- with Invalid_argument _
- -> Util.error ("Bad argument form for merging schemes") in
- (* TOFO: enlever le ignore et declarer l'inductif *)
- ignore(Merge.merge c1 c2 args1 args2 id)
+ let f1 = Constrintern.interp_constr Evd.empty (Global.env())
+ (CRef (Libnames.Ident (Util.dummy_loc,id1))) in
+ let f2 = Constrintern.interp_constr Evd.empty (Global.env())
+ (CRef (Libnames.Ident (Util.dummy_loc,id2))) in
+ let f1type = Typing.type_of (Global.env()) Evd.empty f1 in
+ let f2type = Typing.type_of (Global.env()) Evd.empty f2 in
+ let ar1 = List.length (fst (decompose_prod f1type)) in
+ let ar2 = List.length (fst (decompose_prod f2type)) in
+ let _ =
+ if ar1 <> List.length cl1 then
+ Util.error ("not the right number of arguments for " ^ string_of_id id1) in
+ let _ =
+ if ar2 <> List.length cl2 then
+ Util.error ("not the right number of arguments for " ^ string_of_id id2) in
+ Merge.merge id1 id2 (Array.of_list cl1) (Array.of_list cl2) id
]
END
diff --git a/contrib/funind/indfun.ml b/contrib/funind/indfun.ml
index 82bee01f..a6cbb321 100644
--- a/contrib/funind/indfun.ml
+++ b/contrib/funind/indfun.ml
@@ -22,8 +22,8 @@ let is_rec_info scheme_info =
let choose_dest_or_ind scheme_info =
if is_rec_info scheme_info
- then Tactics.new_induct
- else Tactics.new_destruct
+ then Tactics.new_induct false
+ else Tactics.new_destruct false
let functional_induction with_clean c princl pat =
@@ -48,8 +48,8 @@ let functional_induction with_clean c princl pat =
| InType -> finfo.rect_lemma
in
let princ = (* then we get the principle *)
- try mkConst (out_some princ_option )
- with Failure "out_some" ->
+ try mkConst (Option.get princ_option )
+ with Option.IsNone ->
(*i If there is not default lemma defined then,
we cross our finger and try to find a lemma named f_ind
(or f_rec, f_rect) i*)
@@ -77,7 +77,7 @@ let functional_induction with_clean c princl pat =
if princ_infos.Tactics.farg_in_concl
then [c] else []
in
- List.map (fun c -> Tacexpr.ElimOnConstr c) (args@c_list)
+ List.map (fun c -> Tacexpr.ElimOnConstr (c,NoBindings)) (args@c_list)
in
let princ' = Some (princ,bindings) in
let princ_vars =
@@ -120,7 +120,8 @@ let functional_induction with_clean c princl pat =
princ_infos
args_as_induction_constr
princ'
- pat)
+ pat
+ None)
subst_and_reduce
g
@@ -139,14 +140,14 @@ type newfixpoint_expr =
let rec abstract_rawconstr c = function
| [] -> c
| Topconstr.LocalRawDef (x,b)::bl -> Topconstr.mkLetInC(x,b,abstract_rawconstr c bl)
- | Topconstr.LocalRawAssum (idl,t)::bl ->
- List.fold_right (fun x b -> Topconstr.mkLambdaC([x],t,b)) idl
+ | Topconstr.LocalRawAssum (idl,k,t)::bl ->
+ List.fold_right (fun x b -> Topconstr.mkLambdaC([x],k,t,b)) idl
(abstract_rawconstr c bl)
let interp_casted_constr_with_implicits sigma env impls c =
(* Constrintern.interp_rawconstr_with_implicits sigma env [] impls c *)
Constrintern.intern_gen false sigma env ~impls:([],impls)
- ~allow_soapp:false ~ltacvars:([],[]) c
+ ~allow_patvar:false ~ltacvars:([],[]) c
(*
@@ -160,7 +161,7 @@ let build_newrecursive
in
let (rec_sign,rec_impls) =
List.fold_left
- (fun (env,impls) (recname,_,bl,arityc,_) ->
+ (fun (env,impls) ((_,recname),_,bl,arityc,_) ->
let arityc = Command.generalize_constr_expr arityc bl in
let arity = Constrintern.interp_type sigma env0 arityc in
let impl =
@@ -213,7 +214,7 @@ let rec is_rec names =
| RRec _ -> error "RRec not handled"
| RIf(_,b,_,lhs,rhs) ->
(lookup names b) || (lookup names lhs) || (lookup names rhs)
- | RLetIn(_,na,t,b) | RLambda(_,na,t,b) | RProd(_,na,t,b) ->
+ | RLetIn(_,na,t,b) | RLambda(_,na,_,t,b) | RProd(_,na,_,t,b) ->
lookup names t || lookup (Nameops.name_fold Idset.remove na names) b
| RLetTuple(_,nal,_,t,b) -> lookup names t ||
lookup
@@ -224,7 +225,7 @@ let rec is_rec names =
)
b
| RApp(_,f,args) -> List.exists (lookup names) (f::args)
- | RCases(_,_,el,brl) ->
+ | RCases(_,_,_,el,brl) ->
List.exists (fun (e,_) -> lookup names e) el ||
List.exists (lookup_br names) brl
and lookup_br names (_,idl,_,rt) =
@@ -266,7 +267,7 @@ let derive_inversion fix_names =
)
with e ->
msg_warning
- (str "Cannot build functional inversion principle" ++
+ (str "Cannot built inversion information" ++
if do_observe () then Cerrors.explain_exn e else mt ())
with _ -> ()
@@ -297,7 +298,7 @@ let generate_principle on_error
is_general do_built fix_rec_l recdefs interactive_proof
(continue_proof : int -> Names.constant array -> Term.constr array -> int ->
Tacmach.tactic) : unit =
- let names = List.map (function (name,_,_,_,_) -> name) fix_rec_l in
+ let names = List.map (function ((_, name),_,_,_,_) -> name) fix_rec_l in
let fun_bodies = List.map2 prepare_body fix_rec_l recdefs in
let funs_args = List.map fst fun_bodies in
let funs_types = List.map (function (_,_,_,types,_) -> types) fix_rec_l in
@@ -318,7 +319,7 @@ let generate_principle on_error
f_R_mut)
in
let fname_kn (fname,_,_,_,_) =
- let f_ref = Ident (dummy_loc,fname) in
+ let f_ref = Ident fname in
locate_with_msg
(pr_reference f_ref++str ": Not an inductive type!")
locate_constant
@@ -351,17 +352,17 @@ let generate_principle on_error
let register_struct is_rec fixpoint_exprl =
match fixpoint_exprl with
- | [(fname,_,bl,ret_type,body),_] when not is_rec ->
+ | [((_,fname),_,bl,ret_type,body),_] when not is_rec ->
Command.declare_definition
fname
- (Decl_kinds.Global,Options.boxed_definitions (),Decl_kinds.Definition)
+ (Decl_kinds.Global,Flags.boxed_definitions (),Decl_kinds.Definition)
bl
None
body
(Some ret_type)
(fun _ _ -> ())
| _ ->
- Command.build_recursive fixpoint_exprl (Options.boxed_definitions())
+ Command.build_recursive fixpoint_exprl (Flags.boxed_definitions())
let generate_correction_proof_wf f_ref tcc_lemma_ref
is_mes functional_ref eq_ref rec_arg_num rec_arg_type nb_args relation
@@ -402,7 +403,7 @@ let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas
)
)
in
- Topconstr.CApp (dummy_loc,(None,Topconstr.mkIdentC (id_of_string "eq")),
+ Topconstr.CApp (dummy_loc,(None,Topconstr.mkRefC (Qualid (dummy_loc,(qualid_of_string "Logic.eq")))),
[(f_app_args,None);(body,None)])
in
let eq = Command.generalize_constr_expr unbounded_eq args in
@@ -434,7 +435,7 @@ let register_mes fname rec_impls wf_mes_expr wf_arg using_lemmas args ret_type b
| None ->
begin
match args with
- | [Topconstr.LocalRawAssum ([(_,Name x)],t)] -> t,x
+ | [Topconstr.LocalRawAssum ([(_,Name x)],k,t)] -> t,x
| _ -> error "Recursive argument must be specified"
end
| Some wf_args ->
@@ -442,7 +443,7 @@ let register_mes fname rec_impls wf_mes_expr wf_arg using_lemmas args ret_type b
match
List.find
(function
- | Topconstr.LocalRawAssum(l,t) ->
+ | Topconstr.LocalRawAssum(l,k,t) ->
List.exists
(function (_,Name id) -> id = wf_args | _ -> false)
l
@@ -450,7 +451,7 @@ let register_mes fname rec_impls wf_mes_expr wf_arg using_lemmas args ret_type b
)
args
with
- | Topconstr.LocalRawAssum(_,t) -> t,wf_args
+ | Topconstr.LocalRawAssum(_,k,t) -> t,wf_args
| _ -> assert false
with Not_found -> assert false
in
@@ -462,7 +463,7 @@ let register_mes fname rec_impls wf_mes_expr wf_arg using_lemmas args ret_type b
let fun_from_mes =
let applied_mes =
Topconstr.mkAppC(wf_mes_expr,[Topconstr.mkIdentC wf_arg]) in
- Topconstr.mkLambdaC ([(dummy_loc,Name wf_arg)],wf_arg_type,applied_mes)
+ Topconstr.mkLambdaC ([(dummy_loc,Name wf_arg)],Topconstr.default_binder_kind,wf_arg_type,applied_mes)
in
let wf_rel_from_mes =
Topconstr.mkAppC(Topconstr.mkRefC ltof,[wf_arg_type;fun_from_mes])
@@ -475,7 +476,7 @@ let do_generate_principle on_error register_built interactive_proof fixpoint_exp
let recdefs,rec_impls = build_newrecursive fixpoint_exprl in
let _is_struct =
match fixpoint_exprl with
- | [((name,Some (Wf (wf_rel,wf_x,using_lemmas)),args,types,body))] ->
+ | [(((_,name),Some (Wf (wf_rel,wf_x,using_lemmas)),args,types,body))] ->
let pre_hook =
generate_principle
on_error
@@ -488,7 +489,7 @@ let do_generate_principle on_error register_built interactive_proof fixpoint_exp
if register_built
then register_wf name rec_impls wf_rel wf_x using_lemmas args types body pre_hook;
false
- | [((name,Some (Mes (wf_mes,wf_x,using_lemmas)),args,types,body))] ->
+ | [(((_,name),Some (Mes (wf_mes,wf_x,using_lemmas)),args,types,body))] ->
let pre_hook =
generate_principle
on_error
@@ -503,20 +504,15 @@ let do_generate_principle on_error register_built interactive_proof fixpoint_exp
true
| _ ->
let fix_names =
- List.map (function (name,_,_,_,_) -> name) fixpoint_exprl
+ List.map (function ((_,name),_,_,_,_) -> name) fixpoint_exprl
in
let is_one_rec = is_rec fix_names in
let old_fixpoint_exprl =
List.map
(function
| (name,Some (Struct id),args,types,body),_ ->
- let names =
- List.map
- snd
- (Topconstr.names_of_local_assums args)
- in
let annot =
- try Some (list_index (Name id) names - 1), Topconstr.CStructRec
+ try Some (dummy_loc, id), Topconstr.CStructRec
with Not_found ->
raise (UserError("",str "Cannot find argument " ++
Ppconstr.pr_id id))
@@ -529,7 +525,8 @@ let do_generate_principle on_error register_built interactive_proof fixpoint_exp
(dummy_loc,"Function",
Pp.str "the recursive argument needs to be specified in Function")
else
- (name,(Some 0, Topconstr.CStructRec),args,types,body),
+ let loc, na = List.hd names in
+ (name,(Some (loc, Nameops.out_name na), Topconstr.CStructRec),args,types,body),
(None:Vernacexpr.decl_notation)
| (_,Some (Wf _),_,_,_),_ | (_,Some (Mes _),_,_,_),_->
error
@@ -539,7 +536,7 @@ let do_generate_principle on_error register_built interactive_proof fixpoint_exp
in
(* ok all the expressions are structural *)
let fix_names =
- List.map (function (name,_,_,_,_) -> name) fixpoint_exprl
+ List.map (function ((_,name),_,_,_,_) -> name) fixpoint_exprl
in
let is_rec = List.exists (is_rec fix_names) recdefs in
if register_built then register_struct is_rec old_fixpoint_exprl;
@@ -570,11 +567,11 @@ let rec add_args id new_args b =
CArrow(loc,add_args id new_args b1, add_args id new_args b2)
| CProdN(loc,nal,b1) ->
CProdN(loc,
- List.map (fun (nal,b2) -> (nal,add_args id new_args b2)) nal,
+ List.map (fun (nal,k,b2) -> (nal,k,add_args id new_args b2)) nal,
add_args id new_args b1)
| CLambdaN(loc,nal,b1) ->
CLambdaN(loc,
- List.map (fun (nal,b2) -> (nal,add_args id new_args b2)) nal,
+ List.map (fun (nal,k,b2) -> (nal,k,add_args id new_args b2)) nal,
add_args id new_args b1)
| CLetIn(loc,na,b1,b2) ->
CLetIn(loc,na,add_args id new_args b1,add_args id new_args b2)
@@ -588,22 +585,22 @@ let rec add_args id new_args b =
| CApp(loc,(pf,b),bl) ->
CApp(loc,(pf,add_args id new_args b),
List.map (fun (e,o) -> add_args id new_args e,o) bl)
- | CCases(loc,b_option,cel,cal) ->
- CCases(loc,option_map (add_args id new_args) b_option,
+ | CCases(loc,sty,b_option,cel,cal) ->
+ CCases(loc,sty,Option.map (add_args id new_args) b_option,
List.map (fun (b,(na,b_option)) ->
add_args id new_args b,
- (na,option_map (add_args id new_args) b_option)) cel,
+ (na,Option.map (add_args id new_args) b_option)) cel,
List.map (fun (loc,cpl,e) -> (loc,cpl,add_args id new_args e)) cal
)
| CLetTuple(loc,nal,(na,b_option),b1,b2) ->
- CLetTuple(loc,nal,(na,option_map (add_args id new_args) b_option),
+ CLetTuple(loc,nal,(na,Option.map (add_args id new_args) b_option),
add_args id new_args b1,
add_args id new_args b2
)
| CIf(loc,b1,(na,b_option),b2,b3) ->
CIf(loc,add_args id new_args b1,
- (na,option_map (add_args id new_args) b_option),
+ (na,Option.map (add_args id new_args) b_option),
add_args id new_args b2,
add_args id new_args b3
)
@@ -644,13 +641,15 @@ let rec chop_n_arrow n t =
let new_n =
let rec aux (n:int) = function
[] -> n
- | (nal,t'')::nal_ta' ->
+ | (nal,k,t'')::nal_ta' ->
let nal_l = List.length nal in
if n >= nal_l
then
aux (n - nal_l) nal_ta'
else
- let new_t' = Topconstr.CProdN(dummy_loc,((snd (list_chop n nal)),t'')::nal_ta',t')
+ let new_t' =
+ Topconstr.CProdN(dummy_loc,
+ ((snd (list_chop n nal)),k,t'')::nal_ta',t')
in
raise (Stop new_t')
in
@@ -668,12 +667,12 @@ let rec get_args b t : Topconstr.local_binder list *
| Topconstr.CLambdaN (loc, (nal_ta), b') ->
begin
let n =
- (List.fold_left (fun n (nal,_) ->
+ (List.fold_left (fun n (nal,_,_) ->
n+List.length nal) 0 nal_ta )
in
let nal_tas,b'',t'' = get_args b' (chop_n_arrow n t) in
- (List.map (fun (nal,ta) ->
- (Topconstr.LocalRawAssum (nal,ta))) nal_ta)@nal_tas, b'',t''
+ (List.map (fun (nal,k,ta) ->
+ (Topconstr.LocalRawAssum (nal,k,ta))) nal_ta)@nal_tas, b'',t''
end
| _ -> [],b,t
@@ -711,26 +710,13 @@ let make_graph (f_ref:global_reference) =
let l =
List.map
(fun (id,(n,recexp),bl,t,b) ->
- let bl' =
- List.flatten
- (List.map
- (function
- | Topconstr.LocalRawDef (na,_)-> []
- | Topconstr.LocalRawAssum (nal,_) -> nal
- )
- bl
- )
- in
- let rec_id =
- match List.nth bl' (out_some n) with
- |(_,Name id) -> id | _ -> anomaly ""
- in
+ let loc, rec_id = Option.get n in
let new_args =
List.flatten
(List.map
(function
| Topconstr.LocalRawDef (na,_)-> []
- | Topconstr.LocalRawAssum (nal,_) ->
+ | Topconstr.LocalRawAssum (nal,_,_) ->
List.map
(fun (loc,n) ->
CRef(Libnames.Ident(loc, Nameops.out_name n)))
@@ -739,7 +725,7 @@ let make_graph (f_ref:global_reference) =
nal_tas
)
in
- let b' = add_args id new_args b in
+ let b' = add_args (snd id) new_args b in
(id, Some (Struct rec_id),nal_tas@bl,t,b')
)
fixexprl
@@ -747,13 +733,13 @@ let make_graph (f_ref:global_reference) =
l
| _ ->
let id = id_of_label (con_label c) in
- [(id,None,nal_tas,t,b)]
+ [((dummy_loc,id),None,nal_tas,t,b)]
in
do_generate_principle error_error false false expr_list;
(* We register the infos *)
let mp,dp,_ = repr_con c in
List.iter
- (fun (id,_,_,_,_) -> add_Function false (make_con mp dp (label_of_id id)))
+ (fun ((_,id),_,_,_,_) -> add_Function false (make_con mp dp (label_of_id id)))
expr_list
diff --git a/contrib/funind/indfun_common.ml b/contrib/funind/indfun_common.ml
index 13b242d5..4010b49d 100644
--- a/contrib/funind/indfun_common.ml
+++ b/contrib/funind/indfun_common.ml
@@ -76,7 +76,7 @@ let chop_rlambda_n =
then List.rev acc,rt
else
match rt with
- | Rawterm.RLambda(_,name,t,b) -> chop_lambda_n ((name,t,false)::acc) (n-1) b
+ | Rawterm.RLambda(_,name,k,t,b) -> chop_lambda_n ((name,t,false)::acc) (n-1) b
| Rawterm.RLetIn(_,name,v,b) -> chop_lambda_n ((name,v,true)::acc) (n-1) b
| _ ->
raise (Util.UserError("chop_rlambda_n",
@@ -90,7 +90,7 @@ let chop_rprod_n =
then List.rev acc,rt
else
match rt with
- | Rawterm.RProd(_,name,t,b) -> chop_prod_n ((name,t)::acc) (n-1) b
+ | Rawterm.RProd(_,name,k,t,b) -> chop_prod_n ((name,t)::acc) (n-1) b
| _ -> raise (Util.UserError("chop_rprod_n",str "chop_rprod_n: Not enough products"))
in
chop_prod_n []
@@ -131,7 +131,7 @@ let coq_constant s =
(Coqlib.init_modules @ Coqlib.arith_modules) s;;
let constant sl s =
- constr_of_reference
+ constr_of_global
(Nametab.locate (make_qualid(Names.make_dirpath
(List.map id_of_string (List.rev sl)))
(id_of_string s)));;
@@ -153,7 +153,7 @@ open Entries
open Decl_kinds
open Declare
let definition_message id =
- Options.if_verbose message ((string_of_id id) ^ " is defined")
+ Flags.if_verbose message ((string_of_id id) ^ " is defined")
let save with_clean id const (locality,kind) hook =
@@ -237,24 +237,29 @@ let with_full_print f a =
let old_implicit_args = Impargs.is_implicit_args ()
and old_strict_implicit_args = Impargs.is_strict_implicit_args ()
and old_contextual_implicit_args = Impargs.is_contextual_implicit_args () in
- let old_rawprint = !Options.raw_print in
- Options.raw_print := true;
+ let old_rawprint = !Flags.raw_print in
+ let old_dump = !Flags.dump in
+ Flags.raw_print := true;
Impargs.make_implicit_args false;
Impargs.make_strict_implicit_args false;
Impargs.make_contextual_implicit_args false;
+ Impargs.make_contextual_implicit_args false;
+ Flags.dump := false;
try
let res = f a in
Impargs.make_implicit_args old_implicit_args;
Impargs.make_strict_implicit_args old_strict_implicit_args;
Impargs.make_contextual_implicit_args old_contextual_implicit_args;
- Options.raw_print := old_rawprint;
+ Flags.raw_print := old_rawprint;
+ Flags.dump := old_dump;
res
with
| e ->
Impargs.make_implicit_args old_implicit_args;
Impargs.make_strict_implicit_args old_strict_implicit_args;
Impargs.make_contextual_implicit_args old_contextual_implicit_args;
- Options.raw_print := old_rawprint;
+ Flags.raw_print := old_rawprint;
+ Flags.dump := old_dump;
raise e
@@ -319,12 +324,12 @@ let subst_Function (_,subst,finfos) =
in
let function_constant' = do_subst_con finfos.function_constant in
let graph_ind' = do_subst_ind finfos.graph_ind in
- let equation_lemma' = Util.option_smartmap do_subst_con finfos.equation_lemma in
- let correctness_lemma' = Util.option_smartmap do_subst_con finfos.correctness_lemma in
- let completeness_lemma' = Util.option_smartmap do_subst_con finfos.completeness_lemma in
- let rect_lemma' = Util.option_smartmap do_subst_con finfos.rect_lemma in
- let rec_lemma' = Util.option_smartmap do_subst_con finfos.rec_lemma in
- let prop_lemma' = Util.option_smartmap do_subst_con finfos.prop_lemma in
+ let equation_lemma' = Option.smartmap do_subst_con finfos.equation_lemma in
+ let correctness_lemma' = Option.smartmap do_subst_con finfos.correctness_lemma in
+ let completeness_lemma' = Option.smartmap do_subst_con finfos.completeness_lemma in
+ let rect_lemma' = Option.smartmap do_subst_con finfos.rect_lemma in
+ let rec_lemma' = Option.smartmap do_subst_con finfos.rec_lemma in
+ let prop_lemma' = Option.smartmap do_subst_con finfos.prop_lemma in
if function_constant' == finfos.function_constant &&
graph_ind' == finfos.graph_ind &&
equation_lemma' == finfos.equation_lemma &&
@@ -354,12 +359,12 @@ let export_Function infos = Some infos
let discharge_Function (_,finfos) =
let function_constant' = Lib.discharge_con finfos.function_constant
and graph_ind' = Lib.discharge_inductive finfos.graph_ind
- and equation_lemma' = Util.option_smartmap Lib.discharge_con finfos.equation_lemma
- and correctness_lemma' = Util.option_smartmap Lib.discharge_con finfos.correctness_lemma
- and completeness_lemma' = Util.option_smartmap Lib.discharge_con finfos.completeness_lemma
- and rect_lemma' = Util.option_smartmap Lib.discharge_con finfos.rect_lemma
- and rec_lemma' = Util.option_smartmap Lib.discharge_con finfos.rec_lemma
- and prop_lemma' = Util.option_smartmap Lib.discharge_con finfos.prop_lemma
+ and equation_lemma' = Option.smartmap Lib.discharge_con finfos.equation_lemma
+ and correctness_lemma' = Option.smartmap Lib.discharge_con finfos.correctness_lemma
+ and completeness_lemma' = Option.smartmap Lib.discharge_con finfos.completeness_lemma
+ and rect_lemma' = Option.smartmap Lib.discharge_con finfos.rect_lemma
+ and rec_lemma' = Option.smartmap Lib.discharge_con finfos.rec_lemma
+ and prop_lemma' = Option.smartmap Lib.discharge_con finfos.prop_lemma
in
if function_constant' == finfos.function_constant &&
graph_ind' == finfos.graph_ind &&
@@ -387,12 +392,12 @@ let pr_info f_info =
str "function_constant := " ++ Printer.pr_lconstr (mkConst f_info.function_constant)++ fnl () ++
str "function_constant_type := " ++
(try Printer.pr_lconstr (Global.type_of_global (ConstRef f_info.function_constant)) with _ -> mt ()) ++ fnl () ++
- str "equation_lemma := " ++ (Util.option_fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) f_info.equation_lemma (mt ()) ) ++ fnl () ++
- str "completeness_lemma :=" ++ (Util.option_fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) f_info.completeness_lemma (mt ()) ) ++ fnl () ++
- str "correctness_lemma := " ++ (Util.option_fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) f_info.correctness_lemma (mt ()) ) ++ fnl () ++
- str "rect_lemma := " ++ (Util.option_fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) f_info.rect_lemma (mt ()) ) ++ fnl () ++
- str "rec_lemma := " ++ (Util.option_fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) f_info.rec_lemma (mt ()) ) ++ fnl () ++
- str "prop_lemma := " ++ (Util.option_fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) f_info.prop_lemma (mt ()) ) ++ fnl () ++
+ str "equation_lemma := " ++ (Option.fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) f_info.equation_lemma (mt ()) ) ++ fnl () ++
+ str "completeness_lemma :=" ++ (Option.fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) f_info.completeness_lemma (mt ()) ) ++ fnl () ++
+ str "correctness_lemma := " ++ (Option.fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) f_info.correctness_lemma (mt ()) ) ++ fnl () ++
+ str "rect_lemma := " ++ (Option.fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) f_info.rect_lemma (mt ()) ) ++ fnl () ++
+ str "rec_lemma := " ++ (Option.fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) f_info.rec_lemma (mt ()) ) ++ fnl () ++
+ str "prop_lemma := " ++ (Option.fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) f_info.prop_lemma (mt ()) ) ++ fnl () ++
str "graph_ind := " ++ Printer.pr_lconstr (mkInd f_info.graph_ind) ++ fnl ()
let pr_table tb =
diff --git a/contrib/funind/invfun.ml b/contrib/funind/invfun.ml
index c7a3d164..63d44916 100644
--- a/contrib/funind/invfun.ml
+++ b/contrib/funind/invfun.ml
@@ -16,6 +16,7 @@ open Tacticals
open Tactics
open Indfun_common
open Tacmach
+open Termops
open Sign
open Hiddentac
@@ -23,13 +24,13 @@ open Hiddentac
let pr_binding prc =
function
- | loc, Rawterm.NamedHyp id, c -> hov 1 (Ppconstr.pr_id id ++ str " := " ++ Pp.cut () ++ prc c)
- | loc, Rawterm.AnonHyp n, c -> hov 1 (int n ++ str " := " ++ Pp.cut () ++ prc c)
+ | loc, Rawterm.NamedHyp id, (_,c) -> hov 1 (Ppconstr.pr_id id ++ str " := " ++ Pp.cut () ++ prc c)
+ | loc, Rawterm.AnonHyp n, (_,c) -> hov 1 (int n ++ str " := " ++ Pp.cut () ++ prc c)
let pr_bindings prc prlc = function
| Rawterm.ImplicitBindings l ->
brk (1,1) ++ str "with" ++ brk (1,1) ++
- Util.prlist_with_sep spc prc l
+ Util.prlist_with_sep spc (fun (_,c) -> prc c) l
| Rawterm.ExplicitBindings l ->
brk (1,1) ++ str "with" ++ brk (1,1) ++
Util.prlist_with_sep spc (fun b -> str"(" ++ pr_binding prlc b ++ str")") l
@@ -59,13 +60,13 @@ let observennl strm =
let do_observe_tac s tac g =
- try let goal = begin try (Printer.pr_goal (sig_it g)) with _ -> assert false end in
- let v = tac g in msgnl (goal ++ fnl () ++ s ++(str " ")++(str "finished")); v
- with e ->
- let goal = begin try (Printer.pr_goal (sig_it g)) with _ -> assert false end in
- msgnl (str "observation "++ s++str " raised exception " ++
- Cerrors.explain_exn e ++ str " on goal " ++ goal );
- raise e;;
+ let goal = begin try (Printer.pr_goal (sig_it g)) with _ -> assert false end in
+ try
+ let v = tac g in msgnl (goal ++ fnl () ++ s ++(str " ")++(str "finished")); v
+ with e ->
+ msgnl (str "observation "++ s++str " raised exception " ++
+ Cerrors.explain_exn e ++ str " on goal " ++ goal );
+ raise e;;
let observe_tac s tac g =
@@ -314,7 +315,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
| None -> (id::pre_args,pre_tac)
| Some b ->
(pre_args,
- tclTHEN (h_reduce (Rawterm.Unfold([[],EvalVarRef id])) allHyps) pre_tac
+ tclTHEN (h_reduce (Rawterm.Unfold([Rawterm.all_occurrences_expr,EvalVarRef id])) allHyps) pre_tac
)
else (pre_args,pre_tac)
@@ -425,7 +426,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
List.fold_left2
(fun (bindings,avoid) (x,_,_) p ->
let id = Nameops.next_ident_away (Nameops.out_name x) avoid in
- (dummy_loc,Rawterm.NamedHyp id,p)::bindings,id::avoid
+ (dummy_loc,Rawterm.NamedHyp id,inj_open p)::bindings,id::avoid
)
([],pf_ids_of_hyps g)
princ_infos.params
@@ -435,7 +436,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
List.rev (fst (List.fold_left2
(fun (bindings,avoid) (x,_,_) p ->
let id = Nameops.next_ident_away (Nameops.out_name x) avoid in
- (dummy_loc,Rawterm.NamedHyp id,nf_zeta p)::bindings,id::avoid)
+ (dummy_loc,Rawterm.NamedHyp id,inj_open (nf_zeta p))::bindings,id::avoid)
([],avoid)
princ_infos.predicates
(lemmas)))
@@ -461,14 +462,14 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
]
g
-(* [generalize_depedent_of x hyp g]
+(* [generalize_dependent_of x hyp g]
generalize every hypothesis which depends of [x] but [hyp]
*)
-let generalize_depedent_of x hyp g =
+let generalize_dependent_of x hyp g =
tclMAP
(function
| (id,None,t) when not (id = hyp) &&
- (Termops.occur_var (pf_env g) x t) -> h_generalize [mkVar id]
+ (Termops.occur_var (pf_env g) x t) -> tclTHEN (h_generalize [mkVar id]) (thin [id])
| _ -> tclIDTAC
)
(pf_hyps g)
@@ -490,12 +491,17 @@ and intros_with_rewrite_aux : tactic =
| Prod(_,t,t') ->
begin
match kind_of_term t with
- | App(eq,args) when (eq_constr eq eq_ind) ->
- if isVar args.(1)
+ | App(eq,args) when (eq_constr eq eq_ind) ->
+ if Reductionops.is_conv (pf_env g) (project g) args.(1) args.(2)
+ then
+ let id = pf_get_new_id (id_of_string "y") g in
+ tclTHENSEQ [ h_intro id; thin [id]; intros_with_rewrite ] g
+
+ else if isVar args.(1)
then
let id = pf_get_new_id (id_of_string "y") g in
tclTHENSEQ [ h_intro id;
- generalize_depedent_of (destVar args.(1)) id;
+ generalize_dependent_of (destVar args.(1)) id;
tclTRY (Equality.rewriteLR (mkVar id));
intros_with_rewrite
]
@@ -513,7 +519,7 @@ and intros_with_rewrite_aux : tactic =
Tauto.tauto g
| Case(_,_,v,_) ->
tclTHENSEQ[
- h_case (v,Rawterm.NoBindings);
+ h_case false (v,Rawterm.NoBindings);
intros_with_rewrite
] g
| LetIn _ ->
@@ -550,7 +556,7 @@ let rec reflexivity_with_destruct_cases g =
match kind_of_term (snd (destApp (pf_concl g))).(2) with
| Case(_,_,v,_) ->
tclTHENSEQ[
- h_case (v,Rawterm.NoBindings);
+ h_case false (v,Rawterm.NoBindings);
intros;
observe_tac "reflexivity_with_destruct_cases" reflexivity_with_destruct_cases
]
@@ -567,9 +573,9 @@ let rec reflexivity_with_destruct_cases g =
match kind_of_term (pf_type_of g (mkVar id)) with
| App(eq,[|_;t1;t2|]) when eq_constr eq eq_ind ->
if Equality.discriminable (pf_env g) (project g) t1 t2
- then Equality.discr id g
+ then Equality.discrHyp id g
else if Equality.injectable (pf_env g) (project g) t1 t2
- then tclTHENSEQ [Equality.inj [] id;thin [id];intros_with_rewrite] g
+ then tclTHENSEQ [Equality.injHyp id;thin [id];intros_with_rewrite] g
else tclIDTAC g
| _ -> tclIDTAC g
)
@@ -665,8 +671,8 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
if infos.is_general || Rtree.is_infinite graph_def.mind_recargs
then
let eq_lemma =
- try out_some (infos).equation_lemma
- with Failure "out_some" -> anomaly "Cannot find equation lemma"
+ try Option.get (infos).equation_lemma
+ with Option.IsNone -> anomaly "Cannot find equation lemma"
in
tclTHENSEQ[
tclMAP h_intro ids;
@@ -682,7 +688,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
h_generalize (List.map mkVar ids);
thin ids
]
- else unfold_in_concl [([],Names.EvalConstRef (destConst f))]
+ else unfold_in_concl [(all_occurrences,Names.EvalConstRef (destConst f))]
in
(* The proof of each branche itself *)
let ind_number = ref 0 in
@@ -706,7 +712,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
(* we expand the definition of the function *)
observe_tac "rewrite_tac" (rewrite_tac this_ind_number this_branche_ids);
(* introduce hypothesis with some rewrite *)
- (intros_with_rewrite);
+ observe_tac "intros_with_rewrite" intros_with_rewrite;
(* The proof is (almost) complete *)
observe_tac "reflexivity" (reflexivity_with_destruct_cases)
]
@@ -720,7 +726,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
(h_generalize [mkApp(applist(graph_principle,params),Array.map (fun c -> applist(c,params)) lemmas)]);
h_intro graph_principle_id;
observe_tac "" (tclTHEN_i
- (observe_tac "elim" ((elim (mkVar hres,Rawterm.NoBindings) (Some (mkVar graph_principle_id,Rawterm.NoBindings)))))
+ (observe_tac "elim" ((elim false (mkVar hres,Rawterm.NoBindings) (Some (mkVar graph_principle_id,Rawterm.NoBindings)))))
(fun i g -> observe_tac "prove_branche" (prove_branche i) g ))
]
g
@@ -769,7 +775,7 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g
Array.of_list
(List.map
(fun entry ->
- (entry.Entries.const_entry_body, out_some entry.Entries.const_entry_type )
+ (entry.Entries.const_entry_body, Option.get entry.Entries.const_entry_type )
)
(make_scheme (array_map_to_list (fun const -> const,Rawterm.RType None) funs))
)
@@ -960,13 +966,13 @@ let invfun qhyp f =
in
try
let finfos = find_Function_infos f in
- let f_correct = mkConst(out_some finfos.correctness_lemma)
+ let f_correct = mkConst(Option.get finfos.correctness_lemma)
and kn = fst finfos.graph_ind
in
Tactics.try_intros_until (fun hid -> functional_inversion kn hid (mkConst f) f_correct) qhyp
with
| Not_found -> error "No graph found"
- | Failure "out_some" -> error "Cannot use equivalence with graph!"
+ | Option.IsNone -> error "Cannot use equivalence with graph!"
let invfun qhyp f g =
@@ -983,23 +989,23 @@ let invfun qhyp f g =
try
if not (isConst f1) then failwith "";
let finfos = find_Function_infos (destConst f1) in
- let f_correct = mkConst(out_some finfos.correctness_lemma)
+ 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 "" | Failure "out_some" | Not_found ->
+ with | Failure "" | Option.IsNone | Not_found ->
try
let f2,_ = decompose_app args.(2) in
if not (isConst f2) then failwith "";
let finfos = find_Function_infos (destConst f2) in
- let f_correct = mkConst(out_some finfos.correctness_lemma)
+ 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 "" ->
errorlabstrm "" (str "Hypothesis" ++ Ppconstr.pr_id hid ++ str " must contain at leat one Function")
- | Failure "out_some" ->
+ | Option.IsNone ->
if do_observe ()
then
error "Cannot use equivalence with graph for any side of the equality"
diff --git a/contrib/funind/merge.ml b/contrib/funind/merge.ml
index 1b796a81..ec456aae 100644
--- a/contrib/funind/merge.ml
+++ b/contrib/funind/merge.ml
@@ -9,13 +9,16 @@
(* Merging of induction principles. *)
(*i $Id: i*)
-
+open Libnames
+open Tactics
+open Indfun_common
open Util
open Topconstr
open Vernacexpr
open Pp
open Names
open Term
+open Termops
open Declarations
open Environ
open Rawterm
@@ -25,6 +28,8 @@ open Rawtermops
(** {2 Useful operations on constr and rawconstr} *)
+let rec popn i c = if i<=0 then c else pop (popn (i-1) c)
+
(** Substitutions in constr *)
let compare_constr_nosub t1 t2 =
if compare_constr (fun _ _ -> false) t1 t2
@@ -110,6 +115,19 @@ let prNamedLDecl s lc =
List.iter (fun (nm,_,tp) -> prNamedConstr (string_of_name nm) tp) lc;
prstr "\n";
end
+let prNamedRLDecl s lc =
+ begin
+ prstr s; prstr "\n"; prstr "{§§ ";
+ List.iter
+ (fun x ->
+ match x with
+ | (nm,None,Some tp) -> prNamedRConstr (string_of_name nm) tp
+ | (nm,Some bdy,None) -> prNamedRConstr ("(letin) "^string_of_name nm) bdy
+ | _ -> assert false
+ ) lc;
+ prstr " §§}\n";
+ prstr "\n";
+ end
let showind (id:identifier) =
let cstrid = Tacinterp.constr_of_id (Global.env()) id in
@@ -193,7 +211,7 @@ type linked_var =
| Funres
(** When merging two graphs, parameters may become regular arguments,
- and thus be shifted. This type describe the result of computing
+ and thus be shifted. This type describes the result of computing
the changes. *)
type 'a shifted_params =
{
@@ -237,39 +255,47 @@ type 'a merged_arg =
| Arg_linked of 'a
| Arg_funres
+(** Information about graph merging of two inductives.
+ All rel_decl list are IN REVERSE ORDER (ie well suited for compose) *)
+
type merge_infos =
{
- ident:identifier; (* new inductive name *)
+ ident:identifier; (** new inductive name *)
mib1: mutual_inductive_body;
oib1: one_inductive_body;
mib2: mutual_inductive_body;
oib2: one_inductive_body;
- (* Array of links of the first inductive (should be all stable) *)
+
+ (** Array of links of the first inductive (should be all stable) *)
lnk1: int merged_arg array;
- (* Array of links of the second inductive (point to the first ind param/args) *)
+
+ (** Array of links of the second inductive (point to the first ind param/args) *)
lnk2: int merged_arg array;
- (* number of rec params of ind1 which remai rec param in merge *)
- nrecprms1: int;
- (* number of other rec params of ind1 (which become non parm) *)
- notherprms1:int;
- (* number of functional result params of ind2 (which become non parm) *)
- nfunresprms1:int;
- (* list of decl of rec parms from ind1 which remain parms *)
+
+ (** rec params which remain rec param (ie not linked) *)
recprms1: rel_declaration list;
- (* List of other rec parms from ind1 *)
- otherprms1: rel_declaration list; (* parms that became args *)
- funresprms1: rel_declaration list; (* parms that are functional result args *)
- (* number of rec params of ind2 which remain rec param in merge (and not linked) *)
+ recprms2: rel_declaration list;
+ nrecprms1: int;
nrecprms2: int;
- (* number of other params of ind2 (which become non rec parm) *)
+
+ (** rec parms which became non parm (either linked to something
+ or because after a rec parm that became non parm) *)
+ otherprms1: rel_declaration list;
+ otherprms2: rel_declaration list;
+ notherprms1:int;
notherprms2:int;
- (* number of functional result params of ind2 (which become non parm) *)
+
+ (** args which remain args in merge *)
+ args1:rel_declaration list;
+ args2:rel_declaration list;
+ nargs1:int;
+ nargs2:int;
+
+ (** functional result args *)
+ funresprms1: rel_declaration list;
+ funresprms2: rel_declaration list;
+ nfunresprms1:int;
nfunresprms2:int;
- (* list of decl of rec parms from ind2 which remain parms (and not linked) *)
- recprms2: rel_declaration list;
- (* List of other rec parms from ind2 (which are linked or become non parm) *)
- otherprms2: rel_declaration list;
- funresprms2: rel_declaration list; (* parms that are functional result args *)
}
@@ -288,7 +314,11 @@ let pr_merginfo x =
let isPrm_stable x = match x with Prm_stable _ -> true | _ -> false
-let isArg_stable x = match x with Arg_stable _ -> true | _ -> false
+(* ?? prm_linked?? *)
+let isArg_stable x = match x with Arg_stable _ | Prm_arg _ -> true | _ -> false
+
+let is_stable x =
+ match x with Arg_stable _ | Prm_stable _ | Prm_arg _ -> true | _ -> false
let isArg_funres x = match x with Arg_funres -> true | _ -> false
@@ -346,6 +376,24 @@ let verify_inds mib1 mib2 =
if mib2.mind_ntypes <> 1 then error "Second argument is mutual";
()
+(*
+(** [build_raw_params prms_decl avoid] returns a list of variables
+ attributed to the list of decl [prms_decl], avoiding names in
+ [avoid]. *)
+let build_raw_params prms_decl avoid =
+ let dummy_constr = compose_prod (List.map (fun (x,_,z) -> x,z) prms_decl) (mkRel 1) in
+ let _ = prNamedConstr "DUMMY" dummy_constr in
+ let dummy_rawconstr = Detyping.detype false avoid [] dummy_constr in
+ let _ = prNamedRConstr "RAWDUMMY" dummy_rawconstr in
+ let res,_ = raw_decompose_prod dummy_rawconstr in
+ let comblist = List.combine prms_decl res in
+ comblist, res , (avoid @ (Idset.elements (ids_of_rawterm dummy_rawconstr)))
+*)
+
+let ids_of_rawlist avoid rawl =
+ List.fold_left Idset.union avoid (List.map ids_of_rawterm rawl)
+
+
(** {1 Merging function graphs} *)
@@ -366,6 +414,7 @@ let verify_inds mib1 mib2 =
ones, they become non rec (and the following too). And functinal
argument have to be shifted at the end *)
let shift_linked_params mib1 mib2 (lnk1:linked_var array) (lnk2:linked_var array) id =
+ let _ = prstr "\nYOUHOU shift\n" in
let linked_targets = revlinked lnk2 in
let is_param_of_mib1 x = x < mib1.mind_nparams_rec in
let is_param_of_mib2 x = x < mib2.mind_nparams_rec in
@@ -409,15 +458,29 @@ let shift_linked_params mib1 mib2 (lnk1:linked_var array) (lnk2:linked_var array
let n_params2 = array_prfx mlnk2 (fun i x -> not (isPrm_stable x)) in
let bldprms arity_ctxt mlnk =
list_fold_lefti
- (fun i (acc1,acc2,acc3) x ->
+ (fun i (acc1,acc2,acc3,acc4) x ->
+ prstr (pr_merginfo mlnk.(i));prstr "\n";
match mlnk.(i) with
- | Prm_stable _ -> x::acc1 , acc2 , acc3
- | Prm_arg _ | Arg_stable _ -> acc1 , x::acc2 , acc3
- | Arg_funres -> acc1 , acc2 , x::acc3
- | _ -> acc1 , acc2 , acc3) (* Prm_linked and Arg_xxx = forget it *)
- ([],[],[]) arity_ctxt in
- let recprms1,otherprms1,funresprms1 = bldprms (List.rev oib1.mind_arity_ctxt) mlnk1 in
- let recprms2,otherprms2,funresprms2 = bldprms (List.rev oib2.mind_arity_ctxt) mlnk2 in
+ | Prm_stable _ -> x::acc1 , acc2 , acc3, acc4
+ | Prm_arg _ -> acc1 , x::acc2 , acc3, acc4
+ | Arg_stable _ -> acc1 , acc2 , x::acc3, acc4
+ | Arg_funres -> acc1 , acc2 , acc3, x::acc4
+ | _ -> acc1 , acc2 , acc3, acc4)
+ ([],[],[],[]) arity_ctxt in
+(* let arity_ctxt2 =
+ build_raw_params oib2.mind_arity_ctxt
+ (Idset.elements (ids_of_rawterm oib1.mind_arity_ctxt)) in*)
+ let recprms1,otherprms1,args1,funresprms1 = bldprms (List.rev oib1.mind_arity_ctxt) mlnk1 in
+ let _ = prstr "\n\n\n" in
+ let recprms2,otherprms2,args2,funresprms2 = bldprms (List.rev oib2.mind_arity_ctxt) mlnk2 in
+ let _ = prstr "\notherprms1:\n" in
+ let _ =
+ List.iter (fun (x,_,y) -> prstr (string_of_name x^" : ");prconstr y;prstr "\n")
+ otherprms1 in
+ let _ = prstr "\notherprms2:\n" in
+ let _ =
+ List.iter (fun (x,_,y) -> prstr (string_of_name x^" : ");prconstr y;prstr "\n")
+ otherprms2 in
{
ident=id;
mib1=mib1;
@@ -429,14 +492,18 @@ let shift_linked_params mib1 mib2 (lnk1:linked_var array) (lnk2:linked_var array
nrecprms1 = n_params1;
recprms1 = recprms1;
otherprms1 = otherprms1;
+ args1 = args1;
funresprms1 = funresprms1;
notherprms1 = Array.length mlnk1 - n_params1;
nfunresprms1 = List.length funresprms1;
+ nargs1 = List.length args1;
nrecprms2 = n_params2;
recprms2 = recprms2;
otherprms2 = otherprms2;
+ args2 = args2;
funresprms2 = funresprms2;
notherprms2 = Array.length mlnk2 - n_params2;
+ nargs2 = List.length args2;
nfunresprms2 = List.length funresprms2;
}
@@ -447,45 +514,61 @@ let shift_linked_params mib1 mib2 (lnk1:linked_var array) (lnk2:linked_var array
exception NoMerge
-(* lnk is an link array of *all* args (from 1 and 2) *)
-let merge_app c1 c2 id1 id2 shift filter_shift_stable =
+let rec merge_app c1 c2 id1 id2 shift filter_shift_stable =
let lnk = Array.append shift.lnk1 shift.lnk2 in
match c1 , c2 with
| RApp(_,f1, arr1), RApp(_,f2,arr2) when isVarf id1 f1 && isVarf id2 f2 ->
+ let _ = prstr "\nICI1!\n";Pp.flush_all() in
let args = filter_shift_stable lnk (arr1 @ arr2) in
RApp (dummy_loc,RVar (dummy_loc,shift.ident) , args)
| RApp(_,f1, arr1), RApp(_,f2,arr2) -> raise NoMerge
- | _ -> raise NoMerge
-
-let merge_app_unsafe c1 c2 shift filter_shift_stable =
+ | RLetIn(_,nme,bdy,trm) , _ ->
+ let _ = prstr "\nICI2!\n";Pp.flush_all() in
+ let newtrm = merge_app trm c2 id1 id2 shift filter_shift_stable in
+ RLetIn(dummy_loc,nme,bdy,newtrm)
+ | _, RLetIn(_,nme,bdy,trm) ->
+ let _ = prstr "\nICI3!\n";Pp.flush_all() in
+ let newtrm = merge_app c1 trm id1 id2 shift filter_shift_stable in
+ RLetIn(dummy_loc,nme,bdy,newtrm)
+ | _ -> let _ = prstr "\nICI4!\n";Pp.flush_all() in
+ raise NoMerge
+
+let rec merge_app_unsafe c1 c2 shift filter_shift_stable =
let lnk = Array.append shift.lnk1 shift.lnk2 in
match c1 , c2 with
| RApp(_,f1, arr1), RApp(_,f2,arr2) ->
let args = filter_shift_stable lnk (arr1 @ arr2) in
RApp (dummy_loc,RVar(dummy_loc,shift.ident) , args)
- | _ -> raise NoMerge
+ (* FIXME: what if the function appears in the body of the let? *)
+ | RLetIn(_,nme,bdy,trm) , _ ->
+ let _ = prstr "\nICI2 '!\n";Pp.flush_all() in
+ let newtrm = merge_app_unsafe trm c2 shift filter_shift_stable in
+ RLetIn(dummy_loc,nme,bdy,newtrm)
+ | _, RLetIn(_,nme,bdy,trm) ->
+ let _ = prstr "\nICI3 '!\n";Pp.flush_all() in
+ let newtrm = merge_app_unsafe c1 trm shift filter_shift_stable in
+ RLetIn(dummy_loc,nme,bdy,newtrm)
+ | _ -> let _ = prstr "\nICI4 '!\n";Pp.flush_all() in raise NoMerge
(* Heuristic when merging two lists of hypothesis: merge every rec
- calls of nrach 1 with all rec calls of branch 2. *)
+ calls of branch 1 with all rec calls of branch 2. *)
(* TODO: reecrire cette heuristique (jusqu'a merge_types) *)
-let onefoud = ref false (* Ugly *)
-
-let rec merge_rec_hyps shift accrec (ltyp:(Names.name * Rawterm.rawconstr) list)
- filter_shift_stable =
+let rec merge_rec_hyps shift accrec
+ (ltyp:(Names.name * rawconstr option * rawconstr option) list)
+ filter_shift_stable : (Names.name * rawconstr option * rawconstr option) list =
+ let mergeonehyp t reldecl =
+ match reldecl with
+ | (nme,x,Some (RApp(_,i,args) as ind))
+ -> nme,x, Some (merge_app_unsafe ind t shift filter_shift_stable)
+ | (nme,Some _,None) -> error "letins with recursive calls not treated yet"
+ | (nme,None,Some _) -> assert false
+ | (nme,None,None) | (nme,Some _,Some _) -> assert false in
match ltyp with
| [] -> []
- | (nme,(RApp(_,f, largs) as t)) :: lt when isVarf ind2name f ->
- let _ = onefoud := true in
- let rechyps =
- List.map
- (fun (nme,ind) ->
- match ind with
- | RApp(_,i,args) ->
- nme, merge_app_unsafe ind t shift filter_shift_stable
- | _ -> assert false)
- accrec in
+ | (nme,None,Some (RApp(_,f, largs) as t)) :: lt when isVarf ind2name f ->
+ let rechyps = List.map (mergeonehyp t) accrec in
rechyps @ merge_rec_hyps shift accrec lt filter_shift_stable
| e::lt -> e :: merge_rec_hyps shift accrec lt filter_shift_stable
@@ -494,50 +577,58 @@ let rec build_suppl_reccall (accrec:(name * rawconstr) list) concl2 shift =
List.map (fun (nm,tp) -> (nm,merge_app_unsafe tp concl2 shift)) accrec
-let find_app (nme:identifier) (ltyp: (name * rawconstr) list) =
+let find_app (nme:identifier) ltyp =
try
ignore
(List.map
(fun x ->
match x with
- | _,(RApp(_,f,_)) when isVarf nme f -> raise (Found 0)
+ | _,None,Some (RApp(_,f,_)) when isVarf nme f -> raise (Found 0)
| _ -> ())
ltyp);
false
with Found _ -> true
+
+let prnt_prod_or_letin nm letbdy typ =
+ match letbdy , typ with
+ | Some lbdy , None -> prNamedRConstr ("(letin) " ^ string_of_name nm) lbdy
+ | None , Some tp -> prNamedRConstr (string_of_name nm) tp
+ | _ , _ -> assert false
+
-let rec merge_types shift accrec1 (ltyp1:(name * rawconstr) list)
- concl1 (ltyp2:(name * rawconstr) list) concl2
- : (name * rawconstr) list * rawconstr =
+let rec merge_types shift accrec1
+ (ltyp1:(name * rawconstr option * rawconstr option) list)
+ (concl1:rawconstr) (ltyp2:(name * rawconstr option * rawconstr option) list) concl2
+ : (name * rawconstr option * rawconstr option) list * rawconstr =
let _ = prstr "MERGE_TYPES\n" in
let _ = prstr "ltyp 1 : " in
- let _ = List.iter (fun (nm,tp) -> prNamedRConstr (string_of_name nm) tp) ltyp1 in
+ let _ = List.iter (fun (nm,lbdy,tp) -> prnt_prod_or_letin nm lbdy tp) ltyp1 in
let _ = prstr "\nltyp 2 : " in
- let _ = List.iter (fun (nm,tp) -> prNamedRConstr (string_of_name nm) tp) ltyp2 in
+ let _ = List.iter (fun (nm,lbdy,tp) -> prnt_prod_or_letin nm lbdy tp) ltyp2 in
let _ = prstr "\n" in
-
-
let res =
match ltyp1 with
| [] ->
let isrec1 = (accrec1<>[]) in
let isrec2 = find_app ind2name ltyp2 in
- let _ = if isrec2 then prstr " ISREC2 TRUE" else prstr " ISREC2 FALSE" in
- let _ = if isrec1 then prstr " ISREC1 TRUE\n" else prstr " ISREC1 FALSE\n" in
let rechyps =
if isrec1 && isrec2
- then merge_rec_hyps shift accrec1 ltyp2 filter_shift_stable
+ then (* merge_rec_hyps shift accrec1 ltyp2 filter_shift_stable *)
+ merge_rec_hyps shift [name_of_string "concl1",None,Some concl1] ltyp2
+ filter_shift_stable_right
+ @ merge_rec_hyps shift accrec1 [name_of_string "concl2",None, Some concl2]
+ filter_shift_stable
else if isrec1
(* if rec calls in accrec1 and not in ltyp2, add one to ltyp2 *)
- then merge_rec_hyps shift accrec1 (ltyp2@[name_of_string "concl2",concl2])
- filter_shift_stable
+ then
+ merge_rec_hyps shift accrec1
+ (ltyp2@[name_of_string "concl2",None,Some concl2]) filter_shift_stable
else if isrec2
- then merge_rec_hyps shift [name_of_string "concl1",concl1] ltyp2
+ then merge_rec_hyps shift [name_of_string "concl1",None,Some concl1] ltyp2
filter_shift_stable_right
- else [] in
+ else ltyp2 in
let _ = prstr"\nrechyps : " in
- let _ = List.iter
- (fun (nm,tp) -> prNamedRConstr (string_of_name nm) tp) rechyps in
+ let _ = List.iter(fun (nm,lbdy,tp)-> prnt_prod_or_letin nm lbdy tp) rechyps in
let _ = prstr "MERGE CONCL : " in
let _ = prNamedRConstr "concl1" concl1 in
let _ = prstr " with " in
@@ -548,15 +639,22 @@ let rec merge_types shift accrec1 (ltyp1:(name * rawconstr) list)
let _ = prstr "FIN " in
let _ = prNamedRConstr "concl" concl in
let _ = prstr "\n" in
+
rechyps , concl
- | (nme,t1)as e ::lt1 ->
- match t1 with
+ | (nme,None, Some t1)as e ::lt1 ->
+ (match t1 with
| RApp(_,f,carr) when isVarf ind1name f ->
merge_types shift (e::accrec1) lt1 concl1 ltyp2 concl2
| _ ->
let recres, recconcl2 =
merge_types shift accrec1 lt1 concl1 ltyp2 concl2 in
- ((nme,t1) :: recres) , recconcl2
+ ((nme,None,Some t1) :: recres) , recconcl2)
+ | (nme,Some bd, None) ::lt1 ->
+ (* FIXME: what if ind1name appears in bd? *)
+ let recres, recconcl2 =
+ merge_types shift accrec1 lt1 concl1 ltyp2 concl2 in
+ ((nme,Some bd,None) :: recres) , recconcl2
+ | (_,None,None)::_ | (_,Some _,Some _)::_ -> assert false
in
res
@@ -578,9 +676,9 @@ let build_link_map_aux (allargs1:identifier array) (allargs2:identifier array)
let build_link_map allargs1 allargs2 lnk =
let allargs1 =
- Array.of_list (List.rev (List.map (fun (x,y) -> id_of_name x) allargs1)) in
+ Array.of_list (List.rev (List.map (fun (x,_,_) -> id_of_name x) allargs1)) in
let allargs2 =
- Array.of_list (List.rev (List.map (fun (x,y) -> id_of_name x) allargs2)) in
+ Array.of_list (List.rev (List.map (fun (x,_,_) -> id_of_name x) allargs2)) in
build_link_map_aux allargs1 allargs2 lnk
@@ -598,7 +696,7 @@ let build_link_map allargs1 allargs2 lnk =
forall recparams1 (recparams2 without linked params),
forall ordparams1 (ordparams2 without linked params),
- H1a' -> H2a' -> ... -> H2a' -> H2b' -> ...
+ H1a' -> H2a' -> ... -> H2a' -> H2b'(shifted) -> ...
-> (newI x1 ... z1 x2 y2 ...z2 without linked params)
where Hix' have been adapted, ie:
@@ -621,21 +719,27 @@ let merge_one_constructor (shift:merge_infos) (typcstr1:rawconstr)
shift.mib1.mind_nparams + shift.oib1.mind_nrealargs - shift.nfunresprms1 in
let nargs2 =
shift.mib2.mind_nparams + shift.oib2.mind_nrealargs - shift.nfunresprms2 in
- let allargs1,rest1 = raw_decompose_prod_n nargs1 typcstr1 in
- let allargs2,rest2 = raw_decompose_prod_n nargs2 typcstr2 in
+ let allargs1,rest1 = raw_decompose_prod_or_letin_n nargs1 typcstr1 in
+ let allargs2,rest2 = raw_decompose_prod_or_letin_n nargs2 typcstr2 in
(* Build map of linked args of [typcstr2], and apply it to [typcstr2]. *)
let linked_map = build_link_map allargs1 allargs2 shift.lnk2 in
let rest2 = change_vars linked_map rest2 in
- let hyps1,concl1 = raw_decompose_prod rest1 in
- let hyps2,concl2' = raw_decompose_prod rest2 in
+ let hyps1,concl1 = raw_decompose_prod_or_letin rest1 in
+ let hyps2,concl2' = raw_decompose_prod_or_letin rest2 in
let ltyp,concl2 =
merge_types shift [] (List.rev hyps1) concl1 (List.rev hyps2) concl2' in
- let typ = raw_compose_prod concl2 (List.rev ltyp) in
+ let _ = prNamedRLDecl "ltyp result:" ltyp in
+ let typ = raw_compose_prod_or_letin concl2 (List.rev ltyp) in
let revargs1 =
list_filteri (fun i _ -> isArg_stable shift.lnk1.(i)) (List.rev allargs1) in
+ let _ = prNamedRLDecl "ltyp allargs1" allargs1 in
+ let _ = prNamedRLDecl "ltyp revargs1" revargs1 in
let revargs2 =
list_filteri (fun i _ -> isArg_stable shift.lnk2.(i)) (List.rev allargs2) in
- let typwithprms = raw_compose_prod typ (List.rev revargs2 @ List.rev revargs1) in
+ let _ = prNamedRLDecl "ltyp allargs2" allargs2 in
+ let _ = prNamedRLDecl "ltyp revargs2" revargs2 in
+ let typwithprms =
+ raw_compose_prod_or_letin typ (List.rev revargs2 @ List.rev revargs1) in
typwithprms
@@ -661,22 +765,16 @@ let merge_constructor_id id1 id2 shift:identifier =
constructor [(name*type)]. These are translated to rawterms
first, each of them having distinct var names. *)
let rec merge_constructors (shift:merge_infos) (avoid:Idset.t)
- (typcstr1:(identifier * types) list)
- (typcstr2:(identifier * types) list) : (identifier * rawconstr) list =
+ (typcstr1:(identifier * rawconstr) list)
+ (typcstr2:(identifier * rawconstr) list) : (identifier * rawconstr) list =
List.flatten
(List.map
- (fun (id1,typ1) ->
- let typ1 = substitterm 0 (mkRel 1) (mkVar ind1name) typ1 in
- let rawtyp1 = Detyping.detype false (Idset.elements avoid) [] typ1 in
- let idsoftyp1:Idset.t = ids_of_rawterm rawtyp1 in
+ (fun (id1,rawtyp1) ->
List.map
- (fun (id2,typ2) ->
- let typ2 = substitterm 0 (mkRel 1) (mkVar ind2name) typ2 in
- (* Avoid also rawtyp1 names *)
- let avoid2 = Idset.union avoid idsoftyp1 in
- let rawtyp2 = Detyping.detype false (Idset.elements avoid2) [] typ2 in
+ (fun (id2,rawtyp2) ->
let typ = merge_one_constructor shift rawtyp1 rawtyp2 in
let newcstror_id = merge_constructor_id id1 id2 shift in
+ let _ = prstr "\n**************\n" in
newcstror_id , typ)
typcstr2)
typcstr1)
@@ -685,22 +783,33 @@ let rec merge_constructors (shift:merge_infos) (avoid:Idset.t)
inductive bodies [oib1] and [oib2], linking with [lnk], params
info in [shift], avoiding identifiers in [avoid]. *)
let rec merge_inductive_body (shift:merge_infos) avoid (oib1:one_inductive_body)
- (oib2:one_inductive_body) : (identifier * rawconstr) list =
- let lcstr1 = Array.to_list oib1.mind_user_lc in
- let lcstr2 = Array.to_list oib2.mind_user_lc in
+ (oib2:one_inductive_body) =
+ (* building rawconstr type of constructors *)
+ let mkrawcor nme avoid typ =
+ (* first replace rel 1 by a varname *)
+ let substindtyp = substitterm 0 (mkRel 1) (mkVar nme) typ in
+ Detyping.detype false (Idset.elements avoid) [] substindtyp in
+ let lcstr1: rawconstr list =
+ Array.to_list (Array.map (mkrawcor ind1name avoid) oib1.mind_user_lc) in
+ (* add to avoid all indentifiers of lcstr1 *)
+ let avoid2 = Idset.union avoid (ids_of_rawlist avoid lcstr1) in
+ let lcstr2 =
+ Array.to_list (Array.map (mkrawcor ind2name avoid2) oib2.mind_user_lc) in
+ let avoid3 = Idset.union avoid (ids_of_rawlist avoid lcstr2) in
+
+ let params1 =
+ try fst (raw_decompose_prod_n shift.nrecprms1 (List.hd lcstr1))
+ with _ -> [] in
+ let params2 =
+ try fst (raw_decompose_prod_n shift.nrecprms2 (List.hd lcstr2))
+ with _ -> [] 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
+
cstror_suffix_init();
- merge_constructors shift avoid lcstr1 lcstr2
+ params1,params2,merge_constructors shift avoid3 lcstr1 lcstr2
-(** [build_raw_params prms_decl avoid] returns a list of variables
- attributed to the list of decl [prms_decl], avoiding names in
- [avoid]. *)
-let build_raw_params prms_decl avoid =
- let dummy_constr = compose_prod prms_decl mkProp in
- let dummy_rawconstr = Detyping.detype false avoid [] dummy_constr in
- let res,_ = raw_decompose_prod dummy_rawconstr in
- res , (avoid @ (Idset.elements (ids_of_rawterm dummy_rawconstr)))
(** [merge_mutual_inductive_body lnk mib1 mib2 shift] merge mutual
inductive bodies [mib1] and [mib2] linking vars with
@@ -708,42 +817,35 @@ let build_raw_params prms_decl avoid =
For the moment, inductives are supposed to be non mutual.
*)
let rec merge_mutual_inductive_body
- (mib1:mutual_inductive_body) (mib2:mutual_inductive_body)
- (shift:merge_infos) =
+ (mib1:mutual_inductive_body) (mib2:mutual_inductive_body) (shift:merge_infos) =
(* Mutual not treated, we take first ind body of each. *)
- let nprms1 = mib1.mind_nparams_rec in (* n# of rec uniform parms of mib1 *)
- let prms1 = (* rec uniform parms of mib1 *)
- List.map (fun (x,_,y) -> x,y) (fst (list_chop nprms1 mib1.mind_params_ctxt)) in
-
- (* useless: *)
- let prms1_named,avoid' = build_raw_params prms1 [] in
- let prms2_named,avoid = build_raw_params prms1 avoid' in
- let avoid:Idset.t = List.fold_right Idset.add avoid Idset.empty in
- (* *** *)
-
- merge_inductive_body shift avoid mib1.mind_packets.(0) mib2.mind_packets.(0)
+ merge_inductive_body shift Idset.empty mib1.mind_packets.(0) mib2.mind_packets.(0)
+let rawterm_to_constr_expr x = (* build a constr_expr from a rawconstr *)
+ Flags.with_option Flags.raw_print (Constrextern.extern_rawtype Idset.empty) x
-let merge_rec_params_and_arity params1 params2 shift (concl:constr) =
- let params = shift.recprms1 @ shift.recprms2 in
- let resparams, _ =
+let merge_rec_params_and_arity prms1 prms2 shift (concl:constr) =
+ let params = prms2 @ prms1 in
+ let resparams =
List.fold_left
- (fun (acc,env) (nme,_,tp) ->
- let typ = Constrextern.extern_constr false env tp in
- let newenv = Environ.push_rel (nme,None,tp) env in
- LocalRawAssum ([(dummy_loc,nme)] , typ) :: acc , newenv)
- ([],Global.env())
- params in
+ (fun acc (nme,tp) ->
+ let _ = prstr "param :" in
+ let _ = prNamedRConstr (string_of_name nme) tp in
+ let _ = prstr " ; " in
+ let typ = rawterm_to_constr_expr tp in
+ LocalRawAssum ([(dummy_loc,nme)], Topconstr.default_binder_kind, typ) :: acc)
+ [] params in
let concl = Constrextern.extern_constr false (Global.env()) concl in
let arity,_ =
List.fold_left
(fun (acc,env) (nm,_,c) ->
let typ = Constrextern.extern_constr false env c in
let newenv = Environ.push_rel (nm,None,c) env in
- CProdN (dummy_loc, [[(dummy_loc,nm)],typ] , acc) , newenv)
+ CProdN (dummy_loc, [[(dummy_loc,nm)],Topconstr.default_binder_kind,typ] , acc) , newenv)
(concl,Global.env())
- (shift.otherprms1@shift.otherprms2@shift.funresprms1@shift.funresprms2) in
+ (shift.funresprms2 @ shift.funresprms1
+ @ shift.args2 @ shift.args1 @ shift.otherprms2 @ shift.otherprms1) in
resparams,arity
@@ -752,20 +854,37 @@ let merge_rec_params_and_arity params1 params2 shift (concl:constr) =
induct_expr corresponding to the the list of constructor types
[rawlist], named ident.
FIXME: params et cstr_expr (arity) *)
-let rawterm_list_to_inductive_expr mib1 mib2 shift
+let rawterm_list_to_inductive_expr prms1 prms2 mib1 mib2 shift
(rawlist:(identifier * rawconstr) list):inductive_expr =
- let rawterm_to_constr_expr x = (* build a constr_expr from a rawconstr *)
- Options.with_option Options.raw_print (Constrextern.extern_rawtype Idset.empty) x in
let lident = dummy_loc, shift.ident in
let bindlist , cstr_expr = (* params , arities *)
- merge_rec_params_and_arity
- mib1.mind_params_ctxt mib2.mind_params_ctxt shift mkSet in
+ merge_rec_params_and_arity prms1 prms2 shift mkSet in
let lcstor_expr : (bool * (lident * constr_expr)) list =
List.map (* zeta_normalize t ? *)
(fun (id,t) -> false, ((dummy_loc,id),rawterm_to_constr_expr t))
rawlist in
lident , bindlist , cstr_expr , lcstor_expr
+
+
+let mkProd_reldecl (rdecl:rel_declaration) (t2:rawconstr) =
+ match rdecl with
+ | (nme,None,t) ->
+ let traw = Detyping.detype false [] [] t in
+ RProd (dummy_loc,nme,Explicit,traw,t2)
+ | (_,Some _,_) -> assert false
+
+
+
+
+let mkProd_reldecl (rdecl:rel_declaration) (t2:rawconstr) =
+ match rdecl with
+ | (nme,None,t) ->
+ let traw = Detyping.detype false [] [] t in
+ RProd (dummy_loc,nme,Explicit,traw,t2)
+ | (_,Some _,_) -> assert false
+
+
(** [merge_inductive ind1 ind2 lnk] merges two graphs, linking
variables specified in [lnk]. Graphs are not supposed to be mutual
inductives for the moment. *)
@@ -777,35 +896,124 @@ let merge_inductive (ind1: inductive) (ind2: inductive)
let _ = verify_inds mib1 mib2 in (* raises an exception if something wrong *)
(* compute params that become ordinary args (because linked to ord. args) *)
let shift_prm = shift_linked_params mib1 mib2 lnk1 lnk2 id in
- let rawlist = merge_mutual_inductive_body mib1 mib2 shift_prm in
- let indexpr = rawterm_list_to_inductive_expr mib1 mib2 shift_prm rawlist in
+ let prms1,prms2, rawlist = merge_mutual_inductive_body mib1 mib2 shift_prm in
+ let _ = prstr "\nrawlist : " in
+ let _ =
+ List.iter (fun (nm,tp) -> prNamedRConstr (string_of_id nm) tp;prstr "\n") rawlist in
+ let _ = prstr "\nend rawlist\n" in
+(* FIX: retransformer en constr ici
+ let shift_prm =
+ { shift_prm with
+ recprms1=prms1;
+ recprms1=prms1;
+ } in *)
+ let indexpr = rawterm_list_to_inductive_expr prms1 prms2 mib1 mib2 shift_prm rawlist in
(* Declare inductive *)
Command.build_mutual [(indexpr,None)] true (* means: not coinductive *)
-
-let merge (cstr1:constr) (cstr2:constr) (args1:constr array) (args2:constr array) id =
- let env = Global.env() in
- let ind1,_cstrlist1 = Inductiveops.find_inductive env Evd.empty cstr1 in
- let ind2,_cstrlist2 = Inductiveops.find_inductive env Evd.empty cstr2 in
- let lnk1 = (* args1 are unlinked. FIXME? mergescheme (G x x) ?? *)
- Array.mapi (fun i c -> Unlinked) args1 in
- let _ = lnk1.(Array.length lnk1 - 1) <- Funres in (* last arg is functional result *)
- let lnk2 = (* args2 may be linked to args1 members. FIXME: same
- as above: vars may be linked inside args2?? *)
+(* Find infos on identifier id. *)
+let find_Function_infos_safe (id:identifier): Indfun_common.function_info =
+ let kn_of_id x =
+ let f_ref = Libnames.Ident (dummy_loc,x) in
+ locate_with_msg (str "Don't know what to do with " ++ Libnames.pr_reference f_ref)
+ 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")
+
+(** [merge id1 id2 args1 args2 id] builds and declares a new inductive
+ type called [id], representing the merged graphs of both graphs
+ [ind1] and [ind2]. identifiers occuring in both arrays [args1] and
+ [args2] are considered linked (i.e. are the same variable) in the
+ new graph.
+
+ Warning: For the moment, repetitions of an id in [args1] or
+ [args2] are not supported. *)
+let merge (id1:identifier) (id2:identifier) (args1:identifier array)
+ (args2:identifier array) id : unit =
+ let finfo1 = find_Function_infos_safe id1 in
+ let finfo2 = find_Function_infos_safe id2 in
+ (* FIXME? args1 are supposed unlinked. mergescheme (G x x) ?? *)
+ (* We add one arg (functional arg of the graph) *)
+ let lnk1 = Array.make (Array.length args1 + 1) Unlinked in
+ let lnk2' = (* args2 may be linked to args1 members. FIXME: same
+ as above: vars may be linked inside args2?? *)
Array.mapi
(fun i c ->
match array_find args1 (fun i x -> x=c) with
| Some j -> Linked j
| None -> Unlinked)
args2 in
- let _ = lnk2.(Array.length lnk2 - 1) <- Funres in (* last arg is functional result *)
- let resa = merge_inductive ind1 ind2 lnk1 lnk2 id in
- resa
-
-
-
+ (* We add one arg (functional arg of the graph) *)
+ let lnk2 = Array.append lnk2' (Array.make 1 Unlinked) in
+ (* setting functional results *)
+ let _ = lnk1.(Array.length lnk1 - 1) <- Funres in
+ let _ = lnk2.(Array.length lnk2 - 1) <- Funres in
+ merge_inductive finfo1.graph_ind finfo2.graph_ind lnk1 lnk2 id
+
+
+let remove_last_arg c =
+ let (x,y) = decompose_prod c in
+ let xnolast = List.rev (List.tl (List.rev x)) in
+ compose_prod xnolast y
+
+let rec remove_n_fst_list n l = if n=0 then l else remove_n_fst_list (n-1) (List.tl l)
+let remove_n_last_list n l = List.rev (remove_n_fst_list n (List.rev l))
+
+let remove_last_n_arg n c =
+ let (x,y) = decompose_prod c in
+ let xnolast = remove_n_last_list n x in
+ compose_prod xnolast y
+
+(* [funify_branches relinfo nfuns branch] returns the branch [branch]
+ of the relinfo [relinfo] modified to fit in a functional principle.
+ Things to do:
+ - remove indargs from rel applications
+ - replace *variables only* corresponding to function (recursive)
+ results by the actual function application. *)
+let funify_branches relinfo nfuns branch =
+ let mut_induct, induct =
+ match relinfo.indref with
+ | None -> assert false
+ | Some (IndRef ((mutual_ind,i) as ind)) -> mutual_ind,ind
+ | _ -> assert false in
+ let is_dom c =
+ match kind_of_term c with
+ | Ind((u,_)) | Construct((u,_),_) -> u = mut_induct
+ | _ -> false in
+ let _dom_i c =
+ assert (is_dom c);
+ match kind_of_term c with
+ | Ind((u,i)) | Construct((u,_),i) -> i
+ | _ -> assert false in
+ let _is_pred c shift =
+ match kind_of_term c with
+ | Rel i -> let reali = i-shift in (reali>=0 && reali<relinfo.nbranches)
+ | _ -> false in
+ (* FIXME: *)
+ (Anonymous,Some mkProp,mkProp)
+
+let relprinctype_to_funprinctype relprinctype nfuns =
+ let relinfo = compute_elim_sig relprinctype in
+ assert (not relinfo.farg_in_concl);
+ assert (relinfo.indarg_in_concl);
+ (* first remove indarg and indarg_in_concl *)
+ let relinfo_noindarg = { relinfo with
+ indarg_in_concl = false; indarg = None;
+ concl = remove_last_arg (pop relinfo.concl); } in
+ (* the nfuns last induction arguments are functional ones: remove them *)
+ let relinfo_argsok = { relinfo_noindarg with
+ nargs = relinfo_noindarg.nargs - nfuns;
+ (* args is in reverse order, so remove fst *)
+ args = remove_n_fst_list nfuns relinfo_noindarg.args;
+ concl = popn nfuns relinfo_noindarg.concl
+ } in
+ let new_branches =
+ List.map (funify_branches relinfo_argsok nfuns) relinfo_argsok.branches in
+ let relinfo_branches = { relinfo_argsok with branches = new_branches } in
+ relinfo_branches
(* @article{ bundy93rippling,
author = "Alan Bundy and Andrew Stevens and Frank van Harmelen and Andrew Ireland and Alan Smaill",
diff --git a/contrib/funind/rawterm_to_relation.ml b/contrib/funind/rawterm_to_relation.ml
index b34a1097..08a97fd2 100644
--- a/contrib/funind/rawterm_to_relation.ml
+++ b/contrib/funind/rawterm_to_relation.ml
@@ -368,7 +368,7 @@ let raw_push_named (na,raw_value,raw_typ) env =
match na with
| Anonymous -> env
| Name id ->
- let value = Util.option_map (Pretyping.Default.understand Evd.empty env) raw_value in
+ let value = Option.map (Pretyping.Default.understand Evd.empty env) raw_value in
let typ = Pretyping.Default.understand_type Evd.empty env raw_typ in
Environ.push_named (id,value,typ) env
@@ -398,12 +398,12 @@ let add_pat_variables pat typ env : Environ.env =
| Anonymous -> assert false
| Name id ->
let new_t = substl ctxt t in
- let new_v = option_map (substl ctxt) v in
+ let new_v = Option.map (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 ())
+ 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 ())
);
(Environ.push_named (id,new_v,new_t) env,mkVar id::ctxt)
)
@@ -446,7 +446,7 @@ let rec pattern_to_term_and_type env typ = function
let patl_as_term =
List.map2 (pattern_to_term_and_type env) (List.rev cs_args_types) patternl
in
- mkRApp(mkRRef(Libnames.ConstructRef constr),
+ mkRApp(mkRRef(ConstructRef constr),
implicit_args@patl_as_term
)
@@ -586,7 +586,7 @@ let rec build_entry_lc env funnames avoid rt : rawconstr build_entry_return =
| RProd _ -> error "Cannot apply a type"
end (* end of the application treatement *)
- | RLambda(_,n,t,b) ->
+ | RLambda(_,n,_,t,b) ->
(* we first compute the list of constructor
corresponding to the body of the function,
then the one corresponding to the type
@@ -601,7 +601,7 @@ let rec build_entry_lc env funnames avoid rt : rawconstr build_entry_return =
let new_env = raw_push_named (new_n,None,t) env in
let b_res = build_entry_lc new_env funnames avoid b in
combine_results (combine_lam new_n) t_res b_res
- | RProd(_,n,t,b) ->
+ | RProd(_,n,_,t,b) ->
(* we first compute the list of constructor
corresponding to the body of the function,
then the one corresponding to the type
@@ -627,7 +627,7 @@ let rec build_entry_lc env funnames avoid rt : rawconstr build_entry_return =
in
let b_res = build_entry_lc new_env funnames avoid b in
combine_results (combine_letin n) v_res b_res
- | RCases(_,_,el,brl) ->
+ | RCases(_,_,_,el,brl) ->
(* we create the discrimination function
and treat the case itself
*)
@@ -689,7 +689,7 @@ let rec build_entry_lc env funnames avoid rt : rawconstr build_entry_return =
build_entry_lc env funnames avoid b
| RDynamic _ -> error "Not handled RDynamic"
and build_entry_lc_from_case env funname make_discr
- (el:tomatch_tuple)
+ (el:tomatch_tuples)
(brl:Rawterm.cases_clauses) avoid :
rawconstr build_entry_return =
match el with
@@ -865,7 +865,7 @@ let is_res id =
*)
let rec rebuild_cons nb_args relname args crossed_types depth rt =
match rt with
- | RProd(_,n,t,b) ->
+ | RProd(_,n,k,t,b) ->
let not_free_in_t id = not (is_free_in id t) in
let new_crossed_types = t::crossed_types in
begin
@@ -928,7 +928,7 @@ let rec rebuild_cons nb_args relname args crossed_types depth rt =
(Idset.filter not_free_in_t id_to_exclude)
| _ -> mkRProd(n,t,new_b),Idset.filter not_free_in_t id_to_exclude
end
- | RLambda(_,n,t,b) ->
+ | RLambda(_,n,k,t,b) ->
begin
let not_free_in_t id = not (is_free_in id t) in
let new_crossed_types = t :: crossed_types in
@@ -944,7 +944,7 @@ let rec rebuild_cons nb_args relname args crossed_types depth rt =
then
new_b, Idset.remove id (Idset.filter not_free_in_t id_to_exclude)
else
- RProd(dummy_loc,n,t,new_b),Idset.filter not_free_in_t id_to_exclude
+ RProd(dummy_loc,n,k,t,new_b),Idset.filter not_free_in_t id_to_exclude
| _ -> anomaly "Should not have an anonymous function here"
(* We have renamed all the anonymous functions during alpha_renaming phase *)
@@ -1016,11 +1016,12 @@ let rec compute_cst_params relnames params = function
compute_cst_params_from_app [] (params,rtl)
| RApp(_,f,args) ->
List.fold_left (compute_cst_params relnames) params (f::args)
- | RLambda(_,_,t,b) | RProd(_,_,t,b) | RLetIn(_,_,t,b) | RLetTuple(_,_,_,t,b) ->
+ | RLambda(_,_,_,t,b) | RProd(_,_,_,t,b) | RLetIn(_,_,t,b) | RLetTuple(_,_,_,t,b) ->
let t_params = compute_cst_params relnames params t in
compute_cst_params relnames t_params b
- | RCases _ -> params (* If there is still cases at this point they can only be
- discriminitation ones *)
+ | RCases _ ->
+ params (* If there is still cases at this point they can only be
+ discriminitation ones *)
| RSort _ -> params
| RHole _ -> params
| RIf _ | RRec _ | RCast _ | RDynamic _ ->
@@ -1153,7 +1154,7 @@ let do_build_inductive
else
Topconstr.CProdN
(dummy_loc,
- [[(dummy_loc,n)],Constrextern.extern_rawconstr Idset.empty t],
+ [[(dummy_loc,n)],Topconstr.default_binder_kind,Constrextern.extern_rawconstr Idset.empty t],
acc
)
)
@@ -1173,7 +1174,7 @@ let do_build_inductive
Topconstr.LocalRawDef((dummy_loc,n), Constrextern.extern_rawconstr Idset.empty t)
else
Topconstr.LocalRawAssum
- ([(dummy_loc,n)], Constrextern.extern_rawconstr Idset.empty t)
+ ([(dummy_loc,n)], Topconstr.default_binder_kind, Constrextern.extern_rawconstr Idset.empty t)
)
rels_params
in
@@ -1181,8 +1182,8 @@ let do_build_inductive
Array.map (List.map
(fun (id,t) ->
false,((dummy_loc,id),
- Options.with_option
- Options.raw_print
+ Flags.with_option
+ Flags.raw_print
(Constrextern.extern_rawtype Idset.empty) ((* zeta_normalize *) t)
)
))
@@ -1218,7 +1219,7 @@ let do_build_inductive
(* in *)
let _time2 = System.get_time () in
try
- with_full_print (Options.silently (Command.build_mutual rel_inds)) true
+ with_full_print (Flags.silently (Command.build_mutual rel_inds)) true
with
| UserError(s,msg) as e ->
let _time3 = System.get_time () in
diff --git a/contrib/funind/rawtermops.ml b/contrib/funind/rawtermops.ml
index 113ddd8b..92396af5 100644
--- a/contrib/funind/rawtermops.ml
+++ b/contrib/funind/rawtermops.ml
@@ -12,10 +12,10 @@ let idmap_is_empty m = m = Idmap.empty
let mkRRef ref = RRef(dummy_loc,ref)
let mkRVar id = RVar(dummy_loc,id)
let mkRApp(rt,rtl) = RApp(dummy_loc,rt,rtl)
-let mkRLambda(n,t,b) = RLambda(dummy_loc,n,t,b)
-let mkRProd(n,t,b) = RProd(dummy_loc,n,t,b)
+let mkRLambda(n,t,b) = RLambda(dummy_loc,n,Explicit,t,b)
+let mkRProd(n,t,b) = RProd(dummy_loc,n,Explicit,t,b)
let mkRLetIn(n,t,b) = RLetIn(dummy_loc,n,t,b)
-let mkRCases(rto,l,brl) = RCases(dummy_loc,rto,l,brl)
+let mkRCases(rto,l,brl) = RCases(dummy_loc,Term.RegularStyle,rto,l,brl)
let mkRSort s = RSort(dummy_loc,s)
let mkRHole () = RHole(dummy_loc,Evd.BinderType Anonymous)
let mkRCast(b,t) = RCast(dummy_loc,b,CastConv (Term.DEFAULTcast,t))
@@ -26,27 +26,59 @@ let mkRCast(b,t) = RCast(dummy_loc,b,CastConv (Term.DEFAULTcast,t))
*)
let raw_decompose_prod =
let rec raw_decompose_prod args = function
- | RProd(_,n,t,b) ->
+ | RProd(_,n,k,t,b) ->
raw_decompose_prod ((n,t)::args) b
| rt -> args,rt
in
raw_decompose_prod []
+let raw_decompose_prod_or_letin =
+ let rec raw_decompose_prod args = function
+ | RProd(_,n,k,t,b) ->
+ raw_decompose_prod ((n,None,Some t)::args) b
+ | RLetIn(_,n,t,b) ->
+ raw_decompose_prod ((n,Some t,None)::args) b
+ | rt -> args,rt
+ in
+ raw_decompose_prod []
+
let raw_compose_prod =
List.fold_left (fun b (n,t) -> mkRProd(n,t,b))
+let raw_compose_prod_or_letin =
+ List.fold_left (
+ fun concl decl ->
+ match decl with
+ | (n,None,Some t) -> mkRProd(n,t,concl)
+ | (n,Some bdy,None) -> mkRLetIn(n,bdy,concl)
+ | _ -> assert false)
+
let raw_decompose_prod_n n =
let rec raw_decompose_prod i args c =
if i<=0 then args,c
else
match c with
- | RProd(_,n,t,b) ->
+ | RProd(_,n,_,t,b) ->
raw_decompose_prod (i-1) ((n,t)::args) b
| rt -> args,rt
in
raw_decompose_prod n []
+let raw_decompose_prod_or_letin_n n =
+ let rec raw_decompose_prod i args c =
+ if i<=0 then args,c
+ else
+ match c with
+ | RProd(_,n,_,t,b) ->
+ raw_decompose_prod (i-1) ((n,None,Some t)::args) b
+ | RLetIn(_,n,t,b) ->
+ raw_decompose_prod (i-1) ((n,Some t,None)::args) b
+ | rt -> args,rt
+ in
+ raw_decompose_prod n []
+
+
let raw_decompose_app =
let rec decompose_rapp acc rt =
(* msgnl (str "raw_decompose_app on : "++ Printer.pr_rawconstr rt); *)
@@ -103,15 +135,17 @@ let change_vars =
change_vars mapping rt',
List.map (change_vars mapping) rtl
)
- | RLambda(loc,name,t,b) ->
+ | RLambda(loc,name,k,t,b) ->
RLambda(loc,
name,
+ k,
change_vars mapping t,
change_vars (remove_name_from_mapping mapping name) b
)
- | RProd(loc,name,t,b) ->
+ | RProd(loc,name,k,t,b) ->
RProd(loc,
name,
+ k,
change_vars mapping t,
change_vars (remove_name_from_mapping mapping name) b
)
@@ -125,12 +159,12 @@ let change_vars =
let new_mapping = List.fold_left remove_name_from_mapping mapping nal in
RLetTuple(loc,
nal,
- (na, option_map (change_vars mapping) rto),
+ (na, Option.map (change_vars mapping) rto),
change_vars mapping b,
change_vars new_mapping e
)
- | RCases(loc,infos,el,brl) ->
- RCases(loc,
+ | RCases(loc,sty,infos,el,brl) ->
+ RCases(loc,sty,
infos,
List.map (fun (e,x) -> (change_vars mapping e,x)) el,
List.map (change_vars_br mapping) brl
@@ -138,7 +172,7 @@ let change_vars =
| RIf(loc,b,(na,e_option),lhs,rhs) ->
RIf(loc,
change_vars mapping b,
- (na,option_map (change_vars mapping) e_option),
+ (na,Option.map (change_vars mapping) e_option),
change_vars mapping lhs,
change_vars mapping rhs
)
@@ -229,21 +263,21 @@ let rec alpha_rt excluded rt =
let new_rt =
match rt with
| RRef _ | RVar _ | REvar _ | RPatVar _ -> rt
- | RLambda(loc,Anonymous,t,b) ->
+ | RLambda(loc,Anonymous,k,t,b) ->
let new_id = Nameops.next_ident_away (id_of_string "_x") excluded in
let new_excluded = new_id :: excluded in
let new_t = alpha_rt new_excluded t in
let new_b = alpha_rt new_excluded b in
- RLambda(loc,Name new_id,new_t,new_b)
- | RProd(loc,Anonymous,t,b) ->
+ RLambda(loc,Name new_id,k,new_t,new_b)
+ | RProd(loc,Anonymous,k,t,b) ->
let new_t = alpha_rt excluded t in
let new_b = alpha_rt excluded b in
- RProd(loc,Anonymous,new_t,new_b)
+ RProd(loc,Anonymous,k,new_t,new_b)
| RLetIn(loc,Anonymous,t,b) ->
let new_t = alpha_rt excluded t in
let new_b = alpha_rt excluded b in
RLetIn(loc,Anonymous,new_t,new_b)
- | RLambda(loc,Name id,t,b) ->
+ | RLambda(loc,Name id,k,t,b) ->
let new_id = Nameops.next_ident_away id excluded in
let t,b =
if new_id = id
@@ -255,8 +289,8 @@ let rec alpha_rt excluded rt =
let new_excluded = new_id::excluded in
let new_t = alpha_rt new_excluded t in
let new_b = alpha_rt new_excluded b in
- RLambda(loc,Name new_id,new_t,new_b)
- | RProd(loc,Name id,t,b) ->
+ RLambda(loc,Name new_id,k,new_t,new_b)
+ | RProd(loc,Name id,k,t,b) ->
let new_id = Nameops.next_ident_away id excluded in
let new_excluded = new_id::excluded in
let t,b =
@@ -268,7 +302,7 @@ let rec alpha_rt excluded rt =
in
let new_t = alpha_rt new_excluded t in
let new_b = alpha_rt new_excluded b in
- RProd(loc,Name new_id,new_t,new_b)
+ RProd(loc,Name new_id,k,new_t,new_b)
| RLetIn(loc,Name id,t,b) ->
let new_id = Nameops.next_ident_away id excluded in
let t,b =
@@ -306,20 +340,20 @@ let rec alpha_rt excluded rt =
if idmap_is_empty mapping
then rto,t,b
else let replace = change_vars mapping in
- (option_map replace rto, t,replace b)
+ (Option.map replace rto, t,replace b)
in
let new_t = alpha_rt new_excluded new_t in
let new_b = alpha_rt new_excluded new_b in
- let new_rto = option_map (alpha_rt new_excluded) new_rto in
+ let new_rto = Option.map (alpha_rt new_excluded) new_rto in
RLetTuple(loc,new_nal,(na,new_rto),new_t,new_b)
- | RCases(loc,infos,el,brl) ->
+ | RCases(loc,sty,infos,el,brl) ->
let new_el =
List.map (function (rt,i) -> alpha_rt excluded rt, i) el
in
- RCases(loc,infos,new_el,List.map (alpha_br excluded) brl)
+ RCases(loc,sty,infos,new_el,List.map (alpha_br excluded) brl)
| RIf(loc,b,(na,e_o),lhs,rhs) ->
RIf(loc,alpha_rt excluded b,
- (na,option_map (alpha_rt excluded) e_o),
+ (na,Option.map (alpha_rt excluded) e_o),
alpha_rt excluded lhs,
alpha_rt excluded rhs
)
@@ -357,17 +391,16 @@ let is_free_in id =
| REvar _ -> false
| RPatVar _ -> false
| RApp(_,rt,rtl) -> List.exists is_free_in (rt::rtl)
- | RLambda(_,n,t,b) | RProd(_,n,t,b) | RLetIn(_,n,t,b) ->
+ | RLambda(_,n,_,t,b) | RProd(_,n,_,t,b) | RLetIn(_,n,t,b) ->
let check_in_b =
match n with
| Name id' -> id_ord id' id <> 0
| _ -> true
in
is_free_in t || (check_in_b && is_free_in b)
- | RCases(_,_,el,brl) ->
+ | RCases(_,_,_,el,brl) ->
(List.exists (fun (e,_) -> is_free_in e) el) ||
List.exists is_free_in_br brl
-
| RLetTuple(_,nal,_,b,t) ->
let check_in_nal =
not (List.exists (function Name id' -> id'= id | _ -> false) nal)
@@ -428,17 +461,19 @@ let replace_var_by_term x_id term =
replace_var_by_pattern rt',
List.map replace_var_by_pattern rtl
)
- | RLambda(_,Name id,_,_) when id_ord id x_id == 0 -> rt
- | RLambda(loc,name,t,b) ->
+ | RLambda(_,Name id,_,_,_) when id_ord id x_id == 0 -> rt
+ | RLambda(loc,name,k,t,b) ->
RLambda(loc,
name,
+ k,
replace_var_by_pattern t,
replace_var_by_pattern b
)
- | RProd(_,Name id,_,_) when id_ord id x_id == 0 -> rt
- | RProd(loc,name,t,b) ->
+ | RProd(_,Name id,_,_,_) when id_ord id x_id == 0 -> rt
+ | RProd(loc,name,k,t,b) ->
RProd(loc,
name,
+ k,
replace_var_by_pattern t,
replace_var_by_pattern b
)
@@ -455,19 +490,19 @@ let replace_var_by_term x_id term =
| RLetTuple(loc,nal,(na,rto),def,b) ->
RLetTuple(loc,
nal,
- (na,option_map replace_var_by_pattern rto),
+ (na,Option.map replace_var_by_pattern rto),
replace_var_by_pattern def,
replace_var_by_pattern b
)
- | RCases(loc,infos,el,brl) ->
- RCases(loc,
+ | RCases(loc,sty,infos,el,brl) ->
+ RCases(loc,sty,
infos,
List.map (fun (e,x) -> (replace_var_by_pattern e,x)) el,
List.map replace_var_by_pattern_br brl
)
| RIf(loc,b,(na,e_option),lhs,rhs) ->
RIf(loc, replace_var_by_pattern b,
- (na,option_map replace_var_by_pattern e_option),
+ (na,Option.map replace_var_by_pattern e_option),
replace_var_by_pattern lhs,
replace_var_by_pattern rhs
)
@@ -558,15 +593,15 @@ let ids_of_rawterm c =
| RVar (_,id) -> id::acc
| RApp (loc,g,args) ->
ids_of_rawterm [] g @ List.flatten (List.map (ids_of_rawterm []) args) @ acc
- | RLambda (loc,na,ty,c) -> idof na :: ids_of_rawterm [] ty @ ids_of_rawterm [] c @ acc
- | RProd (loc,na,ty,c) -> idof na :: ids_of_rawterm [] ty @ ids_of_rawterm [] c @ acc
+ | RLambda (loc,na,k,ty,c) -> idof na :: ids_of_rawterm [] ty @ ids_of_rawterm [] c @ acc
+ | RProd (loc,na,k,ty,c) -> idof na :: ids_of_rawterm [] ty @ ids_of_rawterm [] c @ acc
| RLetIn (loc,na,b,c) -> idof na :: ids_of_rawterm [] b @ ids_of_rawterm [] c @ acc
| RCast (loc,c,CastConv(k,t)) -> ids_of_rawterm [] c @ ids_of_rawterm [] t @ acc
| RCast (loc,c,CastCoerce) -> ids_of_rawterm [] c @ acc
| RIf (loc,c,(na,po),b1,b2) -> ids_of_rawterm [] c @ ids_of_rawterm [] b1 @ ids_of_rawterm [] b2 @ acc
| RLetTuple (_,nal,(na,po),b,c) ->
List.map idof nal @ ids_of_rawterm [] b @ ids_of_rawterm [] c @ acc
- | RCases (loc,rtntypopt,tml,brchl) ->
+ | RCases (loc,sty,rtntypopt,tml,brchl) ->
List.flatten (List.map (fun (_,idl,patl,c) -> idl @ ids_of_rawterm [] c) brchl)
| RRec _ -> failwith "Fix inside a constructor branch"
| (RSort _ | RHole _ | RRef _ | REvar _ | RPatVar _ | RDynamic _) -> []
@@ -590,15 +625,17 @@ let zeta_normalize =
zeta_normalize_term rt',
List.map zeta_normalize_term rtl
)
- | RLambda(loc,name,t,b) ->
+ | RLambda(loc,name,k,t,b) ->
RLambda(loc,
name,
+ k,
zeta_normalize_term t,
zeta_normalize_term b
)
- | RProd(loc,name,t,b) ->
+ | RProd(loc,name,k,t,b) ->
RProd(loc,
- name,
+ name,
+ k,
zeta_normalize_term t,
zeta_normalize_term b
)
@@ -608,19 +645,19 @@ let zeta_normalize =
| RLetTuple(loc,nal,(na,rto),def,b) ->
RLetTuple(loc,
nal,
- (na,option_map zeta_normalize_term rto),
+ (na,Option.map zeta_normalize_term rto),
zeta_normalize_term def,
zeta_normalize_term b
)
- | RCases(loc,infos,el,brl) ->
- RCases(loc,
+ | RCases(loc,sty,infos,el,brl) ->
+ RCases(loc,sty,
infos,
List.map (fun (e,x) -> (zeta_normalize_term e,x)) el,
List.map zeta_normalize_br brl
)
| RIf(loc,b,(na,e_option),lhs,rhs) ->
RIf(loc, zeta_normalize_term b,
- (na,option_map zeta_normalize_term e_option),
+ (na,Option.map zeta_normalize_term e_option),
zeta_normalize_term lhs,
zeta_normalize_term rhs
)
@@ -659,24 +696,23 @@ let expand_as =
with Not_found -> rt
end
| RApp(loc,f,args) -> RApp(loc,expand_as map f,List.map (expand_as map) args)
- | RLambda(loc,na,t,b) -> RLambda(loc,na,expand_as map t, expand_as map b)
- | RProd(loc,na,t,b) -> RProd(loc,na,expand_as map t, expand_as map b)
+ | RLambda(loc,na,k,t,b) -> RLambda(loc,na,k,expand_as map t, expand_as map b)
+ | RProd(loc,na,k,t,b) -> RProd(loc,na,k,expand_as map t, expand_as map b)
| RLetIn(loc,na,v,b) -> RLetIn(loc,na, expand_as map v,expand_as map b)
| RLetTuple(loc,nal,(na,po),v,b) ->
- RLetTuple(loc,nal,(na,option_map (expand_as map) po),
+ RLetTuple(loc,nal,(na,Option.map (expand_as map) po),
expand_as map v, expand_as map b)
| RIf(loc,e,(na,po),br1,br2) ->
- RIf(loc,expand_as map e,(na,option_map (expand_as map) po),
+ RIf(loc,expand_as map e,(na,Option.map (expand_as map) po),
expand_as map br1, expand_as map br2)
| RRec _ -> error "Not handled RRec"
| RDynamic _ -> error "Not handled RDynamic"
| RCast(loc,b,CastConv(kind,t)) -> RCast(loc,expand_as map b,CastConv(kind,expand_as map t))
| RCast(loc,b,CastCoerce) -> RCast(loc,expand_as map b,CastCoerce)
- | RCases(loc,po,el,brl) ->
- RCases(loc, option_map (expand_as map) po, List.map (fun (rt,t) -> expand_as map rt,t) el,
+ | RCases(loc,sty,po,el,brl) ->
+ RCases(loc, sty, Option.map (expand_as map) po, List.map (fun (rt,t) -> expand_as map rt,t) el,
List.map (expand_as_br map) brl)
-
and expand_as_br map (loc,idl,cpl,rt) =
- (loc,idl,cpl, expand_as (List.fold_left add_as map cpl) rt)
+ (loc,idl,cpl, expand_as (List.fold_left add_as map cpl) rt)
in
expand_as Idmap.empty
diff --git a/contrib/funind/rawtermops.mli b/contrib/funind/rawtermops.mli
index 9647640c..358c6ba6 100644
--- a/contrib/funind/rawtermops.mli
+++ b/contrib/funind/rawtermops.mli
@@ -22,7 +22,7 @@ val mkRApp : rawconstr*(rawconstr list) -> rawconstr
val mkRLambda : Names.name*rawconstr*rawconstr -> rawconstr
val mkRProd : Names.name*rawconstr*rawconstr -> rawconstr
val mkRLetIn : Names.name*rawconstr*rawconstr -> rawconstr
-val mkRCases : rawconstr option * tomatch_tuple * cases_clauses -> rawconstr
+val mkRCases : rawconstr option * tomatch_tuples * cases_clauses -> rawconstr
val mkRSort : rawsort -> rawconstr
val mkRHole : unit -> rawconstr (* we only build Evd.BinderType Anonymous holes *)
val mkRCast : rawconstr* rawconstr -> rawconstr
@@ -31,8 +31,14 @@ val mkRCast : rawconstr* rawconstr -> rawconstr
These are analogous to the ones constrs
*)
val raw_decompose_prod : rawconstr -> (Names.name*rawconstr) list * rawconstr
+val raw_decompose_prod_or_letin :
+ rawconstr -> (Names.name*rawconstr option*rawconstr option) list * rawconstr
val raw_decompose_prod_n : int -> rawconstr -> (Names.name*rawconstr) list * rawconstr
+val raw_decompose_prod_or_letin_n : int -> rawconstr ->
+ (Names.name*rawconstr option*rawconstr option) list * rawconstr
val raw_compose_prod : rawconstr -> (Names.name*rawconstr) list -> rawconstr
+val raw_compose_prod_or_letin: rawconstr ->
+ (Names.name*rawconstr option*rawconstr option) list -> rawconstr
val raw_decompose_app : rawconstr -> rawconstr*(rawconstr list)
diff --git a/contrib/funind/recdef.ml b/contrib/funind/recdef.ml
new file mode 100644
index 00000000..c9bf2f1f
--- /dev/null
+++ b/contrib/funind/recdef.ml
@@ -0,0 +1,1430 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(*i camlp4deps: "parsing/grammar.cma" i*)
+
+(* $Id: recdef.ml 11094 2008-06-10 19:35:23Z herbelin $ *)
+
+open Term
+open Termops
+open Environ
+open Declarations
+open Entries
+open Pp
+open Names
+open Libnames
+open Nameops
+open Util
+open Closure
+open RedFlags
+open Tacticals
+open Typing
+open Tacmach
+open Tactics
+open Nametab
+open Decls
+open Declare
+open Decl_kinds
+open Tacred
+open Proof_type
+open Vernacinterp
+open Pfedit
+open Topconstr
+open Rawterm
+open Pretyping
+open Pretyping.Default
+open Safe_typing
+open Constrintern
+open Hiddentac
+
+open Equality
+open Auto
+open Eauto
+
+open Genarg
+
+
+let compute_renamed_type gls c =
+ rename_bound_var (pf_env gls) [] (pf_type_of gls c)
+
+let qed () = Command.save_named true
+let defined () = Command.save_named false
+
+let pf_get_new_ids idl g =
+ let ids = pf_ids_of_hyps g in
+ List.fold_right
+ (fun id acc -> next_global_ident_away false id (acc@ids)::acc)
+ idl
+ []
+
+let pf_get_new_id id g =
+ List.hd (pf_get_new_ids [id] g)
+
+let h_intros l =
+ tclMAP h_intro l
+
+let do_observe_tac s tac g =
+ let goal = begin (Printer.pr_goal (sig_it g)) end in
+ try let v = tac g in msgnl (goal ++ fnl () ++ (str "recdef ") ++
+ (str s)++(str " ")++(str "finished")); v
+ with e ->
+ msgnl (str "observation "++str s++str " raised exception " ++
+ Cerrors.explain_exn e ++ str " on goal " ++ goal );
+ raise e;;
+
+
+let observe_tac s tac g =
+ if Tacinterp.get_debug () <> Tactic_debug.DebugOff
+ then do_observe_tac s tac g
+ else tac g
+
+let hyp_ids = List.map id_of_string
+ ["x";"v";"k";"def";"p";"h";"n";"h'"; "anonymous"; "teq"; "rec_res";
+ "hspec";"heq"; "hrec"; "hex"; "teq"; "pmax";"hle"];;
+
+let rec nthtl = function
+ l, 0 -> l | _::tl, n -> nthtl (tl, n-1) | [], _ -> [];;
+
+let hyp_id n l = List.nth l n;;
+
+let (x_id:identifier) = hyp_id 0 hyp_ids;;
+let (v_id:identifier) = hyp_id 1 hyp_ids;;
+let (k_id:identifier) = hyp_id 2 hyp_ids;;
+let (def_id:identifier) = hyp_id 3 hyp_ids;;
+let (p_id:identifier) = hyp_id 4 hyp_ids;;
+let (h_id:identifier) = hyp_id 5 hyp_ids;;
+let (n_id:identifier) = hyp_id 6 hyp_ids;;
+let (h'_id:identifier) = hyp_id 7 hyp_ids;;
+let (ano_id:identifier) = hyp_id 8 hyp_ids;;
+let (rec_res_id:identifier) = hyp_id 10 hyp_ids;;
+let (hspec_id:identifier) = hyp_id 11 hyp_ids;;
+let (heq_id:identifier) = hyp_id 12 hyp_ids;;
+let (hrec_id:identifier) = hyp_id 13 hyp_ids;;
+let (hex_id:identifier) = hyp_id 14 hyp_ids;;
+let (teq_id:identifier) = hyp_id 15 hyp_ids;;
+let (pmax_id:identifier) = hyp_id 16 hyp_ids;;
+let (hle_id:identifier) = hyp_id 17 hyp_ids;;
+
+let message s = if Flags.is_verbose () then msgnl(str s);;
+
+let def_of_const t =
+ match (kind_of_term t) with
+ Const sp ->
+ (try (match (Global.lookup_constant sp) with
+ {const_body=Some c} -> Declarations.force c
+ |_ -> assert false)
+ with _ ->
+ anomaly ("Cannot find definition of constant "^
+ (string_of_id (id_of_label (con_label sp))))
+ )
+ |_ -> assert false
+
+let type_of_const t =
+ match (kind_of_term t) with
+ Const sp -> Typeops.type_of_constant (Global.env()) sp
+ |_ -> assert false
+
+let arg_type t =
+ match kind_of_term (def_of_const t) with
+ Lambda(a,b,c) -> b
+ | _ -> assert false;;
+
+let evaluable_of_global_reference r =
+ match r with
+ ConstRef sp -> EvalConstRef sp
+ | VarRef id -> EvalVarRef id
+ | _ -> assert false;;
+
+
+let rank_for_arg_list h =
+ let predicate a b =
+ try List.for_all2 eq_constr a b with
+ Invalid_argument _ -> false in
+ let rec rank_aux i = function
+ | [] -> None
+ | x::tl -> if predicate h x then Some i else rank_aux (i+1) tl in
+ rank_aux 0;;
+
+let rec (find_call_occs : int -> constr -> constr ->
+ (constr list -> constr) * constr list list) =
+ fun nb_lam f expr ->
+ match (kind_of_term expr) with
+ App (g, args) when g = f ->
+ (fun l -> List.hd l), [Array.to_list args]
+ | App (g, args) ->
+ let (largs: constr list) = Array.to_list args in
+ let rec find_aux = function
+ [] -> (fun x -> []), []
+ | a::upper_tl ->
+ (match find_aux upper_tl with
+ (cf, ((arg1::args) as args_for_upper_tl)) ->
+ (match find_call_occs nb_lam f a with
+ cf2, (_ :: _ as other_args) ->
+ let rec avoid_duplicates args =
+ match args with
+ | [] -> (fun _ -> []), []
+ | h::tl ->
+ let recomb_tl, args_for_tl =
+ avoid_duplicates tl in
+ match rank_for_arg_list h args_for_upper_tl with
+ | None ->
+ (fun l -> List.hd l::recomb_tl(List.tl l)),
+ h::args_for_tl
+ | Some i ->
+ (fun l -> List.nth l (i+List.length args_for_tl)::
+ recomb_tl l),
+ args_for_tl
+ in
+ let recombine, other_args' =
+ avoid_duplicates other_args in
+ let len1 = List.length other_args' in
+ (fun l -> cf2 (recombine l)::cf(nthtl(l,len1))),
+ other_args'@args_for_upper_tl
+ | _, [] -> (fun x -> a::cf x), args_for_upper_tl)
+ | _, [] ->
+ (match find_call_occs nb_lam f a with
+ cf, (arg1::args) -> (fun l -> cf l::upper_tl), (arg1::args)
+ | _, [] -> (fun x -> a::upper_tl), [])) in
+ begin
+ match (find_aux largs) with
+ cf, [] -> (fun l -> mkApp(g, args)), []
+ | cf, args ->
+ (fun l -> mkApp (g, Array.of_list (cf l))), args
+ end
+ | Rel(v) -> if v > nb_lam then error "find_call_occs : Rel" else ((fun l -> expr),[])
+ | Var(id) -> (fun l -> expr), []
+ | Meta(_) -> error "find_call_occs : Meta"
+ | Evar(_) -> error "find_call_occs : Evar"
+ | Sort(_) -> (fun l -> expr), []
+ | Cast(b,_,_) -> find_call_occs nb_lam f b
+ | Prod(_,_,_) -> error "find_call_occs : Prod"
+ | Lambda(na,t,b) ->
+ begin
+ match find_call_occs (succ nb_lam) f b with
+ | _, [] -> (* Lambda are authorized as long as they do not contain
+ recursives calls *)
+ (fun l -> expr),[]
+ | _ -> error "find_call_occs : Lambda"
+ end
+ | LetIn(na,v,t,b) ->
+ begin
+ match find_call_occs nb_lam f v, find_call_occs (succ nb_lam) f b with
+ | (_,[]),(_,[]) ->
+ ((fun l -> expr), [])
+ | (_,[]),(cf,(_::_ as l)) ->
+ ((fun l -> mkLetIn(na,v,t,cf l)),l)
+ | (cf,(_::_ as l)),(_,[]) ->
+ ((fun l -> mkLetIn(na,cf l,t,b)), l)
+ | _ -> error "find_call_occs : LetIn"
+ end
+ | Const(_) -> (fun l -> expr), []
+ | Ind(_) -> (fun l -> expr), []
+ | Construct (_, _) -> (fun l -> expr), []
+ | Case(i,t,a,r) ->
+ (match find_call_occs nb_lam f a with
+ cf, (arg1::args) -> (fun l -> mkCase(i, t, (cf l), r)),(arg1::args)
+ | _ -> (fun l -> expr),[])
+ | Fix(_) -> error "find_call_occs : Fix"
+ | CoFix(_) -> error "find_call_occs : CoFix";;
+
+let coq_constant s =
+ Coqlib.gen_constant_in_modules "RecursiveDefinition"
+ (Coqlib.init_modules @ Coqlib.arith_modules) s;;
+
+let constant sl s =
+ constr_of_global
+ (locate (make_qualid(Names.make_dirpath
+ (List.map id_of_string (List.rev sl)))
+ (id_of_string s)));;
+
+let find_reference sl s =
+ (locate (make_qualid(Names.make_dirpath
+ (List.map id_of_string (List.rev sl)))
+ (id_of_string s)));;
+
+let delayed_force f = f ()
+
+let le_lt_SS = function () -> (constant ["Recdef"] "le_lt_SS")
+let le_lt_n_Sm = function () -> (coq_constant "le_lt_n_Sm")
+
+let le_trans = function () -> (coq_constant "le_trans")
+let le_lt_trans = function () -> (coq_constant "le_lt_trans")
+let lt_S_n = function () -> (coq_constant "lt_S_n")
+let le_n = function () -> (coq_constant "le_n")
+let refl_equal = function () -> (coq_constant "refl_equal")
+let eq = function () -> (coq_constant "eq")
+let ex = function () -> (coq_constant "ex")
+let coq_sig_ref = function () -> (find_reference ["Coq";"Init";"Specif"] "sig")
+let coq_sig = function () -> (coq_constant "sig")
+let coq_O = function () -> (coq_constant "O")
+let coq_S = function () -> (coq_constant "S")
+
+let gt_antirefl = function () -> (coq_constant "gt_irrefl")
+let lt_n_O = function () -> (coq_constant "lt_n_O")
+let lt_n_Sn = function () -> (coq_constant "lt_n_Sn")
+
+let f_equal = function () -> (coq_constant "f_equal")
+let well_founded_induction = function () -> (coq_constant "well_founded_induction")
+let well_founded = function () -> (coq_constant "well_founded")
+let acc_rel = function () -> (coq_constant "Acc")
+let acc_inv_id = function () -> (coq_constant "Acc_inv")
+let well_founded_ltof = function () -> (Coqlib.coq_constant "" ["Arith";"Wf_nat"] "well_founded_ltof")
+let iter_ref = function () -> (try find_reference ["Recdef"] "iter" with Not_found -> error "module Recdef not loaded")
+let max_ref = function () -> (find_reference ["Recdef"] "max")
+let iter = function () -> (constr_of_global (delayed_force iter_ref))
+let max_constr = function () -> (constr_of_global (delayed_force max_ref))
+
+let ltof_ref = function () -> (find_reference ["Coq";"Arith";"Wf_nat"] "ltof")
+let coq_conj = function () -> find_reference ["Coq";"Init";"Logic"] "conj"
+
+(* These are specific to experiments in nat with lt as well_founded_relation, *)
+(* but this should be made more general. *)
+let nat = function () -> (coq_constant "nat")
+let lt = function () -> (coq_constant "lt")
+
+(* This is simply an implementation of the case_eq tactic. this code
+ should be replaced with the tactic defined in Ltac in Init/Tactics.v *)
+let mkCaseEq a : tactic =
+ (fun g ->
+ let type_of_a = pf_type_of g a in
+ tclTHENLIST
+ [h_generalize [mkApp(delayed_force refl_equal, [| type_of_a; a|])];
+ (fun g2 ->
+ change_in_concl None
+ (pattern_occs [((false,[1]), a)] (pf_env g2) Evd.empty (pf_concl g2))
+ g2);
+ simplest_case a] g);;
+
+(* This is like the previous one except that it also rewrite on all
+ hypotheses except the ones given in the first argument. All the
+ modified hypotheses are generalized in the process and should be
+ introduced back later; the result is the pair of the tactic and the
+ list of hypotheses that have been generalized and cleared. *)
+let mkDestructEq :
+ identifier list -> constr -> goal sigma -> tactic * identifier list =
+ fun not_on_hyp expr g ->
+ let hyps = pf_hyps g in
+ let to_revert =
+ Util.map_succeed
+ (fun (id,_,t) ->
+ if List.mem id not_on_hyp || not (Termops.occur_term expr t)
+ then failwith "is_expr_context";
+ id) hyps in
+ let to_revert_constr = List.rev_map mkVar to_revert in
+ let type_of_expr = pf_type_of g expr in
+ let new_hyps = mkApp(delayed_force refl_equal, [|type_of_expr; expr|])::
+ to_revert_constr in
+ tclTHENLIST
+ [h_generalize new_hyps;
+ (fun g2 ->
+ change_in_concl None
+ (pattern_occs [((false,[1]), expr)] (pf_env g2) Evd.empty (pf_concl g2)) g2);
+ simplest_case expr], to_revert
+
+let rec mk_intros_and_continue thin_intros (extra_eqn:bool)
+ cont_function (eqs:constr list) nb_lam (expr:constr) g =
+ let finalize () = if extra_eqn then
+ let teq = pf_get_new_id teq_id g in
+ tclTHENLIST
+ [ h_intro teq;
+ thin thin_intros;
+ h_intros thin_intros;
+
+ tclMAP
+ (fun eq -> tclTRY (Equality.general_rewrite_in true all_occurrences teq eq false))
+ (List.rev eqs);
+ (fun g1 ->
+ let ty_teq = pf_type_of g1 (mkVar teq) in
+ let teq_lhs,teq_rhs =
+ let _,args = try destApp ty_teq with _ -> Pp.msgnl (Printer.pr_goal (sig_it g1) ++ fnl () ++ pr_id teq ++ str ":" ++ Printer.pr_lconstr ty_teq); assert false in
+ args.(1),args.(2)
+ in
+ cont_function (mkVar teq::eqs) (replace_term teq_lhs teq_rhs expr) g1
+ )
+ ]
+ g
+ else
+ tclTHENSEQ[
+ thin thin_intros;
+ h_intros thin_intros;
+ cont_function eqs expr
+ ] g
+ in
+ if nb_lam = 0
+ then finalize ()
+ else
+ match kind_of_term expr with
+ | Lambda (n, _, b) ->
+ let n1 =
+ match n with
+ Name x -> x
+ | Anonymous -> ano_id
+ in
+ let new_n = pf_get_new_id n1 g in
+ tclTHEN (h_intro new_n)
+ (mk_intros_and_continue thin_intros extra_eqn cont_function eqs
+ (pred nb_lam) (subst1 (mkVar new_n) b)) g
+ | _ ->
+ assert false
+(* finalize () *)
+let const_of_ref = function
+ ConstRef kn -> kn
+ | _ -> anomaly "ConstRef expected"
+
+let simpl_iter clause =
+ reduce
+ (Lazy
+ {rBeta=true;rIota=true;rZeta= true; rDelta=false;
+ rConst = [ EvalConstRef (const_of_ref (delayed_force iter_ref))]})
+(* (Simpl (Some ([],mkConst (const_of_ref (delayed_force iter_ref))))) *)
+ clause
+
+(* The boolean value is_mes expresses that the termination is expressed
+ using a measure function instead of a well-founded relation. *)
+let tclUSER tac is_mes l g =
+ let clear_tac =
+ match l with
+ | None -> h_clear true []
+ | Some l -> tclMAP (fun id -> tclTRY (h_clear false [id])) (List.rev l)
+ in
+ tclTHENSEQ
+ [
+ clear_tac;
+ if is_mes
+ then tclTHEN
+ (unfold_in_concl [(all_occurrences, evaluable_of_global_reference
+ (delayed_force ltof_ref))])
+ tac
+ else tac
+ ]
+ g
+
+
+let list_rewrite (rev:bool) (eqs: constr list) =
+ tclREPEAT
+ (List.fold_right
+ (fun eq i -> tclORELSE (rewriteLR eq) i)
+ (if rev then (List.rev eqs) else eqs) (tclFAIL 0 (mt())));;
+
+let base_leaf_terminate (func:global_reference) eqs expr =
+(* let _ = msgnl (str "entering base_leaf") in *)
+ (fun g ->
+ let k',h =
+ match pf_get_new_ids [k_id;h_id] g with
+ [k';h] -> k',h
+ | _ -> assert false
+ in
+ tclTHENLIST
+ [observe_tac "first split" (split (ImplicitBindings [expr]));
+ observe_tac "second split"
+ (split (ImplicitBindings [delayed_force coq_O]));
+ observe_tac "intro k" (h_intro k');
+ observe_tac "case on k"
+ (tclTHENS (simplest_case (mkVar k'))
+ [(tclTHEN (h_intro h)
+ (tclTHEN (simplest_elim (mkApp (delayed_force gt_antirefl,
+ [| delayed_force coq_O |])))
+ default_auto)); tclIDTAC ]);
+ intros;
+ simpl_iter onConcl;
+ unfold_constr func;
+ list_rewrite true eqs;
+ default_auto] g);;
+
+(* La fonction est donnee en premier argument a la
+ fonctionnelle suivie d'autres Lambdas et de Case ...
+ Pour recuperer la fonction f a partir de la
+ fonctionnelle *)
+
+let get_f foncl =
+ match (kind_of_term (def_of_const foncl)) with
+ Lambda (Name f, _, _) -> f
+ |_ -> error "la fonctionnelle est mal definie";;
+
+
+let rec compute_le_proofs = function
+ [] -> assumption
+ | a::tl ->
+ tclORELSE assumption
+ (tclTHENS
+ (fun g ->
+ let le_trans = delayed_force le_trans in
+ let t_le_trans = compute_renamed_type g le_trans in
+ let m_id =
+ let _,_,t = destProd t_le_trans in
+ let na,_,_ = destProd t in
+ Nameops.out_name na
+ in
+ apply_with_bindings
+ (le_trans,
+ ExplicitBindings[dummy_loc,NamedHyp m_id,a])
+ g)
+ [compute_le_proofs tl;
+ tclORELSE (apply (delayed_force le_n)) assumption])
+
+let make_lt_proof pmax le_proof =
+ tclTHENS
+ (fun g ->
+ let le_lt_trans = delayed_force le_lt_trans in
+ let t_le_lt_trans = compute_renamed_type g le_lt_trans in
+ let m_id =
+ let _,_,t = destProd t_le_lt_trans in
+ let na,_,_ = destProd t in
+ Nameops.out_name na
+ in
+ apply_with_bindings
+ (le_lt_trans,
+ ExplicitBindings[dummy_loc,NamedHyp m_id, pmax]) g)
+ [observe_tac "compute_le_proofs" (compute_le_proofs le_proof);
+ tclTHENLIST[observe_tac "lt_S_n" (apply (delayed_force lt_S_n)); default_full_auto]];;
+
+let rec list_cond_rewrite k def pmax cond_eqs le_proofs =
+ match cond_eqs with
+ [] -> tclIDTAC
+ | eq::eqs ->
+ (fun g ->
+ let t_eq = compute_renamed_type g (mkVar eq) in
+ let k_id,def_id =
+ let k_na,_,t = destProd t_eq in
+ let _,_,t = destProd t in
+ let def_na,_,_ = destProd t in
+ Nameops.out_name k_na,Nameops.out_name def_na
+ in
+ tclTHENS
+ (general_rewrite_bindings false all_occurrences
+ (mkVar eq,
+ ExplicitBindings[dummy_loc, NamedHyp k_id, mkVar k;
+ dummy_loc, NamedHyp def_id, mkVar def]) false)
+ [list_cond_rewrite k def pmax eqs le_proofs;
+ observe_tac "make_lt_proof" (make_lt_proof pmax le_proofs)] g
+ )
+
+let rec introduce_all_equalities func eqs values specs bound le_proofs
+ cond_eqs =
+ match specs with
+ [] ->
+ fun g ->
+ let ids = pf_ids_of_hyps g in
+ let s_max = mkApp(delayed_force coq_S, [|bound|]) in
+ let k = next_global_ident_away true k_id ids in
+ let ids = k::ids in
+ let h' = next_global_ident_away true (h'_id) ids in
+ let ids = h'::ids in
+ let def = next_global_ident_away true def_id ids in
+ tclTHENLIST
+ [observe_tac "introduce_all_equalities_final split" (split (ImplicitBindings [s_max]));
+ observe_tac "introduce_all_equalities_final intro k" (h_intro k);
+ tclTHENS
+ (observe_tac "introduce_all_equalities_final case k" (simplest_case (mkVar k)))
+ [
+ tclTHENLIST[h_intro h';
+ simplest_elim(mkApp(delayed_force lt_n_O,[|s_max|]));
+ default_full_auto];
+ tclIDTAC
+ ];
+ observe_tac "clearing k " (clear [k]);
+ observe_tac "intros k h' def" (h_intros [k;h';def]);
+ observe_tac "simple_iter" (simpl_iter onConcl);
+ observe_tac "unfold functional"
+ (unfold_in_concl[((true,[1]),evaluable_of_global_reference func)]);
+ observe_tac "rewriting equations"
+ (list_rewrite true eqs);
+ observe_tac ("cond rewrite "^(string_of_id k)) (list_cond_rewrite k def bound cond_eqs le_proofs);
+ observe_tac "refl equal" (apply (delayed_force refl_equal))] g
+ | spec1::specs ->
+ fun g ->
+ let ids = ids_of_named_context (pf_hyps g) in
+ let p = next_global_ident_away true p_id ids in
+ let ids = p::ids in
+ let pmax = next_global_ident_away true pmax_id ids in
+ let ids = pmax::ids in
+ let hle1 = next_global_ident_away true hle_id ids in
+ let ids = hle1::ids in
+ let hle2 = next_global_ident_away true hle_id ids in
+ let ids = hle2::ids in
+ let heq = next_global_ident_away true heq_id ids in
+ tclTHENLIST
+ [simplest_elim (mkVar spec1);
+ list_rewrite true eqs;
+ h_intros [p; heq];
+ simplest_elim (mkApp(delayed_force max_constr, [| bound; mkVar p|]));
+ h_intros [pmax; hle1; hle2];
+ introduce_all_equalities func eqs values specs
+ (mkVar pmax) ((mkVar pmax)::le_proofs)
+ (heq::cond_eqs)] g;;
+
+let string_match s =
+ if String.length s < 3 then failwith "string_match";
+ try
+ for i = 0 to 3 do
+ if String.get s i <> String.get "Acc_" i then failwith "string_match"
+ done;
+ with Invalid_argument _ -> failwith "string_match"
+
+let retrieve_acc_var g =
+ (* Julien: I don't like this version .... *)
+ let hyps = pf_ids_of_hyps g in
+ map_succeed
+ (fun id -> string_match (string_of_id id);id)
+ hyps
+
+let rec introduce_all_values concl_tac is_mes acc_inv func context_fn
+ eqs hrec args values specs =
+ (match args with
+ [] ->
+ tclTHENLIST
+ [observe_tac "split" (split(ImplicitBindings
+ [context_fn (List.map mkVar (List.rev values))]));
+ observe_tac "introduce_all_equalities" (introduce_all_equalities func eqs
+ (List.rev values) (List.rev specs) (delayed_force coq_O) [] [])]
+ | arg::args ->
+ (fun g ->
+ let ids = ids_of_named_context (pf_hyps g) in
+ let rec_res = next_global_ident_away true rec_res_id ids in
+ let ids = rec_res::ids in
+ let hspec = next_global_ident_away true hspec_id ids in
+ let tac =
+ observe_tac "introduce_all_values" (
+ introduce_all_values concl_tac is_mes acc_inv func context_fn eqs
+ hrec args
+ (rec_res::values)(hspec::specs)) in
+ (tclTHENS
+ (observe_tac "elim h_rec"
+ (simplest_elim (mkApp(mkVar hrec, Array.of_list arg)))
+ )
+ [tclTHENLIST [h_intros [rec_res; hspec];
+ tac];
+ (tclTHENS
+ (observe_tac "acc_inv" (apply (Lazy.force acc_inv)))
+ [(* tclTHEN (tclTRY(list_rewrite true eqs)) *)
+ (observe_tac "h_assumption" h_assumption)
+ ;
+ tclTHENLIST
+ [
+ tclTRY(list_rewrite true eqs);
+ observe_tac "user proof"
+ (fun g ->
+ tclUSER
+ concl_tac
+ is_mes
+ (Some (hrec::hspec::(retrieve_acc_var g)@specs))
+ g
+ )
+ ]
+ ]
+ )
+ ]) g)
+
+ )
+
+
+let rec_leaf_terminate f_constr concl_tac is_mes acc_inv hrec (func:global_reference) eqs expr =
+ match find_call_occs 0 f_constr expr with
+ | context_fn, args ->
+ observe_tac "introduce_all_values"
+ (introduce_all_values concl_tac is_mes acc_inv func context_fn eqs hrec args [] [])
+
+let proveterminate rec_arg_id is_mes acc_inv (hrec:identifier)
+ (f_constr:constr) (func:global_reference) base_leaf rec_leaf =
+ let rec proveterminate (eqs:constr list) (expr:constr) =
+ try
+ (* let _ = msgnl (str "entering proveterminate") in *)
+ let v =
+ match (kind_of_term expr) with
+ Case (ci, t, a, l) ->
+ (match find_call_occs 0 f_constr a with
+ _,[] ->
+ (fun g ->
+ let destruct_tac, rev_to_thin_intro =
+ mkDestructEq rec_arg_id a g in
+ tclTHENS destruct_tac
+ (list_map_i
+ (fun i -> mk_intros_and_continue
+ (List.rev rev_to_thin_intro)
+ true
+ proveterminate
+ eqs
+ ci.ci_cstr_nargs.(i))
+ 0 (Array.to_list l)) g)
+ | _, _::_ ->
+ (match find_call_occs 0 f_constr expr with
+ _,[] -> observe_tac "base_leaf" (base_leaf func eqs expr)
+ | _, _:: _ ->
+ observe_tac "rec_leaf"
+ (rec_leaf is_mes acc_inv hrec func eqs expr)))
+ | _ ->
+ (match find_call_occs 0 f_constr expr with
+ _,[] ->
+ (try observe_tac "base_leaf" (base_leaf func eqs expr)
+ with e -> (msgerrnl (str "failure in base case");raise e ))
+ | _, _::_ ->
+ observe_tac "rec_leaf"
+ (rec_leaf is_mes acc_inv hrec func eqs expr)) in
+ v
+ with e -> begin msgerrnl(str "failure in proveterminate"); raise e end
+ in
+ proveterminate
+
+let hyp_terminates nb_args func =
+ let a_arrow_b = arg_type (constr_of_global func) in
+ let rev_args,b = decompose_prod_n nb_args a_arrow_b in
+ let left =
+ mkApp(delayed_force iter,
+ Array.of_list
+ (lift 5 a_arrow_b:: mkRel 3::
+ constr_of_global func::mkRel 1::
+ List.rev (list_map_i (fun i _ -> mkRel (6+i)) 0 rev_args)
+ )
+ )
+ in
+ let right = mkRel 5 in
+ let equality = mkApp(delayed_force eq, [|lift 5 b; left; right|]) in
+ let result = (mkProd ((Name def_id) , lift 4 a_arrow_b, equality)) in
+ let cond = mkApp(delayed_force lt, [|(mkRel 2); (mkRel 1)|]) in
+ let nb_iter =
+ mkApp(delayed_force ex,
+ [|delayed_force nat;
+ (mkLambda
+ (Name
+ p_id,
+ delayed_force nat,
+ (mkProd (Name k_id, delayed_force nat,
+ mkArrow cond result))))|])in
+ let value = mkApp(delayed_force coq_sig,
+ [|b;
+ (mkLambda (Name v_id, b, nb_iter))|]) in
+ compose_prod rev_args value
+
+
+
+let tclUSER_if_not_mes concl_tac is_mes names_to_suppress =
+ if is_mes
+ then tclCOMPLETE (h_simplest_apply (delayed_force well_founded_ltof))
+ else tclUSER concl_tac is_mes names_to_suppress
+
+let termination_proof_header is_mes input_type ids args_id relation
+ rec_arg_num rec_arg_id tac wf_tac : tactic =
+ begin
+ fun g ->
+ let nargs = List.length args_id in
+ let pre_rec_args =
+ List.rev_map
+ mkVar (fst (list_chop (rec_arg_num - 1) args_id))
+ in
+ let relation = substl pre_rec_args relation in
+ let input_type = substl pre_rec_args input_type in
+ let wf_thm = next_global_ident_away true (id_of_string ("wf_R")) ids in
+ let wf_rec_arg =
+ next_global_ident_away true
+ (id_of_string ("Acc_"^(string_of_id rec_arg_id)))
+ (wf_thm::ids)
+ in
+ let hrec = next_global_ident_away true hrec_id
+ (wf_rec_arg::wf_thm::ids) in
+ let acc_inv =
+ lazy (
+ mkApp (
+ delayed_force acc_inv_id,
+ [|input_type;relation;mkVar rec_arg_id|]
+ )
+ )
+ in
+ tclTHEN
+ (h_intros args_id)
+ (tclTHENS
+ (observe_tac
+ "first assert"
+ (assert_tac
+ true (* the assert thm is in first subgoal *)
+ (Name wf_rec_arg)
+ (mkApp (delayed_force acc_rel,
+ [|input_type;relation;mkVar rec_arg_id|])
+ )
+ )
+ )
+ [
+ (* accesibility proof *)
+ tclTHENS
+ (observe_tac
+ "second assert"
+ (assert_tac
+ true
+ (Name wf_thm)
+ (mkApp (delayed_force well_founded,[|input_type;relation|]))
+ )
+ )
+ [
+ (* interactive proof that the relation is well_founded *)
+ observe_tac "wf_tac" (wf_tac is_mes (Some args_id));
+ (* this gives the accessibility argument *)
+ observe_tac
+ "apply wf_thm"
+ (h_simplest_apply (mkApp(mkVar wf_thm,[|mkVar rec_arg_id|]))
+ )
+ ]
+ ;
+ (* rest of the proof *)
+ tclTHENSEQ
+ [observe_tac "generalize"
+ (onNLastHyps (nargs+1)
+ (fun (id,_,_) ->
+ tclTHEN (h_generalize [mkVar id]) (h_clear false [id])
+ ))
+ ;
+ observe_tac "h_fix" (h_fix (Some hrec) (nargs+1));
+ h_intros args_id;
+ h_intro wf_rec_arg;
+ observe_tac "tac" (tac wf_rec_arg hrec acc_inv)
+ ]
+ ]
+ ) g
+ end
+
+
+
+let rec instantiate_lambda t l =
+ match l with
+ | [] -> t
+ | a::l ->
+ let (bound_name, _, body) = destLambda t in
+ instantiate_lambda (subst1 a body) l
+;;
+
+
+let whole_start (concl_tac:tactic) nb_args is_mes func input_type relation rec_arg_num : tactic =
+ begin
+ fun g ->
+ let ids = ids_of_named_context (pf_hyps g) in
+ let func_body = (def_of_const (constr_of_global func)) in
+ let (f_name, _, body1) = destLambda func_body in
+ let f_id =
+ match f_name with
+ | Name f_id -> next_global_ident_away true f_id ids
+ | Anonymous -> anomaly "Anonymous function"
+ in
+ let n_names_types,_ = decompose_lam_n nb_args body1 in
+ let n_ids,ids =
+ List.fold_left
+ (fun (n_ids,ids) (n_name,_) ->
+ match n_name with
+ | Name id ->
+ let n_id = next_global_ident_away true id ids in
+ n_id::n_ids,n_id::ids
+ | _ -> anomaly "anonymous argument"
+ )
+ ([],(f_id::ids))
+ n_names_types
+ in
+ let rec_arg_id = List.nth n_ids (rec_arg_num - 1) in
+ let expr = instantiate_lambda func_body (mkVar f_id::(List.map mkVar n_ids)) in
+ termination_proof_header
+ is_mes
+ input_type
+ ids
+ n_ids
+ relation
+ rec_arg_num
+ rec_arg_id
+ (fun rec_arg_id hrec acc_inv g ->
+ (proveterminate
+ [rec_arg_id]
+ is_mes
+ acc_inv
+ hrec
+ (mkVar f_id)
+ func
+ base_leaf_terminate
+ (rec_leaf_terminate (mkVar f_id) concl_tac)
+ []
+ expr
+ )
+ g
+ )
+ (tclUSER_if_not_mes concl_tac)
+ g
+ end
+
+let get_current_subgoals_types () =
+ let pts = get_pftreestate () in
+ let _,subs = extract_open_pftreestate pts in
+ List.map snd ((* List.sort (fun (x,_) (y,_) -> x -y ) *)subs )
+
+let build_and_l l =
+ let and_constr = Coqlib.build_coq_and () in
+ let conj_constr = coq_conj () in
+ let mk_and p1 p2 =
+ Term.mkApp(and_constr,[|p1;p2|]) in
+ let rec f = function
+ | [] -> failwith "empty list of subgoals!"
+ | [p] -> p,tclIDTAC,1
+ | p1::pl ->
+ let c,tac,nb = f pl in
+ mk_and p1 c,
+ tclTHENS
+ (apply (constr_of_global conj_constr))
+ [tclIDTAC;
+ tac
+ ],nb+1
+ in f l
+
+
+let is_rec_res id =
+ let rec_res_name = string_of_id rec_res_id in
+ let id_name = string_of_id id in
+ try
+ String.sub id_name 0 (String.length rec_res_name) = rec_res_name
+ with _ -> false
+
+let clear_goals =
+ let rec clear_goal t =
+ match kind_of_term t with
+ | Prod(Name id as na,t,b) ->
+ let b' = clear_goal b in
+ if noccurn 1 b' && (is_rec_res id)
+ then pop b'
+ else if b' == b then t
+ else mkProd(na,t,b')
+ | _ -> map_constr clear_goal t
+ in
+ List.map clear_goal
+
+
+let build_new_goal_type () =
+ let sub_gls_types = get_current_subgoals_types () in
+ let sub_gls_types = clear_goals sub_gls_types in
+ let res = build_and_l sub_gls_types in
+ res
+
+
+ (*
+let prove_with_tcc lemma _ : tactic =
+ fun gls ->
+ let hid = next_global_ident_away true h_id (pf_ids_of_hyps gls) in
+ tclTHENSEQ
+ [
+ h_generalize [lemma];
+ h_intro hid;
+ Elim.h_decompose_and (mkVar hid);
+ gen_eauto(* default_eauto *) false (false,5) [] (Some [])
+ (* default_auto *)
+ ]
+ gls
+ *)
+
+
+
+let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_name (gls_type,decompose_and_tac,nb_goal) =
+ let current_proof_name = get_current_proof_name () in
+ let name = match goal_name with
+ | Some s -> s
+ | None ->
+ try (add_suffix current_proof_name "_subproof")
+ with _ -> anomaly "open_new_goal with an unamed theorem"
+ in
+ let sign = Global.named_context () in
+ let sign = clear_proofs sign in
+ let na = next_global_ident_away false name [] in
+ if occur_existential gls_type then
+ Util.error "\"abstract\" cannot handle existentials";
+ let hook _ _ =
+ let opacity =
+ let na_ref = Libnames.Ident (dummy_loc,na) in
+ let na_global = Nametab.global na_ref in
+ match na_global with
+ ConstRef c ->
+ let cb = Global.lookup_constant c in
+ if cb.Declarations.const_opaque then true
+ else begin match cb.const_body with None -> true | _ -> false end
+ | _ -> anomaly "equation_lemma: not a constant"
+ in
+ let lemma = mkConst (Lib.make_con na) in
+ ref_ := Some lemma ;
+ let lid = ref [] in
+ let h_num = ref (-1) in
+ Flags.silently Vernacentries.interp (Vernacexpr.VernacAbort None);
+ build_proof
+ ( fun gls ->
+ let hid = next_global_ident_away true h_id (pf_ids_of_hyps gls) in
+ tclTHENSEQ
+ [
+ h_generalize [lemma];
+ h_intro hid;
+ (fun g ->
+ let ids = pf_ids_of_hyps g in
+ tclTHEN
+ (Elim.h_decompose_and (mkVar hid))
+ (fun g ->
+ let ids' = pf_ids_of_hyps g in
+ lid := List.rev (list_subtract ids' ids);
+ if !lid = [] then lid := [hid];
+(* list_iter_i *)
+(* (fun i v -> *)
+(* msgnl (str "hyp" ++ int i ++ str " " ++ *)
+(* Nameops.pr_id v ++ fnl () ++ fnl())) *)
+(* !lid; *)
+ tclIDTAC g
+ )
+ g
+ );
+ ] gls)
+ (fun g ->
+ match kind_of_term (pf_concl g) with
+ | App(f,_) when eq_constr f (well_founded ()) ->
+ Auto.h_auto None [] (Some []) g
+ | _ ->
+ incr h_num;
+ tclTHEN
+ (eapply_with_bindings (mkVar (List.nth !lid !h_num), NoBindings))
+ e_assumption
+ g)
+;
+ Command.save_named opacity;
+ in
+ start_proof
+ na
+ (Decl_kinds.Global, Decl_kinds.Proof Decl_kinds.Lemma)
+ sign
+ gls_type
+ hook ;
+ by (
+ fun g ->
+ tclTHEN
+ (decompose_and_tac)
+ (tclORELSE
+ (tclFIRST
+ (List.map
+ (fun c ->
+ tclTHENSEQ
+ [intros;
+ h_simplest_apply (interp_constr Evd.empty (Global.env()) c);
+ tclCOMPLETE Auto.default_auto
+ ]
+ )
+ using_lemmas)
+ ) tclIDTAC)
+ g);
+ try
+ by tclIDTAC; (* raises UserError _ if the proof is complete *)
+ if Flags.is_verbose () then (pp (Printer.pr_open_subgoals()))
+ with UserError _ ->
+ defined ()
+
+;;
+
+
+let com_terminate
+ tcc_lemma_name
+ tcc_lemma_ref
+ is_mes
+ fonctional_ref
+ input_type
+ relation
+ rec_arg_num
+ thm_name using_lemmas
+ nb_args
+ hook =
+ let start_proof (tac_start:tactic) (tac_end:tactic) =
+ let (evmap, env) = Command.get_current_context() in
+ start_proof thm_name
+ (Global, Proof Lemma) (Environ.named_context_val env)
+ (hyp_terminates nb_args fonctional_ref) hook;
+ by (observe_tac "starting_tac" tac_start);
+ by (observe_tac "whole_start" (whole_start tac_end nb_args is_mes fonctional_ref
+ input_type relation rec_arg_num ))
+
+ in
+ start_proof tclIDTAC tclIDTAC;
+ try
+ let new_goal_type = build_new_goal_type () in
+ open_new_goal start_proof using_lemmas tcc_lemma_ref
+ (Some tcc_lemma_name)
+ (new_goal_type)
+ with Failure "empty list of subgoals!" ->
+ (* a non recursive function declared with measure ! *)
+ defined ()
+
+
+
+
+let ind_of_ref = function
+ | IndRef (ind,i) -> (ind,i)
+ | _ -> anomaly "IndRef expected"
+
+let (value_f:constr list -> global_reference -> constr) =
+ fun al fterm ->
+ let d0 = dummy_loc in
+ let rev_x_id_l =
+ (
+ List.fold_left
+ (fun x_id_l _ ->
+ let x_id = next_global_ident_away true x_id x_id_l in
+ x_id::x_id_l
+ )
+ []
+ al
+ )
+ in
+ let fun_body =
+ RCases
+ (d0,RegularStyle,None,
+ [RApp(d0, RRef(d0,fterm), List.rev_map (fun x_id -> RVar(d0, x_id)) rev_x_id_l),
+ (Anonymous,None)],
+ [d0, [v_id], [PatCstr(d0,(ind_of_ref
+ (delayed_force coq_sig_ref),1),
+ [PatVar(d0, Name v_id);
+ PatVar(d0, Anonymous)],
+ Anonymous)],
+ RVar(d0,v_id)])
+ in
+ let value =
+ List.fold_left2
+ (fun acc x_id a ->
+ RLambda
+ (d0, Name x_id, Explicit, RDynamic(d0, constr_in a),
+ acc
+ )
+ )
+ fun_body
+ rev_x_id_l
+ (List.rev al)
+ in
+ understand Evd.empty (Global.env()) value;;
+
+let (declare_fun : identifier -> logical_kind -> constr -> global_reference) =
+ fun f_id kind value ->
+ let ce = {const_entry_body = value;
+ const_entry_type = None;
+ const_entry_opaque = false;
+ const_entry_boxed = true} in
+ ConstRef(declare_constant f_id (DefinitionEntry ce, kind));;
+
+let (declare_f : identifier -> logical_kind -> constr list -> global_reference -> global_reference) =
+ fun f_id kind input_type fterm_ref ->
+ declare_fun f_id kind (value_f input_type fterm_ref);;
+
+let rec n_x_id ids n =
+ if n = 0 then []
+ else let x = next_global_ident_away true x_id ids in
+ x::n_x_id (x::ids) (n-1);;
+
+let start_equation (f:global_reference) (term_f:global_reference)
+ (cont_tactic:identifier list -> tactic) g =
+ let ids = pf_ids_of_hyps g in
+ let terminate_constr = constr_of_global term_f in
+ let nargs = nb_prod (type_of_const terminate_constr) in
+ let x = n_x_id ids nargs in
+ tclTHENLIST [
+ h_intros x;
+ unfold_in_concl [(all_occurrences, evaluable_of_global_reference f)];
+ observe_tac "simplest_case"
+ (simplest_case (mkApp (terminate_constr,
+ Array.of_list (List.map mkVar x))));
+ observe_tac "prove_eq" (cont_tactic x)] g;;
+
+let base_leaf_eq func eqs f_id g =
+ let ids = pf_ids_of_hyps g in
+ let k = next_global_ident_away true k_id ids in
+ let p = next_global_ident_away true p_id (k::ids) in
+ let v = next_global_ident_away true v_id (p::k::ids) in
+ let heq = next_global_ident_away true heq_id (v::p::k::ids) in
+ let heq1 = next_global_ident_away true heq_id (heq::v::p::k::ids) in
+ let hex = next_global_ident_away true hex_id (heq1::heq::v::p::k::ids) in
+ tclTHENLIST [
+ h_intros [v; hex];
+ simplest_elim (mkVar hex);
+ h_intros [p;heq1];
+ tclTRY
+ (rewriteRL
+ (mkApp(mkVar heq1,
+ [|mkApp (delayed_force coq_S, [|mkVar p|]);
+ mkApp(delayed_force lt_n_Sn, [|mkVar p|]); f_id|])));
+ simpl_iter onConcl;
+ tclTRY (unfold_in_concl [((true,[1]), evaluable_of_global_reference func)]);
+ list_rewrite true eqs;
+ apply (delayed_force refl_equal)] g;;
+
+let f_S t = mkApp(delayed_force coq_S, [|t|]);;
+
+
+let rec introduce_all_values_eq cont_tac functional termine
+ f p heq1 pmax bounds le_proofs eqs ids =
+ function
+ [] ->
+ let heq2 = next_global_ident_away true heq_id ids in
+ tclTHENLIST
+ [forward None (IntroIdentifier heq2)
+ (mkApp(mkVar heq1, [|f_S(f_S(mkVar pmax))|]));
+ simpl_iter (onHyp heq2);
+ unfold_in_hyp [((true,[1]), evaluable_of_global_reference
+ (global_of_constr functional))]
+ ((all_occurrences_expr, heq2), Tacexpr.InHyp);
+ tclTHENS
+ (fun gls ->
+ let t_eq = compute_renamed_type gls (mkVar heq2) in
+ let def_id =
+ let _,_,t = destProd t_eq in let def_na,_,_ = destProd t in
+ Nameops.out_name def_na
+ in
+ observe_tac "rewrite heq" (general_rewrite_bindings false all_occurrences
+ (mkVar heq2,
+ ExplicitBindings[dummy_loc,NamedHyp def_id,
+ f]) false) gls)
+ [tclTHENLIST
+ [observe_tac "list_rewrite" (list_rewrite true eqs);
+ cont_tac pmax le_proofs];
+ tclTHENLIST[apply (delayed_force le_lt_SS);
+ compute_le_proofs le_proofs]]]
+ | arg::args ->
+ let v' = next_global_ident_away true v_id ids in
+ let ids = v'::ids in
+ let hex' = next_global_ident_away true hex_id ids in
+ let ids = hex'::ids in
+ let p' = next_global_ident_away true p_id ids in
+ let ids = p'::ids in
+ let new_pmax = next_global_ident_away true pmax_id ids in
+ let ids = pmax::ids in
+ let hle1 = next_global_ident_away true hle_id ids in
+ let ids = hle1::ids in
+ let hle2 = next_global_ident_away true hle_id ids in
+ let ids = hle2::ids in
+ let heq = next_global_ident_away true heq_id ids in
+ let ids = heq::ids in
+ let heq2 = next_global_ident_away true heq_id ids in
+ let ids = heq2::ids in
+ tclTHENLIST
+ [mkCaseEq(mkApp(termine, Array.of_list arg));
+ h_intros [v'; hex'];
+ simplest_elim(mkVar hex');
+ h_intros [p'];
+ simplest_elim(mkApp(delayed_force max_constr, [|mkVar pmax;
+ mkVar p'|]));
+ h_intros [new_pmax;hle1;hle2];
+ introduce_all_values_eq
+ (fun pmax' le_proofs'->
+ tclTHENLIST
+ [cont_tac pmax' le_proofs';
+ h_intros [heq;heq2];
+ observe_tac ("rewriteRL " ^ (string_of_id heq2))
+ (tclTRY (rewriteLR (mkVar heq2)));
+ tclTRY (tclTHENS
+ ( fun g ->
+ let t_eq = compute_renamed_type g (mkVar heq) in
+ let k_id,def_id =
+ let k_na,_,t = destProd t_eq in
+ let _,_,t = destProd t in
+ let def_na,_,_ = destProd t in
+ Nameops.out_name k_na,Nameops.out_name def_na
+ in
+ let c_b = (mkVar heq,
+ ExplicitBindings
+ [dummy_loc, NamedHyp k_id,
+ f_S(mkVar pmax');
+ dummy_loc, NamedHyp def_id, f])
+ in
+ observe_tac "general_rewrite_bindings" ( (general_rewrite_bindings false all_occurrences
+ c_b false))
+ g
+ )
+ [tclIDTAC;
+ tclTHENLIST
+ [apply (delayed_force le_lt_n_Sm);
+ compute_le_proofs le_proofs']])])
+ functional termine f p heq1 new_pmax
+ (p'::bounds)((mkVar pmax)::le_proofs) eqs
+ (heq2::heq::hle2::hle1::new_pmax::p'::hex'::v'::ids) args]
+
+
+let rec_leaf_eq termine f ids functional eqs expr fn args =
+ let p = next_global_ident_away true p_id ids in
+ let ids = p::ids in
+ let v = next_global_ident_away true v_id ids in
+ let ids = v::ids in
+ let hex = next_global_ident_away true hex_id ids in
+ let ids = hex::ids in
+ let heq1 = next_global_ident_away true heq_id ids in
+ let ids = heq1::ids in
+ let hle1 = next_global_ident_away true hle_id ids in
+ let ids = hle1::ids in
+ tclTHENLIST
+ [observe_tac "intros v hex" (h_intros [v;hex]);
+ simplest_elim (mkVar hex);
+ h_intros [p;heq1];
+ h_generalize [mkApp(delayed_force le_n,[|mkVar p|])];
+ h_intros [hle1];
+ observe_tac "introduce_all_values_eq" (introduce_all_values_eq
+ (fun _ _ -> tclIDTAC)
+ functional termine f p heq1 p [] [] eqs ids args);
+ observe_tac "failing here" (apply (delayed_force refl_equal))]
+
+let rec prove_eq (termine:constr) (f:constr)(functional:global_reference)
+ (eqs:constr list) (expr:constr) =
+(* tclTRY *)
+ (match kind_of_term expr with
+ Case(ci,t,a,l) ->
+ (match find_call_occs 0 f a with
+ _,[] ->
+ (fun g ->
+ let destruct_tac,rev_to_thin_intro = mkDestructEq [] a g in
+ tclTHENS
+ destruct_tac
+ (list_map_i
+ (fun i -> mk_intros_and_continue
+ (List.rev rev_to_thin_intro) true
+ (prove_eq termine f functional)
+ eqs ci.ci_cstr_nargs.(i))
+ 0 (Array.to_list l)) g)
+ | _,_::_ ->
+ (match find_call_occs 0 f expr with
+ _,[] -> base_leaf_eq functional eqs f
+ | fn,args ->
+ fun g ->
+ let ids = ids_of_named_context (pf_hyps g) in
+ rec_leaf_eq termine f ids
+ (constr_of_global functional)
+ eqs expr fn args g))
+ | _ ->
+ (match find_call_occs 0 f expr with
+ _,[] -> base_leaf_eq functional eqs f
+ | fn,args ->
+ fun g ->
+ let ids = ids_of_named_context (pf_hyps g) in
+ observe_tac "rec_leaf_eq" (rec_leaf_eq
+ termine f ids (constr_of_global functional)
+ eqs expr fn args) g));;
+
+let (com_eqn : identifier ->
+ global_reference -> global_reference -> global_reference
+ -> constr -> unit) =
+ fun eq_name functional_ref f_ref terminate_ref equation_lemma_type ->
+ let opacity =
+ match terminate_ref with
+ | ConstRef c ->
+ let cb = Global.lookup_constant c in
+ if cb.Declarations.const_opaque then true
+ else begin match cb.const_body with None -> true | _ -> false end
+ | _ -> anomaly "terminate_lemma: not a constant"
+ in
+ let (evmap, env) = Command.get_current_context() in
+ let f_constr = (constr_of_global f_ref) in
+ let equation_lemma_type = subst1 f_constr equation_lemma_type in
+ (start_proof eq_name (Global, Proof Lemma)
+ (Environ.named_context_val env) equation_lemma_type (fun _ _ -> ());
+ by
+ (start_equation f_ref terminate_ref
+ (fun x ->
+ prove_eq
+ (constr_of_global terminate_ref)
+ f_constr
+ functional_ref
+ []
+ (instantiate_lambda
+ (def_of_const (constr_of_global functional_ref))
+ (f_constr::List.map mkVar x)
+ )
+ )
+ );
+(* (try Vernacentries.interp (Vernacexpr.VernacShow Vernacexpr.ShowProof) with _ -> ()); *)
+(* Vernacentries.interp (Vernacexpr.VernacShow Vernacexpr.ShowScript); *)
+ Flags.silently (fun () ->Command.save_named opacity) () ;
+(* Pp.msgnl (str "eqn finished"); *)
+
+ );;
+
+let nf_zeta env =
+ Reductionops.clos_norm_flags (Closure.RedFlags.mkflags [Closure.RedFlags.fZETA])
+ env
+ Evd.empty
+
+let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num eq
+ generate_induction_principle using_lemmas : unit =
+ let function_type = interp_constr Evd.empty (Global.env()) type_of_f in
+ let env = push_named (function_name,None,function_type) (Global.env()) in
+(* Pp.msgnl (str "function type := " ++ Printer.pr_lconstr function_type); *)
+ let equation_lemma_type = interp_gen (OfType None) Evd.empty env ~impls:([],rec_impls) eq in
+(* Pp.msgnl (Printer.pr_lconstr equation_lemma_type); *)
+ let res_vars,eq' = decompose_prod equation_lemma_type in
+ let env_eq' = Environ.push_rel_context (List.map (fun (x,y) -> (x,None,y)) res_vars) env in
+ let eq' = nf_zeta env_eq' eq' in
+ let res =
+(* Pp.msgnl (str "res_var :=" ++ Printer.pr_lconstr_env (push_rel_context (List.map (function (x,t) -> (x,None,t)) res_vars) env) eq'); *)
+(* Pp.msgnl (str "rec_arg_num := " ++ str (string_of_int rec_arg_num)); *)
+(* Pp.msgnl (str "eq' := " ++ str (string_of_int rec_arg_num)); *)
+ match kind_of_term eq' with
+ | App(e,[|_;_;eq_fix|]) ->
+ mkLambda (Name function_name,function_type,subst_var function_name (compose_lam res_vars eq_fix))
+ | _ -> failwith "Recursive Definition (res not eq)"
+ in
+ let pre_rec_args,function_type_before_rec_arg = decompose_prod_n (rec_arg_num - 1) function_type in
+ let (_, rec_arg_type, _) = destProd function_type_before_rec_arg in
+ let arg_types = List.rev_map snd (fst (decompose_prod_n (List.length res_vars) function_type)) in
+ let equation_id = add_suffix function_name "_equation" in
+ 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 Definition) res in
+ let env_with_pre_rec_args = push_rel_context(List.map (function (x,t) -> (x,None,t)) pre_rec_args) env in
+ let relation =
+ interp_constr
+ Evd.empty
+ env_with_pre_rec_args
+ r
+ 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 (make_short_qualid term_id) in
+ let f_ref = declare_f function_name (IsProof Lemma) arg_types term_ref in
+(* message "start second proof"; *)
+ let stop = ref false in
+ begin
+ try com_eqn equation_id functional_ref f_ref term_ref (subst_var function_name equation_lemma_type)
+ with e ->
+ begin
+ if Tacinterp.get_debug () <> Tactic_debug.DebugOff
+ then pperrnl (str "Cannot create equation Lemma " ++ Cerrors.explain_exn e)
+ else anomaly "Cannot create equation Lemma"
+ ;
+(* ignore(try Vernacentries.vernac_reset_name (Util.dummy_loc,functional_id) with _ -> ()); *)
+ stop := true;
+ end
+ end;
+ if not !stop
+ then
+ let eq_ref = Nametab.locate (make_short_qualid equation_id ) in
+ let f_ref = destConst (constr_of_global f_ref)
+ and functional_ref = destConst (constr_of_global functional_ref)
+ 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 rec_arg_type (nb_prod res) relation;
+ if Flags.is_verbose ()
+ then msgnl (h 1 (Ppconstr.pr_id function_name ++
+ spc () ++ str"is defined" )++ fnl () ++
+ h 1 (Ppconstr.pr_id equation_id ++
+ spc () ++ str"is defined" )
+ )
+ in
+ try
+ com_terminate
+ tcc_lemma_name
+ tcc_lemma_constr
+ is_mes functional_ref
+ rec_arg_type
+ relation rec_arg_num
+ term_id
+ using_lemmas
+ (List.length res_vars)
+ hook
+ with e ->
+ begin
+ ignore(try Vernacentries.vernac_reset_name (Util.dummy_loc,functional_id) with _ -> ());
+(* anomaly "Cannot create termination Lemma" *)
+ raise e
+ end
+
+
+
diff --git a/contrib/funind/tacinv.ml4 b/contrib/funind/tacinv.ml4
deleted file mode 100644
index 5d19079b..00000000
--- a/contrib/funind/tacinv.ml4
+++ /dev/null
@@ -1,872 +0,0 @@
-(*i camlp4deps: "parsing/grammar.cma" i*)
-
-(*s FunInv Tactic: inversion following the shape of a function. *)
-
-(* Deprecated: see indfun_main.ml4 instead *)
-
-(* Don't delete this file yet, it may be used for other purposes *)
-
-(*i*)
-open Termops
-open Equality
-open Names
-open Pp
-open Tacmach
-open Proof_type
-open Tacinterp
-open Tactics
-open Tacticals
-open Term
-open Util
-open Printer
-open Reductionops
-open Inductiveops
-open Coqlib
-open Refine
-open Typing
-open Declare
-open Decl_kinds
-open Safe_typing
-open Vernacinterp
-open Evd
-open Environ
-open Entries
-open Setoid_replace
-open Tacinvutils
-(*i*)
-
-module Smap = Map.Make(struct type t = constr let compare = compare end)
-let smap_to_list m = Smap.fold (fun c cb l -> (c,cb)::l) m []
-let merge_smap m1 m2 = Smap.fold (fun c cb m -> Smap.add c cb m) m1 m2
-let rec listsuf i l = if i<=0 then l else listsuf (i-1) (List.tl l)
-let rec listpref i l = if i<=0 then [] else List.hd l :: listpref (i-1) (List.tl l)
-let rec split3 l =
- List.fold_right (fun (e1,e2,e3) (a,b,c) -> (e1::a),(e2::b),(e3::c)) l ([],[],[])
-
-let mkthesort = mkProp (* would like to put Type here, but with which index? *)
-
-(* this is the prefix used to name equality hypothesis generated by
- case analysis*)
-let equality_hyp_string = "_eg_"
-
-(* bug de refine: on doit ssavoir sur quelle hypothese on se trouve. valeur
- initiale au debut de l'appel a la fonction proofPrinc: 1. *)
-let nthhyp = ref 1
-
-let debug i = prstr ("DEBUG "^ string_of_int i ^"\n")
-let pr2constr = (fun c1 c2 -> prconstr c1; prstr " <---> "; prconstr c2)
-(* Operations on names *)
-let id_of_name = function
- Anonymous -> id_of_string "H"
- | Name id -> id;;
-let string_of_name nme = string_of_id (id_of_name nme)
- (*end debugging *)
-
-(* Interpretation of constr's *)
-let constr_of c = Constrintern.interp_constr Evd.empty (Global.env()) c
-
-(*s specific manipulations on constr *)
-let lift1_leqs leq=
- List.map
- (function (r,(typofg,g,d))
- -> lift 1 r, (lift 1 typofg, lift 1 g , lift 1 d)) leq
-
-let lift1_relleqs leq= List.map (function (r,x) -> lift 1 r,x) leq
-
-(* WARNING: In the types, we don't lift the rels in the type. This is
- intentional. Use with care. *)
-let lift1_lvars lvars= List.map
- (function x,(nme,c) -> lift 1 x, (nme, (*lift 1*) c)) lvars
-
-let pop1_levar levars = List.map (function ev,tev -> ev, popn 1 tev) levars
-
-
-let rec add_n_dummy_prod t n =
- if n<=0 then t
- else add_n_dummy_prod (mkNamedProd (id_of_string "DUMMY") mkthesort t) (n-1)
-
-(* [add_lambdas t gl [csr1;csr2...]] returns [[x1:type of csr1]
- [x2:type of csr2] t [csr <- x1 ...]], names of abstracted variables
- are not specified *)
-let rec add_lambdas t gl lcsr =
- match lcsr with
- | [] -> t
- | csr::lcsr' ->
- let hyp_csr,hyptyp = csr,(pf_type_of gl csr) in
- lambda_id hyp_csr hyptyp (add_lambdas t gl lcsr')
-
-(* [add_pis t gl [csr1;csr2...]] returns ([x1] :type of [csr1]
- [x2]:type of csr2) [t]*)
-let rec add_pis t gl lcsr =
- match lcsr with
- | [] -> t
- | csr::lcsr' ->
- let hyp_csr,hyptyp = csr,(pf_type_of gl csr) in
- prod_id hyp_csr hyptyp (add_pis t gl lcsr')
-
-let mkProdEg teq eql eqr concl =
- mkProd (name_of_string "eg", mkEq teq eql eqr, lift 1 concl)
-
-let eqs_of_beqs x =
- List.map (function (_,(a,b,c)) -> (Anonymous, mkEq a b c)) x
-
-
-let rec eqs_of_beqs_named_aux s i l =
- match l with
- | [] -> []
- | (r,(a,b,c))::l' ->
- (Name(id_of_string (s^ string_of_int i)), mkEq a b c)
- ::eqs_of_beqs_named_aux s (i-1) l'
-
-
-let eqs_of_beqs_named s l = eqs_of_beqs_named_aux s (List.length l) l
-
-let rec patternify ltypes c nme =
- match ltypes with
- | [] -> c
- | (mv,t)::ltypes' ->
- let c'= substitterm 0 mv (mkRel 1) c in
- let tlift = lift (List.length ltypes') t in
- let res =
- patternify ltypes' (mkLambda (newname_append nme "rec", tlift, c')) nme in
- res
-
-let rec npatternify ltypes c =
- match ltypes with
- | [] -> c
- | (mv,nme,t)::ltypes' ->
- let c'= substitterm 0 mv (mkRel 1) c in
- let tlift = lift (List.length ltypes') t in
- let res =
- npatternify ltypes' (mkLambda (newname_append nme "", tlift, c')) in
- res
-
-(* fait une application (c m1 m2...mn, où mi est une evar, on rend également
- la liste des evar munies de leur type) *)
-let rec apply_levars c lmetav =
- match lmetav with
- | [] -> [],c
- | (i,typ) :: lmetav' ->
- let levars,trm = apply_levars c lmetav' in
- let exkey = mknewexist() in
- ((exkey,typ)::levars), applistc trm [mkEvar exkey]
- (* EXPERIMENT le refine est plus long si on met un cast:
- ((exkey,typ)::levars), mkCast ((applistc trm [mkEvar exkey]),typ) *)
-
-
-let prod_change_concl c newconcl =
- let lv,_ = decompose_prod c in prod_it newconcl lv
-
-let lam_change_concl c newconcl =
- let lv,_ = decompose_prod c in lam_it newconcl lv
-
-
-let rec mkAppRel c largs n =
- match largs with
- | [] -> c
- | arg::largs' ->
- let newc = mkApp (c,[|(mkRel n)|]) in mkAppRel newc largs' (n-1)
-
-let applFull c typofc =
- let lv,t = decompose_prod typofc in
- let ltyp = List.map fst lv in
- let res = mkAppRel c ltyp (List.length ltyp) in
- res
-
-(* Take two terms with same structure and return a map of deBruijn from the
- first to the second. Only DeBruijn should be different between the two
- terms. *)
-let rec build_rel_map typ type_of_b =
- match (kind_of_term typ), (kind_of_term type_of_b) with
- Evar _ , Evar _ -> Smap.empty
- | Const c1, Const c2 when c1=c2 -> Smap.empty
- | Ind c1, Ind c2 when c1=c2 -> Smap.empty
- | Rel i, Rel j when i=j -> Smap.empty
- | Rel i, Rel j -> Smap.add typ type_of_b Smap.empty
- | Prod (name,c1,c2), Prod (nameb,c1b,c2b) ->
- let map1 = build_rel_map c1 c1b in
- let map2 = build_rel_map (pop c2) (pop c2b) in
- merge_smap map1 map2
- | App (f,args), App (fb,argsb) when Array.length args = Array.length argsb ->
- build_rel_map_list (Array.to_list args) (Array.to_list argsb)
- | _,_ -> failwith ("Could not generate case annotation. "^
- "Incompatibility between annotation and actual type")
-
-and build_rel_map_list ltyp ltype_of_b =
- List.fold_left2 (fun a b c -> merge_smap a (build_rel_map b c))
- Smap.empty ltyp ltype_of_b
-
-
-(*s Use (and proof) of the principle *)
-
-(* This is the type of the argument of [proofPrinc] *)
-
-type mimickinfo =
- {
- concl: constr; (* conclusion voulue, cad (xi:ti)gl, ou gl est le but a
- prouver, et xi:ti correspondent aux arguments donnés à
- la tactique. On enlèvera un produit à chaque fois
- qu'on rencontrera un binder, sans lift ou pop.
- Initialement: une seule conclusion, puis specifique à
- chaque branche. *)
- absconcl: constr array; (* conclusions patternisées pour pouvoir être
- appliquées = un predicat pour chaque fixpt
- mutuel. *)
- mimick: constr; (* le terme qu'on imite. On plongera dedans au fur et
- à mesure, sans lift ni pop. *)
- env: env; (* The global typing environment, we will add thing in it when
- going inside the term (push_rel, push_rec_types) *)
- sigma: Evd.evar_map;
- nmefonc: constr array; (* la constante correspondant à la fonction
- appelée, permet de remplacer les appels
- recursifs par des appels à la constante
- correspondante (non pertinent (et inutile) si
- on permet l'appel de la tactique sur une terme
- donné directement (au lieu d'une constante
- comme pour l'instant)). *)
- fonc: int * int; (* bornes des indices des variable correspondant aux
- appels récursifs (plusieurs car fixp. mutuels),
- utile pour reconnaître les appels récursifs
- (ATTENTION: initialement vide, reste vide tant qu'on
- n'est pas dans un fix). *)
- doeqs: bool; (* this reference is to toggle building of equalities during
- the building of the principle (default is true) *)
- fix: bool; (* did I already went through a fix or case constr? lambdas
- found before a case or a fix are treated as parameters of
- the induction principle *)
- lst_vars: (constr*(name*constr)) list ; (* Variables rencontrées jusque là *)
- lst_eqs: (Term.constr * (Term.constr * Term.constr * Term.constr)) list ;
- (* liste d'équations engendrées au cours du
- parcours, cette liste grandit à chaque
- case, et il faut lifter le tout à chaque
- binder *)
- lst_recs: constr list ; (* appels récursifs rencontrés jusque là *)
- }
-
-(* This is the return type of [proofPrinc] *)
-type 'a funind = (* 'A = CONTR OU CONSTR ARRAY *)
- {
-
- princ:'a; (* le (ou les) principe(s) demandé(s), il contient des meta
- variables représentant soit des trous à prouver plus tard,
- soit les conclusions à compléter avant de rendre le terme
- (suivant qu'on utilise le principe pour faire refine ou
- functional scheme). Il y plusieurs conclusions si plusieurs
- fonction mutuellement récursives) voir la suite. *)
- evarlist: (constr*Term.types) list; (* [(ev1,tev1);(ev2,tev2)...]]
- l'ensemble des meta variables
- correspondant à des trous. [evi]
- est la meta variable, [tevi] est
- son type. *)
- hypnum: (int*int*int) list; (* [[(in,jn,kn)...]] sont les nombres
- respectivement de variables, d'équations,
- et d'hypothèses de récurrence pour le but
- n. Permet de faire le bon nombre d'intros
- et des rewrite au bons endroits dans la
- suite. *)
- mutfixmetas: constr array ; (* un tableau de meta variables correspondant
- à chacun des prédicats mutuellement
- récursifs construits. *)
- conclarray: types array; (* un tableau contenant les conclusions
- respectives de chacun des prédicats
- mutuellement récursifs. Permet de finir la
- construction du principe. *)
- params:(constr*name*constr) list; (* [[(metavar,param,tparam)..]] la
- liste des paramètres (les lambdas
- au-dessus du fix) du fixpoint si
- fixpoint il y a, le paramètre est
- une meta var, dont on stocke le nom
- et le type. TODO: utiliser la
- structure adequat? *)
- }
-
-
-
-let empty_funind_constr =
- {
- princ = mkProp;
- evarlist = [];
- hypnum = [];
- mutfixmetas = [||];
- conclarray = [||];
- params = []
- }
-
-let empty_funind_array =
- { empty_funind_constr with
- princ = [||];
- }
-
-(* Replace the calls to the function (recursive calls) by calls to the
- corresponding constant *)
-let replace_reccalls mi b =
- let d,f = mi.fonc in
- let res = ref b in
- let _ = for i = d to f do
- res := substitterm 0 (mkRel i) mi.nmefonc.(f-i) !res done in
- !res
-
-
-
-(* collects all information of match branches stored in [l] *)
-let rec collect_cases l =
- match l with
- | [||] -> empty_funind_array
- | arr ->
- let x = arr.(0) in
- let resrec = collect_cases (Array.sub arr 1 (Array.length arr - 1)) in
- { x with
- princ= Array.append [|x.princ|] resrec.princ;
- evarlist = x.evarlist@resrec.evarlist;
- hypnum = x.hypnum@resrec.hypnum;
- }
-
-let collect_pred l =
- let l1,l2,l3 = split3 l in
- Array.of_list l1 , Array.of_list l2 , Array.of_list l3
-
-
-(* [build_pred n tarr] builds the right predicates for each element of [tarr]
- (of type: [type array] of size [n]). Return the list of triples:
- (?i ,
- fun (x1:t1) ... (xn:tn) => (?i x1...xn) ,
- forall (x1:t1) ... (xn:tn), (?i x1...xn)),
- where ti's are deduced from elements of tarr, which are of the form:
- t1 -> t2 -> ... -> tn -> <nevermind>. *)
-let rec build_pred n tarr =
- if n >= Array.length tarr (* iarr *) then []
- else
- let ftyp = Array.get tarr n in
- let gl = mknewmeta() in
- let gl_app = applFull gl ftyp in
- let pis = prod_change_concl ftyp gl_app in
- let gl_abstr = lam_change_concl ftyp gl_app in
- (gl,gl_abstr,pis):: build_pred (n+1) tarr
-
-
-let heq_prefix = "H_eq_"
-
-type kind_of_hyp = Var | Eq (*| Rec*)
-
-(* the main function, build the principle by exploring the term and reproduce
- the same structure. *)
-let rec proofPrinc mi: constr funind =
- match kind_of_term mi.mimick with
- (* Fixpoint: we reproduce the Fix, fonc becomes (1,nbofmutf) to point on
- the name of recursive calls *)
- | Fix((iarr,i),(narr,tarr,carr)) ->
- (* We construct the right predicates for each mutual fixpt *)
- let evararr,newabsconcl,pisarr = collect_pred (build_pred 0 tarr) in
- let newenv = push_rec_types (narr,tarr,carr) mi.env in
- let anme',aappel_rec,llevar,llposeq =
- collect_fix mi 0 iarr narr carr pisarr newabsconcl newenv in
- let anme = Array.map (fun nme -> newname_append nme "_ind") anme' in
- {
- princ = mkFix((iarr,i),(anme, pisarr,aappel_rec));
- evarlist= pop1_levar llevar; (* llevar are put outside the fix, so we pop 1 *)
- hypnum = llposeq;
- mutfixmetas = evararr;
- conclarray = pisarr;
- params = []
- }
- (* <pcase> Cases b of arrPt end.*)
- | Case (cinfo, pcase, b, arrPt) ->
- let prod_pcase,_ = decompose_lam pcase in
- let _nmeb,_ = List.hd prod_pcase in
- let newb'= apply_leqtrpl_t b mi.lst_eqs in
- let type_of_b = Typing.type_of mi.env mi.sigma b in
- (* Replace the recursive calls to the function by calls to the constant *)
- let newb = replace_reccalls mi newb' in
- let cases = collect_cases (Array.mapi (fold_proof mi b type_of_b newb) arrPt) in
- (* the match (case) annotation must be transformed, see [build_pcase] below *)
- let newpcase = build_pcase mi pcase b type_of_b newb in
- let trm' = mkCase (cinfo,newpcase,newb, cases.princ) in
- { cases with
- princ = if mi.doeqs then mkApp (trm',[|(mkRefl type_of_b newb)|]) else trm';
- params = [] (* FIX: fix parms here (fixpt inside a match)*)
- }
-
-
- | Lambda(nme, typ, cstr) ->
- let _, _, cconcl = destProd mi.concl in
- let d,f=mi.fonc in
- let newenv = push_rel (nme,None,typ) mi.env in
- let newlst_var = (* if this lambda is a param, then don't add it here *)
- if mi.fix then (mkRel 1,(nme,typ)) :: lift1_lvars mi.lst_vars
- else (*(mkRel 1,(nme,typ)) :: *) lift1_lvars mi.lst_vars in
- let newmi = {mi with concl=cconcl; mimick=cstr; env=newenv;
- fonc = (if d > 0 then d+1 else 0) , (if f > 0 then f+1 else 0);
- lst_vars = newlst_var ; lst_eqs = lift1_leqs mi.lst_eqs;
- lst_recs = lift1L mi.lst_recs} in
- let resrec = proofPrinc newmi in
- (* are we inside a fixpoint or a case? then this is a normal lambda *)
- if mi.fix
- then { resrec with princ = mkLambda (nme,typ,resrec.princ) ; params = [] }
- else (* otherwise this is a parameter *)
- let metav = mknewmeta() in
- let substmeta t = popn 1 (substitterm 0 (mkRel 1) metav t) in
- { resrec with
- princ = substmeta resrec.princ;
- evarlist = List.map (fun (ev,tev) -> ev, substmeta tev) resrec.evarlist;
- conclarray = Array.map substmeta resrec.conclarray;
- params = (metav,nme,typ) :: resrec.params
- }
-
-
- | LetIn(nme,cstr1, typ, cstr) ->
- failwith ("I don't deal with let ins yet. "^
- "Please expand them before applying this function.")
-
- | u ->
- let varrels = List.rev (List.map fst mi.lst_vars) in
- let varnames = List.map snd mi.lst_vars in
- let nb_vars = List.length varnames in
- let nb_eqs = List.length mi.lst_eqs in
- let _eqrels = List.map fst mi.lst_eqs in
- (* [terms_recs]: appel rec du fixpoint, On concatène les appels recs
- trouvés dans les let in et les Cases avec ceux trouves dans u (ie
- mi.mimick). *)
- (* TODO: il faudra gérer plusieurs pt fixes imbriqués ? *)
- let terms_recs = mi.lst_recs @ hdMatchSub_cpl mi.mimick mi.fonc in
- (*c construction du terme: application successive des variables, des
- egalites et des appels rec, a la variable existentielle correspondant a
- l'hypothese de recurrence en cours. *)
- (* d'abord, on fabrique les types des appels recursifs en replacant le nom
- de des fonctions par les predicats dans [terms_recs]: [(f_i t u v)]
- devient [(P_i t u v)] *)
- (* TODO optimiser ici: *)
- let appsrecpred = exchange_reli_arrayi_L mi.absconcl mi.fonc terms_recs in
- let typeofhole'' = prod_it_anonym_lift mi.concl appsrecpred in
- let typeofhole = prodn nb_vars varnames typeofhole'' in
- (* Un bug de refine m'oblige à mettre ici un H (meta variable à ce point,
- mais remplacé par H avant le refine) au lieu d'un '?', je mettrai les
- '?' à la fin comme ça [(([H1,H2,H3...] ...) ? ? ?)] *)
- let newmeta = mknewmeta() in
- let concl_with_var = applistc newmeta varrels in
- let conclrecs = applistc concl_with_var terms_recs in
- { empty_funind_constr with
- princ = conclrecs;
- evarlist = [ newmeta , typeofhole ];
- hypnum = [ nb_vars , List.length terms_recs , nb_eqs ];
- conclarray = mi.absconcl;
- }
-
-
-(* C'est un peu compliqué ici: en cas de type inductif vraiment dépendant
- l'annotation de type du case [pcase] contient des lambdas supplémentaires
- en tête. Je les récupère dans la variable [suppllam_pcase]. Le problème est
- que la conclusion de l'annotation du nouveauacse doit faire référence à ces
- variables plutôt qu'à celle de l'exterieur. Ce qui suit permet de changer
- les reference de newpcase' pour pointer vers les lambda du piquant. On
- procède comme suit: on repère les rels qui pointent à l'interieur de
- l'annotation dans la fonction initiale et on les relie à celle du type
- voulu pour le case, pour ça ([build_rel_map]) on parcourt en même temps le
- dernier lambda du piquant ([typ]) (qui contient le type de l'argument du
- case) et le type attendu pour le case ([type_of_b]) et on construit un
- map. Ensuite on remplace les rels correspondant dans la preuve construite
- en suivant le map. *)
-
-and build_pcase mi pcase b type_of_b newb =
- let prod_pcase,_ = decompose_lam pcase in
- let nme,typ = List.hd prod_pcase in
- (* je remplace b par rel1 (apres avoir lifte un coup) dans la future
- annotation du futur case: ensuite je mettrai un lambda devant *)
- let typeof_case'' = substitterm 0 (lift 1 b) (mkRel 1) (lift 1 mi.concl) in
- let suppllam_pcase = List.tl prod_pcase in
- let suppllam_pcasel = List.length suppllam_pcase in
- let rel_smap =
- if suppllam_pcasel=0 then Smap.empty else (* FIX: is this test necessary ? *)
- build_rel_map (lift suppllam_pcasel type_of_b) typ in
- let newpcase''' =
- Smap.fold (fun e e' acc -> substitterm 0 e (lift 1 e') acc)
- rel_smap typeof_case'' in
- let neweq = mkEq (lift (suppllam_pcasel + 1) type_of_b)
- (lift (suppllam_pcasel + 1) newb) (mkRel 1) in
- let newpcase'' =
- if mi.doeqs
- then mkProd (name_of_string "eg", neweq, lift 1 newpcase''')
- else newpcase''' in
- (* construction du dernier lambda du piquant. *)
- let newpcase' = mkLambda (newname_append nme "_ind" ,typ, newpcase'') in
- (* ajout des lambdas supplémentaires (type dépendant) du piquant. *)
- lamn suppllam_pcasel suppllam_pcase newpcase'
-
-
-(* [fold_proof mi b typeofb newb l n] rend le resultat de l'appel recursif sur
- cstr (correpsondant au ième elt de [arrPt] ci-dessus et donc au ième
- constructeur de [typeofb]), appele avec les bons arguments: [mi.concl]
- devient [(DUMMY1:t1;...;DUMMY:tn)concl'], ou [n] est le nombre d'arguments
- du constructeur considéré, et [concl'] est [mi.concl] ou l'on a réécrit [b]
- en ($c_n$ [rel1]...). *)
-and fold_proof mi b type_of_b newb i cstr =
- let new_lst_recs = mi.lst_recs @ hdMatchSub_cpl b mi.fonc in
- (* mise a jour de concl pour l'interieur du case, concl'= concl[b <- C x3
- x2 x1... ], sans quoi les annotations ne sont plus coherentes *)
- let cstr_appl,nargs = nth_dep_constructor type_of_b i in
- let concl'' =
- substitterm 0 (lift nargs b) cstr_appl (lift nargs mi.concl) in
- let neweq = mkEq type_of_b newb (popn nargs cstr_appl) in
- let concl_dummy = add_n_dummy_prod concl'' nargs in
- let lsteqs_rew = apply_eq_leqtrpl mi.lst_eqs neweq in
- let new_lsteqs = (mkRel (-nargs),(type_of_b,newb, popn nargs cstr_appl))::lsteqs_rew in
- let a',a'' = decompose_lam_n nargs cstr in
- let newa'' =
- if mi.doeqs
- then mkLambda (name_of_string heq_prefix,lift nargs neweq,lift 1 a'')
- else a'' in
- let newmimick = lamn nargs a' newa'' in
- let b',b'' = decompose_prod_n nargs concl_dummy in
- let newb'' =
- if mi.doeqs
- then mkProd (name_of_string heq_prefix,lift nargs neweq,lift 1 b'')
- else b'' in
- let newconcl = prodn nargs b' newb'' in
- let newmi = {mi with mimick=newmimick; concl=newconcl; fix=true;
- lst_eqs= new_lsteqs; lst_recs = new_lst_recs} in
- proofPrinc newmi
-
-
-and collect_fix mi n iarr narr carr pisarr newabsconcl newenv =
- if n >= Array.length iarr then [||],[||],[],[]
- else
- let nme = Array.get narr n in
- let c = Array.get carr n in
- (* rappelle sur le sous-terme, on ajoute un niveau de
- profondeur (lift) parce que Fix est un binder. *)
- let newmi = {mi with concl=(pisarr.(n)); absconcl=newabsconcl;
- mimick=c; fonc=(1,((Array.length iarr)));env=newenv;fix=true;
- lst_vars=lift1_lvars mi.lst_vars; lst_eqs=lift1_leqs mi.lst_eqs;
- lst_recs= lift1L mi.lst_recs;} in
- let resrec = proofPrinc newmi in
- let lnme,lappel_rec,llevar,llposeq =
- collect_fix mi (n+1) iarr narr carr pisarr newabsconcl newenv in
- Array.append [|nme|] lnme , Array.append [|resrec.princ|] lappel_rec
- , (resrec.evarlist@llevar) , (resrec.hypnum@llposeq)
-
-let mkevarmap_aux ex = let x,y = ex in (mkevarmap_from_listex x),y
-
-
-(* TODO: deal with any term, not only a constant. *)
-let interp_fonc_tacarg fonctac gl =
- (* [fonc] is the constr corresponding to fontact not unfolded,
- if [fonctac] is a (qualified) name then this is a [const] ?. *)
-(* let fonc = constr_of_Constr fonctac in *)
- (* TODO: replace the [with _ -> ] by something more precise in
- the following. *)
- (* [def_fonc] is the definition of fonc. TODO: We should do this only
- if [fonc] is a const, and take [fonc] otherwise.*)
- try fonctac, pf_const_value gl (destConst fonctac)
- with _ -> failwith ("don't know how to deal with this function "
- ^"(DEBUG:is it a constante?)")
-
-
-
-
-(* [invfun_proof fonc def_fonc gl_abstr pis] builds the principle,
- following the shape of [def_fonc], [fonc] is the constant
- corresponding to [def_func] (or a reduced form of it ?), gl_abstr and
- pis are the goal to be proved, of the form [x,y...]g and (x.y...)g.
-
- This function calls the big function proofPrinc. *)
-
-let invfun_proof fonc def_fonc gl_abstr pis env sigma =
- let mi = {concl=pis; absconcl=gl_abstr; mimick=def_fonc; env=env;
- sigma=sigma; nmefonc=fonc; fonc=(0,0); doeqs=true; fix=false ;
- lst_vars = []; lst_eqs = []; lst_recs = []} in
- proofPrinc mi
-
-(* Do intros [i] times, then do rewrite on all introduced hyps which are called
- like [heq_prefix], FIX: have another filter than the name. *)
-let rec iterintro i =
- if i<=0 then tclIDTAC else
- tclTHEN
- (tclTHEN
- intro
- (iterintro (i-1)))
- (fun gl ->
- (tclREPEAT
- (tclNTH_HYP i
- (fun hyp ->
- let hypname = (string_of_id (destVar hyp)) in
- let sub =
- try String.sub hypname 0 (String.length heq_prefix)
- with _ -> "" (* different than [heq_prefix] *) in
- if sub=heq_prefix then rewriteLR hyp else tclFAIL 0 (str "Cannot rewrite"))
- )) gl)
-
-
-(*
- (fun hyp gl ->
- let _ = prstr ("nthhyp= "^ string_of_int i) in
- if isConst hyp && ((name_of_const hyp)==heq_prefix) then
- let _ = prstr "YES\n" in
- rewriteLR hyp gl
- else
- let _ = prstr "NO\n" in
- tclIDTAC gl)
- *)
-
-(* [invfun_basic C listargs_ids gl dorew lposeq] builds the tactic
- which:
- \begin{itemize}
- \item Do refine on C (the induction principle),
- \item try to Clear listargs_ids
- \item if boolean dorew is true, then intro all new hypothesis, and
- try rewrite on those hypothesis that are equalities.
- \end{itemize}
-*)
-
-let invfun_basic open_princ_proof_applied listargs_ids gl dorew lposeq =
- (tclTHEN_i
- (tclTHEN
- (tclTHEN
- (* Refine on the right term (following the sheme of the
- given function) *)
- (fun gl -> refine open_princ_proof_applied gl)
- (* Clear the hypothesis given as arguments of the tactic
- (because they are generalized) *)
- (tclTHEN simpl_in_concl (tclTRY (clear listargs_ids))))
- (* Now we introduce the created hypothesis, and try rewrite on
- equalities due to case analysis *)
- (fun gl -> (tclIDTAC gl)))
- (fun i gl ->
- if not dorew then tclIDTAC gl
- else
- (* d,m,f correspond respectively to vars, induction hyps and
- equalities*)
- let d,m,f = List.nth lposeq (i-1) in
- tclTHEN (iterintro (d)) (tclDO m (tclTRY intro)) gl)
- )
- gl
-
-
-
-
-(* This function trys to reduce instanciated arguments, provided they
- are of the form [(C t u v...)] where [C] is a constructor, and
- provided that the argument is not the argument of a fixpoint (i.e. the
- argument corresponds to a simple lambda) . *)
-let rec applistc_iota cstr lcstr env sigma =
- match lcstr with
- | [] -> cstr,[]
- | arg::lcstr' ->
- let arghd =
- if isApp arg then let x,_ = destApp arg in x else arg in
- if isConstruct arghd (* of the form [(C ...)]*)
- then
- applistc_iota (Tacred.nf env sigma (nf_beta (applistc cstr [arg])))
- lcstr' env sigma
- else
- try
- let nme,typ,suite = destLambda cstr in
- let c, l = applistc_iota suite lcstr' env sigma in
- mkLambda (nme,typ,c), arg::l
- with _ -> cstr,arg::lcstr' (* the arg does not correspond to a lambda*)
-
-
-
-(* TODO: ne plus mettre les sous-but à l'exterieur, mais à l'intérieur (le bug
- de refine est normalement resolu). Ca permettra 2 choses: d'une part que
- les preuves soient plus simple, et d'autre part de fabriquer un terme de
- refine qui pourra s'aapliquer SANS FAIRE LES INTROS AVANT, ce qui est bcp
- mieux car fonctionne comme induction et plus comme inversion (pas de perte
- de connexion entre les hypothèse et les variables). *)
-
-(*s Tactic that makes induction and case analysis following the shape
- of a function (idf) given with arguments (listargs) *)
-let invfun c l dorew gl =
-(* \begin{itemize}
- \item [fonc] = the constant corresponding to the function
- (necessary for equalities of the form [(f x1 x2 ...)=...] where
- [f] is the recursive function).
- \item [def_fonc] = body of the function, where let ins have
- been expanded. *)
- let fonc, def_fonc' = interp_fonc_tacarg c gl in
- let def_fonc'',listargs' =
- applistc_iota def_fonc' l (pf_env gl) (project gl) in
- let def_fonc = expand_letins def_fonc'' in
- (* quantifies on previously generalized arguments.
- [(x1:T1)...g[arg1 <- x1 ...]] *)
- let pis = add_pis (pf_concl gl) gl listargs' in
- (* princ_proof builds the principle *)
- let _ = resetmeta() in
- let pr = invfun_proof [|fonc|] def_fonc [||] pis (pf_env gl) (project gl) in
- (* Generalize the goal. [[x1:T1][x2:T2]... g[arg1 <- x1 ...]]. *)
- let gl_abstr' = add_lambdas (pf_concl gl) gl listargs' in
- (* apply parameters immediately *)
- let gl_abstr =
- applistc gl_abstr' (List.map (fun (x,y,z) -> x) (List.rev pr.params)) in
- (* we apply args of the fix now, the parameters will be applied later *)
- let princ_proof_applied_args =
- applistc pr.princ (listsuf (List.length pr.params) listargs') in
- (* parameters are still there so patternify must not take them -> lift *)
- let princ_proof_applied_lift =
- lift (List.length pr.evarlist) princ_proof_applied_args in
- let princ_applied_hyps'' = patternify (List.rev pr.evarlist)
- princ_proof_applied_lift (Name (id_of_string "Hyp")) in
- (* if there was a fix, we will not add "Q" as in funscheme, so we make a pop,
- TODO: find were we made the lift in proofPrinc instead and supress it here,
- and add lift in funscheme. *)
- let princ_applied_hyps' =
- if Array.length pr.mutfixmetas > 0 then popn 1 princ_applied_hyps''
- else princ_applied_hyps'' in
- (* if there is was fix, we have to replace the meta representing the
- predicate of the goal by the abstracted goal itself. *)
- let princ_applied_hyps =
- if Array.length pr.mutfixmetas > 0 then(* mutual Fixpoint not treated in the tactic*)
- (substit_red 0 (pr.mutfixmetas.(0)) gl_abstr princ_applied_hyps')
- else princ_applied_hyps' (* No Fixpoint *) in
- let _ = prNamedConstr "princ_applied_hyps" princ_applied_hyps in
- (* Same thing inside levar *)
- let newlevar' =
- if Array.length pr.mutfixmetas > 0 then(* mutual Fixpoint not treated in the tactic*)
- List.map (fun (x,y) -> x,substit_red 0 (pr.mutfixmetas.(0)) gl_abstr y) pr.evarlist
- else pr.evarlist
- in
- (* replace params metavar by real args *)
- let rec replace_parms lparms largs t =
- match lparms, largs with
- [], _ -> t
- | ((p,_,_)::lp), (a::la) -> let t'= substitterm 0 p a t in replace_parms lp la t'
- | _, _ -> error "problem with number of args." in
- let princ_proof_applied = replace_parms pr.params listargs' princ_applied_hyps in
- let _ = prNamedLConstr "levar:" (List.map fst newlevar') in
- let _ = prNamedLConstr "levar types:" (List.map snd newlevar') in
- let _ = prNamedConstr "princ_proof_applied" princ_proof_applied in
- (* replace also in levar *)
- let newlevar =
- List.rev (List.map (fun (x,y) -> x, replace_parms pr.params listargs' y) newlevar') in
-(*
- (* replace params metavar by abstracted variables *)
- let princ_proof_params = npatternify (List.rev pr.params) princ_applied_hyps in
- (* we apply now the real parameters *)
- let princ_proof_applied =
- applistc princ_proof_params (listpref (List.length pr.params) listargs') in
-*)
- let princ_applied_evars = apply_levars princ_proof_applied newlevar in
- let open_princ_proof_applied = princ_applied_evars in
- let _ = prNamedConstr "princ_applied_evars" (snd princ_applied_evars) in
- let _ = prNamedLConstr "evars" (List.map snd (fst princ_applied_evars)) in
- let listargs_ids = List.map destVar (List.filter isVar listargs') in
- (* debug: impression du but*)
- let lgl = Evd.to_list (sig_sig gl) in
- let _ = prNamedLConstr "\ngl= " (List.map (fun x -> (snd x).evar_concl) lgl) in
- let _ = prstr "fin gl \n\n" in
- invfun_basic (mkevarmap_aux open_princ_proof_applied) listargs_ids
- gl dorew pr.hypnum
-
-(* function must be a constant, all arguments must be given. *)
-let invfun_verif c l dorew gl =
- if not (isConst c) then error "given function is not a constant"
- else
- let x,_ = decompose_prod (pf_type_of gl c) in
- if List.length x = List.length l then
- try invfun c l dorew gl
- with UserError (x,y) -> raise (UserError (x,y))
- else error "wrong number of arguments for the function"
-
-
-
-
-(* Construction of the functional scheme. *)
-let buildFunscheme fonc mutflist =
- let def_fonc = expand_letins (def_of_const fonc) in
- let ftyp = type_of (Global.env ()) Evd.empty fonc in
- let _ = resetmeta() in
- let gl = mknewmeta() in
- let gl_app = applFull gl ftyp in
- let pis = prod_change_concl ftyp gl_app in
- (* Here we call the function invfun_proof, that effectively
- builds the scheme *)
-(* let princ_proof,levar,_,evararr,absc,parms = *)
- let _ = prstr "Recherche du principe... lancement de invfun_proof\n" in
- let pr = invfun_proof mutflist def_fonc [||] pis (Global.env()) Evd.empty in
- (* parameters are still there (unboud rel), and patternify must not take them
- -> lift*)
- let princ_proof_lift = lift (List.length pr.evarlist) pr.princ in
- let princ_proof_hyps =
- patternify (List.rev pr.evarlist) princ_proof_lift (Name (id_of_string "Hyp")) in
- let rec princ_replace_metas ev abs i t =
- if i>= Array.length ev then t
- else (* fix? *)
- princ_replace_metas ev abs (i+1)
- (mkLambda (
- (Name (id_of_string ("Q"^(string_of_int i)))),
- prod_change_concl (lift 0 abs.(i)) mkthesort,
- (substitterm 0 ev.(i) (mkRel 1) (lift 0 t))))
- in
- let rec princ_replace_params params t =
- List.fold_left (
- fun acc (ev,nam,typ) ->
- mkLambda (Name (id_of_name nam) , typ,
- substitterm 0 ev (mkRel 1) (lift 0 acc)))
- t (List.rev params) in
- if Array.length pr.mutfixmetas = 0 (* Is there a Fixpoint? *)
- then (* No Fixpoint *)
- princ_replace_params pr.params (mkLambda ((Name (id_of_string "Q")),
- prod_change_concl ftyp mkthesort,
- (substitterm 0 gl (mkRel 1) princ_proof_hyps)))
- else (* there is a fix -> add parameters + replace metas *)
- let princ_rpl =
- princ_replace_metas pr.mutfixmetas pr.conclarray 0 princ_proof_hyps in
- princ_replace_params pr.params princ_rpl
-
-
-
-(* Declaration of the functional scheme. *)
-let declareFunScheme f fname mutflist =
- let _ = prstr "Recherche du perincipe...\n" in
- let id_to_cstr id =
- try constr_of_id (Global.env()) id
- with
- Not_found -> error (string_of_id id ^ " not found in the environment") in
- let flist = if mutflist=[] then [f] else mutflist in
- let fcstrlist = Array.of_list (List.map id_to_cstr flist) in
- let idf = id_to_cstr f in
- let scheme = buildFunscheme idf fcstrlist in
- let _ = prstr "Principe:" in
- let _ = prconstr scheme in
- let ce = {
- const_entry_body = scheme;
- const_entry_type = None;
- const_entry_opaque = false;
- const_entry_boxed = true } in
- let _= ignore (declare_constant fname (DefinitionEntry ce,IsDefinition Scheme)) in
- ()
-
-
-
-TACTIC EXTEND functional_induction
- [ "old" "functional" "induction" constr(c) ne_constr_list(l) ]
- -> [ invfun_verif c l true ]
-END
-
-VERNAC COMMAND EXTEND FunctionalScheme
- [ "Old" "Functional" "Scheme" ident(na) ":=" "Induction" "for"
- ident(c) "with" ne_ident_list(l) ]
- -> [ declareFunScheme c na l ]
-| [ "Old" "Functional" "Scheme" ident(na) ":=" "Induction" "for" ident (c) ]
- -> [ declareFunScheme c na [] ]
-END
-
-
-
-
-
-(*
-*** Local Variables: ***
-*** compile-command: "make -C ../.. contrib/funind/tacinv.cmo" ***
-*** tuareg-default-indent:1 ***
-*** tuareg-begin-indent:1 ***
-*** tuareg-let-indent:1 ***
-*** tuareg-match-indent:-1 ***
-*** tuareg-try-indent:1 ***
-*** tuareg-with-indent:1 ***
-*** tuareg-if-then-else-inden:1 ***
-*** fill-column: 78 ***
-*** indent-tabs-mode: nil ***
-*** test-tactic: "../../bin/coqtop -translate -q -batch -load-vernac-source ../../test-suite/success/Funind.v" ***
-*** End: ***
-*)
-
-
diff --git a/contrib/funind/tacinvutils.ml b/contrib/funind/tacinvutils.ml
deleted file mode 100644
index ce775e0b..00000000
--- a/contrib/funind/tacinvutils.ml
+++ /dev/null
@@ -1,284 +0,0 @@
-(* tacinvutils.ml *)
-(*s utilities *)
-
-(*i*)
-open Names
-open Util
-open Term
-open Termops
-open Coqlib
-open Pp
-open Printer
-open Inductiveops
-open Environ
-open Declarations
-open Nameops
-open Evd
-open Sign
-open Reductionops
-(*i*)
-
-(*s printing of constr -- debugging *)
-
-(* comment this line to see debug msgs *)
-let msg x = () ;; let pr_lconstr c = str ""
- (* uncomment this to see debugging *)
-let prconstr c = msg (str" " ++ pr_lconstr c ++ str"\n")
-let prlistconstr lc = List.iter prconstr lc
-let prstr s = msg(str s)
-
-let prchr () = msg (str" (ret) \n")
-let prNamedConstr s c =
- begin
- msg(str "");
- msg(str(s^"==>\n ") ++ pr_lconstr c ++ str "\n<==\n");
- msg(str "");
- end
-
-let prNamedLConstr_aux lc =
- List.iter (prNamedConstr "#>") lc
-
-let prNamedLConstr s lc =
- begin
- prstr s;
- prNamedLConstr_aux lc
- end
-
-
-(* FIXME: ref 1, pas bon, si? *)
-let evarcpt = ref 0
-let metacpt = ref 0
-let mknewexist ()=
- begin
- evarcpt := !evarcpt+1;
- !evarcpt,[||]
- end
-
-let resetexist ()= evarcpt := 0
-
-let mknewmeta ()=
- begin
- metacpt := !metacpt+1;
- mkMeta (!metacpt)
- end
-
-let resetmeta () = metacpt := 0
-
-let rec mkevarmap_from_listex lex =
- match lex with
- | [] -> Evd.empty
- | ((ex,_),typ)::lex' ->
-(* let _ = prstr "mkevarmap" in
- let _ = prstr ("evar n. " ^ string_of_int ex ^ " ") in
- let _ = prstr "OF TYPE: " in
- let _ = prconstr typ in*)
- let info = {
- evar_concl = typ;
- evar_hyps = empty_named_context_val;
- evar_body = Evar_empty;
- evar_extra = None} in
- Evd.add (mkevarmap_from_listex lex') ex info
-
-let mkEq typ c1 c2 =
- mkApp (build_coq_eq(),[| typ; c1; c2|])
-
-let mkRefl typ c1 =
- mkApp ((build_coq_eq_data()).refl, [| typ; c1|])
-
-let rec popn i c = if i<=0 then c else pop (popn (i-1) c)
-
-
-(* Operations on names *)
-let id_of_name = function
- Anonymous -> id_of_string "H"
- | Name id -> id;;
-let string_of_name nme = string_of_id (id_of_name nme)
-let name_of_string str = Name (id_of_string str)
-let newname_append nme str =
- Name(id_of_string ((string_of_id (id_of_name nme))^str))
-
-(* Substitutions in constr *)
-
-let compare_constr_nosub t1 t2 =
- if compare_constr (fun _ _ -> false) t1 t2
- then true
- else false
-
-let rec compare_constr' t1 t2 =
- if compare_constr_nosub t1 t2
- then true
- else (compare_constr (compare_constr') t1 t2)
-
-let rec substitterm prof t by_t in_u =
- if (compare_constr' (lift prof t) in_u)
- then (lift prof by_t)
- else map_constr_with_binders succ
- (fun i -> substitterm i t by_t) prof in_u
-
-
-let apply_eqtrpl eq t =
- let r,(tb,b,by_t) = eq in
- substitterm 0 b by_t t
-
-let apply_eqtrpl_lt lt eq = List.map (apply_eqtrpl eq) lt
-
-let apply_leqtrpl_t t leq =
- List.fold_left (fun x y -> apply_eqtrpl y x) t leq
-
-
-let apply_refl_term eq t =
- let _,arr = destApp eq in
- let reli= (Array.get arr 1) in
- let by_t= (Array.get arr 2) in
- substitterm 0 reli by_t t
-
-let apply_eq_leqtrpl leq eq =
- List.map
- (function (r,(tb,b,t)) ->
- r,(tb,
- (if isRel b then b else (apply_refl_term eq b)), apply_refl_term eq t))
- leq
-
-
-
-(* [(a b c) a] -> true *)
-let constr_head_match u t=
- if isApp u
- then
- let uhd,args= destApp u in
- uhd=t
- else false
-
-(* My operations on constr *)
-let lift1L l = (List.map (lift 1) l)
-let mkArrow_lift t1 t2 = mkArrow t1 (lift 1 t2)
-let mkProd_liftc nme c1 c2 = mkProd (nme,c1,(lift 1 c2))
-(* prod_it_lift x [a1 a2 ...] *)
-let prod_it_lift ini lcpl =
- List.fold_right (function a,b -> (fun c -> mkProd_liftc a b c)) ini lcpl;;
-
-let prod_it_anonym_lift trm lst = List.fold_right mkArrow_lift lst trm
-
-let lam_it_anonymous trm lst =
- List.fold_right
- (fun elt res -> mkLambda(Name(id_of_string "Hrec"),elt,res)) lst trm
-
-let lambda_id id typeofid cstr =
- let cstr' = mkNamedLambda (id_of_string "FUNX") typeofid cstr in
- substitterm 0 id (mkRel 0) cstr'
-
-let prod_id id typeofid cstr =
- let cstr' = mkNamedProd (id_of_string "FUNX") typeofid cstr in
- substitterm 0 id (mkRel 0) cstr'
-
-
-
-
-
-let nth_dep_constructor indtype n =
- let sigma = Evd.empty and env = Global.env() in
- let indtypedef = find_rectype env sigma indtype in
- let indfam,_ = dest_ind_type indtypedef in
- let arr_cstr_summary = get_constructors env indfam in
- let cstr_sum = Array.get arr_cstr_summary n in
- build_dependent_constructor cstr_sum, cstr_sum.cs_nargs
-
-
-let rec buildrefl_from_eqs eqs =
- match eqs with
- | [] -> []
- | cstr::eqs' ->
- let eq,args = destApp cstr in
- (mkRefl (Array.get args 0) (Array.get args 2))
- :: (buildrefl_from_eqs eqs')
-
-
-
-
-(* list of occurrences of a term inside another *)
-(* Cofix will be wrong, not sure Fix is correct too *)
-let rec hdMatchSub u t=
- let subres =
- match kind_of_term u with
- | Lambda (nm,tp,cstr) | Prod (nm,tp,cstr) -> hdMatchSub (lift 1 cstr) t
- | Fix (_,(lna,tl,bl)) ->
- Array.fold_left
- (fun acc cstr -> acc @ hdMatchSub (lift (Array.length tl) cstr) t)
- [] bl
- | LetIn _ -> assert false
- (* Correct? *)
- | _ -> fold_constr (fun l cstr -> l @ hdMatchSub cstr t) [] u
- in
- if constr_head_match u t then u :: subres else subres
-
-
-(* let hdMatchSub_list u lt = List.flatten (List.map (hdMatchSub u) lt) *)
-let hdMatchSub_cpl u (d,f) =
- let res = ref [] in
- begin
- for i = d to f do res := hdMatchSub u (mkRel i) @ !res done;
- !res
- end
-
-
-(* destApplication raises an exception if [t] is not an application *)
-let exchange_hd_prod subst_hd t =
- let hd,args= destApplication t in mkApp (subst_hd,args)
-
-(* substitute t by by_t in head of products inside in_u, reduces each
- product found *)
-let rec substit_red prof t by_t in_u =
- if constr_head_match in_u (lift prof t)
- then
- let x = whd_beta (exchange_hd_prod (lift prof by_t) in_u) in
- x
- else
- map_constr_with_binders succ (fun i u -> substit_red i t by_t u) prof in_u
-
-(* [exchange_reli_arrayi t=(reli x y ...) tarr (d,f)] exchange each
- reli by tarr.(f-i). *)
-let exchange_reli_arrayi tarr (d,f) t =
- let hd,args= destApp t in
- let i = destRel hd in
- let res = whd_beta (mkApp (tarr.(f-i) ,args)) in
- res
-
-let exchange_reli_arrayi_L tarr (d,f) =
- List.map (exchange_reli_arrayi tarr (d,f))
-
-
-(* expand all letins in a term, before building the principle. *)
-let rec expand_letins mimick =
- match kind_of_term mimick with
- | LetIn(nme,cstr1, typ, cstr) ->
- let cstr' = substitterm 0 (mkRel 1) (lift 1 cstr1) cstr in
- expand_letins (pop cstr')
- | x -> map_constr expand_letins mimick
-
-
-(* Valeur d'une constante, or identity *)
-let def_of_const t =
- match kind_of_term t with
- | Const sp ->
- (try
- match Global.lookup_constant sp with
- {const_body=Some c} -> force c
- |_ -> assert false
- with _ -> assert false)
- | _ -> t
-
-(* nom d'une constante. Must be a constante. x*)
-let name_of_const t =
- match (kind_of_term t) with
- Const cst -> Names.string_of_label (Names.con_label cst)
- |_ -> assert false
- ;;
-
-
-(*i
-*** Local Variables:
-*** compile-command: "make -k tacinvutils.cmo"
-*** test-tactic: "../../bin/coqtop -translate -q -batch -load-vernac-source ../../test-suite/success/Funind.v"
-*** End:
-i*)
-
diff --git a/contrib/funind/tacinvutils.mli b/contrib/funind/tacinvutils.mli
deleted file mode 100644
index 64b21213..00000000
--- a/contrib/funind/tacinvutils.mli
+++ /dev/null
@@ -1,80 +0,0 @@
-(* tacinvutils.ml *)
-(*s utilities *)
-
-(*i*)
-open Termops
-open Equality
-open Names
-open Pp
-open Tacmach
-open Proof_type
-open Tacinterp
-open Tactics
-open Tacticals
-open Term
-open Util
-open Printer
-open Reductionops
-open Inductiveops
-open Coqlib
-open Refine
-open Evd
-(*i*)
-
-(* printing debugging *)
-val prconstr: constr -> unit
-val prlistconstr: constr list -> unit
-val prNamedConstr:string -> constr -> unit
-val prNamedLConstr:string -> constr list -> unit
-val prstr: string -> unit
-
-
-val mknewmeta: unit -> constr
-val mknewexist: unit -> existential
-val resetmeta: unit -> unit (* safe *)
-val resetexist: unit -> unit (* be careful with this one *)
-val mkevarmap_from_listex: (Term.existential * Term.types) list -> evar_map
-val mkEq: types -> constr -> constr -> constr
-(* let mkEq typ c1 c2 = mkApp (build_coq_eq_data.eq(),[| typ; c1; c2|]) *)
-val mkRefl: types -> constr -> constr
-val buildrefl_from_eqs: constr list -> constr list
-(* typ c1 = mkApp ((constant ["Coq"; "Init"; "Logic"] "refl_equal"), [| typ; c1|]) *)
-
-val nth_dep_constructor: constr -> int -> (constr*int)
-
-val prod_it_lift: (name*constr) list -> constr -> constr
-val prod_it_anonym_lift: constr -> constr list -> constr
-val lam_it_anonymous: constr -> constr list -> constr
-val lift1L: (constr list) -> constr list
-val popn: int -> constr -> constr
-val lambda_id: constr -> constr -> constr -> constr
-val prod_id: constr -> constr -> constr -> constr
-
-
-val name_of_string : string -> name
-val newname_append: name -> string -> name
-
-val apply_eqtrpl: constr*(constr*constr*constr) -> constr -> constr
-val substitterm: int -> constr -> constr -> constr -> constr
-val apply_leqtrpl_t:
- constr -> (constr*(constr*constr*constr)) list -> constr
-val apply_eq_leqtrpl:
- (constr*(constr*constr*constr)) list -> constr -> (constr*(constr*constr*constr)) list
-(* val apply_leq_lt: constr list -> constr list -> constr list *)
-
-val hdMatchSub: constr -> constr -> constr list
-val hdMatchSub_cpl: constr -> int*int -> constr list
-val exchange_hd_prod: constr -> constr -> constr
-val exchange_reli_arrayi_L: constr array -> int*int -> constr list -> constr list
-val substit_red: int -> constr -> constr -> constr -> constr
-val expand_letins: constr -> constr
-
-val def_of_const: constr -> constr
-val name_of_const: constr -> string
-
-(*i
- *** Local Variables: ***
- *** compile-command: "make -C ../.. contrib/funind/tacinvutils.cmi" ***
- *** End: ***
-i*)
-
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-09 19:59:42 +0000