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
Iavor Diatchki
fd67463b2b
Add a hacky way to get local executable path
2019-02-12 14:38:17 -08:00
Brian Huffman
244848326c
Special case for svFromInteger at bit width 0. Fixes #563 .
...
This change ensures that `fromInteger x : [0]` is concrete,
even if `x` is symbolic.
2019-02-11 10:57:29 -08:00
Brian Huffman
b1edb9e36e
No more rebindable syntax. Fixes #568 .
...
When syntactic sugar for constants "negate", "complement" or "splitAt"
is used, the names of those primitives are now resolved during the
type checking phase. This makes them consistent with the handling of
other desugared primitives like "fromThen", etc.
2019-02-08 09:56:37 -08:00
Aaron Tomb
10e87616a2
Update frozen versions of crackNum
2019-02-01 08:51:16 -08:00
Aaron Tomb
016395f403
Update frozen versions of crackNum
2019-02-01 08:24:32 -08:00
Aaron Tomb
8ed77c130d
Update SBV version in Cabal freeze files
2019-02-01 08:16:44 -08:00
