From: Andrea Asperti Date: Mon, 19 Dec 2005 16:03:29 +0000 (+0000) Subject: moved term indexing (in both discrimination and path tree forms) from paramodulation... X-Git-Tag: make_still_working~7983 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=20ea4afc703668c1c643aaf81d62aeae51be36a1;p=helm.git moved term indexing (in both discrimination and path tree forms) from paramodulation/ to cic/ --- diff --git a/helm/ocaml/cic/.depend b/helm/ocaml/cic/.depend index 58a8c3bed..a35156331 100644 --- a/helm/ocaml/cic/.depend +++ b/helm/ocaml/cic/.depend @@ -4,6 +4,7 @@ cicParser.cmi: cic.cmo cicUtil.cmi: cic.cmo helmLibraryObjects.cmi: cic.cmo discrimination_tree.cmi: cic.cmo +path_indexing.cmi: cic.cmo cic.cmo: cicUniv.cmi cic.cmx: cicUniv.cmx unshare.cmo: cic.cmo unshare.cmi @@ -22,3 +23,5 @@ libraryObjects.cmo: helmLibraryObjects.cmi libraryObjects.cmi libraryObjects.cmx: helmLibraryObjects.cmx libraryObjects.cmi discrimination_tree.cmo: cic.cmo discrimination_tree.cmi discrimination_tree.cmx: cic.cmx discrimination_tree.cmi +path_indexing.cmo: cic.cmo path_indexing.cmi +path_indexing.cmx: cic.cmx path_indexing.cmi diff --git a/helm/ocaml/cic/Makefile b/helm/ocaml/cic/Makefile index a0cfe0daa..4e36af019 100644 --- a/helm/ocaml/cic/Makefile +++ b/helm/ocaml/cic/Makefile @@ -9,7 +9,8 @@ INTERFACE_FILES = \ cicUtil.mli \ helmLibraryObjects.mli \ libraryObjects.mli \ - discrimination_tree.mli + discrimination_tree.mli \ + path_indexing.mli IMPLEMENTATION_FILES = \ cic.ml $(INTERFACE_FILES:%.mli=%.ml) EXTRA_OBJECTS_TO_INSTALL = cic.ml cic.cmi diff --git a/helm/ocaml/cic/discrimination_tree.ml b/helm/ocaml/cic/discrimination_tree.ml index fd234df98..6e2529016 100644 --- a/helm/ocaml/cic/discrimination_tree.ml +++ b/helm/ocaml/cic/discrimination_tree.ml @@ -23,7 +23,7 @@ * http://cs.unibo.it/helm/. *) -module DiscriminationTreeIndexing = +module DiscriminationTreeIndexing = functor (A:Set.S) -> struct @@ -59,7 +59,6 @@ module DiscriminationTreeIndexing = module DiscriminationTree = Trie.Make(PSMap);; type t = A.t DiscriminationTree.t - type elt = A.elt let empty = DiscriminationTree.empty (* diff --git a/helm/ocaml/cic/discrimination_tree.mli b/helm/ocaml/cic/discrimination_tree.mli index 5c5e6f05d..61631f478 100644 --- a/helm/ocaml/cic/discrimination_tree.mli +++ b/helm/ocaml/cic/discrimination_tree.mli @@ -26,20 +26,16 @@ module DiscriminationTreeIndexing : functor (A : Set.S) -> sig - type path_string_elem = Cic.term - type path_string = path_string_elem list val arities : (Cic.term, int) Hashtbl.t - val path_string_of_term : Cic.term -> Cic.term list type key = Cic.term type t - type elt = A.elt val empty : t - val index : t -> Cic.term -> A.elt -> t - val remove_index : t -> Cic.term -> A.elt -> t - val in_index : t -> Cic.term -> (A.elt -> bool) -> bool + val index : t -> key -> A.elt -> t + val remove_index : t -> key -> A.elt -> t + val in_index : t -> key -> (A.elt -> bool) -> bool val retrieve_generalizations : t -> key -> A.t val retrieve_unifiables : t -> key -> A.t end diff --git a/helm/ocaml/cic/path_indexing.ml b/helm/ocaml/cic/path_indexing.ml new file mode 100644 index 000000000..81c3583e1 --- /dev/null +++ b/helm/ocaml/cic/path_indexing.ml @@ -0,0 +1,225 @@ +(* Copyright (C) 2005, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +(* path indexing implementation *) + +(* position of the subterm, subterm (Appl are not stored...) *) + +module PathIndexing = + functor(A:Set.S) -> + struct + +type path_string_elem = Index of int | Term of Cic.term;; +type path_string = path_string_elem list;; + + +let rec path_strings_of_term index = + let module C = Cic in function + | C.Meta _ -> [ [Index index; Term (C.Implicit None)] ] + | C.Appl (hd::tl) -> + let p = if index > 0 then [Index index; Term hd] else [Term hd] in + let _, res = + List.fold_left + (fun (i, r) t -> + let rr = path_strings_of_term i t in + (i+1, r @ (List.map (fun ps -> p @ ps) rr))) + (1, []) tl + in + res + | term -> [ [Index index; Term term] ] +;; + +(* +let string_of_path_string ps = + String.concat "." + (List.map + (fun e -> + let s = + match e with + | Index i -> "Index " ^ (string_of_int i) + | Term t -> "Term " ^ (CicPp.ppterm t) + in + "(" ^ s ^ ")") + ps) +;; +*) + +module OrderedPathStringElement = struct + type t = path_string_elem + + let compare t1 t2 = + match t1, t2 with + | Index i, Index j -> Pervasives.compare i j + | Term t1, Term t2 -> if t1 = t2 then 0 else Pervasives.compare t1 t2 + | Index _, Term _ -> -1 + | Term _, Index _ -> 1 +end + +module PSMap = Map.Make(OrderedPathStringElement);; + +module PSTrie = Trie.Make(PSMap);; + +type t = A.t PSTrie.t +type key = Cic.term +let empty = PSTrie.empty +let arities = Hashtbl.create 0 + +let index trie term info = + let ps = path_strings_of_term 0 term in + List.fold_left + (fun trie ps -> + let ps_set = try PSTrie.find ps trie with Not_found -> A.empty in + let trie = PSTrie.add ps (A.add info ps_set) trie in + trie) trie ps + +let remove_index trie term info= + let ps = path_strings_of_term 0 term in + List.fold_left + (fun trie ps -> + try + let ps_set = A.remove info (PSTrie.find ps trie) in + if A.is_empty ps_set then + PSTrie.remove ps trie + else + PSTrie.add ps ps_set trie + with Not_found -> trie) trie ps +;; + +let in_index trie term test = + let ps = path_strings_of_term 0 term in + let ok ps = + try + let set = PSTrie.find ps trie in + A.exists test set + with Not_found -> + false + in + List.exists ok ps +;; + + +let head_of_term = function + | Cic.Appl (hd::tl) -> hd + | term -> term +;; + + +let subterm_at_pos index term = + if index = 0 then + term + else + match term with + | Cic.Appl l -> + (try List.nth l index with Failure _ -> raise Not_found) + | _ -> raise Not_found +;; + + +let rec retrieve_generalizations trie term = + match trie with + | PSTrie.Node (value, map) -> + let res = + match term with + | Cic.Meta _ -> A.empty + | term -> + let hd_term = head_of_term term in + try + let n = PSMap.find (Term hd_term) map in + match n with + | PSTrie.Node (Some s, _) -> s + | PSTrie.Node (None, m) -> + let l = + PSMap.fold + (fun k v res -> + match k with + | Index i -> + let t = subterm_at_pos i term in + let s = retrieve_generalizations v t in + s::res + | _ -> res) + m [] + in + match l with + | hd::tl -> + List.fold_left (fun r s -> A.inter r s) hd tl + | _ -> A.empty + with Not_found -> + A.empty + in + try + let n = PSMap.find (Term (Cic.Implicit None)) map in + match n with + | PSTrie.Node (Some s, _) -> A.union res s + | _ -> res + with Not_found -> + res +;; + + +let rec retrieve_unifiables trie term = + match trie with + | PSTrie.Node (value, map) -> + let res = + match term with + | Cic.Meta _ -> + PSTrie.fold + (fun ps v res -> A.union res v) + (PSTrie.Node (None, map)) + A.empty + | _ -> + let hd_term = head_of_term term in + try + let n = PSMap.find (Term hd_term) map in + match n with + | PSTrie.Node (Some v, _) -> v + | PSTrie.Node (None, m) -> + let l = + PSMap.fold + (fun k v res -> + match k with + | Index i -> + let t = subterm_at_pos i term in + let s = retrieve_unifiables v t in + s::res + | _ -> res) + m [] + in + match l with + | hd::tl -> + List.fold_left (fun r s -> A.inter r s) hd tl + | _ -> A.empty + with Not_found -> + A.empty + in + try + let n = PSMap.find (Term (Cic.Implicit None)) map in + match n with + | PSTrie.Node (Some s, _) -> A.union res s + | _ -> res + with Not_found -> + res +;; + +end diff --git a/helm/ocaml/cic/path_indexing.mli b/helm/ocaml/cic/path_indexing.mli new file mode 100644 index 000000000..899901618 --- /dev/null +++ b/helm/ocaml/cic/path_indexing.mli @@ -0,0 +1,42 @@ +(* Copyright (C) 2005, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +module PathIndexing : + functor (A : Set.S) -> + sig + val arities : (Cic.term, int) Hashtbl.t + + type key = Cic.term + type t + + val empty : t + val index : t -> key -> A.elt -> t + val remove_index : t -> key -> A.elt -> t + val in_index : t -> key -> (A.elt -> bool) -> bool + val retrieve_generalizations : t -> key -> A.t + val retrieve_unifiables : t -> key -> A.t + end + + diff --git a/helm/ocaml/paramodulation/.depend b/helm/ocaml/paramodulation/.depend index ec3ba7d6c..7c6673bad 100644 --- a/helm/ocaml/paramodulation/.depend +++ b/helm/ocaml/paramodulation/.depend @@ -1,11 +1,12 @@ inference.cmi: utils.cmi +equality_indexing.cmi: utils.cmi inference.cmi utils.cmo: utils.cmi utils.cmx: utils.cmi inference.cmo: utils.cmi inference.cmi inference.cmx: utils.cmx inference.cmi -path_indexing.cmo: utils.cmi inference.cmi -path_indexing.cmx: utils.cmx inference.cmx -indexing.cmo: utils.cmi inference.cmi -indexing.cmx: utils.cmx inference.cmx +equality_indexing.cmo: utils.cmi inference.cmi equality_indexing.cmi +equality_indexing.cmx: utils.cmx inference.cmx equality_indexing.cmi +indexing.cmo: utils.cmi inference.cmi equality_indexing.cmi +indexing.cmx: utils.cmx inference.cmx equality_indexing.cmx saturation.cmo: utils.cmi inference.cmi indexing.cmo saturation.cmx: utils.cmx inference.cmx indexing.cmx diff --git a/helm/ocaml/paramodulation/Makefile b/helm/ocaml/paramodulation/Makefile index 683bac671..854621090 100644 --- a/helm/ocaml/paramodulation/Makefile +++ b/helm/ocaml/paramodulation/Makefile @@ -2,10 +2,10 @@ PACKAGE = paramodulation INTERFACE_FILES = \ utils.mli \ - inference.mli + inference.mli\ + equality_indexing.mli IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml) \ - path_indexing.ml \ indexing.ml \ saturation.ml diff --git a/helm/ocaml/paramodulation/equality_indexing.ml b/helm/ocaml/paramodulation/equality_indexing.ml new file mode 100644 index 000000000..fd3fa5c32 --- /dev/null +++ b/helm/ocaml/paramodulation/equality_indexing.ml @@ -0,0 +1,129 @@ +(* Copyright (C) 2005, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +module type EqualityIndex = + sig + module PosEqSet : Set.S with type elt = Utils.pos * Inference.equality + val arities : (Cic.term, int) Hashtbl.t + type key = Cic.term + type t = Discrimination_tree.DiscriminationTreeIndexing(PosEqSet).t + val empty : t + val retrieve_generalizations : t -> key -> PosEqSet.t + val retrieve_unifiables : t -> key -> PosEqSet.t + val init_index : unit -> unit + val remove_index : t -> Inference.equality -> t + val index : t -> Inference.equality -> t + val in_index : t -> Inference.equality -> bool + end + +module DT = +struct + module OrderedPosEquality = struct + type t = Utils.pos * Inference.equality + let compare = Pervasives.compare + end + + module PosEqSet = Set.Make(OrderedPosEquality);; + + include Discrimination_tree.DiscriminationTreeIndexing(PosEqSet) + + + (* DISCRIMINATION TREES *) + let init_index () = + Hashtbl.clear arities; + ;; + + let remove_index tree equality = + let _, _, (_, l, r, ordering), _, _ = equality in + match ordering with + | Utils.Gt -> remove_index tree l (Utils.Left, equality) + | Utils.Lt -> remove_index tree r (Utils.Right, equality) + | _ -> + let tree = remove_index tree r (Utils.Right, equality) in + remove_index tree l (Utils.Left, equality) + + let index tree equality = + let _, _, (_, l, r, ordering), _, _ = equality in + match ordering with + | Utils.Gt -> index tree l (Utils.Left, equality) + | Utils.Lt -> index tree r (Utils.Right, equality) + | _ -> + let tree = index tree r (Utils.Right, equality) in + 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 + in_index tree l meta_convertibility || in_index tree r meta_convertibility + + end + +module PT = + struct + module OrderedPosEquality = struct + type t = Utils.pos * Inference.equality + let compare = Pervasives.compare + end + + module PosEqSet = Set.Make(OrderedPosEquality);; + + include Discrimination_tree.DiscriminationTreeIndexing(PosEqSet) + + + (* DISCRIMINATION TREES *) + let init_index () = + Hashtbl.clear arities; + ;; + + let remove_index tree equality = + let _, _, (_, l, r, ordering), _, _ = equality in + match ordering with + | Utils.Gt -> remove_index tree l (Utils.Left, equality) + | Utils.Lt -> remove_index tree r (Utils.Right, equality) + | _ -> + let tree = remove_index tree r (Utils.Right, equality) in + remove_index tree l (Utils.Left, equality) + + let index tree equality = + let _, _, (_, l, r, ordering), _, _ = equality in + match ordering with + | Utils.Gt -> index tree l (Utils.Left, equality) + | Utils.Lt -> index tree r (Utils.Right, equality) + | _ -> + let tree = index tree r (Utils.Right, equality) in + 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 + in_index tree l meta_convertibility || in_index tree r meta_convertibility +end + diff --git a/helm/ocaml/paramodulation/equality_indexing.mli b/helm/ocaml/paramodulation/equality_indexing.mli new file mode 100644 index 000000000..d7c3bec5e --- /dev/null +++ b/helm/ocaml/paramodulation/equality_indexing.mli @@ -0,0 +1,43 @@ +(* Copyright (C) 2005, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.cs.unibo.it/ + *) + +module type EqualityIndex = + sig + module PosEqSet : Set.S with type elt = Utils.pos * Inference.equality + val arities : (Cic.term, int) Hashtbl.t + type key = Cic.term + type t = Discrimination_tree.DiscriminationTreeIndexing(PosEqSet).t + val empty : t + val retrieve_generalizations : t -> key -> PosEqSet.t + val retrieve_unifiables : t -> key -> PosEqSet.t + val init_index : unit -> unit + val remove_index : t -> Inference.equality -> t + val index : t -> Inference.equality -> t + val in_index : t -> Inference.equality -> bool + end + +module DT : EqualityIndex +module PT : EqualityIndex + diff --git a/helm/ocaml/paramodulation/indexing.ml b/helm/ocaml/paramodulation/indexing.ml index 8c4137556..523cff882 100644 --- a/helm/ocaml/paramodulation/indexing.ml +++ b/helm/ocaml/paramodulation/indexing.ml @@ -23,21 +23,16 @@ * 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);; +module Index = Equality_indexing.DT (* discrimination tree based indexing *) +(* +module Index = Equality_indexing.DT (* path tree based indexing *) +*) let debug_print = Utils.debug_print;; type retrieval_mode = Matching | Unification;; - let print_candidates mode term res = let _ = match mode with @@ -62,105 +57,11 @@ let indexing_retrieval_time = ref 0.;; let apply_subst = CicMetaSubst.apply_subst -(* -(* NO INDEXING *) -let init_index () = () - -let empty_table () = [] - -let index table equality = - let _, _, (_, l, r, ordering), _, _ = equality in - match ordering with - | Utils.Gt -> (Utils.Left, equality)::table - | Utils.Lt -> (Utils.Right, equality)::table - | _ -> (Utils.Left, equality)::(Utils.Right, equality)::table -;; - -let remove_index table equality = - List.filter (fun (p, e) -> e != equality) table -;; - -let in_index table equality = - List.exists (fun (p, e) -> e == equality) table -;; - -let get_candidates mode table term = table -*) - - -(* -(* PATH INDEXING *) -let init_index () = () - -let empty_table () = - Path_indexing.PSTrie.empty -;; - -let index = Path_indexing.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 - let res = - let s = - match mode with - | Matching -> Path_indexing.retrieve_generalizations trie term - | Unification -> Path_indexing.retrieve_unifiables trie term -(* Path_indexing.retrieve_all trie term *) - in - Path_indexing.PosEqSet.elements s - in -(* print_candidates mode term res; *) - let t2 = Unix.gettimeofday () in - indexing_retrieval_time := !indexing_retrieval_time +. (t2 -. t1); - res -;; -*) - -(* DISCRIMINATION TREES *) -let init_index () = - Hashtbl.clear DT.arities; -;; - -let empty_table () = - DT.empty -;; - -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 - +let index = Index.index +let remove_index = Index.remove_index +let in_index = Index.in_index +let empty = Index.empty +let init_index = Index.init_index (* 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 @@ -180,10 +81,10 @@ let get_candidates mode tree term = let res = let s = match mode with - | Matching -> DT.retrieve_generalizations tree term - | Unification -> DT.retrieve_unifiables tree term + | Matching -> Index.retrieve_generalizations tree term + | Unification -> Index.retrieve_unifiables tree term in - PosEqSet.elements s + Index.PosEqSet.elements s in (* print_candidates mode term res; *) (* print_endline (Discrimination_tree.string_of_discrimination_tree tree); *) diff --git a/helm/ocaml/paramodulation/path_indexing.ml b/helm/ocaml/paramodulation/path_indexing.ml deleted file mode 100644 index 06da404ab..000000000 --- a/helm/ocaml/paramodulation/path_indexing.ml +++ /dev/null @@ -1,287 +0,0 @@ -(* Copyright (C) 2005, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - *) - -(* path indexing implementation *) - -(* position of the subterm, subterm (Appl are not stored...) *) -type path_string_elem = Index of int | Term of Cic.term;; -type path_string = path_string_elem list;; - - -let rec path_strings_of_term index = - let module C = Cic in function - | C.Meta _ -> [ [Index index; Term (C.Implicit None)] ] - | C.Appl (hd::tl) -> - let p = if index > 0 then [Index index; Term hd] else [Term hd] in - let _, res = - List.fold_left - (fun (i, r) t -> - let rr = path_strings_of_term i t in - (i+1, r @ (List.map (fun ps -> p @ ps) rr))) - (1, []) tl - in - res - | term -> [ [Index index; Term term] ] -;; - - -let string_of_path_string ps = - String.concat "." - (List.map - (fun e -> - let s = - match e with - | Index i -> "Index " ^ (string_of_int i) - | Term t -> "Term " ^ (CicPp.ppterm t) - in - "(" ^ s ^ ")") - ps) -;; - - -module OrderedPathStringElement = struct - type t = path_string_elem - - let compare t1 t2 = - match t1, t2 with - | Index i, Index j -> Pervasives.compare i j - | Term t1, Term t2 -> if t1 = t2 then 0 else Pervasives.compare t1 t2 - | Index _, Term _ -> -1 - | Term _, Index _ -> 1 -end - -module PSMap = Map.Make(OrderedPathStringElement);; - -module OrderedPosEquality = struct - type t = Utils.pos * Inference.equality - - let compare = Pervasives.compare -end - -module PosEqSet = Set.Make(OrderedPosEquality);; - - -module PSTrie = Trie.Make(PSMap);; - - -let index trie equality = - let _, _, (_, l, r, ordering), _, _ = equality in - let psl = path_strings_of_term 0 l - and psr = path_strings_of_term 0 r in - let index pos trie ps = - let ps_set = try PSTrie.find ps trie with Not_found -> PosEqSet.empty in - let trie = PSTrie.add ps (PosEqSet.add (pos, equality) ps_set) trie in - trie - in - match ordering with - | Utils.Gt -> List.fold_left (index Utils.Left) trie psl - | Utils.Lt -> List.fold_left (index Utils.Right) trie psr - | _ -> - let trie = List.fold_left (index Utils.Left) trie psl in - List.fold_left (index Utils.Right) trie psr -;; - - -let remove_index trie equality = - let _, _, (_, l, r, ordering), _, _ = equality in - let psl = path_strings_of_term 0 l - and psr = path_strings_of_term 0 r in - let remove_index pos trie ps = - try - let ps_set = PosEqSet.remove (pos, equality) (PSTrie.find ps trie) in - if PosEqSet.is_empty ps_set then - PSTrie.remove ps trie - else - PSTrie.add ps ps_set trie - with Not_found -> - trie - in - match ordering with - | Utils.Gt -> List.fold_left (remove_index Utils.Left) trie psl - | Utils.Lt -> List.fold_left (remove_index Utils.Right) trie psr - | _ -> - let trie = List.fold_left (remove_index Utils.Left) trie psl in - List.fold_left (remove_index Utils.Right) trie psr -;; - - -let in_index trie equality = - let _, _, (_, l, r, ordering), _, _ = equality in - let psl = path_strings_of_term 0 l - and psr = path_strings_of_term 0 r in - let meta_convertibility = Inference.meta_convertibility_eq equality in - let ok ps = - try - let set = PSTrie.find ps trie in - PosEqSet.exists (fun (p, e) -> meta_convertibility e) set - with Not_found -> - false - in - (List.exists ok psl) || (List.exists ok psr) -;; - - -let head_of_term = function - | Cic.Appl (hd::tl) -> hd - | term -> term -;; - - -let subterm_at_pos index term = - if index = 0 then - term - else - match term with - | Cic.Appl l -> - (try List.nth l index with Failure _ -> raise Not_found) - | _ -> raise Not_found -;; - - -let rec retrieve_generalizations trie term = - match trie with - | PSTrie.Node (value, map) -> - let res = - match term with - | Cic.Meta _ -> PosEqSet.empty - | term -> - let hd_term = head_of_term term in - try - let n = PSMap.find (Term hd_term) map in - match n with - | PSTrie.Node (Some s, _) -> s - | PSTrie.Node (None, m) -> - let l = - PSMap.fold - (fun k v res -> - match k with - | Index i -> - let t = subterm_at_pos i term in - let s = retrieve_generalizations v t in - s::res - | _ -> res) - m [] - in - match l with - | hd::tl -> - List.fold_left (fun r s -> PosEqSet.inter r s) hd tl - | _ -> PosEqSet.empty - with Not_found -> - PosEqSet.empty - in - try - let n = PSMap.find (Term (Cic.Implicit None)) map in - match n with - | PSTrie.Node (Some s, _) -> PosEqSet.union res s - | _ -> res - with Not_found -> - res -;; - - -let rec retrieve_unifiables trie term = - match trie with - | PSTrie.Node (value, map) -> - let res = - match term with - | Cic.Meta _ -> - PSTrie.fold - (fun ps v res -> PosEqSet.union res v) - (PSTrie.Node (None, map)) - PosEqSet.empty - | _ -> - let hd_term = head_of_term term in - try - let n = PSMap.find (Term hd_term) map in - match n with - | PSTrie.Node (Some v, _) -> v - | PSTrie.Node (None, m) -> - let l = - PSMap.fold - (fun k v res -> - match k with - | Index i -> - let t = subterm_at_pos i term in - let s = retrieve_unifiables v t in - s::res - | _ -> res) - m [] - in - match l with - | hd::tl -> - List.fold_left (fun r s -> PosEqSet.inter r s) hd tl - | _ -> PosEqSet.empty - with Not_found -> - PosEqSet.empty - in - try - let n = PSMap.find (Term (Cic.Implicit None)) map in - match n with - | PSTrie.Node (Some s, _) -> PosEqSet.union res s - | _ -> res - with Not_found -> - res -;; - - -let retrieve_all trie term = - PSTrie.fold - (fun k v s -> PosEqSet.union v s) trie PosEqSet.empty -;; - - -let string_of_pstrie trie = - let rec to_string level = function - | PSTrie.Node (v, map) -> - let s = - match v with - | Some v -> - (String.make (2 * level) ' ') ^ - "{" ^ (String.concat "; " - (List.map - (fun (p, e) -> - "(" ^ (Utils.string_of_pos p) ^ ", " ^ - (Inference.string_of_equality e) ^ ")") - (PosEqSet.elements v))) ^ "}" - | None -> "" - in - let rest = - String.concat "\n" - (PSMap.fold - (fun k v s -> - let ks = - match k with - | Index i -> "Index " ^ (string_of_int i) - | Term t -> "Term " ^ (CicPp.ppterm t) - in - let rs = to_string (level+1) v in - ((String.make (2 * level) ' ') ^ ks ^ "\n" ^ rs)::s) - map []) - in - s ^ rest - in - to_string 0 trie -;; - diff --git a/helm/ocaml/paramodulation/saturation.ml b/helm/ocaml/paramodulation/saturation.ml index 2e7f1f21a..bef39f7b2 100644 --- a/helm/ocaml/paramodulation/saturation.ml +++ b/helm/ocaml/paramodulation/saturation.ml @@ -221,8 +221,7 @@ let make_passive neg pos = List.fold_left (fun s e -> EqualitySet.add e s) EqualitySet.empty equalities in let table = - List.fold_left (fun tbl e -> Indexing.index tbl e) - (Indexing.empty_table ()) pos + List.fold_left (fun tbl e -> Indexing.index tbl e) Indexing.empty pos in (neg, set_of neg), (pos, set_of pos), @@ -231,7 +230,7 @@ let make_passive neg pos = let make_active () = - [], Indexing.empty_table () + [], Indexing.empty ;; @@ -364,7 +363,7 @@ let prune_passive howmany (active, _) passive = maximal_retained_equality := Some (EqualitySet.max_elt ps); let tbl = EqualitySet.fold - (fun e tbl -> Indexing.index tbl e) ps (Indexing.empty_table ()) + (fun e tbl -> Indexing.index tbl e) ps Indexing.empty in (nl, ns), (pl, ps), tbl ;; @@ -398,7 +397,7 @@ let infer env sign current (active_list, active_table) = let neg, pos = infer_positive table tl in neg, res @ pos in - let curr_table = Indexing.index (Indexing.empty_table ()) current in + let curr_table = Indexing.index Indexing.empty current in let neg, pos = infer_positive curr_table active_list in neg, res @ pos in @@ -655,7 +654,7 @@ let backward_simplify_active env new_pos new_table min_weight active = ) else (s, eq)::res, if s = Negative then tbl else Indexing.index tbl eq) - active_list ([], Indexing.empty_table ()), + active_list ([], Indexing.empty), List.fold_right (fun (s, eq) (n, p) -> if (s <> Negative) && (is_identity env eq) then ( @@ -692,7 +691,7 @@ let backward_simplify_passive env new_pos new_table min_weight passive = and pl, ps, newp = List.fold_right (f Positive) pl ([], ps, []) in let passive_table = List.fold_left - (fun tbl e -> Indexing.index tbl e) (Indexing.empty_table ()) pl + (fun tbl e -> Indexing.index tbl e) Indexing.empty pl in match newn, newp with | [], [] -> ((nl, ns), (pl, ps), passive_table), None @@ -706,7 +705,7 @@ let backward_simplify env new' ?passive active = (fun (l, t, w) e -> let ew, _, _, _, _ = e in (Positive, e)::l, Indexing.index t e, min ew w) - ([], Indexing.empty_table (), 1000000) (snd new') + ([], Indexing.empty, 1000000) (snd new') in let active, newa = backward_simplify_active env new_pos new_table min_weight active in @@ -1843,7 +1842,7 @@ let main dbd full term metasenv ugraph = let tbl = List.fold_left (fun t (_, e) -> Indexing.index t e) - (Indexing.empty_table ()) active + Indexing.empty active in let res = forward_simplify env e (active, tbl) in match others with @@ -2020,7 +2019,7 @@ let saturate let tbl = List.fold_left (fun t (_, e) -> Indexing.index t e) - (Indexing.empty_table ()) active + Indexing.empty active in let res = forward_simplify env e (active, tbl) in match others with @@ -2215,7 +2214,7 @@ let retrieve_and_print dbd term metasenv ugraph = let tbl = List.fold_left (fun t (_, e) -> Indexing.index t e) - (Indexing.empty_table ()) active + Indexing.empty active in let res = forward_simplify env (Positive, e) (active, tbl) in match others with @@ -2301,7 +2300,7 @@ let main_demod_equalities dbd term metasenv ugraph = let tbl = List.fold_left (fun t (_, e) -> Indexing.index t e) - (Indexing.empty_table ()) active + Indexing.empty active in let res = forward_simplify env e (active, tbl) in match others with