GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2025-01-08 08:49:44 +03:00
Code Issues Projects Releases Wiki Activity
2,179 Commits 66 Branches 28 Tags 96 MiB
c3eca4f22a
Commit Graph

1291 Commits

Author SHA1 Message Date
Brian Huffman
b8ecb4abbe Fix typo in comment. 2018-07-11 04:52:55 -07:00
Iavor Diatchki
1666ea3bd0 Merge branch 'master' of github.com:GaloisInc/cryptol 2018-07-10 17:05:37 -07:00
Iavor Diatchki
2f00384038 Fixes #521 2018-07-10 17:05:31 -07:00
Brian Huffman
be8c334efe Reference interpreter uses base and infLength printing options. 
Fixes #412.
 2018-07-10 09:58:37 -07:00
Brian Huffman
186e2a0a82 Reference evaluator tracks lengths of list values. 2018-07-10 09:35:06 -07:00
Brian Huffman
ca62acc727 Remove non-primitives @@ and !! from reference evaluator prims. 2018-07-10 09:30:49 -07:00
Brian Huffman
ee2d2ec9c4 Fix typo in comment. 2018-07-10 08:47:53 -07:00
Brian Huffman
f3a9a7ceb7 Fix typo in typechecker error message. 2018-07-09 18:30:38 -07: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
cf6e7161f5 Bugfix: Remember the results of defaulting. 2018-06-28 14:23:13 -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
Iavor Diatchki
0bf36808ed Improve various defaulting/instantiatiation warnings and error messages. 2018-06-25 16:48:10 -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
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
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
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
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
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
Brian Huffman
47df3e69b9 Remove obsolete primitives integer and intmod. 
Use the generalized `demote` instead.
 2018-06-18 18:09:03 -07:00
Brian Huffman
7424731e3f Generalize [a,b..c] to work for types in class Literal. 2018-06-15 17:45:57 -07:00
Brian Huffman
cbba44f692 Generalize [a..b] to work for types in class Literal. 2018-06-15 17:17:54 -07:00
Brian Huffman
9cbda930c7 Fix compiler warnings. 2018-06-15 11:12:50 -07:00
Brian Huffman
01667d8486 Merge branch 'master' into literal-class 
# Conflicts:
#	lib/Cryptol.cry
 2018-06-15 11:10:11 -07:00
Brian Huffman
a7b69892f1 Add primitives toZ and fromZ for converting integers to/from Z n. 2018-06-15 10:13:09 -07:00
Brian Huffman
59104829a0 Rename Cryptol.Utils.PP.<> to avoid clash with Semigroup operator. 
The pretty-printing operator `<>` is now called `<.>`.

Cryptol now compiles without warnings on both ghc 8.2 and 8.4.
 2018-06-14 10:17:49 -07:00
Brian Huffman
5ac32d1ad5 Add a variant of the demote primitive for type Z n. 
intmod : {val, mn} (fin val, n >= val + 1) => Z n
 2018-06-14 06:17:51 -07:00
Brian Huffman
daac41fdec Fix implementation of ^^ on type Z n in symbolic backend. 2018-06-14 06:16:04 -07:00
Brian Huffman
a8f3e189e0 Remove unused import. 2018-06-13 11:57:51 -07:00
Brian Huffman
ea9b0a9194 Make type Z n an instance of class Literal. 
instance (fin val, fin m, m >= val + 1) => Literal val (Z m)
 2018-06-13 11:55:26 -07:00
Brian Huffman
b3d2851923 Merge branch 'master' into literal-class 
# Conflicts:
#	src/Cryptol/TypeCheck/Kind.hs
#	src/Cryptol/TypeCheck/Solve.hs
 2018-06-13 11:41:35 -07:00
Brian Huffman
4f1a743585 Remove special cases in evaluator for types Z 0 and Z inf. 
These types are now forbidden by the type checker.
 2018-06-13 11:32:23 -07:00
Brian Huffman
ec19538a3b Make type Z n a partial type operator, requiring (fin n, n >= 1). 2018-06-13 11:16:46 -07:00
Brian Huffman
9a2437b727 Use size parameter in random value generator for type Integer. 2018-06-13 10:50:58 -07:00
Brian Huffman
30ba719343 Fix exhaustive and random testing for integers-mod-n type. 2018-06-13 09:35:12 -07:00
Brian Huffman
7da2219caf Initial implementation of type Z n (integers mod n). 
This covers most of #510, including the type itself and the
class instances, but not any of the new primitive functions.
 2018-06-11 18:03:18 -07:00
Brian Huffman
e11806f64a Reimplement comparison primitives by recursion on the TValue. 2018-06-11 16:40:57 -07:00
Brian Huffman
f7b8373a4a Fix incomplete pattern match warnings. 2018-06-11 15:33:46 -07:00
Brian Huffman
4adb4bc13a Remove unused constructors from Parser.AST.Type datatype. 2018-06-11 15:23:09 -07:00
Brian Huffman
9188878c4e Renamer handles built-in types like Integer and Bit using TApp. 2018-06-11 15:03:12 -07:00
Brian Huffman
d5c9a030da Split new modules Fixity and Selector from Cryptol.Parser.AST. 2018-06-11 14:28:49 -07:00
Brian Huffman
7cf26f8653 Remove dead code. 2018-06-11 11:10:53 -07:00
Brian Huffman
083d42ad30 Remove integer-based arguments to logicUnary and logicBinary. 
Type `Integer` is not an instance of class `Logic`, so we don't need
to implement logic operations for this type.
 2018-06-11 11:04:56 -07:00
