X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Focaml%2Fparamodulation%2Fsaturation.ml;h=94f26a7e68c5c58c59d9fdf5ecbc906edf2ca5eb;hb=5e1fd9ee5ced5737c7fd4f25fca47feda1fda8e9;hp=793e48423b1d999d97a342fa8affe2048d2f3399;hpb=c9d7e6a946744890def5b5471c93b4dbd78c4ac9;p=helm.git

diff --git a/helm/ocaml/paramodulation/saturation.ml b/helm/ocaml/paramodulation/saturation.ml
index 793e48423..94f26a7e6 100644
--- a/helm/ocaml/paramodulation/saturation.ml
+++ b/helm/ocaml/paramodulation/saturation.ml
@@ -18,10 +18,10 @@ let elapsed_time = ref 0.;;
 let maximal_retained_equality = ref None;;
 
 (* equality-selection related globals *)
-let use_fullred = ref false;;
-let weight_age_ratio = ref 0;; (* settable by the user from the command line *)
+let use_fullred = ref true;;
+let weight_age_ratio = ref 3;; (* settable by the user from the command line *)
 let weight_age_counter = ref !weight_age_ratio;;
-let symbols_ratio = ref 0;;
+let symbols_ratio = ref 2;;
 let symbols_counter = ref 0;;
 
 (* statistics... *)
@@ -44,7 +44,7 @@ let symbols_of_equality (_, (_, left, right), _, _) =
 ;;
 *)
 
-let symbols_of_equality ((_, (_, left, right, _), _, _) as equality) =
+let symbols_of_equality ((_, _, (_, left, right, _), _, _) as equality) =
   let m1 = symbols_of_term left in
   let m = 
     TermMap.fold
@@ -64,17 +64,6 @@ let symbols_of_equality ((_, (_, left, right, _), _, _) as equality) =
 ;;
 
 
-let weight_of_equality (_, (ty, left, right, _), _, _) =
-  let meta_number = ref 0 in
-  let weight_of t =
-    let weight, ml =  weight_of_term t in
-    meta_number := !meta_number + (List.fold_left (fun r (_, n) -> r+n) 0 ml);
-    weight
-  in
-  (weight_of ty) + (weight_of left) + (weight_of right), meta_number
-;;
-
-
 module OrderedEquality = struct
   type t = Inference.equality
 
@@ -82,17 +71,25 @@ module OrderedEquality = struct
     match meta_convertibility_eq eq1 eq2 with
     | true -> 0
     | false ->
