1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
|
{-# LANGUAGE NoImplicitPrelude #-}
{-# LANGUAGE RecordWildCards #-}
module Test.Golden where
import Api qualified
import Provers qualified
import Tptp.UnsortedFirstOrder (toText)
import Base
import Provers (defaultTimeLimit)
import Control.Monad.Logger
import Control.Monad.Reader
import Data.Text qualified as Text
import Data.Text.IO qualified as TextIO
import Data.Text.Lazy.IO qualified as LazyTextIO
import System.Directory
import System.FilePath
import Test.Tasty
import Test.Tasty.Golden (goldenVsFile, findByExtension)
import Text.Pretty.Simple (pShowNoColor)
import UnliftIO
import UnliftIO.Environment
import Api (Options(withDumpPremselTraining))
testOptions :: Api.Options
testOptions = Api.Options
{ Api.withDumpPremselTraining = Api.WithoutDumpPremselTraining
, Api.withCache = Api.WithoutCache
, Api.withFilter = Api.WithoutFilter
, inputPath = error "testOptions: no inputPath"
, withDump = Api.WithoutDump
, withLogging = Api.WithoutLogging
, withMemoryLimit = Provers.defaultMemoryLimit
, withOmissions = Api.WithOmissions
, withParseOnly = Api.WithoutParseOnly
, withProver = Api.WithDefaultProver
, withTimeLimit = Provers.defaultTimeLimit
, withVersion = Api.WithoutVersion
, withMegalodon = Api.WithoutMegalodon
, withFailList = Api.WithoutFailList
}
goldenTests :: IO TestTree
goldenTests = runReaderT goldenTestGroup testOptions
goldenTestGroup :: (MonadUnliftIO io, MonadReader Api.Options io) => io TestTree
goldenTestGroup = testGroup "golden tests" <$> sequence
[ tokenizing
, scanning
, parsing
, glossing
, generatingTasks
, encodingTasks
, verification
]
-- | A testing triple consists of a an 'input' file, which is proccesed, resulting
-- in 'output' file, which is then compared to a 'golden' file.
data Triple = Triple
{ input :: FilePath
, output :: FilePath
, golden :: FilePath
}
deriving (Show, Eq)
-- | Gathers all the files for the test. We test all examples and everything in @test/pass/@.
-- The golden files for all tests are stored in @test/pass/@, so we need to adjust the filepath
-- of the files from @examples/@.
gatherTriples :: MonadIO io => String -> io [Triple]
gatherTriples stage = do
inputs <- liftIO (findByExtension [".tex"] "test/examples")
pure $
[ Triple{..}
| input <- inputs
, let input' = "test" </> "golden" </> takeBaseName input </> stage
, let golden = input' <.> "golden"
, let output = input' <.> "out"
]
createTripleDirectoriesIfMissing :: MonadIO io => Triple -> io ()
createTripleDirectoriesIfMissing Triple{..} = liftIO $
createDirectoryIfMissing True (takeDirectory output)
makeGoldenTest :: (MonadUnliftIO io, MonadReader Api.Options io) => String -> (Triple -> io ()) -> io TestTree
makeGoldenTest stage action = do
triples <- gatherTriples stage
for triples createTripleDirectoriesIfMissing
runInIO <- askRunInIO
pure $ testGroup stage
[ goldenVsFile
(takeBaseName input) -- test name
golden
output
(runInIO (action triple))
| triple@Triple{..} <- triples
]
tokenizing :: (MonadUnliftIO io, MonadReader Api.Options io) => io TestTree
tokenizing = makeGoldenTest "tokenizing" $ \Triple{..} -> do
tokenStream <- Api.tokenize input
liftIO (LazyTextIO.writeFile output (pShowNoColor (Api.simpleStream tokenStream)))
scanning :: (MonadUnliftIO io, MonadReader Api.Options io) => io TestTree
scanning = makeGoldenTest "scanning" $ \Triple{..} -> do
lexicalItems <- Api.scan input
liftIO (LazyTextIO.writeFile output (pShowNoColor lexicalItems))
parsing :: (MonadUnliftIO io, MonadReader Api.Options io) => io TestTree
parsing = makeGoldenTest "parsing" $ \Triple{..} -> do
(parseResult, _) <- Api.parse input
liftIO (LazyTextIO.writeFile output (pShowNoColor parseResult))
glossing :: (MonadUnliftIO io, MonadReader Api.Options io) => io TestTree
glossing = makeGoldenTest "glossing" $ \Triple{..} -> do
(interpretationResult, _) <- Api.gloss input
liftIO (LazyTextIO.writeFile output (pShowNoColor interpretationResult))
generatingTasks :: (MonadUnliftIO io, MonadReader Api.Options io) => io TestTree
generatingTasks = makeGoldenTest "generating tasks" $ \Triple{..} -> do
(tasks, _) <- Api.generateTasks input
liftIO $ LazyTextIO.writeFile output (pShowNoColor tasks)
encodingTasks :: (MonadUnliftIO io, MonadReader Api.Options io) => io TestTree
encodingTasks = makeGoldenTest "encoding tasks" $ \Triple{..} -> do
tasks <- Api.encodeTasks input
liftIO (TextIO.writeFile output (Text.intercalate "\n------------------\n" (toText <$> tasks)))
verification :: (MonadUnliftIO io, MonadReader Api.Options io) => io TestTree
verification = makeGoldenTest "verification" $ \Triple{..} -> do
vampirePathPath <- (?? "vampire") <$> lookupEnv "NAPROCHE_VAMPIRE"
let defaultProverInstance = Provers.vampire vampirePathPath Provers.Silent Provers.defaultTimeLimit Provers.defaultMemoryLimit
answers <- runNoLoggingT (Api.verify defaultProverInstance input)
liftIO (LazyTextIO.writeFile output (pShowNoColor answers))
|
