-- module HatExplore where import LowLevel (FileNode(..),openHatFile,nil,unevaluated,entered,interrupted ,NodeType(..),nodeType ,peekResult,peekSubExprs,peekExpArg,getParentNode ,hiddenChildren,getSrcRef,getDefnRef,getErrorLoc ,hatVersionNumber) import qualified SrcRef (SrcRef(..)) import SrcRef (readSrcRef,defnSrcRef) import Ident (Ident,getIdentAt) import SExp (prettyEquation2) import CommonUI (Options,initialOptions) import Detect (findMain) import CommonUI (safeReadInt,hatObserve,hatTrail,hatDetect,hatAnim) import HighlightStyle import System.IO (hSetBuffering,BufferMode(..),stdin,stdout,stderr,hPutStrLn) import Foreign.C.String (withCString) import Numeric (showHex) import System.IO.Unsafe (unsafePerformIO) import System.Cmd (system) import System.Environment (getArgs,getProgName,getEnv) import System.Exit (exitWith,ExitCode(..)) import Data.List (isSuffixOf,sortBy,partition,union) import Control.Monad (liftM) import Data.Char (isAlpha) import Explore (Coord(..),noCoord,isNoCoord,isNextCoord,beforeCoord ,afterCoord,Row,Col ,Location(..),isVirtLocation,isNoLocation ,isImproperLocation,mkLocation,getLocation,hasUseLocation ,getDefLocation,getUseLocation ,redexParent) main = do hatFile <- initHatFile startNode <- determineStartNode startInteraction startNode printNodes :: String -> [FileNode] -> IO () -- for testing only printNodes str nodes = putStrLn (str ++ ':' : foldr myShow "" (map int nodes)) where myShow i xs = ',' : showHex i xs showNode :: FileNode -> String showNode = flip showHex "" . int initHatFile :: IO FilePath initHatFile = do prog <- System.Environment.getProgName hatFile <- determineHatFile withCString prog (\p-> withCString hatFile (openHatFile p)) return hatFile determineHatFile :: IO FilePath determineHatFile = do args <- System.Environment.getArgs case args of (f:_) -> return (rectify f) _ -> do hPutStrLn stderr ("error: no trace file") exitWith (ExitFailure 1) where rectify :: FilePath -> FilePath rectify f | ".hat" `isSuffixOf` f = f | otherwise = f ++ ".hat" dropHS :: FilePath -> FilePath dropHS f = case reverse f of 's':'h':'.':name -> reverse name 's':'h':'l':'.':name -> reverse name getErrorRedex :: IO FileNode -- determine the redex that caused a runtime error -- if no runtime error then return nil getErrorRedex = do errRedex <- getErrorLoc -- careful, might be nil, Hidden or trusted return (firstWithSrcRef errRedex) firstWithSrcRef :: FileNode -> FileNode -- return redex or first ancestor in traced code that has source reference -- redex may be nil, Hidden, or in trusted code (then has hidden parent) firstWithSrcRef redex = if redex /= nil && (getSrcRef redex == nil || isHidden (redexParent redex)) then firstWithSrcRef (redexParent redex) else redex determineStartNode :: IO FileNode -- either Main.main or passed as first argument determineStartNode = do maybeNode <- getArgumentNode 1 case maybeNode of Just node -> return node Nothing -> do errRedex <- getErrorRedex if errRedex /= nil then return errRedex else do mainNode <- findMain if mainNode == LowLevel.nil then do putStrLn "Could not find \"Main.main\"!" exitWith (ExitFailure 1) else return mainNode getArgumentNode :: Int -> IO (Maybe FileNode) -- get node from nth program argument, if it exists getArgumentNode argNo = do arguments <- System.Environment.getArgs return $ if length arguments <= argNo then Nothing else case safeReadInt 0 (arguments!!argNo) of 0 -> Nothing i -> let node = (FileNode i) in if expIsRedex node then Just node else let parent = redexParent node in if parent == nil then Nothing else Just parent -- if given node is not a redex try its parent -------------------------------------------------------------------- traverseReduct :: FileNode -> (Slice,[FileNode],[FileNode]) -- given node of redex determine -- slice that covers part of reduct that *may* have been demanded (approxim.) -- edt-children (demanded redexes (applications)) -- cafs (shared children) traverseReduct redex = if reduct `elem` [LowLevel.nil,unevaluated,entered,interrupted] then (emptySlice,[],[]) else go reduct emptySlice where (parent,reduct) = case nodeType redex of ExpConstUse -> let constDef = peekExpArg redex 0 constRes = peekResult constDef in if constRes `notElem` [nil,unevaluated,entered,interrupted] then case nodeType constRes of ExpProjection -> let projParent = getParentNode constRes in if projParent /= constDef then (getParentNode projParent,projParent) -- pattern binding else (constDef,constRes) _ -> (constDef,constRes) else (constDef,constRes) _ -> (redex,peekResult redex) gos :: [FileNode] -> Slice -> (Slice,[FileNode],[FileNode]) gos [] slice = (slice,[],[]) gos (exp:exps) slice = let (slice1,redexes1,consts1) = gos exps slice (slice2,redexes2,consts2) = go exp slice1 in (slice2,redexes2++redexes1,consts2++consts1) go :: FileNode -> Slice -> (Slice,[FileNode],[FileNode]) go exp slice = if getParentNode exp /= parent then (slice,[],[]) else case nodeType exp of ExpApp -> if isRedex exp then let (newSlice,redexes,consts) = gos (peekSubExprs exp) (addToSlice loc slice) in (newSlice,exp:redexes,consts) else (subtractFromSlice loc slice,[],[]) ExpValueApp -> gos (tail (peekSubExprs exp)) (addToSlice loc slice) -- first arg is atom for which there is no location ExpValueUse -> (addToSlice loc slice,[],[]) ExpConstUse -> if isRedex (peekExpArg exp 0) then -- check constDef (addToSlice loc slice,[],[exp]) else (subtractFromSlice loc slice,[],[]) ExpConstDef -> error "traverseReduct: ExpConstDef" ExpGuard -> let (slice1,redexes1,consts1) = traverseReduct exp (slice2,redexes2,consts2) = go (peekExpArg exp 0) slice1 in (slice2,redexes1++redexes2,consts1++consts2) -- sadly trace contains no useful location for guard -- existing location is that of boolean expression ExpCase -> let (slice1,redexes1,consts1) = traverseReduct exp slice2 = addToSlice (Location{begin=begin loc ,end=Coord{row=row (begin loc) ,col = col (begin loc)+3}}) (mergeSlices slice1 (subtractFromSlice loc slice)) (slice3,redexes2,consts2) = go (peekExpArg exp 0) slice2 in (slice3,redexes1++redexes2,consts1++consts2) -- subtract whole subexpression from slice before adding "case" -- and demanded parts ExpIf -> let (slice1,redexes1,consts1) = traverseReduct exp slice2 = addToSlice (Location{begin=begin loc ,end=Coord{row=row (begin loc) ,col = col (begin loc)+1}}) (mergeSlices slice1 (subtractFromSlice loc slice)) (slice3,redexes2,consts2) = go (peekExpArg exp 0) slice2 in (slice3,redexes1++redexes2,consts1++consts2) -- subtract whole subexpression from slice before adding "if" -- and demanded parts ExpFieldUpdate -> if isRedex exp then let (slice,redexes,consts) = gos (peekSubExprs exp) (addToSlice loc slice) in (slice,exp:redexes,consts) else (subtractFromSlice loc slice,[],[]) ExpProjection -> (addToSlice loc slice,[],[]) -- argument must have different parent ExpHidden -> (emptySlice,hiddenChildren exp,[]) -- (slice,[],[]) ExpForward -> go (peekResult exp) slice -- just walk through ExpChar -> (addToSlice loc slice,[],[]) ExpInt -> (addToSlice loc slice,[],[]) ExpInteger -> (addToSlice loc slice,[],[]) ExpRat -> (addToSlice loc slice,[],[]) ExpRational -> (addToSlice loc slice,[],[]) ExpFloat -> (addToSlice loc slice,[],[]) ExpDouble -> (addToSlice loc slice,[],[]) _ -> error "getReductSubExpNodes: unexpected node type" where (_,loc) = getUseLocation exp isRedex :: FileNode -> Bool -- assume there is a non-nil result isRedex exp = peekResult exp `notElem` [unevaluated,exp] -- partial application can have a result pointing to itself -------------------------------------------------------------------- redexAllChildren :: FileNode -> [FileNode] -- given a redex, i.e. application or constUse -- yield all children, including trusted ones -- children are applications or constUses redexAllChildren redex = appRedexes ++ constRedexes where (_,appRedexes,constRedexes) = traverseReduct redex expSort :: [FileNode] -> [FileNode] expSort = sortBy cmp where cmp red1 red2 = compare loc1 loc2 where (_,loc1) = getUseLocation red1 (_,loc2) = getUseLocation red2 redexChildren :: FileNode -> [FileNode] -- excludes trusted children (currently even those with children, TO DO) -- currently this function is not used at all redexChildren = filter suspectedRedex . redexAllChildren suspectedRedex :: FileNode -> Bool -- given application or constUse suspectedRedex redex = result `elem` [entered,interrupted] || not (isHidden result && null (hiddenChildren result)) where result = redexResult redex redexResult :: FileNode -> FileNode -- given application or constUse return the reduct (or entered, etc) -- this is usually not the final result redexResult redex = case nodeType redex of ExpApp -> peekResult redex ExpConstUse -> peekResult (peekExpArg redex 0) ExpConstDef -> peekResult redex -- the following are just for reliablity ExpGuard -> peekResult redex ExpCase -> peekResult redex ExpIf -> peekResult redex ExpFieldUpdate -> peekResult redex _ -> error ("redexResult: unexpected redex " ++ showNode redex) redexParents :: FileNode -> [FileNode] -- list of ancestors, first is the parent redexParents redex = let parent = redexParent redex in if parent == nil then [] else parent : redexParents parent expIsRedex :: FileNode -> Bool expIsRedex node = case nodeType node of ExpApp -> isRedex node ExpConstUse -> isRedex (peekExpArg node 0) ExpConstDef -> isRedex node _ -> False isHidden :: FileNode -> Bool isHidden node = case nodeType node of ExpHidden -> True _ -> False -------------------------------------------------------------------- updRedexFaultyDescendants :: State -> State -- all descendants including redex itself that may be faulty -- i.e. descendant tree without subtrees started by a correct redex updRedexFaultyDescendants state = state{faultSetRoot = root ,faultSet = if root == nil then emptySet else go root id emptySet} where -- root is first wrong redex when going up parents root = case filter (`elemSet` (wrong state)) (cur (redexes state):parents state) of (wrong:_) -> wrong [] -> nil -- continuation passing style, threading already visited nodes -- to avoid looping for mutually recursive constants go :: FileNode -> (Set FileNode -> Set FileNode) -> Set FileNode -> Set FileNode go redex cont collected = if redexCorrect redex state || redex `elemSet` collected then cont collected else (foldr ($) cont (map go (redexAllChildren redex))) (insertSet redex collected) -------------------------------------------------------------------- redexDefUsedSlice :: State -> FileNode -> Slice redexDefUsedSlice state redex = let (file,loc) = getDefLocation redex in if file /= filename (cur (modules state)) then emptySlice else used where (used,_,_) = traverseReduct redex redexDefSlice :: State -> FileNode -> Slice redexDefSlice state redex = let (file,loc) = getDefLocation redex in if file == filename (cur (modules state)) then mkSlice loc else emptySlice redexUseLocation :: FileNode -> Location -- assumes given node is redex, i.e. application or constUse -- location covers full redex, including all subexpressions redexUseLocation redex = if redex `elem` [nil,unevaluated,entered,interrupted] then error "redexUseLocation: invalid redex" else loc where (_,loc) = getUseLocation redex redexUseSlice :: FileNode -> Slice -- assumes given node is redex, i.e. application or constUse -- slice includes the application and all subconstructs -- that are values or may be values redexUseSlice redex = if redex `elem` [nil,unevaluated,entered,interrupted] then error "redexUseSlice: invalid redex" else gos (peekSubExprs redex) (mkSlice loc) where parent = getParentNode redex (_,loc) = getUseLocation redex gos :: [FileNode] -> Slice -> Slice gos exps slice = foldr go slice exps go :: FileNode -> Slice -> Slice go exp slice = if getParentNode exp /= parent then slice else case nodeType exp of ExpApp -> subtractFromSlice loc slice ExpValueApp -> gos (tail (peekSubExprs exp)) (addToSlice loc slice) ExpValueUse -> addToSlice loc slice ExpConstUse -> subtractFromSlice loc slice ExpConstDef -> slice -- only if original redex was constUse ExpGuard -> subtractFromSlice loc slice ExpCase -> subtractFromSlice loc slice ExpIf -> subtractFromSlice loc slice ExpFieldUpdate -> subtractFromSlice loc slice ExpChar -> addToSlice loc slice ExpInt -> addToSlice loc slice ExpInteger -> addToSlice loc slice ExpRat -> addToSlice loc slice ExpRational -> addToSlice loc slice ExpFloat -> addToSlice loc slice ExpDouble -> addToSlice loc slice _ -> error "redexUseSlice: unexpected node type" where (_,loc) = getUseLocation exp -------------------------------------------------------------------- borderSlice :: Text -> Slice -- construct slice of all spaces at beginning and ends of lines borderSlice text = Slice (go 1 text) where go :: Int -> Text -> [Location] go _ [] = [] go curRow (line:rest) = (if leftSpace > 0 then (Location{begin=Coord{row=curRow,col=1} ,end=Coord{row=curRow,col=leftSpace}}:) else id) ((Location{begin=Coord{row=curRow,col=lastCol-rightSpace+1} ,end=Coord{row=curRow,col=maxBound}}:) (go (curRow+1) rest)) where lastCol = length revLine leftSpace = length (takeWhile (==' ') line) rightSpace = length (takeWhile (==' ') revLine) revLine = case reverse line of '\r':rest -> rest all -> all -------------------------------------------------------------------- startInteraction :: FileNode -> IO () startInteraction startRedex = do hSetBuffering stdin NoBuffering hSetBuffering stdout NoBuffering (width,height) <- getTerminalSize putStr cls let allParents = redexParents startRedex current <- loadModule (fst (getLocation startRedex)) curModules <- insertModules allParents (mkCursorSeq [] current []) checkModules (newRedex (State { modules = curModules , window = Coord{row=height,col=width} , firstRow = 1 , parents = allParents , redexes = undefined , correct = emptySet , wrong = emptySet , neither = emptySet , faultSetRoot = nil , faultSet = emptySet , showFaultSet = False , showPart = False , message = "Press h for help." }) startRedex) fileTags :: State -> [Tag] fileTags state = let redexSlice = mkSlice (redexUseLocation (cur (redexes state))) siblings = cursorSeqToList (redexes state) (suspectedSiblings,trustedSiblings) = partition suspectedRedex siblings (correctSus,otherSus) = partition (`elemSet` (correct state)) suspectedSiblings (wrongFaultySus,neitherSus) = partition (`elemSet` (wrong state)) otherSus (neitherTrust,otherTrust) = partition (`elemSet` (neither state)) trustedSiblings (wrongFaultyTrust,correctTrust) = partition (`elemSet` (wrong state)) trustedSiblings correctSiblings = correctTrust ++ correctSus neitherSiblings = neitherTrust ++ neitherSus (faultySiblings,wrongSiblings) = partition (`redexFaulty` state) (wrongFaultyTrust ++ wrongFaultySus) correctSiblingsSlice = mergeSlicesMap redexUseSlice correctSiblings neitherSiblingsSlice = mergeSlicesMap redexUseSlice neitherSiblings wrongSiblingsSlice = mergeSlicesMap redexUseSlice wrongSiblings faultySiblingsSlice = mergeSlicesMap redexUseSlice faultySiblings makeSlice = if showPart state then redexDefUsedSlice else redexDefSlice in if filename (cur (modules state)) == fst (getUseLocation (cur (redexes state))) then combineSlices [(redexSlice,currentM) ,(correctSiblingsSlice,correctM) ,(wrongSiblingsSlice,wrongM) ,(neitherSiblingsSlice,markedM) ,(faultySiblingsSlice,faultyM) ,(border (cur (modules state)),emptyM) ,(if showFaultSet state then manySlices (makeSlice state) (faultSet state) else makeSlice state (cur (redexes state)) ,definitionM)] else case getLocation (cur (redexes state)) of (file,loc) -> combineSlices ((if file == filename (cur (modules state)) then ((mkSlice loc,currentM):) else id) [(border (cur (modules state)),emptyM) ,(if showFaultSet state then manySlices (makeSlice state) (faultSet state) else makeSlice state (cur (redexes state)) ,definitionM)]) redexMark :: FileNode -> State -> Mark redexMark red state = (if showFaultSet state && red == faultSetRoot state then (combMarks definitionM) else id) $ (if red == cur (redexes state) then (combMarks currentM) else id) $ (if red `elemSet` correct state then correctM else if red `elemSet` wrong state then if redexFaulty red state then faultyM else wrongM else if red `elemSet` neither state || suspectedRedex red then markedM else correctM) equationText :: State -> Int -> FileNode -> String equationText state no eqn = leftWidth 2 (show no) ++ ". " ++ mark2Highlights (redexMark eqn state) ++ take (col (window state)-5) (removeHighlights (prettyEquation2 initialOptions eqn)) ++ highlightOff -- need to remove highlights in equation, because otherwise -- highlights not correctly nested and line cut off too early leftWidth width = reverse . take width . (++ repeat ' ') . reverse removeHighlights :: String -> String removeHighlights xs = ys ++ if null zs then [] else (removeHighlights . tail . dropWhile (/= 'm')) zs where (ys,zs) = span (/= '\ESC') xs defaultMessage :: State -> String defaultMessage state = "Call " ++ show (curIndex (redexes state)) ++ "/" ++ show (lengthCursorSeq (redexes state)) ++ " | " ++ (if showFaultSet state then "faulty slice" else "definition") ++ " | " ++ (if showPart state then "executed part" else "complete") force :: [a] -> [a] -- force evaluation of whole list spine force = reverse . reverse cutOffText :: Int -> Text -> String -- cut off text at given width, handling embedded escape sequences correctly -- (not all, e.g. not goto) -- also does not cut off escape sequences appearing just after width -- incomplete lines are filled up with spaces cutOffText mw = init . unlines . (map (cutOffLine mw)) where cutOffLine :: Int -> String -> String cutOffLine w xs = case xs of "" -> replicate w ' ' (c:cs) -> if c == '\ESC' then let (escapeSeq,end:rest) = break isAlpha cs in c : escapeSeq++[end]++cutOffLine w rest else if w == 0 then highlightOff else c : cutOffLine (w-1) cs display :: State -> IO () display state = do let lastRow = firstRow state + row (window state) - srcRow - 1 tags = fileTags state markedText = markText (text (cur (modules state))) (firstRow state) lastRow tags eqns = reverse (cur (redexes state) : take (eqnNo-1) (parents state)) firstEqnNo = length (parents state)-length eqns+2 putStr (home ++ lineWrap False) writeFile "test.txt" (show tags) (putStr . force . cutOffText (col (window state))) $ -- force minimises flickering of screen output highlight [Bold] ("==== Hat-Explore " ++ hatVersionNumber ++ " ==== " ++ (if null (message state) then defaultMessage state else message state) ++ ' ':repeat '=') : zipWith (equationText state) [firstEqnNo..] eqns ++ replicate (eqnNo - length eqns) "" ++ highlight [Bold] ("---- "++filename (cur (modules state)) ++" ---- lines "++show (firstRow state)++" to " ++show lastRow++' ':repeat '-') : markedText putStr home data SrcModule = SrcModule { filename :: String , text :: Text , len :: Row , border :: Slice } eqnNo = 5 :: Int srcRow = eqnNo+2 :: Int srcRows state = row (window state) - srcRow data State = State { modules :: CursorSeq SrcModule -- ordered alphabetically , window :: Coord , firstRow :: Row , parents :: [FileNode] -- ancestors of redexes , redexes :: CursorSeq FileNode -- current redex + siblings ordered by location , correct :: Set FileNode -- trusted ones not listed , wrong :: Set FileNode , neither :: Set FileNode -- subset of trusted ones , faultSetRoot :: FileNode , faultSet :: Set FileNode , showFaultSet :: Bool , showPart :: Bool , message :: String } newRedex :: State -> FileNode -> State -- set given redex in state; assume parents are already set correctly -- note: a parent might be a pseudo-parent of a constant newRedex state new = case parents state of (parent:_) -> let parChildren = expSort (redexAllChildren parent) (left,rest) = break (== new) parChildren in if null rest -- redex not amongst children of parent then state{redexes = mkCursorSeq [] new []} else state{redexes = mkCursorSeq left new (tail rest)} [] -> state{redexes = mkCursorSeq [] new []} help :: IO () help = do putStr (cls ++ goto 1 1) putStr (highlight [Bold] "==== Help Text ===============================") putStr (goto 1 2) putStr helpText getChar return () where helpText = " cursor down follow current call\n cursor up go back to caller of current call\n cursor left go to call further left in current definition body\n cursor right go to call further right in current definition body\n\n c declare current equation to be correct (wrt. intentions)\n w declare current equation to be wrong (wrt. intentions)\n n undo declaration of correctness (neither correct nor wrong)\n a amnesia - forget all declarations as correct or wrong\n\n f toggle between showing fault set or just current definition\n p toggle between showing used part of definition or full\n\n < change to alphabetically preceeding module\n > change to alphabetically succeeding module\n\n t scroll source window to top of code\n u scroll source window upwards\n d scroll source window downwards\n b scroll source window to bottom of code\n\n r redraw everything after change of window size\n h or ? display this help text\n\n q quit\n\n\nMeaning of colours:\ngreen - correct, amber - wrong, blue - unkown, red - faulty.\n\n Press any key to continue. " loop :: State -> IO () loop state1 = do let state2 = updRedexFaultyDescendants state1 display state2 let state = state2{message = ""} c <- getChar case c of 'q' -> putStr cls 'u' -> let oldRow = firstRow state in loop state{firstRow = if oldRow>1 then oldRow-1 else oldRow} 'd' -> let oldRow = firstRow state in loop state{firstRow = if oldRow<=len (cur (modules state)) then oldRow+1 else oldRow} 't' -> loop state{firstRow = 1} 'b' -> loop state{firstRow = max 1 (len (cur (modules state)) -(row (window state))+2)} 'r' -> do (width,height) <- getTerminalSize loop state{window=Coord{row=height,col=width}} 'c' -> loop (declareCorrect state) 'w' -> loop (declareWrong state) 'n' -> loop (declareNeither state) 'a' -> loop state{correct=emptySet,wrong=emptySet,neither=emptySet} 'f' -> loop state{showFaultSet=not (showFaultSet state)} 'p' -> loop state{showPart = not (showPart state)} '<' -> if lengthCursorSeq (modules state) == 1 then loop state{message = "There is only one module."} else loop state{modules = rotateLeft (modules state)} '>' -> if lengthCursorSeq (modules state) == 1 then loop state{message = "There is only one module."} else loop state{modules = rotateRight (modules state)} 'o' -> do System.Cmd.system (hatObserve (dropHS (filename (cur (modules state)))) (head (words (removeHighlights -- crude approximation (prettyEquation2 initialOptions (cur (redexes state))))))) loop state{message = "Spawned hat-observe"} 'l' -> do System.Cmd.system (hatTrail (dropHS (filename (cur (modules state)))) (cur (redexes state))) loop state{message = "Spawned hat-trail"} 'e' -> do System.Cmd.system (hatDetect (dropHS (filename (cur (modules state)))) (cur (redexes state))) loop state{message = "Spawned hat-detect"} 'i' -> do System.Cmd.system (hatAnim (dropHS (filename (cur (modules state)))) (cur (redexes state))) loop state{message = "Spawned hat-anim"} 'h' -> help >> loop state '?' -> help >> loop state '\ESC' -> do c <- getChar if c `elem` "[O" then do c <- getChar case c of 'D' -> -- cursor left if lengthCursorSeq (redexes state) == 1 then loop state{message = "The call has no siblings."} else loop state{redexes = rotateLeft (redexes state)} 'C' -> -- cursor right if lengthCursorSeq (redexes state) == 1 then loop state{message = "The call has no siblings."} else loop state{redexes = rotateRight (redexes state)} 'A' -> -- cursor up if not (null (parents state)) then checkModules (newRedex state{parents = tail (parents state)} (head (parents state))) else loop state{message = "This is a top-level constant whose caller is unknown."} 'B' -> -- cursor down -- TO DO: handle constDef differently case expSort (redexAllChildren (cur (redexes state))) of (child:_) -> checkModules (newRedex state{parents = cur (redexes state) : parents state} child) [] -> loop state{message = "There are no child calls."} else loop state{message = "Unkown command. Press h for help."} _ -> loop state{message = "Unkown command. Press h for help."} loadModule :: FilePath -> IO SrcModule loadModule filename = do filecontent <- readFile filename let srcText = lines (expandTabs 0 filecontent) return (SrcModule { filename = filename , text = srcText , len = length srcText , border = borderSlice srcText}) expandTabs :: Col -> String -> String expandTabs _ "" = "" expandTabs c (x:xs) = case x of '\t' -> replicate spaces ' ' ++ expandTabs (c+spaces) xs '\n' -> '\n' : expandTabs 0 xs '\r' -> expandTabs 0 xs '\v' -> '\n' : expandTabs 0 xs _ -> x : (expandTabs $! (c+1)) xs where spaces = 8 - c `mod` 8 checkModules :: State -> IO () -- called after redex was changed -- ensure that module of redex use is loaded and becomes current Module checkModules state = do newModules <- insertModule (cur (redexes state)) (modules state) loop (checkRow state{modules = newModules}) insertModules :: [FileNode] -> CursorSeq SrcModule -> IO (CursorSeq SrcModule) insertModules [] modules = return modules insertModules (n:ns) modules = do modules2 <- insertModule n modules insertModules ns modules2 insertModule :: FileNode -> CursorSeq SrcModule -> IO (CursorSeq SrcModule) -- ensure that module of given node is loaded and becomes current one insertModule node oldModules = let curFilename = fst (getLocation node) in case selectCurrent ((== curFilename) . filename) oldModules of Just newModules -> return newModules Nothing -> do current <- loadModule curFilename return (insertNewCurrent ((< curFilename) . filename) current oldModules) checkRow :: State -> State -- insure that redex use (or def if no use) is within the displayed window checkRow state = if firstInter >= firstRow state && lastInter < firstRow state + rows then state else if modLen <= rows then state{firstRow = 1} else if lastInter - firstInter >= rows then state{firstRow = firstInter} else let start = firstInter - (rows - (lastInter-firstInter+1)) `div` 2 in if start + rows -1 > modLen then state{firstRow = modLen - rows + 1} else if start < 1 then state{firstRow = 1} else state{firstRow = start} where rows = srcRows state modLen = len (cur (modules state)) (firstInter,lastInter) = rowsOfInterest state rowsOfInterest :: State -> (Row,Row) rowsOfInterest state = if hasUseLocation (cur (redexes state)) then (row (begin (head siblingLocations)) ,row (end (last siblingLocations))) else (row (begin curLoc),row (end curLoc)) where (_,curLoc) = getLocation (cur (redexes state)) Slice siblingLocations = foldr mergeSlices emptySlice (map redexUseSlice (cursorSeqToList (redexes state))) declareCorrect :: State -> State declareCorrect state@State{correct=cor,wrong=wr,neither=nei} = let red = cur (redexes state) in state{correct = if suspectedRedex red then insertSet red cor else cor ,wrong = removeSet red wr ,neither = removeSet red nei} declareWrong :: State -> State declareWrong state@State{correct=cor,wrong=wr,neither=nei} = let red = cur (redexes state) in state{correct = removeSet red cor ,wrong = insertSet red wr ,neither = removeSet red nei} declareNeither :: State -> State declareNeither state@State{correct=cor,wrong=wr,neither=nei} = let red = cur (redexes state) in state{correct = removeSet red cor ,wrong = removeSet red wr ,neither = if suspectedRedex red then nei else insertSet red nei} redexFaulty :: FileNode -> State -> Bool -- cannot otherwise keep track of faulty redexes, because don't know -- pseudoparents of a constant. redexFaulty red state = red `elemSet` (wrong state) && all (flip redexCorrect state) (redexAllChildren red) redexCorrect :: FileNode -> State -> Bool redexCorrect red state = red `elemSet` correct state || not (suspectedRedex red || red `elemSet` neither state || red `elemSet` wrong state) ----------------------------- type Text = [String] -- list of tab and newline-free lines; 1 char = 1 col type MarkedText = [String] -- may include escape sequences for highlighting mark2Highlights :: Mark -> String mark2Highlights Empty = highlightOn [Normal] -- default marking mark2Highlights (Mark hi1 hi2 ) = highlightOn (Normal : hi1 ++ hi2) -- the foreground colour is never changed -- this may be problematic if default foreground does not contrast with -- the various background colours chosen here -- however, some terminals (e.g. kde) interpret bold + foreground colour -- as a lighter foreground colour; so to obtain bold plus background colour -- also on these terminals, the foreground is never changed. markText :: Text -> Row -> Row -> [Tag] -> MarkedText -- markup input text from first row up to second row -- result only contains the specified rows -- filled up with empty rows if necessary -- assumes at least first row and rows mentioned in tags exist in text markText text beginRow endRow tags = markTextTo startText startTags endRow where startText = drop (beginRow-1) text startTags = getTagsFromRow tags beginRow markTextTo :: Text -> [Tag] -> Row -> MarkedText -- assumes that coords of first tag are coords of first text char markTextTo text (t:ts) lastRow = (mark2Highlights (mark t)++line):lines where (line:lines) = go text (start t) ts go :: Text -> Coord -> [Tag] -> MarkedText go (line:lines) current (t:ts) = if row (start t) > lastRow then copyLastLines (line:lines) (row current) else if row (start t) == row current then let (firstLine,restLine) = splitAt (col (start t) - col current) line (mRestLine:mRest) = go (restLine:lines) (start t) ts in (firstLine ++ mark2Highlights (mark t) ++ mRestLine) : mRest else -- row (start t) > row current line : go lines Coord{row = row current+1,col = 1} (t:ts) go lines current _ = -- either no lines or no tags copyLastLines lines (row current) copyLastLines :: Text -> Row -> MarkedText copyLastLines (line:lines) currentRow = if currentRow < lastRow then line : copyLastLines lines (currentRow+1) else -- currentRow == lastRow [line ++ highlightOff] copyLastLines [] currentRow = replicate (lastRow-currentRow-1) [] ++ [highlightOff] splitText :: Text -> Coord -> Coord -> (Text,Text) -- all texts start and end with incomplete rows splitText (line:lines) first second = if row first == row second then let (firstLine,restLine) = splitAt (col second - col first) line in ([firstLine],restLine:lines) else -- row first < row second let (firstText,secondText) = splitText lines Coord{row = row first+1,col = 1} second in (line:firstText,secondText) getTagsFromRow :: [Tag] -> Row -> [Tag] -- first tag starts at beginning of the row getTagsFromRow tags first = go tags noneM where go [] m = [Tag{start=Coord{row=first,col=1},mark=m}] go (t:ts) m = case compare (row (start t)) first of LT -> go ts (mark t) EQ -> if col (start t) == 1 then t:ts else Tag{start=Coord{row=first,col=1},mark=m}:t:ts GT -> Tag{start=Coord{row=first,col=1},mark=m}:t:ts data Mark = Empty | Mark [Highlight] [Highlight] deriving Show -- TESTING -- second (possibly) contains background colour -- first contains all other highlighting -- they are separate to simplify combination (does it??) emptyM = Empty currentM = Mark [Underscore,Bold] [] markedM = Mark [] [Background Cyan] correctM = Mark [] [Background Green] wrongM = Mark [] [Background Yellow] faultyM = Mark [] [Background Red] definitionM = Mark [Bold] [] noneM = Mark [] [] combMarks :: Mark -> Mark -> Mark combMarks Empty _ = Empty combMarks _ Empty = Empty combMarks (Mark hi11 hi12) (Mark hi21 hi22) = Mark (hi11 `union` hi21) (hi12 `union` hi22) data Tag = Tag {start :: Coord, mark :: Mark} deriving Show -- TESTING combineSlices :: [(Slice,Mark)] -> [Tag] combineSlices = foldr1 combTags . map (uncurry slice2Tags) slice2Tags :: Slice -> Mark -> [Tag] slice2Tags slice m = enter (unSlice slice) where enter :: [Location] -> [Tag] enter [] = [] enter (l:ls) = if end l < begin l then enter ls else Tag{start = begin l, mark = m} : exit (l:ls) exit :: [Location] -> [Tag] exit (l:ls) = Tag{start= afterCoord (end l), mark = noneM} : enter ls combTags :: [Tag] -> [Tag] -> [Tag] combTags t1s t2s = go noneM t1s noneM t2s where go :: Mark -> [Tag] -> Mark -> [Tag] -> [Tag] -- keep track of current mark for each tag sequence go m1 [] _ ts = map (\t -> t{mark = combMarks m1 (mark t)}) ts go _ ts m2 [] = map (\t -> t{mark = combMarks m2 (mark t)}) ts go m1 (t1:t1s) m2 (t2:t2s) = case compare (start t1) (start t2) of LT -> Tag{start = start t1, mark = combMarks (mark t1) m2} : go (mark t1) t1s m2 (t2:t2s) GT -> Tag{start = start t2, mark = combMarks (mark t2) m1} : go m1 (t1:t1s) (mark t2) t2s EQ -> Tag{start = start t1, mark = combMarks (mark t1) (mark t2)} : go (mark t1) t1s (mark t2) t2s ------------------------------------------------------- newtype Slice = Slice {unSlice :: [Location]} -- proper locations, non-overlapping and ordered compressSlice :: Slice -> Slice compressSlice (Slice []) = Slice [] compressSlice (Slice [l]) = Slice [l] compressSlice (Slice (l1:l2:ls)) = if isNextCoord (end l1) (begin l2) then compressSlice (Slice (Location{begin = begin l1, end = end l2}:ls)) else Slice (l1 : unSlice (compressSlice (Slice (l2:ls)))) mergeSlices :: Slice -> Slice -> Slice -- additive combination of two slices mergeSlices rs (Slice []) = rs mergeSlices (Slice []) rs = rs mergeSlices (Slice (l1:l1s)) (Slice (l2:l2s)) = if end l1 < begin l2 then -- location 1 before location 2 Slice (l1 : (unSlice (mergeSlices (Slice l1s) (Slice (l2:l2s))))) else if end l2 < begin l1 then -- location 2 before location 1 Slice (l2 : (unSlice (mergeSlices (Slice (l1:l1s)) (Slice l2s)))) else if end l1 < end l2 then mergeSlices (Slice l1s) (Slice (Location{begin = min (begin l1) (begin l2),end = end l2} : l2s)) else -- end l2 <= end l1 mergeSlices (Slice (Location{begin = min (begin l1) (begin l2),end = end l1} : l1s)) (Slice l2s) addToSlice :: Location -> Slice -> Slice -- maybe a more efficient implementation will be done later addToSlice loc = mergeSlices (Slice [loc]) subtractFromSlice :: Location -> Slice -> Slice -- given location must be improper or -- nested in one of the locations of the slice -- or be outside any locations of the slice; no overlap subtractFromSlice l (Slice []) = emptySlice subtractFromSlice l1 (Slice (l2:ls)) = if isImproperLocation l1 then Slice (l2:ls) else if begin l1 > end l2 then -- l1 not nested in l2 Slice (l2 : unSlice (subtractFromSlice l1 (Slice ls))) else -- from assumption of nesting follows that l1 nested in l2 if begin l1 == begin l2 then if end l1 == end l2 then Slice ls else Slice (Location{begin=afterCoord (end l1),end=end l2} : ls) else if end l1 == end l2 then Slice (Location{begin=begin l2,end=beforeCoord (begin l1)} : ls) else Slice (Location{begin=begin l2,end=beforeCoord (begin l1)} : Location{begin=afterCoord (end l1),end=end l2} : ls) mergeSlicesMap :: (a -> Slice) -> [a] -> Slice mergeSlicesMap f ns = foldr mergeSlices emptySlice (map f ns) manySlices :: (FileNode -> Slice) -> Set FileNode -> Slice manySlices f set = foldr mergeSlices emptySlice (map f (deSet set)) emptySlice :: Slice emptySlice = Slice [] mkSlice :: Location -> Slice mkSlice l = if isVirtLocation l || isNoLocation l then Slice [] else Slice [l] ------------------------------------------------------------------- -- abstract data type ordered sequence of elements with one current element data CursorSeq a = CursorSeq {cur :: a, left :: [a], right :: [a]} -- describes sequence with elements ordered as follows: -- reverse left ++ cur : right -- with one element marked as current element lengthCursorSeq :: CursorSeq a -> Int lengthCursorSeq cs = 1 + length (left cs) + length (right cs) cursorSeqToList :: CursorSeq a -> [a] cursorSeqToList cs = reverse (left cs) ++ cur cs : right cs mkCursorSeq :: [a] -> a -> [a] -> CursorSeq a mkCursorSeq l c r = CursorSeq{cur = c, left = reverse l, right = r} insertNewCurrent :: (a -> Bool) -> a -> CursorSeq a -> CursorSeq a -- predicate is true for all smaller elements insertNewCurrent p c cs = let elements = reverse (left cs) ++ cur cs : right cs (l,r) = span p elements in mkCursorSeq l c r curIndex :: CursorSeq a -> Int curIndex cs = length (left cs) + 1 selectCurrent :: (a -> Bool) -> CursorSeq a -> Maybe (CursorSeq a) -- may not find element fulfilling predicate selectCurrent p cs = let elements = reverse (left cs) ++ cur cs : right cs (l,r) = break p elements in case r of [] -> Nothing (c:r') -> Just (mkCursorSeq l c r') rotateLeft :: CursorSeq a -> CursorSeq a -- jumps at end rotateLeft cs = let l = left cs in if null l then if null (right cs) then cs else let r = reverse (cur cs:right cs) in CursorSeq{cur = head r, left = tail r, right = []} else CursorSeq{cur = head l, left = tail l, right = cur cs:right cs} rotateRight :: CursorSeq a -> CursorSeq a -- jumps at end rotateRight cs = let r = right cs in if null r then if null (left cs) then cs else let l = reverse (cur cs:left cs) in CursorSeq{cur = head l, left = [], right = tail l} else CursorSeq{cur = head r, left = cur cs:left cs, right = tail r} ------------------------------------------------------------------- -- abstract data type set newtype Set a = Set {deSet :: [a]} emptySet :: Set a emptySet = Set [] insertSet :: Eq a => a -> Set a -> Set a insertSet x set = if x `elemSet` set then set else Set (x: deSet set) elemSet :: Eq a => a -> Set a -> Bool elemSet x set = x `elem` deSet set removeSet :: Eq a => a -> Set a -> Set a removeSet x set = Set [y | y <- deSet set, y /= x] subSet :: Eq a => Set a -> Set a -> Bool subSet s1 s2 = all (`elemSet` s2) (deSet s1) unionSet :: Eq a => Set a -> Set a -> Set a unionSet s1 s2 = foldr insertSet s2 (deSet s1) -------------------------------------------------------------------