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
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
|
(***********************************************************************)
(* 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 *)
(***********************************************************************)
(* $Id$ *)
open Pp
open Util
open Names
open Term
open Sign
open Reduction
open Environ
open Logic
open Tacmach
open Evd
open Proof_trees
open Clenv
(* If you have a precise idea of the intended use of the following code, please
write to Eduardo.Gimenez@inria.fr and ask for the prize :-)
-- Eduardo (11/8/97) *)
type wc = walking_constraints
let pf_get_new_id id gls =
next_ident_away id (pf_ids_of_hyps gls)
let pf_get_new_ids ids gls =
let avoid = pf_ids_of_hyps gls in
List.fold_right
(fun id acc -> (next_ident_away id (acc@avoid))::acc)
ids []
type arg_binder =
| Dep of identifier
| Nodep of int
| Abs of int
type arg_bindings = (arg_binder * constr) list
let clenv_constrain_with_bindings bl clause =
if bl = [] then
clause
else
let all_mvs = collect_metas (clenv_template clause).rebus
and ind_mvs = clenv_independent clause
(clenv_template clause,
clenv_template_type clause) in
let nb_indep = List.length ind_mvs in
let rec matchrec clause = function
| [] -> clause
| (b,c)::t ->
let k =
match b with
| Dep s ->
if List.mem_assoc b t then
errorlabstrm "clenv_match_args"
[< 'sTR "The variable "; pr_id s;
'sTR " occurs more than once in binding" >];
clenv_lookup_name clause s
| Nodep n ->
let index = if n > 0 then n-1 else nb_indep+n in
if List.mem_assoc (Nodep (index+1)) t or
List.mem_assoc (Nodep (index-nb_indep)) t
then errorlabstrm "clenv_match_args"
[< 'sTR "The position "; 'iNT n ;
'sTR " occurs more than once in binding" >];
(try
List.nth ind_mvs index
with Failure _ ->
errorlabstrm "clenv_constrain_with_bindings"
[< 'sTR"Clause did not have " ; 'iNT n ; 'sTR"-th" ;
'sTR" unnamed argument" >])
| Abs n ->
(try
if n > 0 then
List.nth all_mvs (n-1)
else if n < 0 then
List.nth (List.rev all_mvs) (-n-1)
else error "clenv_constrain_with_bindings"
with Failure _ ->
errorlabstrm "clenv_constrain_with_bindings"
[< 'sTR"Clause did not have " ; 'iNT n ; 'sTR"-th" ;
'sTR" absolute argument" >])
in
let env = Global.env () in
let sigma = Evd.empty in
let k_typ = nf_betaiota env sigma (clenv_instance_type clause k) in
let c_typ = nf_betaiota env sigma (w_type_of clause.hook c) in
matchrec (clenv_assign k c (clenv_unify k_typ c_typ clause)) t
in
matchrec clause bl
let add_prod_rel sigma (t,env) =
match kind_of_term t with
| IsProd (na,t1,b) ->
(b,push_rel_assum (na, t1) env)
| IsLetIn (na,c1,t1,b) ->
(b,push_rel_def (na,c1, t1) env)
| _ -> failwith "add_prod_rel"
let rec add_prods_rel sigma (t,env) =
try
add_prods_rel sigma (add_prod_rel sigma (whd_betadeltaiota env sigma t,env))
with Failure "add_prod_rel" ->
(t,env)
(* What follows is part of the contents of the former file tactics3.ml *)
let res_pf_THEN kONT clenv tac gls =
let clenv' = (clenv_unique_resolver false clenv gls) in
(tclTHEN (clenv_refine kONT clenv') (tac clenv')) gls
let res_pf_THEN_i kONT clenv tac gls =
let clenv' = (clenv_unique_resolver false clenv gls) in
tclTHEN_i (clenv_refine kONT clenv') (tac clenv') gls
let elim_res_pf_THEN_i kONT clenv tac gls =
let clenv' = (clenv_unique_resolver true clenv gls) in
tclTHEN_i (clenv_refine kONT clenv') (tac clenv') gls
let rec build_args acc ce p_0 p_1 =
match kind_of_term p_0, p_1 with
| (IsProd (na,a,b), (a_0::bargs)) ->
let (newa,ce') = (build_term ce (na,Some a) a_0) in
build_args (newa::acc) ce' (subst1 a_0 b) bargs
| (IsLetIn (na,a,t,b), args) -> build_args acc ce (subst1 a b) args
| (_, []) -> (List.rev acc,ce)
| (_, (_::_)) -> failwith "mk_clenv_using"
and build_term ce p_0 c =
let env = w_env ce.hook in
match p_0, kind_of_term c with
| ((na,Some t), IsMeta mv) ->
(* let mv = new_meta() in *)
(mkMeta mv, clenv_pose (na,mv,t) ce)
| ((na,_), IsCast (c,t)) -> build_term ce (na,Some t) c
| ((na,Some t), _) ->
if (not((occur_meta c))) then
(c,ce)
else
let (hd,args) =
whd_betadeltaiota_stack env (w_Underlying ce.hook) c in
let hdty = w_type_of ce.hook hd in
let (args,ce') =
build_args [] ce (w_whd_betadeltaiota ce.hook hdty) args in
let newc = applist(hd,args) in
let t' = clenv_type_of ce' newc in
if w_conv_x ce'.hook t t' then
(newc,ce')
else
failwith "mk_clenv_using"
| ((na,None), _) ->
if (not((occur_meta c))) then
(c,ce)
else
let (hd,args) =
whd_betadeltaiota_stack env (w_Underlying ce.hook) c in
let hdty = w_type_of ce.hook hd in
let (args,ce') =
build_args [] ce (w_whd_betadeltaiota ce.hook hdty) args in
let newc = applist(hd,args) in
(newc,ce')
let mk_clenv_using wc c =
let ce = mk_clenv wc mkImplicit in
let (newc,ce') =
try
build_term ce (Anonymous,None) c
with Failure _ ->
raise (RefinerError (NotWellTyped c))
in
clenv_change_head (newc,clenv_type_of ce' newc) ce'
let applyUsing c gl =
let (wc,kONT) = startWalk gl in
let clause = mk_clenv_using wc c in
res_pf kONT clause gl
let clenv_apply_n_times n ce =
let templtyp = clenv_instance_template_type ce
and templval = (clenv_template ce).rebus in
let rec apprec ce argacc (n,ty) =
let env = Global.env () in
let templtyp = whd_betadeltaiota env (w_Underlying ce.hook) ty in
match (n, kind_of_term templtyp) with
| (0, _) ->
clenv_change_head (applist(templval,List.rev argacc), templtyp) ce
| (n, IsProd (na,dom,rng)) ->
let mv = new_meta() in
let newce = clenv_pose (na,mv,dom) ce in
apprec newce (mkMeta mv::argacc) (n-1, subst1 (mkMeta mv) rng)
| (n, IsLetIn (na,b,t,c)) ->
apprec ce argacc (n, subst1 b c)
| (n, _) -> failwith "clenv_apply_n_times"
in
apprec ce [] (n, templtyp)
|
