Check simple constraints (i.e. ones using only constants).

Changes syntax of tuple type from * to , so that nexps of the form 8 * 'n can be supported in the parser, which was apparently not true before.

7 files changed, 53 insertions, 24 deletions

diff --git a/src/lexer.mll b/src/lexer.mll
index 410e24a3..988ddb7c 100644
--- a/src/lexer.mll
+++ b/src/lexer.mll
@@ -193,6 +193,7 @@ rule token = parse
   | "<<<"				{ (LtLtLt(r"<<<")) }
   | "<+"				{ (LtPlus(r"<+")) }
   | "**"				{ (StarStar(r"**")) }
+  | "[|"                                { SquareBar }
   | "~^"				{ (TildeCarrot(r"~^")) }
 
   | ">=_s"				{ (GtEqUnderS(r">=_s")) }
diff --git a/src/parser.mly b/src/parser.mly
index ada8365a..fb4c322e 100644
--- a/src/parser.mly
+++ b/src/parser.mly
@@ -66,6 +66,7 @@ let bkloc k = BK_aux(k,loc ())
 let kloc k = K_aux(k,loc ())
 let kiloc ki = KOpt_aux(ki,loc ())
 let tloc t = ATyp_aux(t,loc ())
+let tlocl t l1 l2 = ATyp_aux(t,locn l1 l2)
 let lloc l = L_aux(l,loc ())
 let ploc p = P_aux(p,loc ())
 let fploc p = FP_aux(p,loc ())
@@ -360,10 +361,16 @@ app_typ:
   | Register Lt app_typs Gt
     { tloc (ATyp_app(Id_aux(Id "register", locn 1 1),$3)) }
 
-star_typ_list:
+app_num_typ:
   | app_typ
+    { $1 }
+  | Num
+     { tloc (ATyp_constant $1) }
+
+star_typ_list:
+  | app_num_typ
     { [$1] }
-  | app_typ Star star_typ_list
+  | app_num_typ Star star_typ_list
     { $1::$3 }
 
 star_typ:
@@ -376,9 +383,7 @@ star_typ:
 exp_typ:
    | star_typ
      { $1 }
-   | Num
-     { tloc (ATyp_constant $1) }
-   | TwoStarStar typ
+   | TwoStarStar nexp_typ
      { tloc (ATyp_exp($2)) }
 
 nexp_typ:
@@ -387,12 +392,28 @@ nexp_typ:
    | atomic_typ Plus nexp_typ
      { tloc (ATyp_sum($1,$3)) }
    | Lparen atomic_typ Plus nexp_typ Rparen
-     { tloc (ATyp_sum($2,$4)) }
+     { tloc (ATyp_sum($2,$4)) } 
+   | Num Plus nexp_typ
+     { tloc (ATyp_sum((tlocl (ATyp_constant $1) 1 1),$3)) }
+   | Lparen Num Plus nexp_typ Rparen
+     { tloc (ATyp_sum((tlocl (ATyp_constant $2) 2 2),$4)) } 
+
+tup_typ_list:
+   | app_typ Comma app_typ
+       { [$1;$3] }
+   | app_typ Comma tup_typ_list
+       { $1::$3 }
+
+tup_typ:
+   | app_typ
+     { $1 }
+   | Lparen tup_typ_list Rparen
+     { tloc (ATyp_tup $2) }
 
 typ:
-  | star_typ
+  | tup_typ
     { $1 }
-  | star_typ MinusGt typ Effect effect_typ
+  | tup_typ MinusGt typ Effect effect_typ
     { tloc (ATyp_fn($1,$3,$5)) }
 
 lit:
diff --git a/src/test/regbits.sail b/src/test/regbits.sail
index 0a41280d..ed2a95e0 100644
--- a/src/test/regbits.sail
+++ b/src/test/regbits.sail
@@ -9,7 +9,7 @@ register (xer) XER
 register (bit) query
 
 function (bit[64]) main _ = {
-  XER := 0b010101010101010101010101010101010101010101010101010101010101001;
+  XER := 0b0101010101010101010101010101010101010101010101010101010101010010;
   f := XER;
   (bit[7]) foo := XER[57..63];
   query := XER.SO;
diff --git a/src/test/test1.sail b/src/test/test1.sail
index 0050a257..64722089 100644
--- a/src/test/test1.sail
+++ b/src/test/test1.sail
@@ -2,8 +2,8 @@ default Nat 'i
 default Order 'o
 default bool b
 default forall 'a. list<'a> b
-val forall 'a, 'b . ('a * 'b) -> 'b effect pure snd
-val forall Type 'i, 'b. ('i * 'b) -> 'i effect pure fst
+val forall 'a, 'b . ('a, 'b) -> 'b effect pure snd
+val forall Type 'i, 'b. ('i, 'b) -> 'i effect pure fst
 typedef int_list [name = "il"] = list<nat>
 typedef reco = const struct forall 'i, 'a, 'b. { 'a['i] v; 'b w; }
 typedef maybe = const union forall 'a. { Nne; 'a Sme; }
@@ -23,10 +23,10 @@ function unit ignore(x) = ()
 scattered typedef ast = const union
 scattered function ast f
 
-union ast member  bit * bit * bit A
+union ast member  (bit, bit, bit) A
 function clause f (  A (a,b,c) ) = C(a)
 
-union ast member  bit * bit B
+union ast member  (bit, bit) B
 function clause f (  B (a,b) ) = C(a)
 
 union ast member  bit C
