{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}
{- |
Module      :  ./Comorphisms/ExtModal2ExtModalNoSubsorts.hs
Description :  coding out subsorting
Copyright   :  (c) C. Maeder DFKI GmbH 2012
License     :  GPLv2 or higher, see LICENSE.txt

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

Coding out subsorting (SubPCFOL= -> PCFOL=),
   following Chap. III:3.1 of the CASL Reference Manual
-}

module Comorphisms.ExtModal2ExtModalNoSubsorts where

import Logic.Logic
import Logic.Comorphism

import qualified Data.Set as Set

import Common.AS_Annotation

-- CASL
import CASL.AS_Basic_CASL
import CASL.Sign
import CASL.Morphism
import CASL.Inject
import CASL.Project
import CASL.Monoton
import CASL.Sublogic

import ExtModal.Logic_ExtModal
import ExtModal.AS_ExtModal
import ExtModal.StatAna
import ExtModal.Sublogic as EM

import Comorphisms.CASL2PCFOL

-- | The identity of the comorphism
data ExtModal2ExtModalNoSubsorts = ExtModal2ExtModalNoSubsorts deriving Int -> ExtModal2ExtModalNoSubsorts -> ShowS
[ExtModal2ExtModalNoSubsorts] -> ShowS
ExtModal2ExtModalNoSubsorts -> String
(Int -> ExtModal2ExtModalNoSubsorts -> ShowS)
-> (ExtModal2ExtModalNoSubsorts -> String)
-> ([ExtModal2ExtModalNoSubsorts] -> ShowS)
-> Show ExtModal2ExtModalNoSubsorts
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ExtModal2ExtModalNoSubsorts] -> ShowS
$cshowList :: [ExtModal2ExtModalNoSubsorts] -> ShowS
show :: ExtModal2ExtModalNoSubsorts -> String
$cshow :: ExtModal2ExtModalNoSubsorts -> String
showsPrec :: Int -> ExtModal2ExtModalNoSubsorts -> ShowS
$cshowsPrec :: Int -> ExtModal2ExtModalNoSubsorts -> ShowS
Show

instance Language ExtModal2ExtModalNoSubsorts -- default definition is okay

instance Comorphism ExtModal2ExtModalNoSubsorts
               ExtModal ExtModalSL EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS
               SYMB_MAP_ITEMS ExtModalSign ExtModalMorph
               Symbol RawSymbol ()
               ExtModal ExtModalSL EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS
               SYMB_MAP_ITEMS ExtModalSign ExtModalMorph
               Symbol RawSymbol () where
    sourceLogic :: ExtModal2ExtModalNoSubsorts -> ExtModal
sourceLogic ExtModal2ExtModalNoSubsorts = ExtModal
ExtModal
    sourceSublogic :: ExtModal2ExtModalNoSubsorts -> ExtModalSL
sourceSublogic ExtModal2ExtModalNoSubsorts = Sublogic -> ExtModalSL
forall a. a -> CASL_SL a
mkTop Sublogic
maxSublogic
    targetLogic :: ExtModal2ExtModalNoSubsorts -> ExtModal
targetLogic ExtModal2ExtModalNoSubsorts = ExtModal
ExtModal
    mapSublogic :: ExtModal2ExtModalNoSubsorts -> ExtModalSL -> Maybe ExtModalSL
mapSublogic ExtModal2ExtModalNoSubsorts sl :: ExtModalSL
sl = ExtModalSL -> Maybe ExtModalSL
forall a. a -> Maybe a
Just
      (ExtModalSL -> Maybe ExtModalSL) -> ExtModalSL -> Maybe ExtModalSL
forall a b. (a -> b) -> a -> b
$ if ExtModalSL -> Bool
forall a. CASL_SL a -> Bool
has_sub ExtModalSL
sl then -- subsorting is coded out
            ExtModalSL
