Commit Graph

15 Commits

Author SHA1 Message Date
Robert Dockins
998bddc7a7 Merge remote-tracking branch 'origin/master' into new-eval
Fix some minor conflicts in the test suite.
Conflicts:
	tests/issues/issue002.icry.fails
	tests/issues/issue148.icry.stdout
	tests/issues/issue198.icry.stdout
	tests/issues/issue214.icry.stdout
	tests/issues/issue290v2.icry.stdout
	tests/issues/issue312.icry.fails
2016-07-12 14:58:53 -07:00
Adam C. Foltzer
2c428804bc remove splitBy and update documentation
Closes #291
2016-07-05 09:58:49 -07:00
Rob Dockins
33710b6d25 Update unit test golden outputs 2016-05-30 17:51:08 -07:00
Robert Dockins
38946745c3 Add the 'lg2' type function as a synonym.
Fixes #248
2016-05-04 17:54:08 -07:00
Robert Dockins
c620cbf237 Update the parser to allow prefix operators in more places.
This allows us to define (~) as a prefix operator symbol synonym
for `complement`.

Fixes #296.
2016-05-04 16:26:36 -07:00
Iavor S. Diatchki
c9e4fab6a8 Fix up tests. 2015-08-12 15:52:18 -07:00
Trevor Elliott
4d469fa2ce Update test output 2015-06-29 16:34:11 -07:00
Trevor Elliott
9b7e46724c Give 100 fixity levels, and fix prelude fixity again
Also fix issue198, which had been accidentally updated while failing
2015-06-10 11:55:54 -07:00
Trevor Elliott
fb98af636a Slight test output change 2015-06-09 17:02:07 -07:00
Iavor S. Diatchki
089ddc688e Port defaulting to new solver; hook it in with prove implication. 2015-02-25 16:52:24 -08:00
Adam C. Foltzer
3d275ea44c add load targets to search path
Fixes a bug pointed out by @weaversa:
https://github.com/GaloisInc/cryptol/issues/127#issuecomment-64464455

In addition to the other search path changes in #127, we now will add
the directory containing files to be loaded to the search path. This
applies to:

- files loaded with a command line argument, like in the original
  comment
- arguments to `:l`, so for example `:l examples/DES.cry` would work
- batch file arguments, so for example running `cryptol -b
  /some/path/bar.cry` adds `/some/path` to the search path.
2015-02-17 15:27:59 -08:00
Trevor Elliott
41ca73ffaa Update tests for changes to inference
The changes didn't alter the behavior of the typechecker, only the
warning/error output, and the order of some variables when generalizing.
2014-12-30 10:43:38 -08:00
Trevor Elliott
2401954532 The goals are equivalent 2014-12-16 17:56:07 -08:00
Adam C. Foltzer
284338c938 Add the mono-binds flag
When `:set mono-binds=on`, any local definitions lacking type
signatures will not be generalized (i.e., will be monomorphic). This
reduces what is in most cases unnecessary polymorphism that can give
rise to constraints that are difficult to solve. This also improves
the performance of the Cryptol interpreter by lifting many polymorphic
type applications out of the inner loops that are commonly defined as
bindings in `where` clauses.

The flag is on by default in the Cryptol REPL, and in most cases makes
it possible to leave out more type signatures in `where` clauses than
before. However, some programs really do rely on inferring polymorphic
types for local variables; in this case adding an explicit polymorphic
type signature to the local binding in question will make the program
typecheck.
2014-12-15 17:48:25 -08:00
Adam C. Foltzer
ba0a0e8576 Initial import from internal repo 2014-04-17 15:34:25 -07:00