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