{- |

Module : ./Propositional/Parse_AS_Basic.hs

Description : Parser for basic specs

Copyright : (c) Dominik Luecke, Uni Bremen 2007

License : GPLv2 or higher, see LICENSE.txt

Maintainer : luecke@informatik.uni-bremen.de

Stability : experimental

Portability : portable

Parser for abstract syntax for propositional logic

Ref.

<http://en.wikipedia.org/wiki/Propositional_logic>

-}

module Propositional.Parse_AS_Basic

( basicSpec -- Parser for basic specs

, symbItems

, symbMapItems

, impFormula

) where

import Common.AnnoState

import Common.AS_Annotation

import Common.Id

import Common.Keywords

import Common.Lexer

import Common.Token

import Common.Parsec

import Common.GlobalAnnotations (PrefixMap)

import Propositional.AS_BASIC_Propositional as AS_BASIC

import Text.ParserCombinators.Parsec

propKeywords :: [String]

propKeywords = criticalKeywords ++

[ propS

, notS

, trueS

, falseS ]

-- | Toplevel parser for basic specs

basicSpec :: PrefixMap -> AParser st AS_BASIC.BASIC_SPEC

basicSpec _ =

fmap AS_BASIC.Basic_spec (annosParser parseBasicItems)

<|> (oBraceT >> cBraceT >> return (AS_BASIC.Basic_spec []))

-- | Parser for basic items

parseBasicItems :: AParser st AS_BASIC.BASIC_ITEMS

parseBasicItems = parsePredDecl <|> parseAxItems

-- | parser for predicate declarations

parsePredDecl :: AParser st AS_BASIC.BASIC_ITEMS

parsePredDecl = fmap AS_BASIC.Pred_decl predItem

-- | parser for Axiom_items

parseAxItems :: AParser st AS_BASIC.BASIC_ITEMS

parseAxItems = do

d <- dotT

(fs, ds) <- aFormula `separatedBy` dotT

(_, an) <- optSemi

let _ = catRange (d : ds)

ns = init fs ++ [appendAnno (last fs) an]

return $ AS_BASIC.Axiom_items ns

-- | Any word to token

propId :: GenParser Char st Token

propId = pToken $ reserved propKeywords scanAnyWords

-- | parser for predicates = propositions

predItem :: AParser st AS_BASIC.PRED_ITEM

predItem = do

v <- asKey (propS ++ sS) <|>

asKey propS

(ps, cs) <- propId `separatedBy` anComma

return $ AS_BASIC.Pred_item ps $ catRange $ v : cs

-- | Parser for implies @=>@

implKey :: AParser st Token

implKey = asKey implS

-- | Parser for and @\/\ @

andKey :: AParser st Token

andKey = asKey lAnd

-- | Parser for or @\\\/@

orKey :: AParser st Token

orKey = asKey lOr

-- | Parser for true

trueKey :: AParser st Token

trueKey = asKey trueS

-- | Parser for false

falseKey :: AParser st Token

falseKey = asKey falseS

-- | Parser for not

notKey :: AParser st Token

notKey = asKey notS

-- | Parser for negation

negKey :: AParser st Token

negKey = asKey negS

-- | Parser for equivalence @<=>@

equivKey :: AParser st Token

equivKey = asKey equivS

-- | Parser for primitive formulae

primFormula :: AParser st AS_BASIC.FORMULA

primFormula =

do c <- trueKey

return (AS_BASIC.True_atom $ tokPos c)

<|>

do c <- falseKey

return (AS_BASIC.False_atom $ tokPos c)

<|>

do c <- notKey <|> negKey <?> "\"not\""

k <- primFormula

return (AS_BASIC.Negation k $ tokPos c)

<|> parenFormula

<|> fmap AS_BASIC.Predication propId

-- | Parser for formulae containing 'and' and 'or'

andOrFormula :: AParser st AS_BASIC.FORMULA

andOrFormula = do

f <- primFormula

do c <- andKey

(fs, ps) <- primFormula `separatedBy` andKey

return . AS_BASIC.Conjunction (f : fs) . catRange $ c : ps

<|> do

c <- orKey

(fs, ps) <- primFormula `separatedBy` orKey

return . AS_BASIC.Disjunction (f : fs) . catRange $ c : ps

<|> return f

-- | Parser for formulae with implications

impFormula :: AParser st AS_BASIC.FORMULA

impFormula = do

f <- andOrFormula

do c <- implKey

(fs, ps) <- andOrFormula `separatedBy` implKey

return . makeImpl (f : fs) . catPosAux $ c : ps

<|> do

c <- equivKey

g <- andOrFormula

return . AS_BASIC.Equivalence f g $ tokPos c

<|> return f

where

makeImpl [f, g] p = AS_BASIC.Implication f g (Range p)

makeImpl (f : r) (c : p) = AS_BASIC.Implication f (makeImpl r p) (Range [c])

makeImpl _ _ = error "makeImpl got illegal argument"

-- | Parser for formulae with parentheses

parenFormula :: AParser st AS_BASIC.FORMULA

parenFormula = do

oParenT << addAnnos

f <- impFormula << addAnnos

cParenT >> return f

-- | Toplevel parser for formulae

aFormula :: AParser st (Annoted AS_BASIC.FORMULA)

aFormula = allAnnoParser impFormula

-- | parsing a prop symbol

symb :: GenParser Char st SYMB

symb = fmap Symb_id propId

-- | parsing one symbol or a mapping of one to a second symbol

symbMap :: GenParser Char st SYMB_OR_MAP

symbMap = do

s <- symb

do f <- pToken $ toKey mapsTo

t <- symb

return (Symb_map s t $ tokPos f)

<|> return (Symb s)

-- | Parse a list of comma separated symbols.

symbItems :: GenParser Char st SYMB_ITEMS

symbItems = do

(is, ps) <- symbs

return (Symb_items is $ catRange ps)

-- | parse a comma separated list of symbols

symbs :: GenParser Char st ([SYMB], [Token])

symbs = do

s <- symb

do c <- commaT `followedWith` symb

(is, ps) <- symbs

return (s : is, c : ps)

<|> return ([s], [])

-- | parse a list of symbol mappings

symbMapItems :: GenParser Char st SYMB_MAP_ITEMS

symbMapItems = do

(is, ps) <- symbMaps

return (Symb_map_items is $ catRange ps)

-- | parse a comma separated list of symbol mappings

symbMaps :: GenParser Char st ([SYMB_OR_MAP], [Token])

symbMaps = do

s <- symbMap

do c <- commaT `followedWith` symb

(is, ps) <- symbMaps

return (s : is, c : ps)

<|> return ([s], [])