Various cleanups to ott grammar

Add additional well-formedness check when calling typing rules

11 files changed, 158 insertions, 198 deletions

diff --git a/language/sail.ott b/language/sail.ott
index 4116013e..7ec736c5 100644
--- a/language/sail.ott
+++ b/language/sail.ott
@@ -151,30 +151,22 @@ id :: '' ::=
 % We don't enforce a lexical convention on infix operators, as some of the 
 % targets use alphabetical infix operators.
 
-% Vector builtins 
+% Vector builtins
   | vector_access          :: M :: vector_access  {{ ichlo (Id "vector_access") }} 
   | vector_update          :: M :: vector_update  {{ ichlo (Id "vector_update") }}
   | vector_update_subrange :: M :: vector_update_subrange {{ ichlo (Id "vector_update_subrange") }}
   | vector_subrange        :: M :: vector_subrange {{ ichlo (Id "vector_subrange") }}
-  | vector_append        :: M :: vector_append {{ ichlo (Id "vector_append") }}
-
-% Comparison builtins
-  | lteq_atom_atom :: M :: lteq_atom_atom {{ ichlo (Id "lteq_atom_atom") }}
-  | gteq_atom_atom :: M :: gteq_atom_atom {{ ichlo (Id "gteq_atom_atom") }}
-  | lt_atom_atom :: M :: lt_atom_atom {{ ichlo (Id "lt_atom_atom") }}
-  | gt_atom_atom :: M :: gt_atom_atom {{ ichlo (Id "gt_atom_atom") }}
-  
+  | vector_append          :: M :: vector_append {{ ichlo (Id "vector_append") }}
+
 kid :: '' ::=
-  {{ com kinded IDs: $[[Type]]$, $[[Nat]]$, $[[Order]]$, and $[[Effect]]$ variables }}
+  {{ com kinded IDs: Type, Int, and Order variables }}
   {{ aux _ l }}
-  | ' x                       :: :: var
- 
+  | ' x :: :: var
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 % Kinds and Types                                              %
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
-
 grammar
 
 base_kind :: 'BK_' ::=
@@ -191,7 +183,7 @@ kind :: 'K_' ::=
 % we'll never use  ...-> Nat , .. Order , .. or Effects
 
 nexp :: 'Nexp_' ::=
-  {{ com numeric expression, of kind $[[Nat]]$ }}
+  {{ com numeric expression, of kind Int }}
   {{ aux _ l }}
   | id                                  :: :: id       {{ com abbreviation identifier }}
   | kid                                 :: :: var      {{ com variable }}
@@ -199,33 +191,33 @@ nexp :: 'Nexp_' ::=
   | id ( nexp1 , ... , nexpn )          :: :: app      {{ com app }}
   | nexp1 * nexp2                       :: :: times    {{ com product }}
   | nexp1 + nexp2                       :: :: sum      {{ com sum }}
-  | nexp1 - nexp2			:: :: minus    {{ com subtraction }}
+  | nexp1 - nexp2                       :: :: minus    {{ com subtraction }}
   | 2** nexp                            :: :: exp      {{ com exponential }}
-  | neg nexp				:: I :: neg    {{ com for internal use only}}
+  | neg nexp                            :: I :: neg    {{ com for internal use only}}
   | ( nexp )                            :: S :: paren  {{ ichlo [[nexp]] }}
 
-order :: 'Ord_' ::=  
-  {{ com vector order specifications, of kind $[[Order]]$}}
-  {{ aux _ l }} 
+order :: 'Ord_' ::=
+  {{ com vector order specifications, of kind Order }}
+  {{ aux _ l }}
   | kid                                 :: :: var {{ com variable }} 
   | inc                                 :: :: inc  {{ com increasing }}
   | dec                                 :: :: dec  {{ com decreasing }}
-  | ( order )                             :: S :: paren {{ ichlo [[order]] }}
+  | ( order )                           :: S :: paren {{ ichlo [[order]] }}
 
 base_effect :: 'BE_' ::=
   {{ com effect }}
-  {{ aux _ l }}  
+  {{ aux _ l }}
   | rreg                                :: :: rreg {{ com read register }}
   | wreg                                :: :: wreg {{ com write register }}
   | rmem                                :: :: rmem {{ com read memory }}
   | rmemt                               :: :: rmemt {{ com read memory and tag }}
   | wmem                                :: :: wmem {{ com write memory }}
-  | wmea				                :: :: eamem {{ com signal effective address for writing memory }}
+  | wmea                                :: :: eamem {{ com signal effective address for writing memory }}
   | exmem                               :: :: exmem {{ com determine if a store-exclusive (ARM) is going to succeed }}
