summaryrefslogtreecommitdiff
path: root/src/test
diff options
context:
space:
mode:
Diffstat (limited to 'src/test')
-rw-r--r--src/test/run_tests.ml1
-rw-r--r--src/test/test1.sail5
2 files changed, 5 insertions, 1 deletions
diff --git a/src/test/run_tests.ml b/src/test/run_tests.ml
index f614306b..d1a90f38 100644
--- a/src/test/run_tests.ml
+++ b/src/test/run_tests.ml
@@ -6,6 +6,7 @@ let tests = [
"test3", Test3.defs;
"pattern", Pattern.defs;
"vectors", Vectors.defs;
+ "regbits", Regbits.defs;
(*"power", Power.defs;*)
] ;;
diff --git a/src/test/test1.sail b/src/test/test1.sail
index 3d69018d..0050a257 100644
--- a/src/test/test1.sail
+++ b/src/test/test1.sail
@@ -14,6 +14,9 @@ val forall Nat 'a, Nat 'b. bit['a:'b] sliced
let bit v = bitzero
let ( bit [ 32 ] ) v1 = 0b101
+val forall Type 'a. 'a -> 'a effect pure identity
+function forall Type 'a. 'a identity i = i
+
function unit ignore(x) = ()
(* scattered function definition and union definition *)
@@ -32,7 +35,7 @@ function clause f ( C (a) ) = C(a)
end ast
end f
-function unit a (bit) b = if b then () else ()
+function unit a (bit) b = if identity(b) then (identity()) else ()
function bit sw s = switch s { case 0 -> bitzero }