Release 0.5.9.

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

diff --git a/helm/software/components/ng_tactics/nAuto.ml b/helm/software/components/ng_tactics/nAuto.ml
index 7a33d6266da45052fc2a16328d60f8dcbf5ce5b8..640128616719fdbeb76aa7eead5beed334e15e40 100644 (file)
--- a/helm/software/components/ng_tactics/nAuto.ml
+++ b/helm/software/components/ng_tactics/nAuto.ml
@@ -13,7 +13,7 @@
 
 open Printf
 
-let debug = ref true
+let debug = ref false
 let debug_print ?(depth=0) s = 
   if !debug then prerr_endline (String.make depth '\t'^Lazy.force s) else ()
 let debug_do f = if !debug then f () else ()
@@ -24,9 +24,6 @@ module Ast = CicNotationPt
 
 (* =================================== paramod =========================== *)
 let auto_paramod ~params:(l,_) status goal =
-  let l = match l with
-    | None -> raise (Error (lazy "no proof found",None))
-    | Some l -> l in
   let gty = get_goalty status goal in
   let n,h,metasenv,subst,o = status#obj in
   let status,t = term_of_cic_term status gty (ctx_of gty) in
@@ -44,7 +41,7 @@ let auto_paramod ~params:(l,_) status goal =
     NCicParamod.nparamod status metasenv subst (ctx_of gty) (NCic.Rel ~-1,t) l 
   with
   | [] -> raise (Error (lazy "no proof found",None))
-  | (pt, _, metasenv, subst)::_ -> 
+  | (pt, metasenv, subst)::_ -> 
       let status = status#set_obj (n,h,metasenv,subst,o) in
       instantiate status goal (mk_cic_term (ctx_of gty) pt)
 ;;
@@ -1502,7 +1499,7 @@ let auto_main flags signature (pos : 'a and_pos) cache =
                  status pos cache 
 
   and attack pos cache and_item =
-    (* show pos; uncomment to show the tree *)
+    show pos; (* uncomment to show the tree *)
     match and_item with
     | _, S _ -> assert false (* next would close the proof or give a D *) 
     | _, L _ -> assert false (* L is a final solution *)
@@ -1621,40 +1618,6 @@ let auto_tac ~params:(_univ,flags) status =
     up_to depth depth
 ;;
 
-let rec rm_assoc n = function
-  | [] -> assert false
-  | (x,i)::tl when n=x -> i,tl
-  | p::tl -> let i,tl = rm_assoc n tl in i,p::tl
-;;
-
-let merge canonicals elements n m =
-  let cn,canonicals = rm_assoc n canonicals in
-  let cm,canonicals = rm_assoc m canonicals in
-  let ln,elements = rm_assoc cn elements in
-  let lm,elements = rm_assoc cm elements in
-  let canonicals = 
-    (n,cm)::(m,cm)::List.map 
-      (fun (x,xc) as p  -> 
-        if xc = cn then (x,cm) else p) canonicals
-  in 
-  let elements = (cn,ln@lm)::elements 
-  in
-    canonicals,elements
-;;
-
-let clusters f l =
-  let canonicals = List.map (fun x -> (x,x)) l in
-  let elements = List.map (fun x -> (x,[x])) l in
-   List.fold_left 
-     (fun (canonicals,elements) x ->
-       let dep = f x in
-        List.fold_left 
-          (fun (canonicals,elements) d ->
-             merge canonicals elements d x) 
-          (canonicals,elements) dep)
-     (canonicals,elements) l
-;;
-
 let group_by_tac ~eq_predicate ~action:tactic status = 
  let goals = head_goals status#stack in
  if List.length goals < 2 then tactic status 
@@ -1678,7 +1641,7 @@ let group_by_tac ~eq_predicate ~action:tactic status =
     let l2 = HExtlib.list_mapi (fun x i -> x,i+1) l2 in
     List.map (fun x -> List.assoc x l2) l1
   in
-  NTactics.block_tac ([ NTactics.branch_tac ~force:false]
+  NTactics.block_tac ([ NTactics.branch_tac ]
     @
     HExtlib.list_concat ~sep:[NTactics.shift_tac]
       (List.map (fun gl-> [NTactics.pos_tac (pos_of gl goals); tactic]) classes)
@@ -1709,17 +1672,9 @@ let auto_tac ~params =
 ;;
 
 (* ========================= dispatching of auto/auto_paramod ============ *)
-let auto_tac ~params:(_,flags as params) ?trace_ref =
+let auto_tac ~params:(_,flags as params) =
   if List.mem_assoc "paramodulation" flags then 
-    auto_paramod_tac ~params 
-  else if List.mem_assoc "demod" flags then 
-    NnAuto.demod_tac ~params 
-  else if List.mem_assoc "paramod" flags then 
-    NnAuto.paramod_tac ~params 
-  else if List.mem_assoc "fast_paramod" flags then 
-    NnAuto.fast_eq_check_tac ~params  
-  else if List.mem_assoc "slir" flags then 
-    NnAuto.auto_tac ~params ?trace_ref
+    auto_paramod_tac ~params  
   else 
     auto_tac ~params
 ;;