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