matita/components/extlib/discrimination_tree.ml

   1 (* Copyright (C) 2005, HELM Team.
   2  *
   3  * This file is part of HELM, an Hypertextual, Electronic
   4  * Library of Mathematics, developed at the Computer Science
   5  * Department, University of Bologna, Italy.
   6  *
   7  * HELM is free software; you can redistribute it and/or
   8  * modify it under the terms of the GNU General Public License
   9  * as published by the Free Software Foundation; either version 2
  10  * of the License, or (at your option) any later version.
  11  *
  12  * HELM is distributed in the hope that it will be useful,
  13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  15  * GNU General Public License for more details.
  16  *
  17  * You should have received a copy of the GNU General Public License
  18  * along with HELM; if not, write to the Free Software
  19  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
  20  * MA  02111-1307, USA.
  21  *
  22  * For details, see the HELM World-Wide-Web page,
  23  * http://cs.unibo.it/helm/.
  24  *)
  25
  26 (* $Id$ *)
  27
  28 type 'a path_string_elem =
  29   | Constant of 'a * int (* name, arity *)
  30   | Bound of int * int (* rel, arity *)
  31   | Variable (* arity is 0 *)
  32   | Proposition (* arity is 0 *)
  33   | Datatype (* arity is 0 *)
  34   | Dead (* arity is 0 *)
  35 ;;
  36
  37 type 'a path = ('a path_string_elem) list;;
  38
  39 module type Indexable = sig
  40   type input
  41   type constant_name
  42   val compare:
  43     constant_name path_string_elem ->
  44     constant_name path_string_elem -> int
  45   val string_of_path : constant_name path -> string
  46   val path_string_of : input -> constant_name path
  47 end
  48
  49 let arity_of = function
  50   | Constant (_,a)
  51   | Bound (_,a) -> a
  52   | _ -> 0
  53 ;;
  54
  55 module type DiscriminationTree =
  56     sig
  57
  58       type input
  59       type data
  60       type dataset
  61       type constant_name
  62       type t
  63
  64       val iter : t -> (constant_name path -> dataset -> unit) -> unit
  65       val fold : t -> (constant_name path -> dataset -> 'b -> 'b) -> 'b -> 'b
  66
  67       val empty : t
  68       val index : t -> input -> data -> t
  69       val remove_index : t -> input -> data -> t
  70       val in_index : t -> input -> (data -> bool) -> bool
  71       val retrieve_generalizations : t -> input -> dataset
  72       val retrieve_unifiables : t -> input -> dataset
  73
  74       module type Collector = sig
  75         type t
  76         val empty : t
  77         val union : t -> t -> t
  78         val inter : t -> t -> data list
  79         val to_list : t -> data list
  80       end
  81       module Collector : Collector
  82       val retrieve_generalizations_sorted : t -> input -> Collector.t
  83       val retrieve_unifiables_sorted : t -> input -> Collector.t
  84     end
  85
  86 module Make (I:Indexable) (A:Set.S) : DiscriminationTree
  87 with type constant_name = I.constant_name and type input = I.input
  88 and type data = A.elt and type dataset = A.t =
  89
  90     struct
  91
  92       module OrderedPathStringElement = struct
  93         type t = I.constant_name path_string_elem
  94         let compare = I.compare
  95       end
  96
  97       type constant_name = I.constant_name
  98       type data = A.elt
  99       type dataset = A.t
 100       type input = I.input
 101
 102       module PSMap = Map.Make(OrderedPathStringElement);;
 103
 104       type key = PSMap.key
 105
 106       module DiscriminationTree = Trie.Make(PSMap);;
 107
 108       type t = A.t DiscriminationTree.t
 109
 110       let empty = DiscriminationTree.empty;;
 111
 112       let iter dt f = DiscriminationTree.iter (fun p x -> f p x) dt;;
 113
 114       let fold dt f = DiscriminationTree.fold (fun p x -> f p x) dt;;
 115
 116       let index tree term info =
 117         let ps = I.path_string_of term in
 118         let ps_set =
 119           try DiscriminationTree.find ps tree with Not_found -> A.empty
 120         in
 121         DiscriminationTree.add ps (A.add info ps_set) tree
 122       ;;
 123
 124       let remove_index tree term info =
 125         let ps = I.path_string_of term in
 126         try
 127           let ps_set = A.remove info (DiscriminationTree.find ps tree) in
 128           if A.is_empty ps_set then DiscriminationTree.remove ps tree
 129           else DiscriminationTree.add ps ps_set tree
 130         with Not_found -> tree
 131       ;;
 132
 133       let in_index tree term test =
 134         let ps = I.path_string_of term in
 135         try
 136           let ps_set = DiscriminationTree.find ps tree in
 137           A.exists test ps_set
 138         with Not_found -> false
 139       ;;
 140
 141       (* You have h(f(x,g(y,z)),t) whose path_string_of_term_with_jl is
 142          (h,2).(f,2).(x,0).(g,2).(y,0).(z,0).(t,0) and you are at f and want to
 143          skip all its progeny, thus you want to reach t.
 144
 145          You need to skip as many elements as the sum of all arieties contained
 146           in the progeny of f.
 147
 148          The input ariety is the one of f while the path is x.g....t
 149          Should be the equivalent of after_t in the literature (handbook A.R.)
 150        *)
 151       let rec skip arity path =
 152         if arity = 0 then path else match path with
 153         | [] -> assert false
 154         | m::tl -> skip (arity-1+arity_of m) tl
 155       ;;
 156
 157       (* the equivalent of skip, but on the index, thus the list of trees
 158          that are rooted just after the term represented by the tree root
 159          are returned (we are skipping the root) *)
 160       let skip_root = function DiscriminationTree.Node (_value, map) ->
 161         let rec get n = function DiscriminationTree.Node (_v, m) as tree ->
 162            if n = 0 then [tree] else
 163            PSMap.fold (fun k v res -> (get (n-1 + arity_of k) v) @ res) m []
 164         in
 165           PSMap.fold (fun k v res -> (get (arity_of k) v) @ res) map []
 166       ;;
 167
 168       let retrieve unif tree term =
 169         let path = I.path_string_of term in
 170         let rec retrieve path tree =
 171           match tree, path with
 172           | DiscriminationTree.Node (Some s, _), [] -> s
 173           | DiscriminationTree.Node (None, _), [] -> A.empty
 174           | DiscriminationTree.Node (_, _map), Variable::path when unif ->
 175               List.fold_left A.union A.empty
 176                 (List.map (retrieve path) (skip_root tree))
 177           | DiscriminationTree.Node (_, map), node::path ->
 178               A.union
 179                  (if not unif && node = Variable then A.empty else
 180                   try retrieve path (PSMap.find node map)
 181                   with Not_found -> A.empty)
 182                  (try
 183                     match PSMap.find Variable map,skip (arity_of node) path with
 184                     | DiscriminationTree.Node (Some s, _), [] -> s
 185                     | n, path -> retrieve path n
 186                   with Not_found -> A.empty)
 187        in
 188         retrieve path tree
 189       ;;
 190
 191       let retrieve_generalizations tree term = retrieve false tree term;;
 192       let retrieve_unifiables tree term = retrieve true tree term;;
 193
 194       module O = struct
 195         type t = A.t * int
 196         let compare (sa,wa) (sb,wb) =
 197           let c = compare wb wa in
 198           if c <> 0 then c else A.compare sb sa
 199       end
 200       module S = Set.Make(O)
 201
 202       (* TASSI: here we should think of a smarted data structure *)
 203       module type Collector = sig
 204         type t
 205         val empty : t
 206         val union : t -> t -> t
 207         val inter : t -> t -> data list
 208         val to_list : t -> data list
 209       end
 210       module Collector : Collector with type t = S.t = struct
 211         type t = S.t
 212         let union = S.union
 213         let empty = S.empty
 214
 215         let merge l =
 216           let rec aux s w = function
 217             | [] -> [s,w]
 218             | (t, wt)::tl when w = wt -> aux (A.union s t) w tl
 219             | (t, wt)::tl -> (s, w) :: aux t wt tl
 220           in
 221           match l with
 222           | [] -> []
 223           | (s, w) :: l -> aux s w l
 224
 225         let rec undup ~eq = function
 226           | [] -> []
 227           | x :: tl -> x :: undup ~eq (List.filter (fun y -> not(eq x y)) tl)
 228
 229         let to_list t =
 230           undup ~eq:(fun x y -> A.equal (A.singleton x) (A.singleton y))
 231             (List.flatten (List.map
 232               (fun x,_ -> A.elements x) (merge (S.elements t))))
 233
 234         let inter t1 t2 =
 235           let l1 = merge (S.elements t1) in
 236           let l2 = merge (S.elements t2) in
 237           let res =
 238            List.flatten
 239             (List.map
 240               (fun s, w ->
 241                  HExtlib.filter_map (fun x ->
 242                    try Some (x, w + snd (List.find (fun (s,_w) -> A.mem x s) l2))
 243                    with Not_found -> None)
 244                    (A.elements s))
 245               l1)
 246           in
 247           undup ~eq:(fun x y -> A.equal (A.singleton x) (A.singleton y))
 248             (List.map fst (List.sort (fun (_,x) (_,y) -> y - x) res))
 249       end
 250
 251       let retrieve_sorted unif tree term =
 252         let path = I.path_string_of term in
 253         let rec retrieve n path tree =
 254           match tree, path with
 255           | DiscriminationTree.Node (Some s, _), [] -> S.singleton (s, n)
 256           | DiscriminationTree.Node (None, _), [] -> S.empty
 257           | DiscriminationTree.Node (_, _map), Variable::path when unif ->
 258               List.fold_left S.union S.empty
 259                 (List.map (retrieve n path) (skip_root tree))
 260           | DiscriminationTree.Node (_, map), node::path ->
 261               S.union
 262                  (if not unif && node = Variable then S.empty else
 263                   try retrieve (n+1) path (PSMap.find node map)
 264                   with Not_found -> S.empty)
 265                  (try
 266                     match PSMap.find Variable map,skip (arity_of node) path with
 267                     | DiscriminationTree.Node (Some s, _), [] ->
 268                        S.singleton (s, n)
 269                     | no, path -> retrieve n path no
 270                   with Not_found -> S.empty)
 271        in
 272         retrieve 0 path tree
 273       ;;
 274
 275       let retrieve_generalizations_sorted tree term =
 276         retrieve_sorted false tree term;;
 277       let retrieve_unifiables_sorted tree term =
 278         retrieve_sorted true tree term;;
 279   end
 280 ;;
 281