document coercions

1 files changed, 71 insertions, 14 deletions

diff --git a/src/type_internal.ml b/src/type_internal.ml
index 85783ada..a8951836 100644
--- a/src/type_internal.ml
+++ b/src/type_internal.ml
@@ -3356,6 +3356,12 @@ let rec type_coerce_internal co d_env enforce is_explicit widen bounds t1 cs1 e
   (*let _ = Printf.eprintf "called type_coerce_internal is_explicit %b, widen %b, turning %s with actual %s into %s with actual %s\n" 
     is_explicit widen (t_to_string t1) (t_to_string t1_actual) (t_to_string t2) (t_to_string t2_actual) in*)
   match t1_actual.t,t2_actual.t with
+
+    (* Toptions is an internal constructor representing the type we're
+    going to be casting to and the natural type.  source-language type
+    annotations might be demanding a coercion, so this checks
+    conformance and adds a coercion if needed *)
+
   | Toptions(to1,Some to2),_ -> 
     if (conforms_to_t d_env false true to1 t2_actual || conforms_to_t d_env false true to2 t2_actual)
     then begin t1_actual.t <- t2_actual.t; (t2,csp,pure_e,e) end
@@ -3368,12 +3374,17 @@ let rec type_coerce_internal co d_env enforce is_explicit widen bounds t1 cs1 e
   | _,Toptions(to1,Some to2) -> 
     if (conforms_to_t d_env false true to1 t1_actual || conforms_to_t d_env false true to2 t1_actual)
     then begin t2_actual.t <- t1_actual.t; (t1,csp,pure_e,e) end
-    else eq_error l ((t_to_string t1) ^ " can match neither expexted type " ^
+    else eq_error l ((t_to_string t1) ^ " can match neither expected type " ^
                         (t_to_string to1) ^ " nor " ^ (t_to_string to2))
   | _,Toptions(to1,None) -> 
     if is_explicit
     then type_coerce_internal co d_env enforce is_explicit widen bounds t1_actual cs1 e to1 cs2
     else (t1,csp,pure_e,e)
+
+        (* recursive coercions to components of tuples.  They may be
+        complex expressions, not top-level tuples, so we sometimes
+        need to add a pattern match. At present we do that almost
+        always, unnecessarily often.  The any_coerced is wrong *)
   | Ttup t1s, Ttup t2s ->
     let tl1,tl2 = List.length t1s,List.length t2s in
     if tl1=tl2 then 
@@ -3402,10 +3413,16 @@ let rec type_coerce_internal co d_env enforce is_explicit widen bounds t1 cs1 e
            (t2,csp@cs,efs,e')
     else eq_error l ("Found a tuple of length " ^ (string_of_int tl1) ^
                      " but expected a tuple of length " ^ (string_of_int tl2))
+
+
+        (* all the Tapp cases *)
   | Tapp(id1,args1),Tapp(id2,args2) ->
     if id1=id2 && (id1 <> "vector")
+        (* no coercion needed, so fall back to consistency *)
     then let t',cs' = type_consistent co d_env enforce widen t1 t2 in (t',cs',pure_e,e)
     else (match id1,id2,is_explicit with
+
+      (* can coerce between two vectors just to change the start index *)
     | "vector","vector",_ ->
       (match args1,args2 with
       | [TA_nexp b1;TA_nexp r1;TA_ord o1;TA_typ t1i],
@@ -3421,6 +3438,8 @@ let rec type_coerce_internal co d_env enforce is_explicit widen bounds t1 cs1 e
         let e' = E_aux(E_internal_cast ((l,(Base(([],t2),Emp_local,[],pure_e,pure_e,nob))),e),(l,tannot)) in
         (t2,cs@cs',pure_e,e')
       | _ -> raise (Reporting_basic.err_unreachable l "vector is not properly kinded"))
+
+          (* coercion from a bit vector into a number *)
     | "vector","range",_ -> 
       (match args1,args2 with
       | [TA_nexp b1;TA_nexp r1;TA_ord _;TA_typ {t=Tid "bit"}],
@@ -3435,6 +3454,8 @@ let rec type_coerce_internal co d_env enforce is_explicit widen bounds t1 cs1 e
       | [TA_nexp b1;TA_nexp r1;TA_ord o;TA_typ t],_ -> 
         eq_error l "Cannot convert non-bit vector into an range"
       | _,_ -> raise (Reporting_basic.err_unreachable l "vector or range is not properly kinded"))
+
+          (* similar to vector/range case *)
     | "vector","atom",_ -> 
       (match args1,args2 with
       | [TA_nexp b1;TA_nexp r1;TA_ord _;TA_typ {t=Tid "bit"}],
@@ -3447,6 +3468,9 @@ let rec type_coerce_internal co d_env enforce is_explicit widen bounds t1 cs1 e
       | [TA_nexp b1;TA_nexp r1;TA_ord o;TA_typ t],_ -> 
         eq_error l "Cannot convert non-bit vector into an range"
       | _,_ -> raise (Reporting_basic.err_unreachable l "vector or range is not properly kinded"))
+
+          (* coercion from number into bit vector, if there's an explicit type annotation in the source (the "true") *)
+          (* this can be lossy, if it doesn't fit into that vector, so we want to require the user to specify the vector size. It was desired by some users, but maybe should be turned back into an error and an explicit truncate function be used *)
     | "range","vector",true -> 
       (match args2,args1 with
       | [TA_nexp b1;TA_nexp r1;TA_ord {order = Oinc};TA_typ {t=Tid "bit"}],
@@ -3470,6 +3494,8 @@ let rec type_coerce_internal co d_env enforce is_explicit widen bounds t1 cs1 e
       | [TA_nexp b1;TA_nexp r1;TA_ord o;TA_typ t],_ -> 
         eq_error l "Cannot convert a range into a non-bit vector"
       | _,_ -> raise (Reporting_basic.err_unreachable l "vector or range is not properly kinded"))
+
+          (* similar to number to bit vector case *)
     | "atom","vector",true -> 
       (match args2,args1 with
       | [TA_nexp b1;TA_nexp r1;TA_ord {order = Oinc};TA_typ {t=Tid "bit"}],
@@ -3492,6 +3518,8 @@ let rec type_coerce_internal co d_env enforce is_explicit widen bounds t1 cs1 e
       | [TA_nexp b1;TA_nexp r1;TA_ord o;TA_typ t],_ -> 
         eq_error l "Cannot convert a range into a non-bit vector"
       | _,_ -> raise (Reporting_basic.err_unreachable l "vector or range is not properly kinded"))
+
+          (* implicit dereference of a register, from register<t> to t, and then perhaps also from t to the expected type *)
     | "register",_,_ ->
       (match args1 with
         | [TA_typ t] ->
@@ -3507,16 +3535,24 @@ let rec type_coerce_internal co d_env enforce is_explicit widen bounds t1 cs1 e
           let (t',cs,ef',e) = type_coerce co d_env Guarantee is_explicit widen bounds t new_e t2 in
           (t',cs,union_effects ef ef',e)
         | _ -> raise (Reporting_basic.err_unreachable l "register is not properly kinded"))
+
+          (* otherwise in Tapp case, fall back on type_consistent *)
     | _,_,_ -> 
       let t',cs' = type_consistent co d_env enforce widen t1 t2 in (t',cs',pure_e,e))
+
+        (* bit vector of length 1 to bit *)
   | Tapp("vector",[TA_nexp b1;TA_nexp r1;TA_ord o;TA_typ {t=Tid "bit"}]),Tid("bit") ->
     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)))))
