Syntax changes per discussion with Peter, as well as L2.ott document clean up.

Could not at this time return lists to [| |] from [|| ||] as the parser cannot distinguish a cast with enum’s syntactic sugar from the start of a parenthesised list (i.e. ( [|3|] ) And there are still conflicts with moving enums to [3], so those changes can’t be pushed in with current parser technology.

9 files changed, 270 insertions, 311 deletions

diff --git a/src/initial_check.ml b/src/initial_check.ml
index 18a853d9..ef80efcc 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -10,14 +10,14 @@ type 'a envs_out = 'a * envs
 let id_to_string (Id_aux(id,l)) =
   match id with | Id(x) | DeIid(x) -> x
 
-let var_to_string (Var_aux(Var v,l)) = v
+let var_to_string (Kid_aux(Var v,l)) = v
 
 (*placeholder, write in type_internal*)
 let kind_to_string kind = match kind.k with
   | K_Nat -> "Nat"
   | K_Typ -> "Type"
   | K_Ord -> "Order"
-  | K_Efct -> "Effects"
+  | K_Efct -> "Effect"
   | _ -> " kind pp place holder "
 
 let typquant_to_quantkinds k_env typquant = 
@@ -57,14 +57,14 @@ let to_ast_id (Parse_ast.Id_aux(id,l)) =
              | Parse_ast.Id(x) -> Id(x)
              | Parse_ast.DeIid(x) -> DeIid(x)) , l)
 
