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