diff --git a/Codec/TPTP/Base.hs b/Codec/TPTP/Base.hs
--- a/Codec/TPTP/Base.hs
+++ b/Codec/TPTP/Base.hs
@@ -320,6 +320,13 @@
       [] -> cnf
       vars -> for_all vars cnf
 
+-- | Universally quantify all free variables in the formula
+univquant_free_vars_FC :: FormulaC -> FormulaC
+univquant_free_vars_FC cnf =
+    case S.toList (freeVars (forgetFC cnf)) of
+      [] -> cnf
+      vars -> for_all vars cnf
+
 instance FreeVars Formula where
     freeVars = foldF
                freeVars
diff --git a/Parser.y b/Parser.y
--- a/Parser.y
+++ b/Parser.y
@@ -70,23 +70,23 @@
 
 %%
 
-TPTP_file  :: {[TPTP_Input_ c]}
+TPTP_file  :: {[TPTP_Input]}
 TPTP_file  : {[]} | TPTP_input TPTP_file  {$1 : $2}
 
-TPTP_input  :: {TPTP_Input_ c}
+TPTP_input  :: {TPTP_Input}
 TPTP_input  : annotated_formula  {$1}
              | include  { $1 }
              | comment { Comment $1 }
 
-annotated_formula  :: {TPTP_Input_ c}
+annotated_formula  :: {TPTP_Input}
 annotated_formula  :  fof_annotated  {$1}
                     | cnf_annotated  {$1}
 
-fof_annotated  :: {TPTP_Input_ c}
+fof_annotated  :: {TPTP_Input}
 fof_annotated  : fof lp name  comma formula_role  comma fof_formula  annotations  rp dot
        { AFormula        $3               $5                $7           $8 }
 
-cnf_annotated  :: {TPTP_Input_ c}
+cnf_annotated  :: {TPTP_Input}
 cnf_annotated  : cnf lp name  comma formula_role  comma cnf_formula  annotations  rp dot
        { AFormula          $3              $5  (univquant_free_vars $7) $8 }
 
@@ -99,38 +99,38 @@
 formula_role  : lower_word_ { Role $1 }
 
 
-fof_formula  :: {F c}
+fof_formula  :: {Formula}
 fof_formula  : binary_formula  { $1 }
               | unitary_formula  { $1 }
 
-binary_formula  :: {F c}
+binary_formula  :: {Formula}
 binary_formula  : nonassoc_binary  {$1}
                  | assoc_binary  {$1}
 
-nonassoc_binary  :: {F c}
+nonassoc_binary  :: {Formula}
 nonassoc_binary  : unitary_formula  binary_connective  unitary_formula
                   { $2 $1 $3 }
 
 
-assoc_binary  :: {F c}
+assoc_binary  :: {Formula}
 assoc_binary  : or_formula  { $1 }
                | and_formula  { $1 }
 
 
-or_formula  :: {F c}
+or_formula  :: {Formula}
 or_formula  : unitary_formula   vline  unitary_formula  more_or_formula
                { L.foldl (.|.) ($1 .|. $3) $4 }
 
-more_or_formula  :: {[F c]}
+more_or_formula  :: {[Formula]}
 more_or_formula  : {[]} | vline  unitary_formula more_or_formula
                   { $2 : $3 }
 
-and_formula  :: {F c}
+and_formula  :: {Formula}
 and_formula  : unitary_formula  ampersand unitary_formula  more_and_formula
                { L.foldl (.&.) ($1 .&. $3) $4 }
 
 
-more_and_formula  :: {[F c]}
+more_and_formula  :: {[Formula]}
 more_and_formula  : {[]} | ampersand unitary_formula more_and_formula
                    { $2 : $3 }
 
@@ -140,7 +140,7 @@
                   | atomic_formula      {$1}
                   | lp fof_formula  rp  {$2}
 
-quantified_formula  :: {F c}
+quantified_formula  :: {Formula}
 quantified_formula  : quantifier  lbra variable_list  rbra colon unitary_formula
                      { $1 $3 $6 }
 
