{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}
{- |
Module      :  ./Comorphisms/THFP_P2THFP.hs
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 Int -> THFP_P2THFP -> ShowS
[THFP_P2THFP] -> ShowS
THFP_P2THFP -> String
(Int -> THFP_P2THFP -> ShowS)
-> (THFP_P2THFP -> String)
-> ([THFP_P2THFP] -> ShowS)
-> Show THFP_P2THFP
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [THFP_P2THFP] -> ShowS
$cshowList :: [THFP_P2THFP] -> ShowS
show :: THFP_P2THFP -> String
$cshow :: THFP_P2THFP -> String
showsPrec :: Int -> THFP_P2THFP -> ShowS
$cshowsPrec :: Int -> THFP_P2THFP -> ShowS
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
sourceLogic THFP_P2THFP = THF
THF
    sourceSublogic :: THFP_P2THFP -> THFSl
sourceSublogic THFP_P2THFP = THFSl
SL.tHFP_P
    targetLogic :: THFP_P2THFP -> THF
targetLogic THFP_P2THFP = THF
THF
    mapSublogic :: THFP_P2THFP -> THFSl -> Maybe THFSl
mapSublogic THFP_P2THFP sl :: THFSl
sl = THFSl -> Maybe THFSl
forall a. a -> Maybe a
Just (THFSl -> Maybe THFSl) -> THFSl -> Maybe THFSl
forall a b. (a -> b) -> a -> b
$ THFSl
sl { ext_Poly :: Bool
SL.ext_Poly = Bool
False }
    map_theory :: THFP_P2THFP
-> (SignTHF, [Named THFFormula])
-> Result (SignTHF, [Named THFFormula])
map_theory THFP_P2THFP = (SignTHF, [Named THFFormula])
-> Result (SignTHF, [Named THFFormula])
trans_theory
    has_model_expansion :: THFP_P2THFP -> Bool
has_model_expansion THFP_P2THFP = Bool
True

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