Correct bug in parsing and handling a['a:'b] types

7 files changed, 38 insertions, 28 deletions

diff --git a/src/initial_check.ml b/src/initial_check.ml
index ed4a0208..83a2c5ab 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -137,6 +137,7 @@ and to_ast_nexp (k_env : kind Envmap.t) (n: Parse_ast.atyp) : Ast.nexp =
       let n2 = to_ast_nexp k_env t2 in
       Nexp_aux(Nexp_sum(n1,n2),l)
     | Parse_ast.ATyp_exp(t1) -> Nexp_aux(Nexp_exp(to_ast_nexp k_env t1),l)
+    | Parse_ast.ATyp_neg(t1) -> Nexp_aux(Nexp_neg(to_ast_nexp k_env t1),l)
     | Parse_ast.ATyp_tup(typs) ->
       let rec times_loop (typs : Parse_ast.atyp list) (one_ok : bool) : nexp =
         (match typs,one_ok with
diff --git a/src/lexer.mll b/src/lexer.mll
index e8ee92db..410e24a3 100644
--- a/src/lexer.mll
+++ b/src/lexer.mll
@@ -71,14 +71,14 @@ let kw_table =
      ("default",		 (fun _ -> Default));
      ("deinfix",                 (fun _ -> Deinfix));
      ("effect",                  (fun _ -> Effect));
-     ("Effect",                 (fun _ -> EFFECT));
+     ("Effect",                  (fun _ -> EFFECT));
      ("end",                     (fun _ -> End));
      ("enumerate",		 (fun _ -> Enumerate));
      ("else",                    (fun _ -> Else));
      ("extern",                  (fun _ -> Extern));
      ("false",                   (fun _ -> False));
      ("forall",                  (fun _ -> Forall));
-     ("foreach",                  (fun _ -> Foreach));
+     ("foreach",                 (fun _ -> Foreach));
      ("function",                (fun x -> Function_));
      ("if",                      (fun x -> If_));
      ("in",			 (fun x -> In));
@@ -171,6 +171,7 @@ rule token = parse
   | "^^"				{ (CarrotCarrot(r"^^")) }
   | "::" as i                           { (ColonColon(r i)) }
   | ":="                                { ColonEq }
+  | ":>"                                { ColonGt }
   | ".."				{ DotDot }
   | "=/="				{ (EqDivEq(r"=/=")) }
   | "=="				{ (EqEq(r"==")) }
@@ -184,6 +185,7 @@ rule token = parse
   | "#>>"				{ (HashGtGt(r"#>>")) }
   | "#<<"				{ (HashLtLt(r"#<<")) }
   | "->"                                { MinusGt }
+  | "<:"                                { LtColon }
   | "<="				{ (LtEq(r"<=")) }
   | "<=+"				{ (LtEqPlus(r"<=+")) }
   | "<>"				{ (LtGt(r"<>")) }
diff --git a/src/parser.mly b/src/parser.mly
index 856d3266..d29f0d16 100644
--- a/src/parser.mly
+++ b/src/parser.mly
@@ -96,27 +96,22 @@ let make_enum_sugar_bounded typ1 typ2 =
 let make_enum_sugar typ1 =
   make_enum_sugar_bounded typ1 (ATyp_aux(ATyp_constant(0), Unknown))
 
-let make_vector_sugar_bounded typ typ1 typ2 = 
-  ATyp_app(Id_aux(Id("vector"),Unknown),
-           [typ1;typ2;ATyp_aux(ATyp_inc,Unknown);typ])
+let make_r bot top =
+  match bot,top with
+    | ATyp_aux(ATyp_constant b,_),ATyp_aux(ATyp_constant t,l) ->
+      ATyp_aux(ATyp_constant ((t-b)+1),l)
+    | bot,(ATyp_aux(_,l) as top) ->
+      ATyp_aux((ATyp_sum ((ATyp_aux (ATyp_sum (top, ATyp_aux(ATyp_constant 1,Unknown)), Unknown)),
+			  (ATyp_aux ((ATyp_neg bot),Unknown)))), l)				   
+
+let make_vector_sugar_bounded is_inc typ typ1 typ2 = 
+  let rise,ord = 
+    if is_inc 
+    then make_r typ1 typ2,ATyp_inc 
+    else make_r typ2 typ1,ATyp_dec in
+  ATyp_app(Id_aux(Id("vector"),Unknown),[typ1;rise;ATyp_aux(ord,Unknown);typ])
 let make_vector_sugar typ typ1 =
-  make_vector_sugar_bounded typ (ATyp_aux(ATyp_constant(0),Unknown)) typ1
-    
-
-let space = " "
-let star = "*"
-
-(*let mk_pre_x_l sk1 (sk2,id) sk3 l =
-  if (sk2 = None || sk2 = Some []) && (sk3 = None || sk3 = Some []) then
-    PreX_l(sk1,(None,id),None,l)
-  else if (sk2 = Some [Ws space] &&
-           sk3 = Some [Ws space] &&
-           (Ulib.Text.left id 1 = star ||
-            Ulib.Text.right id 1 = star)) then
-    PreX_l(sk1,(None,id),None,l)
-  else
-    raise (Parse_error_locn(l, "illegal whitespace in parenthesised infix name"))*)
-
+  make_vector_sugar_bounded true typ (ATyp_aux(ATyp_constant(0),Unknown)) typ1
 
 %}
 
