Support separated memory read/write functions.

Also allows register writing functions to be on the left hand side of an assignment in the same way.
The last parameter to a writing function is the value to be written, and should appear on the right hand side of an assignment expression.

8 files changed, 141 insertions, 69 deletions

diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem
index 0a112962..e08e4053 100644
--- a/src/lem_interp/interp.lem
+++ b/src/lem_interp/interp.lem
@@ -73,6 +73,7 @@ type value =
  | V_ctor of id * t * value
  | V_unknown (* Distinct from undefined, used by memory system *)
  | V_register of reg_form (* Value to store register access, when not actively reading or writing *)
+ | V_register_alias of (alias_spec tannot) * tannot (* Same as above, but to a concatenation of two registers *)
 
 let rec id_value_eq (i, v) (i', v') = i = i' && value_eq v v'
 and value_eq left right =
@@ -172,6 +173,7 @@ let rec to_registers (Defs defs) =
   | def::defs -> 
     match def with 
     | DEF_reg_dec (DEC_aux (DEC_reg typ id) (l,tannot)) -> (id, V_register(Reg id tannot)) :: (to_registers (Defs defs))
+    | DEF_reg_dec (DEC_aux (DEC_alias id aspec) (l,tannot)) -> (id, V_register_alias aspec tannot) :: (to_registers (Defs defs))
     | _ -> to_registers (Defs defs)
     end 
   end 
diff --git a/src/lem_interp/run_interp.ml b/src/lem_interp/run_interp.ml
index 2f8c5e97..d449f53c 100644
--- a/src/lem_interp/run_interp.ml
+++ b/src/lem_interp/run_interp.ml
@@ -153,7 +153,7 @@ module Reg = struct
 (*    eprintf "%s -> %s\n" (id_to_string id) (val_to_string v);*)
     v
 end ;;
-
+(* Old Mem, that used the id to map as well as the int... which seems wrong
 module Mem = struct
   include Map.Make(struct
     type t = (id * big_int)
@@ -174,8 +174,27 @@ module Mem = struct
   *)
   let to_string (n, idx) v =
     sprintf "%s[%s] -> %s" (id_to_string n) (string_of_big_int idx) (val_to_string v)
+end ;;*)
+
+module Mem = struct
+  include Map.Make(struct
+    type t = big_int
+    let compare v1 v2 = compare_big_int v1 v2
+  end)
+  (* debugging memory accesses
+  let add idx v m =
+    eprintf "[%s] <- %s\n" (string_of_big_int idx) (val_to_string v);
+    add idx v m
+  let find idx m =
+    let v = find idx m in
+    eprintf "[%s] -> %s\n" (string_of_big_int idx) (val_to_string v);
+    v
+  *)
+  let to_string idx v =
+    sprintf "[%s] -> %s" (string_of_big_int idx) (val_to_string v)
 end ;;
 
+
 let vconcat v v' = vec_concat (V_tuple [v; v']) ;;
 
 let slice v = function
@@ -213,14 +232,14 @@ let rec perform_action ((reg, mem) as env) = function
      | BF_concat _ -> failwith "unimplemented: non-contiguous register write")
  (* memory *)
  | Read_mem (id, V_lit(L_aux((L_num n),_)), sub) ->
-     slice (Mem.find (id, n) mem) sub, env
+     slice (Mem.find n mem) sub, env
  | Write_mem (id, V_lit(L_aux(L_num n,_)), None, value) ->
-     unit_lit, (reg, Mem.add (id, n) value mem)
+     unit_lit, (reg, Mem.add n value mem)
  (* multi-byte accesses to memory *)
  | Read_mem (id, V_tuple [V_lit(L_aux(L_num n,_)); V_lit(L_aux(L_num size,_))], sub) ->
      let rec fetch k acc =
        if eq_big_int k size then slice acc sub else
-         let slice = Mem.find (id, add_big_int n k) mem in
+         let slice = Mem.find (add_big_int n k) mem in
          fetch (succ_big_int k) (vconcat acc slice)
      in
      fetch zero_big_int (V_vector (zero_big_int, true, [])), env
@@ -235,14 +254,14 @@ let rec perform_action ((reg, mem) as env) = function
          let n1 = mult_int_big_int byte_size k in
          let n2 = sub_big_int (mult_int_big_int byte_size (succ_big_int k)) (big_int_of_int 1) in
          let slice = slice_vector value n1 n2 in
