Fixed parser to parse 2** nexp expressions properly

This introduces some shift/reduce and reduce/reduce conflicts, but I don't think these matter.

9 files changed, 76 insertions, 90 deletions

diff --git a/lib/prelude.sail b/lib/prelude.sail
index f3637945..17b49980 100644
--- a/lib/prelude.sail
+++ b/lib/prelude.sail
@@ -16,7 +16,7 @@ val forall Nat 'n, Nat 'l, Nat 'm, Nat 'o, Type 'a, 'l >= 0, 'm <= 'o, 'o <= 'l.
   (vector<'n,'l,inc,'a>, [:'m:], [:'o:]) -> vector<'m,'o - 'm,inc,'a> effect pure vector_subrange_inc
 
 val forall Nat 'n, Nat 'l, Nat 'm, Nat 'o, Type 'a, 'n >= 'm, 'm >= 'o, 'o >= 'n - 'l + 1.
-  (vector<'n,'l,dec,'a>, [:'m:], [:'o:]) -> vector<'m,'m - 'o - 1,dec,'a> effect pure vector_subrange_dec
+  (vector<'n,'l,dec,'a>, [:'m:], [:'o:]) -> vector<'m,'m - ('o - 1),dec,'a> effect pure vector_subrange_dec
 
 overload vector_subrange [vector_subrange_inc; vector_subrange_dec]
 
@@ -39,7 +39,7 @@ overload (deinfix ^^) [duplicate; duplicate_bits]
 val forall Nat 'n, Nat 'm, Nat 'o, Nat 'p, Order 'ord.
     vector<'o, 'n, 'ord, bit> -> vector<'p, 'm, 'ord, bit> effect pure extz
 
-val forall Nat 'n, Nat 'm, Nat 'o, Nat 'p, Order 'ord.
+val cast forall Nat 'n, Nat 'm, Nat 'o, Nat 'p, Order 'ord.
     vector<'o, 'n, 'ord, bit> -> vector<'p, 'm, 'ord, bit> effect pure exts
 
 overload EXTZ [extz]
diff --git a/mips_new_tc/mips_tlb.sail b/mips_new_tc/mips_tlb.sail
index 99e6eac5..f3b19d94 100644
--- a/mips_new_tc/mips_tlb.sail
+++ b/mips_new_tc/mips_tlb.sail
@@ -87,15 +87,15 @@ function (bit[64], bool) TLBTranslate2 ((bit[64]) vAddr, (MemAccessType) accessT
       (SignalExceptionTLB(TLBMod, vAddr))
     else
       let res = (bit[64]) switch evenOddBit {
-	case ([:12:]) evenOddBit -> EXTZ(pfn[23..((evenOddBit)-(12))] : vAddr[((evenOddBit)-(1)) .. 0])
-	case ([:14:]) evenOddBit -> EXTZ(pfn[23..((evenOddBit)-(12))] : vAddr[((evenOddBit)-(1)) .. 0])
-	case ([:16:]) evenOddBit -> EXTZ(pfn[23..((evenOddBit)-(12))] : vAddr[((evenOddBit)-(1)) .. 0])
-	case ([:18:]) evenOddBit -> EXTZ(pfn[23..((evenOddBit)-(12))] : vAddr[((evenOddBit)-(1)) .. 0])
-	case ([:20:]) evenOddBit -> EXTZ(pfn[23..((evenOddBit)-(12))] : vAddr[((evenOddBit)-(1)) .. 0])
-	case ([:22:]) evenOddBit -> EXTZ(pfn[23..((evenOddBit)-(12))] : vAddr[((evenOddBit)-(1)) .. 0])
-	case ([:24:]) evenOddBit -> EXTZ(pfn[23..((evenOddBit)-(12))] : vAddr[((evenOddBit)-(1)) .. 0])
-	case ([:26:]) evenOddBit -> EXTZ(pfn[23..((evenOddBit)-(12))] : vAddr[((evenOddBit)-(1)) .. 0])
-	case ([:28:]) evenOddBit -> EXTZ(pfn[23..((evenOddBit)-(12))] : vAddr[((evenOddBit)-(1)) .. 0])
+	case ([:12:]) evenOddBit -> EXTZ(pfn[23..(evenOddBit - 12)] : vAddr[(evenOddBit - 1) .. 0])
+	case ([:14:]) evenOddBit -> EXTZ(pfn[23..(evenOddBit - 12)] : vAddr[(evenOddBit - 1) .. 0])
+	case ([:16:]) evenOddBit -> EXTZ(pfn[23..(evenOddBit - 12)] : vAddr[(evenOddBit - 1) .. 0])
+	case ([:18:]) evenOddBit -> EXTZ(pfn[23..(evenOddBit - 12)] : vAddr[(evenOddBit - 1) .. 0])
+	case ([:20:]) evenOddBit -> EXTZ(pfn[23..(evenOddBit - 12)] : vAddr[(evenOddBit - 1) .. 0])
+	case ([:22:]) evenOddBit -> EXTZ(pfn[23..(evenOddBit - 12)] : vAddr[(evenOddBit - 1) .. 0])
+	case ([:24:]) evenOddBit -> EXTZ(pfn[23..(evenOddBit - 12)] : vAddr[(evenOddBit - 1) .. 0])
+	case ([:26:]) evenOddBit -> EXTZ(pfn[23..(evenOddBit - 12)] : vAddr[(evenOddBit - 1) .. 0])
+	case ([:28:]) evenOddBit -> EXTZ(pfn[23..(evenOddBit - 12)] : vAddr[(evenOddBit - 1) .. 0])
       } in
       (res, (bool) (if (accessType == StoreData) then caps else capl)) (* FIXME: get rid of explicit cast here *)
     case None ->  (SignalExceptionTLB(
diff --git a/src/parser.mly b/src/parser.mly
index 0240e368..e4b05d29 100644
--- a/src/parser.mly
+++ b/src/parser.mly
@@ -344,29 +344,7 @@ effect_typ:
   | Pure
     { tloc (ATyp_set([])) }
 
-atomic_typ:
-  | tid
-    { tloc (ATyp_id $1) }
-  | tyvar
-    { tloc (ATyp_var $1) }
-  | effect_typ
-    { $1 }
-  | Inc
-    { tloc (ATyp_inc) }
-  | Dec
-    { tloc (ATyp_dec) } 
-  | SquareBar nexp_typ BarSquare
-      { tloc (make_range_sugar $2) }
-  | SquareBar nexp_typ Colon nexp_typ BarSquare
-      { tloc (make_range_sugar_bounded $2 $4) }
-  | SquareColon nexp_typ ColonSquare
-      { tloc (make_atom_sugar $2) }
-  | Lparen typ Rparen
-    { $2 }
-
 vec_typ:
-  | atomic_typ
-      { $1 }
   | tid Lsquare nexp_typ Rsquare
       { tloc (make_vector_sugar false false (ATyp_aux ((ATyp_id $1), locn 1 1)) $3) }
   | tid Lsquare nexp_typ Colon nexp_typ Rsquare
@@ -385,70 +363,73 @@ vec_typ:
       { tloc (make_vector_sugar_bounded true false "vector" (ATyp_aux ((ATyp_var $1), locn 1 1)) $3 $5) }
 
 app_typs:
-  | nexp_typ
+  | atomic_typ
     { [$1] }
-  | nexp_typ Comma app_typs
+  | atomic_typ Comma app_typs
     { $1::$3 }
 
-app_typ:
+atomic_typ:
   | vec_typ
     { $1 }
+  | range_typ
+    { $1 }
+  | nexp_typ
+    { $1 }
+  | Inc
+    { tloc (ATyp_inc) }
+  | Dec
+    { tloc (ATyp_dec) }
   | tid Lt app_typs Gt
     { tloc (ATyp_app($1,$3)) }
   | Register Lt app_typs Gt
     { tloc (ATyp_app(Id_aux(Id "register", locn 1 1),$3)) }
 
-app_num_typ:
-  | app_typ
-    { $1 }
-  | Num
-     { tloc (ATyp_constant $1) }
+range_typ:
+  | SquareBar nexp_typ BarSquare
+      { tloc (make_range_sugar $2) }
+  | SquareBar nexp_typ Colon nexp_typ BarSquare
+      { tloc (make_range_sugar_bounded $2 $4) }
+  | SquareColon nexp_typ ColonSquare
+      { tloc (make_atom_sugar $2) }
 
-star_typ:
-  | app_num_typ
+nexp_typ:
+  | nexp_typ Plus nexp_typ2
+    { tloc (ATyp_sum ($1, $3)) }
+  | nexp_typ Minus nexp_typ2
+    { tloc (ATyp_minus ($1, $3)) }
+  | nexp_typ2
     { $1 }
-  | app_num_typ Star nexp_typ
-    { tloc (ATyp_times ($1, $3)) }
 
-exp_typ:
-   | star_typ
-     { $1 }
-   | TwoStarStar atomic_typ
-     { tloc (ATyp_exp($2)) }
-   | TwoStarStar atomic_typ Minus Num
-     { tloc (ATyp_minus (tloc (ATyp_exp $2), tloc (ATyp_constant $4))) }
-   | TwoStarStar Num
-     { tloc (ATyp_exp (tloc (ATyp_constant $2))) }
+nexp_typ2:
+  | nexp_typ2 Star nexp_typ3
+    { tloc (ATyp_times ($1, $3)) }
+  | nexp_typ3
+    { $1 }
 
-nexp_typ:
-   | exp_typ
+nexp_typ3:
+  | TwoStarStar nexp_typ4
+     { tloc (ATyp_exp $2) }
+  | nexp_typ4
      { $1 }
-   | atomic_typ Plus nexp_typ
-     { tloc (ATyp_sum($1,$3)) }
-   | Lparen atomic_typ Plus nexp_typ Rparen
-     { 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)) } 
-   | atomic_typ Minus nexp_typ
-     { tloc (ATyp_minus($1,$3)) }
-   | Lparen atomic_typ Minus nexp_typ Rparen
-     { tloc (ATyp_minus($2,$4)) } 
-   | Num Minus nexp_typ
-     { tloc (ATyp_minus((tlocl (ATyp_constant $1) 1 1),$3)) }
-   | Lparen Num Minus nexp_typ Rparen
-       { tloc (ATyp_minus((tlocl (ATyp_constant $2) 2 2),$4)) }
 
+nexp_typ4:
+  | Num
+    { tlocl (ATyp_constant $1) 1 1 }
+  | tid
+    { tloc (ATyp_id $1) }
+  | tyvar
+    { tloc (ATyp_var $1) }
+  | Lparen tup_typ Rparen
+    { $2 }
 
 tup_typ_list:
-   | app_typ Comma app_typ
+   | atomic_typ Comma atomic_typ
        { [$1;$3] }
-   | app_typ Comma tup_typ_list
+   | atomic_typ Comma tup_typ_list
        { $1::$3 }
 
 tup_typ:
-   | app_typ
+   | atomic_typ
      { $1 }
    | Lparen tup_typ_list Rparen
      { tloc (ATyp_tup $2) }
@@ -481,7 +462,6 @@ lit:
   | Bitone
     { lloc L_one }
 
-
 atomic_pat:
   | lit
     { ploc (P_lit $1) }
@@ -489,8 +469,8 @@ atomic_pat:
     { ploc P_wild }
   | Lparen pat As id Rparen
     { ploc (P_as($2,$4)) }
-  | Lparen typ Rparen atomic_pat
-    { ploc (P_typ($2,$4)) } 
+  | Lparen tup_typ Rparen atomic_pat
+    { ploc (P_typ($2,$4)) }
   | id
     { ploc (P_app($1,[])) }
   | Lcurly fpats Rcurly
@@ -573,7 +553,7 @@ atomic_exp:
     { eloc (E_lit($1)) }
   | Lparen exp Rparen
     { $2 }
-  | Lparen typ Rparen atomic_exp 
+  | Lparen tup_typ Rparen atomic_exp
     { eloc (E_cast($2,$4)) }
   | Lparen comma_exps Rparen
     { eloc (E_tuple($2)) }
@@ -660,7 +640,7 @@ right_atomic_exp:
       if $6 <> "to" && $6 <> "downto" then
        raise (Parse_error_locn ((loc ()),"Missing \"to\" or \"downto\" in foreach loop"));
       let step = eloc (E_lit(lloc (L_num 1))) in
-      let ord = 
+      let ord =
         if $6 = "to"
         then ATyp_aux(ATyp_inc,(locn 6 6))
         else ATyp_aux(ATyp_dec,(locn 6 6)) in
diff --git a/src/type_check_new.ml b/src/type_check_new.ml
index 5a0735fb..9f589cbc 100644
--- a/src/type_check_new.ml
+++ b/src/type_check_new.ml
@@ -46,7 +46,7 @@ open Util
 open Ast_util
 open Big_int
 
-let debug = ref 2
+let debug = ref 1
 let depth = ref 0
 
 let rec indent n = match n with
@@ -349,6 +349,7 @@ module Env : sig
   val get_casts : t -> id list
   val allow_casts : t -> bool
   val no_casts : t -> t
+  val enable_casts : t -> t
   val add_cast : id -> t -> t
   val lookup_id : id -> t -> lvar
   val fresh_kid : t -> kid
@@ -705,6 +706,7 @@ end = struct
   let allow_casts env = env.allow_casts
 
   let no_casts env = { env with allow_casts = false }
+  let enable_casts env = { env with allow_casts = true }
 
   let add_cast cast env =
     typ_print ("Adding cast " ^ string_of_id cast);
@@ -1851,7 +1853,7 @@ and bind_lexp env (LEXP_aux (lexp_aux, (l, ())) as lexp) typ =
          | Local (Immutable, vtyp) -> true, vtyp
          | Local (Mutable, vtyp) | Register vtyp -> false, vtyp
        in
-       let access = infer_exp env (E_aux (E_app (mk_id "vector_subrange", [E_aux (E_id v, (l, ())); exp1; exp2]), (l, ()))) in
+       let access = infer_exp (Env.enable_casts env) (E_aux (E_app (mk_id "vector_subrange", [E_aux (E_id v, (l, ())); exp1; exp2]), (l, ()))) in
        let E_aux (E_app (_, [_; inferred_exp1; inferred_exp2]), _) = access in
        match typ_of access with
        | Typ_aux (Typ_app (id, [Typ_arg_aux (Typ_arg_typ deref_typ, _)]), _) when string_of_id id = "register" ->
@@ -1871,7 +1873,7 @@ and bind_lexp env (LEXP_aux (lexp_aux, (l, ())) as lexp) typ =
          | Local (Immutable, vtyp) -> true, vtyp
          | Local (Mutable, vtyp) | Register vtyp -> false, vtyp
        in
-       let access = infer_exp env (E_aux (E_app (mk_id "vector_access", [E_aux (E_id v, (l, ())); exp]), (l, ()))) in
+       let access = infer_exp (Env.enable_casts env) (E_aux (E_app (mk_id "vector_access", [E_aux (E_id v, (l, ())); exp]), (l, ()))) in
        let E_aux (E_app (_, [_; inferred_exp]), _) = access in
        match typ_of access with
        | Typ_aux (Typ_app (id, [Typ_arg_aux (Typ_arg_typ deref_typ, _)]), _) when string_of_id id = "register" ->
diff --git a/src/type_check_new.mli b/src/type_check_new.mli
index b3749cbb..4d8b3917 100644
--- a/src/type_check_new.mli
+++ b/src/type_check_new.mli
@@ -164,6 +164,8 @@ val pat_typ_of : tannot pat -> typ
 
 val effect_of : tannot exp -> effect
 
+val propagate_exp_effect : tannot exp -> tannot exp
+
 (* Fully type-check an AST
 
 Some invariants that will hold of a fully checked AST are:
@@ -174,7 +176,7 @@ Some invariants that will hold of a fully checked AST are:
    calls E_app to vector access functions. This is different to the
    old type checker.
 
- * Every expressions type annotation (tanot) will be Some (typ, env).
+ * Every expressions type annotation (tannot) will be Some (typ, env).
 
  * Also every pattern will be annotated with the type it matches.
 
diff --git a/test/typecheck/pass/bitwise_not_gen.sail b/test/typecheck/pass/bitwise_not_gen.sail
index 8be3ea5c..6d36c566 100644
--- a/test/typecheck/pass/bitwise_not_gen.sail
+++ b/test/typecheck/pass/bitwise_not_gen.sail
@@ -2,7 +2,7 @@
 val forall Nat 'n, Nat 'm, Order 'o. vector<'n,'m,'o,bit> -> vector<'n,'m,'o,bit> effect pure bitwise_not
 
 default Order dec
-    
+
 val forall 'n. bit['n] -> bit['n] effect pure test
-    
-function forall 'n. bit['n] test ((bit['n]) x) = bitwise_not(bitwise_not(x))
\ No newline at end of file
+
+function forall 'n. bit['n] test ((bit['n]) x) = bitwise_not(bitwise_not(x))
diff --git a/test/typecheck/pass/mips400.sail b/test/typecheck/pass/mips400.sail
index 38680fcf..1e8691d9 100644
--- a/test/typecheck/pass/mips400.sail
+++ b/test/typecheck/pass/mips400.sail
@@ -13,7 +13,7 @@ val forall Nat 'n, Nat 'l, Nat 'm, Nat 'o, Type 'a, 'l >= 0, 'm <= 'o, 'o <= 'l.
   (vector<'n,'l,inc,'a>, [:'m:], [:'o:]) -> vector<'m,'o - 'm,inc,'a> effect pure vector_subrange_inc
 
 val forall Nat 'n, Nat 'l, Nat 'm, Nat 'o, Type 'a, 'n >= 'm, 'm >= 'o, 'o >= 'n - 'l + 1.
-  (vector<'n,'l,dec,'a>, [:'m:], [:'o:]) -> vector<'m,'m - 'o - 1,dec,'a> effect pure vector_subrange_dec
+  (vector<'n,'l,dec,'a>, [:'m:], [:'o:]) -> vector<'m,'m - ('o - 1),dec,'a> effect pure vector_subrange_dec
 
 overload vector_subrange [vector_subrange_inc; vector_subrange_dec]
 
@@ -491,7 +491,7 @@ register (bit[1]) UART_RVALID
 
 (* Check whether a given 64-bit vector is a properly sign extended 32-bit word *)
 val bit[64] -> bool effect pure NotWordVal
-function bool NotWordVal (word) = 
+function bool NotWordVal (word) =
     (word[31] ^^ 32) != word[63..32]
 
 (* Read numbered GP reg. (r0 is always zero) *)
diff --git a/test/typecheck/pass/set_spsr.sail b/test/typecheck/pass/set_spsr.sail
index b30343a2..7fac206c 100644
--- a/test/typecheck/pass/set_spsr.sail
+++ b/test/typecheck/pass/set_spsr.sail
@@ -4,7 +4,7 @@ val forall Nat 'n, Nat 'l, Nat 'm, Nat 'o, Type 'a, 'l >= 0, 'm <= 'o, 'o <= 'l.
   (vector<'n,'l,inc,'a>, [:'m:], [:'o:]) -> vector<'m,'o - 'm,inc,'a> effect pure vector_subrange_inc
 
 val forall Nat 'n, Nat 'l, Nat 'm, Nat 'o, Type 'a, 'n >= 'm, 'm >= 'o, 'o >= 'n - 'l + 1.
-  (vector<'n,'l,dec,'a>, [:'m:], [:'o:]) -> vector<'m,'m - 'o - 1,dec,'a> effect pure vector_subrange_dec
+  (vector<'n,'l,dec,'a>, [:'m:], [:'o:]) -> vector<'m,'m - ('o - 1),dec,'a> effect pure vector_subrange_dec
 
 overload vector_subrange [vector_subrange_inc; vector_subrange_dec]
 
diff --git a/test/typecheck/pass/simple_scattered.sail b/test/typecheck/pass/simple_scattered.sail
index 41479888..a500cd1f 100644
--- a/test/typecheck/pass/simple_scattered.sail
+++ b/test/typecheck/pass/simple_scattered.sail
@@ -10,6 +10,8 @@ scattered function forall Num 'datasize, Num 'destsize, Num 'regsize. unit execu
 
 union ast member (bit[8], bit['regsize]) test
 
+union ast member int test2
+
 function clause execute (test (x, y)) =
 {
   return ()