diff options
| author | Thomas Bauereiss | 2018-03-14 10:56:57 +0000 |
|---|---|---|
| committer | Thomas Bauereiss | 2018-03-14 12:21:47 +0000 |
| commit | 71febd33cb9759ee524b6d7a8be3b66cba236c0e (patch) | |
| tree | 28f3e704cce279bd209d147a0a4e5dee82cbe75a /src/pretty_print_lem.ml | |
| parent | be1f5f26ca68fad23eada8a3adb5cfb6b958ff51 (diff) | |
Make partiality more explicit in library functions of Lem shallow embedding
Some functions are partial, e.g. converting a bitvector to an integer, which
might fail for the bit list representation due to undefined bits. Undefined
cases can be handled in different ways:
- call Lem's failwith, which maps to undefined/ARB in Isabelle and HOL (the
default so far),
- return an option type,
- raise a failure in the monad, or
- use a bitstream oracle to resolve undefined bits.
This patch adds different versions of partial functions corresponding to those
options. The desired behaviour can be selected by choosing a binding in the
Sail prelude. The naming scheme is that the failwith version is the default,
while the other versions have the suffixes _maybe, _fail, and _oracle,
respectively.
Diffstat (limited to 'src/pretty_print_lem.ml')
| -rw-r--r-- | src/pretty_print_lem.ml | 12 |
1 files changed, 7 insertions, 5 deletions
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml index d347c1bd..eb9feee3 100644 --- a/src/pretty_print_lem.ml +++ b/src/pretty_print_lem.ml @@ -148,14 +148,16 @@ let simple_num l n = E_aux ( simple_annot (Parse_ast.Generated l) (atom_typ (Nexp_aux (Nexp_constant n, Parse_ast.Generated l)))) -let effectful_set = - List.exists +let effectful_set = function + | [] -> false + | _ -> true + (*List.exists (fun (BE_aux (eff,_)) -> match eff with | BE_rreg | BE_wreg | BE_rmem | BE_rmemt | BE_wmem | BE_eamem | BE_exmem | BE_wmv | BE_wmvt | BE_barr | BE_depend | BE_nondet | BE_escape -> true - | _ -> false) + | _ -> false)*) let effectful (Effect_aux (Effect_set effs, _)) = effectful_set effs @@ -362,7 +364,7 @@ let doc_lit_lem (L_aux(lit,l)) = | L_hex n -> failwith "Shouldn't happen" (*"(num_to_vec " ^ ("0x" ^ n) ^ ")" (*shouldn't happen*)*) | L_bin n -> failwith "Shouldn't happen" (*"(num_to_vec " ^ ("0b" ^ n) ^ ")" (*shouldn't happen*)*) | L_undef -> - utf8string "(failwith \"undefined value of unsupported type\")" + utf8string "(return (failwith \"undefined value of unsupported type\"))" | L_string s -> utf8string ("\"" ^ s ^ "\"") | L_real s -> (* Lem does not support decimal syntax, so we translate a string @@ -790,7 +792,7 @@ let doc_exp_lem, doc_let_lem = let epp = brackets expspp in let (epp,aexp_needed) = if is_bit_typ etyp && !opt_mwords then - let bepp = string "of_bits" ^^ space ^^ parens (align epp) in + let bepp = string "of_bits_failwith" ^^ space ^^ parens (align epp) in (bepp ^^ doc_tannot_lem ctxt (env_of full_exp) false t, true) else (epp,aexp_needed) in if aexp_needed then parens (align epp) else epp |