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