blob: 312e1da9327bcc4232ed4f284b4a16a96f710d68 (
plain)
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
|
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE NoImplicitPrelude #-}
-- | Exact prepared-request dump publication.
module Felix.RequestDump
( DumpObservationError(..)
, prepareRequestObserver
, captureDumpFailure
, renderDumpObservationError
) where
import Base
import Felix.Output.Atomic (writeBytesAtomically)
import Felix.OutputPlan qualified as Output
import Felix.Verification
( VerificationRequestObserver
, verificationRequestObserver
)
import Felix.Provers
import Control.Exception (displayException)
import Control.Exception qualified as Exception
import Data.Text qualified as Text
import System.Directory qualified as Directory
import System.FilePath.Posix qualified as Posix
data DumpObservationError
= DumpDirectoryCreationFailed !FilePath !Text
| DumpRequestWriteFailed !WorkPosition !FilePath !Text
deriving stock (Show, Eq)
instance Exception.Exception DumpObservationError
prepareRequestObserver
:: Maybe Output.DumpOutputPlan
-> IO (Either DumpObservationError VerificationRequestObserver)
prepareRequestObserver = \case
Nothing ->
pure
(Right
(verificationRequestObserver
(\_position _request -> pure ())))
Just dumpPlan -> do
let root = Output.dumpOutputPath dumpPlan
created <- tryIOError
(Directory.createDirectoryIfMissing True root)
pure case created of
Left failure ->
Left
(DumpDirectoryCreationFailed
root
(Text.pack (displayException failure)))
Right () ->
Right (verificationRequestObserver (writeDumpRequest root))
writeDumpRequest
:: FilePath
-> WorkPosition
-> PreparedVerificationRequest
-> IO ()
writeDumpRequest root position request = do
let destination =
root
Posix.</> ( show (workPositionModuleOrdinal position)
<> "-"
<> show (workPositionLocalRequestOrdinal position)
)
Posix.<.> "p"
tryIOError
(writeBytesAtomically
destination
(preparedVerificationBytes request)) >>= \case
Left failure ->
Exception.throwIO
(DumpRequestWriteFailed
position
destination
(Text.pack (displayException failure)))
Right () -> pure ()
captureDumpFailure
:: IO value
-> IO (Either DumpObservationError value)
captureDumpFailure = Exception.try
renderDumpObservationError :: DumpObservationError -> Text
renderDumpObservationError = \case
DumpDirectoryCreationFailed path message ->
"Could not create dump directory "
<> Text.pack (show path)
<> ": "
<> message
DumpRequestWriteFailed _position path message ->
"Could not write request dump "
<> Text.pack (show path)
<> ": "
<> message
|
