module TPTP.Pretty (printBasicTheory, printNamedSentence) where
import TPTP.AS
import TPTP.Sign
import Common.AS_Annotation hiding (Name)
import Common.Id (Token)
import Common.Doc hiding (defn)
import Common.DocUtils
import Data.Char (toLower)
import qualified Data.Map as Map
import qualified Data.Set as Set
instance Pretty Symbol where
pretty :: Symbol -> Doc
pretty = Symbol -> Doc
printSymbol
instance Pretty Sign where
pretty :: Sign -> Doc
pretty = Sign -> Doc
printSign
instance Pretty BASIC_SPEC where
pretty :: BASIC_SPEC -> Doc
pretty = BASIC_SPEC -> Doc
printBasicSpec
instance Pretty TPTP where
pretty :: TPTP -> Doc
pretty = TPTP -> Doc
printTPTP
instance Pretty TPTP_input where
pretty :: TPTP_input -> Doc
pretty = TPTP_input -> Doc
printTPTP_input
instance Pretty Comment where
pretty :: Comment -> Doc
pretty = Comment -> Doc
printComment
instance Pretty DefinedComment where
pretty :: DefinedComment -> Doc
pretty = DefinedComment -> Doc
printDefinedComment
instance Pretty SystemComment where
pretty :: SystemComment -> Doc
pretty = SystemComment -> Doc
printSystemComment
instance Pretty Annotated_formula where
pretty :: Annotated_formula -> Doc
pretty = Annotated_formula -> Doc
printAnnotated_formula
instance Pretty TPI_annotated where
pretty :: TPI_annotated -> Doc
pretty = TPI_annotated -> Doc
printTPI_annotated
instance Pretty THF_annotated where
pretty :: THF_annotated -> Doc
pretty = THF_annotated -> Doc
printTHF_annotated
instance Pretty TFX_annotated where
pretty :: TFX_annotated -> Doc
pretty = TFX_annotated -> Doc
printTFX_annotated
instance Pretty TFF_annotated where
pretty :: TFF_annotated -> Doc
pretty = TFF_annotated -> Doc
printTFF_annotated
instance Pretty TCF_annotated where
pretty :: TCF_annotated -> Doc
pretty = TCF_annotated -> Doc
printTCF_annotated
instance Pretty FOF_annotated where
pretty :: FOF_annotated -> Doc
pretty = FOF_annotated -> Doc
printFOF_annotated
instance Pretty CNF_annotated where
pretty :: CNF_annotated -> Doc
pretty = CNF_annotated -> Doc
printCNF_annotated
instance Pretty Annotations where
pretty :: Annotations -> Doc
pretty = Annotations -> Doc
printAnnotations
instance Pretty Formula_role where
pretty :: Formula_role -> Doc
pretty = Formula_role -> Doc
printFormula_role
instance Pretty THF_formula where
pretty :: THF_formula -> Doc
pretty = THF_formula -> Doc
printTHF_formula
instance Pretty THF_logic_formula where
pretty :: THF_logic_formula -> Doc
pretty = THF_logic_formula -> Doc
printTHF_logic_formula
instance Pretty THF_binary_formula where
pretty :: THF_binary_formula -> Doc
pretty = THF_binary_formula -> Doc
printTHF_binary_formula
instance Pretty THF_binary_pair where
pretty :: THF_binary_pair -> Doc
pretty = THF_binary_pair -> Doc
printTHF_binary_pair
instance Pretty THF_binary_tuple where
pretty :: THF_binary_tuple -> Doc
pretty = THF_binary_tuple -> Doc
printTHF_binary_tuple
instance Pretty THF_unitary_formula where
pretty :: THF_unitary_formula -> Doc
pretty = THF_unitary_formula -> Doc
printTHF_unitary_formula
instance Pretty THF_quantified_formula where
pretty :: THF_quantified_formula -> Doc
pretty = THF_quantified_formula -> Doc
printTHF_quantified_formula
instance Pretty THF_quantification where
pretty :: THF_quantification -> Doc
pretty = THF_quantification -> Doc
printTHF_quantification
instance Pretty THF_variable where
pretty :: THF_variable -> Doc
pretty = THF_variable -> Doc
printTHF_variable
instance Pretty THF_typed_variable where
pretty :: THF_typed_variable -> Doc
pretty = THF_typed_variable -> Doc
printTHF_typed_variable
instance Pretty THF_unary_formula where
pretty :: THF_unary_formula -> Doc
pretty = THF_unary_formula -> Doc
printTHF_unary_formula
instance Pretty THF_atom where
pretty :: THF_atom -> Doc
pretty = THF_atom -> Doc
printTHF_atom
instance Pretty THF_function where
pretty :: THF_function -> Doc
pretty = THF_function -> Doc
printTHF_function
instance Pretty THF_conn_term where
pretty :: THF_conn_term -> Doc
pretty = THF_conn_term -> Doc
printTHF_conn_term
instance Pretty THF_conditional where
pretty :: THF_conditional -> Doc
pretty = THF_conditional -> Doc
printTHF_conditional
instance Pretty THF_let where
pretty :: THF_let -> Doc
pretty = THF_let -> Doc
printTHF_let
instance Pretty THF_let_defns where
pretty :: THF_let_defns -> Doc
pretty = THF_let_defns -> Doc
printTHF_let_defns
instance Pretty THF_let_defn where
pretty :: THF_let_defn -> Doc
pretty = THF_let_defn -> Doc
printTHF_let_defn
instance Pretty THF_let_quantified_defn where
pretty :: THF_let_quantified_defn -> Doc
pretty = THF_let_quantified_defn -> Doc
printTHF_let_quantified_defn
instance Pretty THF_let_plain_defn where
pretty :: THF_let_plain_defn -> Doc
pretty = THF_let_plain_defn -> Doc
printTHF_let_plain_defn
instance Pretty THF_let_defn_LHS where
pretty :: THF_let_defn_LHS -> Doc
pretty = THF_let_defn_LHS -> Doc
printTHF_let_defn_LHS
instance Pretty THF_type_formula where
pretty :: THF_type_formula -> Doc
pretty = THF_type_formula -> Doc
printTHF_type_formula
instance Pretty THF_typeable_formula where
pretty :: THF_typeable_formula -> Doc
pretty = THF_typeable_formula -> Doc
printTHF_typeable_formula
instance Pretty THF_subtype where
pretty :: THF_subtype -> Doc
pretty = THF_subtype -> Doc
printTHF_subtype
instance Pretty THF_top_level_type where
pretty :: THF_top_level_type -> Doc
pretty = THF_top_level_type -> Doc
printTHF_top_level_type
instance Pretty THF_unitary_type where
pretty :: THF_unitary_type -> Doc
pretty = THF_unitary_type -> Doc
printTHF_unitary_type
instance Pretty THF_binary_type where
pretty :: THF_binary_type -> Doc
pretty = THF_binary_type -> Doc
printTHF_binary_type
instance Pretty THF_sequent where
pretty :: THF_sequent -> Doc
pretty = THF_sequent -> Doc
printTHF_sequent
instance Pretty THF_tuple where
pretty :: THF_tuple -> Doc
pretty = THF_tuple -> Doc
printTHF_tuple
instance Pretty TFX_formula where
pretty :: TFX_formula -> Doc
pretty = TFX_formula -> Doc
printTFX_formula
instance Pretty TFX_logic_formula where
pretty :: TFX_logic_formula -> Doc
pretty = TFX_logic_formula -> Doc
printTFX_logic_formula
instance Pretty TFF_formula where
pretty :: TFF_formula -> Doc
pretty = TFF_formula -> Doc
printTFF_formula
instance Pretty TFF_logic_formula where
pretty :: TFF_logic_formula -> Doc
pretty = TFF_logic_formula -> Doc
printTFF_logic_formula
instance Pretty TFF_binary_formula where
pretty :: TFF_binary_formula -> Doc
pretty = TFF_binary_formula -> Doc
printTFF_binary_formula
instance Pretty TFF_binary_nonassoc where
pretty :: TFF_binary_nonassoc -> Doc
pretty = TFF_binary_nonassoc -> Doc
printTFF_binary_nonassoc
instance Pretty TFF_binary_assoc where
pretty :: TFF_binary_assoc -> Doc
pretty = TFF_binary_assoc -> Doc
printTFF_binary_assoc
instance Pretty TFF_unitary_formula where
pretty :: TFF_unitary_formula -> Doc
pretty = TFF_unitary_formula -> Doc
printTFF_unitary_formula
instance Pretty TFF_quantified_formula where
pretty :: TFF_quantified_formula -> Doc
pretty = TFF_quantified_formula -> Doc
printTFF_quantified_formula
instance Pretty TFF_variable where
pretty :: TFF_variable -> Doc
pretty = TFF_variable -> Doc
printTFF_variable
instance Pretty TFF_typed_variable where
pretty :: TFF_typed_variable -> Doc
pretty = TFF_typed_variable -> Doc
printTFF_typed_variable
instance Pretty TFF_unary_formula where
pretty :: TFF_unary_formula -> Doc
pretty = TFF_unary_formula -> Doc
printTFF_unary_formula
instance Pretty TFF_conditional where
pretty :: TFF_conditional -> Doc
pretty = TFF_conditional -> Doc
printTFF_conditional
instance Pretty TFF_let where
pretty :: TFF_let -> Doc
pretty = TFF_let -> Doc
printTFF_let
instance Pretty TFF_let_term_defns where
pretty :: TFF_let_term_defns -> Doc
pretty = TFF_let_term_defns -> Doc
printTFF_let_term_defns
instance Pretty TFF_let_term_defn where
pretty :: TFF_let_term_defn -> Doc
pretty = TFF_let_term_defn -> Doc
printTFF_let_term_defn
instance Pretty TFF_let_term_binding where
pretty :: TFF_let_term_binding -> Doc
pretty = TFF_let_term_binding -> Doc
printTFF_let_term_binding
instance Pretty TFF_let_formula_defns where
pretty :: TFF_let_formula_defns -> Doc
pretty = TFF_let_formula_defns -> Doc
printTFF_let_formula_defns
instance Pretty TFF_let_formula_defn where
pretty :: TFF_let_formula_defn -> Doc
pretty = TFF_let_formula_defn -> Doc
printTFF_let_formula_defn
instance Pretty TFF_let_formula_binding where
pretty :: TFF_let_formula_binding -> Doc
pretty = TFF_let_formula_binding -> Doc
printTFF_let_formula_binding
instance Pretty TFF_sequent where
pretty :: TFF_sequent -> Doc
pretty = TFF_sequent -> Doc
printTFF_sequent
instance Pretty TFF_formula_tuple where
pretty :: TFF_formula_tuple -> Doc
pretty = TFF_formula_tuple -> Doc
printTFF_formula_tuple
instance Pretty TFF_typed_atom where
pretty :: TFF_typed_atom -> Doc
pretty = TFF_typed_atom -> Doc
printTFF_typed_atom
instance Pretty TFF_subtype where
pretty :: TFF_subtype -> Doc
pretty = TFF_subtype -> Doc
printTFF_subtype
instance Pretty TFF_top_level_type where
pretty :: TFF_top_level_type -> Doc
pretty = TFF_top_level_type -> Doc
printTFF_top_level_type
instance Pretty TF1_quantified_type where
pretty :: TF1_quantified_type -> Doc
pretty = TF1_quantified_type -> Doc
printTF1_quantified_type
instance Pretty TFF_monotype where
pretty :: TFF_monotype -> Doc
pretty = TFF_monotype -> Doc
printTFF_monotype
instance Pretty TFF_unitary_type where
pretty :: TFF_unitary_type -> Doc
pretty = TFF_unitary_type -> Doc
printTFF_unitary_type
instance Pretty TFF_atomic_type where
pretty :: TFF_atomic_type -> Doc
pretty = TFF_atomic_type -> Doc
printTFF_atomic_type
instance Pretty TFF_mapping_type where
pretty :: TFF_mapping_type -> Doc
pretty = TFF_mapping_type -> Doc
printTFF_mapping_type
instance Pretty TFF_xprod_type where
pretty :: TFF_xprod_type -> Doc
pretty = TFF_xprod_type -> Doc
printTFF_xprod_type
instance Pretty TCF_formula where
pretty :: TCF_formula -> Doc
pretty = TCF_formula -> Doc
printTCF_formula
instance Pretty TCF_logic_formula where
pretty :: TCF_logic_formula -> Doc
pretty = TCF_logic_formula -> Doc
printTCF_logic_formula
instance Pretty TCF_quantified_formula where
pretty :: TCF_quantified_formula -> Doc
pretty = TCF_quantified_formula -> Doc
printTCF_quantified_formula
instance Pretty FOF_formula where
pretty :: FOF_formula -> Doc
pretty = FOF_formula -> Doc
printFOF_formula
instance Pretty FOF_logic_formula where
pretty :: FOF_logic_formula -> Doc
pretty = FOF_logic_formula -> Doc
printFOF_logic_formula
instance Pretty FOF_binary_formula where
pretty :: FOF_binary_formula -> Doc
pretty = FOF_binary_formula -> Doc
printFOF_binary_formula
instance Pretty FOF_binary_nonassoc where
pretty :: FOF_binary_nonassoc -> Doc
pretty = FOF_binary_nonassoc -> Doc
printFOF_binary_nonassoc
instance Pretty FOF_binary_assoc where
pretty :: FOF_binary_assoc -> Doc
pretty = FOF_binary_assoc -> Doc
printFOF_binary_assoc
instance Pretty FOF_unitary_formula where
pretty :: FOF_unitary_formula -> Doc
pretty = FOF_unitary_formula -> Doc
printFOF_unitary_formula
instance Pretty FOF_quantified_formula where
pretty :: FOF_quantified_formula -> Doc
pretty = FOF_quantified_formula -> Doc
printFOF_quantified_formula
instance Pretty FOF_unary_formula where
pretty :: FOF_unary_formula -> Doc
pretty = FOF_unary_formula -> Doc
printFOF_unary_formula
instance Pretty FOF_infix_unary where
pretty :: FOF_infix_unary -> Doc
pretty = FOF_infix_unary -> Doc
printFOF_infix_unary
instance Pretty FOF_atomic_formula where
pretty :: FOF_atomic_formula -> Doc
pretty = FOF_atomic_formula -> Doc
printFOF_atomic_formula
instance Pretty FOF_plain_atomic_formula where
pretty :: FOF_plain_atomic_formula -> Doc
pretty = FOF_plain_atomic_formula -> Doc
printFOF_plain_atomic_formula
instance Pretty FOF_defined_atomic_formula where
pretty :: FOF_defined_atomic_formula -> Doc
pretty = FOF_defined_atomic_formula -> Doc
printFOF_defined_atomic_formula
instance Pretty FOF_defined_plain_formula where
pretty :: FOF_defined_plain_formula -> Doc
pretty = FOF_defined_plain_formula -> Doc
printFOF_defined_plain_formula
instance Pretty FOF_defined_infix_formula where
pretty :: FOF_defined_infix_formula -> Doc
pretty = FOF_defined_infix_formula -> Doc
printFOF_defined_infix_formula
instance Pretty FOF_system_atomic_formula where
pretty :: FOF_system_atomic_formula -> Doc
pretty = FOF_system_atomic_formula -> Doc
printFOF_system_atomic_formula
instance Pretty FOF_plain_term where
pretty :: FOF_plain_term -> Doc
pretty = FOF_plain_term -> Doc
printFOF_plain_term
instance Pretty FOF_defined_term where
pretty :: FOF_defined_term -> Doc
pretty = FOF_defined_term -> Doc
printFOF_defined_term
instance Pretty FOF_defined_atomic_term where
pretty :: FOF_defined_atomic_term -> Doc
pretty = FOF_defined_atomic_term -> Doc
printFOF_defined_atomic_term
instance Pretty FOF_defined_plain_term where
pretty :: FOF_defined_plain_term -> Doc
pretty = FOF_defined_plain_term -> Doc
printFOF_defined_plain_term
instance Pretty FOF_system_term where
pretty :: FOF_system_term -> Doc
pretty = FOF_system_term -> Doc
printFOF_system_term
instance Pretty FOF_term where
pretty :: FOF_term -> Doc
pretty = FOF_term -> Doc
printFOF_term
instance Pretty FOF_function_term where
pretty :: FOF_function_term -> Doc
pretty = FOF_function_term -> Doc
printFOF_function_term
instance Pretty TFF_conditional_term where
pretty :: TFF_conditional_term -> Doc
pretty = TFF_conditional_term -> Doc
printTFF_conditional_term
instance Pretty TFF_let_term where
pretty :: TFF_let_term -> Doc
pretty = TFF_let_term -> Doc
printTFF_let_term
instance Pretty FOF_sequent where
pretty :: FOF_sequent -> Doc
pretty = FOF_sequent -> Doc
printFOF_sequent
instance Pretty FOF_formula_tuple where
pretty :: FOF_formula_tuple -> Doc
pretty = FOF_formula_tuple -> Doc
printFOF_formula_tuple
instance Pretty CNF_formula where
pretty :: CNF_formula -> Doc
pretty = CNF_formula -> Doc
printCNF_formula
instance Pretty Disjunction where
pretty :: Disjunction -> Doc
pretty = Disjunction -> Doc
printDisjunction
instance Pretty Literal where
pretty :: Literal -> Doc
pretty = Literal -> Doc
printLiteral
instance Pretty THF_quantifier where
pretty :: THF_quantifier -> Doc
pretty = THF_quantifier -> Doc
printTHF_quantifier
instance Pretty TH1_quantifier where
pretty :: TH1_quantifier -> Doc
pretty = TH1_quantifier -> Doc
printTH1_quantifier
instance Pretty TH0_quantifier where
pretty :: TH0_quantifier -> Doc
pretty = TH0_quantifier -> Doc
printTH0_quantifier
instance Pretty THF_pair_connective where
pretty :: THF_pair_connective -> Doc
pretty = THF_pair_connective -> Doc
printTHF_pair_connective
instance Pretty THF_unary_connective where
pretty :: THF_unary_connective -> Doc
pretty = THF_unary_connective -> Doc
printTHF_unary_connective
instance Pretty TH1_unary_connective where
pretty :: TH1_unary_connective -> Doc
pretty = TH1_unary_connective -> Doc
printTH1_unary_connective
instance Pretty FOF_quantifier where
pretty :: FOF_quantifier -> Doc
pretty = FOF_quantifier -> Doc
printFOF_quantifier
instance Pretty Binary_connective where
pretty :: Binary_connective -> Doc
pretty = Binary_connective -> Doc
printBinary_connective
instance Pretty Assoc_connective where
pretty :: Assoc_connective -> Doc
pretty = Assoc_connective -> Doc
printAssoc_connective
instance Pretty Unary_connective where
pretty :: Unary_connective -> Doc
pretty = Unary_connective -> Doc
printUnary_connective
instance Pretty Defined_type where
pretty :: Defined_type -> Doc
pretty = Defined_type -> Doc
printDefined_type
instance Pretty Atom where
pretty :: Atom -> Doc
pretty = Atom -> Doc
printAtom
instance Pretty Untyped_atom where
pretty :: Untyped_atom -> Doc
pretty = Untyped_atom -> Doc
printUntyped_atom
instance Pretty Defined_proposition where
pretty :: Defined_proposition -> Doc
pretty = Defined_proposition -> Doc
printDefined_proposition
instance Pretty Defined_predicate where
pretty :: Defined_predicate -> Doc
pretty = Defined_predicate -> Doc
printDefined_predicate
instance Pretty Defined_infix_pred where
pretty :: Defined_infix_pred -> Doc
pretty = Defined_infix_pred -> Doc
printDefined_infix_pred
instance Pretty Defined_functor where
pretty :: Defined_functor -> Doc
pretty = Defined_functor -> Doc
printDefined_functor
instance Pretty Defined_term where
pretty :: Defined_term -> Doc
pretty = Defined_term -> Doc
printDefined_term
instance Pretty Source where
pretty :: Source -> Doc
pretty = Source -> Doc
printSource
instance Pretty DAG_source where
pretty :: DAG_source -> Doc
pretty = DAG_source -> Doc
printDAG_source
instance Pretty Inference_record where
pretty :: Inference_record -> Doc
pretty = Inference_record -> Doc
printInference_record
instance Pretty Parent_info where
pretty :: Parent_info -> Doc
pretty = Parent_info -> Doc
printParent_info
instance Pretty Internal_source where
pretty :: Internal_source -> Doc
pretty = Internal_source -> Doc
printInternal_source
instance Pretty Intro_type where
pretty :: Intro_type -> Doc
pretty = Intro_type -> Doc
printIntro_type
instance Pretty External_source where
pretty :: External_source -> Doc
pretty = External_source -> Doc
printExternal_source
instance Pretty File_source where
pretty :: File_source -> Doc
pretty = File_source -> Doc
printFile_source
instance Pretty Theory where
pretty :: Theory -> Doc
pretty = Theory -> Doc
printTheory
instance Pretty Theory_name where
pretty :: Theory_name -> Doc
pretty = Theory_name -> Doc
printTheory_name
instance Pretty Creator_source where
pretty :: Creator_source -> Doc
pretty = Creator_source -> Doc
printCreator_source
instance Pretty Useful_info where
pretty :: Useful_info -> Doc
pretty = Useful_info -> Doc
printUseful_info
instance Pretty Info_item where
pretty :: Info_item -> Doc
pretty = Info_item -> Doc
printInfo_item
instance Pretty Formula_item where
pretty :: Formula_item -> Doc
pretty = Formula_item -> Doc
printFormula_item
instance Pretty Inference_item where
pretty :: Inference_item -> Doc
pretty = Inference_item -> Doc
printInference_item
instance Pretty Inference_status where
pretty :: Inference_status -> Doc
pretty = Inference_status -> Doc
printInference_status
instance Pretty Status_value where
pretty :: Status_value -> Doc
pretty = Status_value -> Doc
printStatus_value
instance Pretty Inference_info where
pretty :: Inference_info -> Doc
pretty = Inference_info -> Doc
printInference_info
instance Pretty New_symbol_record where
pretty :: New_symbol_record -> Doc
pretty = New_symbol_record -> Doc
printNew_symbol_record
instance Pretty Principal_symbol where
pretty :: Principal_symbol -> Doc
pretty = Principal_symbol -> Doc
printPrincipal_symbol
instance Pretty Include where
pretty :: Include -> Doc
pretty = Include -> Doc
printInclude
instance Pretty General_term where
pretty :: General_term -> Doc
pretty = General_term -> Doc
printGeneral_term
instance Pretty General_data where
pretty :: General_data -> Doc
pretty = General_data -> Doc
printGeneral_data
instance Pretty General_function where
pretty :: General_function -> Doc
pretty = General_function -> Doc
printGeneral_function
instance Pretty Formula_data where
pretty :: Formula_data -> Doc
pretty = Formula_data -> Doc
printFormula_data
instance Pretty Name where
pretty :: Name -> Doc
pretty = Name -> Doc
printName
instance Pretty Number where
pretty :: Number -> Doc
pretty = Number -> Doc
printNumber
printBasicTheory :: (Sign, [Named Sentence]) -> Doc
printBasicTheory :: (Sign, [Named Annotated_formula]) -> Doc
printBasicTheory (_, l :: [Named Annotated_formula]
l) = [Doc] -> Doc
vsep ((Named Annotated_formula -> Doc)
-> [Named Annotated_formula] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Named Annotated_formula -> Doc
printNamedSentence [Named Annotated_formula]
l) Doc -> Doc -> Doc
$+$ String -> Doc
text ""
printNamedSentence :: Named Sentence -> Doc
printNamedSentence :: Named Annotated_formula -> Doc
printNamedSentence = Annotated_formula -> Doc
printAnnotated_formula (Annotated_formula -> Doc)
-> (Named Annotated_formula -> Annotated_formula)
-> Named Annotated_formula
-> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Named Annotated_formula -> Annotated_formula
forall s a. SenAttr s a -> s
sentence (Named Annotated_formula -> Annotated_formula)
-> (Named Annotated_formula -> Named Annotated_formula)
-> Named Annotated_formula
-> Annotated_formula
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Named Annotated_formula -> Named Annotated_formula
adjust_formula_role
printSymbol :: Symbol -> Doc
printSymbol :: Symbol -> Doc
printSymbol = Token -> Doc
forall a. Pretty a => a -> Doc
pretty (Token -> Doc) -> (Symbol -> Token) -> Symbol -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> Token
symbolId
printSign :: Sign -> Doc
printSign :: Sign -> Doc
printSign s :: Sign
s =
[Doc] -> Doc
vsep [ String -> Doc
text "%{"
, if Set Token -> Bool
forall a. Set a -> Bool
Set.null (Set Token -> Bool) -> Set Token -> Bool
forall a b. (a -> b) -> a -> b
$ Sign -> Set Token
constantSet Sign
s then Doc
empty else
String -> Doc
text "constants: "
Doc -> Doc -> Doc
<+> [Doc] -> Doc
sepByCommas ((Token -> Doc) -> [Token] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Token -> Doc
forall a. Pretty a => a -> Doc
pretty ([Token] -> [Doc]) -> [Token] -> [Doc]
forall a b. (a -> b) -> a -> b
$ Set Token -> [Token]
forall a. Set a -> [a]
Set.toList (Set Token -> [Token]) -> Set Token -> [Token]
forall a b. (a -> b) -> a -> b
$ Sign -> Set Token
constantSet Sign
s)
, if Set Number -> Bool
forall a. Set a -> Bool
Set.null (Set Number -> Bool) -> Set Number -> Bool
forall a b. (a -> b) -> a -> b
$ Sign -> Set Number
numberSet Sign
s then Doc
empty else
String -> Doc
text "numbers: "
Doc -> Doc -> Doc
<+> [Doc] -> Doc
sepByCommas ((Number -> Doc) -> [Number] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Number -> Doc
forall a. Pretty a => a -> Doc
pretty ([Number] -> [Doc]) -> [Number] -> [Doc]
forall a b. (a -> b) -> a -> b
$ Set Number -> [Number]
forall a. Set a -> [a]
Set.toList (Set Number -> [Number]) -> Set Number -> [Number]
forall a b. (a -> b) -> a -> b
$ Sign -> Set Number
numberSet Sign
s)
, if Set Token -> Bool
forall a. Set a -> Bool
Set.null (Set Token -> Bool) -> Set Token -> Bool
forall a b. (a -> b) -> a -> b
$ Sign -> Set Token
propositionSet Sign
s then Doc
empty else
String -> Doc
text "propositions: "
Doc -> Doc -> Doc
<+> [Doc] -> Doc
sepByCommas ((Token -> Doc) -> [Token] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Token -> Doc
forall a. Pretty a => a -> Doc
pretty ([Token] -> [Doc]) -> [Token] -> [Doc]
forall a b. (a -> b) -> a -> b
$ Set Token -> [Token]
forall a. Set a -> [a]
Set.toList (Set Token -> [Token]) -> Set Token -> [Token]
forall a b. (a -> b) -> a -> b
$ Sign -> Set Token
propositionSet Sign
s)
, if Map Untyped_atom TFF_top_level_type -> Bool
forall k a. Map k a -> Bool
Map.null (Sign -> Map Untyped_atom TFF_top_level_type
tffPredicateMap Sign
s) Bool -> Bool -> Bool
&& Map THFTypeable THF_top_level_type -> Bool
forall k a. Map k a -> Bool
Map.null (Sign -> Map THFTypeable THF_top_level_type
thfPredicateMap Sign
s) Bool -> Bool -> Bool
&& Map Token (Set Int) -> Bool
forall k a. Map k a -> Bool
Map.null (Sign -> Map Token (Set Int)
fofPredicateMap Sign
s) then Doc
empty else
String -> Doc
text "predicates: "
Doc -> Doc -> Doc
<+> [Doc] -> Doc
vcat (Doc -> [Doc] -> [Doc]
punctuate Doc
comma
(((THFTypeable, THF_top_level_type) -> Doc)
-> [(THFTypeable, THF_top_level_type)] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (THFTypeable, THF_top_level_type) -> Doc
printTHFType (Map THFTypeable THF_top_level_type
-> [(THFTypeable, THF_top_level_type)]
forall k a. Map k a -> [(k, a)]
Map.toList (Map THFTypeable THF_top_level_type
-> [(THFTypeable, THF_top_level_type)])
-> Map THFTypeable THF_top_level_type
-> [(THFTypeable, THF_top_level_type)]
forall a b. (a -> b) -> a -> b
$ Sign -> Map THFTypeable THF_top_level_type
thfPredicateMap Sign
s)
[Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++ ((Untyped_atom, TFF_top_level_type) -> Doc)
-> [(Untyped_atom, TFF_top_level_type)] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Untyped_atom, TFF_top_level_type) -> Doc
printTFFType (Map Untyped_atom TFF_top_level_type
-> [(Untyped_atom, TFF_top_level_type)]
forall k a. Map k a -> [(k, a)]
Map.toList (Map Untyped_atom TFF_top_level_type
-> [(Untyped_atom, TFF_top_level_type)])
-> Map Untyped_atom TFF_top_level_type
-> [(Untyped_atom, TFF_top_level_type)]
forall a b. (a -> b) -> a -> b
$ Sign -> Map Untyped_atom TFF_top_level_type
tffPredicateMap Sign
s)
[Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++ ((Token, Set Int) -> Doc) -> [(Token, Set Int)] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Token, Set Int) -> Doc
printFOFPredicate (Map Token (Set Int) -> [(Token, Set Int)]
forall k a. Map k a -> [(k, a)]
Map.toList (Map Token (Set Int) -> [(Token, Set Int)])
-> Map Token (Set Int) -> [(Token, Set Int)]
forall a b. (a -> b) -> a -> b
$ Sign -> Map Token (Set Int)
fofPredicateMap Sign
s)))
, if Map Token (Set Int) -> Bool
forall k a. Map k a -> Bool
Map.null (Sign -> Map Token (Set Int)
fofFunctorMap Sign
s) then Doc
empty else
String -> Doc
text "functors: "
Doc -> Doc -> Doc
<+> [Doc] -> Doc
vcat (Doc -> [Doc] -> [Doc]
punctuate Doc
comma
(((Token, Set Int) -> Doc) -> [(Token, Set Int)] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Token, Set Int) -> Doc
printFOFFunctor (Map Token (Set Int) -> [(Token, Set Int)]
forall k a. Map k a -> [(k, a)]
Map.toList (Map Token (Set Int) -> [(Token, Set Int)])
-> Map Token (Set Int) -> [(Token, Set Int)]
forall a b. (a -> b) -> a -> b
$ Sign -> Map Token (Set Int)
fofFunctorMap Sign
s)))
, if Map Untyped_atom TFF_top_level_type -> Bool
forall k a. Map k a -> Bool
Map.null (Sign -> Map Untyped_atom TFF_top_level_type
tffTypeConstantMap Sign
s) Bool -> Bool -> Bool
&& Map THFTypeable THF_top_level_type -> Bool
forall k a. Map k a -> Bool
Map.null (Sign -> Map THFTypeable THF_top_level_type
thfTypeConstantMap Sign
s) then Doc
empty else
String -> Doc
text "type constants: "
Doc -> Doc -> Doc
<+> [Doc] -> Doc
vcat (Doc -> [Doc] -> [Doc]
punctuate Doc
comma
(((THFTypeable, THF_top_level_type) -> Doc)
-> [(THFTypeable, THF_top_level_type)] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (THFTypeable, THF_top_level_type) -> Doc
printTHFType (Map THFTypeable THF_top_level_type
-> [(THFTypeable, THF_top_level_type)]
forall k a. Map k a -> [(k, a)]
Map.toList (Map THFTypeable THF_top_level_type
-> [(THFTypeable, THF_top_level_type)])
-> Map THFTypeable THF_top_level_type
-> [(THFTypeable, THF_top_level_type)]
forall a b. (a -> b) -> a -> b
$ Sign -> Map THFTypeable THF_top_level_type
thfTypeConstantMap Sign
s)
[Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++ ((Untyped_atom, TFF_top_level_type) -> Doc)
-> [(Untyped_atom, TFF_top_level_type)] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Untyped_atom, TFF_top_level_type) -> Doc
printTFFType (Map Untyped_atom TFF_top_level_type
-> [(Untyped_atom, TFF_top_level_type)]
forall k a. Map k a -> [(k, a)]
Map.toList (Map Untyped_atom TFF_top_level_type
-> [(Untyped_atom, TFF_top_level_type)])
-> Map Untyped_atom TFF_top_level_type
-> [(Untyped_atom, TFF_top_level_type)]
forall a b. (a -> b) -> a -> b
$ Sign -> Map Untyped_atom TFF_top_level_type
tffTypeConstantMap Sign
s)))
, if Map Untyped_atom TFF_top_level_type -> Bool
forall k a. Map k a -> Bool
Map.null (Sign -> Map Untyped_atom TFF_top_level_type
tffTypeFunctorMap Sign
s) Bool -> Bool -> Bool
&& Map THFTypeable THF_top_level_type -> Bool
forall k a. Map k a -> Bool
Map.null (Sign -> Map THFTypeable THF_top_level_type
thfTypeFunctorMap Sign
s) then Doc
empty else
String -> Doc
text "type functors: "
Doc -> Doc -> Doc
<+> [Doc] -> Doc
vcat (Doc -> [Doc] -> [Doc]
punctuate Doc
comma
(((THFTypeable, THF_top_level_type) -> Doc)
-> [(THFTypeable, THF_top_level_type)] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (THFTypeable, THF_top_level_type) -> Doc
printTHFType (Map THFTypeable THF_top_level_type
-> [(THFTypeable, THF_top_level_type)]
forall k a. Map k a -> [(k, a)]
Map.toList (Map THFTypeable THF_top_level_type
-> [(THFTypeable, THF_top_level_type)])
-> Map THFTypeable THF_top_level_type
-> [(THFTypeable, THF_top_level_type)]
forall a b. (a -> b) -> a -> b
$ Sign -> Map THFTypeable THF_top_level_type
thfTypeFunctorMap Sign
s)
[Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++ ((Untyped_atom, TFF_top_level_type) -> Doc)
-> [(Untyped_atom, TFF_top_level_type)] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Untyped_atom, TFF_top_level_type) -> Doc
printTFFType (Map Untyped_atom TFF_top_level_type
-> [(Untyped_atom, TFF_top_level_type)]
forall k a. Map k a -> [(k, a)]
Map.toList (Map Untyped_atom TFF_top_level_type
-> [(Untyped_atom, TFF_top_level_type)])
-> Map Untyped_atom TFF_top_level_type
-> [(Untyped_atom, TFF_top_level_type)]
forall a b. (a -> b) -> a -> b
$ Sign -> Map Untyped_atom TFF_top_level_type
tffTypeFunctorMap Sign
s)))
, if Map Untyped_atom Atom -> Bool
forall k a. Map k a -> Bool
Map.null (Sign -> Map Untyped_atom Atom
tffSubtypeMap Sign
s) Bool -> Bool -> Bool
&& Map THF_atom THF_atom -> Bool
forall k a. Map k a -> Bool
Map.null (Sign -> Map THF_atom THF_atom
thfSubtypeMap Sign
s) then Doc
empty else
String -> Doc
text "subtypes: "
Doc -> Doc -> Doc
<+> [Doc] -> Doc
vcat (Doc -> [Doc] -> [Doc]
punctuate Doc
comma
(((THF_atom, THF_atom) -> Doc) -> [(THF_atom, THF_atom)] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (THF_atom, THF_atom) -> Doc
printTHFSubType (Map THF_atom THF_atom -> [(THF_atom, THF_atom)]
forall k a. Map k a -> [(k, a)]
Map.toList (Map THF_atom THF_atom -> [(THF_atom, THF_atom)])
-> Map THF_atom THF_atom -> [(THF_atom, THF_atom)]
forall a b. (a -> b) -> a -> b
$ Sign -> Map THF_atom THF_atom
thfSubtypeMap Sign
s)
[Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++ ((Untyped_atom, Atom) -> Doc) -> [(Untyped_atom, Atom)] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Untyped_atom, Atom) -> Doc
printTFFSubType (Map Untyped_atom Atom -> [(Untyped_atom, Atom)]
forall k a. Map k a -> [(k, a)]
Map.toList (Map Untyped_atom Atom -> [(Untyped_atom, Atom)])
-> Map Untyped_atom Atom -> [(Untyped_atom, Atom)]
forall a b. (a -> b) -> a -> b
$ Sign -> Map Untyped_atom Atom
tffSubtypeMap Sign
s)))
, String -> Doc
text "}%"]
where
printTHFType :: (THFTypeable, THF_top_level_type) -> Doc
printTHFType :: (THFTypeable, THF_top_level_type) -> Doc
printTHFType (t :: THFTypeable
t, tlt :: THF_top_level_type
tlt) = THF_type_formula -> Doc
forall a. Pretty a => a -> Doc
pretty (THF_type_formula -> Doc) -> THF_type_formula -> Doc
forall a b. (a -> b) -> a -> b
$ case THFTypeable
t of
THFTypeFormula f :: THF_typeable_formula
f -> THF_typeable_formula -> THF_top_level_type -> THF_type_formula
THFTF_typeable THF_typeable_formula
f THF_top_level_type
tlt
THFTypeConstant c :: Token
c -> Token -> THF_top_level_type -> THF_type_formula
THFTF_constant Token
c THF_top_level_type
tlt
printTFFType :: (Untyped_atom, TFF_top_level_type) -> Doc
printTFFType :: (Untyped_atom, TFF_top_level_type) -> Doc
printTFFType (a :: Untyped_atom
a, tlt :: TFF_top_level_type
tlt) = TFF_typed_atom -> Doc
forall a. Pretty a => a -> Doc
pretty (TFF_typed_atom -> Doc) -> TFF_typed_atom -> Doc
forall a b. (a -> b) -> a -> b
$ Untyped_atom -> TFF_top_level_type -> TFF_typed_atom
TFFTA_plain Untyped_atom
a TFF_top_level_type
tlt
printFOFPredicate :: (Predicate, Set.Set Int) -> Doc
printFOFPredicate :: (Token, Set Int) -> Doc
printFOFPredicate (p :: Token
p, arities :: Set Int
arities) = [Doc] -> Doc
vcat ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> [Doc] -> [Doc]
punctuate Doc
comma ([Doc] -> [Doc]) -> [Doc] -> [Doc]
forall a b. (a -> b) -> a -> b
$
(Int -> Doc) -> [Int] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Token -> Defined_type -> Int -> Doc
printFOFPredicateOrFunctor Token
p Defined_type
O) ([Int] -> [Doc]) -> [Int] -> [Doc]
forall a b. (a -> b) -> a -> b
$ Set Int -> [Int]
forall a. Set a -> [a]
Set.toList Set Int
arities
printFOFFunctor :: (TPTP_functor, Set.Set Int) -> Doc
printFOFFunctor :: (Token, Set Int) -> Doc
printFOFFunctor (p :: Token
p, arities :: Set Int
arities) = [Doc] -> Doc
vcat ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> [Doc] -> [Doc]
punctuate Doc
comma ([Doc] -> [Doc]) -> [Doc] -> [Doc]
forall a b. (a -> b) -> a -> b
$
(Int -> Doc) -> [Int] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Token -> Defined_type -> Int -> Doc
printFOFPredicateOrFunctor Token
p Defined_type
I) ([Int] -> [Doc]) -> [Int] -> [Doc]
forall a b. (a -> b) -> a -> b
$ Set Int -> [Int]
forall a. Set a -> [a]
Set.toList Set Int
arities
printFOFPredicateOrFunctor :: Token -> Defined_type -> Int -> Doc
printFOFPredicateOrFunctor :: Token -> Defined_type -> Int -> Doc
printFOFPredicateOrFunctor token :: Token
token typ :: Defined_type
typ arity :: Int
arity =
let arguments :: Doc
arguments =
if Int
arity Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== 0
then Doc
empty
else if Int
arity Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== 1
then Defined_type -> Doc
forall a. Pretty a => a -> Doc
pretty Defined_type
I Doc -> Doc -> Doc
<+> String -> Doc
text ">"
else Doc -> Doc
parens (Doc -> [Doc] -> Doc
sepBy (String -> Doc
text "*") ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ (Defined_type -> Doc) -> [Defined_type] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Defined_type -> Doc
forall a. Pretty a => a -> Doc
pretty ([Defined_type] -> [Doc]) -> [Defined_type] -> [Doc]
forall a b. (a -> b) -> a -> b
$ Int -> Defined_type -> [Defined_type]
forall a. Int -> a -> [a]
replicate Int
arity Defined_type
I)
Doc -> Doc -> Doc
<+> String -> Doc
text ">"
in Token -> Doc
forall a. Pretty a => a -> Doc
pretty Token
token Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
colon Doc -> Doc -> Doc
<+> Doc
arguments Doc -> Doc -> Doc
<+> Defined_type -> Doc
forall a. Pretty a => a -> Doc
pretty Defined_type
typ
printTHFSubType :: (THF_atom, THF_atom) -> Doc
printTHFSubType :: (THF_atom, THF_atom) -> Doc
printTHFSubType (a1 :: THF_atom
a1, a2 :: THF_atom
a2) = THF_subtype -> Doc
forall a. Pretty a => a -> Doc
pretty (THF_subtype -> Doc) -> THF_subtype -> Doc
forall a b. (a -> b) -> a -> b
$ THF_atom -> THF_atom -> THF_subtype
THF_subtype THF_atom
a1 THF_atom
a2
printTFFSubType :: (Untyped_atom, Atom) -> Doc
printTFFSubType :: (Untyped_atom, Atom) -> Doc
printTFFSubType (a1 :: Untyped_atom
a1, a2 :: Atom
a2) = TFF_subtype -> Doc
forall a. Pretty a => a -> Doc
pretty (TFF_subtype -> Doc) -> TFF_subtype -> Doc
forall a b. (a -> b) -> a -> b
$ Untyped_atom -> Atom -> TFF_subtype
TFF_subtype Untyped_atom
a1 Atom
a2
printBasicSpec :: BASIC_SPEC -> Doc
printBasicSpec :: BASIC_SPEC -> Doc
printBasicSpec (Basic_spec xs :: [Annoted TPTP]
xs) = [Doc] -> Doc
vcat ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ (Annoted TPTP -> Doc) -> [Annoted TPTP] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Annoted TPTP -> Doc
forall a. Pretty a => a -> Doc
pretty [Annoted TPTP]
xs
printTPTP :: TPTP -> Doc
printTPTP :: TPTP -> Doc
printTPTP (TPTP tptp_inputs :: [TPTP_input]
tptp_inputs) = [Doc] -> Doc
vsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ (TPTP_input -> Doc) -> [TPTP_input] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map TPTP_input -> Doc
forall a. Pretty a => a -> Doc
pretty [TPTP_input]
tptp_inputs
printTPTP_input :: TPTP_input -> Doc
printTPTP_input :: TPTP_input -> Doc
printTPTP_input x :: TPTP_input
x = case TPTP_input
x of
Annotated_formula a :: Annotated_formula
a -> Annotated_formula -> Doc
forall a. Pretty a => a -> Doc
pretty Annotated_formula
a
TPTP_include i :: Include
i -> Include -> Doc
forall a. Pretty a => a -> Doc
pretty Include
i
TPTP_comment c :: Comment
c -> Comment -> Doc
forall a. Pretty a => a -> Doc
pretty Comment
c
TPTP_defined_comment c :: DefinedComment
c -> DefinedComment -> Doc
forall a. Pretty a => a -> Doc
pretty DefinedComment
c
TPTP_system_comment c :: SystemComment
c -> SystemComment -> Doc
forall a. Pretty a => a -> Doc
pretty SystemComment
c
printComment :: Comment -> Doc
comment :: Comment
comment = case Comment
comment of
Comment_line c :: Token
c -> String -> Doc
text "%" Doc -> Doc -> Doc
<+> Token -> Doc
forall a. Pretty a => a -> Doc
pretty Token
c
Comment_block c :: Token
c -> String -> Doc
text "/*" Doc -> Doc -> Doc
<+> Token -> Doc
forall a. Pretty a => a -> Doc
pretty Token
c Doc -> Doc -> Doc
<+> String -> Doc
text "*/"
printDefinedComment :: DefinedComment -> Doc
comment :: DefinedComment
comment = case DefinedComment
comment of
Defined_comment_line c :: Token
c -> String -> Doc
text "%$" Doc -> Doc -> Doc
<+> Token -> Doc
forall a. Pretty a => a -> Doc
pretty Token
c
Defined_comment_block c :: Token
c -> String -> Doc
text "/*$" Doc -> Doc -> Doc
<+> Token -> Doc
forall a. Pretty a => a -> Doc
pretty Token
c Doc -> Doc -> Doc
<+> String -> Doc
text "*/"
printSystemComment :: SystemComment -> Doc
comment :: SystemComment
comment = case SystemComment
comment of
System_comment_line c :: Token
c -> String -> Doc
text "%$$" Doc -> Doc -> Doc
<+> Token -> Doc
forall a. Pretty a => a -> Doc
pretty Token
c
System_comment_block c :: Token
c -> String -> Doc
text "/*$$" Doc -> Doc -> Doc
<+> Token -> Doc
forall a. Pretty a => a -> Doc
pretty Token
c Doc -> Doc -> Doc
<+> String -> Doc
text "*/"
printAnnotated_formula :: Annotated_formula -> Doc
printAnnotated_formula :: Annotated_formula -> Doc
printAnnotated_formula x :: Annotated_formula
x = case Annotated_formula
x of
AF_THF_Annotated f :: THF_annotated
f -> THF_annotated -> Doc
forall a. Pretty a => a -> Doc
pretty THF_annotated
f
AF_TFX_Annotated f :: TFX_annotated
f -> TFX_annotated -> Doc
forall a. Pretty a => a -> Doc
pretty TFX_annotated
f
AF_TFF_Annotated f :: TFF_annotated
f -> TFF_annotated -> Doc
forall a. Pretty a => a -> Doc
pretty TFF_annotated
f
AF_TCF_Annotated f :: TCF_annotated
f -> TCF_annotated -> Doc
forall a. Pretty a => a -> Doc
pretty TCF_annotated
f
AF_FOF_Annotated f :: FOF_annotated
f -> FOF_annotated -> Doc
forall a. Pretty a => a -> Doc
pretty FOF_annotated
f
AF_CNF_Annotated f :: CNF_annotated
f -> CNF_annotated -> Doc
forall a. Pretty a => a -> Doc
pretty CNF_annotated
f
AF_TPI_Annotated f :: TPI_annotated
f -> TPI_annotated -> Doc
forall a. Pretty a => a -> Doc
pretty TPI_annotated
f
printAnnotationsIfAnnotated :: Annotations -> Doc
printAnnotationsIfAnnotated :: Annotations -> Doc
printAnnotationsIfAnnotated a :: Annotations
a@(Annotations ma :: Maybe (Source, Optional_info)
ma) = case Maybe (Source, Optional_info)
ma of
Just _ -> Doc
comma Doc -> Doc -> Doc
<+> Annotations -> Doc
forall a. Pretty a => a -> Doc
pretty Annotations
a
Nothing -> Doc
empty
printTPI_annotated :: TPI_annotated -> Doc
printTPI_annotated :: TPI_annotated -> Doc
printTPI_annotated x :: TPI_annotated
x = case TPI_annotated
x of
TPI_annotated n :: Name
n r :: Formula_role
r f :: FOF_formula
f a :: Annotations
a ->
String -> Doc
text "tpi"
Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc -> Doc
parens ([Doc] -> Doc
sepByCommas [Name -> Doc
forall a. Pretty a => a -> Doc
pretty Name
n, Formula_role -> Doc
forall a. Pretty a => a -> Doc
pretty Formula_role
r, FOF_formula -> Doc
forall a. Pretty a => a -> Doc
pretty FOF_formula
f] Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Annotations -> Doc
printAnnotationsIfAnnotated Annotations
a)
Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> String -> Doc
text "."
printTHF_annotated :: THF_annotated -> Doc
printTHF_annotated :: THF_annotated -> Doc
printTHF_annotated x :: THF_annotated
x = case THF_annotated
x of
THF_annotated n :: Name
n r :: Formula_role
r f :: THF_formula
f a :: Annotations
a ->
String -> Doc
text "thf"
Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc -> Doc
parens ([Doc] -> Doc
sepByCommas [Name -> Doc
forall a. Pretty a => a -> Doc
pretty Name
n, Formula_role -> Doc
forall a. Pretty a => a -> Doc
pretty Formula_role
r, THF_formula -> Doc
forall a. Pretty a => a -> Doc
pretty THF_formula
f] Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Annotations -> Doc
printAnnotationsIfAnnotated Annotations
a)
Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> String -> Doc
text "."
printTFX_annotated :: TFX_annotated -> Doc
printTFX_annotated :: TFX_annotated -> Doc
printTFX_annotated x :: TFX_annotated
x = case TFX_annotated
x of
TFX_annotated n :: Name
n r :: Formula_role
r f :: TFX_formula
f a :: Annotations
a ->
String -> Doc
text "tfx"
Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc -> Doc
parens ([Doc] -> Doc
sepByCommas [Name -> Doc
forall a. Pretty a => a -> Doc
pretty Name
n, Formula_role -> Doc
forall a. Pretty a => a -> Doc
pretty Formula_role
r, TFX_formula -> Doc
forall a. Pretty a => a -> Doc
pretty TFX_formula
f] Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Annotations -> Doc
printAnnotationsIfAnnotated Annotations
a)
Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> String -> Doc
text "."
printTFF_annotated :: TFF_annotated -> Doc
printTFF_annotated :: TFF_annotated -> Doc
printTFF_annotated x :: TFF_annotated
x = case TFF_annotated
x of
TFF_annotated n :: Name
n r :: Formula_role
r f :: TFF_formula
f a :: Annotations
a ->
String -> Doc
text "tff"
Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc -> Doc
parens ([Doc] -> Doc
sepByCommas [Name -> Doc
forall a. Pretty a => a -> Doc
pretty Name
n, Formula_role -> Doc
forall a. Pretty a => a -> Doc
pretty Formula_role
r, TFF_formula -> Doc
forall a. Pretty a => a -> Doc
pretty TFF_formula
f] Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Annotations -> Doc
printAnnotationsIfAnnotated Annotations
a)
Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> String -> Doc
text "."
printTCF_annotated :: TCF_annotated -> Doc
printTCF_annotated :: TCF_annotated -> Doc
printTCF_annotated x :: TCF_annotated
x = case TCF_annotated
x of
TCF_annotated n :: Name
n r :: Formula_role
r f :: TCF_formula
f a :: Annotations
a ->
String -> Doc
text "tcf"
Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc -> Doc
parens ([Doc] -> Doc
sepByCommas [Name -> Doc
forall a. Pretty a => a -> Doc
pretty Name
n, Formula_role -> Doc
forall a. Pretty a => a -> Doc
pretty Formula_role
r, TCF_formula -> Doc
forall a. Pretty a => a -> Doc
pretty TCF_formula
f] Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Annotations -> Doc
printAnnotationsIfAnnotated Annotations
a)
Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> String -> Doc
text "."
printFOF_annotated :: FOF_annotated -> Doc
printFOF_annotated :: FOF_annotated -> Doc
printFOF_annotated x :: FOF_annotated
x = case FOF_annotated
x of
FOF_annotated n :: Name
n r :: Formula_role
r f :: FOF_formula
f a :: Annotations
a ->
String -> Doc
text "fof"
Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc -> Doc
parens ([Doc] -> Doc
sepByCommas [Name -> Doc
forall a. Pretty a => a -> Doc
pretty Name
n, Formula_role -> Doc
forall a. Pretty a => a -> Doc
pretty Formula_role
r, FOF_formula -> Doc
forall a. Pretty a => a -> Doc
pretty FOF_formula
f] Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Annotations -> Doc
printAnnotationsIfAnnotated Annotations
a)
Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> String -> Doc
text "."
printCNF_annotated :: CNF_annotated -> Doc
printCNF_annotated :: CNF_annotated -> Doc
printCNF_annotated x :: CNF_annotated
x = case CNF_annotated
x of
CNF_annotated n :: Name
n r :: Formula_role
r f :: CNF_formula
f a :: Annotations
a ->
String -> Doc
text "cnf"
Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc -> Doc
parens ([Doc] -> Doc
sepByCommas [Name -> Doc
forall a. Pretty a => a -> Doc
pretty Name
n, Formula_role -> Doc
forall a. Pretty a => a -> Doc
pretty Formula_role
r, CNF_formula -> Doc
forall a. Pretty a => a -> Doc
pretty CNF_formula
f]
Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Annotations -> Doc
printAnnotationsIfAnnotated Annotations
a)
Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> String -> Doc
text "."
printAnnotations :: Annotations -> Doc
printAnnotations :: Annotations -> Doc
printAnnotations (Annotations mAnno :: Maybe (Source, Optional_info)
mAnno) = case Maybe (Source, Optional_info)
mAnno of
Nothing -> Doc
empty
Just (source :: Source
source, optionalInfo :: Optional_info
optionalInfo) ->
[Doc] -> Doc
fsep [Source -> Doc
forall a. Pretty a => a -> Doc
pretty Source
source, Optional_info -> Doc
printOptional_info Optional_info
optionalInfo]
printFormula_role :: Formula_role -> Doc
printFormula_role :: Formula_role -> Doc
printFormula_role x :: Formula_role
x = case Formula_role
x of
Other_formula_role t :: Token
t -> Token -> Doc
forall a. Pretty a => a -> Doc
pretty Token
t
_ -> String -> Doc
text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ (Char -> Char) -> String -> String
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toLower (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ Formula_role -> String
forall a. Show a => a -> String
show Formula_role
x
printTHF_formula :: THF_formula -> Doc
printTHF_formula :: THF_formula -> Doc
printTHF_formula x :: THF_formula
x = case THF_formula
x of
THFF_logic f :: THF_logic_formula
f -> THF_logic_formula -> Doc
forall a. Pretty a => a -> Doc
pretty THF_logic_formula
f
THFF_sequent s :: THF_sequent
s -> THF_sequent -> Doc
forall a. Pretty a => a -> Doc
pretty THF_sequent
s
printTHF_logic_formula :: THF_logic_formula -> Doc
printTHF_logic_formula :: THF_logic_formula -> Doc
printTHF_logic_formula x :: THF_logic_formula
x = case THF_logic_formula
x of
THFLF_binary f :: THF_binary_formula
f -> THF_binary_formula -> Doc
forall a. Pretty a => a -> Doc
pretty THF_binary_formula
f
THFLF_unitary f :: THF_unitary_formula
f -> THF_unitary_formula -> Doc
forall a. Pretty a => a -> Doc
pretty THF_unitary_formula
f
THFLF_type f :: THF_type_formula
f -> THF_type_formula -> Doc
forall a. Pretty a => a -> Doc
pretty THF_type_formula
f
THFLF_subtype f :: THF_subtype
f -> THF_subtype -> Doc
forall a. Pretty a => a -> Doc
pretty THF_subtype
f
printTHF_binary_formula :: THF_binary_formula -> Doc
printTHF_binary_formula :: THF_binary_formula -> Doc
printTHF_binary_formula x :: THF_binary_formula
x = case THF_binary_formula
x of
THFBF_pair a :: THF_binary_pair
a -> THF_binary_pair -> Doc
forall a. Pretty a => a -> Doc
pretty THF_binary_pair
a
THFBF_tuple a :: THF_binary_tuple
a -> THF_binary_tuple -> Doc
forall a. Pretty a => a -> Doc
pretty THF_binary_tuple
a
printTHF_binary_pair :: THF_binary_pair -> Doc
printTHF_binary_pair :: THF_binary_pair -> Doc
printTHF_binary_pair x :: THF_binary_pair
x = case THF_binary_pair
x of
THF_binary_pair c :: THF_pair_connective
c f1 :: THF_unitary_formula
f1 f2 :: THF_unitary_formula
f2 -> [Doc] -> Doc
fsep [THF_unitary_formula -> Doc
forall a. Pretty a => a -> Doc
pretty THF_unitary_formula
f1, THF_pair_connective -> Doc
forall a. Pretty a => a -> Doc
pretty THF_pair_connective
c, THF_unitary_formula -> Doc
forall a. Pretty a => a -> Doc
pretty THF_unitary_formula
f2]
printTHF_binary_tuple :: THF_binary_tuple -> Doc
printTHF_binary_tuple :: THF_binary_tuple -> Doc
printTHF_binary_tuple x :: THF_binary_tuple
x = case THF_binary_tuple
x of
THFBT_or fs :: [THF_unitary_formula]
fs -> [THF_unitary_formula] -> Doc
printTHF_or_formula [THF_unitary_formula]
fs
THFBT_and fs :: [THF_unitary_formula]
fs -> [THF_unitary_formula] -> Doc
printTHF_and_formula [THF_unitary_formula]
fs
THFBT_apply fs :: [THF_unitary_formula]
fs -> [THF_unitary_formula] -> Doc
printTHF_apply_formula [THF_unitary_formula]
fs
printTHF_or_formula :: THF_or_formula -> Doc
printTHF_or_formula :: [THF_unitary_formula] -> Doc
printTHF_or_formula fs :: [THF_unitary_formula]
fs = Doc -> [Doc] -> Doc
sepBy Doc
vline ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ (THF_unitary_formula -> Doc) -> [THF_unitary_formula] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map THF_unitary_formula -> Doc
forall a. Pretty a => a -> Doc
pretty [THF_unitary_formula]
fs
printTHF_and_formula :: THF_or_formula -> Doc
printTHF_and_formula :: [THF_unitary_formula] -> Doc
printTHF_and_formula fs :: [THF_unitary_formula]
fs = Doc -> [Doc] -> Doc
sepBy Doc
andD ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ (THF_unitary_formula -> Doc) -> [THF_unitary_formula] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map THF_unitary_formula -> Doc
forall a. Pretty a => a -> Doc
pretty [THF_unitary_formula]
fs
printTHF_apply_formula :: THF_or_formula -> Doc
printTHF_apply_formula :: [THF_unitary_formula] -> Doc
printTHF_apply_formula fs :: [THF_unitary_formula]
fs = Doc -> [Doc] -> Doc
sepBy Doc
atD ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ (THF_unitary_formula -> Doc) -> [THF_unitary_formula] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map THF_unitary_formula -> Doc
forall a. Pretty a => a -> Doc
pretty [THF_unitary_formula]
fs
printTHF_unitary_formula :: THF_unitary_formula -> Doc
printTHF_unitary_formula :: THF_unitary_formula -> Doc
printTHF_unitary_formula x :: THF_unitary_formula
x = case THF_unitary_formula
x of
THFUF_quantified a :: THF_quantified_formula
a -> THF_quantified_formula -> Doc
forall a. Pretty a => a -> Doc
pretty THF_quantified_formula
a
THFUF_unary a :: THF_unary_formula
a -> THF_unary_formula -> Doc
forall a. Pretty a => a -> Doc
pretty THF_unary_formula
a
THFUF_atom a :: THF_atom
a -> THF_atom -> Doc
forall a. Pretty a => a -> Doc
pretty THF_atom
a
THFUF_conditional a :: THF_conditional
a -> THF_conditional -> Doc
forall a. Pretty a => a -> Doc
pretty THF_conditional
a
THFUF_let a :: THF_let
a -> THF_let -> Doc
forall a. Pretty a => a -> Doc
pretty THF_let
a
THFUF_tuple a :: THF_tuple
a -> THF_tuple -> Doc
forall a. Pretty a => a -> Doc
pretty THF_tuple
a
THFUF_logic a :: THF_logic_formula
a -> Doc -> Doc
parens (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ THF_logic_formula -> Doc
forall a. Pretty a => a -> Doc
pretty THF_logic_formula
a
printTHF_quantified_formula :: THF_quantified_formula -> Doc
printTHF_quantified_formula :: THF_quantified_formula -> Doc
printTHF_quantified_formula x :: THF_quantified_formula
x = case THF_quantified_formula
x of
THF_quantified_formula q :: THF_quantification
q f :: THF_unitary_formula
f -> [Doc] -> Doc
hsep [THF_quantification -> Doc
forall a. Pretty a => a -> Doc
pretty THF_quantification
q, THF_unitary_formula -> Doc
forall a. Pretty a => a -> Doc
pretty THF_unitary_formula
f]
printTHF_quantification :: THF_quantification -> Doc
printTHF_quantification :: THF_quantification -> Doc
printTHF_quantification x :: THF_quantification
x = case THF_quantification
x of
THF_quantification q :: THF_quantifier
q vars :: [THF_variable]
vars ->
[Doc] -> Doc
hsep [THF_quantifier -> Doc
forall a. Pretty a => a -> Doc
pretty THF_quantifier
q, Doc -> Doc
brackets ([THF_variable] -> Doc
printTHF_variable_list [THF_variable]
vars) Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
colon]
printTHF_variable_list :: THF_variable_list -> Doc
printTHF_variable_list :: [THF_variable] -> Doc
printTHF_variable_list vars :: [THF_variable]
vars = [Doc] -> Doc
sepByCommas ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ (THF_variable -> Doc) -> [THF_variable] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map THF_variable -> Doc
forall a. Pretty a => a -> Doc
pretty [THF_variable]
vars
printTHF_variable :: THF_variable -> Doc
printTHF_variable :: THF_variable -> Doc
printTHF_variable x :: THF_variable
x = case THF_variable
x of
THFV_typed a :: THF_typed_variable
a -> THF_typed_variable -> Doc
forall a. Pretty a => a -> Doc
pretty THF_typed_variable
a
THFV_variable a :: Token
a -> Token -> Doc
forall a. Pretty a => a -> Doc
pretty Token
a
printTHF_typed_variable :: THF_typed_variable -> Doc
printTHF_typed_variable :: THF_typed_variable -> Doc
printTHF_typed_variable x :: THF_typed_variable
x = case THF_typed_variable
x of
THF_typed_variable v :: Token
v tlt :: THF_top_level_type
tlt -> [Doc] -> Doc
fsep [Token -> Doc
forall a. Pretty a => a -> Doc
pretty Token
v Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
colon, THF_top_level_type -> Doc
forall a. Pretty a => a -> Doc
pretty THF_top_level_type
tlt]
printTHF_unary_formula :: THF_unary_formula -> Doc
printTHF_unary_formula :: THF_unary_formula -> Doc
printTHF_unary_formula x :: THF_unary_formula
x = case THF_unary_formula
x of
THF_unary_formula c :: THF_unary_connective
c f :: THF_logic_formula
f -> THF_unary_connective -> Doc
forall a. Pretty a => a -> Doc
pretty THF_unary_connective
c Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc -> Doc
parens (THF_logic_formula -> Doc
forall a. Pretty a => a -> Doc
pretty THF_logic_formula
f)
printTHF_atom :: THF_atom -> Doc
printTHF_atom :: THF_atom -> Doc
printTHF_atom x :: THF_atom
x = case THF_atom
x of
THF_atom_function a :: THF_function
a -> THF_function -> Doc
forall a. Pretty a => a -> Doc
pretty THF_function
a
THF_atom_variable a :: Token
a -> Token -> Doc
forall a. Pretty a => a -> Doc
pretty Token
a
THF_atom_defined a :: Defined_term
a -> Defined_term -> Doc
forall a. Pretty a => a -> Doc
pretty Defined_term
a
THF_atom_conn a :: THF_conn_term
a -> THF_conn_term -> Doc
forall a. Pretty a => a -> Doc
pretty THF_conn_term
a
printTHF_function :: THF_function -> Doc
printTHF_function :: THF_function -> Doc
printTHF_function x :: THF_function
x = case THF_function
x of
THFF_atom a :: Atom
a -> Atom -> Doc
forall a. Pretty a => a -> Doc
pretty Atom
a
THFF_functor f :: Token
f args :: [THF_logic_formula]
args -> Token -> Doc
forall a. Pretty a => a -> Doc
pretty Token
f Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc -> Doc
parens ([THF_logic_formula] -> Doc
printTHF_arguments [THF_logic_formula]
args)
THFF_defined f :: Defined_functor
f args :: [THF_logic_formula]
args -> Defined_functor -> Doc
forall a. Pretty a => a -> Doc
pretty Defined_functor
f Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc -> Doc
parens ([THF_logic_formula] -> Doc
printTHF_arguments [THF_logic_formula]
args)
THFF_system f :: Token
f args :: [THF_logic_formula]
args -> Token -> Doc
forall a. Pretty a => a -> Doc
pretty Token
f Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc -> Doc
parens ([THF_logic_formula] -> Doc
printTHF_arguments [THF_logic_formula]
args)
printTHF_conn_term :: THF_conn_term -> Doc
printTHF_conn_term :: THF_conn_term -> Doc
printTHF_conn_term x :: THF_conn_term
x = case THF_conn_term
x of
THFC_pair a :: THF_pair_connective
a -> THF_pair_connective -> Doc
forall a. Pretty a => a -> Doc
pretty THF_pair_connective
a
THFC_assoc a :: Assoc_connective
a -> Assoc_connective -> Doc
forall a. Pretty a => a -> Doc
pretty Assoc_connective
a
THFC_unary a :: THF_unary_connective
a -> THF_unary_connective -> Doc
forall a. Pretty a => a -> Doc
pretty THF_unary_connective
a
printTHF_conditional :: THF_conditional -> Doc
printTHF_conditional :: THF_conditional -> Doc
printTHF_conditional x :: THF_conditional
x = case THF_conditional
x of
THF_conditional f_if :: THF_logic_formula
f_if f_then :: THF_logic_formula
f_then f_else :: THF_logic_formula
f_else ->
String -> Doc
text "$ite"
Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc -> Doc
parens ([Doc] -> Doc
sepByCommas [THF_logic_formula -> Doc
forall a. Pretty a => a -> Doc
pretty THF_logic_formula
f_if, THF_logic_formula -> Doc
forall a. Pretty a => a -> Doc
pretty THF_logic_formula
f_then, THF_logic_formula -> Doc
forall a. Pretty a => a -> Doc
pretty THF_logic_formula
f_else])
printTHF_let :: THF_let -> Doc
printTHF_let :: THF_let -> Doc
printTHF_let x :: THF_let
x = case THF_let
x of
THF_let defns :: THF_let_defns
defns f :: THF_formula
f ->
String -> Doc
text "$let" Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc -> Doc
parens ([Doc] -> Doc
sepByCommas [THF_let_defns -> Doc
forall a. Pretty a => a -> Doc
pretty THF_let_defns
defns, THF_formula -> Doc
forall a. Pretty a => a -> Doc
pretty THF_formula
f])
printTHF_let_defns :: THF_let_defns -> Doc
printTHF_let_defns :: THF_let_defns -> Doc
printTHF_let_defns x :: THF_let_defns
x = case THF_let_defns
x of
THFLD_single a :: THF_let_defn
a -> THF_let_defn -> Doc
forall a. Pretty a => a -> Doc
pretty THF_let_defn
a
THFLD_many a :: [THF_let_defn]
a -> Doc -> Doc
brackets (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [THF_let_defn] -> Doc
printTHF_let_defn_list [THF_let_defn]
a
printTHF_let_defn_list :: THF_let_defn_list -> Doc
printTHF_let_defn_list :: [THF_let_defn] -> Doc
printTHF_let_defn_list = [Doc] -> Doc
sepByCommas ([Doc] -> Doc)
-> ([THF_let_defn] -> [Doc]) -> [THF_let_defn] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (THF_let_defn -> Doc) -> [THF_let_defn] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map THF_let_defn -> Doc
forall a. Pretty a => a -> Doc
pretty
printTHF_let_defn :: THF_let_defn -> Doc
printTHF_let_defn :: THF_let_defn -> Doc
printTHF_let_defn x :: THF_let_defn
x = case THF_let_defn
x of
THFLD_quantified a :: THF_let_quantified_defn
a -> THF_let_quantified_defn -> Doc
forall a. Pretty a => a -> Doc
pretty THF_let_quantified_defn
a
THFLD_plain a :: THF_let_plain_defn
a -> THF_let_plain_defn -> Doc
forall a. Pretty a => a -> Doc
pretty THF_let_plain_defn
a
printTHF_let_quantified_defn :: THF_let_quantified_defn -> Doc
printTHF_let_quantified_defn :: THF_let_quantified_defn -> Doc
printTHF_let_quantified_defn x :: THF_let_quantified_defn
x = case THF_let_quantified_defn
x of
THF_let_quantified_defn q :: THF_quantification
q lpd :: THF_let_plain_defn
lpd ->
THF_quantification -> Doc
forall a. Pretty a => a -> Doc
pretty THF_quantification
q Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc -> Doc
parens (THF_let_plain_defn -> Doc
forall a. Pretty a => a -> Doc
pretty THF_let_plain_defn
lpd)
printTHF_let_plain_defn :: THF_let_plain_defn -> Doc
printTHF_let_plain_defn :: THF_let_plain_defn -> Doc
printTHF_let_plain_defn x :: THF_let_plain_defn
x = case THF_let_plain_defn
x of
THF_let_plain_defn lhs :: THF_let_defn_LHS
lhs f :: THF_formula
f -> [Doc] -> Doc
fsep [THF_let_defn_LHS -> Doc
forall a. Pretty a => a -> Doc
pretty THF_let_defn_LHS
lhs, Doc
assignment, THF_formula -> Doc
forall a. Pretty a => a -> Doc
pretty THF_formula
f]
printTHF_let_defn_LHS :: THF_let_defn_LHS -> Doc
printTHF_let_defn_LHS :: THF_let_defn_LHS -> Doc
printTHF_let_defn_LHS x :: THF_let_defn_LHS
x = case THF_let_defn_LHS
x of
THFLDL_constant a :: Token
a -> Token -> Doc
forall a. Pretty a => a -> Doc
pretty Token
a
THFLDL_functor f :: Token
f args :: [FOF_term]
args -> Token -> Doc
forall a. Pretty a => a -> Doc
pretty Token
f Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc -> Doc
parens ([FOF_term] -> Doc
printFOF_arguments [FOF_term]
args)
THFLDL_tuple a :: THF_tuple
a -> THF_tuple -> Doc
forall a. Pretty a => a -> Doc
pretty THF_tuple
a
printTHF_arguments :: THF_arguments -> Doc
printTHF_arguments :: [THF_logic_formula] -> Doc
printTHF_arguments x :: [THF_logic_formula]
x = [THF_logic_formula] -> Doc
printTHF_formula_list [THF_logic_formula]
x
printTHF_type_formula :: THF_type_formula -> Doc
printTHF_type_formula :: THF_type_formula -> Doc
printTHF_type_formula x :: THF_type_formula
x = case THF_type_formula
x of
THFTF_typeable f :: THF_typeable_formula
f tlt :: THF_top_level_type
tlt -> [Doc] -> Doc
fsep [THF_typeable_formula -> Doc
forall a. Pretty a => a -> Doc
pretty THF_typeable_formula
f Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
colon, THF_top_level_type -> Doc
forall a. Pretty a => a -> Doc
pretty THF_top_level_type
tlt]
THFTF_constant c :: Token
c tlt :: THF_top_level_type
tlt -> [Doc] -> Doc
fsep [Token -> Doc
forall a. Pretty a => a -> Doc
pretty Token
c Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
colon, THF_top_level_type -> Doc
forall a. Pretty a => a -> Doc
pretty THF_top_level_type
tlt]
printTHF_typeable_formula :: THF_typeable_formula -> Doc
printTHF_typeable_formula :: THF_typeable_formula -> Doc
printTHF_typeable_formula x :: THF_typeable_formula
x = case THF_typeable_formula
x of
THFTF_atom a :: THF_atom
a -> THF_atom -> Doc
forall a. Pretty a => a -> Doc
pretty THF_atom
a
THFTF_logic a :: THF_logic_formula
a -> Doc -> Doc
parens (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ THF_logic_formula -> Doc
forall a. Pretty a => a -> Doc
pretty THF_logic_formula
a
printTHF_subtype :: THF_subtype -> Doc
printTHF_subtype :: THF_subtype -> Doc
printTHF_subtype x :: THF_subtype
x = case THF_subtype
x of
THF_subtype a1 :: THF_atom
a1 a2 :: THF_atom
a2 -> [Doc] -> Doc
fsep [THF_atom -> Doc
forall a. Pretty a => a -> Doc
pretty THF_atom
a1, Doc
subtype_sign, THF_atom -> Doc
forall a. Pretty a => a -> Doc
pretty THF_atom
a2]
printTHF_top_level_type :: THF_top_level_type -> Doc
printTHF_top_level_type :: THF_top_level_type -> Doc
printTHF_top_level_type x :: THF_top_level_type
x = case THF_top_level_type
x of
THFTLT_unitary a :: THF_unitary_type
a -> THF_unitary_type -> Doc
forall a. Pretty a => a -> Doc
pretty THF_unitary_type
a
THFTLT_mapping a :: [THF_unitary_type]
a -> [THF_unitary_type] -> Doc
printTHF_mapping_type [THF_unitary_type]
a
printTHF_unitary_type :: THF_unitary_type -> Doc
printTHF_unitary_type :: THF_unitary_type -> Doc
printTHF_unitary_type x :: THF_unitary_type
x = case THF_unitary_type
x of
THFUT_unitary a :: THF_unitary_formula
a -> THF_unitary_formula -> Doc
forall a. Pretty a => a -> Doc
pretty THF_unitary_formula
a
THFUT_binary a :: THF_binary_type
a -> Doc -> Doc
parens (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ THF_binary_type -> Doc
forall a. Pretty a => a -> Doc
pretty THF_binary_type
a
printTHF_binary_type :: THF_binary_type -> Doc
printTHF_binary_type :: THF_binary_type -> Doc
printTHF_binary_type x :: THF_binary_type
x = case THF_binary_type
x of
THFBT_mapping a :: [THF_unitary_type]
a -> [THF_unitary_type] -> Doc
printTHF_mapping_type [THF_unitary_type]
a
THFBT_xprod a :: [THF_unitary_type]
a -> [THF_unitary_type] -> Doc
printTHF_xprod_type [THF_unitary_type]
a
THFBT_union a :: [THF_unitary_type]
a -> [THF_unitary_type] -> Doc
printTHF_union_type [THF_unitary_type]
a
printTHF_mapping_type :: THF_mapping_type -> Doc
printTHF_mapping_type :: [THF_unitary_type] -> Doc
printTHF_mapping_type = Doc -> [Doc] -> Doc
sepBy Doc
arrow ([Doc] -> Doc)
-> ([THF_unitary_type] -> [Doc]) -> [THF_unitary_type] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (THF_unitary_type -> Doc) -> [THF_unitary_type] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map THF_unitary_type -> Doc
forall a. Pretty a => a -> Doc
pretty
printTHF_xprod_type :: THF_xprod_type -> Doc
printTHF_xprod_type :: [THF_unitary_type] -> Doc
printTHF_xprod_type = Doc -> [Doc] -> Doc
sepBy Doc
star ([Doc] -> Doc)
-> ([THF_unitary_type] -> [Doc]) -> [THF_unitary_type] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (THF_unitary_type -> Doc) -> [THF_unitary_type] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map THF_unitary_type -> Doc
forall a. Pretty a => a -> Doc
pretty
printTHF_union_type :: THF_union_type -> Doc
printTHF_union_type :: [THF_unitary_type] -> Doc
printTHF_union_type = Doc -> [Doc] -> Doc
sepBy Doc
plus ([Doc] -> Doc)
-> ([THF_unitary_type] -> [Doc]) -> [THF_unitary_type] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (THF_unitary_type -> Doc) -> [THF_unitary_type] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map THF_unitary_type -> Doc
forall a. Pretty a => a -> Doc
pretty
printTHF_sequent :: THF_sequent -> Doc
printTHF_sequent :: THF_sequent -> Doc
printTHF_sequent x :: THF_sequent
x = case THF_sequent
x of
THFS_plain t1 :: THF_tuple
t1 t2 :: THF_tuple
t2 -> Doc -> [Doc] -> Doc
sepBy Doc
gentzen_arrow [THF_tuple -> Doc
forall a. Pretty a => a -> Doc
pretty THF_tuple
t1, THF_tuple -> Doc
forall a. Pretty a => a -> Doc
pretty THF_tuple
t2]
THFS_parens a :: THF_sequent
a -> Doc -> Doc
parens (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ THF_sequent -> Doc
forall a. Pretty a => a -> Doc
pretty THF_sequent
a
printTHF_tuple :: THF_tuple -> Doc
printTHF_tuple :: THF_tuple -> Doc
printTHF_tuple x :: THF_tuple
x = case THF_tuple
x of
THF_tuple a :: [THF_logic_formula]
a -> Doc -> Doc
brackets (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [THF_logic_formula] -> Doc
printTHF_formula_list [THF_logic_formula]
a
printTHF_formula_list :: THF_formula_list -> Doc
printTHF_formula_list :: [THF_logic_formula] -> Doc
printTHF_formula_list = [Doc] -> Doc
sepByCommas ([Doc] -> Doc)
-> ([THF_logic_formula] -> [Doc]) -> [THF_logic_formula] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (THF_logic_formula -> Doc) -> [THF_logic_formula] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map THF_logic_formula -> Doc
forall a. Pretty a => a -> Doc
pretty
printTFX_formula :: TFX_formula -> Doc
printTFX_formula :: TFX_formula -> Doc
printTFX_formula x :: TFX_formula
x = case TFX_formula
x of
TFXF_logic a :: TFX_logic_formula
a -> TFX_logic_formula -> Doc
forall a. Pretty a => a -> Doc
pretty TFX_logic_formula
a
TFXF_sequent a :: THF_sequent
a -> THF_sequent -> Doc
forall a. Pretty a => a -> Doc
pretty THF_sequent
a
printTFX_logic_formula :: TFX_logic_formula -> Doc
printTFX_logic_formula :: TFX_logic_formula -> Doc
printTFX_logic_formula x :: TFX_logic_formula
x = case TFX_logic_formula
x of
TFXLF_binary a :: THF_binary_formula
a -> THF_binary_formula -> Doc
forall a. Pretty a => a -> Doc
pretty THF_binary_formula
a
TFXLF_unitary a :: THF_unitary_formula
a -> THF_unitary_formula -> Doc
forall a. Pretty a => a -> Doc
pretty THF_unitary_formula
a
TFXLF_typed a :: TFF_typed_atom
a -> TFF_typed_atom -> Doc
forall a. Pretty a => a -> Doc
pretty TFF_typed_atom
a
TFXLF_subtype a :: TFF_subtype
a -> TFF_subtype -> Doc
forall a. Pretty a => a -> Doc
pretty TFF_subtype
a
printTFF_formula :: TFF_formula -> Doc
printTFF_formula :: TFF_formula -> Doc
printTFF_formula x :: TFF_formula
x = case TFF_formula
x of
TFFF_logic a :: TFF_logic_formula
a -> TFF_logic_formula -> Doc
forall a. Pretty a => a -> Doc
pretty TFF_logic_formula
a
TFFF_atom a :: TFF_typed_atom
a -> TFF_typed_atom -> Doc
forall a. Pretty a => a -> Doc
pretty TFF_typed_atom
a
TFFF_sequent a :: TFF_sequent
a -> TFF_sequent -> Doc
forall a. Pretty a => a -> Doc
pretty TFF_sequent
a
printTFF_logic_formula :: TFF_logic_formula -> Doc
printTFF_logic_formula :: TFF_logic_formula -> Doc
printTFF_logic_formula x :: TFF_logic_formula
x = case TFF_logic_formula
x of
TFFLF_binary a :: TFF_binary_formula
a -> TFF_binary_formula -> Doc
forall a. Pretty a => a -> Doc
pretty TFF_binary_formula
a
TFFLF_unitary a :: TFF_unitary_formula
a -> TFF_unitary_formula -> Doc
forall a. Pretty a => a -> Doc
pretty TFF_unitary_formula
a
TFFLF_subtype a :: TFF_subtype
a -> TFF_subtype -> Doc
forall a. Pretty a => a -> Doc
pretty TFF_subtype
a
printTFF_binary_formula :: TFF_binary_formula -> Doc
printTFF_binary_formula :: TFF_binary_formula -> Doc
printTFF_binary_formula x :: TFF_binary_formula
x = case TFF_binary_formula
x of
TFFBF_nonassoc a :: TFF_binary_nonassoc
a -> TFF_binary_nonassoc -> Doc
forall a. Pretty a => a -> Doc
pretty TFF_binary_nonassoc
a
TFFBF_assoc a :: TFF_binary_assoc
a -> TFF_binary_assoc -> Doc
forall a. Pretty a => a -> Doc
pretty TFF_binary_assoc
a
printTFF_binary_nonassoc :: TFF_binary_nonassoc -> Doc
printTFF_binary_nonassoc :: TFF_binary_nonassoc -> Doc
printTFF_binary_nonassoc x :: TFF_binary_nonassoc
x = case TFF_binary_nonassoc
x of
TFF_binary_nonassoc c :: Binary_connective
c f1 :: TFF_unitary_formula
f1 f2 :: TFF_unitary_formula
f2 -> [Doc] -> Doc
fsep [TFF_unitary_formula -> Doc
forall a. Pretty a => a -> Doc
pretty TFF_unitary_formula
f1, Binary_connective -> Doc
forall a. Pretty a => a -> Doc
pretty Binary_connective
c, TFF_unitary_formula -> Doc
forall a. Pretty a => a -> Doc
pretty TFF_unitary_formula
f2]
printTFF_binary_assoc :: TFF_binary_assoc -> Doc
printTFF_binary_assoc :: TFF_binary_assoc -> Doc
printTFF_binary_assoc x :: TFF_binary_assoc
x = case TFF_binary_assoc
x of
TFFBA_or a :: [TFF_unitary_formula]
a -> [TFF_unitary_formula] -> Doc
printTFF_or_formula [TFF_unitary_formula]
a
TFFBA_and a :: [TFF_unitary_formula]
a -> [TFF_unitary_formula] -> Doc
printTFF_and_formula [TFF_unitary_formula]
a
printTFF_or_formula :: TFF_or_formula -> Doc
printTFF_or_formula :: [TFF_unitary_formula] -> Doc
printTFF_or_formula = Doc -> [Doc] -> Doc
sepBy Doc
vline ([Doc] -> Doc)
-> ([TFF_unitary_formula] -> [Doc]) -> [TFF_unitary_formula] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TFF_unitary_formula -> Doc) -> [TFF_unitary_formula] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map TFF_unitary_formula -> Doc
forall a. Pretty a => a -> Doc
pretty
printTFF_and_formula :: TFF_and_formula -> Doc
printTFF_and_formula :: [TFF_unitary_formula] -> Doc
printTFF_and_formula = Doc -> [Doc] -> Doc
sepBy Doc
andD ([Doc] -> Doc)
-> ([TFF_unitary_formula] -> [Doc]) -> [TFF_unitary_formula] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TFF_unitary_formula -> Doc) -> [TFF_unitary_formula] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map TFF_unitary_formula -> Doc
forall a. Pretty a => a -> Doc
pretty
printTFF_unitary_formula :: TFF_unitary_formula -> Doc
printTFF_unitary_formula :: TFF_unitary_formula -> Doc
printTFF_unitary_formula x :: TFF_unitary_formula
x = case TFF_unitary_formula
x of
TFFUF_quantified a :: TFF_quantified_formula
a -> TFF_quantified_formula -> Doc
forall a. Pretty a => a -> Doc
pretty TFF_quantified_formula
a
TFFUF_unary a :: TFF_unary_formula
a -> TFF_unary_formula -> Doc
forall a. Pretty a => a -> Doc
pretty TFF_unary_formula
a
TFFUF_atomic a :: FOF_atomic_formula
a -> FOF_atomic_formula -> Doc
forall a. Pretty a => a -> Doc
pretty FOF_atomic_formula
a
TFFUF_conditional a :: TFF_conditional
a -> TFF_conditional -> Doc
forall a. Pretty a => a -> Doc
pretty TFF_conditional
a
TFFUF_let a :: TFF_let
a -> TFF_let -> Doc
forall a. Pretty a => a -> Doc
pretty TFF_let
a
TFFUF_logic a :: TFF_logic_formula
a -> Doc -> Doc
parens (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ TFF_logic_formula -> Doc
forall a. Pretty a => a -> Doc
pretty TFF_logic_formula
a
printTFF_quantified_formula :: TFF_quantified_formula -> Doc
printTFF_quantified_formula :: TFF_quantified_formula -> Doc
printTFF_quantified_formula x :: TFF_quantified_formula
x = case TFF_quantified_formula
x of
TFF_quantified_formula q :: FOF_quantifier
q vars :: [TFF_variable]
vars f :: TFF_unitary_formula
f ->
[Doc] -> Doc
hsep [FOF_quantifier -> Doc
forall a. Pretty a => a -> Doc
pretty FOF_quantifier
q, Doc -> Doc
brackets ([TFF_variable] -> Doc
printTFF_variable_list [TFF_variable]
vars) Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
colon, TFF_unitary_formula -> Doc
forall a. Pretty a => a -> Doc
pretty TFF_unitary_formula
f]
printTFF_variable_list :: TFF_variable_list -> Doc
printTFF_variable_list :: [TFF_variable] -> Doc
printTFF_variable_list = [Doc] -> Doc
sepByCommas ([Doc] -> Doc)
-> ([TFF_variable] -> [Doc]) -> [TFF_variable] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TFF_variable -> Doc) -> [TFF_variable] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map TFF_variable -> Doc
forall a. Pretty a => a -> Doc
pretty
printTFF_variable :: TFF_variable -> Doc
printTFF_variable :: TFF_variable -> Doc
printTFF_variable x :: TFF_variable
x = case TFF_variable
x of
TFFV_typed a :: TFF_typed_variable
a -> TFF_typed_variable -> Doc
forall a. Pretty a => a -> Doc
pretty TFF_typed_variable
a
TFFV_variable a :: Token
a -> Token -> Doc
forall a. Pretty a => a -> Doc
pretty Token
a
printTFF_typed_variable :: TFF_typed_variable -> Doc
printTFF_typed_variable :: TFF_typed_variable -> Doc
printTFF_typed_variable x :: TFF_typed_variable
x = case TFF_typed_variable
x of
TFF_typed_variable v :: Token
v t :: TFF_atomic_type
t -> [Doc] -> Doc
fsep [Token -> Doc
forall a. Pretty a => a -> Doc
pretty Token
v Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
colon, TFF_atomic_type -> Doc
forall a. Pretty a => a -> Doc
pretty TFF_atomic_type
t]
printTFF_unary_formula :: TFF_unary_formula -> Doc
printTFF_unary_formula :: TFF_unary_formula -> Doc
printTFF_unary_formula x :: TFF_unary_formula
x = case TFF_unary_formula
x of
TFFUF_connective c :: Unary_connective
c f :: TFF_unitary_formula
f -> [Doc] -> Doc
fsep [Unary_connective -> Doc
forall a. Pretty a => a -> Doc
pretty Unary_connective
c, TFF_unitary_formula -> Doc
forall a. Pretty a => a -> Doc
pretty TFF_unitary_formula
f]
TFFUF_infix a :: FOF_infix_unary
a -> FOF_infix_unary -> Doc
forall a. Pretty a => a -> Doc
pretty FOF_infix_unary
a
printTFF_conditional :: TFF_conditional -> Doc
printTFF_conditional :: TFF_conditional -> Doc
printTFF_conditional x :: TFF_conditional
x = case TFF_conditional
x of
TFF_conditional f_if :: TFF_logic_formula
f_if f_then :: TFF_logic_formula
f_then f_else :: TFF_logic_formula
f_else ->
String -> Doc
text "$ite_f"
Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc -> Doc
parens ([Doc] -> Doc
sepByCommas [TFF_logic_formula -> Doc
forall a. Pretty a => a -> Doc
pretty TFF_logic_formula
f_if, TFF_logic_formula -> Doc
forall a. Pretty a => a -> Doc
pretty TFF_logic_formula
f_then, TFF_logic_formula -> Doc
forall a. Pretty a => a -> Doc
pretty TFF_logic_formula
f_else])
printTFF_let :: TFF_let -> Doc
printTFF_let :: TFF_let -> Doc
printTFF_let x :: TFF_let
x = case TFF_let
x of
TFF_let_term_defns defns :: TFF_let_term_defns
defns f :: TFF_formula
f ->
String -> Doc
text "$let_tf"
Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc -> Doc
parens ([Doc] -> Doc
sepByCommas [TFF_let_term_defns -> Doc
forall a. Pretty a => a -> Doc
pretty TFF_let_term_defns
defns, TFF_formula -> Doc
forall a. Pretty a => a -> Doc
pretty TFF_formula
f])
TFF_let_formula_defns defns :: TFF_let_formula_defns
defns f :: TFF_formula
f ->
String -> Doc
text "$let_ff"
Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc -> Doc
parens ([Doc] -> Doc
sepByCommas [TFF_let_formula_defns -> Doc
forall a. Pretty a => a -> Doc
pretty TFF_let_formula_defns
defns, TFF_formula -> Doc
forall a. Pretty a => a -> Doc
pretty TFF_formula
f])
printTFF_let_term_defns :: TFF_let_term_defns -> Doc
printTFF_let_term_defns :: TFF_let_term_defns -> Doc
printTFF_let_term_defns x :: TFF_let_term_defns
x = case TFF_let_term_defns
x of
TFFLTD_single a :: TFF_let_term_defn
a -> TFF_let_term_defn -> Doc
forall a. Pretty a => a -> Doc
pretty TFF_let_term_defn
a
TFFLTD_many a :: [TFF_let_term_defn]
a -> Doc -> Doc
brackets (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [TFF_let_term_defn] -> Doc
printTFF_let_term_list [TFF_let_term_defn]
a
printTFF_let_term_list :: TFF_let_term_list -> Doc
printTFF_let_term_list :: [TFF_let_term_defn] -> Doc
printTFF_let_term_list = [Doc] -> Doc
sepByCommas ([Doc] -> Doc)
-> ([TFF_let_term_defn] -> [Doc]) -> [TFF_let_term_defn] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TFF_let_term_defn -> Doc) -> [TFF_let_term_defn] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map TFF_let_term_defn -> Doc
forall a. Pretty a => a -> Doc
pretty
printTFF_let_term_defn :: TFF_let_term_defn -> Doc
printTFF_let_term_defn :: TFF_let_term_defn -> Doc
printTFF_let_term_defn x :: TFF_let_term_defn
x = case TFF_let_term_defn
x of
TFFLTD_variable vars :: [TFF_variable]
vars defn :: TFF_let_term_defn
defn ->
[Doc] -> Doc
fsep [ String -> Doc
text "!"
, Doc -> Doc
brackets ([TFF_variable] -> Doc
printTFF_variable_list [TFF_variable]
vars) Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
colon
, TFF_let_term_defn -> Doc
forall a. Pretty a => a -> Doc
pretty TFF_let_term_defn
defn
]
TFFLTD_binding a :: TFF_let_term_binding
a -> TFF_let_term_binding -> Doc
forall a. Pretty a => a -> Doc
pretty TFF_let_term_binding
a
printTFF_let_term_binding :: TFF_let_term_binding -> Doc
printTFF_let_term_binding :: TFF_let_term_binding -> Doc
printTFF_let_term_binding x :: TFF_let_term_binding
x = case TFF_let_term_binding
x of
TFFLTB_plain pt :: FOF_plain_term
pt t :: FOF_term
t -> [Doc] -> Doc
fsep [FOF_plain_term -> Doc
forall a. Pretty a => a -> Doc
pretty FOF_plain_term
pt, String -> Doc
text "=" ,FOF_term -> Doc
forall a. Pretty a => a -> Doc
pretty FOF_term
t]
TFFLTB_binding a :: TFF_let_term_binding
a -> Doc -> Doc
parens (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ TFF_let_term_binding -> Doc
forall a. Pretty a => a -> Doc
pretty TFF_let_term_binding
a
printTFF_let_formula_defns :: TFF_let_formula_defns -> Doc
printTFF_let_formula_defns :: TFF_let_formula_defns -> Doc
printTFF_let_formula_defns x :: TFF_let_formula_defns
x = case TFF_let_formula_defns
x of
TFFLFD_single a :: TFF_let_formula_defn
a -> TFF_let_formula_defn -> Doc
forall a. Pretty a => a -> Doc
pretty TFF_let_formula_defn
a
TFFLFD_many a :: [TFF_let_formula_defn]
a -> Doc -> Doc
brackets (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [TFF_let_formula_defn] -> Doc
printTFF_let_formula_list [TFF_let_formula_defn]
a
printTFF_let_formula_list :: TFF_let_formula_list -> Doc
printTFF_let_formula_list :: [TFF_let_formula_defn] -> Doc
printTFF_let_formula_list = [Doc] -> Doc
sepByCommas ([Doc] -> Doc)
-> ([TFF_let_formula_defn] -> [Doc])
-> [TFF_let_formula_defn]
-> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TFF_let_formula_defn -> Doc) -> [TFF_let_formula_defn] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map TFF_let_formula_defn -> Doc
forall a. Pretty a => a -> Doc
pretty
printTFF_let_formula_defn :: TFF_let_formula_defn -> Doc
printTFF_let_formula_defn :: TFF_let_formula_defn -> Doc
printTFF_let_formula_defn x :: TFF_let_formula_defn
x = case TFF_let_formula_defn
x of
TFFLFD_variable vars :: [TFF_variable]
vars defn :: TFF_let_formula_defn
defn ->
[Doc] -> Doc
fsep [ String -> Doc
text "!"
, Doc -> Doc
brackets ([TFF_variable] -> Doc
printTFF_variable_list [TFF_variable]
vars) Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
colon
, TFF_let_formula_defn -> Doc
forall a. Pretty a => a -> Doc
pretty TFF_let_formula_defn
defn
]
TFFLFD_binding a :: TFF_let_formula_binding
a -> TFF_let_formula_binding -> Doc
forall a. Pretty a => a -> Doc
pretty TFF_let_formula_binding
a
printTFF_let_formula_binding :: TFF_let_formula_binding -> Doc
printTFF_let_formula_binding :: TFF_let_formula_binding -> Doc
printTFF_let_formula_binding x :: TFF_let_formula_binding
x = case TFF_let_formula_binding
x of
TFFLFB_plain paf :: FOF_plain_atomic_formula
paf uf :: TFF_unitary_formula
uf -> [Doc] -> Doc
fsep [FOF_plain_atomic_formula -> Doc
forall a. Pretty a => a -> Doc
pretty FOF_plain_atomic_formula
paf, TFF_unitary_formula -> Doc
forall a. Pretty a => a -> Doc
pretty TFF_unitary_formula
uf]
TFFLFB_binding a :: TFF_let_formula_binding
a -> Doc -> Doc
parens (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ TFF_let_formula_binding -> Doc
forall a. Pretty a => a -> Doc
pretty TFF_let_formula_binding
a
printTFF_sequent :: TFF_sequent -> Doc
printTFF_sequent :: TFF_sequent -> Doc
printTFF_sequent x :: TFF_sequent
x = case TFF_sequent
x of
TFFS_plain t1 :: TFF_formula_tuple
t1 t2 :: TFF_formula_tuple
t2 -> Doc -> [Doc] -> Doc
sepBy Doc
gentzen_arrow [TFF_formula_tuple -> Doc
forall a. Pretty a => a -> Doc
pretty TFF_formula_tuple
t1, TFF_formula_tuple -> Doc
forall a. Pretty a => a -> Doc
pretty TFF_formula_tuple
t2]
TFFS_parens a :: TFF_sequent
a -> Doc -> Doc
parens (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ TFF_sequent -> Doc
forall a. Pretty a => a -> Doc
pretty TFF_sequent
a
printTFF_formula_tuple :: TFF_formula_tuple -> Doc
printTFF_formula_tuple :: TFF_formula_tuple -> Doc
printTFF_formula_tuple x :: TFF_formula_tuple
x = case TFF_formula_tuple
x of
TFF_formula_tuple a :: [TFF_logic_formula]
a -> Doc -> Doc
brackets (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [TFF_logic_formula] -> Doc
printTFF_formula_tuple_list [TFF_logic_formula]
a
printTFF_formula_tuple_list :: TFF_formula_tuple_list -> Doc
printTFF_formula_tuple_list :: [TFF_logic_formula] -> Doc
printTFF_formula_tuple_list = [Doc] -> Doc
sepByCommas ([Doc] -> Doc)
-> ([TFF_logic_formula] -> [Doc]) -> [TFF_logic_formula] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TFF_logic_formula -> Doc) -> [TFF_logic_formula] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map TFF_logic_formula -> Doc
forall a. Pretty a => a -> Doc
pretty
printTFF_typed_atom :: TFF_typed_atom -> Doc
printTFF_typed_atom :: TFF_typed_atom -> Doc
printTFF_typed_atom x :: TFF_typed_atom
x = case TFF_typed_atom
x of
TFFTA_plain ua :: Untyped_atom
ua tlt :: TFF_top_level_type
tlt -> [Doc] -> Doc
fsep [Untyped_atom -> Doc
forall a. Pretty a => a -> Doc
pretty Untyped_atom
ua Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
colon, TFF_top_level_type -> Doc
forall a. Pretty a => a -> Doc
pretty TFF_top_level_type
tlt]
TFFTA_parens a :: TFF_typed_atom
a -> Doc -> Doc
parens (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ TFF_typed_atom -> Doc
forall a. Pretty a => a -> Doc
pretty TFF_typed_atom
a
printTFF_subtype :: TFF_subtype -> Doc
printTFF_subtype :: TFF_subtype -> Doc
printTFF_subtype x :: TFF_subtype
x = case TFF_subtype
x of
TFF_subtype ua :: Untyped_atom
ua a :: Atom
a -> [Doc] -> Doc
fsep [Untyped_atom -> Doc
forall a. Pretty a => a -> Doc
pretty Untyped_atom
ua, Doc
subtype_sign, Atom -> Doc
forall a. Pretty a => a -> Doc
pretty Atom
a]
printTFF_top_level_type :: TFF_top_level_type -> Doc
printTFF_top_level_type :: TFF_top_level_type -> Doc
printTFF_top_level_type x :: TFF_top_level_type
x = case TFF_top_level_type
x of
TFFTLT_atomic a :: TFF_atomic_type
a -> TFF_atomic_type -> Doc
forall a. Pretty a => a -> Doc
pretty TFF_atomic_type
a
TFFTLT_mapping a :: TFF_mapping_type
a -> TFF_mapping_type -> Doc
forall a. Pretty a => a -> Doc
pretty TFF_mapping_type
a
TFFTLT_quantified a :: TF1_quantified_type
a -> TF1_quantified_type -> Doc
forall a. Pretty a => a -> Doc
pretty TF1_quantified_type
a
TFFTLT_parens a :: TFF_top_level_type
a -> Doc -> Doc
parens (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ TFF_top_level_type -> Doc
forall a. Pretty a => a -> Doc
pretty TFF_top_level_type
a
printTF1_quantified_type :: TF1_quantified_type -> Doc
printTF1_quantified_type :: TF1_quantified_type -> Doc
printTF1_quantified_type x :: TF1_quantified_type
x = case TF1_quantified_type
x of
TF1_quantified_type vars :: [TFF_variable]
vars t :: TFF_monotype
t ->
[Doc] -> Doc
fsep [ String -> Doc
text "!>"
, Doc -> Doc
brackets ([TFF_variable] -> Doc
printTFF_variable_list [TFF_variable]
vars) Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
colon
, TFF_monotype -> Doc
forall a. Pretty a => a -> Doc
pretty TFF_monotype
t
]
printTFF_monotype :: TFF_monotype -> Doc
printTFF_monotype :: TFF_monotype -> Doc
printTFF_monotype x :: TFF_monotype
x = case TFF_monotype
x of
TFFMT_atomic a :: TFF_atomic_type
a -> TFF_atomic_type -> Doc
forall a. Pretty a => a -> Doc
pretty TFF_atomic_type
a
TFFMT_mapping a :: TFF_mapping_type
a -> Doc -> Doc
parens (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ TFF_mapping_type -> Doc
forall a. Pretty a => a -> Doc
pretty TFF_mapping_type
a
printTFF_unitary_type :: TFF_unitary_type -> Doc
printTFF_unitary_type :: TFF_unitary_type -> Doc
printTFF_unitary_type x :: TFF_unitary_type
x = case TFF_unitary_type
x of
TFFUT_atomic a :: TFF_atomic_type
a -> TFF_atomic_type -> Doc
forall a. Pretty a => a -> Doc
pretty TFF_atomic_type
a
TFFUT_xprod a :: TFF_xprod_type
a -> Doc -> Doc
parens (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ TFF_xprod_type -> Doc
forall a. Pretty a => a -> Doc
pretty TFF_xprod_type
a
printTFF_atomic_type :: TFF_atomic_type -> Doc
printTFF_atomic_type :: TFF_atomic_type -> Doc
printTFF_atomic_type x :: TFF_atomic_type
x = case TFF_atomic_type
x of
TFFAT_constant a :: Token
a -> Token -> Doc
forall a. Pretty a => a -> Doc
pretty Token
a
TFFAT_defined a :: Defined_type
a -> Defined_type -> Doc
forall a. Pretty a => a -> Doc
pretty Defined_type
a
TFFAT_functor f :: Token
f args :: [TFF_atomic_type]
args -> Token -> Doc
forall a. Pretty a => a -> Doc
pretty Token
f Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc -> Doc
parens ([TFF_atomic_type] -> Doc
printTFF_type_arguments [TFF_atomic_type]
args)
TFFAT_variable a :: Token
a -> Token -> Doc
forall a. Pretty a => a -> Doc
pretty Token
a
printTFF_type_arguments :: TFF_type_arguments -> Doc
printTFF_type_arguments :: [TFF_atomic_type] -> Doc
printTFF_type_arguments = [Doc] -> Doc
sepByCommas ([Doc] -> Doc)
-> ([TFF_atomic_type] -> [Doc]) -> [TFF_atomic_type] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TFF_atomic_type -> Doc) -> [TFF_atomic_type] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map TFF_atomic_type -> Doc
forall a. Pretty a => a -> Doc
pretty
printTFF_mapping_type :: TFF_mapping_type -> Doc
printTFF_mapping_type :: TFF_mapping_type -> Doc
printTFF_mapping_type x :: TFF_mapping_type
x = case TFF_mapping_type
x of
TFF_mapping_type ut :: TFF_unitary_type
ut at :: TFF_atomic_type
at -> [Doc] -> Doc
fsep [TFF_unitary_type -> Doc
forall a. Pretty a => a -> Doc
pretty TFF_unitary_type
ut, Doc
arrow, TFF_atomic_type -> Doc
forall a. Pretty a => a -> Doc
pretty TFF_atomic_type
at]
printTFF_xprod_type :: TFF_xprod_type -> Doc
printTFF_xprod_type :: TFF_xprod_type -> Doc
printTFF_xprod_type x :: TFF_xprod_type
x = case TFF_xprod_type
x of
TFF_xprod_type ut :: TFF_unitary_type
ut ats :: [TFF_atomic_type]
ats -> Doc -> [Doc] -> Doc
sepBy Doc
star ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ TFF_unitary_type -> Doc
forall a. Pretty a => a -> Doc
pretty TFF_unitary_type
ut Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
: (TFF_atomic_type -> Doc) -> [TFF_atomic_type] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map TFF_atomic_type -> Doc
forall a. Pretty a => a -> Doc
pretty [TFF_atomic_type]
ats
printTCF_formula :: TCF_formula -> Doc
printTCF_formula :: TCF_formula -> Doc
printTCF_formula x :: TCF_formula
x = case TCF_formula
x of
TCFF_logic a :: TCF_logic_formula
a -> TCF_logic_formula -> Doc
forall a. Pretty a => a -> Doc
pretty TCF_logic_formula
a
TCFF_atom a :: TFF_typed_atom
a -> TFF_typed_atom -> Doc
forall a. Pretty a => a -> Doc
pretty TFF_typed_atom
a
printTCF_logic_formula :: TCF_logic_formula -> Doc
printTCF_logic_formula :: TCF_logic_formula -> Doc
printTCF_logic_formula x :: TCF_logic_formula
x = case TCF_logic_formula
x of
TCFLF_quantified a :: TCF_quantified_formula
a -> TCF_quantified_formula -> Doc
forall a. Pretty a => a -> Doc
pretty TCF_quantified_formula
a
TCFLF_cnf a :: CNF_formula
a -> CNF_formula -> Doc
forall a. Pretty a => a -> Doc
pretty CNF_formula
a
printTCF_quantified_formula :: TCF_quantified_formula -> Doc
printTCF_quantified_formula :: TCF_quantified_formula -> Doc
printTCF_quantified_formula x :: TCF_quantified_formula
x = case TCF_quantified_formula
x of
TCF_quantified vars :: [TFF_variable]
vars f :: CNF_formula
f ->
[Doc] -> Doc
fsep [ String -> Doc
text "!"
, Doc -> Doc
brackets ([TFF_variable] -> Doc
printTFF_variable_list [TFF_variable]
vars) Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
colon
, CNF_formula -> Doc
forall a. Pretty a => a -> Doc
pretty CNF_formula
f
]
printFOF_formula :: FOF_formula -> Doc
printFOF_formula :: FOF_formula -> Doc
printFOF_formula x :: FOF_formula
x = case FOF_formula
x of
FOFF_logic a :: FOF_logic_formula
a -> FOF_logic_formula -> Doc
forall a. Pretty a => a -> Doc
pretty FOF_logic_formula
a
FOFF_sequent a :: FOF_sequent
a -> FOF_sequent -> Doc
forall a. Pretty a => a -> Doc
pretty FOF_sequent
a
printFOF_logic_formula :: FOF_logic_formula -> Doc
printFOF_logic_formula :: FOF_logic_formula -> Doc
printFOF_logic_formula x :: FOF_logic_formula
x = case FOF_logic_formula
x of
FOFLF_binary a :: FOF_binary_formula
a -> FOF_binary_formula -> Doc
forall a. Pretty a => a -> Doc
pretty FOF_binary_formula
a
FOFLF_unitary a :: FOF_unitary_formula
a -> FOF_unitary_formula -> Doc
forall a. Pretty a => a -> Doc
pretty FOF_unitary_formula
a
printFOF_binary_formula :: FOF_binary_formula -> Doc
printFOF_binary_formula :: FOF_binary_formula -> Doc
printFOF_binary_formula x :: FOF_binary_formula
x = case FOF_binary_formula
x of
FOFBF_nonassoc a :: FOF_binary_nonassoc
a -> FOF_binary_nonassoc -> Doc
forall a. Pretty a => a -> Doc
pretty FOF_binary_nonassoc
a
FOFBF_assoc a :: FOF_binary_assoc
a -> FOF_binary_assoc -> Doc
forall a. Pretty a => a -> Doc
pretty FOF_binary_assoc
a
printFOF_binary_nonassoc :: FOF_binary_nonassoc -> Doc
printFOF_binary_nonassoc :: FOF_binary_nonassoc -> Doc
printFOF_binary_nonassoc x :: FOF_binary_nonassoc
x = case FOF_binary_nonassoc
x of
FOF_binary_nonassoc c :: Binary_connective
c f1 :: FOF_unitary_formula
f1 f2 :: FOF_unitary_formula
f2 ->
[Doc] -> Doc
fsep [FOF_unitary_formula -> Doc
forall a. Pretty a => a -> Doc
pretty FOF_unitary_formula
f1, Binary_connective -> Doc
forall a. Pretty a => a -> Doc
pretty Binary_connective
c, FOF_unitary_formula -> Doc
forall a. Pretty a => a -> Doc
pretty FOF_unitary_formula
f2]
printFOF_binary_assoc :: FOF_binary_assoc -> Doc
printFOF_binary_assoc :: FOF_binary_assoc -> Doc
printFOF_binary_assoc x :: FOF_binary_assoc
x = case FOF_binary_assoc
x of
FOFBA_or a :: [FOF_unitary_formula]
a -> [FOF_unitary_formula] -> Doc
printFOF_or_formula [FOF_unitary_formula]
a
FOFBA_and a :: [FOF_unitary_formula]
a -> [FOF_unitary_formula] -> Doc
printFOF_and_formula [FOF_unitary_formula]
a
printFOF_or_formula :: FOF_or_formula -> Doc
printFOF_or_formula :: [FOF_unitary_formula] -> Doc
printFOF_or_formula = Doc -> [Doc] -> Doc
sepBy Doc
vline ([Doc] -> Doc)
-> ([FOF_unitary_formula] -> [Doc]) -> [FOF_unitary_formula] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (FOF_unitary_formula -> Doc) -> [FOF_unitary_formula] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map FOF_unitary_formula -> Doc
forall a. Pretty a => a -> Doc
pretty
printFOF_and_formula :: FOF_and_formula -> Doc
printFOF_and_formula :: [FOF_unitary_formula] -> Doc
printFOF_and_formula = Doc -> [Doc] -> Doc
sepBy Doc
andD ([Doc] -> Doc)
-> ([FOF_unitary_formula] -> [Doc]) -> [FOF_unitary_formula] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (FOF_unitary_formula -> Doc) -> [FOF_unitary_formula] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map FOF_unitary_formula -> Doc
forall a. Pretty a => a -> Doc
pretty
printFOF_unitary_formula :: FOF_unitary_formula -> Doc
printFOF_unitary_formula :: FOF_unitary_formula -> Doc
printFOF_unitary_formula x :: FOF_unitary_formula
x = case FOF_unitary_formula
x of
FOFUF_quantified a :: FOF_quantified_formula
a -> FOF_quantified_formula -> Doc
forall a. Pretty a => a -> Doc
pretty FOF_quantified_formula
a
FOFUF_unary a :: FOF_unary_formula
a -> FOF_unary_formula -> Doc
forall a. Pretty a => a -> Doc
pretty FOF_unary_formula
a
FOFUF_atomic a :: FOF_atomic_formula
a -> FOF_atomic_formula -> Doc
forall a. Pretty a => a -> Doc
pretty FOF_atomic_formula
a
FOFUF_logic a :: FOF_logic_formula
a -> Doc -> Doc
parens (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ FOF_logic_formula -> Doc
forall a. Pretty a => a -> Doc
pretty FOF_logic_formula
a
printFOF_quantified_formula :: FOF_quantified_formula -> Doc
printFOF_quantified_formula :: FOF_quantified_formula -> Doc
printFOF_quantified_formula x :: FOF_quantified_formula
x = case FOF_quantified_formula
x of
FOF_quantified_formula q :: FOF_quantifier
q vars :: [Token]
vars f :: FOF_unitary_formula
f ->
[Doc] -> Doc
fsep [ FOF_quantifier -> Doc
forall a. Pretty a => a -> Doc
pretty FOF_quantifier
q
, Doc -> Doc
brackets ([Token] -> Doc
printFOF_variable_list [Token]
vars) Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
colon
, FOF_unitary_formula -> Doc
forall a. Pretty a => a -> Doc
pretty FOF_unitary_formula
f
]
printFOF_variable_list :: FOF_variable_list -> Doc
printFOF_variable_list :: [Token] -> Doc
printFOF_variable_list = [Doc] -> Doc
sepByCommas ([Doc] -> Doc) -> ([Token] -> [Doc]) -> [Token] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Token -> Doc) -> [Token] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Token -> Doc
forall a. Pretty a => a -> Doc
pretty
printFOF_unary_formula :: FOF_unary_formula -> Doc
printFOF_unary_formula :: FOF_unary_formula -> Doc
printFOF_unary_formula x :: FOF_unary_formula
x = case FOF_unary_formula
x of
FOFUF_connective c :: Unary_connective
c f :: FOF_unitary_formula
f -> [Doc] -> Doc
fsep [Unary_connective -> Doc
forall a. Pretty a => a -> Doc
pretty Unary_connective
c, FOF_unitary_formula -> Doc
forall a. Pretty a => a -> Doc
pretty FOF_unitary_formula
f]
FOFUF_infix a :: FOF_infix_unary
a -> FOF_infix_unary -> Doc
forall a. Pretty a => a -> Doc
pretty FOF_infix_unary
a
printFOF_infix_unary :: FOF_infix_unary -> Doc
printFOF_infix_unary :: FOF_infix_unary -> Doc
printFOF_infix_unary x :: FOF_infix_unary
x = case FOF_infix_unary
x of
FOF_infix_unary t1 :: FOF_term
t1 t2 :: FOF_term
t2 -> [Doc] -> Doc
fsep [FOF_term -> Doc
forall a. Pretty a => a -> Doc
pretty FOF_term
t1, Doc
infix_inequality, FOF_term -> Doc
forall a. Pretty a => a -> Doc
pretty FOF_term
t2]
printFOF_atomic_formula :: FOF_atomic_formula -> Doc
printFOF_atomic_formula :: FOF_atomic_formula -> Doc
printFOF_atomic_formula x :: FOF_atomic_formula
x = case FOF_atomic_formula
x of
FOFAT_plain a :: FOF_plain_atomic_formula
a -> FOF_plain_atomic_formula -> Doc
forall a. Pretty a => a -> Doc
pretty FOF_plain_atomic_formula
a
FOFAT_defined a :: FOF_defined_atomic_formula
a -> FOF_defined_atomic_formula -> Doc
forall a. Pretty a => a -> Doc
pretty FOF_defined_atomic_formula
a
FOFAT_system a :: FOF_system_atomic_formula
a -> FOF_system_atomic_formula -> Doc
forall a. Pretty a => a -> Doc
pretty FOF_system_atomic_formula
a
printFOF_plain_atomic_formula :: FOF_plain_atomic_formula -> Doc
printFOF_plain_atomic_formula :: FOF_plain_atomic_formula -> Doc
printFOF_plain_atomic_formula x :: FOF_plain_atomic_formula
x = case FOF_plain_atomic_formula
x of
FOFPAF_proposition a :: Token
a -> Token -> Doc
forall a. Pretty a => a -> Doc
pretty Token
a
FOFPAF_predicate p :: Token
p args :: [FOF_term]
args -> Token -> Doc
forall a. Pretty a => a -> Doc
pretty Token
p Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc -> Doc
parens ([FOF_term] -> Doc
printFOF_arguments [FOF_term]
args)
printFOF_defined_atomic_formula :: FOF_defined_atomic_formula -> Doc
printFOF_defined_atomic_formula :: FOF_defined_atomic_formula -> Doc
printFOF_defined_atomic_formula x :: FOF_defined_atomic_formula
x = case FOF_defined_atomic_formula
x of
FOFDAF_plain a :: FOF_defined_plain_formula
a -> FOF_defined_plain_formula -> Doc
forall a. Pretty a => a -> Doc
pretty FOF_defined_plain_formula
a
FOFDAF_infix a :: FOF_defined_infix_formula
a -> FOF_defined_infix_formula -> Doc
forall a. Pretty a => a -> Doc
pretty FOF_defined_infix_formula
a
printFOF_defined_plain_formula :: FOF_defined_plain_formula -> Doc
printFOF_defined_plain_formula :: FOF_defined_plain_formula -> Doc
printFOF_defined_plain_formula x :: FOF_defined_plain_formula
x = case FOF_defined_plain_formula
x of
FOFDPF_proposition a :: Defined_proposition
a -> Defined_proposition -> Doc
forall a. Pretty a => a -> Doc
pretty Defined_proposition
a
FOFDPF_predicate p :: Defined_predicate
p args :: [FOF_term]
args -> Defined_predicate -> Doc
forall a. Pretty a => a -> Doc
pretty Defined_predicate
p Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc -> Doc
parens ([FOF_term] -> Doc
printFOF_arguments [FOF_term]
args)
printFOF_defined_infix_formula :: FOF_defined_infix_formula -> Doc
printFOF_defined_infix_formula :: FOF_defined_infix_formula -> Doc
printFOF_defined_infix_formula x :: FOF_defined_infix_formula
x = case FOF_defined_infix_formula
x of
FOF_defined_infix_formula dip :: Defined_infix_pred
dip t1 :: FOF_term
t1 t2 :: FOF_term
t2 -> [Doc] -> Doc
fsep [FOF_term -> Doc
forall a. Pretty a => a -> Doc
pretty FOF_term
t1, Defined_infix_pred -> Doc
forall a. Pretty a => a -> Doc
pretty Defined_infix_pred
dip, FOF_term -> Doc
forall a. Pretty a => a -> Doc
pretty FOF_term
t2]
printFOF_system_atomic_formula :: FOF_system_atomic_formula -> Doc
printFOF_system_atomic_formula :: FOF_system_atomic_formula -> Doc
printFOF_system_atomic_formula x :: FOF_system_atomic_formula
x = case FOF_system_atomic_formula
x of
FOF_system_atomic_formula a :: FOF_system_term
a -> FOF_system_term -> Doc
forall a. Pretty a => a -> Doc
pretty FOF_system_term
a
printFOF_plain_term :: FOF_plain_term -> Doc
printFOF_plain_term :: FOF_plain_term -> Doc
printFOF_plain_term x :: FOF_plain_term
x = case FOF_plain_term
x of
FOFPT_constant a :: Token
a -> Token -> Doc
forall a. Pretty a => a -> Doc
pretty Token
a
FOFPT_functor f :: Token
f args :: [FOF_term]
args -> Token -> Doc
forall a. Pretty a => a -> Doc
pretty Token
f Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc -> Doc
parens ([FOF_term] -> Doc
printFOF_arguments [FOF_term]
args)
printFOF_defined_term :: FOF_defined_term -> Doc
printFOF_defined_term :: FOF_defined_term -> Doc
printFOF_defined_term x :: FOF_defined_term
x = case FOF_defined_term
x of
FOFDT_term a :: Defined_term
a -> Defined_term -> Doc
forall a. Pretty a => a -> Doc
pretty Defined_term
a
FOFDT_atomic a :: FOF_defined_atomic_term
a -> FOF_defined_atomic_term -> Doc
forall a. Pretty a => a -> Doc
pretty FOF_defined_atomic_term
a
printFOF_defined_atomic_term :: FOF_defined_atomic_term -> Doc
printFOF_defined_atomic_term :: FOF_defined_atomic_term -> Doc
printFOF_defined_atomic_term x :: FOF_defined_atomic_term
x = case FOF_defined_atomic_term
x of
FOFDAT_plain a :: FOF_defined_plain_term
a -> FOF_defined_plain_term -> Doc
forall a. Pretty a => a -> Doc
pretty FOF_defined_plain_term
a
printFOF_defined_plain_term :: FOF_defined_plain_term -> Doc
printFOF_defined_plain_term :: FOF_defined_plain_term -> Doc
printFOF_defined_plain_term x :: FOF_defined_plain_term
x = case FOF_defined_plain_term
x of
FOFDPT_constant a :: Defined_functor
a -> Defined_functor -> Doc
forall a. Pretty a => a -> Doc
pretty Defined_functor
a
FOFDPT_functor f :: Defined_functor
f args :: [FOF_term]
args -> Defined_functor -> Doc
forall a. Pretty a => a -> Doc
pretty Defined_functor
f Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc -> Doc
parens ([FOF_term] -> Doc
printFOF_arguments [FOF_term]
args)
printFOF_system_term :: FOF_system_term -> Doc
printFOF_system_term :: FOF_system_term -> Doc
printFOF_system_term x :: FOF_system_term
x = case FOF_system_term
x of
FOFST_constant a :: Token
a -> Token -> Doc
forall a. Pretty a => a -> Doc
pretty Token
a
FOFST_functor f :: Token
f args :: [FOF_term]
args -> Token -> Doc
forall a. Pretty a => a -> Doc
pretty Token
f Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc -> Doc
parens ([FOF_term] -> Doc
printFOF_arguments [FOF_term]
args)
printFOF_arguments :: FOF_arguments -> Doc
printFOF_arguments :: [FOF_term] -> Doc
printFOF_arguments = [Doc] -> Doc
sepByCommas ([Doc] -> Doc) -> ([FOF_term] -> [Doc]) -> [FOF_term] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (FOF_term -> Doc) -> [FOF_term] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map FOF_term -> Doc
forall a. Pretty a => a -> Doc
pretty
printFOF_term :: FOF_term -> Doc
printFOF_term :: FOF_term -> Doc
printFOF_term x :: FOF_term
x = case FOF_term
x of
FOFT_function a :: FOF_function_term
a -> FOF_function_term -> Doc
forall a. Pretty a => a -> Doc
pretty FOF_function_term
a
FOFT_variable a :: Token
a -> Token -> Doc
forall a. Pretty a => a -> Doc
pretty Token
a
FOFT_conditional a :: TFF_conditional_term
a -> TFF_conditional_term -> Doc
forall a. Pretty a => a -> Doc
pretty TFF_conditional_term
a
FOFT_let a :: TFF_let_term
a -> TFF_let_term -> Doc
forall a. Pretty a => a -> Doc
pretty TFF_let_term
a
printFOF_function_term :: FOF_function_term -> Doc
printFOF_function_term :: FOF_function_term -> Doc
printFOF_function_term x :: FOF_function_term
x = case FOF_function_term
x of
FOFFT_plain a :: FOF_plain_term
a -> FOF_plain_term -> Doc
forall a. Pretty a => a -> Doc
pretty FOF_plain_term
a
FOFFT_defined a :: FOF_defined_term
a -> FOF_defined_term -> Doc
forall a. Pretty a => a -> Doc
pretty FOF_defined_term
a
FOFFT_system a :: FOF_system_term
a -> FOF_system_term -> Doc
forall a. Pretty a => a -> Doc
pretty FOF_system_term
a
printTFF_conditional_term :: TFF_conditional_term -> Doc
printTFF_conditional_term :: TFF_conditional_term -> Doc
printTFF_conditional_term x :: TFF_conditional_term
x = case TFF_conditional_term
x of
TFF_conditional_term f_if :: TFF_logic_formula
f_if t_then :: FOF_term
t_then t_else :: FOF_term
t_else ->
String -> Doc
text "$ite_t"
Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc -> Doc
parens ([Doc] -> Doc
sepByCommas [TFF_logic_formula -> Doc
forall a. Pretty a => a -> Doc
pretty TFF_logic_formula
f_if, FOF_term -> Doc
forall a. Pretty a => a -> Doc
pretty FOF_term
t_then, FOF_term -> Doc
forall a. Pretty a => a -> Doc
pretty FOF_term
t_else])
printTFF_let_term :: TFF_let_term -> Doc
printTFF_let_term :: TFF_let_term -> Doc
printTFF_let_term x :: TFF_let_term
x = case TFF_let_term
x of
TFFLT_formula defns :: TFF_let_formula_defns
defns t :: FOF_term
t ->
String -> Doc
text "$let_ft" Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc -> Doc
parens ([Doc] -> Doc
sepByCommas [TFF_let_formula_defns -> Doc
forall a. Pretty a => a -> Doc
pretty TFF_let_formula_defns
defns, FOF_term -> Doc
forall a. Pretty a => a -> Doc
pretty FOF_term
t])
TFFLT_term defns :: TFF_let_term_defns
defns t :: FOF_term
t ->
String -> Doc
text "$let_tt" Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc -> Doc
parens ([Doc] -> Doc
sepByCommas [TFF_let_term_defns -> Doc
forall a. Pretty a => a -> Doc
pretty TFF_let_term_defns
defns, FOF_term -> Doc
forall a. Pretty a => a -> Doc
pretty FOF_term
t])
printFOF_sequent :: FOF_sequent -> Doc
printFOF_sequent :: FOF_sequent -> Doc
printFOF_sequent x :: FOF_sequent
x = case FOF_sequent
x of
FOFS_plain t1 :: FOF_formula_tuple
t1 t2 :: FOF_formula_tuple
t2 -> [Doc] -> Doc
fsep [FOF_formula_tuple -> Doc
forall a. Pretty a => a -> Doc
pretty FOF_formula_tuple
t1, Doc
gentzen_arrow, FOF_formula_tuple -> Doc
forall a. Pretty a => a -> Doc
pretty FOF_formula_tuple
t2]
FOFS_parens a :: FOF_sequent
a -> Doc -> Doc
parens (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ FOF_sequent -> Doc
forall a. Pretty a => a -> Doc
pretty FOF_sequent
a
printFOF_formula_tuple :: FOF_formula_tuple -> Doc
printFOF_formula_tuple :: FOF_formula_tuple -> Doc
printFOF_formula_tuple x :: FOF_formula_tuple
x = case FOF_formula_tuple
x of
FOF_formula_tuple a :: [FOF_logic_formula]
a -> Doc -> Doc
brackets (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [FOF_logic_formula] -> Doc
printFOF_formula_tuple_list [FOF_logic_formula]
a
printFOF_formula_tuple_list :: FOF_formula_tuple_list -> Doc
printFOF_formula_tuple_list :: [FOF_logic_formula] -> Doc
printFOF_formula_tuple_list = [Doc] -> Doc
sepByCommas ([Doc] -> Doc)
-> ([FOF_logic_formula] -> [Doc]) -> [FOF_logic_formula] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (FOF_logic_formula -> Doc) -> [FOF_logic_formula] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map FOF_logic_formula -> Doc
forall a. Pretty a => a -> Doc
pretty
printCNF_formula :: CNF_formula -> Doc
printCNF_formula :: CNF_formula -> Doc
printCNF_formula x :: CNF_formula
x = case CNF_formula
x of
CNFF_plain a :: Disjunction
a -> Disjunction -> Doc
forall a. Pretty a => a -> Doc
pretty Disjunction
a
CNFF_parens a :: Disjunction
a -> Doc -> Doc
parens (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Disjunction -> Doc
forall a. Pretty a => a -> Doc
pretty Disjunction
a
printDisjunction :: Disjunction -> Doc
printDisjunction :: Disjunction -> Doc
printDisjunction x :: Disjunction
x = case Disjunction
x of
Disjunction ls :: [Literal]
ls -> Doc -> [Doc] -> Doc
sepBy Doc
vline ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ (Literal -> Doc) -> [Literal] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Literal -> Doc
forall a. Pretty a => a -> Doc
pretty [Literal]
ls
printLiteral :: Literal -> Doc
printLiteral :: Literal -> Doc
printLiteral x :: Literal
x = case Literal
x of
Lit_atomic a :: FOF_atomic_formula
a -> FOF_atomic_formula -> Doc
forall a. Pretty a => a -> Doc
pretty FOF_atomic_formula
a
Lit_negative a :: FOF_atomic_formula
a -> String -> Doc
text "~" Doc -> Doc -> Doc
<+> FOF_atomic_formula -> Doc
forall a. Pretty a => a -> Doc
pretty FOF_atomic_formula
a
Lit_fof_infix a :: FOF_infix_unary
a -> FOF_infix_unary -> Doc
forall a. Pretty a => a -> Doc
pretty FOF_infix_unary
a
printTHF_quantifier :: THF_quantifier -> Doc
printTHF_quantifier :: THF_quantifier -> Doc
printTHF_quantifier x :: THF_quantifier
x = case THF_quantifier
x of
THFQ_fof a :: FOF_quantifier
a -> FOF_quantifier -> Doc
forall a. Pretty a => a -> Doc
pretty FOF_quantifier
a
THFQ_th0 a :: TH0_quantifier
a -> TH0_quantifier -> Doc
forall a. Pretty a => a -> Doc
pretty TH0_quantifier
a
THFQ_th1 a :: TH1_quantifier
a -> TH1_quantifier -> Doc
forall a. Pretty a => a -> Doc
pretty TH1_quantifier
a
printTH1_quantifier :: TH1_quantifier -> Doc
printTH1_quantifier :: TH1_quantifier -> Doc
printTH1_quantifier x :: TH1_quantifier
x = case TH1_quantifier
x of
TH1_DependentProduct -> String -> Doc
text "!>"
TH1_DependentSum -> String -> Doc
text "?*"
printTH0_quantifier :: TH0_quantifier -> Doc
printTH0_quantifier :: TH0_quantifier -> Doc
printTH0_quantifier x :: TH0_quantifier
x = case TH0_quantifier
x of
TH0_LambdaBinder -> String -> Doc
text "^"
TH0_IndefiniteDescription -> String -> Doc
text "@+"
TH0_DefiniteDescription -> String -> Doc
text "@-"
printTHF_pair_connective :: THF_pair_connective -> Doc
printTHF_pair_connective :: THF_pair_connective -> Doc
printTHF_pair_connective x :: THF_pair_connective
x = case THF_pair_connective
x of
THF_infix_equality -> Doc
infix_equality
Infix_inequality -> Doc
infix_inequality
THFPC_binary a :: Binary_connective
a -> Binary_connective -> Doc
forall a. Pretty a => a -> Doc
pretty Binary_connective
a
THF_assignment -> Doc
assignment
printTHF_unary_connective :: THF_unary_connective -> Doc
printTHF_unary_connective :: THF_unary_connective -> Doc
printTHF_unary_connective x :: THF_unary_connective
x = case THF_unary_connective
x of
THFUC_unary a :: Unary_connective
a -> Unary_connective -> Doc
forall a. Pretty a => a -> Doc
pretty Unary_connective
a
THFUC_th1 a :: TH1_unary_connective
a -> TH1_unary_connective -> Doc
forall a. Pretty a => a -> Doc
pretty TH1_unary_connective
a
printTH1_unary_connective :: TH1_unary_connective -> Doc
printTH1_unary_connective :: TH1_unary_connective -> Doc
printTH1_unary_connective x :: TH1_unary_connective
x = case TH1_unary_connective
x of
TH1_PiForAll -> String -> Doc
text "!!"
TH1_PiSigmaExists -> String -> Doc
text "??"
TH1_PiIndefiniteDescription -> String -> Doc
text "@@+"
TH1_PiDefiniteDescription -> String -> Doc
text "@@-"
TH1_PiEquality -> String -> Doc
text "@="
subtype_sign :: Doc
subtype_sign :: Doc
subtype_sign = Doc
less_sign Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
less_sign
printFOF_quantifier :: FOF_quantifier -> Doc
printFOF_quantifier :: FOF_quantifier -> Doc
printFOF_quantifier x :: FOF_quantifier
x = case FOF_quantifier
x of
ForAll -> String -> Doc
text "!"
Exists -> String -> Doc
text "?"
printBinary_connective :: Binary_connective -> Doc
printBinary_connective :: Binary_connective -> Doc
printBinary_connective x :: Binary_connective
x = case Binary_connective
x of
Equivalence -> String -> Doc
text "<=>"
Implication -> String -> Doc
text "=>"
ReverseImplication -> String -> Doc
text "<="
XOR -> String -> Doc
text "<~>"
NOR -> String -> Doc
text "~|"
NAND -> String -> Doc
text "~&"
printAssoc_connective :: Assoc_connective -> Doc
printAssoc_connective :: Assoc_connective -> Doc
printAssoc_connective x :: Assoc_connective
x = case Assoc_connective
x of
OR -> String -> Doc
text "|"
AND -> String -> Doc
text "&"
printUnary_connective :: Unary_connective -> Doc
printUnary_connective :: Unary_connective -> Doc
printUnary_connective x :: Unary_connective
x = case Unary_connective
x of
NOT -> String -> Doc
text "~"
printDefined_type :: Defined_type -> Doc
printDefined_type :: Defined_type -> Doc
printDefined_type x :: Defined_type
x = case Defined_type
x of
OType -> String -> Doc
text "$oType"
O -> String -> Doc
text "$o"
IType -> String -> Doc
text "$iType"
I -> String -> Doc
text "$i"
TType -> String -> Doc
text "$tType"
Real -> String -> Doc
text "$real"
Rat -> String -> Doc
text "$rat"
Int -> String -> Doc
text "$int"
printAtom :: Atom -> Doc
printAtom :: Atom -> Doc
printAtom x :: Atom
x = case Atom
x of
Atom_untyped a :: Untyped_atom
a -> Untyped_atom -> Doc
forall a. Pretty a => a -> Doc
pretty Untyped_atom
a
Atom_constant a :: Defined_functor
a -> Defined_functor -> Doc
forall a. Pretty a => a -> Doc
pretty Defined_functor
a
printUntyped_atom :: Untyped_atom -> Doc
printUntyped_atom :: Untyped_atom -> Doc
printUntyped_atom x :: Untyped_atom
x = case Untyped_atom
x of
UA_constant a :: Token
a -> Token -> Doc
forall a. Pretty a => a -> Doc
pretty Token
a
UA_system a :: Token
a -> Token -> Doc
forall a. Pretty a => a -> Doc
pretty Token
a
printDefined_proposition :: Defined_proposition -> Doc
printDefined_proposition :: Defined_proposition -> Doc
printDefined_proposition x :: Defined_proposition
x = case Defined_proposition
x of
TPTP_true -> String -> Doc
text "$true"
TPTP_false -> String -> Doc
text "$false"
printDefined_predicate :: Defined_predicate -> Doc
printDefined_predicate :: Defined_predicate -> Doc
printDefined_predicate x :: Defined_predicate
x = case Defined_predicate
x of
Distinct -> String -> Doc
text "$distinct"
Less -> String -> Doc
text "$less"
Lesseq -> String -> Doc
text "$lesseq"
Greater -> String -> Doc
text "$greater"
Greatereq -> String -> Doc
text "$greatereq"
Is_int -> String -> Doc
text "$is_int"
Is_rat -> String -> Doc
text "$is_rat"
Box_P -> String -> Doc
text "$box_P"
Box_i -> String -> Doc
text "$box_i"
Box_int -> String -> Doc
text "$box_int"
Box -> String -> Doc
text "$box"
Dia_P -> String -> Doc
text "$dia_P"
Dia_i -> String -> Doc
text "$dia_i"
Dia_int -> String -> Doc
text "$dia_int"
Dia -> String -> Doc
text "$dia"
printDefined_infix_pred :: Defined_infix_pred -> Doc
printDefined_infix_pred :: Defined_infix_pred -> Doc
printDefined_infix_pred x :: Defined_infix_pred
x = case Defined_infix_pred
x of
Defined_infix_equality -> Doc
infix_equality
Defined_assignment -> Doc
assignment
printDefined_functor :: Defined_functor -> Doc
printDefined_functor :: Defined_functor -> Doc
printDefined_functor x :: Defined_functor
x = case Defined_functor
x of
Uminus -> String -> Doc
text "$uminus"
Sum -> String -> Doc
text "$sum"
Difference -> String -> Doc
text "$difference"
Product -> String -> Doc
text "$product"
Quotient -> String -> Doc
text "$quotient"
Quotient_e -> String -> Doc
text "$quotient_e"
Quotient_t -> String -> Doc
text "$quotient_t"
Quotient_f -> String -> Doc
text "$quotient_f"
Remainder_e -> String -> Doc
text "$remainder_e"
Remainder_t -> String -> Doc
text "$remainder_t"
Remainder_f -> String -> Doc
text "$remainder_f"
Floor -> String -> Doc
text "$floor"
Ceiling -> String -> Doc
text "$ceiling"
Truncate -> String -> Doc
text "$truncate"
Round -> String -> Doc
text "$round"
To_int -> String -> Doc
text "$to_int"
To_rat -> String -> Doc
text "$to_rat"
To_real -> String -> Doc
text "$to_real"
DF_atomic_defined_word a :: Token
a -> Token -> Doc
forall a. Pretty a => a -> Doc
pretty Token
a
printDefined_term :: Defined_term -> Doc
printDefined_term :: Defined_term -> Doc
printDefined_term x :: Defined_term
x = case Defined_term
x of
DT_number a :: Number
a -> Number -> Doc
forall a. Pretty a => a -> Doc
pretty Number
a
DT_object a :: Token
a -> Token -> Doc
forall a. Pretty a => a -> Doc
pretty Token
a
printSource :: Source -> Doc
printSource :: Source -> Doc
printSource x :: Source
x = case Source
x of
Source_DAG a :: DAG_source
a -> DAG_source -> Doc
forall a. Pretty a => a -> Doc
pretty DAG_source
a
Source_internal a :: Internal_source
a -> Internal_source -> Doc
forall a. Pretty a => a -> Doc
pretty Internal_source
a
Source_external a :: External_source
a -> External_source -> Doc
forall a. Pretty a => a -> Doc
pretty External_source
a
Unknown_source -> String -> Doc
text "unknown"
Source_many a :: [Source]
a -> Doc -> Doc
brackets (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Source] -> Doc
printSources [Source]
a
printSources :: Sources -> Doc
printSources :: [Source] -> Doc
printSources = [Doc] -> Doc
sepByCommas ([Doc] -> Doc) -> ([Source] -> [Doc]) -> [Source] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Source -> Doc) -> [Source] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Source -> Doc
forall a. Pretty a => a -> Doc
pretty
printDAG_source :: DAG_source -> Doc
printDAG_source :: DAG_source -> Doc
printDAG_source x :: DAG_source
x = case DAG_source
x of
DAGS_name a :: Name
a -> Name -> Doc
forall a. Pretty a => a -> Doc
pretty Name
a
DAGS_record a :: Inference_record
a -> Inference_record -> Doc
forall a. Pretty a => a -> Doc
pretty Inference_record
a
printInference_record :: Inference_record -> Doc
printInference_record :: Inference_record -> Doc
printInference_record x :: Inference_record
x = case Inference_record
x of
Inference_record ir :: Token
ir ui :: Useful_info
ui ip :: [Parent_info]
ip ->
String -> Doc
text "inference"
Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc -> Doc
parens ([Doc] -> Doc
sepByCommas [Token -> Doc
forall a. Pretty a => a -> Doc
pretty Token
ir, Useful_info -> Doc
forall a. Pretty a => a -> Doc
pretty Useful_info
ui, [Parent_info] -> Doc
printInference_parents [Parent_info]
ip])
printInference_rule :: Inference_rule -> Doc
printInference_rule :: Token -> Doc
printInference_rule = Token -> Doc
forall a. Pretty a => a -> Doc
pretty
printInference_parents :: Inference_parents -> Doc
printInference_parents :: [Parent_info] -> Doc
printInference_parents = Doc -> Doc
brackets (Doc -> Doc) -> ([Parent_info] -> Doc) -> [Parent_info] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Parent_info] -> Doc
printParent_list
printParent_list :: Parent_list -> Doc
printParent_list :: [Parent_info] -> Doc
printParent_list = [Doc] -> Doc
sepByCommas ([Doc] -> Doc) -> ([Parent_info] -> [Doc]) -> [Parent_info] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Parent_info -> Doc) -> [Parent_info] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Parent_info -> Doc
forall a. Pretty a => a -> Doc
pretty
printParent_info :: Parent_info -> Doc
printParent_info :: Parent_info -> Doc
printParent_info x :: Parent_info
x = case Parent_info
x of
Parent_info s :: Source
s d :: Parent_details
d -> [Doc] -> Doc
fsep [Source -> Doc
forall a. Pretty a => a -> Doc
pretty Source
s, Parent_details -> Doc
printParent_details Parent_details
d]
printParent_details :: Parent_details -> Doc
printParent_details :: Parent_details -> Doc
printParent_details x :: Parent_details
x = case Parent_details
x of
Just gl :: [General_term]
gl -> [General_term] -> Doc
printGeneral_list [General_term]
gl
Nothing -> Doc
empty
printInternal_source :: Internal_source -> Doc
printInternal_source :: Internal_source -> Doc
printInternal_source x :: Internal_source
x = case Internal_source
x of
Internal_source it :: Intro_type
it oi :: Optional_info
oi ->
String -> Doc
text "introduced" Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc -> Doc
parens ([Doc] -> Doc
fsep [Intro_type -> Doc
forall a. Pretty a => a -> Doc
pretty Intro_type
it, Optional_info -> Doc
forall a. Pretty a => a -> Doc
pretty Optional_info
oi])
printIntro_type :: Intro_type -> Doc
printIntro_type :: Intro_type -> Doc
printIntro_type x :: Intro_type
x = case Intro_type
x of
IntroTypeDefinition -> String -> Doc
text "definition"
AxiomOfChoice -> String -> Doc
text "axiom_of_choice"
Tautology -> String -> Doc
text "tautology"
IntroTypeAssumption -> String -> Doc
text "assumption"
printExternal_source :: External_source -> Doc
printExternal_source :: External_source -> Doc
printExternal_source x :: External_source
x = case External_source
x of
ExtSrc_file a :: File_source
a -> File_source -> Doc
forall a. Pretty a => a -> Doc
pretty File_source
a
ExtSrc_theory a :: Theory
a -> Theory -> Doc
forall a. Pretty a => a -> Doc
pretty Theory
a
ExtSrc_creator a :: Creator_source
a -> Creator_source -> Doc
forall a. Pretty a => a -> Doc
pretty Creator_source
a
printFile_source :: File_source -> Doc
printFile_source :: File_source -> Doc
printFile_source x :: File_source
x = case File_source
x of
File_source fn :: File_name
fn fi :: File_info
fi ->
String -> Doc
text "file" Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc -> Doc
parens ([Doc] -> Doc
fsep [String -> Doc
text "'" Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> File_name -> Doc
forall a. Pretty a => a -> Doc
pretty File_name
fn Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> String -> Doc
text "'",
File_info -> Doc
printFile_info File_info
fi])
printFile_info :: File_info -> Doc
printFile_info :: File_info -> Doc
printFile_info x :: File_info
x = case File_info
x of
Just n :: Name
n -> [Doc] -> Doc
fsep [Doc
comma, String -> Doc
text "'" Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Name -> Doc
forall a. Pretty a => a -> Doc
pretty Name
n Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> String -> Doc
text "'"]
Nothing -> Doc
empty
printTheory :: Theory -> Doc
printTheory :: Theory -> Doc
printTheory x :: Theory
x = case Theory
x of
Theory tn :: Theory_name
tn oi :: Optional_info
oi -> String -> Doc
text "theory" Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc -> Doc
parens ([Doc] -> Doc
fsep [Theory_name -> Doc
forall a. Pretty a => a -> Doc
pretty Theory_name
tn, Optional_info -> Doc
forall a. Pretty a => a -> Doc
pretty Optional_info
oi])
printTheory_name :: Theory_name -> Doc
printTheory_name :: Theory_name -> Doc
printTheory_name x :: Theory_name
x = case Theory_name
x of
TN_equality -> String -> Doc
text "equality"
TN_ac -> String -> Doc
text "ac"
printCreator_source :: Creator_source -> Doc
printCreator_source :: Creator_source -> Doc
printCreator_source x :: Creator_source
x = case Creator_source
x of
Creator_source cn :: Token
cn oi :: Optional_info
oi ->
String -> Doc
text "creator" Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc -> Doc
parens ([Doc] -> Doc
fsep [Token -> Doc
printCreator_name Token
cn, Optional_info -> Doc
forall a. Pretty a => a -> Doc
pretty Optional_info
oi])
printCreator_name :: Creator_name -> Doc
printCreator_name :: Token -> Doc
printCreator_name = Token -> Doc
forall a. Pretty a => a -> Doc
pretty
printOptional_info :: Optional_info -> Doc
printOptional_info :: Optional_info -> Doc
printOptional_info x :: Optional_info
x = case Optional_info
x of
Just ui :: Useful_info
ui -> Doc
comma Doc -> Doc -> Doc
<+> Useful_info -> Doc
forall a. Pretty a => a -> Doc
pretty Useful_info
ui
Nothing -> Doc
empty
printUseful_info :: Useful_info -> Doc
printUseful_info :: Useful_info -> Doc
printUseful_info x :: Useful_info
x = case Useful_info
x of
UI_items a :: [Info_item]
a -> Doc -> Doc
brackets (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Info_item] -> Doc
printInfo_items [Info_item]
a
UI_general_list a :: [General_term]
a -> [General_term] -> Doc
forall a. Pretty a => a -> Doc
pretty [General_term]
a
printInfo_items :: Info_items -> Doc
printInfo_items :: [Info_item] -> Doc
printInfo_items = [Doc] -> Doc
sepByCommas ([Doc] -> Doc) -> ([Info_item] -> [Doc]) -> [Info_item] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Info_item -> Doc) -> [Info_item] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Info_item -> Doc
forall a. Pretty a => a -> Doc
pretty
printInfo_item :: Info_item -> Doc
printInfo_item :: Info_item -> Doc
printInfo_item x :: Info_item
x = case Info_item
x of
Info_formula a :: Formula_item
a -> Formula_item -> Doc
forall a. Pretty a => a -> Doc
pretty Formula_item
a
Info_inference a :: Inference_item
a -> Inference_item -> Doc
forall a. Pretty a => a -> Doc
pretty Inference_item
a
Info_general a :: General_function
a -> General_function -> Doc
forall a. Pretty a => a -> Doc
pretty General_function
a
printFormula_item :: Formula_item -> Doc
printFormula_item :: Formula_item -> Doc
printFormula_item x :: Formula_item
x = case Formula_item
x of
FI_description a :: Token
a -> Token -> Doc
printDescription_item Token
a
FI_iquote a :: Token
a -> Token -> Doc
printIquote_item Token
a
printDescription_item :: Description_item -> Doc
printDescription_item :: Token -> Doc
printDescription_item a :: Token
a = String -> Doc
text "description" Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc -> Doc
parens (Token -> Doc
forall a. Pretty a => a -> Doc
pretty Token
a)
printIquote_item :: Iquote_item -> Doc
printIquote_item :: Token -> Doc
printIquote_item a :: Token
a = String -> Doc
text "iquote" Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc -> Doc
parens (Token -> Doc
forall a. Pretty a => a -> Doc
pretty Token
a)
printInference_item :: Inference_item -> Doc
printInference_item :: Inference_item -> Doc
printInference_item x :: Inference_item
x = case Inference_item
x of
Inf_status a :: Inference_status
a -> Inference_status -> Doc
forall a. Pretty a => a -> Doc
pretty Inference_status
a
Inf_assumption a :: [Name]
a -> [Name] -> Doc
printAssumptions_record [Name]
a
Inf_symbol a :: New_symbol_record
a -> New_symbol_record -> Doc
forall a. Pretty a => a -> Doc
pretty New_symbol_record
a
Inf_refutation a :: File_source
a -> File_source -> Doc
printRefutation File_source
a
printInference_status :: Inference_status -> Doc
printInference_status :: Inference_status -> Doc
printInference_status x :: Inference_status
x = case Inference_status
x of
Inf_value a :: Status_value
a -> String -> Doc
text "status" Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc -> Doc
parens (Status_value -> Doc
forall a. Pretty a => a -> Doc
pretty Status_value
a)
Inf_info a :: Inference_info
a -> Inference_info -> Doc
forall a. Pretty a => a -> Doc
pretty Inference_info
a
printStatus_value :: Status_value -> Doc
printStatus_value :: Status_value -> Doc
printStatus_value x :: Status_value
x = case Status_value
x of
SUC -> String -> Doc
text "suc"
UNP -> String -> Doc
text "unp"
SAP -> String -> Doc
text "sap"
ESA -> String -> Doc
text "esa"
SAT -> String -> Doc
text "sat"
FSA -> String -> Doc
text "fsa"
THM -> String -> Doc
text "thm"
EQV -> String -> Doc
text "eqv"
TAC -> String -> Doc
text "tac"
WEC -> String -> Doc
text "wec"
ETH -> String -> Doc
text "eth"
TAU -> String -> Doc
text "tau"
WTC -> String -> Doc
text "wtc"
WTH -> String -> Doc
text "wth"
CAX -> String -> Doc
text "cax"
SCA -> String -> Doc
text "sca"
TCA -> String -> Doc
text "tca"
WCA -> String -> Doc
text "wca"
CUP -> String -> Doc
text "cup"
CSP -> String -> Doc
text "csp"
ECS -> String -> Doc
text "ecs"
CSA -> String -> Doc
text "csa"
CTH -> String -> Doc
text "cth"
CEQ -> String -> Doc
text "ceq"
UNC -> String -> Doc
text "unc"
WCC -> String -> Doc
text "wcc"
ECT -> String -> Doc
text "ect"
FUN -> String -> Doc
text "fun"
UNS -> String -> Doc
text "uns"
WUC -> String -> Doc
text "wuc"
WCT -> String -> Doc
text "wct"
SCC -> String -> Doc
text "scc"
UCA -> String -> Doc
text "uca"
NOC -> String -> Doc
text "noc"
printInference_info :: Inference_info -> Doc
printInference_info :: Inference_info -> Doc
printInference_info x :: Inference_info
x = case Inference_info
x of
Inference_info ir :: Token
ir aw :: Token
aw gl :: [General_term]
gl ->
Token -> Doc
printInference_rule Token
ir
Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc -> Doc
parens ([Doc] -> Doc
sepByCommas [Token -> Doc
forall a. Pretty a => a -> Doc
pretty Token
aw, [General_term] -> Doc
printGeneral_list [General_term]
gl])
printAssumptions_record :: Assumptions_record -> Doc
printAssumptions_record :: [Name] -> Doc
printAssumptions_record x :: [Name]
x =
String -> Doc
text "assumptions" Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc -> Doc
parens (Doc -> Doc
brackets (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Name] -> Doc
printName_list [Name]
x)
printRefutation :: Refutation -> Doc
printRefutation :: File_source -> Doc
printRefutation a :: File_source
a = String -> Doc
text "refutation" Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc -> Doc
parens (File_source -> Doc
printFile_source File_source
a)
printNew_symbol_record :: New_symbol_record -> Doc
printNew_symbol_record :: New_symbol_record -> Doc
printNew_symbol_record x :: New_symbol_record
x = case New_symbol_record
x of
New_symbol_record aw :: Token
aw nsl :: [Principal_symbol]
nsl ->
String -> Doc
text "new_symbols"
Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc -> Doc
parens ([Doc] -> Doc
sepByCommas [Token -> Doc
forall a. Pretty a => a -> Doc
pretty Token
aw, Doc -> Doc
brackets (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Principal_symbol] -> Doc
printNew_symbol_list [Principal_symbol]
nsl])
printNew_symbol_list :: New_symbol_list -> Doc
printNew_symbol_list :: [Principal_symbol] -> Doc
printNew_symbol_list = [Doc] -> Doc
sepByCommas ([Doc] -> Doc)
-> ([Principal_symbol] -> [Doc]) -> [Principal_symbol] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Principal_symbol -> Doc) -> [Principal_symbol] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Principal_symbol -> Doc
forall a. Pretty a => a -> Doc
pretty
printPrincipal_symbol :: Principal_symbol -> Doc
printPrincipal_symbol :: Principal_symbol -> Doc
printPrincipal_symbol x :: Principal_symbol
x = case Principal_symbol
x of
PS_functor a :: Token
a -> Token -> Doc
forall a. Pretty a => a -> Doc
pretty Token
a
PS_variable a :: Token
a -> Token -> Doc
forall a. Pretty a => a -> Doc
pretty Token
a
printInclude :: Include -> Doc
printInclude :: Include -> Doc
printInclude x :: Include
x = case Include
x of
Include fn :: File_name
fn fs :: Formula_selection
fs ->
String -> Doc
text "include" Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc -> Doc
parens ([Doc] -> Doc
fsep [File_name -> Doc
forall a. Pretty a => a -> Doc
pretty File_name
fn, Formula_selection -> Doc
printFormula_selection Formula_selection
fs])
printFormula_selection :: Formula_selection -> Doc
printFormula_selection :: Formula_selection -> Doc
printFormula_selection x :: Formula_selection
x = case Formula_selection
x of
Just ns :: [Name]
ns -> [Doc] -> Doc
fsep [Doc
comma, Doc -> Doc
brackets (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Name] -> Doc
printName_list [Name]
ns]
Nothing -> Doc
empty
printName_list :: Name_list -> Doc
printName_list :: [Name] -> Doc
printName_list = [Doc] -> Doc
sepByCommas ([Doc] -> Doc) -> ([Name] -> [Doc]) -> [Name] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name -> Doc) -> [Name] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Name -> Doc
forall a. Pretty a => a -> Doc
pretty
printGeneral_term :: General_term -> Doc
printGeneral_term :: General_term -> Doc
printGeneral_term x :: General_term
x = case General_term
x of
GT_data a :: General_data
a -> General_data -> Doc
forall a. Pretty a => a -> Doc
pretty General_data
a
GT_DataTerm gd :: General_data
gd gt :: General_term
gt -> [Doc] -> Doc
fsep [General_data -> Doc
forall a. Pretty a => a -> Doc
pretty General_data
gd Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
colon, General_term -> Doc
forall a. Pretty a => a -> Doc
pretty General_term
gt]
GT_list a :: [General_term]
a -> [General_term] -> Doc
printGeneral_list [General_term]
a
printGeneral_data :: General_data -> Doc
printGeneral_data :: General_data -> Doc
printGeneral_data x :: General_data
x = case General_data
x of
GD_atomic_word a :: Token
a -> Token -> Doc
forall a. Pretty a => a -> Doc
pretty Token
a
GD_general_function a :: General_function
a -> General_function -> Doc
forall a. Pretty a => a -> Doc
pretty General_function
a
GD_variable a :: Token
a -> Token -> Doc
forall a. Pretty a => a -> Doc
pretty Token
a
GD_number a :: Number
a -> Number -> Doc
forall a. Pretty a => a -> Doc
pretty Number
a
GD_distinct_object a :: Token
a -> Token -> Doc
forall a. Pretty a => a -> Doc
pretty Token
a
GD_formula_data a :: Formula_data
a -> Formula_data -> Doc
forall a. Pretty a => a -> Doc
pretty Formula_data
a
GD_bind v :: Token
v fd :: Formula_data
fd -> String -> Doc
text "bind" Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc -> Doc
parens ([Doc] -> Doc
sepByCommas [Token -> Doc
forall a. Pretty a => a -> Doc
pretty Token
v, Formula_data -> Doc
forall a. Pretty a => a -> Doc
pretty Formula_data
fd])
printGeneral_function :: General_function -> Doc
printGeneral_function :: General_function -> Doc
printGeneral_function x :: General_function
x = case General_function
x of
General_function aw :: Token
aw gt :: [General_term]
gt -> Token -> Doc
forall a. Pretty a => a -> Doc
pretty Token
aw Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc -> Doc
parens ([General_term] -> Doc
printGeneral_terms [General_term]
gt)
printFormula_data :: Formula_data -> Doc
printFormula_data :: Formula_data -> Doc
printFormula_data x :: Formula_data
x = case Formula_data
x of
FD_THF a :: THF_formula
a -> THF_formula -> Doc
forall a. Pretty a => a -> Doc
pretty THF_formula
a
FD_TFF a :: TFF_formula
a -> TFF_formula -> Doc
forall a. Pretty a => a -> Doc
pretty TFF_formula
a
FD_FOF a :: FOF_formula
a -> FOF_formula -> Doc
forall a. Pretty a => a -> Doc
pretty FOF_formula
a
FD_CNF a :: CNF_formula
a -> CNF_formula -> Doc
forall a. Pretty a => a -> Doc
pretty CNF_formula
a
FD_FOT a :: FOF_term
a -> FOF_term -> Doc
forall a. Pretty a => a -> Doc
pretty FOF_term
a
printGeneral_list :: General_list -> Doc
printGeneral_list :: [General_term] -> Doc
printGeneral_list = Doc -> Doc
brackets (Doc -> Doc) -> ([General_term] -> Doc) -> [General_term] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [General_term] -> Doc
forall a. Pretty a => a -> Doc
pretty
printGeneral_terms :: General_terms -> Doc
printGeneral_terms :: [General_term] -> Doc
printGeneral_terms = [Doc] -> Doc
sepByCommas ([Doc] -> Doc)
-> ([General_term] -> [Doc]) -> [General_term] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (General_term -> Doc) -> [General_term] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map General_term -> Doc
forall a. Pretty a => a -> Doc
pretty
printName :: Name -> Doc
printName :: Name -> Doc
printName x :: Name
x = case Name
x of
NameString a :: Token
a -> Token -> Doc
forall a. Pretty a => a -> Doc
pretty Token
a
NameInteger