helm/software/components/ng_refiner/discrimination_tree.ml

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