diff --git a/CTLParser.hs b/CTLParser.hs index 74ea9c4bab18ac3c29f2cf86722644a75fae1bc8..6f0fe3b8695504a4caf4eef4bc4c26678b34d4bd 100644 --- a/CTLParser.hs +++ b/CTLParser.hs @@ -3,6 +3,7 @@ module CTLParser where import qualified CTL as C import CTL(CTL) import Data.Char(isLower) +import Data.Either(isLeft) import Data.Maybe(isNothing,fromJust) data Token p = @@ -25,13 +26,11 @@ data Token p = parseCTLFull :: String -> Either String (CTL Char) parseCTLFull str = do tokens <- tokenizeCTL str - let res = parseCTL tokens - if isNothing res then - Left "Parse error" - else if not $ null $ fst $ fromJust res then - Left $ "Parse not completed, '" ++ show (fst $ fromJust res) ++ "' was left over" + res <- parseCTL tokens + if not $ null $ fst res then + Left $ "Parse not completed, '" ++ show (fst res) ++ "' was left over" else - Right $ snd $ fromJust res + Right $ snd res tokenizeCTL :: String -> Either String [Token Char] tokenizeCTL = mapM tokenizeCTLChar @@ -54,27 +53,27 @@ tokenizeCTLChar x | isLower x = Right $ Proposition x tokenizeCTLChar x = Left $ "Unknown input character " ++ show x -parseCTL :: [Token p] -> Maybe ([Token p], CTL p) -parseCTL [] = Nothing +parseCTL :: Show p => [Token p] -> Either String ([Token p], CTL p) +parseCTL [] = Left "Expected formula, got EOF" parseCTL xs = do (rest, left) <- parseCTLsingle xs if null rest then return (rest, left) else do - let getOp Until = Just C.Until - getOp Or = Just C.Or - getOp And = Just C.And - getOp _ = Nothing + let getOp Until = Right C.Until + getOp Or = Right C.Or + getOp And = Right C.And + getOp _ = Left "" op' = getOp $ head rest - if isNothing op' then + if isLeft op' then return (rest, left) else do op <- op' right <- parseCTL $ tail rest return $ op left <$> right -parseCTLsingle :: [Token p] -> Maybe ([Token p], CTL p) -parseCTLsingle (Proposition p:rest) = Just (rest, C.Proposition p) +parseCTLsingle :: Show p => [Token p] -> Either String ([Token p], CTL p) +parseCTLsingle (Proposition p:rest) = Right (rest, C.Proposition p) parseCTLsingle (Negation:rest) = fmap C.Negation <$> parseCTL rest parseCTLsingle (Globally:rest) = fmap C.Globally <$> parseCTL rest parseCTLsingle (Finally:rest) = fmap C.Finally <$> parseCTL rest @@ -85,5 +84,7 @@ parseCTLsingle (Start:rest) = do (rest',content) <- parseCTL rest case rest' of (End:rest'') -> return (rest'',content) - _ -> Nothing -parseCTLsingle _ = Nothing + (x:_) -> Left $ "Expected 'End' (aka ')'), got '" ++ show x ++ "'" + [] -> Left "Expected 'End' (aka ')'), got EOF" +parseCTLsingle (x:_) = Left $ "Expected Proposition, Unary Operator, or 'Start' (aka '('), got '" ++ show x ++ "'" +parseCTLsingle [] = Left "Expected Proposition, Unary Operator, or 'Start' (aka '('), got EOF"