{- |
Module      :  ./THF/HasCASL2THF0Buildins.hs
Description :  create legal THF mixfix identifier
Copyright   :  (c) A. Tsogias, DFKI Bremen 2011
License     :  GPLv2 or higher, see LICENSE.txt

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

translations for the buildins of HasCasl
-}

module THF.HasCASL2THF0Buildins where

import Common.AS_Annotation
import Common.DocUtils
import Common.Result
import Common.Id

import HasCASL.Builtin

import THF.As
import THF.Cons
import THF.Sign
import THF.ParseTHF
import THF.Translate
import THF.PrintTHF ()

import Text.ParserCombinators.Parsec

import Data.Maybe
import qualified Data.Set as Set
import qualified Data.Map as Map

{- -----------------------------------------------------------------------------
Assumps
----------------------------------------------------------------------------- -}

preDefHCAssumps :: Set.Set Id -> ConstMap
preDefHCAssumps :: Set Id -> ConstMap
preDefHCAssumps ids :: Set Id
ids =
    let asl :: [(Id, Constant -> ConstInfo)]
asl = [ (Id
botId, Constant -> ConstInfo
botci)
              , (Id
defId, Constant -> ConstInfo
defci)
              , (Id
notId, Constant -> ConstInfo
o2ci)
              , (Id
negId, Constant -> ConstInfo
o2ci)
-- , (whenElse,    "hcc" ++ show whenElse)
              , (Id
trueId, Constant -> ConstInfo
o1ci)
              , (Id
falseId, Constant -> ConstInfo
o1ci)
              , (Id
eqId, Constant -> ConstInfo
a2o1ci)
              , (Id
exEq, Constant -> ConstInfo
a2o1ci)
              , (Id
resId, Constant -> ConstInfo
resci)
              , (Id
andId, Constant -> ConstInfo
o3ci)
              , (Id
orId, Constant -> ConstInfo
o3ci)
              , (Id
eqvId, Constant -> ConstInfo
o3ci)
              , (Id
implId, Constant -> ConstInfo
o3ci)
              , (Id
infixIf, Constant -> ConstInfo
o3ci) ]
    in [(Constant, ConstInfo)] -> ConstMap
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(Constant, ConstInfo)] -> ConstMap)
-> [(Constant, ConstInfo)] -> ConstMap
forall a b. (a -> b) -> a -> b
$ ((Id, Constant -> ConstInfo) -> (Constant, ConstInfo))
-> [(Id, Constant -> ConstInfo)] -> [(Constant, ConstInfo)]
forall a b. (a -> b) -> [a] -> [b]
map
            (\ (i :: Id
i, tf :: Constant -> ConstInfo
tf) -> let c :: Constant
c = (Maybe Constant -> Constant
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe Constant -> Constant)
-> (Id -> Maybe Constant) -> Id -> Constant
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Result Constant -> Maybe Constant
forall a. Result a -> Maybe a
maybeResult (Result Constant -> Maybe Constant)
-> (Id -> Result Constant) -> Id -> Maybe Constant
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Id -> Result Constant
transAssumpId) Id
i
                           in (Constant
c , Constant -> ConstInfo
tf Constant
c))
            (((Id, Constant -> ConstInfo) -> Bool)
-> [(Id, Constant -> ConstInfo)] -> [(Id, Constant -> ConstInfo)]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ (i :: Id
i, _) -> Id -> Set Id -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member Id
i Set Id
ids) [(Id, Constant -> ConstInfo)]
asl)

o1ci :: Constant -> ConstInfo
o1ci :: Constant -> ConstInfo
o1ci c :: Constant
c = ConstInfo :: Constant -> Name -> Type -> Annotations -> ConstInfo
ConstInfo
    { constId :: Constant
constId = Constant
c
    , constName :: Name
constName = Constant -> Name
mkConstsName Constant
c
    , constType :: Type
constType = Type
OType
    , constAnno :: Annotations
constAnno = Annotations
Null }

o2ci :: Constant -> ConstInfo
o2ci :: Constant -> ConstInfo
o2ci c :: Constant
c = ConstInfo :: Constant -> Name -> Type -> Annotations -> ConstInfo
ConstInfo
    { constId :: Constant
constId = Constant
c
    , constName :: Name
constName = Constant -> Name
mkConstsName Constant
c
    , constType :: Type
constType = Type -> Type -> Type
MapType Type
OType Type
OType
    , constAnno :: Annotations
constAnno = Annotations
Null }

o3ci :: Constant -> ConstInfo
o3ci :: Constant -> ConstInfo
o3ci c :: Constant
c = ConstInfo :: Constant -> Name -> Type -> Annotations -> ConstInfo
ConstInfo
    { constId :: Constant
constId = Constant
c
    , constName :: Name
constName = Constant -> Name
mkConstsName Constant
c
    , constType :: Type
constType = Type -> Type -> Type
MapType Type
OType (Type -> Type -> Type
MapType Type
OType Type
OType)
    , constAnno :: Annotations
constAnno = Annotations
Null }

a2o1ci :: Constant -> ConstInfo
a2o1ci :: Constant -> ConstInfo
a2o1ci c :: Constant
c = ConstInfo :: Constant -> Name -> Type -> Annotations -> ConstInfo
ConstInfo
    { constId :: Constant
constId = Constant
c
    , constName :: Name
constName = Constant -> Name
mkConstsName Constant
c
    , constType :: Type
constType = Type -> Type -> Type
MapType (Token -> Type
VType (Token -> Type) -> Token -> Type
forall a b. (a -> b) -> a -> b
$ String -> Token
mkSimpleId "A")
                          (Type -> Type -> Type
MapType (Token -> Type
VType (Token -> Type) -> Token -> Type
forall a b. (a -> b) -> a -> b
$ String -> Token
mkSimpleId "A") Type
OType)
    , constAnno :: Annotations
constAnno = Annotations
Null }

resci :: Constant -> ConstInfo
resci :: Constant -> ConstInfo
resci c :: Constant
c = ConstInfo :: Constant -> Name -> Type -> Annotations -> ConstInfo
ConstInfo
    { constId :: Constant
constId = Constant
c
    , constName :: Name
constName = Constant -> Name
mkConstsName Constant
c
    , constType :: Type
constType = Type -> Type -> Type
MapType (Token -> Type
VType (Token -> Type) -> Token -> Type
forall a b. (a -> b) -> a -> b
$ String -> Token
mkSimpleId "A")
                          (Type -> Type -> Type
MapType (Token -> Type
VType (Token -> Type) -> Token -> Type
forall a b. (a -> b) -> a -> b
$ String -> Token
mkSimpleId "B")
                                    (Token -> Type
VType (Token -> Type) -> Token -> Type
forall a b. (a -> b) -> a -> b
$ String -> Token
mkSimpleId "A"))
    , constAnno :: Annotations
constAnno = Annotations
Null }

botci :: Constant -> ConstInfo
botci :: Constant -> ConstInfo
botci c :: Constant
c = ConstInfo :: Constant -> Name -> Type -> Annotations -> ConstInfo
ConstInfo
    { constId :: Constant
constId = Constant
c
    , constName :: Name
constName = Constant -> Name
mkConstsName Constant
c
    , constType :: Type
constType = Type
OType
    , constAnno :: Annotations
constAnno = Annotations
Null }

defci :: Constant -> ConstInfo
defci :: Constant -> ConstInfo
defci c :: Constant
c = ConstInfo :: Constant -> Name -> Type -> Annotations -> ConstInfo
ConstInfo
    { constId :: Constant
constId = Constant
c
    , constName :: Name
constName = Constant -> Name
mkConstsName Constant
c
    , constType :: Type
constType = Type -> Type -> Type
MapType (Token -> Type
VType (Token -> Type) -> Token -> Type
forall a b. (a -> b) -> a -> b
$ String -> Token
mkSimpleId "A") Type
OType
    , constAnno :: Annotations
constAnno = Annotations
Null }

{- -----------------------------------------------------------------------------
Axioms
----------------------------------------------------------------------------- -}

preDefAxioms :: Set.Set Id -> [Named THFFormula]
preDefAxioms :: Set Id -> [Named THFFormula]
preDefAxioms ids :: Set Id
ids =
    let axl :: [(Id, Constant -> String)]
axl = [ (Id
notId, Constant -> String
notFS)
              , (Id
negId, Constant -> String
notFS)
              , (Id
trueId, Constant -> String
trueFS)
              , (Id
falseId, Constant -> String
falseFS)
              , (Id
andId, Constant -> String
andFS)
              , (Id
orId, Constant -> String
orFS)
              , (Id
eqvId, Constant -> String
eqvFS)
              , (Id
implId, Constant -> String
implFS)
              , (Id
infixIf, Constant -> String
ifFS)
              , (Id
resId, Constant -> String
resFS)
              , (Id
botId, Constant -> String
botFS)
              , (Id
defId, Constant -> String
defFS)
{- , (whenElse,    "hcc" ++ show whenElse) -} ]
    in ((Id, Constant -> String) -> Named THFFormula)
