Refine overloading resolution with respect to vectors and ranges

Fix a few other bugs as well

3 files changed, 89 insertions, 36 deletions

diff --git a/src/test/test3.sail b/src/test/test3.sail
index 98ebb2d6..5e9ba2df 100644
--- a/src/test/test3.sail
+++ b/src/test/test3.sail
@@ -48,7 +48,7 @@ function nat main _ = {
 
   (* extern calls *)
   dummy_reg := 3 + 39;
-  dummy_reg := (deinfix +)(5, 37);
+  (*dummy_reg := (deinfix +)(5, 37);*)
   (* casts and external calls *)
   dummy_reg := 0b01 + 0b01;
   dummy_reg2 := 0b00000001;
diff --git a/src/type_check.ml b/src/type_check.ml
index 005cd70b..7c6ad921 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -667,7 +667,7 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)):
 	(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*)
+          (*let _ = Printf.printf "Selected an overloaded function for %s, variant with function type %s for actual type %s\n" i (t_to_string t) (t_to_string arg_t) in*)
 	  (match t.t with
 	  | Tfn(arg,ret,imp,ef') ->
             (match arg.t,arg_t.t with
@@ -832,10 +832,14 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)):
         | Tabbrev(_,{t=Tapp("vector",[_;_;TA_ord ord;TA_typ t])}) | Tapp("vector",[_;_;TA_ord ord;TA_typ t]) -> ord,t
         | _ -> ord,item_t in
       let cs_loc = 
-	match ord.order with
-	  | Oinc ->
+	match (ord.order,d_env.default_o.order) with
+	  | (Oinc,_) ->
+	    [LtEq((Expr l),base,min); LtEq((Expr l),{nexp=Nadd(min,m_rise)},{nexp=Nadd(base,rise)})] 
+	  | (Odec,_) -> 
+	    [GtEq((Expr l),base,min); LtEq((Expr l),{nexp=Nadd(min,m_rise)},{nexp=Nadd(base,{nexp=Nneg rise})})]
+	  | (_,Oinc) -> 
 	    [LtEq((Expr l),base,min); LtEq((Expr l),{nexp=Nadd(min,m_rise)},{nexp=Nadd(base,rise)})] 
-	  | Odec -> 
+	  | (_,Odec) ->
 	    [GtEq((Expr l),base,min); LtEq((Expr l),{nexp=Nadd(min,m_rise)},{nexp=Nadd(base,{nexp=Nneg rise})})]
 	  | _ -> typ_error l "A vector must be either increasing or decreasing to access a single element"
       in 
@@ -856,13 +860,23 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)):
       let i2t = {t=Tapp("range",[TA_nexp min2;TA_nexp m_rise2])} in
       let (i2', ti2, _,cs_i2,ef_i2) = check_exp envs imp_param i2t i2 in
       let cs_loc =
-	match ord.order with
-	  | Oinc -> 
+	match (ord.order,d_env.default_o.order) with
+	  | (Oinc,_) -> 
 	    [LtEq((Expr l),base,min1); LtEq((Expr l),{nexp=Nadd(min1,m_rise1)},{nexp=Nadd(min2,m_rise2)}); 
 	     LtEq((Expr l),{nexp=Nadd(min2,m_rise2)},{nexp=Nadd(base,rise)});
 	     LtEq((Expr l),min1,base_n); LtEq((Expr l),base_n,{nexp=Nadd(min1,m_rise1)});
 	     LtEq((Expr l),rise_n,{nexp=Nadd(min2,m_rise2)})]
-	  | Odec ->
+	  | (Odec,_) ->
+	    [GtEq((Expr l),base,{nexp=Nadd(min1,m_rise1)}); GtEq((Expr l),{nexp=Nadd(min1,m_rise1)},{nexp=Nadd(min2,m_rise2)});
+	     GtEq((Expr l),{nexp=Nadd(min2,m_rise2)},{nexp=Nadd(base,{nexp=Nneg rise})});
+	     GtEq((Expr l),min1,base_n); GtEq((Expr l),base_n,{nexp=Nadd(min1,m_rise1)});
+	     GtEq((Expr l),rise_n,{nexp=Nadd(min2,m_rise2)})]
+	  | (_,Oinc) ->
+	    [LtEq((Expr l),base,min1); LtEq((Expr l),{nexp=Nadd(min1,m_rise1)},{nexp=Nadd(min2,m_rise2)}); 
+	     LtEq((Expr l),{nexp=Nadd(min2,m_rise2)},{nexp=Nadd(base,rise)});
+	     LtEq((Expr l),min1,base_n); LtEq((Expr l),base_n,{nexp=Nadd(min1,m_rise1)});
+	     LtEq((Expr l),rise_n,{nexp=Nadd(min2,m_rise2)})]
+	  | (_,Odec) -> 
 	    [GtEq((Expr l),base,{nexp=Nadd(min1,m_rise1)}); GtEq((Expr l),{nexp=Nadd(min1,m_rise1)},{nexp=Nadd(min2,m_rise2)});
 	     GtEq((Expr l),{nexp=Nadd(min2,m_rise2)},{nexp=Nadd(base,{nexp=Nneg rise})});
 	     GtEq((Expr l),min1,base_n); GtEq((Expr l),base_n,{nexp=Nadd(min1,m_rise1)});
@@ -884,10 +898,14 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)):
       let (i', ti, _,cs_i,ef_i) = check_exp envs imp_param it i in
       let (e', te, _,cs_e,ef_e) = check_exp envs imp_param item_t e in
       let cs_loc = 
-	match ord.order with
-	  | Oinc ->
+	match (ord.order,d_env.default_o.order) with
+	  | (Oinc,_) ->
 	    [LtEq((Expr l),base,min); LtEq((Expr l),{nexp=Nadd(min,m_rise)},{nexp=Nadd(base,rise)})] 
-	  | Odec -> 
+	  | (Odec,_) -> 
+	    [GtEq((Expr l),base,min); LtEq((Expr l),{nexp=Nadd(min,m_rise)},{nexp=Nadd(base,{nexp=Nneg rise})})]
+	  | (_,Oinc) ->
+	    [LtEq((Expr l),base,min); LtEq((Expr l),{nexp=Nadd(min,m_rise)},{nexp=Nadd(base,rise)})]
+	  | (_,Odec) -> 
 	    [GtEq((Expr l),base,min); LtEq((Expr l),{nexp=Nadd(min,m_rise)},{nexp=Nadd(base,{nexp=Nneg rise})})]
 	  | _ -> typ_error l "A vector must be either increasing or decreasing to change a single element"
       in      
@@ -917,11 +935,17 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)):
 	    let cs_add = [Eq((Expr l),base_e,min1);LtEq((Expr l),rise,m_rise2)] in
 	    (e',ti',env_e,cs_e@cs_add,ef_e) in	     
       let cs_loc =
