Created version of typecheck test suite for sail2 branch

Currently doesn't try to compile to lem or use the MIPS spec

All the failing tests have been removed because I intend to handle
them differently - they were very fragile before because there was no
indication of why they failed, so as sail evolved they tended to start
failing for the wrong reasons and not testing what they were supposed
to.

7 files changed, 75 insertions, 12 deletions

diff --git a/src/initial_check.ml b/src/initial_check.ml
index 5f3930b6..87adb290 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -1022,7 +1022,6 @@ let generate_undefineds vs_ids (Defs defs) =
            gen_vs (mk_id "undefined_string") "unit -> string effect {undef}";
            gen_vs (mk_id "undefined_list") "forall ('a:Type). 'a -> list('a) effect {undef}";
            gen_vs (mk_id "undefined_range") "forall 'n 'm. (atom('n), atom('m)) -> range('n,'m) effect {undef}";
-           (* FIXME: How to handle inc/dec order correctly? *)
            gen_vs (mk_id "undefined_vector") "forall 'n ('a:Type) ('ord : Order). (atom('n), 'a) -> vector('n, 'ord,'a) effect {undef}";
            (* Only used with lem_mwords *)
            gen_vs (mk_id "undefined_bitvector") "forall 'n. atom('n) -> vector('n, dec, bit) effect {undef}";
diff --git a/src/initial_check.mli b/src/initial_check.mli
index 9d1e0d30..5466dece 100644
--- a/src/initial_check.mli
+++ b/src/initial_check.mli
@@ -54,6 +54,15 @@ open Ast_util
 val opt_undefined_gen : bool ref
 val opt_magic_hash : bool ref
 
+(* This is a bit of a hack right now - it ensures that the undefiend
+   builtins (undefined_vector etc), only get added to the ast
+   once. The original assumption in sail is that the whole AST gets
+   processed at once (therefore they could only get added once), and
+   this isn't true any more with the interpreter. This needs to be
+   public so the interpreter can set it back to false if it unloads
+   all the loaded files. *)
+val have_undefined_builtins : bool ref
+
 val ast_of_def_string : order -> string -> unit defs
 val process_ast : order -> Parse_ast.defs -> unit defs
 
diff --git a/src/isail.ml b/src/isail.ml
index a0e45e45..e6dcc809 100644
--- a/src/isail.ml
+++ b/src/isail.ml
@@ -112,6 +112,8 @@ let print_program () =
      let sep = "-----------------------------------------------------" |> Util.blue |> Util.clear in
      List.map stack_string stack |> List.rev |> List.iter (fun code -> print_endline code; print_endline sep);
      print_endline out
+  | Evaluation (Done (_, v)) ->
+     print_endline (Value.string_of_value v |> Util.green |> Util.clear)
   | Evaluation _ -> ()
 
 let rec run () =
@@ -177,6 +179,8 @@ let help = function
   | ":l" | ":load" -> String.concat "\n"
      [ "(:l | :load) <files> - Load sail files and add their definitions to the interactive environment.";
        "Files containing scattered definitions must be loaded together." ]
+  | ":u" | ":unload" ->
+     "(:u | :unload) - Unload all loaded files."
   | cmd ->
      "Either invalid command passed to help, or no documentation for " ^ cmd ^ ". Try :help :help."
 
@@ -236,8 +240,10 @@ let handle_input' input =
          | ":commands" ->
             let commands =
               [ "Universal commands - :(t)ype :(i)nfer :(q)uit :(v)erbose :clear :commands :help";
-                "Normal mode commands - :elf :(l)oad";
-                "Evaluation mode commands - :(r)un :(s)tep :(n)ormal" ]
+                "Normal mode commands - :elf :(l)oad :(u)nload";
+                "Evaluation mode commands - :(r)un :(s)tep :(n)ormal";
+                "";
+                ":(c)ommand can be called as either :c or :command." ]
             in
             List.iter print_endline commands
          | ":help" -> print_endline (help arg)
