From 579cd897d7873436ba6cfb3469b185bf6b321dac Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Thu, 8 Feb 2018 15:03:34 +0000
Subject: Add (most of) the bitvector cast insertion transformation to help Lem
 go from a general type `bits('n)` to a specific type `bits(16)` at a case
 split, and the other way around for a returned value. Doesn't handle function
 clause patterns yet

---
 lib/mono_rewrites.sail | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'lib')

diff --git a/lib/mono_rewrites.sail b/lib/mono_rewrites.sail
index 1af9b17f..167a2fdd 100644
--- a/lib/mono_rewrites.sail
+++ b/lib/mono_rewrites.sail
@@ -27,6 +27,10 @@ val "exts_vec" : forall 'n 'm. (atom('m),vector('n, dec, bit)) -> vector('m, dec
 val extsv : forall 'n 'm. vector('n, dec, bit) -> vector('m, dec, bit) effect pure
 function extsv(v) = exts_vec(sizeof('m),v)
 
+/* This is generated internally to deal with case splits which reveal the size
+   of a bitvector */
+val bitvector_cast = "zeroExtend" : forall 'n. bits('n) -> bits('n) effect pure
+
 /* Definitions for the rewrites */
 
 val slice_mask : forall 'n, 'n >= 0. (int, int) -> bits('n) effect pure
-- 
cgit v1.2.3