Various cleanups to ott grammar

Add additional well-formedness check when calling typing rules

10 files changed, 106 insertions, 44 deletions

diff --git a/src/ast_util.ml b/src/ast_util.ml
index 3c6cbeb2..f872ac2f 100644
--- a/src/ast_util.ml
+++ b/src/ast_util.ml
@@ -60,6 +60,7 @@ let lvar_typ = function
   | Local (_, typ) -> typ
   | Register (_, _, typ) -> typ
   | Enum typ -> typ
+  | Unbound -> failwith "No type for unbound variable"
 
 let no_annot = (Parse_ast.Unknown, ())
 
@@ -962,6 +963,9 @@ let rec lexp_to_exp (LEXP_aux (lexp_aux, annot) as le) =
   | LEXP_vector_range (lexp, e1, e2) -> rewrap (E_vector_subrange (lexp_to_exp lexp, e1, e2))
   | LEXP_field (lexp, id) -> rewrap (E_field (lexp_to_exp lexp, id))
   | LEXP_memory (id, exps) -> rewrap (E_app (id, exps))
+  | LEXP_vector_concat [] -> rewrap (E_vector [])
+  | LEXP_vector_concat (lexp :: lexps) ->
+     List.fold_left (fun exp lexp -> rewrap (E_vector_append (exp, lexp_to_exp lexp))) (lexp_to_exp lexp) lexps
   | LEXP_deref exp -> rewrap (E_app (mk_id "reg_deref", [exp]))
 
 let is_unit_typ = function
@@ -1274,6 +1278,8 @@ and subst_lexp id value (LEXP_aux (lexp_aux, annot) as lexp) =
     | LEXP_tup lexps -> LEXP_tup (List.map (subst_lexp id value) lexps)
     | LEXP_vector (lexp, exp) -> LEXP_vector (subst_lexp id value lexp, subst id value exp)
     | LEXP_vector_range (lexp, exp1, exp2) -> LEXP_vector_range (subst_lexp id value lexp, subst id value exp1, subst id value exp2)
+    | LEXP_vector_concat lexps ->
+       LEXP_vector_concat (List.map (subst_lexp id value) lexps)
     | LEXP_field (lexp, id') -> LEXP_field (subst_lexp id value lexp, id')
   in
   wrap lexp_aux
diff --git a/src/c_backend.ml b/src/c_backend.ml
index 53015f8a..738f9748 100644
--- a/src/c_backend.ml
+++ b/src/c_backend.ml
@@ -1248,10 +1248,6 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
      (fun clexp -> icopy l clexp unit_fragment),
      []
 
-(*
-  | aexp -> failwith ("Cannot compile ANF expression: " ^ Pretty_print_sail.to_string (pp_aexp aexp))
- *)
-
 and compile_block ctx = function
   | [] -> []
   | exp :: exps ->
@@ -1750,7 +1746,7 @@ let flat_id () =
   incr flat_counter;
   id
 
-let flatten_instrs ctx =
+let flatten_instrs =
   let rec flatten = function
     | I_aux (I_decl (ctyp, decl_id), aux) :: instrs ->
        let fid = flat_id () in
@@ -1778,13 +1774,13 @@ let flatten_instrs ctx =
   function
   | CDEF_fundef (function_id, heap_return, args, body) ->
      flat_counter := 0;
-     [CDEF_fundef (function_id, heap_return, args, flatten body)]
+     CDEF_fundef (function_id, heap_return, args, flatten body)
 
   | CDEF_let (n, bindings, instrs) ->
     flat_counter := 0;
-    [CDEF_let (n, bindings, flatten instrs)]
+    CDEF_let (n, bindings, flatten instrs)
 
-  | cdef -> [cdef]
+  | cdef -> cdef
 
 let rec specialize_variants ctx =
 
