Commits

maloneymr  committed 8162205

Parser now works 100%

  • Participants
  • Parent commits 273a411

Comments (0)

Files changed (3)

                "(x:*)->(y:*)->x y",
                "\\x:*.x",
                "\\x:*.\\y:*.x",
-               "x -> y -> z" ]
+               "x -> y -> z",
+               "* = *",
+               "\\x:*. \\y:*. x = y",
+               "\\x:*. \\y:*. x x = y" ]
   mapM_ par progs
+  putStrLn "DONE"
 
 import Text.Parsec.Prim
 
 type Binding = (String, Term)
-type PState = ([Binding], [String])
+type PState = [Binding]
 
-initPState = ([], [])
+initPState = []
 
 pushBinding :: Binding -> GenParser Token PState ()
-pushBinding b = modifyState $ \(bs, hist) -> (b:bs, hist)
+pushBinding b = modifyState $ \bs -> b:bs
 
 popBinding :: GenParser Token PState ()
-popBinding = modifyState $ \(b:bs, hist) -> (bs, hist)
+popBinding = modifyState $ \(b:bs) -> bs
 
 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)
-  
+  bindings <- getState
+  let find ((name', _):xs) | name' == name = 0
+                           | otherwise = 1 + find xs
+      idx = if name `elem` map fst bindings then find bindings else -1
+  return $ idx
 
 -- Precedence Rules
 
 pTerm :: GenParser Token PState Term
 pTerm = try pLambda <|>
-        pApp
-
-pApp = try pApply <|>
-       pFunc
+        pFunc
 
 pFunc = try pFuncArrow <|>
         try pFuncDep <|>
-        pBasic
+        pEq
+
+pEq = try pEqual <|>
+      pApp
+     
+pApp = do
+  ts <- many1 pBasic
+  return $ foldl1 App ts
 
 pBasic = try pStar <|>
          try pVar <|>
   t2 <- pTerm
   return $ Lam t1 t2
 
+-- PEq
+
+pEqual = do
+  t1 <- pApp
+  consumeToken TEq
+  t2 <- pApp
+  return $ Eq t1 t2
+
 -- App
 
 pApply = do
-  f <- pFunc
+  f <- pBasic
   a <- pApp
   return $ App f a
 
 pFuncArrow = do
   t1 <- pApp
   consumeToken TArr
-  t2 <- pApp
+  pushBinding ("_", t1) -- anonymous binding
+  t2 <- pFunc
+  popBinding
   return $ Forall t1 t2
 
 pFuncDep = do 
 
 --
 
-
-
-
 pIdent = do
   (TIdent name) <- tokSatisfy $ (\x -> 
           case x of
   case res of
        Left errorMsg -> print errorMsg
        Right term -> print term
+  putStrLn ""
  
 
 pProgram = do
 consumeAnyToken = tokSatisfy (const True)
   
 
-{-
-Grammar
 
-TERM := VAR
-        STAR
-        '(' TERM ')'
-        '(' VAR ':' TERM ')' '->' TERM
-        '\' VAR ':' TERM '->' TERM
-        TERM TERM
-        TERM '->' TERM
 
-
-
--}

File Tokenizer.hs

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