GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-12-14 17:51:43 +03:00
Code Issues Projects Releases Wiki Activity
1,780 Commits 68 Branches 28 Tags 95 MiB
409e544772
Commit Graph

264 Commits

Author SHA1 Message Date
Brian Huffman
409e544772 Restrict polynomial literals to bitvector types. Fixes #530. 2018-07-20 10:06:16 -07:00
Aaron Tomb
0b46db36ce Fix capitalization of MiniLock in test 2018-07-20 10:04:11 -07:00
Brian Huffman
5451683f4a Add regression test for #494. 2018-07-19 15:08:24 -07:00
Brian Huffman
d58aebcee8 Fix shadowing warnings in example cryptol code. 
Shadowing a name from the Cryptol prelude produces an unpredictable
warning message with a temporary file name, which is not good for our
regression test suite.
 2018-07-19 14:48:12 -07:00
Brian Huffman
d803192b2b Add regression test that loads all modules from examples directory. 
This file should be updated every time a new module is added to
`examples`.

Fixes #529.
 2018-07-19 09:57:18 -07:00
Brian Huffman
1e5209ade5 Add regression test for #413. 2018-07-11 13:00:53 -07:00
Brian Huffman
56824291b2 Add inequality constraints to types of fromThen and fromThenTo. 
This ensures that all applications of partial type functions are
well-defined.

Fixes #416.
 2018-07-11 12:58:49 -07:00
Brian Huffman
be8c334efe Reference interpreter uses base and infLength printing options. 
Fixes #412.
 2018-07-10 09:58:37 -07:00
Iavor Diatchki
4c6a69c0cf Improvements to naming of variables. 
This does a bunch of small changes, that should improve the usability
of Cryptol.  Namely:
  * When we are forced to make up a name, pick something derived from
    the source of the variable, annotated with the unique.
  * When pretty printing a schema, use "n,m,i,j,k" for numeric variables
    and "a,b,c,d,e" for value type vairable.
  * When generalizing, put numeric vairables first.
 2018-06-28 15:58:11 -07:00
Brian Huffman
836771aded Tweak names and order of type variables on Cryptol prelude functions. 
Also update test output for new type variable names.

See #517.
 2018-06-28 14:14:44 -07:00
Iavor Diatchki
75b56e251e Complain when we spot invalid literals. Fixes #519 2018-06-28 14:13:07 -07:00
Brian Huffman
a4a3207f9f Swap type argument order for zext and sext. 
The new argument order works better for partial type application,
so e.g. zext`{32} extends its argument to 32 bits.
 2018-06-28 10:40:37 -07:00
Iavor Diatchki
0bf36808ed Improve various defaulting/instantiatiation warnings and error messages. 2018-06-25 16:48:10 -07:00
Brian Huffman
9fcb481161 Generalize [x,y...] (infFromThen primitive) to class Arith. 2018-06-21 18:24:12 -07:00
Brian Huffman
4697683ac4 Generalize [x...] (i.e. infFrom primitive) to class Arith. 2018-06-21 17:57:13 -07:00
Brian Huffman
86898c1076 Remove now-redundant primitive toZ; use fromInteger instead. 2018-06-21 17:05:33 -07:00
Brian Huffman
dbd05b5acc Generalize prelude function fromInteger to class Arith. 2018-06-21 16:59:01 -07:00
Brian Huffman
1f0f41cf2b Add regression test for #323. 2018-06-21 09:33:44 -07:00
Iavor Diatchki
d46c5e26de Use the full path when suggesting the fix for the test. Fixes #509 2018-06-20 16:55:49 -07:00
Iavor Diatchki
cd2f6e045f Fix more tests. 2018-06-20 16:34:59 -07:00
Iavor Diatchki
29cef7008a Merge remote-tracking branch 'origin/master' into literal-class 2018-06-20 15:10:21 -07:00
Brian Huffman
171cfa00d1 Fix output for tests/issues/T146.icry to reflect changes in unification. 2018-06-20 15:09:01 -07:00
Iavor Diatchki
b179a6aad7 Merge remote-tracking branch 'origin/master' into literal-class 2018-06-20 15:06:43 -07:00
Iavor Diatchki
0d81f0ba25 Implement defaulting in the presence of overloaded literals. 2018-06-20 15:06:19 -07:00
Brian Huffman
bae811376c Fix test output for #146. 2018-06-20 14:57:54 -07:00
Brian Huffman
7a265773a8 Add regression test for #513. 2018-06-20 11:13:50 -07:00
Iavor Diatchki
e579113d05 Merge remote-tracking branch 'origin/master' into literal-class 
# Conflicts:
#	tests/mono-binds/test04.icry.stdout
#	tests/regression/check01.icry.stdout
#	tests/regression/check16-tab.icry.stdout
#	tests/regression/check16.icry.stdout
#	tests/regression/check21.icry.stdout
#	tests/regression/check22.icry.stdout
 2018-06-20 09:14:17 -07:00
Iavor Diatchki
33f0ab3979 Improved locations for defaulting warnings. 2018-06-19 17:28:59 -07:00
Brian Huffman
cc478e8684 Update test output. 2018-06-15 14:20:27 -07:00
Brian Huffman
e512dc2c17 Update test case output. 2018-06-15 14:15:39 -07:00
Brian Huffman
b3df205e04 Adapt test output to new primitives. 2018-06-15 10:18:02 -07:00
Brian Huffman
570f0be2ea Remove redundant fin constraint from the type of demote. 
`fin bits` and `bits >= width val` together imply `fin val`.
 2018-06-14 12:33:20 -07:00
Brian Huffman
dda5d34131 Fix constraints on type of primitive intmod. 
The old type did not forbid literals of the invalid type `Z inf`.
 2018-06-14 12:24:32 -07:00
Brian Huffman
50f54c9610 Fix test output due to addition of new primitive. 2018-06-14 06:22:59 -07:00
Brian Huffman
ab000984d2 Remove redundant prelude functions not, extend, and extendSigned. 
These were recently moved here from Cryptol::Extras. They are duplicates
of existing functions `complement`, `zext`, and `sext`.

See #427.
 2018-05-24 14:41:09 -07:00
Aaron Tomb
c42a135fce Update tests to account for Cryptol::Extras merge 2018-05-24 09:23:17 -07:00
Brian Huffman
62dfa1d58f Use sbv version 7.7. Fixes #486. 
Also add regression test for #486.
 2018-04-30 09:54:26 -07:00
Brian Huffman
3be72ae2cb Replace indexing primitives (!!) and (@@) with cryptol implementations. 2018-04-18 16:50:39 -07:00
Brian Huffman
2cdf9bd159 Replace primitives pmult, pmod, pdiv with cryptol implementations. 2018-04-15 06:56:20 -07:00
Diatchki
fcf5230bbd Fix build 
Make it work with GHC 8.2
 2018-04-03 09:55:31 -07:00
Aaron Tomb
02e9ea5ea5 Fix test output due to re-sorting environment 2018-04-02 15:35:10 -07:00
Aaron Tomb
0bbb7fa6ec Fix tests with GHC 8.4.1 2018-04-02 15:35:03 -07:00
Brian Huffman
fccf55f30f Remove obsolete cvs-era $Header$ keywords. 2018-03-22 13:33:12 -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
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
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
f658f0244d Add another test. 2017-11-28 14:26:12 -08:00
Iavor Diatchki
c5e0540a0f Fix test. 2017-10-30 14:24:47 -07:00
Iavor Diatchki
3f4cc570cf Use a record for all module parameters at the value level. Also improve PP 2017-10-25 16:39:29 -07:00