~/bend-docscommunity

LAWS.bend open laws/TODOs

raw source on the hub · import 0x4c13780015689c83e56d725a171fc6e9/LAWS.bend as LAWS

2 imports
import Base
import ./lib.bend as U

Laws

law make_show provedin PROOF.bendsource · line 5 · raw

{0x4c13780015689c83e56d725a171fc6e9/lib.Url.to_string(0x4c13780015689c83e56d725a171fc6e9/lib.Url{"http", "example.com", "/a", "x=1"}) == "http://example.com/a?x=1" : String}

Construction and rendering.

law build_alias provedin PROOF.bendsource · line 9 · raw

{0x4c13780015689c83e56d725a171fc6e9/lib.Url.build(0x4c13780015689c83e56d725a171fc6e9/lib.Url{"https", "example.com", "", ""}) == "https://example.com" : String}

law show_alias provedin PROOF.bendsource · line 13 · raw

{0x4c13780015689c83e56d725a171fc6e9/lib.Url.show(0x4c13780015689c83e56d725a171fc6e9/lib.Url{"https", "example.com", "/", "q"}) == "https://example.com/?q" : String}

law parse_http provedin PROOF.bendsource · line 18 · raw

{0x4c13780015689c83e56d725a171fc6e9/lib.Url.parse("http://example.com") == Some{0x4c13780015689c83e56d725a171fc6e9/lib.Url{"http", "example.com", "", ""}} : Maybe<&2, 0x4c13780015689c83e56d725a171fc6e9/lib.Url>}

Accepted absolute forms.

law parse_https_path_query provedin PROOF.bendsource · line 23 · raw

{0x4c13780015689c83e56d725a171fc6e9/lib.Url.parse("https://example.com/a/b?x=1") == Some{0x4c13780015689c83e56d725a171fc6e9/lib.Url{"https", "example.com", "/a/b", "x=1"}} : Maybe<&2, 0x4c13780015689c83e56d725a171fc6e9/lib.Url>}

law parse_empty_path_query provedin PROOF.bendsource · line 28 · raw

{0x4c13780015689c83e56d725a171fc6e9/lib.Url.parse("http://example.com?x") == Some{0x4c13780015689c83e56d725a171fc6e9/lib.Url{"http", "example.com", "", "x"}} : Maybe<&2, 0x4c13780015689c83e56d725a171fc6e9/lib.Url>}

law parse_trailing_slash provedin PROOF.bendsource · line 33 · raw

{0x4c13780015689c83e56d725a171fc6e9/lib.Url.parse("http://example.com/") == Some{0x4c13780015689c83e56d725a171fc6e9/lib.Url{"http", "example.com", "/", ""}} : Maybe<&2, 0x4c13780015689c83e56d725a171fc6e9/lib.Url>}

law parse_repeated_path_slash provedin PROOF.bendsource · line 38 · raw

{0x4c13780015689c83e56d725a171fc6e9/lib.Url.parse("http://example.com/a//b") == Some{0x4c13780015689c83e56d725a171fc6e9/lib.Url{"http", "example.com", "/a//b", ""}} : Maybe<&2, 0x4c13780015689c83e56d725a171fc6e9/lib.Url>}

law parse_roundtrip provedin PROOF.bendsource · line 43 · raw

{0x4c13780015689c83e56d725a171fc6e9/lib.Url.parse(0x4c13780015689c83e56d725a171fc6e9/lib.Url.to_string(0x4c13780015689c83e56d725a171fc6e9/lib.Url{"https", "host", "/p", "a=b"})) == Some{0x4c13780015689c83e56d725a171fc6e9/lib.Url{"https", "host", "/p", "a=b"}} : Maybe<&2, 0x4c13780015689c83e56d725a171fc6e9/lib.Url>}

law reject_relative provedin PROOF.bendsource · line 49 · raw

{0x4c13780015689c83e56d725a171fc6e9/lib.Url.parse("/relative/path") == None{} : Maybe<&2, 0x4c13780015689c83e56d725a171fc6e9/lib.Url>}

