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 + +