{-# LANGUAGE MultiParamTypeClasses, ScopedTypeVariables
  , TypeSynonymInstances, FlexibleInstances #-}
{- |
Module      :  ./CspCASL/Logic_CspCASL.hs
Description :  CspCASL instance of type class logic
Copyright   :  (c)  Markus Roggenbach, Till Mossakowski and Uni Bremen 2003
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  M.Roggenbach@swansea.ac.uk
Stability   :  experimental
Portability :  non-portable(import Logic.Logic)

Here is the place where the class Logic is instantiated for CspCASL.  A
CspCASL signature is a CASL signature with a set of named channels and
processes. Every process has a profile. Morphisms are supposed to allow
renaming of channels and processes, too. Also sublogics (as a superset of some
CASL sublogics) are still missing.
-}

module CspCASL.Logic_CspCASL
  ( GenCspCASL (..)
  , CspCASLSemantics
  , CspCASL
  , cspCASL
  , Trace (..)
  , traceCspCASL
  , Failure (..)
  , failureCspCASL
  ) where

import Logic.Logic
import Logic.Prover

import Common.DocUtils

import CASL.Logic_CASL
import CASL.Parse_AS_Basic
import CASL.Morphism
import CASL.Sign
import CASL.ToDoc
import qualified CASL.MapSentence as MapSen
import qualified CASL.SimplifySen as SimpSen

import CspCASL.ATC_CspCASL ()
import CspCASL.CspCASL_Keywords
import CspCASL.Morphism as CspCASL_Morphism
import CspCASL.Parse_CspCASL ()
import CspCASL.Print_CspCASL ()
import qualified CspCASL.SignCSP as SignCSP
import qualified CspCASL.SimplifySen as SimplifySen
import CspCASL.StatAnaCSP
import CspCASL.SymbItems
import CspCASL.Symbol
import CspCASL.SymMapAna

import CspCASLProver.CspCASLProver (cspCASLProver)

-- | a generic logic id for CspCASL with different semantics
data GenCspCASL a = GenCspCASL a deriving Int -> GenCspCASL a -> ShowS
[GenCspCASL a] -> ShowS
GenCspCASL a -> String
(Int -> GenCspCASL a -> ShowS)
-> (GenCspCASL a -> String)
-> ([GenCspCASL a] -> ShowS)
-> Show (GenCspCASL a)
forall a. Show a => Int -> GenCspCASL a -> ShowS
forall a. Show a => [GenCspCASL a] -> ShowS
forall a. Show a => GenCspCASL a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [GenCspCASL a] -> ShowS
$cshowList :: forall a. Show a => [GenCspCASL a] -> ShowS
show :: GenCspCASL a -> String
$cshow :: forall a. Show a => GenCspCASL a -> String
showsPrec :: Int -> GenCspCASL a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> GenCspCASL a -> ShowS
Show

cspCASL :: GenCspCASL ()
cspCASL :: GenCspCASL ()
cspCASL = () -> GenCspCASL ()
forall a. a -> GenCspCASL a
GenCspCASL ()

-- | The top-level logic with the loosest semantics (and without provers)
type CspCASL = GenCspCASL ()

instance Show a => Language (GenCspCASL a) where
      language_name :: GenCspCASL a -> String
language_name (GenCspCASL a :: a
a) = "CspCASL"
        String -> ShowS
forall a. [a] -> [a] -> [a]
++ let s :: String
s = a -> String
forall a. Show a => a -> String
show a
a in if String
s String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== "()" then "" else '_' Char -> ShowS
forall a. a -> [a] -> [a]
: String
s
      description :: GenCspCASL a -> String
description _ =
        "CspCASL - extension of CASL with the process algebra CSP\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++
        "See http://www.cs.swan.ac.uk/~csmarkus/ProcessesAndData/"

-- | Instance of Sentences for CspCASL
instance Show a => Sentences (GenCspCASL a)
    -- sentence
    SignCSP.CspCASLSen
    -- signature
    SignCSP.CspCASLSign
    -- morphism
    CspCASL_Morphism.CspCASLMorphism
    -- symbol
    CspSymbol
    where
      map_sen :: GenCspCASL a -> CspCASLMorphism -> CspCASLSen -> Result CspCASLSen
map_sen (GenCspCASL _) m :: CspCASLMorphism
m = CspCASLSen -> Result CspCASLSen
forall (m :: * -> *) a. Monad m => a -> m a
return (CspCASLSen -> Result CspCASLSen)
-> (CspCASLSen -> CspCASLSen) -> CspCASLSen -> Result CspCASLSen
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MapSen CspSen CspSign CspAddMorphism
-> CspCASLMorphism -> CspCASLSen -> CspCASLSen
forall e m f.
MorphismExtension e m =>
MapSen f e m -> Morphism f e m -> FORMULA f -> FORMULA f
MapSen.mapSen MapSen CspSen CspSign CspAddMorphism
mapSen CspCASLMorphism
m
      sym_name :: GenCspCASL a -> CspSymbol -> Id
sym_name (GenCspCASL _) = CspSymbol -> Id
cspSymName
      symmap_of :: GenCspCASL a -> CspCASLMorphism -> EndoMap CspSymbol
symmap_of (GenCspCASL _) = CspCASLMorphism -> EndoMap CspSymbol
cspMorphismToCspSymbMap
      simplify_sen :: GenCspCASL a -> CspCASLSign -> CspCASLSen -> CspCASLSen
simplify_sen (GenCspCASL _) =
        Min CspSen CspSign
-> (CspCASLSign -> CspSen -> CspSen)
-> CspCASLSign
-> CspCASLSen
-> CspCASLSen
forall f e.
(FormExtension f, TermExtension f) =>
Min f e
-> (Sign f e -> f -> f) -> Sign f e -> FORMULA f -> FORMULA f
SimpSen.simplifySen ((CspSen -> Result CspSen) -> Min CspSen CspSign
forall a b. a -> b -> a
const CspSen -> Result CspSen
forall (m :: * -> *) a. Monad m => a -> m a
return) CspCASLSign -> CspSen -> CspSen
SimplifySen.simplifySen
      sym_of :: GenCspCASL a -> CspCASLSign -> [Set CspSymbol]
sym_of (GenCspCASL _) = CspCASLSign -> [Set CspSymbol]
symSets
      symKind :: GenCspCASL a -> CspSymbol -> String
symKind (GenCspCASL _) = Doc -> String
forall a. Show a => a -> String
show (Doc -> String) -> (CspSymbol -> Doc) -> CspSymbol -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CspSymbType -> Doc
forall a. Pretty a => a -> Doc
pretty (CspSymbType -> Doc)
-> (CspSymbol -> CspSymbType) -> CspSymbol -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CspSymbol -> CspSymbType
cspSymbType
      print_named :: GenCspCASL a -> Named CspCASLSen -> Doc
print_named (GenCspCASL _) = Named CspCASLSen -> Doc
forall f. FormExtension f => Named (FORMULA f) -> Doc
printTheoryFormula

-- | Syntax of CspCASL
instance Show a => Syntax (GenCspCASL a)
    CspBasicSpec -- basic_spec
    CspSymbol
    CspSymbItems
    CspSymbMapItems
    where
      parse_symb_items :: GenCspCASL a -> Maybe (PrefixMap -> AParser st CspSymbItems)
parse_symb_items (GenCspCASL _) = (PrefixMap -> AParser st CspSymbItems)
-> Maybe (PrefixMap -> AParser st CspSymbItems)
forall a. a -> Maybe a
Just ((PrefixMap -> AParser st CspSymbItems)
 -> Maybe (PrefixMap -> AParser st CspSymbItems))
-> (AParser st CspSymbItems
    -> PrefixMap -> AParser st CspSymbItems)
-> AParser st CspSymbItems
-> Maybe (PrefixMap -> AParser st CspSymbItems)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AParser st CspSymbItems -> PrefixMap -> AParser st CspSymbItems
forall a b. a -> b -> a
const (AParser st CspSymbItems
 -> Maybe (PrefixMap -> AParser st CspSymbItems))
-> AParser st CspSymbItems
-> Maybe (PrefixMap -> AParser st CspSymbItems)
forall a b. (a -> b) -> a -> b
$ AParser st CspSymbItems
forall st. AParser st CspSymbItems
cspSymbItems
      parse_symb_map_items :: GenCspCASL a -> Maybe (PrefixMap -> AParser st CspSymbMapItems)
parse_symb_map_items (GenCspCASL _) = (PrefixMap -> AParser st CspSymbMapItems)
-> Maybe (PrefixMap -> AParser st CspSymbMapItems)
forall a. a -> Maybe a
Just ((PrefixMap -> AParser st CspSymbMapItems)
 -> Maybe (PrefixMap -> AParser st CspSymbMapItems))
-> (AParser st CspSymbMapItems
    -> PrefixMap -> AParser st CspSymbMapItems)
-> AParser st CspSymbMapItems
-> Maybe (PrefixMap -> AParser st CspSymbMapItems)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AParser st CspSymbMapItems
-> PrefixMap -> AParser st CspSymbMapItems
forall a b. a -> b -> a
const (AParser st CspSymbMapItems
 -> Maybe (PrefixMap -> AParser st CspSymbMapItems))
-> AParser st CspSymbMapItems
-> Maybe (PrefixMap -> AParser st CspSymbMapItems)
forall a b. (a -> b) -> a -> b
$ AParser st CspSymbMapItems
forall st. AParser st CspSymbMapItems
cspSymbMapItems
      parse_basic_spec :: GenCspCASL a -> Maybe (PrefixMap -> AParser st CspBasicSpec)
parse_basic_spec (GenCspCASL _) = (PrefixMap -> AParser st CspBasicSpec)
-> Maybe (PrefixMap -> AParser st CspBasicSpec)
forall a. a -> Maybe a
Just ((PrefixMap -> AParser st CspBasicSpec)
 -> Maybe (PrefixMap -> AParser st CspBasicSpec))
-> (PrefixMap -> AParser st CspBasicSpec)
-> Maybe (PrefixMap -> AParser st CspBasicSpec)
forall a b. (a -> b) -> a -> b
$ [String] -> PrefixMap -> AParser st CspBasicSpec
forall f s b st.
(TermParser f, AParsable s, AParsable b) =>
[String] -> PrefixMap -> AParser st (BASIC_SPEC b s f)
basicSpec [String]
startCspKeywords

-- lattices (for sublogics) missing

class Show a => CspCASLSemantics a where
  cspProvers :: a
    -> [Prover SignCSP.CspCASLSign SignCSP.CspCASLSen
        CspCASL_Morphism.CspCASLMorphism () ()]
  cspProvers _ = []

{- further dummy types for the trace of the failure semantics can be added
   and made an instance of CspCASLSemantics.
   "identity" Comorphisms between these different logics still need to be
   defined.
-}

instance CspCASLSemantics ()

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

traceCspCASL :: GenCspCASL Trace
traceCspCASL :: GenCspCASL Trace
traceCspCASL = Trace -> GenCspCASL Trace
forall a. a -> GenCspCASL a
GenCspCASL Trace
Trace

failureCspCASL :: GenCspCASL Failure
failureCspCASL :: GenCspCASL Failure
failureCspCASL = Failure -> GenCspCASL Failure
forall a. a -> GenCspCASL a
GenCspCASL Failure
Failure

instance CspCASLSemantics Trace where
    cspProvers :: Trace -> [Prover CspCASLSign CspCASLSen CspCASLMorphism () ()]
cspProvers _ = [Prover CspCASLSign CspCASLSen CspCASLMorphism () ()
cspCASLProver]

instance CspCASLSemantics Failure

-- | Instance of Logic for CspCASL
instance CspCASLSemantics a => Logic (GenCspCASL a)
    -- Sublogics (missing)
    ()
    -- basic_spec
    CspBasicSpec
    -- sentence
    SignCSP.CspCASLSen
    -- symb_items
    CspSymbItems
    -- symb_map_items
    CspSymbMapItems
    -- signature
    SignCSP.CspCASLSign
    -- morphism
    CspCASL_Morphism.CspCASLMorphism
    CspSymbol
    CspRawSymbol
    -- proof_tree (missing)
    ()
    where
      stability :: GenCspCASL a -> Stability
stability (GenCspCASL _) = Stability
Testing
      data_logic :: GenCspCASL a -> Maybe AnyLogic
data_logic (GenCspCASL _) = AnyLogic -> Maybe AnyLogic
forall a. a -> Maybe a
Just (CASL -> AnyLogic
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> AnyLogic
Logic CASL
CASL)
      empty_proof_tree :: GenCspCASL a -> ()
empty_proof_tree _ = ()
      provers :: GenCspCASL a
-> [Prover CspCASLSign CspCASLSen CspCASLMorphism () ()]
provers (GenCspCASL _) = a -> [Prover CspCASLSign CspCASLSen CspCASLMorphism () ()]
forall a.
CspCASLSemantics a =>
a -> [Prover CspCASLSign CspCASLSen CspCASLMorphism () ()]
cspProvers (a
forall a. HasCallStack => a
undefined :: a)

-- | Static Analysis for CspCASL
instance Show a => StaticAnalysis (GenCspCASL a)
    -- basic_spec
    CspBasicSpec
    -- sentence
    SignCSP.CspCASLSen
    -- symb_items
    CspSymbItems
    -- symb_map_items
    CspSymbMapItems
    -- signature
    SignCSP.CspCASLSign
    -- morphism
    CspCASL_Morphism.CspCASLMorphism
    CspSymbol
    CspRawSymbol
    where
      basic_analysis :: GenCspCASL a
-> Maybe
     ((CspBasicSpec, CspCASLSign, GlobalAnnos)
      -> Result
           (CspBasicSpec, ExtSign CspCASLSign CspSymbol, [Named CspCASLSen]))
basic_analysis (GenCspCASL _) = ((CspBasicSpec, CspCASLSign, GlobalAnnos)
 -> Result
      (CspBasicSpec, ExtSign CspCASLSign CspSymbol, [Named CspCASLSen]))
-> Maybe
     ((CspBasicSpec, CspCASLSign, GlobalAnnos)
      -> Result
           (CspBasicSpec, ExtSign CspCASLSign CspSymbol, [Named CspCASLSen]))
forall a. a -> Maybe a
Just (CspBasicSpec, CspCASLSign, GlobalAnnos)
-> Result
     (CspBasicSpec, ExtSign CspCASLSign CspSymbol, [Named CspCASLSen])
basicAnalysisCspCASL
      stat_symb_items :: GenCspCASL a
-> CspCASLSign -> [CspSymbItems] -> Result [CspRawSymbol]
stat_symb_items (GenCspCASL _) = CspCASLSign -> [CspSymbItems] -> Result [CspRawSymbol]
cspStatSymbItems
      stat_symb_map_items :: GenCspCASL a
-> CspCASLSign
-> Maybe CspCASLSign
-> [CspSymbMapItems]
-> Result (EndoMap CspRawSymbol)
stat_symb_map_items (GenCspCASL _) = CspCASLSign
-> Maybe CspCASLSign
-> [CspSymbMapItems]
-> Result (EndoMap CspRawSymbol)
cspStatSymbMapItems
      id_to_raw :: GenCspCASL a -> Id -> CspRawSymbol
id_to_raw (GenCspCASL _) = Id -> CspRawSymbol
idToCspRaw
      symbol_to_raw :: GenCspCASL a -> CspSymbol -> CspRawSymbol
symbol_to_raw (GenCspCASL _) = CspSymbol -> CspRawSymbol
ACspSymbol
      matches :: GenCspCASL a -> CspSymbol -> CspRawSymbol -> Bool
matches (GenCspCASL _) = CspSymbol -> CspRawSymbol -> Bool
cspMatches

      empty_signature :: GenCspCASL a -> CspCASLSign
empty_signature (GenCspCASL _) = CspCASLSign
SignCSP.emptyCspCASLSign
      is_subsig :: GenCspCASL a -> CspCASLSign -> CspCASLSign -> Bool
is_subsig (GenCspCASL _) = CspCASLSign -> CspCASLSign -> Bool
SignCSP.isCspCASLSubSig
      subsig_inclusion :: GenCspCASL a
-> CspCASLSign -> CspCASLSign -> Result CspCASLMorphism
subsig_inclusion (GenCspCASL _) = CspCASLSign -> CspCASLSign -> Result CspCASLMorphism
cspSubsigInclusion
      signature_union :: GenCspCASL a -> CspCASLSign -> CspCASLSign -> Result CspCASLSign
signature_union (GenCspCASL _) = CspCASLSign -> CspCASLSign -> Result CspCASLSign
SignCSP.unionCspCASLSign
      signatureDiff :: GenCspCASL a -> CspCASLSign -> CspCASLSign -> Result CspCASLSign
signatureDiff (GenCspCASL _) s :: CspCASLSign
s = CspCASLSign -> Result CspCASLSign
forall (m :: * -> *) a. Monad m => a -> m a
return (CspCASLSign -> Result CspCASLSign)
-> (CspCASLSign -> CspCASLSign)
-> CspCASLSign
-> Result CspCASLSign
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (CspSign -> CspSign -> CspSign)
-> CspCASLSign -> CspCASLSign -> CspCASLSign
forall e f. (e -> e -> e) -> Sign f e -> Sign f e -> Sign f e
diffSig CspSign -> CspSign -> CspSign
SignCSP.diffCspSig CspCASLSign
s
      morphism_union :: GenCspCASL a
-> CspCASLMorphism -> CspCASLMorphism -> Result CspCASLMorphism
morphism_union (GenCspCASL _) =
          (CspCASLMorphism -> CspCASLMorphism -> Result CspAddMorphism)
-> (CspSign -> CspSign -> CspSign)
-> CspCASLMorphism
-> CspCASLMorphism
-> Result CspCASLMorphism
forall f e m.
(Morphism f e m -> Morphism f e m -> Result m)
-> (e -> e -> e)
-> Morphism f e m
-> Morphism f e m
-> Result (Morphism f e m)
morphismUnion CspCASLMorphism -> CspCASLMorphism -> Result CspAddMorphism
CspCASL_Morphism.cspAddMorphismUnion
                        CspSign -> CspSign -> CspSign
SignCSP.cspSignUnion

      induced_from_morphism :: GenCspCASL a
-> EndoMap CspRawSymbol -> CspCASLSign -> Result CspCASLMorphism
induced_from_morphism (GenCspCASL _) = EndoMap CspRawSymbol -> CspCASLSign -> Result CspCASLMorphism
cspInducedFromMorphism
      induced_from_to_morphism :: GenCspCASL a
-> EndoMap CspRawSymbol
-> ExtSign CspCASLSign CspSymbol
-> ExtSign CspCASLSign CspSymbol
-> Result CspCASLMorphism
induced_from_to_morphism (GenCspCASL _) = EndoMap CspRawSymbol
-> ExtSign CspCASLSign CspSymbol
-> ExtSign CspCASLSign CspSymbol
-> Result CspCASLMorphism
cspInducedFromToMorphism
      cogenerated_sign :: GenCspCASL a
-> Set CspSymbol -> CspCASLSign -> Result CspCASLMorphism
cogenerated_sign (GenCspCASL _) = Set CspSymbol -> CspCASLSign -> Result CspCASLMorphism
cspCogeneratedSign
      generated_sign :: GenCspCASL a
-> Set CspSymbol -> CspCASLSign -> Result CspCASLMorphism
generated_sign (GenCspCASL _) = Set CspSymbol -> CspCASLSign -> Result CspCASLMorphism
cspGeneratedSign