diff options
| author | Kathy Gray | 2016-07-25 13:57:48 +0100 |
|---|---|---|
| committer | Kathy Gray | 2016-07-25 13:57:48 +0100 |
| commit | e393e35b394b4d5def97f476818f63d0a7aa0cbc (patch) | |
| tree | 061f70bc513e3a2d2072c5065d1d6c4bd0adc55d /src | |
| parent | c2694d69cc4b8fe2a956bf60fd9b9061ac775bc0 (diff) | |
auto coerce to bit vector from bit
pretty print lret effects into lem
Diffstat (limited to 'src')
| -rw-r--r-- | src/pretty_print.ml | 1 | ||||
| -rw-r--r-- | src/type_internal.ml | 8 |
2 files changed, 7 insertions, 2 deletions
diff --git a/src/pretty_print.ml b/src/pretty_print.ml index 24906734..6680ef60 100644 --- a/src/pretty_print.ml +++ b/src/pretty_print.ml @@ -151,6 +151,7 @@ and pp_format_base_effect_lem (BE_aux(e,l)) = | BE_unspec -> "BE_unspec" | BE_nondet -> "BE_nondet" | BE_lset -> "BE_lset" + | BE_lret -> "BE_lret" | BE_escape -> "BE_escape") ^ " " ^ (pp_format_l_lem l) ^ ")" and pp_format_effects_lem (Effect_aux(e,l)) = diff --git a/src/type_internal.ml b/src/type_internal.ml index 8047b61a..31023efa 100644 --- a/src/type_internal.ml +++ b/src/type_internal.ml @@ -3369,7 +3369,8 @@ let rec type_coerce_internal co d_env enforce is_explicit widen bounds t1 cs1 e (match args2,args1 with | [TA_nexp b1;TA_nexp r1;TA_ord {order = Oinc};TA_typ {t=Tid "bit"}], [TA_nexp b2;TA_nexp r2;] -> - let cs = [] (*[LtEq(co,Guarantee,r2,mk_sub {nexp=N2n(r1,None)} n_one)] (*This constraint failing should be a warning, but truncation is ok*)*) in + let cs = [] (*[LtEq(co,Guarantee,r2,mk_sub {nexp=N2n(r1,None)} n_one)] + (*This constraint failing should be a warning, but truncation is ok*)*) in let tannot = (l, Base(([],t2), External (Some "to_vec_inc"), cs, pure_e, (get_cummulative_effects (get_eannot e)), bounds)) in (t2,cs,pure_e,E_aux(E_app((Id_aux(Id "to_vec_inc",l)), @@ -3430,7 +3431,10 @@ let rec type_coerce_internal co d_env enforce is_explicit widen bounds t1 cs1 e let cs = [Eq(co,r1,n_one)] in (t2,cs,pure_e,E_aux((E_app ((Id_aux (Id "most_significant", l)), [e])), (l, cons_tag_annot_efr t2 (External (Some "most_significant")) - cs (get_cummulative_effects (get_eannot e))))) + cs (get_cummulative_effects (get_eannot e))))) + | Tid("bit"),Tapp("vector",[TA_nexp b1;TA_nexp r1;TA_ord o;TA_typ {t=Tid "bit"}]) -> + let cs = [Eq(co,r1,n_one)] in + (t2,cs,pure_e,E_aux(E_vector [e], (l, constrained_annot_efr t2 cs (get_cummulative_effects (get_eannot e))))) | Tid("bit"),Tapp("range",[TA_nexp b1;TA_nexp r1]) -> let t',cs'= type_consistent co d_env enforce false {t=Tapp("range",[TA_nexp n_zero;TA_nexp n_one])} t2 in (t2,cs',pure_e, |