-         let mem' = Mem.add (id, add_big_int n k) slice mem in
+         let mem' = Mem.add (add_big_int n k) slice mem in
          update (succ_big_int k) mem'
      in unit_lit, (reg, update zero_big_int mem)
  (* This case probably never happens in the POWER spec anyway *)
  | Write_mem (id, V_lit(L_aux(L_num n,_)), Some (start, stop), (V_vector _ as value)) ->
-     let old_val = Mem.find (id, n) mem in
+     let old_val = Mem.find n mem in
      let new_val = fupdate_vector_slice old_val value start stop in
-     unit_lit, (reg, Mem.add (id, n) new_val mem)
+     unit_lit, (reg, Mem.add n new_val mem)
  (* special case for slices of size 1: wrap value in a vector *)
  | Write_reg ((Reg (_, _) as r), (Some (start, stop) as slice), value) when eq_big_int start stop ->
      perform_action env (Write_reg (r, slice, V_vector(zero_big_int, true, [value])))
diff --git a/src/pretty_print.ml b/src/pretty_print.ml
index 40b6d60f..c500beb1 100644
--- a/src/pretty_print.ml
+++ b/src/pretty_print.ml
@@ -606,6 +606,7 @@ let doc_typ, doc_atomic_typ, doc_nexp =
   | Typ_tup typs -> parens (separate_map comma_sp app_typ typs)
   | _ -> app_typ ty
   and app_typ ((Typ_aux (t, _)) as ty) = match t with