-        let _, (ty, left, right, _), _, _ = eq1
-        and _, (ty', left', right', _), _, _ = eq2 in
-(*         let w1, m1 = weight_of_equality eq1 *)
-(*         and w2, m2 = weight_of_equality eq2 in        *)
-        let weight_of t = fst (weight_of_term ~consider_metas:false t) in
-        let w1 = (weight_of ty) + (weight_of left) + (weight_of right)
-        and w2 = (weight_of ty') + (weight_of left') + (weight_of right') in
+        let w1, _, (ty, left, right, _), _, a = eq1
+        and w2, _, (ty', left', right', _), _, a' = eq2 in
+(*         let weight_of t = fst (weight_of_term ~consider_metas:false t) in *)
+(*         let w1 = (weight_of ty) + (weight_of left) + (weight_of right) *)
+(*         and w2 = (weight_of ty') + (weight_of left') + (weight_of right') in *)
         match Pervasives.compare w1 w2 with
-        | 0 -> Pervasives.compare eq1 eq2
-(*             let res = Pervasives.compare m1 m2 in *)
-(*             if res = 0 then Pervasives.compare eq1 eq2 else res *)
+        | 0 ->
+            let res = (List.length a) - (List.length a') in
+            if res <> 0 then res else (
+              try
+                let res = Pervasives.compare (List.hd a) (List.hd a') in
+                if res <> 0 then res else Pervasives.compare eq1 eq2
+              with _ -> Pervasives.compare eq1 eq2
+(*               match a, a' with *)
+(*               | (Cic.Meta (i, _)::_), (Cic.Meta (j, _)::_) -> *)
+(*                   let res = Pervasives.compare i j in *)
+(*                   if res <> 0 then res else Pervasives.compare eq1 eq2 *)
+(*               | _, _ -> Pervasives.compare eq1 eq2 *)
+            )
         | res -> res
 end
 
@@ -379,7 +376,10 @@ let infer env sign current (active_list, active_table) =
   let new_neg, new_pos = 
     match sign with
     | Negative ->
-        Indexing.superposition_left env active_table current, []
+        let maxm, res = 
+          Indexing.superposition_left !maxmeta env active_table current in
+        maxmeta := maxm;
+        res, [] 
     | Positive ->
         let maxm, res =
           Indexing.superposition_right !maxmeta env active_table current in
@@ -387,7 +387,9 @@ let infer env sign current (active_list, active_table) =
         let rec infer_positive table = function
           | [] -> [], []
           | (Negative, equality)::tl ->
-              let res = Indexing.superposition_left env table equality in
+              let maxm, res =
+                Indexing.superposition_left !maxmeta env table equality in
+              maxmeta := maxm;
               let neg, pos = infer_positive table tl in
               res @ neg, pos
           | (Positive, equality)::tl ->
@@ -417,7 +419,7 @@ let contains_empty env (negative, positive) =
   try
     let found =
       List.find
-        (fun (proof, (ty, left, right, ordering), m, a) ->
+        (fun (w, proof, (ty, left, right, ordering), m, a) ->
            fst (CicReduction.are_convertible context left right ugraph))
         negative
     in
@@ -458,11 +460,11 @@ let forward_simplify env (sign, current) ?passive (active_list, active_table) =
   
   let demodulate table current = 
     let newmeta, newcurrent =
-      Indexing.demodulation !maxmeta env table current in
+      Indexing.demodulation !maxmeta env table sign current in
     maxmeta := newmeta;
     if is_identity env newcurrent then
       if sign = Negative then Some (sign, newcurrent)
-      else (Inference.delete_proof newcurrent; None)
+      else None
     else
       Some (sign, newcurrent)
   in
@@ -486,13 +488,12 @@ let forward_simplify env (sign, current) ?passive (active_list, active_table) =
       if ok then res else None
   | Some (Positive, c) ->
       if Indexing.in_index active_table c then
-        (Inference.delete_proof c; None)
+        None
       else
         match passive_table with
         | None -> res
         | Some passive_table ->
-            if Indexing.in_index passive_table c then
-              (Inference.delete_proof c; None)
+            if Indexing.in_index passive_table c then None
             else res
 
 (*   | Some (s, c) -> if find_duplicate s c all then None else res *)
@@ -546,8 +547,9 @@ let forward_simplify_new env (new_neg, new_pos) ?passive active =
   let t2 = Unix.gettimeofday () in
   fs_time_info.build_all <- fs_time_info.build_all +. (t2 -. t1);
   
-  let demodulate table target =
-    let newmeta, newtarget = Indexing.demodulation !maxmeta env table target in
+  let demodulate sign table target =
+    let newmeta, newtarget =
+      Indexing.demodulation !maxmeta env table sign target in
     maxmeta := newmeta;
     newtarget
   in
@@ -559,13 +561,13 @@ let forward_simplify_new env (new_neg, new_pos) ?passive active =
   let t1 = Unix.gettimeofday () in
 
   let new_neg, new_pos =
-    let new_neg = List.map (demodulate active_table) new_neg
-    and new_pos = List.map (demodulate active_table) new_pos in
+    let new_neg = List.map (demodulate Negative active_table) new_neg
+    and new_pos = List.map (demodulate Positive active_table) new_pos in
     match passive_table with
     | None -> new_neg, new_pos
     | Some passive_table ->
-        List.map (demodulate passive_table) new_neg,
-        List.map (demodulate passive_table) new_pos
+        List.map (demodulate Negative passive_table) new_neg,
+        List.map (demodulate Positive passive_table) new_pos
   in
 
   let t2 = Unix.gettimeofday () in
@@ -575,12 +577,9 @@ let forward_simplify_new env (new_neg, new_pos) ?passive active =
     List.fold_left
       (fun s e ->
          if not (Inference.is_identity env e) then
-           if EqualitySet.mem e s then
-             (Inference.delete_proof e; s)
-           else
-             EqualitySet.add e s
-         else
-           (Inference.delete_proof e; s))
+           if EqualitySet.mem e s then s
+           else EqualitySet.add e s
+         else s)
       EqualitySet.empty new_pos
   in
   let new_pos = EqualitySet.elements new_pos_set in
@@ -612,16 +611,11 @@ let forward_simplify_new env (new_neg, new_pos) ?passive active =
   let is_duplicate =
     match passive_table with
     | None ->
-        (fun e ->
-           let ok = not (Indexing.in_index active_table e) in
-           if not ok then Inference.delete_proof e;
-           ok)
+        (fun e -> not (Indexing.in_index active_table e))
     | Some passive_table ->
         (fun e ->
-           let ok = not ((Indexing.in_index active_table e) ||
-                           (Indexing.in_index passive_table e)) in
-           if not ok then Inference.delete_proof e;
-           ok)
+           not ((Indexing.in_index active_table e) ||
+                  (Indexing.in_index passive_table e)))
   in
   new_neg, List.filter is_duplicate new_pos
 
@@ -658,7 +652,6 @@ let backward_simplify_active env new_pos new_table active =
          if List.mem (s, eq) res then
            res, tbl
          else if (is_identity env eq) || (find eq res) then (
-           Inference.delete_proof eq;
            res, tbl
          ) (* else if (find eq res) then *)
 (*            res, tbl *)
@@ -668,7 +661,6 @@ let backward_simplify_active env new_pos new_table active =
     List.fold_right
       (fun (s, eq) (n, p) ->
          if (s <> Negative) && (is_identity env eq) then (
-           Inference.delete_proof eq;
            (n, p)
          ) else
            if s = Negative then eq::n, p
@@ -849,7 +841,7 @@ let rec given_clause env passive active =
                         al @ [(sign, current)], Indexing.index tbl current
                   in
                   let passive = add_to_passive passive new' in
-(*                   let (_, ns), (_, ps), _ = passive in *)
+                  let (_, ns), (_, ps), _ = passive in
 (*                   Printf.printf "passive:\n%s\n" *)
 (*                     (String.concat "\n" *)
 (*                        ((List.map (fun e -> "Negative " ^ *)
@@ -977,6 +969,16 @@ let rec given_clause_fullred env passive active =
             match contains_empty env new' with
             | false, _ -> 
                 let passive = add_to_passive passive new' in
+                let (_, ns), (_, ps), _ = passive in
+(*                 Printf.printf "passive:\n%s\n" *)
+(*                   (String.concat "\n" *)
+(*                      ((List.map (fun e -> "Negative " ^ *)
+(*                                    (string_of_equality ~env e)) *)
+(*                          (EqualitySet.elements ns)) @ *)
+(*                         (List.map (fun e -> "Positive " ^ *)
+(*                                      (string_of_equality ~env e)) *)
+(*                            (EqualitySet.elements ps)))); *)
+(*                 print_newline (); *)
                 given_clause_fullred env passive active
             | true, goal ->
                 Success (goal, env)
@@ -984,9 +986,7 @@ let rec given_clause_fullred env passive active =
 ;;
 
 
-let get_from_user () =
-  let dbd = Mysql.quick_connect
-    ~host:"localhost" ~user:"helm" ~database:"mowgli" () in
+let get_from_user ~(dbd:Mysql.dbd) =
   let rec get () =
     match read_line () with
     | "" -> []
@@ -1008,19 +1008,33 @@ let main () =
   let module T = CicTypeChecker in
   let module PET = ProofEngineTypes in
   let module PP = CicPp in
-  let term, metasenv, ugraph = get_from_user () in
+  let dbd = Mysql.quick_connect
+    ~host:"localhost" ~user:"helm" ~database:"mowgli" () in
+  let term, metasenv, ugraph = get_from_user ~dbd in
   let proof = None, (1, [], term)::metasenv, C.Meta (1, []), term in
-  let proof, goals =
-    PET.apply_tactic (PrimitiveTactics.intros_tac ()) (proof, 1) in
-  let goal = List.nth goals 0 in
+  let status = PET.apply_tactic (PrimitiveTactics.intros_tac ()) (proof, 1) in
+  let proof, goals = status in
+  let goal' = List.nth goals 0 in
   let _, metasenv, meta_proof, _ = proof in
-  let _, context, goal = CicUtil.lookup_meta goal metasenv in
+  let _, context, goal = CicUtil.lookup_meta goal' metasenv in
   let equalities, maxm = find_equalities context proof in
-  maxmeta := maxm; (* TODO ugly!! *)
+  let library_equalities, maxm =
+    find_library_equalities ~dbd (proof, goal') (maxm+1) in
+  maxmeta := maxm+2; (* TODO ugly!! *)
+  let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
+  let new_meta_goal, metasenv, type_of_goal =
+    let _, context, ty = CicUtil.lookup_meta goal' metasenv in
+    Printf.printf "\n\nTIPO DEL GOAL: %s\n" (CicPp.ppterm ty);
+    print_newline ();
+    Cic.Meta (maxm+1, irl),
+    (maxm+1, context, ty)::metasenv,
+    ty
+  in
+(*   let new_meta_goal = Cic.Meta (goal', irl) in *)
   let env = (metasenv, context, ugraph) in
   try
-    let term_equality = equality_of_term meta_proof goal in
-    let meta_proof, (eq_ty, left, right, ordering), _, _ = term_equality in
+    let term_equality = equality_of_term new_meta_goal goal in
+    let _, meta_proof, (eq_ty, left, right, ordering), _, _ = term_equality in
     let active = make_active () in
     let passive = make_passive [term_equality] equalities in
     Printf.printf "\ncurrent goal: %s\n"
@@ -1047,9 +1061,34 @@ let main () =
           Printf.printf "NO proof found! :-(\n\n"
       | Success (Some goal, env) ->
           Printf.printf "OK, found a proof!\n";
-          let proof = Inference.build_term_proof goal in
-          print_endline (PP.pp proof (names_of_context context));
+          let proof = Inference.build_proof_term goal in         
+          (* REMEMBER: we have to instantiate meta_proof, we should use
+             apply  the "apply" tactic to proof and status 
+          *)
+          let names = names_of_context context in
+          print_endline (PP.pp proof names);
+(*           print_endline (PP.ppterm proof); *)
+          
           print_endline (string_of_float (finish -. start));
+          let newmetasenv =
+            List.fold_left
+              (fun m (_, _, _, menv, _) -> m @ menv) metasenv equalities
+          in
+          let _ =
+          try
+            let ty, ug =
+              CicTypeChecker.type_of_aux' newmetasenv context proof ugraph
+            in
+            Printf.printf
+              "\nGOAL was: %s\nPROOF has type: %s\nconvertible?: %s\n\n"
+              (CicPp.pp type_of_goal names) (CicPp.pp ty names)
+              (string_of_bool
+                 (fst (CicReduction.are_convertible context type_of_goal ty ug)));
+          with e ->
+            Printf.printf "MAXMETA USED: %d\n" !maxmeta;
+          in
+          ()
+            
       | Success (None, env) ->
           Printf.printf "Success, but no proof?!?\n\n"
     in
@@ -1076,7 +1115,82 @@ let main () =
 ;;
 
 
-let configuration_file = ref "../../gTopLevel/gTopLevel.conf.xml";;
+let saturation_tactic status =
+  let module C = Cic in
+  let saturation_tac (proof, goal) =
+    maxmeta := 0;
+(*     if List.length goals <> 1 then *)
+(*       raise (ProofEngineTypes.Fail "There should be only one open goal"); *)
+    
+(*     let goal' = List.hd goals in *)
+    let goal' = goal in
+    let uri, metasenv, meta_proof, term_to_prove = proof in
+    let _, context, goal = CicUtil.lookup_meta goal' metasenv in
+    let equalities, maxm = find_equalities context proof in
+    maxmeta := maxm+2;
+    let new_meta_goal, metasenv, type_of_goal =
+      let irl =
+        CicMkImplicit.identity_relocation_list_for_metavariable context in
+      let _, context, ty = CicUtil.lookup_meta goal' metasenv in
+      Printf.printf "\n\nTIPO DEL GOAL: %s\n" (CicPp.ppterm ty);
+      print_newline ();
+      Cic.Meta (maxm+1, irl),
+      (maxm+1, context, ty)::metasenv,
+      ty
+    in
+    let ugraph = CicUniv.empty_ugraph in
+    let env = (metasenv, context, ugraph) in
+    try
+      let term_equality = equality_of_term new_meta_goal goal in
+(*       let _, meta_proof, (eq_ty, left, right, ordering), _, _ = term_equality in *)
+      let active = make_active () in
+      let passive = make_passive [term_equality] equalities in
+      let res = given_clause_fullred env passive active in
+      match res with
+      | Success (Some goal, env) ->
+          Printf.printf "OK, found a proof!\n";
+          let proof = Inference.build_proof_term goal in         
+          let names = names_of_context context in
+          print_endline (CicPp.pp proof names);
+          let newmetasenv =
+            let i1 =
+              match new_meta_goal with
+              | C.Meta (i, _) -> i | _ -> assert false
+            in
+            let i2 =
+              match meta_proof with
+              | C.Meta (i, _) -> i | _ -> assert false
+            in
+            List.filter (fun (i, _, _) -> i <> i1 && i <> i2) metasenv
+          in
+          let newstatus =
+            try
+              let ty, ug =
+                CicTypeChecker.type_of_aux' newmetasenv context proof ugraph
+              in
+              Printf.printf
+                "\nGOAL was: %s\nPROOF has type: %s\nconvertible?: %s\n\n"
+                (CicPp.pp type_of_goal names) (CicPp.pp ty names)
+                (string_of_bool
+                   (fst (CicReduction.are_convertible
+                           context type_of_goal ty ug)));
+              ((uri, newmetasenv, proof, term_to_prove), [])
+            with e ->
+              raise (ProofEngineTypes.Fail
+                       "Found a proof, but it doesn't typecheck")
+          in
+          newstatus          
+      | _ ->
+          raise (ProofEngineTypes.Fail "NO proof found")
+    with e ->
+      raise (ProofEngineTypes.Fail "saturation failed")
+  in
+  ProofEngineTypes.mk_tactic saturation_tac
+;;
+
+
+
+let configuration_file = ref "../../matita/matita.conf.xml";;
 
 let _ =
   let set_ratio v = weight_age_ratio := (v+1); weight_age_counter := (v+1)
@@ -1084,16 +1198,17 @@ let _ =
   and set_conf f = configuration_file := f
   and set_lpo () = Utils.compare_terms := lpo
   and set_kbo () = Utils.compare_terms := nonrec_kbo
-  and set_fullred () = use_fullred := true
+  and set_fullred b = use_fullred := b
   and set_time_limit v = time_limit := float_of_int v
   in
   Arg.parse [
-    "-f", Arg.Unit set_fullred, "Use full-reduction strategy";
+    "-f", Arg.Bool set_fullred,
+    "Enable/disable full-reduction strategy (default: enabled)";
     
-    "-r", Arg.Int set_ratio, "Weight-Age equality selection ratio (default: 0)";
+    "-r", Arg.Int set_ratio, "Weight-Age equality selection ratio (default: 3)";
 
     "-s", Arg.Int set_sel,
-    "symbols-based selection ratio (relative to the weight ratio)";
+    "symbols-based selection ratio (relative to the weight ratio, default: 2)";
 
     "-c", Arg.String set_conf, "Configuration file (for the db connection)";