move value type definitions to ott, and introduce new E_internal_value ast node for passing around encapsulated evaluated values; change Interp.to_exp to now just wrap values in this node

3 files changed, 1051 insertions, 421 deletions

diff --git a/language/l2.lem b/language/l2.lem
index f9d0a087..2d99e304 100644
--- a/language/l2.lem
+++ b/language/l2.lem
@@ -1,6 +1,8 @@
-(* generated by Ott 0.25 from: l2_typ.ott l2.ott *)
+(* generated by Ott 0.25 from: l2.ott *)
 open import Pervasives
 
+open import Pervasives
+open import Pervasives_extra
 open import Map
 open import Maybe
 open import Set_extra
@@ -30,10 +32,6 @@ type base_kind_aux =  (* base kind *)
  | BK_effect (* kind of effect sets *)
 
 
-type base_kind = 
- | BK_aux of base_kind_aux * l
-
-
 type kid_aux =  (* kinded IDs: $Type$, $Nat$, $Order$, and $Effect$ variables *)
  | Var of x
 
@@ -43,8 +41,8 @@ type id_aux =  (* identifier *)
  | DeIid of x (* remove infix status *)
 
 
-type kind_aux =  (* kinds *)
- | K_kind of list base_kind
+type base_kind = 
+ | BK_aux of base_kind_aux * l
 
 
 type kid = 
@@ -55,8 +53,8 @@ type id =
  | Id_aux of id_aux * l
 
 
-type kind = 
- | K_aux of kind_aux * l
+type kind_aux =  (* kinds *)
+ | K_kind of list base_kind
 
 
 type nexp_aux =  (* numeric expression, of kind $Nat$ *)
@@ -73,13 +71,20 @@ and nexp =
  | Nexp_aux of nexp_aux * l
 
 
+type kind = 
+ | K_aux of kind_aux * l
+
+
 type base_effect_aux =  (* effect *)
  | BE_rreg (* read register *)
  | BE_wreg (* write register *)
  | BE_rmem (* read memory *)
+ | BE_rmemt (* read memory and tag *)
  | BE_wmem (* write memory *)
  | BE_eamem (* signal effective address for writing memory *)
+ | BE_exmem (* determine if a store-exclusive (ARM) is going to succeed *)
  | BE_wmv (* write memory, sending only value *)
+ | BE_wmvt (* write memory, sending only value and tag *)
  | BE_barr (* memory barrier *)
  | BE_depend (* dynamic footprint *)
  | BE_undef (* undefined-instruction exception *)
@@ -118,11 +123,6 @@ let effect_union e1 e2 =
   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
@@ -130,14 +130,19 @@ type n_constraint_aux =  (* constraint over kind $Nat$ *)
  | NC_nat_set_bounded of kid * list integer
 
 
-type kinded_id = 
- | KOpt_aux of kinded_id_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 = 
  | NC_aux of n_constraint_aux * l
 
 
+type kinded_id = 
+ | KOpt_aux of kinded_id_aux * l
+
+
 type quant_item_aux =  (* kinded identifier or $Nat$ constraint *)
  | QI_id of kinded_id (* optionally kinded identifier *)
  | QI_const of n_constraint (* $Nat$ constraint *)
@@ -152,19 +157,6 @@ type typquant_aux =  (* type quantifiers and constraints *)
  | TypQ_no_forall (* empty *)
 
 
-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_string of string (* string constant *)
- | L_undef (* undefined-value constant *)
-
-
 type typquant = 
  | TypQ_aux of typquant_aux * l
 
@@ -190,14 +182,40 @@ and typ_arg =
  | Typ_arg_aux of typ_arg_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_string of string (* string constant *)
