{-# LANGUAGE CPP, MultiParamTypeClasses, TypeSynonymInstances

, FlexibleInstances #-}

{- |

Module : $Header$

Description : Instance of class Logic for the CASL logic

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

License : GPLv2 or higher, see LICENSE.txt

Maintainer : till@informatik.uni-bremen.de

Stability : provisional

Portability : non-portable (imports Logic.Logic)

Instance of class Logic for the CASL logic

Also the instances for Syntax and Category.

-}

module CASL.Logic_CASL where

import ATC.ProofTree ()

import CASL.AS_Basic_CASL

import CASL.Parse_AS_Basic

import CASL.Kif

import CASL.Kif2CASL

import CASL.Fold

import CASL.ToDoc

import CASL.ToItem (bsToItem)

import CASL.SymbolParser

import CASL.MapSentence

import CASL.Amalgamability

import CASL.ATC_CASL ()

import CASL.Sublogic as SL

import CASL.Sign

import CASL.StaticAna

import CASL.ColimSign

import CASL.Morphism

import CASL.SymbolMapAnalysis

import CASL.Taxonomy

import CASL.Simplify

import CASL.SimplifySen

import CASL.CCC.FreeTypes

import CASL.CCC.OnePoint () -- currently unused

import CASL.Qualify

import CASL.Quantification

import qualified CASL.OMDocImport as OMI

import CASL.OMDocExport

import CASL.Freeness

-- test

import CASL.Formula (formula)

--

#ifdef UNI_PACKAGE

import CASL.QuickCheck

#endif

import Common.ProofTree

import Common.Consistency

import Common.DocUtils

import Data.Monoid

import qualified Data.Set as Set

import Logic.Logic

data CASL = CASL deriving Show

instance Language CASL where

description _ = unlines

[ "CASL - the Common algebraic specification language"

, "This logic is subsorted partial first-order logic"

, " with sort generation constraints"

, "See the CASL User Manual, LNCS 2900, Springer Verlag"

, "and the CASL Reference Manual, LNCS 2960, Springer Verlag"

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

, ""

, "Abbreviations of sublogic names indicate the following feature:"

, " Sub -> with subsorting"

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

, " P -> with partial functions"

, " C -> with sort generation constraints"

, " eC -> C without renamings"

, " sC -> C with injective constructors"

, " seC -> sC and eC"

, " FOL -> first order logic"

, " FOAlg -> FOL without predicates"

, " Horn -> positive conditional logic"

, " GHorn -> generalized Horn"

, " GCond -> GHorn without predicates"

, " Cond -> Horn without predicates"

, " Atom -> atomic logic"

, " Eq -> Atom without predicates"

, " = -> with equality"

, ""

, "Examples:"

, " SubPCFOL= -> the CASL logic itself"

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

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

, " SubPAtom -> the atomic subset of CASL"

, " SubPCAtom -> SubPAtom with sort generation constraints"

, " Eq= -> classical equational logic" ]

type CASLBasicSpec = BASIC_SPEC () () ()

trueC :: a -> b -> Bool

trueC _ _ = True

instance (Ord f, Ord e, Ord m, MorphismExtension e m) =>

Category (Sign f e) (Morphism f e m) where

ide sig = idMor (ideMorphismExtension $ extendedInfo sig) sig

inverse = inverseMorphism inverseMorphismExtension

composeMorphisms = composeM composeMorphismExtension

dom = msource

cod = mtarget

isInclusion = isInclusionMorphism isInclusionMorphismExtension

legal_mor = legalMor

instance Monoid (BASIC_SPEC b s f) where

mempty = Basic_spec []

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

-- abstract syntax, parsing (and printing)

instance Syntax CASL CASLBasicSpec

Symbol SYMB_ITEMS SYMB_MAP_ITEMS

where

parsersAndPrinters CASL = addSyntax "KIF"

(const $ fmap kif2CASL kifBasic, pretty)

$ makeDefault (basicSpec [], pretty)

-- parse_symbol CASL = Just $ parseSymb [] -- need static analysis for symbol

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

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