{- |
Module      :  ./THF/Print.hs
Description :  Seveal Pretty instances.
Copyright   :  (c) A. Tsogias, DFKI Bremen 2011
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Alexis.Tsogias@dfki.de
Stability   :  provisional
Portability :  portable

Pretty instances some data structures of As, Sign and Cons
-}

module THF.Print where

import Common.DocUtils
import Common.Doc
import Common.AS_Annotation

import THF.Cons
import THF.Sign
import THF.PrintTHF
import THF.As (THFFormula, FormulaRole (..))

import qualified Data.Map as Map
import Data.Maybe (fromMaybe)

{- -----------------------------------------------------------------------------
Some pretty instances for datastructures defined in Cons and Sign and
other print methods
----------------------------------------------------------------------------- -}

instance Pretty BasicSpecTHF where
    pretty :: BasicSpecTHF -> Doc
pretty (BasicSpecTHF a :: [TPTP_THF]
a) = [TPTP_THF] -> Doc
printTPTPTHF [TPTP_THF]
a

instance Pretty SymbolTHF where
    pretty :: SymbolTHF -> Doc
pretty s :: SymbolTHF
s = case SymbolTHF -> SymbolType
symType SymbolTHF
s of
        ST_Const t :: Type
t -> Constant -> Doc
forall a. Pretty a => a -> Doc
pretty (SymbolTHF -> Constant
symId SymbolTHF
s) Doc -> Doc -> Doc
<+> String -> Doc
text ":" Doc -> Doc -> Doc
<+> Type -> Doc
forall a. Pretty a => a -> Doc
pretty Type
t
        ST_Type k :: Kind
k -> Constant -> Doc
forall a. Pretty a => a -> Doc
pretty (SymbolTHF -> Constant
symId SymbolTHF
s) Doc -> Doc -> Doc
<+> String -> Doc
text ":" Doc -> Doc -> Doc
<+> Kind -> Doc
forall a. Pretty a => a -> Doc
pretty Kind
k

instance Pretty SignTHF where
    pretty :: SignTHF -> Doc
pretty s :: SignTHF
s =
        let ts :: Doc
ts = (TypeInfo -> Doc -> Doc) -> Doc -> Map Constant TypeInfo -> Doc
forall a b k. (a -> b -> b) -> b -> Map k a -> b
Map.foldr (\ ti :: TypeInfo
ti d :: Doc
d -> Doc
d Doc -> Doc -> Doc
$+$ TypeInfo -> Doc
forall a. Pretty a => a -> Doc
pretty TypeInfo
ti) Doc
empty (SignTHF -> Map Constant TypeInfo
types SignTHF
s)
            cs :: Doc
cs = (ConstInfo -> Doc -> Doc) -> Doc -> Map Constant ConstInfo -> Doc
forall a b k. (a -> b -> b) -> b -> Map k a -> b
Map.foldr (\ ci :: ConstInfo
ci d :: Doc
d -> Doc
d Doc -> Doc -> Doc
$+$ ConstInfo -> Doc
forall a. Pretty a => a -> Doc
pretty ConstInfo
ci) Doc
empty (SignTHF -> Map Constant ConstInfo
consts SignTHF
s)
        in String -> Doc
text "%Types:" Doc -> Doc -> Doc
$+$ Doc
ts Doc -> Doc -> Doc
$++$ String -> Doc
text "%Constants: " Doc -> Doc -> Doc
$+$ Doc
cs

instance Pretty Kind where
    pretty :: Kind -> Doc
pretty k :: Kind
k = case Kind
k of
        Kind -> String -> Doc
text "$tType"

instance Pretty Type where
    pretty :: Type -> Doc
pretty t :: Type
t = case Type
t of
        TType -> String -> Doc
text "$tType"
        OType -> String -> Doc
text "$o"
        IType -> String -> Doc
text "$i"
        MapType t1 :: Type
t1 t2 :: Type
t2 -> Type -> Doc
forall a. Pretty a => a -> Doc
pretty Type
t1 Doc -> Doc -> Doc
<+> String -> Doc
text ">" Doc -> Doc -> Doc
<+> Type -> Doc
forall a. Pretty a => a -> Doc
pretty Type
t2
        CType c :: Constant
c -> Constant -> Doc
prettyConstant Constant
c
        SType st :: Token
st -> Token -> Doc
prettyAtomicSystemWord Token
st
        VType v :: Token
v -> Token -> Doc
prettyUpperWord Token
v
        ParType t1 :: Type
