blob: 7429cd162769ee647df8e40af052159cf8a87a47 (
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
|
(************************************************************************)
(* 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: evarutil.mli 8695 2006-04-10 16:33:52Z msozeau $ i*)
(*i*)
open Util
open Names
open Rawterm
open Term
open Sign
open Evd
open Environ
open Reductionops
(*i*)
(*s This modules provides useful functions for unification modulo evars *)
(***********************************************************)
(* Metas *)
(* [new_meta] is a generator of unique meta variables *)
val new_meta : unit -> metavariable
val mk_new_meta : unit -> constr
(* [new_untyped_evar] is a generator of unique evar keys *)
val new_untyped_evar : unit -> existential_key
(***********************************************************)
(* Creating a fresh evar given their type and context *)
val new_evar :
evar_defs -> env -> ?src:loc * hole_kind -> types -> evar_defs * constr
(* the same with side-effects *)
val e_new_evar :
evar_defs ref -> env -> ?src:loc * hole_kind -> types -> constr
(* Create a fresh evar in a context different from its definition context:
[new_evar_instance sign evd ty inst] creates a new evar of context
[sign] and type [ty], [inst] is a mapping of the evar context to
the context where the evar should occur. This means that the terms
of [inst] are typed in the occurrence context and their type (seen
as a telescope) is [sign] *)
val new_evar_instance :
named_context_val -> evar_defs -> types -> ?src:loc * hole_kind ->
constr list -> evar_defs * constr
(***********************************************************)
(* Instanciate evars *)
(* suspicious env ? *)
val evar_define :
env -> existential -> constr -> evar_defs -> evar_defs * evar list
(***********************************************************)
(* Evars/Metas switching... *)
(* [evars_to_metas] generates new metavariables for each non dependent
existential and performs the replacement in the given constr; it also
returns the evar_map extended with dependent evars *)
val evars_to_metas : evar_map -> open_constr -> (evar_map * constr)
val non_instantiated : evar_map -> (evar * evar_info) list
(***********************************************************)
(* Unification utils *)
val is_ground_term : evar_defs -> constr -> bool
val is_eliminator : constr -> bool
val head_is_embedded_evar : evar_defs -> constr -> bool
val solve_simple_eqn :
(env -> evar_defs -> conv_pb -> constr -> constr -> evar_defs * bool)
-> env -> evar_defs -> conv_pb * existential * constr ->
evar_defs * bool
val define_evar_as_arrow : evar_defs -> existential -> evar_defs * types
val define_evar_as_lambda : evar_defs -> existential -> evar_defs * types
val define_evar_as_sort : evar_defs -> existential -> evar_defs * sorts
(***********************************************************)
(* Value/Type constraints *)
val judge_of_new_Type : unit -> unsafe_judgment
type type_constraint_type = (int * int) option * constr
type type_constraint = type_constraint_type option
type val_constraint = constr option
val empty_tycon : type_constraint
val mk_tycon_type : constr -> type_constraint_type
val mk_abstr_tycon_type : int -> constr -> type_constraint_type
val mk_tycon : constr -> type_constraint
val mk_abstr_tycon : int -> constr -> type_constraint
val empty_valcon : val_constraint
val mk_valcon : constr -> val_constraint
val split_tycon :
loc -> env -> evar_defs -> type_constraint ->
evar_defs * (name * type_constraint * type_constraint)
val valcon_of_tycon : type_constraint -> val_constraint
val lift_abstr_tycon_type : int -> type_constraint_type -> type_constraint_type
val lift_tycon_type : int -> type_constraint_type -> type_constraint_type
val lift_tycon : int -> type_constraint -> type_constraint
(***********************************************************)
(* [whd_ise] raise [Uninstantiated_evar] if an evar remains uninstantiated; *)
(* *[whd_evar]* and *[nf_evar]* leave uninstantiated evar as is *)
val nf_evar : evar_map -> constr -> constr
val j_nf_evar : evar_map -> unsafe_judgment -> unsafe_judgment
val jl_nf_evar :
evar_map -> unsafe_judgment list -> unsafe_judgment list
val jv_nf_evar :
evar_map -> unsafe_judgment array -> unsafe_judgment array
val tj_nf_evar :
evar_map -> unsafe_type_judgment -> unsafe_type_judgment
val nf_evar_info : evar_map -> evar_info -> evar_info
val nf_evars : evar_map -> evar_map
(* Same for evar defs *)
val nf_isevar : evar_defs -> constr -> constr
val j_nf_isevar : evar_defs -> unsafe_judgment -> unsafe_judgment
val jl_nf_isevar :
evar_defs -> unsafe_judgment list -> unsafe_judgment list
val jv_nf_isevar :
evar_defs -> unsafe_judgment array -> unsafe_judgment array
val tj_nf_isevar :
evar_defs -> unsafe_type_judgment -> unsafe_type_judgment
val nf_evar_defs : evar_defs -> evar_defs
(* Replacing all evars *)
exception Uninstantiated_evar of existential_key
val whd_ise : evar_map -> constr -> constr
val whd_castappevar : evar_map -> constr -> constr
(*********************************************************************)
(* debug pretty-printer: *)
val pr_tycon_type : env -> type_constraint_type -> Pp.std_ppcmds
val pr_tycon : env -> type_constraint -> Pp.std_ppcmds
|
