{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}

{- |

Module : ./CoCASL/Logic_CoCASL.hs

Description : Instance of class Logic for CoCASL

Copyright : (c) Till Mossakowski, Uni Bremen 2002-2004

License : GPLv2 or higher, see LICENSE.txt

Maintainer : hausmann@informatik.uni-bremen.de

Stability : provisional

Portability : portable

Instance of class Logic for CoCASL.

-}

module CoCASL.Logic_CoCASL where

import CoCASL.AS_CoCASL

import CoCASL.ATC_CoCASL ()

import CoCASL.CoCASLSign

import CoCASL.Parse_AS

import CoCASL.StatAna

import CoCASL.Sublogic

import CASL.AS_Basic_CASL

import CASL.Logic_CASL

import CASL.MapSentence

import CASL.Morphism

import CASL.Parse_AS_Basic

import CASL.Sign

import CASL.Sublogic

import CASL.SymbolMapAnalysis

import CASL.SymbolParser

import Data.List

import Common.DocUtils

import Logic.Logic

data CoCASL = CoCASL deriving Show

instance Language CoCASL where

description _ = "CoCASL is the coalgebraic extension of CASL."

type CoCASLMor = Morphism C_FORMULA CoCASLSign (DefMorExt CoCASLSign)

type CoCASLFORMULA = FORMULA C_FORMULA

instance SignExtension CoCASLSign where

isSubSignExtension = isSubCoCASLSign

instance Syntax CoCASL C_BASIC_SPEC Symbol SYMB_ITEMS SYMB_MAP_ITEMS where

parse_basic_spec CoCASL = Just $ basicSpec cocasl_reserved_words

parse_symb_items CoCASL = Just $ symbItems cocasl_reserved_words

parse_symb_map_items CoCASL = Just $ symbMapItems cocasl_reserved_words

-- CoCASL logic

map_C_FORMULA :: MapSen C_FORMULA CoCASLSign (DefMorExt CoCASLSign)

map_C_FORMULA mor frm = case frm of

BoxOrDiamond b m f ps -> let

newF = mapSen map_C_FORMULA mor f

newM = case m of

Simple_mod _ -> m

Term_mod t -> Term_mod $ mapTerm map_C_FORMULA mor t

in BoxOrDiamond b newM newF ps

phi -> phi

instance Sentences CoCASL CoCASLFORMULA CSign CoCASLMor Symbol where

map_sen CoCASL m = return . mapSen map_C_FORMULA m

sym_of CoCASL = symOf

symKind CoCASL = show . pretty . symbolKind . symbType

symmap_of CoCASL = morphismToSymbMap

sym_name CoCASL = symName

instance StaticAnalysis CoCASL C_BASIC_SPEC CoCASLFORMULA

SYMB_ITEMS SYMB_MAP_ITEMS

CSign

CoCASLMor

Symbol RawSymbol where

basic_analysis CoCASL = Just basicCoCASLAnalysis

sen_analysis CoCASL = Just co_sen_analysis

stat_symb_map_items CoCASL = statSymbMapItems

stat_symb_items CoCASL = statSymbItems

symbol_to_raw CoCASL = symbolToRaw

id_to_raw CoCASL = idToRaw

matches CoCASL = CASL.Morphism.matches

empty_signature CoCASL = emptySign emptyCoCASLSign

signature_union CoCASL s = return . addSig addCoCASLSign s

intersection CoCASL s = return . interSig interCoCASLSign s

morphism_union CoCASL = plainMorphismUnion addCoCASLSign

final_union CoCASL = finalUnion addCoCASLSign

is_subsig CoCASL = isSubSig isSubCoCASLSign

subsig_inclusion CoCASL = sigInclusion emptyMorExt

cogenerated_sign CoCASL = cogeneratedSign emptyMorExt

generated_sign CoCASL = generatedSign emptyMorExt

induced_from_morphism CoCASL = inducedFromMorphism emptyMorExt

induced_from_to_morphism CoCASL =

inducedFromToMorphism emptyMorExt isSubCoCASLSign diffCoCASLSign

instance NameSL Bool where

nameSL b = if b then "Co" else ""

instance MinSL Bool C_FORMULA where

minSL = minFormSublogic

instance MinSL Bool C_SIG_ITEM where

minSL = minCSigItem

instance MinSL Bool C_BASIC_ITEM where

minSL = minCBaseItem

instance MinSL Bool CoCASLSign where

minSL = const bottom

instance ProjForm Bool C_FORMULA where

projForm _ = Just . ExtFORMULA

instance ProjSigItem Bool C_SIG_ITEM C_FORMULA where

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

instance ProjBasic Bool C_BASIC_ITEM C_SIG_ITEM C_FORMULA where

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

instance Logic CoCASL CoCASL_Sublogics

C_BASIC_SPEC CoCASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS

CSign

CoCASLMor

Symbol RawSymbol () where

parse_basic_sen CoCASL = Just $ const parseSen

stability CoCASL = Testing

proj_sublogic_epsilon CoCASL = pr_epsilon emptyMorExt

all_sublogics CoCASL = sublogics_all [True]

sublogicDimensions CoCASL = sDims [[True]]

parseSublogic CoCASL = parseSL parseCo

empty_proof_tree CoCASL = ()

parseCo :: String -> Maybe (Bool, String)

parseCo s = case stripPrefix "Co" s of

Just r | not $ isPrefixOf "nd" r -> Just (True, r)

_ -> Just (False, s)