A cleaned version of auto_tac_new.

diff --git a/helm/ocaml/tactics/autoTactic.ml b/helm/ocaml/tactics/autoTactic.ml
index 7f6be1d9bb2480be5a1b1c5e6231770d368472e0..3d4fc7126bcc781d041c0f6acf194696cf266b4a 100644 (file)
--- a/helm/ocaml/tactics/autoTactic.ml
+++ b/helm/ocaml/tactics/autoTactic.ml
@@ -23,7 +23,9 @@
  * http://cs.unibo.it/helm/.
  *)
 
-let debug_print = fun _ -> ()
+ let debug_print = prerr_endline 
+
+(* let debug_print = fun _ -> () *)
 
 (* Da rimuovere, solo per debug*)
 let print_context ctx =
@@ -220,63 +222,6 @@ let search_theorems_in_context status =
     []
 ;;     
 
-(** splits a list of goals in three groups: closed propositional goals,
-  open propositional goals and non proposotional goals *)
-
-let split proof l =
-  let _,metasenv,_,_ = proof in
-  List.fold_left
-    (fun (c,o,z,n) g ->
-       try
-        let (_, ey, ty) = CicUtil.lookup_meta g metasenv in
-        let ty_sort,u = 
-          CicTypeChecker.type_of_aux' metasenv ey ty CicUniv.empty_ugraph in
-        let b,_ = 
-          CicReduction.are_convertible ey (Cic.Sort Cic.Prop) ty_sort u in
-          if b then
-            (if CicUtil.is_meta_closed ty then
-               (g::c,o,z,n)
-             else
-               (c,g::o,z,n))
-          else (c,o,z,g::n)
-       with
-          CicUtil.Meta_not_found _ -> (c,o,g::z,n)
-    )
-    ([],[],[],[]) l
-;;
-       
-let my_weight dbd sign proof g =
-  let res = 
-    search_theorems_in_context (proof,g) in
-   (* @
-    (List.map snd (MetadataQuery.experimental_hint 
-      ~dbd ~facts:false ?signature:sign (proof,g))) in *)
-  List.fold_left
-    (fun n (_,(_,l)) -> n+(List.length l)+1)
-    0 res
-;;
-
-let  add_weight dbd sign proof =
-  List.map (function g -> (g,my_weight dbd sign proof g)) 
-
-;;
-
-
-(* let reorder_goals dbd sign proof goals = 
-  List.rev goals *) 
-
-(* let reorder_goals dbd sign proof goals =
-  let (c,o,z,n) = split proof goals
-  in c@o@n@z *)
-
-let reorder_goals dbd sign proof goals =
-  let (c,o,z,n) = split proof goals in
-    match o with
-       [] -> c@n@z
-      | [g] ->c@[g]@n@z
-      | l -> 
-         let l' = add_weight dbd sign proof l in
-         c@(List.map fst (List.sort (fun (_,x) (_,y) -> x - y) l'))@n@z
 
 let compare_goals proof goal1 goal2 =
   let _,metasenv,_,_ = proof in
@@ -355,11 +300,9 @@ let rec auto_single dbd proof goal ey ty depth width sign already_seen_goals
            [] (* the empty list means no choices, i.e. failure *)
        | No _ 
        | NotYetInspected ->
-             (*
              debug_print ("CURRENT GOAL = " ^ (CicPp.ppterm ty));
              debug_print ("CURRENT PROOF = " ^ (CicPp.ppterm p));
              debug_print ("CURRENT HYP = " ^ (fst (print_context ey)));
-             *)
            let sign, new_sign =
              if is_meta_closed then
                None, Some (MetadataConstraints.signature_of ty)
@@ -368,14 +311,13 @@ let rec auto_single dbd proof goal ey ty depth width sign already_seen_goals
              new_search_theorems 
                search_theorems_in_context dbd
                proof goal (depth-1) new_sign in
-           let global_choices = [] in
-(*
+           let global_choices =
              new_search_theorems 
                (fun status -> 
                   List.map snd
                   (MetadataQuery.experimental_hint 
                      ~dbd ~facts:facts ?signature:sign status))
-               dbd proof goal (depth-1) new_sign in *)
+               dbd proof goal (depth-1) new_sign in 
            let all_choices =
              local_choices@global_choices in
            let sorted_choices = 
@@ -444,61 +386,30 @@ and auto_new_aux dbd width already_seen_goals = function
   | (subst,(proof, (goal,0)::_, _))::tl -> 
       auto_new dbd width already_seen_goals tl 
   | (subst,(proof, goals, _))::tl when 
-      (List.length goals) > width+1 -> 
+      (List.length goals) > width -> 
       auto_new dbd width already_seen_goals tl 
   | (subst,(proof, (goal,depth)::gtl, sign))::tl -> 
-      let maxdepthgoals,othergoals =
-       let rec aux acc =
-         function
-             (g,d)::l when d=depth -> aux (g::acc) l
-           |l -> (acc,l) in
-         aux [goal] gtl in
       let _,metasenv,p,_ = proof in
-      let len1 = List.length maxdepthgoals in
-      let maxdepthgoals = reorder_goals dbd sign proof maxdepthgoals in
-      let len2 = List.length maxdepthgoals in
-       match maxdepthgoals with
-         [] -> debug_print 
-           ("caso sospetto " ^ (string_of_int (List.length othergoals)) ^ " " ^ string_of_int depth);
-           auto_new dbd 
-             width already_seen_goals((subst,(proof, othergoals, sign))::tl) 
-       | goal::tgs -> 
-           let  gtl = (List.map (fun x->(x,depth)) tgs)@othergoals in
-             begin
-      let meta_inf =
-       try
-         let (_, ey ,ty) =
-           CicUtil.lookup_meta goal metasenv in
-           Some (ey,ty)
-       with _ -> None 
-      in
-       match meta_inf with 
-         | Some (ey,ty) ->
-            begin
-           match (auto_single dbd proof goal ey ty depth
-       (width - (List.length gtl) - (len1-len2)) sign already_seen_goals) 
-               with
-                   [] -> auto_new dbd width already_seen_goals tl
-                 | (local_subst,(proof,[],sign))::tl1 -> 
-                     let new_subst f t = f (subst t) in
-                     let is_meta_closed = CicUtil.is_meta_closed ty in
-                     let all_choices =
-                       if is_meta_closed then 
-                         (new_subst local_subst,(proof,gtl,sign))::tl
-                       else
-                         let tl2 = 
-                           (List.map 
-                              (function (f,(p,l,s)) -> (new_subst f,(p,l@gtl,s))) tl1)
-                         in                     
-                           (new_subst local_subst,(proof,gtl,sign))::tl2@tl in
-                       auto_new dbd width already_seen_goals all_choices 
-                 | _ -> assert false
-           end
-         | None -> debug_print "caso none";
-             auto_new 
-               dbd width already_seen_goals ((subst,(proof, gtl, sign))::tl)
-             end
-;; 
+      let (_, ey ,ty) = CicUtil.lookup_meta goal metasenv in
+      match (auto_single dbd proof goal ey ty depth
+       (width - (List.length gtl)) sign already_seen_goals) 
+      with
+         [] -> auto_new dbd width already_seen_goals tl
+       | (local_subst,(proof,[],sign))::tl1 -> 
+           let new_subst f t = f (subst t) in
+           let is_meta_closed = CicUtil.is_meta_closed ty in
+           let all_choices =
+             if is_meta_closed then 
+               (new_subst local_subst,(proof,gtl,sign))::tl
+             else
+               let tl2 = 
+                 (List.map 
+                    (function (f,(p,l,s)) -> (new_subst f,(p,l@gtl,s))) tl1)
+               in                       
+                 (new_subst local_subst,(proof,gtl,sign))::tl2@tl in
+             auto_new dbd width already_seen_goals all_choices 
+       | _ -> assert false
+ ;; 
 
 let default_depth = 5
 let default_width = 3