@@ -148,7 +148,7 @@
 variable_list  : variable  { [$1] }
                 | variable  comma variable_list  { $1 : $3 }
 
-unary_formula  :: {F c}
+unary_formula  :: {Formula}
 unary_formula  : unary_connective  unitary_formula  { $1 $2 }
                 | fol_infix_unary  { $1 }
 
@@ -159,16 +159,16 @@
 -- cnf_formula : assoc_binary {$1}
 --             | lp assoc_binary rp {$2}
 
-cnf_formula  :: {F c}
+cnf_formula  :: {Formula}
 cnf_formula  :  lp disjunction  rp  { $2 }
               | disjunction  { $1 }
 
 
-disjunction  :: {F c}
+disjunction  :: {Formula}
 disjunction  : literal  more_disjunction
               { L.foldl (.|.) $1 $2 }
 
-more_disjunction  :: {[F c]}
+more_disjunction  :: {[Formula]}
 more_disjunction  :  {[]} | vline  literal more_disjunction
                    { $2 : $3 }
 
@@ -177,7 +177,7 @@
           | tilde atomic_formula  { (.~.) $2}
           | fol_infix_unary  {$1}
 
-fol_infix_unary  :: {F c}
+fol_infix_unary  :: {Formula}
 fol_infix_unary  : term  infix_inequality  term  { $2 $1 $3 }
 
 quantifier :: {[V] -> Formula -> Formula}
@@ -202,24 +202,24 @@
 -- defined_type  :== $oType | $o | $iType | $i | $tType | $real | $int
 -- system_type  :== atomic_system_word
 
-atomic_formula  :: {F c}
+atomic_formula  :: {Formula}
 atomic_formula  :  plain_atomic_formula    {$1}
                  | defined_atomic_formula  {$1}
                  | system_atomic_formula   {$1}
 
 
-plain_atomic_formula  :: {F c}
+plain_atomic_formula  :: {Formula}
 plain_atomic_formula  : plain_term  { fApp2pApp $1 }
 
 -- plain_atomic_formula  :== proposition  | predicate  lp arguments  rp
 -- proposition  :== predicate
 -- predicate  :== atomic_word
 
-defined_atomic_formula  :: {F c}
+defined_atomic_formula  :: {Formula}
 defined_atomic_formula  :  defined_plain_formula  {$1}
                          | defined_infix_formula  {$1}
 
-defined_plain_formula  :: {F c}
+defined_plain_formula  :: {Formula}
 defined_plain_formula  : defined_plain_term  {fApp2pApp $1}
 
 --defined_plain_formula  :== defined_prop  | defined_pred  lp arguments  rp
@@ -229,10 +229,10 @@
 --defined_pred  :== $equal
 
 
-defined_infix_formula  :: {F c}
+defined_infix_formula  :: {Formula}
 defined_infix_formula  : term  defined_infix_pred  term  { $2 $1 $3 }
 
-defined_infix_pred :: { T c -> T c -> F c }
+defined_infix_pred :: {  Term -> Term -> Formula }
 defined_infix_pred  : infix_equality  { $1 }
 
 infix_equality  :: { Term -> Term -> Formula }
@@ -241,7 +241,7 @@
 infix_inequality  :: { Term -> Term -> Formula }
 infix_inequality  : nequals { (.!=.) }
 
-system_atomic_formula  :: {F c}
+system_atomic_formula  :: {Formula}
 system_atomic_formula  : system_term  {fApp2pApp $1}
 
 term  :: {Term}
@@ -300,7 +300,7 @@
 variable  :: {V}
 variable  : upper_word {V $1}
 
-arguments  :: {[T c]}
+arguments  :: {[Term]}
 arguments  : term  {[$1]}
             | term  comma arguments  { $1 : $3 }
 
diff --git a/ParserC.y b/ParserC.y
--- a/ParserC.y
+++ b/ParserC.y
@@ -71,25 +71,25 @@
 
 %%
 
