8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova{- |

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina SojakovaModule : $Header$

cb5d588c4c3b286cc1e7210335d6ef7f584d79bcKristina SojakovaCopyright : (c) Klaus L�ttich, Uni Bremen 2002-2004

097b7fb3f8f90e87120d30bf37a1d89fe0ddfaf0Kristina SojakovaLicence : similar to LGPL, see HetCATS/LICENCE.txt or LIZENZ.txt

211c5fb252e0a776baad9a4857ab198659289a4aKristina Sojakova

211c5fb252e0a776baad9a4857ab198659289a4aKristina SojakovaMaintainer : hets@tzi.de

211c5fb252e0a776baad9a4857ab198659289a4aKristina SojakovaStability : provisional

211c5fb252e0a776baad9a4857ab198659289a4aKristina SojakovaPortability : portable

211c5fb252e0a776baad9a4857ab198659289a4aKristina Sojakova

211c5fb252e0a776baad9a4857ab198659289a4aKristina Sojakova Here is the place where the class Logic is instantiated for CASL.

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova Also the instances for Syntax an Category.

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova-}

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovamodule CASL.Logic_CASL(module CASL.Logic_CASL, CASLSign, CASLMor) where

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovaimport CASL.AS_Basic_CASL

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovaimport CASL.LaTeX_CASL

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovaimport CASL.Parse_AS_Basic

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovaimport CASL.SymbolParser

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovaimport CASL.MapSentence

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovaimport CASL.Amalgamability

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovaimport Common.AS_Annotation

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovaimport Common.AnnoState(emptyAnnos)

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovaimport Common.Lib.Parsec

45caf47cd6ed07be0637f6c51e4735512ce9d83aKristina Sojakovaimport Logic.Logic

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovaimport Common.Lexer((<<))

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakovaimport CASL.ATC_CASL

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakovaimport CASL.Sublogic

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovaimport CASL.Sign

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakovaimport CASL.StaticAna

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakovaimport CASL.Morphism

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakovaimport CASL.SymbolMapAnalysis

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovaimport CASL.CCC.FreeTypes

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovaimport Data.Dynamic

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovaimport Common.DynamicUtils

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakovaimport CASL.CCC.OnePoint

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakovaimport Options

cb5d588c4c3b286cc1e7210335d6ef7f584d79bcKristina Sojakova

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakovadata CASL = CASL deriving Show

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakovainstance Language CASL where

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova description _ =

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova "CASL - the Common algebraic specification language\n\

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova \This logic is subsorted partial first-order logic with sort generation constraints\n\

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova \See the CASL User Manual, LNCS 2900\n\

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova \and the CASL Reference Manual, LNCS 2960\n\

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova \See also http://www.cofi.info/CASL.html"

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakovatype CASLBasicSpec = BASIC_SPEC () () ()

cb5d588c4c3b286cc1e7210335d6ef7f584d79bcKristina Sojakovatype CASLFORMULA = FORMULA ()

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova-- Following types are imported from CASL.Amalgamability:

81d28e8372831ae5e6054d8d2212f0114b09b79aKristina Sojakova-- type CASLSign = Sign () ()

81d28e8372831ae5e6054d8d2212f0114b09b79aKristina Sojakova-- type CASLMor = Morphism () () ()

cb5d588c4c3b286cc1e7210335d6ef7f584d79bcKristina Sojakova

cb5d588c4c3b286cc1e7210335d6ef7f584d79bcKristina Sojakovadummy :: a -> b -> ()

cb5d588c4c3b286cc1e7210335d6ef7f584d79bcKristina Sojakovadummy _ _ = ()

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina SojakovatrueC :: a -> b -> Bool

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina SojakovatrueC _ _ = True

cb5d588c4c3b286cc1e7210335d6ef7f584d79bcKristina Sojakova

cb5d588c4c3b286cc1e7210335d6ef7f584d79bcKristina Sojakova-- simplify_sen :: lid -> sign -> sentence -> sentence

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina SojakovasimplifySen :: (Sign f e -> a -> a) -> Sign f e -> FORMULA a -> FORMULA a

cb5d588c4c3b286cc1e7210335d6ef7f584d79bcKristina SojakovasimplifySen e_func sign form =

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova case form of

