diff options
Diffstat (limited to 'lambda-calcul/haskell/src')
| -rw-r--r-- | lambda-calcul/haskell/src/Minilang/Lambda.hs | 25 | ||||
| -rw-r--r-- | lambda-calcul/haskell/src/Minilang/Lambda/Eval.hs | 9 | ||||
| -rw-r--r-- | lambda-calcul/haskell/src/Minilang/Lambda/Infer.hs | 10 | ||||
| -rw-r--r-- | lambda-calcul/haskell/src/Minilang/Lambda/Unify.hs | 5 | ||||
| -rw-r--r-- | lambda-calcul/haskell/src/Minilang/Log.hs | 140 | ||||
| -rw-r--r-- | lambda-calcul/haskell/src/Minilang/REPL/Net.hs | 178 | ||||
| -rw-r--r-- | lambda-calcul/haskell/src/Minilang/REPL/Run.hs | 60 | ||||
| -rw-r--r-- | lambda-calcul/haskell/src/Minilang/REPL/Types.hs | 2 | ||||
| -rw-r--r-- | lambda-calcul/haskell/src/Minilang/Server.hs | 71 |
9 files changed, 463 insertions, 37 deletions
diff --git a/lambda-calcul/haskell/src/Minilang/Lambda.hs b/lambda-calcul/haskell/src/Minilang/Lambda.hs new file mode 100644 index 0000000..9d0f3cf --- /dev/null +++ b/lambda-calcul/haskell/src/Minilang/Lambda.hs @@ -0,0 +1,25 @@ +module Minilang.Lambda where + +import Minilang.Lambda.DeBruijn (eval, fromDeBruijn, toDeBruijn) +import Minilang.Lambda.Eval (Env, Term) +import Minilang.Lambda.Infer (Context, TypeError, infer) +import Minilang.Lambda.Parser (AST, desugar) +import Minilang.Lambda.Unify (Type) + +-- | Top-level evaluator +-- Load an AST into given `Env` and `Context`, returning an extended +-- `Env` and `Context` with declarations bound +loadProgram :: + AST -> + Env -> + Context -> + Either TypeError (Term, Type, Env, Context) +-- loadProgram (Let d r) ρ γ = do +-- (ρ', γ') <- checkD 0 d ρ γ +-- loadProgram r ρ' γ' +loadProgram expr env context = + let term = desugar expr + in case infer term of + Left typeError -> Left typeError + Right typ -> + Right (fromDeBruijn $ eval (toDeBruijn term), typ, env, context) diff --git a/lambda-calcul/haskell/src/Minilang/Lambda/Eval.hs b/lambda-calcul/haskell/src/Minilang/Lambda/Eval.hs index 58f8ba6..7f7aad7 100644 --- a/lambda-calcul/haskell/src/Minilang/Lambda/Eval.hs +++ b/lambda-calcul/haskell/src/Minilang/Lambda/Eval.hs @@ -1,13 +1,16 @@ +{-# LANGUAGE DeriveAnyClass #-} + module Minilang.Lambda.Eval where -import Data.Text (Text, unpack) -import Debug.Trace (trace) +import Data.Aeson (FromJSON, ToJSON) +import Data.Text (Text) +import GHC.Generics (Generic) data Term = Var Text | Lam Text Term | App Term Term - deriving (Show, Read, Eq) + deriving (Show, Read, Eq, Generic, ToJSON, FromJSON) type Env = [(Text, Term)] diff --git a/lambda-calcul/haskell/src/Minilang/Lambda/Infer.hs b/lambda-calcul/haskell/src/Minilang/Lambda/Infer.hs index 94fecb3..2e1814e 100644 --- a/lambda-calcul/haskell/src/Minilang/Lambda/Infer.hs +++ b/lambda-calcul/haskell/src/Minilang/Lambda/Infer.hs @@ -1,13 +1,16 @@ {-# LANGUAGE LambdaCase #-} +{-# LANGUAGE DeriveAnyClass #-} module Minilang.Lambda.Infer where import Control.Monad.State (MonadState (..), StateT, evalStateT, modify) +import Data.Aeson (FromJSON, ToJSON) import Data.Bifunctor (first) import Data.Char (chr, ord) import qualified Data.List as List import qualified Data.Map as Map import Data.Text (Text, pack) +import GHC.Generics (Generic) import qualified Minilang.Lambda.Eval as Eval import Minilang.Lambda.Unify (Type (..), UnifyError, apply, unify) import Prelude hiding (lookup) @@ -48,8 +51,11 @@ typeOf (Var _ t) = t typeOf (Lam _ _ t) = t typeOf (App _ _ t) = t -data Context = Context {nextVar :: Int, typeContext :: Map.Map Text Type} - deriving (Eq, Show) +data Context = Context + { nextVar :: Int, + typeContext :: Map.Map Text Type + } + deriving (Eq, Show, Generic, ToJSON, FromJSON) annotate :: Eval.Term -> Either TypeError (ATerm Type) annotate t = diff --git a/lambda-calcul/haskell/src/Minilang/Lambda/Unify.hs b/lambda-calcul/haskell/src/Minilang/Lambda/Unify.hs index df66113..f3fff04 100644 --- a/lambda-calcul/haskell/src/Minilang/Lambda/Unify.hs +++ b/lambda-calcul/haskell/src/Minilang/Lambda/Unify.hs @@ -1,15 +1,18 @@ -- ported from https://www.cs.cornell.edu/courses/cs3110/2011sp/Lectures/lec26-type-inference/type-inference.htm {-# LANGUAGE LambdaCase #-} +{-# LANGUAGE DeriveAnyClass #-} module Minilang.Lambda.Unify where import Data.Text (Text) +import GHC.Generics (Generic) +import Data.Aeson (ToJSON, FromJSON) type Identifier = Text data Type = TyVar Text | Type :-> Type - deriving (Show, Eq) + deriving (Show, Eq, Generic, ToJSON, FromJSON) infixr 5 :-> diff --git a/lambda-calcul/haskell/src/Minilang/Log.hs b/lambda-calcul/haskell/src/Minilang/Log.hs new file mode 100644 index 0000000..bae4f19 --- /dev/null +++ b/lambda-calcul/haskell/src/Minilang/Log.hs @@ -0,0 +1,140 @@ +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# OPTIONS_GHC -Wall -Werror #-} +{-# OPTIONS_GHC -Wno-missing-fields #-} + +-- | A simple logger that reads `LogEntry` from a `TBChan` and dumps JSON-formatted +-- strings to `stdout`. +module Minilang.Log + ( -- * Types + LoggerEnv, + + -- * Constructor & Destructor + newLog, + stopLogger, + fakeLogger, + + -- * Logging functions + logInfo, + logError, + withLog, + ) +where + +import Control.Concurrent.Async (Async, async, cancel) +import Control.Concurrent.STM (TChan, atomically, newTChan, readTChan, writeTChan) +import Control.Monad (forever) +import Control.Monad.Trans (MonadIO (..)) +import Data.Aeson +import qualified Data.ByteString as BS +import qualified Data.ByteString.Lazy as LBS +import Data.Text (Text) +import Data.Time.Clock + ( UTCTime, + diffUTCTime, + getCurrentTime, + ) +import System.IO (Handle, stdout) + +-- | Environment to control a logger thread. +data LoggerEnv m = LoggerEnv + { logger :: Maybe Logger, + loggerId :: Text, + logInfo :: forall a. (ToJSON a) => a -> m (), + logError :: forall a. (ToJSON a) => a -> m (), + withLog :: forall a b. (ToJSON a) => a -> m b -> m b, + stopLogger :: m () + } + +type Logger = TChan BS.ByteString + +fakeLogger :: (MonadIO m) => LoggerEnv m +fakeLogger = LoggerEnv Nothing "foo" (const $ pure ()) (const $ pure ()) (const id) (pure ()) + +-- | Starts an asynchronous log-processing thread and returns an initialised `LoggerEnv`. +newLog :: (MonadIO m) => Text -> m (LoggerEnv m) +newLog loggerId = liftIO $ do + chan <- liftIO $ atomically newTChan + loggerThread <- async $ runLog chan stdout + return $ + LoggerEnv + { logger = Just chan, + logInfo = logEvent' chan loggerId, + logError = logError' chan loggerId, + withLog = withLog' chan loggerId, + stopLogger = stopLogger' loggerThread, + loggerId + } + +runLog :: TChan BS.ByteString -> Handle -> IO a +runLog chan hdl = forever $ do + toLog <- atomically $ readTChan chan + BS.hPutStr hdl . (<> "\n") $ toLog + +stopLogger' :: (MonadIO m) => Async () -> m () +stopLogger' = liftIO . cancel + +logEvent' :: (ToJSON a, MonadIO m) => Logger -> Text -> a -> m () +logEvent' chan logId message = do + ts <- liftIO getCurrentTime + liftIO $ + atomically $ + writeTChan chan $ + LBS.toStrict $ + encode $ + object + [ "timestamp" .= ts, + "loggerId" .= logId, + "message" .= message + ] + +withLog' :: (ToJSON a, MonadIO m) => Logger -> Text -> a -> m b -> m b +withLog' chan logId message act = do + startTime <- liftIO getCurrentTime + logStart chan logId startTime message + b <- act + endTime <- liftIO getCurrentTime + logEnd chan logId startTime endTime message + pure b + +logStart :: (ToJSON a, MonadIO m) => Logger -> Text -> UTCTime -> a -> m () +logStart chan logId ts command = + liftIO $ + atomically $ + writeTChan chan $ + LBS.toStrict $ + encode $ + object + [ "timestamp" .= ts, + "servicer" .= logId, + "message" .= command + ] + +logEnd :: (ToJSON a, MonadIO m) => Logger -> Text -> UTCTime -> UTCTime -> a -> m () +logEnd chan logId ts en outcome = + liftIO $ + atomically $ + writeTChan chan $ + LBS.toStrict $ + encode $ + object + [ "timestamp" .= en, + "durationMs" .= (diffUTCTime en ts * 1000), + "servicer" .= logId, + "message" .= outcome + ] + +logError' :: (ToJSON a, MonadIO m) => Logger -> Text -> a -> m () +logError' chan logId err = liftIO $ do + ts <- liftIO getCurrentTime + liftIO $ + atomically $ + writeTChan chan $ + LBS.toStrict $ + encode $ + object + [ "timestamp" .= ts, + "servicer" .= logId, + "error" .= err + ] diff --git a/lambda-calcul/haskell/src/Minilang/REPL/Net.hs b/lambda-calcul/haskell/src/Minilang/REPL/Net.hs new file mode 100644 index 0000000..1bafeaa --- /dev/null +++ b/lambda-calcul/haskell/src/Minilang/REPL/Net.hs @@ -0,0 +1,178 @@ +{-# LANGUAGE GeneralizedNewtypeDeriving #-} + +-- | A version of REPL that interacts through a websocket. +module Minilang.REPL.Net where + +import Control.Concurrent.STM (atomically) +import Control.Concurrent.STM.TVar +import Control.Monad.Catch +import Control.Monad.State +import Data.Aeson + ( ToJSON, + eitherDecode, + encode, + object, + (.=), + ) +import Data.ByteString (ByteString) +import qualified Data.ByteString.Lazy as LBS +import Data.Either (fromRight) +import Data.Map as Map +import Data.Serialize hiding (encode) +import Data.Text (Text, pack, unpack) +import Data.Text.Encoding (decodeUtf8With) +import Data.Text.Encoding.Error (lenientDecode) +import Minilang.Log +import Minilang.REPL (withInputs) +import Minilang.REPL.Purer (purerREPL) +import Minilang.REPL.Run (runREPL) +import Minilang.REPL.Types +import Network.Wai (Application) +import Network.Wai.Handler.WebSockets +import qualified Network.WebSockets as WS +import System.Directory (getCurrentDirectory) +import System.FilePath (takeFileName, (</>)) + +-- | Configuration of the WS server +data ServerConfig = ServerConfig + { -- | The host/IP to listen on. If 0.0.0.0, then the server listens + configHost :: String, + -- | The port to listen on. If 0, a random port will be assigned. + configPort :: Int + } + deriving (Eq, Show) + +data NetEnv = NetEnv + { connection :: WS.Connection, + logger :: LoggerEnv IO, + repl :: TVar REPLEnv + -- , storage :: FileStorage + } + +newtype Net m a = Net {runNet :: StateT NetEnv m a} + deriving (Functor, Applicative, Monad, MonadTrans, MonadIO, MonadState NetEnv) + +instance Serialize In where + put out = do + let bs = encode out + putWord64be (fromIntegral $ LBS.length bs) + putLazyByteString bs + + get = do + len <- getWord64be + bs <- getLazyByteString (fromIntegral len) + case eitherDecode bs of + Right out -> pure out + Left err -> fail err + +-- doStore :: In -> Net IO (Either Text ()) +-- doStore out = do +-- fs <- gets storage +-- res <- liftIO $ store fs (pure $ Right out) handleStorageResult +-- case res of +-- WriteSucceed _ -> pure $ Right () +-- err -> pure $ Left (pack $ show err) +-- where +-- handleStorageResult (Right (WriteSucceed _)) = pure $ Right () +-- handleStorageResult (Right err) = pure $ Left $ pack $ show err +-- handleStorageResult (Left err) = pure $ Left $ pack err + +netLog :: (ToJSON a) => a -> Net IO () +netLog logEntry = gets logger >>= liftIO . flip logInfo logEntry + +instance MonadREPL (Net IO) where + input = do + inp <- gets connection >>= lift . wsReceive + -- res <- doStore inp + -- case res of + -- Right () -> netLog (object ["action" .= ("input" :: Text), "content" .= inp]) + -- Left txt -> netLog (object ["action" .= ("storageError" :: Text), "content" .= txt]) + netLog (object ["action" .= ("input" :: Text), "content" .= inp]) + pure inp + + output a = do + gets connection >>= lift . wsSend a + netLog (object ["action" .= ("output" :: Text), "content" .= a]) + + prompt = pure () + getEnv = gets repl >>= lift . readTVarIO + setEnv e' = gets repl >>= lift . atomically . flip writeTVar e' + + -- TODO what does this mean? perhaps it coiuld be used to load some + -- virtual files edited by user in their env? + load = const (pure (Right "")) + +instance (MonadThrow m) => MonadThrow (Net m) where + throwM = lift . throwM + +instance (MonadCatch m) => MonadCatch (Net m) where + Net m `catch` f = Net $ m `catch` \e -> runNet (f e) + +-- instance TypeChecker (Net IO) where +-- emit (CheckD ev) = gets logger >>= \env -> liftIO $ logInfo env ev +-- emit _ = pure () + +wsReceive :: WS.Connection -> IO In +wsReceive cnx = + fromRight (In "") . eitherDecode <$> WS.receiveData cnx + +wsSend :: Out -> WS.Connection -> IO () +wsSend out cnx = + WS.sendBinaryData cnx (encode out) + +safeDecodeUtf8 :: ByteString -> Text +safeDecodeUtf8 = decodeUtf8With lenientDecode + +clientHandler :: LoggerEnv IO -> TVar (Map ByteString (TVar REPLEnv)) -> WS.PendingConnection -> IO () +clientHandler loggerEnv envs cnx = do + let path = WS.requestPath $ WS.pendingRequest cnx + logInfo loggerEnv $ object ["action" .= ("StartedREPL" :: Text), "path" .= safeDecodeUtf8 path] + conn <- WS.acceptRequest cnx + -- storageFile <- mkStorageFile path + -- withStorage storageFile $ \fileStorage -> do + replEnv <- newREPLEnv + WS.withPingThread conn 30 (pure ()) $ + evalStateT (runNet runREPL) (NetEnv conn loggerEnv replEnv) + where + newREPLEnv = newTVarIO initialREPL + +-- findOrCreateREPL :: (H.Store IO store) => store -> ByteString -> IO (TVar REPLEnv) +-- findOrCreateREPL storageFile path = do +-- (env, shouldLoad) <- atomically $ do +-- envMaps <- readTVar envs +-- (newEnv, shouldLoad) <- case Map.lookup path envMaps of +-- Nothing -> newTVar initialREPL >>= \v -> pure (v, True) +-- Just e -> pure (e, False) +-- writeTVar envs (Map.insert path newEnv envMaps) +-- pure (newEnv, shouldLoad) +-- -- FIXME there is a race condition here +-- if shouldLoad +-- then replay storageFile env +-- else pure env + +-- mkStorageFile path = do +-- let f = takeFileName (unpack (safeDecodeUtf8 path)) +-- dir <- getCurrentDirectory +-- pure $ defaultOptions {storageFilePath = dir </> f} + +-- replay :: (H.Store IO store) => store -> TVar REPLEnv -> IO (TVar REPLEnv) +-- replay storage envVar = do +-- res <- H.load storage +-- case res of +-- LoadSucceed coms -> do +-- atomically $ do +-- env <- readTVar envVar +-- let newEnv = withInputs env coms +-- writeTVar envVar (purerREPL newEnv) +-- logInfo loggerEnv $ +-- object +-- [ "action" .= ("Loaded" :: Text), +-- "numCommands" .= length coms +-- ] +-- pure envVar +-- err -> do +-- logInfo loggerEnv $ object ["action" .= ("ErrorLoading" :: Text), "error" .= pack (show err)] +-- pure envVar + +runNetREPL :: LoggerEnv IO -> TVar (Map ByteString (TVar REPLEnv)) -> Application -> Application +runNetREPL loggerEnv envs = websocketsOr WS.defaultConnectionOptions (clientHandler loggerEnv envs) diff --git a/lambda-calcul/haskell/src/Minilang/REPL/Run.hs b/lambda-calcul/haskell/src/Minilang/REPL/Run.hs index a4b50f4..c90ecde 100644 --- a/lambda-calcul/haskell/src/Minilang/REPL/Run.hs +++ b/lambda-calcul/haskell/src/Minilang/REPL/Run.hs @@ -10,11 +10,12 @@ import Control.Monad.Catch import Data.Text hiding (replicate) import qualified Data.Text as Text import Debug.Trace (trace) +import Minilang.Lambda (loadProgram) import Minilang.Lambda.DeBruijn (eval, fromDeBruijn, toDeBruijn) +import Minilang.Lambda.Eval (newEnv) import Minilang.Lambda.Infer (infer, newContext) import Minilang.Lambda.Parser (desugar, parse) import Minilang.REPL.Types -import Minilang.Lambda.Eval (newEnv) -- | Run a REPL session runREPL :: @@ -49,41 +50,40 @@ handleCommand :: (MonadCatch m, MonadREPL m) => Command -> m () -handleCommand ClearEnv = getEnv >>= \e -> setEnv (e{env = newEnv, context = newContext}) +handleCommand ClearEnv = getEnv >>= \e -> setEnv (e {env = newEnv, context = newContext}) handleCommand DumpEnv = - getEnv >>= \REPLEnv{..} -> - output (CurrentEnv env context) + getEnv >>= \REPLEnv {..} -> + output (CurrentEnv env context) handleCommand (Load (File file)) = do - t <- load file - case t of - Left err -> output (Msg $ pack $ show err) - Right prog -> loadProgramInEnv prog + t <- load file + case t of + Left err -> output (Msg $ pack $ show err) + Right prog -> loadProgramInEnv prog handleCommand (Load (Data prog)) = loadProgramInEnv prog -handleCommand (Set (StepTypeChecker st)) = getEnv >>= \e -> setEnv (e{stepTypeCheck = st}) -handleCommand (Set (DebugParser st)) = getEnv >>= \e -> setEnv (e{debugParser = st}) +handleCommand (Set (StepTypeChecker st)) = getEnv >>= \e -> setEnv (e {stepTypeCheck = st}) +handleCommand (Set (DebugParser st)) = getEnv >>= \e -> setEnv (e {debugParser = st}) handleCommand Help = - output (Msg helpText) + output (Msg helpText) loadProgramInEnv :: (MonadCatch m, MonadREPL m) => Text -> m () -loadProgramInEnv prog = undefined -- do --- repl@REPLEnv{rho = ρ, gamma = γ, debugParser} <- getEnv --- case runParser program (ParserState debugParser) "" (unpack prog) of --- Left err -> output (Msg $ pack $ show err) --- Right e -> --- ( do --- (ρ', γ') <- loadProgram e ρ γ --- setEnv (repl{rho = ρ', gamma = γ'}) --- output (Msg makeMessage) --- ) --- `catch` \(TypingError err) -> output (Msg err) --- where --- makeMessage = --- "Loaded \"" --- <> ( if Text.length prog > 15 --- then Text.take 15 prog <> "..." --- else prog --- ) --- <> "\"" +loadProgramInEnv prog = do + repl@REPLEnv {env, context} <- getEnv + case parse prog of + Left err -> output (Msg $ pack $ show err) + Right e -> do + case loadProgram e env context of + Left typeError -> output (Msg $ pack $ show typeError) + Right (term, typ, env', context') -> do + setEnv (repl {env = env', context = context'}) + output (Evaluated term typ) + where + makeMessage = + "Loaded \"" + <> ( if Text.length prog > 15 + then Text.take 15 prog <> "..." + else prog + ) + <> "\"" diff --git a/lambda-calcul/haskell/src/Minilang/REPL/Types.hs b/lambda-calcul/haskell/src/Minilang/REPL/Types.hs index 383987b..3a82018 100644 --- a/lambda-calcul/haskell/src/Minilang/REPL/Types.hs +++ b/lambda-calcul/haskell/src/Minilang/REPL/Types.hs @@ -78,7 +78,7 @@ data Out | CurrentEnv Env Context | Msg Text | Bye - deriving (Eq, Show, Generic) + deriving (Eq, Show, Generic, ToJSON, FromJSON) data Flag = StepTypeChecker Bool diff --git a/lambda-calcul/haskell/src/Minilang/Server.hs b/lambda-calcul/haskell/src/Minilang/Server.hs new file mode 100644 index 0000000..5c34db4 --- /dev/null +++ b/lambda-calcul/haskell/src/Minilang/Server.hs @@ -0,0 +1,71 @@ +{-# LANGUAGE TypeApplications #-} + +-- | An HTTP server providing a basic REPL and text editor to work +-- collaboratively on Minilang code. +module Minilang.Server where + +import Control.Concurrent.Async +import Control.Concurrent.STM.TVar +import Data.Aeson + ( Value, + decode, + object, + (.=), + ) +import Data.ByteString.Lazy (fromStrict) +import Data.Default +import Data.Text (Text) +import Minilang.Log +import Minilang.REPL.Net +import Network.Wai +import Network.Wai.Application.Static +import Network.Wai.Handler.Warp as Warp +import Network.Wai.Middleware.RequestLogger +import Network.Wai.Middleware.RequestLogger.JSON +import System.Log.FastLogger (fromLogStr) +import Control.Concurrent.Async + +data Server = Server + { serverThread :: Maybe (Async ()) + -- ^If the server is running, this will contain the underlying + , serverPort :: Int + -- ^The actual port this server is listening on. Useful when + } + +-- | Starts HTTP server on given port. +-- This server serves static files from public/ directory and also +-- exposes a WebSocket-based REPL under `/repl` path. +startServer :: Int -> IO Server +startServer serverPort = do + envs <- newTVarIO mempty + logger <- newLog "minilang" + loggerMiddleware <- runHTTPLog logger + let app = loggerMiddleware $ runNetREPL logger envs staticResources + (port, action) <- startWarp serverPort app + thread <- async action + logInfo logger $ object ["action" .= ("Started" :: Text), "port" .= port] + pure $ Server (Just thread) port + where + startWarp 0 app = do + (port, socket) <- openFreePort + pure (port, Warp.runSettingsSocket defaultSettings socket app) + startWarp port app = pure (port, Warp.run port app) + + runHTTPLog logger = + mkRequestLogger $ + def + { outputFormat = CustomOutputFormatWithDetails formatAsJSON, + destination = Callback (\str -> logInfo logger (decode @Value $ fromStrict $ fromLogStr str)) + } + +stopServer :: Server -> IO () +stopServer (Server (Just th) _) = cancel th +stopServer _ = pure () + +waitServer :: Server -> IO () +waitServer (Server (Just th) _) = wait th +waitServer _ = pure () + +-- | Serve static resources under `public/` directory +staticResources :: Application +staticResources = staticApp (defaultFileServerSettings "public") |