Extend type checking so that patterns with vector concatenation don't permit under specified vector lengths (at least for function patterns)

Extend interpreter interface to have a function for Christopher's instruction analysis

5 files changed, 451 insertions, 172 deletions

diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem
index 60419886..49d8cbfe 100644
--- a/src/lem_interp/interp_inter_imp.lem
+++ b/src/lem_interp/interp_inter_imp.lem
@@ -302,7 +302,7 @@ let initial_instruction_state top_level main args =
   Interp.Thunk_frame (E_aux (E_app (Id_aux (Id main) Interp_ast.Unknown) e_args) (Interp_ast.Unknown, Nothing)) 
     top_level Interp.eenv (Interp.emem "istate top level") Interp.Top
 
-type interp_value_helper_mode = Ivh_translate | Ivh_decode | Ivh_unsupported | Ivh_illegal
+type interp_value_helper_mode = Ivh_translate | Ivh_decode | Ivh_unsupported | Ivh_illegal | Ivh_analysis
 type interp_value_return =
   | Ivh_value of Interp.value
   | Ivh_value_after_exn of Interp.value
@@ -311,6 +311,7 @@ type interp_value_return =
 let rec interp_to_value_helper arg ivh_mode err_str instr direction registers events exn_seen thunk =
   let errk_str = match ivh_mode with
     | Ivh_translate -> "translate"
+    | Ivh_analysis -> "analysis"
     | Ivh_decode -> "decode"
     | Ivh_unsupported -> "supported_instructions"
     | Ivh_illegal -> "illegal instruction" end in
@@ -323,15 +324,16 @@ let rec interp_to_value_helper arg ivh_mode err_str instr direction registers ev
       else
         (match ivh_mode with
          | Ivh_translate -> (Ivh_value value, events_out)
+         | Ivh_analysis -> (Ivh_value value, events_out)
          | _ ->
            (match value with
             | Interp.V_ctor (Id_aux (Id "Some") _) _ _ vinstr -> (Ivh_value vinstr,events_out)
             | Interp.V_ctor (Id_aux (Id "None") _) _ _ _ ->
-              (match ivh_mode with
-               | Ivh_decode -> (Ivh_error (Not_an_instruction_error arg), events_out)
-               | Ivh_illegal -> (Ivh_error (Not_an_instruction_error arg), events_out)
-               | Ivh_unsupported -> (Ivh_error (Unsupported_instruction_error instr), events_out)
-               | Ivh_translate -> Assert_extra.failwith "Reached unreachable pattern" end)
+              (match (ivh_mode,arg) with
+               | (Ivh_decode, (Just arg)) -> (Ivh_error (Not_an_instruction_error arg), events_out)
+               | (Ivh_illegal, (Just arg)) -> (Ivh_error (Not_an_instruction_error arg), events_out)
+               | (Ivh_unsupported, _) -> (Ivh_error (Unsupported_instruction_error instr), events_out)
+               | _ -> Assert_extra.failwith "Reached unreachable pattern" end)
             | _ -> (Ivh_error (Internal_error ("Value not an option for " ^ errk_str)), events_out) end) end)
     | (Interp.Error l msg,_,_) -> (Ivh_error (Internal_error msg), events_out)
     | (Interp.Action (Interp.Return value) stack,_,_) ->
@@ -413,7 +415,7 @@ let translate_address top_level end_flag thunk_name registers address =
   let (arg,_) = Interp.to_exp int_mode Interp.eenv intern_val in
   let internal_direction = if direction = D_increasing then Interp.IInc else Interp.IDec in
   let (address_error,events) =
