diff options
| author | Kathy Gray | 2015-03-04 15:00:32 +0000 |
|---|---|---|
| committer | Kathy Gray | 2015-03-04 15:00:32 +0000 |
| commit | ab466ba3331a5dbbf3967c29a2a5d7468eb4d763 (patch) | |
| tree | 462ae3edbf4c89d43c3cfeaf62554685a72c5e85 | |
| parent | ef0b2daa613c81f2ea42168023fd70e6f6dee187 (diff) | |
Fix off-by-one constraint error on vector to number coercions
| -rw-r--r-- | src/type_internal.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/type_internal.ml b/src/type_internal.ml index b8731422..3b7392b6 100644 --- a/src/type_internal.ml +++ b/src/type_internal.ml @@ -2061,11 +2061,11 @@ let rec type_coerce_internal co d_env is_explicit widen t1 cs1 e t2 cs2 = (match args1,args2 with | [TA_nexp b1;TA_nexp r1;TA_ord {order = Oinc};TA_typ {t=Tid "bit"}], [TA_nexp b2;TA_nexp r2;] -> - let cs = [Eq(co,b2,n_zero);GtEq(co,r2,{nexp=N2n(r1,None)})] in + let cs = [Eq(co,b2,n_zero);GtEq(co,r2,{nexp = Nadd({nexp=N2n(r1,None)},{nexp = Nneg n_one})})] in (t2,cs,pure_e,E_aux(E_app((Id_aux(Id "to_num_inc",l)),[e]),(l,Base(([],t2),External None,cs,pure_e,nob)))) | [TA_nexp b1;TA_nexp r1;TA_ord {order = Odec};TA_typ {t=Tid "bit"}], [TA_nexp b2;TA_nexp r2;] -> - let cs = [Eq(co,b2,n_zero);GtEq(co,r2,{nexp=N2n(r1,None)})] in + let cs = [Eq(co,b2,n_zero);GtEq(co,r2,{nexp = Nadd({nexp=N2n(r1,None)},{nexp = Nneg n_one})})] in (t2,cs,pure_e,E_aux(E_app((Id_aux(Id "to_num_dec",l)),[e]),(l,Base(([],t2),External None,cs,pure_e,nob)))) | [TA_nexp b1;TA_nexp r1;TA_ord {order = Ovar o};TA_typ {t=Tid "bit"}],_ -> eq_error l "Cannot convert a vector to an range without an order" |