Commit Graph

21 Commits

Author SHA1 Message Date
Brian Huffman
f609b36225 Rename primitive demote to the more self-explanatory name number.
The name "demote" is only meaningful to those who already know what
the Cryptol primitive does. Also, due to recent changes in the error
and warning messages, the name "demote" is showing up much more often
in REPL output. For example:

    Defaulting type argument 'rep' of 'demote' to [2]

    Showing a specific instance of polymorphic result:
      * Using 'Integer' for type argument 'rep' of 'Cryptol::demote'

These messages will hopefully be made less confusing to non-experts
if the name "demote" is replaced with "number".
2018-07-27 13:52:57 -07:00
Aaron Tomb
99f3fdbf37 Merge Cryptol/Extras.cry with Cryptol.cry
Closes #427.
2018-05-23 15:55:05 -07:00
Brian Huffman
fccf55f30f Remove obsolete cvs-era $Header$ keywords. 2018-03-22 13:33:12 -07:00
Iavor Diatchki
2bf932045d Fix benchmarking code 2017-10-30 13:20:50 -07:00
Iavor Diatchki
98e8a4b308 Fix the benchmarking code. 2017-10-23 10:14:17 -07:00
Iavor Diatchki
b5ef48dcd7 Fix-up the benchmarking code. 2017-10-06 11:55:48 -07:00
Aaron Tomb
33b064b88c Fix benchmarks for SBV 7.0 2017-07-21 08:42:49 -07:00
Aaron Tomb
d76f21f89e Update benchmarks to find Prelude and CryptolTC.z3
Since they don’t run in the normal REPL environment, they need to know
about where to find the Prelude and CryptolTC.z3 more directly.
2017-03-21 12:31:04 -07:00
Adam C. Foltzer
1a68b4f640 add benchmarks for Extras
There are separate benchmarks for the Extras.cry module and the combined
Prelude + Extras module because the performance characteristics are nonlinear.
2016-08-09 13:47:25 -04:00
Rob Dockins
bdcfdd39a1 Update benchmarks for new interpreters 2016-05-30 23:07:05 -07:00
Brian Huffman
1322156d28 Remove trailing whitespace 2016-02-19 10:08:20 -08:00
Adam C. Foltzer
4d3fc9a413 Update copyright dates and add missing headers 2016-01-19 18:19:35 -08:00
Adam C. Foltzer
92c328f108 fix benchmarks for name API changes 2015-10-22 13:32:37 -07:00
Adam C. Foltzer
b8ba4ebd69 fix benchmarks and NFData instances
The benchmark suite no longer uses the `iteSolver` option.

Added a dependency on `deepseq-generics` so that the `NFData` instances
work correctly in Stackage LTS 2. Versions of `deepseq` before 1.4 have
a default instance that amounts to WHNF rather than NF, so benchmarks
were being measured incorrectly.
2015-10-21 13:19:15 -07:00
Adam C. Foltzer
28461e7b72 update attribution on SHA512 2015-09-14 17:18:47 -07:00
Adam C. Foltzer
50ca428018 add regression in #269 to benchmark suite 2015-08-20 15:49:06 -07:00
Adam C. Foltzer
32e55cc11f add benchmark sources 2015-08-12 14:41:44 -07:00
Adam C. Foltzer
4e6dcaa026 add NFData instances for many cryptol types
add more benchmarks as well
2015-08-12 14:29:30 -07:00
Adam C. Foltzer
e9c85a3925 add a hex version of Big Sequence 2015-08-10 16:53:08 -07:00
Adam C. Foltzer
d3d6ae154a add typechecking and large sequence benchmarks 2015-08-10 13:52:01 -07:00
Adam C. Foltzer
b6d6691ab0 start benchmarking suite with a Prelude parse test 2015-08-10 11:24:36 -07:00