More type checking and conversions

(Temporarily turning off unbound identifier checks, until all variable-introducing forms are checked)

4 files changed, 59 insertions, 22 deletions

diff --git a/src/finite_map.ml b/src/finite_map.ml
index 3058e0c9..fd0a5553 100644
--- a/src/finite_map.ml
+++ b/src/finite_map.ml
@@ -93,7 +93,11 @@ module Fmap_map(Key : Set.OrderedType) : Fmap
   let insert m (k,v) = M.add k v m
   let union m1 m2 = 
     M.merge (fun k v1 v2 -> match v2 with | None -> v1 | Some _ -> v2) m1 m2
-  let intersect m1 m2 = m2 (*WRITE ME TODO*)
+  let intersect m1 m2 = 
+    M.fold (fun k v res -> 
+      if (M.mem k m2)
+      then M.add k v res
+      else res) M.empty m1
   let merge f m1 m2 = M.merge f m1 m2
   let apply m k = 
     try
diff --git a/src/test/test3.sail b/src/test/test3.sail
index 89c710bc..e4844204 100644
--- a/src/test/test3.sail
+++ b/src/test/test3.sail
@@ -16,24 +16,24 @@ function nat main _ = {
   (* left-hand side function call = memory write *)
   MEM(0) := 0;
   (* memory read, thanks to effect { rmem} above *)
-  MEM(0);
+  ignore(MEM(0));
   (* register write, idem *)
   dummy_reg := 1;
   (* register read, thanks to register declaration *)
-  dummy_reg;
+  ignore(dummy_reg);
 
   (* infix call *)
-  7 * 9;
+  ignore(7 * 9);
 
   (* Some more checks *)
   MEM(1) := 2;
-  MEM(1);
+  ignore(MEM(1));
   MEM_GPU(0) := 3;
-  MEM_GPU(0);
+  ignore(MEM_GPU(0));
   MEM_SIZE(0,1) := 4;
-  MEM_SIZE(0,1);
+  ignore(MEM_SIZE(0,1));
 
   (* extern calls *)
-  3 + 39;
+  ignore(3 + 39);
   add(5, 37);
 }
diff --git a/src/type_check.ml b/src/type_check.ml
index 59ee8920..8c4f4a44 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -372,7 +372,7 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp
           let t',cs',e' = type_coerce l t (rebuild (Some((params,t),tag,cs))) expect_t in
           (e',t',t_env,cs@cs')
         )
