Newer
Older
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
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE OverloadedStrings #-}
module Server (runApi) where
import Data.Maybe
import qualified Data.Map as M
import Data.List.Split (splitOn)
import Control.Monad.Trans (liftIO)
import Data.Vector (fromList)
import Data.ByteString.Lazy (ByteString)
import Data.Proxy
import Data.Text.Lazy.Encoding (encodeUtf8)
import Data.Text.Lazy (pack)
import Data.Aeson
import Control.Monad.Trans.Except
import System.IO
import GHC.Generics
import Network.HTTP.Types
import Network.Wai.Handler.Warp
import Network.Wai
import Servant
import Servant.Server
import Servant.Docs
import SimpleFormulaChecker (compareSpec)
import qualified SimpleFormulaChecker as S
import LogicIR.Backend.Z3.Model
-- | Data types.
type ApiArg = String
data ApiResponseType = Equivalent | NotEquivalent | Undefined
deriving Generic
data ApiResponse = ApiResponse
{ responseType :: ApiResponseType
, model :: Maybe Z3Model
}
deriving Generic
instance ToJSON ApiResponseType
instance ToJSON ApiResponse
instance ToJSON ModelVal where
toJSON (BoolVal b) = toJSON b
toJSON (IntVal n) = toJSON n
toJSON (RealVal n) = toJSON n
toJSON (ManyVal vs) = Array $ fromList $ map toJSON vs
type CompareApi = "compare"
:> QueryParam "a" ApiArg
:> QueryParam "b" ApiArg
:> Get '[JSON] ApiResponse
compareApi :: Proxy CompareApi
compareApi = Proxy
-- | API documentation.
instance ToParam (QueryParam "a" String) where
toParam _ =
DocQueryParam "a" ["examples/javawlp_edsl/src/nl/uu/javawlp_edsl/Main.java:real1", "..."]
"Method location formatted as: <java_source_file>:<method_name>"
Normal
instance ToParam (QueryParam "b" String) where
toParam _ =
DocQueryParam "b" ["examples/javawlp_edsl/src/nl/uu/javawlp_edsl/Main.java:real2", "..."]
"Method location formatted as: <java_source_file>:<method_name>" Normal
instance ToSample ApiResponse where
toSamples _ = singleSample ApiResponse
{ responseType = NotEquivalent
, model = Just $ M.fromList
[ ("a", ManyVal [RealVal 0.0, RealVal (-0.5)])
, ("i", IntVal 10)
]
}
docsBS :: ByteString
docsBS = encodeUtf8
. pack
. markdown
$ docsWithIntros [intro] compareApi
where intro = DocIntro "Welcome" ["This is our webservice's API.", "Enjoy!"]
apiDocs :: API
apiDocs = docs compareApi
type DocsApi = CompareApi :<|> Raw
docsApi :: Proxy DocsApi
docsApi = Proxy
server :: Server DocsApi
server = server' :<|> Tagged serveDocs where
serveDocs _ respond =
respond $ responseLBS ok200 [plain] docsBS
plain = ("Content-Type", "text/plain")
app :: Application
app = serve docsApi server
-- | Server implementation.
runApi :: IO ()
runApi = do
let port = 8888
settings =
setPort port $
setBeforeMainLoop (hPutStrLn stderr ("listening on port " ++ show port))
defaultSettings
runSettings settings app
server' :: Server CompareApi
server' = getCompareResponse
getCompareResponse :: Maybe String -> Maybe String -> Handler ApiResponse
getCompareResponse a b = do
let [srcA, methodA] = splitOn ":" (fromJust a)
let [srcB, methodB] = splitOn ":" (fromJust b)
response <- liftIO $ compareSpec (srcA, methodA) (srcB, methodB)
return $ case response of
S.Equivalent ->
ApiResponse { responseType = Equivalent, model = Nothing }
S.NotEquivalent model ->
ApiResponse { responseType = NotEquivalent, model = Just model }
_ -> ApiResponse { responseType = Undefined, model = Nothing }