Brian Huffman
2228c03565 Simplify case expression. 2018-06-10 12:42:10 -07:00
Brian Huffman
6b3dc6d9d4 For quick-checking integer properties, use a randomized bit width. 
The distribution is unbounded, but is biased to smaller bit widths,
and is designed to have an average bit-width of 64.
 2018-05-25 11:07:19 -07:00
Brian Huffman
c7d5f51240 Report "untestable type" error when using :exhaust with type Integer. 2018-05-24 17:24:11 -07:00
Aaron Tomb
99f3fdbf37 Merge Cryptol/Extras.cry with Cryptol.cry 
Closes #427.
 2018-05-23 15:55:05 -07:00
Brian Huffman
3a4bc6a2af Allow ":set <boolean-flag> = false" and ":set <boolean-flag> = true". 
Previously we only allowed enable/disable, on/off, or yes/no.
 2018-05-22 15:17:15 -07:00
Iavor Diatchki
9e3f7ec13f Merge branch 'master' of github.com:GaloisInc/cryptol 2018-05-22 14:27:12 -07:00
Iavor Diatchki
a0c15874e2 Factor out panic code into its own little package. 2018-05-22 14:27:03 -07:00
Brian Huffman
9fccc00867 Remove obsolete GF(2) polynomial primitives from reference interpreter. 2018-05-14 17:32:09 -07:00
Brian Huffman
26acdd0dad Pass pretty printing options to printer for reference interpreter. 
(The options are not actually used yet.)
 2018-05-14 17:03:00 -07:00
Iavor Diatchki
52f335deaa Asllow writing fancier kinds. This is in preparation for type primitives/abstract types. 2018-05-11 16:05:20 -07:00
Iavor Diatchki
e0cbfb1531 Fixup and clean-up checking of non-builting type applications. 
Fixes #506
 2018-05-11 10:38:00 -07:00
Iavor Diatchki
35ece3c3ed Use a datatype instead of Bool, to be more explicit about what it means. 2018-05-11 10:37:18 -07:00
Iavor Diatchki
2e2ac8c09d Just comments and layout 2018-05-11 10:07:12 -07:00
Iavor Diatchki
812ecec79c Fail if a built-in type has been applied to some arguments. 
Fixes #507
 2018-05-11 10:05:39 -07:00
Brian Huffman
13363c4c9b fastTypeOf doesn't perform any simplification when substituting types. 
This makes it more useful for the saw-core translation, because we
can notice when type coercions need to be applied.
 2018-05-10 15:23:53 -07:00
Iavor Diatchki
ec5e84dd37 Add a fin constraint on following matches in a comprehension. 
Fixes #505.   It doesn't really make sense to have infinite things
following a finite thing in a comprehension, as there would be a whole
lot of unreachable elements.  Since this is likely an error, we try
to catch it with the types.
 2018-05-07 11:52:43 -07:00
Iavor Diatchki
59aa5f11d0 Fix typos 2018-05-07 11:50:51 -07:00
Brian Huffman
42e89b11ae Make :check work for tests involving type Integer. 2018-04-20 16:00:32 -07:00
Brian Huffman
3be72ae2cb Replace indexing primitives (!!) and (@@) with cryptol implementations. 2018-04-18 16:50:39 -07:00
Brian Huffman
2cdf9bd159 Replace primitives pmult, pmod, pdiv with cryptol implementations. 2018-04-15 06:56:20 -07:00
Iavor Diatchki
849cee862b Fix up binding of it to values. 2018-04-02 09:49:17 -07:00
Iavor Diatchki
47ed3b57ad Make :check and :exhaust bind the counter example in it 
Fixes #449
 2018-03-30 17:10:38 -07:00
Iavor Diatchki
bfb3290e9b Improve display ordering on names and group constraint synonyms separately. 
See #503
 2018-03-30 15:28:22 -07:00
Aaron Tomb
9d344bb452 Fix build with GHC 8.4.1 2018-03-23 15:08:09 -07:00
Brian Huffman
fccf55f30f Remove obsolete cvs-era $Header$ keywords. 2018-03-22 13:33:12 -07:00
Brian Huffman
c1949586c2 Thunk elements of EList expressions of type Bit during evaluation. 
Fixes #488.
 2018-03-21 17:55:11 -07:00
Brian Huffman
d84d697aae Fix compiler warnings and remove dead code. 2018-03-21 11:21:48 -07:00
Brian Huffman
83442f5049 Implement signed shift (>>$) and less-than (<$) in reference interpreter. 
Fixes #469.
 2018-03-21 09:58:48 -07:00
Brian Huffman
134d8cca4c Thunk elements of EList, ETuple, and ERec expressions during evaluation. 
Fixes #432.
 2018-03-07 18:21:16 -08:00
Brian Huffman
ff86d02600 Fix typo in docstring. 2018-01-11 10:24:26 -08:00
Brian Huffman
60e03d7313 Suppress unused-variable warning for names that are defined externally. 
Previously names were considered "local" if they have the same module
name as the module name that we are performing renaming on (the idea
being that all "external" names would have been imported from a different
module).

However, this assumption doesn't hold for the "<interactive>" module,
which is used for REPL declarations. Names from earlier REPL declarations
should be considered "external" when renaming later REPL expressions, even
though they have the same "<interactive>" module name.

The problem is fixed by checking whether a name was already present in the
old naming environment; if so, then it is considered "external" and will
not generate an unused-variable warning.
 2018-01-11 10:23:19 -08:00
Iavor Diatchki
79e6f83c70 Report proper errors instead of panicing. 
Previously I erroneously thought this would be reported by the renamer,
so I turned the errors into panics.

Fixes #493
 2018-01-04 15:27:37 -08:00
