6118
|
1 |
(* Title: Pure/General/path.ML
|
5011
|
2 |
ID: $Id$
|
|
3 |
Author: Markus Wenzel, TU Muenchen
|
|
4 |
|
6183
|
5 |
Abstract algebra of file paths (external encoding Unix-style).
|
5011
|
6 |
*)
|
|
7 |
|
|
8 |
signature PATH =
|
|
9 |
sig
|
6183
|
10 |
datatype elem = Root | Parent | Basic of string | Variable of string
|
|
11 |
eqtype T
|
|
12 |
val rep: T -> elem list
|
6460
|
13 |
val is_current: T -> bool
|
6183
|
14 |
val current: T
|
|
15 |
val root: T
|
|
16 |
val parent: T
|
|
17 |
val basic: string -> T
|
|
18 |
val variable: string -> T
|
|
19 |
val is_absolute: T -> bool
|
|
20 |
val is_basic: T -> bool
|
|
21 |
val append: T -> T -> T
|
6270
|
22 |
val appends: T list -> T
|
6319
|
23 |
val make: string list -> T
|
5011
|
24 |
val pack: T -> string
|
|
25 |
val unpack: 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
|
7714
|
31 |
val position: T -> Position.T
|
5011
|
32 |
end;
|
|
33 |
|
6187
|
34 |
structure Path: PATH =
|
5011
|
35 |
struct
|
|
36 |
|
6183
|
37 |
|
|
38 |
(* path elements *)
|
|
39 |
|
|
40 |
datatype elem = Root | Parent | Basic of string | Variable of string;
|
|
41 |
|
6223
|
42 |
fun err_elem msg chs = error (msg ^ " path element specification: " ^ quote (implode chs));
|
6183
|
43 |
|
6319
|
44 |
fun check_elem (chs as []) = err_elem "Illegal" chs
|
|
45 |
| check_elem (chs as ["~"]) = err_elem "Illegal" chs
|
6223
|
46 |
| check_elem (chs as ["~", "~"]) = err_elem "Illegal" chs
|
|
47 |
| check_elem chs =
|
|
48 |
(case ["/", "\\", "$", ":"] inter_string chs of
|
|
49 |
[] => chs
|
|
50 |
| bads => err_elem ("Illegal character(s) " ^ commas_quote bads ^ " in") chs);
|
|
51 |
|
|
52 |
val basic_elem = Basic o implode o check_elem;
|
|
53 |
val variable_elem = Variable o implode o check_elem;
|
6183
|
54 |
|
|
55 |
fun is_var (Variable _) = true
|
|
56 |
| is_var _ = false;
|
|
57 |
|
|
58 |
|
5011
|
59 |
(* type path *)
|
|
60 |
|
6183
|
61 |
datatype T = Path of elem list;
|
|
62 |
|
|
63 |
fun rep (Path xs) = xs;
|
5011
|
64 |
|
6460
|
65 |
fun is_current (Path []) = true
|
|
66 |
| is_current _ = false;
|
|
67 |
|
5011
|
68 |
val current = Path [];
|
6183
|
69 |
val root = Path [Root];
|
|
70 |
val parent = Path [Parent];
|
|
71 |
fun basic s = Path [basic_elem (explode s)];
|
|
72 |
fun variable s = Path [variable_elem (explode s)];
|
5011
|
73 |
|
6183
|
74 |
fun is_absolute (Path (Root :: _)) = true
|
|
75 |
| is_absolute _ = false;
|
5011
|
76 |
|
6183
|
77 |
fun is_basic (Path [Basic _]) = true
|
|
78 |
| is_basic _ = false;
|
5011
|
79 |
|
|
80 |
|
|
81 |
(* append and norm *)
|
|
82 |
|
|
83 |
(*append non-normal path (2n arg) to reversed normal one, result is normal*)
|
|
84 |
fun rev_app xs [] = rev xs
|
6183
|
85 |
| rev_app _ (Root :: ys) = rev_app [Root] ys
|
|
86 |
| rev_app (x :: xs) (Parent :: ys) =
|
|
87 |
if x = Parent orelse is_var x then rev_app (Parent :: x :: xs) ys
|
|
88 |
else if x = Root then rev_app (x :: xs) ys
|
5011
|
89 |
else rev_app xs ys
|
|
90 |
| rev_app xs (y :: ys) = rev_app (y :: xs) ys;
|
|
91 |
|
6183
|
92 |
fun append (Path xs) (Path ys) = Path (rev_app (rev xs) ys);
|
15570
|
93 |
fun appends paths = Library.foldl (uncurry append) (current, paths);
|
6319
|
94 |
val make = appends o map basic;
|
5011
|
95 |
fun norm path = rev_app [] path;
|
|
96 |
|
6183
|
97 |
|
|
98 |
(* pack *)
|
5011
|
99 |
|
6183
|
100 |
fun pack_elem Root = ""
|
|
101 |
| pack_elem Parent = ".."
|
|
102 |
| pack_elem (Basic s) = s
|
|
103 |
| pack_elem (Variable s) = "$" ^ s;
|
5011
|
104 |
|
|
105 |
fun pack (Path []) = "."
|
6183
|
106 |
| pack (Path (Root :: xs)) = "/" ^ space_implode "/" (map pack_elem xs)
|
|
107 |
| pack (Path xs) = space_implode "/" (map pack_elem xs);
|
5011
|
108 |
|
|
109 |
|
6183
|
110 |
(* unpack *)
|
|
111 |
|
|
112 |
fun unpack_elem "" = Root
|
|
113 |
| unpack_elem ".." = Parent
|
|
114 |
| unpack_elem "~" = Variable "HOME"
|
|
115 |
| unpack_elem "~~" = Variable "ISABELLE_HOME"
|
|
116 |
| unpack_elem s =
|
|
117 |
(case explode s of
|
|
118 |
"$" :: cs => variable_elem cs
|
|
119 |
| cs => basic_elem cs);
|
|
120 |
|
|
121 |
val unpack_elems = map unpack_elem o filter_out (equal "" orf equal ".");
|
|
122 |
|
|
123 |
fun unpack str = Path (norm
|
|
124 |
(case space_explode "/" str of
|
|
125 |
"" :: ss => Root :: unpack_elems ss
|
|
126 |
| ss => unpack_elems ss));
|
|
127 |
|
5011
|
128 |
|
6183
|
129 |
(* base element *)
|
|
130 |
|
7929
|
131 |
fun split_path f (path as Path xs) =
|
|
132 |
(case try split_last xs of
|
15531
|
133 |
SOME (prfx, Basic s) => f (prfx, s)
|
7929
|
134 |
| _ => error ("Cannot split path into dir/base: " ^ quote (pack path)));
|
6183
|
135 |
|
14912
|
136 |
val dir = split_path (fn (prfx, _) => Path prfx);
|
7929
|
137 |
val base = split_path (fn (_, s) => Path [Basic s]);
|
6183
|
138 |
|
7929
|
139 |
fun ext "" path = path
|
|
140 |
| ext e path = split_path (fn (prfx, s) => append (Path prfx) (basic (s ^ "." ^ e))) path;
|
6183
|
141 |
|
14912
|
142 |
val split_ext = split_path (fn (prfx, s) => apfst (append (Path prfx))
|
7929
|
143 |
(case take_suffix (not_equal ".") (explode s) of
|
14912
|
144 |
([], _) => (Path [Basic s], "")
|
15570
|
145 |
| (cs, e) => (Path [Basic (implode (Library.take (length cs - 1, cs)))], implode e)));
|
6319
|
146 |
|
6183
|
147 |
|
17827
|
148 |
(* expand variables *)
|
5011
|
149 |
|
17827
|
150 |
fun eval (Variable s) =
|
|
151 |
(case getenv s of
|
|
152 |
"" => error ("Undefined Isabelle environment variable: " ^ quote s)
|
|
153 |
| path => rep (unpack path))
|
|
154 |
| eval x = [x];
|
5011
|
155 |
|
17827
|
156 |
val expand = rep #> map eval #> List.concat #> norm #> Path;
|
|
157 |
val position = expand #> pack #> quote #> Position.line_name 1;
|
5011
|
158 |
|
|
159 |
end;
|