X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fparamodulation%2Fsaturation.ml;h=8e67bc7a05cee8147a2f0a774f56f0fe7073d12e;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=c0a7ec61180450d9e1633f4001bac144d7fbdc38;hpb=8b55faddb06e3c4b0a13839210bb49170939b33e;p=helm.git 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))) +;;