Merge new pretty-printer

12 files changed, 281 insertions, 184 deletions

diff --git a/language/l2.lem b/language/l2.lem
index 969a5bbf..4921c16b 100644
--- a/language/l2.lem
+++ b/language/l2.lem
@@ -75,6 +75,11 @@ type base_effect =
  | BE_aux of base_effect_aux * l
 
 
+type id_aux =  (* Identifier *)
+ | Id of x
+ | DeIid of x (* remove infix status *)
+
+
 type effect_aux =  (* effect set, of kind Effects *)
  | Effect_var of kid
  | Effect_set of list base_effect (* effect set *)
@@ -86,9 +91,8 @@ type order_aux =  (* vector order specifications, of kind Order *)
  | Ord_dec (* decreasing (big-endian) *)
 
 
-type id_aux =  (* Identifier *)
- | Id of x
- | DeIid of x (* remove infix status *)
+type id = 
+ | Id_aux of id_aux * l
 
 
 type effect = 
@@ -98,10 +102,6 @@ type effect =
 type order = 
  | Ord_aux of order_aux * l
 
-
-type id = 
- | Id_aux of id_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
@@ -142,19 +142,6 @@ type typquant_aux =  (* type quantifiers and constraints *)
  | 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 typ_aux =  (* Type expressions, of kind $Type$ *)
  | Typ_wild (* Unspecified type *)
  | Typ_id of id (* Defined type *)
@@ -180,14 +167,31 @@ type typquant =
  | TypQ_aux of typquant_aux * l
 
 
-type lit = 
- | L_aux of lit_aux * l
+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 typschm_aux =  (* type scheme *)
  | TypSchm_ts of typquant * typ
 
 
+type lit = 
+ | L_aux of lit_aux * l
+
+
+type typschm = 
+ | TypSchm_aux of typschm_aux * l
+
+
 type pat_aux 'a =  (* Pattern *)
  | P_lit of lit (* literal constant pattern *)
  | P_wild (* wildcard *)
@@ -212,10 +216,6 @@ and fpat 'a =
  | FP_aux of (fpat_aux 'a) * annot 'a
 
 
-type typschm = 
- | TypSchm_aux of typschm_aux * l
-
-
 type exp_aux 'a =  (* Expression *)
  | E_block of list (exp 'a) (* block (parsing conflict with structs?) *)
  | E_id of id (* identifier *)
@@ -227,7 +227,7 @@ type exp_aux 'a =  (* Expression *)
  | 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)) (* vector (indexed consecutively) *)
+ | 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 *)
@@ -269,6 +269,13 @@ and fexps_aux 'a =  (* Field-expression list *)
 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)
 
