{- |
Module      :  ./CommonLogic/OMDocImport.hs
Description :  OMDoc-to-CommonLogic conversion
Copyright   :  (c) Iulia Ignatov, DFKI Bremen 2009, Eugen Kuksa, Uni Bremen 2011
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  eugenk@informatik.uni-bremen.de
Stability   :  experimental
Portability :  portable

Common Logic implementation of the interface functions
omdocToSym and omdocToSen from class Logic.
The actual instantiation can be found in module "CommonLogic.Logic_CommonLogic".
-}


module CommonLogic.OMDocImport
       ( omdocToSym
       , omdocToSen
       ) where


import OMDoc.DataTypes

import CommonLogic.AS_CommonLogic as AS
import CommonLogic.Symbol
import CommonLogic.OMDoc

import Common.Id
import Common.Result
import Common.AS_Annotation


type Env = SigMapI Symbol

-- | TCSymbol is transformed into a CommonLogic Symbol with given name
omdocToSym :: Env -> TCElement -> String -> Result Symbol
omdocToSym _ (TCSymbol _ _ sr _) n =
     case sr of
       Obj -> return $ Symbol (nameToId n)
       _ -> fail $ "omdocToSym: only objects are allowed as symbol roles, but found" ++ show sr
omdocToSym _ symb _ = fail $ "omdocToSym: only TCSymbols are allowed, but found: " ++ show symb


-- | Sentences from OMElements
omdocToSen :: Env -> TCElement -> String -> Result (Maybe (Named TEXT_META))
omdocToSen e (TCSymbol _ t sr _) n =
    case nameDecode n of
      Just _ ->
          return Nothing -- don't translate encoded names here
      Nothing ->
          let ns = makeNamed n $ emptyTextMeta { getText = toText e t }
              res b = return $ Just $ ns { isAxiom = b }
          in case sr of
               Axiom -> res True
               Theorem -> res False
               _ -> return Nothing
omdocToSen _ sym _ = fail $ concat [ "omdocToSen: only TCSymbol is allowed,"
                                   , " but found: ", show sym ]

toText :: Env -> OMElement -> TEXT
toText e om = case om of
  OMA (op : subl)
    | op == const_and -> Text (map (toPhrase e) subl) nullRange
    | op == const_textName -> case subl of
        [OMV (OMName n _), txt@(OMA _)] -> Named_text (strToToken n) (toText e txt) nullRange
        _ -> error $ "toText: only two arguments supported, but found " ++ show subl
    | otherwise -> error $ concat ["toText: only ", show const_and , " and ",
            show const_textName, " and Named_text supported, but found ", show op]
  _ -> error $ "toText: only OMA with at lease one argument is allowed, but found " ++ show om

toPhrase :: Env -> OMElement -> PHRASE
toPhrase e om = case om of
  OMBIND op [n] m ->
      if op == const_module
      then Module $ toModule e m n
      else Sentence $ toSen e om
  OMA (op : cmt : [txt]) ->
      if op == const_comment
      then Comment_text (varToComment cmt) (toText e txt) nullRange
      else Sentence $ toSen e om
  _ -> Sentence $ toSen e om

toModule :: Env -> OMElement -> OMElement -> MODULE
toModule e om n = case om of
  OMA (op : txt : exs) ->
      if op == const_moduleExcludes
      then Mod_ex (toName n) (map toName exs) (toText e txt) nullRange
      else Mod (toName n) (toText e om) nullRange
  _ -> Mod (toName n) (toText e om) nullRange
  where toName (OMV (OMName k _)) = strToToken k
        toName k = error $ "toModule: only OMV OMName supported, but found " ++ show k


toSen :: Env -> OMElement -> SENTENCE
toSen e om = case om of
  OMBIND binder args body ->
    let vars = map toNameSeqmark args
        sent = toSen e body
        quant | binder == const_forall = Universal
              | binder == const_exists = Existential
              | otherwise = error "toSen: not supported binder"
        in Quant_sent quant vars sent nullRange
  OMA (omh : os)
    | omh == const_and ->
      Bool_sent (Junction Conjunction (map (toSen e) os)) nullRange
    | omh == const_or ->
      Bool_sent (Junction Disjunction (map (toSen e) os)) nullRange
    | omh == const_implies ->
      let s1 : s2 : [] = map (toSen e) os
      in Bool_sent (BinOp Implication s1 s2) nullRange
    | omh == const_equivalent ->
      let s1 : s2 : [] = map (toSen e) os
      in Bool_sent (BinOp Biconditional s1 s2) nullRange
    | omh == const_not -> let ns : [] = map (toSen e) os
                          in Bool_sent (Negation ns) nullRange
    | omh == const_eq -> let t1 : t2 : [] = map (omdocToTerm e) os
                         in Atom_sent (Equation t1 t2) nullRange
    | omh == const_comment && not (null os) ->
      let s : [] = map (toSen e) $ tail os
      in Comment_sent (varToComment $ head os) s nullRange
    | omh == const_comment -> error "toSen: commented sentence has no comment"
    | omh == const_irregular -> let s : [] = map (toSen e) os
                                in Irregular_sent s nullRange
    | otherwise -> Atom_sent (Atom (omdocToTerm e omh)
                              (map (omdocToTermSeq e) os)) nullRange
  _ -> error $
       concat [ "toSen: only applications and quantifications are allowed,"
              , " but found: ", show om ]

toNameSeqmark :: OMElement -> NAME_OR_SEQMARK
toNameSeqmark (OMV (OMName n _)) = let dec = strToToken n
                                     in if isSeqMark n
                                        then SeqMark dec
                                        else AS.Name dec
toNameSeqmark _ = error "toNameSeqmark: only variables allowed"

omdocToTerm :: Env -> OMElement -> TERM
omdocToTerm e (OMA (omh : om))
                     | omh == const_comment_term
                        && not (null om) = let t : [] = map (omdocToTerm e) $ tail om
                                           in Comment_term t (varToComment $ head om) nullRange
                     | omh == const_comment_term = error "omdocToTerm: commented term has no comment"
                     | otherwise = let th = omdocToTerm e omh
                                       ts = map (omdocToTermSeq e) om
                                    in Funct_term th ts nullRange
omdocToTerm _ (OMS (_, OMName n _)) = Name_term (strToToken n)
omdocToTerm _ (OMV (OMName n _)) = Name_term (strToToken n)
omdocToTerm _ om = error $ "omdocToTerm: only applications and symbols allowed, but found: " ++ show om


omdocToTermSeq :: Env -> OMElement -> TERM_SEQ
omdocToTermSeq e om@(OMA _) = Term_seq $ omdocToTerm e om
omdocToTermSeq _ (OMS (_, OMName n _)) = let dec = strToToken n
                                         in if isSeqMark n
                                            then Seq_marks dec
                                            else Term_seq (Name_term dec)
omdocToTermSeq _ (OMV (OMName n _)) = let dec = strToToken n
                                       in if isSeqMark n
                                          then Seq_marks dec
                                          else Term_seq (Name_term dec)
omdocToTermSeq _ om = error $ "omdocToTermSeq: only applications, symbols and variables allowed, but found: " ++ show om

strToToken :: String -> Token
strToToken s = Token s nullRange

isSeqMark :: String -> Bool
isSeqMark ('.' : _) = True
isSeqMark _ = False

varToComment :: OMElement -> COMMENT
varToComment (OMV (OMName cmt _)) = Comment cmt nullRange
varToComment om = error $ "varToComment: only OMV OMName supported, but found: " ++ show om
