{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}
module Comorphisms.CASL_DL2CASL
(
CASL_DL2CASL (..)
)
where
import Logic.Logic
import Logic.Comorphism
import Common.AS_Annotation
import Common.ProofTree
import Common.Result
import qualified Common.Lib.Rel as Rel
import CASL_DL.PredefinedCASLAxioms
import CASL_DL.Logic_CASL_DL
import CASL_DL.AS_CASL_DL
import CASL_DL.Sign ()
import CASL_DL.StatAna
import CASL_DL.Sublogics
import CASL.Logic_CASL
import CASL.AS_Basic_CASL
import CASL.Sign
import CASL.Morphism
import CASL.Sublogic as Sublogic
import qualified Data.Set as Set
data CASL_DL2CASL = CASL_DL2CASL deriving Show
instance Language CASL_DL2CASL
instance Comorphism
CASL_DL2CASL
CASL_DL
CASL_DL_SL
DL_BASIC_SPEC
DLFORMULA
SYMB_ITEMS
SYMB_MAP_ITEMS
DLSign
DLMor
Symbol
RawSymbol
ProofTree
CASL
CASL_Sublogics
CASLBasicSpec
CASLFORMULA
SYMB_ITEMS
SYMB_MAP_ITEMS
CASLSign
CASLMor
Symbol
RawSymbol
ProofTree
where
sourceLogic CASL_DL2CASL = CASL_DL
targetLogic CASL_DL2CASL = CASL
sourceSublogic CASL_DL2CASL = SROIQ
mapSublogic CASL_DL2CASL _ = Just $ Sublogic.caslTop
{ sub_features = LocFilSub
, cons_features = emptyMapConsFeature }
map_symbol CASL_DL2CASL _ = Set.singleton
map_sentence CASL_DL2CASL = trSentence
map_morphism CASL_DL2CASL = mapMor
map_theory CASL_DL2CASL = trTheory
isInclusionComorphism CASL_DL2CASL = True
has_model_expansion CASL_DL2CASL = True
mapMor :: DLMor -> Result CASLMor
mapMor inMor =
let
ms = trSign $ msource inMor
mt = trSign $ mtarget inMor
sm = sort_map inMor
fm = op_map inMor
pm = pred_map inMor
in return (embedMorphism () ms mt)
{ sort_map = sm
, op_map = fm
, pred_map = pm }
projectToCASL :: DLSign -> CASLSign
projectToCASL dls = dls
{
sentences = []
, extendedInfo = ()
}
trSign :: DLSign -> CASLSign
trSign inSig =
let
inC = projectToCASL inSig `uniteCASLSign` predefSign
inSorts = sortSet inSig
inData = sortSet predefSign
in
inC
{
sortRel = Rel.insertKey thing
$ Rel.insertKey dataS
$ Set.fold (`Rel.insertDiffPair` dataS)
(Set.fold (`Rel.insertDiffPair` thing)
(sortRel inC) inSorts)
$ Set.delete dataS inData
}
trTheory :: (DLSign, [Named (FORMULA DL_FORMULA)]) ->
Result (CASLSign, [Named (FORMULA ())])
trTheory (inSig, inForms) = do
outForms <- mapR (trNamedSentence inSig) inForms
return (trSign inSig, predefinedAxioms ++ outForms)
trNamedSentence :: DLSign -> Named (FORMULA DL_FORMULA) ->
Result (Named (FORMULA ()))
trNamedSentence inSig inForm = do
outSen <- trSentence inSig $ sentence inForm
return $ mapNamed (const outSen) inForm
trSentence :: DLSign -> FORMULA DL_FORMULA -> Result (FORMULA ())
trSentence inSig inF =
case inF of
Quantification qf vs frm rn ->
do
outF <- trSentence inSig frm
return (Quantification qf vs outF rn)
Junction j fns rn ->
do
outF <- mapR (trSentence inSig) fns
return (Junction j outF rn)
Relation f1 c f2 rn ->
do
out1 <- trSentence inSig f1
out2 <- trSentence inSig f2
return (Relation out1 c out2 rn)
Negation frm rn ->
do
outF <- trSentence inSig frm
return (Negation outF rn)
Atom b rn -> return (Atom b rn)
Predication pr trm rn ->
do
ot <- mapR (trTerm inSig) trm
return (Predication pr ot rn)
Definedness tm rn ->
do
ot <- trTerm inSig tm
return (Definedness ot rn)
Equation t1 e t2 rn ->
do
ot1 <- trTerm inSig t1
ot2 <- trTerm inSig t2
return (Equation ot1 e ot2 rn)
Membership t1 st rn ->
do
ot <- trTerm inSig t1
return (Membership ot st rn)
Mixfix_formula trm ->
do
ot <- trTerm inSig trm
return (Mixfix_formula ot)
Unparsed_formula str rn ->
return (Unparsed_formula str rn)
Sort_gen_ax cstr ft ->
return (Sort_gen_ax cstr ft)
QuantOp {} -> fail "CASL_DL2CASL.QuantOp"
QuantPred {} -> fail "CASL_DL2CASL.QuantPred"
ExtFORMULA form ->
case form of
Cardinality {} ->
fail "Mapping of cardinality not implemented"
trTerm :: DLSign -> TERM DL_FORMULA -> Result (TERM ())
trTerm inSig inF =
case inF of
Qual_var v s rn -> return (Qual_var v s rn)
Application os tms rn ->
do
ot <- mapR (trTerm inSig) tms
return (Application os ot rn)
Sorted_term trm st rn ->
do
ot <- trTerm inSig trm
return (Sorted_term ot st rn)
Cast trm st rn ->
do
ot <- trTerm inSig trm
return (Cast ot st rn)
Conditional t1 frm t2 rn ->
do
ot1 <- trTerm inSig t1
ot2 <- trTerm inSig t2
of1 <- trSentence inSig frm
return (Conditional ot1 of1 ot2 rn)
Unparsed_term str rn -> return (Unparsed_term str rn)
Mixfix_qual_pred ps -> return (Mixfix_qual_pred ps)
Mixfix_term trm ->
do
ot <- mapR (trTerm inSig) trm
return (Mixfix_term ot)
Mixfix_token tok -> return (Mixfix_token tok)
Mixfix_sorted_term st rn -> return (Mixfix_sorted_term st rn)
Mixfix_cast st rn -> return (Mixfix_cast st rn)
Mixfix_parenthesized trm rn ->
do
ot <- mapR (trTerm inSig) trm
return (Mixfix_parenthesized ot rn)
Mixfix_bracketed trm rn ->
do
ot <- mapR (trTerm inSig) trm
return (Mixfix_bracketed ot rn)
Mixfix_braced trm rn ->
do
ot <- mapR (trTerm inSig) trm
return (Mixfix_braced ot rn)
ExtTERM _ -> return $ ExtTERM ()