{- |
Module      :  ./CommonLogic/OMDocExport.hs
Description :  CommonLogic-to-OMDoc 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
export_senToOmdoc and export_symToOmdoc from class Logic.
The actual instantiation can be found in module "CommonLogic.Logic_CommonLogic".
-}

module CommonLogic.OMDocExport
       ( exportSymToOmdoc
       , exportSenToOmdoc
       ) where

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

import OMDoc.DataTypes

import Common.Id
import Common.Result

import qualified Data.Map as Map


type Env = NameMap Symbol

-- | Exports the symbol @n@ to OMDoc
exportSymToOmdoc :: Env -> Symbol -> String -> Result TCElement
exportSymToOmdoc :: Env -> Symbol -> String -> Result TCElement
exportSymToOmdoc _ _ n :: String
n = TCElement -> Result TCElement
forall (m :: * -> *) a. Monad m => a -> m a
return (TCElement -> Result TCElement) -> TCElement -> Result TCElement
forall a b. (a -> b) -> a -> b
$ String -> OMElement -> SymbolRole -> Maybe OMElement -> TCElement
TCSymbol String
n OMElement
const_symbol SymbolRole
Obj Maybe OMElement
forall a. Maybe a
Nothing


-- | Exports the text @tm@ to OMDoc
exportSenToOmdoc :: Env -> TEXT_META
                 -> Result TCorOMElement
exportSenToOmdoc :: Env -> TEXT_META -> Result TCorOMElement
exportSenToOmdoc en :: Env
en tm :: TEXT_META
tm = TCorOMElement -> Result TCorOMElement
forall (m :: * -> *) a. Monad m => a -> m a
return (TCorOMElement -> Result TCorOMElement)
-> TCorOMElement -> Result TCorOMElement
forall a b. (a -> b) -> a -> b
$ OMElement -> TCorOMElement
forall a b. b -> Either a b
Right (OMElement -> TCorOMElement) -> OMElement -> TCorOMElement
forall a b. (a -> b) -> a -> b
$ Env -> [NAME_OR_SEQMARK] -> TEXT -> OMElement
exportText Env
en [] (TEXT -> OMElement) -> TEXT -> OMElement
forall a b. (a -> b) -> a -> b
$ TEXT_META -> TEXT
AS.getText TEXT_META
tm

exportText :: Env -> [NAME_OR_SEQMARK] -> TEXT -> OMElement
exportText :: Env -> [NAME_OR_SEQMARK] -> TEXT -> OMElement
exportText en :: Env
en vars :: [NAME_OR_SEQMARK]
vars txt :: TEXT
txt = case TEXT
txt of
  Text phrs :: [PHRASE]
phrs _ ->
      [OMElement] -> OMElement
OMA ([OMElement] -> OMElement) -> [OMElement] -> OMElement
forall a b. (a -> b) -> a -> b
$ OMElement
const_and OMElement -> [OMElement] -> [OMElement]
forall a. a -> [a] -> [a]
: (PHRASE -> OMElement) -> [PHRASE] -> [OMElement]
forall a b. (a -> b) -> [a] -> [b]
map (Env -> [NAME_OR_SEQMARK] -> PHRASE -> OMElement
exportPhr Env
en [NAME_OR_SEQMARK]
vars) ((PHRASE -> Bool) -> [PHRASE] -> [PHRASE]
forall a. (a -> Bool) -> [a] -> [a]
filter PHRASE -> Bool
nonImportation [PHRASE]
phrs)
  Named_text n :: NAME
n t :: TEXT
t _ ->
      [OMElement] -> OMElement
OMA [OMElement
const_textName, OMName -> OMElement
OMV (OMName -> OMElement) -> OMName -> OMElement
forall a b. (a -> b) -> a -> b
$ String -> OMName
mkSimpleName (String -> OMName) -> String -> OMName
forall a b. (a -> b) -> a -> b
$ NAME -> String
tokStr NAME
n, Env -> [NAME_OR_SEQMARK] -> TEXT -> OMElement
exportText Env
en [NAME_OR_SEQMARK]
vars TEXT
t]
  where nonImportation :: PHRASE -> Bool
