diff options
| author | Thomas Bauereiss | 2019-01-17 01:10:54 +0000 |
|---|---|---|
| committer | Thomas Bauereiss | 2019-01-17 01:10:54 +0000 |
| commit | 63fa9e0e2807e4b5fc3f825e6914a2fab5de37e3 (patch) | |
| tree | 95d3cac889537febc41ae0c2b606bef3e37a174d /src/pretty_print_lem.ml | |
| parent | 783d4d217387274a397f7c667d368461601d3891 (diff) | |
Output configuration registers for Lem
Treat them as constants for now (with their initial value); in order to
support updates, we would have to embed them properly into the monads.
Diffstat (limited to 'src/pretty_print_lem.ml')
| -rw-r--r-- | src/pretty_print_lem.ml | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml index 73c1fe8b..69c9b9e8 100644 --- a/src/pretty_print_lem.ml +++ b/src/pretty_print_lem.ml @@ -581,6 +581,8 @@ let doc_exp_lem, doc_let_lem = then wrap_parens (separate space [string "liftR"; parens (doc)]) else wrap_parens doc in match e with + | E_assign(_, _) when has_effect (effect_of full_exp) BE_config -> + string "return ()" (* TODO *) | E_assign((LEXP_aux(le_act,tannot) as le), e) -> (* can only be register writes *) let t = typ_of_annot tannot in @@ -825,7 +827,7 @@ let doc_exp_lem, doc_let_lem = if is_bitvector_typ base_typ then liftR (parens (align (group (prefix 0 1 epp (doc_tannot_lem ctxt env true base_typ))))) else liftR epp - else if Env.is_register id env then doc_id_lem (append_id id "_ref") + else if Env.is_register id env && is_regtyp (typ_of full_exp) env then doc_id_lem (append_id id "_ref") else if is_ctor env id then doc_id_lem_ctor id else doc_id_lem id | E_lit lit -> doc_lit_lem lit @@ -1360,9 +1362,9 @@ let doc_dec_lem (DEC_aux (reg, ((l, _) as annot))) = ^/^ hardline else raise (Reporting.err_unreachable l __POS__ ("can't deal with register type " ^ string_of_typ typ)) else raise (Reporting.err_unreachable l __POS__ ("can't deal with register type " ^ string_of_typ typ)) *) + | DEC_config(id, typ, exp) -> separate space [string "let"; doc_id_lem id; equals; doc_exp_lem empty_ctxt false exp] ^^ hardline | DEC_alias(id,alspec) -> empty | DEC_typ_alias(typ,id,alspec) -> empty - | DEC_config _ -> empty let doc_spec_lem (VS_aux (valspec,annot)) = match valspec with |