| Age | Commit message (Collapse) | Author |
|---|
|
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.
|
|
|
|
|
|
Also interpreter now supports reading and writing of basic registers (i.e with no subranges yet)
|
|
|
|
|
|
of kind and type system
|
|
Syntax:
foreach id from exp (to|downto) exp (by exp)? exp
foreach and by are keywords; from, to and downto aren't.
|
|
to support type casts; syntax changes not yet reflected in ott file
|
|
|
|
The ott files have been adjusted to reflect some syntax changes in typquant specifications, and the type annotations are not optional for function definitions; we need additional syntax to help the parser if we want to allow functions without type annotations.
|
|
|
|
Output is only given in the event of a parse or lex failure (with poor reporting for now)
There are still 10 shift/reduce conflicts that may need further investigating and a few syntax changes that need discussion.
|
|
|
|
syntax needs to change.
ott file now builds a pdf again
|
|
|
|
|
|
|
|
|
