more abstract implementation;
authorwenzelm
Wed Feb 03 16:36:38 1999 +0100 (1999-02-03)
changeset 6183ca3ff2fee318
parent 6182 4a07dfe3583f
child 6184 8d7a328e2d0c
more abstract implementation;
src/Pure/General/path.ML
     1.1 --- a/src/Pure/General/path.ML	Wed Feb 03 16:32:32 1999 +0100
     1.2 +++ b/src/Pure/General/path.ML	Wed Feb 03 16:36:38 1999 +0100
     1.3 @@ -2,103 +2,141 @@
     1.4      ID:         $Id$
     1.5      Author:     Markus Wenzel, TU Muenchen
     1.6  
     1.7 -Abstract algebra of file paths.  External representation Unix-style.
     1.8 +Abstract algebra of file paths (external encoding Unix-style).
     1.9  *)
    1.10  
    1.11  signature PATH =
    1.12  sig
    1.13 -  type T
    1.14 +  datatype elem = Root | Parent | Basic of string | Variable of string
    1.15 +  eqtype T
    1.16 +  val rep: T -> elem list
    1.17 +  val current: T
    1.18 +  val root: T
    1.19 +  val parent: T
    1.20 +  val basic: string -> T
    1.21 +  val variable: string -> T
    1.22 +  val is_absolute: T -> bool
    1.23 +  val is_basic: T -> bool
    1.24 +  val append: T -> T -> T
    1.25    val pack: T -> string
    1.26    val unpack: string -> T
    1.27 -  val current: T
    1.28 -  val parent: T
    1.29 -  val root: T
    1.30 -  val variable: string -> T
    1.31 -  val absolute: T -> bool
    1.32 -  val base: T -> string
    1.33 -  val append: T -> T -> T
    1.34 -  val evaluate: (string -> T) -> T -> T
    1.35 -  val expand: (string -> string) -> string -> string
    1.36 -  val base_name: string -> string
    1.37 -  val is_base: string -> bool
    1.38 +  val base: T -> T
    1.39 +  val ext: string -> T -> T
    1.40 +(* FIXME  val evaluate: (string -> T) -> T -> T	*)
    1.41 +  val expand: T -> T
    1.42  end;
    1.43  
    1.44 -structure Path: PATH =
    1.45 +structure Path(* FIXME : PATH *) =
    1.46  struct
    1.47  
    1.48 +
    1.49 +(* path elements *)
    1.50 +
    1.51 +datatype elem = Root | Parent | Basic of string | Variable of string;
    1.52 +
    1.53 +fun no_meta_chars chs =
    1.54 +  (case ["/", "\\", "$", "~"] inter_string chs of
    1.55 +    [] => chs
    1.56 +  | bads => error ("Illegal character(s) " ^ commas_quote bads ^
    1.57 +      " in path element specification: " ^ quote (implode chs)));
    1.58 +
    1.59 +val basic_elem = Basic o implode o no_meta_chars;
    1.60 +val variable_elem = Variable o implode o no_meta_chars;
    1.61 +
    1.62 +fun is_var (Variable _) = true
    1.63 +  | is_var _ = false;
    1.64 +
    1.65 +
    1.66  (* type path *)
    1.67  
    1.68 -datatype T = Path of string list;
    1.69 +datatype T = Path of elem list;
    1.70 +
    1.71 +fun rep (Path xs) = xs;
    1.72  
    1.73  val current = Path [];
    1.74 -val parent = Path [".."];
    1.75 -val root = Path ["/"];
    1.76 -
    1.77 -fun absolute (Path ("/" :: _)) = true
    1.78 -  | absolute _ = false;
    1.79 +val root = Path [Root];
    1.80 +val parent = Path [Parent];
    1.81 +fun basic s = Path [basic_elem (explode s)];
    1.82 +fun variable s = Path [variable_elem (explode s)];
    1.83  
    1.84 -fun base (Path []) = ""
    1.85 -  | base (Path ["/"]) = ""
    1.86 -  | base (Path xs) = snd (split_last xs);
    1.87 +fun is_absolute (Path (Root :: _)) = true
    1.88 +  | is_absolute _ = false;
    1.89  
    1.90 -fun variable name = Path ["$" ^ name];
    1.91 -fun is_variable elem = ord elem = ord "$";
    1.92 +fun is_basic (Path [Basic _]) = true
    1.93 +  | is_basic _ = false;
    1.94  
    1.95  
    1.96  (* append and norm *)
    1.97  
    1.98  (*append non-normal path (2n arg) to reversed normal one, result is normal*)
    1.99  fun rev_app xs [] = rev xs
   1.100 -  | rev_app _ ("/" :: ys) = rev_app ["/"] ys
   1.101 -  | rev_app xs ("." :: ys) = rev_app xs ys
   1.102 -  | rev_app (x :: xs) (".." :: ys) =
   1.103 -      if x = ".." orelse is_variable x then rev_app (".." :: x :: xs) ys
   1.104 -      else if x = "/" then rev_app (x :: xs) ys
   1.105 +  | rev_app _ (Root :: ys) = rev_app [Root] ys
   1.106 +  | rev_app (x :: xs) (Parent :: ys) =
   1.107 +      if x = Parent orelse is_var x then rev_app (Parent :: x :: xs) ys
   1.108 +      else if x = Root then rev_app (x :: xs) ys
   1.109        else rev_app xs ys
   1.110    | rev_app xs (y :: ys) = rev_app (y :: xs) ys;
   1.111  
   1.112 +fun append (Path xs) (Path ys) = Path (rev_app (rev xs) ys);
   1.113  fun norm path = rev_app [] path;
   1.114  
   1.115 -fun append (Path xs) (Path ys) = Path (rev_app (rev xs) ys);
   1.116 +
   1.117 +(* pack *)
   1.118  
   1.119 -
   1.120 -(* pack and unpack *)
   1.121 +fun pack_elem Root = ""
   1.122 +  | pack_elem Parent = ".."
   1.123 +  | pack_elem (Basic s) = s
   1.124 +  | pack_elem (Variable s) = "$" ^ s;
   1.125  
   1.126  fun pack (Path []) = "."
   1.127 -  | pack (Path ("/" :: xs)) = "/" ^ space_implode "/" xs
   1.128 -  | pack (Path xs) = space_implode "/" xs;
   1.129 -
   1.130 -fun unpack str =
   1.131 -  (case space_explode "/" str of
   1.132 -    [""] => []
   1.133 -  | "" :: xs => "/" :: filter (not_equal "") xs
   1.134 -  | xs => filter (not_equal "") xs)
   1.135 -    |> map (fn "~" => "$HOME" | x => x)
   1.136 -    |> norm
   1.137 -    |> Path;
   1.138 +  | pack (Path (Root :: xs)) = "/" ^ space_implode "/" (map pack_elem xs)
   1.139 +  | pack (Path xs) = space_implode "/" (map pack_elem xs);
   1.140  
   1.141  
   1.142 -(* eval variables *)
   1.143 +(* unpack *)
   1.144 +
   1.145 +fun unpack_elem "" = Root
   1.146 +  | unpack_elem ".." = Parent
   1.147 +  | unpack_elem "~" = Variable "HOME"
   1.148 +  | unpack_elem "~~" = Variable "ISABELLE_HOME"
   1.149 +  | unpack_elem s =
   1.150 +      (case explode s of
   1.151 +        "$" :: cs => variable_elem cs
   1.152 +      | cs => basic_elem cs);
   1.153 +
   1.154 +val unpack_elems = map unpack_elem o filter_out (equal "" orf equal ".");
   1.155 +
   1.156 +fun unpack str = Path (norm
   1.157 +  (case space_explode "/" str of
   1.158 +    "" :: ss => Root :: unpack_elems ss
   1.159 +  | ss => unpack_elems ss));
   1.160 +
   1.161  
   1.162 -fun eval env x =
   1.163 -  if is_variable x then
   1.164 -    let val Path ys = env (implode (tl (explode x)))
   1.165 -    in ys end
   1.166 -  else [x];
   1.167 +(* base element *)
   1.168 +
   1.169 +fun err_no_base path =
   1.170 +  error ("No base path element in " ^ quote (pack path));
   1.171 +
   1.172 +fun base (path as Path xs) =
   1.173 +  (case try split_last xs of
   1.174 +    Some (_, x as Basic _) => Path [x]
   1.175 +  | _ => err_no_base path);
   1.176 +
   1.177 +fun ext e (path as Path xs) =
   1.178 +  (case try split_last xs of
   1.179 +    Some (prfx, Basic s) => if e = "" then path else Path (prfx @ [Basic (s ^ "." ^ e)])
   1.180 +  | _ => err_no_base path);
   1.181 +
   1.182 +
   1.183 +(* evaluate variables *)
   1.184 +
   1.185 +fun eval env (Variable s) = rep (env s)
   1.186 +  | eval _ x = [x];
   1.187  
   1.188  fun evaluate env (Path xs) =
   1.189    Path (norm (flat (map (eval env) xs)));
   1.190  
   1.191 -
   1.192 -(* operations on packed paths *)
   1.193 -
   1.194 -fun expand env str =
   1.195 -  pack (evaluate (unpack o env) (unpack str));
   1.196 -
   1.197 -val base_name = base o unpack;
   1.198 -
   1.199 -fun is_base str =
   1.200 -  not (exists (equal "/" orf equal "$") (explode str));
   1.201 +val expand = evaluate (unpack o getenv);
   1.202  
   1.203  
   1.204  end;