The new evaluator allows us to have more direct control over
evaluation order, and makes it straightforward to implement tracing
primitives. There are two new primitives 'trace' and 'traceVal' in the
Cryptol prelude that produce tracing output when evaluated.
Fixes#68
Fix some minor conflicts in the test suite.
Conflicts:
tests/issues/issue002.icry.fails
tests/issues/issue148.icry.stdout
tests/issues/issue198.icry.stdout
tests/issues/issue214.icry.stdout
tests/issues/issue290v2.icry.stdout
tests/issues/issue312.icry.fails
The major change in this patch is to add a new type of 'WordValue'
which is always used to represent finite sequences of bits. A word
value is either a packed word, or a sequence of lazy bits. The 'VSeq'
constructor, in constrast, is now never used for a finite sequence of
bits.
This avoids certain thorny problems that arise when trying to faithfully
implement the lazy semantics of Cryptol. We now do not have to commit
to a value at type '[n]' being represented as a packed word or as an
unpacked word until relatively late. This allows us to perform type-directed
eta-expansion at every recursive call before we know how words will be represented.
This patch fixes all the outstanding strictness bugs that I know of.
Unfortunately, we seem to lose some ground on performance. The new evaluator
is now about 5% slower than the old one on the AES benchmark, and quite a bit
slower on the SHA1 benchmark. Fortunately, the use if LRU caches for memoization
of sequences seems to keep heap usage to manageable levels; so programs generally
complete, even if they take a long time.
Cryptol.Eval.Type now provides three evaluation functions
for types:
evalType :: EvalEnv -> Type -> Either Nat' TValue
evalValType :: EvalEnv -> Type -> TValue
evalNumType :: EvalEnv -> Type -> Nat'
evalValType requires the type to have kind *.
evalNumType requires the type to have kind #.
evalType works on a Cryptol types of either kind.
This mostly takes care of issue #343, but some problems
remain:
- There is no TValue representation for newtypes
- Many incomplete pattern warnings in Symbolic/Prims.hs
