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