Added support for set constraints

Also added some additional tests in test/typecheck

11 files changed, 99 insertions, 11 deletions

diff --git a/src/ast.ml b/src/ast.ml
index 6710c749..df3098b5 100644
--- a/src/ast.ml
+++ b/src/ast.ml
@@ -172,6 +172,8 @@ n_constraint_aux =  (* constraint over kind $_$ *)
  | NC_bounded_ge of nexp * nexp
  | NC_bounded_le of nexp * nexp
  | NC_nat_set_bounded of kid * (int) list
+ (* We need this for the new typechecker when as nexp is substituted for an id *)
+ | NC_set_subst of nexp * int list
 
 
 type 
diff --git a/src/type_check_new.ml b/src/type_check_new.ml
index 5f997409..f33a7db1 100644
--- a/src/type_check_new.ml
+++ b/src/type_check_new.ml
@@ -210,6 +210,8 @@ let string_of_n_constraint = function
   | NC_aux (NC_fixed (n1, n2), _) -> string_of_nexp n1 ^ " = " ^ string_of_nexp n2
   | NC_aux (NC_bounded_ge (n1, n2), _) -> string_of_nexp n1 ^ " >= " ^ string_of_nexp n2
   | NC_aux (NC_bounded_le (n1, n2), _) -> string_of_nexp n1 ^ " <= " ^ string_of_nexp n2
+  | NC_aux (NC_set_subst (nexp, ns), _) ->
+     string_of_nexp nexp ^ " IN {" ^ string_of_list ", " string_of_int ns ^ "}"
   | NC_aux (NC_nat_set_bounded (kid, ns), _) ->
      string_of_kid kid ^ " IN {" ^ string_of_list ", " string_of_int ns ^ "}"
 
@@ -340,9 +342,10 @@ and nc_subst_nexp_aux l sv subst = function
   | NC_bounded_ge (n1, n2) -> NC_bounded_ge (nexp_subst sv subst n1, nexp_subst sv subst n2)
   | NC_bounded_le (n1, n2) -> NC_bounded_le (nexp_subst sv subst n1, nexp_subst sv subst n2)
   | NC_nat_set_bounded (kid, ints) as set_nc ->
-      if compare kid sv = 0
-      then typ_error l ("Cannot substitute " ^ string_of_kid sv ^ " into set constraint " ^ string_of_n_constraint (NC_aux (set_nc, l)))
-      else set_nc
+     if Kid.compare kid sv = 0
+     then NC_set_subst (Nexp_aux (subst, Parse_ast.Unknown), ints)
+     else set_nc
+  | NC_set_subst (nexp, ints) -> NC_set_subst (nexp_subst sv subst nexp, ints) 
 
 let rec typ_subst_nexp sv subst (Typ_aux (typ, l)) = Typ_aux (typ_subst_nexp_aux sv subst typ, l)
 and typ_subst_nexp_aux sv subst = function
@@ -784,7 +787,8 @@ end = struct
     | NC_bounded_ge (n1, n2) -> wf_nexp env n1; wf_nexp env n2
     | NC_bounded_le (n1, n2) -> wf_nexp env n1; wf_nexp env n2
     | NC_nat_set_bounded (kid, ints) -> () (* MAYBE: We could demand that ints are all unique here *)
-
+    | NC_set_subst (nexp, ints) -> wf_nexp env nexp
+                                          
   let get_constraints env = env.constraints
 
   let add_constraint (NC_aux (_, l) as constr) env =
@@ -985,16 +989,17 @@ let rec nexp_constraint var_of (Nexp_aux (nexp, l)) =
   | Nexp_exp nexp -> Constraint.pow2 (nexp_constraint var_of nexp)
   | Nexp_neg nexp -> Constraint.sub (Constraint.constant (big_int_of_int 0)) (nexp_constraint var_of nexp)
 
-let nc_constraint var_of (NC_aux (nc, _)) =
+let rec nc_constraint var_of (NC_aux (nc, l)) =
   match nc with
   | NC_fixed (nexp1, nexp2) -> Constraint.eq (nexp_constraint var_of nexp1) (nexp_constraint var_of nexp2)
   | NC_bounded_ge (nexp1, nexp2) -> Constraint.gteq (nexp_constraint var_of nexp1) (nexp_constraint var_of nexp2)
   | NC_bounded_le (nexp1, nexp2) -> Constraint.lteq (nexp_constraint var_of nexp1) (nexp_constraint var_of nexp2)
