{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances #-}
{- |
Module      :  ./Comorphisms/CommonLogicModuleElimination.hs
Description :  Comorphism from CommonLogic to CommonLogic
Copyright   :  (c) Eugen Kuksa, Uni Bremen 2011
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  eugenk@informatik.uni-bremen.de
Stability   :  experimental (not complete: typleclass-instances missing)
Portability :  non-portable (via Logic.Logic)

Translating comorphism from CommonLogic to CommonLogic in order to eliminate
modules.

-}


module Comorphisms.CommonLogicModuleElimination (
        CommonLogicModuleElimination (..)
    )
    where

import Logic.Logic as Logic
import Logic.Comorphism

import Common.ProofTree
import Common.Result
import qualified Common.AS_Annotation as AS_Anno

-- Common Logic
import CommonLogic.AS_CommonLogic
import qualified CommonLogic.Logic_CommonLogic as Logic
import qualified CommonLogic.Sign as Sign
import qualified CommonLogic.Symbol as Symbol
import qualified CommonLogic.Morphism as Mor
import qualified CommonLogic.Sublogic as Sl
import CommonLogic.ModuleElimination

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

instance Language CommonLogicModuleElimination where
  language_name :: CommonLogicModuleElimination -> String
language_name CommonLogicModuleElimination = "CommonLogicModuleElimination"

instance Comorphism
    CommonLogicModuleElimination -- comorphism
    Logic.CommonLogic       -- lid domain
    Sl.CommonLogicSL        -- sublogics codomain
    BASIC_SPEC              -- Basic spec domain
    TEXT_META               -- sentence domain
    SYMB_ITEMS              -- symb_items
    SYMB_MAP_ITEMS          -- symbol map items domain
    Sign.Sign               -- signature domain
    Mor.Morphism            -- morphism domain
    Symbol.Symbol           -- symbol domain
    Symbol.Symbol           -- rawsymbol domain
    ProofTree               -- proof tree codomain
    Logic.CommonLogic       -- lid domain
    Sl.CommonLogicSL        -- sublogics codomain
    BASIC_SPEC              -- Basic spec domain
    TEXT_META               -- sentence domain
    SYMB_ITEMS              -- symb_items
    SYMB_MAP_ITEMS          -- symbol map items domain
    Sign.Sign               -- signature domain
    Mor.Morphism            -- morphism domain
    Symbol.Symbol           -- symbol domain
    Symbol.Symbol           -- rawsymbol domain
    ProofTree               -- proof tree codomain
    where
      sourceLogic :: CommonLogicModuleElimination -> CommonLogic
sourceLogic CommonLogicModuleElimination = CommonLogic
Logic.CommonLogic
      sourceSublogic :: CommonLogicModuleElimination -> CommonLogicSL
sourceSublogic CommonLogicModuleElimination = CommonLogicSL
Sl.top
      targetLogic :: CommonLogicModuleElimination -> CommonLogic
targetLogic CommonLogicModuleElimination = CommonLogic
Logic.CommonLogic
      mapSublogic :: CommonLogicModuleElimination
-> CommonLogicSL -> Maybe CommonLogicSL
mapSublogic CommonLogicModuleElimination = CommonLogicSL -> Maybe CommonLogicSL
forall a. a -> Maybe a
Just (CommonLogicSL -> Maybe CommonLogicSL)
-> (CommonLogicSL -> CommonLogicSL)
-> CommonLogicSL
-> Maybe CommonLogicSL
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CommonLogicSL -> CommonLogicSL
mapSub
      map_theory :: CommonLogicModuleElimination
-> (Sign, [Named TEXT_META]) -> Result (Sign, [Named TEXT_META])
map_theory CommonLogicModuleElimination = (Sign, [Named TEXT_META]) -> Result (Sign, [Named TEXT_META])
mapTheory
      map_morphism :: CommonLogicModuleElimination -> Morphism -> Result Morphism
map_morphism CommonLogicModuleElimination = Morphism -> Result Morphism
mapMor
      map_sentence :: CommonLogicModuleElimination
-> Sign -> TEXT_META -> Result TEXT_META
map_sentence CommonLogicModuleElimination = Sign -> TEXT_META -> Result TEXT_META
mapSentence
      -- hasCommonLogicModuleElimination_model_expansion  = True -- TODO: check if it is really True


mapSub :: Sl.CommonLogicSL -> Sl.CommonLogicSL
mapSub :: CommonLogicSL -> CommonLogicSL
mapSub = CommonLogicSL -> CommonLogicSL
forall a. a -> a
id

mapMor :: Mor.Morphism -> Result Mor.Morphism
mapMor :: Morphism -> Result Morphism
mapMor = Morphism -> Result Morphism
forall (m :: * -> *) a. Monad m => a -> m a
return

mapSentence :: Sign.Sign -> TEXT_META -> Result TEXT_META
mapSentence :: Sign -> TEXT_META -> Result TEXT_META
mapSentence _ txt :: TEXT_META
txt = TEXT_META -> Result TEXT_META
forall (m :: * -> *) a. Monad m => a -> m a
return (TEXT_META -> Result TEXT_META) -> TEXT_META -> Result TEXT_META
forall a b. (a -> b) -> a -> b
$ TEXT_META -> TEXT_META
eliminateModules TEXT_META
txt

{- -----------------------------------------------------------------------------
MODULE ELIMINATION                                                        --
----------------------------------------------------------------------------- -}


mapTheory :: (Sign.Sign, [AS_Anno.Named TEXT_META])
             -> Result (Sign.Sign, [AS_Anno.Named TEXT_META])
mapTheory :: (Sign, [Named TEXT_META]) -> Result (Sign, [Named TEXT_META])
mapTheory (srcSign :: Sign
srcSign, srcTexts :: [Named TEXT_META]
srcTexts) =
  (Sign, [Named TEXT_META]) -> Result (Sign, [Named TEXT_META])
forall (m :: * -> *) a. Monad m => a -> m a
return (Sign
srcSign,
          (Named TEXT_META -> Named TEXT_META)
-> [Named TEXT_META] -> [Named TEXT_META]
forall a b. (a -> b) -> [a] -> [b]
map ((String -> TEXT_META -> Named TEXT_META)
-> (String, TEXT_META) -> Named TEXT_META
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry String -> TEXT_META -> Named TEXT_META
forall a s. a -> s -> SenAttr s a
AS_Anno.makeNamed ((String, TEXT_META) -> Named TEXT_META)
-> (Named TEXT_META -> (String, TEXT_META))
-> Named TEXT_META
-> Named TEXT_META
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String, TEXT_META) -> (String, TEXT_META)
elimModSnd ((String, TEXT_META) -> (String, TEXT_META))
-> (Named TEXT_META -> (String, TEXT_META))
-> Named TEXT_META
-> (String, TEXT_META)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Named TEXT_META -> (String, TEXT_META)
senAndName) [Named TEXT_META]
srcTexts)
  where senAndName :: AS_Anno.Named TEXT_META -> (String, TEXT_META)
        senAndName :: Named TEXT_META -> (String, TEXT_META)
senAndName t :: Named TEXT_META
t = (Named TEXT_META -> String
forall s a. SenAttr s a -> a
AS_Anno.senAttr Named TEXT_META
t, Named TEXT_META -> TEXT_META
forall s a. SenAttr s a -> s
AS_Anno.sentence Named TEXT_META
t)
        elimModSnd :: (String, TEXT_META) -> (String, TEXT_META)
        elimModSnd :: (String, TEXT_META) -> (String, TEXT_META)
elimModSnd (s :: String
s, t :: TEXT_META
t) = (String
s, TEXT_META -> TEXT_META
eliminateModules TEXT_META
t)