nonImportation p :: PHRASE
p = case PHRASE
p of
          Importation _ -> Bool
False
          _ -> Bool
True

exportPhr :: Env -> [NAME_OR_SEQMARK] -> PHRASE -> OMElement
exportPhr :: Env -> [NAME_OR_SEQMARK] -> PHRASE -> OMElement
exportPhr en :: Env
en vars :: [NAME_OR_SEQMARK]
vars phr :: PHRASE
phr = case PHRASE
phr of
   Importation _ -> OMElement
forall a. HasCallStack => a
undefined -- does not occur
   Module m :: MODULE
m -> OMElement -> [OMElement] -> OMElement -> OMElement
OMBIND OMElement
const_module [MODULE -> OMElement
modName MODULE
m] (OMElement -> OMElement) -> OMElement -> OMElement
forall a b. (a -> b) -> a -> b
$ Env -> [NAME_OR_SEQMARK] -> MODULE -> OMElement
exportModule Env
en [NAME_OR_SEQMARK]
vars MODULE
m
   Sentence s :: SENTENCE
s -> Env -> [NAME_OR_SEQMARK] -> SENTENCE -> OMElement
exportSen Env
en [NAME_OR_SEQMARK]
vars SENTENCE
s
   Comment_text c :: COMMENT
c t :: TEXT
t _ ->
      [OMElement] -> OMElement
OMA [OMElement
const_comment, COMMENT -> OMElement
varFromComment COMMENT
c, Env -> [NAME_OR_SEQMARK] -> TEXT -> OMElement
exportText Env
en [NAME_OR_SEQMARK]
vars TEXT
t]
  where modName :: MODULE -> OMElement
modName m :: MODULE
m = case MODULE
m of
          Mod n :: NAME
n _ _ -> NAME_OR_SEQMARK -> OMElement
exportVar (NAME_OR_SEQMARK -> OMElement) -> NAME_OR_SEQMARK -> OMElement
forall a b. (a -> b) -> a -> b
$ NAME -> NAME_OR_SEQMARK
AS.Name NAME
n
          Mod_ex n :: NAME
n _ _ _ -> NAME_OR_SEQMARK -> OMElement
exportVar (NAME_OR_SEQMARK -> OMElement) -> NAME_OR_SEQMARK -> OMElement
forall a b. (a -> b) -> a -> b
$ NAME -> NAME_OR_SEQMARK
AS.Name NAME
n

exportModule :: Env -> [NAME_OR_SEQMARK] -> MODULE -> OMElement
exportModule :: Env -> [NAME_OR_SEQMARK] -> MODULE -> OMElement
exportModule en :: Env
en vars :: [NAME_OR_SEQMARK]
vars m :: MODULE
m = case MODULE
m of
  Mod _ t :: TEXT
t _ -> Env -> [NAME_OR_SEQMARK] -> TEXT -> OMElement
exportText Env
en [NAME_OR_SEQMARK]
vars TEXT
t
  Mod_ex _ exs :: [NAME]
exs t :: TEXT
t _ -> [OMElement] -> OMElement
OMA ([OMElement] -> OMElement) -> [OMElement] -> OMElement
forall a b. (a -> b) -> a -> b
$ OMElement
const_moduleExcludes OMElement -> [OMElement] -> [OMElement]
forall a. a -> [a] -> [a]
: Env -> [NAME_OR_SEQMARK] -> TEXT -> OMElement
exportText Env
en [NAME_OR_SEQMARK]
vars TEXT
t
      OMElement -> [OMElement] -> [OMElement]
