Typechecking lets, concrete vectors, and function calls (minus effects)

6 files changed, 121 insertions, 21 deletions

diff --git a/src/parser.mly b/src/parser.mly
index b8b0e43a..5779b3b4 100644
--- a/src/parser.mly
+++ b/src/parser.mly
@@ -92,8 +92,7 @@ let mk_eannotn _ = Effect_opt_aux(Effect_opt_pure,Unknown)
 let mk_namesectn _ = Name_sect_aux(Name_sect_none,Unknown)
 
 let make_enum_sugar_bounded typ1 typ2 =
-  ATyp_app(Id_aux(Id("enum"),Unknown),
-           [typ1; typ2; ATyp_aux(ATyp_inc,Unknown)])
+  ATyp_app(Id_aux(Id("enum"),Unknown),[typ1; typ2;])
 let make_enum_sugar typ1 =
   make_enum_sugar_bounded typ1 (ATyp_aux(ATyp_constant(0), Unknown))
 
@@ -101,7 +100,7 @@ let make_vector_sugar_bounded typ typ1 typ2 =
   ATyp_app(Id_aux(Id("vector"),Unknown),
            [typ1;typ2;ATyp_aux(ATyp_inc,Unknown);typ])
 let make_vector_sugar typ typ1 =
-  make_vector_sugar_bounded typ typ1 (ATyp_aux(ATyp_constant(0),Unknown))
+  make_vector_sugar_bounded typ (ATyp_aux(ATyp_constant(0),Unknown)) typ1
     
 
 let space = " "
diff --git a/src/test/test1.sail b/src/test/test1.sail
index c035ea4b..0cb592d8 100644
--- a/src/test/test1.sail
+++ b/src/test/test1.sail
@@ -31,5 +31,5 @@ end ast
 
 function bit sw s = switch s { case 0 -> bitzero }
 
-function bit main _ = {sw(0); v1[0] }
+function bit main _ = {ignore(sw(0)); v1[0] }
 
diff --git a/src/test/vectors.sail b/src/test/vectors.sail
index 515b2be4..f1fc6199 100644
--- a/src/test/vectors.sail
+++ b/src/test/vectors.sail
@@ -1,4 +1,5 @@
 let (bit[32]) v = 0b101
+let (bit[4]) v2 = [0,1,0,0]
 register (bit[32]) i
 
 register nat match_success
diff --git a/src/type_check.ml b/src/type_check.ml
index 3a8a6389..be195033 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -373,13 +373,14 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp
 	| L_true  -> bool_t,lit
 	| L_false -> bool_t,lit
 	| L_num i -> 