-      | Some None | None -> typ_error l ("Identifier " ^ (id_to_string id) ^ " is unbound"))
+      | Some None | None -> (* Turned off until lexp is type checked. TURN ME BACK ON:: typ_error l ("Identifier " ^ (id_to_string id) ^ " is unbound")*) (rebuild None,expect_t,t_env,[]))
     | E_lit (L_aux(lit,l')) ->
       let t = (match lit with
         | L_unit  -> {t = Tid "unit"} 
diff --git a/src/type_internal.ml b/src/type_internal.ml
index 693afdcc..4a3aaec0 100644
--- a/src/type_internal.ml
+++ b/src/type_internal.ml
@@ -77,17 +77,23 @@ type tannot = ((t_params * t) * tag * nexp_range list) option
 
 type exp = tannot Ast.exp
 
+let v_count = ref 0
 let t_count = ref 0
 let n_count = ref 0
 let o_count = ref 0
 let e_count = ref 0
 
 let reset_fresh _ = 
-  begin t_count := 0;
+  begin v_count := 0;
+        t_count := 0;
         n_count := 0;
 	o_count := 0;
 	e_count := 0;
   end
+let new_id _ =
+  let i = !v_count in
+  v_count := i+1;
+  (string_of_int i) ^ "v"
 let new_t _ = 
   let i = !t_count in
   t_count := i + 1;
@@ -125,7 +131,10 @@ let nat_typ = {t=Tid "nat"}
 let pure = {effect=Eset []}
 let initial_typ_env =
   Envmap.from_list [
+    ("ignore",Some(([("a",{k=K_Typ})],{t=Tfn ({t=Tvar "a"},unit_t,pure)}),External,[]));
     ("+",Some(([],{t= Tfn ({t=Ttup([nat_typ;nat_typ])},nat_typ,pure)}),External,[]));
+    ("*",Some(([],{t= Tfn ({t=Ttup([nat_typ;nat_typ])},nat_typ,pure)}),External,[]));
+    
   ]
 
 let rec t_subst s_env t =
@@ -240,11 +249,11 @@ let rec nexp_eq n1 n2 =
 
 (*Is checking for structural equality amongst the types, building constraints for kind Nat. 
   When considering two enum type applications, will check for consistency instead of equality
-  Note: needs an environment to handle type abbreviations*)
+  Note: needs an environment to handle type abbreviations, and to lookup in the case either is a Tid or Tapp*)
 let rec type_consistent l t1 t2 = 
   match t1.t,t2.t with
   | Tvar v1,Tvar v2 -> if v1 = v2 then (t2,[]) else eq_error l ("Type variables " ^ v1 ^ " and " ^ v2 ^ " do not match and cannot be unified")
-  | Tid v1,Tid v2 -> if v1 = v2 then (t2,[]) else eq_error l ("Type variables " ^ v1 ^ " and " ^ v2 ^ " do not match and cannot be unified") (*lookup for abbrev*)
+  | Tid v1,Tid v2 -> if v1 = v2 then (t2,[]) else eq_error l ("Types " ^ v1 ^ " and " ^ v2 ^ " do not match") (*lookup for abbrev*)
   | Tfn(tin1,tout1,effect1),Tfn(tin2,tout2,effect2) -> 
     let (tin,cin) = type_consistent l tin1 tin2 in
     let (tout,cout) = type_consistent l tout1 tout2 in
@@ -288,14 +297,38 @@ and type_arg_eq l ta1 ta2 =
 
 
 let rec type_coerce l t1 e t2 = 
-  (t2,[],e)
-  (*match t1.t,t2.t with
-  | Tid v1,Tid v2 -> if v1 = v2 then (None,[]) else eq_error l ("Type variables " ^ v1 ^ " and " ^ v2 ^ " do not match and cannot be unified") (*lookup for abbrev*)
+  match t1.t,t2.t with
   | Ttup t1s, Ttup t2s ->
-    (None,(List.flatten (List.map snd (List.map2 (type_consistent l) t1s t2s))))
-  | Tapp(id1,args1), Tapp(id2,args2) ->
-    if id1=id2 && (List.length args2 = List.length args2) then
-      (None,(List.flatten (List.map2 (type_arg_eq l) args1 args2)))
-    else eq_error l ("Type application of " ^ id1 ^ " and " ^ id2 ^ " must match")
-  | _,_ -> let (t2,consts) = type_consistent l t1 t2 in
-	     (None,consts)*)
+    let tl1,tl2 = List.length t1s,List.length t2s in
+    if tl1=tl2 then 
+      let ids = List.map (fun _ -> Id_aux(Id (new_id ()),l)) t1s in
+      let vars = List.map2 (fun i t -> E_aux(E_id(i),(l,Some(([],t),Emp,[])))) ids t1s in
+      let (coerced_ts,cs,coerced_vars) = 
+        List.fold_right2 (fun v (t1,t2) (ts,cs,es) -> let (t',c',e') = type_coerce l t1 v t2 in
+                                                      ((t'::ts),c'@cs,(e'::es)))
+          vars (List.combine t1s t2s) ([],[],[]) in
+      if vars = coerced_vars then (t2,cs,e)
+      else let e' = E_aux(E_case(e,[(Pat_aux(Pat_exp(P_aux(P_tup (List.map2 (fun i t -> P_aux(P_id i,(l,(Some(([],t),Emp,[]))))) ids t1s),(l,Some(([],t1),Emp,[]))),
+                                               E_aux(E_tuple coerced_vars,(l,Some(([],t2),Emp,cs)))),
+                                             (l,Some(([],t2),Emp,[]))))]),
+                          (l,(Some(([],t2),Emp,[])))) in
+           (t2,cs,e')
+    else eq_error l ("A tuple of length " ^ (string_of_int tl1) ^ " cannot be used where a tuple of length " ^ (string_of_int tl2) ^ " is expected")
+  | Tapp(id1,args1),Tapp(id2,args2) ->
+    if id1=id2 
+    then let t',cs' = type_consistent l t1 t2 in (t',cs',e)
+    else (match id1,id2 with
+    | "vector","enum" -> 
+      (match args1,args2 with
+      | [TA_nexp b1;TA_nexp r1;TA_ord {order = Oinc};TA_typ {t=Tid "bit"}],
+        [TA_nexp b2;TA_nexp r2;TA_ord {order = Oinc}] -> (t2,[],e) (*TODO*)
+      | [TA_nexp b1;TA_nexp r1;TA_ord {order = Odec};TA_typ {t=Tid "bit"}],
+        [TA_nexp b2;TA_nexp r2;TA_ord {order = Odec}] -> (t2,[],e) (*TODO*)
+      | [TA_nexp b1;TA_nexp r1;TA_ord {order = Ovar o};TA_typ {t=Tid "bit"}],_ -> (t2,[],e) (*TODO*)
+      | [TA_nexp b1;TA_nexp r1;TA_ord o;TA_typ t],_ -> 
+        eq_error l "Cannot convert non-bit vector into an enum")
+    | "enum","vector" -> (t2,[],e) (*TODO*)
+    | _,_ -> let t',cs' = type_consistent l t1 t2 in (t',cs',e))
+  | Tapp("enum",args1),Tid(i) -> (t2,[],e) (*Need env*)
+  | Tid(i),Tapp("enum",args1) -> (t2,[],e) (*Need env*)
+  | _,_ -> let t',cs = type_consistent l t1 t2 in (t',cs,e)