From 61380673d7cff22e19041260cbba4a9cbf5c09c5 Mon Sep 17 00:00:00 2001 From: Alberto Griggio Date: Fri, 22 Jul 2005 17:27:40 +0000 Subject: [PATCH] - better exception handling - compiled with -pack to get a Paramodulation namespace - fixed a bug in Inference.unification_simple --- helm/ocaml/paramodulation/.depend | 2 + helm/ocaml/paramodulation/Makefile | 16 +++++ .../paramodulation/discrimination_tree.ml | 7 ++- helm/ocaml/paramodulation/indexing.ml | 32 ++++++---- helm/ocaml/paramodulation/inference.ml | 59 +++++++++++-------- helm/ocaml/paramodulation/saturation.ml | 45 +++++++------- 6 files changed, 102 insertions(+), 59 deletions(-) diff --git a/helm/ocaml/paramodulation/.depend b/helm/ocaml/paramodulation/.depend index 8a74093c5..591ad1df8 100644 --- a/helm/ocaml/paramodulation/.depend +++ b/helm/ocaml/paramodulation/.depend @@ -11,3 +11,5 @@ indexing.cmo: utils.cmi inference.cmi discrimination_tree.cmo 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 diff --git a/helm/ocaml/paramodulation/Makefile b/helm/ocaml/paramodulation/Makefile index 321f5fba7..a21e59af7 100644 --- a/helm/ocaml/paramodulation/Makefile +++ b/helm/ocaml/paramodulation/Makefile @@ -24,6 +24,22 @@ IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml) \ 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) \ diff --git a/helm/ocaml/paramodulation/discrimination_tree.ml b/helm/ocaml/paramodulation/discrimination_tree.ml index dc87e7503..56e8bd44a 100644 --- a/helm/ocaml/paramodulation/discrimination_tree.ml +++ b/helm/ocaml/paramodulation/discrimination_tree.ml @@ -145,7 +145,8 @@ let rec subterm_at_pos pos term = | 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 ;; @@ -198,7 +199,7 @@ let retrieve_generalizations tree term = 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 @@ -264,7 +265,7 @@ let retrieve_unifiables tree term = 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 diff --git a/helm/ocaml/paramodulation/indexing.ml b/helm/ocaml/paramodulation/indexing.ml index be02d8c1b..4e222fd6a 100644 --- a/helm/ocaml/paramodulation/indexing.ml +++ b/helm/ocaml/paramodulation/indexing.ml @@ -169,7 +169,7 @@ let rec find_matches metasenv context ugraph lift_amount term = 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 @@ -184,10 +184,13 @@ let rec find_matches metasenv context ugraph lift_amount term = 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 @@ -237,7 +240,10 @@ let rec find_all_matches ?(unif_fun=Inference.unification) 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 @@ -254,7 +260,10 @@ let rec find_all_matches ?(unif_fun=Inference.unification) 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 @@ -272,9 +281,12 @@ let rec find_all_matches ?(unif_fun=Inference.unification) 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 ;; @@ -314,13 +326,13 @@ let subsumption env table target = 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 diff --git a/helm/ocaml/paramodulation/inference.ml b/helm/ocaml/paramodulation/inference.ml index dfdbab614..746a2faea 100644 --- a/helm/ocaml/paramodulation/inference.ml +++ b/helm/ocaml/paramodulation/inference.ml @@ -476,14 +476,23 @@ let unification_simple metasenv context t1 t2 ugraph = 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") @@ -492,12 +501,19 @@ let unification_simple metasenv context t1 t2 ugraph = 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 ;; @@ -594,7 +610,7 @@ let matching_simple metasenv context t1 t2 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 (); *) @@ -645,7 +661,9 @@ let matching metasenv context t1 t2 ugraph = (* 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); *) @@ -664,8 +682,6 @@ let beta_expand ?(metas_ok=true) ?(match_only=false) 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" *) @@ -954,11 +970,11 @@ let beta_expand ?(metas_ok=true) ?(match_only=false) (* 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 @@ -996,10 +1012,6 @@ let beta_expand ?(metas_ok=true) ?(match_only=false) (* 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 = @@ -1096,6 +1108,7 @@ let equations_blacklist = "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"; *) ] ;; @@ -1235,7 +1248,7 @@ let fix_metas newmeta ((w, p, (ty, left, right, o), menv, args) as equality) = (* (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 diff --git a/helm/ocaml/paramodulation/saturation.ml b/helm/ocaml/paramodulation/saturation.ml index f56b8946f..13bb5714a 100644 --- 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") *) ;; -- 2.39.2