{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}
{- |
Module      :  ./COL/Logic_COL.hs
Description :  COL instance of class Logic
Copyright   :  (c) Till Mossakowski, Uni Bremen 2002-2004
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  till@informatik.uni-bremen.de
Stability   :  provisional
Portability :  non-portable (via Logic)

COL instance of class Logic
-}

module COL.Logic_COL where

import COL.AS_COL
import COL.COLSign
import COL.ATC_COL ()
import COL.Parse_AS ()
import COL.StatAna
import COL.Print_AS ()
import CASL.Sign
import CASL.StaticAna
import CASL.MixfixParser
import CASL.Morphism
import CASL.SymbolMapAnalysis
import CASL.AS_Basic_CASL
import CASL.Parse_AS_Basic
import CASL.MapSentence
import CASL.SymbolParser
import CASL.Logic_CASL ()
import Logic.Logic

import Common.DocUtils

data COL = COL deriving Int -> COL -> ShowS
[COL] -> ShowS
COL -> String
(Int -> COL -> ShowS)
-> (COL -> String) -> ([COL] -> ShowS) -> Show COL
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [COL] -> ShowS
$cshowList :: [COL] -> ShowS
show :: COL -> String
$cshow :: COL -> String
showsPrec :: Int -> COL -> ShowS
$cshowsPrec :: Int -> COL -> ShowS
Show

instance Language COL where
 description :: COL -> String
description _ =
  "COLCASL extends CASL by constructors and observers"

type C_BASIC_SPEC = BASIC_SPEC () COL_SIG_ITEM ()
type CSign = Sign () COLSign
type COLMor = Morphism () COLSign (DefMorExt COLSign)
type COLFORMULA = FORMULA ()

instance SignExtension COLSign where
  isSubSignExtension :: COLSign -> COLSign -> Bool
isSubSignExtension = COLSign -> COLSign -> Bool
isSubCOLSign

instance Syntax COL C_BASIC_SPEC
                Symbol SYMB_ITEMS SYMB_MAP_ITEMS
      where
         parse_basic_spec :: COL -> Maybe (PrefixMap -> AParser st C_BASIC_SPEC)
parse_basic_spec COL = (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]
col_reserved_words
         parse_symb_items :: COL -> Maybe (PrefixMap -> AParser st SYMB_ITEMS)
parse_symb_items COL = (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]
col_reserved_words
         parse_symb_map_items :: COL -> Maybe (PrefixMap -> AParser st SYMB_MAP_ITEMS)
parse_symb_map_items COL = (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]
col_reserved_words

instance Sentences COL COLFORMULA CSign COLMor Symbol where
      map_sen :: COL -> COLMor -> COLFORMULA -> Result COLFORMULA
map_sen COL m :: COLMor
m = COLFORMULA -> Result COLFORMULA
forall (m :: * -> *) a. Monad m => a -> m a
return (COLFORMULA -> Result COLFORMULA)
-> (COLFORMULA -> COLFORMULA) -> COLFORMULA -> Result COLFORMULA
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MapSen () COLSign (DefMorExt COLSign)
-> COLMor -> COLFORMULA -> COLFORMULA
forall e m f.
MorphismExtension e m =>
MapSen f e m -> Morphism f e m -> FORMULA f -> FORMULA f
mapSen ((() -> ()) -> MapSen () COLSign (DefMorExt COLSign)
forall a b. a -> b -> a
const () -> ()
forall a. a -> a
id) COLMor
m
      sym_of :: COL -> CSign -> [Set Symbol]
sym_of COL = CSign -> [Set Symbol]
forall f e. Sign f e -> [Set Symbol]
symOf
      symKind :: COL -> Symbol -> String
symKind COL = 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 :: COL -> COLMor -> EndoMap Symbol
symmap_of COL = COLMor -> EndoMap Symbol
forall f e m. Morphism f e m -> EndoMap Symbol
morphismToSymbMap
      sym_name :: COL -> Symbol -> Id
