THFP_P2THFP.hs revision 880945fae9c3f61341f1cd94439c802b7a0af194
e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}
e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder{- |
e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian MaederModule : $Header$
45ad02e03fb913ba373d8fdcfe50244be3df31eaChristian MaederDescription : Comorphism from THFP_P to THFP
e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian MaederCopyright : (c) J. von Schroeder, DFKI Bremen 2012
e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian MaederLicense : GPLv2 or higher, see LICENSE.txt
e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder
e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian MaederMaintainer : J. von Schroeder <j.von_schroeder@dfki.de>
e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian MaederStability : provisional
45ad02e03fb913ba373d8fdcfe50244be3df31eaChristian MaederPortability : non-portable (imports Logic.Logic)
45ad02e03fb913ba373d8fdcfe50244be3df31eaChristian Maeder
45ad02e03fb913ba373d8fdcfe50244be3df31eaChristian MaederThe comorphism from THFP to THF0.
45ad02e03fb913ba373d8fdcfe50244be3df31eaChristian Maeder-}
45ad02e03fb913ba373d8fdcfe50244be3df31eaChristian Maeder
45ad02e03fb913ba373d8fdcfe50244be3df31eaChristian Maedermodule Comorphisms.THFP_P2THFP where
45ad02e03fb913ba373d8fdcfe50244be3df31eaChristian Maeder
45ad02e03fb913ba373d8fdcfe50244be3df31eaChristian Maederimport Logic.Logic as Logic
45ad02e03fb913ba373d8fdcfe50244be3df31eaChristian Maederimport Logic.Comorphism
45ad02e03fb913ba373d8fdcfe50244be3df31eaChristian Maeder
45ad02e03fb913ba373d8fdcfe50244be3df31eaChristian Maederimport Common.ProofTree
45ad02e03fb913ba373d8fdcfe50244be3df31eaChristian Maederimport Common.Result
45ad02e03fb913ba373d8fdcfe50244be3df31eaChristian Maederimport Common.AS_Annotation (Named)
45ad02e03fb913ba373d8fdcfe50244be3df31eaChristian Maeder
e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maederimport THF.Logic_THF
e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maederimport THF.Cons
e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maederimport THF.Sign
e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maederimport qualified THF.Sublogic as SL
e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maederimport THF.As
10b02b2343246df6773585636fe3ddbefa3b6a1bChristian Maederimport THF.Utils
e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maederimport THF.Poly
e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder
e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maederdata THFP_P2THFP = THFP_P2THFP deriving Show
ee31a8a5f5d786472f2b5dfb271b38e6d401fa35Christian Maeder
ee31a8a5f5d786472f2b5dfb271b38e6d401fa35Christian Maederinstance Language THFP_P2THFP
ee31a8a5f5d786472f2b5dfb271b38e6d401fa35Christian Maeder
e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maederinstance Comorphism THFP_P2THFP
ee31a8a5f5d786472f2b5dfb271b38e6d401fa35Christian Maeder THF SL.THFSl
e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder BasicSpecTHF THFFormula () ()
e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder SignTHF MorphismTHF SymbolTHF () ProofTree
ee31a8a5f5d786472f2b5dfb271b38e6d401fa35Christian Maeder THF SL.THFSl
ee31a8a5f5d786472f2b5dfb271b38e6d401fa35Christian Maeder BasicSpecTHF THFFormula () ()
e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder SignTHF MorphismTHF SymbolTHF () ProofTree where
e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder sourceLogic THFP_P2THFP = THF
ee31a8a5f5d786472f2b5dfb271b38e6d401fa35Christian Maeder sourceSublogic THFP_P2THFP = SL.tHFP_P
ee31a8a5f5d786472f2b5dfb271b38e6d401fa35Christian Maeder targetLogic THFP_P2THFP = THF
e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder mapSublogic THFP_P2THFP _ = Just SL.tHFP
ee31a8a5f5d786472f2b5dfb271b38e6d401fa35Christian Maeder map_theory THFP_P2THFP = trans_theory
e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder has_model_expansion THFP_P2THFP = True
e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder
e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maedertrans_theory :: (SignTHF,[Named THFFormula])
e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder -> Result (SignTHF,[Named THFFormula])
e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maedertrans_theory (sig, sentences1) = do
e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder (cs,sentences) <- infer (consts sig) sentences1
e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder let sig1 = sig {consts = cs}
e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder return (recreateSymbols sig1,sentences)
e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder