summaryrefslogtreecommitdiff
path: root/library/declare.ml
diff options
context:
space:
mode:
Diffstat (limited to 'library/declare.ml')
-rw-r--r--library/declare.ml70
1 files changed, 29 insertions, 41 deletions
diff --git a/library/declare.ml b/library/declare.ml
index 14cddd6c..88503b42 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: declare.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
-
(** This module is about the low-level declaration of logical objects *)
open Pp
@@ -80,7 +78,10 @@ let discharge_variable (_,o) = match o with
| Inr (id,_) -> Some (Inl (variable_constraints id))
| Inl _ -> Some o
-let (inVariable,_) =
+type variable_obj =
+ (Univ.constraints, identifier * variable_declaration) union
+
+let inVariable : variable_obj -> obj =
declare_object { (default_object "VARIABLE") with
cache_function = cache_variable;
discharge_function = discharge_variable;
@@ -105,20 +106,26 @@ type constant_declaration = constant_entry * logical_kind
let load_constant i ((sp,kn),(_,_,kind)) =
if Nametab.exists_cci sp then
alreadydeclared (pr_id (basename sp) ++ str " already exists");
- let con = Global.constant_of_delta (constant_of_kn kn) in
+ let con = Global.constant_of_delta_kn kn in
Nametab.push (Nametab.Until i) sp (ConstRef con);
add_constant_kind con kind
(* Opening means making the name without its module qualification available *)
let open_constant i ((sp,kn),_) =
- let con = Global.constant_of_delta (constant_of_kn kn) in
+ let con = Global.constant_of_delta_kn kn in
Nametab.push (Nametab.Exactly i) sp (ConstRef con)
+let exists_name id =
+ variable_exists id or Global.exists_objlabel (label_of_id id)
+
+let check_exists sp =
+ let id = basename sp in
+ if exists_name id then alreadydeclared (pr_id id ++ str " already exists")
+
let cache_constant ((sp,kn),(cdt,dhyps,kind)) =
let id = basename sp in
let _,dir,_ = repr_kn kn in
- if variable_exists id or Nametab.exists_cci sp then
- alreadydeclared (pr_id id ++ str " already exists");
+ check_exists sp;
let kn' = Global.add_constant dir id cdt in
assert (kn' = constant_of_kn kn);
Nametab.push (Nametab.Until 1) sp (ConstRef (constant_of_kn kn));
@@ -141,13 +148,16 @@ let discharge_constant ((sp,kn),(cdt,dhyps,kind)) =
Some (GlobalRecipe recipe,(discharged_hyps kn sechyps)@dhyps,kind)
(* Hack to reduce the size of .vo: we keep only what load/open needs *)
-let dummy_constant_entry = ConstantEntry (ParameterEntry (mkProp,false))
+let dummy_constant_entry = ConstantEntry (ParameterEntry (None,mkProp,None))
let dummy_constant (ce,_,mk) = dummy_constant_entry,[],mk
let classify_constant cst = Substitute (dummy_constant cst)
-let (inConstant,_) =
+type constant_obj =
+ global_declaration * Dischargedhypsmap.discharged_hyps * logical_kind
+
+let inConstant : constant_obj -> obj =
declare_object { (default_object "CONSTANT") with
cache_function = cache_constant;
load_function = load_constant;
@@ -156,35 +166,19 @@ let (inConstant,_) =
subst_function = ident_subst_function;
discharge_function = discharge_constant }
-let hcons_constant_declaration = function
- | DefinitionEntry ce when !Flags.hash_cons_proofs ->
- let (hcons1_constr,_) = hcons_constr (hcons_names()) in
- DefinitionEntry
- { const_entry_body = hcons1_constr ce.const_entry_body;
- const_entry_type = Option.map hcons1_constr ce.const_entry_type;
- const_entry_opaque = ce.const_entry_opaque;
- const_entry_boxed = ce.const_entry_boxed }
- | cd -> cd
-
let declare_constant_common id dhyps (cd,kind) =
let (sp,kn) = add_leaf id (inConstant (cd,dhyps,kind)) in
- let c = Global.constant_of_delta (constant_of_kn kn) in
+ let c = Global.constant_of_delta_kn kn in
declare_constant_implicits c;
Heads.declare_head (EvalConstRef c);
Notation.declare_ref_arguments_scope (ConstRef c);
c
-let declare_constant_gen internal id (cd,kind) =
- let cd = hcons_constant_declaration cd in
+let declare_constant ?(internal = UserVerbose) id (cd,kind) =
let kn = declare_constant_common id [] (ConstantEntry cd,kind) in
!xml_declare_constant (internal,kn);
kn
-(* TODO: add a third function to distinguish between KernelVerbose
- * and user Verbose *)
-let declare_internal_constant = declare_constant_gen KernelSilent
-let declare_constant = declare_constant_gen UserVerbose
-
(** Declaration of inductive blocks *)
let declare_inductive_argument_scopes kn mie =
@@ -196,7 +190,7 @@ let declare_inductive_argument_scopes kn mie =
let inductive_names sp kn mie =
let (dp,_) = repr_path sp in
- let kn = Global.mind_of_delta (mind_of_kn kn) in
+ let kn = Global.mind_of_delta_kn kn in
let names, _ =
List.fold_left
(fun (names, n) ind ->
@@ -215,16 +209,8 @@ let inductive_names sp kn mie =
([], 0) mie.mind_entry_inds
in names
-let check_exists_inductive (sp,_) =
- (if variable_exists (basename sp) then
- alreadydeclared (pr_id (basename sp) ++ str " already exists"));
- if Nametab.exists_cci sp then
- let (_,id) = repr_path sp in
- alreadydeclared (pr_id id ++ str " already exists")
-
let load_inductive i ((sp,kn),(_,mie)) =
let names = inductive_names sp kn mie in
- List.iter check_exists_inductive names;
List.iter (fun (sp, ref) -> Nametab.push (Nametab.Until i) sp ref ) names
let open_inductive i ((sp,kn),(_,mie)) =
@@ -233,7 +219,7 @@ let open_inductive i ((sp,kn),(_,mie)) =
let cache_inductive ((sp,kn),(dhyps,mie)) =
let names = inductive_names sp kn mie in
- List.iter check_exists_inductive names;
+ List.iter check_exists (List.map fst names);
let id = basename sp in
let _,dir,_ = repr_kn kn in
let kn' = Global.add_mind dir id mie in
@@ -245,7 +231,7 @@ let cache_inductive ((sp,kn),(dhyps,mie)) =
let discharge_inductive ((sp,kn),(dhyps,mie)) =
- let mind = (Global.mind_of_delta (mind_of_kn kn)) in
+ let mind = Global.mind_of_delta_kn kn in
let mie = Global.lookup_mind mind in
let repl = replacement_context () in
let sechyps = section_segment_of_mutual_inductive mind in
@@ -266,7 +252,9 @@ let dummy_inductive_entry (_,m) = ([],{
mind_entry_finite = true;
mind_entry_inds = List.map dummy_one_inductive_entry m.mind_entry_inds })
-let (inInductive,_) =
+type inductive_obj = Dischargedhypsmap.discharged_hyps * mutual_inductive_entry
+
+let inInductive : inductive_obj -> obj =
declare_object {(default_object "INDUCTIVE") with
cache_function = cache_inductive;
load_function = load_inductive;
@@ -281,7 +269,7 @@ let declare_mind isrecord mie =
| ind::_ -> ind.mind_entry_typename
| [] -> anomaly "cannot declare an empty list of inductives" in
let (sp,kn as oname) = add_leaf id (inInductive ([],mie)) in
- let mind = (Global.mind_of_delta (mind_of_kn kn)) in
+ let mind = Global.mind_of_delta_kn kn in
declare_mib_implicits mind;
declare_inductive_argument_scopes mind mie;
!xml_declare_inductive (isrecord,oname);