Can typecheck universe-polymorphic id

1 files changed, 94 insertions, 26 deletions

diff --git a/src/Parser.hs b/src/Parser.hs
index 7464d85..fcab060 100644
--- a/src/Parser.hs
+++ b/src/Parser.hs
@@ -4,7 +4,6 @@ import Control.Monad
 import Data.Char
 import Data.List (foldl')
 import Text.Parsec hiding (token)
-import Text.Parsec.Expr
 
 import AST
 
@@ -28,7 +27,7 @@ pDef = do
   whitespace
   token ":"
   whitespace
-  typ <- pTerm
+  typ <- pTerm 0
   whitespaceTo0
   name2 <- pName
   when (name /= name2) $
@@ -36,27 +35,56 @@ pDef = do
   whitespace
   token "="
   whitespace
-  rhs <- pTerm
+  rhs <- pTerm 0
   return (Definition name (rhs :| typ))
 
-pTerm :: Parser Term
-pTerm = buildExpressionParser optable pTermEAtom
-  where
-    optable =
-      [[Infix (token "->" >> return makePi) AssocRight
-       ,Infix (token "→" >> return makePi) AssocRight]
-      ,[Infix (token ":" >> return (\a b -> TAnnot (a :| b))) AssocNone]]
+-- operator precedences:
+--   0 _:_
+--   1 (_ : _) -> _
+--   2 _,_
+
+pTerm :: Int -> Parser Term
+pTerm p | p <= 0 = do
+  e1 <- pTerm 1
+  whitespace
+  choice
+    [do token ":"
+        whitespace
+        e2 <- pTerm 1
+        return (TAnnot (e1 :| e2))
+    ,return e1]
+
+pTerm 1 = do
+  e1 <- pTerm 2
+  whitespace
+  choice
+    [do (token "->" <|> token "→")
+        (x :| ty) <- case e1 of
+          TAnnot (TVar x :| ty) -> return (x :| ty)
+          _ -> fail $ "Expected (x : type) as left-hand side of (->)"
+        whitespace
+        e2 <- pTerm 1
+        return (TPi x ty e2)
+    ,return e1]
+
+pTerm 2 = do
+  e1 <- pTerm 3
+  whitespace
+  choice
+    [do token ","
+        whitespace
+        e2 <- pTerm 2
+        return (TPair e1 e2)
+    ,return e1]
 
-makePi :: Term -> Term -> Term
-makePi (TAnnot (TVar x :| ty1)) ty2 = TPi x ty1 ty2
-makePi ty1 ty2 = TPi ";_" ty1 ty2
+pTerm _ = pTermEAtom
 
 pTermEAtom :: Parser Term
-pTermEAtom = pLambda <|> pApp
+pTermEAtom = pLambda <|> pSpecialApp <|> pApp
 
 pLambda :: Parser Term
 pLambda = do
-  token "\\" <|> token "λ"
+  void (char '\\') <|> token "λ"
   whitespace
   _ <- char '('
   whitespace
@@ -64,63 +92,103 @@ pLambda = do
   whitespace
   token ":"
   whitespace
-  ty <- pTerm
+  ty <- pTerm 0
   whitespace
   _ <- char ')'
   whitespace
   token "->"
-  rhs <- pTerm
+  whitespace
+  rhs <- pTerm 0
   return (TLam x ty rhs)
 
+pSpecialApp :: Parser Term
+pSpecialApp = pSet <|> pSetw <|> pSigma
+  where
+    pSet :: Parser Term
+    pSet = do
+      token "Set"
+      whitespace
+      e <- pTermEAtom
+      return (TSet e)
+
+    pSetw :: Parser Term
+    pSetw = do
+      token "Setw"
+      whitespace
+      n <- read <$> many1 digit
+      return (TSetw n)
+
+    pSigma :: Parser Term
+    pSigma = do
+      token "Sigma"
+      whitespace
+      _ <- char '('
+      whitespace
+      x <- pName
+      whitespace
+      token ":"
+      whitespace
+      ty <- pTerm 0
+      whitespace
+      _ <- char ')'
+      whitespace
+      rhs <- pTermEAtom
+      return (TSigma x ty rhs)
+
 pApp :: Parser Term
 pApp = do
   e1 <- pAtom
-  args <- many (try (whitespace >> pTerm))
+  args <- many (try (whitespace >> pAtom))
   return (foldl' TApp e1 args)
 
 pAtom :: Parser Term
 pAtom = choice
   [do _ <- char '('
       whitespace
-      e <- pTerm
+      e <- pTerm 0
       whitespace
       _ <- char ')'
       return e
   ,TVar <$> pName]
 
-TODO TPair, TSigma ("%"). The rest are environment entries.
+-- TODO TPair, TSigma ("%"). The rest are environment entries.
 
 pName :: Parser Name
 pName = do
   name <- many1 pNameChar
   guard (name `notElem` keywords)
+  guard (head name /= '\\')  -- lambda syntax
   return name
   where
     keywords = ["=", "->", "→", ":", "?", "\\", "λ", "∀", "..", "..."
-               ,"%"  -- for Sigma; hopefully temporary
-               ,"forall", "data", "import", "in", "let"]
+               ,"forall", "data", "import", "in", "let"
+               ,"Sigma", ","  -- temporary
+               ]
 
 pNameChar :: Parser Char
 pNameChar = satisfy (\c -> not (isSpace c) && c `notElem` ".;{}()@\"")
 
 inlineWhite :: Parser ()
 inlineWhite = do
-  spaces
+  skipMany inlineSpace
   choice
     [inlineComment
     -- TODO: nested {- -} comments
     ,return ()]
 
 inlineComment :: Parser ()
-inlineComment = token "--" >> manyTill anyChar newline >> return ()
+inlineComment = token "--" >> manyTill anyChar (lookAhead newline) >> return ()
 
 -- | Skips to the furthest point from here that can be reached without
 -- consuming any tokens, and without ending on column 0.
 whitespace :: Parser ()
 whitespace = do
   inlineWhite
-  optional $
-    many newline >> (void space <|> inlineComment) >> whitespace
+  optional $ try $
+    many newline >> (inlineSpace <|> inlineComment) >> whitespace
+
+inlineSpace :: Parser ()
+inlineSpace = void (satisfy (\c -> isSpace c && c /= '\n')) <?> "inline whitespace"
 
 -- | Skips as much whitespace as possible, and throws an error if that doesn't
 -- leave us on column 0.