6118
|
1 |
(* Title: Pure/General/path.ML
|
5011
|
2 |
ID: $Id$
|
|
3 |
Author: Markus Wenzel, TU Muenchen
|
|
4 |
|
|
5 |
Abstract algebra of file paths. External representation Unix-style.
|
|
6 |
*)
|
|
7 |
|
|
8 |
signature PATH =
|
|
9 |
sig
|
|
10 |
type T
|
|
11 |
val pack: T -> string
|
|
12 |
val unpack: string -> T
|
|
13 |
val current: T
|
|
14 |
val parent: T
|
|
15 |
val root: T
|
|
16 |
val variable: string -> T
|
|
17 |
val absolute: T -> bool
|
|
18 |
val base: T -> string
|
|
19 |
val append: T -> T -> T
|
|
20 |
val evaluate: (string -> T) -> T -> T
|
|
21 |
val expand: (string -> string) -> string -> string
|
|
22 |
val base_name: string -> string
|
|
23 |
val is_base: string -> bool
|
|
24 |
end;
|
|
25 |
|
|
26 |
structure Path: PATH =
|
|
27 |
struct
|
|
28 |
|
|
29 |
(* type path *)
|
|
30 |
|
|
31 |
datatype T = Path of string list;
|
|
32 |
|
|
33 |
val current = Path [];
|
|
34 |
val parent = Path [".."];
|
|
35 |
val root = Path ["/"];
|
|
36 |
|
|
37 |
fun absolute (Path ("/" :: _)) = true
|
|
38 |
| absolute _ = false;
|
|
39 |
|
|
40 |
fun base (Path []) = ""
|
|
41 |
| base (Path ["/"]) = ""
|
|
42 |
| base (Path xs) = snd (split_last xs);
|
|
43 |
|
|
44 |
fun variable name = Path ["$" ^ name];
|
|
45 |
fun is_variable elem = ord elem = ord "$";
|
|
46 |
|
|
47 |
|
|
48 |
(* append and norm *)
|
|
49 |
|
|
50 |
(*append non-normal path (2n arg) to reversed normal one, result is normal*)
|
|
51 |
fun rev_app xs [] = rev xs
|
|
52 |
| rev_app _ ("/" :: ys) = rev_app ["/"] ys
|
|
53 |
| rev_app xs ("." :: ys) = rev_app xs ys
|
|
54 |
| rev_app (x :: xs) (".." :: ys) =
|
|
55 |
if x = ".." orelse is_variable x then rev_app (".." :: x :: xs) ys
|
|
56 |
else if x = "/" then rev_app (x :: xs) ys
|
|
57 |
else rev_app xs ys
|
|
58 |
| rev_app xs (y :: ys) = rev_app (y :: xs) ys;
|
|
59 |
|
|
60 |
fun norm path = rev_app [] path;
|
|
61 |
|
|
62 |
fun append (Path xs) (Path ys) = Path (rev_app (rev xs) ys);
|
|
63 |
|
|
64 |
|
|
65 |
(* pack and unpack *)
|
|
66 |
|
|
67 |
fun pack (Path []) = "."
|
|
68 |
| pack (Path ("/" :: xs)) = "/" ^ space_implode "/" xs
|
|
69 |
| pack (Path xs) = space_implode "/" xs;
|
|
70 |
|
|
71 |
fun unpack str =
|
|
72 |
(case space_explode "/" str of
|
|
73 |
[""] => []
|
|
74 |
| "" :: xs => "/" :: filter (not_equal "") xs
|
|
75 |
| xs => filter (not_equal "") xs)
|
|
76 |
|> map (fn "~" => "$HOME" | x => x)
|
|
77 |
|> norm
|
|
78 |
|> Path;
|
|
79 |
|
|
80 |
|
|
81 |
(* eval variables *)
|
|
82 |
|
|
83 |
fun eval env x =
|
|
84 |
if is_variable x then
|
|
85 |
let val Path ys = env (implode (tl (explode x)))
|
|
86 |
in ys end
|
|
87 |
else [x];
|
|
88 |
|
|
89 |
fun evaluate env (Path xs) =
|
|
90 |
Path (norm (flat (map (eval env) xs)));
|
|
91 |
|
|
92 |
|
|
93 |
(* operations on packed paths *)
|
|
94 |
|
|
95 |
fun expand env str =
|
|
96 |
pack (evaluate (unpack o env) (unpack str));
|
|
97 |
|
|
98 |
val base_name = base o unpack;
|
|
99 |
|
|
100 |
fun is_base str =
|
|
101 |
not (exists (equal "/" orf equal "$") (explode str));
|
|
102 |
|
|
103 |
|
|
104 |
end;
|