Iavor Diatchki
920cb58ad0
Some cleanup and doubt that I've enconded the algorithm correctly
2017-09-27 09:50:47 -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
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
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
Iavor Diatchki
c3882a79b5
Named instantiations
2017-09-19 14:47:40 -07:00
Iavor Diatchki
9f2a2ac3a4
Incomplete example of using 'abstract' types.
2017-09-19 14:28:08 -07:00
Iavor Diatchki
9d0092cfd9
Typos and language fixes
2017-09-19 10:32:08 -07:00
Iavor Diatchki
dd46e174e0
Another iteration of the design.
2017-09-19 10:25:17 -07:00
Iavor Diatchki
4bbf2fbb5a
Some notes no how the design might work.
2017-09-18 15:04:08 -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
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
Eric Mertens
28bc4f81de
Work around happy bug by adding type signature on ipat
2017-09-11 10:36:59 -07:00
Eric Mertens
bf571569fa
Add upper bound on happy
...
A bug introduced in happy-1.19.6 causes incorrect type signatures
to be generated in the parser source file which lead to type
checker errors
2017-09-11 10:20:22 -07:00
robdockins
bbcd39d400
Merge pull request #439 from GaloisInc/signed-arith
...
Add operations for signed arithmetic, and carry condition testing.
2017-08-17 10:27:18 -07:00
Robert Dockins
8333b81c16
Update CryptolPrims documentation
2017-08-16 18:26:40 -07:00
Robert Dockins
9550d1b8dd
Update syntax documentation
2017-08-16 18:22:49 -07:00
Robert Dockins
ef047d3a19
Fix test breakage due to new operations in the Cryptol prelude.
2017-08-16 17:37:24 -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
a6d29c73c7
Merge remote-tracking branch 'origin' into signed-arith
2017-08-07 11:55:48 -07:00
Aaron Tomb
e40b15cc5d
Fix type signatures in MiniLock SCrypt example
2017-08-07 08:37:20 -07:00
Robert Dockins
2b9e5a2421
Add signed and unsigned bitvector extensions
2017-08-04 17:04:29 -07:00
Robert Dockins
9a3b64e088
Fix the definition of the signed borrow function
2017-08-04 17:03:23 -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
1e453436b2
Fix grammatical errors in manuals
2017-08-02 19:46:26 -07:00
