Add optional overloading on expected return type to fix bug in constraint solving; get test_power running again by supporting the correct operations and bit operations

6 files changed, 121 insertions, 29 deletions

diff --git a/src/lem_interp/interp_lib.lem b/src/lem_interp/interp_lib.lem
index e994fdfe..0b7bb74a 100644
--- a/src/lem_interp/interp_lib.lem
+++ b/src/lem_interp/interp_lib.lem
@@ -49,6 +49,28 @@ let bitwise_binop op (V_tuple [V_vector idx inc v; V_vector idx' inc' v']) =
   let apply (x, y) = bool_to_bit(op (bit_to_bool x) (bit_to_bool y)) in
   V_vector idx inc (List.map apply (List.zip v v'))
 
+let bitwise_xor_bit (V_tuple [V_lit (L_aux l1 loc1);V_lit (L_aux l2 loc2)]) = match (l1,l2) with
+  | (L_zero,L_zero) -> V_lit (L_aux l1 loc1)
+  | (L_zero,L_one)  -> V_lit (L_aux l2 loc2)
+  | (L_one,L_zero)  -> V_lit (L_aux l1 loc1)
+  | (L_one,L_one)   -> V_lit (L_aux L_zero loc1)
+end;;
+
+let bitwise_or_bit (V_tuple [V_lit (L_aux l1 loc1);V_lit (L_aux l2 loc2)]) = match (l1,l2) with
+  | (L_zero,L_zero) -> V_lit (L_aux l1 loc1)
+  | (L_zero,L_one)  -> V_lit (L_aux l2 loc2)
+  | (L_one,L_zero)  -> V_lit (L_aux l1 loc1)
+  | (L_one,L_one)   -> V_lit (L_aux l1 loc1)
+end;;
+
+let bitwise_and_bit (V_tuple [V_lit (L_aux l1 loc1);V_lit (L_aux l2 loc2)]) = match (l1,l2) with
+  | (L_zero,L_zero) -> V_lit (L_aux l1 loc1)
+  | (L_zero,L_one)  -> V_lit (L_aux l1 loc1)
+  | (L_one,L_zero)  -> V_lit (L_aux l2 loc2)
+  | (L_one,L_one)   -> V_lit (L_aux l1 loc1)
+end;;
+
+
 (* BitSeq expects LSB first.
  * By convention, MSB is on the left, so increasing = Big-Endian (MSB0),
  * hence MSB first.
@@ -91,6 +113,15 @@ let arith_op_vec_range op (V_tuple args) = match args with
   else arith_op_vec op (V_tuple [l1;(to_vec_dec (List.length cs) n)])
 end ;;
 
+let arith_op_range_vec_range op (V_tuple args) = match args with
+  | [n;(V_vector _ _ _ as l2)] ->
+    arith_op op (V_tuple [n;(to_num true l2)])
+end ;;
+let arith_op_vec_range_range op (V_tuple args) = match args with
+  | [(V_vector _ _ _ as l1);n] ->
+    arith_op op (V_tuple [(to_num true l1);n])
+end ;;
+
 let compare_op op (V_tuple args) = match args with
   | [V_lit(L_aux (L_num x) lx); V_lit(L_aux (L_num y) ly)] -> 
     if (op x y)
@@ -116,7 +147,9 @@ let function_map = [
   ("add", arith_op (+));
   ("add_vec", arith_op_vec (+));
   ("add_vec_range", arith_op_vec_range (+));
+  ("add_vec_range_range", arith_op_vec_range_range (+));
   ("add_range_vec", arith_op_range_vec (+));
+  ("add_range_vec_range", arith_op_range_vec_range (+));
   ("minus", arith_op (-));
   ("minus_vec", arith_op_vec (-));
   ("eq", eq);
@@ -132,8 +165,11 @@ let function_map = [
   ("bitwise_not", bitwise_not);
   ("bitwise_not_bit", bitwise_not_bit);
   ("bitwise_and", bitwise_binop (&&));
+  ("bitwise_and_bit", bitwise_and_bit);
   ("bitwise_or", bitwise_binop (||));
+  ("bitwise_or_bit", bitwise_or_bit);
   ("bitwise_xor", bitwise_binop xor);
+  ("bitwise_xor_bit", bitwise_xor_bit);
   ("lt", compare_op (<));
   ("gt", compare_op (>));
   ("lt_vec", compare_op_vec (<));
diff --git a/src/lem_interp/run_interp.ml b/src/lem_interp/run_interp.ml
index 7e992e3a..45768966 100644
--- a/src/lem_interp/run_interp.ml
+++ b/src/lem_interp/run_interp.ml
@@ -214,7 +214,7 @@ let run
   ?(reg=Reg.empty)
   ?(mem=Mem.empty)
   (name, test) =
-  let mode = {eager_eval = true} in
+  let mode = {eager_eval = false} in
   let rec loop env = function
   | Value (v, _) -> debugf "%s: returned %s\n" name (val_to_string v); true, env
   | Action (a, s) ->
diff --git a/src/pretty_print.ml b/src/pretty_print.ml
index 7ade113c..6145c7c4 100644
--- a/src/pretty_print.ml
+++ b/src/pretty_print.ml
@@ -363,7 +363,7 @@ and pp_lem_exp ppf (E_aux(e,(l,annot))) =
     | E_let(leb,exp) -> fprintf ppf "@[<0>(E_aux (%a %a %a) (%a, %a))@]" kwd "E_let" pp_lem_let leb pp_lem_exp exp pp_lem_l l pp_annot annot
     | E_assign(lexp,exp) -> fprintf ppf "@[<0>(E_aux (%a %a %a) (%a, %a))@]" kwd "E_assign" pp_lem_lexp lexp pp_lem_exp exp pp_lem_l l pp_annot annot
   (* XXX missing cases *)
-  | E_internal_cast ((_, Overload (_, _)), _) | E_internal_exp _ -> assert false
+  | E_internal_cast ((_, Overload (_,_, _)), _) | E_internal_exp _ -> assert false
   in
   print_e ppf e
 
@@ -844,7 +844,7 @@ let doc_exp, doc_let =
       (* doc_op (doc_id op) (exp l) (exp r) *)
   (* XXX missing case
      AAA internal_cast should never have an overload, if it's been seen it's a bug *)
-  | E_internal_cast ((_, Overload (_, _)), _) | E_internal_exp _ -> assert false
+  | E_internal_cast ((_, Overload (_, _,_ )), _) | E_internal_exp _ -> assert false
 
   and let_exp (LB_aux(lb,_)) = match lb with
   | LB_val_explicit(ts,pat,e) ->
diff --git a/src/type_check.ml b/src/type_check.ml
index 5311b0b6..d198b525 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -470,7 +470,7 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp
             let (ret_t,cs_r',e') = type_coerce (Expr l) d_env false ret (E_aux(E_app(id, parms'),(l,(Base(([],ret),tag,cs,ef'))))) expect_t in
             (e',ret_t,t_env,cs@cs'@cs_r',union_effects ef_p ef'))
         | _ -> typ_error l ("Expected a function or constructor, found identifier " ^ i ^ " bound to type " ^ (t_to_string t)))
-      | Some(Overload(Base((params,t),tag,cs,ef),variants)) ->
+      | Some(Overload(Base((params,t),tag,cs,ef),overload_return,variants)) ->
 	let t_p,cs_p,ef_p = subst params t cs ef in
 	let args,arg_t,arg_cs,arg_ef =  
 	  (match t_p.t with
@@ -486,9 +486,9 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp
 		let ((E_aux(E_tuple parms',tannot')),arg_t,_,cs',ef_p) = check_exp envs arg (E_aux(E_tuple parms,(l,NoTyp))) in
 		(parms',arg_t,cs',ef_p))
 	  | _ -> typ_error l ("Expected a function or constructor, found identifier " ^ i ^ " bound to type " ^ (t_to_string t))) in
-	(match (select_overload_variant d_env variants arg_t) with
-	  | NoTyp -> typ_error l ("No matching function found with name " ^ i ^ " that expects parameters " ^ (t_to_string arg_t))
-	  | Base((params,t),tag,cs,ef) ->
+	(match (select_overload_variant d_env true overload_return variants arg_t) with
+	  | [] -> typ_error l ("No matching function found with name " ^ i ^ " that expects parameters " ^ (t_to_string arg_t))
+	  | [Base((params,t),tag,cs,ef)] ->
 	    (match t.t with
 	      | Tfn(arg,ret,ef') ->
 		let args',arg_cs' =
@@ -502,8 +502,28 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp
 		      parms',cs) in
 		let (ret_t,cs_r,e') = 
 		  type_coerce (Expr l) d_env false ret (E_aux(E_app(id,args'),(l,(Base(([],ret),tag,cs,ef))))) expect_t in
-		(e',ret_t,t_env,cs_p@arg_cs@arg_cs'@cs_r,union_effects ef_p (union_effects arg_ef ef'))
-	      | _ -> assert false))
+		(e',ret_t,t_env,cs_p@arg_cs@arg_cs'@cs_r,union_effects ef_p (union_effects arg_ef ef'))	   
+	      | _ -> assert false)
+	  | variants' ->
+	    (match select_overload_variant d_env false true variants' expect_t with
+	      | [] -> typ_error l ("No matching function found with name " ^ i ^ ", expecting parameters " ^ (t_to_string arg_t) ^ " and returning " ^ (t_to_string expect_t))
+	      | [Base((params,t),tag,cs,ef)] ->
+		(match t.t with
+		  |Tfn(arg,ret,ef') ->
+		    let args',arg_cs' = 
+		      (match args with		    
+			| [parm] ->
+			  let _,cs,parm' = type_coerce (Expr l) d_env false arg_t parm arg in
+			  [parm'],cs
+			| parms ->
+			  let (_,cs,(E_aux(E_tuple parms',tannot'))) = 
+			    type_coerce (Expr l) d_env false arg_t (E_aux(E_tuple parms,(l,NoTyp))) arg in
+			  parms',cs) in
+		    let (ret_t,cs_r,e') = 
+		      type_coerce (Expr l) d_env false ret (E_aux(E_app(id,args'),(l,(Base(([],ret),tag,cs,ef))))) expect_t in
+		    (e',ret_t,t_env,cs_p@arg_cs@arg_cs'@cs_r,union_effects ef_p (union_effects arg_ef ef'))
+	         | _ -> assert false)
+	      | _ -> typ_error l ("More than one function found with name " ^ i ^ " that expects parameters " ^ (t_to_string arg_t) ^ " and returns " ^ (t_to_string expect_t) ^ ". Try adding a cast")))
       | _ -> typ_error l ("Unbound function " ^ i)) 
     | E_app_infix(lft,op,rht) -> 
       let i = id_to_string op in
@@ -520,7 +540,7 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp
           let ret_t,cs_r',e' = type_coerce (Expr l) d_env false ret (E_aux(E_app_infix(lft',op,rht'),(l,(Base(([],ret),tag,cs,ef))))) expect_t in
           (e',ret_t,t_env,cs@cs'@cs_r',union_effects ef ef')
         | _ -> typ_error l ("Expected a function or constructor, found identifier " ^ i ^ " bound to type " ^ (t_to_string t)))
-      | Some(Overload(Base((params,t),tag,cs,ef),variants)) ->
+      | Some(Overload(Base((params,t),tag,cs,ef),overload_return,variants)) ->
 	let t_p,cs_p,ef_p = subst params t cs ef in
 	let lft',rht',arg_t,arg_cs,arg_ef =  
 	  (match t_p.t with
@@ -529,9 +549,9 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp
             (lft',rht',arg_t,cs',ef')
 	  | _ -> typ_error l ("Expected a function or constructor, found identifier " ^ i ^ " bound to type " ^ (t_to_string t))) in
         (*let _ = Printf.printf "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 variants arg_t) with
-	| NoTyp -> typ_error l ("No matching function found with name " ^ i ^ " that expects parameters " ^ (t_to_string arg_t))
-	| Base((params,t),tag,cs,ef) ->
+	(match (select_overload_variant d_env true overload_return variants arg_t) with
+	| [] -> typ_error l ("No matching function found with name " ^ i ^ " that expects parameters " ^ (t_to_string arg_t))
+	| [Base((params,t),tag,cs,ef)] ->
           (*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,ef') ->
@@ -543,7 +563,23 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp
 	        type_coerce (Expr l) d_env false ret (E_aux(E_app_infix(lft',op,rht'),(l,(Base(([],ret),tag,cs,ef))))) expect_t in
 	      (e',ret_t,t_env,cs_p@arg_cs@cs_lft@cs_rght@cs@cs_r,union_effects ef_p (union_effects arg_ef ef'))
             |_ -> assert false)
-	  | _ -> assert false))
+	  | _ -> assert false)
+	| variants ->
+	  (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)] -> 
+	      (match t.t with
+		| Tfn(arg,ret,ef') ->
+		  (match arg.t,arg_t.t with
+		    | Ttup([tlft;trght]),Ttup([tlft_t;trght_t]) ->
+		      let (_,cs_lft,lft') = type_coerce (Expr l) d_env false tlft_t lft' tlft in
+		      let (_,cs_rght,rht') = type_coerce (Expr l) d_env false trght_t rht' trght in
+		      let (ret_t,cs_r,e') = 
+			type_coerce (Expr l) d_env false ret (E_aux(E_app_infix(lft',op,rht'),(l,(Base(([],ret),tag,cs,ef))))) expect_t in
+		      (e',ret_t,t_env,cs_p@arg_cs@cs_lft@cs_rght@cs@cs_r,union_effects ef_p (union_effects arg_ef ef'))
+		    |_ -> assert false)
+		| _ -> assert false)
+	    | _ -> typ_error l ("More than one function found with name " ^ i ^ " that expects parameters " ^ (t_to_string arg_t) ^ " returning " ^ (t_to_string expect_t) ^ ". Try adding a cast")))
       | _ -> typ_error l ("Unbound infix function " ^ i))
     | E_tuple(exps) ->
       (match expect_t.t with
diff --git a/src/type_internal.ml b/src/type_internal.ml
index f8799d37..8423ecf5 100644
--- a/src/type_internal.ml
+++ b/src/type_internal.ml
@@ -95,7 +95,7 @@ type t_params = (string * kind) list
 type tannot = 
   | NoTyp
   | Base of (t_params * t) * tag * nexp_range list * effect
-  | Overload of tannot * tannot list (* First tannot is the most polymorphic version; the list includes all variants. All t to be Tfn *)
+  | Overload of tannot * bool * tannot list (* First tannot is the most polymorphic version; the boolean indicates whether the overloaded functions can use the return type; the list includes all variants. All t to be Tfn *)
 
 (*type tannot = ((t_params * t) * tag * nexp_range list * effect) option*)
 type 'a emap = 'a Envmap.t
@@ -178,7 +178,7 @@ let rec tannot_to_string = function
   | NoTyp -> "No tannot"
   | Base((vars,t),tag,ncs,ef) ->
     "Tannot: type = " ^ (t_to_string t) ^ " tag = " ^ tag_to_string tag ^ " constraints = not printing effect = " ^ e_to_string ef
-  | Overload(poly,variants) ->
+  | Overload(poly,_,variants) ->
     "Overloaded: poly = " ^ tannot_to_string poly
 
 let rec effect_remove_dups = function
@@ -758,7 +758,7 @@ let mk_bitwise_op name symb arity =
   let gen_args = Array.to_list (Array.make arity {t = Tvar "a"}) in
   let varg,barg,garg = if (arity = 1) then List.hd vec_args,List.hd bit_args,List.hd gen_args 
                        else mk_tup vec_args,mk_tup bit_args, mk_tup gen_args in
-  (symb,Overload(Base(((mk_typ_params ["a"]),mk_pure_fun garg {t=Tvar "a"}), External (Some name),[],pure_e),
+  (symb,Overload(Base(((mk_typ_params ["a"]),mk_pure_fun garg {t=Tvar "a"}), External (Some name),[],pure_e),true,
                  [Base((["n",{k=K_Nat}; "o",{k=K_Ord}], mk_pure_fun varg vec_typ),External (Some name),[],pure_e);
                   Base(([],mk_pure_fun barg bit_t),External (Some (name ^ "_bit")),[],pure_e)]))
 
@@ -767,6 +767,7 @@ let initial_typ_env =
     ("ignore",Base(([("a",{k=K_Typ})],mk_pure_fun {t=Tvar "a"} unit_t),External None,[],pure_e));
     ("+",Overload(Base(((mk_typ_params ["a";"b";"c"]),
                         (mk_pure_fun (mk_tup [{t=Tvar "a"};{t=Tvar "b"}]) {t=Tvar "c"})),External (Some "add"),[],pure_e),
+		  true,
                   [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")])
 		                      (mk_range (mk_add (mk_nv "n") (mk_nv "o")) (mk_add (mk_nv "m") (mk_nv "p"))))),
@@ -781,12 +782,25 @@ let initial_typ_env =
                                      (mk_vector bit_t (Ovar "ord") (Nvar "n") (Nvar "m")))),
                         External (Some "add_vec_range"),
                         [LtEq(Specc(Parse_ast.Int("+",None)),mk_add (mk_nv "o") (mk_nv "p"),{nexp=N2n (mk_nv "m",None)})],pure_e);
+		   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")])
+			              (mk_range (mk_nv "o") (mk_add (mk_nv "p") {nexp = N2n (mk_nv "m",None)})))),
+			External (Some "add_vec_range_range"),
+			[LtEq(Specc(Parse_ast.Int("+",None)),mk_add (mk_nv "o") (mk_nv "p"),{nexp=N2n (mk_nv "m",None)})],pure_e);
                    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");])
                                       (mk_vector bit_t (Ovar "ord") (Nvar "n") (Nvar "m")))),
                         External (Some "add_range_vec"),
                        [LtEq(Specc(Parse_ast.Int("+",None)),mk_add (mk_nv "o") (mk_nv "p"),{nexp = N2n (mk_nv "m",None)})],pure_e);
+		   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");])
+			              (mk_range (mk_nv "o") (mk_add (mk_nv "p") {nexp = N2n (mk_nv "m",None)})))),
+			External (Some "add_range_vec_range"),
+			[LtEq(Specc(Parse_ast.Int("+",None)),mk_add (mk_nv "o") (mk_nv "p"),{nexp=N2n (mk_nv "m",None)})],pure_e);
+
                   Base(((mk_nat_params ["o";"p"]@(mk_ord_params["ord"])),
                         (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (Nvar "o") (Nvar "p"); bit_t])
                                      (mk_vector bit_t (Ovar "ord") (Nvar "o") (Nvar "p")))),
@@ -802,6 +816,7 @@ let initial_typ_env =
 		        External (Some "multiply"),[],pure_e));
     ("-",Overload(Base(((mk_typ_params ["a";"b";"c"]),
                         (mk_pure_fun (mk_tup [{t=Tvar "a"};{t=Tvar "b"}]) {t=Tvar "c"})), External (Some "minus"),[],pure_e),
+		  true,
                   [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")])
@@ -829,6 +844,7 @@ let initial_typ_env =
      Overload(Base(((mk_typ_params ["a";"b";"c"]),
                     (mk_pure_fun (mk_tup [{t=Tvar "a"};{t=Tvar "b"}]) {t=Tvar "c"})),
                    External (Some "mod"),[],pure_e),
+	      true,
               [Base(((mk_nat_params["n";"m";"o"]),
                      (mk_pure_fun (mk_tup [mk_range (mk_nv "n") (mk_nv "m"); mk_range (mk_nv "o") {nexp = Nconst zero}])
                                   (mk_range {nexp = Nconst zero} (mk_sub (mk_nv "o") {nexp = Nconst one})))),
@@ -842,6 +858,7 @@ let initial_typ_env =
      Overload(Base(((mk_typ_params ["a";"b";"c"]),
                     (mk_pure_fun (mk_tup [{t=Tvar "a"};{t=Tvar "b"}]) {t=Tvar "c"})),
                    External (Some "quot"),[],pure_e),
+	      true,
               [Base(((mk_nat_params["n";"m";"o";"p";"q";"r"]),
                      (mk_pure_fun (mk_tup [mk_range (mk_nv "n") (mk_nv "m"); mk_range (mk_nv "o") (mk_nv "p")])
                                   (mk_range (mk_nv "q") (mk_nv "r")))),
@@ -861,6 +878,7 @@ let initial_typ_env =
     ("to_vec_dec",Base(([("a",{k=K_Typ})],{t= Tfn (nat_typ,{t=Tvar "a"},pure_e)}),External None,[],pure_e));
     ("==",
      Overload( Base((mk_typ_params ["a";"b"],(mk_pure_fun (mk_tup [{t=Tvar "a"};{t=Tvar "b"}]) bit_t)),External (Some "eq"),[],pure_e),
+	       false,
      [Base(([("n",{k=K_Nat});("m",{k=K_Nat});("o",{k=K_Nat});("p",{k=K_Nat})],
 	    {t = Tfn({t=Ttup([mk_range (mk_nv "n") (mk_nv "m");mk_range (mk_nv "o") (mk_nv "p")])},bit_t,pure_e)}), External (Some "eq"),
 	   [Eq(Specc(Parse_ast.Int("==",None)),
@@ -870,6 +888,7 @@ let initial_typ_env =
     ("!=",Base((["a",{k=K_Typ}],{t= Tfn ({t=Ttup([{t=Tvar "a"};{t=Tvar "a"}])},bit_t,pure_e)}),External (Some "neq"),[],pure_e));
     ("<",
      Overload(Base((["a",{k=K_Typ}],{t= Tfn ({t=Ttup([{t=Tvar "a"};{t=Tvar "a"}])},bit_t,pure_e)}),External (Some "lt"),[],pure_e),
+	      false,
      [Base(([("n",{k=K_Nat});("m",{k=K_Nat});("o",{k=K_Nat});("p",{k=K_Nat})],
 	    {t = Tfn({t=Ttup([mk_range (mk_nv "n") (mk_nv "m");mk_range (mk_nv "o") (mk_nv "p")])},bit_t,pure_e)}), External (Some "lt_vec"),
 	   [LtEq(Specc(Parse_ast.Int("<",None)),
@@ -880,6 +899,7 @@ let initial_typ_env =
                               mk_vector bit_t (Ovar "ord") (Nvar "p") (Nvar "n")])},bit_t,pure_e)}), External (Some "lt"),[],pure_e);]));
     (">",
      Overload(Base((["a",{k=K_Typ}],{t= Tfn ({t=Ttup([{t=Tvar "a"};{t=Tvar "a"}])},bit_t,pure_e)}),External (Some "gt"),[],pure_e),
+	      false,
      [Base(([("n",{k=K_Nat});("m",{k=K_Nat});("o",{k=K_Nat});("p",{k=K_Nat})],
 	    {t = Tfn({t=Ttup([mk_range (mk_nv "n") (mk_nv "m");mk_range (mk_nv "o") (mk_nv "p")])},bit_t,pure_e)}), External (Some "gt_vec"),
 	   [GtEq(Specc(Parse_ast.Int(">",None)),
@@ -1374,7 +1394,7 @@ let rec type_coerce_internal co d_env is_explicit t1 cs1 e t2 cs2 =
 and type_coerce co d_env is_explicit t1 e t2 = type_coerce_internal co d_env is_explicit t1 [] e t2 [];;
 
 let rec conforms_to_t spec actual =
-  (*let _ = Printf.printf "conforms_to_t called with %s, %s\n" (t_to_string spec) (t_to_string actual) in*)
+  let _ = Printf.printf "conforms_to_t called with %s, %s\n" (t_to_string spec) (t_to_string actual) in
   match spec.t,actual.t with
     | Tuvar _,_ -> true
     | Ttup ss, Ttup acs -> (List.length ss = List.length acs) && List.for_all2 conforms_to_t ss acs
@@ -1398,14 +1418,14 @@ and conforms_to_ta spec actual =
     | TA_eft  s, TA_eft  a -> conforms_to_e s a
     | _ -> false
 and conforms_to_n spec actual =
-  (*let _ = Printf.printf "conforms_to_n called with %s, %s\n" (n_to_string spec) (n_to_string actual) in*)
+  let _ = Printf.printf "conforms_to_n called with %s, %s\n" (n_to_string spec) (n_to_string actual) in
   match spec.nexp,actual.nexp with
     | Nuvar _,_ -> true
     | Nconst si,Nconst ai -> eq_big_int si ai
-    | _,_ -> false
+    | _,_ -> true
 and conforms_to_o spec actual =
   match spec.order,actual.order with
-    | Ouvar _,_ | Oinc,Oinc | Odec,Odec -> true
+    | Ouvar _,_ | Oinc,Oinc | Odec,Odec | _, Ouvar _ -> true
     | _,_ -> false
 and conforms_to_e spec actual =
   match spec.effect,actual.effect with
@@ -1413,18 +1433,18 @@ and conforms_to_e spec actual =
     | _,Euvar _ -> false
     | _,_ -> false
 
-let rec select_overload_variant d_env variants actual_type =
+let rec select_overload_variant d_env params_check get_all variants actual_type =
   match variants with
-    | [] -> NoTyp
-    | NoTyp::variants | Overload _::variants -> select_overload_variant d_env variants actual_type
+    | [] -> []
+    | NoTyp::variants | Overload _::variants -> select_overload_variant d_env params_check get_all variants actual_type
     | Base((parms,t),tag,cs,ef)::variants ->
       let t,cs,ef = subst parms t cs ef in
       let t,cs' = get_abbrev d_env t in
       (match t.t with
 	| Tfn(a,r,e) ->
-	  if conforms_to_t a actual_type 
-	  then Base(([],t),tag,cs@cs',ef)
-	  else select_overload_variant d_env variants actual_type
+	  if (if params_check then conforms_to_t a actual_type else conforms_to_t actual_type r)
+	  then (Base(([],t),tag,cs@cs',ef))::(if get_all then (select_overload_variant d_env params_check get_all variants actual_type) else [])
+	  else select_overload_variant d_env params_check get_all variants actual_type
 	| _ -> assert false (*Turn into unreachable error*))      
 
 let rec in_constraint_env = function
diff --git a/src/type_internal.mli b/src/type_internal.mli
index 2aff6db3..7c0c2645 100644
--- a/src/type_internal.mli
+++ b/src/type_internal.mli
@@ -93,7 +93,7 @@ type t_params = (string * kind) list
 type tannot = 
   | NoTyp
   | Base of (t_params * t) * tag * nexp_range list * effect
-  | Overload of tannot * tannot list (* First tannot is the most polymorphic version; the list includes all variants. All t to be Tfn *)
+  | Overload of tannot * bool * tannot list (* First tannot is the most polymorphic version; the list includes all variants. All t to be Tfn *)
 (*type tannot = ((t_params * t) * tag * nexp_range list * effect) option*)
 type 'a emap = 'a Envmap.t
 
@@ -142,7 +142,7 @@ val get_abbrev : def_envs -> t -> (t * nexp_range list)
 val normalize_nexp : nexp -> nexp
 val get_index : nexp -> int (*TEMPORARILY expose nindex through this for debugging purposes*)
 
-val select_overload_variant : def_envs -> tannot list -> t -> tannot
+val select_overload_variant : def_envs -> bool -> bool -> tannot list -> t -> tannot list
 
 (*May raise an exception if a contradiction is found*)
 val resolve_constraints : nexp_range list -> nexp_range list