src/Pure/General/path.ML
author haftmann
Tue Oct 20 16:13:01 2009 +0200 (2009-10-20)
changeset 33037 b22e44496dc2
parent 29606 fedb8be05f24
child 33038 8f9594c31de4
permissions -rw-r--r--
replaced old_style infixes eq_set, subset, union, inter and variants by generic versions
     1 (*  Title:      Pure/General/path.ML
     2     Author:     Markus Wenzel, TU Muenchen
     3 
     4 Abstract algebra of file paths (external encoding in Unix style).
     5 *)
     6 
     7 signature PATH =
     8 sig
     9   eqtype T
    10   val is_current: T -> bool
    11   val current: T
    12   val root: T
    13   val parent: T
    14   val basic: string -> T
    15   val variable: string -> T
    16   val is_absolute: T -> bool
    17   val is_basic: T -> bool
    18   val append: T -> T -> T
    19   val appends: T list -> T
    20   val make: string list -> T
    21   val implode: T -> string
    22   val explode: string -> T
    23   val dir: T -> T
    24   val base: T -> T
    25   val ext: string -> T -> T
    26   val split_ext: T -> T * string
    27   val expand: T -> T
    28   val position: T -> Position.T
    29 end;
    30 
    31 structure Path: PATH =
    32 struct
    33 
    34 
    35 (* path elements *)
    36 
    37 datatype elem = Root | Parent | Basic of string | Variable of string;
    38 
    39 fun err_elem msg chs = error (msg ^ " path element specification: " ^ quote (implode chs));
    40 
    41 fun check_elem (chs as []) = err_elem "Illegal" chs
    42   | check_elem (chs as ["~"]) = err_elem "Illegal" chs
    43   | check_elem (chs as ["~", "~"]) = err_elem "Illegal" chs
    44   | check_elem chs =
    45       (case gen_inter (op =) (["/", "\\", "$", ":"], chs) of
    46         [] => chs
    47       | bads => err_elem ("Illegal character(s) " ^ commas_quote bads ^ " in") chs);
    48 
    49 val basic_elem = Basic o implode o check_elem;
    50 val variable_elem = Variable o implode o check_elem;
    51 
    52 fun is_var (Variable _) = true
    53   | is_var _ = false;
    54 
    55 
    56 (* type path *)
    57 
    58 datatype T = Path of elem list;
    59 
    60 fun rep (Path xs) = xs;
    61 
    62 fun is_current (Path []) = true
    63   | is_current _ = false;
    64 
    65 val current = Path [];
    66 val root = Path [Root];
    67 val parent = Path [Parent];
    68 fun basic s = Path [basic_elem (explode s)];
    69 fun variable s = Path [variable_elem (explode s)];
    70 
    71 fun is_absolute (Path (Root :: _)) = true
    72   | is_absolute _ = false;
    73 
    74 fun is_basic (Path [Basic _]) = true
    75   | is_basic _ = false;
    76 
    77 
    78 (* append and norm *)
    79 
    80 (*append non-normal path (2n arg) to reversed normal one, result is normal*)
    81 fun rev_app xs [] = rev xs
    82   | rev_app _ (Root :: ys) = rev_app [Root] ys
    83   | rev_app (x :: xs) (Parent :: ys) =
    84       if x = Parent orelse is_var x then rev_app (Parent :: x :: xs) ys
    85       else if x = Root then rev_app (x :: xs) ys
    86       else rev_app xs ys
    87   | rev_app xs (y :: ys) = rev_app (y :: xs) ys;
    88 
    89 fun append (Path xs) (Path ys) = Path (rev_app (rev xs) ys);
    90 fun appends paths = Library.foldl (uncurry append) (current, paths);
    91 val make = appends o map basic;
    92 fun norm path = rev_app [] path;
    93 
    94 
    95 (* implode *)
    96 
    97 fun implode_elem Root = ""
    98   | implode_elem Parent = ".."
    99   | implode_elem (Basic s) = s
   100   | implode_elem (Variable s) = "$" ^ s;
   101 
   102 fun implode_path (Path []) = "."
   103   | implode_path (Path (Root :: xs)) = "/" ^ space_implode "/" (map implode_elem xs)
   104   | implode_path (Path xs) = space_implode "/" (map implode_elem xs);
   105 
   106 
   107 (* explode *)
   108 
   109 fun explode_elem "" = Root
   110   | explode_elem ".." = Parent
   111   | explode_elem "~" = Variable "HOME"
   112   | explode_elem "~~" = Variable "ISABELLE_HOME"
   113   | explode_elem s =
   114       (case explode s of
   115         "$" :: cs => variable_elem cs
   116       | cs => basic_elem cs);
   117 
   118 val explode_elems = map explode_elem o filter_out (fn c => c = "" orelse c = ".");
   119 
   120 fun explode_path str = Path (norm
   121   (case space_explode "/" str of
   122     "" :: ss => Root :: explode_elems ss
   123   | ss => explode_elems ss));
   124 
   125 
   126 (* base element *)
   127 
   128 fun split_path f (path as Path xs) =
   129   (case try split_last xs of
   130     SOME (prfx, Basic s) => f (prfx, s)
   131   | _ => error ("Cannot split path into dir/base: " ^ quote (implode_path path)));
   132 
   133 val dir = split_path (fn (prfx, _) => Path prfx);
   134 val base = split_path (fn (_, s) => Path [Basic s]);
   135 
   136 fun ext "" path = path
   137   | ext e path = split_path (fn (prfx, s) => append (Path prfx) (basic (s ^ "." ^ e))) path;
   138 
   139 val split_ext = split_path (fn (prfx, s) => apfst (append (Path prfx))
   140   (case take_suffix (fn c => c <> ".") (explode s) of
   141     ([], _) => (Path [Basic s], "")
   142   | (cs, e) => (Path [Basic (implode (Library.take (length cs - 1, cs)))], implode e)));
   143 
   144 
   145 (* expand variables *)
   146 
   147 fun eval (Variable s) =
   148     (case getenv s of
   149       "" => error ("Undefined Isabelle environment variable: " ^ quote s)
   150     | path => rep (explode_path path))
   151   | eval x = [x];
   152 
   153 val expand = rep #> maps eval #> norm #> Path;
   154 
   155 
   156 (* source position *)
   157 
   158 val position = Position.file o implode_path o expand;
   159 
   160 
   161 (*final declarations of this structure!*)
   162 val implode = implode_path;
   163 val explode = explode_path;
   164 
   165 end;