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) `IsTerm
 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    (fun s -> distribute_tac (fun status goal ->
 399       let goalty = get_goalty status goal in
 400       let status,canon,rest =
 401        match !l with
 402           [] ->
 403            (match where with
 404                _,_,(None,_,_)  -> fail (lazy "No term to generalize")
 405              | txt,txtlen,(Some what,_,_) ->
 406                 let status, what =
 407                  disambiguate status (ctx_of goalty) (txt,txtlen,what) None
 408                 in
 409                  status,what,[]
 410            )
 411         | he::tl -> status,he,tl in
 412       let status =
 413        List.fold_left
 414          (fun s t -> unify s (ctx_of goalty) canon t) status rest in
 415       let status, canon = term_of_cic_term status canon (ctx_of goalty) in
 416       instantiate status goal
 417        (mk_cic_term (ctx_of goalty) (NCic.Appl [NCic.Implicit `Term ; canon ]))
 418    ) s) ]
 419 ;;
 420
 421 let cut_tac t =
 422  block_tac [
 423   exact_tac ("",0, Ast.Appl [Ast.Implicit `JustOne; Ast.Implicit `JustOne]);
 424   branch_tac;
 425    pos_tac [3]; exact_tac t;
 426    shift_tac; pos_tac [2]; skip_tac;
 427   merge_tac ]
 428 ;;
 429
 430 let lapply_tac (s,n,t) =
 431  exact_tac (s,n, Ast.Appl [Ast.Implicit `JustOne; t])
 432 ;;
 433
 434 let reduce_tac ~reduction ~where =
 435   let change status t =
 436     match reduction with
 437     | `Normalize perform_delta ->
 438         normalize status
 439          ?delta:(if perform_delta then None else Some max_int) (ctx_of t) t
 440     | `Whd perform_delta ->
 441         whd status
 442          ?delta:(if perform_delta then None else Some max_int) (ctx_of t) t
 443   in
 444   let where = GrafiteDisambiguate.disambiguate_npattern where in
 445   select0_tac ~where ~job:(`ChangeWith change)
 446 ;;
 447
 448 let change_tac ~where ~with_what =
 449   let change status t =
 450     let status, ww = disambiguate status (ctx_of t) with_what  None in
 451     let status = unify status (ctx_of t) t ww in
 452     status, ww
 453   in
 454   let where = GrafiteDisambiguate.disambiguate_npattern where in
 455   select0_tac ~where ~job:(`ChangeWith change)
 456 ;;
 457
 458 let letin_tac ~where ~what:(_,_,w) name =
 459  block_tac [
 460   select_tac ~where ~job:(`Substexpand 1) true;
 461   exact_tac
 462    ("",0,Ast.LetIn((Ast.Ident (name,None),None),w,Ast.Implicit `JustOne));
 463  ]
 464 ;;
 465
 466 let apply_tac (s,n,t) =
 467   let t = Ast.Appl [t; Ast.Implicit `Vector] in
 468   exact_tac (s,n,t)
 469 ;;
 470
 471 type indtyinfo = {
 472         rightno: int;
 473         leftno: int;
 474         consno: int;
 475         lefts: NCic.term list;
 476         rights: NCic.term list;
 477         reference: NReference.reference;
 478  }
 479 ;;
 480
 481 let ref_of_indtyinfo iti = iti.reference;;
 482
 483 let analyze_indty_tac ~what indtyref =
 484  distribute_tac (fun status goal ->
 485   let goalty = get_goalty status goal in
 486   let status, what = disambiguate status (ctx_of goalty) what None in
 487   let status, ty_what = typeof status (ctx_of what) what in
 488   let status, (r,consno,lefts,rights) = analyse_indty status ty_what in
 489   let leftno = List.length lefts in
 490   let rightno = List.length rights in
 491   indtyref := Some {
 492     rightno = rightno; leftno = leftno; consno = consno;
 493     lefts = lefts; rights = rights; reference = r;
 494   };
 495   exec id_tac status goal)
 496 ;;
 497
 498 let sort_of_goal_tac sortref = distribute_tac (fun status goal ->
 499   let goalty = get_goalty status goal in
 500   let status,sort = typeof status (ctx_of goalty) goalty in
 501   let status, sort = fix_sorts status sort in
 502   let status, sort = term_of_cic_term status sort (ctx_of goalty) in
 503    sortref := sort;
 504    status)
 505 ;;
 506
 507 let elim_tac ~what:(txt,len,what) ~where =
 508   let what = txt, len, Ast.Appl [what; Ast.Implicit `Vector] in
 509   let indtyinfo = ref None in
 510   let sort = ref (NCic.Rel 1) in
 511   atomic_tac (block_tac [
 512     analyze_indty_tac ~what indtyinfo;
 513     (fun s -> select_tac
 514       ~where ~job:(`Substexpand ((HExtlib.unopt !indtyinfo).rightno+1)) true s);
 515     sort_of_goal_tac sort;
 516     (fun status ->
 517      let ity = HExtlib.unopt !indtyinfo in
 518      let NReference.Ref (uri, _) = ity.reference in
 519      let name =
 520        NUri.name_of_uri uri ^ "_" ^
 521         snd (NCicElim.ast_of_sort
 522           (match !sort with NCic.Sort x -> x | _ -> assert false))
 523      in
 524      let eliminator =
 525        let _,_,w = what in
 526        Ast.Appl [ Ast.Ident (name,None) ; Ast.Implicit `Vector ; w ]
 527      in
 528      exact_tac ("",0,eliminator) status) ])
 529 ;;
 530
 531 let rewrite_tac ~dir ~what:(_,_,what) ~where status =
 532  let sortref = ref (NCic.Rel 1) in
 533  let status = sort_of_goal_tac sortref status in
 534  let suffix = "_" ^ snd (NCicElim.ast_of_sort
 535    (match !sortref with NCic.Sort x -> x | _ -> assert false))
 536  in
 537  let name =
 538   match dir with
 539      `LeftToRight -> "eq" ^ suffix ^ "_r"
 540    | `RightToLeft -> "eq" ^ suffix
 541  in
 542   block_tac
 543    [ select_tac ~where ~job:(`Substexpand 1) true;
 544      exact_tac
 545       ("",0,
 546        Ast.Appl(Ast.Ident(name,None)::HExtlib.mk_list (Ast.Implicit `JustOne) 5@
 547         [what]))] status
 548 ;;
 549
 550 let intro_tac name =
 551  block_tac
 552   [ exact_tac
 553      ("",0,(Ast.Binder (`Lambda,
 554       (Ast.Ident (name,None),None),Ast.Implicit `JustOne)));
 555     if name = "_" then clear_tac [name] else id_tac ]
 556 ;;
 557
 558 let cases ~what status goal =
 559  let gty = get_goalty status goal in
 560  let status, what = disambiguate status (ctx_of gty) what None in
 561  let status, ty = typeof status (ctx_of what) what in
 562  let status, (ref, consno, _, _) = analyse_indty status ty in
 563  let status, what = term_of_cic_term status what (ctx_of gty) in
 564  let t =
 565   NCic.Match (ref,NCic.Implicit `Term, what,
 566     HExtlib.mk_list (NCic.Implicit `Term) consno)
 567  in
 568  instantiate status goal (mk_cic_term (ctx_of gty) t)
 569 ;;
 570
 571 let cases_tac ~what:(txt,len,what) ~where =
 572   let what = txt, len, Ast.Appl [what; Ast.Implicit `Vector] in
 573   let indtyinfo = ref None in
 574   atomic_tac
 575    (block_tac [
 576       analyze_indty_tac ~what indtyinfo;
 577       (fun s -> select_tac
 578        ~where ~job:(`Substexpand ((HExtlib.unopt !indtyinfo).rightno+1))true s);
 579       distribute_tac (cases ~what) ])
 580 ;;
 581
 582 let case1_tac name =
 583  let name = if name = "_" then "_clearme" else name in
 584  block_tac [ intro_tac name;
 585              cases_tac
 586               ~where:("",0,(None,[],None))
 587               ~what:("",0,Ast.Ident (name,None));
 588              if name = "_clearme" then clear_tac ["_clearme"] else id_tac ]
 589 ;;
 590
 591 let constructor_tac ?(num=1) ~args = distribute_tac (fun status goal ->
 592   if num < 1 then fail (lazy "constructor numbers begin with 1");
 593   let gty = get_goalty status goal in
 594   let status, (r,_,_,_) = analyse_indty status gty in
 595   let ref = NReference.mk_constructor num r in
 596   let t =
 597     if args = [] then Ast.NRef ref else
 598     Ast.Appl (HExtlib.list_concat ~sep:[Ast.Implicit `Vector]
 599       ([Ast.NRef ref] :: List.map (fun _,_,x -> [x]) args))
 600   in
 601   exec (apply_tac ("",0,t)) status goal)
 602 ;;
 603
 604 let assert0_tac (hyps,concl) = distribute_tac (fun status goal ->
 605  let gty = get_goalty status goal in
 606  let eq status ctx t1 t2 =
 607   let status,t1 = disambiguate status ctx t1 None in
 608   let status,t1 = apply_subst status ctx t1 in
 609   let status,t1 = term_of_cic_term status t1 ctx in
 610   let t2 = mk_cic_term ctx t2 in
 611   let status,t2 = apply_subst status ctx t2 in
 612   let status,t2 = term_of_cic_term status t2 ctx in
 613   prerr_endline ("COMPARING: " ^ NCicPp.ppterm ~subst:[] ~metasenv:[] ~context:ctx t1 ^ " vs " ^ NCicPp.ppterm ~subst:[] ~metasenv:[] ~context:ctx t2);
 614   assert (t1=t2);
 615   status
 616  in
 617  let status,gty' = term_of_cic_term status gty (ctx_of gty) in
 618  let status = eq status (ctx_of gty) concl gty' in
 619  let status,_ =
 620   List.fold_right2
 621    (fun (id1,e1) ((id2,e2) as item) (status,ctx) ->
 622      assert (id1=id2 || (prerr_endline (id1 ^ " vs " ^ id2); false));
 623      match e1,e2 with
 624         `Decl t1, NCic.Decl t2 ->
 625           let status = eq status ctx t1 t2 in
 626           status,item::ctx
 627       | `Def (b1,t1), NCic.Def (b2,t2) ->
 628           let status = eq status ctx t1 t2 in
 629           let status = eq status ctx b1 b2 in
 630           status,item::ctx
 631       | _ -> assert false
 632    ) hyps (ctx_of gty) (status,[])
 633  in
 634   exec id_tac status goal)
 635 ;;
 636
 637 let assert_tac seqs status =
 638  match status#stack with
 639   | [] -> assert false
 640   | (g,_,_,_) :: s ->
 641      assert (List.length g = List.length seqs);
 642      (match seqs with
 643          [] -> id_tac
 644        | [seq] -> assert0_tac seq
 645        | _ ->
 646          block_tac
 647           (branch_tac::
 648           HExtlib.list_concat ~sep:[shift_tac]
 649             (List.map (fun seq -> [assert0_tac seq]) seqs)@
 650           [merge_tac])
 651      ) status
 652 ;;
 653