{- |

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]