diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-10-21 12:07:04 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-10-21 12:07:04 +0000 |
commit | a26b6952a1a61c00f8ecafce7ad6bd6576352814 (patch) | |
tree | f69c406ae9a34c8ab967e06d3e5e9630ab8c2ec2 /library/nametab.ml | |
parent | 1451dd046e318b0a53218b44a691854381eac6f5 (diff) |
Nouvelle fonction cherchant tous les noms d'un suffixe donne
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4687 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library/nametab.ml')
-rwxr-xr-x | library/nametab.ml | 29 |
1 files changed, 27 insertions, 2 deletions
diff --git a/library/nametab.ml b/library/nametab.ml index c6ab79557..08b09a4a0 100755 --- a/library/nametab.ml +++ b/library/nametab.ml @@ -71,6 +71,7 @@ module type NAMETREE = sig val exists : user_name -> 'a t -> bool val user_name : qualid -> 'a t -> user_name val shortest_qualid : Idset.t -> user_name -> 'a t -> qualid + val find_prefixes : qualid -> 'a t -> 'a list end module Make(U:UserName) : NAMETREE with type user_name = U.t @@ -212,7 +213,7 @@ let shortest_qualid ctx uname tab = let hidden = Idset.mem id ctx in let rec find_uname pos dir (path,tab) = match path with | Absolute (u,_) | Relative (u,_) - when u=uname && not(pos=[] && hidden) -> List.rev pos + when u=uname && not(pos=[] && hidden) -> List.rev pos | _ -> match dir with [] -> raise Not_found @@ -221,7 +222,25 @@ let shortest_qualid ctx uname tab = let ptab = Idmap.find id tab in let found_dir = find_uname [] dir ptab in make_qualid (make_dirpath found_dir) id - + +let push_node node l = + match node with + | Absolute (_,o) | Relative (_,o) when not (List.mem o l) -> o::l + | _ -> l + +let rec flatten_idmap tab l = + ModIdmap.fold (fun _ (current,idtab) l -> + flatten_idmap idtab (push_node current l)) tab l + +let rec search_prefixes (current,modidtab) = function + | modid :: path -> search_prefixes (ModIdmap.find modid modidtab) path + | [] -> List.rev (flatten_idmap modidtab (push_node current [])) + +let find_prefixes qid tab = + try + let (dir,id) = repr_qualid qid in + search_prefixes (Idmap.find id tab) (repr_dirpath dir) + with Not_found -> [] end @@ -373,6 +392,12 @@ let locate_section qid = | DirClosedSection dir -> dir | _ -> raise Not_found +let locate_all qid = + List.fold_right (fun a l -> match a with TrueGlobal a -> a::l | _ -> l) + (SpTab.find_prefixes qid !the_ccitab) [] + +let extended_locate_all qid = SpTab.find_prefixes qid !the_ccitab + (* Derived functions *) let locate_constant qid = |