diff options
| author | Alasdair Armstrong | 2019-05-17 18:38:35 +0100 |
|---|---|---|
| committer | Alasdair Armstrong | 2019-05-17 18:38:35 +0100 |
| commit | a1ef7946b96d95b3192f8db496f09d4bb23b775a (patch) | |
| tree | fffb42d83bebfae64ae1be1149e8c5e660753ed1 /src/initial_check.ml | |
| parent | f0b547154b3d2ce9e4bac74b0c56f20d6db76cd2 (diff) | |
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.
Diffstat (limited to 'src/initial_check.ml')
| -rw-r--r-- | src/initial_check.ml | 3 |
1 files changed, 2 insertions, 1 deletions
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) = |