check

Tests: unit tests, properties and models, run by heff test.

A test is a top-level definition of type Test: heff test FILE runs each one of the file’s own, after its watches, but one another of them uses (directly or through the file’s other definitions), which runs under that one, by its groups’ names. It is found by its type, not by its name; a watch stays an example in a definition’s documentation, a test is what is checked of it, and both are counted by the same runner.

import check import co import generator as Generator

arithmetic : Test arithmetic = group “arithmetic” [ unit “one and one” (assertEqual (1 + 1) 2) , property “reversed twice” (do xs <- forAll (Generator.list 0 20 (Generator.int 0 99)) label (if null xs then “empty” else “not empty”) assertEqual (reverse (reverse xs)) xs) ]

A test is a computation with effects, and its type says which: a unit test only checks (check), a property also draws random values (random). Neither can do anything else. The runner handles both, and gives the randomness from a seed, so that a run is replayed by its seed. It handles them in a generator’s monad, so a property is itself a generator, of runs: a run that fails shrinks as all of its draws do, each made again from the shrinks of those before it, with no shrinking written for it.

An integration test (integration) also has the world outside: the process (commands run, std.process) and the filesystem. heff test cannot run it in itself; it builds the file’s tests into a program through C (integrationMain), and runs each integration test in it, in a new directory of its own, killed at its time limit (withinTime). A unit test or an integration test may keep golden texts (golden), held to the files kept beside the test’s, or written there by heff test --update.

What a value is shown as, for a counterexample or for what differs, is its type’s Debug (the prelude’s: as the source writes it, a string quoted, not its Show text), an instance argument: a type of the test’s own is given one by an instance (instance instanceDebugColor : Debug Color). A generator is given by hand. Two values are equal for assertEqual when they are shown the same, as a watch holds when its value is shown as its expectation is.

A model-based test (agree) runs a program of commands on a system and on a model of it, and holds when they observe the same after each command; a property draws the programs, which shrink to a short one that tells the two apart (std.ordmap against a list).

RandomF

data RandomF (m : Type -> Type) x = Draw (Generator.Generator x)

Randomness: a value drawn from a generator.

random

random : HFunctor

For random values drawn: what a property is given, and a unit test is not.

Failure

data Failure = Because String | Differ String String

Why a test failed: said in words, or two values (shown) that are not the same, what was expected first.

CheckF

data CheckF (m : Type -> Type) x
  = Fail Failure
  | Discard
  | Skip String
  | Label String x
  | Note (Unit -> String) x
  | Golden String String x
  | Sub String (m Unit) x

Checking: a failure, a run given up on (its assumptions do not hold), a label of the run (counted over the runs), a note (shown if the run fails; made only then), a golden text (a name, and the text, held by heff test to the one kept under that name), and a subtest (its name, and what it does), and a test skipped (why: what it needs is not there).

check

check : HFunctor

For what a test says of itself: a failure, a case discarded or skipped, labels and notes, a golden text compared, and its subtests.

forAll

forAll : {a : Type}
       -> {e : HFunctor}
       -> {{rnd : random <: e}}
       -> {{chk : check <: e}}
       -> {{shows : Debug a}}
       -> Generator.Generator a
       -> Co e a

A value of g, shown (debug) if the run fails.

failure

failure : {a : Type}
        -> {e : HFunctor}
        -> {{chk : check <: e}}
        -> String
        -> Co e a

The test fails, for this reason.

assert

assert : {e : HFunctor} -> {{chk : check <: e}} -> String -> Bool -> Co e Unit

The test fails unless b holds; what says what should have.

assertEqual

assertEqual : {a : Type}
            -> {e : HFunctor}
            -> {{chk : check <: e}}
            -> {{shows : Debug a}}
            -> a
            -> a
            -> Co e Unit

The test fails unless what was got (first) and what was expected are the same when shown (debug); then it says what differs.

assume

assume : {e : HFunctor} -> {{chk : check <: e}} -> Bool -> Co e Unit

The run is given up on unless b holds: a property’s assumption. Runs given up on are not counted as runs, and too many fail it.

skip

skip : {a : Type} -> {e : HFunctor} -> {{chk : check <: e}} -> String -> Co e a

