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