elsa 0.1.0.1 → 0.2.0.0

raw patch · 5 files changed

+102/−14 lines, 5 files

Files

• elsa.cabal +1/−1
• src/Language/Elsa/Eval.hs +3/−4
• src/Language/Elsa/Types.hs +1/−1
• src/Language/Elsa/Utils.hs +5/−1
• tests/Test.hs +92/−7

@@ -1,5 +1,5 @@ name:                elsa-version:             0.1.0.1+version:             0.2.0.0 synopsis:            A tiny language for understanding the lambda-calculus description:         elsa is a small proof checker for verifying sequences of                      reductions of lambda-calculus terms. The goal is to help

@@ -8,8 +8,7 @@ import           Control.Monad.State import           Data.Maybe           (mapMaybe, isJust, maybeToList) import           Language.Elsa.Types-import           Language.Elsa.Utils  (qPushes, qInit, qPop, fromEither)-+import           Language.Elsa.Utils  (traceShow, qPushes, qInit, qPop, fromEither)  -------------------------------------------------------------------------------- elsa :: Elsa a -> [Result a]@@ -196,7 +195,7 @@ isNormEq :: Env a -> Expr a -> Expr a -> Bool isNormEq g e1 e2 = isEquiv g e1' e2   where-    e1'          = evalNO (canon g e1)+    e1'          = traceShow ("evalNO" ++ show e1) $ evalNO (traceShow "CANON" $ canon g e1)  -- | normal-order reduction evalNO :: Expr a -> Expr a@@ -218,7 +217,7 @@ bSubst :: Expr a -> Id -> Expr a -> Expr a bSubst e x e' = subst e (M.singleton x e'')   where-    e''       = alphaShift n e'+    e''       = e' -- alphaShift n e'     n         = 1 + maximum (0 : mapMaybe isAId vs)     vs        = S.toList (freeVars e') 

@@ -143,7 +143,7 @@ instance PPrint (Expr a) where   pprint (EVar x _)     = x   pprint (EApp e1 e2 _) = printf "(%s %s)" (pprint e1) (pprint e2)-  pprint e@(ELam {})    = printf "\\%s -> %s" (pprint xs) (pprint body)+  pprint e@(ELam {})    = printf "(\\%s -> %s)" (pprint xs) (pprint body)     where       (xs, body)        = bkLam e 

@@ -37,7 +37,11 @@ handleIO f e = return . Left $ "Warning: Couldn't open " <> f <> ": " <> show e  traceShow :: (Show a) => String -> a -> a-traceShow msg x = trace (printf "TRACE: %s = %s" msg (show x)) x+traceShow msg x+  | False+  = trace (printf "TRACE: %s = %s" msg (show x)) x+  | otherwise +  = x  safeHead :: a -> [a] -> a safeHead def []    = def

@@ -1,11 +1,96 @@ {-# LANGUAGE OverloadedStrings #-}+{-# OPTIONS_GHC -fno-warn-orphans #-} --- import Control.Exception--- import Test.Tasty--- import Common--- import Data.List (isInfixOf)--- import qualified Language.Elsa.Types as Nano--- import qualified Language.Nano.Eval  as Nano+module Main where +import System.Directory+import System.Exit+import System.FilePath+import System.Environment+import System.IO+import System.IO.Error+import Control.Monad (when)+import Test.Tasty+import Test.Tasty.HUnit+import Text.Printf+import Language.Elsa+ main :: IO ()-main = return ()+main = defaultMain =<< group "Tests" [unitTests]++unitTests = group "Unit"+  [ testGroup "ok"      <$> dirTests "tests/ok"       TestOk+  , testGroup "further" <$> dirTests "tests/further"  TestPartial+  , testGroup "invalid" <$> dirTests "tests/invalid"  TestInvalid+  ]++data Outcome+  = TestOk+  | TestPartial+  | TestInvalid+  | TestMixed+  deriving (Eq, Ord, Show)++--------------------------------------------------------------------------------+dirTests :: FilePath -> Outcome -> IO [TestTree]+--------------------------------------------------------------------------------+dirTests root code+  = do files    <- walkDirectory root+       let tests = [ root </> rel | f <- files, isTest f, let rel = makeRelative root f ]+       return    $ mkTest code <$> tests++isTest   :: FilePath -> Bool+isTest f = takeExtension f `elem` [".lc"]++--------------------------------------------------------------------------------+mkTest :: Outcome -> FilePath -> TestTree+--------------------------------------------------------------------------------+mkTest code file+  = testCase file $ do+     res <- doTest file+     when (res /= code) (assertFailure "Wrong Result")++doTest :: FilePath -> IO Outcome+doTest f =  resultOutcome . elsa <$> parseFile f++resultOutcome :: [Result a] -> Outcome+resultOutcome rs = case (oks, invs, parts) of+                     (True, False, False) -> TestOk+                     (False, True, False) -> TestInvalid+                     (False, False, True) -> TestPartial+                     _                    -> TestMixed+  where+    oks          = notNull [ r | r@(OK {})      <- rs ]+    invs         = notNull [ r | r@(Invalid {}) <- rs ]+    parts        = notNull [ r | r@(Partial {}) <- rs ]+    notNull      = not . null++----------------------------------------------------------------------------------------+-- Generic Helpers+----------------------------------------------------------------------------------------++group n xs = testGroup n <$> sequence xs++----------------------------------------------------------------------------------------+walkDirectory :: FilePath -> IO [FilePath]+----------------------------------------------------------------------------------------+walkDirectory root+  = do (ds,fs) <- partitionM doesDirectoryExist . candidates =<< (getDirectoryContents root `catchIOError` const (return []))+       (fs++) <$> concatMapM walkDirectory ds+  where+    candidates fs = [root </> f | f <- fs, not (isExtSeparator (head f))]++partitionM :: Monad m => (a -> m Bool) -> [a] -> m ([a],[a])+partitionM f = go [] []+  where+    go ls rs []     = return (ls,rs)+    go ls rs (x:xs) = do b <- f x+                         if b then go (x:ls) rs xs+                              else go ls (x:rs) xs++-- isDirectory :: FilePath -> IO Bool+-- isDirectory = fmap Posix.isDirectory . Posix.getFileStatus++concatMapM :: Applicative m => (a -> m [b]) -> [a] -> m [b]+concatMapM _ []     = pure []+concatMapM f (x:xs) = (++) <$> f x <*> concatMapM f xs