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 module OrderedPathStringElement = struct
  20   type t = path_string_elem
  21
  22   let compare = Pervasives.compare
  23 end
  24
  25 module PSMap = Map.Make(OrderedPathStringElement);;
  26
  27
  28 module DiscriminationTree = struct
  29   type key = path_string
  30   type t = Node of (Utils.pos * Inference.equality) option * (t PSMap.t)
  31
  32   let empty = Node (None, PSMap.empty)
  33
  34   let rec find l t =
  35     match (l, t) with
  36     | [], Node (None, _) -> raise Not_found
  37     | [], Node (Some v, _) -> v
  38     | x::r, Node (_, m) -> find r (PSMap.find x m)
  39
  40   let rec mem l t =
  41     match (l, t) with
  42     | [], Node (None, _) -> false
  43     | [], Node (Some _, _) -> true
  44     | x::r, Node (_, m) -> try mem r (PSMap.find x m) with Not_found -> false
  45
  46   let add l v t =
  47     let rec ins = function
  48       | [], Node (_, m) -> Node (Some v, m)
  49       | x::r, Node (v, m) ->
  50           let t' = try PSMap.find x m with Not_found -> empty in
  51           let t'' = ins (r, t') in
  52           Node (v, PSMap.add x t'' m)
  53     in
  54     ins (l, t)
  55
  56   let rec remove l t =
  57     match (l, t) with
  58     | [], Node (_, m) -> Node (None, m)
  59     | x::r, Node (v, m) ->
  60         try
  61           let t' = remove r (PSMap.find x m) in
  62           Node (v, if t' = empty then PSMap.remove x m else PSMap.add x t' m)
  63         with Not_found ->
  64           t
  65
  66   let rec fold f t acc =
  67     let rec traverse revp t acc = match t with
  68       | Node (None, m) ->
  69           PSMap.fold (fun x -> traverse (x::revp)) m acc
  70       | Node (Some v, m) ->
  71           f (List.rev revp) v (PSMap.fold (fun x -> traverse (x::revp)) m acc)
  72     in
  73     traverse [] t acc
  74
  75 end
  76
  77
  78 let index tree equality =
  79   let _, (_, l, r, ordering), _, _ = equality in
  80   let psl = path_string_of_term l
  81   and psr = path_string_of_term r in
  82   match ordering with
  83   | Utils.Gt -> DiscriminationTree.add psl (Utils.Left, equality) tree
  84   | Utils.Lt -> DiscriminationTree.add psr (Utils.Right, equality) tree
  85   | _ ->
  86       let tree = DiscriminationTree.add psl (Utils.Left, equality) tree in
  87       DiscriminationTree.add psr (Utils.Right, equality) tree
  88 ;;
  89
  90
  91 let remove_index tree equality =
  92   let _, (_, l, r, ordering), _, _ = equality in
  93   let psl = path_string_of_term l
  94   and psr = path_string_of_term r in
  95   match ordering with
  96   | Utils.Gt -> DiscriminationTree.remove psl tree
  97   | Utils.Lt -> DiscriminationTree.remove psr tree
  98   | _ ->
  99       let tree = DiscriminationTree.remove psl tree in
 100       DiscriminationTree.remove psr tree
 101 ;;
 102
 103
 104 let in_index tree equality =
 105   let _, (_, l, r, ordering), _, _ = equality in
 106   let psl = path_string_of_term l
 107   and psr = path_string_of_term r in
 108   let meta_convertibility = Inference.meta_convertibility_eq equality in
 109   let ok ps =
 110     try let _, eq = DiscriminationTree.find ps tree in meta_convertibility eq
 111     with Not_found -> false
 112   in
 113   (ok psl) || (ok psr)
 114 ;;
 115
 116
 117 let head_of_term = function
 118   | Cic.Appl (hd::tl) -> hd
 119   | term -> term
 120 ;;
 121
 122
 123 let rec subterm_at_pos pos term =
 124   match pos with
 125   | [] -> term
 126   | index::pos ->
 127       match term with
 128       | Cic.Appl l ->
 129           (try subterm_at_pos pos (List.nth l index) with _ -> raise Not_found)
 130       | _ -> raise Not_found
 131 ;;
 132
 133
 134 let next_t pos term =
 135   let t = subterm_at_pos pos term in
 136   try
 137     let t2 = subterm_at_pos [1] t in
 138     pos @ [1]
 139   with Not_found ->
 140     match pos with
 141     | [] -> [1]
 142     | pos -> List.fold_right (fun i r -> if r = [] then [i+1] else i::r) pos []
 143 ;;
 144
 145
 146 let rec after_t pos term =
 147   let pos' =
 148     match pos with
 149     | [] -> raise Not_found
 150     | pos -> List.fold_right (fun i r -> if r = [] then [i+1] else i::r) pos []
 151   in
 152   try
 153     let t = subterm_at_pos pos' term in pos'
 154   with Not_found ->
 155     let pos, _ =
 156       List.fold_right
 157         (fun i (r, b) -> if b then (i::r, true) else (r, true)) pos ([], false)
 158     in
 159     after_t pos term
 160 ;;
 161
 162
 163 let retrieve_generalizations tree term =
 164   let rec retrieve tree term pos =
 165     match tree with
 166     | DiscriminationTree.Node (value, map) ->
 167         let res =
 168           try
 169             let hd_term = head_of_term (subterm_at_pos pos term) in
 170             let n = PSMap.find hd_term map in
 171             match n with
 172             | DiscriminationTree.Node (Some s, _) -> [s]
 173             | DiscriminationTree.Node (None, _) ->
 174                 retrieve n term (next_t pos term)
 175           with Not_found ->
 176             []
 177         in
 178         try
 179           let n = PSMap.find (Cic.Implicit None) map in
 180           res @ (retrieve n term (after_t pos term))
 181         with Not_found ->
 182           res
 183   in
 184   retrieve tree term []
 185 ;;
 186
 187
 188 let jump_list = function
 189   | DiscriminationTree.Node (value, map) ->
 190       let rec get n tree =
 191         match tree with
 192         | DiscriminationTree.Node (v, m) ->
 193             if n = 0 then
 194               [tree]
 195             else
 196               PSMap.fold
 197                 (fun k v res ->
 198                    let a = try Hashtbl.find arities k with Not_found -> 0 in
 199                    (get (n-1 + a) v) @ res) m []
 200       in
 201       PSMap.fold
 202         (fun k v res ->
 203            let arity = try Hashtbl.find arities k with Not_found -> 0 in
 204            (get arity v) @ res)
 205         map []
 206 ;;
 207
 208
 209 let retrieve_unifiables tree term =
 210   let rec retrieve tree term pos =
 211     match tree with
 212     | DiscriminationTree.Node (value, map) ->
 213         let res =
 214           try
 215             match subterm_at_pos pos term with
 216             | Cic.Meta _ ->
 217                 List.concat
 218                   (List.map
 219                      (fun t -> retrieve t term (next_t pos term))
 220                      (jump_list tree))
 221             | subterm ->
 222                 let hd_term = head_of_term subterm in
 223                 let n = PSMap.find hd_term map in
 224                 match n with
 225                 | DiscriminationTree.Node (Some s, _) -> [s]
 226                 | DiscriminationTree.Node (None, _) ->
 227                     retrieve n term (next_t pos term)
 228           with Not_found ->
 229             []
 230         in
 231         try
 232           let n = PSMap.find (Cic.Implicit None) map in
 233           res @ (retrieve n term (after_t pos term))
 234         with Not_found ->
 235           res
 236   in
 237   retrieve tree term []
 238 ;;