summaryrefslogtreecommitdiff
path: root/src/test/test4.sail
diff options
context:
space:
mode:
authorAlasdair Armstrong2018-07-30 19:16:34 +0100
committerAlasdair Armstrong2018-08-01 16:42:33 +0100
commit1479ae359fd3afebf9c3dfb6e58a77254e8140ea (patch)
treeffcfd96409467a5c41009f68afe1f65a2c7a3d49 /src/test/test4.sail
parent0b70a9d7464d6c30534d2f511cb8c9879c76b1e5 (diff)
Remove old test directory in src/test
Diffstat (limited to 'src/test/test4.sail')
-rw-r--r--src/test/test4.sail67
1 files changed, 0 insertions, 67 deletions
diff --git a/src/test/test4.sail b/src/test/test4.sail
deleted file mode 100644
index fa0133ca..00000000
--- a/src/test/test4.sail
+++ /dev/null
@@ -1,67 +0,0 @@
-(* hack to display log messages. Syntax: LOG(0) := "log message"; *)
-val extern forall Type 'a . (nat, 'a) -> unit effect { wmem } LOG
-
-register (bit[1]) GPR0
-register (bit[1]) GPR1
-
-let (vector <0, 2, inc, (register<bit[1] >)>) GPR = [ GPR0, GPR1 ]
-
-(* if we access GPR with a bit or a nat - doing the conversion in the
- caller, works as expected *)
-function unit good ((bit) RA ) =
-{
- LOG(0) := "good";
- (nat) x := GPR[RA];
-}
-
-function unit good2 ((nat) RA ) =
-{
- LOG(0) := "good2";
- (nat) x := GPR[RA];
-}
-
-(* but here, the first to_num_inc(RA) somehow inhibits the cast,
- yielding to_num_inc(GPR0) instead of to_num_inc(0b0) *)
-function unit bad ((bit[1]) RA ) =
-{
- LOG(0) := "oldbad";
- (nat) x := GPR[RA];
-}
-
-(* and now, another bug - when DCR contains registers of bits instead of bit[0] *)
-
-register (bit) DCR0
-register (bit) DCR1
-
-let (vector <0, 2, inc, (register<bit >)>) DCR = [ DCR0, DCR1 ]
-
-(* also fails only when passing RA as a vector, nat and bit work fine as
- above;
- error message is different though, and very disturbing:
- "error: No matching patterns in case", corresponding to the DCR[RA]
- expression *)
-function unit bad2 ((bit[1]) RA ) =
-{
- LOG(0) := "oldbad2";
- (nat) x := DCR[RA];
-}
-
-
-function unit main () = {
- LOG(0) := "init";
-
- GPR[0] := 0b0;
- GPR[1] := 0b1;
-
- DCR[0] := bitzero;
- DCR[1] := bitone;
-
- good(bitzero);
- good2(0);
-
- (* a first bug *)
- bad(0b0);
-
- (* another bug :-) comment out first one to see it *)
- bad2(0b0);
-}