{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}
{- |
Module      :  $Header$
Description :  Comorphism from THFP_P to THFP
Copyright   :  (c) J. von Schroeder, DFKI Bremen 2012
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  J. von Schroeder <jonathan.von_schroeder@dfki.de>
Stability   :  provisional
Portability :  non-portable (imports Logic.Logic)

The comorphism from THFP to THF0.
-}

module Comorphisms.THFP_P2THFP where

import Logic.Logic as Logic
import Logic.Comorphism

import Common.ProofTree
import Common.Result
import Common.AS_Annotation (Named)

import THF.Logic_THF
import THF.Cons
import THF.Sign
import qualified THF.Sublogic as SL
import THF.As
import THF.Utils
import THF.Poly

data THFP_P2THFP = THFP_P2THFP deriving Show

instance Language THFP_P2THFP

instance Comorphism THFP_P2THFP
                THF SL.THFSl
                BasicSpecTHF THFFormula () ()
                SignTHF MorphismTHF SymbolTHF () ProofTree
                THF SL.THFSl
                BasicSpecTHF THFFormula () ()
                SignTHF MorphismTHF SymbolTHF () ProofTree where
    sourceLogic THFP_P2THFP = THF
    sourceSublogic THFP_P2THFP = SL.tHFP_P
    targetLogic THFP_P2THFP = THF
    mapSublogic THFP_P2THFP sl = Just $ sl { SL.ext_Poly = False }
    map_theory THFP_P2THFP = trans_theory
    has_model_expansion THFP_P2THFP = True

trans_theory :: (SignTHF, [Named THFFormula])
                -> Result (SignTHF, [Named THFFormula])
trans_theory (sig, sentences1) = do
 (cs, sentences) <- infer (consts sig) sentences1
 let sig1 = sig {consts = cs}
 return (recreateSymbols sig1, sentences)
