GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-12-20 22:41:56 +03:00
Code Issues Projects Releases Wiki Activity
1,707 Commits 67 Branches 28 Tags 96 MiB
86898c1076
Commit Graph

36 Commits

Author SHA1 Message Date
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
Iavor Diatchki
0d81f0ba25 Implement defaulting in the presence of overloaded literals. 2018-06-20 15:06:19 -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
Aaron Tomb
02e9ea5ea5 Fix test output due to re-sorting environment 2018-04-02 15:35:10 -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
3f4cc570cf Use a record for all module parameters at the value level. Also improve PP 2017-10-25 16:39:29 -07:00
Brian Huffman
cce32a4868 Merge branch 'master' into integer 
This brings the Logic and Zero type classes into the integer branch.
 2017-09-28 13:18:27 -07:00
Brian Huffman
35423d0243 Update test output. 2017-09-15 16:38:03 -07:00
Brian Huffman
860060c085 Fix test output. 2017-09-15 14:05:27 -07:00
Brian Huffman
5332d98261 Fix test output 2017-09-13 17:04:52 -07:00
Robert Dockins
ef047d3a19 Fix test breakage due to new operations in the Cryptol prelude. 2017-08-16 17:37:24 -07:00
Iavor Diatchki
1e4fb89f4c Fix test, due to changes in the Prelude. 2017-07-10 11:05:59 -07:00
Aaron Tomb
e282c65a7e Fix test failures from latest type checker changes 
Recent changes resolved issue 002, so we no longer need to indicate that
it's expected to fail. Other small changes to the type checker have
made things like type variable numbers change slightly.
 2017-06-20 10:08:36 -07:00
Brian Huffman
9a267b1f0c Removed definition of binary infix (~) from Cryptol prelude. Fixes #423. 
This change partially reverts changeset c620cbf2, which fixed #296,
which was about supporting `:t (~)` in the REPL.

As of this change, `:t (~)` will no longer work in the REPL.
The regression test for issue #296 is removed.
 2017-05-24 09:39:50 -07:00
Iavor S. Diatchki
2c3145a417 Fix some of the broken tests. 2017-02-08 17:24:15 -08:00
Brian Huffman
dafd48cad0 Simplify type of primitive function 'pmult'. Fixes #366. 
Old: (fin a, fin b) => [a] -> [b] -> [max 1 (a + b) - 1]
New: (fin a, fin b) => [1 + a] -> [1 + b] -> [1 + a + b]
 2016-09-20 15:13:40 -07:00
Robert Dockins
28d4f1d3fe Modify 'updates' and 'updatesEnd' to take the indices and values 
as separate vector arguments, rather than as a single vector
argument of pairs.
 2016-08-16 14:36:46 -07:00
Robert Dockins
64267f51ac Add the short-cutting boolean operators (/\), (\/), and (==>) 
to the Cryptol prelude.  This is in service of eventually addressing
issue #241.
 2016-08-12 17:12:34 -07:00
Robert Dockins
f746ef0d66 Fix test suite after changes to Cryptol prelude altered output 2016-08-12 12:22:58 -07:00
Robert Dockins
998bddc7a7 Merge remote-tracking branch 'origin/master' into new-eval 
Fix some minor conflicts in the test suite.
Conflicts:
	tests/issues/issue002.icry.fails
	tests/issues/issue148.icry.stdout
	tests/issues/issue198.icry.stdout
	tests/issues/issue214.icry.stdout
	tests/issues/issue290v2.icry.stdout
	tests/issues/issue312.icry.fails
 2016-07-12 14:58:53 -07:00
Adam C. Foltzer
2c428804bc remove splitBy and update documentation 
Closes #291
 2016-07-05 09:58:49 -07:00
Rob Dockins
33710b6d25 Update unit test golden outputs 2016-05-30 17:51:08 -07:00
Robert Dockins
38946745c3 Add the 'lg2' type function as a synonym. 
Fixes #248
 2016-05-04 17:54:08 -07:00
Robert Dockins
c620cbf237 Update the parser to allow prefix operators in more places. 
This allows us to define (~) as a prefix operator symbol synonym
for `complement`.

Fixes #296.
 2016-05-04 16:26:36 -07:00
Adam C. Foltzer
07da2018b7 switch to more portable seeding for random 
The `random` primitive previously took a `[32]` seed, but this causes
inconsistency between 32-bit and 64-bit platforms when the seed is large
enough to wrap around in GHC's representation of an `Int`. This patch
switches to an API that seeds directly with four 64-bit words, and so
should behave the same way on our supported platforms.
 2016-01-19 18:17:34 -08:00
Iavor S. Diatchki
c9e4fab6a8 Fix up tests. 2015-08-12 15:52:18 -07:00
Trevor Elliott
f06b4deaea Update 226 output, as it uses :browse 2015-06-09 14:32:17 -07:00
Brian Huffman
c2859d579b Update output for regression test 226 2014-07-21 16:18:47 -07:00
Adam C. Foltzer
ba0a0e8576 Initial import from internal repo 2014-04-17 15:34:25 -07:00