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, p) :: s ->
  38         match filter_open g, k with
  39         | loc :: loc_tl, _ ->
  40              (([ loc ], t, loc_tl @+ k, tag, p) :: s)
  41         | [], loc :: k ->
  42             assert (is_open loc);
  43             (([ loc ], t, k, tag, p) :: 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, p) :: 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, p) :: 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, p) :: (g', t', k', tag, p') :: 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, p)
  71                 :: (loc_tl, t', k', tag, p') :: 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, p) :: (g', t', k', tag, p') :: 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, p)
  85            :: (([ loc ] @+ g') @- l_js, t', k', tag, p') :: 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, p) :: (g', t', k', tag, p') :: 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, p)
 105            :: (([ loc ] @+ g') @- l_js, t', k', tag, p') :: 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, p) :: (g', t', k', tag, p') :: s
 116        when is_fresh loc ->
 117             (([loc] @+ g', t, [], `BranchTag, p) :: ([], t', k', tag, p') :: 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, p) :: s ->
 128         ((t @+ filter_open g @+ g' @+ k, t', k', tag, p) :: 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, p) :: 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,p) :: 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, p) :: 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, p) :: 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,_) :: _ 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         cl: NCic.constructor list;
 496  }
 497 ;;
 498
 499 let ref_of_indtyinfo iti = iti.reference;;
 500
 501 let analyze_indty_tac ~what indtyref =
 502  distribute_tac (fun (status as orig_status) goal ->
 503   let goalty = get_goalty status goal in
 504   let status, what = disambiguate status (ctx_of goalty) what `XTInd in
 505   let status, ty_what = typeof status (ctx_of what) what in
 506   let _status, (r,consno,lefts,rights,cl) = analyse_indty status ty_what in
 507   let leftno = List.length lefts in
 508   let rightno = List.length rights in
 509   indtyref := Some {
 510     rightno = rightno; leftno = leftno; consno = consno; reference = r;
 511     cl = cl;
 512   };
 513   exec id_tac orig_status goal)
 514 ;;
 515
 516 let sort_of_goal_tac sortref = distribute_tac (fun status goal ->
 517   let goalty = get_goalty status goal in
 518   let status,sort = typeof status (ctx_of goalty) goalty in
 519   let status, sort = fix_sorts status sort in
 520   let ctx = ctx_of goalty in
 521   let status, sort = whd status (ctx_of sort) sort in
 522   let status, sort = term_of_cic_term status sort ctx in
 523    sortref := sort;
 524    status)
 525 ;;
 526
 527 let pp_ref reference =
 528   let NReference.Ref (uri,spec) = reference in
 529   let nstring = NUri.string_of_uri uri in
 530   (*"Shareno: " ^ (string_of_int nuri) ^*) "Uri: " ^ nstring ^
 531   (match spec with
 532     | NReference.Decl -> "Decl"
 533     | NReference.Def n -> "Def " ^ (string_of_int n)
 534     | NReference.Fix (n1,n2,n3) -> "Fix " ^ (string_of_int n1) ^ " " ^ (string_of_int n2) ^ " " ^ (string_of_int n3)(* fixno, recparamno, height *)
 535     | NReference.CoFix n -> "CoFix " ^ (string_of_int n)
 536     | NReference.Ind (b,n1,n2) -> "Ind " ^ (string_of_bool b) ^ " " ^ (string_of_int n1) ^ " " ^ (string_of_int n2)(* inductive, indtyno, leftno *)
 537     | NReference.Con (n1,n2,n3) ->  "Con " ^ (string_of_int n1) ^ " " ^ (string_of_int n2) ^ " " ^ (string_of_int n3)(* indtyno, constrno, leftno  *)
 538   ) ;;
 539
 540 let pp_cl cl =
 541   let rec pp_aux acc =
 542     match acc with
 543     | [] -> ""
 544     | (_,consname,_) :: tl -> consname ^ ", " ^ pp_aux tl
 545   in
 546     pp_aux cl
 547 ;;
 548
 549 let pp_indtyinfo ity = "leftno: " ^ (string_of_int ity.leftno) ^ ", consno: " ^ (string_of_int
 550                                                                                    ity.consno) ^ ", rightno: " ^
 551                        (string_of_int ity.rightno) ^ ", reference: " ^ (pp_ref ity.reference) ^ ",
 552                        cl: " ^ (pp_cl ity.cl);;
 553
 554 let elim_tac ~what:(txt,len,what) ~where =
 555   let what = txt, len, Ast.Appl [what; Ast.Implicit `Vector] in
 556   let indtyinfo = ref None in
 557   let sort = ref (NCic.Rel 1) in
 558   atomic_tac (block_tac [
 559     analyze_indty_tac ~what indtyinfo;
 560     (fun s -> select_tac
 561       ~where ~job:(`Substexpand ((HExtlib.unopt !indtyinfo).rightno+1)) true s);
 562     sort_of_goal_tac sort;
 563     (fun status ->
 564      let ity = HExtlib.unopt !indtyinfo in
 565      let NReference.Ref (uri, _) = ity.reference in
 566      let name =
 567        NUri.name_of_uri uri ^ "_" ^
 568         snd (NCicElim.ast_of_sort
 569           (match !sort with NCic.Sort x -> x | _ -> assert false))
 570      in
 571      let eliminator =
 572        let _,_,w = what in
 573        Ast.Appl [ Ast.Ident (name,None) ; Ast.Implicit `Vector ; w ]
 574      in
 575      exact_tac ("",0,eliminator) status) ])
 576 ;;
 577
 578 let rewrite_tac ~dir ~what:(_,_,what) ~where status =
 579  let sortref = ref (NCic.Rel 1) in
 580  let status = sort_of_goal_tac sortref status in
 581  let suffix = "_" ^ snd (NCicElim.ast_of_sort
 582    (match !sortref with NCic.Sort x -> x | _ -> assert false))
 583  in
 584  let name =
 585   match dir with
 586      `LeftToRight -> "eq" ^ suffix ^ "_r"
 587    | `RightToLeft -> "eq" ^ suffix
 588  in
 589  let what = Ast.Appl [what; Ast.Implicit `Vector] in
 590   block_tac
 591    [ select_tac ~where ~job:(`Substexpand 2) true;
 592      exact_tac
 593       ("",0,
 594        Ast.Appl(Ast.Ident(name,None)::HExtlib.mk_list (Ast.Implicit `JustOne) 5@
 595         [what]))] status
 596 ;;
 597
 598 let intro_tac name =
 599  block_tac
 600   [ exact_tac
 601      ("",0,(Ast.Binder (`Lambda,
 602       (Ast.Ident (name,None),None),Ast.Implicit `JustOne)));
 603     if name = "_" then clear_tac [name] else id_tac ]
 604 ;;
 605
 606 let name_counter = ref 0;;
 607 let intros_tac ?names_ref names s =
 608   let names_ref, prefix =
 609     match names_ref with | None -> ref [], "__" | Some r -> r, "H"
 610   in
 611   if names = [] then
 612    repeat_tac
 613      (fun s ->
 614         incr name_counter;
 615         (* TODO: generate better names *)
 616         let name = prefix ^ string_of_int !name_counter in
 617         let s = intro_tac name s in
 618         names_ref := !names_ref @ [name];
 619         s)
 620      s
 621    else
 622      block_tac (List.map intro_tac names) s
 623 ;;
 624
 625 let cases ~what status goal =
 626  let gty = get_goalty status goal in
 627  let status, what = disambiguate status (ctx_of gty) what `XTInd in
 628  let status, ty = typeof status (ctx_of what) what in
 629  let status, (ref, consno, _, _,_) = analyse_indty status ty in
 630  let status, what = term_of_cic_term status what (ctx_of gty) in
 631  let t =
 632   NCic.Match (ref,NCic.Implicit `Term, what,
 633     HExtlib.mk_list (NCic.Implicit `Term) consno)
 634  in
 635  instantiate status goal (mk_cic_term (ctx_of gty) t)
 636 ;;
 637
 638 let cases_tac ~what:(txt,len,what) ~where =
 639   let what = txt, len, Ast.Appl [what; Ast.Implicit `Vector] in
 640   let indtyinfo = ref None in
 641   atomic_tac
 642    (block_tac [
 643       analyze_indty_tac ~what indtyinfo;
 644       (fun s -> select_tac
 645        ~where ~job:(`Substexpand ((HExtlib.unopt !indtyinfo).rightno+1))true s);
 646       distribute_tac (cases ~what) ])
 647 ;;
 648
 649 let case1_tac name =
 650  let name = if name = "_" then "_clearme" else name in
 651  block_tac [ intro_tac name;
 652              cases_tac
 653               ~where:("",0,(None,[],None))
 654               ~what:("",0,Ast.Ident (name,None));
 655              if name = "_clearme" then clear_tac ["_clearme"] else id_tac ]
 656 ;;
 657
 658 let constructor_tac ?(num=1) ~args = distribute_tac (fun status goal ->
 659   let gty = get_goalty status goal in
 660   let status, (r,consno,_,_,_) = analyse_indty status gty in
 661   if num < 1 || num > consno then fail (lazy "Non existant constructor");
 662   let ref = NReference.mk_constructor num r in
 663   let t =
 664     if args = [] then Ast.NRef ref else
 665     Ast.Appl (HExtlib.list_concat ~sep:[Ast.Implicit `Vector]
 666       ([Ast.NRef ref] :: List.map (fun _,_,x -> [x]) args))
 667   in
 668   exec (apply_tac ("",0,t)) status goal)
 669 ;;
 670
 671 let assert0_tac (hyps,concl) = distribute_tac (fun status goal ->
 672  let gty = get_goalty status goal in
 673  let eq status ctx t1 t2 =
 674   let status,t1 = disambiguate status ctx t1 `XTSort in
 675   let status,t1 = apply_subst status ctx t1 in
 676   let status,t1 = term_of_cic_term status t1 ctx in
 677   let t2 = mk_cic_term ctx t2 in
 678   let status,t2 = apply_subst status ctx t2 in
 679   let status,t2 = term_of_cic_term status t2 ctx in
 680   prerr_endline ("COMPARING: " ^ status#ppterm ~subst:[] ~metasenv:[] ~context:ctx t1 ^ " vs " ^ status#ppterm ~subst:[] ~metasenv:[] ~context:ctx t2);
 681   assert (t1=t2);
 682   status
 683  in
 684  let status,gty' = term_of_cic_term status gty (ctx_of gty) in
 685  let status = eq status (ctx_of gty) concl gty' in
 686  let status,_ =
 687   List.fold_right2
 688    (fun (id1,e1) ((id2,e2) as item) (status,ctx) ->
 689      assert (id1=id2 || (prerr_endline (id1 ^ " vs " ^ id2); false));
 690      match e1,e2 with
 691         `Decl t1, NCic.Decl t2 ->
 692           let status = eq status ctx t1 t2 in
 693           status,item::ctx
 694       | `Def (b1,t1), NCic.Def (b2,t2) ->
 695           let status = eq status ctx t1 t2 in
 696           let status = eq status ctx b1 b2 in
 697           status,item::ctx
 698       | _ -> assert false
 699    ) hyps (ctx_of gty) (status,[])
 700  in
 701   exec id_tac status goal)
 702 ;;
 703
 704 let assert_tac seqs status =
 705  match status#stack with
 706   | [] -> assert false
 707   | (g,_,_,_) :: _s ->
 708      assert (List.length g = List.length seqs);
 709      (match seqs with
 710          [] -> id_tac
 711        | [seq] -> assert0_tac seq
 712        | _ ->
 713          block_tac
 714           ((branch_tac ~force:false)::
 715           HExtlib.list_concat ~sep:[shift_tac]
 716             (List.map (fun seq -> [assert0_tac seq]) seqs)@
 717           [merge_tac])
 718      ) status
 719 ;;
 720
 721 let inversion_tac ~what:(txt,len,what) ~where =
 722   let what = txt, len, Ast.Appl [what; Ast.Implicit `Vector] in
 723   let indtyinfo = ref None in
 724   let sort = ref (NCic.Rel 1) in
 725   atomic_tac (block_tac [
 726     analyze_indty_tac ~what indtyinfo;
 727     (fun s -> select_tac
 728       ~where ~job:(`Substexpand ((HExtlib.unopt !indtyinfo).rightno+1)) true s);
 729     sort_of_goal_tac sort;
 730     (fun status ->
 731      let ity = HExtlib.unopt !indtyinfo in
 732      let NReference.Ref (uri, _) = ity.reference in
 733      let name =
 734        NUri.name_of_uri uri ^ "_inv_" ^
 735         snd (NCicElim.ast_of_sort
 736           (match !sort with NCic.Sort x -> x | _ -> assert false))
 737      in
 738      let eliminator =
 739        let _,_,w = what in
 740        Ast.Appl [ Ast.Ident (name,None) ; Ast.Implicit `Vector ; w ; Ast.Implicit `Vector]
 741      in
 742      exact_tac ("",0,eliminator) status) ])
 743 ;;