4176N/A{- |

0N/AModule : $EmptyHeader$

0N/ADescription : <optional short description entry>

0N/ACopyright : (c) <Authors or Affiliations>

0N/ALicense : GPLv2 or higher

0N/A

0N/AMaintainer : <email>

0N/AStability : unstable | experimental | provisional | stable | frozen

0N/APortability : portable | non-portable (<reason>)

0N/A

0N/A<optional description>

0N/A-}

0N/Amodule CommonLogic.OMDocExport where

0N/A

0N/Aimport CommonLogic.AS_CommonLogic

0N/Aimport CommonLogic.Sign

0N/Aimport CommonLogic.Symbol

2362N/Aimport CommonLogic.OMDoc

2362N/A

2362N/Aimport OMDoc.DataTypes

1178N/A

4880N/Aimport Common.Id

0N/Aimport Common.Result

0N/Aimport Common.AS_Annotation

1178N/Aimport qualified Common.Lib.Rel as Rel

0N/A

0N/Aimport qualified Data.Map as Map

0N/Aimport Data.Maybe

0N/A

0N/A

4880N/A

4880N/Atype Env = NameMap Symbol

4880N/A

4880N/A

4880N/A

4880N/AexportSymToOmdoc :: Env -> Symbol -> String -> Result TCElement

4880N/AexportSymToOmdoc _ _ n = return $ (TCSymbol n const_symbol Obj Nothing)

4880N/A

4880N/A

4880N/A

4880N/A------------------------------------------------------------

4880N/AexportSenToOmdoc :: Env -> SENTENCE

4880N/A -> Result TCorOMElement

4880N/AexportSenToOmdoc en s = return $ Right $ exportSenToOmdoc' en [] s

4880N/A

0N/A

0N/AexportSenToOmdoc' :: Env -> [NAME_OR_SEQMARK] -> SENTENCE

0N/A -> OMElement

0N/AexportSenToOmdoc' en vars s = case s of

0N/A Quant_sent qs _ -> case qs of

0N/A Universal vars2 s2 -> OMBIND const_forall

0N/A (map exportVar vars2)

0N/A (exportSenToOmdoc' en (union vars vars2) s2)

4880N/A Existential vars2 s2 -> OMBIND const_exists

4880N/A (map exportVar vars2)

4880N/A (exportSenToOmdoc' en (union vars vars2) s2)

4880N/A Bool_sent bs _ -> case bs of

0N/A Conjunction ss -> OMA $ const_and : (map (exportSenToOmdoc' en vars) ss)

0N/A Disjunction ss -> OMA $ const_or : (map (exportSenToOmdoc' en vars) ss)

0N/A Negation s1 -> OMA [ const_not,

0N/A exportSenToOmdoc' en vars s1]

0N/A Implication s1 s2 -> OMA [ const_implies,

4880N/A exportSenToOmdoc' en vars s1,

4880N/A exportSenToOmdoc' en vars s2]

4880N/A Biconditional s1 s2 -> OMA [ const_equivalent,

4880N/A exportSenToOmdoc' en vars s1,

0N/A exportSenToOmdoc' en vars s2]

0N/A Atom_sent at ir -> case at of

0N/A Equation t1 t2 -> OMA [ const_eq ,

0N/A exportTerm en vars t1,

4880N/A exportTerm en vars t2 ]

4880N/A Atom pt tts -> OMA $ (exportTerm en pt) : (map (exportTermSeq en vars) tts)

4880N/A Comment_sent com s1 ir -> OMA [const_comment,

4880N/A exportSenToOmdoc' en vars s1]

4880N/A Irregular_sent s1 ir -> OMA [const_irregular,

0N/A exportSenToOmdoc' en vars s1]

0N/A

0N/AexportTerm :: Env -> [NAME_OR_SEQMARK] -> TERM -> OMElement

4880N/AexportTerm e vars t = case t of

0N/A Name_term n -> if finds (CommonLogic.AS_CommonLogic.Name n) vars

4880N/A then exportVar (CommonLogic.AS_CommonLogic.Name n)

4880N/A else oms e n

0N/A Funct_term ft tss ir -> OMA $ (exportTerm e vars ft) : (map (exportTermSeq e vars) tss)

0N/A Comment_term t1 com ir -> OMA [ const_comment_term,

0N/A exportTerm e vars t1 ]

4880N/A

0N/A

4880N/AexportTermSeq :: Env -> [NAME_OR_SEQMARK] -> TERM_SEQ -> OMElement

4880N/AexportTermSeq e vars ts = case ts of

0N/A Term_seq t -> exportTerm e vars t

0N/A Seq_marks s -> if finds (SeqMark s) vars

0N/A then exportVar (SeqMark s)

4880N/A else oms e s

0N/A

4880N/AexportVar :: NAME_OR_SEQMARK -> OMElement

4880N/AexportVar (CommonLogic.AS_CommonLogic.Name n) = OMV $ mkSimpleName $ tokStr n

0N/AexportVar (SeqMark s) = OMV $ mkSimpleName $ tokStr s

0N/A

0N/A

4880N/A

0N/Aoms :: Env -> Token -> OMElement

1178N/Aoms e x = let s = toSymbol x

1178N/A err = error $ "oms: no mapping for the symbol"

0N/A 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 tk@(Token toks tokp) = Symbol (nameToId toks)

finds :: NAME_OR_SEQMARK -> [NAME_OR_SEQMARK] -> Bool

finds _ [] = False

finds n a@(m:vars) = if n == m

then True

else False

union :: [a] -> [a] -> [a]

union [] v2 = v2

union a@(v:v1) v2 = v : (union v1 v2)