aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib
diff options
context:
space:
mode:
Diffstat (limited to 'contrib')
-rw-r--r--contrib/funind/functional_principles_proofs.ml151
-rw-r--r--contrib/funind/functional_principles_types.ml10
-rw-r--r--contrib/funind/indfun.ml16
-rw-r--r--contrib/funind/indfun_common.ml24
-rw-r--r--contrib/funind/indfun_common.mli4
-rw-r--r--contrib/funind/rawterm_to_relation.ml239
6 files changed, 337 insertions, 107 deletions
diff --git a/contrib/funind/functional_principles_proofs.ml b/contrib/funind/functional_principles_proofs.ml
index 6241eb1de..903136ca2 100644
--- a/contrib/funind/functional_principles_proofs.ml
+++ b/contrib/funind/functional_principles_proofs.ml
@@ -59,9 +59,9 @@ let list_chop ?(msg="") n l =
failwith (msg ^ msg')
-let make_refl_eq type_of_t t =
- let refl_equal_term = Lazy.force refl_equal in
- mkApp(refl_equal_term,[|type_of_t;t|])
+let make_refl_eq constructor type_of_t t =
+(* let refl_equal_term = Lazy.force refl_equal in *)
+ mkApp(constructor,[|type_of_t;t|])
type pte_info =
@@ -109,11 +109,19 @@ let intro_erasing id = tclTHEN (thin [id]) (introduction id)
let rec_hyp_id = id_of_string "rec_hyp"
let is_trivial_eq t =
- match kind_of_term t with
- | App(f,[|_;t1;t2|]) when eq_constr f (Lazy.force eq) ->
- eq_constr t1 t2
- | _ -> false
-
+ let res = try
+ begin
+ match kind_of_term t with
+ | App(f,[|_;t1;t2|]) when eq_constr f (Lazy.force eq) ->
+ eq_constr t1 t2
+ | App(f,[|t1;a1;t2;a2|]) when eq_constr f (jmeq ()) ->
+ eq_constr t1 t2 && eq_constr a1 a2
+ | _ -> false
+ end
+ with _ -> false
+ in
+(* observe (str "is_trivial_eq " ++ Printer.pr_lconstr t ++ (if res then str " true" else str " false")); *)
+ res
let rec incompatible_constructor_terms t1 t2 =
let c1,arg1 = decompose_app t1
@@ -127,10 +135,19 @@ let rec incompatible_constructor_terms t1 t2 =
)
let is_incompatible_eq t =
- match kind_of_term t with
- | App(f,[|_;t1;t2|]) when eq_constr f (Lazy.force eq) ->
- incompatible_constructor_terms t1 t2
- | _ -> false
+ let res =
+ try
+ match kind_of_term t with
+ | App(f,[|_;t1;t2|]) when eq_constr f (Lazy.force eq) ->
+ incompatible_constructor_terms t1 t2
+ | App(f,[|u1;t1;u2;t2|]) when eq_constr f (jmeq ()) ->
+ (eq_constr u1 u2 &&
+ incompatible_constructor_terms t1 t2)
+ | _ -> false
+ with _ -> false
+ in
+ if res then observe (str "is_incompatible_eq " ++ Printer.pr_lconstr t);
+ res
let change_hyp_with_using msg hyp_id t tac : tactic =
fun g ->
@@ -146,7 +163,7 @@ let change_hyp_with_using msg hyp_id t tac : tactic =
exception TOREMOVE
-let prove_trivial_eq h_id context (type_of_term,term) =
+let prove_trivial_eq h_id context (constructor,type_of_term,term) =
let nb_intros = List.length context in
tclTHENLIST
[
@@ -156,7 +173,7 @@ let prove_trivial_eq h_id context (type_of_term,term) =
fst (list_chop ~msg:"prove_trivial_eq : " nb_intros (pf_ids_of_hyps g))
in
let context_hyps' =
- (mkApp(Lazy.force refl_equal,[|type_of_term;term|]))::
+ (mkApp(constructor,[|type_of_term;term|]))::
(List.map mkVar context_hyps)
in
let to_refine = applist(mkVar h_id,List.rev context_hyps') in
@@ -165,10 +182,21 @@ let prove_trivial_eq h_id context (type_of_term,term) =
]
-let isAppConstruct t =
- if isApp t
- then isConstruct (fst (destApp t))
- else false
+
+let find_rectype env c =
+ let (t, l) = decompose_app (Reduction.whd_betadeltaiota env c) in
+ match kind_of_term t with
+ | Ind ind -> (t, l)
+ | Construct _ -> (t,l)
+ | _ -> raise Not_found
+
+
+let isAppConstruct ?(env=Global.env ()) t =
+ try
+ let t',l = find_rectype (Global.env ()) t in
+ observe (str "isAppConstruct : " ++ Printer.pr_lconstr t ++ str " -> " ++ Printer.pr_lconstr (applist (t',l)));
+ true
+ with Not_found -> false
let nf_betaiotazeta = (* Reductionops.local_strong Reductionops.whd_betaiotazeta *)
let clos_norm_flags flgs env sigma t =
@@ -176,10 +204,11 @@ let nf_betaiotazeta = (* Reductionops.local_strong Reductionops.whd_betaiotazeta
clos_norm_flags Closure.betaiotazeta Environ.empty_env Evd.empty
+
let change_eq env sigma hyp_id (context:Sign.rel_context) x t end_of_type =
- let nochange msg =
+ let nochange ?t' msg =
begin
-(* observe (str ("Not treating ( "^msg^" )") ++ pr_lconstr t ); *)
+ observe (str ("Not treating ( "^msg^" )") ++ pr_lconstr t ++ str " " ++ match t' with None -> str "" | Some t -> Printer.pr_lconstr t );
failwith "NoChange";
end
in
@@ -188,12 +217,23 @@ let change_eq env sigma hyp_id (context:Sign.rel_context) x t 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";
let f_eq,args = destApp t in
- if not (eq_constr f_eq (Lazy.force eq)) then nochange "not an equality";
- let t1 = args.(1)
- and t2 = args.(2)
- and t1_typ = args.(0)
+ let constructor,t1,t2,t1_typ =
+ try
+ if (eq_constr f_eq (Lazy.force eq))
+ then
+ let t1 = (args.(1),args.(0))
+ and t2 = (args.(2),args.(0))
+ and t1_typ = args.(0)
+ in
+ (Lazy.force refl_equal,t1,t2,t1_typ)
+ else
+ if (eq_constr f_eq (jmeq ()))
+ then
+ (jmeq_refl (),(args.(1),args.(0)),(args.(3),args.(2)),args.(0))
+ else nochange "not an equality"
+ with _ -> nochange "not an equality"
in
- if not (closed0 t1) then nochange "not a closed lhs";
+ if not ((closed0 (fst t1)) && (closed0 (snd 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
@@ -211,16 +251,17 @@ let change_eq env sigma hyp_id (context:Sign.rel_context) x t end_of_type =
else if isAppConstruct t1 && isAppConstruct t2
then
begin
- let c1,args1 = destApp t1
- and c2,args2 = destApp t2
+ let c1,args1 = find_rectype env t1
+ and c2,args2 = find_rectype env t2
in
- if not (eq_constr c1 c2) then anomaly "deconstructing equation";
- array_fold_left2 compute_substitution sub args1 args2
+ if not (eq_constr c1 c2) then nochange "cannot solve (diff)";
+ List.fold_left2 compute_substitution sub args1 args2
end
else
- if (eq_constr t1 t2) then sub else nochange "cannot solve"
+ if (eq_constr t1 t2) then sub else nochange ~t':(make_refl_eq constructor (Reduction.whd_betadeltaiota env t1) t2) "cannot solve (diff)"
in
- let sub = compute_substitution Intmap.empty t1 t2 in
+ let sub = compute_substitution Intmap.empty (snd t1) (snd t2) in
+ let sub = compute_substitution sub (fst t1) (fst t2) in
let end_of_type_with_pop = pop end_of_type in (*the equation will be removed *)
let new_end_of_type =
(* Ugly hack to prevent Map.fold order change between ocaml-3.08.3 and ocaml-3.08.4
@@ -234,7 +275,7 @@ let change_eq env sigma hyp_id (context:Sign.rel_context) x t end_of_type =
in
let old_context_length = List.length context + 1 in
let witness_fun =
- mkLetIn(Anonymous,make_refl_eq t1_typ t1,t,
+ mkLetIn(Anonymous,make_refl_eq constructor t1_typ (fst t1),t,
mkApp(mkVar hyp_id,Array.init old_context_length (fun i -> mkRel (old_context_length - i)))
)
in
@@ -450,14 +491,20 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma =
let real_type_of_hyp =
it_mkProd_or_LetIn ~init:popped_t' context
in
- let _,args = destApp t_x in
+ let hd,args = destApp t_x in
+ let get_args hd args =
+ if eq_constr hd (Lazy.force eq)
+ then (Lazy.force refl_equal,args.(0),args.(1))
+ else (jmeq_refl (),args.(0),args.(1))
+ in
tclTHENLIST
[
change_hyp_with_using
"prove_trivial_eq"
hyp_id
real_type_of_hyp
- ((* observe_tac "prove_trivial_eq" *) (prove_trivial_eq hyp_id context (args.(0),args.(1))));
+ ((* observe_tac "prove_trivial_eq" *)
+ (prove_trivial_eq hyp_id context (get_args hd args)));
scan_type context popped_t'
]
else
@@ -631,28 +678,32 @@ let build_proof
let g_nb_prod = nb_prod (pf_concl g) in
let type_of_term = pf_type_of g t in
let term_eq =
- make_refl_eq type_of_term t
+ make_refl_eq (Lazy.force refl_equal) type_of_term t
in
tclTHENSEQ
[
h_generalize (term_eq::(List.map mkVar dyn_infos.rec_hyps));
thin dyn_infos.rec_hyps;
pattern_option [(false,[1]),t] None;
- h_simplest_case t;
- (fun g' ->
- let g'_nb_prod = nb_prod (pf_concl g') in
- let nb_instanciate_partial = g'_nb_prod - g_nb_prod in
- observe_tac "treat_new_case"
- (treat_new_case
- ptes_infos
- nb_instanciate_partial
- (build_proof do_finalize)
- t
- dyn_infos)
- g'
- )
+ (fun g -> observe_tac "toto" (
+ tclTHENSEQ [h_simplest_case t;
+ (fun g' ->
+ let g'_nb_prod = nb_prod (pf_concl g') in
+ let nb_instanciate_partial = g'_nb_prod - g_nb_prod in
+ observe_tac "treat_new_case"
+ (treat_new_case
+ ptes_infos
+ nb_instanciate_partial
+ (build_proof do_finalize)
+ t
+ dyn_infos)
+ g'
+ )
- ] g
+ ]) g
+ )
+ ]
+ g
in
build_proof do_finalize_t {dyn_infos with info = t} g
| Lambda(n,t,b) ->
@@ -1206,7 +1257,7 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams :
nb_rec_hyps = List.length branches
}
in
- (* observe_tac "cleaning" *) (clean_goal_with_heq
+ observe_tac "cleaning" (clean_goal_with_heq
(Idmap.map prove_rec_hyp ptes_to_fix)
do_prove
dyn_infos)
diff --git a/contrib/funind/functional_principles_types.ml b/contrib/funind/functional_principles_types.ml
index b03bdf31a..5155e614d 100644
--- a/contrib/funind/functional_principles_types.ml
+++ b/contrib/funind/functional_principles_types.ml
@@ -328,7 +328,7 @@ let build_functional_principle interactive_proof old_princ_type sorts funs i pro
in
(* let time2 = System.get_time () in *)
(* Pp.msgnl (str "computing principle type := " ++ System.fmt_time_difference time1 time2); *)
- (* observe (str "new_principle_type : " ++ pr_lconstr new_principle_type); *)
+ observe (str "new_principle_type : " ++ pr_lconstr new_principle_type);
let new_princ_name =
next_global_ident_away true (id_of_string "___________princ_________") []
in
@@ -356,6 +356,7 @@ let generate_functional_principle
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 =
@@ -718,9 +719,10 @@ let build_case_scheme fa =
in
let princ_name = (fun (x,_,_) -> x) fa in
let _ =
-(* observe (str "Generating " ++ Ppconstr.pr_id princ_name ++str " with " ++ *)
-(* pr_lconstr scheme_type ++ str " and " ++ (fun a -> prlist_with_sep spc (fun c -> pr_lconstr (mkConst c)) (Array.to_list a)) this_block_funs *)
-(* ); *)
+ (* Pp.msgnl (str "Generating " ++ Ppconstr.pr_id princ_name ++str " with " ++
+ pr_lconstr scheme_type ++ str " and " ++ (fun a -> prlist_with_sep spc (fun c -> pr_lconstr (mkConst c)) (Array.to_list a)) this_block_funs
+ );
+ *)
generate_functional_principle
false
scheme_type
diff --git a/contrib/funind/indfun.ml b/contrib/funind/indfun.ml
index b6b2cbd11..d7a7c311a 100644
--- a/contrib/funind/indfun.ml
+++ b/contrib/funind/indfun.ml
@@ -272,26 +272,36 @@ let derive_inversion fix_names =
with _ -> ()
let warning_error names e =
+ let e_explain e =
+ match e with
+ | ToShow e -> spc () ++ Cerrors.explain_exn e
+ | _ -> if do_observe () then (spc () ++ Cerrors.explain_exn e) else mt ()
+ in
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 ())
+ e_explain e)
| 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 ())
+ e_explain e)
| _ -> anomaly ""
let error_error names e =
+ let e_explain e =
+ match e with
+ | ToShow e -> spc () ++ Cerrors.explain_exn e
+ | _ -> if do_observe () then (spc () ++ Cerrors.explain_exn e) else mt ()
+ in
match e with
| Building_graph e ->
errorlabstrm ""
(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 ())
+ e_explain e)
| _ -> anomaly ""
let generate_principle on_error
diff --git a/contrib/funind/indfun_common.ml b/contrib/funind/indfun_common.ml
index 4892128a0..69cc0607b 100644
--- a/contrib/funind/indfun_common.ml
+++ b/contrib/funind/indfun_common.ml
@@ -524,3 +524,27 @@ let _ = declare_bool_option strict_tcc_sig
exception Building_graph of exn
exception Defining_principle of exn
+exception ToShow of exn
+
+let init_constant dir s =
+ try
+ Coqlib.gen_constant "Function" dir s
+ with e -> raise (ToShow e)
+
+let jmeq () =
+ try
+ (Coqlib.check_required_library ["Coq";"Logic";"JMeq"];
+ init_constant ["Logic";"JMeq"] "JMeq")
+ with e -> raise (ToShow e)
+
+let jmeq_rec () =
+ try
+ Coqlib.check_required_library ["Coq";"Logic";"JMeq"];
+ init_constant ["Logic";"JMeq"] "JMeq_rec"
+ with e -> raise (ToShow e)
+
+let jmeq_refl () =
+ try
+ Coqlib.check_required_library ["Coq";"Logic";"JMeq"];
+ init_constant ["Logic";"JMeq"] "JMeq_refl"
+ with e -> raise (ToShow e)
diff --git a/contrib/funind/indfun_common.mli b/contrib/funind/indfun_common.mli
index 2d741f0b3..e9aa692b6 100644
--- a/contrib/funind/indfun_common.mli
+++ b/contrib/funind/indfun_common.mli
@@ -45,7 +45,8 @@ val def_of_const : Term.constr -> Term.constr
val eq : Term.constr Lazy.t
val refl_equal : Term.constr Lazy.t
val const_of_id: identifier -> constant
-
+val jmeq : unit -> Term.constr
+val jmeq_refl : unit -> Term.constr
(* [save_named] is a copy of [Command.save_named] but uses
[nf_betaiotazeta] instead of [nf_betaiotaevar_preserving_vm_cast]
@@ -114,5 +115,6 @@ val do_observe : unit -> bool
(* To localize pb *)
exception Building_graph of exn
exception Defining_principle of exn
+exception ToShow of exn
val is_strict_tcc : unit -> bool
diff --git a/contrib/funind/rawterm_to_relation.ml b/contrib/funind/rawterm_to_relation.ml
index 75f6207fc..d54aca4e6 100644
--- a/contrib/funind/rawterm_to_relation.ml
+++ b/contrib/funind/rawterm_to_relation.ml
@@ -25,7 +25,6 @@ type binder_type =
type raw_context = (binder_type*rawconstr) list
-
(*
compose_raw_context [(bt_1,n_1,t_1);......] rt returns
b_1(n_1,t_1,.....,bn(n_k,t_k,rt)) where the b_i's are the
@@ -712,20 +711,25 @@ and build_entry_lc_from_case env funname make_discr
el
(mk_result [] [] avoid)
in
- (****** The next works only if the match is not dependent ****)
let types =
List.map (fun (case_arg,_) ->
let case_arg_as_constr = Pretyping.Default.understand Evd.empty env case_arg in
Typing.type_of env Evd.empty case_arg_as_constr
) el
in
+ (****** The next works only if the match is not dependent ****)
let results =
List.map
- (build_entry_lc_from_case_term
+ (fun ca ->
+ let res = build_entry_lc_from_case_term
env types
- funname (make_discr (* (List.map fst el) *))
+ funname (make_discr)
[] brl
- case_resl.to_avoid)
+ case_resl.to_avoid
+ ca
+ in
+ res
+ )
case_resl.result
in
{
@@ -754,14 +758,17 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve
let pat_ids = get_pattern_id renamed_pat in
let env_with_pat_ids = add_pat_variables pat typ new_env in
List.fold_right
- (fun id acc ->
- let typ_of_id = Typing.type_of env_with_pat_ids Evd.empty (mkVar id) in
- let raw_typ_of_id =
- Detyping.detype false [] (Termops.names_of_rel_context env_with_pat_ids) typ_of_id
- in
- mkRProd (Name id,raw_typ_of_id,acc))
- pat_ids
- (raw_make_neq pat'_as_term (pattern_to_term renamed_pat))
+ (fun id acc ->
+ let typ_of_id =
+ Typing.type_of env_with_pat_ids Evd.empty (mkVar id)
+ in
+ let raw_typ_of_id =
+ Detyping.detype false []
+ (Termops.names_of_rel_context env_with_pat_ids) typ_of_id
+ in
+ mkRProd (Name id,raw_typ_of_id,acc))
+ pat_ids
+ (raw_make_neq pat'_as_term (pattern_to_term renamed_pat))
)
patl
types
@@ -790,7 +797,6 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve
matched_expr
in
(* 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 ...)
2- If there exists a previous branch which pattern unify with the one of this branch
@@ -815,7 +821,6 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve
raw_typ_of_id
)::acc
else acc
-
)
idl
[(Prod Anonymous,raw_make_eq ~typ pat_as_term e)]
@@ -863,7 +868,9 @@ let is_res id =
rebuild the raw constructors expression.
eliminates some meaningless equalities, applies some rewrites......
*)
-let rec rebuild_cons nb_args relname args crossed_types depth rt =
+let rec rebuild_cons env nb_args relname args crossed_types depth rt =
+ observe (str "rebuilding : " ++ pr_rawconstr rt);
+
match rt with
| RProd(_,n,k,t,b) ->
let not_free_in_t id = not (is_free_in id t) in
@@ -874,50 +881,147 @@ let rec rebuild_cons nb_args relname args crossed_types depth rt =
begin
match args' with
| (RVar(_,this_relname))::args' ->
- let new_b,id_to_exclude =
- rebuild_cons
- nb_args relname
- args new_crossed_types
- (depth + 1) b
- in
- (*i The next call to mk_rel_id is valid since we are constructing the graph
+ (*i The next call to mk_rel_id is
+ valid since we are constructing the graph
Ensures by: obvious
i*)
let new_t =
mkRApp(mkRVar(mk_rel_id this_relname),args'@[res_rt])
- in mkRProd(n,new_t,new_b),
+ in
+ let t' = Pretyping.Default.understand Evd.empty env new_t in
+ let new_env = Environ.push_rel (n,None,t') env in
+ let new_b,id_to_exclude =
+ rebuild_cons new_env
+ nb_args relname
+ args new_crossed_types
+ (depth + 1) b
+ in
+ mkRProd(n,new_t,new_b),
Idset.filter not_free_in_t id_to_exclude
| _ -> (* the first args is the name of the function! *)
assert false
end
- | RApp(_,RRef(_,eq_as_ref),[_;RVar(_,id);rt])
+ | RApp(loc1,RRef(loc2,eq_as_ref),[ty;RVar(loc3,id);rt])
when eq_as_ref = Lazy.force Coqlib.coq_eq_ref && n = Anonymous
->
- let is_in_b = is_free_in id b in
- let _keep_eq =
- not (List.exists (is_free_in id) args) || is_in_b ||
- List.exists (is_free_in id) crossed_types
- in
- let new_args = List.map (replace_var_by_term id rt) args in
- let subst_b =
- if is_in_b then b else replace_var_by_term id rt b
- in
- let new_b,id_to_exclude =
- rebuild_cons
- nb_args relname
- new_args new_crossed_types
- (depth + 1) subst_b
- in
- mkRProd(n,t,new_b),id_to_exclude
+ begin
+ try
+ observe (str "computing new type for eq : " ++ pr_rawconstr rt);
+ let t' = Pretyping.Default.understand Evd.empty env t in
+ let is_in_b = is_free_in id b in
+ let _keep_eq =
+ not (List.exists (is_free_in id) args) || is_in_b ||
+ List.exists (is_free_in id) crossed_types
+ in
+ let new_args = List.map (replace_var_by_term id rt) args in
+ let subst_b =
+ if is_in_b then b else replace_var_by_term id rt b
+ in
+ let new_env = Environ.push_rel (n,None,t') env in
+ let new_b,id_to_exclude =
+ rebuild_cons
+ new_env
+ nb_args relname
+ new_args new_crossed_types
+ (depth + 1) subst_b
+ in
+ mkRProd(n,t,new_b),id_to_exclude
+ with _ ->
+ let jmeq = Libnames.IndRef (destInd (jmeq ())) in
+ let ty' = Pretyping.Default.understand Evd.empty env ty in
+ let ind,args' = Inductive.find_inductive env ty' in
+ let mib,_ = Global.lookup_inductive ind in
+ let nparam = mib.Declarations.mind_nparams in
+ let params,arg' =
+ ((Util.list_chop nparam args'))
+ in
+ let rt_typ =
+ RApp(Util.dummy_loc,
+ RRef (Util.dummy_loc,Libnames.IndRef ind),
+ (List.map
+ (fun p -> Detyping.detype false []
+ (Termops.names_of_rel_context env)
+ p) params)@(Array.to_list
+ (Array.make
+ (List.length args' - nparam)
+ (mkRHole ()))))
+ in
+ let eq' =
+ RApp(loc1,RRef(loc2,jmeq),[ty;RVar(loc3,id);rt_typ;rt])
+ in
+ observe (str "computing new type for jmeq : " ++ pr_rawconstr eq');
+ let eq'_as_constr = Pretyping.Default.understand Evd.empty env eq' in
+ observe (str " computing new type for jmeq : done") ;
+ let new_args =
+ match kind_of_term eq'_as_constr with
+ | App(_,[|_;_;ty;_|]) ->
+ let ty = Array.to_list (snd (destApp ty)) in
+ let ty' = snd (Util.list_chop nparam ty) in
+ List.fold_left2
+ (fun acc var_as_constr arg ->
+ if isRel var_as_constr
+ then
+ let (na,_,_) =
+ Environ.lookup_rel (destRel var_as_constr) env
+ in
+ match na with
+ | Anonymous -> acc
+ | Name id' ->
+ (id',Detyping.detype false []
+ (Termops.names_of_rel_context env)
+ arg)::acc
+ else if isVar var_as_constr
+ then (destVar var_as_constr,Detyping.detype false []
+ (Termops.names_of_rel_context env)
+ arg)::acc
+ else acc
+ )
+ []
+ arg'
+ ty'
+ | _ -> assert false
+ in
+ let is_in_b = is_free_in id b in
+ let _keep_eq =
+ not (List.exists (is_free_in id) args) || is_in_b ||
+ List.exists (is_free_in id) crossed_types
+ in
+ let new_args =
+ List.fold_left
+ (fun args (id,rt) ->
+ List.map (replace_var_by_term id rt) args
+ )
+ args
+ ((id,rt)::new_args)
+ in
+ let subst_b =
+ if is_in_b then b else replace_var_by_term id rt b
+ in
+ let new_env =
+ let t' = Pretyping.Default.understand Evd.empty env eq' in
+ Environ.push_rel (n,None,t') env
+ in
+ let new_b,id_to_exclude =
+ rebuild_cons
+ new_env
+ nb_args relname
+ new_args new_crossed_types
+ (depth + 1) subst_b
+ in
+ mkRProd(n,eq',new_b),id_to_exclude
+ end
(* J.F:. keep this comment it explain how to remove some meaningless equalities
if keep_eq then
mkRProd(n,t,new_b),id_to_exclude
else new_b, Idset.add id id_to_exclude
*)
| _ ->
+ observe (str "computing new type for prod : " ++ pr_rawconstr rt);
+ let t' = Pretyping.Default.understand Evd.empty env t in
+ let new_env = Environ.push_rel (n,None,t') env in
let new_b,id_to_exclude =
- rebuild_cons
+ rebuild_cons new_env
nb_args relname
args new_crossed_types
(depth + 1) b
@@ -932,10 +1036,13 @@ let rec rebuild_cons nb_args relname args crossed_types depth rt =
begin
let not_free_in_t id = not (is_free_in id t) in
let new_crossed_types = t :: crossed_types in
+ observe (str "computing new type for lambda : " ++ pr_rawconstr rt);
+ let t' = Pretyping.Default.understand Evd.empty env t in
match n with
| Name id ->
+ let new_env = Environ.push_rel (n,None,t') env in
let new_b,id_to_exclude =
- rebuild_cons
+ rebuild_cons new_env
nb_args relname
(args@[mkRVar id])new_crossed_types
(depth + 1 ) b
@@ -952,8 +1059,11 @@ let rec rebuild_cons nb_args relname args crossed_types depth rt =
| RLetIn(_,n,t,b) ->
begin
let not_free_in_t id = not (is_free_in id t) in
+ let t' = Pretyping.Default.understand Evd.empty env t in
+ let type_t' = Typing.type_of env Evd.empty t' in
+ let new_env = Environ.push_rel (n,Some t',type_t') env in
let new_b,id_to_exclude =
- rebuild_cons
+ rebuild_cons new_env
nb_args relname
args (t::crossed_types)
(depth + 1 ) b in
@@ -968,14 +1078,16 @@ let rec rebuild_cons nb_args relname args crossed_types depth rt =
begin
let not_free_in_t id = not (is_free_in id t) in
let new_t,id_to_exclude' =
- rebuild_cons
+ rebuild_cons env
nb_args
relname
args (crossed_types)
depth t
in
+ let t' = Pretyping.Default.understand Evd.empty env new_t in
+ let new_env = Environ.push_rel (na,None,t') env in
let new_b,id_to_exclude =
- rebuild_cons
+ rebuild_cons new_env
nb_args relname
args (t::crossed_types)
(depth + 1) b
@@ -993,11 +1105,11 @@ let rec rebuild_cons nb_args relname args crossed_types depth rt =
(* debuging wrapper *)
-let rebuild_cons nb_args relname args crossed_types rt =
+let rebuild_cons env nb_args relname args crossed_types rt =
(* observennl (str "rebuild_cons : rt := "++ pr_rawconstr rt ++ *)
(* str "nb_args := " ++ str (string_of_int nb_args)); *)
let res =
- rebuild_cons nb_args relname args crossed_types 0 rt
+ rebuild_cons env nb_args relname args crossed_types 0 rt
in
(* observe (str " leads to "++ pr_rawconstr (fst res)); *)
res
@@ -1103,6 +1215,35 @@ let do_build_inductive
(Global.env ())
in
let resa = Array.map (build_entry_lc env funnames_as_set []) rta in
+ let env_with_graphs =
+ let rel_arity i funargs = (* Reduilding arities (with parameters) *)
+ let rel_first_args :(Names.name * Rawterm.rawconstr * bool ) list =
+ funargs
+ in
+ List.fold_right
+ (fun (n,t,is_defined) acc ->
+ if is_defined
+ then
+ Topconstr.CLetIn(dummy_loc,(dummy_loc, n),Constrextern.extern_rawconstr Idset.empty t,
+ acc)
+ else
+ Topconstr.CProdN
+ (dummy_loc,
+ [[(dummy_loc,n)],Topconstr.default_binder_kind,Constrextern.extern_rawconstr Idset.empty t],
+ acc
+ )
+ )
+ rel_first_args
+ (rebuild_return_type returned_types.(i))
+ in
+ (* We need to lift back our work topconstr but only with all information
+ We mimick a Set Printing All.
+ Then save the graphs and reset Printing options to their primitive values
+ *)
+ let rel_arities = Array.mapi rel_arity funsargs in
+ Util.array_fold_left2 (fun env rel_name rel_ar ->
+ Environ.push_named (rel_name,None, Constrintern.interp_constr Evd.empty env rel_ar) env) env relnames rel_arities
+ in
(* and of the real constructors*)
let constr i res =
List.map
@@ -1111,7 +1252,7 @@ let do_build_inductive
let nb_args = List.length funsargs.(i) in
(* with_full_print (fun rt -> Pp.msgnl (str "raw constr " ++ pr_rawconstr rt)) rt; *)
fst (
- rebuild_cons nb_args relnames.(i)
+ rebuild_cons env_with_graphs nb_args relnames.(i)
[]
[]
rt
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-05 22:00:02 +0000