From db57b08d789de234c152c3f2a665000311b7335d Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Tue, 25 Oct 2005 14:18:39 +0000 Subject: [PATCH] experimental version --- helm/ocaml/paramodulation/indexing.ml | 98 ++++++++++------ helm/ocaml/paramodulation/inference.ml | 19 ++-- helm/ocaml/paramodulation/inference.mli | 2 +- helm/ocaml/paramodulation/saturate_main.ml | 11 +- helm/ocaml/paramodulation/saturation.ml | 126 ++++++++++++++++++++- 5 files changed, 207 insertions(+), 49 deletions(-) diff --git a/helm/ocaml/paramodulation/indexing.ml b/helm/ocaml/paramodulation/indexing.ml index b748afec7..c964e3a78 100644 --- a/helm/ocaml/paramodulation/indexing.ml +++ b/helm/ocaml/paramodulation/indexing.ml @@ -298,7 +298,7 @@ let rec find_all_matches ?(unif_fun=Inference.unification) returns true if target is subsumed by some equality in table *) let subsumption env table target = - let _, (ty, left, right, _), tmetas, _ = target in + let _, _, (ty, left, right, _), tmetas, _ = target in let metasenv, context, ugraph = env in let metasenv = metasenv @ tmetas in let samesubst subst subst' = @@ -324,14 +324,15 @@ let subsumption env table target = in let rec ok what = function | [] -> false, [] - | (_, subst, menv, ug, ((pos, (_, _, (_, l, r, o), _, _)), _))::tl -> + | (_, subst, menv, ug, ((pos, (_, _, (_, l, r, o), m, _)), _))::tl -> try let other = if pos = Utils.Left then r else l in let subst', menv', ug' = let t1 = Unix.gettimeofday () in try let r = - Inference.matching metasenv context what other ugraph in + Inference.matching (metasenv @ menv @ m) context what other ugraph + in let t2 = Unix.gettimeofday () in match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1); r @@ -348,18 +349,26 @@ let subsumption env table target = ok what tl in let r, subst = ok right leftr in - if r then - true, subst - else - let rightr = - match right with - | Cic.Meta _ -> [] - | _ -> - let rightc = get_candidates Matching table right in - find_all_matches ~unif_fun:Inference.matching - metasenv context ugraph 0 right ty rightc - in - ok left rightr + let r, s = + if r then + true, subst + else + let rightr = + match right with + | Cic.Meta _ -> [] + | _ -> + let rightc = get_candidates Matching table right in + find_all_matches ~unif_fun:Inference.matching + metasenv context ugraph 0 right ty rightc + in + ok left rightr + in + (if r then + debug_print + (lazy + (Printf.sprintf "SUBSUMPTION! %s\n%s\n" + (Inference.string_of_equality target) (Utils.print_subst s)))); + r, s ;; @@ -553,26 +562,47 @@ let rec demodulation_equality newmeta env table sign target = !maxmeta, res in let res = demodulation_aux metasenv' context ugraph table 0 left in - match res with - | Some t -> - let newmeta, newtarget = build_newtarget true t in - if (Inference.is_identity (metasenv', context, ugraph) newtarget) || - (Inference.meta_convertibility_eq target newtarget) then - newmeta, newtarget - else - demodulation_equality newmeta env table sign newtarget - | None -> - let res = demodulation_aux metasenv' context ugraph table 0 right in - match res with - | Some t -> - let newmeta, newtarget = build_newtarget false t in - if (Inference.is_identity (metasenv', context, ugraph) newtarget) || + let newmeta, newtarget = + match res with + | Some t -> + let newmeta, newtarget = build_newtarget true t in + if (Inference.is_identity (metasenv', context, ugraph) newtarget) || (Inference.meta_convertibility_eq target newtarget) then - newmeta, newtarget - else - demodulation_equality newmeta env table sign newtarget - | None -> - newmeta, target + newmeta, newtarget + else + demodulation_equality newmeta env table sign newtarget + | None -> + let res = demodulation_aux metasenv' context ugraph table 0 right in + match res with + | Some t -> + let newmeta, newtarget = build_newtarget false t in + if (Inference.is_identity (metasenv', context, ugraph) newtarget) || + (Inference.meta_convertibility_eq target newtarget) then + newmeta, newtarget + else + demodulation_equality newmeta env table sign newtarget + | None -> + newmeta, target + in + (* newmeta, newtarget *) + (* tentiamo di ridurre usando CicReduction.normalize *) + let w, p, (ty, left, right, o), m, a = newtarget in + let left' = ProofEngineReduction.simpl context left in + let right' = ProofEngineReduction.simpl context right in + let newleft = + if !Utils.compare_terms left' left = Utils.Lt then left' else left in + let newright = + if !Utils.compare_terms right' right = Utils.Lt then right' else right in + if newleft != left || newright != right then ( + debug_print + (lazy + (Printf.sprintf "left: %s, left': %s\nright: %s, right': %s\n" + (CicPp.ppterm left) (CicPp.ppterm left') (CicPp.ppterm right) + (CicPp.ppterm right'))) + ); + let w' = Utils.compute_equality_weight ty newleft newright in + let o' = !Utils.compare_terms newleft newright in + newmeta, (w', p, (ty, newleft, newright, o'), m, a) ;; diff --git a/helm/ocaml/paramodulation/inference.ml b/helm/ocaml/paramodulation/inference.ml index b9f165edb..105b708e9 100644 --- a/helm/ocaml/paramodulation/inference.ml +++ b/helm/ocaml/paramodulation/inference.ml @@ -449,7 +449,7 @@ let unification metasenv context t1 t2 ugraph = ;; -(* let unification = CicUnification.fo_unif;; *) +let unification = CicUnification.fo_unif;; exception MatchingFailure;; @@ -590,6 +590,7 @@ let find_equalities context proof = ;; +(* let equations_blacklist = List.fold_left (fun s u -> UriManager.UriSet.add (UriManager.uri_of_string u) s) @@ -622,6 +623,9 @@ let equations_blacklist = "cic:/matita/logic/equality/eq_rect.con"; ] ;; +*) +let equations_blacklist = UriManager.UriSet.empty;; + let find_library_equalities dbd context status maxmeta = let module C = Cic in @@ -724,13 +728,13 @@ let find_library_equalities dbd context status maxmeta = let uriset, eqlist = (List.fold_left (fun (s, l) (u, e) -> - if List.exists (meta_convertibility_eq e) l then ( + if List.exists (meta_convertibility_eq e) (List.map snd l) then ( debug_print (lazy (Printf.sprintf "NO!! %s already there!" (string_of_equality e))); (UriManager.UriSet.add u s, l) - ) else (UriManager.UriSet.add u s, e::l)) + ) else (UriManager.UriSet.add u s, (u, e)::l)) (UriManager.UriSet.empty, []) found) in uriset, eqlist, maxm @@ -911,9 +915,10 @@ let equality_of_term proof term = type environment = Cic.metasenv * Cic.context * CicUniv.universe_graph;; -let is_identity ((_, context, ugraph) as env) = function - | ((_, _, (ty, left, right, _), _, _) as equality) -> +let is_identity ((metasenv, context, ugraph) as env) = function + | ((_, _, (ty, left, right, _), menv, _) as equality) -> (left = right || - (meta_convertibility left right) || - (fst (CicReduction.are_convertible context left right ugraph))) + (* (meta_convertibility left right) || *) + (fst (CicReduction.are_convertible + ~metasenv:(metasenv @ menv) context left right ugraph))) ;; diff --git a/helm/ocaml/paramodulation/inference.mli b/helm/ocaml/paramodulation/inference.mli index f2b7073d1..55f3df414 100644 --- a/helm/ocaml/paramodulation/inference.mli +++ b/helm/ocaml/paramodulation/inference.mli @@ -84,7 +84,7 @@ val find_equalities: *) val find_library_equalities: HMysql.dbd -> Cic.context -> ProofEngineTypes.status -> int -> - UriManager.UriSet.t * equality list * int + UriManager.UriSet.t * (UriManager.uri * equality) list * int (** searches the library for theorems that are not equalities (returned by the diff --git a/helm/ocaml/paramodulation/saturate_main.ml b/helm/ocaml/paramodulation/saturate_main.ml index efcc3a2d8..ce4182e1a 100644 --- a/helm/ocaml/paramodulation/saturate_main.ml +++ b/helm/ocaml/paramodulation/saturate_main.ml @@ -42,6 +42,8 @@ let get_from_user ~(dbd:HMysql.dbd) = let full = ref false;; +let retrieve_only = ref false;; + let _ = let module S = Saturation in let set_ratio v = S.weight_age_ratio := v; S.weight_age_counter := v @@ -58,6 +60,7 @@ let _ = and set_width w = S.maxwidth := w and set_depth d = S.maxdepth := d and set_full () = full := true + and set_retrieve () = retrieve_only := true in Arg.parse [ "-full", Arg.Unit set_full, "Enable full mode"; @@ -84,6 +87,8 @@ let _ = "-d", Arg.Int set_depth, Printf.sprintf "Maximal depth (default: %d)" !Saturation.maxdepth; + + "-retrieve", Arg.Unit set_retrieve, "retrieve only"; ] (fun a -> ()) "Usage:" in Helm_registry.load_from !configuration_file; @@ -96,4 +101,8 @@ let dbd = HMysql.quick_connect () in let term, metasenv, ugraph = get_from_user ~dbd in -Saturation.main dbd !full term metasenv ugraph;; +if !retrieve_only then + Saturation.retrieve_and_print dbd term metasenv ugraph +else + Saturation.main dbd !full term metasenv ugraph +;; diff --git a/helm/ocaml/paramodulation/saturation.ml b/helm/ocaml/paramodulation/saturation.ml index c0a7ec611..8e67bc7a0 100644 --- a/helm/ocaml/paramodulation/saturation.ml +++ b/helm/ocaml/paramodulation/saturation.ml @@ -486,7 +486,19 @@ let forward_simplify env (sign, current) ?passive (active_list, active_table) = maxmeta := newmeta; if is_identity env newcurrent then if sign = Negative then Some (sign, newcurrent) - else None + else ( +(* debug_print *) +(* (lazy *) +(* (Printf.sprintf "\ncurrent was: %s\nnewcurrent is: %s\n" *) +(* (string_of_equality current) *) +(* (string_of_equality newcurrent))); *) +(* debug_print *) +(* (lazy *) +(* (Printf.sprintf "active is: %s" *) +(* (String.concat "\n" *) +(* (List.map (fun (_, e) -> (string_of_equality e)) active_list)))); *) + None + ) else Some (sign, newcurrent) in @@ -513,10 +525,18 @@ let forward_simplify env (sign, current) ?passive (active_list, active_table) = None else match passive_table with - | None -> res + | None -> + if fst (Indexing.subsumption env active_table c) then + None + else + res | Some passive_table -> if Indexing.in_index passive_table c then None - else res + else + let r1, _ = Indexing.subsumption env active_table c in + if r1 then None else + let r2, _ = Indexing.subsumption env passive_table c in + if r2 then None else res ;; type fs_time_info_t = { @@ -598,7 +618,7 @@ let forward_simplify_new env (new_neg, new_pos) ?passive active = not ((Indexing.in_index active_table e) || (Indexing.in_index passive_table e))) in - new_neg, List.filter is_duplicate new_pos + new_neg, List.filter subs (List.filter is_duplicate new_pos) ;; @@ -1693,6 +1713,7 @@ let main dbd full term metasenv ugraph = let lib_eq_uris, library_equalities, maxm = 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 = @@ -1789,8 +1810,8 @@ let main dbd full term metasenv ugraph = Printf.printf "\nequalities:\n%s\n" (String.concat "\n" (List.map - (string_of_equality ~env) - (equalities @ library_equalities))); + (string_of_equality ~env) equalities)); +(* (equalities @ library_equalities))); *) print_endline "--------------------------------------------------"; let start = Unix.gettimeofday () in print_endline "GO!"; @@ -1912,6 +1933,7 @@ let saturate let lib_eq_uris, library_equalities, maxm = find_library_equalities dbd context (proof, goal') (maxm+2) in + let library_equalities = List.map snd library_equalities in let t2 = Unix.gettimeofday () in maxmeta := maxm+2; let equalities = @@ -2069,3 +2091,95 @@ if connect_to_auto then ( AutoTactic.term_is_equality := Inference.term_is_equality; );; + +let retrieve_and_print dbd term metasenv ugraph = + let module C = Cic in + let module T = CicTypeChecker in + let module PET = ProofEngineTypes in + let module PP = CicPp in + let proof = None, (1, [], term)::metasenv, C.Meta (1, []), term in + let status = PET.apply_tactic (PrimitiveTactics.intros_tac ()) (proof, 1) in + let proof, goals = status in + let goal' = List.nth goals 0 in + let uri, metasenv, meta_proof, term_to_prove = proof in + let _, context, goal = CicUtil.lookup_meta goal' metasenv in + let eq_indexes, equalities, maxm = find_equalities context proof in + let new_meta_goal, metasenv, type_of_goal = + let irl = + CicMkImplicit.identity_relocation_list_for_metavariable context in + let _, context, ty = CicUtil.lookup_meta goal' metasenv in + debug_print + (lazy (Printf.sprintf "\n\nTIPO DEL GOAL: %s\n" (CicPp.ppterm ty))); + Cic.Meta (maxm+1, irl), + (maxm+1, context, ty)::metasenv, + ty + in + let ugraph = CicUniv.empty_ugraph in + let env = (metasenv, context, ugraph) in + let goal = Inference.BasicProof new_meta_goal, [], goal in + let t1 = Unix.gettimeofday () in + let lib_eq_uris, library_equalities, maxm = + find_library_equalities dbd context (proof, goal') (maxm+2) + in + let t2 = Unix.gettimeofday () in + maxmeta := maxm+2; + let equalities = + let equalities = (* equalities @ *) library_equalities in + debug_print + (lazy + (Printf.sprintf "\n\nequalities:\n%s\n" + (String.concat "\n" + (List.map + (fun (u, e) -> +(* Printf.sprintf "%s: %s" *) + (UriManager.string_of_uri u) +(* (string_of_equality e) *) + ) + equalities)))); + debug_print (lazy "SIMPLYFYING EQUALITIES..."); + let rec simpl e others others_simpl = + let (u, e) = e in + let active = List.map (fun (u, e) -> (Positive, e)) + (others @ others_simpl) in + let tbl = + List.fold_left + (fun t (_, e) -> Indexing.index t e) + (Indexing.empty_table ()) active + in + let res = forward_simplify env (Positive, e) (active, tbl) in + match others with + | hd::tl -> ( + match res with + | None -> simpl hd tl others_simpl + | Some e -> simpl hd tl ((u, (snd e))::others_simpl) + ) + | [] -> ( + match res with + | None -> others_simpl + | Some e -> (u, (snd e))::others_simpl + ) + in + match equalities with + | [] -> [] + | hd::tl -> + let others = tl in (* List.map (fun e -> (Positive, e)) tl in *) + let res = + List.rev (simpl (*(Positive,*) hd others []) + in + debug_print + (lazy + (Printf.sprintf "\nequalities AFTER:\n%s\n" + (String.concat "\n" + (List.map + (fun (u, e) -> + Printf.sprintf "%s: %s" + (UriManager.string_of_uri u) + (string_of_equality e) + ) + res)))); + res + in + debug_print + (lazy + (Printf.sprintf "Time to retrieve equalities: %.9f\n" (t2 -. t1))) +;; -- 2.39.2