-TPTP_file  :: {[TPTP_Input_ c]}
+TPTP_file  :: {[TPTP_Input_C]}
 TPTP_file  : {[]} | TPTP_input TPTP_file  {$1 : $2}
 
-TPTP_input  :: {TPTP_Input_ c}
+TPTP_input  :: {TPTP_Input_C}
 TPTP_input  : annotated_formula  {$1}
              | include  { $1 }
              | comment { Comment $1 }
 
-annotated_formula  :: {TPTP_Input_ c}
+annotated_formula  :: {TPTP_Input_C}
 annotated_formula  :  fof_annotated  {$1}
                     | cnf_annotated  {$1}
 
-fof_annotated  :: {TPTP_Input_ c}
+fof_annotated  :: {TPTP_Input_C}
 fof_annotated  : fof lp name  comma formula_role  comma fof_formula  annotations  rp dot
        { AFormula        $3               $5                $7           $8 }
 
-cnf_annotated  :: {TPTP_Input}
+cnf_annotated  :: {TPTP_Input_C}
 cnf_annotated  : cnf lp name  comma formula_role  comma cnf_formula  annotations  rp dot
-       { AFormula          $3              $5  (univquant_free_vars $7) $8 }
+       { AFormula          $3              $5  (univquant_free_vars_FC $7) $8 }
 
 
 annotations  :: { Annotations }
@@ -100,38 +100,38 @@
 formula_role  : lower_word_ { Role $1 }
 
 
-fof_formula  :: {F c}
+fof_formula  :: {FormulaC}
 fof_formula  : binary_formula  { $1 }
               | unitary_formula  { $1 }
 
-binary_formula  :: {F c}
+binary_formula  :: {FormulaC}
 binary_formula  : nonassoc_binary  {$1}
                  | assoc_binary  {$1}
 
-nonassoc_binary  :: {F c}
+nonassoc_binary  :: {FormulaC}
 nonassoc_binary  : unitary_formula  binary_connective  unitary_formula
                   { $2 $1 $3 }
 
 
-assoc_binary  :: {F c}
+assoc_binary  :: {FormulaC}
 assoc_binary  : or_formula  { $1 }
                | and_formula  { $1 }
 
 
-or_formula  :: {F c}
+or_formula  :: {FormulaC}
 or_formula  : unitary_formula   vline  unitary_formula  more_or_formula
                { L.foldl (.|.) ($1 .|. $3) $4 }
 
-more_or_formula  :: {[F c]}
+more_or_formula  :: {[FormulaC]}
 more_or_formula  : {[]} | vline  unitary_formula more_or_formula
                   { $2 : $3 }
 
-and_formula  :: {F c}
+and_formula  :: {FormulaC}
 and_formula  : unitary_formula  ampersand unitary_formula  more_and_formula
                { L.foldl (.&.) ($1 .&. $3) $4 }
 
 
-more_and_formula  :: {[F c]}
+more_and_formula  :: {[FormulaC]}
 more_and_formula  : {[]} | ampersand unitary_formula more_and_formula
                    { $2 : $3 }
 
@@ -141,7 +141,7 @@
                   | atomic_formula      {$1}
                   | lp fof_formula  rp  {$2}
 
-quantified_formula  :: {F c}
+quantified_formula  :: {FormulaC}
 quantified_formula  : quantifier  lbra variable_list  rbra colon unitary_formula
                      { $1 $3 $6 `withComments` comm $5 }
 
@@ -149,7 +149,7 @@
 variable_list  : variable  { [$1] }
                 | variable  comma variable_list  { $1 : $3 }
 
-unary_formula  :: {F c}
+unary_formula  :: {FormulaC}
 unary_formula  : unary_connective  unitary_formula  { $1 $2 }
                 | fol_infix_unary  { $1 }
 
@@ -160,16 +160,16 @@
 -- cnf_formula : assoc_binary {$1}
 --             | lp assoc_binary rp {$2}
 
-cnf_formula  :: {F c}
+cnf_formula  :: {FormulaC}
 cnf_formula  :  lp disjunction  rp  { $2 }
               | disjunction  { $1 }
 
 
