(* 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.;;
type result =
- | Failure
- | Success of Inference.equality option * environment
+ | ParamodulationFailure
+ | ParamodulationSuccess of Inference.equality option * environment
;;
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 *)
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
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"
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
(* print_newline (); *)
given_clause env passive active
| true, goal ->
- Success (goal, env)
+ ParamodulationSuccess (goal, env)
)
;;
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
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"
(* print_newline (); *)
given_clause_fullred env passive active
| true, goal ->
- Success (goal, env)
+ ParamodulationSuccess (goal, env)
)
;;
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 =
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);
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
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" ^^
;;
-exception Failure of string
-
let saturate dbd (proof, goal) =
let module C = Cic in
maxmeta := 0;
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
(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") *)
;;