Merge remote-tracking branch 'origin/master' into sail_new_tc

1 files changed, 365 insertions, 332 deletions

diff --git a/src/lem_interp/interp_ast.lem b/src/lem_interp/interp_ast.lem
index b706d3aa..733d1a36 100644
--- a/src/lem_interp/interp_ast.lem
+++ b/src/lem_interp/interp_ast.lem
@@ -40,9 +40,11 @@
 (*  SUCH DAMAGE.                                                          *)
 (*========================================================================*)
 
-(* 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
@@ -72,21 +74,17 @@ 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 =  (* variables with kind, ticked to differntiate from program variables *)
+type kid_aux =  (* kinded IDs: $Type$, $Nat$, $Order$, and $Effect$ variables *)
  | Var of x
 
 
-type id_aux =  (* Identifier *)
+type id_aux =  (* identifier *)
  | Id of x
  | 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 = 
@@ -97,24 +95,28 @@ 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 =  (* expression of kind Nat, for vector sizes and origins *)
- | Nexp_id of id (* identifier, bound by def Nat x = nexp *)
+type nexp_aux =  (* numeric expression, of kind $Nat$ *)
+ | Nexp_id of id (* abbreviation identifier *)
  | Nexp_var of kid (* variable *)
  | Nexp_constant of integer (* constant *)
  | Nexp_times of nexp * nexp (* product *)
  | Nexp_sum of nexp * nexp (* sum *)
  | Nexp_minus of nexp * nexp (* subtraction *)
  | Nexp_exp of nexp (* exponential *)
- | Nexp_neg of nexp (* For internal use *)
+ | Nexp_neg of nexp (* for internal use only *)
 
 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 *)
@@ -129,23 +131,23 @@ type base_effect_aux =  (* effect *)
  | BE_depend (* dynamic footprint *)
  | BE_undef (* undefined-instruction exception *)
  | BE_unspec (* unspecified values *)
- | BE_nondet (* nondeterminism from intra-instruction parallelism *)
- | BE_escape (* Tracking of expressions and functions that might call exit *)
- | BE_lset (* Local mutation happend; not user-writable *)
- | BE_lret (* Local return happened; not user-writable *)
+ | BE_nondet (* nondeterminism, from $nondet$ *)
+ | BE_escape (* potential call of  $exit$ *)
+ | BE_lset (* local mutation; not user-writable *)
+ | BE_lret (* local return; not user-writable *)
 
 
 type base_effect = 
  | BE_aux of base_effect_aux * l
 
 
-type order_aux =  (* vector order specifications, of kind Order *)
+type order_aux =  (* vector order specifications, of kind $Order$ *)
  | Ord_var of kid (* variable *)
- | Ord_inc (* increasing (little-endian) *)
- | Ord_dec (* decreasing (big-endian) *)
+ | Ord_inc (* increasing *)
+ | Ord_dec (* decreasing *)
 
 
-type effect_aux =  (* effect set, of kind Effects *)
+type effect_aux =  (* effect set, of kind $Effect$ *)
  | Effect_var of kid
  | Effect_set of list base_effect (* effect set *)
 
@@ -163,11 +165,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
@@ -175,17 +172,22 @@ 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 quant_item_aux =  (* Either a kinded identifier or a nexp constraint for a typquant *)
- | QI_id of kinded_id (* An optionally kinded identifier *)
- | QI_const of n_constraint (* A constraint for this type *)
+type 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 *)
 
 
 type quant_item = 
@@ -194,38 +196,25 @@ type quant_item =
 
 type typquant_aux =  (* type quantifiers and constraints *)
  | TypQ_tq of list quant_item
- | TypQ_no_forall (* sugar, omitting quantifier and constraints *)
-
-
-type lit_aux =  (* Literal constant *)
- | L_unit (* $() : unit$ *)
- | L_zero (* $bitzero : bit$ *)
- | L_one (* $bitone : bit$ *)
- | L_true (* $true : bool$ *)
- | L_false (* $false : bool$ *)
- | L_num of integer (* natural number constant *)
- | L_hex of string (* bit vector constant, C-style *)
- | L_bin of string (* bit vector constant, C-style *)
- | L_undef (* constant representing undefined values *)
- | L_string of string (* string constant *)
+ | TypQ_no_forall (* empty *)
 
 
 type typquant = 
  | TypQ_aux of typquant_aux * l
 
 
