Commit Graph

322 Commits

Author SHA1 Message Date
Rob Dockins
c1b641c420 Add a test case for issue725 2020-05-26 17:08:20 -07:00
Rob Dockins
aaf78e23ec Add a bit more output for the Satisfiable/Counterexample cases 2020-05-26 17:08:20 -07:00
Brian Huffman
37f1fd8b4b Add regression test for #731. 2020-05-18 17:17:58 -07:00
Brian Huffman
700b31803c Add regression test for #723. 2020-05-15 07:36:11 -07:00
Iavor Diatchki
c3eca4f22a Check that the declared type of prims matches the expected one.
Fixes #711
2020-05-05 14:30:25 -07:00
robdockins
f29f0158ff
Merge pull request #703 from GaloisInc/issue702
issue702
2020-04-23 12:22:25 -07:00
Brian Huffman
4dd77c756b Update type variable numbering in test suite output. 2020-04-20 11:29:49 -07:00
Rob Dockins
ce85155dbe Add unit test for issue702 2020-04-17 17:48:44 -07:00
robdockins
87ad864185
Merge pull request #684 from GaloisInc/eval-refactor
Evaluator refactor
2020-04-02 09:42:04 -07:00
Rob Dockins
d08046d063 Test case for issue #662 2020-04-02 09:40:44 -07:00
Rob Dockins
943e11478a Add regression test for word updates 2020-03-30 15:09:53 -07:00
Iavor Diatchki
fcc7a19998 More information when browsing.
This implements the feature request in #689
2020-03-24 16:53:48 -07:00
Rob Dockins
f016a9a9fc Define carry and scarry instead of making them primitive. 2020-03-17 13:25:39 -07:00
Iavor Diatchki
3038eacf54 Add a test for record updating.
This completes the implementation of record updates.
Fixes #399
2020-01-21 11:35:19 -08:00
Kevin Quick
578d268b8e
Update cryptol-test-runner maintainer and license 2019-12-23 18:18:54 -08:00
Brian Huffman
aec6cb0a7e Add regression test for #670. 2019-12-16 18:02:56 -08:00
Brian Huffman
3281e7c121 Revert "Add regression test for #444."
This reverts commit 85bff672ef.

The error message in the expected output file `issue444.icry.stdout`
contained a system-specific absolute file path.

Fixes #673.
2019-12-16 14:12:44 -08:00
Brian Huffman
4b29967315 Add regression test for issue #614. 2019-12-13 11:13:03 -08:00
Brian Huffman
4da0f19a21 Add regression test for #667. 2019-12-06 15:51:57 -08:00
Brian Huffman
c230e2395c Use Data.Map to normalize record field order in Value type.
Fixes #667.
2019-12-06 15:48:50 -08:00
Brian Huffman
67fc36764c Add regression test for #664. 2019-11-26 22:23:53 -08:00
Brian Huffman
85bff672ef Add regression test for #444. 2019-11-21 06:04:27 -08:00
Aaron Tomb
ddbd664326
Merge pull request #655 from GaloisInc/at-ghc-881
Fix build with GHC 8.8

Also updates CI to use GHC 8.4, 8.6, and 8.8 on both Travis and AppVeyor, and makes some small tweaks to make the tests pass in all six configurations.
2019-11-01 13:56:05 -07:00
Aaron Tomb
82d4a1b81a Fix test output for issues/allexamples 2019-11-01 12:28:13 -07:00
Aaron Tomb
47b2eccad7 Remove leading ./ from file names in test output 2019-10-28 13:57:37 -07:00
Aaron Tomb
3ea5e9e51c Make issue072 test more robust to solver versions 2019-10-25 11:39:31 -07:00
Iavor Diatchki
8fe9f5efa9 Add support for working with in-memory sources.
Currently we only use this for the Prelude, which is baked into Cryptol.
Previously we used to save it in a temporary file, which would show
up in error messages, leading to bad user experience and unreliable
test outputs.

Also improves the shadowing errors.

Fixes #569
2019-07-05 14:09:04 -07:00
Iavor Diatchki
ca4968ff3d Fix test. The error message changed, but is still valid.
We should really have only one way to say this,
I made a ticket: #633
2019-07-05 09:37:45 -07:00
Iavor Diatchki
4b5d569e09 Fix tests---some variables got renumbered.
We really should fix this up so we don't print the numbers unless
there really is an ambiguity.
2019-07-05 09:34:20 -07:00
Iavor Diatchki
72068cb961 Move type-level primitives to the Prelude.
For the time being, there is still some information about them that
is duplicated in Cryptol.TypeCheck.TCon, but we at least the parsed syntax
does not depend on the typechecked syntax.
2019-07-02 17:34:36 -07:00
Iavor Diatchki
1cfadef5ea Add a forgotten test 2019-07-01 10:26:39 -07:00
Brian Huffman
1e11ff6b8b Add type constraint synonyms (<) and (>).
Fixes #400.
2019-06-26 20:44:13 -07:00
Brian Huffman
14d25e8f9a Fix pretty printing for infix type/constraint synonyms. 2019-06-26 18:19:12 -07:00
Brian Huffman
10da255fd1 Re-implement infix type constraint (<=) as a constraint synonym.
Also removed special-case hack for (<=) in the renamer.

Also adapted test case output to account for the new prelude declaration.
2019-06-26 18:04:16 -07:00
Brian Huffman
0a1cea2912 Update test suite output to accommodate new prelude function. 2019-06-18 15:39:56 -07:00
Iavor Diatchki
ec7c9a0f6e Don't generalize a rec. group, if any members are marked as monomorphic.
Fixes #607
2019-06-14 16:14:14 -07:00
Iavor Diatchki
08c537122a Update nQueens example to not print the found solution. 2019-03-25 16:20:17 -07:00
Brian Huffman
7cb16586d4 Add regression test for #581. 2019-03-18 15:29:36 -07:00
Brian Huffman
5076273c10 Add regression test for issue #582. 2019-03-18 14:53:09 -07:00
Brian Huffman
9584fdb54d Remove some duplicate files from /examples that were also in cryptol-specs.
See #571.
2019-03-01 18:34:23 -08:00
Iavor S. Diatchki
139c7d50ac
Merge pull request #576 from GaloisInc/fingerprints
Track file content fingerprints alongside loaded modules
2019-02-28 11:02:27 -08:00
Eric Mertens
5e75f834e7 Update test for new utf-8 error message 2019-02-28 10:04:17 -08:00
Brian Huffman
24fb6c9511 Remove unused primitive fromThen. 2019-02-27 16:57:00 -08:00
Brian Huffman
c387dbe5fd Remove all uses of [x..] syntax from examples and tests. 2019-02-27 16:25:53 -08:00
Iavor Diatchki
d38eab4b2c Fix test. 2019-01-25 10:20:40 -08:00
Iavor Diatchki
4312787724 Fixes #565 2019-01-24 17:00:16 -08:00
Iavor Diatchki
60c1baebfd Indent goals to be shown a bit further, to line up with assumptions. 2019-01-08 16:42:34 -08:00
Iavor Diatchki
d8b1a7a601 Improve some of the error messages. 2019-01-03 11:28:59 -08:00
Iavor Diatchki
d377f38c9d Use the factored-out test-runner. 2018-12-11 16:30:02 -08:00
Brian Huffman
9b7597c4fd Update changed test output. 2018-12-11 15:52:19 -08:00