David Thrane Christiansen
|
8a9565595b
|
Render each test on a single line
|
2019-03-19 13:26:01 -07:00 |
|
David Thrane Christiansen
|
e064233acd
|
Preliminary support for dumping tests
Fix misspelling in help text
|
2019-03-19 13:25:55 -07:00 |
|
Brian Huffman
|
fc6e6be518
|
Tighten lower interval bounds for /^ operator.
The result of `x /^ y` can never be 0 unless `x` is 0.
|
2019-03-18 18:05:41 -07:00 |
|
Brian Huffman
|
7cb16586d4
|
Add regression test for #581.
|
2019-03-18 15:29:36 -07:00 |
|
Brian Huffman
|
5e8d8d6f80
|
Implement /^ and %^ for intervals. Fixes #581.
|
2019-03-18 15:29:04 -07:00 |
|
Brian Huffman
|
5076273c10
|
Add regression test for issue #582.
|
2019-03-18 14:53:09 -07:00 |
|
Brian Huffman
|
6265cb3b0e
|
Add well-formedness constraints for uses of /^ and %^. Fixes #582.
|
2019-03-18 14:06:04 -07:00 |
|
Aaron Tomb
|
3af02e9599
|
Make GHC 8.6 Cabal freeze file less strict
Now it'll work with 8.6.x
|
2019-03-11 15:16:12 -07:00 |
|
Aaron Tomb
|
361e052a78
|
Bump SBV version in Cabal freeze files
|
2019-03-11 12:21:23 -07:00 |
|
Aaron Tomb
|
be13fedb65
|
Merge pull request #580 from LeventErkok/master
Changes required to compile Cryptol with SBV 8.1; and model-validation support
|
2019-03-11 12:20:41 -07:00 |
|
Aaron Tomb
|
600b5ec049
|
Update path for cryptol-specs in .gitmodules
|
2019-03-11 12:13:08 -07:00 |
|
Levent Erkok
|
375166d06f
|
Add a prover-validate flag and pass it to SBV (default: off)
This should address the issue reported in https://github.com/GaloisInc/cryptol/issues/558
|
2019-03-09 13:44:20 -08:00 |
|
Levent Erkok
|
f3a26e24b7
|
Undo changes for elapsed time bug workaround
SBV 8.1 prints the time correctly, so this workaround isn't needed
Fixes https://github.com/GaloisInc/cryptol/issues/572
|
2019-03-09 13:27:35 -08:00 |
|
Levent Erkok
|
cbdf7c696a
|
Make cryptol compile with SBV 8.1
|
2019-03-09 13:26:41 -08:00 |
|
Brian Huffman
|
dc48fedcbc
|
Reimplement symbolic updates more efficiently. Fixes #579.
|
2019-03-04 18:07:33 -08:00 |
|
Brian Huffman
|
0db6a86f73
|
Fix typos in comments.
|
2019-03-04 18:05:23 -08:00 |
|
Aaron Tomb
|
1548d2ecf4
|
Remove deleted examples from Makefile
|
2019-03-04 11:16:50 -08:00 |
|
Brian Huffman
|
9584fdb54d
|
Remove some duplicate files from /examples that were also in cryptol-specs.
See #571.
|
2019-03-01 18:34:23 -08:00 |
|
Brian Huffman
|
acafb2952d
|
Add cryptol-specs as git submodule under /examples.
|
2019-03-01 18:05:28 -08:00 |
|
Iavor Diatchki
|
a33ddf1ae3
|
Improvements to edit/reload logic.
See #578 for details.
|
2019-03-01 17:25:43 -08:00 |
|
Iavor Diatchki
|
afe89d2ad4
|
Add examples of doing record updates
|
2019-03-01 11:10:28 -08:00 |
|
Iavor S. Diatchki
|
139c7d50ac
|
Merge pull request #576 from GaloisInc/fingerprints
Track file content fingerprints alongside loaded modules
|
2019-02-28 11:02:27 -08:00 |
|
Brian Huffman
|
6b53cd0c2f
|
Fix typo in documentation.
|
2019-02-28 10:46:41 -08:00 |
|
brianhuffman
|
f8aca88d9d
|
Merge pull request #575 from GaloisInc/wip/no-from-then
Remove [x..] syntax.
|
2019-02-28 10:42:38 -08:00 |
|
Brian Huffman
|
e59c9abfbb
|
Remove [x..] and [x,y..] syntax from documentation.
|
2019-02-28 10:38:38 -08:00 |
|
Eric Mertens
|
5e75f834e7
|
Update test for new utf-8 error message
|
2019-02-28 10:04:17 -08:00 |
|
Eric Mertens
|
5786fcf190
|
Track file content fingerprints alongside loaded modules
|
2019-02-28 09:40:21 -08:00 |
|
Brian Huffman
|
7ea4884fdd
|
Remove unused primitive type operator lengthFromThen.
|
2019-02-27 17:11:18 -08:00 |
|
Brian Huffman
|
24fb6c9511
|
Remove unused primitive fromThen.
|
2019-02-27 16:57:00 -08:00 |
|
Brian Huffman
|
61a17adb02
|
Remove [x..] and [x,y..] syntax from Cryptol.
|
2019-02-27 16:36:53 -08:00 |
|
Brian Huffman
|
c387dbe5fd
|
Remove all uses of [x..] syntax from examples and tests.
|
2019-02-27 16:25:53 -08:00 |
|
Aaron Tomb
|
00b58277bb
|
Update AppVeyor configuration
|
2019-02-25 16:06:01 -08:00 |
|
Aaron Tomb
|
8ed4dad321
|
Update Travis for GHC 8.6
|
2019-02-22 17:06:36 -08:00 |
|
Iavor Diatchki
|
6a8c6c3134
|
Update Syntax.md and re-sync it with Syntax.tex
Note that Syntax.tex should be generated automatically
|
2019-02-18 17:20:01 -08:00 |
|
Iavor Diatchki
|
1b780c21e1
|
Merge branch 'master' into rec-upd
|
2019-02-17 18:51:20 -08:00 |
|
Iavor Diatchki
|
9ad5568332
|
Fixup function notation in records
|
2019-02-17 18:45:50 -08:00 |
|
Iavor Diatchki
|
cf7d97fcaf
|
Reference implementation of updates.
|
2019-02-17 18:01:27 -08:00 |
|
Iavor Diatchki
|
631a56c558
|
Concrete evaluation
|
2019-02-17 17:48:54 -08:00 |
|
Iavor Diatchki
|
41f09183f5
|
Create updating dictionaries
|
2019-02-17 17:17:00 -08:00 |
|
Iavor Diatchki
|
9ae35253eb
|
Type checking done (except evidence) + fixes prinintg + filling missing cases
|
2019-02-16 17:15:03 -08:00 |
|
Iavor Diatchki
|
82ce40f0b6
|
Replace undefined with error to tell them apart (these are temporary)
|
2019-02-16 13:08:46 -08:00 |
|
Iavor Diatchki
|
9ca6ac7a82
|
Parsing of nested field updates
|
2019-02-16 13:08:19 -08:00 |
|
Iavor Diatchki
|
d0c2285b74
|
Do most of the desugaring for record updates in the renamer
XXX. Perhaps we should just handle { _ | x = e } here too?
|
2019-02-16 13:07:51 -08:00 |
|
Iavor Diatchki
|
ff81ea4095
|
This should correct issue #572
We should leave the ticket open until we figure out if this is actually
a bug in SBV, as the API it exposes is quite odd.
|
2019-02-14 14:11:40 -08:00 |
|
Iavor Diatchki
|
1dafdb77c6
|
Renamer changes for update
|
2019-02-12 17:07:29 -08:00 |
|
Iavor Diatchki
|
50f82a02d3
|
Basics of setting a single field.
|
2019-02-12 16:40:43 -08:00 |
|
Iavor Diatchki
|
fbe1c8c7a7
|
Generalize the dictionary for HasGoal to support multiple methods.
Also get started on selectors, but that's incomplete.
|
2019-02-12 16:24:52 -08:00 |
|
Iavor Diatchki
|
ea7f95e37d
|
Add a new constructor for updating records to the intermediate language.
|
2019-02-12 16:24:08 -08:00 |
|
Iavor Diatchki
|
895f69f1c3
|
Fix parser error
|
2019-02-12 14:56:03 -08:00 |
|
Iavor Diatchki
|
40642ff43e
|
Merge branch 'master' into rec-upd
|
2019-02-12 14:48:14 -08:00 |
|