Generalise pairs to n-tuples (#19)

This (surprisingly annoying-to-write?) PR generalises the pairs that we had previously to tuples of arbitrary length. This will be useful for the multiple mailboxes extension.

Note that currently we still can't do nested pattern matching: while we can construct `((1, 2), 3)`, we can't deconstruct it like `let ((x, y), z) = ((1, 2), 3) in y` just yet. One for another patch.

This patch also removes the unit constant and unit type (which are nullary tuples and the nullary tuple type respectively). 
To preserve backwards compatibility, `Unit` is now an alias for `()`.

Author: SimonJF

lib/common/common_types.ml

@@ -6,14 +6,12 @@ module Base = struct
         | Int
         | Bool
         | String
-        | Unit
     [@@deriving show]
 
     let pp ppf =
         let ps = Format.pp_print_string ppf in
         function
            | Atom -> ps "Atom"
-           | Unit -> ps "Unit"
            | Int -> ps "Int"
            | Bool -> ps "Bool"
            | String -> ps "String"
@@ -30,24 +28,20 @@ type tag = string
 (* Boxed constants *)
 module Constant = struct
     type t =
-        | Unit
         | Int of int
         | String of string
         | Bool of bool
 
     let type_of = function
-        | Unit -> Base.Unit
         | Int _ -> Base.Int
         | Bool _ -> Base.Bool
         | String _ -> Base.String
 
     let pp ppf = function
-        | Unit -> Format.pp_print_string ppf "()"
         | Int i -> Format.pp_print_int ppf i
         | String s -> Format.fprintf ppf "\"%s\"" s
         | Bool b -> Format.pp_print_bool ppf b
 
-    let unit = Unit
     let wrap_int i = Int i
     let wrap_string s = String s
     let wrap_bool b = Bool b

lib/common/ir.ml

@@ -85,12 +85,11 @@ and comp_node =
         args: value list
       }
     | If of { test: value; then_expr: comp; else_expr: comp }