@@ -283,23 +290,14 @@ and letbind 'a =
  | LB_aux of (letbind_aux 'a) * annot 'a
 
 
-type effect_opt_aux =  (* Optional effect annotation for functions *)
- | Effect_opt_pure (* sugar for empty effect set *)
- | Effect_opt_effect of effect
-
-
 type rec_opt_aux =  (* Optional recursive annotation for functions *)
  | Rec_nonrec (* non-recursive *)
  | Rec_rec (* recursive *)
 
 
-type funcl_aux 'a =  (* Function clause *)
- | FCL_Funcl of id * (pat 'a) * (exp 'a)
-
-
-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 type_union_aux =  (* Type union constructors *)
@@ -307,34 +305,43 @@ type type_union_aux =  (* Type union constructors *)
  | Tu_ty_id of typ * id
 
 
+type funcl_aux 'a =  (* Function clause *)
+ | FCL_Funcl of id * (pat 'a) * (exp 'a)
+
+
 type tannot_opt_aux =  (* Optional type annotation for functions *)
  | Typ_annot_opt_some of typquant * typ
 
 
-type effect_opt = 
- | Effect_opt_aux of effect_opt_aux * l
+type name_scm_opt_aux =  (* Optional variable-naming-scheme specification for variables of defined type *)
+ | Name_sect_none
+ | Name_sect_some of string
 
 
 type rec_opt = 
  | Rec_aux of rec_opt_aux * l
 
 
-type funcl 'a = 
- | FCL_aux of (funcl_aux 'a) * 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 type_union = 
  | Tu_aux of type_union_aux * l
 
 
+type funcl 'a = 
+ | FCL_aux of (funcl_aux 'a) * l
+
+
 type tannot_opt = 
  | Typ_annot_opt_aux of tannot_opt_aux * l
 
 
+type name_scm_opt = 
+ | Name_sect_aux of name_scm_opt_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 *)
@@ -344,6 +351,10 @@ and index_range =
  | BF_aux of index_range_aux * l
 
 
+type dec_spec_aux 'a =  (* Register declarations *)
+ | DEC_reg of typ * id
+
+
 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 *)
@@ -353,18 +364,6 @@ type scattered_def_aux 'a =  (* Function and type union definitions that can be
  | SD_scattered_end of id (* scattered definition end *)
 
 
-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 dec_spec_aux 'a =  (* Register declarations *)
- | DEC_reg of typ * id
-
-
 type fundef_aux 'a =  (* Function definition *)
  | FD_function of rec_opt * tannot_opt * effect_opt * list (funcl 'a)
 
@@ -374,24 +373,28 @@ type default_spec_aux 'a =  (* Default kinding or typing assumption *)
  | 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 scattered_def 'a = 
- | SD_aux of (scattered_def_aux 'a) * annot 'a
-
-
-type type_def 'a = 
- | TD_aux of (type_def_aux 'a) * annot 'a
-
-
 type dec_spec 'a = 
  | DEC_aux of (dec_spec_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
 
@@ -400,6 +403,10 @@ 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
 
@@ -440,6 +447,15 @@ let rec disjoint_all sets =
 end
 
 
+type ne =  (* internal numeric expressions *)
+ | Ne_var of x
+ | Ne_const of integer
+ | Ne_mult of ne * ne
+ | Ne_add of list ne
+ | Ne_exp of ne
+ | Ne_unary of ne
+
+
 type k =  (* Internal kinds *)
  | Ki_typ
  | Ki_nat
@@ -449,13 +465,11 @@ type k =  (* Internal kinds *)
  | Ki_infer (* Representing an unknown kind, inferred by context *)
 
 
-type ne =  (* internal numeric expressions *)
- | Ne_var of x
- | Ne_const of integer
- | Ne_mult of ne * ne
- | Ne_add of list ne
- | Ne_exp of ne
- | Ne_unary of ne
+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
 
 
 type kinf =  (* Whether a kind is default or from a local binding *)
@@ -468,13 +482,6 @@ type tid =  (* A type identifier or type variable *)
  | Tid_var of kid
 
 
-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
-
-
 type t =  (* Internal types *)
  | T_id of x
  | T_var of x
@@ -551,10 +558,10 @@ let fresh_kid denv = Var "x" (*TODO When strings can be manipulated, this should
 
 
 
-type I = inf
+type E = env
 
 
-type E = env
+type I = inf
 
 
 
diff --git a/language/l2.ml b/language/l2.ml
index 6501ff28..3ce5cac3 100644
--- a/language/l2.ml
+++ b/language/l2.ml
@@ -74,9 +74,9 @@ base_effect =
 
 
 type 
-effect_aux =  (* effect set, of kind Effects *)
-   Effect_var of kid
- | Effect_set of (base_effect) list (* effect set *)
+id_aux =  (* Identifier *)
+   Id of x
+ | DeIid of x (* remove infix status *)
 
 
 type 
@@ -87,14 +87,14 @@ order_aux =  (* vector order specifications, of kind Order *)
 
 
 type 
-id_aux =  (* Identifier *)
-   Id of x
- | DeIid of x (* remove infix status *)
+effect_aux =  (* effect set, of kind Effects *)
+   Effect_var of kid
+ | Effect_set of (base_effect) list (* effect set *)
 
 
 type 
-effect = 
-   Effect_aux of effect_aux * l
+id = 
+   Id_aux of id_aux * l
 
 
 type 
@@ -103,8 +103,8 @@ order =
 
 
 type 
-id = 
-   Id_aux of id_aux * l
+effect = 
+   Effect_aux of effect_aux * l
 
 
 type 
@@ -163,11 +163,6 @@ lit_aux =  (* Literal 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 *)
@@ -190,6 +185,11 @@ and typ_arg =
 
 
 type 
+typquant = 
+   TypQ_aux of typquant_aux * l
+
+
+type 
 lit = 
    L_aux of lit_aux * l
 
@@ -200,10 +200,7 @@ typschm_aux =  (* type scheme *)
 
 
 type 
-'a fpat = 
-   FP_aux of 'a fpat_aux * 'a annot
-
-and 'a pat_aux =  (* Pattern *)
+'a pat_aux =  (* Pattern *)
    P_lit of lit (* literal constant pattern *)
  | P_wild (* wildcard *)
  | P_as of 'a pat * id (* named pattern *)
@@ -223,6 +220,9 @@ and 'a pat =
 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 = 
@@ -241,7 +241,7 @@ type
  | 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 (* vector (indexed consecutively) *)
+ | 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 *)
@@ -283,6 +283,13 @@ and 'a fexps_aux =  (* Field-expression list *)
 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
 
diff --git a/language/l2.ott b/language/l2.ott
index 7b619652..a880527c 100644
--- a/language/l2.ott
+++ b/language/l2.ott
@@ -482,7 +482,7 @@ pat :: 'P_' ::=
   | [ pat1 , .. , patn  ]                     :: :: vector
    {{ com vector pattern }}
 
-  | [ num1 = pat1 , .. , numn = patn  ]                     :: :: vector_indexed
+  | [ num1 = pat1 , .. , numn = patn ]                     :: :: vector_indexed
    {{ com vector pattern (with explicit indices) }}
 
 % cf ntoes for this
@@ -561,7 +561,7 @@ exp :: 'E_' ::=
 % here the expi are of type 'a and the result is a vector of 'a, whereas in exp1 : ... : expn 
 % the expi and the result are both of type vector of 'a 
 
-  | [ num1 = exp1 , ... , numn = expn ]               :: :: vector_indexed {{ com vector (indexed consecutively) }}
+  | [ num1 = exp1 , ... , numn = expn , opt_default ]               :: :: vector_indexed {{ com vector (indexed consecutively) }}
 % num1 .. numn must be a consecutive list of naturals
 
 % we pick [ ] not { } for vector literals for consistency with their
@@ -655,6 +655,12 @@ fexps :: 'FES_' ::=
   {{ aux _ annot }} {{ auxparam 'a }}
   | fexp1 ; ... ; fexpn semi_opt                        :: :: Fexps
 
+opt_default :: 'Def_val_' ::=
+  {{ com Optional default value for indexed vectors, to define a defualt value for any unspecified positions in a sparse map }}
+  {{ aux _ annot }} {{ auxparam 'a }}
+  |                                                     :: :: empty
+  | default = exp                                       :: :: dec
+
 pexp :: 'Pat_' ::=
   {{ com Pattern match }}
   {{ aux _ annot }} {{ auxparam 'a }}
diff --git a/language/l2_parse.ml b/language/l2_parse.ml
index 7be33bc4..a283b605 100644
--- a/language/l2_parse.ml
+++ b/language/l2_parse.ml
@@ -208,7 +208,7 @@ exp_aux =  (* Expression *)
  | 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 ((int * exp)) list (* vector (indexed consecutively) *)
+ | E_vector_indexed of ((int * 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 *)
@@ -237,6 +237,13 @@ and fexps_aux =  (* Field-expression list *)
 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
 
@@ -264,26 +271,26 @@ type_union_aux =  (* Type union constructors *)
 
 
 type 
-tannot_opt_aux =  (* Optional type annotation for functions *)
-   Typ_annot_opt_none
- | Typ_annot_opt_some of typquant * atyp
+rec_opt_aux =  (* Optional recursive annotation for functions *)
+   Rec_nonrec (* non-recursive *)
+ | Rec_rec (* recursive *)
 
 
 type 
-effect_opt_aux =  (* Optional effect annotation for functions *)
-   Effect_opt_pure (* sugar for empty effect set *)
- | Effect_opt_effect of atyp
+funcl_aux =  (* Function clause *)
+   FCL_Funcl of id * pat * exp
 
 
 type 
-rec_opt_aux =  (* Optional recursive annotation for functions *)
-   Rec_nonrec (* non-recursive *)
- | Rec_rec (* recursive *)
+tannot_opt_aux =  (* Optional type annotation for functions *)
+   Typ_annot_opt_none
+ | Typ_annot_opt_some of typquant * atyp
 
 
 type 
-funcl_aux =  (* Function clause *)
-   FCL_Funcl of id * pat * exp
+effect_opt_aux =  (* Optional effect annotation for functions *)
+   Effect_opt_pure (* sugar for empty effect set *)
+ | Effect_opt_effect of atyp
 
 
 type 
@@ -307,16 +314,6 @@ type_union =
 
 
 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
 
@@ -327,10 +324,13 @@ funcl =
 
 
 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
+tannot_opt = 
+   Typ_annot_opt_aux of tannot_opt_aux * l
+
+
+type 
+effect_opt = 
+   Effect_opt_aux of effect_opt_aux * l
 
 
 type 
@@ -343,19 +343,13 @@ type_def_aux =  (* Type definition body *)
 
 
 type 
-dec_spec_aux =  (* Register declarations *)
-   DEC_reg of atyp * id
-
-
-type 
-default_typing_spec_aux =  (* Default kinding or typing assumption *)
-   DT_kind of base_kind * kid
- | DT_typ of typschm * id
+fundef_aux =  (* Function definition *)
+   FD_function of rec_opt * tannot_opt * effect_opt * (funcl) list
 
 
 type 
-fundef_aux =  (* Function definition *)
-   FD_function of rec_opt * tannot_opt * effect_opt * (funcl) list
+dec_spec_aux =  (* Register declarations *)
+   DEC_reg of atyp * id
 
 
 type 
@@ -369,8 +363,16 @@ scattered_def_aux =  (* Function and type union definitions that can be spread a
 
 
 type 
-val_spec = 
-   VS_aux of val_spec_aux * l
+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 
+default_typing_spec_aux =  (* Default kinding or typing assumption *)
+   DT_kind of base_kind * kid
+ | DT_typ of typschm * id
 
 
 type 
@@ -379,23 +381,28 @@ type_def =
 
 
 type 
+fundef = 
+   FD_aux of fundef_aux * l
+
+
+type 
 dec_spec = 
    DEC_aux of dec_spec_aux * l
 
 
 type 
-default_typing_spec = 
-   DT_aux of default_typing_spec_aux * l
+scattered_def = 
+   SD_aux of scattered_def_aux * l
 
 
 type 
-fundef = 
-   FD_aux of fundef_aux * l
+val_spec = 
+   VS_aux of val_spec_aux * l
 
 
 type 
-scattered_def = 
-   SD_aux of scattered_def_aux * l
+default_typing_spec = 
+   DT_aux of default_typing_spec_aux * l
 
 
 type 
diff --git a/language/l2_parse.ott b/language/l2_parse.ott
index 1f365a3f..11b51f2a 100644
--- a/language/l2_parse.ott
+++ b/language/l2_parse.ott
@@ -452,7 +452,7 @@ exp :: 'E_' ::=
 % here the expi are of type 'a and the result is a vector of 'a, whereas in exp1 : ... : expn 
 % the expi and the result are both of type vector of 'a 
 
-  | [ num1 = exp1 , ... , numn = expn ]               :: :: vector_indexed {{ com vector (indexed consecutively) }}
+  | [ num1 = exp1 , ... , numn = expn , opt_default ]               :: :: vector_indexed {{ com vector (indexed consecutively) }}
 % num1 .. numn must be a consecutive list of naturals
 
 % we pick [ ] not { } for vector literals for consistency with their
@@ -544,6 +544,12 @@ fexps :: 'FES_' ::=
 %  {{ aux _ annot }} {{ auxparam 'a }}
   | fexp1 ; ... ; fexpn semi_opt                        :: :: Fexps
 
+opt_default :: 'Def_val_' ::=
+  {{ com Optional default value for indexed vectors, to define a defualt value for any unspecified positions in a sparse map }}
+  {{ aux _ l }} 
+  |                                                     :: :: empty
+  | default = exp                                       :: :: dec
+
 pexp :: 'Pat_' ::=
   {{ com Pattern match }}
   {{ aux _ l }}
diff --git a/src/initial_check.ml b/src/initial_check.ml
index 2548bf19..95578d9f 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -354,7 +354,7 @@ and to_ast_exp (k_env : kind Envmap.t) (Parse_ast.E_aux(exp,l) : Parse_ast.exp)
     | Parse_ast.E_for(id,e1,e2,e3,atyp,e4) -> 
       E_for(to_ast_id id,to_ast_exp k_env e1, to_ast_exp k_env e2, to_ast_exp k_env e3,to_ast_order k_env atyp, to_ast_exp k_env e4)
     | Parse_ast.E_vector(exps) -> E_vector(List.map (to_ast_exp k_env) exps)
-    | Parse_ast.E_vector_indexed(iexps) -> E_vector_indexed(List.map (fun (i,e) -> (i,to_ast_exp k_env e)) iexps)
+    | Parse_ast.E_vector_indexed(iexps,default) -> E_vector_indexed(List.map (fun (i,e) -> (i,to_ast_exp k_env e)) iexps, Def_val_aux(Def_val_empty,(l,NoTyp))) (*TODO transform the default *)
     | Parse_ast.E_vector_access(vexp,exp) -> E_vector_access(to_ast_exp k_env vexp, to_ast_exp k_env exp)
     | Parse_ast.E_vector_subrange(vex,exp1,exp2) -> E_vector_subrange(to_ast_exp k_env vex, to_ast_exp k_env exp1, to_ast_exp k_env exp2)
     | Parse_ast.E_vector_update(vex,exp1,exp2) -> E_vector_update(to_ast_exp k_env vex, to_ast_exp k_env exp1, to_ast_exp k_env exp2)
diff --git a/src/lem_interp/Interp_interface.lem b/src/lem_interp/Interp_interface.lem
index 0767ea79..0e05fafe 100644
--- a/src/lem_interp/Interp_interface.lem
+++ b/src/lem_interp/Interp_interface.lem
@@ -4,49 +4,49 @@ type read_kind = Interp.read_kind
 type write_kind = Interp.write_kind
 type barrier_kind = Interp.barrier_kind
 
+type word8 = nat (* bounded at a byte, for when lem supports it*)
+
 type value = 
-| Bitvector of list nat (*Always 0 or 1; should this be a Word.bitSequence? *)
-| Bytevector of list (list nat) (* Should this be a list of Word.bitSequence? *)
+| Bitvector of list bool (* For register accesses *)
+| Bytevector of list word8 (* For memory accesses *)
 | Unknown
 
 type instruction_state = Interp.stack
 type context = Interp.top_level
 
-type reg_name = Interp.reg_form (*for now...*)
+type slice = (integer * integer)
+
+type reg_name = 
+| Reg of string (*Name of the register, accessing the entire register*)
+| Reg_slice of string * slice (*Name of the register, accessing from the first to second integer of the slice*)
+| Reg_field of string * string * slice (*Name of the register, name of the field of the register accessed, the slice of the field*)
+| Reg_f_slice of string * string * slice * slice (* Same as above but only accessing second slice of the field *)
 
 type outcome =
 | Read_mem of read_kind * value * (value -> instruction_state)
 | Write_mem of write_kind * value * value * (bool -> instruction_state)
 | Barrier of barrier_kind * instruction_state
-| Read_reg of reg_name * (value -> instruction_state) (*What about slicing?*)
+| Read_reg of reg_name * (value -> instruction_state) 
 | Write_reg of reg_name * value * instruction_state
 | Nondet_choice of list instruction_state
 | Internal of instruction_state
 | Done
 | Error of string
 
+type event = 
+| E_read_mem of read_kind * value
+| E_write_mem of write_kind * value
+| E_barrier of barrier_kind
+| E_read_reg of reg_name
+| E_write_reg of reg_name
+(*Should multiple memory accesses be represented with a special form to denote this or potentially merged into one read or left in place*)
+
+
 val build_context : Interp.defs Interp.tannot -> context
 val initial_instruction_state : context -> string -> value -> instruction_state
 
 type interp_mode = <| eager_eval : bool |>
-val interp : instruction_state -> interp_mode -> outcome
-
-val interp_exhaustive : instruction_state -> list outcome (*not sure what event was ment to be*)
-
-val intern_value : value -> Interp.value
-val extern_value : Interp.value -> value
-
-let build_context defs = Interp.to_top_env defs
-
-let intern_value v = match v with
-  | Bitvector bs -> Interp.V_vector 0 true (List.map (fun | 0 -> (Interp.V_lit (Interp_ast.L_aux Interp_ast.L_zero Interp_ast.Unknown)) 
-							  | _ -> (Interp.V_lit (Interp_ast.L_aux Interp_ast.L_one Interp_ast.Unknown))) bs)
-  | Unknown -> Interp.V_unknown
+val interp : interp_mode -> instruction_state -> outcome
 
-let extern_value v = match v with
-  | Interp.V_vector _ true bits -> Bitvector (List.map (fun | Interp.V_lit (Interp_ast.L_aux Interp_ast.L_zero _) -> 0
-							    | _ -> 1) bits)
-  | _ -> Unknown
+val interp_exhaustive : instruction_state -> list event
 
-let initial_instruction_state top_level main arg = 
-  Interp.Frame Nothing (E_aux (E_app (Id_aux (Id main) Interp_ast.Unknown) [ intern_value arg ]) (Interp_ast.Unknown, Nothing)) top_level [] Interp.emem
diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem
index 84bf6960..efd2f866 100644
--- a/src/lem_interp/interp.lem
+++ b/src/lem_interp/interp.lem
@@ -427,9 +427,9 @@ let rec to_exp v =
 	if (inc && n=0) 
 	then E_vector (List.map to_exp vals) 
 	else if inc then
-          E_vector_indexed (List.reverse (snd (List.foldl (fun (n,acc) e -> (n+1,(n, to_exp e)::acc)) (n,[]) vals)))
+          E_vector_indexed (List.reverse (snd (List.foldl (fun (n,acc) e -> (n+1,(n, to_exp e)::acc)) (n,[]) vals))) (Def_val_aux Def_val_empty (Interp_ast.Unknown,Nothing))
 	else 
-          E_vector_indexed (snd (List.foldr (fun e (n,acc) -> (n+1,(n, to_exp e)::acc)) (n-(list_length vals),[]) vals))
+          E_vector_indexed (snd (List.foldr (fun e (n,acc) -> (n+1,(n, to_exp e)::acc)) (n-(list_length vals),[]) vals)) (Def_val_aux Def_val_empty (Interp_ast.Unknown,Nothing))
       | V_record t ivals -> 
 	E_record(FES_aux (FES_Fexps
 			    (List.map (fun (id,value) -> (FE_aux (FE_Fexp id (to_exp value)) (Unknown,Nothing))) ivals) false) 
@@ -964,12 +964,12 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
       exp_list mode t_level (fun exps -> E_aux (E_tuple exps) (l,annot)) V_tuple l_env l_mem [] exps
     | E_vector(exps) ->
       exp_list mode t_level (fun exps -> E_aux (E_vector exps) (l,annot)) (fun vals -> V_vector 0 true vals) l_env l_mem [] exps
-    | E_vector_indexed(iexps) ->
+    | E_vector_indexed iexps default ->
       let (indexes,exps) = List.unzip iexps in
       let is_inc = match typ with
         | T_app "vector" (T_args [T_arg_nexp _;T_arg_nexp _; T_arg_order (Ord_aux Ord_inc _); _]) -> true
         | _ -> false end in
-      exp_list mode t_level (fun es -> (E_aux (E_vector_indexed (map2 (fun i e -> (i,e)) indexes es)) (l,annot))) 
+      exp_list mode t_level (fun es -> (E_aux (E_vector_indexed (map2 (fun i e -> (i,e)) indexes es) default) (l,annot))) 
                        (fun vals -> V_vector (List_extra.head indexes) is_inc vals) l_env l_mem [] exps
     | E_block(exps) -> interp_block mode t_level l_env l_env l_mem exps
     | E_app f args ->
diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem
new file mode 100644
index 00000000..59acb04a
--- /dev/null
+++ b/src/lem_interp/interp_inter_imp.lem
@@ -0,0 +1,63 @@
+import Interp
+import Interp_lib
+open import Interp_interface
+
+import Num
+
+val intern_value : value -> Interp.value
+val extern_value : Interp.value -> value
+val extern_reg : Interp.reg_form -> maybe (integer * integer) -> reg_name
+
+let build_context defs = Interp.to_top_env defs
+
+let to_bits l = (List.map (fun b -> match b with
+                               | false -> (Interp.V_lit (Interp_ast.L_aux Interp_ast.L_zero Interp_ast.Unknown)) 
+			       | true ->  (Interp.V_lit (Interp_ast.L_aux Interp_ast.L_one Interp_ast.Unknown)) end) l)
+let from_bits l = (List.map (fun b -> match b with
+                                 | Interp.V_lit (Interp_ast.L_aux Interp_ast.L_zero _) -> false
+				 | _ -> true end) l) 
+let rec to_bytes l = match l with
+  | [] -> []
+  | (a::b::c::d::e::f::g::h::rest) ->
+    (integerFromBoolList [a;b;c;d;e;f;g;h])::(to_bytes rest)
+end
+		   
+let intern_value v = match v with
+  | Bitvector bs -> Interp.V_vector 0 true  (to_bits bs)
+  | Bytevector bys -> Interp.V_vector 0 true (to_bits (List.concat (List.map (bitSeqFromInteger 8 Nothing) bys)))
+  | Unknown -> Interp.V_unknown
+end
+
+let extern_value for_mem v = match v with
+  | Interp.V_vector _ true bits ->
+    if for_mem 
+    then Bytevector (to_bytes (from_bits bits))
+    else Bitvector (from_bits bits)
+  | _ -> Unknown
+end
+
+let extern_reg r slice = match (r,slice) with
+  | (Interp.Reg(Id_aux (Id x,_)),Nothing) -> Reg x
+  | (Interp.Reg(Id_aux (Id x,_)),Just(i1,i2)) -> Reg_slice x (i1,i2)
+  | (Interp.SubReg (Id_aux (Id x,_)) (Interp.Reg(Id_aux (Id y,_))) (Interp_ast.BF_aux(Interp_ast.BF_single i) _),Nothing) -> Reg_field x y (i,i)
+end
+
+let initial_instruction_state top_level main arg = 
+  Interp.Frame Nothing (E_aux (E_app (Id_aux (Id main) Interp_ast.Unknown) [ intern_value arg ]) (Interp_ast.Unknown, Nothing)) top_level [] Interp.emem
+
+let interp mode i_state = 
+  match Interp.resume mode i_state None with
+  | Interp.Value _ -> Done
+  | Interp.Error l msg -> Error msg (*Todo, add the l information the string format*)
+  | Interp.Action a next_state ->
+    match a with
+    | Interp.Read_reg reg_form slice -> Read_reg reg_form (fun v -> Interp.add_answer_to_stack (intern_value v) next_state)
+    | Interp.Write_reg reg_form slice value -> Write_reg reg_form (extern_value value) next_state
+    | Interp.Read_mem (Id_aux (Id i) _) value slice 
+        (*Need to lookup the Mem function used to determine appropriate value, and possible appropriate read_kind *)
+      -> Read_mem Interp.Read_plain (extern_value value) (fun v -> Interp.add_answer_to_stack (intern_value v) next_state)
+    | Interp.Write_mem (Id_aux (id i) _) loc_val slice write_val ->
+      Write_mem Interp.Write_plain (extern_value loc_val) (extern_value write_val) next_state
+    | Interp.Call_extern id value -> (*Connect here to a list of external functions*) foo
+    end 
+  end
diff --git a/src/pretty_print.ml b/src/pretty_print.ml
index 75075c69..9f0382f5 100644
--- a/src/pretty_print.ml
+++ b/src/pretty_print.ml
@@ -236,7 +236,7 @@ and pp_exp ppf (E_aux(e,(_,annot))) =
     fprintf ppf "@[<0> %a %a (%a %a %a %a %a %a %a %a)@ @[<1>%a@]@]" 
       kwd "foreach " pp_id id kwd "from " pp_exp exp1 kwd " to " pp_exp exp2 kwd "by " pp_exp exp3 kwd "in" pp_ord order pp_exp exp4
   | E_vector(exps) -> fprintf ppf "@[<0>%a%a%a@]" kwd "[" (list_pp pp_comma_exp pp_exp) exps kwd "]"
-  | E_vector_indexed(iexps) -> 
+  | E_vector_indexed(iexps,default) -> 
     let iformat ppf (i,e) = fprintf ppf "@[<1>%i%a %a%a@]" i kwd " = " pp_exp e kwd "," in
     let lformat ppf (i,e) = fprintf ppf "@[<1>%i%a %a@]" i kwd " = " pp_exp e in
     fprintf ppf "@[<0> %a%a%a@]" kwd "[" (list_pp iformat lformat) iexps kwd "]"
@@ -671,7 +671,7 @@ and pp_lem_exp ppf (E_aux(e,(l,annot))) =
       fprintf ppf "@[<0>(E_aux (%a %a %a %a %a %a @ @[<1> %a @]) (%a, %a))@]" 
 	kwd "E_for" pp_lem_id id pp_lem_exp exp1 pp_lem_exp exp2 pp_lem_exp exp3 pp_lem_ord order pp_lem_exp exp4 pp_lem_l l pp_annot annot
     | E_vector(exps) -> fprintf ppf "@[<0>(E_aux (%a [%a]) (%a, %a))@]" kwd "E_vector" (list_pp pp_semi_lem_exp pp_lem_exp) exps pp_lem_l l pp_annot annot
-    | E_vector_indexed(iexps) -> 
+    | E_vector_indexed(iexps,default) -> (*TODO print out default when it is an nonempty*) 
       let iformat ppf (i,e) = fprintf ppf "@[<1>(%i %a %a) %a@]" i kwd ", " pp_lem_exp e kwd ";" in
       let lformat ppf (i,e) = fprintf ppf "@[<1>(%i %a %a) @]" i kwd ", " pp_lem_exp e in
       fprintf ppf "@[<0>(E_aux (%a [%a]) (%a, %a))@]" kwd "E_vector_indexed" (list_pp iformat lformat) iexps pp_lem_l l pp_annot annot
@@ -1127,7 +1127,8 @@ let doc_exp, doc_let =
       braces (doc_op (string "with") (exp e) (separate_map semi_sp doc_fexp fexps))
   | E_vector exps ->
       brackets (separate_map comma exp exps)
-  | E_vector_indexed iexps ->
+  | E_vector_indexed (iexps, default) ->
+      (* XXX TODO print default when it is non-empty *)
       let iexp (i,e) = doc_op equals (doc_int i) (exp e) in
       brackets (separate_map comma iexp iexps)
   | E_vector_update(v,e1,e2) ->
diff --git a/src/type_check.ml b/src/type_check.ml
index 258873ce..5499c3e2 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -622,7 +622,7 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp
       let t = {t = Tapp("vector",[TA_nexp({nexp=Nconst 0});TA_nexp({nexp=Nconst (List.length es)});TA_ord({order=Oinc});TA_typ item_t])} in
       let t',cs',e' = type_coerce (Expr l) d_env t (E_aux(E_vector es,(l,Base(([],t),Emp_local,[],pure_e)))) expect_t in
       (e',t',t_env,cs@cs',effect)
-    | E_vector_indexed eis ->
+    | E_vector_indexed(eis,default) ->
       let item_t = match expect_t.t with
         | Tapp("vector",[base;rise;ord;TA_typ item_t]) -> item_t
         | _ -> new_t () in
@@ -639,7 +639,7 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp
 				 eis) ([],[],pure_e,first)) in
       let t = {t = Tapp("vector",[TA_nexp({nexp=Nconst first});TA_nexp({nexp=Nconst (List.length eis)});
 				  TA_ord({order= if is_increasing then Oinc else Odec});TA_typ item_t])} in
-      let t',cs',e' = type_coerce (Expr l) d_env t (E_aux(E_vector_indexed es,(l,Base(([],t),Emp_local,[],pure_e)))) expect_t in
+      let t',cs',e' = type_coerce (Expr l) d_env t (E_aux(E_vector_indexed(es,default),(l,Base(([],t),Emp_local,[],pure_e)))) expect_t in
       (e',t',t_env,cs@cs',effect)
     | E_vector_access(vec,i) ->
       let base,rise,ord = new_n(),new_n(),new_o() in
diff --git a/src/type_internal.ml b/src/type_internal.ml
index 26a03d6a..abee5a9c 100644
--- a/src/type_internal.ml
+++ b/src/type_internal.ml
@@ -1017,7 +1017,7 @@ let rec type_coerce_internal co d_env t1 cs1 e t2 cs2 =
   | Tid("bit"),Tapp("vector",[TA_nexp {nexp=Nconst i};TA_nexp r1;TA_ord o;TA_typ {t=Tid "bit"}]) ->
     let cs = [Eq(co,r1,{nexp = Nconst 1})] in
     let t2' = {t = Tapp("vector",[TA_nexp {nexp=Nconst i};TA_nexp {nexp=Nconst 1};TA_ord o;TA_typ {t=Tid "bit"}])} in
-    (t2',cs,E_aux(E_vector_indexed [(i,e)],(l,Base(([],t2),Emp_local,cs,pure_e))))
+    (t2',cs,E_aux(E_vector_indexed([(i,e)],Def_val_aux(Def_val_empty,(l,NoTyp))) ,(l,Base(([],t2),Emp_local,cs,pure_e))))
   | Tapp("vector",[TA_nexp ({nexp=Nconst i} as b1);TA_nexp r1;TA_ord o;TA_typ {t=Tid "bit"}]),Tid("bit") ->
     let cs = [Eq(co,r1,{nexp = Nconst 1})] in
     (t2,cs,E_aux((E_vector_access (e,(E_aux(E_lit(L_aux(L_num i,l)),