From 42f6ee722ff2b9f49a0b981c0d43aed761098277 Mon Sep 17 00:00:00 2001 From: Kathy Gray Date: Mon, 17 Mar 2014 17:37:36 +0000 Subject: More coercions --- src/test/regbits.sail | 4 ++-- src/type_check.ml | 27 +++++++++++++-------------- src/type_internal.ml | 16 ++++++++++++++++ 3 files changed, 31 insertions(+), 16 deletions(-) (limited to 'src') 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 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 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))), -- cgit v1.2.3