Commit Graph

1841 Commits

Author SHA1 Message Date
Adam C. Foltzer
b39c6e3702 implicit :prove all properties when no argument given
closes #93
2014-09-09 15:27:46 -04:00
Adam C. Foltzer
15e6fec34d update documentation for #82 2014-09-09 11:59:39 -04:00
Adam C. Foltzer
c3c043cc6b implement 0-based tuple indexing; fixes #82 2014-09-09 11:59:39 -04:00
Adam C. Foltzer
6a79019ef6 fixes #89
Very small change to code, lots of change to expected output of interpreter!
2014-09-09 10:49:29 -04:00
Thomas M. DuBuisson
a2fbf632f5 Use tf-random for higher-quality randoms.
Notice the randoms from StdGen are well-known to be quite bad.  For
example, see comments in issue #86.
2014-09-08 21:47:05 -07:00
Adam C. Foltzer
a0bb572388 add note about solvers for ZUC theorem 2014-09-08 14:45:10 -07:00
Joseph Kiniry
b2f0e3db4e Merge pull request #88 from TomMD/master
Fix #86 - make randomWord produce uniform randoms
2014-09-05 13:42:09 -07:00
Thomas M. DuBuisson
5dfb3e9250 Fix #86 - make randomWord produce uniform randoms
When :check was executed on a function accepting words as arguments
cryptol would generate mostly small words.  This strategy failed to find
counter-examples in formulas such as:

    (\a b -> (((a : [16]) + b) % 17) == ( (a % 17 + b %17) % 17 ) )