+
+      (* bit to a bitvector of length 1 *)
   | 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)))))
+
+      (* bit to a number range (including 0..1) *)
   | 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,
@@ -3527,6 +3563,9 @@ let rec type_coerce_internal co d_env enforce is_explicit widen bounds t1 cs1 e
                                       E_aux(E_lit(L_aux(L_num 1,l)),(l,simple_annot t2))),
                               (l,simple_annot t2));]),
            (l,simple_annot_efr t2 (get_cummulative_effects (get_eannot e)))))   
+
+
+      (* similar to above, bit to a singleton number range *)
   | Tid("bit"),Tapp("atom",[TA_nexp b1]) ->
     let t',cs'= type_consistent co d_env enforce false t2 {t=Tapp("range",[TA_nexp n_zero;TA_nexp n_one])} in
     (t2,cs',pure_e,
@@ -3537,6 +3576,9 @@ let rec type_coerce_internal co d_env enforce is_explicit widen bounds t1 cs1 e
                                       E_aux(E_lit(L_aux(L_num 1,l)),(l,simple_annot t2))),
                               (l,simple_annot t2));]),
            (l,simple_annot_efr t2 (get_cummulative_effects (get_eannot e)))))
+
+
+      (* number range to a bit *)
   | Tapp("range",[TA_nexp b1;TA_nexp r1;]),Tid("bit") ->
     let t',cs'= type_consistent co d_env enforce false t1 {t=Tapp("range",[TA_nexp n_zero;TA_nexp n_one])} in
     let efr = get_cummulative_effects (get_eannot e)
@@ -3545,6 +3587,8 @@ let rec type_coerce_internal co d_env enforce is_explicit widen bounds t1 cs1 e
                                  E_aux(E_lit(L_aux(L_one,l)),(l,simple_annot bit_t)),
                                  E_aux(E_lit(L_aux(L_zero,l)),(l,simple_annot bit_t))),
                             (l,simple_annot_efr bit_t efr)))
+
+      (* similar to above *)
   | Tapp("atom",[TA_nexp b1]),Tid("bit") ->
     let t',cs'= type_consistent co d_env enforce false t1 {t=Tapp("range",[TA_nexp n_zero;TA_nexp n_one])} in
     let efr = get_cummulative_effects (get_eannot e)
