Logic_ConstraintCASL.hs revision aef85341cfb8e8d26e43d810718f876ddfeb43e9
57221209d11b05aa0373cc3892d5df89ba96ebf9Christian MaederModule : $Header$
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederCopyright : (c) Klaus L�ttich, Uni Bremen 2002-2005
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
1549f3abf73c1122acff724f718b615c82fa3648Till MossakowskiMaintainer : till@tzi.de
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuStability : provisional
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederPortability : portable
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederHere is the place where the class Logic is instantiated for CASL.
351145cfe8c03b4d47133c96b209f2bd6cfbf504Christian Maeder Also the instances for Syntax an Category.
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder real implementation for map_sen
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maedermodule ConstraintCASL.Logic_ConstraintCASL(module ConstraintCASL.Logic_ConstraintCASL, CASLSign, ConstraintCASLMor) where
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maederdata ConstraintCASL = ConstraintCASL deriving Show
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maederinstance Language ConstraintCASL where
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder description _ =
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder "ConstraintCASL - a restriction of CASL to constraint\
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder \formulas over predicates"
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder-- dummy of "Min f e"
351391e0e3226210e7ffb183b334da9f96de36eaChristian MaederdummyMin :: b -> c -> Result ()
351391e0e3226210e7ffb183b334da9f96de36eaChristian MaederdummyMin _ _ = Result {diags = [], maybeResult = Just ()}
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maederinstance Category ConstraintCASL ConstraintCASLSign ConstraintCASLMor
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder -- ide :: id -> object -> morphism
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder ide ConstraintCASL = idMor dummy
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder -- comp :: id -> morphism -> morphism -> Maybe morphism
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder comp ConstraintCASL = compose (const id)
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder -- dom, cod :: id -> morphism -> object
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder dom ConstraintCASL = msource
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder cod ConstraintCASL = mtarget
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder -- legal_obj :: id -> object -> Bool
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder legal_obj ConstraintCASL = legalSign
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder -- legal_mor :: id -> morphism -> Bool
f8b715ab2993083761c0aedb78f1819bcf67b6ccChristian Maeder legal_mor ConstraintCASL = legalMor
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder-- abstract syntax, parsing (and printing)
ad270004874ce1d0697fb30d7309f180553bb315Christian Maederinstance Syntax ConstraintCASL ConstraintCASLBasicSpec
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder SYMB_ITEMS SYMB_MAP_ITEMS
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang parse_basic_spec ConstraintCASL = Just $ basicSpec constraintKeywords
23a00c966f2aa8da525d7a7c51933c99964426c0Christian Maeder parse_symb_items ConstraintCASL = Just $ symbItems []
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder parse_symb_map_items ConstraintCASL = Just $ symbMapItems []
8e9c3881fb6e710b1e08bf5ac8ff9d393df2e74eChristian Maeder-- lattices (for sublogics) is missing
8c63cd89ef840cd7a3d3b75f0207dc800388c800Christian Maederinstance Sentences ConstraintCASL ConstraintCASLFORMULA () ConstraintCASLSign ConstraintCASLMor Symbol where
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder map_sen ConstraintCASL m = return . mapSen (\ _ -> id) m
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder parse_sentence ConstraintCASL = Just (fmap item (aFormula [] << eof))
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder sym_of ConstraintCASL = symOf
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski symmap_of ConstraintCASL = morphismToSymbMap
aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maeder sym_name ConstraintCASL = symName
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder conservativityCheck ConstraintCASL th mor phis =
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder error "conservativityCheck ConstraintCASL nyi"
90c174bac60a72ffd81bc3bf5ae2dd9a61943b8bChristian Maeder -- fmap (fmap fst) (checkFreeType th mor phis)
2561b4bfc45d280ee2be8a7870314670e4e682e4Christian Maeder simplify_sen ConstraintCASL =
ca020e82eb3567e7bdbb1cf70729efbd07e9caa4Klaus Luettich error "simplify_sen ConstraintCASL nyi" -- simplifySen dummyMin dummy
ca020e82eb3567e7bdbb1cf70729efbd07e9caa4Klaus Luettichinstance StaticAnalysis ConstraintCASL ConstraintCASLBasicSpec ConstraintCASLFORMULA ()
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder SYMB_ITEMS SYMB_MAP_ITEMS
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski ConstraintCASLSign
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder ConstraintCASLMor
c7e03d0708369f944b6f235057b39142a21599f2Mihai Codescu Symbol RawSymbol where
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder basic_analysis ConstraintCASL = Just basicConstraintCASLAnalysis
986d3f255182539098a97ac86da9eeee5b7a72e3Christian Maeder stat_symb_map_items ConstraintCASL = statSymbMapItems
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder stat_symb_items ConstraintCASL = statSymbItems
8e80792f474d154ff11762fac081a422e34f1accChristian Maeder ensures_amalgamability ConstraintCASL (opts, diag, sink, desc) =
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder error "ConstraintCASL.ensures_amalgamability not yet implemented"
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder --ensuresAmalgamability opts diag sink desc
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder sign_to_basic_spec ConstraintCASL _sigma _sens = Basic_spec [] -- ???
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder symbol_to_raw ConstraintCASL = symbolToRaw
16e124196c6b204769042028c74f533509c9b5d3Christian Maeder id_to_raw ConstraintCASL = idToRaw
4c7f058cdd19ce67b2b5d4b7f69703d0f8a21e38Christian Maeder matches ConstraintCASL = CASL.Morphism.matches
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian Maeder is_transportable ConstraintCASL = isSortInjective
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian Maeder empty_signature ConstraintCASL = emptySign ()
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian Maeder signature_union ConstraintCASL sigma1 sigma2 =
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian Maeder return $ addSig dummy sigma1 sigma2
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian Maeder morphism_union ConstraintCASL = morphismUnion (const id) dummy
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian Maeder final_union ConstraintCASL = finalUnion dummy
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian Maeder is_subsig ConstraintCASL = isSubSig trueC
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian Maeder inclusion ConstraintCASL = sigInclusion dummy trueC
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian Maeder cogenerated_sign ConstraintCASL = cogeneratedSign dummy
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maeder generated_sign ConstraintCASL = generatedSign dummy
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maeder induced_from_morphism ConstraintCASL = inducedFromMorphism dummy
e6dccba746efe07338d3107fed512e713fd50b28Christian Maeder induced_from_to_morphism ConstraintCASL = inducedFromToMorphism dummy trueC
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maeder theory_to_taxonomy ConstraintCASL =
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder error "theory_to_taxonomy ConstraintCASL nyi" -- convTaxo
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maederinstance Logic ConstraintCASL CASL.Sublogic.CASL_Sublogics
351145cfe8c03b4d47133c96b209f2bd6cfbf504Christian Maeder ConstraintCASLBasicSpec ConstraintCASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS
d5833d2ee7bafcbf2fdd2bdfd9a728c769b100c7Christian Maeder ConstraintCASLSign
d5833d2ee7bafcbf2fdd2bdfd9a728c769b100c7Christian Maeder ConstraintCASLMor
9a6779c8495854bdf36e4a87f98f095e8d0a6e45Christian Maeder Symbol RawSymbol () where
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder stability _ = Experimental
81101b83a042f5a1bdeeef93b1b49aff05817e44Christian Maeder sublogic_names ConstraintCASL = CASL.Sublogic.sublogics_name
351145cfe8c03b4d47133c96b209f2bd6cfbf504Christian Maeder all_sublogics ConstraintCASL = CASL.Sublogic.sublogics_all
d5833d2ee7bafcbf2fdd2bdfd9a728c769b100c7Christian Maeder data_logic ConstraintCASL = Nothing
81101b83a042f5a1bdeeef93b1b49aff05817e44Christian Maeder is_in_basic_spec ConstraintCASL = CASL.Sublogic.in_basic_spec
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder is_in_sentence ConstraintCASL = CASL.Sublogic.in_sentence
351145cfe8c03b4d47133c96b209f2bd6cfbf504Christian Maeder is_in_symb_items ConstraintCASL = CASL.Sublogic.in_symb_items
d5833d2ee7bafcbf2fdd2bdfd9a728c769b100c7Christian Maeder is_in_symb_map_items ConstraintCASL = CASL.Sublogic.in_symb_map_items
81101b83a042f5a1bdeeef93b1b49aff05817e44Christian Maeder is_in_sign ConstraintCASL = CASL.Sublogic.in_sign
81101b83a042f5a1bdeeef93b1b49aff05817e44Christian Maeder is_in_morphism ConstraintCASL = CASL.Sublogic.in_morphism
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maeder is_in_symbol ConstraintCASL = CASL.Sublogic.in_symbol
d0c66a832d7b556e20ea4af4852cdc27a5463d51Christian Maeder min_sublogic_basic_spec ConstraintCASL = CASL.Sublogic.sl_basic_spec
d0c66a832d7b556e20ea4af4852cdc27a5463d51Christian Maeder min_sublogic_sentence ConstraintCASL = CASL.Sublogic.sl_sentence
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder min_sublogic_symb_items ConstraintCASL = CASL.Sublogic.sl_symb_items
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder min_sublogic_symb_map_items ConstraintCASL = CASL.Sublogic.sl_symb_map_items
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder min_sublogic_sign ConstraintCASL = CASL.Sublogic.sl_sign
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder min_sublogic_morphism ConstraintCASL = CASL.Sublogic.sl_morphism
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder min_sublogic_symbol ConstraintCASL = CASL.Sublogic.sl_symbol
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder proj_sublogic_basic_spec ConstraintCASL = CASL.Sublogic.pr_basic_spec
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder proj_sublogic_symb_items ConstraintCASL = CASL.Sublogic.pr_symb_items
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder proj_sublogic_symb_map_items ConstraintCASL = CASL.Sublogic.pr_symb_map_items
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder proj_sublogic_sign ConstraintCASL = CASL.Sublogic.pr_sign
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder proj_sublogic_morphism ConstraintCASL = CASL.Sublogic.pr_morphism
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder proj_sublogic_epsilon ConstraintCASL = CASL.Sublogic.pr_epsilon dummy
fa167e362877db231378e17ba49c66fbb84862fcChristian Maeder proj_sublogic_symbol ConstraintCASL = CASL.Sublogic.pr_symbol