components/cic/discrimination_tree.ml

   1 (* Copyright (C) 2005, HELM Team.
   2  *
   3  * This file is part of HELM, an Hypertextual, Electronic
   4  * Library of Mathematics, developed at the Computer Science
   5  * Department, University of Bologna, Italy.
   6  *
   7  * HELM is free software; you can redistribute it and/or
   8  * modify it under the terms of the GNU General Public License
   9  * as published by the Free Software Foundation; either version 2
  10  * of the License, or (at your option) any later version.
  11  *
  12  * HELM is distributed in the hope that it will be useful,
  13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  15  * GNU General Public License for more details.
  16  *
  17  * You should have received a copy of the GNU General Public License
  18  * along with HELM; if not, write to the Free Software
  19  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
  20  * MA  02111-1307, USA.
  21  *
  22  * For details, see the HELM World-Wide-Web page,
  23  * http://cs.unibo.it/helm/.
  24  *)
  25
  26 (* $Id$ *)
  27
  28 module DiscriminationTreeIndexing =
  29   functor (A:Set.S) ->
  30     struct
  31
  32       type path_string_elem =
  33         | Function | Constant of UriManager.uri
  34         | Bound of int | Variable | Proposition | Datatype ;;
  35       type path_string = path_string_elem list;;
  36
  37
  38       (* needed by the retrieve_* functions, to know the arities of the
  39        * "functions" *)
  40
  41       let ppelem = function
  42         | Function -> "Fun"
  43         | Constant uri -> UriManager.name_of_uri uri
  44         | Bound i -> string_of_int i
  45         | Variable -> "?"
  46         | Proposition -> "Prop"
  47         | Datatype -> "Type"
  48       ;;
  49       let pppath l = String.concat "::" (List.map ppelem l) ;;
  50       let elem_of_cic = function
  51         | Cic.Meta _ -> Variable
  52         | Cic.Lambda _ -> Function
  53         | Cic.Rel i -> Bound i
  54         | Cic.Sort (Cic.Prop) -> Proposition
  55         | Cic.Sort _ -> Datatype
  56         | term ->
  57             try Constant (CicUtil.uri_of_term term)
  58             with Invalid_argument _ -> Variable (* HACK! *)
  59       ;;
  60       let path_string_of_term arities =
  61         let set_arity arities k n =
  62           (assert (k<>Variable || n=0);
  63           (k,n)::(List.remove_assoc k arities))
  64         in
  65         let rec aux arities = function
  66           | Cic.Appl ((hd::tl) as l) ->
  67               let arities =
  68                 set_arity arities (elem_of_cic hd) (List.length tl) in
  69               List.fold_left
  70                 (fun (arities,path) t ->
  71                    let arities,tpath = aux arities t in
  72                      arities,path@tpath)
  73                 (arities,[]) l
  74           | t -> arities, [elem_of_cic t]
  75         in
  76           aux arities
  77       ;;
  78       let compare_elem e1 e2 =
  79         match e1,e2 with
  80         | Constant u1,Constant u2 -> UriManager.compare u1 u2
  81         | e1,e2 -> Pervasives.compare e1 e2
  82       ;;
  83
  84       module OrderedPathStringElement = struct
  85         type t = path_string_elem
  86         let compare = compare_elem
  87       end
  88
  89       module PSMap = Map.Make(OrderedPathStringElement);;
  90
  91       type key = PSMap.key
  92
  93       module DiscriminationTree = Trie.Make(PSMap);;
  94
  95       type t = A.t DiscriminationTree.t * (path_string_elem*int) list
  96       let empty = DiscriminationTree.empty, [] ;;
  97
  98       let index (tree,arity) term info =
  99         let arity,ps = path_string_of_term arity term in
 100         let ps_set =
 101           try DiscriminationTree.find ps tree
 102           with Not_found -> A.empty in
 103         let tree = DiscriminationTree.add ps (A.add info ps_set) tree in
 104         tree,arity
 105       ;;
 106
 107       let remove_index (tree,arity) term info =
 108         let arity,ps = path_string_of_term arity term in
 109         try
 110           let ps_set = A.remove info (DiscriminationTree.find ps tree) in
 111           if A.is_empty ps_set then
 112             DiscriminationTree.remove ps tree,arity
 113           else
 114             DiscriminationTree.add ps ps_set tree,arity
 115         with Not_found ->
 116           tree,arity
 117       ;;
 118
 119       let in_index (tree,arity) term test =
 120         let arity,ps = path_string_of_term arity term in
 121         try
 122           let ps_set = DiscriminationTree.find ps tree in
 123           A.exists test ps_set
 124         with Not_found ->
 125           false
 126       ;;
 127
 128       let head_of_term = function
 129         | Cic.Appl (hd::tl) -> hd
 130         | term -> term
 131       ;;
 132
 133       let rec skip_prods = function
 134         | Cic.Prod (_,_,t) -> skip_prods t
 135         | term -> term
 136       ;;
 137
 138       let rec subterm_at_pos pos term =
 139         match pos with
 140           | [] -> term
 141           | index::pos ->
 142               match term with
 143                 | Cic.Appl l ->
 144                     (try subterm_at_pos pos (List.nth l index)
 145                      with Failure _ -> raise Not_found)
 146                 | _ -> raise Not_found
 147       ;;
 148
 149
 150       let rec after_t pos term =
 151         let pos' =
 152           match pos with
 153             | [] -> raise Not_found
 154             | pos ->
 155                 List.fold_right
 156                   (fun i r -> if r = [] then [i+1] else i::r) pos []
 157         in
 158           try
 159             ignore(subterm_at_pos pos' term ); pos'
 160           with Not_found ->
 161             let pos, _ =
 162               List.fold_right
 163                 (fun i (r, b) -> if b then (i::r, true) else (r, true))
 164                 pos ([], false)
 165             in
 166               after_t pos term
 167       ;;
 168
 169
 170       let next_t pos term =
 171         let t = subterm_at_pos pos term in
 172           try
 173             let _ = subterm_at_pos [1] t in
 174               pos @ [1]
 175           with Not_found ->
 176             match pos with
 177               | [] -> [1]
 178               | pos -> after_t pos term
 179       ;;
 180
 181       let retrieve_generalizations (tree,arity) term =
 182         let term = skip_prods term in
 183         let rec retrieve tree term pos =
 184           match tree with
 185             | DiscriminationTree.Node (Some s, _) when pos = [] -> s
 186             | DiscriminationTree.Node (_, map) ->
 187                 let res =
 188                   let hd_term =
 189                     elem_of_cic (head_of_term (subterm_at_pos pos term))
 190                   in
 191                   if hd_term = Variable then A.empty else
 192                   try
 193                     let n = PSMap.find hd_term map in
 194                       match n with
 195                         | DiscriminationTree.Node (Some s, _) -> s
 196                         | DiscriminationTree.Node (None, _) ->
 197                             let newpos =
 198                               try next_t pos term
 199                               with Not_found -> []
 200                             in
 201                               retrieve n term newpos
 202                   with Not_found ->
 203                     A.empty
 204                 in
 205                   try
 206                     let n = PSMap.find Variable map in
 207                     let newpos = try after_t pos term with Not_found -> [-1] in
 208                       if newpos = [-1] then
 209                         match n with
 210                           | DiscriminationTree.Node (Some s, _) -> A.union s res
 211                           | _ -> res
 212                       else
 213                         A.union res (retrieve n term newpos)
 214                   with Not_found ->
 215                     res
 216         in
 217           retrieve tree term []
 218       ;;
 219
 220
 221       let jump_list arities = function
 222         | DiscriminationTree.Node (value, map) ->
 223             let rec get n tree =
 224               match tree with
 225                 | DiscriminationTree.Node (v, m) ->
 226                     if n = 0 then
 227                       [tree]
 228                     else
 229                       PSMap.fold
 230                         (fun k v res ->
 231                            let a =
 232                              try List.assoc k arities
 233                              with Not_found -> 0
 234                            in
 235                              (get (n-1 + a) v) @ res) m []
 236             in
 237               PSMap.fold
 238                 (fun k v res ->
 239                    let arity =
 240                      try
 241                        List.assoc k arities
 242                      with Not_found -> 0 in
 243                      (get arity v) @ res)
 244                 map []
 245       ;;
 246
 247
 248       let retrieve_unifiables (tree,arities) term =
 249         let term = skip_prods term in
 250         let rec retrieve tree term pos =
 251           match tree with
 252             | DiscriminationTree.Node (Some s, _) when pos = [] -> s
 253             | DiscriminationTree.Node (_, map) ->
 254                 let subterm =
 255                   try Some (subterm_at_pos pos term) with Not_found -> None
 256                 in
 257                 match subterm with
 258                 | None -> A.empty
 259                 | Some (Cic.Meta _) ->
 260                       let newpos = try next_t pos term with Not_found -> [] in
 261                       let jl = jump_list arities tree in
 262                         List.fold_left
 263                           (fun r s -> A.union r s)
 264                           A.empty
 265                           (List.map (fun t -> retrieve t term newpos) jl)
 266                   | Some subterm ->
 267                       let res =
 268                         let hd_term = elem_of_cic (head_of_term subterm) in
 269                           if hd_term = Variable then
 270                            A.empty else
 271                         try
 272                           let n = PSMap.find hd_term map in
 273                             match n with
 274                               | DiscriminationTree.Node (Some s, _) -> s
 275                               | DiscriminationTree.Node (None, _) ->
 276                                   retrieve n term (next_t pos term)
 277                         with Not_found ->
 278                           A.empty
 279                       in
 280                         try
 281                           let n = PSMap.find Variable map in
 282                           let newpos =
 283                             try after_t pos term
 284                             with Not_found -> [-1]
 285                           in
 286                             if newpos = [-1] then
 287                               match n with
 288                                 | DiscriminationTree.Node (Some s, _) ->
 289                                     A.union s res
 290                                 | _ -> res
 291                             else
 292                               A.union res (retrieve n term newpos)
 293                         with Not_found ->
 294                           res
 295       in
 296         retrieve tree term []
 297   end
 298 ;;
 299