-  | NC_nat_set_bounded (_, []) -> Constraint.literal false
-  | NC_nat_set_bounded (kid, (int :: ints)) ->
+  | NC_nat_set_bounded (kid, ints) -> nc_constraint var_of (NC_aux (NC_set_subst (nvar kid, ints), l))
+  | NC_set_subst (_, []) -> Constraint.literal false
+  | NC_set_subst (nexp, (int :: ints)) ->
      List.fold_left Constraint.disj
-                    (Constraint.eq (Constraint.variable (var_of kid)) (Constraint.constant (big_int_of_int int)))
-                    (List.map (fun i -> Constraint.eq (Constraint.variable (var_of kid)) (Constraint.constant (big_int_of_int i))) ints)
+                    (Constraint.eq (nexp_constraint var_of nexp) (Constraint.constant (big_int_of_int int)))
+                    (List.map (fun i -> Constraint.eq (nexp_constraint var_of nexp) (Constraint.constant (big_int_of_int i))) ints)
 
 let rec nc_constraints var_of ncs =
   match ncs with
diff --git a/test/typecheck/fail/bv_simple_index_no_cast.sail b/test/typecheck/fail/bv_simple_index_no_cast.sail
new file mode 100644
index 00000000..74f46ab7
--- /dev/null
+++ b/test/typecheck/fail/bv_simple_index_no_cast.sail
@@ -0,0 +1,9 @@
+val forall Nat 'n, Nat 'l, Type 'a, 'l >= 0. (vector<'n,'l,dec,'a>, [|'n - 'l + 1:'n|]) -> 'a effect pure vector_access_dec
+val forall Nat 'n, Nat 'l, Type 'a, 'l >= 0. (vector<'n,'l,inc,'a>, [|'n:'n + 'l - 1|]) -> 'a effect pure vector_access_inc
+
+overload vector_access [vector_access_inc; vector_access_dec]
+
+function bool bv ((bit[64]) x) =
+{
+  x[32]
+}
diff --git a/test/typecheck/fail/nat_set.sail b/test/typecheck/fail/nat_set.sail
new file mode 100644
index 00000000..036183c5
--- /dev/null
+++ b/test/typecheck/fail/nat_set.sail
@@ -0,0 +1,9 @@
+
+function forall Nat 'n, 'n IN {1,2,3}. bool test (([:'n:]) x) =
+{
+  true
+}
+
+let x = test(1)
+let y = test(3)
+let z = test(4)
\ No newline at end of file
diff --git a/test/typecheck/fail/word_width_bytes_mips.sail b/test/typecheck/fail/word_width_bytes_mips.sail
new file mode 100644
index 00000000..91f3e787
--- /dev/null
+++ b/test/typecheck/fail/word_width_bytes_mips.sail
@@ -0,0 +1,11 @@
+typedef WordType = enumerate {B; H; W; D}
+
+(* This fails because it's not true for all combinations of 'r and WordType *)
+(* Needs existential types, i.e. return type should be exists Nat 'r, 'r in {1,2,4,8}. [:'r:] *)
+function forall Nat 'r, 'r IN {1,2,4,8}. wordWidthBytes((WordType) w) =
+  switch(w) {
+    case B -> 1
+    case H -> 2
+    case W -> 4
+    case D -> 8
+  }
diff --git a/test/typecheck/pass/bv_simple_index.sail b/test/typecheck/pass/bv_simple_index.sail
new file mode 100644
index 00000000..72e1b094
--- /dev/null
+++ b/test/typecheck/pass/bv_simple_index.sail
@@ -0,0 +1,11 @@
+val forall Nat 'n, Nat 'l, Type 'a, 'l >= 0. (vector<'n,'l,dec,'a>, [|'n - 'l + 1:'n|]) -> 'a effect pure vector_access_dec
+val forall Nat 'n, Nat 'l, Type 'a, 'l >= 0. (vector<'n,'l,inc,'a>, [|'n:'n + 'l - 1|]) -> 'a effect pure vector_access_inc
+
+overload vector_access [vector_access_inc; vector_access_dec]
+
+val cast bit -> bool effect pure cast_bit_bool
+
+function bool bv ((bit[64]) x) =
+{
+  x[32]
+}
diff --git a/test/typecheck/pass/bv_simple_index_bit.sail b/test/typecheck/pass/bv_simple_index_bit.sail
new file mode 100644
index 00000000..2ba5b928
--- /dev/null
+++ b/test/typecheck/pass/bv_simple_index_bit.sail
@@ -0,0 +1,9 @@
+val forall Nat 'n, Nat 'l, Type 'a, 'l >= 0. (vector<'n,'l,dec,'a>, [|'n - 'l + 1:'n|]) -> 'a effect pure vector_access_dec
+val forall Nat 'n, Nat 'l, Type 'a, 'l >= 0. (vector<'n,'l,inc,'a>, [|'n:'n + 'l - 1|]) -> 'a effect pure vector_access_inc
+
+overload vector_access [vector_access_inc; vector_access_dec]
+
+function bit bv ((bit[64]) x) =
+{
+  x[32]
+}
diff --git a/test/typecheck/pass/nat_set.sail b/test/typecheck/pass/nat_set.sail
new file mode 100644
index 00000000..46338353
--- /dev/null
+++ b/test/typecheck/pass/nat_set.sail
@@ -0,0 +1,8 @@
+
+function forall Nat 'n, 'n IN {1,2,3}. bool test (([:'n:]) x) =
+{
+  true
+}
+
+let x = test(1)
+let y = test(3)
\ No newline at end of file
diff --git a/test/typecheck/pass/set_mark.sail b/test/typecheck/pass/set_mark.sail
new file mode 100644
index 00000000..59710c46
--- /dev/null
+++ b/test/typecheck/pass/set_mark.sail
@@ -0,0 +1,6 @@
+
+val cast forall Num 'n, Num 'm, Order 'ord. [:0:] -> vector<'n,'m,'ord,bit> effect pure cast_zero_bv
+
+function forall Num 'N, 'N IN {32}. bit['N] Foo32( (bit['N]) x) = x
+
+let x = Foo32( (bit[32]) 0)
diff --git a/test/typecheck/pass/set_mark2.sail b/test/typecheck/pass/set_mark2.sail
new file mode 100644
index 00000000..c1433058
--- /dev/null
+++ b/test/typecheck/pass/set_mark2.sail
@@ -0,0 +1,5 @@
+val cast forall Num 'n, Num 'm, Order 'ord. [:0:] -> vector<'n,'m,'ord,bit> effect pure cast_zero_bv
+
+function forall Nat 'N, 'N IN {32, 64}. bit['N] Foo32( (bit['N]) x) = x
+
+let x = Foo32( (bit[64]) 0)
diff --git a/test/typecheck/run_tests.sh b/test/typecheck/run_tests.sh
index 7fca4770..f33f21ac 100755
--- a/test/typecheck/run_tests.sh
+++ b/test/typecheck/run_tests.sh
@@ -11,6 +11,9 @@ NC='\033[0m'
 mkdir -p $DIR/rtpass
 mkdir -p $DIR/rtfail
 
