{- |
Module : ./CommonLogic/Parse_KIF.hs
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]