Ocaml generation now just needing big int/little int issues resolved (probably) at least for Power.

5 files changed, 124 insertions, 41 deletions

diff --git a/src/gen_lib/sail_values.ml b/src/gen_lib/sail_values.ml
index c789ff52..8a1a27c6 100644
--- a/src/gen_lib/sail_values.ml
+++ b/src/gen_lib/sail_values.ml
@@ -15,6 +15,11 @@ let to_bool = function
   | Vone  -> true
   | Vundef -> assert false
 
+let is_one i =
+  if eq_big_int i unit_big_int
+  then Vone
+  else Vzero
+
 let get_barray  = function
   | Vvector(a,_,_) -> a
   | Vregister(a,_,_,_) -> !a
@@ -117,8 +122,8 @@ let set_vector_subrange_vec v n m new_v =
       done;
     end
   in
-  match v with
-  | VvectorR(array,start,is_inc) ->
+  match v, new_v with
+  | VvectorR(array,start,is_inc),VvectorR(new_v,_,_) ->
     let (length,offset) = if is_inc then (m-n+1,n-start) else (n-m+1,start-n) in
     walker array length offset new_v
   | _ -> ()
diff --git a/src/pretty_print.ml b/src/pretty_print.ml
index db49989f..a4042588 100644
--- a/src/pretty_print.ml
+++ b/src/pretty_print.ml
@@ -1447,14 +1447,16 @@ let doc_exp_ocaml, doc_let_ocaml =
            let field_f = match t.t with
              | Tid "bit" | Tabbrev(_,{t=Tid "bit"}) -> string "get_register_field_bit"
              | _ -> string "get_register_field_vec" in
-           parens (separate space [field_f; string reg; string_lit (string field)])
+           parens (separate space [field_f; string (String.uncapitalize reg); string_lit (string field)])
          | Alias_extract(reg,start,stop) ->
            if start = stop
-           then parens (separate space [string "bit_vector_access";string reg;doc_int start])
+           then parens (separate space [string "bit_vector_access";string (String.uncapitalize reg);doc_int start])
            else parens
-               (separate space [string "vector_subrange"; string reg; doc_int start; doc_int stop])
+               (separate space [string "vector_subrange"; string (String.uncapitalize reg); doc_int start; doc_int stop])
          | Alias_pair(reg1,reg2) ->
-           parens (separate space [string "vector_concat"; string reg1; string reg2]))
+           parens (separate space [string "vector_concat";
+                                   string (String.uncapitalize reg1);
+                                   string (String.uncapitalize reg2)]))
       | _ -> doc_id_ocaml id)
     | E_lit lit -> doc_lit_ocaml false lit
     | E_cast(typ,e) ->
@@ -1492,7 +1494,8 @@ let doc_exp_ocaml, doc_let_ocaml =
        | Base((_,t),_,_,_,_,_) ->
          match t.t with
          | Tapp("vector", [TA_nexp start; TA_nexp len; TA_ord order; _])
-         | Tabbrev(_,{t= Tapp("vector", [TA_nexp start; TA_nexp len; TA_ord order; _])}) ->
+         | Tabbrev(_,{t= Tapp("vector", [TA_nexp start; TA_nexp len; TA_ord order; _])})
+         | Tapp("reg", [TA_typ {t =Tapp("vector", [TA_nexp start; TA_nexp len; TA_ord order; _])}]) ->
            let call = if is_bit_vector t then (string "make_indexed_bitv") else (string "make_indexed_v") in
            let dir,dir_out = match order.order with
              | Oinc -> true,"true"
@@ -1571,7 +1574,7 @@ let doc_exp_ocaml, doc_let_ocaml =
   and doc_lexp_ocaml top_call ((LEXP_aux(lexp,(l,annot))) as le) =
     let exp = top_exp false in
     match lexp with
-    | LEXP_vector(v,e) -> parens ((string "vector_access") ^^ space ^^ (doc_lexp_ocaml false v)) ^^ dot ^^ parens (exp e)
+    | LEXP_vector(v,e) -> doc_lexp_array_ocaml le
     | LEXP_vector_range(v,e1,e2) ->
       parens ((string "vector_subrange") ^^ space ^^ (doc_lexp_ocaml false v) ^^ space ^^ (exp e1) ^^ space ^^ (exp e2))
     | LEXP_field(v,id) -> (doc_lexp_ocaml false v) ^^ dot ^^ doc_id_ocaml id