-    interp_to_value_helper (Opcode bytes) Ivh_translate val_str ("",[],[]) internal_direction
+    interp_to_value_helper (Just (Opcode bytes)) Ivh_translate val_str ("",[],[]) internal_direction
       registers [] false
       (fun _ -> Interp.resume 
         int_mode 
@@ -433,6 +435,77 @@ let translate_address top_level end_flag thunk_name registers address =
      | _ -> Assert_extra.failwith "Not an internal error either" end 
 end
 
+let value_of_instruction_param direction (name,typ,v) = 
+  let vec = intern_ifield_value direction v in
+  let v = match vec with
+    | Interp.V_vector start dir bits ->
+      match typ with
+      | Bit -> match bits with | [b] -> b | _ -> Assert_extra.failwith "Expected a bitvector of length 1" end
+      | Range _ -> Interp_lib.to_num Interp_lib.Unsigned vec
+      | Enum _ _ -> Interp_lib.to_num Interp_lib.Unsigned vec
+      | _ -> vec
+    end 
+    | _ -> Assert_extra.failwith "intern_ifield did not return vector"
+  end in v
+
+let intern_instruction direction (name,parms,_) =
+  Interp.V_ctor (Interp.id_of_string name) (T_id "ast") Interp.C_Union
+    (Interp.V_tuple (List.map (value_of_instruction_param direction) parms))
+
+let instruction_analysis top_level end_flag thunk_name regn_to_reg_details registers instruction =
+  let mode = make_mode true false end_flag in
+  let int_mode = mode.internal_mode in
+  let (Context top_env direction _ _ _ _ _ _) = top_level in
+  let intern_val = intern_instruction direction instruction in
+  let val_str = Interp.string_of_value intern_val in
+  let (arg,_) = Interp.to_exp int_mode Interp.eenv intern_val in
+  let internal_direction = if direction = D_increasing then Interp.IInc else Interp.IDec in
+  let (analysis_or_error,events) =
+    interp_to_value_helper Nothing Ivh_analysis val_str ("",[],[]) internal_direction
+      registers [] false
+      (fun _ -> Interp.resume 
+        int_mode 
+        (Interp.Thunk_frame 
+         (E_aux (E_app (Id_aux (Id thunk_name) Interp_ast.Unknown) [arg])
+            (Interp_ast.Unknown, Nothing)) 
+         top_env Interp.eenv (Interp.emem "instruction analysis top level") Interp.Top) Nothing) in
+  match (analysis_or_error) with
+  | Ivh_value regs ->
+    (match regs with
+     | Interp.V_tuple [Interp.V_list regs1; Interp.V_list regs2; Interp.V_list regs3] ->
+       let reg_to_reg_name v = match v with
+         | Interp.V_ctor (Id_aux (Id "RFull") _) _ _ (Interp.V_lit (L_aux (L_string n) _)) ->
+           let (start,length,direction,_) = regn_to_reg_details n Nothing in
+           Reg n start length direction
+         | Interp.V_ctor (Id_aux (Id "RSlice") _) _ _
+             (Interp.V_tuple [Interp.V_lit (L_aux (L_string n) _);
+                              Interp.V_lit (L_aux (L_num s1) _);
+                              Interp.V_lit (L_aux (L_num s2) _);]) ->
+           let (start,length,direction,_) = regn_to_reg_details n Nothing in
+           Reg_slice n start direction (natFromInteger s1, natFromInteger s2)
+                                       (*Note, this may need to change order depending on the direction*)
+         | Interp.V_ctor (Id_aux (Id "RSliceBit") _) _ _
+             (Interp.V_tuple [Interp.V_lit (L_aux (L_string n) _);
+                              Interp.V_lit (L_aux (L_num s) _);]) ->
+           let (start,length,direction,_) = regn_to_reg_details n Nothing in
+           Reg_slice n start direction (natFromInteger s,natFromInteger s)
+         | Interp.V_ctor (Id_aux (Id "RField") _) _ _
+             (Interp.V_tuple [Interp.V_lit (L_aux (L_string n) _);
+                              Interp.V_lit (L_aux (L_string f) _);]) ->
+           let (start,length,direction,span) = regn_to_reg_details n (Just f) in
+           Reg_field n start direction f span             
+         | _ -> Assert_extra.failwith "Analysis did not return an element of the specified type" end
+       in
+       let (regs1,regs2,regs3) =
+         (List.map reg_to_reg_name regs1, List.map reg_to_reg_name regs2, List.map reg_to_reg_name regs3) in
+       (Just (regs1,regs2,regs3), events)
+     | _ -> Assert_extra.failwith "Analysis did not return a three-tuple of lists" end)
+  | Ivh_value_after_exn _ ->
+    (Nothing, events)
+  | Ivh_error err -> match err with
+     | Internal_error msg -> Assert_extra.failwith msg
+     | _ -> Assert_extra.failwith "Not an internal error either" end 
+end
 
 let rec find_instruction i = function
   | [] -> Nothing
@@ -460,7 +533,7 @@ let decode_to_istate top_level registers value =
   let (arg,_) = Interp.to_exp mode Interp.eenv intern_val in
   let internal_direction = if direction = D_increasing then Interp.IInc else Interp.IDec in
   let (instr_decoded_error,events) =
-    interp_to_value_helper value Ivh_decode val_str ("",[],[]) internal_direction registers [] false
+    interp_to_value_helper (Just value) Ivh_decode val_str ("",[],[]) internal_direction registers [] false
       (fun _ -> Interp.resume 
           mode 
           (Interp.Thunk_frame 
@@ -488,7 +561,7 @@ let decode_to_istate top_level registers value =
         | _ -> Assert_extra.failwith "decoded instruction not a constructor" end in 
       let (arg,_) = Interp.to_exp mode Interp.eenv instr in
       let (instr_decoded_error,events) =
-        interp_to_value_helper value Ivh_unsupported val_str instr_external internal_direction
+        interp_to_value_helper (Just value) Ivh_unsupported val_str instr_external internal_direction
           registers [] false
         (fun _ -> Interp.resume 
             mode
diff --git a/src/lem_interp/interp_interface.lem b/src/lem_interp/interp_interface.lem
index 99b4daf6..2da9e060 100644
--- a/src/lem_interp/interp_interface.lem
+++ b/src/lem_interp/interp_interface.lem
@@ -1154,6 +1154,10 @@ val translate_address :
   context -> end_flag -> string -> maybe (list (reg_name * register_value)) -> address
   -> maybe address * maybe (list event)
 
+val instruction_analysis :
+  context -> end_flag -> string -> (string -> (nat * nat * direction * (nat * nat)))
+  -> maybe (list (reg_name * register_value)) -> instruction -> (list reg_name * list reg_name * list reg_name)
+
 val byte_list_of_memory_value : end_flag -> memory_value -> maybe (list byte)
 let byte_list_of_memory_value endian mv = 
   let mv = if endian = E_big_endian then mv else List.reverse mv in
diff --git a/src/type_check.ml b/src/type_check.ml
index 9a99cc36..eed53609 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -472,6 +472,199 @@ let rec check_pattern envs emp_tag expect_t (P_aux(p,(l,annot))) : ((tannot pat)
       let t = {t = Tapp("list",[TA_typ u])} in
       (P_aux(P_list(pats'),(l,cons_tag_annot  t emp_tag cs)), env,constraints@cs,bounds,t)
 
+let rec check_pattern_after_constraint_res envs concrete_length_req expect_t (P_aux(p,(l,annot))) : t  =
+  let check_pat = check_pattern_after_constraint_res envs in
+  let (Env(d_env,t_env,b_env,tp_env)) = envs in
+  (*let _ = Printf.eprintf "checking pattern after constraints with expected type %s\n" (t_to_string expect_t) in*)
+  let expect_t,_ = get_abbrev d_env expect_t in
+  (*let _ = Printf.eprintf "check pattern after constraints expect_t after abbrev %s\n" (t_to_string expect_t) in*)
+  let expect_actual = match expect_t.t with | Tabbrev(_,t) -> t | _ -> expect_t in
+  let t_inferred = match annot with
+    | Base((_,t),tag,cs,_,_,_) -> t
+    | _ -> failwith "Inference pass did not annotate a pattern with Base annot" in
+  match p with
+  | P_lit (L_aux(lit,l')) ->
+    let t_from_lit = (match lit with
+        | L_unit  -> unit_t 
+        | L_zero | L_one | L_true | L_false -> bit_t
+        | L_num i -> 
+          (match expect_actual.t with
+           | Tid "bit" -> if i = 0 || i = 1 then bit_t else typ_error l' "Given number but expected bit"
+           | _ -> {t = Tapp("atom", [TA_nexp (mk_c_int i)])})
+        | L_hex s -> 
+          let size = big_int_of_int ((String.length s) * 4) in
+          let is_inc = match d_env.default_o.order with | Oinc -> true | _ -> false in
+          mk_vector bit_t d_env.default_o (if is_inc then n_zero else mk_c (sub_big_int size one)) (mk_c size)
+        | L_bin s -> 
+          let size = big_int_of_int (String.length s) in
+          let is_inc = match d_env.default_o.order with | Oinc -> true | _ -> false in
+          mk_vector bit_t d_env.default_o (if is_inc then n_zero else mk_c(sub_big_int size one)) (mk_c size)
+        | L_string s -> string_t
+        | L_undef -> typ_error l' "Cannot pattern match on undefined") in
+    let t_c,_ = type_consistent (Patt l) d_env Require true t_from_lit t_inferred in
+    let t,_   = type_consistent (Patt l) d_env Require true t_c expect_t in
+    t
+  | P_wild ->
+    let t,_ = type_consistent (Patt l) d_env Require true t_inferred expect_t in t
+  | P_as(pat,id) -> check_pat concrete_length_req expect_t pat
+  | P_typ(typ,pat) -> 
+    let tdec = typ_to_t envs false false typ in
+    let tdec = typ_subst tp_env false tdec in
+    let default _ = let tdec = check_pat false tdec pat in
+      let t,_ = type_consistent (Patt l) d_env Guarantee false tdec t_inferred in
+      let t,_ = type_consistent (Patt l) d_env Guarantee false t expect_t in
+      t
+    in
+    (match tdec.t, concrete_length_req with
+     | Tapp ("vector", [_;TA_nexp {nexp = Nconst _};_;_]), true -> default ()
+     | Tapp ("vector",_), true ->
+       (try (let tdec = check_pat true tdec pat in
+            let t,_ = type_consistent (Patt l) d_env Guarantee false tdec t_inferred in
+            let t,_ = type_consistent (Patt l) d_env Guarantee false t expect_t in t) with
+       | Reporting_basic.Fatal_error(Reporting_basic.Err_type _) ->
+         typ_error l "Type annotation does not provide a concrete vector length and one cannot be inferred")
+     | _ -> default ())
+  | P_id id -> 
+    let i = id_to_string id in
+    let default t =
+      let t,_ = type_consistent (Patt l) d_env Guarantee false t t_inferred in
+      let t,_ = type_consistent (Patt l) d_env Guarantee false t expect_t in t in
+    (match Envmap.apply t_env i with
+     | Some(Base((params,t),Constructor n,cs,efl,efr,bounds)) ->
+       let t,cs,ef,_ = subst params false false t cs efl in
+       (match t.t with
+        | Tfn({t = Tid "unit"},t',IP_none,ef) -> 
+          if conforms_to_t d_env false false t' expect_t then default t' else default t
+        | Tfn(t1,t',IP_none,e) -> 
+          if conforms_to_t d_env false false t' expect_t
+          then typ_error l ("Constructor " ^ i ^ " expects arguments of type " ^ (t_to_string t) ^ ", found none")
+          else default t'
+        | _ -> raise (Reporting_basic.err_unreachable l "Constructor tannot does not have function type"))
+     | Some(Base((params,t),Enum max,cs,efl,efr,bounds)) -> 
+       let t,cs,ef,_ = subst params false false t cs efl in default t
+     | _ -> (match t_inferred.t, concrete_length_req with
+         | Tapp ("vector", [_;TA_nexp {nexp = Nconst _};_;_]), true -> default t_inferred
+         | Tapp ("vector", _), true ->
+           typ_error l ("Unable to infer a vector length for paramter " ^ i ^ ", a type annotation may be required.")
+         | _ -> default t_inferred))
+    | P_app(id,pats) -> 
+      let i = id_to_string id in
+      (*let _ = Printf.eprintf "checking constructor pattern %s\n" i in*)
+      (match Envmap.apply t_env i with
+        | None | Some NoTyp | Some Overload _ -> typ_error l ("Constructor " ^ i ^ " in pattern is undefined")
+        | Some(Base((params,t),Constructor n,constraints,efl,efr,bounds)) -> 
+          let t,dec_cs,_,_ = subst params false false t constraints efl in
+          (match t.t with
+            | Tid id -> if pats = [] 
+              then let t',ret_cs = type_consistent (Patt l) d_env Guarantee false t expect_t in t'
+              else typ_error l ("Constructor " ^ i ^ " does not expect arguments")
+            | Tfn(t1,t2,IP_none,ef) ->
+              let t',ret_cs = type_consistent (Patt l) d_env Guarantee false t2 expect_t in
+              (match pats with
+              | [] -> let _ = type_consistent (Patt l) d_env Guarantee false unit_t t1 in t'
+              | [p] -> check_pat concrete_length_req t1 p 
+              | pats -> check_pat concrete_length_req t1 (P_aux(P_tup(pats),(l,annot))))
+            | _ -> typ_error l ("Identifier " ^ i ^ " must be a union constructor"))
+        | Some(Base((params,t),tag,constraints,efl,efr,bounds)) -> 
+          typ_error l ("Identifier " ^ i ^ " used in pattern is not a union constructor"))
+    | P_record(fpats,_) -> 
+      (match (fields_to_rec fpats d_env.rec_env) with
+        | None -> typ_error l ("No struct exists with the listed fields")
+        | Some(id,tannot,typ_pats) ->
+          (match tannot with
+            | (Base((vs,t),tag,cs,eft,_,bounds)) ->
+              let (ft_subst,cs,_,_) = subst vs false false t cs pure_e in
+              let subst_rtyp,subst_typs = 
+                match ft_subst.t with | Tfn({t=Ttup tups},rt,_,_) -> rt,tups 
+                  | _ -> raise (Reporting_basic.err_unreachable l "fields_to_rec gave a non function type") in
+              let _ = 
+                List.map2 (fun (_,id,l,pat) styp -> check_pat concrete_length_req styp pat) typ_pats subst_typs in
+              let t',cs' = type_consistent (Patt l) d_env Guarantee false ft_subst expect_t in t'
+            | _ -> raise (Reporting_basic.err_unreachable l "fields_to_rec returned a non Base tannot")))
+    | P_vector pats -> 
+      let (item_t, base, rise, ord) = match expect_actual.t with 
+        | Tapp("vector",[TA_nexp b;TA_nexp r;TA_ord o;TA_typ i]) -> (i,b,r,o)
+        | Tuvar _ -> (new_t (),new_n (),new_n(), d_env.default_o) 
+        | _ -> typ_error l ("Expected a " ^ t_to_string expect_actual ^ " but found a vector") in
+      let ts = List.map (check_pat false item_t) pats in
+      let (u,cs) = List.fold_right (fun u (t,cs) ->
+          let t',cs = type_consistent (Patt l) d_env Require true u t in t',cs) ts (item_t,[]) in
+      let len = List.length ts in
+      let t = 
+        match (ord.order,d_env.default_o.order) with
+        | (Oinc,_) | (Ovar _, Oinc) | (Ouvar _,Oinc) -> 
+          {t = Tapp("vector",[TA_nexp n_zero;
+                              TA_nexp (mk_c_int len);
+                              TA_ord{order=Oinc};
+                              TA_typ u])}
+        | (Odec,_) | (Ovar _, Odec) | (Ouvar _,Odec) -> 
+          {t= Tapp("vector", [TA_nexp (mk_c (if len = 0 then zero else (big_int_of_int (len -1))));
+                              TA_nexp (mk_c_int len);
+                              TA_ord{order=Odec};
+                              TA_typ u;])}
+        | _ -> raise (Reporting_basic.err_unreachable l "Default order not set") in
+      let _,_ = type_consistent (Patt l) d_env Guarantee true t expect_t in t
+    | P_vector_indexed(ipats) -> 
+      let item_t = match expect_actual.t with
+        | Tapp("vector",[b;r;o;TA_typ i]) -> i
+        | Tuvar _ -> new_t () 
+        | _ -> typ_error l ("Expected a vector by pattern form, but a " ^ t_to_string expect_actual ^ " by type") in
+      let (is,pats) = List.split ipats in
+      let (fst,lst) = (List.hd is),(List.hd (List.rev is)) in
+      let inc_or_dec = 
+        if fst < lst then
+          (let _ = List.fold_left 
+             (fun i1 i2 -> if i1 < i2 then i2 
+               else typ_error l "Indexed vector pattern was inconsistently increasing") fst (List.tl is) in
+           true)
+        else if lst < fst then
+          (let _ = List.fold_left
+             (fun i1 i2 -> if i1 > i2 then i2
+               else typ_error l "Indexed vector pattern was inconsistently decreasing") fst (List.tl is) in
+           false)
+        else typ_error l "Indexed vector cannot be determined as either increasing or decreasing" in
+      let base,rise = new_n (), new_n () in
+      let ts = List.map (fun (_,pat) -> check_pat concrete_length_req item_t pat) ipats in
+      let co = Patt l in
+      let (u,cs) = List.fold_right (fun u (t,cs) -> type_consistent co d_env Require true u t) ts (item_t,[]) in
+      {t = Tapp("vector",[(TA_nexp base);(TA_nexp rise);
+                          (TA_ord{order=(if inc_or_dec then Oinc else Odec)});(TA_typ u)])}
+    | P_tup(pats) -> 
+      let item_ts = match expect_actual.t with
+        | Ttup ts ->
+          if (List.length ts) = (List.length pats) 
+          then ts
+          else typ_error l ("Expected a pattern with a tuple with " ^
+                            (string_of_int (List.length ts)) ^ " elements, found one with " ^
+                            (string_of_int (List.length pats)))
+        | Tuvar _ -> List.map (fun _ -> new_t ()) pats 
+        | _ -> typ_error l ("Expected a tuple by pattern form, but a " ^ (t_to_string expect_actual) ^ " by type") in
+      let ts = List.map (fun (pat,t) -> check_pat false t pat) (List.combine pats item_ts) in
+      {t = Ttup ts}
+    | P_vector_concat pats -> 
+      let item_t,base,rise,order = 
+        match expect_t.t with 
+          | Tapp("vector",[TA_nexp(b);TA_nexp(r);TA_ord(o);TA_typ item])
+          | Tabbrev(_,{t=Tapp("vector",[TA_nexp(b);TA_nexp(r);TA_ord(o);TA_typ item])}) -> item,b,r,o
+          | _ -> new_t (),new_n (), new_n (), d_env.default_o in
+      let vec_ti _ = {t= Tapp("vector",[TA_nexp (new_n ());TA_nexp (new_n ());TA_ord order;TA_typ item_t])} in
+      let _ =
+        let rec walk = function
+          | [] -> []
+          | [p] ->
+            [check_pat concrete_length_req (*use enclosing pattern status in case of nested concats*) (vec_ti ()) p]
+          | p::ps -> (check_pat true (vec_ti ()) p)::(walk ps) in
+        walk pats in
+      {t = Tapp("vector",[(TA_nexp base);(TA_nexp rise);(TA_ord order);(TA_typ item_t)])}
+    | P_list(pats) -> 
+      let item_t = match expect_actual.t with
+        | Tapp("list",[TA_typ i]) -> i
+        | Tuvar _ -> new_t () 
+        | _ -> typ_error l ("Expected a list here by pattern form, but expected a " ^ t_to_string expect_actual ^ " by type") in
+      let ts = List.map (check_pat false item_t) pats in
+      let u = List.fold_right (fun u t -> let t',_ = type_consistent (Patt l) d_env Require true u t in t') ts item_t in
+      {t = Tapp("list",[TA_typ u])}
+
 let simp_exp e l t = E_aux(e,(l,simple_annot t))
 
 (*widen lets outer expressions control whether inner expressions should widen in the presence of literals or not.
@@ -2058,7 +2251,8 @@ let check_fundef envs (FD_aux(FD_function(recopt,tannotopt,effectopt,funcls),(l,
       let (ids,_,constraints) = typq_to_params envs typq in
       let t = typ_to_t envs false false typ in
       (*TODO add check that ids == typ_params when has_spec*)
-      let t,constraints,_,t_param_env = subst (if has_spec then typ_params else ids) true true t constraints pure_e in
+      let t,constraints,_,t_param_env =
+        subst (if has_spec then typ_params else ids) true true t constraints pure_e in
       let p_t = new_t () in
       let ef = new_e () in
       t,p_t,Base((ids,{t=Tfn(p_t,t,IP_none,ef)}),Emp_global,constraints,ef,pure_e,nob),t_param_env in
@@ -2075,10 +2269,12 @@ let check_fundef envs (FD_aux(FD_function(recopt,tannotopt,effectopt,funcls),(l,
                          merge_bounds b_env b_env',tp_env)) imp_param true true ret_t ret_t exp in
         (*let _ = Printf.eprintf "checked function %s : %s -> %s\n" 
           (id_to_string id) (t_to_string param_t) (t_to_string ret_t) in
-        let _ = Printf.eprintf "constraints were pattern: %s\n expression: %s\n" 
+          let _ = Printf.eprintf "constraints were pattern: %s\n expression: %s\n" 
           (constraints_to_string cs_p) (constraints_to_string cs_e) in*)
         let cs = CondCons(Fun l,cond_kind,None,cs_p,cs_e) in
         (FCL_aux((FCL_Funcl(id,pat',exp')),(l,(Base(([],ret_t),Emp_global,[cs],ef,pure_e,nob)))),(cs,ef))) funcls) in
+  let check_pattern_after_constraints (FCL_aux ((FCL_Funcl (_, pat, _)), _)) =
+    check_pattern_after_constraint_res (Env(d_env,t_env,b_env,tp_env)) false param_t pat in
   let update_pattern var (FCL_aux ((FCL_Funcl(id,(P_aux(pat,t)),exp)),annot)) =
     let pat' = match pat with
       | P_lit (L_aux (L_unit,l')) -> P_aux(P_id (Id_aux (Id var, l')), t)
@@ -2091,7 +2287,9 @@ let check_fundef envs (FD_aux(FD_function(recopt,tannotopt,effectopt,funcls),(l,
       (*let _ = Printf.eprintf "Function %s is in env\n" id in*)
       let u,constraints,eft,t_param_env = subst_with_env t_param_env true u constraints eft in
       let _,cs_decs = type_consistent (Specc l) d_env Require false t u in
-      (*let _ = Printf.eprintf "valspec consistent with declared type for %s, %s ~< %s with %s derived constraints and %s stated\n" id (t_to_string t) (t_to_string u) (constraints_to_string cs_decs) (constraints_to_string (constraints@c')) in*)
+      (*let _ = Printf.eprintf "valspec consistent with type for %s, %s ~< %s with %s deriveds and %s stated\n" 
+        id (t_to_string t) (t_to_string u) (constraints_to_string cs_decs) 
+        (constraints_to_string (constraints@c')) in*)
       let imp_param = match u.t with 
         | Tfn(_,_,IP_user n,_) -> Some n
         | _ -> None in
@@ -2104,8 +2302,9 @@ let check_fundef envs (FD_aux(FD_function(recopt,tannotopt,effectopt,funcls),(l,
       let tannot =
         check_tannot l (match map with | None -> tannot | Some m -> add_map_tannot m tannot) imp_param cs' ef in
       (*let _ = Printf.eprintf "remaining constraints are: %s\n" (constraints_to_string cs') in
-      let _ = Printf.eprintf "check_tannot ok for %s val type %s derived type %s \n" 
+        let _ = Printf.eprintf "check_tannot ok for %s val type %s derived type %s \n" 
         id (t_to_string u) (t_to_string t) in*)
+      let _ = List.map check_pattern_after_constraints funcls in
       let funcls = match imp_param with
         | Some {nexp = Nvar i} -> List.map (update_pattern i) funcls
         | _ -> funcls
@@ -2126,6 +2325,7 @@ let check_fundef envs (FD_aux(FD_function(recopt,tannotopt,effectopt,funcls),(l,
       let tannot = check_tannot l
                                 (match map with | None -> tannot | Some m -> add_map_tannot m tannot)
                                 None cs' ef in
+      let _ = List.map check_pattern_after_constraints funcls in
       (*let _ = Printf.eprintf "done funcheck case2\n" in*)
       (FD_aux(FD_function(recopt,tannotopt,effectopt,funcls),(l,tannot))),
       Env(d_env,(if is_rec then t_env else Envmap.insert t_env (id,tannot)),b_env,tp_env)
diff --git a/src/type_internal.ml b/src/type_internal.ml
index c7b47831..4f232ca6 100644
--- a/src/type_internal.ml
+++ b/src/type_internal.ml
@@ -1931,11 +1931,12 @@ let mk_pure_imp arg ret var = {t = Tfn (arg,ret,IP_length (mk_nv var),pure_e)}
 let lib_tannot param_typs func cs =
   Base(param_typs, External func, cs, pure_e, pure_e, nob)
 
+let mk_ovar s = {order = Ovar s}
 let mk_range n1 n2 = {t=Tapp("range",[TA_nexp n1;TA_nexp n2])}
 let mk_atom n1 = {t = Tapp("atom",[TA_nexp n1])}
-let mk_vector typ order start size = {t=Tapp("vector",[TA_nexp start; TA_nexp size; TA_ord {order}; TA_typ typ])}
+let mk_vector typ order start size = {t=Tapp("vector",[TA_nexp start; TA_nexp size; TA_ord order; TA_typ typ])}
 let mk_bitwise_op name symb arity =
-  let ovar = Ovar "o"  in
+  let ovar = mk_ovar "o"  in
   let vec_typ = mk_vector bit_t ovar (mk_nv "n") (mk_nv "m") in
   let single_bit_vec_typ = mk_vector bit_t ovar (mk_nv "n") n_one in
   let vec_args = Array.to_list (Array.make arity vec_typ) in
@@ -1959,7 +1960,7 @@ let initial_typ_env =
     ("None", Base((["a", {k=K_Typ}], mk_pure_fun unit_t {t=Tapp("option", [TA_typ {t=Tvar "a"}])}),
                   Constructor 2,[],pure_e,pure_e,nob));
     ("most_significant", lib_tannot ((mk_nat_params ["n";"m"]@(mk_ord_params ["ord"])),
-                                     (mk_pure_fun (mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m")) bit_t))
+                                     (mk_pure_fun (mk_vector bit_t (mk_ovar "ord") (mk_nv "n") (mk_nv "m")) bit_t))
                                     None []);
     ("+",Overload(
       lib_tannot ((mk_typ_params ["a";"b";"c"]),
@@ -1970,51 +1971,51 @@ let initial_typ_env =
                                 (mk_atom (mk_add (mk_nv "n") (mk_nv "m")))))
                   (Some "add") [];
        lib_tannot ((mk_nat_params ["n";"o";"p"])@(mk_ord_params ["ord"]),
-                   (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "n");
-                                         mk_vector bit_t (Ovar "ord") (mk_nv "p") (mk_nv "n")])
-                                (mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "n"))))
+                   (mk_pure_fun (mk_tup [mk_vector bit_t (mk_ovar "ord") (mk_nv "o") (mk_nv "n");
+                                         mk_vector bit_t (mk_ovar "ord") (mk_nv "p") (mk_nv "n")])
+                                (mk_vector bit_t (mk_ovar "ord") (mk_nv "o") (mk_nv "n"))))
                   (Some "add_vec") [];
        lib_tannot ((mk_nat_params ["n";"o";"p";"q"])@(mk_ord_params ["ord"]),
-                   (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "n");
-                                         mk_vector bit_t (Ovar "ord") (mk_nv "p") (mk_nv "n")])
+                   (mk_pure_fun (mk_tup [mk_vector bit_t (mk_ovar "ord") (mk_nv "o") (mk_nv "n");
+                                         mk_vector bit_t (mk_ovar "ord") (mk_nv "p") (mk_nv "n")])
                                 (mk_range (mk_nv "q") (mk_2n (mk_nv "n")))))
                   (Some "add_vec_vec_range") [];
        lib_tannot ((mk_nat_params ["n";"m";"o"])@(mk_ord_params ["ord"]),
-                   (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m");
+                   (mk_pure_fun (mk_tup [mk_vector bit_t (mk_ovar "ord") (mk_nv "n") (mk_nv "m");
                                          mk_atom (mk_nv "o")])
-                                (mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m"))))
+                                (mk_vector bit_t (mk_ovar "ord") (mk_nv "n") (mk_nv "m"))))
                   (Some "add_vec_range")
                   [LtEq(Specc(Parse_ast.Int("+",None)),Require, (mk_nv "o"),mk_sub (mk_2n (mk_nv "m")) n_one)];
        lib_tannot ((mk_nat_params ["n";"o";"p"])@(mk_ord_params ["ord"]),
-                   (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "n");
-                                         mk_vector bit_t (Ovar "ord") (mk_nv "p") (mk_nv "n")])
-                                (mk_tup [(mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "n")); bit_t; bit_t])))
+                   (mk_pure_fun (mk_tup [mk_vector bit_t (mk_ovar "ord") (mk_nv "o") (mk_nv "n");
+                                         mk_vector bit_t (mk_ovar "ord") (mk_nv "p") (mk_nv "n")])
+                                (mk_tup [(mk_vector bit_t (mk_ovar "ord") (mk_nv "o") (mk_nv "n")); bit_t; bit_t])))
                   (Some "add_overflow_vec") [];
        lib_tannot ((mk_nat_params ["n";"m";"o";])@(mk_ord_params ["ord"]),
-                   (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m");
+                   (mk_pure_fun (mk_tup [mk_vector bit_t (mk_ovar "ord") (mk_nv "n") (mk_nv "m");
                                          mk_atom (mk_nv "o")])
                                 (mk_range (mk_nv "o") (mk_add (mk_nv "o") (mk_2n (mk_nv "m"))))))
                   (Some "add_vec_range_range")
                   [LtEq(Specc(Parse_ast.Int("+",None)),Require,(mk_nv "o"),mk_sub (mk_2n (mk_nv "m")) n_one)];
        lib_tannot ((mk_nat_params ["n";"m";"o"])@(mk_ord_params ["ord"]),
                    (mk_pure_fun (mk_tup [mk_atom (mk_nv "o");
-                                         mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m");])
-                                (mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m"))))
+                                         mk_vector bit_t (mk_ovar "ord") (mk_nv "n") (mk_nv "m");])
+                                (mk_vector bit_t (mk_ovar "ord") (mk_nv "n") (mk_nv "m"))))
                   (Some "add_range_vec")
                   [LtEq(Specc(Parse_ast.Int("+",None)),Require,(mk_nv "o"),mk_sub (mk_2n (mk_nv "m")) n_one)];
        lib_tannot ((mk_nat_params ["n";"m";"o"])@(mk_ord_params ["ord"]),
                    (mk_pure_fun (mk_tup [mk_atom (mk_nv "o");
-                                         mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m");])
+                                         mk_vector bit_t (mk_ovar "ord") (mk_nv "n") (mk_nv "m");])
                                 (mk_range (mk_nv "o") (mk_add (mk_nv "o") (mk_sub (mk_2n (mk_nv "m")) n_one)))))
                   (Some "add_range_vec_range")
                   [LtEq(Specc(Parse_ast.Int("+",None)),Require,(mk_nv "o"),mk_sub (mk_2n (mk_nv "m")) n_one)];
        lib_tannot ((mk_nat_params ["o";"p"]@(mk_ord_params["ord"])),
-                   (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "p"); bit_t])
-                                (mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "p"))))
+                   (mk_pure_fun (mk_tup [mk_vector bit_t (mk_ovar "ord") (mk_nv "o") (mk_nv "p"); bit_t])
+                                (mk_vector bit_t (mk_ovar "ord") (mk_nv "o") (mk_nv "p"))))
                    (Some "add_vec_bit") [];
        lib_tannot ((mk_nat_params ["o";"p"]@(mk_ord_params["ord"])),
-                   (mk_pure_fun (mk_tup [bit_t; mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "p")])
-                                (mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "p"))))
+                   (mk_pure_fun (mk_tup [bit_t; mk_vector bit_t (mk_ovar "ord") (mk_nv "o") (mk_nv "p")])
+                                (mk_vector bit_t (mk_ovar "ord") (mk_nv "o") (mk_nv "p"))))
                   (Some "add_bit_vec") [];
       ]));
     ("+_s",Overload(
@@ -2026,55 +2027,55 @@ let initial_typ_env =
                                 (mk_atom (mk_add (mk_nv "n") (mk_nv "m")))))
                   (Some "add_signed") [];
        lib_tannot ((mk_nat_params ["n";"o";"p"])@(mk_ord_params ["ord"]),
-                  (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "n");
-                                        mk_vector bit_t (Ovar "ord") (mk_nv "p") (mk_nv "n")])
-                               (mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "n"))))
+                  (mk_pure_fun (mk_tup [mk_vector bit_t (mk_ovar "ord") (mk_nv "o") (mk_nv "n");
+                                        mk_vector bit_t (mk_ovar "ord") (mk_nv "p") (mk_nv "n")])
+                               (mk_vector bit_t (mk_ovar "ord") (mk_nv "o") (mk_nv "n"))))
                   (Some "add_vec_signed") [];
        lib_tannot ((mk_nat_params ["n";"o";"p";"q"])@(mk_ord_params ["ord"]),
-                   (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "n");
-                                         mk_vector bit_t (Ovar "ord") (mk_nv "p") (mk_nv "n")])
+                   (mk_pure_fun (mk_tup [mk_vector bit_t (mk_ovar "ord") (mk_nv "o") (mk_nv "n");
+                                         mk_vector bit_t (mk_ovar "ord") (mk_nv "p") (mk_nv "n")])
                                 (mk_range (mk_nv "q") (mk_2n (mk_nv "n")))))
                   (Some "add_vec_vec_range_signed") [];
        lib_tannot ((mk_nat_params ["n";"m";"o"])@(mk_ord_params ["ord"]),
-                   (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m");
+                   (mk_pure_fun (mk_tup [mk_vector bit_t (mk_ovar "ord") (mk_nv "n") (mk_nv "m");
                                          mk_atom (mk_nv "o")])
-                                (mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m"))))
+                                (mk_vector bit_t (mk_ovar "ord") (mk_nv "n") (mk_nv "m"))))
                   (Some "add_vec_range_signed")
                   [LtEq(Specc(Parse_ast.Int("+",None)),Require,(mk_nv "o"),(mk_sub (mk_2n (mk_nv "m")) n_one))];
        lib_tannot ((mk_nat_params ["n";"o";"p"])@(mk_ord_params ["ord"]),
-                   (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "n");
-                                         mk_vector bit_t (Ovar "ord") (mk_nv "p") (mk_nv "n")])
-                                (mk_tup [(mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "n")); bit_t; bit_t])))
+                   (mk_pure_fun (mk_tup [mk_vector bit_t (mk_ovar "ord") (mk_nv "o") (mk_nv "n");
+                                         mk_vector bit_t (mk_ovar "ord") (mk_nv "p") (mk_nv "n")])
+                                (mk_tup [(mk_vector bit_t (mk_ovar "ord") (mk_nv "o") (mk_nv "n")); bit_t; bit_t])))
                   (Some "add_overflow_vec_signed") [];
        lib_tannot ((mk_nat_params ["n";"m";"o";])@(mk_ord_params ["ord"]),
-                   (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m");
+                   (mk_pure_fun (mk_tup [mk_vector bit_t (mk_ovar "ord") (mk_nv "n") (mk_nv "m");
                                          mk_atom (mk_nv "o")])
                                 (mk_range (mk_nv "o") (mk_add (mk_nv "o") (mk_2n (mk_nv "m"))))))
                    (Some "add_vec_range_range_signed")
                    [LtEq(Specc(Parse_ast.Int("+",None)),Require, (mk_nv "o"),mk_sub (mk_2n (mk_nv "m")) n_one)];
        lib_tannot ((mk_nat_params ["n";"m";"o"])@(mk_ord_params ["ord"]),
                    (mk_pure_fun (mk_tup [mk_atom (mk_nv "o");
-                                         mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m");])
-                                (mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m"))))
+                                         mk_vector bit_t (mk_ovar "ord") (mk_nv "n") (mk_nv "m");])
+                                (mk_vector bit_t (mk_ovar "ord") (mk_nv "n") (mk_nv "m"))))
                   (Some "add_range_vec_signed")
                   [LtEq(Specc(Parse_ast.Int("+",None)),Require,(mk_nv "o"),(mk_sub (mk_2n (mk_nv "m")) n_one))];
        lib_tannot ((mk_nat_params ["n";"m";"o";])@(mk_ord_params ["ord"]),
                    (mk_pure_fun (mk_tup [mk_atom (mk_nv "o");
-                                         mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m");])
+                                         mk_vector bit_t (mk_ovar "ord") (mk_nv "n") (mk_nv "m");])
                                 (mk_range (mk_nv "o") (mk_add (mk_nv "o") (mk_2n (mk_nv "m"))))))
                   (Some "add_range_vec_range_signed")
                   [LtEq(Specc(Parse_ast.Int("+",None)),Require,(mk_nv "o"),(mk_sub (mk_2n (mk_nv "m")) n_one))];
        lib_tannot ((mk_nat_params ["o";"p"]@(mk_ord_params["ord"])),
-                   (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "p"); bit_t])
-                                (mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "p"))))
+                   (mk_pure_fun (mk_tup [mk_vector bit_t (mk_ovar "ord") (mk_nv "o") (mk_nv "p"); bit_t])
+                                (mk_vector bit_t (mk_ovar "ord") (mk_nv "o") (mk_nv "p"))))
                   (Some "add_vec_bit_signed") [];
        lib_tannot ((mk_nat_params ["o";"p"]@(mk_ord_params["ord"])),
-                   (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "p"); bit_t])
-                                (mk_tup [(mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "p")); bit_t; bit_t])))
+                   (mk_pure_fun (mk_tup [mk_vector bit_t (mk_ovar "ord") (mk_nv "o") (mk_nv "p"); bit_t])
+                                (mk_tup [(mk_vector bit_t (mk_ovar "ord") (mk_nv "o") (mk_nv "p")); bit_t; bit_t])))
                   (Some "add_overflow_vec_bit_signed") [];
        lib_tannot ((mk_nat_params ["o";"p"]@(mk_ord_params["ord"])),
-                   (mk_pure_fun (mk_tup [bit_t; mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "p")])
-                                (mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "p"))))
+                   (mk_pure_fun (mk_tup [bit_t; mk_vector bit_t (mk_ovar "ord") (mk_nv "o") (mk_nv "p")])
+                                (mk_vector bit_t (mk_ovar "ord") (mk_nv "o") (mk_nv "p"))))
                   (Some "add_bit_vec_signed") [];
       ]));
     ("-_s",Overload(
@@ -2086,38 +2087,38 @@ let initial_typ_env =
                                 (mk_atom (mk_sub (mk_nv "n") (mk_nv "m")))))
                   (Some "minus") [];
        lib_tannot ((mk_nat_params ["n";"o";"p"])@(mk_ord_params ["ord"]),
-                   (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "n");
-                                         mk_vector bit_t (Ovar "ord") (mk_nv "p") (mk_nv "n")])
-                                (mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "n"))))
+                   (mk_pure_fun (mk_tup [mk_vector bit_t (mk_ovar "ord") (mk_nv "o") (mk_nv "n");
+                                         mk_vector bit_t (mk_ovar "ord") (mk_nv "p") (mk_nv "n")])
+                                (mk_vector bit_t (mk_ovar "ord") (mk_nv "o") (mk_nv "n"))))
                   (Some "minus_vec_signed") [];
        lib_tannot ((mk_nat_params ["n";"m";"o"])@(mk_ord_params ["ord"]),
-                   (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m");
+                   (mk_pure_fun (mk_tup [mk_vector bit_t (mk_ovar "ord") (mk_nv "n") (mk_nv "m");
                                          mk_atom (mk_nv "o")])
-                                (mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m"))))
+                                (mk_vector bit_t (mk_ovar "ord") (mk_nv "n") (mk_nv "m"))))
                   (Some "minus_vec_range_signed") [];
        lib_tannot ((mk_nat_params ["n";"m";"o";])@(mk_ord_params ["ord"]),
-                   (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m");
+                   (mk_pure_fun (mk_tup [mk_vector bit_t (mk_ovar "ord") (mk_nv "n") (mk_nv "m");
                                          mk_atom (mk_nv "o")])
                                 (mk_range (mk_nv "o") (mk_add (mk_nv "o") (mk_2n (mk_nv "m"))))))
                   (Some "minus_vec_range_range_signed") [];
        lib_tannot ((mk_nat_params ["n";"m";"o"])@(mk_ord_params ["ord"]),
                    (mk_pure_fun (mk_tup [mk_atom (mk_nv "o");
-                                         mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m");])
-                                (mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m"))))
+                                         mk_vector bit_t (mk_ovar "ord") (mk_nv "n") (mk_nv "m");])
+                                (mk_vector bit_t (mk_ovar "ord") (mk_nv "n") (mk_nv "m"))))
                   (Some "minus_range_vec_signed") []; 
        lib_tannot ((mk_nat_params ["n";"m";"o"])@(mk_ord_params ["ord"]),
                    (mk_pure_fun (mk_tup [mk_atom (mk_nv "o");
-                                         mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m");])
+                                         mk_vector bit_t (mk_ovar "ord") (mk_nv "n") (mk_nv "m");])
                                 (mk_range (mk_nv "o") (mk_add (mk_nv "o") (mk_2n (mk_nv "m"))))))
                   (Some "minus_range_vec_range_signed") [];
        lib_tannot ((mk_nat_params ["n";"o";"p"])@(mk_ord_params ["ord"]),
-                   (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "n");
-                                         mk_vector bit_t (Ovar "ord") (mk_nv "p") (mk_nv "n")])
-                                (mk_tup [(mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "n")); bit_t; bit_t])))
+                   (mk_pure_fun (mk_tup [mk_vector bit_t (mk_ovar "ord") (mk_nv "o") (mk_nv "n");
+                                         mk_vector bit_t (mk_ovar "ord") (mk_nv "p") (mk_nv "n")])
+                                (mk_tup [(mk_vector bit_t (mk_ovar "ord") (mk_nv "o") (mk_nv "n")); bit_t; bit_t])))
                   (Some "minus_overflow_vec_signed") [];
        lib_tannot ((mk_nat_params ["o";"p"]@(mk_ord_params["ord"])),
-                   (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "p"); bit_t])
-                                (mk_tup [(mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "p")); bit_t; bit_t])))
+                   (mk_pure_fun (mk_tup [mk_vector bit_t (mk_ovar "ord") (mk_nv "o") (mk_nv "p"); bit_t])
+                                (mk_tup [(mk_vector bit_t (mk_ovar "ord") (mk_nv "o") (mk_nv "p")); bit_t; bit_t])))
                   (Some "minus_overflow_vec_bit_signed") [];
       ]));
     ("-",Overload(
@@ -2129,42 +2130,42 @@ let initial_typ_env =
                                 (mk_atom (mk_sub (mk_nv "n") (mk_nv "m")))))
                   (Some "minus") [];
        lib_tannot ((mk_nat_params ["n";"o";"p"])@(mk_ord_params ["ord"]),
-                   (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "n");
-                                         mk_vector bit_t (Ovar "ord") (mk_nv "p") (mk_nv "n")])
-                                (mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "n"))))
+                   (mk_pure_fun (mk_tup [mk_vector bit_t (mk_ovar "ord") (mk_nv "o") (mk_nv "n");
+                                         mk_vector bit_t (mk_ovar "ord") (mk_nv "p") (mk_nv "n")])
+                                (mk_vector bit_t (mk_ovar "ord") (mk_nv "o") (mk_nv "n"))))
                   (Some "minus_vec") [];
        lib_tannot ((mk_nat_params ["m";"n";"o";"p"])@(mk_ord_params ["ord"]),
-                   (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "n");
-                                         mk_vector bit_t (Ovar "ord") (mk_nv "p") (mk_nv "n")])
+                   (mk_pure_fun (mk_tup [mk_vector bit_t (mk_ovar "ord") (mk_nv "o") (mk_nv "n");
+                                         mk_vector bit_t (mk_ovar "ord") (mk_nv "p") (mk_nv "n")])
                                 (mk_atom (mk_nv "m")))) (Some "minus_vec_vec_range") [];
        lib_tannot ((mk_nat_params ["n";"m";"o"])@(mk_ord_params ["ord"]),
-                   (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m");
+                   (mk_pure_fun (mk_tup [mk_vector bit_t (mk_ovar "ord") (mk_nv "n") (mk_nv "m");
                                          mk_atom (mk_nv "o")])
-                                (mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m")))) 
+                                (mk_vector bit_t (mk_ovar "ord") (mk_nv "n") (mk_nv "m")))) 
                   (Some "minus_vec_range") [];
        lib_tannot ((mk_nat_params ["n";"m";"o";])@(mk_ord_params ["ord"]),
-                   (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m");
+                   (mk_pure_fun (mk_tup [mk_vector bit_t (mk_ovar "ord") (mk_nv "n") (mk_nv "m");
                                          mk_atom (mk_nv "o")])
                                 (mk_range (mk_nv "o") (mk_add (mk_nv "o") (mk_2n (mk_nv "m"))))))
                   (Some "minus_vec_range_range") [];
        lib_tannot ((mk_nat_params ["n";"m";"o"])@(mk_ord_params ["ord"]),
                    (mk_pure_fun (mk_tup [mk_atom (mk_nv "o");
-                                         mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m");])
-                                (mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m"))))
+                                         mk_vector bit_t (mk_ovar "ord") (mk_nv "n") (mk_nv "m");])
+                                (mk_vector bit_t (mk_ovar "ord") (mk_nv "n") (mk_nv "m"))))
                   (Some "minus_range_vec") []; 
        lib_tannot ((mk_nat_params ["n";"m";"o";])@(mk_ord_params ["ord"]),
                    (mk_pure_fun (mk_tup [mk_atom (mk_nv "o");
-                                         mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m");])
+                                         mk_vector bit_t (mk_ovar "ord") (mk_nv "n") (mk_nv "m");])
                                 (mk_range (mk_nv "o") (mk_add (mk_nv "o") (mk_2n (mk_nv "m"))))))
                   (Some "minus_range_vec_range") [];
        lib_tannot ((mk_nat_params ["n";"o";"p"])@(mk_ord_params ["ord"]),
-                   (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "n");
-                                         mk_vector bit_t (Ovar "ord") (mk_nv "p") (mk_nv "n")])
-                                (mk_tup [(mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "n")); bit_t; bit_t])))
+                   (mk_pure_fun (mk_tup [mk_vector bit_t (mk_ovar "ord") (mk_nv "o") (mk_nv "n");
+                                         mk_vector bit_t (mk_ovar "ord") (mk_nv "p") (mk_nv "n")])
+                                (mk_tup [(mk_vector bit_t (mk_ovar "ord") (mk_nv "o") (mk_nv "n")); bit_t; bit_t])))
                   (Some "minus_overflow_vec") [];
        lib_tannot ((mk_nat_params ["o";"p"]@(mk_ord_params["ord"])),
-                   (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "p"); bit_t])
-                                (mk_tup [(mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "p")); bit_t; bit_t])))
+                   (mk_pure_fun (mk_tup [mk_vector bit_t (mk_ovar "ord") (mk_nv "o") (mk_nv "p"); bit_t])
+                                (mk_tup [(mk_vector bit_t (mk_ovar "ord") (mk_nv "o") (mk_nv "p")); bit_t; bit_t])))
                    (Some "minus_overflow_vec_bit") [];
       ]));
     ("*",Overload(
@@ -2177,19 +2178,19 @@ let initial_typ_env =
                                 (mk_atom (mk_mult (mk_nv "n") (mk_nv "m")))))
                   (Some "multiply") [];
        Base(((mk_nat_params ["n";"o";"p";"q"])@(mk_ord_params ["ord"]),
-             (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "n");
-                                   mk_vector bit_t (Ovar "ord") (mk_nv "p") (mk_nv "n")])
-                          (mk_vector bit_t (Ovar "ord") (mk_nv "q") (mk_add (mk_nv "n") (mk_nv "n"))))),
+             (mk_pure_fun (mk_tup [mk_vector bit_t (mk_ovar "ord") (mk_nv "o") (mk_nv "n");
+                                   mk_vector bit_t (mk_ovar "ord") (mk_nv "p") (mk_nv "n")])
+                          (mk_vector bit_t (mk_ovar "ord") (mk_nv "q") (mk_add (mk_nv "n") (mk_nv "n"))))),
             (External (Some "multiply_vec")), [],pure_e,pure_e,nob);
        Base(((mk_nat_params ["n";"m";"o";"p"])@(mk_ord_params ["ord"]),
              (mk_pure_fun (mk_tup [mk_atom (mk_nv "o");
-                                   mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m")])
-                          (mk_vector bit_t (Ovar "ord") (mk_nv "q") (mk_add (mk_nv "m") (mk_nv "m"))))),
+                                   mk_vector bit_t (mk_ovar "ord") (mk_nv "n") (mk_nv "m")])
+                          (mk_vector bit_t (mk_ovar "ord") (mk_nv "q") (mk_add (mk_nv "m") (mk_nv "m"))))),
             (External (Some "mult_range_vec")),[],pure_e,pure_e,nob);
        Base(((mk_nat_params ["n";"m";"o";"p"])@(mk_ord_params ["ord"]),
-             (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m");
+             (mk_pure_fun (mk_tup [mk_vector bit_t (mk_ovar "ord") (mk_nv "n") (mk_nv "m");
                                    mk_atom (mk_nv "o")])
-                           (mk_vector bit_t (Ovar "ord") (mk_nv "q") (mk_add (mk_nv "m") (mk_nv "m"))))),
+                           (mk_vector bit_t (mk_ovar "ord") (mk_nv "q") (mk_add (mk_nv "m") (mk_nv "m"))))),
             (External (Some "mult_vec_range")),[],pure_e,pure_e,nob);
       ]));
     ("*_s",Overload(
@@ -2202,24 +2203,24 @@ let initial_typ_env =
                           (mk_atom (mk_mult (mk_nv "n") (mk_nv "m"))))),
             (External (Some "multiply_signed")), [],pure_e,pure_e,nob);
        Base(((mk_nat_params ["n";"o";"p";"m"])@(mk_ord_params ["ord"]),
-             (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "n");
-                                   mk_vector bit_t (Ovar "ord") (mk_nv "p") (mk_nv "n")])
-                          (mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_add (mk_nv "n") (mk_nv "n"))))),
+             (mk_pure_fun (mk_tup [mk_vector bit_t (mk_ovar "ord") (mk_nv "o") (mk_nv "n");
+                                   mk_vector bit_t (mk_ovar "ord") (mk_nv "p") (mk_nv "n")])
+                          (mk_vector bit_t (mk_ovar "ord") (mk_nv "o") (mk_add (mk_nv "n") (mk_nv "n"))))),
             (External (Some "multiply_vec_signed")), [],pure_e,pure_e,nob);
        Base(((mk_nat_params ["n";"m";"o";"p"])@(mk_ord_params ["ord"]),
              (mk_pure_fun (mk_tup [mk_atom (mk_nv "o");
-                                   mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m")])
-                          (mk_vector bit_t (Ovar "ord") (mk_nv "p") (mk_add (mk_nv "m") (mk_nv "m"))))),
+                                   mk_vector bit_t (mk_ovar "ord") (mk_nv "n") (mk_nv "m")])
+                          (mk_vector bit_t (mk_ovar "ord") (mk_nv "p") (mk_add (mk_nv "m") (mk_nv "m"))))),
             (External (Some "mult_range_vec_signed")),[],pure_e,pure_e,nob);
        Base(((mk_nat_params ["n";"m";"o";"p"])@(mk_ord_params ["ord"]),
-             (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m");
+             (mk_pure_fun (mk_tup [mk_vector bit_t (mk_ovar "ord") (mk_nv "n") (mk_nv "m");
                                    mk_atom (mk_nv "o")])
-                          (mk_vector bit_t (Ovar "ord") (mk_nv "p") (mk_add (mk_nv "m") (mk_nv "m"))))),
+                          (mk_vector bit_t (mk_ovar "ord") (mk_nv "p") (mk_add (mk_nv "m") (mk_nv "m"))))),
             (External (Some "mult_vec_range_signed")),[],pure_e,pure_e,nob);
        Base(((mk_nat_params ["n";"o";"p";"m"])@(mk_ord_params ["ord"]),
-             (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "n");
-                                   mk_vector bit_t (Ovar "ord") (mk_nv "p") (mk_nv "n")])
-                          (mk_tup [(mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_add (mk_nv "n") (mk_nv "n")));
+             (mk_pure_fun (mk_tup [mk_vector bit_t (mk_ovar "ord") (mk_nv "o") (mk_nv "n");
+                                   mk_vector bit_t (mk_ovar "ord") (mk_nv "p") (mk_nv "n")])
+                          (mk_tup [(mk_vector bit_t (mk_ovar "ord") (mk_nv "o") (mk_add (mk_nv "n") (mk_nv "n")));
                                    bit_t;bit_t]))),
             (External (Some "mult_overflow_vec_signed")), [],pure_e,pure_e,nob);
       ]));
