X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fparamodulation%2Fdiscrimination_tree.ml;fp=helm%2Focaml%2Fparamodulation%2Fdiscrimination_tree.ml;h=dc87e750398a9ea647c48683ad4f559e5bac8097;hb=e701ae61ea78b5bcbc8919ccb51f4f2ada8c5f23;hp=254a423327a9de6c48b2c241610e9387c766b064;hpb=f3db9a0fa7715783e93e4f927d5c73bff28090fa;p=helm.git diff --git a/helm/ocaml/paramodulation/discrimination_tree.ml b/helm/ocaml/paramodulation/discrimination_tree.ml index 254a42332..dc87e7503 100644 --- a/helm/ocaml/paramodulation/discrimination_tree.ml +++ b/helm/ocaml/paramodulation/discrimination_tree.ml @@ -41,59 +41,6 @@ module PosEqSet = Set.Make(OrderedPosEquality);; module DiscriminationTree = Trie.Make(PSMap);; - -(* -module DiscriminationTree = struct - type key = path_string - type t = Node of PosEqSet.t option * (t PSMap.t) - - let empty = Node (None, PSMap.empty) - - let rec find l t = - match (l, t) with - | [], Node (None, _) -> raise Not_found - | [], Node (Some v, _) -> v - | x::r, Node (_, m) -> find r (PSMap.find x m) - - let rec mem l t = - match (l, t) with - | [], Node (None, _) -> false - | [], Node (Some _, _) -> true - | x::r, Node (_, m) -> try mem r (PSMap.find x m) with Not_found -> false - - let add l v t = - let rec ins = function - | [], Node (_, m) -> Node (Some v, m) - | x::r, Node (v, m) -> - let t' = try PSMap.find x m with Not_found -> empty in - let t'' = ins (r, t') in - Node (v, PSMap.add x t'' m) - in - ins (l, t) - - let rec remove l t = - match (l, t) with - | [], Node (_, m) -> Node (None, m) - | x::r, Node (v, m) -> - try - let t' = remove r (PSMap.find x m) in - let m' = if t' = empty then PSMap.remove x m else PSMap.add x t' m in - Node (v, m') - with Not_found -> - t - - let rec fold f t acc = - let rec traverse revp t acc = match t with - | Node (None, m) -> - PSMap.fold (fun x -> traverse (x::revp)) m acc - | Node (Some v, m) -> - f (List.rev revp) v (PSMap.fold (fun x -> traverse (x::revp)) m acc) - in - traverse [] t acc - -end -*) - let string_of_discrimination_tree tree = let rec to_string level = function