forall a. a -> [a] -> [a]
: (NAME -> OMElement) -> [NAME] -> [OMElement]
forall a b. (a -> b) -> [a] -> [b]
map (NAME_OR_SEQMARK -> OMElement
exportVar (NAME_OR_SEQMARK -> OMElement)
-> (NAME -> NAME_OR_SEQMARK) -> NAME -> OMElement
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NAME -> NAME_OR_SEQMARK
AS.Name) [NAME]
exs

exportSen :: Env -> [NAME_OR_SEQMARK] -> SENTENCE
                  -> OMElement
exportSen :: Env -> [NAME_OR_SEQMARK] -> SENTENCE -> OMElement
exportSen en :: Env
en vars :: [NAME_OR_SEQMARK]
vars s :: SENTENCE
s = case SENTENCE
s of
      Quant_sent q :: QUANT
q vars2 :: [NAME_OR_SEQMARK]
vars2 s2 :: SENTENCE
s2 _ ->
        OMElement -> [OMElement] -> OMElement -> OMElement
OMBIND (case QUANT
q of
                   Universal -> OMElement
const_forall
                   Existential -> OMElement
const_exists)
        ((NAME_OR_SEQMARK -> OMElement) -> [NAME_OR_SEQMARK] -> [OMElement]
forall a b. (a -> b) -> [a] -> [b]
map NAME_OR_SEQMARK -> OMElement
exportVar [NAME_OR_SEQMARK]
vars2)
        (Env -> [NAME_OR_SEQMARK] -> SENTENCE -> OMElement
exportSen Env
en ([NAME_OR_SEQMARK]
vars [NAME_OR_SEQMARK] -> [NAME_OR_SEQMARK] -> [NAME_OR_SEQMARK]
forall a. [a] -> [a] -> [a]
++ [NAME_OR_SEQMARK]
vars2) SENTENCE
s2)
      Bool_sent bs :: BOOL_SENT
bs _ -> case BOOL_SENT
bs of
          Junction j :: AndOr
j ss :: [SENTENCE]
ss ->
            [OMElement] -> OMElement
OMA ([OMElement] -> OMElement) -> [OMElement] -> OMElement
forall a b. (a -> b) -> a -> b
$ (case AndOr
j of Conjunction -> OMElement
const_and
                             Disjunction -> OMElement
const_or)
            OMElement -> [OMElement] -> [OMElement]
forall a. a -> [a] -> [a]
: (SENTENCE -> OMElement) -> [SENTENCE] -> [OMElement]
forall a b. (a -> b) -> [a] -> [b]
map (Env -> [NAME_OR_SEQMARK] -> SENTENCE -> OMElement
exportSen Env
en [NAME_OR_SEQMARK]
vars) [SENTENCE]
ss
          Negation s1 :: SENTENCE
s1 -> [OMElement] -> OMElement
OMA [ OMElement
const_not, Env -> [NAME_OR_SEQMARK] -> SENTENCE -> OMElement
exportSen Env
en [NAME_OR_SEQMARK]
vars SENTENCE
s1]
          BinOp op :: ImplEq
op s1 :: SENTENCE
s1 s2 :: SENTENCE
s2 -> [OMElement] -> OMElement
OMA
              [ case ImplEq
op of Implication -> OMElement
const_implies
                           Biconditional -> OMElement
const_equivalent
              , Env -> [NAME_OR_SEQMARK] -> SENTENCE -> OMElement
exportSen Env
en [NAME_OR_SEQMARK]
vars SENTENCE
s1
              , Env -> [NAME_OR_SEQMARK] -> SENTENCE -> OMElement
exportSen Env
en [NAME_OR_SEQMARK]
vars SENTENCE
s2]
      Atom_sent at :: ATOM
at _ -> case ATOM
at of
          Equation t1 :: TERM
t1 t2 :: TERM
t2 -> [OMElement] -> OMElement
OMA
              [ OMElement
const_eq
              , Env -> [NAME_OR_SEQMARK] -> TERM -> OMElement
exportTerm Env
en [NAME_OR_SEQMARK]
vars TERM
t1
              , Env -> [NAME_OR_SEQMARK] -> TERM -> OMElement
exportTerm Env
en [NAME_OR_SEQMARK]
vars TERM
t2 ]
          Atom pt :: TERM
