added homepage URL, now we have one

[helm.git] / helm / ocaml / paramodulation / saturation.ml

diff --git a/helm/ocaml/paramodulation/saturation.ml b/helm/ocaml/paramodulation/saturation.ml
index ec7634d94525ce35007ea475e72a959784c7b4a7..413c7b15ea7bd760ed301b64f46d025336c3a646 100644 (file)
--- a/helm/ocaml/paramodulation/saturation.ml
+++ b/helm/ocaml/paramodulation/saturation.ml
@@ -5,10 +5,6 @@ open Utils;;
 (* set to false to disable paramodulation inside auto_tac *)
 let connect_to_auto = true;;
 
-let debug = true;;
-
-let debug_print = if debug then prerr_endline else ignore;;
-
 
 (* profiling statistics... *)
 let infer_time = ref 0.;;
@@ -41,8 +37,8 @@ let maxmeta = ref 0;;
 
 
 type result =
-  | Failure
-  | Success of Inference.equality option * environment
+  | ParamodulationFailure
+  | ParamodulationSuccess of Inference.equality option * environment
 ;;
 
 
@@ -91,7 +87,7 @@ module OrderedEquality = struct
               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
+              with Failure "hd" -> Pervasives.compare eq1 eq2
 (*               match a, a' with *)
 (*               | (Cic.Meta (i, _)::_), (Cic.Meta (j, _)::_) -> *)
 (*                   let res = Pervasives.compare i j in *)
@@ -758,7 +754,7 @@ let rec given_clause env passive active =
   kept_clauses := (size_of_passive passive) + (size_of_active active);
     
   match passive_is_empty passive with
-  | true -> Failure
+  | true -> ParamodulationFailure
   | false ->
       let (sign, current), passive = select env passive active in
       let time1 = Unix.gettimeofday () in
@@ -772,7 +768,7 @@ let rec given_clause env passive active =
           if (sign = Negative) && (is_identity env current) then (
             debug_print (Printf.sprintf "OK!!! %s %s" (string_of_sign sign)
                            (string_of_equality ~env current));
-            Success (Some current, env)
+            ParamodulationSuccess (Some current, env)
           ) else (            
             debug_print "\n================================================";
             debug_print (Printf.sprintf "selected: %s %s"
@@ -786,7 +782,7 @@ let rec given_clause env passive active =
             
             let res, goal = contains_empty env new' in
             if res then
-              Success (goal, env)
+              ParamodulationSuccess (goal, env)
             else 
               let t1 = Unix.gettimeofday () in
               let new' = forward_simplify_new env new' (* ~passive *) active in
@@ -861,7 +857,7 @@ let rec given_clause env passive active =
 (*                   print_newline (); *)
                   given_clause env passive active
               | true, goal ->
-                  Success (goal, env)
+                  ParamodulationSuccess (goal, env)
           )
 ;;
 
@@ -893,7 +889,7 @@ let rec given_clause_fullred env passive active =
   kept_clauses := (size_of_passive passive) + (size_of_active active);
 
   match passive_is_empty passive with
-  | true -> Failure
+  | true -> ParamodulationFailure
   | false ->
       let (sign, current), passive = select env passive active in
       let time1 = Unix.gettimeofday () in
@@ -907,7 +903,7 @@ let rec given_clause_fullred env passive active =
           if (sign = Negative) && (is_identity env current) then (
             debug_print (Printf.sprintf "OK!!! %s %s" (string_of_sign sign)
                            (string_of_equality ~env current));
-            Success (Some current, env)
+            ParamodulationSuccess (Some current, env)
           ) else (
             debug_print "\n================================================";
             debug_print (Printf.sprintf "selected: %s %s"
@@ -989,7 +985,7 @@ let rec given_clause_fullred env passive active =
 (*                 print_newline (); *)
                 given_clause_fullred env passive active
             | true, goal ->
-                Success (goal, env)
+                ParamodulationSuccess (goal, env)
           )
 ;;
 
@@ -1009,9 +1005,9 @@ let main dbd term metasenv ugraph =
   let _, metasenv, meta_proof, _ = proof in
   let _, context, goal = CicUtil.lookup_meta goal' metasenv in
   let equalities, maxm = find_equalities context proof in
-  let library_equalities, maxm =
-    find_library_equalities ~dbd context (proof, goal') (maxm+1)
-  in
+(*   let library_equalities, maxm = *)
+(*     find_library_equalities ~dbd context (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 =
@@ -1029,7 +1025,7 @@ let main dbd term metasenv ugraph =
     let _, meta_proof, (eq_ty, left, right, ordering), _, _ = term_equality in
     let active = make_active () in
     let passive =
-      make_passive [term_equality] (equalities @ library_equalities)
+      make_passive [term_equality] (equalities (* @ library_equalities *))
     in
     Printf.printf "\ncurrent goal: %s\n"
       (string_of_equality ~env term_equality);
@@ -1051,9 +1047,9 @@ let main dbd term metasenv ugraph =
     let finish = Unix.gettimeofday () in
     let _ =
       match res with
-      | Failure ->
+      | ParamodulationFailure ->
           Printf.printf "NO proof found! :-(\n\n"
-      | Success (Some goal, env) ->
+      | ParamodulationSuccess (Some goal, env) ->
           let proof = Inference.build_proof_term goal in         
           let newmetasenv =
             List.fold_left
@@ -1085,7 +1081,7 @@ let main dbd term metasenv ugraph =
           in
           ()
             
-      | Success (None, env) ->
+      | ParamodulationSuccess (None, env) ->
           Printf.printf "Success, but no proof?!?\n\n"
     in
     Printf.printf ("infer_time: %.9f\nforward_simpl_time: %.9f\n" ^^
@@ -1111,8 +1107,6 @@ let main dbd term metasenv ugraph =
 ;;
 
 
-exception Failure of string
-
 let saturate dbd (proof, goal) =
   let module C = Cic in
   maxmeta := 0;
@@ -1143,7 +1137,7 @@ let saturate dbd (proof, goal) =
     in
     let res = given_clause_fullred env passive active in
     match res with
-    | Success (Some goal, env) ->
+    | ParamodulationSuccess (Some goal, env) ->
         debug_print "OK, found a proof!";
         let proof = Inference.build_proof_term goal in         
         let names = names_of_context context in
@@ -1176,7 +1170,7 @@ let saturate dbd (proof, goal) =
                  (string_of_bool
                     (fst (CicReduction.are_convertible
                             context type_of_goal ty ug))));
-            let equality_for_replace t1 i =
+            let equality_for_replace i t1 =
               match t1 with
               | C.Meta (n, _) -> n = i
               | _ -> false
@@ -1195,14 +1189,15 @@ let saturate dbd (proof, goal) =
                 (CicPp.pp real_proof [](* names *))
                 (CicPp.pp term_to_prove names));
             ((uri, newmetasenv, real_proof, term_to_prove), [])
-          with e ->
+          with CicTypeChecker.TypeCheckerFailure _ ->
             debug_print "THE PROOF DOESN'T TYPECHECK!!!";
             debug_print (CicPp.pp proof names);
-            raise (Failure "Found a proof, but it doesn't typecheck")
+            raise
+              (ProofEngineTypes.Fail "Found a proof, but it doesn't typecheck")
         in
         newstatus          
     | _ ->
-        raise (Failure "NO proof found")
+        raise (ProofEngineTypes.Fail "NO proof found")
 (*   with e -> *)
 (*     raise (Failure "saturation failed") *)
 ;;