Add type annotations to lem grammar, including printing out the annotated ast, and extending the interpreter to expect annotations.

Annotations and locations are still not used by the interpreter.

6 files changed, 741 insertions, 459 deletions

diff --git a/language/Makefile b/language/Makefile
index d650f957..2076069c 100644
--- a/language/Makefile
+++ b/language/Makefile
@@ -9,7 +9,7 @@ all: l2.pdf l2_parse.pdf l2.ml l2_parse.ml l2.lem
 %Theory.uo: %Script.sml
 	Holmake --qof -I $(OTTLIB) $@
 
-l2.tex: l2.ott l2_rules.ott
+l2.tex: l2.ott l2_typ.ott l2_rules.ott
 	ott -sort false -generate_aux_rules false -o $@ -picky_multiple_parses true $^
 
 %.tex: %.ott
@@ -21,12 +21,8 @@ l2.tex: l2.ott l2_rules.ott
 %Script.sml: %.ott
 	ott -sort false -generate_aux_rules true -o $@ -picky_multiple_parses true $^
 
-%.lem: %.ott
-	# work around what is probably a bug in -generate_aux_rules true: when we try to generate Lem code with
-	# that turned on, we get some surprising-looking parse failures in a
-	# few rules.  Likely we're not doing the proper transform for rules
-	# generated from inductive relation syntax.
-	ott -sort false -generate_aux_rules false -o $@ -picky_multiple_parses true $^
+l2.lem: l2.ott l2_typ.ott
+	ott -sort false -generate_aux_rules true -o $@ -picky_multiple_parses true $^
 
 clean:
 	rm -rf *~
diff --git a/language/l2.lem b/language/l2.lem
index 630c976d..30027846 100644
--- a/language/l2.lem
+++ b/language/l2.lem
@@ -1,4 +1,4 @@
-(* generated by Ott 0.23 from: l2.ott *)
+(* generated by Ott 0.24 from: l2_typ.ott l2.ott *)
 open import Pervasives
 
 open import Map
@@ -8,7 +8,9 @@ open import Set_extra
 type l =
   | Unknown
   | Trans of string * maybe l
-  | Range of nat * nat
+  | Range of string * nat * nat * nat * nat
+
+type annot 'a = l * 'a
 
 val duplicates : forall 'a. list 'a -> list 'a
 
@@ -20,30 +22,45 @@ val subst : forall 'a. list 'a -> list 'a -> bool
 type x = string (* identifier *)
 type ix = string (* infix identifier *)
 
-type kid =  (* variables with kind, ticked to differntiate from program variables *)
- | Var of x
-
-
-type base_kind =  (* base kind *)
+type base_kind_aux =  (* base kind *)
  | BK_type (* kind of types *)
  | BK_nat (* kind of natural number size expressions *)
  | BK_order (* kind of vector order specifications *)
  | BK_effect (* kind of effect sets *)
 
 
-type nexp =  (* expression of kind Nat, for vector sizes and origins *)
+type base_kind = 
+ | BK_aux of base_kind_aux * l
+
+
+type kid_aux =  (* variables with kind, ticked to differntiate from program variables *)
+ | Var of x
+
+
+type kind_aux =  (* kinds *)
+ | K_kind of list base_kind
+
+
+type kid = 
+ | Kid_aux of kid_aux * l
+
+
+type kind = 
+ | K_aux of kind_aux * l
+
+
+type nexp_aux =  (* expression of kind Nat, for vector sizes and origins *)
  | Nexp_var of kid (* variable *)
  | Nexp_constant of natural (* constant *)
  | Nexp_times of nexp * nexp (* product *)
  | Nexp_sum of nexp * nexp (* sum *)
  | Nexp_exp of nexp (* exponential *)
 
