1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(* $Id: global.ml,v 1.43.2.1 2004/07/16 19:30:35 herbelin Exp $ *)
open Util
open Names
open Term
open Sign
open Environ
open Safe_typing
open Summary
(* We introduce here the global environment of the system, and we declare it
as a synchronized table. *)
let global_env = ref empty_environment
let safe_env () = !global_env
let env () = env_of_safe_env !global_env
let _ =
declare_summary "Global environment"
{ freeze_function = (fun () -> !global_env);
unfreeze_function = (fun fr -> global_env := fr);
init_function = (fun () -> global_env := empty_environment);
survive_module = true;
survive_section = false }
(* Then we export the functions of [Typing] on that environment. *)
let universes () = universes (env())
let named_context () = named_context (env())
let push_named_assum a =
let (cst,env) = push_named_assum a !global_env in
global_env := env;
cst
let push_named_def d =
let (cst,env) = push_named_def d !global_env in
global_env := env;
cst
(*let add_thing add kn thing =
let _,dir,l = repr_kn kn in
let kn',newenv = add dir l thing !global_env in
if kn = kn' then
global_env := newenv
else
anomaly "Kernel names do not match."
*)
let add_thing add dir id thing =
let kn, newenv = add dir (label_of_id id) thing !global_env in
global_env := newenv;
kn
let add_constant = add_thing add_constant
let add_mind = add_thing add_mind
let add_modtype = add_thing (fun _ -> add_modtype) ()
let add_module = add_thing (fun _ -> add_module) ()
let add_constraints c = global_env := add_constraints c !global_env
let set_engagement c = global_env := set_engagement c !global_env
let start_module id params mtyo =
let l = label_of_id id in
let mp,newenv = start_module l params mtyo !global_env in
global_env := newenv;
mp
let end_module id =
let l = label_of_id id in
let mp,newenv = end_module l !global_env in
global_env := newenv;
mp
let start_modtype id params =
let l = label_of_id id in
let mp,newenv = start_modtype l params !global_env in
global_env := newenv;
mp
let end_modtype id =
let l = label_of_id id in
let kn,newenv = end_modtype l !global_env in
global_env := newenv;
kn
let lookup_named id = lookup_named id (env())
let lookup_constant kn = lookup_constant kn (env())
let lookup_inductive ind = Inductive.lookup_mind_specif (env()) ind
let lookup_mind kn = lookup_mind kn (env())
let lookup_module mp = lookup_module mp (env())
let lookup_modtype kn = lookup_modtype kn (env())
let start_library dir =
let mp,newenv = start_library dir !global_env in
global_env := newenv;
mp
let export s = snd (export !global_env s)
let import cenv digest =
let mp,newenv = import cenv digest !global_env in
global_env := newenv;
mp
(*s Function to get an environment from the constants part of the global
environment and a given context. *)
let env_of_context hyps =
reset_with_named_context hyps (env())
open Libnames
let type_of_reference env = function
| VarRef id -> let (_,_,t) = Environ.lookup_named id env in t
| ConstRef c -> Environ.constant_type env c
| IndRef ind -> Inductive.type_of_inductive env ind
| ConstructRef cstr -> Inductive.type_of_constructor env cstr
let type_of_global t = type_of_reference (env ()) t
(*let get_kn dp l =
make_kn (current_modpath !global_env) dp l
*)
|