diff options
Diffstat (limited to 'lambda-calcul/haskell')
| -rw-r--r-- | lambda-calcul/haskell/src/Minilang/API.hs | 72 | ||||
| -rw-r--r-- | lambda-calcul/haskell/src/Minilang/App.hs | 68 | ||||
| -rw-r--r-- | lambda-calcul/haskell/src/Minilang/Lambda.hs | 78 | ||||
| -rw-r--r-- | lambda-calcul/haskell/src/Minilang/Lambda/Unify.hs | 5 | ||||
| -rw-r--r-- | lambda-calcul/haskell/src/Minilang/REPL.hs | 35 | ||||
| -rw-r--r-- | lambda-calcul/haskell/src/Minilang/REPL/Pure.hs | 21 | ||||
| -rw-r--r-- | lambda-calcul/haskell/src/Minilang/REPL/Run.hs | 50 | ||||
| -rw-r--r-- | lambda-calcul/haskell/src/Minilang/REPL/Types.hs | 58 | ||||
| -rw-r--r-- | lambda-calcul/haskell/test/Minilang/IntegrationSpec.hs | 17 | ||||
| -rw-r--r-- | lambda-calcul/haskell/test/Minilang/Lambda/ParserSpec.hs | 15 | ||||
| -rw-r--r-- | lambda-calcul/haskell/test/Minilang/REPL/NetSpec.hs | 45 | ||||
| -rw-r--r-- | lambda-calcul/haskell/test/Minilang/REPLSpec.hs | 68 | ||||
| -rw-r--r-- | lambda-calcul/haskell/test/Minilang/ServerSpec.hs | 12 |
13 files changed, 279 insertions, 265 deletions
diff --git a/lambda-calcul/haskell/src/Minilang/API.hs b/lambda-calcul/haskell/src/Minilang/API.hs index 0be70ff..9638da8 100644 --- a/lambda-calcul/haskell/src/Minilang/API.hs +++ b/lambda-calcul/haskell/src/Minilang/API.hs @@ -17,25 +17,25 @@ import Data.Data (Proxy (..)) import Data.Text (Text) import Data.Time (UTCTime) import GHC.Generics (Generic) -import Servant - ( Delete, - Description, - FromHttpApiData, - Get, - JSON, - Post, - QueryParam, - Raw, - ReqBody, - StdMethod (POST), - Summary, - ToHttpApiData, - Verb, - parseUrlPiece, - toUrlPiece, - (:<|>), - (:>), - ) +import Servant ( + Delete, + Description, + FromHttpApiData, + Get, + JSON, + Post, + QueryParam, + Raw, + ReqBody, + StdMethod (POST), + Summary, + ToHttpApiData, + Verb, + parseUrlPiece, + toUrlPiece, + (:<|>), + (:>), + ) import System.Random (StdGen, uniformList) type LambdaAPI = @@ -91,12 +91,13 @@ type GetNextChallenge = type PostAnswer = Summary - "Post an answer to the current challenge for the given user." :> - Description "The answer should be given as JSON string representing the result \ - \of evaluating the current challenge's expression in the untyped λ-calculus. This \ - \textual representation should be consistent with the grammar given in the REPL's \ - \\"Help\" panel. Expect to be surprised 🤔 !\ - \" + "Post an answer to the current challenge for the given user." + :> Description + "The answer should be given as JSON string representing the result \ + \of evaluating the current challenge's expression in the untyped λ-calculus. This \ + \textual representation should be consistent with the grammar given in the REPL's \ + \\"Help\" panel. Expect to be surprised 🤔 !\ + \" :> "api" :> "challenge" :> QueryParam "token" Token @@ -107,10 +108,10 @@ lambdaAPI :: Proxy LambdaAPI lambdaAPI = Proxy data Score = Score - { user :: User, - grade :: Int, - lastTest :: Maybe UTCTime, - lastResult :: Maybe Bool + { user :: User + , grade :: Int + , lastTest :: Maybe UTCTime + , lastResult :: Maybe Bool } deriving (Eq, Show, Generic, ToJSON, FromJSON) @@ -130,16 +131,15 @@ newToken :: StdGen -> (ByteString, StdGen) newToken = first LBS.pack . uniformList 16 data Challenge = Challenge - { level :: Int, - expr :: Text, - description :: Text, - answer :: Text + { level :: Int + , expr :: Text + , description :: Text } deriving (Eq, Show, Generic, ToJSON, FromJSON) defaultChallenges :: [Challenge] defaultChallenges = - [ Challenge 0 "x" "A lone free variable. What does x reduce to?" "x", - Challenge 1 "y" "Another free variable. What does y reduce to?" "y", - Challenge 2 "(lam (x) x)" "The identity function. What is its normal form?" "(lam (x) x)" + [ Challenge 0 "x" "A lone free variable. What does x reduce to?" + , Challenge 1 "y" "Another free variable. What does y reduce to?" + , Challenge 2 "(lam (x) x)" "The identity function. What is its normal form?" ] diff --git a/lambda-calcul/haskell/src/Minilang/App.hs b/lambda-calcul/haskell/src/Minilang/App.hs index 0174547..4340708 100644 --- a/lambda-calcul/haskell/src/Minilang/App.hs +++ b/lambda-calcul/haskell/src/Minilang/App.hs @@ -20,19 +20,19 @@ import Data.Text.Encoding (decodeUtf8, encodeUtf8) import Data.Time (getCurrentTime) import Minilang.API (Challenge (..), LambdaAPI, Score (..), Token (..), User (..), newToken) import Minilang.Lambda.Parser (pretty) -import Minilang.REPL (withInputs, replEnvWith) +import Minilang.REPL (replEnvWith, withInputs) import Minilang.REPL.Purer (PurerEnv (..)) -import Minilang.REPL.Types (Command (..), Content (..), Evaluator (..), In (..), Out (..), initialREPL) +import Minilang.REPL.Types (Command (..), Content (..), Evaluator (..), In (..), Out (..)) import Network.Wai.Application.Static (defaultFileServerSettings, staticApp) -import Servant (ServerT, err400, err500, errBody, (:<|>) (..), err404) +import Servant (ServerT, err400, err404, err500, errBody, (:<|>) (..)) import Servant.Server (Application, Handler (..), Tagged (..)) import System.Random (StdGen) data Env = Env - { gen :: TVar StdGen, - users :: TVar (Map Token Score), - challenges :: [Challenge], - evaluator :: Evaluator + { gen :: TVar StdGen + , users :: TVar (Map Token Score) + , challenges :: [Challenge] + , evaluator :: Evaluator } makeEnv :: StdGen -> [Challenge] -> Evaluator -> IO Env @@ -72,7 +72,7 @@ registerUser user@(User name) = do pure token unregisterUser :: (MonadReader Env m, MonadIO m) => Maybe Token -> m Score -unregisterUser Nothing = liftIO $ throwM $ err400 {errBody = "Missing token"} +unregisterUser Nothing = liftIO $ throwM $ err400{errBody = "Missing token"} unregisterUser (Just token) = do checkUserToken token score <- @@ -84,7 +84,7 @@ unregisterUser (Just token) = do writeTVar tvar updatedMap pure score case score of - Nothing -> liftIO $ throwM $ err400 {errBody = "User does not exist"} + Nothing -> liftIO $ throwM $ err400{errBody = "User does not exist"} Just s -> pure s checkDuplicateUser :: (MonadIO m, MonadReader Env m) => Text -> m () @@ -93,10 +93,10 @@ checkDuplicateUser name = usersMap <- readTVar user when (isUserRegistered name usersMap) $ throwM $ - err400 {errBody = "User already registered"} + err400{errBody = "User already registered"} isUserRegistered :: Text -> Map Token Score -> Bool -isUserRegistered name = Map.foldr (\Score {user = User {username}} acc -> username == name || acc) False +isUserRegistered name = Map.foldr (\Score{user = User{username}} acc -> username == name || acc) False generateToken :: (MonadReader Env m, MonadIO m) => m Token generateToken = @@ -116,11 +116,11 @@ getUser :: (MonadIO m, MonadReader Env m) => Maybe Token -> m Score getUser mToken = do usersMap <- asks users >>= liftIO . readTVarIO case mToken >>= (`Map.lookup` usersMap) of - Nothing -> liftIO $ throwM $ err404 {errBody = "User does not exist"} + Nothing -> liftIO $ throwM $ err404{errBody = "User does not exist"} Just score -> pure score getChallenge :: (MonadReader Env m, MonadIO m) => Maybe Token -> m Challenge -getChallenge Nothing = liftIO $ throwM $ err400 {errBody = "Missing token"} +getChallenge Nothing = liftIO $ throwM $ err400{errBody = "Missing token"} getChallenge (Just token) = do checkUserToken token getCurrentChallenge token @@ -129,7 +129,7 @@ checkUserToken :: (MonadReader Env m, MonadIO m) => Token -> m () checkUserToken token = do usersMap <- asks users >>= liftIO . readTVarIO case Map.lookup token usersMap of - Nothing -> liftIO $ throwM $ err400 {errBody = "Token " <> LBS.fromStrict (encodeUtf8 (unToken token)) <> " does not exist"} + Nothing -> liftIO $ throwM $ err400{errBody = "Token " <> LBS.fromStrict (encodeUtf8 (unToken token)) <> " does not exist"} Just _ -> pure () updateUserLastTest :: (MonadIO m, MonadReader Env m) => Token -> TestResult -> m () @@ -138,28 +138,28 @@ updateUserLastTest token result = do asks users >>= \user -> liftIO $ atomically $ do usersMap <- readTVar user case Map.lookup token usersMap of - Nothing -> throwM $ err400 {errBody = "Cannot update last test: Invalid token"} + Nothing -> throwM $ err400{errBody = "Cannot update last test: Invalid token"} Just score -> do - let updatedScore = score {lastTest = Just time, lastResult = Just (isSuccess result)} + let updatedScore = score{lastTest = Just time, lastResult = Just (isSuccess result)} updatedMap = Map.insert token updatedScore usersMap writeTVar user updatedMap postAnswer :: (MonadReader Env m, MonadIO m) => Maybe Token -> Text -> m () -postAnswer Nothing _ = liftIO $ throwM $ err400 {errBody = "Missing token"} -postAnswer (Just token) expected = do +postAnswer Nothing _ = liftIO $ throwM $ err400{errBody = "Missing token"} +postAnswer (Just token) answer = do checkUserToken token - Challenge {expr} <- getCurrentChallenge token + Challenge{level, expr} <- getCurrentChallenge token ev <- asks evaluator - let PurerEnv {outputs} = withInputs (replEnvWith ev) [Com (Load (Data expr))] - result = evaluateOutputs outputs expected + let PurerEnv{outputs} = withInputs (replEnvWith ev) [Com (Load (Data expr))] + result = evaluateAnswer level outputs answer updateUserLastTest token result case result of TestSucceeded -> upgradeUserChallenge token TestFailed msg -> - liftIO $ throwM $ err400 {errBody = "Test failed: " <> LBS.fromStrict (encodeUtf8 msg)} + liftIO $ throwM $ err400{errBody = "Test failed: " <> LBS.fromStrict (encodeUtf8 msg)} TestErrored msg -> - liftIO $ throwM $ err500 {errBody = "Error evaluating answer: " <> LBS.fromStrict (encodeUtf8 msg)} + liftIO $ throwM $ err500{errBody = "Error evaluating answer: " <> LBS.fromStrict (encodeUtf8 msg)} data TestResult = TestSucceeded | TestFailed Text | TestErrored Text @@ -167,17 +167,17 @@ isSuccess :: TestResult -> Bool isSuccess TestSucceeded = True isSuccess _ = False -evaluateOutputs :: [Out] -> Text -> TestResult -evaluateOutputs outputs expected = +evaluateAnswer :: Int -> [Out] -> Text -> TestResult +evaluateAnswer grade outputs answer = case outputs of [Bye, Evaluated ast _ _] -> - if pretty ast /= expected - then TestFailed "Incorrect result" + if pretty ast /= answer + then TestFailed $ "Incorrect result for question " <> pack (show grade) <> " got " <> answer <> ", try again" else TestSucceeded [Bye] -> - if expected == "" + if answer == "" then TestSucceeded - else TestFailed "Incorrect result" + else TestFailed $ "Incorrect result for question " <> pack (show grade) <> " got " <> answer <> ", try again" [Bye, Msg msg] -> TestFailed msg _ -> TestErrored $ pack $ show outputs @@ -186,20 +186,20 @@ upgradeUserChallenge token = do asks users >>= \user -> liftIO $ atomically $ do usersMap <- readTVar user case Map.lookup token usersMap of - Nothing -> throwM $ err400 {errBody = "Cannot update last test: Invalid token"} + Nothing -> throwM $ err400{errBody = "Cannot update last test: Invalid token"} Just score -> do - let updatedScore = score {grade = succ (grade score)} + let updatedScore = score{grade = succ (grade score)} updatedMap = Map.insert token updatedScore usersMap writeTVar user updatedMap getCurrentChallenge :: (MonadIO m, MonadReader Env m) => Token -> m Challenge getCurrentChallenge token = do - Env {users, challenges} <- ask + Env{users, challenges} <- ask liftIO $ atomically $ do usersMap <- readTVar users case Map.lookup token usersMap of - Nothing -> throwM $ err400 {errBody = "Cannot find challenge: Invalid token"} - Just Score {grade} -> + Nothing -> throwM $ err400{errBody = "Cannot find challenge: Invalid token"} + Just Score{grade} -> pure $ challenges !! grade -- | Serve static resources under `public/` directory diff --git a/lambda-calcul/haskell/src/Minilang/Lambda.hs b/lambda-calcul/haskell/src/Minilang/Lambda.hs index fbaf35d..82ab8bf 100644 --- a/lambda-calcul/haskell/src/Minilang/Lambda.hs +++ b/lambda-calcul/haskell/src/Minilang/Lambda.hs @@ -19,46 +19,46 @@ loadProgram :: Env -> Context -> [AST] -> - Either TypeError ([(Term, Type)], Env, Context) + Either TypeError ([(Term, Maybe Type)], Env, Context) loadProgram evaluator language env context exprs = fmap (\(res, e, c) -> (reverse res, e, c)) result - where - result = - foldl - ( \acc expr -> - case acc of - Left typeError -> Left typeError - Right (results, env', context') -> - case runExpr language expr env' context' of - Left typeError -> Left typeError - Right (Nothing, env'', context'') -> - Right (results, env'', context'') - Right (Just res, env'', context'') -> - Right (res : results, env'', context'') - ) - (Right ([], env, context)) - exprs - - runExpr language (Def ident body) env context = - let term = evalInEnvWith evaluator env body - in case language of - Typed -> - case infer term of + where + result = + foldl + ( \acc expr -> + case acc of + Left typeError -> Left typeError + Right (results, env', context') -> + case runExpr expr env' context' of Left typeError -> Left typeError - Right typ -> - Right (Nothing, (ident, term) : env, extendContext ident typ context) - Untyped -> - Right (Nothing, (ident, term) : env, context) - runExpr language expr env context = - let v = evalInEnvWith evaluator env expr - in case language of - Typed -> - case infer v of - Left typeError -> Left typeError - Right typ -> - Right (Just (v, typ), env, context) - Untyped -> - Right (Just (v, TyVar "<?>"), env, context) + Right (Nothing, env'', context'') -> + Right (results, env'', context'') + Right (Just res, env'', context'') -> + Right (res : results, env'', context'') + ) + (Right ([], env, context)) + exprs + + runExpr (Def ident body) env' context' = + let term = evalInEnvWith evaluator env' body + in case language of + Typed -> + case infer term of + Left typeError -> Left typeError + Right typ -> + Right (Nothing, (ident, term) : env', extendContext ident typ context') + Untyped -> + Right (Nothing, (ident, term) : env', context') + runExpr expr env' context' = + let v = evalInEnvWith evaluator env' expr + in case language of + Typed -> + case infer v of + Left typeError -> Left typeError + Right typ -> + Right (Just (v, Just typ), env', context') + Untyped -> + Right (Just (v, Nothing), env', context') -- | Evaluate an 'AST' in the given 'Env' using the De Bruijn CBV evaluator. -- This is the default evaluator used by the server and REPL. @@ -74,11 +74,11 @@ evalInEnvWith DeBruijn env expr = env' = (second toDeBruijn <$> env) ++ builtinDeBruijnEnv in fromDeBruijn $ eval' env' (toDeBruijn term) evalInEnvWith NbE env expr = - let term = desugar expr + let term = desugar expr -- Build an EnvValue from the user Env by evaluating each binding's -- Term in the accumulated value env (builtins always available at the -- bottom). foldl builds left-to-right so earlier bindings are visible -- when evaluating later ones. - envV = foldl addBinding builtinEnvValue env + envV = foldl addBinding builtinEnvValue env addBinding acc (name, t) = (name, Eval.eval acc t) : acc in Eval.readBack (Eval.eval envV term) diff --git a/lambda-calcul/haskell/src/Minilang/Lambda/Unify.hs b/lambda-calcul/haskell/src/Minilang/Lambda/Unify.hs index 96e9990..fa6f1dd 100644 --- a/lambda-calcul/haskell/src/Minilang/Lambda/Unify.hs +++ b/lambda-calcul/haskell/src/Minilang/Lambda/Unify.hs @@ -1,11 +1,12 @@ +{-# LANGUAGE DeriveAnyClass #-} -- 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.Aeson (FromJSON, ToJSON) import Data.Text (Text) import GHC.Generics (Generic) -import Data.Aeson (ToJSON, FromJSON) type Identifier = Text diff --git a/lambda-calcul/haskell/src/Minilang/REPL.hs b/lambda-calcul/haskell/src/Minilang/REPL.hs index 7da2042..35883b9 100644 --- a/lambda-calcul/haskell/src/Minilang/REPL.hs +++ b/lambda-calcul/haskell/src/Minilang/REPL.hs @@ -23,34 +23,35 @@ import Minilang.REPL.Pure import Minilang.REPL.Purer import Minilang.REPL.Run import Minilang.REPL.Types +import System.Console.Haskeline ( + defaultBehavior, + defaultSettings, + historyFile, + runInputTBehavior, + setComplete, + ) import System.Environment (lookupEnv) -import Text.Read (readMaybe) -import System.Console.Haskeline - ( defaultBehavior, - defaultSettings, - historyFile, - runInputTBehavior, - setComplete, - ) import System.IO (Handle, stderr) +import Text.Read (readMaybe) -- | Read the evaluator selection from the @MINILANG_EVAL@ environment variable. -- Returns 'DeBruijn' when the variable is absent or unrecognised. evaluatorFromEnv :: IO Evaluator evaluatorFromEnv = lookupEnv "MINILANG_EVAL" >>= \case - Nothing -> pure DeBruijn + Nothing -> pure DeBruijn Just raw -> case readMaybe raw of Just ev -> pure ev Nothing -> do Text.hPutStrLn stderr $ - "Warning: unknown MINILANG_EVAL value " <> Text.pack (show raw) - <> ", falling back to DeBruijn" + "Warning: unknown MINILANG_EVAL value " + <> Text.pack (show raw) + <> ", falling back to DeBruijn" pure DeBruijn -- | Build the initial 'REPLEnv' using the given 'Evaluator'. replEnvWith :: Evaluator -> REPLEnv -replEnvWith ev = initialREPL { evaluator = ev } +replEnvWith ev = initialREPL{evaluator = ev} -- * Haskeline REPL @@ -58,8 +59,8 @@ withTerminal :: Evaluator -> IO () withTerminal ev = runInputTBehavior defaultBehavior settings $ evalStateT (runHaskeline runREPL) (replEnvWith ev) - where - settings = setComplete completion $ defaultSettings {historyFile = Just "~/.minilang.history"} + where + settings = setComplete completion $ defaultSettings{historyFile = Just "~/.minilang.history"} -- * Other REPLs @@ -79,9 +80,9 @@ withIO ev hin hout = do Right prog -> case loadProgram ev Untyped newEnv newContext prog of Right (results, _, _) -> mapM_ (Text.hPutStrLn hout . render) results Left err -> Text.hPutStrLn hout (Text.pack $ show err) - where - render :: (Term, Type) -> Text - render (term, _typ) = pretty (resugar term) -- TODO: handle types <> " : " <> Unify.pretty typ + where + render :: (Term, Maybe Type) -> Text + render (term, typ) = pretty (resugar term) <> renderType typ -- * Pure REPL diff --git a/lambda-calcul/haskell/src/Minilang/REPL/Pure.hs b/lambda-calcul/haskell/src/Minilang/REPL/Pure.hs index 8250152..d9dbbbe 100644 --- a/lambda-calcul/haskell/src/Minilang/REPL/Pure.hs +++ b/lambda-calcul/haskell/src/Minilang/REPL/Pure.hs @@ -13,9 +13,9 @@ import qualified Minilang.Lambda.Unify as Type import Minilang.REPL.Types data PureEnv = PureEnv - { inputText :: [Text], - outputText :: [Text], - pureREPL :: REPLEnv + { inputText :: [Text] + , outputText :: [Text] + , pureREPL :: REPLEnv } newtype PureREPL a = PureREPL {runPure :: CatchT (State PureEnv) a} @@ -26,25 +26,30 @@ instance MonadREPL PureREPL where ins <- gets inputText case ins of [] -> pure EOF - (t : ts) -> modify (\e -> e {inputText = ts}) >> pure (interpret t) + (t : ts) -> modify (\e -> e{inputText = ts}) >> pure (interpret t) - output t = modify $ \e -> e {outputText = render t : outputText e} + output t = modify $ \e -> e{outputText = render t : outputText e} prompt = pure () getEnv = gets pureREPL - setEnv e' = modify $ \e -> e {pureREPL = e'} + setEnv e' = modify $ \e -> e{pureREPL = e'} load f = pure $ Left $ REPLError $ "cannot load file " <> f <> " in Pure interpreter" render :: Out -> Text render = \case Msg t -> t - Evaluated ast _term typ -> pretty ast <> " : " <> Type.pretty typ - Defined ident typ -> ident <> " : " <> Type.pretty typ + Evaluated ast _term typ -> pretty ast <> renderType typ + Defined ident typ -> ident <> renderType typ Bye -> "Bye!" other -> pack (show other) +renderType :: Maybe Type.Type -> Text +renderType typ = case typ of + Nothing -> "" + Just t -> " : " <> Type.pretty t + instance MonadThrow PureREPL where throwM = throw diff --git a/lambda-calcul/haskell/src/Minilang/REPL/Run.hs b/lambda-calcul/haskell/src/Minilang/REPL/Run.hs index 26f3cad..ba09007 100644 --- a/lambda-calcul/haskell/src/Minilang/REPL/Run.hs +++ b/lambda-calcul/haskell/src/Minilang/REPL/Run.hs @@ -8,7 +8,7 @@ module Minilang.REPL.Run where import Control.Monad.Catch import Data.Text hiding (replicate) -import Minilang.Lambda (loadProgram, evalInEnvWith) +import Minilang.Lambda (evalInEnvWith, loadProgram) import Minilang.Lambda.Eval (newEnv) import Minilang.Lambda.Infer (extendContext, infer, newContext) import qualified Minilang.Lambda.Infer as Infer @@ -20,21 +20,21 @@ import Minilang.REPL.Types runREPL :: (MonadCatch m, MonadREPL m) => m () runREPL = go - where - go = do - prompt - raw <- input - case raw of - EOF -> output Bye - In txt -> handleUserInput txt >> go - Com cmd -> handleCommand cmd >> go + where + go = do + prompt + raw <- input + case raw of + EOF -> output Bye + In txt -> handleUserInput txt >> go + Com cmd -> handleCommand cmd >> go handleUserInput :: (MonadCatch m, MonadREPL m) => Text -> m () handleUserInput txt = do - repl@REPLEnv {language, evaluator, env, context} <- getEnv + repl@REPLEnv{language, evaluator, env, context} <- getEnv case parse txt of Left err -> output (Msg $ pack $ show err) Right (Def ident body) -> do @@ -46,13 +46,13 @@ handleUserInput txt = do Right typ -> do setEnv $ repl - { env = (ident, v) : env, - context = extendContext ident typ context + { env = (ident, v) : env + , context = extendContext ident typ context } - output (Defined ident typ) + output (Defined ident (Just typ)) Untyped -> do - setEnv $ repl {env = (ident, v) : env} - output (Defined ident (TyVar "<?>")) + setEnv $ repl{env = (ident, v) : env} + output (Defined ident Nothing) Right expr -> do let v = evalInEnvWith evaluator env expr ast = resugar v @@ -62,17 +62,17 @@ handleUserInput txt = do Left typeError -> output (Msg $ Infer.render typeError) Right typ -> do let - output (Evaluated ast v typ) + output (Evaluated ast v (Just typ)) Untyped -> - output (Evaluated ast v (TyVar "<?>")) + output (Evaluated ast v Nothing) 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 {..} -> + getEnv >>= \REPLEnv{..} -> output (CurrentEnv env context language) handleCommand (Load (File file)) = do t <- load file @@ -80,15 +80,15 @@ handleCommand (Load (File file)) = do 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 (Set (SelectLanguage lang)) = getEnv >>= \e -> - setEnv (e {language = lang}) + setEnv (e{language = lang}) >> output (Msg $ "Language set to " <> pack (show lang)) handleCommand (Set (SelectEvaluator ev)) = getEnv >>= \e -> - setEnv (e {evaluator = ev}) + setEnv (e{evaluator = ev}) >> output (Msg $ "Evaluator set to " <> pack (show ev)) handleCommand Help = output (Msg helpText) @@ -98,12 +98,12 @@ loadProgramInEnv :: Text -> m () loadProgramInEnv prog = do - repl@REPLEnv {env, context, language, evaluator} <- getEnv + repl@REPLEnv{env, context, language, evaluator} <- getEnv case parseProgram prog of Left err -> output (Msg $ pack $ show err) Right exprs -> do case loadProgram evaluator language env context exprs of Left typeError -> output (Msg $ pack $ show typeError) Right (results, env', context') -> do - setEnv (repl {env = env', context = context'}) + setEnv (repl{env = env', context = context'}) mapM_ (\(term, typ) -> output (Evaluated (resugar term) term typ)) results diff --git a/lambda-calcul/haskell/src/Minilang/REPL/Types.hs b/lambda-calcul/haskell/src/Minilang/REPL/Types.hs index 0b0472e..3bcbbb1 100644 --- a/lambda-calcul/haskell/src/Minilang/REPL/Types.hs +++ b/lambda-calcul/haskell/src/Minilang/REPL/Types.hs @@ -7,13 +7,13 @@ import Control.Exception (Exception) import Data.Aeson (FromJSON, ToJSON) import Data.Text as Text hiding (replicate) import GHC.Generics -import Minilang.Lambda.Eval (Term, Env, newEnv) +import Minilang.Lambda.Eval (Env, Term, newEnv) import Minilang.Lambda.Infer (Context, newContext) import Minilang.Lambda.Parser (AST) import Minilang.Lambda.Unify (Type) import Text.Read (readMaybe) -class (Monad m) => MonadREPL m where +class Monad m => MonadREPL m where -- | Returns the current environment for this session -- Environment is made of an `Env`ironment binding names to `Decl`arations -- and typing `Context` binding names to `Value`s denoting evaluated types. @@ -44,13 +44,13 @@ instance Exception REPLError -- | REPL state data REPLEnv = REPLEnv - { env :: Env, - context :: Context, - curIndent :: Int, - stepTypeCheck :: Bool, - debugParser :: Bool, - language :: Language, - evaluator :: Evaluator + { env :: Env + , context :: Context + , curIndent :: Int + , stepTypeCheck :: Bool + , debugParser :: Bool + , language :: Language + , evaluator :: Evaluator } initialREPL :: REPLEnv @@ -77,8 +77,8 @@ data Content deriving (Eq, Show, Generic, ToJSON, FromJSON) data Out - = Defined Text Type - | Evaluated AST Term Type + = Defined Text (Maybe Type) + | Evaluated AST Term (Maybe Type) | CurrentEnv Env Context Language | Msg Text | Bye @@ -128,27 +128,27 @@ interpret (unpack -> (':' : 'l' : 'a' : 'n' : 'g' : ' ' : lang)) = interpret (unpack -> (':' : 'e' : 'v' : 'a' : 'l' : ' ' : ev)) = case readMaybe ev of Nothing -> Com Help - Just e -> Com $ Set $ SelectEvaluator e + Just e -> Com $ Set $ SelectEvaluator e interpret t = In t helpText :: Text helpText = Text.unlines - [ "REPL Commands Help:", - " :h(elp) : Display this help", - " :q(uit) : Exit the interpreter", - " :e(nv) : Displays the current interpreter's environment", - " This dumps both the Environment, where values are defined,", - " and the typing Context, where types are defined. ", - " :c(lear) : Clear the current interpreter's environment", - " :set <option> : Set an option modifying the interpreter's behaviour", - " :unset <option> : Remove an option that's been set previously", - " :l(oad) <file> : load content of <file> into the interpreter, parsing and type-checking it", - " :lang <Language> : Switch type-checking language (Untyped | Typed)", - " :eval <Evaluator>: Switch reduction strategy (DeBruijn | NbE)", - "", - "Options: ", - " step : Run the typechecker step-by-step, pausing at each rule application and", - " waiting for user to hit <enter> key to continue", - " debug : Debug parser, displaying the trail of rules tried and triggered" + [ "REPL Commands Help:" + , " :h(elp) : Display this help" + , " :q(uit) : Exit the interpreter" + , " :e(nv) : Displays the current interpreter's environment" + , " This dumps both the Environment, where values are defined," + , " and the typing Context, where types are defined. " + , " :c(lear) : Clear the current interpreter's environment" + , " :set <option> : Set an option modifying the interpreter's behaviour" + , " :unset <option> : Remove an option that's been set previously" + , " :l(oad) <file> : load content of <file> into the interpreter, parsing and type-checking it" + , " :lang <Language> : Switch type-checking language (Untyped | Typed)" + , " :eval <Evaluator>: Switch reduction strategy (DeBruijn | NbE)" + , "" + , "Options: " + , " step : Run the typechecker step-by-step, pausing at each rule application and" + , " waiting for user to hit <enter> key to continue" + , " debug : Debug parser, displaying the trail of rules tried and triggered" ] diff --git a/lambda-calcul/haskell/test/Minilang/IntegrationSpec.hs b/lambda-calcul/haskell/test/Minilang/IntegrationSpec.hs index ef05e20..d0265ac 100644 --- a/lambda-calcul/haskell/test/Minilang/IntegrationSpec.hs +++ b/lambda-calcul/haskell/test/Minilang/IntegrationSpec.hs @@ -6,8 +6,12 @@ import Control.Exception (bracket) import Data.Aeson (eitherDecodeFileStrict) import Data.Proxy (Proxy (..)) import Data.Text (Text) +import qualified Data.Text as Text import Minilang.API -import Minilang.REPL.Types (Evaluator (..)) +import Minilang.Lambda.Parser (pretty) +import Minilang.REPL (withInput, withInputs) +import Minilang.REPL.Purer (PurerEnv (..)) +import Minilang.REPL.Types (Command (Load), Content (..), Evaluator (..), In (Com), Out (..), initialREPL) import Minilang.Server (Server (..), startServer, stopServer) import Network.HTTP.Client (defaultManagerSettings, newManager) import Servant.API ((:<|>) (..)) @@ -89,12 +93,19 @@ spec = -- | Fetch the current challenge for the token, post the known answer, and -- assert the server accepted it (200 OK / no exception). solveChallenge :: ClientEnv -> Token -> Challenge -> IO () -solveChallenge env token Challenge{level, answer} = do +solveChallenge env token Challenge{level, expr} = do -- Confirm the server gives us the challenge we expect at this grade Challenge{level = serverLevel} <- runC env $ challengeClient (Just token) serverLevel `shouldBe` level -- Post the correct answer - runC env $ answerClient (Just token) answer + let PurerEnv{outputs} = withInputs initialREPL [Com (Load (Data expr))] + case outputs of + -- NOTE: Outputs are in reverse order, so the first output is the last one produced by the REPL. + (Bye : Evaluated ast _ _ : _) -> do + runC env $ answerClient (Just token) (pretty ast) + [Bye] -> + runC env $ answerClient (Just token) "" + answer -> fail $ "Unexpected answer format: " <> show answer -- --------------------------------------------------------------------------- -- Server lifecycle diff --git a/lambda-calcul/haskell/test/Minilang/Lambda/ParserSpec.hs b/lambda-calcul/haskell/test/Minilang/Lambda/ParserSpec.hs index 40866bb..0050973 100644 --- a/lambda-calcul/haskell/test/Minilang/Lambda/ParserSpec.hs +++ b/lambda-calcul/haskell/test/Minilang/Lambda/ParserSpec.hs @@ -8,10 +8,9 @@ import Data.Either (isLeft, isRight) import Data.Function ((&)) import Data.Text (Text, pack) import qualified Data.Text as Text -import Minilang.Lambda.Eval (Term (Lam)) +import Minilang.Lambda.Eval (Term (Lam), normalise) import qualified Minilang.Lambda.Eval as Eval -import Minilang.Lambda.Parser (AST (..), desugar, initialChars, parse, parseProgram, pretty, restChars, escapeString) -import Minilang.Lambda.Eval (normalise) +import Minilang.Lambda.Parser (AST (..), desugar, escapeString, initialChars, parse, parseProgram, pretty, restChars) import Test.Hspec (Spec, describe, it, parallel, shouldBe, shouldSatisfy) import Test.Hspec.QuickCheck (prop) import Test.QuickCheck ( @@ -91,13 +90,13 @@ spec = parallel $ do <> Text.concat ( map ( \(Identifier v, t) -> - "(" <> v <> " " <> pretty t <> ")" + "(" <> v <> " " <> pretty t <> ")\n" ) bound ) - <> ") " + <> ")\n " <> pretty body - <> ")" + <> ")\n" ) `shouldSatisfy` isRight @@ -370,8 +369,8 @@ genAst depth = -- logic is tested separately. genStrLit :: Gen AST genStrLit = StrLit . pack <$> listOf (elements safeChars) - where - safeChars = filter (\c -> c /= '"' && c /= '\\') [' '..'~'] + where + safeChars = filter (\c -> c /= '"' && c /= '\\') [' ' .. '~'] genDef :: Int -> Gen AST genDef n = Def . unIdent <$> arbitrary <*> genAst n diff --git a/lambda-calcul/haskell/test/Minilang/REPL/NetSpec.hs b/lambda-calcul/haskell/test/Minilang/REPL/NetSpec.hs index 6a2b1ab..2f8880a 100644 --- a/lambda-calcul/haskell/test/Minilang/REPL/NetSpec.hs +++ b/lambda-calcul/haskell/test/Minilang/REPL/NetSpec.hs @@ -1,6 +1,5 @@ module Minilang.REPL.NetSpec where --- import Control.Concurrent (threadDelay) import Control.Concurrent.Async import Control.Concurrent.STM.TVar import Control.Exception (bracket) @@ -46,48 +45,48 @@ withServer = runTestClient :: Int -> String -> [In] -> IO [Either String Out] runTestClient port envId inputs = runClient "127.0.0.1" port ("/repl/" <> envId) client - where - client cnx = do - outs <- forM inputs $ \inp -> do - WS.sendBinaryData cnx (encode inp) - eitherDecode <$> WS.receiveData cnx - WS.sendBinaryData cnx (encode EOF) - WS.sendClose cnx (encode ("" :: String)) - pure outs + where + client cnx = do + outs <- forM inputs $ \inp -> do + WS.sendBinaryData cnx (encode inp) + eitherDecode <$> WS.receiveData cnx + WS.sendBinaryData cnx (encode EOF) + WS.sendClose cnx (encode ("" :: String)) + pure outs temporaryFile :: (FilePath -> IO c) -> IO c temporaryFile = bracket newTempFile removeFile - where - newTempFile = do - dir <- getTemporaryDirectory - (f, h) <- mkstemp (dir </> "repl.test") - hClose h - pure f + where + newTempFile = do + dir <- getTemporaryDirectory + (f, h) <- mkstemp (dir </> "repl.test") + hClose h + pure f spec :: Spec spec = around withServer $ describe "MiniLang Network REPL" $ do - it "evaluates expression and returns evaluation result" $ \Server {serverPort} -> do + it "evaluates expression and returns evaluation result" $ \Server{serverPort} -> do let inp = [Com (Set (SelectLanguage Typed)), In "((lam (x) x) y)"] expectedOutput = - [ Right (Msg "Language set to Typed"), - Right $ Evaluated (AST.Sym "y") (Var "y") (TyVar "a") + [ Right (Msg "Language set to Typed") + , Right $ Evaluated (AST.Sym "y") (Var "y") (Just $ TyVar "a") ] res <- runTestClient serverPort ".newenv1" inp res `shouldBe` expectedOutput - it "allows retrieving empty initial env" $ \Server {serverPort} -> do + it "allows retrieving empty initial env" $ \Server{serverPort} -> do let inp = [Com (Set (SelectLanguage Typed)), Com DumpEnv] expectedOutput = - [ Right (Msg "Language set to Typed"), - Right $ CurrentEnv newEnv newContext Typed + [ Right (Msg "Language set to Typed") + , Right $ CurrentEnv newEnv newContext Typed ] res <- runTestClient serverPort ".newenv2" inp res `shouldBe` expectedOutput - it "can reconnect to existing environment" $ \Server {serverPort} -> do + it "can reconnect to existing environment" $ \Server{serverPort} -> do let inp = [In "Unit : U = Sum(tt)"] _ <- runTestClient serverPort ".newenv3" inp res <- runTestClient serverPort ".newenv3" [In "Unit"] @@ -95,5 +94,5 @@ spec = around withServer $ res `shouldSatisfy` isEvaluated isEvaluated :: [Either a Out] -> Bool -isEvaluated [Right (Evaluated _ _ _)] = True +isEvaluated [Right Evaluated{}] = True isEvaluated _ = False diff --git a/lambda-calcul/haskell/test/Minilang/REPLSpec.hs b/lambda-calcul/haskell/test/Minilang/REPLSpec.hs index e382df4..1754cdb 100644 --- a/lambda-calcul/haskell/test/Minilang/REPLSpec.hs +++ b/lambda-calcul/haskell/test/Minilang/REPLSpec.hs @@ -1,11 +1,9 @@ module Minilang.REPLSpec where import Control.Exception (bracket) -import Data.Either (isRight) import Data.Text.IO import Minilang.Lambda.Eval (Term (Lam, Var)) import Minilang.Lambda.Parser (AST (..)) -import Minilang.Lambda.Unify (Type (TyVar)) import Minilang.REPL import Minilang.REPL.Purer (PurerEnv (..)) import Minilang.REPL.Run (loadProgramInEnv) @@ -26,8 +24,8 @@ spec = parallel $ ["((lam (x) x) y)"] out - `shouldBe` [ "Bye!", - "y : <?>" + `shouldBe` [ "Bye!" + , "y" ] it "evaluates untyped MiniLang terms with definitions" $ do @@ -36,24 +34,24 @@ spec = parallel $ ["(def id (lam (x) x))", "(id y)"] out - `shouldBe` [ "Bye!", - "y : <?>", - "id : <?>" + `shouldBe` [ "Bye!" + , "y" + , "id" ] it "evaluates typed MiniLang terms with definitions" $ do let out = withInput - [ ":lang Typed", - "(def id (lam (x) x))", - "(id y)" + [ ":lang Typed" + , "(def id (lam (x) x))" + , "(id y)" ] out - `shouldBe` [ "Bye!", - "y : a", - "id : a -> a", - "Language set to Typed" + `shouldBe` [ "Bye!" + , "y : a" + , "id : a -> a" + , "Language set to Typed" ] it "defaults untyped terms" $ do @@ -65,58 +63,58 @@ spec = parallel $ ] out - `shouldBe` [ "Bye!", - "(lam (z s) (s (lam (z s) (s (lam (z s) z))))) : <?>" + `shouldBe` [ "Bye!" + , "(lam (z s) (s (lam (z s) (s (lam (z s) z)))))" ] it "do typecheck term when language is set to 'Typed'" $ do let out = withInput - [ ":lang Typed", - "(let ((Succ (lam (n z s) (s n))) \ + [ ":lang Typed" + , "(let ((Succ (lam (n z s) (s n))) \ \ (Zero (lam (z s) z))) \ \ (Succ (Succ Zero)))" ] out - `shouldBe` [ "Bye!", - "(lam (z s) (s (lam (z s) (s (lam (z s) z))))) : a -> ((c -> ((e -> f -> e) -> g) -> g) -> h) -> h", - "Language set to Typed" + `shouldBe` [ "Bye!" + , "(lam (z s) (s (lam (z s) (s (lam (z s) z))))) : a -> ((c -> ((e -> f -> e) -> g) -> g) -> h) -> h" + , "Language set to Typed" ] it "shows error when trying to load a non-existent file" $ do withInput [":load foo"] - `shouldBe` [ "Bye!", - "REPLError \"cannot load file foo in Pure interpreter\"" + `shouldBe` [ "Bye!" + , "REPLError \"cannot load file foo in Pure interpreter\"" ] it "can load 'bool-prog.lisp'" $ do boolProg <- readFile "bool-prog.lisp" - let PurerEnv {outputs} = runProgram (loadProgramInEnv boolProg) + let PurerEnv{outputs} = runProgram (loadProgramInEnv boolProg) outputs - `shouldBe` [ Evaluated (Abs ["f", "t"] (Sym "t")) (Lam "f" (Lam "t" (Var "t"))) (TyVar "<?>"), - Evaluated (Abs ["f", "t"] (Sym "f")) (Lam "f" (Lam "t" (Var "f"))) (TyVar "<?>"), - Evaluated (Abs ["f", "t"] (Sym "f")) (Lam "f" (Lam "t" (Var "f"))) (TyVar "<?>") + `shouldBe` [ Evaluated (Abs ["f", "t"] (Sym "t")) (Lam "f" (Lam "t" (Var "t"))) Nothing + , Evaluated (Abs ["f", "t"] (Sym "f")) (Lam "f" (Lam "t" (Var "f"))) Nothing + , Evaluated (Abs ["f", "t"] (Sym "f")) (Lam "f" (Lam "t" (Var "f"))) Nothing ] it "can load 'bool.lisp'" $ do boolProg <- readFile "bool.lisp" - let PurerEnv {outputs} = runProgram (loadProgramInEnv boolProg) + let PurerEnv{outputs} = runProgram (loadProgramInEnv boolProg) outputs `shouldBe` [ Evaluated (Abs ["f", "t"] (Sym "f")) (Lam "f" (Lam "t" (Var "f"))) - (TyVar "<?>") + Nothing ] it "can load 'fac.lisp'" $ do boolProg <- readFile "fac.lisp" - let PurerEnv {outputs} = runProgram (loadProgramInEnv boolProg) + let PurerEnv{outputs} = runProgram (loadProgramInEnv boolProg) outputs `shouldBe` [ Evaluated (Abs ["f", "t"] (Sym "t")) (Lam "f" (Lam "t" (Var "t"))) - (TyVar "<?>") + Nothing ] around withTempFile $ @@ -136,11 +134,11 @@ spec = parallel $ out <- readFile outputFileName out - `shouldBe` "\955\928> (lam (z s) (s (lam (z s) z))) : <?>\n\955\928> Bye!\n" + `shouldBe` "\955\928> (lam (z s) (s (lam (z s) z)))\n\955\928> Bye!\n" withTempFile :: (String -> IO ()) -> IO () withTempFile = bracket mkTempFile rmTempFile - where - mkTempFile = getTemporaryDirectory >>= \dir -> mkstemp (dir </> "test-repl") >>= \(fp, h) -> hClose h >> pure fp - rmTempFile fn = removeFile fn >> removeFile (fn <.> "out") + where + mkTempFile = getTemporaryDirectory >>= \dir -> mkstemp (dir </> "test-repl") >>= \(fp, h) -> hClose h >> pure fp + rmTempFile fn = removeFile fn >> removeFile (fn <.> "out") diff --git a/lambda-calcul/haskell/test/Minilang/ServerSpec.hs b/lambda-calcul/haskell/test/Minilang/ServerSpec.hs index 2860c40..8d0b182 100644 --- a/lambda-calcul/haskell/test/Minilang/ServerSpec.hs +++ b/lambda-calcul/haskell/test/Minilang/ServerSpec.hs @@ -51,7 +51,7 @@ spec = with (app testSeed) $ do it "GET /api/leaderboard returns empty list of scores at start" $ do get "/api/leaderboard" - `shouldRespondWith` 200 {matchBody = arrayOfLengthOf (Proxy @Score) 0} + `shouldRespondWith` 200{matchBody = arrayOfLengthOf (Proxy @Score) 0} it "POST /api/register returns registration token given user is not registered" $ do postJSON "/api/register" alice @@ -66,7 +66,7 @@ spec = with (app testSeed) $ do it "GET /api/leaderboard returns list of one element after user registers" $ do void $ postJSON "/api/register" alice get "/api/leaderboard" - `shouldRespondWith` 200 {matchBody = arrayOfLengthOf (Proxy @Score) 1} + `shouldRespondWith` 200{matchBody = arrayOfLengthOf (Proxy @Score) 1} it "POST /api/register returns 400 given user is already registered" $ do void $ postJSON "/api/register" alice @@ -84,7 +84,7 @@ spec = with (app testSeed) $ do `shouldRespondWith` 404 it "GET /api/challenge returns next challenge given user is registered" $ do - let expected = LT.unpack $ decodeUtf8 $ encode $ Challenge {level = 0, expr = "x", description = "A lone free variable. What does x reduce to?", answer = "x"} + let expected = LT.unpack $ decodeUtf8 $ encode $ Challenge{level = 0, expr = "x", description = "A lone free variable. What does x reduce to?"} postJSON "/api/register" alice `shouldRespondWith` 201 @@ -123,7 +123,7 @@ spec = with (app testSeed) $ do `shouldRespondWith` 400 it "GET /api/challenge returns next level challenge after successful POST" $ do - let expected = LT.unpack $ decodeUtf8 $ encode $ Challenge {level = 1, expr = "y", description = "Another free variable. What does y reduce to?", answer = "y"} + let expected = LT.unpack $ decodeUtf8 $ encode $ Challenge{level = 1, expr = "y", description = "Another free variable. What does y reduce to?"} void $ postJSON "/api/register" alice void $ postJSON ("/api/challenge?token=" <> LBS.toStrict token) "\"x\"" @@ -147,7 +147,7 @@ spec = with (app testSeed) $ do { matchBody = MatchBody $ \_ actual -> case eitherDecode actual of Right (score :: Score) -> - if score == Score {user = User "alice", grade = 0, lastTest = Nothing, lastResult = Nothing} + if score == Score{user = User "alice", grade = 0, lastTest = Nothing, lastResult = Nothing} then Nothing else Just $ "Expected score with grade 0, but got " ++ show score Left err -> Just $ "Failed to decode JSON: " ++ err @@ -190,7 +190,7 @@ spec = with (app testSeed) $ do postJSON :: BS.ByteString -> ByteString -> WaiSession () SResponse postJSON url = request "POST" url [("Content-Type", "application/json")] -arrayOfLengthOf :: forall elem proxy. (FromJSON elem) => proxy elem -> Int -> MatchBody +arrayOfLengthOf :: forall elem proxy. FromJSON elem => proxy elem -> Int -> MatchBody arrayOfLengthOf _ len = MatchBody $ \_ actual -> case eitherDecode actual of Right (scores :: [elem]) -> |