ftshell-0.3: src/Commands.hs
-- 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
simp <- fromShellSt getSimplifyOutput
l <- fromShellSt getCurrentLanguageSubset
let pt = prettyTheorem opts $
(if simp && l `elem` [BasicSubset, SubsetWithFix EquationalTheorem]
then simplify
else id) $
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
simp <- fromShellSt getSimplifyOutput
l <- fromShellSt getCurrentLanguageSubset
let simpL = if simp && l `elem` [BasicSubset, SubsetWithFix EquationalTheorem]
then simplifyUnfoldedLift
else id
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 . simpL) 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)
simp <- fromShellSt getSimplifyOutput
if simp then shellPutStrLn "The output will be simplified, if possible."
else shellPutStrLn "The output will not be simplified."
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
-- Toggles the simplify output flag
cmdToggleSimplify :: Sh ShellState ()
cmdToggleSimplify = do
modifyShellSt $ \s -> s { getSimplifyOutput = not (getSimplifyOutput s) }
simp <- fromShellSt getSimplifyOutput
if simp then shellPutStrLn "The output will be simplified, if possible."
else shellPutStrLn "The output will not be simplified."
-- 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>"