X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FautoTactic.ml;h=6afef50e050f2fb69a5f4e7ad0b9292f7cea9dd1;hb=46f19eadce5f3a11c0ae26934fd8d1b597906416;hp=ce700f2de5091c9f7532570453cc10401d4c62d6;hpb=e09713d333183e929f108ff8bb8fbe2a25bfcac7;p=helm.git

diff --git a/helm/ocaml/tactics/autoTactic.ml b/helm/ocaml/tactics/autoTactic.ml
index ce700f2de..6afef50e0 100644
--- a/helm/ocaml/tactics/autoTactic.ml
+++ b/helm/ocaml/tactics/autoTactic.ml
@@ -23,6 +23,8 @@
  * http://cs.unibo.it/helm/.
  *)
 
+let debug_print = fun _ -> ()
+
 (* Da rimuovere, solo per debug*)
 let print_context ctx =
     let print_name =
@@ -75,7 +77,8 @@ let search_theorems_in_context status =
     []
 ;;     
 
-let depth = 6;;
+let depth = 5;;
+let width = 3;;
 
 let new_search_theorems f proof goal depth gtl sign =
   let choices = f (proof,goal)
@@ -104,10 +107,10 @@ let rec auto dbd = function
       match meta_inf with
 	  Some (ey, ty) ->
             (* the goal is still there *)
-            (* 
-	    prerr_endline ("CURRENT GOAL = " ^ (CicPp.ppterm ty));
-	    prerr_endline ("CURRENT PROOF = " ^ (CicPp.ppterm p));
-	    prerr_endline ("CURRENT HYP = " ^ (fst (print_context ey)));
+            (*
+	    debug_print ("CURRENT GOAL = " ^ (CicPp.ppterm ty));
+	    debug_print ("CURRENT PROOF = " ^ (CicPp.ppterm p));
+	    debug_print ("CURRENT HYP = " ^ (fst (print_context ey)));
             *)
             (* if the goal contains metavariables we use the input
                signature for at_most constraints *)
@@ -153,14 +156,14 @@ let rec auto dbd = function
 ;; 
 
 
-let auto_tac  ~(dbd:Mysql.dbd) =
+let auto_tac  ?num ~(dbd:Mysql.dbd) =
   let auto_tac dbh (proof,goal) =
-  prerr_endline "Entro in Auto";
+  debug_print "Entro in Auto";
   match (auto dbd [(proof, [(goal,depth)],None)]) with
-      [] ->  prerr_endline("Auto failed");
+      [] ->  debug_print("Auto failed");
 	raise (ProofEngineTypes.Fail "No Applicable theorem")
     | (proof,[],_)::_ ->  
-	prerr_endline "AUTO_TAC HA FINITO";
+	debug_print "AUTO_TAC HA FINITO";
 	(proof,[])
     | _ -> assert false
   in
@@ -174,7 +177,8 @@ let auto_tac  ~(dbd:Mysql.dbd) =
    goals. We assume that the context is invariant for application. 
    To this aim, it is essential to sall hint_verbose, that in turns calls
    apply_verbose. *)
-   
+
+
 
 type exitus = 
     No of int 
@@ -196,8 +200,14 @@ let search_theorems_in_context status =
       [] -> []
     | hd::tl ->
 	let res =
