| Age | Commit message (Collapse) | Author |
|---|
|
rewrite_defs_pat_lits
|
|
Changes the representation of function types in the ast from
Typ_fn : typ -> typ
to
Typ_fn : typ list -> typ
to more accurately represent their use in the various backends, where we often compile functions to either their curried representations as in Lem and Isabelle, or just
multiple argument functions in C. There's still some oddity because a single pattern in a function clause can bind against multiple arguments, and maybe we want to
forbid this in the future. The syntax also hasn't changed (yet), so in theory this change shouldn't break anything (but it invariably will...).
In the future we would ideally require that a function with N arguments has exactly N patterns in its declaration, one for each argument so
f : (x, y) -> z
f _ = ...
would be disallowed (as _ matches both x and y), forcing
f(_, _) = z
this would simply quite a few things,
Also we could have a different syntax for function argument lists and tuples, because it's rather hard to define a function that actually takes a tuple with the syntax
how it is now.
Some issues I noticed when doing this refactoring:
Line 1926 of Coq translation. untuple_args_pat is maybe no longer needed? However there's still some funnyness where a pattern can be used to bind multiple function
arguments so maybe it still is.
Line 2306 of monomorphisation. I simplified the logic here. I think it's equivalent now, but I could be wrong.
Line 4517 of rewrites. I'm not sure what make_cstr_mappings is doing here, but hopefully the simpler version is the same.
|
|
|
|
|
|
Handles the common case of a single level string append pattern in a
way designed to be friendlier to Coq etc, by generating an auxiliary
function for each pattern rather than emitting a massive nested
pattern match twice.
|
|
When converting to A-normal form I just used the type of the then
branch of if statements to get the type of the whole if statement -
usually they'd be the same, but with flow typing one of the branches
can have a false constraint, which then allows the optimizer to fit
any integer into a 64-bit integer causing an overflow. The fix is to
correctly use the type the typechecker gives for the whole if
statement.
Also add decimal_string_of_bits to the C output.
Rename is_reftyp to is_ref_typ to be more consistent with other
is_X_typ functions in Ast_util.
|
|
- more hex_bits functions, add decimal_string_of_bits
- extra tuple unfolding in constructors
- note that variables can be redundant wildcard clauses
- update RISC-V patch
|
|
|
|
the generated pattern so re-typechecking works
|
|
Assigning to an uninitialized variable as the last statement in a
block is almost certainly a type, and if that occurs then the
lift_assign re-write will introduce empty blocks causing this error to
occur. Now when we see such an empty block when converting to A-normal
form we turn it into unit, and emit a warning stating that an empty
block has been found as well as the probable cause (uninitialized
variable).
|
|
Now that Jenkins is updated to a newer version of OCaml we can finally
fix some warning with more recent versions of OCaml than 4.02.3. Also
fix a Lem test case that was failing.
|
|
Particularly useful when execute has been split up (e.g., on RISC-V).
Only enabled on Coq for now.
|
|
and use the original ids rather than fresh ones; both to allow referring to matched ids in guards
|
|
|
|
|
|
Allow pat_lits rewrite to map L_unit to wildcard patterns, rather than
introducing eq_unit tests as guards.
Add a fold_function and fold_funcl functions in rewriter.ml that apply
the pattern and expression algebras to top-level functions, which
means that they correctly get applied to top-level function patterns
when they are used. Currently modifying the re-writing passes to do
this introduces some bugs which needs investigated further. The
current situation is that top-level patterns and patterns elsewhere
are often treated differently because rewrite_exp doesn't (and indeed
cannot, due to how the re-writer is structured) rewrite top level
patterns.
Fix pattern completeness check for unit literals
Fix a bug in Sail->ANF transform where blocks were always annotated
with type unit incorrectly. This caused issues in pattern literal
re-writes where the guard was a block returning a boolean. A test case
for this is added as test/c/and_block.sail.
Fix a bug caused by nested polymorphic function calls and matching in
top-level patterns. Test case is test/c/tl_poly_match.sail.
Pass location info through codegen_conversion for better error
reporting
|
|
|
|
guards
|
|
exp_of_mpat
|
|
cleaner generated code and reduced compiler warnings
|
|
Interpreter used a re-write (vector concat removal) that is dependent
on the vector_string_to_bit_list rewriting pass. This fixes the
interpreter to work without either vector concat removal, or turning
bitstrings into vector literals like [bitzero, bitzero, bitone]. This
has the upside of reducing the number of steps the interpreter needs
for working with bitvectors so should improve interpreter performance.
We also now test all the C compilation tests behave the same using the
interpreter. Currently the real number tests fail due to limitations
of Lem's rational library (this must be fixed in Lem). This required
supporting configuration registers in the interpreter. As such the
interpreter was refactored to more cleanly process registers when
building an initial global state. The functions are also collected
into the global state, which removes the need to search for them in
the AST every time a function call happens. This should not only
improve performance, but also removes the need to pass an AST into the
interpretation functions.
|
|
an explicit rewrite step in Rewrites, just before pat_lits
|
|
|
|
generated id pattern"
This reverts commit 9fdd1ecbed32ebb408256628b6661ccbf5f16c18.
|
|
pattern
|
|
Also fix nested matches and generic rewriting under E_throw.
|
|
Tweak extra Coq files to match.
Tweak early return rewrite to use declared return type, which can always
be put into an E_cast.
|
|
Deals with pattern matches generated from mappings, plus the occasional
error.
|
|
Prevents redundant clauses.
|
|
|
|
|
|
Rather than exporting the implementation of type annotations as
type tannot = (Env.t * typ * effect) option
we leave it abstract as
type tannot
Some additional functions have been added to type_check.mli to work
with these abstract type annotations. Most use cases where the type
was constructed explicitly can be handled by using either mk_tannot or
empty_tannot. For pattern matching on a tannot there is a function
val destruct_tannot : tannot -> (Env.t * typ * effect) option
Note that it is specifically not guaranteed that using mk_tannot on
the elements returned by destruct_tannot re-constructs the same
tannot, as destruct_tannot is only used to give the old view of a type
annotation, and we may add additional information that will not be
returned by destruct_tannot.
|
|
|
|
These match the new ASL pattern constructors:
- !p matches if the pattern p does not match
- { p1, ... pn } matches if any of the patterns p1 ... pn match
We desugar the set pattern "{p1, ... pn}" into "p1 | (p2 | ... pn)".
ASL does not have pattern binding but Sail does. The rules at the
moment are that none of the pattern can contain patterns. This could
be relaxed by allowing "p1 | p2" to bind variables provided p1 and p2
both bind the same variables.
|
|
E_internal_cast, E_sizeof_internal, E_internal_exp,
E_internal_exp_user, E_comment, and E_comment_struc were all
unused. For a lem based interpreter, we want to be able to compile it
to iUsabelle, and due to slowness inherent in Isabelle's datatype
package we want to remove unused constructors in our AST type.
Also remove the lem_ast backend - it's heavily bitrotted, and for
loading the ARM ast into the interpreter it's just not viable to use
this approach as it just doesn't scale. We really need a way to be
able to serialise and deserialise the AST efficiently in Lem.
|
|
Fixes monomorphisation on files using mappings.
Also extended constant propagation to handle pattern matches on
bitvector expressions (because an earlier rewrite replaces the literals).
Also moved L_undef rewriting because monomorphisation can handle them
but not the replacement functions.
|
|
Uses previous stage to deal with (e.g.) guards.
New option -dcoq_warn_nonex tells you where all of the extra default
cases were added.
|
|
|
|
|
|
|
|
|
|
|
|
Necessary to prevent redundant clauses that Coq will reject
(There's still a problem if you use a variable rather than a wildcard,
see the test)
|
|
|
|
Remember and use fallthrough clauses instead of dropping them when the last
clause in a group has a guard
|
|
|
|
(involved some manual tinkering with gitignore, type_check, riscv)
|
|
We now store the location where type variables were bound, so we can
use this information when printing error messages.
Factor type errors out into type_error.ml. This means that
Type_check.check is now Type_error.check, as it previously it handled
wrapping the type_errors into reporting_basic
errors. Type_check.check' has therefore been renamed to
Type_check.check.
|
|
multiple arguments weren't type-checking correctly
|
|
|