diff --git a/src/test/test3.sail b/src/test/test3.sail
index 778d323a..78d60513 100644
--- a/src/test/test3.sail
+++ b/src/test/test3.sail
@@ -6,7 +6,7 @@ register (bit[8]) dummy_reg2
    memory-writing functions are figured out syntactically. *)
 val extern nat -> nat effect { wmem , rmem }  MEM
 val extern nat -> nat effect { wmem , rmem }  MEM_GPU
-val extern ( nat * nat ) -> (bit[8]) effect { wmem , rmem }  MEM_SIZE
+val extern forall Nat 'n . ( nat, [|'n|] ) -> (bit['n * 8]) effect { wmem , rmem }  MEM_SIZE
 val extern nat -> (bit[8]) effect { wmem , rmem }  MEM_WORD
 
 (* XXX types are wrong *)
@@ -18,8 +18,8 @@ val extern forall Type 'a . nat -> 'a effect pure to_vec_dec = "to_vec_dec"
 function unit ignore(x) = ()
 
 (* extern functions *)
-val extern ( nat * nat ) -> nat effect pure add = "add"
-val extern ( nat * nat ) -> nat effect pure (deinfix + ) = "add"   (* infix plus *)
+val extern ( nat, nat ) -> nat effect pure add = "add"
+val extern ( nat, nat ) -> nat effect pure (deinfix + ) = "add"   (* infix plus *)
 
 function nat (deinfix * ) ( (nat) x, (nat) y ) = 42
 
diff --git a/src/test/vectors.sail b/src/test/vectors.sail
index f1af224b..de610a39 100644
--- a/src/test/vectors.sail
+++ b/src/test/vectors.sail
@@ -1,6 +1,6 @@
-let (bit[32]) v = 0b101
+let (bit[3]) v = 0b101
 let (bit[4]) v2 = [0,1,0,0]
-register (bit[32]) i
+register (bit[4]) i
 
 let (bit[10]) v3 = 0b0101010111
 register (bit[10]) slice_check
diff --git a/src/type_internal.ml b/src/type_internal.ml
index af4bd49d..f958803a 100644
--- a/src/type_internal.ml
+++ b/src/type_internal.ml
@@ -232,9 +232,10 @@ let rec eval_nexp n =
       let n1' = eval_nexp n1 in
       (match n1'.nexp with
 	| Nconst i ->
-	  let rec two_pow = function
-	    | 0 -> 1;
-	    | n -> 2* (two_pow n-1) in
+	  let rec two_pow n =
+	    match n with 
+	    | 0 -> 1
+	    | n -> (two_pow (n-1)) in
 	  {nexp = Nconst(two_pow i)}
 	| _ -> {nexp = N2n n1'})
     | Nvar _ | Nuvar _ -> n
@@ -959,11 +960,13 @@ let rec type_coerce_internal l d_env t1 cs1 e t2 cs2 =
 and type_coerce l d_env t1 e t2 = type_coerce_internal l d_env t1 [] e t2 []
 
 let rec simple_constraint_check cs = 
-  let _ = Printf.printf "simple_constraint_check\n" in
+(*  let _ = Printf.printf "simple_constraint_check\n" in *)
   match cs with 
   | [] -> []
   | Eq(l,n1,n2)::cs -> 
+(*    let _ = Printf.printf "eq check, about to eval_nexp of %s, %s\n" (n_to_string n1) (n_to_string n2) in *)
     let n1',n2' = eval_nexp n1,eval_nexp n2 in
+(*    let _ = Printf.printf "finished evaled to %s, %s\n" (n_to_string n1') (n_to_string n2') in*)
     (match n1'.nexp,n2.nexp with
       | Nconst i1, Nconst i2 -> 
 	if i1==i2 
@@ -972,7 +975,9 @@ let rec simple_constraint_check cs =
 			 ^ string_of_int i1 ^ " to equal " ^ string_of_int i2)
       | _,_ -> Eq(l,n1',n2')::(simple_constraint_check cs))
   | GtEq(l,n1,n2)::cs -> 
+(*    let _ = Printf.printf ">= check, about to eval_nexp of %s, %s\n" (n_to_string n1) (n_to_string n2) in*)
     let n1',n2' = eval_nexp n1,eval_nexp n2 in
+(*    let _ = Printf.printf "finished evaled to %s, %s\n" (n_to_string n1') (n_to_string n2') in*)
     (match n1'.nexp,n2.nexp with
       | Nconst i1, Nconst i2 -> 
 	if i1>=i2 
@@ -981,7 +986,9 @@ let rec simple_constraint_check cs =
 			 ^ string_of_int i1 ^ " to be greater than or equal to " ^ string_of_int i2)
       | _,_ -> GtEq(l,n1',n2')::(simple_constraint_check cs))
   | LtEq(l,n1,n2)::cs -> 
+(*    let _ = Printf.printf "<= check, about to eval_nexp of %s, %s\n" (n_to_string n1) (n_to_string n2) in *)
     let n1',n2' = eval_nexp n1,eval_nexp n2 in
+(*    let _ = Printf.printf "finished evaled to %s, %s\n" (n_to_string n1') (n_to_string n2') in*)
     (match n1'.nexp,n2.nexp with
       | Nconst i1, Nconst i2 -> 
 	if i1<=i2 
@@ -992,8 +999,8 @@ let rec simple_constraint_check cs =
   | x::cs -> x::(simple_constraint_check cs)
     
 let resolve_constraints cs = 
-  (*let complex_constraints = simple_constraint_check cs in
-  complex_constraints*) cs
+  let complex_constraints = simple_constraint_check cs in
+  complex_constraints (*cs*)
 
 
 let check_tannot l annot constraints efs =