moved Thy/path.ML to General/path.ML;
authorwenzelm
Wed Jun 10 11:51:28 1998 +0200 (1998-06-10)
changeset 501137c253fd3dc6
parent 5010 9101b70b696d
child 5012 086b055c4d73
moved Thy/path.ML to General/path.ML;
src/Pure/General/path.ML
src/Pure/Thy/path.ML
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/General/path.ML	Wed Jun 10 11:51:28 1998 +0200
     1.3 @@ -0,0 +1,104 @@
     1.4 +(*  Title:      Pure/Thy/path.ML
     1.5 +    ID:         $Id$
     1.6 +    Author:     Markus Wenzel, TU Muenchen
     1.7 +
     1.8 +Abstract algebra of file paths.  External representation Unix-style.
     1.9 +*)
    1.10 +
    1.11 +signature PATH =
    1.12 +sig
    1.13 +  type T
    1.14 +  val pack: T -> string
    1.15 +  val unpack: string -> T
    1.16 +  val current: T
    1.17 +  val parent: T
    1.18 +  val root: T
    1.19 +  val variable: string -> T
    1.20 +  val absolute: T -> bool
    1.21 +  val base: T -> string
    1.22 +  val append: T -> T -> T
    1.23 +  val evaluate: (string -> T) -> T -> T
    1.24 +  val expand: (string -> string) -> string -> string
    1.25 +  val base_name: string -> string
    1.26 +  val is_base: string -> bool
    1.27 +end;
    1.28 +
    1.29 +structure Path: PATH =
    1.30 +struct
    1.31 +
    1.32 +(* type path *)
    1.33 +
    1.34 +datatype T = Path of string list;
    1.35 +
    1.36 +val current = Path [];
    1.37 +val parent = Path [".."];
    1.38 +val root = Path ["/"];
    1.39 +
    1.40 +fun absolute (Path ("/" :: _)) = true
    1.41 +  | absolute _ = false;
    1.42 +
    1.43 +fun base (Path []) = ""
    1.44 +  | base (Path ["/"]) = ""
    1.45 +  | base (Path xs) = snd (split_last xs);
    1.46 +
    1.47 +fun variable name = Path ["$" ^ name];
    1.48 +fun is_variable elem = ord elem = ord "$";
    1.49 +
    1.50 +
    1.51 +(* append and norm *)
    1.52 +
    1.53 +(*append non-normal path (2n arg) to reversed normal one, result is normal*)
    1.54 +fun rev_app xs [] = rev xs
    1.55 +  | rev_app _ ("/" :: ys) = rev_app ["/"] ys
    1.56 +  | rev_app xs ("." :: ys) = rev_app xs ys
    1.57 +  | rev_app (x :: xs) (".." :: ys) =
    1.58 +      if x = ".." orelse is_variable x then rev_app (".." :: x :: xs) ys
    1.59 +      else if x = "/" then rev_app (x :: xs) ys
    1.60 +      else rev_app xs ys
    1.61 +  | rev_app xs (y :: ys) = rev_app (y :: xs) ys;
    1.62 +
    1.63 +fun norm path = rev_app [] path;
    1.64 +
    1.65 +fun append (Path xs) (Path ys) = Path (rev_app (rev xs) ys);
    1.66 +
    1.67 +
    1.68 +(* pack and unpack *)
    1.69 +
    1.70 +fun pack (Path []) = "."
    1.71 +  | pack (Path ("/" :: xs)) = "/" ^ space_implode "/" xs
    1.72 +  | pack (Path xs) = space_implode "/" xs;
    1.73 +
    1.74 +fun unpack str =
    1.75 +  (case space_explode "/" str of
    1.76 +    [""] => []
    1.77 +  | "" :: xs => "/" :: filter (not_equal "") xs
    1.78 +  | xs => filter (not_equal "") xs)
    1.79 +    |> map (fn "~" => "$HOME" | x => x)
    1.80 +    |> norm
    1.81 +    |> Path;
    1.82 +
    1.83 +
    1.84 +(* eval variables *)
    1.85 +
    1.86 +fun eval env x =
    1.87 +  if is_variable x then
    1.88 +    let val Path ys = env (implode (tl (explode x)))
    1.89 +    in ys end
    1.90 +  else [x];
    1.91 +
    1.92 +fun evaluate env (Path xs) =
    1.93 +  Path (norm (flat (map (eval env) xs)));
    1.94 +
    1.95 +
    1.96 +(* operations on packed paths *)
    1.97 +
    1.98 +fun expand env str =
    1.99 +  pack (evaluate (unpack o env) (unpack str));
   1.100 +
   1.101 +val base_name = base o unpack;
   1.102 +
   1.103 +fun is_base str =
   1.104 +  not (exists (equal "/" orf equal "$") (explode str));
   1.105 +
   1.106 +
   1.107 +end;
     2.1 --- a/src/Pure/Thy/path.ML	Wed Jun 10 11:50:52 1998 +0200
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,104 +0,0 @@
     2.4 -(*  Title:      Pure/Thy/path.ML
     2.5 -    ID:         $Id$
     2.6 -    Author:     Markus Wenzel, TU Muenchen
     2.7 -
     2.8 -Abstract algebra of file paths.  External representation Unix-style.
     2.9 -*)
    2.10 -
    2.11 -signature PATH =
    2.12 -sig
    2.13 -  type T
    2.14 -  val pack: T -> string
    2.15 -  val unpack: string -> T
    2.16 -  val current: T
    2.17 -  val parent: T
    2.18 -  val root: T
    2.19 -  val variable: string -> T
    2.20 -  val absolute: T -> bool
    2.21 -  val base: T -> string
    2.22 -  val append: T -> T -> T
    2.23 -  val evaluate: (string -> T) -> T -> T
    2.24 -  val expand: (string -> string) -> string -> string
    2.25 -  val base_name: string -> string
    2.26 -  val is_base: string -> bool
    2.27 -end;
    2.28 -
    2.29 -structure Path: PATH =
    2.30 -struct
    2.31 -
    2.32 -(* type path *)
    2.33 -
    2.34 -datatype T = Path of string list;
    2.35 -
    2.36 -val current = Path [];
    2.37 -val parent = Path [".."];
    2.38 -val root = Path ["/"];
    2.39 -
    2.40 -fun absolute (Path ("/" :: _)) = true
    2.41 -  | absolute _ = false;
    2.42 -
    2.43 -fun base (Path []) = ""
    2.44 -  | base (Path ["/"]) = ""
    2.45 -  | base (Path xs) = snd (split_last xs);
    2.46 -
    2.47 -fun variable name = Path ["$" ^ name];
    2.48 -fun is_variable elem = ord elem = ord "$";
    2.49 -
    2.50 -
    2.51 -(* append and norm *)
    2.52 -
    2.53 -(*append non-normal path (2n arg) to reversed normal one, result is normal*)
    2.54 -fun rev_app xs [] = rev xs
    2.55 -  | rev_app _ ("/" :: ys) = rev_app ["/"] ys
    2.56 -  | rev_app xs ("." :: ys) = rev_app xs ys
    2.57 -  | rev_app (x :: xs) (".." :: ys) =
    2.58 -      if x = ".." orelse is_variable x then rev_app (".." :: x :: xs) ys
    2.59 -      else if x = "/" then rev_app (x :: xs) ys
    2.60 -      else rev_app xs ys
    2.61 -  | rev_app xs (y :: ys) = rev_app (y :: xs) ys;
    2.62 -
    2.63 -fun norm path = rev_app [] path;
    2.64 -
    2.65 -fun append (Path xs) (Path ys) = Path (rev_app (rev xs) ys);
    2.66 -
    2.67 -
    2.68 -(* pack and unpack *)
    2.69 -
    2.70 -fun pack (Path []) = "."
    2.71 -  | pack (Path ("/" :: xs)) = "/" ^ space_implode "/" xs
    2.72 -  | pack (Path xs) = space_implode "/" xs;
    2.73 -
    2.74 -fun unpack str =
    2.75 -  (case space_explode "/" str of
    2.76 -    [""] => []
    2.77 -  | "" :: xs => "/" :: filter (not_equal "") xs
    2.78 -  | xs => filter (not_equal "") xs)
    2.79 -    |> map (fn "~" => "$HOME" | x => x)
    2.80 -    |> norm
    2.81 -    |> Path;
    2.82 -
    2.83 -
    2.84 -(* eval variables *)
    2.85 -
    2.86 -fun eval env x =
    2.87 -  if is_variable x then
    2.88 -    let val Path ys = env (implode (tl (explode x)))
    2.89 -    in ys end
    2.90 -  else [x];
    2.91 -
    2.92 -fun evaluate env (Path xs) =
    2.93 -  Path (norm (flat (map (eval env) xs)));
    2.94 -
    2.95 -
    2.96 -(* operations on packed paths *)
    2.97 -
    2.98 -fun expand env str =
    2.99 -  pack (evaluate (unpack o env) (unpack str));
   2.100 -
   2.101 -val base_name = base o unpack;
   2.102 -
   2.103 -fun is_base str =
   2.104 -  not (exists (equal "/" orf equal "$") (explode str));
   2.105 -
   2.106 -
   2.107 -end;