@@ -1601,9 +1604,12 @@ let doc_exp_ocaml, doc_let_ocaml =
       | E_aux(_,(_,Base((_,t),_,_,_,_,_))) ->
         (match t.t with
          | Tapp("vector", [_;_;_;(TA_typ ({t=Tid "bit"} | {t=Tabbrev(_,{t=Tid "bit"})}))]) |
-           Tabbrev(_,{t=Tapp("vector",[_;_;_;TA_typ ({t=Tid "bit"} | {t=Tabbrev(_,{t=Tid "bit"})})])}) ->
+           Tabbrev(_,{t=Tapp("vector",[_;_;_;TA_typ ({t=Tid "bit"} | {t=Tabbrev(_,{t=Tid "bit"})})])}) |
+           Tapp("reg", [TA_typ {t= Tapp("vector", [_;_;_;(TA_typ ({t=Tid "bit"} | {t=Tabbrev(_,{t=Tid "bit"})}))])}])
+           ->
            (false,true)
-         | Tid "bit" | Tabbrev(_,{t=Tid "bit"}) -> (true,false)
+         | Tid "bit" | Tabbrev(_,{t=Tid "bit"}) | Tapp("reg",[TA_typ ({t=Tid "bit"} | {t=Tabbrev(_,{t=Tid "bit"})})])
+           -> (true,false)
          | _ -> (false,false))
       | _ -> (false,false) in
     match lexp with
@@ -1613,7 +1619,7 @@ let doc_exp_ocaml, doc_let_ocaml =
          dot ^^ parens (exp e))
         (exp e_new_v)
     | LEXP_vector_range(v,e1,e2) ->
