From: Alberto Griggio Date: Mon, 20 Jun 2005 18:01:42 +0000 (+0000) Subject: discrimination trees X-Git-Tag: INDEXING_NO_PROOFS~111 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=101ecc0bc98f6f979d08200ae562ce89bffc0670;p=helm.git discrimination trees --- diff --git a/helm/ocaml/paramodulation/discrimination_tree.ml b/helm/ocaml/paramodulation/discrimination_tree.ml new file mode 100644 index 000000000..8753782d4 --- /dev/null +++ b/helm/ocaml/paramodulation/discrimination_tree.ml @@ -0,0 +1,238 @@ +type path_string_elem = Cic.term;; +type path_string = path_string_elem list;; + + +(* needed by the retrieve_* functions, to know the arities of the "functions" *) +let arities = Hashtbl.create 11;; + + +let rec path_string_of_term = function + | Cic.Meta _ -> [Cic.Implicit None] + | Cic.Appl ((hd::tl) as l) -> + if not (Hashtbl.mem arities hd) then + Hashtbl.add arities hd (List.length tl); + List.concat (List.map path_string_of_term l) + | term -> [term] +;; + + +module OrderedPathStringElement = struct + type t = path_string_elem + + let compare = Pervasives.compare +end + +module PSMap = Map.Make(OrderedPathStringElement);; + + +module DiscriminationTree = struct + type key = path_string + type t = Node of (Utils.pos * Inference.equality) option * (t PSMap.t) + + let empty = Node (None, PSMap.empty) + + let rec find l t = + match (l, t) with + | [], Node (None, _) -> raise Not_found + | [], Node (Some v, _) -> v + | x::r, Node (_, m) -> find r (PSMap.find x m) + + let rec mem l t = + match (l, t) with + | [], Node (None, _) -> false + | [], Node (Some _, _) -> true + | x::r, Node (_, m) -> try mem r (PSMap.find x m) with Not_found -> false + + let add l v t = + let rec ins = function + | [], Node (_, m) -> Node (Some v, m) + | x::r, Node (v, m) -> + let t' = try PSMap.find x m with Not_found -> empty in + let t'' = ins (r, t') in + Node (v, PSMap.add x t'' m) + in + ins (l, t) + + let rec remove l t = + match (l, t) with + | [], Node (_, m) -> Node (None, m) + | x::r, Node (v, m) -> + try + let t' = remove r (PSMap.find x m) in + Node (v, if t' = empty then PSMap.remove x m else PSMap.add x t' m) + with Not_found -> + t + + let rec fold f t acc = + let rec traverse revp t acc = match t with + | Node (None, m) -> + PSMap.fold (fun x -> traverse (x::revp)) m acc + | Node (Some v, m) -> + f (List.rev revp) v (PSMap.fold (fun x -> traverse (x::revp)) m acc) + in + traverse [] t acc + +end + + +let index tree equality = + let _, (_, l, r, ordering), _, _ = equality in + let psl = path_string_of_term l + and psr = path_string_of_term r in + match ordering with + | Utils.Gt -> DiscriminationTree.add psl (Utils.Left, equality) tree + | Utils.Lt -> DiscriminationTree.add psr (Utils.Right, equality) tree + | _ -> + let tree = DiscriminationTree.add psl (Utils.Left, equality) tree in + DiscriminationTree.add psr (Utils.Right, equality) tree +;; + + +let remove_index tree equality = + let _, (_, l, r, ordering), _, _ = equality in + let psl = path_string_of_term l + and psr = path_string_of_term r in + match ordering with + | Utils.Gt -> DiscriminationTree.remove psl tree + | Utils.Lt -> DiscriminationTree.remove psr tree + | _ -> + let tree = DiscriminationTree.remove psl tree in + DiscriminationTree.remove psr tree +;; + + +let in_index tree equality = + let _, (_, l, r, ordering), _, _ = equality in + let psl = path_string_of_term l + and psr = path_string_of_term r in + let meta_convertibility = Inference.meta_convertibility_eq equality in + let ok ps = + try let _, eq = DiscriminationTree.find ps tree in meta_convertibility eq + with Not_found -> false + in + (ok psl) || (ok psr) +;; + + +let head_of_term = function + | Cic.Appl (hd::tl) -> hd + | term -> term +;; + + +let rec subterm_at_pos pos term = + match pos with + | [] -> term + | index::pos -> + match term with + | Cic.Appl l -> + (try subterm_at_pos pos (List.nth l index) with _ -> raise Not_found) + | _ -> raise Not_found +;; + + +let next_t pos term = + let t = subterm_at_pos pos term in + try + let t2 = subterm_at_pos [1] t in + pos @ [1] + with Not_found -> + match pos with + | [] -> [1] + | pos -> List.fold_right (fun i r -> if r = [] then [i+1] else i::r) pos [] +;; + + +let rec after_t pos term = + let pos' = + match pos with + | [] -> raise Not_found + | pos -> List.fold_right (fun i r -> if r = [] then [i+1] else i::r) pos [] + in + try + let t = subterm_at_pos pos' term in pos' + with Not_found -> + let pos, _ = + List.fold_right + (fun i (r, b) -> if b then (i::r, true) else (r, true)) pos ([], false) + in + after_t pos term +;; + + +let retrieve_generalizations tree term = + let rec retrieve tree term pos = + match tree with + | DiscriminationTree.Node (value, map) -> + let res = + try + let hd_term = head_of_term (subterm_at_pos pos term) in + let n = PSMap.find hd_term map in + match n with + | DiscriminationTree.Node (Some s, _) -> [s] + | DiscriminationTree.Node (None, _) -> + retrieve n term (next_t pos term) + with Not_found -> + [] + in + try + let n = PSMap.find (Cic.Implicit None) map in + res @ (retrieve n term (after_t pos term)) + with Not_found -> + res + in + retrieve tree term [] +;; + + +let jump_list = function + | DiscriminationTree.Node (value, map) -> + let rec get n tree = + match tree with + | DiscriminationTree.Node (v, m) -> + if n = 0 then + [tree] + else + PSMap.fold + (fun k v res -> + let a = try Hashtbl.find arities k with Not_found -> 0 in + (get (n-1 + a) v) @ res) m [] + in + PSMap.fold + (fun k v res -> + let arity = try Hashtbl.find arities k with Not_found -> 0 in + (get arity v) @ res) + map [] +;; + + +let retrieve_unifiables tree term = + let rec retrieve tree term pos = + match tree with + | DiscriminationTree.Node (value, map) -> + let res = + try + match subterm_at_pos pos term with + | Cic.Meta _ -> + List.concat + (List.map + (fun t -> retrieve t term (next_t pos term)) + (jump_list tree)) + | subterm -> + let hd_term = head_of_term subterm in + let n = PSMap.find hd_term map in + match n with + | DiscriminationTree.Node (Some s, _) -> [s] + | DiscriminationTree.Node (None, _) -> + retrieve n term (next_t pos term) + with Not_found -> + [] + in + try + let n = PSMap.find (Cic.Implicit None) map in + res @ (retrieve n term (after_t pos term)) + with Not_found -> + res + in + retrieve tree term [] +;;