module Igor2.UI.UIStarter where

import Prelude hiding ((<$>))

import Text.ParserCombinators.Parsec hiding (space, char)
import qualified Text.ParserCombinators.Parsec.Token as T 
import Text.ParserCombinators.Parsec.Language( emptyDef, haskellDef, GenLanguageDef(..) )
import Control.Monad (when, liftM4)
import Control.Monad.Error (catchError, Error)
import System.Directory (doesFileExist, doesDirectoryExist)
import System.Environment
import System.Exit
import System.CPUTime
import System.IO

import Text.Printf


import Data.Time.Clock
import Data.Time.LocalTime
import Data.Time.Calendar
import Data.Function (on)
import Data.Maybe (isJust, fromJust, mapMaybe)
import qualified Data.Map as M
import qualified Data.Set as S

import Syntax
import Syntax.Specification
import Igor2.Config
import Igor2.Data.Rules
import Igor2.UI.REPLoop
import Igor2.UI.Help
import Igor2.SynthesisEngine
import Igor2.Logging
import IOInterpreter
import Igor2.Ppr hiding (integer)

import Debug.Trace

version :: String
version = "v0.8"

prompt :: String
prompt = "IgorII > "

displayWidth = 120

render s x = renderPretty 0.95 (fromInteger.colWidth $ s) x
renderStatic x = renderPretty 0.95 displayWidth x
display s x = displayIO stdout (render s x)
displayStatic x = displayIO stdout (renderStatic x)

 

--------------------------------------------------------------------------------
-- not nice to have two optiuon recordsm one for the UI, and one for Igor
data EnvState = EState 
    { config :: SCR
    , typeCheck :: Bool
    , dumpDir   :: String
    , colWidth  :: Integer
    , context   :: !Specification
    , history   :: M.Map ([Name],[Name]) [String]  
    }
    deriving (Show)
             
ctxFile   = scr_ctxFile . config
debug     = scr_debug . config
simplify  = scr_simplify . config
enhanced  = scr_enhanced . config
para      = scr_para . config
greedySplt = scr_greedySplt . config
accum     = scr_accum . config
greedyMtch = scr_greedyMtch . config
dumpLog   = scr_dumpLog . config
verbose   = scr_verbose . config
verbosity = scr_verbosity . config
maxLoops  = scr_maxLoops . config
maxTiers  = scr_maxTiers . config
redOrder  = scr_redOrder . config


