X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Ftactics%2Fparamodulation%2Fsaturation.ml;h=445eccdbc2f217565c67b5f319cb2652c105066e;hb=33f9ff7f9693a77f194112291bd149e7c0d80e71;hp=6ab9f59e28206cdd47331ccd91bdf055d1fb038b;hpb=45d872c9c4af6cffd39fd9af490da09f9066d1c1;p=helm.git

diff --git a/components/tactics/paramodulation/saturation.ml b/components/tactics/paramodulation/saturation.ml
index 6ab9f59e2..445eccdbc 100644
--- a/components/tactics/paramodulation/saturation.ml
+++ b/components/tactics/paramodulation/saturation.ml
@@ -23,9 +23,9 @@
  * http://cs.unibo.it/helm/.
  *)
 
-(* $Id$ *)
+let _profiler = <:profiler<_profiler>>;;
 
-(* <:profiler<"saturation">> *)
+(* $Id$ *)
 
 open Inference;;
 open Utils;;
@@ -106,7 +106,7 @@ module OrderedEquality = struct
   let compare eq1 eq2 =
     match Equality.meta_convertibility_eq eq1 eq2 with
     | true -> 0
-    | false ->
+    | false -> 
         let w1, _, (ty,left, right, _), m1,_ = Equality.open_equality eq1 in
         let w2, _, (ty',left', right', _), m2,_ = Equality.open_equality eq2 in
         match Pervasives.compare w1 w2 with
@@ -342,8 +342,14 @@ let infer env current (active_list, active_table) =
     (ignore(Indexing.check_target c current "infer1");
      ignore(List.map (function current -> Indexing.check_target c current "infer2") active_list)); 
   let new_pos = 
-    let maxm, res =
-      Indexing.superposition_right !maxmeta env active_table current in
+      let maxm, copy_of_current = Equality.fix_metas !maxmeta current in
+        maxmeta := maxm;
+      let active_table =  Indexing.index active_table copy_of_current in
+      let _ = <:start<current contro active>> in
+      let maxm, res =
+        Indexing.superposition_right !maxmeta env active_table current 
+      in
+      let _ = <:stop<current contro active>> in
       if Utils.debug_metas then
         ignore(List.map 
                  (function current -> 
@@ -353,7 +359,8 @@ let infer env current (active_list, active_table) =
         | [] -> []
         | equality::tl ->
             let maxm, res =
-              Indexing.superposition_right !maxmeta env table equality in
+              Indexing.superposition_right ~subterms_only:true !maxmeta env table equality 
+            in
               maxmeta := maxm;
               if Utils.debug_metas then
                 ignore
@@ -363,16 +370,19 @@ let infer env current (active_list, active_table) =
               let pos = infer_positive table tl in
               res @ pos
       in
+(*
       let maxm, copy_of_current = Equality.fix_metas !maxmeta current in
         maxmeta := maxm;
+*)
       let curr_table = Indexing.index Indexing.empty current in
-      let pos = infer_positive curr_table (copy_of_current::active_list) 
-      in 
+      let _ = <:start<active contro current>> in
+      let pos = infer_positive curr_table ((*copy_of_current::*)active_list) in
+      let _ = <:stop<active contro current>> in
       if Utils.debug_metas then 
         ignore(List.map 
                  (function current -> 
                     Indexing.check_target c current "sup3") pos);
-        res @ pos
+      res @ pos
   in
   derived_clauses := !derived_clauses + (List.length new_pos);
   match !maximal_retained_equality with
@@ -389,8 +399,6 @@ let infer env current (active_list, active_table) =
 
 let check_for_deep_subsumption env active_table eq =
   let _,_,(eq_ty, left, right, order),metas,id = Equality.open_equality eq in
-  if id = 14242 then assert false;
-  
   let check_subsumed deep l r = 
     let eqtmp = 
       Equality.mk_tmp_equality(0,(eq_ty,l,r,Utils.Incomparable),metas)in
@@ -561,37 +569,28 @@ let forward_simplify_new env new_pos ?passive active =
         (fun current -> Indexing.check_target c current "forward new pos") 
       new_pos;)
     end;
-  let t1 = Unix.gettimeofday () in
-
   let active_list, active_table = active in
   let passive_table =
     match passive with
     | None -> None
     | Some ((_, _), pt) -> Some pt
   in
-  let t2 = Unix.gettimeofday () in
-  fs_time_info.build_all <- fs_time_info.build_all +. (t2 -. t1);
-  
   let demodulate sign table target =
     let newmeta, newtarget =
       Indexing.demodulation_equality !maxmeta env table sign target in
     maxmeta := newmeta;
     newtarget
   in
-  let t1 = Unix.gettimeofday () in
   (* we could also demodulate using passive. Currently we don't *)
   let new_pos =
     List.map (demodulate Positive active_table) new_pos 
   in
-  let t2 = Unix.gettimeofday () in
-  fs_time_info.demodulate <- fs_time_info.demodulate +. (t2 -. t1);
-
   let new_pos_set =
     List.fold_left
       (fun s e ->
          if not (Equality.is_identity env e) then
-           if EqualitySet.mem e s then s
-           else EqualitySet.add e s
+(*            if EqualitySet.mem e s then s *)
+           (*else*) EqualitySet.add e s
          else s)
       EqualitySet.empty new_pos
   in
@@ -617,7 +616,7 @@ let forward_simplify_new env new_pos ?passive active =
            not ((Indexing.in_index active_table e) ||
                   (Indexing.in_index passive_table e)))
   in
-  List.filter subs (List.filter is_duplicate new_pos)
+    List.filter subs (List.filter is_duplicate new_pos)
 ;;
 
 
@@ -1309,9 +1308,6 @@ let infer_goal_set env active goals =
         let selected = hd in
         let passive_goals = tl in
         let new' = Indexing.superposition_left env (snd active) selected in
-        let metasenv, context, ugraph = env in
-        let names = names_of_context context in
-        List.iter (fun (_,_,x) -> prerr_endline ("X: " ^ CicPp.pp x names)) new';
         selected::active_goals, passive_goals @ new'
     | _::tl -> aux tl
   in 
@@ -1356,11 +1352,14 @@ let given_clause
     else if Unix.gettimeofday () > max_time then
       (ParamodulationFailure "No more time to spend")
     else
+      let _ = prerr_endline "simpl goal with active" in
       let goals = simplify_goal_set env goals passive active in  
       match check_if_goals_set_is_solved env active goals with
       | Some p -> 
-          Printf.eprintf "Found a proof in: %f\n" 
-            (Unix.gettimeofday() -. initial_time);
+          prerr_endline 
+            (Printf.sprintf "Found a proof in: %f\n" 
+              (Unix.gettimeofday() -. initial_time));
+(*          assert false;*)
           ParamodulationSuccess p
       | None -> 
           prerr_endline 
@@ -1382,13 +1381,13 @@ let given_clause
           kept_clauses := (size_of_passive passive) + (size_of_active active);
           (* SELECTION *)
           if passive_is_empty passive then
-            ParamodulationFailure "No more passive" (* maybe this is a success! *)
+            ParamodulationFailure "No more passive"(*maybe this is a success! *)
           else
             begin
               let goals = infer_goal_set env active goals in
               let current, passive = select env goals passive in
-              Printf.eprintf  "Selected = %s\n"
-                (Equality.string_of_equality ~env current);
+              prerr_endline (Printf.sprintf  "Selected = %s\n"
+                (Equality.string_of_equality ~env current));
               (* SIMPLIFICATION OF CURRENT *)
               let res = 
                 forward_simplify env (Positive, current) ~passive active 
@@ -1397,23 +1396,24 @@ let given_clause
               | None -> step goals theorems passive active (iterno+1)
               | Some current ->
                   (* GENERATION OF NEW EQUATIONS *)
+                  prerr_endline "infer";
                   let new' = infer env current active in
+                  prerr_endline "infer goal";
                   let goals = infer_goal_set_with_current env current goals in
                   let active = 
-                    if Equality.is_identity env current then 
-                      assert false 
-                      (* nonsense code, check to se if it can be removed *)
-                    else
                       let al, tbl = active in
                       al @ [current], Indexing.index tbl current
                   in
                   (* FORWARD AND BACKWARD SIMPLIFICATION *)
+                  prerr_endline "fwd/back simpl";
                   let rec simplify new' active passive =
                     let new' = forward_simplify_new env new' ~passive active in
                     let active, passive, newa, retained, pruned =
                       backward_simplify env new' ~passive  active 
                     in
-                    let passive = List.fold_left filter_dependent passive pruned in
+                    let passive = 
+                      List.fold_left filter_dependent passive pruned 
+                    in
                     match newa, retained with
                     | None, None -> active, passive, new'
                     | Some p, None 
@@ -1421,6 +1421,7 @@ let given_clause
                     | Some p, Some rp -> simplify (new' @ p @ rp) active passive
                   in
                   let active, passive, new' = simplify new' active passive in
+                  prerr_endline "simpl goal with new";
                   let goals = 
                     let a,b,_ = build_table new' in
                     simplify_goal_set env goals passive (a,b)
@@ -1746,7 +1747,7 @@ let saturate
 *)
       let goals = make_goal_set goal in
       let max_iterations = 1000 in
-      let max_time = Unix.gettimeofday () +.  600. (* minutes *) in
+      let max_time = Unix.gettimeofday () +.  120. (* minutes *) in
       given_clause env goals theorems passive active max_iterations max_time 
     in
     let finish = Unix.gettimeofday () in
@@ -1766,15 +1767,11 @@ let saturate
           (ProofEngineHelpers.compare_metasenvs 
             ~newmetasenv:metasenv ~oldmetasenv:proof_menv)
       in
-      let free_metas = 
-        List.filter (fun i -> i <> goalno)
-          (ProofEngineHelpers.compare_metasenvs 
-            ~oldmetasenv:metasenv ~newmetasenv:proof_menv)
-      in
       let goal_proof, side_effects_t = 
-        let initial = Equality.build_proof_term newproof in
+        let initial = newproof in
         Equality.build_goal_proof goalproof initial type_of_goal side_effects
       in
+prerr_endline (CicPp.pp goal_proof names);
       let goal_proof = Subst.apply_subst subsumption_subst goal_proof in
       let side_effects_t = 
         List.map (Subst.apply_subst subsumption_subst) side_effects_t
@@ -1800,8 +1797,12 @@ let saturate
       let goal_proof = replace goal_proof in
         (* ok per le meta libere... ma per quelle che c'erano e sono rimaste? 
          * what mi pare buono, sostituisce solo le meta farlocche *)
-        prerr_endline (CicPp.pp goal_proof names);
       let side_effects_t = List.map replace side_effects_t in
+      let free_metas = 
+        List.filter (fun i -> i <> goalno)
+          (ProofEngineHelpers.compare_metasenvs 
+            ~oldmetasenv:metasenv ~newmetasenv:goal_proof_menv)
+      in
       (* check/refine/... build the new proof *)
       let replaced_goal = 
         ProofEngineReduction.replace
@@ -1827,18 +1828,24 @@ let saturate
         (goalno,(context,goal_proof,type_of_goal))::subst_side_effects
       in
       let _ = 
-        let ty,_ =
+        try
           CicTypeChecker.type_of_aux' real_menv context goal_proof
             CicUniv.empty_ugraph
-        in
-        ty
+        with 
+        | CicUtil.Meta_not_found _ 
+        | CicTypeChecker.TypeCheckerFailure _ 
+        | CicTypeChecker.AssertFailure _ 
+        | Invalid_argument "list_fold_left2" as exn ->
+            prerr_endline "THE PROOF DOES NOT TYPECHECK!";
+            prerr_endline (CicPp.pp goal_proof names);
+            raise exn
       in
       let proof, real_metasenv = 
         ProofEngineHelpers.subst_meta_and_metasenv_in_proof
           proof goalno (CicMetaSubst.apply_subst final_subst) real_menv
       in
       let open_goals = 
-        match free_meta with Some (Cic.Meta (m,_)) -> [m] | _ -> [] 
+        match free_meta with Some(Cic.Meta(m,_)) when m<>goalno ->[m] | _ ->[] 
       in
       Printf.eprintf 
         "GOALS APERTI: %s\nMETASENV PRIMA:\n%s\nMETASENV DOPO:\n%s\n" 
@@ -2033,7 +2040,7 @@ let demodulate_tac ~dbd ~pattern ((proof,goal)(*s initialstatus*)) =
   in
   if changed then
     begin
-      let opengoal = Cic.Meta(maxm,irl) in
+      let opengoal = Equality.Exact (Cic.Meta(maxm,irl)) in
       let proofterm,_ = 
         Equality.build_goal_proof newproof opengoal ty [] in
         let extended_metasenv = (maxm,context,newty)::metasenv in
@@ -2055,3 +2062,7 @@ let demodulate_tac ~dbd ~pattern ((proof,goal)(*s initialstatus*)) =
 let demodulate_tac ~dbd ~pattern = 
   ProofEngineTypes.mk_tactic (demodulate_tac ~dbd ~pattern)
 ;;
+
+let get_stats () = 
+  <:show<Saturation.>> ^ Indexing.get_stats () ^ Inference.get_stats ();;
+