From ff7180e6b5c139848ee187c2fb6faf8070749cd1 Mon Sep 17 00:00:00 2001 From: Arnaud Bailly Date: Tue, 30 Jul 2019 13:56:27 +0200 Subject: [PATCH] check noprelude option when starting up without loading a file #65 --- src/Idris/Main.idr | 20 +++++++------- tests/Main.idr | 13 +++++---- tests/idris2/basic028/Do.idr | 49 ++++++++++++++++++++++++++++++++++ tests/idris2/basic028/expected | 7 +++++ tests/idris2/basic028/input | 6 +++++ tests/idris2/basic028/run | 5 ++++ 6 files changed, 84 insertions(+), 16 deletions(-) create mode 100644 tests/idris2/basic028/Do.idr create mode 100644 tests/idris2/basic028/expected create mode 100644 tests/idris2/basic028/input create mode 100755 tests/idris2/basic028/run diff --git a/src/Idris/Main.idr b/src/Idris/Main.idr index 0e0d348..f46f906 100644 --- a/src/Idris/Main.idr +++ b/src/Idris/Main.idr @@ -126,22 +126,24 @@ stMain opts u <- newRef UST initUState updateREPLOpts + session <- getSession case fname of Nothing => logTime "Loading prelude" $ - readPrelude - Just f => logTime "Loading main file" $ + when (not $ noprelude session) $ + readPrelude + Just f => logTime "Loading main file" $ loadMainFile f doRepl <- postOptions opts - if doRepl - then + if doRepl + then if ide || ideSocket - then - if not ideSocket + then + if not ideSocket then do setOutput (IDEMode 0 stdin stdout) replIDE {c} {u} {m} - else do + else do f <- coreLift $ initIDESocketFile 38398 case f of Left err => do @@ -149,8 +151,8 @@ stMain opts coreLift $ exit 1 Right file => do setOutput (IDEMode 0 file file) - replIDE {c} {u} {m} - else do + replIDE {c} {u} {m} + else do iputStrLn $ "Welcome to Idris 2 version " ++ version ++ ". Enjoy yourself!" repl {c} {u} {m} diff --git a/tests/Main.idr b/tests/Main.idr index 76b197c..428f581 100644 --- a/tests/Main.idr +++ b/tests/Main.idr @@ -5,7 +5,7 @@ import System %default covering ttimpTests : List String -ttimpTests +ttimpTests = ["basic001", "basic002", "basic003", "basic004", "basic005", "basic006", "coverage001", "coverage002", @@ -28,7 +28,7 @@ idrisTests "basic011", "basic012", "basic013", "basic014", "basic015", "basic016", "basic017", "basic018", "basic019", "basic020", "basic021", "basic022", "basic023", "basic024", "basic025", - "basic026", "basic027", + "basic026", "basic027", "basic028", "coverage001", "coverage002", "coverage003", "coverage004", "error001", "error002", "error003", "error004", "error005", "error006", "error007", "error008", "error009", "error010", @@ -58,16 +58,16 @@ typeddTests chezTests : List String chezTests - = ["chez001", "chez002", "chez003", "chez004", + = ["chez001", "chez002", "chez003", "chez004", "chez005", "chez006", "chez007"] chdir : String -> IO Bool -chdir dir +chdir dir = do ok <- foreign FFI_C "chdir" (String -> IO Int) dir pure (ok == 0) fail : String -> IO () -fail err +fail err = do putStrLn err exitWith (ExitFailure 1) @@ -134,7 +134,7 @@ main then runChezTests idris2 filteredChezTests else pure [] let res = nonCGTestRes ++ chezTestRes - putStrLn (show (length (filter id res)) ++ "/" ++ show (length res) + putStrLn (show (length (filter id res)) ++ "/" ++ show (length res) ++ " tests successful") if (any not res) then exitWith (ExitFailure 1) @@ -142,4 +142,3 @@ main where testPaths : String -> List String -> List String testPaths dir tests = map (\test => dir ++ "/" ++ test) tests - diff --git a/tests/idris2/basic028/Do.idr b/tests/idris2/basic028/Do.idr new file mode 100644 index 0000000..156f27c --- /dev/null +++ b/tests/idris2/basic028/Do.idr @@ -0,0 +1,49 @@ +data Maybe a = Nothing + | Just a + +infixl 1 >>= + +(>>=) : Maybe a -> (a -> Maybe b) -> Maybe b +(>>=) Nothing k = Nothing +(>>=) (Just x) k = k x + +data Nat : Type where + Z : Nat + S : Nat -> Nat + +plus : Nat -> Nat -> Nat +plus Z y = y +plus (S k) y = S (plus k y) + +maybeAdd' : Maybe Nat -> Maybe Nat -> Maybe Nat +maybeAdd' x y + = x >>= \x' => + y >>= \y' => + Just (plus x' y') + +maybeAdd : Maybe Nat -> Maybe Nat -> Maybe Nat +maybeAdd x y + = do x' <- x + y' <- y + Just (plus x' y') + +data Either : Type -> Type -> Type where + Left : a -> Either a b + Right : b -> Either a b + +mEmbed : Maybe a -> Maybe (Either String a) +mEmbed Nothing = Just (Left "FAIL") +mEmbed (Just x) = Just (Right x) + +mPatBind : Maybe Nat -> Maybe Nat -> Maybe Nat +mPatBind x y + = do Right res <- mEmbed (maybeAdd x y) + | Left err => Just Z + Just res + +mLetBind : Maybe Nat -> Maybe Nat -> Maybe Nat +mLetBind x y + = do let Just res = maybeAdd x y + | Nothing => Just Z + Just res + diff --git a/tests/idris2/basic028/expected b/tests/idris2/basic028/expected new file mode 100644 index 0000000..c76d47c --- /dev/null +++ b/tests/idris2/basic028/expected @@ -0,0 +1,7 @@ +Welcome to Idris 2 version 0.0. Enjoy yourself! +Main> 1/1: Building Do (Do.idr) +Main> Just (S (S (S Z))) +Main> Just Z +Main> Just (S (S (S Z))) +Main> Just Z +Main> Bye for now! diff --git a/tests/idris2/basic028/input b/tests/idris2/basic028/input new file mode 100644 index 0000000..9630947 --- /dev/null +++ b/tests/idris2/basic028/input @@ -0,0 +1,6 @@ +:l Do.idr +mPatBind (Just (S Z)) (Just (S (S Z))) +mPatBind (Just (S Z)) Nothing +mLetBind (Just (S Z)) (Just (S (S Z))) +mLetBind (Just (S Z)) Nothing +:q diff --git a/tests/idris2/basic028/run b/tests/idris2/basic028/run new file mode 100755 index 0000000..1caedf8 --- /dev/null +++ b/tests/idris2/basic028/run @@ -0,0 +1,5 @@ +unset IDRIS2_PATH + +$1 --no-prelude < input + +rm -rf build