Add a return exp form to Sail, supported in type checker and in interpreter.

TODO: add an event for a return so that rewriters can find and remove them as needed for OCaml and Lem

1 files changed, 1 insertions, 0 deletions

diff --git a/language/l2_parse.ott b/language/l2_parse.ott
index d768c766..f1e994f6 100644
--- a/language/l2_parse.ott
+++ b/language/l2_parse.ott
@@ -546,6 +546,7 @@ exp :: 'E_' ::=
 
   | sizeof atyp                                         :: :: sizeof
   | exit exp						:: :: exit
+  | return exp                                          :: :: return
   | assert ( exp , exp' )                               :: :: assert
 
   | ( exp )                                             :: S :: paren {{ ichlo [[exp]] }}