SSL pathname.pvs

pathname : THEORY
BEGIN

  pathname_path(name:string) : list[string]

  pathname_name(name:string) : string
 
  pathname_type(name:string) :string

  pathname_dir(name:string) : string =
    LET path = pathname_path(name) IN
    IF null?(path) THEN ""
    ELSIF car(path) = "/" THEN
      format("/~{~a/~}",{|cdr(path)|})
    ELSE
      format("~{~a/~}",{|path|})
    ENDIF

END pathname