pt tts :: [TERM_SEQ]
tts ->
              [OMElement] -> OMElement
OMA ([OMElement] -> OMElement) -> [OMElement] -> OMElement
forall a b. (a -> b) -> a -> b
$ Env -> [NAME_OR_SEQMARK] -> TERM -> OMElement
exportTerm Env
en [NAME_OR_SEQMARK]
vars TERM
pt OMElement -> [OMElement] -> [OMElement]
forall a. a -> [a] -> [a]
: (TERM_SEQ -> OMElement) -> [TERM_SEQ] -> [OMElement]
forall a b. (a -> b) -> [a] -> [b]
map (Env -> [NAME_OR_SEQMARK] -> TERM_SEQ -> OMElement
exportTermSeq Env
en [NAME_OR_SEQMARK]
vars) [TERM_SEQ]
tts
      Comment_sent _com :: COMMENT
_com s1 :: SENTENCE
s1 _ ->
          [OMElement] -> OMElement
OMA [OMElement
const_comment, COMMENT -> OMElement
varFromComment COMMENT
_com, Env -> [NAME_OR_SEQMARK] -> SENTENCE -> OMElement
exportSen Env
en [NAME_OR_SEQMARK]
vars SENTENCE
s1]
      Irregular_sent s1 :: SENTENCE
s1 _ ->
          [OMElement] -> OMElement
OMA [OMElement
const_irregular, Env -> [NAME_OR_SEQMARK] -> SENTENCE -> OMElement
exportSen Env
en [NAME_OR_SEQMARK]
vars SENTENCE
s1]

exportTerm :: Env -> [NAME_OR_SEQMARK] -> TERM -> OMElement
exportTerm :: Env -> [NAME_OR_SEQMARK] -> TERM -> OMElement
exportTerm e :: Env
e vars :: [NAME_OR_SEQMARK]
vars t :: TERM
t = case TERM
t of
     Name_term n :: NAME
n -> if NAME -> NAME_OR_SEQMARK
AS.Name NAME
n NAME_OR_SEQMARK -> [NAME_OR_SEQMARK] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [NAME_OR_SEQMARK]
vars
                    then NAME_OR_SEQMARK -> OMElement
exportVar (NAME -> NAME_OR_SEQMARK
AS.Name NAME
n)
                    else Env -> NAME -> OMElement
oms Env
e NAME
n
     Funct_term ft :: TERM
ft tss :: [TERM_SEQ]
tss _ ->
         [OMElement] -> OMElement
OMA ([OMElement] -> OMElement) -> [OMElement] -> OMElement
forall a b. (a -> b) -> a -> b
$ Env -> [NAME_OR_SEQMARK] -> TERM -> OMElement
exportTerm Env
e [NAME_OR_SEQMARK]
vars TERM
ft OMElement -> [OMElement] -> [OMElement]
forall a. a -> [a] -> [a]
: (TERM_SEQ -> OMElement) -> [TERM_SEQ] -> [OMElement]
forall a b. (a -> b) -> [a] -> [b]
map (Env -> [NAME_OR_SEQMARK] -> TERM_SEQ -> OMElement
exportTermSeq Env
e [NAME_OR_SEQMARK]
vars) [TERM_SEQ]
tss
     Comment_term t1 :: TERM
t1 _com :: COMMENT
_com _ ->
         [OMElement] -> OMElement
OMA [ OMElement
const_comment_term, COMMENT -> OMElement
varFromComment COMMENT
_com, Env -> [NAME_OR_SEQMARK] -> TERM -> OMElement
exportTerm Env
e [NAME_OR_SEQMARK]
vars TERM
t1 ]
     That_term s :: SENTENCE
s _ ->
         [OMElement] -> OMElement
