THFP_P2THFP.hs revision 880945fae9c3f61341f1cd94439c802b7a0af194
e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}
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 MaederMaintainer : J. von Schroeder <j.von_schroeder@dfki.de>
e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian MaederStability : provisional
45ad02e03fb913ba373d8fdcfe50244be3df31eaChristian MaederPortability : non-portable (imports Logic.Logic)
45ad02e03fb913ba373d8fdcfe50244be3df31eaChristian MaederThe comorphism from THFP to THF0.
e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maederimport qualified THF.Sublogic as SL
e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maederdata THFP_P2THFP = THFP_P2THFP deriving Show
ee31a8a5f5d786472f2b5dfb271b38e6d401fa35Christian Maederinstance Language THFP_P2THFP
e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maederinstance Comorphism THFP_P2THFP
e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder BasicSpecTHF THFFormula () ()
e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder SignTHF MorphismTHF SymbolTHF () ProofTree
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 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)