GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-12-15 18:52:13 +03:00
Code Issues Projects Releases Wiki Activity
2,050 Commits 68 Branches 28 Tags 95 MiB
0a68d4e3a1
Commit Graph

2050 Commits

This Branch
This Branch
All Branches
Author SHA1 Message Date
Brian Huffman
0a68d4e3a1 Haddock comment for instance Eq Type. Fixes #645. 2019-10-18 10:50:44 -07:00
Aaron Tomb
ce0365fb80 Bump master Cryptol version to 2.8.1 2019-09-17 10:08:42 -07:00
Aaron Tomb
1cb884ce11
Merge pull request #644 from GaloisInc/at-rel28-prep 
Update CHANGES.md and Travis config for 2.8.0
 2019-09-04 08:30:22 -07:00
Aaron Tomb
ae6de61d28 Add changes for Cryptol 2.8.0 to CHANGES.md 2019-09-03 10:16:15 -07:00
Aaron Tomb
d16f70b956 Disable macOS builds on Travis for now 
They're not really reproducible, given the use of Homebrew. Dependency
versions update suddenly, and always at the most inconvenient times.
 2019-09-03 09:40:35 -07:00
brianhuffman
8581f8e0b2
Merge pull request #642 from GaloisInc/issue615 
Make :dumptests check whether type is testable before starting.
 2019-08-30 07:37:30 -07:00
Brian Huffman
64423cbcdc Make :dumptests check whether type is testable before starting. 
Instead of panicking, :dumptests will now print the message
"The expression is not of a testable type" when used with an
inappropriately-typed expression. Also, Integer return values
are now supported.

Fixes #615.
 2019-08-29 12:32:44 -07:00
Aaron Tomb
dbfb329d2b
Merge pull request #641 from GaloisInc/at-rel28-prep 
Bump dependency versions in prep for 2.8.0 release

This includes the version of Z3 used in the Docker image
 2019-08-28 13:50:46 -07:00
Aaron Tomb
7d62081632 Bump dependency versions in prep for 2.8.0 release 
This includes the version of Z3 used in the Docker image
 2019-08-28 13:24:58 -07:00
Brian Huffman
9c55ec56c6 Export commandList from module Cryptol.REPL.Command. 2019-08-28 11:22:29 -07:00
Brian Huffman
12805bef0e Avoid calling wordLit with bitsizes greater than maxBitIntWidth. 
Fixes #636.
 2019-07-24 16:50:40 -07:00
Brian Huffman
2e72a7387c Replace fromIntegral with fromInteger or toInteger where possible. 
See #637.
 2019-07-24 13:13:11 -07:00
Brian Huffman
484f9fc631 Fix typos in comments. 2019-07-24 13:10:34 -07:00
Iavor Diatchki
ce26749142 Flush after storing, so that we can see the content. 2019-07-05 14:52:13 -07:00
Iavor Diatchki
8fe9f5efa9 Add support for working with in-memory sources. 
Currently we only use this for the Prelude, which is baked into Cryptol.
Previously we used to save it in a temporary file, which would show
up in error messages, leading to bad user experience and unreliable
test outputs.

Also improves the shadowing errors.

Fixes #569
 2019-07-05 14:09:04 -07:00
Iavor S. Diatchki
cc5c10b4c4
Merge pull request #630 from GaloisInc/prelude_prims 
Prelude Prims
 2019-07-05 09:57:58 -07:00
Iavor Diatchki
ca4968ff3d Fix test. The error message changed, but is still valid. 
We should really have only one way to say this,
I made a ticket: #633
 2019-07-05 09:37:45 -07:00
Iavor Diatchki
4b5d569e09 Fix tests---some variables got renumbered. 
We really should fix this up so we don't print the numbers unless
there really is an ambiguity.
 2019-07-05 09:34:20 -07:00
Iavor Diatchki
91b69e85cd Remove debugging output. 2019-07-05 09:31:44 -07:00
Iavor Diatchki
7c708faa47 Show additional type constraints in help message. 2019-07-05 09:16:53 -07:00
Iavor Diatchki
a0b4b14f86 Make constraints on type constructors/functions explicit. 
This is mostly working, but I still need to update the help on the REPL
to show the constraints.
 2019-07-03 17:03:31 -07:00
Iavor Diatchki
971897d9ca Use 'Prop' instead of '@' to write the kind of a constraint. 
This is more consistent with how we've been printing kinds for a while,
so no need to change the notation.
 2019-07-03 10:21:04 -07:00
