← Back to branch summary

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

« back to all changes in this revision

Viewing changes to checker/environ.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:
checker/environ.ml
 
1
open Util
 
2
open Names
 
3
open Univ
 
4
open Term
 
5
open Declarations
 
6
 
 
7
type globals = {
 
8
  env_constants : constant_body Cmap.t;
 
9
  env_inductives : mutual_inductive_body KNmap.t;
 
10
  env_modules : module_body MPmap.t;
 
11
  env_modtypes : module_type_body MPmap.t;
 
12
  env_alias : module_path MPmap.t }
 
13
 
 
14
type stratification = {
 
15
  env_universes : universes;
 
16
  env_engagement : engagement option
 
17
}
 
18
 
 
19
type env = {
 
20
    env_globals       : globals;
 
21
    env_named_context : named_context;
 
22
    env_rel_context   : rel_context;
 
23
    env_stratification : stratification;
 
24
    env_imports : Digest.t MPmap.t }
 
25
 
 
26
let empty_env = {
 
27
  env_globals =
 
28
  { env_constants = Cmap.empty;
 
29
    env_inductives = KNmap.empty;
 
30
    env_modules = MPmap.empty;
 
31
    env_modtypes = MPmap.empty;
 
32
    env_alias = MPmap.empty };
 
33
  env_named_context = [];
 
34
  env_rel_context = [];
 
35
  env_stratification =
 
36
  { env_universes = Univ.initial_universes;
 
37
    env_engagement = None};
 
38
  env_imports = MPmap.empty }
 
39
 
 
40
let engagement env = env.env_stratification.env_engagement
 
41
let universes env = env.env_stratification.env_universes
 
42
let named_context env = env.env_named_context
 
43
let rel_context env = env.env_rel_context
 
44
 
 
45
let set_engagement c env =
 
46
  match env.env_stratification.env_engagement with
 
47
    | Some c' -> if c=c' then env else error "Incompatible engagement"
 
48
    | None ->
 
49
        { env with env_stratification =
 
50
          { env.env_stratification with env_engagement = Some c } }
 
51
 
 
52
(* Digests *)
 
53
 
 
54
let add_digest env dp digest =
 
55
  { env with env_imports = MPmap.add (MPfile dp) digest env.env_imports }
 
56
 
 
57
let lookup_digest env dp =
 
58
  MPmap.find (MPfile dp) env.env_imports
 
59
 
 
60
(* Rel context *)
 
61
let lookup_rel n env =
 
62
  let rec lookup_rel n sign =
 
63
    match n, sign with
 
64
      | 1, decl :: _ -> decl
 
65
      | n, _ :: sign -> lookup_rel (n-1) sign
 
66
      | _, []        -> raise Not_found in
 
67
  lookup_rel n env.env_rel_context
 
68
 
 
69
let push_rel d env =
 
70
    { env with
 
71
      env_rel_context = d :: env.env_rel_context }
 
72
 
 
73
let push_rel_context ctxt x = fold_rel_context push_rel ctxt ~init:x
 
74
    
 
75
let push_rec_types (lna,typarray,_) env =
 
76
  let ctxt = array_map2_i (fun i na t -> (na, None, lift i t)) lna typarray in
 
77
  Array.fold_left (fun e assum -> push_rel assum e) env ctxt
 
78
 
 
79
(* Named context *)
 
80
 
 
81
let push_named d env = 
 
82
(*  if not (env.env_rel_context = []) then raise (ASSERT env.env_rel_context);
 
83
  assert (env.env_rel_context = []); *)
 
84
    { env with  
 
85
      env_named_context = d :: env.env_named_context }
 
86
 
 
87
let lookup_named id env =
 
88
  let rec lookup_named id = function
 
