From 255b77f23a79a08c1d0f5569e613620aae2b4d0e Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Wed, 1 Nov 2017 10:38:44 +0000
Subject: Support bitvector-size-parametric functions in Lem output Translates
 atom('n) types into itself('n) types that won't be erased Also exports more
 rewriting functions

---
 src/gen_lib/sail_operators_mwords.lem | 10 ++++++++++
 1 file changed, 10 insertions(+)

(limited to 'src/gen_lib')

diff --git a/src/gen_lib/sail_operators_mwords.lem b/src/gen_lib/sail_operators_mwords.lem
index d4dca80c..8fb55137 100644
--- a/src/gen_lib/sail_operators_mwords.lem
+++ b/src/gen_lib/sail_operators_mwords.lem
@@ -3,6 +3,16 @@ open import Machine_word
 open import Sail_impl_base
 open import Sail_values
 
+(* Translating between a type level number (itself 'n) and an integer *)
+
+let size_itself_int x = integerFromNat (size_itself x)
+
+(* NB: the corresponding sail type is forall 'n. atom('n) -> itself('n),
+   the actual integer is ignored. *)
+
+val make_the_value : forall 'n. integer -> itself 'n
+let inline make_the_value x = the_value
+
 (*** Bit vector operations *)
 
 let bitvector_length bs = integerFromNat (word_length bs)
-- 
cgit v1.2.3