diff options
| -rw-r--r-- | lib/prelude.sail | 7 | ||||
| -rw-r--r-- | src/ast_util.ml | 1 | ||||
| -rw-r--r-- | src/type_check.ml | 8 | ||||
| -rw-r--r-- | test/typecheck/pass/cons_pattern_synonym.sail | 7 |
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 |