blob: b1f08a69164b0dd4757944010373c0b20b7cfd1f (
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
|
(************************************************************************)
(* 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$ i*)
(*i*)
open Util
open Names
open Term
open Sign
open Environ
open Evd
open Evarutil
open Mod_subst
(*i*)
(***************************************************************)
(* The Type of Constructions clausale environments. *)
(* [templenv] is the typing context
* [env] is the mapping from metavar and evar numbers to their types
* and values.
* [templval] is the template which we are trying to fill out.
* [templtyp] is its type.
* [namenv] is a mapping from metavar numbers to names, for
* use in instantiating metavars by name.
*)
type clausenv = {
templenv : env;
env : evar_defs;
templval : constr freelisted;
templtyp : constr freelisted }
(* Substitution is not applied on templenv (because [subst_clenv] is
applied only on hints which typing env is overwritten by the
goal env) *)
val subst_clenv : substitution -> 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 : evar_info sigma -> constr * types -> clausenv
val mk_clenv_from_n :
evar_info sigma -> int option -> constr * types -> clausenv
val mk_clenv_rename_from : evar_info sigma -> constr * types -> clausenv
val mk_clenv_rename_from_n :
evar_info sigma -> int option -> constr * types -> clausenv
val mk_clenv_type_of : evar_info sigma -> constr -> clausenv
(***************************************************************)
(* linking of clenvs *)
val connect_clenv : evar_info sigma -> clausenv -> clausenv
val clenv_fchain : metavariable -> clausenv -> clausenv -> clausenv
(***************************************************************)
(* Unification with clenvs *)
(* Unifies two terms in a clenv. The boolean is [allow_K] (see [Unification]) *)
val clenv_unify :
bool -> conv_pb -> constr -> constr -> clausenv -> clausenv
(* unifies the concl of the goal with the type of the clenv *)
val clenv_unique_resolver :
bool -> clausenv -> evar_info sigma -> clausenv
(* same as above ([allow_K=false]) but replaces remaining metas
with fresh evars *)
val evar_clenv_unique_resolver :
clausenv -> evar_info sigma -> clausenv
(***************************************************************)
(* 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. *)
type arg_bindings = (int * constr) list
val clenv_independent : clausenv -> metavariable list
val clenv_missing : clausenv -> metavariable list
(* defines metas corresponding to the name of the bindings *)
val clenv_match_args :
constr Rawterm.explicit_bindings -> clausenv -> clausenv
val clenv_constrain_with_bindings : arg_bindings -> clausenv -> clausenv
(* start with a clenv to refine with a given term with bindings *)
(* 1- the arity of the lemma is fixed *)
val make_clenv_binding_apply :
evar_info sigma -> int -> constr * constr -> constr Rawterm.bindings ->
clausenv
val make_clenv_binding :
evar_info sigma -> constr * constr -> constr Rawterm.bindings -> clausenv
(* other stuff *)
val clenv_environments :
evar_defs -> int option -> types -> evar_defs * constr list * types
val clenv_environments_evars :
env -> evar_defs -> int option -> types -> evar_defs * constr list * types
(***************************************************************)
(* Pretty-print *)
val pr_clenv : clausenv -> Pp.std_ppcmds
|