Iavor Diatchki
4aa68c9cf4 Add a note for another useful rule 2018-01-04 10:59:33 -08:00
Iavor Diatchki
762b31597f Add a case to solve things like: 4 == 2 ^^ x 2018-01-04 10:57:05 -08:00
Iavor Diatchki
bc45e751d1 Fixes #492 incorrect simplification for tMax 2018-01-03 09:56:47 -08:00
Iavor Diatchki
989e5734ef Move defaulting code to a separate module. 2017-12-22 16:01:19 -08:00
Iavor Diatchki
7bf0fa8222 Remove evaluator cases that should not occur. 
These are translated away in the solver.
 2017-12-22 11:24:44 -08:00
Iavor Diatchki
c481fbc6e8 Handle lifted selectors in the solver, so they are not visible in evaluator. 2017-12-22 11:23:54 -08:00
Iavor Diatchki
defb9b0598 When things go wrong, give us a hint as to where they did. 2017-12-22 11:23:26 -08:00
Iavor Diatchki
b9957e49ce Make location more precise 2017-12-21 14:39:58 -08:00
Iavor Diatchki
2dff60fb0e Allow some errors to subsume others. 2017-12-21 14:34:37 -08:00
Iavor Diatchki
978b3b232b Remove errors that should have been handled by the renamer. 2017-12-21 14:28:58 -08:00
Iavor Diatchki
9c06f07223 Move errors to their own module. 2017-12-21 13:59:53 -08:00
Iavor Diatchki
8bf780b969 Print even when malformed. Useful for printing before renamer. 2017-12-21 13:32:17 -08:00
Iavor Diatchki
89d453a6fa Print location under, as it was before. 2017-12-21 10:21:53 -08:00
Iavor Diatchki
c093d05659 Don't print file locations twice. 2017-12-21 10:19:04 -08:00
Iavor Diatchki
32fb511ced Add location more generally. 2017-12-15 14:12:38 -08:00
Iavor Diatchki
7db18e817c Improve error message for ambiguous types. 2017-12-15 14:05:15 -08:00
Iavor Diatchki
2272a59314 Rename type synonyms properly. 2017-12-01 10:29:42 -08:00
Iavor Diatchki
5cd90d0045 Fix up scoping when instantiating modules. 2017-12-01 09:51:28 -08:00
Iavor Diatchki
c0b4ddd608 Keep track of the order in which type parameters are declared in the file. 2017-11-28 14:07:14 -08:00
Iavor Diatchki
9de90e5752 Slightly better parser messages. 2017-11-15 15:36:45 -08:00
Brian Huffman
79fbb61aa7 Require doc-strings to start with "/**" with exactly 2 asterisks. 
Things like "/******* WARNING ********/" are now parsed as ordinary
comments. See #438.
 2017-11-15 11:36:25 -08:00
Brian Huffman
511e97767f Disallow spaces inside qualified names (e.g. Foo::x). Fixes #381. 2017-11-15 10:52:36 -08:00
Iavor Diatchki
2b396f0d66 Buble up Error in the first argument of Literal 2017-11-14 17:14:42 -08:00
Iavor Diatchki
d517193296 Default types of kind * to Integer. 2017-11-14 17:14:24 -08:00
Iavor Diatchki
8700ad6832 Run warning check whenever we do some renaming, instead of just in the module. 
Hopefully this fixes #483 properly this time.
 2017-11-14 16:11:00 -08:00
Iavor Diatchki
5ccb0bb4ad Warn for unused type names. 
Fixes #483.
 2017-11-14 15:57:15 -08:00
Brian Huffman
00d07cfbb9 Fix implementation of demote primitive in reference interpreter. 2017-11-10 08:35:19 -08:00
Brian Huffman
231c5713c4 Adapt internal uses of demote primitive to its new type 2017-11-10 08:34:58 -08:00
Brian Huffman
5eb67c0513 Introduce class Literal and generalize primitive demote to use it. 
demote : {val, a} Literal val a => a

instance (fin val) => Literal val Integer
instance (fin val, fin bits, bits >= width val) => Literal val [bits]
 2017-11-08 15:23:08 -08:00
Iavor Diatchki
c4b156e499 Don't add an empty record, if the module has not value parameters. 
Fixes #484
 2017-11-08 14:19:40 -08:00
Iavor Diatchki
a8d5c5c602 Add some better cancellation of common constants. 2017-11-08 14:13:49 -08:00
Iavor Diatchki
7e964aa1cd Add a simplification rule for subtraction. 2017-11-07 15:51:05 -08:00
Iavor Diatchki
e1b9e0b5bf Merge branch 'master' of github.com:GaloisInc/cryptol 2017-11-07 13:59:28 -08:00
Iavor Diatchki
0adcddb792 Remember edit path. 2017-11-07 11:27:50 -08:00
Iavor Diatchki
f71ba16345 Fix order of type applications. 2017-11-07 11:27:37 -08:00
Brian Huffman
30b7d2918a Implement signed operators (/$) and (%$) in reference interpreter. 
This partially addresses ticket #469.
 2017-11-06 16:55:32 -08:00
Brian Huffman
8f94daf783 Catch calls to error coming from SBV library. Fixes #479. 2017-11-06 14:10:01 -08:00
Brian Huffman
c587d3fcb4 Allow underscores in numeric literals. Implements #477. 
The implementation allows any number of underscores between
digits, or between the base specifier and digits. Underscores
are not allowed at the beginning or end of a numeric literal.

0x1234_5678  (OK)
0b_0110_1001 (OK)
0xff______ff (OK)
5_000_000    (OK)
2_________3  (OK)
0_x1234      (BAD)
_0xff        (BAD)
52_          (BAD)
_5           (BAD)
 2017-11-02 17:00:46 -07:00