-  | wmv					                :: :: wmv   {{ com write memory, sending only value }}
+  | wmv                                 :: :: wmv   {{ com write memory, sending only value }}
   | wmvt                                :: :: wmvt  {{ com write memory, sending only value and tag }}
   | barr                                :: :: barr {{ com memory barrier }}
-  | depend				                :: :: depend {{ com dynamic footprint }}
+  | depend                              :: :: depend {{ com dynamic footprint }}
   | undef                               :: :: undef {{ com undefined-instruction exception }}
   | unspec                              :: :: unspec {{ com unspecified values }}
   | nondet                              :: :: nondet {{ com nondeterminism, from $[[nondet]]$ }}
@@ -233,18 +225,13 @@ base_effect :: 'BE_' ::=
   | config                              :: :: config {{ com configuration option }}
 
 effect :: 'Effect_' ::=
-  {{ com effect set, of kind $[[Effect]]$ }}
   {{ aux _ l }}
- | { base_effect1 , .. , base_effectn }           :: :: set {{ com effect set }}
- | pure                                 :: M :: pure {{ com sugar for empty effect set }} 
-   {{ lem (Effect_set [])  }} {{icho [[{}]] }}
- | effect1 u+ .. u+ effectn                   :: M :: union {{ com union of sets of effects }} {{ icho [] }}
-   {{ lem (List.foldr effect_union (Effect_aux (Effect_set []) Unknown) [[effect1..effectn]]) }}
-
-% TODO: are we going to need any effect polymorphism?  Conceivably for built-in maps and folds.  Yes.  But we think we don't need any interesting effect-set expressions, eg effectset-variable union {rreg}. 
+  | { base_effect1 , .. , base_effectn }           :: :: set {{ com effect set }}
+  | pure                                           :: M :: pure {{ com sugar for empty effect set }}
+    {{ lem (Effect_set []) }}
 
 typ :: 'Typ_' ::=
-  {{ com type expressions, of kind $[[Type]]$ }}
+  {{ com type expressions, of kind Type }}
   {{ aux _ l }}
   |                                            :: :: internal_unknown
   | id                                         :: :: id
@@ -289,40 +276,15 @@ typ :: 'Typ_' ::=
 % not sure how first-class it should be, though
 % use "reg word32" etc for the types of vanilla registers 
 
- 
 typ_arg :: 'Typ_arg_' ::=
   {{ com type constructor arguments of all kinds }}
-  {{ aux _ l }} 
+  {{ aux _ l }}
   | nexp       :: :: nexp
   | typ        :: :: typ
   | order      :: :: order
 
