Added tests for union constructor matching

4 files changed, 82 insertions, 1 deletions

diff --git a/src/ast_util.ml b/src/ast_util.ml
index a84df58b..d41ef180 100644
--- a/src/ast_util.ml
+++ b/src/ast_util.ml
@@ -285,6 +285,7 @@ and string_of_pat (P_aux (pat, l)) =
   | P_id v -> string_of_id v
   | P_typ (typ, pat) -> "(" ^ string_of_typ typ ^ ") " ^ string_of_pat pat
   | P_tup pats -> "(" ^ string_of_list ", " string_of_pat pats ^ ")"
+  | P_app (f, pats) -> string_of_id f ^ "(" ^ string_of_list ", " string_of_pat pats ^ ")"
   | _ -> "PAT"
 and string_of_lexp (LEXP_aux (lexp, _)) =
   match lexp with
diff --git a/src/type_check_new.ml b/src/type_check_new.ml
index 281ead22..e87a6bd2 100644
--- a/src/type_check_new.ml
+++ b/src/type_check_new.ml
@@ -317,6 +317,7 @@ module Env : sig
   type t
   val add_val_spec : id -> typquant * typ -> t -> t
   val get_val_spec : id -> t -> typquant * typ
+  val is_union_constructor : id -> t -> bool
   val add_record : id -> typquant -> (typ * id) list -> t -> t
   val is_record : id -> t -> bool
   val get_accessor : id -> t -> typquant * typ
@@ -428,6 +429,15 @@ end = struct
         { env with top_val_specs = Bindings.add id bind env.top_val_specs }
       end
 
+  let is_union_constructor id env =
+    let is_ctor id (Tu_aux (tu, _)) = match tu with
+      | Tu_id ctor_id when Id.compare id ctor_id = 0 -> true
+      | Tu_ty_id (_, ctor_id) when Id.compare id ctor_id = 0 -> true
+      | _ -> false
+    in
+    let type_unions = List.concat (List.map (fun (_, (_, tus)) -> tus) (Bindings.bindings env.variants)) in
+    List.exists (is_ctor id) type_unions
+
   let get_typ_var kid env =
     try KBindings.find kid env.typ_vars with
     | Not_found -> typ_error (kid_loc kid) ("No kind identifier " ^ string_of_kid kid)
@@ -1649,7 +1659,7 @@ and bind_pat env (P_aux (pat_aux, (l, ())) as pat) (Typ_aux (typ_aux, _) as typ)
           annot_pat (P_tup (List.rev tpats)) typ, env
        | _ -> typ_error l "Cannot bind tuple pattern against non tuple type"
      end
-  | P_app (f, pats) ->
+  | P_app (f, pats) when Env.is_union_constructor f env ->
      begin
        let (typq, ctor_typ) = Env.get_val_spec f env in
        let quants = quant_items typq in
@@ -1680,6 +1690,8 @@ and bind_pat env (P_aux (pat_aux, (l, ())) as pat) (Typ_aux (typ_aux, _) as typ)
           end
        | _ -> typ_error l ("Mal-formed constructor " ^ string_of_id f)
      end
+  | P_app (f, _) when not (Env.is_union_constructor f env) ->
+     typ_error l (string_of_id f ^ " is not a union constructor in pattern " ^ string_of_pat pat)
   | _ ->
      let (inferred_pat, env) = infer_pat env pat in
      subtyp l env (pat_typ_of inferred_pat) typ;
diff --git a/test/typecheck/fail/option_either1.sail b/test/typecheck/fail/option_either1.sail
new file mode 100644
index 00000000..569ba212
--- /dev/null
+++ b/test/typecheck/fail/option_either1.sail
@@ -0,0 +1,35 @@
+default Order inc
+
+typedef option = const union forall Type 'a. {
+    None;
+    'a Some
+}
+
+function forall Type 'a. option<'a> none () = None
+
+function forall Type 'a. option<'a> some (('a) x) = Some(x)
+
+function forall Type 'a. int test ((option<'a>) x) =
+{
+  switch x {
+    case None -> 0
+    case (Some(y)) -> 1
+  }
+}
+
+typedef either = const union forall Type 'a, Type 'b. {
+  'a Left;
+  'b Right
+}
+
+val forall Nat 'n, 'n >= 0. bit['n] -> int effect pure signed
+
+function forall Type 'a, Type 'b. either<'a,'b> right (('b) x) = Right(x)
+
+function int test2 ((either<int,bit[1]>) x) =
+{
+  switch x {
+    case (Left(l)) -> l
+    case (right(r)) -> signed(r)
+  }
+}
diff --git a/test/typecheck/pass/option_either.sail b/test/typecheck/pass/option_either.sail
new file mode 100644
index 00000000..c466daf4
--- /dev/null
+++ b/test/typecheck/pass/option_either.sail
@@ -0,0 +1,33 @@
+default Order inc
+
+typedef option = const union forall Type 'a. {
+    None;
+    'a Some
+}
+
+function forall Type 'a. option<'a> none () = None
+
+function forall Type 'a. option<'a> some (('a) x) = Some(x)
+
+function forall Type 'a. int test ((option<'a>) x) =
+{
+  switch x {
+    case None -> 0
+    case (Some(y)) -> 1
+  }
+}
+
+typedef either = const union forall Type 'a, Type 'b. {
+  'a Left;
+  'b Right
+}
+
+val forall Nat 'n, 'n >= 0. bit['n] -> int effect pure signed
+
+function int test2 ((either<int,bit[1]>) x) =
+{
+  switch x {
+    case (Left(l)) -> l
+    case (Right(r)) -> signed(r)
+  }
+}