d29201dd5328b88140ce050100693c501852657dChristian Maeder{-# LANGUAGE CPP, MultiParamTypeClasses, TypeSynonymInstances

211c5fb252e0a776baad9a4857ab198659289a4aKristina Sojakova , FlexibleInstances #-}

e9458b1a7a19a63aa4c179f9ab20f4d50681c168Jens Elkner{- |

211c5fb252e0a776baad9a4857ab198659289a4aKristina SojakovaModule : $Header$

211c5fb252e0a776baad9a4857ab198659289a4aKristina SojakovaDescription : Instance of class Logic for the CASL logic

94e2e03f6efde106de095ef4ea0ec87f74955a31Kristina SojakovaCopyright : (c) Klaus Luettich, Uni Bremen 2002-2005

98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : GPLv2 or higher, see LICENSE.txt

211c5fb252e0a776baad9a4857ab198659289a4aKristina Sojakova

94e2e03f6efde106de095ef4ea0ec87f74955a31Kristina SojakovaMaintainer : till@informatik.uni-bremen.de

211c5fb252e0a776baad9a4857ab198659289a4aKristina SojakovaStability : provisional

211c5fb252e0a776baad9a4857ab198659289a4aKristina SojakovaPortability : non-portable (imports Logic.Logic)

211c5fb252e0a776baad9a4857ab198659289a4aKristina Sojakova

a3a6b6ebe9c2d1dc3554e44779dc7361a90e7617Kristina SojakovaInstance of class Logic for the CASL logic

211c5fb252e0a776baad9a4857ab198659289a4aKristina Sojakova Also the instances for Syntax and Category.

211c5fb252e0a776baad9a4857ab198659289a4aKristina Sojakova-}

211c5fb252e0a776baad9a4857ab198659289a4aKristina Sojakova

7bb21262b4e6ea26f20869f13d2163583c120156Kristina Sojakovamodule CASL.Logic_CASL where

7bb21262b4e6ea26f20869f13d2163583c120156Kristina Sojakova

e16b3696b2c173aac14200321868ed81b8f7dc69Christian Maederimport ATC.ProofTree ()

e16b3696b2c173aac14200321868ed81b8f7dc69Christian Maeder

e16b3696b2c173aac14200321868ed81b8f7dc69Christian Maederimport CASL.AS_Basic_CASL

e16b3696b2c173aac14200321868ed81b8f7dc69Christian Maederimport CASL.Parse_AS_Basic

e16b3696b2c173aac14200321868ed81b8f7dc69Christian Maederimport CASL.Kif

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederimport CASL.Kif2CASL

e16b3696b2c173aac14200321868ed81b8f7dc69Christian Maederimport CASL.Fold

65e11df7259566aa1d95e5977c7ebf1c332a9461Kristina Sojakovaimport CASL.ToDoc

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakovaimport CASL.ToItem (bsToItem)

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakovaimport CASL.SymbolParser

9f8b6c20948cc102562f8ad0c39a4b5e3855b02fKristina Sojakovaimport CASL.MapSentence

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakovaimport CASL.Amalgamability

2ddc9d39235393dca2e40203dde20284db4c3deeKristina Sojakovaimport CASL.ATC_CASL ()

2ddc9d39235393dca2e40203dde20284db4c3deeKristina Sojakovaimport CASL.Sublogic as SL

45caf47cd6ed07be0637f6c51e4735512ce9d83aKristina Sojakovaimport CASL.Sign

e16b3696b2c173aac14200321868ed81b8f7dc69Christian Maederimport CASL.StaticAna

150dbefbeef7403ab31ecbf9c3bb56515be67cdfKristina Sojakovaimport CASL.ColimSign

150dbefbeef7403ab31ecbf9c3bb56515be67cdfKristina Sojakovaimport CASL.Morphism

150dbefbeef7403ab31ecbf9c3bb56515be67cdfKristina Sojakovaimport CASL.SymbolMapAnalysis

150dbefbeef7403ab31ecbf9c3bb56515be67cdfKristina Sojakovaimport CASL.Taxonomy

150dbefbeef7403ab31ecbf9c3bb56515be67cdfKristina Sojakovaimport CASL.Simplify

150dbefbeef7403ab31ecbf9c3bb56515be67cdfKristina Sojakovaimport CASL.SimplifySen

dd6f22b9dcff2695181b86372e4df03d5b96e92dKristina Sojakovaimport CASL.CCC.FreeTypes

dd6f22b9dcff2695181b86372e4df03d5b96e92dKristina Sojakovaimport CASL.CCC.OnePoint () -- currently unused

150dbefbeef7403ab31ecbf9c3bb56515be67cdfKristina Sojakovaimport CASL.Qualify

150dbefbeef7403ab31ecbf9c3bb56515be67cdfKristina Sojakovaimport CASL.Quantification

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakovaimport qualified CASL.OMDocImport as OMI

9be5b6267dea82f0eb283bd4ae9d4f83e05a6944Christian Maederimport CASL.OMDocExport

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakovaimport CASL.Freeness

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova

14650c9e129d8dc51ed55b2edc6ec27d9f0f6d00Kristina Sojakova#ifdef UNI_PACKAGE

9be5b6267dea82f0eb283bd4ae9d4f83e05a6944Christian Maederimport CASL.QuickCheck

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder#endif

150dbefbeef7403ab31ecbf9c3bb56515be67cdfKristina Sojakova

e16b3696b2c173aac14200321868ed81b8f7dc69Christian Maederimport Common.ProofTree

e16b3696b2c173aac14200321868ed81b8f7dc69Christian Maederimport Common.Consistency

e16b3696b2c173aac14200321868ed81b8f7dc69Christian Maederimport Common.DocUtils

e16b3696b2c173aac14200321868ed81b8f7dc69Christian Maeder

150dbefbeef7403ab31ecbf9c3bb56515be67cdfKristina Sojakovaimport Data.Monoid

a65c6747c9acbbebc93baba7bae94d2e3d8cdafbTill Mossakowskiimport qualified Data.Set as Set

150dbefbeef7403ab31ecbf9c3bb56515be67cdfKristina Sojakova

9be5b6267dea82f0eb283bd4ae9d4f83e05a6944Christian Maederimport Logic.Logic

9be5b6267dea82f0eb283bd4ae9d4f83e05a6944Christian Maeder

150dbefbeef7403ab31ecbf9c3bb56515be67cdfKristina Sojakovadata CASL = CASL deriving Show

150dbefbeef7403ab31ecbf9c3bb56515be67cdfKristina Sojakova

345d3dcc9f809776009851c446916fc770aa428dKristina Sojakovainstance Language CASL where

a669e4685b32ff5ca1bca785eacc5e30a545b010Christian Maeder description _ = unlines

a669e4685b32ff5ca1bca785eacc5e30a545b010Christian Maeder [ "CASL - the Common algebraic specification language"

63dbf3642c023a8bebbc8ca0d56f698114551c8cKristina Sojakova , "This logic is subsorted partial first-order logic"

cb5d588c4c3b286cc1e7210335d6ef7f584d79bcKristina Sojakova , " with sort generation constraints"

150dbefbeef7403ab31ecbf9c3bb56515be67cdfKristina Sojakova , "See the CASL User Manual, LNCS 2900, Springer Verlag"

150dbefbeef7403ab31ecbf9c3bb56515be67cdfKristina Sojakova , "and the CASL Reference Manual, LNCS 2960, Springer Verlag"

9be5b6267dea82f0eb283bd4ae9d4f83e05a6944Christian Maeder , "See also http://www.cofi.info/CASL.html"

9be5b6267dea82f0eb283bd4ae9d4f83e05a6944Christian Maeder , ""

2fa2a7c86b9416f0e1607787e9416e274feb1143Christian Maeder , "Abbreviations of sublogic names indicate the following feature:"

9be5b6267dea82f0eb283bd4ae9d4f83e05a6944Christian Maeder , " Sub -> with subsorting"

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

9be5b6267dea82f0eb283bd4ae9d4f83e05a6944Christian Maeder , " P -> with partial functions"

9be5b6267dea82f0eb283bd4ae9d4f83e05a6944Christian Maeder , " C -> with sort generation constraints"

2fa2a7c86b9416f0e1607787e9416e274feb1143Christian Maeder , " eC -> C without renamings"

2ddc9d39235393dca2e40203dde20284db4c3deeKristina Sojakova , " sC -> C with injective constructors"

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova , " seC -> sC and eC"

2ddc9d39235393dca2e40203dde20284db4c3deeKristina Sojakova , " FOL -> first order logic"

a669e4685b32ff5ca1bca785eacc5e30a545b010Christian Maeder , " FOAlg -> FOL without predicates"

80d2ec8f37d5ddec13c14b17b1bab01e9c94630aChristian Maeder , " Horn -> positive conditional logic"

c82e21a85ef57135a0c582ca0f418b1541151645Kristina Sojakova , " GHorn -> generalized Horn"

63dbf3642c023a8bebbc8ca0d56f698114551c8cKristina Sojakova , " GCond -> GHorn without predicates"

c82e21a85ef57135a0c582ca0f418b1541151645Kristina Sojakova , " Cond -> Horn without predicates"

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova , " Atom -> atomic logic"

a669e4685b32ff5ca1bca785eacc5e30a545b010Christian Maeder , " Eq -> Atom without predicates"

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova , " = -> with equality"

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova , ""

a669e4685b32ff5ca1bca785eacc5e30a545b010Christian Maeder , "Examples:"

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova , " SubPCFOL= -> the CASL logic itself"

63dbf3642c023a8bebbc8ca0d56f698114551c8cKristina Sojakova , " FOAlg= -> first order algebra (without predicates)"

63dbf3642c023a8bebbc8ca0d56f698114551c8cKristina Sojakova , " SubPHorn= -> the positive conditional fragement of CASL"

45caf47cd6ed07be0637f6c51e4735512ce9d83aKristina Sojakova , " SubPAtom -> the atomic subset of CASL"

df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina Sojakova , " SubPCAtom -> SubPAtom with sort generation constraints"

df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina Sojakova , " Eq= -> classical equational logic" ]

345a7bff808e621f05d2ce86fdbab2a28c9e0d3dKristina Sojakova

cb5d588c4c3b286cc1e7210335d6ef7f584d79bcKristina Sojakovatype CASLBasicSpec = BASIC_SPEC () () ()

150dbefbeef7403ab31ecbf9c3bb56515be67cdfKristina Sojakova

150dbefbeef7403ab31ecbf9c3bb56515be67cdfKristina SojakovatrueC :: a -> b -> Bool

4b61e23f57d9d13d036aedb1b10178d3e013ab38Kristina SojakovatrueC _ _ = True

9be5b6267dea82f0eb283bd4ae9d4f83e05a6944Christian Maeder

2fa2a7c86b9416f0e1607787e9416e274feb1143Christian Maederinstance (Ord f, Ord e, Ord m, MorphismExtension e m) =>

9be5b6267dea82f0eb283bd4ae9d4f83e05a6944Christian Maeder Category (Sign f e) (Morphism f e m) where

9be5b6267dea82f0eb283bd4ae9d4f83e05a6944Christian Maeder ide sig = idMor (ideMorphismExtension $ extendedInfo sig) sig

9be5b6267dea82f0eb283bd4ae9d4f83e05a6944Christian Maeder inverse = inverseMorphism inverseMorphismExtension

9be5b6267dea82f0eb283bd4ae9d4f83e05a6944Christian Maeder composeMorphisms = composeM composeMorphismExtension

2fa2a7c86b9416f0e1607787e9416e274feb1143Christian Maeder dom = msource

2ddc9d39235393dca2e40203dde20284db4c3deeKristina Sojakova cod = mtarget

4b61e23f57d9d13d036aedb1b10178d3e013ab38Kristina Sojakova isInclusion = isInclusionMorphism isInclusionMorphismExtension

345d3dcc9f809776009851c446916fc770aa428dKristina Sojakova legal_mor = legalMor

345d3dcc9f809776009851c446916fc770aa428dKristina Sojakova

345d3dcc9f809776009851c446916fc770aa428dKristina Sojakovainstance Monoid (BASIC_SPEC b s f) where

345d3dcc9f809776009851c446916fc770aa428dKristina Sojakova mempty = Basic_spec []

mappend (Basic_spec l1) (Basic_spec l2) = Basic_spec $ l1 ++ l2

-- abstract syntax, parsing (and printing)

instance Syntax CASL CASLBasicSpec

SYMB_ITEMS SYMB_MAP_ITEMS

where

parsersAndPrinters CASL = addSyntax "KIF"

(const $ fmap kif2CASL kifBasic, pretty)

$ makeDefault (basicSpec [], pretty)

parse_symb_items CASL = Just $ symbItems []

parse_symb_map_items CASL = Just $ symbMapItems []

toItem CASL = bsToItem

-- lattices (for sublogics)

instance Lattice a => SemiLatticeWithTop (CASL_SL a) where

join = sublogics_max

top = SL.top

class Lattice a => MinSL a f where

minSL :: f -> CASL_SL a

instance MinSL () () where

minSL () = bottom

class NameSL a where

nameSL :: a -> String

instance NameSL () where

nameSL _ = ""

class Lattice a => ProjForm a f where

projForm :: CASL_SL a -> f -> Maybe (FORMULA f)

instance Lattice a => ProjForm a () where

projForm _ = Just . ExtFORMULA

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

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

instance (Lattice a, ProjForm a f) => ProjSigItem a () f where

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

class (Lattice a, ProjForm a f) => ProjBasic a b s f where

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

instance (Lattice a, ProjForm a f, ProjSigItem a s f)

=> ProjBasic a () s f where

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

instance (NameSL a) => SublogicName (CASL_SL a) where

sublogicName = sublogics_name nameSL

instance (MinSL a f, MinSL a s, MinSL a b) =>

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

minSublogic = sl_basic_spec minSL minSL minSL

instance MinSL a f => MinSublogic (CASL_SL a) (FORMULA f) where

minSublogic = sl_sentence minSL

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

minSublogic = sl_symb_items

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

minSublogic = sl_symb_map_items

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

minSublogic = sl_sign minSL

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

minSublogic = sl_morphism minSL

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

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

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

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