]> matita.cs.unibo.it Git - helm.git/blob - helm/ocaml/cic/path_indexing.ml
moved term indexing (in both discrimination and path tree forms) from paramodulation...
[helm.git] / helm / ocaml / cic / path_indexing.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 (* path indexing implementation *)
27
28 (* position of the subterm, subterm (Appl are not stored...) *)
29
30 module PathIndexing =
31   functor(A:Set.S) -> 
32     struct
33
34 type path_string_elem = Index of int | Term of Cic.term;;
35 type path_string = path_string_elem list;; 
36
37
38 let rec path_strings_of_term index =
39   let module C = Cic in function
40   | C.Meta _ -> [ [Index index; Term (C.Implicit None)] ]
41   | C.Appl (hd::tl) ->
42       let p = if index > 0 then [Index index; Term hd] else [Term hd] in
43       let _, res = 
44         List.fold_left
45           (fun (i, r) t ->
46              let rr = path_strings_of_term i t in
47              (i+1, r @ (List.map (fun ps -> p @ ps) rr)))
48           (1, []) tl
49       in
50       res
51   | term -> [ [Index index; Term term] ]
52 ;;
53
54 (*
55 let string_of_path_string ps =
56   String.concat "."
57     (List.map
58        (fun e ->
59           let s =
60             match e with
61             | Index i -> "Index " ^ (string_of_int i)
62             | Term t -> "Term " ^ (CicPp.ppterm t)
63           in
64           "(" ^ s ^ ")")
65        ps)
66 ;;  
67 *)
68
69 module OrderedPathStringElement = struct
70   type t = path_string_elem
71
72   let compare t1 t2 =
73     match t1, t2 with
74     | Index i, Index j -> Pervasives.compare i j
75     | Term t1, Term t2 -> if t1 = t2 then 0 else Pervasives.compare t1 t2
76     | Index _, Term _ -> -1
77     | Term _, Index _ -> 1
78 end
79
80 module PSMap = Map.Make(OrderedPathStringElement);;
81
82 module PSTrie = Trie.Make(PSMap);;
83
84 type t = A.t PSTrie.t
85 type key = Cic.term
86 let empty = PSTrie.empty
87 let arities = Hashtbl.create 0
88
89 let index trie term info =
90   let ps = path_strings_of_term 0 term in
91   List.fold_left 
92   (fun trie ps ->
93      let ps_set = try PSTrie.find ps trie with Not_found -> A.empty in
94      let trie = PSTrie.add ps (A.add info ps_set) trie in
95        trie) trie ps
96
97 let remove_index trie term info=
98   let ps = path_strings_of_term 0 term in
99   List.fold_left
100     (fun trie ps ->
101        try
102         let ps_set = A.remove info (PSTrie.find ps trie) in
103         if A.is_empty ps_set then
104           PSTrie.remove ps trie
105         else
106           PSTrie.add ps ps_set trie
107        with Not_found -> trie) trie ps
108 ;;
109
110 let in_index trie term test =
111   let ps = path_strings_of_term 0 term in
112   let ok ps =
113     try
114       let set = PSTrie.find ps trie in
115         A.exists test set
116     with Not_found ->
117       false
118   in
119   List.exists ok ps
120 ;;
121
122
123 let head_of_term = function
124   | Cic.Appl (hd::tl) -> hd
125   | term -> term
126 ;;
127
128
129 let subterm_at_pos index term =
130   if index = 0 then
131     term
132   else
133     match term with
134     | Cic.Appl l ->
135         (try List.nth l index with Failure _ -> raise Not_found)
136     | _ -> raise Not_found
137 ;;
138
139
140 let rec retrieve_generalizations trie term =
141   match trie with
142   | PSTrie.Node (value, map) ->
143       let res = 
144         match term with
145         | Cic.Meta _ -> A.empty
146         | term ->
147             let hd_term = head_of_term term in
148             try
149               let n = PSMap.find (Term hd_term) map in
150               match n with
151               | PSTrie.Node (Some s, _) -> s
152               | PSTrie.Node (None, m) ->
153                   let l = 
154                     PSMap.fold
155                       (fun k v res ->
156                          match k with
157                          | Index i ->
158                              let t = subterm_at_pos i term in
159                              let s = retrieve_generalizations v t in
160                              s::res
161                          | _ -> res)
162                       m []
163                   in
164                   match l with
165                   | hd::tl ->
166                       List.fold_left (fun r s -> A.inter r s) hd tl
167                   | _ -> A.empty
168             with Not_found ->
169               A.empty
170       in
171       try
172         let n = PSMap.find (Term (Cic.Implicit None)) map in
173         match n with
174         | PSTrie.Node (Some s, _) -> A.union res s
175         | _ -> res
176       with Not_found ->
177         res
178 ;;
179
180
181 let rec retrieve_unifiables trie term =
182   match trie with
183   | PSTrie.Node (value, map) ->
184       let res = 
185         match term with
186         | Cic.Meta _ ->
187             PSTrie.fold
188               (fun ps v res -> A.union res v)
189               (PSTrie.Node (None, map))
190               A.empty
191         | _ ->
192             let hd_term = head_of_term term in
193             try
194               let n = PSMap.find (Term hd_term) map in
195               match n with
196               | PSTrie.Node (Some v, _) -> v
197               | PSTrie.Node (None, m) ->
198                   let l = 
199                     PSMap.fold
200                       (fun k v res ->
201                          match k with
202                          | Index i ->
203                              let t = subterm_at_pos i term in
204                              let s = retrieve_unifiables v t in
205                              s::res
206                          | _ -> res)
207                       m []
208                   in
209                   match l with
210                   | hd::tl ->
211                       List.fold_left (fun r s -> A.inter r s) hd tl
212                   | _ -> A.empty
213             with Not_found ->
214               A.empty
215       in
216       try
217         let n = PSMap.find (Term (Cic.Implicit None)) map in
218         match n with
219         | PSTrie.Node (Some s, _) -> A.union res s
220         | _ -> res
221       with Not_found ->
222         res
223 ;;
224
225 end