gstest Examples

map

map.test.gs

label log{§gs{map}} $ ∧ (label log{§gs{nil}} $ forall gscode{f} $ λ 'f. map f nil `assert.eq` nil ) ∧ (label log{§gs{singleton}} $ forall gscode{f} $ λ 'f. forall gscode{x} $ λ 'x. map f (singleton x) `assert.eq` singleton (f x) ) ∧ (label log{§gs{<>}} $ forall gscode{f} $ λ 'f. forall gscode{xn} $ λ 'xn. forall gscode{ys} $ λ 'ys. map f (xn <> ys) `assert.eq` map f xn <> map f ys )

An expression of the form ∧ t0 ∧ t1 ∧ t2 is called a list; when the left-most operand of a series of left-associative operators is ommitted Global Script will supply a default value, if one is declared for the left-most operator, which will usually be the left identity of the left-most operator. In the specific case of ∧, the supplied value will be true, so ∧ t0 ∧ t1 ∧ t2 is syntax sugar for true ∧ t0 ∧ t1 ∧ t2, which is equivalent to t0 ∧ t1 ∧ t2. It is a compile-time error to use the list syntax when no supplied argument is declared for the left-most operator.

$ is a low-precedence right-associative application, same as in Haskell.

label log{label} test names a test. The label is given using Global Script logical markup.

forall gscode{x} p tests that p holds for all values (generally, all total finite values) of its domain. Global Script uses an exhaustive enumeration / exhaustive testing strategy to implement the universal quantifier; values are tested in order of increasing ‘size’ as defined by the generator. forall's first implicit argument is the generator to use, so an alternative generator can be supplied as forall @gen gscode{nm} p.

gscode{x} is the literal syntax for Global Script source with markup, of type globalscript.gscode.t (the same type as the argument to the gs macro). forall requires a name for the generated value to improve the quality of error messages by labeling the generated values. To allow forall to display the generated value if the test fails, its type should be an instance of the of fmtgs.c overload, which allows generating a literal denoting the given value and formatted as a globalscript.gscode.t value. The fmtgs.c instance is the second implicit argument to forall, so if you need to over-ride it for some reason you can use forall @_ @fmt.

assert.eq is polytypic; a default instance for module eq.c instances is available as assert.eq.byEq. assert.eq.byEq additionally requires a fmtgs.c instance to display the argument values in error messages. The assert.eq instance for lists doesn't use assert.eq.byEq, but is defined directly in terms of the assert.eq instance on list elements; it allows equal infinite lists to be tested and provides better error messages.