blob: 65307debea7a5288cbc1a93f66c6121ec6af1ecf (
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
|
(***********************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
(* \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 Tacmach
open Proof_type
open Evar_refiner
(*i*)
(* [new_meta] is a generator of unique meta variables *)
val new_meta : unit -> int
(* [exist_to_meta] generates new metavariables for each existential
and performs the replacement in the given constr *)
val exist_to_meta :
((existential * constr) list * constr) ->
((int * constr) list * constr)
(* The Type of Constructions clausale environments. *)
type 'a freelisted = {
rebus : 'a;
freemetas : Intset.t }
type clbinding =
| Cltyp of constr freelisted
| Clval of constr freelisted * constr freelisted
type 'a clausenv = {
templval : constr freelisted;
templtyp : constr freelisted;
namenv : identifier Intmap.t;
env : clbinding Intmap.t;
hook : 'a }
(* [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 instanciating metavars by name.
* [env] is the mapping from metavar numbers to their types
* and values.
* [hook] is the pointer to the current walking context, for
* integrating existential vars and metavars. *)
type wc = walking_constraints (* for a better reading of the following *)
val unify : constr -> tactic
val unify_0 :
Reductionops.conv_pb -> (int * constr) list -> wc -> constr -> constr
-> (int * constr) list * (constr * constr) list
val collect_metas : constr -> int list
val mk_clenv : 'a -> constr -> 'a clausenv
val mk_clenv_from : 'a -> constr * constr -> 'a clausenv
val mk_clenv_from_n : 'a -> int -> constr * constr -> 'a clausenv
val mk_clenv_rename_from : wc -> constr * constr -> wc clausenv
val mk_clenv_rename_from_n : wc -> int -> constr * constr -> wc clausenv
val mk_clenv_hnf_constr_type_of : wc -> constr -> wc clausenv
val mk_clenv_printable_type_of : wc -> constr -> wc clausenv
val mk_clenv_type_of : wc -> constr -> wc clausenv
val connect_clenv : wc -> 'a clausenv -> wc clausenv
val clenv_change_head : constr * constr -> 'a clausenv -> 'a clausenv
val clenv_assign : int -> constr -> 'a clausenv -> 'a clausenv
val clenv_instance_term : wc clausenv -> constr -> constr
val clenv_pose : name * int * constr -> 'a clausenv -> 'a clausenv
val clenv_template : 'a clausenv -> constr freelisted
val clenv_template_type : 'a clausenv -> constr freelisted
val clenv_instance_type : wc clausenv -> int -> constr
val clenv_instance_template : wc clausenv -> constr
val clenv_instance_template_type : wc clausenv -> constr
val clenv_unify :
Reductionops.conv_pb -> constr -> constr -> wc clausenv -> wc clausenv
val clenv_fchain : int -> 'a clausenv -> wc clausenv -> wc clausenv
val clenv_refine : (wc -> tactic) -> wc clausenv -> tactic
val res_pf : (wc -> tactic) -> wc clausenv -> tactic
val res_pf_cast : (wc -> tactic) -> wc clausenv -> tactic
val elim_res_pf : (wc -> tactic) -> wc clausenv -> tactic
val clenv_independent :
wc clausenv -> constr freelisted * constr freelisted -> int list
val clenv_missing :
'a clausenv -> constr freelisted * constr freelisted -> int list
val clenv_constrain_missing_args : constr list -> wc clausenv -> wc clausenv
val clenv_constrain_dep_args : constr list -> wc clausenv -> wc clausenv
val clenv_lookup_name : 'a clausenv -> identifier -> int
val clenv_match_args : (bindOcc * constr) list -> wc clausenv -> wc clausenv
val e_res_pf : (wc -> tactic) -> wc clausenv -> tactic
val clenv_type_of : wc clausenv -> constr -> constr
val clenv_unique_resolver : bool -> wc clausenv -> goal sigma -> wc clausenv
val make_clenv_binding_apply :
walking_constraints ->
int ->
constr * constr ->
(bindOcc * types) list ->
walking_constraints clausenv
val make_clenv_binding :
walking_constraints ->
constr * constr ->
(bindOcc * types) list ->
walking_constraints clausenv
(* Exported for program.ml only *)
val clenv_add_sign :
(identifier * types) -> wc clausenv -> wc clausenv
val constrain_clenv_to_subterm :
wc clausenv -> constr * constr -> wc clausenv * constr
val clenv_constrain_dep_args_of :
int -> constr list -> wc clausenv -> wc clausenv
val constrain_clenv_using_subterm_list :
bool -> wc clausenv -> constr list -> constr -> wc clausenv * constr list
val clenv_typed_unify :
Reductionops.conv_pb -> constr -> constr -> wc clausenv -> wc clausenv
val pr_clenv : 'a clausenv -> Pp.std_ppcmds
(*i This should be in another module i*)
(* [abstract_list_all env sigma t c l] *)
(* abstracts the terms in l over c to get a term of type t *)
val abstract_list_all :
Environ.env -> 'a Evd.evar_map -> constr -> constr -> constr list -> constr
|