+pass=0
+fail=0
+
 for i in `ls $DIR/pass/`;
 do
     printf "testing $i expecting pass: "
@@ -18,11 +21,15 @@ do
     then
 	if $DIR/../../sail -dno_cast -just_check $DIR/rtpass/$i 2> /dev/null;
 	then
+	    (( pass += 2))
 	    printf "${GREEN}pass${NC}\n"
 	else
-	    printf "${YELLOW}pass${NC}\n"
+	    (( fail += 1 ))
+	    (( pass += 1 ))
+	    printf "${YELLOW}pass but failed re-check${NC}\n"
 	fi
     else
+	(( fail += 2 ))
 	printf "${RED}fail${NC}\n"
     fi
 done
@@ -32,13 +39,19 @@ do
     printf "testing $i expecting fail: "
     if $DIR/../../sail -ddump_tc_ast -just_check $DIR/fail/$i 2> /dev/null 1> $DIR/rtfail/$i;
     then
+	(( fail += 2 ))
 	printf "${RED}pass${NC}\n"
     else
 	if $DIR/../../sail -dno_cast -just_check $DIR/rtfail/$i 2> /dev/null;
 	then
-	    printf "${YELLOW}fail${NC}\n"
+	    (( fail += 1 ))
+	    (( pass += 1 ))
+	    printf "${YELLOW}fail but passed re-check${NC}\n"
 	else
+	    (( pass += 2 ))
 	    printf "${GREEN}fail${NC}\n"
 	fi
     fi
 done
+
+printf "Passed ${pass} out of $(( pass + fail ))\n"