summaryrefslogtreecommitdiff
path: root/plugins/funind/functional_principles_types.ml
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/funind/functional_principles_types.ml')
-rw-r--r--plugins/funind/functional_principles_types.ml143
1 files changed, 75 insertions, 68 deletions
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 545f8931..45e5aaf5 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -6,7 +6,6 @@ open Vars
open Context
open Namegen
open Names
-open Declareops
open Pp
open Entries
open Tactics
@@ -106,7 +105,7 @@ 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 Termops.pop (array_get_start args)) in
-(* observe (str "replacing " ++ pr_lconstr c ++ str " by " ++ pr_lconstr res); *)
+ observe (str "replacing " ++ pr_lconstr c ++ str " by " ++ pr_lconstr res);
res
in
let rec compute_new_princ_type remove env pre_princ : types*(constr list) =
@@ -116,7 +115,8 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
begin
try match Environ.lookup_rel n env with
| _,_,t when is_dom t -> raise Toberemoved
- | _ -> pre_princ,[] with Not_found -> assert false
+ | _ -> pre_princ,[]
+ with Not_found -> assert false
end
| Prod(x,t,b) ->
compute_new_princ_type_for_binder remove mkProd env x t b
@@ -234,7 +234,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
-let change_property_sort toSort princ princName =
+let change_property_sort evd toSort princ princName =
let princ_info = compute_elim_sig princ in
let change_sort_in_predicate (x,v,t) =
(x,None,
@@ -244,46 +244,48 @@ let change_property_sort toSort princ princName =
compose_prod args (mkSort toSort)
)
in
- let princName_as_constr = Constrintern.global_reference princName in
+ let evd,princName_as_constr =
+ Evd.fresh_global
+ (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,
Array.init nargs
(fun i -> mkRel (nargs - i )))
in
- it_mkLambda_or_LetIn
+ evd, it_mkLambda_or_LetIn
(it_mkLambda_or_LetIn init
(List.map change_sort_in_predicate princ_info.predicates)
)
princ_info.params
-let build_functional_principle interactive_proof old_princ_type sorts funs i proof_tac hook =
+let build_functional_principle (evd:Evd.evar_map ref) interactive_proof old_princ_type sorts funs i proof_tac hook =
(* First we get the type of the old graph principle *)
let mutr_nparams = (compute_elim_sig old_princ_type).nparams in
(* let time1 = System.get_time () in *)
let new_principle_type =
compute_new_princ_type_from_rel
- (Array.map mkConst funs)
+ (Array.map mkConstU funs)
sorts
old_princ_type
in
(* let time2 = System.get_time () in *)
(* Pp.msgnl (str "computing principle type := " ++ System.fmt_time_difference time1 time2); *)
- observe (str "new_principle_type : " ++ pr_lconstr new_principle_type);
let new_princ_name =
next_ident_away_in_goal (Id.of_string "___________princ_________") []
in
+ let _ = evd := fst(Typing.e_type_of ~refresh:true (Global.env ()) !evd new_principle_type ) in
let hook = Lemmas.mk_hook (hook new_principle_type) in
begin
Lemmas.start_proof
new_princ_name
- (Decl_kinds.Global,false,(Decl_kinds.Proof Decl_kinds.Theorem))
- (*FIXME*) Evd.empty
- new_principle_type
+ (Decl_kinds.Global,Flags.is_universe_polymorphism (),(Decl_kinds.Proof Decl_kinds.Theorem))
+ !evd
+ new_principle_type
hook
- ;
+ ;
(* let _tim1 = System.get_time () in *)
- ignore (Pfedit.by (Proofview.V82.tactic (proof_tac (Array.map mkConst funs) mutr_nparams)));
+ ignore (Pfedit.by (Proofview.V82.tactic (proof_tac (Array.map mkConstU funs) mutr_nparams)));
(* let _tim2 = System.get_time () in *)
(* begin *)
(* let dur1 = System.time_difference tim1 tim2 in *)
@@ -294,7 +296,7 @@ let build_functional_principle interactive_proof old_princ_type sorts funs i pro
-let generate_functional_principle
+let generate_functional_principle (evd: Evd.evar_map ref)
interactive_proof
old_princ_type sorts new_princ_name funs i proof_tac
=
@@ -311,20 +313,23 @@ let generate_functional_principle
match new_princ_name with
| Some (id) -> id,id
| None ->
- let id_of_f = Label.to_id (con_label f) in
+ let id_of_f = Label.to_id (con_label (fst f)) in
id_of_f,Indrec.make_elimination_ident id_of_f (family_of_sort type_sort)
in
let names = ref [new_princ_name] in
- let hook new_principle_type _ _ =
+ let evd' = !evd in
+ let hook =
+ fun new_principle_type _ _ ->
if Option.is_empty sorts
then
(* let id_of_f = Label.to_id (con_label f) in *)
let register_with_sort fam_sort =
let s = Universes.new_sort_in_family fam_sort in
let name = Indrec.make_elimination_ident base_new_princ_name fam_sort in
- let value = change_property_sort s new_principle_type new_princ_name in
- (* Pp.msgnl (str "new principle := " ++ pr_lconstr value); *)
- let ce = Declare.definition_entry value in (*FIXME, no poly, nothing *)
+ let evd',value = change_property_sort evd' s new_principle_type new_princ_name in
+ let evd' = fst (Typing.e_type_of ~refresh:true (Global.env ()) evd' value) in
+ (* Pp.msgnl (str "new principle := " ++ pr_lconstr value); *)
+ let ce = Declare.definition_entry ~poly:(Flags.is_universe_polymorphism ()) ~univs:(Evd.universe_context evd') value in
ignore(
Declare.declare_constant
name
@@ -338,7 +343,7 @@ let generate_functional_principle
register_with_sort InSet
in
let ((id,(entry,g_kind)),hook) =
- build_functional_principle interactive_proof old_princ_type new_sorts funs i
+ build_functional_principle evd interactive_proof old_princ_type new_sorts funs i
proof_tac hook
in
(* Pr 1278 :
@@ -441,39 +446,37 @@ let get_funs_constant mp dp =
exception No_graph_found
exception Found_type of int
-let make_scheme (fas : (constant*glob_sort) list) : Entries.definition_entry list =
- let env = Global.env ()
- and sigma = Evd.empty in
+let make_scheme evd (fas : (pconstant*glob_sort) list) : Entries.definition_entry list =
+ let env = Global.env () in
let funs = List.map fst fas in
let first_fun = List.hd funs in
-
-
- let funs_mp,funs_dp,_ = Names.repr_con first_fun in
+ let funs_mp,funs_dp,_ = KerName.repr (Constant.canonical (fst first_fun)) in
let first_fun_kn =
try
- fst (find_Function_infos first_fun).graph_ind
+ fst (find_Function_infos (fst first_fun)).graph_ind
with Not_found -> raise No_graph_found
in
- let this_block_funs_indexes = get_funs_constant funs_mp funs_dp first_fun in
- let this_block_funs = Array.map fst this_block_funs_indexes in
+ let this_block_funs_indexes = get_funs_constant funs_mp funs_dp (fst first_fun) in
+ let this_block_funs = Array.map (fun (c,_) -> (c,snd first_fun)) this_block_funs_indexes in
let prop_sort = InProp in
let funs_indexes =
let this_block_funs_indexes = Array.to_list this_block_funs_indexes in
List.map
- (function cst -> List.assoc_f Constant.equal cst this_block_funs_indexes)
+ (function cst -> List.assoc_f Constant.equal (fst cst) this_block_funs_indexes)
funs
in
let ind_list =
List.map
(fun (idx) ->
let ind = first_fun_kn,idx in
- (ind,Univ.Instance.empty)(*FIXME*),true,prop_sort
+ (ind,snd first_fun),true,prop_sort
)
funs_indexes
in
let sigma, schemes =
- Indrec.build_mutual_induction_scheme env sigma ind_list
+ Indrec.build_mutual_induction_scheme env !evd ind_list
in
+ let _ = evd := sigma in
let l_schemes =
List.map (Typing.type_of env sigma) schemes
in
@@ -484,6 +487,7 @@ let make_scheme (fas : (constant*glob_sort) list) : Entries.definition_entry lis
)
fas
in
+ evd:=sigma;
(* We create the first priciple by tactic *)
let first_type,other_princ_types =
match l_schemes with
@@ -492,34 +496,34 @@ let make_scheme (fas : (constant*glob_sort) list) : Entries.definition_entry lis
in
let ((_,(const,_)),_) =
try
- build_functional_principle false
+ build_functional_principle evd false
first_type
(Array.of_list sorts)
this_block_funs
0
- (prove_princ_for_struct false 0 (Array.of_list funs))
+ (prove_princ_for_struct evd false 0 (Array.of_list (List.map fst funs)))
(fun _ _ _ -> ())
- with e when Errors.noncritical e ->
- begin
- begin
- try
- let id = Pfedit.get_current_proof_name () in
- let s = Id.to_string id in
- let n = String.length "___________princ_________" in
- if String.length s >= n
- then if String.equal (String.sub s 0 n) "___________princ_________"
- then Pfedit.delete_current_proof ()
- else ()
- else ()
- with e when Errors.noncritical e -> ()
- end;
- raise (Defining_principle e)
- end
+ with e when Errors.noncritical e ->
+ begin
+ begin
+ try
+ let id = Pfedit.get_current_proof_name () in
+ let s = Id.to_string id in
+ let n = String.length "___________princ_________" in
+ if String.length s >= n
+ then if String.equal (String.sub s 0 n) "___________princ_________"
+ then Pfedit.delete_current_proof ()
+ else ()
+ else ()
+ with e when Errors.noncritical e -> ()
+ end;
+ raise (Defining_principle e)
+ end
in
incr i;
let opacity =
- let finfos = find_Function_infos this_block_funs.(0) in
+ let finfos = find_Function_infos (fst first_fun) in
try
let equation = Option.get finfos.equation_lemma in
Declareops.is_opaque (Global.lookup_constant equation)
@@ -533,7 +537,7 @@ let make_scheme (fas : (constant*glob_sort) list) : Entries.definition_entry lis
[const]
else
let other_fun_princ_types =
- let funs = Array.map mkConst this_block_funs in
+ let funs = Array.map mkConstU this_block_funs in
let sorts = Array.of_list sorts in
List.map (compute_new_princ_type_from_rel funs sorts) other_princ_types
in
@@ -566,12 +570,13 @@ let make_scheme (fas : (constant*glob_sort) list) : Entries.definition_entry lis
*)
let ((_,(const,_)),_) =
build_functional_principle
+ evd
false
(List.nth other_princ_types (!i - 1))
(Array.of_list sorts)
this_block_funs
!i
- (prove_princ_for_struct false !i (Array.of_list funs))
+ (prove_princ_for_struct evd false !i (Array.of_list (List.map fst funs)))
(fun _ _ _ -> ())
in
const
@@ -589,24 +594,27 @@ let make_scheme (fas : (constant*glob_sort) list) : Entries.definition_entry lis
in
const::other_result
+
let build_scheme fas =
Dumpglob.pause ();
- let bodies_types =
- make_scheme
- (List.map
+ let evd = (ref Evd.empty) in
+ let pconstants = (List.map
(fun (_,f,sort) ->
let f_as_constant =
try
- match Smartlocate.global_with_alias f with
- | Globnames.ConstRef c -> c
- | _ -> Errors.error "Functional Scheme can only be used with functions"
+ Smartlocate.global_with_alias f
with Not_found ->
Errors.error ("Cannot find "^ Libnames.string_of_reference f)
in
- (f_as_constant,sort)
+ let evd',f = Evd.fresh_global (Global.env ()) !evd f_as_constant in
+ let evd',_ = Typing.e_type_of ~refresh:true (Global.env ()) evd' f in
+ let _ = evd := evd' in
+ (destConst f,sort)
)
fas
- )
+ ) in
+ let bodies_types =
+ make_scheme evd pconstants
in
List.iter2
(fun (princ_id,_,_) def_entry ->
@@ -633,14 +641,10 @@ let build_case_scheme fa =
with Not_found ->
Errors.error ("Cannot find "^ Libnames.string_of_reference f)) fa in
let first_fun,u = destConst funs in
-
let funs_mp,funs_dp,_ = Names.repr_con first_fun in
let first_fun_kn = try fst (find_Function_infos first_fun).graph_ind with Not_found -> raise No_graph_found in
-
-
-
let this_block_funs_indexes = get_funs_constant funs_mp funs_dp first_fun in
- let this_block_funs = Array.map fst this_block_funs_indexes in
+ let this_block_funs = Array.map (fun (c,_) -> (c,u)) this_block_funs_indexes in
let prop_sort = InProp in
let funs_indexes =
let this_block_funs_indexes = Array.to_list this_block_funs_indexes in
@@ -666,12 +670,15 @@ let build_case_scheme fa =
);
*)
generate_functional_principle
+ (ref Evd.empty)
false
scheme_type
(Some ([|sorts|]))
(Some princ_name)
this_block_funs
0
- (prove_princ_for_struct false 0 [|fst (destConst funs)|])
+ (prove_princ_for_struct (ref Evd.empty) false 0 [|fst (destConst funs)|])
in
()
+
+
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-15 07:16:49 +0000