]> matita.cs.unibo.it Git - helm.git/blob - helm/ocaml/paramodulation/discrimination_tree.ml
may fix the nigtly build
[helm.git] / helm / ocaml / paramodulation / discrimination_tree.ml
1 type path_string_elem = Cic.term;;
2 type path_string = path_string_elem list;;
3
4
5 (* needed by the retrieve_* functions, to know the arities of the "functions" *)
6 let arities = Hashtbl.create 11;;
7
8
9 let rec path_string_of_term = function
10   | Cic.Meta _ -> [Cic.Implicit None]
11   | Cic.Appl ((hd::tl) as l) ->
12       if not (Hashtbl.mem arities hd) then
13         Hashtbl.add arities hd (List.length tl);
14       List.concat (List.map path_string_of_term l)
15   | term -> [term]
16 ;;
17
18
19 let string_of_path_string ps =
20   String.concat "." (List.map CicPp.ppterm ps)
21 ;;
22
23
24 module OrderedPathStringElement = struct
25   type t = path_string_elem
26
27   let compare = Pervasives.compare
28 end
29
30 module PSMap = Map.Make(OrderedPathStringElement);;
31
32
33 module OrderedPosEquality = struct
34   type t = Utils.pos * Inference.equality
35
36   let compare = Pervasives.compare
37 end
38
39 module PosEqSet = Set.Make(OrderedPosEquality);;
40
41
42 module DiscriminationTree = Trie.Make(PSMap);;
43
44
45 (*
46 module DiscriminationTree = struct
47   type key = path_string
48   type t = Node of PosEqSet.t option * (t PSMap.t)
49
50   let empty = Node (None, PSMap.empty)
51
52   let rec find l t =
53     match (l, t) with
54     | [], Node (None, _) -> raise Not_found
55     | [], Node (Some v, _) -> v
56     | x::r, Node (_, m) -> find r (PSMap.find x m)
57         
58   let rec mem l t =
59     match (l, t) with
60     | [], Node (None, _) -> false
61     | [], Node (Some _, _) -> true
62     | x::r, Node (_, m) -> try mem r (PSMap.find x m) with Not_found -> false
63
64   let add l v t =
65     let rec ins = function
66       | [], Node (_, m) -> Node (Some v, m)
67       | x::r, Node (v, m) ->
68           let t' = try PSMap.find x m with Not_found -> empty in
69           let t'' = ins (r, t') in
70           Node (v, PSMap.add x t'' m)
71     in
72     ins (l, t)
73
74   let rec remove l t =
75     match (l, t) with
76     | [], Node (_, m) -> Node (None, m)
77     | x::r, Node (v, m) ->
78         try
79           let t' = remove r (PSMap.find x m) in
80           let m' = if t' = empty then PSMap.remove x m else PSMap.add x t' m in
81           Node (v, m')
82         with Not_found ->
83           t
84
85   let rec fold f t acc =
86     let rec traverse revp t acc = match t with
87       | Node (None, m) -> 
88           PSMap.fold (fun x -> traverse (x::revp)) m acc
89       | Node (Some v, m) -> 
90           f (List.rev revp) v (PSMap.fold (fun x -> traverse (x::revp)) m acc)
91     in
92     traverse [] t acc
93
94 end
95 *)
96
97   
98 let string_of_discrimination_tree tree =
99   let rec to_string level = function
100     | DiscriminationTree.Node (value, map) ->
101         let s =
102           match value with
103           | Some v ->
104               (String.make (2 * level) ' ') ^
105                 "{" ^ (String.concat "; "
106                          (List.map
107                             (fun (p, e) ->
108                                "(" ^ (Utils.string_of_pos p) ^ ", " ^ 
109                                  (Inference.string_of_equality e) ^ ")")
110                             (PosEqSet.elements v))) ^ "}"
111           | None -> "" 
112         in
113         let rest =
114           String.concat "\n"
115             (PSMap.fold
116                (fun k v s ->
117                   let ks = CicPp.ppterm k in
118                   let rs = to_string (level+1) v in
119                   ((String.make (2 * level) ' ') ^ ks ^ "\n" ^ rs)::s)
120                map [])
121         in
122         s ^ rest
123   in
124   to_string 0 tree
125 ;;
126
127
128 let index tree equality =
129   let _, (_, l, r, ordering), _, _ = equality in
130   let psl = path_string_of_term l
131   and psr = path_string_of_term r in
132   let index pos tree ps =
133     let ps_set =
134       try DiscriminationTree.find ps tree with Not_found -> PosEqSet.empty in
135     let tree =
136       DiscriminationTree.add ps (PosEqSet.add (pos, equality) ps_set) tree in
137     tree
138   in
139   match ordering with
140   | Utils.Gt -> index Utils.Left tree psl
141   | Utils.Lt -> index Utils.Right tree psr
142   | _ ->
143       let tree = index Utils.Left tree psl in
144       index Utils.Right tree psr
145 ;;
146
147
148 let remove_index tree equality =
149   let _, (_, l, r, ordering), _, _ = equality in
150   let psl = path_string_of_term l
151   and psr = path_string_of_term r in
152   let remove_index pos tree ps =
153     try
154       let ps_set =
155         PosEqSet.remove (pos, equality) (DiscriminationTree.find ps tree) in
156       if PosEqSet.is_empty ps_set then
157         DiscriminationTree.remove ps tree
158       else
159         DiscriminationTree.add ps ps_set tree
160     with Not_found ->
161       tree
162   in
163   match ordering with
164   | Utils.Gt -> remove_index Utils.Left tree psl
165   | Utils.Lt -> remove_index Utils.Right tree psr
166   | _ ->
167       let tree = remove_index Utils.Left tree psl in
168       remove_index Utils.Right tree psr
169 ;;
170
171
172 let in_index tree equality =
173   let _, (_, l, r, ordering), _, _ = equality in
174   let psl = path_string_of_term l
175   and psr = path_string_of_term r in
176   let meta_convertibility = Inference.meta_convertibility_eq equality in
177   let ok ps =
178     try
179       let set = DiscriminationTree.find ps tree in
180       PosEqSet.exists (fun (p, e) -> meta_convertibility e) set
181     with Not_found ->
182       false
183   in
184   (ok psl) || (ok psr)
185 ;;
186
187
188 let head_of_term = function
189   | Cic.Appl (hd::tl) -> hd
190 (*   | Cic.Meta _ -> Cic.Implicit None *)
191   | term -> term
192 ;;
193
194
195 let rec subterm_at_pos pos term =
196   match pos with
197   | [] -> term
198   | index::pos ->
199       match term with
200       | Cic.Appl l ->
201           (try subterm_at_pos pos (List.nth l index) with _ -> raise Not_found)
202       | _ -> raise Not_found
203 ;;
204
205
206 let rec after_t pos term =
207   let pos' =
208     match pos with
209     | [] -> raise Not_found
210     | pos -> List.fold_right (fun i r -> if r = [] then [i+1] else i::r) pos []
211   in
212   try
213     let t = subterm_at_pos pos' term in pos'
214   with Not_found ->
215     let pos, _ =
216       List.fold_right
217         (fun i (r, b) -> if b then (i::r, true) else (r, true)) pos ([], false)
218     in
219     after_t pos term
220 ;;
221
222
223 let next_t pos term =
224   let t = subterm_at_pos pos term in
225   try
226     let _ = subterm_at_pos [1] t in
227     pos @ [1]
228   with Not_found ->
229     match pos with
230     | [] -> [1]
231     | pos -> after_t pos term
232 ;;     
233
234
235 let retrieve_generalizations tree term =
236   let rec retrieve tree term pos =
237     match tree with
238     | DiscriminationTree.Node (Some s, _) when pos = [] -> s
239     | DiscriminationTree.Node (_, map) ->
240         let res =
241           try
242             let hd_term = head_of_term (subterm_at_pos pos term) in
243             let n = PSMap.find hd_term map in
244             match n with
245             | DiscriminationTree.Node (Some s, _) -> s
246             | DiscriminationTree.Node (None, _) ->
247                 let newpos = try next_t pos term with Not_found -> [] in
248                 retrieve n term newpos
249           with Not_found ->
250             PosEqSet.empty
251         in
252         try
253           let n = PSMap.find (Cic.Implicit None) map in
254           let newpos = try after_t pos term with _ -> [-1] in
255           if newpos = [-1] then
256             match n with
257             | DiscriminationTree.Node (Some s, _) -> PosEqSet.union s res
258             | _ -> res
259           else
260             PosEqSet.union res (retrieve n term newpos)
261         with Not_found ->
262           res
263   in
264   retrieve tree term []
265 ;;
266
267
268 let jump_list = function
269   | DiscriminationTree.Node (value, map) ->
270       let rec get n tree =
271         match tree with
272         | DiscriminationTree.Node (v, m) ->
273             if n = 0 then
274               [tree]
275             else
276               PSMap.fold
277                 (fun k v res ->
278                    let a = try Hashtbl.find arities k with Not_found -> 0 in
279                    (get (n-1 + a) v) @ res) m []
280       in
281       PSMap.fold
282         (fun k v res ->
283            let arity = try Hashtbl.find arities k with Not_found -> 0 in
284            (get arity v) @ res)
285         map []
286 ;;
287
288
289 let retrieve_unifiables tree term =
290   let rec retrieve tree term pos =
291     match tree with
292     | DiscriminationTree.Node (Some s, _) when pos = [] -> s
293     | DiscriminationTree.Node (_, map) ->
294         let subterm =
295           try Some (subterm_at_pos pos term) with Not_found -> None
296         in
297         match subterm with
298         | None -> PosEqSet.empty
299         | Some (Cic.Meta _) ->
300             let newpos = try next_t pos term with Not_found -> [] in
301             let jl = jump_list tree in
302             List.fold_left
303               (fun r s -> PosEqSet.union r s)
304               PosEqSet.empty
305               (List.map (fun t -> retrieve t term newpos) jl)
306         | Some subterm ->
307             let res = 
308               try
309                 let hd_term = head_of_term subterm in
310                 let n = PSMap.find hd_term map in
311                 match n with
312                 | DiscriminationTree.Node (Some s, _) -> s
313                 | DiscriminationTree.Node (None, _) ->
314                     retrieve n term (next_t pos term)
315               with Not_found ->
316                 PosEqSet.empty
317             in
318             try
319               let n = PSMap.find (Cic.Implicit None) map in
320               let newpos = try after_t pos term with _ -> [-1] in
321               if newpos = [-1] then
322                 match n with
323                 | DiscriminationTree.Node (Some s, _) -> PosEqSet.union s res
324                 | _ -> res
325               else
326                 PosEqSet.union res (retrieve n term newpos)
327             with Not_found ->
328               res
329   in
330   retrieve tree term []
331 ;;