Iavor Diatchki
d6d8ab1d35 Try to shrink the model, when defaulting at the REPL. Fixes #476 2017-10-30 17:26:18 -07:00
Iavor Diatchki
d7d1f21434 Cancel out finite positive variables. 2017-10-30 14:25:15 -07:00
Iavor Diatchki
07eac47989 Merge remote-tracking branch 'origin/abstract-types' 2017-10-27 15:12:22 -07:00
Iavor Diatchki
3f8a8b8874 Add forgotten file 2017-10-27 15:07:15 -07:00
Iavor Diatchki
2d3e146766 Allow evaluation in parameterized module, as long as parameters are not used. 2017-10-27 14:59:32 -07:00
Iavor Diatchki
4cf83a3c3d Keep track of the file that cause an error. 
Also, now we automatically switch to working on this file, which
is sometimes nice, and sometimes confusing...
 2017-10-27 11:02:08 -07:00
Brian Huffman
bc5fe0e4c9 Add combinators tIsRec and aRec for matching record types (TRec). 2017-10-27 10:54:32 -07:00
Iavor Diatchki
35a3843685 Remember the path when editing. 2017-10-27 10:21:50 -07:00
Iavor S. Diatchki
65ebbb5956 Extend core linter with support for parameterized modules. 2017-10-26 14:20:29 -07:00
Iavor S. Diatchki
26240742a4 Pretty print when panicing, makes it easier to see 2017-10-26 11:50:48 -07:00
Iavor S. Diatchki
8627945ade Fix up transformation 2017-10-26 11:50:36 -07:00
Iavor Diatchki
b87f387d38 Add param in the correct place, but there's still something wrong. 2017-10-25 17:00:11 -07:00
Iavor Diatchki
3f4cc570cf Use a record for all module parameters at the value level. Also improve PP 2017-10-25 16:39:29 -07:00
Iavor Diatchki
ee7506b32a Only drop common stars or space at the beginning of a comment. 2017-10-25 11:28:30 -07:00
Iavor Diatchki
5c51d32a4e Fix up html syntax highlighting. 2017-10-25 11:12:37 -07:00
Iavor Diatchki
c666731495 Print help for type parameters. 2017-10-24 16:12:12 -07:00
Iavor Diatchki
6056eaad4b Use proper types for module parameters; allows for stroing metadata 
For example, documentaiton.
 2017-10-24 15:43:32 -07:00
Iavor Diatchki
2f53602749 We need to instantiate constraints, not parameterize them! 2017-10-24 14:04:30 -07:00
Iavor Diatchki
e2d74066d8 Only load by module name, if we have a special module name. 
Otherwise, scripts tend to fail to reload, as they have no module name,
which defaults to `Main`, but the file name is called something else.
 2017-10-24 13:46:48 -07:00
