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