diff options
| author | Alasdair Armstrong | 2018-03-02 19:17:51 +0000 |
|---|---|---|
| committer | Alasdair Armstrong | 2018-03-02 19:34:54 +0000 |
| commit | ea2ff78cf675298df64e8ebacca7156b68f3c5c8 (patch) | |
| tree | 61500ccdd47247a4eab6bd19ece039d598267d28 /src/gen_lib/sail_values.lem | |
| parent | 936150eda67ddbd216653fe4030bb6b790c6bb17 (diff) | |
Use sail_lib.lem values in C backend
Rather than just using strings to represent literals, now use value
types from sail_lib.lem to represent them. This allows for expressions
to be evaluated at compile time, which will be useful for future
optimisations involving constant folding and propagation, and allows
the intermediate bytecode to be interpreted using the same lem
builtins that the shallow embedding uses.
To get this to work I had to tweak the build process slightly to allow
ml files to import lem files from gen_lib/. Hopefully this doesn't
break anything!
Diffstat (limited to 'src/gen_lib/sail_values.lem')
| -rw-r--r-- | src/gen_lib/sail_values.lem | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem index 4d67cbfc..fce595e0 100644 --- a/src/gen_lib/sail_values.lem +++ b/src/gen_lib/sail_values.lem @@ -108,6 +108,12 @@ let showBitU = function | BU -> "U" end +let bitU_char = function + | B0 -> #'0' + | B1 -> #'1' + | BU -> #'?' +end + instance (Show bitU) let show = showBitU end @@ -307,7 +313,7 @@ declare {isabelle} termination_argument hexstring_of_bits = automatic let show_bitlist bs = match hexstring_of_bits bs with | Just s -> toString (#'0' :: #'x' :: s) - | Nothing -> show bs + | Nothing -> toString (#'0' :: #'b' :: map bitU_char bs) end (*** List operations *) |