Very basic start to monomorphisation testing

3 files changed, 91 insertions, 0 deletions

diff --git a/test/mono/fnreduce.sail b/test/mono/fnreduce.sail
new file mode 100644
index 00000000..f39fb87d
--- /dev/null
+++ b/test/mono/fnreduce.sail
@@ -0,0 +1,69 @@
+(* Test constant propagation part of monomorphisation involving
+   functions.  We should reduce a function application when the
+   arguments are suitable values, the function is pure and the result
+   is a value.
+ *)
+
+typedef AnEnum = enumerate { One; Two; Three }
+
+typedef EnumlikeUnion = const union { First; Second }
+
+typedef ProperUnion = const union {
+  (AnEnum) Stuff;
+  (EnumlikeUnion) Nonsense;
+}
+
+function AnEnum canReduce ((AnEnum) x) = {
+  switch (x) {
+  case One -> Two
+  case x -> x
+  }
+}
+
+function nat cannotReduce ((AnEnum) x) = {
+  let (nat) y = switch (x) { case One -> 1 case _ -> 5 } in
+  2 + y
+}
+
+function AnEnum effect {rreg} fakeUnpure ((AnEnum) x) = {
+  switch (x) {
+  case One -> Two
+  case x -> x
+  }
+}
+
+function EnumlikeUnion canReduceUnion ((AnEnum) x) = {
+  switch (x) {
+  case One -> First
+  case _ -> Second
+  }
+}
+
+function ProperUnion canReduceUnion2 ((AnEnum) x) = {
+  switch (x) {
+  case One -> Nonsense(First)
+  case y -> Stuff(y)
+  }
+}
+
+(* FIXME LATER: once effect handling is in place we should get an error
+   because this isn't pure *)
+
+val AnEnum -> (AnEnum,nat,AnEnum,EnumlikeUnion,ProperUnion) effect pure test
+
+function test (x) = {
+  let a = canReduce(x) in
+  let b = cannotReduce(x) in
+  let c = fakeUnpure(x) in
+  let d = canReduceUnion(x) in
+  let e = canReduceUnion2(x) in
+  (a,b,c,d,e)
+}
+
+val unit -> bool effect pure run
+
+function run () = {
+  test(One) == (Two,3,Two,First,Nonsense(First)) &
+  test(Two) == (Two,7,Two,Second,Stuff(Two)) &
+  test(Three) == (Three,7,Three,Second,Stuff(Three))
+}
diff --git a/test/mono/test.ml b/test/mono/test.ml
new file mode 100644
index 00000000..cd6c6041
--- /dev/null
+++ b/test/mono/test.ml
@@ -0,0 +1 @@
+if Fnreduce_embed_sequential.run() then print_endline "OK" else print_endline "Failed";;
diff --git a/test/mono/test.sh b/test/mono/test.sh
new file mode 100755
index 00000000..7b1eeb64
--- /dev/null
+++ b/test/mono/test.sh
@@ -0,0 +1,21 @@
+#!/bin/bash
+
+set -ex
+
+DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" && pwd )"
+SAILDIR="$DIR/../.."
+LEMDIR="$DIR/../../../lem"
+OUTDIR="$DIR/fnreduce-ml"
+ZARITH="$LEMDIR/ocaml-lib/dependencies/zarith"
+
+"$SAILDIR/sail" -lem "$SAILDIR/lib/prelude.sail" -mono-split fnreduce.sail:43:x "$DIR/fnreduce.sail" -o "$DIR/fnreduce"
+if [ -d "$OUTDIR" ]; then
+  rm -- "$OUTDIR"/*
+else
+  mkdir -- "$OUTDIR"
+fi
+"$LEMDIR/bin/lem" -ocaml -lib "$SAILDIR/src/lem_interp" "$SAILDIR/src/gen_lib/sail_values.lem" "$SAILDIR/src/gen_lib/state.lem" "$DIR/fnreduce_embed_types.lem" "$DIR/fnreduce_embed_sequential.lem" -outdir "$OUTDIR"
+cp -- "$DIR"/test.ml "$OUTDIR"
+cd "$OUTDIR"
+ocamlc -I "$ZARITH" "$ZARITH/zarith.cma" -dllpath "$ZARITH" -I "$LEMDIR/ocaml-lib" "$LEMDIR/ocaml-lib/extract.cma" -I "$SAILDIR/src/_build/lem_interp" "$SAILDIR/src/_build/lem_interp/extract.cma" sail_values.ml state.ml fnreduce_embed_types.ml fnreduce_embed_sequential.ml test.ml -o test
+./test