Fixed various issues regarding typechecking lists.

5 files changed, 42 insertions, 0 deletions

diff --git a/src/ast_util.ml b/src/ast_util.ml
index df8f5af3..01509ab8 100644
--- a/src/ast_util.ml
+++ b/src/ast_util.ml
@@ -296,6 +296,8 @@ let rec string_of_exp (E_aux (exp, _)) =
      ^ string_of_exp body
   | E_assert (test, msg) -> "assert(" ^ string_of_exp test ^ ", " ^ string_of_exp msg ^ ")"
   | E_exit exp -> "exit " ^ string_of_exp exp
+  | E_cons (x, xs) -> string_of_exp x ^ " :: " ^ string_of_exp xs
+  | E_list xs -> "[||" ^ string_of_list ", " string_of_exp xs ^ "||]"
   | _ -> "INTERNAL"
 and string_of_pexp (Pat_aux (pexp, _)) =
   match pexp with
diff --git a/src/type_check.ml b/src/type_check.ml
index 2a23eb93..e61d1425 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -118,6 +118,12 @@ let is_range (Typ_aux (typ_aux, _)) =
        when string_of_id f = "range" -> Some (n1, n2)
   | _ -> None
 
+let is_list (Typ_aux (typ_aux, _)) =
+  match typ_aux with
+  | Typ_app (f, [Typ_arg_aux (Typ_arg_typ typ, _)])
+       when string_of_id f = "list" -> Some typ
+  | _ -> None
+
 let nconstant c = Nexp_aux (Nexp_constant c, Parse_ast.Unknown)
 let nminus n1 n2 = Nexp_aux (Nexp_minus (n1, n2), Parse_ast.Unknown)
 let nsum n1 n2 = Nexp_aux (Nexp_sum (n1, n2), Parse_ast.Unknown)
@@ -1690,6 +1696,23 @@ let rec check_exp env (E_aux (exp_aux, (l, ())) as exp : unit exp) (Typ_aux (typ
           Pat_aux (Pat_when (tpat, checked_guard, crule check_exp env case typ), (l, None))
      in
      annot_exp (E_case (inferred_exp, List.map (fun case -> check_case case typ) cases)) typ
+  | E_cons (x, xs), _ ->
+     begin
+       match is_list (Env.expand_synonyms env typ) with
+       | Some elem_typ ->
+          let checked_xs = crule check_exp env xs typ in
+          let checked_x = crule check_exp env x elem_typ in
+          annot_exp (E_cons (checked_x, checked_xs)) typ
+       | None -> typ_error l ("Cons " ^ string_of_exp exp ^ " must have list type, got " ^ string_of_typ typ)
+     end
+  | E_list xs, _ ->
+     begin
+       match is_list (Env.expand_synonyms env typ) with
+       | Some elem_typ ->
+          let checked_xs = List.map (fun x -> crule check_exp env x elem_typ) xs in
+          annot_exp (E_list checked_xs) typ
+       | None -> typ_error l ("List " ^ string_of_exp exp ^ " must have list type, got " ^ string_of_typ typ)
+     end
   | E_let (LB_aux (letbind, (let_loc, _)), exp), _ ->
      begin
        match letbind with
@@ -2466,6 +2489,13 @@ and propagate_exp_effect_aux = function
      let p_lb, eff = propagate_letbind_effect letbind in
      let p_exp = propagate_exp_effect exp in
      E_let (p_lb, p_exp), union_effects (effect_of p_exp) eff
+  | E_cons (x, xs) ->
+     let p_x = propagate_exp_effect x in
+     let p_xs = propagate_exp_effect xs in
+     E_cons (p_x, p_xs), union_effects (effect_of p_x) (effect_of p_xs)
+  | E_list xs ->
+     let p_xs = List.map propagate_exp_effect xs in
+     E_list p_xs, collect_effects p_xs
   | E_assign (lexp, exp) ->
      let p_lexp = propagate_lexp_effect lexp in
      let p_exp = propagate_exp_effect exp in
diff --git a/test/typecheck/pass/list_cons.sail b/test/typecheck/pass/list_cons.sail
new file mode 100644
index 00000000..6f103bf6
--- /dev/null
+++ b/test/typecheck/pass/list_cons.sail
@@ -0,0 +1 @@
+function list<int> foo ((int) i, (list<int>) l) = i :: l
diff --git a/test/typecheck/pass/list_cons2.sail b/test/typecheck/pass/list_cons2.sail
new file mode 100644
index 00000000..8c34282b
--- /dev/null
+++ b/test/typecheck/pass/list_cons2.sail
@@ -0,0 +1,7 @@
+function list<int> foo ((int) i, (list<int>) l) = i :: l
+
+function list<int> bar () = [||||]
+
+function list<int> baz ((list<int>) l) = l
+
+function list<int> quux () = baz ([||||])
diff --git a/test/typecheck/pass/list_lit.sail b/test/typecheck/pass/list_lit.sail
new file mode 100644
index 00000000..d4febadf
--- /dev/null
+++ b/test/typecheck/pass/list_lit.sail
@@ -0,0 +1,2 @@
+
+let (list<int>) xs = [||1,2,3,4,5,6||]