@@ -135,7 +130,7 @@ let star = "*"
 
 %token Bar Comma Dot Eof Minus Semi Under
 %token Lcurly Rcurly Lparen Rparen Lsquare Rsquare
-%token BarBar BarSquare BarBarSquare ColonEq DotDot ColonGt MinusGt LtBar SquareBar SquareBarBar
+%token BarBar BarSquare BarBarSquare ColonEq DotDot ColonGt MinusGt LtBar LtColon SquareBar SquareBarBar
 
 /*Terminals with content*/
 
@@ -327,11 +322,19 @@ vec_typ:
   | tid Lsquare nexp_typ Rsquare
       { tloc (make_vector_sugar (ATyp_aux ((ATyp_id $1), locn 1 1)) $3) }
   | tid Lsquare nexp_typ Colon nexp_typ Rsquare
-      { tloc (make_vector_sugar_bounded (ATyp_aux ((ATyp_id $1), locn 1 1)) $3 $5) }
+      { tloc (make_vector_sugar_bounded true (ATyp_aux ((ATyp_id $1), locn 1 1)) $3 $5) }
+  | tid Lsquare nexp_typ LtColon nexp_typ Rsquare
+      { tloc (make_vector_sugar_bounded true (ATyp_aux ((ATyp_id $1), locn 1 1)) $3 $5) }
+  | tid Lsquare nexp_typ ColonGt nexp_typ Rsquare
+      { tloc (make_vector_sugar_bounded false (ATyp_aux ((ATyp_id $1), locn 1 1)) $3 $5) }
   | tyvar Lsquare nexp_typ Rsquare
       { tloc (make_vector_sugar (ATyp_aux ((ATyp_var $1), locn 1 1)) $3) }
   | tyvar Lsquare nexp_typ Colon nexp_typ Rsquare
-      { tloc (make_vector_sugar_bounded (ATyp_aux ((ATyp_var $1), locn 1 1)) $3 $5) }
+      { tloc (make_vector_sugar_bounded true (ATyp_aux ((ATyp_var $1), locn 1 1)) $3 $5) }
+  | tyvar Lsquare nexp_typ LtColon nexp_typ Rsquare
+      { tloc (make_vector_sugar_bounded true (ATyp_aux ((ATyp_var $1), locn 1 1)) $3 $5) }
+  | tyvar Lsquare nexp_typ ColonGt nexp_typ Rsquare
+      { tloc (make_vector_sugar_bounded false (ATyp_aux ((ATyp_var $1), locn 1 1)) $3 $5) }
 
 app_typs:
   | nexp_typ
diff --git a/src/pre_lexer.mll b/src/pre_lexer.mll
index 5f55cc72..b8869812 100644
--- a/src/pre_lexer.mll
+++ b/src/pre_lexer.mll
@@ -133,8 +133,8 @@ rule token = parse
 
   | "2**" | "&"	| "@" | "|" | "^" | ":"  | "," | "."  | "/" | "=" | "!" | ">" | "-" | "<" |
     "+" | ";" | "*" | "~" | "_" | "{" | "}" | "(" | ")" | "[" | "]" | "&&" | "||" | "|]" | "||]" |
