HM parser

diff --git a/src/HM/Parser.hs b/src/HM/Parser.hs
index f02a7cc..47c4649 100644 (file)
--- a/src/HM/Parser.hs
+++ b/src/HM/Parser.hs
@@ -23,6 +23,16 @@ import Control.Applicative
 
 import HM.Term
 
 
 import HM.Term
 

+-- $setup
+-- >>> import Test.QuickCheck
+-- >>> import Test.HM.Term
+
+-- | 
+-- >>> print $ Lam "x" (Var "x")
+-- (λx.x)
+
+
+

 braced :: String -> String
 braced t = "(" ++ t ++ ")"
 
 braced :: String -> String
 braced t = "(" ++ t ++ ")"
 


@@ -58,39 +68,34 @@ parseTerm = parseLet <|>
             parseVar <|>
             parseLambda
 
             parseVar <|>
             parseLambda
 

-parseTermNA :: Parser Term
-parseTermNA = parseLet <|>
+parseTermNoApp :: Parser Term
+parseTermNoApp = parseLet <|>

             parseVar <|>
             parseLambda
 
             parseVar <|>
             parseLambda
 

-parseTypeAndTermNA :: Parser TypedTerm
-parseTypeAndTermNA = do
-  term <- parseTermNA
+parseTypeAndTerm :: Parser Term -> Parser TypedTerm
+parseTypeAndTerm p = do
+  term <- p

   string " :: "
   tp <- parseTypeScheme
   return $! TTerm term tp
 
   string " :: "
   tp <- parseTypeScheme
   return $! TTerm term tp
 

-parseTypeAndTerm :: Parser TypedTerm
-parseTypeAndTerm = do
-  term <- parseTerm
-  string " :: "
-  tp <- parseTypeScheme
-  return $! TTerm term tp

 
 

-parseTypedTermNA :: Parser TypedTerm
-parseTypedTermNA = parseBraces <|>
-                   parseTypeAndTermNA <|>
-                   (NTTerm <$> parseTerm)
+parseTypedTermNoApp :: Parser TypedTerm
+parseTypedTermNoApp = parseBraces parseTypedTerm <|>
+                      parseTypeAndTerm parseTermNoApp <|>
+                      (NTTerm <$> parseTermNoApp)

 
 parseTypedTerm :: Parser TypedTerm
 
 parseTypedTerm :: Parser TypedTerm

-parseTypedTerm = parseBraces <|>
-                parseTypeAndTerm <|>
-                (NTTerm <$> parseTerm)
+parseTypedTerm = parseBraces parseTypedTerm <|>
+                 parseTypeAndTerm parseTerm <|>
+                 (NTTerm <$> parseTerm)

 
 parseType :: Parser Type
 
 parseType :: Parser Type

-parseType = parsePrimitive <|>
-            parseTypeVar <|>
-            parseTypeFunction
+parseType = parseBraces parseType <|>
+            parseTypeFunction <|>
+            parsePrimitive <|>
+            parseTypeVar

 
 parsePrimitive :: Parser Type
 parsePrimitive = do
 
 parsePrimitive :: Parser Type
 parsePrimitive = do


@@ -99,32 +104,33 @@ parsePrimitive = do
 
 parseTypeVar :: Parser Type
 parseTypeVar = do
 
 parseTypeVar :: Parser Type
 parseTypeVar = do

-  x <- many1 $ satisfy isAsciiLower
+  x <- many1 $ satisfy isAsciiLower 

   return $! TypeVar x
 
 parseTypeFunction :: Parser Type
 parseTypeFunction = do
   return $! TypeVar x
 
 parseTypeFunction :: Parser Type
 parseTypeFunction = do

-  a <- parseType
+  a <- parseBraces parseType <|> parsePrimitive <|> parseTypeVar

   string " -> "
   b <- parseType
   return $! TypeFunction a b
 
 parseTypeScheme :: Parser TypeScheme
   string " -> "
   b <- parseType
   return $! TypeFunction a b
 
 parseTypeScheme :: Parser TypeScheme

