components/cic/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 module DiscriminationTreeIndexing =
  29   functor (A:Set.S) ->
  30     struct
  31
  32       type path_string_elem = Cic.term;;
  33       type path_string = path_string_elem list;;
  34
  35
  36       (* needed by the retrieve_* functions, to know the arities of the "functions" *)
  37
  38       let arities = Hashtbl.create 11;;
  39
  40       let shared_implicit = [Cic.Implicit None]
  41
  42       let rec path_string_of_term = function
  43         | Cic.Meta _ -> shared_implicit
  44         | Cic.Appl ((hd::tl) as l) ->
  45             if not (Hashtbl.mem arities hd) then
  46               Hashtbl.add arities hd (List.length tl);
  47             List.concat (List.map path_string_of_term l)
  48         | term -> [term]
  49       ;;
  50
  51
  52       module OrderedPathStringElement = struct
  53         type t = path_string_elem
  54
  55         let compare = Pervasives.compare
  56       end
  57
  58       module PSMap = Map.Make(OrderedPathStringElement);;
  59
  60       type key = PSMap.key
  61
  62       module DiscriminationTree = Trie.Make(PSMap);;
  63
  64       type t = A.t DiscriminationTree.t
  65       let empty = DiscriminationTree.empty
  66
  67 (*
  68       module OrderedPosEquality = struct
  69         type t = Utils.pos * Inference.equality
  70         let compare = Pervasives.compare
  71       end
  72
  73       module PosEqSet = Set.Make(OrderedPosEquality);;
  74
  75       let string_of_discrimination_tree tree =
  76         let rec to_string level = function
  77           | DiscriminationTree.Node (value, map) ->
  78               let s =
  79                 match value with
  80                   | Some v ->
  81                       (String.make (2 * level) ' ') ^
  82                         "{" ^ (String.concat "; "
  83                                  (List.map
  84                                     (fun (p, e) ->
  85                                        "(" ^ (Utils.string_of_pos p) ^ ", " ^
  86                                          (Inference.string_of_equality e) ^ ")")
  87                                     (PosEqSet.elements v))) ^ "}"
  88                   | None -> ""
  89               in
  90               let rest =
  91                 String.concat "\n"
  92                   (PSMap.fold
  93                      (fun k v s ->
  94                         let ks = CicPp.ppterm k in
  95                         let rs = to_string (level+1) v in
  96                           ((String.make (2 * level) ' ') ^ ks ^ "\n" ^ rs)::s)
  97                      map [])
  98               in
  99                 s ^ rest
 100         in
 101           to_string 0 tree
 102       ;;
 103 *)
 104
 105       let index tree term info =
 106         let ps = path_string_of_term term in
 107         let ps_set =
 108           try DiscriminationTree.find ps tree
 109           with Not_found -> A.empty in
 110         let tree =
 111           DiscriminationTree.add ps (A.add info ps_set) tree in
 112         tree
 113
 114 (*
 115       let index tree equality =
 116         let _, _, (_, l, r, ordering), _, _ = equality in
 117         let psl = path_string_of_term l
 118         and psr = path_string_of_term r in
 119         let index pos tree ps =
 120           let ps_set =
 121             try DiscriminationTree.find ps tree with Not_found -> PosEqSet.empty in
 122           let tree =
 123             DiscriminationTree.add ps (PosEqSet.add (pos, equality) ps_set) tree in
 124             tree
 125         in
 126           match ordering with
 127             | Utils.Gt -> index Utils.Left tree psl
 128             | Utils.Lt -> index Utils.Right tree psr
 129             | _ ->
 130                 let tree = index Utils.Left tree psl in
 131                   index Utils.Right tree psr
 132       ;;
 133 *)
 134
 135       let remove_index tree term info =
 136         let ps = path_string_of_term term in
 137         try
 138           let ps_set =
 139             A.remove info (DiscriminationTree.find ps tree) in
 140             if A.is_empty ps_set then
 141               DiscriminationTree.remove ps tree
 142             else
 143               DiscriminationTree.add ps ps_set tree
 144         with Not_found ->
 145           tree
 146
 147 (*
 148 let remove_index tree equality =
 149   let _, _, (_, l, r, ordering), _, _ = equality in
 150   let psl = path_string_of_term l
 151   and psr = path_string_of_term r in
 152   let remove_index pos tree ps =
 153     try
 154       let ps_set =
 155         PosEqSet.remove (pos, equality) (DiscriminationTree.find ps tree) in
 156       if PosEqSet.is_empty ps_set then
 157         DiscriminationTree.remove ps tree
 158       else
 159         DiscriminationTree.add ps ps_set tree
 160     with Not_found ->
 161       tree
 162   in
 163   match ordering with
 164   | Utils.Gt -> remove_index Utils.Left tree psl
 165   | Utils.Lt -> remove_index Utils.Right tree psr
 166   | _ ->
 167       let tree = remove_index Utils.Left tree psl in
 168       remove_index Utils.Right tree psr
 169 ;;
 170 *)
 171
 172
 173       let in_index tree term test =
 174         let ps = path_string_of_term term in
 175         try
 176           let ps_set = DiscriminationTree.find ps tree in
 177           A.exists test ps_set
 178         with Not_found ->
 179           false
 180
 181 (*
 182       let in_index tree equality =
 183         let _, _, (_, l, r, ordering), _, _ = equality in
 184         let psl = path_string_of_term l
 185         and psr = path_string_of_term r in
 186         let meta_convertibility = Inference.meta_convertibility_eq equality in
 187         let ok ps =
 188           try
 189             let set = DiscriminationTree.find ps tree in
 190               PosEqSet.exists (fun (p, e) -> meta_convertibility e) set
 191           with Not_found ->
 192             false
 193         in
 194           (ok psl) || (ok psr)
 195 ;;
 196 *)
 197
 198
 199       let head_of_term = function
 200         | Cic.Appl (hd::tl) -> hd
 201         | term -> term
 202       ;;
 203
 204
 205       let rec subterm_at_pos pos term =
 206         match pos with
 207           | [] -> term
 208           | index::pos ->
 209               match term with
 210                 | Cic.Appl l ->
 211                     (try subterm_at_pos pos (List.nth l index)
 212                      with Failure _ -> raise Not_found)
 213                 | _ -> raise Not_found
 214       ;;
 215
 216
 217       let rec after_t pos term =
 218         let pos' =
 219           match pos with
 220             | [] -> raise Not_found
 221             | pos -> List.fold_right (fun i r -> if r = [] then [i+1] else i::r) pos []
 222         in
 223           try
 224             ignore(subterm_at_pos pos' term ); pos'
 225           with Not_found ->
 226             let pos, _ =
 227               List.fold_right
 228                 (fun i (r, b) -> if b then (i::r, true) else (r, true)) pos ([], false)
 229             in
 230               after_t pos term
 231       ;;
 232
 233
 234       let next_t pos term =
 235         let t = subterm_at_pos pos term in
 236           try
 237             let _ = subterm_at_pos [1] t in
 238               pos @ [1]
 239           with Not_found ->
 240             match pos with
 241               | [] -> [1]
 242               | pos -> after_t pos term
 243       ;;
 244
 245
 246       let retrieve_generalizations tree term =
 247         let rec retrieve tree term pos =
 248           match tree with
 249             | DiscriminationTree.Node (Some s, _) when pos = [] -> s
 250             | DiscriminationTree.Node (_, map) ->
 251                 let res =
 252                   try
 253                     let hd_term = head_of_term (subterm_at_pos pos term) in
 254                     let n = PSMap.find hd_term map in
 255                       match n with
 256                         | DiscriminationTree.Node (Some s, _) -> s
 257                         | DiscriminationTree.Node (None, _) ->
 258                             let newpos = try next_t pos term with Not_found -> [] in
 259                               retrieve n term newpos
 260                   with Not_found ->
 261                     A.empty
 262                 in
 263                   try
 264                     let n = PSMap.find (Cic.Implicit None) map in
 265                     let newpos = try after_t pos term with Not_found -> [-1] in
 266                       if newpos = [-1] then
 267                         match n with
 268                           | DiscriminationTree.Node (Some s, _) -> A.union s res
 269                           | _ -> res
 270                       else
 271                         A.union res (retrieve n term newpos)
 272                   with Not_found ->
 273                     res
 274         in
 275           retrieve tree term []
 276       ;;
 277
 278
 279       let jump_list = function
 280         | DiscriminationTree.Node (value, map) ->
 281             let rec get n tree =
 282               match tree with
 283                 | DiscriminationTree.Node (v, m) ->
 284                     if n = 0 then
 285                       [tree]
 286                     else
 287                       PSMap.fold
 288                         (fun k v res ->
 289                            let a = try Hashtbl.find arities k with Not_found -> 0 in
 290                              (get (n-1 + a) v) @ res) m []
 291             in
 292               PSMap.fold
 293                 (fun k v res ->
 294                    let arity = try Hashtbl.find arities k with Not_found -> 0 in
 295                      (get arity v) @ res)
 296                 map []
 297       ;;
 298
 299
 300       let retrieve_unifiables tree term =
 301         let rec retrieve tree term pos =
 302           match tree with
 303             | DiscriminationTree.Node (Some s, _) when pos = [] -> s
 304             | DiscriminationTree.Node (_, map) ->
 305                 let subterm =
 306                   try Some (subterm_at_pos pos term) with Not_found -> None
 307                 in
 308                   match subterm with
 309                     | None -> A.empty
 310                     | Some (Cic.Meta _) ->
 311                         let newpos = try next_t pos term with Not_found -> [] in
 312                         let jl = jump_list tree in
 313                           List.fold_left
 314                             (fun r s -> A.union r s)
 315                             A.empty
 316                             (List.map (fun t -> retrieve t term newpos) jl)
 317                     | Some subterm ->
 318                         let res =
 319                           try
 320                             let hd_term = head_of_term subterm in
 321                             let n = PSMap.find hd_term map in
 322                               match n with
 323                                 | DiscriminationTree.Node (Some s, _) -> s
 324                                 | DiscriminationTree.Node (None, _) ->
 325                                     retrieve n term (next_t pos term)
 326                           with Not_found ->
 327                             A.empty
 328                         in
 329                           try
 330                             let n = PSMap.find (Cic.Implicit None) map in
 331                             let newpos = try after_t pos term with Not_found -> [-1] in
 332                               if newpos = [-1] then
 333                                 match n with
 334                                   | DiscriminationTree.Node (Some s, _) -> A.union s res
 335                                   | _ -> res
 336                               else
 337                                 A.union res (retrieve n term newpos)
 338                           with Not_found ->
 339                             res
 340         in
 341           retrieve tree term []
 342     end
 343 ;;
 344