logic-TPTP 0.4.6.0 → 0.4.7.0

raw patch · 10 files changed

+313/−110 lines, 10 filesdep +bytestringdep +logic-TPTPdep +pcre-lightdep ~QuickCheckdep ~ansi-wl-pprintdep ~basenew-component:exe:ParseRandomnew-component:exe:PrettyPrintFilenew-component:exe:TestImportExportImportFilenew-uploaderPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependencies added: bytestring, logic-TPTP, pcre-light, process

Dependency ranges changed: QuickCheck, ansi-wl-pprint, base, mtl

API changes (from Hackage documentation)

Files

• Codec/TPTP/Base.hs +7/−0
• Parser.y +27/−27
• ParserC.y +34/−33
• logic-TPTP.cabal +93/−10
• testing/Common.hs +55/−0
• testing/ParseRandom.hs +4/−14
• testing/PrettyPrintFile.hs +4/−15
• testing/SimpleArgs.hs +84/−0
• testing/TestImportExportImportFile.hs +3/−7
• testing/TestImportExportRandom.hs +2/−4

@@ -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

@@ -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 } 

@@ -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 }

@@ -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

@@ -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 [])

@@ -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 

@@ -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

@@ -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++"]"

@@ -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 

@@ -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