modifyHistory :: (Pretty a) => EnvState -> ([Name],[Name]) -> [[[a]]] -> EnvState
modifyHistory s k v = 
    let v' = map (unlines.(map (show.pretty))) (head v)
    -- TODO : Now only the first tier of results ist stored in history
    in s{history = M.insert k v' (history s)}
    
examplesInScope :: EnvState -> [(Name,Rules)]
examplesInScope = (map (\(m,es) -> (m, mkRules es))) . M.toList . spec_bindings . context
                   
defaultState :: EnvState
defaultState = EState
    { config = defaultSCR
    , typeCheck = True
    , dumpDir   = "."
    , colWidth  = 80
    , context   = defaultSpec
    , history   = M.empty
    }   
    

genRepl :: EnvState -> REPL EnvState
genRepl state = REPL {
    repl_init = return (prompt,state),
    repl_eval = eval,
    repl_exit = exit
    }

    
runInteractive :: IO ()
runInteractive = do
    sayHello True
    readEvalPrintLoop (genRepl defaultState)
   
runBatch :: Bool -> FilePath -> IO ()
runBatch noBanner file = do
    when (not noBanner) $ sayHello False
    putStrLn $ "Running IgorII in batch mode with file: " ++ file
    (q,state') <- loadBatch defaultState file
    putStrLn $ "...batch processing finished."
    if q then exit state'
      else readEvalPrintLoop (genRepl state')      
    
runCmdLine :: Bool -> [String] -> IO ()
runCmdLine noBanner cmd = do
    when (not noBanner) $ sayHello False
    eval defaultState (unwords cmd) >>= exit.snd
    

eval :: EnvState -> String -> IO (Bool, EnvState)
eval s line = 
    case parseCmdLine line of
        Right r  -> foldUntil runCmd s r
        Left msg -> do{ putStrLn ("Unknown input " ++ msg) >>
                        return (False, s)}


exit :: EnvState -> IO ()
exit _s = do
    putStrLn "Bye."
    exitWith ExitSuccess  

--------------------------------------------------------------------------------
-- 
runCmd :: EnvState -> Cmd -> IO (Bool, EnvState)
runCmd s Noop                   = return (False, s)
runCmd s Quit                   = return (True, s)
runCmd s (Help verbose)         = printHelp s verbose
runCmd s (SetOpt f)                = return (False, f s) 
runCmd s Info                   = display s (getSettings s) >> return (False,s)
runCmd s (Batch path)           = loadBatch s path
runCmd s (Load path)            = loadFile s path
runCmd s (Generalise tgts bgks) = startIgor s tgts bgks
runCmd s (Test i tgts bgks expr)= evalExpr s i (tgts,bgks) expr >> return (False,s)
runCmd s Reset                  = return (False, defaultState)
runCmd s (Yell st)              = yell s st >> return (False,s)
   
foldUntil :: (Monad m) => (a -> b -> m (Bool,a)) -> a -> [b] -> m (Bool,a)
foldUntil f state []     = return (False,state)
foldUntil f state (l:ls) = do
    qs@(q, state') <- f state l
    if q then return qs
     else foldUntil f state' ls
  
sayHello :: Bool -> IO ()
sayHello isInteractive = do 
    displayStatic igorLogo
    putStrLn $ "Welcome to IgorII. "
    when isInteractive $ putStrLn $ "Type :h to get help."
                 
igorLogo :: Doc
igorLogo = text $ "\
\\n\
\  .___                   ._ ._             \n\            
\  |   | ____  ____ ._____| || |  ._       \n\
\  |   |/ __ \\/  _ \\|  __ \\ || | _| |__ \n\ 
\  |   / /_/  ) <_> )  | \\/ || |/_   _/   \n\
\  |___\\___  /\\____/|__|  |_||_|  |_|    \n\
\     /_____/                " ++ version ++ "\n\n" 

printHelp :: EnvState -> Bool -> IO (Bool, EnvState)
printHelp s verbose = do
    showHelp 
    when verbose $ display s verboseHelp
    return (False, s)

-- Show the simple (non-verbose) help
showHelp :: IO () 
showHelp = displayStatic $ helpText
    where
    helpText = linebreak <> 
               bold (text "Interactive commands (may be abbreviated):") <$$>
               bold (text "==========================================") <$$> 
               vcat (map getHelp commands) <$$>
               linebreak


usage :: IO ()
usage = putStrLn "Usage: igorII [path/to/batch/file]"

yell s st = display s (blue (text "Igor says:") <+> text st <> linebreak) 
      
loadBatch :: EnvState -> String -> IO (Bool, EnvState)
loadBatch s p =
    (checkFile p >> readFile p >>= (foldUntil eval s) . lines . stripComments)
     `catchError` 
    (\e -> reportError ("Failed to load file:") e >> return (False,s))
   
-- strips comments '--' until the end of line '\n'
stripComments :: String -> String
stripComments "" = ""
stripComments ('-':'-':cs) = skip cs
  where skip "" = ""
        skip s@('\n':_) = stripComments s
        skip (_:s) = skip s
stripComments (c:cs) = c : stripComments cs       
    
      
      
loadFile :: EnvState -> String -> IO (Bool, EnvState)
loadFile s p = ( time (checkFile p >> when (typeCheck s) (typecheck  p) >>
                 parseSpec p) >>= \(ctx,d) -> 
                  putDoc (text "File loaded in" <+> d) >> 
                  return (False,s{context=ctx, config=(config s){scr_ctxFile=p}})
               ) `catchError` (\e -> 
                 reportError ("Failed to load file:") e >> 
                 return (False,s)
               )

evalExpr :: EnvState -> Int -> ([Name],[Name]) -> String -> IO ()
evalExpr s i k@(ts,bs) e = do
    
    let tdefs = M.lookup k (history s)
    let bdefs = mapMaybe ((flip M.lookup (history s)).(flip(,)[]).(:[])) bs 
              -- do not use I/O for BK, so try to get bk functions from history, 
    if (not.isJust $ tdefs) then printerr  >> return ()
       else do let d =  map concat $ sequence $ (fromJust tdefs):bdefs
               if (i < 1) || (i > (length d))
                 then mapM_ (test e d) [1..(length d)]
                 else test e d i 
    where
    -- test 'i'th hypotheses
    test e d i = ( do r <- (interprete (ctxFile s) $ prepare (d !! (i-1)) e) 
                      hPutDoc stdout $ text "Testing" <+> int i <> 
                                     text ". hypothesis" <+> text "of:" <+> 
                                     setDoc <^> text e <+> text " == " <+> 
                                     text r <$> linebreak 
                  ) `catchError` (\e -> reportError "" e)
               
    prepare d c = "let " ++ (concatMap (++ "; ") (lines d)) ++ "in " ++ c
    printerr = reportError "No such setting in history:" setDoc
    setDoc = encloseSep squote squote comma (map pretty ts) <> 
             (if not.null $ bs 
                then empty <+> text "with" <+> encloseSep squote squote comma (map pretty bs)
                else text "")
              
startIgor :: EnvState -> [Name] -> [Name] -> IO (Bool,EnvState)
startIgor s tgts bgks =
    let conf = (setTargets tgts) . (setBackground bgks) . config $ s
        exmpls = liftM2 (,) (getBindings tgts (context s))(getBindings bgks (context s)) 
    in case exmpls of
        Left msg      -> reportError "" msg >> return (False, s)
        Right (ts,bs) -> do
          (res, t) <- withLogState s conf (\logstate -> time (startSynthesis (spec_ctx $ context s) conf logstate ts bs))
          let s' = either (const s) (modifyHistory s (tgts, bgks) . snd) res
          printResult s' conf t res
          return (False, s')


time :: IO a -> IO (a, Doc) 
time ioa = do
    t1 <- getCPUTime
    a <- ioa
    t2 <- getCPUTime
    let t :: Double
        t = fromIntegral (t2-t1) * 1e-12
    return $ (a , text (printf "%6.4fs" $ if t == 0 then 0.0001 else t) <>linebreak)

date :: IO (Integer,Int,Int,TimeOfDay) -- :: (year,month,day,CPUTime)
date = do
       (y,m,d) <- getCurrentTime >>= return . toGregorian . utctDay
       t       <- getZonedTime >>= return . localTimeOfDay . zonedTimeToLocalTime 
       return (y,m,d,t)

showDate = date >>= \(y,m,d,s) ->
             return $ (shows y).(addzero m).(shows m).(addzero d).(shows d).(showChar '_') $ show s
             where
             addzero m = if m <= 9 then shows 0 else id

printResult :: (Pretty a) =>  EnvState -> SCR -> Doc
            -> Either String ([(Name, Int)], [[[a]]]) -> IO ()
printResult s c t rs = do
    let w   = fromInteger $ colWidth s
    let res = resToDoc w t rs
    hPutDoc stdout $ introBanner <$$> pretty c <$$> res

withLogState :: Pretty a => EnvState -> SCR -> (LogState -> IO a) -> IO a
withLogState s c action = do
    if dumpLog s then do
        checkDir (dumpDir s)
        name <- showDate
        let file = dumpDir s ++ "/" ++ name ++ ".log"
        fhandle <- openFile file AppendMode
	let bannerWidth = fromInteger (colWidth s)
	renderLog fhandle $ introBanner <$$> pretty c <$$> logBanner bannerWidth
        result <- action . hToLogState $ Just fhandle
	renderLog fhandle $ resBanner bannerWidth <$$> pretty result
        hClose fhandle
        return result
      else action $ hToLogState Nothing
    where hToLogState = mkLogState (verbosity s) (verbose s)
          renderLog fhandle = displayIO fhandle . renderPretty 0.5 140

reportError :: (Show a) => String -> a -> IO ()                  
reportError s e = putDoc $ align ( (red. text $ "ERROR:") <+> 
                           vsep (text s : (map text (lines . show $ e))) <> 
                           linebreak)

logBanner w = frame w "Log  Log  Log  Log  Log  Log"
resBanner w = frame w "Results  Results  Results  Results"
introBanner = linebreak <> 
              indent 6 (bold (text "- - - - START SYNTHESIS WITH" <+> 
                              text "- - - -")) <> linebreak
outroBanner = indent 6 (bold (text "- - - - - - - FINISHED" <+> 
                              text "- - - - - - -"))
                              
resToDoc :: (Pretty a) => 
           Int -> Doc -> Either String ([(Name,Int)],[[[a]]]) -> Doc
resToDoc w t (Left msg) = 
  outroBanner <$$> (red . text $ "UNCAUGHT ERROR: " ++ msg ++ "\n")
resToDoc w t (Right (ls,ts)) = 
    outroBanner <$$>
    (foldl printLoop (text "    loops" ) ls) <$>
    (indent 13 $ text "CPU:" <+> t) <$>
    if null ts then (indent 7 $ red $ text "NO RESULTS! Exhausted Searchspace!") <$> linebreak
     else vcat (map (printTier (length ts)) (zip ts [1..]))
    where
    printLoop d (n,i) = linebreak <> 
                        indent 13 (fill 12 (pretty n) <+>
                        text "in" <+> int (i-1)) <+> d
printTier :: (Pretty a) => Int -> ([[a]],Int) ->  Doc
printTier 1 (hs,i) = vcat (map (printHypo (length hs)) (zip hs [1..])) 
printTier j (hs,i) = linebreak <> 
                     (bold (text "TIER" <+> int i <+> text "of" <+> int j)) <$$>
                     vcat (map (printHypo (length hs)) (zip hs [1..]))  <$$>
                     linebreak  
printHypo :: (Pretty a) => Int -> ([a],Int) ->  Doc    
printHypo j (d,i) =  linebreak <> 
                     indent 17 (bold (text "HYPOTHESIS" <+> int i <+> 
                                text "of" <+> int j)) <$$>
                     linebreak <> 
                     vcat (map pretty d) <$$>
                     linebreak 
                        
                         
frame w s = vsep [line,header s,line,softline]
    where
    line     = text "*" <> filler w '-' 2 <> text  "*"
    header s = text "|" <> center w s 2 <> text "|"    

textLine w str offset = filler w '-' (length str + 1 + offset) <+> text str
filler w c offset = hcat (replicate (w - offset) (char c))
center w str offset = spaces <> text str <> spaces
    where
    spaces = hcat $ replicate ((w - (length str) - offset) `div` 2) space 


--------------------------------------------------------------------------------
-- Commands
--------------------------------------------------------------------------------


data Cmd
 = Quit
 | Noop
 | Batch FilePath
 | Load FilePath
 | SetOpt (EnvState -> EnvState)
 | Reset
 | Generalise [Name] [Name]
 | Test Int [Name] [Name] String
 | GenAndTest Int [Name] [Name] String
 | Info
 | Yell String
 | Help Bool    
 
commands :: [(String, String, Parser Cmd)]
commands =
    [ (":quit",
            "Quit program.",                  return Quit)
    , (":help",
            "Show this help.",                return (Help False))
    , (":verboseHelp",
            "Show verbose help.",             return (Help True))
    , (":load <path/to/file>",
            "Load a spec file into context.", pIdentifier Load)
    , (":reset",
            "Reset the current context.",     return Reset)
    , (":batch <path/to/file>",
            "Run a batch file",               pIdentifier Batch)
    , (":yell \"something\"",
            "Yell on command line.",          pString Yell)
    , (":set <option>",
            "Set options.",                   pSetOpt)
    , (":info",
            "Show current settings.",         return Info)
    , (":generalise <tgts> [with <bgks>]",
            "Start generalisation.",          pStart)
    , (":test [<i>] <tgts> [with <bgks>] on \"expr\"",
            "Test a generalised program.",    pTest)
    ]

-- clip tailing arguments from command info and generate a shortcut    
clipCommand :: String -> [String]
clipCommand = (\s@(c:c':_) -> [(c:c':[]),s]) . head. words
     
getHelp :: (String, String, a) -> Doc
getHelp (cmd, help, _) =
    hang 45 $ (fill 45 (text cmd)) <> fillSep (map text (words help))

flags :: [(String, String, EnvState->Bool, Bool->EnvState->EnvState)]
flags = 
    [ ("debug",             "debug mode",
            debug,     \ v s -> s{ config=(config s){scr_debug = v }})
    , ("verbose",           "be verbose",
            verbose,   \ v s -> s{ config=(config s){scr_verbose = v }})
    , ("dumpLog",           "dump log to file",
            dumpLog,   \ v s -> s{ config=(config s){scr_dumpLog  = v }})
    , ("simplify",           "simplify the final hypotheses",
            simplify,  \ v s -> s{ config=(config s){scr_simplify  = v }})
    , ("greedySplt",           "enable greedy rule-splittinge",
            greedySplt,  \ v s -> s{ config=(config s){scr_greedySplt  = v }})
    , ("accum",             "introduce accumulator variables",
            accum,     \ v s -> s{ config=(config s){scr_accum  = v }})
    , ("greedyMtch",        "greedily match calls",
            greedyMtch, \ v s -> s{ config= (config s) {scr_greedyMtch = v}})
    , ("enhanced",           "synthesise in enhanced mode",
            enhanced,  \ v s -> s{ config=(config s){scr_enhanced  = v }})
    , ("para",           "use paramoprhisms instead of catamorphisms",
            para,  \ v s -> s{ config=(config s){scr_para  = v }})
    , ("typeCheck",           "force to type check the specification",
            typeCheck, \ v s -> s{ typeCheck  = v })
    ] 
   
intOptions :: [(String, String, EnvState->Integer, Integer->EnvState->EnvState)]
intOptions = 
    [ ("colWidth",          "Set the column width of your display",
            colWidth,  \ v s -> s{ colWidth = v}),
      ("maxLoops",          "Stop synthesis after 'n' cycles",
            maxLoops,  \ v s -> s{ config=(config s){scr_maxLoops = v}}),
      ("maxTiers",          "Return the first 'n' tiers of closed programs",
            maxTiers,  \ v s -> s{ config=(config s){ scr_maxTiers = v}}),
      ("verbosity",         "Set the verbosity level from 4(all) to 0 (errors only)",
            verb2Int.verbosity,  \ v s -> s{ config=(config s){scr_verbosity = int2Verb v}})
    ]
   
strOptions :: [(String, String, EnvState->String, String->EnvState->EnvState)]
strOptions = 
    [ ("dumpDir", "Directory log files are dumped to",
            dumpDir,  \ v s -> s{ dumpDir = v}),
      ("redOrder", "Reduction order, how to compare recursive arguments to ensure termination",
            show.redOrder,  \ v s -> s{ config=(config s){scr_redOrder = read v}})
    ]          


getSettings :: EnvState -> Doc
getSettings s = 
    linebreak <> 
    center w "Current settings" 0 <$>
    textLine w "Flags" 0 <$> showEntries flags  <$>
    textLine w "Options" 0  <$> showEntries intOptions
                            <$> showEntries strOptions <$>
    textLine w "Examples in Scope" 0 <$> 
        indent 2 (fill 15 (text "Name") <> 
                    (text (if beVerbose then "" else "#"))
                    <> text "Examples") <$>
        indent 2 (text $ replicate 25 '-' ) <$>
        indent 2 (vcat $ map showExample  (examplesInScope s))  <$>
    if beVerbose
      then pretty (context s) <$> text "History :" <$>  pretty (history s) <$> linebreak
      else text ""  <$> linebreak
    where
    w = (fromInteger.colWidth $ s)
    beVerbose = verbose s
    showEntry name value descr = 
        hang 30 $ fill 30 ((fill 15 (text name) <> text " = ") <> 
                        text (show value)) <> 
                        fillSep (map text (words descr)) 
    showEntries entries = 
        indent 2 $ vcat [ showEntry name (getter s) descr |
                         (name,descr,getter,_setter) <- entries]
    showExample (n,r) = 
        fill 30 ((fill 15 (pretty n) <+> text "|->") <+> 
                  if beVerbose then pretty r else int $ S.size r )
                      
--------------------------------------------------------------------------------
-- parsing commandline strings to commands
--------------------------------------------------------------------------------

-- my own token parser
lexer :: T.TokenParser ()
lexer = T.makeTokenParser
         (haskellDef
         { reservedNames   = concat [ clipCommand c| (c,_,_) <-  commands] ++
                             [ f | (f,_,_,_) <-  flags]++
                             [ o | (o,_,_,_) <-  intOptions]++
                             [ o | (o,_,_,_) <-  strOptions]
         , reservedOpNames = [":",";", "with", "on"]
         , identLetter    = alphaNum <|> oneOf "-+_'.~/" 
         , identStart     = alphaNum <|> oneOf "-+_'.~/" 
         
         })

-- shortcuts         
whiteSpace    = T.whiteSpace lexer
semiSep1      = T.semiSep1 lexer
commaSep1     = T.commaSep1 lexer
reserved      = T.reserved lexer
reservedOp    = T.reservedOp lexer
stringLiteral = T.stringLiteral lexer
integer       = T.integer lexer
identifier    = T.identifier lexer
--symbol        = T.symbol lexer

parseCmdLine :: String -> Either String [Cmd]
parseCmdLine = either (Left . show) Right . parse pBatch ""
-- parser rules

-- pBatch ::= pCommand (; pCommand)*
pBatch :: Parser [Cmd]
pBatch = do{ whiteSpace
           ; x <- semiSep1 pCommand
           ; eof
           ; return x
           }
       <?> "cmd1; cmd2; ... ; cmdN\nType :h to get help!"

-- pCommand ::= eof | Quit | Help | ...
pCommand :: Parser Cmd
pCommand = do{ eof
             ; return Noop
             }
       <|> choice [ do{ choice $ map reserved (clipCommand c) ; p} | 
                                    (c,_,p) <- commands]
       <?> "<command>"
             
pSetOpt :: Parser Cmd
pSetOpt =  do cmds <-  many1 (choice [pFlag, pIntOption, pStrOption])
              return $ foldl1 compose cmds
    where
    compose (SetOpt f) (SetOpt g) = SetOpt (g . f)         
         
pFlag :: Parser Cmd
pFlag = do{ reservedOp "+"
          ; setter <- choice [ do{reserved f; return $ s True} 
                            | (f,_,_,s) <- flags]
          ; return $ SetOpt setter
          }
    <|> do{ reservedOp "-"
          ; setter <- choice [ do{ reserved f; return $ s False} 
                                    | (f,_,_,s) <- flags ]
          ; return $ SetOpt setter
          }
    <?> ":set s[+|-]<flag>"             
          
pIntOption :: Parser Cmd
pIntOption = do{ f <- choice [ do{reserved o; return s} 
                            | (o,_,_,s) <- intOptions]
               ; i <- choice [ reservedOp "=" >> integer
                            , reservedOp "=-" >> integer >>= return .(*(-1))
                            , reservedOp "=+" >> integer ]
               ; return $ SetOpt (f i)
               } 
         <?> ":set <option>=<value>"
          
pStrOption :: Parser Cmd
pStrOption = do{ f <- choice [ do{reserved o; return s} 
                            | (o,_,_,s) <- strOptions]
               ; reservedOp "="
               ; i <- stringLiteral
               ; return $ SetOpt (f i)
            }
   <?> ":set <option>=<value>"

pString, pIdentifier :: (String -> Cmd) -> Parser Cmd
pString c = stringLiteral >>= return . c
pIdentifier c = identifier >>= return . c

pName = liftM mkName $ identifier
pNames = commaSep1 pName


pStart :: Parser Cmd
pStart = do{ targets <- pNames
           ; bgkldg  <- liftM (maybe [] id) $ optionMaybe (do{reservedOp "with"; pNames})
           ;return $ Generalise targets bgkldg
           }
     <?> ":generalise <t1,t2 ...> [with <b1,b2 ...>]"
          

pTest :: Parser Cmd
pTest = do{ i       <- liftM (maybe 0 fromInteger) $ optionMaybe integer
          ; targets <- pNames
          ; bgkldg  <- liftM (maybe [] id) $ optionMaybe (do{reservedOp "with"; pNames})
          ; exprssn <- do{reservedOp "on"; stringLiteral}
          ; return $ Test i targets bgkldg exprssn
           }
     <?> ":test <i> <t1 t2 ...> [with <b1 b2 ...>] on \"expression\""            

