práce na parseru pro HM

diff --git a/src/HM.hs b/src/HM.hs
index 83bbe04..065ccbb 100644 (file)
--- a/src/HM.hs
+++ b/src/HM.hs
@@ -11,18 +11,27 @@
 module HM
   ( -- * Types
     Type(..)
-  , Term
+  , TypeScheme(..)
+  , Term(..)
+  , TypedTerm(..)
     -- * Type inference
   , algW
   ) where
 
+import Control.Monad.State
+
 import HM.Term
 import HM.Parser
 
 type Substitution = TypeScheme -> TypeScheme
+type VarS a = State Int a
 
 fresh :: TypeVarName
 fresh = undefined
+--fresh = do
+--  n <- get
+--  "a" ++ show n
+  
 
 substitute :: TypeScheme -> TypeVarName -> TypeScheme -> TypeScheme
 substitute = undefined
@@ -32,17 +41,17 @@ unify (TScheme (Primitive a)) (TScheme (Primitive b)) | a == b = Right id
 unify (TScheme (TypeVar a)) (TScheme (TypeVar b)) | a == b = Right id
 unify a b = Left $ "cannot unify " ++ show a ++ " with " ++ show b
 
-algW :: HMTerm -> Either String TypeScheme
-algW (HMTerm (Var _) t) = Right t
-algW (HMTerm (Lambda x t) (TScheme p)) = do
-  let v = TScheme (TypeVar fresh)
-      np = substitute v x t
-  unify p np
-algW (HMTerm (App u v) t) = do
-  tu <- algW u
-  tv <- algW v
-  case tu of
-    (TScheme (TypeFunction a b)) -> do
-      unify a tv
-      return b
-    _ -> Left $ "cannot apply " ++ show tu ++ " to " ++ show tv
+algW :: TypedTerm -> Either String TypeScheme
+algW (TTerm (Var _) t) = Right t
+--algW (TTerm (Lam x t) (TScheme p)) = do
+--  let v = TScheme (TypeVar fresh)
+--      np = substitute v x t
+--  unify p np
+--algW (TTerm (App u v) t) = do
+--  tu <- algW u
+--  tv <- algW v
+--  case tu of
+--    (TScheme (TypeFunction a b)) -> do
+--      unify a tv
+--      return b
+--    _ -> Left $ "cannot apply " ++ show tu ++ " to " ++ show tv

diff --git a/src/HM/Parser.hs b/src/HM/Parser.hs
index 556cbdb..f02a7cc 100644 (file)
--- a/src/HM/Parser.hs
+++ b/src/HM/Parser.hs
@@ -16,13 +16,12 @@ module HM.Parser
   , parseTerm
   )  where
 
+import Data.Char (isAsciiLower, isAsciiUpper)
 import Data.Text as T hiding (map)
 import Data.Attoparsec.Text
 import Control.Applicative
 
 import HM.Term
-import qualified Lambda.Parser.Fancy as Lambda
-import qualified Lambda.Term as Lambda
 
 braced :: String -> String
 braced t = "(" ++ t ++ ")"
@@ -31,9 +30,9 @@ instance Show Term where
   show (Var x) = x
   show (Lam x (NTTerm (Lam y t))) = show (Lam (x ++ " " ++ y) t)
   show (Lam x t) = braced $ "λ" ++ x ++ "." ++ show t 
-  show (App a (NTTerm (App b c))) = show a ++ " " ++ (braced $ show (App b c))
+  show (App a (NTTerm (App b c))) = show a ++ " " ++ braced ( show (App b c))
   show (App t r) = show t ++ " " ++ show r
-  show (Let x e1 e2) = braced $ "let " ++ x ++ " = " ++ show e1 ++ " in " ++ show e2 
+  show (Let x e1 e2) = braced $ "LET " ++ x ++ " = " ++ show e1 ++ " IN " ++ show e2 
 
 instance Show TypedTerm where
   show (NTTerm t) = show t
@@ -48,36 +47,126 @@ instance Show TypeScheme where
   show (TScheme t) = show t
   show (TSForAll x t) = braced $ "∀" ++ x ++ ": " ++ show t
 
-tRead :: String -> Term
-tRead = undefined
+tRead :: String -> TypedTerm
+tRead s = case parseOnly (parseTypedTerm <* endOfInput) (T.pack s) of
+    (Right t) -> t
+    (Left e) -> error e
 
-parseTerm :: Parser TypedTerm
+parseTerm :: Parser Term
 parseTerm = parseLet <|>
-            (lambdaToHM <$> Lambda.parseTerm)
+            parseApp <|>
+            parseVar <|>
+            parseLambda
 
