{- |

Module : $Header$

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 _ _ n = return $ TCSymbol n const_symbol Obj Nothing

-- | Exports the text @tm@ to OMDoc

exportSenToOmdoc :: Env -> TEXT_META

-> Result TCorOMElement

exportSenToOmdoc en tm = return $ Right $ exportText en [] $ AS.getText tm

exportText :: Env -> [NAME_OR_SEQMARK] -> TEXT -> OMElement

exportText en vars txt = case txt of

Text phrs _ ->

OMA $ const_and : map (exportPhr en vars) (filter nonImportation phrs)

Named_text n t _ ->

OMA [const_textName, OMV $ mkSimpleName $ tokStr n, exportText en vars t]

where nonImportation p = case p of

Importation _ -> False

_ -> True

exportPhr :: Env -> [NAME_OR_SEQMARK] -> PHRASE -> OMElement

exportPhr en vars phr = case phr of

Importation _ -> undefined -- does not occur

Module m -> OMBIND const_module [modName m] $ exportModule en vars m

Sentence s -> exportSen en vars s

Comment_text c t _ ->

OMA [const_comment, varFromComment c, exportText en vars t]

where modName m = case m of

Mod n _ _ -> exportVar $ AS.Name n

Mod_ex n _ _ _ -> exportVar $ AS.Name n

exportModule :: Env -> [NAME_OR_SEQMARK] -> MODULE -> OMElement

exportModule en vars m = case m of

Mod _ t _ -> exportText en vars t

Mod_ex _ exs t _ -> OMA $ const_moduleExcludes : exportText en vars t

: map (exportVar . AS.Name) exs

exportSen :: Env -> [NAME_OR_SEQMARK] -> SENTENCE

-> OMElement

exportSen en vars s = case s of

Quant_sent q vars2 s2 _ ->

OMBIND (case q of

Universal -> const_forall

Existential -> const_exists)

(map exportVar vars2)

(exportSen en (vars ++ vars2) s2)

Bool_sent bs _ -> case bs of

Junction j ss ->

OMA $ (case j of Conjunction -> const_and

Disjunction -> const_or)

: map (exportSen en vars) ss

Negation s1 -> OMA [ const_not, exportSen en vars s1]

BinOp op s1 s2 -> OMA

[ case op of Implication -> const_implies

Biconditional -> const_equivalent

, exportSen en vars s1

, exportSen en vars s2]

Atom_sent at _ -> case at of

Equation t1 t2 -> OMA

[ const_eq

, exportTerm en vars t1

, exportTerm en vars t2 ]

Atom pt tts ->

OMA $ exportTerm en vars pt : map (exportTermSeq en vars) tts

Comment_sent _com s1 _ ->

OMA [const_comment, varFromComment _com, exportSen en vars s1]

Irregular_sent s1 _ ->

OMA [const_irregular, exportSen en vars s1]

exportTerm :: Env -> [NAME_OR_SEQMARK] -> TERM -> OMElement

exportTerm e vars t = case t of

Name_term n -> if AS.Name n `elem` vars

then exportVar (AS.Name n)

else oms e n

Funct_term ft tss _ ->

OMA $ exportTerm e vars ft : map (exportTermSeq e vars) tss

Comment_term t1 _com _ ->

OMA [ const_comment_term, varFromComment _com, exportTerm e vars t1 ]

That_term s _ ->

OMA [ const_that, exportSen e vars s ]

exportTermSeq :: Env -> [NAME_OR_SEQMARK] -> TERM_SEQ -> OMElement

exportTermSeq e vars ts = case ts of

Term_seq t -> exportTerm e vars t

Seq_marks s -> if SeqMark s `elem` vars

then exportVar (SeqMark s)

else oms e s

exportVar :: NAME_OR_SEQMARK -> OMElement

exportVar (AS.Name n) = OMV $ mkSimpleName $ tokStr n

exportVar (SeqMark s) = OMV $ mkSimpleName $ tokStr s

varFromComment :: COMMENT -> OMElement

varFromComment (Comment x _) = OMV $ mkSimpleName x

oms :: Env -> Token -> OMElement

oms e x =

let s = toSymbol x

err = error $ "oms: no mapping for the symbol " ++ show s

-- printId1 (symName s) ++ "\n" ++ show e ++ "\n\n\n" ++ ""

in simpleOMS $ findInEnv err e s

findInEnv :: (Ord k) => a -> Map.Map k a -> k -> a

findInEnv err m x = Map.findWithDefault err x m

-- transform a NAME_OR_SEQMARK into a symbol.

toSymbol :: Token -> Symbol

toSymbol = Symbol . simpleIdToId