| Age | Commit message (Collapse) | Author |
|---|
|
|
|
Now constraints on type constructors are checked correctly when
checking that types are well formed using Env.wf_typ. The arity and
kind of type constructor arguments are also checked in the same way.
Also some general cleanups to the type checker code, with some
auxillary functions being moved to more appropriate files.
|
|
There are several key changes here:
1) This commit allows for user defined operations in n-expressions
using the Nexp_app constructor. These operations are linked to
operators in the SMT solver, by using the smt extern when defining
operations. Notably, this allows integer division and modular
arithmetic to be used in types. This is best demonstrated with an
example:
infixl 7 /
infixl 7 %
val operator / = {
smt: "div",
ocaml: "quotient"
} : forall 'n 'm, 'm != 0. (atom('n), atom('m)) -> {'o, 'o = 'n / 'm. atom('o)}
val mod_atom = {
smt: "mod",
ocaml: "modulus"
} : forall 'n 'm. (atom('n), atom('m)) -> {'o, 'o = mod_atom('n, 'm). atom('o)}
val "print_int" : (string, int) -> unit
overload operator % = mod_atom
val main : unit -> unit
function main () = {
let 'm : {'x, 'x % 3 = 1. atom('x)} = 4;
let 'n = m / 3;
_prove(constraint(('m - 1) % 3 = 0));
_prove(constraint('n * 3 + 1 = 'm));
(* let x = 3 / 0; (* Will fail *) *)
print_int("n = ", n);
()
}
As can be seen, these nexp ops can be arbitrary user defined operators
and even operator overloading works (although there are some caveats).
This feature is very experimental, and some things won't work very
well once you use custom operators - notably unification. However,
this not necissarily a downside, because if restrict yourself to the
subset of sail types that correspond to liquid types, then there is
never a need to unify n-expressions. Looking further ahead, if we
switch to a liquid type system a la minisail, then we no longer need
to treat + - and * specially in n-expressions. So possible future
refactorings could involve collapsing the Nexp datatype.
2) The typechecker is stricter about valspecs (and other types) being
well-formed. This is a breaking change because previously we allowed
things like:
val f : atom('n) -> atom('n)
and now this must be
val f : forall 'n. atom('n) -> atom('n)
if we want to allow the first syntax, then initial-check should
desugar it this way - but it must be well-formed by the time it hits
the type-checker, otherwise it's not clear that we do the right
thing. Note we can actually have top-level type variables by using
top-level let bindings with P_var. There's a future line of
refactoring that would make it so that type variables can shadow each
other properly (we should do this) - currently they all have to have
unique names.
3) atom('n) is no longer syntactic sugar for range('n, 'n). The reason
why we want to do this is that if we wanted to be smart about what
sail operations can be translated into SMT operations at the type
level we care very much that they talk about atoms and not
ranges. Why? Because atom is the term level representation of a
specific type variable so it's clear how to map between term level
functions and type level functions, i.e. (atom('n) -> atom('n)) can be
reflected at the type level by a type level function with kind Int ->
Int, but the same is not true for range. Furthermore, both are
interdefinable as
atom('n) -> range('n, 'n)
range('n, 'm) -> {'o, 'n <= 'o <= 'm. atom('n)}
and I think the second is actually slightly more elegant. This change
*should* be backwards compatible, as the type-checker knows how to
convert from atom to ranges and unify them with each other, but there
may be bugs introduced here...
|
|
Possibly useful for Brian's monomorphisation code
|
|
|
|
What does this mean? Basically undefined values can't be created for
types that contain free type variables, so for example: undefined :
list(int) is good, but undefined : list('a) is bad. The reason we want
to do this is because we can't compile them away statically, and this
leads to situations where type-checkable code fails in the rewriter
and gives horribly confusing error messages that don't relate to code
the user wrote at all.
As an example the following used to typecheck, but fail in the
rewriter with a confusing error message, whereas now the typechecker
should reject all cases which would trigger that failure in rewriting.
val test : forall ('a:Type). list('a) -> unit effect {wreg, undef}
function test xs = {
xs_mut = xs;
xs_mut = undefined; (* We don't know what kind of undefined 'a is *)
()
}
There's a slight hitch, namely that in the undefined_type functions
created by the -undefined_gen option, we do want to allow functions
that have polymorphic undefined values, so that we can generate
undefined generators for polymorphic datatypes such as:
union option ('a:Type) = {
Some : 'a,
None
}
These functions are always have a specific form that allows the
rewriter to succesfully remove the polymorphic undefined value for the
'a argument for Sone. As such there's a flag in the typechecking
environment for polymorphic undefineds that is enabled when it sees a
function with the undefined_ name prefix.
Also: Fixed some test cases that were broken due to escape effect being added to assert.
|
|
embedding
Checks for command-line flag -undefined_gen and uses the undefined value
generator functions of the form undefined_typ to initialise registers
|
|
|
|
|
|
|
|
|
|
|
|
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
|
|
- Bitvector pattern rewriting had stopped working due to a line of code being
lost in some merge.
- Fix a bug in early return rewriting that caused returns getting pulled out of
if-statements to disappear.
- There were some variable name clashes with keywords because doc_lem_id was
not always called.
- Ast_util.is_number failed to check for "int" and "nat" built-in types,
causing pattern matching on natural number literals to fail.
|
|
Also improves flow typing in assert statements for ASL parser
This patch does currently introduce a few test failures, probably due
to the new way literals are handled in case statements, which needs to
be investigated and fixed if possible.
|
|
|
|
|
|
|
|
|
|
also rename NC_nat_set_bounded to NC_set (it was an int set not a nat set anyway)
|
|
just LB_val in AST
also rename functions in rewriter.ml appropriately.
|
|
|
|
Also fixed basic ocaml test suite
|
|
as GPR
This was wrongly translated as an update of the vector of references.
|
|
- Support tuples in lexps
- Rewrite trivial sizeofs
- Rewrite early returns more aggressively
- Support let bindings with ticked variables (binding both a type-level and
term-level variable at the same time)
|
|
syntactically correct ocaml
|
|
experiments
|
|
Also, rewrite expressions in global let bindings (not only function bodies)
|
|
Also generate a function which initializes all the registers in a spec to undefined. This gives us the information we need post-rewriting to generate registers of any arbitrary type.
|
|
backed.
Ocaml doesn't support undefined values, so we need a way to remove
them from the specification in order to generate good ocaml
code. There are more subtle issues to - like if we initialize a
mutable variable with an undefined list, then the ocaml runtime has no
way of telling what it's length should be (as this information is
removed by the simple_types pass).
We therefore rewrite undefined literals with calls to functions that
create undefined types, e.g.
(bool) undefined becomes undefined_bool ()
(vector<'n,'m,dec,bit>) undefined becomes undefined_vector(sizeof 'n, sizeof 'm, undefined_bit ())
We therefore have to generate undefined_X functions for any user
defined datatype X. initial_check seems to be the logical place for
this. This is straightforward provided the user defined types are
not-recursive (and it shouldn't be too bad even if they are).
|
|
|
|
Basically we needed to make the rewriting step for E_sizeof and
E_constraint more aggressively try to rewrite those expressions from
variables in scope, without adding new parameters to pass the type
variables at runtime, as this can break in the presence of existential
quantification. Still some cleanup to do in this code, but tests on
the arm spec show that it now introduces the minimal amount of new
parameters.
|
|
|
|
The reason you want this is to do something like (note new parser only):
*********
default Order dec
type bits 'n:Int = vector('n - 1, 'n, dec, bit)
val zeros : forall 'n. atom('n) -> bits('n)
val decode : bool -> unit
function decode b = {
let 'datasize: {|32, 64|} = if b then 32 else 64;
let imm: bits('datasize) = zeros(datasize);
()
}
*********
for the ASL decode functions, where the typechecker now knows that the
datasize variable and the length of imm are the same.
|
|
|
|
to translate exceptions in ASL. See test/typecheck/pass/trycatch.sail.
|
|
Conflicts:
src/pretty_print_common.ml
|
|
- Add some missing "wreg" effect annotations in the type checker
- Improve pretty-printing of register type definitions: In addition to a
"build" function, output an actual type definition, and some getter/setter
functions for register fields
- Fix a bug in sizeof rewriting that caused it to fail when rewriting nested
calls of functions that contained sizeof expressions
- Fix pretty-printing of user-defined union types with type variables (cf. test
case option_either.sail)
- Simplify nexps, e.g. "(8 * 8) - 1" becomes "63", in order to be able to
output more type annotations with bitvector lengths
- Add (back) some support for specifying Lem bindings in val specs using
"val extern ... foo = bar"
- Misc bug fixes
|
|
|
|
|
|
|
|
|
|
|
|
|
|
generation.
|
|
|
|
|
|
Ast_util.string_of_exp
|
