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