import HatTrace
import HatTrie
import HatExpressionTree
import PrettyExp (showExpression,showReduction)
import HighlightStyle (highlight,Highlight(..),Colour(..))
import Maybe
import System
import Monad (when)
import List  (isPrefixOf)
import Char  (isDigit,digitToInt,toUpper)
import IO    (hFlush,stdout)

spawnObserveCmd = "xterm -e hat-observe-T "
spawnObserveEnd = "&"
spawnJavaCmd = "hat-trail-in-java "
spawnJavaEnd = "&"
spawnTrailCmd = "xterm -e hat-trail-T "
spawnTrailEnd = "&"

shortHelpText = ":h for help, :q to quit"

-----------------------------------------------------------------------
-- misc functions
-----------------------------------------------------------------------

checkArguments :: [String] -> Bool
checkArguments arguments =
    let l = length arguments in
    if l==1 then True
    else if l/=3 then False
    else head (tail arguments)=="-remote"

getStartReduction :: HatTrace -> [String] -> HatNode
getStartReduction hattrace arguments =
    if length arguments==3 then
       let adr = fromRemoteRep hattrace (head (drop 2 arguments)) in
       if isValidNode adr then adr else getStartReduction hattrace []
    else
       let maybeMainCAF = hatMain hattrace in
       if isInvalidNode maybeMainCAF then
	    error "Bad file format! \"main\" CAF could not be found!"
       else maybeMainCAF

upStr :: String -> String
upStr = map toUpper

main = do
    arguments <- getArgs
    if checkArguments arguments==False then
        putStrLn cmdlineHelpText
      else do
        let file = head arguments       -- first argument is file name
        maybehattrace <- openTrace file -- open Redex Trail file
        if isNothing maybehattrace then
	    putStrLn ("hat-detect\n\nError: cannot open file \""++file++"\".")
	  else do
	    let hattrace = fromJust maybehattrace
	        startReduction = getStartReduction hattrace arguments
	    putStrLn ("\n        hat-detect "++hatVersionNumber
                      ++" ("++shortHelpText++")\n")
            (b,e,newstate) <- interactive (file,hattrace)
                                          emptyState{children=[startReduction]}
            when (b && e> -1) (do putStrLn "Ok, no error found."
                                  _ <- getLine
                                  return ())


-- type for state of session
data State = State
	{ children    :: [HatNode]	-- current EDT children
	, recentNodes :: [(HatNode, LinExpr, Bool)] -- already considered nodes
	, trusted     :: [HatNode]	-- trusted fun-identifiers
	, postponed   :: [(Int,HatNode)]-- postponed questions
	, questnumber :: Int		-- current question number
	, cutoffdepth :: Int		-- cutoff depth for prettyPrinting
	, verboseMode :: Bool		-- verboseMode
	, memoMode    :: Bool		-- memoizeMode
	, reconsider  :: Bool		-- True when reconsidering a
	}				--   postponed question
emptyState :: State
emptyState = State
	{ children = []
	, recentNodes = []
	, trusted = []
	, postponed = []
	, questnumber = 1
	, cutoffdepth = 10
	, verboseMode = False
	, memoMode = True
	, reconsider = False
	}
setState :: Mode -> State -> State
setState (Verbose b) state = state {verboseMode=b}
setState (Memoise b) state = state {memoMode=b}
setState (CutOff n)  state = state {cutoffdepth=max n 1}
setState (Deeper n)  state = state {cutoffdepth=cutoffdepth state + n}
setState (Shallower n) state = state {cutoffdepth=max (cutoffdepth state - n) 1}

showState :: Mode -> State -> String
showState (Verbose _) state = highlight [Underscore] "verbose" ++" mode is "
                              ++ if verboseMode state then "active" else "off"
showState (Memoise _) state = highlight [Underscore] "memoisation" ++" mode is "
                              ++ if memoMode state then "active" else "off"
showState (CutOff _)  state = "expression "++highlight [Underscore] "cutoff"
                              ++" depth = "++ show (cutoffdepth state)
showState (Deeper _)  state = showState (CutOff 0) state
showState (Shallower _) state = showState (CutOff 0) state

