expand unsigned comparisons

3 files changed, 45 insertions, 18 deletions

diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem
index 1a97f5db..7cdc5149 100644
--- a/src/lem_interp/interp.lem
+++ b/src/lem_interp/interp.lem
@@ -168,13 +168,6 @@ let reg_size reg =
       end 
 end 
 
-let vector_length v = match v with
-  | V_vector n inc vals -> List.length vals
-  | V_vector_sparse n m inc vals def -> m
-  | V_lit _ -> 1
-  | _ -> 0
-end
-
 (*Constant unit value, for use in interpreter *)
 let unitv = V_lit (L_aux L_unit Unknown)
 
@@ -458,6 +451,13 @@ let rec binary_taint thunk vall valr =
    | (vl,vr) -> thunk vl vr
 end 
 
+let vector_length v = match (detaint v) with
+  | V_vector n inc vals -> List.length vals
+  | V_vector_sparse n m inc vals def -> m
+  | V_lit _ -> 1
+  | _ -> 0
+end
+
 val access_vector : value -> nat -> value
 let access_vector v n =
   retaint v (match (detaint v) with
diff --git a/src/type_check.ml b/src/type_check.ml
index db1d8e2d..134a2c6c 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -697,7 +697,9 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)):
       let check_parms arg_t lft rht =
         match check_exp envs imp_param arg_t (E_aux(E_tuple [lft;rht],(l,NoTyp))) with
         | ((E_aux(E_tuple [lft';rht'],_)),arg_t,_,cs',_,ef') -> (lft',rht',arg_t,cs',ef')
-        | _ -> raise (Reporting_basic.err_unreachable l "check exp given tuple and tuple type and returned non-tuple") in
+        | _ -> 
+	  raise (Reporting_basic.err_unreachable l "check exp given tuple and tuple type and returned non-tuple") 
+      in
       let check_result ret imp tag cs ef lft rht =
         match imp with
 	  (*| IP_length _ ->  
@@ -724,14 +726,14 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)):
           let (lft',rht',arg_t,cs_p,ef_p) = check_parms arg lft rht in
           let ret_t,cs_r',ef_r,e' = check_result ret imp tag cs ef lft' rht' in
           (e',ret_t,t_env,cs@cs_p@cs_r',nob,union_effects ef (union_effects ef_p ef_r))
-        | _ -> typ_error l ("Expected a function or constructor, found identifier " ^ i ^ " bound to type " ^ (t_to_string t)))
+        | _ -> 
+	  typ_error l ("Expected a function, found identifier " ^ i ^ " bound to type " ^ (t_to_string t)))
       | Some(Overload(Base((params,t),tag,cs,ef,_),overload_return,variants)) ->
 	let t_p,cs_p,ef_p,_ = subst params false t cs ef in
 	let lft',rht',arg_t,arg_cs,arg_ef =  
 	  (match t_p.t with
 	  | Tfn(arg,ret,_,ef') -> check_parms arg lft rht
-	  | _ -> typ_error l ("Expected a function or constructor, found identifier " ^
-				 i ^ " bound to type " ^ (t_to_string t))) in
+	  | _ -> 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*)
 	(match (select_overload_variant d_env true overload_return variants arg_t) with
 	| [] -> 
diff --git a/src/type_internal.ml b/src/type_internal.ml
index 9534f70f..c2aa3e85 100644
--- a/src/type_internal.ml
+++ b/src/type_internal.ml
@@ -1550,6 +1550,22 @@ let initial_typ_env =
 				    mk_vector bit_t (Ovar "ord") (Nvar "p") (Nvar "n")]) bit_t)),
 	     External (Some "lt_vec_signed"),[],pure_e,nob);
        ]));
