Typeing rules for patterns and easy expressions

4 files changed, 419 insertions, 570 deletions

diff --git a/language/l2.lem b/language/l2.lem
index 51bad620..90974dfc 100644
--- a/language/l2.lem
+++ b/language/l2.lem
@@ -32,20 +32,16 @@ val subst : forall 'a. list 'a -> list 'a -> bool
 type x = string (* identifier *)
 type ix = string (* infix identifier *)
 
-type base_kind =  (* base kind *)
- | BK_type (* kind of types *)
- | BK_nat (* kind of natural number size expressions *)
- | BK_order (* kind of vector order specifications *)
- | BK_effects (* kind of effect sets *)
-
-
 type id =  (* Identifier *)
  | Id of x
  | DeIid of x (* remove infix status *)
 
 
-type kind =  (* kinds *)
- | K_kind of list base_kind
+type base_kind =  (* base kind *)
+ | BK_type (* kind of types *)
+ | BK_nat (* kind of natural number size expressions *)
+ | BK_order (* kind of vector order specifications *)
+ | BK_effects (* kind of effect sets *)
 
 
 type nexp =  (* expression of kind $Nat$, for vector sizes and origins *)
@@ -56,6 +52,10 @@ type nexp =  (* expression of kind $Nat$, for vector sizes and origins *)
  | Nexp_exp of nexp (* exponential *)
 
 
+type kind =  (* kinds *)
+ | K_kind of list base_kind
+
+
 type efct =  (* effect *)
  | Effect_rreg (* read register *)
  | Effect_wreg (* write register *)
@@ -66,11 +66,6 @@ type efct =  (* effect *)
  | Effect_nondet (* nondeterminism from intra-instruction parallelism *)
 
 
-type kinded_id =  (* optionally kind-annotated identifier *)
- | KOpt_none of id (* identifier *)
- | KOpt_kind of kind * id (* kind-annotated variable *)
-
-
 type nexp_constraint =  (* constraint over kind $Nat$ *)
  | NC_fixed of nexp * nexp
  | NC_bounded_ge of nexp * nexp
@@ -78,6 +73,11 @@ type nexp_constraint =  (* constraint over kind $Nat$ *)
  | NC_nat_set_bounded of id * list num
 
 
+type kinded_id =  (* optionally kind-annotated identifier *)
+ | KOpt_none of id (* identifier *)
+ | KOpt_kind of kind * id (* kind-annotated variable *)
+
+
 type order =  (* vector order specifications, of kind $Order$ *)
  | Ord_id of id (* identifier *)
  | Ord_inc (* increasing (little-endian) *)
