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