showIdent :: HatNode -> String
showIdent node = hatCExpressionStr False 10 node

{-
-- This version does pretty-printing in C.
showRed :: Bool -> Int -> HatNode -> String
showRed verboseMode cutoff node =
    let s1 = hatCExpressionStr verboseMode cutoff node
	res = hatResult node
	s2 = if isValidNode res then
                  " = " ++ hatCExpressionStr verboseMode cutoff res
	     else ""
    in s1++s2
-}

showRed :: Bool -> Int -> HatNode -> String
showRed verboseMode cutoff node =
    prettyPrint cutoff verboseMode node ++ " = "
    ++ prettyPrint cutoff verboseMode (hatResult node)


-- Add new node to the list of recent nodes.  List holds node, linear
-- representation of it, and the value of the users answer (Yes=True, No=False)
addToRecentNodes :: [(HatNode,LinExpr,Bool)] -> HatNode -> Bool
                    -> [(HatNode,LinExpr,Bool)]

addToRecentNodes recentNodes node answerYes =
    (node, linearizeExpr (toHatExpressionTree 100 node), answerYes)
    : recentNodes

-- check, whether node is less general than an earlier given answer
memoizeCheck :: [(HatNode,LinExpr,Bool)] -> HatNode -> Maybe Bool
memoizeCheck recentNodes node =
    memoizeCheck' recentNodes (linearizeExpr (toHatExpressionTree 100 node))
  where
    memoizeCheck' [] _ = Nothing
    memoizeCheck' ((_,expr2,answer):recentNodes) expr1 =
        if compareExpr expr1 expr2 then Just answer
        else memoizeCheck' recentNodes expr1

interactive :: (String,HatTrace) -> State -> IO (Bool,Int,State)
interactive _ state
    | null (children state) && null (postponed state) =
        -- nothing else to do
        return (True,0,state)
interactive hatfile state
    | null (children state) && not (null (postponed state)) =
        -- take one postponed question as new current question
        interactive hatfile state {children=[node]
                                  ,questnumber=qn
                                  ,postponed=tail (postponed state)
                                  ,reconsider=False
                                  }
    where (qn,node) = head (postponed state)
interactive hatfile state | not (null (children state)) =
  let node = head (children state) -- ask about the next remaining EDT child
      answer = memoizeCheck (recentNodes state) node in
  if node  `elem`  map (\(a,_,_)->a) (recentNodes state)
      || (memoMode state && isJust answer)
  then if fromJust answer -- don't ask about identical(!) node in memoizemode
       then doCommand (Answer Yes) hatfile state -- pretend user answered "YES"
       else doCommand (Answer No)  hatfile state -- pretend user answered "NO"
  else if hatLeftmost node `elem` trusted state
       then doCommand (Answer Yes) hatfile state -- pretend user answered "YES"
       else do when (reconsider state) (putStrLn "reconsider: ")
               putStr (showReduction (verboseMode state) (cutoffdepth state)
                                     node 
                                     (highlight [Foreground Blue]
                                                (show (questnumber state)++" "))
                                     "? ")
               hFlush stdout
               cmd <- getCommand
               doCommand cmd hatfile state


getNumberParam :: String -> String -> String -> Maybe Int
getNumberParam cmd pattern1 pattern2 = 
    if length pattern1 < length pattern2
    then getNumberParam' cmd pattern2 pattern1
    else getNumberParam' cmd pattern1 pattern2
    where
     getNumberParam' cmd pattern1 pattern2 =
	 let com = upStr cmd in
         if take (length pattern1) com == pattern1
	 then stringToInt (drop (length pattern1) cmd)
	 else if take (length pattern2) com == pattern2
              then stringToInt (drop (length pattern2) cmd)
	      else Nothing

doCommand :: Cmd -> (String,HatTrace) -> State -> IO (Bool,Int,State)

doCommand Quit hatfile state = return (True,-1,state)
doCommand Help hatfile state =
     do putStrLn interactiveHelpText
        interactive hatfile state
doCommand Status hatfile state =
     do mapM_ (\m-> putStrLn (showState m state))
              [Verbose True,Memoise True,CutOff 0]
        interactive hatfile state
