{-# LANGUAGE DeriveDataTypeable #-}

module Options (Args(..),TypeSystem(..),options) where

import System.Console.CmdArgs.Implicit
import System.IO.Unsafe

data TypeSystem = CCω
                | Predicative
  deriving (Show, Data, Typeable)

data Args = 
  Args {verb :: Int,
        typeSystem :: TypeSystem,
        showSorts :: Bool,
        files :: [String]
        } 
  deriving (Show, Data, Typeable)
           
sample = cmdArgsMode $ 
         Args { verb = 0 &= help "verbosity" &= opt (0 :: Int),
                typeSystem = enum [Predicative &= name "P" &= help "Agda (Predicative)", 
                                   CCω &= name "I" &= help "CCω (Impredicative)"]
                               , -- &= opt (0 :: Int),
                showSorts = False &= help "display sort annotations in normal forms",
                files = [] &= args &= typFile
              }
         
         
options = unsafePerformIO (cmdArgsRun sample)