From 5143129baac805d3a49ac3ee9f3344c7a447634f Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 30 Oct 2016 17:53:07 +0100 Subject: Termops API using EConstr. --- plugins/funind/indfun.ml | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) (limited to 'plugins/funind/indfun.ml') diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 99b04898ba..a264c37c57 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -14,20 +14,21 @@ open Sigma.Notations module RelDecl = Context.Rel.Declaration -let is_rec_info scheme_info = +let is_rec_info sigma scheme_info = let test_branche min acc decl = acc || ( let new_branche = it_mkProd_or_LetIn mkProp (fst (decompose_prod_assum (RelDecl.get_type decl))) in - let free_rels_in_br = Termops.free_rels new_branche in + let free_rels_in_br = Termops.free_rels sigma (EConstr.of_constr new_branche) in let max = min + scheme_info.Tactics.npredicates in Int.Set.exists (fun i -> i >= min && i< max) free_rels_in_br ) in List.fold_left_i test_branche 1 false (List.rev scheme_info.Tactics.branches) -let choose_dest_or_ind scheme_info = - Tactics.induction_destruct (is_rec_info scheme_info) false +let choose_dest_or_ind scheme_info args = + Proofview.tclBIND Proofview.tclEVARMAP (fun sigma -> + Tactics.induction_destruct (is_rec_info sigma scheme_info) false args) let functional_induction with_clean c princl pat = let res = -- cgit v1.2.3 From e27949240f5b1ee212e7d0fe3326a21a13c4abb0 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 6 Nov 2016 17:21:44 +0100 Subject: Typing API using EConstr. --- plugins/funind/indfun.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins/funind/indfun.ml') diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index a264c37c57..0743fc5d92 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -369,7 +369,7 @@ 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 uprinc in + let princ_type = Typing.e_type_of ~refresh:true env evd (EConstr.of_constr uprinc) in Functional_principles_types.generate_functional_principle evd interactive_proof -- cgit v1.2.3 From cbea91d815f134d63d02d8fb1bd78ed97db28cd1 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 11 Nov 2016 19:52:48 +0100 Subject: Tacmach API using EConstr. --- plugins/funind/indfun.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'plugins/funind/indfun.ml') diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 0743fc5d92..e3ba522467 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -75,11 +75,11 @@ let functional_induction with_clean c princl pat = user_err (str "Cannot find induction principle for " ++Printer.pr_lconstr (mkConst c') ) in - (princ,NoBindings, Tacmach.pf_unsafe_type_of g' princ,g') + (princ,NoBindings, Tacmach.pf_unsafe_type_of g' (EConstr.of_constr princ),g') | _ -> raise (UserError(None,str "functional induction must be used with a function" )) end | Some ((princ,binding)) -> - princ,binding,Tacmach.pf_unsafe_type_of g princ,g + princ,binding,Tacmach.pf_unsafe_type_of g (EConstr.of_constr princ),g in let princ_infos = Tactics.compute_elim_sig princ_type in let args_as_induction_constr = -- cgit v1.2.3 From 485bbfbed4ae4a28119c4e42c5e40fd77abf4f8a Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 13 Nov 2016 20:38:41 +0100 Subject: Tactics API using EConstr. --- plugins/funind/indfun.ml | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) (limited to 'plugins/funind/indfun.ml') diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index e3ba522467..37a76bec1c 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -81,7 +81,8 @@ let functional_induction with_clean c princl pat = | Some ((princ,binding)) -> princ,binding,Tacmach.pf_unsafe_type_of g (EConstr.of_constr princ),g in - let princ_infos = Tactics.compute_elim_sig princ_type in + let princ_type = EConstr.of_constr princ_type in + let princ_infos = Tactics.compute_elim_sig (Tacmach.project g') princ_type in let args_as_induction_constr = let c_list = if princ_infos.Tactics.farg_in_concl @@ -89,9 +90,11 @@ let functional_induction with_clean c princl pat = in 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 ({ Tacexpr.delayed = fun env sigma -> Sigma ((c,NoBindings), sigma, Sigma.refl) })),(None,pat),None)) + List.map2 (fun c pat -> ((None,Tacexpr.ElimOnConstr ({ Tacexpr.delayed = fun env sigma -> Sigma ((EConstr.of_constr c,NoBindings), sigma, Sigma.refl) })),(None,pat),None)) (args@c_list) encoded_pat_as_patlist in + let princ = EConstr.of_constr princ in + let bindings = Miscops.map_bindings EConstr.of_constr bindings in let princ' = Some (princ,bindings) in let princ_vars = List.fold_right -- cgit v1.2.3 From 531590c223af42c07a93142ab0cea470a98964e6 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 24 Nov 2016 17:15:15 +0100 Subject: Removing compatibility layers in Retyping --- plugins/funind/indfun.ml | 1 + 1 file changed, 1 insertion(+) (limited to 'plugins/funind/indfun.ml') diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 37a76bec1c..1b899c152f 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -373,6 +373,7 @@ let generate_principle (evd:Evd.evar_map ref) pconstants on_error 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 princ_type = EConstr.Unsafe.to_constr princ_type in Functional_principles_types.generate_functional_principle evd interactive_proof -- cgit v1.2.3 From a5499688bd76def8de3d8e1089a49c7a08430903 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 25 Nov 2016 14:54:40 +0100 Subject: Funind API using EConstr. --- plugins/funind/indfun.ml | 45 +++++++++++++++++++++++++-------------------- 1 file changed, 25 insertions(+), 20 deletions(-) (limited to 'plugins/funind/indfun.ml') diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 1b899c152f..e22fed391e 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -2,6 +2,7 @@ open CErrors open Util open Names open Term +open EConstr open Pp open Indfun_common open Libnames @@ -18,8 +19,8 @@ let is_rec_info sigma scheme_info = let test_branche min acc decl = acc || ( let new_branche = - it_mkProd_or_LetIn mkProp (fst (decompose_prod_assum (RelDecl.get_type decl))) in - let free_rels_in_br = Termops.free_rels sigma (EConstr.of_constr new_branche) in + it_mkProd_or_LetIn mkProp (fst (decompose_prod_assum sigma (EConstr.of_constr (RelDecl.get_type decl)))) in + let free_rels_in_br = Termops.free_rels sigma new_branche in let max = min + scheme_info.Tactics.npredicates in Int.Set.exists (fun i -> i >= min && i< max) free_rels_in_br ) @@ -32,20 +33,21 @@ let choose_dest_or_ind scheme_info args = let functional_induction with_clean c princl pat = let res = - let f,args = decompose_app c in fun g -> + let sigma = Tacmach.project g in + let f,args = decompose_app sigma c in let princ,bindings, princ_type,g' = match princl with | None -> (* No principle is given let's find the good one *) begin - match kind_of_term f with + match EConstr.kind sigma f with | Const (c',u) -> let princ_option = let finfo = (* we first try to find out a graph on f *) try find_Function_infos c' with Not_found -> user_err (str "Cannot find induction information on "++ - Printer.pr_lconstr (mkConst c') ) + Printer.pr_leconstr (mkConst c') ) in match Tacticals.elimination_sort_of_goal g with | InProp -> finfo.prop_lemma @@ -73,15 +75,16 @@ 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_lconstr (mkConst c') ) + ++Printer.pr_leconstr (mkConst c') ) in - (princ,NoBindings, Tacmach.pf_unsafe_type_of g' (EConstr.of_constr princ),g') + let princ = EConstr.of_constr princ in + (princ,NoBindings,EConstr.of_constr (Tacmach.pf_unsafe_type_of g' princ),g') | _ -> raise (UserError(None,str "functional induction must be used with a function" )) end | Some ((princ,binding)) -> - princ,binding,Tacmach.pf_unsafe_type_of g (EConstr.of_constr princ),g + princ,binding,EConstr.of_constr (Tacmach.pf_unsafe_type_of g princ),g in - let princ_type = EConstr.of_constr princ_type in + let sigma = Tacmach.project g' in let princ_infos = Tactics.compute_elim_sig (Tacmach.project g') princ_type in let args_as_induction_constr = let c_list = @@ -90,15 +93,13 @@ let functional_induction with_clean c princl pat = in 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 ({ Tacexpr.delayed = fun env sigma -> Sigma ((EConstr.of_constr c,NoBindings), sigma, Sigma.refl) })),(None,pat),None)) + List.map2 (fun c pat -> ((None,Tacexpr.ElimOnConstr ({ Tacexpr.delayed = fun env sigma -> Sigma ((c,NoBindings), sigma, Sigma.refl) })),(None,pat),None)) (args@c_list) encoded_pat_as_patlist in - let princ = EConstr.of_constr princ in - let bindings = Miscops.map_bindings EConstr.of_constr bindings in let princ' = Some (princ,bindings) in let princ_vars = List.fold_right - (fun a acc -> try Id.Set.add (destVar a) acc with DestKO -> acc) + (fun a acc -> try Id.Set.add (destVar sigma a) acc with DestKO -> acc) args Id.Set.empty in @@ -247,7 +248,8 @@ let derive_inversion fix_names = let evd,c = Evd.fresh_global (Global.env ()) evd (Constrintern.locate_reference (Libnames.qualid_of_ident id)) in - evd, destConst c::l + let c = EConstr.of_constr c in + evd, destConst evd c::l ) fix_names (evd',[]) @@ -267,7 +269,8 @@ let derive_inversion fix_names = (Global.env ()) evd (Constrintern.locate_reference (Libnames.qualid_of_ident (mk_rel_id id))) in - evd,(fst (destInd id))::l + let id = EConstr.of_constr id in + evd,(fst (destInd evd id))::l ) fix_names (evd',[]) @@ -334,7 +337,7 @@ let error_error names e = 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 array -> Term.constr array -> int -> + (continue_proof : int -> Names.constant array -> EConstr.constr array -> int -> Tacmach.tactic) : unit = let names = List.map (function (((_, name),_),_,_,_,_),_ -> name) fix_rec_l in let fun_bodies = List.map2 prepare_body fix_rec_l recdefs in @@ -408,7 +411,8 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp let evd,c = Evd.fresh_global (Global.env ()) evd (Constrintern.locate_reference (Libnames.qualid_of_ident fname)) in - evd,((destConst c)::l) + let c = EConstr.of_constr c in + evd,((destConst evd c)::l) ) (Evd.from_env (Global.env ()),[]) fixpoint_exprl @@ -422,7 +426,8 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp let evd,c = Evd.fresh_global (Global.env ()) evd (Constrintern.locate_reference (Libnames.qualid_of_ident fname)) in - evd,((destConst c)::l) + let c = EConstr.of_constr c in + evd,((destConst evd c)::l) ) (Evd.from_env (Global.env ()),[]) fixpoint_exprl @@ -432,7 +437,7 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp let generate_correction_proof_wf f_ref tcc_lemma_ref is_mes functional_ref eq_ref rec_arg_num rec_arg_type nb_args relation - (_: int) (_:Names.constant array) (_:Term.constr array) (_:int) : Tacmach.tactic = + (_: int) (_:Names.constant array) (_:EConstr.constr array) (_:int) : Tacmach.tactic = Functional_principles_proofs.prove_principle_for_gen (f_ref,functional_ref,eq_ref) tcc_lemma_ref is_mes rec_arg_num rec_arg_type relation @@ -840,7 +845,7 @@ let make_graph (f_ref:global_reference) = | ConstRef c -> begin try c,Global.lookup_constant c with Not_found -> - raise (UserError (None,str "Cannot find " ++ Printer.pr_lconstr (mkConst c)) ) + raise (UserError (None,str "Cannot find " ++ Printer.pr_leconstr (mkConst c)) ) end | _ -> raise (UserError (None, str "Not a function reference") ) in -- cgit v1.2.3 From 02dd160233adc784eac732d97a88356d1f0eaf9b Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 25 Nov 2016 18:34:53 +0100 Subject: Removing various compatibility layers of tactics. --- plugins/funind/indfun.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'plugins/funind/indfun.ml') diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index e22fed391e..1cde4420e5 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -78,11 +78,11 @@ let functional_induction with_clean c princl pat = ++Printer.pr_leconstr (mkConst c') ) in let princ = EConstr.of_constr princ in - (princ,NoBindings,EConstr.of_constr (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)) -> - princ,binding,EConstr.of_constr (Tacmach.pf_unsafe_type_of g princ),g + princ,binding,Tacmach.pf_unsafe_type_of g princ,g in let sigma = Tacmach.project g' in let princ_infos = Tactics.compute_elim_sig (Tacmach.project g') princ_type in -- cgit v1.2.3 From b4b90c5d2e8c413e1981c456c933f35679386f09 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 26 Nov 2016 16:18:47 +0100 Subject: Definining EConstr-based contexts. This removes quite a few unsafe casts. Unluckily, I had to reintroduce the old non-module based names for these data structures, because I could not reproduce easily the same hierarchy in EConstr. --- plugins/funind/indfun.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins/funind/indfun.ml') diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 1cde4420e5..a7489fb7b4 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -19,7 +19,7 @@ let is_rec_info sigma scheme_info = let test_branche min acc decl = acc || ( let new_branche = - it_mkProd_or_LetIn mkProp (fst (decompose_prod_assum sigma (EConstr.of_constr (RelDecl.get_type decl)))) in + it_mkProd_or_LetIn mkProp (fst (decompose_prod_assum sigma (RelDecl.get_type decl))) in let free_rels_in_br = Termops.free_rels sigma new_branche in let max = min + scheme_info.Tactics.npredicates in Int.Set.exists (fun i -> i >= min && i< max) free_rels_in_br -- cgit v1.2.3 From 7babf0d42af11f5830bc157a671bd81b478a4f02 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 1 Apr 2017 02:36:16 +0200 Subject: Using delayed universe instances in EConstr. The transition has been done a bit brutally. I think we can still save a lot of useless normalizations here and there by providing the right API in EConstr. Nonetheless, this is a first step. --- plugins/funind/indfun.ml | 11 ++++++++--- 1 file changed, 8 insertions(+), 3 deletions(-) (limited to 'plugins/funind/indfun.ml') diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index a7489fb7b4..2852152e13 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -249,7 +249,8 @@ let derive_inversion fix_names = Evd.fresh_global (Global.env ()) evd (Constrintern.locate_reference (Libnames.qualid_of_ident id)) in let c = EConstr.of_constr c in - evd, destConst evd c::l + let (cst, u) = destConst evd c in + evd, (cst, EInstance.kind evd u) :: l ) fix_names (evd',[]) @@ -412,7 +413,9 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp Evd.fresh_global (Global.env ()) evd (Constrintern.locate_reference (Libnames.qualid_of_ident fname)) in let c = EConstr.of_constr c in - evd,((destConst evd c)::l) + let (cst, u) = destConst evd c in + let u = EInstance.kind evd u in + evd,((cst, u) :: l) ) (Evd.from_env (Global.env ()),[]) fixpoint_exprl @@ -427,7 +430,9 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp Evd.fresh_global (Global.env ()) evd (Constrintern.locate_reference (Libnames.qualid_of_ident fname)) in let c = EConstr.of_constr c in - evd,((destConst evd c)::l) + let (cst, u) = destConst evd c in + let u = EInstance.kind evd u in + evd,((cst, u) :: l) ) (Evd.from_env (Global.env ()),[]) fixpoint_exprl -- cgit v1.2.3