b38846b15c8891c6dec44dcc4f96ca40721bf663rbb{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}

b38846b15c8891c6dec44dcc4f96ca40721bf663rbb{- |

b38846b15c8891c6dec44dcc4f96ca40721bf663rbbModule : $Header$

b38846b15c8891c6dec44dcc4f96ca40721bf663rbbDescription : Comorphism from THFP_P to THFP

b38846b15c8891c6dec44dcc4f96ca40721bf663rbbCopyright : (c) J. von Schroeder, DFKI Bremen 2012

b38846b15c8891c6dec44dcc4f96ca40721bf663rbbLicense : GPLv2 or higher, see LICENSE.txt

b38846b15c8891c6dec44dcc4f96ca40721bf663rbb

b38846b15c8891c6dec44dcc4f96ca40721bf663rbbMaintainer : J. von Schroeder <jonathan.von_schroeder@dfki.de>

b38846b15c8891c6dec44dcc4f96ca40721bf663rbbStability : provisional

b38846b15c8891c6dec44dcc4f96ca40721bf663rbbPortability : non-portable (imports Logic.Logic)

b38846b15c8891c6dec44dcc4f96ca40721bf663rbb

b38846b15c8891c6dec44dcc4f96ca40721bf663rbbThe comorphism from THFP to THF0.

b38846b15c8891c6dec44dcc4f96ca40721bf663rbb-}

b38846b15c8891c6dec44dcc4f96ca40721bf663rbb

b38846b15c8891c6dec44dcc4f96ca40721bf663rbbmodule Comorphisms.THFP_P2THFP where

b38846b15c8891c6dec44dcc4f96ca40721bf663rbb

b38846b15c8891c6dec44dcc4f96ca40721bf663rbbimport Logic.Logic as Logic

b38846b15c8891c6dec44dcc4f96ca40721bf663rbbimport Logic.Comorphism

b38846b15c8891c6dec44dcc4f96ca40721bf663rbb

b38846b15c8891c6dec44dcc4f96ca40721bf663rbbimport Common.ProofTree

b38846b15c8891c6dec44dcc4f96ca40721bf663rbbimport Common.Result

b38846b15c8891c6dec44dcc4f96ca40721bf663rbbimport Common.AS_Annotation (Named)

b38846b15c8891c6dec44dcc4f96ca40721bf663rbb

b38846b15c8891c6dec44dcc4f96ca40721bf663rbbimport THF.Logic_THF

b38846b15c8891c6dec44dcc4f96ca40721bf663rbbimport THF.Cons

b38846b15c8891c6dec44dcc4f96ca40721bf663rbbimport THF.Sign

b38846b15c8891c6dec44dcc4f96ca40721bf663rbbimport qualified THF.Sublogic as SL

b38846b15c8891c6dec44dcc4f96ca40721bf663rbbimport THF.As

b38846b15c8891c6dec44dcc4f96ca40721bf663rbbimport THF.Utils

b38846b15c8891c6dec44dcc4f96ca40721bf663rbbimport THF.Poly

b38846b15c8891c6dec44dcc4f96ca40721bf663rbb

b38846b15c8891c6dec44dcc4f96ca40721bf663rbbdata THFP_P2THFP = THFP_P2THFP deriving Show

b38846b15c8891c6dec44dcc4f96ca40721bf663rbb

b38846b15c8891c6dec44dcc4f96ca40721bf663rbbinstance Language THFP_P2THFP

b38846b15c8891c6dec44dcc4f96ca40721bf663rbb

b38846b15c8891c6dec44dcc4f96ca40721bf663rbbinstance Comorphism THFP_P2THFP

b38846b15c8891c6dec44dcc4f96ca40721bf663rbb THF SL.THFSl

b38846b15c8891c6dec44dcc4f96ca40721bf663rbb BasicSpecTHF THFFormula () ()

b38846b15c8891c6dec44dcc4f96ca40721bf663rbb SignTHF MorphismTHF SymbolTHF () ProofTree

b38846b15c8891c6dec44dcc4f96ca40721bf663rbb THF SL.THFSl

b38846b15c8891c6dec44dcc4f96ca40721bf663rbb BasicSpecTHF THFFormula () ()

b38846b15c8891c6dec44dcc4f96ca40721bf663rbb SignTHF MorphismTHF SymbolTHF () ProofTree where

b38846b15c8891c6dec44dcc4f96ca40721bf663rbb sourceLogic THFP_P2THFP = THF

b38846b15c8891c6dec44dcc4f96ca40721bf663rbb sourceSublogic THFP_P2THFP = SL.tHFP_P

b38846b15c8891c6dec44dcc4f96ca40721bf663rbb targetLogic THFP_P2THFP = THF

b38846b15c8891c6dec44dcc4f96ca40721bf663rbb mapSublogic THFP_P2THFP sl = Just $ sl { SL.ext_Poly = False }

b38846b15c8891c6dec44dcc4f96ca40721bf663rbb map_theory THFP_P2THFP = trans_theory

b38846b15c8891c6dec44dcc4f96ca40721bf663rbb has_model_expansion THFP_P2THFP = True

b38846b15c8891c6dec44dcc4f96ca40721bf663rbb

b38846b15c8891c6dec44dcc4f96ca40721bf663rbbtrans_theory :: (SignTHF,[Named THFFormula])

b38846b15c8891c6dec44dcc4f96ca40721bf663rbb -> Result (SignTHF,[Named THFFormula])

b38846b15c8891c6dec44dcc4f96ca40721bf663rbbtrans_theory (sig, sentences1) = do

b38846b15c8891c6dec44dcc4f96ca40721bf663rbb (cs,sentences) <- infer (consts sig) sentences1

b38846b15c8891c6dec44dcc4f96ca40721bf663rbb let sig1 = sig {consts = cs}

b38846b15c8891c6dec44dcc4f96ca40721bf663rbb return (recreateSymbols sig1,sentences)

b38846b15c8891c6dec44dcc4f96ca40721bf663rbb