From 79b81722d8cfe3c2c2fa16bbc8643e8243dfa015 Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Fri, 21 Jul 2017 17:31:08 +0100
Subject: Add a prove builtin that allows testing flow typing

For example:

default Order dec

val bit[64] -> unit effect pure test64

val cast forall 'n, 'n = 32 | 'n = 64. bit['n] -> unit effect pure test

function forall 'n. unit test addr =
{
  _prove(constraint('n != 16));
  assert(constraint('n = 64), "64-bit mode");
  _prove(constraint('n = 64));
  test64(addr);
}

This doesn't affect the AST at all as _prove is just a ordinary function
that the typechecker treats specially.
---
 editors/sail-mode.el | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'editors')

diff --git a/editors/sail-mode.el b/editors/sail-mode.el
index c898fc1e..96059a3f 100644
--- a/editors/sail-mode.el
+++ b/editors/sail-mode.el
@@ -710,6 +710,8 @@ Based on Tuareg mode. See Tuareg mode for usage"
    sail-font-lock-keywords
    `(("\\<\\(extern\\|cast\\|overload\\|deinfix\\|function\\|scattered\\|clause\\|effect\\|default\\|struct\\|const\\|union\\|val\\|typedef\\|let\\|rec\\|and\\|end\\|register\\|alias\\|member\\|enumerate\\)\\>"
       0 sail-font-lock-governing-face nil nil)
+     ("\\<\\(_prove\\)\\>"
+      0 font-lock-preprocessor-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\\|in\\|switch\\|with\\|case\\|when\\|exit\\|constraint\\|sizeof\\|nondet\\|from\\|by\\|return\\)\\>"
       0 font-lock-keyword-face nil nil)
@@ -724,7 +726,7 @@ Based on Tuareg mode. See Tuareg mode for usage"
      ("\\<\\(val\\|and\\|let\\>[ \t\n]*\\(\\(\\w\\|[_,?~.]\\)*\\)\\>\\(\\(\\w\\|[->_ \t,?~.]\\|(\\(\\w\\|[--->_ \t,?~.=]\\)*)\\)*\\)"
       6 font-lock-variable-name-face keep nil)
      ("\\<\\([?~]?[_[:alpha:]]\\w*\\)[ \t\n]*:[^:>=]"
-      1 font-lock-variable-name-face keep nil)
+      0 font-lock-variable-name-face keep nil)
      ("^#\\w+\\>" 0 font-lock-preprocessor-face t nil)
      ))
   (setq font-lock-defaults
-- 
cgit v1.2.3