@@ -2240,15 +2241,15 @@ let initial_typ_env =
              (External (Some "modulo")),
              [GtEq(Specc(Parse_ast.Int("modulo",None)),Require,(mk_nv "o"),n_one)],pure_e,pure_e,nob);
         Base(((mk_nat_params["n";"m";"o"])@(mk_ord_params["ord"]),
-              (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m");
+              (mk_pure_fun (mk_tup [mk_vector bit_t (mk_ovar "ord") (mk_nv "n") (mk_nv "m");
                                     mk_range n_one (mk_nv "o")])
-                           (mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m")))),
+                           (mk_vector bit_t (mk_ovar "ord") (mk_nv "n") (mk_nv "m")))),
              (External (Some "mod_vec_range")),
              [GtEq(Specc(Parse_ast.Int("mod",None)),Require,(mk_nv "o"),n_one);],pure_e,pure_e,nob);
         Base(((mk_nat_params["n";"m"])@(mk_ord_params["ord"]),
-              (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m");
-                                    mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m")])
-                 (mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m")))),
+              (mk_pure_fun (mk_tup [mk_vector bit_t (mk_ovar "ord") (mk_nv "n") (mk_nv "m");
+                                    mk_vector bit_t (mk_ovar "ord") (mk_nv "n") (mk_nv "m")])
+                 (mk_vector bit_t (mk_ovar "ord") (mk_nv "n") (mk_nv "m")))),
              (External (Some "mod_vec")),[],pure_e,pure_e,nob)]));
     ("mod_s",
      Overload(
@@ -2262,15 +2263,15 @@ let initial_typ_env =
              (External (Some "mod_signed")),
              [GtEq(Specc(Parse_ast.Int("modulo",None)),Require,(mk_nv "o"),n_one)],pure_e,pure_e,nob);
         Base(((mk_nat_params["n";"m";"o"])@(mk_ord_params["ord"]),
-              (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m");
+              (mk_pure_fun (mk_tup [mk_vector bit_t (mk_ovar "ord") (mk_nv "n") (mk_nv "m");
                                     mk_range n_one (mk_nv "o")])
-                           (mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m")))),
+                           (mk_vector bit_t (mk_ovar "ord") (mk_nv "n") (mk_nv "m")))),
              (External (Some "mod_signed_vec_range")),
              [GtEq(Specc(Parse_ast.Int("mod",None)),Require,(mk_nv "o"),n_one);],pure_e,pure_e,nob);
         Base(((mk_nat_params["n";"m"])@(mk_ord_params["ord"]),
-              (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m");
-                                    mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m")])
-                 (mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m")))),
+              (mk_pure_fun (mk_tup [mk_vector bit_t (mk_ovar "ord") (mk_nv "n") (mk_nv "m");
+                                    mk_vector bit_t (mk_ovar "ord") (mk_nv "n") (mk_nv "m")])
+                 (mk_vector bit_t (mk_ovar "ord") (mk_nv "n") (mk_nv "m")))),
              (External (Some "mod_signed_vec")),[],pure_e,pure_e,nob)]));
     ("div",
      Base(((mk_nat_params["n";"m";"o";]),
@@ -2296,15 +2297,15 @@ let initial_typ_env =
                                           (mk_mult (mk_nv "n") (mk_nv "o")),(mk_nv "m"))],
              pure_e,pure_e,nob);
         Base(((mk_nat_params["n";"m";"p";"q"])@(mk_ord_params["ord"]),
-              (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m");
-                                    mk_vector bit_t (Ovar "ord") (mk_nv "p") (mk_nv "q")])
-                           (mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m")))),
+              (mk_pure_fun (mk_tup [mk_vector bit_t (mk_ovar "ord") (mk_nv "n") (mk_nv "m");
+                                    mk_vector bit_t (mk_ovar "ord") (mk_nv "p") (mk_nv "q")])
+                           (mk_vector bit_t (mk_ovar "ord") (mk_nv "n") (mk_nv "m")))),
              (External (Some "quot_vec")),[GtEq(Specc(Parse_ast.Int("quot",None)),Require, mk_nv "m", mk_nv "q")],
              pure_e,pure_e,nob);
         Base(((mk_nat_params["n";"m";"p";"q"])@(mk_ord_params["ord"]),
-              (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m");
-                                    mk_vector bit_t (Ovar "ord") (mk_nv "p") (mk_nv "q")])
-                           (mk_tup [(mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m")); bit_t;bit_t]))),
+              (mk_pure_fun (mk_tup [mk_vector bit_t (mk_ovar "ord") (mk_nv "n") (mk_nv "m");
+                                    mk_vector bit_t (mk_ovar "ord") (mk_nv "p") (mk_nv "q")])
+                           (mk_tup [(mk_vector bit_t (mk_ovar "ord") (mk_nv "n") (mk_nv "m")); bit_t;bit_t]))),
              (External (Some "quot_overflow_vec")),
              [GtEq(Specc(Parse_ast.Int("quot",None)),Require, mk_nv "m", mk_nv "q")],
              pure_e,pure_e,nob)]));
@@ -2321,26 +2322,26 @@ let initial_typ_env =
               LtEq(Specc(Parse_ast.Int("quot",None)),Guarantee,(mk_mult (mk_nv "p") (mk_nv "r")),mk_nv "m")],
              pure_e,pure_e,nob);
         Base(((mk_nat_params["n";"m";"p";"q"])@(mk_ord_params["ord"]),
-              (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m");
-                                    mk_vector bit_t (Ovar "ord") (mk_nv "p") (mk_nv "q")])
-                           (mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m")))),
+              (mk_pure_fun (mk_tup [mk_vector bit_t (mk_ovar "ord") (mk_nv "n") (mk_nv "m");
+                                    mk_vector bit_t (mk_ovar "ord") (mk_nv "p") (mk_nv "q")])
+                           (mk_vector bit_t (mk_ovar "ord") (mk_nv "n") (mk_nv "m")))),
              (External (Some "quot_vec_signed")),
              [GtEq(Specc(Parse_ast.Int("quot",None)),Require, mk_nv "m", mk_nv "q")],pure_e,pure_e,nob);
         Base(((mk_nat_params["n";"m";"p";"q"])@(mk_ord_params["ord"]),
-              (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m");
-                                    mk_vector bit_t (Ovar "ord") (mk_nv "p") (mk_nv "q")])
-                           (mk_tup [(mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m")); bit_t;bit_t]))),
+              (mk_pure_fun (mk_tup [mk_vector bit_t (mk_ovar "ord") (mk_nv "n") (mk_nv "m");
+                                    mk_vector bit_t (mk_ovar "ord") (mk_nv "p") (mk_nv "q")])
+                           (mk_tup [(mk_vector bit_t (mk_ovar "ord") (mk_nv "n") (mk_nv "m")); bit_t;bit_t]))),
              (External (Some "quot_overflow_vec_signed")),
              [GtEq(Specc(Parse_ast.Int("quot",None)),Require, mk_nv "m", mk_nv "q")],pure_e,pure_e,nob);
        ]));
     ("length", Base((["a",{k=K_Typ}]@(mk_nat_params["n";"m"])@(mk_ord_params["ord"]),
-                     (mk_pure_fun (mk_vector {t=Tvar "a"} (Ovar "ord") (mk_nv "n") (mk_nv "m"))
+                     (mk_pure_fun (mk_vector {t=Tvar "a"} (mk_ovar "ord") (mk_nv "n") (mk_nv "m"))
                                   (mk_atom (mk_nv "m")))),
                     (External (Some "length")),[],pure_e,pure_e,nob));
     (* incorrect types for typechecking processed sail code; do we care? *)
     ("mask",Base(((mk_typ_params ["a"])@(mk_nat_params["n";"m";"o";"p"])@(mk_ord_params["ord"]),
-                  (mk_pure_imp (mk_vector {t=Tvar "a"} (Ovar "ord") (mk_nv "n") (mk_nv "m"))
-                               (mk_vector {t=Tvar "a"} (Ovar "ord") (mk_nv "p") (mk_nv "o")) "o")),
+                  (mk_pure_imp (mk_vector {t=Tvar "a"} (mk_ovar "ord") (mk_nv "n") (mk_nv "m"))
+                               (mk_vector {t=Tvar "a"} (mk_ovar "ord") (mk_nv "p") (mk_nv "o")) "o")),
                  (External (Some "mask")),
                  [GtEq(Specc(Parse_ast.Int("mask",None)),Guarantee, (mk_nv "m"), (mk_nv "o"))],pure_e,pure_e,nob));
     (*TODO These should be IP_start *)
