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_ast.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_ast.ml')
| -rw-r--r-- | src/pretty_print_lem_ast.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/pretty_print_lem_ast.ml b/src/pretty_print_lem_ast.ml index 559c1116..228ddbb8 100644 --- a/src/pretty_print_lem_ast.ml +++ b/src/pretty_print_lem_ast.ml @@ -182,8 +182,8 @@ and pp_format_base_effect_lem (BE_aux(e,l)) = | BE_undef -> "BE_undef" | BE_unspec -> "BE_unspec" | BE_nondet -> "BE_nondet" - | BE_lset -> "BE_lset" - | BE_lret -> "BE_lret" + (*| BE_lset -> "BE_lset" + | BE_lret -> "BE_lret"*) | BE_escape -> "BE_escape") ^ " " ^ (pp_format_l_lem l) ^ ")" and pp_format_effects_lem (Effect_aux(e,l)) = |