Merge branch 'master' of bitbucket.org:Peter_Sewell/sail

Conflicts:
	language/manual.pdf

52 files changed, 3962 insertions, 427 deletions

diff --git a/src/LICENCE b/src/LICENCE
new file mode 100644
index 00000000..5992fbfc
--- /dev/null
+++ b/src/LICENCE
@@ -0,0 +1,39 @@
+   Sail
+
+Copyright (c) 2013-2017 
+  Kathyrn Gray
+  Shaked Flur
+  Stephen Kell
+  Gabriel Kerneis
+  Robert Norton-Wright
+  Christopher Pulte
+  Peter Sewell
+
+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.
diff --git a/src/Makefile b/src/Makefile
index 7927f9bc..9b8b727d 100644
--- a/src/Makefile
+++ b/src/Makefile
@@ -1,3 +1,45 @@
+##########################################################################
+#     Sail                                                               #
+#                                                                        #
+#  Copyright (c) 2013-2017                                               #
+#    Kathyrn Gray                                                        #
+#    Shaked Flur                                                         #
+#    Stephen Kell                                                        #
+#    Gabriel Kerneis                                                     #
+#    Robert Norton-Wright                                                #
+#    Christopher Pulte                                                   #
+#    Peter Sewell                                                        #
+#                                                                        #
+#  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.                                                          #
+##########################################################################
+
 .PHONY: all sail test clean doc lib power test_power test_idempotence
 
 all: sail lib doc
@@ -39,10 +81,10 @@ MIPS_NOTLB_SAILS:=$(MIPS_NOTLB_SAILS_PRE) $(BITBUCKET_ROOT)/sail/etc/regfp.sail
 
 CHERI_SAIL_DIR:=$(BITBUCKET_ROOT)/sail/cheri
 
-CHERI_NOTLB_SAILS:=$(MIPS_SAIL_DIR)/mips_prelude.sail $(MIPS_SAIL_DIR)/mips_tlb_stub.sail $(CHERI_SAIL_DIR)/cheri_prelude_256.sail $(CHERI_SAIL_DIR)/cheri_prelude_common.sail $(MIPS_SAIL_DIR)/mips_insts.sail $(CHERI_SAIL_DIR)/cheri_insts.sail $(MIPS_SAIL_DIR)/mips_ri.sail $(MIPS_SAIL_DIR)/mips_epilogue.sail
-CHERI_SAILS:=$(MIPS_SAIL_DIR)/mips_prelude.sail $(MIPS_SAIL_DIR)/mips_tlb.sail $(CHERI_SAIL_DIR)/cheri_prelude_256.sail $(CHERI_SAIL_DIR)/cheri_prelude_common.sail $(MIPS_SAIL_DIR)/mips_insts.sail $(CHERI_SAIL_DIR)/cheri_insts.sail $(MIPS_SAIL_DIR)/mips_ri.sail $(MIPS_SAIL_DIR)/mips_epilogue.sail
+CHERI_NOTLB_SAILS:=$(MIPS_SAIL_DIR)/mips_prelude.sail $(MIPS_SAIL_DIR)/mips_tlb_stub.sail $(CHERI_SAIL_DIR)/cheri_types.sail $(CHERI_SAIL_DIR)/cheri_prelude_256.sail $(CHERI_SAIL_DIR)/cheri_prelude_common.sail $(MIPS_SAIL_DIR)/mips_insts.sail $(CHERI_SAIL_DIR)/cheri_insts.sail $(MIPS_SAIL_DIR)/mips_ri.sail $(MIPS_SAIL_DIR)/mips_epilogue.sail
+CHERI_SAILS:=$(MIPS_SAIL_DIR)/mips_prelude.sail $(MIPS_SAIL_DIR)/mips_tlb.sail $(CHERI_SAIL_DIR)/cheri_types.sail $(CHERI_SAIL_DIR)/cheri_prelude_256.sail $(CHERI_SAIL_DIR)/cheri_prelude_common.sail $(MIPS_SAIL_DIR)/mips_insts.sail $(CHERI_SAIL_DIR)/cheri_insts.sail $(MIPS_SAIL_DIR)/mips_ri.sail $(MIPS_SAIL_DIR)/mips_epilogue.sail
 
-CHERI128_SAILS:=$(MIPS_SAIL_DIR)/mips_prelude.sail $(MIPS_SAIL_DIR)/mips_tlb.sail $(CHERI_SAIL_DIR)/cheri_prelude_128.sail $(CHERI_SAIL_DIR)/cheri_prelude_common.sail $(MIPS_SAIL_DIR)/mips_insts.sail $(CHERI_SAIL_DIR)/cheri_insts.sail $(MIPS_SAIL_DIR)/mips_ri.sail $(MIPS_SAIL_DIR)/mips_epilogue.sail
+CHERI128_SAILS:=$(MIPS_SAIL_DIR)/mips_prelude.sail $(MIPS_SAIL_DIR)/mips_tlb.sail $(CHERI_SAIL_DIR)/cheri_types.sail  $(CHERI_SAIL_DIR)/cheri_prelude_128.sail $(CHERI_SAIL_DIR)/cheri_prelude_common.sail $(MIPS_SAIL_DIR)/mips_insts.sail $(CHERI_SAIL_DIR)/cheri_insts.sail $(MIPS_SAIL_DIR)/mips_ri.sail $(MIPS_SAIL_DIR)/mips_epilogue.sail
 
 elf:
 	make -C $(ELFDIR)
diff --git a/src/Makefile-non-opam b/src/Makefile-non-opam
index 11f510fe..18fe6aa4 100644
--- a/src/Makefile-non-opam
+++ b/src/Makefile-non-opam
@@ -1,3 +1,45 @@
+##########################################################################
+#     Sail                                                               #
+#                                                                        #
+#  Copyright (c) 2013-2017                                               #
+#    Kathyrn Gray                                                        #
+#    Shaked Flur                                                         #
+#    Stephen Kell                                                        #
+#    Gabriel Kerneis                                                     #
+#    Robert Norton-Wright                                                #
+#    Christopher Pulte                                                   #
+#    Peter Sewell                                                        #
+#                                                                        #
+#  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.                                                          #
+##########################################################################
+
 THIS_MAKEFILE := $(lastword $(MAKEFILE_LIST))
 # NOTE: it matters that this path is *not* canonicalised (realpath'd).
 # If we realpath it, the ocaml deps files will include realpaths, and