89
    | (id',_,_ as decl) :: _ when id=id' -> decl
 
90
    | _ :: sign -> lookup_named id sign
 
91
    | [] -> raise Not_found in
 
92
  lookup_named id env.env_named_context
 
93
 
 
94
(* A local const is evaluable if it is defined  *)
 
95
 
 
96
let named_type id env =
 
97
  let (_,_,t) = lookup_named id env in t
 
98
 
 
99
(* Universe constraints *)
 
100
let add_constraints c env =
 
101
  if c == Constraint.empty then 
 
102
    env 
 
103
  else
 
104
    let s = env.env_stratification in
 
105
    { env with env_stratification = 
 
106
      { s with env_universes = merge_constraints c s.env_universes } }
 
107
 
 
108
(* Global constants *)
 
109
 
 
110
let lookup_constant kn env =
 
111
  Cmap.find kn env.env_globals.env_constants
 
112
 
 
113
let add_constant kn cs env =
 
114
  let new_constants = 
 
115
    Cmap.add kn cs env.env_globals.env_constants in
 
116
  let new_globals = 
 
117
    { env.env_globals with 
 
118
        env_constants = new_constants } in 
 
119
  { env with env_globals = new_globals }
 
120
 
 
121
(* constant_type gives the type of a constant *)
 
122
let constant_type env kn =
 
123
  let cb = lookup_constant kn env in
 
124
  cb.const_type  
 
125
 
 
126
type const_evaluation_result = NoBody | Opaque
 
127
 
 
128
exception NotEvaluableConst of const_evaluation_result
 
129
 
 
130
let constant_value env kn =
 
131
  let cb = lookup_constant kn env in
 
132
  if cb.const_opaque then raise (NotEvaluableConst Opaque);
 
133
  match cb.const_body with
 
134
    | Some l_body -> force_constr l_body
 
135
    | None -> raise (NotEvaluableConst NoBody)
 
136
 
 
137
let constant_opt_value env cst =
 
138
  try Some (constant_value env cst)
 
139
  with NotEvaluableConst _ -> None
 
140
 
 
141
(* A global const is evaluable if it is defined and not opaque *)
 
142
let evaluable_constant cst env =
 
143
  try let _  = constant_value env cst in true
 
144
  with Not_found | NotEvaluableConst _ -> false
 
145
 
 
146
(* Mutual Inductives *)
 
147
let lookup_mind kn env =
 
148
  KNmap.find kn env.env_globals.env_inductives
 
149
 
 
150
let rec scrape_mind env kn = 
 
151
  match (lookup_mind kn env).mind_equiv with
 
152
    | None -> kn
 
153
    | Some kn' -> scrape_mind env kn'
 
154
 
 
155
let add_mind kn mib env =
 
156
  let new_inds = KNmap.add kn mib env.env_globals.env_inductives in
 
157
  let new_globals = 
 
158
    { env.env_globals with 
 
159
        env_inductives = new_inds } in
 
160
  { env with env_globals = new_globals }
 
161
 
 
162
let rec mind_equiv env (kn1,i1) (kn2,i2) =
 
163
  let rec equiv kn1 kn2 =
 
164
    kn1 = kn2 ||
 
165
    scrape_mind env kn1 = scrape_mind env kn2 in
 
166
  i1 = i2 && equiv kn1 kn2
 
167
 
 
168
 
 
169
(* Modules *)
 
170
 
 
171
let add_modtype ln mtb env = 
 
172
  let new_modtypes = MPmap.add ln mtb env.env_globals.env_modtypes in
 
173
  let new_globals = 
 
174
    { env.env_globals with 
 
175
        env_modtypes = new_modtypes } in
 
176
  { env with env_globals = new_globals }
 
177
 
 
178
let shallow_add_module mp mb env = 
 
179
  let new_mods = MPmap.add mp mb env.env_globals.env_modules in
 
180
  let new_globals = 
 
181
    { env.env_globals with 
 
182
        env_modules = new_mods } in
 
183
  { env with env_globals = new_globals }
 
184
 
 
185
let register_alias mp1 mp2 env =
 
186
  let new_alias =  MPmap.add mp1 mp2 env.env_globals.env_alias in
 
187
  let new_globals = 
 
188
    { env.env_globals with 
 
189
        env_alias = new_alias } in
 
190
    { env with env_globals = new_globals }
 
191
 
 
192
let rec scrape_alias mp env = 
 
193
  try
 
194
    let mp1 = MPmap.find mp env.env_globals.env_alias in
 
195
      scrape_alias mp1 env
 
196
  with
 
197
      Not_found -> mp
 
198
 
 
199
let lookup_module mp env = 
 
200
  MPmap.find mp env.env_globals.env_modules
 
201
 
 
202
let lookup_modtype ln env = 
 
203
  MPmap.find ln env.env_globals.env_modtypes