aboutsummaryrefslogtreecommitdiff
path: root/plugins/funind
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/funind')
-rw-r--r--plugins/funind/FunInd.v10
-rw-r--r--plugins/funind/Recdef.v10
-rw-r--r--plugins/funind/functional_principles_proofs.ml79
-rw-r--r--plugins/funind/functional_principles_proofs.mli1
-rw-r--r--plugins/funind/functional_principles_types.ml123
-rw-r--r--plugins/funind/functional_principles_types.mli25
-rw-r--r--plugins/funind/g_indfun.ml443
-rw-r--r--plugins/funind/glob_term_to_relation.ml339
-rw-r--r--plugins/funind/glob_term_to_relation.mli3
-rw-r--r--plugins/funind/glob_termops.ml323
-rw-r--r--plugins/funind/glob_termops.mli33
-rw-r--r--plugins/funind/indfun.ml216
-rw-r--r--plugins/funind/indfun.mli12
-rw-r--r--plugins/funind/indfun_common.ml88
-rw-r--r--plugins/funind/indfun_common.mli32
-rw-r--r--plugins/funind/invfun.ml96
-rw-r--r--plugins/funind/invfun.mli19
-rw-r--r--plugins/funind/merge.ml1002
-rw-r--r--plugins/funind/recdef.ml190
-rw-r--r--plugins/funind/recdef.mli9
-rw-r--r--plugins/funind/recdef_plugin.mlpack1
21 files changed, 794 insertions, 1860 deletions
diff --git a/plugins/funind/FunInd.v b/plugins/funind/FunInd.v
index b8a05e5cc0..12458c1072 100644
--- a/plugins/funind/FunInd.v
+++ b/plugins/funind/FunInd.v
@@ -1,9 +1,11 @@
(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
Require Coq.extraction.Extraction.
diff --git a/plugins/funind/Recdef.v b/plugins/funind/Recdef.v
index 8b4dbbb45c..d94e62b45a 100644
--- a/plugins/funind/Recdef.v
+++ b/plugins/funind/Recdef.v
@@ -1,9 +1,11 @@
(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
Require Export Coq.funind.FunInd.
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index ba46f78aa8..5336948642 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -1,8 +1,7 @@
-open API
open Printer
open CErrors
open Util
-open Term
+open Constr
open EConstr
open Vars
open Namegen
@@ -45,6 +44,10 @@ let observe_tac s tac g = observe_tac_stream (str s) tac g
*)
+let pr_leconstr_fp =
+ let sigma, env = Pfedit.get_current_context () in
+ Printer.pr_leconstr_env env sigma
+
let debug_queue = Stack.create ()
let rec print_debug_queue e =
@@ -173,7 +176,7 @@ let is_incompatible_eq sigma t =
| _ -> false
with e when CErrors.noncritical e -> false
in
- if res then observe (str "is_incompatible_eq " ++ Printer.pr_leconstr t);
+ if res then observe (str "is_incompatible_eq " ++ pr_leconstr_fp t);
res
let change_hyp_with_using msg hyp_id t tac : tactic =
@@ -221,12 +224,13 @@ let find_rectype env sigma c =
let isAppConstruct ?(env=Global.env ()) sigma t =
try
let t',l = find_rectype env sigma t in
- observe (str "isAppConstruct : " ++ Printer.pr_leconstr t ++ str " -> " ++ Printer.pr_leconstr (applist (t',l)));
+ observe (str "isAppConstruct : " ++ Printer.pr_leconstr_env env sigma t ++ str " -> " ++
+ Printer.pr_leconstr_env env sigma (applist (t',l)));
true
with Not_found -> false
let nf_betaiotazeta = (* Reductionops.local_strong Reductionops.whd_betaiotazeta *)
- Reductionops.clos_norm_flags CClosure.betaiotazeta Environ.empty_env Evd.empty
+ Reductionops.clos_norm_flags CClosure.betaiotazeta Environ.empty_env @@ Evd.from_env Environ.empty_env
exception NoChange
@@ -234,11 +238,12 @@ exception NoChange
let change_eq env sigma hyp_id (context:rel_context) x t end_of_type =
let nochange ?t' msg =
begin
- observe (str ("Not treating ( "^msg^" )") ++ pr_leconstr t ++ str " " ++ match t' with None -> str "" | Some t -> Printer.pr_leconstr t );
+ observe (str ("Not treating ( "^msg^" )") ++ pr_leconstr_env env sigma t ++ str " " ++
+ match t' with None -> str "" | Some t -> Printer.pr_leconstr_env env sigma t );
raise NoChange;
end
in
- let eq_constr c1 c2 = Evarconv.e_conv env (ref sigma) c1 c2 in
+ let eq_constr c1 c2 = Option.has_some (Evarconv.conv env sigma c1 c2) in
if not (noccurn sigma 1 end_of_type)
then nochange "dependent"; (* if end_of_type depends on this term we don't touch it *)
if not (isApp sigma t) then nochange "not an equality";
@@ -319,7 +324,7 @@ let change_eq env sigma hyp_id (context:rel_context) x t end_of_type =
context
in
let new_type_of_hyp =
- Reductionops.nf_betaiota sigma new_type_of_hyp in
+ Reductionops.nf_betaiota env sigma new_type_of_hyp in
let new_ctxt,new_end_of_type =
decompose_prod_n_assum sigma ctxt_size new_type_of_hyp
in
@@ -409,9 +414,9 @@ let rewrite_until_var arg_num eq_ids : tactic =
let rec_pte_id = Id.of_string "Hrec"
let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma =
- let coq_False = EConstr.of_constr (Universes.constr_of_global @@ Coqlib.build_coq_False ()) in
- let coq_True = EConstr.of_constr (Universes.constr_of_global @@ Coqlib.build_coq_True ()) in
- let coq_I = EConstr.of_constr (Universes.constr_of_global @@ Coqlib.build_coq_I ()) in
+ let coq_False = EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.build_coq_False ()) in
+ let coq_True = EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.build_coq_True ()) in
+ let coq_I = EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.build_coq_I ()) in
let rec scan_type context type_of_hyp : tactic =
if isLetIn sigma type_of_hyp then
let real_type_of_hyp = it_mkProd_or_LetIn type_of_hyp context in
@@ -588,12 +593,12 @@ let treat_new_case ptes_infos nb_prod continue_tac term dyn_infos =
tclTHENLIST
[
(* We first introduce the variables *)
- tclDO nb_first_intro (Proofview.V82.of_tactic (intro_avoiding dyn_infos.rec_hyps));
+ tclDO nb_first_intro (Proofview.V82.of_tactic (intro_avoiding (Id.Set.of_list dyn_infos.rec_hyps)));
(* Then the equation itself *)
Proofview.V82.of_tactic (intro_using heq_id);
onLastHypId (fun heq_id -> tclTHENLIST [
(* Then the new hypothesis *)
- tclMAP (fun id -> Proofview.V82.of_tactic (introduction ~check:false id)) dyn_infos.rec_hyps;
+ tclMAP (fun id -> Proofview.V82.of_tactic (introduction id)) dyn_infos.rec_hyps;
observe_tac "after_introduction" (fun g' ->
(* We get infos on the equations introduced*)
let new_term_value_eq = pf_unsafe_type_of g' (mkVar heq_id) in
@@ -693,6 +698,7 @@ let build_proof
: tactic =
let rec build_proof_aux do_finalize dyn_infos : tactic =
fun g ->
+ let env = pf_env g in
let sigma = project g in
(* observe (str "proving on " ++ Printer.pr_lconstr_env (pf_env g) term);*)
match EConstr.kind sigma dyn_infos.info with
@@ -789,7 +795,7 @@ let build_proof
do_finalize dyn_infos g
| Lambda _ ->
let new_term =
- Reductionops.nf_beta sigma dyn_infos.info in
+ Reductionops.nf_beta env sigma dyn_infos.info in
build_proof do_finalize {dyn_infos with info = new_term}
g
| LetIn _ ->
@@ -822,8 +828,9 @@ let build_proof
| Fix _ | CoFix _ ->
user_err Pp.(str ( "Anonymous local (co)fixpoints are not handled yet"))
+
| Proj _ -> user_err Pp.(str "Prod")
- | Prod _ -> user_err Pp.(str "Prod")
+ | Prod _ -> do_finalize dyn_infos g
| LetIn _ ->
let new_infos =
{ dyn_infos with
@@ -841,7 +848,7 @@ let build_proof
| Rel _ -> anomaly (Pp.str "Free var in goal conclusion!")
and build_proof do_finalize dyn_infos g =
(* observe (str "proving with "++Printer.pr_lconstr dyn_infos.info++ str " on goal " ++ pr_gls g); *)
- observe_tac_stream (str "build_proof with " ++ Printer.pr_leconstr dyn_infos.info ) (build_proof_aux do_finalize dyn_infos) g
+ observe_tac_stream (str "build_proof with " ++ pr_leconstr_fp dyn_infos.info ) (build_proof_aux do_finalize dyn_infos) g
and build_proof_args do_finalize dyn_infos (* f_args' args *) :tactic =
fun g ->
let (f_args',args) = dyn_infos.info in
@@ -957,7 +964,7 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num
(* observe (str "rec_args_num := " ++ str (string_of_int (rec_args_num + 1) )); *)
let f_def = Global.lookup_constant (fst (destConst evd f)) in
let eq_lhs = mkApp(f,Array.init (nb_params + nb_args) (fun i -> mkRel(nb_params + nb_args - i))) in
- let f_body = Option.get (Global.body_of_constant_body f_def) in
+ let (f_body, _) = Option.get (Global.body_of_constant_body f_def) in
let f_body = EConstr.of_constr f_body in
let params,f_body_with_params = decompose_lam_n evd nb_params f_body in
let (_,num),(_,_,bodies) = destFix evd f_body_with_params in
@@ -1006,7 +1013,7 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num
lemma_type
(Lemmas.mk_hook (fun _ _ -> ()));
ignore (Pfedit.by (Proofview.V82.tactic prove_replacement));
- Lemmas.save_proof (Vernacexpr.(Proved(Transparent,None)));
+ Lemmas.save_proof (Vernacexpr.(Proved(Proof_global.Transparent,None)));
evd
@@ -1043,9 +1050,9 @@ let do_replace (evd:Evd.evar_map ref) params rec_arg_num rev_args_id f fun_num a
(Global.env ()) !evd
(Constrintern.locate_reference (qualid_of_ident equation_lemma_id))
in
- let res = EConstr.of_constr res in
- evd:=evd';
- let _ = Typing.e_type_of ~refresh:true (Global.env ()) evd res in
+ evd:=evd';
+ let sigma, _ = Typing.type_of ~refresh:true (Global.env ()) !evd res in
+ evd := sigma;
res
in
let nb_intro_to_do = nb_prod (project g) (pf_concl g) in
@@ -1091,11 +1098,13 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
in
let get_body const =
match Global.body_of_constant const with
- | Some body ->
+ | Some (body, _) ->
+ let env = Global.env () in
+ let sigma = Evd.from_env env in
Tacred.cbv_norm_flags
(CClosure.RedFlags.mkflags [CClosure.RedFlags.fZETA])
- (Global.env ())
- (Evd.empty)
+ env
+ sigma
(EConstr.of_constr body)
| None -> user_err Pp.(str "Cannot define a principle over an axiom ")
in
@@ -1135,7 +1144,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
princ_params
);
observe (str "fbody_with_full_params := " ++
- pr_leconstr fbody_with_full_params
+ pr_leconstr_env (Global.env ()) !evd fbody_with_full_params
);
let all_funs_with_full_params =
Array.map (fun f -> applist(f, List.rev_map var_of_decl full_params)) all_funs
@@ -1147,7 +1156,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
let bodies_with_all_params =
Array.map
(fun body ->
- Reductionops.nf_betaiota (project g)
+ Reductionops.nf_betaiota (pf_env g) (project g)
(applist(substl (List.rev (Array.to_list all_funs_with_full_params)) body,
List.rev_map var_of_decl princ_params))
)
@@ -1185,12 +1194,12 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
let body_with_param,num =
let body = get_body fnames.(i) in
let body_with_full_params =
- Reductionops.nf_betaiota (project g) (
+ Reductionops.nf_betaiota (pf_env g) (project g) (
applist(body,List.rev_map var_of_decl full_params))
in
match EConstr.kind (project g) body_with_full_params with
| Fix((_,num),(_,_,bs)) ->
- Reductionops.nf_betaiota (project g)
+ Reductionops.nf_betaiota (pf_env g) (project g)
(
(applist
(substl
@@ -1235,7 +1244,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
if this_fix_info.idx + 1 = 0
then tclIDTAC (* Someone tries to defined a principle on a fully parametric definition declared as a fixpoint (strange but ....) *)
else
- observe_tac_stream (str "h_fix " ++ int (this_fix_info.idx +1) ) (Proofview.V82.of_tactic (fix (Some this_fix_info.name) (this_fix_info.idx +1)))
+ observe_tac_stream (str "h_fix " ++ int (this_fix_info.idx +1) ) (Proofview.V82.of_tactic (fix this_fix_info.name (this_fix_info.idx +1)))
else
Proofview.V82.of_tactic (Tactics.mutual_fix this_fix_info.name (this_fix_info.idx + 1)
other_fix_infos 0)
@@ -1273,7 +1282,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
nb_rec_hyps = -100;
rec_hyps = [];
info =
- Reductionops.nf_betaiota (project g)
+ Reductionops.nf_betaiota (pf_env g) (project g)
(applist(fix_body,List.rev_map mkVar args_id));
eq_hyps = []
}
@@ -1333,7 +1342,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
nb_rec_hyps = -100;
rec_hyps = [];
info =
- Reductionops.nf_betaiota Evd.empty
+ Reductionops.nf_betaiota (pf_env g) (project g)
(applist(fbody_with_full_params,
(List.rev_map var_of_decl princ_params)@
(List.rev_map mkVar args_id)
@@ -1382,7 +1391,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
(* Proof of principles of general functions *)
-(* let hrec_id =
+(* let hrec_id = Recdef.hrec_id *)
(* and acc_inv_id = Recdef.acc_inv_id *)
(* and ltof_ref = Recdef.ltof_ref *)
(* and acc_rel = Recdef.acc_rel *)
@@ -1596,7 +1605,7 @@ let prove_principle_for_gen
match !tcc_lemma_ref with
| Undefined -> user_err Pp.(str "No tcc proof !!")
| Value lemma -> EConstr.of_constr lemma
- | Not_needed -> EConstr.of_constr (Universes.constr_of_global @@ Coqlib.build_coq_I ())
+ | Not_needed -> EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.build_coq_I ())
in
(* let rec list_diff del_list check_list = *)
(* match del_list with *)
@@ -1614,7 +1623,7 @@ let prove_principle_for_gen
let hid =
next_ident_away_in_goal
(Id.of_string "prov")
- hyps
+ (Id.Set.of_list hyps)
in
tclTHENLIST
[
@@ -1650,7 +1659,7 @@ let prove_principle_for_gen
(* observe_tac "reverting" *) (revert (List.rev (acc_rec_arg_id::args_ids)));
(* (fun g -> observe (Printer.pr_goal (sig_it g) ++ fnl () ++ *)
(* str "fix arg num" ++ int (List.length args_ids + 1) ); tclIDTAC g); *)
- (* observe_tac "h_fix " *) (Proofview.V82.of_tactic (fix (Some fix_id) (List.length args_ids + 1)));
+ (* observe_tac "h_fix " *) (Proofview.V82.of_tactic (fix fix_id (List.length args_ids + 1)));
(* (fun g -> observe (Printer.pr_goal (sig_it g) ++ fnl() ++ pr_lconstr_env (pf_env g ) (pf_unsafe_type_of g (mkVar fix_id) )); tclIDTAC g); *)
h_intros (List.rev (acc_rec_arg_id::args_ids));
Proofview.V82.of_tactic (Equality.rewriteLR (mkConst eq_ref));
diff --git a/plugins/funind/functional_principles_proofs.mli b/plugins/funind/functional_principles_proofs.mli
index d03fc475e0..64fbfaeedf 100644
--- a/plugins/funind/functional_principles_proofs.mli
+++ b/plugins/funind/functional_principles_proofs.mli
@@ -1,4 +1,3 @@
-open API
open Names
val prove_princ_for_struct :
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 8ffd15f9fb..b2a528a1fd 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -1,8 +1,9 @@
-open API
open Printer
open CErrors
-open Util
open Term
+open Sorts
+open Util
+open Constr
open Vars
open Namegen
open Names
@@ -12,7 +13,6 @@ open Tactics
open Context.Rel.Declaration
open Indfun_common
open Functional_principles_proofs
-open Misctypes
module RelDecl = Context.Rel.Declaration
@@ -41,7 +41,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
| decl :: predicates ->
(match Context.Rel.Declaration.get_name decl with
| Name x ->
- let id = Namegen.next_ident_away x avoid in
+ let id = Namegen.next_ident_away x (Id.Set.of_list avoid) in
Hashtbl.add tbl id x;
RelDecl.set_name (Name id) decl :: change_predicates_names (id::avoid) predicates
| Anonymous -> anomaly (Pp.str "Anonymous property binder."))
@@ -82,7 +82,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
let is_pte =
let set = List.fold_right Id.Set.add ptes_vars Id.Set.empty in
fun t ->
- match kind_of_term t with
+ match Constr.kind t with
| Var id -> Id.Set.mem id set
| _ -> false
in
@@ -102,13 +102,13 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
let pre_princ = EConstr.Unsafe.to_constr pre_princ in
let pre_princ = substl (List.map mkVar ptes_vars) pre_princ in
let is_dom c =
- match kind_of_term c with
+ match Constr.kind c with
| Ind((u,_),_) -> MutInd.equal u rel_as_kn
| Construct(((u,_),_),_) -> MutInd.equal u rel_as_kn
| _ -> false
in
let get_fun_num c =
- match kind_of_term c with
+ match Constr.kind c with
| Ind((_,num),_) -> num
| Construct(((_,num),_),_) -> num
| _ -> assert false
@@ -116,12 +116,14 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
let dummy_var = mkVar (Id.of_string "________") in
let mk_replacement c i args =
let res = mkApp(rel_to_fun.(i), Array.map pop (array_get_start args)) in
- observe (str "replacing " ++ pr_lconstr c ++ str " by " ++ pr_lconstr res);
+ observe (str "replacing " ++
+ pr_lconstr_env env Evd.empty c ++ str " by " ++
+ pr_lconstr_env env Evd.empty res);
res
in
let rec compute_new_princ_type remove env pre_princ : types*(constr list) =
let (new_princ_type,_) as res =
- match kind_of_term pre_princ with
+ match Constr.kind pre_princ with
| Rel n ->
begin
try match Environ.lookup_rel n env with
@@ -151,12 +153,12 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
in
let new_f,binders_to_remove_from_f = compute_new_princ_type remove env f in
applistc new_f new_args,
- list_union_eq eq_constr binders_to_remove_from_f binders_to_remove
+ list_union_eq Constr.equal binders_to_remove_from_f binders_to_remove
| LetIn(x,v,t,b) ->
compute_new_princ_type_for_letin remove env x v t b
| _ -> pre_princ,[]
in
-(* let _ = match kind_of_term pre_princ with *)
+(* let _ = match Constr.kind pre_princ with *)
(* | Prod _ -> *)
(* observe(str "compute_new_princ_type for "++ *)
(* pr_lconstr_env env pre_princ ++ *)
@@ -172,13 +174,13 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
let new_x : Name.t = get_name (Termops.ids_of_context env) x in
let new_env = Environ.push_rel (LocalAssum (x,t)) env in
let new_b,binders_to_remove_from_b = compute_new_princ_type remove new_env b in
- if List.exists (eq_constr (mkRel 1)) binders_to_remove_from_b
- then (pop new_b), filter_map (eq_constr (mkRel 1)) pop binders_to_remove_from_b
+ if List.exists (Constr.equal (mkRel 1)) binders_to_remove_from_b
+ then (pop new_b), filter_map (Constr.equal (mkRel 1)) pop binders_to_remove_from_b
else
(
bind_fun(new_x,new_t,new_b),
list_union_eq
- eq_constr
+ Constr.equal
binders_to_remove_from_t
(List.map pop binders_to_remove_from_b)
)
@@ -191,7 +193,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
| Toberemoved_with_rel (n,c) ->
(* observe (str "Decl of "++Ppconstr.Name.print x ++ str " is removed "); *)
let new_b,binders_to_remove_from_b = compute_new_princ_type remove env (substnl [c] n b) in
- new_b, list_add_set_eq eq_constr (mkRel n) (List.map pop binders_to_remove_from_b)
+ new_b, list_add_set_eq Constr.equal (mkRel n) (List.map pop binders_to_remove_from_b)
end
and compute_new_princ_type_for_letin remove env x v t b =
begin
@@ -201,14 +203,14 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
let new_x : Name.t = get_name (Termops.ids_of_context env) x in
let new_env = Environ.push_rel (LocalDef (x,v,t)) env in
let new_b,binders_to_remove_from_b = compute_new_princ_type remove new_env b in
- if List.exists (eq_constr (mkRel 1)) binders_to_remove_from_b
- then (pop new_b),filter_map (eq_constr (mkRel 1)) pop binders_to_remove_from_b
+ if List.exists (Constr.equal (mkRel 1)) binders_to_remove_from_b
+ then (pop new_b),filter_map (Constr.equal (mkRel 1)) pop binders_to_remove_from_b
else
(
mkLetIn(new_x,new_v,new_t,new_b),
list_union_eq
- eq_constr
- (list_union_eq eq_constr binders_to_remove_from_t binders_to_remove_from_v)
+ Constr.equal
+ (list_union_eq Constr.equal binders_to_remove_from_t binders_to_remove_from_v)
(List.map pop binders_to_remove_from_b)
)
@@ -220,12 +222,12 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
| Toberemoved_with_rel (n,c) ->
(* observe (str "Decl of "++Ppconstr.Name.print x ++ str " is removed "); *)
let new_b,binders_to_remove_from_b = compute_new_princ_type remove env (substnl [c] n b) in
- new_b, list_add_set_eq eq_constr (mkRel n) (List.map pop binders_to_remove_from_b)
+ new_b, list_add_set_eq Constr.equal (mkRel n) (List.map pop binders_to_remove_from_b)
end
and compute_new_princ_type_with_acc remove env e (c_acc,to_remove_acc) =
let new_e,to_remove_from_e = compute_new_princ_type remove env e
in
- new_e::c_acc,list_union_eq eq_constr to_remove_from_e to_remove_acc
+ new_e::c_acc,list_union_eq Constr.equal to_remove_from_e to_remove_acc
in
(* observe (str "Computing new principe from " ++ pr_lconstr_env env_with_params_and_predicates pre_princ); *)
let pre_res,_ =
@@ -264,7 +266,7 @@ let change_property_sort evd toSort princ princName =
(Global.env ()) evd (Constrintern.locate_reference (Libnames.qualid_of_ident princName)) in
let init =
let nargs = (princ_info.nparams + (List.length princ_info.predicates)) in
- mkApp(princName_as_constr,
+ mkApp(EConstr.Unsafe.to_constr princName_as_constr,
Array.init nargs
(fun i -> mkRel (nargs - i )))
in
@@ -287,9 +289,10 @@ let build_functional_principle (evd:Evd.evar_map ref) interactive_proof old_prin
(* let time2 = System.get_time () in *)
(* Pp.msgnl (str "computing principle type := " ++ System.fmt_time_difference time1 time2); *)
let new_princ_name =
- next_ident_away_in_goal (Id.of_string "___________princ_________") []
+ next_ident_away_in_goal (Id.of_string "___________princ_________") Id.Set.empty
in
- let _ = Typing.e_type_of ~refresh:true (Global.env ()) evd (EConstr.of_constr new_principle_type) in
+ let sigma, _ = Typing.type_of ~refresh:true (Global.env ()) !evd (EConstr.of_constr new_principle_type) in
+ evd := sigma;
let hook = Lemmas.mk_hook (hook new_principle_type) in
begin
Lemmas.start_proof
@@ -319,8 +322,7 @@ let generate_functional_principle (evd: Evd.evar_map ref)
try
let f = funs.(i) in
- let env = Global.env () in
- let type_sort = Evarutil.evd_comb1 (Evd.fresh_sort_in_family env) evd InType in
+ let type_sort = Evarutil.evd_comb1 Evd.fresh_sort_in_family evd InType in
let new_sorts =
match sorts with
| None -> Array.make (Array.length funs) (type_sort)
@@ -331,7 +333,7 @@ let generate_functional_principle (evd: Evd.evar_map ref)
| Some (id) -> id,id
| None ->
let id_of_f = Label.to_id (Constant.label (fst f)) in
- id_of_f,Indrec.make_elimination_ident id_of_f (family_of_sort type_sort)
+ id_of_f,Indrec.make_elimination_ident id_of_f (Sorts.family type_sort)
in
let names = ref [new_princ_name] in
let hook =
@@ -340,14 +342,18 @@ let generate_functional_principle (evd: Evd.evar_map ref)
then
(* let id_of_f = Label.to_id (con_label f) in *)
let register_with_sort fam_sort =
- let evd' = Evd.from_env (Global.env ()) in
- let evd',s = Evd.fresh_sort_in_family env evd' fam_sort in
- let name = Indrec.make_elimination_ident base_new_princ_name fam_sort in
- let evd',value = change_property_sort evd' s new_principle_type new_princ_name in
- let evd' = fst (Typing.type_of ~refresh:true (Global.env ()) evd' (EConstr.of_constr value)) in
- (* Pp.msgnl (str "new principle := " ++ pr_lconstr value); *)
- let ce = Declare.definition_entry ~poly:(Flags.is_universe_polymorphism ()) ~univs:(snd (Evd.universe_context evd')) value in
- ignore(
+ let evd' = Evd.from_env (Global.env ()) in
+ let evd',s = Evd.fresh_sort_in_family evd' fam_sort in
+ let name = Indrec.make_elimination_ident base_new_princ_name fam_sort in
+ let evd',value = change_property_sort evd' s new_principle_type new_princ_name in
+ let evd' = fst (Typing.type_of ~refresh:true (Global.env ()) evd' (EConstr.of_constr value)) in
+ (* Pp.msgnl (str "new principle := " ++ pr_lconstr value); *)
+ let univs =
+ let poly = Flags.is_universe_polymorphism () in
+ Evd.const_univ_entry ~poly evd'
+ in
+ let ce = Declare.definition_entry ~univs value in
+ ignore(
Declare.declare_constant
name
(DefinitionEntry ce,
@@ -390,7 +396,7 @@ exception Not_Rec
let get_funs_constant mp dp =
let get_funs_constant const e : (Names.Constant.t*int) array =
- match kind_of_term ((strip_lam e)) with
+ match Constr.kind ((strip_lam e)) with
| Fix((_,(na,_,_))) ->
Array.mapi
(fun i na ->
@@ -407,7 +413,7 @@ let get_funs_constant mp dp =
function const ->
let find_constant_body const =
match Global.body_of_constant const with
- | Some body ->
+ | Some (body, _) ->
let body = Tacred.cbv_norm_flags
(CClosure.RedFlags.mkflags [CClosure.RedFlags.fZETA])
(Global.env ())
@@ -431,7 +437,7 @@ let get_funs_constant mp dp =
let first_params = List.hd l_params in
List.iter
(fun params ->
- if not (List.equal (fun (n1, c1) (n2, c2) -> Name.equal n1 n2 && eq_constr c1 c2) first_params params)
+ if not (List.equal (fun (n1, c1) (n2, c2) -> Name.equal n1 n2 && Constr.equal c1 c2) first_params params)
then user_err Pp.(str "Not a mutal recursive block")
)
l_params
@@ -440,7 +446,7 @@ let get_funs_constant mp dp =
let _check_bodies =
try
let extract_info is_first body =
- match kind_of_term body with
+ match Constr.kind body with
| Fix((idxs,_),(na,ta,ca)) -> (idxs,na,ta,ca)
| _ ->
if is_first && Int.equal (List.length l_bodies) 1
@@ -451,7 +457,7 @@ let get_funs_constant mp dp =
let check body = (* Hope this is correct *)
let eq_infos (ia1, na1, ta1, ca1) (ia2, na2, ta2, ca2) =
Array.equal Int.equal ia1 ia2 && Array.equal Name.equal na1 na2 &&
- Array.equal eq_constr ta1 ta2 && Array.equal eq_constr ca1 ca2
+ Array.equal Constr.equal ta1 ta2 && Array.equal Constr.equal ca1 ca2
in
if not (eq_infos first_infos (extract_info false body))
then user_err Pp.(str "Not a mutal recursive block")
@@ -464,7 +470,7 @@ let get_funs_constant mp dp =
exception No_graph_found
exception Found_type of int
-let make_scheme evd (fas : (pconstant*glob_sort) list) : Safe_typing.private_constants definition_entry list =
+let make_scheme evd (fas : (pconstant*Sorts.family) list) : Safe_typing.private_constants definition_entry list =
let env = Global.env () in
let funs = List.map fst fas in
let first_fun = List.hd funs in
@@ -501,8 +507,8 @@ let make_scheme evd (fas : (pconstant*glob_sort) list) : Safe_typing.private_con
let i = ref (-1) in
let sorts =
List.rev_map (fun (_,x) ->
- Evarutil.evd_comb1 (Evd.fresh_sort_in_family env) evd (Pretyping.interp_elimination_sort x)
- )
+ Evarutil.evd_comb1 Evd.fresh_sort_in_family evd x
+ )
fas
in
(* We create the first priciple by tactic *)
@@ -565,7 +571,7 @@ let make_scheme evd (fas : (pconstant*glob_sort) list) : Safe_typing.private_con
List.map (* we can now compute the other principles *)
(fun scheme_type ->
incr i;
- observe (Printer.pr_lconstr scheme_type);
+ observe (Printer.pr_lconstr_env env sigma scheme_type);
let type_concl = (strip_prod_assum scheme_type) in
let applied_f = List.hd (List.rev (snd (decompose_app type_concl))) in
let f = fst (decompose_app applied_f) in
@@ -575,10 +581,10 @@ let make_scheme evd (fas : (pconstant*glob_sort) list) : Safe_typing.private_con
let t = (strip_prod_assum t) in
let applied_g = List.hd (List.rev (snd (decompose_app t))) in
let g = fst (decompose_app applied_g) in
- if eq_constr f g
+ if Constr.equal f g
then raise (Found_type j);
- observe (Printer.pr_lconstr f ++ str " <> " ++
- Printer.pr_lconstr g)
+ observe (Printer.pr_lconstr_env env sigma f ++ str " <> " ++
+ Printer.pr_lconstr_env env sigma g)
)
ta;
@@ -620,18 +626,25 @@ let build_scheme fas =
Smartlocate.global_with_alias f
with Not_found ->
user_err ~hdr:"FunInd.build_scheme"
- (str "Cannot find " ++ Libnames.pr_reference f)
+ (str "Cannot find " ++ Libnames.pr_qualid f)
in
- let evd',f = Evd.fresh_global (Global.env ()) !evd f_as_constant in
+ let evd',f = Evd.fresh_global (Global.env ()) !evd f_as_constant in
let _ = evd := evd' in
- let _ = Typing.e_type_of ~refresh:true (Global.env ()) evd (EConstr.of_constr f) in
- (destConst f,sort)
- )
+ let sigma, _ = Typing.type_of ~refresh:true (Global.env ()) !evd f in
+ evd := sigma;
+ let c, u =
+ try EConstr.destConst !evd f
+ with DestKO ->
+ user_err Pp.(pr_econstr_env (Global.env ()) !evd f ++spc () ++ str "should be the named of a globally defined function")
+ in
+ (c, EConstr.EInstance.kind !evd u), sort
+ )
fas
) in
let bodies_types =
make_scheme evd pconstants
in
+
List.iter2
(fun (princ_id,_,_) def_entry ->
ignore
@@ -651,10 +664,10 @@ let build_case_scheme fa =
(* in *)
let funs =
let (_,f,_) = fa in
- try fst (Universes.unsafe_constr_of_global (Smartlocate.global_with_alias f))
+ try fst (Global.constr_of_global_in_context (Global.env ()) (Smartlocate.global_with_alias f))
with Not_found ->
user_err ~hdr:"FunInd.build_case_scheme"
- (str "Cannot find " ++ Libnames.pr_reference f) in
+ (str "Cannot find " ++ Libnames.pr_qualid f) in
let first_fun,u = destConst funs in
let funs_mp,funs_dp,_ = Constant.repr3 first_fun in
let first_fun_kn = try fst (find_Function_infos first_fun).graph_ind with Not_found -> raise No_graph_found in
@@ -675,7 +688,7 @@ let build_case_scheme fa =
let scheme_type = EConstr.Unsafe.to_constr ((Typing.unsafe_type_of env sigma) (EConstr.of_constr scheme)) in
let sorts =
(fun (_,_,x) ->
- Universes.new_sort_in_family (Pretyping.interp_elimination_sort x)
+ UnivGen.new_sort_in_family x
)
fa
in
diff --git a/plugins/funind/functional_principles_types.mli b/plugins/funind/functional_principles_types.mli
index d6ad7ef0d2..97f9acdb3a 100644
--- a/plugins/funind/functional_principles_types.mli
+++ b/plugins/funind/functional_principles_types.mli
@@ -1,15 +1,15 @@
(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
-open API
open Names
-open Term
-open Misctypes
+open Constr
val generate_functional_principle :
Evd.evar_map ref ->
@@ -31,15 +31,10 @@ val generate_functional_principle :
(EConstr.constr array -> int -> Tacmach.tactic) ->
unit
-val compute_new_princ_type_from_rel : constr array -> Sorts.t array ->
- types -> types
-
-
exception No_graph_found
val make_scheme : Evd.evar_map ref ->
- (pconstant*glob_sort) list -> Safe_typing.private_constants Entries.definition_entry list
-
-val build_scheme : (Id.t*Libnames.reference*glob_sort) list -> unit
-val build_case_scheme : (Id.t*Libnames.reference*glob_sort) -> unit
+ (pconstant*Sorts.family) list -> Safe_typing.private_constants Entries.definition_entry list
+val build_scheme : (Id.t*Libnames.qualid*Sorts.family) list -> unit
+val build_case_scheme : (Id.t*Libnames.qualid*Sorts.family) -> unit
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index 56048f92e4..a2d31780dd 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -1,13 +1,12 @@
(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
-(*i camlp4deps: "grammar/grammar.cma" i*)
-open API
-open Grammar_API
open Ltac_plugin
open Util
open Pp
@@ -16,7 +15,8 @@ open Indfun_common
open Indfun
open Genarg
open Stdarg
-open Misctypes
+open Tacarg
+open Tactypes
open Pcoq
open Pcoq.Prim
open Pcoq.Constr
@@ -39,7 +39,9 @@ let pr_fun_ind_using_typed prc prlc _ opt_c =
match opt_c with
| None -> mt ()
| Some b ->
- let (_, b) = b (Global.env ()) Evd.empty in
+ let env = Global.env () in
+ let evd = Evd.from_env env in
+ let (_, b) = b env evd in
spc () ++ hov 2 (str "using" ++ spc () ++ Miscprint.pr_with_bindings prc prlc b)
@@ -69,9 +71,9 @@ let pr_intro_as_pat _prc _ _ pat =
str"<simple_intropattern>"
| None -> mt ()
-let out_disjunctive = function
- | loc, IntroAction (IntroOrAndPattern l) -> (loc,l)
- | _ -> CErrors.user_err Pp.(str "Disjunctive or conjunctive intro pattern expected.")
+let out_disjunctive = CAst.map (function
+ | IntroAction (IntroOrAndPattern l) -> l
+ | _ -> CErrors.user_err Pp.(str "Disjunctive or conjunctive intro pattern expected."))
ARGUMENT EXTEND with_names TYPED AS intropattern_opt PRINTED BY pr_intro_as_pat
| [ "as" simple_intropattern(ipat) ] -> [ Some ipat ]
@@ -124,7 +126,7 @@ ARGUMENT EXTEND auto_using'
END
module Gram = Pcoq.Gram
-module Vernac = Pcoq.Vernac_
+module Vernac = Pvernac.Vernac_
module Tactic = Pltac
type function_rec_definition_loc_argtype = (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) Loc.located
@@ -146,8 +148,7 @@ END
let () =
let raw_printer _ _ _ (loc,body) = Ppvernac.pr_rec_definition body in
- let printer _ _ _ _ = str "<Unavailable printer for rec_definition>" in
- Pptactic.declare_extra_genarg_pprule wit_function_rec_definition_loc raw_printer printer printer
+ Pptactic.declare_extra_vernac_genarg_pprule wit_function_rec_definition_loc raw_printer
(* TASSI: n'importe quoi ! *)
VERNAC COMMAND EXTEND Function
@@ -157,7 +158,7 @@ VERNAC COMMAND EXTEND Function
| _,((_,(_,CStructRec),_,_,_),_) -> false) recsl in
match
Vernac_classifier.classify_vernac
- (Vernacexpr.VernacFixpoint(None, List.map snd recsl))
+ (Vernacexpr.(VernacExpr([], VernacFixpoint(Decl_kinds.NoDischarge, List.map snd recsl))))
with
| Vernacexpr.VtSideff ids, _ when hard ->
Vernacexpr.(VtStartProof ("Classic", GuaranteesOpacity, ids), VtLater)
@@ -167,12 +168,12 @@ END
let pr_fun_scheme_arg (princ_name,fun_name,s) =
Names.Id.print princ_name ++ str " :=" ++ spc() ++ str "Induction for " ++
- Libnames.pr_reference fun_name ++ spc() ++ str "Sort " ++
- Ppconstr.pr_glob_sort s
+ Libnames.pr_qualid fun_name ++ spc() ++ str "Sort " ++
+ Termops.pr_sort_family s
VERNAC ARGUMENT EXTEND fun_scheme_arg
PRINTED BY pr_fun_scheme_arg
-| [ ident(princ_name) ":=" "Induction" "for" reference(fun_name) "Sort" sort(s) ] -> [ (princ_name,fun_name,s) ]
+| [ ident(princ_name) ":=" "Induction" "for" reference(fun_name) "Sort" sort_family(s) ] -> [ (princ_name,fun_name,s) ]
END
@@ -180,11 +181,11 @@ let warning_error names e =
let (e, _) = ExplainErr.process_vernac_interp_error (e, Exninfo.null) in
match e with
| Building_graph e ->
- let names = pr_enum Libnames.pr_reference names in
+ let names = pr_enum Libnames.pr_qualid names in
let error = if do_observe () then (spc () ++ CErrors.print e) else mt () in
warn_cannot_define_graph (names,error)
| Defining_principle e ->
- let names = pr_enum Libnames.pr_reference names in
+ let names = pr_enum Libnames.pr_qualid names in
let error = if do_observe () then CErrors.print e else mt () in
warn_cannot_define_principle (names,error)
| _ -> raise e
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index db2af2be53..5fc4293cbb 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -1,8 +1,7 @@
-open API
open Printer
open Pp
open Names
-open Term
+open Constr
open Vars
open Glob_term
open Glob_ops
@@ -11,7 +10,6 @@ open Indfun_common
open CErrors
open Util
open Glob_termops
-open Misctypes
module RelDecl = Context.Rel.Declaration
module NamedDecl = Context.Named.Declaration
@@ -33,6 +31,14 @@ type binder_type =
type glob_context = (binder_type*glob_constr) list
+
+let rec solve_trivial_holes pat_as_term e =
+ match DAst.get pat_as_term, DAst.get e with
+ | GHole _,_ -> e
+ | GApp(fp,argsp),GApp(fe,argse) when glob_constr_eq fp fe ->
+ DAst.make (GApp((solve_trivial_holes fp fe),List.map2 solve_trivial_holes argsp argse))
+ | _,_ -> pat_as_term
+
(*
compose_glob_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
@@ -113,13 +119,13 @@ let combine_args arg args =
let ids_of_binder = function
- | LetIn Anonymous | Prod Anonymous | Lambda Anonymous -> []
- | LetIn (Name id) | Prod (Name id) | Lambda (Name id) -> [id]
+ | LetIn Anonymous | Prod Anonymous | Lambda Anonymous -> Id.Set.empty
+ | LetIn (Name id) | Prod (Name id) | Lambda (Name id) -> Id.Set.singleton id
let rec change_vars_in_binder mapping = function
[] -> []
| (bt,t)::l ->
- let new_mapping = List.fold_right Id.Map.remove (ids_of_binder bt) mapping in
+ let new_mapping = Id.Set.fold Id.Map.remove (ids_of_binder bt) mapping in
(bt,change_vars mapping t)::
(if Id.Map.is_empty new_mapping
then l
@@ -130,27 +136,27 @@ let rec replace_var_by_term_in_binder x_id term = function
| [] -> []
| (bt,t)::l ->
(bt,replace_var_by_term x_id term t)::
- if Id.List.mem x_id (ids_of_binder bt)
+ if Id.Set.mem x_id (ids_of_binder bt)
then l
else replace_var_by_term_in_binder x_id term l
-let add_bt_names bt = List.append (ids_of_binder bt)
+let add_bt_names bt = Id.Set.union (ids_of_binder bt)
let apply_args ctxt body args =
let need_convert_id avoid id =
- List.exists (is_free_in id) args || Id.List.mem id avoid
+ List.exists (is_free_in id) args || Id.Set.mem id avoid
in
let need_convert avoid bt =
- List.exists (need_convert_id avoid) (ids_of_binder bt)
+ Id.Set.exists (need_convert_id avoid) (ids_of_binder bt)
in
- let next_name_away (na:Name.t) (mapping: Id.t Id.Map.t) (avoid: Id.t list) =
+ let next_name_away (na:Name.t) (mapping: Id.t Id.Map.t) (avoid: Id.Set.t) =
match na with
- | Name id when Id.List.mem id avoid ->
+ | Name id when Id.Set.mem id avoid ->
let new_id = Namegen.next_ident_away id avoid in
- Name new_id,Id.Map.add id new_id mapping,new_id::avoid
+ Name new_id,Id.Map.add id new_id mapping,Id.Set.add new_id avoid
| _ -> na,mapping,avoid
in
- let next_bt_away bt (avoid:Id.t list) =
+ let next_bt_away bt (avoid:Id.Set.t) =
match bt with
| LetIn na ->
let new_na,mapping,new_avoid = next_name_away na Id.Map.empty avoid in
@@ -175,15 +181,15 @@ let apply_args ctxt body args =
let new_avoid,new_ctxt',new_body,new_id =
if need_convert_id avoid id
then
- let new_avoid = id::avoid in
+ let new_avoid = Id.Set.add id avoid in
let new_id = Namegen.next_ident_away id new_avoid in
- let new_avoid' = new_id :: new_avoid in
+ let new_avoid' = Id.Set.add new_id new_avoid in
let mapping = Id.Map.add id new_id Id.Map.empty in
let new_ctxt' = change_vars_in_binder mapping ctxt' in
let new_body = change_vars mapping body in
new_avoid',new_ctxt',new_body,new_id
else
- id::avoid,ctxt',body,id
+ Id.Set.add id avoid,ctxt',body,id
in
let new_body = replace_var_by_term new_id arg new_body in
let new_ctxt' = replace_var_by_term_in_binder new_id arg new_ctxt' in
@@ -207,7 +213,7 @@ let apply_args ctxt body args =
in
(new_bt,t)::new_ctxt',new_body
in
- do_apply [] ctxt body args
+ do_apply Id.Set.empty ctxt body args
let combine_app f args =
@@ -227,7 +233,12 @@ let combine_lam n t b =
compose_glob_context b.context b.value )
}
-
+let combine_prod2 n t b =
+ {
+ context = [];
+ value = mkGProd(n, compose_glob_context t.context t.value,
+ compose_glob_context b.context b.value )
+ }
let combine_prod n t b =
{ context = t.context@((Prod n,t.value)::b.context); value = b.value}
@@ -275,7 +286,7 @@ let make_discr_match_el =
*)
let make_discr_match_brl i =
List.map_i
- (fun j (_,(idl,patl,_)) -> Loc.tag @@
+ (fun j {CAst.v=(idl,patl,_)} -> CAst.make @@
if Int.equal j i
then (idl,patl, mkGRef (Lazy.force coq_True_ref))
else (idl,patl, mkGRef (Lazy.force coq_False_ref))
@@ -340,16 +351,16 @@ let raw_push_named (na,raw_value,raw_typ) env =
let typ,_ = Pretyping.understand env (Evd.from_env env) ~expected_type:Pretyping.IsType raw_typ in
(match raw_value with
| None ->
- Environ.push_named (NamedDecl.LocalAssum (id,typ)) env
+ EConstr.push_named (NamedDecl.LocalAssum (id,typ)) env
| Some value ->
- Environ.push_named (NamedDecl.LocalDef (id, value, typ)) env)
+ EConstr.push_named (NamedDecl.LocalDef (id, value, typ)) env)
let add_pat_variables pat typ env : Environ.env =
let rec add_pat_variables env pat typ : Environ.env =
observe (str "new rel env := " ++ Printer.pr_rel_context_of env (Evd.from_env env));
- match pat.CAst.v with
+ match DAst.get pat with
| PatVar na -> Environ.push_rel (RelDecl.LocalAssum (na,typ)) env
| PatCstr(c,patl,na) ->
let Inductiveops.IndType(indf,indargs) =
@@ -366,29 +377,30 @@ let add_pat_variables pat typ env : Environ.env =
fst (
Context.Rel.fold_outside
(fun decl (env,ctxt) ->
- let open Context.Rel.Declaration in
- match decl with
+ let open Context.Rel.Declaration in
+ let sigma, _ = Pfedit.get_current_context () in
+ match decl with
| LocalAssum (Anonymous,_) | LocalDef (Anonymous,_,_) -> assert false
| LocalAssum (Name id, t) ->
- let new_t = substl ctxt t in
- observe (str "for variable " ++ Ppconstr.pr_id id ++ fnl () ++
- str "old type := " ++ Printer.pr_lconstr t ++ fnl () ++
- str "new type := " ++ Printer.pr_lconstr new_t ++ fnl ()
- );
- let open Context.Named.Declaration in
- (Environ.push_named (LocalAssum (id,new_t)) env,mkVar id::ctxt)
- | LocalDef (Name id, v, t) ->
- let new_t = substl ctxt t in
- let new_v = substl ctxt v in
- observe (str "for variable " ++ Ppconstr.pr_id id ++ fnl () ++
- str "old type := " ++ Printer.pr_lconstr t ++ fnl () ++
- str "new type := " ++ Printer.pr_lconstr new_t ++ fnl () ++
- str "old value := " ++ Printer.pr_lconstr v ++ fnl () ++
- str "new value := " ++ Printer.pr_lconstr new_v ++ fnl ()
- );
- let open Context.Named.Declaration in
- (Environ.push_named (LocalDef (id,new_v,new_t)) env,mkVar id::ctxt)
- )
+ let new_t = substl ctxt t in
+ observe (str "for variable " ++ Ppconstr.pr_id id ++ fnl () ++
+ str "old type := " ++ Printer.pr_lconstr_env env sigma t ++ fnl () ++
+ str "new type := " ++ Printer.pr_lconstr_env env sigma new_t ++ fnl ()
+ );
+ let open Context.Named.Declaration in
+ (Environ.push_named (LocalAssum (id,new_t)) env,mkVar id::ctxt)
+ | LocalDef (Name id, v, t) ->
+ let new_t = substl ctxt t in
+ let new_v = substl ctxt v in
+ observe (str "for variable " ++ Ppconstr.pr_id id ++ fnl () ++
+ str "old type := " ++ Printer.pr_lconstr_env env sigma t ++ fnl () ++
+ str "new type := " ++ Printer.pr_lconstr_env env sigma new_t ++ fnl () ++
+ str "old value := " ++ Printer.pr_lconstr_env env sigma v ++ fnl () ++
+ str "new value := " ++ Printer.pr_lconstr_env env sigma new_v ++ fnl ()
+ );
+ let open Context.Named.Declaration in
+ (Environ.push_named (LocalDef (id,new_v,new_t)) env,mkVar id::ctxt)
+ )
(Environ.rel_context new_env)
~init:(env,[])
)
@@ -399,7 +411,7 @@ let add_pat_variables pat typ env : Environ.env =
-let rec pattern_to_term_and_type env typ = CAst.with_val (function
+let rec pattern_to_term_and_type env typ = DAst.with_val (function
| PatVar Anonymous -> assert false
| PatVar (Name id) ->
mkGVar id
@@ -422,7 +434,7 @@ let rec pattern_to_term_and_type env typ = CAst.with_val (function
Array.to_list
(Array.init
(cst_narg - List.length patternl)
- (fun i -> Detyping.detype false [] env (Evd.from_env env) (EConstr.of_constr csta.(i)))
+ (fun i -> Detyping.detype Detyping.Now false Id.Set.empty env (Evd.from_env env) (EConstr.of_constr csta.(i)))
)
in
let patl_as_term =
@@ -466,9 +478,9 @@ let rec pattern_to_term_and_type env typ = CAst.with_val (function
let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
- observe (str " Entering : " ++ Printer.pr_glob_constr rt);
+ observe (str " Entering : " ++ Printer.pr_glob_constr_env env rt);
let open CAst in
- match rt.v with
+ match DAst.get rt with
| GRef _ | GVar _ | GEvar _ | GPatVar _ | GSort _ | GHole _ ->
(* do nothing (except changing type of course) *)
mk_result [] rt avoid
@@ -484,13 +496,13 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
(mk_result [] [] avoid)
in
begin
- match f.v with
+ match DAst.get f with
| GLambda _ ->
let rec aux t l =
match l with
| [] -> t
- | u::l -> CAst.make @@
- match t.v with
+ | u::l -> DAst.make @@
+ match DAst.get t with
| GLambda(na,_,nat,b) ->
GLetIn(na,u,None,aux b l)
| _ ->
@@ -506,8 +518,8 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
The "value" of this branch is then simply [res]
*)
let rt_as_constr,ctx = Pretyping.understand env (Evd.from_env env) rt in
- let rt_typ = Typing.unsafe_type_of env (Evd.from_env env) (EConstr.of_constr rt_as_constr) in
- let res_raw_type = Detyping.detype false [] env (Evd.from_env env) rt_typ in
+ let rt_typ = Typing.unsafe_type_of env (Evd.from_env env) rt_as_constr in
+ let res_raw_type = Detyping.detype Detyping.Now false Id.Set.empty env (Evd.from_env env) rt_typ in
let res = fresh_id args_res.to_avoid "_res" in
let new_avoid = res::args_res.to_avoid in
let res_rt = mkGVar res in
@@ -547,12 +559,12 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
match n with
| Name id when List.exists (is_free_in id) args ->
(* need to alpha-convert the name *)
- let new_id = Namegen.next_ident_away id avoid in
+ let new_id = Namegen.next_ident_away id (Id.Set.of_list avoid) in
let new_avoid = id:: avoid in
let new_b =
replace_var_by_term
id
- (CAst.make @@ GVar id)
+ (DAst.make @@ GVar id)
b
in
(Name new_id,new_b,new_avoid)
@@ -578,6 +590,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
*)
build_entry_lc env funnames avoid (mkGApp(b,args))
| GRec _ -> user_err Pp.(str "Not handled GRec")
+ | GProj _ -> user_err Pp.(str "Funind does not support primitive projections")
| GProd _ -> user_err Pp.(str "Cannot apply a type")
end (* end of the application treatement *)
@@ -605,22 +618,23 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
let t_res = build_entry_lc env funnames avoid t in
let new_env = raw_push_named (n,None,t) env in
let b_res = build_entry_lc new_env funnames avoid b in
- combine_results (combine_prod n) t_res b_res
+ if List.length t_res.result = 1 && List.length b_res.result = 1
+ then combine_results (combine_prod2 n) t_res b_res
+ else combine_results (combine_prod n) t_res b_res
| GLetIn(n,v,typ,b) ->
(* we first compute the list of constructor
corresponding to the body of the function,
then the one corresponding to the value [t]
and combine the two result
*)
- let v = match typ with None -> v | Some t -> CAst.make ?loc:rt.loc @@ GCast (v,CastConv t) in
+ let v = match typ with None -> v | Some t -> DAst.make ?loc:rt.loc @@ GCast (v,CastConv t) in
let v_res = build_entry_lc env funnames avoid v in
let v_as_constr,ctx = Pretyping.understand env (Evd.from_env env) v in
- let v_type = Typing.unsafe_type_of env (Evd.from_env env) (EConstr.of_constr v_as_constr) in
- let v_type = EConstr.Unsafe.to_constr v_type in
+ let v_type = Typing.unsafe_type_of env (Evd.from_env env) v_as_constr in
let new_env =
match n with
Anonymous -> env
- | Name id -> Environ.push_named (NamedDecl.LocalDef (id,v_as_constr,v_type)) env
+ | Name id -> EConstr.push_named (NamedDecl.LocalDef (id,v_as_constr,v_type)) env
in
let b_res = build_entry_lc new_env funnames avoid b in
combine_results (combine_letin n) v_res b_res
@@ -632,19 +646,19 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
build_entry_lc_from_case env funnames make_discr el brl avoid
| GIf(b,(na,e_option),lhs,rhs) ->
let b_as_constr,ctx = Pretyping.understand env (Evd.from_env env) b in
- let b_typ = Typing.unsafe_type_of env (Evd.from_env env) (EConstr.of_constr b_as_constr) in
+ let b_typ = Typing.unsafe_type_of env (Evd.from_env env) b_as_constr in
let (ind,_) =
try Inductiveops.find_inductive env (Evd.from_env env) b_typ
with Not_found ->
user_err (str "Cannot find the inductive associated to " ++
- Printer.pr_glob_constr b ++ str " in " ++
- Printer.pr_glob_constr rt ++ str ". try again with a cast")
+ Printer.pr_glob_constr_env env b ++ str " in " ++
+ Printer.pr_glob_constr_env env rt ++ str ". try again with a cast")
in
let case_pats = build_constructors_of_type (fst ind) [] in
assert (Int.equal (Array.length case_pats) 2);
let brl =
List.map_i
- (fun i x -> Loc.tag ([],[case_pats.(i)],x))
+ (fun i x -> CAst.make ([],[case_pats.(i)],x))
0
[lhs;rhs]
in
@@ -664,17 +678,17 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
nal
in
let b_as_constr,ctx = Pretyping.understand env (Evd.from_env env) b in
- let b_typ = Typing.unsafe_type_of env (Evd.from_env env) (EConstr.of_constr b_as_constr) in
+ let b_typ = Typing.unsafe_type_of env (Evd.from_env env) b_as_constr in
let (ind,_) =
try Inductiveops.find_inductive env (Evd.from_env env) b_typ
with Not_found ->
user_err (str "Cannot find the inductive associated to " ++
- Printer.pr_glob_constr b ++ str " in " ++
- Printer.pr_glob_constr rt ++ str ". try again with a cast")
+ Printer.pr_glob_constr_env env b ++ str " in " ++
+ Printer.pr_glob_constr_env env rt ++ str ". try again with a cast")
in
let case_pats = build_constructors_of_type (fst ind) nal_as_glob_constr in
assert (Int.equal (Array.length case_pats) 1);
- let br = Loc.tag ([],[case_pats.(0)],e) in
+ let br = CAst.make ([],[case_pats.(0)],e) in
let match_expr = mkGCases(None,[b,(Anonymous,None)],[br]) in
build_entry_lc env funnames avoid match_expr
@@ -682,6 +696,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
| GRec _ -> user_err Pp.(str "Not handled GRec")
| GCast(b,_) ->
build_entry_lc env funnames avoid b
+ | GProj(_,_) -> user_err Pp.(str "Funind does not support primitive projections")
and build_entry_lc_from_case env funname make_discr
(el:tomatch_tuples)
(brl:Glob_term.cases_clauses) avoid :
@@ -709,7 +724,7 @@ and build_entry_lc_from_case env funname make_discr
let types =
List.map (fun (case_arg,_) ->
let case_arg_as_constr,ctx = Pretyping.understand env (Evd.from_env env) case_arg in
- EConstr.Unsafe.to_constr (Typing.unsafe_type_of env (Evd.from_env env) (EConstr.of_constr case_arg_as_constr))
+ EConstr.Unsafe.to_constr (Typing.unsafe_type_of env (Evd.from_env env) case_arg_as_constr)
) el
in
(****** The next works only if the match is not dependent ****)
@@ -740,7 +755,7 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve
| [] -> (* computed_branches *) {result = [];to_avoid = avoid}
| br::brl' ->
(* alpha conversion to prevent name clashes *)
- let _,(idl,patl,return) = alpha_br avoid br in
+ let {CAst.v=(idl,patl,return)} = alpha_br avoid br in
let new_avoid = idl@avoid in (* for now we can no more use idl as an identifier *)
(* building a list of precondition stating that we are not in this branch
(will be used in the following recursive calls)
@@ -759,7 +774,7 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve
Typing.unsafe_type_of env_with_pat_ids (Evd.from_env env) (EConstr.mkVar id)
in
let raw_typ_of_id =
- Detyping.detype false []
+ Detyping.detype Detyping.Now false Id.Set.empty
env_with_pat_ids (Evd.from_env env) typ_of_id
in
mkGProd (Name id,raw_typ_of_id,acc))
@@ -805,15 +820,21 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve
(fun pat e typ_as_constr ->
let this_pat_ids = ids_of_pat pat in
let typ_as_constr = EConstr.of_constr typ_as_constr in
- let typ = Detyping.detype false [] new_env (Evd.from_env env) typ_as_constr in
+ let typ = Detyping.detype Detyping.Now false Id.Set.empty new_env (Evd.from_env env) typ_as_constr in
let pat_as_term = pattern_to_term pat in
+ (* removing trivial holes *)
+ let pat_as_term = solve_trivial_holes pat_as_term e in
+ (* observe (str "those_pattern_preconds" ++ spc () ++ *)
+ (* str "pat" ++ spc () ++ pr_glob_constr pat_as_term ++ spc ()++ *)
+ (* str "e" ++ spc () ++ pr_glob_constr e ++spc ()++ *)
+ (* str "typ_as_constr" ++ spc () ++ pr_lconstr typ_as_constr); *)
List.fold_right
(fun id acc ->
if Id.Set.mem id this_pat_ids
then (Prod (Name id),
let typ_of_id = Typing.unsafe_type_of new_env (Evd.from_env env) (EConstr.mkVar id) in
let raw_typ_of_id =
- Detyping.detype false [] new_env (Evd.from_env env) typ_of_id
+ Detyping.detype Detyping.Now false Id.Set.empty new_env (Evd.from_env env) typ_of_id
in
raw_typ_of_id
)::acc
@@ -855,37 +876,45 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve
{ brl'_res with result = this_branch_res@brl'_res.result }
-let is_res id =
- try
+let is_res r = match DAst.get r with
+| GVar id ->
+ begin try
String.equal (String.sub (Id.to_string id) 0 4) "_res"
- with Invalid_argument _ -> false
+ with Invalid_argument _ -> false end
+| _ -> false
+let is_gr c gr = match DAst.get c with
+| GRef (r, _) -> GlobRef.equal r gr
+| _ -> false
+let is_gvar c = match DAst.get c with
+| GVar id -> true
+| _ -> false
let same_raw_term rt1 rt2 =
- match CAst.(rt1.v, rt2.v) with
- | GRef(r1,_), GRef (r2,_) -> Globnames.eq_gr r1 r2
+ match DAst.get rt1, DAst.get rt2 with
+ | GRef(r1,_), GRef (r2,_) -> GlobRef.equal r1 r2
| GHole _, GHole _ -> true
| _ -> false
let decompose_raw_eq lhs rhs =
- let rec decompose_raw_eq lhs rhs acc =
- observe (str "decomposing eq for " ++ pr_glob_constr lhs ++ str " " ++ pr_glob_constr rhs);
- let (rhd,lrhs) = glob_decompose_app rhs in
- let (lhd,llhs) = glob_decompose_app lhs in
- observe (str "lhd := " ++ pr_glob_constr lhd);
- observe (str "rhd := " ++ pr_glob_constr rhd);
+ let _, env = Pfedit.get_current_context () in
+ let rec decompose_raw_eq lhs rhs acc =
+ observe (str "decomposing eq for " ++ pr_glob_constr_env env lhs ++ str " " ++ pr_glob_constr_env env rhs);
+ let (rhd,lrhs) = glob_decompose_app rhs in
+ let (lhd,llhs) = glob_decompose_app lhs in
+ observe (str "lhd := " ++ pr_glob_constr_env env lhd);
+ observe (str "rhd := " ++ pr_glob_constr_env env rhd);
observe (str "llhs := " ++ int (List.length llhs));
observe (str "lrhs := " ++ int (List.length lrhs));
- let sllhs = List.length llhs in
- let slrhs = List.length lrhs in
- if same_raw_term lhd rhd && Int.equal sllhs slrhs
+ let sllhs = List.length llhs in
+ let slrhs = List.length lrhs in
+ if same_raw_term lhd rhd && Int.equal sllhs slrhs
then
(* let _ = assert false in *)
List.fold_right2 decompose_raw_eq llhs lrhs acc
else (lhs,rhs)::acc
in
decompose_raw_eq lhs rhs []
-
exception Continue
(*
@@ -894,29 +923,30 @@ exception Continue
eliminates some meaningless equalities, applies some rewrites......
*)
let rec rebuild_cons env nb_args relname args crossed_types depth rt =
- observe (str "rebuilding : " ++ pr_glob_constr rt);
+ observe (str "rebuilding : " ++ pr_glob_constr_env env rt);
let open Context.Rel.Declaration in
let open CAst in
- match rt.v with
+ match DAst.get rt with
| GProd(n,k,t,b) ->
let not_free_in_t id = not (is_free_in id t) in
let new_crossed_types = t::crossed_types in
begin
- match t with
- | { v = GApp(({ v = GVar res_id } as res_rt),args') } when is_res res_id ->
+ match DAst.get t with
+ | GApp(res_rt ,args') when is_res res_rt ->
begin
- match args' with
- | { v = GVar this_relname }::args' ->
+ let arg = List.hd args' in
+ match DAst.get arg with
+ | GVar this_relname ->
(*i The next call to mk_rel_id is
valid since we are constructing the graph
Ensures by: obvious
i*)
let new_t =
- mkGApp(mkGVar(mk_rel_id this_relname),args'@[res_rt])
+ mkGApp(mkGVar(mk_rel_id this_relname),List.tl args'@[res_rt])
in
let t',ctx = Pretyping.understand env (Evd.from_env env) new_t in
- let new_env = Environ.push_rel (LocalAssum (n,t')) env in
+ let new_env = EConstr.push_rel (LocalAssum (n,t')) env in
let new_b,id_to_exclude =
rebuild_cons new_env
nb_args relname
@@ -928,12 +958,16 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
| _ -> (* the first args is the name of the function! *)
assert false
end
- | { loc = loc1; v = GApp({ loc = loc2; v = GRef(eq_as_ref,_) },[ty; { loc = loc3; v = GVar id};rt]) }
- when Globnames.eq_gr eq_as_ref (Lazy.force Coqlib.coq_eq_ref) && n == Anonymous
+ | GApp(eq_as_ref,[ty; id ;rt])
+ when is_gvar id && is_gr eq_as_ref (Lazy.force Coqlib.coq_eq_ref) && n == Anonymous
->
+ let loc1 = rt.CAst.loc in
+ let loc2 = eq_as_ref.CAst.loc in
+ let loc3 = id.CAst.loc in
+ let id = match DAst.get id with GVar id -> id | _ -> assert false in
begin
try
- observe (str "computing new type for eq : " ++ pr_glob_constr rt);
+ observe (str "computing new type for eq : " ++ pr_glob_constr_env env rt);
let t' =
try fst (Pretyping.understand env (Evd.from_env env) t)(*FIXME*)
with e when CErrors.noncritical e -> raise Continue
@@ -947,7 +981,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
let subst_b =
if is_in_b then b else replace_var_by_term id rt b
in
- let new_env = Environ.push_rel (LocalAssum (n,t')) env in
+ let new_env = EConstr.push_rel (LocalAssum (n,t')) env in
let new_b,id_to_exclude =
rebuild_cons
new_env
@@ -959,16 +993,16 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
with Continue ->
let jmeq = Globnames.IndRef (fst (EConstr.destInd Evd.empty (jmeq ()))) in
let ty',ctx = Pretyping.understand env (Evd.from_env env) ty in
- let ind,args' = Inductive.find_inductive env ty' in
+ let ind,args' = Inductiveops.find_inductive env Evd.(from_env env) ty' in
let mib,_ = Global.lookup_inductive (fst ind) in
let nparam = mib.Declarations.mind_nparams in
let params,arg' =
((Util.List.chop nparam args'))
in
- let rt_typ = CAst.make @@
- GApp(CAst.make @@ GRef (Globnames.IndRef (fst ind),None),
+ let rt_typ = DAst.make @@
+ GApp(DAst.make @@ GRef (Globnames.IndRef (fst ind),None),
(List.map
- (fun p -> Detyping.detype false []
+ (fun p -> Detyping.detype Detyping.Now false Id.Set.empty
env (Evd.from_env env)
(EConstr.of_constr p)) params)@(Array.to_list
(Array.make
@@ -976,31 +1010,31 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
(mkGHole ()))))
in
let eq' =
- CAst.make ?loc:loc1 @@ GApp(CAst.make ?loc:loc2 @@GRef(jmeq,None),[ty;CAst.make ?loc:loc3 @@ GVar id;rt_typ;rt])
+ DAst.make ?loc:loc1 @@ GApp(DAst.make ?loc:loc2 @@GRef(jmeq,None),[ty;DAst.make ?loc:loc3 @@ GVar id;rt_typ;rt])
in
- observe (str "computing new type for jmeq : " ++ pr_glob_constr eq');
+ observe (str "computing new type for jmeq : " ++ pr_glob_constr_env env eq');
let eq'_as_constr,ctx = Pretyping.understand env (Evd.from_env env) eq' in
observe (str " computing new type for jmeq : done") ;
+ let sigma = Evd.(from_env env) in
let new_args =
- match kind_of_term eq'_as_constr with
+ match EConstr.kind sigma eq'_as_constr with
| App(_,[|_;_;ty;_|]) ->
- let ty = Array.to_list (snd (destApp ty)) in
+ let ty = Array.to_list (snd (EConstr.destApp sigma ty)) in
let ty' = snd (Util.List.chop nparam ty) in
List.fold_left2
(fun acc var_as_constr arg ->
- let arg = EConstr.of_constr arg in
if isRel var_as_constr
then
let na = RelDecl.get_name (Environ.lookup_rel (destRel var_as_constr) env) in
match na with
| Anonymous -> acc
| Name id' ->
- (id',Detyping.detype false []
+ (id',Detyping.detype Detyping.Now false Id.Set.empty
env
(Evd.from_env env)
arg)::acc
else if isVar var_as_constr
- then (destVar var_as_constr,Detyping.detype false []
+ then (destVar var_as_constr,Detyping.detype Detyping.Now false Id.Set.empty
env
(Evd.from_env env)
arg)::acc
@@ -1029,7 +1063,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
in
let new_env =
let t',ctx = Pretyping.understand env (Evd.from_env env) eq' in
- Environ.push_rel (LocalAssum (n,t')) env
+ EConstr.push_rel (LocalAssum (n,t')) env
in
let new_b,id_to_exclude =
rebuild_cons
@@ -1045,8 +1079,8 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
mkGProd(n,t,new_b),id_to_exclude
else new_b, Id.Set.add id id_to_exclude
*)
- | { loc = loc1; v = GApp({ loc = loc2; v = GRef(eq_as_ref,_) },[ty;rt1;rt2]) }
- when Globnames.eq_gr eq_as_ref (Lazy.force Coqlib.coq_eq_ref) && n == Anonymous
+ | GApp(eq_as_ref,[ty;rt1;rt2])
+ when is_gr eq_as_ref (Lazy.force Coqlib.coq_eq_ref) && n == Anonymous
->
begin
try
@@ -1057,7 +1091,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
List.fold_left
(fun acc (lhs,rhs) ->
mkGProd(Anonymous,
- mkGApp(mkGRef(eq_as_ref),[mkGHole ();lhs;rhs]),acc)
+ mkGApp(mkGRef(Lazy.force Coqlib.coq_eq_ref),[mkGHole ();lhs;rhs]),acc)
)
b
l
@@ -1065,9 +1099,9 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
rebuild_cons env nb_args relname args crossed_types depth new_rt
else raise Continue
with Continue ->
- observe (str "computing new type for prod : " ++ pr_glob_constr rt);
+ observe (str "computing new type for prod : " ++ pr_glob_constr_env env rt);
let t',ctx = Pretyping.understand env (Evd.from_env env) t in
- let new_env = Environ.push_rel (LocalAssum (n,t')) env in
+ let new_env = EConstr.push_rel (LocalAssum (n,t')) env in
let new_b,id_to_exclude =
rebuild_cons new_env
nb_args relname
@@ -1081,9 +1115,9 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
| _ -> mkGProd(n,t,new_b),Id.Set.filter not_free_in_t id_to_exclude
end
| _ ->
- observe (str "computing new type for prod : " ++ pr_glob_constr rt);
+ observe (str "computing new type for prod : " ++ pr_glob_constr_env env rt);
let t',ctx = Pretyping.understand env (Evd.from_env env) t in
- let new_env = Environ.push_rel (LocalAssum (n,t')) env in
+ let new_env = EConstr.push_rel (LocalAssum (n,t')) env in
let new_b,id_to_exclude =
rebuild_cons new_env
nb_args relname
@@ -1100,11 +1134,11 @@ let rec rebuild_cons env 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_glob_constr rt);
+ observe (str "computing new type for lambda : " ++ pr_glob_constr_env env rt);
let t',ctx = Pretyping.understand env (Evd.from_env env) t in
match n with
| Name id ->
- let new_env = Environ.push_rel (LocalAssum (n,t')) env in
+ let new_env = EConstr.push_rel (LocalAssum (n,t')) env in
let new_b,id_to_exclude =
rebuild_cons new_env
nb_args relname
@@ -1115,19 +1149,20 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
then
new_b, Id.Set.remove id (Id.Set.filter not_free_in_t id_to_exclude)
else
- CAst.make @@ GProd(n,k,t,new_b),Id.Set.filter not_free_in_t id_to_exclude
+ DAst.make @@ GProd(n,k,t,new_b),Id.Set.filter not_free_in_t id_to_exclude
| _ -> anomaly (Pp.str "Should not have an anonymous function here.")
(* We have renamed all the anonymous functions during alpha_renaming phase *)
end
| GLetIn(n,v,t,b) ->
begin
- let t = match t with None -> v | Some t -> CAst.make ?loc:rt.loc @@ GCast (v,CastConv t) in
+ let t = match t with None -> v | Some t -> DAst.make ?loc:rt.loc @@ GCast (v,CastConv t) in
let not_free_in_t id = not (is_free_in id t) in
let evd = (Evd.from_env env) in
let t',ctx = Pretyping.understand env evd t in
let evd = Evd.from_ctx ctx in
- let type_t' = Typing.unsafe_type_of env evd (EConstr.of_constr t') in
+ let type_t' = Typing.unsafe_type_of env evd t' in
+ let t' = EConstr.Unsafe.to_constr t' in
let type_t' = EConstr.Unsafe.to_constr type_t' in
let new_env = Environ.push_rel (LocalDef (n,t',type_t')) env in
let new_b,id_to_exclude =
@@ -1138,7 +1173,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
match n with
| Name id when Id.Set.mem id id_to_exclude && depth >= nb_args ->
new_b,Id.Set.remove id (Id.Set.filter not_free_in_t id_to_exclude)
- | _ -> CAst.make @@ GLetIn(n,t,None,new_b), (* HOPING IT WOULD WORK *)
+ | _ -> DAst.make @@ GLetIn(n,t,None,new_b), (* HOPING IT WOULD WORK *)
Id.Set.filter not_free_in_t id_to_exclude
end
| GLetTuple(nal,(na,rto),t,b) ->
@@ -1153,7 +1188,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
depth t
in
let t',ctx = Pretyping.understand env (Evd.from_env env) new_t in
- let new_env = Environ.push_rel (LocalAssum (na,t')) env in
+ let new_env = EConstr.push_rel (LocalAssum (na,t')) env in
let new_b,id_to_exclude =
rebuild_cons new_env
nb_args relname
@@ -1164,7 +1199,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
(* | Name id when Id.Set.mem id id_to_exclude -> *)
(* new_b,Id.Set.remove id (Id.Set.filter not_free_in_t id_to_exclude) *)
(* | _ -> *)
- CAst.make @@ GLetTuple(nal,(na,None),t,new_b),
+ DAst.make @@ GLetTuple(nal,(na,None),t,new_b),
Id.Set.filter not_free_in_t (Id.Set.union id_to_exclude id_to_exclude')
end
@@ -1190,12 +1225,15 @@ let rebuild_cons env nb_args relname args crossed_types rt =
TODO: Find a valid way to deal with implicit arguments here!
*)
-let rec compute_cst_params relnames params gt = CAst.with_val (function
+let rec compute_cst_params relnames params gt = DAst.with_val (function
| GRef _ | GVar _ | GEvar _ | GPatVar _ -> params
- | GApp({ CAst.v = GVar relname' },rtl) when Id.Set.mem relname' relnames ->
- compute_cst_params_from_app [] (params,rtl)
| GApp(f,args) ->
+ begin match DAst.get f with
+ | GVar relname' when Id.Set.mem relname' relnames ->
+ compute_cst_params_from_app [] (params,args)
+ | _ ->
List.fold_left (compute_cst_params relnames) params (f::args)
+ end
| GLambda(_,_,t,b) | GProd(_,_,t,b) | GLetTuple(_,_,t,b) ->
let t_params = compute_cst_params relnames params t in
compute_cst_params relnames t_params b
@@ -1208,14 +1246,14 @@ let rec compute_cst_params relnames params gt = CAst.with_val (function
discrimination ones *)
| GSort _ -> params
| GHole _ -> params
- | GIf _ | GRec _ | GCast _ ->
+ | GIf _ | GRec _ | GCast _ | GProj _ ->
raise (UserError(Some "compute_cst_params", str "Not handled case"))
) gt
and compute_cst_params_from_app acc (params,rtl) =
+ let is_gid id c = match DAst.get c with GVar id' -> Id.equal id id' | _ -> false in
match params,rtl with
| _::_,[] -> assert false (* the rel has at least nargs + 1 arguments ! *)
- | ((Name id,_,None) as param)::params', { CAst.v = GVar id' }::rtl'
- when Id.compare id id' == 0 ->
+ | ((Name id,_,None) as param)::params', c::rtl' when is_gid id c ->
compute_cst_params_from_app (param::acc) (params',rtl')
| _ -> List.rev acc
@@ -1256,12 +1294,12 @@ let rec rebuild_return_type rt =
CAst.make ?loc @@ Constrexpr.CProdN(n,rebuild_return_type t')
| Constrexpr.CLetIn(na,v,t,t') ->
CAst.make ?loc @@ Constrexpr.CLetIn(na,v,t,rebuild_return_type t')
- | _ -> CAst.make ?loc @@ Constrexpr.CProdN([[Loc.tag Anonymous],
- Constrexpr.Default Decl_kinds.Explicit, rt],
+ | _ -> CAst.make ?loc @@ Constrexpr.CProdN([Constrexpr.CLocalAssum ([CAst.make Anonymous],
+ Constrexpr.Default Decl_kinds.Explicit, rt)],
CAst.make @@ Constrexpr.CSort(GType []))
let do_build_inductive
- evd (funconstants: Term.pconstant list) (funsargs: (Name.t * glob_constr * glob_constr option) list list)
+ evd (funconstants: pconstant list) (funsargs: (Name.t * glob_constr * glob_constr option) list list)
returned_types
(rtl:glob_constr list) =
let _time1 = System.get_time () in
@@ -1312,12 +1350,12 @@ let do_build_inductive
(fun (n,t,typ) acc ->
match typ with
| Some typ ->
- CAst.make @@ Constrexpr.CLetIn((Loc.tag n),with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t,
+ CAst.make @@ Constrexpr.CLetIn((CAst.make n),with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t,
Some (with_full_print (Constrextern.extern_glob_constr Id.Set.empty) typ),
acc)
| None ->
CAst.make @@ Constrexpr.CProdN
- ([[(Loc.tag n)],Constrexpr_ops.default_binder_kind,with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t],
+ ([Constrexpr.CLocalAssum([CAst.make n],Constrexpr_ops.default_binder_kind,with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t)],
acc
)
)
@@ -1330,8 +1368,9 @@ let do_build_inductive
*)
let rel_arities = Array.mapi rel_arity funsargs in
Util.Array.fold_left2 (fun env rel_name rel_ar ->
- Environ.push_named (LocalAssum (rel_name,
- fst (with_full_print (Constrintern.interp_constr env evd) rel_ar))) env) env relnames rel_arities
+ let rex = fst (with_full_print (Constrintern.interp_constr env evd) rel_ar) in
+ let rex = EConstr.Unsafe.to_constr rex in
+ Environ.push_named (LocalAssum (rel_name,rex)) env) env relnames rel_arities
in
(* and of the real constructors*)
let constr i res =
@@ -1379,12 +1418,12 @@ let do_build_inductive
(fun (n,t,typ) acc ->
match typ with
| Some typ ->
- CAst.make @@ Constrexpr.CLetIn((Loc.tag n),with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t,
+ CAst.make @@ Constrexpr.CLetIn((CAst.make n),with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t,
Some (with_full_print (Constrextern.extern_glob_constr Id.Set.empty) typ),
acc)
| None ->
CAst.make @@ Constrexpr.CProdN
- ([[(Loc.tag n)],Constrexpr_ops.default_binder_kind,with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t],
+ ([Constrexpr.CLocalAssum([CAst.make n],Constrexpr_ops.default_binder_kind,with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t)],
acc
)
)
@@ -1411,18 +1450,18 @@ let do_build_inductive
(fun (n,t,typ) ->
match typ with
| Some typ ->
- Constrexpr.CLocalDef((Loc.tag n), Constrextern.extern_glob_constr Id.Set.empty t,
+ Constrexpr.CLocalDef((CAst.make n), Constrextern.extern_glob_constr Id.Set.empty t,
Some (with_full_print (Constrextern.extern_glob_constr Id.Set.empty) typ))
| None ->
Constrexpr.CLocalAssum
- ([(Loc.tag n)], Constrexpr_ops.default_binder_kind, Constrextern.extern_glob_constr Id.Set.empty t)
+ ([(CAst.make n)], Constrexpr_ops.default_binder_kind, Constrextern.extern_glob_constr Id.Set.empty t)
)
rels_params
in
let ext_rels_constructors =
Array.map (List.map
(fun (id,t) ->
- false,((Loc.tag id),
+ false,((CAst.make id),
with_full_print
(Constrextern.extern_glob_type Id.Set.empty) ((* zeta_normalize *) (alpha_rt rel_params_ids t))
)
@@ -1430,7 +1469,7 @@ let do_build_inductive
(rel_constructors)
in
let rel_ind i ext_rel_constructors =
- (((Loc.tag @@ relnames.(i)), None),
+ (((CAst.make @@ relnames.(i)), None),
rel_params,
Some rel_arities.(i),
ext_rel_constructors),[]
@@ -1460,8 +1499,8 @@ let do_build_inductive
let _time2 = System.get_time () in
try
with_full_print
- (Flags.silently (Command.do_mutual_inductive rel_inds (Flags.is_universe_polymorphism ()) false false))
- Decl_kinds.Finite
+ (Flags.silently (ComInductive.do_mutual_inductive rel_inds (Flags.is_universe_polymorphism ()) false false ~uniform:ComInductive.NonUniformParameters))
+ Declarations.Finite
with
| UserError(s,msg) as e ->
let _time3 = System.get_time () in
@@ -1472,7 +1511,7 @@ let do_build_inductive
in
let msg =
str "while trying to define"++ spc () ++
- Ppvernac.pr_vernac (Vernacexpr.VernacInductive(false,false,Decl_kinds.Finite,repacked_rel_inds))
+ Ppvernac.pr_vernac Vernacexpr.(VernacExpr([], VernacInductive(None,false,Declarations.Finite,repacked_rel_inds)))
++ fnl () ++
msg
in
@@ -1487,7 +1526,7 @@ let do_build_inductive
in
let msg =
str "while trying to define"++ spc () ++
- Ppvernac.pr_vernac (Vernacexpr.VernacInductive(false,false,Decl_kinds.Finite,repacked_rel_inds))
+ Ppvernac.pr_vernac Vernacexpr.(VernacExpr([], VernacInductive(None,false,Declarations.Finite,repacked_rel_inds)))
++ fnl () ++
CErrors.print reraise
in
diff --git a/plugins/funind/glob_term_to_relation.mli b/plugins/funind/glob_term_to_relation.mli
index 7ad7de0792..ff0e98d00f 100644
--- a/plugins/funind/glob_term_to_relation.mli
+++ b/plugins/funind/glob_term_to_relation.mli
@@ -1,4 +1,3 @@
-open API
open Names
(*
@@ -12,7 +11,7 @@ val build_inductive :
Id.t list -> (* The list of function name *)
*)
Evd.evar_map ->
- Term.pconstant list ->
+ Constr.pconstant list ->
(Name.t*Glob_term.glob_constr*Glob_term.glob_constr option) list list -> (* The list of function args *)
Constrexpr.constr_expr list -> (* The list of function returned type *)
Glob_term.glob_constr list -> (* the list of body *)
diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml
index 726a8203d7..954fc3bab4 100644
--- a/plugins/funind/glob_termops.ml
+++ b/plugins/funind/glob_termops.ml
@@ -1,93 +1,35 @@
-open API
open Pp
+open Constr
open Glob_term
open CErrors
open Util
open Names
open Decl_kinds
-open Misctypes
(*
Some basic functions to rebuild glob_constr
In each of them the location is Loc.ghost
*)
-let mkGRef ref = CAst.make @@ GRef(ref,None)
-let mkGVar id = CAst.make @@ GVar(id)
-let mkGApp(rt,rtl) = CAst.make @@ GApp(rt,rtl)
-let mkGLambda(n,t,b) = CAst.make @@ GLambda(n,Explicit,t,b)
-let mkGProd(n,t,b) = CAst.make @@ GProd(n,Explicit,t,b)
-let mkGLetIn(n,b,t,c) = CAst.make @@ GLetIn(n,b,t,c)
-let mkGCases(rto,l,brl) = CAst.make @@ GCases(Term.RegularStyle,rto,l,brl)
-let mkGSort s = CAst.make @@ GSort(s)
-let mkGHole () = CAst.make @@ GHole(Evar_kinds.BinderType Anonymous,Misctypes.IntroAnonymous,None)
-let mkGCast(b,t) = CAst.make @@ GCast(b,CastConv t)
+let mkGRef ref = DAst.make @@ GRef(ref,None)
+let mkGVar id = DAst.make @@ GVar(id)
+let mkGApp(rt,rtl) = DAst.make @@ GApp(rt,rtl)
+let mkGLambda(n,t,b) = DAst.make @@ GLambda(n,Explicit,t,b)
+let mkGProd(n,t,b) = DAst.make @@ GProd(n,Explicit,t,b)
+let mkGLetIn(n,b,t,c) = DAst.make @@ GLetIn(n,b,t,c)
+let mkGCases(rto,l,brl) = DAst.make @@ GCases(RegularStyle,rto,l,brl)
+let mkGHole () = DAst.make @@ GHole(Evar_kinds.BinderType Anonymous,Namegen.IntroAnonymous,None)
(*
Some basic functions to decompose glob_constrs
These are analogous to the ones constrs
*)
-let glob_decompose_prod =
- let rec glob_decompose_prod args = function
- | { CAst.v = GProd(n,k,t,b) } ->
- glob_decompose_prod ((n,t)::args) b
- | rt -> args,rt
- in
- glob_decompose_prod []
-
-let glob_decompose_prod_or_letin =
- let rec glob_decompose_prod args = function
- | { CAst.v = GProd(n,k,t,b) } ->
- glob_decompose_prod ((n,None,Some t)::args) b
- | { CAst.v = GLetIn(n,b,t,c) } ->
- glob_decompose_prod ((n,Some b,t)::args) c
- | rt -> args,rt
- in
- glob_decompose_prod []
-
-let glob_compose_prod =
- List.fold_left (fun b (n,t) -> mkGProd(n,t,b))
-
-let glob_compose_prod_or_letin =
- List.fold_left (
- fun concl decl ->
- match decl with
- | (n,None,Some t) -> mkGProd(n,t,concl)
- | (n,Some bdy,t) -> mkGLetIn(n,bdy,t,concl)
- | _ -> assert false)
-
-let glob_decompose_prod_n n =
- let rec glob_decompose_prod i args c =
- if i<=0 then args,c
- else
- match c with
- | { CAst.v = GProd(n,_,t,b) } ->
- glob_decompose_prod (i-1) ((n,t)::args) b
- | rt -> args,rt
- in
- glob_decompose_prod n []
-
-
-let glob_decompose_prod_or_letin_n n =
- let rec glob_decompose_prod i args c =
- if i<=0 then args,c
- else
- match c with
- | { CAst.v = GProd(n,_,t,b) } ->
- glob_decompose_prod (i-1) ((n,None,Some t)::args) b
- | { CAst.v = GLetIn(n,b,t,c) } ->
- glob_decompose_prod (i-1) ((n,Some b,t)::args) c
- | rt -> args,rt
- in
- glob_decompose_prod n []
-
-
let glob_decompose_app =
let rec decompose_rapp acc rt =
(* msgnl (str "glob_decompose_app on : "++ Printer.pr_glob_constr rt); *)
- match rt with
- | { CAst.v = GApp(rt,rtl) } ->
+ match DAst.get rt with
+ | GApp(rt,rtl) ->
decompose_rapp (List.fold_left (fun y x -> x::y) acc rtl) rt
- | rt -> rt,List.rev acc
+ | _ -> rt,List.rev acc
in
decompose_rapp []
@@ -102,18 +44,6 @@ let glob_make_eq ?(typ= mkGHole ()) t1 t2 =
let glob_make_neq t1 t2 =
mkGApp(mkGRef (Lazy.force Coqlib.coq_not_ref),[glob_make_eq t1 t2])
-(* [glob_make_or P1 P2] build the glob_constr corresponding to [P1 \/ P2] *)
-let glob_make_or t1 t2 = mkGApp (mkGRef(Lazy.force Coqlib.coq_or_ref),[t1;t2])
-
-(* [glob_make_or_list [P1;...;Pn]] build the glob_constr corresponding
- to [P1 \/ ( .... \/ Pn)]
-*)
-let rec glob_make_or_list = function
- | [] -> invalid_arg "mk_or"
- | [e] -> e
- | e::l -> glob_make_or e (glob_make_or_list l)
-
-
let remove_name_from_mapping mapping na =
match na with
| Anonymous -> mapping
@@ -121,7 +51,7 @@ let remove_name_from_mapping mapping na =
let change_vars =
let rec change_vars mapping rt =
- CAst.map_with_loc (fun ?loc -> function
+ DAst.map_with_loc (fun ?loc -> function
| GRef _ as x -> x
| GVar id ->
let new_id =
@@ -178,13 +108,14 @@ let change_vars =
| GHole _ as x -> x
| GCast(b,c) ->
GCast(change_vars mapping b,
- Miscops.map_cast_type (change_vars mapping) c)
+ Glob_ops.map_cast_type (change_vars mapping) c)
+ | GProj(p,c) -> GProj(p, change_vars mapping c)
) rt
- and change_vars_br mapping ((loc,(idl,patl,res)) as br) =
+ and change_vars_br mapping ({CAst.loc;v=(idl,patl,res)} as br) =
let new_mapping = List.fold_right Id.Map.remove idl mapping in
if Id.Map.is_empty new_mapping
then br
- else (loc,(idl,patl,change_vars new_mapping res))
+ else CAst.make ?loc (idl,patl,change_vars new_mapping res)
in
change_vars
@@ -192,22 +123,22 @@ let change_vars =
let rec alpha_pat excluded pat =
let loc = pat.CAst.loc in
- match pat.CAst.v with
+ match DAst.get pat with
| PatVar Anonymous ->
let new_id = Indfun_common.fresh_id excluded "_x" in
- (CAst.make ?loc @@ PatVar(Name new_id)),(new_id::excluded),Id.Map.empty
+ (DAst.make ?loc @@ PatVar(Name new_id)),(new_id::excluded),Id.Map.empty
| PatVar(Name id) ->
if Id.List.mem id excluded
then
- let new_id = Namegen.next_ident_away id excluded in
- (CAst.make ?loc @@ PatVar(Name new_id)),(new_id::excluded),
+ let new_id = Namegen.next_ident_away id (Id.Set.of_list excluded) in
+ (DAst.make ?loc @@ PatVar(Name new_id)),(new_id::excluded),
(Id.Map.add id new_id Id.Map.empty)
else pat, excluded,Id.Map.empty
| PatCstr(constr,patl,na) ->
let new_na,new_excluded,map =
match na with
| Name id when Id.List.mem id excluded ->
- let new_id = Namegen.next_ident_away id excluded in
+ let new_id = Namegen.next_ident_away id (Id.Set.of_list excluded) in
Name new_id,new_id::excluded, Id.Map.add id new_id Id.Map.empty
| _ -> na,excluded,Id.Map.empty
in
@@ -220,7 +151,7 @@ let rec alpha_pat excluded pat =
([],new_excluded,map)
patl
in
- (CAst.make ?loc @@ PatCstr(constr,List.rev new_patl,new_na)),new_excluded,new_map
+ (DAst.make ?loc @@ PatCstr(constr,List.rev new_patl,new_na)),new_excluded,new_map
let alpha_patl excluded patl =
let patl,new_excluded,map =
@@ -239,7 +170,7 @@ let alpha_patl excluded patl =
let raw_get_pattern_id pat acc =
let rec get_pattern_id pat =
- match pat.CAst.v with
+ match DAst.get pat with
| PatVar(Anonymous) -> assert false
| PatVar(Name id) ->
[id]
@@ -258,11 +189,11 @@ let get_pattern_id pat = raw_get_pattern_id pat []
let rec alpha_rt excluded rt =
let loc = rt.CAst.loc in
- let new_rt = CAst.make ?loc @@
- match rt.CAst.v with
+ let new_rt = DAst.make ?loc @@
+ match DAst.get rt with
| GRef _ | GVar _ | GEvar _ | GPatVar _ as rt -> rt
| GLambda(Anonymous,k,t,b) ->
- let new_id = Namegen.next_ident_away (Id.of_string "_x") excluded in
+ let new_id = Namegen.next_ident_away (Id.of_string "_x") (Id.Set.of_list excluded) in
let new_excluded = new_id :: excluded in
let new_t = alpha_rt new_excluded t in
let new_b = alpha_rt new_excluded b in
@@ -277,7 +208,7 @@ let rec alpha_rt excluded rt =
let new_c = alpha_rt excluded c in
GLetIn(Anonymous,new_b,new_t,new_c)
| GLambda(Name id,k,t,b) ->
- let new_id = Namegen.next_ident_away id excluded in
+ let new_id = Namegen.next_ident_away id (Id.Set.of_list excluded) in
let t,b =
if Id.equal new_id id
then t, b
@@ -290,7 +221,7 @@ let rec alpha_rt excluded rt =
let new_b = alpha_rt new_excluded b in
GLambda(Name new_id,k,new_t,new_b)
| GProd(Name id,k,t,b) ->
- let new_id = Namegen.next_ident_away id excluded in
+ let new_id = Namegen.next_ident_away id (Id.Set.of_list excluded) in
let new_excluded = new_id::excluded in
let t,b =
if Id.equal new_id id
@@ -303,7 +234,7 @@ let rec alpha_rt excluded rt =
let new_b = alpha_rt new_excluded b in
GProd(Name new_id,k,new_t,new_b)
| GLetIn(Name id,b,t,c) ->
- let new_id = Namegen.next_ident_away id excluded in
+ let new_id = Namegen.next_ident_away id (Id.Set.of_list excluded) in
let c =
if Id.equal new_id id then c
else change_vars (Id.Map.add id new_id Id.Map.empty) c
@@ -321,7 +252,7 @@ let rec alpha_rt excluded rt =
match na with
| Anonymous -> (na::nal,excluded,mapping)
| Name id ->
- let new_id = Namegen.next_ident_away id excluded in
+ let new_id = Namegen.next_ident_away id (Id.Set.of_list excluded) in
if Id.equal new_id id
then
na::nal,id::excluded,mapping
@@ -358,27 +289,28 @@ let rec alpha_rt excluded rt =
| GHole _ as rt -> rt
| GCast (b,c) ->
GCast(alpha_rt excluded b,
- Miscops.map_cast_type (alpha_rt excluded) c)
+ Glob_ops.map_cast_type (alpha_rt excluded) c)
| GApp(f,args) ->
GApp(alpha_rt excluded f,
List.map (alpha_rt excluded) args
)
+ | GProj(p,c) -> GProj(p, alpha_rt excluded c)
in
new_rt
-and alpha_br excluded (loc,(ids,patl,res)) =
+and alpha_br excluded {CAst.loc;v=(ids,patl,res)} =
let new_patl,new_excluded,mapping = alpha_patl excluded patl in
let new_ids = List.fold_right raw_get_pattern_id new_patl [] in
let new_excluded = new_ids@excluded in
let renamed_res = change_vars mapping res in
let new_res = alpha_rt new_excluded renamed_res in
- (loc,(new_ids,new_patl,new_res))
+ CAst.make ?loc (new_ids,new_patl,new_res)
(*
[is_free_in id rt] checks if [id] is a free variable in [rt]
*)
let is_free_in id =
- let rec is_free_in x = CAst.with_loc_val (fun ?loc -> function
+ let rec is_free_in x = DAst.with_loc_val (fun ?loc -> function
| GRef _ -> false
| GVar id' -> Id.compare id' id == 0
| GEvar _ -> false
@@ -414,15 +346,16 @@ let is_free_in id =
| GHole _ -> false
| GCast (b,(CastConv t|CastVM t|CastNative t)) -> is_free_in b || is_free_in t
| GCast (b,CastCoerce) -> is_free_in b
+ | GProj (_,c) -> is_free_in c
) x
- and is_free_in_br (_,(ids,_,rt)) =
+ and is_free_in_br {CAst.v=(ids,_,rt)} =
(not (Id.List.mem id ids)) && is_free_in rt
in
is_free_in
-let rec pattern_to_term pt = CAst.with_val (function
+let rec pattern_to_term pt = DAst.with_val (function
| PatVar Anonymous -> assert false
| PatVar(Name id) ->
mkGVar id
@@ -449,8 +382,8 @@ let rec pattern_to_term pt = CAst.with_val (function
let replace_var_by_term x_id term =
- let rec replace_var_by_pattern x = CAst.map (function
- | GVar id when Id.compare id x_id == 0 -> term.CAst.v
+ let rec replace_var_by_pattern x = DAst.map (function
+ | GVar id when Id.compare id x_id == 0 -> DAst.get term
| GRef _
| GVar _
| GEvar _
@@ -506,12 +439,14 @@ let replace_var_by_term x_id term =
| GHole _ as rt -> rt
| GCast(b,c) ->
GCast(replace_var_by_pattern b,
- Miscops.map_cast_type replace_var_by_pattern c)
+ Glob_ops.map_cast_type replace_var_by_pattern c)
+ | GProj(p,c) ->
+ GProj(p,replace_var_by_pattern c)
) x
- and replace_var_by_pattern_br ((loc,(idl,patl,res)) as br) =
+ and replace_var_by_pattern_br ({CAst.loc;v=(idl,patl,res)} as br) =
if List.exists (fun id -> Id.compare id x_id == 0) idl
then br
- else (loc,(idl,patl,replace_var_by_pattern res))
+ else CAst.make ?loc (idl,patl,replace_var_by_pattern res)
in
replace_var_by_pattern
@@ -523,11 +458,10 @@ exception NotUnifiable
let rec are_unifiable_aux = function
| [] -> ()
- | eq::eqs ->
- let open CAst in
- match eq with
- | { v = PatVar _ },_ | _, { v = PatVar _ } -> are_unifiable_aux eqs
- | { v = PatCstr(constructor1,cpl1,_) }, { v = PatCstr(constructor2,cpl2,_) } ->
+ | (l, r) ::eqs ->
+ match DAst.get l, DAst.get r with
+ | PatVar _ ,_ | _, PatVar _-> are_unifiable_aux eqs
+ | PatCstr(constructor1,cpl1,_), PatCstr(constructor2,cpl2,_) ->
if not (eq_constructor constructor2 constructor1)
then raise NotUnifiable
else
@@ -546,11 +480,10 @@ let are_unifiable pat1 pat2 =
let rec eq_cases_pattern_aux = function
| [] -> ()
- | eq::eqs ->
- let open CAst in
- match eq with
- | { v = PatVar _ }, { v = PatVar _ } -> eq_cases_pattern_aux eqs
- | { v = PatCstr(constructor1,cpl1,_) }, { v = PatCstr(constructor2,cpl2,_) } ->
+ | (l, r) ::eqs ->
+ match DAst.get l, DAst.get r with
+ | PatVar _, PatVar _ -> eq_cases_pattern_aux eqs
+ | PatCstr(constructor1,cpl1,_), PatCstr(constructor2,cpl2,_) ->
if not (eq_constructor constructor2 constructor1)
then raise NotUnifiable
else
@@ -570,7 +503,7 @@ let eq_cases_pattern pat1 pat2 =
let ids_of_pat =
- let rec ids_of_pat ids = CAst.with_val (function
+ let rec ids_of_pat ids = DAst.with_val (function
| PatVar Anonymous -> ids
| PatVar(Name id) -> Id.Set.add id ids
| PatCstr(_,patl,_) -> List.fold_left ids_of_pat ids patl
@@ -578,112 +511,21 @@ let ids_of_pat =
in
ids_of_pat Id.Set.empty
-let id_of_name = function
- | Anonymous -> Id.of_string "x"
- | Name x -> x
-
-(* TODO: finish Rec caes *)
-let ids_of_glob_constr c =
- let rec ids_of_glob_constr acc {loc; CAst.v = c} =
- let idof = id_of_name in
- match c with
- | GVar id -> id::acc
- | GApp (g,args) ->
- ids_of_glob_constr [] g @ List.flatten (List.map (ids_of_glob_constr []) args) @ acc
- | GLambda (na,k,ty,c) -> idof na :: ids_of_glob_constr [] ty @ ids_of_glob_constr [] c @ acc
- | GProd (na,k,ty,c) -> idof na :: ids_of_glob_constr [] ty @ ids_of_glob_constr [] c @ acc
- | GLetIn (na,b,t,c) -> idof na :: ids_of_glob_constr [] b @ Option.cata (ids_of_glob_constr []) [] t @ ids_of_glob_constr [] c @ acc
- | GCast (c,(CastConv t|CastVM t|CastNative t)) -> ids_of_glob_constr [] c @ ids_of_glob_constr [] t @ acc
- | GCast (c,CastCoerce) -> ids_of_glob_constr [] c @ acc
- | GIf (c,(na,po),b1,b2) -> ids_of_glob_constr [] c @ ids_of_glob_constr [] b1 @ ids_of_glob_constr [] b2 @ acc
- | GLetTuple (nal,(na,po),b,c) ->
- List.map idof nal @ ids_of_glob_constr [] b @ ids_of_glob_constr [] c @ acc
- | GCases (sty,rtntypopt,tml,brchl) ->
- List.flatten (List.map (fun (_,(idl,patl,c)) -> idl @ ids_of_glob_constr [] c) brchl)
- | GRec _ -> failwith "Fix inside a constructor branch"
- | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) -> []
- in
- (* build the set *)
- List.fold_left (fun acc x -> Id.Set.add x acc) Id.Set.empty (ids_of_glob_constr [] c)
-
-
-
-
-
-let zeta_normalize =
- let rec zeta_normalize_term x = CAst.map (function
- | GRef _
- | GVar _
- | GEvar _
- | GPatVar _ as rt -> rt
- | GApp(rt',rtl) ->
- GApp(zeta_normalize_term rt',
- List.map zeta_normalize_term rtl
- )
- | GLambda(name,k,t,b) ->
- GLambda(name,
- k,
- zeta_normalize_term t,
- zeta_normalize_term b
- )
- | GProd(name,k,t,b) ->
- GProd(name,
- k,
- zeta_normalize_term t,
- zeta_normalize_term b
- )
- | GLetIn(Name id,def,typ,b) ->
- (zeta_normalize_term (replace_var_by_term id def b)).CAst.v
- | GLetIn(Anonymous,def,typ,b) ->
- (zeta_normalize_term b).CAst.v
- | GLetTuple(nal,(na,rto),def,b) ->
- GLetTuple(nal,
- (na,Option.map zeta_normalize_term rto),
- zeta_normalize_term def,
- zeta_normalize_term b
- )
- | GCases(sty,infos,el,brl) ->
- GCases(sty,
- infos,
- List.map (fun (e,x) -> (zeta_normalize_term e,x)) el,
- List.map zeta_normalize_br brl
- )
- | GIf(b,(na,e_option),lhs,rhs) ->
- GIf(zeta_normalize_term b,
- (na,Option.map zeta_normalize_term e_option),
- zeta_normalize_term lhs,
- zeta_normalize_term rhs
- )
- | GRec _ -> raise (UserError(None,str "Not handled GRec"))
- | GSort _
- | GHole _ as rt -> rt
- | GCast(b,c) ->
- GCast(zeta_normalize_term b,
- Miscops.map_cast_type zeta_normalize_term c)
- ) x
- and zeta_normalize_br (loc,(idl,patl,res)) =
- (loc,(idl,patl,zeta_normalize_term res))
- in
- zeta_normalize_term
-
-
-
-
let expand_as =
- let rec add_as map ({loc; CAst.v = pat } as rt) =
- match pat with
+ let rec add_as map rt =
+ match DAst.get rt with
| PatVar _ -> map
| PatCstr(_,patl,Name id) ->
Id.Map.add id (pattern_to_term rt) (List.fold_left add_as map patl)
| PatCstr(_,patl,_) -> List.fold_left add_as map patl
in
- let rec expand_as map = CAst.map (function
+ let rec expand_as map = DAst.map (function
| GRef _ | GEvar _ | GPatVar _ | GSort _ | GHole _ as rt -> rt
| GVar id as rt ->
begin
try
- (Id.Map.find id map).CAst.v
+ DAst.get (Id.Map.find id map)
with Not_found -> rt
end
| GApp(f,args) -> GApp(expand_as map f,List.map (expand_as map) args)
@@ -699,19 +541,17 @@ let expand_as =
| GRec _ -> user_err Pp.(str "Not handled GRec")
| GCast(b,c) ->
GCast(expand_as map b,
- Miscops.map_cast_type (expand_as map) c)
+ Glob_ops.map_cast_type (expand_as map) c)
| GCases(sty,po,el,brl) ->
GCases(sty, Option.map (expand_as map) po, List.map (fun (rt,t) -> expand_as map rt,t) el,
List.map (expand_as_br map) brl)
+ | GProj(p,c) -> GProj(p, expand_as map c)
)
- and expand_as_br map (loc,(idl,cpl,rt)) =
- (loc,(idl,cpl, expand_as (List.fold_left add_as map cpl) rt))
+ and expand_as_br map {CAst.loc; v=(idl,cpl,rt)} =
+ CAst.make ?loc (idl,cpl, expand_as (List.fold_left add_as map cpl) rt)
in
expand_as Id.Map.empty
-
-
-
(* [resolve_and_replace_implicits ?expected_type env sigma rt] solves implicits of [rt] w.r.t. [env] and [sigma] and then replace them by their solution
*)
@@ -722,12 +562,13 @@ let resolve_and_replace_implicits ?(flags=Pretyping.all_and_fail_flags) ?(expect
(* we first (pseudo) understand [rt] and get back the computed evar_map *)
(* FIXME : JF (30/03/2017) I'm not completely sure to have split understand as needed.
If someone knows how to prevent solved existantial removal in understand, please do not hesitate to change the computation of [ctx] here *)
- let ctx,_ = Pretyping.ise_pretype_gen flags env sigma Glob_ops.empty_lvar expected_type rt in
- let ctx, f = Evarutil.nf_evars_and_universes ctx in
+ let ctx,_,_ = Pretyping.ise_pretype_gen flags env sigma Glob_ops.empty_lvar expected_type rt in
+ let ctx = Evd.minimize_universes ctx in
+ let f c = EConstr.of_constr (Evarutil.nf_evars_universes ctx (EConstr.Unsafe.to_constr c)) in
(* then we map [rt] to replace the implicit holes by their values *)
let rec change rt =
- match rt.CAst.v with
+ match DAst.get rt with
| GHole(ImplicitArg(grk,pk,bk),_,_) -> (* we only want to deal with implicit arguments *)
(
try (* we scan the new evar map to find the evar corresponding to this hole (by looking the source *)
@@ -735,7 +576,7 @@ If someone knows how to prevent solved existantial removal in understand, pleas
(fun _ evi _ ->
match evi.evar_source with
| (loc_evi,ImplicitArg(gr_evi,p_evi,b_evi)) ->
- if Globnames.eq_gr grk gr_evi && pk=p_evi && bk=b_evi && rt.CAst.loc = loc_evi
+ if GlobRef.equal grk gr_evi && pk=p_evi && bk=b_evi && rt.CAst.loc = loc_evi
then raise (Found evi)
| _ -> ()
)
@@ -746,10 +587,34 @@ If someone knows how to prevent solved existantial removal in understand, pleas
with Found evi -> (* we found the evar corresponding to this hole *)
match evi.evar_body with
| Evar_defined c ->
- (* we just have to lift the solution in glob_term *)
- Detyping.detype false [] env ctx (EConstr.of_constr (f c))
+ (* we just have to lift the solution in glob_term *)
+ Detyping.detype Detyping.Now false Id.Set.empty env ctx (f c)
| Evar_empty -> rt (* the hole was not solved : we do nothing *)
)
+ | (GHole(BinderType na,_,_)) -> (* we only want to deal with implicit arguments *)
+ (
+ let res =
+ try (* we scan the new evar map to find the evar corresponding to this hole (by looking the source *)
+ Evd.fold (* to simulate an iter *)
+ (fun _ evi _ ->
+ match evi.evar_source with
+ | (loc_evi,BinderType na') ->
+ if Name.equal na na' && rt.CAst.loc = loc_evi then raise (Found evi)
+ | _ -> ()
+ )
+ ctx
+ ();
+ (* the hole was not solved : we do nothing *)
+ rt
+ with Found evi -> (* we found the evar corresponding to this hole *)
+ match evi.evar_body with
+ | Evar_defined c ->
+ (* we just have to lift the solution in glob_term *)
+ Detyping.detype Detyping.Now false Id.Set.empty env ctx (f c)
+ | Evar_empty -> rt (* the hole was not solved : we d when falseo nothing *)
+ in
+ res
+ )
| _ -> Glob_ops.map_glob_constr change rt
in
change rt
diff --git a/plugins/funind/glob_termops.mli b/plugins/funind/glob_termops.mli
index b6d2c45437..481a8be3ba 100644
--- a/plugins/funind/glob_termops.mli
+++ b/plugins/funind/glob_termops.mli
@@ -1,7 +1,5 @@
-open API
open Names
open Glob_term
-open Misctypes
(* [get_pattern_id pat] returns a list of all the variable appearing in [pat] *)
val get_pattern_id : cases_pattern -> Id.t list
@@ -15,29 +13,18 @@ val pattern_to_term : cases_pattern -> glob_constr
Some basic functions to rebuild glob_constr
In each of them the location is Util.Loc.ghost
*)
-val mkGRef : Globnames.global_reference -> glob_constr
+val mkGRef : GlobRef.t -> glob_constr
val mkGVar : Id.t -> glob_constr
val mkGApp : glob_constr*(glob_constr list) -> glob_constr
val mkGLambda : Name.t * glob_constr * glob_constr -> glob_constr
val mkGProd : Name.t * glob_constr * glob_constr -> glob_constr
val mkGLetIn : Name.t * glob_constr * glob_constr option * glob_constr -> glob_constr
val mkGCases : glob_constr option * tomatch_tuples * cases_clauses -> glob_constr
-val mkGSort : glob_sort -> glob_constr
val mkGHole : unit -> glob_constr (* we only build Evd.BinderType Anonymous holes *)
-val mkGCast : glob_constr* glob_constr -> glob_constr
(*
Some basic functions to decompose glob_constrs
These are analogous to the ones constrs
*)
-val glob_decompose_prod : glob_constr -> (Name.t*glob_constr) list * glob_constr
-val glob_decompose_prod_or_letin :
- glob_constr -> (Name.t*glob_constr option*glob_constr option) list * glob_constr
-val glob_decompose_prod_n : int -> glob_constr -> (Name.t*glob_constr) list * glob_constr
-val glob_decompose_prod_or_letin_n : int -> glob_constr ->
- (Name.t*glob_constr option*glob_constr option) list * glob_constr
-val glob_compose_prod : glob_constr -> (Name.t*glob_constr) list -> glob_constr
-val glob_compose_prod_or_letin: glob_constr ->
- (Name.t*glob_constr option*glob_constr option) list -> glob_constr
val glob_decompose_app : glob_constr -> glob_constr*(glob_constr list)
@@ -45,14 +32,6 @@ val glob_decompose_app : glob_constr -> glob_constr*(glob_constr list)
val glob_make_eq : ?typ:glob_constr -> glob_constr -> glob_constr -> glob_constr
(* [glob_make_neq t1 t2] build the glob_constr corresponding to [t1 <> t2] *)
val glob_make_neq : glob_constr -> glob_constr -> glob_constr
-(* [glob_make_or P1 P2] build the glob_constr corresponding to [P1 \/ P2] *)
-val glob_make_or : glob_constr -> glob_constr -> glob_constr
-
-(* [glob_make_or_list [P1;...;Pn]] build the glob_constr corresponding
- to [P1 \/ ( .... \/ Pn)]
-*)
-val glob_make_or_list : glob_constr list -> glob_constr
-
(* alpha_conversion functions *)
@@ -110,18 +89,8 @@ val eq_cases_pattern : cases_pattern -> cases_pattern -> bool
*)
val ids_of_pat : cases_pattern -> Id.Set.t
-(* TODO: finish this function (Fix not treated) *)
-val ids_of_glob_constr: glob_constr -> Id.Set.t
-
-(*
- removing let_in construction in a glob_constr
-*)
-val zeta_normalize : Glob_term.glob_constr -> Glob_term.glob_constr
-
-
val expand_as : glob_constr -> glob_constr
-
(* [resolve_and_replace_implicits ?expected_type env sigma rt] solves implicits of [rt] w.r.t. [env] and [sigma] and then replace them by their solution
*)
val resolve_and_replace_implicits :
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 2c5dae1cde..489a40ed09 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -1,8 +1,8 @@
-open API
open CErrors
+open Sorts
open Util
open Names
-open Term
+open Constr
open EConstr
open Pp
open Indfun_common
@@ -10,7 +10,7 @@ open Libnames
open Globnames
open Glob_term
open Declarations
-open Misctypes
+open Tactypes
open Decl_kinds
module RelDecl = Context.Rel.Declaration
@@ -47,7 +47,7 @@ let functional_induction with_clean c princl pat =
try find_Function_infos c'
with Not_found ->
user_err (str "Cannot find induction information on "++
- Printer.pr_leconstr (mkConst c') )
+ Printer.pr_leconstr_env (Tacmach.pf_env g) sigma (mkConst c') )
in
match Tacticals.elimination_sort_of_goal g with
| InProp -> finfo.prop_lemma
@@ -75,10 +75,9 @@ let functional_induction with_clean c princl pat =
(* mkConst(const_of_id princ_name ),g (\* FIXME *\) *)
with Not_found -> (* This one is neither defined ! *)
user_err (str "Cannot find induction principle for "
- ++Printer.pr_leconstr (mkConst c') )
+ ++ Printer.pr_leconstr_env (Tacmach.pf_env g) sigma (mkConst c') )
in
- let princ = EConstr.of_constr princ in
- (princ,NoBindings,Tacmach.pf_unsafe_type_of g' princ,g')
+ (princ,NoBindings,Tacmach.pf_unsafe_type_of g' princ,g')
| _ -> raise (UserError(None,str "functional induction must be used with a function" ))
end
| Some ((princ,binding)) ->
@@ -91,10 +90,19 @@ let functional_induction with_clean c princl pat =
if princ_infos.Tactics.farg_in_concl
then [c] else []
in
+ if List.length args + List.length c_list = 0
+ then user_err Pp.(str "Cannot recognize a valid functional scheme" );
let encoded_pat_as_patlist =
- List.make (List.length args + List.length c_list - 1) None @ [pat] in
- List.map2 (fun c pat -> ((None,Tacexpr.ElimOnConstr (fun env sigma -> (sigma,(c,NoBindings)) )),(None,pat),None))
- (args@c_list) encoded_pat_as_patlist
+ List.make (List.length args + List.length c_list - 1) None @ [pat]
+ in
+ List.map2
+ (fun c pat ->
+ ((None,
+ Ltac_plugin.Tacexpr.ElimOnConstr (fun env sigma -> (sigma,(c,NoBindings)))),
+ (None,pat),
+ None))
+ (args@c_list)
+ encoded_pat_as_patlist
in
let princ' = Some (princ,bindings) in
let princ_vars =
@@ -141,8 +149,7 @@ let rec abstract_glob_constr c = function
| Constrexpr.CLocalPattern _::bl -> assert false
let interp_casted_constr_with_implicits env sigma impls c =
- Constrintern.intern_gen Pretyping.WithoutTypeConstraint env ~impls
- c
+ Constrintern.intern_gen Pretyping.WithoutTypeConstraint env sigma ~impls c
(*
Construct a fixpoint as a Glob_term
@@ -155,14 +162,14 @@ let build_newrecursive
let sigma = Evd.from_env env0 in
let (rec_sign,rec_impls) =
List.fold_left
- (fun (env,impls) (((_,recname),_),bl,arityc,_) ->
+ (fun (env,impls) (({CAst.v=recname},_),bl,arityc,_) ->
let arityc = Constrexpr_ops.mkCProdN bl arityc in
let arity,ctx = Constrintern.interp_type env0 sigma arityc in
- let evdref = ref (Evd.from_env env0) in
- let _, (_, impls') = Constrintern.interp_context_evars env evdref bl in
- let impl = Constrintern.compute_internalization_data env0 Constrintern.Recursive arity impls' in
+ let evd = Evd.from_env env0 in
+ let evd, (_, (_, impls')) = Constrintern.interp_context_evars env evd bl in
+ let impl = Constrintern.compute_internalization_data env0 evd Constrintern.Recursive arity impls' in
let open Context.Named.Declaration in
- (Environ.push_named (LocalAssum (recname,arity)) env, Id.Map.add recname impl impls))
+ (EConstr.push_named (LocalAssum (recname,arity)) env, Id.Map.add recname impl impls))
(env0,Constrintern.empty_internalization_env) lnameargsardef in
let recdef =
(* Declare local notations *)
@@ -192,7 +199,7 @@ let error msg = user_err Pp.(str msg)
let is_rec names =
let names = List.fold_right Id.Set.add names Id.Set.empty in
let check_id id names = Id.Set.mem id names in
- let rec lookup names gt = match gt.CAst.v with
+ let rec lookup names gt = match DAst.get gt with
| GVar(id) -> check_id id names
| GRef _ | GEvar _ | GPatVar _ | GSort _ | GHole _ -> false
| GCast(b,_) -> lookup names b
@@ -215,7 +222,8 @@ let is_rec names =
| GCases(_,_,el,brl) ->
List.exists (fun (e,_) -> lookup names e) el ||
List.exists (lookup_br names) brl
- and lookup_br names (_,(idl,_,rt)) =
+ | GProj(_,c) -> lookup names c
+ and lookup_br names {CAst.v=(idl,_,rt)} =
let new_names = List.fold_right Id.Set.remove idl names in
lookup new_names rt
in
@@ -252,7 +260,6 @@ let derive_inversion fix_names =
let evd,c =
Evd.fresh_global
(Global.env ()) evd (Constrintern.locate_reference (Libnames.qualid_of_ident id)) in
- let c = EConstr.of_constr c in
let (cst, u) = destConst evd c in
evd, (cst, EInstance.kind evd u) :: l
)
@@ -274,15 +281,13 @@ let derive_inversion fix_names =
(Global.env ()) evd
(Constrintern.locate_reference (Libnames.qualid_of_ident (mk_rel_id id)))
in
- let id = EConstr.of_constr id in
- evd,(fst (destInd evd id))::l
+ evd,(fst (destInd evd id))::l
)
fix_names
(evd',[])
in
Invfun.derive_correctness
Functional_principles_types.make_scheme
- functional_induction
fix_names_as_constant
lind;
with e when CErrors.noncritical e ->
@@ -344,7 +349,7 @@ let generate_principle (evd:Evd.evar_map ref) pconstants on_error
is_general do_built (fix_rec_l:(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) recdefs interactive_proof
(continue_proof : int -> Names.Constant.t array -> EConstr.constr array -> int ->
Tacmach.tactic) : unit =
- let names = List.map (function (((_, name),_),_,_,_,_),_ -> name) fix_rec_l in
+ let names = List.map (function (({CAst.v=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
@@ -357,17 +362,17 @@ let generate_principle (evd:Evd.evar_map ref) pconstants on_error
(*i The next call to mk_rel_id is valid since we have just construct the graph
Ensures by : do_built
i*)
- let f_R_mut = Ident (Loc.tag @@ mk_rel_id (List.nth names 0)) in
+ let f_R_mut = qualid_of_ident @@ mk_rel_id (List.nth names 0) in
let ind_kn =
fst (locate_with_msg
- (pr_reference f_R_mut++str ": Not an inductive type!")
+ (pr_qualid f_R_mut++str ": Not an inductive type!")
locate_ind
f_R_mut)
in
let fname_kn (((fname,_),_,_,_,_),_) =
- let f_ref = Ident fname in
- locate_with_msg
- (pr_reference f_ref++str ": Not an inductive type!")
+ let f_ref = qualid_of_ident ?loc:fname.CAst.loc fname.CAst.v in
+ locate_with_msg
+ (pr_qualid f_ref++str ": Not an inductive type!")
locate_constant
f_ref
in
@@ -380,7 +385,8 @@ let generate_principle (evd:Evd.evar_map ref) pconstants on_error
let evd = ref (Evd.from_env env) in
let evd',uprinc = Evd.fresh_global env !evd princ in
let _ = evd := evd' in
- let princ_type = Typing.e_type_of ~refresh:true env evd (EConstr.of_constr uprinc) in
+ let sigma, princ_type = Typing.type_of ~refresh:true env !evd uprinc in
+ evd := sigma;
let princ_type = EConstr.Unsafe.to_constr princ_type in
Functional_principles_types.generate_functional_principle
evd
@@ -404,19 +410,19 @@ let generate_principle (evd:Evd.evar_map ref) pconstants on_error
let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) =
match fixpoint_exprl with
- | [(((_,fname),pl),_,bl,ret_type,body),_] when not is_rec ->
+ | [(({CAst.v=fname},pl),_,bl,ret_type,body),_] when not is_rec ->
let body = match body with | Some body -> body | None -> user_err ~hdr:"Function" (str "Body of Function must be given") in
- Command.do_definition
+ ComDefinition.do_definition
+ ~program_mode:false
fname
(Decl_kinds.Global,(Flags.is_universe_polymorphism ()),Decl_kinds.Definition) pl
bl None body (Some ret_type) (Lemmas.mk_hook (fun _ _ -> ()));
let evd,rev_pconstants =
List.fold_left
- (fun (evd,l) ((((_,fname),_),_,_,_,_),_) ->
+ (fun (evd,l) ((({CAst.v=fname},_),_,_,_,_),_) ->
let evd,c =
Evd.fresh_global
(Global.env ()) evd (Constrintern.locate_reference (Libnames.qualid_of_ident fname)) in
- let c = EConstr.of_constr c in
let (cst, u) = destConst evd c in
let u = EInstance.kind evd u in
evd,((cst, u) :: l)
@@ -426,14 +432,13 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp
in
evd,List.rev rev_pconstants
| _ ->
- Command.do_fixpoint Global (Flags.is_universe_polymorphism ()) fixpoint_exprl;
+ ComFixpoint.do_fixpoint Global (Flags.is_universe_polymorphism ()) fixpoint_exprl;
let evd,rev_pconstants =
List.fold_left
- (fun (evd,l) ((((_,fname),_),_,_,_,_),_) ->
+ (fun (evd,l) ((({CAst.v=fname},_),_,_,_,_),_) ->
let evd,c =
Evd.fresh_global
(Global.env ()) evd (Constrintern.locate_reference (Libnames.qualid_of_ident fname)) in
- let c = EConstr.of_constr c in
let (cst, u) = destConst evd c in
let u = EInstance.kind evd u in
evd,((cst, u) :: l)
@@ -459,7 +464,7 @@ let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas
let rec_arg_num =
let names =
List.map
- snd
+ CAst.(with_val (fun x -> x))
(Constrexpr_ops.names_of_local_assums args)
in
match wf_arg with
@@ -472,17 +477,17 @@ let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas
let unbounded_eq =
let f_app_args =
CAst.make @@ Constrexpr.CAppExpl(
- (None,(Ident (Loc.tag fname)),None) ,
+ (None,qualid_of_ident fname,None) ,
(List.map
(function
- | _,Anonymous -> assert false
- | _,Name e -> (Constrexpr_ops.mkIdentC e)
+ | {CAst.v=Anonymous} -> assert false
+ | {CAst.v=Name e} -> (Constrexpr_ops.mkIdentC e)
)
(Constrexpr_ops.names_of_local_assums args)
)
)
in
- CAst.make @@ Constrexpr.CApp ((None,Constrexpr_ops.mkRefC (Qualid (Loc.tag (qualid_of_string "Logic.eq")))),
+ CAst.make @@ Constrexpr.CApp ((None,Constrexpr_ops.mkRefC (qualid_of_string "Logic.eq")),
[(f_app_args,None);(body,None)])
in
let eq = Constrexpr_ops.mkCProdN args unbounded_eq in
@@ -514,7 +519,7 @@ let register_mes fname rec_impls wf_mes_expr wf_rel_expr_opt wf_arg using_lemmas
| None ->
begin
match args with
- | [Constrexpr.CLocalAssum ([(_,Name x)],k,t)] -> t,x
+ | [Constrexpr.CLocalAssum ([{CAst.v=Name x}],k,t)] -> t,x
| _ -> error "Recursive argument must be specified"
end
| Some wf_args ->
@@ -524,7 +529,7 @@ let register_mes fname rec_impls wf_mes_expr wf_rel_expr_opt wf_arg using_lemmas
(function
| Constrexpr.CLocalAssum(l,k,t) ->
List.exists
- (function (_,Name id) -> Id.equal id wf_args | _ -> false)
+ (function {CAst.v=Name id} -> Id.equal id wf_args | _ -> false)
l
| _ -> false
)
@@ -539,13 +544,13 @@ let register_mes fname rec_impls wf_mes_expr wf_rel_expr_opt wf_arg using_lemmas
| None ->
let ltof =
let make_dir l = DirPath.make (List.rev_map Id.of_string l) in
- Libnames.Qualid (Loc.tag @@ Libnames.qualid_of_path
- (Libnames.make_path (make_dir ["Arith";"Wf_nat"]) (Id.of_string "ltof")))
- in
+ Libnames.qualid_of_path
+ (Libnames.make_path (make_dir ["Arith";"Wf_nat"]) (Id.of_string "ltof"))
+ in
let fun_from_mes =
let applied_mes =
Constrexpr_ops.mkAppC(wf_mes_expr,[Constrexpr_ops.mkIdentC wf_arg]) in
- Constrexpr_ops.mkLambdaC ([(Loc.tag @@ Name wf_arg)],Constrexpr_ops.default_binder_kind,wf_arg_type,applied_mes)
+ Constrexpr_ops.mkLambdaC ([CAst.make @@ Name wf_arg],Constrexpr_ops.default_binder_kind,wf_arg_type,applied_mes)
in
let wf_rel_from_mes =
Constrexpr_ops.mkAppC(Constrexpr_ops.mkRefC ltof,[wf_arg_type;fun_from_mes])
@@ -556,7 +561,7 @@ let register_mes fname rec_impls wf_mes_expr wf_rel_expr_opt wf_arg using_lemmas
let a = Names.Id.of_string "___a" in
let b = Names.Id.of_string "___b" in
Constrexpr_ops.mkLambdaC(
- [Loc.tag @@ Name a;Loc.tag @@ Name b],
+ [CAst.make @@ Name a; CAst.make @@ Name b],
Constrexpr.Default Explicit,
wf_arg_type,
Constrexpr_ops.mkAppC(wf_rel_expr,
@@ -590,11 +595,11 @@ and rebuild_nal aux bk bl' nal typ =
match nal,typ with
| _,{ CAst.v = CProdN([],typ) } -> rebuild_nal aux bk bl' nal typ
| [], _ -> rebuild_bl aux bl' typ
- | na::nal,{ CAst.v = CProdN((na'::nal',bk',nal't)::rest,typ') } ->
- if Name.equal (snd na) (snd na') || Name.is_anonymous (snd na')
+ | na::nal,{ CAst.v = CProdN(CLocalAssum(na'::nal',bk',nal't)::rest,typ') } ->
+ if Name.equal (na.CAst.v) (na'.CAst.v) || Name.is_anonymous (na'.CAst.v)
then
let assum = CLocalAssum([na],bk,nal't) in
- let new_rest = if nal' = [] then rest else ((nal',bk',nal't)::rest) in
+ let new_rest = if nal' = [] then rest else (CLocalAssum(nal',bk',nal't)::rest) in
rebuild_nal
(assum::aux)
bk
@@ -603,7 +608,7 @@ and rebuild_nal aux bk bl' nal typ =
(CAst.make @@ CProdN(new_rest,typ'))
else
let assum = CLocalAssum([na'],bk,nal't) in
- let new_rest = if nal' = [] then rest else ((nal',bk',nal't)::rest) in
+ let new_rest = if nal' = [] then rest else (CLocalAssum(nal',bk',nal't)::rest) in
rebuild_nal
(assum::aux)
bk
@@ -616,10 +621,10 @@ and rebuild_nal aux bk bl' nal typ =
let rebuild_bl aux bl typ = rebuild_bl aux bl typ
let recompute_binder_list (fixpoint_exprl : (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) =
- let fixl,ntns = Command.extract_fixpoint_components false fixpoint_exprl in
- let ((_,_,typel),_,ctx,_) = Command.interp_fixpoint fixl ntns in
+ let fixl,ntns = ComFixpoint.extract_fixpoint_components false fixpoint_exprl in
+ let ((_,_,typel),_,ctx,_) = ComFixpoint.interp_fixpoint ~cofix:false fixl ntns in
let constr_expr_typel =
- with_full_print (List.map (Constrextern.extern_constr false (Global.env ()) (Evd.from_ctx ctx))) typel in
+ with_full_print (List.map (fun c -> Constrextern.extern_constr false (Global.env ()) (Evd.from_ctx ctx) (EConstr.of_constr c))) typel in
let fixpoint_exprl_with_new_bl =
List.map2 (fun ((lna,(rec_arg_opt,rec_order),bl,ret_typ,opt_body),notation_list) fix_typ ->
@@ -637,7 +642,7 @@ let do_generate_principle pconstants on_error register_built interactive_proof
let _is_struct =
match fixpoint_exprl with
| [((_,(wf_x,Constrexpr.CWfRec wf_rel),_,_,_),_) as fixpoint_expr] ->
- let (((((_,name),pl),_,args,types,body)),_) as fixpoint_expr =
+ let (((({CAst.v=name},pl),_,args,types,body)),_) as fixpoint_expr =
match recompute_binder_list [fixpoint_expr] with
| [e] -> e
| _ -> assert false
@@ -658,10 +663,10 @@ let do_generate_principle pconstants on_error register_built interactive_proof
true
in
if register_built
- then register_wf name rec_impls wf_rel (map_option snd wf_x) using_lemmas args types body pre_hook;
+ then register_wf name rec_impls wf_rel (map_option (fun x -> x.CAst.v) wf_x) using_lemmas args types body pre_hook;
false
|[((_,(wf_x,Constrexpr.CMeasureRec(wf_mes,wf_rel_opt)),_,_,_),_) as fixpoint_expr] ->
- let (((((_,name),_),_,args,types,body)),_) as fixpoint_expr =
+ let (((({CAst.v=name},_),_,args,types,body)),_) as fixpoint_expr =
match recompute_binder_list [fixpoint_expr] with
| [e] -> e
| _ -> assert false
@@ -682,7 +687,7 @@ let do_generate_principle pconstants on_error register_built interactive_proof
true
in
if register_built
- then register_mes name rec_impls wf_mes wf_rel_opt (map_option snd wf_x) using_lemmas args types body pre_hook;
+ then register_mes name rec_impls wf_mes wf_rel_opt (map_option (fun x -> x.CAst.v) wf_x) using_lemmas args types body pre_hook;
true
| _ ->
List.iter (function ((_na,(_,ord),_args,_body,_type),_not) ->
@@ -695,7 +700,7 @@ let do_generate_principle pconstants on_error register_built interactive_proof
fixpoint_exprl;
let fixpoint_exprl = recompute_binder_list fixpoint_exprl in
let fix_names =
- List.map (function ((((_,name),_),_,_,_,_),_) -> name) fixpoint_exprl
+ List.map (function ((({CAst.v=name},_),_,_,_,_),_) -> name) fixpoint_exprl
in
(* ok all the expressions are structural *)
let recdefs,rec_impls = build_newrecursive fixpoint_exprl in
@@ -722,28 +727,27 @@ let do_generate_principle pconstants on_error register_built interactive_proof
()
let rec add_args id new_args = CAst.map (function
- | CRef (r,_) as b ->
- begin match r with
- | Libnames.Ident(loc,fname) when Id.equal fname id ->
- CAppExpl((None,r,None),new_args)
- | _ -> b
- end
+ | CRef (qid,_) as b ->
+ if qualid_is_ident qid && Id.equal (qualid_basename qid) id then
+ CAppExpl((None,qid,None),new_args)
+ else b
| CFix _ | CCoFix _ -> anomaly ~label:"add_args " (Pp.str "todo.")
| CProdN(nal,b1) ->
- CProdN(List.map (fun (nal,k,b2) -> (nal,k,add_args id new_args b2)) nal,
+ CProdN(List.map (function CLocalAssum (nal,k,b2) -> CLocalAssum (nal,k,add_args id new_args b2)
+ | CLocalDef (na,b1,t) -> CLocalDef (na,add_args id new_args b1,Option.map (add_args id new_args) t)
+ | CLocalPattern _ -> user_err (Pp.str "pattern with quote not allowed here.")) nal,
add_args id new_args b1)
| CLambdaN(nal,b1) ->
- CLambdaN(List.map (fun (nal,k,b2) -> (nal,k,add_args id new_args b2)) nal,
+ CLambdaN(List.map (function CLocalAssum (nal,k,b2) -> CLocalAssum (nal,k,add_args id new_args b2)
+ | CLocalDef (na,b1,t) -> CLocalDef (na,add_args id new_args b1,Option.map (add_args id new_args) t)
+ | CLocalPattern _ -> user_err (Pp.str "pattern with quote not allowed here.")) nal,
add_args id new_args b1)
| CLetIn(na,b1,t,b2) ->
CLetIn(na,add_args id new_args b1,Option.map (add_args id new_args) t,add_args id new_args b2)
- | CAppExpl((pf,r,us),exprl) ->
- begin
- match r with
- | Libnames.Ident(loc,fname) when Id.equal fname id ->
- CAppExpl((pf,r,us),new_args@(List.map (add_args id new_args) exprl))
- | _ -> CAppExpl((pf,r,us),List.map (add_args id new_args) exprl)
- end
+ | CAppExpl((pf,qid,us),exprl) ->
+ if qualid_is_ident qid && Id.equal (qualid_basename qid) id then
+ CAppExpl((pf,qid,us),new_args@(List.map (add_args id new_args) exprl))
+ else CAppExpl((pf,qid,us),List.map (add_args id new_args) exprl)
| CApp((pf,b),bl) ->
CApp((pf,add_args id new_args b),
List.map (fun (e,o) -> add_args id new_args e,o) bl)
@@ -752,7 +756,7 @@ let rec add_args id new_args = CAst.map (function
List.map (fun (b,na,b_option) ->
add_args id new_args b,
na, b_option) cel,
- List.map (fun (loc,(cpl,e)) -> Loc.tag ?loc @@ (cpl,add_args id new_args e)) cal
+ List.map CAst.(map (fun (cpl,e) -> (cpl,add_args id new_args e))) cal
)
| CLetTuple(nal,(na,b_option),b1,b2) ->
CLetTuple(nal,(na,Option.map (add_args id new_args) b_option),
@@ -773,12 +777,13 @@ let rec add_args id new_args = CAst.map (function
| CSort _ as b -> b
| CCast(b1,b2) ->
CCast(add_args id new_args b1,
- Miscops.map_cast_type (add_args id new_args) b2)
+ Glob_ops.map_cast_type (add_args id new_args) b2)
| CRecord pars ->
CRecord (List.map (fun (e,o) -> e, add_args id new_args o) pars)
| CNotation _ -> anomaly ~label:"add_args " (Pp.str "CNotation.")
| CGeneralization _ -> anomaly ~label:"add_args " (Pp.str "CGeneralization.")
| CDelimiters _ -> anomaly ~label:"add_args " (Pp.str "CDelimiters.")
+ | CProj _ -> user_err Pp.(str "Funind does not support primitive projections")
)
exception Stop of Constrexpr.constr_expr
@@ -791,7 +796,7 @@ let rec chop_n_arrow n t =
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.CAst.v with
- | Constrexpr.CProdN(nal_ta',t') -> (* If we have a forall, to result are possible :
+ | Constrexpr.CProdN(nal_ta',t') -> (* If we have a forall, two results 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
@@ -803,7 +808,7 @@ let rec chop_n_arrow n t =
let new_n =
let rec aux (n:int) = function
[] -> n
- | (nal,k,t'')::nal_ta' ->
+ | CLocalAssum(nal,k,t'')::nal_ta' ->
let nal_l = List.length nal in
if n >= nal_l
then
@@ -811,9 +816,10 @@ let rec chop_n_arrow n t =
else
let new_t' = CAst.make @@
Constrexpr.CProdN(
- ((snd (List.chop n nal)),k,t'')::nal_ta',t')
+ CLocalAssum((snd (List.chop n nal)),k,t'')::nal_ta',t')
in
raise (Stop new_t')
+ | _ -> anomaly (Pp.str "Not enough products.")
in
aux n nal_ta'
in
@@ -826,39 +832,37 @@ let rec chop_n_arrow n t =
let rec get_args b t : Constrexpr.local_binder_expr list *
Constrexpr.constr_expr * Constrexpr.constr_expr =
match b.CAst.v with
- | Constrexpr.CLambdaN ((nal_ta), b') ->
+ | Constrexpr.CLambdaN (CLocalAssum(nal,k,ta) as d::rest, 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,k,ta) ->
- (Constrexpr.CLocalAssum (nal,k,ta))) nal_ta)@nal_tas, b'',t''
+ let n = List.length nal in
+ let nal_tas,b'',t'' = get_args (CAst.make ?loc:b.CAst.loc @@ Constrexpr.CLambdaN (rest,b')) (chop_n_arrow n t) in
+ d :: nal_tas, b'',t''
end
+ | Constrexpr.CLambdaN ([], b) -> [],b,t
| _ -> [],b,t
-let make_graph (f_ref:global_reference) =
+let make_graph (f_ref : GlobRef.t) =
let c,c_body =
match f_ref with
- | ConstRef c ->
- begin try c,Global.lookup_constant c
- with Not_found ->
- raise (UserError (None,str "Cannot find " ++ Printer.pr_leconstr (mkConst c)) )
- end
- | _ -> raise (UserError (None, str "Not a function reference") )
+ | ConstRef c ->
+ begin try c,Global.lookup_constant c
+ with Not_found ->
+ let sigma, env = Pfedit.get_current_context () in
+ raise (UserError (None,str "Cannot find " ++ Printer.pr_leconstr_env env sigma (mkConst c)) )
+ end
+ | _ -> raise (UserError (None, str "Not a function reference") )
in
(match Global.body_of_constant_body c_body with
| None -> error "Cannot build a graph over an axiom!"
- | Some body ->
+ | Some (body, _) ->
let env = Global.env () in
let sigma = Evd.from_env env in
let extern_body,extern_type =
with_full_print (fun () ->
- (Constrextern.extern_constr false env sigma body,
+ (Constrextern.extern_constr false env sigma (EConstr.of_constr body),
Constrextern.extern_type false env sigma
- ((*FIXME*) Typeops.type_of_constant_type env c_body.const_type)
+ (EConstr.of_constr (*FIXME*) c_body.const_type)
)
)
()
@@ -870,7 +874,7 @@ let make_graph (f_ref:global_reference) =
let l =
List.map
(fun (id,(n,recexp),bl,t,b) ->
- let loc, rec_id = Option.get n in
+ let { CAst.loc; v=rec_id } = Option.get n in
let new_args =
List.flatten
(List.map
@@ -878,29 +882,29 @@ let make_graph (f_ref:global_reference) =
| Constrexpr.CLocalDef (na,_,_)-> []
| Constrexpr.CLocalAssum (nal,_,_) ->
List.map
- (fun (loc,n) -> CAst.make ?loc @@
- CRef(Libnames.Ident(loc, Nameops.Name.get_id n),None))
+ (fun {CAst.loc;v=n} -> CAst.make ?loc @@
+ CRef(Libnames.qualid_of_ident ?loc @@ Nameops.Name.get_id n,None))
nal
| Constrexpr.CLocalPattern _ -> assert false
)
nal_tas
)
in
- let b' = add_args (snd id) new_args b in
- ((((id,None), ( Some (Loc.tag rec_id),CStructRec),nal_tas@bl,t,Some b'),[]):(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list))
+ let b' = add_args id.CAst.v new_args b in
+ ((((id,None), ( Some CAst.(make rec_id),CStructRec),nal_tas@bl,t,Some b'),[]):(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list))
)
fixexprl
in
l
| _ ->
let id = Label.to_id (Constant.label c) in
- [(((Loc.tag id),None),(None,Constrexpr.CStructRec),nal_tas,t,Some b),[]]
+ [((CAst.make id,None),(None,Constrexpr.CStructRec),nal_tas,t,Some b),[]]
in
let mp,dp,_ = Constant.repr3 c in
do_generate_principle [c,Univ.Instance.empty] error_error false false expr_list;
(* We register the infos *)
List.iter
- (fun ((((_,id),_),_,_,_,_),_) -> add_Function false (Constant.make3 mp dp (Label.of_id id)))
+ (fun ((({CAst.v=id},_),_,_,_,_),_) -> add_Function false (Constant.make3 mp dp (Label.of_id id)))
expr_list)
let do_generate_principle = do_generate_principle [] warning_error true
diff --git a/plugins/funind/indfun.mli b/plugins/funind/indfun.mli
index fc7da6a338..f209fb19fd 100644
--- a/plugins/funind/indfun.mli
+++ b/plugins/funind/indfun.mli
@@ -1,9 +1,9 @@
-open API
-open Misctypes
+open Names
+open Tactypes
-val warn_cannot_define_graph : ?loc:Loc.t -> Pp.std_ppcmds * Pp.std_ppcmds -> unit
+val warn_cannot_define_graph : ?loc:Loc.t -> Pp.t * Pp.t -> unit
-val warn_cannot_define_principle : ?loc:Loc.t -> Pp.std_ppcmds * Pp.std_ppcmds -> unit
+val warn_cannot_define_principle : ?loc:Loc.t -> Pp.t * Pp.t -> unit
val do_generate_principle :
bool ->
@@ -15,8 +15,8 @@ val functional_induction :
bool ->
EConstr.constr ->
(EConstr.constr * EConstr.constr bindings) option ->
- Tacexpr.or_and_intro_pattern option ->
+ Ltac_plugin.Tacexpr.or_and_intro_pattern option ->
Goal.goal Evd.sigma -> Goal.goal list Evd.sigma
-val make_graph : Globnames.global_reference -> unit
+val make_graph : GlobRef.t -> unit
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 6fe6888f3d..4eee2c7a45 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -1,9 +1,10 @@
-open API
open Names
open Pp
+open Constr
open Libnames
open Globnames
open Refiner
+
let mk_prefix pre id = Id.of_string (pre^(Id.to_string id))
let mk_rel_id = mk_prefix "R_"
let mk_correct_id id = Nameops.add_suffix (mk_rel_id id) "_correct"
@@ -13,7 +14,7 @@ let mk_equation_id id = Nameops.add_suffix id "_equation"
let msgnl m =
()
-let fresh_id avoid s = Namegen.next_ident_away_in_goal (Id.of_string s) avoid
+let fresh_id avoid s = Namegen.next_ident_away_in_goal (Id.of_string s) (Id.Set.of_list avoid)
let fresh_name avoid s = Name (fresh_id avoid s)
@@ -30,9 +31,7 @@ let id_of_name = function
Name id -> id
| _ -> raise Not_found
-let locate ref =
- let (loc,qid) = qualid_of_reference ref in
- Nametab.locate qid
+let locate qid = Nametab.locate qid
let locate_ind ref =
match locate ref with
@@ -67,7 +66,7 @@ let chop_rlambda_n =
if n == 0
then List.rev acc,rt
else
- match rt.CAst.v with
+ match DAst.get rt with
| Glob_term.GLambda(name,k,t,b) -> chop_lambda_n ((name,t,None)::acc) (n-1) b
| Glob_term.GLetIn(name,v,t,b) -> chop_lambda_n ((name,v,t)::acc) (n-1) b
| _ ->
@@ -81,7 +80,7 @@ let chop_rprod_n =
if n == 0
then List.rev acc,rt
else
- match rt.CAst.v with
+ match DAst.get rt with
| Glob_term.GProd(name,k,t,b) -> chop_prod_n ((name,t)::acc) (n-1) b
| _ -> raise (CErrors.UserError(Some "chop_rprod_n",str "chop_rprod_n: Not enough products"))
in
@@ -99,21 +98,16 @@ let list_union_eq eq_fun l1 l2 =
let list_add_set_eq eq_fun x l =
if List.exists (eq_fun x) l then l else x::l
-
-
-
let const_of_id id =
- let _,princ_ref =
- qualid_of_reference (Libnames.Ident (Loc.tag id))
- in
+ let princ_ref = qualid_of_ident id in
try Constrintern.locate_reference princ_ref
with Not_found ->
CErrors.user_err ~hdr:"IndFun.const_of_id"
(str "cannot find " ++ Id.print id)
let def_of_const t =
- match (Term.kind_of_term t) with
- Term.Const sp ->
+ match Constr.kind t with
+ Const sp ->
(try (match Environ.constant_opt_value_in (Global.env()) sp with
| Some c -> c
| _ -> assert false)
@@ -121,7 +115,7 @@ let def_of_const t =
|_ -> assert false
let coq_constant s =
- Universes.constr_of_global @@
+ UnivGen.constr_of_global @@
Coqlib.gen_reference_in_modules "RecursiveDefinition"
Coqlib.init_modules s;;
@@ -182,12 +176,13 @@ let with_full_print f a =
and old_contextual_implicit_args = Impargs.is_contextual_implicit_args () in
let old_rawprint = !Flags.raw_print in
let old_printuniverses = !Constrextern.print_universes in
+ let old_printallowmatchdefaultclause = !Detyping.print_allow_match_default_clause in
Constrextern.print_universes := true;
+ Detyping.print_allow_match_default_clause := false;
Flags.raw_print := true;
Impargs.make_implicit_args false;
Impargs.make_strict_implicit_args false;
Impargs.make_contextual_implicit_args false;
- Impargs.make_contextual_implicit_args false;
Dumpglob.pause ();
try
let res = f a in
@@ -196,6 +191,7 @@ let with_full_print f a =
Impargs.make_contextual_implicit_args old_contextual_implicit_args;
Flags.raw_print := old_rawprint;
Constrextern.print_universes := old_printuniverses;
+ Detyping.print_allow_match_default_clause := old_printallowmatchdefaultclause;
Dumpglob.continue ();
res
with
@@ -205,6 +201,7 @@ let with_full_print f a =
Impargs.make_contextual_implicit_args old_contextual_implicit_args;
Flags.raw_print := old_rawprint;
Constrextern.print_universes := old_printuniverses;
+ Detyping.print_allow_match_default_clause := old_printallowmatchdefaultclause;
Dumpglob.continue ();
raise reraise
@@ -270,12 +267,12 @@ let subst_Function (subst,finfos) =
in
let function_constant' = do_subst_con finfos.function_constant in
let graph_ind' = do_subst_ind finfos.graph_ind in
- let equation_lemma' = Option.smartmap do_subst_con finfos.equation_lemma in
- let correctness_lemma' = Option.smartmap do_subst_con finfos.correctness_lemma in
- let completeness_lemma' = Option.smartmap do_subst_con finfos.completeness_lemma in
- let rect_lemma' = Option.smartmap do_subst_con finfos.rect_lemma in
- let rec_lemma' = Option.smartmap do_subst_con finfos.rec_lemma in
- let prop_lemma' = Option.smartmap do_subst_con finfos.prop_lemma in
+ let equation_lemma' = Option.Smart.map do_subst_con finfos.equation_lemma in
+ let correctness_lemma' = Option.Smart.map do_subst_con finfos.correctness_lemma in
+ let completeness_lemma' = Option.Smart.map do_subst_con finfos.completeness_lemma in
+ let rect_lemma' = Option.Smart.map do_subst_con finfos.rect_lemma in
+ let rec_lemma' = Option.Smart.map do_subst_con finfos.rec_lemma in
+ let prop_lemma' = Option.Smart.map do_subst_con finfos.prop_lemma in
if function_constant' == finfos.function_constant &&
graph_ind' == finfos.graph_ind &&
equation_lemma' == finfos.equation_lemma &&
@@ -303,12 +300,12 @@ let classify_Function infos = Libobject.Substitute infos
let discharge_Function (_,finfos) =
let function_constant' = Lib.discharge_con finfos.function_constant
and graph_ind' = Lib.discharge_inductive finfos.graph_ind
- and equation_lemma' = Option.smartmap Lib.discharge_con finfos.equation_lemma
- and correctness_lemma' = Option.smartmap Lib.discharge_con finfos.correctness_lemma
- and completeness_lemma' = Option.smartmap Lib.discharge_con finfos.completeness_lemma
- and rect_lemma' = Option.smartmap Lib.discharge_con finfos.rect_lemma
- and rec_lemma' = Option.smartmap Lib.discharge_con finfos.rec_lemma
- and prop_lemma' = Option.smartmap Lib.discharge_con finfos.prop_lemma
+ and equation_lemma' = Option.Smart.map Lib.discharge_con finfos.equation_lemma
+ and correctness_lemma' = Option.Smart.map Lib.discharge_con finfos.correctness_lemma
+ and completeness_lemma' = Option.Smart.map Lib.discharge_con finfos.completeness_lemma
+ and rect_lemma' = Option.Smart.map Lib.discharge_con finfos.rect_lemma
+ and rec_lemma' = Option.Smart.map Lib.discharge_con finfos.rec_lemma
+ and prop_lemma' = Option.Smart.map Lib.discharge_con finfos.prop_lemma
in
if function_constant' == finfos.function_constant &&
graph_ind' == finfos.graph_ind &&
@@ -331,18 +328,18 @@ let discharge_Function (_,finfos) =
is_general = finfos.is_general
}
-open Term
-
let pr_ocst c =
- Option.fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) c (mt ())
+ let sigma, env = Pfedit.get_current_context () in
+ Option.fold_right (fun v acc -> Printer.pr_lconstr_env env sigma (mkConst v)) c (mt ())
let pr_info f_info =
+ let sigma, env = Pfedit.get_current_context () in
str "function_constant := " ++
- Printer.pr_lconstr (mkConst f_info.function_constant)++ fnl () ++
+ Printer.pr_lconstr_env env sigma (mkConst f_info.function_constant)++ fnl () ++
str "function_constant_type := " ++
(try
- Printer.pr_lconstr
- (Global.type_of_global_unsafe (ConstRef f_info.function_constant))
+ Printer.pr_lconstr_env env sigma
+ (fst (Global.type_of_global_in_context env (ConstRef f_info.function_constant)))
with e when CErrors.noncritical e -> mt ()) ++ fnl () ++
str "equation_lemma := " ++ pr_ocst f_info.equation_lemma ++ fnl () ++
str "completeness_lemma :=" ++ pr_ocst f_info.completeness_lemma ++ fnl () ++
@@ -350,7 +347,7 @@ let pr_info f_info =
str "rect_lemma := " ++ pr_ocst f_info.rect_lemma ++ fnl () ++
str "rec_lemma := " ++ pr_ocst f_info.rec_lemma ++ fnl () ++
str "prop_lemma := " ++ pr_ocst f_info.prop_lemma ++ fnl () ++
- str "graph_ind := " ++ Printer.pr_lconstr (mkInd f_info.graph_ind) ++ fnl ()
+ str "graph_ind := " ++ Printer.pr_lconstr_env env sigma (mkInd f_info.graph_ind) ++ fnl ()
let pr_table tb =
let l = Cmap_env.fold (fun k v acc -> v::acc) tb [] in
@@ -472,7 +469,7 @@ let jmeq () =
try
Coqlib.check_required_library Coqlib.jmeq_module_name;
EConstr.of_constr @@
- Universes.constr_of_global @@
+ UnivGen.constr_of_global @@
Coqlib.coq_reference "Function" ["Logic";"JMeq"] "JMeq"
with e when CErrors.noncritical e -> raise (ToShow e)
@@ -480,7 +477,7 @@ let jmeq_refl () =
try
Coqlib.check_required_library Coqlib.jmeq_module_name;
EConstr.of_constr @@
- Universes.constr_of_global @@
+ UnivGen.constr_of_global @@
Coqlib.coq_reference "Function" ["Logic";"JMeq"] "JMeq_refl"
with e when CErrors.noncritical e -> raise (ToShow e)
@@ -493,7 +490,7 @@ let well_founded = function () -> EConstr.of_constr (coq_constant "well_founded"
let acc_rel = function () -> EConstr.of_constr (coq_constant "Acc")
let acc_inv_id = function () -> EConstr.of_constr (coq_constant "Acc_inv")
-let well_founded_ltof () = EConstr.of_constr @@ Universes.constr_of_global @@
+let well_founded_ltof () = EConstr.of_constr @@ UnivGen.constr_of_global @@
Coqlib.coq_reference "" ["Arith";"Wf_nat"] "well_founded_ltof"
let ltof_ref = function () -> (find_reference ["Coq";"Arith";"Wf_nat"] "ltof")
@@ -546,7 +543,16 @@ let prodn n env b =
(* compose_prod [xn:Tn;..;x1:T1] b = (x1:T1)..(xn:Tn)b *)
let compose_prod l b = prodn (List.length l) l b
-type tcc_lemma_value =
+type tcc_lemma_value =
| Undefined
- | Value of Term.constr
+ | Value of constr
| Not_needed
+
+(* We only "purify" on exceptions. XXX: What is this doing here? *)
+let funind_purify f x =
+ let st = Vernacstate.freeze_interp_state `No in
+ try f x
+ with e ->
+ let e = CErrors.push e in
+ Vernacstate.unfreeze_interp_state st;
+ Exninfo.iraise e
diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli
index f7a9cedd73..7e52ee224f 100644
--- a/plugins/funind/indfun_common.mli
+++ b/plugins/funind/indfun_common.mli
@@ -1,6 +1,4 @@
-open API
open Names
-open Pp
(*
The mk_?_id function build different name w.r.t. a function
@@ -12,7 +10,7 @@ val mk_complete_id : Id.t -> Id.t
val mk_equation_id : Id.t -> Id.t
-val msgnl : std_ppcmds -> unit
+val msgnl : Pp.t -> unit
val fresh_id : Id.t list -> string -> Id.t
val fresh_name : Id.t list -> string -> Name.t
@@ -22,11 +20,11 @@ val array_get_start : 'a array -> 'a array
val id_of_name : Name.t -> Id.t
-val locate_ind : Libnames.reference -> inductive
-val locate_constant : Libnames.reference -> Constant.t
+val locate_ind : Libnames.qualid -> inductive
+val locate_constant : Libnames.qualid -> Constant.t
val locate_with_msg :
- Pp.std_ppcmds -> (Libnames.reference -> 'a) ->
- Libnames.reference -> 'a
+ Pp.t -> (Libnames.qualid -> 'a) ->
+ Libnames.qualid -> 'a
val filter_map : ('a -> bool) -> ('a -> 'b) -> 'a list -> 'b list
val list_union_eq :
@@ -40,10 +38,10 @@ val chop_rlambda_n : int -> Glob_term.glob_constr ->
val chop_rprod_n : int -> Glob_term.glob_constr ->
(Name.t*Glob_term.glob_constr) list * Glob_term.glob_constr
-val def_of_const : Term.constr -> Term.constr
+val def_of_const : Constr.t -> Constr.t
val eq : EConstr.constr Lazy.t
val refl_equal : EConstr.constr Lazy.t
-val const_of_id: Id.t -> Globnames.global_reference(* constantyes *)
+val const_of_id: Id.t -> GlobRef.t(* constantyes *)
val jmeq : unit -> EConstr.constr
val jmeq_refl : unit -> EConstr.constr
@@ -90,8 +88,8 @@ val update_Function : function_info -> unit
(** debugging *)
-val pr_info : function_info -> Pp.std_ppcmds
-val pr_table : unit -> Pp.std_ppcmds
+val pr_info : function_info -> Pp.t
+val pr_table : unit -> Pp.t
(* val function_debug : bool ref *)
@@ -109,19 +107,21 @@ val h_intros: Names.Id.t list -> Tacmach.tactic
val h_id : Names.Id.t
val hrec_id : Names.Id.t
val acc_inv_id : EConstr.constr Util.delayed
-val ltof_ref : Globnames.global_reference Util.delayed
+val ltof_ref : GlobRef.t Util.delayed
val well_founded_ltof : EConstr.constr Util.delayed
val acc_rel : EConstr.constr Util.delayed
val well_founded : EConstr.constr Util.delayed
-val evaluable_of_global_reference : Globnames.global_reference -> Names.evaluable_global_reference
+val evaluable_of_global_reference : GlobRef.t -> Names.evaluable_global_reference
val list_rewrite : bool -> (EConstr.constr*bool) list -> Tacmach.tactic
val decompose_lam_n : Evd.evar_map -> int -> EConstr.t ->
(Names.Name.t * EConstr.t) list * EConstr.t
val compose_lam : (Names.Name.t * EConstr.t) list -> EConstr.t -> EConstr.t
val compose_prod : (Names.Name.t * EConstr.t) list -> EConstr.t -> EConstr.t
-
-type tcc_lemma_value =
+
+type tcc_lemma_value =
| Undefined
- | Value of Term.constr
+ | Value of Constr.t
| Not_needed
+
+val funind_purify : ('a -> 'b) -> ('a -> 'b)
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index e6f10a880c..439274240f 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -1,18 +1,20 @@
(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
-open API
open Ltac_plugin
open Declarations
open CErrors
open Util
open Names
open Term
+open Constr
open EConstr
open Vars
open Pp
@@ -21,7 +23,7 @@ open Tacticals
open Tactics
open Indfun_common
open Tacmach
-open Misctypes
+open Tactypes
open Termops
open Context.Rel.Declaration
@@ -56,12 +58,6 @@ let do_observe_tac s tac g =
CErrors.iprint e ++ str " on goal" ++ fnl() ++ goal ));
iraise reraise;;
-
-let observe_tac_strm s tac g =
- if do_observe ()
- then do_observe_tac s tac g
- else tac g
-
let observe_tac s tac g =
if do_observe ()
then do_observe_tac (str s) tac g
@@ -71,7 +67,7 @@ let observe_tac s tac g =
let nf_zeta =
Reductionops.clos_norm_flags (CClosure.RedFlags.mkflags [CClosure.RedFlags.fZETA])
Environ.empty_env
- Evd.empty
+ (Evd.from_env Environ.empty_env)
let thin ids gl = Proofview.V82.of_tactic (Tactics.clear ids) gl
@@ -85,12 +81,8 @@ let thin ids gl = Proofview.V82.of_tactic (Tactics.clear ids) gl
let make_eq () =
try
- EConstr.of_constr (Universes.constr_of_global (Coqlib.build_coq_eq ()))
+ EConstr.of_constr (UnivGen.constr_of_global (Coqlib.build_coq_eq ()))
with _ -> assert false
-let make_eq_refl () =
- try
- EConstr.of_constr (Universes.constr_of_global (Coqlib.build_coq_eq_refl ()))
- with _ -> assert false
(* [generate_type g_to_f f graph i] build the completeness (resp. correctness) lemma type if [g_to_f = true]
@@ -110,9 +102,9 @@ let generate_type evd g_to_f f graph i =
let evd',graph =
Evd.fresh_global (Global.env ()) !evd (Globnames.IndRef (fst (destInd !evd graph)))
in
- let graph = EConstr.of_constr graph in
evd:=evd';
- let graph_arity = Typing.e_type_of (Global.env ()) evd graph in
+ let sigma, graph_arity = Typing.type_of (Global.env ()) !evd graph in
+ evd := sigma;
let ctxt,_ = decompose_prod_assum !evd graph_arity in
let fun_ctxt,res_type =
match ctxt with
@@ -132,9 +124,9 @@ let generate_type evd g_to_f f graph i =
| Name id -> Some id
| Anonymous -> None
in
- let named_ctxt = List.map_filter filter fun_ctxt in
+ let named_ctxt = Id.Set.of_list (List.map_filter filter fun_ctxt) in
let res_id = Namegen.next_ident_away_in_goal (Id.of_string "_res") named_ctxt in
- let fv_id = Namegen.next_ident_away_in_goal (Id.of_string "fv") (res_id :: named_ctxt) in
+ let fv_id = Namegen.next_ident_away_in_goal (Id.of_string "fv") (Id.Set.add res_id named_ctxt) in
(*i we can then type the argument to be applied to the function [f] i*)
let args_as_rels = Array.of_list (args_from_decl 1 [] fun_ctxt) in
(*i
@@ -180,7 +172,6 @@ let find_induction_principle evd f =
| None -> raise Not_found
| Some rect_lemma ->
let evd',rect_lemma = Evd.fresh_global (Global.env ()) !evd (Globnames.ConstRef rect_lemma) in
- let rect_lemma = EConstr.of_constr rect_lemma in
let evd',typ = Typing.type_of ~refresh:true (Global.env ()) evd' rect_lemma in
evd:=evd';
rect_lemma,typ
@@ -190,14 +181,13 @@ let rec generate_fresh_id x avoid i =
if i == 0
then []
else
- let id = Namegen.next_ident_away_in_goal x avoid in
+ let id = Namegen.next_ident_away_in_goal x (Id.Set.of_list avoid) in
id::(generate_fresh_id x (id::avoid) (pred i))
-(* [prove_fun_correct functional_induction funs_constr graphs_constr schemes lemmas_types_infos i ]
+(* [prove_fun_correct funs_constr graphs_constr schemes lemmas_types_infos i ]
is the tactic used to prove correctness lemma.
- [functional_induction] is the tactic defined in [indfun] (dependency problem)
[funs_constr], [graphs_constr] [schemes] [lemmas_types_infos] are the mutually recursive functions
(resp. graphs of the functions and principles and correctness lemma types) to prove correct.
@@ -218,7 +208,7 @@ let rec generate_fresh_id x avoid i =
\end{enumerate}
*)
-let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes lemmas_types_infos i : Tacmach.tactic =
+let prove_fun_correct evd funs_constr graphs_constr schemes lemmas_types_infos i : Tacmach.tactic =
fun g ->
(* first of all we recreate the lemmas types to be used as predicates of the induction principle
that is~:
@@ -240,7 +230,7 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes
environment and due to the bug #1174, we will need to pose the principle
using a name
*)
- let principle_id = Namegen.next_ident_away_in_goal (Id.of_string "princ") ids in
+ let principle_id = Namegen.next_ident_away_in_goal (Id.of_string "princ") (Id.Set.of_list ids) in
let ids = principle_id :: ids in
(* We get the branches of the principle *)
let branches = List.rev princ_infos.branches in
@@ -249,7 +239,7 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes
List.map
(fun decl ->
List.map
- (fun id -> Loc.tag @@ IntroNaming (IntroIdentifier id))
+ (fun id -> CAst.make @@ IntroNaming (Namegen.IntroIdentifier id))
(generate_fresh_id (Id.of_string "y") ids (List.length (fst (decompose_prod_assum evd (RelDecl.get_type decl)))))
)
branches
@@ -265,9 +255,9 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes
(* We get the identifiers of this branch *)
let pre_args =
List.fold_right
- (fun (_,pat) acc ->
+ (fun {CAst.v=pat} acc ->
match pat with
- | IntroNaming (IntroIdentifier id) -> id::acc
+ | IntroNaming (Namegen.IntroIdentifier id) -> id::acc
| _ -> anomaly (Pp.str "Not an identifier.")
)
(List.nth intro_pats (pred i))
@@ -397,7 +387,7 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes
let params_bindings,avoid =
List.fold_left2
(fun (bindings,avoid) decl p ->
- let id = Namegen.next_ident_away (Nameops.Name.get_id (RelDecl.get_name decl)) avoid in
+ let id = Namegen.next_ident_away (Nameops.Name.get_id (RelDecl.get_name decl)) (Id.Set.of_list avoid) in
p::bindings,id::avoid
)
([],pf_ids_of_hyps g)
@@ -407,7 +397,7 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes
let lemmas_bindings =
List.rev (fst (List.fold_left2
(fun (bindings,avoid) decl p ->
- let id = Namegen.next_ident_away (Nameops.Name.get_id (RelDecl.get_name decl)) avoid in
+ let id = Namegen.next_ident_away (Nameops.Name.get_id (RelDecl.get_name decl)) (Id.Set.of_list avoid) in
(nf_zeta p)::bindings,id::avoid)
([],avoid)
princ_infos.predicates
@@ -522,7 +512,7 @@ and intros_with_rewrite_aux : Tacmach.tactic =
intros_with_rewrite
] g
end
- | Ind _ when EConstr.eq_constr sigma t (EConstr.of_constr (Universes.constr_of_global @@ Coqlib.build_coq_False ())) ->
+ | Ind _ when EConstr.eq_constr sigma t (EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.build_coq_False ())) ->
Proofview.V82.of_tactic tauto g
| Case(_,_,v,_) ->
tclTHENLIST[
@@ -571,6 +561,11 @@ let rec reflexivity_with_destruct_cases g =
with e when CErrors.noncritical e -> Proofview.V82.of_tactic reflexivity
in
let eq_ind = make_eq () in
+ let my_inj_flags = Some {
+ Equality.keep_proof_equalities = false;
+ injection_in_context = false; (* for compatibility, necessary *)
+ injection_pattern_l2r_order = false; (* probably does not matter; except maybe with dependent hyps *)
+ } in
let discr_inject =
Tacticals.onAllHypsAndConcl (
fun sc g ->
@@ -581,8 +576,8 @@ let rec reflexivity_with_destruct_cases g =
| App(eq,[|_;t1;t2|]) when EConstr.eq_constr (project g) eq eq_ind ->
if Equality.discriminable (pf_env g) (project g) t1 t2
then Proofview.V82.of_tactic (Equality.discrHyp id) g
- else if Equality.injectable (pf_env g) (project g) t1 t2
- then tclTHENLIST [Proofview.V82.of_tactic (Equality.injHyp None id);thin [id];intros_with_rewrite] g
+ else if Equality.injectable (pf_env g) (project g) ~keep_proofs:None t1 t2
+ then tclTHENLIST [Proofview.V82.of_tactic (Equality.injHyp my_inj_flags None id);thin [id];intros_with_rewrite] g
else tclIDTAC g
| _ -> tclIDTAC g
)
@@ -747,20 +742,20 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : Tacmach.tacti
g
-(* [derive_correctness make_scheme functional_induction funs graphs] create correctness and completeness
+(* [derive_correctness make_scheme funs graphs] create correctness and completeness
lemmas for each function in [funs] w.r.t. [graphs]
[make_scheme] is Functional_principle_types.make_scheme (dependency pb) and
- [functional_induction] is Indfun.functional_induction (same pb)
*)
-let derive_correctness make_scheme functional_induction (funs: pconstant list) (graphs:inductive list) =
+let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list) =
assert (funs <> []);
assert (graphs <> []);
let funs = Array.of_list funs and graphs = Array.of_list graphs in
let map (c, u) = mkConstU (c, EInstance.make u) in
let funs_constr = Array.map map funs in
- States.with_state_protection_on_exception
+ (* XXX STATE Why do we need this... why is the toplevel protection not enought *)
+ funind_purify
(fun () ->
let env = Global.env () in
let evd = ref (Evd.from_env env) in
@@ -775,7 +770,8 @@ let derive_correctness make_scheme functional_induction (funs: pconstant list) (
let type_info = (type_of_lemma_ctxt,type_of_lemma_concl) in
graphs_constr.(i) <- graph;
let type_of_lemma = EConstr.it_mkProd_or_LetIn type_of_lemma_concl type_of_lemma_ctxt in
- let _ = Typing.e_type_of (Global.env ()) evd type_of_lemma in
+ let sigma, _ = Typing.type_of (Global.env ()) !evd type_of_lemma in
+ evd := sigma;
let type_of_lemma = nf_zeta type_of_lemma in
observe (str "type_of_lemma := " ++ Printer.pr_leconstr_env (Global.env ()) !evd type_of_lemma);
type_of_lemma,type_info
@@ -798,12 +794,12 @@ let derive_correctness make_scheme functional_induction (funs: pconstant list) (
(fun entry ->
(EConstr.of_constr (fst (fst(Future.force entry.Entries.const_entry_body))), EConstr.of_constr (Option.get entry.Entries.const_entry_type ))
)
- (make_scheme evd (Array.map_to_list (fun const -> const,GType []) funs))
+ (make_scheme evd (Array.map_to_list (fun const -> const,Sorts.InType) funs))
)
)
in
let proving_tac =
- prove_fun_correct !evd functional_induction funs_constr graphs_constr schemes lemmas_types_infos
+ prove_fun_correct !evd funs_constr graphs_constr schemes lemmas_types_infos
in
Array.iteri
(fun i f_as_constant ->
@@ -822,13 +818,12 @@ let derive_correctness make_scheme functional_induction (funs: pconstant list) (
ignore (Pfedit.by
(Proofview.V82.tactic (observe_tac ("prove correctness ("^(Id.to_string f_id)^")")
(proving_tac i))));
- (Lemmas.save_proof (Vernacexpr.(Proved(Transparent,None))));
+ (Lemmas.save_proof (Vernacexpr.(Proved(Proof_global.Transparent,None))));
let finfo = find_Function_infos (fst f_as_constant) in
(* let lem_cst = fst (destConst (Constrintern.global_reference lem_id)) in *)
let _,lem_cst_constr = Evd.fresh_global
(Global.env ()) !evd (Constrintern.locate_reference (Libnames.qualid_of_ident lem_id)) in
- let lem_cst_constr = EConstr.of_constr lem_cst_constr in
- let (lem_cst,_) = destConst !evd lem_cst_constr in
+ let (lem_cst,_) = destConst !evd lem_cst_constr in
update_Function {finfo with correctness_lemma = Some lem_cst};
)
@@ -845,7 +840,7 @@ let derive_correctness make_scheme functional_induction (funs: pconstant list) (
EConstr.it_mkProd_or_LetIn type_of_lemma_concl type_of_lemma_ctxt
in
let type_of_lemma = nf_zeta type_of_lemma in
- observe (str "type_of_lemma := " ++ Printer.pr_leconstr type_of_lemma);
+ observe (str "type_of_lemma := " ++ Printer.pr_leconstr_env env !evd type_of_lemma);
type_of_lemma,type_info
)
funs_constr
@@ -884,12 +879,11 @@ let derive_correctness make_scheme functional_induction (funs: pconstant list) (
ignore (Pfedit.by
(Proofview.V82.tactic (observe_tac ("prove completeness ("^(Id.to_string f_id)^")")
(proving_tac i)))) ;
- (Lemmas.save_proof (Vernacexpr.(Proved(Transparent,None))));
+ (Lemmas.save_proof (Vernacexpr.(Proved(Proof_global.Transparent,None))));
let finfo = find_Function_infos (fst f_as_constant) in
let _,lem_cst_constr = Evd.fresh_global
(Global.env ()) !evd (Constrintern.locate_reference (Libnames.qualid_of_ident lem_id)) in
- let lem_cst_constr = EConstr.of_constr lem_cst_constr in
- let (lem_cst,_) = destConst !evd lem_cst_constr in
+ let (lem_cst,_) = destConst !evd lem_cst_constr in
update_Function {finfo with completeness_lemma = Some lem_cst}
)
funs)
@@ -973,7 +967,7 @@ let functional_inversion kn hid fconst f_correct : Tacmach.tactic =
Proofview.V82.of_tactic (generalize [applist(f_correct,(Array.to_list f_args)@[res;mkVar hid])]);
thin [hid];
Proofview.V82.of_tactic (Simple.intro hid);
- Proofview.V82.of_tactic (Inv.inv FullInversion None (NamedHyp hid));
+ Proofview.V82.of_tactic (Inv.inv Inv.FullInversion None (NamedHyp hid));
(fun g ->
let new_ids = List.filter (fun id -> not (Id.Set.mem id old_ids)) (pf_ids_of_hyps g) in
tclMAP (revert_graph kn pre_tac) (hid::new_ids) g
diff --git a/plugins/funind/invfun.mli b/plugins/funind/invfun.mli
new file mode 100644
index 0000000000..3ddc609201
--- /dev/null
+++ b/plugins/funind/invfun.mli
@@ -0,0 +1,19 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+val invfun :
+ Tactypes.quantified_hypothesis ->
+ Names.GlobRef.t option ->
+ Evar.t Evd.sigma -> Evar.t list Evd.sigma
+val derive_correctness :
+ (Evd.evar_map ref ->
+ (Constr.pconstant * Sorts.family) list ->
+ 'a Entries.definition_entry list) ->
+ Constr.pconstant list -> Names.inductive list -> unit
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
deleted file mode 100644
index 63662a4437..0000000000
--- a/plugins/funind/merge.ml
+++ /dev/null
@@ -1,1002 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
-
-(* Merging of induction principles. *)
-
-open API
-open Globnames
-open Tactics
-open Indfun_common
-open CErrors
-open Util
-open Constrexpr
-open Vernacexpr
-open Pp
-open Names
-open Term
-open Vars
-open Declarations
-open Glob_term
-open Glob_termops
-open Decl_kinds
-open Context.Rel.Declaration
-
-module RelDecl = Context.Rel.Declaration
-
-(** {1 Utilities} *)
-
-(** {2 Useful operations on constr and glob_constr} *)
-
-let pop c = Vars.lift (-1) c
-let rec popn i c = if i<=0 then c else pop (popn (i-1) c)
-
-(** Substitutions in constr *)
-let compare_constr_nosub t1 t2 =
- if compare_constr (fun _ _ -> false) t1 t2
- 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.understand (Global.env()) Evd.empty
-
-(** Operations on names and identifiers *)
-let id_of_name = function
- Anonymous -> Id.of_string "H"
- | Name id -> id;;
-let name_of_string = Id.of_string %> Name.mk_name
-let string_of_name = id_of_name %> Id.to_string
-
-(** [isVarf f x] returns [true] if term [x] is of the form [(Var f)]. *)
-let isVarf f x =
- match x with
- | { CAst.v = GVar x } -> Id.equal x f
- | _ -> false
-
-(** [ident_global_exist id] returns true if identifier [id] is linked
- in global environment. *)
-let ident_global_exist id =
- try
- let ans = CAst.make @@ CRef (Libnames.Ident (Loc.tag id), None) in
- let _ = ignore (Constrintern.intern_constr (Global.env()) ans) in
- true
- with e when CErrors.noncritical e -> false
-
-(** [next_ident_fresh id] returns a fresh identifier (ie not linked in
- global env) with base [id]. *)
-let next_ident_fresh (id:Id.t) =
- let res = ref id in
- while ident_global_exist !res do res := Nameops.increment_subscript !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_glob_constr 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 prNamedRLDecl s lc =
- begin
- prstr s; prstr "\n"; prstr "{§§ ";
- List.iter
- (fun x ->
- match x with
- | (nm,None,Some tp) -> prNamedRConstr (string_of_name nm) tp
- | (nm,Some bdy,None) -> prNamedRConstr ("(letin) "^string_of_name nm) bdy
- | _ -> assert false
- ) lc;
- prstr " §§}\n";
- prstr "\n";
- end
-
-(** {2 Misc} *)
-
-exception Found of int
-
-(* Array scanning *)
-
-let array_prfx (arr: 'a array) (pred: int -> 'a -> bool): int =
-match Array.findi pred arr with
-| None -> Array.length arr (* all elt are positive *)
-| Some i -> i
-
-(* 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 describes 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 (Int)
-
-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
-
-(** Information about graph merging of two inductives.
- All rel_decl list are IN REVERSE ORDER (ie well suited for compose) *)
-
-type merge_infos =
- {
- ident:Id.t; (** 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;
-
- (** rec params which remain rec param (ie not linked) *)
- recprms1: Context.Rel.Declaration.t list;
- recprms2: Context.Rel.Declaration.t list;
- nrecprms1: int;
- nrecprms2: int;
-
- (** rec parms which became non parm (either linked to something
- or because after a rec parm that became non parm) *)
- otherprms1: Context.Rel.Declaration.t list;
- otherprms2: Context.Rel.Declaration.t list;
- notherprms1:int;
- notherprms2:int;
-
- (** args which remain args in merge *)
- args1:Context.Rel.Declaration.t list;
- args2:Context.Rel.Declaration.t list;
- nargs1:int;
- nargs2:int;
-
- (** functional result args *)
- funresprms1: Context.Rel.Declaration.t list;
- funresprms2: Context.Rel.Declaration.t list;
- nfunresprms1:int;
- nfunresprms2:int;
- }
-
-
-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
-
-(* ?? prm_linked?? *)
-let isArg_stable x = match x with Arg_stable _ | Prm_arg _ -> true | _ -> false
-
-let is_stable x =
- match x with Arg_stable _ | Prm_stable _ | Prm_arg _ -> true | _ -> false
-
-let isArg_funres x = match x with Arg_funres -> true | _ -> false
-
-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)
-
-
-let error msg = user_err Pp.(str msg)
-
-(** {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 mib1.mind_finite == Decl_kinds.CoFinite then error "First argument is coinductive";
- if mib2.mind_finite == Decl_kinds.CoFinite then error "Second argument is coinductive";
- if not (Int.equal mib1.mind_ntypes 1) then error "First argument is mutual";
- if not (Int.equal mib2.mind_ntypes 1) then error "Second argument is mutual";
- ()
-
-(*
-(** [build_raw_params prms_decl avoid] returns a list of variables
- attributed to the list of decl [prms_decl], avoiding names in
- [avoid]. *)
-let build_raw_params prms_decl avoid =
- let dummy_constr = compose_prod (List.map (fun (x,_,z) -> x,z) prms_decl) (mkRel 1) in
- let _ = prNamedConstr "DUMMY" dummy_constr in
- let dummy_glob_constr = Detyping.detype false avoid [] dummy_constr in
- let _ = prNamedRConstr "RAWDUMMY" dummy_glob_constr in
- let res,_ = glob_decompose_prod dummy_glob_constr in
- let comblist = List.combine prms_decl res in
- comblist, res , (avoid @ (Id.Set.elements (ids_of_glob_constr dummy_glob_constr)))
-*)
-
-let ids_of_rawlist avoid rawl =
- List.fold_left Id.Set.union avoid (List.map ids_of_glob_constr rawl)
-
-
-
-(** {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 _ = prstr "\nYOUHOU shift\n" in
- let linked_targets = revlinked lnk2 in
- let is_param_of_mib1 x = x < mib1.mind_nparams_rec in
- let is_param_of_mib2 x = x < mib2.mind_nparams_rec in
- 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,acc4) x ->
- prstr (pr_merginfo mlnk.(i));prstr "\n";
- match mlnk.(i) with
- | Prm_stable _ -> x::acc1 , acc2 , acc3, acc4
- | Prm_arg _ -> acc1 , x::acc2 , acc3, acc4
- | Arg_stable _ -> acc1 , acc2 , x::acc3, acc4
- | Arg_funres -> acc1 , acc2 , acc3, x::acc4
- | _ -> acc1 , acc2 , acc3, acc4)
- ([],[],[],[]) arity_ctxt in
-(* let arity_ctxt2 =
- build_raw_params oib2.mind_arity_ctxt
- (Id.Set.elements (ids_of_glob_constr oib1.mind_arity_ctxt)) in*)
- let recprms1,otherprms1,args1,funresprms1 = bldprms (List.rev oib1.mind_arity_ctxt) mlnk1 in
- let _ = prstr "\n\n\n" in
- let recprms2,otherprms2,args2,funresprms2 = bldprms (List.rev oib2.mind_arity_ctxt) mlnk2 in
- let _ = prstr "\notherprms1:\n" in
- let _ =
- List.iter (fun decl -> prstr (string_of_name (RelDecl.get_name decl) ^ " : ");
- prconstr (RelDecl.get_type decl); prstr "\n")
- otherprms1 in
- let _ = prstr "\notherprms2:\n" in
- let _ =
- List.iter (fun decl -> prstr (string_of_name (RelDecl.get_name decl) ^ " : "); prconstr (RelDecl.get_type decl); prstr "\n")
- otherprms2 in
- {
- ident=id;
- mib1=mib1;
- oib1 = oib1;
- mib2=mib2;
- oib2 = oib2;
- lnk1 = mlnk1;
- lnk2 = mlnk2;
- nrecprms1 = n_params1;
- recprms1 = recprms1;
- otherprms1 = otherprms1;
- args1 = args1;
- funresprms1 = funresprms1;
- notherprms1 = Array.length mlnk1 - n_params1;
- nfunresprms1 = List.length funresprms1;
- nargs1 = List.length args1;
- nrecprms2 = n_params2;
- recprms2 = recprms2;
- otherprms2 = otherprms2;
- args2 = args2;
- funresprms2 = funresprms2;
- notherprms2 = Array.length mlnk2 - n_params2;
- nargs2 = List.length args2;
- nfunresprms2 = List.length funresprms2;
- }
-
-
-
-
-(** {1 Merging functions} *)
-
-exception NoMerge
-
-let rec merge_app c1 c2 id1 id2 shift filter_shift_stable =
- let lnk = Array.append shift.lnk1 shift.lnk2 in
- match CAst.(c1.v, c2.v) with
- | GApp(f1, arr1), GApp(f2,arr2) when isVarf id1 f1 && isVarf id2 f2 ->
- let _ = prstr "\nICI1!\n" in
- let args = filter_shift_stable lnk (arr1 @ arr2) in
- CAst.make @@ GApp ((CAst.make @@ GVar shift.ident) , args)
- | GApp(f1, arr1), GApp(f2,arr2) -> raise NoMerge
- | GLetIn(nme,bdy,typ,trm) , _ ->
- let _ = prstr "\nICI2!\n" in
- let newtrm = merge_app trm c2 id1 id2 shift filter_shift_stable in
- CAst.make @@ GLetIn(nme,bdy,typ,newtrm)
- | _, GLetIn(nme,bdy,typ,trm) ->
- let _ = prstr "\nICI3!\n" in
- let newtrm = merge_app c1 trm id1 id2 shift filter_shift_stable in
- CAst.make @@ GLetIn(nme,bdy,typ,newtrm)
- | _ -> let _ = prstr "\nICI4!\n" in
- raise NoMerge
-
-let rec merge_app_unsafe c1 c2 shift filter_shift_stable =
- let lnk = Array.append shift.lnk1 shift.lnk2 in
- match CAst.(c1.v, c2.v) with
- | GApp(f1, arr1), GApp(f2,arr2) ->
- let args = filter_shift_stable lnk (arr1 @ arr2) in
- CAst.make @@ GApp (CAst.make @@ GVar shift.ident, args)
- (* FIXME: what if the function appears in the body of the let? *)
- | GLetIn(nme,bdy,typ,trm) , _ ->
- let _ = prstr "\nICI2 '!\n" in
- let newtrm = merge_app_unsafe trm c2 shift filter_shift_stable in
- CAst.make @@ GLetIn(nme,bdy,typ,newtrm)
- | _, GLetIn(nme,bdy,typ,trm) ->
- let _ = prstr "\nICI3 '!\n" in
- let newtrm = merge_app_unsafe c1 trm shift filter_shift_stable in
- CAst.make @@ GLetIn(nme,bdy,typ,newtrm)
- | _ -> let _ = prstr "\nICI4 '!\n" in raise NoMerge
-
-
-
-(* Heuristic when merging two lists of hypothesis: merge every rec
- calls of branch 1 with all rec calls of branch 2. *)
-(* TODO: reecrire cette heuristique (jusqu'a merge_types) *)
-let rec merge_rec_hyps shift accrec
- (ltyp:(Name.t * glob_constr option * glob_constr option) list)
- filter_shift_stable : (Name.t * glob_constr option * glob_constr option) list =
- let mergeonehyp t reldecl =
- match reldecl with
- | (nme,x,Some ({ CAst.v = GApp(i,args)} as ind))
- -> nme,x, Some (merge_app_unsafe ind t shift filter_shift_stable)
- | (nme,Some _,None) -> error "letins with recursive calls not treated yet"
- | (nme,None,Some _) -> assert false
- | (nme,None,None) | (nme,Some _,Some _) -> assert false in
- match ltyp with
- | [] -> []
- | (nme,None,Some ({ CAst. v = GApp(f, largs) } as t)) :: lt when isVarf ind2name f ->
- let rechyps = List.map (mergeonehyp t) accrec in
- rechyps @ merge_rec_hyps shift accrec lt filter_shift_stable
- | e::lt -> e :: merge_rec_hyps shift accrec lt filter_shift_stable
-
-
-let build_suppl_reccall (accrec:(Name.t * glob_constr) list) concl2 shift =
- List.map (fun (nm,tp) -> (nm,merge_app_unsafe tp concl2 shift)) accrec
-
-
-let find_app (nme:Id.t) ltyp =
- try
- ignore
- (List.map
- (fun x ->
- match x with
- | _,None,Some { CAst.v = GApp(f,_)} when isVarf nme f -> raise (Found 0)
- | _ -> ())
- ltyp);
- false
- with Found _ -> true
-
-let prnt_prod_or_letin nm letbdy typ =
- match letbdy , typ with
- | Some lbdy , None -> prNamedRConstr ("(letin) " ^ string_of_name nm) lbdy
- | None , Some tp -> prNamedRConstr (string_of_name nm) tp
- | _ , _ -> assert false
-
-
-let rec merge_types shift accrec1
- (ltyp1:(Name.t * glob_constr option * glob_constr option) list)
- (concl1:glob_constr) (ltyp2:(Name.t * glob_constr option * glob_constr option) list) concl2
- : (Name.t * glob_constr option * glob_constr option) list * glob_constr =
- let _ = prstr "MERGE_TYPES\n" in
- let _ = prstr "ltyp 1 : " in
- let _ = List.iter (fun (nm,lbdy,tp) -> prnt_prod_or_letin nm lbdy tp) ltyp1 in
- let _ = prstr "\nltyp 2 : " in
- let _ = List.iter (fun (nm,lbdy,tp) -> prnt_prod_or_letin nm lbdy tp) ltyp2 in
- let _ = prstr "\n" in
- let res =
- match ltyp1 with
- | [] ->
- let isrec1 = not (List.is_empty accrec1) in
- let isrec2 = find_app ind2name ltyp2 in
- let rechyps =
- if isrec1 && isrec2
- then (* merge_rec_hyps shift accrec1 ltyp2 filter_shift_stable *)
- merge_rec_hyps shift [name_of_string "concl1",None,Some concl1] ltyp2
- filter_shift_stable_right
- @ merge_rec_hyps shift accrec1 [name_of_string "concl2",None, Some concl2]
- filter_shift_stable
- else if isrec1
- (* if rec calls in accrec1 and not in ltyp2, add one to ltyp2 *)
- then
- merge_rec_hyps shift accrec1
- (ltyp2@[name_of_string "concl2",None,Some concl2]) filter_shift_stable
- else if isrec2
- then merge_rec_hyps shift [name_of_string "concl1",None,Some concl1] ltyp2
- filter_shift_stable_right
- else ltyp2 in
- let _ = prstr"\nrechyps : " in
- let _ = List.iter(fun (nm,lbdy,tp)-> prnt_prod_or_letin nm lbdy tp) rechyps in
- let _ = prstr "MERGE CONCL : " in
- let _ = prNamedRConstr "concl1" concl1 in
- let _ = prstr " with " in
- 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,None, Some t1)as e ::lt1 ->
- (match t1.CAst.v with
- | GApp(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,None,Some t1) :: recres) , recconcl2)
- | (nme,Some bd, None) ::lt1 ->
- (* FIXME: what if ind1name appears in bd? *)
- let recres, recconcl2 =
- merge_types shift accrec1 lt1 concl1 ltyp2 concl2 in
- ((nme,Some bd,None) :: recres) , recconcl2
- | (_,None,None)::_ | (_,Some _,Some _)::_ -> assert false
- in
- res
-
-
-(** [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:Id.t array) (allargs2:Id.t array)
- (lnk:int merged_arg array) =
- Array.fold_left_i
- (fun i acc e ->
- if Int.equal i (Array.length lnk - 1) then acc (* functional arg, not in allargs *)
- else
- match e with
- | Prm_linked j | Arg_linked j -> Id.Map.add allargs2.(i) allargs1.(j) acc
- | _ -> acc)
- Id.Map.empty lnk
-
-let build_link_map allargs1 allargs2 lnk =
- let allargs1 =
- Array.of_list (List.rev_map (fun (x,_,_) -> id_of_name x) allargs1) in
- let allargs2 =
- Array.of_list (List.rev_map (fun (x,_,_) -> 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'(shifted) -> ...
- -> (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:glob_constr)
- (typcstr2:glob_constr) : glob_constr =
- (* 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 = glob_decompose_prod_or_letin_n nargs1 typcstr1 in
- let allargs2,rest2 = glob_decompose_prod_or_letin_n nargs2 typcstr2 in
- (* Build map of linked args of [typcstr2], and apply it to [typcstr2]. *)
- let linked_map = build_link_map allargs1 allargs2 shift.lnk2 in
- let rest2 = change_vars linked_map rest2 in
- let hyps1,concl1 = glob_decompose_prod_or_letin rest1 in
- let hyps2,concl2' = glob_decompose_prod_or_letin rest2 in
- let ltyp,concl2 =
- merge_types shift [] (List.rev hyps1) concl1 (List.rev hyps2) concl2' in
- let _ = prNamedRLDecl "ltyp result:" ltyp in
- let typ = glob_compose_prod_or_letin concl2 (List.rev ltyp) in
- let revargs1 =
- list_filteri (fun i _ -> isArg_stable shift.lnk1.(i)) (List.rev allargs1) in
- let _ = prNamedRLDecl "ltyp allargs1" allargs1 in
- let _ = prNamedRLDecl "ltyp revargs1" revargs1 in
- let revargs2 =
- list_filteri (fun i _ -> isArg_stable shift.lnk2.(i)) (List.rev allargs2) in
- let _ = prNamedRLDecl "ltyp allargs2" allargs2 in
- let _ = prNamedRLDecl "ltyp revargs2" revargs2 in
- let typwithprms =
- glob_compose_prod_or_letin 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:Id.t =
- let id = Id.to_string 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 glob_constr
- first, each of them having distinct var names. *)
-let merge_constructors (shift:merge_infos) (avoid:Id.Set.t)
- (typcstr1:(Id.t * glob_constr) list)
- (typcstr2:(Id.t * glob_constr) list) : (Id.t * glob_constr) list =
- List.flatten
- (List.map
- (fun (id1,rawtyp1) ->
- List.map
- (fun (id2,rawtyp2) ->
- let typ = merge_one_constructor shift rawtyp1 rawtyp2 in
- let newcstror_id = merge_constructor_id id1 id2 shift in
- let _ = prstr "\n**************\n" in
- newcstror_id , typ)
- typcstr2)
- typcstr1)
-
-(** [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 merge_inductive_body (shift:merge_infos) avoid (oib1:one_inductive_body)
- (oib2:one_inductive_body) =
- (* building glob_constr type of constructors *)
- let mkrawcor nme avoid typ =
- (* first replace rel 1 by a varname *)
- let substindtyp = substitterm 0 (mkRel 1) (mkVar nme) typ in
- let substindtyp = EConstr.of_constr substindtyp in
- Detyping.detype false (Id.Set.elements avoid) (Global.env()) Evd.empty substindtyp in
- let lcstr1: glob_constr list =
- Array.to_list (Array.map (mkrawcor ind1name avoid) oib1.mind_user_lc) in
- (* add to avoid all indentifiers of lcstr1 *)
- let avoid2 = Id.Set.union avoid (ids_of_rawlist avoid lcstr1) in
- let lcstr2 =
- Array.to_list (Array.map (mkrawcor ind2name avoid2) oib2.mind_user_lc) in
- let avoid3 = Id.Set.union avoid (ids_of_rawlist avoid lcstr2) in
-
- let params1 =
- try fst (glob_decompose_prod_n shift.nrecprms1 (List.hd lcstr1))
- with e when CErrors.noncritical e -> [] in
- let params2 =
- try fst (glob_decompose_prod_n shift.nrecprms2 (List.hd lcstr2))
- with e when CErrors.noncritical e -> [] 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();
- params1,params2,merge_constructors shift avoid3 lcstr1 lcstr2
-
-
-(** [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 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. *)
- merge_inductive_body shift Id.Set.empty mib1.mind_packets.(0) mib2.mind_packets.(0)
-
-
-let glob_constr_to_constr_expr x = (* build a constr_expr from a glob_constr *)
- Flags.with_option Flags.raw_print (Constrextern.extern_glob_type Id.Set.empty) x
-
-let merge_rec_params_and_arity prms1 prms2 shift (concl:constr) =
- let params = prms2 @ prms1 in
- let resparams =
- List.fold_left
- (fun acc (nme,tp) ->
- let _ = prstr "param :" in
- let _ = prNamedRConstr (string_of_name nme) tp in
- let _ = prstr " ; " in
- let typ = glob_constr_to_constr_expr tp in
- CLocalAssum ([(Loc.tag nme)], Constrexpr_ops.default_binder_kind, typ) :: acc)
- [] params in
- let concl = Constrextern.extern_constr false (Global.env()) Evd.empty concl in
- let arity,_ =
- List.fold_left
- (fun (acc,env) decl ->
- let nm = Context.Rel.Declaration.get_name decl in
- let c = RelDecl.get_type decl in
- let typ = Constrextern.extern_constr false env Evd.empty c in
- let newenv = Environ.push_rel (LocalAssum (nm,c)) env in
- CAst.make @@ CProdN ([[(Loc.tag nm)],Constrexpr_ops.default_binder_kind,typ] , acc) , newenv)
- (concl,Global.env())
- (shift.funresprms2 @ shift.funresprms1
- @ shift.args2 @ shift.args1 @ shift.otherprms2 @ shift.otherprms1) in
- resparams,arity
-
-
-
-(** [glob_constr_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 glob_constr_list_to_inductive_expr prms1 prms2 mib1 mib2 shift
- (rawlist:(Id.t * glob_constr) list) =
- let lident = (Loc.tag shift.ident), None in
- let bindlist , cstr_expr = (* params , arities *)
- merge_rec_params_and_arity prms1 prms2 shift mkSet in
- let lcstor_expr : (bool * (lident * constr_expr)) list =
- List.map (* zeta_normalize t ? *)
- (fun (id,t) -> false, ((Loc.tag id),glob_constr_to_constr_expr t))
- rawlist in
- lident , bindlist , Some cstr_expr , lcstor_expr
-
-
-let mkProd_reldecl (rdecl:Context.Rel.Declaration.t) (t2:glob_constr) =
- match rdecl with
- | LocalAssum (nme,t) ->
- let t = EConstr.of_constr t in
- let traw = Detyping.detype false [] (Global.env()) Evd.empty t in
- CAst.make @@ GProd (nme,Explicit,traw,t2)
- | LocalDef _ -> assert false
-
-
-(** [merge_inductive ind1 ind2 lnk] merges two graphs, linking
- variables specified in [lnk]. Graphs are not supposed to be mutual
- inductives for the moment. *)
-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 prms1,prms2, rawlist = merge_mutual_inductive_body mib1 mib2 shift_prm in
- let _ = prstr "\nrawlist : " in
- let _ =
- List.iter (fun (nm,tp) -> prNamedRConstr (Id.to_string nm) tp;prstr "\n") rawlist in
- let _ = prstr "\nend rawlist\n" in
-(* FIX: retransformer en constr ici
- let shift_prm =
- { shift_prm with
- recprms1=prms1;
- recprms1=prms1;
- } in *)
- let indexpr = glob_constr_list_to_inductive_expr prms1 prms2 mib1 mib2 shift_prm rawlist in
- (* Declare inductive *)
- let indl,_,_ = Command.extract_mutual_inductive_declaration_components [(indexpr,[])] in
- let mie,pl,impls = Command.interp_mutual_inductive indl []
- false (* non-cumulative *) false (*FIXMEnon-poly *) false (* means not private *) Decl_kinds.Finite (* means: not coinductive *) in
- (* Declare the mutual inductive block with its associated schemes *)
- ignore (Command.declare_mutual_inductive_with_eliminations mie pl impls)
-
-
-(* Find infos on identifier id. *)
-let find_Function_infos_safe (id:Id.t): Indfun_common.function_info =
- let kn_of_id x =
- let f_ref = Libnames.Ident (Loc.tag x) in
- locate_with_msg (str "Don't know what to do with " ++ Libnames.pr_reference f_ref)
- locate_constant f_ref in
- try find_Function_infos (kn_of_id id)
- with Not_found ->
- user_err ~hdr:"indfun" (Id.print id ++ str " has no functional scheme")
-
-(** [merge id1 id2 args1 args2 id] builds and declares a new inductive
- type called [id], representing the merged graphs of both graphs
- [ind1] and [ind2]. identifiers occurring in both arrays [args1] and
- [args2] are considered linked (i.e. are the same variable) in the
- new graph.
-
- Warning: For the moment, repetitions of an id in [args1] or
- [args2] are not supported. *)
-let merge (id1:Id.t) (id2:Id.t) (args1:Id.t array)
- (args2:Id.t array) id : unit =
- let finfo1 = find_Function_infos_safe id1 in
- let finfo2 = find_Function_infos_safe id2 in
- (* FIXME? args1 are supposed unlinked. mergescheme (G x x) ?? *)
- (* We add one arg (functional arg of the graph) *)
- let lnk1 = Array.make (Array.length args1 + 1) Unlinked in
- let lnk2' = (* args2 may be linked to args1 members. FIXME: same
- as above: vars may be linked inside args2?? *)
- Array.mapi
- (fun i c ->
- match Array.findi (fun i x -> Id.equal x c) args1 with
- | Some j -> Linked j
- | None -> Unlinked)
- args2 in
- (* We add one arg (functional arg of the graph) *)
- let lnk2 = Array.append lnk2' (Array.make 1 Unlinked) in
- (* setting functional results *)
- let _ = lnk1.(Array.length lnk1 - 1) <- Funres in
- let _ = lnk2.(Array.length lnk2 - 1) <- Funres in
- merge_inductive finfo1.graph_ind finfo2.graph_ind lnk1 lnk2 id
-
-
-let remove_last_arg c =
- let (x,y) = decompose_prod c in
- let xnolast = List.rev (List.tl (List.rev x)) in
- compose_prod xnolast y
-
-let rec remove_n_fst_list n l = if Int.equal n 0 then l else remove_n_fst_list (n-1) (List.tl l)
-let remove_n_last_list n l = List.rev (remove_n_fst_list n (List.rev l))
-
-let remove_last_n_arg n c =
- let (x,y) = decompose_prod c in
- let xnolast = remove_n_last_list n x in
- compose_prod xnolast y
-
-(* [funify_branches relinfo nfuns branch] returns the branch [branch]
- of the relinfo [relinfo] modified to fit in a functional principle.
- Things to do:
- - remove indargs from rel applications
- - replace *variables only* corresponding to function (recursive)
- results by the actual function application. *)
-let funify_branches relinfo nfuns branch =
- let mut_induct, induct =
- match relinfo.indref with
- | None -> assert false
- | Some (IndRef ((mutual_ind,i) as ind)) -> mutual_ind,ind
- | _ -> assert false in
- let is_dom c =
- match kind_of_term c with
- | Ind(((u,_),_)) | Construct(((u,_),_),_) -> MutInd.equal u mut_induct
- | _ -> false in
- let _dom_i c =
- assert (is_dom c);
- match kind_of_term c with
- | Ind((u,i)) | Construct((u,_),i) -> i
- | _ -> assert false in
- let _is_pred c shift =
- match kind_of_term c with
- | Rel i -> let reali = i-shift in (reali>=0 && reali<relinfo.nbranches)
- | _ -> false in
- (* FIXME: *)
- LocalDef (Anonymous,EConstr.mkProp,EConstr.mkProp)
-
-
-let relprinctype_to_funprinctype relprinctype nfuns =
- let relprinctype = EConstr.of_constr relprinctype in
- let relinfo = compute_elim_sig Evd.empty (** FIXME*) relprinctype in
- assert (not relinfo.farg_in_concl);
- assert (relinfo.indarg_in_concl);
- (* first remove indarg and indarg_in_concl *)
- let relinfo_noindarg = { relinfo with
- indarg_in_concl = false; indarg = None;
- concl = EConstr.of_constr (remove_last_arg (pop (EConstr.Unsafe.to_constr relinfo.concl))); } in
- (* the nfuns last induction arguments are functional ones: remove them *)
- let relinfo_argsok = { relinfo_noindarg with
- nargs = relinfo_noindarg.nargs - nfuns;
- (* args is in reverse order, so remove fst *)
- args = remove_n_fst_list nfuns relinfo_noindarg.args;
- concl = EConstr.of_constr (popn nfuns (EConstr.Unsafe.to_constr relinfo_noindarg.concl));
- } in
- let new_branches =
- List.map (funify_branches relinfo_argsok nfuns) relinfo_argsok.branches in
- let relinfo_branches = { relinfo_argsok with branches = new_branches } in
- relinfo_branches
-
-(* @article{ bundy93rippling,
- author = "Alan Bundy and Andrew Stevens and Frank van Harmelen and Andrew Ireland and Alan Smaill",
- 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" }
-
- *)
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 1705cac789..7298342e1e 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1,16 +1,17 @@
(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
-open API
module CVars = Vars
-open Term
+open Constr
open EConstr
open Vars
open Namegen
@@ -36,7 +37,7 @@ open Glob_term
open Pretyping
open Termops
open Constrintern
-open Misctypes
+open Tactypes
open Genredexpr
open Equality
@@ -48,29 +49,33 @@ open Context.Rel.Declaration
(* Ugly things which should not be here *)
-let coq_constant m s = EConstr.of_constr @@ Universes.constr_of_global @@
+let coq_constant m s = EConstr.of_constr @@ UnivGen.constr_of_global @@
Coqlib.coq_reference "RecursiveDefinition" m s
let arith_Nat = ["Arith";"PeanoNat";"Nat"]
let arith_Lt = ["Arith";"Lt"]
+let pr_leconstr_rd =
+ let sigma, env = Pfedit.get_current_context () in
+ Printer.pr_leconstr_env env sigma
+
let coq_init_constant s =
EConstr.of_constr (
- Universes.constr_of_global @@
+ UnivGen.constr_of_global @@
Coqlib.gen_reference_in_modules "RecursiveDefinition" Coqlib.init_modules s)
let find_reference sl s =
let dp = Names.DirPath.make (List.rev_map Id.of_string sl) in
locate (make_qualid dp (Id.of_string s))
-let declare_fun f_id kind ?(ctx=Univ.UContext.empty) value =
- let ce = definition_entry ~univs:ctx value (*FIXME *) in
+let declare_fun f_id kind ?univs value =
+ let ce = definition_entry ?univs value (*FIXME *) in
ConstRef(declare_constant f_id (DefinitionEntry ce, kind));;
-let defined () = Lemmas.save_proof (Vernacexpr.(Proved (Transparent,None)))
+let defined () = Lemmas.save_proof (Vernacexpr.(Proved (Proof_global.Transparent,None)))
let def_of_const t =
- match (kind_of_term t) with
+ match (Constr.kind t) with
Const sp ->
(try (match constant_opt_value_in (Global.env ()) sp with
| Some c -> c
@@ -90,7 +95,7 @@ let type_of_const sigma t =
|_ -> assert false
let constr_of_global x =
- fst (Universes.unsafe_constr_of_global x)
+ fst (Global.constr_of_global_in_context (Global.env ()) x)
let constant sl s = constr_of_global (find_reference sl s)
@@ -101,12 +106,12 @@ let const_of_ref = function
let nf_zeta env =
Reductionops.clos_norm_flags (CClosure.RedFlags.mkflags [CClosure.RedFlags.fZETA])
- env
- Evd.empty
+ env (Evd.from_env env)
let nf_betaiotazeta = (* Reductionops.local_strong Reductionops.whd_betaiotazeta *)
- Reductionops.clos_norm_flags CClosure.betaiotazeta Environ.empty_env Evd.empty
+ Reductionops.clos_norm_flags CClosure.betaiotazeta Environ.empty_env
+ (Evd.from_env Environ.empty_env)
@@ -116,13 +121,17 @@ let nf_betaiotazeta = (* Reductionops.local_strong Reductionops.whd_betaiotazeta
(* Generic values *)
let pf_get_new_ids idl g =
let ids = pf_ids_of_hyps g in
+ let ids = Id.Set.of_list ids in
List.fold_right
- (fun id acc -> next_global_ident_away id (acc@ids)::acc)
+ (fun id acc -> next_global_ident_away id (Id.Set.union (Id.Set.of_list acc) ids)::acc)
idl
[]
+let next_ident_away_in_goal ids avoid =
+ next_ident_away_in_goal ids (Id.Set.of_list avoid)
+
let compute_renamed_type gls c =
- rename_bound_vars_as_displayed (project gls) (*no avoid*) [] (*no rels*) []
+ rename_bound_vars_as_displayed (project gls) (*no avoid*) Id.Set.empty (*no rels*) []
(pf_unsafe_type_of gls c)
let h'_id = Id.of_string "h'"
let teq_id = Id.of_string "teq"
@@ -134,13 +143,13 @@ let def_id = Id.of_string "def"
let p_id = Id.of_string "p"
let rec_res_id = Id.of_string "rec_res";;
let lt = function () -> (coq_init_constant "lt")
-let le = function () -> (coq_init_constant "le")
+let le = function () -> (Coqlib.gen_reference_in_modules "RecursiveDefinition" Coqlib.init_modules "le")
let ex = function () -> (coq_init_constant "ex")
let nat = function () -> (coq_init_constant "nat")
let iter_ref () =
try find_reference ["Recdef"] "iter"
with Not_found -> user_err Pp.(str "module Recdef not loaded")
-let iter = function () -> (constr_of_global (delayed_force iter_ref))
+let iter_rd = function () -> (constr_of_global (delayed_force iter_ref))
let eq = function () -> (coq_init_constant "eq")
let le_lt_SS = function () -> (constant ["Recdef"] "le_lt_SS")
let le_lt_n_Sm = function () -> (coq_constant arith_Lt "le_lt_n_Sm")
@@ -172,8 +181,9 @@ let simpl_iter clause =
clause
(* Others ugly things ... *)
-let (value_f:Term.constr list -> global_reference -> Term.constr) =
+let (value_f: Constr.t list -> GlobRef.t -> Constr.t) =
let open Term in
+ let open Constr in
fun al fterm ->
let rev_x_id_l =
(
@@ -191,20 +201,21 @@ let (value_f:Term.constr list -> global_reference -> Term.constr) =
in
let env = Environ.push_rel_context context (Global.env ()) in
let glob_body =
- CAst.make @@
+ DAst.make @@
GCases
(RegularStyle,None,
- [CAst.make @@ GApp(CAst.make @@ GRef(fterm,None), List.rev_map (fun x_id -> CAst.make @@ GVar x_id) rev_x_id_l),
+ [DAst.make @@ GApp(DAst.make @@ GRef(fterm,None), List.rev_map (fun x_id -> DAst.make @@ GVar x_id) rev_x_id_l),
(Anonymous,None)],
- [Loc.tag ([v_id], [CAst.make @@ PatCstr ((destIndRef (delayed_force coq_sig_ref),1),
- [CAst.make @@ PatVar(Name v_id); CAst.make @@ PatVar Anonymous],
+ [CAst.make ([v_id], [DAst.make @@ PatCstr ((destIndRef (delayed_force coq_sig_ref),1),
+ [DAst.make @@ PatVar(Name v_id); DAst.make @@ PatVar Anonymous],
Anonymous)],
- CAst.make @@ GVar v_id)])
+ DAst.make @@ GVar v_id)])
in
let body = fst (understand env (Evd.from_env env) glob_body)(*FIXME*) in
+ let body = EConstr.Unsafe.to_constr body in
it_mkLambda_or_LetIn body context
-let (declare_f : Id.t -> logical_kind -> Term.constr list -> global_reference -> global_reference) =
+let (declare_f : Id.t -> logical_kind -> Constr.t list -> GlobRef.t -> GlobRef.t) =
fun f_id kind input_type fterm_ref ->
declare_fun f_id kind (value_f input_type fterm_ref);;
@@ -332,7 +343,8 @@ let check_not_nested sigma forbidden e =
try
check_not_nested e
with UserError(_,p) ->
- user_err ~hdr:"_" (str "on expr : " ++ Printer.pr_leconstr e ++ str " " ++ p)
+ let _, env = Pfedit.get_current_context () in
+ user_err ~hdr:"_" (str "on expr : " ++ Printer.pr_leconstr_env env sigma e ++ str " " ++ p)
(* ['a info] contains the local information for traveling *)
type 'a infos =
@@ -344,7 +356,7 @@ type 'a infos =
f_id : Id.t; (* function name *)
f_constr : constr; (* function term *)
f_terminate : constr; (* termination proof term *)
- func : global_reference; (* functional reference *)
+ func : GlobRef.t; (* functional reference *)
info : 'a;
is_main_branch : bool; (* on the main branch or on a matched expression *)
is_final : bool; (* final first order term or not *)
@@ -450,7 +462,7 @@ let rec travel_aux jinfo continuation_tac (expr_info:constr infos) g =
check_not_nested sigma (expr_info.f_id::expr_info.forbidden_ids) expr_info.info;
jinfo.otherS () expr_info continuation_tac expr_info g
with e when CErrors.noncritical e ->
- user_err ~hdr:"Recdef.travel" (str "the term " ++ Printer.pr_leconstr expr_info.info ++ str " can not contain a recursive call to " ++ Id.print expr_info.f_id)
+ user_err ~hdr:"Recdef.travel" (str "the term " ++ Printer.pr_leconstr_env (pf_env g) sigma expr_info.info ++ str " can not contain a recursive call to " ++ Id.print expr_info.f_id)
end
| Lambda(n,t,b) ->
begin
@@ -458,7 +470,7 @@ let rec travel_aux jinfo continuation_tac (expr_info:constr infos) g =
check_not_nested sigma (expr_info.f_id::expr_info.forbidden_ids) expr_info.info;
jinfo.otherS () expr_info continuation_tac expr_info g
with e when CErrors.noncritical e ->
- user_err ~hdr:"Recdef.travel" (str "the term " ++ Printer.pr_leconstr expr_info.info ++ str " can not contain a recursive call to " ++ Id.print expr_info.f_id)
+ user_err ~hdr:"Recdef.travel" (str "the term " ++ Printer.pr_leconstr_env (pf_env g) sigma expr_info.info ++ str " can not contain a recursive call to " ++ Id.print expr_info.f_id)
end
| Case(ci,t,a,l) ->
begin
@@ -486,8 +498,8 @@ let rec travel_aux jinfo continuation_tac (expr_info:constr infos) g =
jinfo.apP (f,args) expr_info continuation_tac in
travel_args jinfo
expr_info.is_main_branch new_continuation_tac new_infos g
- | Case _ -> user_err ~hdr:"Recdef.travel" (str "the term " ++ Printer.pr_leconstr expr_info.info ++ str " can not contain an applied match (See Limitation in Section 2.3 of refman)")
- | _ -> anomaly (Pp.str "travel_aux : unexpected "++ Printer.pr_leconstr expr_info.info ++ Pp.str ".")
+ | Case _ -> user_err ~hdr:"Recdef.travel" (str "the term " ++ Printer.pr_leconstr_env (pf_env g) sigma expr_info.info ++ str " can not contain an applied match (See Limitation in Section 2.3 of refman)")
+ | _ -> anomaly (Pp.str "travel_aux : unexpected "++ Printer.pr_leconstr_env (pf_env g) sigma expr_info.info ++ Pp.str ".")
end
| Cast(t,_,_) -> travel jinfo continuation_tac {expr_info with info=t} g
| Const _ | Var _ | Meta _ | Evar _ | Sort _ | Construct _ | Ind _ ->
@@ -510,7 +522,7 @@ and travel_args jinfo is_final continuation_tac infos =
{infos with info=arg;is_final=false}
and travel jinfo continuation_tac expr_info =
observe_tac
- (str jinfo.message ++ Printer.pr_leconstr expr_info.info)
+ (str jinfo.message ++ pr_leconstr_rd expr_info.info)
(travel_aux jinfo continuation_tac expr_info)
(* Termination proof *)
@@ -726,7 +738,7 @@ let terminate_case next_step (ci,a,t,l) expr_info continuation_tac infos g =
let destruct_tac,rev_to_thin_intro =
mkDestructEq [expr_info.rec_arg_id] a' g in
let to_thin_intro = List.rev rev_to_thin_intro in
- observe_tac (str "treating cases (" ++ int (Array.length l) ++ str")" ++ spc () ++ Printer.pr_leconstr a')
+ observe_tac (str "treating cases (" ++ int (Array.length l) ++ str")" ++ spc () ++ Printer.pr_leconstr_env (pf_env g) sigma a')
(try
(tclTHENS
destruct_tac
@@ -735,7 +747,7 @@ let terminate_case next_step (ci,a,t,l) expr_info continuation_tac infos g =
with
| UserError(Some "Refiner.thensn_tac3",_)
| UserError(Some "Refiner.tclFAIL_s",_) ->
- (observe_tac (str "is computable " ++ Printer.pr_leconstr new_info.info) (next_step continuation_tac {new_info with info = nf_betaiotazeta new_info.info} )
+ (observe_tac (str "is computable " ++ Printer.pr_leconstr_env (pf_env g) sigma new_info.info) (next_step continuation_tac {new_info with info = nf_betaiotazeta new_info.info} )
))
g
@@ -848,9 +860,13 @@ let rec prove_le g =
Proofview.V82.of_tactic (apply (delayed_force le_n));
begin
try
- let matching_fun =
- pf_is_matching g
- (Pattern.PApp(Pattern.PRef (Globnames.global_of_constr (EConstr.Unsafe.to_constr (le ()))),[|Pattern.PVar (destVar sigma x);Pattern.PMeta None|])) in
+ let matching_fun c = match EConstr.kind sigma c with
+ | App (c, [| x0 ; _ |]) ->
+ EConstr.isVar sigma x0 &&
+ Id.equal (destVar sigma x0) (destVar sigma x) &&
+ EConstr.is_global sigma (le ()) c
+ | _ -> false
+ in
let (h,t) = List.find (fun (_,t) -> matching_fun t) (pf_hyps_types g)
in
let y =
@@ -883,8 +899,8 @@ let rec make_rewrite_list expr_info max = function
Proofview.V82.of_tactic (general_rewrite_bindings false Locus.AllOccurrences
true (* dep proofs also: *) true
(mkVar hp,
- ExplicitBindings[Loc.tag @@ (NamedHyp def, expr_info.f_constr);
- Loc.tag @@ (NamedHyp k, f_S max)]) false) g) )
+ ExplicitBindings[CAst.make @@ (NamedHyp def, expr_info.f_constr);
+ CAst.make @@ (NamedHyp k, f_S max)]) false) g) )
)
[make_rewrite_list expr_info max l;
observe_tclTHENLIST (str "make_rewrite_list")[ (* x < S max proof *)
@@ -910,8 +926,8 @@ let make_rewrite expr_info l hp max =
(Proofview.V82.of_tactic (general_rewrite_bindings false Locus.AllOccurrences
true (* dep proofs also: *) true
(mkVar hp,
- ExplicitBindings[Loc.tag @@ (NamedHyp def, expr_info.f_constr);
- Loc.tag @@ (NamedHyp k, f_S (f_S max))]) false)) g)
+ ExplicitBindings[CAst.make @@ (NamedHyp def, expr_info.f_constr);
+ CAst.make @@ (NamedHyp k, f_S (f_S max))]) false)) g)
[observe_tac(str "make_rewrite finalize") (
(* tclORELSE( h_reflexivity) *)
(observe_tclTHENLIST (str "make_rewrite")[
@@ -986,11 +1002,11 @@ let rec intros_values_eq expr_info acc =
let equation_others _ expr_info continuation_tac infos =
if expr_info.is_final && expr_info.is_main_branch
then
- observe_tac (str "equation_others (cont_tac +intros) " ++ Printer.pr_leconstr expr_info.info)
+ observe_tac (str "equation_others (cont_tac +intros) " ++ pr_leconstr_rd expr_info.info)
(tclTHEN
(continuation_tac infos)
- (observe_tac (str "intros_values_eq equation_others " ++ Printer.pr_leconstr expr_info.info) (intros_values_eq expr_info [])))
- else observe_tac (str "equation_others (cont_tac) " ++ Printer.pr_leconstr expr_info.info) (continuation_tac infos)
+ (observe_tac (str "intros_values_eq equation_others " ++ pr_leconstr_rd expr_info.info) (intros_values_eq expr_info [])))
+ else observe_tac (str "equation_others (cont_tac) " ++ pr_leconstr_rd expr_info.info) (continuation_tac infos)
let equation_app f_and_args expr_info continuation_tac infos =
if expr_info.is_final && expr_info.is_main_branch
@@ -1036,11 +1052,12 @@ let prove_eq = travel equation_info
*)
let compute_terminate_type nb_args func =
let open Term in
+ let open Constr in
let open CVars in
let _,a_arrow_b,_ = destLambda(def_of_const (constr_of_global func)) in
let rev_args,b = decompose_prod_n nb_args a_arrow_b in
let left =
- mkApp(delayed_force iter,
+ mkApp(delayed_force iter_rd,
Array.of_list
(lift 5 a_arrow_b:: mkRel 3::
constr_of_global func::mkRel 1::
@@ -1135,7 +1152,7 @@ let termination_proof_header is_mes input_type ids args_id relation
tclTHEN (Proofview.V82.of_tactic (Tactics.generalize [mkVar id])) (Proofview.V82.of_tactic (clear [id])))
))
;
- observe_tac (str "fix") (Proofview.V82.of_tactic (fix (Some hrec) (nargs+1)));
+ observe_tac (str "fix") (Proofview.V82.of_tactic (fix hrec (nargs+1)));
h_intros args_id;
Proofview.V82.of_tactic (Simple.intro wf_rec_arg);
observe_tac (str "tac") (tac wf_rec_arg hrec wf_rec_arg acc_inv)
@@ -1219,12 +1236,12 @@ let whole_start (concl_tac:tactic) nb_args is_mes func input_type relation rec_a
let get_current_subgoals_types () =
let p = Proof_global.give_me_the_proof () in
- let { Evd.it=sgs ; sigma=sigma } = Proof.V82.subgoals p in
- sigma, List.map (Goal.V82.abstract_type sigma) sgs
+ let sgs,_,_,_,sigma = Proof.proof p in
+ sigma, List.map (Goal.V82.abstract_type sigma) sgs
exception EmptySubgoals
let build_and_l sigma l =
- let and_constr = Universes.constr_of_global @@ Coqlib.build_coq_and () in
+ let and_constr = UnivGen.constr_of_global @@ Coqlib.build_coq_and () in
let conj_constr = coq_conj () in
let mk_and p1 p2 =
mkApp(EConstr.of_constr and_constr,[|p1;p2|]) in
@@ -1289,9 +1306,9 @@ let build_new_goal_type () =
let is_opaque_constant c =
let cb = Global.lookup_constant c in
match cb.Declarations.const_body with
- | Declarations.OpaqueDef _ -> Vernacexpr.Opaque None
- | Declarations.Undef _ -> Vernacexpr.Opaque None
- | Declarations.Def _ -> Vernacexpr.Transparent
+ | Declarations.OpaqueDef _ -> Proof_global.Opaque
+ | Declarations.Undef _ -> Proof_global.Opaque
+ | Declarations.Def _ -> Proof_global.Transparent
let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decompose_and_tac,nb_goal) =
(* Pp.msgnl (str "gls_type := " ++ Printer.pr_lconstr gls_type); *)
@@ -1303,12 +1320,12 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp
with e when CErrors.noncritical e ->
anomaly (Pp.str "open_new_goal with an unamed theorem.")
in
- let na = next_global_ident_away name [] in
+ let na = next_global_ident_away name Id.Set.empty in
if Termops.occur_existential sigma gls_type then
CErrors.user_err Pp.(str "\"abstract\" cannot handle existentials");
let hook _ _ =
let opacity =
- let na_ref = Libnames.Ident (Loc.tag na) in
+ let na_ref = qualid_of_ident na in
let na_global = Smartlocate.global_with_alias na_ref in
match na_global with
ConstRef c -> is_opaque_constant c
@@ -1386,7 +1403,7 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp
(fun c ->
Proofview.V82.of_tactic (Tacticals.New.tclTHENLIST
[intros;
- Simple.apply (EConstr.of_constr (fst (interp_constr (Global.env()) Evd.empty c))) (*FIXME*);
+ Simple.apply (fst (interp_constr (Global.env()) Evd.empty c)) (*FIXME*);
Tacticals.New.tclCOMPLETE Auto.default_auto
])
)
@@ -1413,7 +1430,7 @@ let com_terminate
nb_args ctx
hook =
let start_proof ctx (tac_start:tactic) (tac_end:tactic) =
- let (evmap, env) = Lemmas.get_current_context() in
+ let evd, env = Pfedit.get_current_context () in
Lemmas.start_proof thm_name
(Global, false (* FIXME *), Proof Lemma) ~sign:(Environ.named_context_val env)
ctx (EConstr.of_constr (compute_terminate_type nb_args fonctional_ref)) hook;
@@ -1439,7 +1456,7 @@ let com_terminate
-let start_equation (f:global_reference) (term_f:global_reference)
+let start_equation (f:GlobRef.t) (term_f:GlobRef.t)
(cont_tactic:Id.t list -> tactic) g =
let sigma = project g in
let ids = pf_ids_of_hyps g in
@@ -1456,8 +1473,8 @@ let start_equation (f:global_reference) (term_f:global_reference)
observe_tac (str "prove_eq") (cont_tactic x)]) g;;
let (com_eqn : int -> Id.t ->
- global_reference -> global_reference -> global_reference
- -> Term.constr -> unit) =
+ GlobRef.t -> GlobRef.t -> GlobRef.t
+ -> Constr.t -> unit) =
fun nb_arg eq_name functional_ref f_ref terminate_ref equation_lemma_type ->
let open CVars in
let opacity =
@@ -1465,13 +1482,13 @@ let (com_eqn : int -> Id.t ->
| ConstRef c -> is_opaque_constant c
| _ -> anomaly ~label:"terminate_lemma" (Pp.str "not a constant.")
in
- let (evmap, env) = Lemmas.get_current_context() in
- let evmap = Evd.from_ctx (Evd.evar_universe_context evmap) in
+ let evd, env = Pfedit.get_current_context () in
+ let evd = Evd.from_ctx (Evd.evar_universe_context evd) in
let f_constr = constr_of_global f_ref in
let equation_lemma_type = subst1 f_constr equation_lemma_type in
(Lemmas.start_proof eq_name (Global, false, Proof Lemma)
~sign:(Environ.named_context_val env)
- evmap
+ evd
(EConstr.of_constr equation_lemma_type)
(Lemmas.mk_hook (fun _ _ -> ()));
ignore (by
@@ -1511,18 +1528,17 @@ let (com_eqn : int -> Id.t ->
let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num eq
generate_induction_principle using_lemmas : unit =
let open Term in
+ let open Constr in
let open CVars in
let env = Global.env() in
- let evd = ref (Evd.from_env env) in
- let function_type = interp_type_evars env evd type_of_f in
- let function_type = EConstr.Unsafe.to_constr function_type in
- let env = push_named (Context.Named.Declaration.LocalAssum (function_name,function_type)) env in
+ let evd = Evd.from_env env in
+ let evd, function_type = interp_type_evars env evd type_of_f in
+ let env = EConstr.push_named (Context.Named.Declaration.LocalAssum (function_name,function_type)) env in
(* Pp.msgnl (str "function type := " ++ Printer.pr_lconstr function_type); *)
- let ty = interp_type_evars env evd ~impls:rec_impls eq in
- let ty = EConstr.Unsafe.to_constr ty in
- let evm, nf = Evarutil.nf_evars_and_universes !evd in
- let equation_lemma_type = nf_betaiotazeta (EConstr.of_constr (nf ty)) in
- let function_type = nf function_type in
+ let evd, ty = interp_type_evars env evd ~impls:rec_impls eq in
+ let evd = Evd.minimize_universes evd in
+ let equation_lemma_type = nf_betaiotazeta (Evarutil.nf_evar evd ty) in
+ let function_type = EConstr.to_constr ~abort_on_undefined_evars:false evd function_type in
let equation_lemma_type = EConstr.Unsafe.to_constr equation_lemma_type in
(* Pp.msgnl (str "lemma type := " ++ Printer.pr_lconstr equation_lemma_type ++ fnl ()); *)
let res_vars,eq' = decompose_prod equation_lemma_type in
@@ -1533,7 +1549,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
(* Pp.msgnl (str "res_var :=" ++ Printer.pr_lconstr_env (push_rel_context (List.map (function (x,t) -> (x,None,t)) res_vars) env) eq'); *)
(* Pp.msgnl (str "rec_arg_num := " ++ str (string_of_int rec_arg_num)); *)
(* Pp.msgnl (str "eq' := " ++ str (string_of_int rec_arg_num)); *)
- match kind_of_term eq' with
+ match Constr.kind eq' with
| App(e,[|_;_;eq_fix|]) ->
mkLambda (Name function_name,function_type,subst_var function_name (compose_lam res_vars eq_fix))
| _ -> failwith "Recursive Definition (res not eq)"
@@ -1544,21 +1560,24 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
let equation_id = add_suffix function_name "_equation" in
let functional_id = add_suffix function_name "_F" in
let term_id = add_suffix function_name "_terminate" in
- let functional_ref = declare_fun functional_id (IsDefinition Decl_kinds.Definition) ~ctx:(snd (Evd.universe_context evm)) res in
+ let functional_ref =
+ let univs = Entries.Monomorphic_const_entry (Evd.universe_context_set evd) in
+ declare_fun functional_id (IsDefinition Decl_kinds.Definition) ~univs res
+ in
(* Refresh the global universes, now including those of _F *)
- let evm = Evd.from_env (Global.env ()) in
+ let evd = Evd.from_env (Global.env ()) in
let env_with_pre_rec_args = push_rel_context(List.map (function (x,t) -> LocalAssum (x,t)) pre_rec_args) env in
let relation, evuctx =
- interp_constr env_with_pre_rec_args evm r
+ interp_constr env_with_pre_rec_args evd r
in
- let evm = Evd.from_ctx evuctx in
+ let evd = Evd.from_ctx evuctx in
let tcc_lemma_name = add_suffix function_name "_tcc" in
let tcc_lemma_constr = ref Undefined in
(* let _ = Pp.msgnl (str "relation := " ++ Printer.pr_lconstr_env env_with_pre_rec_args relation) in *)
let hook _ _ =
let term_ref = Nametab.locate (qualid_of_ident term_id) in
let f_ref = declare_f function_name (IsProof Lemma) arg_types term_ref in
- let _ = Extraction_plugin.Table.extraction_inline true [Ident (Loc.tag term_id)] in
+ let _ = Extraction_plugin.Table.extraction_inline true [qualid_of_ident term_id] in
(* message "start second proof"; *)
let stop =
try com_eqn (List.length res_vars) equation_id functional_ref f_ref term_ref (subst_var function_name equation_lemma_type);
@@ -1581,7 +1600,9 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
and functional_ref = destConst (constr_of_global functional_ref)
and eq_ref = destConst (constr_of_global eq_ref) in
generate_induction_principle f_ref tcc_lemma_constr
- functional_ref eq_ref rec_arg_num (EConstr.of_constr rec_arg_type) (nb_prod evm (EConstr.of_constr res)) (EConstr.of_constr relation);
+ functional_ref eq_ref rec_arg_num
+ (EConstr.of_constr rec_arg_type)
+ (nb_prod evd (EConstr.of_constr res)) relation;
Flags.if_verbose
msgnl (h 1 (Ppconstr.pr_id function_name ++
spc () ++ str"is defined" )++ fnl () ++
@@ -1589,15 +1610,16 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
spc () ++ str"is defined" )
)
in
- States.with_state_protection_on_exception (fun () ->
+ (* XXX STATE Why do we need this... why is the toplevel protection not enought *)
+ funind_purify (fun () ->
com_terminate
tcc_lemma_name
tcc_lemma_constr
is_mes functional_ref
(EConstr.of_constr rec_arg_type)
- (EConstr.of_constr relation) rec_arg_num
+ relation rec_arg_num
term_id
using_lemmas
(List.length res_vars)
- evm (Lemmas.mk_hook hook))
+ evd (Lemmas.mk_hook hook))
()
diff --git a/plugins/funind/recdef.mli b/plugins/funind/recdef.mli
index f3d5e73320..549f1fc0e4 100644
--- a/plugins/funind/recdef.mli
+++ b/plugins/funind/recdef.mli
@@ -1,6 +1,5 @@
-open API
+open Constr
-(* val evaluable_of_global_reference : Libnames.global_reference -> Names.evaluable_global_reference *)
val tclUSER_if_not_mes :
Tacmach.tactic ->
bool ->
@@ -12,9 +11,9 @@ bool ->
Constrintern.internalization_env ->
Constrexpr.constr_expr ->
Constrexpr.constr_expr ->
- int -> Constrexpr.constr_expr -> (Term.pconstant ->
+ int -> Constrexpr.constr_expr -> (pconstant ->
Indfun_common.tcc_lemma_value ref ->
- Term.pconstant ->
- Term.pconstant -> int -> EConstr.types -> int -> EConstr.constr -> 'a) -> Constrexpr.constr_expr list -> unit
+ pconstant ->
+ pconstant -> int -> EConstr.types -> int -> EConstr.constr -> unit) -> Constrexpr.constr_expr list -> unit
diff --git a/plugins/funind/recdef_plugin.mlpack b/plugins/funind/recdef_plugin.mlpack
index 2b443f2a1b..755fa4f879 100644
--- a/plugins/funind/recdef_plugin.mlpack
+++ b/plugins/funind/recdef_plugin.mlpack
@@ -6,5 +6,4 @@ Functional_principles_proofs
Functional_principles_types
Invfun
Indfun
-Merge
G_indfun
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-07 02:38:24 +0000