disco-lang / disco

Functional teaching language for use in a discrete mathematics course
Other
164 stars 23 forks source link

Tests that crash don't print counterexamples #364

Open byorgey opened 1 year ago

byorgey commented 1 year ago

Consider this test (from test/prop-fail/):

!!! forall a : Q, b : Q. divide a b * b =!= a
divide : Q -> Q -> Q
divide a b = a / b

It fails with a division by zero error, as it should, and prints out an example that led to the crash (a = 0, b = 0). After merging #365 , however, it will still fail but no longer prints out the example. Splitting out a separate issue to look into this later.

byorgey commented 7 months ago

For reference, here's the current output:

Disco> :load test/prop-fail/bad-tests.disco 
Loading bad-tests.disco...
Running tests...
  badmap:
  - Certainly false: badmap(λx. x / 0)([3, 4, 5]) =!= [6, 7, 8]
    Test failed with an error:
      Error: division by zero.
  - Certainly false: badmap(λx. x)([1, 2]) =!= [1, 2]
    - Left side:  [1, 1, 2, 2, 3]
    - Right side: [1, 2]
  - Certainly false: badmap(λx. x + 1)([3, 4]) > [5, 6]
  divide:
  - Certainly false: ∀a, b. divide(a)(b) * b =!= a
    Test failed with an error:
      Error: division by zero.
  - Certainly false: ∀a. divide(a)(2) < a
    Found counterexample:
      a = 0
  - Possibly false: ∃a. divide(a)(2) =!= abs(a) + 1
    No example was found; checked 50 possibilities.
Loaded.
byorgey commented 1 month ago

Also, why does the - Certainly false: badmap(λx. x + 1)([3, 4]) > [5, 6] case not print out any counterexample either?