diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/gen_lib/sail_values.ml | 1 | ||||
| -rw-r--r-- | src/pretty_print_ocaml.ml | 20 | ||||
| -rw-r--r-- | src/type_internal.ml | 1 | ||||
| -rw-r--r-- | src/type_internal.mli | 1 |
4 files changed, 21 insertions, 2 deletions
diff --git a/src/gen_lib/sail_values.ml b/src/gen_lib/sail_values.ml index aa3141ed..77d149bf 100644 --- a/src/gen_lib/sail_values.ml +++ b/src/gen_lib/sail_values.ml @@ -15,6 +15,7 @@ type value = | Vbit of vbit (*Mostly for Vundef in place of undefined register place holders*) exception Sail_exit +exception Sail_return let string_of_bit = function | Vone -> "1" 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 diff --git a/src/type_internal.ml b/src/type_internal.ml index 60dbecc4..ad7a772e 100644 --- a/src/type_internal.ml +++ b/src/type_internal.ml @@ -3142,6 +3142,7 @@ let has_rmem_effect = has_effect (BE_aux(BE_rmem, Parse_ast.Unknown)) let has_wmem_effect = has_effect (BE_aux(BE_wmem, Parse_ast.Unknown)) let has_eamem_effect = has_effect (BE_aux(BE_eamem, Parse_ast.Unknown)) let has_memv_effect = has_effect (BE_aux(BE_wmv, Parse_ast.Unknown)) +let has_lret_effect = has_effect (BE_aux(BE_lret, Parse_ast.Unknown)) (*Similarly to above.*) let effects_eq co e1 e2 = diff --git a/src/type_internal.mli b/src/type_internal.mli index 7946a115..4912585a 100644 --- a/src/type_internal.mli +++ b/src/type_internal.mli @@ -251,6 +251,7 @@ val has_rmem_effect : effect -> bool val has_wmem_effect : effect -> bool val has_eamem_effect : effect -> bool val has_memv_effect : effect -> bool +val has_lret_effect : effect -> bool val initial_kind_env : kind Envmap.t val initial_abbrev_env : tannot Envmap.t |