]> matita.cs.unibo.it Git - helm.git/blob - helm/software/components/cic/discrimination_tree.ml
Implicit annotationas are now printed
[helm.git] / 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 type DiscriminationTree =
109     sig
110
111       type input 
112       type data
113       type dataset
114       type constant_name
115       type t
116
117       val iter : t -> (constant_name path -> dataset -> unit) -> unit
118
119       val empty : t
120       val index : t -> input -> data -> t
121       val remove_index : t -> input -> data -> t
122       val in_index : t -> input -> (data -> bool) -> bool
123       val retrieve_generalizations : t -> input -> dataset
124       val retrieve_unifiables : t -> input -> dataset
125     end
126
127 module Make (I:Indexable) (A:Set.S) : DiscriminationTree 
128 with type constant_name = I.constant_name and type input = I.input
129 and type data = A.elt and type dataset = A.t =
130
131     struct
132
133       module OrderedPathStringElement = struct
134         type t = I.constant_name path_string_elem
135         let compare = I.compare
136       end
137
138       type constant_name = I.constant_name
139       type data = A.elt
140       type dataset = A.t
141       type input = I.input
142
143       module PSMap = Map.Make(OrderedPathStringElement);;
144
145       type key = PSMap.key
146
147       module DiscriminationTree = Trie.Make(PSMap);;
148
149       type t = A.t DiscriminationTree.t
150
151       let empty = DiscriminationTree.empty;;
152
153       let iter dt f = DiscriminationTree.iter (fun p x -> f p x) dt;;
154
155       let index tree term info =
156         let ps = I.path_string_of term in
157         let ps_set =
158           try DiscriminationTree.find ps tree with Not_found -> A.empty 
159         in
160         DiscriminationTree.add ps (A.add info ps_set) tree
161       ;;
162
163       let remove_index tree term info =
164         let ps = I.path_string_of term in
165         try
166           let ps_set = A.remove info (DiscriminationTree.find ps tree) in
167           if A.is_empty ps_set then DiscriminationTree.remove ps tree
168           else DiscriminationTree.add ps ps_set tree
169         with Not_found -> tree
170       ;;
171
172       let in_index tree term test =
173         let ps = I.path_string_of term in
174         try
175           let ps_set = DiscriminationTree.find ps tree in
176           A.exists test ps_set
177         with Not_found -> false
178       ;;
179
180       (* You have h(f(x,g(y,z)),t) whose path_string_of_term_with_jl is 
181          (h,2).(f,2).(x,0).(g,2).(y,0).(z,0).(t,0) and you are at f and want to
182          skip all its progeny, thus you want to reach t.
183       
184          You need to skip as many elements as the sum of all arieties contained
185           in the progeny of f.
186       
187          The input ariety is the one of f while the path is x.g....t  
188          Should be the equivalent of after_t in the literature (handbook A.R.)
189        *)
190       let rec skip arity path =
191         if arity = 0 then path else match path with 
192         | [] -> assert false 
193         | m::tl -> skip (arity-1+arity_of m) tl
194       ;;
195
196       (* the equivalent of skip, but on the index, thus the list of trees
197          that are rooted just after the term represented by the tree root
198          are returned (we are skipping the root) *)
199       let skip_root = function DiscriminationTree.Node (value, map) ->
200         let rec get n = function DiscriminationTree.Node (v, m) as tree ->
201            if n = 0 then [tree] else 
202            PSMap.fold (fun k v res -> (get (n-1 + arity_of k) v) @ res) m []
203         in
204           PSMap.fold (fun k v res -> (get (arity_of k) v) @ res) map []
205       ;;
206
207       let retrieve unif tree term =
208         let path = I.path_string_of term in
209         let rec retrieve path tree =
210           match tree, path with
211           | DiscriminationTree.Node (Some s, _), [] -> s
212           | DiscriminationTree.Node (None, _), [] -> A.empty 
213           | DiscriminationTree.Node (_, map), Variable::path when unif ->
214               List.fold_left A.union A.empty
215                 (List.map (retrieve path) (skip_root tree))
216           | DiscriminationTree.Node (_, map), node::path ->
217               A.union
218                  (if not unif && node = Variable then A.empty else
219                   try retrieve path (PSMap.find node map)
220                   with Not_found -> A.empty)
221                  (try
222                     match PSMap.find Variable map,skip (arity_of node) path with
223                     | DiscriminationTree.Node (Some s, _), [] -> s
224                     | n, path -> retrieve path n
225                   with Not_found -> A.empty)
226        in
227         retrieve path tree
228       ;;
229
230       let retrieve_generalizations tree term = retrieve false tree term;;
231       let retrieve_unifiables tree term = retrieve true tree term;;
232   end
233 ;;
234