{- |
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