diff --git a/src/c_backend.mli b/src/c_backend.mli
new file mode 100644
index 00000000..142a5ed5
--- /dev/null
+++ b/src/c_backend.mli
@@ -0,0 +1,78 @@
+(**************************************************************************)
+(*     Sail                                                               *)
+(*                                                                        *)
+(*  Copyright (c) 2013-2017                                               *)
+(*    Kathyrn Gray                                                        *)
+(*    Shaked Flur                                                         *)
+(*    Stephen Kell                                                        *)
+(*    Gabriel Kerneis                                                     *)
+(*    Robert Norton-Wright                                                *)
+(*    Christopher Pulte                                                   *)
+(*    Peter Sewell                                                        *)
+(*    Alasdair Armstrong                                                  *)
+(*    Brian Campbell                                                      *)
+(*    Thomas Bauereiss                                                    *)
+(*    Anthony Fox                                                         *)
+(*    Jon French                                                          *)
+(*    Dominic Mulligan                                                    *)
+(*    Stephen Kell                                                        *)
+(*    Mark Wassell                                                        *)
+(*                                                                        *)
+(*  All rights reserved.                                                  *)
+(*                                                                        *)
+(*  This software was developed by the University of Cambridge Computer   *)
+(*  Laboratory as part of the Rigorous Engineering of Mainstream Systems  *)
+(*  (REMS) project, funded by EPSRC grant EP/K008528/1.                   *)
+(*                                                                        *)
+(*  Redistribution and use in source and binary forms, with or without    *)
+(*  modification, are permitted provided that the following conditions    *)
+(*  are met:                                                              *)
+(*  1. Redistributions of source code must retain the above copyright     *)
+(*     notice, this list of conditions and the following disclaimer.      *)
+(*  2. Redistributions in binary form must reproduce the above copyright  *)
+(*     notice, this list of conditions and the following disclaimer in    *)
+(*     the documentation and/or other materials provided with the         *)
+(*     distribution.                                                      *)
+(*                                                                        *)
+(*  THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS''    *)
+(*  AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED     *)
+(*  TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A       *)
+(*  PARTICULAR PURPOSE ARE DISCLAIMED.  IN NO EVENT SHALL THE AUTHOR OR   *)
+(*  CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,          *)
+(*  SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT      *)
+(*  LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF      *)
+(*  USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND   *)
+(*  ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,    *)
+(*  OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT    *)
+(*  OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF    *)
+(*  SUCH DAMAGE.                                                          *)
+(**************************************************************************)
+
+open Bytecode
+open Type_check
+
+(** Global compilation options *)
+
+val opt_ddump_flow_graphs : bool ref
+val opt_trace : bool ref
+val opt_static : bool ref
+
+(** Optimization flags *)
+
+val optimize_primops : bool ref
+val optimize_hoist_allocations : bool ref
+val optimize_struct_updates : bool ref
+
+(** The compilation context. *)
+type ctx
+
+(** Create a context from a typechecking environment. This environment
+   should be the environment returned by typechecking the full AST. *)
+val initial_ctx : Env.t -> ctx
+
+val compile_ast : ctx -> tannot Ast.defs -> unit
+
+val bytecode_ast : ctx -> (cdef list -> cdef list) -> tannot Ast.defs -> cdef list
+
+(** Rewriting steps for compiled ASTs *)
+val flatten_instrs : cdef -> cdef
diff --git a/src/initial_check.ml b/src/initial_check.ml
index bec9d847..bc0fe07a 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -627,26 +627,16 @@ and to_ast_record_try (k_env:kind Envmap.t) (def_ord:order) (Parse_ast.E_aux(exp
 
 let to_ast_default (names, k_env, default_order) (default : Parse_ast.default_typing_spec) : default_spec envs_out =
   match default with
-  | Parse_ast.DT_aux(df,l) ->
-    (match df with
-    | Parse_ast.DT_kind(bk,v) ->
-      let k,k_typ = to_ast_base_kind bk in
-      let v = to_ast_var v in
-      let key = var_to_string v in
-      DT_aux(DT_kind(k,v),l),(names,(Envmap.insert k_env (key,k_typ)),default_order)
-    | Parse_ast.DT_typ(typschm,id) ->
-      let tps,_,_ = to_ast_typschm k_env default_order typschm in
-      DT_aux(DT_typ(tps,to_ast_id id),l),(names,k_env,default_order)
-    | Parse_ast.DT_order(bk,o) ->
-      let k,k_typ = to_ast_base_kind bk in
-      (match (k,o) with
-	| (BK_aux(BK_order, _), Parse_ast.ATyp_aux(Parse_ast.ATyp_inc,lo)) ->
-	  let default_order = Ord_aux(Ord_inc,lo) in
-	  DT_aux(DT_order default_order,l),(names,k_env,default_order)
-	| (BK_aux(BK_order, _), Parse_ast.ATyp_aux(Parse_ast.ATyp_dec,lo)) ->
-	  let default_order = Ord_aux(Ord_dec,lo) in
-	  DT_aux(DT_order default_order,l),(names,k_env,default_order)
-	| _ -> typ_error l "Inc and Dec must have kind Order" None None None))
+  | Parse_ast.DT_aux(Parse_ast.DT_order(bk,o),l) ->
+     let k,k_typ = to_ast_base_kind bk in
+     (match (k,o) with
+      | (BK_aux(BK_order, _), Parse_ast.ATyp_aux(Parse_ast.ATyp_inc,lo)) ->
+         let default_order = Ord_aux(Ord_inc,lo) in
+         DT_aux(DT_order default_order,l),(names,k_env,default_order)
+      | (BK_aux(BK_order, _), Parse_ast.ATyp_aux(Parse_ast.ATyp_dec,lo)) ->
+         let default_order = Ord_aux(Ord_dec,lo) in
+         DT_aux(DT_order default_order,l),(names,k_env,default_order)
+      | _ -> typ_error l "Inc and Dec must have kind Order" None None None)
 
 let to_ast_spec (names,k_env,default_order) (val_:Parse_ast.val_spec) : (unit val_spec) envs_out =
   match val_ with
diff --git a/src/isail.ml b/src/isail.ml
index 4adc1cd2..60c35ca7 100644
--- a/src/isail.ml
+++ b/src/isail.ml
@@ -282,7 +282,7 @@ let handle_input' input =
             let ast = Process_file.rewrite_ast_c !interactive_ast in
             let ast, env = Specialize.specialize ast !interactive_env in
             let ctx = initial_ctx env in
-            let byte_ast = bytecode_ast ctx (fun cdefs -> List.concat (List.map (flatten_instrs ctx) cdefs)) ast in
+            let byte_ast = bytecode_ast ctx (List.map flatten_instrs) ast in
             let chan = open_out arg in
             Util.opt_colors := false;
             Pretty_print_sail.pretty_sail chan (separate_map hardline Bytecode_util.pp_cdef byte_ast);
diff --git a/src/parse_ast.ml b/src/parse_ast.ml
index b5875ea7..d9ffb184 100644
--- a/src/parse_ast.ml
+++ b/src/parse_ast.ml
@@ -424,9 +424,7 @@ name_scm_opt =
 
 type 
 default_typing_spec_aux =  (* Default kinding or typing assumption, and default order for literal vectors and vector shorthands *)
-   DT_kind of base_kind * kid
- | DT_order of base_kind * atyp
- | DT_typ of typschm * id
+   DT_order of base_kind * atyp
 
 
 type mpat_aux =  (* Mapping pattern. Mostly the same as normal patterns but only constructible parts *)
diff --git a/src/pretty_print_common.ml b/src/pretty_print_common.ml
index d223b07a..b449c72a 100644
--- a/src/pretty_print_common.ml
+++ b/src/pretty_print_common.ml
@@ -111,7 +111,8 @@ let doc_effect (BE_aux (e,_)) =
   | BE_escape -> "escape"
   | BE_undef -> "undef"
   | BE_unspec -> "unspec"
-  | BE_nondet -> "nondet")
+  | BE_nondet -> "nondet"
+  | BE_config -> "config")
 
 let doc_effects (Effect_aux(e,_)) = match e with
   | Effect_set [] -> string "pure"
diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml
index 9d9b4b4e..06f1d768 100644
--- a/src/pretty_print_sail.ml
+++ b/src/pretty_print_sail.ml
@@ -443,10 +443,7 @@ let doc_funcl (FCL_aux (FCL_Funcl (id, Pat_aux (pexp,_)), _)) =
   | Pat_when (pat,wh,exp) ->
      group (separate space [doc_id id; parens (separate space [doc_pat pat; string "if"; doc_exp wh]); string "="; doc_exp exp])
 
-let doc_default (DT_aux(df,_)) = match df with
-  | DT_kind(bk,v) -> string "DT_kind" (* separate space [string "default"; doc_bkind bk; doc_var v] *)
-  | DT_typ(ts,id) -> separate space [string "default"; doc_typschm ts; doc_id id]
-  | DT_order(ord) -> separate space [string "default"; string "Order"; doc_ord ord]
+let doc_default (DT_aux (DT_order ord, _)) = separate space [string "default"; string "Order"; doc_ord ord]
 
 let doc_fundef (FD_aux (FD_function (r, typa, efa, funcls), _)) =
   match funcls with
diff --git a/src/sail_lib.ml b/src/sail_lib.ml
index 16b1d3cc..a7f91beb 100644
--- a/src/sail_lib.ml
+++ b/src/sail_lib.ml
@@ -507,7 +507,7 @@ let int_of_string_opt s =
   try
     Some (int_of_string s)
   with
