1 (* Copyright (C) 2002, HELM Team.
3 * This file is part of HELM, an Hypertextual, Electronic
4 * Library of Mathematics, developed at the Computer Science
5 * Department, University of Bologna, Italy.
7 * HELM is free software; you can redistribute it and/or
8 * modify it under the terms of the GNU General Public License
9 * as published by the Free Software Foundation; either version 2
10 * of the License, or (at your option) any later version.
12 * HELM is distributed in the hope that it will be useful,
13 * but WITHOUT ANY WARRANTY; without even the implied warranty of
14 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15 * GNU General Public License for more details.
17 * You should have received a copy of the GNU General Public License
18 * along with HELM; if not, write to the Free Software
19 * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
22 * For details, see the HELM World-Wide-Web page,
23 * http://cs.unibo.it/helm/.
26 (* $Id: destructTactic.ml 9774 2009-05-15 19:37:08Z sacerdot $ *)
29 open Continuationals.Stack
33 if debug then (fun x -> prerr_endline (Lazy.force x)) else (fun _ -> ())
39 "z" ^ string_of_int !i
43 let id = if id = "_" then fresh_name () else id in
44 NotationPt.Ident (id,None)
47 let rec mk_prods l t =
50 | hd::tl -> NotationPt.Binder (`Forall, (mk_id hd, None), mk_prods tl t)
57 | l -> NotationPt.Appl l
60 let rec iter f n acc =
62 else iter f (n-1) (f n acc)
65 let subst_metasenv_and_fix_names status =
66 let u,h,metasenv, subst,o = status#obj in
68 NCicUntrusted.map_obj_kind ~skip_body:true
69 (NCicUntrusted.apply_subst status subst []) o
71 status#set_obj(u,h,NCicUntrusted.apply_subst_metasenv status subst metasenv,subst,o)
74 (* input: nome della variabile riscritta
75 * output: lista dei nomi delle variabili il cui tipo dipende dall'input *)
76 let cascade_select_in_ctx status ~subst ctx skip iname =
77 let lctx, rctx = HExtlib.split_nth (iname - 1) ctx in
78 let lctx = List.rev lctx in
79 let rec rm_last = function
81 | hd::tl -> hd::(rm_last tl)
84 let indices,_ = List.fold_left
85 (fun (acc,context) item ->
87 | n,(NCic.Decl s | NCic.Def (s,_))
88 when (not (List.for_all (fun x -> NCicTypeChecker.does_not_occur status ~subst context (x-1) x s) acc)
89 && not (List.mem n skip)) ->
90 List.iter (fun m -> pp (lazy ("acc has " ^ (string_of_int m)))) acc;
91 pp (lazy ("acc occurs in the type of " ^ n));
92 (1::List.map ((+) 1) acc, item::context)
93 | _ -> (List.map ((+) 1) acc, item::context))
95 let indices = rm_last indices in
96 let res = List.map (fun n -> let s,_ = List.nth ctx (n-1) in s) indices in
97 List.iter (fun n -> pp (lazy n)) res;
98 pp (lazy (status#ppcontext ~metasenv:[] ~subst ctx));
102 let rec mk_fresh_name ctx firstch n =
103 let candidate = (String.make 1 firstch) ^ (string_of_int n) in
104 if (List.for_all (fun (s,_) -> s <> candidate) ctx) then candidate
105 else mk_fresh_name ctx firstch (n+1)
108 let arg_list nleft t =
109 let rec drop_prods n t =
112 | NCic.Prod (_,_,ta) -> drop_prods (n-1) ta
113 | _ -> raise (Failure "drop_prods")
115 let rec aux = function
116 | NCic.Prod (_,so,ta) -> so::aux ta
118 in aux (drop_prods nleft t)
121 let nargs it nleft consno =
122 pp (lazy (Printf.sprintf "nargs %d %d" nleft consno));
123 let _,indname,_,cl = it in
124 let _,_,t_k = List.nth cl consno in
125 List.length (arg_list nleft t_k) ;;
127 let default_pattern = "",0,(None,[],Some NotationPt.UserInput);;
129 "",0,(None,[],Some NotationPt.Binder
130 (`Pi, (mk_id "_",Some (NotationPt.Appl
131 [ NotationPt.Implicit `JustOne
132 ; NotationPt.Implicit `JustOne
133 ; NotationPt.UserInput
134 ; NotationPt.Implicit `JustOne ])),
135 NotationPt.Implicit `JustOne));;
137 let prod_pattern_jm =
138 "",0,(None,[],Some NotationPt.Binder
139 (`Pi, (mk_id "_",Some (NotationPt.Appl
140 [ NotationPt.Implicit `JustOne
141 ; NotationPt.Implicit `JustOne
142 ; NotationPt.UserInput
143 ; NotationPt.Implicit `JustOne
144 ; NotationPt.Implicit `JustOne ])),
145 NotationPt.Implicit `JustOne));;
148 "",0,(None,[n, NotationPt.Appl
149 [ NotationPt.Implicit `JustOne
150 ; NotationPt.Implicit `JustOne
151 ; NotationPt.UserInput
152 ; NotationPt.Implicit `JustOne ] ],
155 let hp_pattern_jm n =
156 "",0,(None,[n, NotationPt.Appl
157 [ NotationPt.Implicit `JustOne
158 ; NotationPt.Implicit `JustOne
159 ; NotationPt.UserInput
160 ; NotationPt.Implicit `JustOne
161 ; NotationPt.Implicit `JustOne ] ],
164 (* returns the discrimination = injection+contradiction principle *)
166 let mk_discriminator it ~use_jmeq nleft xyty status =
167 let _,indname,_,cl = it in
170 let mk_eq tys ts us es n =
172 mk_appl [mk_id "jmeq";
173 NotationPt.Implicit `JustOne; List.nth ts n;
174 NotationPt.Implicit `JustOne; List.nth us n]
176 (* eqty = Tn u0 e0...un-1 en-1 *)
178 (List.nth tys n :: iter (fun i acc ->
183 (* params = [T0;t0;...;Tn;tn;u0;e0;un-1;en-1] *)
184 let params = iter (fun i acc ->
186 List.nth ts i :: acc) n
189 List.nth es i:: acc) (n-1) []) in
190 mk_appl [mk_id "eq"; eqty;
191 mk_appl (mk_id ("R" ^ string_of_int n) :: params);
198 let _,name,_ = List.nth cl j in
202 let branch i j ts us =
203 let nargs = nargs it nleft i in
204 let es = List.map (fun x -> mk_id ("e" ^ string_of_int x)) (HExtlib.list_seq 0 nargs) in
208 NotationPt.Binder (`Lambda, (mk_id ("x" ^ string_of_int i), None),
209 NotationPt.Binder (`Lambda, (mk_id ("p" ^ string_of_int i), None),
211 (NotationPt.Implicit (`Tagged ("T" ^ (string_of_int x)))))
212 (HExtlib.list_seq 0 nargs) in
215 NotationPt.Binder (`Lambda, (mk_id ("x" ^ string_of_int i), None),
216 NotationPt.Binder (`Lambda, (mk_id ("p" ^ string_of_int i), None),
218 (mk_appl [mk_id "eq"; NotationPt.Implicit `JustOne;
219 mk_appl (mk_id (kname it i)::
220 List.map (fun x -> mk_id ("x" ^string_of_int x))
221 (HExtlib.list_seq 0 (List.length ts)));
222 mk_appl (mk_id (kname it j)::us)])]
224 (** NotationPt.Binder (`Lambda, (mk_id "e",
227 NotationPt.Implicit `JustOne;
228 mk_appl (mk_id (kname it i)::ts);
229 mk_appl (mk_id (kname it j)::us)])),
230 let ts = ts @ [mk_id "e"] in
233 NotationPt.Implicit `JustOne;
234 mk_appl (mk_id (kname it j)::us)] in
235 let us = us @ [refl2] in *)
236 NotationPt.Binder (`Forall, (mk_id "P", Some (NotationPt.Sort (`NType "1") )),
238 NotationPt.Binder (`Forall, (mk_id "_",
239 Some (iter (fun i acc ->
240 NotationPt.Binder (`Forall, (List.nth es i, Some (mk_eq tys ts us es i)), acc))
242 (** (NotationPt.Binder (`Forall, (mk_id "_",
243 Some (mk_eq tys ts us es nargs)),*)
244 (mk_id "P"))), mk_id "P")
248 let inner i ts = NotationPt.Case
250 (*Some (NotationPt.Binder (`Lambda, (mk_id "y",None),
251 NotationPt.Binder (`Forall, (mk_id "_", Some
252 (mk_appl [mk_id "eq";NotationPt.Implicit
253 `JustOne;(*NotationPt.Implicit `JustOne*)
254 mk_appl (mk_id (kname it i)::ts);mk_id "y"])),
255 NotationPt.Implicit `JustOne )))*)
259 let nargs_kty = nargs it nleft j in
260 let us = iter (fun m acc -> mk_id ("u" ^ (string_of_int m))::acc)
261 (nargs_kty - 1) [] in
263 iter (fun _ acc -> None::acc) (nargs_kty - 1) [] in
264 NotationPt.Pattern (kname it j,
266 List.combine us nones),
268 (HExtlib.list_seq 0 (List.length cl)))
270 let outer = NotationPt.Case
275 let nargs_kty = nargs it nleft i in
276 let ts = iter (fun m acc -> mk_id ("t" ^ (string_of_int m))::acc)
277 (nargs_kty - 1) [] in
279 iter (fun _ acc -> None::acc) (nargs_kty - 1) [] in
280 NotationPt.Pattern (kname it i,
282 List.combine ts nones),
284 (HExtlib.list_seq 0 (List.length cl))) in
285 let principle = NotationPt.Binder (`Lambda, (mk_id "x", Some xyty),
286 NotationPt.Binder (`Lambda, (mk_id "y", Some xyty), outer))
288 pp (lazy ("discriminator = " ^ (NotationPp.pp_term status principle)));
293 let hd_of_term = function
294 | NCic.Appl (hd::_) -> hd
298 let name_of_rel ~context rel =
299 let s, _ = List.nth context (rel-1) in s
302 (* let lookup_in_ctx ~context n =
303 List.nth context ((List.length context) - n - 1)
306 let mk_sym s = NotationPt.Symbol (s,0);;
308 let discriminate_tac ~context cur_eq status =
309 pp (lazy (Printf.sprintf "discriminate: equation %s" (name_of_rel ~context cur_eq)));
311 let dbranch it ~use_jmeq leftno consno =
312 let refl_id = mk_sym "refl" in
313 pp (lazy (Printf.sprintf "dbranch %d %d" leftno consno));
314 let nlist = HExtlib.list_seq 0 (nargs it leftno consno) in
315 (* (\forall ...\forall P.\forall DH : ( ... = ... -> P). P) *)
316 let params = List.map (fun x -> NTactics.intro_tac ("a" ^ string_of_int x)) nlist in
317 NTactics.reduce_tac ~reduction:(`Normalize true) ~where:default_pattern::
319 NTactics.intro_tac "P";
320 NTactics.intro_tac "DH";
321 NTactics.apply_tac ("",0,mk_id "DH");
322 NTactics.apply_tac ("",0,refl_id); (* well, it works even if no goal is selected after applying DH... *)
324 let dbranches it ~use_jmeq leftno =
325 pp (lazy (Printf.sprintf "dbranches %d" leftno));
327 let nbranches = List.length cl in
328 let branches = iter (fun n acc ->
329 let m = nbranches - n - 1 in
330 if m = 0 then acc @ (dbranch it ~use_jmeq leftno m)
331 else acc @ NTactics.shift_tac :: (dbranch it ~use_jmeq
334 if nbranches > 1 then
335 NTactics.branch_tac ~force:false:: branches @ [NTactics.merge_tac]
339 let eq_name,(NCic.Decl s | NCic.Def (s,_)) = List.nth context (cur_eq-1) in
340 let _,ctx' = HExtlib.split_nth cur_eq context in
341 let status, s = NTacStatus.whd status ctx' (mk_cic_term ctx' s) in
342 let status, s = term_of_cic_term status s ctx' in
343 let status, leftno, it, use_jmeq =
344 let it, t1, t2, use_jmeq = match s with
345 | NCic.Appl [_;it;t1;t2] -> it,t1,t2,false
346 | NCic.Appl [_;it;t1;_;t2] -> it,t1,t2,true
347 | _ -> assert false in
348 (* XXX: serve? ho già fatto whd *)
349 let status, it = whd status ctx' (mk_cic_term ctx' it) in
350 let status, it = term_of_cic_term status it ctx' in
351 let _uri,indtyno,its = match it with
352 | NCic.Const (NReference.Ref (uri, NReference.Ind (_,indtyno,_)) as r)
353 | NCic.Appl (NCic.Const
354 (NReference.Ref (uri, NReference.Ind (_,indtyno,_)) as r)::_) ->
355 uri, indtyno, NCicEnvironment.get_checked_indtys status r
356 | _ -> pp (lazy ("discriminate: indty =" ^ status#ppterm
357 ~metasenv:[] ~subst:[] ~context:[] it)) ; assert false in
358 let _,leftno,its,_,_ = its in
359 status, leftno, List.nth its indtyno, use_jmeq
363 let _,_,arity,_ = it in
364 List.length (arg_list 0 arity) in
365 let _,itname,_,_ = it in
366 let params = List.map (fun x -> "a" ^ string_of_int x) (HExtlib.list_seq 1 (itnargs+1)) in
367 let xyty = mk_appl (List.map mk_id (itname::params)) in
368 let print_tac s status = pp s ; status in
371 let status, discr = mk_discriminator it ~use_jmeq leftno xyty status in
372 let cut_term = mk_prods params (NotationPt.Binder (`Forall, (mk_id "x",
374 NotationPt.Binder (`Forall, (mk_id "y", Some xyty),
375 (if use_jmeq then fun tgt ->
376 NotationPt.Binder (`Forall, (mk_id "e",
378 [mk_sym "jmsimeq"; NotationPt.Implicit `JustOne; mk_id "x";
379 NotationPt.Implicit `JustOne; mk_id "y"])),tgt)
381 NotationPt.Binder (`Forall, (mk_id "e",
382 Some (mk_appl [mk_sym "eq";NotationPt.Implicit `JustOne; mk_id "x"; mk_id "y"])),tgt))
383 (mk_appl [discr; mk_id "x"; mk_id "y"(*;mk_id "e"*)])))) in
384 let status = print_tac (lazy ("cut_term = "^ NotationPp.pp_term status cut_term)) status in
385 NTactics.cut_tac ("",0, cut_term)
388 print_tac (lazy "ci sono");
389 NTactics.reduce_tac ~reduction:(`Normalize true) ~where:default_pattern
391 @ List.map (fun x -> NTactics.intro_tac x) params @
392 [NTactics.intro_tac "x";
393 NTactics.intro_tac "y";
394 NTactics.intro_tac "Deq";
395 print_tac (lazy "ci sono 2");
396 NTactics.rewrite_tac ~dir:`RightToLeft ~what:("",0,mk_id "Deq") ~where:default_pattern;
397 NTactics.cases_tac ~what:("",0,mk_id "x") ~where:default_pattern]
398 @ dbranches it ~use_jmeq leftno @
400 print_tac (lazy "ci sono 3");
401 NTactics.intro_tac "#discriminate";
402 NTactics.apply_tac ("",0,mk_appl ([mk_id "#discriminate"]@
403 HExtlib.mk_list (NotationPt.Implicit `JustOne) (List.length params + 2) @
405 (* NTactics.reduce_tac ~reduction:(`Normalize true) ~where:default_pattern; *)
406 NTactics.clear_tac ["#discriminate"];
407 NTactics.merge_tac; print_tac (lazy "the end of discriminate")]
411 let saturate_skip status context skip =
415 let ix = HExtlib.list_index ((=) x) (List.map fst context)
419 fst (cascade_select_in_ctx status ~subst:(get_subst status) context [] (i+1)) @ acc) skip skip)
422 let subst_tac ~context ~dir skip cur_eq =
423 fun status as oldstatus ->
424 let eq_name,(NCic.Decl s | NCic.Def (s,_)) = List.nth context (cur_eq-1) in
425 let _,ctx' = HExtlib.split_nth cur_eq context in
426 let status, s = NTacStatus.whd status ctx' (mk_cic_term ctx' s) in
427 let status, s = term_of_cic_term status s ctx' in
428 let skip = saturate_skip status context skip in
429 pp (lazy (Printf.sprintf "subst: equation %s" eq_name));
430 let l, r = match s with
431 | NCic.Appl [_;_;t1;t2] | NCic.Appl [_;_;t1;_;t2] -> t1,t2
432 | _ -> assert false in
433 let var = match dir with
435 | `RightToLeft -> r in
436 (* let var = match var with
438 | _ -> assert false in *)
439 let names_to_gen, _ =
442 cascade_select_in_ctx status ~subst:(get_subst status) context skip (var+cur_eq)
443 | _ -> cascade_select_in_ctx status ~subst:(get_subst status) context skip cur_eq in
444 let names_to_gen = List.filter (fun n -> n <> eq_name) names_to_gen in
445 if (List.exists (fun x -> List.mem x skip) names_to_gen)
449 NTactics.generalize_tac
450 ~where:("",0,(Some (mk_id x),[], Some NotationPt.UserInput)) in
451 NTactics.block_tac ((List.map gen_tac names_to_gen)@
452 [NTactics.clear_tac names_to_gen;
453 NTactics.rewrite_tac ~dir
454 ~what:("",0,mk_id eq_name) ~where:default_pattern;
455 (* NTactics.reduce_tac ~reduction:(`Normalize true)
456 ~where:default_pattern;*)
457 NTactics.try_tac (NTactics.clear_tac [eq_name])]@
458 (List.map NTactics.intro_tac (List.rev names_to_gen))) status
461 let clearid_tac ~context skip cur_eq =
463 let eq_name,(NCic.Decl s | NCic.Def (s,_)) = List.nth context (cur_eq-1) in
464 let _,ctx' = HExtlib.split_nth cur_eq context in
465 let status, s = NTacStatus.whd status ctx' (mk_cic_term ctx' s) in
466 let status, s = term_of_cic_term status s ctx' in
467 let skip = saturate_skip status context skip in
471 | NCic.Appl [_;_;_;_] -> mk_id "streicherK"
472 | NCic.Appl [_;_;_;_;_] -> mk_id "streicherKjmeq"
475 pp (lazy (Printf.sprintf "clearid: equation %s" eq_name));
476 let names_to_gen, _ =
477 cascade_select_in_ctx ~subst:(get_subst status) context cur_eq in
478 let names_to_gen = names_to_gen @ [eq_name] in
480 NTactics.generalize_tac
481 ~where:("",0,(Some (mk_id x),[], Some NotationPt.UserInput)) in
482 NTactics.block_tac ((List.map gen_tac names_to_gen)@
483 [NTactics.clear_tac names_to_gen;
484 NTactics.apply_tac ("",0, mk_appl [streicher_id;
485 NotationPt.Implicit `JustOne;
486 NotationPt.Implicit `JustOne;
487 NotationPt.Implicit `JustOne;
488 NotationPt.Implicit `JustOne]);
489 NTactics.reduce_tac ~reduction:(`Normalize true)
490 ~where:default_pattern] @
491 (let names_to_intro =
492 match List.rev names_to_gen with
495 List.map NTactics.intro_tac names_to_intro)) status
498 pp (lazy (Printf.sprintf "clearid: equation %s" eq_name));
500 | NCic.Appl [_;_;_;_] ->
502 let streicher_id = mk_id "streicherK"
504 let names_to_gen, _ =
505 cascade_select_in_ctx status ~subst:(get_subst status) context skip cur_eq in
506 let names_to_gen = names_to_gen @ [eq_name] in
508 NTactics.generalize_tac
509 ~where:("",0,(Some (mk_id x),[], Some NotationPt.UserInput)) in
510 NTactics.block_tac ((List.map gen_tac names_to_gen)@
511 [NTactics.clear_tac names_to_gen;
512 NTactics.apply_tac ("",0, mk_appl [streicher_id;
513 NotationPt.Implicit `JustOne;
514 NotationPt.Implicit `JustOne;
515 NotationPt.Implicit `JustOne;
516 NotationPt.Implicit `JustOne]);
517 (* NTactics.reduce_tac ~reduction:(`Normalize true)
518 ~where:default_pattern *)
520 (let names_to_intro =
521 match List.rev names_to_gen with
524 List.map NTactics.intro_tac names_to_intro)) status
525 | NCic.Appl [_;_;_;_;_] ->
527 let streicher_id = mk_id "streicherK"
529 let names_to_gen, _ =
530 cascade_select_in_ctx status ~subst:(get_subst status) context skip cur_eq in
531 let names_to_gen = names_to_gen (* @ [eq_name]*) in
533 NTactics.generalize_tac
534 ~where:("",0,(Some (mk_id x),[], Some NotationPt.UserInput)) in
535 let gen_eq = NTactics.generalize_tac
536 ~where:("",0,(Some (mk_appl [mk_id "jmeq_to_eq";
537 NotationPt.Implicit `JustOne;
538 NotationPt.Implicit `JustOne;
539 NotationPt.Implicit `JustOne;
540 mk_id eq_name]),[], Some NotationPt.UserInput)) in
541 NTactics.block_tac ((List.map gen_tac names_to_gen)@gen_eq::
542 [NTactics.clear_tac names_to_gen;
543 NTactics.try_tac (NTactics.clear_tac [eq_name]);
544 NTactics.apply_tac ("",0, mk_appl [streicher_id;
545 NotationPt.Implicit `JustOne;
546 NotationPt.Implicit `JustOne;
547 NotationPt.Implicit `JustOne;
548 NotationPt.Implicit `JustOne]);
549 (* NTactics.reduce_tac ~reduction:(`Normalize true)
550 ~where:default_pattern *)
552 (let names_to_intro = List.rev names_to_gen in
553 List.map NTactics.intro_tac names_to_intro)) status
557 let get_ctx st goal =
558 ctx_of (get_goalty st goal)
561 (* = select + classify *)
562 let select_eq ctx acc domain status goal =
563 let classify ~use_jmeq ~subst ctx' l r =
564 (* FIXME: metasenv *)
565 if NCicReduction.are_convertible status ~metasenv:[] ~subst ctx' l r
566 then status, `Identity
567 else status, (match hd_of_term l, hd_of_term r with
568 | NCic.Const (NReference.Ref (_,NReference.Con (_,ki,nleft)) as kref),
569 NCic.Const (NReference.Ref (_,NReference.Con (_,kj,_))) ->
570 if ki != kj then `Discriminate (0,true, use_jmeq)
572 let rit = NReference.mk_indty true kref in
573 let _,_,its,_,itno = NCicEnvironment.get_checked_indtys status rit in
574 let it = List.nth its itno in
575 let newprods = nargs it nleft (ki-1) in
576 `Discriminate (newprods, false, use_jmeq)
578 when NCicTypeChecker.does_not_occur status ~subst ctx' (j-1) j r
579 && l = NCic.Rel j -> `Subst `LeftToRight
581 when NCicTypeChecker.does_not_occur status ~subst ctx' (j-1) j l
582 && r = NCic.Rel j -> `Subst `RightToLeft
583 | (NCic.Rel _, _ | _, NCic.Rel _ ) -> `Cycle (* could be a blob too... *)
587 let index = List.length ctx - i in
588 pp (lazy ("provo classify di index = " ^string_of_int index));
589 match (List.nth ctx (index - 1)) with
590 | n, (NCic.Decl ty | NCic.Def (ty,_)) ->
591 (let _,ctx_ty = HExtlib.split_nth index ctx in
592 let status, ty = NTacStatus.whd status ctx_ty (mk_cic_term ctx_ty ty) in
593 let status, ty = term_of_cic_term status ty ctx_ty in
594 pp (lazy (Printf.sprintf "select_eq tries %s" (status#ppterm ~context:ctx_ty ~subst:[] ~metasenv:[] ty)));
595 let status, kind = match ty with
596 | NCic.Appl [NCic.Const (NReference.Ref (u,_)) ;_;l;r]
597 when NUri.name_of_uri u = "eq" ->
598 classify ~use_jmeq:false ~subst:(get_subst status) ctx_ty l r
599 | NCic.Appl [NCic.Const (NReference.Ref (u,_)) ;lty;l;rty;r]
600 when NUri.name_of_uri u = "jmeq" &&
601 NCicReduction.are_convertible status ~metasenv:[]
602 ~subst:(get_subst status) ctx_ty lty rty
603 -> classify ~use_jmeq:true ~subst:(get_subst status) ctx_ty l r
604 | _ -> status, `NonEq
607 let status, goalty = term_of_cic_term status (get_goalty status goal) ctx in
608 status, Some (List.length ctx - i), kind
609 | `Cycle | `Blob | `NonEq -> aux (i+1) (* XXX: skip cyclic/blob equations for now *)
611 if (List.for_all (fun x -> x <> n) acc) &&
612 (List.exists (fun x -> x = n) domain)
613 then status, Some (List.length ctx - i), kind
615 with Failure _ | Invalid_argument _ -> status, None, `Blob
619 let tagged_intro_tac curtag name =
621 | `Notag -> NTactics.intro_tac name
624 [ NTactics.intro_tac name
625 ; NTactics.reduce_tac
626 ~reduction:(`Whd true) ~where:((if use_jmeq then hp_pattern_jm else hp_pattern) name) ]
629 distribute_tac (fun s g ->
630 let eq_name,(NCic.Decl s | NCic.Def (s,_)) = List.nth context (cur_eq-1) in
631 let _,ctx' = HExtlib.split_nth cur_eq context in
632 let status, s = NTacStatus.whd status ctx' (mk_cic_term ctx' s) in
633 let status, s = term_of_cic_term status s ctx' in
636 | NCic.Appl [_;it;t1;t2] -> false
637 | NCic.Appl [_;it;t1;_;t2] -> true
638 | _ -> assert false in
640 let it, t1, t2, use_jmeq = match s with
641 | NCic.Appl [_;it;t1;t2] -> it,t1,t2,false
642 | NCic.Appl [_;it;t1;_;t2] -> it,t1,t2,true
643 | _ -> assert false in
644 [ NTactics.intro_tac name
645 ; NTactics.reduce_tac ~reduction:(`Whd true) ~where:prod_pattern ]*)
648 let rec destruct_tac0 tags acc domain skip status goal =
654 let pptags tags = String.concat ", " (List.map pptag tags) in
655 let ctx = get_ctx status goal in
656 let subst = get_subst status in
657 let get_newgoal os ns ogoal =
658 let go, gc = NTactics.compare_statuses ~past:os ~present:ns in
659 let go' = ([ogoal] @- gc) @+ go in
660 match go' with [] -> assert false | g::_ -> g
662 let status, selection, kind = select_eq ctx acc domain status goal in
663 pp (lazy ("destruct: acc is " ^ String.concat "," acc ));
664 match selection, kind with
666 pp (lazy (Printf.sprintf
667 "destruct: no selection, context is %s, stack is %s"
668 (status#ppcontext ~metasenv:[] ~subst ctx) (pptags tags)));
672 let fresh = mk_fresh_name ctx 'e' 0 in
673 let status' = NTactics.exec (tagged_intro_tac curtag fresh) status goal in
674 destruct_tac0 tags' acc (fresh::domain) skip status'
675 (get_newgoal status status' goal))
676 | Some cur_eq, `Discriminate (newprods,conflict,use_jmeq) ->
677 pp (lazy (Printf.sprintf
678 "destruct: discriminate - nselection is %d, context is %s,stack is %s"
679 cur_eq (status#ppcontext ~metasenv:[] ~subst ctx) (pptags tags)));
680 let status' = NTactics.exec (discriminate_tac ~context:ctx cur_eq) status goal in
681 if conflict then status'
683 let newtags = HExtlib.mk_list (`Eq use_jmeq) newprods in
684 destruct_tac0 (newtags@tags)
685 (name_of_rel ~context:ctx cur_eq::acc)
686 (List.filter (fun x -> x <> name_of_rel ~context:ctx cur_eq) domain)
688 status' (get_newgoal status status' goal)
689 | Some cur_eq, `Subst dir ->
690 pp (lazy (Printf.sprintf
691 "destruct: subst - selection is %d, context is %s, stack is %s"
692 cur_eq (status#ppcontext ~metasenv:[] ~subst ctx) (pptags tags)));
693 let status' = NTactics.exec (subst_tac ~context:ctx ~dir skip cur_eq) status goal in
694 pp (lazy (Printf.sprintf " ctx after subst = %s" (status#ppcontext ~metasenv:[] ~subst (get_ctx status' (get_newgoal status status' goal)))));
695 let eq_name,_ = List.nth ctx (cur_eq-1) in
696 let newgoal = get_newgoal status status' goal in
699 let _ = NTactics.find_in_context eq_name (get_ctx status' newgoal) in false
701 let rm_eq b l = if b then List.filter (fun x -> x <> eq_name) l else l in
702 let acc = rm_eq has_cleared acc in
703 let skip = rm_eq has_cleared skip in
704 let domain = rm_eq has_cleared domain in
705 destruct_tac0 tags acc domain skip status' newgoal
706 | Some cur_eq, `Identity ->
707 pp (lazy (Printf.sprintf
708 "destruct: identity - selection is %d, context is %s, stack is %s"
709 cur_eq (status#ppcontext ~metasenv:[] ~subst ctx) (pptags tags)));
710 let eq_name,_ = List.nth ctx (cur_eq-1) in
711 let status' = NTactics.exec (clearid_tac ~context:ctx skip cur_eq) status goal in
712 let newgoal = get_newgoal status status' goal in
715 let _ = NTactics.find_in_context eq_name (get_ctx status' newgoal) in false
717 let rm_eq b l = if b then List.filter (fun x -> x <> eq_name) l else l in
718 let acc = rm_eq has_cleared acc in
719 let skip = rm_eq has_cleared skip in
720 let domain = rm_eq has_cleared domain in
721 destruct_tac0 tags acc domain skip status' newgoal
722 | Some cur_eq, `Cycle -> (* TODO, should never happen *)
723 pp (lazy (Printf.sprintf
724 "destruct: cycle - selection is %d, context is %s, stack is %s"
725 cur_eq (status#ppcontext ~metasenv:[] ~subst ctx) (pptags tags)));
727 | Some cur_eq, `Blob ->
728 pp (lazy (Printf.sprintf
729 "destruct: blob - selection is %d, context is %s, stack is %s"
730 cur_eq (status#ppcontext ~metasenv:[] ~subst ctx) (pptags tags)));
735 let destruct_tac dom skip s =
736 NTactics.distribute_tac
738 let ctx = get_ctx s' g in
739 let domain = match dom with
740 | None -> List.map (fun (n,_) -> n) ctx
743 destruct_tac0 [] [] domain skip s' g) s;;