diff options
| author | Kathy Gray | 2016-07-25 14:27:59 +0100 |
|---|---|---|
| committer | Kathy Gray | 2016-07-25 14:27:59 +0100 |
| commit | 48829c4ad90ceedefe4005ef682a4a0315681f37 (patch) | |
| tree | 0a83efa82fd3939d3a96ee688800bfcc73a7b286 /src | |
| parent | e393e35b394b4d5def97f476818f63d0a7aa0cbc (diff) | |
Support return in interpreter pretty printer (also fix typo for default case)
Diffstat (limited to 'src')
| -rw-r--r-- | src/lem_interp/pretty_interp.ml | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/src/lem_interp/pretty_interp.ml b/src/lem_interp/pretty_interp.ml index 13e697d4..f17b5d56 100644 --- a/src/lem_interp/pretty_interp.ml +++ b/src/lem_interp/pretty_interp.ml @@ -89,7 +89,8 @@ let doc_effect (BE_aux (e,_)) = | BE_unspec -> "unspec" | BE_escape -> "escape" | BE_nondet -> "nondet" - | BE_lset -> "(*lset*)") + | BE_lset -> "(*lset*)" + | BE_lret -> "(*lret*)") let doc_effects (Effect_aux(e,_)) = match e with | Effect_var v -> doc_var v @@ -405,6 +406,7 @@ let doc_exp, doc_let = let cases = separate_map (break 1) (doc_case env add_red) pexps in surround 2 1 opening cases rbrace | E_exit e -> separate space [string "exit"; exp env add_red e;] + | E_return e -> separate space [string "return"; exp env add_red e;] | E_assert(e,msg) -> string "assert" ^^ parens (separate_map comma (exp env add_red) [e; msg]) (* adding parens and loop for lower precedence *) | E_app (_, _)|E_vector_access (_, _)|E_vector_subrange (_, _, _) @@ -437,7 +439,7 @@ let doc_exp, doc_let = (* doc_op (doc_id op) (exp l) (exp r) *) (* XXX missing case *) | E_comment _ | E_comment_struc _ -> string "" - | _-> failwith "internal expression escpaed" + | _-> failwith "internal expression escaped" and let_exp env add_red (LB_aux(lb,_)) = match lb with | LB_val_explicit(ts,pat,e) -> |