Equality between range and bit vector

The type-constraints are inspired from those for (+). They seem to work
but I am not sure they make sense.

The vector is interpreted as unsigned.

2 files changed, 27 insertions, 8 deletions

diff --git a/src/lem_interp/interp_lib.lem b/src/lem_interp/interp_lib.lem
index 4d6ae138..5289be88 100644
--- a/src/lem_interp/interp_lib.lem
+++ b/src/lem_interp/interp_lib.lem
@@ -13,14 +13,6 @@ let compose f g x = f (V_tuple [g x]) ;;
 
 let is_one (V_lit (L_aux b lb)) = V_lit (L_aux (if b = L_one then L_true else L_false) lb) ;;
 
-let eq (V_tuple [x; y]) = V_lit (L_aux (if value_eq x y then L_one else L_zero) Unknown) ;;
-
-let neg (V_tuple [V_lit (L_aux arg la)]) = V_lit (L_aux (match arg with
-  | L_one -> L_zero
-  | L_zero -> L_one end) la) ;;
-
-let neq = compose neg eq ;;
-
 let lt_range (V_tuple[V_lit (L_aux (L_num l1) lr);V_lit (L_aux (L_num l2) ll);]) =
   if l1 < l2
   then V_lit (L_aux L_one Unknown)
@@ -80,6 +72,17 @@ let exts len ((V_vector _ inc _) as v) =
   to_vec inc len (to_num true v)
 ;;
 
+let eq (V_tuple [x; y]) = V_lit (L_aux (if value_eq x y then L_one else L_zero) Unknown) ;;
+(* XXX interpret vectors as unsigned numbers for equality *)
+let eq_vec_range (V_tuple [v; r]) = eq (V_tuple [to_num false v; r]) ;;
+let eq_range_vec (V_tuple [r; v]) = eq (V_tuple [r; to_num false v]) ;;
+
+let neg (V_tuple [V_lit (L_aux arg la)]) = V_lit (L_aux (match arg with
+  | L_one -> L_zero
+  | L_zero -> L_one end) la) ;;
+
+let neq = compose neg eq ;;
+
 let arith_op op (V_tuple args) = match args with
   | [V_lit(L_aux (L_num x) lx); V_lit(L_aux (L_num y) ly)] -> V_lit(L_aux (L_num (op x y)) lx)
   end ;;
@@ -138,6 +141,8 @@ let function_map = [
   ("minus", arith_op (-));
   ("minus_vec", arith_op_vec (-));
   ("eq", eq);
+  ("eq_vec_range", eq_vec_range);
+  ("eq_range_vec", eq_range_vec);
   ("neq", neq);
   ("vec_concat", vec_concat);
   ("is_one", is_one);
diff --git a/src/type_internal.ml b/src/type_internal.ml
index 00522798..5444fb9e 100644
--- a/src/type_internal.ml
+++ b/src/type_internal.ml
@@ -884,6 +884,20 @@ let initial_typ_env =
 	   [Eq(Specc(Parse_ast.Int("==",None)),
 	       {nexp=Nadd({nexp=Nvar "n"},{nexp=Nvar "m"})},
 	       {nexp=Nadd({nexp=Nvar "o"},{nexp=Nvar "p"})})],pure_e);
+      (* == : bit['n] * [|'o;'p|] -> bit_t *)
+      Base(((mk_nat_params ["n";"m";"o";"p"])@(mk_ord_params ["ord"]),
+           (mk_pure_fun (mk_tup [mk_range (mk_nv "o") (mk_nv "p");
+                                 mk_vector bit_t (Ovar "ord") (Nvar "n") (Nvar "m")])
+                        bit_t)),
+           External (Some "eq_range_vec"),
+           [Eq(Specc(Parse_ast.Int("==",None)),mk_add (mk_nv "o") (mk_nv "p"),{nexp=N2n (mk_nv "m",None)})],pure_e);
+      (* == : [|'o;'p|] * bit['n] -> bit_t *)
+      Base(((mk_nat_params ["n";"m";"o";"p"])@(mk_ord_params ["ord"]),
+           (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (Nvar "n") (Nvar "m");
+                                 mk_range (mk_nv "o") (mk_nv "p")])
+                        bit_t)),
+           External (Some "eq_vec_range"),
+           [Eq(Specc(Parse_ast.Int("==",None)),mk_add (mk_nv "o") (mk_nv "p"),{nexp=N2n (mk_nv "m",None)})],pure_e);
       Base((["a",{k=K_Typ}],{t= Tfn ({t=Ttup([{t=Tvar "a"};{t=Tvar "a"}])},bit_t,pure_e)}),External (Some "eq"),[],pure_e)]));
     ("!=",Base((["a",{k=K_Typ}],{t= Tfn ({t=Ttup([{t=Tvar "a"};{t=Tvar "a"}])},bit_t,pure_e)}),External (Some "neq"),[],pure_e));
     ("<",