helm/ocaml/paramodulation/discrimination_tree.ml

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