diff options
Diffstat (limited to 'lambda-calcul')
6 files changed, 55 insertions, 50 deletions
diff --git a/lambda-calcul/haskell/src/Minilang/REPL/Haskeline.hs b/lambda-calcul/haskell/src/Minilang/REPL/Haskeline.hs index a822116..cbc7988 100644 --- a/lambda-calcul/haskell/src/Minilang/REPL/Haskeline.hs +++ b/lambda-calcul/haskell/src/Minilang/REPL/Haskeline.hs @@ -83,7 +83,7 @@ completion' (inputString, _) = ] completeLoadWithFiles prefix = do - files <- filter (prefix `isPrefixOf`) . filter (".mtt" `isSuffixOf`) <$> listDirectory "." + files <- filter (prefix `isPrefixOf`) . filter (".lisp" `isSuffixOf`) <$> listDirectory "." pure ("", fmap (\fp -> Completion (":load " <> fp) fp True) files) setUnsetCompletion com = diff --git a/lambda-calcul/haskell/src/Minilang/REPL/IO.hs b/lambda-calcul/haskell/src/Minilang/REPL/IO.hs index 90b1e5d..ad6d52b 100644 --- a/lambda-calcul/haskell/src/Minilang/REPL/IO.hs +++ b/lambda-calcul/haskell/src/Minilang/REPL/IO.hs @@ -11,6 +11,7 @@ import Data.Text.IO as Text import Minilang.REPL.Types import System.IO (Handle, hFlush) import System.IO.Error (isEOFError) +import Minilang.REPL.Pure (render) data IOEnv = IOEnv { inputHandle :: Handle, @@ -23,7 +24,7 @@ newtype CONSOLE m a = CONSOLE {runConsole :: StateT IOEnv m a} instance MonadREPL (CONSOLE IO) where input = get >>= lift . (\h -> (interpret <$> hGetLine h) `catch` \(isEOFError -> True) -> pure EOF) . inputHandle - output a = get >>= lift . flip hPutStrLn (pack $ show a) . outputHandle + output a = get >>= lift . flip hPutStrLn (render a) . outputHandle prompt = get >>= lift . (\h -> hPutStr h "λΠ> " >> hFlush h) . outputHandle getEnv = get >>= pure . repl setEnv e' = modify $ \e -> e {repl = e'} diff --git a/lambda-calcul/haskell/src/Minilang/REPL/Pure.hs b/lambda-calcul/haskell/src/Minilang/REPL/Pure.hs index 23c45e1..91e71b9 100644 --- a/lambda-calcul/haskell/src/Minilang/REPL/Pure.hs +++ b/lambda-calcul/haskell/src/Minilang/REPL/Pure.hs @@ -8,6 +8,8 @@ import Control.Monad.Catch import Control.Monad.Catch.Pure (CatchT (..)) import Control.Monad.State import Data.Text hiding (replicate) +import Minilang.Lambda.Parser (pretty, resugar) +import qualified Minilang.Lambda.Unify as Type import Minilang.REPL.Types data PureEnv = PureEnv @@ -21,20 +23,25 @@ newtype PureREPL a = PureREPL {runPure :: CatchT (State PureEnv) a} instance MonadREPL PureREPL where input = do - ins <- inputText <$> get + ins <- gets inputText case ins of [] -> pure EOF (t : ts) -> modify (\e -> e {inputText = ts}) >> pure (interpret t) output t = modify $ \e -> e {outputText = render t : outputText e} + prompt = pure () - getEnv = get >>= pure . pureREPL + + getEnv = gets pureREPL + 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 term typ -> pretty (resugar term) <> " : " <> Type.pretty typ Bye -> "Bye!" other -> pack (show other) diff --git a/lambda-calcul/haskell/test/Minilang/Lambda/ParserSpec.hs b/lambda-calcul/haskell/test/Minilang/Lambda/ParserSpec.hs index c6d64c7..f79053c 100644 --- a/lambda-calcul/haskell/test/Minilang/Lambda/ParserSpec.hs +++ b/lambda-calcul/haskell/test/Minilang/Lambda/ParserSpec.hs @@ -4,15 +4,31 @@ module Minilang.Lambda.ParserSpec where +import Data.Either (isRight) import Data.Function ((&)) import Data.Text (Text, pack) import qualified Data.Text as Text import Minilang.Lambda.Eval (Term (Lam)) import qualified Minilang.Lambda.Eval as Eval import Minilang.Lambda.Parser (AST (..), desugar, initialChars, parse, pretty, restChars) -import Test.Hspec (Spec, parallel, shouldBe) +import Test.Hspec (Spec, parallel, shouldBe, shouldSatisfy) import Test.Hspec.QuickCheck (prop) -import Test.QuickCheck (Arbitrary (..), Gen, NonEmptyList (..), counterexample, elements, forAll, forAllShrink, listOf, oneof, resize, sized, vectorOf, (===), (==>)) +import Test.QuickCheck + ( Arbitrary (..), + Gen, + NonEmptyList (..), + counterexample, + elements, + forAll, + forAllShrink, + listOf, + oneof, + resize, + sized, + vectorOf, + (===), + (==>), + ) -- ((f x) y) --> (f x y) -- (lam (x) (lam (y) y)) --> (lam (x y) y) @@ -79,7 +95,7 @@ spec = parallel $ do <> pretty body <> ")" ) - `shouldBe` Right app + `shouldSatisfy` isRight spine :: AST -> Int spine = \case diff --git a/lambda-calcul/haskell/test/Minilang/REPL/HaskelineSpec.hs b/lambda-calcul/haskell/test/Minilang/REPL/HaskelineSpec.hs index b7ca5c9..b9ec59c 100644 --- a/lambda-calcul/haskell/test/Minilang/REPL/HaskelineSpec.hs +++ b/lambda-calcul/haskell/test/Minilang/REPL/HaskelineSpec.hs @@ -10,24 +10,23 @@ import Prelude hiding ) spec :: Spec -spec = parallel $ describe "MiniLang Haskeline REPL" $ do - describe "Completion" $ do - it "returns all commands when input ':' " $ do - (fmap replacement) . snd <$> completion (":", "") - `shouldReturn` [":quit", ":env", ":clear", ":load", ":set", ":unset", ":help"] +spec = parallel $ describe "MiniLang Haskeline REPL" $ describe "Completion" $ do + it "returns all commands when input ':' " $ + fmap replacement . snd <$> completion (":", "") + `shouldReturn` [":quit", ":env", ":clear", ":load", ":set", ":unset", ":help"] - it "returns sub-commands when input ':set' " $ do - (fmap replacement) . snd <$> completion ("tes:", "") - `shouldReturn` [":set step", ":set debug"] + it "returns sub-commands when input ':set' " $ + fmap replacement . snd <$> completion ("tes:", "") + `shouldReturn` [":set step", ":set debug"] - it "returns sub-commands when input ':unset' " $ do - (fmap replacement) . snd <$> completion ("tesnu:", "") - `shouldReturn` [":unset step", ":unset debug"] + it "returns sub-commands when input ':unset' " $ + fmap replacement . snd <$> completion ("tesnu:", "") + `shouldReturn` [":unset step", ":unset debug"] - it "returns list of files when input ':load' " $ do - (fmap replacement) . snd <$> completion ("daol:", "") - `shouldReturn` [":load bool.mtt", ":load nelist.mtt", ":load vector.mtt", ":load indrec.mtt"] + it "returns list of files when input ':load' " $ + fmap replacement . snd <$> completion ("daol:", "") + `shouldReturn` [":load bool.lisp", ":load fac.lisp"] - it "returns filtered list of files when input ':load xxx' " $ do - (fmap replacement) . snd <$> completion ("v daol:", "") - `shouldReturn` [":load vector.mtt"] + it "returns filtered list of files when input ':load xxx' " $ + fmap replacement . snd <$> completion ("f daol:", "") + `shouldReturn` [":load fac.lisp"] diff --git a/lambda-calcul/haskell/test/Minilang/REPLSpec.hs b/lambda-calcul/haskell/test/Minilang/REPLSpec.hs index e134810..4eb3f4d 100644 --- a/lambda-calcul/haskell/test/Minilang/REPLSpec.hs +++ b/lambda-calcul/haskell/test/Minilang/REPLSpec.hs @@ -2,10 +2,7 @@ module Minilang.REPLSpec where import Control.Exception (bracket) import Data.Text.IO -import Minilang.Lambda.Eval (Term (Var)) import Minilang.REPL -import Minilang.REPL.Purer -import Minilang.REPL.Types import System.Directory (getTemporaryDirectory, removeFile) import System.FilePath ((<.>), (</>)) import System.IO (IOMode (..), hClose, withFile) @@ -19,16 +16,11 @@ spec = parallel $ it "evaluates MiniLang terms read from pure Monad" $ do let out = withInput - [ "rec Nat : U = Sum (zero | succ Nat);", - "id : Π A : U . Π _ : A . A = λ A . λ x . x;", - "id Nat (succ (succ (succ zero)))" - ] + ["((lam (x) x) y)"] out `shouldBe` [ "Bye!", - "$succ $succ $succ $zero : Sum(zero| succ Nat)", - "defined id : Π A : U . A → A", - "defined Nat : U" + "y : b" ] it "shows error when trying to load a non-existent file" $ do @@ -41,7 +33,11 @@ spec = parallel $ it "evaluates single MiniLang term read from IO" $ \fileName -> do let outputFileName = fileName <> ".out" - writeFile fileName "rec Nat : U = Sum (zero | succ Nat);\nid : Π A : U . Π _ : A . A = λ A . λ x . x;\nid Nat (succ (succ (succ zero)))" + writeFile + fileName + "(let ((Succ (lam (n z s) (s n))) \ + \ (Zero (lam (z s) z))) \ + \ Zero)" _ <- withFile fileName ReadMode $ \hin -> withFile outputFileName AppendMode $ \hout -> @@ -50,21 +46,7 @@ spec = parallel $ out <- readFile outputFileName out - `shouldBe` "\955\928> defined Nat : U\n\955\928> defined id : \928 A : U . A \8594 A\n\955\928> succ succ succ zero : Sum(zero| succ Nat)\n\955\928> Bye!\n" - - describe "Purer REPL" $ do - it "keeps handling Inputs even when they fail" $ do - let inputs = - [ In "Unit : U", - In "Unit : U = Sum(tt)", - Com DumpEnv - ] - - env (purerREPL (withInputs initialREPL inputs)) - `shouldBe` [("Unit", Var "x")] - - outputs (withInputs initialREPL inputs) - `shouldContain` [Msg "cannot find \"Unit\" in empty context"] + `shouldBe` "\955\928> (lam (z s) z) : c -> d -> c\n\955\928> Bye!\n" withTempFile :: (String -> IO ()) -> IO () withTempFile = |