import Base
import ./lib.bend as P

law normalize_empty:
  { P.Path.normalize("") == "" : String }

law normalize_absolute_root:
  { P.Path.normalize("///") == "/" : String }

law normalize_collapses_slashes:
  { P.Path.normalize("/a//b/") == "/a/b" : String }

law normalize_relative:
  { P.Path.normalize("a///b") == "a/b" : String }

law normalize_keeps_dot_components:
  { P.Path.normalize("a/./b") == "a/./b" : String }

law is_absolute_root:
  { P.Path.is_absolute("/tmp") == True{} : Bool }

law is_absolute_relative:
  { P.Path.is_absolute("tmp") == False{} : Bool }

law segments_drop_empty:
  {
    P.Path.segments("/a//b/") == "a" <> "b" <> Nil{}
    : List<&2, String>
  }

law split_is_segments:
  {
    P.Path.split("a/b") == "a" <> "b" <> Nil{}
    : List<&2, String>
  }

law join_relative:
  { P.Path.join("a", "b") == "a/b" : String }

law join_absolute_second:
  { P.Path.join("a", "/b") == "/b" : String }

law join_all_segments:
  {
    P.Path.join_all("a" <> "b" <> "c" <> Nil{}) == "a/b/c"
    : String
  }

law basename_nested:
  { P.Path.basename("/usr//local/bin/") == "bin" : String }

law basename_root:
  { P.Path.basename("/") == "" : String }

law dirname_nested:
  { P.Path.dirname("/usr//local/bin/") == "/usr/local" : String }

law dirname_single:
  { P.Path.dirname("bin") == "." : String }

law dirname_root:
  { P.Path.dirname("/") == "/" : String }

law extension_simple:
  { P.Path.extension("archive.tar.gz") == ".gz" : String }

law extension_hidden:
  { P.Path.extension(".profile") == "" : String }

law extension_hidden_with_suffix:
  { P.Path.extension(".profile.bak") == ".bak" : String }

law extension_none:
  { P.Path.extension("README") == "" : String }

law is_absolute_empty:
  { P.Path.is_absolute("") == False{} : Bool }

law is_absolute_slash:
  { P.Path.is_absolute("/") == True{} : Bool }

law segments_empty:
  { P.Path.segments("") == Nil{} : List<&2, String> }

law segments_single:
  { P.Path.segments("foo") == "foo" <> Nil{} : List<&2, String> }

law join_empty_empty:
  { P.Path.join("", "") == "" : String }

law join_empty_rel:
  { P.Path.join("", "a/b") == "a/b" : String }

law join_all_nil:
  { P.Path.join_all(Nil{}) == "" : String }

law join_all_one:
  { P.Path.join_all("a" <> Nil{}) == "a" : String }

law normalize_idempotent_simple:
  { P.Path.normalize(P.Path.normalize("/a//b/")) == "/a/b" : String }

law basename_file:
  { P.Path.basename("dir/file.txt") == "file.txt" : String }

law dirname_file:
  { P.Path.dirname("dir/file.txt") == "dir" : String }

law extension_txt:
  { P.Path.extension("file.txt") == ".txt" : String }

law split_eq_segments_abs:
  {
    P.Path.split("/a/b") == P.Path.segments("/a/b")
    : List<&2, String>
  }