Iavor S. Diatchki
300383772f
Just a clarification
2017-10-19 15:17:39 -07:00
Iavor S. Diatchki
095a7718d9
Add a pass to rewrite a param. module, into a non-param module
...
All definitions are parameterized by all parameters.
2017-10-19 13:45:40 -07:00
Iavor Diatchki
b8780ab68f
Add some tests.
2017-10-18 14:33:41 -07:00
Iavor Diatchki
c3d8b4b3f8
Allow focusing of parameterized modules; disable evaluation in such contexts.
2017-10-18 14:33:12 -07:00
Iavor Diatchki
432638a77a
Allow a value parameter to be defined by another value parameter.
2017-10-18 13:36:37 -07:00
Iavor Diatchki
1cbbba7c32
More functionality
2017-10-17 16:26:05 -07:00
Iavor Diatchki
dda54aa016
More progress
2017-10-16 15:54:42 -07:00
Iavor Diatchki
acacd0b53d
Merge remote-tracking branch 'origin/master' into abstract-types
...
# Conflicts:
# src/Cryptol/TypeCheck/Monad.hs
2017-10-16 14:25:08 -07:00
Iavor Diatchki
942173b7f9
Add comments and fixes #473
2017-10-16 14:09:52 -07:00
Iavor Diatchki
a85ff3a54b
Add comments
2017-10-16 14:05:46 -07:00
Iavor Diatchki
6ba8849216
Just reformat
2017-10-16 14:05:31 -07:00
Iavor Diatchki
043334f8f9
Name is cryptol nowadays
2017-10-16 14:05:17 -07:00
Iavor Diatchki
ec456b9447
Fix typo
2017-10-16 14:05:01 -07:00
Iavor S. Diatchki
15f236d42b
More loading of instances (incomplete)
2017-10-13 15:27:42 -07:00
Iavor S. Diatchki
2b21610796
Better integration of module parameters with module system and REPL
2017-10-13 11:35:46 -07:00
Iavor S. Diatchki
7dc7be45bb
Merge remote-tracking branch 'origin/master' into abstract-types
...
# Conflicts:
# src/Cryptol/REPL/Monad.hs
2017-10-13 10:45:35 -07:00
Iavor S. Diatchki
3f2ac1171c
Comments
2017-10-13 10:40:24 -07:00
Iavor Diatchki
51808bbf23
More comments
2017-10-06 16:24:10 -07:00
Iavor Diatchki
f71b951108
Some documentation.
2017-10-06 15:57:45 -07:00
Aaron Tomb
ef09fde6e5
Fix Travis for real now
2017-10-06 14:44:11 -07:00
Aaron Tomb
3134acbb7d
Better section names for Travis
2017-10-06 14:35:58 -07:00
Aaron Tomb
1cb7d4dcaa
Use cabal new-build on AppVeyor
2017-10-06 14:19:01 -07:00
Aaron Tomb
39766c1b2e
Use cabal new-build on Travis
2017-10-06 14:17:35 -07:00
Iavor Diatchki
b5ef48dcd7
Fix-up the benchmarking code.
2017-10-06 11:55:48 -07:00
Iavor S. Diatchki
13ac2d9f05
wibble
2017-10-05 15:52:50 -07:00
Brian Huffman
109255e28f
Update generated pdfs.
2017-10-05 15:14:49 -07:00
Brian Huffman
fd0fc99418
Update some Integer-related stuff in the reference interpreter.
2017-10-05 15:13:37 -07:00
Iavor S. Diatchki
4e65ad03f9
Almost complete module instantiation
2017-10-05 15:10:25 -07:00
Brian Huffman
e84dcc5126
Document logical connectives (==>, /\, \/) in Programming Cryptol book.
2017-10-05 14:17:51 -07:00
Brian Huffman
fd9e003cd3
More documentation for REPL commands :browse and :help.
2017-10-05 13:51:50 -07:00
Iavor S. Diatchki
f64f051842
Now wild cards in the types of module parameters
2017-10-05 13:49:25 -07:00
Iavor S. Diatchki
f7adf8f4ba
Validate schemas properly
2017-10-05 13:46:24 -07:00
Iavor S. Diatchki
933e2cd2ee
Merge branch 'abstract-types' of github.com:GaloisInc/cryptol into abstract-types
...
# Conflicts:
# src/Cryptol/ModuleSystem/InstantiateModule.hs
2017-10-05 12:45:11 -07:00
Brian Huffman
59a34a4624
Update table of Cryptol primitives with new type constraints.
2017-10-05 11:29:21 -07:00
Brian Huffman
11067f8220
Document new type classes Zero, Logic, and SignedCmp. Fixes #451 .
2017-10-05 11:15:49 -07:00
Brian Huffman
361be3827e
Fix incorrect spacing after abbreviation "vs."
2017-10-05 11:08:34 -07:00
Brian Huffman
6d484c854d
Fix inaccurate statements about Cmp class.
2017-10-05 10:38:37 -07:00
Brian Huffman
1909e9ca51
In Programming Cryptol table of contents, make entire lines clickable links.
2017-10-05 10:24:23 -07:00
Brian Huffman
ffe113669e
Document the REPL let-definition feature. Fixes #359 .
2017-10-05 10:23:34 -07:00
Brian Huffman
7b0b8836c0
Fix outdated reference to inf a constraint in docs.
2017-10-05 10:20:57 -07:00
Brian Huffman
0478ec434c
Uniformly place footnotes after punctuation.
2017-10-05 09:25:44 -07:00
Brian Huffman
4b386477ec
Avoid creating a new option when :set is used with a prefix of a name.
...
Fixes #450 .
2017-10-04 21:22:59 -07:00
Brian Huffman
a9de74ed5d
Implement module-name completion and validation for :browse.
...
Fixes #396 .
2017-10-04 19:17:42 -07:00
Iavor Diatchki
1f2cacbae5
Merge branch 'master' of github.com:GaloisInc/cryptol
2017-10-04 15:50:41 -07:00
Iavor Diatchki
5208739653
Don't print directly to stdout. Fixes #166
2017-10-04 15:50:31 -07:00
Brian Huffman
d025108bd2
Make :browse filter declarations by module name instead of value name.
...
See #396 .
2017-10-04 15:45:25 -07:00
Brian Huffman
2b568897da
Remove implicit Bit type signature on rhs of property declarations.
...
Fixes #224 .
It might be desirable to add some other check for `property` declarations
to make sure that their types are predicates of some arity.
2017-10-04 15:26:17 -07:00
Brian Huffman
3a154f948a
Add regression test for issue #463 .
2017-10-04 13:47:24 -07:00
Brian Huffman
c7380d35d4
Fix symbolic indexing function indexFront to avoid indexing past the end.
...
Previously it would create a lookup table with 2^w entries, where w is
the bit-width of the index. Now the lookup table has min(2^w, n) entries,
where n is the length of the indexed vector.
Fixes #463 .
2017-10-04 13:46:58 -07:00
Brian Huffman
a5a7a393be
Add definitions of SHAKE128 and SHAKE256 to keccak.cry
2017-10-04 10:39:10 -07:00
