From 7cfc4e5146be5666419451bdd516f1f3f264d24a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 25 Jan 2015 14:42:51 +0100 Subject: Imported Upstream version 8.5~beta1+dfsg --- pretyping/recordops.ml | 221 ++++++++++++++++++++----------------------------- 1 file changed, 90 insertions(+), 131 deletions(-) (limited to 'pretyping/recordops.ml') diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index f9cd3501..6dc0d1f3 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -1,27 +1,26 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* fst (subst_con subst kn))) + List.smartmap + (Option.smartmap (fun kn -> fst (subst_con_kn subst kn))) projs in let id' = fst (subst_constructor subst id) in @@ -104,56 +105,6 @@ 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 : constr * MethodsDnet.ident -> obj = - 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 *) (* the effective components of a structure and the projections of the *) @@ -163,16 +114,18 @@ let declare_method cons ev sign = c := [x1:B1]...[xk:Bk](Build_R a1...am t1...t_n) - If ti has the form (ci ui1...uir) where ci is a global reference and -if the corresponding projection Li of the structure R is defined, one -declare a "conversion" between ci and Li + If ti has the form (ci ui1...uir) where ci is a global reference (or + a sort, or a product or a reference to a parameter) and if the + corresponding projection Li of the structure R is defined, one + declares a "conversion" between ci and Li. x1:B1..xk:Bk |- (Li a1..am (c x1..xk)) =_conv (ci ui1...uir) -that maps the pair (Li,ci) to the following data + that maps the pair (Li,ci) to the following data o_DEF = c o_TABS = B1...Bk + o_INJ = Some n (when ci is a reference to the parameter xi) o_PARAMS = a1...am o_NARAMS = m o_TCOMP = ui1...uir @@ -181,7 +134,8 @@ that maps the pair (Li,ci) to the following data type obj_typ = { o_DEF : constr; - o_INJ : int; (* position of trivial argument (negative= none) *) + o_CTX : Univ.ContextSet.t; + o_INJ : int option; (* position of trivial argument if any *) o_TABS : constr list; (* ordered *) o_TPARAMS : constr list; (* ordered *) o_NPARAMS : int; @@ -193,42 +147,60 @@ type cs_pattern = | Sort_cs of sorts_family | Default_cs -let object_table = ref (Refmap.empty : (cs_pattern * obj_typ) list Refmap.t) +let eq_cs_pattern p1 p2 = match p1, p2 with +| Const_cs gr1, Const_cs gr2 -> eq_gr gr1 gr2 +| Prod_cs, Prod_cs -> true +| Sort_cs s1, Sort_cs s2 -> Sorts.family_equal s1 s2 +| Default_cs, Default_cs -> true +| _ -> false + +let rec assoc_pat a = function + | ((pat, t), e) :: xs -> if eq_cs_pattern pat a then (t, e) else assoc_pat a xs + | [] -> raise Not_found + + +let object_table = + Summary.ref (Refmap.empty : ((cs_pattern * constr) * obj_typ) list Refmap.t) + ~name:"record-canonical-structs" let canonical_projections () = - Refmap.fold (fun x -> List.fold_right (fun (y,c) acc -> ((x,y),c)::acc)) + Refmap.fold (fun x -> List.fold_right (fun ((y,_),c) acc -> ((x,y),c)::acc)) !object_table [] let keep_true_projections projs kinds = - map_succeed (function (p,(_,true)) -> p | _ -> failwith "") - (List.combine projs kinds) + let filter (p, (_, b)) = if b then Some p else None in + List.map_filter filter (List.combine projs kinds) let cs_pattern_of_constr t = match kind_of_term t with App (f,vargs) -> begin - try Const_cs (global_of_constr f) , -1, Array.to_list vargs + try Const_cs (global_of_constr f) , None, Array.to_list vargs with e when Errors.noncritical e -> raise Not_found end - | Rel n -> Default_cs, pred n, [] - | Prod (_,a,b) when not (Termops.dependent (mkRel 1) b) -> Prod_cs, -1, [a; Termops.pop b] - | Sort s -> Sort_cs (family_of_sort s), -1, [] + | Rel n -> Default_cs, Some n, [] + | Prod (_,a,b) when not (Termops.dependent (mkRel 1) b) -> Prod_cs, None, [a; Termops.pop b] + | Sort s -> Sort_cs (family_of_sort s), None, [] | _ -> begin - try Const_cs (global_of_constr t) , -1, [] + try Const_cs (global_of_constr t) , None, [] with e when Errors.noncritical e -> 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_lam (Global.env()) Evd.empty c in - let lt = List.rev (List.map snd lt) in + let env = Global.env () in + let ctx = Environ.constant_context env con in + let u = Univ.UContext.instance ctx in + let v = (mkConstU (con,u)) in + let ctx = Univ.ContextSet.of_context ctx in + let c = Environ.constant_value_in env (con,u) in + let lt,t = Reductionops.splay_lam env Evd.empty c in + let lt = List.rev_map snd lt in let args = snd (decompose_app t) in let { s_EXPECTEDPARAM = p; s_PROJ = lpj; s_PROJKIND = kl } = lookup_structure ind in - let params, projs = list_chop p args in + let params, projs = List.chop p args in let lpj = keep_true_projections lpj kl in let lps = List.combine lpj projs in let comp = @@ -239,48 +211,48 @@ let compute_canonical_projections (con,ind) = begin try let patt, n , args = cs_pattern_of_constr t in - ((ConstRef proji_sp, patt, n, args) :: l) + ((ConstRef proji_sp, patt, t, n, args) :: 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" - ++ Termops.print_constr t ++ str " in instance " - ++ con_pp ++ str " of " ++ proji_sp_pp ++ str ", ignoring it.")); + (let con_pp = Nametab.pr_global_env Id.Set.empty (ConstRef con) + and proji_sp_pp = Nametab.pr_global_env Id.Set.empty (ConstRef proji_sp) in + msg_warning (strbrk "No global reference exists for projection value" + ++ Termops.print_constr t ++ strbrk " in instance " + ++ con_pp ++ str " of " ++ proji_sp_pp ++ strbrk ", 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; + List.map (fun (refi,c,t,inj,argj) -> + (refi,(c,t)), + {o_DEF=v; o_CTX=ctx; 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 + Const_cs c -> Nametab.pr_global_env Id.Set.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 + if Int.equal i 1 then let lo = compute_canonical_projections o in - List.iter (fun ((proj,cs_pat),s) -> + List.iter (fun ((proj,(cs_pat,_ as pat)),s) -> let l = try Refmap.find proj !object_table with Not_found -> [] in - let ocs = try Some (List.assoc cs_pat l) + let ocs = try Some (assoc_pat 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 -> + | None -> object_table := Refmap.add proj ((pat,s)::l) !object_table; + | Some (c, 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) + let prj = (Nametab.pr_global_env Id.Set.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 + msg_warning (strbrk "Ignoring canonical projection to " ++ hd_val + ++ strbrk " by " ++ prj ++ strbrk " in " + ++ new_can_s ++ strbrk ": redundant with " ++ old_can_s)) lo let cache_canonical_structure o = open_canonical_structure 1 o @@ -288,9 +260,9 @@ let cache_canonical_structure o = 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 - let ind' = Inductiveops.subst_inductive subst ind in - if cst' == cst & ind' == ind then obj else (cst',ind') + let cst' = subst_constant subst cst in + let ind' = subst_ind subst ind in + if cst' == cst && ind' == ind then obj else (cst',ind') let discharge_canonical_structure (_,(cst,ind)) = Some (Lib.discharge_con cst,Lib.discharge_inductive ind) @@ -314,7 +286,9 @@ let error_not_structure ref = let check_and_decompose_canonical_structure ref = let sp = match ref with ConstRef sp -> sp | _ -> error_not_structure ref in let env = Global.env () in - let vc = match Environ.constant_opt_value env sp with + let ctx = Environ.constant_context env sp in + let u = Univ.UContext.instance ctx in + let vc = match Environ.constant_opt_value_in env (sp, u) with | Some vc -> vc | None -> error_not_structure ref in let body = snd (splay_lam (Global.env()) Evd.empty vc) in @@ -322,7 +296,7 @@ let check_and_decompose_canonical_structure ref = | App (f,args) -> f,args | _ -> error_not_structure ref in let indsp = match kind_of_term f with - | Construct (indsp,1) -> indsp + | Construct ((indsp,1),u) -> indsp | _ -> error_not_structure ref in let s = try lookup_structure indsp with Not_found -> error_not_structure ref in let ntrue_projs = List.length (List.filter (fun (_, x) -> x) s.s_PROJKIND) in @@ -334,32 +308,17 @@ let declare_canonical_structure ref = add_canonical_structure (check_and_decompose_canonical_structure ref) let lookup_canonical_conversion (proj,pat) = - List.assoc pat (Refmap.find proj !object_table) + assoc_pat pat (Refmap.find proj !object_table) let is_open_canonical_projection env sigma (c,args) = try - let n = find_projection_nparams (global_of_constr c) in + let ref = global_of_constr c in + let n = find_projection_nparams ref in + (** Check if there is some canonical projection attached to this structure *) + let _ = Refmap.find ref !object_table in try - let arg = whd_betadeltaiota env sigma (List.nth args n) in + let arg = whd_betadeltaiota env sigma (Stack.nth args n) in let hd = match kind_of_term arg with App (hd, _) -> hd | _ -> arg in - not (isConstruct hd) + not (isConstruct hd) with Failure _ -> false with Not_found -> false - -let freeze () = - !structure_table, !projection_table, !object_table - -let unfreeze (s,p,o) = - structure_table := s; projection_table := p; object_table := o - -let init () = - structure_table := Indmap.empty; projection_table := Cmap.empty; - object_table := Refmap.empty - -let _ = init() - -let _ = - Summary.declare_summary "objdefs" - { Summary.freeze_function = freeze; - Summary.unfreeze_function = unfreeze; - Summary.init_function = init } -- cgit v1.2.3