Fixing assorted bugs. Adding ability to put a type on the identifier being assigned to in assignments.

7 files changed, 87 insertions, 10 deletions

diff --git a/src/initial_check.ml b/src/initial_check.ml
index 83a2c5ab..2a80ff37 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -384,10 +384,12 @@ and to_ast_lexp (k_env : kind Envmap.t) (Parse_ast.E_aux(exp,l) : Parse_ast.exp)
 	  | [E_aux(E_tuple exps,_)] -> LEXP_memory(to_ast_id f',exps)
 	  | args -> LEXP_memory(to_ast_id f', args))
       | _ -> typ_error l' "memory call on lefthand side of assignment must begin with an id" None None None)
+    | Parse_ast.E_cast(typ,Parse_ast.E_aux(Parse_ast.E_id(id),l')) ->
+      LEXP_cast(to_ast_typ k_env typ, to_ast_id id)
     | 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)
     | Parse_ast.E_field(fexp,id) -> LEXP_field(to_ast_lexp k_env fexp, to_ast_id id)
-    | _ -> typ_error l "Only identifiers, vector accesses, vector slices, and fields can be on the lefthand side of an assignment" None None None)
+    | _ -> typ_error l "Only identifiers, cast identifiers, vector accesses, vector slices, and fields can be on the lefthand side of an assignment" None None None)
       , (l,None))
 
 and to_ast_case (k_env : kind Envmap.t) (Parse_ast.Pat_aux(pex,l) : Parse_ast.pexp) : tannot pexp =
diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem
index fe4568fb..75e6443e 100644
--- a/src/lem_interp/interp.lem
+++ b/src/lem_interp/interp.lem
@@ -1095,6 +1095,34 @@ and create_write_message_or_update t_level value l_env l_mem is_top_level ((LEXP
          end)
       | (Action a s,lm, le) -> ((Action a s,lm,le), Just (fun (E_aux (E_tuple es) _) -> (LEXP_aux (LEXP_memory id es) (l,annot))))
       | e -> (e,Nothing) end
+    | LEXP_cast typc id -> 
+      match tag with
+	| Tag_empty ->
+	  match in_env l_env id with
+	    | Just (V_boxref n t) -> 
+	      if is_top_level 
+	      then ((Value (V_lit (L_aux L_unit l)), update_mem l_mem n value, l_env),Nothing)
+	      else ((Value (in_mem l_mem n), l_mem, l_env),Just (fun e -> LEXP_aux (LEXP_cast typc id) (l,annot)))
+	    | Just v -> 
+	      if is_top_level then ((Error l "Writes must be to reg values",l_mem,l_env),Nothing) 
+	      else ((Value v,l_mem,l_env),Just (fun e -> LEXP_aux(LEXP_cast typc id) (l,annot)))
+	    | Nothing -> 	  
+	      if is_top_level 
+              then begin
+		let (Mem c m) = l_mem in
+		let l_mem = (Mem (c+1) m) in
+		((Value (V_lit (L_aux L_unit l)), update_mem l_mem c value, (id,(V_boxref c typ))::l_env),Nothing)
+              end
+              else ((Error l (String.stringAppend "Undefined id " (get_id id)),l_mem,l_env),Nothing)
+          end 
+        | Tag_extern _ ->
+	  let regf = Reg id typ in
+	  let request = (Action (Write_reg regf Nothing value) 
+			        (Frame (Id_aux (Id "0") l) 
+				       (E_aux (E_id (Id_aux (Id "0") l)) (l,intern_annot annot)) l_env l_mem Top),l_mem,l_env) in
+          if is_top_level then (request,Nothing) else (request,Just (fun e -> LEXP_aux (LEXP_cast typc id) (l,annot)))
+        | _ -> ((Error l (String.stringAppend "Internal error: writing to id with tag other than extern or empty " (get_id id)),l_mem,l_env),Nothing)
+      end 
     | LEXP_vector lexp exp -> 
       match (interp_main t_level l_env l_mem exp) with
       | (Value i,lm,le) ->
diff --git a/src/pretty_print.ml b/src/pretty_print.ml
index a06d1fe5..7ee110d3 100644
--- a/src/pretty_print.ml
+++ b/src/pretty_print.ml
@@ -261,6 +261,7 @@ and pp_lexp ppf (LEXP_aux(lexp,_)) =
   match lexp with
   | LEXP_id(id) -> pp_id ppf id
   | LEXP_memory(id,args) -> fprintf ppf "@[%a(%a)@]" pp_id id (list_pp pp_exp pp_exp) args
+  | LEXP_cast(typ,id) -> fprintf ppf "@[(%a) %a@]" pp_typ typ pp_id id
   | 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
@@ -681,6 +682,7 @@ and pp_lem_lexp ppf (LEXP_aux(lexp,(l,annot))) =
     match lexp with
       | LEXP_id(id) -> fprintf ppf "(%a %a)" kwd "LEXP_id" pp_lem_id id
       | 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_cast(typ,id) -> fprintf ppf "(LEXP_cast %a %a)" pp_lem_typ typ pp_lem_id id
       | 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
diff --git a/src/test/run_tests.ml b/src/test/run_tests.ml
index f614306b..d1a90f38 100644
--- a/src/test/run_tests.ml
+++ b/src/test/run_tests.ml
@@ -6,6 +6,7 @@ let tests = [
   "test3", Test3.defs;
   "pattern", Pattern.defs;
   "vectors", Vectors.defs;
+  "regbits", Regbits.defs;
   (*"power", Power.defs;*)
 ] ;;
 
diff --git a/src/test/test1.sail b/src/test/test1.sail
index 3d69018d..0050a257 100644
--- a/src/test/test1.sail
+++ b/src/test/test1.sail
@@ -14,6 +14,9 @@ val forall Nat 'a, Nat 'b. bit['a:'b] sliced
 let bit v = bitzero
 let ( bit [ 32 ] ) v1 = 0b101
 
+val forall Type 'a. 'a -> 'a effect pure identity
+function forall Type 'a. 'a identity i = i
+
 function unit ignore(x) = ()
 
 (* scattered function definition and union definition *)
@@ -32,7 +35,7 @@ function clause f (  C (a) ) = C(a)
 end ast
 end f
 
-function unit a (bit) b = if b then () else ()
+function unit a (bit) b = if identity(b) then (identity()) else ()
 
 function bit sw s = switch s { case 0 -> bitzero }
 
diff --git a/src/type_check.ml b/src/type_check.ml
index 6cf4ca9b..fda5c97c 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -148,10 +148,13 @@ let typschm_to_tannot envs ((TypSchm_aux(typschm,l)):typschm) (tag : tag) : tann
       let (ids,constraints) = typq_to_params envs tq in
       Some((ids,t),tag,constraints,pure_e)
 
-let into_register (t : tannot) : tannot =
+let into_register d_env (t : tannot) : tannot =
   match t with
     | Some((ids,ty),tag,constraints,eft) -> 
-      (match ty.t with 
+      let ty' =  match get_abbrev d_env ty with
+	| Some(t,cs,e) -> t
+	| None -> ty in
+      (match ty'.t with 
 	| Tapp("register",_)-> t
 	| _ -> Some((ids, {t= Tapp("register",[TA_typ ty])}),tag,constraints,eft))
     | None -> None
@@ -375,6 +378,9 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp
         typ_error l ("Identifier " ^ i ^ " must be defined, not just specified, before use")
       | Some(Some((params,t),tag,cs,ef)) ->
 	let t,cs,ef = subst params t cs ef in
+	let t,cs,ef = match get_abbrev d_env t with
+	  | Some(t,cs1,ef1) -> t,cs@cs1,union_effects ef ef1
+	  | None -> t,cs,ef in
         (match t.t,expect_t.t with 
         | Tfn _,_ -> typ_error l ("Identifier " ^ (id_to_string id) ^ " is bound to a function and cannot be used as a value")
         | Tapp("register",[TA_typ(t')]),Tapp("register",[TA_typ(expect_t')]) -> 
@@ -513,7 +519,6 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp
        expect_t,Envmap.intersect then_env else_env,then_c@else_c@c1,
        union_effects ef1 (union_effects then_ef else_ef))
     | E_for(id,from,to_,step,order,block) -> 
-      (* TODO::: This presently assumes increasing; this should be checked if that's the assumption we want *)
       let fb,fr,tb,tr,sb,sr = new_n(),new_n(),new_n(),new_n(),new_n(),new_n() in
       let ft,tt,st = {t=Tapp("enum",[TA_nexp fb;TA_nexp fr])},
 	{t=Tapp("enum",[TA_nexp tb;TA_nexp tr])},{t=Tapp("enum",[TA_nexp sb;TA_nexp sr])} in     
@@ -922,6 +927,36 @@ and check_lexp envs (LEXP_aux(lexp,(l,annot))) : (tannot lexp * typ * tannot ema
 		| _ -> 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)))
 	| _ -> typ_error l ("Unbound identifier " ^ i))
