blob: e406b1487ad23eb89f194494da925acd2f3a19ba (
plain)
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
213
|
(************************************************************************)
(* 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 *)
(************************************************************************)
(*i $Id: termops.mli 9314 2006-10-29 20:11:08Z herbelin $ i*)
open Util
open Pp
open Names
open Term
open Sign
open Environ
(* Universes *)
val new_univ : unit -> Univ.universe
val new_sort_in_family : sorts_family -> sorts
val new_Type : unit -> types
val new_Type_sort : unit -> sorts
val refresh_universes : types -> types
(* printers *)
val print_sort : sorts -> std_ppcmds
val pr_sort_family : sorts_family -> std_ppcmds
(* debug printer: do not use to display terms to the casual user... *)
val set_print_constr : (env -> constr -> std_ppcmds) -> unit
val print_constr : constr -> std_ppcmds
val print_constr_env : env -> constr -> std_ppcmds
val print_named_context : env -> std_ppcmds
val print_rel_context : env -> std_ppcmds
val print_env : env -> std_ppcmds
(* iterators on terms *)
val prod_it : init:types -> (name * types) list -> types
val lam_it : init:constr -> (name * types) list -> constr
val rel_vect : int -> int -> constr array
val rel_list : int -> int -> constr list
val extended_rel_list : int -> rel_context -> constr list
val extended_rel_vect : int -> rel_context -> constr array
val push_rel_assum : name * types -> env -> env
val push_rels_assum : (name * types) list -> env -> env
val push_named_rec_types : name array * types array * 'a -> env -> env
val lookup_rel_id : identifier -> rel_context -> int * types
val mkProd_or_LetIn : rel_declaration -> types -> types
val mkProd_wo_LetIn : rel_declaration -> types -> types
val it_mkProd_wo_LetIn : init:types -> rel_context -> types
val it_mkProd_or_LetIn : init:types -> rel_context -> types
val it_mkLambda_or_LetIn : init:constr -> rel_context -> constr
val it_named_context_quantifier :
(named_declaration -> 'a -> 'a) -> init:'a -> named_context -> 'a
val it_mkNamedProd_or_LetIn : init:types -> named_context -> types
val it_mkNamedLambda_or_LetIn : init:constr -> named_context -> constr
val it_mkNamedProd_wo_LetIn : init:types -> named_context -> types
(**********************************************************************)
(* Generic iterators on constr *)
val map_constr_with_named_binders :
(name -> 'a -> 'a) ->
('a -> constr -> constr) -> 'a -> constr -> constr
val map_constr_with_binders_left_to_right :
(rel_declaration -> 'a -> 'a) ->
('a -> constr -> constr) ->
'a -> constr -> constr
val map_constr_with_full_binders :
(rel_declaration -> 'a -> 'a) ->
('a -> constr -> constr) -> 'a -> constr -> constr
(* [fold_constr_with_binders g f n acc c] folds [f n] on the immediate
subterms of [c] starting from [acc] and proceeding from left to
right according to the usual representation of the constructions as
[fold_constr] but it carries an extra data [n] (typically a lift
index) which is processed by [g] (which typically add 1 to [n]) at
each binder traversal; it is not recursive *)
val fold_constr_with_binders :
('a -> 'a) -> ('a -> 'b -> constr -> 'b) -> 'a -> 'b -> constr -> 'b
val iter_constr_with_full_binders :
(rel_declaration -> 'a -> 'a) -> ('a -> constr -> unit) -> 'a ->
constr -> unit
(**********************************************************************)
val strip_head_cast : constr -> constr
(* occur checks *)
exception Occur
val occur_meta : types -> bool
val occur_existential : types -> bool
val occur_const : constant -> types -> bool
val occur_evar : existential_key -> types -> bool
val occur_in_global : env -> identifier -> constr -> unit
val occur_var : env -> identifier -> types -> bool
val occur_var_in_decl :
env ->
identifier -> 'a * types option * types -> bool
val occur_term : constr -> constr -> bool
val free_rels : constr -> Intset.t
(* Substitution of metavariables *)
type metamap = (metavariable * constr) list
val subst_meta : metamap -> constr -> constr
(* [pop c] lifts by -1 the positive indexes in [c] *)
val pop : constr -> constr
(* bindings of an arbitrary large term. Uses equality modulo
reduction of let *)
val dependent : constr -> constr -> bool
val subst_term_gen :
(constr -> constr -> bool) -> constr -> constr -> constr
val replace_term_gen :
(constr -> constr -> bool) ->
constr -> constr -> constr -> constr
val subst_term : constr -> constr -> constr
val replace_term : constr -> constr -> constr -> constr
val subst_term_occ_gen :
int list -> int -> constr -> types -> int * types
val subst_term_occ : int list -> constr -> types -> types
val subst_term_occ_decl :
int list -> constr -> named_declaration -> named_declaration
val error_invalid_occurrence : int list -> 'a
(* Alternative term equalities *)
val eta_reduce_head : constr -> constr
val eta_eq_constr : constr -> constr -> bool
(* finding "intuitive" names to hypotheses *)
val first_char : identifier -> string
val lowercase_first_char : identifier -> string
val sort_hdchar : sorts -> string
val hdchar : env -> types -> string
val id_of_name_using_hdchar :
env -> types -> name -> identifier
val named_hd : env -> types -> name -> name
val named_hd_type : env -> types -> name -> name
val mkProd_name : env -> name * types * types -> types
val mkLambda_name : env -> name * types * constr -> constr
(* Deprecated synonyms of [mkProd_name] and [mkLambda_name] *)
val prod_name : env -> name * types * types -> types
val lambda_name : env -> name * types * constr -> constr
val prod_create : env -> types * types -> constr
val lambda_create : env -> types * constr -> constr
val name_assumption : env -> rel_declaration -> rel_declaration
val name_context : env -> rel_context -> rel_context
val mkProd_or_LetIn_name : env -> types -> rel_declaration -> types
val mkLambda_or_LetIn_name : env -> constr -> rel_declaration -> constr
val it_mkProd_or_LetIn_name : env -> types -> rel_context -> types
val it_mkLambda_or_LetIn_name : env -> constr -> rel_context -> constr
(* name contexts *)
type names_context = name list
val add_name : name -> names_context -> names_context
val lookup_name_of_rel : int -> names_context -> name
val lookup_rel_of_name : identifier -> names_context -> int
val empty_names_context : names_context
val ids_of_rel_context : rel_context -> identifier list
val ids_of_named_context : named_context -> identifier list
val ids_of_context : env -> identifier list
val names_of_rel_context : env -> names_context
(* Set of local names *)
val vars_of_env: env -> Idset.t
val add_vname : Idset.t -> name -> Idset.t
(* sets of free identifiers *)
type used_idents = identifier list
val occur_rel : int -> name list -> identifier -> bool
val occur_id : name list -> identifier -> constr -> bool
val next_global_ident_away :
(*allow section vars:*) bool -> identifier -> identifier list -> identifier
val next_name_not_occuring :
bool -> name -> identifier list -> name list -> constr -> identifier
val concrete_name :
bool -> identifier list -> name list -> name -> constr ->
name * identifier list
val concrete_let_name :
bool -> identifier list -> name list -> name -> constr -> name * identifier list
val rename_bound_var : env -> identifier list -> types -> types
(* other signature iterators *)
val process_rel_context : (rel_declaration -> env -> env) -> env -> env
val assums_of_rel_context : rel_context -> (name * constr) list
val lift_rel_context : int -> rel_context -> rel_context
val fold_named_context_both_sides :
('a -> named_declaration -> named_declaration list -> 'a) ->
named_context -> init:'a -> 'a
val mem_named_context : identifier -> named_context -> bool
val make_all_name_different : env -> env
val global_vars : env -> constr -> identifier list
val global_vars_set_of_decl : env -> named_declaration -> Idset.t
(* Test if an identifier is the basename of a global reference *)
val is_section_variable : identifier -> bool
val isGlobalRef : constr -> bool
(* Combinators on judgments *)
val on_judgment : (types -> types) -> unsafe_judgment -> unsafe_judgment
val on_judgment_value : (types -> types) -> unsafe_judgment -> unsafe_judgment
val on_judgment_type : (types -> types) -> unsafe_judgment -> unsafe_judgment
|
