1(* Title: Pure/General/path.ML 2 Author: Markus Wenzel, TU Muenchen 3 4Algebra of file-system paths: basic POSIX notation, extended by named 5roots (e.g. //foo) and variables (e.g. $BAR). 6*) 7 8signature PATH = 9sig 10 eqtype T 11 val is_current: T -> bool 12 val current: T 13 val root: T 14 val named_root: string -> T 15 val parent: T 16 val make: string list -> T 17 val basic: string -> T 18 val variable: string -> T 19 val has_parent: T -> bool 20 val is_absolute: T -> bool 21 val is_basic: T -> bool 22 val starts_basic: T -> bool 23 val append: T -> T -> T 24 val appends: T list -> T 25 val implode: T -> string 26 val explode: string -> T 27 val explode_pos: string * Position.T -> T * Position.T 28 val decode: T XML.Decode.T 29 val split: string -> T list 30 val pretty: T -> Pretty.T 31 val print: T -> string 32 val dir: T -> T 33 val base: T -> T 34 val ext: string -> T -> T 35 val split_ext: T -> T * string 36 val exe: T -> T 37 val expand: T -> T 38 val file_name: T -> string 39 val smart_implode: T -> string 40 val position: T -> Position.T 41 eqtype binding 42 val binding: T * Position.T -> binding 43 val binding0: T -> binding 44 val map_binding: (T -> T) -> binding -> binding 45 val dest_binding: binding -> T * Position.T 46 val path_of_binding: binding -> T 47 val pos_of_binding: binding -> Position.T 48 val proper_binding: binding -> unit 49 val implode_binding: binding -> string 50 val explode_binding: string * Position.T -> binding 51 val explode_binding0: string -> binding 52end; 53 54structure Path: PATH = 55struct 56 57(* path elements *) 58 59datatype elem = 60 Root of string | 61 Basic of string | 62 Variable of string | 63 Parent; 64 65local 66 67fun err_elem msg s = error (msg ^ " path element " ^ quote s); 68 69val illegal_elem = ["", "~", "~~", ".", ".."]; 70val illegal_char = ["/", "\\", "$", ":", "\"", "'", "<", ">", "|", "?", "*"]; 71 72fun check_elem s = 73 if member (op =) illegal_elem s then err_elem "Illegal" s 74 else 75 (s, ()) |-> fold_string (fn c => fn () => 76 if ord c < 32 then 77 err_elem ("Illegal control character " ^ string_of_int (ord c) ^ " in") s 78 else if member (op =) illegal_char c then 79 err_elem ("Illegal character " ^ quote c ^ " in") s 80 else ()); 81 82in 83 84val root_elem = Root o tap check_elem; 85val basic_elem = Basic o tap check_elem; 86val variable_elem = Variable o tap check_elem; 87 88end; 89 90 91(* type path *) 92 93datatype T = Path of elem list; (*reversed elements*) 94 95fun rep (Path xs) = xs; 96 97fun is_current (Path []) = true 98 | is_current _ = false; 99 100val current = Path []; 101val root = Path [Root ""]; 102fun named_root s = Path [root_elem s]; 103val make = Path o rev o map basic_elem; 104fun basic s = Path [basic_elem s]; 105fun variable s = Path [variable_elem s]; 106val parent = Path [Parent]; 107 108fun has_parent (Path xs) = exists (fn Parent => true | _ => false) xs; 109 110fun is_absolute (Path xs) = 111 (case try List.last xs of 112 SOME (Root _) => true 113 | _ => false); 114 115fun is_basic (Path [Basic _]) = true 116 | is_basic _ = false; 117 118fun all_basic (Path elems) = 119 forall (fn Basic _ => true | _ => false) elems; 120 121fun starts_basic (Path xs) = 122 (case try List.last xs of 123 SOME (Basic _) => true 124 | _ => false); 125 126 127(* append and norm *) 128 129fun apply (y as Root _) _ = [y] 130 | apply Parent (xs as (Root _ :: _)) = xs 131 | apply Parent (Basic _ :: rest) = rest 132 | apply y xs = y :: xs; 133 134fun append (Path xs) (Path ys) = Path (fold_rev apply ys xs); 135fun appends paths = Library.foldl (uncurry append) (current, paths); 136 137fun norm elems = fold_rev apply elems []; 138 139 140(* implode *) 141 142local 143 144fun implode_elem (Root "") = "" 145 | implode_elem (Root s) = "//" ^ s 146 | implode_elem (Basic s) = s 147 | implode_elem (Variable s) = "$" ^ s 148 | implode_elem Parent = ".."; 149 150in 151 152fun implode_path (Path []) = "." 153 | implode_path (Path [Root ""]) = "/" 154 | implode_path (Path xs) = space_implode "/" (rev (map implode_elem xs)); 155 156end; 157 158 159(* explode *) 160 161fun explode_path str = 162 let 163 fun explode_elem s = 164 (if s = ".." then Parent 165 else if s = "~" then Variable "USER_HOME" 166 else if s = "~~" then Variable "ISABELLE_HOME" 167 else 168 (case try (unprefix "$") s of 169 SOME s' => variable_elem s' 170 | NONE => basic_elem s)) 171 handle ERROR msg => cat_error msg ("The error(s) above occurred in " ^ quote str); 172 173 val (roots, raw_elems) = 174 (case chop_prefix (equal "") (space_explode "/" str) |>> length of 175 (0, es) => ([], es) 176 | (1, es) => ([Root ""], es) 177 | (_, []) => ([Root ""], []) 178 | (_, e :: es) => ([root_elem e], es)); 179 val elems = raw_elems |> filter_out (fn c => c = "" orelse c = ".") |> map explode_elem; 180 181 in Path (norm (rev elems @ roots)) end; 182 183fun explode_pos (s, pos) = 184 (explode_path s handle ERROR msg => error (msg ^ Position.here pos), pos); 185 186fun split str = 187 space_explode ":" str 188 |> map_filter (fn s => if s = "" then NONE else SOME (explode_path s)); 189 190val decode = XML.Decode.string #> explode_path; 191 192 193(* print *) 194 195fun pretty path = 196 let val s = implode_path path 197 in Pretty.mark (Markup.path s) (Pretty.str (quote s)) end; 198 199val print = Pretty.unformatted_string_of o pretty; 200 201val _ = ML_system_pp (fn _ => fn _ => Pretty.to_polyml o pretty); 202 203 204(* base element *) 205 206fun split_path f (Path (Basic s :: xs)) = f (Path xs, s) 207 | split_path _ path = error ("Cannot split path into dir/base: " ^ print path); 208 209val dir = split_path #1; 210val base = split_path (fn (_, s) => Path [Basic s]); 211 212fun ext "" = I 213 | ext e = split_path (fn (prfx, s) => append prfx (basic (s ^ "." ^ e))); 214 215val split_ext = split_path (fn (prfx, s) => apfst (append prfx) 216 (case chop_suffix (fn c => c <> ".") (raw_explode s) of 217 ([], _) => (Path [Basic s], "") 218 | (cs, e) => (Path [Basic (implode (take (length cs - 1) cs))], implode e))); 219 220val exe = ML_System.platform_is_windows ? ext "exe"; 221 222 223(* expand variables *) 224 225fun eval (Variable s) = 226 let val path = explode_path (getenv_strict s) in 227 if exists (fn Variable _ => true | _ => false) (rep path) then 228 error ("Illegal path variable nesting: " ^ s ^ "=" ^ print path) 229 else rep path 230 end 231 | eval x = [x]; 232 233val expand = rep #> maps eval #> norm #> Path; 234 235val file_name = implode_path o base o expand; 236 237 238(* smart implode *) 239 240fun smart_implode path = 241 let 242 val full_name = implode_path (expand path); 243 fun fold_path a = 244 (case try (implode_path o expand o explode_path) a of 245 SOME b => 246 if full_name = b then SOME a 247 else 248 (case try (unprefix (b ^ "/")) full_name of 249 SOME name => SOME (a ^ "/" ^ name) 250 | NONE => NONE) 251 | NONE => NONE); 252 in 253 (case get_first fold_path ["$AFP", "~~", "$ISABELLE_HOME_USER", "~"] of 254 SOME name => name 255 | NONE => implode_path path) 256 end; 257 258val position = Position.file o smart_implode; 259 260 261(* binding: strictly monotonic path with position *) 262 263datatype binding = Binding of T * Position.T; 264 265fun binding (path, pos) = 266 if all_basic path then Binding (path, pos) 267 else error ("Bad path binding: " ^ print path ^ Position.here pos); 268 269fun binding0 path = binding (path, Position.none); 270 271fun map_binding f (Binding (path, pos)) = binding (f path, pos); 272 273fun dest_binding (Binding args) = args; 274val path_of_binding = dest_binding #> #1; 275val pos_of_binding = dest_binding #> #2; 276 277fun proper_binding binding = 278 if is_current (path_of_binding binding) 279 then error ("Empty path" ^ Position.here (pos_of_binding binding)) 280 else (); 281 282val implode_binding = path_of_binding #> implode_path; 283 284val explode_binding = binding o explode_pos; 285fun explode_binding0 s = explode_binding (s, Position.none); 286 287 288(*final declarations of this structure!*) 289val implode = implode_path; 290val explode = explode_path; 291 292end; 293