summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--test/mono/fnreduce.sail77
-rw-r--r--test/mono/set.sail35
-rw-r--r--test/mono/test.ml2
-rwxr-xr-xtest/mono/test.sh15
-rw-r--r--test/mono/tests8
-rw-r--r--test/mono/union-exist.sail43
-rw-r--r--test/mono/varmatch.sail21
-rw-r--r--test/mono/vector.sail26
8 files changed, 135 insertions, 92 deletions
diff --git a/test/mono/fnreduce.sail b/test/mono/fnreduce.sail
index f39fb87d..27d6b14a 100644
--- a/test/mono/fnreduce.sail
+++ b/test/mono/fnreduce.sail
@@ -1,66 +1,83 @@
-(* Test constant propagation part of monomorphisation involving
+val add_int = {ocaml: "add_int", lem: "integerAdd"} : (int, int) -> int
+overload operator + = {add_int}
+val eq_int = {ocaml: "eq_int", lem: "eq"} : (int, int) -> bool
+val eq_anything = {ocaml: "(fun (x, y) -> x = y)", lem: "eq"} : forall ('a : Type). ('a, 'a) -> bool
+overload operator == = {eq_int, eq_anything}
+
+
+/* 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 }
+enum AnEnum = One | Two | Three
-typedef EnumlikeUnion = const union { First; Second }
+union EnumlikeUnion = { First, Second }
-typedef ProperUnion = const union {
- (AnEnum) Stuff;
- (EnumlikeUnion) Nonsense;
+union ProperUnion = {
+ Stuff : AnEnum,
+ Nonsense : EnumLikeUnion
}
-function AnEnum canReduce ((AnEnum) x) = {
- switch (x) {
- case One -> Two
- case x -> x
+val canReduce : AnEnum -> AnEnum
+
+function canReduce (x) = {
+ match (x) {
+ One => Two,
+ x => x
}
}
-function nat cannotReduce ((AnEnum) x) = {
- let (nat) y = switch (x) { case One -> 1 case _ -> 5 } in
+val cannotReduce : AnEnum -> int
+
+function cannotReduce (x) = {
+ let y : int = match (x) { One => 1, _ => 5 } in
2 + y
}
-function AnEnum effect {rreg} fakeUnpure ((AnEnum) x) = {
- switch (x) {
- case One -> Two
- case x -> x
+register whatever : int
+
+val impure : AnEnum -> AnEnum effect {rreg}
+
+function impure (x) = {
+ match (x) {
+ One => Two,
+ x => let _ = whatever in x
}
}
-function EnumlikeUnion canReduceUnion ((AnEnum) x) = {
- switch (x) {
- case One -> First
- case _ -> Second
+val canReduceUnion : AnEnum -> EnumlikeUnion
+
+function canReduceUnion (x) = {
+ match (x) {
+ One => First,
+ _ => Second
}
}
-function ProperUnion canReduceUnion2 ((AnEnum) x) = {
- switch (x) {
- case One -> Nonsense(First)
- case y -> Stuff(y)
+val canReduceUnion2 : AnEnum -> ProperUnion
+
+function canReduceUnion2 (x) = {
+ match (x) {
+ One => Nonsense(First),
+ 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
+val test : AnEnum -> (AnEnum,int,AnEnum,EnumlikeUnion,ProperUnion) effect {rreg}
function test (x) = {
let a = canReduce(x) in
let b = cannotReduce(x) in
- let c = fakeUnpure(x) in
+ let c = impure(x) in
let d = canReduceUnion(x) in
let e = canReduceUnion2(x) in
(a,b,c,d,e)
}
-val unit -> bool effect pure run
+val run : unit -> bool effect {rreg}
function run () = {
test(One) == (Two,3,Two,First,Nonsense(First)) &
diff --git a/test/mono/set.sail b/test/mono/set.sail
index ecc06137..203f2219 100644
--- a/test/mono/set.sail
+++ b/test/mono/set.sail
@@ -1,26 +1,41 @@
default Order dec
-
-(* A function which is merely parametrised by a size does not need to be
- monomorphised *)
-
-val forall 'n, 'n in {32,64}. [:'n:] -> bit[64] effect pure parametric
+type bits ('n : Int) = vector('n, dec, bit)
+val operator & = "and_bool" : (bool, bool) -> bool
+val eq_vec = {ocaml: "eq_list", lem: "eq_vec"} : forall 'n. (bits('n), bits('n)) -> bool
+val eq_int = {ocaml: "eq_int", lem: "eq"} : (int, int) -> bool
+overload operator == = {eq_int, eq_vec}
+val vector_subrange = {ocaml: "subrange", lem: "subrange_vec_dec"} : forall ('n : Int) ('m : Int) ('o : Int), 'o <= 'm <= 'n.
+ (bits('n), atom('m), atom('o)) -> bits('m - ('o - 1))
+val mult_int = {ocaml: "mult", lem: "integerMult"} : (int, int) -> int
+overload operator * = {mult_range, mult_int, mult_real}
+val "extz_vec" : forall 'n 'm. (atom('m),vector('n, dec, bit)) -> vector('m, dec, bit) effect pure
+val extz : forall 'n 'm. vector('n, dec, bit) -> vector('m, dec, bit) effect pure
+function extz(v) = extz_vec(sizeof('m),v)
+val "exts_vec" : forall 'n 'm. (atom('m),vector('n, dec, bit)) -> vector('m, dec, bit) effect pure
+val exts : forall 'n 'm. vector('n, dec, bit) -> vector('m, dec, bit) effect pure
+function exts(v) = exts_vec(sizeof('m),v)
+
+/* A function which is merely parametrised by a size does not need to be
+ monomorphised */
+
+val parametric : forall 'n, 'n in {32,64}. atom('n) -> bits(64)
function parametric(n) = {
- let (bit['n]) x = exts(0x80000000) in
+ let x : bits('n) = exts(0x80000000) in
extz(x)
}
-(* But if we do a calculation on the size then we'll need to case split *)
+/* But if we do a calculation on the size then we'll need to case split */
-val forall 'n, 'n in {16,32}. [:'n:] -> bit[64] effect pure depends
+val depends : forall 'n, 'n in {16,32}. atom('n) -> bits(64)
function depends(n) = {
let 'm = 2 * n in
- let (bit['m]) x = exts(0x80000000) in
+ let x : bits('m) = exts(0x80000000) in
extz(x)
}
-val unit -> bool effect pure run
+val run : unit -> bool
function run () =
parametric(32) == 0x0000000080000000 &
diff --git a/test/mono/test.ml b/test/mono/test.ml
index f99abfb8..efa1de54 100644
--- a/test/mono/test.ml
+++ b/test/mono/test.ml
@@ -1 +1 @@
-if Testout_embed_sequential.run() then print_endline "OK" else print_endline "Failed";;
+if Testout.run() then print_endline "OK" else print_endline "Failed";;
diff --git a/test/mono/test.sh b/test/mono/test.sh
index 2a5aa80b..7af2e93e 100755
--- a/test/mono/test.sh
+++ b/test/mono/test.sh
@@ -24,20 +24,13 @@ set +e
while read -u 3 TEST ARGS; do
if [ -z "$TESTONLY" -o "$TEST" = "$TESTONLY" ]; then
-# echo "$TEST ocaml"
-# rm -f -- "$OUTDIR"/*
-# "$SAILDIR/sail" -ocaml "$SAILDIR/lib/prelude.sail" "$SAILDIR/lib/prelude_wrappers.sail" "$DIR/$TEST" -o "$OUTDIR/testout" $ARGS
-# cp -- "$SAILDIR"/src/gen_lib/sail_values.ml .
-# cp -- "$DIR"/test.ml .
-# 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 testout.ml test.ml -o test
-# ./test
-
+
echo "$TEST lem - ocaml" | tee -a -- "$LOG"
rm -f -- "$OUTDIR"/*
- "$SAILDIR/sail" -lem -lem_sequential -lem_mwords "$SAILDIR/lib/prelude.sail" "$SAILDIR/lib/prelude_wrappers.sail" "$DIR/$TEST".sail -o "$OUTDIR/testout" $ARGS $@ &>> "$LOG" && \
- "$LEMDIR/bin/lem" -ocaml -lib "$SAILDIR/src/lem_interp" "$SAILDIR/src/gen_lib/sail_values.lem" "$SAILDIR/src/gen_lib/sail_operators_mwords.lem" "$SAILDIR/src/gen_lib/state.lem" testout_embed_types_sequential.lem testout_embed_sequential.lem -outdir "$OUTDIR" &>> "$LOG" && \
+ "$SAILDIR/sail" -lem -lem_mwords "$DIR/$TEST".sail -o "$OUTDIR/testout" $ARGS $@ &>> "$LOG" && \
+ "$LEMDIR/bin/lem" -ocaml -lib "$SAILDIR/src/lem_interp" "$SAILDIR/src/gen_lib/sail_values.lem" "$SAILDIR/src/gen_lib/sail_operators.lem" "$SAILDIR/src/gen_lib/sail_operators_mwords.lem" "$SAILDIR/src/lem_interp/sail_instr_kinds.lem" "$SAILDIR/src/gen_lib/prompt.lem" "$SAILDIR/src/gen_lib/state_monad.lem" "$SAILDIR/src/gen_lib/state.lem" "$SAILDIR/src/gen_lib/prompt_monad.lem" testout_types.lem testout.lem -outdir "$OUTDIR" &>> "$LOG" && \
cp -- "$DIR"/test.ml "$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 sail_operators_mwords.ml state.ml testout_embed_types_sequential.ml testout_embed_sequential.ml test.ml -o test &>> "$LOG" && \
+ ocamlfind ocamlc -linkpkg -package zarith -package lem sail_values.ml sail_operators.ml sail_operators_mwords.ml sail_instr_kinds.ml prompt_monad.ml prompt.ml state_monad.ml state.ml testout_types.ml testout.ml test.ml -o test &>> "$LOG" && \
./test |& tee -a -- "$LOG" || \
(echo "Failed:"; echo; tail -- "$LOG"; echo; echo)
fi
diff --git a/test/mono/tests b/test/mono/tests
index 27e161cf..8847f03e 100644
--- a/test/mono/tests
+++ b/test/mono/tests
@@ -1,7 +1,7 @@
-fnreduce -mono-split fnreduce.sail:43:x
-varmatch -mono-split varmatch.sail:7:x
-vector -mono-split vector.sail:7:sel
-union-exist -mono-split union-exist.sail:9:v
+fnreduce -mono_split fnreduce.sail:43:x
+varmatch -mono_split varmatch.sail:7:x
+vector -mono_split vector.sail:7:sel
+union-exist -mono_split union-exist.sail:9:v
fnreduce -auto_mono
varmatch -auto_mono
vector -auto_mono
diff --git a/test/mono/union-exist.sail b/test/mono/union-exist.sail
index 74ab429a..9ec3ee33 100644
--- a/test/mono/union-exist.sail
+++ b/test/mono/union-exist.sail
@@ -1,29 +1,34 @@
default Order dec
+type bits ('n : Int) = vector('n, dec, bit)
+val operator & = "and_bool" : (bool, bool) -> bool
+val eq_vec = {ocaml: "eq_list", lem: "eq_vec"} : forall 'n. (bits('n), bits('n)) -> bool
+val eq_int = {ocaml: "eq_int", lem: "eq"} : (int, int) -> bool
+overload operator == = {eq_int, eq_vec}
+val vector_subrange = {ocaml: "subrange", lem: "subrange_vec_dec"} : forall ('n : Int) ('m : Int) ('o : Int), 'o <= 'm <= 'n.
+ (bits('n), atom('m), atom('o)) -> bits('m - ('o - 1))
-typedef myunion = const union {
- (exist 'n, 'n in {8,16}. ([:'n:],bit['n])) MyConstr;
+
+union myunion = {
+ MyConstr : {'n, 'n in {8,16}. (atom('n),bits('n))}
}
-val bit[2] -> myunion effect pure make
+val make : bits(2) -> myunion
function make(v) =
- (* Can't mention these below without running into exp/nexp parsing conflict! *)
+ /* Can't mention these below without running into exp/nexp parsing conflict! */
let eight = 8 in let sixteen = 16 in
- switch v {
- case 0b00 -> MyConstr( ( eight, 0x12) )
- case 0b01 -> MyConstr( (sixteen,0x1234) )
- case 0b10 -> MyConstr( ( eight, 0x56) )
- case 0b11 -> MyConstr( (sixteen,0x5678) )
- }
-
-val myunion -> bit[32] effect pure use
-
-function use(MyConstr('n)) = {
- switch n {
- case (n,v) -> extz(v)
- }
-}
-val unit -> bool effect pure run
+ let r : {'n, 'n in {8,16}. (atom('n),bits('n))} = match v {
+ 0b00 => ( eight, 0x12),
+ 0b01 => (sixteen,0x1234),
+ 0b10 => ( eight, 0x56),
+ 0b11 => (sixteen,0x5678)
+ } in MyConstr(r)
+
+val use : myunion -> bits(32)
+
+function use(MyConstr((n,v) as (atom('n),bits('n)))) = extz(v)
+
+val run : unit -> bool
function run () = {
use(make(0b00)) == 0x00000012 &
diff --git a/test/mono/varmatch.sail b/test/mono/varmatch.sail
index 7d2b9b73..279c16be 100644
--- a/test/mono/varmatch.sail
+++ b/test/mono/varmatch.sail
@@ -1,16 +1,21 @@
-(* Check that when we case split on a variable that the constant propagation
- handles the default case correctly. *)
+val operator & = "and_bool" : (bool, bool) -> bool
+val operator == = {ocaml: "(fun (x, y) -> x = y)", lem: "eq"} : forall ('a : Type). ('a, 'a) -> bool
-typedef AnEnum = enumerate { One; Two; Three }
+/* Check that when we case split on a variable that the constant propagation
+ handles the default case correctly. */
-function AnEnum foo((AnEnum) x) = {
- switch (x) {
- case One -> Two
- case y -> y
+enum AnEnum = One | Two | Three
+
+val foo : AnEnum -> AnEnum
+
+function foo(x) = {
+ match (x) {
+ One => Two,
+ y => y
}
}
-val unit -> bool effect pure run
+val run : unit -> bool
function run () = {
foo(One) == Two &
diff --git a/test/mono/vector.sail b/test/mono/vector.sail
index 03f36da5..5740075b 100644
--- a/test/mono/vector.sail
+++ b/test/mono/vector.sail
@@ -1,18 +1,26 @@
-(* Check case splitting on a vector *)
-
default Order dec
+type bits ('n : Int) = vector('n, dec, bit)
+val operator & = "and_bool" : (bool, bool) -> bool
+val eq_vec = {ocaml: "eq_list", lem: "eq_vec"} : forall 'n. (bits('n), bits('n)) -> bool
+val eq_int = {ocaml: "eq_int", lem: "eq"} : (int, int) -> bool
+overload operator == = {eq_int, eq_vec}
+val vector_subrange = {ocaml: "subrange", lem: "subrange_vec_dec"} : forall ('n : Int) ('m : Int) ('o : Int), 'o <= 'm <= 'n.
+ (bits('n), atom('m), atom('o)) -> bits('m - ('o - 1))
+
+
+/* Check case splitting on a vector */
-val bit[32] -> nat effect pure test
+val test : bits(32) -> nat
-function nat test((bit[2]) sel : (bit[30]) _) = {
- switch (sel) {
- case 0b00 -> 5
- case 0b10 -> 1
- case _ -> 0
+function test((sel : bits(2)) @ (_ : bits(30))) = {
+ match (sel) {
+ 0b00 => 5,
+ 0b10 => 1,
+ _ => 0
}
}
-val unit -> bool effect pure run
+val run : unit -> bool
function run () = {
test(0x0f353533) == 5 &
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-12 01:53:06 +0000