CASL_DL2CASL.hs revision 9ecf13b5fd914bc7272f1fc17348d7f4a8c77061
09249711700a6acbc40a2e337688b434d7aafa28Christian MaederDescription : Inclusion of CASL_DL into CASL
76647324ed70f33b95a881b536d883daccf9568dChristian MaederCopyright : (c) Uni Bremen 2007
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt
3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederMaintainer : luecke@informatik.uni-bremen.de
abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian MaederStability : provisional
76647324ed70f33b95a881b536d883daccf9568dChristian MaederPortability : non-portable (via Logic.Logic)
e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maeder CASL_DL2CASL(..)
10b02b2343246df6773585636fe3ddbefa3b6a1bChristian Maederimport qualified Common.Lib.Rel as Rel
0a39036fa485579a7b7c81cdd44a412392571927Christian Maeder--CASL_DL = domain
d48085f765fca838c1d972d2123601997174583dChristian Maeder--CASL = codomain
a39a820684c1974350f46593025e0bb279f41bc6Christian Maederimport CASL.Sublogic as Sublogic
76647324ed70f33b95a881b536d883daccf9568dChristian Maederimport qualified Data.Set as Set
d48085f765fca838c1d972d2123601997174583dChristian Maederdata CASL_DL2CASL = CASL_DL2CASL deriving Show
d48085f765fca838c1d972d2123601997174583dChristian Maederinstance Language CASL_DL2CASL
05ae87b9efa19655024b0b6ac344d250b96567cdChristian Maederinstance Comorphism
d48085f765fca838c1d972d2123601997174583dChristian Maeder CASL_DL2CASL -- comorphism
793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder CASL_DL -- lid domain
a716971174535184da7713ed308423e355a4aa66Christian Maeder CASL_DL_SL -- sublogics domain
793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder DL_BASIC_SPEC -- Basic spec domain
793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder DLFORMULA -- sentence domain
5e5c3fbbf8c22b883d551d83429b9f8d8041f1e0Christian Maeder SYMB_ITEMS -- symbol items domain
feab655b0275874012c3cf9859064c177860cc70Christian Maeder SYMB_MAP_ITEMS -- symbol map items domain
f2c2b420e386a90d940c758c631d16f12952d2b7Christian Maeder DLSign -- signature domain
f2c2b420e386a90d940c758c631d16f12952d2b7Christian Maeder DLMor -- morphism domain
f2c2b420e386a90d940c758c631d16f12952d2b7Christian Maeder Symbol -- symbol domain
793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder RawSymbol -- rawsymbol domain
793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder ProofTree -- proof tree codomain
a716971174535184da7713ed308423e355a4aa66Christian Maeder CASL -- lid codomain
a716971174535184da7713ed308423e355a4aa66Christian Maeder CASL_Sublogics -- sublogics codomain
5e5c3fbbf8c22b883d551d83429b9f8d8041f1e0Christian Maeder CASLBasicSpec -- Basic spec codomain
a716971174535184da7713ed308423e355a4aa66Christian Maeder CASLFORMULA -- sentence codomain
a716971174535184da7713ed308423e355a4aa66Christian Maeder SYMB_ITEMS -- symbol items codomain
a716971174535184da7713ed308423e355a4aa66Christian Maeder SYMB_MAP_ITEMS -- symbol map items codomain
a716971174535184da7713ed308423e355a4aa66Christian Maeder CASLSign -- signature codomain
5e5c3fbbf8c22b883d551d83429b9f8d8041f1e0Christian Maeder CASLMor -- morphism codomain
793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder Symbol -- symbol codomain
ee6c748be810b24e3c70ffd74f291c7394e389f5Christian Maeder RawSymbol -- rawsymbol codomain
ee6c748be810b24e3c70ffd74f291c7394e389f5Christian Maeder ProofTree -- proof tree domain
9884c7cef7e5a2c8595d5ef8c7d32b9b44a3fad8Christian Maeder sourceLogic CASL_DL2CASL = CASL_DL
fd2dcd5c071e938c07338fd3a32296819b8a2333Christian Maeder targetLogic CASL_DL2CASL = CASL
fd2dcd5c071e938c07338fd3a32296819b8a2333Christian Maeder sourceSublogic CASL_DL2CASL = SROIQ
fd2dcd5c071e938c07338fd3a32296819b8a2333Christian Maeder mapSublogic CASL_DL2CASL _ = Just $ Sublogic.caslTop
fd2dcd5c071e938c07338fd3a32296819b8a2333Christian Maeder { sub_features = LocFilSub
9884c7cef7e5a2c8595d5ef8c7d32b9b44a3fad8Christian Maeder , cons_features = emptyMapConsFeature }
ee6c748be810b24e3c70ffd74f291c7394e389f5Christian Maeder map_symbol CASL_DL2CASL s = Set.singleton s
ee6c748be810b24e3c70ffd74f291c7394e389f5Christian Maeder map_sentence CASL_DL2CASL = trSentence
ee6c748be810b24e3c70ffd74f291c7394e389f5Christian Maeder map_morphism CASL_DL2CASL = mapMor
ee6c748be810b24e3c70ffd74f291c7394e389f5Christian Maeder map_theory CASL_DL2CASL = trTheory
ee6c748be810b24e3c70ffd74f291c7394e389f5Christian Maeder isInclusionComorphism CASL_DL2CASL = True
ee6c748be810b24e3c70ffd74f291c7394e389f5Christian Maeder has_model_expansion CASL_DL2CASL = True
793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder-- ^ mapping of morphims, we just forget the
d48085f765fca838c1d972d2123601997174583dChristian Maeder-- ^ additional features
793945d4ac7c0f22760589c87af8e71427c76118Christian MaedermapMor :: DLMor -> Result CASLMor
793945d4ac7c0f22760589c87af8e71427c76118Christian MaedermapMor inMor =
793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder ms = trSign $ msource inMor
5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder mt = trSign $ mtarget inMor
793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder sm = sort_map inMor
793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder fm = op_map inMor
a716971174535184da7713ed308423e355a4aa66Christian Maeder pm = pred_map inMor
a716971174535184da7713ed308423e355a4aa66Christian Maeder in return (embedMorphism () ms mt)
a716971174535184da7713ed308423e355a4aa66Christian Maeder { sort_map = sm
67a14e04c885a87e4273a300eef60e680531088cChristian Maeder , op_map = fm
67a14e04c885a87e4273a300eef60e680531088cChristian Maeder , pred_map = pm }
d48085f765fca838c1d972d2123601997174583dChristian Maeder-- ^ we forget additional information in the signature
d48085f765fca838c1d972d2123601997174583dChristian MaederprojectToCASL :: DLSign -> CASLSign
d48085f765fca838c1d972d2123601997174583dChristian MaederprojectToCASL dls = dls
5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder sentences = []
d48085f765fca838c1d972d2123601997174583dChristian Maeder , extendedInfo = ()
d48085f765fca838c1d972d2123601997174583dChristian Maeder-- ^ Thing is established as the TopSort of all sorts
d48085f765fca838c1d972d2123601997174583dChristian Maeder-- ^ defined in the CASL_DL spec, a predefined signature
76647324ed70f33b95a881b536d883daccf9568dChristian MaedertrSign :: DLSign -> CASLSign
d48085f765fca838c1d972d2123601997174583dChristian MaedertrSign inSig =
d48085f765fca838c1d972d2123601997174583dChristian Maeder inC = (projectToCASL inSig) `uniteCASLSign` predefSign
d48085f765fca838c1d972d2123601997174583dChristian Maeder inSorts = sortSet inSig
d48085f765fca838c1d972d2123601997174583dChristian Maeder inData = sortSet dataSig_CASL
d48085f765fca838c1d972d2123601997174583dChristian Maeder sortSet = Set.insert topSort $ Set.insert topSortD $ sortSet inC,
d48085f765fca838c1d972d2123601997174583dChristian Maeder (sortRel inC) inSorts) $
76647324ed70f33b95a881b536d883daccf9568dChristian Maeder Set.delete topSortD inData
35cd0c10843c2cdbbe29f00a2a5d7e5e4f2d0064Christian Maeder-- ^ translation of the signature
d48085f765fca838c1d972d2123601997174583dChristian Maeder-- ^ predefined axioms are added
d48085f765fca838c1d972d2123601997174583dChristian MaederrtrSign :: DLSign -> Result CASLSign
5b1f1d57c75562a7af79e8256f4afa07febe921bChristian MaederrtrSign inSig = return $ trSign inSig
35cd0c10843c2cdbbe29f00a2a5d7e5e4f2d0064Christian Maeder-- Translation of theories
35cd0c10843c2cdbbe29f00a2a5d7e5e4f2d0064Christian MaedertrTheory :: (DLSign, [Named (FORMULA DL_FORMULA)]) ->
35cd0c10843c2cdbbe29f00a2a5d7e5e4f2d0064Christian Maeder Result (CASLSign, [Named (FORMULA ())])
35cd0c10843c2cdbbe29f00a2a5d7e5e4f2d0064Christian MaedertrTheory (inSig, inForms) =
35cd0c10843c2cdbbe29f00a2a5d7e5e4f2d0064Christian Maeder outForms <- mapR (\x -> trNamedSentence inSig x) inForms
76647324ed70f33b95a881b536d883daccf9568dChristian Maeder outSig <- rtrSign inSig
d48085f765fca838c1d972d2123601997174583dChristian Maeder return (outSig, predefinedAxioms ++ outForms)
d48085f765fca838c1d972d2123601997174583dChristian Maeder-- ^ translation of named sentences
d48085f765fca838c1d972d2123601997174583dChristian MaedertrNamedSentence :: DLSign -> Named (FORMULA DL_FORMULA) ->
76647324ed70f33b95a881b536d883daccf9568dChristian Maeder Result (Named (FORMULA ()))
d48085f765fca838c1d972d2123601997174583dChristian MaedertrNamedSentence inSig inForm =
3eb7ebab2dd79ac5277f087b18e8f05b9e9f0f9bChristian Maeder inAttL = senAttr inForm
3eb7ebab2dd79ac5277f087b18e8f05b9e9f0f9bChristian Maeder isAxL = isAxiom inForm
81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder isDefL = isDef inForm
d976ba42e9d48c289f9c73147669c7e57b7aa98eChristian Maeder wasThL = wasTheorem inForm
3eb7ebab2dd79ac5277f087b18e8f05b9e9f0f9bChristian Maeder simpAL = simpAnno inForm
3eb7ebab2dd79ac5277f087b18e8f05b9e9f0f9bChristian Maeder inSenL = sentence inForm
81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder outSen <- trSentence inSig inSenL
d976ba42e9d48c289f9c73147669c7e57b7aa98eChristian Maeder return SenAttr
6b1153c560b677f9f5da2a60ee8a10de75ff90c5Christian Maeder senAttr = inAttL
d976ba42e9d48c289f9c73147669c7e57b7aa98eChristian Maeder , isAxiom = isAxL
81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder , isDef = isDefL
76647324ed70f33b95a881b536d883daccf9568dChristian Maeder , wasTheorem = wasThL
81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder , simpAnno = simpAL
81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder , sentence = outSen
81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder-- ^ translation of sentences
81946e2b3f6dde6167f48769bd02c7a634736856Christian MaedertrSentence :: DLSign -> FORMULA DL_FORMULA -> Result (FORMULA ())
76647324ed70f33b95a881b536d883daccf9568dChristian MaedertrSentence inSig inF =
81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder Quantification qf vs frm rn ->
a39a820684c1974350f46593025e0bb279f41bc6Christian Maeder outF <- trSentence inSig frm
72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder return (Quantification qf vs (outF) rn)
a39a820684c1974350f46593025e0bb279f41bc6Christian Maeder Conjunction fns rn ->
d48085f765fca838c1d972d2123601997174583dChristian Maeder outF <- mapR (\x -> trSentence inSig x) fns
d48085f765fca838c1d972d2123601997174583dChristian Maeder return (Conjunction outF rn)
d48085f765fca838c1d972d2123601997174583dChristian Maeder Disjunction fns rn ->
e47d29b522739fbf08aac80c6faa447dde113fbcChristian Maeder outF <- mapR (\x -> trSentence inSig x) fns
e47d29b522739fbf08aac80c6faa447dde113fbcChristian Maeder return (Disjunction outF rn)
d48085f765fca838c1d972d2123601997174583dChristian Maeder Implication f1 f2 b rn ->
d48085f765fca838c1d972d2123601997174583dChristian Maeder out1 <- trSentence inSig f1
e47d29b522739fbf08aac80c6faa447dde113fbcChristian Maeder out2 <- trSentence inSig f2
d48085f765fca838c1d972d2123601997174583dChristian Maeder return (Implication out1 out2 b rn)
d48085f765fca838c1d972d2123601997174583dChristian Maeder Equivalence f1 f2 rn ->
72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder out1 <- trSentence inSig f1
d48085f765fca838c1d972d2123601997174583dChristian Maeder out2 <- trSentence inSig f2
d48085f765fca838c1d972d2123601997174583dChristian Maeder return (Equivalence out1 out2 rn)
d48085f765fca838c1d972d2123601997174583dChristian Maeder Negation frm rn ->
81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder outF <- trSentence inSig frm
a39a820684c1974350f46593025e0bb279f41bc6Christian Maeder return (Negation outF rn)
a39a820684c1974350f46593025e0bb279f41bc6Christian Maeder True_atom rn -> do return (True_atom rn)
a39a820684c1974350f46593025e0bb279f41bc6Christian Maeder False_atom rn -> do return (False_atom rn)
a39a820684c1974350f46593025e0bb279f41bc6Christian Maeder Predication pr trm rn ->
81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder ot <- mapR (\x -> trTerm inSig x) trm
d48085f765fca838c1d972d2123601997174583dChristian Maeder return (Predication pr ot rn)
35cd0c10843c2cdbbe29f00a2a5d7e5e4f2d0064Christian Maeder Definedness tm rn ->
35cd0c10843c2cdbbe29f00a2a5d7e5e4f2d0064Christian Maeder ot <- trTerm inSig tm
35cd0c10843c2cdbbe29f00a2a5d7e5e4f2d0064Christian Maeder return (Definedness ot rn)
35cd0c10843c2cdbbe29f00a2a5d7e5e4f2d0064Christian Maeder Existl_equation t1 t2 rn ->
81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder ot1 <- trTerm inSig t1
76647324ed70f33b95a881b536d883daccf9568dChristian Maeder ot2 <- trTerm inSig t2
35cd0c10843c2cdbbe29f00a2a5d7e5e4f2d0064Christian Maeder return (Existl_equation ot1 ot2 rn)
81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder Strong_equation t1 t2 rn ->
81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder ot1 <- trTerm inSig t1
81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder ot2 <- trTerm inSig t2
81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder return (Strong_equation ot1 ot2 rn)
5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder Membership t1 st rn ->
a39a820684c1974350f46593025e0bb279f41bc6Christian Maeder ot <- trTerm inSig t1
a39a820684c1974350f46593025e0bb279f41bc6Christian Maeder return (Membership ot st rn)
c9fd6322389afc35c1803a0614f094298bc7cba3Christian Maeder Mixfix_formula trm ->
98c47b3c137bdb20c53b6c1d346c0fb48b48d673Christian Maeder ot <- trTerm inSig trm
81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder return (Mixfix_formula ot)
a39a820684c1974350f46593025e0bb279f41bc6Christian Maeder Unparsed_formula str rn ->
72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder do return (Unparsed_formula str rn)
81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder Sort_gen_ax cstr ft ->
76647324ed70f33b95a881b536d883daccf9568dChristian Maeder do return (Sort_gen_ax cstr ft)
98c47b3c137bdb20c53b6c1d346c0fb48b48d673Christian Maeder ExtFORMULA form ->
c9fd6322389afc35c1803a0614f094298bc7cba3Christian Maeder Cardinality _ _ _ _ _ _ ->
c9fd6322389afc35c1803a0614f094298bc7cba3Christian Maeder fail "Mapping for cardinality expressions not yet implemented"
3eb7ebab2dd79ac5277f087b18e8f05b9e9f0f9bChristian Maeder-- ^ translation of terms
98c47b3c137bdb20c53b6c1d346c0fb48b48d673Christian MaedertrTerm :: DLSign -> TERM DL_FORMULA -> Result (TERM ())
98c47b3c137bdb20c53b6c1d346c0fb48b48d673Christian MaedertrTerm inSig inF =
98c47b3c137bdb20c53b6c1d346c0fb48b48d673Christian Maeder Qual_var v s rn -> return (Qual_var v s rn)
98c47b3c137bdb20c53b6c1d346c0fb48b48d673Christian Maeder Application os tms rn ->
5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder ot <- mapR (\x -> trTerm inSig x) tms
98c47b3c137bdb20c53b6c1d346c0fb48b48d673Christian Maeder return (Application os ot rn)
98c47b3c137bdb20c53b6c1d346c0fb48b48d673Christian Maeder Sorted_term trm st rn ->
17889a13fbcd155040fa0323ffe82393d53051fcChristian Maeder ot <- trTerm inSig trm
17889a13fbcd155040fa0323ffe82393d53051fcChristian Maeder return (Sorted_term ot st rn)
17889a13fbcd155040fa0323ffe82393d53051fcChristian Maeder Cast trm st rn ->
17889a13fbcd155040fa0323ffe82393d53051fcChristian Maeder ot <- trTerm inSig trm
17889a13fbcd155040fa0323ffe82393d53051fcChristian Maeder return (Cast ot st rn)
a39a820684c1974350f46593025e0bb279f41bc6Christian Maeder Conditional t1 frm t2 rn ->
a39a820684c1974350f46593025e0bb279f41bc6Christian Maeder ot1 <- trTerm inSig t1
5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder ot2 <- trTerm inSig t2
81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder of1 <- trSentence inSig frm
a39a820684c1974350f46593025e0bb279f41bc6Christian Maeder return (Conditional ot1 of1 ot2 rn)
81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder Unparsed_term str rn -> do return (Unparsed_term str rn)
81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder Mixfix_qual_pred ps -> do return (Mixfix_qual_pred ps)
35cd0c10843c2cdbbe29f00a2a5d7e5e4f2d0064Christian Maeder Mixfix_term trm ->
81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder ot <- mapR (\x -> trTerm inSig x) trm
81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder return (Mixfix_term ot)
17889a13fbcd155040fa0323ffe82393d53051fcChristian Maeder Mixfix_token tok -> do return (Mixfix_token tok)
17889a13fbcd155040fa0323ffe82393d53051fcChristian Maeder Mixfix_sorted_term st rn -> do return (Mixfix_sorted_term st rn)
17889a13fbcd155040fa0323ffe82393d53051fcChristian Maeder Mixfix_cast st rn -> do return (Mixfix_cast st rn)
5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder Mixfix_parenthesized trm rn ->
17889a13fbcd155040fa0323ffe82393d53051fcChristian Maeder ot <- mapR (\x -> trTerm inSig x) trm
17889a13fbcd155040fa0323ffe82393d53051fcChristian Maeder return (Mixfix_parenthesized ot rn)
17889a13fbcd155040fa0323ffe82393d53051fcChristian Maeder Mixfix_bracketed trm rn ->
81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder ot <- mapR (\x -> trTerm inSig x) trm
81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder return (Mixfix_bracketed ot rn)
81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder Mixfix_braced trm rn ->
e47d29b522739fbf08aac80c6faa447dde113fbcChristian Maeder ot <- mapR (\x -> trTerm inSig x) trm
e47d29b522739fbf08aac80c6faa447dde113fbcChristian Maeder return (Mixfix_braced ot rn)