GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-12-17 21:11:35 +03:00
Code Issues Projects Releases Wiki Activity
1,252 Commits 67 Branches 28 Tags 95 MiB
b5d6715b21
Commit Graph

1252 Commits

This Branch
This Branch
All Branches
Author SHA1 Message Date
Iavor S. Diatchki
f6a4aef4cc A more readable version of (possibly?) the same code 2017-02-08 18:59:24 -08:00
Iavor S. Diatchki
a8ddf035f2 Lookup variables in the interval map 2017-02-08 18:59:05 -08:00
Iavor S. Diatchki
2c3145a417 Fix some of the broken tests. 2017-02-08 17:24:15 -08:00
Iavor S. Diatchki
424d02eb27 Fix copy-paste error in normalization of LenFromThenTo 2017-02-08 16:30:04 -08:00
Iavor S. Diatchki
568a26b9aa Restore functionality of Panic 2017-02-08 16:29:45 -08:00
Iavor S. Diatchki
3c15d086d1 Merge branch 'master' into wip/solver 2017-02-08 16:24:46 -08:00
Iavor S. Diatchki
8c19abb452 Merge branch 'master' of github.com:GaloisInc/cryptol 2017-02-08 16:19:00 -08:00
Iavor S. Diatchki
6bef779780 Add a flag to control if batch execution stops on the first error or not. 
This is off by default.
 2017-02-08 16:18:50 -08:00
Iavor S. Diatchki
fa37734956 Add a flag to control if we show prover timing stats or not. 2017-02-08 16:08:20 -08:00
Iavor S. Diatchki
3c2c9a857a Fix test to account for printing of operators' precedences. 2017-02-08 16:07:54 -08:00
Iavor S. Diatchki
710355176a More rules and things; external solver disabled; we can at least load ChaCha 2017-02-08 15:08:50 -08:00
Iavor S. Diatchki
90c6adbfcd Goals as Sets works again. 2017-02-03 17:10:50 -08:00
Iavor S. Diatchki
336ea625b0 In InferM types don't contain thunks. 2017-02-03 15:56:19 -08:00
Iavor S. Diatchki
44085b4c5d Keep maintaining evaluated invariant 2017-02-03 14:21:24 -08:00
Iavor S. Diatchki
5ebf13212a Remove extra layer of simplification. 
We should not be inferring unevaluated types.

XXX: The whole ECast story is probably broken now, as we evaluate substitutions
directly, but we don't do the corresponding rewrites on terms.

XXX: Do we need ECast at all?
 2017-02-03 13:52:33 -08:00
Iavor S. Diatchki
5c3a258d7f Rewrites for some more common cases 2017-02-03 13:25:42 -08:00
Iavor S. Diatchki
984108b68d Move simplification of types into SimpleSolver + some quick eqn rewrites. 2017-02-03 12:13:39 -08:00
Brian Huffman
140ab21f11 Add new unoptimized reference interpreter; use in REPL with ":eval <expr>" 2017-02-03 09:02:25 -08:00
Brian Huffman
44692d1f33 Fix typos in comments 2017-02-03 09:00:14 -08:00
Brian Huffman
f0e3ca2d69 Simplify shifter function; eliminate compiler warnings. 2017-02-02 10:37:37 -08:00
Iavor S. Diatchki
18ac6507ef Remove unused stuff, and define more reasonable comparisons on types. 2017-02-01 15:00:49 -08:00
Iavor S. Diatchki
f3db823f3e Checkpoint: (broken, but builds) 2017-02-01 11:43:01 -08:00
Aaron Tomb
13b704f840 Remove references to sbv repository 2017-02-01 09:09:59 -08:00
Iavor S. Diatchki
b788079244 More aggressive goal simplification. 2017-01-31 14:12:53 -08:00
Iavor S. Diatchki
12bb2c30c8 Merge branch 'master' into wip/solver 2017-01-31 10:15:49 -08:00
Iavor S. Diatchki
ee1c8c796b Switch to using the official sbv release. 2017-01-31 10:04:34 -08:00
Iavor S. Diatchki
baa19ce362 Checkpoint. 2017-01-30 18:14:10 -08:00
Iavor S. Diatchki
9bb61ec9a2 Add PTrue and Error to the syntax (not yet used) 2017-01-30 10:55:08 -08:00
Iavor S. Diatchki
c3ce33f5a6 Remove old stuff 2017-01-30 10:54:45 -08:00
Iavor S. Diatchki
10cf6f16e3 Print stats about the prover. Fixes #392 2017-01-27 16:14:37 -08:00
Iavor S. Diatchki
ecdb774abb Show information about precedence and fixity in the operator help. Fixes #391 2017-01-27 10:59:17 -08:00
Iavor S. Diatchki
09dc9b4655 Distinguish success and failure when returning to the OS. Fixes #390 
Currently we only distinguish between success and failure, but in the
future we could add more error codes if that would be useful.

