{- |

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, mapsTo)

import Common.GlobalAnnotations (PrefixMap)

import Data.Either (lefts, rights)

import qualified Data.Set as Set

import qualified Data.Map as Map

import qualified CommonLogic.Tools as Tools

import CommonLogic.Lexer_CLIF

import Text.ParserCombinators.Parsec as Parsec

import Control.Monad (liftM)

-- | parser for getText

cltext :: PrefixMap -> CharParser st TEXT_META

cltext pm = 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 ++ Map.toList pm

}

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 <|> enclosedname) <?> "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 <|> enclosedname) <?> "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 (Junction Conjunction s)

$ Range $ joinRanges [rangeSpan c, rangeSpan s]

<|> do

c <- orKey

s <- many sentence

return $ Bool_sent (Junction 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 (BinOp 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 (BinOp 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 (BinOp Implication (Atom_sent functerm rn) s) rn

) rn) rn

else Quant_sent Universal [n] (quantsent3 t mg bs nts (

Bool_sent (Junction 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 (BinOp Implication

(Atom_sent functerm nullRange) s) rn) rn

else

Quant_sent Existential bs (Bool_sent (Junction 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 <|> enclosedname) <?> "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

c <- try thatKey

s <- sentence

return $ That_term s $ Range $ joinRanges [rangeSpan c, rangeSpan s]

<|> do

t <- liftM Name_term $ pToken quotedstring

return $ Funct_term t [] $ Range $ 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 (Junction 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

(\(n,t) -> Set.union (Tools.indvC_term t) (Set.singleton n))

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

intNameOrSeqMark :: CharParser st NAME_OR_SEQMARK

intNameOrSeqMark = do

s <- seqmark -- fix seqmark parser for one

return $ SeqMark s

<|> do

n <- identifier

return $ Name n

-- | Parse a list of comma separated symbols.

symbItems :: GenParser Char st SYMB_ITEMS

symbItems = do

(is, ps) <- symbs

return (Symb_items is $ catRange ps)

-- | parse a comma separated list of symbols

symbs :: GenParser Char st ([NAME_OR_SEQMARK], [Token])

symbs = do

s <- intNameOrSeqMark

do c <- commaT `followedWith` intNameOrSeqMark

(is, ps) <- symbs

return (s:is, c:ps)

<|> return ([s], [])

-- | parse a list of symbol mappings

symbMapItems :: GenParser Char st SYMB_MAP_ITEMS

symbMapItems = do

(is, ps) <- symbMaps

return (Symb_map_items is $ catRange ps)

-- | parse a comma separated list of symbol mappings

symbMaps :: GenParser Char st ([SYMB_OR_MAP], [Token])

symbMaps = do

s <- symbMap

many white

do c <- commaT `followedWith` intNameOrSeqMark

(is, ps) <- symbMaps

return (s:is, c:ps)

<|> return ([s], [])

-- | parsing one symbol or a mapping of one to a second symbol

symbMap :: GenParser Char st SYMB_OR_MAP

symbMap = symbMapS <|> symbMapN

symbMapS :: GenParser Char st SYMB_OR_MAP

symbMapS = do

s <- seqmark

do f <- pToken $ toKey mapsTo

t <- seqmark

return (Symb_mapS s t $ tokPos f)

<|> return (Symb $ SeqMark s)

symbMapN :: GenParser Char st SYMB_OR_MAP

symbMapN = do

s <- identifier

do f <- pToken $ toKey mapsTo

t <- identifier

return (Symb_mapN s t $ tokPos f)

<|> return (Symb $ Name s)

-- | Toplevel parser for basic specs

basicSpec :: PrefixMap -> AnnoState.AParser st BASIC_SPEC

basicSpec pm = parseAxItems pm

<|> do

bi <- AnnoState.allAnnoParser $ parseBasicItems pm

return $ Basic_spec [bi]

-- function to parse different syntaxes

-- parsing: axiom items with dots, clif sentences, clif text

-- first getting only the sentences

parseBasicItems :: PrefixMap -> AnnoState.AParser st BASIC_ITEMS

parseBasicItems pm = try (parseSentences pm)

<|> parseClText pm

-- parseClText

parseSentences :: PrefixMap -> AnnoState.AParser st BASIC_ITEMS

parseSentences pm = do

xs <- many1 $ aFormula pm

return $ Axiom_items xs

-- FIX

parseClText :: PrefixMap -> AnnoState.AParser st BASIC_ITEMS

parseClText pm = do

tx <- cltext pm

return $ Axiom_items (textToAn [tx])

textToAn :: [TEXT_META] -> [Annotation.Annoted TEXT_META]

textToAn = map (\x -> Annotation.Annoted x nullRange [] [])

-- | parser for Axiom_items

parseAxItems :: PrefixMap -> AnnoState.AParser st BASIC_SPEC

parseAxItems pm = do

d <- AnnoState.dotT

(fs, ds) <- AnnoState.allAnnoParser (parseAx pm) `Lexer.separatedBy` 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 :: PrefixMap -> AnnoState.AParser st BASIC_ITEMS

parseAx pm = do

t <- many $ aFormula pm

return $ Axiom_items t

-- | Toplevel parser for formulae

aFormula :: PrefixMap -> AnnoState.AParser st (Annotation.Annoted TEXT_META)

aFormula pm = AnnoState.allAnnoParser (cltext pm)