helm/software/components/ng_refiner/nDiscriminationTree.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 (NReference.Ref (u,_)) -> Constant u
  42         | NCic.Appl _ ->
  43             assert false (* should not happen *)
  44         | NCic.LetIn _ | NCic.Lambda _ | NCic.Prod _ | NCic.Match _ ->
  45             prerr_endline "FIXME: the discrimination tree receives an invalid term";
  46             Dead
  47             (* assert false universe.ml removes these *)
  48       ;;
  49       let path_string_of_term arities =
  50         let set_arity arities k n =
  51           (assert (k<>Variable || n=0);
  52           if k = Dead then arities else (k,n)::(List.remove_assoc k arities))
  53         in
  54         let rec aux arities = function
  55           | NCic.Appl ((hd::tl) as l) ->
  56               let arities =
  57                 set_arity arities (elem_of_cic hd) (List.length tl) in
  58               List.fold_left
  59                 (fun (arities,path) t ->
  60                    let arities,tpath = aux arities t in
  61                      arities,path@tpath)
  62                 (arities,[]) l
  63           | t -> arities, [elem_of_cic t]
  64         in
  65           aux arities
  66       ;;
  67       let compare_elem e1 e2 =
  68         match e1,e2 with
  69         | Constant u1,Constant u2 -> assert false (*NUri.compare u1 u2*)
  70         | e1,e2 -> Pervasives.compare e1 e2
  71       ;;
  72
  73       module OrderedPathStringElement = struct
  74         type t = path_string_elem
  75         let compare = compare_elem
  76       end
  77
  78       module PSMap = Map.Make(OrderedPathStringElement);;
  79
  80       type key = PSMap.key
  81
  82       module DiscriminationTree = Trie.Make(PSMap);;
  83
  84       type t = A.t DiscriminationTree.t * (path_string_elem*int) list
  85       let empty = DiscriminationTree.empty, [] ;;
  86
  87       let iter (dt, _ ) f =
  88         DiscriminationTree.iter (fun _ x -> f x) dt
  89       ;;
  90
  91       let index (tree,arity) term info =
  92         let arity,ps = path_string_of_term arity term in
  93         let ps_set =
  94           try DiscriminationTree.find ps tree
  95           with Not_found -> A.empty in
  96         let tree = DiscriminationTree.add ps (A.add info ps_set) tree in
  97         tree,arity
  98       ;;
  99
 100       let remove_index (tree,arity) term info =
 101         let arity,ps = path_string_of_term arity term in
 102         try
 103           let ps_set = A.remove info (DiscriminationTree.find ps tree) in
 104           if A.is_empty ps_set then
 105             DiscriminationTree.remove ps tree,arity
 106           else
 107             DiscriminationTree.add ps ps_set tree,arity
 108         with Not_found ->
 109           tree,arity
 110       ;;
 111
 112       let in_index (tree,arity) term test =
 113         let arity,ps = path_string_of_term arity term in
 114         try
 115           let ps_set = DiscriminationTree.find ps tree in
 116           A.exists test ps_set
 117         with Not_found ->
 118           false
 119       ;;
 120
 121       let head_of_term = function
 122         | NCic.Appl (hd::tl) -> hd
 123         | term -> term
 124       ;;
 125
 126       let rec skip_prods = function
 127         | NCic.Prod (_,_,t) -> skip_prods t
 128         | term -> term
 129       ;;
 130
 131       let rec subterm_at_pos pos term =
 132         match pos with
 133           | [] -> term
 134           | index::pos ->
 135               match term with
 136                 | NCic.Appl l ->
 137                     (try subterm_at_pos pos (List.nth l index)
 138                      with Failure _ -> raise Not_found)
 139                 | _ -> raise Not_found
 140       ;;
 141
 142
 143       let rec after_t pos term =
 144         let pos' =
 145           match pos with
 146             | [] -> raise Not_found
 147             | pos ->
 148                 List.fold_right
 149                   (fun i r -> if r = [] then [i+1] else i::r) pos []
 150         in
 151           try
 152             ignore(subterm_at_pos pos' term ); pos'
 153           with Not_found ->
 154             let pos, _ =
 155               List.fold_right
 156                 (fun i (r, b) -> if b then (i::r, true) else (r, true))
 157                 pos ([], false)
 158             in
 159               after_t pos term
 160       ;;
 161
 162
 163       let next_t pos term =
 164         let t = subterm_at_pos pos term in
 165           try
 166             let _ = subterm_at_pos [1] t in
 167               pos @ [1]
 168           with Not_found ->
 169             match pos with
 170               | [] -> [1]
 171               | pos -> after_t pos term
 172       ;;
 173
 174       let retrieve_generalizations (tree,arity) term =
 175         let term = skip_prods term in
 176         let rec retrieve tree term pos =
 177           match tree with
 178             | DiscriminationTree.Node (Some s, _) when pos = [] -> s
 179             | DiscriminationTree.Node (_, map) ->
 180                 let res =
 181                   let hd_term =
 182                     elem_of_cic (head_of_term (subterm_at_pos pos term))
 183                   in
 184                   if hd_term = Variable then A.empty else
 185                   try
 186                     let n = PSMap.find hd_term map in
 187                       match n with
 188                         | DiscriminationTree.Node (Some s, _) -> s
 189                         | DiscriminationTree.Node (None, _) ->
 190                             let newpos =
 191                               try next_t pos term
 192                               with Not_found -> []
 193                             in
 194                               retrieve n term newpos
 195                   with Not_found ->
 196                     A.empty
 197                 in
 198                   try
 199                     let n = PSMap.find Variable map in
 200                     let newpos = try after_t pos term with Not_found -> [-1] in
 201                       if newpos = [-1] then
 202                         match n with
 203                           | DiscriminationTree.Node (Some s, _) -> A.union s res
 204                           | _ -> res
 205                       else
 206                         A.union res (retrieve n term newpos)
 207                   with Not_found ->
 208                     res
 209         in
 210           retrieve tree term []
 211       ;;
 212
 213
 214       let jump_list arities = function
 215         | DiscriminationTree.Node (value, map) ->
 216             let rec get n tree =
 217               match tree with
 218                 | DiscriminationTree.Node (v, m) ->
 219                     if n = 0 then
 220                       [tree]
 221                     else
 222                       PSMap.fold
 223                         (fun k v res ->
 224                            let a =
 225                              try List.assoc k arities
 226                              with Not_found -> 0
 227                            in
 228                              (get (n-1 + a) v) @ res) m []
 229             in
 230               PSMap.fold
 231                 (fun k v res ->
 232                    let arity =
 233                      try
 234                        List.assoc k arities
 235                      with Not_found -> 0 in
 236                      (get arity v) @ res)
 237                 map []
 238       ;;
 239
 240
 241       let retrieve_unifiables (tree,arities) term =
 242         let term = skip_prods term in
 243         let rec retrieve tree term pos =
 244           match tree with
 245             | DiscriminationTree.Node (Some s, _) when pos = [] -> s
 246             | DiscriminationTree.Node (_, map) ->
 247                 let subterm =
 248                   try Some (subterm_at_pos pos term) with Not_found -> None
 249                 in
 250                 match subterm with
 251                 | None -> A.empty
 252                 | Some (NCic.Meta _) ->
 253                       let newpos = try next_t pos term with Not_found -> [] in
 254                       let jl = jump_list arities tree in
 255                         List.fold_left
 256                           (fun r s -> A.union r s)
 257                           A.empty
 258                           (List.map (fun t -> retrieve t term newpos) jl)
 259                   | Some subterm ->
 260                       let res =
 261                         let hd_term = elem_of_cic (head_of_term subterm) in
 262                           if hd_term = Variable then
 263                            A.empty else
 264                         try
 265                           let n = PSMap.find hd_term map in
 266                             match n with
 267                               | DiscriminationTree.Node (Some s, _) -> s
 268                               | DiscriminationTree.Node (None, _) ->
 269                                   retrieve n term (next_t pos term)
 270                         with Not_found ->
 271                           A.empty
 272                       in
 273                         try
 274                           let n = PSMap.find Variable map in
 275                           let newpos =
 276                             try after_t pos term
 277                             with Not_found -> [-1]
 278                           in
 279                             if newpos = [-1] then
 280                               match n with
 281                                 | DiscriminationTree.Node (Some s, _) ->
 282                                     A.union s res
 283                                 | _ -> res
 284                             else
 285                               A.union res (retrieve n term newpos)
 286                         with Not_found ->
 287                           res
 288       in
 289         retrieve tree term []
 290   end
 291 ;;
 292