{-# 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
