7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaDescription : A pretty printer for the TPTP Syntax v6.4.0.7
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaCopyright : (c) Eugen Kuksa University of Magdeburg 2017
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaLicense : GPLv2 or higher, see LICENSE.txt
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaMaintainer : Eugen Kuksa <kuksa@iks.cs.ovgu.de>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaStability : provisional
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaPortability : portable
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaA pretty printer for the TPTP Input Syntax v6.4.0.7 taken from
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa<http://www.cs.miami.edu/~tptp/TPTP/SyntaxBNF.html>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksamodule TPTP.Pretty (printBasicTheory, printNamedSentence) where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksaimport Common.AS_Annotation hiding (Name)
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksaimport Common.Id (Token)
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksaimport Common.Doc hiding (defn)
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksaimport Data.Char (toLower)
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksaimport qualified Data.Map as Map
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksaimport qualified Data.Set as Set
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa{- -----------------------------------------------------------------------------
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaPretty instances
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa----------------------------------------------------------------------------- -}
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty Symbol where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printSymbol
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty Sign where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printSign
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty BASIC_SPEC where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printBasicSpec
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty TPTP where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printTPTP
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty TPTP_input where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printTPTP_input
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty Comment where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printComment
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty DefinedComment where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printDefinedComment
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty SystemComment where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printSystemComment
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty Annotated_formula where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printAnnotated_formula
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty TPI_annotated where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printTPI_annotated
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty THF_annotated where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printTHF_annotated
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty TFX_annotated where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printTFX_annotated
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty TFF_annotated where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printTFF_annotated
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty TCF_annotated where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printTCF_annotated
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty FOF_annotated where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printFOF_annotated
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty CNF_annotated where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printCNF_annotated
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty Annotations where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printAnnotations
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty Formula_role where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printFormula_role
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty THF_formula where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printTHF_formula
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty THF_logic_formula where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printTHF_logic_formula
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty THF_binary_formula where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printTHF_binary_formula
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty THF_binary_pair where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printTHF_binary_pair
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty THF_binary_tuple where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printTHF_binary_tuple
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty THF_unitary_formula where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printTHF_unitary_formula
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty THF_quantified_formula where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printTHF_quantified_formula
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty THF_quantification where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printTHF_quantification
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty THF_variable where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printTHF_variable
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty THF_typed_variable where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printTHF_typed_variable
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty THF_unary_formula where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printTHF_unary_formula
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty THF_atom where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printTHF_atom
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty THF_function where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printTHF_function
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty THF_conn_term where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printTHF_conn_term
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty THF_conditional where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printTHF_conditional
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty THF_let where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printTHF_let
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty THF_let_defns where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printTHF_let_defns
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty THF_let_defn where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printTHF_let_defn
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty THF_let_quantified_defn where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printTHF_let_quantified_defn
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty THF_let_plain_defn where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printTHF_let_plain_defn
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty THF_let_defn_LHS where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printTHF_let_defn_LHS
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty THF_type_formula where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printTHF_type_formula
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty THF_typeable_formula where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printTHF_typeable_formula
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty THF_subtype where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printTHF_subtype
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty THF_top_level_type where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printTHF_top_level_type
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty THF_unitary_type where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printTHF_unitary_type
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty THF_binary_type where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printTHF_binary_type
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty THF_sequent where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printTHF_sequent
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty THF_tuple where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printTHF_tuple
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty TFX_formula where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printTFX_formula
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty TFX_logic_formula where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printTFX_logic_formula
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty TFF_formula where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printTFF_formula
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty TFF_logic_formula where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printTFF_logic_formula
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty TFF_binary_formula where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printTFF_binary_formula
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty TFF_binary_nonassoc where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printTFF_binary_nonassoc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty TFF_binary_assoc where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printTFF_binary_assoc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty TFF_unitary_formula where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printTFF_unitary_formula
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty TFF_quantified_formula where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printTFF_quantified_formula
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty TFF_variable where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printTFF_variable
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty TFF_typed_variable where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printTFF_typed_variable
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty TFF_unary_formula where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printTFF_unary_formula
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty TFF_conditional where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printTFF_conditional
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty TFF_let where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printTFF_let
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty TFF_let_term_defns where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printTFF_let_term_defns
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty TFF_let_term_defn where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printTFF_let_term_defn
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty TFF_let_term_binding where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printTFF_let_term_binding
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty TFF_let_formula_defns where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printTFF_let_formula_defns
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty TFF_let_formula_defn where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printTFF_let_formula_defn
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty TFF_let_formula_binding where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printTFF_let_formula_binding
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty TFF_sequent where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printTFF_sequent
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty TFF_formula_tuple where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printTFF_formula_tuple
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty TFF_typed_atom where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printTFF_typed_atom
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty TFF_subtype where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printTFF_subtype
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty TFF_top_level_type where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printTFF_top_level_type
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty TF1_quantified_type where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printTF1_quantified_type
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty TFF_monotype where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printTFF_monotype
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty TFF_unitary_type where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printTFF_unitary_type
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty TFF_atomic_type where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printTFF_atomic_type
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty TFF_mapping_type where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printTFF_mapping_type
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty TFF_xprod_type where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printTFF_xprod_type
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty TCF_formula where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printTCF_formula
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty TCF_logic_formula where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printTCF_logic_formula
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty TCF_quantified_formula where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printTCF_quantified_formula
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty FOF_formula where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printFOF_formula
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty FOF_logic_formula where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printFOF_logic_formula
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty FOF_binary_formula where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printFOF_binary_formula
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty FOF_binary_nonassoc where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printFOF_binary_nonassoc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty FOF_binary_assoc where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printFOF_binary_assoc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty FOF_unitary_formula where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printFOF_unitary_formula
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty FOF_quantified_formula where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printFOF_quantified_formula
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty FOF_unary_formula where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printFOF_unary_formula
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty FOF_infix_unary where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printFOF_infix_unary
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty FOF_atomic_formula where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printFOF_atomic_formula
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty FOF_plain_atomic_formula where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printFOF_plain_atomic_formula
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty FOF_defined_atomic_formula where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printFOF_defined_atomic_formula
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty FOF_defined_plain_formula where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printFOF_defined_plain_formula
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty FOF_defined_infix_formula where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printFOF_defined_infix_formula
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty FOF_system_atomic_formula where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printFOF_system_atomic_formula
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty FOF_plain_term where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printFOF_plain_term
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty FOF_defined_term where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printFOF_defined_term
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty FOF_defined_atomic_term where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printFOF_defined_atomic_term
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty FOF_defined_plain_term where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printFOF_defined_plain_term
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty FOF_system_term where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printFOF_system_term
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty FOF_term where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printFOF_term
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty FOF_function_term where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printFOF_function_term
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty TFF_conditional_term where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printTFF_conditional_term
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty TFF_let_term where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printTFF_let_term
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty FOF_sequent where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printFOF_sequent
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty FOF_formula_tuple where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printFOF_formula_tuple
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty CNF_formula where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printCNF_formula
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty Disjunction where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printDisjunction
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty Literal where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printLiteral
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty THF_quantifier where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printTHF_quantifier
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty TH1_quantifier where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printTH1_quantifier
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty TH0_quantifier where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printTH0_quantifier
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty THF_pair_connective where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printTHF_pair_connective
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty THF_unary_connective where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printTHF_unary_connective
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty TH1_unary_connective where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printTH1_unary_connective
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty FOF_quantifier where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printFOF_quantifier
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty Binary_connective where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printBinary_connective
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty Assoc_connective where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printAssoc_connective
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty Unary_connective where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printUnary_connective
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty Defined_type where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printDefined_type
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty Atom where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printAtom
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty Untyped_atom where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printUntyped_atom
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty Defined_proposition where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printDefined_proposition
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty Defined_predicate where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printDefined_predicate
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty Defined_infix_pred where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printDefined_infix_pred
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty Defined_functor where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printDefined_functor
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty Defined_term where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printDefined_term
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty Source where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printSource
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty DAG_source where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printDAG_source
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty Inference_record where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printInference_record
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty Parent_info where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printParent_info
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty Internal_source where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printInternal_source
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty Intro_type where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printIntro_type
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty External_source where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printExternal_source
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty File_source where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printFile_source
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty Theory where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printTheory
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty Theory_name where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printTheory_name
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty Creator_source where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printCreator_source
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty Useful_info where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printUseful_info
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty Info_item where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printInfo_item
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty Formula_item where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printFormula_item
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty Inference_item where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printInference_item
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty Inference_status where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printInference_status
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty Status_value where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printStatus_value
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty Inference_info where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printInference_info
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty New_symbol_record where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printNew_symbol_record
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty Principal_symbol where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printPrincipal_symbol
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty Include where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printInclude
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty General_term where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printGeneral_term
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty General_data where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printGeneral_data
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty General_function where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printGeneral_function
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty Formula_data where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printFormula_data
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty Name where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printName
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainstance Pretty Number where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty = printNumber
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa{- -----------------------------------------------------------------------------
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaLogic components
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa----------------------------------------------------------------------------- -}
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- Print a newline at the end of the document for good style.
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintBasicTheory :: (Sign, [Named Sentence]) -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintBasicTheory (_, l) = vsep (map printNamedSentence l) $+$ text ""
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintNamedSentence :: Named Sentence -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintNamedSentence = printAnnotated_formula . sentence
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintSymbol :: Symbol -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintSymbol = pretty . symbolId
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintSign :: Sign -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintSign s =
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa vsep [ text "%{"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa , if Set.null $ constantSet s then empty else
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa text "constants: "
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa <+> sepByCommas (map pretty $ Set.toList $ constantSet s)
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa , if Set.null $ numberSet s then empty else
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa text "numbers: "
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa <+> sepByCommas (map pretty $ Set.toList $ numberSet s)
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa , if Set.null $ propositionSet s then empty else
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa text "propositions: "
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa <+> sepByCommas (map pretty $ Set.toList $ propositionSet s)
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa , if Map.null (tffPredicateMap s) && Map.null (thfPredicateMap s) && Map.null (fofPredicateMap s) then empty else
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa text "predicates: "
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa <+> vcat (punctuate comma
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa (map printTHFType (Map.toList $ thfPredicateMap s)
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa ++ map printTFFType (Map.toList $ tffPredicateMap s)
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa ++ map printFOFPredicate (Map.toList $ fofPredicateMap s)))
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa , if Map.null (fofFunctorMap s) then empty else
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa text "functors: "
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa <+> vcat (punctuate comma
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa (map printFOFFunctor (Map.toList $ fofFunctorMap s)))
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa , if Map.null (tffTypeConstantMap s) && Map.null (thfTypeConstantMap s) then empty else
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa text "type constants: "
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa <+> vcat (punctuate comma
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa (map printTHFType (Map.toList $ thfTypeConstantMap s)
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa ++ map printTFFType (Map.toList $ tffTypeConstantMap s)))
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa , if Map.null (tffTypeFunctorMap s) && Map.null (thfTypeFunctorMap s) then empty else
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa text "type functors: "
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa <+> vcat (punctuate comma
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa (map printTHFType (Map.toList $ thfTypeFunctorMap s)
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa ++ map printTFFType (Map.toList $ tffTypeFunctorMap s)))
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa , if Map.null (tffSubtypeMap s) && Map.null (thfSubtypeMap s) then empty else
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa text "subtypes: "
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa <+> vcat (punctuate comma
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa (map printTHFSubType (Map.toList $ thfSubtypeMap s)
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa ++ map printTFFSubType (Map.toList $ tffSubtypeMap s)))
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa , text "}%"]
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa printTHFType :: (THFTypeable, THF_top_level_type) -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa printTHFType (t, tlt) = pretty $ case t of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa THFTypeFormula f -> THFTF_typeable f tlt
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa THFTypeConstant c -> THFTF_constant c tlt
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa printTFFType :: (Untyped_atom, TFF_top_level_type) -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa printTFFType (a, tlt) = pretty $ TFFTA_plain a tlt
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa printFOFPredicate :: (Predicate, Set.Set Int) -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa printFOFPredicate (p, arities) = vcat $ punctuate comma $
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa map (printFOFPredicateOrFunctor p O) $ Set.toList arities
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa printFOFFunctor :: (TPTP_functor, Set.Set Int) -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa printFOFFunctor (p, arities) = vcat $ punctuate comma $
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa map (printFOFPredicateOrFunctor p I) $ Set.toList arities
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa printFOFPredicateOrFunctor :: Token -> Defined_type -> Int -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa printFOFPredicateOrFunctor token typ arity =
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa let arguments =
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa if arity == 0
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa else if arity == 1
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa then pretty I <+> text ">"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa else parens (sepBy (text "*") $ map pretty $ replicate arity I)
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa <+> text ">"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa in pretty token <> colon <+> arguments <+> pretty typ
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa printTHFSubType :: (THF_atom, THF_atom) -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa printTHFSubType (a1, a2) = pretty $ THF_subtype a1 a2
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa printTFFSubType :: (Untyped_atom, Atom) -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa printTFFSubType (a1, a2) = pretty $ TFF_subtype a1 a2
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintBasicSpec :: BASIC_SPEC -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintBasicSpec (Basic_spec xs) = vcat $ map pretty xs
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa{- -----------------------------------------------------------------------------
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaFiles. Empty file is OK
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa----------------------------------------------------------------------------- -}
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <TPTP_file> ::= <TPTP_input>*
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTPTP :: TPTP -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTPTP (TPTP tptp_inputs) = vsep $ map pretty tptp_inputs
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <TPTP_input> ::= <annotated_formula> | <include>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTPTP_input :: TPTP_input -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTPTP_input x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa Annotated_formula a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa TPTP_include i -> pretty i
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa TPTP_comment c -> pretty c
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa TPTP_defined_comment c -> pretty c
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa TPTP_system_comment c -> pretty c
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa{- -----------------------------------------------------------------------------
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa----------------------------------------------------------------------------- -}
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <comment> ::- <comment_line>|<comment_block>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <comment_line> ::- [%]<printable_char>*
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <comment_block> ::: [/][*]<not_star_slash>[*][*]*[/]
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintComment :: Comment -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintComment comment = case comment of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa Comment_line c -> text "%" <+> pretty c
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa Comment_block c -> text "/*" <+> pretty c <+> text "*/"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- %---- <defined_comment> ::- <def_comment_line>|<def_comment_block>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- %---- <def_comment_line> ::: [%]<dollar><printable_char>*
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- %---- <def_comment_block> ::: [/][*]<dollar><not_star_slash>[*][*]*[/]
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintDefinedComment :: DefinedComment -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintDefinedComment comment = case comment of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa Defined_comment_line c -> text "%$" <+> pretty c
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa Defined_comment_block c -> text "/*$" <+> pretty c <+> text "*/"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- %---- <system_comment> ::- <sys_comment_line>|<sys_comment_block>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- %---- <sys_comment_line> ::: [%]<dollar><dollar><printable_char>*
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- %---- <sys_comment_block> ::: [/][*]<dollar><dollar><not_star_slash>[*][*]*[/]
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintSystemComment :: SystemComment -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintSystemComment comment = case comment of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa System_comment_line c -> text "%$$" <+> pretty c
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa System_comment_block c -> text "/*$$" <+> pretty c <+> text "*/"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- %----Formula records
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <annotated_formula> ::= <thf_annotated> | <tfx_annotated> | <tff_annotated> |
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <tcf_annotated> | <fof_annotated> | <cnf_annotated> |
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <tpi_annotated>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintAnnotated_formula :: Annotated_formula -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintAnnotated_formula x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa AF_THF_Annotated f -> pretty f
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa AF_TFX_Annotated f -> pretty f
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa AF_TFF_Annotated f -> pretty f
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa AF_TCF_Annotated f -> pretty f
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa AF_FOF_Annotated f -> pretty f
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa AF_CNF_Annotated f -> pretty f
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa AF_TPI_Annotated f -> pretty f
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <???_annotated> contains the annotations, which are introduced with a comma.
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <annotations> ::= ,<source><optional_info> | <null>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintAnnotationsIfAnnotated :: Annotations -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintAnnotationsIfAnnotated a@(Annotations ma) = case ma of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa Just _ -> comma <+> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa Nothing -> empty
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <tpi_annotated> ::= tpi(<name>,<formula_role>,<tpi_formula><annotations>).
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTPI_annotated :: TPI_annotated -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTPI_annotated x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa TPI_annotated n r f a ->
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa <> parens (sepByCommas [pretty n, pretty r, pretty f] <> printAnnotationsIfAnnotated a)
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <tpi_formula> ::= <fof_formula>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <thf_annotated> ::= thf(<name>,<formula_role>,<thf_formula>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <annotations>).
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTHF_annotated :: THF_annotated -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTHF_annotated x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa THF_annotated n r f a ->
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa <> parens (sepByCommas [pretty n, pretty r, pretty f] <> printAnnotationsIfAnnotated a)
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <tfx_annotated> ::= tfx(<name>,<formula_role>,<tfx_formula>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <annotations>).
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTFX_annotated :: TFX_annotated -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTFX_annotated x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa TFX_annotated n r f a ->
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa <> parens (sepByCommas [pretty n, pretty r, pretty f] <> printAnnotationsIfAnnotated a)
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <tff_annotated> ::= tff(<name>,<formula_role>,<tff_formula>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <annotations>).
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTFF_annotated :: TFF_annotated -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTFF_annotated x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa TFF_annotated n r f a ->
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa <> parens (sepByCommas [pretty n, pretty r, pretty f] <> printAnnotationsIfAnnotated a)
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <tcf_annotated> ::= tcf(<name>,<formula_role>,<tcf_formula>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <annotations>).
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTCF_annotated :: TCF_annotated -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTCF_annotated x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa TCF_annotated n r f a ->
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa <> parens (sepByCommas [pretty n, pretty r, pretty f] <> printAnnotationsIfAnnotated a)
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <fof_annotated> ::= fof(<name>,<formula_role>,<fof_formula>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <annotations>).
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintFOF_annotated :: FOF_annotated -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintFOF_annotated x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa FOF_annotated n r f a ->
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa <> parens (sepByCommas [pretty n, pretty r, pretty f] <> printAnnotationsIfAnnotated a)
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <cnf_annotated> ::= cnf(<name>,<formula_role>,<cnf_formula>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <annotations>).
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintCNF_annotated :: CNF_annotated -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintCNF_annotated x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa CNF_annotated n r f a ->
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa <> parens (sepByCommas [pretty n, pretty r, pretty f]
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa <> printAnnotationsIfAnnotated a)
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <annotations> ::= ,<source><optional_info> | <null>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintAnnotations :: Annotations -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintAnnotations (Annotations mAnno) = case mAnno of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa Nothing -> empty
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa Just (source, optionalInfo) ->
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa fsep [pretty source, printOptional_info optionalInfo]
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- Types for problems
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- %----Types for problems.
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <formula_role> ::= <lower_word>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <formula_role> :== axiom | hypothesis | definition | assumption |
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- lemma | theorem | corollary | conjecture |
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- negated_conjecture | plain | type |
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- fi_domain | fi_functors | fi_predicates | unknown
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintFormula_role :: Formula_role -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintFormula_role x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa Other_formula_role t -> pretty t
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa -- ^ For future updates. Should not be used.
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa _ -> text $ map toLower $ show x
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- %----THF formulae.
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <thf_formula> ::= <thf_logic_formula> | <thf_sequent>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTHF_formula :: THF_formula -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTHF_formula x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa THFF_logic f -> pretty f
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa THFF_sequent s -> pretty s
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <thf_logic_formula> ::= <thf_binary_formula> | <thf_unitary_formula> |
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <thf_type_formula> | <thf_subtype>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTHF_logic_formula :: THF_logic_formula -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTHF_logic_formula x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa THFLF_binary f -> pretty f
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa THFLF_unitary f -> pretty f
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa THFLF_type f -> pretty f
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa THFLF_subtype f -> pretty f
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <thf_binary_formula> ::= <thf_binary_pair> | <thf_binary_tuple>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTHF_binary_formula :: THF_binary_formula -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTHF_binary_formula x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa THFBF_pair a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa THFBF_tuple a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- %----Only some binary connectives can be written without ()s.
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- %----There's no precedence among binary connectives
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <thf_binary_pair> ::= <thf_unitary_formula> <thf_pair_connective>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <thf_unitary_formula>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTHF_binary_pair :: THF_binary_pair -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTHF_binary_pair x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa THF_binary_pair c f1 f2 -> fsep [pretty f1, pretty c, pretty f2]
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <thf_binary_tuple> ::= <thf_or_formula> | <thf_and_formula> |
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <thf_apply_formula>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTHF_binary_tuple :: THF_binary_tuple -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTHF_binary_tuple x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa THFBT_or fs -> printTHF_or_formula fs
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa THFBT_and fs -> printTHF_and_formula fs
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa THFBT_apply fs -> printTHF_apply_formula fs
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <thf_or_formula> ::= <thf_unitary_formula> <vline> <thf_unitary_formula> |
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <thf_or_formula> <vline> <thf_unitary_formula>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTHF_or_formula :: THF_or_formula -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTHF_or_formula fs = sepBy vline $ map pretty fs
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <thf_and_formula> ::= <thf_unitary_formula> & <thf_unitary_formula> |
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <thf_and_formula> & <thf_unitary_formula>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTHF_and_formula :: THF_or_formula -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTHF_and_formula fs = sepBy andD $ map pretty fs
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <thf_apply_formula> ::= <thf_unitary_formula> @ <thf_unitary_formula> |
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <thf_apply_formula> @ <thf_unitary_formula>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTHF_apply_formula :: THF_or_formula -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTHF_apply_formula fs = sepBy atD $ map pretty fs
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <thf_unitary_formula> ::= <thf_quantified_formula> | <thf_unary_formula> |
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <thf_atom> | <thf_conditional> | <thf_let> |
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <thf_tuple> | (<thf_logic_formula>)
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTHF_unitary_formula :: THF_unitary_formula -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTHF_unitary_formula x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa THFUF_quantified a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa THFUF_unary a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa THFUF_atom a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa THFUF_conditional a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa THFUF_let a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa THFUF_tuple a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa THFUF_logic a -> parens $ pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <thf_quantified_formula> ::= <thf_quantification> <thf_unitary_formula>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTHF_quantified_formula :: THF_quantified_formula -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTHF_quantified_formula x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa THF_quantified_formula q f -> hsep [pretty q, pretty f]
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <thf_quantification> ::= <thf_quantifier> [<thf_variable_list>] :
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTHF_quantification :: THF_quantification -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTHF_quantification x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa THF_quantification q vars ->
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa hsep [pretty q, brackets (printTHF_variable_list vars) <> colon]
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <thf_variable_list> ::= <thf_variable> | <thf_variable>,<thf_variable_list>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTHF_variable_list :: THF_variable_list -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTHF_variable_list vars = sepByCommas $ map pretty vars
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <thf_variable> ::= <thf_typed_variable> | <variable>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTHF_variable :: THF_variable -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTHF_variable x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa THFV_typed a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa THFV_variable a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <thf_typed_variable> ::= <variable> : <thf_top_level_type>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTHF_typed_variable :: THF_typed_variable -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTHF_typed_variable x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa THF_typed_variable v tlt -> fsep [pretty v <> colon, pretty tlt]
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <thf_unary_formula> ::= <thf_unary_connective> (<thf_logic_formula>)
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTHF_unary_formula :: THF_unary_formula -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTHF_unary_formula x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa THF_unary_formula c f -> pretty c <> parens (pretty f)
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <thf_atom> ::= <thf_function> | <variable> | <defined_term> |
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <thf_conn_term>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTHF_atom :: THF_atom -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTHF_atom x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa THF_atom_function a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa THF_atom_variable a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa THF_atom_defined a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa THF_atom_conn a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <thf_function> ::= <atom> | <functor>(<thf_arguments>) |
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <defined_functor>(<thf_arguments>) |
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <system_functor>(<thf_arguments>)
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTHF_function :: THF_function -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTHF_function x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa THFF_atom a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa THFF_functor f args -> pretty f <> parens (printTHF_arguments args)
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa THFF_defined f args -> pretty f <> parens (printTHF_arguments args)
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa THFF_system f args -> pretty f <> parens (printTHF_arguments args)
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <thf_conn_term> ::= <thf_pair_connective> | <assoc_connective> |
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <thf_unary_connective>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTHF_conn_term :: THF_conn_term -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTHF_conn_term x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa THFC_pair a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa THFC_assoc a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa THFC_unary a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <thf_conditional> ::= $ite(<thf_logic_formula>,<thf_logic_formula>,
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <thf_logic_formula>)
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTHF_conditional :: THF_conditional -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTHF_conditional x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa THF_conditional f_if f_then f_else ->
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa <> parens (sepByCommas [pretty f_if, pretty f_then, pretty f_else])
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- %----The LHS of a term or formula binding must be a non-variable term that
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- %----is flat with pairwise distinct variable arguments, and the variables in
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- %----the LHS must be exactly those bound in the universally quantified variable
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- %----list, in the same order. Let definitions are not recursive: a non-variable
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- %----symbol introduced in the LHS of a let definition cannot occur in the RHS.
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- %----If a symbol with the same signature as the one in the LHS of the binding
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- %----is declared above the let expression (at the top level or in an
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- %----encompassing let) then it can be used in the RHS of the binding, but it is
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- %----not accessible in the term or formula of the let expression. Let
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- %----expressions can be eliminated by a simple definition expansion.
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <thf_let> ::= $let(<thf_unitary_formula>,<thf_formula>)
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <thf_let> :== $let(<thf_let_defns>,<thf_formula>)
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTHF_let :: THF_let -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTHF_let x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa THF_let defns f ->
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa text "$let" <> parens (sepByCommas [pretty defns, pretty f])
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <thf_let_defns> :== <thf_let_defn> | [<thf_let_defn_list>]
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTHF_let_defns :: THF_let_defns -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTHF_let_defns x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa THFLD_single a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa THFLD_many a -> brackets $ printTHF_let_defn_list a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <thf_let_defn_list> :== <thf_let_defn> | <thf_let_defn>,<thf_let_defn_list>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTHF_let_defn_list :: THF_let_defn_list -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTHF_let_defn_list = sepByCommas . map pretty
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <thf_let_defn> :== <thf_let_quantified_defn> | <thf_let_plain_defn>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTHF_let_defn :: THF_let_defn -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTHF_let_defn x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa THFLD_quantified a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa THFLD_plain a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <thf_let_quantified_defn> :== <thf_quantification> (<thf_let_plain_defn>)
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTHF_let_quantified_defn :: THF_let_quantified_defn -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTHF_let_quantified_defn x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa THF_let_quantified_defn q lpd ->
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa pretty q <> parens (pretty lpd)
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <thf_let_plain_defn> :== <thf_let_defn_LHS> <assignment> <thf_formula>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTHF_let_plain_defn :: THF_let_plain_defn -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTHF_let_plain_defn x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa THF_let_plain_defn lhs f -> fsep [pretty lhs, assignment, pretty f]
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <thf_let_defn_LHS> :== <constant> | <functor>(<fof_arguments>) |
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <thf_tuple>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- %----The <fof_arguments> must all be <variable>s, and the <thf_tuple> may
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- %----contain only <constant>s and <functor>(<fof_arguments>)s
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTHF_let_defn_LHS :: THF_let_defn_LHS -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTHF_let_defn_LHS x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa THFLDL_constant a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa THFLDL_functor f args -> pretty f <> parens (printFOF_arguments args)
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa THFLDL_tuple a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <thf_arguments> ::= <thf_formula_list>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTHF_arguments :: THF_arguments -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTHF_arguments x = printTHF_formula_list x
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <thf_type_formula> ::= <thf_typeable_formula> : <thf_top_level_type>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <thf_type_formula> :== <constant> : <thf_top_level_type>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTHF_type_formula :: THF_type_formula -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTHF_type_formula x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa THFTF_typeable f tlt -> fsep [pretty f <> colon, pretty tlt]
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa THFTF_constant c tlt -> fsep [pretty c <> colon, pretty tlt]
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <thf_typeable_formula> ::= <thf_atom> | (<thf_logic_formula>)
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTHF_typeable_formula :: THF_typeable_formula -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTHF_typeable_formula x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa THFTF_atom a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa THFTF_logic a -> parens $ pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <thf_subtype> ::= <thf_atom> <subtype_sign> <thf_atom>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTHF_subtype :: THF_subtype -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTHF_subtype x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa THF_subtype a1 a2 -> fsep [pretty a1, subtype_sign, pretty a2]
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- %----<thf_top_level_type> appears after ":", where a type is being specified
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- %----for a term or variable. <thf_unitary_type> includes <thf_unitary_formula>,
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- %----so the syntax allows just about any lambda expression with "enough"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- %----parentheses to serve as a type. The expected use of this flexibility is
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- %----parametric polymorphism in types, expressed with lambda abstraction.
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- %----Mapping is right-associative: o > o > o means o > (o > o).
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- %----Xproduct is left-associative: o * o * o means (o * o) * o.
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- %----Union is left-associative: o + o + o means (o + o) + o.
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <thf_top_level_type> ::= <thf_unitary_type> | <thf_mapping_type>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTHF_top_level_type :: THF_top_level_type -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTHF_top_level_type x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa THFTLT_unitary a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa THFTLT_mapping a -> printTHF_mapping_type a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <thf_unitary_type> ::= <thf_unitary_formula> | (<thf_binary_type>)
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTHF_unitary_type :: THF_unitary_type -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTHF_unitary_type x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa THFUT_unitary a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa THFUT_binary a -> parens $ pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- Each of these binary types has at least two (!) list entries.
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <thf_binary_type> ::= <thf_mapping_type> | <thf_xprod_type> |
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <thf_union_type>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTHF_binary_type :: THF_binary_type -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTHF_binary_type x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa THFBT_mapping a -> printTHF_mapping_type a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa THFBT_xprod a -> printTHF_xprod_type a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa THFBT_union a -> printTHF_union_type a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <thf_mapping_type> ::= <thf_unitary_type> <arrow> <thf_unitary_type> |
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <thf_unitary_type> <arrow> <thf_mapping_type>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTHF_mapping_type :: THF_mapping_type -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTHF_mapping_type = sepBy arrow . map pretty
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <thf_xprod_type> ::= <thf_unitary_type> <star> <thf_unitary_type> |
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <thf_xprod_type> <star> <thf_unitary_type>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTHF_xprod_type :: THF_xprod_type -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTHF_xprod_type = sepBy star . map pretty
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <thf_union_type> ::= <thf_unitary_type> <plus> <thf_unitary_type> |
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <thf_union_type> <plus> <thf_unitary_type>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTHF_union_type :: THF_union_type -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTHF_union_type = sepBy plus . map pretty
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- %----Sequents using the Gentzen arrow
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <thf_sequent> ::= <thf_tuple> <gentzen_arrow> <thf_tuple> |
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- (<thf_sequent>)
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTHF_sequent :: THF_sequent -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTHF_sequent x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa THFS_plain t1 t2 -> sepBy gentzen_arrow [pretty t1, pretty t2]
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa THFS_parens a -> parens $ pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <thf_tuple> ::= [] | [<thf_formula_list>]
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTHF_tuple :: THF_tuple -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTHF_tuple x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa THF_tuple a -> brackets $ printTHF_formula_list a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <thf_formula_list> ::= <thf_logic_formula> |
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <thf_logic_formula>,<thf_formula_list>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTHF_formula_list :: THF_formula_list -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTHF_formula_list = sepByCommas . map pretty
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- NOTE: not used by parser
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- %----New material for modal logic semantics, not integrated yet
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <logic_defn_rule> :== <logic_defn_LHS> <assignment> <logic_defn_RHS>-
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- data Logic_defn_rule = Logic_defn_rule Logic_defn_LHS Logic_defn_RHS
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- deriving (Show, Ord, Eq, Data, Typeable)
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- NOTE: not used by parser
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <logic_defn_LHS> :== <logic_defn_value> | <thf_top_level_type> | <name>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <logic_defn_LHS> :== $constants | $quantification | $consequence |
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- $modalities
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- %----The $constants, $quantification, and $consequence apply to all of the
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- %----$modalities. Each of these may be specified only once, but not necessarily
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- %----all in a single annotated formula.-
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- data Logic_defn_LHS = Logic_defn_LHS_value Logic_defn_value
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- | Logic_defn_LHS_THF_Top_level_type THF_top_level_type
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- | Logic_defn_LHS_name Name
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- | LDLC_constants
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- | LDLC_quantification
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- | LDLC_consequence
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- | LDLC_modalities
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- deriving (Show, Ord, Eq, Data, Typeable)
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- NOTE: not used by parser
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <logic_defn_RHS> :== <logic_defn_value> | <thf_unitary_formula>-
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- data Logic_defn_RHS = Logic_defn_RHS_value Logic_defn_value
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- | Logic_defn_RNG_THF_Unitary_forumla THF_unitary_formula
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- deriving (Show, Ord, Eq, Data, Typeable)
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- NOTE: not used by parser
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <logic_defn_value> :== <defined_constant>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <logic_defn_value> :== $rigid | $flexible |
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- $constant | $varying | $cumulative | $decreasing |
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- $local | $global |
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- $modal_system_K | $modal_system_T | $modal_system_D |
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- $modal_system_S4 | $modal_system_S5 |
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- $modal_axiom_K | $modal_axiom_T | $modal_axiom_B |
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- $modal_axiom_D | $modal_axiom_4 | $modal_axiom_5-
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- data Logic_defn_value = Rigid
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- | Flexible
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- | Constant
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- | Cumulative
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- | Decreasing
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- | Modal_system_K
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- | Modal_system_T
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- | Modal_system_D
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- | Modal_system_S4
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- | Modal_system_S5
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- | Modal_axiom_K
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- | Modal_axiom_T
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- | Modal_axiom_B
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- | Modal_axiom_D
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- | Modal_axiom_4
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- | Modal_axiom_5
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- deriving (Show, Ord, Eq, Data, Typeable)
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- %----TFX formulae
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <tfx_formula> ::= <tfx_logic_formula> | <thf_sequent>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTFX_formula :: TFX_formula -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTFX_formula x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa TFXF_logic a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa TFXF_sequent a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <tfx_logic_formula> ::= <thf_logic_formula>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- % <tfx_logic_formula> ::= <thf_binary_formula> | <thf_unitary_formula> |
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- % <tff_typed_atom> | <tff_subtype>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTFX_logic_formula :: TFX_logic_formula -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTFX_logic_formula x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa TFXLF_binary a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa TFXLF_unitary a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa TFXLF_typed a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa TFXLF_subtype a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- %----TFF formulae.
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <tff_formula> ::= <tff_logic_formula> | <tff_typed_atom> |
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <tff_sequent>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTFF_formula :: TFF_formula -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTFF_formula x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa TFFF_logic a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa TFFF_atom a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa TFFF_sequent a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <tff_logic_formula> ::= <tff_binary_formula> | <tff_unitary_formula> |
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <tff_subtype>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTFF_logic_formula :: TFF_logic_formula -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTFF_logic_formula x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa TFFLF_binary a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa TFFLF_unitary a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa TFFLF_subtype a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <tff_binary_formula> ::= <tff_binary_nonassoc> | <tff_binary_assoc>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTFF_binary_formula :: TFF_binary_formula -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTFF_binary_formula x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa TFFBF_nonassoc a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa TFFBF_assoc a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <tff_binary_nonassoc> ::= <tff_unitary_formula> <binary_connective>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <tff_unitary_formula>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTFF_binary_nonassoc :: TFF_binary_nonassoc -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTFF_binary_nonassoc x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa TFF_binary_nonassoc c f1 f2 -> fsep [pretty f1, pretty c, pretty f2]
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <tff_binary_assoc> ::= <tff_or_formula> | <tff_and_formula>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTFF_binary_assoc :: TFF_binary_assoc -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTFF_binary_assoc x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa TFFBA_or a -> printTFF_or_formula a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa TFFBA_and a -> printTFF_and_formula a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <tff_or_formula> ::= <tff_unitary_formula> <vline> <tff_unitary_formula> |
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <tff_or_formula> <vline> <tff_unitary_formula>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTFF_or_formula :: TFF_or_formula -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTFF_or_formula = sepBy vline . map pretty
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <tff_and_formula> ::= <tff_unitary_formula> & <tff_unitary_formula> |
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <tff_and_formula> & <tff_unitary_formula>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTFF_and_formula :: TFF_and_formula -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTFF_and_formula = sepBy andD . map pretty
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <tff_unitary_formula> ::= <tff_quantified_formula> | <tff_unary_formula> |
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <tff_atomic_formula> | <tff_conditional> |
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <tff_let> | (<tff_logic_formula>)
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTFF_unitary_formula :: TFF_unitary_formula -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTFF_unitary_formula x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa TFFUF_quantified a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa TFFUF_unary a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa TFFUF_atomic a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa TFFUF_conditional a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa TFFUF_let a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa TFFUF_logic a -> parens $ pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <tff_quantified_formula> ::= <fof_quantifier> [<tff_variable_list>] :
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <tff_unitary_formula>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTFF_quantified_formula :: TFF_quantified_formula -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTFF_quantified_formula x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa TFF_quantified_formula q vars f ->
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa hsep [pretty q, brackets (printTFF_variable_list vars) <> colon, pretty f]
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <tff_variable_list> ::= <tff_variable> | <tff_variable>,<tff_variable_list>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTFF_variable_list :: TFF_variable_list -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTFF_variable_list = sepByCommas . map pretty
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <tff_variable> ::= <tff_typed_variable> | <variable>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTFF_variable :: TFF_variable -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTFF_variable x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa TFFV_typed a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa TFFV_variable a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <tff_typed_variable> ::= <variable> : <tff_atomic_type>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTFF_typed_variable :: TFF_typed_variable -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTFF_typed_variable x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa TFF_typed_variable v t -> fsep [pretty v <> colon, pretty t]
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <tff_unary_formula> ::= <unary_connective> <tff_unitary_formula> |
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <fof_infix_unary>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTFF_unary_formula :: TFF_unary_formula -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTFF_unary_formula x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa TFFUF_connective c f -> fsep [pretty c, pretty f]
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa TFFUF_infix a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <tff_atomic_formula> ::= <fof_atomic_formula>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- already has a pretty instance (FOF_atomic_formula)
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <tff_conditional> ::= $ite_f(<tff_logic_formula>,<tff_logic_formula>,
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <tff_logic_formula>)
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTFF_conditional :: TFF_conditional -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTFF_conditional x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa TFF_conditional f_if f_then f_else ->
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa text "$ite_f"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa <> parens (sepByCommas [pretty f_if, pretty f_then, pretty f_else])
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <tff_let> ::= $let_tf(<tff_let_term_defns>,<tff_formula>) |
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- $let_ff(<tff_let_formula_defns>,<tff_formula>)
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTFF_let :: TFF_let -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTFF_let x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa TFF_let_term_defns defns f ->
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa text "$let_tf"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa <> parens (sepByCommas [pretty defns, pretty f])
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa TFF_let_formula_defns defns f ->
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa text "$let_ff"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa <> parens (sepByCommas [pretty defns, pretty f])
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- %----See the commentary for <thf_let>.
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <tff_let_term_defns> ::= <tff_let_term_defn> | [<tff_let_term_list>]
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTFF_let_term_defns :: TFF_let_term_defns -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTFF_let_term_defns x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa TFFLTD_single a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa TFFLTD_many a -> brackets $ printTFF_let_term_list a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <tff_let_term_list> ::= <tff_let_term_defn> |
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <tff_let_term_defn>,<tff_let_term_list>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTFF_let_term_list :: TFF_let_term_list -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTFF_let_term_list = sepByCommas . map pretty
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <tff_let_term_defn> ::= ! [<tff_variable_list>] : <tff_let_term_defn> |
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <tff_let_term_binding>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTFF_let_term_defn :: TFF_let_term_defn -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTFF_let_term_defn x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa TFFLTD_variable vars defn ->
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa fsep [ text "!"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa , brackets (printTFF_variable_list vars) <> colon
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa , pretty defn
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa TFFLTD_binding a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <tff_let_term_binding> ::= <fof_plain_term> = <fof_term> |
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- (<tff_let_term_binding>)
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTFF_let_term_binding :: TFF_let_term_binding -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTFF_let_term_binding x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa TFFLTB_plain pt t -> fsep [pretty pt, text "=" ,pretty t]
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa TFFLTB_binding a -> parens $ pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <tff_let_formula_defns> ::= <tff_let_formula_defn> | [<tff_let_formula_list>]
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTFF_let_formula_defns :: TFF_let_formula_defns -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTFF_let_formula_defns x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa TFFLFD_single a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa TFFLFD_many a -> brackets $ printTFF_let_formula_list a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <tff_let_formula_list> ::= <tff_let_formula_defn> |
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <tff_let_formula_defn>,<tff_let_formula_list>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTFF_let_formula_list :: TFF_let_formula_list -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTFF_let_formula_list = sepByCommas . map pretty
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <tff_let_formula_defn> ::= ! [<tff_variable_list>] : <tff_let_formula_defn> |
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <tff_let_formula_binding>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTFF_let_formula_defn :: TFF_let_formula_defn -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTFF_let_formula_defn x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa TFFLFD_variable vars defn ->
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa fsep [ text "!"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa , brackets (printTFF_variable_list vars) <> colon
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa , pretty defn
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa TFFLFD_binding a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <tff_let_formula_binding> ::= <fof_plain_atomic_formula> <=>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <tff_unitary_formula> | (<tff_let_formula_binding>)
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTFF_let_formula_binding :: TFF_let_formula_binding -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTFF_let_formula_binding x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa TFFLFB_plain paf uf -> fsep [pretty paf, pretty uf]
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa TFFLFB_binding a -> parens $ pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <tff_sequent> ::= <tff_formula_tuple> <gentzen_arrow>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <tff_formula_tuple> | (<tff_sequent>)
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTFF_sequent :: TFF_sequent -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTFF_sequent x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa TFFS_plain t1 t2 -> sepBy gentzen_arrow [pretty t1, pretty t2]
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa TFFS_parens a -> parens $ pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <tff_formula_tuple> ::= [] | [<tff_formula_tuple_list>]
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTFF_formula_tuple :: TFF_formula_tuple -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTFF_formula_tuple x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa TFF_formula_tuple a -> brackets $ printTFF_formula_tuple_list a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <tff_formula_tuple_list> ::= <tff_logic_formula> |
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <tff_logic_formula>,<tff_formula_tuple_list>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTFF_formula_tuple_list :: TFF_formula_tuple_list -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTFF_formula_tuple_list = sepByCommas . map pretty
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- %----<tff_typed_atom> can appear only at top level
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <tff_typed_atom> ::= <untyped_atom> : <tff_top_level_type> |
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- (<tff_typed_atom>)
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTFF_typed_atom :: TFF_typed_atom -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTFF_typed_atom x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa TFFTA_plain ua tlt -> fsep [pretty ua <> colon, pretty tlt]
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa TFFTA_parens a -> parens $ pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <tff_subtype> ::= <untyped_atom> <subtype_sign> <atom>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTFF_subtype :: TFF_subtype -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTFF_subtype x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa TFF_subtype ua a -> fsep [pretty ua, subtype_sign, pretty a]
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- %----See <thf_top_level_type> for commentary.
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <tff_top_level_type> ::= <tff_atomic_type> | <tff_mapping_type> |
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <tf1_quantified_type> | (<tff_top_level_type>)
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTFF_top_level_type :: TFF_top_level_type -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTFF_top_level_type x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa TFFTLT_atomic a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa TFFTLT_mapping a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa TFFTLT_quantified a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa TFFTLT_parens a -> parens $ pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <tf1_quantified_type> ::= !> [<tff_variable_list>] : <tff_monotype>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTF1_quantified_type :: TF1_quantified_type -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTF1_quantified_type x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa TF1_quantified_type vars t ->
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa fsep [ text "!>"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa , brackets (printTFF_variable_list vars) <> colon
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <tff_monotype> ::= <tff_atomic_type> | (<tff_mapping_type>)
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTFF_monotype :: TFF_monotype -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTFF_monotype x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa TFFMT_atomic a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa TFFMT_mapping a -> parens $ pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <tff_unitary_type> ::= <tff_atomic_type> | (<tff_xprod_type>)
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTFF_unitary_type :: TFF_unitary_type -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTFF_unitary_type x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa TFFUT_atomic a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa TFFUT_xprod a -> parens $ pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <tff_atomic_type> ::= <type_constant> | <defined_type> |
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <type_functor>(<tff_type_arguments>) | <variable>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTFF_atomic_type :: TFF_atomic_type -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTFF_atomic_type x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa TFFAT_constant a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa TFFAT_defined a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa TFFAT_functor f args -> pretty f <> parens (printTFF_type_arguments args)
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa TFFAT_variable a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <tff_type_arguments> ::= <tff_atomic_type> |
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <tff_atomic_type>,<tff_type_arguments>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTFF_type_arguments :: TFF_type_arguments -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTFF_type_arguments = sepByCommas . map pretty
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- %----For consistency with <thf_unitary_type> (the analogue in thf),
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- %----<tff_atomic_type> should also allow (<tff_atomic_type>), but that causes
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- %----ambiguity.
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <tff_mapping_type> ::= <tff_unitary_type> <arrow> <tff_atomic_type>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTFF_mapping_type :: TFF_mapping_type -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTFF_mapping_type x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa TFF_mapping_type ut at -> fsep [pretty ut, arrow, pretty at]
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <tff_xprod_type> ::= <tff_unitary_type> <star> <tff_atomic_type> |
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <tff_xprod_type> <star> <tff_atomic_type>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTFF_xprod_type :: TFF_xprod_type -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTFF_xprod_type x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa TFF_xprod_type ut ats -> sepBy star $ pretty ut : map pretty ats
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- %----TCF formulae.
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <tcf_formula> ::= <tcf_logic_formula> | <tff_typed_atom>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTCF_formula :: TCF_formula -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTCF_formula x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa TCFF_logic a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa TCFF_atom a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <tcf_logic_formula> ::= <tcf_quantified_formula> | <cnf_formula>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTCF_logic_formula :: TCF_logic_formula -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTCF_logic_formula x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa TCFLF_quantified a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa TCFLF_cnf a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <tcf_quantified_formula> ::= ! [<tff_variable_list>] : <cnf_formula>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTCF_quantified_formula :: TCF_quantified_formula -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTCF_quantified_formula x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa TCF_quantified vars f ->
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa fsep [ text "!"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa , brackets (printTFF_variable_list vars) <> colon
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- %----FOF formulae.
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <fof_formula> ::= <fof_logic_formula> | <fof_sequent>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintFOF_formula :: FOF_formula -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintFOF_formula x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa FOFF_logic a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa FOFF_sequent a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <fof_logic_formula> ::= <fof_binary_formula> | <fof_unitary_formula>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintFOF_logic_formula :: FOF_logic_formula -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintFOF_logic_formula x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa FOFLF_binary a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa FOFLF_unitary a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- %----Future answer variable ideas | <answer_formula>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <fof_binary_formula> ::= <fof_binary_nonassoc> | <fof_binary_assoc>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintFOF_binary_formula :: FOF_binary_formula -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintFOF_binary_formula x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa FOFBF_nonassoc a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa FOFBF_assoc a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- %----Only some binary connectives are associative
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- %----There's no precedence among binary connectives
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <fof_binary_nonassoc> ::= <fof_unitary_formula> <binary_connective>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <fof_unitary_formula>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintFOF_binary_nonassoc :: FOF_binary_nonassoc -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintFOF_binary_nonassoc x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa FOF_binary_nonassoc c f1 f2 ->
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa fsep [pretty f1, pretty c, pretty f2]
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- %----Associative connectives & and | are in <binary_assoc>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <fof_binary_assoc> ::= <fof_or_formula> | <fof_and_formula>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintFOF_binary_assoc :: FOF_binary_assoc -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintFOF_binary_assoc x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa FOFBA_or a -> printFOF_or_formula a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa FOFBA_and a -> printFOF_and_formula a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <fof_or_formula> ::= <fof_unitary_formula> <vline> <fof_unitary_formula> |
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <fof_or_formula> <vline> <fof_unitary_formula>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintFOF_or_formula :: FOF_or_formula -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintFOF_or_formula = sepBy vline . map pretty
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <fof_and_formula> ::= <fof_unitary_formula> & <fof_unitary_formula> |
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <fof_and_formula> & <fof_unitary_formula>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintFOF_and_formula :: FOF_and_formula -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintFOF_and_formula = sepBy andD . map pretty
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- %----<fof_unitary_formula> are in ()s or do not have a <binary_connective> at
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- %----the top level.
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <fof_unitary_formula> ::= <fof_quantified_formula> | <fof_unary_formula> |
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <fof_atomic_formula> | (<fof_logic_formula>)
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintFOF_unitary_formula :: FOF_unitary_formula -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintFOF_unitary_formula x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa FOFUF_quantified a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa FOFUF_unary a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa FOFUF_atomic a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa FOFUF_logic a -> parens $ pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <fof_quantified_formula> ::= <fof_quantifier> [<fof_variable_list>] :
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <fof_unitary_formula>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintFOF_quantified_formula :: FOF_quantified_formula -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintFOF_quantified_formula x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa FOF_quantified_formula q vars f ->
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa fsep [ pretty q
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa , brackets (printFOF_variable_list vars) <> colon
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <fof_variable_list> ::= <variable> | <variable>,<fof_variable_list>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintFOF_variable_list :: FOF_variable_list -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintFOF_variable_list = sepByCommas . map pretty
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <fof_unary_formula> ::= <unary_connective> <fof_unitary_formula> |
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <fof_infix_unary>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintFOF_unary_formula :: FOF_unary_formula -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintFOF_unary_formula x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa FOFUF_connective c f -> fsep [pretty c, pretty f]
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa FOFUF_infix a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <fof_infix_unary> ::= <fof_term> <infix_inequality> <fof_term>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintFOF_infix_unary :: FOF_infix_unary -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintFOF_infix_unary x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa FOF_infix_unary t1 t2 -> fsep [pretty t1, infix_inequality, pretty t2]
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <fof_atomic_formula> ::= <fof_plain_atomic_formula> |
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <fof_defined_atomic_formula> |
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <fof_system_atomic_formula>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintFOF_atomic_formula :: FOF_atomic_formula -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintFOF_atomic_formula x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa FOFAT_plain a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa FOFAT_defined a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa FOFAT_system a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <fof_plain_atomic_formula> ::= <fof_plain_term>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <fof_plain_atomic_formula> :== <proposition> | <predicate>(<fof_arguments>)
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintFOF_plain_atomic_formula :: FOF_plain_atomic_formula -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintFOF_plain_atomic_formula x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa FOFPAF_proposition a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa FOFPAF_predicate p args -> pretty p <> parens (printFOF_arguments args)
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <fof_defined_atomic_formula> ::= <fof_defined_plain_formula> |
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <fof_defined_infix_formula>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintFOF_defined_atomic_formula :: FOF_defined_atomic_formula -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintFOF_defined_atomic_formula x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa FOFDAF_plain a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa FOFDAF_infix a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <fof_defined_plain_formula> ::= <fof_defined_plain_term>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <fof_defined_plain_formula> :== <defined_proposition> |
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <defined_predicate>(<fof_arguments>)
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintFOF_defined_plain_formula :: FOF_defined_plain_formula -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintFOF_defined_plain_formula x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa FOFDPF_proposition a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa FOFDPF_predicate p args -> pretty p <> parens (printFOF_arguments args)
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <fof_defined_infix_formula> ::= <fof_term> <defined_infix_pred> <fof_term>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintFOF_defined_infix_formula :: FOF_defined_infix_formula -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintFOF_defined_infix_formula x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa FOF_defined_infix_formula dip t1 t2 -> fsep [pretty t1, pretty dip, pretty t2]
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- %----System terms have system specific interpretations
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <fof_system_atomic_formula> ::= <fof_system_term>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- %----<fof_system_atomic_formula>s are used for evaluable predicates that are
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- %----available in particular tools. The predicate names are not controlled
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- %----by the TPTP syntax, so use with due care. The same is true for
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- %----<fof_system_term>s.
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintFOF_system_atomic_formula :: FOF_system_atomic_formula -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintFOF_system_atomic_formula x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa FOF_system_atomic_formula a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- %----FOF terms.
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <fof_plain_term> ::= <constant> | <functor>(<fof_arguments>)
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintFOF_plain_term :: FOF_plain_term -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintFOF_plain_term x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa FOFPT_constant a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa FOFPT_functor f args -> pretty f <> parens (printFOF_arguments args)
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- %----Defined terms have TPTP specific interpretations
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <fof_defined_term> ::= <defined_term> | <fof_defined_atomic_term>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintFOF_defined_term :: FOF_defined_term -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintFOF_defined_term x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa FOFDT_term a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa FOFDT_atomic a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <fof_defined_atomic_term> ::= <fof_defined_plain_term>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- %----None yet | <defined_infix_term>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintFOF_defined_atomic_term :: FOF_defined_atomic_term -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintFOF_defined_atomic_term x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa FOFDAT_plain a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa -- | FOFDAT_indix a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- %----None yet <defined_infix_term> ::= <fof_term> <defined_infix_func> <fof_term>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- data Defined_infix_term = Defined_infix_term Defined_infix_func FOF_term FOF_term
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- deriving (Show, Ord, Eq, Data, Typeable)
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- %----None yet <defined_infix_func> ::=
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- data Defined_infix_func =
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <fof_defined_plain_term> ::= <defined_constant> |
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <defined_functor>(<fof_arguments>)
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- %----Add $tuple for tuples, because [<fof_arguments>] doesn't work.
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintFOF_defined_plain_term :: FOF_defined_plain_term -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintFOF_defined_plain_term x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa FOFDPT_constant a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa FOFDPT_functor f args -> pretty f <> parens (printFOF_arguments args)
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- %----System terms have system specific interpretations
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <fof_system_term> ::= <system_constant> | <system_functor>(<fof_arguments>)
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintFOF_system_term :: FOF_system_term -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintFOF_system_term x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa FOFST_constant a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa FOFST_functor f args -> pretty f <> parens (printFOF_arguments args)
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- %----Arguments recurse back up to terms (this is the FOF world here)
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <fof_arguments> ::= <fof_term> | <fof_term>,<fof_arguments>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintFOF_arguments :: FOF_arguments -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintFOF_arguments = sepByCommas . map pretty
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- %----These are terms used as arguments. Not the entry point for terms because
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- %----<fof_plain_term> is also used as <fof_plain_atomic_formula>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <fof_term> ::= <fof_function_term> | <variable> |
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <tff_conditional_term> | <tff_let_term>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintFOF_term :: FOF_term -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintFOF_term x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa FOFT_function a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa FOFT_variable a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa FOFT_conditional a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa FOFT_let a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- %% DAMN THIS JUST WON'T WORK | <tuple_term>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- %----<tuple_term> is for TFF only, but it's here because it's used in
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- %----<fof_atomic_formula>, which is also used as <tff_atomic_formula>.
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- % <tuple_term> ::= [] | [<fof_arguments>]
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <fof_function_term> ::= <fof_plain_term> | <fof_defined_term> |
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <fof_system_term>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintFOF_function_term :: FOF_function_term -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintFOF_function_term x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa FOFFT_plain a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa FOFFT_defined a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa FOFFT_system a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- %----Conditional terms should be used by only TFF.
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <tff_conditional_term> ::= $ite_t(<tff_logic_formula>,<fof_term>,<fof_term>)
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTFF_conditional_term :: TFF_conditional_term -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTFF_conditional_term x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa TFF_conditional_term f_if t_then t_else ->
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa text "$ite_t"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa <> parens (sepByCommas [pretty f_if, pretty t_then, pretty t_else])
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- %----Let terms should be used by only TFF. $let_ft is for use when there is
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- %----a $ite_t in the <fof_term>. See the commentary for $let_tf and $let_ff.
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <tff_let_term> ::= $let_ft(<tff_let_formula_defns>,<fof_term>) |
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- $let_tt(<tff_let_term_defns>,<fof_term>)
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTFF_let_term :: TFF_let_term -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTFF_let_term x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa TFFLT_formula defns t ->
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa text "$let_ft" <> parens (sepByCommas [pretty defns, pretty t])
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa TFFLT_term defns t ->
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa text "$let_tt" <> parens (sepByCommas [pretty defns, pretty t])
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa%----This section is the FOFX syntax. Not yet in use.
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa% <fof_let> ::= := [<fof_let_list>] : <fof_unitary_formula>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa% <fof_let_list> ::= <fof_defined_var> |
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa% <fof_defined_var>,<fof_let_list>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa% <fof_defined_var> ::= <variable> := <fof_logic_formula> |
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa% <variable> :- <fof_term> | (<fof_defined_var>)
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa% <fof_conditional> ::= $ite_f(<fof_logic_formula>,<fof_logic_formula>,
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa% <fof_logic_formula>)
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa% <fof_conditional_term> ::= $ite_t(<fof_logic_formula>,<fof_term>,<fof_term>)
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <fof_sequent> ::= <fof_formula_tuple> <gentzen_arrow>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <fof_formula_tuple> | (<fof_sequent>)
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintFOF_sequent :: FOF_sequent -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintFOF_sequent x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa FOFS_plain t1 t2 -> fsep [pretty t1, gentzen_arrow, pretty t2]
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa FOFS_parens a -> parens $ pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <fof_formula_tuple> ::= [] | [<fof_formula_tuple_list>]
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintFOF_formula_tuple :: FOF_formula_tuple -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintFOF_formula_tuple x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa FOF_formula_tuple a -> brackets $ printFOF_formula_tuple_list a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <fof_formula_tuple_list> ::= <fof_logic_formula> |
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <fof_logic_formula>,<fof_formula_tuple_list>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintFOF_formula_tuple_list :: FOF_formula_tuple_list -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintFOF_formula_tuple_list = sepByCommas . map pretty
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- %----CNF formulae (variables implicitly universally quantified)
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <cnf_formula> ::= <disjunction> | (<disjunction>)
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintCNF_formula :: CNF_formula -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintCNF_formula x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa CNFF_plain a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa CNFF_parens a -> parens $ pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <disjunction> ::= <literal> | <disjunction> <vline> <literal>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintDisjunction :: Disjunction -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintDisjunction x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa Disjunction ls -> sepBy vline $ map pretty ls
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <literal> ::= <fof_atomic_formula> | ~ <fof_atomic_formula> |
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <fof_infix_unary>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintLiteral :: Literal -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintLiteral x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa Lit_atomic a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa Lit_negative a -> text "~" <+> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa Lit_fof_infix a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- %----Connectives - THF
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <thf_quantifier> ::= <fof_quantifier> | <th0_quantifier> |
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <th1_quantifier>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTHF_quantifier :: THF_quantifier -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTHF_quantifier x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa THFQ_fof a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa THFQ_th0 a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa THFQ_th1 a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- %----TH0 quantifiers are also available in TH1
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <th1_quantifier> ::= !> | ?*
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTH1_quantifier :: TH1_quantifier -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTH1_quantifier x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa TH1_DependentProduct -> text "!>"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa TH1_DependentSum -> text "?*"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <th0_quantifier> ::= ^ | @+ | @-
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTH0_quantifier :: TH0_quantifier -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTH0_quantifier x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa TH0_LambdaBinder -> text "^"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa TH0_IndefiniteDescription -> text "@+"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa TH0_DefiniteDescription -> text "@-"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <thf_pair_connective> ::= <infix_equality> | <infix_inequality> |
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <binary_connective> | <assignment>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTHF_pair_connective :: THF_pair_connective -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTHF_pair_connective x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa THF_infix_equality -> infix_equality
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa Infix_inequality -> infix_inequality
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa THFPC_binary a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa THF_assignment -> assignment
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <thf_unary_connective> ::= <unary_connective> | <th1_unary_connective>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTHF_unary_connective :: THF_unary_connective -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTHF_unary_connective x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa THFUC_unary a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa THFUC_th1 a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <th1_unary_connective> ::= !! | ?? | @@+ | @@- | @=
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTH1_unary_connective :: TH1_unary_connective -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTH1_unary_connective x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa TH1_PiForAll -> text "!!"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa TH1_PiSigmaExists -> text "??"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa TH1_PiIndefiniteDescription -> text "@@+"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa TH1_PiDefiniteDescription -> text "@@-"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa TH1_PiEquality -> text "@="
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- %----Connectives - TFF
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- % <tff_pair_connective> ::= <binary_connective> | <assignment>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- Note: not used
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- data TFF_pair_connective = TFFPC_binary Binary_connective
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- | TFFPC_assignment TFF_assignment
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- deriving (Show, Ord, Eq, Data, Typeable)
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <subtype_sign> ::= <less_sign><less_sign>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksasubtype_sign :: Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksasubtype_sign = less_sign <> less_sign
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- %----Connectives - FOF
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <fof_quantifier> ::= ! | ?
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintFOF_quantifier :: FOF_quantifier -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintFOF_quantifier x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa ForAll -> text "!"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa Exists -> text "?"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <binary_connective> ::= <=> | => | <= | <~> | ~<vline> | ~&
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintBinary_connective :: Binary_connective -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintBinary_connective x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa Equivalence -> text "<=>"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa Implication -> text "=>"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa ReverseImplication -> text "<="
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa XOR -> text "<~>"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa NOR -> text "~|"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa NAND -> text "~&"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <assoc_connective> ::= <vline> | &
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintAssoc_connective :: Assoc_connective -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintAssoc_connective x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa OR -> text "|"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa AND -> text "&"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <unary_connective> ::= ~
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintUnary_connective :: Unary_connective -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintUnary_connective x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa NOT -> text "~"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- %----Types for THF and TFF
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <type_constant> ::= <type_functor>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- already has a pretty instance (Token)
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <type_functor> ::= <atomic_word>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- already has a pretty instance (Token)
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <defined_type> ::= <atomic_defined_word>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <defined_type> :== $oType | $o | $iType | $i | $tType |
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- $real | $rat | $int
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintDefined_type :: Defined_type -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintDefined_type x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa OType -> text "$oType"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa O -> text "$o"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa IType -> text "$iType"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa I -> text "$i"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa TType -> text "$tType"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa Real -> text "$real"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa Rat -> text "$rat"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa Int -> text "$int"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <system_type> :== <atomic_system_word>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- Note: not used
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- type System_type = Token
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- %----For all language types
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <atom> ::= <untyped_atom> | <defined_constant>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintAtom :: Atom -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintAtom x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa Atom_untyped a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa Atom_constant a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <untyped_atom> ::= <constant> | <system_constant>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintUntyped_atom :: Untyped_atom -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintUntyped_atom x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa UA_constant a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa UA_system a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- Proposition
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- already has a pretty instance (Token)
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- already has a pretty instance (Token)
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <defined_proposition> :== <atomic_defined_word>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <defined_proposition> :== $true | $false
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintDefined_proposition :: Defined_proposition -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintDefined_proposition x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa TPTP_true -> text "$true"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa TPTP_false -> text "$false"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <defined_predicate> :== <atomic_defined_word>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <defined_predicate> :== $distinct |
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- $less | $lesseq | $greater | $greatereq |
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- $is_int | $is_rat |
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- $box_P | $box_i | $box_int | $box |
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- $dia_P | $dia_i | $dia_int | $dia
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- %----$distinct means that each of it's constant arguments are pairwise !=. It
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- %----is part of the TFF syntax. It can be used only as a fact, not under any
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- %----connective.
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintDefined_predicate :: Defined_predicate -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintDefined_predicate x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa Distinct -> text "$distinct"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa Less -> text "$less"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa Lesseq -> text "$lesseq"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa Greater -> text "$greater"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa Greatereq -> text "$greatereq"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa Is_int -> text "$is_int"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa Is_rat -> text "$is_rat"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa Box_P -> text "$box_P"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa Box_i -> text "$box_i"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa Box_int -> text "$box_int"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa Box -> text "$box"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa Dia_P -> text "$dia_P"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa Dia_i -> text "$dia_i"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa Dia_int -> text "$dia_int"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa Dia -> text "$dia"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <defined_infix_pred> ::= <infix_equality> | <assignment>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <infix_equality> ::= =
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <infix_inequality> ::= !=
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintDefined_infix_pred :: Defined_infix_pred -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintDefined_infix_pred x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa Defined_infix_equality -> infix_equality
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa Defined_assignment -> assignment
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <constant> ::= <functor>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- already has a pretty instance (Token)
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <functor> ::= <atomic_word>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- already has a pretty instance (Token)
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <system_constant> ::= <system_functor>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- already has a pretty instance (Token)
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <system_functor> ::= <atomic_system_word>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- already has a pretty instance (Token)
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <defined_constant> ::= <defined_functor>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- already has a pretty instance (Token)
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <defined_functor> ::= <atomic_defined_word>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <defined_functor> :== $uminus | $sum | $difference | $product |
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- $quotient | $quotient_e | $quotient_t | $quotient_f |
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- $remainder_e | $remainder_t | $remainder_f |
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- $floor | $ceiling | $truncate | $round |
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- $to_int | $to_rat | $to_real
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintDefined_functor :: Defined_functor -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintDefined_functor x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa Uminus -> text "$uminus"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa Sum -> text "$sum"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa Difference -> text "$difference"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa Product -> text "$product"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa Quotient -> text "$quotient"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa Quotient_e -> text "$quotient_e"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa Quotient_t -> text "$quotient_t"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa Quotient_f -> text "$quotient_f"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa Remainder_e -> text "$remainder_e"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa Remainder_t -> text "$remainder_t"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa Remainder_f -> text "$remainder_f"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa Floor -> text "$floor"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa Ceiling -> text "$ceiling"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa Truncate -> text "$truncate"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa Round -> text "$round"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa To_int -> text "$to_int"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa To_rat -> text "$to_rat"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa To_real -> text "$to_real"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa DF_atomic_defined_word a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <defined_term> ::= <number> | <distinct_object>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintDefined_term :: Defined_term -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintDefined_term x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa DT_number a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa DT_object a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <variable> ::= <upper_word>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- already has a pretty instance (Token)
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- %----Formula sources
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <source> ::= <general_term>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <source> :== <dag_source> | <internal_source> |
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <external_source> | unknown | [<sources>]
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintSource :: Source -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintSource x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa Source_DAG a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa Source_internal a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa Source_external a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa Unknown_source -> text "unknown"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa Source_many a -> brackets $ printSources a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- %----Alternative sources are recorded like this, thus allowing representation
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- %----of alternative derivations with shared parts.
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <sources> :== <source> | <source>,<sources>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintSources :: Sources -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintSources = sepByCommas . map pretty
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- %----Only a <dag_source> can be a <name>, i.e., derived formulae can be
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- %----identified by a <name> or an <inference_record>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <dag_source> :== <name> | <inference_record>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintDAG_source :: DAG_source -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintDAG_source x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa DAGS_name a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa DAGS_record a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <inference_record> :== inference(<inference_rule>,<useful_info>,
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <inference_parents>)
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintInference_record :: Inference_record -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintInference_record x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa Inference_record ir ui ip ->
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa text "inference"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa <> parens (sepByCommas [pretty ir, pretty ui, printInference_parents ip])
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <inference_rule> :== <atomic_word>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- %----Examples are deduction | modus_tollens | modus_ponens | rewrite |
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- % resolution | paramodulation | factorization |
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- % cnf_conversion | cnf_refutation | ...
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintInference_rule :: Inference_rule -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintInference_rule = pretty
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- %----<inference_parents> can be empty in cases when there is a justification
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- %----for a tautologous theorem. In case when a tautology is introduced as
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- %----a leaf, e.g., for splitting, then use an <internal_source>.
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <inference_parents> :== [] | [<parent_list>]
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintInference_parents :: Inference_parents -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintInference_parents = brackets . printParent_list
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <parent_list> :== <parent_info> | <parent_info>,<parent_list>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintParent_list :: Parent_list -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintParent_list = sepByCommas . map pretty
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <parent_info> :== <source><parent_details>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintParent_info :: Parent_info -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintParent_info x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa Parent_info s d -> fsep [pretty s, printParent_details d]
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <parent_details> :== :<general_list> | <null>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintParent_details :: Parent_details -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintParent_details x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa Just gl -> printGeneral_list gl
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa Nothing -> empty
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <internal_source> :== introduced(<intro_type><optional_info>)
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintInternal_source :: Internal_source -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintInternal_source x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa Internal_source it oi ->
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa text "introduced" <> parens (fsep [pretty it, pretty oi])
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <intro_type> :== definition | axiom_of_choice | tautology | assumption
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- %----This should be used to record the symbol being defined, or the function
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- %----for the axiom of choice
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintIntro_type :: Intro_type -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintIntro_type x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa IntroTypeDefinition -> text "definition"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa AxiomOfChoice -> text "axiom_of_choice"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa Tautology -> text "tautology"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa IntroTypeAssumption -> text "assumption"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <external_source> :== <file_source> | <theory> | <creator_source>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintExternal_source :: External_source -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintExternal_source x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa ExtSrc_file a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa ExtSrc_theory a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa ExtSrc_creator a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <file_source> :== file(<file_name><file_info>)
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintFile_source :: File_source -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintFile_source x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa File_source fn fi ->
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa text "file" <> parens (fsep [text "'" <> pretty fn <> text "'",
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa printFile_info fi])
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <file_info> :== ,<name> | <null>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintFile_info :: File_info -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintFile_info x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa Just n -> fsep [comma, text "'" <> pretty n <> text "'"]
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa Nothing -> empty
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <theory> :== theory(<theory_name><optional_info>)
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTheory :: Theory -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTheory x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa Theory tn oi -> text "theory" <> parens (fsep [pretty tn, pretty oi])
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <theory_name> :== equality | ac
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTheory_name :: Theory_name -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintTheory_name x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa TN_equality -> text "equality"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa TN_ac -> text "ac"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- %----More theory names may be added in the future. The <optional_info> is
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- %----used to store, e.g., which axioms of equality have been implicitly used,
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- %----e.g., theory(equality,[rst]). Standard format still to be decided.
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <creator_source> :== creator(<creator_name><optional_info>)
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintCreator_source :: Creator_source -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintCreator_source x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa Creator_source cn oi ->
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa text "creator" <> parens (fsep [printCreator_name cn, pretty oi])
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <creator_name> :== <atomic_word>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintCreator_name :: Creator_name -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintCreator_name = pretty
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- %----Useful info fields
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <optional_info> ::= ,<useful_info> | <null>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintOptional_info :: Optional_info -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintOptional_info x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa Just ui -> comma <+> pretty ui
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa Nothing -> empty
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <useful_info> ::= <general_list>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <useful_info> :== [] | [<info_items>]
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintUseful_info :: Useful_info -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintUseful_info x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa UI_items a -> brackets $ printInfo_items a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa UI_general_list a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <info_items> :== <info_item> | <info_item>,<info_items>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintInfo_items :: Info_items -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintInfo_items = sepByCommas . map pretty
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <info_item> :== <formula_item> | <inference_item> |
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <general_function>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintInfo_item :: Info_item -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintInfo_item x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa Info_formula a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa Info_inference a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa Info_general a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- %----Useful info for formula records
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <formula_item> :== <description_item> | <iquote_item>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintFormula_item :: Formula_item -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintFormula_item x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa FI_description a -> printDescription_item a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa FI_iquote a -> printIquote_item a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <description_item> :== description(<atomic_word>)
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintDescription_item :: Description_item -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintDescription_item a = text "description" <> parens (pretty a)
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <iquote_item> :== iquote(<atomic_word>)
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- %----<iquote_item>s are used for recording exactly what the system output about
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- %----the inference step. In the future it is planned to encode this information
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- %----in standardized forms as <parent_details> in each <inference_record>.
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- %----Useful info for inference records
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintIquote_item :: Iquote_item -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintIquote_item a = text "iquote" <> parens (pretty a)
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <inference_item> :== <inference_status> | <assumptions_record> |
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <new_symbol_record> | <refutation>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintInference_item :: Inference_item -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintInference_item x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa Inf_status a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa Inf_assumption a -> printAssumptions_record a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa Inf_symbol a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa Inf_refutation a -> printRefutation a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <inference_status> :== status(<status_value>) | <inference_info>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintInference_status :: Inference_status -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintInference_status x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa Inf_value a -> text "status" <> parens (pretty a)
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa Inf_info a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- %----These are the success status values from the SZS ontology. The most
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- %----commonly used values are:
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- %---- thm - Every model of the parent formulae is a model of the inferred
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- %---- formula. Regular logical consequences.
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- %---- cth - Every model of the parent formulae is a model of the negation of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- %---- the inferred formula. Used for negation of conjectures in FOF to
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- %---- CNF conversion.
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- %---- esa - There exists a model of the parent formulae iff there exists a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- %---- model of the inferred formula. Used for Skolemization steps.
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- %----For the full hierarchy see the SZSOntology file distributed with the TPTP.
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <status_value> :== suc | unp | sap | esa | sat | fsa | thm | eqv | tac |
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- wec | eth | tau | wtc | wth | cax | sca | tca | wca |
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- cup | csp | ecs | csa | cth | ceq | unc | wcc | ect |
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- fun | uns | wuc | wct | scc | uca | noc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintStatus_value :: Status_value -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintStatus_value x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa SUC -> text "suc"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa UNP -> text "unp"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa SAP -> text "sap"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa ESA -> text "esa"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa SAT -> text "sat"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa FSA -> text "fsa"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa THM -> text "thm"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa EQV -> text "eqv"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa TAC -> text "tac"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa WEC -> text "wec"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa ETH -> text "eth"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa TAU -> text "tau"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa WTC -> text "wtc"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa WTH -> text "wth"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa CAX -> text "cax"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa SCA -> text "sca"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa TCA -> text "tca"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa WCA -> text "wca"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa CUP -> text "cup"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa CSP -> text "csp"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa ECS -> text "ecs"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa CSA -> text "csa"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa CTH -> text "cth"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa CEQ -> text "ceq"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa UNC -> text "unc"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa WCC -> text "wcc"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa ECT -> text "ect"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa FUN -> text "fun"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa UNS -> text "uns"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa WUC -> text "wuc"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa WCT -> text "wct"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa SCC -> text "scc"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa UCA -> text "uca"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa NOC -> text "noc"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- %----<inference_info> is used to record standard information associated with an
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- %----arbitrary inference rule. The <inference_rule> is the same as the
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- %----<inference_rule> of the <inference_record>. The <atomic_word> indicates
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- %----the information being recorded in the <general_list>. The <atomic_word>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- %----are (loosely) set by TPTP conventions, and include esplit, sr_split, and
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- %----discharge.
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <inference_info> :== <inference_rule>(<atomic_word>,<general_list>)
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintInference_info :: Inference_info -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintInference_info x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa Inference_info ir aw gl ->
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa printInference_rule ir
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa <> parens (sepByCommas [pretty aw, printGeneral_list gl])
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- %----An <assumptions_record> lists the names of assumptions upon which this
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- %----inferred formula depends. These must be discharged in a completed proof.
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <assumptions_record> :== assumptions([<name_list>])
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintAssumptions_record :: Assumptions_record -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintAssumptions_record x =
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa text "assumptions" <> parens (brackets $ printName_list x)
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- %----A <refutation> record names a file in which the inference recorded here
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- %----is recorded as a proof by refutation.
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <refutation> :== refutation(<file_source>)
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintRefutation :: Refutation -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintRefutation a = text "refutation" <> parens (printFile_source a)
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- %----A <new_symbol_record> provides information about a newly introduced symbol.
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <new_symbol_record> :== new_symbols(<atomic_word>,[<new_symbol_list>])
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintNew_symbol_record :: New_symbol_record -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintNew_symbol_record x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa New_symbol_record aw nsl ->
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa text "new_symbols"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa <> parens (sepByCommas [pretty aw, brackets $ printNew_symbol_list nsl])
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <new_symbol_list> :== <principal_symbol> |
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <principal_symbol>,<new_symbol_list>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintNew_symbol_list :: New_symbol_list -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintNew_symbol_list = sepByCommas . map pretty
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- %----Principal symbols are predicates, functions, variables
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <principal_symbol> :== <functor> | <variable>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintPrincipal_symbol :: Principal_symbol -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintPrincipal_symbol x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa PS_functor a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa PS_variable a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- %----Include directives
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <include> ::= include(<file_name><formula_selection>).
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintInclude :: Include -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintInclude x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa Include fn fs ->
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa text "include" <> parens (fsep [pretty fn, printFormula_selection fs])
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <formula_selection> ::= ,[<name_list>] | <null>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintFormula_selection :: Formula_selection -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintFormula_selection x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa Just ns -> fsep [comma, brackets $ printName_list ns]
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa Nothing -> empty
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <name_list> ::= <name> | <name>,<name_list>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintName_list :: Name_list -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintName_list = sepByCommas . map pretty
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- %----Non-logical data
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <general_term> ::= <general_data> | <general_data>:<general_term> |
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <general_list>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintGeneral_term :: General_term -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintGeneral_term x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa GT_data a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa GT_DataTerm gd gt -> fsep [pretty gd <> colon, pretty gt]
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa GT_list a -> printGeneral_list a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <general_data> ::= <atomic_word> | <general_function> |
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <variable> | <number> | <distinct_object> |
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <formula_data>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintGeneral_data :: General_data -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintGeneral_data x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa GD_atomic_word a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa GD_general_function a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa GD_variable a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa GD_number a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa GD_distinct_object a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa GD_formula_data a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- %----A <general_data> bind() term is used to record a variable binding in an
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- %----inference, as an element of the <parent_details> list.
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <general_data> :== bind(<variable>,<formula_data>)
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa GD_bind v fd -> text "bind" <> parens (sepByCommas [pretty v, pretty fd])
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <general_function> ::= <atomic_word>(<general_terms>)
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintGeneral_function :: General_function -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintGeneral_function x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa General_function aw gt -> pretty aw <> parens (printGeneral_terms gt)
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <formula_data> ::= $thf(<thf_formula>) | $tff(<tff_formula>) |
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- $fof(<fof_formula>) | $cnf(<cnf_formula>) |
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- $fot(<fof_term>)
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- only used in inference
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintFormula_data :: Formula_data -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintFormula_data x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa FD_THF a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa FD_TFF a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa FD_FOF a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa FD_CNF a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa FD_FOT a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <general_list> ::= [] | [<general_terms>]
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintGeneral_list :: General_list -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintGeneral_list = brackets . pretty
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <general_terms> ::= <general_term> | <general_term>,<general_terms>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintGeneral_terms :: General_terms -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintGeneral_terms = sepByCommas . map pretty
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- %----General purpose
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <name> ::= <atomic_word> | <integer>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- %----Integer names are expected to be unsigned
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintName :: Name -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintName x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa NameString a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa NameInteger a -> pretty a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <atomic_word> ::= <lower_word> | <single_quoted>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- already has a pretty instance (Token)
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <atomic_defined_word> ::= <dollar_word>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- already has a pretty instance (Token)
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <atomic_system_word> ::= <dollar_dollar_word>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- already has a pretty instance (Token)
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <number> ::= <integer> | <rational> | <real>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintNumber :: Number -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintNumber x = case x of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa NumInteger a -> text $ show a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa NumRational a -> text $ show a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa NumReal a -> text $ show a
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <distinct_object> ::- <double_quote><do_char>*<double_quote>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- already has a pretty instance (Token)
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <file_name> ::= <single_quoted>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- already has a pretty instance (IRI)
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa{- -----------------------------------------------------------------------------
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaTokens used in syntax
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa----------------------------------------------------------------------------- -}
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <gentzen_arrow> ::= -->
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksagentzen_arrow :: Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksagentzen_arrow = text "-->"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <assignment> ::= :=
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksaassignment :: Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksaassignment = text ":="
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <infix_equality> ::= =
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainfix_equality :: Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainfix_equality = text "="
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa-- <infix_inequality> ::= !=
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainfix_inequality :: Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksainfix_inequality = text "!="
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksavline = text "|"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksastar = text "*"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksaplus = text "+"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksaarrow = text ">"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksaless_sign :: Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksaless_sign = text "<"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaandD = text "&"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaatD = text "@"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa{- -----------------------------------------------------------------------------
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaTokens used in syntax
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa----------------------------------------------------------------------------- -}
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksasepBy :: Doc -> [Doc] -> Doc
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksasepBy delimiter items = case items of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa _ -> fsep $ tail $ concatMap (\ i -> [delimiter, i]) items