+  (*TODO Need to un bid-endian-ify this here, since both can transform to the shorthand, especially with <: and :> *)
   (* Special case simple vectors to improve legibility
    * XXX we assume big-endian here, as usual *)
   | Typ_app(Id_aux (Id "vector", _), [
diff --git a/src/test/power.sail b/src/test/power.sail
index 098057e2..5f1f532b 100644
--- a/src/test/power.sail
+++ b/src/test/power.sail
@@ -7,6 +7,8 @@ function forall Type 'a . 'a BCD_TO_DEC ( x ) = x
 function bit carry_out ( x ) = bitzero
 (* XXX length *)
 function nat length ( x ) = 64
+(* XXX Storage control *)
+function forall Type 'a . 'a real_addr ( x ) = x
 
 (* XXX *)
 val extern forall Nat 'k, Nat 'r,
@@ -41,13 +43,19 @@ function (bit[64]) ROTL(v, n) = v[n .. 63] : v[0 .. (n-1)]
 (* Branch facility registers *)
 
 typedef cr = register bits [ 32 : 63 ] {
-  32 .. 35 : CR0; (* LT, GT, EQ, SO -- fixed-point *)
-  36 .. 39 : CR1; (* FX, FEX, VX, OX -- (decimal) floating-point *)
+  32 .. 35 : CR0;
+    32 : LT; 33 : GT; 34 : EQ; 35 : SO;
+  36 .. 39 : CR1;
+    36 : FX; 37 : FEX; 38 : VX; 39 : OX;
   40 .. 43 : CR2;
   44 .. 47 : CR3;
   48 .. 51 : CR4;
   52 .. 55 : CR5;
-  56 .. 59 : CR6; (* LT, GT, EQ, SO -- vector *)
+  56 .. 59 : CR6;
+    (* name clashing - do we need hierarchical naming for fields, or do
+    we just don't care? LT, GT, etc. are not used in the code anyway.
+    56 : LT; 57 : GT; 58 : EQ; 59 : SO;
+    *)
   60 .. 63 : CR7;
 }
 register (cr) CR
@@ -62,6 +70,8 @@ typedef xer = register bits [ 0 : 63 ] {
 }
 register (xer) XER
 
+register alias CA = XER.CA
+
 (* Fixed-point registers *)
 
 register (bit[64]) GPR0
@@ -119,14 +129,14 @@ let (vector <0, 10, inc, (register<(bit[64])>) >) SPR =
     LR, CTR
   ]
 
-(* XXX bogus, DCR might be numbered with 64-bit values! -
- and it's implementation-dependent; also, some DCR are only 32 bits
+(* XXX DCR is implementation-dependent; also, some DCR are only 32 bits
  instead of 64, and mtdcrux/mfdcrux do special tricks in that case, not
- shown in pseudo-code (?) *)
+ shown in pseudo-code. We just define two dummy DCR here, using sparse
+ vector definition. *)
 register (vector <0, 64, inc, bit>) DCR0
 register (vector <0, 64, inc, bit>) DCR1
-let (vector <0, 2, inc, (register<(vector<0, 64, inc, bit>)>) >) DCR =
-  [ DCR0, DCR1 ]
+let (vector <0, 2** 64, inc, (register<(vector<0, 64, inc, bit>)>) >) DCR =
+  [ 0=DCR0, 1=DCR1 ]
 
 (* Floating-point registers *)
 
@@ -187,8 +197,8 @@ typedef fpscr = register bits [ 0 : 63 ] {
   46 : FI;
   47 .. 51 : FPRF;
   47 : C;
-  48 .. 51 : FPCC; (* the bits of FPCC are named FL, FG, FE and FU,
-                      but those names are never used in pseudo-code. *)
+  48 .. 51 : FPCC;
+    48 : FL; 49 : FG; 50 : FE; 51 : FU;
   53 : VXSOFT;
   54 : VXSQRT;
   55 : VXCVI;
@@ -202,6 +212,31 @@ typedef fpscr = register bits [ 0 : 63 ] {
 }
 register (fpscr) FPSCR
 
+(* Pair-wise access to FPR registers *)
+
+register alias FPRp0 = FPR0 : FPR1
+register alias FPRp2 = FPR2 : FPR3
+register alias FPRp4 = FPR4 : FPR5
+register alias FPRp6 = FPR6 : FPR7
+register alias FPRp8 = FPR8 : FPR9
+register alias FPRp10 = FPR10 : FPR11
+register alias FPRp12 = FPR12 : FPR13
+register alias FPRp14 = FPR14 : FPR15
+register alias FPRp16 = FPR16 : FPR17
+register alias FPRp18 = FPR18 : FPR19
+register alias FPRp20 = FPR20 : FPR21
+register alias FPRp22 = FPR22 : FPR23
+register alias FPRp24 = FPR24 : FPR25
+register alias FPRp26 = FPR26 : FPR27
+register alias FPRp28 = FPR28 : FPR29
+register alias FPRp30 = FPR30 : FPR31
+
+let (vector <0, 32, inc, (register<(bit[128])>)>) FPRp =
+  [ 0 = FPRp0, 2 = FPRp2, 4 = FPRp4, 6 = FPRp6, 8 = FPRp8, 10 = FPRp10,
+  12 = FPRp12, 14 = FPRp14, 16 = FPRp16, 18 = FPRp18, 20 = FPRp20, 22 =
+  FPRp22, 24 = FPRp24, 26 = FPRp26, 28 = FPRp28, 30 = FPRp30 ]
+
+
 (* XXX *)
 val extern bit[32] -> bit[64] effect pure DOUBLE
 val extern bit[64] -> bit[32] effect pure SINGLE
@@ -298,7 +333,8 @@ register (bit[64]) NIA (* next instruction address *)
 register (bit[64]) CIA (* current instruction address *)
 
 
-val extern forall Nat 'n. ( nat , [|'n|] ) -> (bit[8 * 'n]) effect { wmem , rmem } MEM
+val extern forall Nat 'n. ( nat , [|'n|] , bit[8*'n]) -> unit effect { wmem } MEMw
+val extern forall Nat 'n. ( nat , [|'n|] ) -> (bit[8 * 'n]) effect { rmem } MEMr
 
 (* XXX effect for trap? *)
 val extern unit -> unit effect pure trap
@@ -314,12 +350,12 @@ scattered function ast decode
 
 union ast member (bit[5], bit[5], bit[2], bit) Bclr
 
-function clause decode ([bitzero, bitone, bitzero, bitzero, bitone, bitone] :
+function clause decode (0b010011 :
 (bit[5]) BO :
 (bit[5]) BI :
 (bit[3]) _ :
 (bit[2]) BH :
-[bitzero, bitzero, bitzero, bitzero, bitzero, bitone, bitzero, bitzero, bitzero, bitzero] :
+0b0000010000 :
 [LK] as instr) =
   Bclr (BO,BI,BH,LK)
 
@@ -335,7 +371,7 @@ function clause execute (Bclr (BO, BI, BH, LK)) =
 
 union ast member (bit[5], bit[5], bit[16]) Lwz
 
-function clause decode ([bitone, bitzero, bitzero, bitzero, bitzero, bitzero] :
+function clause decode (0b100000 :
 (bit[5]) RT :
 (bit[5]) RA :
 (bit[16]) D as instr) =
@@ -346,12 +382,12 @@ function clause execute (Lwz (RT, RA, D)) =
     (bit[64]) b := 0;
     if RA == 0 then b := 0 else b := GPR[RA];
     EA := b + EXTS (D);
-    GPR[RT] := 0b00000000000000000000000000000000 : MEM (EA,4)
+    GPR[RT] := 0b00000000000000000000000000000000 : MEMr (EA,4)
   }
 
 union ast member (bit[5], bit[5], bit[16]) Stw
 
-function clause decode ([bitone, bitzero, bitzero, bitone, bitzero, bitzero] :
+function clause decode (0b100100 :
 (bit[5]) RS :
 (bit[5]) RA :
 (bit[16]) D as instr) =
@@ -362,12 +398,12 @@ function clause execute (Stw (RS, RA, D)) =
     (bit[64]) b := 0;
     if RA == 0 then b := 0 else b := GPR[RA];
     EA := b + EXTS (D);
-    MEM(EA,4) := (GPR[RS])[32 .. 63]
+    MEMw(EA,4) := (GPR[RS])[32 .. 63]
   }
 
 union ast member (bit[5], bit[5], bit[16]) Stwu
 
-function clause decode ([bitone, bitzero, bitzero, bitone, bitzero, bitone] :
+function clause decode (0b100101 :
 (bit[5]) RS :
 (bit[5]) RA :
 (bit[16]) D as instr) =
@@ -376,13 +412,13 @@ function clause decode ([bitone, bitzero, bitzero, bitone, bitzero, bitone] :
 function clause execute (Stwu (RS, RA, D)) =
   {
     EA := GPR[RA] + EXTS (D);
-    MEM(EA,4) := (GPR[RS])[32 .. 63];
+    MEMw(EA,4) := (GPR[RS])[32 .. 63];
     GPR[RA] := EA
   }
 
 union ast member (bit[5], bit[5], bit[16]) Addi
 
-function clause decode ([bitzero, bitzero, bitone, bitone, bitone, bitzero] :
+function clause decode (0b001110 :
 (bit[5]) RT :
 (bit[5]) RA :
 (bit[16]) SI as instr) =
@@ -393,11 +429,11 @@ function clause execute (Addi (RT, RA, SI)) =
 
 union ast member (bit[5], bit[5], bit[5], bit) Or
 
-function clause decode ([bitzero, bitone, bitone, bitone, bitone, bitone] :
+function clause decode (0b011111 :
 (bit[5]) RS :
 (bit[5]) RA :
 (bit[5]) RB :
-[bitzero, bitone, bitone, bitzero, bitone, bitone, bitone, bitone, bitzero, bitzero] :
+0b0110111100 :
 [Rc] as instr) =
   Or (RS,RA,RB,Rc)
 
@@ -414,7 +450,7 @@ register ast instr (* monitor decoded instructions *)
 (* fetch-decode-execute *)
 function unit fde () = {
   NIA := CIA + 4;
-  instr := decode(MEM(CIA, 4));
+  instr := decode(MEMr(CIA, 4));
   execute(instr);
   CIA := NIA;
 }
diff --git a/src/test/run_power.ml b/src/test/run_power.ml
index e1039b0b..4526a79d 100644
--- a/src/test/run_power.ml
+++ b/src/test/run_power.ml
@@ -29,7 +29,7 @@ let mem = ref Mem.empty ;;
 let add_mem byte addr =
   assert(byte >= 0 && byte < 256);
   let vector = big_int_to_vec (Big_int.big_int_of_int byte) (Big_int.big_int_of_int 8) in
-  let key = Id_aux (Id "MEM", Unknown), addr in
+  let key = (*Id_aux (Id "MEM", Unknown), (* memory map no longer using id, just the address, since read/write id different *)*) addr in
   mem := Mem.add key vector !mem
 ;;
 
diff --git a/src/test/test3.sail b/src/test/test3.sail
index e2dbe2f3..98ebb2d6 100644
--- a/src/test/test3.sail
+++ b/src/test/test3.sail
@@ -4,44 +4,47 @@ register [|0:256|] dummy_reg
 register (bit[8]) dummy_reg2
 (* a function to read from memory; wmem serves no purpose currently,
    memory-writing functions are figured out syntactically. *)
-val extern nat -> nat effect { wmem , rmem }  MEM
-val extern nat -> nat effect { wmem , rmem }  MEM_GPU
-val extern forall Nat 'n . ( nat, [|'n|] ) -> (bit['n * 8]) effect { wmem , rmem }  MEM_SIZE
-val extern nat -> (bit[8]) effect { wmem , rmem }  MEM_WORD
+val extern (nat,nat) -> unit effect { wmem }  MEMw
+val extern nat -> nat effect { rmem } MEMr
+val extern (nat,nat) -> unit effect { wmem }  MEM_GPUw
+val extern nat -> nat effect { rmem} MEM_GPUr
+val extern forall Nat 'n . ( nat, [|'n|], bit['n*8]) -> unit effect { wmem }  MEM_SIZEw
+val extern forall Nat 'n . ( nat, [|'n|]) -> bit['n*8] effect { rmem } MEM_SIZEr
+val extern (nat,bit[8]) -> unit effect { wmem }  MEM_WORDw
+val extern nat -> bit[8] effect { rmem } MEM_WORDr
 
 function nat (deinfix * ) ( (nat) x, (nat) y ) = 42
 
 function nat main _ = {
   (* left-hand side function call = memory write *)
-  MEM(0) := 0;
-  (* memory read, thanks to effect { rmem} above *)
-  ignore(MEM(0));
+  MEMw(0) := 0;
+  ignore(MEMr(0));
   (* register write, idem *)
   dummy_reg := 1;
   (* register read, thanks to register declaration *)
   ignore(dummy_reg);
 
 
-  MEM_WORD(0) := 0b10101010;
-  (MEM_WORD(0))[3..4] := 0b10;
+  MEM_WORDw(0) := 0b10101010;
+  (MEM_WORDw(0))[3..4] := 0b10;
   (* XXX this one is broken - I don't what it should do,
   or even if we should accept it, but the current result
   is to eat up one bit, ending up with a 7-bit word. *)
   (*(MEM_WORD(0))[4..3] := 0b10;*) (*We reject this as 4 > 3 not <= *)
-  ignore(MEM_WORD(0));
+  ignore(MEM_WORDr(0));
 
   (* infix call *)
   ignore(7 * 9);
 
   (* Some more checks *)
-  MEM(1) := 2;
-  ignore(MEM(1));
-  MEM_GPU(0) := 3;
-  ignore(MEM_GPU(0));
-  MEM_SIZE(0,1) := 0b11110000;
-  ignore(MEM_SIZE(0,1));
-  MEM_SIZE(0,2) := 0b1111000010100000;
-  ignore(MEM_SIZE(0,2));
+  MEMw(1) := 2;
+  ignore(MEMr(1));
+  MEM_GPUw(0) := 3;
+  ignore(MEM_GPUr(0));
+  MEM_SIZEw(0,1) := 0b11110000;
+  ignore(MEM_SIZEr(0,1));
+  MEM_SIZEw(0,2) := 0b1111000010100000;
+  ignore(MEM_SIZEr(0,2));
 
   (* extern calls *)
   dummy_reg := 3 + 39;
diff --git a/src/test/test4.sail b/src/test/test4.sail
index 36cb271a..fa0133ca 100644
--- a/src/test/test4.sail
+++ b/src/test/test4.sail
@@ -1,5 +1,5 @@
 (* hack to display log messages. Syntax: LOG(0) := "log message"; *)
-val extern forall Type 'a . nat -> 'a effect { wmem , rmem }  LOG
+val extern forall Type 'a . (nat, 'a) -> unit effect { wmem }  LOG
 
 register (bit[1]) GPR0
 register (bit[1]) GPR1
diff --git a/src/type_check.ml b/src/type_check.ml
index 6cd1f61f..41da8fec 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -1130,28 +1130,39 @@ and check_lexp envs is_top (LEXP_aux(lexp,(l,annot))) : (tannot lexp * typ * tan
 		  then
                     let app,cs_a = get_abbrev d_env apps in
                     let out,cs_o = get_abbrev d_env out in
+		    let cs_call = cs@cs_o@cs_a in
                     (match app.t with
-		      | Ttup ts | Tabbrev(_,{t=Ttup ts}) -> 
-			let (E_aux(E_tuple es,(l',tannot)),t',_,cs',ef_e) = check_exp envs apps (E_aux(E_tuple exps,(l,NoTyp))) in
-			let item_t = match out.t with
-			  | Tid "unit" -> {t = Tapp("vector",[TA_nexp (new_n());TA_nexp (new_n()); TA_ord (new_o());TA_typ bit_t])}
-			  | _ -> out in
-			let ef = (*if is_external then add_effect (BE_aux(BE_wmem,l)) ef_e else*) union_effects ef ef_e in
-			(LEXP_aux(LEXP_memory(id,es),(l,Base(([],unit_t),tag,cs@cs',ef))),item_t,Envmap.empty,tag,cs@cs',ef)
-		      | app_t -> 
+		      | Ttup ts | Tabbrev(_,{t=Ttup ts}) ->
+			let (args,item_t) = ((fun ts -> (List.rev (List.tl ts), List.hd ts)) (List.rev ts)) in
+			let args_t = {t = Ttup args} in
+			let (es, cs_es, ef_es) = 
+			  match args,exps with
+			    | [],[] -> ([],[],pure_e)
+			    | [],[e] -> let (e',_,_,cs_e,ef_e) = check_exp envs unit_t e in ([e'],cs_e,ef_e)
+			    | [],es -> typ_error l ("Expected no arguments for assignment function " ^ i)
+			    | args,[] -> 
+			      typ_error l ("Expected arguments with types " ^ (t_to_string args_t) ^
+					   "for assignment function " ^ i)
+			    | args,es -> 
+			      (match check_exp envs args_t (E_aux (E_tuple exps,(l,NoTyp))) with
+				| (E_aux(E_tuple es,(l',tannot)),_,_,cs_e,ef_e) -> (es,cs_e,ef_e)
+				| _ -> raise (Reporting_basic.err_unreachable l "Gave check_exp a tuple, didn't get a tuple back"))
+			in
+			let ef_all = union_effects ef ef_es in
+			(LEXP_aux(LEXP_memory(id,es),(l,Base(([],out),tag,cs_call,ef))),
+			 item_t,Envmap.empty,tag,cs_call@cs_es,ef_all)
+		      | _ -> 
 			let e = match exps with
 			  | [] -> E_aux(E_lit(L_aux(L_unit,l)),(l,NoTyp))
-			  | [e] -> e
-			  | es -> typ_error l ("Expected only one argument for memory access of " ^ i) in
-			let (e,t',_,cs',ef_e) = check_exp envs apps e in
-			let item_t = match out.t with
-			  | Tid "unit" -> {t = Tapp("vector",[TA_nexp (new_n());TA_nexp (new_n()); TA_ord (new_o());TA_typ bit_t])} 
-			  | _ -> out in
-			  let ef = if is_external then add_effect (BE_aux(BE_wmem,l)) ef_e else union_effects ef ef_e in
-			  (LEXP_aux(LEXP_memory(id,[e]),(l,Base(([],unit_t),tag,cs@cs',ef))), item_t,Envmap.empty,tag,cs@cs',ef))
-		  else typ_error l ("Memory assignments require functions with wmem effect")
-		| _ -> typ_error l ("Memory assignments require functions with declared wmem effect"))
-	    | _ -> typ_error l ("Memory assignments require functions, found " ^ i ^ " which has type " ^ (t_to_string t)))
+			  | [(E_aux(E_lit(L_aux(L_unit,_)),(_,NoTyp)) as e)] -> e
+			  | es -> typ_error l ("Expected no arguments for assignment function " ^ i) in
+			let (e,_,_,cs_e,ef_e) = check_exp envs apps e in
+			let ef_all = union_effects ef ef_e in
+			(LEXP_aux(LEXP_memory(id,[e]),(l,Base(([],out),tag,cs_call,ef))),
+			 app,Envmap.empty,tag,cs_call@cs_e,ef_all))
+		  else typ_error l ("Assignments require functions with a wmem or wreg effect")
+		| _ -> typ_error l ("Assignments require functions with a wmem or wreg effect"))
+	    | _ -> typ_error l ("Assignments require a function here, found " ^ i ^ " which has type " ^ (t_to_string t)))
 	| _ -> typ_error l ("Unbound identifier " ^ i))
     | LEXP_cast(typ,id) -> 
       let i = id_to_string id in