Release 0.5.9.

[helm.git] / helm / software / components / ng_tactics / nTactics.ml

diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml
index 93d8c965c41e1b6181cf29d7f2808e20265992bc..10fa168d492517123eff7b4b18861cb9827cfa47 100644 (file)
--- a/helm/software/components/ng_tactics/nTactics.ml
+++ b/helm/software/components/ng_tactics/nTactics.ml
@@ -22,7 +22,7 @@ module Ast = CicNotationPt
 
 let id_tac status = status ;;
 let print_tac print_status message status = 
-  if print_status then pp_tac_status status;
+  if print_status then pp_status status;
   prerr_endline message; 
   status
 ;;
@@ -46,14 +46,13 @@ let dot_tac status =
    status#set_stack gstatus
 ;;
 
-let branch_tac ?(force=false) status =
+let branch_tac status =
   let gstatus = 
     match status#stack with
     | [] -> assert false
     | (g, t, k, tag) :: s ->
           match init_pos g with (* TODO *)
-          | [] -> fail (lazy "empty goals")
-         | [_] when (not force) -> fail (lazy "too few goals to branch")
+          | [] | [ _ ] -> fail (lazy "too few goals to branch")
           | loc :: loc_tl ->
                ([ loc ], [], [], `BranchTag) :: (loc_tl, t, k, tag) :: s
   in
@@ -261,13 +260,10 @@ let repeat_tac t s =
 
 
 let try_tac tac status =
- let try_tac status =
   try
     tac status
   with NTacStatus.Error _ ->
     status
- in
-  atomic_tac try_tac status
 ;;
 
 let first_tac tacl status =
@@ -374,7 +370,7 @@ let select0_tac ~where:(wanted,hyps,where) ~job  =
    let status, instance = 
      mk_meta status newgoalctx (`Decl newgoalty) `IsTerm
    in
-   instantiate ~refine:false status goal instance)
+   instantiate status goal instance)
 ;;
 
 let select_tac ~where ~job move_down_hyps = 
@@ -423,12 +419,12 @@ let generalize_tac ~where =
 ;;
 
 let cut_tac t = 
- atomic_tac (block_tac [ 
+ block_tac [ 
   exact_tac ("",0, Ast.Appl [Ast.Implicit `JustOne; Ast.Implicit `JustOne]);
   branch_tac;
    pos_tac [3]; exact_tac t;
    shift_tac; pos_tac [2]; skip_tac;
-  merge_tac ])
+  merge_tac ]
 ;;
 
 let lapply_tac (s,n,t) = 
@@ -476,6 +472,8 @@ type indtyinfo = {
         rightno: int;
         leftno: int;
         consno: int;
+        lefts: NCic.term list;
+        rights: NCic.term list;
         reference: NReference.reference;
  }
 ;;
@@ -483,7 +481,7 @@ type indtyinfo = {
 let ref_of_indtyinfo iti = iti.reference;;
 
 let analyze_indty_tac ~what indtyref =
- distribute_tac (fun (status as orig_status) goal ->
+ distribute_tac (fun status goal ->
   let goalty = get_goalty status goal in
   let status, what = disambiguate status (ctx_of goalty) what None in
   let status, ty_what = typeof status (ctx_of what) what in 
@@ -491,9 +489,10 @@ let analyze_indty_tac ~what indtyref =
   let leftno = List.length lefts in
   let rightno = List.length rights in
   indtyref := Some { 
-    rightno = rightno; leftno = leftno; consno = consno; reference = r;
+    rightno = rightno; leftno = leftno; consno = consno;
+    lefts = lefts; rights = rights; reference = r;
   };
-  exec id_tac orig_status goal)
+  exec id_tac status goal)
 ;;
 
 let sort_of_goal_tac sortref = distribute_tac (fun status goal ->
@@ -540,9 +539,8 @@ let rewrite_tac ~dir ~what:(_,_,what) ~where status =
      `LeftToRight -> "eq" ^ suffix ^ "_r"
    | `RightToLeft -> "eq" ^ suffix
  in
- let what = Ast.Appl [what; Ast.Implicit `Vector] in
   block_tac
-   [ select_tac ~where ~job:(`Substexpand 2) true;
+   [ select_tac ~where ~job:(`Substexpand 1) true;
      exact_tac
       ("",0,
        Ast.Appl(Ast.Ident(name,None)::HExtlib.mk_list (Ast.Implicit `JustOne) 5@
@@ -557,25 +555,6 @@ let intro_tac name =
     if name = "_" then clear_tac [name] else id_tac ]
 ;;
 
-let name_counter = ref 0;;
-let intros_tac ?names_ref names s =
-  let names_ref, prefix = 
-    match names_ref with | None -> ref [], "__" | Some r -> r, "H" 
-  in
-  if names = [] then
-   repeat_tac 
-     (fun s ->
-        incr name_counter;
-        (* TODO: generate better names *)
-        let name = prefix ^ string_of_int !name_counter in
-        let s = intro_tac name s in 
-        names_ref := !names_ref @ [name];
-        s)
-     s
-   else
-     block_tac (List.map intro_tac names) s
-;;
-
 let cases ~what status goal =
  let gty = get_goalty status goal in
  let status, what = disambiguate status (ctx_of gty) what None in
@@ -665,33 +644,10 @@ let assert_tac seqs status =
        | [seq] -> assert0_tac seq
        | _ ->
          block_tac
-          ((branch_tac ~force:false)::
+          (branch_tac::
           HExtlib.list_concat ~sep:[shift_tac]
             (List.map (fun seq -> [assert0_tac seq]) seqs)@
           [merge_tac])
      ) status
 ;;
 
-let inversion_tac ~what:(txt,len,what) ~where = 
-  let what = txt, len, Ast.Appl [what; Ast.Implicit `Vector] in
-  let indtyinfo = ref None in
-  let sort = ref (NCic.Rel 1) in
-  atomic_tac (block_tac [
-    analyze_indty_tac ~what indtyinfo;    
-    (fun s -> select_tac 
-      ~where ~job:(`Substexpand ((HExtlib.unopt !indtyinfo).rightno+1)) true s);
-    sort_of_goal_tac sort;
-    (fun status ->
-     let ity = HExtlib.unopt !indtyinfo in
-     let NReference.Ref (uri, _) = ity.reference in
-     let name = 
-       NUri.name_of_uri uri ^ "_inv_" ^
-        snd (NCicElim.ast_of_sort 
-          (match !sort with NCic.Sort x -> x | _ -> assert false))
-     in
-     let eliminator = 
-       let _,_,w = what in
-       Ast.Appl [ Ast.Ident (name,None) ; Ast.Implicit `Vector ; w ]
-     in
-     exact_tac ("",0,eliminator) status) ]) 
-;;