diff options
Diffstat (limited to 'library')
| -rw-r--r-- | library/declare.ml | 42 | ||||
| -rw-r--r-- | library/declare.mli | 8 | ||||
| -rw-r--r-- | library/global.mli | 2 |
3 files changed, 51 insertions, 1 deletions
diff --git a/library/declare.ml b/library/declare.ml index 60a1c5960d..cb5ec1b40d 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -3,6 +3,9 @@ open Util open Names +open Generic +open Term +open Sign open Constant open Inductive open Libobject @@ -126,3 +129,42 @@ let declare_mind mie = push_inductive_names sp mie; declare_inductive_implicits sp + +(* Global references. *) + +let first f v = + let n = Array.length v in + let rec look_for i = + if i = n then raise Not_found; + try f i v.(i) with Not_found -> look_for (succ i) + in + look_for 0 + +let mind_oper_of_id sp id mib = + first + (fun tyi mip -> + if id = mip.mind_typename then + MutInd (sp,tyi) + else + first + (fun cj cid -> + if id = cid then + MutConstruct((sp,tyi),succ cj) + else raise Not_found) + mip.mind_consnames) + mib.mind_packets + +let global_operator sp id = + try + let _ = Global.lookup_constant sp in Const sp + with Not_found -> + let mib = Global.lookup_mind sp in + mind_oper_of_id sp id mib + +let global_reference id = + let sp = Nametab.sp_of_id CCI id in + let oper = global_operator sp id in + let hyps = get_globals (Global.context ()) in + let ids = ids_of_sign hyps in + DOPN(oper, Array.of_list (List.map (fun id -> VAR id) ids)) + diff --git a/library/declare.mli b/library/declare.mli index 21486c250e..f7a0fa0884 100644 --- a/library/declare.mli +++ b/library/declare.mli @@ -23,3 +23,11 @@ val declare_constant : identifier -> constant_entry -> unit val declare_mind : mutual_inductive_entry -> unit + +(*s It also provides a function [global_reference] to construct a global + constr (a constant, an inductive or a constructor) from an identifier. + To do so, it first looks for the section path using [Nametab.sp_of_id] and + then constructs the corresponding term, associated to the current + environment of variables. *) + +val global_reference : identifier -> constr diff --git a/library/global.mli b/library/global.mli index 89cc83cbd5..2e0a541df2 100644 --- a/library/global.mli +++ b/library/global.mli @@ -13,7 +13,7 @@ open Typing (*i*) (* This module defines the global environment of Coq. - The functions below are the exactly the same as the ones in [Typing], + The functions below are exactly the same as the ones in [Typing], operating on that global environment. *) val env : unit -> environment |