Iavor Diatchki
72068cb961 Move type-level primitives to the Prelude. 
For the time being, there is still some information about them that
is duplicated in Cryptol.TypeCheck.TCon, but we at least the parsed syntax
does not depend on the typechecked syntax.
 2019-07-02 17:34:36 -07:00
Iavor Diatchki
1cfadef5ea Add a forgotten test 2019-07-01 10:26:39 -07:00
brianhuffman
c5dec7443a
Merge pull request #628 from GaloisInc/issue625 
Issue625
 2019-06-28 11:31:28 -07:00
Brian Huffman
8b0e236eec Support element type ascriptions on list enumerations: [a,b..c:t]. 
Cf. issue #625.
 2019-06-27 14:31:06 -07:00
Brian Huffman
e03446dbc8 Adjust whitespace. 2019-06-27 14:25:08 -07:00
Brian Huffman
1e11ff6b8b Add type constraint synonyms (<) and (>). 
Fixes #400.
 2019-06-26 20:44:13 -07:00
brianhuffman
c071ff9fa4
Merge pull request #627 from GaloisInc/infix-type 
Infix type synonyms
 2019-06-26 20:06:54 -07:00
Brian Huffman
14d25e8f9a Fix pretty printing for infix type/constraint synonyms. 2019-06-26 18:19:12 -07:00
Brian Huffman
10da255fd1 Re-implement infix type constraint (<=) as a constraint synonym. 
Also removed special-case hack for (<=) in the renamer.

Also adapted test case output to account for the new prelude declaration.
 2019-06-26 18:04:16 -07:00
Brian Huffman
17c47c4ac0 Update type pretty-printer to handle infix type synonyms. 2019-06-26 17:54:40 -07:00
Brian Huffman
fb86b1538c Renamer looks up type operator fixities in the NamingEnv. 
Primitive infix type operators are looked up in a hard-coded
table; everything else is looked up in the NamingEnv.
 2019-06-26 17:36:46 -07:00
Brian Huffman
eadaf4473e Add parser rules for infix type/constraint synonyms. 2019-06-26 17:35:19 -07:00
Brian Huffman
b54e4835ac Make kind checker accept TInfix constructors from the renamer. 2019-06-26 17:29:55 -07:00
Brian Huffman
da1c509ffd Propagate fixities from type declarations into the NamingEnv. 2019-06-26 16:54:40 -07:00
Brian Huffman
019d2af088 NoPat pass annotates type/constraint synonyms with fixities. 2019-06-26 15:20:00 -07:00
Brian Huffman
c0914c96df Add fixity field to TySyn and PropSyn datatypes. 2019-06-26 15:13:37 -07:00
Brian Huffman
0f6e627b52 Fix typos in haddock comments. 2019-06-26 13:29:07 -07:00
Brian Huffman
546d7809e9 Remove fixity table from NamingEnv. 
The Name type already contains fixity information we can use.
 2019-06-26 13:17:13 -07:00
Brian Huffman
d3bc9baa43 Fix typo in haddock comment. 2019-06-26 12:59:41 -07:00
brianhuffman
44a617693b
Merge pull request #626 from GaloisInc/simplify-parser 
Simplify parser
 2019-06-25 17:11:58 -07:00
Brian Huffman
a8552f58a6 Remove duplicated code for parsing/renaming/checking constraints. 
We now re-use the same code that is used to parse, rename, and
kind-check type expressions.
 2019-06-25 14:26:40 -07:00
Brian Huffman
f53c1f8777 Disambiguate Parser.y so we don't need to rely on operator precedences. 2019-06-25 09:54:23 -07:00
Brian Huffman
5b912afe5a Fix typo in comment. 2019-06-24 13:18:41 -07:00
Brian Huffman
eb7b74a041 Improved formatting for fixity error message. 
Cf. #590.
 2019-06-24 11:43:08 -07:00
Brian Huffman
f0e527a9dc More informative, nicer error message for fixity errors. 
Fixes #590.
 2019-06-21 16:01:17 -07:00
Brian Huffman
8001e5d09c Fix typo in comment. 2019-06-21 11:58:21 -07:00
Brian Huffman
5d19320bfa Regenerate pdf of Programming Cryptol book. 2019-06-20 11:07:36 -07:00
Brian Huffman
c62a88a8ec Regenerate Syntax.tex from Syntax.md. 2019-06-20 11:07:18 -07:00