Commits

maloneymr  committed 273a411

Parser is cleaner, but freezes. I guess that's an improvement.

  • Participants
  • Parent commits feb6266

Comments (0)

Files changed (3)

 module Main where
 
-import qualified Parser as P
+import Parser
 
-main = P.main
+main :: IO ()
+main = do 
+  let progs = ["*", 
+               "x", 
+               "(x)", 
+               "*",
+               "(x:*)->x",
+               "*->*",
+               "(x:*)->x",
+               "(x:*)->x->x",
+               "x y",
+               "x y z",
+               "(x:*)->(y:*)->x y",
+               "\\x:*.x",
+               "\\x:*.\\y:*.x",
+               "x -> y -> z" ]
+  mapM_ par progs
+
-
 module Parser where
 
 import Tokenizer
 import Text.Parsec.Pos
 import Text.Parsec.Prim
 
-type PCtx = [(String, Term)]
+type Binding = (String, Term)
+type PState = ([Binding], [String])
 
+initPState = ([], [])
 
-pTerm :: GenParser Token PCtx Term
-pTerm = try pVar <|> 
-        try pStar <|> 
-        pLpTerm 
+pushBinding :: Binding -> GenParser Token PState ()
+pushBinding b = modifyState $ \(bs, hist) -> (b:bs, hist)
+
+popBinding :: GenParser Token PState ()
+popBinding = modifyState $ \(b:bs, hist) -> (bs, hist)
+
+bindingIndex :: String -> GenParser Token PState Int
+bindingIndex name = do
+  (bindings, _) <- getState
+  let idx ((name', _):xs) | name' == name = 0
+                 | otherwise = 1 + idx xs
+  return $ idx bindings
+
+pushVisit :: String ->GenParser Token PState ()
+pushVisit name = modifyState $ \(bindings, visits) -> (bindings, name : visits)
+  
+
+-- Precedence Rules
+
+pTerm :: GenParser Token PState Term
+pTerm = try pLambda <|>
+        pApp
+
+pApp = try pApply <|>
+       pFunc
+
+pFunc = try pFuncArrow <|>
+        try pFuncDep <|>
+        pBasic
+
+pBasic = try pStar <|>
+         try pVar <|>
+         pParen 
+
+-- Lambda
+
+pLambda = do 
+  consumeToken TLam
+  name <- pIdent
+  consumeToken TColon
+  t1 <- pTerm
+  pushBinding (name, t1)
+  consumeToken TDot
+  t2 <- pTerm
+  return $ Lam t1 t2
+
+-- App
+
+pApply = do
+  f <- pFunc
+  a <- pApp
+  return $ App f a
+
+-- Func 
+
+pFuncArrow = do
+  t1 <- pApp
+  consumeToken TArr
+  t2 <- pApp
+  return $ Forall t1 t2
+
+pFuncDep = do 
+  consumeToken TLP
+  name <- pIdent 
+  consumeToken TColon
+  t1 <- pTerm
+  consumeToken TRP
+  consumeToken TArr
+  pushBinding (name, t1)
+  t2 <- pTerm
+  popBinding
+  return $ Forall t1 t2
+
+-- Basic
+
+pStar = do 
+  token <- consumeAnyToken
+  case token of 
+    TStar n -> do
+      return $ Star n
+    otherwise -> parserZero
+  
+pVar = do 
+  name <- pIdent
+  st <- getState
+  id <- bindingIndex name
+  return $ Var id
+
+pParen = do
+  consumeToken TLP
+  t <- pTerm
+  consumeToken TRP
+  return t
+
+--
+
+
+
 
 pIdent = do
   (TIdent name) <- tokSatisfy $ (\x -> 
              otherwise -> False)
   return name
 
-pStar :: GenParser Token st Term  
-pStar = do 
-  (TStar n) <- tokSatisfy $ \x ->
-    case x of 
-      TStar n -> True
-      otherwise -> False
-  return $ Star n
-
-pLpTerm = do consumeToken TLP >> (try paren <|> depFunc)
-  where paren = do
-                 t <- pTerm
-                 consumeToken TRP
-                 return t
-        depFunc = do
-                  name <- pIdent 
-                  consumeToken TColon
-                  t1 <- pTerm
-                  consumeToken TRP
-                  consumeToken TArr
-                  updateState $ ((name, t1):)
-                  t2 <- pTerm
-                  return $ Forall t1 t2
-  
-pRecTerm = do try app <|> arr
-  where app = do
-              t1 <- pTerm
-              t2 <- pRecTerm
-              return $ App t1 t2
-        arr = do
-              consumeToken TArr
-              t <- pTerm
-              return $ t -- wrong
-
-pVar :: GenParser Token PCtx Term
-pVar = do 
-  name <- pIdent
-  st <- getState
-  let idx ((name', _):xs) | name == name' = 0
-                          | otherwise = 1 + idx xs
-      idx [] = -1
-  return $ Var (idx st)
-
-
-{-
-pApp = do
-  char '('
-  t1 <- pTerm
-  char ' '
-  t2 <- pTerm
-  char ')'
-  return $ App t1 t2
-
-pFunc = try pFuncDep <|> pFuncArrow
-
-pFuncArrow = do
-  t1 <- pTerm 
-  char '-'
-  char '>'
-  t2 <- pTerm
-  return $ Forall t1 t2
-
-pFuncDep = do
-  char '('
-  name <- pIdent
-  char ':'
-  t1 <- pTerm
-  char ')'
-  char '-' 
-  char '>'
-  updateState $ ((name, t1):)
-  t2 <- pTerm
-
-  updateState $ ( (name,  t1):)
-  return $ Forall t1 t2
-
-pLam = do
-  char '\\'
-  name <- pIdent
-  char ':'
-  t1 <- pTerm
-  char '-'
-  char '>'
-
-  st <- getState
-  setState $ (name, t1) : st
-  t2 <- pTerm
-  return $ Lam t1 t2
-
--}
-
-main :: IO ()
-main = do 
-  let progs = ["*", "x", "(x)", "*",
-               "(x:*)->x"]
-  mapM_ par progs
 
 par str = do
   putStrLn str
   putStr "  "
   print toks
   putStr "  "
-  let res = runParser pTerm [] "(unkown)" toks
+  let res = runParser pProgram initPState "(unkown)" toks
   case res of
        Left errorMsg -> print errorMsg
        Right term -> print term
-  
+ 
 
-{-
-  let inputs = ["*",
-                "(*)",
-                "(x:*)->*", 
-                "\\x:*->*",
-                "\\x:*->x",
-                "\\x:*->(\\y:*->x)",
-                "\\x:*->(\\y:*->y)",
-                "((x:*)->x)",
-                "\\x:(*->*)->(\\y:*->(x y))"]
-   
-  mapM_ printParse inputs -}
-
+pProgram = do
+  t <- pTerm 
+  eof
+  return t
 
 tokSatisfy :: Monad m => (Token -> Bool) -> ParsecT [Token] u m Token
 tokSatisfy test = tokenPrim show tokNextPos tokTest
 consumeToken :: Token -> GenParser Token st Token
 consumeToken t = tokSatisfy (==t)
 
-getToken :: GenParser Token st Token
-getToken = tokSatisfy (const True)
+consumeAnyToken :: GenParser Token st Token
+consumeAnyToken = tokSatisfy (const True)
   
 
 {-
         TERM TERM
         TERM '->' TERM
 
-TERM := VAR
-        STAR
-        '(' LPTERM
-        '\' VAR ':' TERM '->' TERM
-        TERM '->' TERM
-
-        TERM TERM
-
-TERM := VAR TERM'?
-        STAR TERM'?
-        '(' TERM ')' TERM'?
-        '(' VAR ':' TERM ')' '->' TERM TERM'?
-        '\' VAR ':' TERM '->' TERM TERM'?
-
-TERM' :=
-        TERM TERM'
-        '->' TERM'
-
-LPTERM := TERM ')'
-        | VAR ':' TERM ')' '->' TERM 
-
 
 
 -}

File Tokenizer.hs

            | TArr
            | TLam
            | TColon
+           | TDot
   deriving (Eq, Show)
            
 
 tTokens :: GenParser Char () [Token]
-tTokens = many $ tVar <|> tRP <|> tLP <|> tCol <|> tArr <|> tStar <|> tLam
+tTokens = do
+  many $ do
+    ts <- tVar <|> tRP <|> tLP <|> tCol <|> tArr <|> tStar <|> tLam <|> tDot
+    many (char ' ')
+    return ts
+
 
 tVar :: GenParser Char () Token
 tVar = do
 tCol = do char ':'; return TColon 
 tStar :: GenParser Char () Token 
 tStar = do char '*'; return $ TStar 0
+tDot = do char '.'; return TDot
 
 tokenize :: String -> [Token]
 tokenize input = let Right res = parse tTokens "" input in res