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