Logic_CASL.hs revision bec7e681b0ba4d085638ec7af0cf7ae5068840ca
8267b99c0d7a187abe6f87ad50530dc08f5d1cdcAndy GimblettModule : $Header$
bb83db66bd9b3b4ce67be66419daf29886175276Andy GimblettCopyright : (c) Klaus L�ttich, Uni Bremen 2002-2004
33bdce26495121cdbce30331ef90a1969126a840Liam O'ReillyLicence : similar to LGPL, see HetCATS/LICENCE.txt or LIZENZ.txt
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederMaintainer : hets@tzi.de
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus RoggenbachStability : provisional
bb83db66bd9b3b4ce67be66419daf29886175276Andy GimblettPortability : portable
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach Here is the place where the class Logic is instantiated for CASL.
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach Also the instances for Syntax an Category.
78718c37b1a50086a27e0f031db4cf82bea934aeChristian Maedermodule CASL.Logic_CASL(module CASL.Logic_CASL, CASLSign, CASLMor) where
eeaf0a8a1dc535d105904a2190f26c0835ecf429Andy Gimblettimport CASL.CCC.OnePoint -- currently unused
1538a6e8d77301d6de757616ffc69ee61f1482e4Andy Gimblettdata CASL = CASL deriving Show
c4b2418421546a337f83332fe0db04742dcd735dAndy Gimblettinstance Language CASL where
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly description _ =
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly "CASL - the Common algebraic specification language\n\
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly \This logic is subsorted partial first-order logic \
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly \with sort generation constraints\n\
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly \See the CASL User Manual, LNCS 2900, Springer Verlag\n\
e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblett \and the CASL Reference Manual, LNCS 2960, Springer Verlag\n\
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reillytype CASLBasicSpec = BASIC_SPEC () () ()
6caa773a17aa8cb5b6196abbd5ede98ef01beb8aChristian Maedertype CASLFORMULA = FORMULA ()
6caa773a17aa8cb5b6196abbd5ede98ef01beb8aChristian Maeder-- Following types are imported from CASL.Amalgamability:
6caa773a17aa8cb5b6196abbd5ede98ef01beb8aChristian Maeder-- type CASLSign = Sign () ()
6caa773a17aa8cb5b6196abbd5ede98ef01beb8aChristian Maeder-- type CASLMor = Morphism () () ()
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reillydummy :: a -> b -> ()
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reillydummy _ _ = ()
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly-- dummy of "Min f e"
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'ReillydummyMin :: a -> b -> c -> Result ()
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'ReillydummyMin _ _ _ = Result {diags = [], maybeResult = Just ()}
e771539425f4a0abef9f94cf4b63690f3603f682Andy GimbletttrueC :: a -> b -> Bool
e54c5af823b9775dd2c058185ea5bdf7593950faAndy GimbletttrueC _ _ = True
7caf9f99d426a25d56eb7473fea1f55ce4460762Andy Gimblett-- Typeable instance
7caf9f99d426a25d56eb7473fea1f55ce4460762Andy Gimbletttc_BASIC_SPEC, tc_SYMB_ITEMS, tc_SYMB_MAP_ITEMS, casl_SublocigsTc,
7caf9f99d426a25d56eb7473fea1f55ce4460762Andy Gimblett sentenceTc, signTc, morphismTc, symbolTc, rawSymbolTc :: TyCon
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblettcasl_SublocigsTc = mkTyCon "CASL.Sublogics.CASL_Sublogics"
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimbletttc_BASIC_SPEC = mkTyCon "CASL.AS_Basic_CASL.BASIC_SPEC"
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimbletttc_SYMB_ITEMS = mkTyCon "CASL.AS_Basic_CASL.SYMB_ITEMS"
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimbletttc_SYMB_MAP_ITEMS = mkTyCon "CASL.AS_Basic_CASL.SYMB_MAP_ITEMS"
e54c5af823b9775dd2c058185ea5bdf7593950faAndy GimblettsentenceTc = mkTyCon "CASL.AS_Basic_CASL.FORMULA"
e771539425f4a0abef9f94cf4b63690f3603f682Andy GimblettsignTc = mkTyCon "CASL.Morphism.Sign"
e771539425f4a0abef9f94cf4b63690f3603f682Andy GimblettmorphismTc = mkTyCon "CASL.Morphism.Morphism"
eeaf0a8a1dc535d105904a2190f26c0835ecf429Andy GimblettsymbolTc = mkTyCon "CASL.Morphism.Symbol"
eeaf0a8a1dc535d105904a2190f26c0835ecf429Andy GimblettrawSymbolTc = mkTyCon "CASL.Morphism.RawSymbol"
61051521e4d82769a47f23aecb5fb477de47d534Andy Gimblettinstance (Typeable b, Typeable s, Typeable f)
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett => Typeable (BASIC_SPEC b s f) where
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett typeOf b = mkTyConApp tc_BASIC_SPEC
eeaf0a8a1dc535d105904a2190f26c0835ecf429Andy Gimblett [typeOf $ (undefined :: BASIC_SPEC b s f -> b) b,
eeaf0a8a1dc535d105904a2190f26c0835ecf429Andy Gimblett typeOf $ (undefined :: BASIC_SPEC b s f -> s) b,
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett typeOf $ (undefined :: BASIC_SPEC b s f -> f) b]
eeaf0a8a1dc535d105904a2190f26c0835ecf429Andy Gimblettinstance Typeable SYMB_ITEMS where
d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett typeOf _ = mkTyConApp tc_SYMB_ITEMS []
eeaf0a8a1dc535d105904a2190f26c0835ecf429Andy Gimblettinstance Typeable SYMB_MAP_ITEMS where
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett typeOf _ = mkTyConApp tc_SYMB_MAP_ITEMS []
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblettinstance Typeable f => Typeable (FORMULA f) where
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett typeOf f = mkTyConApp sentenceTc
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly [typeOf $ (undefined :: FORMULA f -> f) f]
fbc0c2baf563fe5b664f0152674a8d3acecca58cAndy Gimblettinstance (Typeable f, Typeable e) => Typeable (Sign f e) where
31f039ffdb33d78cb31d24b71d3155b11a323975Andy Gimblett typeOf s = mkTyConApp signTc
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett [typeOf $ (undefined :: Sign f e -> f) s,
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett typeOf $ (undefined :: Sign f e -> e) s]
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblettinstance (Typeable e, Typeable f, Typeable m) =>
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett Typeable (Morphism f e m) where
f4a5178450076ee54f3a9adb4f91e241aea3ba75Christian Maeder typeOf m = mkTyConApp morphismTc
f4a5178450076ee54f3a9adb4f91e241aea3ba75Christian Maeder [typeOf $ (undefined :: Morphism f e m -> f) m,
90047eafd2de482c67bcd13103c6064e9b0cb254Andy Gimblett typeOf $ (undefined :: Morphism f e m -> e) m,
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett typeOf $ (undefined :: Morphism f e m -> m) m]
e8c03c10d7987b223a9f6bfd5c0c54da21da5b86Andy Gimblettinstance Typeable Symbol where
e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblett typeOf _ = mkTyConApp symbolTc []
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblettinstance Typeable RawSymbol where
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett typeOf _ = mkTyConApp rawSymbolTc []
31f039ffdb33d78cb31d24b71d3155b11a323975Andy Gimblettinstance Typeable CASL_Sublogics where
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett typeOf _ = mkTyConApp casl_SublocigsTc []
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblettinstance Category CASL CASLSign CASLMor
4770d29adda064baa5dbfcca03f600d7608806f7Liam O'Reilly -- ide :: id -> object -> morphism
4770d29adda064baa5dbfcca03f600d7608806f7Liam O'Reilly ide CASL = idMor dummy
4770d29adda064baa5dbfcca03f600d7608806f7Liam O'Reilly -- comp :: id -> morphism -> morphism -> Maybe morphism
4770d29adda064baa5dbfcca03f600d7608806f7Liam O'Reilly comp CASL = compose (const id)
4770d29adda064baa5dbfcca03f600d7608806f7Liam O'Reilly -- dom, cod :: id -> morphism -> object
4770d29adda064baa5dbfcca03f600d7608806f7Liam O'Reilly dom CASL = msource
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett cod CASL = mtarget
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett -- legal_obj :: id -> object -> Bool
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett legal_obj CASL = legalSign
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett -- legal_mor :: id -> morphism -> Bool
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett legal_mor CASL = legalMor
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett-- abstract syntax, parsing (and printing)
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblettinstance Syntax CASL CASLBasicSpec
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett SYMB_ITEMS SYMB_MAP_ITEMS
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett parse_basic_spec CASL = Just $ basicSpec []
e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblett parse_symb_items CASL = Just $ symbItems []
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett parse_symb_map_items CASL = Just $ symbMapItems []
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett-- lattices (for sublogics)
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblettinstance LatticeWithTop CASL_Sublogics where
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett -- meet, join :: l -> l -> l
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblettinstance Sentences CASL CASLFORMULA () CASLSign CASLMor Symbol where
31f039ffdb33d78cb31d24b71d3155b11a323975Andy Gimblett map_sen CASL m = return . mapSen (\ _ -> id) m
31f039ffdb33d78cb31d24b71d3155b11a323975Andy Gimblett parse_sentence CASL = Just (fmap item (aFormula [] << eof))
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett sym_of CASL = symOf
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett symmap_of CASL = morphismToSymbMap
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett sym_name CASL = symName
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett consCheck CASL = checkFreeType
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett simplify_sen CASL = simplifySen dummyMin dummy
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reillyinstance StaticAnalysis CASL CASLBasicSpec CASLFORMULA ()
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly SYMB_ITEMS SYMB_MAP_ITEMS
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly Symbol RawSymbol where
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett basic_analysis CASL = Just $ basicCASLAnalysis
4770d29adda064baa5dbfcca03f600d7608806f7Liam O'Reilly stat_symb_map_items CASL = statSymbMapItems
4770d29adda064baa5dbfcca03f600d7608806f7Liam O'Reilly stat_symb_items CASL = statSymbItems
4770d29adda064baa5dbfcca03f600d7608806f7Liam O'Reilly ensures_amalgamability CASL (opts, diag, sink, desc) =
4770d29adda064baa5dbfcca03f600d7608806f7Liam O'Reilly ensuresAmalgamability opts diag sink desc
f4a5178450076ee54f3a9adb4f91e241aea3ba75Christian Maeder sign_to_basic_spec CASL _sigma _sens = Basic_spec [] -- ???
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett symbol_to_raw CASL = symbolToRaw
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett id_to_raw CASL = idToRaw
e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblett empty_signature CASL = emptySign ()
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett signature_union CASL sigma1 sigma2 =
e8c03c10d7987b223a9f6bfd5c0c54da21da5b86Andy Gimblett return $ addSig dummy sigma1 sigma2
e8c03c10d7987b223a9f6bfd5c0c54da21da5b86Andy Gimblett morphism_union CASL = morphismUnion (const id) dummy
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly final_union CASL = finalUnion dummy
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett is_subsig CASL = isSubSig trueC
e8c03c10d7987b223a9f6bfd5c0c54da21da5b86Andy Gimblett inclusion CASL = sigInclusion dummy trueC
e95030058b77cb83593c85aa4c506caf154f63b7Andy Gimblett cogenerated_sign CASL = cogeneratedSign dummy
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly generated_sign CASL = generatedSign dummy
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly induced_from_morphism CASL = inducedFromMorphism dummy
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly induced_from_to_morphism CASL = inducedFromToMorphism dummy trueC
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly theory_to_taxonomy CASL = convTaxo
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reillyinstance Logic CASL CASL.Sublogic.CASL_Sublogics
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly Symbol RawSymbol () where
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly sublogic_names CASL = CASL.Sublogic.sublogics_name
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly all_sublogics CASL = CASL.Sublogic.sublogics_all
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly data_logic CASL = Nothing
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly is_in_basic_spec CASL = CASL.Sublogic.in_basic_spec
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly is_in_sentence CASL = CASL.Sublogic.in_sentence
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly is_in_symb_items CASL = CASL.Sublogic.in_symb_items
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly is_in_symb_map_items CASL = CASL.Sublogic.in_symb_map_items
c60c643bbac58809100f35f187493b6f170314f0Liam O'Reilly is_in_sign CASL = CASL.Sublogic.in_sign
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly is_in_morphism CASL = CASL.Sublogic.in_morphism
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly is_in_symbol CASL = CASL.Sublogic.in_symbol
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly min_sublogic_basic_spec CASL = CASL.Sublogic.sl_basic_spec
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly min_sublogic_sentence CASL = CASL.Sublogic.sl_sentence
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly min_sublogic_symb_items CASL = CASL.Sublogic.sl_symb_items
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly min_sublogic_symb_map_items CASL = CASL.Sublogic.sl_symb_map_items
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly min_sublogic_sign CASL = CASL.Sublogic.sl_sign
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly min_sublogic_morphism CASL = CASL.Sublogic.sl_morphism
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly min_sublogic_symbol CASL = CASL.Sublogic.sl_symbol
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett proj_sublogic_basic_spec CASL = CASL.Sublogic.pr_basic_spec
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett proj_sublogic_symb_items CASL = CASL.Sublogic.pr_symb_items
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett proj_sublogic_symb_map_items CASL = CASL.Sublogic.pr_symb_map_items
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly proj_sublogic_sign CASL = CASL.Sublogic.pr_sign
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly proj_sublogic_morphism CASL = CASL.Sublogic.pr_morphism
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly proj_sublogic_epsilon CASL = CASL.Sublogic.pr_epsilon dummy
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly proj_sublogic_symbol CASL = CASL.Sublogic.pr_symbol