LAWS.bend source

LAWS.bend on the hub · documented module

import Baseimport ./lib.bend as P# pure places x and leaves the input untouched.law pure_id:  for -A: Type  for x: A  for s: String  { P.Parse.pure(A, x, s) == Some{(x, s)} : Maybe<&1, A & String> }# fail always returns None.law fail_none:  for -A: Type  for s: String  { P.Parse.fail(A, s) == None{} : Maybe<&1, A & String> }# map id on a concrete pure result (definitional).law map_id_pure:  for s: String  {    P.Parse.map(U32, U32, (x => x), P.Parse.pure(U32, 7, s))      == Some{(7, s)}    : Maybe<&1, U32 & String>  }# or(fail, char) degenerates to char on the same input.law or_fail_left_char:  for +c: Char  for +s: String  {    P.Parse.or(Char, P.Parse.fail(Char), P.Parse.char(c), s)      == P.Parse.char(c, s)    : Maybe<&1, Char & String>  }# or(char, fail) keeps a hit on a matching singleton (concrete char).law or_fail_right_char_hit:  {    P.Parse.or(Char, P.Parse.char('a'), P.Parse.fail(Char), SCon{'a', SNil{}})      == Some{('a', SNil{})}    : Maybe<&1, Char & String>  }# char matches the head and returns the tail (concrete char; is_eq needs it).law char_match:  for t: String  { P.Parse.char('a', SCon{'a', t}) == Some{('a', t)} : Maybe<&1, Char & String> }# char fails on empty input.law char_fail_empty:  for +c: Char  { P.Parse.char(c, SNil{}) == None{} : Maybe<&1, Char & String> }# char fails when the head differs (concrete distinct chars).law char_fail_mismatch:  {    P.Parse.char('a', SCon{'b', SNil{}}) == None{}    : Maybe<&1, Char & String>  }# string literal: empty pattern always matches (case-split on s in the proof).law string_empty:  for s: String  { P.Parse.string(SNil{}, s) == Some{(SNil{}, s)} : Maybe<&1, String & String> }# map over fail is None.law map_fail:  for s: String  {    P.Parse.map(U32, U32, (x => x), P.Parse.fail(U32, s))      == None{}    : Maybe<&1, U32 & String>  }# string literal hit consumes the prefix.law string_lit_hit:  {    P.Parse.string(SCon{'a', SNil{}}, SCon{'a', SCon{'b', SNil{}}})      == Some{(SCon{'a', SNil{}}, SCon{'b', SNil{}})}    : Maybe<&1, String & String>  }# string literal miss fails.law string_lit_miss:  {    P.Parse.string(SCon{'a', SNil{}}, SCon{'b', SNil{}})      == None{}    : Maybe<&1, String & String>  }