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