summaryrefslogtreecommitdiff
path: root/contrib/funind
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/funind')
-rw-r--r--contrib/funind/functional_principles_proofs.ml206
-rw-r--r--contrib/funind/functional_principles_types.ml30
-rw-r--r--contrib/funind/indfun.ml328
-rw-r--r--contrib/funind/indfun_common.ml80
-rw-r--r--contrib/funind/indfun_common.mli16
-rw-r--r--contrib/funind/indfun_main.ml4134
-rw-r--r--contrib/funind/invfun.ml80
-rw-r--r--contrib/funind/merge.ml826
-rw-r--r--contrib/funind/rawterm_to_relation.ml86
-rw-r--r--contrib/funind/rawterm_to_relation.mli2
-rw-r--r--contrib/funind/rawtermops.ml96
-rw-r--r--contrib/funind/rawtermops.mli6
-rw-r--r--contrib/funind/tacinvutils.ml5
13 files changed, 1578 insertions, 317 deletions
diff --git a/contrib/funind/functional_principles_proofs.ml b/contrib/funind/functional_principles_proofs.ml
index 7977d4e0..14e2233f 100644
--- a/contrib/funind/functional_principles_proofs.ml
+++ b/contrib/funind/functional_principles_proofs.ml
@@ -39,12 +39,12 @@ let do_observe_tac s tac g =
Cerrors.explain_exn e ++ str " on goal " ++ goal );
raise e;;
-
-let observe_tac s tac g =
+let observe_tac_stream s tac g =
if do_observe ()
- then do_observe_tac (str s) tac g
+ then do_observe_tac s tac g
else tac g
+let observe_tac s tac g = observe_tac_stream (str s) tac g
let tclTRYD tac =
if !Options.debug || do_observe ()
@@ -179,10 +179,11 @@ let nf_betaiotazeta = (* Reductionops.local_strong Reductionops.whd_betaiotazeta
let change_eq env sigma hyp_id (context:Sign.rel_context) x t end_of_type =
let nochange msg =
begin
-(* observe (str ("Not treating ( "^msg^" )") ++ pr_lconstr t ); *)
+ observe (str ("Not treating ( "^msg^" )") ++ pr_lconstr t );
failwith "NoChange";
end
in
+ let eq_constr = Reductionops.is_conv env sigma in
if not (noccurn 1 end_of_type)
then nochange "dependent"; (* if end_of_type depends on this term we don't touch it *)
if not (isApp t) then nochange "not an equality";
@@ -194,6 +195,7 @@ let change_eq env sigma hyp_id (context:Sign.rel_context) x t end_of_type =
in
if not (closed0 t1) then nochange "not a closed lhs";
let rec compute_substitution sub t1 t2 =
+ observe (str "compute_substitution : " ++ pr_lconstr t1 ++ str " === " ++ pr_lconstr t2);
if isRel t2
then
let t2 = destRel t2 in
@@ -313,9 +315,13 @@ let h_reduce_with_zeta =
let rewrite_until_var arg_num eq_ids : tactic =
+ (* tests if the declares recursive argument is neither a Constructor nor
+ an applied Constructor since such a form for the recursive argument
+ will break the Guard when trying to save the Lemma.
+ *)
let test_var g =
let _,args = destApp (pf_concl g) in
- not (isConstruct args.(arg_num))
+ not ((isConstruct args.(arg_num)) || isAppConstruct args.(arg_num))
in
let rec do_rewrite eq_ids g =
if test_var g
@@ -499,7 +505,7 @@ let clean_goal_with_heq ptes_infos continue_tac dyn_infos =
tclTHENLIST
[
tac ;
- (continue_tac new_infos)
+ observe_tac "clean_hyp_with_heq continue" (continue_tac new_infos)
]
g
@@ -779,7 +785,7 @@ let build_proof
finish_proof dyn_infos)
in
observe_tac "build_proof"
- (build_proof do_finish_proof dyn_infos)
+ (build_proof (clean_goal_with_heq ptes_infos do_finish_proof) dyn_infos)
@@ -884,7 +890,8 @@ let generate_equation_lemma fnames f fun_num nb_params nb_args rec_args_num =
(* observe (str "f_body_with_params_and_other_fun " ++ pr_lconstr f_body_with_params_and_other_fun); *)
let eq_rhs = nf_betaiotazeta (mkApp(compose_lam params f_body_with_params_and_other_fun,Array.init (nb_params + nb_args) (fun i -> mkRel(nb_params + nb_args - i)))) in
(* observe (str "eq_rhs " ++ pr_lconstr eq_rhs); *)
- let type_ctxt,type_of_f = Sign.decompose_prod_n_assum (nb_params + nb_args) f_def.const_type in
+ let type_ctxt,type_of_f = Sign.decompose_prod_n_assum (nb_params + nb_args)
+ (Typeops.type_of_constant_type (Global.env()) f_def.const_type) in
let eqn = mkApp(Lazy.force eq,[|type_of_f;eq_lhs;eq_rhs|]) in
let lemma_type = it_mkProd_or_LetIn ~init:eqn type_ctxt in
let f_id = id_of_label (con_label (destConst f)) in
@@ -1332,10 +1339,11 @@ let new_prove_with_tcc is_mes acc_inv hrec tcc_lemma_constr eqs : tactic =
h_intro hid;
Elim.h_decompose_and (mkVar hid);
backtrack_eqs_until_hrec hrec eqs;
- tclCOMPLETE (tclTHENS (* We must have exactly ONE subgoal !*)
- (apply (mkVar hrec))
- [ tclTHENSEQ
- [
+ observe_tac ("new_prove_with_tcc ( applying "^(string_of_id hrec)^" )" )
+ (tclTHENS (* We must have exactly ONE subgoal !*)
+ (apply (mkVar hrec))
+ [ tclTHENSEQ
+ [
thin [hrec];
apply (Lazy.force acc_inv);
(fun g ->
@@ -1344,11 +1352,12 @@ let new_prove_with_tcc is_mes acc_inv hrec tcc_lemma_constr eqs : tactic =
unfold_in_concl [([], evaluable_of_global_reference (delayed_force ltof_ref))] g
else tclIDTAC g
);
- tclTRY(Recdef.list_rewrite true eqs);
- observe_tac "finishing" (tclCOMPLETE (Eauto.gen_eauto false (false,5) [] (Some [])))
+ observe_tac "rew_and_finish"
+ (tclTHEN
+ (tclTRY(Recdef.list_rewrite true eqs))
+ (observe_tac "finishing" (tclCOMPLETE (Eauto.gen_eauto false (false,5) [] (Some [])))))
]
- ]
- )
+ ])
])
gls
@@ -1371,7 +1380,7 @@ let is_valid_hypothesis predicates_name =
| _ -> false
in
is_valid_hypothesis
-
+(*
let fresh_id avoid na =
let id =
match na with
@@ -1450,7 +1459,7 @@ let prove_principle_for_gen
let wf_tac =
if is_mes
then
- Recdef.tclUSER_if_not_mes
+ (fun b -> Recdef.tclUSER_if_not_mes b None)
else fun _ -> prove_with_tcc tcc_lemma_ref []
in
let start_tac g =
@@ -1543,7 +1552,7 @@ let prove_principle_for_gen
let pte_info =
{ proving_tac =
(fun eqs ->
- observe_tac "prove_with_tcc"
+ observe_tac "new_prove_with_tcc"
(new_prove_with_tcc is_mes acc_inv hrec tcc_lemma_ref (List.map mkVar eqs))
);
is_valid = is_valid_hypothesis predicates_names
@@ -1583,13 +1592,160 @@ let prove_principle_for_gen
arg_tac;
start_tac
] g
+*)
-
-
-
-
-
-
+let prove_principle_for_gen
+ (f_ref,functional_ref,eq_ref) tcc_lemma_ref is_mes
+ rec_arg_num rec_arg_type relation gl =
+ let princ_type = pf_concl gl in
+ let princ_info = compute_elim_sig princ_type in
+ let fresh_id =
+ let avoid = ref (pf_ids_of_hyps gl) in
+ fun na ->
+ let new_id =
+ match na with
+ | Name id -> fresh_id !avoid (string_of_id id)
+ | Anonymous -> fresh_id !avoid "H"
+ in
+ avoid := new_id :: !avoid;
+ Name new_id
+ in
+ let fresh_decl (na,b,t) = (fresh_id na,b,t) in
+ let princ_info : elim_scheme =
+ { princ_info with
+ params = List.map fresh_decl princ_info.params;
+ predicates = List.map fresh_decl princ_info.predicates;
+ branches = List.map fresh_decl princ_info.branches;
+ args = List.map fresh_decl princ_info.args
+ }
+ in
+ let wf_tac =
+ if is_mes
+ then
+ (fun b -> Recdef.tclUSER_if_not_mes b None)
+ else fun _ -> prove_with_tcc tcc_lemma_ref []
+ in
+ let real_rec_arg_num = rec_arg_num - princ_info.nparams in
+ let npost_rec_arg = princ_info.nargs - real_rec_arg_num + 1 in
+ let (post_rec_arg,pre_rec_arg) =
+ Util.list_chop npost_rec_arg princ_info.args
+ in
+ let rec_arg_id =
+ match post_rec_arg with
+ | (Name id,_,_)::_ -> id
+ | _ -> assert false
+ in
+ let subst_constrs = List.map (fun (na,_,_) -> mkVar (Nameops.out_name na)) (pre_rec_arg@princ_info.params) in
+ let relation = substl subst_constrs relation in
+ let input_type = substl subst_constrs rec_arg_type in
+ let wf_thm_id = Nameops.out_name (fresh_id (Name (id_of_string "wf_R"))) in
+ let acc_rec_arg_id =
+ Nameops.out_name (fresh_id (Name (id_of_string ("Acc_"^(string_of_id rec_arg_id)))))
+ in
+ let revert l =
+ tclTHEN (h_generalize (List.map mkVar l)) (clear l)
+ in
+ let fix_id = Nameops.out_name (fresh_id (Name hrec_id)) in
+ let prove_rec_arg_acc g =
+ (observe_tac "prove_rec_arg_acc"
+ (tclCOMPLETE
+ (tclTHEN
+ (forward
+ (Some ((fun g -> observe_tac "prove wf" (tclCOMPLETE (wf_tac is_mes)) g)))
+ (Genarg.IntroIdentifier wf_thm_id)
+ (mkApp (delayed_force well_founded,[|input_type;relation|])))
+ (
+ observe_tac
+ "apply wf_thm"
+ (h_apply ((mkApp(mkVar wf_thm_id,
+ [|mkVar rec_arg_id |])),Rawterm.NoBindings)
+ )
+ )
+ )
+ )
+ )
+ g
+ in
+ let args_ids = List.map (fun (na,_,_) -> Nameops.out_name na) princ_info.args in
+ tclTHENSEQ
+ [
+ h_intros
+ (List.rev_map (fun (na,_,_) -> Nameops.out_name na)
+ (princ_info.args@princ_info.branches@princ_info.predicates@princ_info.params)
+ );
+ observe_tac "" (forward
+ (Some (prove_rec_arg_acc))
+ (Genarg.IntroIdentifier acc_rec_arg_id)
+ (mkApp (delayed_force acc_rel,[|input_type;relation;mkVar rec_arg_id|]))
+ );
+ observe_tac "reverting" (revert (List.rev (acc_rec_arg_id::args_ids)));
+ observe_tac "h_fix" (h_fix (Some fix_id) (real_rec_arg_num + 1));
+ h_intros (List.rev (acc_rec_arg_id::args_ids));
+ Equality.rewriteLR (mkConst eq_ref);
+ observe_tac "finish" (fun gl' ->
+ let body =
+ let _,args = destApp (pf_concl gl') in
+ array_last args
+ in
+ let body_info rec_hyps =
+ {
+ nb_rec_hyps = List.length rec_hyps;
+ rec_hyps = rec_hyps;
+ eq_hyps = [];
+ info = body
+ }
+ in
+ let acc_inv =
+ lazy (
+ mkApp (
+ delayed_force acc_inv_id,
+ [|input_type;relation;mkVar rec_arg_id|]
+ )
+ )
+ in
+ let acc_inv = lazy (mkApp(Lazy.force acc_inv, [|mkVar acc_rec_arg_id|])) in
+ let predicates_names =
+ List.map (fun (na,_,_) -> Nameops.out_name na) princ_info.predicates
+ in
+ let pte_info =
+ { proving_tac =
+ (fun eqs ->
+ observe_tac "new_prove_with_tcc"
+ (new_prove_with_tcc
+ is_mes acc_inv fix_id tcc_lemma_ref (List.map mkVar eqs)
+ )
+ );
+ is_valid = is_valid_hypothesis predicates_names
+ }
+ in
+ let ptes_info : pte_info Idmap.t =
+ List.fold_left
+ (fun map pte_id ->
+ Idmap.add pte_id
+ pte_info
+ map
+ )
+ Idmap.empty
+ predicates_names
+ in
+ let make_proof rec_hyps =
+ build_proof
+ false
+ [f_ref]
+ ptes_info
+ (body_info rec_hyps)
+ in
+ observe_tac "instanciate_hyps_with_args"
+ (instanciate_hyps_with_args
+ make_proof
+ (List.map (fun (na,_,_) -> Nameops.out_name na) princ_info.branches)
+ (List.rev args_ids)
+ )
+ gl'
+ )
+
+ ]
+ gl
diff --git a/contrib/funind/functional_principles_types.ml b/contrib/funind/functional_principles_types.ml
index f83eae8d..89ebb75a 100644
--- a/contrib/funind/functional_principles_types.ml
+++ b/contrib/funind/functional_principles_types.ml
@@ -301,9 +301,18 @@ let pp_dur time time' =
str (string_of_float (System.time_difference time time'))
(* let qed () = save_named true *)
-let defined () = Command.save_named false
-
-
+let defined () =
+ try
+ Command.save_named false
+ with
+ | UserError("extract_proof",msg) ->
+ Util.errorlabstrm
+ "defined"
+ ((try
+ str "On goal : " ++ fnl () ++ pr_open_subgoals () ++ fnl ()
+ with _ -> mt ()
+ ) ++msg)
+ | e -> raise e
@@ -346,6 +355,7 @@ let generate_functional_principle
interactive_proof
old_princ_type sorts new_princ_name funs i proof_tac
=
+ try
let f = funs.(i) in
let type_sort = Termops.new_sort_in_family InType in
let new_sorts =
@@ -384,6 +394,9 @@ let generate_functional_principle
Decl_kinds.IsDefinition (Decl_kinds.Scheme)
)
);
+ Options.if_verbose
+ (fun id -> Pp.msgnl (Ppconstr.pr_id id ++ str " is defined"))
+ name;
names := name :: !names
in
register_with_sort InProp;
@@ -393,6 +406,10 @@ let generate_functional_principle
build_functional_principle interactive_proof old_princ_type new_sorts funs i proof_tac hook
in
save false new_princ_name entry g_kind hook
+ with
+ | Defining_principle _ as e -> raise e
+ | e -> raise (Defining_principle e)
+
(* defined () *)
@@ -591,13 +608,6 @@ let make_scheme (fas : (constant*Rawterm.rawsort) list) : Entries.definition_ent
const::other_result
let build_scheme fas =
-(* (fun (f,_) -> *)
-(* try Libnames.constr_of_global (Nametab.global f) *)
-(* with Not_found -> *)
-(* Util.error ("Cannot find "^ Libnames.string_of_reference f) *)
-(* ) *)
-(* fas *)
-
let bodies_types =
make_scheme
(List.map
diff --git a/contrib/funind/indfun.ml b/contrib/funind/indfun.ml
index dffc8120..82bb2869 100644
--- a/contrib/funind/indfun.ml
+++ b/contrib/funind/indfun.ml
@@ -39,7 +39,8 @@ let functional_induction with_clean c princl pat =
let finfo = (* we first try to find out a graph on f *)
try find_Function_infos c'
with Not_found ->
- errorlabstrm "" (str "Cannot find induction information on "++Printer.pr_lconstr (mkConst c') )
+ errorlabstrm "" (str "Cannot find induction information on "++
+ Printer.pr_lconstr (mkConst c') )
in
match Tacticals.elimination_sort_of_goal g with
| InProp -> finfo.prop_lemma
@@ -49,8 +50,9 @@ let functional_induction with_clean c princl pat =
let princ = (* then we get the principle *)
try mkConst (out_some princ_option )
with Failure "out_some" ->
- (*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*)
+ (*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*)
let princ_name =
Indrec.make_elimination_ident
(id_of_label (con_label c'))
@@ -90,45 +92,45 @@ let functional_induction with_clean c princl pat =
let old_idl = List.fold_right Idset.add (Tacmach.pf_ids_of_hyps g) Idset.empty in
let old_idl = Idset.diff old_idl princ_vars in
let subst_and_reduce g =
- let idl =
- map_succeed
- (fun id ->
- if Idset.mem id old_idl then failwith "subst_and_reduce";
- id
- )
- (Tacmach.pf_ids_of_hyps g)
- in
- let flag =
- Rawterm.Cbv
- {Rawterm.all_flags
- with Rawterm.rDelta = false;
- }
- in
if with_clean
then
+ let idl =
+ map_succeed
+ (fun id ->
+ if Idset.mem id old_idl then failwith "subst_and_reduce";
+ id
+ )
+ (Tacmach.pf_ids_of_hyps g)
+ in
+ let flag =
+ Rawterm.Cbv
+ {Rawterm.all_flags
+ with Rawterm.rDelta = false;
+ }
+ in
Tacticals.tclTHEN
(Tacticals.tclMAP (fun id -> Tacticals.tclTRY (Equality.subst [id])) idl )
(Hiddentac.h_reduce flag Tacticals.allClauses)
g
else Tacticals.tclIDTAC g
-
+
in
Tacticals.tclTHEN
(choose_dest_or_ind
- princ_infos
- args_as_induction_constr
- princ'
- pat)
+ princ_infos
+ args_as_induction_constr
+ princ'
+ pat)
subst_and_reduce
g
-
-
+
+
type annot =
Struct of identifier
- | Wf of Topconstr.constr_expr * identifier option
- | Mes of Topconstr.constr_expr * identifier option
+ | Wf of Topconstr.constr_expr * identifier option * Topconstr.constr_expr list
+ | Mes of Topconstr.constr_expr * identifier option * Topconstr.constr_expr list
type newfixpoint_expr =
@@ -184,7 +186,7 @@ let build_newrecursive
States.unfreeze fs; raise e in
States.unfreeze fs; def
in
- recdef
+ recdef,rec_impls
let compute_annot (name,annot,args,types,body) =
@@ -238,29 +240,47 @@ let prepare_body (name,annot,args,types,body) rt =
(fun_args,rt')
-let derive_inversion fix_names =
- try
- Invfun.derive_correctness
- Functional_principles_types.make_scheme
- functional_induction
- (List.map (fun id -> destConst (Tacinterp.constr_of_id (Global.env ()) id)) fix_names)
- (*i The next call to mk_rel_id is valid since we have just construct the graph
- Ensures by : register_built
- i*)
- (List.map (fun id -> destInd (Tacinterp.constr_of_id (Global.env ()) (mk_rel_id id))) fix_names)
- with e ->
- msg_warning (str "Cannot define correction of function and graph" ++ Cerrors.explain_exn e)
-
+let derive_inversion fix_names =
+ try
+ (* we first transform the fix_names identifier into their corresponding constant *)
+ let fix_names_as_constant =
+ List.map (fun id -> destConst (Tacinterp.constr_of_id (Global.env ()) id)) fix_names
+ in
+ (*
+ Then we check that the graphs have been defined
+ If one of the graphs haven't been defined
+ we do nothing
+ *)
+ List.iter (fun c -> ignore (find_Function_infos c)) fix_names_as_constant ;
+ try
+ Invfun.derive_correctness
+ Functional_principles_types.make_scheme
+ functional_induction
+ fix_names_as_constant
+ (*i The next call to mk_rel_id is valid since we have just construct the graph
+ Ensures by : register_built
+ i*)
+ (List.map
+ (fun id -> destInd (Tacinterp.constr_of_id (Global.env ()) (mk_rel_id id)))
+ fix_names
+ )
+ with e ->
+ msg_warning
+ (str "Cannot built inversion information" ++
+ if do_observe () then Cerrors.explain_exn e else mt ())
+ with _ -> ()
+
let generate_principle
- do_built fix_rec_l recdefs interactive_proof parametrize
- (continue_proof : int -> Names.constant array -> Term.constr array -> int -> Tacmach.tactic) : unit =
+ 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 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
try
(* We then register the Inductive graphs of the functions *)
- Rawterm_to_relation.build_inductive parametrize names funs_args funs_types recdefs;
+ Rawterm_to_relation.build_inductive names funs_args funs_types recdefs;
if do_built
then
begin
@@ -286,8 +306,7 @@ let generate_principle
list_map_i
(fun i x ->
let princ = destConst (Indrec.lookup_eliminator (ind_kn,i) (InProp)) in
- let princ_type =
- (Global.lookup_constant princ).Declarations.const_type
+ let princ_type = Typeops.type_of_constant (Global.env()) princ
in
Functional_principles_types.generate_functional_principle
interactive_proof
@@ -301,12 +320,22 @@ let generate_principle
0
fix_rec_l
in
- Array.iter add_Function funs_kn;
+ Array.iter (add_Function is_general) funs_kn;
()
end
with e ->
- Pp.msg_warning (Cerrors.explain_exn e)
-
+ match e with
+ | Building_graph e ->
+ Pp.msg_warning
+ (str "Cannot define graph(s) for " ++
+ h 1 (prlist_with_sep (fun _ -> str","++spc ()) Ppconstr.pr_id names) ++
+ if do_observe () then (spc () ++ Cerrors.explain_exn e) else mt ())
+ | Defining_principle e ->
+ Pp.msg_warning
+ (str "Cannot define principle(s) for "++
+ h 1 (prlist_with_sep (fun _ -> str","++spc ()) Ppconstr.pr_id names) ++
+ if do_observe () then Cerrors.explain_exn e else mt ())
+ | _ -> anomaly ""
let register_struct is_rec fixpoint_exprl =
match fixpoint_exprl with
@@ -330,7 +359,7 @@ let generate_correction_proof_wf f_ref tcc_lemma_ref
tcc_lemma_ref is_mes rec_arg_num rec_arg_type relation
-let register_wf ?(is_mes=false) fname wf_rel_expr wf_arg args ret_type body
+let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas args ret_type body
pre_hook
=
let type_of_f = Command.generalize_constr_expr ret_type args in
@@ -349,13 +378,13 @@ let register_wf ?(is_mes=false) fname wf_rel_expr wf_arg args ret_type body
in
let unbounded_eq =
let f_app_args =
- Topconstr.CApp
+ Topconstr.CAppExpl
(dummy_loc,
- (None,Topconstr.mkIdentC fname) ,
+ (None,(Ident (dummy_loc,fname))) ,
(List.map
(function
| _,Anonymous -> assert false
- | _,Name e -> (Topconstr.mkIdentC e,None)
+ | _,Name e -> (Topconstr.mkIdentC e)
)
(Topconstr.names_of_local_assums args)
)
@@ -365,7 +394,8 @@ let register_wf ?(is_mes=false) fname wf_rel_expr wf_arg args ret_type body
[(f_app_args,None);(body,None)])
in
let eq = Command.generalize_constr_expr unbounded_eq args in
- let hook f_ref tcc_lemma_ref functional_ref eq_ref rec_arg_num rec_arg_type nb_args relation =
+ let hook f_ref tcc_lemma_ref functional_ref eq_ref rec_arg_num rec_arg_type
+ nb_args relation =
try
pre_hook
(generate_correction_proof_wf f_ref tcc_lemma_ref is_mes
@@ -377,15 +407,16 @@ let register_wf ?(is_mes=false) fname wf_rel_expr wf_arg args ret_type body
()
in
Recdef.recursive_definition
- is_mes fname
+ is_mes fname rec_impls
type_of_f
wf_rel_expr
rec_arg_num
eq
hook
+ using_lemmas
-let register_mes fname wf_mes_expr wf_arg args ret_type body =
+let register_mes fname rec_impls wf_mes_expr wf_arg using_lemmas args ret_type body =
let wf_arg_type,wf_arg =
match wf_arg with
| None ->
@@ -424,35 +455,38 @@ let register_mes fname wf_mes_expr wf_arg args ret_type body =
let wf_rel_from_mes =
Topconstr.mkAppC(Topconstr.mkRefC ltof,[wf_arg_type;fun_from_mes])
in
- register_wf ~is_mes:true fname wf_rel_from_mes (Some wf_arg) args ret_type body
+ register_wf ~is_mes:true fname rec_impls wf_rel_from_mes (Some wf_arg)
+ using_lemmas args ret_type body
let do_generate_principle register_built interactive_proof fixpoint_exprl =
- let recdefs = build_newrecursive fixpoint_exprl in
+ let recdefs,rec_impls = build_newrecursive fixpoint_exprl in
let _is_struct =
match fixpoint_exprl with
- | [((name,Some (Wf (wf_rel,wf_x)),args,types,body))] ->
+ | [((name,Some (Wf (wf_rel,wf_x,using_lemmas)),args,types,body))] ->
let pre_hook =
generate_principle
+ true
register_built
fixpoint_exprl
recdefs
true
- false
in
- if register_built then register_wf name wf_rel wf_x args types body pre_hook;
+ 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)),args,types,body))] ->
+ | [((name,Some (Mes (wf_mes,wf_x,using_lemmas)),args,types,body))] ->
let pre_hook =
generate_principle
+ true
register_built
fixpoint_exprl
recdefs
true
- false
in
- if register_built then register_mes name wf_mes wf_x args types body pre_hook;
- false
+ if register_built
+ then register_mes name rec_impls wf_mes wf_x using_lemmas args types body pre_hook;
+ true
| _ ->
let fix_names =
List.map (function (name,_,_,_,_) -> name) fixpoint_exprl
@@ -469,7 +503,9 @@ let do_generate_principle register_built interactive_proof fixpoint_exprl =
in
let annot =
try Some (list_index (Name id) names - 1), Topconstr.CStructRec
- with Not_found -> raise (UserError("",str "Cannot find argument " ++ Ppconstr.pr_id id))
+ with Not_found ->
+ raise (UserError("",str "Cannot find argument " ++
+ Ppconstr.pr_id id))
in
(name,annot,args,types,body),(None:Vernacexpr.decl_notation)
| (name,None,args,types,body),recdef ->
@@ -479,10 +515,11 @@ let do_generate_principle register_built interactive_proof fixpoint_exprl =
(dummy_loc,"Function",
Pp.str "the recursive argument needs to be specified in Function")
else
- (name,(Some 0, Topconstr.CStructRec),args,types,body),(None:Vernacexpr.decl_notation)
+ (name,(Some 0, Topconstr.CStructRec),args,types,body),
+ (None:Vernacexpr.decl_notation)
| (_,Some (Wf _),_,_,_),_ | (_,Some (Mes _),_,_,_),_->
error
- ("Cannot use mutual definition with well-founded recursion")
+ ("Cannot use mutual definition with well-founded recursion or measure")
)
(List.combine fixpoint_exprl recdefs)
in
@@ -493,13 +530,13 @@ let do_generate_principle register_built interactive_proof fixpoint_exprl =
let is_rec = List.exists (is_rec fix_names) recdefs in
if register_built then register_struct is_rec old_fixpoint_exprl;
generate_principle
+ false
register_built
fixpoint_exprl
recdefs
interactive_proof
- true
(Functional_principles_proofs.prove_princ_for_struct interactive_proof);
- if register_built then derive_inversion fix_names;
+ if register_built then derive_inversion fix_names;
true;
in
()
@@ -517,9 +554,13 @@ let rec add_args id new_args b =
| CArrow(loc,b1,b2) ->
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, add_args id new_args b1)
+ CProdN(loc,
+ List.map (fun (nal,b2) -> (nal,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, add_args id new_args b1)
+ CLambdaN(loc,
+ List.map (fun (nal,b2) -> (nal,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)
| CAppExpl(loc,(pf,r),exprl) ->
@@ -530,10 +571,13 @@ let rec add_args id new_args b =
| _ -> CAppExpl(loc,(pf,r),List.map (add_args id new_args) exprl)
end
| 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)
+ 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,
- List.map (fun (b,(na,b_option)) -> add_args id new_args b,(na,option_map (add_args id new_args) b_option)) cel,
+ List.map (fun (b,(na,b_option)) ->
+ add_args id new_args b,
+ (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) ->
@@ -558,7 +602,63 @@ let rec add_args id new_args b =
| CPrim _ -> b
| CDelimiters _ -> anomaly "add_args : CDelimiters"
| CDynamic _ -> anomaly "add_args : CDynamic"
+exception Stop of Topconstr.constr_expr
+
+
+(* [chop_n_arrow n t] chops the [n] first arrows in [t]
+ Acts on Topconstr.constr_expr
+*)
+let rec chop_n_arrow n t =
+ if n <= 0
+ then t (* If we have already removed all the arrows then return the type *)
+ else (* If not we check the form of [t] *)
+ match t with
+ | Topconstr.CArrow(_,_,t) -> (* If we have an arrow, we discard it and recall [chop_n_arrow] *)
+ chop_n_arrow (n-1) t
+ | Topconstr.CProdN(_,nal_ta',t') -> (* If we have a forall, to result are possible :
+ either we need to discard more than the number of arrows contained
+ in this product declaration then we just recall [chop_n_arrow] on
+ the remaining number of arrow to chop and [t'] we discard it and
+ recall [chop_n_arrow], either this product contains more arrows
+ than the number we need to chop and then we return the new type
+ *)
+ begin
+ try
+ let new_n =
+ let rec aux (n:int) = function
+ [] -> n
+ | (nal,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')
+ in
+ raise (Stop new_t')
+ in
+ aux n nal_ta'
+ in
+ chop_n_arrow new_n t'
+ with Stop t -> t
+ end
+ | _ -> anomaly "Not enough products"
+
+let rec get_args b t : Topconstr.local_binder list *
+ Topconstr.constr_expr * Topconstr.constr_expr =
+ match b with
+ | Topconstr.CLambdaN (loc, (nal_ta), b') ->
+ begin
+ let n =
+ (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''
+ end
+ | _ -> [],b,t
let make_graph (f_ref:global_reference) =
@@ -578,68 +678,14 @@ let make_graph (f_ref:global_reference) =
let env = Global.env () in
let body = (force b) in
let extern_body,extern_type =
- 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;
- Impargs.make_implicit_args false;
- Impargs.make_strict_implicit_args false;
- Impargs.make_contextual_implicit_args false;
- try
- let res = Constrextern.extern_constr false env body in
- let res' = Constrextern.extern_type false env c_body.const_type 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;
- res,res'
- with
- | UserError(s,msg) as 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;
- raise e
- | 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;
- raise e
- in
- let rec get_args b t : Topconstr.local_binder list *
- Topconstr.constr_expr * Topconstr.constr_expr =
-(* Pp.msgnl (str "body: " ++Ppconstr.pr_lconstr_expr b); *)
-(* Pp.msgnl (str "type: " ++ Ppconstr.pr_lconstr_expr t); *)
-(* Pp.msgnl (fnl ()); *)
- match b with
- | Topconstr.CLambdaN (loc, (nal_ta), b') ->
- begin
- let n =
- (List.fold_left (fun n (nal,_) ->
- n+List.length nal) 0 nal_ta )
- in
- let rec chop_n_arrow n t =
- if n > 0
- then
- match t with
- | Topconstr.CArrow(_,_,t) -> chop_n_arrow (n-1) t
- | Topconstr.CProdN(_,nal_ta',t') ->
- let n' =
- List.fold_left
- (fun n (nal,t'') ->
- n+List.length nal) n nal_ta'
- in
-(* assert (n'<= n); *)
- chop_n_arrow (n - n') t'
- | _ -> anomaly "Not enough products"
- else t
- 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''
- end
- | _ -> [],b,t
+ with_full_print
+ (fun () ->
+ (Constrextern.extern_constr false env body,
+ Constrextern.extern_type false env
+ (Typeops.type_of_constant_type env c_body.const_type)
+ )
+ )
+ ()
in
let (nal_tas,b,t) = get_args extern_body extern_type in
let expr_list =
@@ -659,7 +705,8 @@ let make_graph (f_ref:global_reference) =
)
in
let rec_id =
- match List.nth bl' (out_some n) with |(_,Name id) -> id | _ -> anomaly ""
+ match List.nth bl' (out_some n) with
+ |(_,Name id) -> id | _ -> anomaly ""
in
let new_args =
List.flatten
@@ -667,7 +714,10 @@ let make_graph (f_ref:global_reference) =
(function
| Topconstr.LocalRawDef (na,_)-> []
| Topconstr.LocalRawAssum (nal,_) ->
- List.map (fun (loc,n) -> CRef(Libnames.Ident(loc, Nameops.out_name n))) nal
+ List.map
+ (fun (loc,n) ->
+ CRef(Libnames.Ident(loc, Nameops.out_name n)))
+ nal
)
nal_tas
)
@@ -685,7 +735,9 @@ let make_graph (f_ref:global_reference) =
do_generate_principle false false expr_list;
(* We register the infos *)
let mp,dp,_ = repr_con c in
- List.iter (fun (id,_,_,_,_) -> add_Function (make_con mp dp (label_of_id id))) expr_list
+ List.iter
+ (fun (id,_,_,_,_) -> add_Function false (make_con mp dp (label_of_id id)))
+ expr_list
(* let make_graph _ = assert false *)
diff --git a/contrib/funind/indfun_common.ml b/contrib/funind/indfun_common.ml
index f41aac20..13b242d5 100644
--- a/contrib/funind/indfun_common.ml
+++ b/contrib/funind/indfun_common.ml
@@ -5,8 +5,8 @@ open Libnames
let mk_prefix pre id = id_of_string (pre^(string_of_id id))
let mk_rel_id = mk_prefix "R_"
-let mk_correct_id id = Nameops.add_suffix id "_correct"
-let mk_complete_id id = Nameops.add_suffix id "_complete"
+let mk_correct_id id = Nameops.add_suffix (mk_rel_id id) "_correct"
+let mk_complete_id id = Nameops.add_suffix (mk_rel_id id) "_complete"
let mk_equation_id id = Nameops.add_suffix id "_equation"
let msgnl m =
@@ -233,6 +233,32 @@ let get_proof_clean do_reduce =
Pfedit.delete_current_proof ();
result
+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;
+ Impargs.make_implicit_args false;
+ Impargs.make_strict_implicit_args false;
+ Impargs.make_contextual_implicit_args 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;
+ 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;
+ raise e
+
+
+
@@ -248,14 +274,18 @@ type function_info =
rect_lemma : constant option;
rec_lemma : constant option;
prop_lemma : constant option;
+ is_general : bool; (* Has this function been defined using general recursive definition *)
}
-type function_db = function_info list
+(* type function_db = function_info list *)
+
+(* let function_table = ref ([] : function_db) *)
-let function_table = ref ([] : function_db)
-
+let from_function = ref Cmap.empty
+let from_graph = ref Indmap.empty
+(*
let rec do_cache_info finfo = function
| [] -> raise Not_found
| (finfo'::finfos as l) ->
@@ -274,6 +304,12 @@ let cache_Function (_,(finfos)) =
in
if new_tbl != !function_table
then function_table := new_tbl
+*)
+
+let cache_Function (_,finfos) =
+ from_function := Cmap.add finfos.function_constant finfos !from_function;
+ from_graph := Indmap.add finfos.graph_ind finfos !from_graph
+
let load_Function _ = cache_Function
let open_Function _ = cache_Function
@@ -307,6 +343,7 @@ let subst_Function (_,subst,finfos) =
rect_lemma = rect_lemma' ;
rec_lemma = rec_lemma';
prop_lemma = prop_lemma';
+ is_general = finfos.is_general
}
let classify_Function (_,infos) = Libobject.Substitute infos
@@ -342,6 +379,7 @@ let discharge_Function (_,finfos) =
rect_lemma = rect_lemma';
rec_lemma = rec_lemma';
prop_lemma = prop_lemma' ;
+ is_general = finfos.is_general
}
open Term
@@ -357,7 +395,8 @@ let pr_info f_info =
str "prop_lemma := " ++ (Util.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 l =
+let pr_table tb =
+ let l = Cmap.fold (fun k v acc -> v::acc) tb [] in
Util.prlist_with_sep fnl pr_info l
let in_Function,out_Function =
@@ -376,17 +415,16 @@ let in_Function,out_Function =
(* Synchronisation with reset *)
let freeze () =
- let tbl = !function_table in
-(* Pp.msgnl (str "freezing function_table : " ++ pr_table tbl); *)
- tbl
-
-let unfreeze l =
+ !from_function,!from_graph
+let unfreeze (functions,graphs) =
(* Pp.msgnl (str "unfreezing function_table : " ++ pr_table l); *)
- function_table :=
- l
+ from_function := functions;
+ from_graph := graphs
+
let init () =
(* Pp.msgnl (str "reseting function_table"); *)
- function_table := []
+ from_function := Cmap.empty;
+ from_graph := Indmap.empty
let _ =
Summary.declare_summary "functions_db_sum"
@@ -405,18 +443,18 @@ let find_or_none id =
let find_Function_infos f =
- List.find (fun finfo -> finfo.function_constant = f) !function_table
+ Cmap.find f !from_function
let find_Function_of_graph ind =
- List.find (fun finfo -> finfo.graph_ind = ind) !function_table
+ Indmap.find ind !from_graph
let update_Function finfo =
(* Pp.msgnl (pr_info finfo); *)
Lib.add_anonymous_leaf (in_Function finfo)
-let add_Function f =
+let add_Function is_general f =
let f_id = id_of_label (con_label f) in
let equation_lemma = find_or_none (mk_equation_id f_id)
and correctness_lemma = find_or_none (mk_correct_id f_id)
@@ -436,12 +474,14 @@ let add_Function f =
rect_lemma = rect_lemma;
rec_lemma = rec_lemma;
prop_lemma = prop_lemma;
- graph_ind = graph_ind
+ graph_ind = graph_ind;
+ is_general = is_general
+
}
in
update_Function finfos
-let pr_table () = pr_table !function_table
+let pr_table () = pr_table !from_function
(*********************************)
(* Debuging *)
let function_debug = ref false
@@ -464,3 +504,5 @@ let do_observe () =
+exception Building_graph of exn
+exception Defining_principle of exn
diff --git a/contrib/funind/indfun_common.mli b/contrib/funind/indfun_common.mli
index 00e1ce8d..7da1d6f0 100644
--- a/contrib/funind/indfun_common.mli
+++ b/contrib/funind/indfun_common.mli
@@ -73,6 +73,12 @@ val get_proof_clean : bool ->
+(* [with_full_print f a] applies [f] to [a] in full printing environment
+
+ This function preserves the print settings
+*)
+val with_full_print : ('a -> 'b) -> 'a -> 'b
+
(*****************)
@@ -86,12 +92,13 @@ type function_info =
rect_lemma : constant option;
rec_lemma : constant option;
prop_lemma : constant option;
+ is_general : bool;
}
val find_Function_infos : constant -> function_info
val find_Function_of_graph : inductive -> function_info
(* WARNING: To be used just after the graph definition !!! *)
-val add_Function : constant -> unit
+val add_Function : bool -> constant -> unit
val update_Function : function_info -> unit
@@ -101,5 +108,10 @@ val pr_info : function_info -> Pp.std_ppcmds
val pr_table : unit -> Pp.std_ppcmds
-val function_debug : bool ref
+(* val function_debug : bool ref *)
val do_observe : unit -> bool
+
+(* To localize pb *)
+exception Building_graph of exn
+exception Defining_principle of exn
+
diff --git a/contrib/funind/indfun_main.ml4 b/contrib/funind/indfun_main.ml4
index 00b5f28c..26a1066c 100644
--- a/contrib/funind/indfun_main.ml4
+++ b/contrib/funind/indfun_main.ml4
@@ -103,10 +103,28 @@ TACTIC EXTEND snewfunind
END
+let pr_constr_coma_sequence prc _ _ = Util.prlist_with_sep Util.pr_coma prc
+
+ARGUMENT EXTEND constr_coma_sequence'
+ TYPED AS constr_list
+ PRINTED BY pr_constr_coma_sequence
+| [ constr(c) "," constr_coma_sequence'(l) ] -> [ c::l ]
+| [ constr(c) ] -> [ [c] ]
+END
+
+let pr_auto_using prc _prlc _prt = Pptactic.pr_auto_using prc
+
+ARGUMENT EXTEND auto_using'
+ TYPED AS constr_list
+ PRINTED BY pr_auto_using
+| [ "using" constr_coma_sequence'(l) ] -> [ l ]
+| [ ] -> [ [] ]
+END
+
VERNAC ARGUMENT EXTEND rec_annotation2
[ "{" "struct" ident(id) "}"] -> [ Struct id ]
-| [ "{" "wf" constr(r) ident_opt(id) "}" ] -> [ Wf(r,id) ]
-| [ "{" "measure" constr(r) ident_opt(id) "}" ] -> [ Mes(r,id) ]
+| [ "{" "wf" constr(r) ident_opt(id) auto_using'(l) "}" ] -> [ Wf(r,id,l) ]
+| [ "{" "measure" constr(r) ident_opt(id) auto_using'(l) "}" ] -> [ Mes(r,id,l) ]
END
@@ -131,8 +149,8 @@ VERNAC ARGUMENT EXTEND rec_definition2
let check_exists_args an =
try
let id = match an with
- | Struct id -> id | Wf(_,Some id) -> id | Mes(_,Some id) -> id
- | Wf(_,None) | Mes(_,None) -> failwith "check_exists_args"
+ | 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
with Not_found -> Util.user_err_loc
@@ -214,11 +232,17 @@ END
(* FINDUCTION *)
(* comment this line to see debug msgs *)
-(* let msg x = () ;; let pr_lconstr c = str "" *)
+let msg x = () ;; let pr_lconstr c = str ""
(* uncomment this to see debugging *)
let prconstr c = msg (str" " ++ Printer.pr_lconstr c ++ str"\n")
let prlistconstr lc = List.iter prconstr lc
let prstr s = msg(str s)
+let prNamedConstr s c =
+ begin
+ msg(str "");
+ msg(str(s^"==>\n ") ++ Printer.pr_lconstr c ++ str "\n<==\n");
+ msg(str "");
+ end
@@ -266,6 +290,55 @@ let rec hdMatchSub inu (test: constr -> bool) : fapp_info list =
max_rel = max_rel; onlyvars = List.for_all isVar args }
::subres
+let mkEq typ c1 c2 =
+ mkApp (Coqlib.build_coq_eq(),[| 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)
+ (tclTHENFIRST
+ (Tactics.assert_as true IntroAnonymous (mkEq typ (mkVar idunsafe) cstr))
+ Tactics.reflexivity)
+ gl
+
+
+let poseq id cstr gl =
+ let x = Tactics.fresh_id [] id gl in
+ poseq_unsafe x cstr gl
+
+(* dirty? *)
+
+let list_constr_largs = ref []
+
+let rec poseq_list_ids_rec lcstr gl =
+ match lcstr with
+ | [] -> tclIDTAC gl
+ | c::lcstr' ->
+ match kind_of_term c with
+ | Var _ ->
+ (list_constr_largs:=c::!list_constr_largs ; poseq_list_ids_rec lcstr' gl)
+ | _ ->
+ let _ = prstr "c = " in
+ let _ = prconstr c in
+ let _ = prstr "\n" in
+ let typ = Tacmach.pf_type_of gl c in
+ let cname = Termops.id_of_name_using_hdchar (Global.env()) typ Anonymous in
+ let x = Tactics.fresh_id [] cname gl in
+ let _ = list_constr_largs:=mkVar x :: !list_constr_largs in
+ let _ = prstr " list_constr_largs = " in
+ let _ = prlistconstr !list_constr_largs in
+ let _ = prstr "\n" in
+
+ tclTHEN
+ (poseq_unsafe x c)
+ (poseq_list_ids_rec lcstr')
+ gl
+
+let poseq_list_ids lcstr gl =
+ let _ = list_constr_largs := [] in
+ poseq_list_ids_rec lcstr gl
(** [find_fapp test g] returns the list of [app_info] of all calls to
functions that satisfy [test] in the conclusion of goal g. Trivial
@@ -296,11 +369,17 @@ let finduction (oid:identifier option) (heuristic: fapp_info list -> fapp_info l
if List.length ordered_info_list = 0 then Util.error "function not found in goal\n";
let taclist: Proof_type.tactic list =
List.map
- (fun info ->
- (tclTHEN
- (functional_induction true (applist (info.fname, info.largs))
- None IntroAnonymous)
+ (fun info ->
+ (tclTHEN
+ (tclTHEN (poseq_list_ids info.largs)
+ (
+ fun gl ->
+ (functional_induction
+ true (applist (info.fname, List.rev !list_constr_largs))
+ None IntroAnonymous) gl))
nexttac)) ordered_info_list in
+ (* we try each (f t u v) until one does not fail *)
+ (* TODO: try also to mix functional schemes *)
tclFIRST taclist g
@@ -313,9 +392,8 @@ let chose_heuristic (oi:int option) : fapp_info list -> fapp_info list =
match oi with
| Some i -> (fun l -> [ List.nth l (i-1) ]) (* occurrence was given by the user *)
| None ->
- (* Default heuristic: keep only occurrence where all arguments
+ (* Default heuristic: put first occurrences where all arguments
are *bound* (meaning already introduced) variables *)
- (* TODO: put other funcalls at the end instead of deleting them *)
let ordering x y =
if x.free && x.onlyvars && y.free && y.onlyvars then 0 (* both pertinent *)
else if x.free && x.onlyvars then -1
@@ -325,6 +403,7 @@ let chose_heuristic (oi:int option) : fapp_info list -> fapp_info list =
List.sort ordering
+
TACTIC EXTEND finduction
["finduction" ident(id) natural_opt(oi)] ->
[
@@ -353,3 +432,36 @@ TACTIC EXTEND fauto
END
+
+TACTIC EXTEND poseq
+ [ "poseq" ident(x) constr(c) ] ->
+ [ poseq x c ]
+END
+
+VERNAC COMMAND EXTEND Showindinfo
+ [ "showindinfo" ident(x) ] -> [ Merge.showind x ]
+END
+
+VERNAC COMMAND EXTEND MergeFunind
+ [ "Mergeschemes" lconstr(c) "with" lconstr(c') "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)
+ ]
+END
diff --git a/contrib/funind/invfun.ml b/contrib/funind/invfun.ml
index 084ec7e0..04110ea9 100644
--- a/contrib/funind/invfun.ml
+++ b/contrib/funind/invfun.ml
@@ -44,25 +44,6 @@ let pr_with_bindings prc prlc (c,bl) =
let pr_constr_with_binding prc (c,bl) : Pp.std_ppcmds =
pr_with_bindings prc prc (c,bl)
-let pr_elim_scheme el =
- let env = Global.env () in
- let msg = str "params := " ++ Printer.pr_rel_context env el.params in
- let env = Environ.push_rel_context el.params env in
- let msg = msg ++ fnl () ++ str "predicates := "++ Printer.pr_rel_context env el.predicates in
- let env = Environ.push_rel_context el.predicates env in
- let msg = msg ++ fnl () ++ str "branches := " ++ Printer.pr_rel_context env el.branches in
- let env = Environ.push_rel_context el.branches env in
- let msg = msg ++ fnl () ++ str "args := " ++ Printer.pr_rel_context env el.args in
- let env = Environ.push_rel_context el.args env in
- let msg =
- Util.option_fold_right
- (fun o msg -> msg ++ fnl () ++ str "indarg := " ++ Printer.pr_rel_context env [o])
- el.indarg
- msg
- in
- let env = Util.option_fold_right (fun o env -> Environ.push_rel_context [o] env) el.indarg env in
- msg ++ fnl () ++ str "concl := " ++ Printer.pr_lconstr_env env el.concl
-
(* The local debuging mechanism *)
let msgnl = Pp.msgnl
@@ -120,7 +101,7 @@ let id_to_constr id =
let generate_type g_to_f f graph i =
(*i we deduce the number of arguments of the function and its returned type from the graph i*)
- let graph_arity = Inductive.type_of_inductive (Global.lookup_inductive (destInd graph)) in
+ let graph_arity = Inductive.type_of_inductive (Global.env()) (Global.lookup_inductive (destInd graph)) in
let ctxt,_ = decompose_prod_assum graph_arity in
let fun_ctxt,res_type =
match ctxt with
@@ -443,17 +424,17 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
let params_bindings,avoid =
List.fold_left2
(fun (bindings,avoid) (x,_,_) p ->
- let id = Termops.next_global_ident_away false (Nameops.out_name x) avoid in
+ let id = Nameops.next_ident_away (Nameops.out_name x) avoid in
(dummy_loc,Rawterm.NamedHyp id,p)::bindings,id::avoid
)
- ([],[])
+ ([],pf_ids_of_hyps g)
princ_infos.params
(List.rev params)
in
let lemmas_bindings =
List.rev (fst (List.fold_left2
(fun (bindings,avoid) (x,_,_) p ->
- let id = Termops.next_global_ident_away false (Nameops.out_name x) avoid in
+ let id = Nameops.next_ident_away (Nameops.out_name x) avoid in
(dummy_loc,Rawterm.NamedHyp id,nf_zeta p)::bindings,id::avoid)
([],avoid)
princ_infos.predicates
@@ -471,7 +452,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
(observe_tac "functional_induction" (
fun g ->
observe
- (str "princ" ++ pr_constr_with_binding (Printer.pr_lconstr_env (pf_env g)) (mkVar principle_id,bindings));
+ (pr_constr_with_binding (Printer.pr_lconstr_env (pf_env g)) (mkVar principle_id,bindings));
functional_induction false (applist(funs_constr.(i),List.map mkVar args_names))
(Some (mkVar principle_id,bindings))
pat g
@@ -493,6 +474,31 @@ let generalize_depedent_of x hyp g =
(pf_hyps g)
g
+
+
+
+
+
+let rec reflexivity_with_destruct_cases g =
+ let destruct_case () =
+ try
+ match kind_of_term (snd (destApp (pf_concl g))).(2) with
+ | Case(_,_,v,_) ->
+ tclTHENSEQ[
+ h_case (v,Rawterm.NoBindings);
+ intros;
+ observe_tac "reflexivity_with_destruct_cases" reflexivity_with_destruct_cases
+ ]
+ | _ -> reflexivity
+ with _ -> reflexivity
+ in
+ tclFIRST
+ [ reflexivity;
+ destruct_case ()
+ ]
+ g
+
+
(* [prove_fun_complete funs graphs schemes lemmas_types_infos i]
is the tactic used to prove completness lemma.
@@ -567,11 +573,12 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
*)
let rewrite_tac j ids : tactic =
let graph_def = graphs.(j) in
- if Rtree.is_infinite graph_def.mind_recargs
+ let infos = try find_Function_infos (destConst funcs.(j)) with Not_found -> error "No graph found" in
+ if infos.is_general || Rtree.is_infinite graph_def.mind_recargs
then
let eq_lemma =
- try out_some (find_Function_infos (destConst funcs.(j))).equation_lemma
- with Failure "out_some" | Not_found -> anomaly "Cannot find equation lemma"
+ try out_some (infos).equation_lemma
+ with Failure "out_some" -> anomaly "Cannot find equation lemma"
in
tclTHENSEQ[
tclMAP h_intro ids;
@@ -677,8 +684,8 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
observe_tac "rewrite_tac" (rewrite_tac this_ind_number this_branche_ids);
(* introduce hypothesis with some rewrite *)
(intros_with_rewrite);
- (* The proof is complete *)
- observe_tac "reflexivity" (reflexivity)
+ (* The proof is (almost) complete *)
+ observe_tac "reflexivity" (reflexivity_with_destruct_cases)
]
g
in
@@ -758,7 +765,7 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g
(Decl_kinds.Global,(Decl_kinds.Proof Decl_kinds.Theorem))
(fst lemmas_types_infos.(i))
(fun _ _ -> ());
- Pfedit.by (observe_tac ("procve correctness ("^(string_of_id f_id)^")") (proving_tac i));
+ Pfedit.by (observe_tac ("prove correctness ("^(string_of_id f_id)^")") (proving_tac i));
do_save ();
let finfo = find_Function_infos f_as_constant in
update_Function
@@ -968,10 +975,17 @@ let invfun qhyp f g =
functional_inversion kn hid f2 f_correct g
with
| Failure "" ->
- errorlabstrm "" (Ppconstr.pr_id hid ++ str " must contain at leat one function")
+ errorlabstrm "" (str "Hypothesis" ++ Ppconstr.pr_id hid ++ str " must contain at leat one Function")
| Failure "out_some" ->
- error "Cannot use equivalence with graph for any side of equality"
- | Not_found -> error "No graph found for any side of equality"
+ if do_observe ()
+ then
+ error "Cannot use equivalence with graph for any side of the equality"
+ else errorlabstrm "" (str "Cannot find inversion information for hypothesis " ++ Ppconstr.pr_id hid)
+ | Not_found ->
+ if do_observe ()
+ then
+ error "No graph found for any side of equality"
+ else errorlabstrm "" (str "Cannot find inversion information for hypothesis " ++ Ppconstr.pr_id hid)
end
| _ -> errorlabstrm "" (Ppconstr.pr_id hid ++ str " must be an equality ")
)
diff --git a/contrib/funind/merge.ml b/contrib/funind/merge.ml
new file mode 100644
index 00000000..1b796a81
--- /dev/null
+++ b/contrib/funind/merge.ml
@@ -0,0 +1,826 @@
+(************************************************************************)
+(* 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 *)
+(************************************************************************)
+
+(* Merging of induction principles. *)
+
+(*i $Id: i*)
+
+open Util
+open Topconstr
+open Vernacexpr
+open Pp
+open Names
+open Term
+open Declarations
+open Environ
+open Rawterm
+open Rawtermops
+
+(** {1 Utilities} *)
+
+(** {2 Useful operations on constr and rawconstr} *)
+
+(** 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 lift_ldecl n ldecl = List.map (fun (x,y) -> x,lift n y) ldecl
+
+let understand = Pretyping.Default.understand Evd.empty (Global.env())
+
+(** Operations on names and identifiers *)
+let id_of_name = function
+ Anonymous -> id_of_string "H"
+ | Name id -> id;;
+let name_of_string str = Name (id_of_string str)
+let string_of_name nme = string_of_id (id_of_name nme)
+
+(** [isVarf f x] returns [true] if term [x] is of the form [(Var f)]. *)
+let isVarf f x =
+ match x with
+ | RVar (_,x) -> Pervasives.compare x f = 0
+ | _ -> false
+
+(** [ident_global_exist id] returns true if identifier [id] is linked
+ in global environment. *)
+let ident_global_exist id =
+ try
+ let ans = CRef (Libnames.Ident (dummy_loc,id)) in
+ let _ = ignore (Constrintern.intern_constr Evd.empty (Global.env()) ans) in
+ true
+ with _ -> false
+
+(** [next_ident_fresh id] returns a fresh identifier (ie not linked in
+ global env) with base [id]. *)
+let next_ident_fresh (id:identifier) =
+ let res = ref id in
+ while ident_global_exist !res do res := Nameops.lift_ident !res done;
+ !res
+
+
+(** {2 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" " ++ Printer.pr_lconstr c)
+let prconstrnl c = msg (str" " ++ Printer.pr_lconstr c ++ str"\n")
+let prlistconstr lc = List.iter prconstr lc
+let prstr s = msg(str s)
+let prNamedConstr s c =
+ begin
+ msg(str "");
+ msg(str(s^" {§ ") ++ Printer.pr_lconstr c ++ str " §} ");
+ msg(str "");
+ end
+let prNamedRConstr s c =
+ begin
+ msg(str "");
+ msg(str(s^" {§ ") ++ Printer.pr_rawconstr c ++ str " §} ");
+ msg(str "");
+ end
+let prNamedLConstr_aux lc = List.iter (prNamedConstr "\n") lc
+let prNamedLConstr s lc =
+ begin
+ prstr "[§§§ ";
+ prstr s;
+ prNamedLConstr_aux lc;
+ prstr " §§§]\n";
+ end
+let prNamedLDecl s lc =
+ begin
+ prstr s; prstr "\n";
+ List.iter (fun (nm,_,tp) -> prNamedConstr (string_of_name nm) tp) lc;
+ prstr "\n";
+ end
+
+let showind (id:identifier) =
+ let cstrid = Tacinterp.constr_of_id (Global.env()) id in
+ let ind1,cstrlist = Inductiveops.find_inductive (Global.env()) Evd.empty cstrid in
+ let mib1,ib1 = Inductive.lookup_mind_specif (Global.env()) ind1 in
+ List.iter (fun (nm, optcstr, tp) ->
+ print_string (string_of_name nm^":");
+ prconstr tp; print_string "\n")
+ ib1.mind_arity_ctxt;
+ (match ib1.mind_arity with
+ | Monomorphic x ->
+ Printf.printf "arity :"; prconstr x.mind_user_arity
+ | Polymorphic x ->
+ Printf.printf "arity : universe?");
+ Array.iteri
+ (fun i x -> Printf.printf"type constr %d :" i ; prconstr x)
+ ib1.mind_user_lc
+
+(** {2 Misc} *)
+
+exception Found of int
+
+(* Array scanning *)
+let array_find (arr: 'a array) (pred: int -> 'a -> bool): int option =
+ try
+ for i=0 to Array.length arr - 1 do if pred i (arr.(i)) then raise (Found i) done;
+ None
+ with Found i -> Some i
+
+let array_prfx (arr: 'a array) (pred: int -> 'a -> bool): int =
+ try
+ for i=0 to Array.length arr - 1 do if pred i (arr.(i)) then raise (Found i) done;
+ Array.length arr (* all elt are positive *)
+ with Found i -> i
+
+let array_fold_lefti (f: int -> 'a -> 'b -> 'a) (acc:'a) (arr:'b array): 'a =
+ let i = ref 0 in
+ Array.fold_left
+ (fun acc x ->
+ let res = f !i acc x in i := !i + 1; res)
+ acc arr
+
+(* Like list_chop but except that [i] is the size of the suffix of [l]. *)
+let list_chop_end i l =
+ let size_prefix = List.length l -i in
+ if size_prefix < 0 then failwith "list_chop_end"
+ else list_chop size_prefix l
+
+let list_fold_lefti (f: int -> 'a -> 'b -> 'a) (acc:'a) (arr:'b list): 'a =
+ let i = ref 0 in
+ List.fold_left
+ (fun acc x ->
+ let res = f !i acc x in i := !i + 1; res)
+ acc arr
+
+let list_filteri (f: int -> 'a -> bool) (l:'a list):'a list =
+ let i = ref 0 in
+ List.filter (fun x -> let res = f !i x in i := !i + 1; res) l
+
+
+(** Iteration module *)
+module For =
+struct
+ let rec map i j (f: int -> 'a) = if i>j then [] else f i :: (map (i+1) j f)
+ let rec foldup i j (f: 'a -> int -> 'a) acc =
+ if i>j then acc else let newacc = f acc i in foldup (i+1) j f newacc
+ let rec folddown i j (f: 'a -> int -> 'a) acc =
+ if i>j then acc else let newacc = f acc j in folddown i (j-1) f newacc
+ let fold i j = if i<j then foldup i j else folddown i j
+end
+
+
+(** {1 Parameters shifting and linking information} *)
+
+(** This type is used to deal with debruijn linked indices. When a
+ variable is linked to a previous one, we will ignore it and refer
+ to previous one. *)
+type linked_var =
+ | Linked of int
+ | Unlinked
+ | Funres
+
+(** When merging two graphs, parameters may become regular arguments,
+ and thus be shifted. This type describe the result of computing
+ the changes. *)
+type 'a shifted_params =
+ {
+ nprm1:'a;
+ nprm2:'a;
+ prm2_unlinked:'a list; (* ranks of unlinked params in nprms2 *)
+ nuprm1:'a;
+ nuprm2:'a;
+ nargs1:'a;
+ nargs2:'a;
+ }
+
+
+let prlinked x =
+ match x with
+ | Linked i -> Printf.sprintf "Linked %d" i
+ | Unlinked -> Printf.sprintf "Unlinked"
+ | Funres -> Printf.sprintf "Funres"
+
+let linkmonad f lnkvar =
+ match lnkvar with
+ | Linked i -> Linked (f i)
+ | Unlinked -> Unlinked
+ | Funres -> Funres
+
+let linklift lnkvar i = linkmonad (fun x -> x+i) lnkvar
+
+(* This map is used to deal with debruijn linked indices. *)
+module Link = Map.Make (struct type t = int let compare = Pervasives.compare end)
+
+let pr_links l =
+ Printf.printf "links:\n";
+ Link.iter (fun k e -> Printf.printf "%d : %s\n" k (prlinked e)) l;
+ Printf.printf "_____________\n"
+
+type 'a merged_arg =
+ | Prm_stable of 'a
+ | Prm_linked of 'a
+ | Prm_arg of 'a
+ | Arg_stable of 'a
+ | Arg_linked of 'a
+ | Arg_funres
+
+type merge_infos =
+ {
+ 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) *)
+ lnk1: int merged_arg array;
+ (* 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 *)
+ 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) *)
+ nrecprms2: int;
+ (* number of other params of ind2 (which become non rec parm) *)
+ notherprms2:int;
+ (* number of functional result params of ind2 (which become non parm) *)
+ 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 *)
+ }
+
+
+let pr_merginfo x =
+ let i,s=
+ match x with
+ | Prm_linked i -> Some i,"Prm_linked"
+ | Arg_linked i -> Some i,"Arg_linked"
+ | Prm_stable i -> Some i,"Prm_stable"
+ | Prm_arg i -> Some i,"Prm_arg"
+ | Arg_stable i -> Some i,"Arg_stable"
+ | Arg_funres -> None , "Arg_funres" in
+ match i with
+ | Some i -> Printf.sprintf "%s(%d)" s i
+ | None -> Printf.sprintf "%s" s
+
+let isPrm_stable x = match x with Prm_stable _ -> true | _ -> false
+
+let isArg_stable x = match x with Arg_stable _ -> true | _ -> false
+
+let isArg_funres x = match x with Arg_funres -> true | _ -> false
+
+let filter_shift_stable (lnk:int merged_arg array) (l:'a list): 'a list =
+ let prms = list_filteri (fun i _ -> isPrm_stable lnk.(i)) l in
+ let args = list_filteri (fun i _ -> isArg_stable lnk.(i)) l in
+ let fres = list_filteri (fun i _ -> isArg_funres lnk.(i)) l in
+ prms@args@fres
+
+(** Reverse the link map, keeping only linked vars, elements are list
+ of int as several vars may be linked to the same var. *)
+let revlinked lnk =
+ For.fold 0 (Array.length lnk - 1)
+ (fun acc k ->
+ match lnk.(k) with
+ | Unlinked | Funres -> acc
+ | Linked i ->
+ let old = try Link.find i acc with Not_found -> [] in
+ Link.add i (k::old) acc)
+ Link.empty
+
+let array_switch arr i j =
+ let aux = arr.(j) in arr.(j) <- arr.(i); arr.(i) <- aux
+
+let filter_shift_stable_right (lnk:int merged_arg array) (l:'a list): 'a list =
+ let larr = Array.of_list l in
+ let _ =
+ Array.iteri
+ (fun j x ->
+ match x with
+ | Prm_linked i -> array_switch larr i j
+ | Arg_linked i -> array_switch larr i j
+ | Prm_stable i -> ()
+ | Prm_arg i -> ()
+ | Arg_stable i -> ()
+ | Arg_funres -> ()
+ ) lnk in
+ filter_shift_stable lnk (Array.to_list larr)
+
+
+
+
+(** {1 Utilities for merging} *)
+
+let ind1name = id_of_string "__ind1"
+let ind2name = id_of_string "__ind2"
+
+(** Performs verifications on two graphs before merging: they must not
+ be co-inductive, and for the moment they must not be mutual
+ either. *)
+let verify_inds mib1 mib2 =
+ if not mib1.mind_finite then error "First argument is coinductive";
+ if not mib2.mind_finite then error "Second argument is coinductive";
+ if mib1.mind_ntypes <> 1 then error "First argument is mutual";
+ if mib2.mind_ntypes <> 1 then error "Second argument is mutual";
+ ()
+
+
+(** {1 Merging function graphs} *)
+
+(** [shift_linked_params mib1 mib2 lnk] Computes which parameters (rec
+ uniform and ordinary ones) of mutual inductives [mib1] and [mib2]
+ remain uniform when linked by [lnk]. All parameters are
+ considered, ie we take parameters of the first inductive body of
+ [mib1] and [mib2].
+
+ Explanation: The two inductives have parameters, some of the first
+ are recursively uniform, some of the last are functional result of
+ the functional graph.
+
+ (I x1 x2 ... xk ... xk' ... xn)
+ (J y1 y2 ... xl ... yl' ... ym)
+
+ Problem is, if some rec unif params are linked to non rec unif
+ 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 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
+ let is_targetted_by_non_recparam_lnk1 i =
+ try
+ let targets = Link.find i linked_targets in
+ List.exists (fun x -> not (is_param_of_mib2 x)) targets
+ with Not_found -> false in
+ let mlnk1 =
+ Array.mapi
+ (fun i lkv ->
+ let isprm = is_param_of_mib1 i in
+ let prmlost = is_targetted_by_non_recparam_lnk1 i in
+ match isprm , prmlost, lnk1.(i) with
+ | true , true , _ -> Prm_arg i (* recparam becoming ordinary *)
+ | true , false , _-> Prm_stable i (* recparam remains recparam*)
+ | false , false , Funres -> Arg_funres
+ | _ , _ , Funres -> assert false (* fun res cannot be a rec param or lost *)
+ | false , _ , _ -> Arg_stable i) (* Args of lnk1 are not linked *)
+ lnk1 in
+ let mlnk2 =
+ Array.mapi
+ (fun i lkv ->
+ (* Is this correct if some param of ind2 is lost? *)
+ let isprm = is_param_of_mib2 i in
+ match isprm , lnk2.(i) with
+ | true , Linked j when not (is_param_of_mib1 j) ->
+ Prm_arg j (* recparam becoming ordinary *)
+ | true , Linked j -> Prm_linked j (*recparam linked to recparam*)
+ | true , Unlinked -> Prm_stable i (* recparam remains recparam*)
+ | false , Linked j -> Arg_linked j (* Args of lnk2 lost *)
+ | false , Unlinked -> Arg_stable i (* Args of lnk2 remains *)
+ | false , Funres -> Arg_funres
+ | true , Funres -> assert false (* fun res cannot be a rec param *)
+ )
+ lnk2 in
+ let oib1 = mib1.mind_packets.(0) in
+ let oib2 = mib2.mind_packets.(0) in
+ (* count params remaining params *)
+ let n_params1 = array_prfx mlnk1 (fun i x -> not (isPrm_stable x)) in
+ 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 ->
+ 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
+ {
+ ident=id;
+ mib1=mib1;
+ oib1 = oib1;
+ mib2=mib2;
+ oib2 = oib2;
+ lnk1 = mlnk1;
+ lnk2 = mlnk2;
+ nrecprms1 = n_params1;
+ recprms1 = recprms1;
+ otherprms1 = otherprms1;
+ funresprms1 = funresprms1;
+ notherprms1 = Array.length mlnk1 - n_params1;
+ nfunresprms1 = List.length funresprms1;
+ nrecprms2 = n_params2;
+ recprms2 = recprms2;
+ otherprms2 = otherprms2;
+ funresprms2 = funresprms2;
+ notherprms2 = Array.length mlnk2 - n_params2;
+ nfunresprms2 = List.length funresprms2;
+ }
+
+
+
+
+(** {1 Merging functions} *)
+
+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 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 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 =
+ 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
+
+
+
+(* Heuristic when merging two lists of hypothesis: merge every rec
+ calls of nrach 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 =
+ 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
+ rechyps @ merge_rec_hyps shift accrec lt filter_shift_stable
+ | e::lt -> e :: merge_rec_hyps shift accrec lt filter_shift_stable
+
+
+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) =
+ try
+ ignore
+ (List.map
+ (fun x ->
+ match x with
+ | _,(RApp(_,f,_)) when isVarf nme f -> raise (Found 0)
+ | _ -> ())
+ ltyp);
+ false
+ with Found _ -> true
+
+let rec merge_types shift accrec1 (ltyp1:(name * rawconstr) list)
+ concl1 (ltyp2:(name * rawconstr) list) concl2
+ : (name * rawconstr) 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 _ = prstr "\nltyp 2 : " in
+ let _ = List.iter (fun (nm,tp) -> prNamedRConstr (string_of_name nm) 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
+ 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
+ else if isrec2
+ then merge_rec_hyps shift [name_of_string "concl1",concl1] ltyp2
+ filter_shift_stable_right
+ else [] in
+ let _ = prstr"\nrechyps : " in
+ let _ = List.iter
+ (fun (nm,tp) -> prNamedRConstr (string_of_name nm) tp) rechyps in
+ let _ = prstr "MERGE CONCL : " in
+ let _ = prNamedRConstr "concl1" concl1 in
+ let _ = prstr " with " in
+ let _ = prNamedRConstr "concl2" concl2 in
+ let _ = prstr "\n" in
+ let concl =
+ merge_app concl1 concl2 ind1name ind2name shift filter_shift_stable in
+ let _ = prstr "FIN " in
+ let _ = prNamedRConstr "concl" concl in
+ let _ = prstr "\n" in
+ rechyps , concl
+ | (nme,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
+ in
+ res
+
+
+(** [build_link_map_aux allargs1 allargs2 shift] returns the mapping of
+ linked args [allargs2] to target args of [allargs1] as specified
+ in [shift]. [allargs1] and [allargs2] are in reverse order. Also
+ returns the list of unlinked vars of [allargs2]. *)
+let build_link_map_aux (allargs1:identifier array) (allargs2:identifier array)
+ (lnk:int merged_arg array) =
+ array_fold_lefti
+ (fun i acc e ->
+ if i = Array.length lnk - 1 then acc (* functional arg, not in allargs *)
+ else
+ match e with
+ | Prm_linked j | Arg_linked j -> Idmap.add allargs2.(i) allargs1.(j) acc
+ | _ -> acc)
+ Idmap.empty lnk
+
+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
+ let allargs2 =
+ Array.of_list (List.rev (List.map (fun (x,y) -> id_of_name x) allargs2)) in
+ build_link_map_aux allargs1 allargs2 lnk
+
+
+(** [merge_one_constructor lnk shift typcstr1 typcstr2] merges the two
+ constructor rawtypes [typcstr1] and [typcstr2]. [typcstr1] and
+ [typcstr2] contain all parameters (including rec. unif. ones) of
+ their inductive.
+
+ if [typcstr1] and [typcstr2] are of the form:
+
+ forall recparams1, forall ordparams1, H1a -> H2a... (I1 x1 y1 ... z1)
+ forall recparams2, forall ordparams2, H2b -> H2b... (I2 x2 y2 ... z2)
+
+ we build:
+
+ forall recparams1 (recparams2 without linked params),
+ forall ordparams1 (ordparams2 without linked params),
+ H1a' -> H2a' -> ... -> H2a' -> H2b' -> ...
+ -> (newI x1 ... z1 x2 y2 ...z2 without linked params)
+
+ where Hix' have been adapted, ie:
+ - linked vars have been changed,
+ - rec calls to I1 and I2 have been replaced by rec calls to
+ newI. More precisely calls to I1 and I2 have been merge by an
+ experimental heuristic (in particular if n o rec calls for I1
+ or I2 is found, we use the conclusion as a rec call). See
+ [merge_types] above.
+
+ Precond: vars sets of [typcstr1] and [typcstr2] must be disjoint.
+
+ TODO: return nothing if equalities (after linking) are contradictory. *)
+let merge_one_constructor (shift:merge_infos) (typcstr1:rawconstr)
+ (typcstr2:rawconstr) : rawconstr =
+ (* FIXME: les noms des parametres corerspondent en principe au
+ parametres du niveau mib, mais il faudrait s'en assurer *)
+ (* shift.nfunresprmsx last args are functional result *)
+ let nargs1 =
+ 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
+ (* 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 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 revargs1 =
+ list_filteri (fun i _ -> isArg_stable shift.lnk1.(i)) (List.rev allargs1) 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
+ typwithprms
+
+
+(** constructor numbering *)
+let fresh_cstror_suffix , cstror_suffix_init =
+ let cstror_num = ref 0 in
+ (fun () ->
+ let res = string_of_int !cstror_num in
+ cstror_num := !cstror_num + 1;
+ res) ,
+ (fun () -> cstror_num := 0)
+
+(** [merge_constructor_id id1 id2 shift] returns the identifier of the
+ new constructor from the id of the two merged constructor and
+ the merging info. *)
+let merge_constructor_id id1 id2 shift:identifier =
+ let id = string_of_id shift.ident ^ "_" ^ fresh_cstror_suffix () in
+ next_ident_fresh (id_of_string id)
+
+
+
+(** [merge_constructors lnk shift avoid] merges the two list of
+ 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 =
+ 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
+ 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
+ let typ = merge_one_constructor shift rawtyp1 rawtyp2 in
+ let newcstror_id = merge_constructor_id id1 id2 shift in
+ newcstror_id , typ)
+ typcstr2)
+ typcstr1)
+
+(** [merge_inductive_body lnk shift avoid oib1 oib2] merges two
+ 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
+ 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
+
+(** [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
+ [lnk]. [shift] information on parameters of the new inductive.
+ 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) =
+ (* 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)
+
+
+
+let merge_rec_params_and_arity params1 params2 shift (concl:constr) =
+ let params = shift.recprms1 @ shift.recprms2 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
+ 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)
+ (concl,Global.env())
+ (shift.otherprms1@shift.otherprms2@shift.funresprms1@shift.funresprms2) in
+ resparams,arity
+
+
+
+(** [rawterm_list_to_inductive_expr ident rawlist] returns the
+ 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
+ (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
+ 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
+
+(** [merge_inductive ind1 ind2 lnk] merges two graphs, linking
+ variables specified in [lnk]. Graphs are not supposed to be mutual
+ inductives for the moment. *)
+let merge_inductive (ind1: inductive) (ind2: inductive)
+ (lnk1: linked_var array) (lnk2: linked_var array) id =
+ let env = Global.env() in
+ let mib1,_ = Inductive.lookup_mind_specif env ind1 in
+ let mib2,_ = Inductive.lookup_mind_specif env ind2 in
+ 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
+ (* 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?? *)
+ 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
+
+
+
+
+
+(* @article{ bundy93rippling,
+ author = "Alan Bundy and Andrew Stevens and Frank van Harmelen and Andrew Ireland and Alan Smaill",
+ title = "Rippling: A Heuristic for Guiding Inductive Proofs",
+ journal = "Artificial Intelligence",
+ volume = "62",
+ number = "2",
+ pages = "185-253",
+ year = "1993",
+ url = "citeseer.ist.psu.edu/bundy93rippling.html" }
+
+ *)
+(*
+*** Local Variables: ***
+*** compile-command: "make -C ../.. contrib/funind/merge.cmo" ***
+*** indent-tabs-mode: nil ***
+*** End: ***
+*)
diff --git a/contrib/funind/rawterm_to_relation.ml b/contrib/funind/rawterm_to_relation.ml
index dbf2f944..aca84f06 100644
--- a/contrib/funind/rawterm_to_relation.ml
+++ b/contrib/funind/rawterm_to_relation.ml
@@ -789,7 +789,7 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve
avoid
matched_expr
in
- (* We know create the precondition of this branch i.e.
+ (* We now create the precondition of this branch i.e.
1- the list of variable appearing in the different patterns of this branch and
the list of equation stating than el = patl (List.flatten ...)
@@ -1074,8 +1074,8 @@ let rec rebuild_return_type rt =
| _ -> Topconstr.CArrow(dummy_loc,rt,Topconstr.CSort(dummy_loc,RType None))
-let build_inductive
- parametrize funnames (funsargs: (Names.name * rawconstr * bool) list list)
+let do_build_inductive
+ funnames (funsargs: (Names.name * rawconstr * bool) list list)
returned_types
(rtl:rawconstr list) =
let _time1 = System.get_time () in
@@ -1085,7 +1085,7 @@ let build_inductive
let funsargs = Array.of_list funsargs in
let returned_types = Array.of_list returned_types in
(* alpha_renaming of the body to prevent variable capture during manipulation *)
- let rtl_alpha = List.map (function rt -> (alpha_rt [] rt) ) rtl in
+ let rtl_alpha = List.map (function rt -> expand_as (alpha_rt [] rt)) rtl in
let rta = Array.of_list rtl_alpha in
(*i The next call to mk_rel_id is valid since we are constructing the graph
Ensures by: obvious
@@ -1108,19 +1108,7 @@ let build_inductive
(function result (* (args',concl') *) ->
let rt = compose_raw_context result.context result.value in
let nb_args = List.length funsargs.(i) in
-(* 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; *)
-(* Impargs.make_implicit_args false; *)
-(* Impargs.make_strict_implicit_args false; *)
-(* Impargs.make_contextual_implicit_args false; *)
-(* Pp.msgnl (str "raw constr " ++ pr_rawconstr rt); *)
-(* 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; *)
+ (* with_full_print (fun rt -> Pp.msgnl (str "raw constr " ++ pr_rawconstr rt)) rt; *)
fst (
rebuild_cons nb_args relnames.(i)
[]
@@ -1145,12 +1133,7 @@ let build_inductive
in
let rel_constructors = Array.mapi rel_constructors resa in
(* Computing the set of parameters if asked *)
- let rels_params =
- if parametrize
- then
- compute_params_name relnames_as_set funsargs rel_constructors
- else []
- in
+ let rels_params = compute_params_name relnames_as_set funsargs rel_constructors in
let nrel_params = List.length rels_params in
let rel_constructors = (* Taking into account the parameters in constructors *)
Array.map (List.map
@@ -1182,8 +1165,6 @@ let build_inductive
Then save the graphs and reset Printing options to their primitive values
*)
let rel_arities = Array.mapi rel_arity funsargs in
- let old_rawprint = !Options.raw_print in
- Options.raw_print := true;
let rel_params =
List.map
(fun (n,t,is_defined) ->
@@ -1199,16 +1180,19 @@ let build_inductive
let ext_rels_constructors =
Array.map (List.map
(fun (id,t) ->
- false,((dummy_loc,id),Constrextern.extern_rawtype Idset.empty ((* zeta_normalize *) t))
+ false,((dummy_loc,id),
+ Options.with_option
+ Options.raw_print
+ (Constrextern.extern_rawtype Idset.empty) ((* zeta_normalize *) t)
+ )
))
(rel_constructors)
in
let rel_ind i ext_rel_constructors =
- (dummy_loc,relnames.(i)),
- None,
+ ((dummy_loc,relnames.(i)),
rel_params,
rel_arities.(i),
- ext_rel_constructors
+ ext_rel_constructors),None
in
let ext_rel_constructors = (Array.mapi rel_ind ext_rels_constructors) in
let rel_inds = Array.to_list ext_rel_constructors in
@@ -1232,58 +1216,36 @@ let build_inductive
(* rel_inds *)
(* ) *)
(* in *)
- 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
- Impargs.make_implicit_args false;
- Impargs.make_strict_implicit_args false;
- Impargs.make_contextual_implicit_args false;
let _time2 = System.get_time () in
-(* Pp.msgnl (str "Bulding Inductive : " ++ str (string_of_float (System.time_difference time1 time2))); *)
try
- Options.silently (Command.build_mutual rel_inds) true;
- let _time3 = System.get_time () in
-(* Pp.msgnl (str "Bulding Done: "++ str (string_of_float (System.time_difference time2 time3))); *)
-(* let msg = *)
-(* str "while trying to define"++ spc () ++ *)
-(* Ppvernac.pr_vernac (Vernacexpr.VernacInductive(true,rel_inds)) ++ fnl () *)
-(* in *)
-(* Pp.msgnl msg; *)
- 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;
- with
- | UserError(s,msg) ->
+ with_full_print (Options.silently (Command.build_mutual rel_inds)) true
+ with
+ | UserError(s,msg) as e ->
let _time3 = System.get_time () in
(* Pp.msgnl (str "error : "++ str (string_of_float (System.time_difference time2 time3))); *)
- 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;
let msg =
str "while trying to define"++ spc () ++
Ppvernac.pr_vernac (Vernacexpr.VernacInductive(true,rel_inds)) ++ fnl () ++
msg
in
observe (msg);
- raise
- (UserError(s, msg))
+ raise e
| e ->
let _time3 = System.get_time () in
(* Pp.msgnl (str "error : "++ str (string_of_float (System.time_difference time2 time3))); *)
- 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;
let msg =
str "while trying to define"++ spc () ++
Ppvernac.pr_vernac (Vernacexpr.VernacInductive(true,rel_inds)) ++ fnl () ++
Cerrors.explain_exn e
in
observe msg;
- raise
- (UserError("",msg))
+ raise e
+let build_inductive funnames funsargs returned_types rtl =
+ try
+ do_build_inductive funnames funsargs returned_types rtl
+ with e -> raise (Building_graph e)
+
+
diff --git a/contrib/funind/rawterm_to_relation.mli b/contrib/funind/rawterm_to_relation.mli
index 9cd04123..0075fb0a 100644
--- a/contrib/funind/rawterm_to_relation.mli
+++ b/contrib/funind/rawterm_to_relation.mli
@@ -1,5 +1,6 @@
+
(*
[build_inductive parametrize funnames funargs returned_types bodies]
constructs and saves the graphs of the functions [funnames] taking [funargs] as arguments
@@ -7,7 +8,6 @@
*)
val build_inductive :
- bool -> (* if true try to detect parameter. Always use it as true except for debug *)
Names.identifier list -> (* The list of function name *)
(Names.name*Rawterm.rawconstr*bool) list list -> (* The list of function args *)
Topconstr.constr_expr list -> (* The list of function returned type *)
diff --git a/contrib/funind/rawtermops.ml b/contrib/funind/rawtermops.ml
index 14805cf4..ed46ec72 100644
--- a/contrib/funind/rawtermops.ml
+++ b/contrib/funind/rawtermops.ml
@@ -35,6 +35,18 @@ let raw_decompose_prod =
let raw_compose_prod =
List.fold_left (fun b (n,t) -> mkRProd(n,t,b))
+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) ->
+ raw_decompose_prod (i-1) ((n,t)::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); *)
@@ -321,14 +333,6 @@ let rec alpha_rt excluded rt =
List.map (alpha_rt excluded) args
)
in
- if Indfun_common.do_observe () && false
- then
- Pp.msgnl (str "debug: alpha_rt(" ++ str "[" ++
- prlist_with_sep (fun _ -> str";") Ppconstr.pr_id excluded ++
- str "]" ++ spc () ++ str "," ++ spc () ++
- Printer.pr_rawconstr rt ++ spc () ++ str ")" ++ spc () ++ str "=" ++
- spc () ++ Printer.pr_rawconstr new_rt
- );
new_rt
and alpha_br excluded (loc,ids,patl,res) =
@@ -339,12 +343,6 @@ and alpha_br excluded (loc,ids,patl,res) =
let new_res = alpha_rt new_excluded renamed_res in
(loc,new_ids,new_patl,new_res)
-
-
-
-
-
-
(*
[is_free_in id rt] checks if [id] is a free variable in [rt]
*)
@@ -541,6 +539,33 @@ let ids_of_pat =
in
ids_of_pat Idset.empty
+let id_of_name = function
+ | Names.Anonymous -> id_of_string "x"
+ | Names.Name x -> x
+
+(* TODO: finish Rec caes *)
+let ids_of_rawterm c =
+ let rec ids_of_rawterm acc c =
+ let idof = id_of_name in
+ match c with
+ | 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
+ | RLetIn (loc,na,b,c) -> idof na :: ids_of_rawterm [] b @ ids_of_rawterm [] c @ acc
+ | RCast (loc,c,k,t) -> ids_of_rawterm [] c @ ids_of_rawterm [] t @ 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) ->
+ 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 _) as x -> []
+ in
+ (* build the set *)
+ List.fold_left (fun acc x -> Idset.add x acc) Idset.empty (ids_of_rawterm [] c)
+
@@ -601,3 +626,46 @@ let zeta_normalize =
(loc,idl,patl,zeta_normalize_term res)
in
zeta_normalize_term
+
+
+
+
+let expand_as =
+
+ let rec add_as map pat =
+ match pat with
+ | PatVar _ -> map
+ | PatCstr(_,_,patl,Name id) ->
+ Idmap.add id (pattern_to_term pat) (List.fold_left add_as map patl)
+ | PatCstr(_,_,patl,_) -> List.fold_left add_as map patl
+ in
+ let rec expand_as map rt =
+ match rt with
+ | RRef _ | REvar _ | RPatVar _ | RSort _ | RHole _ -> rt
+ | RVar(_,id) ->
+ begin
+ try
+ Idmap.find id map
+ 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)
+ | 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),
+ 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),
+ expand_as map br1, expand_as map br2)
+ | RRec _ -> error "Not handled RRec"
+ | RDynamic _ -> error "Not handled RDynamic"
+ | RCast(loc,b,kind,t) -> RCast(loc,expand_as map b,kind,expand_as map t)
+ | RCases(loc,po,el,brl) ->
+ RCases(loc, 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)
+ in
+ expand_as Idmap.empty
diff --git a/contrib/funind/rawtermops.mli b/contrib/funind/rawtermops.mli
index aa355485..9647640c 100644
--- a/contrib/funind/rawtermops.mli
+++ b/contrib/funind/rawtermops.mli
@@ -31,6 +31,7 @@ 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_n : int -> rawconstr -> (Names.name*rawconstr) list * rawconstr
val raw_compose_prod : rawconstr -> (Names.name*rawconstr) list -> rawconstr
val raw_decompose_app : rawconstr -> rawconstr*(rawconstr list)
@@ -107,8 +108,13 @@ val eq_cases_pattern : cases_pattern -> cases_pattern -> bool
*)
val ids_of_pat : cases_pattern -> Names.Idset.t
+(* TODO: finish this function (Fix not treated) *)
+val ids_of_rawterm: rawconstr -> Names.Idset.t
(*
removing let_in construction in a rawterm
*)
val zeta_normalize : Rawterm.rawconstr -> Rawterm.rawconstr
+
+
+val expand_as : rawconstr -> rawconstr
diff --git a/contrib/funind/tacinvutils.ml b/contrib/funind/tacinvutils.ml
index 2877c19d..ce775e0b 100644
--- a/contrib/funind/tacinvutils.ml
+++ b/contrib/funind/tacinvutils.ml
@@ -72,10 +72,11 @@ let rec mkevarmap_from_listex lex =
let _ = prstr ("evar n. " ^ string_of_int ex ^ " ") in
let _ = prstr "OF TYPE: " in
let _ = prconstr typ in*)
- let info ={
+ let info = {
evar_concl = typ;
evar_hyps = empty_named_context_val;
- evar_body = Evar_empty} in
+ evar_body = Evar_empty;
+ evar_extra = None} in
Evd.add (mkevarmap_from_listex lex') ex info
let mkEq typ c1 c2 =
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-08 22:47:26 +0000