← Back to branch summary

~ubuntu-branches/ubuntu/wily/coq-doc/wily

« back to all changes in this revision

Viewing changes to library/global.ml

  • Committer: Bazaar Package Importer
  • Author(s): Stéphane Glondu, Stéphane Glondu, Samuel Mimram
  • Date: 2010-01-07 22:50:39 UTC
  • mfrom: (1.2.2 upstream)
  • Revision ID: james.westby@ubuntu.com-20100107225039-n3cq82589u0qt0s2
Tags: 8.2pl1-1
http://bugs.debian.org/563669
http://bugs.debian.org/543545
[ Stéphane Glondu ]
* New upstream release (Closes: #563669)
  - remove patches
* Packaging overhaul:
  - use git, advertise it in Vcs-* fields of debian/control
  - use debhelper 7 and dh with override
  - use source format 3.0 (quilt)
* debian/control:
  - set Maintainer to d-o-m, set Uploaders to Sam and myself
  - add Homepage field
  - bump Standards-Version to 3.8.3
* Register PDF documentation into doc-base
* Add debian/watch
* Update debian/copyright

[ Samuel Mimram ]
* Change coq-doc's description to mention that it provides documentation in
  pdf format, not postscript, closes: #543545.

Show diffs side-by-side

added added

removed removed

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