module Tests.Parser import Quox.Syntax import Quox.Parser import Quox.Lexer import Tests.Lexer import Data.SnocVect import Text.Parser import TAP export Show tok => ToInfo (ParsingError tok) where toInfo (Error msg Nothing) = [("msg", msg)] toInfo (Error msg (Just loc)) = [("loc", show loc), ("msg", msg)] numberErrs : List1 Info -> Info numberErrs (head ::: []) = head numberErrs (head ::: tail) = go 0 (head :: tail) where number1 : Nat -> Info -> Info number1 n = map $ \(k, v) => (show n ++ k, v) go : Nat -> List Info -> Info go k [] = [] go k (x :: xs) = number1 k x ++ go (S k) xs export ToInfo Parser.Error where toInfo (Lex err) = toInfo err toInfo (Parse errs) = numberErrs $ map toInfo errs toInfo (Leftover toks) = toInfo [("leftover", toks)] RealError = Quox.Parser.Error %hide Lexer.RealError %hide Quox.Parser.Error data Error a = Parser RealError | Unexpected a a | ShouldFail a export Show a => ToInfo (Error a) where toInfo (Parser err) = toInfo err toInfo (Unexpected exp got) = toInfo $ [("expected", exp), ("received", got)] toInfo (ShouldFail got) = toInfo [("success", got)] parameters {c : Bool} (grm : Grammar c a) (input : String) parses : (Show a, Eq a) => a -> Test parses exp = test "\"\{input}\"" $ delay $ case lexParseAll grm input of Right got => if got == exp then Right () else Left $ Unexpected exp got Left err => Left $ Parser err rejects : Show a => Test rejects = test "\"\{input}\" (reject)" $ do case lexParseAll grm input of Left err => Right () Right val => Left $ ShouldFail val tests = "parser" :- [ "numbers" :- let parses = parses number in [ parses "0" 0, parses "1" 1, parses "1000" 1000 ], "bound vars (x, y, z ⊢)" :- let grm = bound [< "x", "y", "z"] parses = parses grm; rejects = rejects grm in [ parses "x" (V 2), parses "y" (V 1), parses "z" (V 0), rejects "M.x", rejects "x.a", rejects "a" ], "bound or free vars (x, y, z ⊢)" :- let parses = parses $ nameWith [< "x", "y", "z"] in [ parses "x" (Left (V 2)), parses "y" (Left (V 1)), parses "z" (Left (V 0)), parses "a" (Right (MakeName [<] (UN "a"))), parses "a.b.c" (Right (MakeName [< "a", "b"] (UN "c"))), parses "a . b . c" (Right (MakeName [< "a", "b"] (UN "c"))), parses "M.x" (Right (MakeName [< "M"] (UN "x"))), parses "x.a" (Right (MakeName [< "x"] (UN "a"))) ], "dimension (x, y, z ⊢)" :- let grm = dimension [< "x", "y", "z"] parses = parses grm; rejects = rejects grm in [ parses "0" (K Zero), parses "1" (K One), rejects "2", parses "x" (B (V 2)), rejects "a" ] ]