{-# 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.Token
import Data.Maybe
import Text.ParserCombinators.Parsec
import Logic.Logic
import TopHybrid.AS_TopHybrid

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

-- Parses the specification after knowing 
--the underlying logic
thSpec :: AnyLogic -> AParser st Spc_Wrap
thSpec (Logic l) =
        do
        asKey "Basic_Spec"
        asKey "{"
        s <- callParser $ parse_basic_spec l
        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 :: Maybe x -> x
callParser = fromMaybe (error "Failed! No parser for this logic")

-- 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 = topParser l bs >>= return . (Frm_Wrap l) 

-- Parser of hybridization of hybridization of sentences
formParser' :: Spc_Wrap -> AParser st Frm_Wrap
formParser' (Spc_Wrap l b _) =
        topParser l (und b) >>= return . (Frm_Wrap l) 

-- 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 >>= return
        where   fp1 = (chainl1 fp2 disjP >>= return)
                fp2 = (chainl1 (fParser l bs) conjP >>= return) 

-- 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 (parse_basic_sen l) bs
        asKey "}"
        return $ UnderLogic f 
