| Age | Commit message (Collapse) | Author |
|---|
|
Fixed some bugs in the initial check that caused valid code to fail to
parse
Add a nid utility function that creates an id n-expression, similar to
nvar, nconstant etc
|
|
See test/typecheck/pass/cons_pattern.sail for an example.
Also cleaned up the propagating effects code by making some of the
variable names less verbose
|
|
Modified initial_check.ml so it no longer requires type_internal. It's
still needs cleaned up in a few ways. Most of the things it's trying
to do could be done nicer if we took some time to re-factor it, and
some of the things should just be handled by the main typechecker,
leaving it as a think layer between the parse_ast and the ast.
Now that's done everything can be switched to the new typechecker and
the _new suffixes were deleted from everything except the
monomorphisation pass because I don't know the status of that.
|
|
1) Added a new construct to the expression level: constraint. This is the
essentially the boolean form of sizeof. Whereas sizeof takes a nexp
and has type [:'n:], constraint takes a n_constraint and returns a
boolean. The hope is this will allow for flow typing to be represented
more explicitly in the generatated sail from ASL.
For example we could have something like:
default Order dec
val bit[64] -> unit effect pure test64
val forall 'n, ('n = 32 | 'n = 64 | 'n = 10) & 'n != 43. bit['n] -> unit effect pure test
function forall 'n. unit test addr =
{
if constraint('n = 32) then {
()
} else {
assert(constraint('n = 64), "64-bit mode");
test64(addr)
}
}
2) The other thing this example demonstrates is that flow constraints
now work with assert and not just if. Even though flow typing will
only guarantee us that 'n != 32 in the else branch, the assert gives
us 'n = 64. This is very useful as it's a common idiom in the ARM
spec to guarantee such things with an assert.
3) Added != to the n_constraint language
4) Changed the n_constraint language to add or and and as constructs
in constraints. Previously one could have a list of conjuncts each of
which were simple inequalites or set constraints, now one can do for
example:
val forall 'n, ('n = 32 | 'n = 64) & 'n in {32, 64}. bit['n] -> unit effect pure test
This has the very nice upside that every n_constraint can now be
negatated when flow-typing if statements. Note also that 'in' has been
introduced as a synonym for 'IN' in the constraint 'n in {32,64}. The
use of a block capital keyword was a bit odd there because all the
other keywords are lowercase.
|
|
|
|
Introduces a when keyword for case statements, as the Pat_when constructor for pexp's in the AST. This allows us to write things like:
typedef T = const union { int C1; int C2 }
function int test ((int) x, (T) y) =
switch y {
case (C1(z)) when z == 0 -> 0
case (C1(z)) when z != 0 -> x quot z
case (C2(z)) -> z
}
this should make translation from ASL's patterns much more straightforward
|
|
* Experimented with using list<bit> to clean up manually monomorphised code in MIPS tlb
* Added option -dtc_verbose to control verbosity of new typechecker
* Allowed functions with val specs to omit their type declarations
|
|
New typechecker has no builtin overloaded operators - instead can now
write something in SAIL like:
overload (deinfix +) [id1; id2; id3]
to set up functions id1, id2, and id3 as overloadings for the +
operator. Any identifier can be overloaded, not just infix ones. This
is done in a backwards compatible way, so the old typechecker removes
the DEF_overload nodes from the ast so the various backends never see
it.
|
|
Added a new feature for implicit casts - now allowable implicit casts
can be specified by the user via a valspec such as
val cast forall Type 'a, Type 'b. 'a -> 'b effect pure cast_anything
with a new AST constructor to represent this as VS_cast_spec. This
constructor is removed and replaced with the standard val spec by the
old typechecker for backwards compatability, so it's only used by the
new typechecker, and won't appear in the ast once it reaches the
backends.
Also added Num as a synonym for the Nat kind in the parser, via the
confusingly named NatNum token (Num by itself was already taken for a
numeric constant).
|
|
# Conflicts:
# src/lem_interp/interp.lem
# src/lem_interp/interp_inter_imp.lem
# src/lem_interp/interp_interface.lem
# src/parser.mly
# src/pretty_print_lem.ml
|
|
|
|
data and invent rmemt and wmvt effects for them. Extend the interpreter context to include lists of tagged memory read and write functions. The memory model must round down the address to the nearest capability aligned address when reading/writing tags. Remove TAGw which is no longer needed as a result.
|
|
|
|
Not working yet
|
|
just an id (hopefully fixes Christopher issue).
|
|
TODO: add an event for a return so that rewriters can find and remove them as needed for OCaml and Lem
|
|
|
|
well as items of kind Type.
Syntax for the feature is:
def Nat id = nexp
Note: some useful nexps may not parse properly.
All typedef forms can also be used as def Type ... if desired, but this is not required.
|
|
Improve printing for asl to sail readability;
Add -o option for selecting the name of file generation;
Add additional initial check module for turning generated ast nodes into ready-to-type-check ast nodes
|
|
This splits the former functionality of exit into errors, which should now use assert(bool,option<string>), and a means of signalling actions such as instruction-level exceptions, interrupts, or other features that impact the ISA. The latter will now be tracked with an effect escape, and so any function containing exit and declared pure will generate a type error.
WARNING: ARM spec will not build with this commit until I modify it. MIPS spec will not build with this commit until modified.
|
|
Events are eamem to signal the memory address to write to and wmv to pass the value to write
|
|
declared return type when consistent instead of using the derived one.
|
|
Also fix type checker bug in not reporting modifications to parameter values
|
|
Fix up parsing on 2** precedence
Fix errors on type variables in function definition
|
|
Fix bug allowing function types in too many places
|
|
function-clause
|
|
|
|
will be reflected in short hand type syntax, inc is still the default if undeclared
So:
default order dec
register bit[32] t (* Declares t as a decreasing vector, starting at 31 on the left and decreasing to 0 *)
default order inc
register bit[32] o (* Declares o as an increasing vector, starting at 0 on the left and increasing to 31 *)
It is presently possible to change the default mid-file; this is almost certainly bad and I will turn it into an error soon.
|
|
|
|
interpreter.
An alias can be read within the interpreter, but not written to. Exits aren't yet taken in the interpreter.
|
|
Also begining to add support for nondeterministic blocks and cleaning up some of the Many warnings on pattern matches
|
|
|
|
|
|
Reduce the number of implicit coercions we're doing, expanding overloading and fixing up types of functions.
Warning: test_power does not run as not all overloaded funcitons are implemented
Warning: vector concatenation does not pretty print to sail source yet
|
|
functions for connecting the interpreter to a memory model)
Also adding default values to index vectors for supporting sparse vectors/maps
|
|
number of coercions
|
|
uses appropriate information gleaned from pattern matching
|
|
|
|
from 0 to 32 etc, doesn't change order yet.).
|
|
assigned to in assignments.
|
|
|
|
ast, and extending the interpreter to expect annotations.
Annotations and locations are still not used by the interpreter.
|
|
|
|
|
|
definition environment. Skipping function definition, let bind, and expression checking for this commit (to come).
|
|
|
|
Could not at this time return lists to [| |] from [|| ||] as the parser cannot distinguish a cast with enum’s syntactic sugar from the start of a parenthesised list (i.e. ( [|3|] ) And there are still conflicts with moving enums to [3], so those changes can’t be pushed in with current parser technology.
|
|
|
|
First pass parser to identify type names is in progress (current test files fail, will correct once pre-parser is in place)
|
|
Added val extern specification to language, parser, printer, and interpreter
Added various def level type system support, expressions type system in place Except for assignment
|