doCommand (Set mode) hatfile state =
     do	let state' = setState mode state
        putStrLn (showState mode state')
        interactive hatfile state'
----
doCommand Children hatfile state =
     do putStrLn ("children = "++show (children state))
        interactive hatfile state
doCommand Trust hatfile state = -- user defined function trusting
     do let child = head (children state)
            trustFun = hatLeftmost child
        putStrLn (showExpression trustFun "   Ok, \""
                  ++ "\" is trusted from now on.")
        (b,q,state') <- interactive hatfile state
				{recentNodes = addToRecentNodes
                                                   (recentNodes state)
                                                   child True
				,trusted = trustFun:trusted state
				,questnumber = questnumber state + 1
				,reconsider = False
				}
        if q/=questnumber state then return (b,q,state')
          else interactive hatfile state { cutoffdepth = cutoffdepth state'
                                         , verboseMode = verboseMode state'
                                         , memoMode = memoMode state'
                                         , reconsider = False
                                         }
doCommand Untrust hatfile state =
     do putStrLn "Ok, all functions are untrusted now."
        interactive hatfile state {trusted=[]}

---- answering the question: yes, no, ?yes, or ?no
doCommand (Answer Yes) hatfile state =
     do let child = head (children state)
        (b,q,state') <- interactive hatfile state
				{ children = tail (children state)
				, recentNodes = addToRecentNodes
							(recentNodes state)
							child True
				, questnumber = questnumber state + 1
				, reconsider = False
				}
        if q/=questnumber state then return (b,q,state')
	  else interactive hatfile state { cutoffdepth = cutoffdepth state'
                                         , verboseMode = verboseMode state'
                                         , memoMode = memoMode state'
                                         , reconsider = False
                                         }
doCommand (Answer QueryYes) hatfile state =
     do let child = head (children state)
        (b,q,state') <- interactive hatfile state
				{ children  = tail (children state)
				, postponed = postponed state ++
						[(questnumber state,child)]
				, questnumber = questnumber state + 1
				, reconsider = False
				}
        if q/=questnumber state then return (b,q,state')
	  else interactive hatfile state { cutoffdepth = cutoffdepth state'
                                         , verboseMode = verboseMode state'
                                         , memoMode = memoMode state'
                                         , reconsider = False
                                         }
doCommand (Answer No) hatfile state =
     do let child = head (children state)
	    newchildren = edtChildren child
        (b,q,state') <- interactive hatfile state
				{ children = newchildren
				, recentNodes = addToRecentNodes
							(recentNodes state)
							child False
				, postponed = []
				, questnumber = questnumber state + 1
				, reconsider = False
				}
        if q==questnumber state then
	       interactive hatfile state { cutoffdepth = cutoffdepth state'
                                         , verboseMode = verboseMode state'
                                         , memoMode = memoMode state'
                                         , reconsider = False
                                         }
          else if b && q==0 then
             do let lmo = hatLeftmost child
		    src = if isInvalidNode lmo then HatNoSourceRef
                                               else hatSourceRef lmo
                putStrLn ("\nErroneous reduction:\n"
		          ++ highlight [Foreground Blue]
                                       (showReduction (verboseMode state)
                                               (cutoffdepth state) child "" "")
                          ++ showExpression lmo
                                  "\nBug found within the body of function: \""
                          ++ "\"\n"
		          ++ "line "++show (row src)++", column "
			  ++ show (column src)
			  ++ " in module \"" ++ moduleName src
			  ++ "\", file: \"" ++ moduleFile src ++"\"")
		putStr ("\n:q to quit, any other key to go back to question "
                        ++ show (questnumber state) ++": ")
		cmd <- getCommand
		case cmd of
                    Quit -> return (False,-1,state')
                    _    -> interactive hatfile state
	  else return (b,q,state')

doCommand (Answer QueryNo) hatfile state | not (reconsider state) =
     do let child = head (children state)
	    newchildren = edtChildren child
        (b,q,state') <- interactive hatfile state
				{ children = newchildren
				, recentNodes = addToRecentNodes
							(recentNodes state)
							child False
				, postponed = []
				, questnumber = questnumber state + 1
				, reconsider = False
				}
        if q==questnumber state then
	       interactive hatfile state { cutoffdepth = cutoffdepth state'
                                         , verboseMode = verboseMode state'
                                         , memoMode = memoMode state'
                                         , reconsider = False
                                         }
          else if b && q==0 then
	              interactive hatfile state
					{ cutoffdepth = cutoffdepth state'
                                        , trusted = trusted state'
                                        , verboseMode = verboseMode state'
                                        , memoMode = memoMode state'
                                        , reconsider = True
                                        }
	  else return (b,q,state')
doCommand (Answer QueryNo) hatfile state | reconsider state =
     do putStrLn ("The question has already been deferred once.\n\
                  \You must answer it now with y/y?/n ")
        interactive hatfile state
doCommand (AskQuestion n) hatfile state =
        if n>0 && n<questnumber state then
	     return (False,n,state) -- return n, and ask question again
        else do putStrLn "No question with this number!"
	        interactive hatfile state
----
doCommand Application hatfile@(file,_) state = interactive hatfile state
doCommand Definition  hatfile@(file,_) state = interactive hatfile state
----
doCommand (StartTool Observe) hatfile@(file,_) state =
     do let child = head (children state)
            obsFun = hatLeftmost child
        errcode <- system (spawnObserveCmd++file++" -remote "
			   ++show (showIdent obsFun)++spawnObserveEnd)
     	when (errcode/=ExitSuccess)
	     (putStrLn ("ERROR: Unable to start hat-observe.\n\
                        \Check settings and availability of hat-observe."))
        interactive hatfile state
doCommand (StartTool Java) hatfile@(file,_) state =
     do let child = head (children state)
            lhsID = toRemoteRep child
	    rhsID = toRemoteRep (hatResult child)
	putStr "Trace left-hand-side (lhs) or rhs? (L/R): "
	lhs <- getLine
        errcode <- system (spawnJavaCmd++file++" -remote "
			      ++(if rhsID=="" || length lhs==0 ||
				   head (upStr lhs)/='R'
                                 then lhsID else rhsID)
                              ++spawnJavaEnd)
        when (errcode/=ExitSuccess)
	     (putStrLn "ERROR: Unable to start hat-trail-in-java.\n\
	 	       \Check settings and availability.")
        interactive hatfile state
doCommand (StartTool Trail) hatfile@(file,_) state =
     do let child = head (children state)
        errcode <- system (spawnTrailCmd++file++" -remote "
                           ++ toRemoteRep child ++ spawnTrailEnd)
        when (errcode/=ExitSuccess)
             (putStrLn "ERROR: Unable to start hat-trail.\n\
	               \Check settings and availability of hat-trail.")
        interactive hatfile state
----
doCommand _ hatfile state =
     do putStrLn ("Unknown command.  "++shortHelpText)
        interactive hatfile state
----


interactiveHelpText = "\
\---------------------------------------------------------------------------\n\
\ y   or  yes      you believe the equation is ok\n\
\ n   or  no       you believe the equation is wrong\n\
\ ?y  or  y?       you are not sure (but try ok for now)\n\
\ ?n  or  n?       you are not sure (but try wrong for now)\n\
\ <n>              go back to question <n>\n\
\ :set             show all current mode settings\n\
\ :set <flag>      change one mode setting\n\
\      <flag> can be: memoise [on|off]:  never ask the same question again\n\
\                     verbose [on|off]:  show unevaluated exprs in full\n\
\                     cutoff <n>:        set subexpression cutoff depth\n\
\ :observe         start hat-observe on the current function\n\
\ :trail           start hat-trail on the current equation\n\
\ :trust           trust all applications of the current function\n\
\ :untrust         untrust ALL functions which were previously trusted\n\
\ :help  :?        show this help text\n\
\ :quit            quit\n\
\---------------------------------------------------------------------------"

{-
\ :application     show the source application site for this equation\n\
\ :definition      show the source definition for this equation\n\
-}

cmdlineHelpText =
   "usage: hat-detect file-name\n"
   ++"       algorithmic debugging on a hat (redex trail) trace file"


data Cmd = Answer Answer | AskQuestion Int
         | Status | Set Mode
         | Trust  | Untrust  | Children
         | StartTool Tool | Application | Definition
         | Help   | Quit | Unknown
data Answer = Yes | No | QueryYes | QueryNo
data Mode = Verbose Bool | Memoise Bool
          | CutOff Int | Deeper Int | Shallower Int
data Tool = Trail   | Observe | Java

getCommand :: IO Cmd
getCommand = do
    s <- getLine
    if null s then return Unknown
      else if all isDigit s then return (number AskQuestion [s] 0)
      else if head s `elem` "yYnN?" then return (answer (map toUpper s))
      else if head s /= ':' then return Unknown
      else case words (tail s) of
          [] -> return Unknown
          (cmd:ss)
              | cmd `isPrefixOf` "quit" -> return Quit
              | cmd `isPrefixOf` "help" -> return Help
              | cmd `isPrefixOf` "trust"   -> return Trust
              | cmd `isPrefixOf` "untrust" -> return Untrust
              | cmd `isPrefixOf` "**"      -> return Children
              | cmd `isPrefixOf` "observe" -> return (StartTool Observe)
              | cmd `isPrefixOf` "trail"   -> return (StartTool Trail)
              | cmd `isPrefixOf` "java"    -> return (StartTool Java)
              | cmd `isPrefixOf` "application" -> return Application
              | cmd `isPrefixOf` "definition"  -> return Definition
              | cmd `isPrefixOf` "set" ->
                  case ss of
                    [] -> return Status
                    (m:sss)
                        | m `isPrefixOf` "verbose" -> return (onOff Verbose sss)
                        | m `isPrefixOf` "memoise" -> return (onOff Memoise sss)
                        | m `isPrefixOf` "memoize" -> return (onOff Memoise sss)
                        | m `isPrefixOf` "cutoff"  ->
                                        return (number (Set . CutOff) sss 10)
                        | otherwise -> return Unknown
              | head cmd == '?' -> return Help
              | head cmd == '+' ->
                          return (number (Set . Deeper) (tail cmd:ss) 1)
              | head cmd == '-' ->
                          return (number (Set . Shallower) (tail cmd:ss) 1)
              | otherwise  ->  return Unknown

onOff :: (Bool->Mode) -> [String] -> Cmd
onOff mode s | null s = Set (mode True)
             | otherwise = case head s of "on" -> Set (mode True)
                                          "active" -> Set (mode True)
                                          "off" -> Set (mode False)
                                          "no" -> Set (mode False)
                                          _ -> Unknown

-- answer expects some partial checking of the string to have been done already
answer :: String -> Cmd
answer "Y"   = Answer Yes
answer "N"   = Answer No
answer "YES" = Answer Yes
answer "NO"  = Answer No
answer "Y?"  = Answer QueryYes
answer "N?"  = Answer QueryNo
answer "?Y"  = Answer QueryYes
answer "?N"  = Answer QueryNo
answer _     = Unknown

-- number builds a Cmd with a number - if no valid number is found, use def
number :: (Int->Cmd) -> [String] -> Int -> Cmd
number cons s def = (maybe (cons def) cons . stringToInt . unwords) s

stringToInt :: String -> Maybe Int
stringToInt s = stringToInt' True 0 s
 where
  stringToInt' True _ ('#':r) = stringToInt' True 0 r -- skip "#" at beginning
  stringToInt' True _ (' ':r) = stringToInt' True 0 r -- skip " " at beginning
--stringToInt' False i (' ':r) = Just i
  stringToInt' first i [] = if first then Nothing else  Just i
  stringToInt' _ i (c:r)
      | isDigit c = stringToInt' False (i*10+(digitToInt c)) r
      | otherwise = Nothing

{-
stringToInt :: String -> Maybe Int
stringToInt s = stringToInt' True 0 s
 where
  stringToInt' True _ (c:r)
      | not (isDigit c) = stringToInt' True 0 r -- skip alphas at beginning
--stringToInt' False i (' ':r) = Just i
  stringToInt' first i [] = if first then Nothing else  Just i
  stringToInt' _ i (c:r)
      | isDigit c = stringToInt' False (i*10+(digitToInt c)) r
      | otherwise = Nothing
-}