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 PSTrie = Trie.Make(PathStringElementMap);; *)
54 module OrderedPosEquality = struct
55 type t = Utils.pos * Inference.equality
57 let compare = Pervasives.compare
60 module PosEqSet = Set.Make(OrderedPosEquality);;
63 * Trie: maps over lists.
64 * Copyright (C) 2000 Jean-Christophe FILLIATRE
66 module PSTrie = struct
67 type key = path_string
68 type t = Node of PosEqSet.t option * (t PSMap.t)
70 let empty = Node (None, PSMap.empty)
74 | [], Node (None, _) -> raise Not_found
75 | [], Node (Some v, _) -> v
76 | x::r, Node (_, m) -> find r (PSMap.find x m)
80 | [], Node (None, _) -> false
81 | [], Node (Some _, _) -> true
82 | x::r, Node (_, m) -> try mem r (PSMap.find x m) with Not_found -> false
85 let rec ins = function
86 | [], Node (_, m) -> Node (Some v, m)
87 | x::r, Node (v, m) ->
88 let t' = try PSMap.find x m with Not_found -> empty in
89 let t'' = ins (r, t') in
90 Node (v, PSMap.add x t'' m)
96 | [], Node (_, m) -> Node (None, m)
97 | x::r, Node (v, m) ->
99 let t' = remove r (PSMap.find x m) in
100 Node (v, if t' = empty then PSMap.remove x m else PSMap.add x t' m)
104 let rec fold f t acc =
105 let rec traverse revp t acc = match t with
107 PSMap.fold (fun x -> traverse (x::revp)) m acc
108 | Node (Some v, m) ->
109 f (List.rev revp) v (PSMap.fold (fun x -> traverse (x::revp)) m acc)
116 let index trie equality =
117 let _, (_, l, r, ordering), _, _ = equality in
118 let psl = path_strings_of_term 0 l
119 and psr = path_strings_of_term 0 r in
120 let index pos trie ps =
121 let ps_set = try PSTrie.find ps trie with Not_found -> PosEqSet.empty in
122 let trie = PSTrie.add ps (PosEqSet.add (pos, equality) ps_set) trie in
123 (* if PosEqSet.mem (pos, equality) (PSTrie.find ps trie) then *)
124 (* Printf.printf "OK: %s, %s indexed\n" (Utils.string_of_pos pos) *)
125 (* (Inference.string_of_equality equality); *)
129 | Utils.Gt -> List.fold_left (index Utils.Left) trie psl
130 | Utils.Lt -> List.fold_left (index Utils.Right) trie psr
132 let trie = List.fold_left (index Utils.Left) trie psl in
133 List.fold_left (index Utils.Right) trie psr
137 let remove_index trie equality =
138 let _, (_, l, r, ordering), _, _ = equality in
139 let psl = path_strings_of_term 0 l
140 and psr = path_strings_of_term 0 r in
141 let remove_index pos trie ps =
143 let ps_set = PosEqSet.remove (pos, equality) (PSTrie.find ps trie) in
144 if PosEqSet.is_empty ps_set then
145 PSTrie.remove ps trie
147 PSTrie.add ps ps_set trie
149 (* Printf.printf "NOT_FOUND: %s, %s\n" (Utils.string_of_pos pos) *)
150 (* (Inference.string_of_equality equality); *)
152 (* raise Not_found *)
155 | Utils.Gt -> List.fold_left (remove_index Utils.Left) trie psl
156 | Utils.Lt -> List.fold_left (remove_index Utils.Right) trie psr
158 let trie = List.fold_left (remove_index Utils.Left) trie psl in
159 List.fold_left (remove_index Utils.Right) trie psr
163 let in_index trie equality =
164 let _, (_, l, r, ordering), _, _ = equality in
165 let psl = path_strings_of_term 0 l
166 and psr = path_strings_of_term 0 r in
167 let meta_convertibility = Inference.meta_convertibility_eq equality in
170 let set = PSTrie.find ps trie in
171 PosEqSet.exists (fun (p, e) -> meta_convertibility e) set
175 (List.exists ok psl) || (List.exists ok psr)
179 let head_of_term = function
180 | Cic.Appl (hd::tl) -> hd
185 let subterm_at_pos index term =
191 (try List.nth l index with Failure _ -> raise Not_found)
192 | _ -> raise Not_found
196 let rec retrieve_generalizations trie term =
198 | PSTrie.Node (value, map) ->
201 | Cic.Meta _ -> PosEqSet.empty
203 let hd_term = head_of_term term in
205 let n = PSMap.find (Term hd_term) map in
207 | PSTrie.Node (Some s, _) -> s
208 | PSTrie.Node (None, m) ->
214 let t = subterm_at_pos i term in
215 let s = retrieve_generalizations v t in
222 List.fold_left (fun r s -> PosEqSet.inter r s) hd tl
223 | _ -> PosEqSet.empty
228 let n = PSMap.find (Term (Cic.Implicit None)) map in
230 | PSTrie.Node (Some s, _) -> PosEqSet.union res s
237 let rec retrieve_unifiables trie term =
239 | PSTrie.Node (value, map) ->
244 (fun ps v res -> PosEqSet.union res v)
245 (PSTrie.Node (None, map))
248 let hd_term = head_of_term term in
250 let n = PSMap.find (Term hd_term) map in
252 | PSTrie.Node (Some v, _) -> v
253 | PSTrie.Node (None, m) ->
259 let t = subterm_at_pos i term in
260 let s = retrieve_unifiables v t in
267 List.fold_left (fun r s -> PosEqSet.inter r s) hd tl
268 | _ -> PosEqSet.empty
270 (* Printf.printf "Not_found: %s, term was: %s\n" *)
271 (* (CicPp.ppterm hd_term) (CicPp.ppterm term); *)
272 (* Printf.printf "map is:\n %s\n\n" *)
273 (* (String.concat "\n" *)
277 (* | Index i -> ("Index " ^ (string_of_int i))::l *)
278 (* | Term t -> ("Term " ^ (CicPp.ppterm t))::l) *)
283 let n = PSMap.find (Term (Cic.Implicit None)) map in
285 | PSTrie.Node (Some s, _) -> PosEqSet.union res s
292 let string_of_pstrie trie =
293 let rec to_string level = function
294 | PSTrie.Node (v, map) ->
298 (String.make (2 * level) ' ') ^
299 "{" ^ (String.concat "; "
302 "(" ^ (Utils.string_of_pos p) ^ ", " ^
303 (Inference.string_of_equality e) ^ ")")
304 (PosEqSet.elements v))) ^ "}"
313 | Index i -> "Index " ^ (string_of_int i)
314 | Term t -> "Term " ^ (CicPp.ppterm t)
316 let rs = to_string (level+1) v in
317 ((String.make (2 * level) ' ') ^ ks ^ "\n" ^ rs)::s)