helm/ocaml/paramodulation/path_indexing.ml

   1 (* path indexing implementation *)
   2
   3 (* position of the subterm, subterm (Appl are not stored...) *)
   4 type path_string_elem = Index of int | Term of Cic.term;;
   5 type path_string = path_string_elem list;;
   6
   7
   8 let rec path_strings_of_term index =
   9   let module C = Cic in function
  10   | C.Meta _ -> [ [Index index; Term (C.Implicit None)] ]
  11   | C.Appl (hd::tl) ->
  12       let p = if index > 0 then [Index index; Term hd] else [Term hd] in
  13       let _, res =
  14         List.fold_left
  15           (fun (i, r) t ->
  16              let rr = path_strings_of_term i t in
  17              (i+1, r @ (List.map (fun ps -> p @ ps) rr)))
  18           (1, []) tl
  19       in
  20       res
  21   | term -> [ [Index index; Term term] ]
  22 ;;
  23
  24
  25 let string_of_path_string ps =
  26   String.concat "."
  27     (List.map
  28        (fun e ->
  29           let s =
  30             match e with
  31             | Index i -> "Index " ^ (string_of_int i)
  32             | Term t -> "Term " ^ (CicPp.ppterm t)
  33           in
  34           "(" ^ s ^ ")")
  35        ps)
  36 ;;
  37
  38
  39 module OrderedPathStringElement = struct
  40   type t = path_string_elem
  41
  42   let compare t1 t2 =
  43     match t1, t2 with
  44     | Index i, Index j -> Pervasives.compare i j
  45     | Term t1, Term t2 -> if t1 = t2 then 0 else Pervasives.compare t1 t2
  46     | Index _, Term _ -> -1
  47     | Term _, Index _ -> 1
  48 end
  49
  50 module PSMap = Map.Make(OrderedPathStringElement);;
  51
  52 module OrderedPosEquality = struct
  53   type t = Utils.pos * Inference.equality
  54
  55   let compare = Pervasives.compare
  56 end
  57
  58 module PosEqSet = Set.Make(OrderedPosEquality);;
  59
  60
  61 module PSTrie = Trie.Make(PSMap);;
  62
  63 (*
  64 (*
  65  * Trie: maps over lists.
  66  * Copyright (C) 2000 Jean-Christophe FILLIATRE
  67  *)
  68 module PSTrie = struct
  69   type key = path_string
  70   type t = Node of PosEqSet.t option * (t PSMap.t)
  71
  72   let empty = Node (None, PSMap.empty)
  73
  74   let rec find l t =
  75     match (l, t) with
  76     | [], Node (None, _) -> raise Not_found
  77     | [], Node (Some v, _) -> v
  78     | x::r, Node (_, m) -> find r (PSMap.find x m)
  79
  80   let rec mem l t =
  81     match (l, t) with
  82     | [], Node (None, _) -> false
  83     | [], Node (Some _, _) -> true
  84     | x::r, Node (_, m) -> try mem r (PSMap.find x m) with Not_found -> false
  85
  86   let add l v t =
  87     let rec ins = function
  88       | [], Node (_, m) -> Node (Some v, m)
  89       | x::r, Node (v, m) ->
  90           let t' = try PSMap.find x m with Not_found -> empty in
  91           let t'' = ins (r, t') in
  92           Node (v, PSMap.add x t'' m)
  93     in
  94     ins (l, t)
  95
  96   let rec remove l t =
  97     match (l, t) with
  98     | [], Node (_, m) -> Node (None, m)
  99     | x::r, Node (v, m) ->
 100         try
 101           let t' = remove r (PSMap.find x m) in
 102           Node (v, if t' = empty then PSMap.remove x m else PSMap.add x t' m)
 103         with Not_found ->
 104           t
 105
 106   let rec fold f t acc =
 107     let rec traverse revp t acc = match t with
 108       | Node (None, m) ->
 109           PSMap.fold (fun x -> traverse (x::revp)) m acc
 110       | Node (Some v, m) ->
 111           f (List.rev revp) v (PSMap.fold (fun x -> traverse (x::revp)) m acc)
 112     in
 113     traverse [] t acc
 114
 115 end
 116 *)
 117
 118
 119 let index trie equality =
 120   let _, _, (_, l, r, ordering), _, _ = equality in
 121   let psl = path_strings_of_term 0 l
 122   and psr = path_strings_of_term 0 r in
 123   let index pos trie ps =
 124     let ps_set = try PSTrie.find ps trie with Not_found -> PosEqSet.empty in
 125     let trie = PSTrie.add ps (PosEqSet.add (pos, equality) ps_set) trie in
 126 (*     if PosEqSet.mem (pos, equality) (PSTrie.find ps trie) then *)
 127 (*       Printf.printf "OK: %s, %s indexed\n" (Utils.string_of_pos pos) *)
 128 (*         (Inference.string_of_equality equality); *)
 129     trie
 130   in
 131   match ordering with
 132   | Utils.Gt -> List.fold_left (index Utils.Left) trie psl
 133   | Utils.Lt -> List.fold_left (index Utils.Right) trie psr
 134   | _ ->
 135       let trie = List.fold_left (index Utils.Left) trie psl in
 136       List.fold_left (index Utils.Right) trie psr
 137 ;;
 138
 139
 140 let remove_index trie equality =
 141   let _, _, (_, l, r, ordering), _, _ = equality in
 142   let psl = path_strings_of_term 0 l
 143   and psr = path_strings_of_term 0 r in
 144   let remove_index pos trie ps =
 145     try
 146       let ps_set = PosEqSet.remove (pos, equality) (PSTrie.find ps trie) in
 147       if PosEqSet.is_empty ps_set then
 148         PSTrie.remove ps trie
 149       else
 150         PSTrie.add ps ps_set trie
 151     with Not_found ->
 152 (*       Printf.printf "NOT_FOUND: %s, %s\n" (Utils.string_of_pos pos) *)
 153 (*         (Inference.string_of_equality equality); *)
 154       trie
 155 (*       raise Not_found *)
 156   in
 157   match ordering with
 158   | Utils.Gt -> List.fold_left (remove_index Utils.Left) trie psl
 159   | Utils.Lt -> List.fold_left (remove_index Utils.Right) trie psr
 160   | _ ->
 161       let trie = List.fold_left (remove_index Utils.Left) trie psl in
 162       List.fold_left (remove_index Utils.Right) trie psr
 163 ;;
 164
 165
 166 let in_index trie equality =
 167   let _, _, (_, l, r, ordering), _, _ = equality in
 168   let psl = path_strings_of_term 0 l
 169   and psr = path_strings_of_term 0 r in
 170   let meta_convertibility = Inference.meta_convertibility_eq equality in
 171   let ok ps =
 172     try
 173       let set = PSTrie.find ps trie in
 174       PosEqSet.exists (fun (p, e) -> meta_convertibility e) set
 175     with Not_found ->
 176       false
 177   in
 178   (List.exists ok psl) || (List.exists ok psr)
 179 ;;
 180
 181
 182 let head_of_term = function
 183   | Cic.Appl (hd::tl) -> hd
 184   | term -> term
 185 ;;
 186
 187
 188 let subterm_at_pos index term =
 189   if index = 0 then
 190     term
 191   else
 192     match term with
 193     | Cic.Appl l ->
 194         (try List.nth l index with Failure _ -> raise Not_found)
 195     | _ -> raise Not_found
 196 ;;
 197
 198
 199 let rec retrieve_generalizations trie term =
 200   match trie with
 201   | PSTrie.Node (value, map) ->
 202       let res =
 203         match term with
 204         | Cic.Meta _ -> PosEqSet.empty
 205         | term ->
 206             let hd_term = head_of_term term in
 207             try
 208               let n = PSMap.find (Term hd_term) map in
 209               match n with
 210               | PSTrie.Node (Some s, _) -> s
 211               | PSTrie.Node (None, m) ->
 212                   let l =
 213                     PSMap.fold
 214                       (fun k v res ->
 215                          match k with
 216                          | Index i ->
 217                              let t = subterm_at_pos i term in
 218                              let s = retrieve_generalizations v t in
 219                              s::res
 220                          | _ -> res)
 221                       m []
 222                   in
 223                   match l with
 224                   | hd::tl ->
 225                       List.fold_left (fun r s -> PosEqSet.inter r s) hd tl
 226                   | _ -> PosEqSet.empty
 227             with Not_found ->
 228               PosEqSet.empty
 229       in
 230       try
 231         let n = PSMap.find (Term (Cic.Implicit None)) map in
 232         match n with
 233         | PSTrie.Node (Some s, _) -> PosEqSet.union res s
 234         | _ -> res
 235       with Not_found ->
 236         res
 237 ;;
 238
 239
 240 let rec retrieve_unifiables trie term =
 241   match trie with
 242   | PSTrie.Node (value, map) ->
 243       let res =
 244         match term with
 245         | Cic.Meta _ ->
 246             PSTrie.fold
 247               (fun ps v res -> PosEqSet.union res v)
 248               (PSTrie.Node (None, map))
 249               PosEqSet.empty
 250         | _ ->
 251             let hd_term = head_of_term term in
 252             try
 253               let n = PSMap.find (Term hd_term) map in
 254               match n with
 255               | PSTrie.Node (Some v, _) -> v
 256               | PSTrie.Node (None, m) ->
 257                   let l =
 258                     PSMap.fold
 259                       (fun k v res ->
 260                          match k with
 261                          | Index i ->
 262                              let t = subterm_at_pos i term in
 263                              let s = retrieve_unifiables v t in
 264                              s::res
 265                          | _ -> res)
 266                       m []
 267                   in
 268                   match l with
 269                   | hd::tl ->
 270                       List.fold_left (fun r s -> PosEqSet.inter r s) hd tl
 271                   | _ -> PosEqSet.empty
 272             with Not_found ->
 273 (*               Printf.printf "Not_found: %s, term was: %s\n" *)
 274 (*                 (CicPp.ppterm hd_term) (CicPp.ppterm term); *)
 275 (*               Printf.printf "map is:\n %s\n\n" *)
 276 (*                 (String.concat "\n" *)
 277 (*                    (PSMap.fold *)
 278 (*                       (fun k v l -> *)
 279 (*                          match k with *)
 280 (*                          | Index i -> ("Index " ^ (string_of_int i))::l *)
 281 (*                          | Term t -> ("Term " ^ (CicPp.ppterm t))::l) *)
 282 (*                       map [])); *)
 283               PosEqSet.empty
 284       in
 285       try
 286         let n = PSMap.find (Term (Cic.Implicit None)) map in
 287         match n with
 288         | PSTrie.Node (Some s, _) -> PosEqSet.union res s
 289         | _ -> res
 290       with Not_found ->
 291         res
 292 ;;
 293
 294
 295 let retrieve_all trie term =
 296   PSTrie.fold
 297     (fun k v s -> PosEqSet.union v s) trie PosEqSet.empty
 298 ;;
 299
 300
 301 let string_of_pstrie trie =
 302   let rec to_string level = function
 303     | PSTrie.Node (v, map) ->
 304         let s =
 305           match v with
 306           | Some v ->
 307               (String.make (2 * level) ' ') ^
 308                 "{" ^ (String.concat "; "
 309                          (List.map
 310                             (fun (p, e) ->
 311                                "(" ^ (Utils.string_of_pos p) ^ ", " ^
 312                                  (Inference.string_of_equality e) ^ ")")
 313                             (PosEqSet.elements v))) ^ "}"
 314           | None -> ""
 315         in
 316         let rest =
 317           String.concat "\n"
 318             (PSMap.fold
 319                (fun k v s ->
 320                   let ks =
 321                     match k with
 322                     | Index i -> "Index " ^ (string_of_int i)
 323                     | Term t -> "Term " ^ (CicPp.ppterm t)
 324                   in
 325                   let rs = to_string (level+1) v in
 326                   ((String.make (2 * level) ' ') ^ ks ^ "\n" ^ rs)::s)
 327                map [])
 328         in
 329         s ^ rest
 330   in
 331   to_string 0 trie
 332 ;;
 333