{- |
Module      :  $Header$
Description :  Parser of the Knowledge Interchange Format
Copyright   :  (c) Karl Luc, DFKI Bremen 2010, Eugen Kuksa and Uni Bremen 2011, Soeren Schulze 2012
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  s.schulze@uni-bremen.de
Stability   :  provisional
Portability :  portable
-}

module CommonLogic.Parse_KIF where

import qualified Common.AnnoState as AnnoState
import qualified Common.AS_Annotation as Annotation
import CommonLogic.AS_CommonLogic as AS
import Common.Id as Id
import Common.Keywords
import Common.Lexer (notFollowedWith)
import Common.Parsec (reserved)
import Common.Token
import Common.GlobalAnnotations (PrefixMap)

import CommonLogic.Lexer_KIF

import Text.ParserCombinators.Parsec as Parsec
import Control.Monad (liftM)

boolop_nary :: [(String, [SENTENCE] -> BOOL_SENT, String)]
boolop_nary = [(andS, Junction Conjunction, "conjunction"),
               (orS, Junction Disjunction, "disjunction")]

boolop_binary :: [(String, SENTENCE -> SENTENCE -> BOOL_SENT, String)]
boolop_binary = [(equivS, BinOp Biconditional, "equivalence"),
                 (implS, BinOp Implication, "implication")]

boolop_quant :: [(String, QUANT, String)]
boolop_quant = [(forallS, Universal, "universal quantifier"),
                (existsS, Existential, "existiantial quantifier")]

parse_keys :: [(String, op_t, String)] -> CharParser st (Token, op_t, String)
parse_keys = choice . map
             (\ (ident, con, desc) ->
               liftM (\ ch -> (ch, con, ident)) (key ident <?> desc))

logsent :: CharParser st SENTENCE
logsent = do ch <- key notS <?> "negation"
             s <- sentence <?> "sentence after \"" ++ notS ++ "\""
             return $ Bool_sent (Negation s)
               $ Range $ joinRanges [rangeSpan ch, rangeSpan s]
      <|> do (ch, con, ident) <- parse_keys boolop_nary
             s <- many sentence <?> "sentences after \"" ++ ident ++ "\""
             return $ Bool_sent (con s)
               $ Range $ joinRanges [rangeSpan ch, rangeSpan s]
      <|> do (ch, con, ident) <- parse_keys boolop_binary
             s1 <- sentence <?> "first sentence after \"" ++ ident ++ "\""
             s2 <- sentence <?> "second sentence after \"" ++ ident ++ "\""
             return $ Bool_sent (con s1 s2)
               $ Range $ joinRanges [rangeSpan ch, rangeSpan s1, rangeSpan s2]
      <|> do (ch, q, ident) <- parse_keys boolop_quant
             vars <- parens (many1 (liftM Name (pToken variable)
                                    <|> liftM SeqMark (pToken rowvar)))
                     <?> "quantified variables"
             s <- sentence <?> "sentence after \"" ++ ident ++ "\""
             return $ Quant_sent q vars s
               $ Range $ joinRanges [rangeSpan ch, rangeSpan vars, rangeSpan s]

plainAtom :: CharParser st ATOM
plainAtom = do
  t <- pToken (word <|> variable) <?> "word"
  return $ Atom (Name_term t) []

atomsent :: CharParser st ATOM -> CharParser st SENTENCE
atomsent = liftM (\ a -> Atom_sent a $ Range $ rangeSpan a)

plainsent :: CharParser st SENTENCE
plainsent = atomsent plainAtom

parensent :: CharParser st SENTENCE
parensent = parens $ logsent <|> relsent <|> eqsent

funterm :: CharParser st TERM
funterm = parens funterm
      <|> do relword <- pToken (reserved
               [equalS, neqS, andS, orS, equivS, implS, forallS, existsS, notS]
               (word <|> variable)) <?> "funword"
             let nt = Name_term relword
             t <- many (liftM Seq_marks (pToken rowvar)
                        <|> liftM Term_seq term) <?> "arguments"
             return $ if null t
               then nt
               else Funct_term nt t
                    (Range $ joinRanges [rangeSpan relword, rangeSpan t])

relsent :: CharParser st SENTENCE
relsent = do
  ft <- funterm
  let a = case ft of
        p@(Name_term _) -> Atom p []
        Funct_term p args _ -> Atom p args
        _ -> error "unknown TERM in relsent"
  atomsent $ return a

neqS :: String
neqS = "/="

eq_ops :: [(String, SENTENCE -> Id.Range -> SENTENCE, String)]
eq_ops = [(equalS, const, "equation"),
          (neqS, \ e rn -> Bool_sent (Negation e) rn, "inequality")]

eqsent :: CharParser st SENTENCE
eqsent = do
  (ch, con, ident) <- parse_keys eq_ops
  t1 <- term <?> "term after \"" ++ ident ++ "\""
  t2 <- term <?> "second term after \"" ++ ident ++ "\""
  let rn = Range $ joinRanges [rangeSpan ch, rangeSpan t1, rangeSpan t2]
  return $ con (Atom_sent (Equation t1 t2) rn) rn

term :: CharParser st TERM
term = liftM Name_term (pToken variable)
   <|> liftM Name_term (pToken word)
   <|> liftM Name_term (pToken quotedString)
   <|> liftM Name_term (pToken number)
   <|> parens (funterm <|> do
               s <- logsent <|> eqsent
               return $ That_term s $ Range $ rangeSpan s)

sentence :: CharParser st SENTENCE
sentence = parensent <|> plainsent

topLevelSentence :: CharParser st SENTENCE
topLevelSentence = notFollowedWith (return ())
                   (choice (map key terminatingKeywords))
                   >> sentence

basicSpec :: PrefixMap -> AnnoState.AParser st BASIC_SPEC
basicSpec _ = do
  many white
  sentences <- many topLevelSentence
  let phrases = map Sentence sentences
  let text = Text phrases $ Range $ joinRanges $ map rangeSpan phrases
  let text_meta = Text_meta text Nothing Nothing []
  let basic_items = Axiom_items [Annotation.emptyAnno text_meta]
  return $ Basic_spec [Annotation.emptyAnno basic_items]
