From 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Wed, 21 Jul 2010 09:46:51 +0200 Subject: Imported Upstream snapshot 8.3~beta0+13298 --- pretyping/recordops.ml | 154 +++++++++++++++++++++++++++++++++++-------------- 1 file changed, 111 insertions(+), 43 deletions(-) (limited to 'pretyping/recordops.ml') diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index 711f332e..6c903238 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: recordops.ml 12187 2009-06-13 19:36:59Z msozeau $ *) +(* $Id$ *) open Util open Pp @@ -18,7 +18,6 @@ open Termops open Typeops open Libobject open Library -open Classops open Mod_subst open Reductionops @@ -32,7 +31,7 @@ open Reductionops projection ou bien une fonction constante (associée à un LetIn) *) type struc_typ = { - s_CONST : constructor; + s_CONST : constructor; s_EXPECTEDPARAM : int; s_PROJKIND : (name * bool) list; s_PROJ : constant option list } @@ -45,19 +44,19 @@ let load_structure i (_,(ind,id,kl,projs)) = let struc = { s_CONST = id; s_EXPECTEDPARAM = n; s_PROJ = projs; s_PROJKIND = kl } in structure_table := Indmap.add ind struc !structure_table; - projection_table := + projection_table := List.fold_right (Option.fold_right (fun proj -> Cmap.add proj struc)) projs !projection_table let cache_structure o = load_structure 1 o -let subst_structure (_,subst,((kn,i),id,kl,projs as obj)) = - let kn' = subst_kn subst kn in +let subst_structure (subst,((kn,i),id,kl,projs as obj)) = + let kn' = subst_ind subst kn in let projs' = (* invariant: struc.s_PROJ is an evaluable reference. Thus we can take *) (* the first component of subst_con. *) - list_smartmap + list_smartmap (Option.smartmap (fun kn -> fst (subst_con subst kn))) projs in @@ -65,7 +64,7 @@ let subst_structure (_,subst,((kn,i),id,kl,projs as obj)) = if projs' == projs && kn' == kn && id' == id then obj else ((kn',i),id',kl,projs') -let discharge_constructor (ind, n) = +let discharge_constructor (ind, n) = (Lib.discharge_inductive ind, n) let discharge_structure (_,(ind,id,kl,projs)) = @@ -73,15 +72,14 @@ let discharge_structure (_,(ind,id,kl,projs)) = List.map (Option.map Lib.discharge_con) projs) let (inStruc,outStruc) = - declare_object {(default_object "STRUCTURE") with + declare_object {(default_object "STRUCTURE") with cache_function = cache_structure; load_function = load_structure; subst_function = subst_structure; - classify_function = (fun (_,x) -> Substitute x); - discharge_function = discharge_structure; - export_function = (function x -> Some x) } + classify_function = (fun x -> Substitute x); + discharge_function = discharge_structure } -let declare_structure (s,c,kl,pl) = +let declare_structure (s,c,kl,pl) = Lib.add_anonymous_leaf (inStruc (s,c,kl,pl)) let lookup_structure indsp = Indmap.find indsp !structure_table @@ -96,6 +94,55 @@ let find_projection = function | ConstRef cst -> Cmap.find cst !projection_table | _ -> raise Not_found +(* Management of a field store : each field + argument of the inferred + * records are stored in a discrimination tree *) + +let subst_id s (gr,ev,evm) = + (fst(subst_global s gr),ev,Evd.subst_evar_map s evm) + +module MethodsDnet : Term_dnet.S + with type ident = global_reference * Evd.evar * Evd.evar_map + = Term_dnet.Make + (struct + type t = global_reference * Evd.evar * Evd.evar_map + let compare = Pervasives.compare + let subst = subst_id + let constr_of (_,ev,evm) = Evd.evar_concl (Evd.find evm ev) + end) + (struct + let reduce c = Reductionops.head_unfold_under_prod + Names.full_transparent_state (Global.env()) Evd.empty c + let direction = true + end) + +let meth_dnet = ref MethodsDnet.empty + +open Summary + +let _ = + declare_summary "record-methods-state" + { freeze_function = (fun () -> !meth_dnet); + unfreeze_function = (fun m -> meth_dnet := m); + init_function = (fun () -> meth_dnet := MethodsDnet.empty) } + +open Libobject + +let load_method (_,(ty,id)) = + meth_dnet := MethodsDnet.add ty id !meth_dnet + +let (in_method,out_method) = + declare_object + { (default_object "RECMETHODS") with + load_function = (fun _ -> load_method); + cache_function = load_method; + subst_function = (fun (s,(ty,id)) -> Mod_subst.subst_mps s ty,subst_id s id); + classify_function = (fun x -> Substitute x) + } + +let methods_matching c = MethodsDnet.search_pattern !meth_dnet c + +let declare_method cons ev sign = + Lib.add_anonymous_leaf (in_method ((Evd.evar_concl (Evd.find sign ev)),(cons,ev,sign))) (************************************************************************) (*s A canonical structure declares "canonical" conversion hints between *) @@ -138,7 +185,7 @@ type cs_pattern = let object_table = ref (Refmap.empty : (cs_pattern * obj_typ) list Refmap.t) -let canonical_projections () = +let canonical_projections () = Refmap.fold (fun x -> List.fold_right (fun (y,c) acc -> ((x,y),c)::acc)) !object_table [] @@ -148,28 +195,28 @@ let keep_true_projections projs kinds = let cs_pattern_of_constr t = match kind_of_term t with - App (f,vargs) -> - begin + App (f,vargs) -> + begin try Const_cs (global_of_constr f) , -1, Array.to_list vargs with - _ -> raise Not_found - end + _ -> raise Not_found + end | Rel n -> Default_cs, pred n, [] | Prod (_,a,b) when not (dependent (mkRel 1) b) -> Prod_cs, -1, [a;pop b] | Sort s -> Sort_cs (family_of_sort s), -1, [] - | _ -> - begin + | _ -> + begin try Const_cs (global_of_constr t) , -1, [] with - _ -> raise Not_found - end + _ -> raise Not_found + end (* Intended to always succeed *) let compute_canonical_projections (con,ind) = let v = mkConst con in let c = Environ.constant_value (Global.env()) con in - let lt,t = Reductionops.splay_lambda (Global.env()) Evd.empty c in + let lt,t = Reductionops.splay_lam (Global.env()) Evd.empty c in let lt = List.rev (List.map snd lt) in let args = snd (decompose_app t) in - let { s_EXPECTEDPARAM = p; s_PROJ = lpj; s_PROJKIND = kl } = + let { s_EXPECTEDPARAM = p; s_PROJ = lpj; s_PROJKIND = kl } = lookup_structure ind in let params, projs = list_chop p args in let lpj = keep_true_projections lpj kl in @@ -180,31 +227,55 @@ let compute_canonical_projections (con,ind) = match spopt with | Some proji_sp -> begin - try + try let patt, n , args = cs_pattern_of_constr t in ((ConstRef proji_sp, patt, n, args) :: l) - with Not_found -> l + with Not_found -> + if Flags.is_verbose () then + (let con_pp = Nametab.pr_global_env Idset.empty (ConstRef con) + and proji_sp_pp = Nametab.pr_global_env Idset.empty (ConstRef proji_sp) in + msg_warning (str "No global reference exists for projection value" + ++ print_constr t ++ str " in instance " + ++ con_pp ++ str " of " ++ proji_sp_pp ++ str ", ignoring it.")); + l end | _ -> l) [] lps in List.map (fun (refi,c,inj,argj) -> (refi,c), - {o_DEF=v; o_INJ=inj; o_TABS=lt; + {o_DEF=v; o_INJ=inj; o_TABS=lt; o_TPARAMS=params; o_NPARAMS=List.length params; o_TCOMPS=argj}) comp +let pr_cs_pattern = function + Const_cs c -> Nametab.pr_global_env Idset.empty c + | Prod_cs -> str "_ -> _" + | Default_cs -> str "_" + | Sort_cs s -> Termops.pr_sort_family s + let open_canonical_structure i (_,o) = if i=1 then let lo = compute_canonical_projections o in List.iter (fun ((proj,cs_pat),s) -> let l = try Refmap.find proj !object_table with Not_found -> [] in - if not (List.mem_assoc cs_pat l) then - object_table := Refmap.add proj ((cs_pat,s)::l) !object_table) lo + let ocs = try Some (List.assoc cs_pat l) + with Not_found -> None + in match ocs with + | None -> object_table := Refmap.add proj ((cs_pat,s)::l) !object_table; + | Some cs -> + if Flags.is_verbose () then + let old_can_s = (Termops.print_constr cs.o_DEF) + and new_can_s = (Termops.print_constr s.o_DEF) in + let prj = (Nametab.pr_global_env Idset.empty proj) + and hd_val = (pr_cs_pattern cs_pat) in + msg_warning (str "Ignoring canonical projection to " ++ hd_val + ++ str " by " ++ prj ++ str " in " + ++ new_can_s ++ str ": redundant with " ++ old_can_s)) lo let cache_canonical_structure o = open_canonical_structure 1 o -let subst_canonical_structure (_,subst,(cst,ind as obj)) = +let subst_canonical_structure (subst,(cst,ind as obj)) = (* invariant: cst is an evaluable reference. Thus we can take *) (* the first component of subst_con. *) let cst' = fst (subst_con subst cst) in @@ -215,13 +286,12 @@ let discharge_canonical_structure (_,(cst,ind)) = Some (Lib.discharge_con cst,Lib.discharge_inductive ind) let (inCanonStruc,outCanonStruct) = - declare_object {(default_object "CANONICAL-STRUCTURE") with + declare_object {(default_object "CANONICAL-STRUCTURE") with open_function = open_canonical_structure; cache_function = cache_canonical_structure; subst_function = subst_canonical_structure; - classify_function = (fun (_,x) -> Substitute x); - discharge_function = discharge_canonical_structure; - export_function = (function x -> Some x) } + classify_function = (fun x -> Substitute x); + discharge_function = discharge_canonical_structure } let add_canonical_structure x = Lib.add_anonymous_leaf (inCanonStruc x) @@ -229,7 +299,7 @@ let add_canonical_structure x = Lib.add_anonymous_leaf (inCanonStruc x) let error_not_structure ref = errorlabstrm "object_declare" - (Nameops.pr_id (id_of_global ref) ++ str" is not a structure object.") + (Nameops.pr_id (basename_of_global ref) ++ str" is not a structure object.") let check_and_decompose_canonical_structure ref = let sp = match ref with ConstRef sp -> sp | _ -> error_not_structure ref in @@ -237,7 +307,7 @@ let check_and_decompose_canonical_structure ref = let vc = match Environ.constant_opt_value env sp with | Some vc -> vc | None -> error_not_structure ref in - let body = snd (splay_lambda (Global.env()) Evd.empty vc) in + let body = snd (splay_lam (Global.env()) Evd.empty vc) in let f,args = match kind_of_term body with | App (f,args) -> f,args | _ -> error_not_structure ref in @@ -259,16 +329,16 @@ let lookup_canonical_conversion (proj,pat) = List.assoc pat (Refmap.find proj !object_table) let is_open_canonical_projection sigma (c,args) = - try + try let l = Refmap.find (global_of_constr c) !object_table in let n = (snd (List.hd l)).o_NPARAMS in - try isEvar (whd_evar sigma (List.nth args n)) with Failure _ -> false + try isEvar_or_Meta (whd_evar sigma (List.nth args n)) with Failure _ -> false with Not_found -> false let freeze () = !structure_table, !projection_table, !object_table -let unfreeze (s,p,o) = +let unfreeze (s,p,o) = structure_table := s; projection_table := p; object_table := o let init () = @@ -277,10 +347,8 @@ let init () = let _ = init() -let _ = +let _ = Summary.declare_summary "objdefs" { Summary.freeze_function = freeze; Summary.unfreeze_function = unfreeze; - Summary.init_function = init; - Summary.survive_module = false; - Summary.survive_section = false } + Summary.init_function = init } -- cgit v1.2.3