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