Allow vector patterns to be used in kernels

brat/Brat/Checker.hs

@@ -866,9 +866,9 @@ detectVecErrors :: UserName  -- Term constructor name
                 -> Checking (Error -> Error)  -- Returns error wrapper to use for recursion
 detectVecErrors vcon (PrefixName [] "Vec") [_, VNum n] [_, VPNum p] ty tp =
   case numMatch B0 n p of
-    Left (NumMatchFail _ _) -> do
-      p' <- toLenConstr p
-      err $ getVecErr tp (show ty) (show n) p'
+    Left (NumMatchFail _ _) -> case (toLenConstr p) of
+      Right p' -> err $ getVecErr tp (show ty) (show n) p'
+      Left p' -> err $ InternalError ("detectVecErrors: Unexpected pattern: " ++ show (toLenConstr p'))
     -- Even if we succed here, the error might pop up when checking the
     -- rest of the vector. We return a function here that intercepts the
     -- error and extends it to the whole vector.
@@ -877,13 +877,14 @@ detectVecErrors vcon (PrefixName [] "Vec") [_, VNum n] [_, VPNum p] ty tp =
                  pure (consError fc tp (show ty) n)
          else pure id
  where
-  -- For constructors that produce something of type Vec we should
-  -- only ever get the patterns NP0 (if vcon == PrefixName [] "nil")
-  -- and NP1Plus (if vcon == PrefixName [] "cons")
-  toLenConstr :: NumPat -> Checking LengthConstraint
+  -- Try to work out the length of a vector
+  -- We only want to know if the vector length is nil or a successor
+  toLenConstr :: NumPat -> Either NumPat (LengthConstraint)
   toLenConstr NP0 = pure $ Length 0
+  toLenConstr (NP1Plus (NP2Times np)) = either (const (Right LengthOdd)) Right (toLenConstr np)
   toLenConstr (NP1Plus _) = pure $ LongerThan 0
-  toLenConstr p = err $ InternalError ("detectVecErrors: Unexpected pattern: " ++ show p)
+  toLenConstr (NP2Times np) = either (const (Right LengthEven)) Right (toLenConstr np)
+  toLenConstr p = Left p
 detectVecErrors _ _ _ _ _ _ = pure id
 
 getVecErr :: Either (Term d k) Pattern -> (String -> String -> LengthConstraint -> ErrorMsg)

brat/Brat/Constructors.hs

@@ -121,6 +121,28 @@ kernelConstructors = M.fromList
        (RPr ("tail", TVec (VApp (VInx (VS VZ)) B0) (VNum $ nVar (VInx VZ)))
         (RPr ("head", VApp (VInx (VS VZ)) B0) R0)))
      ])
+  ,(CConcatEqEven, M.fromList
+     [(CVec, CArgs [VPVar, VPNum (NP2Times NPVar)] (Sy (Sy Zy))
+      -- Star should be a TypeFor m forall m?
+      (REx ("elementType", Star []) ((REx ("halfLength", Nat) (R0))))
+      (RPr ("lhs", TVec (VApp (VInx (VS VZ)) B0) (VApp (VInx VZ) B0))
+        (RPr ("rhs", TVec (VApp (VInx (VS VZ)) B0) (VApp (VInx VZ) B0)) R0)))
+     ])
+  ,(CRiffle, M.fromList
+     [(CVec, CArgs [VPVar, VPNum (NP2Times NPVar)] (Sy (Sy Zy))
+      -- Star should be a TypeFor m forall m?
+      (REx ("elementType", Star []) ((REx ("halfLength", Nat) (R0))))
+      (RPr ("evens", TVec (VApp (VInx (VS VZ)) B0) (VApp (VInx VZ) B0))
+        (RPr ("odds", TVec (VApp (VInx (VS VZ)) B0) (VApp (VInx VZ) B0)) R0)))
+     ])
+  ,(CConcatEqOdd, M.fromList
+     [(CVec, CArgs [VPVar, VPNum (NP1Plus (NP2Times NPVar))] (Sy (Sy Zy))
+      -- Star should be a TypeFor m forall m?
+      (REx ("elementType", Star []) ((REx ("halfLength", Nat) (R0))))
+      (RPr ("lhs", TVec (VApp (VInx (VS VZ)) B0) (VApp (VInx VZ) B0))
+        (RPr ("mid", VApp (VInx (VS VZ)) B0)
+          (RPr ("rhs", TVec (VApp (VInx (VS VZ)) B0) (VApp (VInx VZ) B0)) R0))))
+     ])
   ,(CTrue, M.fromList [(CBit, CArgs [] Zy R0 R0)])
   ,(CFalse, M.fromList [(CBit, CArgs [] Zy R0 R0)])
   ]

brat/Brat/Error.hs

@@ -18,10 +18,12 @@
 instance Show ParseError where
   show = pretty
 
-data LengthConstraintF a = Length a | LongerThan a deriving (Eq, Functor)
+data LengthConstraintF a = Length a | LongerThan a | LengthEven | LengthOdd deriving (Eq, Functor)
 instance Show a => Show (LengthConstraintF a) where
-  show (Length a) = show a
-  show (LongerThan a) = "(> " ++ show a ++ ")"
+  show (Length a) = "of length " ++ show a
+  show (LongerThan a) = "with length (> " ++ show a ++ ")"
+  show LengthEven = "of even length"
+  show LengthOdd = "of odd length"
 
 type LengthConstraint = LengthConstraintF Int
 