-> [(Id, Constant -> String)] -> [Named THFFormula]
forall a b. (a -> b) -> [a] -> [b]
map (\ (i :: Id
i, fs :: Constant -> String
fs) -> Constant -> (Constant -> String) -> Named THFFormula
mkNSD
                (Maybe Constant -> Constant
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe Constant -> Constant) -> Maybe Constant -> Constant
forall a b. (a -> b) -> a -> b
$ Result Constant -> Maybe Constant
forall a. Result a -> Maybe a
maybeResult (Result Constant -> Maybe Constant)
-> Result Constant -> Maybe Constant
forall a b. (a -> b) -> a -> b
$ Id -> Result Constant
transAssumpId Id
i) Constant -> String
fs)
           (((Id, Constant -> String) -> Bool)
-> [(Id, Constant -> String)] -> [(Id, Constant -> String)]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ (i :: Id
i, _) -> Id -> Set Id -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member Id
i Set Id
ids) [(Id, Constant -> String)]
axl)

mkNSD :: Constant -> (Constant -> String) -> Named THFFormula
mkNSD :: Constant -> (Constant -> String) -> Named THFFormula
mkNSD c :: Constant
c f :: Constant -> String
f = (String -> THFFormula -> Named THFFormula
forall a s. a -> s -> SenAttr s a
makeNamed (Doc -> String
forall a. Show a => a -> String
show (Doc -> String) -> (Constant -> Doc) -> Constant -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> Doc
forall a. Pretty a => a -> Doc
pretty (Name -> Doc) -> (Constant -> Name) -> Constant -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Constant -> Name
mkDefName (Constant -> String) -> Constant -> String
forall a b. (a -> b) -> a -> b
$ Constant
c) (THFFormula -> Named THFFormula) -> THFFormula -> Named THFFormula
forall a b. (a -> b) -> a -> b
$ Constant -> (Constant -> String) -> THFFormula
genTHFFormula Constant
c Constant -> String
f)
        { isDef :: Bool
isDef = Bool
True }

genTHFFormula :: Constant -> (Constant -> String) -> THFFormula
genTHFFormula :: Constant -> (Constant -> String) -> THFFormula
genTHFFormula c :: Constant
c f :: Constant -> String
f = case Parsec String () [TPTP_THF]
-> String -> String -> Either ParseError [TPTP_THF]
forall s t a.
Stream s Identity t =>
Parsec s () a -> String -> s -> Either ParseError a
parse Parsec String () [TPTP_THF]
forall st. CharParser st [TPTP_THF]
parseTHF "" (Constant -> String
f Constant
c) of
        Left msg :: ParseError
msg -> String -> THFFormula
forall a. HasCallStack => String -> a
error ([String] -> String
unlines
                   ["Fatal error while generating the predefined Sentence"
                    String -> String -> String
forall a. [a] -> [a] -> [a]
++ " for: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Doc -> String
forall a. Show a => a -> String
show (Constant -> Doc
forall a. Pretty a => a -> Doc
pretty Constant
c),
                    "Parsing " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
forall a. Show a => a -> String
show (Constant -> String
f Constant
c) String -> String -> String
forall a. [a] -> [a] -> [a]
++ " failed with message",
                    ParseError -> String
forall a. Show a => a -> String
show ParseError
msg])
        Right x :: [TPTP_THF]
x -> TPTP_THF -> THFFormula
thfFormulaAF (TPTP_THF -> THFFormula) -> TPTP_THF -> THFFormula
forall a b. (a -> b) -> a -> b
$ [TPTP_THF] -> TPTP_THF
forall a. [a] -> a
head [TPTP_THF]
x

{- -----------------------------------------------------------------------------
formulas as Strings
----------------------------------------------------------------------------- -}

notFS :: Constant -> String
notFS :: Constant -> String
notFS c :: Constant
c =
    let ns :: String
ns = (Doc -> String
forall a. Show a => a -> String
show (Doc -> String) -> (Constant -> Doc) -> Constant -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> Doc
forall a. Pretty a => a -> Doc
pretty (Name -> Doc) -> (Constant -> Name) -> Constant -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Constant -> Name
mkDefName) Constant
c
        cs :: String
cs = (Doc -> String
forall a. Show a => a -> String
show (Doc -> String) -> (Constant -> Doc) -> Constant -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Constant -> Doc
forall a. Pretty a => a -> Doc
pretty) Constant
c
    in String -> String
