# HG changeset patch
# User wenzelm
# Date 878643231 -3600
# Node ID f7130dcacefae83a2e4fc27e0df323e8b3d79f21
# Parent  98c8f40f7bbee586cb8bf9be1680bb43e6eb3c03
Abstract algebra of file paths.  External representation Unix-style.

diff -r 98c8f40f7bbe -r f7130dcacefa src/Pure/Thy/path.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Thy/path.ML	Tue Nov 04 12:33:51 1997 +0100
@@ -0,0 +1,68 @@
+(*  Title:      Pure/Thy/path.ML
+    ID:         $Id$
+    Author:     Markus Wenzel, TU Muenchen
+
+Abstract algebra of file paths.  External representation Unix-style.
+
+TODO:
+  - support variables and  eval:(string->T)->T->T (!?)
+*)
+
+signature PATH =
+sig
+  type T
+  val pack: T -> string
+  val unpack: string -> T
+  val current: T
+  val parent: T
+  val root: T
+  val absolute: T -> bool
+  val append: T -> T -> T
+end;
+
+structure Path: PATH =
+struct
+
+(* type path *)
+
+datatype T = Path of string list;
+
+val current = Path [];
+val parent = Path [".."];
+val root = Path [""];
+
+fun absolute (Path ("" :: _)) = true
+  | absolute _ = false;
+
+
+(* append and norm *)
+
+(*append non-normal path (2n arg) to reversed normal one, result is normal*)
+fun rev_app xs [] = rev xs
+  | rev_app _ ("" :: ys) = rev_app [""] ys
+  | rev_app xs ("." :: ys) = rev_app xs ys
+  | rev_app [] (".." :: ys) = rev_app [".."] ys
+  | rev_app (xs as ".." :: _) (".." :: ys) = rev_app (".." :: xs) ys
+  | rev_app (xs as "" :: _) (".." :: ys) = rev_app xs ys
+  | rev_app (_ :: xs) (".." :: ys) = rev_app xs ys
+  | rev_app xs (y :: ys) = rev_app (y :: xs) ys;
+
+fun norm path = rev_app [] path;
+fun append (Path xs) (Path ys) = Path (rev_app (rev xs) ys);
+
+
+(* pack and unpack *)
+
+fun pack (Path []) = "."
+  | pack (path as Path xs) =
+      (if absolute path then "/" else "") ^ space_implode "/" xs;
+
+fun unpack str =
+  Path (norm
+    (case space_explode "/" str of
+      [""] => []
+    | "" :: xs => "" :: filter (not_equal "") xs
+    | xs => filter (not_equal "") xs));
+
+
+end;