From 8313a3a7acdfdf7f5bbcf74378a503a9fe442d36 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Thu, 29 Jun 2006 13:38:14 +0000 Subject: [PATCH] Cleaning up; removed a couple of "open". --- .../tactics/paramodulation/saturation.ml | 136 +++++++++--------- 1 file changed, 66 insertions(+), 70 deletions(-) diff --git a/components/tactics/paramodulation/saturation.ml b/components/tactics/paramodulation/saturation.ml index 6cd2bcf4a..306f02dcf 100644 --- a/components/tactics/paramodulation/saturation.ml +++ b/components/tactics/paramodulation/saturation.ml @@ -27,10 +27,8 @@ let _profiler = <:profiler<_profiler>>;; (* $Id$ *) -open Inference;; -open Utils;; - (* set to false to disable paramodulation inside auto_tac *) + let connect_to_auto = true;; @@ -79,22 +77,22 @@ type result = | ParamodulationSuccess of new_proof ;; -type goal = Equality.goal_proof * Cic.metasenv * Cic.term;; +(* type goal = Equality.goal_proof * Cic.metasenv * Cic.term;; *) type theorem = Cic.term * Cic.term * Cic.metasenv;; let symbols_of_equality equality = let (_, _, (_, left, right, _), _,_) = Equality.open_equality equality in - let m1 = symbols_of_term left in + let m1 = Utils.symbols_of_term left in let m = - TermMap.fold + Utils.TermMap.fold (fun k v res -> try - let c = TermMap.find k res in - TermMap.add k (c+v) res + let c = Utils.TermMap.find k res in + Utils.TermMap.add k (c+v) res with Not_found -> - TermMap.add k v res) - (symbols_of_term right) m1 + Utils.TermMap.add k v res) + (Utils.symbols_of_term right) m1 in m ;; @@ -177,16 +175,16 @@ let rec select env (goals,_) passive = | _ when (!symbols_counter > 0) -> (symbols_counter := !symbols_counter - 1; let cardinality map = - TermMap.fold (fun k v res -> res + v) map 0 + Utils.TermMap.fold (fun k v res -> res + v) map 0 in let symbols = let _, _, term = goal in - symbols_of_term term + Utils.symbols_of_term term in let card = cardinality symbols in let foldfun k v (r1, r2) = - if TermMap.mem k symbols then - let c = TermMap.find k symbols in + if Utils.TermMap.mem k symbols then + let c = Utils.TermMap.find k symbols in let c1 = abs (c - v) in let c2 = v - c1 in r1 + c2, r2 + c1 @@ -195,7 +193,7 @@ let rec select env (goals,_) passive = in let f equality (i, e) = let common, others = - TermMap.fold foldfun (symbols_of_equality equality) (0, 0) + Utils.TermMap.fold foldfun (symbols_of_equality equality) (0, 0) in let c = others + (abs (common - card)) in if c < i then (c, equality) @@ -204,7 +202,7 @@ let rec select env (goals,_) passive = let e1 = EqualitySet.min_elt pos_set in let initial = let common, others = - TermMap.fold foldfun (symbols_of_equality e1) (0, 0) + Utils.TermMap.fold foldfun (symbols_of_equality e1) (0, 0) in (others + (abs (common - card))), e1 in @@ -305,7 +303,7 @@ let prune_passive howmany (active, _) passive = in let in_weight = round (howmany *. ratio /. (ratio +. 1.)) and in_age = round (howmany /. (ratio +. 1.)) in - debug_print + Utils.debug_print (lazy (Printf.sprintf "in_weight: %d, in_age: %d\n" in_weight in_age)); let counter = ref !symbols_ratio in let rec pickw w ps = @@ -546,7 +544,7 @@ let forward_simplify_new eq_uri env new_pos ?passive active = in (* we could also demodulate using passive. Currently we don't *) let new_pos = - List.map (demodulate Positive active_table) new_pos + List.map (demodulate Utils.Positive active_table) new_pos in let new_pos_set = List.fold_left @@ -689,7 +687,7 @@ let backward_simplify_passive eq_uri env new_pos new_table min_weight passive = let ress = EqualitySet.remove equality ress in resl, ress, e::newn in - let pl, ps, newp = List.fold_right (f Positive) pl ([], ps, []) in + let pl, ps, newp = List.fold_right (f Utils.Positive) pl ([], ps, []) in let passive_table = List.fold_left (fun tbl e -> Indexing.index tbl e) Indexing.empty pl @@ -761,7 +759,7 @@ let is_commutative_law eq = let prova eq_uri env new' active = let given = List.filter is_commutative_law (fst active) in let _ = - debug_print + Utils.debug_print (lazy (Printf.sprintf "symmetric:\n%s\n" (String.concat "\n" @@ -822,8 +820,8 @@ let simplify_theorems env theorems ?passive (active_list, active_table) = match passive with | None -> [], None | Some ((pn, _), (pp, _), pt) -> - let pn = List.map (fun e -> (Negative, e)) pn - and pp = List.map (fun e -> (Positive, e)) pp in + let pn = List.map (fun e -> (Utils.Negative, e)) pn + and pp = List.map (fun e -> (Utils.Positive, e)) pp in pn @ pp, Some pt in let a_theorems, p_theorems = theorems in @@ -858,7 +856,7 @@ let rec simpl eq_uri env e others others_simpl = (fun t e -> Indexing.index t e) Indexing.empty active in - let res = forward_simplify eq_uri env (Positive,e) (active, tbl) in + let res = forward_simplify eq_uri env (Utils.Positive,e) (active, tbl) in match others with | hd::tl -> ( match res with @@ -873,19 +871,19 @@ let rec simpl eq_uri env e others others_simpl = ;; let simplify_equalities eq_uri env equalities = - debug_print + Utils.debug_print (lazy (Printf.sprintf "equalities:\n%s\n" (String.concat "\n" (List.map Equality.string_of_equality equalities)))); - debug_print (lazy "SIMPLYFYING EQUALITIES..."); + Utils.debug_print (lazy "SIMPLYFYING EQUALITIES..."); match equalities with | [] -> [] | hd::tl -> let res = List.rev (simpl eq_uri env hd tl []) in - debug_print + Utils.debug_print (lazy (Printf.sprintf "equalities AFTER:\n%s\n" (String.concat "\n" @@ -917,16 +915,13 @@ let pp_goal_set msg goals names = ;; let check_if_goal_is_subsumed ((_,ctx,_) as env) table (goalproof,menv,ty) = - let names = names_of_context ctx in -(* - Printf.eprintf "check_goal_subsumed: %s\n" (CicPp.pp ty names); -*) + let names = Utils.names_of_context ctx in match ty with | Cic.Appl[Cic.MutInd(uri,_,_);eq_ty;left;right] when LibraryObjects.is_eq_URI uri -> (let goal_equation = Equality.mk_equality - (0,Equality.Exact (Cic.Implicit None),(eq_ty,left,right,Eq),menv) + (0,Equality.Exact (Cic.Implicit None),(eq_ty,left,right,Utils.Eq),menv) in (* match Indexing.subsumption env table goal_equation with*) match Indexing.unification env table goal_equation with @@ -1107,7 +1102,7 @@ let size_of_goal_set_p (_,l) = List.length l;; let given_clause eq_uri ((_,context,_) as env) goals theorems passive active max_iterations max_time = - let names = names_of_context context in + let names = Utils.names_of_context context in let initial_time = Unix.gettimeofday () in let iterations_left iterno = let now = Unix.gettimeofday () in @@ -1192,7 +1187,7 @@ let given_clause in (* SIMPLIFICATION OF CURRENT *) let res = - forward_simplify eq_uri env (Positive, current) active + forward_simplify eq_uri env (Utils.Positive, current) active in match res with | None -> step goals theorems passive active (iterno+1) @@ -1257,12 +1252,12 @@ let rec saturate_equations eq_uri env goal accept_fun passive active = (active, passive) else let current, passive = select env ([goal],[]) passive in - let res = forward_simplify eq_uri env (Positive, current) ~passive active in + let res = forward_simplify eq_uri env (Utils.Positive, current) ~passive active in match res with | None -> saturate_equations eq_uri env goal accept_fun passive active | Some current -> - debug_print (lazy (Printf.sprintf "selected: %s" + Utils.debug_print (lazy (Printf.sprintf "selected: %s" (Equality.string_of_equality ~env current))); let new' = infer eq_uri env current active in let active = @@ -1287,7 +1282,7 @@ let rec saturate_equations eq_uri env goal accept_fun passive active = in let active, passive, new' = simplify new' active passive in let _ = - debug_print + Utils.debug_print (lazy (Printf.sprintf "active:\n%s\n" (String.concat "\n" @@ -1296,7 +1291,7 @@ let rec saturate_equations eq_uri env goal accept_fun passive active = (fst active))))) in let _ = - debug_print + Utils.debug_print (lazy (Printf.sprintf "new':\n%s\n" (String.concat "\n" @@ -1322,17 +1317,17 @@ let main dbd full term metasenv ugraph = let goal' = List.nth goals 0 in let _, metasenv, meta_proof, _ = proof in let _, context, goal = CicUtil.lookup_meta goal' metasenv in - let eq_indexes, equalities, maxm = find_equalities context proof in + let eq_indexes, equalities, maxm = Inference.find_equalities context proof in let lib_eq_uris, library_equalities, maxm = - find_library_equalities dbd context (proof, goal') (maxm+2) + Inference.find_library_equalities dbd context (proof, goal') (maxm+2) in let library_equalities = List.map snd library_equalities 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 _, context, ty = CicUtil.lookup_meta goal' metasenv in - debug_print + Utils.debug_print (lazy (Printf.sprintf "\n\nTIPO DEL GOAL: %s\n\n" (CicPp.ppterm ty))); Cic.Meta (maxm+1, irl), @@ -1343,8 +1338,8 @@ let main dbd full term metasenv ugraph = let t1 = Unix.gettimeofday () in let theorems = if full then - let theorems = find_library_theorems dbd env (proof, goal') lib_eq_uris in - let context_hyp = find_context_hypotheses env eq_indexes in + let theorems = Inference.find_library_theorems dbd env (proof, goal') lib_eq_uris in + let context_hyp = Inference.find_context_hypotheses env eq_indexes in context_hyp @ theorems, [] else let refl_equal = @@ -1356,11 +1351,11 @@ let main dbd full term metasenv ugraph = [(t, ty, [])], [] in let t2 = Unix.gettimeofday () in - debug_print + Utils.debug_print (lazy (Printf.sprintf "Time to retrieve theorems: %.9f\n" (t2 -. t1))); let _ = - debug_print + Utils.debug_print (lazy (Printf.sprintf "Theorems:\n-------------------------------------\n%s\n" @@ -1382,7 +1377,7 @@ let main dbd full term metasenv ugraph = Printf.printf "\ncurrent goal: %s\n" (let _, _, g = goal in CicPp.ppterm g); Printf.printf "\ncontext:\n%s\n" (PP.ppcontext context); - Printf.printf "\nmetasenv:\n%s\n" (print_metasenv metasenv); + Printf.printf "\nmetasenv:\n%s\n" (Utils.print_metasenv metasenv); Printf.printf "\nequalities:\n%s\n" (String.concat "\n" (List.map @@ -1412,7 +1407,7 @@ let main dbd full term metasenv ugraph = (* REMEMBER: we have to instantiate meta_proof, we should use apply the "apply" tactic to proof and status *) - let names = names_of_context context in + let names = Utils.names_of_context context in prerr_endline "OLD PROOF"; print_endline (PP.pp proof names); prerr_endline "NEW PROOF"; @@ -1521,8 +1516,8 @@ let saturate let uri, metasenv, meta_proof, term_to_prove = proof in let _, context, type_of_goal = CicUtil.lookup_meta goalno metasenv in let eq_uri = eq_of_goal type_of_goal in - let names = names_of_context context in - let eq_indexes, equalities, maxm = find_equalities context proof in + let names = Utils.names_of_context context in + let eq_indexes, equalities, maxm = Inference.find_equalities context proof in let ugraph = CicUniv.empty_ugraph in let env = (metasenv, context, ugraph) in let cleaned_goal = Utils.remove_local_context type_of_goal in @@ -1530,7 +1525,7 @@ let saturate let res, time = let t1 = Unix.gettimeofday () in let lib_eq_uris, library_equalities, maxm = - find_library_equalities caso_strano dbd context (proof, goalno) (maxm+2) + Inference.find_library_equalities caso_strano dbd context (proof, goalno) (maxm+2) in let library_equalities = List.map snd library_equalities in let t2 = Unix.gettimeofday () in @@ -1538,14 +1533,14 @@ let saturate let equalities = simplify_equalities eq_uri env (equalities@library_equalities) in - debug_print + Utils.debug_print (lazy (Printf.sprintf "Time to retrieve equalities: %.9f\n" (t2 -. t1))); let t1 = Unix.gettimeofday () in let theorems = if full then - let thms = find_library_theorems dbd env (proof, goalno) lib_eq_uris in - let context_hyp = find_context_hypotheses env eq_indexes in + let thms = Inference.find_library_theorems dbd env (proof, goalno) lib_eq_uris in + let context_hyp = Inference.find_context_hypotheses env eq_indexes in context_hyp @ thms, [] else let refl_equal = LibraryObjects.eq_refl_URI ~eq:eq_uri in @@ -1555,7 +1550,7 @@ let saturate in let t2 = Unix.gettimeofday () in let _ = - debug_print + Utils.debug_print (lazy (Printf.sprintf "Theorems:\n-------------------------------------\n%s\n" @@ -1566,7 +1561,7 @@ let saturate "Term: %s, type: %s" (CicPp.ppterm t) (CicPp.ppterm ty)) (fst theorems))))); - debug_print + Utils.debug_print (lazy (Printf.sprintf "Time to retrieve theorems: %.9f\n" (t2 -. t1))); in @@ -1719,16 +1714,16 @@ let retrieve_and_print dbd term metasenv ugraph = let uri, metasenv, meta_proof, term_to_prove = proof in let _, context, type_of_goal = CicUtil.lookup_meta goal' metasenv in let eq_uri = eq_of_goal type_of_goal in - let eq_indexes, equalities, maxm = find_equalities context proof in + let eq_indexes, equalities, maxm = Inference.find_equalities context proof in let ugraph = CicUniv.empty_ugraph in let env = (metasenv, context, ugraph) in let t1 = Unix.gettimeofday () in let lib_eq_uris, library_equalities, maxm = - find_library_equalities false dbd context (proof, goal') (maxm+2) in + Inference.find_library_equalities false dbd context (proof, goal') (maxm+2) in let t2 = Unix.gettimeofday () in maxmeta := maxm+2; let equalities = (* equalities @ *) library_equalities in - debug_print + Utils.debug_print (lazy (Printf.sprintf "\n\nequalities:\n%s\n" (String.concat "\n" @@ -1739,17 +1734,17 @@ let retrieve_and_print dbd term metasenv ugraph = (* (string_of_equality e) *) ) equalities)))); - debug_print (lazy "RETR: SIMPLYFYING EQUALITIES..."); + Utils.debug_print (lazy "RETR: SIMPLYFYING EQUALITIES..."); let rec simpl e others others_simpl = let (u, e) = e in - let active = List.map (fun (u, e) -> (Positive, e)) + let active = List.map (fun (u, e) -> (Utils.Positive, e)) (others @ others_simpl) in let tbl = List.fold_left (fun t (_, e) -> Indexing.index t e) Indexing.empty active in - let res = forward_simplify eq_uri env (Positive, e) (active, tbl) in + let res = forward_simplify eq_uri env (Utils.Positive, e) (active, tbl) in match others with | hd::tl -> ( match res with @@ -1766,11 +1761,11 @@ let retrieve_and_print dbd term metasenv ugraph = match equalities with | [] -> [] | hd::tl -> - let others = tl in (* List.map (fun e -> (Positive, e)) tl in *) + let others = tl in (* List.map (fun e -> (Utils.Positive, e)) tl in *) let res = List.rev (simpl (*(Positive,*) hd others []) in - debug_print + Utils.debug_print (lazy (Printf.sprintf "\nequalities AFTER:\n%s\n" (String.concat "\n" @@ -1782,7 +1777,7 @@ let retrieve_and_print dbd term metasenv ugraph = ) res)))); res in - debug_print + Utils.debug_print (lazy (Printf.sprintf "Time to retrieve equalities: %.9f\n" (t2 -. t1))) ;; @@ -1800,16 +1795,16 @@ let main_demod_equalities dbd term metasenv ugraph = let _, metasenv, meta_proof, _ = proof in let _, context, goal = CicUtil.lookup_meta goal' metasenv in let eq_uri = eq_of_goal goal in - let eq_indexes, equalities, maxm = find_equalities context proof in + let eq_indexes, equalities, maxm = Inference.find_equalities context proof in let lib_eq_uris, library_equalities, maxm = - find_library_equalities false dbd context (proof, goal') (maxm+2) + Inference.find_library_equalities false dbd context (proof, goal') (maxm+2) in let library_equalities = List.map snd library_equalities 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 _, context, ty = CicUtil.lookup_meta goal' metasenv in - debug_print + Utils.debug_print (lazy (Printf.sprintf "\n\nTRYING TO INFER EQUALITIES MATCHING: %s\n\n" (CicPp.ppterm ty))); @@ -1827,7 +1822,7 @@ let main_demod_equalities dbd term metasenv ugraph = let active = make_active () in let passive = make_passive equalities in Printf.printf "\ncontext:\n%s\n" (PP.ppcontext context); - Printf.printf "\nmetasenv:\n%s\n" (print_metasenv metasenv); + Printf.printf "\nmetasenv:\n%s\n" (Utils.print_metasenv metasenv); Printf.printf "\nequalities:\n%s\n" (String.concat "\n" (List.map @@ -1869,7 +1864,7 @@ let main_demod_equalities dbd term metasenv ugraph = print_newline (); (* with e -> - debug_print (lazy ("EXCEPTION: " ^ (Printexc.to_string e))) + Utils.debug_print (lazy ("EXCEPTION: " ^ (Printexc.to_string e))) *) ;; @@ -1945,6 +1940,7 @@ let rec position_of i x = function * * lists are coded using _ (example: H_H1_H2) *) + let superposition_tac ~target ~table ~subterms_only ~demod_table status = reset_refs(); Indexing.init_index (); @@ -1953,8 +1949,8 @@ let superposition_tac ~target ~table ~subterms_only ~demod_table status = let metano,context,ty = CicUtil.lookup_meta goalno metasenv in let eq_uri,tty = eq_and_ty_of_goal ty in let env = (metasenv, context, CicUniv.empty_ugraph) in - let names = names_of_context context in - let eq_index, equalities, maxm = find_equalities context proof in + let names = Utils.names_of_context context in + let eq_index, equalities, maxm = Inference.find_equalities context proof in let eq_what = let what = find_in_ctx 1 target context in List.nth equalities (position_of 0 what eq_index) -- 2.39.2