X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fparamodulation%2Fsaturation.ml;h=413c7b15ea7bd760ed301b64f46d025336c3a646;hb=e6b28085c97ae7b9bd3f3262b105f6b84f42b047;hp=ec7634d94525ce35007ea475e72a959784c7b4a7;hpb=e701ae61ea78b5bcbc8919ccb51f4f2ada8c5f23;p=helm.git diff --git a/helm/ocaml/paramodulation/saturation.ml b/helm/ocaml/paramodulation/saturation.ml index ec7634d94..413c7b15e 100644 --- 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") *) ;;