Skip to content
Find file
Fetching contributors…
Cannot retrieve contributors at this time
138 lines (105 sloc) 4.72 KB
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TypeSynonymInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE Rank2Types #-}
module JCU.Types where
import Control.Applicative
import Data.Aeson as AE
import qualified Data.Attoparsec.Lazy as AP
import qualified Data.ByteString.Lazy.Char8 as LBS
import qualified Data.ByteString.Char8 as BS
import Data.ListLike (CharStringLazy(..))
import Data.String
import Data.Tree (Tree(..))
import Language.Prolog.NanoProlog.NanoProlog
import Language.Prolog.NanoProlog.Parser
import Text.ParserCombinators.UU.BasicInstances (Parser(), Error, LineColPos)
data DBRule
= DBRule
{ ruleId :: Int
, ruleOrder :: Int
, rule :: Rule
}
data DropReq = DropReq Proof [Int] Rule
deriving Show
data DropRes = DropRes Bool Proof
deriving Show
data Status = Correct
| Incomplete
| Invalid
deriving Show
data AddRes = AddRes Int
type Proof = Tree Term
type PCheck = Tree Status
type ErrorMsg = BS.ByteString
instance ToJSON DBRule where
toJSON (DBRule rid ro rl) = object [ "id" .= rid
, "ro" .= ro
, "rule" .= show rl]
instance FromJSON DropReq where
parseJSON (Object o) = mkJSONDropReq <$> o .: "proof"
<*> o .: "treeLvl"
<*> o .: "rule"
parseJSON val = fail $ "No case for (FromJSON DropReq) with value: " ++ show val
mkJSONDropReq :: Value -> [Int] -> LBS.ByteString -> DropReq
mkJSONDropReq prf lvl rl = DropReq mkProofTree lvl (mkJSONRule rl)
where mkProofTree = case fromJSON prf :: AE.Result Proof of
(AE.Success a) -> a
(AE.Error err) -> error ("Error parsing drop request: " ++ err)
instance ToJSON DropRes where
toJSON (DropRes ufd prf) = object ["unified" .= ufd, "nproof" .= prf]
instance ToJSON PCheck where
toJSON (Node st cs) = object [ "proofCheckResult" .= show st
, "proofCheckChildren" .= toJSON cs ]
instance ToJSON AddRes where
toJSON (AddRes r) = toJSON r
instance ToJSON Rule where
toJSON t = object [ "rule" .= show t ]
instance FromJSON Rule where
parseJSON (Object o) = mkJSONRule <$> o .: "rule"
parseJSON val = fail $ "No case for (FromJSON Rule) with value: " ++ show val
-- TODO: Errors
mkJSONRule :: LBS.ByteString -> Rule
mkJSONRule = fst . startParse pRule . CSL
instance FromJSON Proof where
parseJSON (Object o) = mkJSONProofTree <$> o .: "rootLabel" <*> o .: "childTerms"
parseJSON val = fail $ "No case for (FromJSON Proof) with value: " ++ show val
instance ToJSON Proof where
toJSON (Node t ps) = object [ "term" .= show t
, "childTerms" .= toJSON ps ]
mkJSONProofTree :: LBS.ByteString -> Value -> Proof
mkJSONProofTree tm rts = Node (mkJSONTerm tm) mkProofTrees
where mkProofTrees = case fromJSON rts :: AE.Result [Proof] of
(AE.Success a) -> a
(AE.Error err) -> error ("Error parsing proof tree: " ++ err)
-- TODO: Something with errors
mkJSONTerm :: LBS.ByteString -> Term
mkJSONTerm = fst . startParse pTerm . CSL
mkRule :: LBS.ByteString -> Either ErrorMsg Rule
mkRule = processJSON fromJSON
mkDropReq :: LBS.ByteString -> Either ErrorMsg DropReq
mkDropReq = processJSON fromJSON
mkProof :: LBS.ByteString -> Either ErrorMsg Proof
mkProof = processJSON fromJSON
processJSON :: (Value -> AE.Result a) -> LBS.ByteString -> Either ErrorMsg a
processJSON f raw =
case AP.parse json raw of
(AP.Done _ r) ->
case f r of
(AE.Success a) -> Right a
(AE.Error err) -> Left . fromString $ "Error converting ByteString to data type: " ++ err
(AP.Fail _ _ err) -> Left . fromString $ "Error parsing raw JSON: " ++ err
-- TODO: Try to get rid of the explicit annotations...
parseCheck :: Maybe BS.ByteString -> LBS.ByteString -> (Bool, [ErrorMsg])
parseCheck Nothing _ = checkErr [fromString "Unknown error."]
parseCheck (Just x) body
| x == "rule" = parseMsg pRule body
| x == "term" = parseMsg pTerm body
| otherwise = checkErr [fromString "Invalid type specified"]
where parseMsg :: Parser t -> LBS.ByteString -> (Bool, [ErrorMsg])
parseMsg p txt = writeRes $ startParse p (CSL txt)
writeRes :: (t, [Error LineColPos]) -> (Bool, [ErrorMsg])
writeRes (_, []) = (True, [])
writeRes (_, rs) = checkErr (map (fromString . show) rs)
checkErr :: [ErrorMsg] -> (Bool, [ErrorMsg])
checkErr msg = (False, msg)
Something went wrong with that request. Please try again.