@@ -3552,6 +3596,8 @@ let rec type_coerce_internal co d_env enforce is_explicit widen bounds t1 cs1 e
                                  E_aux(E_lit(L_aux(L_one,l)),(l,simple_annot bit_t)),
                                  E_aux(E_lit(L_aux(L_zero,l)),(l,simple_annot bit_t))),
                             (l,simple_annot_efr bit_t efr)))
+
+      (* number range to an enumeration type *)
   | Tapp("range",[TA_nexp b1;TA_nexp r1;]),Tid(i) -> 
     (match Envmap.apply d_env.enum_env i with
     | Some(enums) -> 
@@ -3564,6 +3610,23 @@ let rec type_coerce_internal co d_env enforce is_explicit widen bounds t1 cs1 e
                                                   (l,simple_annot t2))) enums),
              (l,simple_annot_efr t2 (get_cummulative_effects (get_eannot e)))))
     | None -> eq_error l ("Type mismatch: found a " ^ (t_to_string t1) ^ " but expected " ^ (t_to_string t2)))
+
+        (* similar to above *)
+  | Tapp("atom",[TA_nexp b1]),Tid(i) -> 
+    (match Envmap.apply d_env.enum_env i with
+      | Some(enums) -> 
+        let num_enums = List.length enums in
+        (t2,[GtEq(co,Require,b1,n_zero);
+             LtEq(co,Require,b1,mk_c(big_int_of_int num_enums))],pure_e,
+         E_aux(E_case(e,
+                      List.mapi (fun i a -> Pat_aux(Pat_exp(P_aux(P_lit(L_aux((L_num i),l)),(l, simple_annot t1)),
+                                                            E_aux(E_id(Id_aux(Id a,l)),
+                                                                  (l, tag_annot t2 (Enum num_enums)))),
+                                                    (l,simple_annot t2))) enums),
+               (l,simple_annot_efr t2 (get_cummulative_effects (get_eannot e)))))
+      | None -> eq_error l ("Type mismatch: found a " ^ (t_to_string t1) ^ " but expected " ^ (t_to_string t2)))
+
+        (* bit vector to an enumeration type *)
   | Tapp("vector", [TA_nexp _; TA_nexp size; _; TA_typ {t= Tid "bit"}]), Tid(i) ->
     (match Envmap.apply d_env.enum_env i with
      | Some(enums) ->
@@ -3579,19 +3642,8 @@ let rec type_coerce_internal co d_env enforce is_explicit widen bounds t1 cs1 e
                                                     (l,simple_annot t2))) enums),
               (l,simple_annot_efr t2 (get_cummulative_effects (get_eannot e)))))
      | None -> eq_error l ("Type mismatch: found a " ^ (t_to_string t1) ^ " but expected " ^ (t_to_string t2)))
-  | Tapp("atom",[TA_nexp b1]),Tid(i) -> 
-    (match Envmap.apply d_env.enum_env i with
-      | Some(enums) -> 
-        let num_enums = List.length enums in
-        (t2,[GtEq(co,Require,b1,n_zero);
-             LtEq(co,Require,b1,mk_c(big_int_of_int num_enums))],pure_e,
-         E_aux(E_case(e,
-                      List.mapi (fun i a -> Pat_aux(Pat_exp(P_aux(P_lit(L_aux((L_num i),l)),(l, simple_annot t1)),
-                                                            E_aux(E_id(Id_aux(Id a,l)),
-                                                                  (l, tag_annot t2 (Enum num_enums)))),
-                                                    (l,simple_annot t2))) enums),
-               (l,simple_annot_efr t2 (get_cummulative_effects (get_eannot e)))))
-      | None -> eq_error l ("Type mismatch: found a " ^ (t_to_string t1) ^ " but expected " ^ (t_to_string t2)))
+
+        (* enumeration type to number range *)
   | Tid(i),Tapp("range",[TA_nexp b1;TA_nexp r1;]) -> 
     (match Envmap.apply d_env.enum_env i with
     | Some(enums) -> 
@@ -3602,6 +3654,11 @@ let rec type_coerce_internal co d_env enforce is_explicit widen bounds t1 cs1 e
                                                   (l,simple_annot t2))) enums),
              (l,simple_annot_efr t2 (get_cummulative_effects (get_eannot e)))))
     | None -> eq_error l ("Type mismatch: " ^ (t_to_string t1) ^ " , " ^ (t_to_string t2)))
+
+
+        (* probably there's a missing enumeration type to singleton number range *)
+
+        (* fall through to type_consistent *)
   | _,_ -> let t',cs = type_consistent co d_env enforce widen t1 t2 in (t',cs,pure_e,e)
 
 and type_coerce co d_env enforce is_explicit widen bounds t1 e t2 =