-	match ord.order with
-	  | Oinc -> 
+	match (ord.order,d_env.default_o.order) with
+	  | (Oinc,_) -> 
 	    [LtEq((Expr l),base,min1); LtEq((Expr l),{nexp=Nadd(min1,m_rise1)},{nexp=Nadd(min2,m_rise2)}); 
 	     LtEq((Expr l),{nexp=Nadd(min2,m_rise2)},{nexp=Nadd(base,rise)});]
-	  | Odec ->
+	  | (Odec,_) ->
+	    [GtEq((Expr l),base,{nexp=Nadd(min1,m_rise1)}); GtEq((Expr l),{nexp=Nadd(min1,m_rise1)},{nexp=Nadd(min2,m_rise2)});
+	     GtEq((Expr l),{nexp=Nadd(min2,m_rise2)},{nexp=Nadd(base,{nexp=Nneg rise})});]
+	  | (_,Oinc) -> 
+	    [LtEq((Expr l),base,min1); LtEq((Expr l),{nexp=Nadd(min1,m_rise1)},{nexp=Nadd(min2,m_rise2)}); 
+	     LtEq((Expr l),{nexp=Nadd(min2,m_rise2)},{nexp=Nadd(base,rise)});]
+	  | (_,Odec) -> 	    
 	    [GtEq((Expr l),base,{nexp=Nadd(min1,m_rise1)}); GtEq((Expr l),{nexp=Nadd(min1,m_rise1)},{nexp=Nadd(min2,m_rise2)});
 	     GtEq((Expr l),{nexp=Nadd(min2,m_rise2)},{nexp=Nadd(base,{nexp=Nneg rise})});]
 	  | _ -> typ_error l "A vector must be either increasing or decreasing to modify a slice" in