cb5d588c4c3b286cc1e7210335d6ef7f584d79bcKristina Sojakova ExtFORMULA f -> ExtFORMULA $ e_func sign f

81d28e8372831ae5e6054d8d2212f0114b09b79aKristina Sojakova _ -> form

81d28e8372831ae5e6054d8d2212f0114b09b79aKristina Sojakova

cb5d588c4c3b286cc1e7210335d6ef7f584d79bcKristina Sojakova-- Typeable instance

81d28e8372831ae5e6054d8d2212f0114b09b79aKristina Sojakovatc_BASIC_SPEC, tc_SYMB_ITEMS, tc_SYMB_MAP_ITEMS, casl_SublocigsTc,

81d28e8372831ae5e6054d8d2212f0114b09b79aKristina Sojakova sentenceTc, signTc, morphismTc, symbolTc, rawSymbolTc :: TyCon

81d28e8372831ae5e6054d8d2212f0114b09b79aKristina Sojakova

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakovacasl_SublocigsTc = mkTyCon "CASL.Sublogics.CASL_Sublogics"

81d28e8372831ae5e6054d8d2212f0114b09b79aKristina Sojakovatc_BASIC_SPEC = mkTyCon "CASL.AS_Basic_CASL.BASIC_SPEC"

cb5d588c4c3b286cc1e7210335d6ef7f584d79bcKristina Sojakovatc_SYMB_ITEMS = mkTyCon "CASL.AS_Basic_CASL.SYMB_ITEMS"

81d28e8372831ae5e6054d8d2212f0114b09b79aKristina Sojakovatc_SYMB_MAP_ITEMS = mkTyCon "CASL.AS_Basic_CASL.SYMB_MAP_ITEMS"

81d28e8372831ae5e6054d8d2212f0114b09b79aKristina SojakovasentenceTc = mkTyCon "CASL.AS_Basic_CASL.FORMULA"

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovasignTc = mkTyCon "CASL.Morphism.Sign"

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina SojakovamorphismTc = mkTyCon "CASL.Morphism.Morphism"

f2f62e61c66f678b0042d1a772ff89849d8b2113Kristina SojakovasymbolTc = mkTyCon "CASL.Morphism.Symbol"

f2f62e61c66f678b0042d1a772ff89849d8b2113Kristina SojakovarawSymbolTc = mkTyCon "CASL.Morphism.RawSymbol"

f2f62e61c66f678b0042d1a772ff89849d8b2113Kristina Sojakova

f2f62e61c66f678b0042d1a772ff89849d8b2113Kristina Sojakovainstance (Typeable b, Typeable s, Typeable f)

f2f62e61c66f678b0042d1a772ff89849d8b2113Kristina Sojakova => Typeable (BASIC_SPEC b s f) where

f2f62e61c66f678b0042d1a772ff89849d8b2113Kristina Sojakova typeOf b = mkTyConApp tc_BASIC_SPEC

f2f62e61c66f678b0042d1a772ff89849d8b2113Kristina Sojakova [typeOf $ (undefined :: BASIC_SPEC b s f -> b) b,

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova typeOf $ (undefined :: BASIC_SPEC b s f -> s) b,

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova typeOf $ (undefined :: BASIC_SPEC b s f -> f) b]

887a1999374d1fb3a534e602a8d322de6ef4c8e8Kristina Sojakovainstance Typeable SYMB_ITEMS where

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova typeOf _ = mkTyConApp tc_SYMB_ITEMS []

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovainstance Typeable SYMB_MAP_ITEMS where

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova typeOf _ = mkTyConApp tc_SYMB_MAP_ITEMS []

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovainstance Typeable f => Typeable (FORMULA f) where

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova typeOf f = mkTyConApp sentenceTc

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova [typeOf $ (undefined :: FORMULA f -> f) f]

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovainstance (Typeable f, Typeable e) => Typeable (Sign f e) where

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova typeOf s = mkTyConApp signTc

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova [typeOf $ (undefined :: Sign f e -> f) s,

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova typeOf $ (undefined :: Sign f e -> e) s]

887a1999374d1fb3a534e602a8d322de6ef4c8e8Kristina Sojakovainstance (Typeable e, Typeable f, Typeable m) =>

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova Typeable (Morphism f e m) where

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova typeOf m = mkTyConApp morphismTc

