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