94 lines
2.7 KiB
Idris
94 lines
2.7 KiB
Idris
|
module Tests.FromPTerm
|
|||
|
|
|
|||
|
|
import Quox.Parser.Syntax
|
|||
|
|
import Quox.Parser
|
|||
|
|
import TermImpls
|
|||
|
|
import TAP
|
|||
|
|
|
|||
|
|
import Derive.Prelude
|
|||
|
|
%language ElabReflection
|
|||
|
|
|
|||
|
|
public export
|
|||
|
|
data Failure =
|
|||
|
|
LexError Lexer.Error
|
|||
|
|
| ParseError (List1 (ParsingError Token))
|
|||
|
|
| FromPTermError FromPTermError
|
|||
|
|
| WrongResult String
|
|||
|
|
| ExpectedFail String
|
|||
|
|
|
|||
|
|
%runElab derive "Syntax.FromPTermError" [Show]
|
|||
|
|
|
|||
|
|
export
|
|||
|
|
ToInfo Failure where
|
|||
|
|
toInfo (LexError err) =
|
|||
|
|
[("type", "LexError"), ("info", show err)]
|
|||
|
|
toInfo (ParseError errs) =
|
|||
|
|
("type", "ParseError") ::
|
|||
|
|
map (bimap show show) ([1 .. length errs] `zip` toList errs)
|
|||
|
|
toInfo (FromPTermError err) =
|
|||
|
|
[("type", "FromPTermError"),
|
|||
|
|
("got", show err)]
|
|||
|
|
toInfo (WrongResult got) =
|
|||
|
|
[("type", "WrongResult"), ("got", got)]
|
|||
|
|
toInfo (ExpectedFail got) =
|
|||
|
|
[("type", "ExpectedFail"), ("got", got)]
|
|||
|
|
|
|||
|
|
|
|||
|
|
parameters {c : Bool} {auto _ : Show b}
|
|||
|
|
(grm : Grammar c a) (fromP : a -> Either FromPTermError b)
|
|||
|
|
(inp : String)
|
|||
|
|
parameters {default (ltrim inp) label : String}
|
|||
|
|
parsesWith : (b -> Bool) -> Test
|
|||
|
|
parsesWith p = test label $ do
|
|||
|
|
toks <- mapFst LexError $ lex inp
|
|||
|
|
(pres, _) <- mapFst ParseError $ parse (grm <* eof) toks
|
|||
|
|
res <- mapFst FromPTermError $ fromP pres
|
|||
|
|
unless (p res) $ Left $ WrongResult $ show res
|
|||
|
|
|
|||
|
|
parses : Test
|
|||
|
|
parses = parsesWith $ const True
|
|||
|
|
|
|||
|
|
parsesAs : Eq b => b -> Test
|
|||
|
|
parsesAs exp = parsesWith (== exp)
|
|||
|
|
|
|||
|
|
parameters {default "\{ltrim inp} # fails" label : String}
|
|||
|
|
parseFails : Test
|
|||
|
|
parseFails = test label $ do
|
|||
|
|
toks <- mapFst LexError $ lex inp
|
|||
|
|
(pres, _) <- mapFst ParseError $ parse (grm <* eof) toks
|
|||
|
|
either (const $ Right ()) (Left . ExpectedFail . show) $ fromP pres
|
|||
|
|
|
|||
|
|
|
|||
|
|
FromString BName where fromString = Just . fromString
|
|||
|
|
|
|||
|
|
export
|
|||
|
|
tests : Test
|
|||
|
|
tests = "PTerm → Term" :- [
|
|||
|
|
"dimensions" :-
|
|||
|
|
let fromPDim = fromPDimWith [< "𝑖", "𝑗"]
|
|||
|
|
in [
|
|||
|
|
note "dim ctx: [𝑖, 𝑗]",
|
|||
|
|
parsesAs dim fromPDim "𝑖" (BV 1),
|
|||
|
|
parsesAs dim fromPDim "𝑗" (BV 0),
|
|||
|
|
parseFails dim fromPDim "𝑘",
|
|||
|
|
parsesAs dim fromPDim "0" (K Zero),
|
|||
|
|
parsesAs dim fromPDim "1" (K One)
|
|||
|
|
],
|
|||
|
|
|
|||
|
|
"terms" :-
|
|||
|
|
let fromPTerm' = fromPTermWith [< "𝑖", "𝑗"] [< "A", "x", "y", "z"]
|
|||
|
|
in [
|
|||
|
|
note "dim ctx: [𝑖, 𝑗]; term ctx: [A, x, y, z]",
|
|||
|
|
parsesAs term fromPTerm' "x" $ BVT 2,
|
|||
|
|
parseFails term fromPTerm' "𝑖",
|
|||
|
|
parsesAs term fromPTerm' "f" $ FT "f",
|
|||
|
|
parsesAs term fromPTerm' "λ w ⇒ w" $ ["w"] :\\ BVT 0,
|
|||
|
|
parsesAs term fromPTerm' "λ w ⇒ x" $ ["w"] :\\ BVT 3,
|
|||
|
|
parsesAs term fromPTerm' "λ x ⇒ x" $ ["x"] :\\ BVT 0,
|
|||
|
|
parsesAs term fromPTerm' "λ a b ⇒ f a b" $
|
|||
|
|
["a", "b"] :\\ E (F "f" :@@ [BVT 1, BVT 0]),
|
|||
|
|
parsesAs term fromPTerm' "f @𝑖" $
|
|||
|
|
E $ F "f" :% BV 1
|
|||
|
|
]
|
|||
|
|
]
|