Trevor Elliott
7e1ad7d970
Remove cryptol from the stackage snapshots
2017-03-13 15:50:00 -07:00
Trevor Elliott
302e48068d
Update stackage snapshots
2017-03-13 14:23:25 -07:00
Brian Huffman
4c45e1ba62
Update haddock comments
2017-03-09 11:24:09 -08:00
Brian Huffman
f8290af910
Fix haddock parse errors
2017-03-09 10:58:55 -08:00
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
