| Age | Commit message (Collapse) | Author |
|---|
|
experiments
|
|
break alpha-equivalence.
|
|
The type-checker already supports a user-defined "exception" type that can be
used in throw and try-catch expressions. This patch adds support for that to
the Lem shallow embedding by adapting the existing exception mechanisms of the
state and prompt monads. User-defined exceptions are distinguished from
builtin exception cases. For example, the state monad uses
type ex 'e =
| Exit
| Assert of string
| Throw of 'e
to distinguish between calls to "exit", failed assertions, and user-defined
exceptions, respectively. Early return is also handled using the exception
mechanism, by lifting to a monad with "either 'r exception" as the exception
type, where 'r is the expected return type and "exception" is the user-defined
exception type.
|
|
Pattern matching against literal numbers is not well supported by Lem or
Isabelle. This rewriting step turns them into guarded patterns (which can be
picked up by the guarded pattern rewriting to if-expressions).
|
|
Was missing the case where the tuple of arguments is bound against a single
variable using P_id (not P_as). Now replaces that with the expected number of
argument variables, and rebinds the single variable in the body, as for the
other cases.
|
|
|
|
|
|
This makes Lem prefer plain "definition" when generating Isabelle output for
functions, which is processed by Isabelle much faster than "fun"/"function"
definitions.
This change is not complete yet, because the Sail library functions still need
to be changed to not use tupled arguments (possibly as part of a bigger
refactoring of the library). For now, external functions are special-cased in
the pretty-printer and get tupled arguments.
|
|
|
|
|
|
|
|
|
|
Improved handling of try/catch
Better handling of unprovable constraints when the environment contains
false
|
|
|
|
Recent patches have made the rewriter more strict about performing
type correct rewrites. This is mostly a good thing but did cause some
problems with the ocaml backend.
Currently the sizeof rewriter doesn't seem to preserve type
correctness - I suspect this is because when it resolves the sizeofs,
it generates constraints that are true, but not in a form where the
typechecker can see that they are true. I disabled the re-check after
the sizeof rewriting pass to fix this. Maybe we don't want to do this
anyway because it's slow.
Changes to function clauses with guards + monomorphisation changed how
the typechecker handles literal patterns. I added a rewriting pass to
rewrite literals to guarded equality checks, which is run before
generating ocaml.
The rewriter currently uses Env.empty in a view places. This can cause
bugs because Env.empty is a totally unitialised environment that
doesn't satisfy invariants we expect of an environment. This should be
changed to initial_env and it shouldn't be exported, I fixed a few
cases where this caused things to go wrong, but it should probably not
be exported from Type_check.ml.
|
|
Also, to support this,
constant propagation for integer multiply,
fix substitution of concrete values for nvars,
size parameters in single argument functions,
fix kind for itself,
add eq_atom to prelude
|
|
|
|
|
|
Breaks parsing ambiguities by removing = as an identifier in the old parser
and requiring parentheses for some expressions in the new parser
|
|
Broke analysis a little
|
|
|
|
Also fix bug in mono analysis with generated variables
Breaks lots of typechecking tests because it generates unnecessary
equality tests on units (and the tests don't have generic equality),
which I'll fix next.
|
|
|
|
- Add support for some internal nodes to type checker
- Add more explicit type annotations during rewriting
- Remove hardcoded rewrites for E_vector_update etc from Lem pretty-printer;
these will be resolved by the type checker during rewriting now
|
|
|
|
|
|
Also some simple rules to try to format if statements better based on
contents while pretty printing.
|
|
|
|
|
|
|
|
steps
Parser now has syntax for mutual recusion blocks
mutual {
... fundefs ...
}
which is used for parsing and pretty printing
DEF_internal_mutrec. It's stripped away by the initial_check, so the
typechecker never sees DEF_internal_mutrec. Maybe this could change,
as forcing mutual recursion to be explicit would probably be a good
thing.
Added record syntax to the new parser
New option -dmagic_hash is similar to GHC's -XMagicHash in that it
allows for identifiers to contain the special hash character, which is
used to introduce new autogenerated variables in a way that doesn't
clash with existing names.
Option -sil compiles sail down to the intermediate language defined in
sil.ott (not complete yet).
|
|
|
|
|
|
|
|
|
|
|
|
aarch64 vector instructions.
There's maybe a better more general way to do this but I'm not sure
what that would be.
|
|
|
|
|
|
As discussed previously, we wanted to start refactoring the re-writer
to make it a bit less monolithic, and in the future potentially break
it into separate files for backend-specific rewrites and stuff.
- rewriter.ml now contains the generic re-writing code
- rewrites.ml contains the rewriting passes themselves
It would be nice if the generic rewriting code didn't depend on the
typechecker, because then it could be used in ASL parser on untyped
code.
|
|
|
|
experiments
|
|
and_bool and or_bool now are treated specially in the ocaml backend,
so that they have the correct short-circuiting behaviour. This is
required so that assertions don't fail for the ARM spec for predicates
that shouldn't be tested in certain circumstances, for example things like:
IsAArch32() && AArch32_specific_predicate
Also fixed an issue in the sail library for ocaml where greater than
or equal to was being mapped to greater than.
|
|
|
|
|
|
(mostly to make test cases easier)
|
|
Alastair's test cases revealed that using regular ints causes issues
throughout sail, where all kinds of things can internally overflow in
edge cases. This either causes crashes (e.g. int_of_string fails for
big ints) or bizarre inexplicable behaviour. This patch switches the
sail AST to use big_int rather than int, and updates everything
accordingly.
This touches everything and there may be bugs where I mistranslated
things, and also n = m will still typecheck with big_ints but fail at
runtime (ocaml seems to have decided that static typing is unnecessary
for equality...), as it needs to be changed to eq_big_int.
I also got rid of the old unused ocaml backend while I was updating
things, so as to not have to fix it.
|
|
|
|
Use overloading to find eq/neq
Track range/atom split
Missing type expansion
|
|
experiments
|
