diff options
| author | Robert Norton | 2017-04-11 14:30:22 +0100 |
|---|---|---|
| committer | Shaked Flur | 2017-04-18 13:58:33 +0100 |
| commit | 106d7d8c4793817021d2791159ec373ac36c452d (patch) | |
| tree | 080e099489df2ab2f8dbbd997900ddf2a60cab96 /src/pretty_print_ocaml.ml | |
| parent | fea4672ef7e6b1a6ac1c7dfb2c42dccd4e5386d2 (diff) | |
Implement return using an exception caught in the function body. Polymorphic exceptions are not permitted so a local mutable variable, ret, is used in ocaml to store the return value. This avoids having to define a new exception type for each function. Ocaml infers the type of the option when it is assigned at the return site.
Diffstat (limited to 'src/pretty_print_ocaml.ml')
| -rw-r--r-- | src/pretty_print_ocaml.ml | 20 |
1 files changed, 18 insertions, 2 deletions
diff --git a/src/pretty_print_ocaml.ml b/src/pretty_print_ocaml.ml index 2033e3ba..2d9b6f37 100644 --- a/src/pretty_print_ocaml.ml +++ b/src/pretty_print_ocaml.ml @@ -400,6 +400,8 @@ let doc_exp_ocaml, doc_let_ocaml = surround 2 1 opening cases rparen | E_exit e -> separate space [string "exit"; exp e;] + | E_return e -> + separate space [string "begin ret := Some" ; exp e ; string "; raise Sail_return; end"] | E_app_infix (e1,id,e2) -> let call = match annot with @@ -636,8 +638,22 @@ let doc_rec_ocaml (Rec_aux(r,_)) = match r with let doc_tannot_opt_ocaml (Typ_annot_opt_aux(t,_)) = match t with | Typ_annot_opt_some(tq,typ) -> doc_typquant_ocaml tq (doc_typ_ocaml typ) +let doc_funcl_exp_ocaml (E_aux (e, (l, annot)) as ea) = match annot with + | Base((_,t),tag,nes,efct,efctsum,_) -> + if has_lret_effect efctsum then + separate hardline [string "let ret = ref None in"; + string "try"; + (doc_exp_ocaml ea); + string "with Sail_return -> match(!ret) with"; + string "| Some(x) -> x"; + string "| None -> failwith \"ret unset\"" + ] + else + doc_exp_ocaml ea + | _ -> doc_exp_ocaml ea + let doc_funcl_ocaml (FCL_aux(FCL_Funcl(id,pat,exp),_)) = - group (doc_op arrow (doc_pat_ocaml pat) (doc_exp_ocaml exp)) + group (doc_op arrow (doc_pat_ocaml pat) (doc_funcl_exp_ocaml exp)) let get_id = function | [] -> failwith "FD_function with empty list" @@ -647,7 +663,7 @@ let doc_fundef_ocaml (FD_aux(FD_function(r, typa, efa, fcls),_)) = match fcls with | [] -> failwith "FD_function with empty function list" | [FCL_aux (FCL_Funcl(id,pat,exp),_)] -> - (separate space [(string "let"); (doc_rec_ocaml r); (doc_id_ocaml id); (doc_pat_ocaml pat); equals]) ^^ hardline ^^ (doc_exp_ocaml exp) + (separate space [(string "let"); (doc_rec_ocaml r); (doc_id_ocaml id); (doc_pat_ocaml pat); equals]) ^^ hardline ^^ (doc_funcl_exp_ocaml exp) | _ -> let id = get_id fcls in let sep = hardline ^^ pipe ^^ space in |