author | wenzelm |
Sun, 13 Mar 2011 16:01:00 +0100 | |
changeset 41944 | b97091ae583a |
parent 40627 | becf5d5187cc |
child 43593 | 11140987d415 |
permissions | -rw-r--r-- |
6118 | 1 |
(* Title: Pure/General/path.ML |
5011 | 2 |
Author: Markus Wenzel, TU Muenchen |
3 |
||
36135
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset
|
4 |
Abstract algebra of file paths: basic POSIX notation, extended by |
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset
|
5 |
named roots (e.g. //foo) and variables (e.g. $BAR). |
5011 | 6 |
*) |
7 |
||
8 |
signature PATH = |
|
9 |
sig |
|
6183 | 10 |
eqtype T |
6460 | 11 |
val is_current: T -> bool |
6183 | 12 |
val current: T |
13 |
val root: T |
|
36135
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset
|
14 |
val named_root: string -> T |
6183 | 15 |
val parent: T |
16 |
val basic: string -> T |
|
17 |
val variable: string -> T |
|
18 |
val is_absolute: T -> bool |
|
19 |
val is_basic: T -> bool |
|
20 |
val append: T -> T -> T |
|
6270 | 21 |
val appends: T list -> T |
6319 | 22 |
val make: string list -> T |
41944
b97091ae583a
Path.print is the official way to show file-system paths to users -- note that Path.implode often indicates violation of the abstract datatype;
wenzelm
parents:
40627
diff
changeset
|
23 |
val print: T -> string |
21858
05f57309170c
avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents:
19482
diff
changeset
|
24 |
val implode: T -> string |
05f57309170c
avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents:
19482
diff
changeset
|
25 |
val explode: string -> T |
14912 | 26 |
val dir: T -> T |
6183 | 27 |
val base: T -> T |
28 |
val ext: string -> T -> T |
|
14912 | 29 |
val split_ext: T -> T * string |
6183 | 30 |
val expand: T -> T |
26881 | 31 |
val position: T -> Position.T |
5011 | 32 |
end; |
33 |
||
6187 | 34 |
structure Path: PATH = |
5011 | 35 |
struct |
36 |
||
6183 | 37 |
(* path elements *) |
38 |
||
36135
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset
|
39 |
datatype elem = |
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset
|
40 |
Root of string | |
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset
|
41 |
Basic of string | |
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset
|
42 |
Variable of string | |
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset
|
43 |
Parent; |
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset
|
44 |
|
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset
|
45 |
local |
6183 | 46 |
|
6223 | 47 |
fun err_elem msg chs = error (msg ^ " path element specification: " ^ quote (implode chs)); |
6183 | 48 |
|
6319 | 49 |
fun check_elem (chs as []) = err_elem "Illegal" chs |
50 |
| check_elem (chs as ["~"]) = err_elem "Illegal" chs |
|
6223 | 51 |
| check_elem (chs as ["~", "~"]) = err_elem "Illegal" chs |
52 |
| check_elem chs = |
|
33049
c38f02fdf35d
curried inter as canonical list operation (beware of argument order)
haftmann
parents:
33038
diff
changeset
|
53 |
(case inter (op =) ["/", "\\", "$", ":"] chs of |
6223 | 54 |
[] => chs |
55 |
| bads => err_elem ("Illegal character(s) " ^ commas_quote bads ^ " in") chs); |
|
56 |
||
36135
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset
|
57 |
in |
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset
|
58 |
|
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset
|
59 |
val root_elem = Root o implode o check_elem; |
6223 | 60 |
val basic_elem = Basic o implode o check_elem; |
61 |
val variable_elem = Variable o implode o check_elem; |
|
6183 | 62 |
|
36135
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset
|
63 |
end; |
6183 | 64 |
|
65 |
||
5011 | 66 |
(* type path *) |
67 |
||
36135
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset
|
68 |
datatype T = Path of elem list; (*reversed elements*) |
6183 | 69 |
|
70 |
fun rep (Path xs) = xs; |
|
5011 | 71 |
|
6460 | 72 |
fun is_current (Path []) = true |
73 |
| is_current _ = false; |
|
74 |
||
5011 | 75 |
val current = Path []; |
36135
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset
|
76 |
val root = Path [Root ""]; |
40627
becf5d5187cc
renamed raw "explode" function to "raw_explode" to emphasize its meaning;
wenzelm
parents:
36135
diff
changeset
|
77 |
fun named_root s = Path [root_elem (raw_explode s)]; |
becf5d5187cc
renamed raw "explode" function to "raw_explode" to emphasize its meaning;
wenzelm
parents:
36135
diff
changeset
|
78 |
fun basic s = Path [basic_elem (raw_explode s)]; |
becf5d5187cc
renamed raw "explode" function to "raw_explode" to emphasize its meaning;
wenzelm
parents:
36135
diff
changeset
|
79 |
fun variable s = Path [variable_elem (raw_explode s)]; |
36135
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset
|
80 |
val parent = Path [Parent]; |
5011 | 81 |
|
36135
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset
|
82 |
fun is_absolute (Path xs) = |
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset
|
83 |
(case try List.last xs of |
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset
|
84 |
SOME (Root _) => true |
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset
|
85 |
| _ => false); |
5011 | 86 |
|
6183 | 87 |
fun is_basic (Path [Basic _]) = true |
88 |
| is_basic _ = false; |
|
5011 | 89 |
|
90 |
||
91 |
(* append and norm *) |
|
92 |
||
36135
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset
|
93 |
fun apply (y as Root _) _ = [y] |
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset
|
94 |
| apply Parent (xs as (Root _ :: _)) = xs |
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset
|
95 |
| apply Parent (Basic _ :: rest) = rest |
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset
|
96 |
| apply y xs = y :: xs; |
5011 | 97 |
|
36135
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset
|
98 |
fun append (Path xs) (Path ys) = Path (fold_rev apply ys xs); |
15570 | 99 |
fun appends paths = Library.foldl (uncurry append) (current, paths); |
6319 | 100 |
val make = appends o map basic; |
36135
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset
|
101 |
|
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset
|
102 |
fun norm elems = fold_rev apply elems []; |
5011 | 103 |
|
6183 | 104 |
|
21858
05f57309170c
avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents:
19482
diff
changeset
|
105 |
(* implode *) |
5011 | 106 |
|
36135
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset
|
107 |
local |
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset
|
108 |
|
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset
|
109 |
fun implode_elem (Root "") = "" |
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset
|
110 |
| implode_elem (Root s) = "//" ^ s |
21858
05f57309170c
avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents:
19482
diff
changeset
|
111 |
| implode_elem (Basic s) = s |
36135
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset
|
112 |
| implode_elem (Variable s) = "$" ^ s |
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset
|
113 |
| implode_elem Parent = ".."; |
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset
|
114 |
|
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset
|
115 |
in |
5011 | 116 |
|
21858
05f57309170c
avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents:
19482
diff
changeset
|
117 |
fun implode_path (Path []) = "." |
36135
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset
|
118 |
| implode_path (Path [Root ""]) = "/" |
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset
|
119 |
| implode_path (Path xs) = space_implode "/" (rev (map implode_elem xs)); |
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset
|
120 |
|
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset
|
121 |
end; |
5011 | 122 |
|
41944
b97091ae583a
Path.print is the official way to show file-system paths to users -- note that Path.implode often indicates violation of the abstract datatype;
wenzelm
parents:
40627
diff
changeset
|
123 |
val print = quote o implode_path; |
b97091ae583a
Path.print is the official way to show file-system paths to users -- note that Path.implode often indicates violation of the abstract datatype;
wenzelm
parents:
40627
diff
changeset
|
124 |
|
5011 | 125 |
|
21858
05f57309170c
avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents:
19482
diff
changeset
|
126 |
(* explode *) |
6183 | 127 |
|
36135
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset
|
128 |
local |
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset
|
129 |
|
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset
|
130 |
fun explode_elem ".." = Parent |
21858
05f57309170c
avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents:
19482
diff
changeset
|
131 |
| explode_elem "~" = Variable "HOME" |
05f57309170c
avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents:
19482
diff
changeset
|
132 |
| explode_elem "~~" = Variable "ISABELLE_HOME" |
05f57309170c
avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents:
19482
diff
changeset
|
133 |
| explode_elem s = |
40627
becf5d5187cc
renamed raw "explode" function to "raw_explode" to emphasize its meaning;
wenzelm
parents:
36135
diff
changeset
|
134 |
(case raw_explode s of |
6183 | 135 |
"$" :: cs => variable_elem cs |
136 |
| cs => basic_elem cs); |
|
137 |
||
36135
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset
|
138 |
val explode_elems = |
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset
|
139 |
rev o map explode_elem o filter_out (fn c => c = "" orelse c = "."); |
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset
|
140 |
|
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset
|
141 |
in |
6183 | 142 |
|
36135
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset
|
143 |
fun explode_path str = |
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset
|
144 |
let val (roots, raw_elems) = |
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset
|
145 |
(case take_prefix (equal "") (space_explode "/" str) |>> length of |
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset
|
146 |
(0, es) => ([], es) |
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset
|
147 |
| (1, es) => ([Root ""], es) |
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset
|
148 |
| (_, []) => ([Root ""], []) |
40627
becf5d5187cc
renamed raw "explode" function to "raw_explode" to emphasize its meaning;
wenzelm
parents:
36135
diff
changeset
|
149 |
| (_, e :: es) => ([root_elem (raw_explode e)], es)) |
36135
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset
|
150 |
in Path (norm (explode_elems raw_elems @ roots)) end; |
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset
|
151 |
|
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset
|
152 |
end; |
6183 | 153 |
|
5011 | 154 |
|
6183 | 155 |
(* base element *) |
156 |
||
36135
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset
|
157 |
fun split_path f (Path (Basic s :: xs)) = f (Path xs, s) |
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset
|
158 |
| split_path _ path = error ("Cannot split path into dir/base: " ^ quote (implode_path path)); |
6183 | 159 |
|
36135
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset
|
160 |
val dir = split_path #1; |
7929 | 161 |
val base = split_path (fn (_, s) => Path [Basic s]); |
6183 | 162 |
|
36135
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset
|
163 |
fun ext "" = I |
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset
|
164 |
| ext e = split_path (fn (prfx, s) => append prfx (basic (s ^ "." ^ e))); |
6183 | 165 |
|
36135
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset
|
166 |
val split_ext = split_path (fn (prfx, s) => apfst (append prfx) |
40627
becf5d5187cc
renamed raw "explode" function to "raw_explode" to emphasize its meaning;
wenzelm
parents:
36135
diff
changeset
|
167 |
(case take_suffix (fn c => c <> ".") (raw_explode s) of |
14912 | 168 |
([], _) => (Path [Basic s], "") |
33957 | 169 |
| (cs, e) => (Path [Basic (implode (take (length cs - 1) cs))], implode e))); |
6319 | 170 |
|
6183 | 171 |
|
17827 | 172 |
(* expand variables *) |
5011 | 173 |
|
36135
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset
|
174 |
local |
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset
|
175 |
|
17827 | 176 |
fun eval (Variable s) = |
36135
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset
|
177 |
(case getenv s of |
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset
|
178 |
"" => error ("Undefined Isabelle environment variable: " ^ quote s) |
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset
|
179 |
| path => rep (explode_path path)) |
17827 | 180 |
| eval x = [x]; |
5011 | 181 |
|
36135
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset
|
182 |
in |
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset
|
183 |
|
19482
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19305
diff
changeset
|
184 |
val expand = rep #> maps eval #> norm #> Path; |
21858
05f57309170c
avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents:
19482
diff
changeset
|
185 |
|
36135
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset
|
186 |
end; |
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset
|
187 |
|
21858
05f57309170c
avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents:
19482
diff
changeset
|
188 |
|
26881 | 189 |
(* source position *) |
190 |
||
191 |
val position = Position.file o implode_path o expand; |
|
192 |
||
193 |
||
21858
05f57309170c
avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents:
19482
diff
changeset
|
194 |
(*final declarations of this structure!*) |
05f57309170c
avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents:
19482
diff
changeset
|
195 |
val implode = implode_path; |
05f57309170c
avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents:
19482
diff
changeset
|
196 |
val explode = explode_path; |
5011 | 197 |
|
198 |
end; |
|
36135
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset
|
199 |