]> matita.cs.unibo.it Git - helm.git/blob - helm/software/components/ng_tactics/nTactics.ml
Smarter implementation of instantiate to avoid re-checking twice the same term.
[helm.git] / helm / software / components / ng_tactics / nTactics.ml
1 (*
2     ||M||  This file is part of HELM, an Hypertextual, Electronic        
3     ||A||  Library of Mathematics, developed at the Computer Science     
4     ||T||  Department, University of Bologna, Italy.                     
5     ||I||                                                                
6     ||T||  HELM is free software; you can redistribute it and/or         
7     ||A||  modify it under the terms of the GNU General Public License   
8     \   /  version 2 or (at your option) any later version.      
9      \ /   This software is distributed as is, NO WARRANTY.     
10       V_______________________________________________________________ *)
11
12 (* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *)
13
14 open Printf
15
16 let debug = false
17 let debug_print s = if debug then prerr_endline (Lazy.force s) else ()
18
19 open Continuationals.Stack
20 open NTacStatus
21 module Ast = CicNotationPt
22
23 let id_tac status = status ;;
24 let print_tac print_status message status = 
25   if print_status then pp_status status;
26   prerr_endline message; 
27   status
28 ;;
29
30 let dot_tac status =
31   let gstatus = 
32     match status#stack with
33     | [] -> assert false
34     | ([], _, [], _) :: _ as stack ->
35         (* backward compatibility: do-nothing-dot *)
36         stack
37     | (g, t, k, tag) :: s ->
38         match filter_open g, k with
39         | loc :: loc_tl, _ -> 
40              (([ loc ], t, loc_tl @+ k, tag) :: s) 
41         | [], loc :: k ->
42             assert (is_open loc);
43             (([ loc ], t, k, tag) :: s)
44         | _ -> fail (lazy "can't use \".\" here")
45   in
46    status#set_stack gstatus
47 ;;
48
49 let branch_tac status =
50   let gstatus = 
51     match status#stack with
52     | [] -> assert false
53     | (g, t, k, tag) :: s ->
54           match init_pos g with (* TODO *)
55           | [] | [ _ ] -> fail (lazy "too few goals to branch");
56           | loc :: loc_tl ->
57                ([ loc ], [], [], `BranchTag) :: (loc_tl, t, k, tag) :: s
58   in
59    status#set_stack gstatus
60 ;;
61
62 let shift_tac status =
63   let gstatus = 
64     match status#stack with
65     | (g, t, k, `BranchTag) :: (g', t', k', tag) :: s ->
66           (match g' with
67           | [] -> fail (lazy "no more goals to shift")
68           | loc :: loc_tl ->
69                 (([ loc ], t @+ filter_open g @+ k, [],`BranchTag)
70                 :: (loc_tl, t', k', tag) :: s))
71      | _ -> fail (lazy "can't shift goals here")
72   in
73    status#set_stack gstatus
74 ;;
75
76 let pos_tac i_s status =
77   let gstatus = 
78     match status#stack with
79     | [] -> assert false
80     | ([ loc ], t, [],`BranchTag) :: (g', t', k', tag) :: s
81       when is_fresh loc ->
82         let l_js = List.filter (fun (i, _) -> List.mem i i_s) ([loc] @+ g') in
83           ((l_js, t , [],`BranchTag)
84            :: (([ loc ] @+ g') @- l_js, t', k', tag) :: s)
85     | _ -> fail (lazy "can't use relative positioning here")
86   in
87    status#set_stack gstatus
88 ;;
89
90 let case_tac lab status =
91   let gstatus = 
92     match status#stack with
93     | [] -> assert false
94     | ([ loc ], t, [],`BranchTag) :: (g', t', k', tag) :: s
95       when is_fresh loc ->
96         let l_js =
97           List.filter 
98            (fun curloc -> 
99               let _,_,metasenv,_,_ = status#obj in
100               match NCicUtils.lookup_meta (goal_of_loc curloc) metasenv with
101                   attrs,_,_ when List.mem (`Name lab) attrs -> true
102                 | _ -> false) ([loc] @+ g') in
103           ((l_js, t , [],`BranchTag)
104            :: (([ loc ] @+ g') @- l_js, t', k', tag) :: s)
105     | _ -> fail (lazy "can't use relative positioning here")
106   in
107    status#set_stack gstatus
108 ;;
109
110 let wildcard_tac status =
111   let gstatus = 
112     match status#stack with
113     | [] -> assert false
114     | ([ loc ] , t, [], `BranchTag) :: (g', t', k', tag) :: s
115        when is_fresh loc ->
116             (([loc] @+ g', t, [], `BranchTag) :: ([], t', k', tag) :: s)
117     | _ -> fail (lazy "can't use wildcard here")
118   in
119    status#set_stack gstatus
120 ;;
121
122 let merge_tac status =
123   let gstatus = 
124     match status#stack with
125     | [] -> assert false
126     | (g, t, k,`BranchTag) :: (g', t', k', tag) :: s ->
127         ((t @+ filter_open g @+ g' @+ k, t', k', tag) :: s)
128     | _ -> fail (lazy "can't merge goals here")
129   in
130    status#set_stack gstatus
131 ;;
132       
133 let focus_tac gs status =
134   let gstatus = 
135     match status#stack with
136     | [] -> assert false
137     | s -> assert(gs <> []);
138           let stack_locs =
139             let add_l acc _ _ l = if is_open l then l :: acc else acc in
140             fold ~env:add_l ~cont:add_l ~todo:add_l [] s
141           in
142           List.iter
143             (fun g ->
144               if not (List.exists (fun l -> goal_of_loc l = g) stack_locs) then
145                 fail (lazy (sprintf "goal %d not found (or closed)" g)))
146             gs;
147           (zero_pos gs, [], [], `FocusTag) :: deep_close gs s
148   in
149    status#set_stack gstatus
150 ;;
151
152 let unfocus_tac status =
153   let gstatus = 
154     match status#stack with
155     | [] -> assert false
156     | (g, [], [], `FocusTag) :: s when filter_open g = [] -> s
157     | _ as s -> fail (lazy ("can't unfocus, some goals are still open:\n"^
158       Continuationals.Stack.pp s))
159   in
160    status#set_stack gstatus
161 ;;
162
163 let skip_tac status =
164   let gstatus = 
165     match status#stack with
166     | [] -> assert false
167     | (gl, t, k, tag) :: s -> 
168         let gl = List.map switch_of_loc gl in
169         if List.exists (function Open _ -> true | Closed _ -> false) gl then 
170           fail (lazy "cannot skip an open goal")
171         else 
172           ([],t,k,tag) :: s
173   in
174    status#set_stack gstatus
175 ;;
176
177 let block_tac l status =
178   List.fold_left (fun status tac -> tac status) status l
179 ;;
180
181
182 let compare_statuses ~past ~present =
183  let _,_,past,_,_ = past#obj in 
184  let _,_,present,_,_ = present#obj in 
185  List.map fst (List.filter (fun (i,_) -> not(List.mem_assoc i past)) present),
186  List.map fst (List.filter (fun (i,_) -> not (List.mem_assoc i present)) past)
187 ;;
188
189
190
191 (* Exec and distribute_tac form a retraction pair:
192     1) exec (distribute_tac low_tac) (s,i) = low_tac (s,i)
193     2) tac [s]::G = G1::...::Gn::G' && G' is G with some goals closed =>
194          distribute_tac (exec tac) [s]::G = (G1@...Gn)::G'
195     3) tac G = distribute_tac (exec tac) G if  
196        tac = distribute_tac lowtac
197     4) atomic_tac t === distribute_tac (exec t)
198
199    Note that executing an high tactic on a set of goals may be stronger
200    than executing the same tactic on those goals, but once at a time
201    (e.g. the tactic could perform a global analysis of the set of goals)
202 *)
203
204 let exec tac (low_status : #lowtac_status) g =
205   let stack = [ [0,Open g], [], [], `NoTag ] in
206   let status =
207    (new NTacStatus.status low_status#obj stack)#set_estatus low_status
208   in
209   let status = tac status in
210    (low_status#set_estatus status)#set_obj status#obj
211 ;;
212
213 let distribute_tac tac (status : #tac_status) =
214   match status#stack with
215   | [] -> assert false
216   | (g, t, k, tag) :: s ->
217       debug_print (lazy ("context length " ^string_of_int (List.length g)));
218       let rec aux s go gc =
219         function
220         | [] -> 
221             debug_print (lazy "no selected goals");
222             s, go, gc
223         | loc :: loc_tl ->
224             debug_print (lazy "inner eval tactical");
225             let s, go, gc =
226               if List.exists ((=) (goal_of_loc loc)) gc then
227                 s, go, gc
228               else
229                 match switch_of_loc loc with
230                 | Closed _ -> fail (lazy "cannot apply to a Closed goal")
231                 | Open n -> 
232                    let sn = tac s n in
233                    let go', gc' = compare_statuses ~past:s ~present:sn in
234                    sn, ((go @+ [n]) @- gc') @+ go', gc @+ gc'
235             in
236             aux s go gc loc_tl
237       in
238       let s0 = (new NTacStatus.status status#obj ())#set_estatus status in
239       let s0, go0, gc0 = s0, [], [] in
240       let sn, gon, gcn = aux s0 go0 gc0 g in
241       debug_print (lazy ("opened: "
242         ^ String.concat " " (List.map string_of_int gon)));
243       debug_print (lazy ("closed: "
244         ^ String.concat " " (List.map string_of_int gcn)));
245       let stack =
246         (zero_pos gon, t @~- gcn, k @~- gcn, tag) :: deep_close gcn s
247       in
248        ((status#set_stack stack)#set_obj(sn:>lowtac_status)#obj)#set_estatus sn
249 ;;
250
251 let atomic_tac htac : #tac_status as 'a -> 'a = distribute_tac (exec htac) ;;
252
253 let repeat_tac t s = 
254   let rec repeat t (status : #tac_status as 'a) : 'a = 
255     try repeat t (t status)
256     with NTacStatus.Error _ -> status
257   in
258     atomic_tac (repeat t) s
259 ;;
260
261
262 let try_tac tac status =
263   try
264     tac status
265   with NTacStatus.Error _ ->
266     status
267 ;;
268
269 let first_tac tacl status =
270   let res = 
271    HExtlib.list_findopt
272     (fun tac _ -> try Some (tac status) with NTacStatus.Error _ -> None) tacl
273   in
274     match res with
275       | None -> fail (lazy "No tactics left")
276       | Some x -> x
277 ;;
278
279 let exact_tac t : 's tactic = distribute_tac (fun status goal ->
280  instantiate_with_ast status goal t)
281 ;;
282
283 let assumption_tac status = distribute_tac (fun status goal ->
284   let gty = get_goalty status goal in
285   let context = ctx_of gty in
286   let htac = 
287    first_tac
288     (List.map (fun (name,_) -> exact_tac ("",0,(Ast.Ident (name,None))))
289       context)
290   in
291     exec htac status goal) status
292 ;;
293
294 let find_in_context name context =
295   let rec aux acc = function
296     | [] -> raise Not_found
297     | (hd,_) :: tl when hd = name -> acc
298     | _ :: tl ->  aux (acc + 1) tl
299   in
300   aux 1 context
301 ;;
302
303 let clear_tac names =
304  if names = [] then id_tac
305  else
306   distribute_tac (fun status goal ->
307    let goalty = get_goalty status goal in
308    let js =
309      List.map 
310      (fun name -> 
311         try find_in_context name (ctx_of goalty)
312         with Not_found -> 
313           fail (lazy ("hypothesis '" ^ name ^ "' not found"))) 
314      names
315    in
316    let n,h,metasenv,subst,o = status#obj in
317    let metasenv,subst,_ = NCicMetaSubst.restrict metasenv subst goal js in
318     status#set_obj (n,h,metasenv,subst,o))
319 ;;
320
321 let generalize0_tac args =
322  if args = [] then id_tac
323  else exact_tac ("",0,Ast.Appl (Ast.Implicit `JustOne :: args))
324 ;;
325
326 let select0_tac ~where:(wanted,hyps,where) ~job  =
327  let found, postprocess = 
328    match job with
329    | `Substexpand argsno -> mk_in_scope, mk_out_scope argsno
330    | `Collect l -> (fun s t -> l := t::!l; mk_in_scope s t), mk_out_scope 1
331    | `ChangeWith f -> f,(fun s t -> s, t)
332  in
333  distribute_tac (fun status goal ->
334    let goalty = get_goalty status goal in
335    let path = 
336      match where with None -> NCic.Implicit `Term | Some where -> where 
337    in
338    let status, newgoalctx =
339       List.fold_right
340        (fun (name,d as entry) (status,ctx) ->
341          try
342           let path = List.assoc name hyps in
343            match d with
344               NCic.Decl ty ->
345                let status,ty =
346                 select_term status ~found ~postprocess (mk_cic_term ctx ty)
347                  (wanted,path) in
348                let status,ty = term_of_cic_term status ty ctx in
349                 status,(name,NCic.Decl ty)::ctx
350             | NCic.Def (bo,ty) ->
351                let status,bo =
352                 select_term status ~found ~postprocess (mk_cic_term ctx bo)
353                  (wanted,path) in
354                let status,bo = term_of_cic_term status bo ctx in
355                 status,(name,NCic.Def (bo,ty))::ctx
356          with
357           Not_found -> status, entry::ctx
358        ) (ctx_of goalty) (status,[])
359    in
360    let status, newgoalty = 
361      select_term status ~found ~postprocess goalty (wanted,path) in
362    (* WARNING: the next two lines simply change the context of newgoalty
363       from the old to the new one. Otherwise mk_meta will do that herself,
364       calling relocate that calls delift. However, newgoalty is now
365       ?[out_scope] and thus the delift would trigger the special unification
366       case, which is wrong now :-( *)
367    let status,newgoalty = term_of_cic_term status newgoalty (ctx_of goalty) in
368    let newgoalty = mk_cic_term newgoalctx newgoalty in
369
370    let status, instance = 
371      mk_meta status newgoalctx (`Decl newgoalty) 
372    in
373    instantiate status goal instance)
374 ;;
375
376 let select_tac ~where ~job move_down_hyps = 
377  let (wanted,hyps,where) = GrafiteDisambiguate.disambiguate_npattern where in
378  let path = 
379   match where with None -> NCic.Implicit `Term | Some where -> where in
380  if not move_down_hyps then
381   select0_tac ~where:(wanted,hyps,Some path) ~job
382  else
383   let path = 
384    List.fold_left
385      (fun path (name,path_name) -> NCic.Prod ("_",path_name,path))
386      path (List.rev hyps)
387   in
388    block_tac [ 
389      generalize0_tac (List.map (fun (name,_) -> Ast.Ident (name,None)) hyps);
390      select0_tac ~where:(wanted,[],Some path) ~job;
391      clear_tac (List.map fst hyps) ]
392 ;;
393
394 let generalize_tac ~where = 
395  let l = ref [] in
396  block_tac [ 
397    select_tac ~where ~job:(`Collect l) true; 
398    print_tac true "ha selezionato?";
399    (fun s -> distribute_tac (fun status goal ->
400       let goalty = get_goalty status goal in
401       let status,canon,rest =
402        match !l with
403           [] ->
404            (match where with
405                _,_,(None,_,_)  -> fail (lazy "No term to generalize")
406              | txt,txtlen,(Some what,_,_) ->
407                 let status, what =
408                  disambiguate status (ctx_of goalty) (txt,txtlen,what) None
409                 in
410                  status,what,[]
411            )
412         | he::tl -> status,he,tl in
413       let status = 
414        List.fold_left 
415          (fun s t -> unify s (ctx_of goalty) canon t) status rest in
416       let status, canon = term_of_cic_term status canon (ctx_of goalty) in
417       instantiate status goal 
418        (mk_cic_term (ctx_of goalty) (NCic.Appl [NCic.Implicit `Term ; canon ]))
419    ) s) ]
420 ;;
421
422 let cut_tac t = 
423  block_tac [ 
424   exact_tac ("",0, Ast.Appl [Ast.Implicit `JustOne; Ast.Implicit `JustOne]);
425   branch_tac;
426    pos_tac [2]; exact_tac t;
427    shift_tac; pos_tac [1]; skip_tac;
428   merge_tac ]
429 ;;
430
431 let lapply_tac (s,n,t) = 
432  exact_tac (s,n, Ast.Appl [Ast.Implicit `JustOne; t])
433 ;;
434
435 let reduce_tac ~reduction ~where =
436   let change status t = 
437     match reduction with
438     | `Normalize perform_delta ->
439         normalize status
440          ?delta:(if perform_delta then None else Some max_int) (ctx_of t) t
441     | `Whd perform_delta -> 
442         whd status
443          ?delta:(if perform_delta then None else Some max_int) (ctx_of t) t
444   in
445   let where = GrafiteDisambiguate.disambiguate_npattern where in
446   select0_tac ~where ~job:(`ChangeWith change)
447 ;;
448
449 let change_tac ~where ~with_what =
450   let change status t = 
451     let status, ww = disambiguate status (ctx_of t) with_what  None in
452     let status = unify status (ctx_of t) t ww in
453     status, ww
454   in
455   let where = GrafiteDisambiguate.disambiguate_npattern where in
456   select0_tac ~where ~job:(`ChangeWith change)
457 ;;
458
459 let letin_tac ~where ~what:(_,_,w) name =
460  block_tac [
461   select_tac ~where ~job:(`Substexpand 1) true;
462   exact_tac
463    ("",0,Ast.LetIn((Ast.Ident (name,None),None),w,Ast.Implicit `JustOne));
464  ]
465 ;;
466
467 let apply_tac (s,n,t) = 
468   let t = Ast.Appl [t; Ast.Implicit `Vector] in
469   exact_tac (s,n,t)
470 ;;
471
472 type indtyinfo = {
473         rightno: int;
474         leftno: int;
475         consno: int;
476         lefts: NCic.term list;
477         rights: NCic.term list;
478         reference: NReference.reference;
479  }
480 ;;
481
482 let analyze_indty_tac ~what indtyref =
483  distribute_tac (fun status goal ->
484   let goalty = get_goalty status goal in
485   let status, what = disambiguate status (ctx_of goalty) what None in
486   let status, ty_what = typeof status (ctx_of what) what in 
487   let status, (r,consno,lefts,rights) = analyse_indty status ty_what in
488   let leftno = List.length lefts in
489   let rightno = List.length rights in
490   indtyref := Some { 
491     rightno = rightno; leftno = leftno; consno = consno;
492     lefts = lefts; rights = rights; reference = r;
493   };
494   exec id_tac status goal)
495 ;;
496
497 let sort_of_goal_tac sortref = distribute_tac (fun status goal ->
498   let goalty = get_goalty status goal in
499   let status,sort = typeof status (ctx_of goalty) goalty in
500   let sort = fix_sorts sort in
501   let status, sort = term_of_cic_term status sort (ctx_of goalty) in
502    sortref := sort;
503    status)
504 ;;
505
506 let elim_tac ~what:(txt,len,what) ~where = 
507   let what = txt, len, Ast.Appl [what; Ast.Implicit `Vector] in
508   let indtyinfo = ref None in
509   let sort = ref (NCic.Rel 1) in
510   atomic_tac (block_tac [
511     analyze_indty_tac ~what indtyinfo;    
512     (fun s -> select_tac 
513       ~where ~job:(`Substexpand ((HExtlib.unopt !indtyinfo).rightno+1)) true s);
514     sort_of_goal_tac sort;
515     (fun status ->
516      let ity = HExtlib.unopt !indtyinfo in
517      let NReference.Ref (uri, _) = ity.reference in
518      let name = 
519        NUri.name_of_uri uri ^ "_" ^
520         snd (NCicElim.ast_of_sort 
521           (match !sort with NCic.Sort x -> x | _ -> assert false))
522      in
523      let eliminator = 
524        let _,_,w = what in
525        Ast.Appl [ Ast.Ident (name,None) ; Ast.Implicit `Vector ; w ]
526      in
527      exact_tac ("",0,eliminator) status) ]) 
528 ;;
529
530 let rewrite_tac ~dir ~what:(_,_,what) ~where status =
531  let sortref = ref (NCic.Rel 1) in
532  let status = sort_of_goal_tac sortref status in
533  let suffix = "_" ^ snd (NCicElim.ast_of_sort 
534    (match !sortref with NCic.Sort x -> x | _ -> assert false))
535  in
536  let name =
537   match dir with
538      `LeftToRight -> "eq" ^ suffix ^ "_r"
539    | `RightToLeft -> "eq" ^ suffix
540  in
541   block_tac
542    [ select_tac ~where ~job:(`Substexpand 1) true;
543      exact_tac
544       ("",0,
545        Ast.Appl(Ast.Ident(name,None)::HExtlib.mk_list (Ast.Implicit `JustOne) 5@
546         [what]))] status
547 ;;
548
549 let intro_tac name =
550  block_tac
551   [ exact_tac
552      ("",0,(Ast.Binder (`Lambda,
553       (Ast.Ident (name,None),None),Ast.Implicit `JustOne)));
554     if name = "_" then clear_tac [name] else id_tac ]
555 ;;
556
557 let cases ~what status goal =
558  let gty = get_goalty status goal in
559  let status, what = disambiguate status (ctx_of gty) what None in
560  let status, ty = typeof status (ctx_of what) what in
561  let status, (ref, consno, _, _) = analyse_indty status ty in
562  let status, what = term_of_cic_term status what (ctx_of gty) in
563  let t =
564   NCic.Match (ref,NCic.Implicit `Term, what,
565     HExtlib.mk_list (NCic.Implicit `Term) consno)
566  in
567  instantiate status goal (mk_cic_term (ctx_of gty) t)
568 ;;
569
570 let cases_tac ~what:(txt,len,what) ~where = 
571   let what = txt, len, Ast.Appl [what; Ast.Implicit `Vector] in
572   let indtyinfo = ref None in
573   atomic_tac 
574    (block_tac [
575       analyze_indty_tac ~what indtyinfo;
576       (fun s -> select_tac 
577        ~where ~job:(`Substexpand ((HExtlib.unopt !indtyinfo).rightno+1))true s);
578       distribute_tac (cases ~what) ])
579 ;;
580
581 let case1_tac name =
582  let name = if name = "_" then "_clearme" else name in
583  block_tac [ intro_tac name; 
584              cases_tac 
585               ~where:("",0,(None,[],None)) 
586               ~what:("",0,Ast.Ident (name,None));
587              if name = "_clearme" then clear_tac ["_clearme"] else id_tac ]
588 ;;
589
590 let constructor ?(num=1) ~args status goal = 
591   if num < 1 then fail (lazy "constructor numbers begin with 1");
592   let gty = get_goalty status goal in
593   let status, (r,_,_,_) = analyse_indty status gty in
594   let ref = NReference.mk_constructor num r in
595   let t = 
596     if args = [] then Ast.NRef ref else
597     Ast.Appl (HExtlib.list_concat ~sep:[Ast.Implicit `Vector]
598       ([Ast.NRef ref] :: List.map (fun _,_,x -> [x]) args))
599   in
600   exec (apply_tac ("",0,t)) status goal
601 ;;
602
603 let constructor_tac ?num ~args = distribute_tac (constructor ?num ~args);;
604
605 let assert0_tac (hyps,concl) = distribute_tac (fun status goal ->
606  let gty = get_goalty status goal in
607  let eq status ctx t1 t2 =
608   let status,t1 = disambiguate status ctx t1 None in
609   let status,t1 = apply_subst status ctx t1 in
610   let status,t1 = term_of_cic_term status t1 ctx in
611   let t2 = mk_cic_term ctx t2 in
612   let status,t2 = apply_subst status ctx t2 in
613   let status,t2 = term_of_cic_term status t2 ctx in
614   prerr_endline ("COMPARING: " ^ NCicPp.ppterm ~subst:[] ~metasenv:[] ~context:ctx t1 ^ " vs " ^ NCicPp.ppterm ~subst:[] ~metasenv:[] ~context:ctx t2);
615   assert (t1=t2);
616   status
617  in
618  let status,gty' = term_of_cic_term status gty (ctx_of gty) in
619  let status = eq status (ctx_of gty) concl gty' in
620  let status,_ =
621   List.fold_right2
622    (fun (id1,e1) ((id2,e2) as item) (status,ctx) ->
623      assert (id1=id2 || (prerr_endline (id1 ^ " vs " ^ id2); false));
624      match e1,e2 with
625         `Decl t1, NCic.Decl t2 ->
626           let status = eq status ctx t1 t2 in
627           status,item::ctx
628       | `Def (b1,t1), NCic.Def (b2,t2) ->
629           let status = eq status ctx t1 t2 in
630           let status = eq status ctx b1 b2 in
631           status,item::ctx
632       | _ -> assert false
633    ) hyps (ctx_of gty) (status,[])
634  in
635   exec id_tac status goal)
636 ;;
637
638 let assert_tac seqs status =
639  match status#stack with
640   | [] -> assert false
641   | (g,_,_,_) :: s ->
642      assert (List.length g = List.length seqs);
643      (match seqs with
644          [] -> id_tac
645        | [seq] -> assert0_tac seq
646        | _ ->
647          block_tac
648           (branch_tac::
649           HExtlib.list_concat ~sep:[shift_tac]
650             (List.map (fun seq -> [assert0_tac seq]) seqs)@
651           [merge_tac])
652      ) status
653 ;;
654