Parse_AS_Basic.hs

{-# OPTIONS -fallow-undecidable-instances #-}
{- |
Module      :  $Header$
Description :  Instance of class Logic for propositional logic
Copyright   :  (c) Dominik Luecke, Uni Bremen 2007
License     :  similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

Maintainer  :  luecke@tzi.de
Stability   :  experimental
Portability :  portable

Parser for abstract syntax for propositional logic

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

Acknowledgements:
I'd like to thank Christian Maeder for his help and advice. 

-}

module Propositional.Parse_AS_Basic 
    (
     basicSpec                      -- Parser for basic specs
    ) 
    where

import qualified Common.AnnoState as AnnoState
import qualified Common.AS_Annotation as Annotation
import qualified Common.Id as Id
import qualified Common.Keywords as Keywords
import Common.Lexer as Lexer
import qualified Propositional.AS_BASIC_Propositional as AS_BASIC
import qualified Common.AS_Annotation as AS_Anno
import Text.ParserCombinators.Parsec

propKeywords :: [String]
propKeywords = [
                Keywords.propS
               ,Keywords.notS
               ,Keywords.trueS
               ,Keywords.falseS
               ]

-- | Toplevel parser for basic specs
basicSpec :: AnnoState.AParser st AS_BASIC.BASIC_SPEC
basicSpec = (fmap AS_BASIC.Basic_spec $ AnnoState.annosParser $ parseBasicItems)
            <|> (Lexer.oBraceT >> Lexer.cBraceT >> return (AS_BASIC.Basic_spec []))

-- | Parser for basic items
parseBasicItems :: AnnoState.AParser st AS_BASIC.BASIC_ITEMS
parseBasicItems =
   parsePredDecl
   <|>
   parseAxItems

-- | parser for predicate declarations
parsePredDecl :: AnnoState.AParser st AS_BASIC.BASIC_ITEMS
parsePredDecl = fmap AS_BASIC.Pred_decl predItem

-- | parser for Axiom_items
parseAxItems :: AnnoState.AParser st AS_BASIC.BASIC_ITEMS
parseAxItems =
    do d <- AnnoState.dotT
       (fs, ds) <- aFormula `Lexer.separatedBy` AnnoState.dotT
       (_, an) <- AnnoState.optSemi
       let _  = Id.catPos (d:ds) 
           ns = init fs ++ [AS_Anno.appendAnno (last fs) an]
       return $ AS_BASIC.Axiom_items ns 

-- | Any word to token   
propId :: GenParser Char st Id.Token
propId = Lexer.pToken $ Lexer.reserved propKeywords Lexer.scanAnyWords 

-- | parser for predicates = propositions
predItem :: AnnoState.AParser st AS_BASIC.PRED_ITEM
predItem = 
    do 
      v <- AnnoState.asKey (Keywords.propS++Keywords.sS) <|>
           AnnoState.asKey Keywords.propS
      (ps, cs) <- propId `Lexer.separatedBy` AnnoState.anComma
      return $ AS_BASIC.Pred_item ps $ Id.catPos(v : cs)

-- | Parser for implies @=>@
implKey :: AnnoState.AParser st Id.Token
implKey = AnnoState.asKey Keywords.implS

-- | Parser for and @\/\ @
andKey :: AnnoState.AParser st Id.Token
andKey = AnnoState.asKey Keywords.lAnd

-- | Parser for or @\\\/@
orKey :: AnnoState.AParser st Id.Token
orKey = AnnoState.asKey Keywords.lOr

-- | Parser for true 
trueKey :: AnnoState.AParser st Id.Token
trueKey = AnnoState.asKey Keywords.trueS

-- | Parser for false
falseKey :: AnnoState.AParser st Id.Token
falseKey = AnnoState.asKey Keywords.falseS

-- | Parser for not
notKey :: AnnoState.AParser st Id.Token
notKey = AnnoState.asKey Keywords.notS

-- | Parser for negation
negKey :: AnnoState.AParser st Id.Token
negKey = AnnoState.asKey Keywords.negS

-- | Parser for equivalence @<=>@
equivKey ::  AnnoState.AParser st Id.Token
equivKey = AnnoState.asKey Keywords.equivS

-- | Parser for primitive formulae
primFormula :: AnnoState.AParser st AS_BASIC.FORMULA
primFormula = 
    do c <- trueKey
       return (AS_BASIC.True_atom $ Id.tokPos c)
    <|>
    do c <- falseKey
       return (AS_BASIC.False_atom $ Id.tokPos c)
    <|>
    do c <- notKey <|> negKey <?> "\"not\""
       k <- primFormula
       return (AS_BASIC.Negation k $ Id.tokPos c)
    <|> parenFormula
    <|> fmap AS_BASIC.Predication propId 

-- | Parser for formulae containing 'and' and 'or'
andOrFormula :: AnnoState.AParser st AS_BASIC.FORMULA
andOrFormula =
               do f <- primFormula 
                  do c <- andKey
                     (fs, ps) <- primFormula `Lexer.separatedBy` andKey
                     return (AS_BASIC.Conjunction (f:fs) (Id.catPos (c:ps)))
                    <|>
                    do c <- orKey
                       (fs, ps) <- primFormula `Lexer.separatedBy` orKey
                       return (AS_BASIC.Disjunction (f:fs) (Id.catPos (c:ps)))
                    <|> return f

-- | Parser for formulae with implications
impFormula :: AnnoState.AParser st AS_BASIC.FORMULA
impFormula  =
             do f <- andOrFormula 
                do c <- implKey
                   (fs, ps) <- andOrFormula `Lexer.separatedBy` implKey
                   return (makeImpl      (f:fs) (Id.catPosAux (c:ps)))
                  <|>
                  do c <- equivKey
                     g <- andOrFormula
                     return (AS_BASIC.Equivalence f g $ Id.tokPos c)
                  <|> return f
                    where makeImpl   [f,g] p = AS_BASIC.Implication f g   (Id.Range p)
                          makeImpl   (f:r) (c:p) =
                                     AS_BASIC.Implication f (makeImpl r p)   (Id.Range [c])
                          makeImpl   _ _ =
                              error "makeImpl got illegal argument"

-- | Parser for formulae with parentheses
parenFormula :: AnnoState.AParser st AS_BASIC.FORMULA
parenFormula =
    do Lexer.oParenT << AnnoState.addAnnos
       f <- impFormula << AnnoState.addAnnos
       Lexer.cParenT >> return f

-- | Toplevel parser for formulae
aFormula :: AnnoState.AParser st (AS_Anno.Annoted AS_BASIC.FORMULA)
aFormula = Lexer.bind AS_Anno.appendAnno (AnnoState.annoParser $ impFormula) AnnoState.lineAnnos