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