Various small changes

* Experimented with using list<bit> to clean up manually monomorphised code in MIPS tlb
* Added option -dtc_verbose to control verbosity of new typechecker
* Allowed functions with val specs to omit their type declarations

8 files changed, 45 insertions, 35 deletions

diff --git a/lib/prelude.sail b/lib/prelude.sail
index 17b49980..05b1ac80 100644
--- a/lib/prelude.sail
+++ b/lib/prelude.sail
@@ -18,11 +18,18 @@ val forall Nat 'n, Nat 'l, Nat 'm, Nat 'o, Type 'a, 'l >= 0, 'm <= 'o, 'o <= 'l.
 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
 
-overload vector_subrange [vector_subrange_inc; vector_subrange_dec]
+val forall Nat 'n, Nat 'l, Order 'ord.
+  (vector<'n,'l,'ord,bit>, int, int) -> list<bit> effect pure vector_subrange_bl
+
+overload vector_subrange [vector_subrange_inc; vector_subrange_dec; vector_subrange_bl]
 
 (* Type safe vector append *)
 val forall Nat 'n1, Nat 'l1, Nat 'n2, Nat 'l2, Order 'o, Type 'a, 'l1 >= 0, 'l2 >= 0.
-  (vector<'n1,'l1,'o,'a>, vector<'n2,'l2,'o,'a>) -> vector<'l1 + 'l2 - 1,'l1 + 'l2,'o,'a> effect pure vector_append
+  (vector<'n1,'l1,'o,'a>, vector<'n2,'l2,'o,'a>) -> vector<'l1 + 'l2 - 1,'l1 + 'l2,'o,'a> effect pure vec_append
+
+val (list<bit>, list<bit>) -> list<bit> effect pure list_append
+
+overload vector_append [vec_append; list_append]
 
 (* Implicit register dereferencing *)
 val cast forall Type 'a. register<'a> -> 'a effect {rreg} reg_deref
@@ -39,10 +46,13 @@ 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 'm, Nat 'p, Order 'ord.
+    list<bit> -> vector<'p, 'm, 'ord, bit> effect pure extz_bl
+
 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]
+overload EXTZ [extz; extz_bl]
 overload EXTS [exts]
 
 val forall Type 'a, Nat 'n, Nat 'm, Nat 'o, Nat 'p, Order 'ord, 'm >= 'o.
@@ -187,3 +197,4 @@ typedef option = const union forall Type 'a. {
     None;
     'a Some
 }
+
diff --git a/mips_new_tc/mips_tlb.sail b/mips_new_tc/mips_tlb.sail
index f3b19d94..8e1b03ff 100644
--- a/mips_new_tc/mips_tlb.sail
+++ b/mips_new_tc/mips_tlb.sail
@@ -86,17 +86,7 @@ function (bit[64], bool) TLBTranslate2 ((bit[64]) vAddr, (MemAccessType) accessT
     else if ((accessType == StoreData) & ~(d)) then
       (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])
-      } in
+      let res = (bit[64]) (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(
       if (accessType == StoreData) then XTLBRefillS else XTLBRefillL, vAddr))
diff --git a/src/ast.ml b/src/ast.ml
index f7745eeb..0d418afc 100644
--- a/src/ast.ml
+++ b/src/ast.ml
@@ -414,7 +414,7 @@ rec_opt_aux =  (* Optional recursive annotation for functions *)
 type
 tannot_opt_aux =  (* Optional type annotation for functions *)
    Typ_annot_opt_some of typquant * typ
-
+ | Typ_annot_opt_none
 
 type
 'a alias_spec_aux =  (* Register alias expression forms. Other than where noted, each id must refer to an unaliased register of type vector *)
diff --git a/src/initial_check.ml b/src/initial_check.ml
index b6d4f863..df8fb678 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -779,7 +779,8 @@ let to_ast_rec (Parse_ast.Rec_aux(r,l): Parse_ast.rec_opt) : rec_opt =
 
 let to_ast_tannot_opt (k_env:kind Envmap.t) (def_ord:order) (Parse_ast.Typ_annot_opt_aux(tp,l)):tannot_opt * kind Envmap.t * kind Envmap.t=
   match tp with
-  | Parse_ast.Typ_annot_opt_none -> raise (Reporting_basic.err_unreachable l "Parser generated typ annot opt none")
+  | Parse_ast.Typ_annot_opt_none ->
+     Typ_annot_opt_aux (Typ_annot_opt_none, l), k_env, Envmap.empty
   | Parse_ast.Typ_annot_opt_some(tq,typ) ->
     let typq,k_env,k_local = to_ast_typquant k_env tq in
     Typ_annot_opt_aux(Typ_annot_opt_some(typq,to_ast_typ k_env def_ord typ),l),k_env,k_local
diff --git a/src/parser.mly b/src/parser.mly
index e4b05d29..9f48067f 100644
--- a/src/parser.mly
+++ b/src/parser.mly
@@ -437,7 +437,7 @@ tup_typ:
 typ:
   | tup_typ
     { $1 }
