Iavor Diatchki
a9edd7a389
Merge branch 'master' of github.com:GaloisInc/cryptol
2017-10-03 10:53:45 -07:00
Iavor Diatchki
234615e7b2
Add some comments
2017-10-03 10:53:40 -07:00
Rob Dockins
f02a3c783b
Bump simple-smt version bounds to pull in a bug fix.
...
Fixes #457
2017-10-03 10:20:15 -07:00
Rob Dockins
d32f3324c9
Update syntax reference with new fixity information for (||) and (&&)
2017-10-02 18:17:38 -07:00
Rob Dockins
e7d3ed02f9
Add testcase for issue #389 .
...
Recent improvements to the numeric solver have fixed this issue.
Fixes #389 .
2017-10-02 18:15:02 -07:00
Rob Dockins
42064dd9f2
Add testcase for issue #325 .
2017-10-02 17:49:12 -07:00
Rob Dockins
37f9dc4c4f
Add test for issue #78 .
...
Fixes #78 .
2017-10-02 15:48:51 -07:00
Iavor Diatchki
a233084db8
Merge branch 'master' of github.com:GaloisInc/cryptol
2017-10-02 15:47:23 -07:00
Rob Dockins
d5bfb1b648
Minor update to test suite
2017-10-02 15:40:46 -07:00
Rob Dockins
c0699e2d62
Change the fixity levels of (||) and (&&).
...
This advances the next step in the plan described in issue #241 .
2017-10-02 14:56:33 -07:00
Rob Dockins
2894a1fdef
Make solver startup/shutdown exception-safe.
2017-10-02 14:06:44 -07:00
Rob Dockins
12ac2c383a
Revert "Remove the Data.Sequence-based representation of unpacked bitsequences."
...
This may improve performace on some examples.
This reverts commit d4b70a039a
2017-10-02 11:12:50 -07:00
Brian Huffman
940b9c80ec
Merge branch 'integer'
2017-09-29 14:23:28 -07:00
Brian Huffman
5e4d094eb3
Fix test output due to counterexample printing change.
2017-09-29 14:23:18 -07:00
Aaron Tomb
da1ff8f225
Merge pull request #454 from madnight/patch-1
...
Update copyright notice year from 2016 to 2017
2017-09-29 10:59:16 -07:00
Brian Huffman
3fb74f7f60
Make :check and :exhaust print counterexamples the same way :prove does.
...
This addresses the first part of issue #449 .
2017-09-29 10:19:56 -07:00
Iavor Diatchki
fe88d98213
Merge branch 'master' of github.com:GaloisInc/cryptol
2017-09-29 09:44:42 -07:00
Brian Huffman
7be06d803e
Fix typo in error message.
2017-09-29 09:28:46 -07:00
Iavor S. Diatchki
75ca6b7fa2
Say something if name does not refer to anything
2017-09-28 15:47:23 -07:00
Iavor S. Diatchki
aa44dd7860
Add support for docstrings on type things
...
See #456
2017-09-28 14:39:22 -07:00
Brian Huffman
d9cbfd62d1
Add instance Zero Integer.
2017-09-28 13:26:01 -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
7e34c25e4d
Switch to infix syntax for blocks and padding operators.
...
"x /^ y" is x/y rounded up, i.e. the least n such that x <= y*n.
"x %^ y" is the least k such that x+k is a multiple of y.
For comparison,
"x / y" is x/y rounded down, i.e. the greatest n such that x >= y*n.
"x % y" is the least k such that x-k is a multiple of y.
The new syntax is much more suggestive of the relation to "/" and "%".
2017-09-28 10:26:31 -07:00
Brian Huffman
defadf8730
Fix cut-and-paste error.
2017-09-28 09:45:40 -07:00
Brian Huffman
1e41541405
Let type checker discharge fin (blocks x y) and fin (padding x y).
...
Both of these type operators are always either finite or undefined.
2017-09-28 09:28:07 -07:00
Fabian Beuke
ab75f152d1
Update copyright notice year from 2016 to 2017
2017-09-28 16:18:00 +02:00
Brian Huffman
f04908a551
Adapt example code to use new blocks and padding operators.
2017-09-27 13:55:55 -07:00
Brian Huffman
9bc6d02019
Implement blocks and padding operators for numeric types.
...
The design is as described in issue #96 :
blocks msgLen blockSize = the least n such that msgLen <= blockSize * n
padding msgLen blockSize = least k such that msgLen + k divides blockSize
or alternatively:
msgLen + padding msgLen blockSize = blocks msgLen blockSize * blockSize
2017-09-27 13:43:26 -07:00
Iavor Diatchki
aab03be26a
More wibbles
2017-09-27 10:24:30 -07:00
Iavor Diatchki
208119fbbf
Merge branch 'master' of github.com:GaloisInc/cryptol
2017-09-27 10:17:06 -07:00
Iavor Diatchki
6018af3537
Just documentation
2017-09-27 10:16:58 -07:00
brianhuffman
c32d68dade
Merge pull request #445 from GaloisInc/logic-class
...
Introduce a `Logic` class for bitwise logical operations
2017-09-27 09:10:47 -07:00
Brian Huffman
1ed5640339
Merge branch 'master' into logic-class
...
# Conflicts:
# tests/mono-binds/test05.icry.stdout
2017-09-26 16:50:53 -07:00
Iavor Diatchki
60523d5986
Delete old solver stuff.
...
The main user visible effect of this might be that sometime things on
the Cryptol command line are instantiated in a slightly different way:
we get `inf` sometimes when we got a finite example before.
We could work around this if it is an issue, but I am not sure which
behavior is more reasonable.
2017-09-26 14:02:52 -07:00
Brian Huffman
36f8fff3ca
Support Integer type in reference evaluator (:eval).
2017-09-22 15:45:43 -07:00
Iavor Diatchki
0cc5151e6d
Correct the handling of TCAnd in the SMT translation
2017-09-22 10:43:02 -07:00
Brian Huffman
1d71fa141c
Merge branch 'master' into integer
2017-09-21 17:05:00 -07:00
Brian Huffman
d545abceec
Fix incomplete pattern match warning caused by merge.
2017-09-21 16:47:36 -07:00
Brian Huffman
2c4157ecd4
Merge branch 'master' into logic-class
2017-09-21 16:44:39 -07:00
Brian Huffman
2ce1ca3eca
Change constraint synonym syntax from "constraint" to "type constraint".
...
For example:
type constraint NonZero n = (fin n, 1 <= n)
last : {n, a} NonZero n => [n]a -> a
last xs = xs!0
2017-09-21 13:21:51 -07:00
Brian Huffman
393a11e170
Implement constraint synonyms ( #373 ).
...
The syntax is just as described in ticket #373 : We have a new
declaration form consisting of the keyword 'constraint' followed
by a identifier and optionally a list of type parameters; the
right-hand side is either a single constraint or a parenthesized,
comma-separated list of type constraints. For example:
constraint NonZero n = (fin n, 1 <= n)
last : {n, a} NonZero n => [n]a -> a
last xs = xs!0
2017-09-21 09:40:22 -07:00
Brian Huffman
c4af07a053
Remove unused TokenKW constructors.
2017-09-20 11:38:36 -07:00
Brian Huffman
b4cf793e7f
Adapt fastSchemaOf function to avoid simplifying when instantiating props.
...
Previously, checking the type of e.g. "(&&) `{[2]b}" would not return
"(Logic [2]b) => [2]b -> [2]b -> [2]b" as expected, but
"Logic b => [2]b -> [2]b -> [2]b". This made it impossible to reconstruct
the instances necessary to produce the required Logic dictionary when
translating to saw-core.
2017-09-18 15:54:35 -07:00
Brian Huffman
c6db409837
Add type-matching functions pIsZero and pIsLogic.
2017-09-15 21:50:21 -07:00
Brian Huffman
35423d0243
Update test output.
2017-09-15 16:38:03 -07:00
Brian Huffman
b03f1ae0c2
Add class Zero with zero :: {a} (Zero a) => a.
...
Shift operators also have a `Zero` constraint on the element type.
2017-09-15 16:37:44 -07:00
Brian Huffman
860060c085
Fix test output.
2017-09-15 14:05:27 -07:00
Brian Huffman
a52510e56b
Add 'Logic' class constraints to Cryptol::Extras
2017-09-15 13:38:43 -07:00
Brian Huffman
d1305b2860
Add 'Logic' typeclass with operations complement, &&, ||, ^, zero.
...
Left and right shift operations also gain a Logic constraint,
since they shift in zero values.
2017-09-15 13:33:56 -07:00
Brian Huffman
571d186c6c
Support toInteger/fromInteger with symbolic arguments in :prove/:sat.
2017-09-14 17:51:03 -07:00
