9eb6a481980d81a55898ba418fba72fc3c09d8c8Dominik LueckeDescription : Parser for basic specs
85f112f807210b70172aab985810a37dc6a85eb3Dominik LueckeCopyright : (c) Dominik Luecke, Uni Bremen 2007
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : GPLv2 or higher, see LICENSE.txt
2eeec5240b424984e3ee26296da1eeab6c6d739eChristian MaederMaintainer : luecke@informatik.uni-bremen.de
85f112f807210b70172aab985810a37dc6a85eb3Dominik LueckeStability : experimental
85f112f807210b70172aab985810a37dc6a85eb3Dominik LueckePortability : portable
a785627ef4d2e3c73d9e5b8f7352fc859b85dd2bDominik LueckeParser for abstract syntax for propositional logic
1d677cafe64269a9c961396b85b5b50c126f58d8Dominik Luecke <http://en.wikipedia.org/wiki/Propositional_logic>
202df46772cac2ee2e8627ba196a5faebb6f9a05Christian Maeder ( basicSpec -- Parser for basic specs
202df46772cac2ee2e8627ba196a5faebb6f9a05Christian Maeder , symbMapItems
feeab95fdf7ec92bcce607c104d9dc98e0e6ea90Soeren D. Schulzeimport Common.GlobalAnnotations (PrefixMap)
202df46772cac2ee2e8627ba196a5faebb6f9a05Christian Maederimport Propositional.AS_BASIC_Propositional as AS_BASIC
1d677cafe64269a9c961396b85b5b50c126f58d8Dominik LueckepropKeywords :: [String]
10bcd3a204795307ba4f95009ce72b49383420b3cmaederpropKeywords = criticalKeywords ++
1d677cafe64269a9c961396b85b5b50c126f58d8Dominik Luecke-- | Toplevel parser for basic specs
47b25f012c45a226b702e24b90dedd1a351f5a62cmaederbasicSpec :: PrefixMap -> AParser st AS_BASIC.BASIC_SPEC
47b25f012c45a226b702e24b90dedd1a351f5a62cmaeder fmap AS_BASIC.Basic_spec (annosParser parseBasicItems)
47b25f012c45a226b702e24b90dedd1a351f5a62cmaeder <|> (oBraceT >> cBraceT >> return (AS_BASIC.Basic_spec []))
1d677cafe64269a9c961396b85b5b50c126f58d8Dominik Luecke-- | Parser for basic items
47b25f012c45a226b702e24b90dedd1a351f5a62cmaederparseBasicItems :: AParser st AS_BASIC.BASIC_ITEMS
3936130e6ca87cc693e25838609e86fba272b3aaChristian MaederparseBasicItems = parsePredDecl <|> parseAxItems
9984f2853694755d0c74782b2581e4e3cee86502Dominik Luecke-- | parser for predicate declarations
47b25f012c45a226b702e24b90dedd1a351f5a62cmaederparsePredDecl :: AParser st AS_BASIC.BASIC_ITEMS
9984f2853694755d0c74782b2581e4e3cee86502Dominik LueckeparsePredDecl = fmap AS_BASIC.Pred_decl predItem
9984f2853694755d0c74782b2581e4e3cee86502Dominik Luecke-- | parser for Axiom_items
47b25f012c45a226b702e24b90dedd1a351f5a62cmaederparseAxItems :: AParser st AS_BASIC.BASIC_ITEMS
3936130e6ca87cc693e25838609e86fba272b3aaChristian MaederparseAxItems = do
47b25f012c45a226b702e24b90dedd1a351f5a62cmaeder (fs, ds) <- aFormula `separatedBy` dotT
47b25f012c45a226b702e24b90dedd1a351f5a62cmaeder (_, an) <- optSemi
47b25f012c45a226b702e24b90dedd1a351f5a62cmaeder let _ = catRange (d : ds)
47b25f012c45a226b702e24b90dedd1a351f5a62cmaeder ns = init fs ++ [appendAnno (last fs) an]
da955132262baab309a50fdffe228c9efe68251dCui Jian-- | Any word to token
47b25f012c45a226b702e24b90dedd1a351f5a62cmaederpropId :: GenParser Char st Token
47b25f012c45a226b702e24b90dedd1a351f5a62cmaederpropId = pToken $ reserved propKeywords scanAnyWords
1d677cafe64269a9c961396b85b5b50c126f58d8Dominik Luecke-- | parser for predicates = propositions
47b25f012c45a226b702e24b90dedd1a351f5a62cmaederpredItem :: AParser st AS_BASIC.PRED_ITEM
47b25f012c45a226b702e24b90dedd1a351f5a62cmaeder v <- asKey (propS ++ sS) <|>
47b25f012c45a226b702e24b90dedd1a351f5a62cmaeder asKey propS
47b25f012c45a226b702e24b90dedd1a351f5a62cmaeder (ps, cs) <- propId `separatedBy` anComma
47b25f012c45a226b702e24b90dedd1a351f5a62cmaeder return $ AS_BASIC.Pred_item ps $ catRange $ v : cs
1d677cafe64269a9c961396b85b5b50c126f58d8Dominik Luecke-- | Parser for implies @=>@
47b25f012c45a226b702e24b90dedd1a351f5a62cmaederimplKey :: AParser st Token
47b25f012c45a226b702e24b90dedd1a351f5a62cmaederimplKey = asKey implS
1d677cafe64269a9c961396b85b5b50c126f58d8Dominik Luecke-- | Parser for and @\/\ @
47b25f012c45a226b702e24b90dedd1a351f5a62cmaederandKey :: AParser st Token
47b25f012c45a226b702e24b90dedd1a351f5a62cmaederandKey = asKey lAnd
1d677cafe64269a9c961396b85b5b50c126f58d8Dominik Luecke-- | Parser for or @\\\/@
47b25f012c45a226b702e24b90dedd1a351f5a62cmaederorKey :: AParser st Token
47b25f012c45a226b702e24b90dedd1a351f5a62cmaederorKey = asKey lOr
da955132262baab309a50fdffe228c9efe68251dCui Jian-- | Parser for true
47b25f012c45a226b702e24b90dedd1a351f5a62cmaedertrueKey :: AParser st Token
47b25f012c45a226b702e24b90dedd1a351f5a62cmaedertrueKey = asKey trueS
85f112f807210b70172aab985810a37dc6a85eb3Dominik Luecke-- | Parser for false
47b25f012c45a226b702e24b90dedd1a351f5a62cmaederfalseKey :: AParser st Token
47b25f012c45a226b702e24b90dedd1a351f5a62cmaederfalseKey = asKey falseS
85f112f807210b70172aab985810a37dc6a85eb3Dominik Luecke-- | Parser for not
47b25f012c45a226b702e24b90dedd1a351f5a62cmaedernotKey :: AParser st Token
47b25f012c45a226b702e24b90dedd1a351f5a62cmaedernotKey = asKey notS
85f112f807210b70172aab985810a37dc6a85eb3Dominik Luecke-- | Parser for negation
47b25f012c45a226b702e24b90dedd1a351f5a62cmaedernegKey :: AParser st Token
47b25f012c45a226b702e24b90dedd1a351f5a62cmaedernegKey = asKey negS
1d677cafe64269a9c961396b85b5b50c126f58d8Dominik Luecke-- | Parser for equivalence @<=>@
47b25f012c45a226b702e24b90dedd1a351f5a62cmaederequivKey :: AParser st Token
47b25f012c45a226b702e24b90dedd1a351f5a62cmaederequivKey = asKey equivS
a785627ef4d2e3c73d9e5b8f7352fc859b85dd2bDominik Luecke-- | Parser for primitive formulae
47b25f012c45a226b702e24b90dedd1a351f5a62cmaederprimFormula :: AParser st AS_BASIC.FORMULA
da955132262baab309a50fdffe228c9efe68251dCui JianprimFormula =
85f112f807210b70172aab985810a37dc6a85eb3Dominik Luecke do c <- trueKey
47b25f012c45a226b702e24b90dedd1a351f5a62cmaeder return (AS_BASIC.True_atom $ tokPos c)
85f112f807210b70172aab985810a37dc6a85eb3Dominik Luecke do c <- falseKey
47b25f012c45a226b702e24b90dedd1a351f5a62cmaeder return (AS_BASIC.False_atom $ tokPos c)
85f112f807210b70172aab985810a37dc6a85eb3Dominik Luecke do c <- notKey <|> negKey <?> "\"not\""
1d677cafe64269a9c961396b85b5b50c126f58d8Dominik Luecke k <- primFormula
47b25f012c45a226b702e24b90dedd1a351f5a62cmaeder return (AS_BASIC.Negation k $ tokPos c)
1d677cafe64269a9c961396b85b5b50c126f58d8Dominik Luecke <|> parenFormula
da955132262baab309a50fdffe228c9efe68251dCui Jian <|> fmap AS_BASIC.Predication propId
a785627ef4d2e3c73d9e5b8f7352fc859b85dd2bDominik Luecke-- | Parser for formulae containing 'and' and 'or'
47b25f012c45a226b702e24b90dedd1a351f5a62cmaederandOrFormula :: AParser st AS_BASIC.FORMULA
3936130e6ca87cc693e25838609e86fba272b3aaChristian MaederandOrFormula = do
47b25f012c45a226b702e24b90dedd1a351f5a62cmaeder f <- primFormula
47b25f012c45a226b702e24b90dedd1a351f5a62cmaeder do c <- andKey
47b25f012c45a226b702e24b90dedd1a351f5a62cmaeder (fs, ps) <- primFormula `separatedBy` andKey
47b25f012c45a226b702e24b90dedd1a351f5a62cmaeder return . AS_BASIC.Conjunction (f : fs) . catRange $ c : ps
47b25f012c45a226b702e24b90dedd1a351f5a62cmaeder (fs, ps) <- primFormula `separatedBy` orKey
47b25f012c45a226b702e24b90dedd1a351f5a62cmaeder return . AS_BASIC.Disjunction (f : fs) . catRange $ c : ps
47b25f012c45a226b702e24b90dedd1a351f5a62cmaeder <|> return f
a785627ef4d2e3c73d9e5b8f7352fc859b85dd2bDominik Luecke-- | Parser for formulae with implications
47b25f012c45a226b702e24b90dedd1a351f5a62cmaederimpFormula :: AParser st AS_BASIC.FORMULA
3936130e6ca87cc693e25838609e86fba272b3aaChristian MaederimpFormula = do
47b25f012c45a226b702e24b90dedd1a351f5a62cmaeder f <- andOrFormula
47b25f012c45a226b702e24b90dedd1a351f5a62cmaeder do c <- implKey
47b25f012c45a226b702e24b90dedd1a351f5a62cmaeder (fs, ps) <- andOrFormula `separatedBy` implKey
47b25f012c45a226b702e24b90dedd1a351f5a62cmaeder return . makeImpl (f : fs) . catPosAux $ c : ps
47b25f012c45a226b702e24b90dedd1a351f5a62cmaeder c <- equivKey
47b25f012c45a226b702e24b90dedd1a351f5a62cmaeder g <- andOrFormula
47b25f012c45a226b702e24b90dedd1a351f5a62cmaeder return . AS_BASIC.Equivalence f g $ tokPos c
47b25f012c45a226b702e24b90dedd1a351f5a62cmaeder <|> return f
47b25f012c45a226b702e24b90dedd1a351f5a62cmaeder makeImpl [f, g] p = AS_BASIC.Implication f g (Range p)
47b25f012c45a226b702e24b90dedd1a351f5a62cmaeder makeImpl (f : r) (c : p) = AS_BASIC.Implication f (makeImpl r p) (Range [c])
47b25f012c45a226b702e24b90dedd1a351f5a62cmaeder makeImpl _ _ = error "makeImpl got illegal argument"
1d677cafe64269a9c961396b85b5b50c126f58d8Dominik Luecke-- | Parser for formulae with parentheses
47b25f012c45a226b702e24b90dedd1a351f5a62cmaederparenFormula :: AParser st AS_BASIC.FORMULA
3936130e6ca87cc693e25838609e86fba272b3aaChristian MaederparenFormula = do
47b25f012c45a226b702e24b90dedd1a351f5a62cmaeder oParenT << addAnnos
47b25f012c45a226b702e24b90dedd1a351f5a62cmaeder f <- impFormula << addAnnos
47b25f012c45a226b702e24b90dedd1a351f5a62cmaeder cParenT >> return f
1d677cafe64269a9c961396b85b5b50c126f58d8Dominik Luecke-- | Toplevel parser for formulae
47b25f012c45a226b702e24b90dedd1a351f5a62cmaederaFormula :: AParser st (Annoted AS_BASIC.FORMULA)
47b25f012c45a226b702e24b90dedd1a351f5a62cmaederaFormula = allAnnoParser impFormula
202df46772cac2ee2e8627ba196a5faebb6f9a05Christian Maeder-- | parsing a prop symbol
202df46772cac2ee2e8627ba196a5faebb6f9a05Christian Maedersymb :: GenParser Char st SYMB
202df46772cac2ee2e8627ba196a5faebb6f9a05Christian Maedersymb = fmap Symb_id propId
202df46772cac2ee2e8627ba196a5faebb6f9a05Christian Maeder-- | parsing one symbol or a mapping of one to a second symbol
202df46772cac2ee2e8627ba196a5faebb6f9a05Christian MaedersymbMap :: GenParser Char st SYMB_OR_MAP
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder do f <- pToken $ toKey mapsTo
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder return (Symb_map s t $ tokPos f)
202df46772cac2ee2e8627ba196a5faebb6f9a05Christian Maeder <|> return (Symb s)
202df46772cac2ee2e8627ba196a5faebb6f9a05Christian Maeder-- | Parse a list of comma separated symbols.
202df46772cac2ee2e8627ba196a5faebb6f9a05Christian MaedersymbItems :: GenParser Char st SYMB_ITEMS
202df46772cac2ee2e8627ba196a5faebb6f9a05Christian MaedersymbItems = do
202df46772cac2ee2e8627ba196a5faebb6f9a05Christian Maeder (is, ps) <- symbs
202df46772cac2ee2e8627ba196a5faebb6f9a05Christian Maeder return (Symb_items is $ catRange ps)
202df46772cac2ee2e8627ba196a5faebb6f9a05Christian Maeder-- | parse a comma separated list of symbols
202df46772cac2ee2e8627ba196a5faebb6f9a05Christian Maedersymbs :: GenParser Char st ([SYMB], [Token])
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder do c <- commaT `followedWith` symb
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder (is, ps) <- symbs
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder return (s : is, c : ps)
202df46772cac2ee2e8627ba196a5faebb6f9a05Christian Maeder <|> return ([s], [])
202df46772cac2ee2e8627ba196a5faebb6f9a05Christian Maeder-- | parse a list of symbol mappings
202df46772cac2ee2e8627ba196a5faebb6f9a05Christian MaedersymbMapItems :: GenParser Char st SYMB_MAP_ITEMS
202df46772cac2ee2e8627ba196a5faebb6f9a05Christian MaedersymbMapItems = do
202df46772cac2ee2e8627ba196a5faebb6f9a05Christian Maeder (is, ps) <- symbMaps
3936130e6ca87cc693e25838609e86fba272b3aaChristian Maeder return (Symb_map_items is $ catRange ps)
202df46772cac2ee2e8627ba196a5faebb6f9a05Christian Maeder-- | parse a comma separated list of symbol mappings
202df46772cac2ee2e8627ba196a5faebb6f9a05Christian MaedersymbMaps :: GenParser Char st ([SYMB_OR_MAP], [Token])
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder do c <- commaT `followedWith` symb
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder (is, ps) <- symbMaps
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder return (s : is, c : ps)
202df46772cac2ee2e8627ba196a5faebb6f9a05Christian Maeder <|> return ([s], [])