fixed pattern of type unit

src/ttypes.ml

@@ -190,8 +190,8 @@ let ts_list =
 
 let ts_tuple =
   let ts_tuples = Hashtbl.create 0 in
+  Hashtbl.add ts_tuples 0 ts_unit;
   fun n ->
-    (* if n = 0 then ts_unit else *)
     try Hashtbl.find ts_tuples n
     with Not_found ->
       let ts_id = Ident.create ~loc:Location.none ("tuple" ^ string_of_int n) in

src/typing.ml

@@ -752,7 +752,7 @@ let process_val_spec kid crcm ns id args ret vs =
   let env, ret =
     match (header.sp_hd_ret, ret.ty_node) with
     | [], _ -> (env, [])
-    | _, Tyapp (ts, tyl) when is_ts_tuple ts ->
+    | _, Tyapp (ts, tyl) when not (ts_equal ts ts_unit) && is_ts_tuple ts ->
         let tyl = List.map (fun ty -> (ty, Asttypes.Nolabel)) tyl in
         process_args header.sp_hd_ret tyl env []
     | _, _ -> process_args header.sp_hd_ret [ (ret, Asttypes.Nolabel) ] env []

test/positive/pattern_matching.mli

@@ -1,3 +1,4 @@
+
 type t = O | S of t
 
 val succ : t -> t
@@ -11,3 +12,12 @@ val test1 : t -> t -> t
              | _, S _ -> false
              | O, _   -> false
              | S a, O -> r = S (S a) *)
+
+(* pattern of type unit *)
+val f_unit: int -> unit
+(*@ x1 = f_unit x0
+     ensures match x1 with () -> true *)
+
+(*@ function fun_unit (x: unit): string =
+    match x with
+    | () -> "out" *)

test/positive/pattern_matching.mli.expected

@@ -14,6 +14,13 @@ val test1 : t -> t -> t[@@gospel
              | _, S _ -> false
              | O, _   -> false
              | S a, O -> r = S (S a) |}]
+val f_unit : int -> unit[@@gospel
+                          {| x1 = f_unit x0
+     ensures match x1 with () -> true |}]
+[@@@gospel
+  {| function fun_unit (x: unit): string =
+    match x with
+    | () -> "out" |}]
 
 *******************************
 ****** GOSPEL translation *****
@@ -36,6 +43,13 @@ val test1 : t -> t -> t
     ensures ...
      *)
 
+val f_unit : int -> unit
+(*@ x1 = f_unit x0
+    ensures ...
+     *)
+
+(*@ function fun_unit ... *)
+
 *******************************
 ********* Typed GOSPEL ********
 *******************************
@@ -48,6 +62,7 @@ module pattern_matching.mli
     Logic Symbols
       function O  : t
       function S (_:t) : t
+      function fun_unit (_:unit) : string
 
     Field Symbols
 
@@ -81,5 +96,17 @@ module pattern_matching.mli
                               (S  a:t):t):t):prop then (True ):bool else (False ):
                               bool
                 end::bool = (True ):bool):prop*)
+
+    val f_unit : int -> unit
+    (*@ x1:unit = f_unit x0:int
+        ensures (match x1:unit with
+                |  -> (True ):bool
+                end::bool = (True ):bool):prop*)
+
+    (*@ function fun_unit (x_2:unit): string =
+        match x_2:unit with
+        |  -> "out":string
+        end::string
+    *)
 
 OK