The test is skipped, for this reason: what it needs is not there (a tool not installed, a system it is not of). heff test says it is, and why, and counts it apart, neither held nor failed.

label

label : {e : HFunctor} -> {{chk : check <: e}} -> String -> Co e Unit

The run is counted under l: the runner says what part of the runs each label had, so that a property that held only of trivial values shows.

note

note : {e : HFunctor} -> {{chk : check <: e}} -> String -> Co e Unit

Shown with the counterexample, if the run fails.

golden

golden : {e : HFunctor} -> {{chk : check <: e}} -> String -> String -> Co e Unit

The text, held to the golden one kept under name: heff test keeps it in a file beside the test’s own, in the directory named as the file without its .hf and with .golden (NAME in parser.golden/, of parser.hf), and fails the test where the two differ; heff test --update writes the text there instead. The name is a file’s: letters, digits, -, _ and ., not first. A unit test or an integration test keeps goldens, not a property.

subtest

subtest : {e : HFunctor}
        -> {{chk : check <: e}}
        -> String
        -> Co e Unit
        -> Co e Unit

A test of its own within an integration test, as Go’s t.Run: it is said on a line of its own, test / name, holds or fails by itself and keeps its own golden texts, and --run selects it at its level. heff test runs it in a program of its own, as many at once as its jobs: the test’s program, asked for the subtest by its names, does the test again, doing only the subtests on the way to it. So a test does the same each time up to its subtests, and names each once (no / in a name). What the test does after a subtest is done as if the subtest held.

each : List String -> Co e Unit each Nil = pure MkUnit each (Cons n rest) = do subtest n (do …) each rest

Trace

type Trace =
  { notes : List (Unit -> String)
  , labels : List String
  , goldens : List (String, String)
  , subtests : List String
  }

What a run has said so far, backwards: its notes, labels, golden texts and the subtests it named.

noTrace

noTrace : Trace

andThen

andThen : Trace -> Trace -> Trace

Run

data Run a
  = Going Trace a
  | Failed Trace Failure
  | Discarded
  | Skipped Trace String
  | Reached (Run Unit)

A run of a test, so far: going on, failed, given up on, or come to the subtest it was run for, and what came of that.

after

after : {a : Type} -> Trace -> Run a -> Run a

proceed

proceed : {a b : Type}
        -> (a -> Generator.Generator (Run b))
        -> Run a
        -> Generator.Generator (Run b)

drawAlg

drawAlg : {m : Type -> Type}
        -> {a : Type}
        -> RandomF m a
        -> Generator.Generator (Run a)

checkRun

checkRun : {m : Type -> Type} -> {a : Type} -> CheckF m a -> Run a

checkAlg

checkAlg : {m : Type -> Type}
         -> {a : Type}
         -> CheckF m a
         -> Generator.Generator (Run a)

runner

runner : Handler (random <+> check)

The runner’s handler: a test is a generator of runs, so a draw is a generator’s value, and a run’s draws shrink together.

Config

type Config = { runs : Int, discards : Int, shrinks : Int }

How a property is run: how many runs, how many may be given up on, and how many shrinks are tried at most.

defaults

defaults : Config

outside

outside : HFunctor

The world outside the program: the process (commands run), the filesystem, and the releases the program’s withs keep there.

integrated

integrated : HFunctor

The effects an integration test is run in: checking, and the world outside.

defaultLimit

defaultLimit : Int

How long an integration test is given, unless withinTime says: a minute.

Test

data Test
  = UnitTest String (Co (random <+> check) Unit)
  | PropTest String Config (Co (random <+> check) Unit)
  | IntegrationTest String Int (Co integrated Unit)
  | Group String (List Test)

A test: a unit test, a property, an integration test (its time limit, in milliseconds), or tests under a name. (Each is kept in the runner’s world, its effects given.)

unit

unit : String -> ({e : HFunctor} -> {{chk : check <: e}} -> Co e Unit) -> Test

A unit test: it only checks.

property

property : String
         -> ({e : HFunctor}
             -> {{rnd : random <: e}}
             -> {{chk : check <: e}}
             -> Co e Unit)
         -> Test

A property: it draws random values and checks them, run 100 times (runs says otherwise).

thrownOutside

thrownOutside : Either Process.ProcessError (Either Filesystem.FileError Unit)
              -> Co integrated Unit

