hets/QBF/Parse_AS_Basic.hs

	Parse_AS_Basic.hs revision c56a356d3fcc5e123efa790aab320781d94df3c7
64b763950bf11e9357facbd2b5666631a895c085Trond Norbye{- |
64b763950bf11e9357facbd2b5666631a895c085Trond NorbyeModule      :  $Header$
64b763950bf11e9357facbd2b5666631a895c085Trond NorbyeDescription :  Parser for basic specs
64b763950bf11e9357facbd2b5666631a895c085Trond NorbyeCopyright   :  (c) Jonathan von Schroeder, DFKI GmbH 2010
64b763950bf11e9357facbd2b5666631a895c085Trond NorbyeLicense     :  similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
64b763950bf11e9357facbd2b5666631a895c085Trond Norbye
64b763950bf11e9357facbd2b5666631a895c085Trond NorbyeMaintainer  :  <jonathan.von_schroeder@dfki.de>
64b763950bf11e9357facbd2b5666631a895c085Trond NorbyeStability   :  experimental
64b763950bf11e9357facbd2b5666631a895c085Trond NorbyePortability :  portable
64b763950bf11e9357facbd2b5666631a895c085Trond Norbye
64b763950bf11e9357facbd2b5666631a895c085Trond NorbyeParser for abstract syntax for propositional logic
64b763950bf11e9357facbd2b5666631a895c085Trond Norbye
64b763950bf11e9357facbd2b5666631a895c085Trond Norbye  Ref.
64b763950bf11e9357facbd2b5666631a895c085Trond Norbye  <http://en.wikipedia.org/wiki/Propositional_logic>
64b763950bf11e9357facbd2b5666631a895c085Trond Norbye-}
64b763950bf11e9357facbd2b5666631a895c085Trond Norbye
64b763950bf11e9357facbd2b5666631a895c085Trond Norbyemodule QBF.Parse_AS_Basic
64b763950bf11e9357facbd2b5666631a895c085Trond Norbye  ( basicSpec                      -- Parser for basic specs
64b763950bf11e9357facbd2b5666631a895c085Trond Norbye  , symbItems
64b763950bf11e9357facbd2b5666631a895c085Trond Norbye  , symbMapItems
64b763950bf11e9357facbd2b5666631a895c085Trond Norbye  ) where
64b763950bf11e9357facbd2b5666631a895c085Trond Norbye
64b763950bf11e9357facbd2b5666631a895c085Trond Norbyeimport qualified Common.AnnoState as AnnoState
64b763950bf11e9357facbd2b5666631a895c085Trond Norbyeimport qualified Common.AS_Annotation as Annotation
c0550b01024b910b8c1468811c0ea663b10b1372Trond Norbyeimport Common.Id as Id
64b763950bf11e9357facbd2b5666631a895c085Trond Norbyeimport Common.Keywords as Keywords
64b763950bf11e9357facbd2b5666631a895c085Trond Norbyeimport Common.Lexer as Lexer
64b763950bf11e9357facbd2b5666631a895c085Trond Norbyeimport Common.Parsec
64b763950bf11e9357facbd2b5666631a895c085Trond Norbye
64b763950bf11e9357facbd2b5666631a895c085Trond Norbyeimport QBF.AS_BASIC_QBF as AS_BASIC
64b763950bf11e9357facbd2b5666631a895c085Trond Norbyeimport Text.ParserCombinators.Parsec
64b763950bf11e9357facbd2b5666631a895c085Trond Norbye
64b763950bf11e9357facbd2b5666631a895c085Trond NorbyepropKeywords :: [String]
64b763950bf11e9357facbd2b5666631a895c085Trond NorbyepropKeywords =
64b763950bf11e9357facbd2b5666631a895c085Trond Norbye  [ Keywords.propS
64b763950bf11e9357facbd2b5666631a895c085Trond Norbye  , Keywords.notS
64b763950bf11e9357facbd2b5666631a895c085Trond Norbye  , Keywords.trueS
64b763950bf11e9357facbd2b5666631a895c085Trond Norbye  , Keywords.falseS
64b763950bf11e9357facbd2b5666631a895c085Trond Norbye  , Keywords.forallS
64b763950bf11e9357facbd2b5666631a895c085Trond Norbye  , Keywords.existsS ]
64b763950bf11e9357facbd2b5666631a895c085Trond Norbye
64b763950bf11e9357facbd2b5666631a895c085Trond Norbye-- | Toplevel parser for basic specs
64b763950bf11e9357facbd2b5666631a895c085Trond NorbyebasicSpec :: AnnoState.AParser st AS_BASIC.BASICSPEC
64b763950bf11e9357facbd2b5666631a895c085Trond NorbyebasicSpec =
64b763950bf11e9357facbd2b5666631a895c085Trond Norbye  fmap AS_BASIC.BasicSpec (AnnoState.annosParser parseBasicItems)
64b763950bf11e9357facbd2b5666631a895c085Trond Norbye  <|> (Lexer.oBraceT >> Lexer.cBraceT >> return (AS_BASIC.BasicSpec []))
64b763950bf11e9357facbd2b5666631a895c085Trond Norbye
64b763950bf11e9357facbd2b5666631a895c085Trond Norbye-- | Parser for basic items
64b763950bf11e9357facbd2b5666631a895c085Trond NorbyeparseBasicItems :: AnnoState.AParser st AS_BASIC.BASICITEMS
64b763950bf11e9357facbd2b5666631a895c085Trond NorbyeparseBasicItems = parsePredDecl <|> parseAxItems
64b763950bf11e9357facbd2b5666631a895c085Trond Norbye
64b763950bf11e9357facbd2b5666631a895c085Trond Norbye-- | parser for predicate declarations
64b763950bf11e9357facbd2b5666631a895c085Trond NorbyeparsePredDecl :: AnnoState.AParser st AS_BASIC.BASICITEMS
64b763950bf11e9357facbd2b5666631a895c085Trond NorbyeparsePredDecl = fmap AS_BASIC.PredDecl predItem
64b763950bf11e9357facbd2b5666631a895c085Trond Norbye
64b763950bf11e9357facbd2b5666631a895c085Trond Norbye-- | parser for AxiomItems
64b763950bf11e9357facbd2b5666631a895c085Trond NorbyeparseAxItems :: AnnoState.AParser st AS_BASIC.BASICITEMS
64b763950bf11e9357facbd2b5666631a895c085Trond NorbyeparseAxItems = do
64b763950bf11e9357facbd2b5666631a895c085Trond Norbye       d <- AnnoState.dotT
64b763950bf11e9357facbd2b5666631a895c085Trond Norbye       (fs, ds) <- aFormula `Lexer.separatedBy` AnnoState.dotT
64b763950bf11e9357facbd2b5666631a895c085Trond Norbye       (_, an) <- AnnoState.optSemi
64b763950bf11e9357facbd2b5666631a895c085Trond Norbye       let _ = Id.catRange (d : ds)
64b763950bf11e9357facbd2b5666631a895c085Trond Norbye           ns = init fs ++ [Annotation.appendAnno (last fs) an]
64b763950bf11e9357facbd2b5666631a895c085Trond Norbye       return $ AS_BASIC.AxiomItems ns
64b763950bf11e9357facbd2b5666631a895c085Trond Norbye
64b763950bf11e9357facbd2b5666631a895c085Trond Norbye-- | Any word to token
64b763950bf11e9357facbd2b5666631a895c085Trond NorbyepropId :: GenParser Char st Id.Token
64b763950bf11e9357facbd2b5666631a895c085Trond NorbyepropId = Lexer.pToken $ reserved propKeywords Lexer.scanAnyWords
64b763950bf11e9357facbd2b5666631a895c085Trond Norbye
64b763950bf11e9357facbd2b5666631a895c085Trond Norbye-- | parser for predicates = propositions
64b763950bf11e9357facbd2b5666631a895c085Trond NorbyepredItem :: AnnoState.AParser st AS_BASIC.PREDITEM
64b763950bf11e9357facbd2b5666631a895c085Trond NorbyepredItem = do
64b763950bf11e9357facbd2b5666631a895c085Trond Norbye      v <- AnnoState.asKey (Keywords.propS ++ Keywords.sS) <|>
64b763950bf11e9357facbd2b5666631a895c085Trond Norbye           AnnoState.asKey Keywords.propS
64b763950bf11e9357facbd2b5666631a895c085Trond Norbye      (ps, cs) <- propId `Lexer.separatedBy` AnnoState.anComma
64b763950bf11e9357facbd2b5666631a895c085Trond Norbye      return $ AS_BASIC.PredItem ps $ Id.catRange $ v : cs
64b763950bf11e9357facbd2b5666631a895c085Trond Norbye
64b763950bf11e9357facbd2b5666631a895c085Trond Norbye-- | Parser for implies @=>@
64b763950bf11e9357facbd2b5666631a895c085Trond NorbyeimplKey :: AnnoState.AParser st Id.Token
64b763950bf11e9357facbd2b5666631a895c085Trond NorbyeimplKey = AnnoState.asKey Keywords.implS
64b763950bf11e9357facbd2b5666631a895c085Trond Norbye
64b763950bf11e9357facbd2b5666631a895c085Trond Norbye-- | Parser for and @\/\ @
64b763950bf11e9357facbd2b5666631a895c085Trond NorbyeandKey :: AnnoState.AParser st Id.Token
64b763950bf11e9357facbd2b5666631a895c085Trond NorbyeandKey = AnnoState.asKey Keywords.lAnd
64b763950bf11e9357facbd2b5666631a895c085Trond Norbye
64b763950bf11e9357facbd2b5666631a895c085Trond Norbye-- | Parser for or @\\\/@
64b763950bf11e9357facbd2b5666631a895c085Trond NorbyeorKey :: AnnoState.AParser st Id.Token
64b763950bf11e9357facbd2b5666631a895c085Trond NorbyeorKey = AnnoState.asKey Keywords.lOr
64b763950bf11e9357facbd2b5666631a895c085Trond Norbye
64b763950bf11e9357facbd2b5666631a895c085Trond Norbye-- | Parser for true
64b763950bf11e9357facbd2b5666631a895c085Trond NorbyetrueKey :: AnnoState.AParser st Id.Token
64b763950bf11e9357facbd2b5666631a895c085Trond NorbyetrueKey = AnnoState.asKey Keywords.trueS
64b763950bf11e9357facbd2b5666631a895c085Trond Norbye
64b763950bf11e9357facbd2b5666631a895c085Trond Norbye-- | Parser for false
64b763950bf11e9357facbd2b5666631a895c085Trond NorbyefalseKey :: AnnoState.AParser st Id.Token
64b763950bf11e9357facbd2b5666631a895c085Trond NorbyefalseKey = AnnoState.asKey Keywords.falseS
64b763950bf11e9357facbd2b5666631a895c085Trond Norbye
64b763950bf11e9357facbd2b5666631a895c085Trond Norbye-- | Parser for not
64b763950bf11e9357facbd2b5666631a895c085Trond NorbyenotKey :: AnnoState.AParser st Id.Token
64b763950bf11e9357facbd2b5666631a895c085Trond NorbyenotKey = AnnoState.asKey Keywords.notS
64b763950bf11e9357facbd2b5666631a895c085Trond Norbye
64b763950bf11e9357facbd2b5666631a895c085Trond Norbye-- | Parser for negation
64b763950bf11e9357facbd2b5666631a895c085Trond NorbyenegKey :: AnnoState.AParser st Id.Token
64b763950bf11e9357facbd2b5666631a895c085Trond NorbyenegKey = AnnoState.asKey Keywords.negS
75640e2b0da81c240758d747e76d30acd1ed194dKnut Anders Hatlen
64b763950bf11e9357facbd2b5666631a895c085Trond Norbye-- | Parser for equivalence @<=>@
64b763950bf11e9357facbd2b5666631a895c085Trond NorbyeequivKey :: AnnoState.AParser st Id.Token
64b763950bf11e9357facbd2b5666631a895c085Trond NorbyeequivKey = AnnoState.asKey Keywords.equivS
64b763950bf11e9357facbd2b5666631a895c085Trond Norbye
64b763950bf11e9357facbd2b5666631a895c085Trond Norbye-- | Parser for quantifier forall
64b763950bf11e9357facbd2b5666631a895c085Trond NorbyeforallKey :: AnnoState.AParser st Id.Token
64b763950bf11e9357facbd2b5666631a895c085Trond NorbyeforallKey = AnnoState.asKey Keywords.forallS
64b763950bf11e9357facbd2b5666631a895c085Trond Norbye
64b763950bf11e9357facbd2b5666631a895c085Trond Norbye-- | Parser for quantifier forall
64b763950bf11e9357facbd2b5666631a895c085Trond NorbyeexistsKey :: AnnoState.AParser st Id.Token
64b763950bf11e9357facbd2b5666631a895c085Trond NorbyeexistsKey = AnnoState.asKey Keywords.existsS
64b763950bf11e9357facbd2b5666631a895c085Trond Norbye
64b763950bf11e9357facbd2b5666631a895c085Trond Norbye-- | Parser for primitive formulae
64b763950bf11e9357facbd2b5666631a895c085Trond NorbyeprimFormula :: AnnoState.AParser st AS_BASIC.FORMULA
c0550b01024b910b8c1468811c0ea663b10b1372Trond NorbyeprimFormula =
c0550b01024b910b8c1468811c0ea663b10b1372Trond Norbye    do c <- trueKey
c0550b01024b910b8c1468811c0ea663b10b1372Trond Norbye       return (AS_BASIC.TrueAtom $ Id.tokPos c)
c0550b01024b910b8c1468811c0ea663b10b1372Trond Norbye    <|>
c0550b01024b910b8c1468811c0ea663b10b1372Trond Norbye    do c <- falseKey
9794eb72d2b2da2812cdba67562851047cce4600Trond Norbye       return (AS_BASIC.FalseAtom $ Id.tokPos c)
c0550b01024b910b8c1468811c0ea663b10b1372Trond Norbye    <|>
c0550b01024b910b8c1468811c0ea663b10b1372Trond Norbye    do c <- notKey <|> negKey <?> "\"not\""
64b763950bf11e9357facbd2b5666631a895c085Trond Norbye       k <- primFormula
       return (AS_BASIC.Negation k $ Id.tokPos c)
    <|> parenFormula
    <|>
        do c <- forallKey
           (l, ps) <- propId `Lexer.separatedBy` AnnoState.anComma
           f <- impFormula
           return (if length l < 1 then error "nothing quantified"
                   else AS_BASIC.ForAll l f (Id.tokPos c))
        <|>
        do c <- existsKey
           (l, ps) <- propId `Lexer.separatedBy` AnnoState.anComma
           f <- impFormula
           return $ if length l < 1 then error "nothing quantified"
                    else AS_BASIC.Exists l f (Id.tokPos c)
    <|> 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.catRange (c : ps)))
                    <|>
                    do c <- orKey
                       (fs, ps) <- primFormula `Lexer.separatedBy` orKey
                       return (AS_BASIC.Disjunction (f : fs)
                                          (Id.catRange (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 (Annotation.Annoted AS_BASIC.FORMULA)
aFormula = AnnoState.allAnnoParser impFormula

-- | parsing a prop symbol
symb :: GenParser Char st SYMB
symb = fmap SymbId propId

-- | parsing one symbol or a mapping of one to a second symbol
symbMap :: GenParser Char st SYMBORMAP
symbMap = do
  s <- symb
  do f <- pToken $ toKey mapsTo
     t <- symb
     return (SymbMap s t $ tokPos f)
    <|> return (Symb s)

-- | Parse a list of comma separated symbols.
symbItems :: GenParser Char st SYMBITEMS
symbItems = do
  (is, ps) <- symbs
  return (SymbItems 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 SYMBMAPITEMS
symbMapItems = do
  (is, ps) <- symbMaps
  return (SymbMapItems is $ catRange ps)

-- | parse a comma separated list of symbol mappings
symbMaps :: GenParser Char st ([SYMBORMAP], [Token])
symbMaps = do
  s <- symbMap
  do c <- commaT `followedWith` symb
     (is, ps) <- symbMaps
     return (s : is, c : ps)
    <|> return ([s], [])