packages feed

ftshell (empty) → 0.2

raw patch · 12 files changed

+1797/−0 lines, 12 filesdep +Shellacdep +Shellac-readlinedep +basesetup-changed

Dependencies added: Shellac, Shellac-readline, base, containers, free-theorems, mtl, pretty

Files

+ LICENSE view
@@ -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.
+ README view
@@ -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.++
+ Setup.lhs view
@@ -0,0 +1,4 @@+#!/usr/bin/env runhaskell++> import Distribution.Simple+> main = defaultMain
+ declarations.hs view
@@ -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+++
+ ftshell.cabal view
@@ -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
+ src/Commands.hs view
@@ -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>"++++
+ src/Evaluate.hs view
@@ -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."++
+ src/HelpCommands.hs view
@@ -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."++++
+ src/Settings.hs view
@@ -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.+++
+ src/Shell.hs view
@@ -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"+  ]++
+ src/ShellState.hs view
@@ -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) }++++
+ src/main.hs view
@@ -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."+    ]+