integration

integration : String
            -> ({e : HFunctor}
                -> {{chk : check <: e}}
                -> {{sys : Process.process <: e}}
                -> {{disk : Filesystem.filesystem <: e}}
                -> {{ex : exception Process.ProcessError <: e}}
                -> {{fx : exception Filesystem.FileError <: e}}
                -> {{cu : custodian <: e}}
                -> Co e Unit)
            -> Test

An integration test: it checks, runs commands and reads and writes files. heff test runs it in a program of its own, built through C, in a new directory of its own as its working directory (removed after it), and kills it at its time limit (a minute; withinTime says otherwise). A command held by withProcess that could not be run, a file held by a with that did not open, is thrown; a throw the test does not hear (try) fails it.

group

group : String -> List Test -> Test

Tests under a name.

runs

runs : Int -> Test -> Test

The property run n times (each property of the group).

withinTime

withinTime : Int -> Test -> Test

The integration test given ms milliseconds, not a minute (each integration test of the group).

Machine

type Machine c s m o =
  { system : s
  , model : m
  , step : c -> s -> (s, o)
  , stepModel : c -> m -> (m, o)
  , valid : s -> Bool
  }

A system and a model of it, each run a command at a time, each saying what it observes of the command: they agree when they observe the same. valid is what the system must always be.

agree

agree : {c s m o : Type}
      -> {e : HFunctor}
      -> {{chk : check <: e}}
      -> {{showsC : Debug c}}
      -> {{showsO : Debug o}}
      -> Machine c s m o
      -> List c
      -> Co e Unit

The commands run on the system and on the model, in order: after each, both observe the same, and the system is valid. (Drawn by a property, the commands shrink to a short program that tells them apart.) Each is shown, a command and what is observed, as its type’s Debug writes it.

Outcome

type Outcome =
  { name : String
  , ok : Bool
  , skipped : Maybe String
  , property : Bool
  , runs : Int
  , discarded : Int
  , shrinks : Int
  , labels : List (String, Int)
  , notes : List String
  , failure : Maybe Failure
  , seed : Int
  , goldens : List (String, String)
  , subtests : List String
  }

What came of a test: its name (under its groups’), whether it held, how many runs held and how many were given up on, how many shrinks made the counterexample, how many runs had each label, the counterexample’s notes (what was drawn, in order), why it failed, the seed it was run from, the golden texts it kept (each a name and a text, in order), for heff test to hold to theirs, the subtests it named, in order, for heff test to run, and why it was skipped, if it was (it holds, then, having checked nothing).

hashName

hashName : String -> Int

nubLabels

nubLabels : List String -> List String

countLabels

countLabels : OrdMap.OrdMap String Int
            -> List String
            -> OrdMap.OrdMap String Int

Tally

type Tally = { runs : Int, discarded : Int, labels : OrdMap.OrdMap String Int }

noTally

noTally : Tally

passed

passed : String -> Bool -> Int -> Tally -> List (String, String) -> Outcome

failedWith

failedWith : String
           -> Bool
           -> Int
           -> Tally
           -> Int
           -> Trace
           -> Failure
           -> Outcome

skippedWith

skippedWith : String -> Bool -> Int -> Trace -> String -> Outcome

isFailed

isFailed : {a : Type} -> Run a -> Bool

firstFailing

firstFailing : List (Unit -> Generator.Tree (Run Unit))
             -> Maybe (Generator.Tree (Run Unit))

Shrunk

type Shrunk = { tree : Generator.Tree (Run Unit), shrinks : Int }

shrink

shrink : Int -> Int -> Generator.Tree (Run Unit) -> Shrunk

A failing run made smaller: its first shrink that fails too, then that one’s, as long as there is one (and limit is not reached).

failedRun

failedRun : String -> Bool -> Int -> Tally -> Shrunk -> Outcome

Next

data Next = Again Tally | Done Outcome

After a run: the tally with it, or the outcome it made.

judge

judge : String -> Config -> Int -> Tally -> Generator.Tree (Run Unit) -> Next

loop

loop : String
     -> Config
     -> Int
     -> Generator.Generator (Run Unit)
     -> Generator.Seed
     -> Tally
     -> Outcome

