From 7923ca84defafb95811390e9964671f7a03a4250 Mon Sep 17 00:00:00 2001
From: Dominic Orchard <dom.orchard@gmail.com>
Date: Tue, 5 Mar 2019 17:08:14 +0000
Subject: [PATCH 1/2] fork C from the paper

---
 examples/Sessions.gr                                | 2 +-
 frontend/src/Language/Granule/Checker/Primitives.hs | 3 +++
 interpreter/src/Language/Granule/Eval.hs            | 1 +
 3 files changed, 5 insertions(+), 1 deletion(-)

diff --git a/examples/Sessions.gr b/examples/Sessions.gr
index 82715eaa6..e2ff00a5a 100644
--- a/examples/Sessions.gr
+++ b/examples/Sessions.gr
@@ -45,7 +45,7 @@ recvVec (S n) [c] =
 example2 : ∀ {n : Nat, a : Type}
          . N n → Vec n a → (Vec n a) <Session>
 example2 n list =
-  let c ← forkRep (λc → sendVec c list)
+  let c ← forkC (λc → sendVec c list)
   in recvVec n c
 
 main : (Vec 5 Int, Int) <Session>
diff --git a/frontend/src/Language/Granule/Checker/Primitives.hs b/frontend/src/Language/Granule/Checker/Primitives.hs
index 53a066fe3..43ad4e1ef 100644
--- a/frontend/src/Language/Granule/Checker/Primitives.hs
+++ b/frontend/src/Language/Granule/Checker/Primitives.hs
@@ -183,6 +183,9 @@ binaryOperators =
 builtinSrc :: String
 builtinSrc = [r|
 
+forkC : forall { s : Protocol, k : Coeffect, c : k } . ((Chan s) [c] -> () <Com>) -> ((Chan (Dual s)) [c]) <Com>
+forkC = builtin
+
 data
   ArrayStack
     (capacity : Nat)
diff --git a/interpreter/src/Language/Granule/Eval.hs b/interpreter/src/Language/Granule/Eval.hs
index 7616753b5..d1956f790 100755
--- a/interpreter/src/Language/Granule/Eval.hs
+++ b/interpreter/src/Language/Granule/Eval.hs
@@ -257,6 +257,7 @@ builtIns =
         return . (Pure ()) . Val nullSpan () $ Constr () (mkId ",") [Ext () $ Handle h, boolflag])
   , (mkId "fork",    Ext () $ PrimitiveClosure fork)
   , (mkId "forkRep", Ext () $ PrimitiveClosure forkRep)
+  , (mkId "forkC", Ext () $ PrimitiveClosure forkRep)
   , (mkId "recv",    Ext () $ Primitive recv)
   , (mkId "send",    Ext () $ Primitive send)
   , (mkId "close",   Ext () $ Primitive close)

From 306bb5bb3960b75a64aa43d7b192618fd7352dc4 Mon Sep 17 00:00:00 2001
From: Dominic Orchard <dom.orchard@gmail.com>
Date: Tue, 5 Mar 2019 17:08:25 +0000
Subject: [PATCH 2/2] fix signatures of pattern related things

---
 .../src/Language/Granule/Checker/Patterns.hs     | 16 ++++++++--------
 1 file changed, 8 insertions(+), 8 deletions(-)

diff --git a/frontend/src/Language/Granule/Checker/Patterns.hs b/frontend/src/Language/Granule/Checker/Patterns.hs
index 58702a8bf..a88186d1d 100644
--- a/frontend/src/Language/Granule/Checker/Patterns.hs
+++ b/frontend/src/Language/Granule/Checker/Patterns.hs
@@ -67,21 +67,21 @@ polyShaped t = case leftmostOfApplication t of
 --      - a substitution for variables
 --           caused by pattern matching (e.g., from unification),
 --      - a consumption context explaining usage triggered by pattern matching
-ctxtFromTypedPattern :: (?globals :: Globals, Show t) =>
+ctxtFromTypedPattern :: (?globals :: Globals) =>
   Span
   -> Type
-  -> Pattern t
+  -> Pattern ()
   -> Consumption   -- Consumption behaviour of the patterns in this position so far
   -> MaybeT Checker (Ctxt Assumption, Ctxt Kind, Substitution, Pattern Type, Consumption)
 
 ctxtFromTypedPattern = ctxtFromTypedPattern' Nothing
 
 -- | Inner helper, which takes information about the enclosing coeffect
-ctxtFromTypedPattern' :: (?globals :: Globals, Show t) =>
+ctxtFromTypedPattern' :: (?globals :: Globals) =>
      Maybe (Coeffect, Type)    -- enclosing coeffect
   -> Span
   -> Type
-  -> Pattern t
+  -> Pattern ()
   -> Consumption   -- Consumption behaviour of the patterns in this position so far
   -> MaybeT Checker (Ctxt Assumption, Ctxt Kind, Substitution, Pattern Type, Consumption)
 
@@ -229,9 +229,9 @@ ctxtFromTypedPattern' outerBoxTy _ ty p@(PConstr s _ dataC ps) cons = do
         _ -> halt $ PatternTypingError (Just s) $
                   "Expected type `" <> pretty ty <> "` but got `" <> pretty dataConstructorTypeFresh <> "`"
   where
-    unpeel :: Show t
+    unpeel ::
           -- A list of patterns for each part of a data constructor pattern
-            => [Pattern t]
+               [Pattern ()]
             -- The remaining type of the constructor
             -> Type
             -> MaybeT Checker (Ctxt Assumption, Ctxt Kind, Substitution, [Pattern Type], Consumption)
@@ -256,10 +256,10 @@ ctxtFromTypedPattern' _ s t p _ = do
   halt $ PatternTypingError (Just s)
     $ "Pattern match `" <> pretty p <> "` does not match expected type `" <> pretty t <> "`"
 
-ctxtFromTypedPatterns :: (?globals :: Globals, Show t)
+ctxtFromTypedPatterns :: (?globals :: Globals)
   => Span
   -> Type
-  -> [Pattern t]
+  -> [Pattern ()]
   -> [Consumption]
   -> MaybeT Checker (Ctxt Assumption, Type, Ctxt Kind, Substitution, [Pattern Type], [Consumption])
 ctxtFromTypedPatterns sp ty [] _ = do