887a1999374d1fb3a534e602a8d322de6ef4c8e8Kristina Sojakova [typeOf $ (undefined :: Morphism f e m -> f) m,

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova typeOf $ (undefined :: Morphism f e m -> e) m,

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova typeOf $ (undefined :: Morphism f e m -> m) m]

887a1999374d1fb3a534e602a8d322de6ef4c8e8Kristina Sojakovainstance Typeable Symbol where

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova typeOf _ = mkTyConApp symbolTc []

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovainstance Typeable RawSymbol where

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova typeOf _ = mkTyConApp rawSymbolTc []

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovainstance Typeable CASL_Sublogics where

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova typeOf _ = mkTyConApp casl_SublocigsTc []

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

887a1999374d1fb3a534e602a8d322de6ef4c8e8Kristina Sojakovainstance Category CASL CASLSign CASLMor

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova where

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova -- ide :: id -> object -> morphism

887a1999374d1fb3a534e602a8d322de6ef4c8e8Kristina Sojakova ide CASL = idMor dummy

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova -- comp :: id -> morphism -> morphism -> Maybe morphism

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova comp CASL = compose (const id)

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova -- dom, cod :: id -> morphism -> object

887a1999374d1fb3a534e602a8d322de6ef4c8e8Kristina Sojakova dom CASL = msource

887a1999374d1fb3a534e602a8d322de6ef4c8e8Kristina Sojakova cod CASL = mtarget

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova -- legal_obj :: id -> object -> Bool

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova legal_obj CASL = legalSign

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova -- legal_mor :: id -> morphism -> Bool

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova legal_mor CASL = legalMor

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova-- abstract syntax, parsing (and printing)

887a1999374d1fb3a534e602a8d322de6ef4c8e8Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovainstance Syntax CASL CASLBasicSpec

887a1999374d1fb3a534e602a8d322de6ef4c8e8Kristina Sojakova SYMB_ITEMS SYMB_MAP_ITEMS

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova where

345d3dcc9f809776009851c446916fc770aa428dKristina Sojakova parse_basic_spec CASL = Just $ basicSpec []

345d3dcc9f809776009851c446916fc770aa428dKristina Sojakova parse_symb_items CASL = Just $ symbItems []

cb5d588c4c3b286cc1e7210335d6ef7f584d79bcKristina Sojakova parse_symb_map_items CASL = Just $ symbMapItems []

345d3dcc9f809776009851c446916fc770aa428dKristina Sojakova

345d3dcc9f809776009851c446916fc770aa428dKristina Sojakova-- lattices (for sublogics)

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

45caf47cd6ed07be0637f6c51e4735512ce9d83aKristina Sojakovainstance LatticeWithTop CASL_Sublogics where

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova -- meet, join :: l -> l -> l

45caf47cd6ed07be0637f6c51e4735512ce9d83aKristina Sojakova meet = CASL.Sublogic.sublogics_min

cb5d588c4c3b286cc1e7210335d6ef7f584d79bcKristina Sojakova join = CASL.Sublogic.sublogics_max

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova -- top :: l

45caf47cd6ed07be0637f6c51e4735512ce9d83aKristina Sojakova top = CASL.Sublogic.top

45caf47cd6ed07be0637f6c51e4735512ce9d83aKristina Sojakova

45caf47cd6ed07be0637f6c51e4735512ce9d83aKristina Sojakova-- CASL logic

45caf47cd6ed07be0637f6c51e4735512ce9d83aKristina Sojakova

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakovainstance Sentences CASL CASLFORMULA () CASLSign CASLMor Symbol where

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova map_sen CASL = mapSen (const return)

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova parse_sentence CASL = Just

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova ( \ _sign str ->

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova case runParser (aFormula [] << eof) emptyAnnos "" str of

cb5d588c4c3b286cc1e7210335d6ef7f584d79bcKristina Sojakova Right x -> return $ item x

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova Left err -> fail $ show err )

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova sym_of CASL = symOf

f2f62e61c66f678b0042d1a772ff89849d8b2113Kristina Sojakova symmap_of CASL = morphismToSymbMap

f2f62e61c66f678b0042d1a772ff89849d8b2113Kristina Sojakova sym_name CASL = symName

