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

a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa{- |

a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen KuksaModule : ./Comorphisms/ExtModal2ExtModalNoSubsorts.hs

a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen KuksaDescription : coding out subsorting

a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen KuksaCopyright : (c) C. Maeder DFKI GmbH 2012

a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen KuksaLicense : GPLv2 or higher, see LICENSE.txt

a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa

a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen KuksaMaintainer : Christian.Maeder@dfki.de

a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen KuksaStability : provisional

a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen KuksaPortability : non-portable (imports Logic.Logic)

a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa

a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen KuksaCoding out subsorting (SubPCFOL= -> PCFOL=),

a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa following Chap. III:3.1 of the CASL Reference Manual

a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa-}

a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa

a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksamodule Comorphisms.ExtModal2ExtModalNoSubsorts where

a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa

a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksaimport Logic.Logic

a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksaimport Logic.Comorphism

a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa

a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksaimport qualified Data.Set as Set

a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa

a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksaimport Common.AS_Annotation

a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa

a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa-- CASL

a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksaimport CASL.AS_Basic_CASL

a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksaimport CASL.Sign

a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksaimport CASL.Morphism

a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksaimport 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 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

sourceSublogic ExtModal2ExtModalNoSubsorts = mkTop maxSublogic

targetLogic ExtModal2ExtModalNoSubsorts = ExtModal

mapSublogic ExtModal2ExtModalNoSubsorts sl = Just

$ if has_sub sl then -- subsorting is coded out

sl { sub_features = NoSub

, has_part = True

, which_logic = max Horn $ which_logic sl

, has_eq = True}

else sl

map_theory ExtModal2ExtModalNoSubsorts = mkTheoryMapping (\ sig ->

let e = encodeSig sig in

return (e, map (mapNamed injEMFormula) (monotonicities sig)

++ generateAxioms sig))

(map_sentence ExtModal2ExtModalNoSubsorts)

map_morphism ExtModal2ExtModalNoSubsorts mor = return

(mor { msource = encodeSig $ msource mor,

mtarget = encodeSig $ mtarget mor })

map_sentence ExtModal2ExtModalNoSubsorts _ =

return . projEMFormula . injEMFormula

map_symbol ExtModal2ExtModalNoSubsorts _ = Set.singleton . id

has_model_expansion ExtModal2ExtModalNoSubsorts = True

is_weakly_amalgamable ExtModal2ExtModalNoSubsorts = True

projEMFormula :: FORMULA EM_FORMULA -> FORMULA EM_FORMULA

projEMFormula = projFormula Partial projEM

projEM :: EM_FORMULA -> EM_FORMULA

projEM = mapExtForm projEMFormula

injEMFormula :: FORMULA EM_FORMULA -> FORMULA EM_FORMULA

injEMFormula = injFormula injEM

injEM :: EM_FORMULA -> EM_FORMULA

injEM = mapExtForm injEMFormula