diff options
| author | Alasdair Armstrong | 2017-06-28 17:58:40 +0100 |
|---|---|---|
| committer | Alasdair Armstrong | 2017-06-28 17:58:40 +0100 |
| commit | 32a621d568081cc7f60102d35d84bece9bbd01c5 (patch) | |
| tree | ee641aabcaf42d1cc10dd2dc1838deb8bc21d3a6 /test | |
| parent | 058be7385881ce5a530f76fa48c867d04dca42cf (diff) | |
Improvements to implicit type casting
Added a new feature for implicit casts - now allowable implicit casts
can be specified by the user via a valspec such as
val cast forall Type 'a, Type 'b. 'a -> 'b effect pure cast_anything
with a new AST constructor to represent this as VS_cast_spec. This
constructor is removed and replaced with the standard val spec by the
old typechecker for backwards compatability, so it's only used by the
new typechecker, and won't appear in the ast once it reaches the
backends.
Also added Num as a synonym for the Nat kind in the parser, via the
confusingly named NatNum token (Num by itself was already taken for a
numeric constant).
Diffstat (limited to 'test')
| -rw-r--r-- | test/typecheck/pass/mips_CP0Cause_BD_assign1.sail | 6 | ||||
| -rw-r--r-- | test/typecheck/pass/mips_CauseReg1.sail | 1 | ||||
| -rw-r--r-- | test/typecheck/pass/mips_CauseReg2.sail | 1 | ||||
| -rw-r--r-- | test/typecheck/pass/mips_CauseReg3.sail | 1 |
4 files changed, 7 insertions, 2 deletions
diff --git a/test/typecheck/pass/mips_CP0Cause_BD_assign1.sail b/test/typecheck/pass/mips_CP0Cause_BD_assign1.sail index a3036e1f..68a6ee95 100644 --- a/test/typecheck/pass/mips_CP0Cause_BD_assign1.sail +++ b/test/typecheck/pass/mips_CP0Cause_BD_assign1.sail @@ -1,5 +1,7 @@ -val forall Nat 'n, Order 'ord. [:1:] -> vector<'n,1,'ord,bit> effect pure cast_one_bv -val 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_one_bv +val cast forall Nat 'n, Order 'ord. [:0:] -> vector<'n,1,'ord,bit> effect pure cast_zero_bv + +val cast forall Type 'a, Type 'b. 'a -> 'b effect pure cast_anything default Order dec diff --git a/test/typecheck/pass/mips_CauseReg1.sail b/test/typecheck/pass/mips_CauseReg1.sail index e05d0af8..b9503efa 100644 --- a/test/typecheck/pass/mips_CauseReg1.sail +++ b/test/typecheck/pass/mips_CauseReg1.sail @@ -1,3 +1,4 @@ +default Order dec typedef CauseReg = register bits [ 31 : 0 ] { 31 : BD; (* branch delay *) diff --git a/test/typecheck/pass/mips_CauseReg2.sail b/test/typecheck/pass/mips_CauseReg2.sail index f62824f1..7600c9f1 100644 --- a/test/typecheck/pass/mips_CauseReg2.sail +++ b/test/typecheck/pass/mips_CauseReg2.sail @@ -1,3 +1,4 @@ +default Order dec typedef CauseReg = register bits [ 31 : 1 ] { 31 : BD; (* branch delay *) diff --git a/test/typecheck/pass/mips_CauseReg3.sail b/test/typecheck/pass/mips_CauseReg3.sail index 24b07fcd..48acd4f5 100644 --- a/test/typecheck/pass/mips_CauseReg3.sail +++ b/test/typecheck/pass/mips_CauseReg3.sail @@ -1,3 +1,4 @@ +default Order dec typedef CauseReg = register bits [ 31 : 0 ] { 31 : BD; (* branch delay *) |