| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
Currently not enabled by default, the flag -Xconstraint_synonyms
enables them
For generating constraints in ASL parser, we want to be able to give
names to the constraints that we attach to certain variables. It's
slightly awkward right now when constraints get long complicated
because the entire constraint always has to be typed out in full
whenever it appears, and there's no way to abstract away from that.
This adds constraint synonyms, which work much like type synonyms
except for constraints, e.g.
constraint Size('n) = 'n in {1, 2, 4, 8} | 128 <= 'n <= 256
these constraints can then be used instead of the full constraint, e.g.
val f : forall 'n, where Size('n). int('n) -> unit
Unfortunatly we need to have a keyword to 'call' the constraint
synonym otherwise the grammer stops being LR(1). This could be
resolved by parsing all constraints into Parse_ast.atyp and then
de-sugaring them into constraints, which is what happens for
n-expressions already, but that would require quite a bit of work on
the parser.
To avoid this forcing changes to any other parts of Sail, the intended
invariant is that all constraints appearing anywhere in a type-checked
AST have no constraint synonyms, so they don't have to worry about
matching on NC_app, or calling Env.expand_typquant_synonyms (which
isn't even exported for this reason).
|
|
response and refactor RISC-V model accordingly
|
|
undefined on startup
|
|
|
|
|
|
(Adds 'interpreter' externs as appropriate.)
|
|
And update the RISC-V patch accordingly.
|
|
|
|
Make lem output understand difference between functions taking a tuple
and functions taking multiple arguments. Previously it assumed that no
functions ever took a tuple as an argument, which is incorrect for
mappings.
|
|
|
|
actually take a tuple argument
|
|
|
|
Uses new primop 'string_take' which is much easier to implement in e.g. C
|
|
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.
|
|
|
|
monad
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
(aimed at RISC-V)
|
|
|
|
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.
|
|
When constructing expressions, we need to provide locations for the
generated expressions to give useful error messages. However adding
these at every mk_X function in ast_util would be very verbose,
especially for complex expressions.
Add new locate_X functions (with the one for expressions simply being
called locate), which take a location and recursively apply it to
every child node, e.g.
locate (gen_loc l) (mk_exp (... (mk_exp ..., mk_exp ...)))
would mark every part of the constructed expression as being generated
from code at location l.
|
|
|
|
(This leads to more redundant uses, but I'll tackle that later)
|
|
|
|
- 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
|
|
|
|
|
|
hex_bits_N_matches_prefix
|
|
This really demonstrates why we should switch to Typ_fn being a typ
list * typ constructor because the implementation here feels *really*
hacky with dummy Typ_tup constructors being used to enforce single
arguments for constructors.
|
|
|
|
|
|
- hints for dotp
- handle exists separately when trying eauto to keep search depth low
- more uniform existential handling (i.e., we now handle all existentials
in the way we used to only handle existentials around atoms)
|
|
Broke E_internal_plet on some simple existential types
|
|
the generated pattern so re-typechecking works
|
