GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-12-11 07:00:49 +03:00
Code Issues Projects Releases Wiki Activity
989 Commits 68 Branches 28 Tags 95 MiB
921b50a1a9
Commit Graph

989 Commits

This Branch
This Branch
All Branches
Author SHA1 Message Date
Adam C. Foltzer
921b50a1a9 add GHC 8 stackage nightly 2016-06-07 14:29:20 -07:00
Adam C. Foltzer
76be770d83 clean up 7.8-isms 2016-06-07 13:40:15 -07:00
Brian Huffman
1e3d1f642a New evalType function works on either kind * or # 
Cryptol.Eval.Type now provides three evaluation functions
for types:

  evalType    :: EvalEnv -> Type -> Either Nat' TValue
  evalValType :: EvalEnv -> Type -> TValue
  evalNumType :: EvalEnv -> Type -> Nat'

evalValType requires the type to have kind *.
evalNumType requires the type to have kind #.
evalType works on a Cryptol types of either kind.
 2016-06-06 15:43:22 -07:00
Brian Huffman
9fb3d53d88 TValue represents only value types; Nat' is for size types 
We now have separate evalType and evalNumType functions
for use with kind * and #, respectively.
 2016-06-06 15:10:31 -07:00
Brian Huffman
38f143abcc Pattern match on TValues instead of discriminator functions 2016-06-06 13:31:44 -07:00
Brian Huffman
4de0580d1c Redefine type TValue as an inductive datatype. 
This mostly takes care of issue #343, but some problems
remain:

- There is no TValue representation for newtypes
- Many incomplete pattern warnings in Symbolic/Prims.hs
 2016-06-06 11:36:14 -07:00
Adam C. Foltzer
7c9d2a5158 tweak JSON deriving for cryptol-server 2016-05-31 16:11:50 -07:00
Adam C. Foltzer
875d78800f add note about Z3 on 64-bit Linux 2016-05-31 15:47:50 -07:00
Trevor Elliott
e974a1159b Correct the printing of names with the parsed AST 
Fixes #340
 2016-05-31 14:04:05 -07:00
Trevor Elliott
3d67018c70 Ignore the bytes output of issue220 2016-05-31 11:53:38 -07:00
Trevor Elliott
3c59bf3231 Update the test output for mono-bind test 4 
The type variable name was the only change.
 2016-05-31 11:51:01 -07:00
Trevor Elliott
e0d52087b5 Fix type renaming in patterns 
Fixes #341
 2016-05-31 10:59:26 -07:00
Thomas M. DuBuisson
d9ba571286 Merge branch 'master' of https://github.com/GaloisInc/cryptol 2016-05-31 10:39:11 -07:00
Thomas M. DuBuisson
363651c907 Fixes #320 Use -N1, not -N, as the default RTS option. 2016-05-31 10:38:13 -07:00
Brian Huffman
3b524e1ae5 Fix test output for issue093. 
Since #171 was fixed in b77dd2a8, the tests and proofs
are run in the order they appear in the source file.
 2016-05-31 10:34:51 -07:00
Brian Huffman
0623fdcc63 Evaluate types of predicates before checking their validity 
Fixes #339.
 2016-05-31 10:15:12 -07:00
Trevor Elliott
a139c4e1d1 Fixes #304 2016-05-27 22:00:43 -07:00
Trevor Elliott
7976026789 Update test output renamer errors 2016-05-27 18:50:27 -07:00
Trevor Elliott
a490600df5 Fix overlap errors in the renamer 
* The MultipleSyms error should only show up when the import environment
  contains duplicate symbols, and should be triggered lazily.
* Environments that have had errors reported should be rewritten to no longer
  produce those errors during renameVar/renameType

Fixes #337
 2016-05-27 18:37:57 -07:00
Trevor Elliott
2f21dd509a Remove the generic-trie dependency 2016-05-27 17:05:16 -07:00
Brian Huffman
c6144bd332 Update output for tests 256 and 335 
The :t command now parenthesizes the term when needed.
 2016-05-27 16:25:14 -07:00
