- better exception handling

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

diff --git a/helm/ocaml/paramodulation/saturation.ml b/helm/ocaml/paramodulation/saturation.ml
index f56b8946f0e248d305c8ca2927a01c459543d5be..13bb5714a6678910810168d10d5a684816021eca 100644 (file)
--- a/helm/ocaml/paramodulation/saturation.ml
+++ b/helm/ocaml/paramodulation/saturation.ml
@@ -37,8 +37,8 @@ let maxmeta = ref 0;;
 
 
 type result =
-  | Failure
-  | Success of Inference.equality option * environment
+  | ParamodulationFailure
+  | ParamodulationSuccess of Inference.equality option * environment
 ;;
 
 
@@ -87,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 *)
@@ -754,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
@@ -768,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"
@@ -782,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
@@ -857,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)
           )
 ;;
 
@@ -889,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
@@ -903,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"
@@ -985,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)
           )
 ;;
 
@@ -1005,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 =
@@ -1025,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);
@@ -1047,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
@@ -1081,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" ^^
@@ -1107,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;
@@ -1139,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
@@ -1191,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") *)
 ;;