The property’s runs: each from a seed of its own, at a size growing to 100.

runUnit

runUnit : String -> Int -> Co (random <+> check) Unit -> Outcome

nameOf

nameOf : List String -> String

selectedBy

selectedBy : List Regex.Regex -> List String -> Bool

Whether a test of these names, its groups’ and then its own, is selected by the levels of a pattern (heff test --run): each name matched by the level of its depth, those deeper than the pattern by any, as Go’s -run A/B selects.

runUnder

runUnder : Int -> List Regex.Regex -> List String -> Test -> List Outcome

runTest

runTest : Int -> Test -> List Outcome

Each test, run from the seed: its unit tests and properties (--seed N gives the seed; the same seed runs the same).

runSelected

runSelected : String -> Int -> Test -> List Outcome

Each test the pattern selects (selectedBy), run from the seed: what heff test runs in itself of each test it finds. A pattern that is not read selects none (heff test reads it first).

integrationsUnder

integrationsUnder : List Regex.Regex
                  -> List String
                  -> Test
                  -> List (String, Int)

integrationsSelected

integrationsSelected : String -> Test -> List (String, Int)

The integration tests the pattern selects, each name and time limit: what heff test runs outside itself, a program each.

integrationsIn

integrationsIn : List String -> Test -> List (String, Co integrated Unit)

mapRun

mapRun : {a b : Type} -> (a -> b) -> Run a -> Run b

Outside

type Outside a = List String -> Co outside (Run a)

A run outside: given the names of the subtest it is run for, those not yet come to (none: the test itself).

runOutside

runOutside : RawFunctor

valueOfRun

valueOfRun : {a : Type} -> Run a -> Co outside a

continueOutside

continueOutside : {a b : Type}
                -> (a -> Co outside (Run b))
                -> Run a
                -> Co outside (Run b)

cameTo

cameTo : {a : Type} -> List String -> a -> Run Unit -> Run a

subtestRun

subtestRun : {a : Type}
           -> String
           -> Outside Unit
           -> a
           -> List String
           -> Co outside (Run a)

A subtest come to, run for these names: the test itself names it (none left), and does no more of it; on the way to the one run for, it is done, the names after its own given it; else passed over.

checkOutside

checkOutside : {a : Type} -> CheckF Outside a -> Outside a

outsideRunner

outsideRunner : Handler integrated

The runner of an integration test: checking handled, the world outside’s operations done as they are.

integrationOutcome

integrationOutcome : String -> Run Unit -> Outcome

twice

twice : List String -> Maybe String

badName

badName : String -> Bool

namesHeld

namesHeld : Outcome -> Outcome

what came of a test, its subtests’ names held to being names: each once, and none with a /, which --run takes for a level’s end

subtestOutcome

subtestOutcome : String -> List String -> Run Unit -> Outcome

integrationRun

integrationRun : String
               -> List String
               -> Maybe (String, Co integrated Unit)
               -> Co outside Outcome

failureJson

failureJson : Maybe Failure -> JSON.Json

outcomeJson

outcomeJson : Outcome -> JSON.Json

An outcome of an integration test as its program writes it, JSON: whether it held, its notes, why it failed, its golden texts, its subtests’ names, why it was skipped.

outcomeMarker

outcomeMarker : String

What an integration test’s program writes before its outcome, on a line of its own, where it is run by hand (not by heff test, which names a file for it, outcomeVariable).

outcomeVariable

outcomeVariable : String

The environment variable by which heff test names the file an integration test’s program writes its outcome to: a file of its own, not its output, which what the test runs may write to too.

outcomeWritten

outcomeWritten : Maybe String -> Outcome -> Co outside Unit

Integrations

type Integrations = Co outside Unit

What a file’s integration tests are run by: integrationMain’s.

integrationMain

integrationMain : List Test -> Integrations

The program heff test builds of a file’s tests: it runs the integration test its first argument names (its subtest, the arguments after it naming it a level each), where it is run (in the directory heff test gives it), and writes what came of it to the file outcomeVariable names (else to its output, after outcomeMarker).

instanceDebugFailure

instance instanceDebugFailure : Debug Failure

instanceDebugOutcome

instance instanceDebugOutcome : Debug Outcome

An outcome, as the record it is (for a test of tests).