f2f62e61c66f678b0042d1a772ff89849d8b2113Kristina Sojakova consCheck CASL = checkFreeType

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova simplify_sen CASL = simplifySen dummy

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova

f2f62e61c66f678b0042d1a772ff89849d8b2113Kristina Sojakovainstance StaticAnalysis CASL CASLBasicSpec CASLFORMULA ()

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova SYMB_ITEMS SYMB_MAP_ITEMS

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova CASLSign

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova CASLMor

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova Symbol RawSymbol where

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova basic_analysis CASL = Just $ basicAnalysis

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova (const $ const return)

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova (const return)

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova (const return) const

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova stat_symb_map_items CASL = statSymbMapItems

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova stat_symb_items CASL = statSymbItems

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova -- ensures_amalgamability :: id

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova -- -> (Diagram CASLSign CASLMor, Node, CASLSign, LEdge CASLMor, CASLMor)

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova -- -> Result (Diagram CASLSign CASLMor)

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova ensures_amalgamability CASL (opts, diag, sink, desc) =

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova ensuresAmalgamability opts diag sink desc

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova sign_to_basic_spec CASL _sigma _sens = Basic_spec [] -- ???

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

45caf47cd6ed07be0637f6c51e4735512ce9d83aKristina Sojakova symbol_to_raw CASL = symbolToRaw

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova id_to_raw CASL = idToRaw

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova matches CASL = CASL.Morphism.matches

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova empty_signature CASL = emptySign ()

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova signature_union CASL sigma1 sigma2 =

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova return $ addSig dummy sigma1 sigma2

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova morphism_union CASL = morphismUnion (const id) dummy

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova final_union CASL = finalUnion dummy

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova is_subsig CASL = isSubSig trueC

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova inclusion CASL = sigInclusion dummy trueC

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova cogenerated_sign CASL = cogeneratedSign dummy

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova generated_sign CASL = generatedSign dummy

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova induced_from_morphism CASL = inducedFromMorphism dummy

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova induced_from_to_morphism CASL = inducedFromToMorphism dummy trueC

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovainstance Logic CASL CASL.Sublogic.CASL_Sublogics

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova CASLSign

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova CASLMor

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova Symbol RawSymbol () where

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova sublogic_names CASL = CASL.Sublogic.sublogics_name

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova all_sublogics CASL = CASL.Sublogic.sublogics_all

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova data_logic CASL = Nothing

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova is_in_basic_spec CASL = CASL.Sublogic.in_basic_spec

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova is_in_sentence CASL = CASL.Sublogic.in_sentence

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova is_in_symb_items CASL = CASL.Sublogic.in_symb_items

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova is_in_symb_map_items CASL = CASL.Sublogic.in_symb_map_items

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova is_in_sign CASL = CASL.Sublogic.in_sign

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova is_in_morphism CASL = CASL.Sublogic.in_morphism

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova is_in_symbol CASL = CASL.Sublogic.in_symbol

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova min_sublogic_basic_spec CASL = CASL.Sublogic.sl_basic_spec

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova min_sublogic_sentence CASL = CASL.Sublogic.sl_sentence

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova min_sublogic_symb_items CASL = CASL.Sublogic.sl_symb_items

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova min_sublogic_symb_map_items CASL = CASL.Sublogic.sl_symb_map_items

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova min_sublogic_sign CASL = CASL.Sublogic.sl_sign

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova min_sublogic_morphism CASL = CASL.Sublogic.sl_morphism

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova min_sublogic_symbol CASL = CASL.Sublogic.sl_symbol

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova proj_sublogic_basic_spec CASL = CASL.Sublogic.pr_basic_spec

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova proj_sublogic_symb_items CASL = CASL.Sublogic.pr_symb_items

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova proj_sublogic_symb_map_items CASL = CASL.Sublogic.pr_symb_map_items

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova proj_sublogic_sign CASL = CASL.Sublogic.pr_sign

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova proj_sublogic_morphism CASL = CASL.Sublogic.pr_morphism

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova proj_sublogic_epsilon CASL = CASL.Sublogic.pr_epsilon dummy

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova proj_sublogic_symbol CASL = CASL.Sublogic.pr_symbol

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova