programs: new construct loop ... end for infinite loops

share/emacs/why.el

@@ -30,7 +30,7 @@
    ;; '("(\\*\\([^*)]\\([^*]\\|\\*[^)]\\)*\\)?\\*)" . font-lock-comment-face)
    '("{\\([^}]*\\)}" . font-lock-type-face)
    `(,(why-regexp-opt '("use" "clone" "namespace" "import" "export" "inductive" "external" "logic" "parameter" "exception" "axiom" "lemma" "goal" "type" "mutable" "model" "abstract")) . font-lock-builtin-face)
-   `(,(why-regexp-opt '("and" "any" "match" "let" "rec" "in" "if" "then" "else" "begin" "end" "while" "invariant" "variant" "for" "to" "downto" "do" "done" "label" "assert" "absurd" "assume" "check" "ghost" "try" "with" "theory" "uses" "module")) . font-lock-keyword-face)
+   `(,(why-regexp-opt '("and" "any" "match" "let" "rec" "in" "if" "then" "else" "begin" "end" "while" "invariant" "variant" "for" "to" "downto" "do" "done" "label" "loop" "assert" "absurd" "assume" "check" "ghost" "try" "with" "theory" "uses" "module")) . font-lock-keyword-face)
    ; `(,(why-regexp-opt '("unit" "bool" "int" "float" "prop" "array")) . font-lock-type-face)
    )
   "Minimal highlighting for Why mode")

src/parser/lexer.mll

@@ -92,6 +92,7 @@
 	(* "ghost", GHOST; *)
 	"invariant", INVARIANT;
 	"label", LABEL;
+	"loop", LOOP;
 	"model", MODEL;
 	"module", MODULE;
 	"mutable", MUTABLE;

src/parser/parser.pre.mly

@@ -167,7 +167,7 @@
 
 %token ABSTRACT ABSURD ANY ASSERT ASSUME BEGIN CHECK DO DONE DOWNTO 
 %token EXCEPTION FOR 
-%token FUN INVARIANT LABEL MODEL MODULE MUTABLE PARAMETER RAISE 
+%token FUN INVARIANT LABEL LOOP MODEL MODULE MUTABLE PARAMETER RAISE 
 %token RAISES READS REC TO TRY VARIANT WHILE WRITES
 
 /* symbols */
@@ -1075,7 +1075,7 @@ expr:
    { mk_expr (Ematch (mk_expr (Etuple ($2::$4)), $7)) }
 | LABEL uident COLON expr
    { mk_expr (Elabel ($2, $4)) }
-| DO loop_annotation expr DONE
+| LOOP loop_annotation expr END
    { mk_expr (Eloop ($2, $3)) }
 | WHILE expr DO loop_annotation expr DONE
    { mk_expr

tests/test-pgm-jcf.mlw

@@ -20,10 +20,10 @@ module P
   let foo () =
     {} 
     let x = ref 0 in
-    do 
+    loop 
       x := !x + 1;
       if !x = 100 then raise (Exit !x)
-    done
+    end
     { false } | Exit -> { result = 100 }
 
 end