Merge remote-tracking branch 'origin/sail_new_tc' into experiments

4 files changed, 19 insertions, 4 deletions

diff --git a/lib/prelude.sail b/lib/prelude.sail
index bb19aa8d..bac9532c 100644
--- a/lib/prelude.sail
+++ b/lib/prelude.sail
@@ -181,6 +181,13 @@ overload (deinfix <<) [
   shiftl
 ]
 
+val forall Num 'n, Num 'o, Order 'ord.
+    (vector<'o, 'n, 'ord, bit>, int) -> vector<'o, 'n, 'ord, bit> effect pure shiftr
+
+overload (deinfix >>) [
+  shiftr
+]
+
 (* Boolean operators *)
 val bool -> bool effect pure bool_not
 val (bool, bool) -> bool effect pure bool_or
diff --git a/src/ast_util.ml b/src/ast_util.ml
index 2d714158..67eedf72 100644
--- a/src/ast_util.ml
+++ b/src/ast_util.ml
@@ -294,6 +294,7 @@ 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
   | _ -> "INTERNAL"
 and string_of_pexp (Pat_aux (pexp, _)) =
   match pexp with
diff --git a/src/type_check.ml b/src/type_check.ml
index 1a72edc9..3c133405 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -1910,8 +1910,8 @@ and bind_pat env (P_aux (pat_aux, (l, ())) as pat) (Typ_aux (typ_aux, _) as typ)
   | P_wild -> annot_pat P_wild typ, env
   | P_cons (hd_pat, tl_pat) ->
      begin
-       match typ_aux with
-       | Typ_app (f, [Typ_arg_aux (Typ_arg_typ ltyp, _)]) when Id.compare f (mk_id "list") = 0 ->
+       match Env.expand_synonyms env typ with
+       | Typ_aux (Typ_app (f, [Typ_arg_aux (Typ_arg_typ ltyp, _)]), _) when Id.compare f (mk_id "list") = 0 ->
           let hd_pat, env = bind_pat env hd_pat ltyp in
           let tl_pat, env = bind_pat env tl_pat typ in
           annot_pat (P_cons (hd_pat, tl_pat)) typ, env
@@ -1919,8 +1919,8 @@ and bind_pat env (P_aux (pat_aux, (l, ())) as pat) (Typ_aux (typ_aux, _) as typ)
      end
   | P_list pats ->
      begin
-       match typ_aux with
-       | Typ_app (f, [Typ_arg_aux (Typ_arg_typ ltyp, _)]) when Id.compare f (mk_id "list") = 0 ->
+       match Env.expand_synonyms env typ with
+       | Typ_aux (Typ_app (f, [Typ_arg_aux (Typ_arg_typ ltyp, _)]), _) when Id.compare f (mk_id "list") = 0 ->
           let rec process_pats env = function
             | [] -> [], env
             | (pat :: pats) ->
diff --git a/test/typecheck/pass/cons_pattern_synonym.sail b/test/typecheck/pass/cons_pattern_synonym.sail
new file mode 100644
index 00000000..f5b26294
--- /dev/null
+++ b/test/typecheck/pass/cons_pattern_synonym.sail
@@ -0,0 +1,7 @@
+typedef ty = list<(bit[8])>
+
+function bool foo ((ty) l) =
+  switch l {
+    case _ :: _ -> false
+    case _ -> true
+  }
\ No newline at end of file