encTHF (String
ns String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
defnS String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
cs String -> String -> String
forall a. [a] -> [a] -> [a]
++ " = (^ [A : $o] : ~(A))")

falseFS :: Constant -> String
falseFS :: Constant -> String
falseFS c :: Constant
c =
    let ns :: String
ns = (Doc -> String
forall a. Show a => a -> String
show (Doc -> String) -> (Constant -> Doc) -> Constant -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> Doc
forall a. Pretty a => a -> Doc
pretty (Name -> Doc) -> (Constant -> Name) -> Constant -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Constant -> Name
mkDefName) Constant
c
        cs :: String
cs = (Doc -> String
forall a. Show a => a -> String
show (Doc -> String) -> (Constant -> Doc) -> Constant -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Constant -> Doc
forall a. Pretty a => a -> Doc
pretty) Constant
c
    in String -> String
encTHF (String
ns String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
defnS String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
cs String -> String -> String
forall a. [a] -> [a] -> [a]
++ " = $false")

trueFS :: Constant -> String
trueFS :: Constant -> String
trueFS c :: Constant
c =
    let ns :: String
ns = (Doc -> String
forall a. Show a => a -> String
show (Doc -> String) -> (Constant -> Doc) -> Constant -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> Doc
forall a. Pretty a => a -> Doc
pretty (Name -> Doc) -> (Constant -> Name) -> Constant -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Constant -> Name
mkDefName) Constant
c
        cs :: String
cs = (Doc -> String
forall a. Show a => a -> String
show (Doc -> String) -> (Constant -> Doc) -> Constant -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Constant -> Doc
forall a. Pretty a => a -> Doc
pretty) Constant
c
    in String -> String
encTHF (String
ns String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
defnS String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
cs String -> String -> String
forall a. [a] -> [a] -> [a]
++ " = $true")

andFS :: Constant -> String
andFS :: Constant -> String
andFS c :: Constant
c =
    let ns :: String
ns = (Doc -> String
forall a. Show a => a -> String
show (Doc -> String) -> (Constant -> Doc) -> Constant -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> Doc
forall a. Pretty a => a -> Doc
pretty (Name -> Doc) -> (Constant -> Name) -> Constant -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Constant -> Name
mkDefName) Constant
c
        cs :: String
cs = (Doc -> String
forall a. Show a => a -> String
show (Doc -> String) -> (Constant -> Doc) -> Constant -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Constant -> Doc
forall a. Pretty a => a -> Doc
pretty) Constant
c
    in String -> String
encTHF (String
ns String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
defnS String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
cs String -> String -> String
forall a. [a] -> [a] -> [a]
++ " = (^ [X : $o, Y : $o] : (X & Y))")

orFS :: Constant -> String
orFS :: Constant -> String
orFS c :: Constant
c =
    let ns :: String
ns = (Doc -> String
forall a. Show a => a -> String
show (Doc -> String) -> (Constant -> Doc) -> Constant -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> Doc
forall a. Pretty a => a -> Doc
pretty (Name -> Doc) -> (Constant -> Name) -> Constant -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Constant -> Name
mkDefName) Constant
c
        cs :: String
cs = (Doc -> String
forall a. Show a => a -> String
show (Doc -> String) -> (Constant -> Doc) -> Constant -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Constant -> Doc
forall a. Pretty a => a -> Doc
pretty) Constant
c
    in String -> String
encTHF (String
ns String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
defnS String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
cs String -> String -> String
forall a. [a] -> [a] -> [a]
++ " = (^ [X : $o, Y : $o] : (X | Y))")

eqvFS :: Constant -> String
eqvFS :: Constant -> String
eqvFS c :: Constant
c =
    let ns :: String
ns = (Doc -> String
forall a. Show a => a -> String
show (Doc -> String) -> (Constant -> Doc) -> Constant -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> Doc
forall a. Pretty a => a -> Doc
pretty (Name -> Doc) -> (Constant -> Name) -> Constant -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Constant -> Name
mkDefName) Constant
c
        cs :: String
cs = (Doc -> String
forall a. Show a => a -> String
show (Doc -> String) -> (Constant -> Doc) -> Constant -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Constant -> Doc
forall a. Pretty a => a -> Doc
pretty) Constant
c
    in String -> String
encTHF (String
ns String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
defnS String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
cs String -> String -> String
forall a. [a] -> [a] -> [a]
++ " = (^ [X : $o, Y : $o] : (X <=> Y))")