Brian Huffman
f6a2462306 :t prints un-renamed parsed AST. Fixes #336. 2016-05-27 16:01:55 -07:00
Brian Huffman
d7b117a8ce Use a type-appropriate function argument name 2016-05-27 16:00:59 -07:00
Brian Huffman
bfc8062c69 Avoid extra shadowing warnings when renaming comprehensions 
Fixes #286.
 2016-05-27 15:39:41 -07:00
Aaron Tomb
3658c0962b Fix build with GHC 7.8 
Hide an extra symbol from MonadLib.
 2016-05-25 13:44:51 -07:00
Trevor Elliott
0393c8c54d Fixes #335 
The local type bindings from type annotations in patterns were not being
processed correctly, and built-in type/type-functions were getting shadowed in
binders.
 2016-05-24 11:58:55 -07:00
Brian Huffman
e0e382aa22 Fix typo in comment 2016-05-24 08:22:28 -07:00
Brian Huffman
df27f577a4 Fix typo in comment, whitespace 2016-05-24 08:21:55 -07:00
Iavor S. Diatchki
48642ea282 Fix bogus simplification. 2016-05-12 15:43:31 -07:00
Brian Huffman
70459264ab Use hang and sep instead of hsep to print counterexamples. 
Fixes #329.
 2016-05-11 09:26:57 -07:00
Robert Dockins
9d11fd4485 Fix typo in error constructor name 2016-05-06 14:33:02 -07:00
Robert Dockins
64b8a17c7b Fall back onto unification in more cases when typechecking explicit sequences. 
Fixes #274
 2016-05-06 13:29:49 -07:00
Robert Dockins
92c3b43db8 Add keywords to the REPL autocompletion list. 
In particular, the following keywords will now be suggested by
the REPL autocompletion:
  else, if, let, then, where

These, I believe, are the only keywords which can be entered at
the command line.

Fixes #144
 2016-05-05 13:54:49 -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
b6a83d7cb8 Make a friendlier, non-panic error message for cases where patterns 
introduce nontrivial constraints.

Fixes #290
 2016-05-04 17:38:16 -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
Robert Dockins
59cfe03e54 Update the parser to handle '#' patterns as a special case. 
This partially addresses issue #304.
 2016-05-04 13:54:00 -07:00
Robert Dockins
94f29f46d5 Add Fixity information to Name and the PPName class. 
This allows access to fixity information when pretty-printing
Parser AST, even after the rearranging that is done by the renamer.

Fixes #318
 2016-05-03 17:45:10 -07:00
Robert Dockins
bcb9b1dac1 Fix a boneheaded syntax error 2016-05-03 17:06:32 -07:00
Robert Dockins
21f5993730 Load the Prelude even if a command-line module fails to load. 
Fixes #313
 2016-05-03 15:24:34 -07:00
Robert Dockins
53eef3ed4a Improve the printing of some panic messages. 2016-05-03 12:00:37 -07:00
Dylan McNamee
ab279f01d5 incorporating typos and other improvements to docs 2016-04-27 11:52:09 -07:00
Dylan McNamee
b92cdcccda file cleanup 2016-04-21 13:54:52 -07:00
Dylan McNamee
04e22d8dd6 command appendix 2016-04-21 13:53:02 -07:00
Dylan McNamee
623b847094 merging changes to docs 2016-04-19 11:41:55 -07:00
Joseph Kiniry
0ba8d97c8a Removed extra 's'. 2016-04-18 15:16:39 -07:00
Joseph Kiniry
849fecead8 Merge branch 'master' of github.com:GaloisInc/cryptol 2016-04-18 15:15:58 -07:00
Joseph Kiniry
d43fcc9ebe Whitespace tweak. 2016-04-18 15:15:56 -07:00
Thomas M. DuBuisson
8b577828f6 Simplify constraints of Minilock prims. 
Cryptol 2.3-alpha couldn't math, but thanks to @yav's hard work, Cryptol 2.3 and
later can math!  So with our new found powers comes great simplification.  Not
all is perfect, much like Dori-Mic's situation, but things are much better.
See the width constraints in SCrypt.cry for areas that could be improved with
some semi-obvious statements (forall x. 1 + width x >= width (x - 1)).
 2016-04-12 15:53:12 -07:00
Trevor Elliott
cf979723b7 Fixes #322 
Just needed to recurse through the parens and infix cases in `appTys`.
 2016-04-07 21:26:21 -07:00