sl { sub_features :: SubsortingFeatures
sub_features = SubsortingFeatures
NoSub
               , has_part :: Bool
has_part = Bool
True
               , which_logic :: CASL_Formulas
which_logic = CASL_Formulas -> CASL_Formulas -> CASL_Formulas
forall a. Ord a => a -> a -> a
max CASL_Formulas
Horn (CASL_Formulas -> CASL_Formulas) -> CASL_Formulas -> CASL_Formulas
forall a b. (a -> b) -> a -> b
$ ExtModalSL -> CASL_Formulas
forall a. CASL_SL a -> CASL_Formulas
which_logic ExtModalSL
sl
               , has_eq :: Bool
has_eq = Bool
True}
        else ExtModalSL
sl
    map_theory :: ExtModal2ExtModalNoSubsorts
-> (ExtModalSign, [Named ExtModalFORMULA])
-> Result (ExtModalSign, [Named ExtModalFORMULA])
map_theory ExtModal2ExtModalNoSubsorts = (ExtModalSign -> Result (ExtModalSign, [Named ExtModalFORMULA]))
-> (ExtModalSign -> ExtModalFORMULA -> Result ExtModalFORMULA)
-> (ExtModalSign, [Named ExtModalFORMULA])
-> Result (ExtModalSign, [Named ExtModalFORMULA])
forall (m :: * -> *) sign1 sign2 sentence2 sentence1.
Monad m =>
(sign1 -> m (sign2, [Named sentence2]))
-> (sign1 -> sentence1 -> m sentence2)
-> (sign1, [Named sentence1])
-> m (sign2, [Named sentence2])
mkTheoryMapping (\ sig :: ExtModalSign
sig ->
      let e :: ExtModalSign
e = ExtModalSign -> ExtModalSign
forall f e. Sign f e -> Sign f e
encodeSig ExtModalSign
sig in
      (ExtModalSign, [Named ExtModalFORMULA])
-> Result (ExtModalSign, [Named ExtModalFORMULA])
forall (m :: * -> *) a. Monad m => a -> m a
return (ExtModalSign
e, (Named ExtModalFORMULA -> Named ExtModalFORMULA)
-> [Named ExtModalFORMULA] -> [Named ExtModalFORMULA]
forall a b. (a -> b) -> [a] -> [b]
map ((ExtModalFORMULA -> ExtModalFORMULA)
-> Named ExtModalFORMULA -> Named ExtModalFORMULA
forall s t a. (s -> t) -> SenAttr s a -> SenAttr t a
mapNamed ExtModalFORMULA -> ExtModalFORMULA
injEMFormula) (ExtModalSign -> [Named ExtModalFORMULA]
forall f e. Sign f e -> [Named (FORMULA f)]
monotonicities ExtModalSign
sig)
                 [Named ExtModalFORMULA]
-> [Named ExtModalFORMULA] -> [Named ExtModalFORMULA]
forall a. [a] -> [a] -> [a]
++ ExtModalSign -> [Named ExtModalFORMULA]
forall f e. TermExtension f => Sign f e -> [Named (FORMULA f)]
generateAxioms ExtModalSign
sig))
      (ExtModal2ExtModalNoSubsorts
-> ExtModalSign -> ExtModalFORMULA -> Result ExtModalFORMULA
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid -> sign1 -> sentence1 -> Result sentence2
map_sentence ExtModal2ExtModalNoSubsorts
ExtModal2ExtModalNoSubsorts)
    map_morphism :: ExtModal2ExtModalNoSubsorts
