diff options
| author | Brian Campbell | 2018-06-20 13:20:56 +0100 |
|---|---|---|
| committer | Brian Campbell | 2018-06-20 18:21:27 +0100 |
| commit | c2ce7fa6db14551fa49e1d7b46f795bd629c2061 (patch) | |
| tree | 422d38b945e99bf0ce2c2b2a2b4b52b2a137b32e | |
| parent | 7ef315c49caa8b781891d64edc54a7a1ffc010fd (diff) | |
Coq: port handling of effectful and/or from Lem backend
| -rw-r--r-- | lib/flow.sail | 2 | ||||
| -rw-r--r-- | src/pretty_print_coq.ml | 7 |
2 files changed, 8 insertions, 1 deletions
diff --git a/lib/flow.sail b/lib/flow.sail index 7dc5969e..b698b597 100644 --- a/lib/flow.sail +++ b/lib/flow.sail @@ -2,6 +2,8 @@ $ifndef _FLOW $define _FLOW val not_bool = {coq: "negb", _: "not"} : bool -> bool +/* NB: There are special cases in Sail for effectful uses of and_bool and + or_bool that are not shown here. */ val and_bool = {coq: "andb", _: "and_bool"} : (bool, bool) -> bool val or_bool = {coq: "orb", _: "or_bool"} : (bool, bool) -> bool diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml index 66ce3370..0df96758 100644 --- a/src/pretty_print_coq.ml +++ b/src/pretty_print_coq.ml @@ -680,6 +680,7 @@ let doc_exp_lem, doc_let_lem = let expY = top_exp ctxt true in let expN = top_exp ctxt false in let expV = top_exp ctxt in + let wrap_parens doc = if aexp_needed then parens (doc) else doc in let maybe_add_exist epp = let env = env_of full_exp in let typ = Env.expand_synonyms env (typ_of full_exp) in @@ -769,6 +770,10 @@ let doc_exp_lem, doc_let_lem = if aexp_needed then parens epp else epp | E_app(f,args) -> begin match f with + | Id_aux (Id "and_bool", _) | Id_aux (Id "or_bool", _) + when effectful (effect_of full_exp) -> + let call = doc_id (append_id f "M") in + wrap_parens (hang 2 (flow (break 1) (call :: List.map expY args))) (* temporary hack to make the loop body a function of the temporary variables *) | Id_aux (Id "None", _) as none -> doc_id_ctor none | Id_aux (Id "foreach", _) -> @@ -1084,7 +1089,7 @@ let doc_exp_lem, doc_let_lem = in if aexp_needed then parens (align epp) else epp | E_internal_return (e1) -> - separate space [string "returnm"; expY e1] + wrap_parens (align (separate space [string "returnm"; expY e1])) | E_sizeof nexp -> (match nexp_simp nexp with | Nexp_aux (Nexp_constant i, _) -> doc_lit (L_aux (L_num i, l)) |