+    | LEXP_cast(typ,id) -> 
+      let i = id_to_string id in
+      let ty = typ_to_t typ in
+      (match Envmap.apply t_env i with
+	| Some(Some((parms,t),Default,_,_)) ->
+	  typ_error l ("Identifier " ^ i ^ " cannot be assigned when only a default specification exists")
+	| Some(Some((parms,t),tag,cs,_)) ->
+	  let t,cs,_ = subst parms t cs pure_e in
+	  let t,cs = match get_abbrev d_env t with
+	    | None -> t,cs
+	    | Some(t,cs,e) -> t,cs in
+	  (match t.t with
+	    | Tapp("register",[TA_typ u]) ->
+	      let t',cs = type_consistent l d_env ty u in
+	      let ef = {effect=Eset[BE_aux(BE_wreg,l)]} in
+	      (LEXP_aux(lexp,(l,(Some(([],t),External (Some "register"),cs,ef)))),ty,Envmap.empty,External (Some "register"),[],ef)
+	    | Tapp("reg",[TA_typ u]) ->
+	      let t',cs = type_consistent l d_env ty u in
+	      (LEXP_aux(lexp,(l,(Some(([],t),Emp,cs,pure_e)))),ty,Envmap.empty,Emp,[],pure_e)
+	    | Tuvar _ ->
+	      let u' = {t=Tapp("reg",[TA_typ ty])} in
+	      t.t <- u'.t;
+	      (LEXP_aux(lexp,(l,(Some((([],u'),Emp,cs,pure_e))))),ty,Envmap.empty,Emp,[],pure_e)
+	    | _ -> 
+	      typ_error l 
+		("Can only assign to identifiers with type register or reg, found identifier " ^ i ^ " with type " ^ t_to_string t))
+	| _ -> 
+	  let t = {t=Tapp("reg",[TA_typ ty])} in
+	  let tannot = (Some(([],t),Emp,[],pure_e)) in
+	  (LEXP_aux(lexp,(l,tannot)),ty,Envmap.from_list [i,tannot],Emp,[],pure_e))
     | LEXP_vector(vec,acc) -> 
       let (vec',item_t,env,tag,csi,ef) = check_lexp envs vec in
       let item_t,cs = match get_abbrev d_env item_t with
@@ -936,6 +971,7 @@ and check_lexp envs (LEXP_aux(lexp,(l,annot))) : (tannot lexp * typ * tannot ema
 	  in
 	  let (e,t',_,cs',ef_e) = check_exp envs acc_t acc in
 	  (LEXP_aux(LEXP_vector(vec',e),(l,Some(([],t),tag,cs@cs',union_effects ef ef_e))),t,env,tag,cs@cs',union_effects ef ef_e)
+	| Tuvar _ -> typ_error l "Assignment to one position expected a vector with a known order, found a polymorphic value, try adding a cast"
 	| _ -> typ_error l ("Assignment expected vector, found assignment to type " ^ (t_to_string item_t))) 
     | LEXP_vector_range(vec,e1,e2)-> 
       let (vec',item_t,env,tag,csi,ef) = check_lexp envs vec in
@@ -965,6 +1001,7 @@ and check_lexp envs (LEXP_aux(lexp,(l,annot))) : (tannot lexp * typ * tannot ema
 	  let cs = cs_t@cs@cs1@cs2 in
 	  let ef = union_effects ef (union_effects ef_e ef_e') in
 	  (LEXP_aux(LEXP_vector_range(vec',e1',e2'),(l,Some(([],item_t),tag,cs,ef))),res_t,env,tag,cs,ef)
+	| Tuvar _ -> typ_error l "Assignement to a range of elements requires a vector with a known order, found a polymorphic value, try addinga  cast"
 	| _ -> typ_error l ("Assignment expected vector, found assignment to type " ^ (t_to_string item_t))) 
     | LEXP_field(vec,id)-> 
       let (vec',item_t,env,tag,csi,ef) = check_lexp envs vec in
@@ -1070,7 +1107,7 @@ let check_type_def envs (TD_aux(td,(l,annot))) =
 		   Some(([],{t=Tapp("vector",[TA_nexp base;TA_nexp climb;TA_ord({order=Oinc});TA_typ({t= Tid "bit"})])}),Emp,[],pure_e)))
 		ranges 
 	    in
-	    let tannot = into_register (Some(([],ty),Emp,[],pure_e)) in
+	    let tannot = into_register d_env (Some(([],ty),Emp,[],pure_e)) in
 	    (TD_aux(td,(l,tannot)),
 	     Env({d_env with rec_env = ((id',Register,franges)::d_env.rec_env);
 	       abbrevs = Envmap.insert d_env.abbrevs (id',tannot)},t_env)))
@@ -1097,7 +1134,7 @@ let check_type_def envs (TD_aux(td,(l,annot))) =
 		   Some(([],{t=Tapp("vector",[TA_nexp base;TA_nexp climb;TA_ord({order=Odec});TA_typ({t= Tid "bit"})])}),Emp,[],pure_e)))
 		ranges 
 	    in
-	    let tannot = into_register (Some(([],ty),Emp,[],pure_e)) in
+	    let tannot = into_register d_env (Some(([],ty),Emp,[],pure_e)) in
 	    (TD_aux(td,(l,tannot)),
 	     Env({d_env with rec_env = (id',Register,franges)::d_env.rec_env;
 	       abbrevs = Envmap.insert d_env.abbrevs (id',tannot)},t_env)))
@@ -1192,7 +1229,7 @@ let check_def envs (DEF_aux(def,(l,annot))) =
     | DEF_reg_dec(typ,id) -> 
       let t = (typ_to_t typ) in
       let i = id_to_string id in
-      let tannot = into_register (Some(([],t),External (Some i),[],pure_e)) in 
+      let tannot = into_register d_env (Some(([],t),External (Some i),[],pure_e)) in
       (DEF_aux(def,(l,tannot)),(Env(d_env,Envmap.insert t_env (i,tannot))))
 
 
diff --git a/src/type_internal.ml b/src/type_internal.ml
index 73bd5bc4..932c3057 100644
--- a/src/type_internal.ml
+++ b/src/type_internal.ml
@@ -215,7 +215,8 @@ let rec t_subst s_env t =
   | Tvar i -> (match Envmap.apply s_env i with
                | Some(TA_typ t1) -> t1
                | _ -> t)
-  | Tid _ | Tuvar _ -> t
+  | Tuvar _ -> new_t ()
+  | Tid _ -> t
   | Tfn(t1,t2,e) -> {t =Tfn((t_subst s_env t1),(t_subst s_env t2),(e_subst s_env e)) }
   | Ttup(ts) -> { t= Ttup(List.map (t_subst s_env) ts) }
   | Tapp(i,args) -> {t= Tapp(i,List.map (ta_subst s_env) args)}
@@ -230,7 +231,8 @@ and n_subst s_env n =
   | Nvar i -> (match Envmap.apply s_env i with
                | Some(TA_nexp n1) -> n1
                | _ -> n)
-  | Nconst _ | Nuvar _ -> n
+  | Nuvar _ -> new_n ()
+  | Nconst _ -> n
   | N2n n1 -> { nexp = N2n (n_subst s_env n1) }
   | Nneg n1 -> { nexp = Nneg (n_subst s_env n1) }
   | Nadd(n1,n2) -> { nexp = Nadd(n_subst s_env n1,n_subst s_env n2) }
@@ -240,12 +242,14 @@ and o_subst s_env o =
   | Ovar i -> (match Envmap.apply s_env i with
                | Some(TA_ord o1) -> o1
                | _ -> o)
+  | Ouvar _ -> new_o ()
   | _ -> o
 and e_subst s_env e =
   match e.effect with
   | Evar i -> (match Envmap.apply s_env i with
                | Some(TA_eft e1) -> e1
                | _ -> e)
+  | Euvar _ -> new_e ()
   | _ -> e
 
 let rec cs_subst t_env cs =