-> ExtModalMorph -> Result ExtModalMorph
map_morphism ExtModal2ExtModalNoSubsorts mor :: ExtModalMorph
mor = ExtModalMorph -> Result ExtModalMorph
forall (m :: * -> *) a. Monad m => a -> m a
return
      (ExtModalMorph
mor { msource :: ExtModalSign
msource = ExtModalSign -> ExtModalSign
forall f e. Sign f e -> Sign f e
encodeSig (ExtModalSign -> ExtModalSign) -> ExtModalSign -> ExtModalSign
forall a b. (a -> b) -> a -> b
$ ExtModalMorph -> ExtModalSign
forall f e m. Morphism f e m -> Sign f e
msource ExtModalMorph
mor,
              mtarget :: ExtModalSign
mtarget = ExtModalSign -> ExtModalSign
forall f e. Sign f e -> Sign f e
encodeSig (ExtModalSign -> ExtModalSign) -> ExtModalSign -> ExtModalSign
forall a b. (a -> b) -> a -> b
$ ExtModalMorph -> ExtModalSign
forall f e m. Morphism f e m -> Sign f e
mtarget ExtModalMorph
mor })
    map_sentence :: ExtModal2ExtModalNoSubsorts
-> ExtModalSign -> ExtModalFORMULA -> Result ExtModalFORMULA
map_sentence ExtModal2ExtModalNoSubsorts _ =
      ExtModalFORMULA -> Result ExtModalFORMULA
forall (m :: * -> *) a. Monad m => a -> m a
return (ExtModalFORMULA -> Result ExtModalFORMULA)
-> (ExtModalFORMULA -> ExtModalFORMULA)
-> ExtModalFORMULA
-> Result ExtModalFORMULA
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ExtModalFORMULA -> ExtModalFORMULA
projEMFormula (ExtModalFORMULA -> ExtModalFORMULA)
-> (ExtModalFORMULA -> ExtModalFORMULA)
-> ExtModalFORMULA
-> ExtModalFORMULA
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ExtModalFORMULA -> ExtModalFORMULA
injEMFormula
    map_symbol :: ExtModal2ExtModalNoSubsorts -> ExtModalSign -> Symbol -> Set Symbol
map_symbol ExtModal2ExtModalNoSubsorts _ = Symbol -> Set Symbol
forall a. a -> Set a
Set.singleton (Symbol -> Set Symbol)
-> (Symbol -> Symbol) -> Symbol -> Set Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> Symbol
forall a. a -> a
id
    has_model_expansion :: ExtModal2ExtModalNoSubsorts -> Bool
has_model_expansion ExtModal2ExtModalNoSubsorts = Bool
True
    is_weakly_amalgamable :: ExtModal2ExtModalNoSubsorts -> Bool
is_weakly_amalgamable ExtModal2ExtModalNoSubsorts = Bool
True

projEMFormula :: FORMULA EM_FORMULA -> FORMULA EM_FORMULA
projEMFormula :: ExtModalFORMULA -> ExtModalFORMULA
projEMFormula = OpKind
-> (EM_FORMULA -> EM_FORMULA) -> ExtModalFORMULA -> ExtModalFORMULA
forall f.
TermExtension f =>
OpKind -> (f -> f) -> FORMULA f -> FORMULA f
projFormula OpKind
Partial EM_FORMULA -> EM_FORMULA
projEM

projEM :: EM_FORMULA -> EM_FORMULA
projEM :: EM_FORMULA -> EM_FORMULA
projEM = (ExtModalFORMULA -> ExtModalFORMULA) -> EM_FORMULA -> EM_FORMULA
mapExtForm ExtModalFORMULA -> ExtModalFORMULA
projEMFormula

injEMFormula :: FORMULA EM_FORMULA -> FORMULA EM_FORMULA
injEMFormula :: ExtModalFORMULA -> ExtModalFORMULA
injEMFormula = (EM_FORMULA -> EM_FORMULA) -> ExtModalFORMULA -> ExtModalFORMULA
forall f. TermExtension f => (f -> f) -> FORMULA f -> FORMULA f
injFormula EM_FORMULA -> EM_FORMULA
injEM

injEM :: EM_FORMULA -> EM_FORMULA
injEM :: EM_FORMULA -> EM_FORMULA
injEM = (ExtModalFORMULA -> ExtModalFORMULA) -> EM_FORMULA -> EM_FORMULA
mapExtForm ExtModalFORMULA -> ExtModalFORMULA
injEMFormula