From 3d98ef51b6d719256c9cff85bab6aac4e19dcac0 Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <p.giarrusso@gmail.com>
Date: Sat, 7 Feb 2015 01:50:54 +0100
Subject: [PATCH] Add parsing for postulates (fix #95)

---
 src-lib/PTS/Syntax/Parser.hs | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/src-lib/PTS/Syntax/Parser.hs b/src-lib/PTS/Syntax/Parser.hs
index 462aa78..226724d 100644
--- a/src-lib/PTS/Syntax/Parser.hs
+++ b/src-lib/PTS/Syntax/Parser.hs
@@ -112,6 +112,8 @@ stmt = withPos StmtPos $ asum
   [ Export <$> (keyword "export" *> ident <* semi)
   , Import <$> (keyword "import" *> modname <* semi)
   , Assertion <$> (keyword "assert" *> expr) <*> optionMaybe (colon1 *> expr) <*> optionMaybe (assign *> expr) <* semi
+  -- we don't support argument telescopes for postulates -- yet!
+  , Bind <$> (keyword "postulate" *> ident) <*> pure [] <*> (colon1 *> (Just <$> expr)) <*> pure Nothing <* semi
   , try (Term <$> expr <* semi)
   , Bind <$> ident <*> telescope <*> optionMaybe (colon1 *> expr) <* assign <*> (Just <$> expr) <* semi]
 
@@ -168,7 +170,7 @@ pragma = lexem $ do
     -- LEXER --
      ---------
 
-keywords = ["Lambda", "lambda", "Pi", "if0", "then", "else", "->", "add", "mul", "sub", "div", "module", "import", "export", "assert", "language", "_("]
+keywords = ["Lambda", "lambda", "Pi", "if0", "then", "else", "->", "add", "mul", "sub", "div", "module", "import", "export", "assert", "language", "postulate", "_("]
 
 identChar x = not (isSpace x) && x `notElem` ".:=;/()[]$"