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
|
|
13 |
val current: T
|
|
14 |
val root: T
|
|
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
|
5011
|
21 |
val pack: T -> string
|
|
22 |
val unpack: string -> T
|
6183
|
23 |
val base: T -> T
|
|
24 |
val ext: string -> T -> T
|
|
25 |
val expand: T -> T
|
5011
|
26 |
end;
|
|
27 |
|
6187
|
28 |
structure Path: PATH =
|
5011
|
29 |
struct
|
|
30 |
|
6183
|
31 |
|
|
32 |
(* path elements *)
|
|
33 |
|
|
34 |
datatype elem = Root | Parent | Basic of string | Variable of string;
|
|
35 |
|
|
36 |
fun no_meta_chars chs =
|
|
37 |
(case ["/", "\\", "$", "~"] inter_string chs of
|
|
38 |
[] => chs
|
|
39 |
| bads => error ("Illegal character(s) " ^ commas_quote bads ^
|
|
40 |
" in path element specification: " ^ quote (implode chs)));
|
|
41 |
|
|
42 |
val basic_elem = Basic o implode o no_meta_chars;
|
|
43 |
val variable_elem = Variable o implode o no_meta_chars;
|
|
44 |
|
|
45 |
fun is_var (Variable _) = true
|
|
46 |
| is_var _ = false;
|
|
47 |
|
|
48 |
|
5011
|
49 |
(* type path *)
|
|
50 |
|
6183
|
51 |
datatype T = Path of elem list;
|
|
52 |
|
|
53 |
fun rep (Path xs) = xs;
|
5011
|
54 |
|
|
55 |
val current = Path [];
|
6183
|
56 |
val root = Path [Root];
|
|
57 |
val parent = Path [Parent];
|
|
58 |
fun basic s = Path [basic_elem (explode s)];
|
|
59 |
fun variable s = Path [variable_elem (explode s)];
|
5011
|
60 |
|
6183
|
61 |
fun is_absolute (Path (Root :: _)) = true
|
|
62 |
| is_absolute _ = false;
|
5011
|
63 |
|
6183
|
64 |
fun is_basic (Path [Basic _]) = true
|
|
65 |
| is_basic _ = false;
|
5011
|
66 |
|
|
67 |
|
|
68 |
(* append and norm *)
|
|
69 |
|
|
70 |
(*append non-normal path (2n arg) to reversed normal one, result is normal*)
|
|
71 |
fun rev_app xs [] = rev xs
|
6183
|
72 |
| rev_app _ (Root :: ys) = rev_app [Root] ys
|
|
73 |
| rev_app (x :: xs) (Parent :: ys) =
|
|
74 |
if x = Parent orelse is_var x then rev_app (Parent :: x :: xs) ys
|
|
75 |
else if x = Root then rev_app (x :: xs) ys
|
5011
|
76 |
else rev_app xs ys
|
|
77 |
| rev_app xs (y :: ys) = rev_app (y :: xs) ys;
|
|
78 |
|
6183
|
79 |
fun append (Path xs) (Path ys) = Path (rev_app (rev xs) ys);
|
5011
|
80 |
fun norm path = rev_app [] path;
|
|
81 |
|
6183
|
82 |
|
|
83 |
(* pack *)
|
5011
|
84 |
|
6183
|
85 |
fun pack_elem Root = ""
|
|
86 |
| pack_elem Parent = ".."
|
|
87 |
| pack_elem (Basic s) = s
|
|
88 |
| pack_elem (Variable s) = "$" ^ s;
|
5011
|
89 |
|
|
90 |
fun pack (Path []) = "."
|
6183
|
91 |
| pack (Path (Root :: xs)) = "/" ^ space_implode "/" (map pack_elem xs)
|
|
92 |
| pack (Path xs) = space_implode "/" (map pack_elem xs);
|
5011
|
93 |
|
|
94 |
|
6183
|
95 |
(* unpack *)
|
|
96 |
|
|
97 |
fun unpack_elem "" = Root
|
|
98 |
| unpack_elem ".." = Parent
|
|
99 |
| unpack_elem "~" = Variable "HOME"
|
|
100 |
| unpack_elem "~~" = Variable "ISABELLE_HOME"
|
|
101 |
| unpack_elem s =
|
|
102 |
(case explode s of
|
|
103 |
"$" :: cs => variable_elem cs
|
|
104 |
| cs => basic_elem cs);
|
|
105 |
|
|
106 |
val unpack_elems = map unpack_elem o filter_out (equal "" orf equal ".");
|
|
107 |
|
|
108 |
fun unpack str = Path (norm
|
|
109 |
(case space_explode "/" str of
|
|
110 |
"" :: ss => Root :: unpack_elems ss
|
|
111 |
| ss => unpack_elems ss));
|
|
112 |
|
5011
|
113 |
|
6183
|
114 |
(* base element *)
|
|
115 |
|
|
116 |
fun err_no_base path =
|
|
117 |
error ("No base path element in " ^ quote (pack path));
|
|
118 |
|
|
119 |
fun base (path as Path xs) =
|
|
120 |
(case try split_last xs of
|
|
121 |
Some (_, x as Basic _) => Path [x]
|
|
122 |
| _ => err_no_base path);
|
|
123 |
|
|
124 |
fun ext e (path as Path xs) =
|
|
125 |
(case try split_last xs of
|
|
126 |
Some (prfx, Basic s) => if e = "" then path else Path (prfx @ [Basic (s ^ "." ^ e)])
|
|
127 |
| _ => err_no_base path);
|
|
128 |
|
|
129 |
|
|
130 |
(* evaluate variables *)
|
|
131 |
|
|
132 |
fun eval env (Variable s) = rep (env s)
|
|
133 |
| eval _ x = [x];
|
5011
|
134 |
|
|
135 |
fun evaluate env (Path xs) =
|
|
136 |
Path (norm (flat (map (eval env) xs)));
|
|
137 |
|
6183
|
138 |
val expand = evaluate (unpack o getenv);
|
5011
|
139 |
|
|
140 |
|
|
141 |
end;
|