From 73a2a868f813b03cd60e93b1db25239770cab5df Mon Sep 17 00:00:00 2001
From: Danielle Marshall <danielle@starsandspira.ls>
Date: Wed, 19 Mar 2025 14:04:22 +0000
Subject: [PATCH 01/33] wip: add lists

---
 lib/common/ir.ml                         | 33 +++++++++++++--
 lib/common/pretype.ml                    | 15 +++++++
 lib/common/sugar_ast.ml                  | 26 +++++++++++-
 lib/common/type.ml                       | 17 +++++++-
 lib/frontend/insert_pattern_variables.ml |  3 +-
 lib/frontend/lexer.mll                   |  5 ++-
 lib/frontend/parser.mly                  | 37 ++++++++++++-----
 lib/frontend/sugar_to_ir.ml              | 20 ++++++++-
 lib/typecheck/gen_constraints.ml         | 51 +++++++++++++++++++++--
 lib/typecheck/gripers.ml                 | 14 +++++--
 lib/typecheck/pretypecheck.ml            | 53 +++++++++++++++++++++---
 lib/typecheck/ty_env.ml                  | 46 +++++++++++++++++++-
 lib/typecheck/type_utils.ml              |  4 +-
 test/examples/savina/kfork.pat           | 43 +++++++++++--------
 test/pat-tests/list-1.pat                |  9 ++++
 test/pat-tests/list-2.pat                | 23 ++++++++++
 16 files changed, 348 insertions(+), 51 deletions(-)
 create mode 100644 test/pat-tests/list-1.pat
 create mode 100644 test/pat-tests/list-2.pat

diff --git a/lib/common/ir.ml b/lib/common/ir.ml
index c659c71..cf728ab 100644
--- a/lib/common/ir.ml
+++ b/lib/common/ir.ml
@@ -97,6 +97,11 @@ and comp_node =
         branch1: ((Binder.t[@name "binder"]) * (Type.t[@name "ty"])) * comp;
         branch2: ((Binder.t[@name "binder"]) * (Type.t[@name "ty"])) * comp
     }
