indexing.cmx: utils.cmx inference.cmx discrimination_tree.cmx
saturation.cmo: utils.cmi inference.cmi indexing.cmo
saturation.cmx: utils.cmx inference.cmx indexing.cmx
+saturate_main.cmo: utils.cmi saturation.cmo
+saturate_main.cmx: utils.cmx saturation.cmx
include ../Makefile.common
+
+paramodulation.cmo: $(IMPLEMENTATION_FILES:%.ml=%.cmo)
+ $(OCAMLC) -pack -o $@ $(IMPLEMENTATION_FILES:%.ml=%.cmo)
+
+paramodulation.cmx: $(IMPLEMENTATION_FILES:%.ml=%.cmx)
+ $(OCAMLOPT) -pack -o $@ $(IMPLEMENTATION_FILES:%.ml=%.cmx)
+
+
+$(ARCHIVE): paramodulation.cmo $(LIBRARIES)
+ $(OCAMLC) $(OCAMLARCHIVEOPTIONS) -a -o $@ \
+ paramodulation.cmo
+
+$(ARCHIVE_OPT): paramodulation.cmx $(LIBRARIES_OPT)
+ $(OCAMLOPT) $(OCAMLARCHIVEOPTIONS) -a -o $@ \
+ paramodulation.cmx
+
PARAMOD_OBJS = $(IMPLEMENTATION_FILES:%.ml=%.cmo) \
saturate_main.cmo
PARAMOD_OBJS_OPT = $(IMPLEMENTATION_FILES:%.ml=%.cmx) \
| index::pos ->
match term with
| Cic.Appl l ->
- (try subterm_at_pos pos (List.nth l index) with _ -> raise Not_found)
+ (try subterm_at_pos pos (List.nth l index)
+ with Failure _ -> raise Not_found)
| _ -> raise Not_found
;;
in
try
let n = PSMap.find (Cic.Implicit None) map in
- let newpos = try after_t pos term with _ -> [-1] in
+ let newpos = try after_t pos term with Not_found -> [-1] in
if newpos = [-1] then
match n with
| DiscriminationTree.Node (Some s, _) -> PosEqSet.union s res
in
try
let n = PSMap.find (Cic.Implicit None) map in
- let newpos = try after_t pos term with _ -> [-1] in
+ let newpos = try after_t pos term with Not_found -> [-1] in
if newpos = [-1] then
match n with
| DiscriminationTree.Node (Some s, _) -> PosEqSet.union s res
let t2 = Unix.gettimeofday () in
match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
r
- with e ->
+ with Inference.MatchingFailure as e ->
let t2 = Unix.gettimeofday () in
match_unif_time_no := !match_unif_time_no +. (t2 -. t1);
raise e
if o <> U.Incomparable then
try
do_match c other eq_URI
- with e ->
+ with Inference.MatchingFailure ->
find_matches metasenv context ugraph lift_amount term tl
else
- let res = try do_match c other eq_URI with e -> None in
+ let res =
+ try do_match c other eq_URI
+ with Inference.MatchingFailure -> None
+ in
match res with
| Some (_, s, _, _, _) ->
let c' = (* M. *)apply_subst s c
let t2 = Unix.gettimeofday () in
match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
r
- with e ->
+ with
+ | Inference.MatchingFailure
+ | CicUnification.UnificationFailure _
+ | CicUnification.Uncertain _ as e ->
let t2 = Unix.gettimeofday () in
match_unif_time_no := !match_unif_time_no +. (t2 -. t1);
raise e
let res = do_match c other eq_URI in
res::(find_all_matches ~unif_fun metasenv context ugraph
lift_amount term tl)
- with e ->
+ with
+ | Inference.MatchingFailure
+ | CicUnification.UnificationFailure _
+ | CicUnification.Uncertain _ ->
find_all_matches ~unif_fun metasenv context ugraph
lift_amount term tl
else
else
find_all_matches ~unif_fun metasenv context ugraph
lift_amount term tl
- with e ->
- find_all_matches ~unif_fun metasenv context ugraph
- lift_amount term tl
+ with
+ | Inference.MatchingFailure
+ | CicUnification.UnificationFailure _
+ | CicUnification.Uncertain _ ->
+ find_all_matches ~unif_fun metasenv context ugraph
+ lift_amount term tl
;;
let t2 = Unix.gettimeofday () in
match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
r
- with e ->
+ with Inference.MatchingFailure as e ->
let t2 = Unix.gettimeofday () in
match_unif_time_no := !match_unif_time_no +. (t2 -. t1);
raise e
in
samesubst subst subst'
- with e ->
+ with Inference.MatchingFailure ->
false
in
let r = List.exists (ok right) leftr in
unif subst menv t s
| C.Meta _, t when occurs_check subst s t ->
raise (U.UnificationFailure "Inference.unification.unif")
- | C.Meta (i, l), t ->
- let _, _, ty = CicUtil.lookup_meta i menv in
- let subst =
- if not (List.mem_assoc i subst) then (i, (context, t, ty))::subst
- else subst
- in
- let menv = List.filter (fun (m, _, _) -> i <> m) menv in
- subst, menv
+ | C.Meta (i, l), t -> (
+ try
+ let _, _, ty = CicUtil.lookup_meta i menv in
+ let subst =
+ if not (List.mem_assoc i subst) then (i, (context, t, ty))::subst
+ else subst
+ in
+ let menv = menv in (* List.filter (fun (m, _, _) -> i <> m) menv in *)
+ subst, menv
+ with CicUtil.Meta_not_found m ->
+ let names = names_of_context context in
+ debug_print (
+ Printf.sprintf "Meta_not_found %d!: %s %s\n%s\n\n%s" m
+ (CicPp.pp t1 names) (CicPp.pp t2 names)
+ (print_metasenv menv) (print_metasenv metasenv));
+ assert false
+ )
| _, C.Meta _ -> unif subst menv t s
| C.Appl (hds::_), C.Appl (hdt::_) when hds <> hdt ->
raise (U.UnificationFailure "Inference.unification.unif")
List.fold_left2
(fun (subst', menv) s t -> unif subst' menv s t)
(subst, menv) tls tlt
- with e ->
+ with Invalid_argument _ ->
raise (U.UnificationFailure "Inference.unification.unif")
)
| _, _ -> raise (U.UnificationFailure "Inference.unification.unif")
in
let subst, menv = unif [] metasenv t1 t2 in
+ let menv =
+ List.filter
+ (fun (m, _, _) ->
+ try let _ = List.find (fun (i, _) -> m = i) subst in false
+ with Not_found -> true)
+ menv
+ in
List.rev subst, menv, ugraph
;;
List.fold_left2
(fun (subst, menv) s t -> do_match subst menv s t)
(subst, menv) ls lt
- with e ->
+ with Invalid_argument _ ->
(* print_endline (Printexc.to_string e); *)
(* Printf.printf "NO MATCH: %s %s\n" (CicPp.ppterm s) (CicPp.ppterm t); *)
(* print_newline (); *)
(* print_newline (); *)
subst, metasenv, ugraph
- with e ->
+ with
+ | CicUnification.UnificationFailure _
+ | CicUnification.Uncertain _ ->
(* Printf.printf "failed to match %s %s\n" *)
(* (CicPp.ppterm t1) (CicPp.ppterm t2); *)
(* print_endline (Printexc.to_string e); *)
let module S = CicSubstitution in
let module C = Cic in
- let print_info = false in
-
(* let _ = *)
(* let names = names_of_context context in *)
(* Printf.printf "beta_expand:\nwhat: %s, %s\nwhere: %s, %s\n" *)
(* else *)
((C.Rel (1 + lift_amount), subst', metasenv', ugraph')::res,
lifted_term)
- with e ->
- if print_info then (
- print_endline ("beta_expand ERROR!: " ^ (Printexc.to_string e));
- );
- res, lifted_term
+ with
+ | MatchingFailure
+ | CicUnification.UnificationFailure _
+ | CicUnification.Uncertain _ ->
+ res, lifted_term
in
(* Printf.printf "exit aux\n"; *)
retval
(* if match_only then replace_metas (\* context *\) where *)
(* else where *)
(* in *)
- if print_info then (
- Printf.printf "searching %s inside %s\n"
- (CicPp.ppterm what) (CicPp.ppterm where);
- );
aux 0 where context metasenv [] ugraph
in
let mapfun =
"cic:/Coq/Init/Logic/f_equal3.con";
"cic:/Coq/Init/Logic/sym_eq.con";
(* "cic:/Coq/Logic/Eqdep/UIP_refl.con"; *)
+(* "cic:/Coq/Init/Peano/mult_n_Sm.con"; *)
]
;;
(* (i, (context, Cic.Meta (j, l), ty))::s *)
let _, context, ty = CicUtil.lookup_meta i menv in
(i, (context, Cic.Meta (j, l), ty))::s
- with _ -> s
+ with Not_found -> s
)
| _ -> assert false)
[] args
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") *)
;;
projects / helm.git / commitdiff