Add lists

generate-table.py

@@ -3,7 +3,7 @@
 import subprocess
 from tabulate import tabulate
 
-REPETITIONS = 100
+REPETITIONS = 1000
 
 BENCHMARKS =\
     [
@@ -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

lib/common/ir.ml

@@ -97,6 +97,12 @@ 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;
+        ty: (Type.t[@name "ty"]);
+        nil: comp;
+        cons: ((Binder.t[@name "binder"]) * (Binder.t[@name "binder"])) * comp
+    }
     | New of string
     | Spawn of comp
     | Send of {
@@ -119,6 +125,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 +197,16 @@ and pp_branch name ppf ((bnd, ty), c) =
         Binder.pp bnd
         Type.pp ty
         pp_comp c
+and pp_nil name ppf c =
+  fprintf ppf "%s([]) -> @[<v>%a@]"
+    name
+    pp_comp c
+and pp_cons name ppf ((bnd1, bnd2), c) =
+    fprintf ppf "%s(%a :: %a) -> @[<v>%a@]"
+        name
+        Binder.pp bnd1
+        Binder.pp bnd2
+        pp_comp c
 (* Expressions *)
 and pp_comp ppf comp_with_pos =
     let comp_node = WithPos.node comp_with_pos in
@@ -242,6 +260,13 @@ and pp_comp ppf comp_with_pos =
             pp_value term
             (pp_branch "inl") branch1
             (pp_branch "inr") branch2
+    | CaseL { term; ty; nil; cons } ->
+        fprintf ppf
+            "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; _ } ->
         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 ()
-

lib/common/pretype.ml

@@ -13,6 +13,7 @@ type t =
     | PInterface of string
     | PSum of (t * t)
     | PTuple of t list
+    | PList of t
     [@@name "pretype"]
     [@@deriving visitors { variety = "map" }]
 and base = [%import: Common_types.Base.t]
@@ -38,6 +39,9 @@ let rec pp ppf =
         fprintf ppf "(%a + %a)"
             pp t1
             pp t2
+    | PList t ->
+        Format.fprintf ppf "List(%a)"
+            pp t
     | PInterface name -> ps name
 
 let show t =
@@ -51,6 +55,7 @@ let rec of_type = function
         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)
     | Type.Mailbox { interface; _ } -> PInterface interface
 
 (* As long as a pretype isn't a mailbox type, and isn't a function
@@ -75,4 +80,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

lib/common/sugar_ast.ml

@@ -39,6 +39,15 @@ and expr_node =
         term: expr;
         cont: expr
     }
+    (* Lists *)
+    | Nil
+    | Cons of (expr * expr)
+    | CaseL of {
+        term: expr;
+        ty: (Type.t[@name "ty"]);
+        nil: expr;
+        cons: (sugar_binder * sugar_binder) * expr
+    }
     (* Sums *)
     | Inl of expr
     | Inr of expr
@@ -238,6 +247,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; 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@]@]@]}"
+            pp_expr term
+            Type.pp t1
+            pp_expr e1
+            pp_bnd_ann (b1, t)
+            pp_bnd_ann (b2, t1)
+            pp_expr e2
+        | _ -> fprintf ppf "bad list"
+      end
     | Guard { target; pattern; guards; _ } ->
         fprintf ppf
             "guard %a : %a {@,@[<v 2>  %a@]@,}"
@@ -246,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 } ->
@@ -255,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
@@ -284,4 +310,3 @@ let substitute_solution sol =
         end
     in
     visitor#visit_program ()
-

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
@@ -253,6 +254,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 +290,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 +328,9 @@ let rec pp ppf =
         fprintf ppf "(%a + %a)"
             pp t1
             pp t2
+    | List t ->
+        fprintf ppf "List(%a)"
+            pp t
     | Mailbox { capability; interface; pattern; quasilinearity } ->
         let ql =
             match quasilinearity with
@@ -358,6 +364,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
 
@@ -369,6 +376,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
@@ -377,6 +391,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,21 +412,20 @@ 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
+(* 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)
     | 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
     | _ -> true
 
 let make_function_type linear args result =
@@ -420,3 +437,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 ty

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 {
@@ -31,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. *)
@@ -80,6 +82,42 @@ 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
+                let nil_cont = self#visit_expr env nil_cont in
+                let cons_cont = self#visit_expr env cons_cont in
+                let new_case =
+                    CaseL {
+                        term;
+                        ty = ty_ann;
+                        nil = nil_cont;
+                        cons = ((x_bnd, xs_bnd), cons_cont)
+                    }
+                in
+                { expr_with_pos with node = new_case }
             | _ -> super#visit_expr env expr_with_pos
 
         method! visit_program env p =
@@ -103,4 +141,3 @@ let annotate prog =
         Format.(fprintf std_formatter "=== Annotated Program ===\n%a\n\n"
         Sugar_ast.pp_program prog));
     prog
-