~/bend-docscommunity

LAWS.bend open laws/TODOs

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

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

Laws

law pure_id provedin PROOF.bendsource · line 5 · raw

@-A:Type -> @x:A -> @s:String -> {0xdf88d6b259873c74c8d91fe09934de63/lib.Parse.pure(A, x, s) == Some{(x, s)} : Maybe<&1, Pair(A, String)>}

pure places x and leaves the input untouched.

law fail_none provedin PROOF.bendsource · line 12 · raw

@-A:Type -> @s:String -> {0xdf88d6b259873c74c8d91fe09934de63/lib.Parse.fail(A, s) == None{} : Maybe<&1, Pair(A, String)>}

fail always returns None.

law map_id_pure provedin PROOF.bendsource · line 18 · raw

@s:String -> {0xdf88d6b259873c74c8d91fe09934de63/lib.Parse.map(U32, U32, x => x, 0xdf88d6b259873c74c8d91fe09934de63/lib.Parse.pure(U32, 7, s)) == Some{(7, s)} : Maybe<&1, Pair(U32, String)>}

map id on a concrete pure result (definitional).

law or_fail_left_char provedin PROOF.bendsource · line 27 · raw

@+c:Char -> @+s:String -> {0xdf88d6b259873c74c8d91fe09934de63/lib.Parse.or(Char, 0xdf88d6b259873c74c8d91fe09934de63/lib.Parse.fail(Char), 0xdf88d6b259873c74c8d91fe09934de63/lib.Parse.char(c), s) == 0xdf88d6b259873c74c8d91fe09934de63/lib.Parse.char(c, s) : Maybe<&1, Pair(Char, String)>}

or(fail, char) degenerates to char on the same input.

law or_fail_right_char_hit provedin PROOF.bendsource · line 37 · raw

{0xdf88d6b259873c74c8d91fe09934de63/lib.Parse.or(Char, 0xdf88d6b259873c74c8d91fe09934de63/lib.Parse.char('a'), 0xdf88d6b259873c74c8d91fe09934de63/lib.Parse.fail(Char), "a") == Some{('a', "")} : Maybe<&1, Pair(Char, String)>}

or(char, fail) keeps a hit on a matching singleton (concrete char).

law char_match provedin PROOF.bendsource · line 45 · raw

@t:String -> {0xdf88d6b259873c74c8d91fe09934de63/lib.Parse.char('a', SCon{'a', t}) == Some{('a', t)} : Maybe<&1, Pair(Char, String)>}

char matches the head and returns the tail (concrete char; is_eq needs it).

law char_fail_empty provedin PROOF.bendsource · line 50 · raw

@+c:Char -> {0xdf88d6b259873c74c8d91fe09934de63/lib.Parse.char(c, "") == None{} : Maybe<&1, Pair(Char, String)>}

char fails on empty input.

law char_fail_mismatch provedin PROOF.bendsource · line 55 · raw

{0xdf88d6b259873c74c8d91fe09934de63/lib.Parse.char('a', "b") == None{} : Maybe<&1, Pair(Char, String)>}

char fails when the head differs (concrete distinct chars).

law string_empty provedin PROOF.bendsource · line 62 · raw

@s:String -> {0xdf88d6b259873c74c8d91fe09934de63/lib.Parse.string("", s) == Some{("", s)} : Maybe<&1, Pair(String, String)>}

string literal: empty pattern always matches (case-split on s in the proof).

law map_fail provedin PROOF.bendsource · line 67 · raw

@s:String -> {0xdf88d6b259873c74c8d91fe09934de63/lib.Parse.map(U32, U32, x => x, 0xdf88d6b259873c74c8d91fe09934de63/lib.Parse.fail(U32, s)) == None{} : Maybe<&1, Pair(U32, String)>}

map over fail is None.

law string_lit_hit provedin PROOF.bendsource · line 76 · raw

{0xdf88d6b259873c74c8d91fe09934de63/lib.Parse.string("a", "ab") == Some{("a", "b")} : Maybe<&1, Pair(String, String)>}

string literal hit consumes the prefix.

law string_lit_miss provedin PROOF.bendsource · line 84 · raw

{0xdf88d6b259873c74c8d91fe09934de63/lib.Parse.string("a", "b") == None{} : Maybe<&1, Pair(String, String)>}

string literal miss fails.