Iavor Diatchki
fd0e6258fc More fixes to rewriting code. 2017-10-24 13:41:37 -07:00
Iavor Diatchki
2de8eff416 Fix up translation, to change the type of name to Parameter 2017-10-24 11:59:59 -07:00
Iavor Diatchki
c2ca8f30a7 Fix displaying of parameters. 2017-10-24 11:44:44 -07:00
Iavor Diatchki
8472cfb0db Fix editing and reloading for generated modules. 2017-10-24 11:16:13 -07:00
Iavor Diatchki
4c9d25bf39 Fix up browsing for module with added params. 2017-10-24 11:09:57 -07:00
Iavor Diatchki
ca6b34f621 Refactor module system things; better loading of `A modules. 2017-10-23 15:12:12 -07:00
Iavor Diatchki
05e3a84cd1 Plug in adding parameters to each definition. XXX: fix repl :m :load 2017-10-20 16:33:02 -07:00
Iavor Diatchki
d52c5f5938 Merge remote-tracking branch 'origin/master' into abstract-types 
# Conflicts:
#	src/Cryptol/Parser/ParserUtils.hs
 2017-10-20 14:07:47 -07:00
Iavor Diatchki
1e17bd03cf Make parser use strict text (XXX: does this affect performance +ve or -ve) 
Also makes module names into their own newtype
 2017-10-20 12:00:00 -07:00
Brian Huffman
e3ea9335c8 Put correct VWord width tag on result of symbolic index operation. 
Fixes #474.

Previously, applying (@) at type `[a][b] -> [i] -> [b]` would tag the
result value as having width `a` instead of width `b`. This is now fixed.
 2017-10-20 11:09:32 -07:00
Iavor S. Diatchki
300383772f Just a clarification 2017-10-19 15:17:39 -07:00
Iavor S. Diatchki
095a7718d9 Add a pass to rewrite a param. module, into a non-param module 
All definitions are parameterized by all parameters.
 2017-10-19 13:45:40 -07:00
Iavor Diatchki
c3d8b4b3f8 Allow focusing of parameterized modules; disable evaluation in such contexts. 2017-10-18 14:33:12 -07:00
Iavor Diatchki
432638a77a Allow a value parameter to be defined by another value parameter. 2017-10-18 13:36:37 -07:00
Iavor Diatchki
1cbbba7c32 More functionality 2017-10-17 16:26:05 -07:00
Iavor Diatchki
dda54aa016 More progress 2017-10-16 15:54:42 -07:00
Iavor Diatchki
acacd0b53d Merge remote-tracking branch 'origin/master' into abstract-types 
# Conflicts:
#	src/Cryptol/TypeCheck/Monad.hs
 2017-10-16 14:25:08 -07:00
Iavor Diatchki
942173b7f9 Add comments and fixes #473 2017-10-16 14:09:52 -07:00
Iavor Diatchki
a85ff3a54b Add comments 2017-10-16 14:05:46 -07:00
Iavor Diatchki
6ba8849216 Just reformat 2017-10-16 14:05:31 -07:00
Iavor Diatchki
ec456b9447 Fix typo 2017-10-16 14:05:01 -07:00
Iavor S. Diatchki
15f236d42b More loading of instances (incomplete) 2017-10-13 15:27:42 -07:00
Iavor S. Diatchki
2b21610796 Better integration of module parameters with module system and REPL 2017-10-13 11:35:46 -07:00
Iavor S. Diatchki
7dc7be45bb Merge remote-tracking branch 'origin/master' into abstract-types 
# Conflicts:
#	src/Cryptol/REPL/Monad.hs
 2017-10-13 10:45:35 -07:00
Iavor S. Diatchki
3f2ac1171c Comments 2017-10-13 10:40:24 -07:00
Iavor Diatchki
51808bbf23 More comments 2017-10-06 16:24:10 -07:00
Iavor Diatchki
f71b951108 Some documentation. 2017-10-06 15:57:45 -07:00
Iavor Diatchki
b5ef48dcd7 Fix-up the benchmarking code. 2017-10-06 11:55:48 -07:00
Iavor S. Diatchki
13ac2d9f05 wibble 2017-10-05 15:52:50 -07:00
Brian Huffman
fd0fc99418 Update some Integer-related stuff in the reference interpreter. 2017-10-05 15:13:37 -07:00
Iavor S. Diatchki
4e65ad03f9 Almost complete module instantiation 2017-10-05 15:10:25 -07:00
Iavor S. Diatchki
f64f051842 Now wild cards in the types of module parameters 2017-10-05 13:49:25 -07:00
Iavor S. Diatchki
f7adf8f4ba Validate schemas properly 2017-10-05 13:46:24 -07:00
Iavor S. Diatchki
933e2cd2ee Merge branch 'abstract-types' of github.com:GaloisInc/cryptol into abstract-types 
# Conflicts:
#	src/Cryptol/ModuleSystem/InstantiateModule.hs
 2017-10-05 12:45:11 -07:00
Brian Huffman
4b386477ec Avoid creating a new option when :set is used with a prefix of a name. 
Fixes #450.
 2017-10-04 21:22:59 -07:00
Brian Huffman
a9de74ed5d Implement module-name completion and validation for :browse. 
Fixes #396.
 2017-10-04 19:17:42 -07:00
Iavor Diatchki
1f2cacbae5 Merge branch 'master' of github.com:GaloisInc/cryptol 2017-10-04 15:50:41 -07:00
Iavor Diatchki
5208739653 Don't print directly to stdout. Fixes #166 2017-10-04 15:50:31 -07:00
Brian Huffman
d025108bd2 Make :browse filter declarations by module name instead of value name. 
See #396.
 2017-10-04 15:45:25 -07:00
Brian Huffman
2b568897da Remove implicit Bit type signature on rhs of property declarations. 
Fixes #224.

It might be desirable to add some other check for `property` declarations
to make sure that their types are predicates of some arity.
 2017-10-04 15:26:17 -07:00
Brian Huffman
c7380d35d4 Fix symbolic indexing function indexFront to avoid indexing past the end. 
Previously it would create a lookup table with 2^w entries, where w is
the bit-width of the index. Now the lookup table has min(2^w, n) entries,
where n is the length of the indexed vector.

Fixes #463.
 2017-10-04 13:46:58 -07:00
Iavor Diatchki
f74ad3c29d Fix haddock comment, should restore build process. 2017-10-04 10:09:01 -07:00
brianhuffman
73de3f787f Merge pull request #453 from GaloisInc/blocks-padding 
Implement `blocks` and `padding` operators for numeric types.
 2017-10-04 07:11:19 -07:00
Rob Dockins
2df09a428a Change how test coverage statistics are computed. 
This formulation accounts for the fact that test vectors
are chosen randomly with replacement.

Fixes #461
 2017-10-03 17:37:48 -07:00
Iavor Diatchki
092c0621a3 More checking of module instantiation 2017-10-03 16:38:50 -07:00
Brian Huffman
3b03545552 Merge branch 'master' into blocks-padding 2017-10-03 13:44:32 -07:00
Iavor Diatchki
ef430332f8 Remove unused import. 2017-10-03 13:38:10 -07:00
Iavor Diatchki
2ef0a67d9b Merge branch 'master' into abstract-types 2017-10-03 13:35:57 -07:00
Rob Dockins
9785ed1e32 Add a rule to the numeric solver for "linear unifiers" 
Check for situations where a unification variable is involved in
a sum of terms not containing additional unification variables,
and replace it with a solution and an inequality.
`s1 = ?a + s2 ~~> (?a = s1 - s2, s1 >= s2)`

Fixes #212
 2017-10-03 12:49:17 -07:00
Iavor Diatchki
234615e7b2 Add some comments 2017-10-03 10:53:40 -07:00
Iavor Diatchki
a233084db8 Merge branch 'master' of github.com:GaloisInc/cryptol 2017-10-02 15:47:23 -07:00
Iavor Diatchki
498b99cda3 Split out exports specs; add some parsing for functor instances. 2017-10-02 15:01:45 -07:00
Rob Dockins
c0699e2d62 Change the fixity levels of (||) and (&&). 
This advances the next step in the plan described in issue #241.
 2017-10-02 14:56:33 -07:00
Rob Dockins
2894a1fdef Make solver startup/shutdown exception-safe. 2017-10-02 14:06:44 -07:00
Rob Dockins
12ac2c383a Revert "Remove the Data.Sequence-based representation of unpacked bitsequences." 
This may improve performace on some examples.
This reverts commit d4b70a039a.
 2017-10-02 11:12:50 -07:00
Iavor Diatchki
7135284f80 Basics of sort of module instantiation 2017-09-29 16:27:13 -07:00
Brian Huffman
940b9c80ec Merge branch 'integer' 2017-09-29 14:23:28 -07:00
Brian Huffman
3fb74f7f60 Make :check and :exhaust print counterexamples the same way :prove does. 
This addresses the first part of issue #449.
 2017-09-29 10:19:56 -07:00
Iavor Diatchki
ff94ef30e1 Merge branch 'master' into abstract-types 
# Conflicts:
#	src/Cryptol/TypeCheck/Depends.hs
#	src/Cryptol/TypeCheck/Infer.hs
 2017-09-29 10:06:27 -07:00
Iavor Diatchki
fe88d98213 Merge branch 'master' of github.com:GaloisInc/cryptol 2017-09-29 09:44:42 -07:00
Brian Huffman
7be06d803e Fix typo in error message. 2017-09-29 09:28:46 -07:00
Iavor S. Diatchki
75ca6b7fa2 Say something if name does not refer to anything 2017-09-28 15:47:23 -07:00
Iavor S. Diatchki
aa44dd7860 Add support for docstrings on type things 
See #456
 2017-09-28 14:39:22 -07:00
Brian Huffman
d9cbfd62d1 Add instance Zero Integer. 2017-09-28 13:26:01 -07:00
Brian Huffman
cce32a4868 Merge branch 'master' into integer 
This brings the Logic and Zero type classes into the integer branch.
 2017-09-28 13:18:27 -07:00
Brian Huffman
7e34c25e4d Switch to infix syntax for blocks and padding operators. 
"x /^ y" is x/y rounded up, i.e. the least n such that x <= y*n.
"x %^ y" is the least k such that x+k is a multiple of y.

For comparison,
"x / y" is x/y rounded down, i.e. the greatest n such that x >= y*n.
"x % y" is the least k such that x-k is a multiple of y.

The new syntax is much more suggestive of the relation to "/" and "%".
 2017-09-28 10:26:31 -07:00
Brian Huffman
defadf8730 Fix cut-and-paste error. 2017-09-28 09:45:40 -07:00
Brian Huffman
1e41541405 Let type checker discharge fin (blocks x y) and fin (padding x y). 
Both of these type operators are always either finite or undefined.
 2017-09-28 09:28:07 -07:00
Iavor Diatchki
3f80cc92f9 Checkpoint: not complete, commit to continue WFH 2017-09-27 16:43:00 -07:00
Brian Huffman
9bc6d02019 Implement blocks and padding operators for numeric types. 
The design is as described in issue #96:

blocks msgLen blockSize = the least n such that msgLen <= blockSize * n
padding msgLen blockSize = least k such that msgLen + k divides blockSize

or alternatively:

msgLen + padding msgLen blockSize = blocks msgLen blockSize * blockSize
 2017-09-27 13:43:26 -07:00
Iavor Diatchki
aab03be26a More wibbles 2017-09-27 10:24:30 -07:00
Iavor Diatchki
208119fbbf Merge branch 'master' of github.com:GaloisInc/cryptol 2017-09-27 10:17:06 -07:00
Iavor Diatchki
6018af3537 Just documentation 2017-09-27 10:16:58 -07:00
Brian Huffman
1ed5640339 Merge branch 'master' into logic-class 
# Conflicts:
#	tests/mono-binds/test05.icry.stdout
 2017-09-26 16:50:53 -07:00
Iavor Diatchki
8ea27a3c24 Keep track of tparam types; make bound vars be just tparams. 
The two are very similar anyway, so it makes sense to merge the types.
This also helps display module type parameters using their name, rather
than treating them as unknown variables.

The whole printing of names system is still quite confusing, so maybe
there is a better way to do this, but keeping track of the source of
type parameters seems potentially useful information anyway...
 2017-09-26 16:30:02 -07:00
Iavor Diatchki
b8707033d7 Add module parameters as extra vars---prints nicer error messages. 2017-09-26 15:29:23 -07:00
Iavor Diatchki
83d0132e50 Add module-level constraints to assumptions when proving implications. 2017-09-26 15:21:40 -07:00
Iavor Diatchki
12ee62ff9d Merge branch 'master' into abstract-types 
# Conflicts:
#	src/Cryptol/TypeCheck/Solver/SMT.hs
 2017-09-26 15:21:18 -07:00
Iavor Diatchki
60523d5986 Delete old solver stuff. 
The main user visible effect of this might be that sometime things on
the Cryptol command line are instantiated in a slightly different way:
we get `inf` sometimes when we got a finite example before.

We could work around this if it is an issue, but I am not sure which
behavior is more reasonable.
 2017-09-26 14:02:52 -07:00
Iavor Diatchki
8e7aff62b4 Checkpoint, adding constraints 2017-09-26 10:23:34 -07:00
Iavor Diatchki
7dc1ffc456 Some support for constraints on parameters. 2017-09-25 15:37:50 -07:00
Iavor Diatchki
2c07a55d15 Add call stacks here and there 2017-09-25 15:37:22 -07:00
Iavor Diatchki
9f3f592a2f Add a 5 second time-out to calls to z3 2017-09-25 11:41:20 -07:00
Iavor Diatchki
ccc4b828c2 Represent type parameters as just type variables. 2017-09-25 11:41:00 -07:00
Iavor Diatchki
019d935c2f Merge branch 'master' into abstract-types 
# Conflicts:
#	src/Cryptol/Parser/Lexer.x
#	src/Cryptol/Parser/LexerUtils.hs
#	src/Cryptol/TypeCheck/Depends.hs
#	src/Cryptol/TypeCheck/Infer.hs
#	src/Cryptol/TypeCheck/Kind.hs
#	src/Cryptol/TypeCheck/Solver/SMT.hs
 2017-09-22 16:23:12 -07:00
Brian Huffman
36f8fff3ca Support Integer type in reference evaluator (:eval). 2017-09-22 15:45:43 -07:00
Iavor Diatchki
0cc5151e6d Correct the handling of TCAnd in the SMT translation 2017-09-22 10:43:02 -07:00
Iavor Diatchki
9432f33ca1 Add some missing method defintions 2017-09-22 10:10:04 -07:00
Brian Huffman
1d71fa141c Merge branch 'master' into integer 2017-09-21 17:05:00 -07:00
Brian Huffman
d545abceec Fix incomplete pattern match warning caused by merge. 2017-09-21 16:47:36 -07:00
Brian Huffman
2c4157ecd4 Merge branch 'master' into logic-class 2017-09-21 16:44:39 -07:00
Iavor S. Diatchki
bec59d2faa On my computer this is only trustworthy. strange 2017-09-21 14:58:12 -07:00
Iavor S. Diatchki
d1abac0cec Update design; handle numeric type parameters in type checking SMT 2017-09-21 14:57:53 -07:00
Brian Huffman
2ce1ca3eca Change constraint synonym syntax from "constraint" to "type constraint". 
For example:

type constraint NonZero n = (fin n, 1 <= n)

last : {n, a} NonZero n => [n]a -> a
last xs = xs!0
 2017-09-21 13:21:51 -07:00
Brian Huffman
393a11e170 Implement constraint synonyms (#373). 
The syntax is just as described in ticket #373: We have a new
declaration form consisting of the keyword 'constraint' followed
by a identifier and optionally a list of type parameters; the
right-hand side is either a single constraint or a parenthesized,
comma-separated list of type constraints. For example:

constraint NonZero n = (fin n, 1 <= n)

last : {n, a} NonZero n => [n]a -> a
last xs = xs!0
 2017-09-21 09:40:22 -07:00
Iavor Diatchki
f7e1a941e2 checkpoint 2017-09-21 09:28:01 -07:00
Brian Huffman
c4af07a053 Remove unused TokenKW constructors. 2017-09-20 11:38:36 -07:00
Brian Huffman
b4cf793e7f Adapt fastSchemaOf function to avoid simplifying when instantiating props. 
Previously, checking the type of e.g. "(&&) `{[2]b}" would not return
"(Logic [2]b) => [2]b -> [2]b -> [2]b" as expected, but
"Logic b => [2]b -> [2]b -> [2]b". This made it impossible to reconstruct
the instances necessary to produce the required Logic dictionary when
translating to saw-core.
 2017-09-18 15:54:35 -07:00
