Stuff

1 files changed, 138 insertions, 0 deletions

diff --git a/src/Parser.hs b/src/Parser.hs
new file mode 100644
index 0000000..7464d85
--- /dev/null
+++ b/src/Parser.hs
@@ -0,0 +1,138 @@
+module Parser (parseProgram) where
+
+import Control.Monad
+import Data.Char
+import Data.List (foldl')
+import Text.Parsec hiding (token)
+import Text.Parsec.Expr
+
+import AST
+
+
+type Parser = Parsec String ()
+
+parseProgram :: String -> String -> Either ParseError [Definition]
+parseProgram fname source = parse pProgram fname source
+
+pProgram :: Parser [Definition]
+pProgram = do
+  whitespaceTo0
+  choice
+    [eof >> return []
+    ,(:) <$> pDef <*> pProgram]
+
+-- | Assumes column 0
+pDef :: Parser Definition
+pDef = do
+  name <- pName
+  whitespace
+  token ":"
+  whitespace
+  typ <- pTerm
+  whitespaceTo0
+  name2 <- pName
+  when (name /= name2) $
+    fail $ "Definition of '" ++ name ++ "' followed by definition for '" ++ name2 ++ "'"
+  whitespace
+  token "="
+  whitespace
+  rhs <- pTerm
+  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]]
+
+makePi :: Term -> Term -> Term
+makePi (TAnnot (TVar x :| ty1)) ty2 = TPi x ty1 ty2
+makePi ty1 ty2 = TPi ";_" ty1 ty2
+
+pTermEAtom :: Parser Term
+pTermEAtom = pLambda <|> pApp
+
+pLambda :: Parser Term
+pLambda = do
+  token "\\" <|> token "λ"
+  whitespace
+  _ <- char '('
+  whitespace
+  x <- pName
+  whitespace
+  token ":"
+  whitespace
+  ty <- pTerm
+  whitespace
+  _ <- char ')'
+  whitespace
+  token "->"
+  rhs <- pTerm
+  return (TLam x ty rhs)
+
+pApp :: Parser Term
+pApp = do
+  e1 <- pAtom
+  args <- many (try (whitespace >> pTerm))
+  return (foldl' TApp e1 args)
+
+pAtom :: Parser Term
+pAtom = choice
+  [do _ <- char '('
+      whitespace
+      e <- pTerm
+      whitespace
+      _ <- char ')'
+      return e
+  ,TVar <$> pName]
+
+TODO TPair, TSigma ("%"). The rest are environment entries.
+
+pName :: Parser Name
+pName = do
+  name <- many1 pNameChar
+  guard (name `notElem` keywords)
+  return name
+  where
+    keywords = ["=", "->", "→", ":", "?", "\\", "λ", "∀", "..", "..."
+               ,"%"  -- for Sigma; hopefully temporary
+               ,"forall", "data", "import", "in", "let"]
+
+pNameChar :: Parser Char
+pNameChar = satisfy (\c -> not (isSpace c) && c `notElem` ".;{}()@\"")
+
+inlineWhite :: Parser ()
+inlineWhite = do
+  spaces
+  choice
+    [inlineComment
+    -- TODO: nested {- -} comments
+    ,return ()]
+
+inlineComment :: Parser ()
+inlineComment = token "--" >> manyTill anyChar 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
+
+-- | Skips as much whitespace as possible, and throws an error if that doesn't
+-- leave us on column 0.
+whitespaceTo0 :: Parser ()
+whitespaceTo0 = do
+  inlineWhite
+  choice
+    [eof
+    ,newline >> whitespaceTo0
+    ,do pos <- getPosition
+        when (sourceColumn pos /= 1) $
+          unexpected "indented code"]
+
+token :: String -> Parser ()
+token s = try $ string s >> (eof <|> void (lookAhead (satisfy (\c -> isSpace c || c `elem` ".;{}()@\""))))