Brian Huffman
fd4415803a
Fix compiler warnings
2017-03-09 10:27:20 -08:00
Iavor S. Diatchki
fddcd60d10
Merge branch 'master' of github.com:GaloisInc/cryptol
2017-02-23 15:22:40 -08:00
Iavor S. Diatchki
174bb3c20a
Remove ECast
...
The invariant that this used to ensure does not hold anymore, so
it was more confusing than not to have it.
2017-02-23 15:18:05 -08:00
Iavor S. Diatchki
1d8f2576c8
Add a deriving Eq on Schemas.
...
The equality is completely syntactic.
2017-02-17 11:38:51 -08:00
Iavor S. Diatchki
41131fe7ed
Redo the export to SMT story in a much simpler way.
2017-02-16 16:46:38 -08:00
Iavor S. Diatchki
de770d5aed
Remove warnings.
2017-02-15 11:31:30 -08:00
Iavor S. Diatchki
866722956b
Fall back to old solver, if all else fails.
2017-02-15 11:29:03 -08:00
Iavor S. Diatchki
27eaec689d
Fix test. There is indeed defaulting that should be happening here.
2017-02-15 10:02:15 -08:00
Iavor S. Diatchki
e30b1e7cd3
Wibble
2017-02-15 10:01:57 -08:00
Iavor S. Diatchki
68303fb958
Prefere errors that do not mention unificaion variables.
2017-02-15 09:08:38 -08:00
Iavor S. Diatchki
5e1a3b6f5a
This one works now.
2017-02-15 09:08:15 -08:00
Iavor S. Diatchki
ec58bec6aa
Add .cryptolsrc files
2017-02-15 09:08:02 -08:00
Brian Huffman
091894fc9d
Update reference interpreter to handle run-time errors explicitly
...
The :eval command should never throw an actual run-time exception;
instead, errors are represented alongside bits in the value datatype,
and errors are printed wherever they appear inside the result value.
2017-02-10 13:35:15 -08:00
Iavor S. Diatchki
9d9f9a8de7
Hack, hack. Pass context to solver after defaulting.
...
The structure of all this should be fixed.
2017-02-08 19:00:00 -08:00
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