Rejected forms outside the v1 grammar.

law reject_wrong_scheme provedin PROOF.bendsource · line 52 · raw

{0x4c13780015689c83e56d725a171fc6e9/lib.Url.parse("ftp://example.com") == None{} : Maybe<&2, 0x4c13780015689c83e56d725a171fc6e9/lib.Url>}

law reject_upper_scheme provedin PROOF.bendsource · line 55 · raw

{0x4c13780015689c83e56d725a171fc6e9/lib.Url.parse("HTTP://example.com") == None{} : Maybe<&2, 0x4c13780015689c83e56d725a171fc6e9/lib.Url>}

law reject_empty_host provedin PROOF.bendsource · line 58 · raw

{0x4c13780015689c83e56d725a171fc6e9/lib.Url.parse("http:///path") == None{} : Maybe<&2, 0x4c13780015689c83e56d725a171fc6e9/lib.Url>}

law reject_userinfo provedin PROOF.bendsource · line 61 · raw

{0x4c13780015689c83e56d725a171fc6e9/lib.Url.parse("http://user@example.com/") == None{} : Maybe<&2, 0x4c13780015689c83e56d725a171fc6e9/lib.Url>}

law reject_fragment provedin PROOF.bendsource · line 64 · raw

{0x4c13780015689c83e56d725a171fc6e9/lib.Url.parse("http://example.com/p#part") == None{} : Maybe<&2, 0x4c13780015689c83e56d725a171fc6e9/lib.Url>}

law reject_second_query provedin PROOF.bendsource · line 67 · raw

{0x4c13780015689c83e56d725a171fc6e9/lib.Url.parse("http://example.com/p?a?b") == None{} : Maybe<&2, 0x4c13780015689c83e56d725a171fc6e9/lib.Url>}

law join_empty_path provedin PROOF.bendsource · line 71 · raw

{0x4c13780015689c83e56d725a171fc6e9/lib.Url.to_string(0x4c13780015689c83e56d725a171fc6e9/lib.Url.join_path(0x4c13780015689c83e56d725a171fc6e9/lib.Url{"https", "example.com", "", ""}, "api")) == "https://example.com/api" : String}

Relative path joining.

law join_nested_path provedin PROOF.bendsource · line 76 · raw

{0x4c13780015689c83e56d725a171fc6e9/lib.Url.to_string(0x4c13780015689c83e56d725a171fc6e9/lib.Url.join_path(0x4c13780015689c83e56d725a171fc6e9/lib.Url{"https", "example.com", "/api", "q"}, "v1")) == "https://example.com/api/v1?q" : String}

law join_trailing_slash provedin PROOF.bendsource · line 81 · raw

{0x4c13780015689c83e56d725a171fc6e9/lib.Url.to_string(0x4c13780015689c83e56d725a171fc6e9/lib.Url.join_path(0x4c13780015689c83e56d725a171fc6e9/lib.Url{"http", "example.com", "/api/", ""}, "v1")) == "http://example.com/api/v1" : String}

law join_empty_segment provedin PROOF.bendsource · line 86 · raw

{0x4c13780015689c83e56d725a171fc6e9/lib.Url.join_path(0x4c13780015689c83e56d725a171fc6e9/lib.Url{"http", "example.com", "/api", "q"}, "") == 0x4c13780015689c83e56d725a171fc6e9/lib.Url{"http", "example.com", "/api", "q"} : 0x4c13780015689c83e56d725a171fc6e9/lib.Url}

law join_preserves_query provedin PROOF.bendsource · line 91 · raw

{0x4c13780015689c83e56d725a171fc6e9/lib.Url.join_path(0x4c13780015689c83e56d725a171fc6e9/lib.Url{"http", "example.com", "", "a=1"}, "next") == 0x4c13780015689c83e56d725a171fc6e9/lib.Url{"http", "example.com", "/next", "a=1"} : 0x4c13780015689c83e56d725a171fc6e9/lib.Url}