diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,4 @@
+This software is in the public domain.  Permission to use,  copy, modify,  and
+distribute this software and its documentation for any purpose and without fee
+is hereby granted,  without any conditions or restrictions.   This software is
+provided "as is" without expressed or implied warranty.
diff --git a/README b/README
new file mode 100644
--- /dev/null
+++ b/README
@@ -0,0 +1,35 @@
+
+  DESCRIPTION
+
+This application is a shell-based user interface to the free-theorems
+library. It allows to generate free theorems for nearly any Haskell
+type expression including user-defined data types and type classes.
+See the description of the free-theorems library for the restrictions.
+
+
+
+  DEPENDENCIES
+
+See the file `ftshell.cabal' for dependencies. The dependency on 
+Shellac-readline may be dropped  which needs small changes in the
+file `src/Settings.hs'.
+
+
+  
+  INSTALL
+
+Since this application is cabalised, it uses the standard installation
+process.
+  
+  runhaskell Setup.lhs configure
+  runhaskell Setup.lhs build
+  runhaskell Setup.lhs install
+
+
+
+  USAGE
+
+Start the application by entering `ftshell'. Further information is
+provided by the application itself.
+
+
diff --git a/Setup.lhs b/Setup.lhs
new file mode 100644
--- /dev/null
+++ b/Setup.lhs
@@ -0,0 +1,4 @@
+#!/usr/bin/env runhaskell
+
+> import Distribution.Simple
+> main = defaultMain
diff --git a/declarations.hs b/declarations.hs
new file mode 100644
--- /dev/null
+++ b/declarations.hs
@@ -0,0 +1,299 @@
+
+-- Haskell module `Prelude'
+
+data Bool = False | True
+(&&) :: Bool -> Bool -> Bool
+(||) :: Bool -> Bool -> Bool
+not :: Bool -> Bool
+otherwise :: Bool
+data Maybe a = Nothing | Just a
+maybe :: b -> (a -> b) -> Maybe a -> b
+data Either a b = Left a | Right b
+either :: (a -> c) -> (b -> c) -> Either a b -> c
+data Ordering = LT | EQ | GT
+type String = [Char]
+fst :: (a, b) -> a
+snd :: (a, b) -> b
+curry :: ((a, b) -> c) -> a -> b -> c
+uncurry :: (a -> b -> c) -> (a, b) -> c
+class Eq a where
+  (==) :: a -> a -> Bool
+  (/=) :: a -> a -> Bool
+class Eq a => Ord a where
+  compare :: a -> a -> Ordering
+  (<) :: a -> a -> Bool
+  (<=) :: a -> a -> Bool
+  (>) :: a -> a -> Bool
+  (>=) :: a -> a -> Bool
+max :: a -> a -> a
+min :: a -> a -> a
+class Enum a where
+  succ :: a -> a
+  pred :: a -> a
+  toEnum :: Int -> a
+  fromEnum :: a -> Int
+  enumFrom :: a -> [a]
+  enumFromThen :: a -> a -> [a]
+  enumFromTo :: a -> a -> [a]
+  enumFromThenTo :: a -> a -> a -> [a]
+class Bounded a where
+  minBound :: a
+  maxBound :: a
+type Rational = Ratio Integer
+class (Eq a, Show a) => Num a where
+  (+) :: a -> a -> a
+  (-) :: a -> a -> a
+  (*) :: a -> a -> a
+  negate :: a -> a
+  abs :: a -> a
+  signum :: a -> a
+  fromInteger :: Integer -> a
+class (Num a, Ord a) => Real a where
+  toRational :: a -> Rational
+class (Real a, Enum a) => Integral a where
+  quot :: a -> a -> a
+  rem :: a -> a -> a
+  div :: a -> a -> a
+  mod :: a -> a -> a
+  quotRem :: a -> a -> (a, a)
+  divMod :: a -> a -> (a, a)
+  toInteger :: a -> Integer
+class Num a => Fractional a where
+  (/) :: a -> a -> a
+  recip :: a -> a
+  fromRational :: Rational -> a
+class Fractional a => Floating a where
+  pi :: a
+  exp :: a -> a
+  log :: a -> a
+  sqrt :: a -> a
+  (**) :: a -> a -> a
+  logBase :: a -> a -> a
+  sin :: a -> a
+  cos :: a -> a
+  tan :: a -> a
+  asin :: a -> a
+  acos :: a -> a
+  atan :: a -> a
+  sinh :: a -> a
+  cosh :: a -> a
+  tanh :: a -> a
+  asinh :: a -> a
+  acosh :: a -> a
+  atanh :: a -> a
+class (Real a, Fractional a) => RealFrac a where
+  properFraction :: Integral b => a -> (b, a)
+  truncate :: Integral b => a -> b
+  round :: Integral b => a -> b
+  ceiling :: Integral b => a -> b
+  floor :: Integral b => a -> b
+class (RealFrac a, Floating a) => RealFloat a where
+  floatRadix :: a -> Integer
+  floatDigits :: a -> Int
+  floatRange :: a -> (Int, Int)
+  decodeFloat :: a -> (Integer, Int)
+  encodeFloat :: Integer -> Int -> a
+  exponent :: a -> Int
+  significand :: a -> a
+  scaleFloat :: Int -> a -> a
+  isNaN :: a -> Bool
+  isInfinite :: a -> Bool
+  isDenormalized :: a -> Bool
+  isNegativeZero :: a -> Bool
+  isIEEE :: a -> Bool
+  atan2 :: a -> a -> a
+subtract :: Num a => a -> a -> a
+even :: Integral a => a -> Bool
+odd :: Integral a => a -> Bool
+gcd :: Integral a => a -> a -> a
+lcm :: Integral a => a -> a -> a
+(^) :: (Num a, Integral b) => a -> b -> a
+(^^) :: (Fractional a, Integral b) => a -> b -> a
+fromIntegral :: (Integral a, Num b) => a -> b
+realToFrac :: (Real a, Fractional b) => a -> b
+id :: a -> a
+const :: a -> b -> a
+(.) :: (b -> c) -> (a -> b) -> a -> c
+flip :: (a -> b -> c) -> b -> a -> c
+($) :: (a -> b) -> a -> b
+until :: (a -> Bool) -> (a -> a) -> a -> a
+asTypeOf :: a -> a -> a
+error :: String -> a
+undefined :: a
+seq :: a -> b -> b
+($!) :: (a -> b) -> a -> b
+map :: (a -> b) -> [a] -> [b]
+(++) :: [a] -> [a] -> [a]
+filter :: (a -> Bool) -> [a] -> [a]
+head :: [a] -> a
+last :: [a] -> a
+tail :: [a] -> [a]
+init :: [a] -> [a]
+null :: [a] -> Bool
+length :: [a] -> Int
+(!!) :: [a] -> Int -> a
+reverse :: [a] -> [a]
+foldl :: (a -> b -> a) -> a -> [b] -> a
+foldl1 :: (a -> a -> a) -> [a] -> a
+foldr :: (a -> b -> b) -> b -> [a] -> b
+foldr1 :: (a -> a -> a) -> [a] -> a
+and :: [Bool] -> Bool
+or :: [Bool] -> Bool
+any :: (a -> Bool) -> [a] -> Bool
+all :: (a -> Bool) -> [a] -> Bool
+sum :: Num a => [a] -> a
+product :: Num a => [a] -> a
+concat :: [[a]] -> [a]
+concatMap :: (a -> [b]) -> [a] -> [b]
+maximum :: Ord a => [a] -> a
+minimum :: Ord a => [a] -> a
+scanl :: (a -> b -> a) -> a -> [b] -> [a]
+scanl1 :: (a -> a -> a) -> [a] -> [a]
+scanr :: (a -> b -> b) -> b -> [a] -> [b]
+scanr1 :: (a -> a -> a) -> [a] -> [a]
+iterate :: (a -> a) -> a -> [a]
+repeat :: a -> [a]
+replicate :: Int -> a -> [a]
+cycle :: [a] -> [a]
+take :: Int -> [a] -> [a]
+drop :: Int -> [a] -> [a]
+splitAt :: Int -> [a] -> ([a], [a])
+takeWhile :: (a -> Bool) -> [a] -> [a]
+dropWhile :: (a -> Bool) -> [a] -> [a]
+span :: (a -> Bool) -> [a] -> ([a], [a])
+break :: (a -> Bool) -> [a] -> ([a], [a])
+elem :: Eq a => a -> [a] -> Bool
+notElem :: Eq a => a -> [a] -> Bool
+lookup :: Eq a => a -> [(a, b)] -> Maybe b
+zip :: [a] -> [b] -> [(a, b)]
+zip3 :: [a] -> [b] -> [c] -> [(a, b, c)]
+zipWith :: (a -> b -> c) -> [a] -> [b] -> [c]
+zipWith3 :: (a -> b -> c -> d) -> [a] -> [b] -> [c] -> [d]
+unzip :: [(a, b)] -> ([a], [b])
+unzip3 :: [(a, b, c)] -> ([a], [b], [c])
+lines :: String -> [String]
+words :: String -> [String]
+unlines :: [String] -> String
+unwords :: [String] -> String
+type ShowS = String -> String
+class Show a where
+  showsPrec :: Int -> a -> ShowS
+  show :: a -> String
+  showList :: [a] -> ShowS
+shows :: Show a => a -> ShowS
+showChar :: Char -> ShowS
+showString :: String -> ShowS
+showParen :: Bool -> ShowS -> ShowS
+type ReadS a = String -> [(a, String)]
+class Read a where
+  readsPrec :: Int -> ReadS a
+  readList :: ReadS [a]
+reads :: Read a => ReadS a
+readParen :: Bool -> ReadS a -> ReadS a
+read :: Read a => String -> a
+lex :: ReadS String
+type FilePath = String
+
+
+
+-- Haskell module `Data.Complex'
+
+data Complex a = !a :+ !a
+realPart :: RealFloat a => Complex a -> a
+imagPart :: RealFloat a => Complex a -> a
+mkPolar :: RealFloat a => a -> a -> Complex a
+cis :: RealFloat a => a -> Complex a
+polar :: RealFloat a => Complex a -> (a, a)
+magnitude :: RealFloat a => Complex a -> a
+phase :: RealFloat a => Complex a -> a
+conjugate :: RealFloat a => Complex a -> Complex a
+
+
+
+-- Haskell module `Data.List'
+
+
+intersperse :: a -> [a] -> [a]
+transpose :: [[a]] -> [[a]]
+foldl' :: (a -> b -> a) -> a -> [b] -> a
+foldl1' :: (a -> a -> a) -> [a] -> a
+mapAccumL :: (acc -> x -> (acc, y)) -> acc -> [x] -> (acc, [y])
+mapAccumR :: (acc -> x -> (acc, y)) -> acc -> [x] -> (acc, [y])
+unfoldr :: (b -> Maybe (a, b)) -> b -> [a]
+group :: Eq a => [a] -> [[a]]
+inits :: [a] -> [[a]]
+tails :: [a] -> [[a]]
+isPrefixOf :: Eq a => [a] -> [a] -> Bool
+isSuffixOf :: Eq a => [a] -> [a] -> Bool
+find :: (a -> Bool) -> [a] -> Maybe a
+partition :: (a -> Bool) -> [a] -> ([a], [a])
+zip4 :: [a] -> [b] -> [c] -> [d] -> [(a, b, c, d)]
+zip5 :: [a] -> [b] -> [c] -> [d] -> [e] -> [(a, b, c, d, e)]
+zip6 :: [a] -> [b] -> [c] -> [d] -> [e] -> [f] -> [(a, b, c, d, e, f)]
+zip7 :: [a] -> [b] -> [c] -> [d] -> [e] -> [f] -> [g] -> [(a, b, c, d, e, f, g)]
+zipWith4 :: (a -> b -> c -> d -> e) -> [a] -> [b] -> [c] -> [d] -> [e]
+zipWith5 :: (a -> b -> c -> d -> e -> f) -> [a] -> [b] -> [c] -> [d] -> [e] -> [f]
+zipWith6 :: (a -> b -> c -> d -> e -> f -> g) -> [a] -> [b] -> [c] -> [d] -> [e] -> [f] -> [g]
+zipWith7 :: (a -> b -> c -> d -> e -> f -> g -> h) -> [a] -> [b] -> [c] -> [d] -> [e] -> [f] -> [g] -> [h]
+unzip4 :: [(a, b, c, d)] -> ([a], [b], [c], [d])
+unzip5 :: [(a, b, c, d, e)] -> ([a], [b], [c], [d], [e])
+unzip6 :: [(a, b, c, d, e, f)] -> ([a], [b], [c], [d], [e], [f])
+unzip7 :: [(a, b, c, d, e, f, g)] -> ([a], [b], [c], [d], [e], [f], [g])
+nub :: Eq a => [a] -> [a]
+delete :: Eq a => a -> [a] -> [a]
+(\\) :: Eq a => [a] -> [a] -> [a]
+union :: Eq a => [a] -> [a] -> [a]
+intersect :: Eq a => [a] -> [a] -> [a]
+sort :: Ord a => [a] -> [a]
+insert :: Ord a => a -> [a] -> [a]
+nubBy :: (a -> a -> Bool) -> [a] -> [a]
+deleteBy :: (a -> a -> Bool) -> a -> [a] -> [a]
+deleteFirstsBy :: (a -> a -> Bool) -> [a] -> [a] -> [a]
+unionBy :: (a -> a -> Bool) -> [a] -> [a] -> [a]
+intersectBy :: (a -> a -> Bool) -> [a] -> [a] -> [a]
+groupBy :: (a -> a -> Bool) -> [a] -> [[a]]
+sortBy :: (a -> a -> Ordering) -> [a] -> [a]
+insertBy :: (a -> a -> Ordering) -> a -> [a] -> [a]
+maximumBy :: (a -> a -> Ordering) -> [a] -> a
+minimumBy :: (a -> a -> Ordering) -> [a] -> a
+genericLength :: Num i => [b] -> i
+genericTake :: Integral i => i -> [a] -> [a]
+genericDrop :: Integral i => i -> [a] -> [a]
+genericSplitAt :: Integral i => i -> [b] -> ([b], [b])
+genericIndex :: Integral a => [b] -> a -> b
+genericReplicate :: Integral i => i -> a -> [a]
+
+
+
+-- Haskell module `Data.Maybe'
+
+isJust :: Maybe a -> Bool
+isNothing :: Maybe a -> Bool
+fromJust :: Maybe a -> a
+fromMaybe :: a -> Maybe a -> a
+listToMaybe :: [a] -> Maybe a
+maybeToList :: Maybe a -> [a]
+catMaybes :: [Maybe a] -> [a]
+mapMaybe :: (a -> Maybe b) -> [a] -> [b]
+
+
+
+-- Haskell module `Data.Monoid'
+
+class Monoid a where
+  mempty :: a
+  mappend :: a -> a -> a
+  mconcat :: [a] -> a
+
+
+
+-- Haskell module `Data.Ratio'
+
+data Ratio a = !a :% !a
+(%) :: Integral a => a -> a -> Ratio a
+numerator :: Integral a => Ratio a -> a
+denominator :: Integral a => Ratio a -> a
+approxRational :: RealFrac a => a -> a -> Rational
+
+
+
diff --git a/ftshell.cabal b/ftshell.cabal
new file mode 100644
--- /dev/null
+++ b/ftshell.cabal
@@ -0,0 +1,29 @@
+name:           ftshell
+version:        0.2
+license:        PublicDomain
+license-file:   LICENSE
+author:         Sascha Boehme
+maintainer:     voigt@tcs.inf.tu-dresden.de
+synopsis:       Shell interface to the FreeTheorems library.
+description:
+    The ftshell is a shell-based user interface to interact with the
+    free-theorems library. It offers all possibilities provided by
+    that library to generate free theorems from Haskell type
+    expressions.
+category:       Language, Source-tools
+tested-with: 	GHC==6.8.2
+build-type:	Simple
+build-depends:
+    base >= 1.0
+  , mtl >= 1.0
+  , Shellac >= 0.9
+  , Shellac-readline >= 0.9
+  , free-theorems >= 0.2
+  , pretty >= 1.0.0.0
+  , containers >= 0.1.0.1
+data-files:
+    declarations.hs
+executable:     ftshell
+main-is:        main.hs
+hs-source-dirs: src
+extensions: MultiParamTypeClasses
diff --git a/src/Commands.hs b/src/Commands.hs
new file mode 100644
--- /dev/null
+++ b/src/Commands.hs
@@ -0,0 +1,465 @@
+
+
+
+-- Defines the commands which are not connected to a particular type signature.
+module Commands where
+
+
+
+import Control.Monad (liftM, when)
+import Control.Monad.Trans (liftIO)
+import Data.List (isPrefixOf, intersperse, sort, transpose)
+import Data.Map as Map (fromList, keys, lookup, elems)
+import Data.Maybe (fromJust)
+import Language.Haskell.FreeTheorems
+import Language.Haskell.FreeTheorems.Syntax
+import Language.Haskell.FreeTheorems.Theorems
+import System.Console.Shell
+import System.Console.Shell.ShellMonad
+import Text.PrettyPrint
+
+import ShellState
+
+
+
+
+
+------- File handling ---------------------------------------------------------
+
+
+-- Loads a file of declarations and shows a message of statistics afterwards. 
+cmdLoad :: File -> Sh ShellState ()
+cmdLoad (File fileName) = do
+  state  <- getShellSt
+  state' <- liftIO (loadDeclarations fileName state)
+  modifyShellSt (const state')
+
+
+
+-- Unloads an already loaded file.
+cmdUnload :: Completable LoadedFile -> Sh ShellState ()
+cmdUnload (Completable file) = do
+  files <- fromShellSt getDeclarationsFiles
+  let removeFile st = st { getDeclarationsFiles = filter (/= file) files }
+  when (file `elem` files)
+       (do modifyShellSt removeFile
+           shellPutStrLn $ "Unloaded `" ++ file ++ "'."
+           cmdReload)
+
+
+
+-- A tag to identify names of loaded files.
+data LoadedFile = LoadedFile
+
+instance Completion LoadedFile ShellState where
+  complete _ st input = return $ sort $ filter (isPrefixOf input)
+                                               (getDeclarationsFiles st)
+  completableLabel _ = "<file>"
+
+
+
+-- Resets the shell state and reloads all files.
+-- Resetting deletes all previous user input.
+cmdReload :: Sh ShellState ()
+cmdReload = do
+  files <- fromShellSt getDeclarationsFiles
+  modifyShellSt reset
+  mapM_ (cmdLoad . File) files
+
+
+
+-- Shows the names of all loaded files.
+cmdShowLoadedFiles :: Sh ShellState ()
+cmdShowLoadedFiles = do
+  files <- fromShellSt getDeclarationsFiles
+  if null files
+    then shellPutStrLn "There are no loaded files."
+    else mapM_ shellPutStrLn files
+
+
+
+
+
+------- Declarations ----------------------------------------------------------
+
+
+-- Displays the names of all valid declarations per input file.
+-- Names are shown in groups for algebraic data types, type renamings, type
+-- synonyms, type classes and type signatures.
+-- Names are shown columnwise for each group.
+cmdShowAllDeclarations :: Sh ShellState ()
+cmdShowAllDeclarations = do
+  files   <- fromShellSt getDeclarationsFiles
+  strings <- mapM fileToString files
+  sigs <- fromShellSt getUserSignatureNames
+  let s = prepend "Type signatures entered by the user:" (inColumns 76 3 2 sigs)
+  let allDecls = strings ++ [s]
+
+  if and (map null allDecls)
+    then shellPutStrLn "There are no declarations."
+    else mapM_ shellPutStr allDecls
+
+  where
+    fileToString f = do
+      ds <- mapM (declToString f) declTypes
+      return $ prepend ("In `" ++ f ++ "':") (concat ds)
+
+    declTypes = 
+      [ ("  Algebraic data types:", onlyDataDecl)
+      , ("  Type renamings:",       onlyNewtypeDecl)
+      , ("  Type synonyms:",        onlyTypeDecl)
+      , ("  Type classes:",         onlyClassDecl)
+      , ("  Type signatures:",      onlySigDecl) ]
+    
+    declToString f (label, select) = do
+      ds <- fromShellSt (getDeclarationNamesIn select f)
+      return $ prepend label (inColumns 74 5 2 $ sort ds)
+    
+    prepend _ "" = ""
+    prepend s t  = s ++ "\n" ++ t
+
+
+
+-- Formats a list of strings into a column view.
+-- The first argument is the length of a line, the second one is the indent to
+-- prepend every line, and the third argument describes the gap between items.
+inColumns :: Int -> Int -> Int -> [String] -> String
+inColumns _          _      _   []      = []
+inColumns lineLength indent gap strings = 
+  let max   = gap + maximum (map length strings)
+      nCols = (lineLength + gap) `div` max
+      guess = (length strings) `div` nCols
+      len   = if (length strings) `mod` nCols == 0
+                then guess
+                else guess + 1
+      
+      blocks :: Int -> [a] -> [[a]]
+      blocks n xs = if n == 0
+                      then [xs]
+                      else case xs of
+                             []        -> []
+                             otherwise -> let (s,t) = splitAt n xs
+                                           in s : (blocks n t)
+
+      spaces i  = replicate i ' '
+      resize s  = s ++ spaces (max - length s)
+      toLine xs = concatMap resize xs
+      shift i s = spaces i ++ s
+
+   in (unlines . map (shift indent . toLine) . transpose . blocks len) strings
+
+
+
+-- Shows the declaration for a given name, if it can be found in the list
+-- of all declarations.
+cmdShowDeclaration :: Completable DeclarationName -> Sh ShellState ()
+cmdShowDeclaration (Completable name) = do
+  maybeDecl <- fromShellSt (getDeclarationOf name)
+  case maybeDecl of
+    Nothing -> shellPutStrLn $ "There is no declaration with name `" 
+                               ++ name ++ "'."
+    Just d  -> (shellPutStrLn . doRender 0) d
+
+
+
+-- A tag to identify declaration names.
+data DeclarationName = DeclarationName
+
+instance Completion DeclarationName ShellState where
+  complete _ st input = return $ sort $ filter (isPrefixOf input)
+                                               (getAllDeclarationNames st)
+  completableLabel _ = "<name>"
+
+
+
+-- Shows the signatures loaded from input files and previously entered by the
+-- user.
+cmdShowSignatures :: Sh ShellState ()
+cmdShowSignatures = do
+  files <- fromShellSt getDeclarationsFiles
+  let fs = map (\f -> "In `" ++ f ++ "':") files
+
+  sigs  <- liftM (zip fs) (mapM (fromShellSt . getSignaturesIn) files)
+  sig   <- liftM (\s -> ("Type signatures entered by the user:", s)) 
+                 (fromShellSt getUserSignatures)
+  let s = filter (\(_,l) -> not (null l)) (sigs ++ [sig])
+  
+  if null s
+    then shellPutStrLn "There are no type signatures."
+    else mapM_ showSignature s
+
+  where
+    showSignature (label, sigs) = do
+      shellPutStrLn label
+      let toString = doRender 3 . prettySignature . rawSignature
+      (mapM_ shellPutStrLn . sort . map toString) sigs
+
+
+
+
+
+------- Language subsets ------------------------------------------------------
+
+
+-- Shows the current language subset.
+cmdShowLanguageSubset :: Sh ShellState ()
+cmdShowLanguageSubset = do
+  l <- fromShellSt getCurrentLanguageSubset
+  let name = languageSubsetToString l
+  shellPutStrLn $ "The current language subset is `" ++ name ++ "'."
+
+
+-- Maps language subsets to human-readable strings.
+languageSubsetToString :: LanguageSubset -> String
+languageSubsetToString l = case l of
+  BasicSubset                       -> "basic"
+  SubsetWithFix EquationalTheorem   -> "fix-equational"
+  SubsetWithFix InequationalTheorem -> "fix-inequational"
+  SubsetWithSeq EquationalTheorem   -> "seq-equational"
+  SubsetWithSeq InequationalTheorem -> "seq-inequational"
+
+
+
+-- Changes the current language subset and displays the new one afterwards.
+-- Additionally, if there is a context, an updated theorem is shown.
+cmdSetLanguageSubset :: LanguageSubset -> Sh ShellState ()
+cmdSetLanguageSubset l = do
+  modifyShellSt (setCurrentLanguageSubset l)
+  context <- fromShellSt getCurrentContext
+  maybe cmdShowLanguageSubset (\_ -> cmdShowTheorem) context
+
+
+
+
+
+------- Display current theorem and associates --------------------------------
+
+
+-- Executes a command using the current signature.
+withCurrentSignature :: (ValidSignature -> Sh ShellState ()) -> Sh ShellState ()
+withCurrentSignature command = do
+  context <- fromShellSt getCurrentContext
+  maybe errorNoSignature (command . fst) context
+
+
+errorNoSignature = 
+  shellPutStrLn $
+    "Please enter a signature or a signature name before using this command."
+
+
+errorNoTheorem =
+  shellPutStrLn $
+    "There is no theorem possible for the current type in the current language"
+    ++ "\nsubset. Please select a language subset with `seq'."
+
+
+-- Execute a command using the current context.
+-- The command is applied to the current type signature and the latest 
+-- intermediate generated for that type signature.
+withCurrentContext :: 
+    (ValidSignature -> Intermediate -> Sh ShellState ()) -> Sh ShellState () 
+withCurrentContext command = do
+  context <- fromShellSt getCurrentContext
+  maybe errorNoSignature 
+        (\(s,i) -> maybe errorNoTheorem (command s) i) context
+
+
+
+-- Shows the current type signature.
+cmdShowCurrentSignature :: Sh ShellState ()
+cmdShowCurrentSignature = withCurrentSignature $ \sig -> do
+  shellPutStrLn . doRender 0 . prettySignature . rawSignature $ sig
+
+
+
+-- Shows the current theorem.
+cmdShowTheorem :: Sh ShellState ()
+cmdShowTheorem = withCurrentContext $ \sig intermediate -> do
+  opts <- fromShellSt getCurrentTheoremOptions
+  let pt = prettyTheorem opts (asTheorem intermediate)
+  shellPutStrLn "The free theorem for the type signature\n"
+  (shellPutStrLn . doRender 2 . prettySignature . rawSignature) sig
+  l <- fromShellSt getCurrentLanguageSubset
+  let n = languageSubsetToString l
+  shellPutStrLn $ "\nin the language subset `" ++ n ++ "' is:\n"
+  shellPutStrLn $ (doRender 2 pt) ++ "\n"
+
+
+
+-- Shows the definitions of lifted relations occurring in the current theorem.
+cmdShowLiftedRelations :: Sh ShellState ()
+cmdShowLiftedRelations = withCurrentContext $ \_ intermediate -> do
+  vds  <- fromShellSt (concat . Map.elems . getAllDeclarations)
+  opts <- fromShellSt getCurrentTheoremOptions
+  let lifts = unfoldLifts vds intermediate
+  if null lifts
+    then shellPutStrLn "There are no lifted relations in the current theorem."
+    else do shellPutStrLn ""
+            mapM_ (\s -> shellPutStrLn (s ++ "\n"))
+                  (map (doRender 2 . prettyUnfoldedLift opts) lifts)
+
+
+
+-- Shows the definitions of the class constraints occurring in the current 
+-- theorem.
+cmdShowClasses :: Sh ShellState ()
+cmdShowClasses = withCurrentContext $ \_ intermediate -> do
+  vds  <- fromShellSt (concat . Map.elems . getAllDeclarations)
+  opts <- fromShellSt getCurrentTheoremOptions
+  let classes = unfoldClasses vds intermediate
+  if null classes
+    then shellPutStrLn "There are no class constraints in the current theorem."
+    else do shellPutStrLn ""
+            mapM_ (\s -> shellPutStrLn (s ++ "\n"))
+                  (map (doRender 2 . prettyUnfoldedClass opts) classes)
+
+
+
+
+
+------- Specialising relation variables ---------------------------------------
+
+
+-- Shows all relation variables which can be specialised to functions.
+cmdShowRelationVariables :: Sh ShellState ()
+cmdShowRelationVariables = withCurrentContext $ \_ intermediate -> do
+  let rvs = relationVariables intermediate
+   in if null rvs
+        then shellPutStrLn $
+               "There are no relations variables which could be specialised."
+        else shellPutStrLn 
+               . doRender 0
+               . fcat . punctuate (text "  ")
+               . map prettyRelationVariable 
+               $ rvs
+
+
+
+-- Specialises a relation variable to a function.
+cmdSpecialise :: Completable RelationVariable -> Sh ShellState ()
+cmdSpecialise (Completable rv) = withCurrentContext $ \_ intermediate -> do
+  if rv `notElem` map (\(RVar r) -> r) (relationVariables intermediate)
+    then shellPutStrLn $ "Relation variable `" ++ rv ++ "' cannot be specialised."
+    else do modifyShellSt (addSpecialisation (Left (RVar rv)))
+            cmdShowTheorem
+
+
+
+-- Specialises a relation variable to a function.
+cmdSpecialiseInverse :: Completable RelationVariable -> Sh ShellState ()
+cmdSpecialiseInverse (Completable rv) = withCurrentContext $ \_ intermediate -> do
+  l <- fromShellSt getCurrentLanguageSubset
+  case l of
+    BasicSubset                     -> shellPutStrLn error
+    SubsetWithFix EquationalTheorem -> shellPutStrLn error
+    SubsetWithSeq EquationalTheorem -> shellPutStrLn error
+    otherwise -> do
+      if rv `notElem` map (\(RVar r) -> r) (relationVariables intermediate)
+        then shellPutStrLn $ "There is no relation variable `" ++ rv ++ "'."
+        else do modifyShellSt (addSpecialisation (Right (RVar rv)))
+                cmdShowTheorem
+    
+  where error =
+          "This command cannot be used with the current language subset.\n"
+          ++ "Please use an inequational language subset."
+
+
+
+instance Completion RelationVariable ShellState where
+  complete _ st input = 
+    case getCurrentContext st of
+      Nothing    -> return []
+      Just (_,i) -> return . sort 
+                           . filter (isPrefixOf input)
+                           . map (\(RVar r) -> r) 
+                           $ maybe [] relationVariables i
+  completableLabel _ = "<relation-variable>"
+
+
+
+-- Reverts a specialisation of a relation variable, if at least one
+-- relation variable has been specialised.
+cmdUndo :: Sh ShellState ()
+cmdUndo = do
+  h <- fromShellSt getSpecialisationHistory
+  if null h
+    then shellPutStrLn "There is nothing to undo."
+    else do modifyShellSt undoSpecialisation
+            cmdShowTheorem
+
+
+
+
+
+------- Theorem options -------------------------------------------------------
+
+
+-- Describes a mapping of theorem options to their human-readable name.
+allTheoremOptions = Map.fromList
+  [ ("language-subsets",     OmitLanguageSubsets)
+  , ("type-instantiations",  OmitTypeInstantiations)
+  ]
+
+
+
+-- Show the currently set theorem options.
+cmdShowCurrentTheoremOptions :: Sh ShellState ()
+cmdShowCurrentTheoremOptions = do
+  opts <- fromShellSt getCurrentTheoremOptions
+  shellPutStrLn "The current options for displaying theorems are:"
+  mapM_ (showOpt opts) (Map.keys allTheoremOptions)
+  where
+    showOpt opts o =
+      if fromJust (Map.lookup o allTheoremOptions) `elem` opts
+        then shellPutStrLn $ "  omit " ++ o
+        else shellPutStrLn $ "  show " ++ o
+
+
+
+-- Enables a theorem option.
+cmdTheoremOptionShow :: Completable TheoremOptions -> Sh ShellState ()
+cmdTheoremOptionShow =
+  let del opt os = filter (/= opt) os
+   in updateTheoremOptions del
+
+
+
+-- Disables a theorem option.
+cmdTheoremOptionOmit :: Completable TheoremOptions -> Sh ShellState ()
+cmdTheoremOptionOmit =
+  let add opt os = if opt `notElem` os then opt : os else os
+   in updateTheoremOptions add
+
+
+
+-- Modifies the current theorem options with the help of a modification
+-- function.
+updateTheoremOptions :: 
+    (PrettyTheoremOption -> [PrettyTheoremOption] -> [PrettyTheoremOption])
+    -> Completable TheoremOptions
+    -> Sh ShellState ()
+updateTheoremOptions f (Completable opt) = 
+  case Map.lookup opt allTheoremOptions of
+    Nothing -> shellPutErrLn $ "Unknown theorem option `" ++ opt ++ "'."
+    Just o  -> do modifyShellSt (updateOptions (f o))
+                  cmdShowCurrentTheoremOptions
+                  ctx <- fromShellSt getCurrentContext
+                  maybe (shellSpecial ShellNothing)
+                        (\_ -> shellPutStrLn "" >> cmdShowTheorem) ctx
+  where
+    updateOptions f state =
+      state { getCurrentTheoremOptions = f (getCurrentTheoremOptions state) }
+
+
+
+-- A tag to identify theorem options.
+data TheoremOptions = TheoremOptions
+
+instance Completion TheoremOptions ShellState where
+  complete _ st input = return $ sort $ filter (isPrefixOf input)
+                                               (Map.keys allTheoremOptions)
+  completableLabel _ = "<option>"
+
+
+
+
diff --git a/src/Evaluate.hs b/src/Evaluate.hs
new file mode 100644
--- /dev/null
+++ b/src/Evaluate.hs
@@ -0,0 +1,102 @@
+
+
+
+-- Defines functions used in evaluating any input which is not a command.
+module Evaluate (signatureCompletion, evaluate) where
+
+
+
+import Control.Monad (liftM)
+import Data.List (find, isPrefixOf, tails, sort)
+import Data.Map as Map (elems)
+import Data.Maybe (fromJust)
+import Language.Haskell.FreeTheorems
+import Language.Haskell.FreeTheorems.Syntax
+import System.Console.Shell
+import System.Console.Shell.ShellMonad
+
+import Commands (cmdShowTheorem)
+import ShellState
+
+
+
+-- Provides completion support for type names entered directly at the prompt.
+-- Checks against all known signature names.
+signatureCompletion :: ShellState -> String -> IO [String]
+signatureCompletion state input =
+  return $ sort $ filter (isPrefixOf input) (getAllSignatureNames state)
+
+
+
+-- Evaluate input at the prompt.
+-- Consider any input starting with a colon as misspelled command name and
+-- do nothing (it wouldn't be a proper signature, anyway).
+-- Parse any other input, and if it contains a valid signature, change the
+-- current context and show the according theorem.
+evaluate :: String -> Sh ShellState ()
+evaluate s =
+  if ":" `isPrefixOf` s
+    then shellPutStrLn "Ignored incomplete command."
+    else do
+      result <- parseInput s
+      case result of
+        Nothing  -> shellSpecial ShellNothing
+        Just sig -> modifyShellSt (setCurrentContext sig) >> cmdShowTheorem
+
+
+
+-- Parses the input and returns the parsed signature, if any.
+-- If the input contains "::", then it is is parsed as a signature.
+-- If the input is only one word, it is looked for in the list of all 
+-- signatures. However, if there is no suitable list or if the input contains
+-- more than one word, a new name is generated and prepended to the input
+-- before it is parsed as a signature.
+parseInput :: String -> Sh ShellState (Maybe ValidSignature)
+parseInput s =
+  if any (isPrefixOf "::") (tails s)
+    then parseSignature s
+    else
+      case words s of
+        []        -> return Nothing
+        [x]       -> do maybeSig <- fromShellSt (findSignature x) 
+                        case maybeSig of
+                          Nothing -> createNewNameAndParse s
+                          Just _  -> return maybeSig
+        otherwise -> createNewNameAndParse s
+  where
+    createNewNameAndParse s = do
+      n <- createNewSignatureName
+      parseSignature (n ++ " :: " ++ s)
+        
+
+
+-- Creates a name for a signature which is different to any signature name
+-- in the list of all signatures of the state.
+createNewSignatureName :: Sh ShellState String
+createNewSignatureName = do
+  sigNames <- fromShellSt getAllSignatureNames
+  let newNames = "f":map (\i -> "f" ++ show i) [1..]
+  return $ fromJust $ find (\n -> not $ n `elem` sigNames) newNames
+
+
+
+-- Tries to parse a string to a signature.
+-- If successful, the parsed signature is added to the state and its name is
+-- returned. Otherwise, an error message is printed.
+parseSignature :: String -> Sh ShellState (Maybe ValidSignature)
+parseSignature s = do
+  parse <- fromShellSt getParser
+  decls <- fromShellSt (concat . Map.elems . getAllDeclarations)
+  let (vs,es) = runChecks (parse s >>= checkAgainst decls)
+      sig     = filterSignatures vs
+  if not (null es)
+    then shellPutErrLn ("Error: " ++ show (head es)) >> return Nothing
+    else case sig of
+      []    -> shellPutErrLn errEmptySig >> return Nothing
+      (s:_) -> do modifyShellSt (addUserSignature s)
+                  return (Just s)
+  where      
+    errEmptySig = 
+      "Error: The input was not recognised as a valid type signature."
+
+
diff --git a/src/HelpCommands.hs b/src/HelpCommands.hs
new file mode 100644
--- /dev/null
+++ b/src/HelpCommands.hs
@@ -0,0 +1,89 @@
+
+
+
+-- Shell commands for user help.
+module HelpCommands where
+
+
+import System.Console.Shell
+import System.Console.Shell.ShellMonad
+import Text.PrettyPrint
+
+import ShellState
+
+
+
+paragraph s = 
+  let st = style { lineLength = 78, ribbonsPerLine=1.0 }
+   in do shellPutStrLn . renderStyle st . fsep . map text . words $ s
+         shellPutStrLn ""
+
+
+
+cmdShowShellHelp :: Sh ShellState ()
+cmdShowShellHelp = do
+  shellPutStrLn $ unlines
+    [ ""
+    , "   FTSHELL USER GUIDE"
+    ]
+  paragraph $
+    "This shell allows to automatically generate free theorems for "
+    ++ "Haskell types. See `:help-theorems' for a short introduction to "
+    ++ "free theorems."
+  paragraph $ 
+    "Interaction with this shell is done through entering commands at the "
+    ++ "prompt. Every command is prefixed by a colon, i.e. the character `:'. "
+    ++ "The list of available commands is shown when entering `:help' at the "
+    ++ "prompt. Commands may be completed by pressing the TAB key."
+  paragraph $
+    "Besides entering commands, the user may also input types or type names at "
+    ++ "the prompt. There also, TAB-completion is provided. The available "
+    ++ "types can be obtained by entering either `:all-declarations' or "
+    ++ "`:signatures'."
+  paragraph $
+    "When entering a valid type or the name of an already existing type, the "
+    ++ "current context is switched to this type. The shell's commands are "
+    ++ "then applied to this type and the theorem generated from it, which is "
+    ++ "displayed directly after entering the type or by entering `:theorem'. "
+    ++ "Commands working on the current theorem are `:lifts' to show the "
+    ++ "definition of lifted relations and `:classes' to display class "
+    ++ "constraints occurring in generated theorems."
+  paragraph $
+    "Relation variables of a theorem can be specialized to functions using "
+    ++ "the `:specialise' or the `:specialise-inverse' command. The deduced "
+    ++ "theorem is immediately printed afterwards. Every specialization may "
+    ++ "be undone by the `:undo' command."
+  paragraph $
+    "The display of theorems may be modified by theorem options. They can be "
+    ++ "by either `:show' or `:omit', and the current options are printed "
+    ++ "when `:options' is entered at the prompt."
+
+
+
+
+cmdShowTheoremHelp :: Sh ShellState ()
+cmdShowTheoremHelp = do
+  shellPutStrLn $ unlines
+    [ ""
+    , "   FREE THEOREMS IN A NUTSHELL"
+    ]
+  paragraph $
+    "Free Theorems are results solely derived from the type of a function. "
+    ++ "The key idea is to interpret types as relations. To reflect the "
+    ++ "structure of types, a relational action, which maps relations to a "
+    ++ "relation, is defined for every type constructor. Using relational "
+    ++ "actions, a relation can be constructed for every type, and, by "
+    ++ "applying the definitions of these relational actions, free theorems "
+    ++ "are obtained."
+  paragraph $
+    "Recursion and selective strictness weaken free theorems. To study the "
+    ++ "influences caused by adding these constructs, several sublanguages "
+    ++ "are provided in this application. Here, `fix' corresponds to "
+    ++ "languages where recursion is allowed, and `seq' describes "
+    ++ "sublanguages where both recursion and selective strictness is "
+    ++ "provided. Additionally, it is possible to derive equational and "
+    ++ "inequational theorems."
+
+
+
+
diff --git a/src/Settings.hs b/src/Settings.hs
new file mode 100644
--- /dev/null
+++ b/src/Settings.hs
@@ -0,0 +1,70 @@
+
+
+
+-- Application settings. They can be changed (partly) by command line options.
+module Settings where
+
+
+
+import Paths_ftshell (getDataFileName, version)
+
+import Data.Version (showVersion)
+import Language.Haskell.FreeTheorems (Parsed)
+import Language.Haskell.FreeTheorems.Syntax (Declaration)
+
+-- Import the parsers used by the shell.
+import qualified Language.Haskell.FreeTheorems.Parser.Haskell98 as Haskell98
+import qualified Language.Haskell.FreeTheorems.Parser.Hsx as Hsx
+
+-- Import the backends used by the shell.
+import System.Console.Shell.Backend (ShellBackend)
+import System.Console.Shell.Backend.Readline (readlineBackend)
+
+
+
+-- The filename of the file in which the basic declarations reside.
+-- This file is always loaded on startup.
+basicDeclarationsFileName = "declarations.hs"
+
+
+
+-- A structure containing all application settings.
+-- Note that this structure is partly reflected by 'ShellState'.
+data Settings = Settings
+  { parser           :: String -> Parsed [Declaration]
+  , parserName       :: String
+  , backend          :: ShellBackend ()
+  , backendName      :: String
+  , insteadOfShell   :: Maybe PrintSomething
+  , prelude          :: Maybe FilePath
+  , inputFiles       :: [String]
+  }
+
+
+
+-- Initialize the settings.
+-- The command line options are modifying these settings afterwards.
+initialSettings = do
+  declFileName <- getDataFileName basicDeclarationsFileName
+  return $ Settings
+    { parser           = Hsx.parse
+    , parserName       = "Haskell parser with extensions based on "
+                         ++ "`haskell-src-exts'"
+--    { parser           = Haskell98.parse
+--    , parserName       = "Haskell98 parser based on `haskell-src'"
+    , backend          = readlineBackend
+    , backendName      = "readline-based backend"
+    , insteadOfShell   = Nothing
+    , prelude          = Just declFileName
+    , inputFiles       = []
+    }
+
+
+
+-- Actions to be done instead of running the shell.
+data PrintSomething
+  = PrintHelp       -- Print the available command line options.
+  | PrintVersion    -- Print the application version.
+
+
+
diff --git a/src/Shell.hs b/src/Shell.hs
new file mode 100644
--- /dev/null
+++ b/src/Shell.hs
@@ -0,0 +1,199 @@
+
+
+
+-- Configures and runs the shell.
+module Shell where
+
+
+
+import Paths_ftshell (version)
+
+import Control.Monad (foldM, when)
+import Data.Maybe (catMaybes, maybeToList)
+import Data.Version (showVersion)
+import Language.Haskell.FreeTheorems
+import Language.Haskell.FreeTheorems.Syntax
+import System.Console.Shell
+import System.Console.Shell.ShellMonad
+import System.Environment (getProgName)
+
+import Settings
+import ShellState
+import Evaluate
+import Commands
+import HelpCommands
+
+
+
+-- Initialises and runs the shell.
+initAndRunShell :: Settings -> IO ()
+initAndRunShell settings = do
+  -- show the name and the purpose of the application, and give a quick command
+  -- overview
+  showGreetingMessage settings
+
+  -- create an initial state from the settings given at the command line
+  let initialState = initialShellState settings
+  
+  -- load the declarations files given at the command line
+  let files = maybeToList (prelude settings) ++ inputFiles settings
+  state <- foldM (\s f -> loadDeclarations f s) initialState files
+  when (not (null files)) (putStrLn "")
+  
+  -- initialise the shell and run it
+  let shellDescription = createShellDescription
+  let shellBackend = backend settings
+  runShell shellDescription shellBackend state
+  return ()
+      
+
+
+-- Shows a short message giving the name, version, purpose and the most 
+-- important commands of the shell.
+showGreetingMessage :: Settings -> IO ()
+showGreetingMessage settings = 
+  putStr $ unlines
+    [ "FTshell (version " ++ showVersion version ++ ") - " ++ 
+      "Automatic generation of free theorems"
+    , ""
+    , "Press `:help' for help or `:quit' to quit."
+    , ""
+    ]
+
+
+
+-- Creates the settings for the shell.
+createShellDescription :: ShellDescription ShellState
+createShellDescription =
+  initialShellDescription {
+
+    -- set the available commands, see also the function 'commands'
+    shellCommands      = commands,
+
+    -- commands are prefixed with a colon character
+    commandStyle       = CharPrefixCommands ':',
+    
+    -- set the function called when something else than a command was entered
+    evaluateFunc       = evaluate,
+
+    -- set the prompt of the shell, this is based on the current context
+    -- see 'createPrompt' for more information
+    prompt             = createPrompt,
+
+    -- signatures can be entered directly, tab completion of signatures
+    -- is provided (if the readline backend is used)
+    defaultCompletions = Just signatureCompletion,
+
+    -- command history is turned on
+    historyEnabled     = True,
+
+    -- the maximum number of commands remembered in one session
+    maxHistoryEntries  = 100,
+
+    -- there is no file storing the commands of previous sessions
+    historyFile        = Nothing
+  }
+
+
+
+-- Creates the prompt of the shell based on the current context.
+createPrompt :: ShellState -> IO String
+createPrompt state =
+  case getCurrentContext state of
+    Nothing    -> return "> "
+    Just (s,_) -> let getName = unpackIdent . signatureName . rawSignature
+                   in return (getName s ++ " > ")
+
+
+
+-- Maps short and long command names to command functions.
+commands :: [ShellCommand ShellState]
+commands =
+  [ helpCommand "help"
+
+  , cmd "help-shell" cmdShowShellHelp
+        "Display the shell user guide"
+
+  , cmd "help-free-theorems" cmdShowTheoremHelp
+        "Display an introduction to free theorems\n"
+  
+  , cmd "load" cmdLoad
+        "Load a file of declarations"
+
+  , cmd "unload" cmdUnload
+        "Unload a file of declarations"
+
+  , cmd "reload-all" cmdReload
+        "Reload all declarations files"
+
+  , cmd "files" cmdShowLoadedFiles
+        "Display all loaded declarations files\n"
+  
+  , cmd "all-declarations" cmdShowAllDeclarations
+        "Display all declared constructors"
+
+  , cmd "declaration" cmdShowDeclaration
+        "Display a declaration"
+
+  , cmd "signatures" cmdShowSignatures
+        "Display all available signatures"
+
+ ,  cmd "current-signature" cmdShowCurrentSignature
+        "Display the current signature\n"
+  
+  , cmd "language-subset" cmdShowLanguageSubset
+        "Display the current language subset"
+  
+  , cmd "basic-subset" (cmdSetLanguageSubset $ BasicSubset)
+        "Set `basic' as the current language subset"
+  
+  , cmd "fix-equational"
+        (cmdSetLanguageSubset $ SubsetWithFix EquationalTheorem)
+        "Set `fix-equational' as the current language subset"
+  
+  , cmd "fix-inequational"
+        (cmdSetLanguageSubset $ SubsetWithFix InequationalTheorem)
+        "Set `fix-inequational' as the current language subset"
+  
+  , cmd "seq-equational"
+        (cmdSetLanguageSubset $ SubsetWithSeq EquationalTheorem)
+        "Set `seq-equational' as the current language subset"
+  
+  , cmd "seq-inequational"  
+        (cmdSetLanguageSubset $ SubsetWithSeq InequationalTheorem)
+        "Set `seq-inequational' as the current language subset\n"
+
+  , cmd "theorem" cmdShowTheorem
+        "Display the current theorem"
+  
+  , cmd "lifts" cmdShowLiftedRelations
+        "Display definitions for the lifted relations"
+  
+  , cmd "classes" cmdShowClasses
+        "Display definitions for the class constraints"
+  
+  , cmd "relation-variables" cmdShowRelationVariables
+        "Display all relation variables which can be specialised"
+  
+  , cmd "specialise" cmdSpecialise
+        "Specialise a relation variable to a function"
+  
+  , cmd "specialise-inverse" cmdSpecialiseInverse
+        "Specialise a relation variable to an inverse function"
+  
+  , cmd "undo" cmdUndo
+        "Undo the last specialisation to a function"
+  
+  , cmd "options" cmdShowCurrentTheoremOptions
+        "Display the currently selected theorem options"
+  
+  , cmd "show" cmdTheoremOptionShow
+        "Turn on a theorem option"
+
+  , cmd "omit" cmdTheoremOptionOmit
+        "Turn off a theorem option\n"
+  
+  , exitCommand "quit"
+  ]
+
+
diff --git a/src/ShellState.hs b/src/ShellState.hs
new file mode 100644
--- /dev/null
+++ b/src/ShellState.hs
@@ -0,0 +1,373 @@
+
+
+
+-- Defines the internal state of the application.
+module ShellState where
+
+
+
+import Control.Monad (liftM, when)
+import Data.List (find)
+import qualified Data.Map as Map (Map, empty, elems, insert, lookup)
+import Data.Maybe (mapMaybe)
+import Language.Haskell.FreeTheorems
+import Language.Haskell.FreeTheorems.Syntax
+import Language.Haskell.FreeTheorems.Theorems
+import System.Console.Shell.ShellMonad
+import System.IO (hGetBuffering, hSetBuffering, stdout, BufferMode (..))
+import Text.PrettyPrint as Doc
+
+import Settings
+
+
+
+
+
+------- General purpose functions ---------------------------------------------
+
+-- Render pretty documents.
+doRender :: Int -> Doc -> String
+doRender indent doc = renderStyle (Style PageMode 74 1.2) (nest indent doc)
+
+
+
+-- Applies an information retrieval function to the shell state in a shell
+-- operation.
+fromShellSt :: (ShellState -> a) -> Sh ShellState a
+fromShellSt f = liftM f getShellSt
+
+
+
+
+
+------- Shell state structure -------------------------------------------------
+
+
+-- The structure of the internal state.
+data ShellState = ShellState
+  { getParser            :: String -> Parsed [Declaration]
+        -- The parser which is used for all inputs.
+        -- It should not be changed during the run of the application.
+  
+  , getDeclarationsFiles :: [FilePath]
+        -- The names of all files containing declarations.
+  
+  , getAllDeclarations   :: Map.Map FilePath [ValidDeclaration]
+        -- Maps a file name to the declarations parsed from that file.
+  
+  , getUserSignatures    :: [ValidSignature]
+        -- Contains all signatures entered by the user.
+  
+  , getCurrentLanguageSubset :: LanguageSubset
+        -- The current language subset.
+  
+  , getCurrentContext    :: Maybe (ValidSignature, Maybe Intermediate)
+        -- The current type signature and its interpretation.
+        -- The relation variables stored in 'getSpecialisationHistory' are 
+        -- specialised in the intermediate.
+
+  , getSpecialisationHistory  :: [Either RelationVariable RelationVariable]
+        -- Gives the order of relation variables which were specialised in the
+        -- current theorem. The head was specialised first, while the last
+        -- relation variables were specialised last.
+        -- Left variables are specialised in the standard way, while
+        -- right variables are specialised to inverse functions.
+
+  , getCurrentTheoremOptions :: [PrettyTheoremOption]
+        -- The current options which modify how theorems are pretty-printed.
+
+  }
+
+
+
+-- Initialises the state of the shell from a given settings structure.
+-- The declarations and the declarations files are loaded and added afterwards
+-- by 'loadDeclarations'.
+initialShellState :: Settings -> ShellState
+initialShellState settings = ShellState
+  { getParser                = parser settings
+  , getDeclarationsFiles     = []
+  , getAllDeclarations       = Map.empty
+  , getUserSignatures        = []
+  , getCurrentLanguageSubset = BasicSubset
+  , getCurrentContext        = Nothing
+  , getSpecialisationHistory = []
+  , getCurrentTheoremOptions = [ OmitTypeInstantiations
+                               -- , OmitLanguageSubsets
+                               ]
+  }
+
+
+-- Resets the state. 
+-- All previous state information is lost except the parser and the language
+-- subset. Note that also the list of declarations files is erased.
+-- These files can be added again by subsequent calls to 'loadDeclarations'.
+reset :: ShellState -> ShellState
+reset state = ShellState
+  { getParser                = getParser state
+  , getDeclarationsFiles     = []
+  , getAllDeclarations       = Map.empty
+  , getUserSignatures        = []
+  , getCurrentLanguageSubset = getCurrentLanguageSubset state
+  , getCurrentContext        = Nothing
+  , getSpecialisationHistory = []
+  , getCurrentTheoremOptions = getCurrentTheoremOptions state
+  }
+
+
+
+
+
+------- Loading files ---------------------------------------------------------
+
+
+-- Loads a declarations file. Returns the modified state, selected error
+-- messages and a message containing statistics about loaded declarations.
+loadDeclarations :: FilePath -> ShellState -> IO ShellState
+loadDeclarations path state = do
+  catch
+    (do contents <- readFile path
+        bufferMode <- hGetBuffering stdout
+        hSetBuffering stdout NoBuffering
+        putStr $ "Loading `" ++ path ++ "' ... "
+        let decls   = concat $ Map.elems $ getAllDeclarations state
+            parse   = getParser state
+            (vs,es) = runChecks (parse contents >>= checkAgainst decls)
+
+            -- Create a new state by adding the file name and the parsed
+            -- declarations.
+            state'  = state
+                        { getDeclarationsFiles = getDeclarationsFiles state 
+                                                 ++ [path]
+                        , getAllDeclarations = Map.insert path vs
+                                               (getAllDeclarations state) }
+            
+        if null es
+          then  -- Create a message containing statistics.
+            putStrLn $ 
+              case length vs of
+                0         -> "found no declaration."
+                1         -> "found 1 declaration."
+                otherwise -> "found " ++ show (length vs) ++ " declarations."
+
+          else  -- Create a list of errors.
+            putStrLn . doRender 0 $
+              case length es of
+                1         -> text "found one error:" $$ nest 2 (head es)
+                otherwise -> text ("found " ++ show (length es) ++ " errors:")
+                                    $$ nest 2 (vcat (take 5 es))
+
+        hSetBuffering stdout bufferMode
+        return state'
+    )
+    (\error -> do
+       putStrLn $ "Error: Unable to load the file `" ++ path ++ "'."
+       return state 
+    )
+
+
+
+
+
+------- Declaration functions -------------------------------------------------
+
+
+-- Returns the declarations loaded from the given file.
+getDeclarationsIn :: FilePath -> ShellState -> [ValidDeclaration]
+getDeclarationsIn file state =
+  case Map.lookup file (getAllDeclarations state) of
+    Nothing -> []
+    Just ds -> ds
+
+
+-- Returns the names of all loaded declarations and all type signature name 
+-- entered by the user.
+getAllDeclarationNames :: ShellState -> [String]
+getAllDeclarationNames state =
+  let allNamesIn f = map (unpackIdent . getDeclarationName . rawDeclaration)
+                         (getDeclarationsIn f state)
+   in concatMap (\file -> allNamesIn file) (getDeclarationsFiles state)
+      ++ getUserSignatureNames state
+
+
+
+-- Returns the declaration names loaded from the given file and fitting the
+-- given selector function.
+getDeclarationNamesIn :: 
+    (Declaration -> Bool) -> FilePath -> ShellState -> [String]
+getDeclarationNamesIn select file = 
+  map (unpackIdent . getDeclarationName) 
+  . filter select 
+  . map rawDeclaration 
+  . getDeclarationsIn file
+
+
+
+-- Selector function to retrieve declarations of algebraic data types.
+onlyDataDecl :: Declaration -> Bool
+onlyDataDecl decl = case decl of
+  DataDecl _ -> True
+  otherwise  -> False
+
+
+
+-- Selector function to retrieve declarations of type renamings.
+onlyNewtypeDecl :: Declaration -> Bool
+onlyNewtypeDecl decl = case decl of
+  NewtypeDecl _ -> True
+  otherwise     -> False
+
+
+
+-- Selector function to retrieve declarations of type synonyms.
+onlyTypeDecl :: Declaration -> Bool
+onlyTypeDecl decl = case decl of
+  TypeDecl _ -> True
+  otherwise  -> False
+
+
+
+-- Selector function to retrieve declarations of type classes.
+onlyClassDecl :: Declaration -> Bool
+onlyClassDecl decl = case decl of
+  ClassDecl _ -> True
+  otherwise   -> False
+
+
+
+-- Selector function to retrieve declarations of type signatures.
+onlySigDecl :: Declaration -> Bool
+onlySigDecl decl = case decl of
+  TypeSig _ -> True
+  otherwise -> False
+
+
+
+-- Returns the pretty-printed declaration for the given declaration name, if
+-- there exists a declaration with such a name.
+getDeclarationOf :: String -> ShellState -> Maybe Doc
+getDeclarationOf declName state = 
+  let us = map (TypeSig . rawSignature) (getUserSignatures state)
+      fs = reverse (getDeclarationsFiles state)
+      ds = concatMap (\f -> map rawDeclaration (getDeclarationsIn f state)) fs
+      getName = unpackIdent . getDeclarationName
+   in liftM prettyDeclaration (find (\s -> getName s == declName) (us ++ ds))
+
+
+
+
+
+------- Signature functions ---------------------------------------------------
+
+
+-- Returns the names of all type signatures, both loaded from files and entered
+-- by the user.
+getAllSignatureNames :: ShellState -> [String]
+getAllSignatureNames state =
+  concatMap (\f -> getDeclarationNamesIn onlySigDecl f state)
+            (getDeclarationsFiles state)
+  ++ getUserSignatureNames state
+
+
+
+-- Returns only the names of type signatures entered by the user.
+getUserSignatureNames :: ShellState -> [String]
+getUserSignatureNames =
+  map (unpackIdent . signatureName . rawSignature) . getUserSignatures
+
+
+
+-- Returns all signatures loaded from the given file.
+getSignaturesIn :: FilePath -> ShellState -> [ValidSignature]
+getSignaturesIn file state =
+  case Map.lookup file (getAllDeclarations state) of
+    Nothing -> []
+    Just ds -> filterSignatures ds
+
+
+
+-- Adds a user-entered type signature to the list of known type signatures.
+addUserSignature :: ValidSignature -> ShellState -> ShellState
+addUserSignature s state = 
+  state { getUserSignatures = getUserSignatures state ++ [s] }
+
+
+
+-- Returns a type signature for the given name or Nothing, if there is no
+-- type signature with that name.
+-- Type signatures are searched for beginning from the user-entered type 
+-- signatures and then traversing the loaded files in reverse order.
+findSignature :: String -> ShellState -> Maybe ValidSignature
+findSignature name state = 
+  let us = reverse (getUserSignatures state)
+      fs = reverse (getDeclarationsFiles state)
+      ds = concatMap (\f -> filterSignatures (getDeclarationsIn f state)) fs
+      getName = unpackIdent . signatureName . rawSignature
+   in find (\s -> getName s == name) (us ++ ds)
+
+
+
+
+
+------- Context and language functions ----------------------------------------
+
+
+-- Changes the context to the given type signature.
+setCurrentContext :: ValidSignature -> ShellState -> ShellState
+setCurrentContext sig state = 
+  let l = getCurrentLanguageSubset state
+      d = concat . Map.elems . getAllDeclarations $ state
+      i = interpret d l sig
+   in state { getCurrentContext = Just (sig, i)
+            , getSpecialisationHistory = [] }
+
+
+
+-- Changes the current language subset.
+setCurrentLanguageSubset :: LanguageSubset -> ShellState -> ShellState
+setCurrentLanguageSubset l state =
+  case getCurrentContext state of
+    Nothing    -> state { getCurrentLanguageSubset = l }
+    Just (s,_) -> 
+      let h = getSpecialisationHistory state
+          d = concat . Map.elems . getAllDeclarations $ state
+          f i = either (specialise i) (specialiseInverse i)
+          i = fmap (\i -> foldl f i h) (interpret d l s)
+       in state { getCurrentContext = Just (s,i)
+                , getCurrentLanguageSubset = l }
+
+
+
+-- Adds a relation variable to the end of the specialisation history and 
+-- specialises the given relation variable in the current theorem.
+addSpecialisation :: 
+    Either RelationVariable RelationVariable -> ShellState -> ShellState
+addSpecialisation rv state =
+  case getCurrentContext state of
+    Nothing    -> state
+    Just (s,i) ->
+      let h  = getSpecialisationHistory state ++ [rv]
+          i' = fmap (\i -> either (specialise i) (specialiseInverse i) rv) i
+       in state { getCurrentContext = Just (s, i')
+                , getSpecialisationHistory = h }
+
+
+
+-- Reverts the last specialisation, if there is any.
+undoSpecialisation :: ShellState -> ShellState
+undoSpecialisation state = 
+  if null (getSpecialisationHistory state)
+    then state
+    else case getCurrentContext state of
+           Nothing    -> state
+           Just (s,_) -> let h = init (getSpecialisationHistory state)
+                             l = getCurrentLanguageSubset state
+                             d = concat . Map.elems . getAllDeclarations $ state
+                             f i = either (specialise i) (specialiseInverse i)
+                             i = fmap (\i -> foldl f i h) (interpret d l s)
+                          in state { getSpecialisationHistory = h
+                                   , getCurrentContext = Just (s, i) }
+
+
+
+
diff --git a/src/main.hs b/src/main.hs
new file mode 100644
--- /dev/null
+++ b/src/main.hs
@@ -0,0 +1,128 @@
+
+
+
+-- The main module of the application.
+-- Processes the command line and runs the shell.
+module Main where
+
+
+
+import Paths_ftshell (getDataFileName, version)
+
+import Data.Maybe (isNothing)
+import Data.Version (showVersion)
+import System.Console.GetOpt
+import System.Environment (getProgName, getArgs)
+
+import Settings 
+import Shell (initAndRunShell)
+
+
+
+-- The main entry point of the application.
+-- Processes the command line options.
+-- Shows help or version information, or starts the shell.
+main :: IO ()
+main = do
+  settings <- initialSettings >>= parseOptions
+  case insteadOfShell settings of
+    Just PrintHelp    -> printHelp
+    Just PrintVersion -> printVersion settings
+    Nothing           -> initAndRunShell settings
+
+
+
+
+
+------- Getting the options ----------------------------------------------------
+
+
+
+-- Possible command line option flags.
+data Flag
+  = ShowHelp            -- show the help message
+  | ShowVersion         -- show the version message
+  | LoadFile String     -- load an additional declarations file
+  | DontLoadPrelude     -- don't load the prelude file
+  deriving Eq
+
+
+
+-- The options menu.
+options :: [OptDescr Flag]
+options =
+  [ Option ['h'] ["help"] (NoArg ShowHelp)
+      "show this help message and exit"
+  , Option ['l'] ["load"] (ReqArg LoadFile "FILE")
+      "load an additional file of declarations"
+  , Option ['n'] ["no-prelude"] (NoArg DontLoadPrelude)
+      "don't load the basic file of declarations"
+  , Option ['v'] ["version"] (NoArg ShowVersion)
+      "show version information and exit"
+  ]
+
+
+
+-- Maps the options to the settings.
+parseOptions :: Settings -> IO Settings
+parseOptions settings = do
+  args <- getArgs
+  case getOpt Permute options args of
+    (os, _, []) -> return $ foldl apply settings os
+    (_,  _, es) -> do putStr (unlines es)
+                      return $ settings { insteadOfShell = Just PrintHelp }
+
+
+
+-- Applies one command line option to some given settings.
+apply :: Settings -> Flag -> Settings
+
+apply sets ShowHelp = sets { insteadOfShell = Just PrintHelp }
+
+apply sets ShowVersion = if isNothing (insteadOfShell sets)
+                           then sets { insteadOfShell = Just PrintVersion }
+                           else sets
+
+apply sets (LoadFile s) = sets { inputFiles = inputFiles sets ++ [s] } 
+
+apply sets DontLoadPrelude = sets { prelude = Nothing } 
+
+
+
+
+
+
+------- Printing messages ------------------------------------------------------
+
+
+
+-- Shows the available command line options.
+printHelp :: IO ()
+printHelp = do
+  progName <- getProgName
+  putStr $ usageInfo ("Usage: " ++ progName ++ " [OPTION]...") options
+  putStr $ unlines
+    [ ""
+    , "The application loads first the basic declarations file before every"
+    , "file specified by the `--load' option is loaded in the order given at"
+    , "the command line."
+    , ""
+    ]
+
+
+
+-- Shows the version and additional information.
+printVersion :: Settings -> IO ()
+printVersion sets = do
+  declFile <- getDataFileName basicDeclarationsFileName
+  putStr $ unlines 
+    [ "FTshell, version " ++ showVersion version
+    , "Automatic generation of free theorems"
+    , ""
+    , "Basic declarations file: " ++ declFile
+    , "Parser: " ++ parserName sets
+    , "Shell backend: " ++ backendName sets
+    , ""
+    , "Usage: For basic information, try the `--help' option."
+    ]
+