{-# LANGUAGE MultiParamTypeClasses #-}
{- |
Module      :  ./Temporal/Logic_Temporal.hs
Description :  Instance of class Logic for temporal logic
Copyright   :  (c) Klaus Hartke, Uni Bremen 2008
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Christian.Maeder@dfki.de
Stability   :  experimental
Portability :  non-portable (imports Logic.Logic)

Instance of class Logic for temporal logic
   Also the instances for Syntax and Category.
-}

module Temporal.Logic_Temporal where

import Data.Monoid ()

import Logic.Logic

import Temporal.Sign as Sign
import Temporal.Morphism as Morphism
import qualified Temporal.Symbol as Symbol

import Temporal.AS_BASIC_Temporal as AS_BASIC
import Temporal.ATC_Temporal ()

-- | Lid for termporal logic
data Temporal = Temporal deriving Int -> Temporal -> ShowS
[Temporal] -> ShowS
Temporal -> String
(Int -> Temporal -> ShowS)
-> (Temporal -> String) -> ([Temporal] -> ShowS) -> Show Temporal
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Temporal] -> ShowS
$cshowList :: [Temporal] -> ShowS
show :: Temporal -> String
$cshow :: Temporal -> String
showsPrec :: Int -> Temporal -> ShowS
$cshowsPrec :: Int -> Temporal -> ShowS
Show


-- | Instance of Language for temporal logic
instance Language Temporal
    where
        description :: Temporal -> String
description Temporal = "Temporal logic"


-- | Instance of Category for temporal logic
instance Category
    Sign.Sign
    Morphism.Morphism
    where
        ide :: Sign -> Morphism
ide = Sign -> Morphism
Morphism.idMor  -- Identity morphism
        dom :: Morphism -> Sign
dom = Morphism -> Sign
Morphism.source -- Returns the domain of a morphism
        cod :: Morphism -> Sign
cod = Morphism -> Sign
Morphism.target -- Returns the codomain of a morphism
        legal_mor :: Morphism -> Result ()
legal_mor = Morphism -> Result ()
Morphism.isLegalMorphism -- Tests if the morphism is ok
        composeMorphisms :: Morphism -> Morphism -> Result Morphism
composeMorphisms = Morphism -> Morphism -> Result Morphism
Morphism.composeMor
        -- Composition of morphisms

-- | Instance of Sentences for temporal logic
instance Sentences Temporal
    AS_BASIC.FORMULA
    Sign.Sign
    Morphism.Morphism
    Symbol.Symbol
    where
        sym_of :: Temporal -> Sign -> [Set Symbol]
sym_of Temporal = Set Symbol -> [Set Symbol]
forall a. a -> [a]
singletonList (Set Symbol -> [Set Symbol])
-> (Sign -> Set Symbol) -> Sign -> [Set Symbol]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sign -> Set Symbol
Symbol.symOf
        -- Returns a list of sets of symbols
        symmap_of :: Temporal -> Morphism -> EndoMap Symbol
symmap_of Temporal = Morphism -> EndoMap Symbol
Symbol.getSymbolMap
        -- Returns the symbol map
        sym_name :: Temporal -> Symbol -> Id
sym_name Temporal = Symbol -> Id
Symbol.getSymbolName
        -- Returns the name of a symbol
        map_sen :: Temporal -> Morphism -> FORMULA -> Result FORMULA
map_sen Temporal = Morphism -> FORMULA -> Result FORMULA
Morphism.mapSentence
        -- Translation of sentences along signature morphism
        simplify_sen :: Temporal -> Sign -> FORMULA -> FORMULA
simplify_sen Temporal _ form :: FORMULA
form = FORMULA
form
        -- There is nothing to leave out
        symKind :: Temporal -> Symbol -> String
symKind Temporal _ = "prop"

instance Semigroup AS_BASIC.BASIC_SPEC where
    _ <> :: BASIC_SPEC -> BASIC_SPEC -> BASIC_SPEC
<> _ = BASIC_SPEC
Basic_spec
instance Monoid AS_BASIC.BASIC_SPEC where
    mempty :: BASIC_SPEC
mempty = BASIC_SPEC
Basic_spec

-- | Syntax of Temporal logic
instance Syntax Temporal
    AS_BASIC.BASIC_SPEC
    Symbol.Symbol
    ()
    ()

-- | Instance of Logic for propositional logc
instance Logic Temporal
    ()                                  -- Sublogics
    AS_BASIC.BASIC_SPEC                 -- basic_spec
    AS_BASIC.FORMULA                    -- sentence
    ()                                  -- symb_items
    ()                                  -- symb_map_items
    Sign.Sign                           -- sign
    Morphism.Morphism                   -- morphism
    Symbol.Symbol                       -- symbol
    Symbol.Symbol                       -- raw_symbol
    ()                                  -- proof_tree

-- | Static Analysis for propositional logic
instance StaticAnalysis Temporal
    AS_BASIC.BASIC_SPEC                -- basic_spec
    AS_BASIC.FORMULA                   -- sentence
    ()                                 -- symb_items
    ()                                 -- symb_map_items
    Sign.Sign                          -- sign
    Morphism.Morphism                  -- morphism
    Symbol.Symbol                      -- symbol
    Symbol.Symbol                      -- raw_symbol
        where
          empty_signature :: Temporal -> Sign
empty_signature Temporal = Sign
Sign.emptySig
          is_subsig :: Temporal -> Sign -> Sign -> Bool
is_subsig Temporal = Sign -> Sign -> Bool
Sign.isSubSigOf
          subsig_inclusion :: Temporal -> Sign -> Sign -> Result Morphism
subsig_inclusion Temporal s :: Sign
s = Morphism -> Result Morphism
forall (m :: * -> *) a. Monad m => a -> m a
return (Morphism -> Result Morphism)
-> (Sign -> Morphism) -> Sign -> Result Morphism
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sign -> Sign -> Morphism
Morphism.inclusionMap Sign
s
          signature_union :: Temporal -> Sign -> Sign -> Result Sign
signature_union Temporal = Sign -> Sign -> Result Sign
Sign.sigUnion
          symbol_to_raw :: Temporal -> Symbol -> Symbol
symbol_to_raw Temporal = Symbol -> Symbol
Symbol.symbolToRaw
          id_to_raw :: Temporal -> Id -> Symbol
id_to_raw Temporal = Id -> Symbol
Symbol.idToRaw
          matches :: Temporal -> Symbol -> Symbol -> Bool
matches Temporal = Symbol -> Symbol -> Bool
Symbol.matches