activehs 0.3.0.1 → 0.3.1
raw patch · 16 files changed
+256/−523 lines, 16 filesdep −Agdadep ~pandocdep ~simple-reflect
Dependencies removed: Agda
Dependency ranges changed: pandoc, simple-reflect
Files
- AgdaHighlight.hs +0/−120
- Args.hs +3/−3
- Cache.hs +4/−4
- CheckAgdaCode.hs +0/−175
- Converter.hs +20/−28
- Hash.hs +14/−0
- Logger.hs +47/−0
- Main.hs +20/−32
- Parse.hs +7/−49
- QuickCheck.hs +57/−34
- Result.hs +9/−7
- Simple.hs +16/−10
- Smart.hs +23/−44
- Snap.hs +25/−0
- Special.hs +5/−11
- activehs.cabal +6/−6
− AgdaHighlight.hs
@@ -1,120 +0,0 @@-{-# LANGUAGE GeneralizedNewtypeDeriving #-} - -module AgdaHighlight - ( highlightAgdaAsXHtml --- , FormatOption (..) - ) where - -import Text.Highlighting.Kate as Kate -import Text.Blaze.Renderer.String - -import Control.Monad.State -import System.IO.Unsafe - -import Agda.Syntax.Literal -import Agda.Syntax.Position -import Agda.Syntax.Parser -import Agda.Syntax.Parser.Tokens (Token(..)) - -highlightAgdaAsXHtml :: String -> String -highlightAgdaAsXHtml code = formattedCode - where - language = "agda" - (Right highlightInfo) = highlight code - formattedCode = renderHtml $ formatHtmlBlock defaultFormatOpts highlightInfo - --- | Highlight source code using this syntax definition. -highlight :: String -> Either String [SourceLine] -highlight input = Right $ runSourceLineGen $ do - tokens <- liftIO $ parse tokensParser input - -- tokens :: IO [Tokens] - -- Other parsing method needed - or unsafePerformIO - -- map tokenToSourceLine tokens - mapM_ processToken tokens - where --- processToken :: Token -> SourceLineGen () - processToken token = - case token of - TokKeyword kw iv -> addByInterval (KeywordTok, getSourceByInterval iv) iv -- kw - TokId (iv, id) -> addByInterval (DataTypeTok, getSourceByInterval iv) iv -- dt - TokQId ivds -> mapM_ (\(iv, id) -> addByInterval (DataTypeTok, getSourceByInterval iv) iv) ivds -- dt - TokLiteral lit -> - case lit of - LitInt r i -> addByRange (DecValTok, getSourceByRange r) r -- dv - LitFloat r d -> addByRange (FloatTok, getSourceByRange r) r -- fl - LitString r str -> addByRange (StringTok, getSourceByRange r) r -- st - LitChar r ch -> addByRange (CharTok, getSourceByRange r) r -- ch - LitQName r qn -> addByRange (OtherTok, getSourceByRange r) r -- ? - TokSymbol sym iv -> addByInterval (FunctionTok, getSourceByInterval iv) iv -- TODO: switch by symbol? - TokString (iv, str) -> addByInterval (StringTok, getSourceByInterval iv) iv -- st - TokSetN (iv, n) -> addByInterval (OtherTok, "TokSetN") iv -- ? - TokTeX (iv, str) -> addByInterval (OtherTok, "TokTex") iv -- ? - TokComment (iv, str) -> addByInterval (CommentTok, getSourceByInterval iv) iv -- co - TokDummy -> return () - TokEOF -> return () - - getSourceByInterval :: Interval -> String - getSourceByInterval iv = take len $ drop (st - 1) input - where - st = (fromIntegral . posPos . iStart) iv - end = (fromIntegral . posPos . iEnd) iv - len = end - st - - getSourceByRange :: Range -> String - getSourceByRange (Range ivs) = foldl (++) [] $ map getSourceByInterval ivs - -type LabeledSource = Kate.Token -- ([String], String) - -data SourceLineState = SLS - { slsLines :: [SourceLine] - , slsCurrentLine :: !Int - , slsCurrentChar :: !Int - } deriving (Show) - -newtype SourceLineGen a = SLG (StateT SourceLineState IO a) - deriving (Monad, MonadState SourceLineState, MonadIO) - -newLine :: SourceLineGen () -newLine = modify (\s -> s - { slsLines = (slsLines s) ++ [[]] - , slsCurrentLine = (slsCurrentLine s) + 1 - , slsCurrentChar = 1 - }) - -extendCurrentLine :: LabeledSource -> SourceLineGen () -extendCurrentLine ls@(attrs, source) = modify (\s -> s { slsLines = modLines s, slsCurrentChar = modChars s }) - where - modChars s = (slsCurrentChar s) + (length source) - modLines s = (start s) ++ [ modLine s ] ++ (end s) - modLine s = ((slsLines s) !! ((slsCurrentLine s) - 1)) ++ [ ls ] - start s = fst $ parts s - end s = drop 1 $ snd $ parts s - parts s = splitAt ((slsCurrentLine s) - 1) (slsLines s) - -addAt :: LabeledSource -> Int -> Int -> SourceLineGen () -addAt ls line char = do - currentLine <- gets slsCurrentLine - let lineDiff = line - currentLine - 1 - mapM_ (\x -> newLine) [0..lineDiff] - currentChar <- gets slsCurrentChar - let charDiff = char - currentChar - if charDiff > 0 then extendCurrentLine $ spaceLS charDiff else return () - extendCurrentLine ls - where - spaceLS n = (OtherTok, replicate n ' ') - -addAtPosition :: LabeledSource -> Position -> SourceLineGen () -addAtPosition ls p = addAt ls (fromIntegral $ posLine p) (fromIntegral $ posCol p) - -addByInterval :: LabeledSource -> Interval -> SourceLineGen () -addByInterval ls i = addAtPosition ls (iStart i) - -addByRange :: LabeledSource -> Range -> SourceLineGen () -addByRange ls (Range is) = mapM_ (addByInterval ls) is - -runSourceLineGen :: SourceLineGen a -> [SourceLine] -runSourceLineGen (SLG body) = slsLines $ unsafePerformIO $ execStateT body (SLS - { slsLines = [[]] - , slsCurrentLine = 1 - , slsCurrentChar = 1 - })
Args.hs view
@@ -29,7 +29,7 @@ , port :: Int , lang :: String , static :: Bool- , verbose :: Bool+ , verbose :: Int , verboseinterpreter :: Bool , recompilecmd :: String , magicname :: String@@ -39,7 +39,7 @@ myargs :: Args myargs = Args { sourcedir = "." &= typDir &= help "Directory of lhs files to serve. Default is '.'"- , includedir = [] &= typDir &= help "Additional include directory (eg. path of Agda Standard Library). You can specify more than one. Empty by default."+ , includedir = [] &= typDir &= help "Additional include directory. You can specify more than one. Empty by default." , gendir = "html" &= typDir &= help "Directory to put generated content to serve. Default is 'html'" , exercisedir = "exercise" &= typDir &= help "Directory to put generated exercises to serve. Default is 'exercise'" , templatedir = "" &= typDir &= help "Directory of html template files for pandoc. Default points to the distribution's directory."@@ -54,7 +54,7 @@ , lang = "en" &= typ "LANGUAGE" &= help "Default language. It is 'en' by default." , port = 8000 &= typ "PORT" &= help "Port to listen" , static = False &= help "Do not regenerate pages."- , verbose = False &= help "Verbose activehs output"+ , verbose = 2 &= help "Verbose activehs output" , verboseinterpreter = False &= help "Verbose interpreter output in the browser" , recompilecmd = "ghc -O" &= typ "COMMAND" &= help "Command to run before page generation. Default is 'ghc -O'." , magicname = "a9xYf" &= typ "VARNAME" &= help "Magic variable name."
Cache.hs view
@@ -6,7 +6,7 @@ , clearCache ) where -import Data.Digest.Pure.MD5 (MD5Digest)+import Hash import Control.Concurrent.MVar (MVar, newEmptyMVar, readMVar, putMVar) import Data.Array.IO (IOArray, newArray, readArray, writeArray, getBounds)@@ -22,7 +22,7 @@ data CacheEntry a = CacheEntry - { question :: MD5Digest+ { question :: Hash , answer :: MVar a } @@ -39,7 +39,7 @@ mapM_ (\i -> writeArray (array c) i []) [a..b] -lookupCache :: Cache a -> MD5Digest -> IO (Either a (a -> IO ()))+lookupCache :: Cache a -> Hash -> IO (Either a (a -> IO ())) lookupCache ch e = modifyCacheLine (array ch) (getIndex e) $ \vv -> case lookupIA (cacheLineSize ch) (\x -> e == question x) vv of (Just x_, c) -> do@@ -63,7 +63,7 @@ writeArray ch i x' return r - getIndex :: MD5Digest -> Int+ getIndex :: Hash -> Int getIndex e = 16 * digitToInt a + digitToInt b where (a:b:_) = show e
− CheckAgdaCode.hs
@@ -1,175 +0,0 @@-module CheckAgdaCode- ( typeCheckAgdaCode- ) where----import Smart---import ActiveHs.Base (WrapData2 (WrapData2), TestCase (TestCase))-import Lang-import qualified Result as AHR---import Qualify (qualify)--import Data.Digest.Pure.MD5---import Language.Haskell.Interpreter hiding (eval)--import Agda.Interaction.GhciTop----import Data.Char (isLower)---import Data.List (intercalate)---import Control.Concurrent.MVar---import System.Directory---import qualified System.IO as IO---import System.IO.Unsafe---import Data.Char---import Data.Maybe---import Data.IORef---import Data.Function-import Control.Applicative---import qualified Control.Exception as E----import Agda.Utils.Fresh---import Agda.Utils.Monad---import Agda.Utils.Pretty as P---import Agda.Utils.String-import Agda.Utils.FileName---import qualified Agda.Utils.Trie as Trie---import Agda.Utils.Tuple---import qualified Agda.Utils.IO.UTF8 as UTF8--import Control.Monad.Error---import Control.Monad.Reader-import Control.Monad.State hiding (State)---import Control.Exception---import Data.List as List---import qualified Data.Map as Map---import System.Exit---import qualified System.Mem as System---import System.Time---import Text.PrettyPrint--import Agda.TypeChecker-import Agda.TypeChecking.Monad as TM- hiding (initState, setCommandLineOptions)-import qualified Agda.TypeChecking.Monad as TM-import Agda.TypeChecking.MetaVars-import Agda.TypeChecking.Reduce-import Agda.TypeChecking.Errors--import Agda.Syntax.Fixity-import Agda.Syntax.Position-import Agda.Syntax.Parser-import qualified Agda.Syntax.Parser.Tokens as T-import Agda.Syntax.Concrete as SC-import Agda.Syntax.Common as SCo-import Agda.Syntax.Concrete.Name as CN-import Agda.Syntax.Concrete.Pretty ()-import Agda.Syntax.Abstract as SA-import Agda.Syntax.Abstract.Pretty-import Agda.Syntax.Internal as SI-import Agda.Syntax.Scope.Base-import Agda.Syntax.Scope.Monad hiding (bindName, withCurrentModule)-import qualified Agda.Syntax.Info as Info-import Agda.Syntax.Translation.ConcreteToAbstract-import Agda.Syntax.Translation.AbstractToConcrete hiding (withScope)-import Agda.Syntax.Translation.InternalToAbstract-import Agda.Syntax.Abstract.Name--import Agda.Interaction.EmacsCommand-import Agda.Interaction.Exceptions-import Agda.Interaction.FindFile-import Agda.Interaction.Options-import Agda.Interaction.MakeCase-import qualified Agda.Interaction.BasicOps as B-import Agda.Interaction.Highlighting.Emacs-import Agda.Interaction.Highlighting.Generate-import Agda.Interaction.Highlighting.Precise (HighlightingInfo)-import qualified Agda.Interaction.Imports as Imp--import Agda.Termination.TermCheck--import qualified Agda.Compiler.Epic.Compiler as Epic-import qualified Agda.Compiler.MAlonzo.Compiler as MAlonzo-import qualified Agda.Compiler.JS.Compiler as JS--import qualified Agda.Auto.Auto as Auto--import Agda.Utils.Impossible------typeCheckAgdaCode- :: [FilePath] -> MD5Digest -> Language -> {-TaskChan -> -}FilePath -> String - -> IO [AHR.Result]-typeCheckAgdaCode sourcedirs m5 lang {-ch-} fn ft- = do- s <- ioTCM' fn False (cmd_load fn $ "." : sourcedirs)- return $ case s of- Nothing -> [AHR.Message "Right!" Nothing]- Just err -> [AHR.Error True err]--ioTCM' :: FilePath- -- ^ The current file. If this file does not match- -- 'theCurrentFile', and the 'Interaction' is not- -- \"independent\", then an error is raised.- -> Bool- -- ^ Should syntax highlighting information be produced? In- -- that case this function will generate an Emacs command- -- which interprets this information.- -> Interaction- -> IO (Maybe String)-ioTCM' current highlighting cmd = undefined -{-- infoOnException $ do---- current <- absolute current-- -- Read the state.- let (InteractionState { theTCState = st }) = initState-- -- Run the computation.- r <- runTCM $ catchError (do- put st- x <- withEnv (initEnv- { envEmacs = True- , envInteractiveHighlighting = highlighting- }) $ do- case independence cmd of- Dependent -> ensureFileLoaded current- Independent Nothing ->- -- Make sure that the include directories have- -- been set.- setCommandLineOptions' =<< commandLineOptions- Independent (Just is) -> do- ex <- liftIO $ doesFileExist $ filePath current- setIncludeDirs is $- if ex then ProjectRoot current else CurrentDir- command $ {-makeSilent-} cmd- st <- get- return (Right (x, st))- ) (\e -> do- pers <- stPersistent <$> get- s <- prettyError e- return (Left (pers, s, e))- )-- -- If an error was encountered, display an error message and exit- -- with an error code; otherwise, inform Emacs about the buffer's- -- goals (if current matches the new current file).- let errStatus = Status { sChecked = False- , sShowImplicitArguments =- optShowImplicit $ stPragmaOptions st- }- case r of- Right (Left (_, s, e)) -> displayErrorAndExit errStatus (getRange e) s- Left e -> displayErrorAndExit errStatus (getRange e) $- tcErrString e- Right (Right _) -> return Nothing- where- displayErrorAndExit es range err = return $ Just err--}---
Converter.hs view
@@ -6,18 +6,16 @@ import Parse -import Smart (TaskChan, restart, mkId, interp)+import Smart (TaskChan, restart, interp) import Result (hasError) import Html import Lang import Args+import Hash import qualified Language.Haskell.Exts.Pretty as HPty import qualified Language.Haskell.Exts.Syntax as HSyn -import qualified Agda.Syntax.Concrete as ASyn-import qualified Agda.Utils.Pretty as AUtil- import Text.XHtml.Strict hiding (lang) import Text.Pandoc @@ -26,10 +24,11 @@ import System.FilePath import System.Exit import System.Directory (getTemporaryDirectory, getModificationTime, doesFileExist, getTemporaryDirectory, createDirectoryIfMissing)-import System.Time (diffClockTimes, noTimeDiff) +--import Data.Time (diffUTCTime) import Control.Monad import Data.List+import Data.Char ---------------------------------- @@ -37,7 +36,7 @@ convert ghci args@(Args {magicname, sourcedir, gendir, recompilecmd, verbose}) what = do whenOutOfDate () output input $ do whenOutOfDate () object input $ do- when verbose $ putStrLn $ object ++ " is out of date, regenerating"+ when (verbose > 0) $ putStrLn $ object ++ " is out of date, regenerating" -- x <- system $ recompilecmd ++ " " ++ input let (ghc:args) = words recompilecmd -- !!! (x, out, err) <- readProcessWithExitCode ghc (args ++ [input]) ""@@ -46,16 +45,10 @@ restart ghci return () else fail $ unlines [unwords [recompilecmd, input], show x, out, err]- when verbose $ putStrLn $ output ++ " is out of date, regenerating"- mainParse HaskellMode input >>= extract HaskellMode verbose ghci args what- whenOutOfDate () output input2 $ do- -- watch object code (*.lagdai?) like in haskell mode?- when verbose $ putStrLn $ output ++ " is out of date, regenerating"- mainParse AgdaMode input2 >>= extract AgdaMode verbose ghci args what--- return True+ when (verbose > 0) $ putStrLn $ output ++ " is out of date, regenerating"+ mainParse HaskellMode input >>= extract HaskellMode (verbose > 0) ghci args what where input = sourcedir </> what <.> "lhs"- input2 = sourcedir </> what <.> "lagda" output = gendir </> what <.> "xml" object = sourcedir </> what <.> "o" @@ -68,7 +61,7 @@ ht <- readFile' $ templatedir </> lang' ++ ".template" writeFile' (gendir </> what <.> "xml") $ flip writeHtmlString (Pandoc meta $ concat ss')- $ defaultWriterOptions+ $ def { writerStandalone = True , writerTableOfContents = True , writerSectionDivs = True@@ -78,7 +71,6 @@ where ext = case mode of HaskellMode -> "hs"- AgdaMode -> "agda" lang' = case span (/= '_') . reverse $ what of (l, "") -> lang@@ -106,8 +98,7 @@ HPty.prettyPrint $ HSyn.Module loc (HSyn.ModuleName "Main") directives Nothing Nothing ([mkImport modname funnames, mkImport_ ('X':magicname) modname] ++ imps) []- AgdaModule (directives, ASyn.Module loc modname _ _ : _) -> "open import " ++ show modname ++ " hiding ( " ++ intercalate "; " funnames ++ " )" - _ -> error "error in Converter.extract"+-- _ -> error "error in Converter.extract" mkCodeBlock l = [ CodeBlock ("", ["haskell"], []) $ intercalate "\n" l | not $ null l ]@@ -121,7 +112,7 @@ = return $ mkCodeBlock $ visihidden processBlock _ (Exercise _ visi hidden funnames is) = do- let i = show $ mkId $ unlines funnames+ let i = show $ mkHash $ unlines funnames j = "_j" ++ i fn = what ++ "_" ++ i <.> ext (static_, inForm, rows) = if null hidden@@ -138,7 +129,7 @@ processBlock ii (OneLineExercise 'H' erroneous exp) = return [] processBlock ii (OneLineExercise p erroneous exp) = do- let m5 = mkId $ show ii ++ exp+ let m5 = mkHash $ show ii ++ exp i = show m5 fn = what ++ (if p == 'R' then "_" ++ i else "") <.> ext act = getOne "eval" fn i i@@ -160,7 +151,7 @@ processBlock _ (Text (CodeBlock ("",[t],[]) l)) | t `elem` ["dot","neato","twopi","circo","fdp","dfdp","latex"] = do tmpdir <- getTemporaryDirectory- let i = show $ mkId $ t ++ l+ let i = show $ mkHash $ t ++ l fn = what ++ i imgname = takeFileName fn <.> "png" outfile = gendir </> fn <.> "png"@@ -209,7 +200,7 @@ isLim (Text HorizontalRule) = True isLim _ = False - isHeader (Text (Header _ _)) = True+ isHeader (Text (Header {})) = True isHeader _ = False ------------------------------------@@ -243,10 +234,6 @@ = "{-# LINE 1 \"testenv\" #-}\n" ++ prelude ++ "\n{-# LINE 1 \"input\" #-}\n"-showEnv AgdaMode prelude- = "{- LINE 1 \"testenv\" -}\n"- ++ prelude- ++ "\n{- LINE 1 \"input\" -}\n" mkImport :: String -> [Name] -> HSyn.ImportDecl mkImport m d @@ -257,9 +244,14 @@ , HSyn.importSrc = False , HSyn.importPkg = Nothing , HSyn.importAs = Nothing- , HSyn.importSpecs = Just (True, map (HSyn.IVar . HSyn.Ident) d)+ , HSyn.importSpecs = Just (True, map (HSyn.IVar . mkName) d) } +mkName :: String -> HSyn.Name+mkName n@(c:_)+ | isSymbol c = HSyn.Symbol n+mkName n = HSyn.Ident n+ mkImport_ :: String -> String -> HSyn.ImportDecl mkImport_ magic m = (mkImport m []) { HSyn.importQualified = True, HSyn.importAs = Just $ HSyn.ModuleName magic }@@ -272,7 +264,7 @@ b <- modTime src case (a, b) of (Nothing, Just _) -> m- (Just t1, Just t2) | diffClockTimes t2 t1 > noTimeDiff -> m+ (Just t1, Just t2) | t1 < t2 -> m _ -> return def where modTime f = do
+ Hash.hs view
@@ -0,0 +1,14 @@+module Hash+ ( Hash+ , mkHash+ ) where++import Data.Digest.Pure.MD5 hiding (Hash)+import Data.ByteString.Lazy.UTF8 (fromString)++type Hash = MD5Digest++mkHash :: String -> Hash+mkHash = md5 . fromString++
+ Logger.hs view
@@ -0,0 +1,47 @@+{-# LANGUAGE ViewPatterns, PatternGuards, OverloadedStrings #-}+module Logger+ ( Logger+ , newLogger+ , logMsg+ , logStrMsg+ ) where++import qualified System.FastLogger as SF++import Control.Applicative+import Control.Monad++import qualified Data.ByteString as B+import qualified Data.ByteString.UTF8 as B++-------+++data Logger = Logger+ { logger :: SF.Logger+ , level :: Int+ -- 0: very important message, usually an error report, wrapped in '#####'+ -- 1: important message, wrapped in '####'+ -- 2: normal message+ -- 3, 4, ...: debug messages (not shown by default)+ }++newLogger :: Int -> FilePath -> IO Logger+newLogger l path+ = Logger <$> SF.newLogger path <*> pure l++logStrMsg :: Int -> Logger -> String -> IO ()+logStrMsg l lg+ = logMsg l lg . B.fromString++logMsg :: Int -> Logger -> B.ByteString -> IO ()+logMsg l lg msg = do+ msg' <- SF.timestampedLogEntry $ highlight l msg+ when (l <= level lg) $ SF.logMsg (logger lg) msg'+ where+ highlight 0 = wrap "#####"+ highlight 1 = wrap "####"+ highlight _ = id++ wrap n x = B.concat [n, " ", x, " ", n]+
Main.hs view
@@ -9,34 +9,29 @@ import Args import Special import Lang+import Logger import Result import Html+import Hash+import Snap import Snap.Core import Snap.Http.Server (httpServe) import Snap.Http.Server.Config import Snap.Util.FileServe (getSafePath, serveDirectoryWith, simpleDirectoryConfig) -import Data.Digest.Pure.MD5 (md5)-import System.FastLogger- import qualified Data.Text as T import qualified Data.Text.IO as T-import Data.Text.Encoding (decodeUtf8With)-import Data.Text.Encoding.Error (lenientDecode)-import Data.ByteString (ByteString)-import Data.ByteString.UTF8 (fromString)-import qualified Data.ByteString.Lazy.UTF8 as Lazy import System.FilePath ((</>), takeExtension, dropExtension) import System.Directory (doesFileExist)-import Language.Haskell.Interpreter (liftIO) import Control.Concurrent (threadDelay) import Control.Monad (when) import Control.Applicative ((<|>))-import Data.Time (getCurrentTime, diffUTCTime)+import System.Locale (defaultTimeLocale)+import Data.Time (getCurrentTime, formatTime, diffUTCTime) import Data.Maybe (listToMaybe)-import Prelude hiding (catch)+--import Prelude hiding (catch) --------------------------------------------------------------- @@ -44,9 +39,14 @@ main = getArgs >>= mainWithArgs mainWithArgs :: Args -> IO ()-mainWithArgs args@(Args {port, static, logdir, hoogledb, fileservedir, gendir, mainpage, restartpath, sourcedir, includedir}) = do +mainWithArgs args@(Args {verbose, port, static, logdir, hoogledb, fileservedir, gendir, mainpage, restartpath, sourcedir, includedir}) = do - ch <- startGHCiServer [sourcedir] (logdir </> "interpreter") hoogledb+ ti <- getCurrentTime+ log <- newLogger verbose $ + logdir </> "interpreter_" ++ formatTime defaultTimeLocale "%Y-%m-%d-%H-%M-%S" ti ++ ".log"+ -- "%Y-%m-%d-%H:%M:%S" is not ok, colons are not supported in filenames under windows++ ch <- startGHCiServer [sourcedir] log hoogledb cache <- newCache 10 httpServe@@ -60,8 +60,8 @@ ( method GET ( serveDirectoryWith simpleDirectoryConfig fileservedir <|> serveHtml ch- <|> ifTop (redirect $ fromString mainpage)- <|> path (fromString restartpath) (liftIO $ restart ch >> clearCache cache)+ <|> ifTop (redirectString mainpage)+ <|> pathString restartpath (liftIO $ restart ch >> clearCache cache) ) <|> method POST (exerciseServer (sourcedir:includedir) (cache, ch) args) <|> notFound@@ -79,20 +79,8 @@ getResponse >>= finishWith . setResponseCode 404 ---- --------------------------------------------------------------- -logNormalMsg :: TaskChan -> String -> IO ()-logNormalMsg ch x = do- v <- timestampedLogEntry $ fromString x- logMsg (logger ch) v --getParam' :: ByteString -> Snap (Maybe T.Text)-getParam' = fmap (fmap $ decodeUtf8With lenientDecode) . getParam- type TaskChan' = (Cache (Int, T.Text), TaskChan) exerciseServer :: [FilePath] -> TaskChan' -> Args -> Snap ()@@ -102,18 +90,18 @@ writeText "<html xmlns=\"http://www.w3.org/1999/xhtml\"><body>Too long request.</body></html>" getResponse >>= finishWith . setResponseCode 400 - let md5Id = md5 $ Lazy.fromString params -- could be more efficient- liftIO $ logNormalMsg ch $ " eval " ++ show md5Id ++ " " ++ params+ let md5Id = mkHash params -- could be more efficient+ liftIO $ logStrMsg 2 (logger ch) $ " eval " ++ show md5Id ++ " " ++ params j <- liftIO $ lookupCache cache md5Id (>>= writeText) $ case j of Left (delay, res) -> liftIO $ do- logNormalMsg ch $ " ch " ++ show md5Id+ logStrMsg 2 (logger ch) $ " ch " ++ show md5Id threadDelay delay return res Right cacheAction -> do time <- liftIO $ getCurrentTime res <- fmap renderResults $ do- Just [ss, fn_, x, y, T.unpack -> lang'] <- fmap sequence $ mapM getParam' ["c","f","x","y","lang"]+ Just [ss, fn_, x, y, T.unpack -> lang'] <- fmap sequence $ mapM getTextParam ["c","f","x","y","lang"] let fn = exercisedir </> T.unpack fn_ ext = reverse $ takeWhile (/='.') $ reverse fn@@ -126,7 +114,7 @@ liftIO $ do time' <- getCurrentTime let delay = round $ 1000000 * (realToFrac $ diffUTCTime time' time :: Double) :: Int- logNormalMsg ch $ " end " ++ show md5Id ++ " " ++ show delay ++ " ms " ++ T.unpack res+ logStrMsg 2 (logger ch) $ " end " ++ show md5Id ++ " " ++ show delay ++ " ms " ++ T.unpack res cacheAction (delay, res) return res
Parse.hs view
@@ -15,29 +15,24 @@ import Text.Pandoc -import AgdaHighlight- import qualified Language.Haskell.Exts.Parser as HPar import qualified Language.Haskell.Exts.Syntax as HSyn -{- Agda support (unfinished) -}-import qualified Agda.Syntax.Parser as APar-import qualified Agda.Syntax.Concrete as ASyn- import Data.List.Split (splitOn) import Data.List (tails, partition, groupBy) import Data.Function (on) import Data.Char (isAlpha, isSpace, toUpper, isUpper) import Control.Monad (zipWithM)+import qualified Data.Set as Set --------------------------------- data structures -data ParseMode = HaskellMode | AgdaMode+data ParseMode = HaskellMode -- | AgdaMode deriving (Show, Enum, Eq) data Module = HaskellModule HSyn.Module- | AgdaModule ASyn.Module+-- | AgdaModule ASyn.Module deriving (Show) data Doc@@ -85,7 +80,6 @@ fmap (Doc meta header) $ collectTests mode $ map ({-highlight . -}interpreter . Text) blocks where parseModule :: ParseMode -> String -> IO Module- parseModule AgdaMode m = fmap AgdaModule (APar.parse APar.moduleParser m) parseModule HaskellMode m = case HPar.parseModuleWithMode HPar.defaultParseMode m of (HPar.ParseOk m) -> return $ HaskellModule m parseError -> fail $ "parseHeader: " ++ show parseError@@ -98,10 +92,10 @@ preprocess l | take 3 (dropWhile (==' ') $ reverse l) == "-- " = [] | otherwise = [l] - pState = defaultParserState - { stateSmart = True- , stateStandalone = True- , stateLiterateHaskell = True + pState = def+ { readerSmart = True+ , readerStandalone = True+ , readerExtensions = Set.insert Ext_literate_haskell $ readerExtensions def } interpreter :: BBlock -> BBlock@@ -109,11 +103,6 @@ = OneLineExercise (toUpper x) (isUpper x) e interpreter a = a - highlight :: BBlock -> BBlock- highlight (Text (CodeBlock ("",["sourceCode","literate","haskell"],[]) code)) | mode == AgdaMode- = (Text (RawBlock "html" $ highlightAgdaAsXHtml code))- highlight a = a- ------------------------------ collectTests :: ParseMode -> [BBlock] -> IO [BBlock]@@ -135,38 +124,7 @@ f x _ = return x processLines :: ParseMode -> Bool -> String -> IO ([String], [String], [Name])-processLines AgdaMode = processAgdaLines processLines HaskellMode = processHaskellLines--{- Agda support (unfinished) -}-processAgdaLines :: Bool -> String -> IO ([String], [String], [Name])-processAgdaLines isExercise l_ = do--- return ([], [], [])-- let- l = parts l_-- x <- fmap (zip l) $ mapM (APar.parse APar.moduleParser . ("module X where\n"++) . unlines) l- let- names = map toName $ concatMap (getFName . snd . snd) x---- getFName [Agda.Module _ _ [Agda.TypedBindings _ (Agda.Arg _ _ [Agda.TBind _ a _])] declarations] --- = map Agda.boundName a- getFName [ASyn.Module _ _ _ [ASyn.TypeSig _ n _]]- = [n]- getFName _ = []---- isVisible [Agda.Module _ _ [Agda.TypedBindings _ (Agda.Arg _ _ [Agda.TBind _ a _])] declarations] --- = True- isVisible [ASyn.Module _ _ _ [ASyn.TypeSig _ n _]] = True- isVisible _ = not isExercise-- (visible, hidden) = partition (isVisible . snd . snd) x-- toName n = {- HSyn.Ident $-} show n-- return (concatMap fst visible, concatMap fst hidden, names)- processHaskellLines :: Bool -> String -> IO ([String], [String], [Name]) processHaskellLines isExercise l_ = return (concatMap fst visible, concatMap fst hidden, names)
QuickCheck.hs view
@@ -4,35 +4,51 @@ import ActiveHs.Base (WrapData2 (WrapData2), TestCase (TestCase)) import Lang import Result+import Logger import Qualify (qualify)+import Hash -import Data.Digest.Pure.MD5-import Language.Haskell.Interpreter hiding (eval) import Test.QuickCheck hiding (Result) import qualified Test.QuickCheck.Property as QC import Data.Char (isLower) import Data.List (intercalate)+import Control.Monad (join) import Control.Concurrent.MVar --------------------------------------- quickCheck- :: String -> MD5Digest -> Language -> TaskChan -> FilePath -> String -> [String] -> [([String],String)] + :: String+ -> Hash+ -> Language+ -> TaskChan+ -> FilePath+ -> String+ -> [String]+ -> [([String],String)] -- test cases -> IO [Result]-quickCheck qualifier m5 lang ch fn ft funnames is- = case allRight $ map (qualify qualifier funnames . snd) is of- Left err -> return [Error True err]- Right s_ -> interp False m5 lang ch fn "" $ \a ->- do m <- interpret (mkTestCases [(v,s,s') | ((v,s),s')<- zip is s_]) (as :: [TestCase])- return $ qcs lang m+quickCheck qualifier m5 lang ch fn ft funnames testcases = do+ logStrMsg 3 (logger ch) $ "test cases: " ++ show testcases+ logStrMsg 3 (logger ch) $ "names to be qualified: " ++ show funnames - where- allRight :: [Either a b] -> Either a [b]- allRight x = case [s | Left s<-x] of- (y:_) -> Left y- [] -> Right [s | Right s<-x]+ case allRight $ map (qualify qualifier funnames . snd) testcases of+ Left err -> do+ logStrMsg 3 (logger ch) $ "Error in qualification: " ++ err+ return [Error True err]+ Right s_ -> do+ logStrMsg 3 (logger ch) $ "Qualified expressions: " ++ show s_ + let ts = mkTestCases [(v,s,s') | ((v,s),s')<- zip testcases s_]+ logStrMsg 3 (logger ch) $ "Test cases: " ++ ts+ + interp False m5 lang ch fn "" $ \a ->+ do liftIO $ logStrMsg 3 (logger ch) "Before interpretation"+ m <- interpret ts (as :: [TestCase])+ liftIO $ logStrMsg 3 (logger ch) "After interpretation"+ return $ qcs lang (logger ch) m++ where mkTestCases ss = "[" ++ intercalate ", " (map mkTestCase ss) ++ "]" @@ -41,7 +57,6 @@ ++ unwords ["(" ++ v ++ ")" | v<-vars] ++ " -> qcinner (" ++ showTr vars s ++ ", " ++ parens s ++ ", " ++ parens s2 ++ "))" - showTr vars s = "unwords [" ++ intercalate ", " (map g $ words s) ++ "]" -- !!! where @@ -52,31 +67,39 @@ g x | x `elem` vs = {- "\"(\" ++ -} " show " ++ x -- ++ " ++ \")\"" g x = show x -qcs :: Language -> [TestCase] -> IO [Result]-qcs lang [] = return [Message (translate lang "All test cases are completed.") Nothing]-qcs lang (t:ts) = do- s' <- qc lang t- case s' of- Just rep -> rep- Nothing -> qcs lang ts+qcs :: Language -> Logger -> [TestCase] -> IO [Result]+qcs lang log = join . foldM (return [Message (translate lang "All test cases are completed.") Nothing]) (qc lang log) -- test = qc $ TestCase $ \f (QCNat x) (QCInt y) -> f (show x ++ " + " ++ show y, min 10 (x + y), x + y) -- test' = qc $ TestCase $ \f (QCInt x) -> f ("sqr " ++ show x, min 10 (x*x), x*x) -qc :: Language -> TestCase -> IO (Maybe (IO [Result]))-qc lang (TestCase p) = do+qc :: Language -> Logger -> TestCase -> IO (Maybe (IO [Result]))+qc lang log (TestCase p) = do v <- newMVar Nothing- _ <- quickCheckWithResult (stdArgs { chatty = False }) $ {- QC.noShrinking $ -} p $ ff v+ let ff (s, x, y)+ = QC.whenFail (modifyMVar_ v $ const $ return $ Just $ fmap (ModifyCommandLine s :) res)+ $ QC.morallyDubiousIOProperty+ $ fmap (\s -> if hasError s then QC.failed else QC.succeeded) res+ where+ res = do+ logStrMsg 4 log $ "compare: " ++ s+ compareClearGen lang "noId" $ WrapData2 x y+ _ <- quickCheckWithResult (stdArgs { chatty = False }) $ {- QC.noShrinking $ -} p ff takeMVar v- where- ff v (s, x, y)- = QC.whenFail (modifyMVar_ v $ const $ return $ Just $ fmap (ModifyCommandLine s :) res)- $ QC.morallyDubiousIOProperty- $ fmap f res- where- res = compareClearGen lang "noId" $ WrapData2 x y - f s | hasError s = QC.failed- f s = QC.succeeded+------------------------------------++allRight :: [Either a b] -> Either a [b]+allRight x = case [s | Left s<-x] of+ (y:_) -> Left y+ [] -> Right [s | Right s<-x]++foldM :: Monad m => r -> (a -> m (Maybe r)) -> [a] -> m r+foldM end _ [] = return end+foldM end f (t:ts) = do+ x <- f t+ case x of+ Just r -> return r+ Nothing -> foldM end f ts
Result.hs view
@@ -51,8 +51,10 @@ errors _ = False filterResults :: [Result] -> [Result]-filterResults rs = case filter (not . weakError) rs of- [] -> take 1 rs+filterResults rs = case filter (not . weakOrHardError) rs of+ [] -> case [e | e@(Error True _) <- rs] of+ [] -> take 1 rs+ rs -> take 1 rs rs -> case filter (not . searchResult) rs of [] -> rs rs -> {- nubBy f -} rs@@ -63,14 +65,14 @@ -} hasError :: [Result] -> Bool-hasError rs = case filter (not . weakError) rs of+hasError rs = case filter (not . weakOrHardError) rs of [] -> True rs -> any errors rs -weakError :: Result -> Bool-weakError (Error _ _) = True-weakError (ExprType b _ _ _) = b-weakError _ = False+weakOrHardError :: Result -> Bool+weakOrHardError (Error _ _) = True+weakOrHardError (ExprType b _ _ _) = b+weakOrHardError _ = False searchResult :: Result -> Bool searchResult (SearchResults _ _) = True
Simple.hs view
@@ -4,12 +4,18 @@ ( Task (..), TaskChan , startGHCiServer , restartGHCiServer- , interpret+ , sendToServer , catchError_fixed++ , Interpreter, typeOf, kindOf+ , InterpreterError (..), errMsg, interpret+ , as, liftIO, parens ) where -import Language.Haskell.Interpreter hiding (interpret)+import Logger +import Language.Haskell.Interpreter+ import Control.Concurrent (forkIO) import Control.Concurrent.MVar (MVar, newEmptyMVar, takeMVar, putMVar) import Control.Concurrent.Chan (Chan, newChan, readChan, writeChan)@@ -17,7 +23,7 @@ import Control.Monad (when, forever) import Control.Monad.Error (MonadError, catchError) import Data.List (isPrefixOf)-import Prelude hiding (catch)+--import Prelude hiding (catch) ------------------------- @@ -29,17 +35,17 @@ --------------- -startGHCiServer :: [String] -> (String -> IO ()) -> (String -> IO ()) -> IO TaskChan-startGHCiServer paths{-searchpaths-} logError logMsg = do+startGHCiServer :: [String] -> Logger -> IO TaskChan+startGHCiServer paths{-searchpaths-} log = do ch <- newChan _ <- forkIO $ forever $ do- logMsg "start interpreter"+ logStrMsg 1 log "start interpreter" e <- runInterpreter (handleTask ch Nothing) `catch` \(e :: SomeException) -> return $ Left $ UnknownError "GHCi server died." case e of- Left e -> logError $ "stop interpreter: " ++ show e+ Left e -> logStrMsg 0 log $ "stop interpreter: " ++ show e Right () -> return () return $ TC ch@@ -50,7 +56,7 @@ task <- lift $ readChan ch case task of Just task -> handleTask_ ch oldFn task- Nothing -> liftIO $ logError "interpreter stopped intentionally"+ Nothing -> liftIO $ logStrMsg 0 log "interpreter stopped intentionally" handleTask_ ch oldFn (Task fn repVar m) = do (cont, res) <- do @@ -75,8 +81,8 @@ restartGHCiServer :: TaskChan -> IO () restartGHCiServer (TC ch) = writeChan ch Nothing -interpret :: TaskChan -> FilePath -> Interpreter a -> IO (Either InterpreterError a)-interpret (TC ch) fn m = do+sendToServer :: TaskChan -> FilePath -> Interpreter a -> IO (Either InterpreterError a)+sendToServer (TC ch) fn m = do rep <- newEmptyMVar writeChan ch $ Just $ Task fn rep m takeMVar rep
Smart.hs view
@@ -1,11 +1,23 @@ {-# LANGUAGE ViewPatterns, PatternGuards, OverloadedStrings #-}-module Smart where+module Smart+ ( module Simple+ , startGHCiServer+ , restart+ , TaskChan (..)+ , interp+ , compareClearGen+ , compareMistGen+ , wrap2+ ) where import HoogleCustom import Specialize import Lang import Result+import Logger+import Simple hiding (TaskChan, startGHCiServer) import qualified Simple+import Hash import ActiveHs.Base (WrapData2 (..), WrapData(..)) import Graphics.Diagrams (Diagram)@@ -18,23 +30,14 @@ import Data.Data.GenRep.Functions (mistify, numberErrors) import Data.Data.GenRep.Doc (toDoc) -import Language.Haskell.Interpreter hiding (eval)-import Data.Digest.Pure.MD5 import Hoogle (Database, loadDatabase)-import System.FastLogger -import System.Locale (defaultTimeLocale)-import Data.Time (getCurrentTime, formatTime)-import Data.ByteString.UTF8 (fromString)-import qualified Data.ByteString as B-import qualified Data.ByteString.Lazy.UTF8 as Lazy- import Control.Monad (join) import Data.Dynamic hiding (typeOf) import qualified Data.Data as D import Data.List (nub) import Data.Char (isAlpha)-import Prelude hiding (catch)+--import Prelude hiding (catch) ----------------------------------------------------------------------@@ -46,22 +49,15 @@ , chan :: Simple.TaskChan } -startGHCiServer :: [FilePath] -> FilePath -> FilePath -> IO TaskChan-startGHCiServer searchpaths logfilebase dbname = do- ti <- getCurrentTime- -- log <- newLogger $ logfilebase ++ "_" ++ formatTime defaultTimeLocale "%Y-%m-%d-%H:%M:%S" ti ++ ".log"- -- colons are not supported in filenames under windows- log <- newLogger $ logfilebase ++ "_" ++ formatTime defaultTimeLocale "%Y-%m-%d-%H-%M-%S" ti ++ ".log"+startGHCiServer :: [FilePath] -> Logger -> FilePath -> IO TaskChan+startGHCiServer searchpaths log dbname = do db <- if (dbname == "") then return Nothing else fmap Just $ loadDatabase dbname- ch <- Simple.startGHCiServer- searchpaths- (logMsgWithImportance 5 log . fromString) - (logMsgWithImportance 4 log . fromString)+ ch <- Simple.startGHCiServer searchpaths log return $ TC- { logger = log- , database = db- , chan = ch- }+ { logger = log+ , database = db+ , chan = ch+ } restart :: TaskChan -> IO () restart ch = do@@ -77,23 +73,6 @@ ---------------------------------------------------------------------- -logMsgWithImportance :: Int -> Logger -> B.ByteString -> IO ()-logMsgWithImportance n ch x = do- v <- timestampedLogEntry $ B.concat - [nn, " ", x, " ", nn]- logMsg ch v - where- nn = fromString $ replicate n '#'----------------------------------------------------------------------------mkId :: String -> MD5Digest-mkId = md5 . Lazy.fromString--------------------- getCommand :: String -> (String, String) getCommand (':':'?': (dropSpace -> Just x)) = ("?", x)@@ -108,7 +87,7 @@ dropSpace _ = Nothing -interp :: Bool -> MD5Digest -> Language -> TaskChan -> FilePath -> String +interp :: Bool -> Hash -> Language -> TaskChan -> FilePath -> String -> (String -> Interpreter (IO [Result])) -> IO [Result] interp verboseinterpreter (show -> idi) lang ch fn s@(getCommand -> (c, a)) xy = case c of@@ -120,7 +99,7 @@ c | c `elem` ["t","k",""] -> join $ fmap (either (return . map (Error True) . showErr lang) id)- $ Simple.interpret (chan ch) fn+ $ sendToServer (chan ch) fn $ case c of "t" -> catchE True $ do xx <- typeOf a
+ Snap.hs view
@@ -0,0 +1,25 @@+module Snap where++import Snap.Core+--import Snap.Http.Server (httpServe)+--import Snap.Http.Server.Config+--import Snap.Util.FileServe (getSafePath, serveDirectoryWith, simpleDirectoryConfig)++import Data.Text.Encoding (decodeUtf8With)+import Data.Text.Encoding.Error (lenientDecode)+import qualified Data.Text as T++--import Data.ByteString (ByteString)+import Data.ByteString.UTF8 (fromString)++--------------------++getTextParam :: String -> Snap (Maybe T.Text)+getTextParam = fmap (fmap $ decodeUtf8With lenientDecode) . getParam . fromString++redirectString :: String -> Snap ()+redirectString = redirect . fromString++pathString :: String -> Snap () -> Snap ()+pathString = path . fromString+
Special.hs view
@@ -6,20 +6,17 @@ import Smart import QuickCheck-import CheckAgdaCode import Result import Lang+import Logger import Html import Qualify (qualify)+import Hash import ActiveHs.Base (WrapData2) -import Language.Haskell.Interpreter hiding (eval)-import Data.Digest.Pure.MD5 (MD5Digest)- import qualified Data.Text as T import qualified Data.Text.IO as T-import Data.ByteString.UTF8 (fromString) import Control.DeepSeq import Control.Concurrent.MVar@@ -28,7 +25,7 @@ import System.Directory (getTemporaryDirectory) import Control.Concurrent (threadDelay, forkIO, killThread)-import Prelude hiding (catch)+--import Prelude hiding (catch) ---------------------------------------------------------------@@ -58,14 +55,14 @@ -> FilePath -> T.Text -> Language- -> MD5Digest+ -> Hash -> SpecialTask -> IO [Result] exerciseServer' qualifier ch verbose fn sol lang m5 task = do let error = do- logMsgWithImportance 5 (logger ch) $ fromString $ "Server error:" ++ show m5+ logStrMsg 0 (logger ch) $ "Server error:" ++ show m5 return [Error True "Server error."] action =@@ -100,8 +97,6 @@ ss <- quickCheck qualifier m5 lang ch fn' (T.unpack sol) funnames is let ht = head $ [x | ModifyCommandLine x <- ss] ++ [""] return [ShowInterpreter lang 59 (getTwo "eval2" (takeFileName fn) j i j) j 'E' ht ss]- "agda" -> do- typeCheckAgdaCode sourcedirs m5 lang {-ch-} fn' (T.unpack sol) tmpSaveHs :: String -> String -> T.Text -> IO FilePath tmpSaveHs ext x s = do@@ -110,7 +105,6 @@ tmp = tmpdir </> name ++ "." ++ ext T.writeFile tmp $ case ext of "hs" -> s- "agda" -> T.pack ("module " ++ name ++ " where\n\n") `T.append` s return tmp
activehs.cabal view
@@ -1,5 +1,5 @@ name: activehs-version: 0.3.0.1+version: 0.3.1 category: Education, Documentation synopsis: Haskell code presentation tool description:@@ -43,19 +43,19 @@ Simple, Smart, Cache,+ Hash, Specialize, Qualify, Lang, Result, HoogleCustom, Html,+ Logger, QuickCheck,- CheckAgdaCode,- AgdaHighlight,+ Snap, Special Build-Depends:- Agda >= 2.3.0.1 && < 2.4, highlighting-kate >= 0.5 && < 0.6, hoogle >= 4.2.11 && < 4.3, dia-base >= 0.1 && < 0.2,@@ -80,12 +80,12 @@ pureMD5 >= 2.1 && < 2.2, deepseq >= 1.1 && < 1.4, split >= 0.1 && < 0.3,- pandoc >= 1.8 && < 1.10,+ pandoc >= 1.10 && < 1.11, time >= 1.2 && < 1.5, old-time >= 1.0 && < 1.2, process >= 1.0 && < 1.2, hint >= 0.3.3.2 && < 0.4,- simple-reflect >= 0.2 && < 0.3,+ simple-reflect >= 0.2 && < 0.4, mtl >= 2.0 && < 2.2, old-locale >= 1.0 && < 1.1, cmdargs >= 0.7 && < 0.11