@@ -106,12 +108,12 @@
   show (VecLength tm ty exp act) = unlines ["Expected vector of length " ++ exp
                                        ,"from the type:  " ++ ty
                                        ,"but got vector: " ++ tm
-                                       ,"of length " ++ show act
+                                       ,show act
                                        ]
   show (VecPatLength abs ty exp act) = unlines ["Pattern: " ++ abs
                                        ,"doesn't match type " ++ ty
                                        ,"(expected vector pattern of length " ++ exp ++
-                                        " but got vector pattern of length " ++ show act ++ ")"
+                                        " but got vector pattern " ++ show act ++ ")"
                                        ]
   show (NotVecPat tm ty)= unwords ["Expected", tm
                                   ,"to be a vector pattern when binding type", ty]
@@ -167,7 +169,7 @@
   show UnreachableBranch = "Branch cannot be reached"
   show (CompilingHoles hs) = unlines ("Can't compile file with remaining holes": indent hs)
    where
     indent = fmap ("  " ++)
   show (ThunkLeftOvers overs) = "Expected function to address all inputs, but " ++ overs ++ " wasn't used"
   show (ThunkLeftUnders unders) = "Expected function to return additional values of type: " ++ unders
 
@@ -209,8 +211,8 @@
     ls = lines contents
   in case endLineN - startLineN of
        0 -> [ls!!startLineN, highlightSection startCol endCol]
        n | n > 0 -> let (first:rest) = drop (startLineN - 1) $ take (endLineN + 1) ls
                         (last:rmid) = reverse rest
                     in [first, highlightSection startCol (length first)]
                        ++ (reverse rmid >>= (\l -> [l, highlightSection 0 (length l)]))
                        ++ [last, highlightSection 0 endCol]

brat/examples/brick.brat

@@ -0,0 +1,20 @@
+-- Create a "brickwork" state
+-- Apply a parameterised unitary U to entangle every adjacent pair of qubits in a line architecture.
+-- (don't apply the gate to (q0, qn-1))
+brick(n :: #, -- The number of entangling gates
+      Vec(Float, n), -- Angles for each of the gates
+      U :: { Float -> { Qubit, Qubit -o Qubit, Qubit }}) -- Parameterised unitary
+  -> { Vec(Qubit, n + 1) -o Vec(Qubit, n + 1) }
+brick(0, [], _) = { .. }
+-- Odd number of gates, even number of qubits
+brick(succ(doub(n)), th ,- ths, U) = {
+  (q0 ,- qsEven) =%= (q1 ,- qsOdd) =>
+     let q0, q1 = U(th)(q0, q1) in
+       q0 ,- brick(doub(n), ths, U)(q1 ,- (qsEven =%= qsOdd))
+}
+-- Even number of gates, odd number of qubits
+brick(doub(succ(n)), th ,- ths, U) = { (q0 ,- qsl) =, qmid ,= qsr =>
+  let q1 ,- qs = brick(succ(doub(n)), ths, U)((qsl -, qmid) =,= qsr) in
+    let q0, q1 = U(th)(q0, q1) in
+      q0 ,- q1 ,- qs
+}

brat/test/Test/Compile/Hugr.hs

@@ -60,7 +60,8 @@ nonCompilingExamples = (expectedCheckingFails ++ expectedParsingFails ++
   -- Conjecture: These examples don't compile because number patterns in type
   -- signatures causes `kindCheck` to call `abstract`, creating "Selector"
   -- nodes, which we don't attempt to compile because we want to get rid of them
-  ,"vec-pats"
+  ,"brick" -- Creates Selectors
+
   -- Victims of #389
   ,"arith"
   ,"bell"

brat/test/golden/error/badvec3.brat.golden

@@ -5,6 +5,6 @@ v3 = cons(1, nil)
   Expected vector of length 0
 from the type:  Vec(Int, 0)
 but got vector: [1]
-of length (> 0)
+with length (> 0)
 
 

brat/test/golden/error/even-length.brat

@@ -0,0 +1,5 @@
+f(X :: *, n :: #, Vec(X, n)) -> Vec(X, n)
+f(X, n, xs) = xs
+
+g :: Vec(Nat, 3)
+g = f(Nat, 3, [1] =,= [2])

brat/test/golden/error/even-length.brat.golden

@@ -0,0 +1,10 @@
+Error in test/golden/error/even-length.brat@FC {start = Pos {line = 5, col = 15}, end = Pos {line = 5, col = 26}}:
+g = f(Nat, 3, [1] =,= [2])
+              ^^^^^^^^^^^
+
+  Expected vector of length 3
+from the type:  Vec(VApp VPar In checking_check_defs_1_g_1_ 0 B0, VPar In checking_check_defs_1_g_1_ 1)
+but got vector: concatEqEven([1], [2])
+of even length
+
+

brat/test/golden/error/kbadvec3.brat.golden

@@ -5,6 +5,6 @@ constNil = { b => cons(1, nil) }
   Expected vector of length 0
 from the type:  Vec(Bit, 0)
 but got vector: [1]
-of length (> 0)
+with length (> 0)
 
 

brat/test/golden/error/odd-length.brat

@@ -0,0 +1,5 @@
+f(X :: *, n :: #, Vec(X, n)) -> Vec(X, n)
+f(X, n, xs) = xs
+
+g :: Vec(Nat, 4)
+g = f(Nat, 4, [1] =, 2 ,= [3])

brat/test/golden/error/odd-length.brat.golden

@@ -0,0 +1,10 @@
+Error in test/golden/error/odd-length.brat@FC {start = Pos {line = 5, col = 15}, end = Pos {line = 5, col = 30}}:
+g = f(Nat, 4, [1] =, 2 ,= [3])
+              ^^^^^^^^^^^^^^^
+
+  Expected vector of length 4
+from the type:  Vec(VApp VPar In checking_check_defs_1_g_1_ 0 B0, VPar In checking_check_defs_1_g_1_ 1)
+but got vector: concatEqOdd([1], 2, [3])
+of odd length
+
+