-  | tup_typ MinusGt typ Effect effect_typ
+  | tup_typ MinusGt tup_typ Effect effect_typ
     { tloc (ATyp_fn($1,$3,$5)) }
 
 lit:
diff --git a/src/sail.ml b/src/sail.ml
index e7a2bd99..bff1f58b 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -103,6 +103,9 @@ let options = Arg.align ([
   ( "-ddump_tc_ast",
     Arg.Set opt_ddump_tc_ast,
     " (debug) dump the typechecked ast to stdout");
+  ( "-dtc_verbose",
+    Arg.Int (fun verbosity -> Type_check_new.opt_tc_debug := verbosity),
+    " (debug) verbose typechecker output: 0 is silent");
   ( "-dno_cast",
     Arg.Set opt_dno_cast,
     " (debug) typecheck without any implicit casting");
diff --git a/src/type_check_new.ml b/src/type_check_new.ml
index 9f589cbc..8232fd6a 100644
--- a/src/type_check_new.ml
+++ b/src/type_check_new.ml
@@ -46,16 +46,16 @@ open Util
 open Ast_util
 open Big_int
 
-let debug = ref 1
+let opt_tc_debug = ref 0
 let depth = ref 0
 
 let rec indent n = match n with
   | 0 -> ""
   | n -> "|   " ^ indent (n - 1)
 
-let typ_debug m = if !debug > 1 then prerr_endline (indent !depth ^ m) else ()
+let typ_debug m = if !opt_tc_debug > 1 then prerr_endline (indent !depth ^ m) else ()
 
-let typ_print m = if !debug > 0 then prerr_endline (indent !depth ^ m) else ()
+let typ_print m = if !opt_tc_debug > 0 then prerr_endline (indent !depth ^ m) else ()
 
 let typ_warning m = prerr_endline ("Warning: " ^ m)
 
@@ -2325,23 +2325,26 @@ let funcl_effect (FCL_aux (FCL_Funcl (id, typed_pat, exp), (l, annot))) =
   | None -> no_effect (* Maybe could be assert false. This should never happen *)
 
 let infer_funtyp l env tannotopt funcls =
-  let Typ_annot_opt_aux (Typ_annot_opt_some (quant, ret_typ), _) = tannotopt in
-  let rec typ_from_pat (P_aux (pat_aux, (l, _)) as pat) =
-    match pat_aux with
-    | P_lit lit -> infer_lit env lit
-    | P_typ (typ, _) -> typ
-    | P_tup pats -> mk_typ (Typ_tup (List.map typ_from_pat pats))
-    | _ -> typ_error l ("Cannot infer type from pattern " ^ string_of_pat pat)
-  in
-  match funcls with
-  | [FCL_aux (FCL_Funcl (_, pat, _), _)] ->
-     let arg_typ = typ_from_pat pat in
-     let fn_typ = mk_typ (Typ_fn (arg_typ, ret_typ, Effect_aux (Effect_set [], Parse_ast.Unknown))) in
-     (quant, fn_typ)
-  | _ -> typ_error l "Cannot infer function type for function with multiple clauses"
+  match tannotopt with
+  | Typ_annot_opt_aux (Typ_annot_opt_some (quant, ret_typ), _) ->
+     begin
+       let rec typ_from_pat (P_aux (pat_aux, (l, _)) as pat) =
+         match pat_aux with
+         | P_lit lit -> infer_lit env lit
+         | P_typ (typ, _) -> typ
+         | P_tup pats -> mk_typ (Typ_tup (List.map typ_from_pat pats))
+         | _ -> typ_error l ("Cannot infer type from pattern " ^ string_of_pat pat)
+       in
+       match funcls with
+       | [FCL_aux (FCL_Funcl (_, pat, _), _)] ->
+          let arg_typ = typ_from_pat pat in
+          let fn_typ = mk_typ (Typ_fn (arg_typ, ret_typ, Effect_aux (Effect_set [], Parse_ast.Unknown))) in
+          (quant, fn_typ)
+       | _ -> typ_error l "Cannot infer function type for function with multiple clauses"
+     end
+  | Typ_annot_opt_aux (Typ_annot_opt_none, _) -> typ_error l "Cannot infer function type for unannotated function"
 
 let check_fundef env (FD_aux (FD_function (recopt, tannotopt, effectopt, funcls), (l, _)) as fd_aux) =
-  let (Typ_annot_opt_aux (Typ_annot_opt_some (annot_quant, annot_typ1), _)) = tannotopt in
   let id =
     match (List.fold_right
              (fun (FCL_aux (FCL_Funcl (id, _, _), _)) id' ->
diff --git a/src/type_check_new.mli b/src/type_check_new.mli
index 4d8b3917..f55ccf3a 100644
--- a/src/type_check_new.mli
+++ b/src/type_check_new.mli
@@ -43,6 +43,8 @@
 
 open Ast
 
+val opt_tc_debug : int ref
+
 exception Type_error of l * string;;
 
 type mut = Immutable | Mutable