@@ -2364,12 +2365,12 @@ let initial_typ_env =
         (* == : bit['n] * [:'o:] -> bit_t *)
         Base(((mk_nat_params ["n";"m";"o"])@(mk_ord_params ["ord"]),
               (mk_pure_fun (mk_tup [mk_atom (mk_nv "o");
-                                    mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m")])
+                                    mk_vector bit_t (mk_ovar "ord") (mk_nv "n") (mk_nv "m")])
                            bit_t)),
              (External (Some "eq_range_vec")),[],pure_e,pure_e,nob);
         (* == : [:'o:] * bit['n] -> bit_t *)
         Base(((mk_nat_params ["n";"m";"o"])@(mk_ord_params ["ord"]),
-              (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m");
+              (mk_pure_fun (mk_tup [mk_vector bit_t (mk_ovar "ord") (mk_nv "n") (mk_nv "m");
                                     mk_atom (mk_nv "o")])
                            bit_t)),
              (External (Some "eq_vec_range")),[],pure_e,pure_e,nob);
@@ -2390,11 +2391,11 @@ let initial_typ_env =
                         GtEq(Specc(Parse_ast.Int("<",None)),Guarantee, mk_nv "n", mk_nv "m"))],
              pure_e,pure_e,nob);
         Base((((mk_nat_params ["n";"o";"p"])@["ord",{k=K_Ord}]),
-              (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "n");
-                                    mk_vector bit_t (Ovar "ord") (mk_nv "p") (mk_nv "n")]) bit_t)),
+              (mk_pure_fun (mk_tup [mk_vector bit_t (mk_ovar "ord") (mk_nv "o") (mk_nv "n");
+                                    mk_vector bit_t (mk_ovar "ord") (mk_nv "p") (mk_nv "n")]) bit_t)),
              (External (Some "lt_vec")),[],pure_e,pure_e,nob);
        Base(((mk_nat_params ["n";"m";"o"]@["ord",{k=K_Ord}]),
-             (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m");
+             (mk_pure_fun (mk_tup [mk_vector bit_t (mk_ovar "ord") (mk_nv "n") (mk_nv "m");
                                    mk_atom (mk_nv "o")]) bit_t)),
             (External (Some "lt_vec_range")), [], pure_e,pure_e, nob);
        ]));