+    ("<_u",
+     Overload(
+       Base((["a",{k=K_Typ};"b",{k=K_Typ}],(mk_pure_fun (mk_tup [{t=Tvar "a"};{t=Tvar "b"}]) bit_t)),
+	    External (Some "lt"),[],pure_e,nob),
+       false,
+       [Base(((mk_nat_params ["n"; "m"; "o";"p"]),
+	      (mk_pure_fun (mk_tup [mk_range (mk_nv "n") (mk_nv "m");mk_range (mk_nv "o") (mk_nv "p")]) bit_t)),
+	     External (Some "lt_unsigned"),
+	     [LtEq(Specc(Parse_ast.Int("<_u",None)),Guarantee, mk_add (mk_nv "n") n_one, mk_nv "o");
+	      LtEq(Specc(Parse_ast.Int("<_u",None)),Guarantee, mk_add (mk_nv "m") n_one, mk_nv "p")],
+	     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") (Nvar "o") (Nvar "n");
+				    mk_vector bit_t (Ovar "ord") (Nvar "p") (Nvar "n")]) bit_t)),
+	     External (Some "lt_vec_unsigned"),[],pure_e,nob);
+       ]));
     (">",
      Overload(
        Base((["a",{k=K_Typ};"b",{k=K_Typ}],(mk_pure_fun (mk_tup [{t=Tvar "a"};{t=Tvar "b"}]) bit_t)),
@@ -1586,6 +1602,22 @@ let initial_typ_env =
 				    mk_vector bit_t (Ovar "ord") (Nvar "p") (Nvar "n")]) bit_t)), 
 	     External (Some "gt_vec_signed"),[],pure_e,nob);
        ]));
+    (">_u",
+     Overload(
+       Base((["a",{k=K_Typ};"b",{k=K_Typ}],(mk_pure_fun (mk_tup [{t=Tvar "a"};{t=Tvar "b"}]) bit_t)),
+	    External (Some "gt"),[],pure_e,nob),
+       false,
+       [Base(((mk_nat_params ["n";"m";"o";"p"]), 
+	      (mk_pure_fun (mk_tup [mk_range (mk_nv "n") (mk_nv "m");mk_range (mk_nv "o") (mk_nv "p")]) bit_t)),
+	     External (Some "gt_unsigned"),
+	     [GtEq(Specc(Parse_ast.Int(">_s",None)),Guarantee, mk_nv "n", mk_add (mk_nv "o") n_one);
+	      GtEq(Specc(Parse_ast.Int(">_s",None)),Guarantee, mk_nv "m", mk_add (mk_nv "p") n_one)],
+	     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") (Nvar "o") (Nvar "n");
+				    mk_vector bit_t (Ovar "ord") (Nvar "p") (Nvar "n")]) bit_t)), 
+	     External (Some "gt_vec_unsigned"),[],pure_e,nob);
+       ]));
     ("<=",
      Overload(
        Base((["a",{k=K_Typ}],(mk_pure_fun (mk_tup [{t=Tvar "a"};{t=Tvar "a"}]) bit_t)),
@@ -1650,13 +1682,6 @@ let initial_typ_env =
 				    mk_vector bit_t (Ovar "ord") (Nvar "p") (Nvar "n")]) bit_t)), 
 	     External (Some "gteq_vec_signed"),[],pure_e,nob);
        ]));
-    (*Unlikely to be the correct type; probably needs to be bit vectors*)
-    ("<_u",Base((["a",{k=K_Typ}],(mk_pure_fun (mk_tup [{t=Tvar "a"};{t=Tvar "a"}]) bit_t)),
-		External (Some "ltu"),[],pure_e,nob));
-    ("<_u",Base((["a",{k=K_Typ}],(mk_pure_fun (mk_tup [{t=Tvar "a"};{t=Tvar "a"}]) bit_t)),
-		External (Some "ltu"),[],pure_e,nob));
-    (">_u",Base((["a",{k=K_Typ}],(mk_pure_fun (mk_tup [{t=Tvar "a"};{t=Tvar "a"}]) bit_t)),
-		External (Some "gtu"),[],pure_e,nob));
     ("is_one",Base(([],(mk_pure_fun bit_t bit_t)),External (Some "is_one"),[],pure_e,nob));
     (*correct again*)
     mk_bitwise_op "bitwise_not" "~" 1;