X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fparamodulation%2Findexing.ml;h=8c41375565652266966189d1d068d7b3bba437c2;hb=b52f57d8573a909a486d52a7317e017f56d07199;hp=b748afec7357c55270d9ec38fb6a67752be70b28;hpb=b6bec181b81b3cbc56ec8914dcd7e6a029c7d84f;p=helm.git diff --git a/helm/ocaml/paramodulation/indexing.ml b/helm/ocaml/paramodulation/indexing.ml index b748afec7..8c4137556 100644 --- a/helm/ocaml/paramodulation/indexing.ml +++ b/helm/ocaml/paramodulation/indexing.ml @@ -23,6 +23,15 @@ * http://cs.unibo.it/helm/. *) +module OrderedPosEquality = struct + type t = Utils.pos * Inference.equality + let compare = Pervasives.compare + end + +module PosEqSet = Set.Make(OrderedPosEquality);; + +module DT = Discrimination_tree.DiscriminationTreeIndexing(PosEqSet);; + let debug_print = Utils.debug_print;; @@ -53,8 +62,6 @@ let indexing_retrieval_time = ref 0.;; let apply_subst = CicMetaSubst.apply_subst - - (* (* NO INDEXING *) let init_index () = () @@ -90,8 +97,16 @@ let empty_table () = ;; let index = Path_indexing.index -and remove_index = Path_indexing.remove_index -and in_index = Path_indexing.in_index;; +let remove_index tree equality = + let _, _, (_, l, r, ordering), _, _ = equality in + match ordering with + | Utils.Gt -> DT.remove_index tree l equality + | Utils.Lt -> DT.remove_index tree r equality + | _ -> + DT.remove_index (DT.remove_index tree r equality) l equality + + +let in_index = Path_indexing.in_index;; let get_candidates mode trie term = let t1 = Unix.gettimeofday () in @@ -111,31 +126,66 @@ let get_candidates mode trie term = ;; *) - (* DISCRIMINATION TREES *) let init_index () = - Hashtbl.clear Discrimination_tree.arities; + Hashtbl.clear DT.arities; ;; let empty_table () = - Discrimination_tree.DiscriminationTree.empty + DT.empty ;; -let index = Discrimination_tree.index -and remove_index = Discrimination_tree.remove_index -and in_index = Discrimination_tree.in_index;; +let remove_index tree equality = + let _, _, (_, l, r, ordering), _, _ = equality in + match ordering with + | Utils.Gt -> DT.remove_index tree l (Utils.Left, equality) + | Utils.Lt -> DT.remove_index tree r (Utils.Right, equality) + | _ -> + let tree = DT.remove_index tree r (Utils.Right, equality) in + DT.remove_index tree l (Utils.Left, equality) + +let index tree equality = + let _, _, (_, l, r, ordering), _, _ = equality in + match ordering with + | Utils.Gt -> DT.index tree l (Utils.Left, equality) + | Utils.Lt -> DT.index tree r (Utils.Right, equality) + | _ -> + let tree = DT.index tree r (Utils.Right, equality) in + DT.index tree l (Utils.Left, equality) + + +let in_index tree equality = + let _, _, (_, l, r, ordering), _, _ = equality in + let meta_convertibility (pos,equality') = + Inference.meta_convertibility_eq equality equality' + in + DT.in_index tree l meta_convertibility || DT.in_index tree r meta_convertibility + + +(* returns a list of all the equalities in the tree that are in relation + "mode" with the given term, where mode can be either Matching or + Unification. + Format of the return value: list of tuples in the form: + (position - Left or Right - of the term that matched the given one in this + equality, + equality found) + + Note that if equality is "left = right", if the ordering is left > right, + the position will always be Left, and if the ordering is left < right, + position will be Right. +*) let get_candidates mode tree term = let t1 = Unix.gettimeofday () in let res = let s = match mode with - | Matching -> Discrimination_tree.retrieve_generalizations tree term - | Unification -> Discrimination_tree.retrieve_unifiables tree term + | Matching -> DT.retrieve_generalizations tree term + | Unification -> DT.retrieve_unifiables tree term in - Discrimination_tree.PosEqSet.elements s + PosEqSet.elements s in -(* print_candidates mode term res; *) + (* print_candidates mode term res; *) (* print_endline (Discrimination_tree.string_of_discrimination_tree tree); *) (* print_newline (); *) let t2 = Unix.gettimeofday () in @@ -153,6 +203,22 @@ let match_unif_time_no = ref 0.;; termty can be Implicit if it is not needed. The result (one of the sides of the equality, actually) should be not greater (wrt the term ordering) than term + + Format of the return value: + + (term to substitute, [Cic.Rel 1 properly lifted - see the various + build_newtarget functions inside the various + demodulation_* functions] + substitution used for the matching, + metasenv, + ugraph, [substitution, metasenv and ugraph have the same meaning as those + returned by CicUnification.fo_unif] + (equality where the matching term was found, [i.e. the equality to use as + rewrite rule] + uri [either eq_ind_URI or eq_ind_r_URI, depending on the direction of + the equality: this is used to build the proof term, again see one of + the build_newtarget functions] + )) *) let rec find_matches metasenv context ugraph lift_amount term termty = let module C = Cic in @@ -204,8 +270,8 @@ let rec find_matches metasenv context ugraph lift_amount term termty = in match res with | Some (_, s, _, _, _) -> - let c' = apply_subst s c - and other' = apply_subst s other in + let c' = apply_subst s c in + let other' = U.guarded_simpl context (apply_subst s other) in let order = cmp c' other' in let names = U.names_of_context context in if order = U.Gt then @@ -298,7 +364,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 +390,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 +415,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 ;; @@ -463,6 +538,7 @@ let rec demodulation_equality newmeta env table sign target = let module S = CicSubstitution in let module M = CicMetaSubst in let module HL = HelmLibraryObjects in + let module U = Utils in let metasenv, context, ugraph = env in let _, proof, (eq_ty, left, right, order), metas, args = target in let metasenv' = metasenv @ metas in @@ -479,7 +555,7 @@ let rec demodulation_equality newmeta env table sign target = in let what, other = if pos = Utils.Left then what, other else other, what in let newterm, newproof = - let bo = apply_subst subst (S.subst other t) in + let bo = U.guarded_simpl context (apply_subst subst (S.subst other t)) in let name = C.Name ("x_Demod_" ^ (string_of_int !demod_counter)) in incr demod_counter; let bo' = @@ -496,8 +572,8 @@ let rec demodulation_equality newmeta env table sign target = incr maxmeta; let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in - debug_print (lazy (Printf.sprintf "\nADDING META: %d\n" !maxmeta)); - print_newline (); +(* debug_print (lazy (Printf.sprintf "\nADDING META: %d\n" !maxmeta)); *) +(* print_newline (); *) C.Meta (!maxmeta, irl) in let eq_found = @@ -553,26 +629,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) ;; @@ -723,14 +820,14 @@ let superposition_left newmeta (metasenv, context, ugraph) table target = let maxmeta = ref newmeta in let build_new (bo, s, m, ug, (eq_found, eq_URI)) = - debug_print (lazy "\nSUPERPOSITION LEFT\n"); +(* debug_print (lazy "\nSUPERPOSITION LEFT\n"); *) let time1 = Unix.gettimeofday () in let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in let what, other = if pos = Utils.Left then what, other else other, what in let newgoal, newproof = - let bo' = apply_subst s (S.subst other bo) in + let bo' = U.guarded_simpl context (apply_subst s (S.subst other bo)) in let name = C.Name ("x_SupL_" ^ (string_of_int !sup_l_counter)) in incr sup_l_counter; let bo'' = @@ -765,10 +862,10 @@ let superposition_left newmeta (metasenv, context, ugraph) table target = in match proof with | Inference.BasicProof _ -> - debug_print (lazy "replacing a BasicProof"); +(* debug_print (lazy "replacing a BasicProof"); *) pb | Inference.ProofGoalBlock (_, parent_proof) -> - debug_print (lazy "replacing another ProofGoalBlock"); +(* debug_print (lazy "replacing another ProofGoalBlock"); *) Inference.ProofGoalBlock (pb, parent_proof) | _ -> assert false in @@ -913,7 +1010,7 @@ let rec demodulation_goal newmeta env table goal = incr maxmeta; let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in - debug_print (lazy (Printf.sprintf "\nADDING META: %d\n" !maxmeta)); +(* debug_print (lazy (Printf.sprintf "\nADDING META: %d\n" !maxmeta)); *) C.Meta (!maxmeta, irl) in let eq_found = @@ -936,19 +1033,19 @@ let rec demodulation_goal newmeta env table goal = in let rec repl = function | Inference.NoProof -> - debug_print (lazy "replacing a NoProof"); +(* debug_print (lazy "replacing a NoProof"); *) pb | Inference.BasicProof _ -> - debug_print (lazy "replacing a BasicProof"); +(* debug_print (lazy "replacing a BasicProof"); *) pb | Inference.ProofGoalBlock (_, parent_proof) -> - debug_print (lazy "replacing another ProofGoalBlock"); +(* debug_print (lazy "replacing another ProofGoalBlock"); *) Inference.ProofGoalBlock (pb, parent_proof) | (Inference.SubProof (term, meta_index, p) as subproof) -> - debug_print - (lazy - (Printf.sprintf "replacing %s" - (Inference.string_of_proof subproof))); +(* debug_print *) +(* (lazy *) +(* (Printf.sprintf "replacing %s" *) +(* (Inference.string_of_proof subproof))); *) Inference.SubProof (term, meta_index, repl p) | _ -> assert false in repl proof