diff options
| -rw-r--r-- | interp/declare.ml | 21 | ||||
| -rw-r--r-- | pretyping/recordops.ml | 83 | ||||
| -rw-r--r-- | pretyping/recordops.mli | 11 | ||||
| -rw-r--r-- | vernac/canonical.ml | 39 | ||||
| -rw-r--r-- | vernac/canonical.mli | 12 | ||||
| -rw-r--r-- | vernac/record.ml | 24 | ||||
| -rw-r--r-- | vernac/record.mli | 2 | ||||
| -rw-r--r-- | vernac/vernac.mllib | 1 | ||||
| -rw-r--r-- | vernac/vernacentries.ml | 4 |
9 files changed, 118 insertions, 79 deletions
diff --git a/interp/declare.ml b/interp/declare.ml index 717f8ef49a..76b4bab2ce 100644 --- a/interp/declare.ml +++ b/interp/declare.ml @@ -346,6 +346,25 @@ let inInductive : mutual_inductive_entry -> obj = discharge_function = discharge_inductive; rebuild_function = rebuild_inductive } +let cache_prim (_,(p,c)) = Recordops.register_primitive_projection p c + +let load_prim _ p = cache_prim p + +let subst_prim (subst,(p,c)) = Mod_subst.subst_proj_repr subst p, Mod_subst.subst_constant subst c + +let discharge_prim (_,(p,c)) = Some (Lib.discharge_proj_repr p, c) + +let inPrim : (Projection.Repr.t * Constant.t) -> obj = + declare_object { + (default_object "PRIMPROJS") with + cache_function = cache_prim ; + load_function = load_prim; + subst_function = subst_prim; + classify_function = (fun x -> Substitute x); + discharge_function = discharge_prim } + +let declare_primitive_projection p c = Lib.add_anonymous_leaf (inPrim (p,c)) + let declare_one_projection univs (mind,_ as ind) ~proj_npars proj_arg label (term,types) = let id = Label.to_id label in let univs, u = match univs with @@ -360,7 +379,7 @@ let declare_one_projection univs (mind,_ as ind) ~proj_npars proj_arg label (ter let entry = definition_entry ~types ~univs term in let cst = declare_constant id (DefinitionEntry entry, IsDefinition StructureComponent) in let p = Projection.Repr.make ind ~proj_npars ~proj_arg label in - Recordops.declare_primitive_projection p cst + declare_primitive_projection p cst let declare_projections univs mind = diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index ef56458f99..1feb8acd5f 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -21,7 +21,6 @@ open Pp open Names open Globnames open Constr -open Libobject open Mod_subst open Reductionops @@ -50,10 +49,10 @@ let projection_table = type struc_tuple = constructor * (Name.t * bool) list * Constant.t option list -let load_structure i (_, (id,kl,projs)) = +let register_structure env (id,kl,projs) = let open Declarations in let ind = fst id in - let mib, mip = Global.lookup_inductive ind in + let mib, mip = Inductive.lookup_mind_specif env ind in let n = mib.mind_nparams in let struc = { s_CONST = id; s_EXPECTEDPARAM = n; s_PROJ = projs; s_PROJKIND = kl } in @@ -62,10 +61,7 @@ let load_structure i (_, (id,kl,projs)) = 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, (id, kl, projs as obj)) = +let subst_structure subst (id, kl, projs as obj) = let projs' = (* invariant: struc.s_PROJ is an evaluable reference. Thus we can take *) (* the first component of subst_con. *) @@ -77,19 +73,6 @@ let subst_structure (subst, (id, kl, projs as obj)) = if projs' == projs && id' == id then obj else (id',kl,projs') -let discharge_structure (_, x) = Some x - -let inStruc : struc_tuple -> obj = - 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 } - -let declare_structure o = - Lib.add_anonymous_leaf (inStruc o) - let lookup_structure indsp = Indmap.find indsp !structure_table let lookup_projections indsp = (lookup_structure indsp).s_PROJ @@ -107,26 +90,9 @@ let is_projection cst = Cmap.mem cst !projection_table let prim_table = Summary.ref (Cmap_env.empty : Projection.Repr.t Cmap_env.t) ~name:"record-prim-projs" -let load_prim i (_,(p,c)) = +let register_primitive_projection p c = prim_table := Cmap_env.add c p !prim_table -let cache_prim p = load_prim 1 p - -let subst_prim (subst,(p,c)) = subst_proj_repr subst p, subst_constant subst c - -let discharge_prim (_,(p,c)) = Some (Lib.discharge_proj_repr p, c) - -let inPrim : (Projection.Repr.t * Constant.t) -> obj = - declare_object { - (default_object "PRIMPROJS") with - cache_function = cache_prim ; - load_function = load_prim; - subst_function = subst_prim; - classify_function = (fun x -> Substitute x); - discharge_function = discharge_prim } - -let declare_primitive_projection p c = Lib.add_anonymous_leaf (inPrim (p,c)) - let is_primitive_projection c = Cmap_env.mem c !prim_table let find_primitive_projection c = @@ -224,7 +190,7 @@ let warn_projection_no_head_constant = ++ con_pp ++ str " of " ++ proji_sp_pp ++ strbrk ", ignoring it.") (* Intended to always succeed *) -let compute_canonical_projections env warn (con,ind) = +let compute_canonical_projections env ~warn (con,ind) = let ctx = Environ.constant_context env con in let u = Univ.make_abstract_instance ctx in let v = (mkConstU (con,u)) in @@ -274,11 +240,8 @@ let warn_redundant_canonical_projection = ++ strbrk " by " ++ prj ++ strbrk " in " ++ new_can_s ++ strbrk ": redundant with " ++ old_can_s) -let add_canonical_structure warn o = - (* XXX: Undesired global access to env *) - let env = Global.env () in - let sigma = Evd.from_env env in - compute_canonical_projections env warn o |> +let register_canonical_structure ~warn env sigma o = + compute_canonical_projections env ~warn o |> List.iter (fun ((proj, (cs_pat, _ as pat)), s) -> let l = try GlobRef.Map.find proj !object_table with Not_found -> [] in match assoc_pat cs_pat l with @@ -294,31 +257,13 @@ let add_canonical_structure warn o = warn_redundant_canonical_projection (hd_val, prj, new_can_s, old_can_s) ) -let open_canonical_structure i (_, o) = - if Int.equal i 1 then add_canonical_structure false o - -let cache_canonical_structure (_, o) = - add_canonical_structure true 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' = 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 (_,x) = Some x - -let inCanonStruc : Constant.t * inductive -> obj = - 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 } - -let add_canonical_structure x = Lib.add_anonymous_leaf (inCanonStruc x) - (*s High-level declaration of a canonical structure *) let error_not_structure ref description = @@ -327,20 +272,17 @@ let error_not_structure ref description = (Id.print (Nametab.basename_of_global ref) ++ str"." ++ spc() ++ description)) -let check_and_decompose_canonical_structure ref = +let check_and_decompose_canonical_structure env sigma ref = let sp = match ref with ConstRef sp -> sp | _ -> error_not_structure ref (str "Expected an instance of a record or structure.") in - let env = Global.env () 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 (str "Could not find its value in the global environment.") in - let env = Global.env () in - let evd = Evd.from_env env in - let body = snd (splay_lam (Global.env()) evd (EConstr.of_constr vc)) in + let body = snd (splay_lam env sigma (EConstr.of_constr vc)) in let body = EConstr.Unsafe.to_constr body in let f,args = match kind body with | App (f,args) -> f,args @@ -353,15 +295,12 @@ let check_and_decompose_canonical_structure ref = try lookup_structure indsp with Not_found -> error_not_structure ref - (str "Could not find the record or structure " ++ Termops.Internal.print_constr_env env evd (EConstr.mkInd indsp)) in + (str "Could not find the record or structure " ++ Termops.Internal.print_constr_env env sigma (EConstr.mkInd 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 (str "Got too few arguments to the record or structure constructor."); (sp,indsp) -let declare_canonical_structure ref = - add_canonical_structure (check_and_decompose_canonical_structure ref) - let lookup_canonical_conversion (proj,pat) = assoc_pat pat (GlobRef.Map.find proj !object_table) diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli index 53a33f6bab..f0594d513a 100644 --- a/pretyping/recordops.mli +++ b/pretyping/recordops.mli @@ -26,7 +26,8 @@ type struc_typ = { type struc_tuple = constructor * (Name.t * bool) list * Constant.t option list -val declare_structure : struc_tuple -> unit +val register_structure : Environ.env -> struc_tuple -> unit +val subst_structure : Mod_subst.substitution -> struc_tuple -> struc_tuple (** [lookup_structure isp] returns the struc_typ associated to the inductive path [isp] if it corresponds to a structure, otherwise @@ -47,7 +48,7 @@ val find_projection : GlobRef.t -> struc_typ val is_projection : Constant.t -> bool (** Sets up the mapping from constants to primitive projections *) -val declare_primitive_projection : Projection.Repr.t -> Constant.t -> unit +val register_primitive_projection : Projection.Repr.t -> Constant.t -> unit val is_primitive_projection : Constant.t -> bool @@ -80,8 +81,12 @@ val cs_pattern_of_constr : Environ.env -> constr -> cs_pattern * int option * co val pr_cs_pattern : cs_pattern -> Pp.t val lookup_canonical_conversion : (GlobRef.t * cs_pattern) -> constr * obj_typ -val declare_canonical_structure : GlobRef.t -> unit +val register_canonical_structure : warn:bool -> Environ.env -> Evd.evar_map -> + Constant.t * inductive -> unit +val subst_canonical_structure : Mod_subst.substitution -> Constant.t * inductive -> Constant.t * inductive val is_open_canonical_projection : Environ.env -> Evd.evar_map -> Reductionops.state -> bool val canonical_projections : unit -> ((GlobRef.t * cs_pattern) * obj_typ) list + +val check_and_decompose_canonical_structure : Environ.env -> Evd.evar_map -> GlobRef.t -> Constant.t * inductive diff --git a/vernac/canonical.ml b/vernac/canonical.ml new file mode 100644 index 0000000000..92d5731f92 --- /dev/null +++ b/vernac/canonical.ml @@ -0,0 +1,39 @@ +(************************************************************************) +(* * 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 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) +open Names +open Libobject +open Recordops + +let open_canonical_structure i (_, o) = + let env = Global.env () in + let sigma = Evd.from_env env in + if Int.equal i 1 then register_canonical_structure env sigma ~warn:false o + +let cache_canonical_structure (_, o) = + let env = Global.env () in + let sigma = Evd.from_env env in + register_canonical_structure ~warn:true env sigma o + +let discharge_canonical_structure (_,x) = Some x + +let inCanonStruc : Constant.t * inductive -> obj = + declare_object {(default_object "CANONICAL-STRUCTURE") with + open_function = open_canonical_structure; + cache_function = cache_canonical_structure; + subst_function = (fun (subst,c) -> subst_canonical_structure subst c); + classify_function = (fun x -> Substitute x); + discharge_function = discharge_canonical_structure } + +let add_canonical_structure x = Lib.add_anonymous_leaf (inCanonStruc x) + +let declare_canonical_structure ref = + let env = Global.env () in + let sigma = Evd.from_env env in + add_canonical_structure (check_and_decompose_canonical_structure env sigma ref) diff --git a/vernac/canonical.mli b/vernac/canonical.mli new file mode 100644 index 0000000000..5b223a0615 --- /dev/null +++ b/vernac/canonical.mli @@ -0,0 +1,12 @@ +(************************************************************************) +(* * 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 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) +open Names + +val declare_canonical_structure : GlobRef.t -> unit diff --git a/vernac/record.ml b/vernac/record.ml index a7c5318f11..74e5a03659 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -30,6 +30,7 @@ open Constrexpr open Constrexpr_ops open Goptions open Context.Rel.Declaration +open Libobject module RelDecl = Context.Rel.Declaration @@ -373,6 +374,27 @@ let declare_projections indsp ctx ?(kind=StructureComponent) binder_name coers f open Typeclasses +let load_structure i (_, structure) = + Recordops.register_structure (Global.env()) structure + +let cache_structure o = + load_structure 1 o + +let subst_structure (subst, (id, kl, projs as obj)) = + Recordops.subst_structure subst obj + +let discharge_structure (_, x) = Some x + +let inStruc : Recordops.struc_tuple -> obj = + 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 } + +let declare_structure_entry o = + Lib.add_anonymous_leaf (inStruc o) let declare_structure ~cum finite ubinders univs paramimpls params template ?(kind=StructureComponent) ?name record_data = let nparams = List.length params in @@ -443,7 +465,7 @@ let declare_structure ~cum finite ubinders univs paramimpls params template ?(ki let kinds,sp_projs = declare_projections rsp ctx ~kind binder_name.(i) coers fieldimpls fields in let build = ConstructRef cstr in let () = if is_coe then Class.try_add_new_coercion build ~local:false poly in - let () = Recordops.declare_structure(cstr, List.rev kinds, List.rev sp_projs) in + let () = declare_structure_entry (cstr, List.rev kinds, List.rev sp_projs) in rsp in List.mapi map record_data diff --git a/vernac/record.mli b/vernac/record.mli index 9852840d12..12a2a765b5 100644 --- a/vernac/record.mli +++ b/vernac/record.mli @@ -24,6 +24,8 @@ val declare_projections : Constr.rel_context -> (Name.t * bool) list * Constant.t option list +val declare_structure_entry : Recordops.struc_tuple -> unit + val definition_structure : universe_decl_expr option -> inductive_kind -> template:bool option -> Decl_kinds.cumulative_inductive_flag -> Decl_kinds.polymorphic -> diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib index 3ee785413c..7f5c265eea 100644 --- a/vernac/vernac.mllib +++ b/vernac/vernac.mllib @@ -12,6 +12,7 @@ Vernacextend Ppvernac Proof_using Lemmas +Canonical Class Egramcoq Metasyntax diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 7ef3777445..a8dfc9cb5a 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -572,7 +572,7 @@ let vernac_definition_hook p = function | Coercion -> Some (Class.add_coercion_hook p) | CanonicalStructure -> - Some (Lemmas.mk_hook (fun _ _ _ -> Recordops.declare_canonical_structure)) + Some (Lemmas.mk_hook (fun _ _ _ -> Canonical.declare_canonical_structure)) | SubClass -> Some (Class.add_subclass_hook p) | _ -> None @@ -1041,7 +1041,7 @@ let vernac_require from import qidl = (* Coercions and canonical structures *) let vernac_canonical r = - Recordops.declare_canonical_structure (smart_global r) + Canonical.declare_canonical_structure (smart_global r) let vernac_coercion ~atts ref qids qidt = let local, polymorphic = Attributes.(parse Notations.(locality ++ polymorphic) atts) in |