{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances #-}
{- |
Module      :  ./RelationalScheme/Logic_Rel.hs
Description :  Instance of class Logic for Rel
Copyright   :  (c) Dominik Luecke, Uni Bremen 2008
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  luecke@informatik.uni-bremen.de
Stability   :  experimental
Portability :  non-portable (imports Logic.Logic)

Instance of class Logic for RelationalSchemes
-}

module RelationalScheme.Logic_Rel where

import Common.DocUtils
import Common.Id

import Data.Monoid ()
import qualified Data.Set as Set

import Logic.Logic

import RelationalScheme.AS
import RelationalScheme.Sign
import RelationalScheme.ParseRS
import RelationalScheme.ATC_RelationalScheme ()
import RelationalScheme.StaticAnalysis

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

instance Language RelScheme where
    description :: RelScheme -> String
description _ =
        "Simple logic for Relational Schemes"

-- | Instance of Category for Rel
instance Category
        Sign                   -- sign
        RSMorphism             -- mor
        where
                dom :: RSMorphism -> Sign
dom = RSMorphism -> Sign
domain
                cod :: RSMorphism -> Sign
cod = RSMorphism -> Sign
codomain
                ide :: Sign -> RSMorphism
ide = Sign -> RSMorphism
idMor
                composeMorphisms :: RSMorphism -> RSMorphism -> Result RSMorphism
composeMorphisms = RSMorphism -> RSMorphism -> Result RSMorphism
comp_rst_mor

-- | Instance of Sentences for Rel
instance Sentences RelScheme Sentence Sign RSMorphism RSSymbol where
    -- there is nothing to leave out
    simplify_sen :: RelScheme -> Sign -> Sentence -> Sentence
simplify_sen RelScheme _ form :: Sentence
form = Sentence
form
    print_named :: RelScheme -> Named Sentence -> Doc
print_named _ = (Sentence -> Doc) -> Annoted Sentence -> Doc
forall a. (a -> Doc) -> Annoted a -> Doc
printAnnoted Sentence -> Doc
forall a. Pretty a => a -> Doc
pretty (Annoted Sentence -> Doc)
-> (Named Sentence -> Annoted Sentence) -> Named Sentence -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Named Sentence -> Annoted Sentence
forall s. Named s -> Annoted s
fromLabelledSen
    map_sen :: RelScheme -> RSMorphism -> Sentence -> Result Sentence
map_sen RelScheme = RSMorphism -> Sentence -> Result Sentence
map_rel
    symKind :: RelScheme -> RSSymbol -> String
symKind RelScheme = Doc -> String
forall a. Show a => a -> String
show (Doc -> String) -> (RSSymbol -> Doc) -> RSSymbol -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RSSymbolKind -> Doc
forall a. Pretty a => a -> Doc
pretty (RSSymbolKind -> Doc)
-> (RSSymbol -> RSSymbolKind) -> RSSymbol -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RSSymbol -> RSSymbolKind
sym_kind

instance Semigroup RSRelationships where
    (RSRelationships l1 :: [Annoted Sentence]
l1 r1 :: Range
r1) <> :: RSRelationships -> RSRelationships -> RSRelationships
<> (RSRelationships l2 :: [Annoted Sentence]
l2 r2 :: Range
r2) =
        [Annoted Sentence] -> Range -> RSRelationships
RSRelationships ([Annoted Sentence]
l1 [Annoted Sentence] -> [Annoted Sentence] -> [Annoted Sentence]
forall a. [a] -> [a] -> [a]
++ [Annoted Sentence]
l2) (Range -> RSRelationships) -> Range -> RSRelationships
forall a b. (a -> b) -> a -> b
$ Range -> Range -> Range
appRange Range
r1 Range
r2
instance Monoid RSRelationships where
    mempty :: RSRelationships
mempty = [Annoted Sentence] -> Range -> RSRelationships
RSRelationships [] Range
nullRange

instance Semigroup RSTables where
    (RSTables s1 :: Set RSTable
s1) <> :: Sign -> Sign -> Sign
<> (RSTables s2 :: Set RSTable
s2) = Set RSTable -> Sign
RSTables (Set RSTable -> Sign) -> Set RSTable -> Sign
forall a b. (a -> b) -> a -> b
$ Set RSTable -> Set RSTable -> Set RSTable
forall a. Ord a => Set a -> Set a -> Set a
Set.union Set RSTable
s1 Set RSTable
s2
instance Monoid RSTables where
    mempty :: Sign
mempty = Sign
emptyRSSign

instance Semigroup RSScheme where
    (RSScheme l1 :: Sign
l1 s1 :: RSRelationships
s1 r1 :: Range
r1) <> :: RSScheme -> RSScheme -> RSScheme
<> (RSScheme l2 :: Sign
l2 s2 :: RSRelationships
s2 r2 :: Range
r2) = Sign -> RSRelationships -> Range -> RSScheme
RSScheme
      (Sign
l1 Sign -> Sign -> Sign
forall a. Semigroup a => a -> a -> a
<> Sign
l2) (RSRelationships
s1 RSRelationships -> RSRelationships -> RSRelationships
forall a. Semigroup a => a -> a -> a
<> RSRelationships
s2) (Range -> RSScheme) -> Range -> RSScheme
forall a b. (a -> b) -> a -> b
$ Range -> Range -> Range
appRange Range
r1 Range
r2
instance Monoid RSScheme where
    mempty :: RSScheme
mempty = Sign -> RSRelationships -> Range -> RSScheme
RSScheme Sign
forall a. Monoid a => a
mempty RSRelationships
forall a. Monoid a => a
mempty Range
nullRange

-- | Syntax of Rel
instance Syntax RelScheme RSScheme RSSymbol () () where
         parse_basic_spec :: RelScheme -> Maybe (PrefixMap -> AParser st RSScheme)
parse_basic_spec RelScheme = (PrefixMap -> AParser st RSScheme)
-> Maybe (PrefixMap -> AParser st RSScheme)
forall a. a -> Maybe a
Just PrefixMap -> AParser st RSScheme
forall st. PrefixMap -> AParser st RSScheme
parseRSScheme
         parse_symb_items :: RelScheme -> Maybe (PrefixMap -> AParser st ())
parse_symb_items _ = Maybe (PrefixMap -> AParser st ())
forall a. Maybe a
Nothing
         parse_symb_map_items :: RelScheme -> Maybe (PrefixMap -> AParser st ())
parse_symb_map_items _ = Maybe (PrefixMap -> AParser st ())
forall a. Maybe a
Nothing

-- | Instance of Logic for Relational Schemes
instance Logic RelScheme
    ()                     -- Sublogics
    RSScheme               -- basic_spec
    Sentence               -- sentence
    ()                     -- symb_items
    ()                     -- symb_map_items
    Sign                   -- sign
    RSMorphism             -- morphism
    RSSymbol               -- symbol
    RSRawSymbol            -- raw_symbol
    ()                     -- proof_tree
    where
      stability :: RelScheme -> Stability
stability RelScheme = Stability
Experimental

-- | Static Analysis for Rel
instance StaticAnalysis RelScheme
    RSScheme                      -- basic_spec
    Sentence                      -- sentence
    ()                            -- symb_items
    ()                            -- symb_map_items
    Sign                          -- sign
    RSMorphism                    -- morphism
    RSSymbol                      -- symbol
    RSRawSymbol                   -- raw_symbol
    where
      basic_analysis :: RelScheme
-> Maybe
     ((RSScheme, Sign, GlobalAnnos)
      -> Result (RSScheme, ExtSign Sign RSSymbol, [Named Sentence]))
basic_analysis RelScheme = ((RSScheme, Sign, GlobalAnnos)
 -> Result (RSScheme, ExtSign Sign RSSymbol, [Named Sentence]))
-> Maybe
     ((RSScheme, Sign, GlobalAnnos)
      -> Result (RSScheme, ExtSign Sign RSSymbol, [Named Sentence]))
forall a. a -> Maybe a
Just (RSScheme, Sign, GlobalAnnos)
-> Result (RSScheme, ExtSign Sign RSSymbol, [Named Sentence])
basic_Rel_analysis
      empty_signature :: RelScheme -> Sign
empty_signature RelScheme = Sign
emptyRSSign
      is_subsig :: RelScheme -> Sign -> Sign -> Bool
is_subsig RelScheme = Sign -> Sign -> Bool
isRSSubsig
      subsig_inclusion :: RelScheme -> Sign -> Sign -> Result RSMorphism
subsig_inclusion RelScheme = Sign -> Sign -> Result RSMorphism
rsInclusion
      signature_union :: RelScheme -> Sign -> Sign -> Result Sign
signature_union RelScheme = Sign -> Sign -> Result Sign
forall (m :: * -> *). MonadFail m => Sign -> Sign -> m Sign
uniteSig