hets/THF/HasCASL2THF.hs

	HasCASL2THF.hs revision e21e5f0fa66bf80e14cfd3f571e09b3952e46ad9
765f3b8c82bca96eeb44463da2305201b1a493daChristian Maeder{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances #-}
765f3b8c82bca96eeb44463da2305201b1a493daChristian Maeder{- |
765f3b8c82bca96eeb44463da2305201b1a493daChristian MaederModule      :  $Header$
765f3b8c82bca96eeb44463da2305201b1a493daChristian MaederDescription :  translation from HasCASL to THF
765f3b8c82bca96eeb44463da2305201b1a493daChristian MaederCopyright   :  (c) A. Tsogias, DFKI Bremen 2011
765f3b8c82bca96eeb44463da2305201b1a493daChristian MaederLicense     :  GPLv2 or higher, see LICENSE.txt
765f3b8c82bca96eeb44463da2305201b1a493daChristian Maeder
765f3b8c82bca96eeb44463da2305201b1a493daChristian MaederMaintainer  :
765f3b8c82bca96eeb44463da2305201b1a493daChristian MaederStability   :
765f3b8c82bca96eeb44463da2305201b1a493daChristian MaederPortability :  non-portable (imports Logic.Logic)
765f3b8c82bca96eeb44463da2305201b1a493daChristian Maeder
765f3b8c82bca96eeb44463da2305201b1a493daChristian MaederThe embedding comorphism from HasCASL to THF.
765f3b8c82bca96eeb44463da2305201b1a493daChristian Maeder-}
765f3b8c82bca96eeb44463da2305201b1a493daChristian Maeder
765f3b8c82bca96eeb44463da2305201b1a493daChristian Maeder-- TODO move this file from Hets/THF to Hets/Comorphisms
765f3b8c82bca96eeb44463da2305201b1a493daChristian Maeder
765f3b8c82bca96eeb44463da2305201b1a493daChristian Maedermodule Comorphisms.HasCASL2THF where
765f3b8c82bca96eeb44463da2305201b1a493daChristian Maeder
765f3b8c82bca96eeb44463da2305201b1a493daChristian Maederimport Logic.Logic as Logic
765f3b8c82bca96eeb44463da2305201b1a493daChristian Maederimport Logic.Comorphism
765f3b8c82bca96eeb44463da2305201b1a493daChristian Maeder
765f3b8c82bca96eeb44463da2305201b1a493daChristian Maederimport HasCASL.Logic_HasCASL
765f3b8c82bca96eeb44463da2305201b1a493daChristian Maederimport HasCASL.Sublogic
765f3b8c82bca96eeb44463da2305201b1a493daChristian Maederimport HasCASL.Le
765f3b8c82bca96eeb44463da2305201b1a493daChristian Maederimport HasCASL.As
765f3b8c82bca96eeb44463da2305201b1a493daChristian Maederimport HasCASL.AsUtils
765f3b8c82bca96eeb44463da2305201b1a493daChristian Maederimport HasCASL.Builtin
765f3b8c82bca96eeb44463da2305201b1a493daChristian Maeder
765f3b8c82bca96eeb44463da2305201b1a493daChristian Maederimport THF.Logic_THF
765f3b8c82bca96eeb44463da2305201b1a493daChristian Maederimport THF.Cons as THFCons
765f3b8c82bca96eeb44463da2305201b1a493daChristian Maeder
765f3b8c82bca96eeb44463da2305201b1a493daChristian Maeder-- | The identity of the comorphism
765f3b8c82bca96eeb44463da2305201b1a493daChristian Maederdata HasCASL2THF = HasCASL2THF deriving Show
765f3b8c82bca96eeb44463da2305201b1a493daChristian Maeder
765f3b8c82bca96eeb44463da2305201b1a493daChristian Maederinstance Language HasCASL2THF
765f3b8c82bca96eeb44463da2305201b1a493daChristian Maeder
765f3b8c82bca96eeb44463da2305201b1a493daChristian Maederinstance Comorphism HasCASL2THF
765f3b8c82bca96eeb44463da2305201b1a493daChristian Maeder                HasCASL Sublogic
765f3b8c82bca96eeb44463da2305201b1a493daChristian Maeder                BasicSpec HCAS.Sentence SymbItems SymbMapItems
765f3b8c82bca96eeb44463da2305201b1a493daChristian Maeder                Env Morphism Symbol RawSymbol ()
765f3b8c82bca96eeb44463da2305201b1a493daChristian Maeder                THF ()
765f3b8c82bca96eeb44463da2305201b1a493daChristian Maeder                () THFCons.Sentence () ()
765f3b8c82bca96eeb44463da2305201b1a493daChristian Maeder                () THFMorphism THFCons.Symbol () () where
765f3b8c82bca96eeb44463da2305201b1a493daChristian Maeder    sourceLogic HasCASL2THF = HasCASL
765f3b8c82bca96eeb44463da2305201b1a493daChristian Maeder    sourceSublogic HasCASL2THF = top
4d7def117f71589712fa1f9b13b1997609e4a0b0Christian Maeder    targetLogic HasCASL2THF = THF
4d7def117f71589712fa1f9b13b1997609e4a0b0Christian Maeder