X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic%2Fdiscrimination_tree.ml;h=546f4a34fce9f01b2fcca86ff0148af5ee6ee045;hb=04f22df647f35080b499b720bca7bc0eb1794c64;hp=33ecea7cecabc2c6bbf93bb0732bd93f8cf91c79;hpb=beb4e1e9549d5b43e24907dc86c7ef899e487a3c;p=helm.git diff --git a/helm/software/components/cic/discrimination_tree.ml b/helm/software/components/cic/discrimination_tree.ml index 33ecea7ce..546f4a34f 100644 --- a/helm/software/components/cic/discrimination_tree.ml +++ b/helm/software/components/cic/discrimination_tree.ml @@ -30,8 +30,8 @@ module DiscriminationTreeIndexing = struct type path_string_elem = - | Function | Constant of UriManager.uri - | Bound of int | Variable | Proposition | Datatype ;; + | Constant of UriManager.uri + | Bound of int | Variable | Proposition | Datatype | Dead;; type path_string = path_string_elem list;; @@ -39,50 +39,47 @@ module DiscriminationTreeIndexing = * "functions" *) let ppelem = function - | Function -> "Fun" | Constant uri -> UriManager.name_of_uri uri | Bound i -> string_of_int i | Variable -> "?" | Proposition -> "Prop" | Datatype -> "Type" + | Dead -> "DEAD" ;; let pppath l = String.concat "::" (List.map ppelem l) ;; let elem_of_cic = function - | Cic.Meta _ -> Variable - | Cic.Lambda _ -> Function + | Cic.Meta _ | Cic.Implicit _ -> Variable | Cic.Rel i -> Bound i | Cic.Sort (Cic.Prop) -> Proposition | Cic.Sort _ -> Datatype - | term -> - try Constant (CicUtil.uri_of_term term) - with Invalid_argument _ -> Variable (* HACK! *) + | Cic.Const _ | Cic.Var _ | Cic.MutInd _ | Cic.MutConstruct _ as t -> + (try Constant (CicUtil.uri_of_term t) + with Invalid_argument _ -> assert false) + | Cic.Appl _ -> + assert false (* should not happen *) + | Cic.LetIn _ | Cic.Lambda _ | Cic.Prod _ | Cic.Cast _ + | Cic.MutCase _ | Cic.Fix _ | Cic.CoFix _ -> + HLog.debug "FIXME: the trie receives an invalid term"; + Dead + (* assert false universe.ml removes these *) ;; - 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); + if k = Dead then arities else (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 +98,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 +110,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 +122,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,29 +131,15 @@ 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 ;; + let rec skip_prods = function + | Cic.Prod (_,_,t) -> skip_prods t + | term -> term + ;; let rec subterm_at_pos pos term = match pos with @@ -287,14 +185,18 @@ let remove_index tree equality = ;; let retrieve_generalizations (tree,arity) term = + let term = skip_prods term in let rec retrieve tree term pos = match tree with | DiscriminationTree.Node (Some s, _) when pos = [] -> s | DiscriminationTree.Node (_, map) -> let res = + let hd_term = + elem_of_cic (head_of_term (subterm_at_pos pos term)) + in + if hd_term = Variable then A.empty else try - let hd_term = head_of_term (subterm_at_pos pos term) in - let n = PSMap.find (elem_of_cic hd_term) map in + let n = PSMap.find hd_term map in match n with | DiscriminationTree.Node (Some s, _) -> s | DiscriminationTree.Node (None, _) -> @@ -332,21 +234,25 @@ 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 [] ;; let retrieve_unifiables (tree,arities) term = + let term = skip_prods term in let rec retrieve tree term pos = match tree with | DiscriminationTree.Node (Some s, _) when pos = [] -> s @@ -365,9 +271,11 @@ let remove_index tree equality = (List.map (fun t -> retrieve t term newpos) jl) | Some subterm -> let res = + let hd_term = elem_of_cic (head_of_term subterm) in + if hd_term = Variable then + A.empty else try - let hd_term = head_of_term subterm in - let n = PSMap.find (elem_of_cic hd_term) map in + let n = PSMap.find hd_term map in match n with | DiscriminationTree.Node (Some s, _) -> s | DiscriminationTree.Node (None, _) ->