Make hex constants work; improve utility of casts for selecting overloaded functions

6 files changed, 121 insertions, 67 deletions

diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem
index ab4aa7ff..7ae5caff 100644
--- a/src/lem_interp/interp.lem
+++ b/src/lem_interp/interp.lem
@@ -240,17 +240,43 @@ let is_lit_vector (L_aux l _) =
   | _ -> false
 end
 
+(*Both make an endian assumption, and should use a flag to switch*)
 val litV_to_vec : lit -> value
 let litV_to_vec (L_aux lit l) =
   match lit with
   | L_hex s ->
-    let hexes = String.toCharList s in
-    (* XXX unimplemented *)
-    V_vector 0 true []
+    let to_v b = V_lit (L_aux b l) in
+    let hexes = List.map to_v 
+                 (List.concat 
+		    (List.map 
+		       (fun s -> match s with
+			 | #'0' -> [L_zero;L_zero;L_zero;L_zero]
+			 | #'1' -> [L_zero;L_zero;L_zero;L_one ]
+			 | #'2' -> [L_zero;L_zero;L_one ;L_zero]
+			 | #'3' -> [L_zero;L_zero;L_one ;L_one ]
+			 | #'4' -> [L_zero;L_one ;L_zero;L_zero]
+			 | #'5' -> [L_zero;L_one ;L_zero;L_one ]
+			 | #'6' -> [L_zero;L_one ;L_one ;L_zero]
+			 | #'7' -> [L_zero;L_one ;L_one ;L_one ]
+			 | #'8' -> [L_one ;L_zero;L_zero;L_zero]
+			 | #'9' -> [L_one ;L_zero;L_zero;L_one ]
+			 | #'A' -> [L_one ;L_zero;L_one ;L_zero]
+			 | #'B' -> [L_one ;L_zero;L_one ;L_one ]
+			 | #'C' -> [L_one ;L_one ;L_zero;L_zero]
+			 | #'D' -> [L_one ;L_one ;L_zero;L_one ]
+			 | #'E' -> [L_one ;L_one ;L_one ;L_zero]
+			 | #'F' -> [L_one ;L_one ;L_one ;L_one ]
+			 | #'a' -> [L_one ;L_zero;L_one ;L_zero]
+			 | #'b' -> [L_one ;L_zero;L_one ;L_one ]
+			 | #'c' -> [L_one ;L_one ;L_zero;L_zero]
+			 | #'d' -> [L_one ;L_one ;L_zero;L_one ]
+			 | #'e' -> [L_one ;L_one ;L_one ;L_zero]
+			 | #'f' -> [L_one ;L_one ;L_one ;L_one ] end)
+		       (String.toCharList s))) in
+    (* XXX assumes endianness *)
+    V_vector 0 true hexes
   | L_bin s -> 
-    let bits = String.toCharList s in
-    let exploded_bits = bits in (*List.map (fun c -> String.toString [c]) bits in*)
-    let bits = List.map (fun s -> match s with | #'0' -> (V_lit (L_aux L_zero l)) | #'1' -> (V_lit (L_aux L_one l)) end) exploded_bits in
+    let bits = List.map (fun s -> match s with | #'0' -> (V_lit (L_aux L_zero l)) | #'1' -> (V_lit (L_aux L_one l)) end) (String.toCharList s) in
     (* XXX assume binary constants are written in big-endian,
      * we might need syntax to change this assumption. *)
     V_vector 0 true bits
diff --git a/src/test/test1.sail b/src/test/test1.sail
index 64722089..18863ce2 100644
--- a/src/test/test1.sail
+++ b/src/test/test1.sail
@@ -14,6 +14,8 @@ val forall Nat 'a, Nat 'b. bit['a:'b] sliced
 let bit v = bitzero
 let ( bit [ 32 ] ) v1 = 0b101
 
+let ( bit [32] ) v2 = 0xABCDEF01
+
 val forall Type 'a. 'a -> 'a effect pure identity
 function forall Type 'a. 'a identity i = i
 
@@ -39,5 +41,5 @@ function unit a (bit) b = if identity(b) then (identity()) else ()
 
 function bit sw s = switch s { case 0 -> bitzero }
 
-function bit main _ = {ignore(sw(0)); v1[0] }
+function bit main _ = {ignore(sw(0)); ignore((nat) v2); v1[0] }
 
diff --git a/src/test/test2.sail b/src/test/test2.sail
index b4a2dd32..0add0c94 100644
--- a/src/test/test2.sail
+++ b/src/test/test2.sail
@@ -2,7 +2,7 @@ function nat id ( n ) = n
 
 function unit f() = {
  (if( true ) then 
-   a := 3
+   a := (nat) (3 + 0b01) mod 4
   else 
    a := 4
  );
diff --git a/src/type_check.ml b/src/type_check.ml
index 1ef44a75..d7c3787d 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -440,11 +440,12 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp
       let t',cs',e' = type_coerce (Expr l) d_env false (get_e_typ e) e expect_t in
       (e',t',t_env,cs@cs',effect)
     | E_cast(typ,e) ->
-      let t = typ_to_t typ in
-      let (e',u,t_env,cs,ef) = check_exp envs (new_t ()) e in
-      let t',cs2,e' = type_coerce (Expr l) d_env true u e' t in
-      let t',cs3,e'' = type_coerce (Expr l) d_env false t e' expect_t in 
-      (e'',t',t_env,cs@cs2@cs3,ef)        
+      let cast_t = typ_to_t typ in
+      let cast_t,cs_a = get_abbrev d_env cast_t in
+      let (e',u,t_env,cs,ef) = check_exp envs cast_t e in
+(*      let t',cs2,e' = type_coerce (Expr l) d_env true u e' cast_t in*)
+      let t',cs3,e'' = type_coerce (Expr l) d_env false cast_t e' expect_t in 
+      (e'',t',t_env,cs_a@cs@cs3,ef)
     | E_app(id,parms) -> 
       let i = id_to_string id in
       (match Envmap.apply t_env i with
diff --git a/src/type_internal.ml b/src/type_internal.ml
index e95f564e..2c7d66a9 100644
--- a/src/type_internal.ml
+++ b/src/type_internal.ml
@@ -32,6 +32,7 @@ and t_aux =
   | Ttup of t list
   | Tapp of string * t_arg list
   | Tabbrev of t * t
+  | Toptions of t * t
   | Tuvar of t_uvar
 and t_uvar = { index : int; mutable subst : t option }
 and nexp = { mutable nexp : nexp_aux }
@@ -125,6 +126,8 @@ let rec string_of_list sep string_of = function
   | [x] -> string_of x
   | x::ls -> (string_of x) ^ sep ^ (string_of_list sep string_of ls)
 
+let debug_mode = ref true;;
+
 let rec t_to_string t = 
   match t.t with
     | Tid i -> i
@@ -133,7 +136,9 @@ let rec t_to_string t =
     | Ttup(tups) -> "(" ^ string_of_list ", " t_to_string tups ^ ")"
     | Tapp(i,args) -> i ^ "<" ^  string_of_list ", " targ_to_string args ^ ">"
     | Tabbrev(ti,ta) -> (t_to_string ti) ^ " : " ^ (t_to_string ta)
-    | Tuvar({index = i;subst = a}) -> "Tu_" ^ string_of_int i ^ "("^ (match a with | None -> "None" | Some t -> t_to_string t) ^")"
+    | Toptions(t1,t2) -> if !debug_mode then ("(either "^ (t_to_string t1) ^ " or " ^ (t_to_string t2) ^ ")") else "_"
+    | Tuvar({index = i;subst = a}) -> 
+      if !debug_mode then "Tu_" ^ string_of_int i ^ "("^ (match a with | None -> "None" | Some t -> t_to_string t) ^")" else "_"
 and targ_to_string = function
   | TA_typ t -> t_to_string t
   | TA_nexp n -> n_to_string n
@@ -151,18 +156,18 @@ and n_to_string n =
     | N2n(n,Some i) -> "2**" ^ (n_to_string n) ^ "(*" ^ (string_of_big_int i) ^ "*)"
     | Npow(n, i) -> "(" ^ (n_to_string n) ^ ")**" ^ (string_of_int i)
     | Nneg n -> "-" ^ (n_to_string n)
-    | Nuvar({nindex=i;nsubst=a}) -> "Nu_" ^ string_of_int i ^ "()"
+    | Nuvar({nindex=i;nsubst=a}) -> if !debug_mode then "Nu_" ^ string_of_int i ^ "()" else "_"
 and e_to_string e = 
   match e.effect with
   | Evar i -> "'" ^ i
   | Eset es -> if []=es then "pure" else "{" ^ "effects not printing" ^"}"
-  | Euvar({eindex=i;esubst=a}) -> string_of_int i ^ "()"
+  | Euvar({eindex=i;esubst=a}) -> if !debug_mode then string_of_int i ^ "()" else "_"
 and o_to_string o = 
   match o.order with
   | Ovar i -> "'" ^ i
   | Oinc -> "inc"
   | Odec -> "dec"
-  | Ouvar({oindex=i;osubst=a}) -> string_of_int i ^ "()"
+  | Ouvar({oindex=i;osubst=a}) -> if !debug_mode then string_of_int i ^ "()" else "_"
 
 let tag_to_string = function
   | Emp_local -> "Emp_local"
@@ -411,6 +416,7 @@ let rec normalize_nexp n =
 	| 0  -> {nexp = Npow(n1,(i1+i2))}
 	| -1 -> {nexp = Nmult(n2',n1')}
 	| _  -> {nexp = Nmult(n1',n2')})
+(*TODO Check and see if the constant should be pushed in, in some of these cases (in others it always should) *)
     | Nconst _, Nadd(n21,n22) | Nvar _,Nadd(n21,n22) | Nuvar _,Nadd(n21,n22) | N2n _, Nadd(n21,n22) | Npow _,Nadd(n21,n22) | Nmult _, Nadd(n21,n22) ->
       normalize_nexp {nexp = Nadd( {nexp = Nmult(n1',n21)}, {nexp = Nmult(n1',n21)})}
     | Nadd(n11,n12),Nconst _ | Nadd(n11,n12),Nvar _ | Nadd(n11,n12), Nuvar _ | Nadd(n11,n12), N2n _ | Nadd(n11,n12),Npow _ | Nadd(n11,n12), Nmult _->
@@ -553,6 +559,7 @@ let rec occurs_check_t (t_box : t) (t : t) : unit =
       List.iter (occurs_check_t t_box) ts
     | Tapp(_,targs) -> List.iter (occurs_check_ta (TA_typ t_box)) targs
     | Tabbrev(t,ta) -> occurs_check_t t_box t; occurs_check_t t_box ta
+    | Toptions(t1,t2) -> occurs_check_t t_box t1; occurs_check_t t_box t2
     | _ -> ()
 and occurs_check_ta (ta_box : t_arg) (ta : t_arg) : unit =
   match ta_box,ta with
@@ -974,6 +981,7 @@ let rec t_subst s_env t =
   | Ttup(ts) -> { t= Ttup(List.map (t_subst s_env) ts) }
   | Tapp(i,args) -> {t= Tapp(i,List.map (ta_subst s_env) args)}
   | Tabbrev(ti,ta) -> {t = Tabbrev(t_subst s_env ti,t_subst s_env ta) }
+  | Toptions(t1,t2) -> {t = Toptions(t_subst s_env t1,t_subst s_env t2) }
 and ta_subst s_env ta =
   match ta with
   | TA_typ t -> TA_typ (t_subst s_env t)
@@ -1045,6 +1053,7 @@ let rec t_remove_unifications s_env t =
   | Ttup(ts) -> List.fold_right (fun t s_env -> t_remove_unifications s_env t) ts s_env
   | Tapp(i,args) -> List.fold_right (fun t s_env -> ta_remove_unifications s_env t) args s_env
   | Tabbrev(ti,ta) -> (t_remove_unifications (t_remove_unifications s_env ti) ta)
+  | Toptions(t1,t2) -> assert false (*This should really be removed by this point*)
 and ta_remove_unifications s_env ta =
   match ta with
   | TA_typ t -> (t_remove_unifications s_env t)
@@ -1106,7 +1115,7 @@ let rec t_to_typ t =
     | Ttup ts -> Typ_aux(Typ_tup(List.map t_to_typ ts),Parse_ast.Unknown)
     | Tapp(i,args) -> Typ_aux(Typ_app(Id_aux((Id i), Parse_ast.Unknown),List.map targ_to_typ_arg args),Parse_ast.Unknown)
     | Tabbrev(t,_) -> t_to_typ t
-    | Tuvar _ -> Typ_aux(Typ_var (Kid_aux((Var "fresh"),Parse_ast.Unknown)),Parse_ast.Unknown)
+    | Tuvar _ | Toptions _ -> Typ_aux(Typ_var (Kid_aux((Var "fresh"),Parse_ast.Unknown)),Parse_ast.Unknown)
 and targ_to_typ_arg targ = 
  Typ_arg_aux( 
   (match targ with
@@ -1232,6 +1241,47 @@ let nexp_eq n1 n2 =
   (*let _ = Printf.printf "compared nexps %s\n" (string_of_bool b) in*)
   b
 
+
+let rec conforms_to_t loosely 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*)
+  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 loosely) ss acs
+    | (Tid is, Tid ia,_) -> is = ia
+    | (Tapp(is,tas), Tapp("register",[TA_typ t]),true) ->
+      if is = "register"
+      then List.for_all2 (conforms_to_ta loosely) tas [TA_typ t]
+      else conforms_to_t loosely spec t
+    | (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 loosely) tas taa)
+    | (Tabbrev(_,s),a,_) -> conforms_to_t loosely s actual
+    | (s,Tabbrev(_,a),_) -> conforms_to_t loosely spec a
+    | (_,_,_) -> false
+and conforms_to_ta loosely 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 loosely s a
+    | TA_nexp s, TA_nexp a -> conforms_to_n loosely 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
+    | _ -> true
+and conforms_to_o loosely spec actual =
+  match (spec.order,actual.order,loosely) with
+    | (Ouvar _,_,true) | (Oinc,Oinc,_) | (Odec,Odec,_) | (_, Ouvar _,true) -> true
+    | _ -> false
+and conforms_to_e loosely spec actual =
+  match (spec.effect,actual.effect,loosely) with
+    | (Euvar _,_,true) -> true
+    | (_,Euvar _,true) -> false
+    | (_,_,true)       -> false (*Should check actual effect equality, using existing function*)
+
 (*Is checking for structural equality amongst the types, building constraints for kind Nat. 
   When considering two range type applications, will check for consistency instead of equality*)
 let rec type_consistent_internal co d_env t1 cs1 t2 cs2 = 
@@ -1300,6 +1350,14 @@ let rec type_coerce_internal co d_env is_explicit t1 cs1 e t2 cs2 =
   | Tabbrev(_,t1),Tabbrev(_,t2) -> 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,to2),_ -> 
+    if (conforms_to_t false to1 t2 || conforms_to_t false to2 t2)
+    then begin t1.t <- t2.t; (t2,csp,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,to2) -> 
+    if (conforms_to_t false to1 t1 || conforms_to_t false to2 t1)
+    then begin t2.t <- t1.t; (t1,csp,e) end
+    else eq_error l ((t_to_string t1) ^ " can match neither expexted type " ^ (t_to_string to1) ^ " nor " ^ (t_to_string to2))
   | Ttup t1s, Ttup t2s ->
     let tl1,tl2 = List.length t1s,List.length t2s in
     if tl1=tl2 then 
@@ -1433,46 +1491,6 @@ 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*)
-  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
-    | Tid is, Tid ia -> is = ia
-    | Tapp(is,tas), Tapp("register",[TA_typ t]) ->
-      if is = "register"
-      then List.for_all2 conforms_to_ta tas [TA_typ t]
-      else conforms_to_t spec t
-    | 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 tas taa)
-    | Tabbrev(_,s),a -> conforms_to_t s actual
-    | s,Tabbrev(_,a) -> conforms_to_t spec a
-    | _,_ -> false
-and conforms_to_ta spec actual =
-  (*let _ = Printf.printf "conforms_to_ta called with %s, %s\n" (targ_to_string spec) (targ_to_string actual) in*)
-  match spec,actual with
-    | TA_typ  s, TA_typ  a -> conforms_to_t s a
-    | TA_nexp s, TA_nexp a -> conforms_to_n s a
-    | TA_ord  s, TA_ord  a -> conforms_to_o s a
-    | 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*)
-  match spec.nexp,actual.nexp with
-    | Nuvar _,_ -> true
-    | Nconst si,Nconst ai -> eq_big_int si ai
-    | _,_ -> true
-and conforms_to_o spec actual =
-  match spec.order,actual.order with
-    | Ouvar _,_ | Oinc,Oinc | Odec,Odec | _, Ouvar _ -> true
-    | _,_ -> false
-and conforms_to_e spec actual =
-  match spec.effect,actual.effect with
-    | Euvar _,_ -> true
-    | _,Euvar _ -> false
-    | _,_ -> false
-
 let rec select_overload_variant d_env params_check get_all variants actual_type =
   match variants with
     | [] -> []
@@ -1480,12 +1498,18 @@ let rec 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
+      let recur _ = select_overload_variant d_env params_check get_all variants actual_type in
       (match t.t with
 	| Tfn(a,r,e) ->
-	  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 is_matching = 
+	    if params_check then conforms_to_t true a actual_type 
+	    else match actual_type.t with
+	      | Toptions(at1,at2) -> (conforms_to_t false at1 r || conforms_to_t false at2 r)
+	      | _ -> conforms_to_t true actual_type r in
+	  if is_matching 
+	  then (Base(([],t),tag,cs@cs',ef))::(if get_all then (recur ()) else [])
+	  else recur ()
+	| _ -> recur () )
 
 let rec in_constraint_env = function
   | [] -> []
diff --git a/src/type_internal.mli b/src/type_internal.mli
index 7c0c2645..a228750f 100644
--- a/src/type_internal.mli
+++ b/src/type_internal.mli
@@ -26,12 +26,13 @@ type e_uvar
 type o_uvar
 type t = { mutable t : t_aux }
 and t_aux =
-  | Tvar of string
-  | Tid of string
-  | Tfn of t * t * effect
-  | Ttup of t list
-  | Tapp of string * t_arg list
+  | Tvar of string (* concrete *)
+  | Tid of string  (* concrete *)
+  | Tfn of t * t * effect (* concrete: neither t can ever be fn *)
+  | Ttup of t list (* concrete: no t can be fn *)
+  | Tapp of string * t_arg list (* concrete *)
   | Tabbrev of t * t (* first t is the specified type, which may itself be an abbrev; second is the ground type, never an abbrev *)
+  | Toptions of t * t (* used in overload or cast to specify a set of types to expect; first is always concrete. Should never appear after type checking *)
   | Tuvar of t_uvar
 and nexp = { mutable nexp : nexp_aux }
 and nexp_aux =