-      parens ((string (if is_bitv then "set_vector_subrange_bit" else "set_vector_subrange_v")) ^^ space ^^
+      parens ((string (if is_bitv then "set_vector_subrange_bit" else "set_vector_subrange_vec")) ^^ space ^^
               doc_lexp_ocaml false v ^^ space ^^ exp e1 ^^ space ^^ exp e2 ^^ space ^^ exp e_new_v)
     | LEXP_field(v,id) ->
       parens ((string (if is_bit then "set_register_field_bit" else "set_register_field_v")) ^^ space ^^
@@ -1624,7 +1630,7 @@ let doc_exp_ocaml, doc_let_ocaml =
          (match alias_info with
           | Alias_field(reg,field) ->
             parens ((if is_bit then string "set_register_field_bit" else string "set_register_field_v") ^^ space ^^
-                    string reg ^^ space ^^string_lit (string field) ^^ space ^^ exp e_new_v)
+                    string (String.uncapitalize reg) ^^ space ^^string_lit (string field) ^^ space ^^ exp e_new_v)
           | Alias_extract(reg,start,stop) ->
             if start = stop
             then
@@ -1633,7 +1639,7 @@ let doc_exp_ocaml, doc_let_ocaml =
                  dot ^^ parens (doc_int start))
                 (exp e_new_v)
             else 
-              parens ((string (if is_bitv then "set_vector_subrange_bit" else "set_vector_subrange_v")) ^^ space ^^
+              parens ((string (if is_bitv then "set_vector_subrange_bit" else "set_vector_subrange_vec")) ^^ space ^^
                       string reg ^^ space ^^ doc_int start ^^ space ^^ doc_int stop ^^ space ^^ exp e_new_v)
           | Alias_pair(reg1,reg2) ->
             parens ((string "set_two_regs") ^^ space ^^ string reg1 ^^ space ^^ string reg2 ^^ space ^^ exp e_new_v))              
@@ -2185,9 +2191,12 @@ let doc_exp_lem, doc_let_lem =
       | E_aux(_,(_,Base((_,t),_,_,_,_,_))) ->
         (match t.t with
          | Tapp("vector", [_;_;_;(TA_typ ({t=Tid "bit"} | {t=Tabbrev(_,{t=Tid "bit"})}))]) |
-           Tabbrev(_,{t=Tapp("vector",[_;_;_;TA_typ ({t=Tid "bit"} | {t=Tabbrev(_,{t=Tid "bit"})})])}) ->
-           (false,true)
-         | Tid "bit" | Tabbrev(_,{t=Tid "bit"}) -> (true,false)
+           Tabbrev(_,{t=Tapp("vector",[_;_;_;TA_typ ({t=Tid "bit"} | {t=Tabbrev(_,{t=Tid "bit"})})])}) | 
+           Tapp("reg",[TA_typ {t = Tapp("vector", [_;_;_;(TA_typ ({t=Tid "bit"} | {t=Tabbrev(_,{t=Tid "bit"})}))])}])
+           ->
+            (false,true)
+         | Tid "bit" | Tabbrev(_,{t=Tid "bit"}) | Tapp("reg",[TA_typ ({t=Tid "bit"} | {t=Tabbrev(_,{t=Tid "bit"})})])
+           -> (true,false)
          | _ -> (false,false))
       | _ -> (false,false) in
     match lexp with
diff --git a/src/rewriter.ml b/src/rewriter.ml
index 30b6b3fe..bc7cba0d 100644
--- a/src/rewriter.ml
+++ b/src/rewriter.ml
@@ -865,6 +865,46 @@ let rewrite_exp_lift_assign_intro rewriters nmap ((E_aux (exp,(l,annot))) as ful
         let exps' = walker exps in
         [(E_aux (E_internal_let(le', e', E_aux(E_block exps', (l, simple_annot {t=Tid "unit"}))),
                  (l, simple_annot t)))]
+      | ((E_aux(E_if(c,t,e),(l,annot))) as exp)::exps ->
+         let vars_t = introduced_variables t in
+         let vars_e = introduced_variables e in
+         let new_vars = Envmap.intersect vars_t vars_e in
+         if Envmap.is_empty new_vars
+         then (rewrite_base exp)::walker exps
+         else
+           let new_nmap = match nmap with
+             | None -> Some(Nexpmap.empty,new_vars)
+             | Some(nm,s) -> Some(nm, Envmap.union new_vars s) in
+           let c' = rewrite_base c in
+           let t' = rewriters.rewrite_exp rewriters new_nmap t in
+           let e' = rewriters.rewrite_exp rewriters new_nmap e in
+           Envmap.fold 
+             (fun res i (t,e) ->
+                let bitlit =  E_aux (E_lit (L_aux(L_zero, Parse_ast.Unknown)),
+                                     (Parse_ast.Unknown, simple_annot bit_t)) in
+                let rangelit = E_aux (E_lit (L_aux (L_num 0, Parse_ast.Unknown)),
+                                      (Parse_ast.Unknown, simple_annot nat_t)) in
+                let set_exp =
+                  match t.t with
+                  | Tid "bit" | Tabbrev(_,{t=Tid "bit"}) -> bitlit
+                  | Tapp("range", _) | Tapp("atom", _) -> rangelit
+                  | Tapp("vector", [_;_;_;TA_typ ( {t=Tid "bit"} | {t=Tabbrev(_,{t=Tid "bit"})})])
+                  | Tapp(("reg"|"register"),[TA_typ ({t = Tapp("vector",
+                                                               [_;_;_;TA_typ ( {t=Tid "bit"}
+                                                                             | {t=Tabbrev(_,{t=Tid "bit"})})])})])
+                  | Tabbrev(_,{t = Tapp("vector",
+                                        [_;_;_;TA_typ ( {t=Tid "bit"}
+                                                      | {t=Tabbrev(_,{t=Tid "bit"})})])}) ->
+                    E_aux (E_vector_indexed([], Def_val_aux(Def_val_dec bitlit,
+                                                            (Parse_ast.Unknown,simple_annot bit_t))),
+                           (Parse_ast.Unknown, simple_annot t))
+                  | _ -> e in
+                [E_aux (E_internal_let (LEXP_aux (LEXP_id (Id_aux (Id i, Parse_ast.Unknown)),
+                                                  (Parse_ast.Unknown, (tag_annot t Emp_intro))),
+                                        set_exp,
+                                        E_aux (E_block res, (Parse_ast.Unknown, (simple_annot unit_t)))),
+                        (Parse_ast.Unknown, simple_annot unit_t))])
+             (E_aux(E_if(c',t',e'), (Parse_ast.Unknown, annot))::(walker exps)) new_vars
       | e::exps -> (rewrite_rec e)::(walker exps)
     in
     rewrap (E_block (walker exps))
@@ -872,16 +912,38 @@ let rewrite_exp_lift_assign_intro rewriters nmap ((E_aux (exp,(l,annot))) as ful
     (match annot with
      | Base((_,t),Emp_intro,_,_,_,_) ->
        let le' = rewriters.rewrite_lexp rewriters nmap le in
-       let e' = rewrite_base e in
-       rewrap (E_internal_let(le', e', E_aux(E_block [], (l, simple_annot {t=Tid "unit"}))))
-     | _ -> rewrite_base full_exp)         
+       (match le' with
+        | LEXP_aux(_, (_,Base(_,Emp_intro,_,_,_,_))) ->
+          let e' = rewrite_base e in
+          rewrap (E_internal_let(le', e', E_aux(E_block [], (l, simple_annot unit_t))))
+        | _ -> E_aux((E_assign(le', rewrite_base e)),(l, tag_annot unit_t Emp_set)))
+     | _ -> rewrite_base full_exp)
   | _ -> rewrite_base full_exp
 
+let rewrite_lexp_lift_assign_intro rewriters map ((LEXP_aux(lexp,(l,annot))) as le) = 
+  let rewrap le = LEXP_aux(le,(l,annot)) in
+  let rewrite_base = rewrite_lexp rewriters map in
+  match lexp with
+  | LEXP_id (Id_aux (Id i, _)) | LEXP_cast (_,(Id_aux (Id i,_))) ->
+    (match annot with
+    | Base((p,t),Emp_intro,cs,e1,e2,bs) ->
+      (match map with
+       | Some(_,s) ->
+         (match Envmap.apply s i with
+          | None -> rewrap lexp
+          | Some _ ->
+            let ls = BE_aux(BE_lset,l) in
+            LEXP_aux(lexp,(l,(Base((p,t),Emp_set,cs,add_effect ls e1, add_effect ls e2,bs)))))
+       | _ -> rewrap lexp)
+    | _ -> rewrap lexp)
+  | _ -> rewrite_base le
+
+
 let rewrite_defs_exp_lift_assign defs = rewrite_defs_base
     {rewrite_exp = rewrite_exp_lift_assign_intro;
      rewrite_pat = rewrite_pat;
      rewrite_let = rewrite_let;
-     rewrite_lexp = rewrite_lexp;
+     rewrite_lexp = rewrite_lexp_lift_assign_intro;
      rewrite_fun = rewrite_fun;
      rewrite_def = rewrite_def;
      rewrite_defs = rewrite_defs_base} defs
diff --git a/src/type_check.ml b/src/type_check.ml
index 4fb2cfc1..5bff7d3d 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -593,16 +593,18 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)):
         | L_undef -> 
           let ef = {effect=Eset[BE_aux(BE_undef,l)]} in
           (match expect_t.t with
-            | Tapp ("vector",[TA_nexp base;TA_nexp {nexp = rise};TA_ord o;(TA_typ {t=Tid "bit"})]) 
-            | Tapp ("register",[TA_typ {t=Tapp ("vector",[TA_nexp base;TA_nexp { nexp = rise};
-                                                          TA_ord o;(TA_typ {t=Tid "bit"})])}])->
+            | Tapp ("vector",[TA_nexp base;TA_nexp rise;TA_ord o;(TA_typ {t=Tid "bit"})]) 
+            | Toptions({t = Tapp ("vector",[TA_nexp base;TA_nexp rise;TA_ord o;(TA_typ {t=Tid "bit"})])}, None) ->
               let f = match o.order with | Oinc -> "to_vec_inc_undef" | Odec -> "to_vec_dec_undef" 
                                          | _ -> (match d_env.default_o.order with
                                              | Oinc -> "to_vec_inc_undef" | Odec -> "to_vec_dec_undef"
                                              | _ -> "to_vec_inc_undef") in
-              let tannot = (l,Base(([],expect_t),External (Some f),[],ef,ef,b_env)) in
+              let _ = set_imp_param rise in
+              let internal_tannot = (l,(cons_bs_annot {t = Tapp("implicit",[TA_nexp rise])} [] b_env)) in
+              let tannot = (l,Base(([],{t = Tapp("vector",[TA_nexp base; TA_nexp rise; TA_ord o; TA_typ bit_t])}),
+                                   External (Some f),[],ef,ef,b_env)) in
               E_aux(E_app((Id_aux((Id f),l)),
-                          [(E_aux (E_internal_exp(tannot), tannot));]),tannot),[],ef
+                          [(E_aux (E_internal_exp(internal_tannot), tannot));]),tannot),[],ef
             | _ -> simp_exp e l (new_t ()),[],ef)) in
       let t',cs',_,e' = type_coerce (Expr l) d_env Require false true b_env (get_e_typ e) e expect_t in
       (e',t',t_env,cs@cs',nob,effect)
@@ -775,15 +777,15 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)):
           (match t_p.t with
           | Tfn(arg,ret,_,ef') -> check_parms arg lft rht
           | _ -> typ_error l ("Expected a function, found identifier " ^ i ^ " bound to type " ^ (t_to_string t))) in
-        let _ = Printf.eprintf "Looking for overloaded function %s, generic type is %s, arg_t is %s\n"
-          i (t_to_string t_p) (t_to_string arg_t) in
+        (*let _ = Printf.eprintf "Looking for overloaded function %s, generic type is %s, arg_t is %s\n"
+          i (t_to_string t_p) (t_to_string arg_t) in*)
         (match (select_overload_variant d_env true overload_return variants arg_t) with
         | [] -> 
           typ_error l ("No function found with name " ^ i ^
                           " that expects parameters " ^ (t_to_string arg_t))
         | [Base((params,t),tag,cs,ef,_,b)] ->
-          let _ = Printf.eprintf "Selected an overloaded function for %s,
-            variant with function type %s for actual type %s\n" i (t_to_string t) (t_to_string arg_t) in
+          (*let _ = Printf.eprintf "Selected an overloaded function for %s,
+            variant with function type %s for actual type %s\n" i (t_to_string t) (t_to_string arg_t) in*)
           (match t.t with
           | Tfn(arg,ret,imp,ef') ->
             (match arg.t,arg_t.t with
@@ -795,15 +797,15 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)):
             |_ -> raise (Reporting_basic.err_unreachable l "function no longer has tuple type"))
           | _ -> raise (Reporting_basic.err_unreachable l "overload variant does not have function"))
         | variants ->
-          let _ = Printf.eprintf "Number of variants found before looking at return value %i\n%!" 
-            (List.length variants) in
+          (*let _ = Printf.eprintf "Number of variants found before looking at return value %i\n%!" 
+            (List.length variants) in*)
           (match (select_overload_variant d_env false true variants expect_t) with
             | [] -> 
               typ_error l ("No matching function found with name " ^ i ^ " that expects parameters " ^
                               (t_to_string arg_t) ^ " returning " ^ (t_to_string expect_t))
             | [Base((params,t),tag,cs,ef,_,b)] -> 
-              let _ = Printf.eprintf "Selected an overloaded function for %s,
-            variant with function type %s for actual type %s\n" i (t_to_string t) (t_to_string arg_t) in
+          (*let _ = Printf.eprintf "Selected an overloaded function for %s,
+            variant with function type %s for actual type %s\n" i (t_to_string t) (t_to_string arg_t) in*)
               (match t.t with
                 | Tfn(arg,ret,imp,ef') ->
                   (match arg.t,arg_t.t with
@@ -943,7 +945,7 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)):
         | (Def_val_empty,false) -> (Def_val_aux(Def_val_empty,(ld,simple_annot item_t)),true,[],pure_e)
         | (Def_val_empty,true)  -> 
           let ef = add_effect (BE_aux(BE_unspec,l)) pure_e in
-          let (de,_,_,_,_,ef_d) = check_exp envs imp_param item_t (E_aux(E_lit (L_aux(L_undef,l)), (l,NoTyp))) in
+          let de = E_aux(E_lit (L_aux(L_undef,l)), (l,simple_annot item_t)) in
           (Def_val_aux(Def_val_dec de, (l, cons_efs_annot item_t [] ef ef)),false,[],ef)
         | (Def_val_dec e,_) -> let (de,t,_,cs_d,_,ef_d) = (check_exp envs imp_param item_t e) in
           (*Check that ef_d doesn't write to memory or registers? *)
@@ -1292,6 +1294,9 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)):
       (E_aux(E_let(lb',e),(l,simple_annot_efr t effects)),t,t_env,cs@cs',nob,effects)
     | E_assign(lexp,exp) ->
       let (lexp',t',_,t_env',tag,cs,b_env',efl,efr) = check_lexp envs imp_param true lexp in
+      let t' = match t'.t with | Tapp("reg",[TA_typ t]) | Tapp("register",[TA_typ t])
+                               | Tabbrev(_,{t=Tapp("register",[TA_typ t])}) -> t
+                               | _ -> t' in
       let (exp',t'',_,cs',_,efr') = check_exp envs imp_param t' exp in
       let (t',c') = type_consistent (Expr l) d_env Require false unit_t expect_t in
       let effects = union_effects efl (union_effects efr efr') in
@@ -1843,8 +1848,8 @@ let check_fundef envs (FD_aux(FD_function(recopt,tannotopt,effectopt,funcls),(l,
   let check t_env tp_env imp_param =
     List.split
       (List.map (fun (FCL_aux((FCL_Funcl(id,pat,exp)),(l,_))) ->
-        let _ = Printf.eprintf "checking function %s : %s -> %s\n" 
-          (id_to_string id) (t_to_string param_t) (t_to_string ret_t) in
+        (*let _ = Printf.eprintf "checking function %s : %s -> %s\n" 
+          (id_to_string id) (t_to_string param_t) (t_to_string ret_t) in*)
         let (pat',t_env',cs_p,b_env',t') = check_pattern (Env(d_env,t_env,b_env,tp_env)) Emp_local param_t pat in
         let _, _ = type_consistent (Patt l) d_env Require false param_t t' in
         let exp',_,_,cs_e,_,ef = 
diff --git a/src/type_internal.ml b/src/type_internal.ml
index 660ef20a..2fb06ce0 100644
--- a/src/type_internal.ml
+++ b/src/type_internal.ml
@@ -467,9 +467,11 @@ let rec pow_i i n =
 let two_pow = pow_i 2
 
 let is_bit_vector t = match t.t with
-  | Tapp("vector", [_;_;_; TA_typ t]) | Tabbrev(_,{t=Tapp("vector",[_;_;_; TA_typ t])}) ->
+  | Tapp("vector", [_;_;_; TA_typ t])
+  | Tabbrev(_,{t=Tapp("vector",[_;_;_; TA_typ t])})
+  | Tapp("reg", [TA_typ {t=Tapp("vector",[_;_;_; TA_typ t])}])->
     (match t.t with
-     | Tid "bit" | Tabbrev(_,{t=Tid "bit"}) -> true
+     | Tid "bit" | Tabbrev(_,{t=Tid "bit"}) | Tapp("reg",[TA_typ {t=Tid "bit"}]) -> true
      | _ -> false)
   | _ -> false
 
@@ -2767,10 +2769,10 @@ let rec type_coerce_internal co d_env enforce is_explicit widen bounds t1 cs1 e
       | [TA_nexp b1;TA_nexp r1;TA_ord _;TA_typ {t=Tid "bit"}],
         [TA_nexp b2;TA_nexp r2;] -> 
         let cs = [Eq(co,b2,n_zero);LtEq(co,Guarantee,mk_sub (mk_2n(r1)) n_one,r2)] in
-        (t2,cs,pure_e,E_aux(E_app((Id_aux(Id "to_num",l)),[e]),
+        (t2,cs,pure_e,E_aux(E_app((Id_aux(Id "unsigned",l)),[e]),
                             (l, constrained_annot_efr t2 cs (get_cummulative_effects (get_eannot e)))))
       | [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"
+        eq_error l "Cannot convert a vector to a range without an order"
       | [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"))
@@ -2779,7 +2781,7 @@ let rec type_coerce_internal co d_env enforce is_explicit widen bounds t1 cs1 e
       | [TA_nexp b1;TA_nexp r1;TA_ord _;TA_typ {t=Tid "bit"}],
         [TA_nexp b2] -> 
         let cs = [GtEq(co,Guarantee,b2,n_zero);LtEq(co,Guarantee,b2,mk_sub (mk_2n(r1)) n_one)] in
-        (t2,cs,pure_e,E_aux(E_app((Id_aux(Id "to_num",l)),[e]),
+        (t2,cs,pure_e,E_aux(E_app((Id_aux(Id "unsigned",l)),[e]),
                             (l, constrained_annot_efr t2 cs (get_cummulative_effects (get_eannot e)))))
       | [TA_nexp b1;TA_nexp r1;TA_ord o;TA_typ t],_ -> 
         eq_error l "Cannot convert non-bit vector into an range"