-% plus more for l-value/r-value pairs, as introduced by the L3 'compound' declarations   ... ref typ
-
-%typ_lib :: 'Typ_lib_' ::=
-%  {{ com library types and syntactic sugar for them }}
-%  {{ aux _ l }} {{ auxparam 'a }}
-% boring base types:
-%%  | unit :: :: unit {{ com unit type with value $()$ }}
-%  | bool :: :: bool {{ com booleans $[[true]]$ and $[[false]]$ }}
-%  | bit :: :: bit  {{ com pure bit values (not mutable bits) }}
-% experimentally trying with two distinct types of bool and bit ...
-%  | nat :: :: nat {{ com natural numbers 0,1,2,... }}
-%  | string :: :: string {{ com UTF8 strings }}
-% finite subranges of nat
-
-parsing
-
-Typ_tup <= Typ_tup
-Typ_fn right Typ_fn
-Typ_fn <= Typ_tup
-%Typ_fn right Typ_app1
-%Typ_tup right Typ_app1
-
-grammar
-
 n_constraint :: 'NC_' ::=
-  {{ com constraint over kind $[[Nat]]$ }}
+  {{ com constraint over kind Int }}
   {{ aux _ l }}
   | nexp = nexp'                                :: :: equal
   | nexp >= nexp'                               :: :: bounded_ge
@@ -344,24 +306,21 @@ kinded_id :: 'KOpt_' ::=
   | kind kid				      :: :: kind {{ com kind-annotated variable }}
 
 quant_item :: 'QI_' ::=
-  {{ com kinded identifier or $[[Nat]]$ constraint }}
+  {{ com kinded identifier or Int constraint }}
   {{ aux _ l }}
   | kinded_id 	  	 	       	      :: :: id {{ com optionally kinded identifier }}
-  | n_constraint			      :: :: const {{ com $[[Nat]]$ constraint }}
+  | n_constraint			      :: :: const {{ com Int constraint }}
 
-typquant :: 'TypQ_' ::= 
+typquant :: 'TypQ_' ::=
   {{ com type quantifiers and constraints}}
   {{ aux _ l }}
   | forall quant_item1 , ... , quant_itemn . :: :: tq %{{ texlong }}
-% WHY ARE CONSTRAINTS HERE AND NOT IN THE KIND LANGUAGE
-  |                           ::  ::  no_forall     {{ com empty }}
+  |                                          :: ::  no_forall     {{ com empty }}
 
 typschm :: 'TypSchm_' ::=
   {{ com type scheme  }}
   {{ aux _ l }}
-  |  typquant typ                                                       :: :: ts
-
-
+  |  typquant typ                            :: :: ts
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 % Type definitions                                             %
@@ -431,21 +390,6 @@ kind_def :: 'KD_' ::=
   {{ aux _ annot }} {{ auxparam 'a }}
   | Def kind id name_scm_opt = nexp                                           :: :: nabbrev
     {{ com $[[Nat]]$-expression abbreviation }}
-%  | Def kind id name_scm_opt = typschm                                        :: D :: abbrev
-%    {{ com type abbreviation }} {{ texlong }}
-%  | Def kind id name_scm_opt = const struct typquant { typ1 id1 ; ... ; typn idn semi_opt }     :: D :: record
-%    {{ com struct type definition }} {{ texlong }}
-%  | Def kind id name_scm_opt = const union typquant { type_union1 ; ... ; type_unionn semi_opt }   :: D :: variant
-%    {{ com union type definition}} {{ texlong }}
-%  | Def kind id name_scm_opt = enumerate { id1 ; ... ; idn semi_opt }   :: D :: enum
-%    {{ com enumeration type definition}} {{ texlong }}
-%
-%  | Def kind id = register bits [ nexp : nexp' ] { index_range1 : id1 ; ... ; index_rangen : idn } 
-%:: D :: register {{ com register mutable bitfield type definition }} {{ texlong }}
-
-
-
-% also sugar [  nexp ] 
 
 type_union :: 'Tu_' ::=
   {{ com type union constructors }}
@@ -458,41 +402,31 @@ index_range :: 'BF_' ::= {{ com index specification, for bitfields in register t
   | num1 '..' num2 :: :: range {{ com index range }}
   | index_range1 , index_range2 :: :: concat {{ com concatenation of index ranges }}
 
-% 
-
-
-
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 % Literals                                                     %
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
-
-grammar
-
 lit :: 'L_' ::=
   {{ com literal constant }}
   {{ aux _ l }}
-  | ( )                                                 :: :: unit  {{ com $() : [[unit]]$ }}
-%Presumably we want to remove bitzero and bitone ?
-  | bitzero                                             :: :: zero {{ com $[[bitzero]] : [[bit]]$ }}
-  | bitone                                              :: :: one {{ com $[[bitone]] : [[bit]]$ }}
-  | true                                                :: :: true  {{ com $[[true]] : [[bool]]$ }}
-  | false                                               :: :: false {{ com $[[false]] : [[bool]]$ }}
-  | num                                         :: :: num  {{ com natural number constant }}
-  | hex                                         :: :: hex  {{ com bit vector constant, C-style }}
-  {{ com hex and bin are constant bit vectors, C-style }}
-  | bin                                         :: :: bin  {{ com bit vector constant, C-style }}
-% Should undefined be of type bit[alpha] or alpha[beta] or just alpha?
-  | string                                              :: :: string {{ com string constant }}
-  | undefined					:: :: undef {{ com undefined-value constant }}
-  | real :: :: real
-  
+  | ( )       :: :: unit
+  | bitzero   :: :: zero
+  | bitone    :: :: one
+  | true      :: :: true
+  | false     :: :: false
+  | num       :: :: num {{ com natural number constant }}
+  | hex       :: :: hex {{ com bit vector constant, C-style }}
+  | bin       :: :: bin  {{ com bit vector constant, C-style }}
+  | string    :: :: string {{ com string constant }}
+  | undefined :: :: undef {{ com undefined-value constant }}
+  | real      :: :: real
+
 semi_opt {{ tex \ottnt{;}^{?} }} :: 'semi_' ::=         {{ phantom }}
                                                         {{ ocaml bool }}
                                                         {{ lem bool }}
                                                         {{ hol bool }}
   {{ com optional semi-colon }}
-  |                                                     :: :: no  
+  |                                                     :: :: no
     {{ hol F }}
     {{ ocaml false }}
     {{ lem false }}
@@ -501,7 +435,6 @@ semi_opt {{ tex \ottnt{;}^{?} }} :: 'semi_' ::=         {{ phantom }}
     {{ ocaml true }}
     {{ lem true }}
 
-
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 % Patterns                                                     %
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -513,32 +446,26 @@ typ_pat :: 'TP_' ::=
   | kid                             :: :: var
   | id ( typ_pat1 , .. , typ_patn ) :: :: app
 
-
-
-pat :: 'P_' ::= 
+pat :: 'P_' ::=
   {{ com pattern }}
   {{ aux _ annot }} {{ auxparam 'a }}
-  | lit                                                 :: :: lit
+  | lit                                     :: :: lit
     {{ com literal constant pattern }}
-  | _                                                   :: :: wild  
+  | _                                       :: :: wild
     {{ com wildcard }}
-  | pat1 | pat2                                         :: :: or
+  | pat1 | pat2                             :: :: or
     {{ com pattern disjunction }}
-  | ~ pat                                               :: :: not
+  | ~ pat                                   :: :: not
     {{ com pattern negation }}
-  | ( pat as id )                                      :: :: as
+  | ( pat as id )                           :: :: as
     {{ com named pattern }}
-% ML-style
-%  | ( pat : typ )                                       :: :: typ
-%    {{ com Typed patterns }}
-% C-style
-  | ( typ ) pat                                       :: :: typ
+  | ( typ ) pat                             :: :: typ
     {{ com typed pattern }}
   | id                                      :: :: id
     {{ com identifier  }}
   | pat typ_pat :: :: var
     {{ com bind pattern to type variable }}
-  | id ( pat1 , .. , patn )                                     :: :: app
+  | id ( pat1 , .. , patn )                 :: :: app
     {{ com union constructor pattern }}
 
 % OR?  do we invent something ghastly including a union keyword?  Perhaps not...
@@ -813,29 +740,10 @@ exp :: 'E_' ::=
   | value :: I :: internal_value {{ com For internal use in interpreter to wrap pre-evaluated values when returning an action }}
   | constraint n_constraint :: :: constraint
 
-%i_direction :: 'I' ::=
-%  | IInc :: :: Inc
-%  | IDec :: :: Dec
-
-%ctor_kind :: 'C_' ::=
-%  | C_Enum nat :: :: Enum
-%  | C_Union    :: :: Union
-
-%reg_form :: 'Form_' ::=
-%  | Reg id tannot i_direction :: :: Reg
-%  | SubReg id reg_form index_range :: :: SubReg
-
-%reg_form_set :: '' ::= {{ phantom }} {{ lem set reg_form }}
-
-%alias_spec_tannot :: '' ::= {{ phantom }} {{ lem alias_spec tannot }} {{ ocaml tannot alias_spec }}
-
-
 lexp :: 'LEXP_' ::= {{ com lvalue expression }}
     {{ aux _ annot }} {{ auxparam 'a }}
-    | id                                                  :: :: id
-%    | ref id                                              :: :: ref
+    | id                                                  :: :: id {{ com identifier }}
     | deref exp                                           :: :: deref
-    {{ com identifier }}
     | id ( exp1 , .. , expn )				  :: :: memory {{ com memory or register write via function call }}
     | id exp	       	    				  :: S :: mem_tup {{ ichlo [[id (exp)]] }}
 {{ com sugared form of above for explicit tuple $[[exp]]$ }}
@@ -843,11 +751,9 @@ lexp :: 'LEXP_' ::= {{ com lvalue expression }}
 {{ com cast }}
     | ( lexp0 , .. , lexpn )                              :: :: tup {{ com multiple (non-memory) assignment }}
     | lexp1 @ ... @ lexpn                                 :: :: vector_concat {{ com vector concatenation L-exp }}
-    | lexp [ exp ]  :: ::                                 vector  {{ com vector element }}
-    | lexp [ exp1 '..' exp2 ]  :: ::                         vector_range {{ com subvector }}
-    % maybe comma-sep such lists too
-    | lexp . id :: :: field                        {{ com struct field }}
-
+    | lexp [ exp ]                                        :: :: vector  {{ com vector element }}
+    | lexp [ exp1 '..' exp2 ]                             :: :: vector_range {{ com subvector }}
+    | lexp . id                                           :: :: field {{ com struct field }}
 
 fexp :: 'FE_' ::=
   {{ com field expression }}
@@ -1052,14 +958,6 @@ default_spec :: 'DT_' ::=
   {{ com default kinding or typing assumption }}
   {{ aux _ l }}
   | default Order order      :: :: order
-  | default base_kind kid    :: :: kind
-  | default typschm id      :: :: typ
-% The intended semantics of these is that if an id in binding position
-% doesn't have a kind or type annotation, then we look through the
-% default regexps (in order from the beginning) and pick the first
-% assumption for which id matches the regexp, if there is one.
-% Otherwise we try to infer.  Perhaps warn if there are multiple matches.
-% For example, we might often have default Type ['alphanum]
 
 scattered_def :: 'SD_' ::=
   {{ com scattered function and union type definitions }}
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