Parse_CLIF.hs

{- |
Module      :  ./CommonLogic/Parse_CLIF.hs
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, parens)
import Common.Keywords (colonS, mapsTo)
import Common.GlobalAnnotations (PrefixMap)
import Common.Parsec
import Common.Token

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

namedtext :: CharParser st (TEXT, [PrefixMapping])
namedtext = do
    n <- identifier <?> "name after \"cl-text\""
    (t, prfxs) <- option (Text [] nullRange, []) text
    return (Named_text n t nullRange, prfxs)

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
  many white
  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 <- many termseq
    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

symbIdentifier :: CharParser st Token
symbIdentifier =
  pToken (reserved (reservedelement ++ casl_reserved_words) scanClSymbol)
  <?> "symbol"

scanClSymbol :: CharParser st String
scanClSymbol = quotedstring <|> enclosedname <|>
 (satisfy (\ c -> clLetters c && notElem c "%{}[],;=")
  <:> many clLetter <?> "words")

intNameOrSeqMark :: CharParser st NAME_OR_SEQMARK
intNameOrSeqMark = do
    s <- seqmark -- fix seqmark parser for one
    return $ SeqMark s
  <|> do
    n <- symbIdentifier
    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 <- symbIdentifier
  do f <- pToken $ toKey mapsTo
     t <- symbIdentifier
     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 Annotation.emptyAnno

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