lemmarathon
7c282538ea
Add Dockerfile.
2018-07-02 12:29:45 -04:00
Brian Huffman
fe4b2d9f70
Update tab-completion for :help to also complete type names.
2018-06-29 16:28:52 -07:00
Brian Huffman
99773d71b7
Memoize result of symbolic if-then-else on sequence types.
...
It is important that we memoize `mergeSeqMap`: Because one
lookup into the merged sequence leads to two other sequence
lookups, the lack of memoization could led to exponential runtime
behavior in the worst case.
Fixes #514 .
2018-06-29 14:16:35 -07:00
Brian Huffman
debe4df76d
Fix broken compilation on ghc 8.2.
2018-06-28 19:34:10 -07:00
Iavor Diatchki
4c6a69c0cf
Improvements to naming of variables.
...
This does a bunch of small changes, that should improve the usability
of Cryptol. Namely:
* When we are forced to make up a name, pick something derived from
the source of the variable, annotated with the unique.
* When pretty printing a schema, use "n,m,i,j,k" for numeric variables
and "a,b,c,d,e" for value type vairable.
* When generalizing, put numeric vairables first.
2018-06-28 15:58:11 -07:00
Iavor Diatchki
1d5d5cdf2f
Merge branch 'master' of github.com:GaloisInc/cryptol
2018-06-28 14:23:24 -07:00
Iavor Diatchki
cf6e7161f5
Bugfix: Remember the results of defaulting.
2018-06-28 14:23:13 -07:00
Brian Huffman
836771aded
Tweak names and order of type variables on Cryptol prelude functions.
...
Also update test output for new type variable names.
See #517 .
2018-06-28 14:14:44 -07:00
Iavor Diatchki
75b56e251e
Complain when we spot invalid literals. Fixes #519
2018-06-28 14:13:07 -07:00
Iavor Diatchki
3560161490
Use the existing test for numeric predicates. Fixes #518
2018-06-28 13:56:01 -07:00
Brian Huffman
a4a3207f9f
Swap type argument order for zext and sext.
...
The new argument order works better for partial type application,
so e.g. zext`{32} extends its argument to 32 bits.
2018-06-28 10:40:37 -07:00
Iavor Diatchki
7a54eeb83c
Merge branch 'master' of github.com:GaloisInc/cryptol
2018-06-25 16:48:17 -07:00
Iavor Diatchki
0bf36808ed
Improve various defaulting/instantiatiation warnings and error messages.
2018-06-25 16:48:10 -07:00
Brian Huffman
220afb51d7
Update CryptolPrims.md for prims with changed types and new instances.
2018-06-25 10:33:37 -07:00
Brian Huffman
9597082be4
Fix definition of demote in reference interpreter.
...
It is now generalized to the `Literal` class.
Also delete implementation of removed primitive `integer`.
2018-06-22 06:31:36 -07:00
Brian Huffman
107e4ae646
Fix primitives for list enumerations in reference interpreter.
...
The types of `fromTo`, `fromThenTo`, `infFrom`, and `infFromThen`
have been generalized to work with classes `Literal` or `Arith`.
2018-06-22 06:27:21 -07:00
Brian Huffman
9fcb481161
Generalize [x,y...] (infFromThen primitive) to class Arith.
2018-06-21 18:24:12 -07:00
Brian Huffman
4697683ac4
Generalize [x...] (i.e. infFrom primitive) to class Arith.
2018-06-21 17:57:13 -07:00
Brian Huffman
86898c1076
Remove now-redundant primitive toZ; use fromInteger instead.
2018-06-21 17:05:33 -07:00
Brian Huffman
dbd05b5acc
Generalize prelude function fromInteger to class Arith.
2018-06-21 16:59:01 -07:00
Brian Huffman
1f0f41cf2b
Add regression test for #323 .
2018-06-21 09:33:44 -07:00
Iavor Diatchki
d46c5e26de
Use the full path when suggesting the fix for the test. Fixes #509
2018-06-20 16:55:49 -07:00
Iavor Diatchki
cd2f6e045f
Fix more tests.
2018-06-20 16:34:59 -07:00
Iavor Diatchki
83de4c7a81
Merge remote-tracking branch 'origin/master' into literal-class
2018-06-20 16:30:59 -07:00
Brian Huffman
3cdfa62908
Fix implementation of negate and lg2 for types Integer and Z n.
...
`lg2` now throws the new `LogNegative` error on negative integer inputs.
Fixes #515 and #516 .
2018-06-20 15:44:19 -07:00
Iavor Diatchki
29cef7008a
Merge remote-tracking branch 'origin/master' into literal-class
2018-06-20 15:10:21 -07:00
Brian Huffman
171cfa00d1
Fix output for tests/issues/T146.icry to reflect changes in unification.
2018-06-20 15:09:01 -07:00
Iavor Diatchki
b179a6aad7
Merge remote-tracking branch 'origin/master' into literal-class
2018-06-20 15:06:43 -07:00
Brian Huffman
29f401bbcb
Tweak unification algorithm to preserve old behavior more.
...
(This fixes lots of trivially-broken regression tests.)
2018-06-20 15:06:27 -07:00
Iavor Diatchki
0d81f0ba25
Implement defaulting in the presence of overloaded literals.
2018-06-20 15:06:19 -07:00
Brian Huffman
bae811376c
Fix test output for #146 .
2018-06-20 14:57:54 -07:00
Brian Huffman
ae091dbaa9
Fix unification algorithm to avoid returning invalid Subst values.
...
When unifying a variable with a type, we now pay attention to the
scope of type parameters upon which the unification variables in the
type may depend. When two unification variables are unified with each
other, we may need to construct the substitution in the reverse
direction, if the parameter scopes of the two variables are different.
2018-06-20 14:52:52 -07:00
Brian Huffman
5e4b1565bf
Document invariant on Subst type; redo checking of the invariant.
...
The "captured variable" check on `instance TVars Schema` is
now considered excessive and has been removed.
Fixes #323 .
2018-06-20 13:53:58 -07:00
Brian Huffman
7a265773a8
Add regression test for #513 .
2018-06-20 11:13:50 -07:00
Brian Huffman
6364c172ee
Remove debugging output.
2018-06-20 11:11:51 -07:00
Brian Huffman
ea9e15b8b9
Add checks for instantiating type schemas containing unification vars.
...
When instantiating a type schema like `{a} [?n][a]`, if the unification
variable `?n` has a dependency on type parameter `a`, then we require
that the type variables can only be instantiated to themselves. This
avoids problems where (after substitution) the unification variable ?n
could be instantiated to a type containing variable `a`.
The user-visible result of this is that recursive declarations with
partial type signatures like `{a} [_][a]` cannot be use polymorphic
recursion; any recursive calls must be at the same type instance.
Fixes #513 .
2018-06-20 11:06:55 -07:00
Brian Huffman
48ceb5dd9a
Fix typos in comments.
2018-06-20 10:40:17 -07:00
Brian Huffman
5d4dd3fc38
Specialize type of TVFree constructor argument for type variable scope.
...
It had always contained only `TVBound` values.
2018-06-20 10:25:18 -07:00
Brian Huffman
ba9ccf6f1a
Further specialize type of lazyTVars table.
...
The lazyTVars table only ever contained TVars of the form `TVBound tp`.
2018-06-20 09:52:26 -07:00
Brian Huffman
ebece48a36
Specialize type of lazyTVars table in state of Kind-checking monad.
...
The lazyTVars table only ever contained types of the form `TVar v`.
2018-06-20 09:35:32 -07:00
Iavor Diatchki
e579113d05
Merge remote-tracking branch 'origin/master' into literal-class
...
# Conflicts:
# tests/mono-binds/test04.icry.stdout
# tests/regression/check01.icry.stdout
# tests/regression/check16-tab.icry.stdout
# tests/regression/check16.icry.stdout
# tests/regression/check21.icry.stdout
# tests/regression/check22.icry.stdout
2018-06-20 09:14:17 -07:00
Iavor Diatchki
287abbf19f
Merge branch 'master' of github.com:GaloisInc/cryptol
2018-06-19 17:29:09 -07:00
Iavor Diatchki
33f0ab3979
Improved locations for defaulting warnings.
2018-06-19 17:28:59 -07:00
Brian Huffman
3e90de49de
Use existing function isBoundTV instead of redefining a new one.
2018-06-19 17:18:30 -07:00
Iavor Diatchki
c6d93043e1
Use version of GHC that is match what's in the path.
2018-06-19 12:43:56 -07:00
Iavor Diatchki
13187ab13c
Redo using the pattern. Ugly. We should switch back to pattern synonyms.
2018-06-19 11:35:51 -07:00
Iavor Diatchki
c24ca27167
Eagerly simplify 'Literal' constraints.
2018-06-19 11:13:11 -07:00
Iavor Diatchki
43461f1764
Typo
2018-06-19 11:12:40 -07:00
Brian Huffman
c1c80ce316
Explicitly check that extendSubst preserves InferM invariant.
...
We ensure that the bound `TVar`s in the current substitution are
always a subset of the bound `TVar`s in scope.
The regression test for #146 now fails earlier due to this check.
On the other hand, issue #323 never fails the `extendSubst` check.
2018-06-18 18:54:15 -07:00
Brian Huffman
fe4e5d9e3c
Fix typos in comments.
2018-06-18 18:11:00 -07:00
