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