sym_name COL = Symbol -> Id
symName

instance StaticAnalysis COL C_BASIC_SPEC COLFORMULA
               SYMB_ITEMS SYMB_MAP_ITEMS
               CSign
               COLMor
               Symbol RawSymbol where
         basic_analysis :: COL
-> Maybe
     ((C_BASIC_SPEC, CSign, GlobalAnnos)
      -> Result (C_BASIC_SPEC, ExtSign CSign Symbol, [Named COLFORMULA]))
basic_analysis COL = ((C_BASIC_SPEC, CSign, GlobalAnnos)
 -> Result (C_BASIC_SPEC, ExtSign CSign Symbol, [Named COLFORMULA]))
-> Maybe
     ((C_BASIC_SPEC, CSign, GlobalAnnos)
      -> Result (C_BASIC_SPEC, ExtSign CSign Symbol, [Named COLFORMULA]))
forall a. a -> Maybe a
Just (((C_BASIC_SPEC, CSign, GlobalAnnos)
  -> Result (C_BASIC_SPEC, ExtSign CSign Symbol, [Named COLFORMULA]))
 -> Maybe
      ((C_BASIC_SPEC, CSign, GlobalAnnos)
       -> Result
            (C_BASIC_SPEC, ExtSign CSign Symbol, [Named COLFORMULA])))
-> ((C_BASIC_SPEC, CSign, GlobalAnnos)
    -> Result (C_BASIC_SPEC, ExtSign CSign Symbol, [Named COLFORMULA]))
-> Maybe
     ((C_BASIC_SPEC, CSign, GlobalAnnos)
      -> Result (C_BASIC_SPEC, ExtSign CSign Symbol, [Named COLFORMULA]))
forall a b. (a -> b) -> a -> b
$ Min () COLSign
-> Ana () () COL_SIG_ITEM () COLSign
-> Ana COL_SIG_ITEM () COL_SIG_ITEM () COLSign
-> Mix () COL_SIG_ITEM () COLSign
-> (C_BASIC_SPEC, CSign, GlobalAnnos)
-> Result (C_BASIC_SPEC, ExtSign CSign Symbol, [Named COLFORMULA])
forall f e b s.
(FormExtension f, TermExtension f) =>
Min f e
-> Ana b b s f e
-> Ana s b s f e
-> Mix b s f e
-> (BASIC_SPEC b s f, Sign f e, GlobalAnnos)
-> Result
     (BASIC_SPEC b s f, ExtSign (Sign f e) Symbol, [Named (FORMULA f)])
basicAnalysis ((() -> Result ()) -> Min () COLSign
forall a b. a -> b -> a
const () -> Result ()
forall (m :: * -> *) a. Monad m => a -> m a
return)
                              ((() -> State CSign ()) -> Ana () () COL_SIG_ITEM () COLSign
forall a b. a -> b -> a
const () -> State CSign ()
forall (m :: * -> *) a. Monad m => a -> m a
return) Ana COL_SIG_ITEM () COL_SIG_ITEM () COLSign
ana_COL_SIG_ITEM
                              Mix () COL_SIG_ITEM () COLSign
forall b s f e. Mix b s f e
emptyMix
         stat_symb_map_items :: COL
-> CSign
-> Maybe CSign
-> [SYMB_MAP_ITEMS]
-> Result (EndoMap RawSymbol)
stat_symb_map_items COL = 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 :: COL -> CSign -> [SYMB_ITEMS] -> Result [RawSymbol]
stat_symb_items COL = CSign -> [SYMB_ITEMS] -> Result [RawSymbol]
forall f e. Sign f e -> [SYMB_ITEMS] -> Result [RawSymbol]
statSymbItems

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

         empty_signature :: COL -> CSign
empty_signature COL = COLSign -> CSign
forall e f. e -> Sign f e
emptySign COLSign
emptyCOLSign
         signature_union :: COL -> CSign -> CSign -> Result CSign