-	  if expect_t = bit_t 
-	  then if i = 0 then bit_t,L_zero
+          (match expect_t.t with
+          | Tid "bit" -> 
+            if i = 0 then bit_t,L_zero
 	    else 
 	      if i = 1 then bit_t,L_one
-	      else typ_error l "Expected bit,found number that cannot be used as a bit"
-	  else {t = Tapp("enum",
-			 [TA_nexp{nexp = Nconst i};TA_nexp{nexp= Nconst 0};])},lit	      
+	      else typ_error l "Expected bit,found a number that cannot be used as a bit"
+          | _ -> {t = Tapp("enum",
+			   [TA_nexp{nexp = Nconst i};TA_nexp{nexp= Nconst 0};])},lit)
 	| L_hex s -> {t = Tapp("vector",
 			       [TA_nexp{nexp = Nconst 0};
 				TA_nexp{nexp = Nconst ((String.length s)*4)};
@@ -398,8 +399,48 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp
       let t',cs = type_consistent l d_env t expect_t in
       let (e',u,t_env,cs') = check_exp envs t' e in
       (e',t',t_env,cs@cs')
-    | E_app(id,parms) -> (E_aux(e,(l,annot)),expect_t,t_env,[]) (*TODO*)
-    | E_app_infix(lft,op,rht) -> (E_aux(e,(l,annot)),expect_t,t_env,[]) (*TODO*)
+    | E_app(id,parms) -> 
+      let i = id_to_string id in
+      (match Envmap.apply t_env i with
+      | Some(Some(tp,Enum,cs)) ->
+        typ_error l ("Expected function with name " ^ i ^ " but found an enumeration identifier")
+      | Some(Some(tp,Default,cs)) ->
+        typ_error l ("Function " ^ i ^ " must be defined, not just declared as a default, before use")
+      | Some(Some((params,t),tag,cs)) ->
+        let t,cs = subst params t cs in
+        (match t.t with
+        | Tfn(arg,ret,ef) ->
+          (match parms with
+          | [] -> 
+            let (p',cs') = type_consistent l d_env unit_t arg in
+            let (ret_t,cs_r,e') = type_coerce l d_env ret (rebuild (Some(([],unit_t),tag,cs@cs'))) expect_t in
+            (e',ret_t,t_env,cs@cs'@cs_r)
+          | [parm] ->
+            let (parm',arg_t,t_env,cs') = check_exp envs arg parm in
+            let (ret_t,cs_r',e') = type_coerce l d_env ret (E_aux(E_app(id,[parm']),(l,(Some(([],ret),tag,cs))))) expect_t in
+            (e',ret_t,t_env,cs@cs'@cs_r')
+          | parms -> 
+            let ((E_aux(E_tuple parms',tannot')),arg_t,t_env,cs') = check_exp envs arg (E_aux(E_tuple parms,(l,None))) in
+            let (ret_t,cs_r',e') = type_coerce l d_env ret (E_aux(E_app(id, parms'),(l,(Some(([],ret),tag,cs))))) expect_t in
+            (e',ret_t,t_env,cs@cs'@cs_r'))
+        | _ -> typ_error l ("Expected a function or constructor, found identifier " ^ i ^ " bound to type " ^ (t_to_string t)))
+      | _ -> typ_error l ("Unbound function " ^ i)) 
+    | E_app_infix(lft,op,rht) -> 
+      let i = id_to_string op in
+      (match Envmap.apply t_env i with
+      | Some(Some(tp,Enum,cs)) ->
+        typ_error l ("Expected function with name " ^ i ^ " but found an enumeration identifier")
+      | Some(Some(tp,Default,cs)) ->
+        typ_error l ("Function " ^ i ^ " must be defined, not just declared as a default, before use")
+      | Some(Some((params,t),tag,cs)) ->
+        let t,cs = subst params t cs in
+        (match t.t with
+        | Tfn(arg,ret,ef) -> 
+          let (E_aux(E_tuple [lft';rht'],tannot'),arg_t,t_env,cs') = check_exp envs arg (E_aux(E_tuple [lft;rht],(l,None))) in
+          let ret_t,cs_r',e' = type_coerce l d_env ret (E_aux(E_app_infix(lft',op,rht'),(l,(Some(([],ret),tag,cs))))) expect_t in
+          (e',ret_t,t_env,cs@cs'@cs_r')
+        | _ -> typ_error l ("Expected a function or constructor, found identifier " ^ i ^ " bound to type " ^ (t_to_string t)))
+      | _ -> typ_error l ("Unbound infix function " ^ i))
     | E_tuple(exps) ->
       (match expect_t.t with
       | Ttup ts ->
@@ -412,17 +453,32 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp
           let t = {t = Ttup typs} in
           (E_aux(E_tuple(exps),(l,Some(([],t),Emp,consts))),t,t_env,consts)
         else typ_error l ("Expected a tuple with length " ^ (string_of_int tl) ^ " found one of length " ^ (string_of_int el))
-      | Tuvar _ ->
+      | _ ->
         let exps,typs,consts = 
           List.fold_right (fun e (exps,typs,consts) -> let (e',t,_,c) = check_exp envs (new_t ()) e in ((e'::exps),(t::typs),c@consts)) exps ([],[],[]) in
-        expect_t.t <- Ttup typs;
-        (E_aux(E_tuple(exps),(l,Some(([],expect_t),Emp,consts))),expect_t,t_env,consts)
-      | _ -> typ_error l "Found a tuple when expecting a value of type INSERT TYPE PRINTING HERE")
+        let t = { t=Ttup typs } in
+        let t',cs',e' = type_coerce l d_env t (E_aux(E_tuple(exps),(l,Some(([],t),Emp,consts)))) expect_t in
+        (e',t',t_env,consts@cs'))
     | E_if(cond,then_,else_) ->
       let (cond',_,_,c1) = check_exp envs bool_t cond in
       let then',then_t,then_env,then_c = check_exp envs expect_t then_ in
       let else',else_t,else_env,else_c = check_exp envs expect_t else_ in
       (E_aux(E_if(cond',then',else'),(l,Some(([],expect_t),Emp,c1@then_c@else_c))),expect_t,Envmap.intersect then_env else_env,then_c@else_c@c1)
+    | E_for(id,from,to_,step,block) -> 
+      (E_aux(e,(l,annot)),expect_t,t_env,[]) (*TODO*)
+    | E_vector(es) ->
+      let item_t = match expect_t.t with
+        | Tapp("vector",[base;rise;ord;TA_typ item_t]) -> item_t
+          (* TODO: Consider whether an enum should be looked for here*)
+        | _ -> new_t () in
+      let es,cs = (List.fold_right (fun (e,_,_,c) (es,cs) -> (e::es),(c@cs)) (List.map (check_exp envs item_t) es) ([],[])) in
+      let t = {t = Tapp("vector",[TA_nexp({nexp=Nconst 0});TA_nexp({nexp=Nconst (List.length es)});TA_ord({order=Oinc});TA_typ item_t])} in
+      let t',cs',e' = type_coerce l d_env t (E_aux(E_vector es,(l,Some(([],t),Emp,cs)))) expect_t in
+      (e',t',t_env,cs@cs')
+    | E_let(lbind,body) -> 
+      let (lb',t_env',cs) = (check_lbind envs lbind) in
+      let (e,t,_,cs') = check_exp (Env(d_env,Envmap.union t_env t_env')) expect_t body in
+      (E_aux(E_let(lb',e),(l,Some(([],t),Emp,cs@cs'))),t,t_env,cs@cs')
     | _ -> (E_aux(e,(l,annot)),expect_t,t_env,[])
 		    
 and check_block orig_envs envs expect_t exps : ((tannot exp) list * tannot * tannot emap * nexp_range list * t) =
@@ -435,6 +491,29 @@ and check_block orig_envs envs expect_t exps : ((tannot exp) list * tannot * tan
 		 let (exps',annot',orig_envs,sc',t) = check_block orig_envs (Env(d_env,t_env)) expect_t exps in
 		 ((e'::exps'),annot',orig_envs,sc@sc',t)
 
+and check_lbind envs (LB_aux(lbind,(l,annot))) : tannot letbind * tannot emap * nexp_range list =
+  let Env(d_env,t_env) = envs in
+  match lbind with
+  | LB_val_explicit(typ,pat,e) -> 
+    let tan = typschm_to_tannot envs typ Emp in
+    (match tan with
+    | Some((params,t),tag,cs) ->
+      let t,cs = subst params t cs in
+      let (pat',env,cs1,u) = check_pattern envs pat in
+      let t',cs' = type_consistent l d_env u t in
+      let (e,t,_,cs2) = check_exp envs t' e in
+      let cs = resolve_constraints cs@cs1@cs'@cs2 in
+      let tannot = resolve_params(Some((params,t),tag,cs)) in
+      (LB_aux (LB_val_explicit(typ,pat',e),(l,tannot)),env,cs)
+    | None -> raise (Reporting_basic.err_unreachable l "typschm_to_tannot failed to produce a Some"))
+  | LB_val_implicit(pat,e) -> 
+    let t = new_t () in
+    let (pat',env,cs1,u) = check_pattern envs pat in
+    let (e,t',_,cs2) = check_exp envs u e in
+    let cs = resolve_constraints cs1@cs2 in
+    let tannot = resolve_params(Some(([],t'),Emp,cs)) in
+    (LB_aux (LB_val_implicit(pat',e),(l,tannot)), env,cs)
+
 (*val check_type_def : envs -> (tannot type_def) -> (tannot type_def) envs_out*)
 let check_type_def envs (TD_aux(td,(l,annot))) =
   let (Env(d_env,t_env)) = envs in
@@ -606,19 +685,20 @@ let check_fundef envs (FD_aux(FD_function(recopt,tannotopt,effectopt,funcls),(l,
 
 (*val check_def : envs -> tannot def -> (tannot def) envs_out*)
 let check_def envs (DEF_aux(def,(l,annot))) = 
+  let (Env(d_env,t_env)) = envs in
   match def with
     | DEF_type tdef -> let td,envs = check_type_def envs tdef in
 		       (DEF_aux((DEF_type td),(l,annot)),envs)
     | DEF_fundef fdef -> let fd,envs = check_fundef envs fdef in
 			 (DEF_aux(DEF_fundef(fd),(l,annot)),envs)
-    | DEF_val letdef -> (DEF_aux(def,(l,annot)),envs)
+    | DEF_val letdef -> let (letbind,t_env_let,_) = check_lbind envs letdef in
+                        (DEF_aux(DEF_val letbind,(l,annot)),Env(d_env,Envmap.union t_env_let t_env))
     | DEF_spec spec -> let vs,envs = check_val_spec envs spec in
 		       (DEF_aux(DEF_spec(vs),(l,annot)),envs)
     | DEF_default default -> let ds,envs = check_default envs default in
 			     (DEF_aux((DEF_default(ds)),(l,annot)),envs)
     | DEF_reg_dec(typ,id) -> 
       let t = (typ_to_t typ) in
-      let (Env(d_env,t_env)) = envs in
       let tannot = into_register (Some(([],t),External,[])) in 
       (DEF_aux(def,(l,tannot)),(Env(d_env,Envmap.insert t_env ((id_to_string id),tannot))))
 
diff --git a/src/type_internal.ml b/src/type_internal.ml
index 96dba7e4..ead2a124 100644
--- a/src/type_internal.ml
+++ b/src/type_internal.ml
@@ -213,13 +213,18 @@ let subst k_env t cs =
   in
   t_subst subst_env t, cs_subst subst_env cs
 
+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 rec t_to_string t = 
   match t.t with
     | Tid i -> i
     | Tvar i -> "'" ^ i
     | Tfn(t1,t2,e) -> (t_to_string t1) ^ " -> " ^ (t_to_string t2) ^ " effect " ^ e_to_string e
-    | Ttup(tups) -> "(" ^ (List.fold_right (fun t ts -> ts^ (t_to_string t) ^ " * ") tups "") ^ ")"
-    | Tapp(i,args) -> i ^ "<" ^ (List.fold_right (fun t ts -> ts^(targ_to_string t) ^ ", ") args "") ^ ">"
+    | Ttup(tups) -> "(" ^ string_of_list " * " t_to_string tups ^ ")"
+    | Tapp(i,args) -> i ^ "<" ^  string_of_list ", " targ_to_string args ^ ">"
     | Tuvar({index = i;subst = a}) -> string_of_int i ^ "()"
 and targ_to_string = function
   | TA_typ t -> t_to_string t
@@ -231,8 +236,21 @@ and n_to_string n =
     | Nvar i -> "'" ^ i
     | Nconst i -> string_of_int i
     | Nadd(n1,n2) -> (n_to_string n1) ^ " + " ^ (n_to_string n2)
-and e_to_string e = "effect"
-and o_to_string o = "order"
+    | Nmult(n1,n2) -> (n_to_string n1) ^ " * " ^ (n_to_string n2)
+    | N2n n -> "2**" ^ (n_to_string n)
+    | Nneg n -> "-" ^ (n_to_string n)
+    | Nuvar({nindex=i;nsubst=a}) -> string_of_int i ^ "()"
+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 ^ "()"
+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 ^ "()"
 
 let get_abbrev d_env t =
   match t.t with
diff --git a/src/type_internal.mli b/src/type_internal.mli
index 458009f5..458fb6fa 100644
--- a/src/type_internal.mli
+++ b/src/type_internal.mli
@@ -91,6 +91,8 @@ val unit_t : t
 val bool_t : t
 val bit_t : t
 
+val t_to_string : t -> string
+
 val reset_fresh : unit -> unit
 val new_t : unit -> t
 val new_n : unit -> nexp