diff options
| author | Kathy Gray | 2014-11-24 18:45:28 +0000 |
|---|---|---|
| committer | Kathy Gray | 2014-11-24 18:45:28 +0000 |
| commit | 623cd571bb9dde646e47951f9827bc3d7fa3a2ac (patch) | |
| tree | f061686f17f8fe052edae45f336aabb660b8d289 | |
| parent | 12d3b1f8d7a8393b0b905e5cf6e62753f5032f6f (diff) | |
Correctly cast between 1 and a single bit
| -rw-r--r-- | src/lem_interp/interp_lib.lem | 6 | ||||
| -rw-r--r-- | src/type_check.ml | 12 |
2 files changed, 10 insertions, 8 deletions
diff --git a/src/lem_interp/interp_lib.lem b/src/lem_interp/interp_lib.lem index 9ee54b16..aca430cb 100644 --- a/src/lem_interp/interp_lib.lem +++ b/src/lem_interp/interp_lib.lem @@ -43,8 +43,10 @@ let rec fill_in_sparse v = match v with end let is_one v = match v with - | V_lit (L_aux b lb) -> V_lit (L_aux (if b = L_one then L_true else L_false) lb) - | V_track (V_lit (L_aux b lb)) r -> V_track (V_lit (L_aux (if b = L_one then L_true else L_false) lb)) r + | V_lit (L_aux (L_num n) lb) -> V_lit (L_aux (if n=1 then L_one else L_zero) lb) + | V_track (V_lit (L_aux (L_num n) lb)) r -> V_track (V_lit (L_aux (if n=1 then L_one else L_zero) lb)) r + | V_lit (L_aux b lb) -> V_lit (L_aux (if b = L_one then L_one else L_zero) lb) + | V_track (V_lit (L_aux b lb)) r -> V_track (V_lit (L_aux (if b = L_one then L_one else L_zero) lb)) r | V_track V_unkown _ -> v | V_unknown -> v end ;; diff --git a/src/type_check.ml b/src/type_check.ml index 3ad382d4..73b66e6e 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -500,23 +500,23 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)): | L_unit -> (rebuild (Base (([],unit_t), Emp_local,[],pure_e))),[],pure_e | L_zero -> (match expect_t.t with - | Tid "bool" -> simp_exp (E_lit(L_aux(L_false,l'))) l bool_t,[],pure_e + | Tid "bool" -> simp_exp (E_lit(L_aux(L_zero,l'))) l bool_t,[],pure_e | _ -> simp_exp e l bit_t,[],pure_e) | L_one -> (match expect_t.t with - | Tid "bool" -> simp_exp (E_lit(L_aux(L_true,l'))) l bool_t,[],pure_e + | Tid "bool" -> simp_exp (E_lit(L_aux(L_one,l'))) l bool_t,[],pure_e | _ -> simp_exp e l bit_t,[],pure_e) | L_true -> simp_exp e l bool_t,[],pure_e | L_false -> simp_exp e l bool_t,[],pure_e | L_num i -> (match expect_t.t with - | Tid "bit" -> + | Tid "bit" | Toptions({t=Tid"bit"},_) -> if i = 0 then simp_exp (E_lit(L_aux(L_zero,l'))) l bit_t,[],pure_e else if i = 1 then simp_exp (E_lit(L_aux(L_one,l'))) l bit_t,[],pure_e else typ_error l ("Expected a bit, found " ^ string_of_int i) - | Tid "bool" -> - if i = 0 then simp_exp (E_lit(L_aux(L_false,l'))) l bool_t,[],pure_e - else if i = 1 then simp_exp (E_lit(L_aux(L_true,l'))) l bool_t ,[],pure_e + | Tid "bool" | Toptions({t=Tid"bool"},_)-> + if i = 0 then simp_exp (E_lit(L_aux(L_zero,l'))) l bit_t,[],pure_e + else if i = 1 then simp_exp (E_lit(L_aux(L_one,l'))) l bit_t ,[],pure_e else typ_error l ("Expected bool or a bit, found " ^ string_of_int i) | Tapp ("vector",[TA_nexp base;TA_nexp rise;TA_ord o;(TA_typ {t=Tid "bit"})]) -> let n = {nexp = Nconst (big_int_of_int i) } in |