diff options
Diffstat (limited to 'language')
| -rw-r--r-- | language/l2.lem | 1 | ||||
| -rw-r--r-- | language/l2.ml | 1 | ||||
| -rw-r--r-- | language/l2.ott | 3 | ||||
| -rw-r--r-- | language/l2_parse.ml | 1 | ||||
| -rw-r--r-- | language/l2_parse.ott | 1 |
5 files changed, 6 insertions, 1 deletions
diff --git a/language/l2.lem b/language/l2.lem index dd300c89..94c93fe5 100644 --- a/language/l2.lem +++ b/language/l2.lem @@ -257,6 +257,7 @@ type exp_aux 'a = (* Expression *) | E_assign of (lexp 'a) * (exp 'a) (* imperative assignment *) | E_sizeof of nexp (* Expression to return the value of the nexp variable or expression at run time *) | E_exit of (exp 'a) (* expression to halt all current execution, potentially calling a system, trap, or interrupt handler with exp *) + | E_return of (exp 'a) (* expression to end current function execution and return the value of exp from the function; this can be used to break out of for loops *) | E_assert of (exp 'a) * (exp 'a) (* expression to halt with error, when the first expression is false, reporting the optional string as an error *) | E_internal_cast of annot 'a * (exp 'a) (* This is an internal cast, generated during type checking that will resolve into a syntactic cast after *) | E_internal_exp of annot 'a (* This is an internal use for passing nexp information to library functions, postponed for constraint solving *) diff --git a/language/l2.ml b/language/l2.ml index 931bc01f..39f430db 100644 --- a/language/l2.ml +++ b/language/l2.ml @@ -271,6 +271,7 @@ type | E_assign of 'a lexp * 'a exp (* imperative assignment *) | E_sizeof of nexp (* Expression to return the value of the nexp variable or expression at run time *) | E_exit of 'a exp (* expression to halt all current execution, potentially calling a system, trap, or interrupt handler with exp *) + | E_return of 'a exp (* expression to end current function execution and return the value of exp from the function; this can be used to break out of for loops *) | E_assert of 'a exp * 'a exp (* expression to halt with error, when the first expression is false, reporting the optional string as an error *) | E_internal_cast of 'a annot * 'a exp (* This is an internal cast, generated during type checking that will resolve into a syntactic cast after *) | E_internal_exp of 'a annot (* This is an internal use for passing nexp information to library functions, postponed for constraint solving *) diff --git a/language/l2.ott b/language/l2.ott index 4af3b9a3..96a30265 100644 --- a/language/l2.ott +++ b/language/l2.ott @@ -667,6 +667,7 @@ exp :: 'E_' ::= | exit exp :: :: exit {{ com expression to halt all current execution, potentially calling a system, trap, or interrupt handler with exp }} + | return exp :: :: return {{ com expression to end current function execution and return the value of exp from the function; this can be used to break out of for loops }} | assert ( exp , exp' ) :: :: assert {{ com expression to halt with error, when the first expression is false, reporting the optional string as an error }} | ( exp ) :: S :: paren {{ ichlo [[exp]] }} @@ -678,7 +679,7 @@ exp :: 'E_' ::= | comment exp :: :: comment_struc {{ com For generated structured comments }} | let lexp = exp in exp' :: :: internal_let {{ com This is an internal node for compilation that demonstrates the scope of a local mutable variable }} | let pat = exp in exp' :: :: internal_plet {{ com This is an internal node, used to distinguised some introduced lets during processing from original ones }} - | return ( exp ) :: :: internal_return {{ com For internal use to embed into monad definition }} + | return_int ( exp ) :: :: internal_return {{ com For internal use to embed into monad definition }} lexp :: 'LEXP_' ::= {{ com lvalue expression }} diff --git a/language/l2_parse.ml b/language/l2_parse.ml index b94d16fe..cf1da35a 100644 --- a/language/l2_parse.ml +++ b/language/l2_parse.ml @@ -233,6 +233,7 @@ exp_aux = (* Expression *) | E_assign of exp * exp (* imperative assignment *) | E_sizeof of atyp | E_exit of exp + | E_return of exp | E_assert of exp * exp and exp = 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]] }} |