From: Andrea Asperti Date: Tue, 28 Nov 2006 17:47:31 +0000 (+0000) Subject: Changed an ahstable into an association list. X-Git-Tag: 0.4.95@7852~768 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=218a5af368cb7ea58c59cad2e7c8ef1f733792c2;p=helm.git Changed an ahstable into an association list. --- diff --git a/components/cic/discrimination_tree.ml b/components/cic/discrimination_tree.ml index 937188dca..b2906e1c9 100644 --- a/components/cic/discrimination_tree.ml +++ b/components/cic/discrimination_tree.ml @@ -57,32 +57,23 @@ module DiscriminationTreeIndexing = try Constant (CicUtil.uri_of_term term) with Invalid_argument _ -> Variable (* HACK! *) ;; - let path_string_of_term arities = - let set_arity n = function - | Variable -> Hashtbl.replace arities Variable 0 - | e -> Hashtbl.replace arities e n + let path_string_of_term arities = + let set_arity arities k n = + (assert (k<>Variable || n=0); + (k,n)::(List.remove_assoc k arities)) in - let rec aux = function + let rec aux arities = function | Cic.Appl ((hd::tl) as l) -> -(* - if Hashtbl.mem arities (elem_of_cic hd) then - begin - let n = Hashtbl.find arities (elem_of_cic hd) in - if n <> List.length tl then - begin - prerr_endline - (String.concat " " - (List.map (fun x -> ppelem (elem_of_cic x)) l)) - end; - assert(n = List.length tl) - end; -*) - set_arity (List.length tl) (elem_of_cic hd); -(* Hashtbl.replace arities (elem_of_cic hd) (List.length tl); *) - List.concat (List.map aux l) - | t -> [elem_of_cic t] + let arities = + set_arity arities (elem_of_cic hd) (List.length tl) in + List.fold_left + (fun (arities,path) t -> + let arities,tpath = aux arities t in + arities,path@tpath) + (arities,[]) l + | t -> arities, [elem_of_cic t] in - aux + aux arities ;; let compare_elem e1 e2 = match e1,e2 with @@ -101,49 +92,11 @@ module DiscriminationTreeIndexing = module DiscriminationTree = Trie.Make(PSMap);; - type t = A.t DiscriminationTree.t * (path_string_elem, int) Hashtbl.t - let empty = DiscriminationTree.empty, Hashtbl.create 11;; - -(* - 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 - ;; -*) + type t = A.t DiscriminationTree.t * (path_string_elem*int) list + let empty = DiscriminationTree.empty, [] ;; let index (tree,arity) term info = - let ps = path_string_of_term arity term in + let arity,ps = path_string_of_term arity term in let ps_set = try DiscriminationTree.find ps tree with Not_found -> A.empty in @@ -151,29 +104,8 @@ module DiscriminationTreeIndexing = tree,arity ;; -(* - 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,arity) term info = - let ps = path_string_of_term arity term in + let arity,ps = path_string_of_term arity term in try let ps_set = A.remove info (DiscriminationTree.find ps tree) in if A.is_empty ps_set then @@ -184,34 +116,8 @@ module DiscriminationTreeIndexing = tree,arity ;; -(* -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,arity) term test = - let ps = path_string_of_term arity term in + let arity,ps = path_string_of_term arity term in try let ps_set = DiscriminationTree.find ps tree in A.exists test ps_set @@ -219,24 +125,6 @@ let remove_index tree equality = 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 @@ -300,7 +188,7 @@ let remove_index tree equality = let hd_term = elem_of_cic (head_of_term (subterm_at_pos pos term)) in - if hd_term = Variable then A.empty else + if hd_term = Variable then A.empty else try let n = PSMap.find hd_term map in match n with @@ -340,15 +228,18 @@ let remove_index tree equality = else PSMap.fold (fun k v res -> - let a = - try Hashtbl.find arities k + let a = + try List.assoc k arities 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 + let arity = + try + List.assoc k arities + with Not_found -> 0 in (get arity v) @ res) map [] ;; @@ -375,7 +266,8 @@ let remove_index tree equality = | Some subterm -> let res = let hd_term = elem_of_cic (head_of_term subterm) in - if hd_term = Variable then A.empty else + if hd_term = Variable then + A.empty else try let n = PSMap.find hd_term map in match n with