Brian Huffman
c6db409837 Add type-matching functions pIsZero and pIsLogic. 2017-09-15 21:50:21 -07:00
Brian Huffman
b03f1ae0c2 Add class Zero with zero :: {a} (Zero a) => a. 
Shift operators also have a `Zero` constraint on the element type.
 2017-09-15 16:37:44 -07:00
Iavor Diatchki
b5196dfb44 Remove warnings, moudule is safe 2017-09-15 16:05:26 -07:00
Iavor Diatchki
f3a3b1cbd0 Start on implementing abstract types/constants (module parameters) 2017-09-15 16:05:16 -07:00
Brian Huffman
d1305b2860 Add 'Logic' typeclass with operations complement, &&, ||, ^, zero. 
Left and right shift operations also gain a Logic constraint,
since they shift in zero values.
 2017-09-15 13:33:56 -07:00
Brian Huffman
571d186c6c Support toInteger/fromInteger with symbolic arguments in :prove/:sat. 2017-09-14 17:51:03 -07:00
Aaron Tomb
c05281d390 Fix spurious failures due to lazy I/O 
Regression test check31 was failing somewhat unpredictably due to the
use of lazy I/O when loading the Z3 prelude for the type checker. Using
the `strict` package seems to fix it.
 2017-09-13 15:31:43 -07:00