@@ -1197,6 +1221,15 @@ and check_lexp envs imp_param is_top (LEXP_aux(lexp,(l,annot))) : (tannot lexp *
 	      (LEXP_aux(lexp,(l,(Base(([],t),Emp_local,cs@cs',pure_e)))),u,Envmap.empty,Emp_local,[],pure_e)
 	    | Tapp("vector",_),false ->
 	      (LEXP_aux(lexp,(l,(Base(([],t),tag,cs@cs',pure_e)))),t,Envmap.empty,Emp_local,[],pure_e)
+	    | (Tfn _ ,_) ->
+	      (match tag with 
+		| External _ | Spec _ | Emp_global -> 
+		  let u = new_t() in
+		  let t = {t = Tapp("reg",[TA_typ u])} in
+		  let tannot = (Base(([],t),Emp_local,[],pure_e)) in
+		  (LEXP_aux(lexp,(l,tannot)),u,Envmap.from_list [i,tannot],Emp_local,[],pure_e)
+		| _ -> 
+		  typ_error l ("Can only assign to identifiers with type register or reg, found identifier " ^ i ^ " with type " ^ t_to_string t)) 
 	    | _,_ -> 
 	      if is_top
 	      then typ_error l 
@@ -1282,6 +1315,15 @@ and check_lexp envs imp_param is_top (LEXP_aux(lexp,(l,annot))) : (tannot lexp *
 	      let u' = {t=Tapp("reg",[TA_typ ty])} in
 	      t.t <- u'.t;
 	      (LEXP_aux(lexp,(l,(Base((([],u'),Emp_local,cs,pure_e))))),ty,Envmap.empty,Emp_local,[],pure_e)
+	    | (Tfn _ ,_) ->
+	      (match tag with 
+		| External _ | Spec _ | Emp_global -> 
+		  let u = new_t() in
+		  let t = {t = Tapp("reg",[TA_typ u])} in
+		  let tannot = (Base(([],t),Emp_local,[],pure_e)) in
+		  (LEXP_aux(lexp,(l,tannot)),u,Envmap.from_list [i,tannot],Emp_local,[],pure_e)
+		| _ -> 
+		  typ_error l ("Can only assign to identifiers with type register or reg, found identifier " ^ i ^ " with type " ^ t_to_string t)) 
 	    | _,_ -> 
 	      if is_top
 	      then typ_error l 
diff --git a/src/type_internal.ml b/src/type_internal.ml
index 63cb5fd0..17728dd9 100644
--- a/src/type_internal.ml
+++ b/src/type_internal.ml
@@ -818,7 +818,7 @@ let mk_vector typ order start size = {t=Tapp("vector",[TA_nexp {nexp=start}; TA_
 let mk_bitwise_op name symb arity =
   let ovar = Ovar "o"  in
   let vec_typ = mk_vector bit_t ovar (Nvar "n") (Nvar "m") in
-  let single_bit_vec_typ = mk_vector bit_t ovar (Nvar "n") (Nconst zero) in
+  let single_bit_vec_typ = mk_vector bit_t ovar (Nvar "n") (Nconst one) in
   let vec_args = Array.to_list (Array.make arity vec_typ) in
   let single_bit_vec_args = Array.to_list (Array.make arity single_bit_vec_typ) in
   let bit_args = Array.to_list (Array.make arity bit_t) in
@@ -1344,37 +1344,46 @@ let nexp_eq n1 n2 =
   b
 
 
-let rec conforms_to_t d_env loosely spec actual =
+let rec conforms_to_t d_env loosely within_coercion spec actual =
 (*let _ = Printf.printf "conforms_to_t called, evaluated loosely? %b, with %s and %s\n" loosely (t_to_string spec) (t_to_string actual) in*)
   let spec,_ = get_abbrev d_env spec in
   let actual,_ = get_abbrev d_env actual in
   match (spec.t,actual.t,loosely) with
     | (Tuvar _,_,true) -> true
-    | (Ttup ss, Ttup acs,_) -> (List.length ss = List.length acs) && List.for_all2 (conforms_to_t d_env loosely) ss acs
+    | (Ttup ss, Ttup acs,_) -> 
+      (List.length ss = List.length acs) && List.for_all2 (conforms_to_t d_env loosely within_coercion) ss acs
     | (Tid is, Tid ia,_) -> is = ia
     | (Tapp(is,tas), Tapp("register",[TA_typ t]),true) ->
       if is = "register" && (List.length tas) = 1
-      then List.for_all2 (conforms_to_ta d_env loosely) tas [TA_typ t]
-      else conforms_to_t d_env loosely spec t
+      then List.for_all2 (conforms_to_ta d_env loosely within_coercion) tas [TA_typ t]
+      else conforms_to_t d_env loosely within_coercion spec t
+    | (Tapp("vector",[TA_nexp bs;TA_nexp rs;TA_ord os;TA_typ ts]),
+       Tapp("vector",[TA_nexp ba;TA_nexp ra;TA_ord oa;TA_typ ta]),_) ->
+      conforms_to_t d_env loosely within_coercion ts ta
+      && conforms_to_o loosely os oa
+      && conforms_to_n false within_coercion eq_big_int rs ra
+    | (Tapp("range",[TA_nexp bs;TA_nexp rs]),Tapp("range",[TA_nexp ba;TA_nexp ra]),_) ->
+      conforms_to_n true within_coercion le_big_int bs ba && conforms_to_n true within_coercion ge_big_int rs ra 
     | (Tapp(is,tas), Tapp(ia, taa),_) -> 
 (*      let _ = Printf.printf "conforms to given two apps: %b, %b\n" (is = ia) (List.length tas = List.length taa) in*)
-      (is = ia) && (List.length tas = List.length taa) && (List.for_all2 (conforms_to_ta d_env loosely) tas taa)
-    | (Tabbrev(_,s),a,_) -> conforms_to_t d_env loosely s actual
-    | (s,Tabbrev(_,a),_) -> conforms_to_t d_env loosely spec a
+      (is = ia) && (List.length tas = List.length taa) && (List.for_all2 (conforms_to_ta d_env loosely within_coercion) tas taa)
+    | (Tabbrev(_,s),a,_) -> conforms_to_t d_env loosely within_coercion s actual
+    | (s,Tabbrev(_,a),_) -> conforms_to_t d_env loosely within_coercion spec a
     | (_,_,_) -> false
-and conforms_to_ta d_env loosely spec actual =
+and conforms_to_ta d_env loosely within_coercion spec actual =
 (*let _ = Printf.printf "conforms_to_ta called, evaluated loosely? %b, with %s and %s\n" loosely (targ_to_string spec) (targ_to_string actual) in*)
   match spec,actual with
-    | TA_typ  s, TA_typ  a -> conforms_to_t d_env loosely s a
-    | TA_nexp s, TA_nexp a -> conforms_to_n loosely s a
+    | TA_typ  s, TA_typ  a -> conforms_to_t d_env loosely within_coercion s a
+    | TA_nexp s, TA_nexp a -> conforms_to_n loosely within_coercion eq_big_int s a
     | TA_ord  s, TA_ord  a -> conforms_to_o loosely s a
     | TA_eft  s, TA_eft  a -> conforms_to_e loosely s a
     | _ -> false
-and conforms_to_n loosely spec actual =
-(*let _ = Printf.printf "conforms_to_n called, evaluated loosely? %b, with %s and %s\n" loosely (n_to_string spec) (n_to_string actual) in*)
-  match (spec.nexp,actual.nexp,loosely) with
-    | (Nuvar _,_,true) -> true
-    | (Nconst si,Nconst ai,_) -> eq_big_int si ai
+and conforms_to_n loosely within_coercion op spec actual =
+(*  let _ = Printf.printf "conforms_to_n called, evaluated loosely? %b, with coercion? %b with %s and %s\n" 
+    loosely within_coercion (n_to_string spec) (n_to_string actual) in*)
+  match (spec.nexp,actual.nexp,loosely,within_coercion) with
+    | (Nconst si,Nconst ai,_,_) -> op si ai
+    | (Nconst _,Nuvar _,false,false) -> false
     | _ -> true
 and conforms_to_o loosely spec actual =
   match (spec.order,actual.order,loosely) with
@@ -1455,13 +1464,13 @@ let rec type_coerce_internal co d_env is_explicit t1 cs1 e t2 cs2 =
   | Tabbrev(_,t1),_ -> type_coerce_internal co d_env is_explicit t1 cs1 e t2 cs2
   | _,Tabbrev(_,t2) -> type_coerce_internal co d_env is_explicit t1 cs1 e t2 cs2
   | Toptions(to1,Some to2),_ -> 
-    if (conforms_to_t d_env false to1 t2 || conforms_to_t d_env false to2 t2)
+    if (conforms_to_t d_env false true to1 t2 || conforms_to_t d_env false true to2 t2)
     then begin t1.t <- t2.t; (t2,csp,pure_e,e) end
     else eq_error l ("Neither " ^ (t_to_string to1) ^
 		     " nor " ^ (t_to_string to2) ^ " can match expected type " ^ (t_to_string t2))
   | Toptions(to1,None),_ -> (t2,csp,pure_e,e)
   | _,Toptions(to1,Some to2) -> 
-    if (conforms_to_t d_env false to1 t1 || conforms_to_t d_env false to2 t1)
+    if (conforms_to_t d_env false true to1 t1 || conforms_to_t d_env false true to2 t1)
     then begin t2.t <- t1.t; (t1,csp,pure_e,e) end
     else eq_error l ((t_to_string t1) ^ " can match neither expexted type " ^ (t_to_string to1) ^ " nor " ^ (t_to_string to2))
   | _,Toptions(to1,None) -> (t1,csp,pure_e,e)
@@ -1617,12 +1626,14 @@ let rec select_overload_variant d_env params_check get_all variants actual_type
       let recur _ = select_overload_variant d_env params_check get_all variants actual_type in
       (match t.t with
 	| Tfn(a,r,_,e) ->
+	  (*let _ = Printf.printf "About to check a variant\n" in*)
 	  let is_matching = 
-	    if params_check then conforms_to_t d_env true a actual_type 
+	    if params_check then conforms_to_t d_env true false a actual_type 
 	    else match actual_type.t with
-	      | Toptions(at1,Some at2) -> (conforms_to_t d_env false at1 r || conforms_to_t d_env false at2 r)
-	      | Toptions(at1,None) -> conforms_to_t d_env false at1 r
-	      | _ -> conforms_to_t d_env true actual_type r in
+	      | Toptions(at1,Some at2) -> (conforms_to_t d_env false true at1 r || conforms_to_t d_env false true at2 r)
+	      | Toptions(at1,None) -> conforms_to_t d_env false true at1 r
+	      | _ -> conforms_to_t d_env true true actual_type r in
+	  (*let _ = Printf.printf "Checked a variant, matching? %b\n" is_matching in*)
 	  if is_matching 
 	  then (Base(([],t),tag,cs@cs',ef))::(if get_all then (recur ()) else [])
 	  else recur ()