Simpler implicit arguments

Rather than using sizeof-rewriting which is slow and error-prone, just
make implicit function arguments explicit, so:

val ZeroExtend : forall 'n 'm, 'm >= 'n. (implicit('m), bits('n)) -> bits('m)
let x : bits(32) = ZeroExtend(0xFFFF)

would be re-written (by the typechecker itself) into

val ZeroExtend : forall 'n 'm, 'm >= 'n. (implicit('m), bits('n)) -> bits('m)
let x : bits(32) = ZeroExtend(32, 0xFFFF)

then all we need to do is map implicit -> int in a rewrite, and use
trivial sizeof-rewriting only. We pretty much never want to use the
form of sizeof-rewriting that propagates function arguments through
multiple functions because it's extremely error-prone. Anything that
isn't re-writable via trivial sizeof rewriting should be a type error,
so it would be good to re-write sizeof expressions within the
type-checker.

1 files changed, 1 insertions, 1 deletions

diff --git a/editors/sail-mode.el b/editors/sail-mode.el
index b1adccaf..25181fea 100644
--- a/editors/sail-mode.el
+++ b/editors/sail-mode.el
@@ -30,7 +30,7 @@
     "overload" "cast" "sizeof" "constant" "constraint" "default" "assert" "newtype" "from"
     "pure" "infixl" "infixr" "infix" "scattered" "end" "try" "catch" "and" "to"
     "throw" "clause" "as" "repeat" "until" "while" "do" "foreach" "bitfield"
-    "mapping" "where" "with"))
+    "mapping" "where" "with" "implicit"))
 
 (defconst sail2-kinds
   '("Int" "Type" "Order" "Bool" "inc" "dec"