Parse_CLIF.hs revision eea1dfbc731d45f624bc3c14bada0617ebaa6eaa
{- |
Module : $Header$
Description : Parser of common logic interchange format
Copyright : (c) Karl Luc, DFKI Bremen 2010, Eugen Kuksa and Uni Bremen 2011
License : GPLv2 or higher, see LICENSE.txt
Maintainer : eugenk@informatik.uni-bremen.de
Stability : provisional
Portability : portable
Parser of common logic interchange format
-}
{-
Ref. Common Logic ISO/IEC IS 24707:2007(E)
-}
module CommonLogic.Parse_CLIF 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.IRI
import Common.Lexer as Lexer hiding (oParenT, cParenT, pToken)
import Common.Keywords (colonS)
import Data.Either (lefts, rights)
import qualified Data.Set as Set
import qualified CommonLogic.Tools as Tools
import CommonLogic.Lexer_CLIF
import CommonLogic.Parse_Symbols (intNameOrSeqMark)
import Text.ParserCombinators.Parsec as Parsec
-- | parser for getText
cltext :: CharParser st TEXT_META
cltext = many white >> (do
try $ oParenT >> clTextKey
(nt, prfxs) <- namedtext
cParenT
return $ tm nt prfxs
<|> do
(t, prfxs) <- text <?> "text"
return $ tm t prfxs
)
where tm :: TEXT -> [PrefixMapping] -> TEXT_META
tm t prfxs = emptyTextMeta { AS.getText = t
, prefix_map = prfxs
}
namedtext :: CharParser st (TEXT, [PrefixMapping])
namedtext = do
n <- identifier <?> "name after \"cl-text\""
(t, prfxs) <- text
return (Named_text n t nullRange, prfxs)
<|> do
n <- identifier <?> "name after \"cl-text\""
return (Named_text n (Text [] nullRange) nullRange, [])
text :: CharParser st (TEXT, [PrefixMapping])
text = do
phrPrfxs <- many1 phrase
let (phr, prfxs) = unzip phrPrfxs
return (Text (concat phr) nullRange, concat prfxs)
-- remove the try
-- keys set here to prevent try in more complex parser to get the right
-- error message in ex. the following text
phrase :: CharParser st ([PHRASE], [PrefixMapping])
phrase = many white >> (do
try (oParenT >> clModuleKey)
(m, prfxs) <- pModule
cParenT
return ([Module m], prfxs)
<|> do
try (oParenT >> clImportsKey)
i <- importation
cParenT
return ([Importation i], [])
<|> do
try (oParenT >> clCommentKey)
c <- quotedstring <?> "comment after \"cl-comment\""
(t, prfxs) <- comment_txt <?> "text after \"cl-comment <comment>\""
cParenT
return ([Comment_text (Comment c nullRange) t nullRange], prfxs)
<|> do
try (oParenT >> clPrefixKey)
pm <- prefix
cParenT
return ([], pm)
<|> do
s <- sentence <?> "sentence"
return ([Sentence s], [])
)
prefix :: CharParser st [PrefixMapping]
prefix = do
p <- (do
string colonS
return colonS
<|> do
x <- ncname
string colonS
return $ x ++ colonS
)
many white
i <- iriCurie
return [(p, i)]
comment_txt :: CharParser st (TEXT, [PrefixMapping])
comment_txt = try text <|> return (Text [] nullRange, [])
-- | parser for module
pModule :: CharParser st (MODULE, [PrefixMapping])
pModule = do
t <- identifier <?> "module name after \"cl-module\""
(exs,(txt, prfxs)) <- pModExcl <?> "text in module"
case exs of
[] -> return (Mod t txt nullRange, prfxs)
_ -> return (Mod_ex t exs txt nullRange, prfxs)
-- | parser for
pModExcl :: CharParser st ([NAME], (TEXT, [PrefixMapping]))
pModExcl = many white >> (do
try (oParenT >> clExcludesKey)
exs <- many identifier <?> "only names in module-exclusion list"
cParenT
tp <- text
return (exs, tp)
<|> do
tp <- text
return ([], tp)
)
importation :: CharParser st IMPORTATION
importation = do
-- clImportsKey
n <- identifier <?> "importation name after \"cl-imports\""
return $ Imp_name n
-- | parser for sentences
sentence :: CharParser st SENTENCE
sentence = parens (do
ck <- try clCommentKey
c <- quotedstring <?> "comment after \"cl-comment\""
s <- sentence <?> "sentence after \"cl-comment <comment>\""
return $ Comment_sent (Comment c $ Range $ rangeSpan c) s
$ Range $ joinRanges [rangeSpan ck, rangeSpan c, rangeSpan s]
<|> do
t0 <- try rolesetTerm
nts <- many rolesetNT
cParenT
return $ rolesetSentence t0 nts
<|> do
at <- atom
return $ Atom_sent at $ Range $ rangeSpan at
<|> do
c <- andKey
s <- many sentence -- joinRanges with s = []?
return $ Bool_sent (Conjunction s) $ Range $ joinRanges [rangeSpan c,
rangeSpan s]
<|> do
c <- orKey
s <- many sentence
return $ Bool_sent (Disjunction s) $ Range $ joinRanges [rangeSpan c,
rangeSpan s]
<|> do
c <- notKey
s <- sentence <?> "sentence after \"not\""
return $ Bool_sent (Negation s) $ Range $ joinRanges [rangeSpan c,
rangeSpan s]
<|> do
c <- try iffKey
s1 <- sentence <?> "sentence after \"iff\""
s2 <- sentence <?> "second sentence after \"iff\""
return $ Bool_sent (Biconditional s1 s2) $ Range $ joinRanges [rangeSpan c,
rangeSpan s1, rangeSpan s1]
<|> do
c <- ifKey
s1 <- sentence <?> "sentence after \"if\""
s2 <- sentence <?> "second sentence after \"if\""
return $ Bool_sent (Implication s1 s2) $ Range $ joinRanges [rangeSpan c,
rangeSpan s1, rangeSpan s1]
<|> do
c <- forallKey
quantsent1 True c
<|> do
c <- existsKey
quantsent1 False c
)
quantsent1 :: Bool -> Token -> CharParser st SENTENCE
quantsent1 t c = do
g <- identifier <?> "predicate after quantifier"
quantsent2 t c $ Just g -- Quant_sent using syntactic sugar
<|>
quantsent2 t c Nothing -- normal Quant_sent
quantsent2 :: Bool -> Token -> Maybe NAME -> CharParser st SENTENCE
quantsent2 t c mg = do
bl <- parens boundlist
s <- sentence
return $ quantsent3 t mg (rights bl) (lefts bl) s
$ Range $ joinRanges [rangeSpan c, rangeSpan s]
quantsent3 :: Bool -> Maybe NAME -> [NAME_OR_SEQMARK]
-> [(NAME_OR_SEQMARK, TERM)] -> SENTENCE -> Range -> SENTENCE
quantsent3 t mg bs ((n,trm):nts) s rn = -- Quant_sent using syntactic sugar
let functerm = case n of
Name nm -> Atom (Funct_term trm [Term_seq $ Name_term nm] nullRange) []
SeqMark sqm -> Atom (Funct_term trm [Seq_marks sqm] nullRange) []
in if t
then Quant_sent (Universal [n] $ quantsent3 t mg bs nts (
Bool_sent (Implication (Atom_sent functerm rn) s) rn
) rn) rn
else Quant_sent (Universal [n] $ quantsent3 t mg bs nts (
Bool_sent (Conjunction [Atom_sent functerm rn, s]) rn
) rn) rn
quantsent3 t mg bs [] s rn =
let quantType = if t then Universal else Existential
in case mg of
Nothing -> Quant_sent (quantType bs s) rn -- normal Quant_sent
Just g -> -- Quant_sent using syntactic sugar
let functerm = Atom (Funct_term (Name_term g) (map (Term_seq . Name_term)
$ Set.elems $ Tools.indvC_sen s) nullRange) []
in if t
then Quant_sent (Universal bs (Bool_sent (Implication
(Atom_sent functerm nullRange) s) rn)) rn
else
Quant_sent (Existential bs (Bool_sent (Conjunction
[Atom_sent functerm nullRange, s]) rn)) rn
boundlist :: CharParser st [Either (NAME_OR_SEQMARK, TERM) NAME_OR_SEQMARK]
boundlist = many (do
nos <- intNameOrSeqMark
return $ Right nos
<|> parens (do
nos <- intNameOrSeqMark
t <- term
return $ Left (nos,t)
)
)
atom :: CharParser st ATOM
atom = do
clEqualsKey
t1 <- term <?> "term after \"=\""
t2 <- term <?> "second term after \"=\""
return $ Equation t1 t2
<|> do
t <- term <?> "term"
ts <- many termseq
return $ Atom t ts
term :: CharParser st TERM
term = do
t <- identifier
return $ Name_term t
<|> term_fun_cmt
term_fun_cmt :: CharParser st TERM
term_fun_cmt = parens (do
ck <- try clCommentKey
c <- quotedstring <?> "comment after \"cl-comment\""
t <- term <?> "term after \"cl-comment <comment>\""
return $ Comment_term t (Comment c $ Range $ rangeSpan c)
$ Range $ joinRanges [rangeSpan ck, rangeSpan c, rangeSpan t]
<|> do
t <- term
ts <- many1 termseq -- many1? yes, because it's a functional term
return $ Funct_term t ts $ Range $ joinRanges [rangeSpan t, rangeSpan ts]
)
termseq :: CharParser st TERM_SEQ
termseq = do
x <- seqmark
return $ Seq_marks x
<|> do
t <- term
return $ Term_seq t
<?> "term or sequence marker in term sequence"
rolesetTerm :: CharParser st TERM
rolesetTerm = do
t0 <- term
oParenT
clRolesetKey
return t0
rolesetNT :: CharParser st (NAME, TERM)
rolesetNT = parens $ do
n <- identifier
t <- term <?> "term"
return (n,t)
rolesetSentence :: TERM -> [(NAME, TERM)] -> SENTENCE
rolesetSentence t0 nts =
let x = rolesetFreeName t0 nts
in Quant_sent (Existential [Name x] (Bool_sent (Conjunction $
rolesetAddToTerm x t0 : map (rolesetMixTerm x) nts
) nullRange)) $ Range $ rangeSpan t0
rolesetFreeName :: TERM -> [(NAME, TERM)] -> NAME
rolesetFreeName trm nts =
let usedNames = Set.union (Tools.setUnion_list
nts) (Tools.indvC_term trm)
in fst $ Tools.freeName ("x", 0) usedNames
rolesetAddToTerm :: NAME -> TERM -> SENTENCE
rolesetAddToTerm x trm = Atom_sent (Atom trm [Term_seq $ Name_term x]) nullRange
rolesetMixTerm :: NAME -> (NAME, TERM) -> SENTENCE
rolesetMixTerm x (n, t) =
Atom_sent (Atom (Name_term n) [Term_seq $ Name_term x, Term_seq t]) nullRange
-- | Toplevel parser for basic specs
basicSpec :: AnnoState.AParser st BASIC_SPEC
basicSpec = do
bi <- parseAxItems
return bi
<|> do
bi <- AnnoState.allAnnoParser parseBasicItems
return $ Basic_spec [bi]
-- function to parse different syntaxes
-- parsing: axiom items with dots, clif sentences, clif text
-- first getting only the sentences
parseBasicItems :: AnnoState.AParser st BASIC_ITEMS
parseBasicItems = try parseSentences
<|> parseClText
-- parseClText
parseSentences :: AnnoState.AParser st BASIC_ITEMS
parseSentences = do
xs <- many1 aFormula
return $ Axiom_items xs
-- FIX
parseClText :: AnnoState.AParser st BASIC_ITEMS
parseClText = do
tx <- cltext
return $ Axiom_items (textToAn [tx])
textToAn :: [TEXT_META] -> [Annotation.Annoted TEXT_META]
textToAn = map (\x -> Annotation.Annoted x nullRange [] [])
-- | parser for Axiom_items
parseAxItems :: AnnoState.AParser st BASIC_SPEC
parseAxItems = do
d <- AnnoState.dotT
(_, an) <- AnnoState.optSemi
let _ = Id.catRange (d : ds)
ns = init fs ++ [Annotation.appendAnno (last fs) an]
return $ Basic_spec ns
-- | Toplevel parser for formulae
parseAx :: AnnoState.AParser st BASIC_ITEMS
parseAx = do
t <- many aFormula
return $ Axiom_items t
-- | Toplevel parser for formulae
aFormula :: AnnoState.AParser st (Annotation.Annoted TEXT_META)
aFormula = AnnoState.allAnnoParser cltext