-  | Failure "int_of_string" -> None
+  | Failure _ -> None
 
 (* highly inefficient recursive implementation *)
 let rec maybe_int_of_prefix = function
diff --git a/src/type_check.ml b/src/type_check.ml
index f98ddb98..e538bc36 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -1653,7 +1653,6 @@ let subst_unifiers unifiers typ =
     | U_nexp nexp -> typ_subst_nexp kid (unaux_nexp nexp) typ
     | U_order ord -> typ_subst_order kid (unaux_order ord) typ
     | U_typ subst -> typ_subst_typ kid (unaux_typ subst) typ
-    | _ -> typ_error Parse_ast.Unknown "Cannot subst unifier"
   in
   List.fold_left subst_unifier typ (KBindings.bindings unifiers)
 
@@ -1663,7 +1662,6 @@ let subst_args_unifiers unifiers typ_args =
     | U_nexp nexp -> List.map (typ_subst_arg_nexp kid (unaux_nexp nexp)) typ_args
     | U_order ord -> List.map (typ_subst_arg_order kid (unaux_order ord)) typ_args
     | U_typ subst -> List.map (typ_subst_arg_typ kid (unaux_typ subst)) typ_args
-    | _ -> typ_error Parse_ast.Unknown "Cannot subst unifier"
   in
   List.fold_left subst_unifier typ_args (KBindings.bindings unifiers)
 
@@ -1673,7 +1671,6 @@ let subst_uvar_unifiers unifiers uvar =
     | U_nexp nexp -> uvar_subst_nexp kid (unaux_nexp nexp) uvar'
     | U_order ord -> uvar_subst_order kid (unaux_order ord) uvar'
     | U_typ subst -> uvar_subst_typ kid (unaux_typ subst) uvar'
-    | _ -> typ_error Parse_ast.Unknown "Cannot subst unifier"
   in
   List.fold_left subst_unifier uvar (KBindings.bindings unifiers)
 
@@ -2233,6 +2230,7 @@ let crule r env exp typ =
   typ_print (lazy (Util.("Check " |> cyan |> clear) ^ string_of_exp exp ^ " <= " ^ string_of_typ typ));
   try
     let checked_exp = r env exp typ in
+    Env.wf_typ env (typ_of checked_exp);
     decr depth; checked_exp
   with
   | Type_error (l, err) -> decr depth; typ_raise l err
@@ -2242,6 +2240,7 @@ let irule r env exp =
   try
     let inferred_exp = r env exp in
     typ_print (lazy (Util.("Infer " |> blue |> clear) ^ string_of_exp exp ^ " => " ^ string_of_typ (typ_of inferred_exp)));
+    Env.wf_typ env (typ_of inferred_exp);
     decr depth;
     inferred_exp
   with
@@ -4355,12 +4354,9 @@ let check_val_spec env (VS_aux (vs, (l, _))) =
 
 let check_default env (DT_aux (ds, l)) =
   match ds with
-  | DT_kind _ -> [DEF_default (DT_aux (ds,l))], env (* Check: Is this supposed to do nothing? *)
   | DT_order (Ord_aux (Ord_inc, _)) -> [DEF_default (DT_aux (ds, l))], Env.set_default_order_inc env
   | DT_order (Ord_aux (Ord_dec, _)) -> [DEF_default (DT_aux (ds, l))], Env.set_default_order_dec env
   | DT_order (Ord_aux (Ord_var _, _)) -> typ_error l "Cannot have variable default order"
-  (* This branch allows us to write something like: default forall Nat 'n. [|'n|] name... what does this even mean?! *)
-  | DT_typ (typschm, id) -> typ_error l ("Unsupported default construct")
 
 let kinded_id_arg kind_id =
   let typ_arg arg = Typ_arg_aux (arg, Parse_ast.Unknown) in