Parser.hs revision d1767fe15b7c3960e36996cc02977c0480ab4b17
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann{- | Module : $Header$
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann - Description : Implementation of logic formula parser
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann - Copyright : (c) Georgel Calin & Lutz Schroeder, DFKI Lab Bremen
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann - License : Similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann - Maintainer : g.calin@jacobs-university.de
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann - Stability : provisional
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann - Portability : portable
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann - Provides the implementation of the generic parser for the L formula datatype
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann------------------------------------
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann-- experiment 2 starting here:
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann------------------------------------
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann--class (SigFeature a b (c d), SigFeature b c (e f)) => MyFeat a b c d e f where
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann-- yoyo :: (a (b (c d))) -> (b (c (e f)))
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann-- pGoOn3 :: (a (b (c d))) -> ModalOperator -> GenParser Char st (Formula (b (c (e f))))
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann--instance MyFeat K K K () K () where
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann-- yoyo sig = K [Mod (K [Mod (K [])])]
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann-- pGoOn3 sig flag = primFormula (yoyo sig) flag
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann--instance MyFeat KD KD KD () KD () where
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann-- yoyo sig = KD [Mod (KD [Mod (KD [])])]
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann-- pGoOn3 sig flag = primFormula (yoyo sig) flag
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann--instance MyFeat K KD K () KD () where
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann-- yoyo sig = KD [Mod (K [Mod (KD [])])]
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann-- pGoOn3 sig flag = primFormula (yoyo sig) flag
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann--instance MyFeat KD K KD () K () where
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann-- yoyo sig = K [Mod (KD [Mod (K [])])]
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann-- pGoOn3 sig flag = primFormula (yoyo sig) flag
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann------------------------------------
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann-- experiment 1 starting here:
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann------------------------------------
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann--class SigFeature a b c => ParseMe a b c where
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann-- pGive :: (a (b c)) -> (b c)
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann-- pGoOn2 :: (a (b c)) -> ModalOperator -> GenParser Char st (Formula (b c))
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann--instance (SigFeature K K (K d), ParseMe K K d) => ParseMe K K (K d) where
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann-- pGive = genericPGive
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann-- pGoOn2 = genericPGoOn2
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann--instance SigFeature K K () => ParseMe K K () where
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann-- pGive sig = trace ("finishing: " ++ sPretty sig) $ K []
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann-- pGoOn2 sig flag = trace ("finishing: " ++ sPretty sig) $ return F
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann--instance (SigFeature KD KD (KD d), ParseMe KD KD d) => ParseMe KD KD (KD d) where
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann-- pGive = genericPGive
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann-- pGoOn2 = genericPGoOn2
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann--instance SigFeature KD KD () => ParseMe KD KD () where
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann-- pGive sig = trace ("finishing: " ++ sPretty sig) $ KD []
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann-- pGoOn2 sig flag = trace ("finishing: " ++ sPretty sig) $ return F
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann--instance (SigFeature KD K (KD d), ParseMe K KD d) => ParseMe KD K (KD d) where
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann-- pGive = genericPGive
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann-- pGoOn2 = genericPGoOn2
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann--instance SigFeature K KD () => ParseMe K KD () where
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann-- pGive sig = trace ("finishing: " ++ sPretty sig) $ KD []
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann-- pGoOn2 sig flag = trace ("finishing: " ++ sPretty sig) $ return F
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann--instance (SigFeature K KD (K d), ParseMe KD K d) => ParseMe K KD (K d) where
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann-- pGive = genericPGive
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann-- pGoOn2 = genericPGoOn2
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann--instance SigFeature KD K () => ParseMe KD K () where
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann-- pGive sig = trace ("finishing: " ++ sPretty sig) $ K []
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann-- pGoOn2 sig flag = trace ("finishing: " ++ sPretty sig) $ return F
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann--genericPGive :: (SigFeature a b (c d), SigFeature b c d, ParseMe a b (c d), ParseMe b c d) => (a (b (c d))) -> (b (c d))
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann--genericPGive sig = ((sSecondFeat sig) [Mod ((sSecondFeat (sNextSig sig)) [])])
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann--genericPGoOn2 :: (SigFeature a b (c d), SigFeature b c d, ParseMe a b (c d), ParseMe b c d) => (a (b (c d))) -> ModalOperator -> GenParser Char st (Formula (b (c d)))
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann--genericPGoOn2 sig flag = return T
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann--genericPGoOn2 sig flag = primFormula (pGive sig) flag
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann-- generic parsing stuff
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel HausmanngenericPGoOn :: (SigFeature a b (c d), SigFeature b c d) => (a (b (c d))) -> ModalOperator -> Parser (Formula (b (c d)))
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel HausmanngenericPGoOn sig flag = primFormula (sNextSig sig) flag
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann-- Normalised negation.
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmannnneg :: Formula (a b) -> Formula (a b)
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmannnneg (Neg phi) = phi
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmannnneg phi = Neg phi
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann-- | Main parser
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmannparser :: (SigFeature a b c) => (a (b c)) -> ModalOperator -> Parser (Formula (a (b c)) )
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmannparser sig flag = implFormula sig flag
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann-- | Parser which translates all implications in disjunctions & conjunctions
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel HausmannimplFormula :: (SigFeature a b c) => (a (b c)) -> ModalOperator -> Parser (Formula (a (b c)) )
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel HausmannimplFormula sig flag = do
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann f <- orFormula sig flag
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann option f (do string "->"
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann i <- implFormula sig flag
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann return $ Or (Neg f) i
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann <|> do try(string "<->")
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann i <- implFormula sig flag
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann return $ And (Or (Neg f) i) (Or f (Neg i))
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann <|> do string "<-"
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann i <- implFormula sig flag
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann return $ Or f (Neg i)
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann <|> do return f
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann-- | Parser for disjunction - used for handling binding order
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel HausmannorFormula :: (SigFeature a b c) => (a (b c)) -> ModalOperator -> Parser (Formula (a (b c)) )
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel HausmannorFormula sig flag = do
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann f <- andFormula sig flag
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann option f $ do
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann g <- orFormula sig flag
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann return $ Or f g
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann-- | Parser for conjunction - used for handling the binding order
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel HausmannandFormula :: (SigFeature a b c) => (a (b c)) -> ModalOperator -> Parser (Formula (a (b c)) )
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel HausmannandFormula sig flag = do
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann f <- primFormula sig flag
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann option f $ do
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann g <- andFormula sig flag
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann return $ And f g
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann{- | Parse a primitive formula: T, F, ~f, <i>f, [i]f, p*,
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann - where i stands for an index, f for a formula and
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann - * for a series of digits i.e. and integer -}
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel HausmannprimFormula :: (SigFeature a b c) => (a (b c)) -> ModalOperator -> Parser (Formula (a (b c)) )
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel HausmannprimFormula sig flag =
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann do string "T"
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann <|> do string "F"
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann <|> do f <- parenFormula sig flag
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann <|> do string "~"
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann f <- primFormula sig flag
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann return $ nneg f
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann <|> do char '<'
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann i <- sParser sig
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann f <- sepBy1 (pGoOn sig flag) (string (fSeparator sig))
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann -- restrict to the default modal operator
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann Ang -> return $ Mod (i f)
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann Sqr -> return $ Neg (Mod (i (map nneg f)))
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann _ -> return $ Mod (i f)
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann <|> do char '['
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann i <- sParser sig
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann f <- sepBy1 (pGoOn sig flag) (string (fSeparator sig))
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann -- restrict to the default modal operator
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann Sqr -> return $ Mod (i f)
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann Ang -> return $ Neg (Mod (i (map nneg f)))
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann _ -> return $ Mod (i f)
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann <|> do char 'p'
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann i <- atomIndex
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann return $ (Atom (fromInteger i))
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann-- | Parser for un-parenthesizing a formula
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel HausmannparenFormula :: (SigFeature a b c) => (a (b c)) -> ModalOperator -> Parser (Formula (a (b c)) )
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel HausmannparenFormula sig flag =
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann f <- parser sig flag
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann-- | Parse integer number
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmannnatural :: GenParser Char st Integer
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmannnatural = fmap read $ many1 digit
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann-- | Parse the possible integer index of a variable
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel HausmannatomIndex :: GenParser Char st Integer
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel HausmannatomIndex = do i <- try natural