implFS :: Constant -> String
implFS :: Constant -> String
implFS c :: Constant
c =
    let ns :: String
ns = (Doc -> String
forall a. Show a => a -> String
show (Doc -> String) -> (Constant -> Doc) -> Constant -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> Doc
forall a. Pretty a => a -> Doc
pretty (Name -> Doc) -> (Constant -> Name) -> Constant -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Constant -> Name
mkDefName) Constant
c
        cs :: String
cs = (Doc -> String
forall a. Show a => a -> String
show (Doc -> String) -> (Constant -> Doc) -> Constant -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Constant -> Doc
forall a. Pretty a => a -> Doc
pretty) Constant
c
    in String -> String
encTHF (String
ns String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
defnS String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
cs String -> String -> String
forall a. [a] -> [a] -> [a]
++ " = (^ [X : $o, Y : $o] : (X => Y))")

ifFS :: Constant -> String
ifFS :: Constant -> String
ifFS c :: Constant
c =
    let ns :: String
ns = (Doc -> String
forall a. Show a => a -> String
show (Doc -> String) -> (Constant -> Doc) -> Constant -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> Doc
forall a. Pretty a => a -> Doc
pretty (Name -> Doc) -> (Constant -> Name) -> Constant -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Constant -> Name
mkDefName) Constant
c
        cs :: String
cs = (Doc -> String
forall a. Show a => a -> String
show (Doc -> String) -> (Constant -> Doc) -> Constant -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Constant -> Doc
forall a. Pretty a => a -> Doc
pretty) Constant
c
    in String -> String
encTHF (String
ns String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
defnS String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
cs String -> String -> String
forall a. [a] -> [a] -> [a]
++ " = (^ [X : $o, Y : $o] : (Y => X))")

resFS :: Constant -> String
resFS :: Constant -> String
resFS c :: Constant
c =
    let ns :: String
ns = (Doc -> String
forall a. Show a => a -> String
show (Doc -> String) -> (Constant -> Doc) -> Constant -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> Doc
forall a. Pretty a => a -> Doc
pretty (Name -> Doc) -> (Constant -> Name) -> Constant -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Constant -> Name
mkDefName) Constant
c
        cs :: String
cs = (Doc -> String
forall a. Show a => a -> String
show (Doc -> String) -> (Constant -> Doc) -> Constant -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Constant -> Doc
forall a. Pretty a => a -> Doc
pretty) Constant
c
    in String -> String
encTHF (String
ns String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
defnS String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
cs String -> String -> String
forall a. [a] -> [a] -> [a]
++ " = (^ [X : A, Y : B] : X)")

botFS :: Constant -> String
botFS :: Constant -> String
botFS c :: Constant
c =
    let ns :: String
ns = (Doc -> String
forall a. Show a => a -> String
show (Doc -> String) -> (Constant -> Doc) -> Constant -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> Doc
forall a. Pretty a => a -> Doc
pretty (Name -> Doc) -> (Constant -> Name) -> Constant -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Constant -> Name
mkDefName) Constant
c
        cs :: String
cs = (Doc -> String
forall a. Show a => a -> String
show (Doc -> String) -> (Constant -> Doc) -> Constant -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Constant -> Doc
forall a. Pretty a => a -> Doc
pretty) Constant
c
    in String -> String
encTHF (String
ns String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
defnS String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
cs String -> String -> String
forall a. [a] -> [a] -> [a]
++ " = $false")

defFS :: Constant -> String
defFS :: Constant -> String
defFS c :: Constant
c =
    let ns :: String
ns = (Doc -> String
forall a. Show a => a -> String
show (Doc -> String) -> (Constant -> Doc) -> Constant -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> Doc
forall a. Pretty a => a -> Doc
pretty (Name -> Doc) -> (Constant -> Name) -> Constant -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Constant -> Name
mkDefName) Constant
c
        cs :: String
cs = (Doc -> String
forall a. Show a => a -> String
show (Doc -> String) -> (Constant -> Doc) -> Constant -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Constant -> Doc
forall a. Pretty a => a -> Doc
pretty) Constant
c
    in String -> String
encTHF (String
ns String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
defnS String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
cs String -> String -> String
forall a. [a] -> [a] -> [a]
++ " = (^ [X : A] : $true)")

defnS :: String
defnS :: String
defnS = ", definition, "

encTHF :: String -> String
encTHF :: String -> String
encTHF s :: String
s = "thf(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")."