OMA [ OMElement
const_that, Env -> [NAME_OR_SEQMARK] -> SENTENCE -> OMElement
exportSen Env
e [NAME_OR_SEQMARK]
vars SENTENCE
s ]

exportTermSeq :: Env -> [NAME_OR_SEQMARK] -> TERM_SEQ -> OMElement
exportTermSeq :: Env -> [NAME_OR_SEQMARK] -> TERM_SEQ -> OMElement
exportTermSeq e :: Env
e vars :: [NAME_OR_SEQMARK]
vars ts :: TERM_SEQ
ts = case TERM_SEQ
ts of
     Term_seq t :: TERM
t -> Env -> [NAME_OR_SEQMARK] -> TERM -> OMElement
exportTerm Env
e [NAME_OR_SEQMARK]
vars TERM
t
     Seq_marks s :: NAME
s -> if NAME -> NAME_OR_SEQMARK
SeqMark NAME
s NAME_OR_SEQMARK -> [NAME_OR_SEQMARK] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [NAME_OR_SEQMARK]
vars
                    then NAME_OR_SEQMARK -> OMElement
exportVar (NAME -> NAME_OR_SEQMARK
SeqMark NAME
s)
                    else Env -> NAME -> OMElement
oms Env
e NAME
s

exportVar :: NAME_OR_SEQMARK -> OMElement
exportVar :: NAME_OR_SEQMARK -> OMElement
exportVar (AS.Name n :: NAME
n) = OMName -> OMElement
OMV (OMName -> OMElement) -> OMName -> OMElement
forall a b. (a -> b) -> a -> b
$ String -> OMName
mkSimpleName (String -> OMName) -> String -> OMName
forall a b. (a -> b) -> a -> b
$ NAME -> String
tokStr NAME
n
exportVar (SeqMark s :: NAME
s) = OMName -> OMElement
OMV (OMName -> OMElement) -> OMName -> OMElement
forall a b. (a -> b) -> a -> b
$ String -> OMName
mkSimpleName (String -> OMName) -> String -> OMName
forall a b. (a -> b) -> a -> b
$ NAME -> String
tokStr NAME
s

varFromComment :: COMMENT -> OMElement
varFromComment :: COMMENT -> OMElement
varFromComment (Comment x :: String
x _) = OMName -> OMElement
OMV (OMName -> OMElement) -> OMName -> OMElement
forall a b. (a -> b) -> a -> b
$ String -> OMName
mkSimpleName String
x


oms :: Env -> Token -> OMElement
oms :: Env -> NAME -> OMElement
oms e :: Env
e x :: NAME
x =
          let s :: Symbol
s = NAME -> Symbol
toSymbol NAME
x
              err :: a
err = String -> a
forall a. HasCallStack => String -> a
error (String -> a) -> String -> a
forall a b. (a -> b) -> a -> b
$ "oms: no mapping for the symbol " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Symbol -> String
forall a. Show a => a -> String
show Symbol
s
                  -- printId1 (symName s) ++ "\n" ++ show e ++ "\n\n\n" ++ ""
           in UniqName -> OMElement
simpleOMS (UniqName -> OMElement) -> UniqName -> OMElement
forall a b. (a -> b) -> a -> b
$ UniqName -> Env -> Symbol -> UniqName
forall k a. Ord k => a -> Map k a -> k -> a
findInEnv UniqName
forall a. a
err Env
e Symbol
s

findInEnv :: (Ord k) => a -> Map.Map k a -> k -> a
findInEnv :: a -> Map k a -> k -> a
findInEnv err :: a
err m :: Map k a
m x :: k
x = a -> k -> Map k a -> a
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault a
err k
x Map k a
m

-- transform a NAME_OR_SEQMARK into a symbol.
toSymbol :: Token -> Symbol
toSymbol :: NAME -> Symbol
toSymbol = Id -> Symbol
Symbol (Id -> Symbol) -> (NAME -> Id) -> NAME -> Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NAME -> Id
simpleIdToId