+    | CaseL of {
+        term: value;
+        nil: (Type.t[@name "ty"]) * comp;
+        cons: (((Binder.t[@name "binder"]) * (Binder.t[@name "binder"])) * (Type.t[@name "ty"])) * comp
+    }
     | New of string
     | Spawn of comp
     | Send of {
@@ -119,6 +124,8 @@ and value_node =
     | Primitive of primitive_name
     | Variable of (Var.t[@name "var"]) * (Pretype.t[@name "pretype"]) option
     | Tuple of value list
+    | Nil
+    | Cons of value * value
     | Inl of value
     | Inr of value
     | Lam of {
@@ -189,6 +196,18 @@ and pp_branch name ppf ((bnd, ty), c) =
         Binder.pp bnd
         Type.pp ty
         pp_comp c
+and pp_nil name ppf (ty, c) =
+  fprintf ppf "%s([]): %a -> @[<v>%a@]"
+    name
+    Type.pp ty
+    pp_comp c
+and pp_cons name ppf (((bnd1, bnd2), ty), c) =
+    fprintf ppf "%s(%a :: %a): %a -> @[<v>%a@]"
+        name
+        Binder.pp bnd1
+        Binder.pp bnd2
+        Type.pp ty
+        pp_comp c
 (* Expressions *)
 and pp_comp ppf comp_with_pos =
     let comp_node = WithPos.node comp_with_pos in
@@ -242,6 +261,12 @@ and pp_comp ppf comp_with_pos =
             pp_value term
             (pp_branch "inl") branch1
             (pp_branch "inr") branch2
+    | CaseL { term; nil; cons } ->
+        fprintf ppf
+            "caseL %a of {@[<v>@[<v>%a@]@,@[<v>%a@]@]}"
+            pp_value term
+            (pp_nil "nil") nil
+            (pp_cons "cons") cons
     | Guard { target; pattern; guards; _ } ->
         fprintf ppf
             "guard %a : %a {@,@[<v 2>  %a@]@,}"
@@ -260,6 +285,9 @@ and pp_value ppf v =
     | Constant c -> Constant.pp ppf c
     | Tuple vs ->
         fprintf ppf "%a" (pp_print_comma_list pp_value) vs
+    | Nil -> Format.pp_print_string ppf "Nil"
+    | Cons (v1, v2) ->
+        fprintf ppf "%a :: %a" pp_value v1 pp_value v2
     | Inl v -> fprintf ppf "inl(%a)" pp_value v
     | Inr v -> fprintf ppf "inr(%a)" pp_value v
     | Lam { linear; parameters; result_type; body } ->
@@ -269,7 +297,7 @@ and pp_value ppf v =
             (pp_print_comma_list pp_param) parameters
             Type.pp result_type
             pp_comp body
-and pp_guard ppf guard_with_pos = 
+and pp_guard ppf guard_with_pos =
     let guard_node = WithPos.node guard_with_pos in
     match guard_node with
     | Receive { tag; payload_binders; mailbox_binder; cont } ->
@@ -293,7 +321,7 @@ let is_free_guard = function
     | Free _ -> true
     | _ -> false
 
-let is_fail_guard guard = 
+let is_fail_guard guard =
     match WithPos.node guard with
     | Fail -> true
     | _ -> false
@@ -312,4 +340,3 @@ let substitute_solution sol =
         end
     in
     visitor#visit_program ()
-
diff --git a/lib/common/pretype.ml b/lib/common/pretype.ml
index f8c96c1..febf2b7 100644
--- a/lib/common/pretype.ml
+++ b/lib/common/pretype.ml
@@ -14,7 +14,12 @@ type t =
     | PFun of { linear: bool; args: (Type.t[@name "ty"]) list; result: t[@name "pretype"] }
     | PInterface of string
     | PSum of (t * t)
+<<<<<<< HEAD
     | PTuple of t list
+=======
+    | PPair of (t * t)
+    | PList of t
+>>>>>>> f735eea (wip: add lists)
     [@@name "pretype"]
     [@@deriving visitors { variety = "map" }]
 and base = [%import: Common_types.Base.t]
@@ -40,6 +45,9 @@ let rec pp ppf =
         fprintf ppf "(%a + %a)"
             pp t1
             pp t2
+    | PList t ->
+        Format.fprintf ppf "[%a]"
+            pp t
     | PInterface name -> ps name
 
 let show t =
@@ -53,6 +61,7 @@ let rec of_type = function
         PFun { linear; args; result = of_type result }
     | Type.Tuple ts -> PTuple (List.map of_type ts)
     | Type.Sum (t1, t2) -> PSum (of_type t1, of_type t2)
+    | Type.List t -> PList (of_type t)
     | Type.Mailbox { interface; _ } -> PInterface interface
 
 (* As long as a pretype isn't a mailbox type, and isn't a function
@@ -80,4 +89,10 @@ let rec to_type = function
                 | Some ty1, Some ty2 -> Some (Type.Sum (ty1, ty2))
                 | _, _ -> None
         end
+    | PList t ->
+        begin
+        match to_type t with
+            | Some t -> Some (Type.List t)
+            | _ -> None
+        end
     | PInterface _ -> None
diff --git a/lib/common/sugar_ast.ml b/lib/common/sugar_ast.ml
index ebd1d1a..7e3f0fe 100644
--- a/lib/common/sugar_ast.ml
+++ b/lib/common/sugar_ast.ml
@@ -39,6 +39,14 @@ and expr_node =
         term: expr;
         cont: expr
     }
+    (* Lists *)
+    | Nil
+    | Cons of (expr * expr)
+    | CaseL of {
+        term: expr;
+        nil: (Type.t[@name "ty"]) * expr;
+        cons: ((sugar_binder * sugar_binder) * (Type.t[@name "ty"])) * expr
+    }
     (* Sums *)
     | Inl of expr
     | Inr of expr
@@ -238,6 +246,23 @@ and pp_expr ppf expr_with_pos =
             (pp_print_comma_list Type.pp) ts
             pp_expr term
             pp_expr cont
+    | Nil -> pp_print_string ppf "Nil"
+    | Cons (e1, e2) ->
+        fprintf ppf "Cons %a %a" pp_expr e1 pp_expr e2
+    | CaseL { term; nil = (t1, e1); cons = (((b1, b2), t2), e2) } -> begin
+      match t1 with
+        | List t ->
+	          fprintf
+            ppf
+            "caseL %a of {@[@[nil: %a -> [@%a@]@]][cons %a %a -> [@%a@]@]@]]}"
+            pp_expr term
+            Type.pp t1
+            pp_expr e1
+            pp_bnd_ann (b1, t)
+            pp_bnd_ann (b2, t2)
+            pp_expr e2
+        | _ -> fprintf ppf "bad list"
+      end
     | Guard { target; pattern; guards; _ } ->
         fprintf ppf
             "guard %a : %a {@,@[<v 2>  %a@]@,}"
@@ -284,4 +309,3 @@ let substitute_solution sol =
         end
     in
     visitor#visit_program ()
-
diff --git a/lib/common/type.ml b/lib/common/type.ml
index 7e5097f..1f951af 100644
--- a/lib/common/type.ml
+++ b/lib/common/type.ml
@@ -253,6 +253,7 @@ type t =
     | Fun of { linear: bool; args: t list; result: t }
     | Tuple of t list
     | Sum of (t * t)
+    | List of t
     | Mailbox of {
         capability: (Capability.t [@name "capability"]);
         interface: string;
@@ -288,6 +289,7 @@ let rec contains_mailbox_type = function
     | Mailbox _ -> true
     | Sum (t1, t2) -> contains_mailbox_type t1 || contains_mailbox_type t2
     | Tuple ts -> List.exists contains_mailbox_type ts
+    | List t -> contains_mailbox_type t
     | _ -> false
 
 (* Easy constructors *)
@@ -325,6 +327,9 @@ let rec pp ppf =
         fprintf ppf "(%a + %a)"
             pp t1
             pp t2
+    | List t ->
+        fprintf ppf "[%a]"
+            pp t
     | Mailbox { capability; interface; pattern; quasilinearity } ->
         let ql =
             match quasilinearity with
@@ -358,6 +363,7 @@ let rec is_lin = function
     | Mailbox { capability = Out; pattern = Some One; _ } -> false
     | Tuple ts -> List.exists is_lin ts
     | Sum (t1, t2) -> is_lin t1 || is_lin t2
+    | List t -> is_lin t
     (* ...but otherwise a mailbox type must be used linearly. *)
     | Mailbox _ -> true
 
@@ -377,6 +383,10 @@ let is_sum = function
     | Sum _ -> true
     | _ -> false
 
+let is_list = function
+  | List _ -> true
+  | _ -> false
+
 let get_pattern = function
     | Mailbox { pattern = Some pat; _ } -> pat
     | _ -> raise (Errors.internal_error "type.ml" "attempted to get pattern of non-mailbox type")
@@ -394,12 +404,14 @@ let rec make_usable = function
     | Mailbox m -> Mailbox { m with quasilinearity = Quasilinearity.Usable }
     | Tuple ts -> Tuple (List.map make_usable ts)
     | Sum (t1, t2) -> Sum (make_usable t1, make_usable t2)
+    | List t -> List (make_usable t)
     | t -> t
 
 let rec make_returnable = function
     | Mailbox m -> Mailbox { m with quasilinearity = Quasilinearity.Returnable }
-    | Tuple ts -> Tuple (List.map make_returnable ts) 
+    | Tuple ts -> Tuple (List.map make_returnable ts)
     | Sum (t1, t2) -> Sum (make_returnable t1, make_returnable t2)
+    | List t -> List (make_returnable t)
     | t -> t
 
 let is_unr = is_lin >> not
@@ -409,6 +421,7 @@ let rec is_returnable = function
         ql = Quasilinearity.Returnable
     | Tuple ts -> List.for_all is_returnable ts
     | Sum  (t1, t2) -> is_returnable t1 && is_returnable t2
+    | List t -> is_returnable t
     | _ -> true
 
 let make_function_type linear args result =
@@ -420,3 +433,5 @@ let make_tuple_type tys =
 let make_sum_type ty1 ty2 =
     Sum (make_returnable ty1, make_returnable ty2)
 
+let make_list_type ty1 =
+    List (make_returnable ty1)
diff --git a/lib/frontend/insert_pattern_variables.ml b/lib/frontend/insert_pattern_variables.ml
index a18f9d6..af4d569 100644
--- a/lib/frontend/insert_pattern_variables.ml
+++ b/lib/frontend/insert_pattern_variables.ml
@@ -22,6 +22,8 @@ let rec annotate_type =
             Tuple (List.map annotate_type ts)
         | Sum (t1, t2) ->
             Sum (annotate_type t1, annotate_type t2)
+        | List t ->
+            List (annotate_type t)
         | Mailbox { pattern = Some _; _ } as mb -> mb
         | Mailbox { capability; interface; pattern = None; quasilinearity } ->
             Mailbox {
@@ -103,4 +105,3 @@ let annotate prog =
         Format.(fprintf std_formatter "=== Annotated Program ===\n%a\n\n"
         Sugar_ast.pp_program prog));
     prog
-
diff --git a/lib/frontend/lexer.mll b/lib/frontend/lexer.mll
index 2f3a4d9..3e55ff6 100644
--- a/lib/frontend/lexer.mll
+++ b/lib/frontend/lexer.mll
@@ -45,9 +45,12 @@ let keywords = [
     "if", IF;
     "else", ELSE;
     "case", CASE;
+    "caseL", CASEL;
     "of", OF;
     "inl", INL;
-    "inr", INR
+    "inr", INR;
+    "nil", NIL;
+    "cons", CONS
 ]
 }
 
diff --git a/lib/frontend/parser.mly b/lib/frontend/parser.mly
index 4c98479..68aa4e4 100644
--- a/lib/frontend/parser.mly
+++ b/lib/frontend/parser.mly
@@ -16,7 +16,7 @@ module ParserPosition
     (* parser position produced by Menhir *)
     type t = Lexpos.t * Lexpos.t
     (* Convert position produced by a parser to SourceCode position *)
-    let pos (start, finish) = 
+    let pos (start, finish) =
         let code = get_instance () in
         Position.make ~start ~finish ~code:code
     (* Wrapper around SourceCode.WithPos.make.  Accepts parser positions. *)
@@ -93,6 +93,9 @@ These will be added in later
 %token AND
 %token OR
 %token CASE
+%token CASEL
+%token NIL
+%token CONS
 %token OF
 %token INL
 %token INR
@@ -125,6 +128,12 @@ inl_branch:
 inr_branch:
     | INR LEFT_PAREN VARIABLE RIGHT_PAREN type_annot RIGHTARROW expr { (($3, $5), $7) }
 
+nil_branch:
+    | NIL type_annot RIGHTARROW expr { ($2, $4) }
+
+cons_branch:
+    | LEFT_PAREN VARIABLE CONS VARIABLE RIGHT_PAREN type_annot RIGHTARROW expr { ((($2, $4), $6), $8) }
+
 expr:
     (* Let *)
     | LET VARIABLE type_annot? EQ expr IN expr
@@ -152,6 +161,8 @@ basic_expr:
     | INR LEFT_PAREN expr RIGHT_PAREN { with_pos_from_positions $startpos $endpos ( Inr $3 )}
     | CASE expr OF LEFT_BRACE inl_branch PIPE inr_branch RIGHT_BRACE
         { with_pos_from_positions $startpos $endpos ( Case { term = $2; branch1 = $5; branch2 = $7} )}
+    | CASEL expr OF LEFT_BRACE nil_branch PIPE cons_branch RIGHT_BRACE
+        { with_pos_from_positions $startpos $endpos ( CaseL { term = $2; nil = $5; cons = $7} )}
     (* New *)
     | NEW LEFT_BRACK interface_name RIGHT_BRACK { with_pos_from_positions $startpos $endpos ( New $3 )}
     (* Spawn *)
@@ -161,21 +172,24 @@ basic_expr:
     (* Sugared Fail forms *)
     | FAIL LEFT_PAREN expr RIGHT_PAREN LEFT_BRACK ty RIGHT_BRACK { with_pos_from_positions $startpos $endpos ( SugarFail ($3, $6))}
     | tuple_exprs { with_pos_from_positions $startpos $endpos ( Tuple $1 ) }
+    | NIL { with_pos_from_positions $startpos $endpos ( Nil ) }
+    | LEFT_PAREN expr CONS expr RIGHT_PAREN { with_pos_from_positions $startpos $endpos ( Cons ($2, $4) ) }
+    (* | LEFT_BRACK expr RIGHT_BRACK { Cons ($2, Nil) } *)
     (* App *)
     | fact LEFT_PAREN expr_list RIGHT_PAREN
         { with_pos_from_positions $startpos $endpos (
             App {   func = with_pos_from_positions $startpos $endpos ($1);
-                    args = $3 } 
+                    args = $3 }
         )}
     (* Lam *)
     | linearity LEFT_PAREN annotated_var_list RIGHT_PAREN COLON ty LEFT_BRACE expr RIGHT_BRACE
         { with_pos_from_positions $startpos $endpos ( Lam { linear = $1; parameters = $3; result_type = $6; body = $8 } )}
     (* Send *)
-    | fact BANG message 
-        { with_pos_from_positions $startpos $endpos( 
-            Send {  target = with_pos_from_positions $startpos $endpos ($1); 
-                    message = $3; 
-                    iname = None 
+    | fact BANG message
+        { with_pos_from_positions $startpos $endpos(
+            Send {  target = with_pos_from_positions $startpos $endpos ($1);
+                    message = $3;
+                    iname = None
             }
         )}
     (* If-Then-Else *)
@@ -275,7 +289,7 @@ simple_pat:
             match $1 with
                 | 0 -> Type.Pattern.Zero
                 | 1 -> Type.Pattern.One
-                | _ -> raise (parse_error "Invalid pattern: expected 0 or 1." 
+                | _ -> raise (parse_error "Invalid pattern: expected 0 or 1."
                                 [Position.make ~start:$startpos ~finish:$endpos ~code:!source_code_instance])
         }
     | LEFT_PAREN pat RIGHT_PAREN { $2 }
@@ -285,7 +299,7 @@ ql:
         match $2 with
             | "R" -> Type.Quasilinearity.Returnable
             | "U" -> Type.Quasilinearity.Usable
-            | _ -> raise (parse_error "Invalid usage: expected U or R." 
+            | _ -> raise (parse_error "Invalid usage: expected U or R."
                             [Position.make ~start:$startpos ~finish:$endpos ~code:!source_code_instance])
     }
 
@@ -316,6 +330,7 @@ mailbox_ty:
 simple_ty:
     | mailbox_ty { $1 }
     | base_ty { $1 }
+    | LEFT_BRACK simple_ty RIGHT_BRACK { Type.make_list_type $2 }
 
 base_ty:
     | CONSTRUCTOR {
@@ -342,13 +357,13 @@ annotated_var_list:
     | separated_list(COMMA, annotated_var)  { $1 }
 
 interface:
-    | INTERFACE interface_name LEFT_BRACE message_list RIGHT_BRACE 
+    | INTERFACE interface_name LEFT_BRACE message_list RIGHT_BRACE
         { with_pos_from_positions $startpos $endpos ( Interface.make $2 $4)  }
 
 decl:
     | DEF VARIABLE LEFT_PAREN annotated_var_list RIGHT_PAREN COLON ty LEFT_BRACE expr
     RIGHT_BRACE {
-        with_pos_from_positions $startpos $endpos ( 
+        with_pos_from_positions $startpos $endpos (
         {
           decl_name = $2;
           decl_parameters = $4;
diff --git a/lib/frontend/sugar_to_ir.ml b/lib/frontend/sugar_to_ir.ml
index 38e31a4..61abaa1 100644
--- a/lib/frontend/sugar_to_ir.ml
+++ b/lib/frontend/sugar_to_ir.ml
@@ -55,7 +55,7 @@ let rec transform_prog :
     let (bnds, env') = add_names env (fun d -> d.Sugar_ast.decl_name) nodes in
     {
         prog_interfaces;
-        prog_decls = WithPos.combine_with_pos_list poses 
+        prog_decls = WithPos.combine_with_pos_list poses
                     (List.map (fun (b, d) -> transform_decl env' d b id) (List.combine bnds nodes));
         prog_body =
             match prog_body with
@@ -139,6 +139,11 @@ and transform_expr :
         | Tuple es ->
             transform_exprs env es (fun _ vs ->
                 with_same_pos (Ir.Return (with_same_pos (Ir.Tuple vs))) |> k env)
+        | Nil -> Ir.Return (Ir.Nil) |> k env
+        | Cons (e1, e2) ->
+            transform_subterm env e1 (fun _ v1 ->
+            transform_subterm env e2 (fun _ v2 ->
+                Ir.Return (Ir.Cons (v1, v2)) |> k env))
         | LetTuple {binders = bs; term; cont; _ } ->
             (* let x = M in N*)
             (* Create IR variables based on the binders *)
@@ -168,6 +173,19 @@ and transform_expr :
                     branch1 = (ir_bnd1, ty1), (transform_expr env1 comp1 id);
                     branch2 = (ir_bnd2, ty2), (transform_expr env2 comp2 id);
                 }) |> k env)
+        | CaseL {
+            term;
+            nil = (ty1, comp1);
+            cons = (((bnd1, bnd2), ty2), comp2) } ->
+            transform_subterm env term (fun env v ->
+                let (ir_bnd1, env1) = add_name env bnd1 in
+                let (ir_bnd2, env2) = add_name env1 bnd2 in
+                with_same_pos (
+                Ir.CaseL {
+                    term = v;
+                    nil = ty1, (transform_expr env comp1 id);
+                    cons = ((ir_bnd1, ir_bnd2), ty2), (transform_expr env2 comp2 id);
+                }) |> k env)
         | Seq (e1, e2) ->
             transform_expr env e1 (fun env c1 ->
             let pos' = WithPos.pos c1 in
diff --git a/lib/typecheck/gen_constraints.ml b/lib/typecheck/gen_constraints.ml
index 210cdeb..e3c69c5 100644
--- a/lib/typecheck/gen_constraints.ml
+++ b/lib/typecheck/gen_constraints.ml
@@ -117,7 +117,7 @@ let rec synthesise_val :
                     (* Finally, ensure that the declared type is a subtype of
                        the inferred type *)
                     List.fold_left (fun acc (inferred, declared) ->
-                        Constraint_set.union acc (subtype ienv declared inferred pos)) 
+                        Constraint_set.union acc (subtype ienv declared inferred pos))
                         Constraint_set.empty
                         zipped
                 in
@@ -167,6 +167,8 @@ and check_val :
             | Sum (t1, t2), PSum (pt1, pt2) ->
                 check_pretype_consistency t1 pt1;
                 check_pretype_consistency t2 pt2
+            | List t, PList pt ->
+                check_pretype_consistency t pt
             | _, _ -> Gripers.pretype_consistency ty pty [pos]
     in
     match WithPos.node v with
@@ -191,6 +193,22 @@ and check_val :
                         check_val ienv decl_env v (Type.make_returnable t2)
                     | _ -> Gripers.expected_sum_type ty [pos]
             end
+        | Nil ->
+            begin
+                match ty with
+                    | Type.List _ -> Ty_env.empty, Constraint_set.empty
+                    | _ -> Gripers.expected_list_type ty
+            end
+        | Cons (v1, v2) ->
+            begin
+                match ty with
+                    | Type.List t ->
+                        let (env1, constrs1) = check_val ienv decl_env v1 t in
+                        let (env2, constrs2) = check_val ienv decl_env v2 ty in
+                        let env, constrs3 = Ty_env.combine ienv env1 env2 in
+                        env, Constraint_set.union_many [constrs1; constrs2; constrs3]
+                    | _ -> Gripers.expected_sum_type ty
+            end
         | Tuple vs ->
             let ts =
                 begin
@@ -360,7 +378,7 @@ and synthesise_comp :
                         in
                         let () =
                             if Type.is_lin binder_ty then
-                                Gripers.unused_synthesised_linear_var 
+                                Gripers.unused_synthesised_linear_var
                                 binder_var binder_ty [pos]
                         in
                         let (env, env_constrs) =
@@ -440,6 +458,33 @@ and check_comp : IEnv.t -> Ty_env.t -> Ir.comp -> Type.t -> Ty_env.t * Constrain
                       env2_constrs; isect_constrs; env_constrs; term_constrs ]
             in
             (env, constrs)
+        | CaseL { term; nil = (ty1, comp1); cons = (((bnd1, bnd2), ty2), comp2) } ->
+            let (term_env, term_constrs) =
+                check_val ienv decl_env term ty1
+            in
+            let var1 = Var.of_binder bnd1 in
+            let var2 = Var.of_binder bnd2 in
+            (* Check both branches, and check that inferred types match annotations *)
+            let (comp1_env, comp1_constrs) = chk comp1 ty in
+            let (comp2_env, comp2_constrs) = chk comp2 ty in
+            let env1_constrs = Ty_env.check_type ienv var1 ty1 comp1_env in
+            let env2_constrs = Ty_env.check_type ienv var2 ty2 comp2_env in
+            (* Calculate merge of the branches (sans binders) *)
+            let isect_env, isect_constrs =
+                Ty_env.intersect
+                    (Ty_env.delete var1 comp1_env)
+                    (Ty_env.delete var2 comp2_env)
+            in
+            (* Finally join the term env with the intersected env *)
+            let env, env_constrs =
+                Ty_env.join ienv term_env isect_env
+            in
+            let constrs =
+                Constraint_set.union_many
+                    [ comp1_constrs; comp2_constrs; env1_constrs;
+                      env2_constrs; isect_constrs; env_constrs; term_constrs ]
+            in
+            (env, constrs)
         | Seq (e1, e2) ->
             (* Check e1 has type unit, check body type *)
             let (e1_env, e1_constrs) = chk e1 Type.unit_type in
@@ -803,7 +848,7 @@ and check_guard :
                                 match ty with
                                     | Mailbox { interface; _ } when (List.mem interface mb_iface_tys) ->
                                         Gripers.duplicate_interface_receive_env
-                                        v interface 
+                                        v interface
                                         [pos]
                                     | _ -> ()
                             ) env
diff --git a/lib/typecheck/gripers.ml b/lib/typecheck/gripers.ml
index e5434db..cefc40f 100644
--- a/lib/typecheck/gripers.ml
+++ b/lib/typecheck/gripers.ml
@@ -142,7 +142,7 @@ let unused_parameter v fn_name ty pos_list =
             v fn_name Type.pp ty
     in
     raise (constraint_gen_error ~subsystem:(Errors.GenCheckDecls) msg pos_list )
-   
+
 
 let subtype_linearity_mismatch t1 t2 pos_list =
     let msg =
@@ -274,6 +274,14 @@ let expected_sum_type instead pos_list =
     in
     raise (constraint_gen_error ~subsystem:Errors.GenCheck msg pos_list)
 
+let expected_list_type instead pos_list =
+    let msg =
+        Format.asprintf
+            "Expected a list type, but got %a."
+            Type.pp instead
+    in
+    raise (constraint_gen_error ~subsystem:Errors.GenCheck msg pos_list)
+
 
 let invalid_ql_sequencing var pos_list =
     let msg =
@@ -303,7 +311,7 @@ let let_not_returnable ty pos_list =
             "The subject of a let-binding must be returnable. However, type %a is only usable."
             Type.pp ty
     in
-    raise (constraint_gen_error ~subsystem:Errors.GenCheck msg pos_list) 
+    raise (constraint_gen_error ~subsystem:Errors.GenCheck msg pos_list)
 
 let duplicate_interface_receive_env var iface pos_list =
     let msg =
@@ -322,5 +330,3 @@ let pretype_consistency ty pty pos_list =
             Pretype.pp pty
     in
     raise (constraint_gen_error ~subsystem:Errors.GenCheck msg pos_list)
-
-
diff --git a/lib/typecheck/pretypecheck.ml b/lib/typecheck/pretypecheck.ml
index 61bbb0d..fd03d28 100644
--- a/lib/typecheck/pretypecheck.ml
+++ b/lib/typecheck/pretypecheck.ml
@@ -8,7 +8,7 @@ open Ir
 open Util.Utility
 open Source_code
 
-let pretype_error msg pos_list = Errors.Pretype_error (msg,pos_list) 
+let pretype_error msg pos_list = Errors.Pretype_error (msg,pos_list)
 
 module Gripers = struct
     open Format
@@ -16,7 +16,7 @@ module Gripers = struct
     let arity_error pos expected_len actual_len =
         let msg =
             asprintf "Arity error. Expects %d arguments, but %d were provided."
-                expected_len 
+                expected_len
                 actual_len
         in
         raise (pretype_error msg [pos])
@@ -24,7 +24,7 @@ module Gripers = struct
     let tuple_arity_error pos expected_len actual_len =
         let msg =
             asprintf "Arity error. Tuple deconstructor has %d binders, but tuple has %d components."
-                expected_len 
+                expected_len
                 actual_len
         in
         raise (pretype_error msg [pos])
@@ -44,7 +44,7 @@ module Gripers = struct
 
     let type_mismatch pos_list expected actual =
         let msg =
-            asprintf "Type mismatch. Expected %a but got %a."                
+            asprintf "Type mismatch. Expected %a but got %a."
                 Pretype.pp expected
                 Pretype.pp actual
         in
@@ -52,7 +52,7 @@ module Gripers = struct
 
     let type_mismatch_with_expected pos expected_msg actual =
         let msg =
-            asprintf "Type mismatch. Expected %s but got %a."                
+            asprintf "Type mismatch. Expected %s but got %a."
                 expected_msg
                 Pretype.pp actual
         in
@@ -60,7 +60,7 @@ module Gripers = struct
 
     let cannot_synth_empty_guards pos () =
         let msg =
-            asprintf "Need at least one non-fail guard to synthesise the type for a 'guard' expression." 
+            asprintf "Need at least one non-fail guard to synthesise the type for a 'guard' expression."
         in
         raise (pretype_error msg [pos])
 
@@ -77,6 +77,15 @@ module Gripers = struct
                 Ir.pp_value term
         in
         raise (pretype_error msg [pos])
+
+    let cannot_synth_nil (term: value) =
+        let pos = WithPos.pos term in
+        let msg =
+            asprintf
+                "Cannot synthesise a type for an empty list %a"
+                Ir.pp_value term
+        in
+        raise (pretype_error msg [pos])
 end
 
 (* Note: This basically works since we only have mailbox subtyping at present.
@@ -140,6 +149,10 @@ let rec synthesise_val ienv env value : (value * Pretype.t) =
             let vs_and_tys = List.map (synthesise_val ienv env) vs in
             let (vs, tys) = List.split vs_and_tys in
             wrap (Tuple vs), Pretype.PTuple tys
+        | Cons (v1, v2) ->
+            let (v1, ty1) = synthesise_val ienv env v1 in
+            let (v2, _) = synthesise_val ienv env v2 in
+            wrap (Cons (v1, v2)), Pretype.PList ty1
         | Lam { linear; parameters; result_type; body } ->
             (* Defer linearity checking to constraint generation. *)
             let param_types  = List.map snd parameters in
@@ -158,6 +171,7 @@ let rec synthesise_val ienv env value : (value * Pretype.t) =
                 result = result_prety
             }
         | Inl _ | Inr _ -> Gripers.cannot_synth_sum value
+        | Nil -> Gripers.cannot_synth_nil value
 and check_val ienv env value ty =
     let (value_node, pos) = WithPos.(node value, pos value) in
     let wrap = WithPos.make ~pos in
@@ -172,6 +186,12 @@ and check_val ienv env value ty =
             raise
                 (Gripers.type_mismatch_with_expected pos
                     "a sum type" ty)
+        | Nil, (Pretype.PList _) ->
+          Nil
+        | Nil, ty ->
+          raise
+            (Gripers.type_mismatch_with_expected
+              "a list type" ty)
         | _ ->
             let value, inferred_ty = synthesise_val ienv env value in
             check_tys [pos] ty inferred_ty;
@@ -248,6 +268,27 @@ and synthesise_comp ienv env comp =
             let cont, cont_ty = synthesise_comp ienv env' cont in
             WithPos.make ~pos
                 (LetTuple { binders; tuple; cont }), cont_ty
+        | CaseL { term; nil = (ty1, e1); cons = (((bnd1, bnd2), ty2), e2) } ->
+            let prety1 = Pretype.of_type ty1 in
+            let prety2 = Pretype.of_type ty2 in
+            let term =
+              check_val ienv env term prety2
+            in
+            let ty3 = match prety1 with
+              | Pretype.PList ty3 -> ty3
+              | _ -> raise (Gripers.type_mismatch_with_expected "a list type" prety1)
+            in
+            let b1_env = PretypeEnv.bind (Var.of_binder bnd1) ty3 env in
+            let b2_env = PretypeEnv.bind (Var.of_binder bnd2) prety1 b1_env in
+            let e2, b2_ty = synthesise_comp ienv b2_env e2 in
+            let e1 = check_comp ienv b2_env e1 b2_ty in
+            WithPos.make ~pos
+              (CaseL { term; nil = (ty1, e1); cons = (((bnd1, bnd2), ty2), e2) }), b2_ty
+        | LetPair { binders = ((b1, _), (b2, _)); pair; cont } ->
+            let pair, pair_ty = synthv pair in
+            let (t1, t2) =
+                match pair_ty with
+                    | Pretype.PPair (t1, t2) -> (t1, t2)
         | Seq (e1, e2) ->
             let e1 = check_comp ienv env e1 (Pretype.unit) in
             let e2, e2_ty = synth e2 in
diff --git a/lib/typecheck/ty_env.ml b/lib/typecheck/ty_env.ml
index 0233ed0..0eb8661 100644
--- a/lib/typecheck/ty_env.ml
+++ b/lib/typecheck/ty_env.ml
@@ -97,6 +97,32 @@ let join : Interface_env.t -> t -> t -> Position.t -> t * Constraint_set.t =
                               pattern = Some pat;
                               quasilinearity = ql
                           }, constrs
+                | List (Mailbox { capability = cap1; interface = iface1; pattern =
+                    Some pat1; quasilinearity = ql1 }),
+                  List (Mailbox { capability = cap2; interface = iface2; pattern =
+                      Some pat2; quasilinearity = ql2 }) ->
+                      (* We can only join variables with the same interface
+                         name. If these match, we can join the types. *)
+                      if iface1 <> iface2 then
+                          Gripers.env_interface_mismatch true
+                            t1 t2 var iface1 iface2
+                      else
+                          (* Check sequencing of QL *)
+                          let ql =
+                              match Quasilinearity.sequence ql1 ql2 with
+                                | Some ql -> ql
+                                | None ->
+                                    Gripers.invalid_ql_sequencing var
+                          in
+                          let ((cap, pat), constrs) =
+                              join_mailbox_types var
+                                (cap1, pat1) (cap2, pat2) in
+                          Mailbox {
+                              capability = cap;
+                              interface = iface1;
+                              pattern = Some pat;
+                              quasilinearity = ql
+                          }, constrs
                 | _, _ ->
                     Gripers.type_mismatch true t1 t2 var [pos]
         in
@@ -226,6 +252,25 @@ let intersect : t -> t -> Position.t -> t * Constraint_set.t =
                               (* Must take strongest QL across all branches. *)
                               quasilinearity = Quasilinearity.max ql1 ql2
                           }, constrs
+                | List (Mailbox { capability = cap1; interface = iface1; pattern =
+                    Some pat1; quasilinearity = ql1 }),
+                  List (Mailbox { capability = cap2; interface = iface2; pattern =
+                      Some pat2; quasilinearity = ql2 }) ->
+                      (* As before -- interface names must be the same*)
+                      if iface1 <> iface2 then
+                          Gripers.env_interface_mismatch
+                            false t1 t2 var iface1 iface2
+                      else
+                          let ((cap, pat), constrs) =
+                              intersect_mailbox_types var
+                                (cap1, pat1) (cap2, pat2) in
+                          Mailbox {
+                              capability = cap;
+                              interface = iface1;
+                              pattern = Some pat;
+                              (* Must take strongest QL across all branches. *)
+                              quasilinearity = Quasilinearity.max ql1 ql2
+                          }, constrs
                 | _, _ ->
                     Gripers.type_mismatch false t1 t2 var [pos]
         in
@@ -313,4 +358,3 @@ let make_unrestricted env pos =
     List.fold_left (fun acc (_, ty) ->
         Constraint_set.union acc (make_unrestricted ty pos)
     ) Constraint_set.empty (bindings env)
-
diff --git a/lib/typecheck/type_utils.ml b/lib/typecheck/type_utils.ml
index 8c41d0b..e413a80 100644
--- a/lib/typecheck/type_utils.ml
+++ b/lib/typecheck/type_utils.ml
@@ -14,6 +14,7 @@ let make_unrestricted t pos =
         (* Trivially unrestricted *)
         | Base _
         | Tuple []
+        | List _
         | Fun { linear = false; _ } -> Constraint_set.empty
         (* Must be unrestricted *)
         | Fun { linear = true; _ }
@@ -42,12 +43,13 @@ let rec subtype_type :
             (* Subtyping covariant for tuples and sums *)
             | Tuple tyas, Tuple tybs ->
                 Constraint_set.union_many
-                    (List.map (fun (tya, tyb) -> subtype_type visited ienv tya tyb pos) 
+                    (List.map (fun (tya, tyb) -> subtype_type visited ienv tya tyb pos)
                         (List.combine tyas tybs))
             | Sum (tya1, tya2), Sum (tyb1, tyb2) ->
                 Constraint_set.union
                     (subtype_type visited ienv tya1 tyb1 pos)
                     (subtype_type visited ienv tya2 tyb2 pos)
+            | List ty1, List ty2 -> subtype_type visited ienv ty1 ty2 pos
             | Mailbox { pattern = None; _ }, _
             | _, Mailbox { pattern = None; _ } ->
                     (* Should have been sorted by annotation pass *)
diff --git a/test/examples/savina/kfork.pat b/test/examples/savina/kfork.pat
index 3f96ed4..3c40cfb 100644
--- a/test/examples/savina/kfork.pat
+++ b/test/examples/savina/kfork.pat
@@ -1,9 +1,8 @@
 ### Adapted from Savina/fjthrput.
 ###
-### Models the creation of n actors that are given a number of messages, for 
+### Models the creation of n actors that are given a number of messages, for
 ### each of which, a computation is performed. The benchmark is parameterized by
-### the number of actor processes. Since the array type is not available in 
-### Pat, we fix the number of actor processes to 3.
+### the number of actor processes.
 
 interface ActorMb {
   Packet()
@@ -26,7 +25,7 @@ def fact(n: Int): Int {
     1
   }
   else {
-    n * (fact(n - 1)) 
+    n * (fact(n - 1))
   }
 }
 
@@ -41,21 +40,31 @@ def flood(numMessages: Int, actorMb: ActorMb!): Unit {
   }
 }
 
-## Launcher.
-def main(): Unit {
-  
-  let actorMb1 = new [ActorMb] in
-  spawn { actor(actorMb1) };
+def spawnActors(numActors: Int, acc: [ActorMb!]): [ActorMb!] {
+    if (numActors <= 0) {
+        acc
+    }
+    else {
+        let newActor = new [ActorMb] in
+            spawn { actor(newActor) };
+            spawnActors(numActors - 1, (newActor cons acc))
+        }
+}
 
-  let actorMb2 = new [ActorMb] in
-  spawn { actor(actorMb2) };
+def floodActors(numMessages: Int, actorMbs: [ActorMb!]): Unit {
+    caseL actorMbs of {
+        nil : [ActorMb!] -> ()
+      | (a cons as) : [ActorMb!] ->
+            flood(numMessages, a);
+            floodActors(numMessages, as)
+        }
+}
 
-  let actorMb3 = new [ActorMb] in
-  spawn { actor(actorMb3) };
+## Launcher.
+def main(numActors: Int): Unit {
 
-  flood(100, actorMb1);
-  flood(1000, actorMb1);
-  flood(10000, actorMb1)
+  let actorMbs = spawnActors(numActors, (nil : [ActorMb!])) in
+    floodActors(1000, actorMbs)
 }
 
-main()
+main(3)
diff --git a/test/pat-tests/list-1.pat b/test/pat-tests/list-1.pat
new file mode 100644
index 0000000..a89c68f
--- /dev/null
+++ b/test/pat-tests/list-1.pat
@@ -0,0 +1,9 @@
+def main(): Unit {
+    let xs = (5 cons (nil : [Int])) in
+    caseL xs of {
+          nil : [Int] -> print("nil")
+        | (y cons ys) : [Int] -> print(intToString(y))
+    }
+}
+
+main()
diff --git a/test/pat-tests/list-2.pat b/test/pat-tests/list-2.pat
new file mode 100644
index 0000000..0bae0e6
--- /dev/null
+++ b/test/pat-tests/list-2.pat
@@ -0,0 +1,23 @@
+def snoc(xs : [Int], x : Int): [Int] {
+    caseL xs of {
+        nil : [Int] -> (x cons (nil : [Int]))
+      | (y cons ys) : [Int] -> (y cons snoc(ys, x))
+    }
+}
+
+def reverse(xs : [Int]): [Int] {
+    caseL xs of {
+          nil : [Int] -> nil
+        | (y cons ys) : [Int] -> snoc(reverse(ys), y)
+    }
+}
+
+def main(): Unit {
+    let xs = (1 cons (2 cons (3 cons (nil : [Int])))) in
+    caseL reverse(xs) of {
+        nil : [Int] -> print("nil")
+      | (y cons ys) : [Int] -> print(intToString(y))
+  }
+}
+
+main()

From 3dd4d098ad26f217c3b79e0d92ea135b37cc4f6d Mon Sep 17 00:00:00 2001
From: Danielle Marshall <danielle@starsandspira.ls>
Date: Wed, 19 Mar 2025 14:05:09 +0000
Subject: [PATCH 02/33] fix pattern variable annotation bug

---
 lib/frontend/insert_pattern_variables.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/lib/frontend/insert_pattern_variables.ml b/lib/frontend/insert_pattern_variables.ml
index af4d569..bf07240 100644
--- a/lib/frontend/insert_pattern_variables.ml
+++ b/lib/frontend/insert_pattern_variables.ml
@@ -33,7 +33,7 @@ let rec annotate_type =
                 quasilinearity
             }
 
-let annotate_interface_type = 
+let annotate_interface_type =
     let open Type in
     function
         (* Outermost MB types (i.e., payloads) are treated as usable. *)

From dfdd31084d557e4c429865996f45db551711ba13 Mon Sep 17 00:00:00 2001
From: Danielle Marshall <danielle@starsandspira.ls>
Date: Wed, 19 Mar 2025 14:09:16 +0000
Subject: [PATCH 03/33] fix free variable not being deleted

---
 lib/typecheck/gen_constraints.ml | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

diff --git a/lib/typecheck/gen_constraints.ml b/lib/typecheck/gen_constraints.ml
index e3c69c5..668017b 100644
--- a/lib/typecheck/gen_constraints.ml
+++ b/lib/typecheck/gen_constraints.ml
@@ -472,8 +472,8 @@ and check_comp : IEnv.t -> Ty_env.t -> Ir.comp -> Type.t -> Ty_env.t * Constrain
             (* Calculate merge of the branches (sans binders) *)
             let isect_env, isect_constrs =
                 Ty_env.intersect
-                    (Ty_env.delete var1 comp1_env)
-                    (Ty_env.delete var2 comp2_env)
+                  comp1_env
+                  (Ty_env.delete var1 (Ty_env.delete var2 comp2_env))
             in
             (* Finally join the term env with the intersected env *)
             let env, env_constrs =
@@ -913,7 +913,11 @@ let check_decls ienv decls =
     (* List of allowed free names: all declaration names. Primitive names won't
      get added into the environment at all. *)
     let allowed_free_names =
+<<<<<<< HEAD
         List.map (fun d -> Var.of_binder d.decl_name) decl_nodes
+=======
+        List.map (fun d -> Var.of_binder d.decl_name) decls
+>>>>>>> e081ef2 (fix free variable not being deleted)
     in
     let decl_env =
         let decl_entry d =

From 6c909857c10a580d26f6c12bb1c6de7f2feb950c Mon Sep 17 00:00:00 2001
From: Danielle Marshall <danielle@starsandspira.ls>
Date: Wed, 19 Mar 2025 14:19:59 +0000
Subject: [PATCH 04/33] add broken list example for testing

---
 test/pat-tests/list-broken.pat | 16 ++++++++++++++++
 1 file changed, 16 insertions(+)
 create mode 100644 test/pat-tests/list-broken.pat

diff --git a/test/pat-tests/list-broken.pat b/test/pat-tests/list-broken.pat
new file mode 100644
index 0000000..a5cef84
--- /dev/null
+++ b/test/pat-tests/list-broken.pat
@@ -0,0 +1,16 @@
+interface Test {
+  Ping()
+}
+
+def spawnMbs(acc : [Test!]) : [Test!] {
+    acc
+}
+
+def test(mbs : [Test!]) : Unit {
+    ()
+}
+
+def main() : Unit {
+    let mbs = spawnMbs(nil : [Test!]) in
+    test(mbs)
+}

From 6e6c1657cf0be70bfb57bbfdee5bda852749ff01 Mon Sep 17 00:00:00 2001
From: Danielle Marshall <danielle@starsandspira.ls>
Date: Wed, 19 Mar 2025 15:00:06 +0000
Subject: [PATCH 05/33] reconcile lists with tuples and error locs

---
 lib/common/pretype.ml            |  4 ----
 lib/frontend/sugar_to_ir.ml      |  4 ++--
 lib/typecheck/gen_constraints.ml | 18 +++++++-----------
 lib/typecheck/pretypecheck.ml    | 11 +++--------
 lib/typecheck/ty_env.ml          |  8 ++++----
 5 files changed, 16 insertions(+), 29 deletions(-)

diff --git a/lib/common/pretype.ml b/lib/common/pretype.ml
index febf2b7..171d3a1 100644
--- a/lib/common/pretype.ml
+++ b/lib/common/pretype.ml
@@ -14,12 +14,8 @@ type t =
     | PFun of { linear: bool; args: (Type.t[@name "ty"]) list; result: t[@name "pretype"] }
     | PInterface of string
     | PSum of (t * t)
-<<<<<<< HEAD
     | PTuple of t list
-=======
-    | PPair of (t * t)
     | PList of t
->>>>>>> f735eea (wip: add lists)
     [@@name "pretype"]
     [@@deriving visitors { variety = "map" }]
 and base = [%import: Common_types.Base.t]
diff --git a/lib/frontend/sugar_to_ir.ml b/lib/frontend/sugar_to_ir.ml
index 61abaa1..957ec05 100644
--- a/lib/frontend/sugar_to_ir.ml
+++ b/lib/frontend/sugar_to_ir.ml
@@ -139,11 +139,11 @@ and transform_expr :
         | Tuple es ->
             transform_exprs env es (fun _ vs ->
                 with_same_pos (Ir.Return (with_same_pos (Ir.Tuple vs))) |> k env)
-        | Nil -> Ir.Return (Ir.Nil) |> k env
+        | Nil -> with_same_pos (Ir.Return (with_same_pos (Ir.Nil))) |> k env
         | Cons (e1, e2) ->
             transform_subterm env e1 (fun _ v1 ->
             transform_subterm env e2 (fun _ v2 ->
-                Ir.Return (Ir.Cons (v1, v2)) |> k env))
+                with_same_pos (Ir.Return (with_same_pos (Ir.Cons (v1, v2)))) |> k env))
         | LetTuple {binders = bs; term; cont; _ } ->
             (* let x = M in N*)
             (* Create IR variables based on the binders *)
diff --git a/lib/typecheck/gen_constraints.ml b/lib/typecheck/gen_constraints.ml
index 668017b..4ebca0f 100644
--- a/lib/typecheck/gen_constraints.ml
+++ b/lib/typecheck/gen_constraints.ml
@@ -197,7 +197,7 @@ and check_val :
             begin
                 match ty with
                     | Type.List _ -> Ty_env.empty, Constraint_set.empty
-                    | _ -> Gripers.expected_list_type ty
+                    | _ -> Gripers.expected_list_type ty [pos]
             end
         | Cons (v1, v2) ->
             begin
@@ -205,9 +205,9 @@ and check_val :
                     | Type.List t ->
                         let (env1, constrs1) = check_val ienv decl_env v1 t in
                         let (env2, constrs2) = check_val ienv decl_env v2 ty in
-                        let env, constrs3 = Ty_env.combine ienv env1 env2 in
+                        let env, constrs3 = Ty_env.combine ienv env1 env2 pos in
                         env, Constraint_set.union_many [constrs1; constrs2; constrs3]
-                    | _ -> Gripers.expected_sum_type ty
+                    | _ -> Gripers.expected_list_type ty [pos]
             end
         | Tuple vs ->
             let ts =
@@ -467,17 +467,17 @@ and check_comp : IEnv.t -> Ty_env.t -> Ir.comp -> Type.t -> Ty_env.t * Constrain
             (* Check both branches, and check that inferred types match annotations *)
             let (comp1_env, comp1_constrs) = chk comp1 ty in
             let (comp2_env, comp2_constrs) = chk comp2 ty in
-            let env1_constrs = Ty_env.check_type ienv var1 ty1 comp1_env in
-            let env2_constrs = Ty_env.check_type ienv var2 ty2 comp2_env in
+            let env1_constrs = Ty_env.check_type ienv var1 ty1 comp1_env pos in
+            let env2_constrs = Ty_env.check_type ienv var2 ty2 comp2_env pos in
             (* Calculate merge of the branches (sans binders) *)
             let isect_env, isect_constrs =
                 Ty_env.intersect
                   comp1_env
-                  (Ty_env.delete var1 (Ty_env.delete var2 comp2_env))
+                  (Ty_env.delete var1 (Ty_env.delete var2 comp2_env)) pos
             in
             (* Finally join the term env with the intersected env *)
             let env, env_constrs =
-                Ty_env.join ienv term_env isect_env
+                Ty_env.join ienv term_env isect_env pos
             in
             let constrs =
                 Constraint_set.union_many
@@ -913,11 +913,7 @@ let check_decls ienv decls =
     (* List of allowed free names: all declaration names. Primitive names won't
      get added into the environment at all. *)
     let allowed_free_names =
-<<<<<<< HEAD
         List.map (fun d -> Var.of_binder d.decl_name) decl_nodes
-=======
-        List.map (fun d -> Var.of_binder d.decl_name) decls
->>>>>>> e081ef2 (fix free variable not being deleted)
     in
     let decl_env =
         let decl_entry d =
diff --git a/lib/typecheck/pretypecheck.ml b/lib/typecheck/pretypecheck.ml
index fd03d28..ec3f030 100644
--- a/lib/typecheck/pretypecheck.ml
+++ b/lib/typecheck/pretypecheck.ml
@@ -187,10 +187,10 @@ and check_val ienv env value ty =
                 (Gripers.type_mismatch_with_expected pos
                     "a sum type" ty)
         | Nil, (Pretype.PList _) ->
-          Nil
+          wrap Nil
         | Nil, ty ->
           raise
-            (Gripers.type_mismatch_with_expected
+            (Gripers.type_mismatch_with_expected pos
               "a list type" ty)
         | _ ->
             let value, inferred_ty = synthesise_val ienv env value in
@@ -276,7 +276,7 @@ and synthesise_comp ienv env comp =
             in
             let ty3 = match prety1 with
               | Pretype.PList ty3 -> ty3
-              | _ -> raise (Gripers.type_mismatch_with_expected "a list type" prety1)
+              | _ -> raise (Gripers.type_mismatch_with_expected pos "a list type" prety1)
             in
             let b1_env = PretypeEnv.bind (Var.of_binder bnd1) ty3 env in
             let b2_env = PretypeEnv.bind (Var.of_binder bnd2) prety1 b1_env in
@@ -284,11 +284,6 @@ and synthesise_comp ienv env comp =
             let e1 = check_comp ienv b2_env e1 b2_ty in
             WithPos.make ~pos
               (CaseL { term; nil = (ty1, e1); cons = (((bnd1, bnd2), ty2), e2) }), b2_ty
-        | LetPair { binders = ((b1, _), (b2, _)); pair; cont } ->
-            let pair, pair_ty = synthv pair in
-            let (t1, t2) =
-                match pair_ty with
-                    | Pretype.PPair (t1, t2) -> (t1, t2)
         | Seq (e1, e2) ->
             let e1 = check_comp ienv env e1 (Pretype.unit) in
             let e2, e2_ty = synth e2 in
diff --git a/lib/typecheck/ty_env.ml b/lib/typecheck/ty_env.ml
index 0eb8661..a1591fa 100644
--- a/lib/typecheck/ty_env.ml
+++ b/lib/typecheck/ty_env.ml
@@ -18,7 +18,7 @@ let lookup_opt = VarMap.find_opt
 let delete = VarMap.remove
 
 let delete_many vars env =
-    List.fold_right (delete) vars env 
+    List.fold_right (delete) vars env
 
 let delete_binder x = VarMap.remove (Ir.Var.of_binder x)
 let singleton = VarMap.singleton
@@ -105,14 +105,14 @@ let join : Interface_env.t -> t -> t -> Position.t -> t * Constraint_set.t =
                          name. If these match, we can join the types. *)
                       if iface1 <> iface2 then
                           Gripers.env_interface_mismatch true
-                            t1 t2 var iface1 iface2
+                            t1 t2 var iface1 iface2 [pos]
                       else
                           (* Check sequencing of QL *)
                           let ql =
                               match Quasilinearity.sequence ql1 ql2 with
                                 | Some ql -> ql
                                 | None ->
-                                    Gripers.invalid_ql_sequencing var
+                                    Gripers.invalid_ql_sequencing var [pos]
                           in
                           let ((cap, pat), constrs) =
                               join_mailbox_types var
@@ -259,7 +259,7 @@ let intersect : t -> t -> Position.t -> t * Constraint_set.t =
                       (* As before -- interface names must be the same*)
                       if iface1 <> iface2 then
                           Gripers.env_interface_mismatch
-                            false t1 t2 var iface1 iface2
+                            false t1 t2 var iface1 iface2 [pos]
                       else
                           let ((cap, pat), constrs) =
                               intersect_mailbox_types var

From be16dbde92045b91fc1b80d8a9c4cce49b5ad89d Mon Sep 17 00:00:00 2001
From: Danielle Marshall <danielle@starsandspira.ls>
Date: Wed, 19 Mar 2025 15:02:53 +0000
Subject: [PATCH 06/33] remove base type hack

---
 lib/frontend/parser.mly | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/lib/frontend/parser.mly b/lib/frontend/parser.mly
index 68aa4e4..2190740 100644
--- a/lib/frontend/parser.mly
+++ b/lib/frontend/parser.mly
@@ -269,6 +269,7 @@ ty:
     | parenthesised_datatypes LOLLI simple_ty       { Type.Fun { linear = true;  args = $1; result = $3} }
     | LEFT_PAREN simple_ty PLUS simple_ty RIGHT_PAREN { Type.make_sum_type $2 $4 }
     | tuple_annotation { Type.make_tuple_type $1 }
+    | LEFT_BRACK simple_ty RIGHT_BRACK { Type.make_list_type $2 }
     | simple_ty { $1 }
 
 interface_name:
@@ -330,7 +331,6 @@ mailbox_ty:
 simple_ty:
     | mailbox_ty { $1 }
     | base_ty { $1 }
-    | LEFT_BRACK simple_ty RIGHT_BRACK { Type.make_list_type $2 }
 
 base_ty:
     | CONSTRUCTOR {

From 66d7ce94b6712f4433f7975ad6215253885770e1 Mon Sep 17 00:00:00 2001
From: Danielle Marshall <danielle@starsandspira.ls>
Date: Fri, 21 Mar 2025 15:51:33 +0000
Subject: [PATCH 07/33] extend a couple more Savina benchmarks to use lists

---
 test/examples/savina/big.pat      |  50 +++++++------
 test/examples/savina/cig_smok.pat | 115 +++++++++++++++++-------------
 2 files changed, 94 insertions(+), 71 deletions(-)

diff --git a/test/examples/savina/big.pat b/test/examples/savina/big.pat
index 8a49a2f..0fbd069 100644
--- a/test/examples/savina/big.pat
+++ b/test/examples/savina/big.pat
@@ -1,10 +1,9 @@
 ### Adapted from Savina/big.
 ###
-### A benchmark that implements a many-to-many message passing scenario. Several 
-### processes are spawned, each of which sends a ping message to the others, and 
-### responds with a pong message to any ping message it receives. The benchmark 
-### is parameterized by the number of processes. Since the array type is not 
-### available in Pat, we fix the number of processes to 3.
+### A benchmark that implements a many-to-many message passing scenario. Several
+### processes are spawned, each of which sends a ping message to the others, and
+### responds with a pong message to any ping message it receives. The benchmark
+### is parameterized by the number of processes.
 
 interface ActorMb {
   Ping(Int),
@@ -18,7 +17,7 @@ interface ExitMb {
 
 interface SinkMb {
   Done(),
-  Actors(ExitMb!, ExitMb!, ExitMb!)
+  Actors([ExitMb!])
 }
 
 ## Actor process handling the launching of main loop.
@@ -32,15 +31,15 @@ def actor(self: ActorMb?, exitMb : ExitMb?, id: Int, sinkMb: SinkMb!): Unit {
 ## Blocks actor process and awaits termination message.
 def await_exit(exitMb: ExitMb?): Unit {
     guard exitMb : Exit {
-        receive Exit() from exitMb -> 
+        receive Exit() from exitMb ->
           free(exitMb)
     }
 }
 
 ## Actor process main loop issuing ping requests and handling pong replies.
-def actor_loop(self: ActorMb?, exitMb: ExitMb?, id:Int, sinkMb: SinkMb!, numPings: Int, actorMb1: ActorMb!, actorMb2: ActorMb!): Unit {
+def actor_loop(self: ActorMb?, exitMb: ExitMb?, id: Int, sinkMb: SinkMb!, numPings: Int, actorMb1: ActorMb!, actorMb2: ActorMb!): Unit {
   guard self: *(Ping + Pong) {
-    free -> 
+    free ->
       await_exit(exitMb)
     receive Ping(pingerId) from self ->
 
@@ -52,7 +51,7 @@ def actor_loop(self: ActorMb?, exitMb: ExitMb?, id:Int, sinkMb: SinkMb!, numPing
 
       if (numPings <= 0) {
 
-        # No more pongs to issue. 
+        # No more pongs to issue.
         sinkMb ! Done();
         actor_exit(self);
         await_exit(exitMb)
@@ -79,7 +78,7 @@ def actor_exit(self: ActorMb?): Unit {
 
 ## Replies to ping messages via a pong issued to the specified actor ID.
 def send_pong(id: Int, pingerId: Int, actorMb1: ActorMb!, actorMb2: ActorMb!): Unit {
-  
+
   # We are not synchronising here, but using IDs, which loses information. This
   # makes the type checker think that it might not receive the pong reply. Thus,
   # the type of the mailbox would be ?(Pong + 1).
@@ -93,9 +92,9 @@ def send_pong(id: Int, pingerId: Int, actorMb1: ActorMb!, actorMb2: ActorMb!): U
 
 ## Randomly issues a ping message to one of the participating actors.
 def send_ping(id: Int, actorMb1: ActorMb!, actorMb2: ActorMb!): Unit {
-  
+
   let pongerId = rand(2) in
-  
+
   if (pongerId == 1) {
     actorMb1 ! Ping(id)
   }
@@ -107,29 +106,36 @@ def send_ping(id: Int, actorMb1: ActorMb!, actorMb2: ActorMb!): Unit {
 ## Sink process that coordinates actor termination.
 def sink(self: SinkMb?): Unit {
   guard self: Actors . (*Done) {
-    receive Actors(exitMb1, exitMb2, exitMb3) from self ->
-      sink_loop(self, exitMb1, exitMb2, exitMb3)
+    receive Actors(exitMbs) from self ->
+      sink_loop(self, exitMbs)
   }
 }
 
 ## Sink process main loop issuing termination messages.
-def sink_loop(self: SinkMb?, exitMb1: ExitMb!, exitMb2: ExitMb!, exitMb3: ExitMb!): Unit {
+def sink_loop(self: SinkMb?, exitMbs : [ExitMb!]): Unit {
   guard self: *Done {
     free ->
       # Notify all actors. Placing the sends in this clause ensures that
       # each actor is notified once.
-        exitMb1 ! Exit();
-        exitMb2 ! Exit();
-        exitMb3 ! Exit()
+      notifyExits(exitMbs)
     receive Done() from self ->
-        sink_loop(self, exitMb1, exitMb2, exitMb3)
+        sink_loop(self, exitMbs)
   }
 }
 
+def notifyExits(exitMbs : [ExitMb!]): Unit {
+    caseL exitMbs of {
+    nil : [ExitMb!] -> ()
+  | (y cons ys) : [ExitMb!] ->
+        y ! Exit();
+        notifyExits(ys)
+    }
+}
+
 
 ## Launcher.
 def main(): Unit {
-  
+
   let sinkMb = new [SinkMb] in
   spawn { sink(sinkMb) };
 
@@ -144,7 +150,7 @@ def main(): Unit {
   spawn { actor(actorMb2, exitMb2, 2, sinkMb) };
   spawn { actor(actorMb3, exitMb3, 3, sinkMb) };
 
-  sinkMb ! Actors(exitMb1, exitMb2, exitMb3);
+  let xs = (exitMb1 cons (exitMb2 cons (exitMb3 cons (nil : [ExitMb!])))) in sinkMb ! Actors(xs);
 
   actorMb1 ! Neighbors(actorMb2, actorMb3); # actorMb1: ?Neighbors
   actorMb2 ! Neighbors(actorMb1, actorMb3); # actorMb2: ?Neighbors
diff --git a/test/examples/savina/cig_smok.pat b/test/examples/savina/cig_smok.pat
index 37ef1e7..4877a34 100644
--- a/test/examples/savina/cig_smok.pat
+++ b/test/examples/savina/cig_smok.pat
@@ -1,12 +1,11 @@
 ### Adapted from Savina/cigsmok.
 ###
 ### A benchmark modelling n smokers and one arbiter that decides which smoker to
-### allow to smoke. The benchmark is parameterized by the number of smoker 
-### processes. Since the array type is not available in Pat, we fix the number 
-### of account processes to 3.
+### allow to smoke. The benchmark is parameterized by the number of smoker
+### processes.
 
 interface ArbiterMb {
-  Start(),
+  Start(Int),
   StartedSmoking()
 }
 
@@ -15,78 +14,96 @@ interface SmokerMb {
   Exit()
 }
 
+def create_smokers(self: ArbiterMb?, moreSmokers: Int, acc: [SmokerMb!]): (ArbiterMb? * [SmokerMb!]) {
+    if (moreSmokers == 0) {
+        (self, acc)
+    }
+    else {
+        let newSmoker = new [SmokerMb] in
+            spawn { smoker(newSmoker, self) };
+            create_smokers(self, moreSmokers - 1, (newSmoker cons acc))
+        }
+}
+
 ## Arbiter process handling the creation of smokers and launching of main loop.
 def arbiter(self: ArbiterMb?, numRounds: Int): Unit {
 
-  let smokerMb1 = new [SmokerMb] in
-  spawn { smoker(smokerMb1, self) };
-
-  let smokerMb2 = new [SmokerMb] in
-  spawn { smoker(smokerMb2, self) };
+  guard self: Start . (*StartedSmoking) {
+    receive Start(numSmokers) from self ->
 
-  let smokerMb3 = new [SmokerMb] in
-  spawn { smoker(smokerMb3, self) };
+       let (self, smokerMbs) = create_smokers(self, numSmokers, (nil : [SmokerMb!])) in
 
-  guard self: Start . (*StartedSmoking) {
-    receive Start() from self ->
-      
-      notify_smoker(smokerMb1, smokerMb2, smokerMb3);
-      arbiter_loop(self, numRounds, smokerMb1, smokerMb2, smokerMb3)
+        let smokerMbs = notify_smoker(numSmokers, smokerMbs) in
+        arbiter_loop(self, numSmokers, numRounds, smokerMbs)
   }
 }
 
 ## Randomly chooses the smoker and requests it to smoke.
-def notify_smoker(smokerMb1: SmokerMb!, smokerMb2: SmokerMb!, smokerMb3: SmokerMb!): Unit {
+def notify_smoker(numSmokers: Int, smokerMbs: [SmokerMb!]): [SmokerMb!] {
 
-  let smokerId = rand(2) in
+  let smokerId = rand(numSmokers - 1) in
   let sleepTimeMs = 1000 in
 
-  if (smokerId == 0) {
-    smokerMb1 ! StartSmoking(rand(sleepTimeMs))
-  }
-  else {
-    if (smokerId == 1) {
-      smokerMb2 ! StartSmoking(rand(sleepTimeMs))
+  notify_aux(smokerId, sleepTimeMs, smokerMbs)
+}
+
+def notify_aux(choice: Int, time: Int, smokerMbs: [SmokerMb!]): [SmokerMb!] {
+if (choice == 0) {
+    caseL smokerMbs of {
+        nil : [SmokerMb!] -> smokerMbs
+        | (mb cons mbs) : [SmokerMb!] ->
+            mb ! StartSmoking(rand(time));
+            smokerMbs
     }
-    else {
-      smokerMb3 ! StartSmoking(rand(sleepTimeMs))
+}
+else {
+    caseL smokerMbs of {
+        nil : [SmokerMb!] -> smokerMbs
+        | (mb cons mbs) : [SmokerMb!] ->
+            let smokerMbs = notify_aux(choice - 1, time, mbs) in
+            smokerMbs
     }
-  }
+}
 }
 
 ## Notifies all smokers to terminate.
-def notify_smoker_exit(smokerMb1: SmokerMb!, smokerMb2: SmokerMb!, smokerMb3: SmokerMb!): Unit {
-  smokerMb1 ! Exit();
-  smokerMb2 ! Exit();
-  smokerMb3 ! Exit()
+def notify_smoker_exit(smokerMbs: [SmokerMb!]): [SmokerMb!] {
+    caseL smokerMbs of {
+        nil : [SmokerMb!] -> smokerMbs
+        | (mb cons mbs) : [SmokerMb!] ->
+            mb ! Exit();
+            notify_smoker_exit(mbs)
+        }
 }
 
-## Arbiter process main loop issuing start smoking requests and handling started 
+## Arbiter process main loop issuing start smoking requests and handling started
 ## smoking replies.
-def arbiter_loop(self: ArbiterMb?, numRounds:Int, smokerMb1: SmokerMb!, smokerMb2: SmokerMb!, smokerMb3: SmokerMb!): Unit {
+def arbiter_loop(self: ArbiterMb?, numSmokers: Int, numRounds: Int, smokerMbs: [SmokerMb!]): Unit {
   guard self: *StartedSmoking {
-    free -> 
+    free ->
       ()
     receive StartedSmoking() from self ->
-      
-      # The if here introduces the internal choice, which means that on the 
+
+      # The if here introduces the internal choice, which means that on the
       # receiver side I might or might not receive the message. In this case,
       # the smoker might or might nor receive the Exit message, and must either
       # use (Exit + 1) or (*Exit) in its pattern.
-      
+
       if (numRounds <= 0) {
-        notify_smoker_exit(smokerMb1, smokerMb2, smokerMb3)
+        let smokerMbs = notify_smoker_exit(smokerMbs) in
+            arbiter_loop(self, numSmokers, numRounds - 1, smokerMbs)
       }
       else {
-        notify_smoker(smokerMb1, smokerMb2, smokerMb3)
-      };
+        let smokerMbs = notify_smoker(numSmokers, smokerMbs) in
+            arbiter_loop(self, numSmokers, numRounds - 1, smokerMbs)
+      }
 
-      # Arbiter needs to service all requests before, even if it has sent the 
+      # Arbiter needs to service all requests before, even if it has sent the
       # Exit messages to smokers. Remember that smokers may still be processing
       # StartSmoking messages, but the arbiter has already issued Exit messages
-      # and it still needs to await all the StartedSmoking replies before 
-      # terminating. This is why we do not have an exit_arbiter flush function. 
-      arbiter_loop(self, numRounds - 1, smokerMb1, smokerMb2, smokerMb3)
+      # and it still needs to await all the StartedSmoking replies before
+      # terminating. This is why we do not have an exit_arbiter flush function.
+
   }
 }
 
@@ -95,7 +112,7 @@ def arbiter_loop(self: ArbiterMb?, numRounds:Int, smokerMb1: SmokerMb!, smokerMb
 def smoker(self: SmokerMb?, arbiterMb: ArbiterMb!): Unit {
   # Smoker may be asked to smoke more than once, or none. This is why the *.
   guard self: (*StartSmoking) . (*Exit) {
-    free -> 
+    free ->
       () # Since the smoker might not even receive an Exit/StartSmoking message due to the if condition above.
     receive StartSmoking(ms) from self ->
       arbiterMb ! StartedSmoking();
@@ -118,12 +135,12 @@ def smoker_exit(self: SmokerMb?): Unit {
 }
 
 ## Launcher.
-def main(): Unit {
-  
+def main(numSmokers : Int): Unit {
+
   let arbiterMb = new [ArbiterMb] in
   spawn { arbiter(arbiterMb, 10) };
 
-  arbiterMb ! Start()
+  arbiterMb ! Start(numSmokers)
 }
 
-main()
+main(5)

From 1ab7e44da5bf35dd5b02df8b737d37a0c09b1820 Mon Sep 17 00:00:00 2001
From: Simon Fowler <simon@simonjf.com>
Date: Sun, 23 Mar 2025 16:45:35 +0000
Subject: [PATCH 08/33] fix issue with kfork

---
 lib/frontend/insert_pattern_variables.ml | 14 +++++++++
 lib/typecheck/gen_constraints.ml         | 36 ++++++++++++++++--------
 lib/typecheck/pretypecheck.ml            |  2 +-
 lib/typecheck/ty_env.ml                  | 24 +++-------------
 lib/typecheck/type_utils.ml              |  9 ++++--
 test/examples/savina/kfork.pat           |  9 +++---
 6 files changed, 53 insertions(+), 41 deletions(-)

diff --git a/lib/frontend/insert_pattern_variables.ml b/lib/frontend/insert_pattern_variables.ml
index bf07240..09deb66 100644
--- a/lib/frontend/insert_pattern_variables.ml
+++ b/lib/frontend/insert_pattern_variables.ml
@@ -82,6 +82,20 @@ let visitor =
                 let new_body = self#visit_expr env body in
                 let new_lam = Lam { linear; parameters; result_type; body = new_body } in
                 { expr_with_pos with node = new_lam }
+            | CaseL { term; nil = (nil_ann, nil_cont); cons = (((x_bnd, xs_bnd), cons_ann), cons_cont)} ->
+                let term = self#visit_expr env term in
+                let nil_ann = annotate_type nil_ann in
+                let nil_cont = self#visit_expr env nil_cont in
+                let cons_ann = annotate_type cons_ann in
+                let cons_cont = self#visit_expr env cons_cont in
+                let new_case =
+                    CaseL {
+                        term; 
+                        nil = (nil_ann, nil_cont);
+                        cons = (((x_bnd, xs_bnd), cons_ann), cons_cont)
+                    }
+                in
+                { expr_with_pos with node = new_case }
             | _ -> super#visit_expr env expr_with_pos
 
         method! visit_program env p =
diff --git a/lib/typecheck/gen_constraints.ml b/lib/typecheck/gen_constraints.ml
index 4ebca0f..0a8e2de 100644
--- a/lib/typecheck/gen_constraints.ml
+++ b/lib/typecheck/gen_constraints.ml
@@ -459,30 +459,41 @@ and check_comp : IEnv.t -> Ty_env.t -> Ir.comp -> Type.t -> Ty_env.t * Constrain
             in
             (env, constrs)
         | CaseL { term; nil = (ty1, comp1); cons = (((bnd1, bnd2), ty2), comp2) } ->
+            (* Check that scrutinee has annotated list type *)
             let (term_env, term_constrs) =
                 check_val ienv decl_env term ty1
             in
-            let var1 = Var.of_binder bnd1 in
-            let var2 = Var.of_binder bnd2 in
-            (* Check both branches, and check that inferred types match annotations *)
+            (* Next, check that comp1 (nil case) has expected return type *)
             let (comp1_env, comp1_constrs) = chk comp1 ty in
+            (* Next, check that comp2 (cons case) has expected return type *)
             let (comp2_env, comp2_constrs) = chk comp2 ty in
-            let env1_constrs = Ty_env.check_type ienv var1 ty1 comp1_env pos in
-            let env2_constrs = Ty_env.check_type ienv var2 ty2 comp2_env pos in
+            (* Next, check that the inferred types in comp2_env match annotations *)
+            let var1 = Var.of_binder bnd1 in
+            let var2 = Var.of_binder bnd2 in
+            let elem_ty =
+                match ty1 with
+                    | Type.List elem_ty -> elem_ty
+                    | _ -> Gripers.expected_list_type ty1 [pos]
+            in
+            let env_constrs = 
+                Constraint_set.union
+                    (Ty_env.check_type ienv var1 elem_ty comp2_env pos)
+                    (Ty_env.check_type ienv var2 ty2 comp2_env pos)
+            in
             (* Calculate merge of the branches (sans binders) *)
             let isect_env, isect_constrs =
                 Ty_env.intersect
                   comp1_env
-                  (Ty_env.delete var1 (Ty_env.delete var2 comp2_env)) pos
+                  (Ty_env.delete_many [var1; var2] comp2_env) pos
             in
-            (* Finally join the term env with the intersected env *)
-            let env, env_constrs =
-                Ty_env.join ienv term_env isect_env pos
+            (* Finally combine the term env with the intersected env *)
+            let env, combine_constrs =
+                Ty_env.combine ienv term_env isect_env pos
             in
             let constrs =
                 Constraint_set.union_many
-                    [ comp1_constrs; comp2_constrs; env1_constrs;
-                      env2_constrs; isect_constrs; env_constrs; term_constrs ]
+                    [ comp1_constrs; comp2_constrs; env_constrs;
+                      combine_constrs; isect_constrs; term_constrs ]
             in
             (env, constrs)
         | Seq (e1, e2) ->
@@ -943,7 +954,8 @@ let check_decls ienv decls =
        arguments removed), along with generated constraints. *)
     let check_decl d pos =
         let (env, body_constrs) =
-            check_comp ienv decl_env d.decl_body d.decl_return_type in
+            check_comp ienv decl_env d.decl_body d.decl_return_type
+        in
         (* Check arguments; remove from environment *)
         let (env, arg_constrs) =
             (* Each inferred argument type should be a subtype of the
diff --git a/lib/typecheck/pretypecheck.ml b/lib/typecheck/pretypecheck.ml
index ec3f030..a954ceb 100644
--- a/lib/typecheck/pretypecheck.ml
+++ b/lib/typecheck/pretypecheck.ml
@@ -151,7 +151,7 @@ let rec synthesise_val ienv env value : (value * Pretype.t) =
             wrap (Tuple vs), Pretype.PTuple tys
         | Cons (v1, v2) ->
             let (v1, ty1) = synthesise_val ienv env v1 in
-            let (v2, _) = synthesise_val ienv env v2 in
+            let v2 = check_val ienv env v2 (Pretype.PList ty1) in
             wrap (Cons (v1, v2)), Pretype.PList ty1
         | Lam { linear; parameters; result_type; body } ->
             (* Defer linearity checking to constraint generation. *)
diff --git a/lib/typecheck/ty_env.ml b/lib/typecheck/ty_env.ml
index a1591fa..c3a80b1 100644
--- a/lib/typecheck/ty_env.ml
+++ b/lib/typecheck/ty_env.ml
@@ -223,7 +223,7 @@ let intersect : t -> t -> Position.t -> t * Constraint_set.t =
                 | _, _ ->
                     Gripers.inconsistent_branch_capabilities var [pos]
         in
-        let intersect_types var (t1: Type.t) (t2: Type.t) : (Type.t * Constraint_set.t) =
+        let rec intersect_types var (t1: Type.t) (t2: Type.t) : (Type.t * Constraint_set.t) =
             match t1, t2 with
                 | Base b1, Base b2 when b1 = b2 ->
                     (Base b1, Constraint_set.empty)
@@ -252,25 +252,9 @@ let intersect : t -> t -> Position.t -> t * Constraint_set.t =
                               (* Must take strongest QL across all branches. *)
                               quasilinearity = Quasilinearity.max ql1 ql2
                           }, constrs
-                | List (Mailbox { capability = cap1; interface = iface1; pattern =
-                    Some pat1; quasilinearity = ql1 }),
-                  List (Mailbox { capability = cap2; interface = iface2; pattern =
-                      Some pat2; quasilinearity = ql2 }) ->
-                      (* As before -- interface names must be the same*)
-                      if iface1 <> iface2 then
-                          Gripers.env_interface_mismatch
-                            false t1 t2 var iface1 iface2 [pos]
-                      else
-                          let ((cap, pat), constrs) =
-                              intersect_mailbox_types var
-                                (cap1, pat1) (cap2, pat2) in
-                          Mailbox {
-                              capability = cap;
-                              interface = iface1;
-                              pattern = Some pat;
-                              (* Must take strongest QL across all branches. *)
-                              quasilinearity = Quasilinearity.max ql1 ql2
-                          }, constrs
+                | List t1, List t2 ->
+                    let ty, constrs = intersect_types var t1 t2 in
+                    List ty, constrs
                 | _, _ ->
                     Gripers.type_mismatch false t1 t2 var [pos]
         in
diff --git a/lib/typecheck/type_utils.ml b/lib/typecheck/type_utils.ml
index e413a80..4763d37 100644
--- a/lib/typecheck/type_utils.ml
+++ b/lib/typecheck/type_utils.ml
@@ -8,13 +8,11 @@ open Common.Source_code
    unrestricted. Output mailbox types cannot be made unrestricted. Input mailbox
    types are unrestricted if they are equivalent to 1.
  *)
-let make_unrestricted t pos =
+let rec make_unrestricted t pos =
     let open Type in
     match t with
         (* Trivially unrestricted *)
         | Base _
-        | Tuple []
-        | List _
         | Fun { linear = false; _ } -> Constraint_set.empty
         (* Must be unrestricted *)
         | Fun { linear = true; _ }
@@ -24,6 +22,11 @@ let make_unrestricted t pos =
         | Mailbox { capability = Capability.Out; pattern = Some pat; _ } ->
                 Constraint_set.of_list
                     [Constraint.make (Pattern.One) pat]
+        | Tuple tys ->
+            Constraint_set.union_many
+                (List.map (fun t -> make_unrestricted t pos) tys)
+        | List ty ->
+            make_unrestricted ty pos
         | _ -> assert false
 
 (* Auxiliary definitions*)
diff --git a/test/examples/savina/kfork.pat b/test/examples/savina/kfork.pat
index 3c40cfb..38c888a 100644
--- a/test/examples/savina/kfork.pat
+++ b/test/examples/savina/kfork.pat
@@ -43,12 +43,11 @@ def flood(numMessages: Int, actorMb: ActorMb!): Unit {
 def spawnActors(numActors: Int, acc: [ActorMb!]): [ActorMb!] {
     if (numActors <= 0) {
         acc
+    } else {
+        let newActor = new[ActorMb] in
+        spawn { actor(newActor) };
+        spawnActors(numActors - 1, (newActor cons acc))
     }
-    else {
-        let newActor = new [ActorMb] in
-            spawn { actor(newActor) };
-            spawnActors(numActors - 1, (newActor cons acc))
-        }
 }
 
 def floodActors(numMessages: Int, actorMbs: [ActorMb!]): Unit {

From cb72202f75c4c7d327dd439aea464ca751684edd Mon Sep 17 00:00:00 2001
From: Simon Fowler <simon@simonjf.com>
Date: Sun, 23 Mar 2025 16:57:00 +0000
Subject: [PATCH 09/33] minor

---
 lib/typecheck/pretypecheck.ml | 12 +++++++-----
 1 file changed, 7 insertions(+), 5 deletions(-)

diff --git a/lib/typecheck/pretypecheck.ml b/lib/typecheck/pretypecheck.ml
index a954ceb..1e19fcf 100644
--- a/lib/typecheck/pretypecheck.ml
+++ b/lib/typecheck/pretypecheck.ml
@@ -268,22 +268,24 @@ and synthesise_comp ienv env comp =
             let cont, cont_ty = synthesise_comp ienv env' cont in
             WithPos.make ~pos
                 (LetTuple { binders; tuple; cont }), cont_ty
-        | CaseL { term; nil = (ty1, e1); cons = (((bnd1, bnd2), ty2), e2) } ->
+        | CaseL { term = scrutinee; nil = (ty1, e1); cons = (((bnd1, bnd2), ty2), e2) } ->
             let prety1 = Pretype.of_type ty1 in
             let prety2 = Pretype.of_type ty2 in
-            let term =
-              check_val ienv env term prety2
+            let scrutinee =
+              check_val ienv env scrutinee prety2
             in
             let ty3 = match prety1 with
               | Pretype.PList ty3 -> ty3
               | _ -> raise (Gripers.type_mismatch_with_expected pos "a list type" prety1)
             in
             let b1_env = PretypeEnv.bind (Var.of_binder bnd1) ty3 env in
-            let b2_env = PretypeEnv.bind (Var.of_binder bnd2) prety1 b1_env in
+            let b2_env = PretypeEnv.bind (Var.of_binder bnd2) prety2 b1_env in
             let e2, b2_ty = synthesise_comp ienv b2_env e2 in
             let e1 = check_comp ienv b2_env e1 b2_ty in
             WithPos.make ~pos
-              (CaseL { term; nil = (ty1, e1); cons = (((bnd1, bnd2), ty2), e2) }), b2_ty
+              (CaseL { scrutinee;
+                       nil = (ty1, e1);
+                       cons = (((bnd1, bnd2), ty2), e2) }), b2_ty
         | Seq (e1, e2) ->
             let e1 = check_comp ienv env e1 (Pretype.unit) in
             let e2, e2_ty = synth e2 in

From 1c425a845b2dbb896867fdbe13c873fe70fa5eef Mon Sep 17 00:00:00 2001
From: Danielle Marshall <danielle@starsandspira.ls>
Date: Wed, 23 Apr 2025 12:14:42 +0100
Subject: [PATCH 10/33] reduce annotations needed for caseL expressions

---
 lib/common/ir.ml                         | 20 ++++++++++----------
 lib/common/sugar_ast.ml                  | 17 +++++++++--------
 lib/frontend/insert_pattern_variables.ml | 12 ++++++------
 lib/frontend/parser.mly                  |  8 ++++----
 lib/frontend/sugar_to_ir.ml              | 10 ++++++----
 lib/typecheck/gen_constraints.ml         |  6 +++---
 lib/typecheck/pretypecheck.ml            | 20 ++++++++++----------
 test/examples/savina/cig_smok.pat        |  2 +-
 test/pat-tests/list-1.pat                |  8 ++++----
 test/pat-tests/list-2.pat                | 18 +++++++++---------
 10 files changed, 62 insertions(+), 59 deletions(-)

diff --git a/lib/common/ir.ml b/lib/common/ir.ml
index cf728ab..63b59ce 100644
--- a/lib/common/ir.ml
+++ b/lib/common/ir.ml
@@ -99,8 +99,9 @@ and comp_node =
     }
     | CaseL of {
         term: value;
-        nil: (Type.t[@name "ty"]) * comp;
-        cons: (((Binder.t[@name "binder"]) * (Binder.t[@name "binder"])) * (Type.t[@name "ty"])) * comp
+        ty: (Type.t[@name "ty"]);
+        nil: comp;
+        cons: ((Binder.t[@name "binder"]) * (Binder.t[@name "binder"])) * comp
     }
     | New of string
     | Spawn of comp
@@ -196,17 +197,15 @@ and pp_branch name ppf ((bnd, ty), c) =
         Binder.pp bnd
         Type.pp ty
         pp_comp c
-and pp_nil name ppf (ty, c) =
-  fprintf ppf "%s([]): %a -> @[<v>%a@]"
+and pp_nil name ppf c =
+  fprintf ppf "%s([]) -> @[<v>%a@]"
     name
-    Type.pp ty
     pp_comp c
-and pp_cons name ppf (((bnd1, bnd2), ty), c) =
-    fprintf ppf "%s(%a :: %a): %a -> @[<v>%a@]"
+and pp_cons name ppf ((bnd1, bnd2), c) =
+    fprintf ppf "%s(%a :: %a) -> @[<v>%a@]"
         name
         Binder.pp bnd1
         Binder.pp bnd2
-        Type.pp ty
         pp_comp c
 (* Expressions *)
 and pp_comp ppf comp_with_pos =
@@ -261,10 +260,11 @@ and pp_comp ppf comp_with_pos =
             pp_value term
             (pp_branch "inl") branch1
             (pp_branch "inr") branch2
-    | CaseL { term; nil; cons } ->
+    | CaseL { term; ty; nil; cons } ->
         fprintf ppf
-            "caseL %a of {@[<v>@[<v>%a@]@,@[<v>%a@]@]}"
+            "caseL %a: %a of {@[<v>@[<v>%a@]@,@[<v>%a@]@]}"
             pp_value term
+            Type.pp ty
             (pp_nil "nil") nil
             (pp_cons "cons") cons
     | Guard { target; pattern; guards; _ } ->
diff --git a/lib/common/sugar_ast.ml b/lib/common/sugar_ast.ml
index 7e3f0fe..f6b2475 100644
--- a/lib/common/sugar_ast.ml
+++ b/lib/common/sugar_ast.ml
@@ -44,8 +44,9 @@ and expr_node =
     | Cons of (expr * expr)
     | CaseL of {
         term: expr;
-        nil: (Type.t[@name "ty"]) * expr;
-        cons: ((sugar_binder * sugar_binder) * (Type.t[@name "ty"])) * expr
+        ty: (Type.t[@name "ty"]);
+        nil: expr;
+        cons: (sugar_binder * sugar_binder) * expr
     }
     (* Sums *)
     | Inl of expr
@@ -249,17 +250,17 @@ and pp_expr ppf expr_with_pos =
     | Nil -> pp_print_string ppf "Nil"
     | Cons (e1, e2) ->
         fprintf ppf "Cons %a %a" pp_expr e1 pp_expr e2
-    | CaseL { term; nil = (t1, e1); cons = (((b1, b2), t2), e2) } -> begin
+    | CaseL { term; ty = t1; nil = e1; cons = ((b1, b2), e2) } -> begin
       match t1 with
         | List t ->
 	          fprintf
             ppf
-            "caseL %a of {@[@[nil: %a -> [@%a@]@]][cons %a %a -> [@%a@]@]@]]}"
+            "caseL %a : %a of {@[@[nil -> [@%a@]@]][cons %a %a -> [@%a@]@]@]]}"
             pp_expr term
             Type.pp t1
             pp_expr e1
             pp_bnd_ann (b1, t)
-            pp_bnd_ann (b2, t2)
+            pp_bnd_ann (b2, t1)
             pp_expr e2
         | _ -> fprintf ppf "bad list"
       end
@@ -271,7 +272,7 @@ and pp_expr ppf expr_with_pos =
             (pp_print_newline_list pp_guard) guards
     | Free e -> fprintf ppf "free(%a)" pp_expr e
     | SugarFail (e, ty) -> fprintf ppf "fail(%a)[%a]" pp_expr e Type.pp ty
-and pp_guard ppf guard_with_node = 
+and pp_guard ppf guard_with_node =
     let guard_node = WithPos.node guard_with_node in
     match guard_node with
     | Receive { tag; payload_binders; mailbox_binder; cont } ->
@@ -280,12 +281,12 @@ and pp_guard ppf guard_with_node =
             (pp_print_comma_list pp_print_string) payload_binders
             mailbox_binder
             pp_expr cont
-    (* 
+    (*
        free -> M
        can be treated as syntactic sugar for
        empty(x) -> free(x); M
     *)
-    | GFree e -> 
+    | GFree e ->
         fprintf ppf "free ->@,  @[<v>%a@]" pp_expr e
     | Empty (x, e) ->
         fprintf ppf "empty(%s) ->@,  @[<v>%a@]" x pp_expr e
diff --git a/lib/frontend/insert_pattern_variables.ml b/lib/frontend/insert_pattern_variables.ml
index 09deb66..fe5a44b 100644
--- a/lib/frontend/insert_pattern_variables.ml
+++ b/lib/frontend/insert_pattern_variables.ml
@@ -82,17 +82,17 @@ let visitor =
                 let new_body = self#visit_expr env body in
                 let new_lam = Lam { linear; parameters; result_type; body = new_body } in
                 { expr_with_pos with node = new_lam }
-            | CaseL { term; nil = (nil_ann, nil_cont); cons = (((x_bnd, xs_bnd), cons_ann), cons_cont)} ->
+            | CaseL { term; ty = ty1; nil = nil_cont; cons = ((x_bnd, xs_bnd), cons_cont)} ->
                 let term = self#visit_expr env term in
-                let nil_ann = annotate_type nil_ann in
+                let ty_ann = annotate_type ty1 in
                 let nil_cont = self#visit_expr env nil_cont in
-                let cons_ann = annotate_type cons_ann in
                 let cons_cont = self#visit_expr env cons_cont in
                 let new_case =
                     CaseL {
-                        term; 
-                        nil = (nil_ann, nil_cont);
-                        cons = (((x_bnd, xs_bnd), cons_ann), cons_cont)
+                        term;
+                        ty = ty_ann;
+                        nil = nil_cont;
+                        cons = ((x_bnd, xs_bnd), cons_cont)
                     }
                 in
                 { expr_with_pos with node = new_case }
diff --git a/lib/frontend/parser.mly b/lib/frontend/parser.mly
index 2190740..6c2dd7d 100644
--- a/lib/frontend/parser.mly
+++ b/lib/frontend/parser.mly
@@ -129,10 +129,10 @@ inr_branch:
     | INR LEFT_PAREN VARIABLE RIGHT_PAREN type_annot RIGHTARROW expr { (($3, $5), $7) }
 
 nil_branch:
-    | NIL type_annot RIGHTARROW expr { ($2, $4) }
+    | NIL RIGHTARROW expr { $3 }
 
 cons_branch:
-    | LEFT_PAREN VARIABLE CONS VARIABLE RIGHT_PAREN type_annot RIGHTARROW expr { ((($2, $4), $6), $8) }
+    | LEFT_PAREN VARIABLE CONS VARIABLE RIGHT_PAREN RIGHTARROW expr { (($2, $4), $7) }
 
 expr:
     (* Let *)
@@ -161,8 +161,8 @@ basic_expr:
     | INR LEFT_PAREN expr RIGHT_PAREN { with_pos_from_positions $startpos $endpos ( Inr $3 )}
     | CASE expr OF LEFT_BRACE inl_branch PIPE inr_branch RIGHT_BRACE
         { with_pos_from_positions $startpos $endpos ( Case { term = $2; branch1 = $5; branch2 = $7} )}
-    | CASEL expr OF LEFT_BRACE nil_branch PIPE cons_branch RIGHT_BRACE
-        { with_pos_from_positions $startpos $endpos ( CaseL { term = $2; nil = $5; cons = $7} )}
+    | CASEL basic_expr type_annot OF LEFT_BRACE nil_branch PIPE cons_branch RIGHT_BRACE
+        { with_pos_from_positions $startpos $endpos ( CaseL { term = $2; ty = $3; nil = $6; cons = $8} )}
     (* New *)
     | NEW LEFT_BRACK interface_name RIGHT_BRACK { with_pos_from_positions $startpos $endpos ( New $3 )}
     (* Spawn *)
diff --git a/lib/frontend/sugar_to_ir.ml b/lib/frontend/sugar_to_ir.ml
index 957ec05..8c324f8 100644
--- a/lib/frontend/sugar_to_ir.ml
+++ b/lib/frontend/sugar_to_ir.ml
@@ -175,16 +175,18 @@ and transform_expr :
                 }) |> k env)
         | CaseL {
             term;
-            nil = (ty1, comp1);
-            cons = (((bnd1, bnd2), ty2), comp2) } ->
+            ty = ty1;
+            nil = comp1;
+            cons = ((bnd1, bnd2), comp2) } ->
             transform_subterm env term (fun env v ->
                 let (ir_bnd1, env1) = add_name env bnd1 in
                 let (ir_bnd2, env2) = add_name env1 bnd2 in
                 with_same_pos (
                 Ir.CaseL {
                     term = v;
-                    nil = ty1, (transform_expr env comp1 id);
-                    cons = ((ir_bnd1, ir_bnd2), ty2), (transform_expr env2 comp2 id);
+                    ty = ty1;
+                    nil = (transform_expr env comp1 id);
+                    cons = (ir_bnd1, ir_bnd2), (transform_expr env2 comp2 id);
                 }) |> k env)
         | Seq (e1, e2) ->
             transform_expr env e1 (fun env c1 ->
diff --git a/lib/typecheck/gen_constraints.ml b/lib/typecheck/gen_constraints.ml
index 0a8e2de..b741e35 100644
--- a/lib/typecheck/gen_constraints.ml
+++ b/lib/typecheck/gen_constraints.ml
@@ -458,7 +458,7 @@ and check_comp : IEnv.t -> Ty_env.t -> Ir.comp -> Type.t -> Ty_env.t * Constrain
                       env2_constrs; isect_constrs; env_constrs; term_constrs ]
             in
             (env, constrs)
-        | CaseL { term; nil = (ty1, comp1); cons = (((bnd1, bnd2), ty2), comp2) } ->
+        | CaseL { term; ty = ty1; nil = comp1; cons = ((bnd1, bnd2), comp2) } ->
             (* Check that scrutinee has annotated list type *)
             let (term_env, term_constrs) =
                 check_val ienv decl_env term ty1
@@ -475,10 +475,10 @@ and check_comp : IEnv.t -> Ty_env.t -> Ir.comp -> Type.t -> Ty_env.t * Constrain
                     | Type.List elem_ty -> elem_ty
                     | _ -> Gripers.expected_list_type ty1 [pos]
             in
-            let env_constrs = 
+            let env_constrs =
                 Constraint_set.union
                     (Ty_env.check_type ienv var1 elem_ty comp2_env pos)
-                    (Ty_env.check_type ienv var2 ty2 comp2_env pos)
+                    (Ty_env.check_type ienv var2 ty1 comp2_env pos)
             in
             (* Calculate merge of the branches (sans binders) *)
             let isect_env, isect_constrs =
diff --git a/lib/typecheck/pretypecheck.ml b/lib/typecheck/pretypecheck.ml
index 1e19fcf..e26b8cc 100644
--- a/lib/typecheck/pretypecheck.ml
+++ b/lib/typecheck/pretypecheck.ml
@@ -268,24 +268,24 @@ and synthesise_comp ienv env comp =
             let cont, cont_ty = synthesise_comp ienv env' cont in
             WithPos.make ~pos
                 (LetTuple { binders; tuple; cont }), cont_ty
-        | CaseL { term = scrutinee; nil = (ty1, e1); cons = (((bnd1, bnd2), ty2), e2) } ->
+        | CaseL { term = scrutinee; ty = ty1; nil = e1; cons = ((bnd1, bnd2), e2) } ->
             let prety1 = Pretype.of_type ty1 in
-            let prety2 = Pretype.of_type ty2 in
             let scrutinee =
-              check_val ienv env scrutinee prety2
+              check_val ienv env scrutinee prety1
             in
-            let ty3 = match prety1 with
-              | Pretype.PList ty3 -> ty3
+            let ty2 = match prety1 with
+              | Pretype.PList ty2 -> ty2
               | _ -> raise (Gripers.type_mismatch_with_expected pos "a list type" prety1)
             in
-            let b1_env = PretypeEnv.bind (Var.of_binder bnd1) ty3 env in
-            let b2_env = PretypeEnv.bind (Var.of_binder bnd2) prety2 b1_env in
+            let b1_env = PretypeEnv.bind (Var.of_binder bnd1) ty2 env in
+            let b2_env = PretypeEnv.bind (Var.of_binder bnd2) prety1 b1_env in
             let e2, b2_ty = synthesise_comp ienv b2_env e2 in
             let e1 = check_comp ienv b2_env e1 b2_ty in
             WithPos.make ~pos
-              (CaseL { scrutinee;
-                       nil = (ty1, e1);
-                       cons = (((bnd1, bnd2), ty2), e2) }), b2_ty
+              (CaseL { term = scrutinee;
+                       ty = ty1;
+                       nil = e1;
+                       cons = ((bnd1, bnd2), e2) }), b2_ty
         | Seq (e1, e2) ->
             let e1 = check_comp ienv env e1 (Pretype.unit) in
             let e2, e2_ty = synth e2 in
diff --git a/test/examples/savina/cig_smok.pat b/test/examples/savina/cig_smok.pat
index 4877a34..74c439f 100644
--- a/test/examples/savina/cig_smok.pat
+++ b/test/examples/savina/cig_smok.pat
@@ -61,7 +61,7 @@ else {
         nil : [SmokerMb!] -> smokerMbs
         | (mb cons mbs) : [SmokerMb!] ->
             let smokerMbs = notify_aux(choice - 1, time, mbs) in
-            smokerMbs
+            (mb cons smokerMbs)
     }
 }
 }
diff --git a/test/pat-tests/list-1.pat b/test/pat-tests/list-1.pat
index a89c68f..ebabfc4 100644
--- a/test/pat-tests/list-1.pat
+++ b/test/pat-tests/list-1.pat
@@ -1,8 +1,8 @@
-def main(): Unit {
+def main() : Unit {
     let xs = (5 cons (nil : [Int])) in
-    caseL xs of {
-          nil : [Int] -> print("nil")
-        | (y cons ys) : [Int] -> print(intToString(y))
+    caseL xs : [Int] of {
+          nil -> print("nil")
+        | (y cons ys) -> print(intToString(y))
     }
 }
 
diff --git a/test/pat-tests/list-2.pat b/test/pat-tests/list-2.pat
index 0bae0e6..a3e27d2 100644
--- a/test/pat-tests/list-2.pat
+++ b/test/pat-tests/list-2.pat
@@ -1,22 +1,22 @@
 def snoc(xs : [Int], x : Int): [Int] {
-    caseL xs of {
-        nil : [Int] -> (x cons (nil : [Int]))
-      | (y cons ys) : [Int] -> (y cons snoc(ys, x))
+    caseL xs : [Int] of {
+        nil -> (x cons (nil : [Int]))
+      | (y cons ys) -> (y cons snoc(ys, x))
     }
 }
 
 def reverse(xs : [Int]): [Int] {
-    caseL xs of {
-          nil : [Int] -> nil
-        | (y cons ys) : [Int] -> snoc(reverse(ys), y)
+    caseL xs : [Int] of {
+          nil -> nil
+        | (y cons ys) -> snoc(reverse(ys), y)
     }
 }
 
 def main(): Unit {
     let xs = (1 cons (2 cons (3 cons (nil : [Int])))) in
-    caseL reverse(xs) of {
-        nil : [Int] -> print("nil")
-      | (y cons ys) : [Int] -> print(intToString(y))
+    caseL reverse(xs) : [Int] of {
+        nil -> print("nil")
+      | (y cons ys) -> print(intToString(y))
   }
 }
 

From 615c2bc10080fdc6a78b85fdc55c37fbecebeaf1 Mon Sep 17 00:00:00 2001
From: Danielle Marshall <danielle@starsandspira.ls>
Date: Wed, 23 Apr 2025 12:27:44 +0100
Subject: [PATCH 11/33] reorganise savina list examples

---
 test/examples/savina/banking.pat        |  58 ++++----
 test/examples/savina/big.pat            |  44 +++---
 test/examples/savina/cig_smok.pat       | 169 ++++++------------------
 test/examples/savina/kfork.pat          |  44 +++---
 test/examples/savina/lists/banking.pat  |  61 +++++++++
 test/examples/savina/lists/barber.pat   |  49 +++++++
 test/examples/savina/lists/big.pat      | 164 +++++++++++++++++++++++
 test/examples/savina/lists/cig_smok.pat | 146 ++++++++++++++++++++
 test/examples/savina/lists/kfork.pat    |  69 ++++++++++
 9 files changed, 597 insertions(+), 207 deletions(-)
 create mode 100644 test/examples/savina/lists/banking.pat
 create mode 100644 test/examples/savina/lists/barber.pat
 create mode 100644 test/examples/savina/lists/big.pat
 create mode 100644 test/examples/savina/lists/cig_smok.pat
 create mode 100644 test/examples/savina/lists/kfork.pat

diff --git a/test/examples/savina/banking.pat b/test/examples/savina/banking.pat
index 58669b8..8249755 100644
--- a/test/examples/savina/banking.pat
+++ b/test/examples/savina/banking.pat
@@ -1,10 +1,10 @@
 ### Adapted from Savina/banking.
 ###
-### A benchmark that implements a request-reply chain passing scenario. Several 
+### A benchmark that implements a request-reply chain passing scenario. Several
 ### account processes are spawned, each of which may be sent a credit request
-### by the central teller process. The benchmark is parameterized by the number 
-### of account processes. Since the array type is not available in Pat, we fix 
-### the number of account processes to 3.
+### by the central teller process. The benchmark is parameterized by the number
+### of account processes. Since the array type is not available in Pat, we fix
+### the number of account processes to 3.
 
 interface TellerMb {
   Start(),
@@ -18,10 +18,10 @@ interface AccountMb {
   Stop()
 }
 
-## Teller process handling the creation of account processes and launching of 
-## main loop.
+## Teller process handling the creation of account processes and launching of
+## main loop.
 def teller(self: TellerMb?, numAccounts: Int): Unit {
-  
+
   # Create accounts.
   let accountMb1 = new [AccountMb] in
   spawn { account(accountMb1, 1, 200) };
@@ -35,7 +35,7 @@ def teller(self: TellerMb?, numAccounts: Int): Unit {
   guard self: Start {
     receive Start() from self ->
 
-      # Note. Even if the randomization of message sending is performed in a 
+      # Note. Even if the randomization of message sending is performed in a
       # different processes, there is no risk of a race condition where the
       # messages are sent to a non-existing mailbox. This is because, as can be
       # gleaned above, mailboxes are created in sequential fashion within this
@@ -47,20 +47,20 @@ def teller(self: TellerMb?, numAccounts: Int): Unit {
 
 ## Randomly chooses the source account.
 def generate_work(tellerMb: TellerMb!, numAccounts: Int, acc1: AccountMb![R], acc2: AccountMb![R], acc3 : AccountMb![R]): Unit {
-  
+
   # Randomly choose source account from which the funds shall be taken.
-  let sourceId = rand(numAccounts - 1) in # -1 because rand() is 0-indexed.
+  let sourceId = rand(numAccounts - 1) in # -1 because rand() is 0-indexed.
   if (sourceId == 0) {
 
-    # First source account.
+    # First source account.
     choose_dst_acc(tellerMb, numAccounts, acc1, acc2, acc3)
   }
-  else { 
+  else {
     if (sourceId == 1) {
 
         # Second source account.
         choose_dst_acc(tellerMb, numAccounts, acc2, acc1, acc3)
-    } 
+    }
     else {
 
         # Third source account.
@@ -69,17 +69,17 @@ def generate_work(tellerMb: TellerMb!, numAccounts: Int, acc1: AccountMb![R], ac
   }
 }
 
-## Randomly chooses the destination account and issues a credit request. The
+## Randomly chooses the destination account and issues a credit request. The
 ## function ensures that the source and destination account are different.
 def choose_dst_acc(tellerMb: TellerMb!, numAccounts: Int, srcAccountMb: AccountMb![R], dstAccountMb1: AccountMb![R], dstAccountMb2 : AccountMb![R]): Unit {
-  
-  # Randomly choose destination account to which funds shall be deposited. -2 
-  # because rand() is 0-indexed, and because we do not include the source 
+
+  # Randomly choose destination account to which funds shall be deposited. -2
+  # because rand() is 0-indexed, and because we do not include the source
   # account in the random choice (i.e., the source account is not permitted to
-  # send funds to itself).
-  let dstAccountId = rand(numAccounts - 2) in 
+  # send funds to itself).
+  let dstAccountId = rand(numAccounts - 2) in
 
-  let dstAccount = 
+  let dstAccount =
     if (dstAccountId == 0) {
       dstAccountMb1
     } else {
@@ -91,12 +91,12 @@ def choose_dst_acc(tellerMb: TellerMb!, numAccounts: Int, srcAccountMb: AccountM
   dstAccount ! Credit(tellerMb, amount, srcAccountMb)
 }
 
-## Teller process main loop handling replies from accounts.
+## Teller process main loop handling replies from accounts.
 def teller_loop(self: TellerMb?, accountMb1: AccountMb!, accountMb2: AccountMb!, accountMb3: AccountMb!): Unit {
   guard self: *Reply {
-    free -> 
+    free ->
 
-      # All credit requests serviced. Stop accounts.
+      # All credit requests serviced. Stop accounts.
       accountMb1 ! Stop();
       accountMb2 ! Stop();
       accountMb3 ! Stop()
@@ -105,11 +105,11 @@ def teller_loop(self: TellerMb?, accountMb1: AccountMb!, accountMb2: AccountMb!,
   }
 }
 
-## Account process handling credit requests issued by the teller, and debit 
-## requests issued by other accounts.
+## Account process handling credit requests issued by the teller, and debit
+## requests issued by other accounts.
 def account(self: AccountMb?, id: Int, balance: Int): Unit {
   guard self: *(Debit + Credit) . Stop {
-    free -> 
+    free ->
       ()
     receive Debit(accountMb, amount) from self ->
 
@@ -130,13 +130,13 @@ def account(self: AccountMb?, id: Int, balance: Int): Unit {
           tellerMb ! Reply();
           account(self, id, balance - amount)
       }
-      
+
     receive Stop() from self ->
       account_exit(self)
   }
 }
 
-## Actor process exit procedure that flushes potential residual messages.
+## Actor process exit procedure that flushes potential residual messages.
 def account_exit(self: AccountMb?): Unit {
   guard self: *(Debit + Credit)  {
     free -> ()
@@ -147,7 +147,7 @@ def account_exit(self: AccountMb?): Unit {
   }
 }
 
-## Launcher.
+## Launcher.
 def main(): Unit {
   let tellerMb = new [TellerMb] in
   spawn { teller(tellerMb, 3) };
diff --git a/test/examples/savina/big.pat b/test/examples/savina/big.pat
index 0fbd069..772c734 100644
--- a/test/examples/savina/big.pat
+++ b/test/examples/savina/big.pat
@@ -3,7 +3,8 @@
 ### A benchmark that implements a many-to-many message passing scenario. Several
 ### processes are spawned, each of which sends a ping message to the others, and
 ### responds with a pong message to any ping message it receives. The benchmark
-### is parameterized by the number of processes.
+### is parameterized by the number of processes. Since the array type is not
+### available in Pat, we fix the number of processes to 3.
 
 interface ActorMb {
   Ping(Int),
@@ -17,7 +18,7 @@ interface ExitMb {
 
 interface SinkMb {
   Done(),
-  Actors([ExitMb!])
+  Actors(ExitMb!, ExitMb!, ExitMb!)
 }
 
 ## Actor process handling the launching of main loop.
@@ -28,7 +29,7 @@ def actor(self: ActorMb?, exitMb : ExitMb?, id: Int, sinkMb: SinkMb!): Unit {
   }
 }
 
-## Blocks actor process and awaits termination message.
+## Blocks actor process and awaits termination message.
 def await_exit(exitMb: ExitMb?): Unit {
     guard exitMb : Exit {
         receive Exit() from exitMb ->
@@ -36,8 +37,8 @@ def await_exit(exitMb: ExitMb?): Unit {
     }
 }
 
-## Actor process main loop issuing ping requests and handling pong replies.
-def actor_loop(self: ActorMb?, exitMb: ExitMb?, id: Int, sinkMb: SinkMb!, numPings: Int, actorMb1: ActorMb!, actorMb2: ActorMb!): Unit {
+## Actor process main loop issuing ping requests and handling pong replies.
+def actor_loop(self: ActorMb?, exitMb: ExitMb?, id:Int, sinkMb: SinkMb!, numPings: Int, actorMb1: ActorMb!, actorMb2: ActorMb!): Unit {
   guard self: *(Ping + Pong) {
     free ->
       await_exit(exitMb)
@@ -58,14 +59,14 @@ def actor_loop(self: ActorMb?, exitMb: ExitMb?, id: Int, sinkMb: SinkMb!, numPin
       }
       else {
 
-        # Issue ping to random participant.
+        # Issue ping to random participant.
         send_ping(id, actorMb1, actorMb2);
         actor_loop(self, exitMb, id, sinkMb, numPings - 1, actorMb1, actorMb2)
       }
   }
 }
 
-## Actor process exit procedure that flushes potential residual messages.
+## Actor process exit procedure that flushes potential residual messages.
 def actor_exit(self: ActorMb?): Unit {
   guard self: (*Ping) . (*Pong) {
     free -> ()
@@ -76,7 +77,7 @@ def actor_exit(self: ActorMb?): Unit {
   }
 }
 
-## Replies to ping messages via a pong issued to the specified actor ID.
+## Replies to ping messages via a pong issued to the specified actor ID.
 def send_pong(id: Int, pingerId: Int, actorMb1: ActorMb!, actorMb2: ActorMb!): Unit {
 
   # We are not synchronising here, but using IDs, which loses information. This
@@ -106,34 +107,27 @@ def send_ping(id: Int, actorMb1: ActorMb!, actorMb2: ActorMb!): Unit {
 ## Sink process that coordinates actor termination.
 def sink(self: SinkMb?): Unit {
   guard self: Actors . (*Done) {
-    receive Actors(exitMbs) from self ->
-      sink_loop(self, exitMbs)
+    receive Actors(exitMb1, exitMb2, exitMb3) from self ->
+      sink_loop(self, exitMb1, exitMb2, exitMb3)
   }
 }
 
 ## Sink process main loop issuing termination messages.
-def sink_loop(self: SinkMb?, exitMbs : [ExitMb!]): Unit {
+def sink_loop(self: SinkMb?, exitMb1: ExitMb!, exitMb2: ExitMb!, exitMb3: ExitMb!): Unit {
   guard self: *Done {
     free ->
-      # Notify all actors. Placing the sends in this clause ensures that
+      # Notify all actors. Placing the sends in this clause ensures that
       # each actor is notified once.
-      notifyExits(exitMbs)
+        exitMb1 ! Exit();
+        exitMb2 ! Exit();
+        exitMb3 ! Exit()
     receive Done() from self ->
-        sink_loop(self, exitMbs)
+        sink_loop(self, exitMb1, exitMb2, exitMb3)
   }
 }
 
-def notifyExits(exitMbs : [ExitMb!]): Unit {
-    caseL exitMbs of {
-    nil : [ExitMb!] -> ()
-  | (y cons ys) : [ExitMb!] ->
-        y ! Exit();
-        notifyExits(ys)
-    }
-}
-
 
-## Launcher.
+## Launcher.
 def main(): Unit {
 
   let sinkMb = new [SinkMb] in
@@ -150,7 +144,7 @@ def main(): Unit {
   spawn { actor(actorMb2, exitMb2, 2, sinkMb) };
   spawn { actor(actorMb3, exitMb3, 3, sinkMb) };
 
-  let xs = (exitMb1 cons (exitMb2 cons (exitMb3 cons (nil : [ExitMb!])))) in sinkMb ! Actors(xs);
+  sinkMb ! Actors(exitMb1, exitMb2, exitMb3);
 
   actorMb1 ! Neighbors(actorMb2, actorMb3); # actorMb1: ?Neighbors
   actorMb2 ! Neighbors(actorMb1, actorMb3); # actorMb2: ?Neighbors
diff --git a/test/examples/savina/cig_smok.pat b/test/examples/savina/cig_smok.pat
index 74c439f..30572be 100644
--- a/test/examples/savina/cig_smok.pat
+++ b/test/examples/savina/cig_smok.pat
@@ -1,146 +1,61 @@
-### Adapted from Savina/cigsmok.
+### Adapted from Savina/fjthrput.
 ###
-### A benchmark modelling n smokers and one arbiter that decides which smoker to
-### allow to smoke. The benchmark is parameterized by the number of smoker
-### processes.
+### Models the creation of n actors that are given a number of messages, for
+### each of which, a computation is performed. The benchmark is parameterized by
+### the number of actor processes. Since the array type is not available in
+### Pat, we fix the number of actor processes to 3.
 
-interface ArbiterMb {
-  Start(Int),
-  StartedSmoking()
+interface ActorMb {
+  Packet()
 }
 
-interface SmokerMb {
-  StartSmoking(Int),
-  Exit()
-}
-
-def create_smokers(self: ArbiterMb?, moreSmokers: Int, acc: [SmokerMb!]): (ArbiterMb? * [SmokerMb!]) {
-    if (moreSmokers == 0) {
-        (self, acc)
-    }
-    else {
-        let newSmoker = new [SmokerMb] in
-            spawn { smoker(newSmoker, self) };
-            create_smokers(self, moreSmokers - 1, (newSmoker cons acc))
-        }
-}
-
-## Arbiter process handling the creation of smokers and launching of main loop.
-def arbiter(self: ArbiterMb?, numRounds: Int): Unit {
-
-  guard self: Start . (*StartedSmoking) {
-    receive Start(numSmokers) from self ->
-
-       let (self, smokerMbs) = create_smokers(self, numSmokers, (nil : [SmokerMb!])) in
-
-        let smokerMbs = notify_smoker(numSmokers, smokerMbs) in
-        arbiter_loop(self, numSmokers, numRounds, smokerMbs)
-  }
-}
-
-## Randomly chooses the smoker and requests it to smoke.
-def notify_smoker(numSmokers: Int, smokerMbs: [SmokerMb!]): [SmokerMb!] {
-
-  let smokerId = rand(numSmokers - 1) in
-  let sleepTimeMs = 1000 in
-
-  notify_aux(smokerId, sleepTimeMs, smokerMbs)
-}
-
-def notify_aux(choice: Int, time: Int, smokerMbs: [SmokerMb!]): [SmokerMb!] {
-if (choice == 0) {
-    caseL smokerMbs of {
-        nil : [SmokerMb!] -> smokerMbs
-        | (mb cons mbs) : [SmokerMb!] ->
-            mb ! StartSmoking(rand(time));
-            smokerMbs
-    }
-}
-else {
-    caseL smokerMbs of {
-        nil : [SmokerMb!] -> smokerMbs
-        | (mb cons mbs) : [SmokerMb!] ->
-            let smokerMbs = notify_aux(choice - 1, time, mbs) in
-            (mb cons smokerMbs)
-    }
-}
-}
-
-## Notifies all smokers to terminate.
-def notify_smoker_exit(smokerMbs: [SmokerMb!]): [SmokerMb!] {
-    caseL smokerMbs of {
-        nil : [SmokerMb!] -> smokerMbs
-        | (mb cons mbs) : [SmokerMb!] ->
-            mb ! Exit();
-            notify_smoker_exit(mbs)
-        }
-}
-
-## Arbiter process main loop issuing start smoking requests and handling started
-## smoking replies.
-def arbiter_loop(self: ArbiterMb?, numSmokers: Int, numRounds: Int, smokerMbs: [SmokerMb!]): Unit {
-  guard self: *StartedSmoking {
+## Actor processes handling the packet requests.
+def actor(self: ActorMb?): Unit {
+  guard self: *Packet {
     free ->
       ()
-    receive StartedSmoking() from self ->
-
-      # The if here introduces the internal choice, which means that on the
-      # receiver side I might or might not receive the message. In this case,
-      # the smoker might or might nor receive the Exit message, and must either
-      # use (Exit + 1) or (*Exit) in its pattern.
-
-      if (numRounds <= 0) {
-        let smokerMbs = notify_smoker_exit(smokerMbs) in
-            arbiter_loop(self, numSmokers, numRounds - 1, smokerMbs)
-      }
-      else {
-        let smokerMbs = notify_smoker(numSmokers, smokerMbs) in
-            arbiter_loop(self, numSmokers, numRounds - 1, smokerMbs)
-      }
-
-      # Arbiter needs to service all requests before, even if it has sent the
-      # Exit messages to smokers. Remember that smokers may still be processing
-      # StartSmoking messages, but the arbiter has already issued Exit messages
-      # and it still needs to await all the StartedSmoking replies before
-      # terminating. This is why we do not have an exit_arbiter flush function.
-
+    receive Packet() from self ->
+      let dummy = fact(rand(100000)) in
+      actor(self)
   }
 }
 
-## Smoker process main loop handling start smoking requests and issuing started
-## smoking replies to/from the arbiter.
-def smoker(self: SmokerMb?, arbiterMb: ArbiterMb!): Unit {
-  # Smoker may be asked to smoke more than once, or none. This is why the *.
-  guard self: (*StartSmoking) . (*Exit) {
-    free ->
-      () # Since the smoker might not even receive an Exit/StartSmoking message due to the if condition above.
-    receive StartSmoking(ms) from self ->
-      arbiterMb ! StartedSmoking();
-      sleep(ms);
-      smoker(self, arbiterMb)
-    receive Exit() from self ->
-      smoker_exit(self)
+## Computes the factorial of n.
+def fact(n: Int): Int {
+  if (n <= 0) {
+    1
+  }
+  else {
+    n * (fact(n - 1))
   }
 }
 
-## Smoker process exit procedure that flushes potential residual messages.
-def smoker_exit(self: SmokerMb?): Unit {
-  guard self: (*StartSmoking) . (*Exit) {
-    free -> () # In case I have one or more Exit/StartSmoking messages due to the if condition above.
-    receive StartSmoking(ms) from self ->
-      smoker_exit(self)
-    receive Exit() from self ->
-      smoker_exit(self)
+## Sends the given number of messages to the specified actor mailbox.
+def flood(numMessages: Int, actorMb: ActorMb!): Unit {
+  if (numMessages <= 0) {
+    ()
+  }
+  else {
+    actorMb ! Packet();
+    flood(numMessages - 1, actorMb)
   }
 }
 
-## Launcher.
-def main(numSmokers : Int): Unit {
+## Launcher.
+def main(): Unit {
+
+  let actorMb1 = new [ActorMb] in
+  spawn { actor(actorMb1) };
+
+  let actorMb2 = new [ActorMb] in
+  spawn { actor(actorMb2) };
 
-  let arbiterMb = new [ArbiterMb] in
-  spawn { arbiter(arbiterMb, 10) };
+  let actorMb3 = new [ActorMb] in
+  spawn { actor(actorMb3) };
 
-  arbiterMb ! Start(numSmokers)
+  flood(100, actorMb1);
+  flood(1000, actorMb1);
+  flood(10000, actorMb1)
 }
 
-main(5)
+main()
diff --git a/test/examples/savina/kfork.pat b/test/examples/savina/kfork.pat
index 38c888a..30572be 100644
--- a/test/examples/savina/kfork.pat
+++ b/test/examples/savina/kfork.pat
@@ -2,13 +2,14 @@
 ###
 ### Models the creation of n actors that are given a number of messages, for
 ### each of which, a computation is performed. The benchmark is parameterized by
-### the number of actor processes.
+### the number of actor processes. Since the array type is not available in
+### Pat, we fix the number of actor processes to 3.
 
 interface ActorMb {
   Packet()
 }
 
-## Actor processes handling the packet requests.
+## Actor processes handling the packet requests.
 def actor(self: ActorMb?): Unit {
   guard self: *Packet {
     free ->
@@ -19,7 +20,7 @@ def actor(self: ActorMb?): Unit {
   }
 }
 
-## Computes the factorial of n.
+## Computes the factorial of n.
 def fact(n: Int): Int {
   if (n <= 0) {
     1
@@ -29,7 +30,7 @@ def fact(n: Int): Int {
   }
 }
 
-## Sends the given number of messages to the specified actor mailbox.
+## Sends the given number of messages to the specified actor mailbox.
 def flood(numMessages: Int, actorMb: ActorMb!): Unit {
   if (numMessages <= 0) {
     ()
@@ -40,30 +41,21 @@ def flood(numMessages: Int, actorMb: ActorMb!): Unit {
   }
 }
 
-def spawnActors(numActors: Int, acc: [ActorMb!]): [ActorMb!] {
-    if (numActors <= 0) {
-        acc
-    } else {
-        let newActor = new[ActorMb] in
-        spawn { actor(newActor) };
-        spawnActors(numActors - 1, (newActor cons acc))
-    }
-}
+## Launcher.
+def main(): Unit {
 
-def floodActors(numMessages: Int, actorMbs: [ActorMb!]): Unit {
-    caseL actorMbs of {
-        nil : [ActorMb!] -> ()
-      | (a cons as) : [ActorMb!] ->
-            flood(numMessages, a);
-            floodActors(numMessages, as)
-        }
-}
+  let actorMb1 = new [ActorMb] in
+  spawn { actor(actorMb1) };
+
+  let actorMb2 = new [ActorMb] in
+  spawn { actor(actorMb2) };
 
-## Launcher.
-def main(numActors: Int): Unit {
+  let actorMb3 = new [ActorMb] in
+  spawn { actor(actorMb3) };
 
-  let actorMbs = spawnActors(numActors, (nil : [ActorMb!])) in
-    floodActors(1000, actorMbs)
+  flood(100, actorMb1);
+  flood(1000, actorMb1);
+  flood(10000, actorMb1)
 }
 
-main(3)
+main()
diff --git a/test/examples/savina/lists/banking.pat b/test/examples/savina/lists/banking.pat
new file mode 100644
index 0000000..30572be
--- /dev/null
+++ b/test/examples/savina/lists/banking.pat
@@ -0,0 +1,61 @@
+### Adapted from Savina/fjthrput.
+###
+### Models the creation of n actors that are given a number of messages, for
+### each of which, a computation is performed. The benchmark is parameterized by
+### the number of actor processes. Since the array type is not available in
+### Pat, we fix the number of actor processes to 3.
+
+interface ActorMb {
+  Packet()
+}
+
+## Actor processes handling the packet requests.
+def actor(self: ActorMb?): Unit {
+  guard self: *Packet {
+    free ->
+      ()
+    receive Packet() from self ->
+      let dummy = fact(rand(100000)) in
+      actor(self)
+  }
+}
+
+## Computes the factorial of n.
+def fact(n: Int): Int {
+  if (n <= 0) {
+    1
+  }
+  else {
+    n * (fact(n - 1))
+  }
+}
+
+## Sends the given number of messages to the specified actor mailbox.
+def flood(numMessages: Int, actorMb: ActorMb!): Unit {
+  if (numMessages <= 0) {
+    ()
+  }
+  else {
+    actorMb ! Packet();
+    flood(numMessages - 1, actorMb)
+  }
+}
+
+## Launcher.
+def main(): Unit {
+
+  let actorMb1 = new [ActorMb] in
+  spawn { actor(actorMb1) };
+
+  let actorMb2 = new [ActorMb] in
+  spawn { actor(actorMb2) };
+
+  let actorMb3 = new [ActorMb] in
+  spawn { actor(actorMb3) };
+
+  flood(100, actorMb1);
+  flood(1000, actorMb1);
+  flood(10000, actorMb1)
+}
+
+main()
diff --git a/test/examples/savina/lists/barber.pat b/test/examples/savina/lists/barber.pat
new file mode 100644
index 0000000..5b86aa8
--- /dev/null
+++ b/test/examples/savina/lists/barber.pat
@@ -0,0 +1,49 @@
+### Adapted from savina/barber.
+###
+### A barber is waiting for customers. When there are no customers the barber sleeps. When a customer
+### arrives, he wakes the barber or sits in one of the waiting chairs in the waiting room. If all chairs
+### are occupied, the customer leaves. Customers repeatedly visit the barber shop until they get a haircut.
+### The key element of the solution is to make sure that whenever a customer or a barber checks the state
+### of the waiting room, they always see a valid state. The problem is implemented using a Selector actor
+### that decides which is the next customer, Customer actors, a Barber actor and a Room actor.
+
+interface RoomMb {
+    Enter(CustomerMb!, RoomMb!),
+    Next(),
+    Exit()
+}
+
+interface BarberMb {
+    Enter(CustomerMb!, RoomMb!),
+    Wait(),
+    Exit()
+}
+
+interface SelectorMb {
+    Start(),
+    Returned(CustomerMb!),
+    Done()
+}
+
+interface CustomerMb {
+    Full(),
+    Wait(),
+    Start(),
+    Done()
+}
+
+def room(self: RoomMb?, capacity: Int, barber: BarberMb!): Unit {
+
+}
+
+def barber(self: BarberMb?): Unit {
+
+}
+
+def selector(self: SelectorMb?, generator: Int, haircuts: Int, room: RoomMb!): Unit {
+
+}
+
+def customer(self: CustomerMb?, selector: SelectorMb!): Unit {
+
+}
diff --git a/test/examples/savina/lists/big.pat b/test/examples/savina/lists/big.pat
new file mode 100644
index 0000000..8755521
--- /dev/null
+++ b/test/examples/savina/lists/big.pat
@@ -0,0 +1,164 @@
+### Adapted from Savina/big.
+###
+### A benchmark that implements a many-to-many message passing scenario. Several
+### processes are spawned, each of which sends a ping message to the others, and
+### responds with a pong message to any ping message it receives. The benchmark
+### is parameterized by the number of processes.
+
+interface ActorMb {
+  Ping(Int),
+  Pong(Int),
+  Neighbors(ActorMb!, ActorMb!)
+}
+
+interface ExitMb {
+  Exit()
+}
+
+interface SinkMb {
+  Done(),
+  Actors([ExitMb!])
+}
+
+## Actor process handling the launching of main loop.
+def actor(self: ActorMb?, exitMb : ExitMb?, id: Int, sinkMb: SinkMb!): Unit {
+  guard self: Neighbors . *(Pong + Ping)  {
+    receive Neighbors(actorMb1, actorMb2) from self ->
+      actor_loop(self, exitMb, id, sinkMb, 100, actorMb1, actorMb2)
+  }
+}
+
+## Blocks actor process and awaits termination message.
+def await_exit(exitMb: ExitMb?): Unit {
+    guard exitMb : Exit {
+        receive Exit() from exitMb ->
+          free(exitMb)
+    }
+}
+
+## Actor process main loop issuing ping requests and handling pong replies.
+def actor_loop(self: ActorMb?, exitMb: ExitMb?, id: Int, sinkMb: SinkMb!, numPings: Int, actorMb1: ActorMb!, actorMb2: ActorMb!): Unit {
+  guard self: *(Ping + Pong) {
+    free ->
+      await_exit(exitMb)
+    receive Ping(pingerId) from self ->
+
+      # Reply to ping.
+      send_pong(id, pingerId, actorMb1, actorMb2);
+      actor_loop(self, exitMb, id, sinkMb, numPings, actorMb1, actorMb2)
+
+    receive Pong(pongerId) from self ->
+
+      if (numPings <= 0) {
+
+        # No more pongs to issue.
+        sinkMb ! Done();
+        actor_exit(self);
+        await_exit(exitMb)
+      }
+      else {
+
+        # Issue ping to random participant.
+        send_ping(id, actorMb1, actorMb2);
+        actor_loop(self, exitMb, id, sinkMb, numPings - 1, actorMb1, actorMb2)
+      }
+  }
+}
+
+## Actor process exit procedure that flushes potential residual messages.
+def actor_exit(self: ActorMb?): Unit {
+  guard self: (*Ping) . (*Pong) {
+    free -> ()
+    receive Ping(pingerId) from self ->
+      actor_exit(self)
+    receive Pong(pongerId) from self ->
+      actor_exit(self)
+  }
+}
+
+## Replies to ping messages via a pong issued to the specified actor ID.
+def send_pong(id: Int, pingerId: Int, actorMb1: ActorMb!, actorMb2: ActorMb!): Unit {
+
+  # We are not synchronising here, but using IDs, which loses information. This
+  # makes the type checker think that it might not receive the pong reply. Thus,
+  # the type of the mailbox would be ?(Pong + 1).
+  if (pingerId == 1) {
+    actorMb1 ! Pong(id)
+  }
+  else {
+    actorMb2 ! Pong(id)
+  }
+}
+
+## Randomly issues a ping message to one of the participating actors.
+def send_ping(id: Int, actorMb1: ActorMb!, actorMb2: ActorMb!): Unit {
+
+  let pongerId = rand(2) in
+
+  if (pongerId == 1) {
+    actorMb1 ! Ping(id)
+  }
+  else {
+    actorMb2 ! Ping(id)
+  }
+}
+
+## Sink process that coordinates actor termination.
+def sink(self: SinkMb?): Unit {
+  guard self: Actors . (*Done) {
+    receive Actors(exitMbs) from self ->
+      sink_loop(self, exitMbs)
+  }
+}
+
+## Sink process main loop issuing termination messages.
+def sink_loop(self: SinkMb?, exitMbs : [ExitMb!]): Unit {
+  guard self: *Done {
+    free ->
+      # Notify all actors. Placing the sends in this clause ensures that
+      # each actor is notified once.
+      notifyExits(exitMbs)
+    receive Done() from self ->
+        sink_loop(self, exitMbs)
+  }
+}
+
+def notifyExits(exitMbs : [ExitMb!]): Unit {
+    caseL exitMbs : [ExitMb!] of {
+    nil -> ()
+  | (y cons ys) ->
+        y ! Exit();
+        notifyExits(ys)
+    }
+}
+
+
+## Launcher.
+def main(): Unit {
+
+  let sinkMb = new [SinkMb] in
+  spawn { sink(sinkMb) };
+
+  let actorMb1 = new [ActorMb] in # actorMb1: ?1
+  let actorMb2 = new [ActorMb] in # actorMb2: ?1
+  let actorMb3 = new [ActorMb] in # actorMb3: ?1
+  let exitMb1 = new [ExitMb] in # exitMb1: ?1
+  let exitMb2 = new [ExitMb] in # exitMb2: ?1
+  let exitMb3 = new [ExitMb] in # exitMb3: ?1
+
+  spawn { actor(actorMb1, exitMb1, 1, sinkMb) };
+  spawn { actor(actorMb2, exitMb2, 2, sinkMb) };
+  spawn { actor(actorMb3, exitMb3, 3, sinkMb) };
+
+  let xs = (exitMb1 cons (exitMb2 cons (exitMb3 cons (nil : [ExitMb!])))) in sinkMb ! Actors(xs);
+
+  actorMb1 ! Neighbors(actorMb2, actorMb3); # actorMb1: ?Neighbors
+  actorMb2 ! Neighbors(actorMb1, actorMb3); # actorMb2: ?Neighbors
+  actorMb3 ! Neighbors(actorMb1, actorMb2); # actorMb3: ?Neighbors
+
+  actorMb1 ! Pong(0); # actorMb1: ?Neighbors . Pong
+  actorMb2 ! Pong(0); # actorMb2: ?Neighbors . Pong
+  actorMb3 ! Pong(0) # actorMb2: ?Neighbors . Pong
+}
+
+main()
diff --git a/test/examples/savina/lists/cig_smok.pat b/test/examples/savina/lists/cig_smok.pat
new file mode 100644
index 0000000..1243c22
--- /dev/null
+++ b/test/examples/savina/lists/cig_smok.pat
@@ -0,0 +1,146 @@
+### Adapted from Savina/cigsmok.
+###
+### A benchmark modelling n smokers and one arbiter that decides which smoker to
+### allow to smoke. The benchmark is parameterized by the number of smoker
+### processes.
+
+interface ArbiterMb {
+  Start(Int),
+  StartedSmoking()
+}
+
+interface SmokerMb {
+  StartSmoking(Int),
+  Exit()
+}
+
+def create_smokers(self: ArbiterMb?, moreSmokers: Int, acc: [SmokerMb!]): (ArbiterMb? * [SmokerMb!]) {
+    if (moreSmokers == 0) {
+        (self, acc)
+    }
+    else {
+        let newSmoker = new [SmokerMb] in
+            spawn { smoker(newSmoker, self) };
+            create_smokers(self, moreSmokers - 1, (newSmoker cons acc))
+        }
+}
+
+## Arbiter process handling the creation of smokers and launching of main loop.
+def arbiter(self: ArbiterMb?, numRounds: Int): Unit {
+
+  guard self: Start . (*StartedSmoking) {
+    receive Start(numSmokers) from self ->
+
+       let (self, smokerMbs) = create_smokers(self, numSmokers, (nil : [SmokerMb!])) in
+
+        let smokerMbs = notify_smoker(numSmokers, smokerMbs) in
+        arbiter_loop(self, numSmokers, numRounds, smokerMbs)
+  }
+}
+
+## Randomly chooses the smoker and requests it to smoke.
+def notify_smoker(numSmokers: Int, smokerMbs: [SmokerMb!]): [SmokerMb!] {
+
+  let smokerId = rand(numSmokers - 1) in
+  let sleepTimeMs = 1000 in
+
+  notify_aux(smokerId, sleepTimeMs, smokerMbs)
+}
+
+def notify_aux(choice: Int, time: Int, smokerMbs: [SmokerMb!]): [SmokerMb!] {
+if (choice == 0) {
+    caseL smokerMbs : [SmokerMb!]  of {
+        nil -> smokerMbs
+        | (mb cons mbs) ->
+            mb ! StartSmoking(rand(time));
+            smokerMbs
+    }
+}
+else {
+    caseL smokerMbs : [SmokerMb!] of {
+        nil -> smokerMbs
+        | (mb cons mbs) ->
+            let smokerMbs = notify_aux(choice - 1, time, mbs) in
+            (mb cons smokerMbs)
+    }
+}
+}
+
+## Notifies all smokers to terminate.
+def notify_smoker_exit(smokerMbs: [SmokerMb!]): [SmokerMb!] {
+    caseL smokerMbs : [SmokerMb!] of {
+        nil -> smokerMbs
+        | (mb cons mbs) ->
+            mb ! Exit();
+            notify_smoker_exit(mbs)
+        }
+}
+
+## Arbiter process main loop issuing start smoking requests and handling started
+## smoking replies.
+def arbiter_loop(self: ArbiterMb?, numSmokers: Int, numRounds: Int, smokerMbs: [SmokerMb!]): Unit {
+  guard self: *StartedSmoking {
+    free ->
+      ()
+    receive StartedSmoking() from self ->
+
+      # The if here introduces the internal choice, which means that on the
+      # receiver side I might or might not receive the message. In this case,
+      # the smoker might or might nor receive the Exit message, and must either
+      # use (Exit + 1) or (*Exit) in its pattern.
+
+      if (numRounds <= 0) {
+        let smokerMbs = notify_smoker_exit(smokerMbs) in
+            arbiter_loop(self, numSmokers, numRounds - 1, smokerMbs)
+      }
+      else {
+        let smokerMbs = notify_smoker(numSmokers, smokerMbs) in
+            arbiter_loop(self, numSmokers, numRounds - 1, smokerMbs)
+      }
+
+      # Arbiter needs to service all requests before, even if it has sent the
+      # Exit messages to smokers. Remember that smokers may still be processing
+      # StartSmoking messages, but the arbiter has already issued Exit messages
+      # and it still needs to await all the StartedSmoking replies before
+      # terminating. This is why we do not have an exit_arbiter flush function.
+
+  }
+}
+
+## Smoker process main loop handling start smoking requests and issuing started
+## smoking replies to/from the arbiter.
+def smoker(self: SmokerMb?, arbiterMb: ArbiterMb!): Unit {
+  # Smoker may be asked to smoke more than once, or none. This is why the *.
+  guard self: (*StartSmoking) . (*Exit) {
+    free ->
+      () # Since the smoker might not even receive an Exit/StartSmoking message due to the if condition above.
+    receive StartSmoking(ms) from self ->
+      arbiterMb ! StartedSmoking();
+      sleep(ms);
+      smoker(self, arbiterMb)
+    receive Exit() from self ->
+      smoker_exit(self)
+  }
+}
+
+## Smoker process exit procedure that flushes potential residual messages.
+def smoker_exit(self: SmokerMb?): Unit {
+  guard self: (*StartSmoking) . (*Exit) {
+    free -> () # In case I have one or more Exit/StartSmoking messages due to the if condition above.
+    receive StartSmoking(ms) from self ->
+      smoker_exit(self)
+    receive Exit() from self ->
+      smoker_exit(self)
+  }
+}
+
+## Launcher.
+def main(numSmokers : Int): Unit {
+
+  let arbiterMb = new [ArbiterMb] in
+  spawn { arbiter(arbiterMb, 10) };
+
+  arbiterMb ! Start(numSmokers)
+}
+
+main(5)
diff --git a/test/examples/savina/lists/kfork.pat b/test/examples/savina/lists/kfork.pat
new file mode 100644
index 0000000..a31ca97
--- /dev/null
+++ b/test/examples/savina/lists/kfork.pat
@@ -0,0 +1,69 @@
+### Adapted from Savina/fjthrput.
+###
+### Models the creation of n actors that are given a number of messages, for
+### each of which, a computation is performed. The benchmark is parameterized by
+### the number of actor processes.
+
+interface ActorMb {
+  Packet()
+}
+
+## Actor processes handling the packet requests.
+def actor(self: ActorMb?): Unit {
+  guard self: *Packet {
+    free ->
+      ()
+    receive Packet() from self ->
+      let dummy = fact(rand(100000)) in
+      actor(self)
+  }
+}
+
+## Computes the factorial of n.
+def fact(n: Int): Int {
+  if (n <= 0) {
+    1
+  }
+  else {
+    n * (fact(n - 1))
+  }
+}
+
+## Sends the given number of messages to the specified actor mailbox.
+def flood(numMessages: Int, actorMb: ActorMb!): Unit {
+  if (numMessages <= 0) {
+    ()
+  }
+  else {
+    actorMb ! Packet();
+    flood(numMessages - 1, actorMb)
+  }
+}
+
+def spawnActors(numActors: Int, acc: [ActorMb!]): [ActorMb!] {
+    if (numActors <= 0) {
+        acc
+    } else {
+        let newActor = new[ActorMb] in
+        spawn { actor(newActor) };
+        spawnActors(numActors - 1, (newActor cons acc))
+    }
+}
+
+def floodActors(numMessages: Int, actorMbs: [ActorMb!]): Unit {
+    caseL actorMbs : [ActorMb!] of {
+        nil -> ()
+      | (a cons as) ->
+            flood(numMessages, a);
+            floodActors(numMessages, as)
+        }
+}
+
+## Launcher.
+def main(numActors: Int): Unit {
+
+  let actorMbs = spawnActors(numActors, (nil : [ActorMb!])) in
+    floodActors(1000, actorMbs)
+}
+
+main(3)

From 4b3dc7717a4463fbbde347bca5091ef6fda653bc Mon Sep 17 00:00:00 2001
From: Simon Fowler <simon@simonjf.com>
Date: Thu, 8 May 2025 15:53:11 +0100
Subject: [PATCH 12/33] Fix #22 (#23)

This ensures that pattern variables are correctly substituted. It also
simplifies each HK solution prior to substitution in order to avoid
pattern blowup.
---
 lib/typecheck/solve_constraints.ml | 17 +++++++++++------
 1 file changed, 11 insertions(+), 6 deletions(-)

diff --git a/lib/typecheck/solve_constraints.ml b/lib/typecheck/solve_constraints.ml
index 010565b..6128592 100644
--- a/lib/typecheck/solve_constraints.ml
+++ b/lib/typecheck/solve_constraints.ml
@@ -97,40 +97,45 @@ let group_lower_bounds
    Finally, simplify the system.
  *)
 let substitute_solutions constrs =
+    let cmp (x1, _) (y1, _) = compare x1 y1 in
     (* Top-to-bottom *)
     let top_to_bottom =
-        List.fold_right (fun (var, pat) (map: Pattern.t stringmap) ->
+        List.fold_left (fun (map: Pattern.t stringmap) (var, pat) ->
             let hk_sol =
                 (* Apply current substitution map to pattern *)
                 Pattern.subst_all pat map
                 (* Compute HK solution *)
                 |> Pattern.hopkins_kozen_solution var
+                (* Simplify*)
+                |> Pattern.simplify
             in
             Settings.if_debug (fun () ->
                 Format.printf "HK Solution for %s: %a\n" var Pattern.pp hk_sol
             );
             PVarMap.add var hk_sol map
-        )  (PVarMap.bindings constrs) PVarMap.empty
+        ) PVarMap.empty (PVarMap.bindings constrs |> List.stable_sort (cmp))
     in
     (*
     Printf.printf "Top to bottom:\n";
         PVarMap.iter (fun k p ->
             Format.(fprintf std_formatter "%s: %a\n" k Pattern.pp p)
         ) top_to_bottom;
-        *)
+    *)
     (* Bottom to top *)
     let bottom_to_top =
-        List.fold_right (fun (var, pat) map ->
+        List.fold_left (fun map (var, pat) ->
             let pat = Pattern.subst_all pat map in
             PVarMap.add var pat map
-        ) (PVarMap.bindings top_to_bottom |> List.rev) PVarMap.empty
+        )
+         PVarMap.empty
+        (PVarMap.bindings top_to_bottom |> List.stable_sort (cmp) |> List.rev)
     in
     (*
     Printf.printf "Bottom to top:\n";
         PVarMap.iter (fun k p ->
             Format.(fprintf std_formatter "%s: %a\n" k Pattern.pp p)
         ) bottom_to_top;
-        *)
+    *)
     (* Simplify constraint system *)
     PVarMap.mapi (
         fun key pat ->

From c5520104a0f61e22bb2f18ff32646689ea24c8c6 Mon Sep 17 00:00:00 2001
From: Simon Fowler <simon@simonjf.com>
Date: Mon, 12 May 2025 09:37:30 +0100
Subject: [PATCH 13/33] add simpler communication aliasing example

---
 test/errors/simple_alias_comm.pat | 23 +++++++++++++++++++++++
 1 file changed, 23 insertions(+)
 create mode 100644 test/errors/simple_alias_comm.pat

diff --git a/test/errors/simple_alias_comm.pat b/test/errors/simple_alias_comm.pat
new file mode 100644
index 0000000..665ca35
--- /dev/null
+++ b/test/errors/simple_alias_comm.pat
@@ -0,0 +1,23 @@
+interface Self { Msg(Other!) }
+interface Other { Reply() }
+
+def interprocess(self: Self?, other1: Other!): Unit {
+    guard self : Msg {
+        receive Msg(other2) from self ->
+            other1 ! Reply();
+            free(self)
+    }
+}
+
+def main(): Unit {
+    let self = new[Self] in
+    let other = new[Other] in
+    spawn { interprocess(self, other) };
+    self ! Msg(other);
+    guard other : Reply {
+        receive Reply() from other ->
+            free(other)
+    }
+}
+
+main()

From edea1c1c561410af22462bd9abc8d3fc6e5d53dd Mon Sep 17 00:00:00 2001
From: Danielle Marshall <danielle@starsandspira.ls>
Date: Thu, 24 Jul 2025 10:52:55 +0100
Subject: [PATCH 14/33] update generate table to use list versions of
 benchmarks

---
 generate-table.py                      |   9 +-
 test/examples/savina/lists/banking.pat | 194 ++++++++++++++++++++-----
 2 files changed, 159 insertions(+), 44 deletions(-)
 mode change 100644 => 100755 generate-table.py

diff --git a/generate-table.py b/generate-table.py
old mode 100644
new mode 100755
index 04ceb74..e55380c
--- a/generate-table.py
+++ b/generate-table.py
@@ -16,13 +16,14 @@
         ("Ping Pong", os.path.join("test", "examples", "savina", "ping_pong_strict.pat")),
         ("Thread Ring", os.path.join("test", "examples", "savina", "thread_ring.pat")),
         ("Counter", os.path.join("test", "examples", "savina", "count.pat")),
-        ("K-Fork", os.path.join("test", "examples", "savina", "kfork.pat")),
+        ("K-Fork", os.path.join("test", "examples", "savina", "lists", "kfork.pat")),
         ("Fibonacci", os.path.join("test", "examples", "savina", "fib.pat")),
-        ("Big", os.path.join("test", "examples", "savina", "big.pat")),
+        ("Big", os.path.join("test", "examples", "savina", "lists", "big.pat")),
         ("Philosopher", os.path.join("test", "examples", "savina", "philosopher.pat")),
-        ("Smokers", os.path.join("test", "examples", "savina", "cig_smok.pat")),
+        ("Smokers", os.path.join("test", "examples", "savina", "lists", "cig_smok.pat")),
         ("Log Map", os.path.join("test", "examples", "savina", "log_map.pat")),
-        ("Transaction", os.path.join("test", "examples", "savina", "banking.pat"))
+        ("Transaction", os.path.join("test", "examples", "savina", "lists", "banking.pat")),
+	("Barber", os.path.join("test", "examples", "savina", "lists", "barber.pat")),
      ]
 
 # Tries to run in strict mode -- returns True if it works, False otherwise
diff --git a/test/examples/savina/lists/banking.pat b/test/examples/savina/lists/banking.pat
index 30572be..35dca7c 100644
--- a/test/examples/savina/lists/banking.pat
+++ b/test/examples/savina/lists/banking.pat
@@ -1,61 +1,175 @@
-### Adapted from Savina/fjthrput.
+### Adapted from Savina/banking.
 ###
-### Models the creation of n actors that are given a number of messages, for
-### each of which, a computation is performed. The benchmark is parameterized by
-### the number of actor processes. Since the array type is not available in
-### Pat, we fix the number of actor processes to 3.
+### A benchmark that implements a request-reply chain passing scenario. Several
+### account processes are spawned, each of which may be sent a credit request
+### by the central teller process. The benchmark is parameterized by the number
+### of account processes.
 
-interface ActorMb {
-  Packet()
+interface TellerMb {
+  Start(),
+  Reply()
 }
 
-## Actor processes handling the packet requests.
-def actor(self: ActorMb?): Unit {
-  guard self: *Packet {
-    free ->
-      ()
-    receive Packet() from self ->
-      let dummy = fact(rand(100000)) in
-      actor(self)
-  }
+interface AccountMb {
+  Debit(AccountMb!, Int),
+  Credit(TellerMb!, Int, AccountMb!),
+  Done(),
+  Stop()
 }
 
-## Computes the factorial of n.
-def fact(n: Int): Int {
-  if (n <= 0) {
-    1
+def spawnAccounts(self: TellerMb?, numsAccounts: [Int], soFar: Int, acc: [AccountMb!]) : (TellerMb? * [AccountMb!]) {
+  caseL numsAccounts : [Int] of {
+    nil -> (self, acc)
+    | (n cons ns) ->
+        let accountMb = new [AccountMb] in
+        spawn { account(accountMb, soFar, n)};
+        spawnAccounts(self, ns, soFar + 1, (accountMb cons acc))
+    }
   }
-  else {
-    n * (fact(n - 1))
+
+## Teller process handling the creation of account processes and launching of
+## main loop.
+def teller(self: TellerMb?, numAccounts : Int, numsAccounts: [Int]): Unit {
+
+  let (self, accountMbs) = spawnAccounts(self, numsAccounts, 1, (nil : [AccountMb!])) in
+
+  guard self: Start {
+    receive Start() from self ->
+
+      # Note. Even if the randomization of message sending is performed in a
+      # different processes, there is no risk of a race condition where the
+      # messages are sent to a non-existing mailbox. This is because, as can be
+      # gleaned above, mailboxes are created in sequential fashion within this
+      # (i.e., the teller) process.
+      spawn { generate_work(self, numAccounts, accountMbs) } ;
+      teller_loop(self, accountMbs)
   }
 }
 
-## Sends the given number of messages to the specified actor mailbox.
-def flood(numMessages: Int, actorMb: ActorMb!): Unit {
-  if (numMessages <= 0) {
-    ()
+## Randomly chooses the source account.
+def generate_work(tellerMb: TellerMb!, numAccounts: Int, accs : [AccountMb!]): Unit {
+
+  # Randomly choose source account from which the funds shall be taken.
+  let sourceId = rand(numAccounts - 1) in # -1 because rand() is 0-indexed.
+
+  let (choice, rest) = pick(accs, sourceId, (nil : [AccountMb!])) in
+  choose_dst_acc(tellerMb, numAccounts, choice, rest)
+}
+
+def pick(accs : [AccountMb!], index : Int, rest : [AccountMb!]) : ([AccountMb!] * [AccountMb!]) {
+if (index == 0) {
+    caseL accs : [AccountMb!] of {
+        nil -> ((nil : [AccountMb!]), rest)
+        | (a cons as) -> ((a cons (nil : [AccountMb!])), append(rest, as))
+    }}
+else {
+    caseL accs : [AccountMb!] of {
+        nil ->  ((nil : [AccountMb!]), rest)
+        | (a cons as) -> pick(as, index - 1, (a cons rest))
+    }}
+}
+
+def append(l1 : [AccountMb!], l2: [AccountMb!]) : [AccountMb!] {
+    caseL l1 : [AccountMb!] of {
+        nil -> l2
+        | (a cons as) -> append(as, (a cons l2))
+    }
+}
+
+## Randomly chooses the destination account and issues a credit request. The
+## function ensures that the source and destination account are different.
+def choose_dst_acc(tellerMb: TellerMb!, numAccounts: Int, srcAccountMb: [AccountMb![R]], dstAccountMbs : [AccountMb!]): Unit {
+
+  # Randomly choose destination account to which funds shall be deposited. -2
+  # because rand() is 0-indexed, and because we do not include the source
+  # account in the random choice (i.e., the source account is not permitted to
+  # send funds to itself).
+  let dstAccountId = rand(numAccounts - 2) in
+
+  let (dstAccount, rest) = (pick(dstAccountMbs, dstAccountId, (nil : [AccountMb!])) : ([AccountMb!] * [AccountMb!]))
+  in
+
+  let amount = rand(200) in
+    caseL srcAccountMb : [AccountMb!] of {
+    nil -> caseL dstAccount : [AccountMb!] of {
+        nil -> ()
+        | (d cons ds) -> ()
+    }
+    | (a cons as) -> caseL dstAccount : [AccountMb!] of {
+        nil -> ()
+        | (d cons ds) -> d ! Credit(tellerMb, amount, a)
+    }
   }
-  else {
-    actorMb ! Packet();
-    flood(numMessages - 1, actorMb)
+}
+
+## Teller process main loop handling replies from accounts.
+def teller_loop(self: TellerMb?, accountMbs : [AccountMb!]): Unit {
+  guard self: *Reply {
+    free ->
+      # All credit requests serviced. Stop accounts.
+      stopAccounts(accountMbs)
+    receive Reply() from self ->
+      teller_loop(self, accountMbs)
   }
 }
 
-## Launcher.
-def main(): Unit {
+def stopAccounts(accs: [AccountMb!]) : Unit {
+    caseL accs : [AccountMb!] of {
+        nil -> ()
+        | (a cons as) ->
+            a ! Stop();
+            stopAccounts(as)
+        }
+}
+
+## Account process handling credit requests issued by the teller, and debit
+## requests issued by other accounts.
+def account(self: AccountMb?, id: Int, balance: Int): Unit {
+  guard self: *(Debit + Credit) . Stop {
+    free ->
+      ()
+    receive Debit(accountMb, amount) from self ->
 
-  let actorMb1 = new [ActorMb] in
-  spawn { actor(actorMb1) };
+      accountMb ! Done();
+      account(self, id, balance + amount)
+    receive Credit(tellerMb, amount, accountMb) from self ->
 
-  let actorMb2 = new [ActorMb] in
-  spawn { actor(actorMb2) };
+      # A more uglier implementation would have been to use the 'global mailbox
+      # way' where all messages are collected in one mailbox.
+      let transMb = new [AccountMb] in
+      accountMb ! Debit(transMb, amount);
 
-  let actorMb3 = new [ActorMb] in
-  spawn { actor(actorMb3) };
+      guard transMb: Done + 1{
+        free ->
+          account(self, id, balance)
+        receive Done() from transMb ->
+          free(transMb);
+          tellerMb ! Reply();
+          account(self, id, balance - amount)
+      }
+
+    receive Stop() from self ->
+      account_exit(self)
+  }
+}
+
+## Actor process exit procedure that flushes potential residual messages.
+def account_exit(self: AccountMb?): Unit {
+  guard self: *(Debit + Credit)  {
+    free -> ()
+    receive Debit(accountMb, amount) from self ->
+      account_exit(self)
+    receive Credit(tellerMb, amount, accountMb) from self ->
+      account_exit(self)
+  }
+}
+
+## Launcher.
+def main(): Unit {
+  let tellerMb = new [TellerMb] in
+  spawn { teller(tellerMb, 3, (200 cons (150 cons (50 cons (nil : [Int]))))) };
 
-  flood(100, actorMb1);
-  flood(1000, actorMb1);
-  flood(10000, actorMb1)
+  tellerMb ! Start()
 }
 
 main()

From 1b36a8480c6f173e84bc02165b737a747e7e208e Mon Sep 17 00:00:00 2001
From: Simon Fowler <simon@simonjf.com>
Date: Thu, 24 Jul 2025 11:28:31 +0100
Subject: [PATCH 15/33] fix issue with type join on lists

---
 lib/common/sugar_ast.ml |  6 +++---
 lib/typecheck/ty_env.ml | 31 ++++---------------------------
 2 files changed, 7 insertions(+), 30 deletions(-)

diff --git a/lib/common/sugar_ast.ml b/lib/common/sugar_ast.ml
index f6b2475..35c6619 100644
--- a/lib/common/sugar_ast.ml
+++ b/lib/common/sugar_ast.ml
@@ -247,15 +247,15 @@ and pp_expr ppf expr_with_pos =
             (pp_print_comma_list Type.pp) ts
             pp_expr term
             pp_expr cont
-    | Nil -> pp_print_string ppf "Nil"
+    | Nil -> pp_print_string ppf "nil"
     | Cons (e1, e2) ->
-        fprintf ppf "Cons %a %a" pp_expr e1 pp_expr e2
+        fprintf ppf "cons %a %a" pp_expr e1 pp_expr e2
     | CaseL { term; ty = t1; nil = e1; cons = ((b1, b2), e2) } -> begin
       match t1 with
         | List t ->
 	          fprintf
             ppf
-            "caseL %a : %a of {@[@[nil -> [@%a@]@]][cons %a %a -> [@%a@]@]@]]}"
+            "caseL %a : %a of {@[@[nil -> @[%a@]@]@]@[cons %a %a -> @[%a@]@]@]}"
             pp_expr term
             Type.pp t1
             pp_expr e1
diff --git a/lib/typecheck/ty_env.ml b/lib/typecheck/ty_env.ml
index c3a80b1..599e788 100644
--- a/lib/typecheck/ty_env.ml
+++ b/lib/typecheck/ty_env.ml
@@ -55,7 +55,7 @@ let join : Interface_env.t -> t -> t -> Position.t -> t * Constraint_set.t =
                         ((In, pat), constrs)
         in
 
-        let join_types (var: Ir.Var.t) (t1: Type.t) (t2: Type.t) : (Type.t * Constraint_set.t) =
+        let rec join_types (var: Ir.Var.t) (t1: Type.t) (t2: Type.t) : (Type.t * Constraint_set.t) =
             let open Type in
             match (t1, t2) with
                 | Base b1, Base b2 when b1 = b2 ->
@@ -97,32 +97,9 @@ let join : Interface_env.t -> t -> t -> Position.t -> t * Constraint_set.t =
                               pattern = Some pat;
                               quasilinearity = ql
                           }, constrs
-                | List (Mailbox { capability = cap1; interface = iface1; pattern =
-                    Some pat1; quasilinearity = ql1 }),
-                  List (Mailbox { capability = cap2; interface = iface2; pattern =
-                      Some pat2; quasilinearity = ql2 }) ->
-                      (* We can only join variables with the same interface
-                         name. If these match, we can join the types. *)
-                      if iface1 <> iface2 then
-                          Gripers.env_interface_mismatch true
-                            t1 t2 var iface1 iface2 [pos]
-                      else
-                          (* Check sequencing of QL *)
-                          let ql =
-                              match Quasilinearity.sequence ql1 ql2 with
-                                | Some ql -> ql
-                                | None ->
-                                    Gripers.invalid_ql_sequencing var [pos]
-                          in
-                          let ((cap, pat), constrs) =
-                              join_mailbox_types var
-                                (cap1, pat1) (cap2, pat2) in
-                          Mailbox {
-                              capability = cap;
-                              interface = iface1;
-                              pattern = Some pat;
-                              quasilinearity = ql
-                          }, constrs
+                | List ty1, List ty2 ->
+                    let ty, constrs = join_types var ty1 ty2 in
+                    List ty, constrs
                 | _, _ ->
                     Gripers.type_mismatch true t1 t2 var [pos]
         in

From 18aa69438a892d4858212c4a2c20c16f7849851e Mon Sep 17 00:00:00 2001
From: Simon Fowler <simon@simonjf.com>
Date: Thu, 24 Jul 2025 12:17:10 +0100
Subject: [PATCH 16/33] get banking working

---
 lib/common/pretype.ml                  | 13 ++++---------
 lib/typecheck/gen_constraints.ml       | 21 ++++++---------------
 lib/typecheck/gripers.ml               |  8 --------
 lib/typecheck/pretypecheck.ml          |  9 ++++-----
 lib/typecheck/solve_constraints.ml     |  6 ++++++
 test/examples/savina/lists/banking.pat |  2 +-
 test/tests.json                        |  5 +++++
 7 files changed, 26 insertions(+), 38 deletions(-)

diff --git a/lib/common/pretype.ml b/lib/common/pretype.ml
index 171d3a1..48ba145 100644
--- a/lib/common/pretype.ml
+++ b/lib/common/pretype.ml
@@ -9,9 +9,7 @@ open Util.Utility
 
 type t =
     | PBase of base
-    (* Functions are always annotated with argument types.
-       The codomain is a pretype, since it is not in binding position. *)
-    | PFun of { linear: bool; args: (Type.t[@name "ty"]) list; result: t[@name "pretype"] }
+    | PFun of { linear: bool; args: (Type.t[@name "ty"]) list; result: (Type.t[@name "ty"]) }
     | PInterface of string
     | PSum of (t * t)
     | PTuple of t list
@@ -32,7 +30,7 @@ let rec pp ppf =
         fprintf ppf "(%a) %s %a"
             (pp_print_comma_list Type.pp) args
             arrow
-            pp result
+            Type.pp result
     | PTuple ts ->
         let pp_star ppf () = pp_print_string ppf " * " in
         fprintf ppf "(%a)"
@@ -54,7 +52,7 @@ let show t =
 let rec of_type = function
     | Type.Base b -> PBase b
     | Type.Fun { linear; args; result } ->
-        PFun { linear; args; result = of_type result }
+        PFun { linear; args; result = result }
     | Type.Tuple ts -> PTuple (List.map of_type ts)
     | Type.Sum (t1, t2) -> PSum (of_type t1, of_type t2)
     | Type.List t -> PList (of_type t)
@@ -67,10 +65,7 @@ let rec of_type = function
 let rec to_type = function
     | PBase b -> Some (Type.Base b)
     | PFun { linear; args; result } ->
-        Option.bind (to_type result)
-        (fun result ->
-            Some (Type.Fun { linear; args; result })
-        )
+        Some (Type.Fun { linear; args; result })
     | PTuple ts ->
         let rec go acc =
             function
diff --git a/lib/typecheck/gen_constraints.ml b/lib/typecheck/gen_constraints.ml
index b741e35..019670b 100644
--- a/lib/typecheck/gen_constraints.ml
+++ b/lib/typecheck/gen_constraints.ml
@@ -60,20 +60,9 @@ let rec synthesise_val :
                         ty, Ty_env.singleton v ty, Constraint_set.empty
                     (* In limited circumstances we can use a pretype annotation to
                        synthesise a function *)
-                    | _, PFun { linear; args; result = PBase b } ->
-                        let ty = Type.function_type linear args (Type.Base b) in
+                    | _, PFun { linear; args; result } ->
+                        let ty = Type.function_type linear args result in
                         ty, Ty_env.singleton v ty, Constraint_set.empty
-                    (* Units *)
-                    | _, PFun { linear; args; result = PTuple [] } ->
-                            let ty = Type.function_type linear args (Type.Tuple []) in
-                        ty, Ty_env.singleton v ty, Constraint_set.empty
-                    | _, PFun _ ->
-                        Gripers.synth_mailbox_function v [pos]
-                    (* Although we have an interface pretype annotation, it's not possible
-                       to reliably infer a mailbox type (even with a fresh constraint) since
-                       we don't, a priori, know the capability. Even if we record the initial
-                       capability, it may be used at different 'modes' throughout the function,
-                       so any inference would in effect be a guess. *)
                     | _, _ ->
                         Gripers.synth_variable v [pos]
             end
@@ -159,8 +148,10 @@ and check_val :
         match ty, pty with
             | Mailbox { interface; _ }, PInterface iname when interface = iname -> ()
             | Base b1, PBase b2 when b1 = b2 -> ()
-            | Fun { result = rty; _ }, PFun { result = rpty; _ } ->
-                check_pretype_consistency rty rpty
+            | Fun _, PFun _ -> 
+                (* Function pretypes are now fully typed, so any errors will be
+                   picked up in constraint generation or constraint resolution. *)
+                ()
             | Tuple ts, PTuple pts ->
                 List.combine ts pts
                 |> List.iter (uncurry check_pretype_consistency)
diff --git a/lib/typecheck/gripers.ml b/lib/typecheck/gripers.ml
index cefc40f..7374589 100644
--- a/lib/typecheck/gripers.ml
+++ b/lib/typecheck/gripers.ml
@@ -12,14 +12,6 @@ let synth_variable v pos_list =
     in
     raise (constraint_gen_error ~subsystem:(Errors.GenSynth) msg pos_list)
 
-let synth_mailbox_function v pos_list =
-    let msg =
-        Format.asprintf
-            "Cannot synthesise type for variable %a: can only synthesise types for functions which return a base type" Ir.Var.pp_name v
-    in
-    raise (constraint_gen_error ~subsystem:(Errors.GenSynth) msg pos_list)
-
-
 let subtype_cap_mismatch t1 t2 pos_list =
     let msg =
       Format.asprintf
diff --git a/lib/typecheck/pretypecheck.ml b/lib/typecheck/pretypecheck.ml
index e26b8cc..abea6e0 100644
--- a/lib/typecheck/pretypecheck.ml
+++ b/lib/typecheck/pretypecheck.ml
@@ -161,14 +161,13 @@ let rec synthesise_val ienv env value : (value * Pretype.t) =
                     (fun (b, ty) -> Var.of_binder b, Pretype.of_type ty)
                     parameters
             in
-            let result_prety = Pretype.of_type result_type in
             let env = PretypeEnv.bind_many pretype_params env in
-            let body = check_comp ienv env body result_prety in
+            let body = check_comp ienv env body (Pretype.of_type result_type) in
             wrap (Lam { linear; parameters; body; result_type }),
             Pretype.PFun {
                 linear = linear;
                 args = param_types;
-                result = result_prety
+                result = result_type 
             }
         | Inl _ | Inr _ -> Gripers.cannot_synth_sum value
         | Nil -> Gripers.cannot_synth_nil value
@@ -317,7 +316,7 @@ and synthesise_comp ienv env comp =
                     check_val ienv env arg arg_ty)
             in
             (* Synthesise result type *)
-            WithPos.make ~pos(App { func; args }), result_ann
+            WithPos.make ~pos(App { func; args }), Pretype.of_type result_ann
         | Send { target; message = (tag, vals); _ } ->
             let open Pretype in
             (* Typecheck target *)
@@ -466,7 +465,7 @@ let check { prog_interfaces; prog_decls; prog_body } =
                 Pretype.PFun {
                     linear = false;
                     args = param_tys;
-                    result = Pretype.of_type d.decl_return_type
+                    result = d.decl_return_type
                 })) (WithPos.extract_list_node prog_decls)
         |> PretypeEnv.from_list
     in
diff --git a/lib/typecheck/solve_constraints.ml b/lib/typecheck/solve_constraints.ml
index 6128592..3d4583a 100644
--- a/lib/typecheck/solve_constraints.ml
+++ b/lib/typecheck/solve_constraints.ml
@@ -437,6 +437,12 @@ let pipeline constrs =
            to rid ourselves of pattern variables *)
         substitute_solutions lbs
     in
+    Settings.if_debug (fun () ->
+        Printf.printf "=== Simplified constraint set ===\n\n";
+        PVarMap.iter (fun k p ->
+            Format.(fprintf std_formatter "%s: %a\n" k Pattern.pp p)
+        ) resolved_constraints
+    );
     (* Check if solutions are satisfiable *)
     check_satisfiability resolved_constraints (get_upper_bounds constrs);
     (* Ensure that none of the pattern variables have been solved as zero *)
diff --git a/test/examples/savina/lists/banking.pat b/test/examples/savina/lists/banking.pat
index 35dca7c..f3ab09d 100644
--- a/test/examples/savina/lists/banking.pat
+++ b/test/examples/savina/lists/banking.pat
@@ -86,7 +86,7 @@ def choose_dst_acc(tellerMb: TellerMb!, numAccounts: Int, srcAccountMb: [Account
   # send funds to itself).
   let dstAccountId = rand(numAccounts - 2) in
 
-  let (dstAccount, rest) = (pick(dstAccountMbs, dstAccountId, (nil : [AccountMb!])) : ([AccountMb!] * [AccountMb!]))
+  let (dstAccount, rest) = (pick(dstAccountMbs, dstAccountId, (nil : [AccountMb!])) : ([AccountMb!Credit] * [AccountMb!1]))
   in
 
   let amount = rand(200) in
diff --git a/test/tests.json b/test/tests.json
index d579605..57d1ddc 100644
--- a/test/tests.json
+++ b/test/tests.json
@@ -22,6 +22,11 @@
                     "name": "Linear function (bad #3: unused linear function)",
                     "filename": "pat-tests/linfun-bad-3.pat",
                     "exit_code": 1
+                },
+                {
+                    "name": "Function returning a mailbox type",
+                    "filename": "pat-tests/mb-function-return.pat",
+                    "exit_code": 0
                 }
             ]
         },

From 77f07f10652a6cdda23e74e2d1c342a45af3a119 Mon Sep 17 00:00:00 2001
From: Simon Fowler <simon@simonjf.com>
Date: Thu, 24 Jul 2025 14:01:26 +0100
Subject: [PATCH 17/33] fix linearity issue with cig_smok

---
 lib/common/type.ml                      |  7 +++++++
 lib/typecheck/ty_env.ml                 | 22 +++++++++++-----------
 test/examples/savina/lists/cig_smok.pat | 10 +++++-----
 3 files changed, 23 insertions(+), 16 deletions(-)

diff --git a/lib/common/type.ml b/lib/common/type.ml
index 1f951af..61b03cc 100644
--- a/lib/common/type.ml
+++ b/lib/common/type.ml
@@ -375,6 +375,13 @@ let is_output_mailbox = function
     | Mailbox { capability = Out; pattern = Some _; _ } -> true
     | _ -> false
 
+let rec contains_output_mailbox = function
+    | Mailbox { capability = Out; pattern = Some _; _} -> true
+    | Sum (t1, t2) -> contains_output_mailbox t1 || contains_output_mailbox t2
+    | Tuple ts -> List.exists contains_output_mailbox ts
+    | List t -> contains_output_mailbox t
+    | _ -> false
+
 let is_tuple = function
     | Tuple _ -> true
     | _ -> false
diff --git a/lib/typecheck/ty_env.ml b/lib/typecheck/ty_env.ml
index 599e788..56641c9 100644
--- a/lib/typecheck/ty_env.ml
+++ b/lib/typecheck/ty_env.ml
@@ -257,24 +257,24 @@ let intersect : t -> t -> Position.t -> t * Constraint_set.t =
             let disjoints =
               let (disjoint_sends, disjoint_others) =
                 List.partition (fun (_, ty) ->
-                  Type.is_output_mailbox ty
+                  Type.contains_output_mailbox ty
                 ) (disjoint1 @ disjoint2)
               in
-              (* !E becomes !(E + 1) *)
-              let disjoint_sends =
-                List.map (fun (var, ty) ->
-                  let ty =
-                    match ty with
-                      | Mailbox { capability = Out; interface; quasilinearity; pattern = Some pat } ->
+              (* Relaxes a mailbox type from !E to !(E+1) *)
+              let rec relax_send_type = function
+                | Mailbox { capability = Out; interface; quasilinearity; pattern = Some pat } ->
                           let pat = Pattern.Plus (pat, Pattern.One) in
                           Mailbox { capability = Out; interface; quasilinearity; pattern = Some pat }
-                      | _ ->
-                          raise (Errors.internal_error "ty_env.ml" "error in disjoint MB combination")
-                  in
+                | List ty -> List (relax_send_type ty)
+                | _ ->
+                  raise (Errors.internal_error "ty_env.ml" "error in disjoint MB combination")
+              in
+              let disjoint_sends =
+                List.map (fun (var, ty) ->
+                  let ty = relax_send_type ty in
                   (var, ty)
                 ) disjoint_sends
               in
-
               let () =
                 List.iter (fun (var, ty) ->
                     if Type.is_lin ty then
diff --git a/test/examples/savina/lists/cig_smok.pat b/test/examples/savina/lists/cig_smok.pat
index 1243c22..be070ef 100644
--- a/test/examples/savina/lists/cig_smok.pat
+++ b/test/examples/savina/lists/cig_smok.pat
@@ -49,16 +49,16 @@ def notify_smoker(numSmokers: Int, smokerMbs: [SmokerMb!]): [SmokerMb!] {
 
 def notify_aux(choice: Int, time: Int, smokerMbs: [SmokerMb!]): [SmokerMb!] {
 if (choice == 0) {
-    caseL smokerMbs : [SmokerMb!]  of {
-        nil -> smokerMbs
+    caseL smokerMbs : [SmokerMb!(1 + StartSmoking)]  of {
+        nil -> nil
         | (mb cons mbs) ->
             mb ! StartSmoking(rand(time));
-            smokerMbs
+            (mb cons mbs)
     }
 }
 else {
     caseL smokerMbs : [SmokerMb!] of {
-        nil -> smokerMbs
+        nil -> nil
         | (mb cons mbs) ->
             let smokerMbs = notify_aux(choice - 1, time, mbs) in
             (mb cons smokerMbs)
@@ -69,7 +69,7 @@ else {
 ## Notifies all smokers to terminate.
 def notify_smoker_exit(smokerMbs: [SmokerMb!]): [SmokerMb!] {
     caseL smokerMbs : [SmokerMb!] of {
-        nil -> smokerMbs
+        nil -> nil
         | (mb cons mbs) ->
             mb ! Exit();
             notify_smoker_exit(mbs)

From 14c98e25b75408df7833f6d031adb07f42f6f244 Mon Sep 17 00:00:00 2001
From: Danielle Marshall <danielle@starsandspira.ls>
Date: Thu, 24 Jul 2025 15:28:50 +0100
Subject: [PATCH 18/33] fix up cig_smok

---
 test/examples/savina/lists/cig_smok.pat | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

diff --git a/test/examples/savina/lists/cig_smok.pat b/test/examples/savina/lists/cig_smok.pat
index be070ef..68b5015 100644
--- a/test/examples/savina/lists/cig_smok.pat
+++ b/test/examples/savina/lists/cig_smok.pat
@@ -49,7 +49,7 @@ def notify_smoker(numSmokers: Int, smokerMbs: [SmokerMb!]): [SmokerMb!] {
 
 def notify_aux(choice: Int, time: Int, smokerMbs: [SmokerMb!]): [SmokerMb!] {
 if (choice == 0) {
-    caseL smokerMbs : [SmokerMb!(1 + StartSmoking)]  of {
+    caseL smokerMbs : [SmokerMb!]  of {
         nil -> nil
         | (mb cons mbs) ->
             mb ! StartSmoking(rand(time));
@@ -81,7 +81,10 @@ def notify_smoker_exit(smokerMbs: [SmokerMb!]): [SmokerMb!] {
 def arbiter_loop(self: ArbiterMb?, numSmokers: Int, numRounds: Int, smokerMbs: [SmokerMb!]): Unit {
   guard self: *StartedSmoking {
     free ->
-      ()
+      caseL smokerMbs : [SmokerMb!] of {
+      nil -> ()
+      | (a cons as) -> ()
+  }
     receive StartedSmoking() from self ->
 
       # The if here introduces the internal choice, which means that on the

From 8dfe75b5b8126c7cc9972d52715226b2b3744338 Mon Sep 17 00:00:00 2001
From: Danielle Marshall <danielle@starsandspira.ls>
Date: Wed, 22 Oct 2025 12:42:41 +0100
Subject: [PATCH 19/33] add in missing list examples

---
 generate-table.py                      |   2 +-
 test/examples/savina/lists/barber.pat  | 160 +++++++++++++++++++++++--
 test/examples/savina/lists/robotsn.pat | 145 ++++++++++++++++++++++
 3 files changed, 295 insertions(+), 12 deletions(-)
 create mode 100644 test/examples/savina/lists/robotsn.pat

diff --git a/generate-table.py b/generate-table.py
index e55380c..61b54c0 100755
--- a/generate-table.py
+++ b/generate-table.py
@@ -3,7 +3,7 @@
 import subprocess
 from tabulate import tabulate
 
-REPETITIONS = 100
+REPETITIONS = 1000
 
 BENCHMARKS =\
     [
diff --git a/test/examples/savina/lists/barber.pat b/test/examples/savina/lists/barber.pat
index 5b86aa8..36b24d2 100644
--- a/test/examples/savina/lists/barber.pat
+++ b/test/examples/savina/lists/barber.pat
@@ -1,4 +1,4 @@
-### Adapted from savina/barber.
+### Adapted from savina/barber. 
 ###
 ### A barber is waiting for customers. When there are no customers the barber sleeps. When a customer
 ### arrives, he wakes the barber or sits in one of the waiting chairs in the waiting room. If all chairs
@@ -8,42 +8,180 @@
 ### that decides which is the next customer, Customer actors, a Barber actor and a Room actor.
 
 interface RoomMb {
-    Enter(CustomerMb!, RoomMb!),
+    Enter(CustomerMb!),
     Next(),
     Exit()
 }
 
 interface BarberMb {
     Enter(CustomerMb!, RoomMb!),
-    Wait(),
     Exit()
 }
 
 interface SelectorMb {
     Start(),
-    Returned(CustomerMb!),
-    Done()
+    Returned(CustomerMb!)
 }
 
 interface CustomerMb {
-    Full(),
-    Wait(),
-    Start(),
-    Done()
+    Full(RoomMb!),
+    Start(RoomMb!),
+    Done(),
+    Exit()
 }
 
-def room(self: RoomMb?, capacity: Int, barber: BarberMb!): Unit {
+def room(self: RoomMb?, capacity: Int, waiters: [CustomerMb!], waiting: Int, barber: BarberMb!): Unit {
+    guard self: *(Enter + Next + Exit) {
+        free -> ()
+        receive Enter(customerMb) from self ->
+            if (waiting == capacity) {
+                customerMb ! Full(self);
+                room(self, capacity, waiters, waiting, barber)
+            }
+            else {
+                sleep(5);
+                room(self, capacity, (customerMb cons waiters), (waiting + 1), barber)
+            }
+        receive Next() from self ->
+            caseL waiters : [CustomerMb!] of {
+                nil ->
+                    sleep(5);
+                    room(self, capacity, (nil : [CustomerMb!]), waiting, barber)
+                | (a cons as) -> 
+                    barber ! Enter(a, self);
+                    room(self, capacity, as, (waiting - 1), barber)
+            }
+        receive Exit() from self ->
+            barber ! Exit();
+            roomExit(self)
+    }
+}
 
+def roomExit(self : RoomMb?) : Unit {
+    guard self: *(Enter + Next + Exit) {
+        free -> ()
+        receive Enter(customerMb) from self -> roomExit(self)
+        receive Next() from self -> roomExit(self)
+        receive Exit() from self -> roomExit(self)
+    }
 }
 
 def barber(self: BarberMb?): Unit {
+    guard self: *(Enter + Exit) {
+        free -> ()
+        receive Enter(customerMb, roomMb) from self ->
+            sleep(10);
+            customerMb ! Done();
+            roomMb ! Next();
+            barber(self)
+        receive Exit() from self ->
+            barberExit(self)
+    }
+}
+
+def barberExit(self : BarberMb?) : Unit {
+    guard self: *(Enter + Exit) {
+        free -> ()
+        receive Enter(customerMb, roomMb) from self -> barberExit(self)
+        receive Exit() from self -> barberExit(self)
+    }
+}
+
+def spawnCustomers(self: SelectorMb?, generator: Int, soFar: Int, acc : [CustomerMb!]): (SelectorMb? * [CustomerMb!]) {
+    if (soFar == generator) {
+            (self, acc)
+        }
+    else {
+        let customerMb = new [CustomerMb] in
+        spawn { customer(customerMb, self)};
+        spawnCustomers(self, generator, (soFar + 1), (customerMb cons acc))
+    }
+}
 
+def startCustomers(customerMbs : [CustomerMb!], room : RoomMb!) : Unit {
+    caseL customerMbs : [CustomerMb!] of {
+        nil -> ()
+        | (a cons as) ->
+            a ! Start(room);
+            startCustomers(as, room)
+    } 
 }
 
-def selector(self: SelectorMb?, generator: Int, haircuts: Int, room: RoomMb!): Unit {
+def doneCustomers(customerMbs : [CustomerMb!]) : Unit {
+    caseL customerMbs : [CustomerMb!] of {
+        nil -> ()
+        | (a cons as) ->
+            a ! Done();
+            doneCustomers(as)
+    } 
+}
+
+def selector(self: SelectorMb?, generator: Int, haircuts: Int, target: Int, customers : [CustomerMb!], room: RoomMb!): Unit {
+    guard self: *(Start + Returned) {
+        free -> ()
+        receive Start() from self ->
+            let (self, newCustomers) = spawnCustomers(self, generator, 0, (nil : [CustomerMb!])) in
+            startCustomers(customers, room);
+            selector(self, generator, haircuts, target, newCustomers, room)
+        receive Returned(customerMb) from self ->
+            let newHaircuts = haircuts + 1 in
+            if (newHaircuts == target) {
+                doneCustomers(customers);
+                room ! Exit();
+                selectorExit(self)
+            }
+            else {
+                customerMb ! Start(room);
+                selector(self, generator, newHaircuts, target, customers, room)
+            }
+    }
+}
 
+def selectorExit(self : SelectorMb?) : Unit {
+    guard self: *(Start + Returned) {
+        free -> ()
+        receive Start() from self -> selectorExit(self)
+        receive Returned(customerMb) from self -> selectorExit(self)
+    }
 }
 
 def customer(self: CustomerMb?, selector: SelectorMb!): Unit {
+    guard self: *(Full + Start + Done + Exit) {
+        free -> ()
+        receive Full(room) from self ->
+            sleep(10);
+            self ! Start(room);
+            customer(self, selector)
+        receive Start(room) from self ->
+            room ! Enter(self);
+            customer(self, selector)
+        receive Done() from self ->
+            selector ! Returned(self);
+            customer(self, selector)
+        receive Exit() from self ->
+            customerExit(self)
+    }
+}
+
+def customerExit(self : CustomerMb?) : Unit {
+    guard self: *(Full + Start + Done + Exit) {
+        free -> ()
+        receive Full(room) from self -> customerExit(self)
+        receive Start(room) from self -> customerExit(self)
+        receive Done() from self -> customerExit(self)
+        receive Exit() from self -> customerExit(self)
+    }
+}
+
+def main() : Unit {
+    let barberMb = new [BarberMb] in
+    spawn {barber(barberMb)};
+
+    let roomMb = new [RoomMb] in
+    spawn {room(roomMb, 2, (nil : [CustomerMb!]), 0, barberMb)};
+
+    let selectorMb = new [SelectorMb] in
+    spawn {selector(selectorMb, 4, 0, 6, (nil : [CustomerMb!]), roomMb)};
 
+    selectorMb ! Start()
 }
diff --git a/test/examples/savina/lists/robotsn.pat b/test/examples/savina/lists/robotsn.pat
new file mode 100644
index 0000000..bcd8696
--- /dev/null
+++ b/test/examples/savina/lists/robotsn.pat
@@ -0,0 +1,145 @@
+interface Door {
+    Want(Int, Robot!),
+    Inside(Robot!),
+    Prepared(Warehouse!),
+    WantLeave(Robot!),
+    Outside(),
+    TableIdle(Warehouse!)
+}
+
+interface Robot {
+    GoIn(Door!),
+    GoOut(Door!),
+    Busy(),
+    Delivered(Warehouse!, Door!)
+}
+
+interface Warehouse {
+    Prepare(Int, Door!),
+    Deliver(Robot!, Door!),
+    PartTaken()
+}
+
+# Door
+def freeDoor(self: Door?, warehouse: Warehouse!): Unit {
+    guard self : *Want {
+        free -> ()
+        receive Want(part, robot) from self ->
+            robot ! GoIn(self);
+            warehouse ! Prepare(part, self);
+            busyDoor(self)
+    }
+}
+
+def busyDoor(self: Door?): Unit {
+    guard self : Inside . Prepared . *Want {
+        receive Want(partNum, robot) from self ->
+            robot ! Busy();
+            busyDoor(self)
+        receive Inside(robot) from self ->
+            guard self : Prepared . *Want {
+                receive Prepared(warehouse) from self ->
+                    warehouse ! Deliver(robot, self);
+                    guard self : WantLeave . TableIdle . *Want {
+                        receive WantLeave(robot) from self ->
+                            robot ! GoOut(self);
+                            finaliseDoor(self, warehouse)
+                    }
+            }
+    }
+}
+
+def finaliseDoor(self: Door?, warehouse: Warehouse!): Unit {
+    guard self : Outside . TableIdle . *Want {
+        receive Outside() from self ->
+            guard self : TableIdle . *Want {
+                receive TableIdle(warehouse) from self ->
+                    freeDoor(self, warehouse)
+            }
+        receive TableIdle(warehouse) from self ->
+            guard self : Outside . *Want {
+                receive Outside() from self ->
+                    freeDoor(self, warehouse)
+            }
+    }
+}
+
+# Robot
+def idleRobot(self: Robot?, door: Door!): Unit {
+    door ! Want(0, self);
+    guard self : (Busy + GoIn) {
+        receive Busy() from self -> free(self)
+        receive GoIn(door) from self ->
+            door ! Inside(self);
+            insideRobot(self)
+    }
+}
+
+def insideRobot(self: Robot?): Unit {
+    let self =
+        guard self : Delivered {
+            receive Delivered(warehouse, door) from self ->
+                warehouse ! PartTaken();
+                door ! WantLeave(self);
+                self
+        }
+    in
+    guard self : GoOut {
+        receive GoOut(door) from self ->
+            door ! Outside();
+            free(self)
+    }
+}
+
+# Warehouse
+def freeWarehouse(self: Warehouse?): Unit {
+    guard self : Prepare + 1 {
+        free -> ()
+        receive Prepare(partNum, door) from self ->
+            door ! Prepared(self);
+            preparedWarehouse(self)
+    }
+}
+
+def preparedWarehouse(self: Warehouse?): Unit {
+    guard self : Deliver {
+        receive Deliver(robot, door) from self ->
+            robot ! Delivered(self, door);
+            handlePartTaken(self, door)
+    }
+}
+
+def handlePartTaken(self: Warehouse?, door: Door!): Unit {
+    guard self : PartTaken {
+        receive PartTaken() from self ->
+            door ! TableIdle(self);
+            freeWarehouse(self)
+    }
+}
+
+def discardList(xs: [Robot!]) : Unit {
+    caseL xs : [Robot!] of {
+        nil -> ()
+        | (a cons as) -> discardList(as)
+    }
+}
+
+def spawnRobots(numRobots: Int, door: Door!, acc: [Robot!]): Unit {
+    if (numRobots <= 0) {
+        discardList(acc)
+    } else {
+        let newRobot = new[Robot] in
+        spawn { idleRobot(newRobot, door) };
+        spawnRobots(numRobots - 1, door, (newRobot cons acc))
+    }
+}
+
+def main(n: Int): Unit {
+    let door = new[Door] in
+    let warehouse = new[Warehouse] in
+    spawn { freeDoor(door, warehouse) };
+    spawnRobots(n, door, (nil : [Robot!]));
+    spawn { freeWarehouse(warehouse) }
+}
+
+main(3)

From ad11a4886fe2cb6873840fe34fc8e1157b5bf28f Mon Sep 17 00:00:00 2001
From: Danielle Marshall <danielle@starsandspira.ls>
Date: Wed, 22 Oct 2025 12:52:15 +0100
Subject: [PATCH 20/33] update syntax of patterns in list examples

---
 test/examples/savina/lists/banking.pat  |  6 +++---
 test/examples/savina/lists/barber.pat   | 16 ++++++++--------
 test/examples/savina/lists/big.pat      | 10 +++++-----
 test/examples/savina/lists/cig_smok.pat |  8 ++++----
 test/examples/savina/lists/kfork.pat    |  2 +-
 test/examples/savina/lists/robotsn.pat  | 14 +++++++-------
 6 files changed, 28 insertions(+), 28 deletions(-)

diff --git a/test/examples/savina/lists/banking.pat b/test/examples/savina/lists/banking.pat
index f3ab09d..c498376 100644
--- a/test/examples/savina/lists/banking.pat
+++ b/test/examples/savina/lists/banking.pat
@@ -104,7 +104,7 @@ def choose_dst_acc(tellerMb: TellerMb!, numAccounts: Int, srcAccountMb: [Account
 
 ## Teller process main loop handling replies from accounts.
 def teller_loop(self: TellerMb?, accountMbs : [AccountMb!]): Unit {
-  guard self: *Reply {
+  guard self: Reply* {
     free ->
       # All credit requests serviced. Stop accounts.
       stopAccounts(accountMbs)
@@ -125,7 +125,7 @@ def stopAccounts(accs: [AccountMb!]) : Unit {
 ## Account process handling credit requests issued by the teller, and debit
 ## requests issued by other accounts.
 def account(self: AccountMb?, id: Int, balance: Int): Unit {
-  guard self: *(Debit + Credit) . Stop {
+  guard self: (Debit + Credit)* . Stop {
     free ->
       ()
     receive Debit(accountMb, amount) from self ->
@@ -155,7 +155,7 @@ def account(self: AccountMb?, id: Int, balance: Int): Unit {
 
 ## Actor process exit procedure that flushes potential residual messages.
 def account_exit(self: AccountMb?): Unit {
-  guard self: *(Debit + Credit)  {
+  guard self: (Debit + Credit)*  {
     free -> ()
     receive Debit(accountMb, amount) from self ->
       account_exit(self)
diff --git a/test/examples/savina/lists/barber.pat b/test/examples/savina/lists/barber.pat
index 36b24d2..533b038 100644
--- a/test/examples/savina/lists/barber.pat
+++ b/test/examples/savina/lists/barber.pat
@@ -31,7 +31,7 @@ interface CustomerMb {
 }
 
 def room(self: RoomMb?, capacity: Int, waiters: [CustomerMb!], waiting: Int, barber: BarberMb!): Unit {
-    guard self: *(Enter + Next + Exit) {
+    guard self: (Enter + Next + Exit)* {
         free -> ()
         receive Enter(customerMb) from self ->
             if (waiting == capacity) {
@@ -58,7 +58,7 @@ def room(self: RoomMb?, capacity: Int, waiters: [CustomerMb!], waiting: Int, bar
 }
 
 def roomExit(self : RoomMb?) : Unit {
-    guard self: *(Enter + Next + Exit) {
+    guard self: (Enter + Next + Exit)* {
         free -> ()
         receive Enter(customerMb) from self -> roomExit(self)
         receive Next() from self -> roomExit(self)
@@ -67,7 +67,7 @@ def roomExit(self : RoomMb?) : Unit {
 }
 
 def barber(self: BarberMb?): Unit {
-    guard self: *(Enter + Exit) {
+    guard self: (Enter + Exit)* {
         free -> ()
         receive Enter(customerMb, roomMb) from self ->
             sleep(10);
@@ -80,7 +80,7 @@ def barber(self: BarberMb?): Unit {
 }
 
 def barberExit(self : BarberMb?) : Unit {
-    guard self: *(Enter + Exit) {
+    guard self: (Enter + Exit)* {
         free -> ()
         receive Enter(customerMb, roomMb) from self -> barberExit(self)
         receive Exit() from self -> barberExit(self)
@@ -117,7 +117,7 @@ def doneCustomers(customerMbs : [CustomerMb!]) : Unit {
 }
 
 def selector(self: SelectorMb?, generator: Int, haircuts: Int, target: Int, customers : [CustomerMb!], room: RoomMb!): Unit {
-    guard self: *(Start + Returned) {
+    guard self: (Start + Returned)* {
         free -> ()
         receive Start() from self ->
             let (self, newCustomers) = spawnCustomers(self, generator, 0, (nil : [CustomerMb!])) in
@@ -138,7 +138,7 @@ def selector(self: SelectorMb?, generator: Int, haircuts: Int, target: Int, cust
 }
 
 def selectorExit(self : SelectorMb?) : Unit {
-    guard self: *(Start + Returned) {
+    guard self: (Start + Returned)* {
         free -> ()
         receive Start() from self -> selectorExit(self)
         receive Returned(customerMb) from self -> selectorExit(self)
@@ -146,7 +146,7 @@ def selectorExit(self : SelectorMb?) : Unit {
 }
 
 def customer(self: CustomerMb?, selector: SelectorMb!): Unit {
-    guard self: *(Full + Start + Done + Exit) {
+    guard self: (Full + Start + Done + Exit)* {
         free -> ()
         receive Full(room) from self ->
             sleep(10);
@@ -164,7 +164,7 @@ def customer(self: CustomerMb?, selector: SelectorMb!): Unit {
 }
 
 def customerExit(self : CustomerMb?) : Unit {
-    guard self: *(Full + Start + Done + Exit) {
+    guard self: (Full + Start + Done + Exit)* {
         free -> ()
         receive Full(room) from self -> customerExit(self)
         receive Start(room) from self -> customerExit(self)
diff --git a/test/examples/savina/lists/big.pat b/test/examples/savina/lists/big.pat
index 8755521..3d521ab 100644
--- a/test/examples/savina/lists/big.pat
+++ b/test/examples/savina/lists/big.pat
@@ -22,7 +22,7 @@ interface SinkMb {
 
 ## Actor process handling the launching of main loop.
 def actor(self: ActorMb?, exitMb : ExitMb?, id: Int, sinkMb: SinkMb!): Unit {
-  guard self: Neighbors . *(Pong + Ping)  {
+  guard self: Neighbors . (Pong + Ping)*  {
     receive Neighbors(actorMb1, actorMb2) from self ->
       actor_loop(self, exitMb, id, sinkMb, 100, actorMb1, actorMb2)
   }
@@ -38,7 +38,7 @@ def await_exit(exitMb: ExitMb?): Unit {
 
 ## Actor process main loop issuing ping requests and handling pong replies.
 def actor_loop(self: ActorMb?, exitMb: ExitMb?, id: Int, sinkMb: SinkMb!, numPings: Int, actorMb1: ActorMb!, actorMb2: ActorMb!): Unit {
-  guard self: *(Ping + Pong) {
+  guard self: (Ping + Pong)* {
     free ->
       await_exit(exitMb)
     receive Ping(pingerId) from self ->
@@ -67,7 +67,7 @@ def actor_loop(self: ActorMb?, exitMb: ExitMb?, id: Int, sinkMb: SinkMb!, numPin
 
 ## Actor process exit procedure that flushes potential residual messages.
 def actor_exit(self: ActorMb?): Unit {
-  guard self: (*Ping) . (*Pong) {
+  guard self: (Ping*) . (Pong*) {
     free -> ()
     receive Ping(pingerId) from self ->
       actor_exit(self)
@@ -105,7 +105,7 @@ def send_ping(id: Int, actorMb1: ActorMb!, actorMb2: ActorMb!): Unit {
 
 ## Sink process that coordinates actor termination.
 def sink(self: SinkMb?): Unit {
-  guard self: Actors . (*Done) {
+  guard self: Actors . (Done*) {
     receive Actors(exitMbs) from self ->
       sink_loop(self, exitMbs)
   }
@@ -113,7 +113,7 @@ def sink(self: SinkMb?): Unit {
 
 ## Sink process main loop issuing termination messages.
 def sink_loop(self: SinkMb?, exitMbs : [ExitMb!]): Unit {
-  guard self: *Done {
+  guard self: Done* {
     free ->
       # Notify all actors. Placing the sends in this clause ensures that
       # each actor is notified once.
diff --git a/test/examples/savina/lists/cig_smok.pat b/test/examples/savina/lists/cig_smok.pat
index 68b5015..ea51dda 100644
--- a/test/examples/savina/lists/cig_smok.pat
+++ b/test/examples/savina/lists/cig_smok.pat
@@ -28,7 +28,7 @@ def create_smokers(self: ArbiterMb?, moreSmokers: Int, acc: [SmokerMb!]): (Arbit
 ## Arbiter process handling the creation of smokers and launching of main loop.
 def arbiter(self: ArbiterMb?, numRounds: Int): Unit {
 
-  guard self: Start . (*StartedSmoking) {
+  guard self: Start . (StartedSmoking*) {
     receive Start(numSmokers) from self ->
 
        let (self, smokerMbs) = create_smokers(self, numSmokers, (nil : [SmokerMb!])) in
@@ -79,7 +79,7 @@ def notify_smoker_exit(smokerMbs: [SmokerMb!]): [SmokerMb!] {
 ## Arbiter process main loop issuing start smoking requests and handling started
 ## smoking replies.
 def arbiter_loop(self: ArbiterMb?, numSmokers: Int, numRounds: Int, smokerMbs: [SmokerMb!]): Unit {
-  guard self: *StartedSmoking {
+  guard self: StartedSmoking* {
     free ->
       caseL smokerMbs : [SmokerMb!] of {
       nil -> ()
@@ -114,7 +114,7 @@ def arbiter_loop(self: ArbiterMb?, numSmokers: Int, numRounds: Int, smokerMbs: [
 ## smoking replies to/from the arbiter.
 def smoker(self: SmokerMb?, arbiterMb: ArbiterMb!): Unit {
   # Smoker may be asked to smoke more than once, or none. This is why the *.
-  guard self: (*StartSmoking) . (*Exit) {
+  guard self: (StartSmoking*) . (Exit*) {
     free ->
       () # Since the smoker might not even receive an Exit/StartSmoking message due to the if condition above.
     receive StartSmoking(ms) from self ->
@@ -128,7 +128,7 @@ def smoker(self: SmokerMb?, arbiterMb: ArbiterMb!): Unit {
 
 ## Smoker process exit procedure that flushes potential residual messages.
 def smoker_exit(self: SmokerMb?): Unit {
-  guard self: (*StartSmoking) . (*Exit) {
+  guard self: (StartSmoking*) . (Exit*) {
     free -> () # In case I have one or more Exit/StartSmoking messages due to the if condition above.
     receive StartSmoking(ms) from self ->
       smoker_exit(self)
diff --git a/test/examples/savina/lists/kfork.pat b/test/examples/savina/lists/kfork.pat
index a31ca97..ca269b8 100644
--- a/test/examples/savina/lists/kfork.pat
+++ b/test/examples/savina/lists/kfork.pat
@@ -10,7 +10,7 @@ interface ActorMb {
 
 ## Actor processes handling the packet requests.
 def actor(self: ActorMb?): Unit {
-  guard self: *Packet {
+  guard self: Packet* {
     free ->
       ()
     receive Packet() from self ->
diff --git a/test/examples/savina/lists/robotsn.pat b/test/examples/savina/lists/robotsn.pat
index bcd8696..5eea045 100644
--- a/test/examples/savina/lists/robotsn.pat
+++ b/test/examples/savina/lists/robotsn.pat
@@ -22,7 +22,7 @@ interface Warehouse {
 
 # Door
 def freeDoor(self: Door?, warehouse: Warehouse!): Unit {
-    guard self : *Want {
+    guard self : Want* {
         free -> ()
         receive Want(part, robot) from self ->
             robot ! GoIn(self);
@@ -32,15 +32,15 @@ def freeDoor(self: Door?, warehouse: Warehouse!): Unit {
 }
 
 def busyDoor(self: Door?): Unit {
-    guard self : Inside . Prepared . *Want {
+    guard self : Inside . Prepared . Want* {
         receive Want(partNum, robot) from self ->
             robot ! Busy();
             busyDoor(self)
         receive Inside(robot) from self ->
-            guard self : Prepared . *Want {
+            guard self : Prepared . Want* {
                 receive Prepared(warehouse) from self ->
                     warehouse ! Deliver(robot, self);
-                    guard self : WantLeave . TableIdle . *Want {
+                    guard self : WantLeave . TableIdle . Want* {
                         receive WantLeave(robot) from self ->
                             robot ! GoOut(self);
                             finaliseDoor(self, warehouse)
@@ -50,14 +50,14 @@ def busyDoor(self: Door?): Unit {
 }
 
 def finaliseDoor(self: Door?, warehouse: Warehouse!): Unit {
-    guard self : Outside . TableIdle . *Want {
+    guard self : Outside . TableIdle . Want* {
         receive Outside() from self ->
-            guard self : TableIdle . *Want {
+            guard self : TableIdle . Want* {
                 receive TableIdle(warehouse) from self ->
                     freeDoor(self, warehouse)
             }
         receive TableIdle(warehouse) from self ->
-            guard self : Outside . *Want {
+            guard self : Outside . Want* {
                 receive Outside() from self ->
                     freeDoor(self, warehouse)
             }

From 069002dc39759b5cc9cd73062729ef5f328a42e2 Mon Sep 17 00:00:00 2001
From: Simon Fowler <simon@simonjf.com>
Date: Wed, 12 Nov 2025 15:41:54 +0000
Subject: [PATCH 21/33] minor

---
 lib/common/type.ml | 11 ++++++-----
 1 file changed, 6 insertions(+), 5 deletions(-)

diff --git a/lib/common/type.ml b/lib/common/type.ml
index 61b03cc..6ae92ae 100644
--- a/lib/common/type.ml
+++ b/lib/common/type.ml
@@ -27,9 +27,10 @@ module Quasilinearity = struct
        to be returnable.
      *)
     let is_sub x1 x2 =
-        match x1, x2 with
-            | Returnable, Usable -> true
-            | x1, x2 -> x1 = x2
+        (Settings.(get disable_quasilinearity)) ||
+            match x1, x2 with
+                | Returnable, Usable -> true
+                | x1, x2 -> x1 = x2
 
     let max ql1 ql2 =
         if ql1 = Returnable || ql2 = Returnable then
@@ -440,5 +441,5 @@ let make_tuple_type tys =
 let make_sum_type ty1 ty2 =
     Sum (make_returnable ty1, make_returnable ty2)
 
-let make_list_type ty1 =
-    List (make_returnable ty1)
+let make_list_type ty =
+    List (make_returnable ty)

From 91e04799894f30425d7eb0914a17662c2b96b71d Mon Sep 17 00:00:00 2001
From: Simon Fowler <simon@simonjf.com>
Date: Wed, 12 Nov 2025 17:08:20 +0000
Subject: [PATCH 22/33] Liberalise quasilinearity for lists

It should be possible for lists to be able to contain usable mailbox
variables, but only if the 'cons' case is statically guaranteed not to
contain any unsafe aliases. This is the same problem as with Receive, so
we can adopt the same solution.
---
 lib/common/type.ml               |  5 +--
 lib/typecheck/gen_constraints.ml | 66 +++++++++-----------------------
 lib/typecheck/gripers.ml         |  4 +-
 lib/typecheck/ty_env.ml          | 41 ++++++++++++++++++++
 lib/typecheck/ty_env.mli         |  5 +++
 test/errors/uaf_lists.pat        | 20 ++++++++++
 6 files changed, 88 insertions(+), 53 deletions(-)
 create mode 100644 test/errors/uaf_lists.pat

diff --git a/lib/common/type.ml b/lib/common/type.ml
index 6ae92ae..e5a16c6 100644
--- a/lib/common/type.ml
+++ b/lib/common/type.ml
@@ -419,7 +419,7 @@ let rec make_returnable = function
     | Mailbox m -> Mailbox { m with quasilinearity = Quasilinearity.Returnable }
     | Tuple ts -> Tuple (List.map make_returnable ts)
     | Sum (t1, t2) -> Sum (make_returnable t1, make_returnable t2)
-    | List t -> List (make_returnable t)
+    (* | List t -> List (make_returnable t) *)
     | t -> t
 
 let is_unr = is_lin >> not
@@ -441,5 +441,4 @@ let make_tuple_type tys =
 let make_sum_type ty1 ty2 =
     Sum (make_returnable ty1, make_returnable ty2)
 
-let make_list_type ty =
-    List (make_returnable ty)
+let make_list_type ty = List ty
diff --git a/lib/typecheck/gen_constraints.ml b/lib/typecheck/gen_constraints.ml
index 019670b..9e4abee 100644
--- a/lib/typecheck/gen_constraints.ml
+++ b/lib/typecheck/gen_constraints.ml
@@ -450,6 +450,11 @@ and check_comp : IEnv.t -> Ty_env.t -> Ir.comp -> Type.t -> Ty_env.t * Constrain
             in
             (env, constrs)
         | CaseL { term; ty = ty1; nil = comp1; cons = ((bnd1, bnd2), comp2) } ->
+            let elem_ty =
+                match ty1 with
+                    | Type.List elem_ty -> elem_ty
+                    | _ -> Gripers.expected_list_type ty1 [pos]
+            in
             (* Check that scrutinee has annotated list type *)
             let (term_env, term_constrs) =
                 check_val ienv decl_env term ty1
@@ -458,13 +463,17 @@ and check_comp : IEnv.t -> Ty_env.t -> Ir.comp -> Type.t -> Ty_env.t * Constrain
             let (comp1_env, comp1_constrs) = chk comp1 ty in
             (* Next, check that comp2 (cons case) has expected return type *)
             let (comp2_env, comp2_constrs) = chk comp2 ty in
-            (* Next, check that the inferred types in comp2_env match annotations *)
+            (* Next, check that the inferred types in comp2_env match annotations and that
+               the cons case doesn't contain any troublesome mailbox variables that could 
+               introduce unsafe aliasing *)
             let var1 = Var.of_binder bnd1 in
-            let var2 = Var.of_binder bnd2 in
-            let elem_ty =
-                match ty1 with
-                    | Type.List elem_ty -> elem_ty
-                    | _ -> Gripers.expected_list_type ty1 [pos]
+            let var2 = Var.of_binder bnd2 in 
+            let comp2_env_no_binders = Ty_env.delete_many [var1; var2] comp2_env in
+            (* If element type is returnable, we know it's the last lexical occurrence 
+               and we don't need this check. *)
+            let () =
+                if (not (Type.is_returnable elem_ty)) then
+                    Ty_env.check_free_mailbox_variables [elem_ty] comp2_env_no_binders
             in
             let env_constrs =
                 Constraint_set.union
@@ -475,7 +484,8 @@ and check_comp : IEnv.t -> Ty_env.t -> Ir.comp -> Type.t -> Ty_env.t * Constrain
             let isect_env, isect_constrs =
                 Ty_env.intersect
                   comp1_env
-                  (Ty_env.delete_many [var1; var2] comp2_env) pos
+                  comp2_env_no_binders
+                  pos
             in
             (* Finally combine the term env with the intersected env *)
             let env, combine_constrs =
@@ -815,47 +825,7 @@ and check_guard :
                   List.fold_right (Ty_env.delete_binder) payload_binders env
                   |> Ty_env.delete_binder mailbox_binder
                 in
-                (* If we are receiving a mailbox variable, without a dependency
-                   graph, we must do some fairly coarse-grained aliasing
-                   control.
-                   There are three strategies:
-                      1. Strict: the environment must be entirely unrestricted
-                          (i.e., no other mailbox variables are free in the receive
-                          block)
-
-                      2. Interface: the environment cannot contain a variable of
-                          the same interface. This means that we know we won't
-                          accidentally alias, without being overly restrictive.
-
-                      3. Nothing: No alias control: permissive, but unsafe.
-                  *)
-                let () =
-                    let mb_iface_tys =
-                        List.filter_map (fun ty ->
-                            if Type.is_mailbox_type ty then
-                                Some (Type.get_interface ty)
-                            else None)
-                        payload_iface_tys
-                    in
-                    let open Settings in
-                    let open ReceiveTypingStrategy in
-                    match get receive_typing_strategy with
-                        | Strict ->
-                            Ty_env.iter (fun v ty ->
-                                if Type.is_lin ty then
-                                    Gripers.unrestricted_recv_env v ty [pos]
-                            ) env
-                        | Interface ->
-                            Ty_env.iter (fun v ty ->
-                                match ty with
-                                    | Mailbox { interface; _ } when (List.mem interface mb_iface_tys) ->
-                                        Gripers.duplicate_interface_receive_env
-                                        v interface
-                                        [pos]
-                                    | _ -> ()
-                            ) env
-                        | Nothing -> ()
-                in
+                Ty_env.check_free_mailbox_variables payload_iface_tys env;
                 (* Calculate the derivative wrt. the tag, and ensure via a
                    constraint that it is included in the calculated payload
                    type. *)
diff --git a/lib/typecheck/gripers.ml b/lib/typecheck/gripers.ml
index 7374589..21e4d3a 100644
--- a/lib/typecheck/gripers.ml
+++ b/lib/typecheck/gripers.ml
@@ -228,7 +228,7 @@ let guard_send_return_type ty pos_list =
 let unrestricted_recv_env var ty pos_list =
     let msg =
         Format.asprintf
-            "The body of a receive guard cannot contain free linear capabilities, but variable %a has type %a."
+            "The body of a receive guard or case expression cannot contain free mailbox variables, but variable %a has type %a."
             Ir.Var.pp_name var Type.pp ty
     in
     raise (constraint_gen_error ~subsystem:Errors.GenCheckGuard msg pos_list)
@@ -308,7 +308,7 @@ let let_not_returnable ty pos_list =
 let duplicate_interface_receive_env var iface pos_list =
     let msg =
         Format.asprintf
-            "To prevent unsafe aliasing, no other variables of the same interface as a received variable may be present in the body of a receive guard. However, variable %a also has interface name %s."
+            "To prevent unsafe aliasing, no other variables of the same interface as a received variable may be present in the body of a receive guard or a case expression. However, variable %a also has interface name %s."
             Ir.Var.pp_name var
             iface
     in
diff --git a/lib/typecheck/ty_env.ml b/lib/typecheck/ty_env.ml
index 56641c9..14b67bd 100644
--- a/lib/typecheck/ty_env.ml
+++ b/lib/typecheck/ty_env.ml
@@ -319,3 +319,44 @@ let make_unrestricted env pos =
     List.fold_left (fun acc (_, ty) ->
         Constraint_set.union acc (make_unrestricted ty pos)
     ) Constraint_set.empty (bindings env)
+
+(* If we are receiving a mailbox variable, without a dependency
+   graph, we must do some fairly coarse-grained aliasing
+   control when receiving from a mailbox or deconstructing a list.
+   There are three strategies:
+      1. Strict: the environment must be entirely unrestricted
+          (i.e., no other mailbox variables are free in the receive
+          block)
+
+      2. Interface: the environment cannot contain a variable of
+          the same interface. This means that we know we won't
+          accidentally alias, without being overly restrictive.
+
+      3. Nothing: No alias control: permissive, but unsafe.
+  *)
+let check_free_mailbox_variables bound_variable_types env =
+    let mb_iface_tys =
+        List.filter_map (fun ty ->
+            if Type.is_mailbox_type ty then
+                Some (Type.get_interface ty)
+            else None)
+        bound_variable_types
+    in
+    let open Settings in
+    let open ReceiveTypingStrategy in
+    match get receive_typing_strategy with
+        | Strict ->
+            iter (fun v ty ->
+                if Type.is_lin ty then
+                    Gripers.unrestricted_recv_env v ty []
+            ) env
+        | Interface ->
+            iter (fun v ty ->
+                match ty with
+                    | Type.Mailbox { interface; _ } when (List.mem interface mb_iface_tys) ->
+                        Gripers.duplicate_interface_receive_env
+                        v interface
+                        []
+                    | _ -> ()
+            ) env
+        | Nothing -> ()
diff --git a/lib/typecheck/ty_env.mli b/lib/typecheck/ty_env.mli
index d73323c..378179e 100644
--- a/lib/typecheck/ty_env.mli
+++ b/lib/typecheck/ty_env.mli
@@ -47,3 +47,8 @@ val make_unrestricted : t -> Position.t -> Constraint_set.t
     the environment.
  *)
 val check_type : Interface_env.t -> Ir.Var.t -> Type.t -> t -> Position.t -> Constraint_set.t
+
+(** Checks to see whether the environment contains any free variables with mailbox type,
+    depending on the current typechecking policy (strict, interface, none). Raises an
+    exception if so. *)
+val check_free_mailbox_variables : Type.t list -> t -> unit
diff --git a/test/errors/uaf_lists.pat b/test/errors/uaf_lists.pat
new file mode 100644
index 0000000..58d4d76
--- /dev/null
+++ b/test/errors/uaf_lists.pat
@@ -0,0 +1,20 @@
+interface Test { M(Test!1) }
+
+def drain(x: Test?): Unit {
+    guard x : M* {
+        free -> ()
+        receive M(y) from z -> drain(z)
+    }
+}
+
+def go(): Unit {
+    let x = new[Test] in
+    let xs = (x cons (nil: [Test![U]])) in
+    caseL xs : [Test!] of {
+          nil -> ()
+        | (a cons as) -> x ! M(a)
+    };
+    drain(x)
+}
+
+go()

From 5abbda08d91b634763020a70db20e54ace8506c5 Mon Sep 17 00:00:00 2001
From: Danielle Marshall <danielle@starsandspira.ls>
Date: Thu, 13 Nov 2025 12:24:23 +0000
Subject: [PATCH 23/33] use sum type instead of list for single chosen mailbox
 in banking example

---
 test/examples/savina/lists/banking.pat | 52 +++++++++++++-------------
 1 file changed, 26 insertions(+), 26 deletions(-)

diff --git a/test/examples/savina/lists/banking.pat b/test/examples/savina/lists/banking.pat
index c498376..bfbaff4 100644
--- a/test/examples/savina/lists/banking.pat
+++ b/test/examples/savina/lists/banking.pat
@@ -56,15 +56,15 @@ def generate_work(tellerMb: TellerMb!, numAccounts: Int, accs : [AccountMb!]): U
   choose_dst_acc(tellerMb, numAccounts, choice, rest)
 }
 
-def pick(accs : [AccountMb!], index : Int, rest : [AccountMb!]) : ([AccountMb!] * [AccountMb!]) {
+def pick(accs : [AccountMb!], index : Int, rest : [AccountMb!]) : ((Unit + AccountMb!) * [AccountMb!]) {
 if (index == 0) {
     caseL accs : [AccountMb!] of {
-        nil -> ((nil : [AccountMb!]), rest)
-        | (a cons as) -> ((a cons (nil : [AccountMb!])), append(rest, as))
+        nil -> let x = () in (inl(x) : (Unit + AccountMb!), rest)
+        | (a cons as) -> (inr(a) : (Unit + AccountMb!), append(rest, as))
     }}
 else {
     caseL accs : [AccountMb!] of {
-        nil ->  ((nil : [AccountMb!]), rest)
+        nil ->  let x = () in (inl(x) : (Unit + AccountMb!), rest)
         | (a cons as) -> pick(as, index - 1, (a cons rest))
     }}
 }
@@ -78,28 +78,28 @@ def append(l1 : [AccountMb!], l2: [AccountMb!]) : [AccountMb!] {
 
 ## Randomly chooses the destination account and issues a credit request. The
 ## function ensures that the source and destination account are different.
-def choose_dst_acc(tellerMb: TellerMb!, numAccounts: Int, srcAccountMb: [AccountMb![R]], dstAccountMbs : [AccountMb!]): Unit {
-
-  # Randomly choose destination account to which funds shall be deposited. -2
-  # because rand() is 0-indexed, and because we do not include the source
-  # account in the random choice (i.e., the source account is not permitted to
-  # send funds to itself).
-  let dstAccountId = rand(numAccounts - 2) in
-
-  let (dstAccount, rest) = (pick(dstAccountMbs, dstAccountId, (nil : [AccountMb!])) : ([AccountMb!Credit] * [AccountMb!1]))
-  in
-
-  let amount = rand(200) in
-    caseL srcAccountMb : [AccountMb!] of {
-    nil -> caseL dstAccount : [AccountMb!] of {
-        nil -> ()
-        | (d cons ds) -> ()
-    }
-    | (a cons as) -> caseL dstAccount : [AccountMb!] of {
-        nil -> ()
-        | (d cons ds) -> d ! Credit(tellerMb, amount, a)
-    }
-  }
+def choose_dst_acc(tellerMb: TellerMb!, numAccounts: Int, srcAccount: (Unit + AccountMb!), dstAccountMbs : [AccountMb!]): Unit {
+
+  (# Randomly choose destination account to which funds shall be deposited. -2
+    # because rand() is 0-indexed, and because we do not include the source
+    # account in the random choice (i.e., the source account is not permitted to
+    # send funds to itself).
+    let dstAccountId = rand(numAccounts - 2) in
+  
+    let (dstAccount, rest) = (pick(dstAccountMbs, dstAccountId, (nil : [AccountMb!])) : ((Unit + AccountMb!Credit) * [AccountMb!1]))
+    in
+  
+    (let amount = rand(200) in
+          case srcAccount : (Unit + AccountMb!) of {
+          inl(u1) : Unit -> case dstAccount : (Unit + AccountMb!) of {
+              inl(u2) : Unit -> ()
+              | inr(d) : AccountMb! -> ()
+          }
+          | inr(a) : AccountMb! -> case dstAccount : (Unit + AccountMb!) of {
+              inl(u) : Unit -> ()
+              | inr(d) : AccountMb! -> d ! Credit(tellerMb, amount, a)
+          }
+        }))
 }
 
 ## Teller process main loop handling replies from accounts.

From d3c78e6931a600783b1ccec69ac0427fbaf54390 Mon Sep 17 00:00:00 2001
From: Simon Fowler <simon@simonjf.com>
Date: Tue, 18 Nov 2025 14:45:35 +0000
Subject: [PATCH 24/33] get banking working

---
 lib/frontend/insert_pattern_variables.ml | 22 ++++++++++++++++++++++
 lib/typecheck/ty_env.ml                  | 12 ++++++++++++
 test/examples/savina/lists/banking.pat   | 18 +++++++++---------
 3 files changed, 43 insertions(+), 9 deletions(-)

diff --git a/lib/frontend/insert_pattern_variables.ml b/lib/frontend/insert_pattern_variables.ml
index fe5a44b..cb1a3bf 100644
--- a/lib/frontend/insert_pattern_variables.ml
+++ b/lib/frontend/insert_pattern_variables.ml
@@ -82,6 +82,28 @@ let visitor =
                 let new_body = self#visit_expr env body in
                 let new_lam = Lam { linear; parameters; result_type; body = new_body } in
                 { expr_with_pos with node = new_lam }
+            | Let { annot = Some ty; binder; term; body } ->
+                let ty = annotate_type ty in
+                let term = self#visit_expr env term in
+                let body = self#visit_expr env body in
+                let new_let = Let { annot = Some ty; binder; term; body } in
+                { expr_with_pos with node = new_let }
+            | LetTuple { annot = Some tys; binders; term; cont } ->
+                let tys = List.map annotate_type tys in
+                let term = self#visit_expr env term in
+                let cont = self#visit_expr env cont in
+                let new_let = LetTuple { annot = Some tys; binders; term; cont } in
+                { expr_with_pos with node = new_let }
+            | Case { term; branch1 = ((bnd1, ty1), e1); branch2 = ((bnd2, ty2), e2) } ->
+                let term = self#visit_expr env term in
+                let ty1 = annotate_type ty1 in
+                let ty2 = annotate_type ty2 in
+                let e1 = self#visit_expr env e1 in
+                let e2 = self#visit_expr env e2 in
+                let new_case = Case {
+                    term; branch1 = ((bnd1, ty1), e1); branch2 = ((bnd2, ty2), e2) }
+                in
+                { expr_with_pos with node = new_case }
             | CaseL { term; ty = ty1; nil = nil_cont; cons = ((x_bnd, xs_bnd), cons_cont)} ->
                 let term = self#visit_expr env term in
                 let ty_ann = annotate_type ty1 in
diff --git a/lib/typecheck/ty_env.ml b/lib/typecheck/ty_env.ml
index 14b67bd..3fd2e3c 100644
--- a/lib/typecheck/ty_env.ml
+++ b/lib/typecheck/ty_env.ml
@@ -232,6 +232,18 @@ let intersect : t -> t -> Position.t -> t * Constraint_set.t =
                 | List t1, List t2 ->
                     let ty, constrs = intersect_types var t1 t2 in
                     List ty, constrs
+                | Sum (t1l, t1r), Sum (t2l, t2r) ->
+                    let tl, constrs1 = intersect_types var t1l t2l in
+                    let tr, constrs2 = intersect_types var t1r t2r in
+                    Sum (tl, tr), Constraint_set.union constrs1 constrs2
+                | Tuple ts1, Tuple ts2 ->
+                    let (ts, constrs) =
+                        List.fold_left2 (fun (acc, constrs) t1 t2 -> 
+                            let t, t_constrs = intersect_types var t1 t2 in
+                            t :: acc, Constraint_set.union t_constrs constrs)
+                        ([], Constraint_set.empty) ts1 ts2
+                    in
+                    Tuple ts, constrs
                 | _, _ ->
                     Gripers.type_mismatch false t1 t2 var [pos]
         in
diff --git a/test/examples/savina/lists/banking.pat b/test/examples/savina/lists/banking.pat
index bfbaff4..95baf84 100644
--- a/test/examples/savina/lists/banking.pat
+++ b/test/examples/savina/lists/banking.pat
@@ -47,30 +47,30 @@ def teller(self: TellerMb?, numAccounts : Int, numsAccounts: [Int]): Unit {
 }
 
 ## Randomly chooses the source account.
-def generate_work(tellerMb: TellerMb!, numAccounts: Int, accs : [AccountMb!]): Unit {
+def generate_work(tellerMb: TellerMb!, numAccounts: Int, accs : [AccountMb![R]]): Unit {
 
   # Randomly choose source account from which the funds shall be taken.
   let sourceId = rand(numAccounts - 1) in # -1 because rand() is 0-indexed.
 
-  let (choice, rest) = pick(accs, sourceId, (nil : [AccountMb!])) in
+  let (choice, rest) = pick(accs, sourceId, (nil : [AccountMb![R]])) in
   choose_dst_acc(tellerMb, numAccounts, choice, rest)
 }
 
-def pick(accs : [AccountMb!], index : Int, rest : [AccountMb!]) : ((Unit + AccountMb!) * [AccountMb!]) {
+def pick(accs : [AccountMb![R]], index : Int, rest : [AccountMb![R]]) : ((Unit + AccountMb![R]) * [AccountMb![R]]) {
 if (index == 0) {
-    caseL accs : [AccountMb!] of {
+    caseL accs : [AccountMb![R]] of {
         nil -> let x = () in (inl(x) : (Unit + AccountMb!), rest)
         | (a cons as) -> (inr(a) : (Unit + AccountMb!), append(rest, as))
     }}
 else {
-    caseL accs : [AccountMb!] of {
+    caseL accs : [AccountMb![R]] of {
         nil ->  let x = () in (inl(x) : (Unit + AccountMb!), rest)
         | (a cons as) -> pick(as, index - 1, (a cons rest))
     }}
 }
 
-def append(l1 : [AccountMb!], l2: [AccountMb!]) : [AccountMb!] {
-    caseL l1 : [AccountMb!] of {
+def append(l1 : [AccountMb![R]], l2: [AccountMb![R]]) : [AccountMb![R]] {
+    caseL l1 : [AccountMb![R]] of {
         nil -> l2
         | (a cons as) -> append(as, (a cons l2))
     }
@@ -78,7 +78,7 @@ def append(l1 : [AccountMb!], l2: [AccountMb!]) : [AccountMb!] {
 
 ## Randomly chooses the destination account and issues a credit request. The
 ## function ensures that the source and destination account are different.
-def choose_dst_acc(tellerMb: TellerMb!, numAccounts: Int, srcAccount: (Unit + AccountMb!), dstAccountMbs : [AccountMb!]): Unit {
+def choose_dst_acc(tellerMb: TellerMb!, numAccounts: Int, srcAccount: (Unit + AccountMb![R]), dstAccountMbs : [AccountMb![R]]): Unit {
 
   (# Randomly choose destination account to which funds shall be deposited. -2
     # because rand() is 0-indexed, and because we do not include the source
@@ -86,7 +86,7 @@ def choose_dst_acc(tellerMb: TellerMb!, numAccounts: Int, srcAccount: (Unit + Ac
     # send funds to itself).
     let dstAccountId = rand(numAccounts - 2) in
   
-    let (dstAccount, rest) = (pick(dstAccountMbs, dstAccountId, (nil : [AccountMb!])) : ((Unit + AccountMb!Credit) * [AccountMb!1]))
+    let (dstAccount, rest) = (pick(dstAccountMbs, dstAccountId, (nil : [AccountMb![R]])) : ((Unit + AccountMb!Credit[R]) * [AccountMb!1[R]]))
     in
   
     (let amount = rand(200) in

From 97722f4a8b52acbfeffa599a67f0aff2319b0035 Mon Sep 17 00:00:00 2001
From: Danielle Marshall <danielle@starsandspira.ls>
Date: Thu, 4 Dec 2025 14:32:54 +0000
Subject: [PATCH 25/33] add case for sum types to make_unrestricted

---
 lib/typecheck/type_utils.ml | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/lib/typecheck/type_utils.ml b/lib/typecheck/type_utils.ml
index e6e2fd6..ddffccf 100644
--- a/lib/typecheck/type_utils.ml
+++ b/lib/typecheck/type_utils.ml
@@ -26,6 +26,8 @@ let rec make_unrestricted t pos =
         | Tuple tys ->
             Constraint_set.union_many
                 (List.map (fun t -> make_unrestricted t pos) tys)
+        | Sum (ty1, ty2) ->
+            Constraint_set.union (make_unrestricted ty1 pos) (make_unrestricted ty2 pos)
         | List ty ->
             make_unrestricted ty pos
         | _ -> assert false

From f9bce315f59232d2e1399181815367845a6f2dff Mon Sep 17 00:00:00 2001
From: Danielle Marshall <danielle@starsandspira.ls>
Date: Thu, 4 Dec 2025 14:39:15 +0000
Subject: [PATCH 26/33] add cases for tuples and sums to join_types

---
 lib/typecheck/ty_env.ml | 12 ++++++++++++
 1 file changed, 12 insertions(+)

diff --git a/lib/typecheck/ty_env.ml b/lib/typecheck/ty_env.ml
index 3fd2e3c..2b715c4 100644
--- a/lib/typecheck/ty_env.ml
+++ b/lib/typecheck/ty_env.ml
@@ -100,6 +100,18 @@ let join : Interface_env.t -> t -> t -> Position.t -> t * Constraint_set.t =
                 | List ty1, List ty2 ->
                     let ty, constrs = join_types var ty1 ty2 in
                     List ty, constrs
+                | Sum (t1l, t1r), Sum (t2l, t2r) ->
+                    let tl, constrs1 = join_types var t1l t2l in
+                    let tr, constrs2 = join_types var t1r t2r in
+                    Sum (tl, tr), Constraint_set.union constrs1 constrs2
+                | Tuple ts1, Tuple ts2 ->
+                    let (ts, constrs) =
+                        List.fold_left2 (fun (acc, constrs) t1 t2 ->
+                            let t, t_constrs = join_types var t1 t2 in
+                            t :: acc, Constraint_set.union t_constrs constrs)
+                        ([], Constraint_set.empty) ts1 ts2
+                    in
+                    Tuple ts, constrs
                 | _, _ ->
                     Gripers.type_mismatch true t1 t2 var [pos]
         in

From a343dee2a889c73b0e67fe51f7bb4bf8e944d876 Mon Sep 17 00:00:00 2001
From: Danielle Marshall <danielle@starsandspira.ls>
Date: Thu, 4 Dec 2025 14:43:54 +0000
Subject: [PATCH 27/33] remove is_returnable and make_returnable cases for
 tuples/sums/lists and add explanatory comment

---
 lib/common/type.ml | 12 ++++--------
 1 file changed, 4 insertions(+), 8 deletions(-)

diff --git a/lib/common/type.ml b/lib/common/type.ml
index e5a16c6..dd10f8b 100644
--- a/lib/common/type.ml
+++ b/lib/common/type.ml
@@ -415,21 +415,17 @@ let rec make_usable = function
     | List t -> List (make_usable t)
     | t -> t
 
-let rec make_returnable = function
+(* Tuples, sums, and lists can all be returnable even if they contain things that are not returnable,
+   as long as we are careful to avoid aliasing when deconstructing the value. *)
+let make_returnable = function
     | Mailbox m -> Mailbox { m with quasilinearity = Quasilinearity.Returnable }
-    | Tuple ts -> Tuple (List.map make_returnable ts)
-    | Sum (t1, t2) -> Sum (make_returnable t1, make_returnable t2)
-    (* | List t -> List (make_returnable t) *)
     | t -> t
 
 let is_unr = is_lin >> not
 
-let rec is_returnable = function
+let is_returnable = function
     | Mailbox { quasilinearity = ql; _ } ->
         ql = Quasilinearity.Returnable
-    | Tuple ts -> List.for_all is_returnable ts
-    | Sum  (t1, t2) -> is_returnable t1 && is_returnable t2
-    | List t -> is_returnable t
     | _ -> true
 
 let make_function_type linear args result =

From 2c2469f96797562fabb3ac3986508b1267e6b25a Mon Sep 17 00:00:00 2001
From: Danielle Marshall <danielle@starsandspira.ls>
Date: Thu, 4 Dec 2025 15:46:25 +0000
Subject: [PATCH 28/33] infix double colon syntax for list cons

---
 lib/frontend/lexer.mll                  |  4 ++--
 test/examples/savina/lists/banking.pat  | 14 +++++++-------
 test/examples/savina/lists/barber.pat   | 10 +++++-----
 test/examples/savina/lists/big.pat      |  4 ++--
 test/examples/savina/lists/cig_smok.pat | 14 +++++++-------
 test/examples/savina/lists/kfork.pat    |  4 ++--
 test/examples/savina/lists/robotsn.pat  |  4 ++--
 test/pat-tests/list-1.pat               |  4 ++--
 test/pat-tests/list-2.pat               | 10 +++++-----
 9 files changed, 34 insertions(+), 34 deletions(-)

diff --git a/lib/frontend/lexer.mll b/lib/frontend/lexer.mll
index 3e55ff6..743bab1 100644
--- a/lib/frontend/lexer.mll
+++ b/lib/frontend/lexer.mll
@@ -49,8 +49,7 @@ let keywords = [
     "of", OF;
     "inl", INL;
     "inr", INR;
-    "nil", NIL;
-    "cons", CONS
+    "nil", NIL
 ]
 }
 
@@ -111,6 +110,7 @@ rule read =
     | "!="     { add_to_source_code lexbuf; NEQ }
     | "->"     { add_to_source_code lexbuf; RIGHTARROW }
     | "-o"     { add_to_source_code lexbuf; LOLLI }
+    | "::"     { add_to_source_code lexbuf; CONS }
     | _ { raise (SyntaxError ("Unexpected char: " ^ Lexing.lexeme lexbuf)) }
     | eof      { EOF }
 and read_string buf =
diff --git a/test/examples/savina/lists/banking.pat b/test/examples/savina/lists/banking.pat
index 95baf84..b8bf8e5 100644
--- a/test/examples/savina/lists/banking.pat
+++ b/test/examples/savina/lists/banking.pat
@@ -20,10 +20,10 @@ interface AccountMb {
 def spawnAccounts(self: TellerMb?, numsAccounts: [Int], soFar: Int, acc: [AccountMb!]) : (TellerMb? * [AccountMb!]) {
   caseL numsAccounts : [Int] of {
     nil -> (self, acc)
-    | (n cons ns) ->
+    | (n :: ns) ->
         let accountMb = new [AccountMb] in
         spawn { account(accountMb, soFar, n)};
-        spawnAccounts(self, ns, soFar + 1, (accountMb cons acc))
+        spawnAccounts(self, ns, soFar + 1, (accountMb :: acc))
     }
   }
 
@@ -60,19 +60,19 @@ def pick(accs : [AccountMb![R]], index : Int, rest : [AccountMb![R]]) : ((Unit +
 if (index == 0) {
     caseL accs : [AccountMb![R]] of {
         nil -> let x = () in (inl(x) : (Unit + AccountMb!), rest)
-        | (a cons as) -> (inr(a) : (Unit + AccountMb!), append(rest, as))
+        | (a :: as) -> (inr(a) : (Unit + AccountMb!), append(rest, as))
     }}
 else {
     caseL accs : [AccountMb![R]] of {
         nil ->  let x = () in (inl(x) : (Unit + AccountMb!), rest)
-        | (a cons as) -> pick(as, index - 1, (a cons rest))
+        | (a :: as) -> pick(as, index - 1, (a :: rest))
     }}
 }
 
 def append(l1 : [AccountMb![R]], l2: [AccountMb![R]]) : [AccountMb![R]] {
     caseL l1 : [AccountMb![R]] of {
         nil -> l2
-        | (a cons as) -> append(as, (a cons l2))
+        | (a :: as) -> append(as, (a :: l2))
     }
 }
 
@@ -116,7 +116,7 @@ def teller_loop(self: TellerMb?, accountMbs : [AccountMb!]): Unit {
 def stopAccounts(accs: [AccountMb!]) : Unit {
     caseL accs : [AccountMb!] of {
         nil -> ()
-        | (a cons as) ->
+        | (a :: as) ->
             a ! Stop();
             stopAccounts(as)
         }
@@ -167,7 +167,7 @@ def account_exit(self: AccountMb?): Unit {
 ## Launcher.
 def main(): Unit {
   let tellerMb = new [TellerMb] in
-  spawn { teller(tellerMb, 3, (200 cons (150 cons (50 cons (nil : [Int]))))) };
+  spawn { teller(tellerMb, 3, (200 :: (150 :: (50 :: (nil : [Int]))))) };
 
   tellerMb ! Start()
 }
diff --git a/test/examples/savina/lists/barber.pat b/test/examples/savina/lists/barber.pat
index 533b038..89f6c41 100644
--- a/test/examples/savina/lists/barber.pat
+++ b/test/examples/savina/lists/barber.pat
@@ -40,14 +40,14 @@ def room(self: RoomMb?, capacity: Int, waiters: [CustomerMb!], waiting: Int, bar
             }
             else {
                 sleep(5);
-                room(self, capacity, (customerMb cons waiters), (waiting + 1), barber)
+                room(self, capacity, (customerMb :: waiters), (waiting + 1), barber)
             }
         receive Next() from self ->
             caseL waiters : [CustomerMb!] of {
                 nil ->
                     sleep(5);
                     room(self, capacity, (nil : [CustomerMb!]), waiting, barber)
-                | (a cons as) -> 
+                | (a :: as) -> 
                     barber ! Enter(a, self);
                     room(self, capacity, as, (waiting - 1), barber)
             }
@@ -94,14 +94,14 @@ def spawnCustomers(self: SelectorMb?, generator: Int, soFar: Int, acc : [Custome
     else {
         let customerMb = new [CustomerMb] in
         spawn { customer(customerMb, self)};
-        spawnCustomers(self, generator, (soFar + 1), (customerMb cons acc))
+        spawnCustomers(self, generator, (soFar + 1), (customerMb :: acc))
     }
 }
 
 def startCustomers(customerMbs : [CustomerMb!], room : RoomMb!) : Unit {
     caseL customerMbs : [CustomerMb!] of {
         nil -> ()
-        | (a cons as) ->
+        | (a :: as) ->
             a ! Start(room);
             startCustomers(as, room)
     } 
@@ -110,7 +110,7 @@ def startCustomers(customerMbs : [CustomerMb!], room : RoomMb!) : Unit {
 def doneCustomers(customerMbs : [CustomerMb!]) : Unit {
     caseL customerMbs : [CustomerMb!] of {
         nil -> ()
-        | (a cons as) ->
+        | (a :: as) ->
             a ! Done();
             doneCustomers(as)
     } 
diff --git a/test/examples/savina/lists/big.pat b/test/examples/savina/lists/big.pat
index 3d521ab..373d323 100644
--- a/test/examples/savina/lists/big.pat
+++ b/test/examples/savina/lists/big.pat
@@ -126,7 +126,7 @@ def sink_loop(self: SinkMb?, exitMbs : [ExitMb!]): Unit {
 def notifyExits(exitMbs : [ExitMb!]): Unit {
     caseL exitMbs : [ExitMb!] of {
     nil -> ()
-  | (y cons ys) ->
+  | (y :: ys) ->
         y ! Exit();
         notifyExits(ys)
     }
@@ -150,7 +150,7 @@ def main(): Unit {
   spawn { actor(actorMb2, exitMb2, 2, sinkMb) };
   spawn { actor(actorMb3, exitMb3, 3, sinkMb) };
 
-  let xs = (exitMb1 cons (exitMb2 cons (exitMb3 cons (nil : [ExitMb!])))) in sinkMb ! Actors(xs);
+  let xs = (exitMb1 :: (exitMb2 :: (exitMb3 :: (nil : [ExitMb!])))) in sinkMb ! Actors(xs);
 
   actorMb1 ! Neighbors(actorMb2, actorMb3); # actorMb1: ?Neighbors
   actorMb2 ! Neighbors(actorMb1, actorMb3); # actorMb2: ?Neighbors
diff --git a/test/examples/savina/lists/cig_smok.pat b/test/examples/savina/lists/cig_smok.pat
index ea51dda..5c3eb9c 100644
--- a/test/examples/savina/lists/cig_smok.pat
+++ b/test/examples/savina/lists/cig_smok.pat
@@ -21,7 +21,7 @@ def create_smokers(self: ArbiterMb?, moreSmokers: Int, acc: [SmokerMb!]): (Arbit
     else {
         let newSmoker = new [SmokerMb] in
             spawn { smoker(newSmoker, self) };
-            create_smokers(self, moreSmokers - 1, (newSmoker cons acc))
+            create_smokers(self, moreSmokers - 1, (newSmoker :: acc))
         }
 }
 
@@ -51,17 +51,17 @@ def notify_aux(choice: Int, time: Int, smokerMbs: [SmokerMb!]): [SmokerMb!] {
 if (choice == 0) {
     caseL smokerMbs : [SmokerMb!]  of {
         nil -> nil
-        | (mb cons mbs) ->
+        | (mb :: mbs) ->
             mb ! StartSmoking(rand(time));
-            (mb cons mbs)
+            (mb :: mbs)
     }
 }
 else {
     caseL smokerMbs : [SmokerMb!] of {
         nil -> nil
-        | (mb cons mbs) ->
+        | (mb :: mbs) ->
             let smokerMbs = notify_aux(choice - 1, time, mbs) in
-            (mb cons smokerMbs)
+            (mb :: smokerMbs)
     }
 }
 }
@@ -70,7 +70,7 @@ else {
 def notify_smoker_exit(smokerMbs: [SmokerMb!]): [SmokerMb!] {
     caseL smokerMbs : [SmokerMb!] of {
         nil -> nil
-        | (mb cons mbs) ->
+        | (mb :: mbs) ->
             mb ! Exit();
             notify_smoker_exit(mbs)
         }
@@ -83,7 +83,7 @@ def arbiter_loop(self: ArbiterMb?, numSmokers: Int, numRounds: Int, smokerMbs: [
     free ->
       caseL smokerMbs : [SmokerMb!] of {
       nil -> ()
-      | (a cons as) -> ()
+      | (a :: as) -> ()
   }
     receive StartedSmoking() from self ->
 
diff --git a/test/examples/savina/lists/kfork.pat b/test/examples/savina/lists/kfork.pat
index ca269b8..9846e84 100644
--- a/test/examples/savina/lists/kfork.pat
+++ b/test/examples/savina/lists/kfork.pat
@@ -46,14 +46,14 @@ def spawnActors(numActors: Int, acc: [ActorMb!]): [ActorMb!] {
     } else {
         let newActor = new[ActorMb] in
         spawn { actor(newActor) };
-        spawnActors(numActors - 1, (newActor cons acc))
+        spawnActors(numActors - 1, (newActor :: acc))
     }
 }
 
 def floodActors(numMessages: Int, actorMbs: [ActorMb!]): Unit {
     caseL actorMbs : [ActorMb!] of {
         nil -> ()
-      | (a cons as) ->
+      | (a :: as) ->
             flood(numMessages, a);
             floodActors(numMessages, as)
         }
diff --git a/test/examples/savina/lists/robotsn.pat b/test/examples/savina/lists/robotsn.pat
index 5eea045..dea2417 100644
--- a/test/examples/savina/lists/robotsn.pat
+++ b/test/examples/savina/lists/robotsn.pat
@@ -120,7 +120,7 @@ def handlePartTaken(self: Warehouse?, door: Door!): Unit {
 def discardList(xs: [Robot!]) : Unit {
     caseL xs : [Robot!] of {
         nil -> ()
-        | (a cons as) -> discardList(as)
+        | (a :: as) -> discardList(as)
     }
 }
 
@@ -130,7 +130,7 @@ def spawnRobots(numRobots: Int, door: Door!, acc: [Robot!]): Unit {
     } else {
         let newRobot = new[Robot] in
         spawn { idleRobot(newRobot, door) };
-        spawnRobots(numRobots - 1, door, (newRobot cons acc))
+        spawnRobots(numRobots - 1, door, (newRobot :: acc))
     }
 }
 
diff --git a/test/pat-tests/list-1.pat b/test/pat-tests/list-1.pat
index ebabfc4..2df1fae 100644
--- a/test/pat-tests/list-1.pat
+++ b/test/pat-tests/list-1.pat
@@ -1,8 +1,8 @@
 def main() : Unit {
-    let xs = (5 cons (nil : [Int])) in
+    let xs = (5 :: (nil : [Int])) in
     caseL xs : [Int] of {
           nil -> print("nil")
-        | (y cons ys) -> print(intToString(y))
+        | (y :: ys) -> print(intToString(y))
     }
 }
 
diff --git a/test/pat-tests/list-2.pat b/test/pat-tests/list-2.pat
index a3e27d2..167c961 100644
--- a/test/pat-tests/list-2.pat
+++ b/test/pat-tests/list-2.pat
@@ -1,22 +1,22 @@
 def snoc(xs : [Int], x : Int): [Int] {
     caseL xs : [Int] of {
-        nil -> (x cons (nil : [Int]))
-      | (y cons ys) -> (y cons snoc(ys, x))
+        nil -> (x :: (nil : [Int]))
+      | (y :: ys) -> (y :: snoc(ys, x))
     }
 }
 
 def reverse(xs : [Int]): [Int] {
     caseL xs : [Int] of {
           nil -> nil
-        | (y cons ys) -> snoc(reverse(ys), y)
+        | (y :: ys) -> snoc(reverse(ys), y)
     }
 }
 
 def main(): Unit {
-    let xs = (1 cons (2 cons (3 cons (nil : [Int])))) in
+    let xs = (1 :: (2 :: (3 :: (nil : [Int])))) in
     caseL reverse(xs) : [Int] of {
         nil -> print("nil")
-      | (y cons ys) -> print(intToString(y))
+      | (y :: ys) -> print(intToString(y))
   }
 }
 

From b1fd43c693f5bc86d2185fc55949fd5c3bc8fed8 Mon Sep 17 00:00:00 2001
From: Danielle Marshall <danielle@starsandspira.ls>
Date: Thu, 4 Dec 2025 16:08:21 +0000
Subject: [PATCH 29/33] less haskellish syntax for list type

---
 lib/frontend/lexer.mll                  |  3 ++-
 lib/frontend/parser.mly                 |  4 +--
 test/examples/savina/lists/banking.pat  | 34 ++++++++++++-------------
 test/examples/savina/lists/barber.pat   | 24 ++++++++---------
 test/examples/savina/lists/big.pat      | 10 ++++----
 test/examples/savina/lists/cig_smok.pat | 20 +++++++--------
 test/examples/savina/lists/kfork.pat    |  8 +++---
 test/examples/savina/lists/robotsn.pat  |  8 +++---
 test/pat-tests/list-1.pat               |  4 +--
 test/pat-tests/list-2.pat               | 14 +++++-----
 10 files changed, 65 insertions(+), 64 deletions(-)

diff --git a/lib/frontend/lexer.mll b/lib/frontend/lexer.mll
index 743bab1..d06edff 100644
--- a/lib/frontend/lexer.mll
+++ b/lib/frontend/lexer.mll
@@ -49,7 +49,8 @@ let keywords = [
     "of", OF;
     "inl", INL;
     "inr", INR;
-    "nil", NIL
+    "nil", NIL;
+    "List", LIST
 ]
 }
 
diff --git a/lib/frontend/parser.mly b/lib/frontend/parser.mly
index fe9d14d..5f41aee 100644
--- a/lib/frontend/parser.mly
+++ b/lib/frontend/parser.mly
@@ -94,6 +94,7 @@ These will be added in later
 %token OR
 %token CASE
 %token CASEL
+%token LIST
 %token NIL
 %token CONS
 %token OF
@@ -174,7 +175,6 @@ basic_expr:
     | tuple_exprs { with_pos_from_positions $startpos $endpos ( Tuple $1 ) }
     | NIL { with_pos_from_positions $startpos $endpos ( Nil ) }
     | LEFT_PAREN expr CONS expr RIGHT_PAREN { with_pos_from_positions $startpos $endpos ( Cons ($2, $4) ) }
-    (* | LEFT_BRACK expr RIGHT_BRACK { Cons ($2, Nil) } *)
     (* App *)
     | fact LEFT_PAREN expr_list RIGHT_PAREN
         { with_pos_from_positions $startpos $endpos (
@@ -269,7 +269,7 @@ ty:
     | parenthesised_datatypes LOLLI simple_ty       { Type.Fun { linear = true;  args = $1; result = $3} }
     | LEFT_PAREN simple_ty PLUS simple_ty RIGHT_PAREN { Type.make_sum_type $2 $4 }
     | tuple_annotation { Type.make_tuple_type $1 }
-    | LEFT_BRACK simple_ty RIGHT_BRACK { Type.make_list_type $2 }
+    | LIST LEFT_PAREN simple_ty RIGHT_PAREN { Type.make_list_type $3 }
     | simple_ty { $1 }
 
 interface_name:
diff --git a/test/examples/savina/lists/banking.pat b/test/examples/savina/lists/banking.pat
index b8bf8e5..c4e3bd4 100644
--- a/test/examples/savina/lists/banking.pat
+++ b/test/examples/savina/lists/banking.pat
@@ -17,8 +17,8 @@ interface AccountMb {
   Stop()
 }
 
-def spawnAccounts(self: TellerMb?, numsAccounts: [Int], soFar: Int, acc: [AccountMb!]) : (TellerMb? * [AccountMb!]) {
-  caseL numsAccounts : [Int] of {
+def spawnAccounts(self: TellerMb?, numsAccounts: List(Int), soFar: Int, acc: List(AccountMb!)) : (TellerMb? * List(AccountMb!)) {
+  caseL numsAccounts : List(Int) of {
     nil -> (self, acc)
     | (n :: ns) ->
         let accountMb = new [AccountMb] in
@@ -29,9 +29,9 @@ def spawnAccounts(self: TellerMb?, numsAccounts: [Int], soFar: Int, acc: [Accoun
 
 ## Teller process handling the creation of account processes and launching of
 ## main loop.
-def teller(self: TellerMb?, numAccounts : Int, numsAccounts: [Int]): Unit {
+def teller(self: TellerMb?, numAccounts : Int, numsAccounts: List(Int)): Unit {
 
-  let (self, accountMbs) = spawnAccounts(self, numsAccounts, 1, (nil : [AccountMb!])) in
+  let (self, accountMbs) = spawnAccounts(self, numsAccounts, 1, (nil : List(AccountMb!))) in
 
   guard self: Start {
     receive Start() from self ->
@@ -47,30 +47,30 @@ def teller(self: TellerMb?, numAccounts : Int, numsAccounts: [Int]): Unit {
 }
 
 ## Randomly chooses the source account.
-def generate_work(tellerMb: TellerMb!, numAccounts: Int, accs : [AccountMb![R]]): Unit {
+def generate_work(tellerMb: TellerMb!, numAccounts: Int, accs : List(AccountMb![R])): Unit {
 
   # Randomly choose source account from which the funds shall be taken.
   let sourceId = rand(numAccounts - 1) in # -1 because rand() is 0-indexed.
 
-  let (choice, rest) = pick(accs, sourceId, (nil : [AccountMb![R]])) in
+  let (choice, rest) = pick(accs, sourceId, (nil : List(AccountMb![R]))) in
   choose_dst_acc(tellerMb, numAccounts, choice, rest)
 }
 
-def pick(accs : [AccountMb![R]], index : Int, rest : [AccountMb![R]]) : ((Unit + AccountMb![R]) * [AccountMb![R]]) {
+def pick(accs : List(AccountMb![R]), index : Int, rest : List(AccountMb![R])) : ((Unit + AccountMb![R]) * List(AccountMb![R])) {
 if (index == 0) {
-    caseL accs : [AccountMb![R]] of {
+    caseL accs : List(AccountMb![R]) of {
         nil -> let x = () in (inl(x) : (Unit + AccountMb!), rest)
         | (a :: as) -> (inr(a) : (Unit + AccountMb!), append(rest, as))
     }}
 else {
-    caseL accs : [AccountMb![R]] of {
+    caseL accs : List(AccountMb![R]) of {
         nil ->  let x = () in (inl(x) : (Unit + AccountMb!), rest)
         | (a :: as) -> pick(as, index - 1, (a :: rest))
     }}
 }
 
-def append(l1 : [AccountMb![R]], l2: [AccountMb![R]]) : [AccountMb![R]] {
-    caseL l1 : [AccountMb![R]] of {
+def append(l1 : List(AccountMb![R]), l2: List(AccountMb![R])) : List(AccountMb![R]) {
+    caseL l1 : List(AccountMb![R]) of {
         nil -> l2
         | (a :: as) -> append(as, (a :: l2))
     }
@@ -78,7 +78,7 @@ def append(l1 : [AccountMb![R]], l2: [AccountMb![R]]) : [AccountMb![R]] {
 
 ## Randomly chooses the destination account and issues a credit request. The
 ## function ensures that the source and destination account are different.
-def choose_dst_acc(tellerMb: TellerMb!, numAccounts: Int, srcAccount: (Unit + AccountMb![R]), dstAccountMbs : [AccountMb![R]]): Unit {
+def choose_dst_acc(tellerMb: TellerMb!, numAccounts: Int, srcAccount: (Unit + AccountMb![R]), dstAccountMbs : List(AccountMb![R])) : Unit {
 
   (# Randomly choose destination account to which funds shall be deposited. -2
     # because rand() is 0-indexed, and because we do not include the source
@@ -86,7 +86,7 @@ def choose_dst_acc(tellerMb: TellerMb!, numAccounts: Int, srcAccount: (Unit + Ac
     # send funds to itself).
     let dstAccountId = rand(numAccounts - 2) in
   
-    let (dstAccount, rest) = (pick(dstAccountMbs, dstAccountId, (nil : [AccountMb![R]])) : ((Unit + AccountMb!Credit[R]) * [AccountMb!1[R]]))
+    let (dstAccount, rest) = (pick(dstAccountMbs, dstAccountId, (nil : List(AccountMb![R]))) : ((Unit + AccountMb!Credit[R]) * List(AccountMb!1[R])))
     in
   
     (let amount = rand(200) in
@@ -103,7 +103,7 @@ def choose_dst_acc(tellerMb: TellerMb!, numAccounts: Int, srcAccount: (Unit + Ac
 }
 
 ## Teller process main loop handling replies from accounts.
-def teller_loop(self: TellerMb?, accountMbs : [AccountMb!]): Unit {
+def teller_loop(self: TellerMb?, accountMbs : List(AccountMb!)): Unit {
   guard self: Reply* {
     free ->
       # All credit requests serviced. Stop accounts.
@@ -113,8 +113,8 @@ def teller_loop(self: TellerMb?, accountMbs : [AccountMb!]): Unit {
   }
 }
 
-def stopAccounts(accs: [AccountMb!]) : Unit {
-    caseL accs : [AccountMb!] of {
+def stopAccounts(accs: List(AccountMb!)) : Unit {
+    caseL accs : List(AccountMb!) of {
         nil -> ()
         | (a :: as) ->
             a ! Stop();
@@ -167,7 +167,7 @@ def account_exit(self: AccountMb?): Unit {
 ## Launcher.
 def main(): Unit {
   let tellerMb = new [TellerMb] in
-  spawn { teller(tellerMb, 3, (200 :: (150 :: (50 :: (nil : [Int]))))) };
+  spawn { teller(tellerMb, 3, (200 :: (150 :: (50 :: (nil : List(Int)))))) };
 
   tellerMb ! Start()
 }
diff --git a/test/examples/savina/lists/barber.pat b/test/examples/savina/lists/barber.pat
index 89f6c41..1615169 100644
--- a/test/examples/savina/lists/barber.pat
+++ b/test/examples/savina/lists/barber.pat
@@ -30,7 +30,7 @@ interface CustomerMb {
     Exit()
 }
 
-def room(self: RoomMb?, capacity: Int, waiters: [CustomerMb!], waiting: Int, barber: BarberMb!): Unit {
+def room(self: RoomMb?, capacity: Int, waiters: List(CustomerMb!), waiting: Int, barber: BarberMb!): Unit {
     guard self: (Enter + Next + Exit)* {
         free -> ()
         receive Enter(customerMb) from self ->
@@ -43,10 +43,10 @@ def room(self: RoomMb?, capacity: Int, waiters: [CustomerMb!], waiting: Int, bar
                 room(self, capacity, (customerMb :: waiters), (waiting + 1), barber)
             }
         receive Next() from self ->
-            caseL waiters : [CustomerMb!] of {
+            caseL waiters : List(CustomerMb!) of {
                 nil ->
                     sleep(5);
-                    room(self, capacity, (nil : [CustomerMb!]), waiting, barber)
+                    room(self, capacity, (nil : List(CustomerMb!)), waiting, barber)
                 | (a :: as) -> 
                     barber ! Enter(a, self);
                     room(self, capacity, as, (waiting - 1), barber)
@@ -87,7 +87,7 @@ def barberExit(self : BarberMb?) : Unit {
     }
 }
 
-def spawnCustomers(self: SelectorMb?, generator: Int, soFar: Int, acc : [CustomerMb!]): (SelectorMb? * [CustomerMb!]) {
+def spawnCustomers(self: SelectorMb?, generator: Int, soFar: Int, acc : List(CustomerMb!)): (SelectorMb? * List(CustomerMb!)) {
     if (soFar == generator) {
             (self, acc)
         }
@@ -98,8 +98,8 @@ def spawnCustomers(self: SelectorMb?, generator: Int, soFar: Int, acc : [Custome
     }
 }
 
-def startCustomers(customerMbs : [CustomerMb!], room : RoomMb!) : Unit {
-    caseL customerMbs : [CustomerMb!] of {
+def startCustomers(customerMbs : List(CustomerMb!), room : RoomMb!) : Unit {
+    caseL customerMbs : List(CustomerMb!) of {
         nil -> ()
         | (a :: as) ->
             a ! Start(room);
@@ -107,8 +107,8 @@ def startCustomers(customerMbs : [CustomerMb!], room : RoomMb!) : Unit {
     } 
 }
 
-def doneCustomers(customerMbs : [CustomerMb!]) : Unit {
-    caseL customerMbs : [CustomerMb!] of {
+def doneCustomers(customerMbs : List(CustomerMb!)) : Unit {
+    caseL customerMbs : List(CustomerMb!) of {
         nil -> ()
         | (a :: as) ->
             a ! Done();
@@ -116,11 +116,11 @@ def doneCustomers(customerMbs : [CustomerMb!]) : Unit {
     } 
 }
 
-def selector(self: SelectorMb?, generator: Int, haircuts: Int, target: Int, customers : [CustomerMb!], room: RoomMb!): Unit {
+def selector(self: SelectorMb?, generator: Int, haircuts: Int, target: Int, customers : List(CustomerMb!), room: RoomMb!): Unit {
     guard self: (Start + Returned)* {
         free -> ()
         receive Start() from self ->
-            let (self, newCustomers) = spawnCustomers(self, generator, 0, (nil : [CustomerMb!])) in
+            let (self, newCustomers) = spawnCustomers(self, generator, 0, (nil : List(CustomerMb!))) in
             startCustomers(customers, room);
             selector(self, generator, haircuts, target, newCustomers, room)
         receive Returned(customerMb) from self ->
@@ -178,10 +178,10 @@ def main() : Unit {
     spawn {barber(barberMb)};
 
     let roomMb = new [RoomMb] in
-    spawn {room(roomMb, 2, (nil : [CustomerMb!]), 0, barberMb)};
+    spawn {room(roomMb, 2, (nil : List(CustomerMb!)), 0, barberMb)};
 
     let selectorMb = new [SelectorMb] in
-    spawn {selector(selectorMb, 4, 0, 6, (nil : [CustomerMb!]), roomMb)};
+    spawn {selector(selectorMb, 4, 0, 6, (nil : List(CustomerMb!)), roomMb)};
 
     selectorMb ! Start()
 }
diff --git a/test/examples/savina/lists/big.pat b/test/examples/savina/lists/big.pat
index 373d323..c26ae95 100644
--- a/test/examples/savina/lists/big.pat
+++ b/test/examples/savina/lists/big.pat
@@ -17,7 +17,7 @@ interface ExitMb {
 
 interface SinkMb {
   Done(),
-  Actors([ExitMb!])
+  Actors(List(ExitMb!))
 }
 
 ## Actor process handling the launching of main loop.
@@ -112,7 +112,7 @@ def sink(self: SinkMb?): Unit {
 }
 
 ## Sink process main loop issuing termination messages.
-def sink_loop(self: SinkMb?, exitMbs : [ExitMb!]): Unit {
+def sink_loop(self: SinkMb?, exitMbs : List(ExitMb!)): Unit {
   guard self: Done* {
     free ->
       # Notify all actors. Placing the sends in this clause ensures that
@@ -123,8 +123,8 @@ def sink_loop(self: SinkMb?, exitMbs : [ExitMb!]): Unit {
   }
 }
 
-def notifyExits(exitMbs : [ExitMb!]): Unit {
-    caseL exitMbs : [ExitMb!] of {
+def notifyExits(exitMbs : List(ExitMb!)): Unit {
+    caseL exitMbs : List(ExitMb!) of {
     nil -> ()
   | (y :: ys) ->
         y ! Exit();
@@ -150,7 +150,7 @@ def main(): Unit {
   spawn { actor(actorMb2, exitMb2, 2, sinkMb) };
   spawn { actor(actorMb3, exitMb3, 3, sinkMb) };
 
-  let xs = (exitMb1 :: (exitMb2 :: (exitMb3 :: (nil : [ExitMb!])))) in sinkMb ! Actors(xs);
+  let xs = (exitMb1 :: (exitMb2 :: (exitMb3 :: (nil : List(ExitMb!))))) in sinkMb ! Actors(xs);
 
   actorMb1 ! Neighbors(actorMb2, actorMb3); # actorMb1: ?Neighbors
   actorMb2 ! Neighbors(actorMb1, actorMb3); # actorMb2: ?Neighbors
diff --git a/test/examples/savina/lists/cig_smok.pat b/test/examples/savina/lists/cig_smok.pat
index 5c3eb9c..83c8cd3 100644
--- a/test/examples/savina/lists/cig_smok.pat
+++ b/test/examples/savina/lists/cig_smok.pat
@@ -14,7 +14,7 @@ interface SmokerMb {
   Exit()
 }
 
-def create_smokers(self: ArbiterMb?, moreSmokers: Int, acc: [SmokerMb!]): (ArbiterMb? * [SmokerMb!]) {
+def create_smokers(self: ArbiterMb?, moreSmokers: Int, acc: List(SmokerMb!)): (ArbiterMb? * List(SmokerMb!)) {
     if (moreSmokers == 0) {
         (self, acc)
     }
@@ -31,7 +31,7 @@ def arbiter(self: ArbiterMb?, numRounds: Int): Unit {
   guard self: Start . (StartedSmoking*) {
     receive Start(numSmokers) from self ->
 
-       let (self, smokerMbs) = create_smokers(self, numSmokers, (nil : [SmokerMb!])) in
+       let (self, smokerMbs) = create_smokers(self, numSmokers, (nil : List(SmokerMb!))) in
 
         let smokerMbs = notify_smoker(numSmokers, smokerMbs) in
         arbiter_loop(self, numSmokers, numRounds, smokerMbs)
@@ -39,7 +39,7 @@ def arbiter(self: ArbiterMb?, numRounds: Int): Unit {
 }
 
 ## Randomly chooses the smoker and requests it to smoke.
-def notify_smoker(numSmokers: Int, smokerMbs: [SmokerMb!]): [SmokerMb!] {
+def notify_smoker(numSmokers: Int, smokerMbs: List(SmokerMb!)): List(SmokerMb!) {
 
   let smokerId = rand(numSmokers - 1) in
   let sleepTimeMs = 1000 in
@@ -47,9 +47,9 @@ def notify_smoker(numSmokers: Int, smokerMbs: [SmokerMb!]): [SmokerMb!] {
   notify_aux(smokerId, sleepTimeMs, smokerMbs)
 }
 
-def notify_aux(choice: Int, time: Int, smokerMbs: [SmokerMb!]): [SmokerMb!] {
+def notify_aux(choice: Int, time: Int, smokerMbs: List(SmokerMb!)): List(SmokerMb!) {
 if (choice == 0) {
-    caseL smokerMbs : [SmokerMb!]  of {
+    caseL smokerMbs : List(SmokerMb!)  of {
         nil -> nil
         | (mb :: mbs) ->
             mb ! StartSmoking(rand(time));
@@ -57,7 +57,7 @@ if (choice == 0) {
     }
 }
 else {
-    caseL smokerMbs : [SmokerMb!] of {
+    caseL smokerMbs : List(SmokerMb!) of {
         nil -> nil
         | (mb :: mbs) ->
             let smokerMbs = notify_aux(choice - 1, time, mbs) in
@@ -67,8 +67,8 @@ else {
 }
 
 ## Notifies all smokers to terminate.
-def notify_smoker_exit(smokerMbs: [SmokerMb!]): [SmokerMb!] {
-    caseL smokerMbs : [SmokerMb!] of {
+def notify_smoker_exit(smokerMbs: List(SmokerMb!)): List(SmokerMb!) {
+    caseL smokerMbs : List(SmokerMb!) of {
         nil -> nil
         | (mb :: mbs) ->
             mb ! Exit();
@@ -78,10 +78,10 @@ def notify_smoker_exit(smokerMbs: [SmokerMb!]): [SmokerMb!] {
 
 ## Arbiter process main loop issuing start smoking requests and handling started
 ## smoking replies.
-def arbiter_loop(self: ArbiterMb?, numSmokers: Int, numRounds: Int, smokerMbs: [SmokerMb!]): Unit {
+def arbiter_loop(self: ArbiterMb?, numSmokers: Int, numRounds: Int, smokerMbs: List(SmokerMb!)): Unit {
   guard self: StartedSmoking* {
     free ->
-      caseL smokerMbs : [SmokerMb!] of {
+      caseL smokerMbs : List(SmokerMb!) of {
       nil -> ()
       | (a :: as) -> ()
   }
diff --git a/test/examples/savina/lists/kfork.pat b/test/examples/savina/lists/kfork.pat
index 9846e84..944e23e 100644
--- a/test/examples/savina/lists/kfork.pat
+++ b/test/examples/savina/lists/kfork.pat
@@ -40,7 +40,7 @@ def flood(numMessages: Int, actorMb: ActorMb!): Unit {
   }
 }
 
-def spawnActors(numActors: Int, acc: [ActorMb!]): [ActorMb!] {
+def spawnActors(numActors: Int, acc: List(ActorMb!)): List(ActorMb!) {
     if (numActors <= 0) {
         acc
     } else {
@@ -50,8 +50,8 @@ def spawnActors(numActors: Int, acc: [ActorMb!]): [ActorMb!] {
     }
 }
 
-def floodActors(numMessages: Int, actorMbs: [ActorMb!]): Unit {
-    caseL actorMbs : [ActorMb!] of {
+def floodActors(numMessages: Int, actorMbs: List(ActorMb!)): Unit {
+    caseL actorMbs : List(ActorMb!) of {
         nil -> ()
       | (a :: as) ->
             flood(numMessages, a);
@@ -62,7 +62,7 @@ def floodActors(numMessages: Int, actorMbs: [ActorMb!]): Unit {
 ## Launcher.
 def main(numActors: Int): Unit {
 
-  let actorMbs = spawnActors(numActors, (nil : [ActorMb!])) in
+  let actorMbs = spawnActors(numActors, (nil : List(ActorMb!))) in
     floodActors(1000, actorMbs)
 }
 
diff --git a/test/examples/savina/lists/robotsn.pat b/test/examples/savina/lists/robotsn.pat
index dea2417..f1acfa2 100644
--- a/test/examples/savina/lists/robotsn.pat
+++ b/test/examples/savina/lists/robotsn.pat
@@ -117,14 +117,14 @@ def handlePartTaken(self: Warehouse?, door: Door!): Unit {
     }
 }
 
-def discardList(xs: [Robot!]) : Unit {
-    caseL xs : [Robot!] of {
+def discardList(xs: List(Robot!)) : Unit {
+    caseL xs : List(Robot!) of {
         nil -> ()
         | (a :: as) -> discardList(as)
     }
 }
 
-def spawnRobots(numRobots: Int, door: Door!, acc: [Robot!]): Unit {
+def spawnRobots(numRobots: Int, door: Door!, acc: List(Robot!)): Unit {
     if (numRobots <= 0) {
         discardList(acc)
     } else {
@@ -138,7 +138,7 @@ def main(n: Int): Unit {
     let door = new[Door] in
     let warehouse = new[Warehouse] in
     spawn { freeDoor(door, warehouse) };
-    spawnRobots(n, door, (nil : [Robot!]));
+    spawnRobots(n, door, (nil : List(Robot!)));
     spawn { freeWarehouse(warehouse) }
 }
 
diff --git a/test/pat-tests/list-1.pat b/test/pat-tests/list-1.pat
index 2df1fae..996c699 100644
--- a/test/pat-tests/list-1.pat
+++ b/test/pat-tests/list-1.pat
@@ -1,6 +1,6 @@
 def main() : Unit {
-    let xs = (5 :: (nil : [Int])) in
-    caseL xs : [Int] of {
+    let xs = (5 :: (nil : List(Int))) in
+    caseL xs : List(Int) of {
           nil -> print("nil")
         | (y :: ys) -> print(intToString(y))
     }
diff --git a/test/pat-tests/list-2.pat b/test/pat-tests/list-2.pat
index 167c961..d290227 100644
--- a/test/pat-tests/list-2.pat
+++ b/test/pat-tests/list-2.pat
@@ -1,20 +1,20 @@
-def snoc(xs : [Int], x : Int): [Int] {
-    caseL xs : [Int] of {
-        nil -> (x :: (nil : [Int]))
+def snoc(xs : List(Int), x : Int): List(Int) {
+    caseL xs : List(Int) of {
+        nil -> (x :: (nil : List(Int)))
       | (y :: ys) -> (y :: snoc(ys, x))
     }
 }
 
-def reverse(xs : [Int]): [Int] {
-    caseL xs : [Int] of {
+def reverse(xs : List(Int)): List(Int) {
+    caseL xs : List(Int) of {
           nil -> nil
         | (y :: ys) -> snoc(reverse(ys), y)
     }
 }
 
 def main(): Unit {
-    let xs = (1 :: (2 :: (3 :: (nil : [Int])))) in
-    caseL reverse(xs) : [Int] of {
+    let xs = (1 :: (2 :: (3 :: (nil : List(Int))))) in
+    caseL reverse(xs) : List(Int) of {
         nil -> print("nil")
       | (y :: ys) -> print(intToString(y))
   }

From e802e4634070b8c89c6bc1b339397a44ba67875a Mon Sep 17 00:00:00 2001
From: Danielle Marshall <danielle@starsandspira.ls>
Date: Thu, 4 Dec 2025 16:10:09 +0000
Subject: [PATCH 30/33] pretty-print list type with new syntax

---
 lib/common/pretype.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/lib/common/pretype.ml b/lib/common/pretype.ml
index 48ba145..976d354 100644
--- a/lib/common/pretype.ml
+++ b/lib/common/pretype.ml
@@ -40,7 +40,7 @@ let rec pp ppf =
             pp t1
             pp t2
     | PList t ->
-        Format.fprintf ppf "[%a]"
+        Format.fprintf ppf "List(%a)"
             pp t
     | PInterface name -> ps name
 

From a219814197a5e6a84c8c68cf860cf47558ae5915 Mon Sep 17 00:00:00 2001
From: Danielle Marshall <danielle@starsandspira.ls>
Date: Thu, 4 Dec 2025 16:27:09 +0000
Subject: [PATCH 31/33] update test suite json with list tests/examples and
 move some badly named/located tests

---
 test/errors/uaf_lists.pat                     |  4 +--
 .../lists/robotsn.pat => robotsn-lists.pat}   |  0
 test/pat-tests/list-broken.pat                | 16 ----------
 test/pat-tests/list-mb.pat                    | 16 ++++++++++
 test/tests.json                               | 31 +++++++++++++++++++
 5 files changed, 49 insertions(+), 18 deletions(-)
 rename test/examples/{savina/lists/robotsn.pat => robotsn-lists.pat} (100%)
 delete mode 100644 test/pat-tests/list-broken.pat
 create mode 100644 test/pat-tests/list-mb.pat

diff --git a/test/errors/uaf_lists.pat b/test/errors/uaf_lists.pat
index 58d4d76..1ab6a12 100644
--- a/test/errors/uaf_lists.pat
+++ b/test/errors/uaf_lists.pat
@@ -9,8 +9,8 @@ def drain(x: Test?): Unit {
 
 def go(): Unit {
     let x = new[Test] in
-    let xs = (x cons (nil: [Test![U]])) in
-    caseL xs : [Test!] of {
+    let xs = (x cons (nil: List(Test![U]))) in
+    caseL xs : List(Test!) of {
           nil -> ()
         | (a cons as) -> x ! M(a)
     };
diff --git a/test/examples/savina/lists/robotsn.pat b/test/examples/robotsn-lists.pat
similarity index 100%
rename from test/examples/savina/lists/robotsn.pat
rename to test/examples/robotsn-lists.pat
diff --git a/test/pat-tests/list-broken.pat b/test/pat-tests/list-broken.pat
deleted file mode 100644
index a5cef84..0000000
--- a/test/pat-tests/list-broken.pat
+++ /dev/null
@@ -1,16 +0,0 @@
-interface Test {
-  Ping()
-}
-
-def spawnMbs(acc : [Test!]) : [Test!] {
-    acc
-}
-
-def test(mbs : [Test!]) : Unit {
-    ()
-}
-
-def main() : Unit {
-    let mbs = spawnMbs(nil : [Test!]) in
-    test(mbs)
-}
diff --git a/test/pat-tests/list-mb.pat b/test/pat-tests/list-mb.pat
new file mode 100644
index 0000000..95a6006
--- /dev/null
+++ b/test/pat-tests/list-mb.pat
@@ -0,0 +1,16 @@
+interface Test {
+  Ping()
+}
+
+def spawnMbs(acc : List(Test!)) : List(Test!) {
+    acc
+}
+
+def test(mbs : List(Test!)) : Unit {
+    ()
+}
+
+def main() : Unit {
+    let mbs = spawnMbs(nil : List(Test!)) in
+    test(mbs)
+}
diff --git a/test/tests.json b/test/tests.json
index ce43bae..5958e0a 100644
--- a/test/tests.json
+++ b/test/tests.json
@@ -103,6 +103,21 @@
                     "name": "n-tuples, bad (2)",
                     "filename": "pat-tests/n-tuples-bad-2.pat",
                     "exit_code": 1
+                },
+                {
+                    "name": "Lists (1)",
+                    "filename": "pat-tests/list-1.pat",
+                    "exit_code": 0
+                },
+                {
+                    "name": "Lists (2)",
+                    "filename": "pat-tests/list-2.pat",
+                    "exit_code": 0
+                },
+                {
+                    "name": "Lists (with mailboxes)",
+                    "filename": "pat-tests/list-mb.pat",
+                    "exit_code": 0
                 }
             ]
         },
@@ -136,10 +151,21 @@
                 {"name": "Thread Ring", "filename": "examples/savina/thread_ring.pat", "exit_code": 0}
             ]
         },
+        { "group": "Correct examples (Savina with lists)",
+          "tests":
+            [
+                {"name": "Banking (lists)", "filename": "examples/savina/lists/banking.pat", "exit_code": 0},
+                {"name": "Big (lists)", "filename": "examples/savina/lists/big.pat", "exit_code": 0},
+                {"name": "Cigarette Smoker (lists)", "filename": "examples/savina/lists/cig_smok.pat", "exit_code": 0},
+                {"name": "kfork (lists)", "filename": "examples/savina/lists/kfork.pat", "exit_code": 0},
+                {"name": "Sleeping Barber", "filename": "examples/savina/lists/barber.pat", "exit_code": 0}
+            ]
+        },
         { "group": "Correct examples (Others)",
           "tests":
             [
                 {"name": "n-Robots", "filename": "examples/robotsn.pat", "exit_code": 0},
+                {"name": "n-Robots (lists)", "filename": "examples/robotsn-lists.pat", "exit_code": 0},
                 {"name": "Guard annotation is a subpattern", "filename": "examples/pat_constr.pat", "exit_code": 0}
             ]
         },
@@ -179,6 +205,11 @@
                     "filename": "errors/uaf3.pat",
                     "exit_code": 1
                 },
+                {
+                    "name": "Use after free (lists)",
+                    "filename": "errors/uaf_lists.pat",
+                    "exit_code": 1
+                },
                 {"name": "Insufficient type information", "filename": "errors/pat_constr.pat", "exit_code": 1},
                 {"name": "Non-exhaustive guards", "filename": "errors/pat_constr2.pat", "exit_code": 1},
                 {"name": "Additional non-supported non-fail guard with nontrivial continuation", "filename": "errors/pat_constr3.pat", "exit_code": 1},

From 3329019ceb2df45800534d5f8beff0376e51c02a Mon Sep 17 00:00:00 2001
From: Danielle Marshall <danielle@starsandspira.ls>
Date: Thu, 4 Dec 2025 16:27:35 +0000
Subject: [PATCH 32/33] restore smoker example that got broken at some point

---
 test/examples/savina/cig_smok.pat | 49 +++++++++++++++----------------
 1 file changed, 23 insertions(+), 26 deletions(-)

diff --git a/test/examples/savina/cig_smok.pat b/test/examples/savina/cig_smok.pat
index a8a737e..ed15e78 100644
--- a/test/examples/savina/cig_smok.pat
+++ b/test/examples/savina/cig_smok.pat
@@ -1,12 +1,13 @@
-### Adapted from Savina/fjthrput.
+### Adapted from Savina/cigsmok.
 ###
-### Models the creation of n actors that are given a number of messages, for
-### each of which, a computation is performed. The benchmark is parameterized by
-### the number of actor processes. Since the array type is not available in
-### Pat, we fix the number of actor processes to 3.
-
-interface ActorMb {
-  Packet()
+### A benchmark modelling n smokers and one arbiter that decides which smoker to
+### allow to smoke. The benchmark is parameterized by the number of smoker 
+### processes. Since the array type is not available in Pat, we fix the number 
+### of account processes to 3.
+
+interface ArbiterMb {
+  Start(),
+  StartedSmoking()
 }
 
 interface SmokerMb {
@@ -34,10 +35,14 @@ def arbiter(self: ArbiterMb?, numRounds: Int): Unit {
   }
 }
 
-## Computes the factorial of n.
-def fact(n: Int): Int {
-  if (n <= 0) {
-    1
+## Randomly chooses the smoker and requests it to smoke.
+def notify_smoker(smokerMb1: SmokerMb!, smokerMb2: SmokerMb!, smokerMb3: SmokerMb!): Unit {
+
+  let smokerId = rand(2) in
+  let sleepTimeMs = 1000 in
+
+  if (smokerId == 0) {
+    smokerMb1 ! StartSmoking(rand(sleepTimeMs))
   }
   else {
     if (smokerId == 1) {
@@ -112,21 +117,13 @@ def smoker_exit(self: SmokerMb?): Unit {
   }
 }
 
-## Launcher.
+## Launcher.
 def main(): Unit {
+  
+  let arbiterMb = new [ArbiterMb] in
+  spawn { arbiter(arbiterMb, 10) };
 
-  let actorMb1 = new [ActorMb] in
-  spawn { actor(actorMb1) };
-
-  let actorMb2 = new [ActorMb] in
-  spawn { actor(actorMb2) };
-
-  let actorMb3 = new [ActorMb] in
-  spawn { actor(actorMb3) };
-
-  flood(100, actorMb1);
-  flood(1000, actorMb1);
-  flood(10000, actorMb1)
+  arbiterMb ! Start()
 }
 
-main()
+main()
\ No newline at end of file

From 0db38156e5f43ee7725b3fabd33b10e7ed819c79 Mon Sep 17 00:00:00 2001
From: Danielle Marshall <danielle@starsandspira.ls>
Date: Fri, 5 Dec 2025 09:54:46 +0000
Subject: [PATCH 33/33] more list pretty printing

---
 lib/common/type.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/lib/common/type.ml b/lib/common/type.ml
index dd10f8b..f11c787 100644
--- a/lib/common/type.ml
+++ b/lib/common/type.ml
@@ -329,7 +329,7 @@ let rec pp ppf =
             pp t1
             pp t2
     | List t ->
-        fprintf ppf "[%a]"
+        fprintf ppf "List(%a)"
             pp t
     | Mailbox { capability; interface; pattern; quasilinearity } ->
         let ql =