| Age | Commit message (Collapse) | Author |
|---|
|
|
|
(rather than for each argument separately)
|
|
Previously we only did top-level literal pattern to guard conversion, this
does it throughout any pattern
|
|
Otherwise the type checker can't figure it out when we substitute
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
consistent names
|
|
|
|
|
|
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).
|
|
|
|
|
|
|
|
|
|
|
