summaryrefslogtreecommitdiff
path: root/pretyping/recordops.ml
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/recordops.ml')
-rw-r--r--pretyping/recordops.ml154
1 files changed, 111 insertions, 43 deletions
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 }
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-16 16:28:55 +0000