-parseTypeScheme = parseForAll <|>
+parseTypeScheme = parseBraces parseTypeScheme <|>
+                  parseForAll <|>

                   (TScheme <$> parseType)
 
 parseForAll :: Parser TypeScheme
 parseForAll = do
   string "FORALL "
   (TypeVar x) <- parseTypeVar
                   (TScheme <$> parseType)
 
 parseForAll :: Parser TypeScheme
 parseForAll = do
   string "FORALL "
   (TypeVar x) <- parseTypeVar

-  string "."
+  string ": " 

   t <- parseTypeScheme
   return $! TSForAll x t
 
   t <- parseTypeScheme
   return $! TSForAll x t
 

-parseBraces :: Parser TypedTerm
-parseBraces = do
+parseBraces :: Parser a -> Parser a
+parseBraces p = do

   char '('
   char '('

-  t <- parseTypedTerm
+  t <- p

   char ')'
   return t 
 
   char ')'
   return t 
 


@@ -154,18 +160,18 @@ parseLambda = do
 
 parseApp :: Parser Term
 parseApp = do
 
 parseApp :: Parser Term
 parseApp = do

-  aps <- sepBy1 parseTypedTermNA (char ' ')
-  return $! createApp aps
+  aps <- sepBy1 parseTypedTermNoApp (char ' ')
+  createApp aps

 
 createLambda :: [Term] -> TypedTerm -> TypedTerm
 createLambda (Var x : vs) t = NTTerm . Lam x $ createLambda vs t
 createLambda [] t = t
 createLambda _ _ = error "createLambda failed"
 
 
 createLambda :: [Term] -> TypedTerm -> TypedTerm
 createLambda (Var x : vs) t = NTTerm . Lam x $ createLambda vs t
 createLambda [] t = t
 createLambda _ _ = error "createLambda failed"
 

-createApp :: [TypedTerm] -> Term
-createApp [t,ts] = App t ts
+createApp :: [TypedTerm] -> Parser Term
+createApp [t,ts] = return $ App t ts

 createApp (t:ts:tss) = createApp (NTTerm (App t ts) : tss)
 createApp (t:ts:tss) = createApp (NTTerm (App t ts) : tss)

-createApp [] = error "empty createApp"
+createApp _ = fail "not App"

 
 
 -- |
 
 
 -- |

diff --git a/src/Lambda.hs b/src/Lambda.hs
index 3026b75..428ac99 100644 (file)
--- a/src/Lambda.hs
+++ b/src/Lambda.hs
@@ -26,6 +26,9 @@ import Control.Monad.State
 
 import Lambda.Term
 
 
 import Lambda.Term
 

+import Debug.Trace
+import Lambda.Parser.Fancy ()
+

 -- $setup
 -- >>> import Control.Applicative
 -- >>> import Lambda.Parser.Fancy
 -- $setup
 -- >>> import Control.Applicative
 -- >>> import Lambda.Parser.Fancy


@@ -133,14 +136,22 @@ travPre fnc term = tr fnc (term, E, Down)
 -- >>> toNormalForm Lazy 100 $ (App (App cK cI) cY)
 -- Just (λx.x)
 --
 -- >>> toNormalForm Lazy 100 $ (App (App cK cI) cY)
 -- Just (λx.x)
 --

--- prop> within 10000000 $ (\ t u -> t == u || t == Nothing || u == Nothing) (alphaNorm <$> toNormalForm Lazy 1000 x) (alphaNorm <$> toNormalForm Eager 1000 x)
+-- prop> within 10000000 $ (\ t u -> t == u || t == Nothing || u == Nothing) (alphaNorm <$> toNormalForm Lazy 100 x) (alphaNorm <$> toNormalForm Eager 100 x)

 
 -- inf = tRead "(\\d.a ((\\d c.c d c) (\\x y z.x z (y z)) (\\f.(\\x.f (x x)) (\\x.f (x x))) e))"
 
 
 -- inf = tRead "(\\d.a ((\\d c.c d c) (\\x y z.x z (y z)) (\\f.(\\x.f (x x)) (\\x.f (x x))) e))"
 