This failure is particularly egregious considering 50% of the inputs
result in False.  We now generate a better distribution of words and are
discussing use of a smart-check like strategy or an evaluation of the
logic to tailor generation in a future release (see issue #87).
2014-09-05 11:57:06 -07:00
Brian Huffman
d63bdc750c 'parseDeclsWith' runs parser with appropriate 'cfgModuleScope' flag
In layout mode, setting cfgModuleScope to true ensures that the lexer
will generate virtual open/close braces and virtual semicolons between
decls.

This is a follow-up to c689a15cfc.
2014-09-04 16:43:34 -07:00
Adam C. Foltzer
4622a1d177 add ZUC example, translated from Cryptol 1 2014-09-04 11:05:42 -07:00
Brian Huffman
c689a15cfc 'parseDeclsWith' uses layout or not depending on Config parameter 2014-09-04 10:35:56 -07:00
Adam C. Foltzer
592c4945d7 add test case for #83 2014-09-04 10:16:18 -07:00
Trevor Elliott
a1b7cbc39d Fix a lexer bug, and add a regression
Closing brackets weren't closing virtual layout blocks.
2014-09-03 13:46:47 -07:00
Trevor Elliott
86918fb0f2 New layout processor
Better handling of the interaction between virtual layout blocks and the
tokens that delimit them.
2014-09-03 13:25:14 -07:00
Trevor Elliott
f3a9ad5fc7 Allow semicolons to delimit declarations
In addition to relying on layout, also allow explicit semicolons to punctuate
layout blocks.
2014-09-03 10:15:26 -07:00
Trevor Elliott
91b026c9dd The second half of the #81 fix
Accidentally didn't commit some additional changes.  This is the other half of
56028ec.
2014-09-03 00:47:29 -07:00
Trevor Elliott
56028ec664 Fix a bug introduced by the parens fix
The fix for #81 ignored a case where a layout block was started by ParenL
symbol.  In that case, the layout level wouldn't be pushed on the stack, and a
parse error would eventually result.  This adds the check into the ParenL
special case, starting an explicit block terminated by a ParenR, as well as a
new virtual layout block.

  Also missing from the original patch was the full offsides check, which must
be repeated in the ParenL special case.  I think that we should probably do some
refactoring of the layout processor, as I doubt that this is the only case that
will produce this behavior.

  Additionally, the BraceL/BraceR cases were removed, as explicitly delimited
layout is not currently supported.
2014-09-03 00:42:46 -07:00
Brian Huffman
9ed8523c68 Tweak parser to require fewer parentheses around if-then-else and lambdas
E.g. "True && if True then True else True" is now accepted without parens.
The grammar now relies on the relatively low precedence of 'else', '->',
and ':' relative to other infix operators to disambiguate parsing. This
addresses issue #74.
2014-09-02 19:22:27 -07:00
Trevor Elliott
34877371f6 Fix the interaction of layout and parens
The layout processor didn't account for layout blocks that were terminated by
parens or braces, so this accounts for that in the context stack that is kept by
the layout processor.  Fixes #81
2014-09-02 18:30:54 -07:00
Adam C. Foltzer
696b96fe12 changed errors to panics for better reporting
Also squashed a couple incomplete patterns when they came up, but
haven't done a full check for all of them.
2014-09-02 17:45:39 -07:00
Adam C. Foltzer
17ee75ea6a add (failing) test case for #81 2014-09-02 16:29:55 -07:00
Brian Huffman
928ac3dc8f Fix bug in 'take' on infinite streams for symbolic simulator
Previously, 'take'ing a finite prefix of an infinite stream would
incorrectly yield a 'VStream' value, which would normally indicate
an infinite result. Now it correctly returns a 'VSeq' value.
2014-09-02 11:09:35 -07:00
Dylan McNamee
3ebc8bffcd Incorporating Sean Weaver's fixes to programming cryptol - ticket #80 2014-09-02 10:26:35 -07:00
Adam C. Foltzer
9346db2d0c Bind sat/prove results to a single type for both unsat and sat, use more record fields
See #66 for more discussion. Basically we don't want the type of `it` to be different for unsat or sat results, so we put undefined values in there instead. Also, instead of using tuples and different field names to distinguish formula arguments of various arities, we use a convention of fields `arg1`, `arg2`, ...
2014-08-21 15:02:35 -07:00
Adam C. Foltzer
b1c4527a28 reference ticket in sat result documentation 2014-08-20 17:13:04 -07:00
Adam C. Foltzer
1cf61e12c3 reword :sat and :prove results as records
Per @weaversa's suggestions in #66, we now bind records to `it` for sat results, leading to less ambiguity about the meaning of those results. There is still some weirdness to this; the fields present in the record change based on the result and the arity of the formula, but this seems like a reasonable approach given that it's not an expression that needs a type.
2014-08-20 17:10:40 -07:00
Adam C. Foltzer
010627a045 clean up some stray notebook files; don't check in history database 2014-08-20 11:27:06 -07:00
Adam C. Foltzer
46bcc188f4 fix external bindings not being in scope in let bodies
The renamer was being run on let bindings without including the NamingEnv of the overall module context. Fixed and added a test case for this.
2014-08-20 11:18:26 -07:00
Adam C. Foltzer
ceb084ca0a Merge branch 'feature/repl-bindings' 2014-08-19 17:15:19 -07:00
Adam C. Foltzer
b78062eafe bind it even when no counterexample/sat is available; add tests
Similar to what @weaversa requested in #66, we bind `it` to `False`
when we can't find a sat assignment, and `it` to `True` when we've
proved a theorem.

Also adds some simple tests for the sat/prove result binding, and let
binding at the repl.
2014-08-19 17:11:43 -07:00
Adam C. Foltzer
5a3c01afc4 Merge branch 'master' into feature/repl-bindings
Conflicts:
	cryptol/REPL/Command.hs
	src/Cryptol/Symbolic.hs

Fixed up Value -> Expr conversion to account for a change in those
types. Reworked sat and prove results to account for changes in that
API.
2014-08-19 11:32:59 -07:00
Adam C. Foltzer
d409116160 Merge branch 'devel'
This was the branch I originally set up for git flow, but we're moving
to production=release and develop=master, so this branch is obsolete.
2014-08-19 10:31:31 -07:00
Adam C. Foltzer
156771a5d5 bind counterexamples and satisfying assignments to it
If the solver returns values for :sat or :prove, we now bind them at
the repl to `it`. If more than one argument is part of the cex/sat
answer, we tuple up/uncurry the arguments.
2014-08-18 19:19:22 -07:00
Adam C. Foltzer
cf1774bbbc change repl syntax to be more like ghci
Since :let was clashing with :load for :l, and for consistency with
ghci, you can now enter bare let expressions at the repl:

> let x = 5

Also, the grammar for the repl parser disallows type bindings, which
were possible in the previous :let.

Semicolons no longer needed, though we can only bind one thing at a
time.
2014-08-18 19:17:27 -07:00
Adam C. Foltzer
33f9012cda restricted grammar of :let commands
For now, you can only enter one binding at a time at the REPL, and can
only enter expression bindings rather than type signatures or type
synonyms. It wouldn't be too hard to add type synonyms, but the value
is questionable.
2014-08-18 14:48:44 -07:00
Adam C. Foltzer
62f38192e9 added it to the REPL 2014-08-18 14:14:37 -07:00
Adam C. Foltzer
1dedf6d693 refactor dynamic environment into ModuleEnv
This just makes for a more consistent API; the "dynamic" environment
as extended by REPL commands is now part of the ModuleEnv. It's
actually more general than just for the REPL. We can use it in general
to add bindings on top of a loaded module context.
2014-08-18 13:28:21 -07:00
Brian Huffman
fdaff29e9d Support for loading multiple source files simultaneously
- track source filepath for each loaded module
- raise error when different loaded files use same module name
2014-08-15 16:18:14 -07:00
Adam C. Foltzer
b2e83f8e27 getVars processes interactively-bound names better
This change fixes the issue where `getVars` in the REPL would return
names with the `#Uniq_...` prefix. This was confusing, and also
messing up tab-completion.
2014-08-14 17:06:00 -07:00
Adam C. Foltzer
f125947117 additional support for let-bound variables at the repl
Let-bound identifiers now show up in `:browse`, get unloaded whenever
we load a new module context, and can be sent to `:sat` and `:prove`.
2014-08-14 16:31:47 -07:00
Adam C. Foltzer
bed85a6b78 initial :let implementation
This works by adding an extended environment to some of the
ModuleSystem functions. This extended environment contains
declarations entered interactively, a naming environment that maps
parsed names to the unique names we use to ensure lexical scope, and
an evaluation environment containing the values of the let-bound
expressions.
2014-08-14 13:14:22 -07:00
yuuko
7d9376dfd5 changed the output of :sat so it is formatted by type 2014-08-14 16:33:37 +01:00
yuuko
52e82226b5 :sat now can provide multiple solutions to equations given to it, the number shown can be set with :set satNum <integer value>, where <0 shows all solutions 2014-08-14 03:34:20 +01:00
Adam C. Foltzer
2b1380beed Add extended environment, support for typechecking and evaluating decls
This is a checkpoint; it builds but doesn't yet work correctly!
2014-08-13 17:51:17 -07:00
Joseph Kiniry
39a472e43f Merge branch 'master' of github.com:GaloisInc/cryptol 2014-08-12 16:24:53 -07:00
Joseph Kiniry
ebbc048ffb Added mention of type alias use/restrictions. 2014-08-12 16:24:46 -07:00
Joseph Kiniry
6fc11569ea Corrected typo. 2014-08-12 16:24:28 -07:00
M Knight
502816fbd3 Add MKRAND RBG 2014-08-10 10:47:19 -05:00
Sam Anklesaria
bede37a436 Merge branch 'newsbv' 2014-08-07 10:57:10 -07:00
Sam Anklesaria
8e54775642 exposing low level uninterpreted interface 2014-08-07 10:54:40 -07:00