{- |

Module : $Header$

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