From 97fefe1fcca363a1317e066e7f4b99b9c1e9987b Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Thu, 12 Jan 2012 16:02:20 +0100 Subject: Imported Upstream version 8.4~beta --- plugins/funind/functional_principles_types.ml | 61 +++++++++++++-------------- 1 file changed, 30 insertions(+), 31 deletions(-) (limited to 'plugins/funind/functional_principles_types.ml') diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index b756492b..6df9d574 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -1,7 +1,6 @@ open Printer open Util open Term -open Termops open Namegen open Names open Declarations @@ -114,9 +113,8 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = in let pre_princ = it_mkProd_or_LetIn - ~init: (it_mkProd_or_LetIn - ~init:(Option.fold_right + (Option.fold_right mkProd_or_LetIn princ_type_info.indarg princ_type_info.concl @@ -140,7 +138,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = in 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 + 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); *) res in @@ -199,58 +197,58 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = begin try let new_t,binders_to_remove_from_t = compute_new_princ_type remove env t in - let new_x : name = get_name (ids_of_context env) x in + let new_x : name = get_name (Termops.ids_of_context env) x in let new_env = Environ.push_rel (x,None,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 + then (Termops.pop new_b), filter_map (eq_constr (mkRel 1)) Termops.pop binders_to_remove_from_b else ( bind_fun(new_x,new_t,new_b), list_union_eq eq_constr binders_to_remove_from_t - (List.map pop binders_to_remove_from_b) + (List.map Termops.pop binders_to_remove_from_b) ) with | Toberemoved -> (* observe (str "Decl of "++Ppconstr.pr_name x ++ str " is removed "); *) let new_b,binders_to_remove_from_b = compute_new_princ_type remove env (substnl [dummy_var] 1 b) in - new_b, List.map pop binders_to_remove_from_b + new_b, List.map Termops.pop binders_to_remove_from_b | Toberemoved_with_rel (n,c) -> (* observe (str "Decl of "++Ppconstr.pr_name 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 eq_constr (mkRel n) (List.map Termops.pop binders_to_remove_from_b) end and compute_new_princ_type_for_letin remove env x v t b = begin try let new_t,binders_to_remove_from_t = compute_new_princ_type remove env t in let new_v,binders_to_remove_from_v = compute_new_princ_type remove env v in - let new_x : name = get_name (ids_of_context env) x in + let new_x : name = get_name (Termops.ids_of_context env) x in let new_env = Environ.push_rel (x,Some 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 + then (Termops.pop new_b),filter_map (eq_constr (mkRel 1)) Termops.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) - (List.map pop binders_to_remove_from_b) + (List.map Termops.pop binders_to_remove_from_b) ) with | Toberemoved -> (* observe (str "Decl of "++Ppconstr.pr_name x ++ str " is removed "); *) let new_b,binders_to_remove_from_b = compute_new_princ_type remove env (substnl [dummy_var] 1 b) in - new_b, List.map pop binders_to_remove_from_b + new_b, List.map Termops.pop binders_to_remove_from_b | Toberemoved_with_rel (n,c) -> (* observe (str "Decl of "++Ppconstr.pr_name 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 eq_constr (mkRel n) (List.map Termops.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 @@ -267,10 +265,10 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = (lift (List.length ptes_vars) pre_res) in it_mkProd_or_LetIn - ~init:(it_mkProd_or_LetIn - ~init:pre_res (List.map (fun (id,t,b) -> Name(Hashtbl.find tbl id), t,b) - new_predicates) - ) + (it_mkProd_or_LetIn + pre_res (List.map (fun (id,t,b) -> Name(Hashtbl.find tbl id), t,b) + new_predicates) + ) princ_type_info.params @@ -283,7 +281,7 @@ let change_property_sort toSort princ princName = compose_prod args (mkSort toSort) ) in - let princName_as_constr = Tacinterp.constr_of_id (Global.env ()) princName in + let princName_as_constr = Constrintern.global_reference princName in let init = let nargs = (princ_info.nparams + (List.length princ_info.predicates)) in mkApp(princName_as_constr, @@ -291,8 +289,7 @@ let change_property_sort toSort princ princName = (fun i -> mkRel (nargs - i ))) in it_mkLambda_or_LetIn - ~init: - (it_mkLambda_or_LetIn ~init + (it_mkLambda_or_LetIn init (List.map change_sort_in_predicate princ_info.predicates) ) princ_info.params @@ -384,10 +381,9 @@ let generate_functional_principle (* Pp.msgnl (str "new principle := " ++ pr_lconstr value); *) let ce = { const_entry_body = value; + const_entry_secctx = None; const_entry_type = None; - const_entry_opaque = false; - const_entry_boxed = Flags.boxed_definitions() - } + const_entry_opaque = false } in ignore( Declare.declare_constant @@ -450,7 +446,7 @@ let get_funs_constant mp dp = in function const -> let find_constant_body const = - match (Global.lookup_constant const ).const_body with + match body_of_constant (Global.lookup_constant const) with | Some b -> let body = force b in let body = Tacred.cbv_norm_flags @@ -475,7 +471,7 @@ let get_funs_constant mp dp = let first_params = List.hd l_params in List.iter (fun params -> - if not ((=) first_params params) + if not (list_equal (fun (n1, c1) (n2, c2) -> n1 = n2 && eq_constr c1 c2) first_params params) then error "Not a mutal recursive block" ) l_params @@ -493,7 +489,10 @@ let get_funs_constant mp dp = in let first_infos = extract_info true (List.hd l_bodies) in let check body = (* Hope this is correct *) - if not (first_infos = (extract_info false body)) + let eq_infos (ia1, na1, ta1, ca1) (ia2, na2, ta2, ca2) = + ia1 = ia2 && na1 = na2 && array_equal eq_constr ta1 ta2 && array_equal eq_constr ca1 ca2 + in + if not (eq_infos first_infos (extract_info false body)) then error "Not a mutal recursive block" in List.iter check l_bodies @@ -504,7 +503,7 @@ let get_funs_constant mp dp = exception No_graph_found exception Found_type of int -let make_scheme (fas : (constant*Rawterm.rawsort) list) : Entries.definition_entry list = +let make_scheme (fas : (constant*Glob_term.glob_sort) list) : Entries.definition_entry list = let env = Global.env () and sigma = Evd.empty in let funs = List.map fst fas in @@ -584,7 +583,7 @@ let make_scheme (fas : (constant*Rawterm.rawsort) list) : Entries.definition_ent let finfos = find_Function_infos this_block_funs.(0) in try let equation = Option.get finfos.equation_lemma in - (Global.lookup_constant equation).Declarations.const_opaque + Declarations.is_opaque (Global.lookup_constant equation) with Option.IsNone -> (* non recursive definition *) false in @@ -639,7 +638,7 @@ let make_scheme (fas : (constant*Rawterm.rawsort) list) : Entries.definition_ent const with Found_type i -> let princ_body = - Termops.it_mkLambda_or_LetIn ~init:(mkFix((idxs,i),decl)) ctxt + Termops.it_mkLambda_or_LetIn (mkFix((idxs,i),decl)) ctxt in {const with Entries.const_entry_body = princ_body; @@ -688,7 +687,7 @@ let build_case_scheme fa = let env = Global.env () and sigma = Evd.empty in (* let id_to_constr id = *) -(* Tacinterp.constr_of_id env id *) +(* Constrintern.global_reference id *) (* in *) let funs = (fun (_,f,_) -> try Libnames.constr_of_global (Nametab.global f) -- cgit v1.2.3