-    "^^" | "::" | ":=" | ".." | "=/=" | "==" | "!=" | "!!" | ">=" | ">=+" | ">>" | ">>>" | ">+" |
-    "#>>" | "#<<" | "->" | "<="	| "<=+"	| "<>" | "<<" | "<<<" | "<+" | "**" | "~^" | ">=_s" |
+    "^^" | "::" | ":>" |  ":=" | ".." | "=/=" | "==" | "!=" | "!!" | ">=" | ">=+" | ">>" | ">>>" | ">+" |
+    "#>>" | "#<<" | "->" | "<:" | "<="	| "<=+"	| "<>" | "<<" | "<<<" | "<+" | "**" | "~^" | ">=_s" |
     ">=_si" | ">=_u" | ">=_ui" | ">>_u" | ">_s" | ">_si" | ">_u" | ">_ui" | "<=_s" | "<=_si" |
     "<=_u" | "<=_ui" | "<_s" | "<_si" | "<_u" | "<_ui" | "**_s" | "**_si" | "*_u" | "*_ui"| "2^"				{ Other }
 
diff --git a/src/pretty_print.ml b/src/pretty_print.ml
index 4190ad9b..57a8ebab 100644
--- a/src/pretty_print.ml
+++ b/src/pretty_print.ml
@@ -90,6 +90,7 @@ and pp_format_nexp (Nexp_aux(n,_)) =
   | Nexp_sum(n1,n2) -> "(" ^ (pp_format_nexp n1) ^ " + " ^ (pp_format_nexp n2) ^ ")"
   | Nexp_times(n1,n2) -> "(" ^  (pp_format_nexp n1) ^ " * " ^ (pp_format_nexp n2) ^ ")"
   | Nexp_exp(n1) -> "2** (" ^ (pp_format_nexp n1) ^ ")"
+  | Nexp_neg(n1) -> "(* - *)" ^ (pp_format_nexp n1)
 and pp_format_ord (Ord_aux(o,_)) = 
   match o with
   | Ord_var(var) -> pp_format_var var
@@ -413,7 +414,8 @@ and pp_format_nexp_lem (Nexp_aux(n,l)) =
     | Nexp_constant(i) -> "(Nexp_constant " ^ string_of_int i ^ ")"
     | Nexp_sum(n1,n2) -> "(Nexp_sum " ^ (pp_format_nexp_lem n1) ^ " " ^ (pp_format_nexp_lem n2) ^ ")"
     | Nexp_times(n1,n2) -> "(Nexp_times " ^  (pp_format_nexp_lem n1) ^ " " ^ (pp_format_nexp_lem n2) ^ ")"
-    | Nexp_exp(n1) -> "(Nexp_exp " ^ (pp_format_nexp_lem n1) ^ ")") ^ " " ^
+    | Nexp_exp(n1) -> "(Nexp_exp " ^ (pp_format_nexp_lem n1) ^ ")"
+    | Nexp_neg(n1) -> "(Nexp_neg " ^ (pp_format_nexp_lem n1) ^ ")") ^ " " ^
     (pp_format_l_lem l) ^ ")"
 and pp_format_ord_lem (Ord_aux(o,l)) = 
   "(Ord_aux " ^ 
diff --git a/src/test/test1.sail b/src/test/test1.sail
index 34210f97..3d69018d 100644
--- a/src/test/test1.sail
+++ b/src/test/test1.sail
@@ -10,6 +10,7 @@ typedef maybe = const union forall 'a. { Nne; 'a Sme; }
 typedef colors = enumerate { red; green; blue }
 typedef creg = register bits [5:10] { 5 : h ; 6..7 : j}
 let bool e = true
+val forall Nat 'a, Nat 'b. bit['a:'b] sliced
 let bit v = bitzero
 let ( bit [ 32 ] ) v1 = 0b101
 
diff --git a/src/type_check.ml b/src/type_check.ml
index e5211d72..6cf4ca9b 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -78,6 +78,7 @@ and anexp_to_nexp ((Nexp_aux(n,l)) : Ast.nexp) : nexp =
     | Nexp_times(n1,n2) -> {nexp=Nmult(anexp_to_nexp n1,anexp_to_nexp n2)}
     | Nexp_sum(n1,n2) -> {nexp=Nadd(anexp_to_nexp n1,anexp_to_nexp n2)}
     | Nexp_exp n -> {nexp=N2n(anexp_to_nexp n)}
+    | Nexp_neg n -> {nexp=Nneg(anexp_to_nexp n)}
 and aeffect_to_effect ((Effect_aux(e,l)) : Ast.effect) : effect = 
   match e with
     | Effect_var (Kid_aux((Var i),l')) -> {effect = Evar i}