@@ -2411,8 +2412,8 @@ let initial_typ_env =
                         GtEq(Specc(Parse_ast.Int("<_s",None)),Guarantee, mk_nv "n", mk_nv "m"))],
              pure_e,pure_e,nob);
         Base((((mk_nat_params ["n";"o";"p"])@["ord",{k=K_Ord}]),
-              (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "n");
-                                    mk_vector bit_t (Ovar "ord") (mk_nv "p") (mk_nv "n")]) bit_t)),
+              (mk_pure_fun (mk_tup [mk_vector bit_t (mk_ovar "ord") (mk_nv "o") (mk_nv "n");
+                                    mk_vector bit_t (mk_ovar "ord") (mk_nv "p") (mk_nv "n")]) bit_t)),
              (External (Some "lt_vec_signed")),[],pure_e,pure_e,nob);
        ]));
     ("<_u",
@@ -2428,8 +2429,8 @@ let initial_typ_env =
                         GtEq(Specc(Parse_ast.Int("<_u",None)),Guarantee, mk_nv "n", mk_nv "m"))],
              pure_e,pure_e,nob);
         Base((((mk_nat_params ["n";"o";"p"])@["ord",{k=K_Ord}]),
-              (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "n");
-                                    mk_vector bit_t (Ovar "ord") (mk_nv "p") (mk_nv "n")]) bit_t)),
+              (mk_pure_fun (mk_tup [mk_vector bit_t (mk_ovar "ord") (mk_nv "o") (mk_nv "n");
+                                    mk_vector bit_t (mk_ovar "ord") (mk_nv "p") (mk_nv "n")]) bit_t)),
              (External (Some "lt_vec_unsigned")),[],pure_e,pure_e,nob);
        ]));
     (">",
@@ -2445,11 +2446,11 @@ let initial_typ_env =
                         LtEq(Specc(Parse_ast.Int(">",None)),Guarantee, mk_nv "n", mk_nv "m"))],
              pure_e,pure_e,nob);
         Base((((mk_nat_params ["n";"o";"p"])@[("ord",{k=K_Ord})]),
-              (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "n");
-                                    mk_vector bit_t (Ovar "ord") (mk_nv "p") (mk_nv "n")]) bit_t)), 
+              (mk_pure_fun (mk_tup [mk_vector bit_t (mk_ovar "ord") (mk_nv "o") (mk_nv "n");
+                                    mk_vector bit_t (mk_ovar "ord") (mk_nv "p") (mk_nv "n")]) bit_t)), 
              (External (Some "gt_vec")),[],pure_e,pure_e,nob);
        Base(((mk_nat_params ["n";"m";"o";]@["ord",{k=K_Ord}]),
-             (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m");
+             (mk_pure_fun (mk_tup [mk_vector bit_t (mk_ovar "ord") (mk_nv "n") (mk_nv "m");
                                    mk_atom (mk_nv "o")]) bit_t)),
             (External (Some "gt_vec_range")), [], pure_e,pure_e, nob);
        ]));
