Trevor Elliott
a595948099
Merge branch 'master' into wip/cs
2014-12-30 11:08:26 -08:00
Trevor Elliott
1eac4a3b9d
Switch from always inferring to checking when possible
2014-12-30 10:49:43 -08:00
Trevor Elliott
ec368fe6af
Fix #16
...
Propagating type signatures down when they're given seems to fix this bug.
2014-12-30 10:49:01 -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
12e0d8605c
Remove unused inferFun function
2014-12-29 23:27:31 -08:00
Trevor Elliott
46e176ed5b
Avoid redundant cases
2014-12-29 23:27:03 -08:00
Adam C. Foltzer
80b3102512
Add support for .cryptol files
...
Fixes #97
2014-12-23 17:48:26 -08:00
Trevor Elliott
ea01ec4aaf
Fix a bug with comprehension checking
...
Wasn't relating the size of the goal type to the size of the arms of the
comprehension.
2014-12-22 14:59:52 -08:00
Trevor Elliott
881f397a48
Check instead of infer
...
We can take advantage of information from signatures if we check instead of
infer. I'm not sure if this is actually paying off, but it should mean that we
unify less when signatures are present, and generate goals that are a little
more specific.
2014-12-19 17:33:16 -08:00
Trevor Elliott
cdccf43891
Implement mapMaybeWithKeyTM for Expr/Prop maps
2014-12-18 18:06:27 -08:00
Trevor Elliott
059cc57c1b
Merge branch 'master' into wip/cs
2014-12-18 17:33:37 -08:00
Trevor Elliott
8f06d2eaf4
Avoid re-applying the substitution to goals
2014-12-18 17:28:55 -08:00
Trevor Elliott
ca6cead8f0
Update the output for test 225
2014-12-18 17:28:34 -08:00
Trevor Elliott
ed14d8a708
Add mapMaybeWithKeyTM to the TrieMap class
2014-12-18 17:16:13 -08:00
Trevor Elliott
de1149d4e9
Fill out nullTM and unionTM for Prop/Expr Tries
2014-12-18 13:13:16 -08:00
Trevor Elliott
2ac0985d3d
Merge branch 'master' into wip/cs
2014-12-18 11:10:37 -08:00
Trevor Elliott
09894319fe
Warning removal
2014-12-18 11:04:18 -08:00
Trevor Elliott
e3d41b0f2c
Add unionTM to the RewMap' Trie
2014-12-18 11:04:08 -08:00
Trevor Elliott
1e063e58f3
Fix Functor/Applicative warning for Result
2014-12-18 11:03:13 -08:00
Iavor S. Diatchki
d9dcbea012
WARNING: NOT SURE ABOUT THIS. For now, assume that all vars send to solver are finite.
2014-12-17 17:43:06 -08:00
Iavor S. Diatchki
a23d294b1c
Use different names when naming multiple non-linear constraints.
2014-12-17 17:42:21 -08:00
Iavor S. Diatchki
284e079d59
Don't rewrite Width to Lg2.
...
Since we don't rewrite assumptions in the same way, we end up with
silly goals like:
x >= width y => x >= lg2 (y + 1)
2014-12-17 17:39:06 -08:00
Iavor S. Diatchki
5657754442
Some extra rules for simplifying + and -
2014-12-17 16:05:50 -08:00
Iavor S. Diatchki
9b420b3810
Convert simplified terms back into goal terms.
2014-12-17 15:40:26 -08:00
Iavor S. Diatchki
76dc6994c1
Convert from solver Prop to cryptol type Prop
2014-12-17 15:40:04 -08:00
Iavor S. Diatchki
cdf1afd261
A nicer way to desugar >=
2014-12-17 15:39:44 -08:00
Iavor S. Diatchki
0a02d7d68e
Redo simplification---this is a bit simpler and, perhaps a little faster.
2014-12-17 14:31:22 -08:00
Iavor S. Diatchki
856e374e64
Re-simplify after applying substitution.
2014-12-17 14:29:50 -08:00
Dylan McNamee
16bca156d7
Salsa20 working better with type checker improvements (thanks, Sean!)
2014-12-17 06:44:39 -05:00
Trevor Elliott
b1d65e1655
Update issue225.icry
...
mono-binds is irrelevant to the bug now.
2014-12-16 17:59:07 -08:00
Trevor Elliott
1466d99e1b
This is fixed by mono-binds
2014-12-16 17:56:28 -08:00
Trevor Elliott
2401954532
The goals are equivalent
2014-12-16 17:56:07 -08:00
Iavor S. Diatchki
8b08cca51d
Merge remote-tracking branch 'origin/master' into wip/cs
2014-12-16 17:47:50 -08:00
Iavor S. Diatchki
2836070488
Fixes to applying substitutin to TypeMap keys.
2014-12-16 17:47:22 -08:00
Iavor S. Diatchki
5666963cd1
Merge remote-tracking branch 'origin/master' into wip/cs
2014-12-16 15:20:14 -08:00
Iavor S. Diatchki
53cc08ece5
Fix a bug with being inconsistent with how we make substitutions.
2014-12-16 15:18:49 -08:00
Trevor Elliott
9e5bf0873f
Fix apSubstTypeMapKeys
...
apSubstTypeMapKeys wasn't pushing the substitution down when the key contained
multiple variables.
2014-12-16 15:09:05 -08:00
Iavor S. Diatchki
494e6eca0e
Clean-up things.
2014-12-16 10:59:00 -08:00
Trevor Elliott
b4d9c85635
Merge in the history of the mono-binds change
2014-12-16 09:58:06 -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
Trevor Elliott
1ba8105ec4
Filter out "true" in simplifyProps
2014-12-15 17:33:38 -08:00
Trevor Elliott
21bf0cb62a
Merge branch 'wip/cs' of github.com:GaloisInc/cryptol into wip/cs
2014-12-15 17:02:44 -08:00
Trevor Elliott
caab26946a
Merge branch 'master' into wip/cs
2014-12-15 17:02:01 -08:00
Trevor Elliott
86585ccbe1
Add a Goals newtype
...
This makes it easier to get the behavior of the TVars instance under control,
as we can choose to only apply the substitution to the values of the map after
first applying it to the keys, and thus possibly removing redundant goals.
2014-12-15 17:01:30 -08:00
Iavor S. Diatchki
7e05e86500
Record the computed substitution.
2014-12-15 15:54:46 -08:00
Iavor S. Diatchki
a5aedf211d
Add constraints araising from improvement.
2014-12-15 15:24:53 -08:00
Iavor S. Diatchki
b6dc236885
Remove smtpOrig, we don't really need it for now.
2014-12-15 14:35:28 -08:00
Trevor Elliott
24b80b1b40
Store goals in a TypeMap, instead of a list
...
This should reduce the number of redundant constraints getting generated.
2014-12-15 13:10:57 -08:00
Iavor S. Diatchki
8484c43f83
Merge branch 'wip/cs' of github.com:GaloisInc/cryptol into wip/cs
...
Conflicts:
src/Cryptol/TypeCheck/Solve.hs
src/Cryptol/TypeCheck/Solver/CrySAT.hs
2014-12-15 11:20:07 -08:00
Iavor S. Diatchki
dcbc3a7d8d
Add improvements based on a linear relation (XXX: Still loosing constraints in imps.)
2014-12-15 11:01:27 -08:00
