wenzelm@6118: (* Title: Pure/General/path.ML wenzelm@5011: ID: $Id$ wenzelm@5011: Author: Markus Wenzel, TU Muenchen wenzelm@5011: wenzelm@5011: Abstract algebra of file paths. External representation Unix-style. wenzelm@5011: *) wenzelm@5011: wenzelm@5011: signature PATH = wenzelm@5011: sig wenzelm@5011: type T wenzelm@5011: val pack: T -> string wenzelm@5011: val unpack: string -> T wenzelm@5011: val current: T wenzelm@5011: val parent: T wenzelm@5011: val root: T wenzelm@5011: val variable: string -> T wenzelm@5011: val absolute: T -> bool wenzelm@5011: val base: T -> string wenzelm@5011: val append: T -> T -> T wenzelm@5011: val evaluate: (string -> T) -> T -> T wenzelm@5011: val expand: (string -> string) -> string -> string wenzelm@5011: val base_name: string -> string wenzelm@5011: val is_base: string -> bool wenzelm@5011: end; wenzelm@5011: wenzelm@5011: structure Path: PATH = wenzelm@5011: struct wenzelm@5011: wenzelm@5011: (* type path *) wenzelm@5011: wenzelm@5011: datatype T = Path of string list; wenzelm@5011: wenzelm@5011: val current = Path []; wenzelm@5011: val parent = Path [".."]; wenzelm@5011: val root = Path ["/"]; wenzelm@5011: wenzelm@5011: fun absolute (Path ("/" :: _)) = true wenzelm@5011: | absolute _ = false; wenzelm@5011: wenzelm@5011: fun base (Path []) = "" wenzelm@5011: | base (Path ["/"]) = "" wenzelm@5011: | base (Path xs) = snd (split_last xs); wenzelm@5011: wenzelm@5011: fun variable name = Path ["$" ^ name]; wenzelm@5011: fun is_variable elem = ord elem = ord "$"; wenzelm@5011: wenzelm@5011: wenzelm@5011: (* append and norm *) wenzelm@5011: wenzelm@5011: (*append non-normal path (2n arg) to reversed normal one, result is normal*) wenzelm@5011: fun rev_app xs [] = rev xs wenzelm@5011: | rev_app _ ("/" :: ys) = rev_app ["/"] ys wenzelm@5011: | rev_app xs ("." :: ys) = rev_app xs ys wenzelm@5011: | rev_app (x :: xs) (".." :: ys) = wenzelm@5011: if x = ".." orelse is_variable x then rev_app (".." :: x :: xs) ys wenzelm@5011: else if x = "/" then rev_app (x :: xs) ys wenzelm@5011: else rev_app xs ys wenzelm@5011: | rev_app xs (y :: ys) = rev_app (y :: xs) ys; wenzelm@5011: wenzelm@5011: fun norm path = rev_app [] path; wenzelm@5011: wenzelm@5011: fun append (Path xs) (Path ys) = Path (rev_app (rev xs) ys); wenzelm@5011: wenzelm@5011: wenzelm@5011: (* pack and unpack *) wenzelm@5011: wenzelm@5011: fun pack (Path []) = "." wenzelm@5011: | pack (Path ("/" :: xs)) = "/" ^ space_implode "/" xs wenzelm@5011: | pack (Path xs) = space_implode "/" xs; wenzelm@5011: wenzelm@5011: fun unpack str = wenzelm@5011: (case space_explode "/" str of wenzelm@5011: [""] => [] wenzelm@5011: | "" :: xs => "/" :: filter (not_equal "") xs wenzelm@5011: | xs => filter (not_equal "") xs) wenzelm@5011: |> map (fn "~" => "$HOME" | x => x) wenzelm@5011: |> norm wenzelm@5011: |> Path; wenzelm@5011: wenzelm@5011: wenzelm@5011: (* eval variables *) wenzelm@5011: wenzelm@5011: fun eval env x = wenzelm@5011: if is_variable x then wenzelm@5011: let val Path ys = env (implode (tl (explode x))) wenzelm@5011: in ys end wenzelm@5011: else [x]; wenzelm@5011: wenzelm@5011: fun evaluate env (Path xs) = wenzelm@5011: Path (norm (flat (map (eval env) xs))); wenzelm@5011: wenzelm@5011: wenzelm@5011: (* operations on packed paths *) wenzelm@5011: wenzelm@5011: fun expand env str = wenzelm@5011: pack (evaluate (unpack o env) (unpack str)); wenzelm@5011: wenzelm@5011: val base_name = base o unpack; wenzelm@5011: wenzelm@5011: fun is_base str = wenzelm@5011: not (exists (equal "/" orf equal "$") (explode str)); wenzelm@5011: wenzelm@5011: wenzelm@5011: end;