| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
embedding
Checks for command-line flag -undefined_gen and uses the undefined value
generator functions of the form undefined_typ to initialise registers
|
|
|
|
|
|
Translates atom('n) types into itself('n) types that won't be erased
Also exports more rewriting functions
|
|
|
|
|
|
See README file for how to set up and use
|
|
|
|
Map to calls to monadic function assert_exp that throws an exception if the
assertion is false
|
|
Put them before the function they declare
|
|
|
|
|
|
experiments
|
|
|
|
|
|
|
|
Cleaned up the option list in sail.ml
|
|
|
|
|
|
|
|
|
|
Fix until loop not being counted as sugar
|
|
|
|
|
|
(complains due to added val spec)
|
|
|
|
the same name between sail and the target
|
|
(includes variables for bitvector sizes)
|
|
appear in the output
|
|
checking that the type variables visible in the output aren't
existential
|
|
|
|
|
|
|
|
|
|
Also added some new utility functions in ast_util
|
|
Fixed an issue in ast.ml with uneccessary type variables
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Fixes a bug where resolving a type synonym failed in the Lem pretty-printer due
to a missing type environment.
|
|
|
|
|
|
(and fix up monomorphisation)
|
|
|
|
|
