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