@@ -94,6 +94,15 @@ type quant_item =  (* Either a kinded identifier or a nexp constraint for a typq
  | QI_const of nexp_constraint (* A constraint for this type *)
 
 
+type ne =  (* internal numeric expressions *)
+ | Ne_var of id
+ | Ne_const of num
+ | Ne_mult of ne * ne
+ | Ne_add of list ne
+ | Ne_exp of ne
+ | Ne_unary of ne
+
+
 type typ =  (* Type expressions, of kind $Type$ *)
  | Typ_wild (* Unspecified type *)
  | Typ_var of id (* Type variable *)
@@ -108,6 +117,11 @@ and typ_arg =  (* Type constructor arguments of all kinds *)
  | Typ_arg_effects of effects
 
 
+type typquant =  (* type quantifiers and constraints *)
+ | TypQ_tq of list quant_item
+ | TypQ_no_forall (* sugar, omitting quantifier and constraints *)
+
+
 type lit =  (* Literal constant *)
  | L_unit (* $() : unit$ *)
  | L_zero (* $bitzero : bit$ *)
@@ -121,9 +135,14 @@ type lit =  (* Literal constant *)
  | L_string of string (* string constant *)
 
 
-type typquant =  (* type quantifiers and constraints *)
- | TypQ_tq of list quant_item
- | TypQ_no_forall (* sugar, omitting quantifier and constraints *)
+type nec =  (* Numeric expression constraints *)
+ | Nec_lteq of ne * ne
+ | Nec_eq of ne * ne
+ | Nec_gteq of ne * ne
+
+
+type typschm =  (* type scheme *)
+ | TypSchm_ts of typquant * typ
 
 
 type pat =  (* Pattern *)
@@ -144,19 +163,6 @@ and fpat =  (* Field pattern *)
  | FP_Fpat of id * pat
 
 
-type typschm =  (* type scheme *)
- | TypSchm_ts of typquant * typ
-
-
-type ne =  (* internal numeric expressions *)
- | Ne_var of id
- | Ne_const of num
- | Ne_mult of ne * ne
- | Ne_add of ne * ne
- | Ne_exp of ne
- | Ne_unary of ne
-
-
 type exp =  (* Expression *)
  | E_block of list exp (* block (parsing conflict with structs?) *)
  | E_id of id (* identifier *)
@@ -203,18 +209,15 @@ and letbind =  (* Let binding *)
  | LB_val_implicit of pat * exp (* value binding, implicit type (pat must be total) *)
 
 
-type k =  (* Internal kinds *)
- | Ki_typ
- | Ki_nat
- | Ki_ord
- | Ki_efct
- | Ki_val (* Representing values, for use in identifier checks *)
- | Ki_ctor of list k * k
- | Ki_infer (* Representing an unknown kind, inferred by context *)
+type index_range =  (* index specification, for bitfields in register types *)
+ | BF_single of num (* single index *)
+ | BF_range of num * num (* index range *)
+ | BF_concat of index_range * index_range (* concatenation of index ranges *)
 
 
-type tannot_opt =  (* Optional type annotation for functions *)
- | Typ_annot_opt_some of typquant * typ
+type naming_scheme_opt =  (* Optional variable-naming-scheme specification for variables of defined type *)
+ | Name_sect_none
+ | Name_sect_some of string
 
 
 type effects_opt =  (* Optional effect annotation for functions *)
@@ -227,23 +230,31 @@ type rec_opt =  (* Optional recursive annotation for functions *)
  | Rec_rec (* recursive *)
 
 
+type tannot_opt =  (* Optional type annotation for functions *)
+ | Typ_annot_opt_some of typquant * typ
+
+
 type funcl =  (* Function clause *)
  | FCL_Funcl of id * pat * exp
 
 
-type index_range =  (* index specification, for bitfields in register types *)
- | BF_single of num (* single index *)
- | BF_range of num * num (* index range *)
- | BF_concat of index_range * index_range (* concatenation of index ranges *)
+type k =  (* Internal kinds *)
+ | Ki_typ
+ | Ki_nat
+ | Ki_ord
+ | Ki_efct
+ | Ki_val (* Representing values, for use in identifier checks *)
+ | Ki_ctor of list k * k
+ | Ki_infer (* Representing an unknown kind, inferred by context *)
 
 
-type naming_scheme_opt =  (* Optional variable-naming-scheme specification for variables of defined type *)
- | Name_sect_none
- | Name_sect_some of string
+type default_typing_spec =  (* Default kinding or typing assumption *)
+ | DT_kind of base_kind * id
+ | DT_typ of typschm * id
 
 
-type fundef =  (* Function definition *)
- | FD_function of rec_opt * tannot_opt * effects_opt * list funcl
+type val_spec =  (* Value type specification *)
+ | VS_val_spec of typschm * id
 
 
 type type_def =  (* Type definition body *)
@@ -254,13 +265,8 @@ type type_def =  (* Type definition body *)
  | TD_register of id * nexp * nexp * list (index_range * id) (* register mutable bitfield type definition *)
 
 
-type default_typing_spec =  (* Default kinding or typing assumption *)
- | DT_kind of base_kind * id
- | DT_typ of typschm * id
-
-
-type val_spec =  (* Value type specification *)
- | VS_val_spec of typschm * id
+type fundef =  (* Function definition *)
+ | FD_function of rec_opt * tannot_opt * effects_opt * list funcl
 
 
 type def =  (* Top-level definition *)
@@ -277,6 +283,14 @@ type def =  (* Top-level definition *)
  | DEF_scattered_end of id (* scattered definition end *)
 
 
+type ts = 
+ | Ts_lst of list t
+
+
+type defs =  (* Definition sequence *)
+ | Defs of list def
+
+
 type typ_lib =  (* library types and syntactic sugar for them *)
  | Typ_lib_unit (* unit type with value $()$ *)
  | Typ_lib_bool (* booleans $true$ and $false$ *)
@@ -294,8 +308,4 @@ type typ_lib =  (* library types and syntactic sugar for them *)
  | Typ_lib_reg of typ (* mutable register components holding typ *)
 
 
-type defs =  (* Definition sequence *)
- | Defs of list def
-
-
 
diff --git a/language/l2.ml b/language/l2.ml
index c5cfd00b..feb1ca32 100644
--- a/language/l2.ml
+++ b/language/l2.ml
@@ -20,19 +20,14 @@ base_kind_aux =  (* base kind *)
 
 
 type 
-base_kind = 
-   BK_aux of base_kind_aux * l
-
-
-type 
 id_aux =  (* Identifier *)
    Id of x
  | DeIid of x (* remove infix status *)
 
 
 type 
-kind_aux =  (* kinds *)
-   K_kind of (base_kind) list
+base_kind = 
+   BK_aux of base_kind_aux * l
 
 
 type 
@@ -41,8 +36,8 @@ id =
 
 
 type 
-kind = 
-   K_aux of kind_aux * l
+kind_aux =  (* kinds *)
+   K_kind of (base_kind) list
 
 
 type 
@@ -58,9 +53,8 @@ and nexp =
 
 
 type 
-kinded_id_aux =  (* optionally kind-annotated identifier *)
-   KOpt_none of id (* identifier *)
- | KOpt_kind of kind * id (* kind-annotated variable *)
+kind = 
+   K_aux of kind_aux * l
 
 
 type 
@@ -72,6 +66,22 @@ nexp_constraint_aux =  (* constraint over kind $_$ *)
 
 
 type 
+kinded_id_aux =  (* optionally kind-annotated identifier *)
+   KOpt_none of id (* identifier *)
+ | KOpt_kind of kind * id (* kind-annotated variable *)
+
+
+type 
+nexp_constraint = 
+   NC_aux of nexp_constraint_aux * l
+
+
+type 
+kinded_id = 
+   KOpt_aux of kinded_id_aux * l
+
+
+type 
 efct_aux =  (* effect *)
    Effect_rreg (* read register *)
  | Effect_wreg (* write register *)
@@ -83,13 +93,9 @@ efct_aux =  (* effect *)
 
 
 type 
-kinded_id = 
-   KOpt_aux of kinded_id_aux * l
-
-
-type 
-nexp_constraint = 
-   NC_aux of nexp_constraint_aux * l
+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 nexp_constraint (* A constraint for this type *)
 
 
 type 
@@ -98,15 +104,8 @@ efct =
 
 
 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 nexp_constraint (* A constraint for this type *)
-
-
-type 
-effects_aux =  (* effect set, of kind $_$ *)
-   Effects_var of id
- | Effects_set of (efct) list (* effect set *)
+quant_item = 
+   QI_aux of quant_item_aux * l
 
 
 type 
@@ -117,13 +116,15 @@ order_aux =  (* vector order specifications, of kind $_$ *)
 
 
 type 
-quant_item = 
-   QI_aux of quant_item_aux * l
+effects_aux =  (* effect set, of kind $_$ *)
+   Effects_var of id
+ | Effects_set of (efct) list (* effect set *)
 
 
 type 
-effects = 
-   Effects_aux of effects_aux * l
+typquant_aux =  (* type quantifiers and constraints *)
+   TypQ_tq of (quant_item) list
+ | TypQ_no_forall (* sugar, omitting quantifier and constraints *)
 
 
 type 
@@ -132,9 +133,13 @@ order =
 
 
 type 
-typquant_aux =  (* type quantifiers and constraints *)
-   TypQ_tq of (quant_item) list
- | TypQ_no_forall (* sugar, omitting quantifier and constraints *)
+effects = 
+   Effects_aux of effects_aux * l
+
+
+type 
+typquant = 
+   TypQ_aux of typquant_aux * l
 
 
 type 
@@ -159,11 +164,6 @@ and typ_arg =
 
 
 type 
-typquant = 
-   TypQ_aux of typquant_aux * l
-
-
-type 
 lit_aux =  (* Literal constant *)
    L_unit (* $() : _$ *)
  | L_zero (* $_ : _$ *)
@@ -283,12 +283,33 @@ and 'a letbind =
 
 
 type 
+ne =  (* internal numeric expressions *)
+   Ne_var of id
+ | Ne_const of int
+ | Ne_mult of ne * ne
+ | Ne_add of (ne) list
+ | Ne_exp of ne
+ | Ne_unary of ne
+
+
+type 
 naming_scheme_opt_aux =  (* Optional variable-naming-scheme specification for variables of defined type *)
    Name_sect_none
  | Name_sect_some of string
 
 
 type 
+rec_opt_aux =  (* Optional recursive annotation for functions *)
+   Rec_nonrec (* non-recursive *)
+ | Rec_rec (* recursive *)
+
+
+type 
+'a funcl_aux =  (* Function clause *)
+   FCL_Funcl of id * 'a pat * 'a exp
+
+
+type 
 'a tannot_opt_aux =  (* Optional type annotation for functions *)
    Typ_annot_opt_some of typquant * typ
 
@@ -300,14 +321,10 @@ type
 
 
 type 
-rec_opt_aux =  (* Optional recursive annotation for functions *)
-   Rec_nonrec (* non-recursive *)
- | Rec_rec (* recursive *)
-
-
-type 
-'a funcl_aux =  (* Function clause *)
-   FCL_Funcl of id * 'a pat * 'a exp
+nec =  (* Numeric expression constraints *)
+   Nec_lteq of ne * ne
+ | Nec_eq of ne * ne
+ | Nec_gteq of ne * ne
 
 
 type 
@@ -326,16 +343,6 @@ naming_scheme_opt =
 
 
 type 
-'a tannot_opt = 
-   Typ_annot_opt_aux of 'a tannot_opt_aux * 'a annot
-
-
-type 
-'a effects_opt = 
-   Effects_opt_aux of 'a effects_opt_aux * 'a annot
-
-
-type 
 rec_opt = 
    Rec_aux of rec_opt_aux * l
 
@@ -346,8 +353,13 @@ type
 
 
 type 
-'a val_spec_aux =  (* Value type specification *)
-   VS_val_spec of typschm * id
+'a tannot_opt = 
+   Typ_annot_opt_aux of 'a tannot_opt_aux * 'a annot
+
+
+type 
+'a effects_opt = 
+   Effects_opt_aux of 'a effects_opt_aux * 'a annot
 
 
 type 
@@ -360,29 +372,19 @@ type
 
 
 type 
-'a default_typing_spec_aux =  (* Default kinding or typing assumption *)
-   DT_kind of base_kind * id
- | DT_typ of typschm * id
-
-
-type 
 'a fundef_aux =  (* Function definition *)
    FD_function of rec_opt * 'a tannot_opt * 'a effects_opt * ('a funcl) list
 
 
 type 
-ne =  (* internal numeric expressions *)
-   Ne_var of id
- | Ne_const of int
- | Ne_mult of ne * ne
- | Ne_add of ne * ne
- | Ne_exp of ne
- | Ne_unary of ne
+'a val_spec_aux =  (* Value type specification *)
+   VS_val_spec of typschm * id
 
 
 type 
-'a val_spec = 
-   VS_aux of 'a val_spec_aux * 'a annot
+'a default_typing_spec_aux =  (* Default kinding or typing assumption *)
+   DT_kind of base_kind * id
+ | DT_typ of typschm * id
 
 
 type 
@@ -391,13 +393,18 @@ type
 
 
 type 
-'a default_typing_spec = 
-   DT_aux of 'a default_typing_spec_aux * 'a annot
+'a fundef = 
+   FD_aux of 'a fundef_aux * 'a annot
 
 
 type 
-'a fundef = 
-   FD_aux of 'a fundef_aux * 'a annot
+'a val_spec = 
+   VS_aux of 'a val_spec_aux * 'a annot
+
+
+type 
+'a default_typing_spec = 
+   DT_aux of 'a default_typing_spec_aux * 'a annot
 
 
 type 
@@ -450,6 +457,11 @@ type
 
 
 type 
+ts = 
+   Ts_lst of (t) list
+
+
+type 
 'a defs =  (* Definition sequence *)
    Defs of ('a def) list
 
diff --git a/language/l2.ott b/language/l2.ott
index 69b2bf9c..f129d9c4 100644
--- a/language/l2.ott
+++ b/language/l2.ott
@@ -268,6 +268,7 @@ effects :: 'Effects_' ::=
  | effect id                                  :: :: var
  | effect { efct1 , .. , efctn }           :: :: set {{ com effect set }}
  | pure                                 :: M :: pure {{ com sugar for empty effect set }} {{ ichlo [] }}
+ | effects1 u+ .. u+ effectsn                   :: M :: union {{ com meta operation for combining sets of effects }} {{ ichlo [] }}
 
 % TODO: are we going to need any effect polymorphism?  Conceivably for built-in maps and folds.  Yes.  But we think we don't need any interesting effect-set expressions, eg effectset-variable union {rreg}. 
 
@@ -888,16 +889,6 @@ defs :: '' ::=
  
 grammar 
 
-%% %% t_subst {{ tex \ensuremath{\sigma} }} :: '' ::= {{ phantom }}
-%% %%                                                 {{ hol (a # t) list }}
-%% %%                                                 {{ lem list (tnvar * t) }}
-%% %%   {{ com Type variable substitutions }}
-%% %%   | { tnvar1 |-> t1 .. tnvarn |-> tn }                  :: :: T_subst
-%% %%     {{ ocaml (assert false) }}
-%% %%     {{ lem ([[tnvar1 t1 .. tnvarn tn]]) }}
-%% %%     {{ hol ([[tnvar1 t1 .. tnvarn tn]]) }}
-%% %% 
-
 k :: 'Ki_' ::=
 {{ com Internal kinds }}
    | K_Typ                                             :: :: typ
@@ -911,31 +902,23 @@ k :: 'Ki_' ::=
 t , u :: 'T_' ::=                                {{ phantom }}
 {{ com Internal types }}
    | id                                           :: :: var
-   | t1 -> t2 effects                                 :: :: fn
-   | t1 * .... * tn                              :: :: tup
+   | t1 -> t2 effects tag S_N                     :: :: fn  {{ com [[S_N]] are constraints for the function, [[tag]] holds generation data }}
+   | ( t1 * .... * tn )                           :: :: tup
    | id t_args                                    :: :: app 
-%% %%   | t_subst ( t )                               :: M :: subst_app
-%% %%     {{ com Multiple substitutions }}
-%% %%     {{ ocaml (assert false) }}
-%% %%     {{ hol (t_subst_t [[t_subst]] [[t]]) }}
-%% %%     {{ lem (t_subst_t [[t_subst]] [[t]]) }}
-%% %%   | t_subst ( tnv )                     :: M :: var_subst_app
-%% %%     {{ com Single variable substitution }}
-%% %%     {{ ocaml (assert false) }}
-%% %%     {{ hol (t_subst_tnv [[t_subst]] [[tnv]]) }}
-%% %%     {{ lem (t_subst_tnv [[t_subst]] [[tnv]]) }}
-%% %%   | curry ( t_multi ,  t )                      :: M :: multifn
-%% %%     {{ com Curried, multiple argument functions }}
-%% %%     {{ ocaml (assert false) }}
-%% %%     {{ hol (FOLDR T_fn [[t]] [[t_multi]]) }}
-%% %%     {{ lem (List.fold_right T_fn [[t_multi]] [[t]]) }}
-%% %% 
+
+tag :: 'Tag_' ::=                                 {{ phantom }}
+{{ com Data indicating where the function 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 }}
+   | _                                    :: :: dontcare 
+
 ne :: 'Ne_' ::=
  {{ com internal numeric expressions }}
    | id                                           :: :: var
    | num                                 :: :: const
    | ne1 * ne2                           :: :: mult
-   | ne1 + ne2                           :: :: add
+   | ne1 + ... + nen                           :: :: add
    | 2 ** ne				 :: :: exp
    | ( - ne )                            :: :: unary
 %% %%   | ne1 + ... + nen                     :: M :: addmany
@@ -950,16 +933,16 @@ ne :: 'Ne_' ::=
      {{ 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 :: '' ::=   {{ phantom }}
+   | 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_' ::=   {{ phantom }}
  {{ com Argument to type constructors }}
  | t :: :: typ
  | ne :: :: nexp
@@ -970,17 +953,12 @@ ne :: 'Ne_' ::=
   {{ com Arguments to type constructors }}
    | t_arg1 ... t_argn                            :: :: T_args
 
-%% %% nec :: '' ::=
-%% %%   {{ com Numeric expression constraints }}
-%% %%   | ne < nec            :: :: lessthan
-%% %%   | ne = nec            :: :: eq
-%% %%   | ne <= nec           :: :: lteq
-%% %%   | ne                          :: :: base
-%% %% 
-%% %% parsing
-%% %% T_fn right T_fn
-%% %% T_tup <= T_multi
-%% %% 
+ nec :: 'Nec_' ::=
+   {{ com Numeric expression constraints }}
+   | ne <= ne'            :: :: lteq
+   | ne = ne'            :: :: eq
+   | ne >= ne'           :: :: gteq
+
 %% %% embed
 %% %% {{ lem
 %% %% 
@@ -1087,30 +1065,40 @@ ne :: 'Ne_' ::=
 %% %%     {{ hol [[x1..xn]] }}
 %% %%     {{ lem [[x1..xn]] }}
 %% %% 
-%% %% S_N {{ tex { \ensuremath{ {\Sigma}^{\mathcal{N} } } } }} :: '' ::= {{ phantom }}
-%% %%                                                                    {{ hol nec list }}
-%% %%                                                                    {{ lem list nec }}
-%% %%    {{ com nexp constraint lists }}
-%% %%    | { nec1 , .. ,  necn }                              :: :: Sn_concrete
-%% %%      {{ hol [[nec1 .. necn]] }}
-%% %%      {{ lem [[nec1 .. necn]] }}
-%% %%    | S_N1 union .. union S_Nn                   :: M :: SN_union
-%% %%      {{ hol (FLAT [[S_N1..S_Nn]]) }}
-%% %%      {{ lem (List.flatten [[S_N1..S_Nn]]) }}
-%% %%      {{ ocaml assert false }}
-%% %% 
-%% %% 
+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.fold_right union_map [[S_N1..S_Nn]] Pmap.empty) }}
+     {{ 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 }}
+ 
+ I :: '' ::=                                                     {{ phantom }}
+  {{ com Information given by type checking an expression; tag only reflects the immediate exp }}
+  | < S_N , effects , tag >                                      :: :: I
+  | Ir                                                           :: :: reset {{ com resets the tag of an I. }} {{ tex {\ottnt{I}_{\textit{reset} } } }}
+  | Ie                                                           :: :: Iempty {{ com Empty constraints, effetcs, tag }} {{ tex {\ottnt{I}_{\epsilon} } }}
+  | I1 u+ .. u+ In                                               :: :: Iunion {{ com Unions the constraints and effects, setting None for the tag }}
+
  E :: '' ::=                                                     {{ phantom }}
                                                                  {{ hol ((string,env_body) fmaptree) }}
                                                                  {{ lem env }}
  {{ com Environments }}
- | < E_t , E_k >                                           :: :: E
+ | < E_t , E_r , E_k >                                           :: :: E
   {{ hol arb }}
-  {{ lem (Env [[E_k]] [[E_t]]) }}
- | E1 u+ E2                                                    :: M :: E_union
-  {{ hol (env_union [[E1]] [[E2]]) }}
-  {{ lem (env_union [[E1]] [[E2]]) }}
-  {{ ocaml assert false }}
+  {{ lem (Env [[E_k]] [[E_r]] [[E_t]]) }}
  | empty                                                       :: M :: E_empty
    {{ hol arb }}
    {{ lem EnvEmp }}
@@ -1140,68 +1128,21 @@ ne :: 'Ne_' ::=
      {{ lem (List.fold_right union_map [[E_t1..E_tn]] Pmap.empty) }}
      {{ ocaml (assert false) }}
 
-%% %% tc_abbrev :: 'Tc_abbrev_' ::=                                   {{ phantom }}
-%% %%                                                                 {{ hol t option }}
-%% %%                                                                 {{ lem option t }}
-%% %%                                                                 {{ ocaml t option }}
-%% %%   {{ com Type abbreviations }}
-%% %%   | . t                                                         :: :: some
-%% %%     {{ hol (SOME [[t]]) }}
-%% %%     {{ lem (Some [[t]]) }}
-%% %%   |                                                             :: :: none
-%% %%     {{ hol NONE }}
-%% %%     {{ lem None }}
-%% %% 
-%% %% tc_def :: '' ::=
-%% %%   {{ com Type and class constructor definitions }} 
-%% %%   | tnvs tc_abbrev                                              :: :: Tc_def
-%% %%     {{ com Type constructors }}
-%% %% 
-%% %% TD {{ tex \ensuremath{\Delta} }} :: 'TD_' ::=                   {{ phantom }}
-%% %%                                                                 {{ hol p |-> tc_def }}
-%% %%                                                                 {{ lem map p tc_def }}
-%% %%   {{ com Type constructor definitions }}
-%% %%   | { p1 |-> tc_def1 , .. , pn |-> tc_defn }                    :: :: concrete
-%% %%     {{ hol (FOLDR (\x E. E |+ x) FEMPTY [[p1 tc_def1 .. pn tc_defn]]) }}
-%% %%     {{ lem (List.fold_right (fun (p,t) m -> Pmap.add p t m) [[p1 tc_def1 .. pn tc_defn]] Pmap.empty) }} 
-%% %%     {{ ocaml (assert false) }}
-%% %%   | TD1 u+ TD2                                                  :: M :: union
-%% %%     {{ hol (FUNION [[TD1]] [[TD2]]) }}
-%% %%     {{ lem (union_map [[TD1]] [[TD2]]) }}
-%% %%     {{ ocaml (assert false) }}
-%% %% 
-%% %% 
-%% %% 
-%% %% D :: 'D_' ::=                                                   {{ phantom }}
-%% %%                                                                 {{ hol ((p |-> tc_def) # (p |-> x list) # (inst list)) }}
-%% %%                                                                 {{ lem tdefs}}
-%% %%   {{ com Global type definition store }}
-%% %%   | < TD , TC , I >                                                     :: :: concrete
-%% %%     {{ hol ([[TD]], [[TC]], [[I]]) }}
-%% %%     {{ lem (D [[TD]] [[TC]] [[I]]) }}
-%% %%   | D1 u+ D2                                                    :: M :: union
-%% %%     {{ hol (case ([[D1]],[[D2]]) of ((x1,x2,x3),(y1,y2,y3)) => (FUNION x1 y1, FUNION x2 y2, x3 ++ y3)) }}
-%% %%     {{ lem (union_tcdefs [[D1]] [[D2]]) }}
-%% %%     {{ ocaml (assert false) }}
-%% %%   | empty                                                       :: M :: empty
-%% %%     {{ hol (FEMPTY, FEMPTY, []) }}
-%% %%     {{ lem DEmp }}
-%% %%     {{ ocaml assert false }}
-%% %% 
-%% %% parsing
-%% %% E_union left E_union
-%% %% 
-%% %% embed
-%% %% {{ lem
-%% %% type tdefs =
-%% %%   | DEmp
-%% %%   | D of (map p tc_def) * (map p (list x)) * (set inst)
-%% %% 
-%% %% val union_tcdefs : tdefs -> tdefs -> tdefs
-%% %% 
-%% %% }}
+ field_typs :: 'FT_' ::=     {{ phantom }}
+ {{ com Record fields }}
+ | id1 : t1 , .. , idn : tn :: :: fields
 
-grammar
+ E_r {{ tex \ottnt{E}^{\textsc{r} } }} :: 'E_r_' ::=             {{ phantom }}
+                                                                 {{ hol (id |-> t) }}
+                                                                 {{ lem map x f_desc }}
+   {{ com Record environments }}
+   | { { field_typs1 } |-> t1 , .. , { field_typsn } |-> tn }                    :: :: concrete
+     {{ hol (FOLDR (\x E. E |+ x) FEMPTY) }}
+     {{ lem (List.fold_right (fun (x,f) m -> Pmap.add x f m)  Pmap.empty) }} 
+   | E_r1 u+ .. u+ E_rn                                          :: M :: union
+     {{ hol (FOLDR FUNION FEMPTY [[E_r1..E_rn]]) }}
+     {{ lem (List.fold_right union_map [[E_r1..E_rn]] Pmap.empty) }}
+     {{ ocaml (assert false) }}
 
 terminals :: '' ::=
   | **                                  :: :: starstar
@@ -1227,8 +1168,6 @@ terminals :: '' ::=
     {{ com \texttt{|>} }}
   | inter                               :: :: inter
     {{ tex \ensuremath{\cap} }}
-%  | union                               :: :: union
-%    {{ tex \ensuremath{\cup} }}
   | u+                                  :: :: uplus
     {{ tex \ensuremath{\uplus} }}
   | NOTIN                               :: :: notin
@@ -1243,6 +1182,10 @@ terminals :: '' ::=
     {{ tex \ensuremath{\langle} }}
   | >                                   :: :: gt
     {{ tex \ensuremath{\rangle} }}
+  | lt                                  :: :: mathlt
+    {{ tex < }}
+  | gt                                  :: :: mathgt
+    {{ tex > }} 
   | |-                                  :: :: vdash
     {{ tex \ensuremath{\vdash} }}
   | |-t					:: :: vdashT
@@ -1267,7 +1210,13 @@ terminals :: '' ::=
     {{ tex \mbox{--} }}
   | empty                               :: :: empty
     {{ tex \ensuremath{\epsilon} }}
- 
+  | consistent_increase                 :: :: ci
+    {{ tex \ottkw{consistent\_increase}~ }}
+  | consistent_decrease                 :: :: cd
+    {{ tex \ottkw{consistent\_decrease}~ }}
+
+ts :: ts_ ::=
+  | t1 , .. , tn :: :: lst 
 
 formula :: formula_ ::=
   | judgement                                                   :: :: judgement
@@ -1287,14 +1236,11 @@ formula :: formula_ ::=
   | E_k ( id ) <-| k						:: :: update_k
      {{ com Update the kind associated with id to k }}        
 
-%% %% %   | TD ( p ) gives tc_def                                     :: :: lookup_tc
-%% %% %     {{ com Type constructor lookup }}
-%% %% %     {{ hol (FLOOKUP [[TD]] [[p]] = SOME [[tc_def]]) }}
-%% %% %     {{ lem Pmap.find [[p]] [[TD]] = [[tc_def]] }} 
-%% %% 
-%% %%   | dom ( E_m1 ) inter dom ( E_m2 ) = emptyset                  :: :: E_m_disjoint
-%% %%     {{ hol (DISJOINT (FDOM [[E_m1]]) (FDOM [[E_m2]])) }}
-%% %%     {{ lem disjoint (Pmap.domain [[E_m1]]) (Pmap.domain [[E_m2]]) }} 
+  | E_r ( id0 .. idn ) gives t , ts                      :: :: lookup_r
+     {{ com Record lookup }}
+
+  | E_r ( t ) gives id0 : t0 .. idn : tn                 :: :: lookup_rt
+    {{ com Record looup by type }}
 
    | dom ( E_t1 ) inter dom ( E_t2 ) = emptyset                  :: :: E_t_disjoint
      {{ hol (DISJOINT (FDOM [[E_t1]]) (FDOM [[E_t2]])) }}
@@ -1330,6 +1276,8 @@ formula :: formula_ ::=
    | id NOTIN dom ( E_t )                                         :: :: notin_dom_t
      {{ hol ([[id]] NOTIN FDOM [[E_t]]) }}
      {{ lem Pervasives.not (Pmap.mem [[id]] [[E_t]]) }} 
+
+   | id0 : t0 .. idn : tn SUBSET id'0 : t'0 .. id'i : t'i       :: :: subsetFields
 %% %% 
 %% %% 
 %% %%   | FV ( t ) SUBSET tnvs                                                :: :: FV_t
@@ -1355,14 +1303,22 @@ formula :: formula_ ::=
 %% %%     {{ hol (~?__semC__. MEM (Inst __semC__ [[p]] [[t]]) [[I]]) }}
 %% %%     {{ lem (Pervasives.not ((Inst [] [[p]] [[t]]) IN [[I]])) }}
 %% %% 
+
+   | num1 lt ... lt numn                                         :: :: increasing
+
+   | num1 gt ... gt numn                                         :: :: decreasing
+
    | E_k1 = E_k2                                                 :: :: E_k_eqn
      {{ ichl ([[E_k1]] = [[E_k2]]) }}
 
-   | E_t1 = E_t2                                                 :: :: E_f_eqn
+   | E_t1 = E_t2                                                 :: :: E_t_eqn
      {{ ichl ([[E_t1]] = [[E_t2]]) }}
  
    | E1 = E2                                                     :: :: E_eqn
      {{ ichl ([[E1]] = [[E2]]) }}
+
+   | S_N1 = S_N2                                                :: :: S_N_eqn
+     {{ ichl ([[S_N1]] = [[S_N2]]) }}
  
 %% %%   | TD1 = TD2                                                   :: :: TD_eqn
 %% %%     {{ ichl ([[TD1]] = [[TD2]]) }}
diff --git a/language/l2_rules.ott b/language/l2_rules.ott
index 7359c1c6..fdd81c96 100644
--- a/language/l2_rules.ott
+++ b/language/l2_rules.ott
@@ -21,11 +21,11 @@ E_k |-t t ok :: :: check_t :: check_t_
  E_k |-t t2 ok
  E_k |-e effects ok
  ------------------------------------------------------------ :: fn
- E_k |-t t1 -> t2 effects ok
+ E_k |-t t1 -> t2 effects tag S_N ok
 
  E_k |-t t1 ok .... E_k |-t tn ok
  ------------------------------------------------------------ :: tup
- E_k |-t t1 * .... * tn ok
+ E_k |-t (t1 * .... * tn) ok
 
  E_k(id) gives K_Lam(k1..kn -> K_Typ)
  E_k,k1 |- t_arg1 ok .. E_k,kn |- t_argn ok
@@ -89,10 +89,10 @@ E_k(id) gives K_Ord
 ----------------------------------------------------------- :: var
 E_k |-o id ok
 
- E_k(id) gives K_infer
- E_k(id) <-| K_Ord
- ------------------------------------------------------------ :: varInfer
- E_k |-o id ok
+E_k(id) gives K_infer
+E_k(id) <-| K_Ord
+------------------------------------------------------------ :: varInfer
+E_k |-o id ok
 
 
 defn
@@ -120,13 +120,13 @@ E_k, K_Ord |- order ok
 %% % 
 %% % %TODO type equality isn't right; neither is type conversion
 %% % 
-%% % defns
-%% % teq :: '' ::=
-%% % 
-%% % defn
-%% % TD |- t1 = t2 :: :: teq :: teq_ 
-%% % {{ com Type equality }}
-%% % by
+defns
+teq :: '' ::=
+
+defn
+E_k |- t1 = t2 :: :: teq :: teq_ 
+{{ com Type equality }}
+by
 %% % 
 %% % TD |- t ok
 %% % ------------------------------------------------------------ :: refl
@@ -181,11 +181,11 @@ E_k |- typ1 ~> t1
 E_k |- typ2 ~> t2
 E_k |-e effects ok
 ------------------------------------------------------------ :: fn
-E_k |- typ1->typ2 effects ~> t1->t2 effects
+E_k |- typ1->typ2 effects ~> t1->t2 effects None
  
 E_k |- typ1 ~> t1 .... E_k |- typn ~> tn
 ------------------------------------------------------------ :: tup
-E_k |- typ1 * .... * typn ~> t1 * .... * tn
+E_k |- typ1 * .... * typn ~> (t1 * .... * tn)
 
 E_k(id) gives K_Lam (k1..kn -> K_Typ)
 E_k,k1 |- typ_arg1 ~> t_arg1 .. E_k,kn |- typ_argn ~> t_argn
@@ -193,7 +193,7 @@ E_k,k1 |- typ_arg1 ~> t_arg1 .. E_k,kn |- typ_argn ~> t_argn
 E_k |- id typ_arg1 .. typ_argn ~> id t_arg1 .. t_argn
 
 E_k |- typ ~> t1
-%E_k |- t1 = t2
+E_k |- t1 = t2
 ------------------------------------------------------------ :: eq
 E_k |- typ ~> t2
 
@@ -248,7 +248,7 @@ by
  |- false : bool
  
  ------------------------------------------------------------ :: num
- |- num : nat
+ |- num : enum num num inc
  
  ------------------------------------------------------------- :: string
  |- string : string
@@ -354,84 +354,87 @@ defns
 check_pat :: '' ::=
  
 defn
-E |- pat : t gives E_t :: :: check_pat :: check_pat_ 
+E |- pat : t gives E_t , S_N :: :: check_pat :: check_pat_ 
 {{ com Typing patterns, building their binding environment }}
 by
 
+|- lit : t
+------------------------------------------------------------ :: lit
+E |- lit : t gives {}, {}
+
 E_k |-t t ok
 ------------------------------------------------------------ :: wild
-<E_t,E_k> |- _ annot : t gives {} 
+<E_t,E_r,E_k> |- _ : t gives {}, {}
 % This case should perhaps indicate the generation of a type variable, with kind Typ
 
-<E_t,E_k> |- pat : t gives E_t1
+<E_t,E_r,E_k> |- pat : t gives E_t1,S_N
 id NOTIN dom(E_t1)
 ------------------------------------------------------------ :: as
-<E_t,E_k> |- (pat as id) : t gives E_t1 u+ {id|->t}
+<E_t,E_r,E_k> |- (pat as id) : t gives E_t1 u+ {id|->t},S_N
 
 E_k |- typ ~> t
-<E_t,E_k> |- pat : t gives E_t1
+<E_t,E_r,E_k> |- pat : t gives E_t1,S_N
 ------------------------------------------------------------ :: typ
-<E_t,E_k> |- (<typ> pat) : t gives E_t1
+<E_t,E_r,E_k> |- (<typ> pat) : t gives E_t1,S_N
 
-%% % TD,E |- ctor id : (t1*..*tn) -> p t_args gives (x of names)
-<E_t,E_k> |- pat1 : t1 gives E_t1 .. <E_t,E_k> |- patn : tn gives E_tn
-%% % disjoint doms(E_l1,..,E_ln)
+E_t(id) gives (t1*..*tn) -> id t_args effect { } Ctor
+<E_t,E_r,E_k> |- pat1 : t1 gives E_t1,S_N1 .. <E_t,E_r,E_k> |- patn : tn gives E_tn,S_Nn
+disjoint doms(E_t1,..,E_tn)
 ------------------------------------------------------------ :: ident_constr
-<E_t,E_k> |- id pat1 .. patn : id t_args gives E_t1 u+ .. u+ E_tn
+<E_t,E_r,E_k> |- id pat1 .. patn : id t_args gives E_t1 u+ .. u+ E_tn, S_N1 u+ .. u+ S_Nn
 
 E_k |-t t ok
  ------------------------------------------------------------ :: var
-<E_t,E_k> |- :P_id: id : t gives E_t u+ {id|->t}
-
-%% % 
-%% % </TD,E |- field idi : p t_args -> ti gives (xi of names) // i />
-%% % </TD,E,E_l |- pati : ti gives E_li//i/>
-%% % disjoint doms(</E_li//i/>)
-%% % duplicates(</xi//i/>) = emptyset
-%% % ------------------------------------------------------------ :: record
-%% % TD,E,E_l |- <| </idi = pati li//i/> semi_opt |> : p t_args gives u+ </E_li//i/>
-%% % 
-%% % TD,E,E_l |- pat1 : t gives E_l1 ... TD,E,E_l |- patn : t gives E_ln
-%% % disjoint doms(E_l1 , ... , E_ln)
-%% % length(pat1 ... patn) = nat
-%% % ----------------------------------------------------------- :: vector
-%% % TD,E,E_l |- [| pat1 ; ... ; patn semi_opt |] : __vector nat t gives E_l1 u+ ... u+ E_ln
-%% % 
-%% % TD,E,E_l |- pat1 : __vector ne1 t gives E_l1 ... TD,E,E_l |- patn : __vector nen t gives E_ln
-%% % disjoint doms(E_l1 , ... , E_ln)
-%% % ne' = ne1 + ... + nen
-%% % ----------------------------------------------------------- :: vectorConcat
-%% % TD,E,E_l |- [| pat1 ... patn  |] : __vector ne' t gives E_l1 u+ ... u+ E_ln
-%% % 
+<E_t,E_r,E_k> |- :P_id: id : t gives E_t u+ {id|->t},{}
 
-<E_t,E_k> |- pat1 : t1 gives E_t1 .... <E_t,E_k> |- patn : tn gives E_tn
+E_r(</idi//i/>) gives id t_args, (</ti//i/>)
+</<E_t,E_r,E_k> |- pati : ti gives E_ti,S_Ni//i/>
+disjoint doms(</E_ti//i/>)
+------------------------------------------------------------ :: record
+<E_t,E_r,E_k> |- { </idi = pati//i/> semi_opt } : id t_args gives u+ </E_ti//i/>, u+ </S_Ni//i/>
+ 
+E |- pat1 : t gives E_t1,S_N1 ... E |- patn : t gives E_tn,S_Nn
+disjoint doms(E_t1 , ... , E_tn)
+length(pat1 ... patn) = num
+----------------------------------------------------------- :: vector
+E |- [ pat1 , ... , patn ] : vector :t_arg_nexp: id num+id inc t gives E_t1 u+ ... u+ E_tn,S_N1 u+ ... u+ S_Nn
+
+E |- pat1 : t gives E_t1,S_N1 ... E |- patn : t gives E_tn,S_Nn
+disjoint doms(E_t1 , ... , E_tn)
+num1 lt ... lt numn
+----------------------------------------------------------- :: indexedVectorInc
+E |- [ num1 = pat1 , ... , numn = patn ] : vector :t_arg_nexp: id :t_arg_nexp: id' inc t gives E_t1 u+ ... u+ E_tn, {id<=num1, id' >= numn + (- num1)} u+ S_N1 u+ ... u+ S_Nn
+
+E |- pat1 : t gives E_t1,S_N1 ... E |- patn : t gives E_tn,S_Nn
+disjoint doms(E_t1 , ... , E_tn)
+num1 gt ... gt numn
+----------------------------------------------------------- :: indexedVectorDec
+E |- [ num1 = pat1 , ... , numn = patn ] : vector :t_arg_nexp: id :t_arg_nexp: id' dec t gives E_t1 u+ ... u+ E_tn, {id>=num1,id'<=num1 +(-numn)} u+ S_N1 u+ ... u+ S_Nn
+
+E |- pat1 : vector ne1 ne'1 inc t gives E_t1,S_N1 ... E |- patn : vector nen ne'n inc t gives E_tn,S_Nn
+disjoint doms(E_t1 , ... , E_tn)
+S_N0 = consistent_increase ne1 ne'1 ... nen ne'n
+----------------------------------------------------------- :: vectorConcatInc
+E |- pat1 : ... : patn : vector :t_arg_nexp: id :t_arg_nexp: id' inc t gives E_t1 u+ ... u+ E_tn,{id<=ne1,id'>= ne'1 + ... + ne'n} u+ S_N0 u+ S_N1 u+ ... u+ S_Nn
+
+E |- pat1 : vector ne1 ne'1 dec t gives E_t1,S_N1 ... E |- patn : vector nen ne'n dec t gives E_tn,S_Nn
+disjoint doms(E_t1 , ... , E_tn)
+S_N0 = consistent_decrease ne1 ne'1 ... nen ne'n
+----------------------------------------------------------- :: vectorConcatDec
+E |- pat1 : ... : patn : vector :t_arg_nexp: id :t_arg_nexp: id' inc t gives E_t1 u+ ... u+ E_tn,{id>=ne1,id'>= ne'1 + ... + ne'n} u+ S_N0 u+ S_N1 u+ ... u+ S_Nn
+
+<E_t,E_r,E_k> |- pat1 : t1 gives E_t1,S_N1 .... <E_t,E_r,E_k> |- patn : tn gives E_tn,S_Nn
 disjoint doms(E_t1,....,E_tn)
 ------------------------------------------------------------ :: tup
-<E_t,E_k> |- (pat1, ...., patn) : t1 * .... * tn gives E_t1 u+ .... u+ E_tn 
+<E_t,E_r,E_k> |- (pat1, ...., patn) : (t1 * .... * tn) gives E_t1 u+ .... u+ E_tn,S_N1 u+ .... u+ S_Nn 
 
-%% % TD |- t ok
-%% % TD,E,E_l |- pat1 : t gives E_l1 .. TD,E,E_l |- patn : t gives E_ln
-%% % disjoint doms(E_l1,..,E_ln)
-%% % ------------------------------------------------------------ :: list
-%% % TD,E,E_l |- [pat1; ..; patn semi_opt] : __list t gives E_l1 u+ .. u+ E_ln 
-%% % 
-%% % TD,E,E_l1 |- pat : t gives E_l2
-%% % ------------------------------------------------------------ :: paren
-%% % TD,E,E_l1 |- (pat) : t gives E_l2
-%% % 
-%% % TD,E,E_l1 |- pat1 : t gives E_l2
-%% % TD,E,E_l1 |- pat2 : __list t gives E_l3
-%% % disjoint doms(E_l2,E_l3)
-%% % ------------------------------------------------------------ :: cons
-%% % TD,E,E_l1 |- pat1 :: pat2 : __list t gives E_l2 u+ E_l3
-%% % 
-%% % |- lit : t
-%% % ------------------------------------------------------------ :: lit
-%% % TD,E,E_l |- lit : t gives {}
-%% % 
-%% % E,E_l |- x not ctor
-%% % ------------------------------------------------------------ :: num_add
-%% % TD,E,E_l |- x l + num : __num gives {x|->__num}
+E_k |-t t ok
+<E_t,E_r,E_k> |- pat1 : t gives E_t1,S_N1 .. <E_t,E_r,E_k> |- patn : t gives E_tn,S_Nn
+disjoint doms(E_t1,..,E_tn)
+------------------------------------------------------------ :: list
+<E_t,E_r,E_k> |- [|pat1, .., patn |] : list t gives E_t1 u+ .. u+ E_tn,S_N1 u+ .. u+ S_Nn
+
+ 
 %% % 
 %% % 
 %% % defns
@@ -472,99 +475,55 @@ disjoint doms(E_t1,....,E_tn)
 %% % ------------------------------------------------------------ :: cons
 %% % <E_m,E_p,E_f,E_x> |- x l1.</y_li.//i/> z_l l2 value
 %% % 
+
 defns
 check_exp :: '' ::=
  
-%% % defn
-%% % TD , E , E_l |- exp : t gives S_c , S_N :: :: check_exp :: check_exp_ 
-%% % {{ com Typing expressions, collecting typeclass and index constraints }}
-%% % by
-%% % 
-%% % :check_exp_aux: TD,E,E_l |- exp_aux : t gives S_c,S_N
-%% % ------------------------------------------------------------ :: all
-%% % TD,E,E_l  |- exp_aux l : t gives S_c,S_N
-%% % 
-%% % defn
-%% % TD , E , E_l |- exp_aux : t gives S_c , S_N :: :: check_exp_aux :: check_exp_aux_
-%% % {{ com Typing expressions, collecting typeclass and index constraints }}
-%% % by
-%% % 
-%% % E_l(x) gives t
-%% % ------------------------------------------------------------ :: var
-%% % TD,E,E_l |- x l1 l2 : t gives {},{}
-%% % 
-%% % %TODO KG Add check that N is in scope
-%% % ------------------------------------------------------------ :: nvar
-%% % TD,E,E_l |- N : __num gives {},{}
-%% % 
-%% % E_l |- id not shadowed
-%% % E |- id value
-%% % TD,E |- ctor id : t_multi -> p t_args gives (x of names)
-%% % ------------------------------------------------------------ :: ctor
-%% % TD,E,E_l |- id : curry(t_multi, p t_args) gives {},{}
-%% % 
-%% % E_l |- id not shadowed
-%% % E |- id value
-%% % TD, E |- val id : t gives S_c
-%% % ------------------------------------------------------------ :: val
-%% % TD,E,E_l |- id : t gives S_c,{}
-%% % 
-%% % 
-%% % TD,E,E_l |- pat1 : t1 gives E_l1 ... TD,E,E_l |- patn : tn gives E_ln
-%% % TD,E,E_l u+ E_l1 u+ ... u+ E_ln |- exp : u gives S_c,S_N
-%% % disjoint doms(E_l1,...,E_ln)
-%% % ------------------------------------------------------------ :: fn
-%% % TD,E,E_l |- fun pat1 ... patn -> exp l : curry((t1*...*tn), u) gives S_c,S_N
-%% % 
-%% % %TODO: the various patterns might want to use different specifications for vector length (i.e. 32 in one and 8+n+8 in another)
-%% % % So should be pati : t gives E_li,S_Ni
-%% % </TD,E,E_l |- pati : t gives E_li//i/>
-%% % </TD,E,E_l u+ E_li |- expi : u gives S_ci, S_Ni//i/>
-%% % ------------------------------------------------------------ :: function
-%% % TD,E,E_l |- function bar_opt </pati -> expi li//i/> end : t -> u gives </S_ci//i/> , </S_Ni//i/>
-%% % 
-%% % %TODO t1 and t1 should be t1 and t'1 so that constraints from any vectors can be extracted and added to S_N
-%% % TD,E,E_l |- exp1 : t1 -> t2 gives S_c1,S_N1
-%% % TD,E,E_l |- exp2 : t1 gives S_c2,S_N2
-%% % ------------------------------------------------------------ :: app
-%% % TD,E,E_l |- exp1 exp2 : t2 gives S_c1 union S_c2, S_N1 union S_N2
-%% % 
-%% % %TODO t1 and t1 should be t1 and t'1 so that constraints from any vectors can be extracted and added to S_N
-%% % %          Same for t2
-%% % :check_exp_aux: TD,E,E_l |- (ix) : t1 -> t2 -> t3 gives S_c1,S_N1
-%% % TD,E,E_l |- exp1 : t1 gives S_c2,S_N2
-%% % TD,E,E_l |- exp2 : t2 gives S_c3,S_N3
-%% % ------------------------------------------------------------ :: infix_app1
-%% % TD,E,E_l |- exp1 ix l exp2 : t3 gives S_c1 union S_c2 union S_c3,S_N1 union S_N2 union S_N3
-%% % 
-%% % %TODO, see above todo
-%% % :check_exp_aux: TD,E,E_l |- x : t1 -> t2 -> t3 gives S_c1,S_N1
-%% % TD,E,E_l |- exp1 : t1 gives S_c2,S_N2
-%% % TD,E,E_l |- exp2 : t2 gives S_c3,S_N3
-%% % ------------------------------------------------------------ :: infix_app2
-%% % TD,E,E_l |- exp1 `x` l exp2 : t3 gives S_c1 union S_c2 union S_c3,S_N1 union S_N2 union S_N3
-%% % 
-%% % %TODO, see above todo, with regard to t_args
-%% % </TD,E |- field idi : p t_args -> ti gives (xi of names)//i/>
-%% % </TD,E,E_l |- expi : ti gives S_ci,S_Ni//i/>
-%% % duplicates(</xi//i/>) = emptyset
-%% % names = {</xi//i/>}
-%% % ------------------------------------------------------------ :: record
-%% % TD,E,E_l |- <| </idi = expi li//i/> semi_opt l |> : p t_args gives </S_ci//i/>,</S_Ni//i/>
-%% % 
-%% % %TODO, see above todo, with regard to t_args
-%% % </TD,E |- field idi : p t_args -> ti gives (xi of names)//i/>
-%% % </TD,E,E_l |- expi : ti gives S_ci,S_Ni//i/>
-%% % duplicates(</xi//i/>) = emptyset
-%% % TD,E,E_l |- exp : p t_args gives S_c',S_N'
-%% % ------------------------------------------------------------ :: recup
-%% % TD,E,E_l |- <| exp with </idi = expi li//i/> semi_opt l |> : p t_args gives S_c' union </S_ci//i/>,S_N' union </S_Ni//i/>
-%% % 
-%% % TD,E,E_l |- exp1 : t gives S_c1,S_N1 ... TD,E,E_l |- expn : t gives S_cn,S_Nn
-%% % length(exp1 ... expn) = nat
-%% % ------------------------------------------------------------ :: vector
-%% % TD,E,E_l |- [| exp1 ; ... ; expn semi_opt |] : __vector nat t gives S_c1 union ... union S_cn, S_N1 union ... union S_Nn
-%% % 
+defn
+E |- exp : t gives I :: :: check_exp :: check_exp_ 
+{{ com Typing expressions, collecting nexp constraints and effects }}
+by
+
+%% TODO::: if t is a reg, need to distinguish here between reg and ref cell access, and add to effect if reg, and maybe add to tag
+ 
+E_t(id) gives t
+------------------------------------------------------------ :: var
+<E_t,E_r,E_k> |- id : t gives Ie
+
+E_t(id) gives t' -> t effect {} Ctor {} 
+<E_t,E_r,E_k> |- exp : t' gives I
+------------------------------------------------------------ :: ctor
+<E_t,E_r,E_k> |- id exp : t gives Ir
+
+ 
+E_t(id) gives t' -> t effects tag S_N
+<E_t,E_r,E_k> |- exp : t' gives <S_N1,effects',_>
+------------------------------------------------------------ :: app
+<E_t,E_r,E_k> |- id exp : t gives <S_N u+ S_N1,effects u+ effects',tag>
+ 
+E_t(id) gives (t1 * t2) -> t effects tag S_N
+<E_t,E_r,E_k> |- exp1 : t1 gives <S_N2,effects2,_>
+<E_t,E_r,E_k> |- exp2 : t2 gives <S_N3,effects3,_>
+------------------------------------------------------------ :: infix_app
+<E_t,E_r,E_k> |- :E_app_infix: exp1 id exp2 : t gives <S_N u+ S_N2 u+ S_N3, effects u+ effects2 u+ effects3,tag>
+
+E_r(</idi//i/>) gives id t_args, </ti//i/>
+</ <E_t,E_r,E_k> |- expi : ti gives Ii//i/>
+------------------------------------------------------------ :: record
+<E_t,E_r,E_k> |- { </idi = expi//i/> semi_opt} : id t_args gives u+ </Ii//i/>
+
+<E_t,E_r,E_k> |- exp : id t_args gives I
+E_r(id t_args) gives </ id'n:t'n//n/>
+</ <E_t,E_r,E_k> |- expi : ti gives Ii//i/>
+</idi:ti//i/> SUBSET </id'n : t'n//n/>
+------------------------------------------------------------ :: recup
+<E_t,E_r,E_k> |- { exp with </idi = expi//i/> semi_opt } : id t_args gives I
+
+E |- exp1 : t gives I1 ... E |- expn : t gives In
+length(exp1 ... expn) = num
+------------------------------------------------------------ :: vector
+E |- [ exp1 , ... , expn ] : vector zero num inc t gives I1 u+ ... u+ In
+ 
 %% % TD,E,E_l |- exp : __vector ne' t gives S_c,S_N
 %% % |- nexp ~> ne
 %% % ------------------------------------------------------------- :: vectorget
@@ -576,141 +535,53 @@ check_exp :: '' ::=
 %% % ne = :Ne_add: ne2 + (- ne1)
 %% % ------------------------------------------------------------- :: vectorsub
 %% % TD,E,E_l |- exp .( nexp1 .. nexp2 ) : __vector ne t gives S_c,S_N union {ne1 < ne2 < ne'}
-%% % 
-%% % E |- id field
-%% % TD,E |- field id : p t_args -> t gives (x of names)
-%% % TD,E,E_l |- exp : p t_args gives S_c,S_N
-%% % ------------------------------------------------------------ :: field
-%% % TD,E,E_l |- exp.id : t gives S_c,S_N
-%% % 
+
+E_r (id t_args) gives </idi : ti//i/> id : t </id'j : t'j//j/>
+<E_t,E_r,E_k> |- exp : id t_args gives I
+------------------------------------------------------------ :: field
+<E_t,E_r,E_k> |- exp.id : t gives Ir
+
 %% % </TD,E,E_l |- pati : t gives E_li//i/>
 %% % </TD,E,E_l u+ E_li |- expi : u gives S_ci,S_Ni//i/>
 %% % TD,E,E_l |- exp : t gives S_c',S_N'
 %% % ------------------------------------------------------------ :: case
 %% % TD,E,E_l |- match exp with bar_opt </pati -> expi li//i/> l end : u gives S_c' union </S_ci//i/>,S_N' union </S_Ni//i/>
-%% % 
-%% % TD,E,E_l |- exp : t gives S_c,S_N
-%% % TD,E |- typ ~> t
-%% % ------------------------------------------------------------ :: typed
-%% % TD,E,E_l |- (exp : typ) : t gives S_c,S_N
-%% % 
+
+<E_t,E_r,E_k> |- exp : t gives I
+E_k |- typ ~> t
+------------------------------------------------------------ :: typed
+<E_t,E_r,E_k> |- (typ) exp : t gives Ir
+
 %% % %KATHYCOMMENT: where does E_l1 come from?
 %% % TD,E,E_l1 |- letbind gives E_l2, S_c1,S_N1
 %% % TD,E,E_l1 u+ E_l2 |- exp : t gives S_c2,S_N2
 %% % ------------------------------------------------------------ :: let
 %% % TD,E,E_l |- let letbind in exp : t gives S_c1 union S_c2,S_N1 union S_N2
-%% % 
-%% % TD,E,E_l |- exp1 : t1 gives S_c1,S_N1 .... TD,E,E_l |- expn : tn gives S_cn,S_Nn
-%% % ------------------------------------------------------------ :: tup
-%% % TD,E,E_l |- (exp1, ...., expn) : t1 * .... * tn gives S_c1 union .... union S_cn,S_N1 union .... union S_Nn
-%% % 
-%% % TD |- t ok
-%% % TD,E,E_l |- exp1 : t gives S_c1,S_N1 .. TD,E,E_l |- expn : t gives S_cn,S_Nn
-%% % ------------------------------------------------------------ :: list
-%% % TD,E,E_l |- [exp1; ..; expn semi_opt] : __list t gives S_c1 union .. union S_cn, S_N1 union .. union S_Nn
-%% % 
-%% % TD,E,E_l |- exp : t gives S_c,S_N
-%% % ------------------------------------------------------------ :: paren
-%% % TD,E,E_l |- (exp) : t gives S_c,S_N
-%% % 
-%% % TD,E,E_l |- exp : t gives S_c,S_N
-%% % ------------------------------------------------------------ :: begin
-%% % TD,E,E_l |- begin exp end : t gives S_c,S_N
-%% % 
-%% % %TODO t might need different index constraints
-%% % TD,E,E_l |- exp1 : __bool gives S_c1,S_N1
-%% % TD,E,E_l |- exp2 : t gives S_c2,S_N2
-%% % TD,E,E_l |- exp3 : t gives S_c3,S_N3
-%% % ------------------------------------------------------------ :: if
-%% % TD,E,E_l |- if exp1 then exp2 else exp3 : t gives S_c1 union S_c2 union S_c3,S_N1 union S_N2 union S_N3
-%% % 
-%% % %TODO t might need different index constraints
-%% % TD,E,E_l |- exp1 : t gives S_c1,S_N1
-%% % TD,E,E_l |- exp2 : __list t gives S_c2,S_N2
-%% % ------------------------------------------------------------ :: cons
-%% % TD,E,E_l |- exp1 :: exp2 : __list t gives S_c1 union S_c2,S_N1 union S_N2
-%% % 
-%% % |- lit : t
-%% % ------------------------------------------------------------ :: lit
-%% % TD,E,E_l |- lit : t gives {},{}
-%% % 
-%% % % TODO: should require that each xi actually appears free in exp1
-%% % </TD |- ti ok//i/>
-%% % TD,E,E_l u+ {</xi|->ti//i/>} |- exp1 : t gives S_c1,S_N1
-%% % TD,E,E_l u+ {</xi|->ti//i/>} |- exp2 : __bool gives S_c2,S_N2
-%% % disjoint doms(E_l, {</xi|->ti//i/>})
-%% % E = <E_m,E_p,E_f,E_x>
-%% % </xi NOTIN dom(E_x)//i/>
-%% % ------------------------------------------------------------ :: set_comp
-%% % TD,E,E_l |- { exp1 | exp2 } : __set t gives S_c1 union S_c2,S_N1 union S_N2
-%% % 
-%% % TD,E,E_l1 |- </qbindi//i/> gives E_l2,S_c1
-%% % TD,E,E_l1 u+ E_l2 |- exp1 : t gives S_c2,S_N2
-%% % TD,E,E_l1 u+ E_l2 |- exp2 :  __bool gives S_c3,S_N3
-%% % ------------------------------------------------------------ :: set_comp_binding
-%% % TD,E,E_l1 |- { exp1 | forall </qbindi//i/> | exp2 } : __set t gives S_c1 union S_c2 union S_c3,S_N2 union S_N3
-%% % 
-%% % TD |- t ok
-%% % TD,E,E_l |- exp1 : t gives S_c1,S_N1 .. TD,E,E_l |- expn : t gives S_cn,S_Nn
-%% % ------------------------------------------------------------ :: set
-%% % TD,E,E_l |- { exp1; ..; expn semi_opt } : __set t gives S_c1 union .. union S_cn,S_N1 union .. union S_Nn
-%% % 
-%% % TD,E,E_l1 |- </qbindi//i/> gives E_l2,S_c1
-%% % TD,E,E_l1 u+ E_l2 |- exp : __bool gives S_c2,S_N2
-%% % ------------------------------------------------------------ :: quant
-%% % TD,E,E_l1 |- q </qbindi//i/> . exp : __bool gives S_c1 union S_c2,S_N2
-%% % 
-%% % TD,E,E_l1 |- list </qbindi//i/> gives E_l2,S_c1
-%% % TD,E,E_l1 u+ E_l2 |- exp1 : t gives S_c2,S_N2
-%% % TD,E,E_l1 u+ E_l2 |- exp2 : __bool gives S_c3,S_N3
-%% % ------------------------------------------------------------ :: list_comp_binding
-%% % TD,E,E_l1 |- [ exp1 | forall </qbindi//i/> | exp2 ] : __list t gives S_c1 union S_c2 union S_c3,S_N2 union S_N3
-%% % 
-%% % defn
-%% % TD , E , E_l1 |- qbind1 .. qbindn gives E_l2 , S_c :: :: check_listquant_binding
-%% % :: check_listquant_binding_
-%% % {{ com Build the environment for quantifier bindings, collecting typeclass constraints }}
-%% %  by
-%% % 
-%% % ------------------------------------------------------------ :: empty
-%% % TD,E,E_l |- gives {},{}
-%% % 
-%% % TD |- t ok
-%% % TD,E,E_l1 u+ {x |-> t} |- </qbindi//i/> gives E_l2,S_c1
-%% % disjoint doms({x |-> t}, E_l2)
-%% % ------------------------------------------------------------ :: var
-%% % TD,E,E_l1 |- x l </qbindi//i/> gives {x |-> t} u+ E_l2,S_c1
-%% % 
-%% % TD,E,E_l1 |- pat : t gives E_l3
-%% % TD,E,E_l1 |- exp : __set t gives S_c1,S_N1
-%% % TD,E,E_l1 u+ E_l3 |- </qbindi//i/> gives E_l2,S_c2
-%% % disjoint doms(E_l3, E_l2)
-%% % ------------------------------------------------------------ :: restr
-%% % TD,E,E_l1 |- (pat IN exp) </qbindi//i/> gives E_l2 u+ E_l3,S_c1 union S_c2
-%% % 
-%% % TD,E,E_l1 |- pat : t gives E_l3
-%% % TD,E,E_l1 |- exp : __list t gives S_c1,S_N1
-%% % TD,E,E_l1 u+ E_l3 |- </qbindi//i/> gives E_l2,S_c2
-%% % disjoint doms(E_l3, E_l2)
-%% % ------------------------------------------------------------ :: list_restr
-%% % TD,E,E_l1 |- (pat MEM exp) </qbindi//i/> gives E_l2 u+ E_l3,S_c1 union S_c2
-%% % 
-%% % defn
-%% % TD , E , E_l1 |- list qbind1 .. qbindn gives E_l2 , S_c :: :: check_quant_binding :: check_quant_binding_
-%% % {{ com Build the environment for quantifier bindings, collecting typeclass constraints }}
-%% %  by
-%% % 
-%% % ------------------------------------------------------------ :: empty
-%% % TD,E,E_l |- list gives {},{}
-%% % 
-%% % TD,E,E_l1 |- pat : t gives E_l3
-%% % TD,E,E_l1 |- exp : __list t gives S_c1,S_N1
-%% % TD,E,E_l1 u+ E_l3 |- </qbindi//i/> gives E_l2,S_c2
-%% % disjoint doms(E_l3, E_l2)
-%% % ------------------------------------------------------------ :: restr
-%% % TD,E,E_l1 |- list (pat MEM exp) </qbindi//i/> gives E_l2 u+ E_l3,S_c1 union S_c2
-%% % 
-%% % 
+ 
+E |- exp1 : t1 gives I1 .... E |- expn : tn gives In
+------------------------------------------------------------ :: tup
+E |- (exp1, .... , expn) : (t1 * .... * tn) gives I1 u+ .... u+ In
+ 
+E |- exp1 : t gives I1 .. E |- expn : t gives In
+------------------------------------------------------------ :: list
+E |- [|exp1, .., expn |] : list t gives I1 u+ .. u+ In
+
+E |- exp1 : bool gives I1
+E |- exp2 : t gives I2
+E |- exp3 : t gives I3
+------------------------------------------------------------ :: if
+E |- if exp1 then exp2 else exp3 : t gives I1 u+ I2 u+ I3
+
+E |- exp1 : t gives I1
+E |- exp2 : list t gives I2
+------------------------------------------------------------ :: cons
+E |- exp1 :: exp2 : list t gives I1 u+ I2
+
+|- lit : t
+------------------------------------------------------------ :: lit
+E |- lit : t gives Ie
+
+
 %% % defn
 %% % TD , E , E_l |- funcl gives { x |-> t } , S_c , S_N :: :: check_funcl :: check_funcl_
 %% % {{ com Build the environment for a function definition clause, collecting typeclass and index constraints }}