diff --git a/src/ast.ml b/src/ast.ml
index 8bf3b60c..5eb45554 120000..100644
--- a/src/ast.ml
+++ b/src/ast.ml
@@ -1 +1,581 @@
-../language/l2.ml
\ No newline at end of file
+(**************************************************************************)
+(*     Sail                                                               *)
+(*                                                                        *)
+(*  Copyright (c) 2013-2017                                               *)
+(*    Kathyrn Gray                                                        *)
+(*    Shaked Flur                                                         *)
+(*    Stephen Kell                                                        *)
+(*    Gabriel Kerneis                                                     *)
+(*    Robert Norton-Wright                                                *)
+(*    Christopher Pulte                                                   *)
+(*    Peter Sewell                                                        *)
+(*                                                                        *)
+(*  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.                                                          *)
+(**************************************************************************)
+
+(* generated by Ott 0.25 from: l2.ott *)
+
+
+type text = string
+
+type l = Parse_ast.l
+
+type 'a annot = l * 'a
+
+
+type x = text (* identifier *)
+type ix = text (* infix identifier *)
+
+type 
+base_kind_aux =  (* base kind *)
+   BK_type (* kind of types *)
+ | BK_nat (* kind of natural number size expressions *)
+ | BK_order (* kind of vector order specifications *)
+ | BK_effect (* kind of effect sets *)
+
+
+type 
+base_kind = 
+   BK_aux of base_kind_aux * l
+
+
+type 
+id_aux =  (* Identifier *)
+   Id of x
+ | DeIid of x (* remove infix status *)
+
+
+type 
+kid_aux =  (* variables with kind, ticked to differntiate from program variables *)
+   Var of x
+
+
+type 
+kind_aux =  (* kinds *)
+   K_kind of (base_kind) list
+
+
+type 
+id = 
+   Id_aux of id_aux * l
+
+
+type 
+kid = 
+   Kid_aux of kid_aux * l
+
+
+type 
+kind = 
+   K_aux of kind_aux * l
+
+
+type 
+nexp_aux =  (* expression of kind Nat, for vector sizes and origins *)
+   Nexp_id of id (* identifier, bound by def Nat x = nexp *)
+ | Nexp_var of kid (* variable *)
+ | Nexp_constant of int (* constant *)
+ | Nexp_times of nexp * nexp (* product *)
+ | Nexp_sum of nexp * nexp (* sum *)
+ | Nexp_minus of nexp * nexp (* subtraction *)
+ | Nexp_exp of nexp (* exponential *)
+ | Nexp_neg of nexp (* For internal use *)
+
+and nexp = 
+   Nexp_aux of nexp_aux * l
+
+
+type 
+base_effect_aux =  (* effect *)
+   BE_rreg (* read register *)
+ | BE_wreg (* write register *)
+ | BE_rmem (* read memory *)
+ | BE_wmem (* write memory *)
+ | BE_eamem (* signal effective address for writing memory *)
+ | BE_wmv (* write memory, sending only value *)
+ | BE_barr (* memory barrier *)
+ | BE_depend (* dynamic footprint *)
+ | BE_undef (* undefined-instruction exception *)
+ | BE_unspec (* unspecified values *)
+ | BE_nondet (* nondeterminism from intra-instruction parallelism *)
+ | BE_escape (* Tracking of expressions and functions that might call exit *)
+ | BE_lset (* Local mutation happend; not user-writable *)
+ | BE_lret (* Local return happened; not user-writable *)
+
+
+type 
+base_effect = 
+   BE_aux of base_effect_aux * l
+
+
+type 
+order_aux =  (* vector order specifications, of kind Order *)
+   Ord_var of kid (* variable *)
+ | Ord_inc (* increasing (little-endian) *)
+ | Ord_dec (* decreasing (big-endian) *)
+
+
+type 
+effect_aux =  (* effect set, of kind Effects *)
+   Effect_var of kid
+ | Effect_set of (base_effect) list (* effect set *)
+
+
+type 
+order = 
+   Ord_aux of order_aux * l
+
+
+type 
+effect = 
+   Effect_aux of effect_aux * l
+
+
+type 
+kinded_id_aux =  (* optionally kind-annotated identifier *)
+   KOpt_none of kid (* identifier *)
+ | KOpt_kind of kind * kid (* kind-annotated variable *)
+
+
+type 
+n_constraint_aux =  (* constraint over kind $_$ *)
+   NC_fixed of nexp * nexp
+ | NC_bounded_ge of nexp * nexp
+ | NC_bounded_le of nexp * nexp
+ | NC_nat_set_bounded of kid * (int) list
+
+
+type 
+kinded_id = 
+   KOpt_aux of kinded_id_aux * l
+
+
+type 
+n_constraint = 
+   NC_aux of n_constraint_aux * l
+
+
+type 
+quant_item_aux =  (* Either a kinded identifier or a nexp constraint for a typquant *)
+   QI_id of kinded_id (* An optionally kinded identifier *)
+ | QI_const of n_constraint (* A constraint for this type *)
+
+
+type 
+quant_item = 
+   QI_aux of quant_item_aux * l
+
+
+type 
+typquant_aux =  (* type quantifiers and constraints *)
+   TypQ_tq of (quant_item) list
+ | TypQ_no_forall (* sugar, omitting quantifier and constraints *)
+
+
+type 
+lit_aux =  (* Literal constant *)
+   L_unit (* $() : _$ *)
+ | L_zero (* $_ : _$ *)
+ | L_one (* $_ : _$ *)
+ | L_true (* $_ : _$ *)
+ | L_false (* $_ : _$ *)
+ | L_num of int (* natural number constant *)
+ | L_hex of string (* bit vector constant, C-style *)
+ | L_bin of string (* bit vector constant, C-style *)
+ | L_undef (* constant representing undefined values *)
+ | L_string of string (* string constant *)
+
+
+type 
+typquant = 
+   TypQ_aux of typquant_aux * l
+
+
+type 
+typ_aux =  (* Type expressions, of kind $_$ *)
+   Typ_wild (* Unspecified type *)
+ | Typ_id of id (* Defined type *)
+ | Typ_var of kid (* Type variable *)
+ | Typ_fn of typ * typ * effect (* Function type (first-order only in user code) *)
+ | Typ_tup of (typ) list (* Tuple type *)
+ | Typ_app of id * (typ_arg) list (* type constructor application *)
+
+and typ = 
+   Typ_aux of typ_aux * l
+
+and typ_arg_aux =  (* Type constructor arguments of all kinds *)
+   Typ_arg_nexp of nexp
+ | Typ_arg_typ of typ
+ | Typ_arg_order of order
+ | Typ_arg_effect of effect
+
+and typ_arg = 
+   Typ_arg_aux of typ_arg_aux * l
+
+
+type 
+lit = 
+   L_aux of lit_aux * l
+
+
+type 
+typschm_aux =  (* type scheme *)
+   TypSchm_ts of typquant * typ
+
+
+type 
+'a pat_aux =  (* Pattern *)
+   P_lit of lit (* literal constant pattern *)
+ | P_wild (* wildcard *)
+ | P_as of 'a pat * id (* named pattern *)
+ | P_typ of typ * 'a pat (* typed pattern *)
+ | P_id of id (* identifier *)
+ | P_app of id * ('a pat) list (* union constructor pattern *)
+ | P_record of ('a fpat) list * bool (* struct pattern *)
+ | P_vector of ('a pat) list (* vector pattern *)
+ | P_vector_indexed of ((int * 'a pat)) list (* vector pattern (with explicit indices) *)
+ | P_vector_concat of ('a pat) list (* concatenated vector pattern *)
+ | P_tup of ('a pat) list (* tuple pattern *)
+ | P_list of ('a pat) list (* list pattern *)
+
+and 'a pat = 
+   P_aux of 'a pat_aux * 'a annot
+
+and 'a fpat_aux =  (* Field pattern *)
+   FP_Fpat of id * 'a pat
+
+and 'a fpat = 
+   FP_aux of 'a fpat_aux * 'a annot
+
+
+type 
+typschm = 
+   TypSchm_aux of typschm_aux * l
+
+
+type 
+'a reg_id_aux = 
+   RI_id of id
+
+
+type 
+'a exp_aux =  (* Expression *)
+   E_block of ('a exp) list (* block *)
+ | E_nondet of ('a exp) list (* nondeterminisitic block, expressions evaluate in an unspecified order, or concurrently *)
+ | E_id of id (* identifier *)
+ | E_lit of lit (* literal constant *)
+ | E_cast of typ * 'a exp (* cast *)
+ | E_app of id * ('a exp) list (* function application *)
+ | E_app_infix of 'a exp * id * 'a exp (* infix function application *)
+ | E_tuple of ('a exp) list (* tuple *)
+ | E_if of 'a exp * 'a exp * 'a exp (* conditional *)
+ | E_for of id * 'a exp * 'a exp * 'a exp * order * 'a exp (* loop *)
+ | E_vector of ('a exp) list (* vector (indexed from 0) *)
+ | E_vector_indexed of ((int * 'a exp)) list * 'a opt_default (* vector (indexed consecutively) *)
+ | E_vector_access of 'a exp * 'a exp (* vector access *)
+ | E_vector_subrange of 'a exp * 'a exp * 'a exp (* subvector extraction *)
+ | E_vector_update of 'a exp * 'a exp * 'a exp (* vector functional update *)
+ | E_vector_update_subrange of 'a exp * 'a exp * 'a exp * 'a exp (* vector subrange update (with vector) *)
+ | E_vector_append of 'a exp * 'a exp (* vector concatenation *)
+ | E_list of ('a exp) list (* list *)
+ | E_cons of 'a exp * 'a exp (* cons *)
+ | E_record of 'a fexps (* struct *)
+ | E_record_update of 'a exp * 'a fexps (* functional update of struct *)
+ | E_field of 'a exp * id (* field projection from struct *)
+ | E_case of 'a exp * ('a pexp) list (* pattern matching *)
+ | E_let of 'a letbind * 'a exp (* let expression *)
+ | E_assign of 'a lexp * 'a exp (* imperative assignment *)
+ | E_sizeof of nexp (* Expression to return the value of the nexp variable or expression at run time *)
+ | E_exit of 'a exp (* expression to halt all current execution, potentially calling a system, trap, or interrupt handler with exp *)
+ | E_return of 'a exp (* expression to end current function execution and return the value of exp from the function; this can be used to break out of for loops *)
+ | E_assert of 'a exp * 'a exp (* expression to halt with error, when the first expression is false, reporting the optional string as an error *)
+ | E_internal_cast of 'a annot * 'a exp (* This is an internal cast, generated during type checking that will resolve into a syntactic cast after *)
+ | E_internal_exp of 'a annot (* This is an internal use for passing nexp information  to library functions, postponed for constraint solving *)
+ | E_sizeof_internal of 'a annot (* For sizeof during type checking, to replace nexp with internal n *)
+ | E_internal_exp_user of 'a annot * 'a annot (* This is like the above but the user has specified an implicit parameter for the current function *)
+ | E_comment of string (* For generated unstructured comments *)
+ | E_comment_struc of 'a exp (* For generated structured comments *)
+ | E_internal_let of 'a lexp * 'a exp * 'a exp (* This is an internal node for compilation that demonstrates the scope of a local mutable variable *)
+ | E_internal_plet of 'a pat * 'a exp * 'a exp (* This is an internal node, used to distinguised some introduced lets during processing from original ones *)
+ | E_internal_return of 'a exp (* For internal use to embed into monad definition *)
+
+and 'a exp = 
+   E_aux of 'a exp_aux * 'a annot
+
+and 'a lexp_aux =  (* lvalue expression *)
+   LEXP_id of id (* identifier *)
+ | LEXP_memory of id * ('a exp) list (* memory write via function call *)
+ | LEXP_cast of typ * id
+ | LEXP_tup of ('a lexp) list (* set multiple at a time, a check will ensure it's not memory *)
+ | LEXP_vector of 'a lexp * 'a exp (* vector element *)
+ | LEXP_vector_range of 'a lexp * 'a exp * 'a exp (* subvector *)
+ | LEXP_field of 'a lexp * id (* struct field *)
+
+and 'a lexp = 
+   LEXP_aux of 'a lexp_aux * 'a annot
+
+and 'a fexp_aux =  (* Field-expression *)
+   FE_Fexp of id * 'a exp
+
+and 'a fexp = 
+   FE_aux of 'a fexp_aux * 'a annot
+
+and 'a fexps_aux =  (* Field-expression list *)
+   FES_Fexps of ('a fexp) list * bool
+
+and 'a fexps = 
+   FES_aux of 'a fexps_aux * 'a annot
+
+and 'a opt_default_aux =  (* Optional default value for indexed vectors, to define a defualt value for any unspecified positions in a sparse map *)
+   Def_val_empty
+ | Def_val_dec of 'a exp
+
+and 'a opt_default = 
+   Def_val_aux of 'a opt_default_aux * 'a annot
+
+and 'a pexp_aux =  (* Pattern match *)
+   Pat_exp of 'a pat * 'a exp
+
+and 'a pexp = 
+   Pat_aux of 'a pexp_aux * 'a annot
+
+and 'a letbind_aux =  (* Let binding *)
+   LB_val_explicit of typschm * 'a pat * 'a exp (* value binding, explicit type ('a pat must be total) *)
+ | LB_val_implicit of 'a pat * 'a exp (* value binding, implicit type ('a pat must be total) *)
+
+and 'a letbind = 
+   LB_aux of 'a letbind_aux * 'a annot
+
+
+type 
+'a reg_id = 
+   RI_aux of 'a reg_id_aux * 'a annot
+
+
+type 
+type_union_aux =  (* Type union constructors *)
+   Tu_id of id
+ | Tu_ty_id of typ * id
+
+
+type 
+name_scm_opt_aux =  (* Optional variable-naming-scheme specification for variables of defined type *)
+   Name_sect_none
+ | Name_sect_some of string
+
+
+type 
+effect_opt_aux =  (* Optional effect annotation for functions *)
+   Effect_opt_pure (* sugar for empty effect set *)
+ | Effect_opt_effect of effect
+
+
+type 
+'a funcl_aux =  (* Function clause *)
+   FCL_Funcl of id * 'a pat * 'a exp
+
+
+type 
+rec_opt_aux =  (* Optional recursive annotation for functions *)
+   Rec_nonrec (* non-recursive *)
+ | Rec_rec (* recursive *)
+
+
+type 
+tannot_opt_aux =  (* Optional type annotation for functions *)
+   Typ_annot_opt_some of typquant * typ
+
+
+type 
+'a alias_spec_aux =  (* Register alias expression forms. Other than where noted, each id must refer to an unaliased register of type vector *)
+   AL_subreg of 'a reg_id * id
+ | AL_bit of 'a reg_id * 'a exp
+ | AL_slice of 'a reg_id * 'a exp * 'a exp
+ | AL_concat of 'a reg_id * 'a reg_id
+
+
+type 
+type_union = 
+   Tu_aux of type_union_aux * l
+
+
+type 
+index_range_aux =  (* index specification, for bitfields in register types *)
+   BF_single of int (* single index *)
+ | BF_range of int * int (* index range *)
+ | BF_concat of index_range * index_range (* concatenation of index ranges *)
+
+and index_range = 
+   BF_aux of index_range_aux * l
+
+
+type 
+name_scm_opt = 
+   Name_sect_aux of name_scm_opt_aux * l
+
+
+type 
+effect_opt = 
+   Effect_opt_aux of effect_opt_aux * l
+
+
+type 
+'a funcl = 
+   FCL_aux of 'a funcl_aux * 'a annot
+
+
+type 
+rec_opt = 
+   Rec_aux of rec_opt_aux * l
+
+
+type 
+tannot_opt = 
+   Typ_annot_opt_aux of tannot_opt_aux * l
+
+
+type 
+'a alias_spec = 
+   AL_aux of 'a alias_spec_aux * 'a annot
+
+
+type 
+'a default_spec_aux =  (* Default kinding or typing assumption *)
+   DT_kind of base_kind * kid
+ | DT_order of order
+ | DT_typ of typschm * id
+
+
+type 
+'a type_def_aux =  (* Type definition body *)
+   TD_abbrev of id * name_scm_opt * typschm (* type abbreviation *)
+ | TD_record of id * name_scm_opt * typquant * ((typ * id)) list * bool (* struct type definition *)
+ | TD_variant of id * name_scm_opt * typquant * (type_union) list * bool (* union type definition *)
+ | TD_enum of id * name_scm_opt * (id) list * bool (* enumeration type definition *)
+ | TD_register of id * nexp * nexp * ((index_range * id)) list (* register mutable bitfield type definition *)
+
+
+type 
+'a val_spec_aux =  (* Value type specification *)
+   VS_val_spec of typschm * id
+ | VS_extern_no_rename of typschm * id
+ | VS_extern_spec of typschm * id * string (* Specify the type and id of a function from Lem, where the string must provide an explicit path to the required function but will not be checked *)
+
+
+type 
+'a kind_def_aux =  (* Definition body for elements of kind; many are shorthands for type\_defs *)
+   KD_nabbrev of kind * id * name_scm_opt * nexp (* nexp abbreviation *)
+ | KD_abbrev of kind * id * name_scm_opt * typschm (* type abbreviation *)
+ | KD_record of kind * id * name_scm_opt * typquant * ((typ * id)) list * bool (* struct type definition *)
+ | KD_variant of kind * id * name_scm_opt * typquant * (type_union) list * bool (* union type definition *)
+ | KD_enum of kind * id * name_scm_opt * (id) list * bool (* enumeration type definition *)
+ | KD_register of kind * id * nexp * nexp * ((index_range * id)) list (* register mutable bitfield type definition *)
+
+
+type 
+'a scattered_def_aux =  (* Function and type union definitions that can be spread across
+         a file. Each one must end in $_$ *)
+   SD_scattered_function of rec_opt * tannot_opt * effect_opt * id (* scattered function definition header *)
+ | SD_scattered_funcl of 'a funcl (* scattered function definition clause *)
+ | SD_scattered_variant of id * name_scm_opt * typquant (* scattered union definition header *)
+ | SD_scattered_unioncl of id * type_union (* scattered union definition member *)
+ | SD_scattered_end of id (* scattered definition end *)
+
+
+type 
+'a fundef_aux =  (* Function definition *)
+   FD_function of rec_opt * tannot_opt * effect_opt * ('a funcl) list
+
+
+type 
+'a dec_spec_aux =  (* Register declarations *)
+   DEC_reg of typ * id
+ | DEC_alias of id * 'a alias_spec
+ | DEC_typ_alias of typ * id * 'a alias_spec
+
+
+type 
+'a default_spec = 
+   DT_aux of 'a default_spec_aux * l
+
+
+type 
+'a type_def = 
+   TD_aux of 'a type_def_aux * 'a annot
+
+
+type 
+'a val_spec = 
+   VS_aux of 'a val_spec_aux * 'a annot
+
+
+type 
+'a kind_def = 
+   KD_aux of 'a kind_def_aux * 'a annot
+
+
+type 
+'a scattered_def = 
+   SD_aux of 'a scattered_def_aux * 'a annot
+
+
+type 
+'a fundef = 
+   FD_aux of 'a fundef_aux * 'a annot
+
+
+type 
+'a dec_spec = 
+   DEC_aux of 'a dec_spec_aux * 'a annot
+
+
+type 
+'a dec_comm =  (* Top-level generated comments *)
+   DC_comm of string (* generated unstructured comment *)
+ | DC_comm_struct of 'a def (* generated structured comment *)
+
+and 'a def =  (* Top-level definition *)
+   DEF_kind of 'a kind_def (* definition of named kind identifiers *)
+ | DEF_type of 'a type_def (* type definition *)
+ | DEF_fundef of 'a fundef (* function definition *)
+ | DEF_val of 'a letbind (* value definition *)
+ | DEF_spec of 'a val_spec (* top-level type constraint *)
+ | DEF_default of 'a default_spec (* default kind and type assumptions *)
+ | DEF_scattered of 'a scattered_def (* scattered function and type definition *)
+ | DEF_reg_dec of 'a dec_spec (* register declaration *)
+ | DEF_comm of 'a dec_comm (* generated comments *)
+
+
+type 
+'a defs =  (* Definition sequence *)
+   Defs of ('a def) list
+
+
+
diff --git a/src/finite_map.ml b/src/finite_map.ml
index 78925e37..411048b6 100644
--- a/src/finite_map.ml
+++ b/src/finite_map.ml
@@ -1,4 +1,47 @@
 (**************************************************************************)
+(*     Sail                                                               *)
+(*                                                                        *)
+(*  Copyright (c) 2013-2017                                               *)
+(*    Kathyrn Gray                                                        *)
+(*    Shaked Flur                                                         *)
+(*    Stephen Kell                                                        *)
+(*    Gabriel Kerneis                                                     *)
+(*    Robert Norton-Wright                                                *)
+(*    Christopher Pulte                                                   *)
+(*    Peter Sewell                                                        *)
+(*                                                                        *)
+(*  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.                                                          *)
+(**************************************************************************)
+
+
+(**************************************************************************)
 (*                        Lem                                             *)
 (*                                                                        *)
 (*          Dominic Mulligan, University of Cambridge                     *)
@@ -44,6 +87,7 @@
 (*  IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.                         *)
 (**************************************************************************)
 
+
 (** finite map library *)
 
 module type Fmap = sig
diff --git a/src/initial_check.ml b/src/initial_check.ml
index 5b813c04..82cc6b7c 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -1,3 +1,45 @@
+(**************************************************************************)
+(*     Sail                                                               *)
+(*                                                                        *)
+(*  Copyright (c) 2013-2017                                               *)
+(*    Kathyrn Gray                                                        *)
+(*    Shaked Flur                                                         *)
+(*    Stephen Kell                                                        *)
+(*    Gabriel Kerneis                                                     *)
+(*    Robert Norton-Wright                                                *)
+(*    Christopher Pulte                                                   *)
+(*    Peter Sewell                                                        *)
+(*                                                                        *)
+(*  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 Type_internal
 open Ast
 
diff --git a/src/initial_check.mli b/src/initial_check.mli
index 14108e08..5e4b7e77 100644
--- a/src/initial_check.mli
+++ b/src/initial_check.mli
@@ -1,3 +1,44 @@
+(**************************************************************************)
+(*     Sail                                                               *)
+(*                                                                        *)
+(*  Copyright (c) 2013-2017                                               *)
+(*    Kathyrn Gray                                                        *)
+(*    Shaked Flur                                                         *)
+(*    Stephen Kell                                                        *)
+(*    Gabriel Kerneis                                                     *)
+(*    Robert Norton-Wright                                                *)
+(*    Christopher Pulte                                                   *)
+(*    Peter Sewell                                                        *)
+(*                                                                        *)
+(*  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 Ast
 open Type_internal
diff --git a/src/initial_check_full_ast.ml b/src/initial_check_full_ast.ml
index 562d778e..b2781350 100644
--- a/src/initial_check_full_ast.ml
+++ b/src/initial_check_full_ast.ml
@@ -1,3 +1,45 @@
+(**************************************************************************)
+(*     Sail                                                               *)
+(*                                                                        *)
+(*  Copyright (c) 2013-2017                                               *)
+(*    Kathyrn Gray                                                        *)
+(*    Shaked Flur                                                         *)
+(*    Stephen Kell                                                        *)
+(*    Gabriel Kerneis                                                     *)
+(*    Robert Norton-Wright                                                *)
+(*    Christopher Pulte                                                   *)
+(*    Peter Sewell                                                        *)
+(*                                                                        *)
+(*  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 Type_internal
 open Ast
 open Type_internal
diff --git a/src/initial_check_full_ast.mli b/src/initial_check_full_ast.mli
index 57346dcf..be612532 100644
--- a/src/initial_check_full_ast.mli
+++ b/src/initial_check_full_ast.mli
@@ -1,3 +1,44 @@
+(**************************************************************************)
+(*     Sail                                                               *)
+(*                                                                        *)
+(*  Copyright (c) 2013-2017                                               *)
+(*    Kathyrn Gray                                                        *)
+(*    Shaked Flur                                                         *)
+(*    Stephen Kell                                                        *)
+(*    Gabriel Kerneis                                                     *)
+(*    Robert Norton-Wright                                                *)
+(*    Christopher Pulte                                                   *)
+(*    Peter Sewell                                                        *)
+(*                                                                        *)
+(*  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 Ast
 open Type_internal
diff --git a/src/lem_interp/instruction_extractor.lem b/src/lem_interp/instruction_extractor.lem
index 074f3bc4..e603bb58 100644
--- a/src/lem_interp/instruction_extractor.lem
+++ b/src/lem_interp/instruction_extractor.lem
@@ -1,3 +1,45 @@
+(*========================================================================*)
+(*     Sail                                                               *)
+(*                                                                        *)
+(*  Copyright (c) 2013-2017                                               *)
+(*    Kathyrn Gray                                                        *)
+(*    Shaked Flur                                                         *)
+(*    Stephen Kell                                                        *)
+(*    Gabriel Kerneis                                                     *)
+(*    Robert Norton-Wright                                                *)
+(*    Christopher Pulte                                                   *)
+(*    Peter Sewell                                                        *)
+(*                                                                        *)
+(*  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 import Interp_ast
 open import Interp_utilities
 open import Pervasives
diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem
index 9072a3bd..543b7639 100644
--- a/src/lem_interp/interp.lem
+++ b/src/lem_interp/interp.lem
@@ -1,3 +1,45 @@
+(*========================================================================*)
+(*     Sail                                                               *)
+(*                                                                        *)
+(*  Copyright (c) 2013-2017                                               *)
+(*    Kathyrn Gray                                                        *)
+(*    Shaked Flur                                                         *)
+(*    Stephen Kell                                                        *)
+(*    Gabriel Kerneis                                                     *)
+(*    Robert Norton-Wright                                                *)
+(*    Christopher Pulte                                                   *)
+(*    Peter Sewell                                                        *)
+(*                                                                        *)
+(*  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 import Pervasives
 import Map
 import Map_extra (* For 'find' instead of using lookup and maybe types, as we know it cannot fail *)
diff --git a/src/lem_interp/interp_ast.lem b/src/lem_interp/interp_ast.lem
index 37719b1b..64fb14b2 120000..100644
--- a/src/lem_interp/interp_ast.lem
+++ b/src/lem_interp/interp_ast.lem
@@ -1 +1,711 @@
-../../language/l2.lem
\ No newline at end of file
+(*========================================================================*)
+(*     Sail                                                               *)
+(*                                                                        *)
+(*  Copyright (c) 2013-2017                                               *)
+(*    Kathyrn Gray                                                        *)
+(*    Shaked Flur                                                         *)
+(*    Stephen Kell                                                        *)
+(*    Gabriel Kerneis                                                     *)
+(*    Robert Norton-Wright                                                *)
+(*    Christopher Pulte                                                   *)
+(*    Peter Sewell                                                        *)
+(*                                                                        *)
+(*  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.                                                          *)
+(*========================================================================*)
+
+(* generated by Ott 0.25 from: l2_typ.ott l2.ott *)
+open import Pervasives
+
+open import Map
+open import Maybe
+open import Set_extra
+
+type l =
+  | Unknown
+  | Int of string * maybe l (*internal types, functions*)
+  | Range of string * nat * nat * nat * nat
+  | Generated of l (*location for a generated node, where l is the location of the closest original source*)
+
+type annot 'a = l * 'a
+
+val duplicates : forall 'a. list 'a -> list 'a
+
+val set_from_list : forall 'a. list 'a -> set 'a
+
+val subst : forall 'a. list 'a -> list 'a -> bool
+
+
+type x = string (* identifier *)
+type ix = string (* infix identifier *)
+
+type base_kind_aux =  (* base kind *)
+ | BK_type (* kind of types *)
+ | BK_nat (* kind of natural number size expressions *)
+ | BK_order (* kind of vector order specifications *)
+ | BK_effect (* kind of effect sets *)
+
+
+type base_kind = 
+ | BK_aux of base_kind_aux * l
+
+
+type kid_aux =  (* variables with kind, ticked to differntiate from program variables *)
+ | Var of x
+
+
+type id_aux =  (* Identifier *)
+ | Id of x
+ | DeIid of x (* remove infix status *)
+
+
+type kind_aux =  (* kinds *)
+ | K_kind of list base_kind
+
+
+type kid = 
+ | Kid_aux of kid_aux * l
+
+
+type id = 
+ | Id_aux of id_aux * l
+
+
+type kind = 
+ | K_aux of kind_aux * l
+
+
+type nexp_aux =  (* expression of kind Nat, for vector sizes and origins *)
+ | Nexp_id of id (* identifier, bound by def Nat x = nexp *)
+ | Nexp_var of kid (* variable *)
+ | Nexp_constant of integer (* constant *)
+ | Nexp_times of nexp * nexp (* product *)
+ | Nexp_sum of nexp * nexp (* sum *)
+ | Nexp_minus of nexp * nexp (* subtraction *)
+ | Nexp_exp of nexp (* exponential *)
+ | Nexp_neg of nexp (* For internal use *)
+
+and nexp = 
+ | Nexp_aux of nexp_aux * l
+
+
+type base_effect_aux =  (* effect *)
+ | BE_rreg (* read register *)
+ | BE_wreg (* write register *)
+ | BE_rmem (* read memory *)
+ | BE_wmem (* write memory *)
+ | BE_eamem (* signal effective address for writing memory *)
+ | BE_wmv (* write memory, sending only value *)
+ | BE_barr (* memory barrier *)
+ | BE_depend (* dynamic footprint *)
+ | BE_undef (* undefined-instruction exception *)
+ | BE_unspec (* unspecified values *)
+ | BE_nondet (* nondeterminism from intra-instruction parallelism *)
+ | BE_escape (* Tracking of expressions and functions that might call exit *)
+ | BE_lset (* Local mutation happend; not user-writable *)
+ | BE_lret (* Local return happened; not user-writable *)
+
+
+type base_effect = 
+ | BE_aux of base_effect_aux * l
+
+
+type order_aux =  (* vector order specifications, of kind Order *)
+ | Ord_var of kid (* variable *)
+ | Ord_inc (* increasing (little-endian) *)
+ | Ord_dec (* decreasing (big-endian) *)
+
+
+type effect_aux =  (* effect set, of kind Effects *)
+ | Effect_var of kid
+ | Effect_set of list base_effect (* effect set *)
+
+
+type order = 
+ | Ord_aux of order_aux * l
+
+
+type effect = 
+ | Effect_aux of effect_aux * l
+
+let effect_union e1 e2 = 
+  match (e1,e2) with
+  | ((Effect_aux (Effect_set els) _),(Effect_aux (Effect_set els2) l)) -> Effect_aux (Effect_set (els++els2)) l
+  end
+
+
+type kinded_id_aux =  (* optionally kind-annotated identifier *)
+ | KOpt_none of kid (* identifier *)
+ | KOpt_kind of kind * kid (* kind-annotated variable *)
+
+
+type n_constraint_aux =  (* constraint over kind $Nat$ *)
+ | NC_fixed of nexp * nexp
+ | NC_bounded_ge of nexp * nexp
+ | NC_bounded_le of nexp * nexp
+ | NC_nat_set_bounded of kid * list integer
+
+
+type kinded_id = 
+ | KOpt_aux of kinded_id_aux * l
+
+
+type n_constraint = 
+ | NC_aux of n_constraint_aux * l
+
+
+type quant_item_aux =  (* Either a kinded identifier or a nexp constraint for a typquant *)
+ | QI_id of kinded_id (* An optionally kinded identifier *)
+ | QI_const of n_constraint (* A constraint for this type *)
+
+
+type quant_item = 
+ | QI_aux of quant_item_aux * l
+
+
+type typquant_aux =  (* type quantifiers and constraints *)
+ | TypQ_tq of list quant_item
+ | TypQ_no_forall (* sugar, omitting quantifier and constraints *)
+
+
+type lit_aux =  (* Literal constant *)
+ | L_unit (* $() : unit$ *)
+ | L_zero (* $bitzero : bit$ *)
+ | L_one (* $bitone : bit$ *)
+ | L_true (* $true : bool$ *)
+ | L_false (* $false : bool$ *)
+ | L_num of integer (* natural number constant *)
+ | L_hex of string (* bit vector constant, C-style *)
+ | L_bin of string (* bit vector constant, C-style *)
+ | L_undef (* constant representing undefined values *)
+ | L_string of string (* string constant *)
+
+
+type typquant = 
+ | TypQ_aux of typquant_aux * l
+
+
+type typ_aux =  (* Type expressions, of kind $Type$ *)
+ | Typ_wild (* Unspecified type *)
+ | Typ_id of id (* Defined type *)
+ | Typ_var of kid (* Type variable *)
+ | Typ_fn of typ * typ * effect (* Function type (first-order only in user code) *)
+ | Typ_tup of list typ (* Tuple type *)
+ | Typ_app of id * list typ_arg (* type constructor application *)
+
+and typ = 
+ | Typ_aux of typ_aux * l
+
+and typ_arg_aux =  (* Type constructor arguments of all kinds *)
+ | Typ_arg_nexp of nexp
+ | Typ_arg_typ of typ
+ | Typ_arg_order of order
+ | Typ_arg_effect of effect
+
+and typ_arg = 
+ | Typ_arg_aux of typ_arg_aux * l
+
+
+type lit = 
+ | L_aux of lit_aux * l
+
+
+type typschm_aux =  (* type scheme *)
+ | TypSchm_ts of typquant * typ
+
+
+type pat_aux 'a =  (* Pattern *)
+ | P_lit of lit (* literal constant pattern *)
+ | P_wild (* wildcard *)
+ | P_as of (pat 'a) * id (* named pattern *)
+ | P_typ of typ * (pat 'a) (* typed pattern *)
+ | P_id of id (* identifier *)
+ | P_app of id * list (pat 'a) (* union constructor pattern *)
+ | P_record of list (fpat 'a) * bool (* struct pattern *)
+ | P_vector of list (pat 'a) (* vector pattern *)
+ | P_vector_indexed of list (integer * (pat 'a)) (* vector pattern (with explicit indices) *)
+ | P_vector_concat of list (pat 'a) (* concatenated vector pattern *)
+ | P_tup of list (pat 'a) (* tuple pattern *)
+ | P_list of list (pat 'a) (* list pattern *)
+
+and pat 'a = 
+ | P_aux of (pat_aux 'a) * annot 'a
+
+and fpat_aux 'a =  (* Field pattern *)
+ | FP_Fpat of id * (pat 'a)
+
+and fpat 'a = 
+ | FP_aux of (fpat_aux 'a) * annot 'a
+
+
+type typschm = 
+ | TypSchm_aux of typschm_aux * l
+
+
+type reg_id_aux 'a = 
+ | RI_id of id
+
+
+type exp_aux 'a =  (* Expression *)
+ | E_block of list (exp 'a) (* block *)
+ | E_nondet of list (exp 'a) (* nondeterminisitic block, expressions evaluate in an unspecified order, or concurrently *)
+ | E_id of id (* identifier *)
+ | E_lit of lit (* literal constant *)
+ | E_cast of typ * (exp 'a) (* cast *)
+ | E_app of id * list (exp 'a) (* function application *)
+ | E_app_infix of (exp 'a) * id * (exp 'a) (* infix function application *)
+ | E_tuple of list (exp 'a) (* tuple *)
+ | E_if of (exp 'a) * (exp 'a) * (exp 'a) (* conditional *)
+ | E_for of id * (exp 'a) * (exp 'a) * (exp 'a) * order * (exp 'a) (* loop *)
+ | E_vector of list (exp 'a) (* vector (indexed from 0) *)
+ | E_vector_indexed of list (integer * (exp 'a)) * (opt_default 'a) (* vector (indexed consecutively) *)
+ | E_vector_access of (exp 'a) * (exp 'a) (* vector access *)
+ | E_vector_subrange of (exp 'a) * (exp 'a) * (exp 'a) (* subvector extraction *)
+ | E_vector_update of (exp 'a) * (exp 'a) * (exp 'a) (* vector functional update *)
+ | E_vector_update_subrange of (exp 'a) * (exp 'a) * (exp 'a) * (exp 'a) (* vector subrange update (with vector) *)
+ | E_vector_append of (exp 'a) * (exp 'a) (* vector concatenation *)
+ | E_list of list (exp 'a) (* list *)
+ | E_cons of (exp 'a) * (exp 'a) (* cons *)
+ | E_record of (fexps 'a) (* struct *)
+ | E_record_update of (exp 'a) * (fexps 'a) (* functional update of struct *)
+ | E_field of (exp 'a) * id (* field projection from struct *)
+ | E_case of (exp 'a) * list (pexp 'a) (* pattern matching *)
+ | E_let of (letbind 'a) * (exp 'a) (* let expression *)
+ | E_assign of (lexp 'a) * (exp 'a) (* imperative assignment *)
+ | E_sizeof of nexp (* Expression to return the value of the nexp variable or expression at run time *)
+ | E_exit of (exp 'a) (* expression to halt all current execution, potentially calling a system, trap, or interrupt handler with exp *)
+ | E_return of (exp 'a) (* expression to end current function execution and return the value of exp from the function; this can be used to break out of for loops *)
+ | E_assert of (exp 'a) * (exp 'a) (* expression to halt with error, when the first expression is false, reporting the optional string as an error *)
+ | E_internal_cast of annot 'a * (exp 'a) (* This is an internal cast, generated during type checking that will resolve into a syntactic cast after *)
+ | E_internal_exp of annot 'a (* This is an internal use for passing nexp information  to library functions, postponed for constraint solving *)
+ | E_sizeof_internal of annot 'a (* For sizeof during type checking, to replace nexp with internal n *)
+ | E_internal_exp_user of annot 'a * annot 'a (* This is like the above but the user has specified an implicit parameter for the current function *)
+ | E_comment of string (* For generated unstructured comments *)
+ | E_comment_struc of (exp 'a) (* For generated structured comments *)
+ | E_internal_let of (lexp 'a) * (exp 'a) * (exp 'a) (* This is an internal node for compilation that demonstrates the scope of a local mutable variable *)
+ | E_internal_plet of (pat 'a) * (exp 'a) * (exp 'a) (* This is an internal node, used to distinguised some introduced lets during processing from original ones *)
+ | E_internal_return of (exp 'a) (* For internal use to embed into monad definition *)
+
+and exp 'a = 
+ | E_aux of (exp_aux 'a) * annot 'a
+
+and lexp_aux 'a =  (* lvalue expression *)
+ | LEXP_id of id (* identifier *)
+ | LEXP_memory of id * list (exp 'a) (* memory write via function call *)
+ | LEXP_cast of typ * id
+ | LEXP_tup of list (lexp 'a) (* set multiple at a time, a check will ensure it's not memory *)
+ | LEXP_vector of (lexp 'a) * (exp 'a) (* vector element *)
+ | LEXP_vector_range of (lexp 'a) * (exp 'a) * (exp 'a) (* subvector *)
+ | LEXP_field of (lexp 'a) * id (* struct field *)
+
+and lexp 'a = 
+ | LEXP_aux of (lexp_aux 'a) * annot 'a
+
+and fexp_aux 'a =  (* Field-expression *)
+ | FE_Fexp of id * (exp 'a)
+
+and fexp 'a = 
+ | FE_aux of (fexp_aux 'a) * annot 'a
+
+and fexps_aux 'a =  (* Field-expression list *)
+ | FES_Fexps of list (fexp 'a) * bool
+
+and fexps 'a = 
+ | FES_aux of (fexps_aux 'a) * annot 'a
+
+and opt_default_aux 'a =  (* Optional default value for indexed vectors, to define a defualt value for any unspecified positions in a sparse map *)
+ | Def_val_empty
+ | Def_val_dec of (exp 'a)
+
+and opt_default 'a = 
+ | Def_val_aux of (opt_default_aux 'a) * annot 'a
+
+and pexp_aux 'a =  (* Pattern match *)
+ | Pat_exp of (pat 'a) * (exp 'a)
+
+and pexp 'a = 
+ | Pat_aux of (pexp_aux 'a) * annot 'a
+
+and letbind_aux 'a =  (* Let binding *)
+ | LB_val_explicit of typschm * (pat 'a) * (exp 'a) (* value binding, explicit type ((pat 'a) must be total) *)
+ | LB_val_implicit of (pat 'a) * (exp 'a) (* value binding, implicit type ((pat 'a) must be total) *)
+
+and letbind 'a = 
+ | LB_aux of (letbind_aux 'a) * annot 'a
+
+
+type reg_id 'a = 
+ | RI_aux of (reg_id_aux 'a) * annot 'a
+
+
+type type_union_aux =  (* Type union constructors *)
+ | Tu_id of id
+ | Tu_ty_id of typ * id
+
+
+type name_scm_opt_aux =  (* Optional variable-naming-scheme specification for variables of defined type *)
+ | Name_sect_none
+ | Name_sect_some of string
+
+
+type effect_opt_aux =  (* Optional effect annotation for functions *)
+ | Effect_opt_pure (* sugar for empty effect set *)
+ | Effect_opt_effect of effect
+
+
+type funcl_aux 'a =  (* Function clause *)
+ | FCL_Funcl of id * (pat 'a) * (exp 'a)
+
+
+type rec_opt_aux =  (* Optional recursive annotation for functions *)
+ | Rec_nonrec (* non-recursive *)
+ | Rec_rec (* recursive *)
+
+
+type tannot_opt_aux =  (* Optional type annotation for functions *)
+ | Typ_annot_opt_some of typquant * typ
+
+
+type alias_spec_aux 'a =  (* Register alias expression forms. Other than where noted, each id must refer to an unaliased register of type vector *)
+ | AL_subreg of (reg_id 'a) * id
+ | AL_bit of (reg_id 'a) * (exp 'a)
+ | AL_slice of (reg_id 'a) * (exp 'a) * (exp 'a)
+ | AL_concat of (reg_id 'a) * (reg_id 'a)
+
+
+type type_union = 
+ | Tu_aux of type_union_aux * l
+
+
+type index_range_aux =  (* index specification, for bitfields in register types *)
+ | BF_single of integer (* single index *)
+ | BF_range of integer * integer (* index range *)
+ | BF_concat of index_range * index_range (* concatenation of index ranges *)
+
+and index_range = 
+ | BF_aux of index_range_aux * l
+
+
+type name_scm_opt = 
+ | Name_sect_aux of name_scm_opt_aux * l
+
+
+type effect_opt = 
+ | Effect_opt_aux of effect_opt_aux * l
+
+
+type funcl 'a = 
+ | FCL_aux of (funcl_aux 'a) * annot 'a
+
+
+type rec_opt = 
+ | Rec_aux of rec_opt_aux * l
+
+
+type tannot_opt = 
+ | Typ_annot_opt_aux of tannot_opt_aux * l
+
+
+type alias_spec 'a = 
+ | AL_aux of (alias_spec_aux 'a) * annot 'a
+
+
+type default_spec_aux 'a =  (* Default kinding or typing assumption *)
+ | DT_kind of base_kind * kid
+ | DT_order of order
+ | DT_typ of typschm * id
+
+
+type type_def_aux 'a =  (* Type definition body *)
+ | TD_abbrev of id * name_scm_opt * typschm (* type abbreviation *)
+ | TD_record of id * name_scm_opt * typquant * list (typ * id) * bool (* struct type definition *)
+ | TD_variant of id * name_scm_opt * typquant * list type_union * bool (* union type definition *)
+ | TD_enum of id * name_scm_opt * list id * bool (* enumeration type definition *)
+ | TD_register of id * nexp * nexp * list (index_range * id) (* register mutable bitfield type definition *)
+
+
+type val_spec_aux 'a =  (* Value type specification *)
+ | VS_val_spec of typschm * id
+ | VS_extern_no_rename of typschm * id
+ | VS_extern_spec of typschm * id * string (* Specify the type and id of a function from Lem, where the string must provide an explicit path to the required function but will not be checked *)
+
+
+type kind_def_aux 'a =  (* Definition body for elements of kind; many are shorthands for type\_defs *)
+ | KD_nabbrev of kind * id * name_scm_opt * nexp (* nexp abbreviation *)
+ | KD_abbrev of kind * id * name_scm_opt * typschm (* type abbreviation *)
+ | KD_record of kind * id * name_scm_opt * typquant * list (typ * id) * bool (* struct type definition *)
+ | KD_variant of kind * id * name_scm_opt * typquant * list type_union * bool (* union type definition *)
+ | KD_enum of kind * id * name_scm_opt * list id * bool (* enumeration type definition *)
+ | KD_register of kind * id * nexp * nexp * list (index_range * id) (* register mutable bitfield type definition *)
+
+
+type scattered_def_aux 'a =  (* Function and type union definitions that can be spread across
+         a file. Each one must end in $id$ *)
+ | SD_scattered_function of rec_opt * tannot_opt * effect_opt * id (* scattered function definition header *)
+ | SD_scattered_funcl of (funcl 'a) (* scattered function definition clause *)
+ | SD_scattered_variant of id * name_scm_opt * typquant (* scattered union definition header *)
+ | SD_scattered_unioncl of id * type_union (* scattered union definition member *)
+ | SD_scattered_end of id (* scattered definition end *)
+
+
+type fundef_aux 'a =  (* Function definition *)
+ | FD_function of rec_opt * tannot_opt * effect_opt * list (funcl 'a)
+
+
+type dec_spec_aux 'a =  (* Register declarations *)
+ | DEC_reg of typ * id
+ | DEC_alias of id * (alias_spec 'a)
+ | DEC_typ_alias of typ * id * (alias_spec 'a)
+
+
+type default_spec 'a = 
+ | DT_aux of (default_spec_aux 'a) * l
+
+
+type type_def 'a = 
+ | TD_aux of (type_def_aux 'a) * annot 'a
+
+
+type val_spec 'a = 
+ | VS_aux of (val_spec_aux 'a) * annot 'a
+
+
+type kind_def 'a = 
+ | KD_aux of (kind_def_aux 'a) * annot 'a
+
+
+type scattered_def 'a = 
+ | SD_aux of (scattered_def_aux 'a) * annot 'a
+
+
+type fundef 'a = 
+ | FD_aux of (fundef_aux 'a) * annot 'a
+
+
+type dec_spec 'a = 
+ | DEC_aux of (dec_spec_aux 'a) * annot 'a
+
+
+type dec_comm 'a =  (* Top-level generated comments *)
+ | DC_comm of string (* generated unstructured comment *)
+ | DC_comm_struct of (def 'a) (* generated structured comment *)
+
+and def 'a =  (* Top-level definition *)
+ | DEF_kind of (kind_def 'a) (* definition of named kind identifiers *)
+ | DEF_type of (type_def 'a) (* type definition *)
+ | DEF_fundef of (fundef 'a) (* function definition *)
+ | DEF_val of (letbind 'a) (* value definition *)
+ | DEF_spec of (val_spec 'a) (* top-level type constraint *)
+ | DEF_default of (default_spec 'a) (* default kind and type assumptions *)
+ | DEF_scattered of (scattered_def 'a) (* scattered function and type definition *)
+ | DEF_reg_dec of (dec_spec 'a) (* register declaration *)
+ | DEF_comm of (dec_comm 'a) (* generated comments *)
+
+
+type defs 'a =  (* Definition sequence *)
+ | Defs of list (def 'a)
+
+
+let rec remove_one i l =
+  match l with
+  | [] -> []
+  | i2::l2 -> if i2 = i then l2 else i2::(remove_one i l2)
+end
+
+let rec remove_from l l2 =
+  match l2 with 
+  | [] -> l
+  | i::l2' -> remove_from (remove_one i l) l2'
+end
+
+let disjoint s1 s2 = Set.null (s1 inter s2)
+
+let rec disjoint_all sets =
+  match sets with
+  | [] -> true
+  | s1::[] -> true
+  | s1::s2::sets -> (disjoint s1 s2) && (disjoint_all (s2::sets))
+end
+
+
+type ne =  (* internal numeric expressions *)
+ | Ne_id of x
+ | Ne_var of x
+ | Ne_const of integer
+ | Ne_inf
+ | Ne_mult of ne * ne
+ | Ne_add of list ne
+ | Ne_minus of ne * ne
+ | Ne_exp of ne
+ | Ne_unary of ne
+
+
+type k =  (* Internal kinds *)
+ | Ki_typ
+ | Ki_nat
+ | Ki_ord
+ | Ki_efct
+ | Ki_ctor of list k * k
+ | Ki_infer (* Representing an unknown kind, inferred by context *)
+
+
+type nec =  (* Numeric expression constraints *)
+ | Nec_lteq of ne * ne
+ | Nec_eq of ne * ne
+ | Nec_gteq of ne * ne
+ | Nec_in of x * list integer
+ | Nec_cond of list nec * list nec
+ | Nec_branch of list nec
+
+
+type tid =  (* A type identifier or type variable *)
+ | Tid_id of id
+ | Tid_var of kid
+
+
+type kinf =  (* Whether a kind is default or from a local binding *)
+ | Kinf_k of k
+ | Kinf_def of k
+
+
+type t =  (* Internal types *)
+ | T_id of x
+ | T_var of x
+ | T_fn of t * t * effect
+ | T_tup of list t
+ | T_app of x * t_args
+ | T_abbrev of t * t
+
+and t_arg =  (* Argument to type constructors *)
+ | T_arg_typ of t
+ | T_arg_nexp of ne
+ | T_arg_effect of effect
+ | T_arg_order of order
+
+and t_args =  (* Arguments to type constructors *)
+ | T_args of list t_arg
+
+
+type tag =  (* Data indicating where the identifier arises and thus information necessary in compilation *)
+ | Tag_empty
+ | Tag_intro (* Denotes an assignment and lexp that introduces a binding *)
+ | Tag_set (* Denotes an expression that mutates a local variable *)
+ | Tag_tuple_assign (* Denotes an assignment with a tuple lexp *)
+ | Tag_global (* Globally let-bound or enumeration based value/variable *)
+ | Tag_ctor (* Data constructor from a type union *)
+ | Tag_extern of maybe string (* External function, specied only with a val statement *)
+ | Tag_default (* Type has come from default declaration, identifier may not be bound locally *)
+ | Tag_spec
+ | Tag_enum of integer
+ | Tag_alias
+ | Tag_unknown of maybe string (* Tag to distinguish an unknown path from a non-analysis non deterministic path *)
+
+
+type tinf =  (* Type variables, type, and constraints, bound to an identifier *)
+ | Tinf_typ of t
+ | Tinf_quant_typ of (map tid kinf) * list nec * tag * t
+
+
+type conformsto =  (* how much conformance does overloading need *)
+ | Conformsto_full
+ | Conformsto_parm
+
+
+type widenvec = 
+ | Widenvec_widen
+ | Widenvec_dont
+ | Widenvec_dontcare
+
+
+type widennum = 
+ | Widennum_widen
+ | Widennum_dont
+ | Widennum_dontcare
+
+
+type tinflist =  (* In place so that a list of tinfs can be referred to without the dot form *)
+ | Tinfs_empty
+ | Tinfs_ls of list tinf
+
+
+type widening =  (* Should we widen vector start locations, should we widen atoms and ranges *)
+ | Widening_w of widennum * widenvec
+
+ type definition_env =
+   | DenvEmp
+   | Denv of (map tid kinf) * (map (list (id*t)) tinf) * (map t (list (nat*id)))
+
+
+let blength (bit) = Ne_const 8
+let hlength (bit) = Ne_const 8
+
+ type env =
+   | EnvEmp 
+   | Env of (map id tinf) * definition_env
+
+ type inf = 
+   | Iemp
+   | Inf of (list nec) * effect
+
+ val denv_union : definition_env -> definition_env -> definition_env
+ let denv_union de1 de2 = 
+  match (de1,de2) with
+   | (DenvEmp,de2) -> de2
+   | (de1,DenvEmp) -> de1
+   | ((Denv ke1 re1 ee1),(Denv ke2 re2 ee2)) ->
+      Denv (ke1 union ke2) (re1 union re2) (ee1 union ee2)
+   end
+
+ val env_union : env -> env -> env
+ let env_union e1 e2 =
+   match (e1,e2) with
+    | (EnvEmp,e2) -> e2
+    | (e1,EnvEmp) -> e1
+    | ((Env te1 de1),(Env te2 de2)) ->
+      Env (te1 union te2) (denv_union de1 de2)
+ end
+
+let inf_union i1 i2 =
+  match (i1,i2) with 
+ | (Iemp,i2) -> i2
+ | (i1,Iemp) -> i1
+ | (Inf n1 e1,Inf n2 e2) -> (Inf (n1++n2) (effect_union e1 e2))
+ end
+
+let fresh_kid denv = Var "x" (*TODO When strings can be manipulated, this should actually build a fresh string*)
+
+
+
+type E = env
+
+
+type I = inf
+
+
+
diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem
index 75e695eb..8c80b1c1 100644
--- a/src/lem_interp/interp_inter_imp.lem
+++ b/src/lem_interp/interp_inter_imp.lem
@@ -1,3 +1,45 @@
+(*========================================================================*)
+(*     Sail                                                               *)
+(*                                                                        *)
+(*  Copyright (c) 2013-2017                                               *)
+(*    Kathyrn Gray                                                        *)
+(*    Shaked Flur                                                         *)
+(*    Stephen Kell                                                        *)
+(*    Gabriel Kerneis                                                     *)
+(*    Robert Norton-Wright                                                *)
+(*    Christopher Pulte                                                   *)
+(*    Peter Sewell                                                        *)
+(*                                                                        *)
+(*  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 import Interp_ast
 import Interp
 import Interp_lib
@@ -1120,17 +1162,17 @@ let nias_of_instruction
   match (thread_ism, instruction_name) with
     | ("PPCGEN_ism", "B") ->
        let () = ensure (not unknown_nia_address)
-                       "unexpected unknown/undefined address in nia_values" in
+                       "unexpected unknown/undefined address in nia_values 1" in
        nias
     | ("PPCGEN_ism", "Bc") ->
        let () = ensure (not unknown_nia_address)
-                       "unexpected unknown/undefined address in nia_values" in
+                       "unexpected unknown/undefined address in nia_values 2" in
        NIA_successor :: nias
     | ("PPCGEN_ism", "Bclr") -> [ NIA_successor; NIA_LR ]
     | ("PPCGEN_ism", "Bcctr") -> [ NIA_successor; NIA_CTR ]
     | ("PPCGEN_ism", "Sc") ->
        let () = ensure (not unknown_nia_address)
-                       "unexpected unknown/undefined address in nia_values" in
+                       "unexpected unknown/undefined address in nia_values 3" in
        match instruction_fields with
        | [(_, _, lev)] ->
           (* LEV field is 7 bits long, pad it with false at beginning *)
@@ -1175,13 +1217,49 @@ let nias_of_instruction
                             | _ -> false
                             end]
 
+
+    (** hacky cut-and-paste for AArch64Gen, duplicating code just to see if this suffices *)
+
+    | ("AArch64GenSail", "BranchImmediate")   -> nias
+    | ("AArch64GenSail", "BranchConditional") -> NIA_successor :: nias
+    | ("AArch64GenSail", "CompareAndBranch")  -> NIA_successor :: nias
+    | ("AArch64GenSail", "TestBitAndBranch")  -> NIA_successor :: nias
+
+    (* AArch64 calculated address branch *)
+    | ("AArch64GenSail", "branch_unconditional_register") ->
+        (* do some parsing of the ast fields to figure out which register holds
+           the branching address i.e. find n in "BR <Xn>". The ast constructor
+           from armV8.sail: (reg_index,BranchType) BranchRegister; *)
+        let n_integer =
+          match instruction_fields with
+          | [(_, _, n); _] -> integer_of_bit_list n
+          | _ -> fail
+          end
+        in
+        let () = ensure (0 <= n_integer && n_integer <= 31)
+                  "expected register number from 0 to 31"
+        in
+        if n_integer = 31 then
+          nias (* BR XZR *)
+        else
+          (* look for Xn (which we actually call Rn) in regs_in *)
+          let n_reg = "R" ^ (String_extra.stringFromInteger n_integer) in
+          [NIA_register r | forall (r MEM regs_in)
+                          | match r with
+                            | (Reg name _ _ _) -> name = n_reg
+                            | _ -> false
+                            end]
+
+    (** end of hacky *)
+
     | ("AArch64LitmusSail", "CtrlDep") -> NIA_successor :: nias
 
+
     | ("MIPS_ism", "B") -> fail
 
-    | _ ->
+    | (s1,s2) ->
        let () = ensure (not unknown_nia_address)
-                       "unexpected unknown/undefined address in nia_values" in
+                       ("unexpected unknown/undefined address in nia_values 4 (\""^s1^"\", \""^s2^"\")") in
         [ NIA_successor ]
     end
 
diff --git a/src/lem_interp/interp_interface.lem b/src/lem_interp/interp_interface.lem
index 1de2de77..27165b15 100644
--- a/src/lem_interp/interp_interface.lem
+++ b/src/lem_interp/interp_interface.lem
@@ -1,3 +1,45 @@
+(*========================================================================*)
+(*     Sail                                                               *)
+(*                                                                        *)
+(*  Copyright (c) 2013-2017                                               *)
+(*    Kathyrn Gray                                                        *)
+(*    Shaked Flur                                                         *)
+(*    Stephen Kell                                                        *)
+(*    Gabriel Kerneis                                                     *)
+(*    Robert Norton-Wright                                                *)
+(*    Christopher Pulte                                                   *)
+(*    Peter Sewell                                                        *)
+(*                                                                        *)
+(*  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.                                                          *)
+(*========================================================================*)
+
 (* PS NOTES FOR KATHY:
 
 pls also change:  
diff --git a/src/lem_interp/interp_lib.lem b/src/lem_interp/interp_lib.lem
index 625dfb6c..36a31f3f 100644
--- a/src/lem_interp/interp_lib.lem
+++ b/src/lem_interp/interp_lib.lem
@@ -1,3 +1,45 @@
+(*========================================================================*)
+(*     Sail                                                               *)
+(*                                                                        *)
+(*  Copyright (c) 2013-2017                                               *)
+(*    Kathyrn Gray                                                        *)
+(*    Shaked Flur                                                         *)
+(*    Stephen Kell                                                        *)
+(*    Gabriel Kerneis                                                     *)
+(*    Robert Norton-Wright                                                *)
+(*    Christopher Pulte                                                   *)
+(*    Peter Sewell                                                        *)
+(*                                                                        *)
+(*  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 import Pervasives
 open import Interp_utilities
 open import Interp
@@ -701,15 +743,15 @@ let rec shift_op_vec op v =
   let fail () = Assert_extra.failwith ("shift_op_vec given unexpected " ^ (string_of_value v)) in
   let arith_op_help vl vr =
     match (vl,vr) with
-      | (V_vector b ord cs,V_lit (L_aux (L_num n) _)) ->
-	let n = natFromInteger n in
-	(match op with
-	  | "<<" -> 
-	    V_vector b ord 
-	      ((from_n_to_n n ((length cs) - 1) cs) ++(List.replicate n (V_lit (L_aux L_zero Unknown))))
-	  | ">>" ->
+    | (V_vector b ord cs,V_lit (L_aux (L_num n) _)) ->
+      let n = natFromInteger n in
+      (match op with
+       | "<<" -> 
+	 V_vector b ord 
+           ((from_n_to_n n ((length cs) - 1) cs) ++(List.replicate n (V_lit (L_aux L_zero Unknown))))
+       | ">>" ->
 	    V_vector b ord
-	      ((List.replicate n (V_lit (L_aux L_zero Unknown))) ++ (from_n_to_n 0 (n-1) cs))
+	      ((List.replicate n (V_lit (L_aux L_zero Unknown))) ++ (from_n_to_n 0 (((length cs) -1) - n) cs))
 	  | "<<<" ->
 	    V_vector b ord
              ((from_n_to_n n ((length cs) -1) cs) ++ (from_n_to_n 0 (n-1) cs))
diff --git a/src/lem_interp/interp_utilities.lem b/src/lem_interp/interp_utilities.lem
index 63287a2e..86042d61 100644
--- a/src/lem_interp/interp_utilities.lem
+++ b/src/lem_interp/interp_utilities.lem
@@ -1,3 +1,45 @@
+(*========================================================================*)
+(*     Sail                                                               *)
+(*                                                                        *)
+(*  Copyright (c) 2013-2017                                               *)
+(*    Kathyrn Gray                                                        *)
+(*    Shaked Flur                                                         *)
+(*    Stephen Kell                                                        *)
+(*    Gabriel Kerneis                                                     *)
+(*    Robert Norton-Wright                                                *)
+(*    Christopher Pulte                                                   *)
+(*    Peter Sewell                                                        *)
+(*                                                                        *)
+(*  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 import Interp_ast
 open import Pervasives
 open import Show_extra
diff --git a/src/lem_interp/pretty_interp.ml b/src/lem_interp/pretty_interp.ml
index 707ba9c3..7d182258 100644
--- a/src/lem_interp/pretty_interp.ml
+++ b/src/lem_interp/pretty_interp.ml
@@ -1,3 +1,45 @@
+(**************************************************************************)
+(*     Sail                                                               *)
+(*                                                                        *)
+(*  Copyright (c) 2013-2017                                               *)
+(*    Kathyrn Gray                                                        *)
+(*    Shaked Flur                                                         *)
+(*    Stephen Kell                                                        *)
+(*    Gabriel Kerneis                                                     *)
+(*    Robert Norton-Wright                                                *)
+(*    Christopher Pulte                                                   *)
+(*    Peter Sewell                                                        *)
+(*                                                                        *)
+(*  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.                                                          *)
+(**************************************************************************)
+
 (* XXX this is copy-pasted from pretty_printer.ml with the following
  * changes:
  * - open Interp_ast instead of Ast; don't open Type_internals
diff --git a/src/lem_interp/printing_functions.ml b/src/lem_interp/printing_functions.ml
index 202af6bb..88dbfbc8 100644
--- a/src/lem_interp/printing_functions.ml
+++ b/src/lem_interp/printing_functions.ml
@@ -1,3 +1,45 @@
+(**************************************************************************)
+(*     Sail                                                               *)
+(*                                                                        *)
+(*  Copyright (c) 2013-2017                                               *)
+(*    Kathyrn Gray                                                        *)
+(*    Shaked Flur                                                         *)
+(*    Stephen Kell                                                        *)
+(*    Gabriel Kerneis                                                     *)
+(*    Robert Norton-Wright                                                *)
+(*    Christopher Pulte                                                   *)
+(*    Peter Sewell                                                        *)
+(*                                                                        *)
+(*  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 Printf ;;
 open Interp_ast ;;
 open Sail_impl_base ;;
diff --git a/src/lem_interp/run_interp.ml b/src/lem_interp/run_interp.ml
index a8291a78..6f5ca07a 100644
--- a/src/lem_interp/run_interp.ml
+++ b/src/lem_interp/run_interp.ml
@@ -1,3 +1,45 @@
+(**************************************************************************)
+(*     Sail                                                               *)
+(*                                                                        *)
+(*  Copyright (c) 2013-2017                                               *)
+(*    Kathyrn Gray                                                        *)
+(*    Shaked Flur                                                         *)
+(*    Stephen Kell                                                        *)
+(*    Gabriel Kerneis                                                     *)
+(*    Robert Norton-Wright                                                *)
+(*    Christopher Pulte                                                   *)
+(*    Peter Sewell                                                        *)
+(*                                                                        *)
+(*  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 Printf ;;
 open Interp_ast ;;
 open Interp ;;
diff --git a/src/lem_interp/run_interp_model.ml b/src/lem_interp/run_interp_model.ml
index cd038a7a..af9a1e0e 100644
--- a/src/lem_interp/run_interp_model.ml
+++ b/src/lem_interp/run_interp_model.ml
@@ -1,3 +1,45 @@
+(**************************************************************************)
+(*     Sail                                                               *)
+(*                                                                        *)
+(*  Copyright (c) 2013-2017                                               *)
+(*    Kathyrn Gray                                                        *)
+(*    Shaked Flur                                                         *)
+(*    Stephen Kell                                                        *)
+(*    Gabriel Kerneis                                                     *)
+(*    Robert Norton-Wright                                                *)
+(*    Christopher Pulte                                                   *)
+(*    Peter Sewell                                                        *)
+(*                                                                        *)
+(*  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 Printf
 open Interp_ast
 open Sail_impl_base
diff --git a/src/lem_interp/run_with_elf.ml b/src/lem_interp/run_with_elf.ml
index 81e6bd6e..813bef3a 100644
--- a/src/lem_interp/run_with_elf.ml
+++ b/src/lem_interp/run_with_elf.ml
@@ -1,3 +1,45 @@
+(**************************************************************************)
+(*     Sail                                                               *)
+(*                                                                        *)
+(*  Copyright (c) 2013-2017                                               *)
+(*    Kathyrn Gray                                                        *)
+(*    Shaked Flur                                                         *)
+(*    Stephen Kell                                                        *)
+(*    Gabriel Kerneis                                                     *)
+(*    Robert Norton-Wright                                                *)
+(*    Christopher Pulte                                                   *)
+(*    Peter Sewell                                                        *)
+(*                                                                        *)
+(*  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 Printf ;;
 open Format ;;
 open Big_int ;;
diff --git a/src/lem_interp/run_with_elf_cheri.ml b/src/lem_interp/run_with_elf_cheri.ml
index 40a6495b..d58a6bd0 100644
--- a/src/lem_interp/run_with_elf_cheri.ml
+++ b/src/lem_interp/run_with_elf_cheri.ml
@@ -1,3 +1,45 @@
+(**************************************************************************)
+(*     Sail                                                               *)
+(*                                                                        *)
+(*  Copyright (c) 2013-2017                                               *)
+(*    Kathyrn Gray                                                        *)
+(*    Shaked Flur                                                         *)
+(*    Stephen Kell                                                        *)
+(*    Gabriel Kerneis                                                     *)
+(*    Robert Norton-Wright                                                *)
+(*    Christopher Pulte                                                   *)
+(*    Peter Sewell                                                        *)
+(*                                                                        *)
+(*  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 Printf ;;
 open Format ;;
 open Big_int ;;
diff --git a/src/lem_interp/run_with_elf_cheri128.ml b/src/lem_interp/run_with_elf_cheri128.ml
index 99a6e681..37685233 100644
--- a/src/lem_interp/run_with_elf_cheri128.ml
+++ b/src/lem_interp/run_with_elf_cheri128.ml
@@ -1,3 +1,45 @@
+(**************************************************************************)
+(*     Sail                                                               *)
+(*                                                                        *)
+(*  Copyright (c) 2013-2017                                               *)
+(*    Kathyrn Gray                                                        *)
+(*    Shaked Flur                                                         *)
+(*    Stephen Kell                                                        *)
+(*    Gabriel Kerneis                                                     *)
+(*    Robert Norton-Wright                                                *)
+(*    Christopher Pulte                                                   *)
+(*    Peter Sewell                                                        *)
+(*                                                                        *)
+(*  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 Printf ;;
 open Format ;;
 open Big_int ;;
@@ -623,7 +665,7 @@ let cheri_register_data_all = mips_register_data_all @ [
 
 let initial_stack_and_reg_data_of_MIPS_elf_file e_entry all_data_memory =
   let initial_stack_data = [] in 
-  let initial_cap_val_int = Nat_big_num.of_string "0x1fffe5a00000800000000000000000000" in (* hex((0x80000 << 64) + (45 << 105) + (0x7fff << 113) + (1 << 128)) *)
+  let initial_cap_val_int = Nat_big_num.of_string "0x1fffe0000000800000000000000000000" in (* hex((0x80000 << 64) + (0x7fff << 113) + (1 << 128)) *)
   let initial_cap_val_reg = Sail_impl_base.register_value_of_integer 129 128 D_decreasing  initial_cap_val_int in
   let initial_register_abi_data : (string * Sail_impl_base.register_value) list = [
     ("CP0Status", Sail_impl_base.register_value_of_integer 32 31 D_decreasing (Nat_big_num.of_string "0x00400000"));
diff --git a/src/lem_interp/sail_impl_base.lem b/src/lem_interp/sail_impl_base.lem
index 3f38f521..97c7cff1 100644
--- a/src/lem_interp/sail_impl_base.lem
+++ b/src/lem_interp/sail_impl_base.lem
@@ -1,3 +1,45 @@
+(*========================================================================*)
+(*     Sail                                                               *)
+(*                                                                        *)
+(*  Copyright (c) 2013-2017                                               *)
+(*    Kathyrn Gray                                                        *)
+(*    Shaked Flur                                                         *)
+(*    Stephen Kell                                                        *)
+(*    Gabriel Kerneis                                                     *)
+(*    Robert Norton-Wright                                                *)
+(*    Christopher Pulte                                                   *)
+(*    Peter Sewell                                                        *)
+(*                                                                        *)
+(*  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 import Pervasives_extra
             
 (* maybe isn't a member of type Ord - this should be in the Lem standard library*)
diff --git a/src/lem_interp/type_check.lem b/src/lem_interp/type_check.lem
index ec8e46bc..179e53d3 100644
--- a/src/lem_interp/type_check.lem
+++ b/src/lem_interp/type_check.lem
@@ -1,3 +1,45 @@
+(*========================================================================*)
+(*     Sail                                                               *)
+(*                                                                        *)
+(*  Copyright (c) 2013-2017                                               *)
+(*    Kathyrn Gray                                                        *)
+(*    Shaked Flur                                                         *)
+(*    Stephen Kell                                                        *)
+(*    Gabriel Kerneis                                                     *)
+(*    Robert Norton-Wright                                                *)
+(*    Christopher Pulte                                                   *)
+(*    Peter Sewell                                                        *)
+(*                                                                        *)
+(*  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 import Pervasives
 import Map
 import Map_extra (* For 'find' instead of using lookup and maybe types, as we know it cannot fail *)
diff --git a/src/lexer.mll b/src/lexer.mll
index c2b95004..98c9098d 100644
--- a/src/lexer.mll
+++ b/src/lexer.mll
@@ -1,47 +1,43 @@
 (**************************************************************************)
-(*                        Lem                                             *)
+(*     Sail                                                               *)
 (*                                                                        *)
-(*          Dominic Mulligan, University of Cambridge                     *)
-(*          Francesco Zappa Nardelli, INRIA Paris-Rocquencourt            *)
-(*          Gabriel Kerneis, University of Cambridge                      *)
-(*          Kathy Gray, University of Cambridge                           *)
-(*          Peter Boehm, University of Cambridge (while working on Lem)   *)
-(*          Peter Sewell, University of Cambridge                         *)
-(*          Scott Owens, University of Kent                               *)
-(*          Thomas Tuerk, University of Cambridge                         *)
+(*  Copyright (c) 2013-2017                                               *)
+(*    Kathyrn Gray                                                        *)
+(*    Shaked Flur                                                         *)
+(*    Stephen Kell                                                        *)
+(*    Gabriel Kerneis                                                     *)
+(*    Robert Norton-Wright                                                *)
+(*    Christopher Pulte                                                   *)
+(*    Peter Sewell                                                        *)
 (*                                                                        *)
-(*  The Lem sources are copyright 2010-2013                               *)
-(*  by the UK authors above and Institut National de Recherche en         *)
-(*  Informatique et en Automatique (INRIA).                               *)
-(*                                                                        *)
-(*  All files except ocaml-lib/pmap.{ml,mli} and ocaml-libpset.{ml,mli}   *)
-(*  are distributed under the license below.  The former are distributed  *)
-(*  under the LGPLv2, as in the LICENSE file.                             *)
+(*  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.         *)
+(*     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.  *)
-(*  3. The names of the authors may not be used to endorse or promote     *)
-(*  products derived from this software without specific prior written    *)
-(*  permission.                                                           *)
+(*     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 AUTHORS ``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 AUTHORS 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.                         *)
+(*  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.                                                          *)
 (**************************************************************************)
 
 {
diff --git a/src/myocamlbuild.ml b/src/myocamlbuild.ml
index 2be63ad7..765553d3 100644
--- a/src/myocamlbuild.ml
+++ b/src/myocamlbuild.ml
@@ -1,3 +1,45 @@
+(**************************************************************************)
+(*     Sail                                                               *)
+(*                                                                        *)
+(*  Copyright (c) 2013-2017                                               *)
+(*    Kathyrn Gray                                                        *)
+(*    Shaked Flur                                                         *)
+(*    Stephen Kell                                                        *)
+(*    Gabriel Kerneis                                                     *)
+(*    Robert Norton-Wright                                                *)
+(*    Christopher Pulte                                                   *)
+(*    Peter Sewell                                                        *)
+(*                                                                        *)
+(*  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 Ocamlbuild_plugin ;;
 open Command ;;
 open Pathname ;;
diff --git a/src/parse_ast.ml b/src/parse_ast.ml
index c4f970ec..2e72761e 120000..100644
--- a/src/parse_ast.ml
+++ b/src/parse_ast.ml
@@ -1 +1,510 @@
-../language/l2_parse.ml
\ No newline at end of file
+(**************************************************************************)
+(*     Sail                                                               *)
+(*                                                                        *)
+(*  Copyright (c) 2013-2017                                               *)
+(*    Kathyrn Gray                                                        *)
+(*    Shaked Flur                                                         *)
+(*    Stephen Kell                                                        *)
+(*    Gabriel Kerneis                                                     *)
+(*    Robert Norton-Wright                                                *)
+(*    Christopher Pulte                                                   *)
+(*    Peter Sewell                                                        *)
+(*                                                                        *)
+(*  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.                                                          *)
+(**************************************************************************)
+
+(* generated by Ott 0.25 from: l2_parse.ott *)
+
+
+type text = string
+
+type l =
+  | Unknown
+  | Int of string * l option
+  | Generated of l
+  | Range of Lexing.position * Lexing.position
+
+type 'a annot = l * 'a
+
+exception Parse_error_locn of l * string
+
+
+type x = text (* identifier *)
+type ix = text (* infix identifier *)
+
+type 
+base_kind_aux =  (* base kind *)
+   BK_type (* kind of types *)
+ | BK_nat (* kind of natural number size expressions *)
+ | BK_order (* kind of vector order specifications *)
+ | BK_effect (* kind of effect sets *)
+
+
+type 
+base_kind = 
+   BK_aux of base_kind_aux * l
+
+
+type 
+base_effect_aux =  (* effect *)
+   BE_rreg (* read register *)
+ | BE_wreg (* write register *)
+ | BE_rmem (* read memory *)
+ | BE_wmem (* write memory *)
+ | BE_wmv (* write memory value *)
+ | BE_eamem (* address for write signaled *)
+ | BE_barr (* memory barrier *)
+ | BE_depend (* dynmically dependent footprint *)
+ | BE_undef (* undefined-instruction exception *)
+ | BE_unspec (* unspecified values *)
+ | BE_nondet (* nondeterminism from intra-instruction parallelism *)
+ | BE_escape
+
+
+type 
+kid_aux =  (* identifiers with kind, ticked to differntiate from program variables *)
+   Var of x
+
+
+type 
+id_aux =  (* Identifier *)
+   Id of x
+ | DeIid of x (* remove infix status *)
+
+
+type 
+kind_aux =  (* kinds *)
+   K_kind of (base_kind) list
+
+
+type 
+base_effect = 
+   BE_aux of base_effect_aux * l
+
+
+type 
+kid = 
+   Kid_aux of kid_aux * l
+
+
+type 
+id = 
+   Id_aux of id_aux * l
+
+
+type 
+kind = 
+   K_aux of kind_aux * l
+
+
+type 
+atyp_aux =  (* expressions of all kinds, to be translated to types, nats, orders, and effects after parsing *)
+   ATyp_id of id (* identifier *)
+ | ATyp_var of kid (* ticked variable *)
+ | ATyp_constant of int (* constant *)
+ | ATyp_times of atyp * atyp (* product *)
+ | ATyp_sum of atyp * atyp (* sum *)
+ | ATyp_minus of atyp * atyp (* subtraction *)
+ | ATyp_exp of atyp (* exponential *)
+ | ATyp_neg of atyp (* Internal (but not M as I want a datatype constructor) negative nexp *)
+ | ATyp_inc (* increasing (little-endian) *)
+ | ATyp_dec (* decreasing (big-endian) *)
+ | ATyp_default_ord (* default order for increasing or decreasing signficant bits *)
+ | ATyp_set of (base_effect) list (* effect set *)
+ | ATyp_fn of atyp * atyp * atyp (* Function type (first-order only in user code), last atyp is an effect *)
+ | ATyp_tup of (atyp) list (* Tuple type *)
+ | ATyp_app of id * (atyp) list (* type constructor application *)
+
+and atyp = 
+   ATyp_aux of atyp_aux * l
+
+
+type 
+kinded_id_aux =  (* optionally kind-annotated identifier *)
+   KOpt_none of kid (* identifier *)
+ | KOpt_kind of kind * kid (* kind-annotated variable *)
+
+
+type 
+n_constraint_aux =  (* constraint over kind $_$ *)
+   NC_fixed of atyp * atyp
+ | NC_bounded_ge of atyp * atyp
+ | NC_bounded_le of atyp * atyp
+ | NC_nat_set_bounded of kid * (int) list
+
+
+type 
+kinded_id = 
+   KOpt_aux of kinded_id_aux * l
+
+
+type 
+n_constraint = 
+   NC_aux of n_constraint_aux * l
+
+
+type 
+quant_item_aux =  (* Either a kinded identifier or a nexp constraint for a typquant *)
+   QI_id of kinded_id (* An optionally kinded identifier *)
+ | QI_const of n_constraint (* A constraint for this type *)
+
+
+type 
+quant_item = 
+   QI_aux of quant_item_aux * l
+
+
+type 
+typquant_aux =  (* type quantifiers and constraints *)
+   TypQ_tq of (quant_item) list
+ | TypQ_no_forall (* sugar, omitting quantifier and constraints *)
+
+
+type 
+typquant = 
+   TypQ_aux of typquant_aux * l
+
+
+type 
+lit_aux =  (* Literal constant *)
+   L_unit (* $() : _$ *)
+ | L_zero (* $_ : _$ *)
+ | L_one (* $_ : _$ *)
+ | L_true (* $_ : _$ *)
+ | L_false (* $_ : _$ *)
+ | L_num of int (* natural number constant *)
+ | L_hex of string (* bit vector constant, C-style *)
+ | L_bin of string (* bit vector constant, C-style *)
+ | L_undef (* undefined value *)
+ | L_string of string (* string constant *)
+
+
+type 
+typschm_aux =  (* type scheme *)
+   TypSchm_ts of typquant * atyp
+
+
+type 
+lit = 
+   L_aux of lit_aux * l
+
+
+type 
+typschm = 
+   TypSchm_aux of typschm_aux * l
+
+
+type 
+pat_aux =  (* Pattern *)
+   P_lit of lit (* literal constant pattern *)
+ | P_wild (* wildcard *)
+ | P_as of pat * id (* named pattern *)
+ | P_typ of atyp * pat (* typed pattern *)
+ | P_id of id (* identifier *)
+ | P_app of id * (pat) list (* union constructor pattern *)
+ | P_record of (fpat) list * bool (* struct pattern *)
+ | P_vector of (pat) list (* vector pattern *)
+ | P_vector_indexed of ((int * pat)) list (* vector pattern (with explicit indices) *)
+ | P_vector_concat of (pat) list (* concatenated vector pattern *)
+ | P_tup of (pat) list (* tuple pattern *)
+ | P_list of (pat) list (* list pattern *)
+
+and pat = 
+   P_aux of pat_aux * l
+
+and fpat_aux =  (* Field pattern *)
+   FP_Fpat of id * pat
+
+and fpat = 
+   FP_aux of fpat_aux * l
+
+
+type 
+exp_aux =  (* Expression *)
+   E_block of (exp) list (* block (parsing conflict with structs?) *)
+ | E_nondet of (exp) list (* block that can evaluate the contained expressions in any ordering *)
+ | E_id of id (* identifier *)
+ | E_lit of lit (* literal constant *)
+ | E_cast of atyp * exp (* cast *)
+ | E_app of id * (exp) list (* function application *)
+ | E_app_infix of exp * id * exp (* infix function application *)
+ | E_tuple of (exp) list (* tuple *)
+ | E_if of exp * exp * exp (* conditional *)
+ | E_for of id * exp * exp * exp * atyp * exp (* loop *)
+ | E_vector of (exp) list (* vector (indexed from 0) *)
+ | E_vector_indexed of (exp) list * opt_default (* vector (indexed consecutively) *)
+ | E_vector_access of exp * exp (* vector access *)
+ | E_vector_subrange of exp * exp * exp (* subvector extraction *)
+ | E_vector_update of exp * exp * exp (* vector functional update *)
+ | E_vector_update_subrange of exp * exp * exp * exp (* vector subrange update (with vector) *)
+ | E_vector_append of exp * exp (* vector concatenation *)
+ | E_list of (exp) list (* list *)
+ | E_cons of exp * exp (* cons *)
+ | E_record of fexps (* struct *)
+ | E_record_update of exp * (exp) list (* functional update of struct *)
+ | E_field of exp * id (* field projection from struct *)
+ | E_case of exp * (pexp) list (* pattern matching *)
+ | E_let of letbind * exp (* let expression *)
+ | E_assign of exp * exp (* imperative assignment *)
+ | E_sizeof of atyp
+ | E_exit of exp
+ | E_return of exp
+ | E_assert of exp * exp
+
+and exp = 
+   E_aux of exp_aux * l
+
+and fexp_aux =  (* Field-expression *)
+   FE_Fexp of id * exp
+
+and fexp = 
+   FE_aux of fexp_aux * l
+
+and fexps_aux =  (* Field-expression list *)
+   FES_Fexps of (fexp) list * bool
+
+and fexps = 
+   FES_aux of fexps_aux * l
+
+and opt_default_aux =  (* Optional default value for indexed vectors, to define a defualt value for any unspecified positions in a sparse map *)
+   Def_val_empty
+ | Def_val_dec of exp
+
+and opt_default = 
+   Def_val_aux of opt_default_aux * l
+
+and pexp_aux =  (* Pattern match *)
+   Pat_exp of pat * exp
+
+and pexp = 
+   Pat_aux of pexp_aux * l
+
+and letbind_aux =  (* Let binding *)
+   LB_val_explicit of typschm * pat * exp (* value binding, explicit type (pat must be total) *)
+ | LB_val_implicit of pat * exp (* value binding, implicit type (pat must be total) *)
+
+and letbind = 
+   LB_aux of letbind_aux * l
+
+
+type 
+tannot_opt_aux =  (* Optional type annotation for functions *)
+   Typ_annot_opt_none
+ | Typ_annot_opt_some of typquant * atyp
+
+
+type 
+effect_opt_aux =  (* Optional effect annotation for functions *)
+   Effect_opt_pure (* sugar for empty effect set *)
+ | Effect_opt_effect of atyp
+
+
+type 
+rec_opt_aux =  (* Optional recursive annotation for functions *)
+   Rec_nonrec (* non-recursive *)
+ | Rec_rec (* recursive *)
+
+
+type 
+funcl_aux =  (* Function clause *)
+   FCL_Funcl of id * pat * exp
+
+
+type 
+type_union_aux =  (* Type union constructors *)
+   Tu_id of id
+ | Tu_ty_id of atyp * id
+
+
+type 
+name_scm_opt_aux =  (* Optional variable-naming-scheme specification for variables of defined type *)
+   Name_sect_none
+ | Name_sect_some of string
+
+
+type 
+tannot_opt = 
+   Typ_annot_opt_aux of tannot_opt_aux * l
+
+
+type 
+effect_opt = 
+   Effect_opt_aux of effect_opt_aux * l
+
+
+type 
+rec_opt = 
+   Rec_aux of rec_opt_aux * l
+
+
+type 
+funcl = 
+   FCL_aux of funcl_aux * l
+
+
+type 
+type_union = 
+   Tu_aux of type_union_aux * l
+
+
+type 
+index_range_aux =  (* index specification, for bitfields in register types *)
+   BF_single of int (* single index *)
+ | BF_range of int * int (* index range *)
+ | BF_concat of index_range * index_range (* concatenation of index ranges *)
+
+and index_range = 
+   BF_aux of index_range_aux * l
+
+
+type 
+name_scm_opt = 
+   Name_sect_aux of name_scm_opt_aux * l
+
+
+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
+
+
+type 
+fundef_aux =  (* Function definition *)
+   FD_function of rec_opt * tannot_opt * effect_opt * (funcl) list
+
+
+type 
+type_def_aux =  (* Type definition body *)
+   TD_abbrev of id * name_scm_opt * typschm (* type abbreviation *)
+ | TD_record of id * name_scm_opt * typquant * ((atyp * id)) list * bool (* struct type definition *)
+ | TD_variant of id * name_scm_opt * typquant * (type_union) list * bool (* union type definition *)
+ | TD_enum of id * name_scm_opt * (id) list * bool (* enumeration type definition *)
+ | TD_register of id * atyp * atyp * ((index_range * id)) list (* register mutable bitfield type definition *)
+
+
+type 
+val_spec_aux =  (* Value type specification *)
+   VS_val_spec of typschm * id
+ | VS_extern_no_rename of typschm * id
+ | VS_extern_spec of typschm * id * string
+
+
+type 
+kind_def_aux =  (* Definition body for elements of kind; many are shorthands for type\_defs *)
+   KD_abbrev of kind * id * name_scm_opt * typschm (* type abbreviation *)
+ | KD_record of kind * id * name_scm_opt * typquant * ((atyp * id)) list * bool (* struct type definition *)
+ | KD_variant of kind * id * name_scm_opt * typquant * (type_union) list * bool (* union type definition *)
+ | KD_enum of kind * id * name_scm_opt * (id) list * bool (* enumeration type definition *)
+ | KD_register of kind * id * atyp * atyp * ((index_range * id)) list (* register mutable bitfield type definition *)
+
+
+type 
+dec_spec_aux =  (* Register declarations *)
+   DEC_reg of atyp * id
+ | DEC_alias of id * exp
+ | DEC_typ_alias of atyp * id * exp
+
+
+type 
+scattered_def_aux =  (* Function and type union definitions that can be spread across
+         a file. Each one must end in $_$ *)
+   SD_scattered_function of rec_opt * tannot_opt * effect_opt * id (* scattered function definition header *)
+ | SD_scattered_funcl of funcl (* scattered function definition clause *)
+ | SD_scattered_variant of id * name_scm_opt * typquant (* scattered union definition header *)
+ | SD_scattered_unioncl of id * type_union (* scattered union definition member *)
+ | SD_scattered_end of id (* scattered definition end *)
+
+
+type 
+default_typing_spec = 
+   DT_aux of default_typing_spec_aux * l
+
+
+type 
+fundef = 
+   FD_aux of fundef_aux * l
+
+
+type 
+type_def = 
+   TD_aux of type_def_aux * l
+
+
+type 
+val_spec = 
+   VS_aux of val_spec_aux * l
+
+
+type 
+kind_def = 
+   KD_aux of kind_def_aux * l
+
+
+type 
+dec_spec = 
+   DEC_aux of dec_spec_aux * l
+
+
+type 
+scattered_def = 
+   SD_aux of scattered_def_aux * l
+
+
+type 
+def =  (* Top-level definition *)
+   DEF_kind of kind_def (* definition of named kind identifiers *)
+ | DEF_type of type_def (* type definition *)
+ | DEF_fundef of fundef (* function definition *)
+ | DEF_val of letbind (* value definition *)
+ | DEF_spec of val_spec (* top-level type constraint *)
+ | DEF_default of default_typing_spec (* default kind and type assumptions *)
+ | DEF_scattered of scattered_def (* scattered definition *)
+ | DEF_reg_dec of dec_spec (* register declaration *)
+
+
+type 
+lexp_aux =  (* lvalue expression, can't occur out of the parser *)
+   LEXP_id of id (* identifier *)
+ | LEXP_mem of id * (exp) list
+ | LEXP_vector of lexp * exp (* vector element *)
+ | LEXP_vector_range of lexp * exp * exp (* subvector *)
+ | LEXP_field of lexp * id (* struct field *)
+
+and lexp = 
+   LEXP_aux of lexp_aux * l
+
+
+type 
+defs =  (* Definition sequence *)
+   Defs of (def) list
+
+
+
diff --git a/src/parser.mly b/src/parser.mly
index fb7ffa44..d172f61b 100644
--- a/src/parser.mly
+++ b/src/parser.mly
@@ -1,47 +1,43 @@
 /**************************************************************************/
-/*                        Lem                                             */
+/*     Sail                                                               */
 /*                                                                        */
-/*          Dominic Mulligan, University of Cambridge                     */
-/*          Francesco Zappa Nardelli, INRIA Paris-Rocquencourt            */
-/*          Gabriel Kerneis, University of Cambridge                      */
-/*          Kathy Gray, University of Cambridge                           */
-/*          Peter Boehm, University of Cambridge (while working on Lem)   */
-/*          Peter Sewell, University of Cambridge                         */
-/*          Scott Owens, University of Kent                               */
-/*          Thomas Tuerk, University of Cambridge                         */
+/*  Copyright (c) 2013-2017                                               */
+/*    Kathyrn Gray                                                        */
+/*    Shaked Flur                                                         */
+/*    Stephen Kell                                                        */
+/*    Gabriel Kerneis                                                     */
+/*    Robert Norton-Wright                                                */
+/*    Christopher Pulte                                                   */
+/*    Peter Sewell                                                        */
 /*                                                                        */
-/*  The Lem sources are copyright 2010-2013                               */
-/*  by the UK authors above and Institut National de Recherche en         */
-/*  Informatique et en Automatique (INRIA).                               */
-/*                                                                        */
-/*  All files except ocaml-lib/pmap.{ml,mli} and ocaml-libpset.{ml,mli}   */
-/*  are distributed under the license below.  The former are distributed  */
-/*  under the LGPLv2, as in the LICENSE file.                             */
+/*  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.         */
+/*     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.  */
-/*  3. The names of the authors may not be used to endorse or promote     */
-/*  products derived from this software without specific prior written    */
-/*  permission.                                                           */
+/*     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 AUTHORS ``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 AUTHORS 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.                         */
+/*  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.                                                          */
 /**************************************************************************/
 
 %{
diff --git a/src/pp.ml b/src/pp.ml
index 0fa8636a..7da8aad3 100644
--- a/src/pp.ml
+++ b/src/pp.ml
@@ -1,47 +1,43 @@
 (**************************************************************************)
-(*                        Lem                                             *)
+(*     Sail                                                               *)
 (*                                                                        *)
-(*          Dominic Mulligan, University of Cambridge                     *)
-(*          Francesco Zappa Nardelli, INRIA Paris-Rocquencourt            *)
-(*          Gabriel Kerneis, University of Cambridge                      *)
-(*          Kathy Gray, University of Cambridge                           *)
-(*          Peter Boehm, University of Cambridge (while working on Lem)   *)
-(*          Peter Sewell, University of Cambridge                         *)
-(*          Scott Owens, University of Kent                               *)
-(*          Thomas Tuerk, University of Cambridge                         *)
+(*  Copyright (c) 2013-2017                                               *)
+(*    Kathyrn Gray                                                        *)
+(*    Shaked Flur                                                         *)
+(*    Stephen Kell                                                        *)
+(*    Gabriel Kerneis                                                     *)
+(*    Robert Norton-Wright                                                *)
+(*    Christopher Pulte                                                   *)
+(*    Peter Sewell                                                        *)
 (*                                                                        *)
-(*  The Lem sources are copyright 2010-2013                               *)
-(*  by the UK authors above and Institut National de Recherche en         *)
-(*  Informatique et en Automatique (INRIA).                               *)
-(*                                                                        *)
-(*  All files except ocaml-lib/pmap.{ml,mli} and ocaml-libpset.{ml,mli}   *)
-(*  are distributed under the license below.  The former are distributed  *)
-(*  under the LGPLv2, as in the LICENSE file.                             *)
+(*  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.         *)
+(*     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.  *)
-(*  3. The names of the authors may not be used to endorse or promote     *)
-(*  products derived from this software without specific prior written    *)
-(*  permission.                                                           *)
+(*     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 AUTHORS ``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 AUTHORS 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.                         *)
+(*  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.                                                          *)
 (**************************************************************************)
 
 (** pretty printing utilities *)
diff --git a/src/pp.mli b/src/pp.mli
index 2c7d6777..0613e433 100644
--- a/src/pp.mli
+++ b/src/pp.mli
@@ -1,47 +1,43 @@
 (**************************************************************************)
-(*                        Lem                                             *)
+(*     Sail                                                               *)
 (*                                                                        *)
-(*          Dominic Mulligan, University of Cambridge                     *)
-(*          Francesco Zappa Nardelli, INRIA Paris-Rocquencourt            *)
-(*          Gabriel Kerneis, University of Cambridge                      *)
-(*          Kathy Gray, University of Cambridge                           *)
-(*          Peter Boehm, University of Cambridge (while working on Lem)   *)
-(*          Peter Sewell, University of Cambridge                         *)
-(*          Scott Owens, University of Kent                               *)
-(*          Thomas Tuerk, University of Cambridge                         *)
+(*  Copyright (c) 2013-2017                                               *)
+(*    Kathyrn Gray                                                        *)
+(*    Shaked Flur                                                         *)
+(*    Stephen Kell                                                        *)
+(*    Gabriel Kerneis                                                     *)
+(*    Robert Norton-Wright                                                *)
+(*    Christopher Pulte                                                   *)
+(*    Peter Sewell                                                        *)
 (*                                                                        *)
-(*  The Lem sources are copyright 2010-2013                               *)
-(*  by the UK authors above and Institut National de Recherche en         *)
-(*  Informatique et en Automatique (INRIA).                               *)
-(*                                                                        *)
-(*  All files except ocaml-lib/pmap.{ml,mli} and ocaml-libpset.{ml,mli}   *)
-(*  are distributed under the license below.  The former are distributed  *)
-(*  under the LGPLv2, as in the LICENSE file.                             *)
+(*  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.         *)
+(*     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.  *)
-(*  3. The names of the authors may not be used to endorse or promote     *)
-(*  products derived from this software without specific prior written    *)
-(*  permission.                                                           *)
+(*     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 AUTHORS ``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 AUTHORS 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.                         *)
+(*  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 Format
diff --git a/src/pre_lexer.mll b/src/pre_lexer.mll
index e6534524..f648a594 100644
--- a/src/pre_lexer.mll
+++ b/src/pre_lexer.mll
@@ -1,47 +1,43 @@
 (**************************************************************************)
-(*                        Lem                                             *)
+(*     Sail                                                               *)
 (*                                                                        *)
-(*          Dominic Mulligan, University of Cambridge                     *)
-(*          Francesco Zappa Nardelli, INRIA Paris-Rocquencourt            *)
-(*          Gabriel Kerneis, University of Cambridge                      *)
-(*          Kathy Gray, University of Cambridge                           *)
-(*          Peter Boehm, University of Cambridge (while working on Lem)   *)
-(*          Peter Sewell, University of Cambridge                         *)
-(*          Scott Owens, University of Kent                               *)
-(*          Thomas Tuerk, University of Cambridge                         *)
+(*  Copyright (c) 2013-2017                                               *)
+(*    Kathyrn Gray                                                        *)
+(*    Shaked Flur                                                         *)
+(*    Stephen Kell                                                        *)
+(*    Gabriel Kerneis                                                     *)
+(*    Robert Norton-Wright                                                *)
+(*    Christopher Pulte                                                   *)
+(*    Peter Sewell                                                        *)
 (*                                                                        *)
-(*  The Lem sources are copyright 2010-2013                               *)
-(*  by the UK authors above and Institut National de Recherche en         *)
-(*  Informatique et en Automatique (INRIA).                               *)
-(*                                                                        *)
-(*  All files except ocaml-lib/pmap.{ml,mli} and ocaml-libpset.{ml,mli}   *)
-(*  are distributed under the license below.  The former are distributed  *)
-(*  under the LGPLv2, as in the LICENSE file.                             *)
+(*  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.         *)
+(*     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.  *)
-(*  3. The names of the authors may not be used to endorse or promote     *)
-(*  products derived from this software without specific prior written    *)
-(*  permission.                                                           *)
+(*     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 AUTHORS ``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 AUTHORS 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.                         *)
+(*  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.                                                          *)
 (**************************************************************************)
 
 {
diff --git a/src/pre_parser.mly b/src/pre_parser.mly
index 85a6bf25..b595d55d 100644
--- a/src/pre_parser.mly
+++ b/src/pre_parser.mly
@@ -1,47 +1,43 @@
 /**************************************************************************/
-/*                        Lem                                             */
+/*     Sail                                                               */
 /*                                                                        */
-/*          Dominic Mulligan, University of Cambridge                     */
-/*          Francesco Zappa Nardelli, INRIA Paris-Rocquencourt            */
-/*          Gabriel Kerneis, University of Cambridge                      */
-/*          Kathy Gray, University of Cambridge                           */
-/*          Peter Boehm, University of Cambridge (while working on Lem)   */
-/*          Peter Sewell, University of Cambridge                         */
-/*          Scott Owens, University of Kent                               */
-/*          Thomas Tuerk, University of Cambridge                         */
+/*  Copyright (c) 2013-2017                                               */
+/*    Kathyrn Gray                                                        */
+/*    Shaked Flur                                                         */
+/*    Stephen Kell                                                        */
+/*    Gabriel Kerneis                                                     */
+/*    Robert Norton-Wright                                                */
+/*    Christopher Pulte                                                   */
+/*    Peter Sewell                                                        */
 /*                                                                        */
-/*  The Lem sources are copyright 2010-2013                               */
-/*  by the UK authors above and Institut National de Recherche en         */
-/*  Informatique et en Automatique (INRIA).                               */
-/*                                                                        */
-/*  All files except ocaml-lib/pmap.{ml,mli} and ocaml-libpset.{ml,mli}   */
-/*  are distributed under the license below.  The former are distributed  */
-/*  under the LGPLv2, as in the LICENSE file.                             */
+/*  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.         */
+/*     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.  */
-/*  3. The names of the authors may not be used to endorse or promote     */
-/*  products derived from this software without specific prior written    */
-/*  permission.                                                           */
+/*     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 AUTHORS ``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 AUTHORS 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.                         */
+/*  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.                                                          */
 /**************************************************************************/
 
 %{
diff --git a/src/pretty_print.ml b/src/pretty_print.ml
index 0da54e53..415d48fd 100644
--- a/src/pretty_print.ml
+++ b/src/pretty_print.ml
@@ -1,3 +1,45 @@
+(**************************************************************************)
+(*     Sail                                                               *)
+(*                                                                        *)
+(*  Copyright (c) 2013-2017                                               *)
+(*    Kathyrn Gray                                                        *)
+(*    Shaked Flur                                                         *)
+(*    Stephen Kell                                                        *)
+(*    Gabriel Kerneis                                                     *)
+(*    Robert Norton-Wright                                                *)
+(*    Christopher Pulte                                                   *)
+(*    Peter Sewell                                                        *)
+(*                                                                        *)
+(*  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 Type_internal
 open Ast
 open Format
@@ -246,38 +288,38 @@ let pp_format_lit_lem (L_aux(lit,l)) =
 let pp_lem_lit ppf l = base ppf (pp_format_lit_lem l)
 
 
-let rec pp_format_t t =
+let rec pp_format_t_lem t =
   match t.t with
     | Tid i -> "(T_id \"" ^ i ^ "\")"
     | Tvar i -> "(T_var \"" ^ i ^ "\")"
-    | Tfn(t1,t2,_,e) -> "(T_fn " ^ (pp_format_t t1) ^ " " ^ (pp_format_t t2) ^ " " ^ pp_format_e e ^ ")"
-    | Ttup(tups) -> "(T_tup [" ^ (list_format "; " pp_format_t tups) ^ "])"
-    | Tapp(i,args) -> "(T_app \"" ^ i ^ "\" (T_args [" ^  list_format "; " pp_format_targ args ^ "]))"
-    | Tabbrev(ti,ta) -> "(T_abbrev " ^ (pp_format_t ti) ^ " " ^ (pp_format_t ta) ^ ")"
+    | Tfn(t1,t2,_,e) -> "(T_fn " ^ (pp_format_t_lem t1) ^ " " ^ (pp_format_t_lem t2) ^ " " ^ pp_format_e_lem e ^ ")"
+    | Ttup(tups) -> "(T_tup [" ^ (list_format "; " pp_format_t_lem tups) ^ "])"
+    | Tapp(i,args) -> "(T_app \"" ^ i ^ "\" (T_args [" ^  list_format "; " pp_format_targ_lem args ^ "]))"
+    | Tabbrev(ti,ta) -> "(T_abbrev " ^ (pp_format_t_lem ti) ^ " " ^ (pp_format_t_lem ta) ^ ")"
     | Tuvar(_) -> "(T_var \"fresh_v\")"
     | Toptions _ -> "(T_var \"fresh_v\")"
-and pp_format_targ = function
-  | TA_typ t -> "(T_arg_typ " ^ pp_format_t t ^ ")"
-  | TA_nexp n -> "(T_arg_nexp " ^ pp_format_n n ^ ")"
-  | TA_eft e -> "(T_arg_effect " ^ pp_format_e e ^ ")"
-  | TA_ord o -> "(T_arg_order " ^ pp_format_o o ^ ")"
-and pp_format_n n =
+and pp_format_targ_lem = function
+  | TA_typ t -> "(T_arg_typ " ^ pp_format_t_lem t ^ ")"
+  | TA_nexp n -> "(T_arg_nexp " ^ pp_format_n_lem n ^ ")"
+  | TA_eft e -> "(T_arg_effect " ^ pp_format_e_lem e ^ ")"
+  | TA_ord o -> "(T_arg_order " ^ pp_format_o_lem o ^ ")"
+and pp_format_n_lem n =
   match n.nexp with
   | Nid (i, n) -> "(Ne_id \"" ^ i ^ " " ^ "\")"
   | Nvar i -> "(Ne_var \"" ^ i ^ "\")"
   | Nconst i -> "(Ne_const " ^ (lemnum string_of_int (int_of_big_int i)) ^ ")"
   | Npos_inf -> "Ne_inf"
-  | Nadd(n1,n2) -> "(Ne_add [" ^ (pp_format_n n1) ^ "; " ^ (pp_format_n n2) ^ "])"
-  | Nsub(n1,n2) -> "(Ne_minus "^ (pp_format_n n1) ^ " " ^ (pp_format_n n2) ^ ")"
-  | Nmult(n1,n2) -> "(Ne_mult " ^ (pp_format_n n1) ^ " " ^ (pp_format_n n2) ^ ")"
-  | N2n(n,Some i) -> "(Ne_exp " ^ (pp_format_n n) ^ "(*" ^ string_of_big_int i ^ "*)" ^ ")"
-  | N2n(n,None) -> "(Ne_exp " ^ (pp_format_n n) ^ ")"
-  | Nneg n -> "(Ne_unary " ^ (pp_format_n n) ^ ")"
+  | Nadd(n1,n2) -> "(Ne_add [" ^ (pp_format_n_lem n1) ^ "; " ^ (pp_format_n_lem n2) ^ "])"
+  | Nsub(n1,n2) -> "(Ne_minus "^ (pp_format_n_lem n1) ^ " " ^ (pp_format_n_lem n2) ^ ")"
+  | Nmult(n1,n2) -> "(Ne_mult " ^ (pp_format_n_lem n1) ^ " " ^ (pp_format_n_lem n2) ^ ")"
+  | N2n(n,Some i) -> "(Ne_exp " ^ (pp_format_n_lem n) ^ "(*" ^ string_of_big_int i ^ "*)" ^ ")"
+  | N2n(n,None) -> "(Ne_exp " ^ (pp_format_n_lem n) ^ ")"
+  | Nneg n -> "(Ne_unary " ^ (pp_format_n_lem n) ^ ")"
   | Nuvar _ -> "(Ne_var \"fresh_v_" ^ string_of_int (get_index n) ^ "\")"
   | Nneg_inf -> "(Ne_unary Ne_inf)"
   | Npow _ -> "power_not_implemented"
   | Ninexact -> "(Ne_add Ne_inf (Ne_unary Ne_inf)"
-and pp_format_e e =
+and pp_format_e_lem e =
   "(Effect_aux " ^
   (match e.effect with
   | Evar i -> "(Effect_var (Kid_aux (Var \"" ^ i ^ "\") Unknown))"
@@ -285,7 +327,7 @@ and pp_format_e e =
                   (list_format "; " pp_format_base_effect_lem es) ^ " ])"
   | Euvar(_) -> "(Effect_var (Kid_aux (Var \"fresh_v\") Unknown))")
   ^ " Unknown)"
-and pp_format_o o =
+and pp_format_o_lem o =
   "(Ord_aux " ^
   (match o.order with
   | Ovar i -> "(Ord_var (Kid_aux (Var \"" ^ i ^ "\") Unknown))"
@@ -312,9 +354,9 @@ let rec pp_format_nes nes =
   "[" ^ (*
   (list_format "; "
      (fun ne -> match ne with
-       | LtEq(_,n1,n2) -> "(Nec_lteq " ^ pp_format_n n1 ^ " " ^ pp_format_n n2 ^ ")"
-       | Eq(_,n1,n2) -> "(Nec_eq " ^ pp_format_n n1 ^ " " ^ pp_format_n n2 ^ ")"
-       | GtEq(_,n1,n2) -> "(Nec_gteq " ^ pp_format_n n1 ^ " " ^ pp_format_n n2 ^ ")"
+       | LtEq(_,n1,n2) -> "(Nec_lteq " ^ pp_format_n_lem n1 ^ " " ^ pp_format_n_lem n2 ^ ")"
+       | Eq(_,n1,n2) -> "(Nec_eq " ^ pp_format_n_lem n1 ^ " " ^ pp_format_n_lem n2 ^ ")"
+       | GtEq(_,n1,n2) -> "(Nec_gteq " ^ pp_format_n_lem n1 ^ " " ^ pp_format_n_lem n2 ^ ")"
        | In(_,i,ns) | InS(_,{nexp=Nvar i},ns) ->
          "(Nec_in \"" ^ i ^ "\" [" ^ (list_format "; " string_of_int ns)^ "])"
        | InS(_,_,ns)  ->
@@ -330,8 +372,8 @@ let pp_format_annot = function
   | NoTyp -> "Nothing"
   | Base((_,t),tag,nes,efct,efctsum,_) ->
     (*TODO print out bindings for use in pattern match in interpreter*)
-     "(Just (" ^ pp_format_t t ^ ", " ^ pp_format_tag tag ^ ", " ^ pp_format_nes nes ^ ", " ^
-       pp_format_e efct ^ ", " ^ pp_format_e efctsum ^ "))"
+     "(Just (" ^ pp_format_t_lem t ^ ", " ^ pp_format_tag tag ^ ", " ^ pp_format_nes nes ^ ", " ^
+       pp_format_e_lem efct ^ ", " ^ pp_format_e_lem efctsum ^ "))"
   | Overload _ -> "Nothing"
 
 let pp_annot ppf ant = base ppf (pp_format_annot ant)
@@ -675,6 +717,116 @@ let pp_lem_defs ppf (Defs(defs)) =
   fprintf ppf "Defs [@[%a@]]@\n" (list_pp pp_lem_def pp_lem_def) defs
 
 
+
+(* **************************************************************************
+   * pp from tannot to ASCII source, for pp of built-in type environment
+*)
+
+
+
+let rec pp_format_t_ascii t =
+  match t.t with
+    | Tid i -> i
+    | Tvar i -> "'" ^ i
+    | Tfn(t1,t2,_,e) -> (pp_format_t_ascii t1) ^ " -> " ^ (pp_format_t_ascii t2) ^ " effect " ^ pp_format_e_ascii e 
+    | Ttup(tups) -> "(" ^ (list_format ", " pp_format_t_ascii tups) ^ ")"
+    | Tapp(i,args) ->  i ^ "<" ^  list_format ", " pp_format_targ_ascii args ^ ">"
+    | Tabbrev(ti,ta) -> (pp_format_t_ascii ti) (* (pp_format_t_ascii ta) *)
+    | Tuvar(_) -> failwith "Tuvar in pp_format_t_ascii"
+    | Toptions _ -> failwith "Toptions in pp_format_t_ascii"
+and pp_format_targ_ascii = function
+  | TA_typ t ->  pp_format_t_ascii t
+  | TA_nexp n -> pp_format_n_ascii n
+  | TA_eft e ->  pp_format_e_ascii e
+  | TA_ord o ->  pp_format_o_ascii o
+and pp_format_n_ascii n =
+  match n.nexp with
+  | Nid (i, n) -> i (* from an abbreviation *)
+  | Nvar i -> "'" ^ i
+  | Nconst i -> (string_of_int (int_of_big_int i))
+  | Npos_inf -> "infinity"
+  | Nadd(n1,n2) -> (pp_format_n_ascii n1) ^ "+" ^ (pp_format_n_ascii n2)
+  | Nsub(n1,n2) -> (pp_format_n_ascii n1) ^ "-" ^ (pp_format_n_ascii n2)
+  | Nmult(n1,n2) -> (pp_format_n_ascii n1) ^ "*" ^ (pp_format_n_ascii n2)
+  | N2n(n,_) -> "2**"^(pp_format_n_ascii n) (* string_of_big_int i ^ *)
+  | Nneg n -> "-" ^ (pp_format_n_ascii n) 
+  | Nuvar _ -> failwith "Nuvar in pp_format_n_ascii"
+  | Nneg_inf -> "-infinity"
+  | Npow _ -> failwith "Npow in pp_format_n_ascii"
+  | Ninexact -> failwith "Ninexact in pp_format_n_ascii"
+and pp_format_e_ascii e =
+  match e.effect with
+  | Evar i -> "'" ^ i
+  | Eset es -> "{" ^
+                  (list_format ", " pp_format_base_effect_ascii es) ^ "}"
+  | Euvar(_) -> failwith "Euvar in pp_format_e_ascii"
+and pp_format_o_ascii o =
+  match o.order with
+  | Ovar i -> "'" ^ i
+  | Oinc -> "inc"
+  | Odec -> "dec"
+  | Ouvar(_) -> failwith "Ouvar in pp_format_o_ascii"
+and pp_format_base_effect_ascii (BE_aux(e,l)) =
+  match e with
+    | BE_rreg -> "rreg"
+    | BE_wreg -> "wreg"
+    | BE_rmem -> "rmem"
+    | BE_wmem -> "wmem"
+    | BE_wmv  -> "wmv"
+    | BE_eamem -> "eamem"
+    | BE_barr -> "barr"
+    | BE_depend -> "depend"
+    | BE_undef -> "undef"
+    | BE_unspec -> "unspec"
+    | BE_nondet -> "nondet"
+    | BE_lset -> "lset"
+    | BE_lret -> "lret"
+    | BE_escape -> "escape"
+
+and pp_format_nes_ascii nes =
+  list_format ", " pp_format_ne_ascii nes
+
+and pp_format_ne_ascii ne =
+  match ne with
+  | Lt(_,_,n1,n2) -> pp_format_n_ascii n1 ^ " < " ^ pp_format_n_ascii n2
+  | LtEq(_,_,n1,n2) -> pp_format_n_ascii n1 ^ " <= " ^ pp_format_n_ascii n2
+  | NtEq(_,n1,n2) ->   pp_format_n_ascii n1 ^ " != " ^ pp_format_n_ascii n2
+  | Eq(_,n1,n2) ->   pp_format_n_ascii n1 ^ " = " ^ pp_format_n_ascii n2
+  | GtEq(_,_,n1,n2) -> pp_format_n_ascii n1 ^ " >= " ^ pp_format_n_ascii n2
+  | Gt(_,_,n1,n2) -> pp_format_n_ascii n1 ^ " > " ^ pp_format_n_ascii n2
+  | In(_,i,ns) | InS(_,{nexp=Nvar i},ns) ->
+  i ^ " IN {" ^ (list_format ", " string_of_int ns)^ "}"
+  | InS(_,_,ns)  -> (* when the variable has been replaced by a unification variable, we use this *)
+  failwith "InS in pp_format_nes_ascii" (*"(Nec_in \"fresh\" [" ^ (list_format "; " string_of_int ns)^ "])"*)
+  | Predicate(_,n1,n2) -> "flow_constraints(" ^ pp_format_ne_ascii n1 ^", "^ pp_format_ne_ascii n2 ^")"
+  | CondCons(_,_,_,nes_c,nes_t) ->
+  failwith "CondCons in pp_format_nes_ascii" (*"(Nec_cond " ^ (pp_format_nes nes_c) ^ " " ^ (pp_format_nes nes_t) ^ ")"*)
+  | BranchCons(_,_,nes_b) ->
+  failwith "BranchCons in pp_format_nes_ascii" (*"(Nec_branch " ^ (pp_format_nes nes_b) ^ ")"*)
+
+
+
+let rec pp_format_annot_ascii = function
+  | NoTyp -> "Nothing"
+  | Base((targs,t),tag,nes,efct,efctsum,_) ->
+    (*TODO print out bindings for use in pattern match in interpreter*)
+     "forall " ^ list_format ", " (function (i,k) -> kind_to_string k ^" "^ i) targs ^ 
+  (match nes with [] -> "" | _ -> ", " ^ pp_format_nes_ascii nes)
+  ^ ". "
+  ^ pp_format_t_ascii t 
+
+(*
+^ " ********** " ^ pp_format_tag tag ^ ", " ^ pp_format_nes nes ^ ", " ^
+       pp_format_e_lem efct ^ ", " ^ pp_format_e_lem efctsum ^ "))"
+*)
+  | Overload (tannot, return_type_overloading_allowed, tannots) -> 
+  pp_format_annot_ascii tannot ^ "\n" ^ String.concat "" (List.map (function tannot' -> "    " ^ pp_format_annot_ascii tannot' ^ "\n") tannots)
+
+
+
+
+
+
 (****************************************************************************
  * PPrint-based source-to-source pretty printer
 ****************************************************************************)
diff --git a/src/pretty_print.mli b/src/pretty_print.mli
index 500d19e2..9a002454 100644
--- a/src/pretty_print.mli
+++ b/src/pretty_print.mli
@@ -1,3 +1,45 @@
+(**************************************************************************)
+(*     Sail                                                               *)
+(*                                                                        *)
+(*  Copyright (c) 2013-2017                                               *)
+(*    Kathyrn Gray                                                        *)
+(*    Shaked Flur                                                         *)
+(*    Stephen Kell                                                        *)
+(*    Gabriel Kerneis                                                     *)
+(*    Robert Norton-Wright                                                *)
+(*    Christopher Pulte                                                   *)
+(*    Peter Sewell                                                        *)
+(*                                                                        *)
+(*  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 Ast
 open Type_internal
 
@@ -11,3 +53,6 @@ val pp_lem_defs : Format.formatter -> tannot defs -> unit
 
 val pp_defs_ocaml : out_channel -> tannot defs -> string -> string list -> unit
 val pp_defs_lem : (out_channel * string list) -> (out_channel * string list) -> (out_channel * string list) -> tannot defs -> string -> unit
+
+
+val pp_format_annot_ascii : tannot -> string
diff --git a/src/process_file.ml b/src/process_file.ml
index cda44e77..273979cf 100644
--- a/src/process_file.ml
+++ b/src/process_file.ml
@@ -1,47 +1,43 @@
 (**************************************************************************)
-(*                        Lem                                             *)
+(*     Sail                                                               *)
 (*                                                                        *)
-(*          Dominic Mulligan, University of Cambridge                     *)
-(*          Francesco Zappa Nardelli, INRIA Paris-Rocquencourt            *)
-(*          Gabriel Kerneis, University of Cambridge                      *)
-(*          Kathy Gray, University of Cambridge                           *)
-(*          Peter Boehm, University of Cambridge (while working on Lem)   *)
-(*          Peter Sewell, University of Cambridge                         *)
-(*          Scott Owens, University of Kent                               *)
-(*          Thomas Tuerk, University of Cambridge                         *)
+(*  Copyright (c) 2013-2017                                               *)
+(*    Kathyrn Gray                                                        *)
+(*    Shaked Flur                                                         *)
+(*    Stephen Kell                                                        *)
+(*    Gabriel Kerneis                                                     *)
+(*    Robert Norton-Wright                                                *)
+(*    Christopher Pulte                                                   *)
+(*    Peter Sewell                                                        *)
 (*                                                                        *)
-(*  The Lem sources are copyright 2010-2013                               *)
-(*  by the UK authors above and Institut National de Recherche en         *)
-(*  Informatique et en Automatique (INRIA).                               *)
-(*                                                                        *)
-(*  All files except ocaml-lib/pmap.{ml,mli} and ocaml-libpset.{ml,mli}   *)
-(*  are distributed under the license below.  The former are distributed  *)
-(*  under the LGPLv2, as in the LICENSE file.                             *)
+(*  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.         *)
+(*     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.  *)
-(*  3. The names of the authors may not be used to endorse or promote     *)
-(*  products derived from this software without specific prior written    *)
-(*  permission.                                                           *)
+(*     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 AUTHORS ``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 AUTHORS 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.                         *)
+(*  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 Type_internal
diff --git a/src/process_file.mli b/src/process_file.mli
index 66b1d8af..2c18b830 100644
--- a/src/process_file.mli
+++ b/src/process_file.mli
@@ -1,47 +1,43 @@
 (**************************************************************************)
-(*                        Lem                                             *)
+(*     Sail                                                               *)
 (*                                                                        *)
-(*          Dominic Mulligan, University of Cambridge                     *)
-(*          Francesco Zappa Nardelli, INRIA Paris-Rocquencourt            *)
-(*          Gabriel Kerneis, University of Cambridge                      *)
-(*          Kathy Gray, University of Cambridge                           *)
-(*          Peter Boehm, University of Cambridge (while working on Lem)   *)
-(*          Peter Sewell, University of Cambridge                         *)
-(*          Scott Owens, University of Kent                               *)
-(*          Thomas Tuerk, University of Cambridge                         *)
+(*  Copyright (c) 2013-2017                                               *)
+(*    Kathyrn Gray                                                        *)
+(*    Shaked Flur                                                         *)
+(*    Stephen Kell                                                        *)
+(*    Gabriel Kerneis                                                     *)
+(*    Robert Norton-Wright                                                *)
+(*    Christopher Pulte                                                   *)
+(*    Peter Sewell                                                        *)
 (*                                                                        *)
-(*  The Lem sources are copyright 2010-2013                               *)
-(*  by the UK authors above and Institut National de Recherche en         *)
-(*  Informatique et en Automatique (INRIA).                               *)
-(*                                                                        *)
-(*  All files except ocaml-lib/pmap.{ml,mli} and ocaml-libpset.{ml,mli}   *)
-(*  are distributed under the license below.  The former are distributed  *)
-(*  under the LGPLv2, as in the LICENSE file.                             *)
+(*  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.         *)
+(*     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.  *)
-(*  3. The names of the authors may not be used to endorse or promote     *)
-(*  products derived from this software without specific prior written    *)
-(*  permission.                                                           *)
+(*     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 AUTHORS ``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 AUTHORS 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.                         *)
+(*  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.                                                          *)
 (**************************************************************************)
 
 val parse_file : string -> Parse_ast.defs
diff --git a/src/reporting_basic.ml b/src/reporting_basic.ml
index 0e2a2e17..5ff43208 100644
--- a/src/reporting_basic.ml
+++ b/src/reporting_basic.ml
@@ -1,4 +1,47 @@
 (**************************************************************************)
+(*     Sail                                                               *)
+(*                                                                        *)
+(*  Copyright (c) 2013-2017                                               *)
+(*    Kathyrn Gray                                                        *)
+(*    Shaked Flur                                                         *)
+(*    Stephen Kell                                                        *)
+(*    Gabriel Kerneis                                                     *)
+(*    Robert Norton-Wright                                                *)
+(*    Christopher Pulte                                                   *)
+(*    Peter Sewell                                                        *)
+(*                                                                        *)
+(*  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.                                                          *)
+(**************************************************************************)
+
+
+(**************************************************************************)
 (*                        Lem                                             *)
 (*                                                                        *)
 (*          Dominic Mulligan, University of Cambridge                     *)
diff --git a/src/reporting_basic.mli b/src/reporting_basic.mli
index 7362d44c..559be9d4 100644
--- a/src/reporting_basic.mli
+++ b/src/reporting_basic.mli
@@ -1,47 +1,43 @@
 (**************************************************************************)
-(*                        Lem                                             *)
+(*     Sail                                                               *)
 (*                                                                        *)
-(*          Dominic Mulligan, University of Cambridge                     *)
-(*          Francesco Zappa Nardelli, INRIA Paris-Rocquencourt            *)
-(*          Gabriel Kerneis, University of Cambridge                      *)
-(*          Kathy Gray, University of Cambridge                           *)
-(*          Peter Boehm, University of Cambridge (while working on Lem)   *)
-(*          Peter Sewell, University of Cambridge                         *)
-(*          Scott Owens, University of Kent                               *)
-(*          Thomas Tuerk, University of Cambridge                         *)
+(*  Copyright (c) 2013-2017                                               *)
+(*    Kathyrn Gray                                                        *)
+(*    Shaked Flur                                                         *)
+(*    Stephen Kell                                                        *)
+(*    Gabriel Kerneis                                                     *)
+(*    Robert Norton-Wright                                                *)
+(*    Christopher Pulte                                                   *)
+(*    Peter Sewell                                                        *)
 (*                                                                        *)
-(*  The Lem sources are copyright 2010-2013                               *)
-(*  by the UK authors above and Institut National de Recherche en         *)
-(*  Informatique et en Automatique (INRIA).                               *)
-(*                                                                        *)
-(*  All files except ocaml-lib/pmap.{ml,mli} and ocaml-libpset.{ml,mli}   *)
-(*  are distributed under the license below.  The former are distributed  *)
-(*  under the LGPLv2, as in the LICENSE file.                             *)
+(*  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.         *)
+(*     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.  *)
-(*  3. The names of the authors may not be used to endorse or promote     *)
-(*  products derived from this software without specific prior written    *)
-(*  permission.                                                           *)
+(*     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 AUTHORS ``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 AUTHORS 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.                         *)
+(*  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.                                                          *)
 (**************************************************************************)
 
 (** Basic error reporting
diff --git a/src/rewriter.ml b/src/rewriter.ml
index 8582f3b5..dc96b952 100644
--- a/src/rewriter.ml
+++ b/src/rewriter.ml
@@ -1,3 +1,45 @@
+(**************************************************************************)
+(*     Sail                                                               *)
+(*                                                                        *)
+(*  Copyright (c) 2013-2017                                               *)
+(*    Kathyrn Gray                                                        *)
+(*    Shaked Flur                                                         *)
+(*    Stephen Kell                                                        *)
+(*    Gabriel Kerneis                                                     *)
+(*    Robert Norton-Wright                                                *)
+(*    Christopher Pulte                                                   *)
+(*    Peter Sewell                                                        *)
+(*                                                                        *)
+(*  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 Big_int
 open Ast
 open Type_internal
diff --git a/src/rewriter.mli b/src/rewriter.mli
index d1d642ff..615d0fa0 100644
--- a/src/rewriter.mli
+++ b/src/rewriter.mli
@@ -1,3 +1,45 @@
+(**************************************************************************)
+(*     Sail                                                               *)
+(*                                                                        *)
+(*  Copyright (c) 2013-2017                                               *)
+(*    Kathyrn Gray                                                        *)
+(*    Shaked Flur                                                         *)
+(*    Stephen Kell                                                        *)
+(*    Gabriel Kerneis                                                     *)
+(*    Robert Norton-Wright                                                *)
+(*    Christopher Pulte                                                   *)
+(*    Peter Sewell                                                        *)
+(*                                                                        *)
+(*  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 Big_int
 open Ast
 open Type_internal
diff --git a/src/sail.ml b/src/sail.ml
index 80560746..1230288b 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -1,47 +1,43 @@
 (**************************************************************************)
-(*                        Lem                                             *)
+(*     Sail                                                               *)
 (*                                                                        *)
-(*          Dominic Mulligan, University of Cambridge                     *)
-(*          Francesco Zappa Nardelli, INRIA Paris-Rocquencourt            *)
-(*          Gabriel Kerneis, University of Cambridge                      *)
-(*          Kathy Gray, University of Cambridge                           *)
-(*          Peter Boehm, University of Cambridge (while working on Lem)   *)
-(*          Peter Sewell, University of Cambridge                         *)
-(*          Scott Owens, University of Kent                               *)
-(*          Thomas Tuerk, University of Cambridge                         *)
+(*  Copyright (c) 2013-2017                                               *)
+(*    Kathyrn Gray                                                        *)
+(*    Shaked Flur                                                         *)
+(*    Stephen Kell                                                        *)
+(*    Gabriel Kerneis                                                     *)
+(*    Robert Norton-Wright                                                *)
+(*    Christopher Pulte                                                   *)
+(*    Peter Sewell                                                        *)
 (*                                                                        *)
-(*  The Lem sources are copyright 2010-2013                               *)
-(*  by the UK authors above and Institut National de Recherche en         *)
-(*  Informatique et en Automatique (INRIA).                               *)
-(*                                                                        *)
-(*  All files except ocaml-lib/pmap.{ml,mli} and ocaml-libpset.{ml,mli}   *)
-(*  are distributed under the license below.  The former are distributed  *)
-(*  under the LGPLv2, as in the LICENSE file.                             *)
+(*  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.         *)
+(*     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.  *)
-(*  3. The names of the authors may not be used to endorse or promote     *)
-(*  products derived from this software without specific prior written    *)
-(*  permission.                                                           *)
+(*     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 AUTHORS ``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 AUTHORS 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.                         *)
+(*  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 Process_file
@@ -104,6 +100,18 @@ let main() =
   if !(opt_print_version)
   then Printf.printf "Sail private release \n"
   else
+    let ppd_initial_typ_env = 
+      String.concat "" 
+        (List.map 
+           (function (id,tannot) ->
+             id ^ " : " ^ 
+             Pretty_print.pp_format_annot_ascii tannot 
+             ^ "\n")
+           (Type_internal.Envmap.to_list Type_internal.initial_typ_env)) in
+    Printf.printf "%s" ppd_initial_typ_env ;
+
+    
+
     let parsed = (List.map (fun f -> (f,(parse_file f)))  !opt_file_arguments) in
     let ast = 
       List.fold_right (fun (_,(Parse_ast.Defs ast_nodes)) (Parse_ast.Defs later_nodes) 
diff --git a/src/sail_lib.ml b/src/sail_lib.ml
index 4cfc1331..df2b6d61 100644
--- a/src/sail_lib.ml
+++ b/src/sail_lib.ml
@@ -1,3 +1,45 @@
+(**************************************************************************)
+(*     Sail                                                               *)
+(*                                                                        *)
+(*  Copyright (c) 2013-2017                                               *)
+(*    Kathyrn Gray                                                        *)
+(*    Shaked Flur                                                         *)
+(*    Stephen Kell                                                        *)
+(*    Gabriel Kerneis                                                     *)
+(*    Robert Norton-Wright                                                *)
+(*    Christopher Pulte                                                   *)
+(*    Peter Sewell                                                        *)
+(*                                                                        *)
+(*  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.                                                          *)
+(**************************************************************************)
+
 (** A Sail library *)
 
 (* This library is not well-thought. It has grown driven by the need to
diff --git a/src/spec_analysis.ml b/src/spec_analysis.ml
index bddeb28c..8cb5a796 100644
--- a/src/spec_analysis.ml
+++ b/src/spec_analysis.ml
@@ -1,3 +1,45 @@
+(**************************************************************************)
+(*     Sail                                                               *)
+(*                                                                        *)
+(*  Copyright (c) 2013-2017                                               *)
+(*    Kathyrn Gray                                                        *)
+(*    Shaked Flur                                                         *)
+(*    Stephen Kell                                                        *)
+(*    Gabriel Kerneis                                                     *)
+(*    Robert Norton-Wright                                                *)
+(*    Christopher Pulte                                                   *)
+(*    Peter Sewell                                                        *)
+(*                                                                        *)
+(*  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 Ast
 open Util
 open Big_int
diff --git a/src/spec_analysis.mli b/src/spec_analysis.mli
index 068b3778..fa8dad3b 100644
--- a/src/spec_analysis.mli
+++ b/src/spec_analysis.mli
@@ -1,3 +1,45 @@
+(**************************************************************************)
+(*     Sail                                                               *)
+(*                                                                        *)
+(*  Copyright (c) 2013-2017                                               *)
+(*    Kathyrn Gray                                                        *)
+(*    Shaked Flur                                                         *)
+(*    Stephen Kell                                                        *)
+(*    Gabriel Kerneis                                                     *)
+(*    Robert Norton-Wright                                                *)
+(*    Christopher Pulte                                                   *)
+(*    Peter Sewell                                                        *)
+(*                                                                        *)
+(*  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 Ast
 open Util
 open Big_int
diff --git a/src/test/mips/test_cp2_csetbounds_cases.elf b/src/test/mips/test_cp2_csetbounds_cases.elf
new file mode 100755
index 00000000..9ba8ab94
--- /dev/null
+++ b/src/test/mips/test_cp2_csetbounds_cases.elf
diff --git a/src/type_check.ml b/src/type_check.ml
index 63942df8..c4119281 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -1,3 +1,45 @@
+(**************************************************************************)
+(*     Sail                                                               *)
+(*                                                                        *)
+(*  Copyright (c) 2013-2017                                               *)
+(*    Kathyrn Gray                                                        *)
+(*    Shaked Flur                                                         *)
+(*    Stephen Kell                                                        *)
+(*    Gabriel Kerneis                                                     *)
+(*    Robert Norton-Wright                                                *)
+(*    Christopher Pulte                                                   *)
+(*    Peter Sewell                                                        *)
+(*                                                                        *)
+(*  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 Big_int
 open Ast
 open Type_internal
diff --git a/src/type_check.mli b/src/type_check.mli
index 02fd2a80..4f78dd03 100644
--- a/src/type_check.mli
+++ b/src/type_check.mli
@@ -1,3 +1,45 @@
+(**************************************************************************)
+(*     Sail                                                               *)
+(*                                                                        *)
+(*  Copyright (c) 2013-2017                                               *)
+(*    Kathyrn Gray                                                        *)
+(*    Shaked Flur                                                         *)
+(*    Stephen Kell                                                        *)
+(*    Gabriel Kerneis                                                     *)
+(*    Robert Norton-Wright                                                *)
+(*    Christopher Pulte                                                   *)
+(*    Peter Sewell                                                        *)
+(*                                                                        *)
+(*  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 Ast
 open Type_internal
 type kind = Type_internal.kind
diff --git a/src/type_internal.ml b/src/type_internal.ml
index 2770d827..b26a7ebd 100644
--- a/src/type_internal.ml
+++ b/src/type_internal.ml
@@ -1,3 +1,45 @@
+(**************************************************************************)
+(*     Sail                                                               *)
+(*                                                                        *)
+(*  Copyright (c) 2013-2017                                               *)
+(*    Kathyrn Gray                                                        *)
+(*    Shaked Flur                                                         *)
+(*    Stephen Kell                                                        *)
+(*    Gabriel Kerneis                                                     *)
+(*    Robert Norton-Wright                                                *)
+(*    Christopher Pulte                                                   *)
+(*    Peter Sewell                                                        *)
+(*                                                                        *)
+(*  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 Ast
 open Util
 open Big_int
@@ -200,7 +242,7 @@ type tannot =
   (*See .mli for purpose of attributes *)
   | Base of (t_params * t) * tag * nexp_range list * effect * effect * bounds_env
   (* First tannot is the most polymorphic version; the list includes all variants. All included t are Tfn *)
-  | Overload of tannot * bool * tannot list 
+  | Overload of tannot * bool * tannot list    (* these tannot's should all be Base *)
 
 type 'a emap = 'a Envmap.t
 
@@ -1842,10 +1884,15 @@ let rec refine_requires check_nvar min_lt max_gt id cs =
 
 let nat_t = {t = Tapp("range",[TA_nexp n_zero;TA_nexp (mk_p_inf());])}
 let int_t = {t = Tapp("range",[TA_nexp (mk_n_inf());TA_nexp (mk_p_inf());])}
-let uint8_t = {t = Tapp("range",[TA_nexp n_zero; TA_nexp (mk_2nc (mk_c_int 8) (big_int_of_int 256))])}
-let uint16_t = {t = Tapp("range",[TA_nexp n_zero; TA_nexp (mk_2nc (mk_c_int 16) (big_int_of_int 65536))])}
-let uint32_t = {t = Tapp("range",[TA_nexp n_zero; TA_nexp (mk_2nc (mk_c_int 32) (big_int_of_string "4294967296"))])}
-let uint64_t = {t = Tapp("range",[TA_nexp n_zero; TA_nexp (mk_2nc (mk_c_int 64) (big_int_of_string "18446744073709551616"))])}
+let uint8_t = {t = Tapp("range",[TA_nexp n_zero; TA_nexp (mk_sub (mk_2nc (mk_c_int 8) (big_int_of_int 256)) n_one)])}
+let uint16_t = {t = Tapp("range",[TA_nexp n_zero;
+                                  TA_nexp (mk_sub (mk_2nc (mk_c_int 16) (big_int_of_int 65536)) n_one)])}
+let uint32_t = {t = Tapp("range",[TA_nexp n_zero;
+                                  TA_nexp (mk_sub (mk_2nc (mk_c_int 32) (big_int_of_string "4294967296")) n_one)])}
+let uint64_t = {t = Tapp("range",[TA_nexp n_zero;
+                                  TA_nexp (mk_sub (mk_2nc (mk_c_int 64) (big_int_of_string "18446744073709551616"))
+                                             (mk_c_int 1))
+                                 ])}
 
 let int8_t = {t = Tapp("range", [TA_nexp (mk_neg (mk_2nc (mk_c_int 7) (big_int_of_int 128))) ;
                                  TA_nexp (mk_c_int 127)])}
@@ -1954,7 +2001,7 @@ let mk_bitwise_op name symb arity =
              (*lib_tannot (["n",{k=K_Nat};"o",{k=K_Ord}],mk_pure_fun svarg single_bit_vec_typ) (Some name) [];*)
              lib_tannot ([],mk_pure_fun barg bit_t) (Some (name ^ "_bit")) []]))
 
-let initial_typ_env =
+let initial_typ_env : tannot Envmap.t =
   Envmap.from_list [
     ("ignore",lib_tannot ([("a",{k=K_Typ})],mk_pure_fun {t=Tvar "a"} unit_t) None []);
     ("Some", Base((["a",{k=K_Typ}], mk_pure_fun {t=Tvar "a"} {t=Tapp("option", [TA_typ {t=Tvar "a"}])}),
@@ -2703,6 +2750,7 @@ let initial_typ_env =
                         (mk_atom (mk_nv "o")))),
           External (Some "min"),[],pure_e,pure_e,nob));
   ]
+
     
 
 let rec typ_subst s_env leave_imp t =
@@ -3350,6 +3398,12 @@ let rec type_coerce_internal co d_env enforce is_explicit widen bounds t1 cs1 e
   (*let _ = Printf.eprintf "called type_coerce_internal is_explicit %b, widen %b, turning %s with actual %s into %s with actual %s\n" 
     is_explicit widen (t_to_string t1) (t_to_string t1_actual) (t_to_string t2) (t_to_string t2_actual) in*)
   match t1_actual.t,t2_actual.t with
+
+    (* Toptions is an internal constructor representing the type we're
+    going to be casting to and the natural type.  source-language type
+    annotations might be demanding a coercion, so this checks
+    conformance and adds a coercion if needed *)
+
   | Toptions(to1,Some to2),_ -> 
     if (conforms_to_t d_env false true to1 t2_actual || conforms_to_t d_env false true to2 t2_actual)
     then begin t1_actual.t <- t2_actual.t; (t2,csp,pure_e,e) end
@@ -3362,12 +3416,17 @@ let rec type_coerce_internal co d_env enforce is_explicit widen bounds t1 cs1 e
   | _,Toptions(to1,Some to2) -> 
     if (conforms_to_t d_env false true to1 t1_actual || conforms_to_t d_env false true to2 t1_actual)
     then begin t2_actual.t <- t1_actual.t; (t1,csp,pure_e,e) end
-    else eq_error l ((t_to_string t1) ^ " can match neither expexted type " ^
+    else eq_error l ((t_to_string t1) ^ " can match neither expected type " ^
                         (t_to_string to1) ^ " nor " ^ (t_to_string to2))
   | _,Toptions(to1,None) -> 
     if is_explicit
     then type_coerce_internal co d_env enforce is_explicit widen bounds t1_actual cs1 e to1 cs2
     else (t1,csp,pure_e,e)
+
+        (* recursive coercions to components of tuples.  They may be
+        complex expressions, not top-level tuples, so we sometimes
+        need to add a pattern match. At present we do that almost
+        always, unnecessarily often.  The any_coerced is wrong *)
   | Ttup t1s, Ttup t2s ->
     let tl1,tl2 = List.length t1s,List.length t2s in
     if tl1=tl2 then 
@@ -3396,10 +3455,16 @@ let rec type_coerce_internal co d_env enforce is_explicit widen bounds t1 cs1 e
            (t2,csp@cs,efs,e')
     else eq_error l ("Found a tuple of length " ^ (string_of_int tl1) ^
                      " but expected a tuple of length " ^ (string_of_int tl2))
+
+
+        (* all the Tapp cases *)
   | Tapp(id1,args1),Tapp(id2,args2) ->
     if id1=id2 && (id1 <> "vector")
+        (* no coercion needed, so fall back to consistency *)
     then let t',cs' = type_consistent co d_env enforce widen t1 t2 in (t',cs',pure_e,e)
     else (match id1,id2,is_explicit with
+
+      (* can coerce between two vectors just to change the start index *)
     | "vector","vector",_ ->
       (match args1,args2 with
       | [TA_nexp b1;TA_nexp r1;TA_ord o1;TA_typ t1i],
@@ -3415,6 +3480,8 @@ let rec type_coerce_internal co d_env enforce is_explicit widen bounds t1 cs1 e
         let e' = E_aux(E_internal_cast ((l,(Base(([],t2),Emp_local,[],pure_e,pure_e,nob))),e),(l,tannot)) in
         (t2,cs@cs',pure_e,e')
       | _ -> raise (Reporting_basic.err_unreachable l "vector is not properly kinded"))
+
+          (* coercion from a bit vector into a number *)
     | "vector","range",_ -> 
       (match args1,args2 with
       | [TA_nexp b1;TA_nexp r1;TA_ord _;TA_typ {t=Tid "bit"}],
@@ -3429,6 +3496,8 @@ let rec type_coerce_internal co d_env enforce is_explicit widen bounds t1 cs1 e
       | [TA_nexp b1;TA_nexp r1;TA_ord o;TA_typ t],_ -> 
         eq_error l "Cannot convert non-bit vector into an range"
       | _,_ -> raise (Reporting_basic.err_unreachable l "vector or range is not properly kinded"))
+
+          (* similar to vector/range case *)
     | "vector","atom",_ -> 
       (match args1,args2 with
       | [TA_nexp b1;TA_nexp r1;TA_ord _;TA_typ {t=Tid "bit"}],
@@ -3441,6 +3510,9 @@ let rec type_coerce_internal co d_env enforce is_explicit widen bounds t1 cs1 e
       | [TA_nexp b1;TA_nexp r1;TA_ord o;TA_typ t],_ -> 
         eq_error l "Cannot convert non-bit vector into an range"
       | _,_ -> raise (Reporting_basic.err_unreachable l "vector or range is not properly kinded"))
+
+          (* coercion from number into bit vector, if there's an explicit type annotation in the source (the "true") *)
+          (* this can be lossy, if it doesn't fit into that vector, so we want to require the user to specify the vector size. It was desired by some users, but maybe should be turned back into an error and an explicit truncate function be used *)
     | "range","vector",true -> 
       (match args2,args1 with
       | [TA_nexp b1;TA_nexp r1;TA_ord {order = Oinc};TA_typ {t=Tid "bit"}],
@@ -3464,6 +3536,8 @@ let rec type_coerce_internal co d_env enforce is_explicit widen bounds t1 cs1 e
       | [TA_nexp b1;TA_nexp r1;TA_ord o;TA_typ t],_ -> 
         eq_error l "Cannot convert a range into a non-bit vector"
       | _,_ -> raise (Reporting_basic.err_unreachable l "vector or range is not properly kinded"))
+
+          (* similar to number to bit vector case *)
     | "atom","vector",true -> 
       (match args2,args1 with
       | [TA_nexp b1;TA_nexp r1;TA_ord {order = Oinc};TA_typ {t=Tid "bit"}],
@@ -3486,6 +3560,8 @@ let rec type_coerce_internal co d_env enforce is_explicit widen bounds t1 cs1 e
       | [TA_nexp b1;TA_nexp r1;TA_ord o;TA_typ t],_ -> 
         eq_error l "Cannot convert a range into a non-bit vector"
       | _,_ -> raise (Reporting_basic.err_unreachable l "vector or range is not properly kinded"))
+
+          (* implicit dereference of a register, from register<t> to t, and then perhaps also from t to the expected type *)
     | "register",_,_ ->
       (match args1 with
         | [TA_typ t] ->
@@ -3501,16 +3577,24 @@ let rec type_coerce_internal co d_env enforce is_explicit widen bounds t1 cs1 e
           let (t',cs,ef',e) = type_coerce co d_env Guarantee is_explicit widen bounds t new_e t2 in
           (t',cs,union_effects ef ef',e)
         | _ -> raise (Reporting_basic.err_unreachable l "register is not properly kinded"))
+
+          (* otherwise in Tapp case, fall back on type_consistent *)
     | _,_,_ -> 
       let t',cs' = type_consistent co d_env enforce widen t1 t2 in (t',cs',pure_e,e))
+
+        (* bit vector of length 1 to bit *)
   | Tapp("vector",[TA_nexp b1;TA_nexp r1;TA_ord o;TA_typ {t=Tid "bit"}]),Tid("bit") ->
     let cs = [Eq(co,r1,n_one)] in
     (t2,cs,pure_e,E_aux((E_app ((Id_aux (Id "most_significant", l)), [e])),
                         (l, cons_tag_annot_efr t2 (External (Some "most_significant"))
                            cs (get_cummulative_effects (get_eannot e)))))
+
+      (* bit to a bitvector of length 1 *)
   | Tid("bit"),Tapp("vector",[TA_nexp b1;TA_nexp r1;TA_ord o;TA_typ {t=Tid "bit"}]) ->
     let cs = [Eq(co,r1,n_one)] in
     (t2,cs,pure_e,E_aux(E_vector [e], (l, constrained_annot_efr t2 cs (get_cummulative_effects (get_eannot e)))))
+
+      (* bit to a number range (including 0..1) *)
   | Tid("bit"),Tapp("range",[TA_nexp b1;TA_nexp r1]) ->
     let t',cs'= type_consistent co d_env enforce false {t=Tapp("range",[TA_nexp n_zero;TA_nexp n_one])} t2 in
     (t2,cs',pure_e,
@@ -3521,6 +3605,9 @@ let rec type_coerce_internal co d_env enforce is_explicit widen bounds t1 cs1 e
                                       E_aux(E_lit(L_aux(L_num 1,l)),(l,simple_annot t2))),
                               (l,simple_annot t2));]),
            (l,simple_annot_efr t2 (get_cummulative_effects (get_eannot e)))))   
+
+
+      (* similar to above, bit to a singleton number range *)
   | Tid("bit"),Tapp("atom",[TA_nexp b1]) ->
     let t',cs'= type_consistent co d_env enforce false t2 {t=Tapp("range",[TA_nexp n_zero;TA_nexp n_one])} in
     (t2,cs',pure_e,
@@ -3531,6 +3618,9 @@ let rec type_coerce_internal co d_env enforce is_explicit widen bounds t1 cs1 e
                                       E_aux(E_lit(L_aux(L_num 1,l)),(l,simple_annot t2))),
                               (l,simple_annot t2));]),
            (l,simple_annot_efr t2 (get_cummulative_effects (get_eannot e)))))
+
+
+      (* number range to a bit *)
   | Tapp("range",[TA_nexp b1;TA_nexp r1;]),Tid("bit") ->
     let t',cs'= type_consistent co d_env enforce false t1 {t=Tapp("range",[TA_nexp n_zero;TA_nexp n_one])} in
     let efr = get_cummulative_effects (get_eannot e)
@@ -3539,6 +3629,8 @@ let rec type_coerce_internal co d_env enforce is_explicit widen bounds t1 cs1 e
                                  E_aux(E_lit(L_aux(L_one,l)),(l,simple_annot bit_t)),
                                  E_aux(E_lit(L_aux(L_zero,l)),(l,simple_annot bit_t))),
                             (l,simple_annot_efr bit_t efr)))
+
+      (* similar to above *)
   | Tapp("atom",[TA_nexp b1]),Tid("bit") ->
     let t',cs'= type_consistent co d_env enforce false t1 {t=Tapp("range",[TA_nexp n_zero;TA_nexp n_one])} in
     let efr = get_cummulative_effects (get_eannot e)
@@ -3546,6 +3638,8 @@ let rec type_coerce_internal co d_env enforce is_explicit widen bounds t1 cs1 e
                                  E_aux(E_lit(L_aux(L_one,l)),(l,simple_annot bit_t)),
                                  E_aux(E_lit(L_aux(L_zero,l)),(l,simple_annot bit_t))),
                             (l,simple_annot_efr bit_t efr)))
+
+      (* number range to an enumeration type *)
   | Tapp("range",[TA_nexp b1;TA_nexp r1;]),Tid(i) -> 
     (match Envmap.apply d_env.enum_env i with
     | Some(enums) -> 
@@ -3558,6 +3652,23 @@ let rec type_coerce_internal co d_env enforce is_explicit widen bounds t1 cs1 e
                                                   (l,simple_annot t2))) enums),
              (l,simple_annot_efr t2 (get_cummulative_effects (get_eannot e)))))
     | None -> eq_error l ("Type mismatch: found a " ^ (t_to_string t1) ^ " but expected " ^ (t_to_string t2)))
+
+        (* similar to above *)
+  | Tapp("atom",[TA_nexp b1]),Tid(i) -> 
+    (match Envmap.apply d_env.enum_env i with
+      | Some(enums) -> 
+        let num_enums = List.length enums in
+        (t2,[GtEq(co,Require,b1,n_zero);
+             LtEq(co,Require,b1,mk_c(big_int_of_int num_enums))],pure_e,
+         E_aux(E_case(e,
+                      List.mapi (fun i a -> Pat_aux(Pat_exp(P_aux(P_lit(L_aux((L_num i),l)),(l, simple_annot t1)),
+                                                            E_aux(E_id(Id_aux(Id a,l)),
+                                                                  (l, tag_annot t2 (Enum num_enums)))),
+                                                    (l,simple_annot t2))) enums),
+               (l,simple_annot_efr t2 (get_cummulative_effects (get_eannot e)))))
+      | None -> eq_error l ("Type mismatch: found a " ^ (t_to_string t1) ^ " but expected " ^ (t_to_string t2)))
+
+        (* bit vector to an enumeration type *)
   | Tapp("vector", [TA_nexp _; TA_nexp size; _; TA_typ {t= Tid "bit"}]), Tid(i) ->
     (match Envmap.apply d_env.enum_env i with
      | Some(enums) ->
@@ -3573,19 +3684,8 @@ let rec type_coerce_internal co d_env enforce is_explicit widen bounds t1 cs1 e
                                                     (l,simple_annot t2))) enums),
               (l,simple_annot_efr t2 (get_cummulative_effects (get_eannot e)))))
      | None -> eq_error l ("Type mismatch: found a " ^ (t_to_string t1) ^ " but expected " ^ (t_to_string t2)))
-  | Tapp("atom",[TA_nexp b1]),Tid(i) -> 
-    (match Envmap.apply d_env.enum_env i with
-      | Some(enums) -> 
-        let num_enums = List.length enums in
-        (t2,[GtEq(co,Require,b1,n_zero);
-             LtEq(co,Require,b1,mk_c(big_int_of_int num_enums))],pure_e,
-         E_aux(E_case(e,
-                      List.mapi (fun i a -> Pat_aux(Pat_exp(P_aux(P_lit(L_aux((L_num i),l)),(l, simple_annot t1)),
-                                                            E_aux(E_id(Id_aux(Id a,l)),
-                                                                  (l, tag_annot t2 (Enum num_enums)))),
-                                                    (l,simple_annot t2))) enums),
-               (l,simple_annot_efr t2 (get_cummulative_effects (get_eannot e)))))
-      | None -> eq_error l ("Type mismatch: found a " ^ (t_to_string t1) ^ " but expected " ^ (t_to_string t2)))
+
+        (* enumeration type to number range *)
   | Tid(i),Tapp("range",[TA_nexp b1;TA_nexp r1;]) -> 
     (match Envmap.apply d_env.enum_env i with
     | Some(enums) -> 
@@ -3596,6 +3696,11 @@ let rec type_coerce_internal co d_env enforce is_explicit widen bounds t1 cs1 e
                                                   (l,simple_annot t2))) enums),
              (l,simple_annot_efr t2 (get_cummulative_effects (get_eannot e)))))
     | None -> eq_error l ("Type mismatch: " ^ (t_to_string t1) ^ " , " ^ (t_to_string t2)))
+
+
+        (* probably there's a missing enumeration type to singleton number range *)
+
+        (* fall through to type_consistent *)
   | _,_ -> let t',cs = type_consistent co d_env enforce widen t1 t2 in (t',cs,pure_e,e)
 
 and type_coerce co d_env enforce is_explicit widen bounds t1 e t2 = 
diff --git a/src/type_internal.mli b/src/type_internal.mli
index b55418fe..091f1e64 100644
--- a/src/type_internal.mli
+++ b/src/type_internal.mli
@@ -1,3 +1,45 @@
+(**************************************************************************)
+(*     Sail                                                               *)
+(*                                                                        *)
+(*  Copyright (c) 2013-2017                                               *)
+(*    Kathyrn Gray                                                        *)
+(*    Shaked Flur                                                         *)
+(*    Stephen Kell                                                        *)
+(*    Gabriel Kerneis                                                     *)
+(*    Robert Norton-Wright                                                *)
+(*    Christopher Pulte                                                   *)
+(*    Peter Sewell                                                        *)
+(*                                                                        *)
+(*  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 Big_int
 
 module Envmap : Finite_map.Fmap with type k = string
@@ -337,3 +379,6 @@ val type_coerce : constraint_origin -> def_envs -> range_enforcement -> bool ->
    When merging atoms, use bool to control widening. 
 *)
 val tannot_merge : constraint_origin -> def_envs -> bool -> tannot -> tannot -> tannot 
+
+val initial_typ_env : tannot Envmap.t
+
diff --git a/src/util.ml b/src/util.ml
index a2bd7cc0..2b6f81f8 100644
--- a/src/util.ml
+++ b/src/util.ml
@@ -1,4 +1,46 @@
 (**************************************************************************)
+(*     Sail                                                               *)
+(*                                                                        *)
+(*  Copyright (c) 2013-2017                                               *)
+(*    Kathyrn Gray                                                        *)
+(*    Shaked Flur                                                         *)
+(*    Stephen Kell                                                        *)
+(*    Gabriel Kerneis                                                     *)
+(*    Robert Norton-Wright                                                *)
+(*    Christopher Pulte                                                   *)
+(*    Peter Sewell                                                        *)
+(*                                                                        *)
+(*  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.                                                          *)
+(**************************************************************************)
+
+(**************************************************************************)
 (*                        Lem                                             *)
 (*                                                                        *)
 (*          Dominic Mulligan, University of Cambridge                     *)
@@ -44,6 +86,7 @@
 (*  IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.                         *)
 (**************************************************************************)
 
+
 module Duplicate(S : Set.S) = struct
 
 type dups = 
diff --git a/src/util.mli b/src/util.mli
index 45e20381..c565cdce 100644
--- a/src/util.mli
+++ b/src/util.mli
@@ -1,47 +1,43 @@
 (**************************************************************************)
-(*                        Lem                                             *)
+(*     Sail                                                               *)
 (*                                                                        *)
-(*          Dominic Mulligan, University of Cambridge                     *)
-(*          Francesco Zappa Nardelli, INRIA Paris-Rocquencourt            *)
-(*          Gabriel Kerneis, University of Cambridge                      *)
-(*          Kathy Gray, University of Cambridge                           *)
-(*          Peter Boehm, University of Cambridge (while working on Lem)   *)
-(*          Peter Sewell, University of Cambridge                         *)
-(*          Scott Owens, University of Kent                               *)
-(*          Thomas Tuerk, University of Cambridge                         *)
+(*  Copyright (c) 2013-2017                                               *)
+(*    Kathyrn Gray                                                        *)
+(*    Shaked Flur                                                         *)
+(*    Stephen Kell                                                        *)
+(*    Gabriel Kerneis                                                     *)
+(*    Robert Norton-Wright                                                *)
+(*    Christopher Pulte                                                   *)
+(*    Peter Sewell                                                        *)
 (*                                                                        *)
-(*  The Lem sources are copyright 2010-2013                               *)
-(*  by the UK authors above and Institut National de Recherche en         *)
-(*  Informatique et en Automatique (INRIA).                               *)
-(*                                                                        *)
-(*  All files except ocaml-lib/pmap.{ml,mli} and ocaml-libpset.{ml,mli}   *)
-(*  are distributed under the license below.  The former are distributed  *)
-(*  under the LGPLv2, as in the LICENSE file.                             *)
+(*  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.         *)
+(*     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.  *)
-(*  3. The names of the authors may not be used to endorse or promote     *)
-(*  products derived from this software without specific prior written    *)
-(*  permission.                                                           *)
+(*     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 AUTHORS ``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 AUTHORS 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.                         *)
+(*  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.                                                          *)
 (**************************************************************************)
 
 (** Mixed useful things *)