-let to_ast_var (Parse_ast.Var_aux(Parse_ast.Var v,l)) = Var_aux(Var v,l)
+let to_ast_var (Parse_ast.Kid_aux(Parse_ast.Var v,l)) = Kid_aux(Var v,l)
 
 let to_ast_base_kind (Parse_ast.BK_aux(k,l')) =
   match k with
   | Parse_ast.BK_type -> BK_aux(BK_type,l'), { k = K_Typ}
   | Parse_ast.BK_nat -> BK_aux(BK_nat,l'), { k = K_Nat }
   | Parse_ast.BK_order -> BK_aux(BK_order,l'), { k = K_Ord }
-  | Parse_ast.BK_effects -> BK_aux(BK_effects,l'), { k = K_Efct }
+  | Parse_ast.BK_effect -> BK_aux(BK_effect,l'), { k = K_Efct }
 
 let to_ast_kind (k_env : kind Envmap.t) (Parse_ast.K_aux(Parse_ast.K_kind(klst),l)) : (Ast.kind * kind) =
   match klst with
@@ -100,7 +100,6 @@ let rec to_ast_typ (k_env : kind Envmap.t) (t: Parse_ast.atyp) : Ast.typ =
                               | K_infer -> k.k <- K_Typ; Typ_var v
                               | _ -> typ_error l "Required a variable with kind Type, encountered " None (Some v) (Some k))
                 | None -> typ_error l "Encountered an unbound variable" None (Some v) None)
-              | Parse_ast.ATyp_wild -> Typ_wild
               | Parse_ast.ATyp_fn(arg,ret,efct) -> Typ_fn( (to_ast_typ k_env arg),
                                                            (to_ast_typ k_env ret),
                                                            (to_ast_effects k_env efct))
@@ -123,15 +122,6 @@ and to_ast_nexp (k_env : kind Envmap.t) (n: Parse_ast.atyp) : Ast.nexp =
   match n with
   | Parse_ast.ATyp_aux(t,l) ->
     (match t with
-    | Parse_ast.ATyp_id(id) ->                 
-                let id = to_ast_id id in
-                let mk = Envmap.apply k_env (id_to_string id) in
-                (match mk with
-                | Some(k) -> Nexp_aux((match k.k with
-                                      | K_Nat -> Nexp_id id
-                                      | K_infer -> k.k <- K_Nat; Nexp_id id
-                                      | _ -> typ_error l "Required a variable with kind Nat, encountered " (Some id) None (Some k)),l)
-                | None -> typ_error l "Encountered an unbound variable" (Some id) None None)
     | Parse_ast.ATyp_var(v) ->                 
                 let v = to_ast_var v in
                 let mk = Envmap.apply k_env (var_to_string v) in
@@ -163,15 +153,6 @@ and to_ast_order (k_env : kind Envmap.t) (o: Parse_ast.atyp) : Ast.order =
   match o with
   | Parse_ast.ATyp_aux(t,l) ->
     Ord_aux( (match t with
-               | Parse_ast.ATyp_id(id) -> 
-                let id = to_ast_id id in
-                let mk = Envmap.apply k_env (id_to_string id) in
-                (match mk with
-                | Some(k) -> (match k.k with
-                              | K_Ord -> Ord_id id
-                              | K_infer -> k.k <- K_Ord; Ord_id id
-                              | _ -> typ_error l "Required an identifier with kind Order, encountered " (Some id) None (Some k))
-                | None -> typ_error l "Encountered an unbound identifier" (Some id) None None)
                | Parse_ast.ATyp_var(v) -> 
                 let v = to_ast_var v in
                 let mk = Envmap.apply k_env (var_to_string v) in
@@ -186,40 +167,31 @@ and to_ast_order (k_env : kind Envmap.t) (o: Parse_ast.atyp) : Ast.order =
                | _ -> typ_error l "Requred an item of kind Order, encountered an illegal form for this kind" None None None
     ), l)
 
-and to_ast_effects (k_env : kind Envmap.t) (e : Parse_ast.atyp) : Ast.effects =
+and to_ast_effects (k_env : kind Envmap.t) (e : Parse_ast.atyp) : Ast.effect =
   match e with
   | Parse_ast.ATyp_aux(t,l) ->
-    Effects_aux( (match t with
-               | Parse_ast.ATyp_efid(id) ->  
-                let id = to_ast_id id in
-                let mk = Envmap.apply k_env (id_to_string id) in
-                (match mk with
-                | Some(k) -> (match k.k with
-                              | K_Efct -> Effects_id id
-                              | K_infer -> k.k <- K_Efct; Effects_id id
-                              | _ -> typ_error l "Required a variable with kind Effect, encountered " (Some id) None (Some k))
-                | None -> typ_error l "Encountered an unbound variable" (Some id) None None)
-               | Parse_ast.ATyp_efvar(v) ->  
+    Effect_aux( (match t with
+               | Parse_ast.ATyp_var(v) ->  
                 let v = to_ast_var v in
                 let mk = Envmap.apply k_env (var_to_string v) in
                 (match mk with
                 | Some(k) -> (match k.k with
-                              | K_Efct -> Effects_var v
-                              | K_infer -> k.k <- K_Efct; Effects_var v
+                              | K_Efct -> Effect_var v
+                              | K_infer -> k.k <- K_Efct; Effect_var v
                               | _ -> typ_error l "Required a variable with kind Effect, encountered " None (Some v) (Some k))
                 | None -> typ_error l "Encountered an unbound variable" None (Some v) None)
                | Parse_ast.ATyp_set(effects) ->
-                 Effects_set( List.map 
+                 Effect_set( List.map 
                              (fun efct -> match efct with
-                             | Parse_ast.Effect_aux(e,l) ->
-                               Effect_aux((match e with 
-                               | Parse_ast.Effect_rreg -> Effect_rreg
-                               | Parse_ast.Effect_wreg -> Effect_wreg
-                               | Parse_ast.Effect_rmem -> Effect_rmem
-                               | Parse_ast.Effect_wmem -> Effect_wmem
-                               | Parse_ast.Effect_undef -> Effect_undef
-                               | Parse_ast.Effect_unspec -> Effect_unspec
-                               | Parse_ast.Effect_nondet -> Effect_nondet),l))
+                             | Parse_ast.BE_aux(e,l) ->
+                               BE_aux((match e with 
+                               | Parse_ast.BE_rreg -> BE_rreg
+                               | Parse_ast.BE_wreg -> BE_wreg
+                               | Parse_ast.BE_rmem -> BE_rmem
+                               | Parse_ast.BE_wmem -> BE_wmem
+                               | Parse_ast.BE_undef -> BE_undef
+                               | Parse_ast.BE_unspec -> BE_unspec
+                               | Parse_ast.BE_nondet -> BE_nondet),l))
                              effects)
                | _ -> typ_error l "Required an item of kind Effects, encountered an illegal form for this kind" None None None
     ), l)
@@ -231,11 +203,11 @@ and to_ast_typ_arg (k_env : kind Envmap.t) (kind : kind) (arg : Parse_ast.atyp)
     | K_Typ -> Typ_arg_typ (to_ast_typ k_env arg)
     | K_Nat  -> Typ_arg_nexp (to_ast_nexp k_env arg)
     | K_Ord -> Typ_arg_order (to_ast_order k_env arg)
-    | K_Efct -> Typ_arg_effects (to_ast_effects k_env arg)
+    | K_Efct -> Typ_arg_effect (to_ast_effects k_env arg)
     | _ -> raise (Reporting_basic.err_unreachable l "To_ast_typ_arg received Lam kind or infer kind")),
     l)
 
-let to_ast_nexp_constraint (k_env : kind Envmap.t) (c : Parse_ast.nexp_constraint) : nexp_constraint =
+let to_ast_nexp_constraint (k_env : kind Envmap.t) (c : Parse_ast.n_constraint) : n_constraint =
   match c with 
   | Parse_ast.NC_aux(nc,l) ->
     NC_aux( (match nc with
@@ -252,7 +224,7 @@ let to_ast_nexp_constraint (k_env : kind Envmap.t) (c : Parse_ast.nexp_constrain
                let n2 = to_ast_nexp k_env t2 in
                NC_bounded_le(n1,n2)
              | Parse_ast.NC_nat_set_bounded(id,bounds) ->
-               NC_nat_set_bounded(to_ast_id id, bounds)
+               NC_nat_set_bounded(to_ast_var id, bounds)
     ), l)               
 
 (* Transforms a typquant while building first the kind environment of declared variables, and also the kind environment in context *)
@@ -398,9 +370,9 @@ and to_ast_lexp (k_env : kind Envmap.t) (Parse_ast.E_aux(exp,l) : Parse_ast.exp)
   LEXP_aux(
     (match exp with
     | Parse_ast.E_id(id) -> LEXP_id(to_ast_id id)
-    | Parse_ast.E_app((Parse_ast.Id_aux(f,l') as f'),[exp]) -> 
+    | Parse_ast.E_app((Parse_ast.Id_aux(f,l') as f'),args) -> 
       (match f with
-      | Parse_ast.Id(id) -> LEXP_memory(to_ast_id f',to_ast_exp k_env exp)
+      | Parse_ast.Id(id) -> LEXP_memory(to_ast_id f',List.map (to_ast_exp k_env) args)
       | _ -> typ_error l' "memory call on lefthand side of assignment must begin with an id" None None None)
     | Parse_ast.E_vector_access(vexp,exp) -> LEXP_vector(to_ast_lexp k_env vexp, to_ast_exp k_env exp)
     | Parse_ast.E_vector_subrange(vexp,exp1,exp2) -> LEXP_vector_range(to_ast_lexp k_env vexp, to_ast_exp k_env exp1, to_ast_exp k_env exp2)
@@ -442,7 +414,7 @@ and to_ast_record_try (k_env : kind Envmap.t) (Parse_ast.E_aux(exp,l) : Parse_as
   | _ ->
     None,Some(l, "Expected a field assignment to be identifier = expression")
       
-let to_ast_default (names, k_env, t_env) (default : Parse_ast.default_typing_spec) : (tannot default_typing_spec) envs_out =
+let to_ast_default (names, k_env, t_env) (default : Parse_ast.default_typing_spec) : (tannot default_spec) envs_out =
   match default with
   | Parse_ast.DT_aux(df,l) ->
     (match df with 
@@ -486,6 +458,11 @@ let rec to_ast_range (Parse_ast.BF_aux(r,l)) = (* TODO add check that ranges are
     | Parse_ast.BF_concat(ir1,ir2) -> BF_concat( to_ast_range ir1, to_ast_range ir2)),
     l)
 
+let to_ast_type_union k_env (Parse_ast.Tu_aux(tu,l)) =
+  match tu with
+    | Parse_ast.Tu_ty_id(atyp,id) -> (Tu_aux(Tu_ty_id ((to_ast_typ k_env atyp),(to_ast_id id)),l))
+    | Parse_ast.Tu_id id -> (Tu_aux(Tu_id(to_ast_id id),l)) 
+
 let to_ast_typedef (names,k_env,t_env) (td:Parse_ast.type_def) : (tannot type_def) envs_out =
   match td with
   | Parse_ast.TD_aux(td,l) ->
@@ -516,11 +493,7 @@ let to_ast_typedef (names,k_env,t_env) (td:Parse_ast.type_def) : (tannot type_de
     let id = to_ast_id id in
     let key = id_to_string id in
     let typq,k_env,_ = to_ast_typquant k_env typq in
-    let arms = List.map (fun (Parse_ast.Tu_aux(tu,l)) -> 
-                             match tu with
-                             | Parse_ast.Tu_ty_id(atyp,id) -> (Tu_aux(Tu_ty_id ((to_ast_typ k_env atyp),(to_ast_id id)),l))
-                             | Parse_ast.Tu_id id -> (Tu_aux(Tu_id(to_ast_id id),l)) ) 
-               arms in (* Add check that all arms have unique names *)
+    let arms = List.map (to_ast_type_union k_env) arms in (* Add check that all arms have unique names *)
     let td_var = TD_aux(TD_variant(id,to_ast_namescm name_scm_opt,typq,arms,false),(l,None)) in
     let typ = (match (typquant_to_quantkinds k_env typq) with
       | [ ] -> {k = K_Typ}
@@ -555,10 +528,10 @@ let to_ast_tannot_opt (k_env : kind Envmap.t) (Parse_ast.Typ_annot_opt_aux(tp,l)
     let typq,k_env,k_local = to_ast_typquant k_env tq in
     Typ_annot_opt_aux(Typ_annot_opt_some(typq,to_ast_typ k_env typ),(l,None)),k_env,k_local
 
-let to_ast_effects_opt (k_env : kind Envmap.t) (Parse_ast.Effects_opt_aux(e,l)) : tannot effects_opt =
+let to_ast_effects_opt (k_env : kind Envmap.t) (Parse_ast.Effect_opt_aux(e,l)) : tannot effect_opt =
   match e with
-  | Parse_ast.Effects_opt_pure -> Effects_opt_aux(Effects_opt_pure,(l,None))
-  | Parse_ast.Effects_opt_effects(typ) -> Effects_opt_aux(Effects_opt_effects(to_ast_effects k_env typ),(l,None))
+  | Parse_ast.Effect_opt_pure -> Effect_opt_aux(Effect_opt_pure,(l,None))
+  | Parse_ast.Effect_opt_effect(typ) -> Effect_opt_aux(Effect_opt_effect(to_ast_effects k_env typ),(l,None))
 
 let to_ast_funcl (names,k_env,t_env) (Parse_ast.FCL_aux(fcl,l) : Parse_ast.funcl) : (tannot funcl) =
   match fcl with
@@ -609,65 +582,65 @@ let to_ast_def (names, k_env, t_env) partial_defs def : def_progress envs_out *
       let t = to_ast_typ k_env typ in
       let id = to_ast_id id in
       ((Finished(DEF_aux(DEF_reg_dec(t,id),(l,None)))),envs),partial_defs (*If tracking types here, update tenv and None*)
-    | Parse_ast.DEF_scattered_function(rec_opt, tannot_opt, effects_opt, id) ->
-      let rec_opt = to_ast_rec rec_opt in
-      let tannot,k_env',k_local = to_ast_tannot_opt k_env tannot_opt in
-      let effects_opt = to_ast_effects_opt k_env' effects_opt in
-      let id = to_ast_id id in
-      (match (def_in_progress id partial_defs) with
-      | None -> let partial_def = ref ((DEF_aux(DEF_fundef(FD_aux(FD_function(rec_opt,tannot,effects_opt,[]),(l,None))),(l,None))),false) in
-                (No_def,envs),((id,(partial_def,k_local))::partial_defs)
-      | Some(d,k) -> typ_error l "Scattered function definition header name already in use by scattered definition" (Some id) None None)
-    | Parse_ast.DEF_scattered_funcl(funcl) -> 
-      (match funcl with
-      | Parse_ast.FCL_aux(Parse_ast.FCL_Funcl(id,_,_),_) -> 
-        let id = to_ast_id id in
-        (match (def_in_progress id partial_defs) with
-        | None -> typ_error l "Scattered function definition clause does not match any exisiting function definition headers" (Some id) None None
-        | Some(d,k) ->
-          (match !d with
-          | DEF_aux(DEF_fundef(FD_aux(FD_function(r,t,e,fcls),fl)),dl),false -> 
-            let funcl = to_ast_funcl (names,Envmap.union k k_env,t_env) funcl in 
-            d:= (DEF_aux(DEF_fundef(FD_aux(FD_function(r,t,e,fcls@[funcl]),fl)),dl),false);
-            (No_def,envs),partial_defs
-          | _,true -> typ_error l "Scattered funciton definition clauses extends ended defintion" (Some id) None None
-          | _ -> typ_error l "Scattered function definition clause matches an existing scattered type definition header" (Some id) None None)))
-    | Parse_ast.DEF_scattered_variant(id,naming_scheme_opt,typquant) -> 
-      let id = to_ast_id id in
-      let name = to_ast_namescm naming_scheme_opt in
-      let typq, k_env',_ = to_ast_typquant k_env typquant in
-      (match (def_in_progress id partial_defs) with
-      | None -> let partial_def = ref ((DEF_aux(DEF_type(TD_aux(TD_variant(id,name,typq,[],false),(l,None))),(l,None))),false) in
-                (Def_place_holder(id,l),envs),(id,(partial_def,k_env'))::partial_defs
-      | Some(d,k) -> typ_error l "Scattered type definition header name already in use by scattered definition" (Some id) None None)
-    | Parse_ast.DEF_scattered_unioncl(id,typ,arm_id) -> 
-      let id = to_ast_id id in
-      let arm_id = to_ast_id arm_id in
-      (match (def_in_progress id partial_defs) with
-      | None -> typ_error l "Scattered type definition clause does not match any existing type definition headers" (Some id) None None
-      | Some(d,k) ->
-        (match !d with
-        | (DEF_aux(DEF_type(TD_aux(TD_variant(id,name,typq,arms,false),tl)),dl), false) -> 
-          let typ = to_ast_typ k typ in
-          d:= (DEF_aux(DEF_type(TD_aux(TD_variant(id,name,typq,arms@[Tu_aux(Tu_ty_id (typ,arm_id), l)],false),tl)),dl),false);
-          (No_def,envs),partial_defs
-        | _,true -> typ_error l "Scattered type definition clause extends ended definition" (Some id) None None
-        | _ -> typ_error l "Scattered type definition clause matches an existing scattered function definition header" (Some id) None None))
-    | Parse_ast.DEF_scattered_end(id) ->
-      let id = to_ast_id id in
-      (match (def_in_progress id partial_defs) with
-      | None -> typ_error l "Scattered definition end does not match any open scattered definitions" (Some id) None None
-      | Some(d,k) ->
-        (match !d with
-        | (DEF_aux(DEF_type(_),_) as def),false ->
-          d:= (def,true);
-          (No_def,envs),partial_defs
-        | (DEF_aux(DEF_fundef(_),_) as def),false ->
-          d:= (def,true);
-          ((Finished def), envs),partial_defs
-        | _, true -> 
-          typ_error l "Scattered definition ended multiple times" (Some id) None None
-        | _ -> raise (Reporting_basic.err_unreachable l "Something in partial_defs other than fundef and type")))
+    | Parse_ast.DEF_scattered(Parse_ast.SD_aux(sd,_)) ->
+      (match sd with
+	| Parse_ast.SD_scattered_function(rec_opt, tannot_opt, effects_opt, id) ->
+	  let rec_opt = to_ast_rec rec_opt in
+	  let tannot,k_env',k_local = to_ast_tannot_opt k_env tannot_opt in
+	  let effects_opt = to_ast_effects_opt k_env' effects_opt in
+	  let id = to_ast_id id in
+	  (match (def_in_progress id partial_defs) with
+	    | None -> let partial_def = ref ((DEF_aux(DEF_fundef(FD_aux(FD_function(rec_opt,tannot,effects_opt,[]),(l,None))),(l,None))),false) in
+                      (No_def,envs),((id,(partial_def,k_local))::partial_defs)
+	    | Some(d,k) -> typ_error l "Scattered function definition header name already in use by scattered definition" (Some id) None None)
+	| Parse_ast.SD_scattered_funcl(funcl) -> 
+	  (match funcl with
+	    | Parse_ast.FCL_aux(Parse_ast.FCL_Funcl(id,_,_),_) -> 
+              let id = to_ast_id id in
+              (match (def_in_progress id partial_defs) with
+		| None -> typ_error l "Scattered function definition clause does not match any exisiting function definition headers" (Some id) None None
+		| Some(d,k) ->
+		  (match !d with
+		    | DEF_aux(DEF_fundef(FD_aux(FD_function(r,t,e,fcls),fl)),dl),false -> 
+		      let funcl = to_ast_funcl (names,Envmap.union k k_env,t_env) funcl in 
+		      d:= (DEF_aux(DEF_fundef(FD_aux(FD_function(r,t,e,fcls@[funcl]),fl)),dl),false);
+		      (No_def,envs),partial_defs
+		    | _,true -> typ_error l "Scattered funciton definition clauses extends ended defintion" (Some id) None None
+		    | _ -> typ_error l "Scattered function definition clause matches an existing scattered type definition header" (Some id) None None)))
+	| Parse_ast.SD_scattered_variant(id,naming_scheme_opt,typquant) -> 
+	  let id = to_ast_id id in
+	  let name = to_ast_namescm naming_scheme_opt in
+	  let typq, k_env',_ = to_ast_typquant k_env typquant in
+	  (match (def_in_progress id partial_defs) with
+	    | None -> let partial_def = ref ((DEF_aux(DEF_type(TD_aux(TD_variant(id,name,typq,[],false),(l,None))),(l,None))),false) in
+                      (Def_place_holder(id,l),envs),(id,(partial_def,k_env'))::partial_defs
+	    | Some(d,k) -> typ_error l "Scattered type definition header name already in use by scattered definition" (Some id) None None)
+	| Parse_ast.SD_scattered_unioncl(id,tu) -> 
+	  let id = to_ast_id id in
+	  (match (def_in_progress id partial_defs) with
+	    | None -> typ_error l "Scattered type definition clause does not match any existing type definition headers" (Some id) None None
+	    | Some(d,k) ->
+              (match !d with
+		| (DEF_aux(DEF_type(TD_aux(TD_variant(id,name,typq,arms,false),tl)),dl), false) -> 
+		  d:= (DEF_aux(DEF_type(TD_aux(TD_variant(id,name,typq,arms@[to_ast_type_union k tu],false),tl)),dl),false);
+		  (No_def,envs),partial_defs
+		| _,true -> typ_error l "Scattered type definition clause extends ended definition" (Some id) None None
+		| _ -> typ_error l "Scattered type definition clause matches an existing scattered function definition header" (Some id) None None))
+	| Parse_ast.SD_scattered_end(id) ->
+	  let id = to_ast_id id in
+	  (match (def_in_progress id partial_defs) with
+	    | None -> typ_error l "Scattered definition end does not match any open scattered definitions" (Some id) None None
+	    | Some(d,k) ->
+              (match !d with
+		| (DEF_aux(DEF_type(_),_) as def),false ->
+		  d:= (def,true);
+		  (No_def,envs),partial_defs
+		| (DEF_aux(DEF_fundef(_),_) as def),false ->
+		  d:= (def,true);
+		  ((Finished def), envs),partial_defs
+		| _, true -> 
+		  typ_error l "Scattered definition ended multiple times" (Some id) None None
+		| _ -> raise (Reporting_basic.err_unreachable l "Something in partial_defs other than fundef and type"))))
     )
 
 let rec to_ast_defs_helper envs partial_defs = function
diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem
index 640f6b1d..c0fec8a1 100644
--- a/src/lem_interp/interp.lem
+++ b/src/lem_interp/interp.lem
@@ -80,14 +80,14 @@ and to_reg_ranges base_id base_reg ranges =
   | (irange,id)::ranges -> (id,(SubReg base_id base_reg irange))::(to_reg_ranges base_id base_reg ranges)
   end
 
-val has_memory_effect : list efct -> bool
+val has_memory_effect : list base_effect -> bool
 let rec has_memory_effect efcts =
   match efcts with
   | [] -> false
   | e::efcts ->
     match e with
-    | Effect_wreg -> true
-    | Effect_wmem -> true
+    | BE_wreg -> true
+    | BE_wmem -> true
     | _ -> has_memory_effect efcts
     end 
   end
@@ -101,7 +101,7 @@ let rec to_memory_ops (Defs defs) =
     match def with
     | DEF_spec valsp ->
       match valsp with
-      | VS_val_spec (TypSchm_ts tq ((Typ_fn a r (Effects_set eff)) as t)) id ->
+      | VS_val_spec (TypSchm_ts tq ((Typ_fn a r (Effect_set eff)) as t)) id ->
         if has_memory_effect eff then (id,t)::(to_memory_ops (Defs defs)) else (to_memory_ops (Defs defs))
       | _ -> to_memory_ops (Defs defs) end
     | _ -> to_memory_ops (Defs defs) end
@@ -633,44 +633,35 @@ and interp_main t_level l_env l_mem exp =
                        (fun vals -> V_vector (List_extra.head indexes) true vals) (*Need to see increasing or not, can look at types later*) l_env l_mem [] exps
     | E_block(exps) -> interp_block t_level l_env l_env l_mem exps
     | E_app f args ->
-      match (f,t_level) with
-      | (id,(defs,externs,regs,mems,ctors)) -> 
-	(match find_function defs id with
-	| Just(funcls) -> 
-          resolve_outcome (interp_main t_level l_env l_mem (List_extra.head args))
-                          (fun argv lm le -> 
-                            (match find_funcl funcls argv with
-	                    | Nothing ->
-                          let name = match id with Id s -> s | DeIid s -> s end in
-                          (Error ("No matching pattern for function " (* XXX ^ name *)),lm,l_env)
-	                    | Just(env,exp) -> 
-                              resolve_outcome (interp_main t_level env lm exp)
-	                                      (fun ret lm le -> (Value ret, lm,l_env))
-                                              (fun a -> update_stack a (fun stack -> (Frame (Id "0") (E_id (Id "0")) l_env lm stack)))
-                             end))
-                          (fun a -> update_stack a (add_to_top_frame (fun a -> (E_app f [a]))))
-	| Nothing -> 
-          (match in_ctors ctors id with
-          | Just(typ) -> 
-            resolve_outcome (interp_main t_level l_env l_mem (List_extra.head args))
-                            (fun argv lm le -> (Value (V_ctor id argv), lm, le))
-                            (fun a -> update_stack a (add_to_top_frame (fun a -> (E_app f [a]))))
+      (match (exp_list t_level (fun es -> E_app f es) V_tuple l_env l_mem [] args) with
+      | (Value v,lm,le) -> 
+         (match (f,t_level) with
+      	 | (id,(defs,externs,regs,mems,ctors)) -> 
+	   (match find_function defs id with
+	   | Just(funcls) -> 
+             (match find_funcl funcls v with
+	     | Nothing -> 
+               let name = match id with Id s -> s | DeIid s -> s end in
+               (Error ("No matching pattern for function " (* XXX ^ name *)),l_mem,l_env)
+	     | Just(env,exp) -> 
+               resolve_outcome (interp_main t_level env l_mem exp)
+	                       (fun ret lm le -> (Value ret, lm,l_env))
+                               (fun a -> update_stack a (fun stack -> (Frame (Id "0") (E_id (Id "0")) l_env l_mem stack)))
+             end)
           | Nothing -> 
-            (match find_memory mems id with
-            | Just(typ) -> 
-              resolve_outcome (interp_main t_level l_env l_mem (List_extra.head args))
-                (fun argv lm le -> (Action (Read_mem id argv Nothing) (Frame (Id "0") (E_id (Id "0")) le lm Top), lm, le))
-                (fun a -> update_stack a (add_to_top_frame (fun a -> (E_app f [a]))))
+            (match in_ctors ctors id with
+            | Just(typ) -> (Value (V_ctor id v), lm, le)
             | Nothing -> 
-              (match find_extern externs id with
-              | Just(str) ->
-                resolve_outcome (interp_main t_level l_env l_mem (List_extra.head args))
-                  (fun argv lm le -> (Action (Call_extern str argv) (Frame (Id "0") (E_id (Id "0")) le lm Top), lm, le))
-                  (fun a -> update_stack a (add_to_top_frame (fun a -> (E_app f [a]))))
-              | Nothing -> (Error "Unknown function call",l_mem,l_env) end)
-	     end) end) end)
-      | _ -> (Error "Application with expression other than identifier",l_mem,l_env)
-      end 
+              (match find_memory mems id with
+              | Just(typ) -> 
+                (Action (Read_mem id v Nothing) (Frame (Id "0") (E_id (Id "0")) le lm Top), lm, le)
+              | Nothing -> 
+                (match find_extern externs id with
+                | Just(str) -> 
+                  (Action (Call_extern str v) (Frame (Id "0") (E_id (Id "0")) le lm Top), lm, le)
+                | Nothing -> (Error "Unknown function call",lm,le) end)
+	       end) end) end) end)
+         | out -> out end)
     | E_app_infix l op r -> 
        let op = match op with
        | Id x -> DeIid x
@@ -751,12 +742,12 @@ and create_write_message_or_update t_level value l_env l_mem is_top_level lexp =
           else ((Error "Undefined id",l_mem,l_env),Nothing)
         end
       end 
-    | LEXP_memory id exp -> 
-      match (interp_main t_level l_env l_mem exp) with
-      | (Value t,lm,le) ->
-        let request = (Action (Write_mem id t Nothing value) (Frame (Id "0") (E_id (Id "0")) l_env lm Top),lm,l_env) in
-        if is_top_level then (request,Nothing) else (request,Just (fun e -> (LEXP_memory id (to_exp t))))
-      | (Action a s,lm, le) -> ((Action a s,lm,le), Just (fun e -> (LEXP_memory id e)))
+    | LEXP_memory id exps -> 
+      match (exp_list t_level E_tuple V_tuple l_env l_mem [] exps) with
+      | (Value (V_tuple vs),lm,le) ->
+        let request = (Action (Write_mem id (V_tuple vs) Nothing value) (Frame (Id "0") (E_id (Id "0")) l_env lm Top),lm,l_env) in
+        if is_top_level then (request,Nothing) else (request,Just (fun e -> (LEXP_memory id (List.map to_exp vs))))
+      | (Action a s,lm, le) -> ((Action a s,lm,le), Just (fun (E_tuple es) -> (LEXP_memory id es)))
       | e -> (e,Nothing) end
     | LEXP_vector lexp exp -> 
       match (interp_main t_level l_env l_mem exp) with
diff --git a/src/lexer.mll b/src/lexer.mll
index 80fd06f4..620ca7a5 100644
--- a/src/lexer.mll
+++ b/src/lexer.mll
@@ -68,7 +68,7 @@ let kw_table =
      ("default",		 (fun _ -> Default));
      ("deinfix",                 (fun _ -> Deinfix));
      ("effect",                  (fun _ -> Effect));
-     ("Effects",                 (fun _ -> Effects));
+     ("Effect",                 (fun _ -> EFFECT));
      ("end",                     (fun _ -> End));
      ("enumerate",		 (fun _ -> Enumerate));
      ("else",                    (fun _ -> Else));
@@ -106,6 +106,15 @@ let kw_table =
      ("OR",			 (fun x -> OR));
      ("quot",			 (fun x -> Quot));
      ("rem",			 (fun x -> Rem));
+
+     ("rreg",                    (fun x -> Rreg));
+     ("wreg",                    (fun x -> Wreg));
+     ("rmem",                    (fun x -> Rmem));
+     ("wmem",                    (fun x -> Wmem));
+     ("undef",                   (fun x -> Undef));
+     ("unspec",                  (fun x -> Unspec));
+     ("nondet",                  (fun x -> Nondet));
+
 ]
 
 let type_names : string list ref = ref []
diff --git a/src/parser.mly b/src/parser.mly
index 4050885f..6ef0a91e 100644
--- a/src/parser.mly
+++ b/src/parser.mly
@@ -55,6 +55,8 @@ let locn m n = Range(Parsing.rhs_start_pos m,Parsing.rhs_end_pos n)
 
 let idl i = Id_aux(i, loc())
 
+let efl e = BE_aux(e, loc())
+
 let ploc p = P_aux(p,loc ())
 let eloc e = E_aux(e,loc ())
 let peloc pe = Pat_aux(pe,loc ())
@@ -76,6 +78,7 @@ let defloc df = DT_aux(df, loc())
 let tdloc td = TD_aux(td, loc())
 let funloc fn = FD_aux(fn, loc())
 let vloc v = VS_aux(v, loc ())
+let sdloc sd = SD_aux(sd, loc ())
 let dloc d = DEF_aux(d,loc ())
 
 let mk_typschm tq t s e = TypSchm_aux((TypSchm_ts(tq,t)),(locn s e))
@@ -84,8 +87,8 @@ let mk_recn _ = (Rec_aux((Rec_nonrec), Unknown))
 let mk_typqn _ = (TypQ_aux(TypQ_no_forall,Unknown))
 let mk_tannot tq t s e = Typ_annot_opt_aux(Typ_annot_opt_some(tq,t),(locn s e))
 let mk_tannotn _ = Typ_annot_opt_aux(Typ_annot_opt_none,Unknown)
-let mk_eannot e i = Effects_opt_aux((Effects_opt_effects(e)),(locn i i))
-let mk_eannotn _ = Effects_opt_aux(Effects_opt_pure,Unknown)
+let mk_eannot e i = Effect_opt_aux((Effect_opt_effect(e)),(locn i i))
+let mk_eannotn _ = Effect_opt_aux(Effect_opt_pure,Unknown)
 let mk_namesectn _ = Name_sect_aux(Name_sect_none,Unknown)
 
 let make_enum_sugar_bounded typ1 typ2 =
@@ -120,8 +123,9 @@ let star = "*"
 
 /*Terminals with no content*/
 
-%token And As Bits By Case Clause Const Dec Default Deinfix Effect Effects End Enumerate Else Extern
+%token And As Bits By Case Clause Const Dec Default Deinfix Effect EFFECT End Enumerate Else Extern
 %token False Forall Foreach Function_ If_ In IN Inc Let_ Member Nat Order Pure Rec Register
+%token Rreg Wreg Rmem Wmem Undef Unspec Nondet
 %token Scattered Struct Switch Then True TwoStarStar Type TYPE Typedef Undefined Union With Val
 
 /* Avoid shift/reduce conflict - see right_atomic_exp rule */
@@ -246,7 +250,7 @@ tid:
 
 tyvar:
   | TyVar
-    { (Var_aux((Var($1)),loc ())) }
+    { (Kid_aux((Var($1)),loc ())) }
 
 atomic_kind:
   | TYPE
@@ -255,8 +259,8 @@ atomic_kind:
     { bkloc BK_nat }
   | Order
     { bkloc BK_order }
-  | Effects
-    { bkloc BK_effects }
+  | EFFECT
+    { bkloc BK_effect }
 
 kind_help:
   | atomic_kind
@@ -269,20 +273,20 @@ kind:
     { K_aux(K_kind($1), loc ()) }
 
 effect:
-  | id
-    { (match $1 with
-       | Id_aux(Id(s),l) ->
-	 Effect_aux
-	   ((match s with
-	   | "rreg" -> (Effect_rreg)
-	   | "wreg" -> (Effect_wreg)
-	   | "rmem" -> (Effect_rmem)
-	   | "wmem" -> (Effect_wmem)
-	   | "undef" -> (Effect_undef)
-	   | "unspec" -> (Effect_unspec)
-	   | "nondet" -> (Effect_nondet)
-	   | _ -> raise (Parse_error_locn (l,"Invalid effect"))),l)
-       | _ -> raise (Parse_error_locn ((loc ()),"Invalid effect"))) }
+  | Rreg 
+    { efl BE_rreg }
+  | Wreg
+    { efl BE_wreg }
+  | Rmem
+    { efl BE_rmem } 
+  | Wmem
+    { efl BE_wmem }
+  | Undef
+    { efl BE_undef }
+  | Unspec
+    { efl BE_unspec }
+  | Nondet
+    { efl BE_nondet }
 
 effect_list:
   | effect
@@ -291,10 +295,8 @@ effect_list:
     { $1::$3 }
 
 effect_typ:
-  | Effect tid
-    { tloc (ATyp_efid($2)) }
-  | Effect Lcurly effect_list Rcurly
-    { tloc (ATyp_set($3)) }
+  | Lcurly effect_list Rcurly
+    { tloc (ATyp_set($2)) }
   | Pure
     { tloc (ATyp_set([])) }
 
@@ -329,14 +331,10 @@ vec_typ:
       { tloc (make_vector_sugar_bounded (ATyp_aux ((ATyp_var $1), locn 1 1)) $3 $5) }
 
 app_typs:
-  | vec_typ
+  | nexp_typ
     { [$1] }
-  | Num
-    { [tloc (ATyp_constant $1)] }
-  | Num app_typs
-    { (ATyp_aux((ATyp_constant $1),locn 1 1))::$2 }
-  | vec_typ app_typs
-    { $1::$2 }
+  | nexp_typ Comma app_typs
+    { $1::$3 }
 
 app_typ:
   | vec_typ
@@ -376,8 +374,8 @@ nexp_typ:
 typ:
   | star_typ
     { $1 }
-  | star_typ MinusGt typ effect_typ
-    { tloc (ATyp_fn($1,$3,$4)) }
+  | star_typ MinusGt typ Effect effect_typ
+    { tloc (ATyp_fn($1,$3,$5)) }
 
 lit:
   | True
@@ -852,33 +850,29 @@ funcl_ands:
 
 /* This causes ambiguity because without a type quantifier it's unclear whether the first id is a function name or a type name for the optional types.*/
 fun_def:
-  | Function_ Rec typquant typ effect_typ funcl_ands
-    { funloc (FD_function(mk_rec 2, mk_tannot $3 $4 3 4, mk_eannot $5 5, $6)) }
+  | Function_ Rec typquant typ Effect effect_typ funcl_ands
+    { funloc (FD_function(mk_rec 2, mk_tannot $3 $4 3 4, mk_eannot $6 6, $7)) }
   | Function_ Rec typquant typ funcl_ands
     { funloc (FD_function(mk_rec 2, mk_tannot $3 $4 3 4, mk_eannotn (), $5)) }
-  | Function_ Rec typ effect_typ funcl_ands
-    { funloc (FD_function(mk_rec 2, mk_tannot (mk_typqn ()) $3 3 3, mk_eannot $4 4, $5)) }
+  | Function_ Rec typ Effect effect_typ funcl_ands
+    { funloc (FD_function(mk_rec 2, mk_tannot (mk_typqn ()) $3 3 3, mk_eannot $5 5, $6)) }
+  | Function_ Rec Effect effect_typ funcl_ands 
+    { funloc (FD_function(mk_rec 2,mk_tannotn (), mk_eannot $4 4, $5)) }
   | Function_ Rec typ funcl_ands
-    { match $3 with
-      | ATyp_aux(ATyp_efid _, _) | ATyp_aux(ATyp_set _, _) ->
-        funloc (FD_function(mk_rec 2,mk_tannotn (), mk_eannot $3 3, $4))
-      | _ ->
-        funloc (FD_function(mk_rec 2,mk_tannot (mk_typqn ()) $3 3 3, mk_eannotn (), $4)) }
-/*  | Function_ Rec funcl_ands
+    { funloc (FD_function(mk_rec 2,mk_tannot (mk_typqn ()) $3 3 3, mk_eannotn (), $4)) }
+  | Function_ Rec funcl_ands
     { funloc (FD_function(mk_rec 2, mk_tannotn (), mk_eannotn (), $3)) }
-*/  | Function_ typquant atomic_typ effect_typ funcl_ands
+  | Function_ typquant atomic_typ effect_typ funcl_ands
     { funloc (FD_function(mk_recn (), mk_tannot $2 $3 2 3, mk_eannot $4 4, $5)) }
   | Function_ typquant typ funcl_ands
     { funloc (FD_function(mk_recn (), mk_tannot $2 $3 2 2, mk_eannotn (), $4)) }
+  | Function_ Effect effect_typ funcl_ands
+    { funloc (FD_function(mk_recn (),mk_tannotn (), mk_eannot $3 3, $4)) }
   | Function_ typ funcl_ands
-    { match $2 with
-      | ATyp_aux(ATyp_efid _, _) | ATyp_aux(ATyp_set _, _) ->
-        funloc (FD_function(mk_recn (),mk_tannotn (), mk_eannot $2 2, $3))
-      | _ ->
-        funloc (FD_function(mk_recn (),mk_tannot (mk_typqn ()) $2 2 2, mk_eannotn (), $3)) }
-/*  | Function_ funcl_ands
+    { funloc (FD_function(mk_recn (),mk_tannot (mk_typqn ()) $2 2 2, mk_eannotn (), $3)) }
+  | Function_ funcl_ands
     { funloc (FD_function(mk_recn (), mk_tannotn (), mk_eannotn (), $2)) }
-*/
+
 
 val_spec:
   | Val typquant typ id
@@ -919,7 +913,7 @@ nexp_constraint:
     { NC_aux(NC_bounded_ge($1,$3), loc () ) }
   | typ LtEq typ
     { NC_aux(NC_bounded_le($1,$3), loc () ) }
-  | id IN Lcurly nums Rcurly
+  | tyvar IN Lcurly nums Rcurly
     { NC_aux(NC_nat_set_bounded($1,$4), loc ()) }
 
 id_constraint:
@@ -1041,42 +1035,38 @@ default_typ:
     { defloc (DT_typ((mk_typschm (mk_typqn ()) $2 2 2),$3)) }
 
 scattered_def:
-  | Function_ Rec typquant typ effect_typ id
-    { (DEF_scattered_function(mk_rec 2, mk_tannot $3 $4 3 4, mk_eannot $5 5, $6)) }
-  | Function_ Rec typ effect_typ id
-    { (DEF_scattered_function(mk_rec 2, mk_tannot (mk_typqn ()) $3 3 3, mk_eannot $4 4, $5)) }
+  | Function_ Rec typquant typ Effect effect_typ id
+    { sdloc (SD_scattered_function(mk_rec 2, mk_tannot $3 $4 3 4, mk_eannot $6 6, $7)) }
+  | Function_ Rec typ Effect effect_typ id
+    { sdloc (SD_scattered_function(mk_rec 2, mk_tannot (mk_typqn ()) $3 3 3, mk_eannot $5 5, $6)) }
   | Function_ Rec typquant typ id
-    { (DEF_scattered_function(mk_rec 2, mk_tannot $3 $4 3 4, mk_eannotn (), $5)) }
+    { sdloc (SD_scattered_function(mk_rec 2, mk_tannot $3 $4 3 4, mk_eannotn (), $5)) }
+  | Function_ Rec Effect effect_typ id
+    { sdloc (SD_scattered_function (mk_rec 2, mk_tannotn (), mk_eannot $4 4, $5)) }
   | Function_ Rec typ id
-    { match $3 with
-      | (ATyp_aux(ATyp_efid _, _)) | (ATyp_aux(ATyp_set _, _)) ->
-        (DEF_scattered_function(mk_rec 2, mk_tannotn (), mk_eannot $3 3, $4))
-      | _ ->
-        (DEF_scattered_function(mk_rec 2,mk_tannot (mk_typqn ()) $3 3 3, mk_eannotn (), $4)) }
+    { sdloc (SD_scattered_function(mk_rec 2,mk_tannot (mk_typqn ()) $3 3 3, mk_eannotn (), $4)) }
   | Function_ Rec id
-    { (DEF_scattered_function(mk_rec 2,mk_tannotn (), mk_eannotn (),$3)) }
-  | Function_ typquant typ effect_typ id
-    { (DEF_scattered_function(mk_recn (),mk_tannot $2 $3 2 3, mk_eannot $4 4, $5)) }
-  | Function_ typ effect_typ id
-    { (DEF_scattered_function(mk_recn (), mk_tannot (mk_typqn ()) $2 2 2, mk_eannot $3 3, $4)) }
+    { sdloc (SD_scattered_function(mk_rec 2,mk_tannotn (), mk_eannotn (),$3)) }
+  | Function_ typquant typ Effect effect_typ id
+    { sdloc (SD_scattered_function(mk_recn (),mk_tannot $2 $3 2 3, mk_eannot $5 5, $6)) }
+  | Function_ typ Effect effect_typ id
+    { sdloc (SD_scattered_function(mk_recn (), mk_tannot (mk_typqn ()) $2 2 2, mk_eannot $4 4, $5)) }
   | Function_ typquant typ id
-    { (DEF_scattered_function(mk_recn (), mk_tannot $2 $3 2 3, mk_eannotn (), $4)) }
+    { sdloc (SD_scattered_function(mk_recn (), mk_tannot $2 $3 2 3, mk_eannotn (), $4)) }
+  | Function_ Effect effect_typ id
+    { sdloc (SD_scattered_function(mk_recn (), mk_tannotn (), mk_eannot $3 3, $4)) }
   | Function_ typ id
-    { match $2 with
-      | (ATyp_aux(ATyp_efid _, _)) | (ATyp_aux(ATyp_set _, _)) ->
-        (DEF_scattered_function(mk_recn (), mk_tannotn (), mk_eannot $2 2, $3))
-      | _ ->
-        (DEF_scattered_function(mk_recn (), mk_tannot (mk_typqn ()) $2 2 2, mk_eannotn (), $3)) }
+    { sdloc (SD_scattered_function(mk_recn (), mk_tannot (mk_typqn ()) $2 2 2, mk_eannotn (), $3)) }
   | Function_ id
-    { (DEF_scattered_function(mk_recn (), mk_tannotn (), mk_eannotn (), $2)) }
+    { sdloc (SD_scattered_function(mk_recn (), mk_tannotn (), mk_eannotn (), $2)) }
   | Typedef id name_sect Eq Const Union typquant
-    { (DEF_scattered_variant($2,$3,$7)) }
+    { sdloc (SD_scattered_variant($2,$3,$7)) }
   | Typedef id Eq Const Union typquant
-    { (DEF_scattered_variant($2,(mk_namesectn ()),$6)) }
+    { sdloc (SD_scattered_variant($2,(mk_namesectn ()),$6)) }
   | Typedef id name_sect Eq Const Union
-    { (DEF_scattered_variant($2,$3,mk_typqn ())) }
+    { sdloc (SD_scattered_variant($2,$3,mk_typqn ())) }
   | Typedef id Eq Const Union
-    { (DEF_scattered_variant($2,mk_namesectn (),mk_typqn ())) }
+    { sdloc (SD_scattered_variant($2,mk_namesectn (),mk_typqn ())) }
 
 def:
   | type_def
@@ -1092,13 +1082,15 @@ def:
   | Register atomic_typ id
     { dloc (DEF_reg_dec($2,$3)) }
   | Scattered scattered_def
-    { dloc $2 }
+    { dloc (DEF_scattered $2) }
   | Function_ Clause funcl
-    { dloc (DEF_scattered_funcl($3)) }
-  | Union id Member atomic_typ id
-    { dloc (DEF_scattered_unioncl($2,$4,$5)) }
+    { dloc (DEF_scattered (sdloc (SD_scattered_funcl($3)))) }
+  | Union id Member typ id
+    { dloc (DEF_scattered (sdloc (SD_scattered_unioncl($2,Tu_aux(Tu_ty_id($4,$5), locn 4 5))))) }
+  | Union id Member id
+    { dloc (DEF_scattered (sdloc (SD_scattered_unioncl($2,Tu_aux(Tu_id($4), locn 4 4))))) }
   | End id
-    { dloc (DEF_scattered_end($2)) }
+    { dloc (DEF_scattered (sdloc (SD_scattered_end($2)))) }
 
 defs_help:
   | def
diff --git a/src/pretty_print.ml b/src/pretty_print.ml
index 083bd087..a32db3b1 100644
--- a/src/pretty_print.ml
+++ b/src/pretty_print.ml
@@ -3,11 +3,11 @@ open Format
 
 let is_atomic_typ (Typ_aux(t,_)) =
   match t with
-  | Typ_var _ | Typ_tup _ -> true
+  | Typ_id _ | Typ_var _ | Typ_tup _ -> true
   | _ -> false
 let is_atomic_nexp (Nexp_aux(n,_)) =
   match n with
-  | Nexp_id _ | Nexp_constant _ | Nexp_exp _ -> true
+  | Nexp_var _ | Nexp_constant _ | Nexp_exp _ -> true
   | _ -> false
  
 let is_atomic_pat (P_aux(p,l)) =
@@ -54,7 +54,7 @@ let pp_format_id (Id_aux(i,_)) =
 
 let pp_id ppf id = base ppf (pp_format_id id)
 
-let pp_format_var (Var_aux(Var v,_)) = "'" ^ v
+let pp_format_var (Kid_aux(Var v,_)) = "'" ^ v
 
 let pp_var ppf var = base ppf (pp_format_var var)
 
@@ -63,7 +63,7 @@ let pp_format_bkind (BK_aux(k,_)) =
   | BK_type -> "Type"
   | BK_nat -> "Nat"
   | BK_order -> "Order"
-  | BK_effects -> "Effects"
+  | BK_effect -> "Effect"
 
 let pp_bkind ppf bk = base ppf (pp_format_bkind bk)
 
@@ -78,13 +78,12 @@ let rec pp_format_typ (Typ_aux(t,_)) =
   | Typ_var(var) -> pp_format_var var
   | Typ_wild -> "_"
   | Typ_fn(arg,ret,efct) -> "(" ^ (parens is_atomic_typ pp_format_typ arg) ^ " -> " ^ 
-                            (parens is_atomic_typ pp_format_typ ret) ^ " " ^
+                            (parens is_atomic_typ pp_format_typ ret) ^ " effect " ^ 
                             (pp_format_effects efct) ^ ")"
   | Typ_tup(typs) -> "(" ^ (list_format " * " pp_format_typ typs) ^ ")"
-  | Typ_app(id,args) -> "(" ^ (pp_format_id id) ^ " " ^ (list_format " " pp_format_typ_arg args) ^ ")"
+  | Typ_app(id,args) -> "(" ^ (pp_format_id id) ^ "<" ^ (list_format ", " pp_format_typ_arg args) ^ ">)"
 and pp_format_nexp (Nexp_aux(n,_)) = 
   match n with
-  | Nexp_id(id) -> pp_format_id id
   | Nexp_var(var) -> pp_format_var var
   | Nexp_constant(i) -> string_of_int i
   | Nexp_sum(n1,n2) -> "(" ^ (pp_format_nexp n1) ^ " + " ^ (pp_format_nexp n2) ^ ")"
@@ -92,35 +91,33 @@ and pp_format_nexp (Nexp_aux(n,_)) =
   | Nexp_exp(n1) -> "2** (" ^ (pp_format_nexp n1) ^ ")"
 and pp_format_ord (Ord_aux(o,_)) = 
   match o with
-  | Ord_id(id) -> pp_format_id id
   | Ord_var(var) -> pp_format_var var
   | Ord_inc -> "inc"
   | Ord_dec -> "dec"  
-and pp_format_effects (Effects_aux(e,_)) =
+and pp_format_effects (Effect_aux(e,_)) =
   match e with
-  | Effects_id(id) -> "effect " ^ pp_format_id id
-  | Effects_var(var) -> "effect " ^ pp_format_var var
-  | Effects_set(efcts) ->
+  | Effect_var(var) -> pp_format_var var
+  | Effect_set(efcts) ->
     if (efcts = []) 
     then "pure"
-    else "effect {" ^
+    else "{" ^
       (list_format "," 
-         (fun (Effect_aux(e,l)) ->
+         (fun (BE_aux(e,l)) ->
 	   match e with
-	   | Effect_rreg -> "rreg"
-	   | Effect_wreg -> "wreg"
-	   | Effect_rmem -> "rmem"
-	   | Effect_wmem -> "wmem"
-	   | Effect_undef -> "undef"
-	   | Effect_unspec -> "unspec"
-	   | Effect_nondet -> "nondet")
+	   | BE_rreg -> "rreg"
+	   | BE_wreg -> "wreg"
+	   | BE_rmem -> "rmem"
+	   | BE_wmem -> "wmem"
+	   | BE_undef -> "undef"
+	   | BE_unspec -> "unspec"
+	   | BE_nondet -> "nondet")
 	 efcts) ^ " }"
 and pp_format_typ_arg (Typ_arg_aux(t,_)) = 
   match t with
   | Typ_arg_typ(t) -> pp_format_typ t
   | Typ_arg_nexp(n) -> pp_format_nexp n
   | Typ_arg_order(o) -> pp_format_ord o
-  | Typ_arg_effects(e) -> pp_format_effects e
+  | Typ_arg_effect(e) -> pp_format_effects e
 
 let pp_typ ppf t = base ppf (pp_format_typ t)
 let pp_nexp ppf n = base ppf (pp_format_nexp n)
@@ -132,8 +129,8 @@ let pp_format_nexp_constraint (NC_aux(nc,_)) =
   | NC_fixed(n1,n2) -> pp_format_nexp n1 ^ " = " ^ pp_format_nexp n2
   | NC_bounded_ge(n1,n2) -> pp_format_nexp n1 ^ " >= " ^ pp_format_nexp n2
   | NC_bounded_le(n1,n2) -> pp_format_nexp n1 ^ " <= " ^ pp_format_nexp n2
-  | NC_nat_set_bounded(id,bounds) -> 
-    pp_format_id id ^
+  | NC_nat_set_bounded(var,bounds) -> 
+    pp_format_var var ^
       " In {" ^
       list_format ", " string_of_int bounds ^
       "}"
@@ -185,7 +182,7 @@ let rec pp_format_pat (P_aux(p,l)) =
   | P_wild -> "_"
   | P_id(id) -> pp_format_id id
   | P_as(pat,id) -> "(" ^ pp_format_pat pat ^ " as " ^ pp_format_id id ^ ")"
-  | P_typ(typ,pat) -> "<" ^ pp_format_typ typ ^ "> " ^ pp_format_pat pat
+  | P_typ(typ,pat) -> "(" ^ pp_format_typ typ ^ ") " ^ pp_format_pat pat
   | P_app(id,pats) -> if (pats = [])
                       then pp_format_id id 
                       else pp_format_id id ^ "(" ^
@@ -199,7 +196,7 @@ let rec pp_format_pat (P_aux(p,l)) =
     "[" ^ list_format "; " (fun (i,p) -> string_of_int i ^ " = " ^ pp_format_pat p) ipats ^ "]"
   | P_vector_concat(pats) -> list_format " ^ " pp_format_pat pats
   | P_tup(pats) -> "(" ^ (list_format ", " (parens is_atomic_pat pp_format_pat) pats) ^ ")"
-  | P_list(pats) -> "[|" ^ (list_format "; " (parens is_atomic_pat pp_format_pat) pats) ^ "|]"
+  | P_list(pats) -> "[||" ^ (list_format "; " (parens is_atomic_pat pp_format_pat) pats) ^ "||]"
 
 let pp_pat ppf p = base ppf (pp_format_pat p)
 let pp_pat_atomic ppf p = base ppf (parens is_atomic_pat pp_format_pat p)
@@ -218,8 +215,8 @@ and pp_exp ppf (E_aux(e,_)) =
                                  kwd "}"
   | E_id(id) -> pp_id ppf id
   | E_lit(lit) -> pp_lit ppf lit
-  | E_cast(typ,exp) -> fprintf ppf "@[<0>%a%a%a %a@]" kwd "<" pp_typ typ kwd ">" pp_exp exp 
-  | E_app(f,args) -> fprintf ppf "@[<0>%a %a@]" pp_id f (list_pp pp_exp pp_exp) args
+  | E_cast(typ,exp) -> fprintf ppf "@[<0>%a%a%a %a@]" kwd "(" pp_typ typ kwd ")" pp_exp exp 
+  | E_app(f,args) -> fprintf ppf "@[<0>%a(%a)@]" pp_id f (list_pp pp_exp pp_exp) args 
   | E_app_infix(l,op,r) -> fprintf ppf "@[<0>%a %a %a@]" pp_exp l pp_id op pp_exp r
   | E_tuple(exps) -> fprintf ppf "@[<0>%a %a %a@]" kwd "(" (list_pp pp_comma_exp pp_exp) exps kwd ")"
   | E_if(c,t,e) -> fprintf ppf "@[<0> %a %a @[<1> %a %a@] @[<1> %a@ %a@]@]" kwd "if " pp_exp c kwd "then" pp_exp t kwd "else" pp_exp e
@@ -260,7 +257,7 @@ and pp_case ppf (Pat_aux(Pat_exp(pat,exp),_)) =
 and pp_lexp ppf (LEXP_aux(lexp,_)) =
   match lexp with
   | LEXP_id(id) -> pp_id ppf id
-  | LEXP_memory(id,exp) -> fprintf ppf "@[%a %a@]" pp_id id pp_exp exp
+  | LEXP_memory(id,args) -> fprintf ppf "@[%a(%a)@]" pp_id id (list_pp pp_exp pp_exp) args
   | LEXP_vector(v,exp) -> fprintf ppf "@[%a %a %a %a@]" pp_lexp v kwd "[" pp_exp exp kwd "]"
   | LEXP_vector_range(v,e1,e2) -> fprintf ppf "@[%a %a %a %a %a %a@]" pp_lexp v kwd "[" pp_exp e1 kwd ":" pp_exp e2 kwd "]"
   | LEXP_field(v,id) -> fprintf ppf "@[%a%a%a@]" pp_lexp v kwd "." pp_id id
@@ -323,10 +320,10 @@ let pp_tannot_opt ppf (Typ_annot_opt_aux(t,_)) =
   match t with
   | Typ_annot_opt_some(tq,typ) -> fprintf ppf "%a %a " pp_typquant tq pp_typ typ
 
-let pp_effects_opt ppf (Effects_opt_aux(e,_)) =
+let pp_effects_opt ppf (Effect_opt_aux(e,_)) =
   match e with
-  | Effects_opt_pure -> fprintf ppf ""
-  | Effects_opt_effects e -> pp_effects ppf e
+  | Effect_opt_pure -> fprintf ppf "effect pure"
+  | Effect_opt_effect e -> fprintf ppf "effect %a" pp_effects e
 
 let pp_funcl ppf (FCL_aux(FCL_Funcl(id,pat,exp),_)) =
   fprintf ppf "@[<0>%a %a %a @[<1>%a@] @]@\n" pp_id id pp_pat_atomic pat kwd "=" pp_exp exp 
@@ -361,7 +358,7 @@ let pp_format_id_lem (Id_aux(i,_)) =
 
 let pp_lem_id ppf id = base ppf (pp_format_id_lem id)
 
-let pp_format_var_lem (Var_aux(Var v,_)) = "(Var \"" ^ v ^ "\")"
+let pp_format_var_lem (Kid_aux(Var v,_)) = "(Var \"" ^ v ^ "\")"
 
 let pp_lem_var ppf var = base ppf (pp_format_var_lem var)
 
@@ -370,7 +367,7 @@ let pp_format_bkind_lem (BK_aux(k,_)) =
   | BK_type -> "BK_type"
   | BK_nat -> "BK_nat"
   | BK_order -> "BK_order"
-  | BK_effects -> "BK_effects"
+  | BK_effect -> "BK_effect"
 
 let pp_lem_bkind ppf bk = base ppf (pp_format_bkind_lem bk)
 
@@ -391,7 +388,6 @@ let rec pp_format_typ_lem (Typ_aux(t,_)) =
   | Typ_wild -> "Typ_wild"
 and pp_format_nexp_lem (Nexp_aux(n,_)) = 
   match n with
-  | Nexp_id(id) -> "(Nexp_id " ^ pp_format_id_lem id ^ ")"
   | Nexp_var(v) -> "(Nexp_var " ^ pp_format_var_lem v ^ ")"
   | Nexp_constant(i) -> "(Nexp_constant " ^ string_of_int i ^ ")"
   | Nexp_sum(n1,n2) -> "(Nexp_sum " ^ (pp_format_nexp_lem n1) ^ " " ^ (pp_format_nexp_lem n2) ^ ")"
@@ -399,33 +395,31 @@ and pp_format_nexp_lem (Nexp_aux(n,_)) =
   | Nexp_exp(n1) -> "(Nexp_exp " ^ (pp_format_nexp_lem n1) ^ ")"
 and pp_format_ord_lem (Ord_aux(o,_)) = 
   match o with
-  | Ord_id(id) -> "(Ord_id " ^ pp_format_id_lem id ^ ")"
   | Ord_var(v) -> "(Ord_var " ^ pp_format_var_lem v ^ ")"
   | Ord_inc -> "Ord_inc"
   | Ord_dec -> "Ord_dec"  
-and pp_format_effects_lem (Effects_aux(e,_)) =
+and pp_format_effects_lem (Effect_aux(e,_)) =
   match e with
-  | Effects_id(id) -> "(Effects_id " ^ pp_format_id id ^ ")"
-  | Effects_var(v) -> "(Effects_var " ^ pp_format_var v ^ ")"
-  | Effects_set(efcts) ->
-    "(Effects_set [" ^
+  | Effect_var(v) -> "(Effect_var " ^ pp_format_var v ^ ")"
+  | Effect_set(efcts) ->
+    "(Effect_set [" ^
       (list_format "; " 
-         (fun (Effect_aux(e,l)) ->
+         (fun (BE_aux(e,l)) ->
 	   match e with
-	   | Effect_rreg -> "Effect_rreg"
-	   | Effect_wreg -> "Effect_wreg"
-	   | Effect_rmem -> "Effect_rmem"
-	   | Effect_wmem -> "Effect_wmem"
-	   | Effect_undef -> "Effect_undef"
-	   | Effect_unspec -> "Effect_unspec"
-	   | Effect_nondet -> "Effect_nondet")
+	   | BE_rreg -> "BE_rreg"
+	   | BE_wreg -> "BE_wreg"
+	   | BE_rmem -> "BE_rmem"
+	   | BE_wmem -> "BE_wmem"
+	   | BE_undef -> "BE_undef"
+	   | BE_unspec -> "BE_unspec"
+	   | BE_nondet -> "BE_nondet")
 	 efcts) ^ " ])"
 and pp_format_typ_arg_lem (Typ_arg_aux(t,_)) = 
   match t with
   | Typ_arg_typ(t) -> "(Typ_arg_typ " ^ pp_format_typ_lem t ^ ")"
   | Typ_arg_nexp(n) -> "(Typ_arg_nexp " ^ pp_format_nexp_lem n ^ ")"
   | Typ_arg_order(o) -> "(Typ_arg_order " ^ pp_format_ord_lem o ^ ")"
-  | Typ_arg_effects(e) -> "(Typ_arg_effects " ^ pp_format_effects_lem e ^ ")"
+  | Typ_arg_effect(e) -> "(Typ_arg_effect " ^ pp_format_effects_lem e ^ ")"
 
 let pp_lem_typ ppf t = base ppf (pp_format_typ_lem t)
 let pp_lem_nexp ppf n = base ppf (pp_format_nexp_lem n)
@@ -438,7 +432,7 @@ let pp_format_nexp_constraint_lem (NC_aux(nc,_)) =
   | NC_bounded_ge(n1,n2) -> "(NC_bounded_ge " ^ pp_format_nexp_lem n1 ^ " " ^ pp_format_nexp_lem n2 ^ ")"
   | NC_bounded_le(n1,n2) -> "(NC_bounded_le " ^ pp_format_nexp_lem n1 ^ " " ^ pp_format_nexp_lem n2 ^ ")"
   | NC_nat_set_bounded(id,bounds) -> "(NC_nat_set_bounded " ^ 
-    pp_format_id id ^
+    pp_format_var_lem id ^
       " [" ^
       list_format "; " string_of_int bounds ^
       "])"
@@ -567,7 +561,7 @@ and pp_lem_case ppf (Pat_aux(Pat_exp(pat,exp),_)) =
 and pp_lem_lexp ppf (LEXP_aux(lexp,_)) =
   match lexp with
   | LEXP_id(id) -> fprintf ppf "(%a %a)" kwd "LEXP_id" pp_lem_id id
-  | LEXP_memory(id,exp) -> fprintf ppf "(%a %a %a)" kwd "LEXP_memory" pp_lem_id id pp_lem_exp exp
+  | LEXP_memory(id,args) -> fprintf ppf "(%a %a [%a])" kwd "LEXP_memory" pp_lem_id id (list_pp pp_semi_lem_exp pp_lem_exp) args
   | LEXP_vector(v,exp) -> fprintf ppf "@[(%a %a %a)@]" kwd "LEXP_vector" pp_lem_lexp v pp_lem_exp exp
   | LEXP_vector_range(v,e1,e2) -> 
     fprintf ppf "@[(%a %a %a %a)@]" kwd "LEXP_vector_range" pp_lem_lexp v  pp_lem_exp e1 pp_lem_exp e2
@@ -631,10 +625,10 @@ let pp_lem_tannot_opt ppf (Typ_annot_opt_aux(t,_)) =
   match t with
   | Typ_annot_opt_some(tq,typ) -> fprintf ppf "(Typ_annot_opt_some %a %a)" pp_lem_typquant tq pp_lem_typ typ
 
-let pp_lem_effects_opt ppf (Effects_opt_aux(e,_)) =
+let pp_lem_effects_opt ppf (Effect_opt_aux(e,_)) =
   match e with
-  | Effects_opt_pure -> fprintf ppf "Effects_opt_pure"
-  | Effects_opt_effects e -> fprintf ppf "(Effects_opt_effects %a)" pp_effects e
+  | Effect_opt_pure -> fprintf ppf "Effect_opt_pure"
+  | Effect_opt_effect e -> fprintf ppf "(Effect_opt_effects %a)" pp_lem_effects e
 
 let pp_lem_funcl ppf (FCL_aux(FCL_Funcl(id,pat,exp),_)) =
   fprintf ppf "@[<0>(%a %a %a %a)@]@\n" kwd "FCL_Funcl" pp_lem_id id pp_lem_pat pat pp_lem_exp exp 
diff --git a/src/test/test1.sail b/src/test/test1.sail
index 128a4a99..5c29f258 100644
--- a/src/test/test1.sail
+++ b/src/test/test1.sail
@@ -2,8 +2,8 @@ default Nat 'i
 default Order 'o
 default bool b
 default forall 'a. list<'a> b
-val forall 'a, 'b . ('a * 'b) -> 'b pure snd
-val forall Type 'i, 'b. ('i * 'b) -> 'i pure fst
+val forall 'a, 'b . ('a * 'b) -> 'b effect pure snd
+val forall Type 'i, 'b. ('i * 'b) -> 'i effect pure fst
 typedef int_list [name = "il"] = list<nat>
 typedef reco = const struct forall 'i, 'a, 'b. { 'a['i] v; 'b w; }
 typedef maybe = const union forall 'a. { Nne; 'a Sme; }
diff --git a/src/test/test3.sail b/src/test/test3.sail
index e77e1b71..89c710bc 100644
--- a/src/test/test3.sail
+++ b/src/test/test3.sail
@@ -7,8 +7,8 @@ val  nat -> nat effect { wmem , rmem }  MEM_GPU
 val ( nat * nat ) -> nat effect { wmem , rmem }  MEM_SIZE
 
 (* extern functions *)
-val extern ( nat * nat ) -> nat pure add = "add"
-val extern ( nat * nat ) -> nat pure (deinfix + ) = "add_infix"   (* infix plus *)
+val extern ( nat * nat ) -> nat effect pure add = "add"
+val extern ( nat * nat ) -> nat effect pure (deinfix + ) = "add_infix"   (* infix plus *)
 
 function nat (deinfix * ) ( (nat) x, (nat) y ) = 42
 
diff --git a/src/type_internal.ml b/src/type_internal.ml
index dabb8100..b019624d 100644
--- a/src/type_internal.ml
+++ b/src/type_internal.ml
@@ -39,7 +39,7 @@ and n_uvar = { nindex : int; mutable nsubst : t option }
 and effect = { mutable effect : effect_aux }
 and effect_aux =
   | Evar of string
-  | Eset of Ast.efct_aux list
+  | Eset of Ast.base_effect list
   | Euvar of e_uvar
 and e_uvar = { eindex : int; mutable esubst : t option }
 and order = { mutable order : order_aux }
diff --git a/src/type_internal.mli b/src/type_internal.mli
index 99b82075..fedc5cc4 100644
--- a/src/type_internal.mli
+++ b/src/type_internal.mli
@@ -38,7 +38,7 @@ and nexp_aux =
 and effect = { mutable effect : effect_aux }
 and effect_aux =
   | Evar of string
-  | Eset of Ast.efct_aux list
+  | Eset of Ast.base_effect list
   | Euvar of e_uvar
 and order = { mutable order : order_aux }
 and order_aux =