Merge remote-tracking branch 'origin/sail2' into asl_flow2

3 files changed, 67 insertions, 0 deletions

diff --git a/test/coq/pass/avoid_lit.sail b/test/coq/pass/avoid_lit.sail
new file mode 100644
index 00000000..7af9ad82
--- /dev/null
+++ b/test/coq/pass/avoid_lit.sail
@@ -0,0 +1,13 @@
+default Order dec
+
+$include <prelude.sail>
+
+// In the calls to sail_zeros below the Coq version needs to end up with
+// 'n for the argument, rather than the literal 8 or 16.  We currently do
+// this by replacing the literal with an underscore and letting Coq figure
+// it out.
+
+val test : forall 'n, 'n in {8,16}. atom('n) -> bits('n)
+
+function test(8) = sail_zeros(8)
+and test(16) = sail_zeros(16)
diff --git a/test/coq/pass/fncasts.sail b/test/coq/pass/fncasts.sail
new file mode 100644
index 00000000..a18c9ecc
--- /dev/null
+++ b/test/coq/pass/fncasts.sail
@@ -0,0 +1,21 @@
+default Order dec
+
+$include <prelude.sail>
+
+// Check that the Coq backend correctly inserts autocasts.
+
+// Here we need a cast after the call to concat to change 'n + 'm to 'm + 'n
+val cast_result : forall 'n 'm, 'n >= 0 & 'm >= 0. (bits('n), bits('m)) -> bits('m + 'n)
+function cast_result (v,w) = v @ w
+
+/* FIXME: ought to cast result as if there were a type annotation
+val no_call : forall 'n 'm, 'n > 0 & 'm > 0. bits('n + 'm) -> bits('m + 'n)
+function no_call(v) = v
+*/
+
+val div_ex : forall 'n 'm, 'n > 0 & 'm > 0. (atom('n), bits('n * 'm)) -> bits('m)
+
+// Here we need a cast before the call to div_ex to change 'n to 1*'n
+val cast_arg : forall 'n, 'n > 0. bits('n) -> bits('n)
+function cast_arg(v) = div_ex(1,v)
+
diff --git a/test/coq/pass/rangepair.sail b/test/coq/pass/rangepair.sail
new file mode 100644
index 00000000..ce08ee4a
--- /dev/null
+++ b/test/coq/pass/rangepair.sail
@@ -0,0 +1,33 @@
+/* Check that tuples of values that should be accompanied by a Coq proof are
+   handled properly. */
+
+$include <prelude.sail>
+
+/* Monadic version */
+
+val getpair_eff : unit -> (range(1,2),range(3,4)) effect {escape}
+
+function getpair_eff () = {
+  assert(true);
+  return (2,3)
+}
+
+val test_eff : unit -> range (4,6) effect {escape}
+
+function test_eff () =
+  let (x,y) = getpair_eff() in
+  x + y
+
+/* Pure version */
+
+val getpair : unit -> (range(1,2),range(3,4))
+
+function getpair () = {
+  return (2,3)
+}
+
+val test : unit -> range (4,6)
+
+function test () =
+  let (x,y) = getpair() in
+  x + y