diff options
Diffstat (limited to 'lambda-calcul/haskell/test/Minilang/REPLSpec.hs')
| -rw-r--r-- | lambda-calcul/haskell/test/Minilang/REPLSpec.hs | 34 |
1 files changed, 8 insertions, 26 deletions
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 = |