{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}

{- |

Module : ./Comorphisms/ExtModal2ExtModalTotal.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.ExtModal2ExtModalTotal where

import Logic.Logic

import Logic.Comorphism

import qualified Data.Map as Map

import qualified Data.Set as Set

import qualified Common.Lib.MapSet as MapSet

import Common.AS_Annotation

import Common.ProofUtils

-- CASL

import CASL.AS_Basic_CASL

import CASL.Fold

import CASL.Morphism

import CASL.Sign

import CASL.Simplify

import CASL.Sublogic

import CASL.Utils

import ExtModal.Logic_ExtModal

import ExtModal.AS_ExtModal

import ExtModal.ExtModalSign

import ExtModal.StatAna

import ExtModal.Sublogic as EM

import Comorphisms.CASL2SubCFOL

-- | The identity of the comorphism

data ExtModal2ExtModalTotal = ExtModal2ExtModalTotal deriving Show

instance Language ExtModal2ExtModalTotal -- default definition is okay

instance Comorphism ExtModal2ExtModalTotal

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 ExtModal2ExtModalTotal = ExtModal

sourceSublogic ExtModal2ExtModalTotal = mkTop maxSublogic

targetLogic ExtModal2ExtModalTotal = ExtModal

mapSublogic ExtModal2ExtModalTotal sl = Just

$ if has_part sl then sl

{ has_part = False -- partiality is coded out

, has_pred = True

, which_logic = max Horn $ which_logic sl

, has_eq = True} else sl

map_theory ExtModal2ExtModalTotal (sig, sens) = let

bsrts = emsortsWithBottom sig

sens1 = generateAxioms True bsrts sig

sens2 = map (mapNamed (noCondsEMFormula . simplifyEMFormula

. codeEMFormula bsrts)) sens

in return

( emEncodeSig bsrts sig

, nameAndDisambiguate $ sens1 ++ sens2)

map_morphism ExtModal2ExtModalTotal mor@Morphism

{msource = src, mtarget = tar}

= return

mor { msource = emEncodeSig (emsortsWithBottom src) src

, mtarget = emEncodeSig (emsortsWithBottom tar) tar

, op_map = Map.map (\ (i, _) -> (i, Total)) $ op_map mor }

map_sentence ExtModal2ExtModalTotal sig sen = let

bsrts = emsortsWithBottom sig

in return $ simplifyEMFormula $ codeEMFormula bsrts sen

map_symbol ExtModal2ExtModalTotal _ s =

Set.singleton s { symbType = totalizeSymbType $ symbType s }

has_model_expansion ExtModal2ExtModalTotal = True

is_weakly_amalgamable ExtModal2ExtModalTotal = True

emEncodeSig :: Set.Set SORT -> Sign f EModalSign -> Sign f EModalSign

emEncodeSig bsrts sig = (encodeSig bsrts sig)

{ extendedInfo = let extInfo = extendedInfo sig in

extInfo { flexOps = MapSet.map mkTotal $ flexOps extInfo }}

emsortsWithBottom :: Sign f e -> Set.Set SORT

emsortsWithBottom sig = sortsWithBottom NoMembershipOrCast sig Set.empty

simplifyEM :: EM_FORMULA -> EM_FORMULA

simplifyEM = mapExtForm simplifyEMFormula

simplifyEMFormula :: FORMULA EM_FORMULA -> FORMULA EM_FORMULA

simplifyEMFormula = simplifyFormula simplifyEM

noCondsEM :: EM_FORMULA -> EM_FORMULA

noCondsEM = mapExtForm noCondsEMFormula

noCondsEMFormula :: FORMULA EM_FORMULA -> FORMULA EM_FORMULA

noCondsEMFormula = codeOutConditionalF noCondsEM

codeEM :: Set.Set SORT -> EM_FORMULA -> EM_FORMULA

codeEM = mapExtForm . codeEMFormula

codeEMFormula :: Set.Set SORT -> FORMULA EM_FORMULA -> FORMULA EM_FORMULA

codeEMFormula bsrts = foldFormula (codeRecord True bsrts $ codeEM bsrts)