880945fae9c3f61341f1cd94439c802b7a0af194Jonathan von Schroeder{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}
880945fae9c3f61341f1cd94439c802b7a0af194Jonathan von SchroederDescription : Comorphism from THFP_P to THFP
880945fae9c3f61341f1cd94439c802b7a0af194Jonathan von SchroederCopyright : (c) J. von Schroeder, DFKI Bremen 2012
880945fae9c3f61341f1cd94439c802b7a0af194Jonathan von SchroederLicense : GPLv2 or higher, see LICENSE.txt
ad1df93673cf323534cdfe18981ad5daae4c90c0Jonathan von SchroederMaintainer : J. von Schroeder <jonathan.von_schroeder@dfki.de>
880945fae9c3f61341f1cd94439c802b7a0af194Jonathan von SchroederStability : provisional
880945fae9c3f61341f1cd94439c802b7a0af194Jonathan von SchroederPortability : non-portable (imports Logic.Logic)
880945fae9c3f61341f1cd94439c802b7a0af194Jonathan von SchroederThe comorphism from THFP to THF0.
880945fae9c3f61341f1cd94439c802b7a0af194Jonathan von Schroederimport qualified THF.Sublogic as SL
880945fae9c3f61341f1cd94439c802b7a0af194Jonathan von Schroederdata THFP_P2THFP = THFP_P2THFP deriving Show
880945fae9c3f61341f1cd94439c802b7a0af194Jonathan von Schroederinstance Language THFP_P2THFP
880945fae9c3f61341f1cd94439c802b7a0af194Jonathan von Schroederinstance Comorphism THFP_P2THFP
880945fae9c3f61341f1cd94439c802b7a0af194Jonathan von Schroeder BasicSpecTHF THFFormula () ()
880945fae9c3f61341f1cd94439c802b7a0af194Jonathan von Schroeder SignTHF MorphismTHF SymbolTHF () ProofTree
880945fae9c3f61341f1cd94439c802b7a0af194Jonathan von Schroeder BasicSpecTHF THFFormula () ()
880945fae9c3f61341f1cd94439c802b7a0af194Jonathan von Schroeder SignTHF MorphismTHF SymbolTHF () ProofTree where
880945fae9c3f61341f1cd94439c802b7a0af194Jonathan von Schroeder sourceLogic THFP_P2THFP = THF
880945fae9c3f61341f1cd94439c802b7a0af194Jonathan von Schroeder sourceSublogic THFP_P2THFP = SL.tHFP_P
880945fae9c3f61341f1cd94439c802b7a0af194Jonathan von Schroeder targetLogic THFP_P2THFP = THF
fee6e355c164d9248e0512436812a476ad0c2e99Jonathan von Schroeder mapSublogic THFP_P2THFP sl = Just $ sl { SL.ext_Poly = False }
880945fae9c3f61341f1cd94439c802b7a0af194Jonathan von Schroeder map_theory THFP_P2THFP = trans_theory
880945fae9c3f61341f1cd94439c802b7a0af194Jonathan von Schroeder has_model_expansion THFP_P2THFP = True
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroedertrans_theory :: (SignTHF, [Named THFFormula])
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder -> Result (SignTHF, [Named THFFormula])
880945fae9c3f61341f1cd94439c802b7a0af194Jonathan von Schroedertrans_theory (sig, sentences1) = do
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder (cs, sentences) <- infer (consts sig) sentences1
880945fae9c3f61341f1cd94439c802b7a0af194Jonathan von Schroeder let sig1 = sig {consts = cs}
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder return (recreateSymbols sig1, sentences)