{-# 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 Int -> CoCASL -> ShowS
[CoCASL] -> ShowS
CoCASL -> String
(Int -> CoCASL -> ShowS)
-> (CoCASL -> String) -> ([CoCASL] -> ShowS) -> Show CoCASL
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [CoCASL] -> ShowS
$cshowList :: [CoCASL] -> ShowS
show :: CoCASL -> String
$cshow :: CoCASL -> String
showsPrec :: Int -> CoCASL -> ShowS
$cshowsPrec :: Int -> CoCASL -> ShowS
Show

instance Language CoCASL where
  description :: CoCASL -> String
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 :: CoCASLSign -> CoCASLSign -> Bool
isSubSignExtension = CoCASLSign -> CoCASLSign -> Bool
isSubCoCASLSign

instance Syntax CoCASL C_BASIC_SPEC Symbol SYMB_ITEMS SYMB_MAP_ITEMS where
    parse_basic_spec :: CoCASL -> Maybe (PrefixMap -> AParser st C_BASIC_SPEC)
parse_basic_spec CoCASL = (PrefixMap -> AParser st C_BASIC_SPEC)
-> Maybe (PrefixMap -> AParser st C_BASIC_SPEC)
forall a. a -> Maybe a
Just ((PrefixMap -> AParser st C_BASIC_SPEC)
 -> Maybe (PrefixMap -> AParser st C_BASIC_SPEC))
-> (PrefixMap -> AParser st C_BASIC_SPEC)
-> Maybe (PrefixMap -> AParser st C_BASIC_SPEC)
forall a b. (a -> b) -> a -> b
$ [String] -> PrefixMap -> AParser st C_BASIC_SPEC
forall f s b st.
(TermParser f, AParsable s, AParsable b) =>
[String] -> PrefixMap -> AParser st (BASIC_SPEC b s f)
basicSpec [String]
cocasl_reserved_words
    parse_symb_items :: CoCASL -> Maybe (PrefixMap -> AParser st SYMB_ITEMS)
parse_symb_items CoCASL = (PrefixMap -> AParser st SYMB_ITEMS)
-> Maybe (PrefixMap -> AParser st SYMB_ITEMS)
forall a. a -> Maybe a
Just ((PrefixMap -> AParser st SYMB_ITEMS)
 -> Maybe (PrefixMap -> AParser st SYMB_ITEMS))
-> (AParser st SYMB_ITEMS -> PrefixMap -> AParser st SYMB_ITEMS)
-> AParser st SYMB_ITEMS
-> Maybe (PrefixMap -> AParser st SYMB_ITEMS)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AParser st SYMB_ITEMS -> PrefixMap -> AParser st SYMB_ITEMS
forall a b. a -> b -> a
const (AParser st SYMB_ITEMS
 -> Maybe (PrefixMap -> AParser st SYMB_ITEMS))
-> AParser st SYMB_ITEMS
-> Maybe (PrefixMap -> AParser st SYMB_ITEMS)
forall a b. (a -> b) -> a -> b
$ [String] -> AParser st SYMB_ITEMS
forall st. [String] -> AParser st SYMB_ITEMS
symbItems [String]
cocasl_reserved_words
    parse_symb_map_items :: CoCASL -> Maybe (PrefixMap -> AParser st SYMB_MAP_ITEMS)
parse_symb_map_items CoCASL = (PrefixMap -> AParser st SYMB_MAP_ITEMS)
-> Maybe (PrefixMap -> AParser st SYMB_MAP_ITEMS)
forall a. a -> Maybe a
Just ((PrefixMap -> AParser st SYMB_MAP_ITEMS)
 -> Maybe (PrefixMap -> AParser st SYMB_MAP_ITEMS))
-> (AParser st SYMB_MAP_ITEMS
    -> PrefixMap -> AParser st SYMB_MAP_ITEMS)
-> AParser st SYMB_MAP_ITEMS
-> Maybe (PrefixMap -> AParser st SYMB_MAP_ITEMS)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AParser st SYMB_MAP_ITEMS -> PrefixMap -> AParser st SYMB_MAP_ITEMS
forall a b. a -> b -> a
const (AParser st SYMB_MAP_ITEMS
 -> Maybe (PrefixMap -> AParser st SYMB_MAP_ITEMS))
-> AParser st SYMB_MAP_ITEMS
-> Maybe (PrefixMap -> AParser st SYMB_MAP_ITEMS)
forall a b. (a -> b) -> a -> b
$ [String] -> AParser st SYMB_MAP_ITEMS
forall st. [String] -> AParser st SYMB_MAP_ITEMS
symbMapItems [String]
cocasl_reserved_words

-- CoCASL logic

map_C_FORMULA :: MapSen C_FORMULA CoCASLSign (DefMorExt CoCASLSign)
map_C_FORMULA :: MapSen C_FORMULA CoCASLSign (DefMorExt CoCASLSign)
map_C_FORMULA mor :: Morphism C_FORMULA CoCASLSign (DefMorExt CoCASLSign)
mor frm :: C_FORMULA
frm = case C_FORMULA
frm of
           BoxOrDiamond b :: Bool
b m :: MODALITY
m f :: FORMULA C_FORMULA
f ps :: Range
ps -> let
              newF :: FORMULA C_FORMULA
newF = MapSen C_FORMULA CoCASLSign (DefMorExt CoCASLSign)
-> Morphism C_FORMULA CoCASLSign (DefMorExt CoCASLSign)
-> FORMULA C_FORMULA
-> FORMULA C_FORMULA
forall e m f.
MorphismExtension e m =>
MapSen f e m -> Morphism f e m -> FORMULA f -> FORMULA f
mapSen MapSen C_FORMULA CoCASLSign (DefMorExt CoCASLSign)
map_C_FORMULA Morphism C_FORMULA CoCASLSign (DefMorExt CoCASLSign)
mor FORMULA C_FORMULA
f
              newM :: MODALITY
newM = case MODALITY
m of
                   Simple_mod _ -> MODALITY
m
                   Term_mod t :: TERM C_FORMULA
t -> TERM C_FORMULA -> MODALITY
Term_mod (TERM C_FORMULA -> MODALITY) -> TERM C_FORMULA -> MODALITY
forall a b. (a -> b) -> a -> b
$ MapSen C_FORMULA CoCASLSign (DefMorExt CoCASLSign)
-> Morphism C_FORMULA CoCASLSign (DefMorExt CoCASLSign)
-> TERM C_FORMULA
-> TERM C_FORMULA
forall f e m. MapSen f e m -> Morphism f e m -> TERM f -> TERM f
mapTerm MapSen C_FORMULA CoCASLSign (DefMorExt CoCASLSign)
map_C_FORMULA Morphism C_FORMULA CoCASLSign (DefMorExt CoCASLSign)
mor TERM C_FORMULA
t
              in Bool -> MODALITY -> FORMULA C_FORMULA -> Range -> C_FORMULA
BoxOrDiamond Bool
b MODALITY
newM FORMULA C_FORMULA
newF Range
ps
           phi :: C_FORMULA
phi -> C_FORMULA
phi

instance Sentences CoCASL CoCASLFORMULA CSign CoCASLMor Symbol where
      map_sen :: CoCASL
-> Morphism C_FORMULA CoCASLSign (DefMorExt CoCASLSign)
-> FORMULA C_FORMULA
-> Result (FORMULA C_FORMULA)
map_sen CoCASL m :: Morphism C_FORMULA CoCASLSign (DefMorExt CoCASLSign)
m = FORMULA C_FORMULA -> Result (FORMULA C_FORMULA)
forall (m :: * -> *) a. Monad m => a -> m a
return (FORMULA C_FORMULA -> Result (FORMULA C_FORMULA))
-> (FORMULA C_FORMULA -> FORMULA C_FORMULA)
-> FORMULA C_FORMULA
-> Result (FORMULA C_FORMULA)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MapSen C_FORMULA CoCASLSign (DefMorExt CoCASLSign)
-> Morphism C_FORMULA CoCASLSign (DefMorExt CoCASLSign)
-> FORMULA C_FORMULA
-> FORMULA C_FORMULA
forall e m f.
MorphismExtension e m =>
MapSen f e m -> Morphism f e m -> FORMULA f -> FORMULA f
mapSen MapSen C_FORMULA CoCASLSign (DefMorExt CoCASLSign)
map_C_FORMULA Morphism C_FORMULA CoCASLSign (DefMorExt CoCASLSign)
m
      sym_of :: CoCASL -> CSign -> [Set Symbol]
sym_of CoCASL = CSign -> [Set Symbol]
forall f e. Sign f e -> [Set Symbol]
symOf
      symKind :: CoCASL -> Symbol -> String
symKind CoCASL = Doc -> String
forall a. Show a => a -> String
show (Doc -> String) -> (Symbol -> Doc) -> Symbol -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SYMB_KIND -> Doc
forall a. Pretty a => a -> Doc
pretty (SYMB_KIND -> Doc) -> (Symbol -> SYMB_KIND) -> Symbol -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SymbType -> SYMB_KIND
symbolKind (SymbType -> SYMB_KIND)
-> (Symbol -> SymbType) -> Symbol -> SYMB_KIND
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> SymbType
symbType
      symmap_of :: CoCASL
-> Morphism C_FORMULA CoCASLSign (DefMorExt CoCASLSign)
-> EndoMap Symbol
symmap_of CoCASL = Morphism C_FORMULA CoCASLSign (DefMorExt CoCASLSign)
-> EndoMap Symbol
forall f e m. Morphism f e m -> EndoMap Symbol
morphismToSymbMap
      sym_name :: CoCASL -> Symbol -> Id
sym_name CoCASL = Symbol -> Id
symName

instance StaticAnalysis CoCASL C_BASIC_SPEC CoCASLFORMULA
               SYMB_ITEMS SYMB_MAP_ITEMS
               CSign
               CoCASLMor
               Symbol RawSymbol where
         basic_analysis :: CoCASL
-> Maybe
     ((C_BASIC_SPEC, CSign, GlobalAnnos)
      -> Result
           (C_BASIC_SPEC, ExtSign CSign Symbol, [Named (FORMULA C_FORMULA)]))
basic_analysis CoCASL = ((C_BASIC_SPEC, CSign, GlobalAnnos)
 -> Result
      (C_BASIC_SPEC, ExtSign CSign Symbol, [Named (FORMULA C_FORMULA)]))
-> Maybe
     ((C_BASIC_SPEC, CSign, GlobalAnnos)
      -> Result
           (C_BASIC_SPEC, ExtSign CSign Symbol, [Named (FORMULA C_FORMULA)]))
forall a. a -> Maybe a
Just (C_BASIC_SPEC, CSign, GlobalAnnos)
-> Result
     (C_BASIC_SPEC, ExtSign CSign Symbol, [Named (FORMULA C_FORMULA)])
basicCoCASLAnalysis
         sen_analysis :: CoCASL
-> Maybe
     ((C_BASIC_SPEC, CSign, FORMULA C_FORMULA)
      -> Result (FORMULA C_FORMULA))
sen_analysis CoCASL = ((C_BASIC_SPEC, CSign, FORMULA C_FORMULA)
 -> Result (FORMULA C_FORMULA))
-> Maybe
     ((C_BASIC_SPEC, CSign, FORMULA C_FORMULA)
      -> Result (FORMULA C_FORMULA))
forall a. a -> Maybe a
Just (C_BASIC_SPEC, CSign, FORMULA C_FORMULA)
-> Result (FORMULA C_FORMULA)
co_sen_analysis
         stat_symb_map_items :: CoCASL
-> CSign
-> Maybe CSign
-> [SYMB_MAP_ITEMS]
-> Result (EndoMap RawSymbol)
stat_symb_map_items CoCASL = CSign
-> Maybe CSign -> [SYMB_MAP_ITEMS] -> Result (EndoMap RawSymbol)
forall f e.
Sign f e
-> Maybe (Sign f e)
-> [SYMB_MAP_ITEMS]
-> Result (EndoMap RawSymbol)
statSymbMapItems
         stat_symb_items :: CoCASL -> CSign -> [SYMB_ITEMS] -> Result [RawSymbol]
stat_symb_items CoCASL = CSign -> [SYMB_ITEMS] -> Result [RawSymbol]
forall f e. Sign f e -> [SYMB_ITEMS] -> Result [RawSymbol]
statSymbItems

         symbol_to_raw :: CoCASL -> Symbol -> RawSymbol
symbol_to_raw CoCASL = Symbol -> RawSymbol
symbolToRaw
         id_to_raw :: CoCASL -> Id -> RawSymbol
id_to_raw CoCASL = Id -> RawSymbol
idToRaw
         matches :: CoCASL -> Symbol -> RawSymbol -> Bool
matches CoCASL = Symbol -> RawSymbol -> Bool
CASL.Morphism.matches

         empty_signature :: CoCASL -> CSign
empty_signature CoCASL = CoCASLSign -> CSign
forall e f. e -> Sign f e
emptySign CoCASLSign
emptyCoCASLSign
         signature_union :: CoCASL -> CSign -> CSign -> Result CSign
signature_union CoCASL s :: CSign
s = CSign -> Result CSign
forall (m :: * -> *) a. Monad m => a -> m a
return (CSign -> Result CSign)
-> (CSign -> CSign) -> CSign -> Result CSign
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (CoCASLSign -> CoCASLSign -> CoCASLSign) -> CSign -> CSign -> CSign
forall e f. (e -> e -> e) -> Sign f e -> Sign f e -> Sign f e
addSig CoCASLSign -> CoCASLSign -> CoCASLSign
addCoCASLSign CSign
s
         intersection :: CoCASL -> CSign -> CSign -> Result CSign
intersection CoCASL s :: CSign
s = CSign -> Result CSign
forall (m :: * -> *) a. Monad m => a -> m a
return (CSign -> Result CSign)
-> (CSign -> CSign) -> CSign -> Result CSign
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (CoCASLSign -> CoCASLSign -> CoCASLSign) -> CSign -> CSign -> CSign
forall e f. (e -> e -> e) -> Sign f e -> Sign f e -> Sign f e
interSig CoCASLSign -> CoCASLSign -> CoCASLSign
interCoCASLSign CSign
s
         morphism_union :: CoCASL
-> Morphism C_FORMULA CoCASLSign (DefMorExt CoCASLSign)
-> Morphism C_FORMULA CoCASLSign (DefMorExt CoCASLSign)
-> Result (Morphism C_FORMULA CoCASLSign (DefMorExt CoCASLSign))
morphism_union CoCASL = (CoCASLSign -> CoCASLSign -> CoCASLSign)
-> Morphism C_FORMULA CoCASLSign (DefMorExt CoCASLSign)
-> Morphism C_FORMULA CoCASLSign (DefMorExt CoCASLSign)
-> Result (Morphism C_FORMULA CoCASLSign (DefMorExt CoCASLSign))
forall e f m.
(e -> e -> e)
-> Morphism f e m -> Morphism f e m -> Result (Morphism f e m)
plainMorphismUnion CoCASLSign -> CoCASLSign -> CoCASLSign
addCoCASLSign
         final_union :: CoCASL -> CSign -> CSign -> Result CSign
final_union CoCASL = (CoCASLSign -> CoCASLSign -> CoCASLSign)
-> CSign -> CSign -> Result CSign
forall e f.
(e -> e -> e) -> Sign f e -> Sign f e -> Result (Sign f e)
finalUnion CoCASLSign -> CoCASLSign -> CoCASLSign
addCoCASLSign
         is_subsig :: CoCASL -> CSign -> CSign -> Bool
is_subsig CoCASL = (CoCASLSign -> CoCASLSign -> Bool) -> CSign -> CSign -> Bool
forall e f. (e -> e -> Bool) -> Sign f e -> Sign f e -> Bool
isSubSig CoCASLSign -> CoCASLSign -> Bool
isSubCoCASLSign
         subsig_inclusion :: CoCASL
-> CSign
-> CSign
-> Result (Morphism C_FORMULA CoCASLSign (DefMorExt CoCASLSign))
subsig_inclusion CoCASL = DefMorExt CoCASLSign
-> CSign
-> CSign
-> Result (Morphism C_FORMULA CoCASLSign (DefMorExt CoCASLSign))
forall m f e. m -> Sign f e -> Sign f e -> Result (Morphism f e m)
sigInclusion DefMorExt CoCASLSign
forall e. DefMorExt e
emptyMorExt
         cogenerated_sign :: CoCASL
-> Set Symbol
-> CSign
-> Result (Morphism C_FORMULA CoCASLSign (DefMorExt CoCASLSign))
cogenerated_sign CoCASL = DefMorExt CoCASLSign
-> Set Symbol
-> CSign
-> Result (Morphism C_FORMULA CoCASLSign (DefMorExt CoCASLSign))
forall m f e.
m -> Set Symbol -> Sign f e -> Result (Morphism f e m)
cogeneratedSign DefMorExt CoCASLSign
forall e. DefMorExt e
emptyMorExt
         generated_sign :: CoCASL
-> Set Symbol
-> CSign
-> Result (Morphism C_FORMULA CoCASLSign (DefMorExt CoCASLSign))
generated_sign CoCASL = DefMorExt CoCASLSign
-> Set Symbol
-> CSign
-> Result (Morphism C_FORMULA CoCASLSign (DefMorExt CoCASLSign))
forall m f e.
m -> Set Symbol -> Sign f e -> Result (Morphism f e m)
generatedSign DefMorExt CoCASLSign
forall e. DefMorExt e
emptyMorExt
         induced_from_morphism :: CoCASL
-> EndoMap RawSymbol
-> CSign
-> Result (Morphism C_FORMULA CoCASLSign (DefMorExt CoCASLSign))
induced_from_morphism CoCASL = DefMorExt CoCASLSign
-> EndoMap RawSymbol
-> CSign
-> Result (Morphism C_FORMULA CoCASLSign (DefMorExt CoCASLSign))
forall e f m.
(Pretty e, Show f) =>
m -> EndoMap RawSymbol -> Sign f e -> Result (Morphism f e m)
inducedFromMorphism DefMorExt CoCASLSign
forall e. DefMorExt e
emptyMorExt
         induced_from_to_morphism :: CoCASL
-> EndoMap RawSymbol
-> ExtSign CSign Symbol
-> ExtSign CSign Symbol
-> Result (Morphism C_FORMULA CoCASLSign (DefMorExt CoCASLSign))
induced_from_to_morphism CoCASL =
             DefMorExt CoCASLSign
-> (CoCASLSign -> CoCASLSign -> Bool)
-> (CoCASLSign -> CoCASLSign -> CoCASLSign)
-> EndoMap RawSymbol
-> ExtSign CSign Symbol
-> ExtSign CSign Symbol
-> Result (Morphism C_FORMULA CoCASLSign (DefMorExt CoCASLSign))
forall e f m.
(Eq e, Show f, Pretty e, Pretty m) =>
m
-> (e -> e -> Bool)
-> (e -> e -> e)
-> EndoMap RawSymbol
-> ExtSign (Sign f e) Symbol
-> ExtSign (Sign f e) Symbol
-> Result (Morphism f e m)
inducedFromToMorphism DefMorExt CoCASLSign
forall e. DefMorExt e
emptyMorExt CoCASLSign -> CoCASLSign -> Bool
isSubCoCASLSign CoCASLSign -> CoCASLSign -> CoCASLSign
diffCoCASLSign

instance NameSL Bool where
    nameSL :: Bool -> String
nameSL b :: Bool
b = if Bool
b then "Co" else ""

instance MinSL Bool C_FORMULA where
    minSL :: C_FORMULA -> CASL_SL Bool
minSL = C_FORMULA -> CASL_SL Bool
minFormSublogic

instance MinSL Bool C_SIG_ITEM where
    minSL :: C_SIG_ITEM -> CASL_SL Bool
minSL = C_SIG_ITEM -> CASL_SL Bool
minCSigItem

instance MinSL Bool C_BASIC_ITEM where
    minSL :: C_BASIC_ITEM -> CASL_SL Bool
minSL = C_BASIC_ITEM -> CASL_SL Bool
minCBaseItem

instance MinSL Bool CoCASLSign where
    minSL :: CoCASLSign -> CASL_SL Bool
minSL = CASL_SL Bool -> CoCASLSign -> CASL_SL Bool
forall a b. a -> b -> a
const CASL_SL Bool
forall a. Lattice a => CASL_SL a
bottom

instance ProjForm Bool C_FORMULA where
    projForm :: CASL_SL Bool -> C_FORMULA -> Maybe (FORMULA C_FORMULA)
projForm _ = FORMULA C_FORMULA -> Maybe (FORMULA C_FORMULA)
forall a. a -> Maybe a
Just (FORMULA C_FORMULA -> Maybe (FORMULA C_FORMULA))
-> (C_FORMULA -> FORMULA C_FORMULA)
-> C_FORMULA
-> Maybe (FORMULA C_FORMULA)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. C_FORMULA -> FORMULA C_FORMULA
forall f. f -> FORMULA f
ExtFORMULA

instance ProjSigItem Bool C_SIG_ITEM C_FORMULA where
    projSigItems :: CASL_SL Bool
-> C_SIG_ITEM -> (Maybe (SIG_ITEMS C_SIG_ITEM C_FORMULA), [Id])
projSigItems _ s :: C_SIG_ITEM
s = (SIG_ITEMS C_SIG_ITEM C_FORMULA
-> Maybe (SIG_ITEMS C_SIG_ITEM C_FORMULA)
forall a. a -> Maybe a
Just (SIG_ITEMS C_SIG_ITEM C_FORMULA
 -> Maybe (SIG_ITEMS C_SIG_ITEM C_FORMULA))
-> SIG_ITEMS C_SIG_ITEM C_FORMULA
-> Maybe (SIG_ITEMS C_SIG_ITEM C_FORMULA)
forall a b. (a -> b) -> a -> b
$ C_SIG_ITEM -> SIG_ITEMS C_SIG_ITEM C_FORMULA
forall s f. s -> SIG_ITEMS s f
Ext_SIG_ITEMS C_SIG_ITEM
s, [])

instance ProjBasic Bool C_BASIC_ITEM C_SIG_ITEM C_FORMULA where
    projBasicItems :: CASL_SL Bool
-> C_BASIC_ITEM
-> (Maybe (BASIC_ITEMS C_BASIC_ITEM C_SIG_ITEM C_FORMULA), [Id])
projBasicItems _ b :: C_BASIC_ITEM
b = (BASIC_ITEMS C_BASIC_ITEM C_SIG_ITEM C_FORMULA
-> Maybe (BASIC_ITEMS C_BASIC_ITEM C_SIG_ITEM C_FORMULA)
forall a. a -> Maybe a
Just (BASIC_ITEMS C_BASIC_ITEM C_SIG_ITEM C_FORMULA
 -> Maybe (BASIC_ITEMS C_BASIC_ITEM C_SIG_ITEM C_FORMULA))
-> BASIC_ITEMS C_BASIC_ITEM C_SIG_ITEM C_FORMULA
-> Maybe (BASIC_ITEMS C_BASIC_ITEM C_SIG_ITEM C_FORMULA)
forall a b. (a -> b) -> a -> b
$ C_BASIC_ITEM -> BASIC_ITEMS C_BASIC_ITEM C_SIG_ITEM C_FORMULA
forall b s f. b -> BASIC_ITEMS b s f
Ext_BASIC_ITEMS C_BASIC_ITEM
b, [])

instance Logic CoCASL CoCASL_Sublogics
               C_BASIC_SPEC CoCASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS
               CSign
               CoCASLMor
               Symbol RawSymbol () where
         parse_basic_sen :: CoCASL -> Maybe (C_BASIC_SPEC -> AParser st (FORMULA C_FORMULA))
parse_basic_sen CoCASL = (C_BASIC_SPEC -> AParser st (FORMULA C_FORMULA))
-> Maybe (C_BASIC_SPEC -> AParser st (FORMULA C_FORMULA))
forall a. a -> Maybe a
Just ((C_BASIC_SPEC -> AParser st (FORMULA C_FORMULA))
 -> Maybe (C_BASIC_SPEC -> AParser st (FORMULA C_FORMULA)))
-> (C_BASIC_SPEC -> AParser st (FORMULA C_FORMULA))
-> Maybe (C_BASIC_SPEC -> AParser st (FORMULA C_FORMULA))
forall a b. (a -> b) -> a -> b
$ AParser st (FORMULA C_FORMULA)
-> C_BASIC_SPEC -> AParser st (FORMULA C_FORMULA)
forall a b. a -> b -> a
const AParser st (FORMULA C_FORMULA)
forall st. AParser st (FORMULA C_FORMULA)
parseSen
         stability :: CoCASL -> Stability
stability CoCASL = Stability
Testing
         proj_sublogic_epsilon :: CoCASL
-> CASL_SL Bool
-> CSign
-> Morphism C_FORMULA CoCASLSign (DefMorExt CoCASLSign)
proj_sublogic_epsilon CoCASL = DefMorExt CoCASLSign
-> CASL_SL Bool
-> CSign
-> Morphism C_FORMULA CoCASLSign (DefMorExt CoCASLSign)
forall m a f e. m -> CASL_SL a -> Sign f e -> Morphism f e m
pr_epsilon DefMorExt CoCASLSign
forall e. DefMorExt e
emptyMorExt
         all_sublogics :: CoCASL -> [CASL_SL Bool]
all_sublogics CoCASL = [Bool] -> [CASL_SL Bool]
forall a. Lattice a => [a] -> [CASL_SL a]
sublogics_all [Bool
True]
         sublogicDimensions :: CoCASL -> [[CASL_SL Bool]]
sublogicDimensions CoCASL = [[Bool]] -> [[CASL_SL Bool]]
forall a. Lattice a => [[a]] -> [[CASL_SL a]]
sDims [[Bool
True]]
         parseSublogic :: CoCASL -> String -> Maybe (CASL_SL Bool)
parseSublogic CoCASL = (String -> Maybe (Bool, String)) -> String -> Maybe (CASL_SL Bool)
forall a.
(String -> Maybe (a, String)) -> String -> Maybe (CASL_SL a)
parseSL String -> Maybe (Bool, String)
parseCo
         empty_proof_tree :: CoCASL -> ()
empty_proof_tree CoCASL = ()

parseCo :: String -> Maybe (Bool, String)
parseCo :: String -> Maybe (Bool, String)
parseCo s :: String
s = case String -> String -> Maybe String
forall a. Eq a => [a] -> [a] -> Maybe [a]
stripPrefix "Co" String
s of
  Just r :: String
r | Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
isPrefixOf "nd" String
r -> (Bool, String) -> Maybe (Bool, String)
forall a. a -> Maybe a
Just (Bool
True, String
r)
  _ -> (Bool, String) -> Maybe (Bool, String)
forall a. a -> Maybe a
Just (Bool
False, String
s)