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