blob: f9a969a253b35e319653342747036e2c10596d21 (
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
|
(************************************************************************)
(* * 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 Constr
open EConstr
open Environ
open Evd
type allowed_evars =
| AllowAll
| AllowFun of (Evar.t -> bool)
type core_unify_flags = {
modulo_conv_on_closed_terms : TransparentState.t option;
use_metas_eagerly_in_conv_on_closed_terms : bool;
use_evars_eagerly_in_conv_on_closed_terms : bool;
modulo_delta : TransparentState.t;
modulo_delta_types : TransparentState.t;
check_applied_meta_types : bool;
use_pattern_unification : bool;
use_meta_bound_pattern_unification : bool;
allowed_evars : allowed_evars;
restrict_conv_on_strict_subterms : bool;
modulo_betaiota : bool;
modulo_eta : bool;
}
type unify_flags = {
core_unify_flags : core_unify_flags;
merge_unify_flags : core_unify_flags;
subterm_unify_flags : core_unify_flags;
allow_K_in_toplevel_higher_order_unification : bool;
resolve_evars : bool
}
val default_core_unify_flags : unit -> core_unify_flags
val default_no_delta_core_unify_flags : unit -> core_unify_flags
val default_unify_flags : unit -> unify_flags
val default_no_delta_unify_flags : TransparentState.t -> unify_flags
val elim_flags : unit -> unify_flags
val elim_no_delta_flags : unit -> unify_flags
val is_keyed_unification : unit -> bool
(** The "unique" unification function *)
val w_unify :
env -> evar_map -> conv_pb -> ?flags:unify_flags -> constr -> constr -> evar_map
(** [w_unify_to_subterm env m (c,t)] performs unification of [c] with a
subterm of [t]. Constraints are added to [m] and the matched
subterm of [t] is also returned. *)
val w_unify_to_subterm :
env -> evar_map -> ?flags:unify_flags -> constr * constr -> evar_map * constr
val w_unify_to_subterm_all :
env -> evar_map -> ?flags:unify_flags -> constr * constr -> (evar_map * constr) list
val w_unify_meta_types : env -> ?flags:unify_flags -> evar_map -> evar_map
(** [w_coerce_to_type env evd c ctyp typ] tries to coerce [c] of type
[ctyp] so that its gets type [typ]; [typ] may contain metavariables *)
val w_coerce_to_type : env -> evar_map -> constr -> types -> types ->
evar_map * constr
(* Looking for subterms in contexts at some occurrences, possibly with pattern*)
exception PatternNotFound
type prefix_of_inductive_support_flag = bool
type abstraction_request =
| AbstractPattern of prefix_of_inductive_support_flag * (types -> bool) * Names.Name.t * (evar_map * constr) * Locus.clause * bool
| AbstractExact of Names.Name.t * constr * types option * Locus.clause * bool
val finish_evar_resolution : ?flags:Pretyping.inference_flags ->
env -> evar_map -> (evar_map * constr) -> evar_map * constr
type 'r abstraction_result =
Names.Id.t * named_context_val *
named_declaration list * Names.Id.t option *
types * (evar_map * constr) option
val make_abstraction : env -> evar_map -> constr ->
abstraction_request -> 'r abstraction_result
val pose_all_metas_as_evars : env -> evar_map -> constr -> evar_map * constr
(*i This should be in another module i*)
(** [abstract_list_all env evd t c l]
abstracts the terms in l over c to get a term of type t
(exported for inv.ml) *)
val abstract_list_all :
env -> evar_map -> constr -> constr -> constr list -> evar_map * (constr * types)
(* For tracing *)
type metabinding = (metavariable * constr * (instance_constraint * instance_typing_status))
type subst0 =
(evar_map *
metabinding list *
(Environ.env * existential * t) list)
val w_merge : env -> bool -> core_unify_flags -> subst0 -> evar_map
val unify_0 : Environ.env ->
Evd.evar_map ->
Evd.conv_pb ->
core_unify_flags ->
types ->
types ->
subst0
val unify_0_with_initial_metas :
subst0 ->
bool ->
Environ.env ->
Evd.conv_pb ->
core_unify_flags ->
types ->
types ->
subst0
|