@@ -263,6 +269,13 @@ let handle_input' input =
                interactive_state := initial_state !interactive_ast;
                interactive_env := env;
                vs_ids := Initial_check.val_spec_ids !interactive_ast
+            | ":u" | ":unload" ->
+               interactive_ast := Ast.Defs [];
+               interactive_env := Type_check.initial_env;
+               interactive_state := initial_state !interactive_ast;
+               vs_ids := Initial_check.val_spec_ids !interactive_ast;
+               (* See initial_check.mli for an explanation of why we need this. *)
+               Initial_check.have_undefined_builtins := false
             | _ -> unrecognised_command cmd
           end
        | Expression str ->
diff --git a/src/lexer.mll b/src/lexer.mll
index d13ba849..fb33552b 100644
--- a/src/lexer.mll
+++ b/src/lexer.mll
@@ -131,7 +131,6 @@ let kw_table =
      ("let",                     (fun x -> Let_));
      ("var",                     (fun _ -> Var));
      ("ref",                     (fun _ -> Ref));
-     ("record",                  (fun _ -> Record));
      ("Int",                     (fun x -> Int));
      ("Order",                   (fun x -> Order));
      ("pure",                    (fun x -> Pure));
@@ -201,6 +200,7 @@ rule token = parse
   | "@"                                 { (At "@") }
   | "2" ws "^"                          { TwoCaret }
   | "^"					{ (Caret(r"^")) }
+  | "::"                                { ColonColon(r "::") }
   | ":"                                 { Colon(r ":") }
   | ","                                 { Comma }
   | ".."                                { DotDot }
diff --git a/src/parser.mly b/src/parser.mly
index 7af70687..b11b4b61 100644
--- a/src/parser.mly
+++ b/src/parser.mly
@@ -107,6 +107,7 @@ let qi_id_of_kopt (KOpt_aux (kopt_aux, l) as kopt) = QI_aux (QI_id kopt, l)
 let mk_recn = (Rec_aux((Rec_nonrec), Unknown))
 let mk_typqn = (TypQ_aux(TypQ_no_forall,Unknown))
 let mk_tannotn = Typ_annot_opt_aux(Typ_annot_opt_none,Unknown)
+let mk_tannot typq typ n m = Typ_annot_opt_aux(Typ_annot_opt_some (typq, typ), loc n m)
 let mk_eannotn = Effect_opt_aux(Effect_opt_pure,Unknown)
 let mk_namesectn = Name_sect_aux(Name_sect_none,Unknown)
 
@@ -157,7 +158,7 @@ let rec desugar_rchain chain s e =
 %token Pure Register Return Scattered Sizeof Struct Then True TwoCaret TYPE Typedef
 %token Undefined Union Newtype With Val Constraint Throw Try Catch Exit Bitfield
 %token Barr Depend Rreg Wreg Rmem Rmemt Wmem Wmv Wmvt Eamem Exmem Undef Unspec Nondet Escape
-%token Repeat Until While Do Record Mutual Var Ref
+%token Repeat Until While Do Mutual Var Ref
 
 %nonassoc Then
 %nonassoc Else
@@ -173,7 +174,7 @@ let rec desugar_rchain chain s e =
 %token <string> String Bin Hex Real
 
 %token <string> Amp At Caret Eq Gt Lt Plus Star EqGt Unit
-%token <string> Colon ExclEq
+%token <string> Colon ColonColon ExclEq
 %token <string> GtEq
 %token <string> LtEq
 
@@ -639,6 +640,8 @@ pat1:
     { $1 }
   | atomic_pat At pat_concat
     { mk_pat (P_vector_concat ($1 :: $3)) $startpos $endpos }
+  | atomic_pat ColonColon pat1
+    { mk_pat (P_cons ($1, $3)) $startpos $endpos }
 
 pat_concat:
   | atomic_pat