-
-type kind =  (* kinds *)
- | K_kind of list base_kind
+and nexp = 
+ | Nexp_aux of nexp_aux * l
 
 
-type base_effect =  (* effect *)
+type base_effect_aux =  (* effect *)
  | BE_rreg (* read register *)
  | BE_wreg (* write register *)
  | BE_rmem (* read memory *)
@@ -53,45 +70,78 @@ type base_effect =  (* effect *)
  | BE_nondet (* nondeterminism from intra-instruction parallelism *)
 
 
-type order =  (* vector order specifications, of kind Order *)
+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 *)
+
+
+type order_aux =  (* vector order specifications, of kind Order *)
  | Ord_var of kid (* variable *)
  | Ord_inc (* increasing (little-endian) *)
  | Ord_dec (* decreasing (big-endian) *)
 
 
-type effect =  (* effect set, of kind Effects *)
- | Effect_var of kid
- | Effect_set of list base_effect (* effect set *)
+type id = 
+ | Id_aux of id_aux * l
 
 
-type id =  (* Identifier *)
- | Id of x
- | DeIid of x (* remove infix status *)
+type effect = 
+ | Effect_aux of effect_aux * l
+
+
+type order = 
+ | Ord_aux of order_aux * l
 
 let effect_union e1 e2 = 
   match (e1,e2) with
-  | (Effect_set els,Effect_set els2) -> Effect_set (els++els2)
+  | ((Effect_aux (Effect_set els) _),(Effect_aux (Effect_set els2) l)) -> Effect_aux (Effect_set (els++els2)) l
   end
 
 
-type n_constraint =  (* constraint over kind $Nat$ *)
+type kinded_id_aux =  (* optionally kind-annotated identifier *)
+ | KOpt_none of kid (* identifier *)
+ | KOpt_kind of kind * kid (* kind-annotated variable *)
+
+
+type n_constraint_aux =  (* constraint over kind $Nat$ *)
  | NC_fixed of nexp * nexp
  | NC_bounded_ge of nexp * nexp
  | NC_bounded_le of nexp * nexp
  | NC_nat_set_bounded of kid * list natural
 
 
-type kinded_id =  (* optionally kind-annotated identifier *)
- | KOpt_none of kid (* identifier *)
- | KOpt_kind of kind * kid (* kind-annotated variable *)
+type kinded_id = 
+ | KOpt_aux of kinded_id_aux * l
+
+
+type n_constraint = 
+ | NC_aux of n_constraint_aux * l
 
 
-type quant_item =  (* Either a kinded identifier or a nexp constraint for a typquant *)
+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 lit =  (* Literal constant *)
+type quant_item = 
+ | QI_aux of quant_item_aux * l
+
+
+type typquant_aux =  (* type quantifiers and constraints *)
+ | TypQ_tq of list quant_item
+ | TypQ_no_forall (* sugar, omitting quantifier and constraints *)
+
+
+type lit_aux =  (* Literal constant *)
  | L_unit (* $() : unit$ *)
  | L_zero (* $bitzero : bit$ *)
  | L_one (* $bitone : bit$ *)
@@ -104,7 +154,7 @@ type lit =  (* Literal constant *)
  | L_string of string (* string constant *)
 
 
-type typ =  (* Type expressions, of kind $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 *)
@@ -112,164 +162,390 @@ type typ =  (* Type expressions, of kind $Type$ *)
  | Typ_tup of list typ (* Tuple type *)
  | Typ_app of id * list typ_arg (* type constructor application *)
 
-and typ_arg =  (* Type constructor arguments of all kinds *)
+and typ = 
+ | Typ_aux of typ_aux * l
+
+and typ_arg_aux =  (* Type constructor arguments of all kinds *)
  | Typ_arg_nexp of nexp
  | Typ_arg_typ of typ
  | Typ_arg_order of order
  | Typ_arg_effect of effect
 
+and typ_arg = 
+ | Typ_arg_aux of typ_arg_aux * l
 
