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