-disjunction  :: {F c}
+disjunction  :: {FormulaC}
 disjunction  : literal  more_disjunction
               { L.foldl (.|.) $1 $2 }
 
-more_disjunction  :: {[F c]}
+more_disjunction  :: {[FormulaC]}
 more_disjunction  :  {[]} | vline  literal more_disjunction
                    { $2 : $3 }
 
@@ -178,7 +178,7 @@
           | tilde atomic_formula  { (.~.) $2}
           | fol_infix_unary  {$1}
 
-fol_infix_unary  :: {F c}
+fol_infix_unary  :: {FormulaC}
 fol_infix_unary  : term  infix_inequality  term  { $2 $1 $3 }
 
 quantifier :: {[V] -> FormulaC -> FormulaC}
@@ -203,24 +203,24 @@
 -- defined_type  :== $oType | $o | $iType | $i | $tType | $real | $int
 -- system_type  :== atomic_system_word
 
-atomic_formula  :: {F c}
+atomic_formula  :: {FormulaC}
 atomic_formula  :  plain_atomic_formula    {$1}
                  | defined_atomic_formula  {$1}
                  | system_atomic_formula   {$1}
 
 
-plain_atomic_formula  :: {F c}
+plain_atomic_formula  :: {FormulaC}
 plain_atomic_formula  : plain_term  { fApp2pApp $1 }
 
 -- plain_atomic_formula  :== proposition  | predicate  lp arguments  rp
 -- proposition  :== predicate
 -- predicate  :== atomic_word
 
-defined_atomic_formula  :: {F c}
+defined_atomic_formula  :: {FormulaC}
 defined_atomic_formula  :  defined_plain_formula  {$1}
                          | defined_infix_formula  {$1}
 
-defined_plain_formula  :: {F c}
+defined_plain_formula  :: {FormulaC}
 defined_plain_formula  : defined_plain_term  {fApp2pApp $1}
 
 --defined_plain_formula  :== defined_prop  | defined_pred  lp arguments  rp
@@ -230,10 +230,10 @@
 --defined_pred  :== $equal
 
 
-defined_infix_formula  :: {F c}
+defined_infix_formula  :: {FormulaC}
 defined_infix_formula  : term  defined_infix_pred  term  { $2 $1 $3 }
 
-defined_infix_pred :: { T c -> T c -> F c }
+defined_infix_pred :: { TermC -> TermC -> FormulaC }
 defined_infix_pred  : infix_equality  { $1 }
 
 infix_equality  :: { TermC -> TermC -> FormulaC }
@@ -242,7 +242,7 @@
 infix_inequality  :: { TermC -> TermC -> FormulaC }
 infix_inequality  : nequals { (.!=.) }
 
-system_atomic_formula  :: {F c}
+system_atomic_formula  :: {FormulaC}
 system_atomic_formula  : system_term  {fApp2pApp $1}
 
 term  :: {TermC}
@@ -273,7 +273,7 @@
 defined_atom  : number {numberLitTerm $1}
                | distinct_object {distinctObjectTerm (stripQuotes '"' $1)}
 
-defined_atomic_term :: {T c}
+defined_atomic_term :: {TermC}
 defined_atomic_term  : defined_plain_term {$1}
 
 defined_plain_term  :: {TermC}
@@ -301,7 +301,7 @@
 variable  :: {V}
 variable  : upper_word {V $1}
 
-arguments  :: {[T c]}
+arguments  :: {[TermC]}
 arguments  : term  {[$1]}
             | term  comma arguments  { $1 : $3 }
 
@@ -347,7 +347,7 @@
 -- assumptions_record  :== assumptions lp [name_list ] rp
 -- refutation  :== refutation lp file_source  rp
 
-include :: {TPTP_Input_ c}
+include :: {TPTP_Input_C}
 include  : include_ lp file_name formula_selection  rp dot { Include $3 $4 }
 
 formula_selection  :: {[AtomicWord]}
@@ -373,7 +373,7 @@
                | formula_data  { $1 }
 
 formula_data :: {GData}
