From d8d857178744ba8bb4c75e5da26fd148a041fe6b Mon Sep 17 00:00:00 2001 From: Craig Roy Date: Mon, 14 Oct 2024 11:30:34 +0100 Subject: [PATCH 1/2] Kernel vec patterns and example --- brat/Brat/Constructors.hs | 22 ++++++++++++++++++++++ brat/examples/brick.brat | 20 ++++++++++++++++++++ 2 files changed, 42 insertions(+) create mode 100644 brat/examples/brick.brat diff --git a/brat/Brat/Constructors.hs b/brat/Brat/Constructors.hs index 127c9185..003b479e 100644 --- a/brat/Brat/Constructors.hs +++ b/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)]) ] diff --git a/brat/examples/brick.brat b/brat/examples/brick.brat new file mode 100644 index 00000000..f3957e49 --- /dev/null +++ b/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 +} From 5775a3b1b8e8ef444922ecdfd1b450dd9b33a2e8 Mon Sep 17 00:00:00 2001 From: Craig Roy Date: Mon, 14 Oct 2024 16:01:53 +0100 Subject: [PATCH 2/2] Slight improvement to a broken system --- brat/Brat/Checker.hs | 17 +++++++++-------- brat/Brat/Error.hs | 12 +++++++----- brat/test/Test/Compile/Hugr.hs | 3 ++- brat/test/golden/error/badvec3.brat.golden | 2 +- brat/test/golden/error/even-length.brat | 5 +++++ brat/test/golden/error/even-length.brat.golden | 10 ++++++++++ brat/test/golden/error/kbadvec3.brat.golden | 2 +- brat/test/golden/error/odd-length.brat | 5 +++++ brat/test/golden/error/odd-length.brat.golden | 10 ++++++++++ 9 files changed, 50 insertions(+), 16 deletions(-) create mode 100644 brat/test/golden/error/even-length.brat create mode 100644 brat/test/golden/error/even-length.brat.golden create mode 100644 brat/test/golden/error/odd-length.brat create mode 100644 brat/test/golden/error/odd-length.brat.golden diff --git a/brat/Brat/Checker.hs b/brat/Brat/Checker.hs index 77715cf1..9c5db8bf 100644 --- a/brat/Brat/Checker.hs +++ b/brat/Brat/Checker.hs @@ -798,9 +798,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. @@ -809,13 +809,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) diff --git a/brat/Brat/Error.hs b/brat/Brat/Error.hs index 869c5002..ea4f024d 100644 --- a/brat/Brat/Error.hs +++ b/brat/Brat/Error.hs @@ -18,10 +18,12 @@ newtype ParseError = PE { pretty :: String } 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 @@ -102,12 +104,12 @@ instance Show ErrorMsg where 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] diff --git a/brat/test/Test/Compile/Hugr.hs b/brat/test/Test/Compile/Hugr.hs index c8f64b6c..a864d589 100644 --- a/brat/test/Test/Compile/Hugr.hs +++ b/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" diff --git a/brat/test/golden/error/badvec3.brat.golden b/brat/test/golden/error/badvec3.brat.golden index 8e337fc8..d32751a0 100644 --- a/brat/test/golden/error/badvec3.brat.golden +++ b/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) diff --git a/brat/test/golden/error/even-length.brat b/brat/test/golden/error/even-length.brat new file mode 100644 index 00000000..2aa0a028 --- /dev/null +++ b/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]) diff --git a/brat/test/golden/error/even-length.brat.golden b/brat/test/golden/error/even-length.brat.golden new file mode 100644 index 00000000..9fa6ab1e --- /dev/null +++ b/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 + + diff --git a/brat/test/golden/error/kbadvec3.brat.golden b/brat/test/golden/error/kbadvec3.brat.golden index b9552ded..dca4b419 100644 --- a/brat/test/golden/error/kbadvec3.brat.golden +++ b/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) diff --git a/brat/test/golden/error/odd-length.brat b/brat/test/golden/error/odd-length.brat new file mode 100644 index 00000000..33a95fcf --- /dev/null +++ b/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]) diff --git a/brat/test/golden/error/odd-length.brat.golden b/brat/test/golden/error/odd-length.brat.golden new file mode 100644 index 00000000..82638e32 --- /dev/null +++ b/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 + +