diff options
Diffstat (limited to 'test/typecheck')
31 files changed, 145 insertions, 98 deletions
diff --git a/test/typecheck/pass/add_vec_lit.sail b/test/typecheck/pass/add_vec_lit.sail index be897021..4d662a8d 100644 --- a/test/typecheck/pass/add_vec_lit.sail +++ b/test/typecheck/pass/add_vec_lit.sail @@ -3,7 +3,7 @@ default Order inc val extern forall Num 'n. (bit['n], bit['n]) -> bit['n] effect pure add_vec = "add_vec" val extern forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n+'o:'m+'p|] effect pure add_range = "add_range" -val cast forall Num 'n. bit['n] -> [|0: 2** 'n - 1|] effect pure cast_vec_range +val cast forall Num 'n. bit['n] -> [|0: 2** 'n - 1|] effect pure unsigned overload (deinfix +) [add_vec; add_range] diff --git a/test/typecheck/pass/arm_FPEXC1.sail b/test/typecheck/pass/arm_FPEXC1.sail index cfae86a1..f711a5ad 100644 --- a/test/typecheck/pass/arm_FPEXC1.sail +++ b/test/typecheck/pass/arm_FPEXC1.sail @@ -1,9 +1,9 @@ default Order dec -val forall Num 'n. (bit['n], int) -> bit effect pure vector_access +val extern forall Num 'n. (bit['n], int) -> bit effect pure vector_access = "bitvector_access_dec" -val forall Num 'n, Num 'm, Num 'o, 'm >= 'o, 'o >= 0, 'n >= 'm + 1. - (bit['n], [:'m:], [:'o:]) -> bit['m - ('o - 1)] effect pure vector_subrange +val extern forall Num 'n, Num 'm, Num 'o, 'm >= 'o, 'o >= 0, 'n >= 'm + 1. + (bit['n], [:'m:], [:'o:]) -> bit['m - ('o - 1)] effect pure vector_subrange = "bitvector_subrange_dec" register vector<32 - 1, 32, dec, bit> _FPEXC32_EL2 diff --git a/test/typecheck/pass/bv_simple_index.sail b/test/typecheck/pass/bv_simple_index.sail index 72e1b094..811b3a5b 100644 --- a/test/typecheck/pass/bv_simple_index.sail +++ b/test/typecheck/pass/bv_simple_index.sail @@ -1,7 +1,7 @@ -val forall Nat 'n, Nat 'l, Type 'a, 'l >= 0. (vector<'n,'l,dec,'a>, [|'n - 'l + 1:'n|]) -> 'a effect pure vector_access_dec -val forall Nat 'n, Nat 'l, Type 'a, 'l >= 0. (vector<'n,'l,inc,'a>, [|'n:'n + 'l - 1|]) -> 'a effect pure vector_access_inc +val forall Nat 'n, Nat 'l, 'l >= 0. (vector<'n,'l,dec,bit>, [|'n - 'l + 1:'n|]) -> bit effect pure bitvector_access_dec +val forall Nat 'n, Nat 'l, 'l >= 0. (vector<'n,'l,inc,bit>, [|'n:'n + 'l - 1|]) -> bit effect pure bitvector_access_inc -overload vector_access [vector_access_inc; vector_access_dec] +overload vector_access [bitvector_access_inc; bitvector_access_dec] val cast bit -> bool effect pure cast_bit_bool diff --git a/test/typecheck/pass/bv_simple_index_bit.sail b/test/typecheck/pass/bv_simple_index_bit.sail index 2ba5b928..46bc19d6 100644 --- a/test/typecheck/pass/bv_simple_index_bit.sail +++ b/test/typecheck/pass/bv_simple_index_bit.sail @@ -1,7 +1,7 @@ -val forall Nat 'n, Nat 'l, Type 'a, 'l >= 0. (vector<'n,'l,dec,'a>, [|'n - 'l + 1:'n|]) -> 'a effect pure vector_access_dec -val forall Nat 'n, Nat 'l, Type 'a, 'l >= 0. (vector<'n,'l,inc,'a>, [|'n:'n + 'l - 1|]) -> 'a effect pure vector_access_inc +val forall Nat 'n, Nat 'l, 'l >= 0. (vector<'n,'l,dec,bit>, [|'n - 'l + 1:'n|]) -> bit effect pure bitvector_access_dec +val forall Nat 'n, Nat 'l, 'l >= 0. (vector<'n,'l,inc,bit>, [|'n:'n + 'l - 1|]) -> bit effect pure bitvector_access_inc -overload vector_access [vector_access_inc; vector_access_dec] +overload vector_access [bitvector_access_inc; bitvector_access_dec] function bit bv ((bit[64]) x) = { diff --git a/test/typecheck/pass/case_simple_constraints.sail b/test/typecheck/pass/case_simple_constraints.sail index f1b87235..335e10ee 100644 --- a/test/typecheck/pass/case_simple_constraints.sail +++ b/test/typecheck/pass/case_simple_constraints.sail @@ -1,9 +1,9 @@ -val forall Nat 'n, Nat 'm. ([:'n + 20:], [:'m:]) -> [:'n + 20 + 'm:] effect pure plus +val extern forall Nat 'n, Nat 'm. ([:'n + 20:], [:'m:]) -> [:'n + 20 + 'm:] effect pure plus = "add" -val forall Nat 'n, 'n <= -10. [:'n:] -> [:'n:] effect pure minus_ten_id +val extern forall Nat 'n, 'n <= -10. [:'n:] -> [:'n:] effect pure minus_ten_id = "id" -val forall Nat 'n, 'n >= 10. [:'n:] -> [:'n:] effect pure ten_id +val extern forall Nat 'n, 'n >= 10. [:'n:] -> [:'n:] effect pure ten_id = "id" val forall Nat 'N, 'N >= 63. [|10:'N|] -> [|10:'N|] effect pure branch diff --git a/test/typecheck/pass/deinfix_plus.sail b/test/typecheck/pass/deinfix_plus.sail index c5a0f1ee..8fc7c00e 100644 --- a/test/typecheck/pass/deinfix_plus.sail +++ b/test/typecheck/pass/deinfix_plus.sail @@ -1,6 +1,6 @@ default Order inc -val extern forall Num 'n. (bit['n], bit['n]) -> bit['n] effect pure bv_add = "bv_add_inc" +val extern forall Num 'n. (bit['n], bit['n]) -> bit['n] effect pure bv_add = "add_vec" overload (deinfix +) [bv_add] diff --git a/test/typecheck/pass/flow_gt1.sail b/test/typecheck/pass/flow_gt1.sail index acfbab68..ddeefd53 100644 --- a/test/typecheck/pass/flow_gt1.sail +++ b/test/typecheck/pass/flow_gt1.sail @@ -1,17 +1,17 @@ default Order inc -val forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n+'o:'m+'p|] effect pure add_range +val extern forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n+'o:'m+'p|] effect pure add_range = "add" -val forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n-'p:'m-'o|] effect pure sub_range +val extern forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n-'p:'m-'o|] effect pure sub_range = "sub" -val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure lt_range_atom -val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure lteq_range_atom -val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure gt_range_atom -val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure gteq_range_atom -val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure lt_atom_range -val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure lteq_atom_range -val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure gt_atom_range -val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure gteq_atom_range +val extern forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure lt_range_atom = "lt" +val extern forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure lteq_range_atom = "lteq" +val extern forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure gt_range_atom = "gt" +val extern forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure gteq_range_atom = "gteq" +val extern forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure lt_atom_range = "lt" +val extern forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure lteq_atom_range = "lteq" +val extern forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure gt_atom_range = "gt" +val extern forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure gteq_atom_range = "gteq" overload (deinfix +) [add_range] overload (deinfix -) [sub_range] diff --git a/test/typecheck/pass/flow_gteq1.sail b/test/typecheck/pass/flow_gteq1.sail index 8918438c..47f7aa0f 100644 --- a/test/typecheck/pass/flow_gteq1.sail +++ b/test/typecheck/pass/flow_gteq1.sail @@ -1,17 +1,17 @@ default Order inc -val forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n+'o:'m+'p|] effect pure add_range +val extern forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n+'o:'m+'p|] effect pure add_range = "add" -val forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n-'p:'m-'o|] effect pure sub_range +val extern forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n-'p:'m-'o|] effect pure sub_range = "sub" -val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure lt_range_atom -val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure lteq_range_atom -val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure gt_range_atom -val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure gteq_range_atom -val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure lt_atom_range -val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure lteq_atom_range -val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure gt_atom_range -val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure gteq_atom_range +val extern forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure lt_range_atom = "lt" +val extern forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure lteq_range_atom = "lteq" +val extern forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure gt_range_atom = "gt" +val extern forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure gteq_range_atom = "gteq" +val extern forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure lt_atom_range = "lt" +val extern forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure lteq_atom_range = "lteq" +val extern forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure gt_atom_range = "gt" +val extern forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure gteq_atom_range = "gteq" overload (deinfix +) [add_range] overload (deinfix -) [sub_range] diff --git a/test/typecheck/pass/flow_lt1.sail b/test/typecheck/pass/flow_lt1.sail index 0f3c1bbc..c210ed7a 100644 --- a/test/typecheck/pass/flow_lt1.sail +++ b/test/typecheck/pass/flow_lt1.sail @@ -1,11 +1,17 @@ default Order inc -val forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n+'o:'m+'p|] effect pure add_range +val extern forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n+'o:'m+'p|] effect pure add_range = "add" -val forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n-'p:'m-'o|] effect pure sub_range +val extern forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n-'p:'m-'o|] effect pure sub_range = "sub" -val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure lt_range_atom -val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure lt_atom_range +val extern forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure lt_range_atom = "lt" +val extern forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure lteq_range_atom = "lteq" +val extern forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure gt_range_atom = "gt" +val extern forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure gteq_range_atom = "gteq" +val extern forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure lt_atom_range = "lt" +val extern forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure lteq_atom_range = "lteq" +val extern forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure gt_atom_range = "gt" +val extern forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure gteq_atom_range = "gteq" overload (deinfix +) [add_range] overload (deinfix -) [sub_range] diff --git a/test/typecheck/pass/flow_lt2.sail b/test/typecheck/pass/flow_lt2.sail index effe0bc4..cccebaa3 100644 --- a/test/typecheck/pass/flow_lt2.sail +++ b/test/typecheck/pass/flow_lt2.sail @@ -1,11 +1,17 @@ default Order inc -val forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n+'o:'m+'p|] effect pure add_range +val extern forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n+'o:'m+'p|] effect pure add_range = "add" -val forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n-'p:'m-'o|] effect pure sub_range +val extern forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n-'p:'m-'o|] effect pure sub_range = "sub" -val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure lt_range_atom -val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure lt_atom_range +val extern forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure lt_range_atom = "lt" +val extern forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure lteq_range_atom = "lteq" +val extern forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure gt_range_atom = "gt" +val extern forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure gteq_range_atom = "gteq" +val extern forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure lt_atom_range = "lt" +val extern forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure lteq_atom_range = "lteq" +val extern forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure gt_atom_range = "gt" +val extern forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure gteq_atom_range = "gteq" overload (deinfix +) [add_range] overload (deinfix -) [sub_range] diff --git a/test/typecheck/pass/flow_lt_assign.sail b/test/typecheck/pass/flow_lt_assign.sail index 4e787741..9601f48f 100644 --- a/test/typecheck/pass/flow_lt_assign.sail +++ b/test/typecheck/pass/flow_lt_assign.sail @@ -1,11 +1,17 @@ default Order inc -val forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n+'o:'m+'p|] effect pure add_range +val extern forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n+'o:'m+'p|] effect pure add_range = "add" -val forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n-'p:'m-'o|] effect pure sub_range +val extern forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n-'p:'m-'o|] effect pure sub_range = "sub" -val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure lt_range_atom -val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure lt_atom_range +val extern forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure lt_range_atom = "lt" +val extern forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure lteq_range_atom = "lteq" +val extern forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure gt_range_atom = "gt" +val extern forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure gteq_range_atom = "gteq" +val extern forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure lt_atom_range = "lt" +val extern forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure lteq_atom_range = "lteq" +val extern forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure gt_atom_range = "gt" +val extern forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure gteq_atom_range = "gteq" overload (deinfix +) [add_range] overload (deinfix -) [sub_range] diff --git a/test/typecheck/pass/flow_lteq1.sail b/test/typecheck/pass/flow_lteq1.sail index d32831a2..ffa4dd8b 100644 --- a/test/typecheck/pass/flow_lteq1.sail +++ b/test/typecheck/pass/flow_lteq1.sail @@ -1,17 +1,17 @@ default Order inc -val forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n+'o:'m+'p|] effect pure add_range +val extern forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n+'o:'m+'p|] effect pure add_range = "add" -val forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n-'p:'m-'o|] effect pure sub_range +val extern forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n-'p:'m-'o|] effect pure sub_range = "sub" -val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure lt_range_atom -val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure lteq_range_atom -val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure gt_range_atom -val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure gteq_range_atom -val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure lt_atom_range -val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure lteq_atom_range -val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure gt_atom_range -val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure gteq_atom_range +val extern forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure lt_range_atom = "lt" +val extern forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure lteq_range_atom = "lteq" +val extern forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure gt_range_atom = "gt" +val extern forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure gteq_range_atom = "gteq" +val extern forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure lt_atom_range = "lt" +val extern forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure lteq_atom_range = "lteq" +val extern forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure gt_atom_range = "gt" +val extern forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure gteq_atom_range = "gteq" overload (deinfix +) [add_range] overload (deinfix -) [sub_range] diff --git a/test/typecheck/pass/let_subtyp_bug.sail b/test/typecheck/pass/let_subtyp_bug.sail new file mode 100644 index 00000000..e2abde2d --- /dev/null +++ b/test/typecheck/pass/let_subtyp_bug.sail @@ -0,0 +1,9 @@ +let ([|5|]) y = 2 + +val unit -> nat effect pure test + +function test() = { + let ([|5|]) x = 2 in + x +} +
\ No newline at end of file diff --git a/test/typecheck/pass/list_cons.sail b/test/typecheck/pass/list_cons.sail new file mode 100644 index 00000000..6f103bf6 --- /dev/null +++ b/test/typecheck/pass/list_cons.sail @@ -0,0 +1 @@ +function list<int> foo ((int) i, (list<int>) l) = i :: l diff --git a/test/typecheck/pass/list_cons2.sail b/test/typecheck/pass/list_cons2.sail new file mode 100644 index 00000000..8c34282b --- /dev/null +++ b/test/typecheck/pass/list_cons2.sail @@ -0,0 +1,7 @@ +function list<int> foo ((int) i, (list<int>) l) = i :: l + +function list<int> bar () = [||||] + +function list<int> baz ((list<int>) l) = l + +function list<int> quux () = baz ([||||]) diff --git a/test/typecheck/pass/list_lit.sail b/test/typecheck/pass/list_lit.sail new file mode 100644 index 00000000..d4febadf --- /dev/null +++ b/test/typecheck/pass/list_lit.sail @@ -0,0 +1,2 @@ + +let (list<int>) xs = [||1,2,3,4,5,6||] diff --git a/test/typecheck/pass/mips_CP0Cause_BD_assign1.sail b/test/typecheck/pass/mips_CP0Cause_BD_assign1.sail index 4dc63e71..7808b2c0 100644 --- a/test/typecheck/pass/mips_CP0Cause_BD_assign1.sail +++ b/test/typecheck/pass/mips_CP0Cause_BD_assign1.sail @@ -1,5 +1,5 @@ -val cast forall Nat 'n, Order 'ord. [:1:] -> vector<'n,1,'ord,bit> effect pure cast_one_bv -val cast forall Nat 'n, Order 'ord. [:0:] -> vector<'n,1,'ord,bit> effect pure cast_zero_bv +val cast forall Nat 'n, Order 'ord. [:1:] -> vector<'n,1,'ord,bit> effect pure cast_1_vec +val cast forall Nat 'n, Order 'ord. [:0:] -> vector<'n,1,'ord,bit> effect pure cast_0_vec default Order dec diff --git a/test/typecheck/pass/mips_CP0Cause_BD_assign2.sail b/test/typecheck/pass/mips_CP0Cause_BD_assign2.sail index b35a0767..26f161e2 100644 --- a/test/typecheck/pass/mips_CP0Cause_BD_assign2.sail +++ b/test/typecheck/pass/mips_CP0Cause_BD_assign2.sail @@ -1,5 +1,5 @@ -val cast forall Nat 'n, Order 'ord. [:1:] -> vector<'n,1,'ord,bit> effect pure cast_one_bv -val cast forall Nat 'n, Order 'ord. [:0:] -> vector<'n,1,'ord,bit> effect pure cast_zero_bv +val cast forall Nat 'n, Order 'ord. [:1:] -> vector<'n,1,'ord,bit> effect pure cast_1_vec +val cast forall Nat 'n, Order 'ord. [:0:] -> vector<'n,1,'ord,bit> effect pure cast_0_vec default Order dec diff --git a/test/typecheck/pass/mips_CP0Cause_access.sail b/test/typecheck/pass/mips_CP0Cause_access.sail index c0e318c4..eb3b9389 100644 --- a/test/typecheck/pass/mips_CP0Cause_access.sail +++ b/test/typecheck/pass/mips_CP0Cause_access.sail @@ -3,10 +3,10 @@ effect pure ADJUST *) -val forall Num 'n, Num 'l, Type 'a, 'l >= 0. (vector<'n,'l,dec,'a>, [|'n - 'l + 1:'n|]) -> 'a effect pure vector_access_dec -val forall Nat 'n, Nat 'l, Type 'a, 'l >= 0. (vector<'n,'l,inc,'a>, [|'n:'n + 'l - 1|]) -> 'a effect pure vector_access_inc +val extern forall Num 'n, Num 'l, 'l >= 0. (vector<'n,'l,dec,bit>, [|'n - 'l + 1:'n|]) -> bit effect pure bitvector_access_dec +val extern forall Nat 'n, Nat 'l, 'l >= 0. (vector<'n,'l,inc,bit>, [|'n:'n + 'l - 1|]) -> bit effect pure bitvector_access_inc -overload vector_access [vector_access_inc; vector_access_dec] +overload vector_access [bitvector_access_inc; bitvector_access_dec] default Order dec diff --git a/test/typecheck/pass/mips_reg_field_bit.sail b/test/typecheck/pass/mips_reg_field_bit.sail index 33560bde..4c37a6e9 100644 --- a/test/typecheck/pass/mips_reg_field_bit.sail +++ b/test/typecheck/pass/mips_reg_field_bit.sail @@ -1,8 +1,8 @@ +default Order dec + val cast forall Nat 'n, Nat 'm, Nat 'o, 'o >= 'm - 1. vector<'n,'m,dec,bit> -> vector<'o,'m,dec,bit> - effect pure ADJUST - -default Order dec + effect pure adjust_dec typedef CauseReg = register bits [ 31 : 0 ] { 31 : BD; (* branch delay *) diff --git a/test/typecheck/pass/mips_reg_field_bv.sail b/test/typecheck/pass/mips_reg_field_bv.sail index 4b82d4de..0ce19b4f 100644 --- a/test/typecheck/pass/mips_reg_field_bv.sail +++ b/test/typecheck/pass/mips_reg_field_bv.sail @@ -1,8 +1,8 @@ +default Order dec + val cast forall Nat 'n, Nat 'm, Nat 'o, 'o >= 'm - 1. vector<'n,'m,dec,bit> -> vector<'o,'m,dec,bit> - effect pure ADJUST - -default Order dec + effect pure adjust_dec typedef CauseReg = register bits [ 31 : 0 ] { 31 : BD; (* branch delay *) diff --git a/test/typecheck/pass/overload_plus.sail b/test/typecheck/pass/overload_plus.sail index 5390a5a4..2aa8ecc5 100644 --- a/test/typecheck/pass/overload_plus.sail +++ b/test/typecheck/pass/overload_plus.sail @@ -1,6 +1,6 @@ default Order inc -val extern forall Nat 'n. (bit['n], bit['n]) -> bit['n] effect pure bv_add = "bv_add_inc" +val extern forall Nat 'n. (bit['n], bit['n]) -> bit['n] effect pure bv_add = "add_vec" overload (deinfix +) [bv_add] diff --git a/test/typecheck/pass/regtyp_vec.sail b/test/typecheck/pass/regtyp_vec.sail index c939cce8..28978882 100644 --- a/test/typecheck/pass/regtyp_vec.sail +++ b/test/typecheck/pass/regtyp_vec.sail @@ -3,12 +3,12 @@ effect pure ADJUST *) -val forall Nat 'n, Nat 'l, Type 'a, 'l >= 0. (vector<'n,'l,dec,'a>, [|'n - 'l + 1:'n|]) -> 'a effect pure vector_access_dec +val forall Nat 'n, Nat 'l, 'l >= 0. (vector<'n,'l,dec,bit>, [|'n - 'l + 1:'n|]) -> bit effect pure bitvector_access_dec (* val forall Nat 'n, Nat 'l, Type 'a, 'l >= 0. (vector<'n,'l,inc,'a>, [|'n:'n + 'l - 1|]) -> 'a effect pure vector_access_inc *) -overload vector_access [vector_access_dec] +overload vector_access [bitvector_access_dec] default Order dec diff --git a/test/typecheck/pass/set_mark.sail b/test/typecheck/pass/set_mark.sail index 59710c46..7bc7370b 100644 --- a/test/typecheck/pass/set_mark.sail +++ b/test/typecheck/pass/set_mark.sail @@ -1,5 +1,5 @@ -val cast forall Num 'n, Num 'm, Order 'ord. [:0:] -> vector<'n,'m,'ord,bit> effect pure cast_zero_bv +val cast forall Num 'n, Num 'm, Order 'ord. [:0:] -> vector<'n,'m,'ord,bit> effect pure cast_0_vec function forall Num 'N, 'N IN {32}. bit['N] Foo32( (bit['N]) x) = x diff --git a/test/typecheck/pass/set_mark2.sail b/test/typecheck/pass/set_mark2.sail index c1433058..cabfb1af 100644 --- a/test/typecheck/pass/set_mark2.sail +++ b/test/typecheck/pass/set_mark2.sail @@ -1,4 +1,4 @@ -val cast forall Num 'n, Num 'm, Order 'ord. [:0:] -> vector<'n,'m,'ord,bit> effect pure cast_zero_bv +val cast forall Num 'n, Num 'm, Order 'ord. [:0:] -> vector<'n,'m,'ord,bit> effect pure cast_0_vec function forall Nat 'N, 'N IN {32, 64}. bit['N] Foo32( (bit['N]) x) = x diff --git a/test/typecheck/pass/vec_pat1.sail b/test/typecheck/pass/vec_pat1.sail index 0a79d701..fe9b4a0a 100644 --- a/test/typecheck/pass/vec_pat1.sail +++ b/test/typecheck/pass/vec_pat1.sail @@ -1,13 +1,16 @@ default Order inc -val extern forall Num 'n. (bit['n], bit['n]) -> bit['n] effect pure bv_add = "bv_add_inc" +val extern forall Num 'n. (bit['n], bit['n]) -> bit['n] effect pure bv_add = "add_vec" -val forall Num 'n, Num 'm, Num 'o, Num 'p, Type 'a. - (vector<'n,'m,inc,'a>, vector<'o,'p,inc,'a>) -> vector<'n,'m + 'p,inc,'a> - effect pure vector_append_inc +val extern forall Num 'n, Num 'l, Num 'm, Num 'o, 'l >= 0, 'm <= 'o, 'o <= 'l. + (vector<'n,'l,inc,bit>, [:'m:], [:'o:]) -> vector<'m,'o + 1 - 'm,inc,bit> effect pure vector_subrange = "bitvector_subrange_inc" + +val forall Num 'n, Num 'm, Num 'o, Num 'p. + (vector<'n,'m,inc,bit>, vector<'o,'p,inc,bit>) -> vector<'n,'m + 'p,inc,bit> + effect pure bitvector_concat overload (deinfix +) [bv_add] -overload vector_append [vector_append_inc] +overload vector_append [bitvector_concat] val (bit[3], bit[3]) -> bit[3] effect pure test diff --git a/test/typecheck/pass/vector_append.sail b/test/typecheck/pass/vector_append.sail index af83c44d..17db3fbd 100644 --- a/test/typecheck/pass/vector_append.sail +++ b/test/typecheck/pass/vector_append.sail @@ -1,7 +1,6 @@ - -val forall Nat 'n1, Nat 'l1, Nat 'n2, Nat 'l2, Order 'o, Type 'a, 'l1 >= 0, 'l2 >= 0. - (vector<'n1,'l1,'o,'a>, vector<'n2,'l2,'o,'a>) -> vector<'n1,'l1 + 'l2,'o,'a> effect pure vector_append +val extern forall Nat 'n1, Nat 'l1, Nat 'n2, Nat 'l2, Order 'o, 'l1 >= 0, 'l2 >= 0. + (vector<'n1,'l1,'o,bit>, vector<'n2,'l2,'o,bit>) -> vector<'n1,'l1 + 'l2,'o,bit> effect pure vector_append = "bitvector_concat" default Order inc @@ -12,4 +11,4 @@ function bit[8] test (v1, v2) = zv := vector_append(v1, v2); zv := v1 : v2; zv -}
\ No newline at end of file +} diff --git a/test/typecheck/pass/vector_append_gen.sail b/test/typecheck/pass/vector_append_gen.sail index ddb027ee..ce63ed87 100644 --- a/test/typecheck/pass/vector_append_gen.sail +++ b/test/typecheck/pass/vector_append_gen.sail @@ -1,8 +1,6 @@ -val forall Nat 'n, Nat 'l, Order 'o, Type 'a, 'l >= 0. (vector<'n,'l,'o,'a>, [|'n:'n + 'l - 1|]) -> 'a effect pure vector_access - -val forall Nat 'n1, Nat 'l1, Nat 'n2, Nat 'l2, Order 'o, Type 'a, 'l1 >= 0, 'l2 >= 0. - (vector<'n1,'l1,'o,'a>, vector<'n2,'l2,'o,'a>) -> vector<'n1,'l1 + 'l2,'o,'a> effect pure vector_append +val extern forall Nat 'n1, Nat 'l1, Nat 'n2, Nat 'l2, Order 'o, 'l1 >= 0, 'l2 >= 0. + (vector<'n1,'l1,'o,bit>, vector<'n2,'l2,'o,bit>) -> vector<'n1,'l1 + 'l2,'o,bit> effect pure vector_append = "bitvector_concat" default Order inc @@ -11,4 +9,4 @@ val forall 'n, 'm, 'n >= 0, 'm >= 0. (bit['n], bit['m]) -> bit['n + 'm] effect p function forall 'n, 'm. bit['n + 'm] test (v1, v2) = { vector_append(v1, v2); -}
\ No newline at end of file +} diff --git a/test/typecheck/pass/vector_subrange_gen.sail b/test/typecheck/pass/vector_subrange_gen.sail index 8857bd18..4ec067de 100644 --- a/test/typecheck/pass/vector_subrange_gen.sail +++ b/test/typecheck/pass/vector_subrange_gen.sail @@ -4,17 +4,18 @@ val forall Nat 'n, Nat 'l, Order 'o, Type 'a, 'l >= 0. (vector<'n,'l,'o,'a>, [|' val forall Nat 'n1, Nat 'l1, Nat 'n2, Nat 'l2, Order 'o, Type 'a, 'l1 >= 0, 'l2 >= 0. (vector<'n1,'l1,'o,'a>, vector<'n2,'l2,'o,'a>) -> vector<'n1,'l1 + 'l2,'o,'a> effect pure vector_append -val forall Nat 'n, Nat 'l, Nat 'm, Nat 'u, Order 'o, Type 'a, 'l >= 0, 'm <= 'u, 'u <= 'l. (vector<'n,'l,'o,'a>, [:'m:], [:'u:]) -> vector<'m,'u - 'm,'o,'a> effect pure vector_subrange +val extern forall Num 'n, Num 'l, Num 'm, Num 'o, 'l >= 0, 'm <= 'o, 'o <= 'l. + (vector<'n,'l,inc,bit>, [:'m:], [:'o:]) -> vector<'m,('o - 'm) + 1,inc,bit> effect pure vector_subrange = "bitvector_subrange_inc" -val forall Nat 'n, Nat 'm. ([:'n:], [:'m:]) -> [:'n - 'm:] effect pure minus +val forall Nat 'n, Nat 'm. ([:'n:], [:'m:]) -> [:'n - 'm:] effect pure sub default Order inc -val forall 'n, 'm, 'n >= 5. bit['n] -> bit['n - 2] effect pure test +val forall 'n, 'm, 'n >= 5. bit['n] -> bit['n - 1] effect pure test -function forall 'n, 'n >= 5. bit['n - 2] test v = +function forall 'n, 'n >= 5. bit['n - 1] test v = { - z := vector_subrange(v, 0, minus(sizeof 'n, 2)); - z := v[0 .. minus(sizeof 'n, 2)]; + z := vector_subrange(v, 0, sub(sizeof 'n, 2)); + z := v[0 .. sub(sizeof 'n, 2)]; z -}
\ No newline at end of file +} diff --git a/test/typecheck/pass/vector_synonym_cast.sail b/test/typecheck/pass/vector_synonym_cast.sail index 72a7e9d0..f1de42e9 100644 --- a/test/typecheck/pass/vector_synonym_cast.sail +++ b/test/typecheck/pass/vector_synonym_cast.sail @@ -1,7 +1,7 @@ typedef vecsyn = vector<0,1,dec,bit> -val cast vector<1,1,dec,bit> -> vector<0,1,dec,bit> effect pure test_cast +val cast vector<1,1,dec,bit> -> vector<0,1,dec,bit> effect pure adjust_dec val vector<1,1,dec,bit> -> vecsyn effect pure test diff --git a/test/typecheck/run_tests.sh b/test/typecheck/run_tests.sh index 8659e60e..073a6251 100755 --- a/test/typecheck/run_tests.sh +++ b/test/typecheck/run_tests.sh @@ -22,6 +22,7 @@ cat $SAILDIR/lib/prelude.sail $MIPS/mips_prelude.sail > $DIR/pass/mips_prelude.s cat $SAILDIR/lib/prelude.sail $MIPS/mips_prelude.sail $MIPS/mips_tlb.sail > $DIR/pass/mips_tlb.sail cat $SAILDIR/lib/prelude.sail $MIPS/mips_prelude.sail $MIPS/mips_tlb.sail $MIPS/mips_wrappers.sail > $DIR/pass/mips_wrappers.sail cat $SAILDIR/lib/prelude.sail $MIPS/mips_prelude.sail $MIPS/mips_tlb.sail $MIPS/mips_wrappers.sail $MIPS/mips_insts.sail $MIPS/mips_epilogue.sail > $DIR/pass/mips_insts.sail +cat $SAILDIR/lib/prelude.sail $MIPS/mips_prelude.sail $MIPS/mips_tlb_stub.sail $MIPS/mips_wrappers.sail $MIPS/mips_insts.sail $MIPS/mips_epilogue.sail > $DIR/pass/mips_notlb.sail pass=0 fail=0 @@ -99,14 +100,20 @@ finish_suite "Expecting fail" function test_lem { for i in `ls $DIR/pass/`; do - if $SAILDIR/sail -lem $DIR/$1/$i 2> /dev/null + # MIPS requires an additional library, Mips_extras_embed. + # It might be useful to allow adding options for specific test cases. + # For now, include the library for all test cases, which doesn't seem to hurt. + if $SAILDIR/sail -lem -lem_lib Mips_extras_embed $DIR/$1/$i 2> /dev/null then green "generated lem for $1/$i" "pass" + cp $MIPS/mips_extras_embed_sequential.lem $DIR/lem/ mv $SAILDIR/${i%%.*}_embed_types.lem $DIR/lem/ mv $SAILDIR/${i%%.*}_embed.lem $DIR/lem/ mv $SAILDIR/${i%%.*}_embed_sequential.lem $DIR/lem/ - if lem -lib $SAILDIR/src/lem_interp -lib $SAILDIR/src/gen_lib/ $DIR/lem/${i%%.*}_embed_types.lem $DIR/lem/${i%%.*}_embed.lem 2> /dev/null + # Test sequential embedding for now + # TODO: Add tests for the free monad + if lem -lib $SAILDIR/src/lem_interp -lib $SAILDIR/src/gen_lib/ $DIR/lem/mips_extras_embed_sequential.lem $DIR/lem/${i%%.*}_embed_types.lem $DIR/lem/${i%%.*}_embed_sequential.lem 2> /dev/null then green "typechecking lem for $1/$i" "pass" else @@ -133,6 +140,8 @@ function test_ocaml { if $SAILDIR/sail -ocaml $DIR/$1/$i 2> /dev/null then green "generated ocaml for $1/$i" "pass" + + rm $SAILDIR/${i%%.*}.ml else red "generated ocaml for $1/$i" "fail" fi |