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 head_of_term = function
 164   | Cic.Appl (hd::tl) -> hd
 165   | term -> term
 166 ;;
 167
 168
 169 let subterm_at_pos index term =
 170   if index = 0 then
 171     term
 172   else
 173     match term with
 174     | Cic.Appl l ->
 175         (try List.nth l index with Failure _ -> raise Not_found)
 176     | _ -> raise Not_found
 177 ;;
 178
 179
 180 let rec retrieve_generalizations trie term =
 181   match trie with
 182   | PSTrie.Node (value, map) ->
 183       let res =
 184         match term with
 185         | Cic.Meta _ -> PosEqSet.empty
 186         | term ->
 187             let hd_term = head_of_term term in
 188             try
 189               let n = PSMap.find (Term hd_term) map in
 190               match n with
 191               | PSTrie.Node (Some s, _) -> s
 192               | PSTrie.Node (None, m) ->
 193                   let l =
 194                     PSMap.fold
 195                       (fun k v res ->
 196                          match k with
 197                          | Index i ->
 198                              let t = subterm_at_pos i term in
 199                              let s = retrieve_generalizations v t in
 200                              s::res
 201                          | _ -> res)
 202                       m []
 203                   in
 204                   match l with
 205                   | hd::tl ->
 206                       List.fold_left (fun r s -> PosEqSet.inter r s) hd tl
 207                   | _ -> PosEqSet.empty
 208             with Not_found ->
 209               PosEqSet.empty
 210       in
 211       try
 212         let n = PSMap.find (Term (Cic.Implicit None)) map in
 213         match n with
 214         | PSTrie.Node (Some s, _) -> PosEqSet.union res s
 215         | _ -> res
 216       with Not_found ->
 217         res
 218 ;;
 219
 220
 221 let rec retrieve_unifiables trie term =
 222   match trie with
 223   | PSTrie.Node (value, map) ->
 224       let res =
 225         match term with
 226         | Cic.Meta _ ->
 227             PSTrie.fold
 228               (fun ps v res -> PosEqSet.union res v)
 229               (PSTrie.Node (None, map))
 230               PosEqSet.empty
 231         | _ ->
 232             let hd_term = head_of_term term in
 233             try
 234               let n = PSMap.find (Term hd_term) map in
 235               match n with
 236               | PSTrie.Node (Some v, _) -> v
 237               | PSTrie.Node (None, m) ->
 238                   let l =
 239                     PSMap.fold
 240                       (fun k v res ->
 241                          match k with
 242                          | Index i ->
 243                              let t = subterm_at_pos i term in
 244                              let s = retrieve_unifiables v t in
 245                              s::res
 246                          | _ -> res)
 247                       m []
 248                   in
 249                   match l with
 250                   | hd::tl ->
 251                       List.fold_left (fun r s -> PosEqSet.inter r s) hd tl
 252                   | _ -> PosEqSet.empty
 253             with Not_found ->
 254 (*               Printf.printf "Not_found: %s, term was: %s\n" *)
 255 (*                 (CicPp.ppterm hd_term) (CicPp.ppterm term); *)
 256 (*               Printf.printf "map is:\n %s\n\n" *)
 257 (*                 (String.concat "\n" *)
 258 (*                    (PSMap.fold *)
 259 (*                       (fun k v l -> *)
 260 (*                          match k with *)
 261 (*                          | Index i -> ("Index " ^ (string_of_int i))::l *)
 262 (*                          | Term t -> ("Term " ^ (CicPp.ppterm t))::l) *)
 263 (*                       map [])); *)
 264               PosEqSet.empty
 265       in
 266       try
 267         let n = PSMap.find (Term (Cic.Implicit None)) map in
 268         match n with
 269         | PSTrie.Node (Some s, _) -> PosEqSet.union res s
 270         | _ -> res
 271       with Not_found ->
 272         res
 273 ;;
 274
 275
 276 let string_of_pstrie trie =
 277   let rec to_string level = function
 278     | PSTrie.Node (v, map) ->
 279         let s =
 280           match v with
 281           | Some v ->
 282               (String.make (2 * level) ' ') ^
 283                 "{" ^ (String.concat "; "
 284                          (List.map
 285                             (fun (p, e) ->
 286                                "(" ^ (Utils.string_of_pos p) ^ ", " ^
 287                                  (Inference.string_of_equality e) ^ ")")
 288                             (PosEqSet.elements v))) ^ "}"
 289           | None -> ""
 290         in
 291         let rest =
 292           String.concat "\n"
 293             (PSMap.fold
 294                (fun k v s ->
 295                   let ks =
 296                     match k with
 297                     | Index i -> "Index " ^ (string_of_int i)
 298                     | Term t -> "Term " ^ (CicPp.ppterm t)
 299                   in
 300                   let rs = to_string (level+1) v in
 301                   ((String.make (2 * level) ' ') ^ ks ^ "\n" ^ rs)::s)
 302                map [])
 303         in
 304         s ^ rest
 305   in
 306   to_string 0 trie
 307 ;;
 308