content: {- |
  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)
  