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