diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/initial_check.ml | 10 | ||||
| -rw-r--r-- | src/lexer.mll | 2 | ||||
| -rw-r--r-- | src/parse_ast.ml | 2 | ||||
| -rw-r--r-- | src/parser.mly | 7 |
4 files changed, 21 insertions, 0 deletions
diff --git a/src/initial_check.ml b/src/initial_check.ml index d08ab8cf..108e04d0 100644 --- a/src/initial_check.ml +++ b/src/initial_check.ml @@ -387,6 +387,16 @@ and to_ast_exp ctx (P.E_aux(exp,l) : P.exp) = | P.E_throw exp -> E_throw (to_ast_exp ctx exp) | P.E_return exp -> E_return(to_ast_exp ctx exp) | P.E_assert(cond,msg) -> E_assert(to_ast_exp ctx cond, to_ast_exp ctx msg) + | P.E_internal_plet(pat,exp1,exp2) -> + if !opt_magic_hash then + E_internal_plet(to_ast_pat ctx pat, to_ast_exp ctx exp1, to_ast_exp ctx exp2) + else + raise (Reporting.err_general l "Internal plet construct found without -dmagic_hash") + | P.E_internal_return(exp) -> + if !opt_magic_hash then + E_internal_return(to_ast_exp ctx exp) + else + raise (Reporting.err_general l "Internal return construct found without -dmagic_hash") | _ -> raise (Reporting.err_unreachable l __POS__ "Unparsable construct in to_ast_exp") ), (l,())) diff --git a/src/lexer.mll b/src/lexer.mll index 604931ac..43426d77 100644 --- a/src/lexer.mll +++ b/src/lexer.mll @@ -181,6 +181,8 @@ let kw_table = ("escape", (fun x -> Escape)); ("configuration", (fun _ -> Configuration)); ("termination_measure", (fun _ -> TerminationMeasure)); + ("internal_plet", (fun _ -> InternalPLet)); + ("internal_return", (fun _ -> InternalReturn)); ] diff --git a/src/parse_ast.ml b/src/parse_ast.ml index 2e78b825..6401331e 100644 --- a/src/parse_ast.ml +++ b/src/parse_ast.ml @@ -275,6 +275,8 @@ exp_aux = (* Expression *) | E_return of exp | E_assert of exp * exp | E_var of exp * exp * exp + | E_internal_plet of pat * exp * exp + | E_internal_return of exp and exp = E_aux of exp_aux * l diff --git a/src/parser.mly b/src/parser.mly index 7540d1f4..cbbc41e3 100644 --- a/src/parser.mly +++ b/src/parser.mly @@ -183,6 +183,7 @@ let rec desugar_rchain chain s e = %token Undefined Union Newtype With Val Constraint Throw Try Catch Exit Bitfield %token Barr Depend Rreg Wreg Rmem Rmemt Wmem Wmv Wmvt Eamem Exmem Undef Unspec Nondet Escape %token Repeat Until While Do Mutual Var Ref Configuration TerminationMeasure +%token InternalPLet InternalReturn %nonassoc Then %nonassoc Else @@ -806,6 +807,12 @@ exp: | While exp Do exp { mk_exp (E_loop (While, $2, $4)) $startpos $endpos } + /* Debugging only, will be rejected in initial_check if debugging isn't on */ + | InternalPLet pat Eq exp In exp + { mk_exp (E_internal_plet ($2,$4,$6)) $startpos $endpos } + | InternalReturn exp + { mk_exp (E_internal_return($2)) $startpos $endpos } + /* The following implements all nine levels of user-defined precedence for operators in expressions, with both left, right and non-associative operators */ |