More coercions

3 files changed, 31 insertions, 16 deletions

diff --git a/src/test/regbits.sail b/src/test/regbits.sail
index 5bc799bb..0a41280d 100644
--- a/src/test/regbits.sail
+++ b/src/test/regbits.sail
@@ -6,14 +6,14 @@
  }
 
 register (xer) XER
-register (bit[1]) query
+register (bit) query
 
 function (bit[64]) main _ = {
   XER := 0b010101010101010101010101010101010101010101010101010101010101001;
   f := XER;
   (bit[7]) foo := XER[57..63];
   query := XER.SO;
-  XER.SO := bitone;
+  XER.SO := 0;
   XER.FOOBAR := 0b11;
   XER }
 
diff --git a/src/type_check.ml b/src/type_check.ml
index 1aa2ea1a..ccf079d0 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -1120,21 +1120,20 @@ let check_type_def envs (TD_aux(td,(l,annot))) =
 	    let franges = 
 	      List.map 
 		(fun ((BF_aux(idx,l)),id) ->
-		  let (base,climb) =
-		    match idx with
-		      | BF_single i -> 
-			if b <= i && i <= t 
-			then {nexp=Nconst i},{nexp=Nconst 0}
-			else typ_error l ("register type declaration " ^ id' ^ " contains a field specification outside of the declared register size")
-		      | BF_range(i1,i2) -> 
-			if i1<i2 
-			then if b<=i1 && i2<=t 
-			  then {nexp=Nconst i1},{nexp=Nconst (i2 - i1)}
-			  else typ_error l ("register type declaration " ^ id' ^ " contains a field specification outside of the declared register size")
-			else typ_error l ("register type declaration " ^ id' ^ " is not consistently increasing")
-		      | BF_concat _ -> assert false (* What is this supposed to imply again?*) in
 		  ((id_to_string id),
-		   Some(([],{t=Tapp("vector",[TA_nexp base;TA_nexp climb;TA_ord({order=Oinc});TA_typ({t= Tid "bit"})])}),Emp,[],pure_e)))
+		   Some(([],
+			match idx with
+			  | BF_single i -> 
+			    if b <= i && i <= t 
+			    then {t = Tid "bit"}
+			    else typ_error l ("register type declaration " ^ id' ^ " contains a field specification outside of the declared register size")
+			  | BF_range(i1,i2) -> 
+			    if i1<i2 
+			    then if b<=i1 && i2<=t 
+			      then {t=Tapp("vector",[TA_nexp {nexp=Nconst i1}; TA_nexp {nexp=Nconst (i2 - i1)}; TA_ord({order=Oinc}); TA_typ {t=Tid "bit"}])}
+			      else typ_error l ("register type declaration " ^ id' ^ " contains a field specification outside of the declared register size")
+			    else typ_error l ("register type declaration " ^ id' ^ " is not consistently increasing")
+			  | BF_concat _ -> assert false (* What is this supposed to imply again?*)),Emp,[],pure_e)))
 		ranges 
 	    in
 	    let tannot = into_register d_env (Some(([],ty),Emp,[],pure_e)) in
diff --git a/src/type_internal.ml b/src/type_internal.ml
index 13c20e9f..795971e3 100644
--- a/src/type_internal.ml
+++ b/src/type_internal.ml
@@ -575,6 +575,22 @@ let rec type_coerce_internal l d_env t1 cs1 e t2 cs2 =
 	| _ -> raise (Reporting_basic.err_unreachable l "register is not properly kinded"))
     | _,_ -> 
       let t',cs' = type_consistent l d_env t1 t2 in (t',cs',e))
+  | Tid("bit"),Tapp("vector",[TA_nexp {nexp=Nconst i};TA_nexp r1;TA_ord o;TA_typ {t=Tid "bit"}]) ->
+    let cs = [Eq(l,r1,{nexp = Nconst 1})] in
+    (t2,cs,E_aux(E_vector_indexed [(i,e)],(l,Some(([],t2),Emp,cs,pure_e))))    
+  | Tapp("vector",[TA_nexp ({nexp=Nconst i} as b1);TA_nexp r1;TA_ord o;TA_typ {t=Tid "bit"}]),Tid("bit") ->
+    let cs = [Eq(l,r1,{nexp = Nconst 1})] in
+    (t2,cs,E_aux((E_vector_access (e,(E_aux(E_lit(L_aux(L_num i,l)),(l,Some(([],{t=Tapp("enum",[TA_nexp b1;TA_nexp {nexp=Nconst 0}])}),Emp,cs,pure_e)))))),
+                 (l,Some(([],t2),Emp,cs,pure_e))))
+  | Tid("bit"),Tapp("enum",[TA_nexp b1;TA_nexp r1]) ->
+    let t',cs'= type_consistent l d_env {t=Tapp("enum",[TA_nexp{nexp=Nconst 0};TA_nexp{nexp=Nconst 1}])} t2 in
+    (t2,cs',E_aux(E_case (e,[Pat_aux(Pat_exp(P_aux(P_lit(L_aux(L_zero,l)),(l,Some(([],t1),Emp,[],pure_e))),
+					     E_aux(E_lit(L_aux(L_num 0,l)),(l,Some(([],t2),Emp,[],pure_e)))),
+				     (l,Some(([],t2),Emp,[],pure_e)));
+			     Pat_aux(Pat_exp(P_aux(P_lit(L_aux(L_one,l)),(l,Some(([],t1),Emp,[],pure_e))),
+					     E_aux(E_lit(L_aux(L_num 1,l)),(l,Some(([],t2),Emp,[],pure_e)))),
+				     (l,Some(([],t2),Emp,[],pure_e)));]),
+		  (l,Some(([],t2),Emp,[],pure_e))))    
   | Tapp("enum",[TA_nexp b1;TA_nexp r1;]),Tid("bit") ->
     let t',cs'= type_consistent l d_env t1 {t=Tapp("enum",[TA_nexp{nexp=Nconst 0};TA_nexp{nexp=Nconst 1}])} 
     in (t2,cs',E_aux(E_if(E_aux(E_app(Id_aux(Id "is_zero",l),[e]),(l,Some(([],bool_t),Emp,[],pure_e))),