Aaron Tomb
254283f7cb
Document configuration of support files
...
Now README.md describes how to tell Cryptol where to find the Prelude
and Z3 configuration files that it needs.
2017-03-21 09:14:09 -07:00
Aaron Tomb
77db35ffda
Document success and error exit codes.
2017-03-21 09:08:48 -07:00
Aaron Tomb
c025f874db
Document the prover-stats option.
2017-03-21 09:06:18 -07:00
Aaron Tomb
aa900df04c
Set user option if exact match, even if prefix
...
The `:set` command wasn't allowing `prover` as a key, since
`prover-stats` also exists. Now it allows an exact match even if it's a
prefix of some other option. To set `prover-stats` or a similar option,
spell it out more completely.
2017-03-21 09:04:17 -07:00
Trevor Elliott
d174ac38ba
Remove transformers-compat and crackNum in the GHC710 config
2017-03-13 16:04:36 -07:00
Trevor Elliott
28d24c151b
Remove QuickCheck from the GHC710 stackage snapshot
2017-03-13 15:54:14 -07:00
Trevor Elliott
5fc47c8dab
Remove monadLib and simple-smt from stackage snapshots
2017-03-13 15:51:28 -07:00
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
