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

6 files changed, 30 insertions, 21 deletions

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