Brian Huffman
5d73b5d405 Merge branch 'master' into integer 
This involved plenty of non-trivial merge edits to fix compilation errors.

# Conflicts:
#	src/Cryptol/Eval.hs
#	src/Cryptol/Eval/Value.hs
#	src/Cryptol/Prims/Eval.hs
#	src/Cryptol/Symbolic/Prims.hs
#	src/Cryptol/Symbolic/Value.hs
#	src/Cryptol/TypeCheck/AST.hs
 2017-09-13 14:28:04 -07:00
Eric Mertens
28bc4f81de Work around happy bug by adding type signature on ipat 2017-09-11 10:36:59 -07:00
Robert Dockins
cefc67a149 Implement signed division and remainder as methods of the Arith class. 
Clarify the documentation that division is "round toward 0" division.
 2017-08-16 17:34:22 -07:00
Robert Dockins
6a30560fc0 Implement the nested lexicographic order for signed comparisons. 
This commit reorganizes how lexicographic comparisons are done in
the concrete simulator to reuse the same combinator from the symbolic
simulator.  This makes it more straightforward to implement the new
signed comparison.
 2017-08-16 13:58:44 -07:00
Robert Dockins
86d28bc01e Merge remote-tracking branch 'origin' into signed-arith 2017-08-16 11:30:27 -07:00
Iavor Diatchki
b3f605d9f4 Pretty print with a bit more space, so we can see what's going on. 2017-08-15 10:52:32 -07:00
Iavor S. Diatchki
ca2136fab9 Merge pull request #440 from sliverdragon37/master 
Adds the :ast and :extract-coq commands for printing out a parseable AST
 2017-08-15 10:25:08 -07:00
Eric Mullen
05b8f0f3c1 more polished 2017-08-14 15:45:37 -07:00
Eric Mullen
505e565bbe performed all suggested changes except new module for ShowAST 2017-08-14 13:28:09 -07:00
Robert Dockins
987e4a0c3b Implement the type-level support required for the new SignedCmp class. 
This class will represent types that can be meaningfully compared for
signed bitvector equality.  It lifts the comparison operations on
nonempty bitvectors through tuples, records and finite sequences via
lexicographic order.
 2017-08-07 12:37:46 -07:00