-formula_data  : dollar_word lp fof_formula  rp { GFormulaData $1 $3 }
+formula_data  : dollar_word lp fof_formula  rp { GFormulaData $1 (forgetFC $3) }
               -- too ambiguous | dollar_word lp cnf_formula  rp { GFormulaData $1 $3 }
 
 general_list  :: {[GTerm]}
@@ -511,6 +511,7 @@
                         go ('\\':which:xs) = which:go xs
                         go (x:xs) = x:go xs
 
-fApp2pApp (T mf) = F $ do FunApp x args <- mf
-                          return $ PredApp x args
+fApp2pApp (T mf) = F $ do x <- mf
+                          case x of
+                            FunApp x args -> return $ PredApp x args
 }
diff --git a/logic-TPTP.cabal b/logic-TPTP.cabal
--- a/logic-TPTP.cabal
+++ b/logic-TPTP.cabal
@@ -1,10 +1,10 @@
 name: logic-TPTP
-version: 0.4.6.0
-cabal-version: >= 1.6
+version: 0.4.7.0
+cabal-version: >= 1.8
 build-type: Simple
 license: GPL
 license-file: LICENSE
-maintainer: Ahn, Ki Yung <kya@pdx.edu>, Daniel Schüssler <daniels@community.haskell.org>
+maintainer: Ahn, Ki Yung <kya@pdx.edu>, Daniel Schüssler <daniels@community.haskell.org>, Masahiro Sakai <masahiro.sakai@gmail.com>
 bug-reports: http://github.com/DanielSchuessler/logic-TPTP/issues
 synopsis: Import, export etc. for TPTP, a syntax for first-order logic
 description:
@@ -35,22 +35,27 @@
 category: Codec,Math,Theorem Provers
 author: Daniel Schüssler
 extra-source-files: testing/compileTests.sh
-                    testing/TestImportExportRandom.hs
-                    testing/TestImportExportImportFile.hs
-                    testing/PrettyPrintFile.hs
-                    testing/ParseRandom.hs
                     changelog.markdown
 
-tested-with: GHC==7.4.1
-tested-with: GHC==7.2.1
-tested-with: GHC==7.0.4
+tested-with: GHC==8.8.2
+tested-with: GHC==8.6.4
+tested-with: GHC==8.4.4
+tested-with: GHC==8.2.2
+tested-with: GHC==8.0.2
+tested-with: GHC==7.10.3
+tested-with: GHC==7.8.4
 
 source-repository head
  type: git
  location: http://github.com/DanielSchuessler/logic-TPTP.git
 
 
+Flag BuildTestPrograms
+  description: build test programs
+  default: False
+  manual: True
 
+
 Library
  ghc-options: -Wall -O2
 
@@ -81,3 +86,81 @@
                   , Util
 
  build-tools: alex >= 3.1.1, happy >= 1.19.1
