Parser.hs revision e9458b1a7a19a63aa4c179f9ab20f4d50681c168
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann - Description : Implementation of logic formula parser
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann - Copyright : (c) Georgel Calin & Lutz Schroeder, DFKI Lab Bremen
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu Prodescu - License : GPLv2 or higher, see LICENSE.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
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder{- ----------------------------------
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederexperiment 2 starting here:
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder---------------------------------- -}
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder{- class (SigFeature a b (c d), SigFeature b c (e f)) => MyFeat a b c d e f where
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederyoyo :: (a (b (c d))) -> (b (c (e f)))
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederpGoOn3 :: (a (b (c d))) -> ModalOperator -> GenParser Char st (Formula (b (c (e f)))) -}
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder{- instance MyFeat K K K () K () where
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederyoyo sig = K [Mod (K [Mod (K [])])]
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederpGoOn3 sig flag = primFormula (yoyo sig) flag -}
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder{- instance MyFeat KD KD KD () KD () where
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederyoyo sig = KD [Mod (KD [Mod (KD [])])]
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederpGoOn3 sig flag = primFormula (yoyo sig) flag -}
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder{- instance MyFeat K KD K () KD () where
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederyoyo sig = KD [Mod (K [Mod (KD [])])]
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederpGoOn3 sig flag = primFormula (yoyo sig) flag -}
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder{- instance MyFeat KD K KD () K () where
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederyoyo sig = K [Mod (KD [Mod (K [])])]
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederpGoOn3 sig flag = primFormula (yoyo sig) flag -}
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder{- ----------------------------------
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederexperiment 1 starting here:
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder---------------------------------- -}
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder{- class SigFeature a b c => ParseMe a b c where
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederpGive :: (a (b c)) -> (b c)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederpGoOn2 :: (a (b c)) -> ModalOperator -> GenParser Char st (Formula (b c)) -}
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder{- instance (SigFeature K K (K d), ParseMe K K d) => ParseMe K K (K d) where
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederpGive = genericPGive
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederpGoOn2 = genericPGoOn2 -}
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder{- instance SigFeature K K () => ParseMe K K () where
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederpGive sig = trace ("finishing: " ++ sPretty sig) $ K []
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederpGoOn2 sig flag = trace ("finishing: " ++ sPretty sig) $ return F -}
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder{- instance (SigFeature KD KD (KD d), ParseMe KD KD d) => ParseMe KD KD (KD d) where
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederpGive = genericPGive
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederpGoOn2 = genericPGoOn2 -}
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder{- instance SigFeature KD KD () => ParseMe KD KD () where
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederpGive sig = trace ("finishing: " ++ sPretty sig) $ KD []
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederpGoOn2 sig flag = trace ("finishing: " ++ sPretty sig) $ return F -}
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder{- instance (SigFeature KD K (KD d), ParseMe K KD d) => ParseMe KD K (KD d) where
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederpGive = genericPGive
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederpGoOn2 = genericPGoOn2 -}
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder{- instance SigFeature K KD () => ParseMe K KD () where
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederpGive sig = trace ("finishing: " ++ sPretty sig) $ KD []
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederpGoOn2 sig flag = trace ("finishing: " ++ sPretty sig) $ return F -}
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder{- instance (SigFeature K KD (K d), ParseMe KD K d) => ParseMe K KD (K d) where
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederpGive = genericPGive
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederpGoOn2 = genericPGoOn2 -}
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder{- instance SigFeature KD K () => ParseMe KD K () where
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederpGive sig = trace ("finishing: " ++ sPretty sig) $ K []
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederpGoOn2 sig flag = trace ("finishing: " ++ sPretty sig) $ return F -}
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder{- 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))
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedergenericPGive sig = ((sSecondFeat sig) [Mod ((sSecondFeat (sNextSig sig)) [])]) -}
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder{- 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)))
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedergenericPGoOn2 sig flag = return T
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedergenericPGoOn2 sig flag = primFormula (pGive sig) flag -}
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann-- generic parsing stuff
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedergenericPGoOn :: (SigFeature a b (c d), SigFeature b c d) =>
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder a (b (c d)) -> ModalOperator -> Parser (Formula (b (c d)))
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedergenericPGoOn sig = primFormula (sNextSig sig)
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
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederparser :: (SigFeature a b c) => a (b c) -> ModalOperator ->
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Parser (Formula (a (b c)) )
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederparser = implFormula
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann-- | Parser which translates all implications in disjunctions & conjunctions
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederimplFormula :: (SigFeature a b c) => a (b c) -> ModalOperator ->
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder 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
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder <|> 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-- | Parser for disjunction - used for handling binding order
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederorFormula :: (SigFeature a b c) => a (b c) -> ModalOperator ->
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder 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
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederandFormula :: (SigFeature a b c) => a (b c) -> ModalOperator ->
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder 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
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder{- | Parse a primitive formula: T, F, ~f, <i>f, [i]f, p*,
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder - where i stands for an index, f for a formula and
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann - * for a series of digits i.e. and integer -}
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederprimFormula :: (SigFeature a b c) => a (b c) -> ModalOperator ->
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Parser (Formula (a (b c)) )
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederprimFormula sig flag =
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann do string "T"
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann <|> do string "F"
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder <|> 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
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder 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)))
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder _ -> return $ Mod (i f)
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann <|> do char '['
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann i <- sParser sig
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder 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)))
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder _ -> return $ Mod (i f)
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann <|> do char 'p'
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann i <- atomIndex
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder return $ Atom (fromInteger i)
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann-- | Parser for un-parenthesizing a formula
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederparenFormula :: (SigFeature a b c) => a (b c) -> ModalOperator ->
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Parser (Formula (a (b c)) )
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederparenFormula sig flag =
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann f <- parser sig flag
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann-- | Parse integer number
d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmannnatural :: GenParser Char st Integer
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroedernatural = 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