Robert Dockins
e3dd83066e Rename signed bitvector operations to put the $ at the end 2017-08-04 17:02:10 -07:00
Robert Dockins
b1a821217e Merge remote-tracking branch 'origin/master' into signed-arith 2017-08-03 13:28:51 -07:00
Robert Dockins
4d974fefac Fix bugs in the signed right shift operation. 
However, see the following SBV issue that currently affects
Cryptol behavior when computing signed right shifts with
symbolic index amounts:
https://github.com/LeventErkok/sbv/issues/323
 2017-08-03 13:26:03 -07:00
Brian Huffman
c5f34e1c51 Fix typos in Haddock strings 2017-08-02 19:46:03 -07:00
Robert Dockins
a68b835d51 Add operations for signed arithmetic, and carry condition testing. 2017-08-02 16:39:07 -07:00
Robert Dockins
08b334fce5 Rename LargeBitsVal into BitsVal 
It is now the only unpack bitsequence representation, so no need to
distinguish it as being "large".
 2017-08-01 16:26:24 -07:00
Robert Dockins
d4b70a039a Remove the Data.Sequence-based representation of unpacked bitsequences. 
It appears to have negligable or negative performance advantages over
the representation on sequence maps.  Deleting the additional representation
removes a lot of code paths, and makes things somewhat simpler.
 2017-08-01 16:04:25 -07:00
Robert Dockins
771d07f920 Implement new "large" bitsequence representation. 
When bitsequences cannot be packed as words, they have been
represented using an explicit sequence datastructure containing
thunks for the individual bits.  However, for finite, but very large,
bitsequences this was consuming unacceptable amounts of memory.

When bitvector lengths cross an arbitrarily-designated threshold
(currently 2^16 bits) we instead use a sparse representation based
on SeqMap, similar to the representation used for other finite and
infinite sequence types.
 2017-08-01 14:49:52 -07:00
Robert Dockins
b564b21b31 Typo in error message 2017-07-31 10:04:52 -07:00
Robert Dockins
0b9c186132 Make 'random' compute on concrete inputs in the symbolic evaluator. 
This patch does not add a warning when using 'random' in symbolic expressions.
We currently don't have any organized mechanism for generating warnings during
evaluation, and the value of emitting such a warning is debatable.

Fixes #364
 2017-07-27 15:45:37 -07:00
Robert Dockins
2fb706a44c Make sure EvalErrors are propigated to the REPL error handler. 
This keeps runtime evaluation errors from killing the Cryptol process.
 2017-07-26 18:05:30 -07:00
Robert Dockins
dba3d2f7d8 Avoid using partial indexing operations. 
Instead raise evaluation errors when indexing into finite sequences
with invalid indices.
 2017-07-26 18:04:38 -07:00
Robert Dockins
399a2e47d5 Add additional thunking in logical and arithemetic primitive operations. 
This prevents a loss of desirable sharing in the interpreter, and turns
recursive algorithms with potential sharing from exponential-time to linear
time.  It appears to have little impact on other algorithms.

Fixes #432
 2017-07-26 15:30:36 -07:00
Aaron Tomb
2fd6599e0b Adopt LeventErkok's suggestion from #435 
Closes #435.
 2017-07-21 12:58:05 -07:00
Aaron Tomb
8aa497206c Re-enable prover identification in stats 2017-07-20 10:38:38 -07:00
Levent Erkok
5857477ab2 Modifications to make cryptol compile with SBV 7.0 
Also, bumped up the version to 2.4.1
 2017-07-18 10:25:00 -07:00
Iavor Diatchki
4a43c675d9 When checking a binding, treat schema validation constraints 
just like any other constraint from the definition.

In particular, if the schema validity depends on an outer context,
the constraints should be solve in that outer context, not here.

Fixes #314
 2017-07-10 17:35:49 -07:00
Iavor Diatchki
c836d8e356 Improve error message. 
Fixes #383
 2017-07-10 17:11:55 -07:00
Iavor Diatchki
b5d6715b21 Add support for comments; panic on completely bogus inputs. 
Note that we still do not check for errors in commands, perhaps we should?
 2017-07-10 16:58:33 -07:00
Iavor Diatchki
affcc25156 Don't crash when we detect and error, tell the user instead! 
Also, improve the printing of the errors a bit.
 2017-07-10 11:59:39 -07:00
Iavor Diatchki
0f825daf2f Bug fix: remember to pop-off the solver's context. 2017-07-10 11:05:47 -07:00
Iavor Diatchki
5a885e9f5a Check for consistency before improving. 
We may want to do this more often, but it may have a performance penalty.

Anyway, we need this check here, because previously the code was assuming
that the goals are known to be consistent, and we are just wanting to
default them, which should never make them inconsistent, just more instantiated.

The current solution is a bit of a stop-gap, until we redo the defaulting
story, and separate it form improvement.
 2017-07-10 10:59:40 -07:00
Iavor Diatchki
89f0af891a Report inconsistent constraints together. 2017-07-10 10:56:56 -07:00
Iavor Diatchki
ae3e0ea106 Add some functionality for simple checking of the consistency of goals. 2017-07-10 10:55:49 -07:00
Iavor Diatchki
04fbc4c1c2 Notice the fin inf is impossible. 2017-07-10 09:41:15 -07:00
Andrey Chudnov
6bdce04727 Extend built-in library caching to Cryptol::Extras 2017-07-07 14:25:22 -07:00
Eric Mullen
92d9049082 correctly print out uids for type variables 2017-07-06 16:52:11 -07:00