Commit Graph

280 Commits

Author SHA1 Message Date
Trevor Elliott
21ab16db4b Add some tests for the mono-binds feature 2014-12-09 12:08:17 -08:00
Trevor Elliott
7dc76662e9 Better partitioning of the monomorphizing code 2014-12-09 12:07:52 -08:00
Trevor Elliott
48d1be1315 Merge branch 'master' into wip/mono-binds 2014-12-09 11:21:01 -08:00
Trevor Elliott
b1eae187e5 Make the cryptol binary depend on the sources
Instead of making the cryptol binary .PHONY, use find to locate all the
sources to depend on.
2014-12-09 11:20:31 -08:00
Trevor Elliott
29448e5789 Merge remote-tracking branch 'origin/master' into wip/mono-binds 2014-12-09 10:40:26 -08:00
Trevor Elliott
7b3fc614bf Remove debugging output 2014-12-08 18:20:32 -08:00
Trevor Elliott
4a0149ed52 Thread a flag through to manage let-generalization
Setting `mono-binds` to `yes` will cause bindings to be made monomorphic when
they don't refer to closed values, and setting `mono-binds` to no will cause
them to always be generalized.
2014-12-08 18:18:14 -08:00
Adam C. Foltzer
abf19641be small tweak to readme wording 2014-12-08 17:30:32 -08:00
Adam C. Foltzer
61e9b4e1fe add pointer to low-hanging fruit issue label 2014-12-08 17:29:26 -08:00
Trevor Elliott
0c22144f55 Test 225 no longer fails, this fixes #5 2014-12-08 16:57:02 -08:00
Trevor Elliott
a8dc88ffaf Merge remote-tracking branch 'origin/master' into wip/mono-binds 2014-12-08 16:46:02 -08:00
Trevor Elliott
f9319b4e9f Updated test output for monomorphic bindings 2014-12-08 16:45:51 -08:00
Trevor Elliott
ed81311a86 Only return changes to the closed environment 2014-12-08 16:35:06 -08:00
Trevor Elliott
55854f2eb0 Make sure to initialize iClosed with the imported environment 2014-12-08 15:58:23 -08:00
Trevor Elliott
b2b27b672f Make sure to pass out the new closed set from inferBinds 2014-12-08 15:57:13 -08:00
Trevor Elliott
907c5f393f Make bindings monomorphic based on use of closed values
Adopt the definition of closed values defined by this post on the ghc blog:

https://ghc.haskell.org/trac/ghc/blog/LetGeneralisationInGhc7
2014-12-08 15:18:40 -08:00
Adam C. Foltzer
7030924083 tweak escaped variable message to be more clear 2014-12-08 14:07:28 -08:00
Brian Huffman
25ee274d38 Merge changes from SBV version 3.3
Includes changes after LeventErkok/sbv@67656c6aba (Nov 3)
and up to LeventErkok/sbv@6468f41bde (Dec 5)
2014-12-08 11:04:28 -08:00
Adam C. Foltzer
9abc779340 update random values after changing random generation 2014-12-05 17:38:00 -08:00
Trevor Elliott
fa104983bd Merge branch 'master' into wip/mono-binds
Conflicts:
	Makefile
	tests/Main.hs
2014-12-05 17:25:56 -08:00
Adam C. Foltzer
969c96e8e1 Don't do fancy progress bars for :check in batch mode 2014-12-05 17:18:29 -08:00
Trevor Elliott
465b0eb103 Add a stdout file for the failing test, issues/T146 2014-12-05 16:52:45 -08:00
Trevor Elliott
b3341c02c9 Allow make test to output the diff results 2014-12-05 16:49:58 -08:00
Trevor Elliott
c2821da104 Make the diff command line absolute 2014-12-05 16:27:08 -08:00
Trevor Elliott
63fe690ef9 Add block decls to the local environment after partitioning 2014-12-05 16:23:51 -08:00
Trevor Elliott
2ea484288e Rename iParams to iLocalEnv 2014-12-05 16:23:26 -08:00
Trevor Elliott
481430ee7d Better partitioning of monomorphic declarations
Partition out declarations that should be monomorphic, based on what they
reference in the environment; declarations that lack signatures but don't
reference anything in the local environment can still be generalized.
2014-12-05 14:27:31 -08:00
Trevor Elliott
b13eb959aa Make the diff command line absolute 2014-12-04 14:36:26 -08:00
Trevor Elliott
80343e7256 Don't generalize bindings in where clauses
A first pass on skipping generalization for bindings in a where clause that
lack type signatures.  The tests that fail as a result of this change are either
because of error locations changing, or a changing number of defaulting
warnings.
2014-12-04 14:21:57 -08:00
Trevor Elliott
ee3647b814 Update renamer errors to clarify some funny situations
This tries to address #125 by making the errors from the renamer a little bit
more clear.

Squashed commit of the following:

commit 8afd3d7961b58df042fe801c3c5e1b9787f813bc
Author: Trevor Elliott <trevor@galois.com>
Date:   Wed Dec 3 19:33:59 2014 -0800

    Update tests for new renamer errors

commit 7cac01836d8943cf3b08d6715ac328e3b6658cef
Author: Trevor Elliott <trevor@galois.com>
Date:   Wed Dec 3 19:33:49 2014 -0800

    Add `at` on errors and warnings to be more consistent