XXX: Mostly the code is written to return an `CommandExitCode` and then
exit at the top level, but there are a few functions that exit directly
(e.g., the setup function).  It would be nice to clean that up.
 2017-01-27 10:37:20 -08:00
Brian Huffman
08a7982a46 Use correct default value for symbolic indexing. Fixes #388. 
We now use the zero value of the element type as the
default; previously we were incorrectly using the zero
value of the *index* type.
 2016-12-13 17:40:57 -08:00
Robert Dockins
e48f430b30 Fix a mismatch when eta-expanding infinite streams that was 
causing Cryptol to panic.  We now expect the `TVStream` type
constructor when eta-expanding streams, which is correct.

Fixes #386
 2016-11-17 18:15:58 -08:00
Robert Dockins
5b502eccd7 Fix the concrete implementation of the 'pdiv' and 'pmod' primitives 
to correctly handle the special case where the length of the dividend
is less than the degree of the divisor polynomial. In this special case
the quotient is always zero and the remainder is equal to the dividend
(zero extended if necessary to fit the output type).

Fixes #384
 2016-10-04 15:15:56 -07: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
Brian Huffman
2300a73a76 Add regression test for issue #382. 2016-09-20 11:25:01 -07:00
Brian Huffman
d895c97c8b expect* functions use correct argument order for mismatch 
The `Type` argument is always the "expected" type (not the
"inferred" type) and so it should be the first argument to
`TypeMismatch` or `unify`.

Fixes #382.
 2016-09-20 11:24:24 -07:00
Brian Huffman
6c2f0fc399 Fix typo: "defintion" -> "definition" 2016-09-20 10:22:16 -07:00
Brian Huffman
0c116c5fa7 Show missing/unexpected field names on type mismatch errors 
Fixes #357.

However, sometimes it shows the types in the wrong order
due to issue #382.
 2016-09-20 09:39:00 -07:00
Brian Huffman
7ccea5dd98 Rename function "endComent" to "endComment" 2016-09-19 15:20:33 -07:00
Brian Huffman
22bb49b3b5 Add regression test for issue #368. 2016-09-19 11:57:06 -07:00
Brian Huffman
60fd82f22b Allow *,+,-,!,^^ to be defined with infix patterns. 
Now the declaration "x * y = rhs" can be used to define
a function named (*) without causing a parse error.

Note that "x # y = rhs" cannot be used to define (#),
as it parses as a pattern binding that defines x and y.

Fixes #368.
 2016-09-19 11:56:42 -07:00
Brian Huffman
6247faa2c8 Add '.' and ':' to the set of allowable operator symbols. 
This fixes part of #368.
 2016-09-19 11:50:30 -07:00
robdockins
7a4cbc8e03 Merge pull request #374 from thoughtpolice/fix-terminal-use 
Fix up terminal title usage and color output
 2016-09-15 09:51:58 -07:00
Brian Huffman
6d6a6ca90c Preserve parens when parsing list enumeration arguments. 
List enumeration arguments are parsed as expressions and
then converted to types afterward. Previously parenthesis
productions were dropped; e.g. "[1..(2+2)*(3+3)]" was
parsed as "[1..2+2*3+3]" before resolving infix precedence.
This is now fixed.

Fixes #379.
 2016-09-14 15:13:38 -07:00
Robert Dockins
a048690e3a Use more efficent algorithms based on barrel-shifters for implementing 
shifts and rotates in the symbolic backend.
Fixes #376
 2016-08-25 12:04:58 -07:00
Robert Dockins
14af3690c6 Update the SIV example to avoid issue #375. 2016-08-23 14:08:15 -07:00
Robert Dockins
cd9ffed00b Update examples to use (/\) instead of (&&) where appropriate, 
and to squash other warnings related to the upcomming precedence change.
 2016-08-22 18:14:44 -07:00
Robert Dockins
e9c8b6ccd1 Add regression test for bitshift operations 2016-08-22 15:36:16 -07:00