+ | L_undef (* undefined-value constant *)
+
+
+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 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 *)
@@ -222,14 +240,252 @@ and fpat 'a =
  | FP_aux of (fpat_aux 'a) * annot 'a
 
 
-type typschm = 
- | TypSchm_aux of typschm_aux * l
+type name_scm_opt_aux =  (* optional variable naming-scheme constraint *)
+ | Name_sect_none
+ | Name_sect_some of string
+
+
+type type_union_aux =  (* type union constructors *)
+ | Tu_id of id
+ | Tu_ty_id of typ * id
+
+
+type name_scm_opt = 
+ | Name_sect_aux of name_scm_opt_aux * l
+
+
+type type_union = 
+ | Tu_aux of type_union_aux * l
+
+
+type kind_def_aux 'a =  (* Definition body for elements of kind *)
+ | KD_nabbrev of kind * id * name_scm_opt * nexp (* $Nat$-expression 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 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 (* tagged 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 kind_def 'a = 
+ | KD_aux of (kind_def_aux 'a) * annot 'a
+
+
+type type_def 'a = 
+ | TD_aux of (type_def_aux 'a) * annot '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 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 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 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 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 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 widennum = 
+ | Widennum_widen
+ | Widennum_dont
+ | Widennum_dontcare
+
+
+type widenvec = 
+ | Widenvec_widen
+ | Widenvec_dont
+ | Widenvec_dontcare
+
+
+type widening =  (* Should we widen vector start locations, should we widen atoms and ranges *)
+ | Widening_w of widennum * widenvec
+
+
+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 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 I = inf
+
+
+type E = env
+
+
+type tannot = maybe (t * tag * list nec * effect * effect)
+
+
+
+type i_direction = 
+ | IInc
+ | IDec
 
 
 type reg_id_aux 'a = 
  | RI_id of id
 
 
+type reg_form = 
+ | Form_Reg of id * tannot * i_direction
+ | Form_SubReg of id * reg_form * index_range
+
+
+type ctor_kind = 
+ | C_Enum of nat
+ | C_Union
+
+
+type reg_id 'a = 
+ | RI_aux of (reg_id_aux 'a) * annot 'a
+
+
 type exp_aux 'a =  (* expression *)
  | E_block of list (exp 'a) (* sequential block *)
  | E_nondet of list (exp 'a) (* nondeterministic block *)
@@ -269,10 +525,25 @@ type exp_aux 'a =  (* expression *)
  | 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 *)
+ | E_internal_value of value (* For internal use in interpreter to wrap pre-evaluated values when returning an action *)
 
 and exp 'a = 
  | E_aux of (exp_aux 'a) * annot 'a
 
+and value =  (* interpreter evaluated value *)
+ | V_boxref of nat * t
+ | V_lit of lit
+ | V_tuple of list value
+ | V_list of list value
+ | V_vector of nat * i_direction * list value
+ | V_vector_sparse of nat * nat * i_direction * list (nat * value) * value
+ | V_record of t * list (id * value)
+ | V_ctor of id * t * ctor_kind * value
+ | V_unknown
+ | V_register of reg_form
+ | V_register_alias of alias_spec tannot * tannot
+ | V_track of value * set reg_form
+
 and lexp_aux 'a =  (* lvalue expression *)
  | LEXP_id of id (* identifier *)
  | LEXP_memory of id * list (exp 'a) (* memory or register write via function call *)
@@ -317,24 +588,14 @@ and letbind_aux 'a =  (* let binding *)
 and letbind 'a = 
  | LB_aux of (letbind_aux 'a) * annot 'a
 
+and alias_spec_aux 'a =  (* register alias expression forms *)
+ | 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 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 constraint *)
- | 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
+and alias_spec 'a = 
+ | AL_aux of (alias_spec_aux 'a) * annot 'a
 
 
 type funcl_aux 'a =  (* function clause *)
@@ -350,32 +611,9 @@ 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 *)
- | 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 effect_opt_aux =  (* optional effect annotation for functions *)
+ | Effect_opt_pure (* sugar for empty effect set *)
+ | Effect_opt_effect of effect
 
 
 type funcl 'a = 
@@ -390,22 +628,8 @@ 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_order of order
- | DT_kind of base_kind * kid
- | 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 (* tagged 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 effect_opt = 
+ | Effect_opt_aux of effect_opt_aux * l
 
 
 type val_spec_aux 'a =  (* value type specification *)
@@ -414,13 +638,8 @@ type val_spec_aux 'a =  (* value type specification *)
  | VS_extern_spec of typschm * id * string (* specify the type of a function from Lem *)
 
 
-type kind_def_aux 'a =  (* Definition body for elements of kind *)
- | KD_nabbrev of kind * id * name_scm_opt * nexp (* $Nat$-expression 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 fundef_aux 'a =  (* function definition *)
+ | FD_function of rec_opt * tannot_opt * effect_opt * list (funcl 'a)
 
 
 type scattered_def_aux 'a =  (* scattered function and union type definitions *)
@@ -431,8 +650,10 @@ type scattered_def_aux 'a =  (* scattered function and union type definitions *)
  | 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 default_spec_aux 'a =  (* default kinding or typing assumption *)
+ | DT_order of order
+ | DT_kind of base_kind * kid
+ | DT_typ of typschm * id
 
 
 type dec_spec_aux 'a =  (* register declarations *)
@@ -441,28 +662,20 @@ type dec_spec_aux 'a =  (* register declarations *)
  | 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 fundef 'a = 
+ | FD_aux of (fundef_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 default_spec 'a = 
+ | DT_aux of (default_spec_aux 'a) * l
 
 
 type dec_spec 'a = 
@@ -489,180 +702,4 @@ 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/language/l2.ml b/language/l2.ml
index 318ed604..13cb2567 100644
--- a/language/l2.ml
+++ b/language/l2.ml
@@ -16,8 +16,8 @@ base_kind_aux =  (* base kind *)
 
 
 type 
-base_kind = 
-   BK_aux of base_kind_aux * Parse_ast.l
+kid_aux =  (* kinded IDs: $_$, $_$, $_$, and $_$ variables *)
+   Var of x
 
 
 type 
@@ -27,13 +27,13 @@ id_aux =  (* identifier *)
 
 
 type 
-kid_aux =  (* kinded IDs: $_$, $_$, $_$, and $_$ variables *)
-   Var of x
+base_kind = 
+   BK_aux of base_kind_aux * Parse_ast.l
 
 
 type 
-kind_aux =  (* kinds *)
-   K_kind of (base_kind) list
+kid = 
+   Kid_aux of kid_aux * Parse_ast.l
 
 
 type 
@@ -42,13 +42,8 @@ id =
 
 
 type 
-kid = 
-   Kid_aux of kid_aux * Parse_ast.l
-
-
-type 
-kind = 
-   K_aux of kind_aux * Parse_ast.l
+kind_aux =  (* kinds *)
+   K_kind of (base_kind) list
 
 
 type 
@@ -67,13 +62,21 @@ and nexp =
 
 
 type 
+kind = 
+   K_aux of kind_aux * Parse_ast.l
+
+
+type 
 base_effect_aux =  (* effect *)
    BE_rreg (* read register *)
  | BE_wreg (* write register *)
  | BE_rmem (* read memory *)
+ | BE_rmemt (* read memory and tag *)
  | BE_wmem (* write memory *)
  | BE_eamem (* signal effective address for writing memory *)
+ | BE_exmem (* determine if a store-exclusive (ARM) is going to succeed *)
  | BE_wmv (* write memory, sending only value *)
+ | BE_wmvt (* write memory, sending only value and tag *)
  | BE_barr (* memory barrier *)
  | BE_depend (* dynamic footprint *)
  | BE_undef (* undefined-instruction exception *)
@@ -113,12 +116,6 @@ effect =
 
 
 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
@@ -127,8 +124,9 @@ n_constraint_aux =  (* constraint over kind $_$ *)
 
 
 type 
-kinded_id = 
-   KOpt_aux of kinded_id_aux * Parse_ast.l
+kinded_id_aux =  (* optionally kind-annotated identifier *)
+   KOpt_none of kid (* identifier *)
+ | KOpt_kind of kind * kid (* kind-annotated variable *)
 
 
 type 
@@ -137,6 +135,11 @@ n_constraint =
 
 
 type 
+kinded_id = 
+   KOpt_aux of kinded_id_aux * Parse_ast.l
+
+
+type 
 quant_item_aux =  (* kinded identifier or $_$ constraint *)
    QI_id of kinded_id (* optionally kinded identifier *)
  | QI_const of n_constraint (* $_$ constraint *)
@@ -154,20 +157,6 @@ typquant_aux =  (* type quantifiers 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_string of string (* string constant *)
- | L_undef (* undefined-value constant *)
-
-
-type 
 typquant = 
    TypQ_aux of typquant_aux * Parse_ast.l
 
@@ -195,8 +184,17 @@ and typ_arg =
 
 
 type 
-lit = 
-   L_aux of lit_aux * Parse_ast.l
+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_string of string (* string constant *)
+ | L_undef (* undefined-value constant *)
 
 
 type 
@@ -205,6 +203,26 @@ typschm_aux =  (* type scheme *)
 
 
 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 * Parse_ast.l
+
+
+type 
+lit = 
+   L_aux of lit_aux * Parse_ast.l
+
+
+type 
+typschm = 
+   TypSchm_aux of typschm_aux * Parse_ast.l
+
+
+type 
 'a pat_aux =  (* pattern *)
    P_lit of lit (* literal constant pattern *)
  | P_wild (* wildcard *)
@@ -230,8 +248,191 @@ and 'a fpat =
 
 
 type 
-typschm = 
-   TypSchm_aux of typschm_aux * Parse_ast.l
+name_scm_opt_aux =  (* optional variable naming-scheme constraint *)
+   Name_sect_none
+ | Name_sect_some of string
+
+
+type 
+type_union_aux =  (* type union constructors *)
+   Tu_id of id
+ | Tu_ty_id of typ * id
+
+
+type 
+name_scm_opt = 
+   Name_sect_aux of name_scm_opt_aux * Parse_ast.l
+
+
+type 
+type_union = 
+   Tu_aux of type_union_aux * Parse_ast.l
+
+
+type 
+'a kind_def_aux =  (* Definition body for elements of kind *)
+   KD_nabbrev of kind * id * name_scm_opt * nexp (* $_$-expression 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 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 (* tagged 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 kind_def = 
+   KD_aux of 'a kind_def_aux * 'a annot
+
+
+type 
+'a type_def = 
+   TD_aux of 'a type_def_aux * 'a annot
+
+
+type 
+ne =  (* internal numeric expressions *)
+   Ne_id of x
+ | Ne_var of x
+ | Ne_const of int
+ | Ne_inf
+ | Ne_mult of ne * ne
+ | Ne_add of (ne) list
+ | Ne_minus of ne * ne
+ | Ne_exp of ne
+ | Ne_unary of ne
+
+
+type 
+t =  (* Internal types *)
+   T_id of x
+ | T_var of x
+ | T_fn of t * t * effect
+ | T_tup of (t) list
+ | 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 (t_arg) list
+
+
+type 
+k =  (* Internal kinds *)
+   Ki_typ
+ | Ki_nat
+ | Ki_ord
+ | Ki_efct
+ | Ki_ctor of (k) list * k
+ | Ki_infer (* Representing an unknown kind, inferred by context *)
+
+
+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 
+nec =  (* Numeric expression constraints *)
+   Nec_lteq of ne * ne
+ | Nec_eq of ne * ne
+ | Nec_gteq of ne * ne
+ | Nec_in of x * (int) list
+ | Nec_cond of (nec) list * (nec) list
+ | Nec_branch of (nec) list
+
+
+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 string option (* 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 int
+ | Tag_alias
+ | Tag_unknown of string option (* 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 e_k * s_N * tag * t
+
+
+type 
+conformsto =  (* how much conformance does overloading need *)
+   Conformsto_full
+ | Conformsto_parm
+
+
+type 
+widennum = 
+   Widennum_widen
+ | Widennum_dont
+ | Widennum_dontcare
+
+
+type 
+widenvec = 
+   Widenvec_widen
+ | Widenvec_dont
+ | Widenvec_dontcare
+
+
+type 
+widening =  (* Should we widen vector start locations, should we widen atoms and ranges *)
+   Widening_w of widennum * widenvec
+
+
+type 
+tinflist =  (* In place so that a list of tinfs can be referred to without the dot form *)
+   Tinfs_empty
+ | Tinfs_ls of (tinf) list
+
+
+type 
+i =  (* Information given by type checking an expression *)
+   I of s_N * effect
+ | Iempty (* Empty constraints, effect *)
+ | Singleunion of i * i
+ | Iunion of (i) list (* Unions the constraints and effect *)
+
+
+type 
+e =  (* Definition environment and lexical environment *)
+   E of e_t * e_d
+ | E_union of e * e
+
+
+type 
+i_direction = 
+   IInc
+ | IDec
 
 
 type 
@@ -240,6 +441,23 @@ type
 
 
 type 
+ctor_kind = 
+   C_Enum of nat
+ | C_Union
+
+
+type 
+reg_form = 
+   Form_Reg of id * tannot * i_direction
+ | Form_SubReg of id * reg_form * index_range
+
+
+type 
+'a reg_id = 
+   RI_aux of 'a reg_id_aux * 'a annot
+
+
+type 
 'a exp_aux =  (* expression *)
    E_block of ('a exp) list (* sequential block *)
  | E_nondet of ('a exp) list (* nondeterministic block *)
@@ -279,10 +497,25 @@ type
  | 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 *)
+ | E_internal_value of value (* For internal use in interpreter to wrap pre-evaluated values when returning an action *)
 
 and 'a exp = 
    E_aux of 'a exp_aux * 'a annot
 
+and value =  (* interpreter evaluated value *)
+   V_boxref of nat * t
+ | V_lit of lit
+ | V_tuple of (value) list
+ | V_list of (value) list
+ | V_vector of nat * i_direction * (value) list
+ | V_vector_sparse of nat * nat * i_direction * ((nat * value)) list * value
+ | V_record of t * ((id * value)) list
+ | V_ctor of id * t * ctor_kind * value
+ | V_unknown
+ | V_register of reg_form
+ | V_register_alias of tannot alias_spec * tannot
+ | V_track of value * reg_form_set
+
 and 'a lexp_aux =  (* lvalue expression *)
    LEXP_id of id (* identifier *)
  | LEXP_memory of id * ('a exp) list (* memory or register write via function call *)
@@ -327,28 +560,14 @@ and 'a letbind_aux =  (* let binding *)
 and 'a letbind = 
    LB_aux of 'a letbind_aux * 'a annot
 
+and 'a alias_spec_aux =  (* register alias expression forms *)
+   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 
-'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 constraint *)
-   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
+and 'a alias_spec = 
+   AL_aux of 'a alias_spec_aux * 'a annot
 
 
 type 
@@ -368,36 +587,9 @@ tannot_opt_aux =  (* optional type annotation for functions *)
 
 
 type 
-'a alias_spec_aux =  (* register alias expression forms *)
-   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 * Parse_ast.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 * Parse_ast.l
-
-
-type 
-name_scm_opt = 
-   Name_sect_aux of name_scm_opt_aux * Parse_ast.l
-
-
-type 
-effect_opt = 
-   Effect_opt_aux of effect_opt_aux * Parse_ast.l
+effect_opt_aux =  (* optional effect annotation for functions *)
+   Effect_opt_pure (* sugar for empty effect set *)
+ | Effect_opt_effect of effect
 
 
 type 
@@ -416,24 +608,8 @@ tannot_opt =
 
 
 type 
-'a alias_spec = 
-   AL_aux of 'a alias_spec_aux * 'a annot
-
-
-type 
-'a default_spec_aux =  (* default kinding or typing assumption *)
-   DT_order of order
- | DT_kind of base_kind * kid
- | 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 (* tagged 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 *)
+effect_opt = 
+   Effect_opt_aux of effect_opt_aux * Parse_ast.l
 
 
 type 
@@ -444,13 +620,8 @@ type
 
 
 type 
-'a kind_def_aux =  (* Definition body for elements of kind *)
-   KD_nabbrev of kind * id * name_scm_opt * nexp (* $_$-expression 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 *)
+'a fundef_aux =  (* function definition *)
+   FD_function of rec_opt * tannot_opt * effect_opt * ('a funcl) list
 
 
 type 
@@ -463,8 +634,10 @@ type
 
 
 type 
-'a fundef_aux =  (* function definition *)
-   FD_function of rec_opt * tannot_opt * effect_opt * ('a funcl) list
+'a default_spec_aux =  (* default kinding or typing assumption *)
+   DT_order of order
+ | DT_kind of base_kind * kid
+ | DT_typ of typschm * id
 
 
 type 
@@ -475,23 +648,13 @@ type
 
 
 type 
-'a default_spec = 
-   DT_aux of 'a default_spec_aux * Parse_ast.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
+'a fundef = 
+   FD_aux of 'a fundef_aux * 'a annot
 
 
 type 
@@ -500,8 +663,8 @@ type
 
 
 type 
-'a fundef = 
-   FD_aux of 'a fundef_aux * 'a annot
+'a default_spec = 
+   DT_aux of 'a default_spec_aux * Parse_ast.l
 
 
 type 
diff --git a/language/l2.ott b/language/l2.ott
index 803472a8..c78c66f8 100644
--- a/language/l2.ott
+++ b/language/l2.ott
@@ -10,6 +10,11 @@ metavar num,numZero,numOne ::=
   {{ lem integer }}
   {{ com Numeric literals }}
 
+metavar nat ::=
+  {{ phantom }}
+  {{ lex numeric }}
+  {{ lem nat }}
+
 metavar hex ::=
   {{ phantom }}
   {{ lex numeric }}
@@ -47,6 +52,8 @@ type 'a annot = l * 'a
 
 embed
 {{ lem
+open import Pervasives
+open import Pervasives_extra
 open import Map
 open import Maybe
 open import Set_extra
@@ -545,12 +552,405 @@ P_app <= P_app
 P_app <= P_as
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% Machinery for typing rules                                   %
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+embed
+{{ lem
+
+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
+}}
+
+ 
+grammar 
+
+k :: 'Ki_' ::=
+{{ com Internal kinds }}
+   | K_Typ                                             :: :: typ
+   | K_Nat                                             :: :: nat
+   | K_Ord                                             :: :: ord
+   | K_Efct                                             :: :: efct
+   | K_Lam ( k0 .. kn -> k' )                  :: :: ctor
+   | K_infer                                           :: :: infer {{ com Representing an unknown kind, inferred by context }}
+
+t , u :: 'T_' ::=                                
+{{ com Internal types }}
+   | x                                            :: :: id
+   | ' x                                          :: :: var
+   | t1 -> t2 effect                        :: :: fn 
+   | ( t1 , .... , tn )                           :: :: tup
+   | x < t_args >                           :: :: app 
+   | t |-> t1                                   :: :: abbrev
+   | register < t_arg >                  :: S :: reg_app {{ ichlo T_app "register" [[t_arg]] }}
+   | range < ne ne' > 			  :: S :: range_app {{ ichlo T_app "range" [[ [ ne ; ne' ] ]] }}
+   | atom < ne >    			  :: S :: atom_app {{ ichlo T_app "atom" [ [[ne]] ] }}
+   | vector < ne ne' order t >           :: S :: vector_app {{ ichlo T_app "vector" [[ [ ne; ne'; ord; t ] ]] }} 
+   | list < t >      	     		 :: S :: list_app {{ ichlo T_app "list" [[t]] }}
+   | reg < t >				 :: S :: box_app {{ ichlo T_app "reg" [[t]] }}
+   | implicit < ne >                      :: S :: implicit_app {{ ichlo T_app "implicit" [[ne]] }}
+   | bit      	     	   	       	          :: S :: bit_typ {{ ichlo T_id "bit" }}
+   | string                                    :: S :: string_typ {{ ichlo T_id "string" }}
+   | unit                                       :: S :: unit_typ {{ ichlo T_id "unit" }} 
+   | t [ t_arg1 / tid1 .. t_argn / tidn ]  :: M :: subst {{ ichlo "todo" }}
+
+optx :: '' ::= {{ phantom }} {{ lem maybe string }} {{ ocaml string option }}
+  | x                                            ::  :: optx_x
+  {{ lem (Just [[x]]) }} {{ ocaml (Some [[x]]) }}
+  |                                              :: :: optx_none
+  {{ lem Nothing }} {{ ocaml None }}
+
+
+tag :: 'Tag_' ::=                                 
+{{ com Data indicating where the identifier arises and thus information necessary in compilation }}
+   | None                                 :: :: empty
+   | Intro                                :: :: intro {{ com Denotes an assignment and lexp that introduces a binding }}
+   | Set                                  :: :: set {{ com Denotes an expression that mutates a local variable }}
+   | Tuple                                :: :: tuple_assign {{ com Denotes an assignment with a tuple lexp }}
+   | Global				  :: :: global {{ com Globally let-bound or enumeration based value/variable }} 
+   | Ctor                                 :: :: ctor {{ com Data constructor from a type union }}
+   | Extern optx                          :: :: extern {{ com External function, specied only with a val statement }}
+   | Default                              :: :: default {{ com Type has come from default declaration, identifier may not be bound locally }}
+   | Spec				  :: :: spec
+   | Enum num				  :: :: enum
+   | Alias				  :: :: alias
+   | Unknown_path optx			  :: :: unknown {{ com Tag to distinguish an unknown path from a non-analysis non deterministic path}}
+
+ne :: 'Ne_' ::=
+ {{ com internal numeric expressions }}
+   | x                                   :: :: id
+   | ' x                                 :: :: var
+   | num                                 :: :: const
+   | infinity                            :: :: inf
+   | ne1 * ne2                           :: :: mult
+   | ne1 + ... + nen                     :: :: add
+   | ne1 - ne2 	 		       :: :: minus
+   | 2 ** ne				 :: :: exp
+   | ( - ne )                            :: :: unary
+   | zero   				 :: S :: zero
+     {{ ichlo (Ne_const 0) }}
+   | one				 :: S :: one
+     {{ ichlo (Ne_const 1) }}
+   | bitlength ( bin )                   :: M :: cbin
+     {{ ocaml (asssert false) }}
+     {{ hol ARB }}
+     {{ lem (blength [[bin]]) }}
+   | bitlength ( hex )                   :: M :: chex
+     {{ ocaml (assert false) }}
+     {{ hol ARB }}
+     {{ lem (hlength [[hex]]) }}
+   | count ( num0 ... numi )                :: M :: length {{ichlo "todo" }}
+   | length ( pat1 ... patn )            :: M :: cpat
+     {{ ocaml (assert false) }}
+     {{ hol ARB }}
+     {{ lem (Ne_const (List.length [[pat1...patn]])) }}
+   | length ( exp1 ... expn )            :: M :: cexp
+     {{ hol ARB }}
+     {{ ocaml (assert false) }}
+     {{ lem (Ne_const (List.length [[exp1...expn]])) }}
+ 
+ t_arg :: 't_arg_' ::=  
+ {{ com Argument to type constructors }}
+ | t :: :: typ
+ | ne :: :: nexp
+ | effect :: :: effect
+ | order :: :: order
+ | fresh :: M :: freshvar {{ ichlo T_arg (T_var "fresh") }}
+
+ t_args :: '' ::=   {{ lem list t_arg }}
+  {{ com Arguments to type constructors }}
+   | t_arg1 ... t_argn                            :: :: T_args
+
+ nec :: 'Nec_' ::=
+   {{ com Numeric expression constraints }}
+   | ne <= ne'            :: :: lteq
+   | ne = ne'            :: :: eq
+   | ne >= ne'           :: :: gteq
+   | ' x 'IN' { num1 , ... , numn } :: :: in
+   | nec0 .. necn -> nec'0 ... nec'm :: :: cond
+   | nec0 ... necn                   :: :: branch
+
+S_N {{ tex {\Sigma^{\textsc{N} } } }} :: '' ::= {{ phantom }}
+                                                                    {{ hol nec list }}
+                                                                    {{ lem list nec }}
+    {{ com nexp constraint lists }}
+    | { nec1 , .. ,  necn }                              :: :: Sn_concrete
+      {{ hol [[nec1 .. necn]] }}
+      {{ lem [[nec1 .. necn]] }}
+   | S_N1 u+ .. u+ S_Nn                                                    :: M :: SN_union
+     {{ hol (FOLDR FUNION FEMPTY [[S_N1..S_Nn]]) }}
+     {{ lem (List.foldr (++) [] [[S_N1..S_Nn]]) }}
+     {{ ocaml (assert false) }}
+   | consistent_increase ne1 ne'1 ... nen ne'n                    :: M :: SN_increasing
+     {{ com Generates constraints from  pairs of constraints, where the first of each pair is always larger than the sum of the previous pair }}
+     {{ ocaml (assert false) }}
+     {{ ichl todo }}
+   | consistent_decrease ne1 ne'1 ... nen ne'n                      :: M :: SN_decreasing
+     {{ com Generates constraints from  pairs of constraints, where the first of each pair is always smaller than the difference of the previous pair }}
+     {{ ocaml assert false }}
+     {{ ichl todo }}
+   | resolve ( S_N )                                                :: :: resolution
+     {{ lem [[S_N]] (* Write constraint solver *) }}
+ 
+
+ E_d {{ tex {\ottnt{E}^{\textsc{d} } } }} :: 'E_d_' ::=  {{ phantom }}
+                                                         {{ lem definition_env }}
+ {{ com Environments storing top level information, such as defined abbreviations, records, enumerations, and kinds }}
+ | < E_k , E_a , E_r , E_e >	     	       		    	 :: :: base
+   {{ hol arb }}
+   {{ lem (Denv [[E_k]] [[E_r]] [[E_e]]) }}
+ | empty       	     					 :: :: empty
+   {{ hol arb }}
+   {{ lem DenvEmp }}
+ | E_d u+ E_d'						 :: :: union
+   {{ hol arb }}
+   {{ lem (denv_union [[E_d]] [[E_d']]) }}
+ 
+ kinf :: 'kinf_' ::=
+   {{ com Whether a kind is default or from a local binding }}
+   | k                                        :: :: k
+   | k default                                :: :: def
+
+ tid :: 'tid_' ::=
+   {{ com A type identifier or type variable }}
+   | id                                      :: :: id
+   | kid                                     :: :: var
+
+ E_k {{ tex {\ottnt{E}^{\textsc{k} } } }} :: 'E_k_' ::=             {{ phantom }}
+                                                                 {{ hol (tid-> kinf) }}
+                                                                 {{ lem (map tid kinf) }}
+   {{ com Kind environments }}
+   | { tid1 |-> kinf1 , .. , tidn |-> kinfn }    :: :: concrete
+     {{ hol (FOLDR (\(k1,k2) E. E |+ (k1,k2)) FEMPTY [[tid1 kinf1 .. tidn kinfn]]) }}
+     {{ lem (List.foldr (fun (x,v) m -> Map.insert x v m) Map.empty [[tid1 kinf1 .. tidn kinfn]]) }} 
+   | E_k1 u+ .. u+ E_kn                                          :: M :: union
+     {{ com In a unioning kinf, {k default} u {k} results in {k} (i.e. the default is locally forgotten) }} 
+     {{ hol (FOLDR FUNION FEMPTY [[E_k1..E_kn]]) }}
+     {{ lem (List.foldr (union) Map.empty [[E_k1..E_kn]]) }}
+     {{ ocaml (assert false) }}
+   | E_k u- E_k1 .. E_kn                                            :: M :: multi_set_minus
+     {{ hol arb }} 
+     {{ lem (Map.fromList (remove_from (Set_extra.toList (Map.toSet [[E_k]]))
+                                       (Set_extra.toList (Map.toSet (List.foldr (union) Map.empty [[E_k1..E_kn]]))))) }} 
+     {{ ocaml assert false }}
+
+ tinf :: 'tinf_' ::=                                                 
+    {{ com Type variables, type, and constraints, bound to an identifier }}
+    | t                                                 :: :: typ
+    | E_k , S_N , tag , t         :: :: quant_typ                                                             
+
+tinflist :: 'tinfs_' ::=
+  {{ com In place so that a list of tinfs can be referred to without the dot form }}
+  | empty :: :: empty
+  | tinf1 ... tinfn  :: :: ls
+
+conformsto :: 'conformsto_' ::=
+  {{ com how much conformance does overloading need }}
+ | full :: :: full
+ | parm :: :: parm
+
+widenvec :: 'widenvec_' ::=
+  | vectors :: :: widen
+  | none    :: :: dont
+  | _       :: :: dontcare
+
+widennum :: 'widennum_' ::=
+  | nums  :: :: widen
+  | none  :: :: dont
+  | _     :: :: dontcare
+
+widening :: 'widening_' ::=
+  {{ com Should we widen vector start locations, should we widen atoms and ranges }}
+  | ( widennum , widenvec ) :: :: w
+
+ E_a {{ tex \ottnt{E}^{\textsc{a} } }} :: 'E_a_' ::=   {{ phantom }}
+                                                                            {{ hol tid |-> tinf}}
+                                                                            {{ lem map tid tinf }} 
+   | { tid1 |-> tinf1 , .. , tidn |-> tinfn } :: :: concrete
+   | E_a1 u+ .. u+ E_an	               :: :: union
+
+ field_typs :: 'FT_' ::=     {{ phantom }}
+                             {{ lem list (id * t) }}
+ {{ com Record fields }}
+ | id1 : t1 , .. , idn : tn :: :: fields
+   {{ lem [[id1 t1..idn tn]] }}
+
+ E_r {{ tex \ottnt{E}^{\textsc{r} } }} :: 'E_r_' ::=             {{ phantom }}
+                                                                 {{ hol (id*t) |-> tinf) }}
+                                                                 {{ lem map (list (id*t)) tinf }}
+   {{ com Record environments }}
+   | { { field_typs1 } |-> tinf1 , .. , { field_typsn } |-> tinfn }                    :: :: concrete
+     {{ hol (FOLDR (\x E. E |+ x) FEMPTY) }}
+     {{ lem (List.foldr (fun (x,f) m -> Map.insert x f m) Map.empty [[field_typs1 tinf1..field_typsn tinfn]]) }} 
+   | E_r1 u+ .. u+ E_rn                                          :: M :: union
+     {{ hol (FOLDR FUNION FEMPTY [[E_r1..E_rn]]) }}
+     {{ lem (List.foldr (union) Map.empty [[E_r1..E_rn]]) }}
+     {{ ocaml (assert false) }}
+
+  enumerate_map :: '' ::=                                        {{ phantom }}
+                                                                 {{ lem (list (nat*id)) }}
+   | { num1 |-> id1 ... numn |-> idn }                           :: :: enum_map
+    {{ lem [[num1 id1...numn idn]] }}
+
+  E_e {{ tex \ottnt{E}^{\textsc{e} } }} :: 'E_e_' ::=            {{ phantom }}
+                                                                 {{ lem (map t (list (nat*id))) }}
+   {{ com Enumeration environments }}
+   | { t1 |-> enumerate_map1 , .. , tn |-> enumerate_mapn }     :: :: base
+     {{ lem (List.foldr (fun (x,f) m -> Map.insert x f m) Map.empty [[t1 enumerate_map1..tn enumerate_mapn]]) }} 
+   | E_e1 u+ .. u+ E_en                                         :: :: union
+     {{ lem (List.foldr (union) Map.empty [[E_e1..E_en]]) }}
+
+    
+embed
+{{ lem
+ type definition_env =
+   | DenvEmp
+   | Denv of (map tid kinf) * (map (list (id*t)) tinf) * (map t (list (nat*id)))
+
+}}
+
+grammar
+
+ E_t {{ tex {\ottnt{E}^{\textsc{t} } } }} :: 'E_t_' ::=          {{ phantom }}
+                                                                 {{ hol (id |-> tinf) }}
+                                                                 {{ lem map id tinf }}
+   {{ com Type environments }}
+   | { id1 |-> tinf1 , .. , idn |-> tinfn }                    :: :: base
+     {{ hol (FOLDR (\x E. E |+ x) FEMPTY [[id1 tinf1 .. idn tinfn]]) }}
+     {{ lem (List.foldr (fun (x,f) m -> Map.insert x f m) Map.empty [[id1 tinf1 .. idn tinfn]]) }} 
+   | { id |-> overload tinf conformsto : tinf1 , ... , tinfn }        :: :: overload
+   | ( E_t1 u+ .... u+ E_tn )                                         :: M :: union
+     {{ hol (FOLDR FUNION FEMPTY [[E_t1....E_tn]]) }}
+     {{ lem (List.foldr (union) Map.empty [[E_t1....E_tn]]) }}
+     {{ ocaml (assert false) }}
+   | u+ E_t1 .. E_tn                                            :: M :: multi_union
+     {{ hol arb }}
+     {{ lem (List.foldr (union) Map.empty [[E_t1..E_tn]]) }}
+     {{ ocaml assert false }}
+   | E_t u- id1 .. idn                                            :: M :: multi_set_minus
+     {{ hol arb }} 
+     {{ lem (Map.fromList (remove_from (Set_extra.toList (Map.toSet [[E_t]]))
+                                       (Set_extra.toList (Map.toSet (List.foldr (union) Map.empty [[id1..idn]]))))) }} 
+     {{ ocaml assert false }}
+   | ( E_t1 inter .... inter E_tn )                                  :: M :: intersect
+     {{ hol arb }}
+     {{ lem (List.foldr (fun a b -> (Map.fromList (Set_extra.toList ((Map.toSet a) inter (Map.toSet b)))))  Map.empty [[E_t1....E_tn]]) }} 
+     {{ ocaml (assert false) }}
+   | inter E_t1 .. E_tn                                            :: M :: multi_inter
+     {{ hol arb }}
+     {{ lem (List.foldr (fun a b -> (Map.fromList (Set_extra.toList ((Map.toSet a) inter (Map.toSet b))))) Map.empty [[E_t1..E_tn]]) }}
+     {{ ocaml assert false }}
+
+
+ts :: ts_ ::=                                     {{ phantom }}
+                                                  {{ lem list t }}
+  | t1 , .. , tn :: :: lst 
+
+embed
+{{ lem
+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*)
+
+}}
+
+grammar
+
+ E :: '' ::=                                                     
+                                                                 {{ hol ((string,env_body) fmaptree) }}
+                                                                 {{ lem env }}
+ {{ com Definition environment and lexical environment }}
+ | < E_t , E_d >                                           :: :: E
+  {{ hol arb }}
+  {{ lem (Env [[E_t]] [[E_d]])  }}
+ | empty                                                       :: M :: E_empty
+   {{ hol arb }}
+   {{ lem EnvEmp }}
+   {{ ocaml assert false }}
+ | E u+ E'                                                      :: :: E_union
+   {{ lem (env_union [[E]] [[E']]) }}
+
+ I :: '' ::=                                                     {{ lem inf }}
+  {{ com Information given by type checking an expression }}
+  | < S_N , effect >                                      :: :: I
+    {{ lem (Inf [[S_N]] [[effect]]) }}
+  | Ie                                                           :: :: Iempty {{ com Empty constraints, effect }} {{ tex {\ottnt{I}_{\epsilon} } }}
+    {{ lem Iemp }}
+  | ( I1 u+ I2 ) :: :: singleunion {{ tex [[I1]] [[u+]] [[I2]] }}
+  | I1 u+ .. u+ In                                               :: :: Iunion {{ com Unions the constraints and effect }}
+    {{ lem (List.foldr inf_union Iemp [[I1..In]]) }}
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 % Expressions                                                  %
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
+embed
+{{ lem
+
+type tannot = maybe (t * tag * list nec * effect * effect)
 
+}}
 
 grammar
+tannot :: '' ::=
+                                                {{ phantom }}
+                                                {{ ocaml tannot }}
+                                                {{ lem tannot }}
+
+
 
 exp :: 'E_' ::=
   {{ com expression }}
@@ -689,7 +1089,37 @@ exp :: 'E_' ::=
   | let lexp = exp in exp'    :: I :: internal_let {{ com This is an internal node for compilation that demonstrates the scope of a local mutable variable }}
   | let pat = exp in exp' :: I :: internal_plet {{ com This is an internal node, used to distinguised some introduced lets during processing from original ones }}
   | return_int ( exp )                                          :: I :: internal_return {{ com For internal use to embed into monad definition }}
-
+  | value :: I :: internal_value {{ com For internal use in interpreter to wrap pre-evaluated values when returning an action }}
+
+i_direction :: 'I' ::=
+  | IInc :: :: Inc
+  | IDec :: :: Dec
+
+ctor_kind :: 'C_' ::=
+  | C_Enum nat :: :: Enum
+  | C_Union    :: :: Union
+
+reg_form :: 'Form_' ::=
+  | Reg id tannot i_direction :: :: Reg
+  | SubReg id reg_form index_range :: :: SubReg
+
+reg_form_set :: '' ::= {{ phantom }} {{ lem set reg_form }}
+
+alias_spec_tannot :: '' ::= {{ phantom }} {{ lem alias_spec tannot }} {{ ocaml tannot alias_spec }}
+
+value :: 'V_' ::= {{ com interpreter evaluated value }}
+  | Boxref nat t                                                                    :: :: boxref
+  | Lit lit                                                                         :: :: lit
+  | Tuple ( value1 , ... , valuen )                                                 :: :: tuple
+  | List ( value1 , ... , valuen )                                                  :: :: list
+  | Vector nat i_direction ( value1 , ... , valuen )                                :: :: vector
+  | Vector_sparse nat' nat'' i_direction ( nat1 value1 , ... , natn valuen ) value' :: :: vector_sparse
+  | Record t ( id1 value1 , ... , idn valuen )                                      :: :: record
+  | V_ctor id t ctor_kind value1                                                    :: :: ctor
+  | Unknown                                                                         :: :: unknown
+  | Register reg_form                                                               :: :: register
+  | Register_alias alias_spec_tannot tannot                                         :: :: register_alias
+  | Track value reg_form_set                                                        :: :: track
 
 lexp :: 'LEXP_' ::= {{ com lvalue expression }}
     {{ aux _ annot }} {{ auxparam 'a }}