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. --- test/typecheck/pass/Replicate/v1.expect | 2 +- test/typecheck/pass/Replicate/v2.expect | 2 +- test/typecheck/pass/add_vec_lit.sail | 4 +-- test/typecheck/pass/arm_FPEXC1.sail | 20 +++++++------- test/typecheck/pass/bitfield_pc.sail | 4 ++- test/typecheck/pass/bitvector_param.sail | 27 +----------------- test/typecheck/pass/decode_patterns.sail | 6 ++-- test/typecheck/pass/exist_tlb.sail | 38 +++++++++++++------------- test/typecheck/pass/existential_ast/v3.expect | 2 +- test/typecheck/pass/existential_ast3/v1.expect | 8 +++--- test/typecheck/pass/existential_ast3/v2.expect | 8 +++--- test/typecheck/pass/existential_ast3/v3.expect | 2 +- test/typecheck/pass/if_infer/v1.expect | 5 ++-- test/typecheck/pass/if_infer/v2.expect | 5 ++-- test/typecheck/pass/if_infer/v3.expect | 2 +- test/typecheck/pass/nexp_synonym/v1.expect | 2 +- test/typecheck/pass/nexp_synonym/v2.expect | 2 +- test/typecheck/pass/nlflow.sail | 2 +- test/typecheck/pass/nzcv.sail | 4 +-- test/typecheck/pass/procstate1.sail | 10 +++---- test/typecheck/pass/pure_record.sail | 16 +++++------ test/typecheck/pass/pure_record2.sail | 16 +++++------ test/typecheck/pass/pure_record3.sail | 20 +++++++------- test/typecheck/pass/reg_32_64/v2.expect | 2 +- test/typecheck/pass/vec_length/v1.expect | 3 +- test/typecheck/pass/vec_length/v1_inc.expect | 3 +- test/typecheck/pass/vec_length/v2.expect | 3 +- test/typecheck/pass/vec_length/v2_inc.expect | 3 +- test/typecheck/pass/vec_length/v3.expect | 3 +- test/typecheck/pass/vec_pat1.sail | 12 ++++---- test/typecheck/pass/vector_subrange_gen.sail | 14 +++------- 31 files changed, 107 insertions(+), 143 deletions(-) (limited to 'test/typecheck') diff --git a/test/typecheck/pass/Replicate/v1.expect b/test/typecheck/pass/Replicate/v1.expect index c40aa5ec..5c52861f 100644 --- a/test/typecheck/pass/Replicate/v1.expect +++ b/test/typecheck/pass/Replicate/v1.expect @@ -2,7 +2,7 @@ Type error: [Replicate/v1.sail]:14:4-30 14 | replicate_bits(x, 'N / 'M)  | ^------------------------^ -  | Tried performing type coercion from vector(('M * div('N, 'M)), dec, bit) to vector('N, dec, bit) on replicate_bits(x, ediv_int(__id(N), bitvector_length(x))) +  | Tried performing type coercion from bitvector(('M * div('N, 'M)), dec) to bitvector('N, dec) on replicate_bits(x, ediv_int(__id(N), bitvector_length(x)))  | Coercion failed because:  | Mismatched argument types in subtype check  | diff --git a/test/typecheck/pass/Replicate/v2.expect b/test/typecheck/pass/Replicate/v2.expect index acadd4e2..7d4891f9 100644 --- a/test/typecheck/pass/Replicate/v2.expect +++ b/test/typecheck/pass/Replicate/v2.expect @@ -2,7 +2,7 @@ Type error: [Replicate/v2.sail]:13:4-30 13 | replicate_bits(x, 'N / 'M)  | ^------------------------^ -  | Tried performing type coercion from {('ex119# : Int), true. vector(('M * 'ex119#), dec, bit)} to vector('N, dec, bit) on replicate_bits(x, tdiv_int(__id(N), bitvector_length(x))) +  | Tried performing type coercion from {('ex128# : Int), true. bitvector(('M * 'ex128#), dec)} to bitvector('N, dec) on replicate_bits(x, tdiv_int(__id(N), bitvector_length(x)))  | Coercion failed because:  | Mismatched argument types in subtype check  | diff --git a/test/typecheck/pass/add_vec_lit.sail b/test/typecheck/pass/add_vec_lit.sail index 7e5c873a..cf29212f 100644 --- a/test/typecheck/pass/add_vec_lit.sail +++ b/test/typecheck/pass/add_vec_lit.sail @@ -1,13 +1,13 @@ default Order inc val add_vec = {ocaml: "add_vec", lem: "add_vec"}: forall ('n : Int). - (vector('n, inc, bit), vector('n, inc, bit)) -> vector('n, inc, bit) + (bitvector('n, inc), bitvector('n, inc)) -> bitvector('n, inc) val add_range = {ocaml: "add_range", lem: "add_range"}: forall ('n : Int) ('m : Int) ('o : Int) ('p : Int). (range('n, 'm), range('o, 'p)) -> range('n + 'o, 'm + 'p) val cast unsigned : forall ('n : Int). - vector('n, inc, bit) -> range(0, 2 ^ 'n - 1) + bitvector('n, inc) -> range(0, 2 ^ 'n - 1) overload operator + = {add_vec, add_range} diff --git a/test/typecheck/pass/arm_FPEXC1.sail b/test/typecheck/pass/arm_FPEXC1.sail index 2021bf67..3f4b8632 100644 --- a/test/typecheck/pass/arm_FPEXC1.sail +++ b/test/typecheck/pass/arm_FPEXC1.sail @@ -1,17 +1,17 @@ default Order dec val vector_access = {ocaml: "access", lem: "access_vec_dec", coq: "access_vec_dec"}: forall ('n : Int). - (vector('n, dec, bit), int) -> bit + (bitvector('n, dec), int) -> bit val vector_subrange = {ocaml: "subrange", lem: "subrange_vec_dec", coq: "subrange_vec_dec"}: forall ('n : Int) ('m : Int) ('o : Int), 'm >= 'o & 'o >= 0 & 'n >= 'm + 1. - (vector('n, dec, bit), atom('m), atom('o)) -> vector('m - ('o - 1), dec, bit) + (bitvector('n, dec), atom('m), atom('o)) -> bitvector('m - ('o - 1), dec) val vector_update_subrange = {ocaml: "update_subrange", lem: "update_subrange_vec_dec", coq: "update_subrange_vec_dec"} : forall 'n 'm 'o. - (vector('n, dec, bit), atom('m), atom('o), vector('m - ('o - 1), dec, bit)) -> vector('n, dec, bit) + (bitvector('n, dec), atom('m), atom('o), bitvector('m - ('o - 1), dec)) -> bitvector('n, dec) -register _FPEXC32_EL2 : vector(32, dec, bit) +register _FPEXC32_EL2 : bitvector(32, dec) -val set_FPEXC32_EL2 : vector(32, dec, bit) -> unit effect {wreg} +val set_FPEXC32_EL2 : bitvector(32, dec) -> unit effect {wreg} function set_FPEXC32_EL2 value_name = { _FPEXC32_EL2[0 .. 0] = [value_name[0]]; @@ -26,10 +26,10 @@ function set_FPEXC32_EL2 value_name = { _FPEXC32_EL2[30 .. 30] = [value_name[30]] } -val get_FPEXC32_EL2 : unit -> vector(32, dec, bit) effect {rreg} +val get_FPEXC32_EL2 : unit -> bitvector(32, dec) effect {rreg} function get_FPEXC32_EL2 () = { - value_name : vector(32, dec, bit) = 0x04000700; + value_name : bitvector(32, dec) = 0x04000700; value_name[0 .. 0] = [_FPEXC32_EL2[0]]; value_name[1 .. 1] = [_FPEXC32_EL2[1]]; value_name[2 .. 2] = [_FPEXC32_EL2[2]]; @@ -44,11 +44,11 @@ function get_FPEXC32_EL2 () = { value_name } -val set_FPEXC : vector(32, dec, bit) -> unit effect {rreg, wreg} +val set_FPEXC : bitvector(32, dec) -> unit effect {rreg, wreg} function set_FPEXC val_name = { - r : vector(32, dec, bit) = val_name; - __tmp_45 : vector(32, dec, bit) = get_FPEXC32_EL2(); + r : bitvector(32, dec) = val_name; + __tmp_45 : bitvector(32, dec) = get_FPEXC32_EL2(); __tmp_45[31 .. 0] = r; set_FPEXC32_EL2(__tmp_45) } diff --git a/test/typecheck/pass/bitfield_pc.sail b/test/typecheck/pass/bitfield_pc.sail index 9764289a..889e27ce 100644 --- a/test/typecheck/pass/bitfield_pc.sail +++ b/test/typecheck/pass/bitfield_pc.sail @@ -1,6 +1,8 @@ +default Order dec + $include -bitfield PC_t : vector(16, dec, bit) = { +bitfield PC_t : bitvector(16, dec) = { H : 15 .. 8, L : 7 .. 0 } diff --git a/test/typecheck/pass/bitvector_param.sail b/test/typecheck/pass/bitvector_param.sail index 77fe7dc3..784a77f9 100644 --- a/test/typecheck/pass/bitvector_param.sail +++ b/test/typecheck/pass/bitvector_param.sail @@ -1,32 +1,7 @@ default Order dec $include - -type bits ('n : Int) = vector('n, dec, bit) - -val vector_subrange = { - ocaml: "subrange", - lem: "subrange_vec_dec", - c: "vector_subrange", - coq: "subrange_vec_dec" -} : forall ('n : Int) ('m : Int) ('o : Int), 0 <= 'o <= 'm < 'n. - (bits('n), atom('m), atom('o)) -> bits('m - 'o + 1) - -val vector_update_subrange_dec = {ocaml: "update_subrange", c: "vector_update_subrange", lem: "update_subrange_vec_dec", coq: "update_subrange_vec_dec"} : forall 'n 'm 'o. - (bits('n), atom('m), atom('o), bits('m - ('o - 1))) -> bits('n) - -val vector_update_subrange_inc = {ocaml: "update_subrange", lem: "update_subrange_vec_inc"} : forall 'n 'm 'o. - (vector('n, inc, bit), atom('m), atom('o), vector('o - ('m - 1), inc, bit)) -> vector('n, inc, bit) - -overload vector_update_subrange = {vector_update_subrange_dec, vector_update_subrange_inc} - -val bitvector_concat = {c: "append", ocaml: "append", lem: "concat_vec", coq: "concat_vec"} : forall ('n : Int) ('m : Int). - (bits('n), bits('m)) -> bits('n + 'm) - -val vector_concat = {ocaml: "append", lem: "append_list"} : forall ('n : Int) ('m : Int) ('a : Type). - (vector('n, dec, 'a), vector('m, dec, 'a)) -> vector('n + 'm, dec, 'a) - -overload append = {bitvector_concat, vector_concat} +$include type xlen : Int = 64 type ylen : Int = 1 diff --git a/test/typecheck/pass/decode_patterns.sail b/test/typecheck/pass/decode_patterns.sail index d54e9416..6f28ec18 100644 --- a/test/typecheck/pass/decode_patterns.sail +++ b/test/typecheck/pass/decode_patterns.sail @@ -2,7 +2,7 @@ default Order dec $include -val decode : vector(16, dec, bit) -> unit +val decode : bitvector(16, dec) -> unit scattered function decode @@ -22,11 +22,11 @@ function clause decode 0x00 @ 0b001 @ [b : bit] @ 0x0 = end decode -val decode2 : vector(16, dec, bit) -> unit +val decode2 : bitvector(16, dec) -> unit function decode2 x = match x { - 0x00 @ 0b000 @ [b : bit] @ 0x0 => + 0x00 @ 0b000 @ [b : bit] @ 0x0 => if b == bitone then { () } else { diff --git a/test/typecheck/pass/exist_tlb.sail b/test/typecheck/pass/exist_tlb.sail index de15edf8..1d0e1d20 100644 --- a/test/typecheck/pass/exist_tlb.sail +++ b/test/typecheck/pass/exist_tlb.sail @@ -1,17 +1,17 @@ $include val extz : forall ('n : Int) ('m : Int) ('ord : Order). - vector('n, 'ord, bit) -> vector('m, 'ord, bit) + bitvector('n, 'ord) -> bitvector('m, 'ord) val exts : forall ('n : Int) ('m : Int) ('ord : Order). - vector('n, 'ord, bit) -> vector('m, 'ord, bit) + bitvector('n, 'ord) -> bitvector('m, 'ord) overload EXTZ = {extz} overload EXTS = {exts} val add_vec : forall ('n : Int) ('ord : Order). - (vector('n, 'ord, bit), vector('n, 'ord, bit)) -> vector('n, 'ord, bit) + (bitvector('n, 'ord), bitvector('n, 'ord)) -> bitvector('n, 'ord) overload operator + = {add_vec} @@ -21,15 +21,15 @@ overload ~ = {bool_not} default Order dec -register CP0LLBit : vector(1, dec, bit) +register CP0LLBit : bitvector(1, dec) -register CP0LLAddr : vector(64, dec, bit) +register CP0LLAddr : bitvector(64, dec) enum MemAccessType = {Instruction, LoadData, StoreData} -type regno = vector(5, dec, bit) +type regno = bitvector(5, dec) -type imm16 = vector(16, dec, bit) +type imm16 = bitvector(16, dec) enum Exception = { EInt, @@ -55,12 +55,12 @@ enum Exception = { enum WordType = {B, H, W, D} -val rGPR : vector(5, dec, bit) -> vector(64, dec, bit) effect {rreg} +val rGPR : bitvector(5, dec) -> bitvector(64, dec) effect {rreg} -val isAddressAligned : (vector(64, dec, bit), WordType) -> bool +val isAddressAligned : (bitvector(64, dec), WordType) -> bool val SignalExceptionBadAddr : forall ('o : Type). - (Exception, vector(64, dec, bit)) -> 'o + (Exception, bitvector(64, dec)) -> 'o val wordWidthBytes : WordType -> {|1, 2, 4, 8|} @@ -72,29 +72,29 @@ function wordWidthBytes w = match w { } val MEMr_reserve_wrapper : forall ('n : Int). - (vector(64, dec, bit), atom('n)) -> vector(8 * 'n, dec, bit) effect {rmem} + (bitvector(64, dec), atom('n)) -> bitvector(8 * 'n, dec) effect {rmem} val MEMr_wrapper : forall ('n : Int). - (vector(64, dec, bit), atom('n)) -> vector(8 * 'n, dec, bit) effect {rmem} + (bitvector(64, dec), atom('n)) -> bitvector(8 * 'n, dec) effect {rmem} -val wGPR : (vector(5, dec, bit), vector(64, dec, bit)) -> unit effect {wreg} +val wGPR : (bitvector(5, dec), bitvector(64, dec)) -> unit effect {wreg} -val addrWrapper : (vector(64, dec, bit), MemAccessType, WordType) -> vector(64, dec, bit) +val addrWrapper : (bitvector(64, dec), MemAccessType, WordType) -> bitvector(64, dec) -function addrWrapper (addr : vector(64, dec, bit), accessType : MemAccessType, width : WordType) = addr +function addrWrapper (addr : bitvector(64, dec), accessType : MemAccessType, width : WordType) = addr -val TLBTranslate : (vector(64, dec, bit), MemAccessType) -> vector(64, dec, bit) +val TLBTranslate : (bitvector(64, dec), MemAccessType) -> bitvector(64, dec) -function TLBTranslate (vAddr : vector(64, dec, bit), accessType : MemAccessType) = vAddr +function TLBTranslate (vAddr : bitvector(64, dec), accessType : MemAccessType) = vAddr union ast = {Load : (WordType, bool, bool, regno, regno, imm16)} val execute : ast -> unit effect {rmem, rreg, wreg} function execute Load(width, signed, linked, base, rt, offset) = { - vAddr : vector(64, dec, bit) = addrWrapper(EXTS(offset) + rGPR(base), LoadData, width); + vAddr : bitvector(64, dec) = addrWrapper(EXTS(offset) + rGPR(base), LoadData, width); if ~(isAddressAligned(vAddr, width)) then SignalExceptionBadAddr(AdEL, vAddr) else let pAddr = TLBTranslate(vAddr, LoadData) in { - memResult : {'t, 't in {1, 2, 4, 8}. vector(8 * 't, dec, bit)} = if linked then { + memResult : {'t, 't in {1, 2, 4, 8}. bitvector(8 * 't, dec)} = if linked then { CP0LLBit = 0b1; CP0LLAddr = pAddr; MEMr_reserve_wrapper(pAddr, wordWidthBytes(width)) diff --git a/test/typecheck/pass/existential_ast/v3.expect b/test/typecheck/pass/existential_ast/v3.expect index 7bb8a4ab..78711c2b 100644 --- a/test/typecheck/pass/existential_ast/v3.expect +++ b/test/typecheck/pass/existential_ast/v3.expect @@ -3,5 +3,5 @@ Type error: 26 | Some(Ctor1(a, x, c))  | ^------------^  | Could not resolve quantifiers for Ctor1 -  | * datasize('ex196#) +  | * datasize('ex205#)  | diff --git a/test/typecheck/pass/existential_ast3/v1.expect b/test/typecheck/pass/existential_ast3/v1.expect index 4b9bd7cc..40657d0c 100644 --- a/test/typecheck/pass/existential_ast3/v1.expect +++ b/test/typecheck/pass/existential_ast3/v1.expect @@ -4,17 +4,17 @@ Type error:  | ^---------------^  | Tried performing type coercion from (int(33), range(0, (2 ^ 5 - 1))) to {('d : Int) ('n : Int), (datasize('d) & (0 <= 'n & ('n + 1) <= 'd)). (int('d), int('n))} on (33, unsigned(a))  | Coercion failed because: -  | (int(33), int('ex158#)) is not a subtype of (int('ex153#), int('ex154#)) +  | (int(33), int('ex167#)) is not a subtype of (int('ex162#), int('ex163#))  | [existential_ast3/v1.sail]:17:48-65  | 17 | if b == 0b0 then (64, unsigned(b @ a)) else (33, unsigned(a));  |  | ^---------------^ -  |  | 'ex153# bound here +  |  | 'ex162# bound here  | [existential_ast3/v1.sail]:17:48-65  | 17 | if b == 0b0 then (64, unsigned(b @ a)) else (33, unsigned(a));  |  | ^---------------^ -  |  | 'ex154# bound here +  |  | 'ex163# bound here  | [existential_ast3/v1.sail]:17:48-65  | 17 | if b == 0b0 then (64, unsigned(b @ a)) else (33, unsigned(a));  |  | ^---------------^ -  |  | 'ex158# bound here +  |  | 'ex167# bound here  | diff --git a/test/typecheck/pass/existential_ast3/v2.expect b/test/typecheck/pass/existential_ast3/v2.expect index 52eb2f13..8954736e 100644 --- a/test/typecheck/pass/existential_ast3/v2.expect +++ b/test/typecheck/pass/existential_ast3/v2.expect @@ -4,17 +4,17 @@ Type error:  | ^---------------^  | Tried performing type coercion from (int(31), range(0, (2 ^ 5 - 1))) to {('d : Int) ('n : Int), (datasize('d) & (0 <= 'n & ('n + 1) <= 'd)). (int('d), int('n))} on (31, unsigned(a))  | Coercion failed because: -  | (int(31), int('ex158#)) is not a subtype of (int('ex153#), int('ex154#)) +  | (int(31), int('ex167#)) is not a subtype of (int('ex162#), int('ex163#))  | [existential_ast3/v2.sail]:17:48-65  | 17 | if b == 0b0 then (64, unsigned(b @ a)) else (31, unsigned(a));  |  | ^---------------^ -  |  | 'ex153# bound here +  |  | 'ex162# bound here  | [existential_ast3/v2.sail]:17:48-65  | 17 | if b == 0b0 then (64, unsigned(b @ a)) else (31, unsigned(a));  |  | ^---------------^ -  |  | 'ex154# bound here +  |  | 'ex163# bound here  | [existential_ast3/v2.sail]:17:48-65  | 17 | if b == 0b0 then (64, unsigned(b @ a)) else (31, unsigned(a));  |  | ^---------------^ -  |  | 'ex158# bound here +  |  | 'ex167# bound here  | diff --git a/test/typecheck/pass/existential_ast3/v3.expect b/test/typecheck/pass/existential_ast3/v3.expect index 0e43cd52..d0fcdc06 100644 --- a/test/typecheck/pass/existential_ast3/v3.expect +++ b/test/typecheck/pass/existential_ast3/v3.expect @@ -3,5 +3,5 @@ Type error: 25 | Some(Ctor(64, unsigned(0b0 @ b @ a)))  | ^-----------------------------^  | Could not resolve quantifiers for Ctor -  | * (datasize(64) & (0 <= 'ex197# & ('ex197# + 1) <= 64)) +  | * (datasize(64) & (0 <= 'ex206# & ('ex206# + 1) <= 64))  | diff --git a/test/typecheck/pass/if_infer/v1.expect b/test/typecheck/pass/if_infer/v1.expect index 011ecbdf..e236d4b6 100644 --- a/test/typecheck/pass/if_infer/v1.expect +++ b/test/typecheck/pass/if_infer/v1.expect @@ -5,8 +5,7 @@ Type error:  | No overloading for vector_access, tried:  | * bitvector_access  | Could not resolve quantifiers for bitvector_access -  | * (0 <= 'ex115# & ('ex115# + 1) <= 3) +  | * (0 <= 'ex124# & ('ex124# + 1) <= 3)  | * plain_vector_access -  | Could not resolve quantifiers for plain_vector_access -  | * (0 <= 'ex118# & ('ex118# + 1) <= 3) +  | No valid casts resulted in unification  | diff --git a/test/typecheck/pass/if_infer/v2.expect b/test/typecheck/pass/if_infer/v2.expect index 9a34f688..fa7fb9ff 100644 --- a/test/typecheck/pass/if_infer/v2.expect +++ b/test/typecheck/pass/if_infer/v2.expect @@ -5,8 +5,7 @@ Type error:  | No overloading for vector_access, tried:  | * bitvector_access  | Could not resolve quantifiers for bitvector_access -  | * (0 <= 'ex115# & ('ex115# + 1) <= 4) +  | * (0 <= 'ex124# & ('ex124# + 1) <= 4)  | * plain_vector_access -  | Could not resolve quantifiers for plain_vector_access -  | * (0 <= 'ex118# & ('ex118# + 1) <= 4) +  | No valid casts resulted in unification  | diff --git a/test/typecheck/pass/if_infer/v3.expect b/test/typecheck/pass/if_infer/v3.expect index 7e0e74bb..b7447d0f 100644 --- a/test/typecheck/pass/if_infer/v3.expect +++ b/test/typecheck/pass/if_infer/v3.expect @@ -6,5 +6,5 @@ Type error:  | * bitvector_access  | Numeric type is non-simple  | * plain_vector_access -  | Numeric type is non-simple +  | No valid casts resulted in unification  | diff --git a/test/typecheck/pass/nexp_synonym/v1.expect b/test/typecheck/pass/nexp_synonym/v1.expect index 9ba21c2c..2f547747 100644 --- a/test/typecheck/pass/nexp_synonym/v1.expect +++ b/test/typecheck/pass/nexp_synonym/v1.expect @@ -2,7 +2,7 @@ Type error: [nexp_synonym/v1.sail]:7:20-31 7 |let v : bits(LEN) = 0xFFFF_FFFF  | ^---------^ -  | Tried performing type coercion from vector(32, dec, bit) to bits(LEN) on 0xFFFFFFFF +  | Tried performing type coercion from bitvector(32, dec) to bits(LEN) on 0xFFFFFFFF  | Coercion failed because:  | Mismatched argument types in subtype check  | diff --git a/test/typecheck/pass/nexp_synonym/v2.expect b/test/typecheck/pass/nexp_synonym/v2.expect index 68d664f7..c4bd774c 100644 --- a/test/typecheck/pass/nexp_synonym/v2.expect +++ b/test/typecheck/pass/nexp_synonym/v2.expect @@ -2,7 +2,7 @@ Type error: [nexp_synonym/v2.sail]:7:20-32 7 |let v : bits(LEN) = 0xFFFF_FFFFF  | ^----------^ -  | Tried performing type coercion from vector(36, dec, bit) to bits(LEN) on 0xFFFFFFFFF +  | Tried performing type coercion from bitvector(36, dec) to bits(LEN) on 0xFFFFFFFFF  | Coercion failed because:  | Mismatched argument types in subtype check  | diff --git a/test/typecheck/pass/nlflow.sail b/test/typecheck/pass/nlflow.sail index 95d2d280..9c426819 100644 --- a/test/typecheck/pass/nlflow.sail +++ b/test/typecheck/pass/nlflow.sail @@ -7,7 +7,7 @@ $include val foo : forall 'n, 'n != 8. int('n) -> unit -function test(xs: vector(4, dec, bit)) -> unit = { +function test(xs: bitvector(4, dec)) -> unit = { if xs == 0b1000 then { throw(Exception()) }; diff --git a/test/typecheck/pass/nzcv.sail b/test/typecheck/pass/nzcv.sail index dc625084..dd1734f6 100644 --- a/test/typecheck/pass/nzcv.sail +++ b/test/typecheck/pass/nzcv.sail @@ -1,9 +1,9 @@ default Order dec val vector_subrange = {ocaml: "subrange", lem: "subrange_vec_dec"} : forall ('n : Int) ('m : Int) ('o : Int), 'o <= 'm <= 'n. - (vector('n, dec, bit), atom('m), atom('o)) -> vector('m - ('o - 1), dec, bit) + (bitvector('n, dec), atom('m), atom('o)) -> bitvector('m - ('o - 1), dec) -val test : vector(4, dec, bit) -> unit +val test : bitvector(4, dec) -> unit function test nzcv = { N = 0b0; diff --git a/test/typecheck/pass/procstate1.sail b/test/typecheck/pass/procstate1.sail index 1d7e15b1..02453c72 100644 --- a/test/typecheck/pass/procstate1.sail +++ b/test/typecheck/pass/procstate1.sail @@ -2,13 +2,13 @@ default Order dec infix 4 == -val operator == = {lem: "eq_vec"} : forall 'n. (vector('n, dec, bit), vector('n, dec, bit)) -> bool +val operator == = {lem: "eq_vec"} : forall 'n. (bitvector('n, dec), bitvector('n, dec)) -> bool struct ProcState ('n : Int) = { - N : vector('n, dec, bit), - Z : vector(1, dec, bit), - C : vector(1, dec, bit), - V : vector(1, dec, bit) + N : bitvector('n, dec), + Z : bitvector(1, dec), + C : bitvector(1, dec), + V : bitvector(1, dec) } register PSTATE : ProcState(1) diff --git a/test/typecheck/pass/pure_record.sail b/test/typecheck/pass/pure_record.sail index 15f14a3b..fe324914 100644 --- a/test/typecheck/pass/pure_record.sail +++ b/test/typecheck/pass/pure_record.sail @@ -1,24 +1,24 @@ default Order dec -struct State ('a : Type) = { - N : vector(1, dec, 'a), - Z : vector(1, dec, bit) +struct State = { + N : bitvector(1, dec), + Z : bitvector(1, dec) } -val myStateM : unit -> State(bit) effect {undef} +val myStateM : unit -> State effect {undef} function myStateM () = { - r : State(bit) = undefined; + r : State = undefined; r.N = 0b1; r.Z = 0b1; r } -let myState : State(bit) = struct { N = 0b1, Z = 0b1 } +let myState : State = struct { N = 0b1, Z = 0b1 } val test : unit -> unit effect {undef} function test () = { - myState2 : State(bit) = struct { N = undefined, Z = 0b1 }; - myState3 : State(bit) = { myState2 with N = 0b0 } + myState2 : State = struct { N = undefined, Z = 0b1 }; + myState3 : State = { myState2 with N = 0b0 } } diff --git a/test/typecheck/pass/pure_record2.sail b/test/typecheck/pass/pure_record2.sail index 588fd324..fe6651db 100644 --- a/test/typecheck/pass/pure_record2.sail +++ b/test/typecheck/pass/pure_record2.sail @@ -1,24 +1,24 @@ default Order dec -struct State('a: Type, 'n: Int) = { - N : vector('n, dec, 'a), - Z : vector(1, dec, bit) +struct State('n: Int) = { + N : bitvector('n, dec), + Z : bitvector(1, dec) } -val myStateM : unit -> State(bit, 1) effect {undef} +val myStateM : unit -> State(1) effect {undef} function myStateM () = { - r : State(bit, 1) = undefined; + r : State(1) = undefined; r.N = 0b1; r.Z = 0b1; r } -let myState : State(bit, 1) = struct { N = 0b1, Z = 0b1 } +let myState : State(1) = struct { N = 0b1, Z = 0b1 } val test : unit -> unit effect {undef} function test () = { - myState2 : State(bit, 1) = struct { N = undefined, Z = 0b1 }; - myState3 : State(bit, 1) = { myState2 with N = 0b0 } + myState2 : State(1) = struct { N = undefined, Z = 0b1 }; + myState3 : State(1) = { myState2 with N = 0b0 } } diff --git a/test/typecheck/pass/pure_record3.sail b/test/typecheck/pass/pure_record3.sail index de388c3e..b1080a1a 100644 --- a/test/typecheck/pass/pure_record3.sail +++ b/test/typecheck/pass/pure_record3.sail @@ -1,27 +1,27 @@ default Order dec -struct State('a: Type, 'n: Int) = { - N : vector('n, dec, 'a), - Z : vector(1, dec, bit) +struct State('n: Int) = { + N : bitvector('n, dec), + Z : bitvector(1, dec) } -register procState : State(bit, 1) +register procState : State(1) -val myStateM : unit -> State(bit, 1) effect {undef} +val myStateM : unit -> State(1) effect {undef} function myStateM () = { - r : State(bit, 1) = undefined; + r : State(1) = undefined; r.N = 0b1; r.Z = 0b1; r } -let myState : State(bit, 1) = struct { N = 0b1, Z = 0b1 } +let myState : State(1) = struct { N = 0b1, Z = 0b1 } val test : unit -> unit effect {undef} function test () = { - myState1 : State(bit, 1) = undefined; - myState2 : State(bit, 1) = struct { N = undefined, Z = 0b1 }; - myState3 : State(bit, 1) = { myState2 with N = 0b0 } + myState1 : State(1) = undefined; + myState2 : State(1) = struct { N = undefined, Z = 0b1 }; + myState3 : State(1) = { myState2 with N = 0b0 } } diff --git a/test/typecheck/pass/reg_32_64/v2.expect b/test/typecheck/pass/reg_32_64/v2.expect index f007c917..24439bed 100644 --- a/test/typecheck/pass/reg_32_64/v2.expect +++ b/test/typecheck/pass/reg_32_64/v2.expect @@ -2,7 +2,7 @@ Type error: [reg_32_64/v2.sail]:21:18-22 21 | (*R)['d .. 0] = data  | ^--^ -  | Tried performing type coercion from vector('d, dec, bit) to vector((('d - 0) + 1), dec, bit) on data +  | Tried performing type coercion from bitvector('d, dec) to bitvector((('d - 0) + 1), dec) on data  | Coercion failed because:  | Mismatched argument types in subtype check  | This error occured because of a previous error: diff --git a/test/typecheck/pass/vec_length/v1.expect b/test/typecheck/pass/vec_length/v1.expect index ce61cf2a..36bd848e 100644 --- a/test/typecheck/pass/vec_length/v1.expect +++ b/test/typecheck/pass/vec_length/v1.expect @@ -7,6 +7,5 @@ Type error:  | Could not resolve quantifiers for bitvector_access  | * (0 <= 10 & (10 + 1) <= 8)  | * plain_vector_access -  | Could not resolve quantifiers for plain_vector_access -  | * (0 <= 10 & (10 + 1) <= 8) +  | No valid casts resulted in unification  | diff --git a/test/typecheck/pass/vec_length/v1_inc.expect b/test/typecheck/pass/vec_length/v1_inc.expect index 3d40cdb0..efbfcc54 100644 --- a/test/typecheck/pass/vec_length/v1_inc.expect +++ b/test/typecheck/pass/vec_length/v1_inc.expect @@ -7,6 +7,5 @@ Type error:  | Could not resolve quantifiers for bitvector_access  | * (0 <= 10 & (10 + 1) <= 8)  | * plain_vector_access -  | Could not resolve quantifiers for plain_vector_access -  | * (0 <= 10 & (10 + 1) <= 8) +  | No valid casts resulted in unification  | diff --git a/test/typecheck/pass/vec_length/v2.expect b/test/typecheck/pass/vec_length/v2.expect index c77ecaa7..9ce8f9a2 100644 --- a/test/typecheck/pass/vec_length/v2.expect +++ b/test/typecheck/pass/vec_length/v2.expect @@ -7,6 +7,5 @@ Type error:  | Could not resolve quantifiers for bitvector_update  | * (0 <= 10 & (10 + 1) <= 8)  | * plain_vector_update -  | Could not resolve quantifiers for plain_vector_update -  | * (0 <= 10 & (10 + 1) <= 8) +  | No valid casts resulted in unification  | diff --git a/test/typecheck/pass/vec_length/v2_inc.expect b/test/typecheck/pass/vec_length/v2_inc.expect index cff65f62..dba312ea 100644 --- a/test/typecheck/pass/vec_length/v2_inc.expect +++ b/test/typecheck/pass/vec_length/v2_inc.expect @@ -7,6 +7,5 @@ Type error:  | Could not resolve quantifiers for bitvector_update  | * (0 <= 10 & (10 + 1) <= 8)  | * plain_vector_update -  | Could not resolve quantifiers for plain_vector_update -  | * (0 <= 10 & (10 + 1) <= 8) +  | No valid casts resulted in unification  | diff --git a/test/typecheck/pass/vec_length/v3.expect b/test/typecheck/pass/vec_length/v3.expect index e3afecee..88e6fa50 100644 --- a/test/typecheck/pass/vec_length/v3.expect +++ b/test/typecheck/pass/vec_length/v3.expect @@ -9,6 +9,5 @@ Type error:  | Could not resolve quantifiers for bitvector_access  | * (0 <= 10 & (10 + 1) <= 8)  | * plain_vector_access -  | Could not resolve quantifiers for plain_vector_access -  | * (0 <= 10 & (10 + 1) <= 8) +  | No valid casts resulted in unification  | diff --git a/test/typecheck/pass/vec_pat1.sail b/test/typecheck/pass/vec_pat1.sail index 6de87a8c..e11a8654 100644 --- a/test/typecheck/pass/vec_pat1.sail +++ b/test/typecheck/pass/vec_pat1.sail @@ -1,15 +1,15 @@ default Order inc val bv_add = {ocaml: "add_vec", lem: "add_vec"}: forall ('n : Int). - (vector('n, inc, bit), vector('n, inc, bit)) -> vector('n, inc, bit) + (bitvector('n, inc), bitvector('n, inc)) -> bitvector('n, inc) val vector_subrange = {ocaml: "subrange", lem: "subrange_vec_inc"}: forall ('l : Int) ('m : Int) ('o : Int), 'l >= 0 & 'm <= 'o & 'o <= 'l. - (vector('l, inc, bit), atom('m), atom('o)) -> vector('o + 1 - 'm, inc, bit) + (bitvector('l, inc), atom('m), atom('o)) -> bitvector('o + 1 - 'm, inc) val bitvector_concat = {ocaml: "append", lem: "concat_vec"} : forall ('m : Int) ('p : Int). - (vector('m, inc, bit), vector('p, inc, bit)) -> vector('m + 'p, inc, bit) + (bitvector('m, inc), bitvector('p, inc)) -> bitvector('m + 'p, inc) -val eq_vec = {ocaml: "eq_list", lem: "eq_vec"} : forall 'n. (vector('n, inc, bit), vector('n, inc, bit)) -> bool +val eq_vec = {ocaml: "eq_list", lem: "eq_vec"} : forall 'n. (bitvector('n, inc), bitvector('n, inc)) -> bool infix 4 == overload operator == = {eq_vec} @@ -18,6 +18,6 @@ overload operator + = {bv_add} overload append = {bitvector_concat} -val test : (vector(3, inc, bit), vector(3, inc, bit)) -> vector(3, inc, bit) +val test : (bitvector(3, inc), bitvector(3, inc)) -> bitvector(3, inc) -function test (x : vector(1, inc, bit) @ 0b1 @ 0b0, z) = (x @ 0b11) + z +function test (x : bitvector(1, inc) @ 0b1 @ 0b0, z) = (x @ 0b11) + z diff --git a/test/typecheck/pass/vector_subrange_gen.sail b/test/typecheck/pass/vector_subrange_gen.sail index b82d6c8c..9f7f4e49 100644 --- a/test/typecheck/pass/vector_subrange_gen.sail +++ b/test/typecheck/pass/vector_subrange_gen.sail @@ -1,23 +1,17 @@ -val vector_access : forall ('l : Int) ('o : Order) ('a : Type), 'l >= 0. - (vector('l, 'o, 'a), range(0, 'l - 1)) -> 'a - -val vector_append : forall ('l1 : Int) ('l2 : Int) ('o : Order) ('a : Type), 'l1 >= 0 & 'l2 >= 0. - (vector('l1, 'o, 'a), vector('l2, 'o, 'a)) -> vector('l1 + 'l2, 'o, 'a) - val vector_subrange = {ocaml: "subrange", lem: "subrange_vec_inc"} : forall ('l : Int) ('m : Int) ('o : Int), 'l >= 0 & 'm <= 'o & 'o <= 'l. - (vector('l, inc, bit), atom('m), atom('o)) -> vector('o - 'm + 1, inc, bit) + (bitvector('l, inc), atom('m), atom('o)) -> bitvector('o - 'm + 1, inc) val sub : forall ('n : Int) ('m : Int). (atom('n), atom('m)) -> atom('n - 'm) -val "length" : forall ('n : Int). vector('n, inc, bit) -> atom('n) +val bitvector_length = "length" : forall ('n : Int). bitvector('n, inc) -> atom('n) -overload __size = {length} +overload __size = {bitvector_length} default Order inc val test : forall 'n 'm, 'n >= 5. - vector('n, inc, bit) -> vector('n - 1, inc, bit) + bitvector('n, inc) -> bitvector('n - 1, inc) function test v = { z = vector_subrange(v, 0, sub('n, 2)); -- cgit v1.2.3