commit 308908ba318a4cdc839710f66f1a487543f8c07e
Author: Trevor Elliott <trevor@galois.com>
Date:   Wed Dec 3 19:06:57 2014 -0800

    More consistent renamer warnings

commit be8100a78e9eaba6d554591121c24ed5dcd3c780
Author: Trevor Elliott <trevor@galois.com>
Date:   Wed Dec 3 18:56:53 2014 -0800

    More consistent error formatting from the renamer

commit 26c45c3b51e0bdbcf6a1431cab8e1eb8760ea0bb
Author: Trevor Elliott <trevor@galois.com>
Date:   Wed Dec 3 18:56:36 2014 -0800

    Remove an un-triggerable error

commit ccdb93e036ba1e111ccd977c8b3b35523f3c1bf0
Author: Trevor Elliott <trevor@galois.com>
Date:   Wed Dec 3 16:38:44 2014 -0800

    Try to give better errors for unbound identifiers

commit eb5784145985bb55c761088eaba27c67d08c1326
Author: Trevor Elliott <trevor@galois.com>
Date:   Wed Dec 3 16:38:23 2014 -0800

    Remove old TODOs about located errors

commit b984bb5f451f3aa7b4fc8f15167483c5142ee9a3
Author: Trevor Elliott <trevor@galois.com>
Date:   Wed Dec 3 14:37:34 2014 -0800

    Differentiate missing type and expression symbols

commit b9e6f13856db6765dced3cb9565cdc8387a7976d
Author: Trevor Elliott <trevor@galois.com>
Date:   Wed Dec 3 14:36:52 2014 -0800

    Remove a shadowing warning
2014-12-03 19:36:06 -08:00
Iavor S. Diatchki
99c3547a08 Record the parameters of the current scheama into fresh variables generated during kind checking. 2014-12-02 15:50:40 -08:00
Iavor S. Diatchki
358d3fc554 Add an example where we can get capture when substituting. 2014-12-02 15:50:40 -08:00
Iavor S. Diatchki
f8c431aee2 Add applicative instances. 2014-12-02 15:50:40 -08:00
Brian Huffman
7420b27785 Add Parser AST constructor EInfFrom to represent [x...] and [x,y...]
As a result, parsed terms including [x...] or [x,y...] now pretty-print
back out using the same syntax.
2014-12-02 14:47:01 -08:00
Brian Huffman
ccfbd1f2de Fix symbolic simulator implementations of (!!) and (@@)
Now these operations correctly set the is-bit flag on
the VSeq constructor when the result type is a list of bits.

Fixes #148.
2014-12-02 14:07:23 -08:00
Brian Huffman
88983488fc Share more code between interpreter and symbolic simulator
Some interpreter/simulator operations are now overloaded using
a newly introduced 'BitWord' type class.
2014-11-13 13:17:31 -08:00
Brian Huffman
6368bcbe38 Make evaluation of lists of bits non-strict in the elements.
This means that e.g. [True, error "foo"]@0 evaluates to True,
similar to how [0x1, error "foo"]@0 evaluates to 0x1.
2014-11-12 13:27:49 -08:00
Brian Huffman
7e099a5236 Speed up implementation of 'width' function
Fixes #139.
2014-11-10 15:45:34 -08:00
Brian Huffman
7adf5b2f6c Speed up lexing of large integer literals
This partially addresses issue #139.
2014-11-10 14:56:29 -08:00
Brian Huffman
0352dca57a Add regression test for github issue #133.
Renamed old "issue133" to "trac133", indicating that it uses a different
numbering system.
2014-11-04 16:10:48 -08:00
Adam C. Foltzer
b05ddd5e54 Partially fixes #73
Due to the limitations of the GHC runtime, we can't get around the
possibility of out-of-memory errors, but we can prevent individual
bitvectors from being too large for the libgmp-backed bignums.

There is now an architecture-dependent check whenever creating a new
`BV` value in the concrete evaluator to ensure the width does not
exceed the GMP limits. If a width is too large, the evaluation returns
to the REPL much like diving by zero.
2014-11-04 14:18:42 -08:00
Adam C. Foltzer
761fb4076d add tests for #73 2014-11-04 14:08:23 -08:00
Adam C. Foltzer
794017ecf5 add guards for bit vector widths during concrete evaluation
Tested on my 64-bit machine; will run tests on Jenkins slaves
2014-11-04 12:11:24 -08:00
Brian Huffman
0a7b39f944 Add regression tests for issue #135. 2014-11-04 12:03:07 -08:00
Brian Huffman
80ec38fcf5 Merge changes from latest version of SBV
Includes changes after LeventErkok/sbv@55a9405954 (Aug 28)
and up to LeventErkok/sbv@67656c6aba (Nov 3)

Fixes #135.
2014-11-04 11:48:02 -08:00
Adam C. Foltzer
9ef8c54919 Working draft of "hacking" document
Merge branch 'feature/issue054'

Closes #54
2014-11-03 11:32:27 -08:00
Adam C. Foltzer
09395fffac add wip branch info to HACKING.md 2014-11-03 11:20:06 -08:00
Brian Huffman
14b9399e33 fix expected test output for issue #128. 2014-10-23 15:02:42 -07:00
Brian Huffman
5ec364680d Add regression test for issue #130. 2014-10-23 15:00:34 -07:00
Thomas M. DuBuisson
f16a297e90 wrt #132 update the expected output for the tests. 2014-10-23 14:28:01 -07:00