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
import qualified Control.Monad.Fail as Fail
type Env = SigMapI Symbol
omdocToSym :: Env -> TCElement -> String -> Result Symbol
omdocToSym :: Env -> TCElement -> String -> Result Symbol
omdocToSym _ (TCSymbol _ _ sr :: SymbolRole
sr _) n :: String
n =
case SymbolRole
sr of
Obj -> Symbol -> Result Symbol
forall (m :: * -> *) a. Monad m => a -> m a
return (Symbol -> Result Symbol) -> Symbol -> Result Symbol
forall a b. (a -> b) -> a -> b
$ Id -> Symbol
Symbol (String -> Id
nameToId String
n)
_ -> String -> Result Symbol
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail (String -> Result Symbol) -> String -> Result Symbol
forall a b. (a -> b) -> a -> b
$ "omdocToSym: only objects are allowed as symbol roles, but found" String -> String -> String
forall a. [a] -> [a] -> [a]
++ SymbolRole -> String
forall a. Show a => a -> String
show SymbolRole
sr
omdocToSym _ symb :: TCElement
symb _ = String -> Result Symbol
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail (String -> Result Symbol) -> String -> Result Symbol
forall a b. (a -> b) -> a -> b
$ "omdocToSym: only TCSymbols are allowed, but found: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ TCElement -> String
forall a. Show a => a -> String
show TCElement
symb
omdocToSen :: Env -> TCElement -> String -> Result (Maybe (Named TEXT_META))
omdocToSen :: Env -> TCElement -> String -> Result (Maybe (Named TEXT_META))
omdocToSen e :: Env
e (TCSymbol _ t :: OMElement
t sr :: SymbolRole
sr _) n :: String
n =
case String -> Maybe (String, [String])
nameDecode String
n of
Just _ ->
Maybe (Named TEXT_META) -> Result (Maybe (Named TEXT_META))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (Named TEXT_META)
forall a. Maybe a
Nothing
Nothing ->
let ns :: Named TEXT_META
ns = String -> TEXT_META -> Named TEXT_META
forall a s. a -> s -> SenAttr s a
makeNamed String
n (TEXT_META -> Named TEXT_META) -> TEXT_META -> Named TEXT_META
forall a b. (a -> b) -> a -> b
$ TEXT_META
emptyTextMeta { getText :: TEXT
getText = Env -> OMElement -> TEXT
toText Env
e OMElement
t }
res :: Bool -> m (Maybe (Named TEXT_META))
res b :: Bool
b = Maybe (Named TEXT_META) -> m (Maybe (Named TEXT_META))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (Named TEXT_META) -> m (Maybe (Named TEXT_META)))
-> Maybe (Named TEXT_META) -> m (Maybe (Named TEXT_META))
forall a b. (a -> b) -> a -> b
$ Named TEXT_META -> Maybe (Named TEXT_META)
forall a. a -> Maybe a
Just (Named TEXT_META -> Maybe (Named TEXT_META))
-> Named TEXT_META -> Maybe (Named TEXT_META)
forall a b. (a -> b) -> a -> b
$ Named TEXT_META
ns { isAxiom :: Bool
isAxiom = Bool
b }
in case SymbolRole
sr of
Axiom -> Bool -> Result (Maybe (Named TEXT_META))
forall (m :: * -> *).
Monad m =>
Bool -> m (Maybe (Named TEXT_META))
res Bool
True
Theorem -> Bool -> Result (Maybe (Named TEXT_META))
forall (m :: * -> *).
Monad m =>
Bool -> m (Maybe (Named TEXT_META))
res Bool
False
_ -> Maybe (Named TEXT_META) -> Result (Maybe (Named TEXT_META))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (Named TEXT_META)
forall a. Maybe a
Nothing
omdocToSen _ sym :: TCElement
sym _ = String -> Result (Maybe (Named TEXT_META))
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail (String -> Result (Maybe (Named TEXT_META)))
-> String -> Result (Maybe (Named TEXT_META))
forall a b. (a -> b) -> a -> b
$ [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ "omdocToSen: only TCSymbol is allowed,"
, " but found: ", TCElement -> String
forall a. Show a => a -> String
show TCElement
sym ]
toText :: Env -> OMElement -> TEXT
toText :: Env -> OMElement -> TEXT
toText e :: Env
e om :: OMElement
om = case OMElement
om of
OMA (op :: OMElement
op : subl :: [OMElement]
subl)
| OMElement
op OMElement -> OMElement -> Bool
forall a. Eq a => a -> a -> Bool
== OMElement
const_and -> [PHRASE] -> Range -> TEXT
Text ((OMElement -> PHRASE) -> [OMElement] -> [PHRASE]
forall a b. (a -> b) -> [a] -> [b]
map (Env -> OMElement -> PHRASE
toPhrase Env
e) [OMElement]
subl) Range
nullRange
| OMElement
op OMElement -> OMElement -> Bool
forall a. Eq a => a -> a -> Bool
== OMElement
const_textName -> case [OMElement]
subl of
[OMV (OMName n :: String
n _), txt :: OMElement
txt@(OMA _)] -> NAME -> TEXT -> Range -> TEXT
Named_text (String -> NAME
strToToken String
n) (Env -> OMElement -> TEXT
toText Env
e OMElement
txt) Range
nullRange
_ -> String -> TEXT
forall a. HasCallStack => String -> a
error (String -> TEXT) -> String -> TEXT
forall a b. (a -> b) -> a -> b
$ "toText: only two arguments supported, but found " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [OMElement] -> String
forall a. Show a => a -> String
show [OMElement]
subl
| Bool
otherwise -> String -> TEXT
forall a. HasCallStack => String -> a
error (String -> TEXT) -> String -> TEXT
forall a b. (a -> b) -> a -> b
$ [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ["toText: only ", OMElement -> String
forall a. Show a => a -> String
show OMElement
const_and , " and ",
OMElement -> String
forall a. Show a => a -> String
show OMElement
const_textName, " and Named_text supported, but found ", OMElement -> String
forall a. Show a => a -> String
show OMElement
op]
_ -> String -> TEXT
forall a. HasCallStack => String -> a
error (String -> TEXT) -> String -> TEXT
forall a b. (a -> b) -> a -> b
$ "toText: only OMA with at lease one argument is allowed, but found " String -> String -> String
forall a. [a] -> [a] -> [a]
++ OMElement -> String
forall a. Show a => a -> String
show OMElement
om
toPhrase :: Env -> OMElement -> PHRASE
toPhrase :: Env -> OMElement -> PHRASE
toPhrase e :: Env
e om :: OMElement
om = case OMElement
om of
OMBIND op :: OMElement
op [n :: OMElement
n] m :: OMElement
m ->
if OMElement
op OMElement -> OMElement -> Bool
forall a. Eq a => a -> a -> Bool
== OMElement
const_module
then MODULE -> PHRASE
Module (MODULE -> PHRASE) -> MODULE -> PHRASE
forall a b. (a -> b) -> a -> b
$ Env -> OMElement -> OMElement -> MODULE
toModule Env
e OMElement
m OMElement
n
else SENTENCE -> PHRASE
Sentence (SENTENCE -> PHRASE) -> SENTENCE -> PHRASE
forall a b. (a -> b) -> a -> b
$ Env -> OMElement -> SENTENCE
toSen Env
e OMElement
om
OMA (op :: OMElement
op : cmt :: OMElement
cmt : [txt :: OMElement
txt]) ->
if OMElement
op OMElement -> OMElement -> Bool
forall a. Eq a => a -> a -> Bool
== OMElement
const_comment
then COMMENT -> TEXT -> Range -> PHRASE
Comment_text (OMElement -> COMMENT
varToComment OMElement
cmt) (Env -> OMElement -> TEXT
toText Env
e OMElement
txt) Range
nullRange
else SENTENCE -> PHRASE
Sentence (SENTENCE -> PHRASE) -> SENTENCE -> PHRASE
forall a b. (a -> b) -> a -> b
$ Env -> OMElement -> SENTENCE
toSen Env
e OMElement
om
_ -> SENTENCE -> PHRASE
Sentence (SENTENCE -> PHRASE) -> SENTENCE -> PHRASE
forall a b. (a -> b) -> a -> b
$ Env -> OMElement -> SENTENCE
toSen Env
e OMElement
om
toModule :: Env -> OMElement -> OMElement -> MODULE
toModule :: Env -> OMElement -> OMElement -> MODULE
toModule e :: Env
e om :: OMElement
om n :: OMElement
n = case OMElement
om of
OMA (op :: OMElement
op : txt :: OMElement
txt : exs :: [OMElement]
exs) ->
if OMElement
op OMElement -> OMElement -> Bool
forall a. Eq a => a -> a -> Bool
== OMElement
const_moduleExcludes
then NAME -> [NAME] -> TEXT -> Range -> MODULE
Mod_ex (OMElement -> NAME
toName OMElement
n) ((OMElement -> NAME) -> [OMElement] -> [NAME]
forall a b. (a -> b) -> [a] -> [b]
map OMElement -> NAME
toName [OMElement]
exs) (Env -> OMElement -> TEXT
toText Env
e OMElement
txt) Range
nullRange
else NAME -> TEXT -> Range -> MODULE
Mod (OMElement -> NAME
toName OMElement
n) (Env -> OMElement -> TEXT
toText Env
e OMElement
om) Range
nullRange
_ -> NAME -> TEXT -> Range -> MODULE
Mod (OMElement -> NAME
toName OMElement
n) (Env -> OMElement -> TEXT
toText Env
e OMElement
om) Range
nullRange
where toName :: OMElement -> NAME
toName (OMV (OMName k :: String
k _)) = String -> NAME
strToToken String
k
toName k :: OMElement
k = String -> NAME
forall a. HasCallStack => String -> a
error (String -> NAME) -> String -> NAME
forall a b. (a -> b) -> a -> b
$ "toModule: only OMV OMName supported, but found " String -> String -> String
forall a. [a] -> [a] -> [a]
++ OMElement -> String
forall a. Show a => a -> String
show OMElement
k
toSen :: Env -> OMElement -> SENTENCE
toSen :: Env -> OMElement -> SENTENCE
toSen e :: Env
e om :: OMElement
om = case OMElement
om of
OMBIND binder :: OMElement
binder args :: [OMElement]
args body :: OMElement
body ->
let vars :: [NAME_OR_SEQMARK]
vars = (OMElement -> NAME_OR_SEQMARK) -> [OMElement] -> [NAME_OR_SEQMARK]
forall a b. (a -> b) -> [a] -> [b]
map OMElement -> NAME_OR_SEQMARK
toNameSeqmark [OMElement]
args
sent :: SENTENCE
sent = Env -> OMElement -> SENTENCE
toSen Env
e OMElement
body
quant :: QUANT
quant | OMElement
binder OMElement -> OMElement -> Bool
forall a. Eq a => a -> a -> Bool
== OMElement
const_forall = QUANT
Universal
| OMElement
binder OMElement -> OMElement -> Bool
forall a. Eq a => a -> a -> Bool
== OMElement
const_exists = QUANT
Existential
| Bool
otherwise = String -> QUANT
forall a. HasCallStack => String -> a
error "toSen: not supported binder"
in QUANT -> [NAME_OR_SEQMARK] -> SENTENCE -> Range -> SENTENCE
Quant_sent QUANT
quant [NAME_OR_SEQMARK]
vars SENTENCE
sent Range
nullRange
OMA (omh :: OMElement
omh : os :: [OMElement]
os)
| OMElement
omh OMElement -> OMElement -> Bool
forall a. Eq a => a -> a -> Bool
== OMElement
const_and ->
BOOL_SENT -> Range -> SENTENCE
Bool_sent (AndOr -> [SENTENCE] -> BOOL_SENT
Junction AndOr
Conjunction ((OMElement -> SENTENCE) -> [OMElement] -> [SENTENCE]
forall a b. (a -> b) -> [a] -> [b]
map (Env -> OMElement -> SENTENCE
toSen Env
e) [OMElement]
os)) Range
nullRange
| OMElement
omh OMElement -> OMElement -> Bool
forall a. Eq a => a -> a -> Bool
== OMElement
const_or ->
BOOL_SENT -> Range -> SENTENCE
Bool_sent (AndOr -> [SENTENCE] -> BOOL_SENT
Junction AndOr
Disjunction ((OMElement -> SENTENCE) -> [OMElement] -> [SENTENCE]
forall a b. (a -> b) -> [a] -> [b]
map (Env -> OMElement -> SENTENCE
toSen Env
e) [OMElement]
os)) Range
nullRange
| OMElement
omh OMElement -> OMElement -> Bool
forall a. Eq a => a -> a -> Bool
== OMElement
const_implies ->
let s1 :: SENTENCE
s1 : s2 :: SENTENCE
s2 : [] = (OMElement -> SENTENCE) -> [OMElement] -> [SENTENCE]
forall a b. (a -> b) -> [a] -> [b]
map (Env -> OMElement -> SENTENCE
toSen Env
e) [OMElement]
os
in BOOL_SENT -> Range -> SENTENCE
Bool_sent (ImplEq -> SENTENCE -> SENTENCE -> BOOL_SENT
BinOp ImplEq
Implication SENTENCE
s1 SENTENCE
s2) Range
nullRange
| OMElement
omh OMElement -> OMElement -> Bool
forall a. Eq a => a -> a -> Bool
== OMElement
const_equivalent ->
let s1 :: SENTENCE
s1 : s2 :: SENTENCE
s2 : [] = (OMElement -> SENTENCE) -> [OMElement] -> [SENTENCE]
forall a b. (a -> b) -> [a] -> [b]
map (Env -> OMElement -> SENTENCE
toSen Env
e) [OMElement]
os
in BOOL_SENT -> Range -> SENTENCE
Bool_sent (ImplEq -> SENTENCE -> SENTENCE -> BOOL_SENT
BinOp ImplEq
Biconditional SENTENCE
s1 SENTENCE
s2) Range
nullRange
| OMElement
omh OMElement -> OMElement -> Bool
forall a. Eq a => a -> a -> Bool
== OMElement
const_not -> let ns :: SENTENCE
ns : [] = (OMElement -> SENTENCE) -> [OMElement] -> [SENTENCE]
forall a b. (a -> b) -> [a] -> [b]
map (Env -> OMElement -> SENTENCE
toSen Env
e) [OMElement]
os
in BOOL_SENT -> Range -> SENTENCE
Bool_sent (SENTENCE -> BOOL_SENT
Negation SENTENCE
ns) Range
nullRange
| OMElement
omh OMElement -> OMElement -> Bool
forall a. Eq a => a -> a -> Bool
== OMElement
const_eq -> let t1 :: TERM
t1 : t2 :: TERM
t2 : [] = (OMElement -> TERM) -> [OMElement] -> [TERM]
forall a b. (a -> b) -> [a] -> [b]
map (Env -> OMElement -> TERM
omdocToTerm Env
e) [OMElement]
os
in ATOM -> Range -> SENTENCE
Atom_sent (TERM -> TERM -> ATOM
Equation TERM
t1 TERM
t2) Range
nullRange
| OMElement
omh OMElement -> OMElement -> Bool
forall a. Eq a => a -> a -> Bool
== OMElement
const_comment Bool -> Bool -> Bool
&& Bool -> Bool
not ([OMElement] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [OMElement]
os) ->
let s :: SENTENCE
s : [] = (OMElement -> SENTENCE) -> [OMElement] -> [SENTENCE]
forall a b. (a -> b) -> [a] -> [b]
map (Env -> OMElement -> SENTENCE
toSen Env
e) ([OMElement] -> [SENTENCE]) -> [OMElement] -> [SENTENCE]
forall a b. (a -> b) -> a -> b
$ [OMElement] -> [OMElement]
forall a. [a] -> [a]
tail [OMElement]
os
in COMMENT -> SENTENCE -> Range -> SENTENCE
Comment_sent (OMElement -> COMMENT
varToComment (OMElement -> COMMENT) -> OMElement -> COMMENT
forall a b. (a -> b) -> a -> b
$ [OMElement] -> OMElement
forall a. [a] -> a
head [OMElement]
os) SENTENCE
s Range
nullRange
| OMElement
omh OMElement -> OMElement -> Bool
forall a. Eq a => a -> a -> Bool
== OMElement
const_comment -> String -> SENTENCE
forall a. HasCallStack => String -> a
error "toSen: commented sentence has no comment"
| OMElement
omh OMElement -> OMElement -> Bool
forall a. Eq a => a -> a -> Bool
== OMElement
const_irregular -> let s :: SENTENCE
s : [] = (OMElement -> SENTENCE) -> [OMElement] -> [SENTENCE]
forall a b. (a -> b) -> [a] -> [b]
map (Env -> OMElement -> SENTENCE
toSen Env
e) [OMElement]
os
in SENTENCE -> Range -> SENTENCE
Irregular_sent SENTENCE
s Range
nullRange
| Bool
otherwise -> ATOM -> Range -> SENTENCE
Atom_sent (TERM -> [TERM_SEQ] -> ATOM
Atom (Env -> OMElement -> TERM
omdocToTerm Env
e OMElement
omh)
((OMElement -> TERM_SEQ) -> [OMElement] -> [TERM_SEQ]
forall a b. (a -> b) -> [a] -> [b]
map (Env -> OMElement -> TERM_SEQ
omdocToTermSeq Env
e) [OMElement]
os)) Range
nullRange
_ -> String -> SENTENCE
forall a. HasCallStack => String -> a
error (String -> SENTENCE) -> String -> SENTENCE
forall a b. (a -> b) -> a -> b
$
[String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ "toSen: only applications and quantifications are allowed,"
, " but found: ", OMElement -> String
forall a. Show a => a -> String
show OMElement
om ]
toNameSeqmark :: OMElement -> NAME_OR_SEQMARK
toNameSeqmark :: OMElement -> NAME_OR_SEQMARK
toNameSeqmark (OMV (OMName n :: String
n _)) = let dec :: NAME
dec = String -> NAME
strToToken String
n
in if String -> Bool
isSeqMark String
n
then NAME -> NAME_OR_SEQMARK
SeqMark NAME
dec
else NAME -> NAME_OR_SEQMARK
AS.Name NAME
dec
toNameSeqmark _ = String -> NAME_OR_SEQMARK
forall a. HasCallStack => String -> a
error "toNameSeqmark: only variables allowed"
omdocToTerm :: Env -> OMElement -> TERM
omdocToTerm :: Env -> OMElement -> TERM
omdocToTerm e :: Env
e (OMA (omh :: OMElement
omh : om :: [OMElement]
om))
| OMElement
omh OMElement -> OMElement -> Bool
forall a. Eq a => a -> a -> Bool
== OMElement
const_comment_term
Bool -> Bool -> Bool
&& Bool -> Bool
not ([OMElement] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [OMElement]
om) = let t :: TERM
t : [] = (OMElement -> TERM) -> [OMElement] -> [TERM]
forall a b. (a -> b) -> [a] -> [b]
map (Env -> OMElement -> TERM
omdocToTerm Env
e) ([OMElement] -> [TERM]) -> [OMElement] -> [TERM]
forall a b. (a -> b) -> a -> b
$ [OMElement] -> [OMElement]
forall a. [a] -> [a]
tail [OMElement]
om
in TERM -> COMMENT -> Range -> TERM
Comment_term TERM
t (OMElement -> COMMENT
varToComment (OMElement -> COMMENT) -> OMElement -> COMMENT
forall a b. (a -> b) -> a -> b
$ [OMElement] -> OMElement
forall a. [a] -> a
head [OMElement]
om) Range
nullRange
| OMElement
omh OMElement -> OMElement -> Bool
forall a. Eq a => a -> a -> Bool
== OMElement
const_comment_term = String -> TERM
forall a. HasCallStack => String -> a
error "omdocToTerm: commented term has no comment"
| Bool
otherwise = let th :: TERM
th = Env -> OMElement -> TERM
omdocToTerm Env
e OMElement
omh
ts :: [TERM_SEQ]
ts = (OMElement -> TERM_SEQ) -> [OMElement] -> [TERM_SEQ]
forall a b. (a -> b) -> [a] -> [b]
map (Env -> OMElement -> TERM_SEQ
omdocToTermSeq Env
e) [OMElement]
om
in TERM -> [TERM_SEQ] -> Range -> TERM
Funct_term TERM
th [TERM_SEQ]
ts Range
nullRange
omdocToTerm _ (OMS (_, OMName n :: String
n _)) = NAME -> TERM
Name_term (String -> NAME
strToToken String
n)
omdocToTerm _ (OMV (OMName n :: String
n _)) = NAME -> TERM
Name_term (String -> NAME
strToToken String
n)
omdocToTerm _ om :: OMElement
om = String -> TERM
forall a. HasCallStack => String -> a
error (String -> TERM) -> String -> TERM
forall a b. (a -> b) -> a -> b
$ "omdocToTerm: only applications and symbols allowed, but found: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ OMElement -> String
forall a. Show a => a -> String
show OMElement
om
omdocToTermSeq :: Env -> OMElement -> TERM_SEQ
omdocToTermSeq :: Env -> OMElement -> TERM_SEQ
omdocToTermSeq e :: Env
e om :: OMElement
om@(OMA _) = TERM -> TERM_SEQ
Term_seq (TERM -> TERM_SEQ) -> TERM -> TERM_SEQ
forall a b. (a -> b) -> a -> b
$ Env -> OMElement -> TERM
omdocToTerm Env
e OMElement
om
omdocToTermSeq _ (OMS (_, OMName n :: String
n _)) = let dec :: NAME
dec = String -> NAME
strToToken String
n
in if String -> Bool
isSeqMark String
n
then NAME -> TERM_SEQ
Seq_marks NAME
dec
else TERM -> TERM_SEQ
Term_seq (NAME -> TERM
Name_term NAME
dec)
omdocToTermSeq _ (OMV (OMName n :: String
n _)) = let dec :: NAME
dec = String -> NAME
strToToken String
n
in if String -> Bool
isSeqMark String
n
then NAME -> TERM_SEQ
Seq_marks NAME
dec
else TERM -> TERM_SEQ
Term_seq (NAME -> TERM
Name_term NAME
dec)
omdocToTermSeq _ om :: OMElement
om = String -> TERM_SEQ
forall a. HasCallStack => String -> a
error (String -> TERM_SEQ) -> String -> TERM_SEQ
forall a b. (a -> b) -> a -> b
$ "omdocToTermSeq: only applications, symbols and variables allowed, but found: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ OMElement -> String
forall a. Show a => a -> String
show OMElement
om
strToToken :: String -> Token
strToToken :: String -> NAME
strToToken s :: String
s = String -> Range -> NAME
Token String
s Range
nullRange
isSeqMark :: String -> Bool
isSeqMark :: String -> Bool
isSeqMark ('.' : _) = Bool
True
isSeqMark _ = Bool
False
varToComment :: OMElement -> COMMENT
(OMV (OMName cmt :: String
cmt _)) = String -> Range -> COMMENT
Comment String
cmt Range
nullRange
varToComment om :: OMElement
om = String -> COMMENT
forall a. HasCallStack => String -> a
error (String -> COMMENT) -> String -> COMMENT
forall a b. (a -> b) -> a -> b
$ "varToComment: only OMV OMName supported, but found: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ OMElement -> String
forall a. Show a => a -> String
show OMElement
om