ExtModal2ExtModalTotal.hs revision 683ee7dc6ecd65a50eb224cf5fa32ca39d907a8c
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maeder{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maeder{- |
914b90f3d6644fd464c5b26712b65d515a58c037Christian MaederModule : $Header$
914b90f3d6644fd464c5b26712b65d515a58c037Christian MaederDescription : coding out subsorting
914b90f3d6644fd464c5b26712b65d515a58c037Christian MaederCopyright : (c) C. Maeder DFKI GmbH 2012
914b90f3d6644fd464c5b26712b65d515a58c037Christian MaederLicense : GPLv2 or higher, see LICENSE.txt
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maeder
914b90f3d6644fd464c5b26712b65d515a58c037Christian MaederMaintainer : Christian.Maeder@dfki.de
914b90f3d6644fd464c5b26712b65d515a58c037Christian MaederStability : provisional
914b90f3d6644fd464c5b26712b65d515a58c037Christian MaederPortability : non-portable (imports Logic.Logic)
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maeder
914b90f3d6644fd464c5b26712b65d515a58c037Christian MaederCoding out subsorting (SubPCFOL= -> PCFOL=),
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maeder following Chap. III:3.1 of the CASL Reference Manual
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maeder-}
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maeder
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maedermodule Comorphisms.ExtModal2ExtModalTotal where
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maeder
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maederimport Logic.Logic
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maederimport Logic.Comorphism
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maeder
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maederimport qualified Data.Map as Map
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maederimport qualified Data.Set as Set
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maeder
683ee7dc6ecd65a50eb224cf5fa32ca39d907a8cChristian Maederimport qualified Common.Lib.MapSet as MapSet
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maederimport Common.AS_Annotation
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maederimport Common.ProofUtils
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maeder
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maeder-- CASL
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maederimport CASL.AS_Basic_CASL
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maederimport CASL.Fold
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maederimport CASL.Morphism
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maederimport CASL.Sign
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maederimport CASL.Simplify
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maeder
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maederimport ExtModal.Logic_ExtModal
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maederimport ExtModal.AS_ExtModal
683ee7dc6ecd65a50eb224cf5fa32ca39d907a8cChristian Maederimport ExtModal.ExtModalSign
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maederimport ExtModal.StatAna
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maederimport ExtModal.Sublogic as EM
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maeder
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maederimport Comorphisms.CASL2SubCFOL
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maeder
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maeder-- | The identity of the comorphism
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maederdata ExtModal2ExtModalTotal = ExtModal2ExtModalTotal deriving Show
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maeder
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maederinstance Language ExtModal2ExtModalTotal -- default definition is okay
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maeder
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maederinstance Comorphism ExtModal2ExtModalTotal
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maeder ExtModal Sublogic EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maeder SYMB_MAP_ITEMS ExtModalSign ExtModalMorph
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maeder Symbol RawSymbol ()
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maeder ExtModal Sublogic EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maeder SYMB_MAP_ITEMS ExtModalSign ExtModalMorph
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maeder Symbol RawSymbol () where
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maeder sourceLogic ExtModal2ExtModalTotal = ExtModal
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maeder sourceSublogic ExtModal2ExtModalTotal = maxSublogic
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maeder targetLogic ExtModal2ExtModalTotal = ExtModal
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maeder mapSublogic ExtModal2ExtModalTotal = Just
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maeder map_theory ExtModal2ExtModalTotal (sig, sens) = let
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maeder bsrts = emsortsWithBottom sig
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maeder sens1 = generateAxioms True bsrts sig
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maeder sens2 = map (mapNamed (simplifyEMFormula . codeEMFormula bsrts)) sens
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maeder in return
683ee7dc6ecd65a50eb224cf5fa32ca39d907a8cChristian Maeder ( emEncodeSig bsrts sig
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maeder , nameAndDisambiguate $ sens1 ++ sens2)
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maeder map_morphism ExtModal2ExtModalTotal mor@Morphism
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maeder {msource = src, mtarget = tar}
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maeder = return
683ee7dc6ecd65a50eb224cf5fa32ca39d907a8cChristian Maeder mor { msource = emEncodeSig (emsortsWithBottom src) src
683ee7dc6ecd65a50eb224cf5fa32ca39d907a8cChristian Maeder , mtarget = emEncodeSig (emsortsWithBottom tar) tar
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maeder , op_map = Map.map (\ (i, _) -> (i, Total)) $ op_map mor }
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maeder map_sentence ExtModal2ExtModalTotal sig sen = let
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maeder bsrts = emsortsWithBottom sig
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maeder in return $ simplifyEMFormula $ codeEMFormula bsrts sen
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maeder map_symbol ExtModal2ExtModalTotal _ s =
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maeder Set.singleton s { symbType = totalizeSymbType $ symbType s }
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maeder has_model_expansion ExtModal2ExtModalTotal = True
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maeder is_weakly_amalgamable ExtModal2ExtModalTotal = True
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maeder
683ee7dc6ecd65a50eb224cf5fa32ca39d907a8cChristian MaederemEncodeSig :: Set.Set SORT -> Sign f EModalSign -> Sign f EModalSign
683ee7dc6ecd65a50eb224cf5fa32ca39d907a8cChristian MaederemEncodeSig bsrts sig = (encodeSig bsrts sig)
683ee7dc6ecd65a50eb224cf5fa32ca39d907a8cChristian Maeder { extendedInfo = let extInfo = extendedInfo sig in
683ee7dc6ecd65a50eb224cf5fa32ca39d907a8cChristian Maeder extInfo { flexOps = MapSet.map mkTotal $ flexOps extInfo }}
683ee7dc6ecd65a50eb224cf5fa32ca39d907a8cChristian Maeder
914b90f3d6644fd464c5b26712b65d515a58c037Christian MaederemsortsWithBottom :: Sign f e -> Set.Set SORT
914b90f3d6644fd464c5b26712b65d515a58c037Christian MaederemsortsWithBottom sig = sortsWithBottom NoMembershipOrCast sig Set.empty
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maeder
914b90f3d6644fd464c5b26712b65d515a58c037Christian MaedersimplifyEM :: EM_FORMULA -> EM_FORMULA
914b90f3d6644fd464c5b26712b65d515a58c037Christian MaedersimplifyEM = mapExtForm simplifyEMFormula
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maeder
914b90f3d6644fd464c5b26712b65d515a58c037Christian MaedersimplifyEMFormula :: FORMULA EM_FORMULA -> FORMULA EM_FORMULA
914b90f3d6644fd464c5b26712b65d515a58c037Christian MaedersimplifyEMFormula = simplifyFormula simplifyEM
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maeder
914b90f3d6644fd464c5b26712b65d515a58c037Christian MaedercodeEM :: Set.Set SORT -> EM_FORMULA -> EM_FORMULA
914b90f3d6644fd464c5b26712b65d515a58c037Christian MaedercodeEM = mapExtForm . codeEMFormula
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maeder
914b90f3d6644fd464c5b26712b65d515a58c037Christian MaedercodeEMFormula :: Set.Set SORT -> FORMULA EM_FORMULA -> FORMULA EM_FORMULA
914b90f3d6644fd464c5b26712b65d515a58c037Christian MaedercodeEMFormula bsrts = foldFormula (codeRecord True bsrts $ codeEM bsrts)