summaryrefslogtreecommitdiff
path: root/pretyping/recordops.ml
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/recordops.ml')
-rw-r--r--pretyping/recordops.ml221
1 files changed, 90 insertions, 131 deletions
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 *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* Created by Amokrane Saïbi, Dec 1998 *)
+(* Created by Amokrane Saïbi, Dec 1998 *)
(* Addition of products and sorts in canonical structures by Pierre
Corbineau, Feb 2008 *)
(* This file registers properties of records: projections and
canonical structures *)
+open Errors
open Util
open Pp
open Names
-open Libnames
+open Globnames
open Nametab
open Term
-open Typeops
open Libobject
-open Library
open Mod_subst
open Reductionops
@@ -29,25 +28,27 @@ open Reductionops
constructor (the name of which defaults to Build_S) *)
(* Table des structures: le nom de la structure (un [inductive]) donne
- le nom du constructeur, le nombre de paramètres et pour chaque
- argument réel du constructeur, le nom de la projection
- correspondante, si valide, et un booléen disant si c'est une vraie
- projection ou bien une fonction constante (associée à un LetIn) *)
+ le nom du constructeur, le nombre de paramètres et pour chaque
+ argument réel du constructeur, le nom de la projection
+ correspondante, si valide, et un booléen disant si c'est une vraie
+ projection ou bien une fonction constante (associée à un LetIn) *)
type struc_typ = {
s_CONST : constructor;
s_EXPECTEDPARAM : int;
- s_PROJKIND : (name * bool) list;
+ s_PROJKIND : (Name.t * bool) list;
s_PROJ : constant option list }
-let structure_table = ref (Indmap.empty : struc_typ Indmap.t)
-let projection_table = ref Cmap.empty
+let structure_table =
+ Summary.ref (Indmap.empty : struc_typ Indmap.t) ~name:"record-structs"
+let projection_table =
+ Summary.ref Cmap.empty ~name:"record-projs"
(* TODO: could be unify struc_typ and struc_tuple ? in particular,
is the inductive always (fst constructor) ? It seems so... *)
type struc_tuple =
- inductive * constructor * (name * bool) list * constant option list
+ inductive * constructor * (Name.t * bool) list * constant option list
let load_structure i (_,(ind,id,kl,projs)) =
let n = (fst (Global.lookup_inductive ind)).Declarations.mind_nparams in
@@ -62,12 +63,12 @@ let cache_structure o =
load_structure 1 o
let subst_structure (subst,((kn,i),id,kl,projs as obj)) =
- let kn' = subst_ind subst kn in
+ let kn' = subst_mind 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
- (Option.smartmap (fun kn -> 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 }
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-16 13:36:14 +0000