blob: 5868f1e9bf74246bc5995caa26b11a9c044f79fa (
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
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
open Names
open Term
open Environ
open Evd
open Mod_subst
open Unification
open Misctypes
(** {6 The Type of Constructions clausale environments.} *)
type clausenv = {
env : env; (** the typing context *)
evd : evar_map; (** the mapping from metavar and evar numbers to their
types and values *)
templval : constr freelisted; (** the template which we are trying to fill
out *)
templtyp : constr freelisted (** its type *)}
val map_clenv : (constr -> constr) -> clausenv -> clausenv
(** subject of clenv (instantiated) *)
val clenv_value : clausenv -> constr
(** type of clenv (instantiated) *)
val clenv_type : clausenv -> types
(** substitute resolved metas *)
val clenv_nf_meta : clausenv -> constr -> constr
(** type of a meta in clenv context *)
val clenv_meta_type : clausenv -> metavariable -> types
val mk_clenv_from : Goal.goal sigma -> constr * types -> clausenv
val mk_clenv_from_n :
Goal.goal sigma -> int option -> constr * types -> clausenv
val mk_clenv_type_of : Goal.goal sigma -> constr -> clausenv
val mk_clenv_from_env : env -> evar_map -> int option -> constr * types -> clausenv
(** Refresh the universes in a clenv *)
val refresh_undefined_univs : clausenv -> clausenv * Univ.universe_level_subst
(** {6 linking of clenvs } *)
val connect_clenv : Goal.goal sigma -> clausenv -> clausenv
val clenv_fchain :
?flags:unify_flags -> metavariable -> clausenv -> clausenv -> clausenv
(** {6 Unification with clenvs } *)
(** Unifies two terms in a clenv. The boolean is [allow_K] (see [Unification]) *)
val clenv_unify :
?flags:unify_flags -> conv_pb -> constr -> constr -> clausenv -> clausenv
(** unifies the concl of the goal with the type of the clenv *)
val clenv_unique_resolver :
?flags:unify_flags -> clausenv -> Goal.goal sigma -> clausenv
val clenv_dependent : clausenv -> metavariable list
val clenv_pose_metas_as_evars : clausenv -> metavariable list -> clausenv
(** {6 Bindings } *)
type arg_bindings = constr explicit_bindings
(** bindings where the key is the position in the template of the
clenv (dependent or not). Positions can be negative meaning to
start from the rightmost argument of the template. *)
val clenv_independent : clausenv -> metavariable list
val clenv_missing : clausenv -> metavariable list
(** for the purpose of inversion tactics *)
exception NoSuchBinding
val clenv_constrain_last_binding : constr -> clausenv -> clausenv
val clenv_unify_meta_types : ?flags:unify_flags -> clausenv -> clausenv
(** start with a clenv to refine with a given term with bindings *)
(** the arity of the lemma is fixed
the optional int tells how many prods of the lemma have to be used
use all of them if None *)
val make_clenv_binding_env_apply :
env -> evar_map -> int option -> constr * constr -> constr bindings ->
clausenv
val make_clenv_binding_apply :
env -> evar_map -> int option -> constr * constr -> constr bindings ->
clausenv
val make_clenv_binding_env :
env -> evar_map -> constr * constr -> constr bindings -> clausenv
val make_clenv_binding :
env -> evar_map -> constr * constr -> constr bindings -> clausenv
(** if the clause is a product, add an extra meta for this product *)
exception NotExtensibleClause
val clenv_push_prod : clausenv -> clausenv
(** {6 Pretty-print (debug only) } *)
val pr_clenv : clausenv -> Pp.std_ppcmds
(** {6 Evar version} *)
type hole = {
hole_evar : constr;
hole_type : types;
hole_deps : bool;
(** Dependent in hypotheses then in conclusion *)
hole_name : Name.t;
}
type clause = {
cl_holes : hole list;
cl_concl : types;
}
val make_evar_clause : env -> evar_map -> int option -> types ->
(evar_map * clause)
(** An evar version of {!make_clenv_binding}. Given a type [t],
[evar_environments env sigma n t bl] tries to eliminate at most [n] products
of the type [t] by filling it with evars. It returns the resulting type
together with the list of holes generated. Assumes that [t] is well-typed
in the environment. *)
val solve_evar_clause : env -> evar_map -> bool -> clause -> constr bindings ->
evar_map
(** [solve_evar_clause env sigma hyps cl bl] tries to solve the holes contained
in [cl] according to the [bl] argument. Assumes that [bl] are well-typed in
the environment. The boolean [hyps] is a compatibility flag that allows to
consider arguments to be dependent only when they appear in hypotheses and
not in the conclusion. *)
|
