helm/software/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 type path_string_elem =
  29   | Constant of UriManager.uri * int (* name, arity *)
  30   | Bound of int * int (* rel, arity *)
  31   | Variable (* arity is 0 *)
  32   | Proposition (* arity is 0 *)
  33   | Datatype (* arity is 0 *)
  34   | Dead (* arity is 0 *)
  35 ;;
  36
  37 let arity_of = function
  38   | Constant (_,a)
  39   | Bound (_,a) -> a
  40   | _ -> 0
  41 ;;
  42
  43 type path = path_string_elem list;;
  44
  45 let ppelem = function
  46   | Constant (uri,arity) ->
  47       "("^UriManager.name_of_uri uri ^ "," ^ string_of_int arity^")"
  48   | Bound (i,arity) ->
  49       "("^string_of_int i ^ "," ^ string_of_int arity^")"
  50   | Variable -> "?"
  51   | Proposition -> "Prop"
  52   | Datatype -> "Type"
  53   | Dead -> "Dead"
  54 ;;
  55
  56 let path_string_of_term_with_jl =
  57   let rec aux arity = function
  58     | Cic.Appl ((Cic.Meta _|Cic.Implicit _)::_) -> [Variable]
  59     | Cic.Appl (Cic.Lambda _ :: _) -> [Variable] (* maybe we should b-reduce *)
  60     | Cic.Appl [] -> assert false
  61     | Cic.Appl (hd::tl) ->
  62         aux (List.length tl) hd @ List.flatten (List.map (aux 0) tl)
  63     | Cic.Cast (t,_) -> aux arity t
  64     | Cic.Lambda (_,s,t) | Cic.Prod (_,s,t) -> [Variable]
  65         (* I think we should CicSubstitution.subst Implicit t *)
  66     | Cic.LetIn (_,s,_,t) -> [Variable] (* z-reduce? *)
  67     | Cic.Meta _ | Cic.Implicit _ -> assert (arity = 0); [Variable]
  68     | Cic.Rel i -> [Bound (i, arity)]
  69     | Cic.Sort (Cic.Prop) -> assert (arity=0); [Proposition]
  70     | Cic.Sort _ -> assert (arity=0); [Datatype]
  71     | Cic.Const _ | Cic.Var _ | Cic.MutInd _ | Cic.MutConstruct _ as t ->
  72         [Constant (CicUtil.uri_of_term t, arity)]
  73     | Cic.MutCase _ | Cic.Fix _ | Cic.CoFix _ -> [Dead]
  74   in
  75     aux 0
  76 ;;
  77
  78 let compare_elem e1 e2 =
  79   match e1,e2 with
  80   | Constant (u1,a1),Constant (u2,a2) ->
  81        let x = UriManager.compare u1 u2 in
  82        if x = 0 then Pervasives.compare a1 a2 else x
  83   | e1,e2 -> Pervasives.compare e1 e2
  84 ;;
  85
  86 let string_of_path l = String.concat "." (List.map ppelem l) ;;
  87
  88 module DiscriminationTreeIndexing =
  89   functor (A:Set.S) ->
  90     struct
  91
  92       module OrderedPathStringElement = struct
  93         type t = path_string_elem
  94         let compare = compare_elem
  95       end
  96
  97       module PSMap = Map.Make(OrderedPathStringElement);;
  98
  99       type key = PSMap.key
 100
 101       module DiscriminationTree = Trie.Make(PSMap);;
 102
 103       type t = A.t DiscriminationTree.t
 104
 105       let empty = DiscriminationTree.empty;;
 106
 107       let iter dt f = DiscriminationTree.iter (fun p x -> f p x) dt;;
 108
 109       let index tree term info =
 110         let ps = path_string_of_term_with_jl term in
 111         let ps_set =
 112           try DiscriminationTree.find ps tree with Not_found -> A.empty
 113         in
 114         DiscriminationTree.add ps (A.add info ps_set) tree
 115       ;;
 116
 117       let remove_index tree term info =
 118         let ps = path_string_of_term_with_jl term in
 119         try
 120           let ps_set = A.remove info (DiscriminationTree.find ps tree) in
 121           if A.is_empty ps_set then DiscriminationTree.remove ps tree
 122           else DiscriminationTree.add ps ps_set tree
 123         with Not_found -> tree
 124       ;;
 125
 126       let in_index tree term test =
 127         let ps = path_string_of_term_with_jl term in
 128         try
 129           let ps_set = DiscriminationTree.find ps tree in
 130           A.exists test ps_set
 131         with Not_found -> false
 132       ;;
 133
 134       (* You have h(f(x,g(y,z)),t) whose path_string_of_term_with_jl is
 135          (h,2).(f,2).(x,0).(g,2).(y,0).(z,0).(t,0) and you are at f and want to
 136          skip all its progeny, thus you want to reach t.
 137
 138          You need to skip as many elements as the sum of all arieties contained
 139           in the progeny of f.
 140
 141          The input ariety is the one of f while the path is x.g....t
 142          Should be the equivalent of after_t in the literature (handbook A.R.)
 143        *)
 144       let rec skip arity path =
 145         if arity = 0 then path else match path with
 146         | [] -> assert false
 147         | m::tl -> skip (arity-1+arity_of m) tl
 148       ;;
 149
 150       (* the equivalent of skip, but on the index, thus the list of trees
 151          that are rooted just after the term represented by the tree root
 152          are returned (we are skipping the root) *)
 153       let skip_root = function DiscriminationTree.Node (value, map) ->
 154         let rec get n = function DiscriminationTree.Node (v, m) as tree ->
 155            if n = 0 then [tree] else
 156            PSMap.fold (fun k v res -> (get (n-1 + arity_of k) v) @ res) m []
 157         in
 158           PSMap.fold (fun k v res -> (get (arity_of k) v) @ res) map []
 159       ;;
 160
 161       let retrieve unif tree term =
 162         let path = path_string_of_term_with_jl term in
 163         let rec retrieve path tree =
 164           match tree, path with
 165           | DiscriminationTree.Node (Some s, _), [] -> s
 166           | DiscriminationTree.Node (None, _), [] -> A.empty
 167           | DiscriminationTree.Node (_, map), Variable::path when unif ->
 168               List.fold_left A.union A.empty
 169                 (List.map (retrieve path) (skip_root tree))
 170           | DiscriminationTree.Node (_, map), node::path ->
 171               A.union
 172                  (if not unif && node = Variable then A.empty else
 173                   try retrieve path (PSMap.find node map)
 174                   with Not_found -> A.empty)
 175                  (try
 176                     match PSMap.find Variable map,skip (arity_of node) path with
 177                     | DiscriminationTree.Node (Some s, _), [] -> s
 178                     | n, path -> retrieve path n
 179                   with Not_found -> A.empty)
 180        in
 181         retrieve path tree
 182       ;;
 183
 184       let retrieve_generalizations tree term = retrieve false tree term;;
 185       let retrieve_unifiables tree term = retrieve true tree term;;
 186   end
 187 ;;
 188