GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-12-15 02:01:39 +03:00
Code Issues Projects Releases Wiki Activity
2,056 Commits 68 Branches 28 Tags 95 MiB
8304eb74de
Commit Graph

296 Commits

Author SHA1 Message Date
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 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
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
Brian Huffman
1e11ff6b8b Add type constraint synonyms (<) and (>). 
Fixes #400.
 2019-06-26 20:44:13 -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
0a1cea2912 Update test suite output to accommodate new prelude function. 2019-06-18 15:39:56 -07:00
Iavor Diatchki
ec7c9a0f6e Don't generalize a rec. group, if any members are marked as monomorphic. 
Fixes #607
 2019-06-14 16:14:14 -07:00
Iavor Diatchki
08c537122a Update nQueens example to not print the found solution. 2019-03-25 16:20:17 -07:00
Brian Huffman
7cb16586d4 Add regression test for #581. 2019-03-18 15:29:36 -07:00
Brian Huffman
5076273c10 Add regression test for issue #582. 2019-03-18 14:53:09 -07:00
Brian Huffman
9584fdb54d Remove some duplicate files from /examples that were also in cryptol-specs. 
See #571.
 2019-03-01 18:34:23 -08:00
Iavor S. Diatchki
139c7d50ac
Merge pull request #576 from GaloisInc/fingerprints 
Track file content fingerprints alongside loaded modules
 2019-02-28 11:02:27 -08:00
Eric Mertens
5e75f834e7 Update test for new utf-8 error message 2019-02-28 10:04:17 -08:00
Brian Huffman
24fb6c9511 Remove unused primitive fromThen. 2019-02-27 16:57:00 -08:00
Brian Huffman
c387dbe5fd Remove all uses of [x..] syntax from examples and tests. 2019-02-27 16:25:53 -08:00
Iavor Diatchki
d38eab4b2c Fix test. 2019-01-25 10:20:40 -08:00
Iavor Diatchki
4312787724 Fixes #565 2019-01-24 17:00:16 -08:00
Iavor Diatchki
60c1baebfd Indent goals to be shown a bit further, to line up with assumptions. 2019-01-08 16:42:34 -08:00
Iavor Diatchki
d8b1a7a601 Improve some of the error messages. 2019-01-03 11:28:59 -08:00
Iavor Diatchki
d377f38c9d Use the factored-out test-runner. 2018-12-11 16:30:02 -08:00
Brian Huffman
9b7597c4fd Update changed test output. 2018-12-11 15:52:19 -08:00
Brian Huffman
20b9b1c193 Rename prelude function width to length, and generalize its type. 
Fixes #550.
 2018-10-10 16:21:38 -07:00
Aaron Tomb
0d0eb2cbc3 Fix path names of .md files during tests 2018-09-04 16:31:36 -07:00
Iavor Diatchki
b7b1baa25b Fix test, to account for changes to eval context checking 2018-08-15 20:26:25 +03:00
Brian Huffman
9e7ae9f9ce Reintroduce demote as a copy of number for backward compatibility. 2018-07-27 14:01:18 -07:00
Brian Huffman
f609b36225 Rename primitive demote to the more self-explanatory name number. 
The name "demote" is only meaningful to those who already know what
the Cryptol primitive does. Also, due to recent changes in the error
and warning messages, the name "demote" is showing up much more often
in REPL output. For example:

    Defaulting type argument 'rep' of 'demote' to [2]

    Showing a specific instance of polymorphic result:
      * Using 'Integer' for type argument 'rep' of 'Cryptol::demote'

These messages will hopefully be made less confusing to non-experts
if the name "demote" is replaced with "number".
 2018-07-27 13:52:57 -07:00
Iavor Diatchki
027037d6ee Fix test 2018-07-26 22:06:31 +03:00
Brian Huffman
72bc388663 Add regression test for #533. 2018-07-20 12:04:03 -07:00
Brian Huffman
5def499908 Capitalize sentences in output of :check and :exhaust. 2018-07-20 10:55:24 -07:00
Brian Huffman
409e544772 Restrict polynomial literals to bitvector types. Fixes #530. 2018-07-20 10:06:16 -07:00
Aaron Tomb
0b46db36ce Fix capitalization of MiniLock in test 2018-07-20 10:04:11 -07:00
Brian Huffman
5451683f4a Add regression test for #494. 2018-07-19 15:08:24 -07:00
Brian Huffman
d58aebcee8 Fix shadowing warnings in example cryptol code. 
Shadowing a name from the Cryptol prelude produces an unpredictable
warning message with a temporary file name, which is not good for our
regression test suite.
 2018-07-19 14:48:12 -07:00
Brian Huffman
d803192b2b Add regression test that loads all modules from examples directory. 
This file should be updated every time a new module is added to
`examples`.

Fixes #529.
 2018-07-19 09:57:18 -07:00
Brian Huffman
1e5209ade5 Add regression test for #413. 2018-07-11 13:00:53 -07:00
Brian Huffman
56824291b2 Add inequality constraints to types of fromThen and fromThenTo. 
This ensures that all applications of partial type functions are
well-defined.

Fixes #416.
 2018-07-11 12:58:49 -07:00
Brian Huffman
be8c334efe Reference interpreter uses base and infLength printing options. 
Fixes #412.
 2018-07-10 09:58:37 -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
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
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
0bf36808ed Improve various defaulting/instantiatiation warnings and error messages. 2018-06-25 16:48:10 -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