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