1
(************************************************************************)
2
(* v * The Coq Proof Assistant / The Coq Development Team *)
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
4
(* \VV/ **************************************************************)
5
(* // * This file is distributed under the terms of the *)
6
(* * GNU Lesser General Public License Version 2.1 *)
7
(************************************************************************)
9
(* $Id: refine.ml 12187 2009-06-13 19:36:59Z msozeau $ *)
11
(* JCF -- 6 janvier 1998 EXPERIMENTAL *)
14
* L'id�e est, en quelque sorte, d'avoir de "vraies" m�tavariables
15
* dans Coq, c'est-�-dire de donner des preuves incompl�tes -- mais
16
* o� les trous sont typ�s -- et que les sous-buts correspondants
17
* soient engendr�s pour finir la preuve.
21
* (x:nat) { y:nat | (minus y x) = x }
22
* et je donne la preuve incompl�te
23
* [x:nat](exist nat [y:nat]((minus y x)=x) (plus x x) ?)
24
* ce qui engendre le but
25
* (minus (plus x x) x)=x
28
(* Pour cela, on proc�de de la mani�re suivante :
30
* 1. Un terme de preuve incomplet est un terme contenant des variables
31
* existentielles Evar i.e. "?" en syntaxe concr�te.
32
* La r�solution de ces variables n'est plus n�cessairement totale
33
* (ise_resolve called with fail_evar=false) et les variables
34
* existentielles restantes sont remplac�es par des m�ta-variables
35
* cast�es par leur types (celui est connu : soit donn�, soit trouv�
36
* pendant la phase de r�solution).
38
* 2. On met ensuite le terme "� plat" i.e. on n'autorise des MV qu'au
39
* permier niveau et pour chacune d'elles, si n�cessaire, on donne
40
* � son tour un terme de preuve incomplet pour la r�soudre.
41
* Exemple: le terme (f a ? [x:nat](e ?)) donne
42
* (f a ?1 ?2) avec ?2 => [x:nat]?3 et ?3 => (e ?4)
43
* ?1 et ?4 donneront des buts
45
* 3. On �crit ensuite une tactique tcc qui engendre les sous-buts
46
* � partir d'une preuve incompl�te.
63
type term_with_holes = TH of constr * metamap * sg_proofs
64
and sg_proofs = (term_with_holes option) list
68
let rec pp_th (TH(c,mm,sg)) =
69
(str"TH=[ " ++ hov 0 (pr_lconstr c ++ fnl () ++
70
(* pp_mm mm ++ fnl () ++ *)
73
hov 0 (prlist_with_sep (fun _ -> (fnl ()))
74
(fun (n,c) -> (int n ++ str" --> " ++ pr_lconstr c)) l)
76
hov 0 (prlist_with_sep (fun _ -> (fnl ()))
77
(function None -> (str"None") | Some th -> (pp_th th)) sg)
79
(* compute_metamap : constr -> 'a evar_map -> term_with_holes
80
* r�alise le 2. ci-dessus
82
* Pour cela, on renvoie une meta_map qui indique pour chaque meta-variable
83
* si elle correspond � un but (None) ou si elle r�duite � son tour
84
* par un terme de preuve incomplet (Some c).
86
* On a donc l'INVARIANT suivant : le terme c rendu est "de niveau 1"
87
* -- i.e. � plat -- et la meta_map contient autant d'�l�ments qu'il y
88
* a de meta-variables dans c. On suppose de plus que l'ordre dans la
89
* meta_map correspond � celui des buts qui seront engendr�s par le refine.
92
let replace_by_meta env sigma = function
93
| TH (m, mm, sgp) when isMeta (strip_outer_cast m) -> m,mm,sgp
94
| (TH (c,mm,_)) as th ->
95
let n = Evarutil.new_meta() in
97
(* quand on introduit une mv on calcule son type *)
98
let ty = match kind_of_term c with
99
| Lambda (Name id,c1,c2) when isCast c2 ->
100
let _,_,t = destCast c2 in mkNamedProd id c1 t
101
| Lambda (Anonymous,c1,c2) when isCast c2 ->
102
let _,_,t = destCast c2 in mkArrow c1 t
103
| _ -> (* (App _ | Case _) -> *)
104
Retyping.get_type_of_with_meta env sigma mm c
106
| Fix ((_,j),(v,_,_)) ->
107
v.(j) (* en pleine confiance ! *)
108
| _ -> invalid_arg "Tcc.replace_by_meta (TO DO)"
111
mkCast (m,DEFAULTcast, ty),[n,ty],[Some th]
115
let replace_in_array keep_length env sigma a =
116
if array_for_all (function (TH (_,_,[])) -> true | _ -> false) a then
118
let a' = Array.map (function
119
| (TH (c,mm,[])) when not keep_length -> c,mm,[]
120
| th -> replace_by_meta env sigma th) a
122
let v' = Array.map pi1 a' in
123
let mm = Array.fold_left (@) [] (Array.map pi2 a') in
124
let sgp = Array.fold_left (@) [] (Array.map pi3 a') in
128
let id = match n with Name x -> x | _ -> id_of_string "_H" in
129
next_global_ident_away true id (ids_of_named_context (named_context env))
131
let rec compute_metamap env sigma c = match kind_of_term c with
132
(* le terme est directement une preuve *)
133
| (Const _ | Evar _ | Ind _ | Construct _ |
134
Sort _ | Var _ | Rel _) ->
137
(* le terme est une mv => un but *)
141
| Cast (m,_, ty) when isMeta m ->
142
TH (c,[destMeta m,ty],[None])
145
(* abstraction => il faut d�composer si le terme dessous n'est pas pur
146
* attention : dans ce cas il faut remplacer (Rel 1) par (Var x)
147
* o� x est une variable FRAICHE *)
148
| Lambda (name,c1,c2) ->
149
let v = fresh env name in
150
let env' = push_named (v,None,c1) env in
151
begin match compute_metamap env' sigma (subst1 (mkVar v) c2) with
152
(* terme de preuve complet *)
153
| TH (_,_,[]) -> TH (c,[],[])
154
(* terme de preuve incomplet *)
156
let m,mm,sgp = replace_by_meta env' sigma th in
157
TH (mkLambda (Name v,c1,m), mm, sgp)
160
| LetIn (name, c1, t1, c2) ->
161
let v = fresh env name in
162
let th1 = compute_metamap env sigma c1 in
163
let env' = push_named (v,Some c1,t1) env in
164
let th2 = compute_metamap env' sigma (subst1 (mkVar v) c2) in
165
begin match th1,th2 with
166
(* terme de preuve complet *)
167
| TH (_,_,[]), TH (_,_,[]) -> TH (c,[],[])
168
(* terme de preuve incomplet *)
169
| TH (c1,mm1,sgp1), TH (c2,mm2,sgp2) ->
171
if sgp1=[] then (c1,mm1,[])
172
else replace_by_meta env sigma th1 in
174
if sgp2=[] then (c2,mm2,[])
175
else replace_by_meta env' sigma th2 in
176
TH (mkNamedLetIn v m1 t1 m2, mm1@mm2, sgp1@sgp2)
181
let a = Array.map (compute_metamap env sigma) (Array.append [|f|] v) in
184
let v',mm,sgp = replace_in_array false env sigma a in
185
let v'' = Array.sub v' 1 (Array.length v) in
186
TH (mkApp(v'.(0), v''),mm,sgp)
191
| Case (ci,p,cc,v) ->
193
let nbr = Array.length v in
194
let v = Array.append [|p;cc|] v in
195
let a = Array.map (compute_metamap env sigma) v in
198
let v',mm,sgp = replace_in_array false env sigma a in
199
let v'' = Array.sub v' 2 nbr in
200
TH (mkCase (ci,v'.(0),v'.(1),v''),mm,sgp)
206
| Fix ((ni,i),(fi,ai,v)) ->
207
(* TODO: use a fold *)
208
let vi = Array.map (fresh env) fi in
209
let fi' = Array.map (fun id -> Name id) vi in
210
let env' = push_named_rec_types (fi',ai,v) env in
212
(compute_metamap env' sigma)
213
(Array.map (substl (List.map mkVar (Array.to_list vi))) v)
217
let v',mm,sgp = replace_in_array true env' sigma a in
218
let fix = mkFix ((ni,i),(fi',ai,v')) in
224
(* Cast. Est-ce bien exact ? *)
225
| Cast (c,_,t) -> compute_metamap env sigma c
226
(*let TH (c',mm,sgp) = compute_metamap sign c in
227
TH (mkCast (c',t),mm,sgp) *)
229
(* Produit. Est-ce bien exact ? *)
232
error "refine: proof term contains metas in a product."
237
| CoFix (i,(fi,ai,v)) ->
238
let vi = Array.map (fresh env) fi in
239
let fi' = Array.map (fun id -> Name id) vi in
240
let env' = push_named_rec_types (fi',ai,v) env in
242
(compute_metamap env' sigma)
243
(Array.map (substl (List.map mkVar (Array.to_list vi))) v)
247
let v',mm,sgp = replace_in_array true env' sigma a in
248
let cofix = mkCoFix (i,(fi',ai,v')) in
255
(* tcc_aux : term_with_holes -> tactic
257
* R�alise le 3. ci-dessus
260
let rec tcc_aux subst (TH (c,mm,sgp) as _th) gl =
261
let c = substl subst c in
262
match (kind_of_term c,sgp) with
263
(* mv => sous-but : on ne fait rien *)
267
| Cast (c,_,_), _ when isMeta c ->
270
(* terme pur => refine *)
274
(* abstraction => intro *)
275
| Lambda (Name id,_,m), _ ->
276
assert (isMeta (strip_outer_cast m));
278
| [None] -> intro_mustbe_force id gl
280
tclTHEN (introduction id)
281
(onLastHyp (fun id -> tcc_aux (mkVar id::subst) th)) gl
285
| Lambda (Anonymous,_,m), _ -> (* if anon vars are allowed in evars *)
286
assert (isMeta (strip_outer_cast m));
288
| [None] -> tclTHEN intro (onLastHyp (fun id -> clear [id])) gl
292
(onLastHyp (fun id ->
295
(tcc_aux (mkVar (*dummy*) id::subst) th))) gl
299
(* let in without holes in the body => possibly dependent intro *)
300
| LetIn (Name id,c1,t1,c2), _ when not (isMeta (strip_outer_cast c1)) ->
301
let c = pf_concl gl in
302
let newc = mkNamedLetIn id c1 t1 c in
304
(change_in_concl None newc)
306
| [None] -> introduction id
308
tclTHEN (introduction id)
309
(onLastHyp (fun id -> tcc_aux (mkVar id::subst) th))
313
(* let in with holes in the body => unable to handle dependency
314
because of evars limitation, use non dependent assert instead *)
315
| LetIn (Name id,c1,t1,c2), _ ->
317
(assert_tac (Name id) t1)
318
[(match List.hd sgp with
320
| Some th -> onLastHyp (fun id -> tcc_aux (mkVar id::subst) th));
321
(match List.tl sgp with
322
| [] -> refine (subst1 (mkVar id) c2) (* a complete proof *)
323
| [None] -> tclIDTAC (* a meta *)
324
| [Some th] -> (* a partial proof *)
325
onLastHyp (fun id -> tcc_aux (mkVar id::subst) th)
326
| _ -> assert false)]
329
(* fix => tactique Fix *)
330
| Fix ((ni,j),(fi,ai,_)) , _ ->
331
let out_name = function
333
| _ -> error "Recursive functions must have names."
335
let fixes = array_map3 (fun f n c -> (out_name f,succ n,c)) fi ni ai in
336
let firsts,lasts = list_chop j (Array.to_list fixes) in
338
(mutual_fix_with_index
339
(out_name fi.(j)) (succ ni.(j)) (firsts@List.tl lasts) j)
342
| Some th -> tcc_aux subst th) sgp)
345
(* cofix => tactique CoFix *)
346
| CoFix (j,(fi,ai,_)) , _ ->
347
let out_name = function
349
| _ -> error "Recursive functions must have names."
351
let cofixes = array_map2 (fun f c -> (out_name f,c)) fi ai in
352
let firsts,lasts = list_chop j (Array.to_list cofixes) in
354
(mutual_cofix_with_index (out_name fi.(j)) (firsts@List.tl lasts) j)
357
| Some th -> tcc_aux subst th) sgp)
360
(* sinon on fait refine du terme puis appels rec. sur les sous-buts.
361
* c'est le cas pour App et MutCase. *)
366
(function None -> tclIDTAC | Some th -> tcc_aux subst th) sgp)
369
(* Et finalement la tactique refine elle-m�me : *)
371
let refine (evd,c) gl =
372
let sigma = project gl in
373
let evd = Evd.evars_of (Typeclasses.resolve_typeclasses
374
~onlyargs:true ~fail:false (pf_env gl)
375
(Evd.create_evar_defs evd))
377
let c = Evarutil.nf_evar evd c in
378
let (evd,c) = Evarutil.evars_to_metas sigma (evd,c) in
379
(* Relies on Cast's put on Meta's by evars_to_metas, because it is otherwise
380
complicated to update meta types when passing through a binder *)
381
let th = compute_metamap (pf_env gl) evd c in
382
tclTHEN (Refiner.tclEVARS evd) (tcc_aux [] th) gl
added
removed
tactics/refine.ml
