Fixed a bug in vector concatenation l-expressions

The code for these is now rather ugly though... it needs to be cleaned up at some point

Also various improvements to new menhir parser

5 files changed, 81 insertions, 34 deletions

diff --git a/editors/sail2-mode.el b/editors/sail2-mode.el
index 4e536ef0..e780695d 100644
--- a/editors/sail2-mode.el
+++ b/editors/sail2-mode.el
@@ -8,7 +8,7 @@
     "else" "match" "in" "return" "register" "forall" "op" "effect"
     "overload" "cast" "sizeof" "constraint" "default" "assert"
     "pure" "infixl" "infixr" "infix" "scattered" "end" "try" "catch"
-    "throw" "clause"))
+    "throw" "clause" "as"))
 
 (defconst sail2-kinds
   '("Int" "Type" "Order" "inc" "dec"
@@ -16,12 +16,16 @@
     "exmem" "undef" "unspec" "nondet" "escape"))
 
 (defconst sail2-types
-  '("vector" "int" "atom" "range" "unit" "bit" "real" "list" "bool" "string"))
+  '("vector" "int" "nat" "atom" "range" "unit" "bit" "real" "list" "bool" "string"))
+
+(defconst sail2-special
+  '("_prove"))
 
 (defconst sail2-font-lock-keywords
   `((,(regexp-opt sail2-keywords 'symbols) . font-lock-keyword-face)
     (,(regexp-opt sail2-kinds 'symbols) . font-lock-builtin-face)
     (,(regexp-opt sail2-types 'symbols) . font-lock-type-face)
+    (,(regexp-opt sail2-special 'symbols) . font-lock-preprocessor-face)
     ("\'[a-zA-z_]+" . font-lock-variable-name-face)
     ("\\_<\\([0-9]+\\|0b[0-9]+\\|0x[0-9a-fA-F]+\\|true\\|false\\|bitone\\|bitzero\\)\\_>\\|()" . font-lock-constant-face)))
 
diff --git a/src/lexer2.mll b/src/lexer2.mll
index a1717d62..1ab5b98b 100644
--- a/src/lexer2.mll
+++ b/src/lexer2.mll
@@ -100,7 +100,6 @@ let kw_table =
      ("by",                      (fun _ -> By));
      ("match",			 (fun _ -> Match));
      ("clause",                  (fun _ -> Clause));
-     ("const",			 (fun _ -> Const));
      ("dec",                     (fun _ -> Dec));
      ("def",                     (fun _ -> Def));
      ("op",                      (fun _ -> Op));
@@ -145,13 +144,6 @@ let kw_table =
      ("with",                    (fun x -> With));
      ("val",                     (fun x -> Val));
 
-     ("div",			 (fun x -> Div_));
-     ("mod",			 (fun x -> Mod));
-     ("mod_s",                   (fun x -> ModUnderS));
-     ("quot",			 (fun x -> Quot));
-     ("quot_s",                  (fun x -> QuotUnderS));
-     ("rem",			 (fun x -> Rem));
-
      ("barr",                    (fun x -> Barr));
      ("depend",                  (fun x -> Depend));
      ("rreg",                    (fun x -> Rreg));
diff --git a/src/parser2.mly b/src/parser2.mly
index 09fe4b41..16e93a59 100644
--- a/src/parser2.mly
+++ b/src/parser2.mly
@@ -124,7 +124,7 @@ let rec desugar_rchain chain s e =
 
 /*Terminals with no content*/
 
-%token And As Assert Bitzero Bitone Bits By Match Clause Const Dec Def Default Effect EFFECT End Op
+%token And As Assert Bitzero Bitone Bits By Match Clause Dec Def Default Effect EFFECT End Op
 %token Enum Else Extern False Forall Exist Foreach Overload Function_ If_ In IN Inc Let_ Member Int Order Cast
 %token Pure Rec Register Return Scattered Sizeof Struct Then True TwoCaret Type TYPE Typedef
 %token Undefined Union With Val Constraint Throw Try Catch
@@ -133,11 +133,8 @@ let rec desugar_rchain chain s e =
 %nonassoc Then
 %nonassoc Else
 
-%token Div_ Mod ModUnderS Quot Rem QuotUnderS
-
 %token Bar Comma Dot Eof Minus Semi Under DotDot
 %token Lcurly Rcurly Lparen Rparen Lsquare Rsquare LcurlyBar RcurlyBar
-%token BarBar BarSquare BarBarSquare ColonEq ColonGt ColonSquare
 %token MinusGt LtBar LtColon SquareBar SquareBarBar
 
 /*Terminals with content*/
@@ -148,7 +145,7 @@ let rec desugar_rchain chain s e =
 
 %token <string> Amp At Caret Div Eq Excl Gt Lt Plus Star EqGt Unit
 %token <string> Colon ExclEq
-%token <string> GtEq GtEqPlus GtGt GtGtGt GtPlus HashGtGt HashLtLt
+%token <string> GtEq GtEqPlus GtGt GtGtGt GtPlus
 %token <string> LtEq LtEqPlus LtGt LtLt LtLtLt LtPlus StarStar
 
 %token <string> Op0 Op1 Op2 Op3 Op4 Op5 Op6 Op7 Op8 Op9
@@ -590,8 +587,8 @@ pat:
     { $1 }
   | atomic_pat As id
     { mk_pat (P_as ($1, $3)) $startpos $endpos }
-  | Lparen pat Comma pat_list Rparen
-    { mk_pat (P_tup ($2 :: $4)) $startpos $endpos }
+  | atomic_pat As kid
+    { mk_pat (P_var ($1, $3)) $startpos $endpos }
 
 pat_list:
   | pat
@@ -614,6 +611,8 @@ atomic_pat:
     { mk_pat (P_typ ($3, $1)) $startpos $endpos }
   | Lparen pat Rparen
     { $2 }
+  | Lparen pat Comma pat_list Rparen
+    { mk_pat (P_tup ($2 :: $4)) $startpos $endpos }
 
 lit:
   | True
@@ -658,9 +657,6 @@ exp:
     { mk_exp (E_case ($2, $4)) $startpos $endpos }
   | Try exp Catch Lcurly case_list Rcurly
     { mk_exp (E_try ($2, $5)) $startpos $endpos }
-  | Lparen exp0 Comma exp_list Rparen
-    { mk_exp (E_tuple ($2 :: $4)) $startpos $endpos }
-
 /* The following implements all nine levels of user-defined precedence for
 operators in expressions, with both left, right and non-associative operators */
 
@@ -858,6 +854,8 @@ atomic_exp:
     { mk_exp (E_sizeof $3) $startpos $endpos }
   | Constraint Lparen nc Rparen
     { mk_exp (E_constraint $3) $startpos $endpos }
+  | Assert Lparen exp Rparen
+    { mk_exp (E_assert ($3, mk_lit_exp (L_string "") $startpos($4) $endpos($4))) $startpos $endpos }
   | Assert Lparen exp Comma exp Rparen
     { mk_exp (E_assert ($3, $5)) $startpos $endpos }
   | atomic_exp Lsquare exp Rsquare
@@ -872,6 +870,8 @@ atomic_exp:
     { mk_exp (E_vector_update_subrange ($2, $4, $6, $8)) $startpos $endpos }
   | Lparen exp Rparen
     { $2 }
+  | Lparen exp Comma exp_list Rparen
+    { mk_exp (E_tuple ($2 :: $4)) $startpos $endpos }
 
 exp_list:
   | exp
diff --git a/src/pretty_print_sail2.ml b/src/pretty_print_sail2.ml
index dfbeaaf8..d9bc0c7c 100644
--- a/src/pretty_print_sail2.ml
+++ b/src/pretty_print_sail2.ml
@@ -91,6 +91,9 @@ let rec doc_pat (P_aux (p_aux, _)) =
   | P_app (id, pats) -> doc_id id ^^ lparen ^^ separate_map (comma ^^ space) doc_pat pats ^^ rparen
   | P_typ (typ, pat) -> separate space [doc_pat pat; colon; doc_typ typ]
   | P_lit lit -> doc_lit lit
+  (* P_var short form sugar *)
+  | P_var (P_aux (P_id id, _), kid) when Id.compare (id_of_kid kid) id == 0 ->
+     doc_kid kid
   | P_var (pat, kid) -> separate space [doc_pat pat; string "as"; doc_kid kid]
   | P_vector_concat pats -> separate_map (space ^^ string "@" ^^ space) doc_pat pats
   | P_wild -> string "_"
@@ -104,7 +107,9 @@ let rec doc_exp (E_aux (e_aux, _) as exp) =
   | E_lit lit -> doc_lit lit
   | E_cast (typ, exp) ->
      separate space [doc_exp exp; colon; doc_typ typ]
-  | E_app (id, exps) -> assert false
+  (* Format a function with a unit argument as f() rather than f(()) *)
+  | E_app (id, [E_aux (E_lit (L_aux (L_unit, _)), _)]) -> doc_id id ^^ string "()"
+  | E_app (id, exps) -> doc_id id ^^ parens (separate_map (comma ^^ space) doc_exp exps)
   | E_app_infix (x, id, y) -> doc_op (doc_id id) (doc_exp x) (doc_exp y)
   | E_tuple exps -> assert false
   | E_if (if_exp, then_exp, else_exp) -> assert false
@@ -121,19 +126,25 @@ let rec doc_exp (E_aux (e_aux, _) as exp) =
   | E_field (exp, id) -> assert false
   | E_case (exp, pexps) ->
      separate space [string "match"; doc_exp exp; doc_pexps pexps]
-  | E_let (lb, exp) -> assert false
+  | E_let (LB_aux (LB_val (pat, binding), _), exp) ->
+     separate space [string "let"; doc_pat pat; equals; doc_exp binding; string "in"; doc_exp exp]
   | E_assign (lexp, exp) ->
      separate space [doc_lexp lexp; equals; doc_exp exp]
   | E_sizeof nexp -> assert false
-  | E_constraint nc -> assert false
+  | E_constraint nc -> string "constraint" ^^ parens (doc_nc nc)
   | E_exit exp -> assert false
+  (* Resugar an assert with an empty message *)
+  | E_assert (exp1, E_aux (E_lit (L_aux (L_string "", _)), _)) -> string "assert" ^^ parens (doc_exp exp1)
+  | E_assert (exp1, exp2) -> string "assert" ^^ parens (doc_exp exp1 ^^ comma ^^ space ^^ doc_exp exp2)
   | E_throw exp -> assert false
   | E_try (exp, pexps) -> assert false
   | E_return exp -> assert false
 and doc_block = function
   | [] -> assert false
+  | [E_aux (E_let (LB_aux (LB_val (pat, binding), _), E_aux (E_block exps, _)), _)] ->
+     separate space [string "let"; doc_pat pat; equals; doc_exp binding] ^^ semi ^^ hardline ^^ doc_block exps
   | [exp] -> doc_exp exp
-  | exp :: exps -> doc_exp exp ^^ semi ^^ break 1 ^^ doc_block exps
+  | exp :: exps -> doc_exp exp ^^ semi ^^ hardline ^^ doc_block exps
 and doc_lexp (LEXP_aux (l_aux, _)) =
   match l_aux with
   | LEXP_id id -> doc_id id
@@ -209,4 +220,4 @@ let rec doc_def def = group (match def with
 let doc_defs (Defs(defs)) =
   separate_map hardline doc_def defs
 
-let pp_defs f d = ToChannel.pretty 1. 120 f (doc_defs d)
+let pp_defs f d = ToChannel.pretty 1. 80 f (doc_defs d)
diff --git a/src/type_check.ml b/src/type_check.ml
index d5b3de0b..76bc0d2a 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -2128,7 +2128,18 @@ and bind_pat env (P_aux (pat_aux, (l, ())) as pat) (Typ_aux (typ_aux, _) as typ)
           let env = Env.add_typ_var kid BK_nat env in
           let typed_pat, env = bind_pat env pat (atom_typ (nvar kid)) in
           annot_pat (P_var (typed_pat, kid)) typ, env
-       | None, _ -> typ_error l ("Cannot bind type variable against non existential type")
+       | None, Typ_aux (Typ_id id, _) when Id.compare id (mk_id "nat") == 0 ->
+          let env = Env.add_typ_var kid BK_nat env in
+          let env = Env.add_constraint (nc_gt (nvar kid) (nconstant 0)) env in
+          let typed_pat, env = bind_pat env pat (atom_typ (nvar kid)) in
+          annot_pat (P_var (typed_pat, kid)) typ, env
+       | None, Typ_aux (Typ_app (id, [Typ_arg_aux (Typ_arg_nexp lo, _); Typ_arg_aux (Typ_arg_nexp hi, _)]), _)
+            when Id.compare id (mk_id "range") == 0 ->
+          let env = Env.add_typ_var kid BK_nat env in
+          let env = Env.add_constraint (nc_and (nc_lteq lo (nvar kid)) (nc_lteq (nvar kid) hi)) env in
+          let typed_pat, env = bind_pat env pat (atom_typ (nvar kid)) in
+          annot_pat (P_var (typed_pat, kid)) typ, env
+       | None, _ -> typ_error l ("Cannot bind type variable against non existential or numeric type")
      end
   | P_wild -> annot_pat P_wild typ, env
   | P_cons (hd_pat, tl_pat) ->
@@ -2393,20 +2404,49 @@ and bind_lexp env (LEXP_aux (lexp_aux, (l, ())) as lexp) typ =
           in
           annot_lexp (LEXP_tup tlexps) typ, env
        (* This case is pretty much just for the PSTATE.<N,Z,C,V> := vector pattern which is really common in ASL. *)
+       (* Maybe this code can be made not horrible? *)
        | Typ_app (id, _) when Id.compare id (mk_id "vector") == 0 ->
           begin
             match destruct_vector env typ with
             | Some (_, vec_len, _, _) ->
-               let bind_bit_tuple lexp (tlexps, env) =
-                 let tlexp, env = bind_lexp env lexp (lvector_typ env (nconstant 1) bit_typ) in
-                 tlexp :: tlexps, env
+               let bind_bits_tuple lexp (tlexps, env, llen) =
+                 match lexp with
+                 | LEXP_aux (LEXP_id v, _) ->
+                    begin
+                      match Env.lookup_id v env with
+                      | Local (Immutable, _) | Enum _ ->
+                         typ_error l ("Cannot modify let-bound constant or enumeration constructor " ^ string_of_id v)
+                      | Unbound ->
+                         typ_error l "Unbound variable in vector tuple assignment"
+                      | Local (Mutable, vtyp) | Register vtyp ->
+                         let llen' = match destruct_vector env vtyp with
+                           | Some (_, llen', _, _) -> llen'
+                           | None -> typ_error l "Variables in vector tuple assignment must be vectors"
+                         in
+                         let tlexp, env = bind_lexp env lexp vtyp in
+                         tlexp :: tlexps, env, nsum llen llen'
+                    end
+                 | LEXP_aux (LEXP_field (LEXP_aux (LEXP_id v, _), fid), _) ->
+                   (* FIXME: will only work for ASL *)
+                   let rec_id =
+                     match Env.lookup_id v env with
+                     | Register (Typ_aux (Typ_id rec_id, _)) -> rec_id
+                     | _ -> typ_error l (string_of_lexp lexp ^ " must be a record register here")
+                   in
+                   let typq, (Typ_aux (Typ_fn (_, vtyp, _), _)) = Env.get_accessor rec_id fid env in
+                   let llen' = match destruct_vector env vtyp with
+                     | Some (_, llen', _, _) -> llen'
+                     | None -> typ_error l "Variables in vector tuple assignment must be vectors"
+                   in
+                   let tlexp, env = bind_lexp env lexp vtyp in
+                   tlexp :: tlexps, env, nsum llen llen'
+                 | _ -> typ_error l "bit vector assignment must only contain identifiers"
                in
-               if prove env (nc_eq vec_len (nconstant (List.length lexps)))
-               then
-                 let (tlexps, env) = List.fold_right bind_bit_tuple lexps ([], env) in
-                 annot_lexp (LEXP_tup tlexps) typ, env
+               let tlexps, env, lexp_len = List.fold_right bind_bits_tuple lexps ([], env, nconstant 0) in
+               if prove env (nc_eq vec_len lexp_len)
+               then annot_lexp (LEXP_tup tlexps) typ, env
                else typ_error l "Vector and tuple length must be the same in assignment"
-            | None -> typ_error l ("Cannot bind tuple l-expression against non tuple or vector type " ^ string_of_typ typ)
+            | None -> typ_error l ("Malformed vector type " ^ string_of_typ typ)
           end
        | _ -> typ_error l ("Cannot bind tuple l-expression against non tuple or vector type " ^ string_of_typ typ)
      end