diff options
Diffstat (limited to 'library')
| -rw-r--r-- | library/declare.ml | 17 | ||||
| -rw-r--r-- | library/declare.mli | 7 | ||||
| -rw-r--r-- | library/global.mli | 2 | ||||
| -rw-r--r-- | library/impargs.ml | 10 | ||||
| -rw-r--r-- | library/lib.ml | 4 | ||||
| -rw-r--r-- | library/lib.mli | 1 | ||||
| -rw-r--r-- | library/libnames.ml | 11 | ||||
| -rw-r--r-- | library/libnames.mli | 2 |
8 files changed, 36 insertions, 18 deletions
diff --git a/library/declare.ml b/library/declare.ml index ea986e3fbe..ecf223ae00 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -142,9 +142,9 @@ let cache_constant ((sp,kn),(cdt,kind)) = errorlabstrm "cache_constant" (pr_id id ++ str " already exists")); let _,dir,_ = repr_kn kn in let kn' = Global.add_constant dir (basename sp) cdt in - if kn' <> kn then + if kn' <> (constant_of_kn kn) then anomaly "Kernel and Library names do not match"; - Nametab.push (Nametab.Until 1) sp (ConstRef kn); + Nametab.push (Nametab.Until 1) sp (ConstRef kn'); csttab := Spmap.add sp kind !csttab (* At load-time, the segment starting from the module name to the discharge *) @@ -154,11 +154,11 @@ let load_constant i ((sp,kn),(_,kind)) = let (_,id) = repr_path sp in errorlabstrm "cache_constant" (pr_id id ++ str " already exists")); csttab := Spmap.add sp kind !csttab; - Nametab.push (Nametab.Until i) sp (ConstRef kn) + Nametab.push (Nametab.Until i) sp (ConstRef (constant_of_kn kn)) (* Opening means making the name without its module qualification available *) let open_constant i ((sp,kn),_) = - Nametab.push (Nametab.Exactly i) sp (ConstRef kn) + Nametab.push (Nametab.Exactly i) sp (ConstRef (constant_of_kn kn)) (* Hack to reduce the size of .vo: we keep only what load/open needs *) let dummy_constant_entry = ConstantEntry (ParameterEntry mkProp) @@ -190,16 +190,17 @@ let hcons_constant_declaration = function let declare_constant_common id discharged_hyps (cd,kind) = let (sp,kn as oname) = add_leaf id (in_constant (cd,kind)) in + let kn = constant_of_kn kn in declare_constant_implicits kn; Symbols.declare_ref_arguments_scope (ConstRef kn); Dischargedhypsmap.set_discharged_hyps sp discharged_hyps; - oname + kn let declare_constant_gen internal id (cd,kind) = let cd = hcons_constant_declaration cd in - let oname = declare_constant_common id [] (ConstantEntry cd,kind) in - !xml_declare_constant (internal,oname); - oname + let kn = declare_constant_common id [] (ConstantEntry cd,kind) in + !xml_declare_constant (internal,kn); + kn let declare_internal_constant = declare_constant_gen true let declare_constant = declare_constant_gen false diff --git a/library/declare.mli b/library/declare.mli index a025982ee0..6af5138881 100644 --- a/library/declare.mli +++ b/library/declare.mli @@ -52,10 +52,11 @@ type constant_declaration = constant_entry * global_kind (* [declare_constant id cd] declares a global declaration (constant/parameter) with name [id] in the current section; it returns the full path of the declaration *) -val declare_constant : identifier -> constant_declaration -> object_name +val declare_constant : + identifier -> constant_declaration -> constant val declare_internal_constant : - identifier -> constant_declaration -> object_name + identifier -> constant_declaration -> constant val redeclare_constant : identifier -> Dischargedhypsmap.discharged_hyps -> @@ -98,5 +99,5 @@ val strength_of_global : global_reference -> strength (* hooks for XML output *) val set_xml_declare_variable : (object_name -> unit) -> unit -val set_xml_declare_constant : (bool * object_name -> unit) -> unit +val set_xml_declare_constant : (bool * constant -> unit) -> unit val set_xml_declare_inductive : (bool * object_name -> unit) -> unit diff --git a/library/global.mli b/library/global.mli index 70ab9b5632..9468f3ef52 100644 --- a/library/global.mli +++ b/library/global.mli @@ -40,7 +40,7 @@ val push_named_def : (identifier * constr * types option) -> Univ.constraints functions verify that given names match those generated by kernel *) val add_constant : - dir_path -> identifier -> global_declaration -> kernel_name + dir_path -> identifier -> global_declaration -> constant val add_mind : dir_path -> identifier -> mutual_inductive_entry -> kernel_name diff --git a/library/impargs.ml b/library/impargs.ml index 5bf920014b..d775433673 100644 --- a/library/impargs.ml +++ b/library/impargs.ml @@ -289,7 +289,7 @@ let list_of_implicits = function (*s Constants. *) -let constants_table = ref KNmap.empty +let constants_table = ref Cmap.empty let compute_constant_implicits kn = let env = Global.env () in @@ -297,7 +297,7 @@ let compute_constant_implicits kn = auto_implicits env (body_of_type cb.const_type) let constant_implicits sp = - try KNmap.find sp !constants_table with Not_found -> No_impl,No_impl + try Cmap.find sp !constants_table with Not_found -> No_impl,No_impl (*s Inductives and constructors. Their implicit arguments are stored in an array, indexed by the inductive number, of pairs $(i,v)$ where @@ -349,7 +349,7 @@ let cache_implicits_decl (r,imps) = | VarRef id -> var_table := Idmap.add id imps !var_table | ConstRef kn -> - constants_table := KNmap.add kn imps !constants_table + constants_table := Cmap.add kn imps !constants_table | IndRef indp -> inductives_table := Indmap.add indp imps !inductives_table; | ConstructRef consp -> @@ -485,7 +485,7 @@ let test_if_implicit find a = with Not_found -> (false,false,false),(false,false,false) let is_implicit_constant sp = - test_if_implicit (KNmap.find sp) !constants_table + test_if_implicit (Cmap.find sp) !constants_table let is_implicit_inductive_definition indp = test_if_implicit (Indmap.find (indp,0)) !inductives_table @@ -496,7 +496,7 @@ let is_implicit_var id = (*s Registration as global tables *) let init () = - constants_table := KNmap.empty; + constants_table := Cmap.empty; inductives_table := Indmap.empty; constructors_table := Constrmap.empty; var_table := Idmap.empty diff --git a/library/lib.ml b/library/lib.ml index c27c9c04c5..16521e627b 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -105,6 +105,10 @@ let make_kn id = let mp,dir = current_prefix () in Names.make_kn mp dir (label_of_id id) +let make_con id = + let mp,dir = current_prefix () in + Names.make_con mp dir (label_of_id id) + let make_oname id = make_path id, make_kn id diff --git a/library/lib.mli b/library/lib.mli index d80822056d..438754a381 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -82,6 +82,7 @@ val make_path : identifier -> section_path (* Kernel-side names *) val current_prefix : unit -> module_path * dir_path val make_kn : identifier -> kernel_name +val make_con : identifier -> constant (* Are we inside an opened section *) val sections_are_opened : unit -> bool diff --git a/library/libnames.ml b/library/libnames.ml index 17fd50b7f2..2fe8f724c4 100644 --- a/library/libnames.ml +++ b/library/libnames.ml @@ -23,7 +23,7 @@ type global_reference = let subst_global subst ref = match ref with | VarRef _ -> ref | ConstRef kn -> - let kn' = subst_kn subst kn in if kn==kn' then ref else + let kn' = subst_con subst kn in if kn==kn' then ref else ConstRef kn' | IndRef (kn,i) -> let kn' = subst_kn subst kn in if kn==kn' then ref else @@ -190,6 +190,8 @@ type extended_global_reference = let encode_kn dir id = make_kn (MPfile dir) empty_dirpath (label_of_id id) +let encode_con dir id = make_con (MPfile dir) empty_dirpath (label_of_id id) + let decode_kn kn = let mp,sec_dir,l = repr_kn kn in match mp,(repr_dirpath sec_dir) with @@ -197,6 +199,13 @@ let decode_kn kn = | _ , [] -> anomaly "MPfile expected!" | _ -> anomaly "Section part should be empty!" +let decode_con kn = + let mp,sec_dir,l = repr_con kn in + match mp,(repr_dirpath sec_dir) with + MPfile dir,[] -> (dir,id_of_label l) + | _ , [] -> anomaly "MPfile expected!" + | _ -> anomaly "Section part should be empty!" + (*s qualified names *) type qualid = section_path diff --git a/library/libnames.mli b/library/libnames.mli index ffb51ec0bb..539aa0b963 100644 --- a/library/libnames.mli +++ b/library/libnames.mli @@ -86,6 +86,8 @@ type extended_global_reference = val encode_kn : dir_path -> identifier -> kernel_name val decode_kn : kernel_name -> dir_path * identifier +val encode_con : dir_path -> identifier -> constant +val decode_con : constant -> dir_path * identifier (*s A [qualid] is a partially qualified ident; it includes fully |