{-# LANGUAGE RankNTypes #-}

{- |

Module : $Header$

License : GPLv2 or higher, see LICENSE.txt

Maintainer : nevrenato@gmail.com

Stability : provisional

Portability : portable

Description :

Parser for an hybridized arbitrary logic

-}

module TopHybrid.Parse_AS where

import Common.AnnoState

import Common.AS_Annotation

import Common.GlobalAnnotations (PrefixMap)

import Common.Token

import Data.Maybe

import qualified Data.Map as Map

import Text.ParserCombinators.Parsec

import Logic.Logic

import TopHybrid.AS_TopHybrid

import Control.Monad (liftM)

-- the top parser; parses an entire specification

thBasic :: (String -> AnyLogic) -> AParser st Spc_Wrap

thBasic getLogic =

do

asKey "baselogic"

logicName <- simpleId

thSpec $ getLogic $ show logicName

basicSpec :: (Syntax lid basic_spec s si sim) =>

lid -> Maybe (PrefixMap -> AParser st basic_spec)

basicSpec l = maybe (parse_basic_spec l) (Just . fst)

(parserAndPrinter Nothing l)

{- Parses the specification after knowing

the underlying logic -}

thSpec :: AnyLogic -> AParser st Spc_Wrap

thSpec (Logic l) =

do

asKey "Basic_Spec"

asKey "{"

s <- callParser l basicSpec Map.empty

asKey "}"

i <- many itemParser

fs <- sepBy (annoFormParser l s) anSemiOrComma

return $ Spc_Wrap l (Bspec i s) fs

{- Calls the underlying logic parser, only if exists. Otherwise

will throw out an error -}

callParser :: (Show a) => a -> (a -> Maybe x) -> x

callParser l f =

fromMaybe (error $ "Failed! No parser for logic " ++ show l) $ f l

-- Parses the declaration of nominals and modalities

itemParser :: AParser st TH_BASIC_ITEM

itemParser =

do

asKey "modalities"

ms <- ids

return $ Simple_mod_decl ms

<|>

do

asKey "nominals"

ns <- ids

return $ Simple_nom_decl ns

where ids = sepBy simpleId anSemiOrComma

-- Formula parser with annotations

annoFormParser :: (Logic l sub bs f s sm si mo sy rw pf) =>

l -> bs -> AParser st (Annoted Frm_Wrap)

annoFormParser l b = allAnnoParser $ formParser l b

-- Just parses the formula, and wraps it in Frm_Wrap

formParser :: (Logic l sub bs f s sm si mo sy rw pf) =>

l -> bs -> AParser st Frm_Wrap

formParser l bs = liftM (Frm_Wrap l) $ topParser l bs

-- Parser of hybridization of hybridization of sentences

formParser' :: Spc_Wrap -> AParser st Frm_Wrap

formParser' (Spc_Wrap l b _) = liftM (Frm_Wrap l) $ topParser l (und b)

{- Parser of sentences

The precendence order is left associative and when the priority

is defined is as follows : () > (not,@,[],<>) > /\ > \/ > (->,<->) -}

topParser :: (Logic l sub bs f s sm si mo sy rw pf) =>

l -> bs -> AParser st (TH_FORMULA f)

topParser l bs = chainl1 fp1 impAndBiP

where fp1 = chainl1 fp2 disjP

fp2 = chainl1 (fParser l bs) conjP

{- BinaryOps parsers, the reason to separate them, is that so we can get a

precedence order -}

conjP :: AParser st (TH_FORMULA f -> TH_FORMULA f -> TH_FORMULA f)

conjP = asKey "/\\" >> return Conjunction

disjP :: AParser st (TH_FORMULA f -> TH_FORMULA f -> TH_FORMULA f)

disjP = asKey "\\/" >> return Disjunction

impAndBiP :: AParser st (TH_FORMULA f -> TH_FORMULA f -> TH_FORMULA f)

impAndBiP = (asKey "=>" >> return Implication) <|>

(asKey "<=>" >> return BiImplication)

-- ------------

-- Parser of sentences without the binary operators

fParser :: (Logic l sub bs f s sm si mo sy rw pf) =>

l -> bs -> AParser st (TH_FORMULA f)

fParser l bs =

do

asKey "("

f <- topParser l bs

asKey ")"

return $ Par f

<|>

do

asKey "not"

f <- fParser l bs <|> topParser l bs

return $ Neg f

<|>

do

asKey "@"

n <- simpleId

f <- fParser l bs <|> topParser l bs

return $ At n f

<|>

do

asKey "!"

n <- simpleId

f <- fParser l bs

return $ Uni n f

<|>

do

asKey "?"

n <- simpleId

f <- fParser l bs

return $ Exist n f

<|>

do

asKey "["

m <- simpleId

asKey "]"

f <- fParser l bs <|> topParser l bs

return $ Box m f

<|>

try (do

asKey "<"

m <- simpleId

asKey ">\""

f <- fParser l bs <|> topParser l bs

return $ Par $ Conjunction (Dia m f) (Box m f))

<|>

do

asKey "<"

m <- simpleId

asKey ">"

f <- fParser l bs <|> topParser l bs

return $ Dia m f

<|>

do

asKey "true"

return TrueA

<|>

do

asKey "false"

return FalseA

<|>

do

n <- simpleId

return $ Here n

<|>

do

asKey "{"

f <- callParser l parse_basic_sen bs

asKey "}"

return $ UnderLogic f