diff options
| author | Kathy Gray | 2014-02-06 16:13:12 +0000 |
|---|---|---|
| committer | Kathy Gray | 2014-02-06 16:13:12 +0000 |
| commit | ede2cc7a69f8d025353ee9df75eca7da8a3cd0c3 (patch) | |
| tree | 578ae7e5e0d3fe2672b2ff0a5e7ac5c04d46d0e1 | |
| parent | eedfe41a826a0a54fcc69fa32d1ad4286f9c9318 (diff) | |
coerce bit to bool when not a literal bit. Note: this will only add a conversion function for expressions of bit type, an explicit cast to bit would be needed to come from an enum or nat.
| -rw-r--r-- | src/type_internal.ml | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/src/type_internal.ml b/src/type_internal.ml index 80aee5cb..b1baa982 100644 --- a/src/type_internal.ml +++ b/src/type_internal.ml @@ -497,6 +497,9 @@ let rec type_coerce l d_env t1 e t2 = (l,Some(([],t2),Emp,[],pure_e)))) enums), (l,Some(([],t2),Emp,[],pure_e)))) | None -> eq_error l ("Type mismatch: " ^ (t_to_string t1) ^ " , " ^ (t_to_string t2)))) + | Tid("bit"),Tid("bool") -> + let e' = E_aux(E_app((Id_aux(Id "is_one",l)),[e]),(l,Some(([],bool_t),External,[],pure_e))) in + (t2,[],e') | Tid(i),Tapp("enum",[TA_nexp b1;TA_nexp r1;]) -> (match get_abbrev d_env t1 with | Some(t1,cs1,ef1) -> |