This allows us to attach information to `EFun` nodes that describe
which named function the lambda belongs to, and which arguments
it handles. This information is filled in by the `NoPat` pass
as it desugars multi-argument functions into a sequence of lambdas
and is used during typechecking to produce error messages.
There is an odd potential for the renamer to get things wrong here.
If a named function has an argument that shadows it's own name,
the renamer may incorrectly resolve the name in a function description
for later arguments. The resulting error message will then point to
the wrong name (although it will be in the vicinity...). It's hard
to fix this without folding the NoPat pass into the renamer (which
we should also do, but it's a nontrivial refactoring).
Multi-argument functions are now desuguared into nested lambdas
in the `NoPat` phase instead of during typechecking. This gives
more sensible results when the same variable is shadowed in the argument
list. In particular, extra "where" bindings that are added for pattern
desugaring now have a scope that is outside patterns and variables
occuring further to the right.
Some programs that used to produce "overlapping symbols" errors are
now accepted with a shadowing warning instead.
The main downside of this refactoring is that the `checkFun` operation
no longer has access to function name or argument numbers for definitions,
as all functions have become single-argument lambdas by typechecking time.
This can be fixed by recording this information in the AST during the
NoPat desugaring instead.
The name binding structure that results from multi-parameter
functions with repeated names, and the interaction with pattern
desugaring is currently very counterintuitive. See issue #567 for
more discussion.
This generator will will generate "special" values, and should
also provide better coverage across the range of values the type
can represent, instead of being strongly biased toward values near
1, as the old generator was.
by enumerating all bitpatterns.
Note, this overcounts somewhat the number of distinct floating point
values there are, since all NaNs are considered identical
as `Float` values. We could be more careful here to avoid
generating more NaN values than required, but I'm not sure it's worth
the effort.
Fixes#1051
After parsing all the "input" values, there may be some left over
if we have used constructs (like prime field recip) that are
defined via uniquely specified variables. We can simply ignore
these extra values.
Expose some additional primitives, such as FMA,
abs, sqrt, and more classification predicates.
Refactor the primitives table for floating-point
values into a single generic table that uses
methods from the `Backend` class.
* Updates all the examples in CrashCourse.tex up to the functions section
This adds more REPL annotations for the exercise checker in the Programming
Cryptol book. There is still more work needed to support many of the examples in
the functions section (and presumably the rest of the book as well), so I think
this is a logical stopping point for now until we add a feature that lets you
write out a file and load it into the repl.
* Updates ProgrammingCryptol.pdf wrt recent changes
* Use ghc 8.10.3 for cryptol-remote-api to test SGX compatibility
* Fix cvc4
* Fix test suite for cryptol-remote-api
* Default to putting the heap as low in address space as possible
