X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=helm%2Focaml%2Fcic%2Fdiscrimination_tree.ml;fp=helm%2Focaml%2Fcic%2Fdiscrimination_tree.ml;h=0bef85a8cc4e7ea1d89c3f708c025c0c998cb545;hb=792b5d29ebae8f917043d9dd226692919b5d6ca1;hp=0000000000000000000000000000000000000000;hpb=a14a8c7637fd0b95e9d4deccb20c6abc98e8f953;p=helm.git diff --git a/helm/ocaml/cic/discrimination_tree.ml b/helm/ocaml/cic/discrimination_tree.ml new file mode 100644 index 000000000..0bef85a8c --- /dev/null +++ b/helm/ocaml/cic/discrimination_tree.ml @@ -0,0 +1,343 @@ +(* Copyright (C) 2005, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +(* $Id$ *) + +module DiscriminationTreeIndexing = + functor (A:Set.S) -> + struct + + 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);; + + type key = PSMap.key + + module DiscriminationTree = Trie.Make(PSMap);; + + type t = A.t DiscriminationTree.t + let empty = DiscriminationTree.empty + +(* + module OrderedPosEquality = struct + type t = Utils.pos * Inference.equality + let compare = Pervasives.compare + end + + module PosEqSet = Set.Make(OrderedPosEquality);; + + let string_of_discrimination_tree tree = + let rec to_string level = function + | DiscriminationTree.Node (value, map) -> + let s = + match value with + | Some v -> + (String.make (2 * level) ' ') ^ + "{" ^ (String.concat "; " + (List.map + (fun (p, e) -> + "(" ^ (Utils.string_of_pos p) ^ ", " ^ + (Inference.string_of_equality e) ^ ")") + (PosEqSet.elements v))) ^ "}" + | None -> "" + in + let rest = + String.concat "\n" + (PSMap.fold + (fun k v s -> + let ks = CicPp.ppterm k in + let rs = to_string (level+1) v in + ((String.make (2 * level) ' ') ^ ks ^ "\n" ^ rs)::s) + map []) + in + s ^ rest + in + to_string 0 tree + ;; +*) + + let index tree term info = + let ps = path_string_of_term term in + let ps_set = + try DiscriminationTree.find ps tree + with Not_found -> A.empty in + let tree = + DiscriminationTree.add ps (A.add info ps_set) tree in + tree + +(* + 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 + let index pos tree ps = + let ps_set = + try DiscriminationTree.find ps tree with Not_found -> PosEqSet.empty in + let tree = + DiscriminationTree.add ps (PosEqSet.add (pos, equality) ps_set) tree in + tree + in + match ordering with + | Utils.Gt -> index Utils.Left tree psl + | Utils.Lt -> index Utils.Right tree psr + | _ -> + let tree = index Utils.Left tree psl in + index Utils.Right tree psr + ;; +*) + + let remove_index tree term info = + let ps = path_string_of_term term in + try + let ps_set = + A.remove info (DiscriminationTree.find ps tree) in + if A.is_empty ps_set then + DiscriminationTree.remove ps tree + else + DiscriminationTree.add ps ps_set tree + with Not_found -> + 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 + let remove_index pos tree ps = + try + let ps_set = + PosEqSet.remove (pos, equality) (DiscriminationTree.find ps tree) in + if PosEqSet.is_empty ps_set then + DiscriminationTree.remove ps tree + else + DiscriminationTree.add ps ps_set tree + with Not_found -> + tree + in + match ordering with + | Utils.Gt -> remove_index Utils.Left tree psl + | Utils.Lt -> remove_index Utils.Right tree psr + | _ -> + let tree = remove_index Utils.Left tree psl in + remove_index Utils.Right tree psr +;; +*) + + + let in_index tree term test = + let ps = path_string_of_term term in + try + let ps_set = DiscriminationTree.find ps tree in + A.exists test ps_set + with Not_found -> + false + +(* + 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 set = DiscriminationTree.find ps tree in + PosEqSet.exists (fun (p, e) -> meta_convertibility e) set + 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 Failure _ -> raise Not_found) + | _ -> raise Not_found + ;; + + + 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 next_t pos term = + let t = subterm_at_pos pos term in + try + let _ = subterm_at_pos [1] t in + pos @ [1] + with Not_found -> + match pos with + | [] -> [1] + | pos -> after_t pos term + ;; + + + let retrieve_generalizations tree term = + let rec retrieve tree term pos = + match tree with + | DiscriminationTree.Node (Some s, _) when pos = [] -> s + | DiscriminationTree.Node (_, 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, _) -> + let newpos = try next_t pos term with Not_found -> [] in + retrieve n term newpos + with Not_found -> + A.empty + in + try + let n = PSMap.find (Cic.Implicit None) map in + let newpos = try after_t pos term with Not_found -> [-1] in + if newpos = [-1] then + match n with + | DiscriminationTree.Node (Some s, _) -> A.union s res + | _ -> res + else + A.union res (retrieve n term newpos) + 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 (Some s, _) when pos = [] -> s + | DiscriminationTree.Node (_, map) -> + let subterm = + try Some (subterm_at_pos pos term) with Not_found -> None + in + match subterm with + | None -> A.empty + | Some (Cic.Meta _) -> + let newpos = try next_t pos term with Not_found -> [] in + let jl = jump_list tree in + List.fold_left + (fun r s -> A.union r s) + A.empty + (List.map (fun t -> retrieve t term newpos) jl) + | Some subterm -> + let res = + try + 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 -> + A.empty + in + try + let n = PSMap.find (Cic.Implicit None) map in + let newpos = try after_t pos term with Not_found -> [-1] in + if newpos = [-1] then + match n with + | DiscriminationTree.Node (Some s, _) -> A.union s res + | _ -> res + else + A.union res (retrieve n term newpos) + with Not_found -> + res + in + retrieve tree term [] + end +;; +