@@ -2466,8 +2467,8 @@ let initial_typ_env =
                         LtEq(Specc(Parse_ast.Int(">_s",None)),Guarantee, mk_nv "m", mk_nv "m"))],
              pure_e,pure_e,nob);
         Base((((mk_nat_params ["n";"o";"p"])@[("ord",{k=K_Ord})]),
-              (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "n");
-                                    mk_vector bit_t (Ovar "ord") (mk_nv "p") (mk_nv "n")]) bit_t)), 
+              (mk_pure_fun (mk_tup [mk_vector bit_t (mk_ovar "ord") (mk_nv "o") (mk_nv "n");
+                                    mk_vector bit_t (mk_ovar "ord") (mk_nv "p") (mk_nv "n")]) bit_t)), 
              (External (Some "gt_vec_signed")),[],pure_e,pure_e,nob);
        ]));
     (">_u",
@@ -2483,8 +2484,8 @@ let initial_typ_env =
                         LtEq(Specc(Parse_ast.Int(">_u",None)),Guarantee, mk_nv "n", mk_nv "n"))],
              pure_e,pure_e,nob);
         Base((((mk_nat_params ["n";"o";"p"])@[("ord",{k=K_Ord})]),
-              (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "n");
-                                    mk_vector bit_t (Ovar "ord") (mk_nv "p") (mk_nv "n")]) bit_t)), 
+              (mk_pure_fun (mk_tup [mk_vector bit_t (mk_ovar "ord") (mk_nv "o") (mk_nv "n");
+                                    mk_vector bit_t (mk_ovar "ord") (mk_nv "p") (mk_nv "n")]) bit_t)), 
              (External (Some "gt_vec_unsigned")),[],pure_e,pure_e,nob);
        ]));
     ("<=",
@@ -2500,16 +2501,16 @@ let initial_typ_env =
                         Gt(Specc(Parse_ast.Int("<=",None)),Guarantee,mk_nv "n",mk_nv "m"))],
              pure_e,pure_e,nob);
         Base(((mk_nat_params ["n";"m";"o";]@["ord",{k=K_Ord}]),
-              (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m");
+              (mk_pure_fun (mk_tup [mk_vector bit_t (mk_ovar "ord") (mk_nv "n") (mk_nv "m");
                                     mk_atom (mk_nv "o")]) bit_t)),
              (External (Some "lteq_vec_range")), [], pure_e,pure_e, nob);
         Base(((mk_nat_params ["n";"m";"o";]@["ord",{k=K_Ord}]),
               (mk_pure_fun (mk_tup [mk_atom (mk_nv "o");
-                                    mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m")]) bit_t)),
+                                    mk_vector bit_t (mk_ovar "ord") (mk_nv "n") (mk_nv "m")]) bit_t)),
              (External (Some "lteq_range_vec")), [], pure_e,pure_e, nob);
         Base((((mk_nat_params ["n";"o";"p"])@["ord",{k=K_Ord}]),
-              (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "n");
-                                    mk_vector bit_t (Ovar "ord") (mk_nv "p") (mk_nv "n")]) bit_t)),
+              (mk_pure_fun (mk_tup [mk_vector bit_t (mk_ovar "ord") (mk_nv "o") (mk_nv "n");
+                                    mk_vector bit_t (mk_ovar "ord") (mk_nv "p") (mk_nv "n")]) bit_t)),
              (External (Some "lteq_vec")),[],pure_e,pure_e,nob);
        ]));
     ("<=_s",
@@ -2524,8 +2525,8 @@ let initial_typ_env =
               LtEq(Specc(Parse_ast.Int("<=",None)),Guarantee,mk_nv "m",mk_nv "p")],
              pure_e,pure_e,nob);
         Base((((mk_nat_params ["n";"o";"p"])@["ord",{k=K_Ord}]),
-              (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "n");
-                                    mk_vector bit_t (Ovar "ord") (mk_nv "p") (mk_nv "n")]) bit_t)),
+              (mk_pure_fun (mk_tup [mk_vector bit_t (mk_ovar "ord") (mk_nv "o") (mk_nv "n");
+                                    mk_vector bit_t (mk_ovar "ord") (mk_nv "p") (mk_nv "n")]) bit_t)),
              (External (Some "lteq_vec_signed")),[],pure_e,pure_e,nob);
        ]));
     (">=",
@@ -2540,16 +2541,16 @@ let initial_typ_env =
               GtEq(Specc(Parse_ast.Int(">=",None)),Guarantee, mk_nv "m", mk_nv "p")],
              pure_e,pure_e,nob);
         Base((((mk_nat_params ["n";"o";"p"])@[("ord",{k=K_Ord})]),
-              (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "n");
-                                    mk_vector bit_t (Ovar "ord") (mk_nv "p") (mk_nv "n")]) bit_t)), 
+              (mk_pure_fun (mk_tup [mk_vector bit_t (mk_ovar "ord") (mk_nv "o") (mk_nv "n");
+                                    mk_vector bit_t (mk_ovar "ord") (mk_nv "p") (mk_nv "n")]) bit_t)), 
              (External (Some "gteq_vec")),[],pure_e,pure_e,nob);
         Base(((mk_nat_params ["n";"m";"o";]@["ord",{k=K_Ord}]),
-              (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m");
+              (mk_pure_fun (mk_tup [mk_vector bit_t (mk_ovar "ord") (mk_nv "n") (mk_nv "m");
                                     mk_atom (mk_nv "o")]) bit_t)),
              (External (Some "gteq_vec_range")), [], pure_e,pure_e, nob);
         Base(((mk_nat_params ["n";"m";"o";]@["ord",{k=K_Ord}]),
               (mk_pure_fun (mk_tup [mk_atom (mk_nv "o");
-                                    mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m")]) bit_t)),
+                                    mk_vector bit_t (mk_ovar "ord") (mk_nv "n") (mk_nv "m")]) bit_t)),
              (External (Some "gteq_range_vec")), [], pure_e,pure_e, nob);
        ]));
     (">=_s",
@@ -2564,13 +2565,13 @@ let initial_typ_env =
               GtEq(Specc(Parse_ast.Int(">=_s",None)),Guarantee, mk_nv "m", mk_nv "p")],
              pure_e,pure_e,nob);
         Base((((mk_nat_params ["n";"o";"p"])@[("ord",{k=K_Ord})]),
-              (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "n");
-                                    mk_vector bit_t (Ovar "ord") (mk_nv "p") (mk_nv "n")]) bit_t)), 
+              (mk_pure_fun (mk_tup [mk_vector bit_t (mk_ovar "ord") (mk_nv "o") (mk_nv "n");
+                                    mk_vector bit_t (mk_ovar "ord") (mk_nv "p") (mk_nv "n")]) bit_t)), 
              (External (Some "gteq_vec_signed")),[],pure_e,pure_e,nob);
        ]));
     ("is_one",Base(([],(mk_pure_fun bit_t bit_t)),(External (Some "is_one")),[],pure_e,pure_e,nob));
     ("signed",Base((mk_nat_params["n";"m";"o"]@[("ord",{k=K_Ord})],
-                    (mk_pure_fun (mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m"))
+                    (mk_pure_fun (mk_vector bit_t (mk_ovar "ord") (mk_nv "n") (mk_nv "m"))
                                  (mk_atom (mk_nv "o")))),
                    External (Some "signed"), 
                   [(GtEq(Specc(Parse_ast.Int("signed",None)),Guarantee, 
@@ -2578,7 +2579,7 @@ let initial_typ_env =
                    (LtEq(Specc(Parse_ast.Int("signed",None)),Guarantee,
                          mk_nv "o", mk_sub (mk_2n (mk_nv "m")) n_one));],pure_e,pure_e,nob));
     ("unsigned",Base((mk_nat_params["n";"m";"o"]@[("ord",{k=K_Ord})],
-                    (mk_pure_fun (mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m"))
+                    (mk_pure_fun (mk_vector bit_t (mk_ovar "ord") (mk_nv "n") (mk_nv "m"))
                                  (mk_atom (mk_nv "o")))),
                    External (Some "unsigned"), 
                   [(GtEq(Specc(Parse_ast.Int("unsigned",None)),Guarantee, 
@@ -2595,40 +2596,40 @@ let initial_typ_env =
      Overload(
        Base((mk_nat_params["n";"o";"p"]@[("a",{k=K_Typ})],
              (mk_pure_fun (mk_tup [{t=Tvar "a"}; mk_atom (mk_nv "n")])
-                (mk_vector bit_t Oinc (mk_nv "o") (mk_nv "p")))),
+                (mk_vector bit_t {order = Oinc} (mk_nv "o") (mk_nv "p")))),
             External (Some "duplicate"), [], pure_e, pure_e, nob),
        false,
        [Base((mk_nat_params ["n"],
               (mk_pure_fun (mk_tup [bit_t;mk_atom (mk_nv "n")])
-                           (mk_vector bit_t Oinc (mk_c zero) (mk_nv "n")))),
+                           (mk_vector bit_t {order=Oinc} (mk_c zero) (mk_nv "n")))),
              External (Some "duplicate"),[],pure_e,pure_e,nob);
         Base((mk_nat_params ["n";"m";"o"]@mk_ord_params["or"],
-              mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "or") (mk_nv "o") (mk_nv "m");
+              mk_pure_fun (mk_tup [mk_vector bit_t (mk_ovar "or") (mk_nv "o") (mk_nv "m");
                                    mk_atom (mk_nv "n")])
-                (mk_vector bit_t (Ovar "or") (mk_nv "o") (mk_mult (mk_nv "m") (mk_nv "n")))),
+                (mk_vector bit_t (mk_ovar "or") (mk_nv "o") (mk_mult (mk_nv "m") (mk_nv "n")))),
              External (Some "duplicate_bits"),[],pure_e,pure_e,nob);]));
     ("<<",Base((((mk_nat_params ["n";"m"])@[("ord",{k=K_Ord})]),
-                (mk_pure_fun (mk_tup [(mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m"));
+                (mk_pure_fun (mk_tup [(mk_vector bit_t (mk_ovar "ord") (mk_nv "n") (mk_nv "m"));
                                       (mk_range n_zero (mk_nv "m"))])
-                             (mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m")))),
+                             (mk_vector bit_t (mk_ovar "ord") (mk_nv "n") (mk_nv "m")))),
                External (Some "bitwise_leftshift"),[],pure_e,pure_e,nob));
     (">>",Base((((mk_nat_params ["n";"m"])@[("ord",{k=K_Ord})]),
-                (mk_pure_fun (mk_tup [(mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m"));
+                (mk_pure_fun (mk_tup [(mk_vector bit_t (mk_ovar "ord") (mk_nv "n") (mk_nv "m"));
                                       (mk_range n_zero (mk_nv "m"))])
-                             (mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m")))),
+                             (mk_vector bit_t (mk_ovar "ord") (mk_nv "n") (mk_nv "m")))),
                External (Some "bitwise_rightshift"),[],pure_e,pure_e,nob));
     ("<<<",Base((((mk_nat_params ["n";"m"])@[("ord",{k=K_Ord})]),
-                     (mk_pure_fun (mk_tup [(mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m"));
+                     (mk_pure_fun (mk_tup [(mk_vector bit_t (mk_ovar "ord") (mk_nv "n") (mk_nv "m"));
                                            (mk_range n_zero (mk_nv "m"))])
-                                  (mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m")))),
+                                  (mk_vector bit_t (mk_ovar "ord") (mk_nv "n") (mk_nv "m")))),
                 External (Some "bitwise_rotate"),[],pure_e,pure_e,nob));
     ("EXTS",Base((((mk_nat_params ["n";"m";"o";"p"])@["ord",{k=K_Ord}]),
-                  (mk_pure_imp (mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "n"))
-                     (mk_vector bit_t (Ovar "ord") (mk_nv "p") (mk_nv "m")) "m")),
+                  (mk_pure_imp (mk_vector bit_t (mk_ovar "ord") (mk_nv "o") (mk_nv "n"))
+                     (mk_vector bit_t (mk_ovar "ord") (mk_nv "p") (mk_nv "m")) "m")),
                  External (Some "exts"),[],pure_e,pure_e,nob));
     ("EXTZ",Base((((mk_nat_params ["n";"m";"o";"p"])@["ord",{k=K_Ord}]),
-                  (mk_pure_imp (mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "n"))
-                     (mk_vector bit_t (Ovar "ord") (mk_nv "p") (mk_nv "m")) "m")),
+                  (mk_pure_imp (mk_vector bit_t (mk_ovar "ord") (mk_nv "o") (mk_nv "n"))
+                     (mk_vector bit_t (mk_ovar "ord") (mk_nv "p") (mk_nv "m")) "m")),
                  External (Some "extz"),[],pure_e,pure_e,nob));
     ("abs",Base(((mk_nat_params ["n";"m";]),
                  (mk_pure_fun (mk_atom (mk_nv "n")) (mk_range n_zero (mk_nv "m")))),
@@ -4171,7 +4172,7 @@ let check_range_consistent require_lt require_gt guarantee_lt guarantee_gt =
     | Some _, None, None, None | None, Some _ , None, None | None, None, Some _ , None | None, None, None, Some _ 
     | Some _, Some _,None,None | None,None,Some _,Some _ (*earlier check should ensure these*)
       -> ()
-    | Some(crlt,rlt), Some(crgt,rgt), Some(cglt,glt), Some(cggt,ggt) -> () (*
+    | Some(crlt,rlt), Some(crgt,rgt), Some(cglt,glt), Some(cggt,ggt) -> 
       if tri_to_bl (nexp_ge rlt glt) (*Can we guarantee the up is less than the required up*)
       then if tri_to_bl (nexp_ge rlt ggt) (*Can we guarantee the lw is less than the required up*)
         then if tri_to_bl (nexp_ge glt rgt) (*Can we guarantee the up is greater than the required lw*)
@@ -4181,7 +4182,7 @@ let check_range_consistent require_lt require_gt guarantee_lt guarantee_gt =
                                               ^ (n_to_string rgt) ^ " but best guarantee is " ^ (n_to_string ggt))
           else multi_constraint_error cglt crgt ("Constraints arising from these locations guarantees a number no greather than " ^ (n_to_string glt) ^ " but requires a number greater than " ^ (n_to_string rgt))
         else multi_constraint_error crlt cggt ("Constraints arising from these locations guarantees a number that is less than " ^ (n_to_string rlt) ^ " but best guarantee is " ^ (n_to_string ggt))
-      else multi_constraint_error crlt cglt ("Constraints arising from these locations require no more than " ^ (n_to_string rlt) ^ " but guarantee indicates it may be above " ^ (n_to_string glt)) *)
+      else multi_constraint_error crlt cglt ("Constraints arising from these locations require no more than " ^ (n_to_string rlt) ^ " but guarantee indicates it may be above " ^ (n_to_string glt)) 
     | _ ->
       (*let _ = Printf.eprintf "check_range_consistent is in the partial case\n" in*)
       ()
diff --git a/src/type_internal.mli b/src/type_internal.mli
index 3ce674dd..b55418fe 100644
--- a/src/type_internal.mli
+++ b/src/type_internal.mli
@@ -150,6 +150,7 @@ val set_imp_param : nexp -> unit
 
 val mk_atom : nexp -> t
 val mk_tup : t list -> t
+val mk_vector : t -> order -> nexp -> nexp -> t
 
 type variable_range =
   | VR_eq of string * nexp