From a1ef7946b96d95b3192f8db496f09d4bb23b775a Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Fri, 17 May 2019 18:38:35 +0100
Subject: Experiment with making vector and bitvector distinct types

Only change that should be needed for 99.9% of uses is to change
vector('n, 'ord, bit) to bitvector('n, 'ord), and adding

$ifndef FEATURE_BITVECTOR_TYPE
type bitvector('n, dec) = vector('n, dec, bit)
$endif

for to support any Sail before this

Currently I have all C, Typechecking, and SMT tests passing, as well
as the RISC-V spec building OCaml and C completely unmodified.
---
 src/initial_check.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'src/initial_check.ml')

diff --git a/src/initial_check.ml b/src/initial_check.ml
index 522faab7..1f15d054 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -859,6 +859,7 @@ let initial_ctx = {
           ("list", [K_type]);
           ("register", [K_type]);
           ("range", [K_int; K_int]);
+          ("bitvector", [K_int; K_order]);
           ("vector", [K_int; K_order; K_type]);
           ("atom", [K_int]);
           ("implicit", [K_int]);
@@ -925,7 +926,7 @@ let undefined_builtin_val_specs =
    extern_of_string (mk_id "undefined_range") "forall 'n 'm. (atom('n), atom('m)) -> range('n,'m) effect {undef}";
    extern_of_string (mk_id "undefined_vector") "forall 'n ('a:Type) ('ord : Order). (atom('n), 'a) -> vector('n, 'ord,'a) effect {undef}";
    (* Only used with lem_mwords *)
-   extern_of_string (mk_id "undefined_bitvector") "forall 'n. atom('n) -> vector('n, dec, bit) effect {undef}";
+   extern_of_string (mk_id "undefined_bitvector") "forall 'n. atom('n) -> bitvector('n, dec) effect {undef}";
    extern_of_string (mk_id "undefined_unit") "unit -> unit effect {undef}"]
 
 let generate_undefineds vs_ids (Defs defs) =
-- 
cgit v1.2.3