From 61ccbc81a2f3b4662ed4a2bad9d07d2003dda3a2 Mon Sep 17 00:00:00 2001 From: glondu Date: Thu, 17 Sep 2009 15:58:14 +0000 Subject: Delete trailing whitespaces in all *.{v,ml*} files git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7 --- library/nametab.ml | 132 ++++++++++++++++++++++++++--------------------------- 1 file changed, 66 insertions(+), 66 deletions(-) (limited to 'library/nametab.ml') diff --git a/library/nametab.ml b/library/nametab.ml index 074386417..31915c95a 100644 --- a/library/nametab.ml +++ b/library/nametab.ml @@ -31,12 +31,12 @@ let error_global_not_found q = raise (GlobalizationError q) type ltac_constant = kernel_name -(* The visibility can be registered either +(* The visibility can be registered either - for all suffixes not shorter then a given int - when the object is loaded inside a module or - for a precise suffix, when the module containing (the module - containing ...) the object is open (imported) + containing ...) the object is open (imported) *) type visibility = Until of int | Exactly of int @@ -46,7 +46,7 @@ type visibility = Until of int | Exactly of int (* This module type will be instantiated by [full_path] of [dir_path] *) (* The [repr] function is assumed to return the reversed list of idents. *) -module type UserName = sig +module type UserName = sig type t val to_string : t -> string val repr : t -> identifier * module_ident list @@ -57,15 +57,15 @@ end partially qualified names of type [qualid]. The mapping of partially qualified names to ['a] is determined by the [visibility] parameter of [push]. - + The [shortest_qualid] function given a user_name Coq.A.B.x, tries to find the shortest among x, B.x, A.B.x and Coq.A.B.x that denotes - the same object. + the same object. *) module type NAMETREE = sig type 'a t type user_name - + val empty : 'a t val push : visibility -> user_name -> 'a -> 'a t -> 'a t val locate : qualid -> 'a t -> 'a @@ -76,15 +76,15 @@ module type NAMETREE = sig val find_prefixes : qualid -> 'a t -> 'a list end -module Make(U:UserName) : NAMETREE with type user_name = U.t - = +module Make(U:UserName) : NAMETREE with type user_name = U.t + = struct type user_name = U.t - type 'a path_status = - Nothing - | Relative of user_name * 'a + type 'a path_status = + Nothing + | Relative of user_name * 'a | Absolute of user_name * 'a (* Dictionaries of short names *) @@ -93,38 +93,38 @@ struct type 'a t = 'a nametree Idmap.t let empty = Idmap.empty - - (* [push_until] is used to register [Until vis] visibility and + + (* [push_until] is used to register [Until vis] visibility and [push_exactly] to [Exactly vis] and [push_tree] chooses the right one*) let rec push_until uname o level (current,dirmap) = function | modid :: path -> - let mc = + let mc = try ModIdmap.find modid dirmap with Not_found -> (Nothing, ModIdmap.empty) in let this = if level <= 0 then match current with - | Absolute (n,_) -> - (* This is an absolute name, we must keep it + | Absolute (n,_) -> + (* This is an absolute name, we must keep it otherwise it may become unaccessible forever *) Flags.if_verbose - warning ("Trying to mask the absolute name \"" - ^ U.to_string n ^ "\"!"); + warning ("Trying to mask the absolute name \"" + ^ U.to_string n ^ "\"!"); current | Nothing | Relative _ -> Relative (uname,o) - else current + else current in let ptab' = push_until uname o (level-1) mc path in (this, ModIdmap.add modid ptab' dirmap) - | [] -> + | [] -> match current with - | Absolute (uname',o') -> + | Absolute (uname',o') -> if o'=o then begin assert (uname=uname'); - current, dirmap + current, dirmap (* we are putting the same thing for the second time :) *) end else @@ -139,15 +139,15 @@ struct let rec push_exactly uname o level (current,dirmap) = function | modid :: path -> - let mc = + let mc = try ModIdmap.find modid dirmap with Not_found -> (Nothing, ModIdmap.empty) in if level = 0 then let this = match current with - | Absolute (n,_) -> - (* This is an absolute name, we must keep it + | Absolute (n,_) -> + (* This is an absolute name, we must keep it otherwise it may become unaccessible forever *) Flags.if_verbose warning ("Trying to mask the absolute name \"" @@ -160,7 +160,7 @@ let rec push_exactly uname o level (current,dirmap) = function else (* not right level *) let ptab' = push_exactly uname o (level-1) mc path in (current, ModIdmap.add modid ptab' dirmap) - | [] -> + | [] -> anomaly "Prefix longer than path! Impossible!" @@ -168,7 +168,7 @@ let push visibility uname o tab = let id,dir = U.repr uname in let ptab = try Idmap.find id tab - with Not_found -> (Nothing, ModIdmap.empty) + with Not_found -> (Nothing, ModIdmap.empty) in let ptab' = match visibility with | Until i -> push_until uname o (i-1) ptab dir @@ -180,46 +180,46 @@ let push visibility uname o tab = let rec search (current,modidtab) = function | modid :: path -> search (ModIdmap.find modid modidtab) path | [] -> current - + let find_node qid tab = let (dir,id) = repr_qualid qid in search (Idmap.find id tab) (repr_dirpath dir) -let locate qid tab = +let locate qid tab = let o = match find_node qid tab with | Absolute (uname,o) | Relative (uname,o) -> o - | Nothing -> raise Not_found + | Nothing -> raise Not_found in o let user_name qid tab = let uname = match find_node qid tab with | Absolute (uname,o) | Relative (uname,o) -> uname - | Nothing -> raise Not_found + | Nothing -> raise Not_found in uname - -let find uname tab = + +let find uname tab = let id,l = U.repr uname in match search (Idmap.find id tab) l with Absolute (_,o) -> o | _ -> raise Not_found let exists uname tab = - try + try let _ = find uname tab in true with Not_found -> false -let shortest_qualid ctx uname tab = +let shortest_qualid ctx uname tab = let id,dir = U.repr uname in 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 - | _ -> - match dir with + | _ -> + match dir with [] -> raise Not_found | id::dir -> find_uname (id::pos) dir (ModIdmap.find id tab) in @@ -239,7 +239,7 @@ let rec flatten_idmap 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 @@ -252,10 +252,10 @@ end (* Global name tables *************************************************) -module SpTab = Make (struct +module SpTab = Make (struct type t = full_path let to_string = string_of_path - let repr sp = + let repr sp = let dir,id = repr_path sp in id, (repr_dirpath dir) end) @@ -271,7 +271,7 @@ type mptab = module_path SpTab.t let the_modtypetab = ref (SpTab.empty : mptab) -module DirTab = Make(struct +module DirTab = Make(struct type t = dir_path let to_string = string_of_dirpath let repr dir = match repr_dirpath dir with @@ -288,9 +288,9 @@ let the_dirtab = ref (DirTab.empty : dirtab) (* Reversed name tables ***************************************************) (* This table translates extended_global_references back to section paths *) -module Globrevtab = Map.Make(struct - type t=extended_global_reference - let compare = compare +module Globrevtab = Map.Make(struct + type t=extended_global_reference + let compare = compare end) type globrevtab = full_path Globrevtab.t @@ -316,7 +316,7 @@ let the_tacticrevtab = ref (KNmap.empty : knrevtab) let push_xref visibility sp xref = the_ccitab := SpTab.push visibility sp xref !the_ccitab; match visibility with - | Until _ -> + | Until _ -> if Globrevtab.mem xref !the_globrevtab then () else @@ -332,19 +332,19 @@ let push_syndef visibility sp kn = let push = push_cci -let push_modtype vis sp kn = +let push_modtype vis sp kn = the_modtypetab := SpTab.push vis sp kn !the_modtypetab; the_modtyperevtab := MPmap.add kn sp !the_modtyperevtab (* This is for tactic definition names *) -let push_tactic vis sp kn = +let push_tactic vis sp kn = the_tactictab := SpTab.push vis sp kn !the_tactictab; the_tacticrevtab := KNmap.add kn sp !the_tacticrevtab (* This is to remember absolute Section/Module names and to avoid redundancy *) -let push_dir vis dir dir_ref = +let push_dir vis dir dir_ref = the_dirtab := DirTab.push vis dir dir_ref !the_dirtab; match dir_ref with DirModule (_,(mp,_)) -> the_modrevtab := MPmap.add mp dir !the_modrevtab @@ -375,23 +375,23 @@ let full_name_tactic qid = SpTab.user_name qid !the_tactictab let locate_dir qid = DirTab.locate qid !the_dirtab -let locate_module qid = +let locate_module qid = match locate_dir qid with | DirModule (_,(mp,_)) -> mp | _ -> raise Not_found -let full_name_module qid = +let full_name_module qid = match locate_dir qid with | DirModule (dir,_) -> dir | _ -> raise Not_found let locate_section qid = match locate_dir qid with - | DirOpenSection (dir, _) + | DirOpenSection (dir, _) | DirClosedSection dir -> dir | _ -> raise Not_found -let locate_all qid = +let locate_all qid = List.fold_right (fun a l -> match a with TrueGlobal a -> a::l | _ -> l) (SpTab.find_prefixes qid !the_ccitab) [] @@ -404,7 +404,7 @@ let locate_constant qid = | TrueGlobal (ConstRef kn) -> kn | _ -> raise Not_found -let locate_mind qid = +let locate_mind qid = match locate_extended qid with | TrueGlobal (IndRef (kn,0)) -> kn | _ -> raise Not_found @@ -423,7 +423,7 @@ let global r = let (loc,qid) = qualid_of_reference r in try match locate_extended qid with | TrueGlobal ref -> ref - | SynDef _ -> + | SynDef _ -> user_err_loc (loc,"global", str "Unexpected reference to a notation: " ++ pr_qualid qid) @@ -433,7 +433,7 @@ let global r = (* Exists functions ********************************************************) let exists_cci sp = SpTab.exists sp !the_ccitab - + let exists_dir dir = DirTab.exists dir !the_dirtab let exists_section = exists_dir @@ -446,18 +446,18 @@ let exists_tactic sp = SpTab.exists sp !the_tactictab (* Reverse locate functions ***********************************************) -let path_of_global ref = +let path_of_global ref = match ref with | VarRef id -> make_path empty_dirpath id | _ -> Globrevtab.find (TrueGlobal ref) !the_globrevtab -let dirpath_of_global ref = +let dirpath_of_global ref = fst (repr_path (path_of_global ref)) -let basename_of_global ref = +let basename_of_global ref = snd (repr_path (path_of_global ref)) -let path_of_syndef kn = +let path_of_syndef kn = Globrevtab.find (SynDef kn) !the_globrevtab let dirpath_of_module mp = @@ -466,18 +466,18 @@ let dirpath_of_module mp = (* Shortest qualid functions **********************************************) -let shortest_qualid_of_global ctx ref = +let shortest_qualid_of_global ctx ref = match ref with | VarRef id -> make_qualid empty_dirpath id | _ -> let sp = Globrevtab.find (TrueGlobal ref) !the_globrevtab in SpTab.shortest_qualid ctx sp !the_ccitab -let shortest_qualid_of_syndef ctx kn = +let shortest_qualid_of_syndef ctx kn = let sp = path_of_syndef kn in SpTab.shortest_qualid ctx sp !the_ccitab -let shortest_qualid_of_module mp = +let shortest_qualid_of_module mp = let dir = MPmap.find mp !the_modrevtab in DirTab.shortest_qualid Idset.empty dir !the_dirtab @@ -512,8 +512,8 @@ let global_inductive r = type frozen = ccitab * dirtab * kntab * kntab * globrevtab * mprevtab * knrevtab * knrevtab -let init () = - the_ccitab := SpTab.empty; +let init () = + the_ccitab := SpTab.empty; the_dirtab := DirTab.empty; the_modtypetab := SpTab.empty; the_tactictab := SpTab.empty; @@ -525,7 +525,7 @@ let init () = let freeze () = - !the_ccitab, + !the_ccitab, !the_dirtab, !the_modtypetab, !the_tactictab, @@ -544,7 +544,7 @@ let unfreeze (ccit,dirt,mtyt,tact,globr,modr,mtyr,tacr) = the_modtyperevtab := mtyr; the_tacticrevtab := tacr -let _ = +let _ = Summary.declare_summary "names" { Summary.freeze_function = freeze; Summary.unfreeze_function = unfreeze; -- cgit v1.2.3