GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-12-17 21:11:35 +03:00
Code Issues Projects Releases Wiki Activity
736 Commits 67 Branches 28 Tags 95 MiB
09847cab01
Commit Graph

736 Commits

This Branch
This Branch
All Branches
Author SHA1 Message Date
Iavor S. Diatchki
09847cab01 Rewrite div equalities as multiplication 2015-08-11 09:21:38 -07:00
Trevor Elliott
4874ad0d6e Make fewer calls to addToComment 2015-08-10 15:04:15 -07:00
Brian Huffman
c9a57766be Use custom applicative functor to speed up interpreter on list comprehensions 2015-08-10 12:19:09 -07:00
Brian Huffman
e5e190a138 Fix typos in comments 2015-08-10 09:22:03 -07:00
Brian Huffman
97a3983077 Optimize evaluation of list comprehensions in Cryptol interpreter 
To avoid doing so many map unions, the evaluation function for list
comprehensions now produces a map containing lists of values instead
of a list of maps.
 2015-08-07 17:51:25 -07:00
Brian Huffman
59df701c57 Optimize append operator (#) on bitvectors. 
The interpreter no longer converts bitvectors to lists of bits before
appending them together.
 2015-08-07 13:44:30 -07:00
Trevor Elliott
24cb45c4ea Merge pull request #266 from msaaltink/issue-258 
Fix for issue #258 (incude of literate file fails)
 2015-08-05 18:35:06 -07:00
Mark Saaltink
cf0e58042c Fix for issue-258 (incude of literate file fails) 2015-08-05 21:25:32 -04:00
Adam C. Foltzer
eac8c9a5f7 Merge pull request #263 from nbraud/master 
README.md: Trivial fixes
 2015-07-29 09:40:40 -07:00
Adam C. Foltzer
d2393de268 add server flag to deps install step 2015-07-28 13:30:20 -07:00
Nicolas Braud-Santoni
3f8cde4eae README.md: Trivial fixes 2015-07-26 15:56:05 +02:00
Daniel Wagner
9d1e1a4c5e instead of deleting bindings at the end of specializing a declaration group, restore them to their previous values 2015-07-23 18:12:00 -07:00
Daniel Wagner
a958ce3328 regression test for a specializer bug 2015-07-23 18:08:14 -07:00
Brian Huffman
75fe508370 More efficient implementation of symbolic indexing. Fixes #250. 2015-07-22 11:14:14 -07:00
Adam C. Foltzer
7e674d0c07 Merge pull request #262 from ntc2/master 
Only require cryptol-server's build depends when it's being built. Workaround for https://github.com/haskell/cabal/issues/1725
 2015-07-22 10:58:26 -07:00
Nathan Collins
7c52103fab Only require cryptol-server's build depends when it's being built. 
By moving `build-depends` under the `if flag(server)` check. The diff
is a little hard to read, because I did not change the indentation of
the dependencies. Thanks @elliottt for the fix!
 2015-07-22 09:22:15 -07:00
Adam C. Foltzer
0d61ed14c3 Merge branch 'feature/cryptol-server' 
Brings the JSON over ZeroMQ server into the main line of development. It
is disabled by default, but there is now a `server` flag in
`cryptol.cabal` that in turn gets enabled if the `CRYPTOL_SERVER`
environment variable is nonempty during `make`.
 2015-07-21 13:20:41 -07:00
Adam C. Foltzer
900e4acf8b clean up cryptol-server for merging 2015-07-21 11:52:17 -07:00
Adam C. Foltzer
a6a62ea656 put counterexamples and sat assignments in replies 2015-07-13 16:02:38 -07:00
Adam C. Foltzer
96a2cf2e44 refactored sat/prove code for non-console clients 2015-07-10 18:19:53 -07:00
Adam C. Foltzer
ce5bbe9f8a squish some warnings 2015-07-10 18:19:46 -07:00
Adam C. Foltzer
d7cf61f8e0 add pretty-printing to some server replies 2015-07-10 18:19:30 -07:00
Adam C. Foltzer
89b4567b93 add missing cryptol-server directory 2015-07-08 18:01:22 -07:00
Adam C. Foltzer
d5aff31d64 remove unnecessary import 2015-07-08 13:58:29 -07:00
Adam C. Foltzer
dbb41dd646 fold server into main Cryptol package 
once merged, we'll disable the build by default so we don't incur the
zeromq dependency, but it would be nice to eventually make the server
the core of all our clients
 2015-07-07 18:13:34 -07:00
Thomas M. DuBuisson
6a7477ba6c Half-fix but not quite issue #256 (Bool ~> Bit). 
We should probably discuss why we want to call things "Bool" if this was
more concious than incidental.  That and change the documentation to
match.
 2015-07-03 14:19:56 -07:00
Adam C. Foltzer
2bb86303bb add proper MonadIO instance for REPL 2015-07-01 12:37:51 -04:00
Adam C. Foltzer
f22cbdc4eb more exports 2015-07-01 12:37:51 -04:00
Adam C. Foltzer
53201d7ac3 additional exports for cryptol-server 2015-07-01 12:37:51 -04:00
Adam C. Foltzer
494bf6d92e tweak patch in 170e5953 to work for 7.8; add test 2015-07-01 12:31:37 -04:00
Trevor Elliott
170e59530b Resolve includes relative to the file that includes them 
Fixes #202
 2015-06-30 10:54:18 -07:00
Trevor Elliott
034f7d12dd Fix a potential problem with infixr type operators 2015-06-30 10:31:13 -07:00
Trevor Elliott
3117d07a79 Observe parens when resolving type operators 
Fixes #254
 2015-06-30 10:19:45 -07:00
Trevor Elliott
fafaf4ca26 Fix right-associative nesting for expressions 2015-06-29 16:54:58 -07:00
Trevor Elliott
4d469fa2ce Update test output 2015-06-29 16:34:11 -07:00
Trevor Elliott
398f5d7196 Fix fixity resolution 
Resolve fixity bottom-up, to allow low-precedence operators the chance to bubble
all the way out.
 2015-06-29 16:00:36 -07:00
Brian Huffman
458c547d5b ListSel on VWord in symbolic backend uses correct endian-ness. 
Fixes #251.
 2015-06-26 14:09:29 -07:00
Aaron Tomb
55154aff2b Allow use of Cabal 1.18 during build 
This eases the build using Stack and GHC 7.8, since GHC 7.8 comes with
Cabal 1.18.
 2015-06-26 13:45:26 -07:00
Iavor S. Diatchki
c791669c76 Fix typo 2015-06-25 10:59:30 -07:00
Iavor S. Diatchki
8fe9bcba08 Correct the rule for equality with constant on division 2015-06-24 14:33:01 -07:00
Iavor S. Diatchki
e7728c2b22 Add a case for Not. Fixes #249. 
This may happen when we check enumerations, because we emit constraints
such as `x /= y`, which ends up looking like `Not (x == y)`.
 2015-06-24 11:34:20 -07:00
Iavor S. Diatchki
91ebb1ca2b Make fin decisions first. 2015-06-24 11:19:52 -07:00
Iavor S. Diatchki
c4c587d14b Add missing case for max. 
Apparently this got lost at some point!
 2015-06-22 15:00:14 -07:00
Iavor S. Diatchki
6785d7078c Print some information, even if there is no doc comment 2015-06-22 11:23:40 -07:00
Iavor S. Diatchki
74714f3071 Fixup/changes to parsing comments 
This addresses some issues where things like /**** were parsed as an
operator, leading to parse errors with some comments.  The intended
behavior is as follows:

  1. /* with no more stars starts a normal block comment
  2. /**+ (i.e., 2 or more starts) starts a document comment
  3. *+/  (i.e., any number of stars, follwed by /) ends any comment
  4. /*+/ is a block coment (e.g., /*******/) is a block comment
 2015-06-22 11:23:22 -07:00
Iavor S. Diatchki
8429d294e6 Add a test for multi-if 2015-06-22 09:25:45 -07:00
Iavor S. Diatchki
8e1f8f5b68 Merge branch 'master' of github.com:GaloisInc/cryptol 2015-06-22 09:20:16 -07:00
Iavor S. Diatchki
6ddec6d128 Reverse alternatives in multi-way if. 
Fixes #245
 2015-06-22 09:20:08 -07:00
Trevor Elliott
5ff6005bed Allow operators to use '\' 
Fix #246
 2015-06-21 01:53:52 +01:00
Iavor S. Diatchki
efc4443707 Remove some unused code. See Cryptol.TypeCheck.AST.tSplitFun for the same. 
XXX: more of this probably shoul go away
 2015-06-19 16:13:18 -07:00