Improvements to implicit type casting

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).

1 files changed, 3 insertions, 3 deletions

diff --git a/editors/sail-mode.el b/editors/sail-mode.el
index 4aa8e9eb..1e34e205 100644
--- a/editors/sail-mode.el
+++ b/editors/sail-mode.el
@@ -640,7 +640,7 @@ though, if you also have `sail-electric-indent' on."
     (setq sail-mode-abbrev-table (make-abbrev-table))
   (mapc 'sail-define-abbrev
         '("scattered" "function" "typedef" "let" "default" "val" "register"
-          "alias" "union" "member" "clause" "extern" "effect"
+          "alias" "union" "member" "clause" "extern" "cast" "effect"
           "rec" "and" "switch" "case" "exit" "foreach" "from" "else"
           "to" "end" "downto" "in" "then" "with" "if" "nondet" "as"
 	  "undefined" "const" "struct" "IN" "deinfix" "return" "sizeof"))
@@ -708,7 +708,7 @@ Based on Tuareg mode. See Tuareg mode for usage"
 (defun sail-install-font-lock ()
   (setq
    sail-font-lock-keywords
-   `(("\\<\\(extern\\|function\\|scattered\\|clause\\|effect\\|default\\|struct\\|const\\|union\\|val\\|typedef\\|in\\|let\\|rec\\|and\\|end\\|register\\|alias\\|member\\|enumerate\\)\\>"
+   `(("\\<\\(extern\\|cast\\|function\\|scattered\\|clause\\|effect\\|default\\|struct\\|const\\|union\\|val\\|typedef\\|in\\|let\\|rec\\|and\\|end\\|register\\|alias\\|member\\|enumerate\\)\\>"
       0 sail-font-lock-governing-face nil nil)
      ("\\<\\(false\\|true\\|bitzero\\|bitone\\|0x[:xdigit:]\\|[:digit:]\\)\\>" 0 font-lock-constant-face nil nil)
      ("\\<\\(as\\|downto\\|else\\|foreach\\|if\\|t\\(hen\\|o\\)\\|when\\|switch\\|with\\|case\\|exit\\|sizeof\\|nondet\\|from\\|by\\|return\\)\\>"
@@ -717,7 +717,7 @@ Based on Tuareg mode. See Tuareg mode for usage"
       2 font-lock-variable-name-face keep nil)
      ("\\<\\(typedef\\|union\\)\\>[ \t\n]*\\(\\(\\w\\|[_ \t()*,]\\)+\\)"
       2 font-lock-type-face keep nil)
-     ("\\<\\(Type\\|Nat\\|Order\\|Effect\\|inc\\|dec\\|implicit\\|vector\\|rreg\\|wreg\\|rmem\\|wmem\\|wmv\\|eamem\\|barr\\|undef\\|escape\\|unspec\\|nondet\\|pure\\|effect\\|IN\\|forall\\|bit\\|unit\\|bool\\|nat\\|int\\)\\>"
+     ("\\<\\(Type\\|Nat\\|Num\\|Order\\|Effect\\|inc\\|dec\\|implicit\\|vector\\|rreg\\|wreg\\|rmem\\|wmem\\|wmv\\|eamem\\|barr\\|undef\\|escape\\|unspec\\|nondet\\|pure\\|effect\\|IN\\|forall\\|bit\\|unit\\|bool\\|nat\\|int\\)\\>"
       0 font-lock-type-face keep nil)
      ("\\<\\(val\\|extern\\|clause\\|and\\||let\\|rec\\>[ \t\n]*\\(\\(\\w\\|[_,?~.]\\)*\\)"
       2 font-lock-variable-name-face keep nil)