@@ -679,6 +682,10 @@ atomic_pat:
     { mk_pat (P_tup ($2 :: $4)) $startpos $endpos }
   | Lsquare pat_list Rsquare
     { mk_pat (P_vector $2) $startpos $endpos }
+  | LsquareBar RsquareBar
+    { mk_pat (P_list []) $startpos $endpos }
+  | LsquareBar pat_list RsquareBar
+    { mk_pat (P_list $2) $startpos $endpos }
 
 lit:
   | True
@@ -854,6 +861,7 @@ exp5:
   | exp5l op5l exp6 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
   | exp6 op5r exp5r { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
   | exp6 At exp5r { mk_exp (E_vector_append ($1, $3)) $startpos $endpos }
+  | exp6 ColonColon exp5r { mk_exp (E_cons ($1, $3)) $startpos $endpos }
   | exp6 { $1 }
 exp5l:
   | exp6 op5 exp6 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
@@ -863,6 +871,7 @@ exp5r:
   | exp6 op5 exp6 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
   | exp6 op5r exp5r { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
   | exp6 At exp5r { mk_exp (E_vector_append ($1, $3)) $startpos $endpos }
+  | exp6 ColonColon exp5r { mk_exp (E_cons ($1, $3)) $startpos $endpos }
   | exp6 { $1 }
 
 exp6:
@@ -999,7 +1008,7 @@ atomic_exp:
     { mk_exp (E_vector_access ($1, $3)) $startpos $endpos }
   | atomic_exp Lsquare exp DotDot exp Rsquare
     { mk_exp (E_vector_subrange ($1, $3, $5)) $startpos $endpos }
-  | Record Lcurly fexp_exp_list Rcurly
+  | Struct Lcurly fexp_exp_list Rcurly
     { mk_exp (E_record $3) $startpos $endpos }
   | Lcurly exp With fexp_exp_list Rcurly
     { mk_exp (E_record_update ($2, $4)) $startpos $endpos }
@@ -1009,6 +1018,8 @@ atomic_exp:
     { mk_exp (E_vector_update ($2, $4, $6)) $startpos $endpos }
   | Lsquare exp With atomic_exp DotDot atomic_exp Eq exp Rsquare
     { mk_exp (E_vector_update_subrange ($2, $4, $6, $8)) $startpos $endpos }
+  | LsquareBar RsquareBar
+    { mk_exp (E_list []) $startpos $endpos }
   | LsquareBar exp_list RsquareBar
     { mk_exp (E_list $2) $startpos $endpos }
   | Lparen exp Rparen
@@ -1038,16 +1049,38 @@ funcl_patexp:
   | Lparen pat If_ exp Rparen Eq exp
     { mk_pexp (Pat_when ($2, $4, $7)) $startpos $endpos }
 
+funcl_patexp_typ:
+  | pat Eq exp
+    { (mk_pexp (Pat_exp ($1, $3)) $startpos $endpos, mk_tannotn) }
+  | pat MinusGt funcl_typ Eq exp
+    { (mk_pexp (Pat_exp ($1, $5)) $startpos $endpos, $3) }
+  | Lparen pat If_ exp Rparen Eq exp
+    { (mk_pexp (Pat_when ($2, $4, $7)) $startpos $endpos, mk_tannotn) }
+  | Lparen pat If_ exp Rparen MinusGt funcl_typ Eq exp
+    { (mk_pexp (Pat_when ($2, $4, $9)) $startpos $endpos, $7) }
+
 funcl:
   | id funcl_patexp
     { mk_funcl (FCL_Funcl ($1, $2)) $startpos $endpos }
 
-funcls:
+funcls2:
   | id funcl_patexp
     { [mk_funcl (FCL_Funcl ($1, $2)) $startpos $endpos] }
-  | id funcl_patexp And funcls
+  | id funcl_patexp And funcls2
     { mk_funcl (FCL_Funcl ($1, $2)) $startpos $endpos :: $4 }
 
+funcls:
+  | id funcl_patexp_typ
+    { let pexp, tannot = $2 in ([mk_funcl (FCL_Funcl ($1, pexp)) $startpos $endpos], tannot) }
+  | id funcl_patexp And funcls2
+    { (mk_funcl (FCL_Funcl ($1, $2)) $startpos $endpos :: $4, mk_tannotn) }
+
+funcl_typ:
+  | Forall typquant Dot typ
+    { mk_tannot $2 $4 $startpos $endpos }
+  | typ
+    { mk_tannot mk_typqn $1 $startpos $endpos }
+
 index_range:
   | Num
     { mk_ir (BF_single $1) $startpos $endpos }
@@ -1130,7 +1163,7 @@ type_unions:
 
 fun_def:
   | Function_ funcls
-    { mk_fun (FD_function (mk_recn, mk_tannotn, mk_eannotn, $2)) $startpos $endpos }
+    { let funcls, tannot = $2 in mk_fun (FD_function (mk_recn, tannot, mk_eannotn, funcls)) $startpos $endpos }
 
 fun_def_list:
   | fun_def
diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml
index 930da39c..887b15a0 100644
--- a/src/pretty_print_sail.ml
+++ b/src/pretty_print_sail.ml
@@ -220,6 +220,7 @@ let rec doc_pat (P_aux (p_aux, _) as pat) =
   | P_wild -> string "_"
   | P_as (pat, id) -> separate space [doc_pat pat; string "as"; doc_id id]
   | P_app (id, pats) -> doc_id id ^^ parens (separate_map (comma ^^ space) doc_pat pats)
+  | P_list pats -> string "[|" ^^ separate_map (comma ^^ space) doc_pat pats ^^ string "|]"
   | _ -> string (string_of_pat pat)
 
 (* if_block_x is true if x should be printed like a block, i.e. with
@@ -285,8 +286,8 @@ let rec doc_exp (E_aux (e_aux, _) as exp) =
      group (separate space [string "if"; doc_exp if_exp; string "then"; doc_exp then_exp; string "else"; doc_exp else_exp])
 
   | E_list exps -> string "[|" ^^ separate_map (comma ^^ space) doc_exp exps ^^ string "|]"
-  | E_cons (exp1, exp2) -> string "E_cons"
-  | E_record fexps -> separate space [string "record"; string "{"; doc_fexps fexps; string "}"]
+  | E_cons (exp1, exp2) -> doc_atomic_exp exp1 ^^ space ^^ string "::" ^^ space ^^ doc_exp exp2
+  | E_record fexps -> separate space [string "struct"; string "{"; doc_fexps fexps; string "}"]
   | E_loop (While, cond, exp) ->
      separate space [string "while"; doc_exp cond; string "do"; doc_exp exp]
   | E_loop (Until, cond, exp) ->
diff --git a/src/type_check.ml b/src/type_check.ml
index 01ff8649..3353daf4 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -2722,6 +2722,14 @@ and infer_exp env (E_aux (exp_aux, (l, ())) as exp) =
             | E_aux (E_app (field, [inferred_exp]) ,_) -> annot_exp (E_field (inferred_exp, field)) (typ_of inferred_acc)
             | _ -> assert false (* Unreachable *)
           end
+       (* Not sure if we need to do anything different with args here. *)
+       | Typ_aux (Typ_app (rectyp, args), _) as typ when Env.is_record rectyp env ->
+          begin
+            let inferred_acc, _ = infer_funapp' l (Env.no_casts env) field (Env.get_accessor_fn rectyp field env) [strip_exp inferred_exp] None in
+            match inferred_acc with
+            | E_aux (E_app (field, [inferred_exp]) ,_) -> annot_exp (E_field (inferred_exp, field)) (typ_of inferred_acc)
+            | _ -> assert false (* Unreachable *)
+          end
        | _ ->  typ_error l ("Field expression " ^ string_of_exp exp ^ " :: " ^ string_of_typ (typ_of inferred_exp) ^ " is not valid")
      end
   | E_tuple exps ->