Setting the prover to "offline" now triggers generation of an SMT-Lib file without invoking a prover on it. If the setting "smtfile" has its default value of "-", the script is printed to standard output. If it has any other value, the value taken as the name of the file to write to. If "smtfile" is set to anything other than "-" during a normal, online proof, the script is saved in the given file after the proof completes, rather than being saved in a temporary file that's subsequently deleted. This behavior can be useful for debugging.
Reopens#94; the book talks about using :e to edit files, and having :exhaust in the command trie breaks this. We need to figure out a better way to disambiguate (#90)
intSize was undefined, causing repl terminate. This is probably because
the incorrect type signature using the scoped type variable (`:: a`
should probably have been `:: SBV a`) either way, bitSize and
bitSizeMaybe should use the same code when the size is finite.
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).
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.
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.
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.
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
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.
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`, ...
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.
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.
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.
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.
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.