-type typ_aux =  (* Type expressions, of kind $Type$ *)
- | Typ_wild (* Unspecified type *)
- | Typ_id of id (* Defined type *)
- | Typ_var of kid (* Type variable *)
- | Typ_fn of typ * typ * effect (* Function type (first-order only in user code) *)
- | Typ_tup of list typ (* Tuple type *)
+type typ_aux =  (* type expressions, of kind $Type$ *)
+ | Typ_wild (* unspecified type *)
+ | Typ_id of id (* defined type *)
+ | Typ_var of kid (* type variable *)
+ | Typ_fn of typ * typ * effect (* Function (first-order only in user code) *)
+ | Typ_tup of list typ (* Tuple *)
  | Typ_app of id * list typ_arg (* type constructor application *)
 
 and typ = 
  | Typ_aux of typ_aux * l
 
-and typ_arg_aux =  (* Type constructor arguments of all kinds *)
+and typ_arg_aux =  (* type constructor arguments of all kinds *)
  | Typ_arg_nexp of nexp
  | Typ_arg_typ of typ
  | Typ_arg_order of order
@@ -235,15 +224,41 @@ 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 pat_aux 'a =  (* Pattern *)
+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 *)
  | P_as of (pat 'a) * id (* named pattern *)
@@ -260,207 +275,33 @@ type pat_aux 'a =  (* Pattern *)
 and pat 'a = 
  | P_aux of (pat_aux 'a) * annot 'a
 
-and fpat_aux 'a =  (* Field pattern *)
+and fpat_aux 'a =  (* field pattern *)
  | FP_Fpat of id * (pat 'a)
 
 and fpat 'a = 
  | FP_aux of (fpat_aux 'a) * annot 'a
 
 
-type typschm = 
- | TypSchm_aux of typschm_aux * l
-
-
-type reg_id_aux 'a = 
- | RI_id of id
-
-
-type exp_aux 'a =  (* Expression *)
- | E_block of list (exp 'a) (* block *)
- | E_nondet of list (exp 'a) (* nondeterminisitic block, expressions evaluate in an unspecified order, or concurrently *)
- | E_id of id (* identifier *)
- | E_lit of lit (* literal constant *)
- | E_cast of typ * (exp 'a) (* cast *)
- | E_app of id * list (exp 'a) (* function application *)
- | E_app_infix of (exp 'a) * id * (exp 'a) (* infix function application *)
- | E_tuple of list (exp 'a) (* tuple *)
- | E_if of (exp 'a) * (exp 'a) * (exp 'a) (* conditional *)
- | E_for of id * (exp 'a) * (exp 'a) * (exp 'a) * order * (exp 'a) (* loop *)
- | E_vector of list (exp 'a) (* vector (indexed from 0) *)
- | E_vector_indexed of list (integer * (exp 'a)) * (opt_default 'a) (* vector (indexed consecutively) *)
- | E_vector_access of (exp 'a) * (exp 'a) (* vector access *)
- | E_vector_subrange of (exp 'a) * (exp 'a) * (exp 'a) (* subvector extraction *)
- | E_vector_update of (exp 'a) * (exp 'a) * (exp 'a) (* vector functional update *)
- | E_vector_update_subrange of (exp 'a) * (exp 'a) * (exp 'a) * (exp 'a) (* vector subrange update (with vector) *)
- | E_vector_append of (exp 'a) * (exp 'a) (* vector concatenation *)
- | E_list of list (exp 'a) (* list *)
- | E_cons of (exp 'a) * (exp 'a) (* cons *)
- | E_record of (fexps 'a) (* struct *)
- | E_record_update of (exp 'a) * (fexps 'a) (* functional update of struct *)
- | E_field of (exp 'a) * id (* field projection from struct *)
- | E_case of (exp 'a) * list (pexp 'a) (* pattern matching *)
- | E_let of (letbind 'a) * (exp 'a) (* let expression *)
- | E_assign of (lexp 'a) * (exp 'a) (* imperative assignment *)
- | E_sizeof of nexp (* Expression to return the value of the nexp variable or expression at run time *)
- | E_exit of (exp 'a) (* expression to halt all current execution, potentially calling a system, trap, or interrupt handler with exp *)
- | E_return of (exp 'a) (* expression to end current function execution and return the value of exp from the function; this can be used to break out of for loops *)
- | E_assert of (exp 'a) * (exp 'a) (* expression to halt with error, when the first expression is false, reporting the optional string as an error *)
- | E_internal_cast of annot 'a * (exp 'a) (* This is an internal cast, generated during type checking that will resolve into a syntactic cast after *)
- | E_internal_exp of annot 'a (* This is an internal use for passing nexp information  to library functions, postponed for constraint solving *)
- | E_sizeof_internal of annot 'a (* For sizeof during type checking, to replace nexp with internal n *)
- | E_internal_exp_user of annot 'a * annot 'a (* This is like the above but the user has specified an implicit parameter for the current function *)
- | E_comment of string (* For generated unstructured comments *)
- | E_comment_struc of (exp 'a) (* For generated structured comments *)
- | E_internal_let of (lexp 'a) * (exp 'a) * (exp 'a) (* This is an internal node for compilation that demonstrates the scope of a local mutable variable *)
- | E_internal_plet of (pat 'a) * (exp 'a) * (exp 'a) (* This is an internal node, used to distinguised some introduced lets during processing from original ones *)
- | E_internal_return of (exp 'a) (* For internal use to embed into monad definition *)
-
-and exp 'a = 
- | E_aux of (exp_aux 'a) * annot 'a
-
-and lexp_aux 'a =  (* lvalue expression *)
- | LEXP_id of id (* identifier *)
- | LEXP_memory of id * list (exp 'a) (* memory write via function call *)
- | LEXP_cast of typ * id
- | LEXP_tup of list (lexp 'a) (* set multiple at a time, a check will ensure it's not memory *)
- | LEXP_vector of (lexp 'a) * (exp 'a) (* vector element *)
- | LEXP_vector_range of (lexp 'a) * (exp 'a) * (exp 'a) (* subvector *)
- | LEXP_field of (lexp 'a) * id (* struct field *)
-
-and lexp 'a = 
- | LEXP_aux of (lexp_aux 'a) * annot 'a
-
-and fexp_aux 'a =  (* Field-expression *)
- | FE_Fexp of id * (exp 'a)
-
-and fexp 'a = 
- | FE_aux of (fexp_aux 'a) * annot 'a
-
-and fexps_aux 'a =  (* Field-expression list *)
- | FES_Fexps of list (fexp 'a) * bool
-
-and fexps 'a = 
- | FES_aux of (fexps_aux 'a) * annot 'a
-
-and opt_default_aux 'a =  (* Optional default value for indexed vectors, to define a defualt value for any unspecified positions in a sparse map *)
- | Def_val_empty
- | Def_val_dec of (exp 'a)
-
-and opt_default 'a = 
- | Def_val_aux of (opt_default_aux 'a) * annot 'a
-
-and pexp_aux 'a =  (* Pattern match *)
- | Pat_exp of (pat 'a) * (exp 'a)
-
-and pexp 'a = 
- | Pat_aux of (pexp_aux 'a) * annot 'a
-
-and letbind_aux 'a =  (* Let binding *)
- | LB_val_explicit of typschm * (pat 'a) * (exp 'a) (* value binding, explicit type ((pat 'a) must be total) *)
- | LB_val_implicit of (pat 'a) * (exp 'a) (* value binding, implicit type ((pat 'a) must be total) *)
-
-and letbind 'a = 
- | LB_aux of (letbind_aux 'a) * annot 'a
-
-
-type reg_id 'a = 
- | RI_aux of (reg_id_aux 'a) * annot 'a
-
-
-type type_union_aux =  (* Type union constructors *)
- | Tu_id of id
- | Tu_ty_id of typ * id
-
-
-type name_scm_opt_aux =  (* Optional variable-naming-scheme specification for variables of defined type *)
+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
-
-
-type funcl_aux 'a =  (* Function clause *)
- | FCL_Funcl of id * (pat 'a) * (exp 'a)
-
-
-type rec_opt_aux =  (* Optional recursive annotation for functions *)
- | Rec_nonrec (* non-recursive *)
- | Rec_rec (* recursive *)
-
-
-type tannot_opt_aux =  (* Optional type annotation for functions *)
- | Typ_annot_opt_some of typquant * typ
-
-
-type alias_spec_aux 'a =  (* Register alias expression forms. Other than where noted, each id must refer to an unaliased register of type vector *)
- | AL_subreg of (reg_id 'a) * id
- | AL_bit of (reg_id 'a) * (exp 'a)
- | AL_slice of (reg_id 'a) * (exp 'a) * (exp 'a)
- | AL_concat of (reg_id 'a) * (reg_id 'a)
-
-
-type type_union = 
- | Tu_aux of type_union_aux * l
-
-
-type index_range_aux =  (* index specification, for bitfields in register types *)
- | BF_single of integer (* single index *)
- | BF_range of integer * integer (* index range *)
- | BF_concat of index_range * index_range (* concatenation of index ranges *)
-
-and index_range = 
- | BF_aux of index_range_aux * l
+type 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 effect_opt = 
- | Effect_opt_aux of effect_opt_aux * l
-
-
-type funcl 'a = 
- | FCL_aux of (funcl_aux 'a) * annot 'a
-
-
-type rec_opt = 
- | Rec_aux of rec_opt_aux * l
-
-
-type tannot_opt = 
- | Typ_annot_opt_aux of tannot_opt_aux * l
-
-
-type alias_spec 'a = 
- | AL_aux of (alias_spec_aux 'a) * annot 'a
-
-
-type default_spec_aux 'a =  (* Default kinding or typing assumption *)
- | DT_kind of base_kind * kid
- | DT_order of order
- | DT_typ of typschm * id
-
-
-type type_def_aux 'a =  (* Type definition body *)
- | TD_abbrev of id * name_scm_opt * typschm (* type abbreviation *)
- | TD_record of id * name_scm_opt * typquant * list (typ * id) * bool (* struct type definition *)
- | TD_variant of id * name_scm_opt * typquant * list type_union * bool (* union type definition *)
- | TD_enum of id * name_scm_opt * list id * bool (* enumeration type definition *)
- | TD_register of id * nexp * nexp * list (index_range * id) (* register mutable bitfield type definition *)
-
-
-type val_spec_aux 'a =  (* Value type specification *)
- | VS_val_spec of typschm * id
- | VS_extern_no_rename of typschm * id
- | VS_extern_spec of typschm * id * string (* Specify the type and id of a function from Lem, where the string must provide an explicit path to the required function but will not be checked *)
+type type_union = 
+ | Tu_aux of type_union_aux * l
 
 
-type kind_def_aux 'a =  (* Definition body for elements of kind; many are shorthands for type\_defs *)
- | KD_nabbrev of kind * id * name_scm_opt * nexp (* nexp abbreviation *)
+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 *)
@@ -468,71 +309,20 @@ type kind_def_aux 'a =  (* Definition body for elements of kind; many are shorth
  | KD_register of kind * id * nexp * nexp * list (index_range * id) (* register mutable bitfield type definition *)
 
 
-type scattered_def_aux 'a =  (* Function and type union definitions that can be spread across
-         a file. Each one must end in $id$ *)
- | SD_scattered_function of rec_opt * tannot_opt * effect_opt * id (* scattered function definition header *)
- | SD_scattered_funcl of (funcl 'a) (* scattered function definition clause *)
- | SD_scattered_variant of id * name_scm_opt * typquant (* scattered union definition header *)
- | SD_scattered_unioncl of id * type_union (* scattered union definition member *)
- | SD_scattered_end of id (* scattered definition end *)
-
-
-type fundef_aux 'a =  (* Function definition *)
- | FD_function of rec_opt * tannot_opt * effect_opt * list (funcl 'a)
-
-
-type dec_spec_aux 'a =  (* Register declarations *)
- | DEC_reg of typ * id
- | DEC_alias of id * (alias_spec 'a)
- | DEC_typ_alias of typ * id * (alias_spec 'a)
-
-
-type default_spec 'a = 
- | DT_aux of (default_spec_aux 'a) * l
-
-
-type type_def 'a = 
- | TD_aux of (type_def_aux 'a) * annot 'a
-
-
-type val_spec 'a = 
- | VS_aux of (val_spec_aux 'a) * annot 'a
+type 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 scattered_def 'a = 
- | SD_aux of (scattered_def_aux 'a) * annot 'a
-
-
-type fundef 'a = 
- | FD_aux of (fundef_aux 'a) * annot 'a
-
-
-type dec_spec 'a = 
- | DEC_aux of (dec_spec_aux 'a) * annot 'a
-
-
-type dec_comm 'a =  (* Top-level generated comments *)
- | DC_comm of string (* generated unstructured comment *)
- | DC_comm_struct of (def 'a) (* generated structured comment *)
-
-and def 'a =  (* Top-level definition *)
- | DEF_kind of (kind_def 'a) (* definition of named kind identifiers *)
- | DEF_type of (type_def 'a) (* type definition *)
- | DEF_fundef of (fundef 'a) (* function definition *)
- | DEF_val of (letbind 'a) (* value definition *)
- | DEF_spec of (val_spec 'a) (* top-level type constraint *)
- | DEF_default of (default_spec 'a) (* default kind and type assumptions *)
- | DEF_scattered of (scattered_def 'a) (* scattered function and type definition *)
- | DEF_reg_dec of (dec_spec 'a) (* register declaration *)
- | DEF_comm of (dec_comm 'a) (* generated comments *)
-
-
-type defs 'a =  (* Definition sequence *)
- | Defs of list (def 'a)
+type type_def 'a = 
+ | TD_aux of (type_def_aux 'a) * annot 'a
 
 
 let rec remove_one i l =
@@ -569,6 +359,24 @@ type ne =  (* internal numeric expressions *)
  | 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
@@ -578,15 +386,6 @@ type k =  (* Internal kinds *)
  | 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
@@ -597,22 +396,13 @@ type kinf =  (* Whether a kind is default or from a local binding *)
  | 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 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 *)
@@ -640,26 +430,26 @@ type conformsto =  (* how much conformance does overloading need *)
  | Conformsto_parm
 
 
+type widennum = 
+ | Widennum_widen
+ | Widennum_dont
+ | Widennum_dontcare
+
+
 type widenvec = 
  | Widenvec_widen
  | Widenvec_dont
  | Widenvec_dontcare
 
 
-type widennum = 
- | Widennum_widen
- | Widennum_dont
- | Widennum_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 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)))
@@ -705,10 +495,253 @@ let fresh_kid denv = Var "x" (*TODO When strings can be manipulated, this should
 
 
 
+type I = inf
+
+
 type E = env
 
 
-type I = inf
+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 *)
+ | E_id of id (* identifier *)
+ | E_lit of lit (* literal constant *)
+ | E_cast of typ * (exp 'a) (* cast *)
+ | E_app of id * list (exp 'a) (* function application *)
+ | E_app_infix of (exp 'a) * id * (exp 'a) (* infix function application *)
+ | E_tuple of list (exp 'a) (* tuple *)
+ | E_if of (exp 'a) * (exp 'a) * (exp 'a) (* conditional *)
+ | E_for of id * (exp 'a) * (exp 'a) * (exp 'a) * order * (exp 'a) (* loop *)
+ | E_vector of list (exp 'a) (* vector (indexed from 0) *)
+ | E_vector_indexed of list (integer * (exp 'a)) * (opt_default 'a) (* vector (indexed consecutively) *)
+ | E_vector_access of (exp 'a) * (exp 'a) (* vector access *)
+ | E_vector_subrange of (exp 'a) * (exp 'a) * (exp 'a) (* subvector extraction *)
+ | E_vector_update of (exp 'a) * (exp 'a) * (exp 'a) (* vector functional update *)
+ | E_vector_update_subrange of (exp 'a) * (exp 'a) * (exp 'a) * (exp 'a) (* vector subrange update, with vector *)
+ | E_vector_append of (exp 'a) * (exp 'a) (* vector concatenation *)
+ | E_list of list (exp 'a) (* list *)
+ | E_cons of (exp 'a) * (exp 'a) (* cons *)
+ | E_record of (fexps 'a) (* struct *)
+ | E_record_update of (exp 'a) * (fexps 'a) (* functional update of struct *)
+ | E_field of (exp 'a) * id (* field projection from struct *)
+ | E_case of (exp 'a) * list (pexp 'a) (* pattern matching *)
+ | E_let of (letbind 'a) * (exp 'a) (* let expression *)
+ | E_assign of (lexp 'a) * (exp 'a) (* imperative assignment *)
+ | E_sizeof of nexp (* the value of nexp at run time *)
+ | E_return of (exp 'a) (* return (exp 'a) from current function *)
+ | E_exit of (exp 'a) (* halt all current execution *)
+ | E_assert of (exp 'a) * (exp 'a) (* halt with error (exp 'a) when not (exp 'a) *)
+ | E_internal_cast of annot 'a * (exp 'a) (* This is an internal cast, generated during type checking that will resolve into a syntactic cast after *)
+ | E_internal_exp of annot 'a (* This is an internal use for passing nexp information  to library functions, postponed for constraint solving *)
+ | E_sizeof_internal of annot 'a (* For sizeof during type checking, to replace nexp with internal n *)
+ | E_internal_exp_user of annot 'a * annot 'a (* This is like the above but the user has specified an implicit parameter for the current function *)
+ | E_comment of string (* For generated unstructured comments *)
+ | E_comment_struc of (exp 'a) (* For generated structured comments *)
+ | E_internal_let of (lexp 'a) * (exp 'a) * (exp 'a) (* This is an internal node for compilation that demonstrates the scope of a local mutable variable *)
+ | E_internal_plet of (pat 'a) * (exp 'a) * (exp 'a) (* This is an internal node, used to distinguised some introduced lets during processing from original ones *)
+ | E_internal_return of (exp 'a) (* For internal use to embed into monad definition *)
+ | 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 *)
+ | LEXP_cast of typ * id (* cast *)
+ | LEXP_tup of list (lexp 'a) (* multiple (non-memory) assignment *)
+ | LEXP_vector of (lexp 'a) * (exp 'a) (* vector element *)
+ | LEXP_vector_range of (lexp 'a) * (exp 'a) * (exp 'a) (* subvector *)
+ | LEXP_field of (lexp 'a) * id (* struct field *)
+
+and lexp 'a = 
+ | LEXP_aux of (lexp_aux 'a) * annot 'a
+
+and fexp_aux 'a =  (* field expression *)
+ | FE_Fexp of id * (exp 'a)
+
+and fexp 'a = 
+ | FE_aux of (fexp_aux 'a) * annot 'a
+
+and fexps_aux 'a =  (* field expression list *)
+ | FES_Fexps of list (fexp 'a) * bool
+
+and fexps 'a = 
+ | FES_aux of (fexps_aux 'a) * annot 'a
+
+and opt_default_aux 'a =  (* optional default value for indexed vector expressions *)
+ | Def_val_empty
+ | Def_val_dec of (exp 'a)
+
+and opt_default 'a = 
+ | Def_val_aux of (opt_default_aux 'a) * annot 'a
+
+and pexp_aux 'a =  (* pattern match *)
+ | Pat_exp of (pat 'a) * (exp 'a)
+
+and pexp 'a = 
+ | Pat_aux of (pexp_aux 'a) * annot 'a
+
+and letbind_aux 'a =  (* let binding *)
+ | LB_val_explicit of typschm * (pat 'a) * (exp 'a) (* let, explicit type ((pat 'a) must be total) *)
+ | LB_val_implicit of (pat 'a) * (exp 'a) (* let, implicit type ((pat 'a) must be total) *)
+
+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)
+
+and alias_spec 'a = 
+ | AL_aux of (alias_spec_aux 'a) * annot 'a
+
+
+type funcl_aux 'a =  (* function clause *)
+ | FCL_Funcl of id * (pat 'a) * (exp 'a)
+
+
+type rec_opt_aux =  (* optional recursive annotation for functions *)
+ | Rec_nonrec (* non-recursive *)
+ | Rec_rec (* recursive *)
+
+
+type tannot_opt_aux =  (* optional type annotation for functions *)
+ | Typ_annot_opt_some of typquant * typ
+
+
+type effect_opt_aux =  (* optional effect annotation for functions *)
+ | Effect_opt_pure (* sugar for empty effect set *)
+ | Effect_opt_effect of effect
+
+
+type funcl 'a = 
+ | FCL_aux of (funcl_aux 'a) * annot 'a
+
+
+type rec_opt = 
+ | Rec_aux of rec_opt_aux * l
+
+
+type tannot_opt = 
+ | Typ_annot_opt_aux of tannot_opt_aux * l
+
+
+type effect_opt = 
+ | Effect_opt_aux of effect_opt_aux * l
+
+
+type val_spec_aux 'a =  (* value type specification *)
+ | VS_val_spec of typschm * id (* specify the type of an upcoming definition *)
+ | VS_extern_no_rename of typschm * id (* specify the type of an external function *)
+ | VS_extern_spec of typschm * id * string (* specify the type of a function from Lem *)
+
+
+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 *)
+ | SD_scattered_function of rec_opt * tannot_opt * effect_opt * id (* scattered function definition header *)
+ | SD_scattered_funcl of (funcl 'a) (* scattered function definition clause *)
+ | SD_scattered_variant of id * name_scm_opt * typquant (* scattered union definition header *)
+ | SD_scattered_unioncl of id * type_union (* scattered union definition member *)
+ | SD_scattered_end of id (* scattered definition end *)
+
+
+type 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 *)
+ | DEC_reg of typ * id
+ | DEC_alias of id * (alias_spec 'a)
+ | DEC_typ_alias of typ * id * (alias_spec 'a)
+
+
+type val_spec 'a = 
+ | VS_aux of (val_spec_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 default_spec 'a = 
+ | DT_aux of (default_spec_aux 'a) * l
+
+
+type dec_spec 'a = 
+ | DEC_aux of (dec_spec_aux 'a) * annot 'a
+
+
+type dec_comm 'a =  (* top-level generated comments *)
+ | DC_comm of string (* generated unstructured comment *)
+ | DC_comm_struct of (def 'a) (* generated structured comment *)
+
+and def 'a =  (* top-level definition *)
+ | DEF_kind of (kind_def 'a) (* definition of named kind identifiers *)
+ | DEF_type of (type_def 'a) (* type definition *)
+ | DEF_fundef of (fundef 'a) (* function definition *)
+ | DEF_val of (letbind 'a) (* value definition *)
+ | DEF_spec of (val_spec 'a) (* top-level type constraint *)
+ | DEF_default of (default_spec 'a) (* default kind and type assumptions *)
+ | DEF_scattered of (scattered_def 'a) (* scattered function and type definition *)
+ | DEF_reg_dec of (dec_spec 'a) (* register declaration *)
+ | DEF_comm of (dec_comm 'a) (* generated comments *)
+
+
+type defs 'a =  (* definition sequence *)
+ | Defs of list (def 'a)