-    | LetPair of {
+    | LetTuple of {
         (* By annotating with inferred pretypes, we can always use a checking rule
            during inference, irrespective of whether both of the binders are used. *)
-        binders: ( ((Binder.t[@name "binder"]) * (Pretype.t[@name "pretype"]) option) *
-                   ((Binder.t[@name "binder"]) * (Pretype.t[@name "pretype"]) option));
-        pair: value;
+        binders: ((Binder.t[@name "binder"]) * (Pretype.t[@name "pretype"]) option) list;
+        tuple: value;
         cont: comp
     }
     | Case of {
@@ -119,7 +118,7 @@ and value_node =
     | Constant of constant
     | Primitive of primitive_name
     | Variable of (Var.t[@name "var"]) * (Pretype.t[@name "pretype"]) option
-    | Pair of value * value
+    | Tuple of value list
     | Inl of value
     | Inr of value
     | Lam of {
@@ -231,11 +230,11 @@ and pp_comp ppf comp_with_pos =
                         pp_value target
                         pp_message message
         end
-    | LetPair { binders = ((b1, _), (b2, _)); pair; cont } ->
-        fprintf ppf "let (%a, %a) = @[<v>%a@] in@,%a"
-            Binder.pp b1
-            Binder.pp b2
-            pp_value pair
+    | LetTuple { binders = bs; tuple; cont } ->
+        let bs = List.map fst bs in
+        fprintf ppf "let %a = @[<v>%a@] in@,%a"
+            (pp_print_comma_list Binder.pp) bs
+            pp_value tuple
             pp_comp cont
     | Case { term; branch1; branch2 } ->
         fprintf ppf
@@ -259,8 +258,8 @@ and pp_value ppf v =
     | Primitive prim -> Format.pp_print_string ppf prim
     | Variable (var, _) -> Var.pp ppf var
     | Constant c -> Constant.pp ppf c
-    | Pair (v1, v2) ->
-        fprintf ppf "(%a, %a)" pp_value v1 pp_value v2
+    | Tuple vs ->
+        fprintf ppf "%a" (pp_print_comma_list pp_value) vs
     | Inl v -> fprintf ppf "inl(%a)" pp_value v
     | Inr v -> fprintf ppf "inr(%a)" pp_value v
     | Lam { linear; parameters; result_type; body } ->
@@ -284,6 +283,7 @@ and pp_guard ppf guard_with_pos =
     | Fail ->
         fprintf ppf "fail"
 
+let unit = Tuple []
 
 let is_receive_guard = function
     | Receive _ -> true

lib/common/lib_types.ml

@@ -20,9 +20,9 @@ let signatures =
     in
     int_ops @ int_rel_ops @ bool_rel_ops @
     [
-        ("print", function_type false [Base Base.String] (Base Base.Unit));
-        ("concat", function_type false [Base Base.String; Base Base.String] (Base Base.String));
+        ("print", function_type false [Base Base.String] Type.unit_type);
+        ("concat", function_type false [Base Base.String; Base Base.String] Type.string_type);
         ("rand", function_type false [Base Base.Int] (Base Base.Int));
-        ("sleep", function_type false [Base Base.Int] (Base Base.Unit));
+        ("sleep", function_type false [Base Base.Int] Type.unit_type);
         ("intToString", function_type false [Base Base.Int] (Base Base.String))
     ]

lib/common/pretype.ml

@@ -14,27 +14,30 @@ type t =
     | PFun of { linear: bool; args: (Type.t[@name "ty"]) list; result: t[@name "pretype"] }
     | PInterface of string
     | PSum of (t * t)
-    | PPair of (t * t)
+    | PTuple of t list
     [@@name "pretype"]
     [@@deriving visitors { variety = "map" }]
 and base = [%import: Common_types.Base.t]
 
+let unit = PTuple []
+
 let rec pp ppf =
-  let ps = Format.pp_print_string ppf in
+  let open Format in
+  let ps = pp_print_string ppf in
   function
     | PBase b -> Common_types.Base.pp ppf b
     | PFun { linear; args; result } ->
         let arrow = if linear then "-o" else "->" in
-        Format.fprintf ppf "(%a) %s %a"
+        fprintf ppf "(%a) %s %a"
             (pp_print_comma_list Type.pp) args
             arrow
             pp result
-    | PPair (t1, t2) ->
-        Format.fprintf ppf "(%a * %a)"
-            pp t1
-            pp t2
+    | PTuple ts ->
+        let pp_star ppf () = pp_print_string ppf " * " in
+        fprintf ppf "(%a)"
+            (pp_print_list ~pp_sep:(pp_star) pp) ts
     | PSum (t1, t2) ->
-        Format.fprintf ppf "(%a + %a)"
+        fprintf ppf "(%a + %a)"
             pp t1
             pp t2
     | PInterface name -> ps name
@@ -48,7 +51,7 @@ let rec of_type = function
     | Type.Base b -> PBase b
     | Type.Fun { linear; args; result } ->
         PFun { linear; args; result = of_type result }
-    | Type.Pair (t1, t2) -> PPair (of_type t1, of_type t2)
+    | Type.Tuple ts -> PTuple (List.map of_type ts)
     | Type.Sum (t1, t2) -> PSum (of_type t1, of_type t2)
     | Type.Mailbox { interface; _ } -> PInterface interface
 
@@ -63,16 +66,18 @@ let rec to_type = function
         (fun result ->
             Some (Type.Fun { linear; args; result })
         )
-    | PPair (t1, t2) ->
-        begin
-        match to_type t1, to_type t2 with
-            | Some ty1, Some ty2 -> Some (Type.Pair (ty1, ty2))
-            | _, _ -> None
-        end
+    | PTuple ts ->
+        let rec go acc =
+            function
+                | [] -> Some (List.rev acc)
+                | x :: xs ->
+                    Option.bind (to_type x) (fun t -> go (t :: acc) xs)
+        in
+        Option.bind (go [] ts) (fun ts -> Some (Type.Tuple ts))
     | PSum (t1, t2) ->
         begin
-        match to_type t1, to_type t2 with
-            | Some ty1, Some ty2 -> Some (Type.Sum (ty1, ty2))
-            | _, _ -> None
+            match to_type t1, to_type t2 with
+                | Some ty1, Some ty2 -> Some (Type.Sum (ty1, ty2))
+                | _, _ -> None
         end
     | PInterface _ -> None

lib/common/sugar_ast.ml

@@ -31,11 +31,11 @@ and expr_node =
         args: expr list
     }
     | If of { test: expr; then_expr: expr; else_expr: expr }
-    (* Pairs *)
-    | Pair of (expr * expr)
-    | LetPair of {
-        binders: sugar_binder * sugar_binder;
-        annot: ((Type.t[@name "ty"]) * (Type.t[@name "ty"])) option;
+    (* Tuples *)
+    | Tuple of expr list
+    | LetTuple of {
+        binders: sugar_binder list;
+        annot: ((Type.t[@name "ty"]) list) option;
         term: expr;
         cont: expr
     }
@@ -224,18 +224,18 @@ and pp_expr ppf expr_with_pos =
             pp_expr e1
             pp_bnd_ann bnd2
             pp_expr e2
-    | Pair (e1, e2) ->
-        fprintf ppf "(%a, %a)" pp_expr e1 pp_expr e2
-    | LetPair { binders = (b1, b2); annot = None; term; cont } ->
-        fprintf ppf "let (%s, %s) = %a in %a"
-            b1 b2
+    | Tuple es ->
+        fprintf ppf "(%a)" (pp_print_comma_list pp_expr) es
+    | LetTuple { binders = bs; annot = None; term; cont } ->
+        fprintf ppf "let (%a) = %a in %a"
+            (pp_print_comma_list pp_print_string) bs
             pp_expr term
             pp_expr cont
-    | LetPair { binders = (b1, b2); annot = Some (t1, t2); term; cont } ->
-        fprintf ppf "let (%s, %s) : (%a * %a) = %a in %a"
-            b1 b2
-            Type.pp t1
-            Type.pp t2
+    | LetTuple { binders = bs; annot = Some ts; term; cont } ->
+        assert (List.length bs = List.length ts);
+        fprintf ppf "let (%a) : (%a) = %a in %a"
+            (pp_print_comma_list pp_print_string) bs
+            (pp_print_comma_list Type.pp) ts
             pp_expr term
             pp_expr cont
     | Guard { target; pattern; guards; _ } ->

lib/common/type.ml

@@ -251,7 +251,7 @@ end
 type t =
     | Base of base
     | Fun of { linear: bool; args: t list; result: t }
-    | Pair of (t * t)
+    | Tuple of t list
     | Sum of (t * t)
     | Mailbox of {
         capability: (Capability.t [@name "capability"]);
@@ -286,14 +286,15 @@ let is_mailbox_type = function
 
 let rec contains_mailbox_type = function
     | Mailbox _ -> true
-    | Sum (t1, t2) | Pair (t1, t2) -> contains_mailbox_type t1 || contains_mailbox_type t2
+    | Sum (t1, t2) -> contains_mailbox_type t1 || contains_mailbox_type t2
+    | Tuple ts -> List.exists contains_mailbox_type ts
     | _ -> false
 
 (* Easy constructors *)
 let int_type = Base Base.Int
 let string_type = Base Base.String
 let bool_type = Base Base.Bool
-let unit_type = Base Base.Unit
+let unit_type = Tuple []
 let atom = Base Base.Atom
 let function_type linear args result =
     Fun { linear; args; result }
@@ -316,10 +317,10 @@ let rec pp ppf =
             (pp_print_comma_list pp) args
             arrow
             pp result
-    | Pair (t1, t2) ->
-        fprintf ppf "(%a * %a)"
-            pp t1
-            pp t2
+    | Tuple ts ->
+        let pp_star ppf () = pp_print_string ppf " * " in
+        fprintf ppf "(%a)"
+            (pp_print_list ~pp_sep:(pp_star) pp) ts
     | Sum (t1, t2) ->
         fprintf ppf "(%a + %a)"
             pp t1
@@ -355,7 +356,7 @@ let rec is_lin = function
     | Fun { linear; _ } -> linear
     (* !1 is unrestricted... *)
     | Mailbox { capability = Out; pattern = Some One; _ } -> false
-    | Pair (t1, t2) -> is_lin t1 || is_lin t2
+    | Tuple ts -> List.exists is_lin ts
     | Sum (t1, t2) -> is_lin t1 || is_lin t2
     (* ...but otherwise a mailbox type must be used linearly. *)
     | Mailbox _ -> true
@@ -368,8 +369,8 @@ let is_output_mailbox = function
     | Mailbox { capability = Out; pattern = Some _; _ } -> true
     | _ -> false
 
-let is_pair = function
-    | Pair _ -> true
+let is_tuple = function
+    | Tuple _ -> true
     | _ -> false
 
 let is_sum = function
@@ -391,13 +392,13 @@ let get_quasilinearity = function
 
 let rec make_usable = function
     | Mailbox m -> Mailbox { m with quasilinearity = Quasilinearity.Usable }
-    | Pair (t1, t2) -> Pair (make_usable t1, make_usable t2)
+    | Tuple ts -> Tuple (List.map make_usable ts)
     | Sum (t1, t2) -> Sum (make_usable t1, make_usable t2)
     | t -> t
 
 let rec make_returnable = function
     | Mailbox m -> Mailbox { m with quasilinearity = Quasilinearity.Returnable }
-    | Pair (t1, t2) -> Pair (make_returnable t1, make_returnable t2)
+    | Tuple ts -> Tuple (List.map make_returnable ts) 
     | Sum (t1, t2) -> Sum (make_returnable t1, make_returnable t2)
     | t -> t
 
@@ -406,15 +407,15 @@ let is_unr = is_lin >> not
 let rec is_returnable = function
     | Mailbox { quasilinearity = ql; _ } ->
         ql = Quasilinearity.Returnable
-    | Pair (t1, t2)
+    | Tuple ts -> List.for_all is_returnable ts
     | Sum  (t1, t2) -> is_returnable t1 && is_returnable t2
     | _ -> true
 
 let make_function_type linear args result =
     Fun { linear; args; result }
 
-let make_pair_type ty1 ty2 =
-    Pair (make_returnable ty1, make_returnable ty2)
+let make_tuple_type tys =
+    Tuple (List.map make_returnable tys)
 
 let make_sum_type ty1 ty2 =
     Sum (make_returnable ty1, make_returnable ty2)

lib/frontend/desugar_let_annotations.ml

@@ -17,13 +17,13 @@ let visitor =
                     let body = self#visit_expr env body in
                     let term = { expr_with_pos with node = Annotate (inner_term, Type.make_returnable annot') } in
                         { expr_with_pos with node = Let { binder; annot = None; term; body } }
-                | LetPair { binders; annot = Some (ty1, ty2); term; cont } ->
+                | LetTuple { binders; annot = Some tys; term; cont } ->
                     let cont = self#visit_expr env cont in
                     let term =
                         { expr_with_pos with node = 
-                            Annotate (term, Type.make_returnable (Type.make_pair_type ty1 ty2)) }
+                            Annotate (term, Type.make_returnable (Type.make_tuple_type tys)) }
                     in
-                        { expr_with_pos with node = LetPair { binders; annot = None; term; cont } }
+                        { expr_with_pos with node = LetTuple { binders; annot = None; term; cont } }
                 | _ -> super#visit_expr env expr_with_pos
     end
 

lib/frontend/insert_pattern_variables.ml

@@ -18,8 +18,8 @@ let rec annotate_type =
                 args = List.map annotate_type args;
                 result = annotate_type result
             }
-        | Pair (t1, t2) ->
-            Pair (annotate_type t1, annotate_type t2)
+        | Tuple ts ->
+            Tuple (List.map annotate_type ts)
         | Sum (t1, t2) ->
             Sum (annotate_type t1, annotate_type t2)
         | Mailbox { pattern = Some _; _ } as mb -> mb