+
+
+Executable TestImportExportImportFile
+ main-is:           TestImportExportImportFile.hs
+ other-modules:     Common
+                  , SimpleArgs
+ hs-source-dirs:    testing
+ build-depends:     logic-TPTP
+                  , base
+                  , ansi-wl-pprint
+                  , pcre-light
+                  , semigroups
+ if impl(ghc <7.10)
+  build-depends:    pcre-light <0.4.1
+ other-extensions:  CPP
+ if !flag(BuildTestPrograms)
+  buildable: False
+
+Test-suite TestImportExportRandom
+ type:              exitcode-stdio-1.0
+ main-is:           TestImportExportRandom.hs
+ other-modules:     Common
+ hs-source-dirs:    testing
+ build-depends:     logic-TPTP
+                  , base
+                  , ansi-wl-pprint
+                  , pcre-light
+                  , QuickCheck
+                  , semigroups
+                  , transformers
+                  , transformers-compat >= 0.5
+ if impl(ghc <7.10)
+  build-depends:    pcre-light <0.4.1
+ other-extensions:  CPP
+
+Executable PrettyPrintFile
+ main-is:           PrettyPrintFile.hs
+ other-modules:     Common
+                  , SimpleArgs
+ hs-source-dirs:    testing
+ build-depends:     logic-TPTP
+                  , ansi-wl-pprint
+                  , base
+                  , bytestring
+                  , containers
+                  , mtl
+                  , pcre-light
+                  , process
+                  , QuickCheck
+                  , semigroups
+                  , syb
+ if impl(ghc <7.10)
+  build-depends:    pcre-light <0.4.1
+ other-extensions:  CPP
+ if !flag(BuildTestPrograms)
+  buildable: False
+
+Executable ParseRandom
+ main-is:           ParseRandom.hs
+ other-modules:     Common
+                  , SimpleArgs
+ hs-source-dirs:    testing
+ build-depends:     logic-TPTP
+                  , ansi-wl-pprint
+                  , base
+                  , bytestring
+                  , containers
+                  , mtl
+                  , pcre-light
+                  , process
+                  , QuickCheck
+                  , semigroups
+                  , syb
+ if impl(ghc <7.10)
+  build-depends:    pcre-light <0.4.1
+ other-extensions:  CPP
+ if !flag(BuildTestPrograms)
+  buildable: False
diff --git a/testing/Common.hs b/testing/Common.hs
new file mode 100644
--- /dev/null
+++ b/testing/Common.hs
@@ -0,0 +1,55 @@
+{-# OPTIONS_GHC -Wall #-}
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE FlexibleContexts #-}
+
+module Common where
+
+import Data.Monoid
+import qualified Data.Semigroup as Semigroup
+import Text.PrettyPrint.ANSI.Leijen
+import Text.Regex.PCRE.Light.Char8
+import Codec.TPTP
+
+
+data AFormulaComparison = OtherSame | OtherDiff String String | FormulaDiff (F DiffResult)
+
+instance Semigroup.Semigroup AFormulaComparison where
+    -- keep the most interesting comparison result
+    (<>) OtherSame y = y
+    (<>) x OtherSame = x
+    (<>) x@(OtherDiff _ _) y@(FormulaDiff (F y0)) = if isSame y0 then y else x
+    (<>) x@(FormulaDiff (F x0)) y@(OtherDiff _ _) = if isSame x0 then x else y
+    (<>) x@(OtherDiff _ _) (OtherDiff _ _) = x
+    (<>) x@(FormulaDiff _ ) (FormulaDiff _ ) = x
+
+instance Monoid AFormulaComparison where
+    mempty = OtherSame
+#if !MIN_VERSION_base(4,11,0)
+    mappend = (Semigroup.<>)
+#endif
+
+instance Pretty AFormulaComparison where
+    pretty (OtherSame) = dullgreen.text$"OtherSame"
+    pretty (OtherDiff x y) = sep
+                             [dullred.text$"OtherDiff"
+                             ,pretty x
+                             ,pretty y
+                             ]
+    pretty (FormulaDiff fd) = pretty fd
+
+compareOther ::  (Eq a, Show a) => a -> a -> AFormulaComparison
+compareOther x y = if x==y then OtherSame else OtherDiff (show x) (show y)
+
+diffAFormula :: (Eq (t (Formula0 (T t) (F t))),Show (t (Formula0 (T t) (F t))),Diffable (F t) (F DiffResult)) =>TPTP_Input_ t -> TPTP_Input_ t -> AFormulaComparison
+diffAFormula (AFormula a b c d) (AFormula a1 b1 c1 d1) =
+    mconcat [ compareOther a a1
+            , compareOther b b1
+            , FormulaDiff (diff c c1)
+            , compareOther d d1
+            ]
+diffAFormula x y = compareOther x y
+
+findUnsupportedFormulaType ::  String -> Maybe String
+findUnsupportedFormulaType =
+    let re = compile "^(thf|tff)\\(" [multiline]
+    in (\x -> (!!1) `fmap` match re x [])
diff --git a/testing/ParseRandom.hs b/testing/ParseRandom.hs
--- a/testing/ParseRandom.hs
+++ b/testing/ParseRandom.hs
@@ -1,22 +1,12 @@
-{-# OPTIONS
- -fglasgow-exts
- -XCPP
- -XTemplateHaskell
- -XNamedFieldPuns
- -XRecordWildCards
- -XDeriveDataTypeable
- -XOverlappingInstances
- -XPackageImports
- -fwarn-incomplete-patterns
- #-}
+{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
+{-# LANGUAGE PackageImports #-}
 
-module ParseRandom where
+module Main where
 
 import Control.Monad
 import Control.Monad.State
 import Control.Applicative((<$>),(<*>))
 import Control.Arrow
-import Text.Printf.TH
 import Data.Maybe
 import Data.List as L
 import Data.Map as M
@@ -26,7 +16,6 @@
 import System.Process
 import Control.Arrow
 import Debug.Trace
-import System.SimpleArgs
 import Data.Generics
 import Test.QuickCheck
 import Data.Monoid
@@ -34,6 +23,7 @@
 import System.Exit
 import Text.Regex.PCRE.Light.Char8
 import Common
+import SimpleArgs
 
 import "logic-TPTP" Codec.TPTP
 
diff --git a/testing/PrettyPrintFile.hs b/testing/PrettyPrintFile.hs
--- a/testing/PrettyPrintFile.hs
+++ b/testing/PrettyPrintFile.hs
@@ -1,22 +1,12 @@
-{-# OPTIONS
- -fglasgow-exts
- -XCPP
- -XTemplateHaskell
- -XNamedFieldPuns
- -XRecordWildCards
- -XDeriveDataTypeable
- -XOverlappingInstances
- -XPackageImports
- -fwarn-incomplete-patterns
- #-}
+{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
+{-# LANGUAGE PackageImports #-}
 
-module PrettyPrintFile where
+module Main where
 
 import Control.Monad
 import Control.Monad.State
 import Control.Applicative((<$>),(<*>))
 import Control.Arrow
-import Text.Printf.TH
 import Data.Maybe
 import Data.List as L
 import Data.Map as M
@@ -27,7 +17,6 @@
 import System.IO
 import Control.Arrow
 import Debug.Trace
-import System.SimpleArgs
 import Data.Generics
 import Test.QuickCheck
 import Data.Monoid
@@ -36,6 +25,6 @@
 import Text.Regex.PCRE.Light.Char8
 
 import "logic-TPTP" Codec.TPTP
-
+import SimpleArgs
 
 main = putStrLn . prettySimple . parse =<< readFile =<< getArgs
diff --git a/testing/SimpleArgs.hs b/testing/SimpleArgs.hs
new file mode 100644
--- /dev/null
+++ b/testing/SimpleArgs.hs
@@ -0,0 +1,84 @@
+{-# LANGUAGE FlexibleInstances, UndecidableInstances, OverlappingInstances #-}
+
+-- Copied and modified from https://hackage.haskell.org/package/simpleargs-0.2.1
+-- which is licensed under GNU LESSER GENERAL PUBLIC LICENSE Version 2.1
+
+-- | Provide a @getArgs@ function that is slightly more advanced than the default, without
+--   going the entire @System.Console.GetOpt@ route.
+--
+--   The idea is to return a tuple (including the 0-tuple @()@ or 1-tuple)
+--   if the supplied arguments match the demands of the program (in number and in type)
+--   or a sensible error message if not.
+--   The returned tuple must contain elements that are in the @Typeable@ and @Read@ classes.
+--
+-- As an examle, here's a simple line counting program. 
+-- Here @getArgs@ makes the program take a single parameter, and returns it
+-- as a @String@:
+--
+-- > main = getArgs >>= readFile >>= print . length . lines
+--
+-- This program will take two parameters, a @Char@ and a @String@:
+--
+-- > main = do
+-- >    (ch,name) <- getArgs
+-- >    putStrLn (ch:"Name is: "++name)
+--
+
+module SimpleArgs (Args, getArgs) where
+
+import qualified System.Environment as S (getArgs)
+import Data.Typeable (Typeable, typeOf)
+
+class Args a where
+    -- | Return appropriately typed program arguments.
+    getArgs :: IO a
+
+argerror :: Typeable a => Int -> [String] -> a
+argerror n xs = let ret = error ("Incorrect number of arguments, got "++show (length xs)++",\n"
+                                ++"expected "++show n ++ " "++show (typeOf ret))
+                in ret
+
+instance Args () where
+    getArgs = S.getArgs >>= return . g
+        where g [] = ()
+              g xs = argerror 0 xs
+
+instance (Read b, Typeable b) => Args b where
+    getArgs = S.getArgs >>= return . g
+        where g [x] = myread x
+              g xs = argerror 1 xs
+
+instance (Read x, Typeable x, Read y, Typeable y) => Args (x,y) where
+    getArgs = S.getArgs >>= return . g
+        where g [x1,x2] = (myread x1,myread x2)
+              g xs = argerror 2 xs
+
+instance (Read t1, Typeable t1,Read t2, Typeable t2,Read t3, Typeable t3) => Args (t1,t2,t3) where
+    getArgs = S.getArgs >>= return . g
+        where g [x1,x2,x3] = (myread x1,myread x2,myread x3)
+              g xs = argerror 3 xs
+
+instance (Read t1,Typeable t1,Read t2,Typeable t2,Read t3,Typeable t3,Read t4,Typeable t4) => Args (t1,t2,t3,t4) where
+    getArgs = S.getArgs >>= return . g
+        where g [x1,x2,x3,x4] = (myread x1,myread x2,myread x3,myread x4)
+              g xs = argerror 4 xs
+
+instance (Read t1,Typeable t1,Read t2,Typeable t2,Read t3,Typeable t3,Read t4,Typeable t4,Read t5,Typeable t5) => Args (t1,t2,t3,t4,t5) where
+    getArgs = S.getArgs >>= return . g
+        where g [x1,x2,x3,x4,x5] = (myread x1,myread x2,myread x3,myread x4,myread x5)
+              g xs = argerror 5 xs
+
+-- | Attempt to parse the parameter as various types
+myread :: (Typeable a, Read a) => String -> a
+myread s = let ret = case map reads [s,sq s,dq s,lq s] of
+                       ([(x,"")]:_) -> x
+                       (_:[(c,"")]:_) -> c
+                       (_:_:[(str,"")]:_) -> str
+                       (_:_:_:[(l,"")]:_) -> l
+                       _ -> error ("Couldn't parse parameter "++show s++" as type "++show (typeOf ret)++".")
+           in ret
+    where
+      -- different types of quoting
+      sq x = "'"++x++"'"
+      dq x = "\""++x++"\""
+      lq x = "["++x++"]"
diff --git a/testing/TestImportExportImportFile.hs b/testing/TestImportExportImportFile.hs
--- a/testing/TestImportExportImportFile.hs
+++ b/testing/TestImportExportImportFile.hs
@@ -1,17 +1,13 @@
-{-# OPTIONS -Wall #-}
+{-# OPTIONS_GHC -Wall #-}
 {-# LANGUAGE PackageImports #-}
-module TestImportExportImportFile where
+module Main where
 
 import Control.Monad
-import Data.Maybe
-import Data.List as L
-import Data.Function
-import System.IO
-import System.SimpleArgs
 import Data.Monoid
 import Text.PrettyPrint.ANSI.Leijen
 import System.Exit
 import Common
+import SimpleArgs
 
 import "logic-TPTP" Codec.TPTP
 
diff --git a/testing/TestImportExportRandom.hs b/testing/TestImportExportRandom.hs
--- a/testing/TestImportExportRandom.hs
+++ b/testing/TestImportExportRandom.hs
@@ -1,9 +1,7 @@
-{-# OPTIONS -Wall #-}
+{-# OPTIONS_GHC -Wall #-}
 {-# LANGUAGE PackageImports #-}
-module TestImportExportRandom where
+module Main where
 
-import Data.Function
-import System.IO
 import Test.QuickCheck
 import Common
 import Data.Functor.Identity