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 /language | |
| 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 'language')
| -rw-r--r-- | language/l2.ott | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/language/l2.ott b/language/l2.ott index c34dedb5..a437f915 100644 --- a/language/l2.ott +++ b/language/l2.ott @@ -230,9 +230,7 @@ base_effect :: 'BE_' ::= | undef :: :: undef {{ com undefined-instruction exception }} | unspec :: :: unspec {{ com unspecified values }} | nondet :: :: nondet {{ com nondeterminism, from $[[nondet]]$ }} - | escape :: :: escape {{ com potential call of $[[exit]]$ }} - | lset :: :: lset {{ com local mutation; not user-writable }} - | lret :: :: lret {{ com local return; not user-writable }} + | escape :: :: escape {{ com potential exception }} effect :: 'Effect_' ::= {{ com effect set, of kind $[[Effect]]$ }} |