diff options
| author | Kathy Gray | 2014-07-04 14:53:27 +0100 |
|---|---|---|
| committer | Kathy Gray | 2014-07-04 14:53:36 +0100 |
| commit | 04934f061ed5dac10d112bdfd3fcbec7e8849dc3 (patch) | |
| tree | eca24ea71463593a77c5acec6129bb39b6b056a2 /src | |
| parent | 8522c1dbf5fc7b739a89873a1d86d45b11bc136f (diff) | |
Correct error of forgetting type information that was allowing more programs than it should have
Diffstat (limited to 'src')
| -rw-r--r-- | src/test/test3.sail | 2 | ||||
| -rw-r--r-- | src/type_check.ml | 12 | ||||
| -rw-r--r-- | src/type_internal.ml | 2 |
3 files changed, 11 insertions, 5 deletions
diff --git a/src/test/test3.sail b/src/test/test3.sail index 3a806f41..e2dbe2f3 100644 --- a/src/test/test3.sail +++ b/src/test/test3.sail @@ -27,7 +27,7 @@ function nat main _ = { (* 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; + (*(MEM_WORD(0))[4..3] := 0b10;*) (*We reject this as 4 > 3 not <= *) ignore(MEM_WORD(0)); (* infix call *) diff --git a/src/type_check.ml b/src/type_check.ml index 3ce90f28..f8ec0642 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -1181,11 +1181,19 @@ and check_lexp envs is_top (LEXP_aux(lexp,(l,annot))) : (tannot lexp * typ * tan let base_e1,range_e1,base_e2,range_e2 = new_n(),new_n(),new_n(),new_n() in let base_t = {t=Tapp("range",[TA_nexp base_e1;TA_nexp range_e1])} in let range_t = {t=Tapp("range",[TA_nexp base_e2;TA_nexp range_e2])} in + let (e1',base_t',_,cs1,ef_e) = check_exp envs base_t e1 in + let (e2',range_t',_,cs2,ef_e') = check_exp envs range_t e2 in + let base_e1,range_e1,base_e2,range_e2 = match base_t'.t,range_t'.t with + | (Tapp("range",[TA_nexp base_e1;TA_nexp range_e1]), + Tapp("range",[TA_nexp base_e2;TA_nexp range_e2])) -> base_e1,range_e1,base_e2,range_e2 + | _ -> base_e1,range_e1,base_e2,range_e2 in let cs_t,res_t = match ord.order with | Oinc -> ([LtEq((Expr l),base,base_e1); LtEq((Expr l),{nexp=Nadd(base_e1,range_e1)},{nexp=Nadd(base_e2,range_e2)}); LtEq((Expr l),{nexp=Nadd(base_e1,range_e2)},{nexp=Nadd(base,rise)})], - {t=Tapp("vector",[TA_nexp base_e1;TA_nexp {nexp=Nadd(base_e2,range_e2)};TA_ord ord;TA_typ t])}) + {t=Tapp("vector",[TA_nexp base_e1; + TA_nexp {nexp = Nadd({nexp = Nadd({nexp=Nadd(base_e2,range_e2)},{nexp = Nconst one})}, + {nexp=Nneg base_e1})};TA_ord ord;TA_typ t])}) | Odec -> ([GtEq((Expr l),base,base_e1); GtEq((Expr l),{nexp=Nadd(base_e1,range_e1)},{nexp=Nadd(base_e2,range_e2)}); GtEq((Expr l),{nexp=Nadd(base_e1,range_e2)},{nexp=Nadd(base,{nexp=Nneg rise})})], @@ -1194,8 +1202,6 @@ and check_lexp envs is_top (LEXP_aux(lexp,(l,annot))) : (tannot lexp * typ * tan TA_ord ord; TA_typ t])}) | _ -> typ_error l ("Assignment to a range of vector elements requires either inc or dec order") in - let (e1',t',_,cs1,ef_e) = check_exp envs base_t e1 in - let (e2',t',_,cs2,ef_e') = check_exp envs range_t e2 in 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,Base(([],item_t),tag,cs,ef))),res_t,env,tag,cs,ef) diff --git a/src/type_internal.ml b/src/type_internal.ml index 31aa1e4b..72d58728 100644 --- a/src/type_internal.ml +++ b/src/type_internal.ml @@ -1338,7 +1338,7 @@ let rec type_consistent_internal co d_env t1 cs1 t2 cs2 = | Tapp("range",[TA_nexp b1;TA_nexp r1;]),Tapp("range",[TA_nexp b2;TA_nexp r2;]) -> if (nexp_eq b1 b2)&&(nexp_eq r1 r2) then (t2,csp) - else (t2, csp@[GtEq(co,b1,b2);LtEq(co,r1,r2)]) + else (t1, csp@[GtEq(co,b1,b2);LtEq(co,r1,r2)]) | Tapp(id1,args1), Tapp(id2,args2) -> let la1,la2 = List.length args1, List.length args2 in if id1=id2 && la1 = la2 |