-type typquant =  (* type quantifiers and constraints *)
- | TypQ_tq of list quant_item
- | TypQ_no_forall (* sugar, omitting quantifier and constraints *)
+
+type typquant = 
+ | TypQ_aux of typquant_aux * l
+
+
+type lit = 
+ | L_aux of lit_aux * l
 
 
-type pat =  (* Pattern *)
+type typschm_aux =  (* type scheme *)
+ | TypSchm_ts of typquant * typ
+
+
+type pat_aux 'a =  (* Pattern *)
  | P_lit of lit (* literal constant pattern *)
  | P_wild (* wildcard *)
- | P_as of pat * id (* named pattern *)
- | P_typ of typ * pat (* typed pattern *)
+ | P_as of (pat 'a) * id (* named pattern *)
+ | P_typ of typ * (pat 'a) (* typed pattern *)
  | P_id of id (* identifier *)
- | P_app of id * list pat (* union constructor pattern *)
- | P_record of list fpat * bool (* struct pattern *)
- | P_vector of list pat (* vector pattern *)
- | P_vector_indexed of list (natural * pat) (* vector pattern (with explicit indices) *)
- | P_vector_concat of list pat (* concatenated vector pattern *)
- | P_tup of list pat (* tuple pattern *)
- | P_list of list pat (* list pattern *)
+ | P_app of id * list (pat 'a) (* union constructor pattern *)
+ | P_record of list (fpat 'a) * bool (* struct pattern *)
+ | P_vector of list (pat 'a) (* vector pattern *)
+ | P_vector_indexed of list (natural * (pat 'a)) (* vector pattern (with explicit indices) *)
+ | P_vector_concat of list (pat 'a) (* concatenated vector pattern *)
+ | P_tup of list (pat 'a) (* tuple pattern *)
+ | P_list of list (pat 'a) (* list pattern *)
 
-and fpat =  (* Field pattern *)
- | FP_Fpat of id * pat
+and pat 'a = 
+ | P_aux of (pat_aux 'a) * annot 'a
 
+and fpat_aux 'a =  (* Field pattern *)
+ | FP_Fpat of id * (pat 'a)
 
-type typschm =  (* type scheme *)
- | TypSchm_ts of typquant * typ
+and fpat 'a = 
+ | FP_aux of (fpat_aux 'a) * annot 'a
 
 
-type exp =  (* Expression *)
- | E_block of list exp (* block (parsing conflict with structs?) *)
+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 *)
  | E_lit of lit (* literal constant *)
- | E_cast of typ * exp (* cast *)
- | E_app of id * list exp (* function application *)
- | E_app_infix of exp * id * exp (* infix function application *)
- | E_tuple of list exp (* tuple *)
- | E_if of exp * exp * exp (* conditional *)
- | E_for of id * exp * exp * exp * order * exp (* loop *)
- | E_vector of list exp (* vector (indexed from 0) *)
- | E_vector_indexed of list (natural * exp) (* vector (indexed consecutively) *)
- | E_vector_access of exp * exp (* vector access *)
- | E_vector_subrange of exp * exp * exp (* subvector extraction *)
- | E_vector_update of exp * exp * exp (* vector functional update *)
- | E_vector_update_subrange of exp * exp * exp * exp (* vector subrange update (with vector) *)
- | E_list of list exp (* list *)
- | E_cons of exp * exp (* cons *)
- | E_record of fexps (* struct *)
- | E_record_update of exp * fexps (* functional update of struct *)
- | E_field of exp * id (* field projection from struct *)
- | E_case of exp * list pexp (* pattern matching *)
- | E_let of letbind * exp (* let expression *)
- | E_assign of lexp * exp (* imperative assignment *)
-
-and lexp =  (* lvalue expression *)
+ | 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 (natural * (exp '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_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 *)
+
+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 (* memory write via function call *)
- | LEXP_vector of lexp * exp (* vector element *)
- | LEXP_vector_range of lexp * exp * exp (* subvector *)
- | LEXP_field of lexp * id (* struct field *)
+ | LEXP_memory of id * list (exp 'a) (* memory write via function call *)
+ | 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 fexp =  (* Field-expression *)
- | FE_Fexp of id * exp
+and lexp 'a = 
+ | LEXP_aux of (lexp_aux 'a) * annot 'a
 
-and fexps =  (* Field-expression list *)
- | FES_Fexps of list fexp * bool
+and fexp_aux 'a =  (* Field-expression *)
+ | FE_Fexp of id * (exp 'a)
 
-and pexp =  (* Pattern match *)
- | Pat_exp of pat * exp
+and fexp 'a = 
+ | FE_aux of (fexp_aux 'a) * annot 'a
 
-and letbind =  (* Let binding *)
- | LB_val_explicit of typschm * pat * exp (* value binding, explicit type (pat must be total) *)
- | LB_val_implicit of pat * exp (* value binding, implicit type (pat must be total) *)
+and fexps_aux 'a =  (* Field-expression list *)
+ | FES_Fexps of list (fexp 'a) * bool
 
+and fexps 'a = 
+ | FES_aux of (fexps_aux 'a) * annot 'a
 
-type type_union =  (* Type union constructors *)
- | Tu_id of id
- | Tu_ty_id of typ * id
+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) *)
 
-type funcl =  (* Function clause *)
- | FCL_Funcl of id * pat * exp
+and letbind 'a = 
+ | LB_aux of (letbind_aux 'a) * annot 'a
 
 
-type effect_opt =  (* Optional effect annotation for functions *)
+type effect_opt_aux =  (* Optional effect annotation for functions *)
  | Effect_opt_pure (* sugar for empty effect set *)
  | Effect_opt_effect of effect
 
 
-type name_scm_opt =  (* Optional variable-naming-scheme specification for variables of defined type *)
+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 rec_opt =  (* Optional recursive annotation for functions *)
- | Rec_nonrec (* non-recursive *)
- | Rec_rec (* recursive *)
+type type_union_aux =  (* Type union constructors *)
+ | Tu_id of id
+ | Tu_ty_id of typ * id
 
 
-type tannot_opt =  (* Optional type annotation for functions *)
+type tannot_opt_aux =  (* Optional type annotation for functions *)
  | Typ_annot_opt_some of typquant * typ
 
 
-type index_range =  (* index specification, for bitfields in register types *)
+type effect_opt = 
+ | Effect_opt_aux of effect_opt_aux * l
+
+
+type rec_opt = 
+ | Rec_aux of rec_opt_aux * l
+
+
+type funcl 'a = 
+ | FCL_aux of (funcl_aux 'a) * annot 'a
+
+
+type name_scm_opt = 
+ | Name_sect_aux of name_scm_opt_aux * l
+
+
+type type_union = 
+ | Tu_aux of type_union_aux * l
+
+
+type tannot_opt = 
+ | Typ_annot_opt_aux of tannot_opt_aux * l
+
+
+type index_range_aux =  (* index specification, for bitfields in register types *)
  | BF_single of natural (* single index *)
  | BF_range of natural * natural (* index range *)
  | BF_concat of index_range * index_range (* concatenation of index ranges *)
 
-
-type val_spec =  (* 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 *)
+and index_range = 
+ | BF_aux of index_range_aux * l
 
 
-type scattered_def =  (* Function and type union definitions that can be spread across
+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 (* scattered function definition clause *)
+ | 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 =  (* Function definition *)
- | FD_function of rec_opt * tannot_opt * effect_opt * list funcl
+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 fundef_aux 'a =  (* Function definition *)
+ | FD_function of rec_opt * tannot_opt * effect_opt * list (funcl 'a)
 
 
-type default_spec =  (* Default kinding or typing assumption *)
+type default_spec_aux 'a =  (* Default kinding or typing assumption *)
  | DT_kind of base_kind * kid
  | DT_typ of typschm * id
 
 
-type type_def =  (* 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 def =  (* Top-level definition *)
- | DEF_type of type_def (* type definition *)
- | DEF_fundef of fundef (* function definition *)
- | DEF_val of letbind (* value definition *)
- | DEF_spec of val_spec (* top-level type constraint *)
- | DEF_default of default_spec (* default kind and type assumptions *)
- | DEF_scattered of scattered_def (* scattered function and type definition *)
+type type_def 'a = 
+ | TD_aux of (type_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) * annot 'a
+
+
+type val_spec 'a = 
+ | VS_aux of (val_spec_aux 'a) * annot 'a
+
+
+type def_aux 'a =  (* Top-level definition *)
+ | 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 typ * id (* register declaration *)
 
 
-type defs =  (* Definition sequence *)
- | Defs of list def
+type def 'a = 
+ | DEF_aux of (def_aux 'a) * annot 'a
+
+
+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 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 ne =  (* internal numeric expressions *)
+ | Ne_var of kid
+ | Ne_const of natural
+ | Ne_mult of ne * ne
+ | Ne_add of list ne
+ | Ne_exp of ne
+ | Ne_unary of ne
+
+
+type kinf =  (* Whether a kind is default or from a local binding *)
+ | Kinf_k of k
+ | Kinf_def of k
+
+
+type tid =  (* A type identifier or type variable *)
+ | Tid_id of id
+ | 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 kid * list natural
+
+
+type tag =  (* Data indicating where the identifier arises and thus information necessary in compilation *)
+ | Tag_empty
+ | 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
+
+
+type t =  (* Internal types *)
+ | T_id of id
+ | T_var of kid
+ | T_fn of t * t * effect
+ | T_tup of list t
+ | T_app of id * t_args
+
+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 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 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
 
 
 
diff --git a/language/l2.ml b/language/l2.ml
index b01a25ac..1c2a6c09 100644
--- a/language/l2.ml
+++ b/language/l2.ml
@@ -1,4 +1,4 @@
-(* generated by Ott 0.23 from: l2.ott *)
+(* generated by Ott 0.24 from: l2.ott *)
 
 
 type text = string
@@ -294,13 +294,13 @@ and 'a lexp_aux =  (* lvalue expression *)
 
 
 type 
-'a effect_opt_aux =  (* Optional effect annotation for functions *)
+effect_opt_aux =  (* Optional effect annotation for functions *)
    Effect_opt_pure (* sugar for empty effect set *)
  | Effect_opt_effect of effect
 
 
 type 
-'a tannot_opt_aux =  (* Optional type annotation for functions *)
+tannot_opt_aux =  (* Optional type annotation for functions *)
    Typ_annot_opt_some of typquant * typ
 
 
@@ -328,13 +328,13 @@ type_union_aux =  (* Type union constructors *)
 
 
 type 
-'a effect_opt = 
-   Effect_opt_aux of 'a effect_opt_aux * 'a annot
+effect_opt = 
+   Effect_opt_aux of effect_opt_aux * l
 
 
 type 
-'a tannot_opt = 
-   Typ_annot_opt_aux of 'a tannot_opt_aux * 'a annot
+tannot_opt = 
+   Typ_annot_opt_aux of tannot_opt_aux * l
 
 
 type 
@@ -369,13 +369,13 @@ and index_range =
 
 type 
 'a fundef_aux =  (* Function definition *)
-   FD_function of rec_opt * 'a tannot_opt * 'a effect_opt * ('a funcl) list
+   FD_function of rec_opt * tannot_opt * effect_opt * ('a funcl) list
 
 
 type 
 'a scattered_def_aux =  (* Function and type union definitions that can be spread across
          a file. Each one must end in $_$ *)
-   SD_scattered_function of rec_opt * 'a tannot_opt * 'a effect_opt * id (* scattered function definition header *)
+   SD_scattered_function of rec_opt * tannot_opt * effect_opt * id (* scattered function definition header *)
  | SD_scattered_funcl of 'a funcl (* scattered function definition clause *)
  | SD_scattered_variant of id * name_scm_opt * typquant (* scattered union definition header *)
  | SD_scattered_unioncl of id * type_union (* scattered union definition member *)
diff --git a/language/l2.ott b/language/l2.ott
index b6a1396f..aa981cc7 100644
--- a/language/l2.ott
+++ b/language/l2.ott
@@ -58,7 +58,9 @@ open import Set_extra
 type l =
   | Unknown
   | Trans of string * maybe l
-  | Range of nat * nat
+  | Range of string * nat * nat * nat * nat
+
+type annot 'a = l * 'a
 
 val duplicates : forall 'a. list 'a -> list 'a
 
@@ -102,7 +104,7 @@ l :: '' ::=                                     {{ phantom }}
 annot :: '' ::=
                                                 {{ phantom }}
                                                 {{ ocaml 'a annot }}
-                                                {{ lem annot }}
+                                                {{ lem annot 'a }}
                                                 {{ hol unit }}
 
 id :: '' ::=
@@ -195,13 +197,13 @@ effect :: 'Effect_' ::=
  | pure                                 :: M :: pure {{ com sugar for empty effect set }} 
    {{ lem (Effect_set [])  }} {{icho [[{}]] }}
  | effect1 u+ .. u+ effectn                   :: M :: union {{ com meta operation for combining sets of effects }} {{ icho [] }}
-   {{ lem (List.foldr effect_union (Effect_set []) [[effect1..effectn]]) }}
+   {{ lem (List.foldr effect_union (Effect_aux (Effect_set []) Unknown) [[effect1..effectn]]) }}
 
 embed
 {{ lem
 let effect_union e1 e2 = 
   match (e1,e2) with
-  | (Effect_set els,Effect_set els2) -> Effect_set (els++els2)
+  | ((Effect_aux (Effect_set els) _),(Effect_aux (Effect_set els2) l)) -> Effect_aux (Effect_set (els++els2)) l
   end
 }}
 
@@ -727,7 +729,7 @@ grammar
 
 tannot_opt :: 'Typ_annot_opt_' ::=
   {{ com Optional type annotation for functions}}
-  {{ aux _ annot }} {{ auxparam 'a }}
+  {{ aux _ l }} 
 %  |                                             :: :: none
 % Currently not optional; one issue, do the type parameters apply over the argument types, or should this be the type of the function and not just the return
   | typquant typ                                :: :: some 
@@ -740,7 +742,7 @@ rec_opt :: 'Rec_' ::=
 
 effect_opt :: 'Effect_opt_' ::=
   {{ com Optional effect annotation for functions }}
-  {{ aux _ annot }} {{ auxparam 'a }}
+  {{ aux _ l }}
   |                                             :: :: pure {{ com sugar for empty effect set }}
   | effectkw effect                              :: :: effect
 
diff --git a/language/l2_rules.ott b/language/l2_rules.ott
index 7e3efcb7..3bade9d4 100644
--- a/language/l2_rules.ott
+++ b/language/l2_rules.ott
@@ -1,323 +1,5 @@
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-% 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 }}
-   | K_Abbrev t                                        :: :: abbrev {{ com Not really a kind, but a convenient way of tracking type abbreviations }}
-
-t , u :: 'T_' ::=                                
-{{ com Internal types }}
-   | id                                           :: :: id
-   | kid                                          :: :: var
-   | t1 -> t2 effect tag S_N                      :: :: fn  {{ com [[S_N]] are constraints for the function, [[tag]] holds generation data }}
-   | ( t1 * .... * tn )                           :: :: tup
-   | id t_args                                    :: :: app 
-   | register t_args                              :: :: reg_app
-   | t [ t1 / id1 ... tn / idn ]		  :: :: subst
-
-tag :: 'Tag_' ::=                                 
-{{ com Data indicating where the identifier arises and thus information necessary in compilation }}
-   | None                                 :: :: empty 
-   | Ctor                                 :: :: ctor {{ com Data constructor from a type union }}
-   | Extern                               :: :: 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 }}
-   | _                                    :: :: dontcare 
-
-ne :: 'Ne_' ::=
- {{ com internal numeric expressions }}
-   | kid                                 :: :: var
-   | num                                 :: :: const
-   | ne1 * ne2                           :: :: mult
-   | ne1 + ... + nen                     :: :: add
-   | 2 ** ne				 :: :: exp
-   | ( - ne )                            :: :: unary
-   | zero   				 :: M :: zero
-     {{ lem (Ne_const 0) }}
-   | bitlength ( bin )                   :: M :: cbin
-     {{ ocaml (asssert false) }}
-     {{ hol ARB }}
-     {{ lem (blength [[bin]]) }}
-   | bitlength ( hex )                   :: M :: chex
-     {{ ocaml (assert false) }}
-     {{ hol ARB }}
-     {{ lem (hlength [[hex]]) }}
-   | 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
-
- 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
-   | kid 'IN' { num1 , ... , numn } :: :: in
-
-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 records, enumerations, and kinds }}
- | < E_k , 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                                                             
-
- 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]]) }} 
-   | ( 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- E_t1 .. E_tn                                            :: 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 [[E_t1..E_tn]]))))) }} 
-     {{ 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+ .. u+ In                                               :: :: Iunion {{ com Unions the constraints and effect }}
-    {{ lem (List.foldr inf_union Iemp [[I1..In]]) }}
-
-
 formula :: formula_ ::=
   | judgement                                                   :: :: judgement
 
diff --git a/language/l2_typ.ott b/language/l2_typ.ott
new file mode 100644
index 00000000..43a3ea17
--- /dev/null
+++ b/language/l2_typ.ott
@@ -0,0 +1,326 @@
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% 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 }}
+   | id                                            :: :: id
+   | kid                                          :: :: var
+   | t1 -> t2 effect                        :: :: fn 
+   | ( t1 * .... * tn )                          :: :: tup
+   | id t_args                                  :: :: app 
+   | register t_args                         :: S :: reg_app {{ ichlo T_app "register" [[t_args]] }}
+   | t [ t1 / id1 ... tn / idn ]            :: 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 
+   | 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				  :: :: enum
+
+ne :: 'Ne_' ::=
+ {{ com internal numeric expressions }}
+   | kid                                 :: :: var
+   | num                                 :: :: const
+   | ne1 * ne2                           :: :: mult
+   | ne1 + ... + nen                     :: :: add
+   | 2 ** ne				 :: :: exp
+   | ( - ne )                            :: :: unary
+   | zero   				 :: S :: zero
+     {{ lem (Ne_const 0) }}
+   | bitlength ( bin )                   :: M :: cbin
+     {{ ocaml (asssert false) }}
+     {{ hol ARB }}
+     {{ lem (blength [[bin]]) }}
+   | bitlength ( hex )                   :: M :: chex
+     {{ ocaml (assert false) }}
+     {{ hol ARB }}
+     {{ lem (hlength [[hex]]) }}
+   | 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
+
+ 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
+   | kid 'IN' { num1 , ... , numn } :: :: in
+
+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 records, enumerations, and kinds }}
+ | < E_k , 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                                                             
+
+ 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]]) }} 
+   | ( 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- E_t1 .. E_tn                                            :: 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 [[E_t1..E_tn]]))))) }} 
+     {{ 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+ .. u+ In                                               :: :: Iunion {{ com Unions the constraints and effect }}
+    {{ lem (List.foldr inf_union Iemp [[I1..In]]) }}
+