-	  try 
-            Some (PT.apply_tac_verbose ~term:(C.Rel n) status ) 
+	  try
+	    let (subst,(proof, goal_list)) =
+              PT.apply_tac_verbose ~term:(C.Rel n) status  in
+            (* 
+	    let goal_list =
+              List.stable_sort (compare_goal_list proof) goal_list in 
+            *)
+	    Some (subst,(proof, goal_list))
 	  with 
 	    PET.Fail _ -> None in
 	(match res with
@@ -210,133 +220,299 @@ let search_theorems_in_context status =
     []
 ;;     
 
-let new_search_theorems f proof goal depth subst sign =
+(** 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
+  let (_, ey1, ty1) = CicUtil.lookup_meta goal1 metasenv in
+  let (_, ey2, ty2) =  CicUtil.lookup_meta goal2 metasenv in
+  let ty_sort1,_ = CicTypeChecker.type_of_aux' metasenv ey1 ty1 
+		     CicUniv.empty_ugraph in
+  let ty_sort2,_ = CicTypeChecker.type_of_aux' metasenv ey2 ty2 
+		     CicUniv.empty_ugraph in
+  let prop1 =
+    let b,_ = CicReduction.are_convertible ey1 (Cic.Sort Cic.Prop) ty_sort1 
+		CicUniv.empty_ugraph in
+      if b then 0 else 1
+  in
+  let prop2 =
+    let b,_ = CicReduction.are_convertible ey2 (Cic.Sort Cic.Prop) ty_sort2 
+		CicUniv.empty_ugraph in
+      if b then 0 else 1
+  in
+  prop1 - prop2
+
+
+let new_search_theorems f dbd proof goal depth sign =
   let choices = f (proof,goal)
   in 
   List.map 
-    (function (local_subst,(proof, goallist)) ->
-       let new_subst t= local_subst (subst t) in
-       (new_subst,(proof,(List.map (function g -> (g,depth)) goallist), sign)))
+    (function (subst,(proof, goallist)) ->
+       (* let goallist = reorder_goals dbd sign proof goallist in *)
+        let goallist = List.sort (compare_goals proof) goallist in 
+       (subst,(proof,(List.map (function g -> (g,depth)) goallist), sign)))
     choices 
 ;;
 
 exception NoOtherChoices;;
-let rec auto_new dbd = function
-    [] -> []
-  | (subst,(proof, [], sign))::tl -> (subst,(proof, [], sign))::tl
-  | (subst,(proof, (goal,0)::_, _))::tl -> auto_new dbd tl
-  | (subst,(proof, (((goal,depth)::gtl) as allg), sign))::tl ->
-      let facts = (depth = 1) in  
-      let name,metasenv,p,statement = proof in
-      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) ->
-            (* first of all we check if the goal has been already
-               inspected *)
-	    let exitus =
-	      try Hashtbl.find inspected_goals ty
-	      with Not_found -> NotYetInspected in
-            let is_meta_closed = CicUtil.is_meta_closed ty in
-	    begin
-            match exitus with
-		Yes (bo,_) ->
-                  (*
-                  prerr_endline "ALREADY PROVED!!!!!!!!!!!!!!!!!!!!!!!!!!!!";
-		  prerr_endline (CicPp.ppterm ty);
-                  *)
-                  let subst_in =
-                    (* if we just apply the subtitution, the type 
-                       is irrelevant: we may use Implicit, since it will 
-                       be dropped *)
-		    CicMetaSubst.apply_subst 
-	              [(goal,(ey, bo, Cic.Implicit None))] in
-		  let (proof,_) = 
-		    ProofEngineHelpers.subst_meta_and_metasenv_in_proof 
-		      proof goal subst_in metasenv in
-                  let new_subst t = (subst_in (subst t)) in
-		  auto_new dbd ((new_subst,(proof,gtl,sign))::tl)
-              | No d when (d >= depth) -> 
-                  (*
-		  prerr_endline "PRUNED!!!!!!!!!!!!!!!!!!!!!!!!!!!!";
-                  *)
-		  auto_new dbd tl
-               
-	      | No _ 
-	      | NotYetInspected -> 
-                  (*
-		  prerr_endline ("CURRENT GOAL = " ^ (CicPp.ppterm ty));
-		  prerr_endline ("CURRENT PROOF = " ^ (CicPp.ppterm p));
-		  prerr_endline ("CURRENT HYP = " ^ (fst (print_context ey)));
-                  *)
-		  let sign, new_sign =
-		    if is_meta_closed then
-		      None, Some (MetadataConstraints.signature_of ty)
-		    else sign,sign in (* maybe the union ? *)
-		  let local_choices =
-		    new_search_theorems 
-		      search_theorems_in_context 
-		      proof goal (depth-1) subst new_sign in
-		  let global_choices =
-		    new_search_theorems 
-		      (fun status -> 
-			 List.map snd 
-			 (MetadataQuery.experimental_hint 
-			    ~dbd ~facts:facts ?signature:sign status))
-		      proof goal (depth-1) subst new_sign in
-		  let all_choices =
-		    local_choices@global_choices in
-		  (match (auto_new dbd all_choices) 
-		   with
-		       [] -> 
-			 (* no proof has been found; we update the
-			    hastable *)
-			 Hashtbl.add inspected_goals ty (No depth);
-			 auto_new dbd tl
-		     | (new_subst,(proof,[],_))::tl1 -> 
-			 (* a proof for goal has been found:
-			    in order to get the proof we apply subst to
-			    Meta[goal] *)
-			 if is_meta_closed  then
-			   begin 
-			     let irl = 
-			       CicMkImplicit.identity_relocation_list_for_metavariable ey in
-			     let meta_proof = 
-			       new_subst (Cic.Meta(goal,irl)) in
-			       Hashtbl.add inspected_goals 
-				 ty (Yes (meta_proof,depth));
+
+let is_in_metasenv goal metasenv =
+  try
+    let (_, ey ,ty) =
+      CicUtil.lookup_meta goal metasenv in
+      true
+  with _ -> false 
+
+let rec auto_single dbd proof goal ey ty depth width sign already_seen_goals
+  =
+  if depth = 0 then [] else
+  if List.mem ty already_seen_goals then [] else
+  let already_seen_goals = ty::already_seen_goals in
+  let facts = (depth = 1) in  
+  let _,metasenv,p,_ = proof in
+    (* first of all we check if the goal has been already
+       inspected *)
+  assert (is_in_metasenv goal metasenv);
+  let exitus =
+    try Hashtbl.find inspected_goals ty
+    with Not_found -> NotYetInspected in
+  let is_meta_closed = CicUtil.is_meta_closed ty in
+    begin
+      match exitus with
+	  Yes (bo,_) ->
+            (*
+              debug_print "ALREADY PROVED!!!!!!!!!!!!!!!!!!!!!!!!!!!!";
+	      debug_print (CicPp.ppterm ty);
+            *)
+            let subst_in =
+              (* if we just apply the subtitution, the type 
+                 is irrelevant: we may use Implicit, since it will 
+                 be dropped *)
+	      CicMetaSubst.apply_subst 
+	        [(goal,(ey, bo, Cic.Implicit None))] in
+	    let (proof,_) = 
+	      ProofEngineHelpers.subst_meta_and_metasenv_in_proof 
+		proof goal subst_in metasenv in
+	      [(subst_in,(proof,[],sign))]
+        | No d when (d >= depth) -> 
+	    (* debug_print "PRUNED!!!!!!!!!!!!!!!!!!!!!!!!!!!!"; *)
+	    [] (* 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)
+	      else sign,sign in (* maybe the union ? *)
+	    let local_choices =
+	      new_search_theorems 
+		search_theorems_in_context dbd
+		proof goal (depth-1) new_sign in
+	    let global_choices = [] in
+(*
+	      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 *)
+	    let all_choices =
+	      local_choices@global_choices in
+	    let sorted_choices = 
+	      List.stable_sort
+		(fun (_, (_, goals1, _)) (_, (_, goals2, _)) ->
+		   Pervasives.compare 
+		   (List.length goals1) (List.length goals2))
+		all_choices in 
+	      (match (auto_new dbd width already_seen_goals sorted_choices) 
+	       with
+		   [] -> 
+		     (* no proof has been found; we update the
+			hastable *)
+		     (* if is_meta_closed then *)
+		       Hashtbl.add inspected_goals ty (No depth);
+		     []
+		 | (subst,(proof,[],sign))::tl1 -> 
+		     (* a proof for goal has been found:
+			in order to get the proof we apply subst to
+			Meta[goal] *)
+		     if is_meta_closed  then
+		       begin 
+			 let irl = 
+			   CicMkImplicit.identity_relocation_list_for_metavariable ey in
+			 let meta_proof = 
+			   subst (Cic.Meta(goal,irl)) in
+			   Hashtbl.add inspected_goals 
+			     ty (Yes (meta_proof,depth));
+(*
+			   begin
+			     let cty,_ = 
+			       CicTypeChecker.type_of_aux' metasenv ey meta_proof CicUniv.empty_ugraph
+			     in
+			       if not (cty = ty) then
+				 begin
+				   debug_print ("ty =  "^CicPp.ppterm ty);
+				   debug_print ("cty =  "^CicPp.ppterm cty);
+				   assert false
+				 end
+				   Hashtbl.add inspected_goals 
+				   ty (Yes (meta_proof,depth));
 			   end;
-			 let all_choices =
-			   let gtl' = List.map fst gtl in
-			     if (gtl = [] || is_meta_closed) then 
-			       (new_subst,(proof,gtl,sign))::tl
-			     else
-			       let tl2 = 
-				 (List.map 
-				    (function (f,(p,l,s)) 
-					 -> (f,(p,l@gtl,s))) tl1)
-			       in			 
-			       (new_subst,(proof,gtl,sign))::tl2@tl in
-		       auto_new dbd all_choices
+*)
+		       end;
+		     (subst,(proof,[],sign))::tl1
 		 | _ -> assert false)
+    end
+      
+and auto_new dbd width already_seen_goals = function
+    [] -> []
+  | (subst,(proof, goals, sign))::tl ->
+      let _,metasenv,_,_ = proof in
+      let is_in_metasenv (goal, _) =
+	try
+	  let (_, ey ,ty) =
+	    CicUtil.lookup_meta goal metasenv in
+	    true
+	with _ -> false in
+      let goals'= List.filter is_in_metasenv goals in
+	auto_new_aux dbd width already_seen_goals 
+	  ((subst,(proof, goals', sign))::tl)
+
+and auto_new_aux dbd width already_seen_goals = function
+  [] -> []
+  | (subst,(proof, [], sign))::tl -> (subst,(proof, [], sign))::tl
+  | (subst,(proof, (goal,0)::_, _))::tl -> 
+      auto_new dbd width already_seen_goals tl 
+  | (subst,(proof, goals, _))::tl when 
+      (List.length goals) > width+1 -> 
+      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 -> auto_new dbd ((subst,(proof,gtl,sign))::tl) 
+	  | None -> debug_print "caso none";
+	      auto_new 
+		dbd width already_seen_goals ((subst,(proof, gtl, sign))::tl)
+	      end
 ;; 
 
 
 let auto_tac_new  ~(dbd:Mysql.dbd) =
   let auto_tac dbd (proof,goal) =
   Hashtbl.clear inspected_goals;
-  prerr_endline "Entro in Auto";
+  debug_print "Entro in Auto";
   let id t = t in
-  match (auto_new dbd [id,(proof, [(goal,depth)],None)]) with
-      [] ->  prerr_endline("Auto failed");
+  match (auto_new dbd width [] [id,(proof, [(goal,depth)],None)]) with
+      [] ->  debug_print("Auto failed");
 	raise (ProofEngineTypes.Fail "No Applicable theorem")
     | (_,(proof,[],_))::_ ->  
-	prerr_endline "AUTO_TAC HA FINITO";
+	debug_print "AUTO_TAC HA FINITO";
+	let _,_,p,_ = proof in
+	debug_print (CicPp.ppterm p);
 	(proof,[])
     | _ -> assert false
   in