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.
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.
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.
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.
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.
The python side of the notebook needed to be updated to expect a
.cabal-sandbox rather than cabal-dev sandbox. Also added a -fnotebook
flag to the cabal file to build the Haskell side of it.
