summaryrefslogtreecommitdiff
path: root/pretyping/recordops.ml
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/recordops.ml')
-rw-r--r--pretyping/recordops.ml128
1 files changed, 80 insertions, 48 deletions
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index 284af0cb..d070edea 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -1,9 +1,11 @@
(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
(* Created by Amokrane Saïbi, Dec 1998 *)
@@ -19,7 +21,7 @@ open Pp
open Names
open Globnames
open Nametab
-open Term
+open Constr
open Libobject
open Mod_subst
open Reductionops
@@ -37,7 +39,7 @@ type struc_typ = {
s_CONST : constructor;
s_EXPECTEDPARAM : int;
s_PROJKIND : (Name.t * bool) list;
- s_PROJ : constant option list }
+ s_PROJ : Constant.t option list }
let structure_table =
Summary.ref (Indmap.empty : struc_typ Indmap.t) ~name:"record-structs"
@@ -48,7 +50,7 @@ let projection_table =
is the inductive always (fst constructor) ? It seems so... *)
type struc_tuple =
- inductive * constructor * (Name.t * bool) list * constant option list
+ inductive * constructor * (Name.t * bool) list * Constant.t option list
let load_structure i (_,(ind,id,kl,projs)) =
let n = (fst (Global.lookup_inductive ind)).Declarations.mind_nparams in
@@ -134,7 +136,7 @@ let find_projection = function
type obj_typ = {
o_DEF : constr;
- o_CTX : Univ.ContextSet.t;
+ o_CTX : Univ.AUContext.t;
o_INJ : int option; (* position of trivial argument if any *)
o_TABS : constr list; (* ordered *)
o_TPARAMS : constr list; (* ordered *)
@@ -144,7 +146,7 @@ type obj_typ = {
type cs_pattern =
Const_cs of global_reference
| Prod_cs
- | Sort_cs of sorts_family
+ | Sort_cs of Sorts.family
| Default_cs
let eq_cs_pattern p1 p2 = match p1, p2 with
@@ -171,16 +173,20 @@ let keep_true_projections 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
+let cs_pattern_of_constr env t =
+ match kind t with
App (f,vargs) ->
begin
try Const_cs (global_of_constr f) , None, Array.to_list vargs
with e when CErrors.noncritical e -> raise Not_found
end
| 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, []
+ | Prod (_,a,b) when Vars.noccurn 1 b -> Prod_cs, None, [a; Vars.lift (-1) b]
+ | Proj (p, c) ->
+ let { Environ.uj_type = ty } = Typeops.infer env c in
+ let _, params = Inductive.find_rectype env ty in
+ Const_cs (ConstRef (Projection.constant p)), None, params @ [c]
+ | Sort s -> Sort_cs (Sorts.family s), None, []
| _ ->
begin
try Const_cs (global_of_constr t) , None, []
@@ -189,27 +195,33 @@ let cs_pattern_of_constr t =
let warn_projection_no_head_constant =
CWarnings.create ~name:"projection-no-head-constant" ~category:"typechecker"
- (fun (t,con_pp,proji_sp_pp) ->
+ (fun (sign,env,t,con,proji_sp) ->
+ let env = Termops.push_rels_assum sign env in
+ let con_pp = Nametab.pr_global_env Id.Set.empty (ConstRef con) in
+ let proji_sp_pp = Nametab.pr_global_env Id.Set.empty (ConstRef proji_sp) in
+ let term_pp = Termops.print_constr_env env Evd.empty (EConstr.of_constr t) in
strbrk "Projection value has no head constant: "
- ++ Termops.print_constr t ++ strbrk " in canonical instance "
+ ++ term_pp ++ strbrk " in canonical instance "
++ con_pp ++ str " of " ++ proji_sp_pp ++ strbrk ", ignoring it.")
(* Intended to always succeed *)
let compute_canonical_projections warn (con,ind) =
let env = Global.env () in
- let ctx = Univ.instantiate_univ_context (Environ.constant_context env con) in
- let u = Univ.UContext.instance ctx in
+ let ctx = Environ.constant_context env con in
+ let u = Univ.make_abstract_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 sign,t = Reductionops.splay_lam env Evd.empty (EConstr.of_constr c) in
+ let sign = List.map (on_snd EConstr.Unsafe.to_constr) sign in
+ let t = EConstr.Unsafe.to_constr t in
+ let lt = List.rev_map snd sign 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 lpj = keep_true_projections lpj kl in
let lps = List.combine lpj projs in
+ let nenv = Termops.push_rels_assum sign env in
let comp =
List.fold_left
(fun l (spopt,t) -> (* comp=components *)
@@ -217,12 +229,10 @@ let compute_canonical_projections warn (con,ind) =
| Some proji_sp ->
begin
try
- let patt, n , args = cs_pattern_of_constr t in
+ let patt, n , args = cs_pattern_of_constr nenv t in
((ConstRef proji_sp, patt, t, n, args) :: l)
with Not_found ->
- 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
- if warn then warn_projection_no_head_constant (t,con_pp,proji_sp_pp);
+ if warn then warn_projection_no_head_constant (sign,env,t,con,proji_sp);
l
end
| _ -> l)
@@ -255,8 +265,8 @@ let add_canonical_structure warn o =
in match ocs with
| None -> object_table := Refmap.add proj ((pat,s)::l) !object_table;
| Some (c, cs) ->
- let old_can_s = (Termops.print_constr cs.o_DEF)
- and new_can_s = (Termops.print_constr s.o_DEF) in
+ let old_can_s = (Termops.print_constr (EConstr.of_constr cs.o_DEF))
+ and new_can_s = (Termops.print_constr (EConstr.of_constr s.o_DEF)) in
let prj = (Nametab.pr_global_env Id.Set.empty proj)
and hd_val = (pr_cs_pattern cs_pat) in
if warn then warn_redundant_canonical_projection (hd_val,prj,new_can_s,old_can_s))
@@ -278,7 +288,7 @@ let subst_canonical_structure (subst,(cst,ind as obj)) =
let discharge_canonical_structure (_,(cst,ind)) =
Some (Lib.discharge_con cst,Lib.discharge_inductive ind)
-let inCanonStruc : constant * inductive -> obj =
+let inCanonStruc : Constant.t * inductive -> obj =
declare_object {(default_object "CANONICAL-STRUCTURE") with
open_function = open_canonical_structure;
cache_function = cache_canonical_structure;
@@ -290,29 +300,40 @@ let add_canonical_structure x = Lib.add_anonymous_leaf (inCanonStruc x)
(*s High-level declaration of a canonical structure *)
-let error_not_structure ref =
- errorlabstrm "object_declare"
- (Nameops.pr_id (basename_of_global ref) ++ str" is not a structure object.")
+let error_not_structure ref description =
+ user_err ~hdr:"object_declare"
+ (str"Could not declare a canonical structure " ++
+ (Id.print (basename_of_global ref) ++ str"." ++ spc() ++
+ str(description)))
let check_and_decompose_canonical_structure ref =
- let sp = match ref with ConstRef sp -> sp | _ -> error_not_structure ref in
+ let sp =
+ match ref with
+ ConstRef sp -> sp
+ | _ -> error_not_structure ref "Expected an instance of a record or structure."
+ in
let env = Global.env () in
- let ctx = Environ.constant_context env sp in
- let u = Univ.UContext.instance ctx in
+ let u = Univ.make_abstract_instance (Environ.constant_context env sp) 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
- let f,args = match kind_of_term body with
+ | None -> error_not_structure ref "Could not find its value in the global environment." in
+ let body = snd (splay_lam (Global.env()) Evd.empty (EConstr.of_constr vc)) (** FIXME *) in
+ let body = EConstr.Unsafe.to_constr body in
+ let f,args = match kind body with
| App (f,args) -> f,args
- | _ -> error_not_structure ref in
- let indsp = match kind_of_term f with
+ | _ ->
+ error_not_structure ref "Expected a record or structure constructor applied to arguments." in
+ let indsp = match kind f with
| Construct ((indsp,1),u) -> indsp
- | _ -> error_not_structure ref in
- let s = try lookup_structure indsp with Not_found -> error_not_structure ref in
+ | _ -> error_not_structure ref "Expected an instance of a record or structure." in
+ let s =
+ try lookup_structure indsp
+ with Not_found ->
+ error_not_structure ref
+ ("Could not find the record or structure " ^ (MutInd.to_string (fst indsp))) in
let ntrue_projs = List.count snd s.s_PROJKIND in
if s.s_EXPECTEDPARAM + ntrue_projs > Array.length args then
- error_not_structure ref;
+ error_not_structure ref "Got too few arguments to the record or structure constructor.";
(sp,indsp)
let declare_canonical_structure ref =
@@ -321,15 +342,26 @@ let declare_canonical_structure ref =
let lookup_canonical_conversion (proj,pat) =
assoc_pat pat (Refmap.find proj !object_table)
+let decompose_projection sigma c args =
+ match EConstr.kind sigma c with
+ | Const (c, u) ->
+ let n = find_projection_nparams (ConstRef c) in
+ (** Check if there is some canonical projection attached to this structure *)
+ let _ = Refmap.find (ConstRef c) !object_table in
+ let arg = Stack.nth args n in
+ arg
+ | Proj (p, c) ->
+ let _ = Refmap.find (ConstRef (Projection.constant p)) !object_table in
+ c
+ | _ -> raise Not_found
+
let is_open_canonical_projection env sigma (c,args) =
+ let open EConstr in
try
- 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
+ let arg = decompose_projection sigma c args in
try
- let arg = whd_all env sigma (Stack.nth args n) in
- let hd = match kind_of_term arg with App (hd, _) -> hd | _ -> arg in
- not (isConstruct hd)
+ let arg = whd_all env sigma arg in
+ let hd = match EConstr.kind sigma arg with App (hd, _) -> hd | _ -> arg in
+ not (isConstruct sigma hd)
with Failure _ -> false
with Not_found -> false
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-07 14:24:54 +0000