Brian Huffman
c1949586c2
Thunk elements of EList expressions of type Bit during evaluation.
...
Fixes #488 .
2018-03-21 17:55:11 -07:00
Brian Huffman
d84d697aae
Fix compiler warnings and remove dead code.
2018-03-21 11:21:48 -07:00
Brian Huffman
2e4fa35209
Remove unused package dependencies.
2018-03-21 11:15:46 -07:00
Aaron Tomb
a8b58a09d6
Bump pinned SBV version to 7.6
2018-03-21 10:20:41 -07:00
Aaron Tomb
6a0d7ca9df
Remove cryptol-test-runner from frozen packages
2018-03-21 10:13:52 -07:00
Brian Huffman
83442f5049
Implement signed shift (>>$) and less-than (<$) in reference interpreter.
...
Fixes #469 .
2018-03-21 09:58:48 -07:00
Brian Huffman
5cd9141fe7
Add functions head and last to Cryptol prelude. Fixes #465 .
...
Also fix regression test output.
2018-03-16 15:10:36 -07:00
Aaron Tomb
7f27ed592d
Remove unnecessary dependency on old-time
2018-03-12 12:53:27 -07:00
Aaron Tomb
b96eef5ef0
Bump library versions for GHC 8.2
2018-03-12 11:02:15 -07:00
Max Orhai
a4a14b4c98
Merge branch 'html-doc-improvements'
2018-03-08 13:38:33 -08:00
Brian Huffman
134d8cca4c
Thunk elements of EList, ETuple, and ERec expressions during evaluation.
...
Fixes #432 .
2018-03-07 18:21:16 -08:00
Max Orhai
1c2996610d
Use blaze for HTML generation
2018-03-05 17:07:19 -08:00
Aaron Tomb
032522a497
Allow GHC 8.2.* with Cabal-based builds
2018-02-28 10:22:55 -08:00
Aaron Tomb
1fae177542
Add Cabal configuration for GHC 8.2
2018-02-28 10:15:29 -08:00
Aaron Tomb
70a4728e5c
Add ONR acknowledgement to README
2018-01-22 10:54:27 -08:00
Aaron Tomb
e704df26cb
Merge pull request #496 from avadacatavra/mailing-list-update
...
updated mailing list in readme
2018-01-19 07:58:02 -08:00
ddh
a4779e4531
updated mailing list in readme
2018-01-19 12:38:22 +00:00
Brian Huffman
ff86d02600
Fix typo in docstring.
2018-01-11 10:24:26 -08:00
Brian Huffman
60e03d7313
Suppress unused-variable warning for names that are defined externally.
...
Previously names were considered "local" if they have the same module
name as the module name that we are performing renaming on (the idea
being that all "external" names would have been imported from a different
module).
However, this assumption doesn't hold for the "<interactive>" module,
which is used for REPL declarations. Names from earlier REPL declarations
should be considered "external" when renaming later REPL expressions, even
though they have the same "<interactive>" module name.
The problem is fixed by checking whether a name was already present in the
old naming environment; if so, then it is considered "external" and will
not generate an unused-variable warning.
2018-01-11 10:23:19 -08:00
Iavor Diatchki
79e6f83c70
Report proper errors instead of panicing.
...
Previously I erroneously thought this would be reported by the renamer,
so I turned the errors into panics.
Fixes #493
2018-01-04 15:27:37 -08:00
Iavor Diatchki
f4d306f1ee
Add a TBox based AES
2018-01-04 14:52:41 -08:00
Iavor Diatchki
4aa68c9cf4
Add a note for another useful rule
2018-01-04 10:59:33 -08:00
Iavor Diatchki
762b31597f
Add a case to solve things like: 4 == 2 ^^ x
2018-01-04 10:57:05 -08:00
Iavor Diatchki
31d6a5d5a7
Split up AES algorithm into multiple modules.
2018-01-03 15:58:10 -08:00
Iavor Diatchki
bc45e751d1
Fixes #492 incorrect simplification for tMax
2018-01-03 09:56:47 -08:00
Iavor Diatchki
989e5734ef
Move defaulting code to a separate module.
2017-12-22 16:01:19 -08:00
Iavor Diatchki
7bf0fa8222
Remove evaluator cases that should not occur.
...
These are translated away in the solver.
2017-12-22 11:24:44 -08:00
Iavor Diatchki
c481fbc6e8
Handle lifted selectors in the solver, so they are not visible in evaluator.
2017-12-22 11:23:54 -08:00
Iavor Diatchki
defb9b0598
When things go wrong, give us a hint as to where they did.
2017-12-22 11:23:26 -08:00
Iavor Diatchki
b9957e49ce
Make location more precise
2017-12-21 14:39:58 -08:00
Iavor Diatchki
2dff60fb0e
Allow some errors to subsume others.
2017-12-21 14:34:37 -08:00
Iavor Diatchki
978b3b232b
Remove errors that should have been handled by the renamer.
2017-12-21 14:28:58 -08:00
Iavor Diatchki
9c06f07223
Move errors to their own module.
2017-12-21 13:59:53 -08:00
Iavor Diatchki
8bf780b969
Print even when malformed. Useful for printing before renamer.
2017-12-21 13:32:17 -08:00
Iavor Diatchki
89d453a6fa
Print location under, as it was before.
2017-12-21 10:21:53 -08:00
Iavor Diatchki
c093d05659
Don't print file locations twice.
2017-12-21 10:19:04 -08:00
Iavor Diatchki
01b72ce0f9
When a test fails, print a suggestion how to make the output gold.
2017-12-21 10:14:44 -08:00
Iavor Diatchki
32fb511ced
Add location more generally.
2017-12-15 14:12:38 -08:00
Iavor Diatchki
7db18e817c
Improve error message for ambiguous types.
2017-12-15 14:05:15 -08:00
Iavor Diatchki
2272a59314
Rename type synonyms properly.
2017-12-01 10:29:42 -08:00
Iavor Diatchki
3443331f06
Add a test
2017-12-01 09:51:43 -08:00
Iavor Diatchki
5cd90d0045
Fix up scoping when instantiating modules.
2017-12-01 09:51:28 -08:00
Iavor Diatchki
173ca8702f
Parametrize polyval by a starting value.
...
This makes it easier to continue hashing:
polyvalFrom H (xs # ys) start = polyvalFrom H ys (polyvalFrom H xs start)
2017-11-28 16:10:48 -08:00
Iavor Diatchki
f658f0244d
Add another test.
2017-11-28 14:26:12 -08:00
Iavor Diatchki
c0b4ddd608
Keep track of the order in which type parameters are declared in the file.
2017-11-28 14:07:14 -08:00
Iavor Diatchki
07029f95c3
Factor out the counter modding part.
...
This is convenient in a proof I am working on.
2017-11-28 11:37:10 -08:00
Iavor Diatchki
93c56ea428
Add support for working directly with key schedules.
...
This is useful for code that uses the same key multiple times.
2017-11-28 11:10:34 -08:00
Iavor Diatchki
9de90e5752
Slightly better parser messages.
2017-11-15 15:36:45 -08:00
Brian Huffman
951eebb8e2
Add more documentation of Cryptol prelude primitives.
2017-11-15 11:37:06 -08:00
Brian Huffman
79fbb61aa7
Require doc-strings to start with "/**" with exactly 2 asterisks.
...
Things like "/******* WARNING ********/" are now parsed as ordinary
comments. See #438 .
2017-11-15 11:36:25 -08:00
