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       val retrieve_generalizations_sorted : t -> input -> (data * int) list
  74       val retrieve_unifiables_sorted : t -> input -> (data * int) list
  75     end
  76
  77 module Make (I:Indexable) (A:Set.S) : DiscriminationTree
  78 with type constant_name = I.constant_name and type input = I.input
  79 and type data = A.elt and type dataset = A.t =
  80
  81     struct
  82
  83       module OrderedPathStringElement = struct
  84         type t = I.constant_name path_string_elem
  85         let compare = I.compare
  86       end
  87
  88       type constant_name = I.constant_name
  89       type data = A.elt
  90       type dataset = A.t
  91       type input = I.input
  92
  93       module PSMap = Map.Make(OrderedPathStringElement);;
  94
  95       type key = PSMap.key
  96
  97       module DiscriminationTree = Trie.Make(PSMap);;
  98
  99       type t = A.t DiscriminationTree.t
 100
 101       let empty = DiscriminationTree.empty;;
 102
 103       let iter dt f = DiscriminationTree.iter (fun p x -> f p x) dt;;
 104
 105       let fold dt f = DiscriminationTree.fold (fun p x -> f p x) dt;;
 106
 107       let index tree term info =
 108         let ps = I.path_string_of term in
 109         let ps_set =
 110           try DiscriminationTree.find ps tree with Not_found -> A.empty
 111         in
 112         DiscriminationTree.add ps (A.add info ps_set) tree
 113       ;;
 114
 115       let remove_index tree term info =
 116         let ps = I.path_string_of term in
 117         try
 118           let ps_set = A.remove info (DiscriminationTree.find ps tree) in
 119           if A.is_empty ps_set then DiscriminationTree.remove ps tree
 120           else DiscriminationTree.add ps ps_set tree
 121         with Not_found -> tree
 122       ;;
 123
 124       let in_index tree term test =
 125         let ps = I.path_string_of term in
 126         try
 127           let ps_set = DiscriminationTree.find ps tree in
 128           A.exists test ps_set
 129         with Not_found -> false
 130       ;;
 131
 132       (* You have h(f(x,g(y,z)),t) whose path_string_of_term_with_jl is
 133          (h,2).(f,2).(x,0).(g,2).(y,0).(z,0).(t,0) and you are at f and want to
 134          skip all its progeny, thus you want to reach t.
 135
 136          You need to skip as many elements as the sum of all arieties contained
 137           in the progeny of f.
 138
 139          The input ariety is the one of f while the path is x.g....t
 140          Should be the equivalent of after_t in the literature (handbook A.R.)
 141        *)
 142       let rec skip arity path =
 143         if arity = 0 then path else match path with
 144         | [] -> assert false
 145         | m::tl -> skip (arity-1+arity_of m) tl
 146       ;;
 147
 148       (* the equivalent of skip, but on the index, thus the list of trees
 149          that are rooted just after the term represented by the tree root
 150          are returned (we are skipping the root) *)
 151       let skip_root = function DiscriminationTree.Node (value, map) ->
 152         let rec get n = function DiscriminationTree.Node (v, m) as tree ->
 153            if n = 0 then [tree] else
 154            PSMap.fold (fun k v res -> (get (n-1 + arity_of k) v) @ res) m []
 155         in
 156           PSMap.fold (fun k v res -> (get (arity_of k) v) @ res) map []
 157       ;;
 158
 159       let retrieve unif tree term =
 160         let path = I.path_string_of term in
 161         let rec retrieve path tree =
 162           match tree, path with
 163           | DiscriminationTree.Node (Some s, _), [] -> s
 164           | DiscriminationTree.Node (None, _), [] -> A.empty
 165           | DiscriminationTree.Node (_, map), Variable::path when unif ->
 166               List.fold_left A.union A.empty
 167                 (List.map (retrieve path) (skip_root tree))
 168           | DiscriminationTree.Node (_, map), node::path ->
 169               A.union
 170                  (if not unif && node = Variable then A.empty else
 171                   try retrieve path (PSMap.find node map)
 172                   with Not_found -> A.empty)
 173                  (try
 174                     match PSMap.find Variable map,skip (arity_of node) path with
 175                     | DiscriminationTree.Node (Some s, _), [] -> s
 176                     | n, path -> retrieve path n
 177                   with Not_found -> A.empty)
 178        in
 179         retrieve path tree
 180       ;;
 181
 182       let retrieve_generalizations tree term = retrieve false tree term;;
 183       let retrieve_unifiables tree term = retrieve true tree term;;
 184
 185       module O = struct
 186         type t = A.t * int
 187         let compare (_,a) (_,b) = compare b a
 188       end
 189       module S = Set.Make(O)
 190
 191       let retrieve_sorted unif tree term =
 192         let path = I.path_string_of term in
 193         let rec retrieve n path tree =
 194           match tree, path with
 195           | DiscriminationTree.Node (Some s, _), [] -> S.singleton (s, n)
 196           | DiscriminationTree.Node (None, _), [] -> S.empty
 197           | DiscriminationTree.Node (_, map), Variable::path when unif ->
 198               List.fold_left S.union S.empty
 199                 (List.map (retrieve n path) (skip_root tree))
 200           | DiscriminationTree.Node (_, map), node::path ->
 201               S.union
 202                  (if not unif && node = Variable then S.empty else
 203                   try retrieve (n+1) path (PSMap.find node map)
 204                   with Not_found -> S.empty)
 205                  (try
 206                     match PSMap.find Variable map,skip (arity_of node) path with
 207                     | DiscriminationTree.Node (Some s, _), [] ->
 208                        S.singleton (s, n)
 209                     | no, path -> retrieve n path no
 210                   with Not_found -> S.empty)
 211        in
 212         List.flatten
 213          (List.map (fun x -> List.map (fun y -> y, snd x) (A.elements (fst x)))
 214           (S.elements (retrieve 0 path tree)))
 215       ;;
 216
 217       let retrieve_generalizations_sorted tree term =
 218         retrieve_sorted false tree term;;
 219       let retrieve_unifiables_sorted tree term =
 220         retrieve_sorted true tree term;;
 221   end
 222 ;;
 223