+
+toNormalFormDebug :: Strategy -> Int -> Term -> Maybe Term
+toNormalFormDebug Eager n = flip evalStateT 0 . travPost (prnt >=> cnt >=> short n >=> return . reduceStep)
+toNormalFormDebug Lazy  n = flip evalStateT 0 . travPre  (prnt >=> cnt >=> short n >=> return . reduceStep)
+

 toNormalForm :: Strategy -> Int -> Term -> Maybe Term
 toNormalForm Eager n = flip evalStateT 0 . travPost (cnt >=> short n >=> return . reduceStep)
 toNormalForm Lazy  n = flip evalStateT 0 . travPre  (cnt >=> short n >=> return . reduceStep)
 
 toNormalForm :: Strategy -> Int -> Term -> Maybe Term
 toNormalForm Eager n = flip evalStateT 0 . travPost (cnt >=> short n >=> return . reduceStep)
 toNormalForm Lazy  n = flip evalStateT 0 . travPre  (cnt >=> short n >=> return . reduceStep)
 

+prnt :: (Monad m) => Term -> StateT Int m Term
+prnt t = traceShow t $ return t
+

 cnt :: (Monad m) => Term -> StateT Int m Term
 cnt t@RedEx{} = do
   modify (+ 1)
 cnt :: (Monad m) => Term -> StateT Int m Term
 cnt t@RedEx{} = do
   modify (+ 1)

diff --git a/tests/Test/HM/Term.hs b/tests/Test/HM/Term.hs
new file mode 100644 (file)
index 0000000..9210c6d
--- /dev/null
+++ b/tests/Test/HM/Term.hs
@@ -0,0 +1,49 @@
+{-# OPTIONS_GHC -fno-warn-orphans #-}
+
+module Test.Term where
+
+import Test.QuickCheck
+import Control.Applicative
+import Lambda.Parser.Fancy
+import Lambda.Term
+
+cP :: Term
+cP = tRead "(λa d c.(λa.e) b (λc.d)) ((λa.(λd.a) (λd c.b ((λa.a) a)) (a ((λa.(λd.e) ((λe.(λd b.a) (λa c.(λa a d.(λd.b (λa d.c) e) (λb b.c a (a d (λb d d e a.d (λb b.d))))) ((λb.a) c)) (d ((λc.(λd.a (λe.e)) (c d)) ((λe.b) a))) c (λa.d (e (λe.(λd c.b) a))) (c (b a)) a (λe.(λa b e b a.d) b)) ((λe.b) (λa.b)) ((λe d.b) b) e) b) ((λc c.a e) (λb.(λb.e) a)))) (λe.e) b (λd c e e c a.c)) a)"
+
+cY :: Term
+cY = tRead "λf.(λx.f (x x)) (λx.f (x x))"
+cI :: Term
+cI = tRead "λx.x"
+cK :: Term
+cK = tRead "λx y.x"
+cS :: Term
+cS = tRead "λx y z.x z (y z)"
+
+instance Arbitrary Term
+  where arbitrary = sized aTerm
+
+aVarName :: Gen String
+aVarName = oneof . map (pure . (:[])) $ ['a'..'e']
+
+aTypeName :: Gen String
+aTypeName = oneof . map (pure . (:[])) $ ['A'..'E']
+
+aComb :: Gen Term
+aComb = oneof . map pure $ [cS, cK, cI, cY]
+
+aVar :: Gen Term
+aVar = liftA Var aVarName
+
+aTerm :: Int -> Gen Term
+aTerm 0 = aVar 
+aTerm n = oneof 
+            [ aVar, aComb
+            , liftA2 Lam aVarName $ aTerm (n - 1)
+            , liftA2 App (aTerm (n `div` 2)) (aTerm (n `div` 2))
+            , liftA3 Let aVar (aTerm (n / 2)) (aTerm (n / 2))]
+
+--
+-- TODO: shrink Terms
+-- TODO: timed tests
+
+