bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder{-# LANGUAGE CPP, MultiParamTypeClasses, TypeSynonymInstances

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder , FlexibleInstances #-}

62ecb1e7f8fd9573eea8369657de12c7bf9f4f25Christian Maeder{- |

97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederModule : $Header$

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian MaederDescription : Instance of class Logic for the CASL logic

b4fbc96e05117839ca409f5f20f97b3ac872d1edTill MossakowskiCopyright : (c) Klaus Luettich, Uni Bremen 2002-2005

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian MaederLicense : GPLv2 or higher, see LICENSE.txt

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder

f3a94a197960e548ecd6520bb768cb0d547457bbChristian MaederMaintainer : till@informatik.uni-bremen.de

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian MaederStability : provisional

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian MaederPortability : non-portable (imports Logic.Logic)

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian MaederInstance of class Logic for the CASL logic

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder Also the instances for Syntax and Category.

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder-}

5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maedermodule CASL.Logic_CASL where

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maederimport ATC.ProofTree ()

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maederimport CASL.AS_Basic_CASL

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maederimport CASL.Parse_AS_Basic

5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maederimport CASL.Kif

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maederimport CASL.Kif2CASL

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maederimport CASL.Fold

5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maederimport CASL.ToDoc

33a5d53a412ba0a4e5847f7538d6da2e22bd116cChristian Maederimport CASL.ToItem (bsToItem)

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maederimport CASL.SymbolParser

e774ab5733a1d673b123b0e63b14dd533e6fd4fcChristian Maederimport CASL.MapSentence

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maederimport CASL.Amalgamability

62ecb1e7f8fd9573eea8369657de12c7bf9f4f25Christian Maederimport CASL.ATC_CASL ()

62ecb1e7f8fd9573eea8369657de12c7bf9f4f25Christian Maederimport CASL.Sublogic as SL

62ecb1e7f8fd9573eea8369657de12c7bf9f4f25Christian Maederimport CASL.Sign

62ecb1e7f8fd9573eea8369657de12c7bf9f4f25Christian Maederimport CASL.StaticAna

62ecb1e7f8fd9573eea8369657de12c7bf9f4f25Christian Maederimport CASL.ColimSign

62ecb1e7f8fd9573eea8369657de12c7bf9f4f25Christian Maederimport CASL.Morphism

62ecb1e7f8fd9573eea8369657de12c7bf9f4f25Christian Maederimport CASL.SymbolMapAnalysis

62ecb1e7f8fd9573eea8369657de12c7bf9f4f25Christian Maederimport CASL.Taxonomy

62ecb1e7f8fd9573eea8369657de12c7bf9f4f25Christian Maederimport CASL.Simplify

62ecb1e7f8fd9573eea8369657de12c7bf9f4f25Christian Maederimport CASL.SimplifySen

62ecb1e7f8fd9573eea8369657de12c7bf9f4f25Christian Maederimport CASL.CCC.FreeTypes

62ecb1e7f8fd9573eea8369657de12c7bf9f4f25Christian Maederimport CASL.CCC.OnePoint () -- currently unused

62ecb1e7f8fd9573eea8369657de12c7bf9f4f25Christian Maederimport CASL.Qualify

717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maederimport CASL.Quantification

717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maederimport qualified CASL.OMDocImport as OMI

62ecb1e7f8fd9573eea8369657de12c7bf9f4f25Christian Maederimport CASL.OMDocExport

62ecb1e7f8fd9573eea8369657de12c7bf9f4f25Christian Maederimport CASL.Freeness

717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder

717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder-- test

717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maederimport CASL.Formula (formula)

62ecb1e7f8fd9573eea8369657de12c7bf9f4f25Christian Maeder

62ecb1e7f8fd9573eea8369657de12c7bf9f4f25Christian Maeder#ifdef UNI_PACKAGE

62ecb1e7f8fd9573eea8369657de12c7bf9f4f25Christian Maederimport CASL.QuickCheck

62ecb1e7f8fd9573eea8369657de12c7bf9f4f25Christian Maeder#endif

62ecb1e7f8fd9573eea8369657de12c7bf9f4f25Christian Maeder

62ecb1e7f8fd9573eea8369657de12c7bf9f4f25Christian Maederimport Common.ProofTree

717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maederimport Common.Consistency

b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maederimport Common.DocUtils

ebcaad207cafc89eeb49d431f40de2ef4c48411cChristian Maeder

b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maederimport Data.Monoid

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maederimport qualified Data.Set as Set

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder

b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maederimport Logic.Logic

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maederdata CASL = CASL deriving Show

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maederinstance Language CASL where

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder description _ = unlines

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder [ "CASL - the Common algebraic specification language"

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder , "This logic is subsorted partial first-order logic"

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder , " with sort generation constraints"

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder , "See the CASL User Manual, LNCS 2900, Springer Verlag"

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder , "and the CASL Reference Manual, LNCS 2960, Springer Verlag"

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder , "See also http://www.cofi.info/CASL.html"

2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder , ""

62ecb1e7f8fd9573eea8369657de12c7bf9f4f25Christian Maeder , "Abbreviations of sublogic names indicate the following feature:"

62ecb1e7f8fd9573eea8369657de12c7bf9f4f25Christian Maeder , " Sub -> with subsorting"

ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian Maeder , " Sul -> with a locally filtered subsort relation"

ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian Maeder , " P -> with partial functions"

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder , " C -> with sort generation constraints"

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder , " eC -> C without renamings"

dfa74d066ea0f00a70276aedecc624c6b3c86deaChristian Maeder , " sC -> C with injective constructors"

ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian Maeder , " seC -> sC and eC"

2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder , " FOL -> first order logic"

2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder , " FOAlg -> FOL without predicates"

2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder , " Horn -> positive conditional logic"

2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder , " GHorn -> generalized Horn"

2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder , " GCond -> GHorn without predicates"

2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder , " Cond -> Horn without predicates"

2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder , " Atom -> atomic logic"

2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder , " Eq -> Atom without predicates"

2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder , " = -> with equality"

2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder , ""

62ecb1e7f8fd9573eea8369657de12c7bf9f4f25Christian Maeder , "Examples:"

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder , " SubPCFOL= -> the CASL logic itself"

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder , " FOAlg= -> first order algebra (without predicates)"

62ecb1e7f8fd9573eea8369657de12c7bf9f4f25Christian Maeder , " SubPHorn= -> the positive conditional fragement of CASL"

3c62e6ef442caf092adcbecf6fccd957dcd72689Christian Maeder , " SubPAtom -> the atomic subset of CASL"

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder , " SubPCAtom -> SubPAtom with sort generation constraints"

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder , " Eq= -> classical equational logic" ]

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maedertype CASLBasicSpec = BASIC_SPEC () () ()

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian MaedertrueC :: a -> b -> Bool

715ffaf874309df081d1e1cd8e05073fc1227729Christian MaedertrueC _ _ = True

62ecb1e7f8fd9573eea8369657de12c7bf9f4f25Christian Maeder

62ecb1e7f8fd9573eea8369657de12c7bf9f4f25Christian Maederinstance (Ord f, Ord e, Ord m, MorphismExtension e m) =>

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder Category (Sign f e) (Morphism f e m) where

62ecb1e7f8fd9573eea8369657de12c7bf9f4f25Christian Maeder ide sig = idMor (ideMorphismExtension $ extendedInfo sig) sig

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder inverse = inverseMorphism inverseMorphismExtension

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder composeMorphisms = composeM composeMorphismExtension

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder dom = msource

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder cod = mtarget

5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder isInclusion = isInclusionMorphism isInclusionMorphismExtension

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder legal_mor = legalMor

836e72a3c413366ba9801726f3b249c7791cb9caChristian Maeder

836e72a3c413366ba9801726f3b249c7791cb9caChristian Maederinstance Monoid (BASIC_SPEC b s f) where

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder mempty = Basic_spec []

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder mappend (Basic_spec l1) (Basic_spec l2) = Basic_spec $ l1 ++ l2

149e43c4a2705a86a0e5fa301ba849fdf19db32eChristian Maeder

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder-- abstract syntax, parsing (and printing)

149e43c4a2705a86a0e5fa301ba849fdf19db32eChristian Maeder

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maederinstance Syntax CASL CASLBasicSpec

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder Symbol SYMB_ITEMS SYMB_MAP_ITEMS

5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder where

5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder parsersAndPrinters CASL = addSyntax "KIF"

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder (const $ fmap kif2CASL kifBasic, pretty)

5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder $ makeDefault (basicSpec [], pretty)

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder parseSingleSymbItem CASL = Just $ symbItem []

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder parse_symb_items CASL = Just $ symbItems []

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder parse_symb_map_items CASL = Just $ symbMapItems []

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder toItem CASL = bsToItem

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder

5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder-- lattices (for sublogics)

797f811e57952d59e73b8cd03b667eef276db972Christian Maeder

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maederinstance Lattice a => SemiLatticeWithTop (CASL_SL a) where

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder join = sublogics_max

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder top = SL.top

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder

5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maederclass Lattice a => MinSL a f where

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder minSL :: f -> CASL_SL a

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder

5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maederinstance MinSL () () where

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder minSL () = bottom

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder

3c62e6ef442caf092adcbecf6fccd957dcd72689Christian Maederclass NameSL a where

149e43c4a2705a86a0e5fa301ba849fdf19db32eChristian Maeder nameSL :: a -> String

149e43c4a2705a86a0e5fa301ba849fdf19db32eChristian Maeder

1738d16957389457347bee85075d3d33d002158fChristian Maederinstance NameSL () where

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder nameSL _ = ""

1738d16957389457347bee85075d3d33d002158fChristian Maeder

33a5d53a412ba0a4e5847f7538d6da2e22bd116cChristian Maederclass Lattice a => ProjForm a f where

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder projForm :: CASL_SL a -> f -> Maybe (FORMULA f)

62ecb1e7f8fd9573eea8369657de12c7bf9f4f25Christian Maeder

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maederinstance Lattice a => ProjForm a () where

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder projForm _ = Just . ExtFORMULA

5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder

b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maederclass (Lattice a, ProjForm a f) => ProjSigItem a s f where

5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder projSigItems :: CASL_SL a -> s -> (Maybe (SIG_ITEMS s f), [SORT])

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maederinstance (Lattice a, ProjForm a f) => ProjSigItem a () f where

88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian Maeder projSigItems _ s = (Just $ Ext_SIG_ITEMS s, [])

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maederclass (Lattice a, ProjForm a f) => ProjBasic a b s f where

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder projBasicItems :: CASL_SL a -> b -> (Maybe (BASIC_ITEMS b s f), [SORT])

88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian Maeder

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maederinstance (Lattice a, ProjForm a f, ProjSigItem a s f)

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder => ProjBasic a () s f where

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder projBasicItems _ b = (Just $ Ext_BASIC_ITEMS b, [])

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maederinstance (NameSL a) => SublogicName (CASL_SL a) where

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder sublogicName = sublogics_name nameSL

88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian Maeder

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maederinstance (MinSL a f, MinSL a s, MinSL a b) =>

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder MinSublogic (CASL_SL a) (BASIC_SPEC b s f) where

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder minSublogic = sl_basic_spec minSL minSL minSL

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maederinstance MinSL a f => MinSublogic (CASL_SL a) (FORMULA f) where

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder minSublogic = sl_sentence minSL

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maederinstance Lattice a => MinSublogic (CASL_SL a) SYMB_ITEMS where

88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian Maeder minSublogic = sl_symb_items

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maederinstance Lattice a => MinSublogic (CASL_SL a) SYMB_MAP_ITEMS where

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder minSublogic = sl_symb_map_items

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maederinstance MinSL a e => MinSublogic (CASL_SL a) (Sign f e) where

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder minSublogic = sl_sign minSL

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maederinstance MinSL a e => MinSublogic (CASL_SL a) (Morphism f e m) where

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder minSublogic = sl_morphism minSL

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder

88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian Maederinstance Lattice a => MinSublogic (CASL_SL a) Symbol where

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder minSublogic = sl_symbol

instance (MinSL a f, MinSL a s, MinSL a b, ProjForm a f,

ProjSigItem a s f, ProjBasic a b s f) =>

ProjectSublogic (CASL_SL a) (BASIC_SPEC b s f) where

projectSublogic = pr_basic_spec projBasicItems projSigItems projForm

instance Lattice a => ProjectSublogicM (CASL_SL a) SYMB_ITEMS where

projectSublogicM = pr_symb_items

instance Lattice a => ProjectSublogicM (CASL_SL a) SYMB_MAP_ITEMS where

projectSublogicM = pr_symb_map_items

instance MinSL a e => ProjectSublogic (CASL_SL a) (Sign f e) where

projectSublogic = pr_sign

instance MinSL a e => ProjectSublogic (CASL_SL a) (Morphism f e m) where

projectSublogic = pr_morphism

instance Lattice a => ProjectSublogicM (CASL_SL a) Symbol where

projectSublogicM = pr_symbol

-- CASL logic

instance Sentences CASL CASLFORMULA CASLSign CASLMor Symbol where

map_sen CASL m = return . mapSen (const id) m

negation CASL = negateFormula

sym_of CASL = symOf

mostSymsOf CASL = sigSymsOf

symmap_of CASL = morphismToSymbMap

sym_name CASL = symName

symKind CASL = show . pretty . symbolKind . symbType

symsOfSen CASL = Set.toList

. foldFormula (symbolsRecord $ const Set.empty)

simplify_sen CASL = simplifyCASLSen

print_named CASL = printTheoryFormula

instance StaticAnalysis CASL CASLBasicSpec CASLFORMULA

SYMB_ITEMS SYMB_MAP_ITEMS

CASLSign

CASLMor

Symbol RawSymbol where

basic_analysis CASL = Just basicCASLAnalysis

sen_analysis CASL = Just cASLsen_analysis

stat_symb_map_items CASL = statSymbMapItems

stat_symb_items CASL = statSymbItems

signature_colimit CASL diag = return $ signColimit diag extCASLColimit

quotient_term_algebra CASL = quotientTermAlgebra

ensures_amalgamability CASL (opts, diag, sink, desc) =

ensuresAmalgamability opts diag sink desc

qualify CASL = qualifySig

symbol_to_raw CASL = symbolToRaw

id_to_raw CASL = idToRaw

matches CASL = CASL.Morphism.matches

is_transportable CASL = isSortInjective

is_injective CASL = isInjective

empty_signature CASL = emptySign ()

add_symb_to_sign CASL = addSymbToSign

signature_union CASL s = return . addSig const s

signatureDiff CASL s = return . diffSig const s

intersection CASL s = return . interSig const s

morphism_union CASL = plainMorphismUnion const

final_union CASL = finalUnion const

is_subsig CASL = isSubSig trueC

subsig_inclusion CASL = sigInclusion ()

cogenerated_sign CASL = cogeneratedSign ()

generated_sign CASL = generatedSign ()

induced_from_morphism CASL = inducedFromMorphism ()

induced_from_to_morphism CASL = inducedFromToMorphism () trueC const

theory_to_taxonomy CASL = convTaxo

instance Logic CASL CASL_Sublogics

CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS

CASLSign

CASLMor

Symbol RawSymbol ProofTree where

stability CASL = Stable

-- for Hybridization

parse_basic_sen CASL = Just $ \ _ -> formula []

proj_sublogic_epsilon CASL = pr_epsilon ()

all_sublogics CASL = sublogics_all []

sublogicDimensions CASL = sDims []

parseSublogic CASL = parseSL (\ s -> Just ((), s))

conservativityCheck CASL = [ConservativityChecker "CCC" checkFreeType]

empty_proof_tree CASL = emptyProofTree

omdoc_metatheory CASL = Just caslMetaTheory

export_senToOmdoc CASL = exportSenToOmdoc

export_symToOmdoc CASL = exportSymToOmdoc

export_theoryToOmdoc CASL = exportTheoryToOmdoc

omdocToSen CASL = OMI.omdocToSen

omdocToSym CASL = OMI.omdocToSym

addOMadtToTheory CASL = OMI.addOMadtToTheory

addOmdocToTheory CASL = OMI.addOmdocToTheory

syntaxTable CASL = Just . getSyntaxTable

#ifdef UNI_PACKAGE

provers CASL = [quickCheckProver]

#endif