Updates for asl_parser

Tweak colours of monomorphistion test output

10 files changed, 64 insertions, 3 deletions

diff --git a/src/ast_util.ml b/src/ast_util.ml
index 396d72a3..03031767 100644
--- a/src/ast_util.ml
+++ b/src/ast_util.ml
@@ -374,6 +374,8 @@ let app_typ id args = mk_typ (Typ_app (id, args))
 let register_typ typ = mk_typ (Typ_app (mk_id "register", [mk_typ_arg (A_typ typ)]))
 let atom_typ nexp =
   mk_typ (Typ_app (mk_id "atom", [mk_typ_arg (A_nexp (nexp_simp nexp))]))
+let implicit_typ nexp =
+  mk_typ (Typ_app (mk_id "implicit", [mk_typ_arg (A_nexp (nexp_simp nexp))]))
 let range_typ nexp1 nexp2 =
   mk_typ (Typ_app (mk_id "range", [mk_typ_arg (A_nexp (nexp_simp nexp1));
                                    mk_typ_arg (A_nexp (nexp_simp nexp2))]))
diff --git a/src/ast_util.mli b/src/ast_util.mli
index 7100cde7..4cbea3dc 100644
--- a/src/ast_util.mli
+++ b/src/ast_util.mli
@@ -124,6 +124,7 @@ val unknown_typ : typ
 val int_typ : typ
 val nat_typ : typ
 val atom_typ : nexp -> typ
+val implicit_typ : nexp -> typ
 val range_typ : nexp -> nexp -> typ
 val bit_typ : typ
 val bool_typ : typ
diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml
index 3d5bd479..f30d5135 100644
--- a/src/pretty_print_sail.ml
+++ b/src/pretty_print_sail.ml
@@ -92,6 +92,8 @@ let rec doc_nexp =
   let rec atomic_nexp (Nexp_aux (n_aux, _) as nexp) =
     match n_aux with
     | Nexp_constant c -> string (Big_int.to_string c)
+    | Nexp_app (Id_aux (DeIid op, _), [n1; n2]) ->
+       separate space [atomic_nexp n1; string op; atomic_nexp n2]
     | Nexp_app (id, nexps) -> string (string_of_nexp nexp)
     (* This segfaults??!!!!
        doc_id id ^^ (parens (separate_map (comma ^^ space) doc_nexp nexps))
diff --git a/src/type_check.ml b/src/type_check.ml
index 77e45752..f31da5f4 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -2025,6 +2025,11 @@ let rec rewrite_sizeof' env (Nexp_aux (aux, l) as nexp) =
      let exp2 = rewrite_sizeof' env nexp2 in
      mk_exp (E_app (mk_id "div", [exp1; exp2]))
 
+  | Nexp_app (id, [nexp1; nexp2]) when string_of_id id = "mod" ->
+     let exp1 = rewrite_sizeof' env nexp1 in
+     let exp2 = rewrite_sizeof' env nexp2 in
+     mk_exp (E_app (mk_id "mod", [exp1; exp2]))
+
   | Nexp_app _ | Nexp_id _ ->
      typ_error env l ("Cannot re-write sizeof(" ^ string_of_nexp nexp ^ ")")
 
diff --git a/test/mono/run_tests.sh b/test/mono/run_tests.sh
index 6a9dedd6..08926aaa 100755
--- a/test/mono/run_tests.sh
+++ b/test/mono/run_tests.sh
@@ -6,9 +6,9 @@ SAILDIR="$DIR/../.."
 TESTSDIR="$DIR"
 OUTPUTDIR="$DIR/test-output"
 
-RED='\033[0;31m'
-GREEN='\033[0;32m'
-YELLOW='\033[0;33m'
+RED='\033[0;91m'
+GREEN='\033[0;92m'
+YELLOW='\033[0;93m'
 NC='\033[0m'
 
 rm -f $DIR/tests.xml
diff --git a/test/typecheck/pass/Replicate.sail b/test/typecheck/pass/Replicate.sail
new file mode 100644
index 00000000..03954a9f
--- /dev/null
+++ b/test/typecheck/pass/Replicate.sail
@@ -0,0 +1,12 @@
+default Order dec
+
+$include <smt.sail>
+$include <prelude.sail>
+
+val Replicate : forall ('M : Int) ('N : Int), 'M >= 1.
+  (implicit('N), bits('M)) -> bits('N) effect {escape}
+
+function Replicate (N, x) = {
+    assert('N % 'M == 0);
+    replicate_bits(x, 'N / 'M)
+}
\ No newline at end of file
diff --git a/test/typecheck/pass/Replicate/v1.expect b/test/typecheck/pass/Replicate/v1.expect
new file mode 100644
index 00000000..92c6d7cd
--- /dev/null
+++ b/test/typecheck/pass/Replicate/v1.expect
@@ -0,0 +1,8 @@
+Type error:
+[Replicate/v1.sail]:11:4-30
+11 |    replicate_bits(x, 'N / 'M)
+   |    ^------------------------^
+   | Tried performing type coercion from vector(('M * div('N, 'M)), dec, bit) to vector('N, dec, bit) on replicate_bits(x, div(__id(N), bitvector_length(x)))
+   | Coercion failed because:
+   | Mismatched argument types in subtype check
+   | 
diff --git a/test/typecheck/pass/Replicate/v1.sail b/test/typecheck/pass/Replicate/v1.sail
new file mode 100644
index 00000000..69f2bb6f
--- /dev/null
+++ b/test/typecheck/pass/Replicate/v1.sail
@@ -0,0 +1,12 @@
+default Order dec
+
+$include <smt.sail>
+$include <prelude.sail>
+
+val Replicate : forall ('M : Int) ('N : Int), 'M >= 0.
+  (implicit('N), bits('M)) -> bits('N) effect {escape}
+
+function Replicate (N, x) = {
+    assert('N % 'M == 0);
+    replicate_bits(x, 'N / 'M)
+}
\ No newline at end of file
diff --git a/test/typecheck/pass/Replicate/v2.expect b/test/typecheck/pass/Replicate/v2.expect
new file mode 100644
index 00000000..0dec309f
--- /dev/null
+++ b/test/typecheck/pass/Replicate/v2.expect
@@ -0,0 +1,8 @@
+Type error:
+[Replicate/v2.sail]:10:4-30
+10 |    replicate_bits(x, 'N / 'M)
+   |    ^------------------------^
+   | Tried performing type coercion from {('ex42# : Int), true. vector(('M * 'ex42#), dec, bit)} to vector('N, dec, bit) on replicate_bits(x, div_int(__id(N), bitvector_length(x)))
+   | Coercion failed because:
+   | Mismatched argument types in subtype check
+   | 
diff --git a/test/typecheck/pass/Replicate/v2.sail b/test/typecheck/pass/Replicate/v2.sail
new file mode 100644
index 00000000..e54b0af4
--- /dev/null
+++ b/test/typecheck/pass/Replicate/v2.sail
@@ -0,0 +1,11 @@
+default Order dec
+
+$include <prelude.sail>
+
+val Replicate : forall ('M : Int) ('N : Int), 'M >= 1.
+  (implicit('N), bits('M)) -> bits('N) effect {escape}
+
+function Replicate (N, x) = {
+    assert('N % 'M == 0);
+    replicate_bits(x, 'N / 'M)
+}
\ No newline at end of file