t1 -> Doc -> Doc
parens (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Type -> Doc
forall a. Pretty a => a -> Doc
pretty Type
t1
        ProdType ts :: [Type]
ts -> Doc -> Doc
parens (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc -> Doc
sepBy ((Type -> Doc) -> [Type] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Type -> Doc
forall a. Pretty a => a -> Doc
pretty [Type]
ts) Doc
starSign

instance Pretty TypeInfo where
    pretty :: TypeInfo -> Doc
pretty ti :: TypeInfo
ti = String -> Doc
text "thf" Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc -> Doc
parens (Name -> Doc
forall a. Pretty a => a -> Doc
pretty (TypeInfo -> Name
typeName TypeInfo
ti) Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
comma
            Doc -> Doc -> Doc
<+> String -> Doc
text "type" Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
comma Doc -> Doc -> Doc
<+>
                (Constant -> Doc
forall a. Pretty a => a -> Doc
pretty (TypeInfo -> Constant
typeId TypeInfo
ti) Doc -> Doc -> Doc
<+> Doc
colon Doc -> Doc -> Doc
<+> Kind -> Doc
forall a. Pretty a => a -> Doc
pretty (TypeInfo -> Kind
typeKind TypeInfo
ti))
            Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Annotations -> Doc
forall a. Pretty a => a -> Doc
pretty (TypeInfo -> Annotations
typeAnno TypeInfo
ti))
            Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> String -> Doc
text "."

instance Pretty ConstInfo where
    pretty :: ConstInfo -> Doc
pretty ci :: ConstInfo
ci = String -> Doc
text "thf" Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc -> Doc
parens (Name -> Doc
forall a. Pretty a => a -> Doc
pretty (ConstInfo -> Name
constName ConstInfo
ci) Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
comma
            Doc -> Doc -> Doc
<+> String -> Doc
text "type" Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
comma Doc -> Doc -> Doc
<+>
                (Constant -> Doc
forall a. Pretty a => a -> Doc
pretty (ConstInfo -> Constant
constId ConstInfo
ci) Doc -> Doc -> Doc
<+> Doc
colon Doc -> Doc -> Doc
<+> Type -> Doc
forall a. Pretty a => a -> Doc
pretty (ConstInfo -> Type
constType ConstInfo
ci))
                Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Annotations -> Doc
forall a. Pretty a => a -> Doc
pretty (ConstInfo -> Annotations
constAnno ConstInfo
ci))
            Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> String -> Doc
text "."

-- print the signature, with axioms and the proof goal
printProblemTHF :: SignTHF -> [Named THFFormula] -> Named THFFormula -> Doc
printProblemTHF :: SignTHF -> [Named THFFormula] -> Named THFFormula -> Doc
printProblemTHF sig :: SignTHF
sig ax :: [Named THFFormula]
ax gl :: Named THFFormula
gl = SignTHF -> Doc
forall a. Pretty a => a -> Doc
pretty SignTHF
sig Doc -> Doc -> Doc
$++$ String -> Doc
text "%Axioms:" Doc -> Doc -> Doc
$+$
    (Doc -> Named THFFormula -> Doc)
-> Doc -> [Named THFFormula] -> Doc
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\ d :: Doc
d e :: Named THFFormula
e -> Doc
d Doc -> Doc -> Doc
$+$ Maybe FormulaRole -> Named THFFormula -> Doc
printNamedSentenceTHF (FormulaRole -> Maybe FormulaRole
forall a. a -> Maybe a
Just FormulaRole
Axiom) Named THFFormula
e) Doc
empty [Named THFFormula]
ax Doc -> Doc -> Doc
$++$
    String -> Doc
text "%Goal:" Doc -> Doc -> Doc
$+$ Maybe FormulaRole -> Named THFFormula -> Doc
printNamedSentenceTHF (FormulaRole -> Maybe FormulaRole
forall a. a -> Maybe a
Just FormulaRole
Conjecture) Named THFFormula
gl

-- print a Named Sentence
printNamedSentenceTHF :: Maybe FormulaRole -> Named THFFormula -> Doc
printNamedSentenceTHF :: Maybe FormulaRole -> Named THFFormula -> Doc
printNamedSentenceTHF r' :: Maybe FormulaRole
r' f :: Named THFFormula
f =
 let r :: FormulaRole
r = FormulaRole -> Maybe FormulaRole -> FormulaRole
forall a. a -> Maybe a -> a
fromMaybe (if Named THFFormula -> Bool
forall s a. SenAttr s a -> Bool
isAxiom Named THFFormula
f then FormulaRole
Axiom
                    else FormulaRole
Conjecture) Maybe FormulaRole
r'
 in String -> Doc
text "thf" Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc -> Doc
parens (String -> Doc
text (Named THFFormula -> String
forall s a. SenAttr s a -> a
senAttr Named THFFormula
f) Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
comma
     Doc -> Doc -> Doc
<+> FormulaRole -> Doc
forall a. Pretty a => a -> Doc
pretty FormulaRole
r Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
comma Doc -> Doc -> Doc
<+> THFFormula -> Doc
forall a. Pretty a => a -> Doc
pretty (Named THFFormula -> THFFormula
forall s a. SenAttr s a -> s
sentence Named THFFormula
f))
     Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> String -> Doc
text "."