-parseLet :: Parser TypedTerm
-parseLet = do
+parseTermNA :: Parser Term
+parseTermNA = parseLet <|>
+            parseVar <|>
+            parseLambda
+
+parseTypeAndTermNA :: Parser TypedTerm
+parseTypeAndTermNA = do
+  term <- parseTermNA
+  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)
+
+parseTypedTerm :: Parser TypedTerm
+parseTypedTerm = parseBraces <|>
+                parseTypeAndTerm <|>
+                (NTTerm <$> parseTerm)
+
+parseType :: Parser Type
+parseType = parsePrimitive <|>
+            parseTypeVar <|>
+            parseTypeFunction
+
+parsePrimitive :: Parser Type
+parsePrimitive = do
+  x <- many1 $ satisfy isAsciiUpper
+  return $! Primitive x
+
+parseTypeVar :: Parser Type
+parseTypeVar = do
+  x <- many1 $ satisfy isAsciiLower
+  return $! TypeVar x
+
+parseTypeFunction :: Parser Type
+parseTypeFunction = do
+  a <- parseType
+  string " -> "
+  b <- parseType
+  return $! TypeFunction a b
+
+parseTypeScheme :: Parser TypeScheme
+parseTypeScheme = parseForAll <|>
+                  (TScheme <$> parseType)
+
+parseForAll :: Parser TypeScheme
+parseForAll = do
+  string "FORALL "
+  (TypeVar x) <- parseTypeVar
+  string "."
+  t <- parseTypeScheme
+  return $! TSForAll x t
+
+parseBraces :: Parser TypedTerm
+parseBraces = do
   char '('
-  string "let "
-  (Lambda.Var x) <- Lambda.parseVar
-  string " = "
-  e1 <- lambdaToHM <$> Lambda.parseTerm
-  string " in "
-  e2 <- lambdaToHM <$> Lambda.parseTerm
+  t <- parseTypedTerm
   char ')'
-  return . NTTerm $ Let x e1 e2
+  return t 
+
+parseLet :: Parser Term
+parseLet = do
+  string "LET "
+  (Var x) <- parseVar
+  string " = "
+  e1 <- parseTypedTerm
+  string " IN "
+  e2 <- parseTypedTerm
+  return $! Let x e1 e2
+
+parseVar :: Parser Term
+parseVar = do
+  x <- many1 $ satisfy isAsciiLower
+  return $! Var x
+
+parseLambda :: Parser Term
+parseLambda = do
+  char '\\' <|> char 'λ' <|> char 'L'
+  vars <- sepBy1 parseVar (char ' ')
+  char '.'
+  t <- parseTypedTerm
+  let (NTTerm l) = createLambda vars t
+  return $! l
+
+parseApp :: Parser Term
+parseApp = do
+  aps <- sepBy1 parseTypedTermNA (char ' ')
+  return $! createApp aps
+
+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 (t:ts:tss) = createApp (NTTerm (App t ts) : tss)
+createApp [] = error "empty createApp"
 
-lambdaToHM :: Lambda.Term -> TypedTerm
-lambdaToHM (Lambda.Var x) = NTTerm $ Var x
-lambdaToHM (Lambda.App t u) = NTTerm $ App (lambdaToHM t) (lambdaToHM u)
-lambdaToHM (Lambda.Lambda x t) = NTTerm $ Lam x (lambdaToHM t)
 
 -- |
 -- TODO prop> t == tRead (show (t :: Term))
-
-{-
-tRead :: String -> Term
-tRead s = case parseOnly (parseTerm <* endOfInput) (T.pack s) of
-    (Right t) -> t
-    (Left e) -> error e
--}

diff --git a/src/Lambda/Parser/Fancy.hs b/src/Lambda/Parser/Fancy.hs
index 9a1deb3..3ad5728 100644 (file)
--- a/src/Lambda/Parser/Fancy.hs
+++ b/src/Lambda/Parser/Fancy.hs
@@ -22,6 +22,7 @@ module Lambda.Parser.Fancy
   , parseVar
   )  where
 
+import Data.Char (isAsciiLower)
 import Data.Text as T hiding (map)
 import Data.Attoparsec.Text
 import Control.Applicative
@@ -56,12 +57,12 @@ tRead s = case parseOnly (parseTerm <* endOfInput) (T.pack s) of
 
 parseVar :: Parser Term
 parseVar = do
-  x <- many1 (letter <|> digit)
+  x <- many1 $ satisfy isAsciiLower
   return $! Var x
 
 parseLambda :: Parser Term
 parseLambda = do
-  char '\\' <|> char 'λ'
+  char '\\' <|> char 'λ' <|> char 'L'
   vars <- sepBy1 parseVar (char ' ')
   char '.'
   t <- parseTerm