From 05c2d0f45dcc632a11b4868b04776c1916b41454 Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Wed, 3 Jan 2018 18:50:21 +0000 Subject: Lots of experimental changes on this branch * Changed comment syntax to C-style /* */ and // * References to registers and mutable variables are never created implicitly - a reference to a register or variable R is now created via the expression "ref R". References are assigned like "(*Y) = X", with "(*ref R) = X" being equivalent to "R = X". Everything is always explicit now, which simplifies the logic in the typechecker. There's also now an invariant that every id directly in a LEXP is mutable, which is actually required for our rewriter steps to be sound. * More flexible syntax for L-expressions to better support wierd power-idioms, some syntax sugar means that: X.GET(a, b, c) ==> _mod_GET(X, a, b, c) X->GET(a, b, c) ==> _mod_GET(ref X, a, b, c) for setters, this can be combined with the (still somewhat poorly named) LEXP_memory construct, such that: X->SET(a, b, c) = Y ==> _mod_SET(ref X, a, b, c, Y) Currently I use the _mod_ prefix for these 'modifier' functions, but we could omit that a la rust. * The register bits typedef construct no longer exists in the typechecker. This construct never worked consistently between backends and inc/dec vectors, and it can be easily replaced by structs with fancy setters/getters if need be. One can also use custom type operators to mimic the syntax, i.e. type operator ... ('n : Int) ('m : Int) = slice('n, 'm) struct cr = { CR0 : 32 ... 35, /* 32 : LT; 33 : GT; 34 : EQ; 35 : SO; */ CR1 : 36 ... 39, /* 36 : FX; 37 : FEX; 38 : VX; 39 : OX; */ CR2 : 40 ... 43, CR3 : 44 ... 47, CR4 : 48 ... 51, CR5 : 52 ... 55, CR6 : 56 ... 59, CR7 : 60 ... 63, } This greatly simplifies a lot of the logic in the typechecker, as it means that E_field is no longer ambiguously overloaded between records and register bit typedefs. This also makes writing semantics for these constructs much simpler. --- src/rewrites.mli | 3 +++ 1 file changed, 3 insertions(+) (limited to 'src/rewrites.mli') diff --git a/src/rewrites.mli b/src/rewrites.mli index ce24a4c4..8fceadff 100644 --- a/src/rewrites.mli +++ b/src/rewrites.mli @@ -57,6 +57,9 @@ val rewrite_undefined : bool -> tannot defs -> tannot defs (* Perform rewrites to exclude AST nodes not supported for ocaml out*) val rewrite_defs_ocaml : (string * (tannot defs -> tannot defs)) list +(* Perform rewrites to exclude AST nodes not supported for interpreter *) +val rewrite_defs_interpreter : (string * (tannot defs -> tannot defs)) list + (* Perform rewrites to exclude AST nodes not supported for lem out*) val rewrite_defs_lem : (string * (tannot defs -> tannot defs)) list -- cgit v1.2.3