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
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
|
(***********************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
(* \VV/ *************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(***********************************************************************)
(*i $Id$ i*)
(*i*)
open Names
open Term
open Declarations
open Univ
open Sign
(*i*)
(*s Unsafe environments. We define here a datatype for environments.
Since typing is not yet defined, it is not possible to check the
informations added in environments, and that is why we speak here
of ``unsafe'' environments. *)
type context
type env
val empty_context : context
val empty_env : env
val universes : env -> universes
val context : env -> context
val rel_context : env -> rel_context
val named_context : env -> named_context
(* This forgets named and rel contexts *)
val reset_context : env -> env
(*s This concerns only local vars referred by names [named_context] *)
val push_named_decl : named_declaration -> env -> env
val push_named_assum : identifier * types -> env -> env
val push_named_def : identifier * constr * types -> env -> env
val change_hyps : (named_context -> named_context) -> env -> env
val instantiate_named_context : named_context -> constr list -> (identifier * constr) list
val pop_named_decl : identifier -> env -> env
(*s This concerns only local vars referred by indice [rel_context] *)
val push_rel : rel_declaration -> env -> env
val push_rel_assum : name * types -> env -> env
val push_rel_def : name * constr * types -> env -> env
val push_rels : rel_context -> env -> env
val push_rels_assum : (name * types) list -> env -> env
val names_of_rel_context : env -> names_context
(*s Returns also the substitution to be applied to rel's *)
val push_rel_context_to_named_context : env -> constr list * env
(*s Push the types of a (co-)fixpoint to [rel_context] *)
val push_rec_types : rec_declaration -> env -> env
(*s Push the types of a (co-)fixpoint to [named_context] *)
val push_named_rec_types : rec_declaration -> env -> env
(* Gives identifiers in [named_context] and [rel_context] *)
val ids_of_context : env -> identifier list
val map_context : (constr -> constr) -> env -> env
(*s Recurrence on [named_context] *)
val fold_named_context : (env -> named_declaration -> 'a -> 'a) -> env -> 'a -> 'a
val process_named_context : (env -> named_declaration -> env) -> env -> env
(* Recurrence on [named_context] starting from younger decl *)
val fold_named_context_reverse : ('a -> named_declaration -> 'a) -> 'a -> env -> 'a
(* [process_named_context_both_sides f env] iters [f] on the named
declarations of [env] taking as argument both the initial segment, the
middle value and the tail segment *)
val process_named_context_both_sides :
(env -> named_declaration -> named_context -> env) -> env -> env
(*s Recurrence on [rel_context] *)
val fold_rel_context : (env -> rel_declaration -> 'a -> 'a) -> env -> 'a -> 'a
val process_rel_context : (env -> rel_declaration -> env) -> env -> env
(*s add entries to environment *)
val set_universes : universes -> env -> env
val add_constraints : constraints -> env -> env
val add_constant :
section_path -> constant_body -> env -> env
val add_mind :
section_path -> mutual_inductive_body -> env -> env
(*s Looks up in environment *)
(* Looks up in the context of local vars referred by names ([named_context]) *)
(* raises [Not_found] if the identifier is not found *)
val lookup_named_type : identifier -> env -> types
val lookup_named_value : identifier -> env -> constr option
val lookup_named : identifier -> env -> constr option * types
(* Looks up in the context of local vars referred by indice ([rel_context]) *)
(* raises [Not_found] if the index points out of the context *)
val lookup_rel_type : int -> env -> name * types
val lookup_rel_value : int -> env -> constr option
(* Looks up in the context of global constant names *)
(* raises [Not_found] if the required path is not found *)
val lookup_constant : constant -> env -> constant_body
(* Looks up in the context of global inductive names *)
(* raises [Not_found] if the required path is not found *)
val lookup_mind : section_path -> env -> mutual_inductive_body
(* Looks up the array of section variables used by a global (constant,
inductive or constructor). *)
val lookup_constant_variables : constant -> env -> constr array
val lookup_inductive_variables : inductive -> env -> constr array
val lookup_constructor_variables : constructor -> env -> constr array
(*s Miscellanous *)
val sp_of_global : env -> global_reference -> section_path
val id_of_global : env -> global_reference -> identifier
val make_all_name_different : env -> env
(*s Functions creating names for anonymous names *)
val id_of_name_using_hdchar : env -> constr -> name -> identifier
(* [named_hd env t na] just returns [na] is it defined, otherwise it
creates a name built from [t] (e.g. ["n"] if [t] is [nat]) *)
val named_hd : env -> constr -> name -> name
(* [lambda_name env (na,t,c)] builds [[[x:t]c] where [x] is created
using [named_hd] if [na] is [Anonymous]; [prod_name env (na,t,c)]
works similarly but build a product; for [it_lambda_name env c
sign] and [it_prod_name env c sign], more recent types should come
first in [sign]; none of these functions substitute named
variables in [c] by de Bruijn indices *)
val lambda_name : env -> name * types * constr -> constr
val prod_name : env -> name * types * constr -> constr
val mkLambda_or_LetIn_name : env -> constr -> rel_declaration -> constr
val mkProd_or_LetIn_name : env -> constr -> rel_declaration -> constr
val it_mkLambda_or_LetIn_name : env -> constr -> rel_context -> constr
val it_mkProd_or_LetIn_name : env -> constr -> rel_context -> constr
val it_mkProd_wo_LetIn : constr -> rel_context -> constr
val it_mkLambda_or_LetIn : constr -> rel_context -> constr
val it_mkProd_or_LetIn : constr -> rel_context -> constr
val it_mkNamedLambda_or_LetIn : constr -> named_context -> constr
val it_mkNamedProd_or_LetIn : constr -> named_context -> constr
val it_mkNamedProd_wo_LetIn : constr -> named_context -> constr
(* [lambda_create env (t,c)] builds [[x:t]c] where [x] is a name built
from [t]; [prod_create env (t,c)] builds [(x:t)c] where [x] is a
name built from [t] *)
val lambda_create : env -> types * constr -> constr
val prod_create : env -> types * constr -> constr
val defined_constant : env -> constant -> bool
val evaluable_constant : env -> constant -> bool
val evaluable_named_decl : env -> identifier -> bool
val evaluable_rel_decl : env -> int -> bool
(*s Ocurrence of section variables. *)
(* [(occur_var id c)] returns [true] if variable [id] occurs free
in c, [false] otherwise *)
val occur_var : env -> identifier -> constr -> bool
val occur_var_in_decl : env -> identifier -> named_declaration -> bool
(* [global_vars c] returns the list of [id]'s occurring as [VAR id] in [c] *)
val global_vars : env -> constr -> identifier list
(* [global_vars_decl d] returns the list of [id]'s occurring as [VAR
id] in declaration [d] (type and body if any) *)
val global_vars_decl : env -> named_declaration -> identifier list
val global_vars_set : env -> constr -> Idset.t
val keep_hyps : env -> Idset.t -> named_context -> named_context
val rename_bound_var : env -> identifier list -> constr -> constr
(*s Modules. *)
type compiled_env
val export : env -> dir_path -> compiled_env
val import : compiled_env -> env -> env
(*s Unsafe judgments. We introduce here the pre-type of judgments, which is
actually only a datatype to store a term with its type and the type of its
type. *)
type unsafe_judgment = {
uj_val : constr;
uj_type : types }
type unsafe_type_judgment = {
utj_val : constr;
utj_type : sorts }
(*s Displays the memory use of an environment. *)
val mem : env -> Pp.std_ppcmds
|
