forked from coq/coq
-
Notifications
You must be signed in to change notification settings - Fork 0
/
evarconv.mli
147 lines (104 loc) · 5.56 KB
/
evarconv.mli
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
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * Copyright INRIA, CNRS and contributors *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
open EConstr
open Environ
open Reductionops
open Evd
open Locus
(** {4 Unification for type inference. } *)
type unify_flags = Evarsolve.unify_flags
(** The default subterm transparent state is no unfoldings *)
val default_flags_of : ?subterm_ts:TransparentState.t -> TransparentState.t -> unify_flags
type unify_fun = unify_flags ->
env -> evar_map -> conv_pb -> constr -> constr -> Evarsolve.unification_result
val conv_fun : unify_fun -> Evarsolve.unifier
exception UnableToUnify of evar_map * Pretype_errors.unification_error
(** {6 Main unification algorithm for type inference. } *)
(** There are two variants for unification: one that delays constraints outside its capabilities
([unify_delay]) and another that tries to solve such remaining constraints using
heuristics ([unify]). *)
(** These functions allow to pass arbitrary flags to the unifier and can delay constraints.
In case the flags are not specified, they default to
[default_flags_of TransparentState.full] currently.
In case of success, the two terms are hence unifiable only if the remaining constraints
can be solved or [check_problems_are_solved] is true.
@raises UnableToUnify in case the two terms do not unify *)
val unify_delay : ?flags:unify_flags -> env -> evar_map -> constr -> constr -> evar_map
val unify_leq_delay : ?flags:unify_flags -> env -> evar_map -> constr -> constr -> evar_map
(** This function also calls [solve_unif_constraints_with_heuristics] to resolve any remaining
constraints. In case of success the two terms are unified without condition.
The with_ho option tells if higher-order unification should be tried to resolve the
constraints.
@raises a PretypeError if it cannot unify *)
val unify : ?flags:unify_flags -> ?with_ho:bool ->
env -> evar_map -> conv_pb -> constr -> constr -> evar_map
(** {6 Unification heuristics. } *)
(** Try heuristics to solve pending unification problems and to solve
evars with candidates.
The with_ho option tells if higher-order unification should be tried
to resolve the constraints.
@raises a PretypeError if it fails to resolve some problem *)
val solve_unif_constraints_with_heuristics :
env -> ?flags:unify_flags -> ?with_ho:bool -> evar_map -> evar_map
(** Check all pending unification problems are solved and raise a
PretypeError otherwise *)
val check_problems_are_solved : env -> evar_map -> unit
(** Check if a canonical structure is applicable *)
val check_conv_record : env -> evar_map ->
state -> state ->
evar_map * (constr * constr)
* constr * constr list * (EConstr.t list * EConstr.t list) *
(EConstr.t list * EConstr.t list) *
(Stack.t * Stack.t) * constr *
(int option * constr)
(** Compares two constants/inductives/constructors unifying their universes.
It required the number of arguments applied to the c/i/c in order to decided
the kind of check it must perform. *)
val compare_heads : env -> evar_map ->
nargs:int -> EConstr.t -> EConstr.t -> Evarsolve.unification_result
(** Try to solve problems of the form ?x[args] = c by second-order
matching, using typing to select occurrences *)
type occurrence_match_test =
env -> evar_map -> constr -> constr -> bool * evar_map
(** When given the choice of abstracting an occurrence or leaving it,
force abstration. *)
type occurrence_selection =
| AtOccurrences of occurrences
| Unspecified of Abstraction.abstraction
(** By default, unspecified, not preferring abstraction.
This provides the most general solutions. *)
val default_occurrence_selection : occurrence_selection
type occurrences_selection =
occurrence_match_test * occurrence_selection list
val default_occurrence_test : allowed_evars:Evarsolve.AllowedEvars.t -> TransparentState.t -> occurrence_match_test
(** [default_occurrence_selection n]
Gives the default test and occurrences for [n] arguments *)
val default_occurrences_selection : ?allowed_evars:Evarsolve.AllowedEvars.t (* By default, all *) ->
TransparentState.t -> int -> occurrences_selection
val second_order_matching : unify_flags -> env -> evar_map ->
EConstr.existential -> occurrences_selection -> constr -> evar_map * bool
(** Declare function to enforce evars resolution by using typing constraints *)
val set_solve_evars : (env -> evar_map -> constr -> evar_map * constr) -> unit
(** Override default [evar_conv_x] algorithm. *)
val set_evar_conv : unify_fun -> unit
(** The default unification algorithm with evars and universes. *)
val evar_conv_x : unify_fun
val evar_unify : Evarsolve.unifier
(**/**)
(* For debugging *)
val evar_eqappr_x : ?rhs_is_already_stuck:bool -> unify_flags ->
env -> evar_map ->
conv_pb -> state -> state ->
Evarsolve.unification_result
val occur_rigidly : Evarsolve.unify_flags ->
'a -> Evd.evar_map -> Evar.t * 'b -> EConstr.t -> bool
(**/**)
(** {6 Functions to deal with impossible cases } *)
val coq_unit_judge : env -> evar_map -> evar_map * EConstr.unsafe_judgment