signature_union COL sigma1 :: CSign
sigma1 =
           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
. (COLSign -> COLSign -> COLSign) -> CSign -> CSign -> CSign
forall e f. (e -> e -> e) -> Sign f e -> Sign f e -> Sign f e
addSig COLSign -> COLSign -> COLSign
addCOLSign CSign
sigma1
         morphism_union :: COL -> COLMor -> COLMor -> Result COLMor
morphism_union COL = (COLSign -> COLSign -> COLSign)
-> COLMor -> COLMor -> Result COLMor
forall e f m.
(e -> e -> e)
-> Morphism f e m -> Morphism f e m -> Result (Morphism f e m)
plainMorphismUnion COLSign -> COLSign -> COLSign
addCOLSign
         final_union :: COL -> CSign -> CSign -> Result CSign
final_union COL = (COLSign -> COLSign -> COLSign) -> CSign -> CSign -> Result CSign
forall e f.
(e -> e -> e) -> Sign f e -> Sign f e -> Result (Sign f e)
finalUnion COLSign -> COLSign -> COLSign
addCOLSign
         is_subsig :: COL -> CSign -> CSign -> Bool
is_subsig COL = (COLSign -> COLSign -> Bool) -> CSign -> CSign -> Bool
forall e f. (e -> e -> Bool) -> Sign f e -> Sign f e -> Bool
isSubSig COLSign -> COLSign -> Bool
isSubCOLSign
         subsig_inclusion :: COL -> CSign -> CSign -> Result COLMor
subsig_inclusion COL = DefMorExt COLSign -> CSign -> CSign -> Result COLMor
forall m f e. m -> Sign f e -> Sign f e -> Result (Morphism f e m)
sigInclusion DefMorExt COLSign
forall e. DefMorExt e
emptyMorExt
         cogenerated_sign :: COL -> Set Symbol -> CSign -> Result COLMor
cogenerated_sign COL = DefMorExt COLSign -> Set Symbol -> CSign -> Result COLMor
forall m f e.
m -> Set Symbol -> Sign f e -> Result (Morphism f e m)
cogeneratedSign DefMorExt COLSign
forall e. DefMorExt e
emptyMorExt
         generated_sign :: COL -> Set Symbol -> CSign -> Result COLMor
generated_sign COL = DefMorExt COLSign -> Set Symbol -> CSign -> Result COLMor
forall m f e.
m -> Set Symbol -> Sign f e -> Result (Morphism f e m)
generatedSign DefMorExt COLSign
forall e. DefMorExt e
emptyMorExt
         induced_from_morphism :: COL -> EndoMap RawSymbol -> CSign -> Result COLMor
induced_from_morphism COL = DefMorExt COLSign -> EndoMap RawSymbol -> CSign -> Result COLMor
forall e f m.
(Pretty e, Show f) =>
m -> EndoMap RawSymbol -> Sign f e -> Result (Morphism f e m)
inducedFromMorphism DefMorExt COLSign
forall e. DefMorExt e
emptyMorExt
         induced_from_to_morphism :: COL
-> EndoMap RawSymbol
-> ExtSign CSign Symbol
-> ExtSign CSign Symbol
-> Result COLMor
induced_from_to_morphism COL =
             DefMorExt COLSign
-> (COLSign -> COLSign -> Bool)
-> (COLSign -> COLSign -> COLSign)
-> EndoMap RawSymbol
-> ExtSign CSign Symbol
-> ExtSign CSign Symbol
-> Result COLMor
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 COLSign
forall e. DefMorExt e
emptyMorExt COLSign -> COLSign -> Bool
isSubCOLSign COLSign -> COLSign -> COLSign
diffCOLSign

instance Logic COL ()
               C_BASIC_SPEC COLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS
               CSign
               COLMor
               Symbol RawSymbol () where
         empty_proof_tree :: COL -> ()
empty_proof_tree _ = ()