1 (* path indexing implementation *)
3 (* position of the subterm, subterm (Appl are not stored...) *)
4 type path_string_elem = Index of int | Term of Cic.term;;
5 type path_string = path_string_elem list;;
8 let rec path_strings_of_term index =
9 let module C = Cic in function
10 | C.Meta _ -> [ [Index index; Term (C.Implicit None)] ]
12 let p = if index > 0 then [Index index; Term hd] else [Term hd] in
16 let rr = path_strings_of_term i t in
17 (i+1, r @ (List.map (fun ps -> p @ ps) rr)))
21 | term -> [ [Index index; Term term] ]
25 let string_of_path_string ps =
31 | Index i -> "Index " ^ (string_of_int i)
32 | Term t -> "Term " ^ (CicPp.ppterm t)
39 module OrderedPathStringElement = struct
40 type t = path_string_elem
44 | Index i, Index j -> Pervasives.compare i j
45 | Term t1, Term t2 -> if t1 = t2 then 0 else Pervasives.compare t1 t2
46 | Index _, Term _ -> -1
47 | Term _, Index _ -> 1
50 module PSMap = Map.Make(OrderedPathStringElement);;
52 module OrderedPosEquality = struct
53 type t = Utils.pos * Inference.equality
55 let compare = Pervasives.compare
58 module PosEqSet = Set.Make(OrderedPosEquality);;
61 module PSTrie = Trie.Make(PSMap);;
65 * Trie: maps over lists.
66 * Copyright (C) 2000 Jean-Christophe FILLIATRE
68 module PSTrie = struct
69 type key = path_string
70 type t = Node of PosEqSet.t option * (t PSMap.t)
72 let empty = Node (None, PSMap.empty)
76 | [], Node (None, _) -> raise Not_found
77 | [], Node (Some v, _) -> v
78 | x::r, Node (_, m) -> find r (PSMap.find x m)
82 | [], Node (None, _) -> false
83 | [], Node (Some _, _) -> true
84 | x::r, Node (_, m) -> try mem r (PSMap.find x m) with Not_found -> false
87 let rec ins = function
88 | [], Node (_, m) -> Node (Some v, m)
89 | x::r, Node (v, m) ->
90 let t' = try PSMap.find x m with Not_found -> empty in
91 let t'' = ins (r, t') in
92 Node (v, PSMap.add x t'' m)
98 | [], Node (_, m) -> Node (None, m)
99 | x::r, Node (v, m) ->
101 let t' = remove r (PSMap.find x m) in
102 Node (v, if t' = empty then PSMap.remove x m else PSMap.add x t' m)
106 let rec fold f t acc =
107 let rec traverse revp t acc = match t with
109 PSMap.fold (fun x -> traverse (x::revp)) m acc
110 | Node (Some v, m) ->
111 f (List.rev revp) v (PSMap.fold (fun x -> traverse (x::revp)) m acc)
119 let index trie equality =
120 let _, _, (_, l, r, ordering), _, _ = equality in
121 let psl = path_strings_of_term 0 l
122 and psr = path_strings_of_term 0 r in
123 let index pos trie ps =
124 let ps_set = try PSTrie.find ps trie with Not_found -> PosEqSet.empty in
125 let trie = PSTrie.add ps (PosEqSet.add (pos, equality) ps_set) trie in
126 (* if PosEqSet.mem (pos, equality) (PSTrie.find ps trie) then *)
127 (* Printf.printf "OK: %s, %s indexed\n" (Utils.string_of_pos pos) *)
128 (* (Inference.string_of_equality equality); *)
132 | Utils.Gt -> List.fold_left (index Utils.Left) trie psl
133 | Utils.Lt -> List.fold_left (index Utils.Right) trie psr
135 let trie = List.fold_left (index Utils.Left) trie psl in
136 List.fold_left (index Utils.Right) trie psr
140 let remove_index trie equality =
141 let _, _, (_, l, r, ordering), _, _ = equality in
142 let psl = path_strings_of_term 0 l
143 and psr = path_strings_of_term 0 r in
144 let remove_index pos trie ps =
146 let ps_set = PosEqSet.remove (pos, equality) (PSTrie.find ps trie) in
147 if PosEqSet.is_empty ps_set then
148 PSTrie.remove ps trie
150 PSTrie.add ps ps_set trie
152 (* Printf.printf "NOT_FOUND: %s, %s\n" (Utils.string_of_pos pos) *)
153 (* (Inference.string_of_equality equality); *)
155 (* raise Not_found *)
158 | Utils.Gt -> List.fold_left (remove_index Utils.Left) trie psl
159 | Utils.Lt -> List.fold_left (remove_index Utils.Right) trie psr
161 let trie = List.fold_left (remove_index Utils.Left) trie psl in
162 List.fold_left (remove_index Utils.Right) trie psr
166 let in_index trie equality =
167 let _, _, (_, l, r, ordering), _, _ = equality in
168 let psl = path_strings_of_term 0 l
169 and psr = path_strings_of_term 0 r in
170 let meta_convertibility = Inference.meta_convertibility_eq equality in
173 let set = PSTrie.find ps trie in
174 PosEqSet.exists (fun (p, e) -> meta_convertibility e) set
178 (List.exists ok psl) || (List.exists ok psr)
182 let head_of_term = function
183 | Cic.Appl (hd::tl) -> hd
188 let subterm_at_pos index term =
194 (try List.nth l index with Failure _ -> raise Not_found)
195 | _ -> raise Not_found
199 let rec retrieve_generalizations trie term =
201 | PSTrie.Node (value, map) ->
204 | Cic.Meta _ -> PosEqSet.empty
206 let hd_term = head_of_term term in
208 let n = PSMap.find (Term hd_term) map in
210 | PSTrie.Node (Some s, _) -> s
211 | PSTrie.Node (None, m) ->
217 let t = subterm_at_pos i term in
218 let s = retrieve_generalizations v t in
225 List.fold_left (fun r s -> PosEqSet.inter r s) hd tl
226 | _ -> PosEqSet.empty
231 let n = PSMap.find (Term (Cic.Implicit None)) map in
233 | PSTrie.Node (Some s, _) -> PosEqSet.union res s
240 let rec retrieve_unifiables trie term =
242 | PSTrie.Node (value, map) ->
247 (fun ps v res -> PosEqSet.union res v)
248 (PSTrie.Node (None, map))
251 let hd_term = head_of_term term in
253 let n = PSMap.find (Term hd_term) map in
255 | PSTrie.Node (Some v, _) -> v
256 | PSTrie.Node (None, m) ->
262 let t = subterm_at_pos i term in
263 let s = retrieve_unifiables v t in
270 List.fold_left (fun r s -> PosEqSet.inter r s) hd tl
271 | _ -> PosEqSet.empty
273 (* Printf.printf "Not_found: %s, term was: %s\n" *)
274 (* (CicPp.ppterm hd_term) (CicPp.ppterm term); *)
275 (* Printf.printf "map is:\n %s\n\n" *)
276 (* (String.concat "\n" *)
280 (* | Index i -> ("Index " ^ (string_of_int i))::l *)
281 (* | Term t -> ("Term " ^ (CicPp.ppterm t))::l) *)
286 let n = PSMap.find (Term (Cic.Implicit None)) map in
288 | PSTrie.Node (Some s, _) -> PosEqSet.union res s
295 let retrieve_all trie term =
297 (fun k v s -> PosEqSet.union v s) trie PosEqSet.empty
301 let string_of_pstrie trie =
302 let rec to_string level = function
303 | PSTrie.Node (v, map) ->
307 (String.make (2 * level) ' ') ^
308 "{" ^ (String.concat "; "
311 "(" ^ (Utils.string_of_pos p) ^ ", " ^
312 (Inference.string_of_equality e) ^ ")")
313 (PosEqSet.elements v))) ^ "}"
322 | Index i -> "Index " ^ (string_of_int i)
323 | Term t -> "Term " ^ (CicPp.ppterm t)
325 let rs = to_string (level+1) v in
326 ((String.make (2 * level) ' ') ^ ks ^ "\n" ^ rs)::s)