From b381c4424ab86b1ba3f8c9b40356565e10b78bf0 Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <p.giarrusso@gmail.com>
Date: Fri, 6 Feb 2015 21:56:17 +0100
Subject: [PATCH 01/18] Add bindings for failed definitions (fix #98)

Untested. This is a close variant to Tillmann's proposal in #98.
---
 src-lib/PTS/Process/File.hs | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/src-lib/PTS/Process/File.hs b/src-lib/PTS/Process/File.hs
index 3402308..b204069 100644
--- a/src-lib/PTS/Process/File.hs
+++ b/src-lib/PTS/Process/File.hs
@@ -168,16 +168,16 @@ processStmt (Bind n args typeAnnot body) = recover () $ do
       whenOption optShowFullTerms $ output (nest 2 (sep [text "full type", nest 2 (pretty 0 t' )]))
 
       -- typecheck type
-      qq <-
+      (qq, s) <-
         flip runEnvironmentT env $
              do
                qq <- typecheckPull t'
-               checkProperType qq (text "in top-level binding of " <+> pretty 0 n) (text "")
-               return qq
+               s <- checkProperType qq (text "in top-level binding of " <+> pretty 0 n) (text "")
+               return (qq, s)
 
       -- use declared type to typecheck push
       qq <- liftEval (eval qq)
-      t <- runEnvironmentT (typecheckPush t qq) env
+      t <- recover (mkVar n qq (Just s)) $ runEnvironmentT (typecheckPush t qq) env
       return t
     Nothing -> do
       -- typecheck pull

From b580313410e57ac45de1cda116181372b64b0821 Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <p.giarrusso@gmail.com>
Date: Fri, 6 Feb 2015 23:25:46 +0100
Subject: [PATCH 02/18] Add `recoverWith` method suggested by Tillmann (#98)

Tillmann suggested writing `recover` in terms of `recoverWith`, but that
requires changing more code, and it was not fully obvious to me how to do those
changes.
---
 src-lib/Control/Monad/Errors/Class.hs | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/src-lib/Control/Monad/Errors/Class.hs b/src-lib/Control/Monad/Errors/Class.hs
index 23ec66e..16ed888 100644
--- a/src-lib/Control/Monad/Errors/Class.hs
+++ b/src-lib/Control/Monad/Errors/Class.hs
@@ -26,3 +26,7 @@ instance (Monoid e, Error e, MonadErrors e m) => MonadErrors e (StateT s m) wher
 instance (Monoid w, MonadErrors e m) => MonadErrors e (WriterT w m) where
   recover x = mapWriterT (recover (x, mempty))
   annotate f = mapWriterT (annotate f)
+
+recoverWith :: (MonadErrors e m, Functor m) => m b -> m b -> m b
+recoverWith computeFallback action =
+    recover Nothing (fmap Just action) >>= maybe computeFallback return

From d7f52dfcd7b8282b2eb6c7c1622c730a7771b0da Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <p.giarrusso@gmail.com>
Date: Sat, 7 Feb 2015 00:23:20 +0100
Subject: [PATCH 03/18] Failing terms: Generate values, not terms (#98)

Follow more closely Tillmann's pseudocode. Instead of generating a typed
variable by hand (duplicating typechecker logic/using a not fully
documented API), and then get from it a value (by evaluation), a type
and a sort, just generate an untyped value by hand (which is easier),
and pass the expected type/sort separately.

I'll admit these conditionals in the needed code are slightly more
complex, but I guess they're OK.

Also, the variable names in the new code are not single letters, which
is somewhat inconsistent (but then, I don't get the old names anyway).
---
 src-lib/PTS/Process/File.hs | 15 +++++++++------
 1 file changed, 9 insertions(+), 6 deletions(-)

diff --git a/src-lib/PTS/Process/File.hs b/src-lib/PTS/Process/File.hs
index b204069..540a869 100644
--- a/src-lib/PTS/Process/File.hs
+++ b/src-lib/PTS/Process/File.hs
@@ -160,7 +160,7 @@ processStmt (Bind n args typeAnnot body) = recover () $ do
 
   env <- getBindings
 
-  t <- case typeAnnot of
+  (maybeT, tType, tSort) <- case typeAnnot of
     Just body' -> do
       -- preprocess type
       let t' = foldTelescope mkPi args body'
@@ -177,18 +177,21 @@ processStmt (Bind n args typeAnnot body) = recover () $ do
 
       -- use declared type to typecheck push
       qq <- liftEval (eval qq)
-      t <- recover (mkVar n qq (Just s)) $ runEnvironmentT (typecheckPush t qq) env
-      return t
+      t <- recover Nothing $ runEnvironmentT (Just <$> typecheckPush t qq) env
+      return (t, qq, Just s)
     Nothing -> do
       -- typecheck pull
       t <- runEnvironmentT (typecheckPull t) env
       q <- liftEval (reify (typeOf t))
       output (nest 2 (sep [text "type:", nest 2 (pretty 0 q)]))
-      return t
+      return (Just t, typeOf t, sortOf t)
 
   -- do binding
-  let v = evalTerm env t
-  putBindings ((n, Binding False v (typeOf t) (sortOf t)) : env)
+  let v =
+        case maybeT of
+          Just t -> evalTerm env t
+          Nothing -> ResidualVar n
+  putBindings ((n, Binding False v tType tSort) : env)
 
 processStmt (Assertion t q' t') = recover () $ assert (showAssertion t q' t') $ do
   output (text "")

From 9f8363ac8017dfdcf8ede065fb7f45368bed280f Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <p.giarrusso@gmail.com>
Date: Sat, 7 Feb 2015 00:28:31 +0100
Subject: [PATCH 04/18] Use checkProperType also without type annotations (fix
 #131)

Declarations without type annotations are going to be well-sorted
in *some* PTS, which might be bigger than the one considered. Hence call
checkProperType there anyway. This finally achieves the consistency
discussed in #98.
---
 examples/Arithmetics.lpts   | 4 ----
 src-lib/PTS/Process/File.hs | 5 +++++
 2 files changed, 5 insertions(+), 4 deletions(-)

diff --git a/examples/Arithmetics.lpts b/examples/Arithmetics.lpts
index 1e864b8..5fa8dc1 100644
--- a/examples/Arithmetics.lpts
+++ b/examples/Arithmetics.lpts
@@ -7,10 +7,6 @@ There is a built-in type `Int`. In bigger languages than STLC, we can even write
 
 < assert Int : *;
 
-and even in STLC we can write
-
-> IntSynonym = Int;
-
 Values of type `Int` can be written as numeric literals.
 
 > assert 0 : Int;
diff --git a/src-lib/PTS/Process/File.hs b/src-lib/PTS/Process/File.hs
index 540a869..da06843 100644
--- a/src-lib/PTS/Process/File.hs
+++ b/src-lib/PTS/Process/File.hs
@@ -183,6 +183,11 @@ processStmt (Bind n args typeAnnot body) = recover () $ do
       -- typecheck pull
       t <- runEnvironmentT (typecheckPull t) env
       q <- liftEval (reify (typeOf t))
+      flip runEnvironmentT env $
+           do
+             tt <- typecheckPull q
+             checkProperType tt (text "in top-level binding of " <+> pretty 0 n) (text "")
+
       output (nest 2 (sep [text "type:", nest 2 (pretty 0 q)]))
       return (Just t, typeOf t, sortOf t)
 

From 7afba16a8d20a13729b321fa5527f26c3a8fe137 Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <p.giarrusso@gmail.com>
Date: Sat, 7 Feb 2015 00:51:20 +0100
Subject: [PATCH 05/18] Refactor new code

---
 src-lib/PTS/Process/File.hs | 23 ++++++++++-------------
 1 file changed, 10 insertions(+), 13 deletions(-)

diff --git a/src-lib/PTS/Process/File.hs b/src-lib/PTS/Process/File.hs
index da06843..da311d6 100644
--- a/src-lib/PTS/Process/File.hs
+++ b/src-lib/PTS/Process/File.hs
@@ -159,6 +159,11 @@ processStmt (Bind n args typeAnnot body) = recover () $ do
   whenOption optShowFullTerms $ output (nest 2 (sep [text "full term", nest 2 (pretty 0 t)]))
 
   env <- getBindings
+  let checkTopLevel typ =
+        flip runEnvironmentT env $ do
+          typ <- typecheckPull typ
+          s <- checkProperType typ (text "in top-level binding of " <+> pretty 0 n) (text "")
+          return (typ, s)
 
   (maybeT, tType, tSort) <- case typeAnnot of
     Just body' -> do
@@ -168,35 +173,27 @@ processStmt (Bind n args typeAnnot body) = recover () $ do
       whenOption optShowFullTerms $ output (nest 2 (sep [text "full type", nest 2 (pretty 0 t' )]))
 
       -- typecheck type
-      (qq, s) <-
-        flip runEnvironmentT env $
-             do
-               qq <- typecheckPull t'
-               s <- checkProperType qq (text "in top-level binding of " <+> pretty 0 n) (text "")
-               return (qq, s)
+      (qq, s) <- checkTopLevel t'
 
       -- use declared type to typecheck push
       qq <- liftEval (eval qq)
       t <- recover Nothing $ runEnvironmentT (Just <$> typecheckPush t qq) env
-      return (t, qq, Just s)
+      return (t, qq, s)
     Nothing -> do
       -- typecheck pull
       t <- runEnvironmentT (typecheckPull t) env
       q <- liftEval (reify (typeOf t))
-      flip runEnvironmentT env $
-           do
-             tt <- typecheckPull q
-             checkProperType tt (text "in top-level binding of " <+> pretty 0 n) (text "")
+      (_, s) <- checkTopLevel q
 
       output (nest 2 (sep [text "type:", nest 2 (pretty 0 q)]))
-      return (Just t, typeOf t, sortOf t)
+      return (Just t, typeOf t, s)
 
   -- do binding
   let v =
         case maybeT of
           Just t -> evalTerm env t
           Nothing -> ResidualVar n
-  putBindings ((n, Binding False v tType tSort) : env)
+  putBindings ((n, Binding False v tType (Just tSort)) : env)
 
 processStmt (Assertion t q' t') = recover () $ assert (showAssertion t q' t') $ do
   output (text "")

From a26ad41b4a08f46e1aecbb924f030323a41ce3b4 Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <p.giarrusso@gmail.com>
Date: Sat, 7 Feb 2015 01:35:17 +0100
Subject: [PATCH 06/18] Share code in prettyprinter

---
 src-lib/PTS/Syntax/Pretty.hs | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/src-lib/PTS/Syntax/Pretty.hs b/src-lib/PTS/Syntax/Pretty.hs
index 39ed1df..c651f29 100644
--- a/src-lib/PTS/Syntax/Pretty.hs
+++ b/src-lib/PTS/Syntax/Pretty.hs
@@ -163,8 +163,10 @@ prettyArgs args = sep (map f args) where
   f (ns, q) = hsep [pretty 0 n | n <- ns] <+> text ":" <+> pretty 0 q
 
 instance Pretty Stmt where
-  pretty p (Bind n args Nothing t)   = pretty 0 n <+> prettyArgs args <+> text "=" <+> pretty 0 t
-  pretty p (Bind n args (Just t') t) = pretty 0 n <+> prettyArgs args <+> text ":" <+> pretty 0 t' <+> text "=" <+> pretty 0 t
+  pretty p (Bind n args t' t) =
+    pretty 0 n <+> prettyArgs args <+>
+           maybe empty (\t' -> text ":" <+> pretty 0 t') t' <+>
+           text "=" <+> pretty 0 t
   pretty p (Term t) = pretty 0 t
   pretty p (Assertion t q' t') = text "assert" <+> prettyAssertion t q' t'
   pretty p (Import n) = text "import" <+> pretty 0 n

From f22fed79b0f85ad6c68a15d7000ddea87f76ac47 Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <p.giarrusso@gmail.com>
Date: Sat, 7 Feb 2015 00:57:44 +0100
Subject: [PATCH 07/18] Prototype postulates (#95)

This is just (the semantics of) Proposal 1 (with a twist), based on the
code for Bind.

No test added yet.
---
 src-lib/PTS/Process/File.hs     | 11 +++++++++++
 src-lib/PTS/Syntax/Statement.hs |  1 +
 2 files changed, 12 insertions(+)

diff --git a/src-lib/PTS/Process/File.hs b/src-lib/PTS/Process/File.hs
index da311d6..5b7fc1b 100644
--- a/src-lib/PTS/Process/File.hs
+++ b/src-lib/PTS/Process/File.hs
@@ -195,6 +195,17 @@ processStmt (Bind n args typeAnnot body) = recover () $ do
           Nothing -> ResidualVar n
   putBindings ((n, Binding False v tType (Just tSort)) : env)
 
+processStmt (Postulate n typ) = recover () $ do
+  -- XXX Looks like a variant of Bind, maybe it should be?
+  env <- getBindings
+  (typ, s) <- flip runEnvironmentT env $ do
+    typ <- typecheckPull typ
+    s <- checkProperType typ (text "in top-level binding of " <+> pretty 0 n) (text "")
+    typ <- liftEval (eval typ)
+    return (typ, s)
+  let v = ResidualVar n
+  putBindings ((n, Binding False v typ (Just s)) : env)
+
 processStmt (Assertion t q' t') = recover () $ assert (showAssertion t q' t') $ do
   output (text "")
   output (text "process assertion")
diff --git a/src-lib/PTS/Syntax/Statement.hs b/src-lib/PTS/Syntax/Statement.hs
index b847be8..8b590e1 100644
--- a/src-lib/PTS/Syntax/Statement.hs
+++ b/src-lib/PTS/Syntax/Statement.hs
@@ -14,3 +14,4 @@ data Stmt
   | Import ModuleName
   | StmtPos Position Stmt
   | Assertion Term (Maybe Term) (Maybe Term)
+  | Postulate Name Term

From 5d34f40ade5021001cbfa3304654a11be76055a0 Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <p.giarrusso@gmail.com>
Date: Sat, 7 Feb 2015 01:38:10 +0100
Subject: [PATCH 08/18] Turn Postulates into bodyless Binding (#95)

---
 src-lib/PTS/Process/File.hs     | 43 +++++++++++++++------------------
 src-lib/PTS/Syntax/Parser.hs    |  2 +-
 src-lib/PTS/Syntax/Pretty.hs    |  2 +-
 src-lib/PTS/Syntax/Statement.hs |  3 +--
 4 files changed, 23 insertions(+), 27 deletions(-)

diff --git a/src-lib/PTS/Process/File.hs b/src-lib/PTS/Process/File.hs
index 5b7fc1b..2f6c9c0 100644
--- a/src-lib/PTS/Process/File.hs
+++ b/src-lib/PTS/Process/File.hs
@@ -13,6 +13,7 @@ import Control.Monad.State (MonadState, get, put, evalStateT)
 import Control.Monad.Trans (MonadIO (liftIO))
 import Control.Monad.Log (MonadLog, runConsoleLogT)
 
+import Data.Traversable (traverse)
 import Data.Maybe (fromMaybe)
 import Data.Monoid (mempty)
 import qualified Data.Map as Map
@@ -121,7 +122,7 @@ liftEval action = do
   env <- getBindings
   return (runEval env action)
 
-processFile :: (Functor m, MonadErrors [PTSError] m, MonadReader Options m, MonadState ProcessingState m, MonadIO m, MonadLog m, MonadAssertions m) => FilePath -> m (Maybe (Module Eval))
+processFile :: (Functor m, MonadErrors [PTSError] m, MonadReader Options m, MonadState ProcessingState m, MonadIO m, MonadLog m, MonadAssertions m, Applicative m) => FilePath -> m (Maybe (Module Eval))
 processFile file = do
   (maybeName, rest) <- processFileInt file
   return $ filterRet <$> maybeName <*> pure rest
@@ -149,14 +150,17 @@ processStmt (Term t) = recover () $ do
   output (nest 2 (sep [text "value:", nest 2 (pretty 0 x)]))
 
 processStmt (Bind n args typeAnnot body) = recover () $ do
-  let t = foldTelescope mkLam args body
+  let t = foldTelescope mkLam args <$> body
   pts <- getLanguage
   output (text "")
   output (text "process binding of" <+> pretty 0 n)
 
   -- preprocess body
-  output (nest 2 (sep [text "original term:", nest 2 (pretty 0 t)]))
-  whenOption optShowFullTerms $ output (nest 2 (sep [text "full term", nest 2 (pretty 0 t)]))
+  flip traverse t $
+    \t ->
+      do
+        output (nest 2 (sep [text "original term:", nest 2 (pretty 0 t)]))
+        whenOption optShowFullTerms $ output (nest 2 (sep [text "full term", nest 2 (pretty 0 t)]))
 
   env <- getBindings
   let checkTopLevel typ =
@@ -170,23 +174,27 @@ processStmt (Bind n args typeAnnot body) = recover () $ do
       -- preprocess type
       let t' = foldTelescope mkPi args body'
       output (nest 2 (sep [text "specified type:", nest 2 (pretty 0 t')]))
-      whenOption optShowFullTerms $ output (nest 2 (sep [text "full type", nest 2 (pretty 0 t' )]))
+      whenOption optShowFullTerms $ output (nest 2 (sep [text "full type", nest 2 (pretty 0 t')]))
 
       -- typecheck type
       (qq, s) <- checkTopLevel t'
 
       -- use declared type to typecheck push
       qq <- liftEval (eval qq)
-      t <- recover Nothing $ runEnvironmentT (Just <$> typecheckPush t qq) env
+      t <- recover Nothing $ runEnvironmentT (traverse (flip typecheckPush qq) t) env
       return (t, qq, s)
     Nothing -> do
       -- typecheck pull
-      t <- runEnvironmentT (typecheckPull t) env
-      q <- liftEval (reify (typeOf t))
-      (_, s) <- checkTopLevel q
-
-      output (nest 2 (sep [text "type:", nest 2 (pretty 0 q)]))
-      return (Just t, typeOf t, s)
+      case t of
+        Just t -> do
+          t <- runEnvironmentT (typecheckPull t) env
+          q <- liftEval (reify (typeOf t))
+          (_, s) <- checkTopLevel q
+
+          output (nest 2 (sep [text "type:", nest 2 (pretty 0 q)]))
+          return (Just t, typeOf t, s)
+        Nothing ->
+          prettyFail $ text "Binding for " <+> pretty 0 n <+> text "specifies neither type nor body."
 
   -- do binding
   let v =
@@ -195,17 +203,6 @@ processStmt (Bind n args typeAnnot body) = recover () $ do
           Nothing -> ResidualVar n
   putBindings ((n, Binding False v tType (Just tSort)) : env)
 
-processStmt (Postulate n typ) = recover () $ do
-  -- XXX Looks like a variant of Bind, maybe it should be?
-  env <- getBindings
-  (typ, s) <- flip runEnvironmentT env $ do
-    typ <- typecheckPull typ
-    s <- checkProperType typ (text "in top-level binding of " <+> pretty 0 n) (text "")
-    typ <- liftEval (eval typ)
-    return (typ, s)
-  let v = ResidualVar n
-  putBindings ((n, Binding False v typ (Just s)) : env)
-
 processStmt (Assertion t q' t') = recover () $ assert (showAssertion t q' t') $ do
   output (text "")
   output (text "process assertion")
diff --git a/src-lib/PTS/Syntax/Parser.hs b/src-lib/PTS/Syntax/Parser.hs
index 4c2555c..462aa78 100644
--- a/src-lib/PTS/Syntax/Parser.hs
+++ b/src-lib/PTS/Syntax/Parser.hs
@@ -113,7 +113,7 @@ stmt = withPos StmtPos $ asum
   , Import <$> (keyword "import" *> modname <* semi)
   , Assertion <$> (keyword "assert" *> expr) <*> optionMaybe (colon1 *> expr) <*> optionMaybe (assign *> expr) <* semi
   , try (Term <$> expr <* semi)
-  , Bind <$> ident <*> telescope <*> optionMaybe (colon1 *> expr) <* assign <*> expr <* semi]
+  , Bind <$> ident <*> telescope <*> optionMaybe (colon1 *> expr) <* assign <*> (Just <$> expr) <* semi]
 
 stmts = many (optional pragma *> stmt)
 
diff --git a/src-lib/PTS/Syntax/Pretty.hs b/src-lib/PTS/Syntax/Pretty.hs
index c651f29..04f3b2e 100644
--- a/src-lib/PTS/Syntax/Pretty.hs
+++ b/src-lib/PTS/Syntax/Pretty.hs
@@ -166,7 +166,7 @@ instance Pretty Stmt where
   pretty p (Bind n args t' t) =
     pretty 0 n <+> prettyArgs args <+>
            maybe empty (\t' -> text ":" <+> pretty 0 t') t' <+>
-           text "=" <+> pretty 0 t
+           maybe empty (\t -> text "=" <+> pretty 0 t) t
   pretty p (Term t) = pretty 0 t
   pretty p (Assertion t q' t') = text "assert" <+> prettyAssertion t q' t'
   pretty p (Import n) = text "import" <+> pretty 0 n
diff --git a/src-lib/PTS/Syntax/Statement.hs b/src-lib/PTS/Syntax/Statement.hs
index 8b590e1..ff8d872 100644
--- a/src-lib/PTS/Syntax/Statement.hs
+++ b/src-lib/PTS/Syntax/Statement.hs
@@ -8,10 +8,9 @@ import PTS.Syntax.Telescope (Telescope)
 import PTS.Syntax.Term (Term)
 
 data Stmt
-  = Bind Name (Telescope Term) (Maybe Term) Term
+  = Bind Name (Telescope Term) (Maybe Term) (Maybe Term)
   | Term Term
   | Export Name
   | Import ModuleName
   | StmtPos Position Stmt
   | Assertion Term (Maybe Term) (Maybe Term)
-  | Postulate Name Term

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 09/18] 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` ".:=;/()[]$"
 

From 60664e915769e0d08adf947fd0bbeab8cd1b624b Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <p.giarrusso@gmail.com>
Date: Sun, 8 Feb 2015 19:58:25 +0100
Subject: [PATCH 10/18] Support telescopes for postulates

That's convenient when refactoring a binding to a postulate, and since
postulates reuse code for bindings, it's also trivial to support.

For instance, now we can turn:

> cons1 (A B : *) : A -> B -> Pair1 A B = ...;

into:

> postulate cons1 (A B : *) : A -> B -> Pair1 A B;
---
 src-lib/PTS/Syntax/Parser.hs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src-lib/PTS/Syntax/Parser.hs b/src-lib/PTS/Syntax/Parser.hs
index 226724d..43968d5 100644
--- a/src-lib/PTS/Syntax/Parser.hs
+++ b/src-lib/PTS/Syntax/Parser.hs
@@ -113,7 +113,7 @@ stmt = withPos StmtPos $ asum
   , 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
+  , Bind <$> (keyword "postulate" *> ident) <*> telescope <*> (colon1 *> (Just <$> expr)) <*> pure Nothing <* semi
   , try (Term <$> expr <* semi)
   , Bind <$> ident <*> telescope <*> optionMaybe (colon1 *> expr) <* assign <*> (Just <$> expr) <* semi]
 

From 59a0613f5ace1ce56eb4c9c555ddafa989334cd7 Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <p.giarrusso@gmail.com>
Date: Sun, 8 Feb 2015 20:12:16 +0100
Subject: [PATCH 11/18] Add example/testcase/doc for postulates

---
 examples/Pair1WithPostulates.lpts | 44 +++++++++++++++++++++++++++++++
 pts.cabal                         |  1 +
 src-test/tests.hs                 |  1 +
 3 files changed, 46 insertions(+)
 create mode 100644 examples/Pair1WithPostulates.lpts

diff --git a/examples/Pair1WithPostulates.lpts b/examples/Pair1WithPostulates.lpts
new file mode 100644
index 0000000..19d9cdb
--- /dev/null
+++ b/examples/Pair1WithPostulates.lpts
@@ -0,0 +1,44 @@
+> language fomega;
+> module Data.Pair1;
+
+Pairs on the expression level. Requires at least System F. Since Pair is an
+in-language type constructor, not a macro, we actually require Fomega.
+
+> Pair1 (A B : *) : * = Pi R : * . (A -> B -> R) -> R;
+
+To test postulates, here we postulate cons1:
+
+> postulate cons1 (A B : *) : A -> B -> Pair1 A B;
+
+even though it's easy to define it:
+
+> cons1impl (A B : *) : A -> B -> Pair1 A B = lambda a b R k . k a b;
+
+Notice how postulates admit telescopes -- we don't have to desugar them by hand:
+
+> postulate cons1 : Pi (A B : *). A -> B -> Pair1 A B;
+> assert cons1 : Pi  (A B : *) . A -> B -> Pair1 A B;
+
+> fst1 (A B : *) : Pair1 A B -> A = lambda p . p A (lambda a b . a);
+> snd1 (A B : *) : Pair1 A B -> B = lambda p . p B (lambda a b . b);
+>
+> pair1 (A B C D : *) : (A -> B) -> (C -> D) -> (Pair1 A C -> Pair1 B D) =
+>   lambda f g p . cons1 B D (f (fst1 A C p)) (g (snd1 A C p));
+>
+> both1 (A B C : *) : (A -> B) -> (A -> C) -> (A -> Pair1 B C) =
+>   lambda f g a . cons1 B C (f a) (g a);
+>
+> curry1 (A B C : *) : (Pair1 A B -> C) -> (A -> B -> C) =
+>   lambda f a b . f (cons1 A B a b);
+>
+> uncurry1 (A B C : *) : (A -> B -> C) -> (Pair1 A B -> C) =
+>   lambda f p . f (fst1 A B p) (snd1 A B p);
+>
+> export Pair1;
+> export cons1;
+> export fst1;
+> export snd1;
+> export pair1;
+> export both1;
+> export curry1;
+> export uncurry1;
diff --git a/pts.cabal b/pts.cabal
index d66fe8a..0ddd1a5 100644
--- a/pts.cabal
+++ b/pts.cabal
@@ -14,6 +14,7 @@ Extra-source-files:  examples/Arithmetics.lpts
                      examples/Functions.lpts
                      examples/Inference.lpts
                      examples/Syntax.lpts
+                     examples/Pair1WithPostulates.lpts
 Data-files:          emacs/pts-mode.el
 Cabal-version:       >= 1.8
 
diff --git a/src-test/tests.hs b/src-test/tests.hs
index 38bbf72..a568166 100644
--- a/src-test/tests.hs
+++ b/src-test/tests.hs
@@ -21,5 +21,6 @@ tests =
   ,  testFile True ["examples"] "ChurchNumbers.lpts"
   ,  testFile True ["examples"] "Functions.lpts"
   ,  testFile True ["examples"] "Inference.lpts"
+  ,  testFile True ["examples"] "Pair1WithPostulates.lpts"
   ,  testFile True ["examples"] "Syntax.lpts"
   ]

From f729dc818c089c31e41dfb5fce8814c73f7c24d6 Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <p.giarrusso@gmail.com>
Date: Sun, 8 Feb 2015 21:59:42 +0100
Subject: [PATCH 12/18] Support cabal repl tests

Add filepath explicitly for the tests as well (even though elsewhere
it's implied by the pts library).
---
 pts.cabal | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/pts.cabal b/pts.cabal
index 0ddd1a5..fdcd242 100644
--- a/pts.cabal
+++ b/pts.cabal
@@ -141,5 +141,6 @@ Test-suite tests
                        HUnit,
                        parsec == 3.1.*,
                        pts,
-                       directory >= 1.2.0.1 && < 1.3
+                       directory >= 1.2.0.1 && < 1.3,
+                       filepath
   -- Ghc-options: -Wall -fno-warn-orphans

From c5bd99c9cafe76a7238c8b1e1acab29ad8a4a908 Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <p.giarrusso@gmail.com>
Date: Sun, 8 Feb 2015 22:12:48 +0100
Subject: [PATCH 13/18] Add assertion to Syntax.lpts

Files are shown in testing output only if they contain assertions (which
seems unfortunate), so add some now.
---
 examples/Syntax.lpts | 1 +
 1 file changed, 1 insertion(+)

diff --git a/examples/Syntax.lpts b/examples/Syntax.lpts
index 892a4d2..18b718b 100644
--- a/examples/Syntax.lpts
+++ b/examples/Syntax.lpts
@@ -4,3 +4,4 @@
 > bar =
 >	2;
 > baz = 3;
+> assert add bar baz = 5;

From eca9624e8bdb4c89e49cd2bb6fd131372fca706b Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <p.giarrusso@gmail.com>
Date: Sun, 8 Feb 2015 22:16:22 +0100
Subject: [PATCH 14/18] Test automatically all files under examples/

---
 src-test/PTS/File/Tests.hs | 19 ++++++++++++++++++-
 src-test/tests.hs          | 22 +++++++++-------------
 2 files changed, 27 insertions(+), 14 deletions(-)

diff --git a/src-test/PTS/File/Tests.hs b/src-test/PTS/File/Tests.hs
index 0c159eb..d259ed9 100644
--- a/src-test/PTS/File/Tests.hs
+++ b/src-test/PTS/File/Tests.hs
@@ -1,6 +1,7 @@
 module PTS.File.Tests
   ( testFile
   , testFileWithOptions
+  , testDir
   ) where
 
 import Control.Monad.Assertions (collectAssertions)
@@ -13,7 +14,8 @@ import PTS.Process.File (processFile)
 import PTS.Process.Main (runOptMonads, withEmptyState)
 import PTS.Options (Options, defaultOptions, optPath, optLiterate, optQuiet)
 
-import System.Directory (findFile)
+import System.Directory (findFile, getDirectoryContents)
+import System.FilePath (takeExtension)
 
 import Test.Framework (Test, testGroup, buildTest)
 import Test.Framework.Providers.HUnit (testCase)
@@ -38,3 +40,18 @@ testFile literate path
       { optQuiet = True
       , optLiterate = literate
       , optPath = path})
+
+testDir :: FilePath -> IO [Test]
+testDir path = do
+  files <- getDirectoryContents path
+  return $
+           [ testFile literate [path] validFile |
+             file <- files,
+             (validFile, literate) <-
+               case takeExtension file of
+                 ".lpts" ->
+                   [(file, True)]
+                 ".pts" ->
+                   [(file, False)]
+                 _ -> []
+           ]
diff --git a/src-test/tests.hs b/src-test/tests.hs
index a568166..4e5e91d 100644
--- a/src-test/tests.hs
+++ b/src-test/tests.hs
@@ -9,18 +9,14 @@ import Test.QuickCheck hiding ((.&.))
 import PTS.Syntax.Substitution.Tests
 import PTS.Syntax.Parser.Tests
 import PTS.Syntax.Pretty.Tests
-import PTS.File.Tests (testFile)
+import PTS.File.Tests (testFile, testDir)
 
-main = defaultMain Main.tests
+main = Main.tests >>= defaultMain
 
-tests =
-  [  PTS.Syntax.Parser.Tests.tests
-  ,  PTS.Syntax.Pretty.Tests.tests
-  ,  PTS.Syntax.Substitution.Tests.tests
-  ,  testFile True ["examples"] "Arithmetics.lpts"
-  ,  testFile True ["examples"] "ChurchNumbers.lpts"
-  ,  testFile True ["examples"] "Functions.lpts"
-  ,  testFile True ["examples"] "Inference.lpts"
-  ,  testFile True ["examples"] "Pair1WithPostulates.lpts"
-  ,  testFile True ["examples"] "Syntax.lpts"
-  ]
+tests = do
+  examples <- testDir "examples"
+  return $
+        [  PTS.Syntax.Parser.Tests.tests
+        ,  PTS.Syntax.Pretty.Tests.tests
+        ,  PTS.Syntax.Substitution.Tests.tests
+        ] ++ examples

From 41585ddd1b1493e3df9fce3ea2954bca893bc6eb Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <p.giarrusso@gmail.com>
Date: Tue, 10 Feb 2015 12:45:18 +0100
Subject: [PATCH 15/18] Coding changes on
 5d34f40ade5021001cbfa3304654a11be76055a0

As suggested in
https://github.com/Blaisorblade/pts/commit/5d34f40ade5021001cbfa3304654a11be76055a0

Reindenting/renaming deferred.
---
 src-lib/PTS/Process/File.hs | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src-lib/PTS/Process/File.hs b/src-lib/PTS/Process/File.hs
index 2f6c9c0..e20df94 100644
--- a/src-lib/PTS/Process/File.hs
+++ b/src-lib/PTS/Process/File.hs
@@ -122,7 +122,7 @@ liftEval action = do
   env <- getBindings
   return (runEval env action)
 
-processFile :: (Functor m, MonadErrors [PTSError] m, MonadReader Options m, MonadState ProcessingState m, MonadIO m, MonadLog m, MonadAssertions m, Applicative m) => FilePath -> m (Maybe (Module Eval))
+processFile :: (Functor m, Applicative m, MonadErrors [PTSError] m, MonadReader Options m, MonadState ProcessingState m, MonadIO m, MonadLog m, MonadAssertions m) => FilePath -> m (Maybe (Module Eval))
 processFile file = do
   (maybeName, rest) <- processFileInt file
   return $ filterRet <$> maybeName <*> pure rest
@@ -156,7 +156,7 @@ processStmt (Bind n args typeAnnot body) = recover () $ do
   output (text "process binding of" <+> pretty 0 n)
 
   -- preprocess body
-  flip traverse t $
+  for t $
     \t ->
       do
         output (nest 2 (sep [text "original term:", nest 2 (pretty 0 t)]))

From 68e8a04ecbb6fc4c332f3bafdfc49c6073873dec Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <p.giarrusso@gmail.com>
Date: Tue, 10 Feb 2015 12:58:14 +0100
Subject: [PATCH 16/18] Reindent/rename (follow up to previous commit)

---
 src-lib/PTS/Process/File.hs | 19 +++++++++----------
 1 file changed, 9 insertions(+), 10 deletions(-)

diff --git a/src-lib/PTS/Process/File.hs b/src-lib/PTS/Process/File.hs
index e20df94..8225444 100644
--- a/src-lib/PTS/Process/File.hs
+++ b/src-lib/PTS/Process/File.hs
@@ -13,7 +13,7 @@ import Control.Monad.State (MonadState, get, put, evalStateT)
 import Control.Monad.Trans (MonadIO (liftIO))
 import Control.Monad.Log (MonadLog, runConsoleLogT)
 
-import Data.Traversable (traverse)
+import Data.Traversable (traverse, for)
 import Data.Maybe (fromMaybe)
 import Data.Monoid (mempty)
 import qualified Data.Map as Map
@@ -150,17 +150,16 @@ processStmt (Term t) = recover () $ do
   output (nest 2 (sep [text "value:", nest 2 (pretty 0 x)]))
 
 processStmt (Bind n args typeAnnot body) = recover () $ do
-  let t = foldTelescope mkLam args <$> body
+  let maybeT = foldTelescope mkLam args <$> body
   pts <- getLanguage
   output (text "")
   output (text "process binding of" <+> pretty 0 n)
 
   -- preprocess body
-  for t $
-    \t ->
-      do
-        output (nest 2 (sep [text "original term:", nest 2 (pretty 0 t)]))
-        whenOption optShowFullTerms $ output (nest 2 (sep [text "full term", nest 2 (pretty 0 t)]))
+
+  for maybeT $ \t -> do
+    output (nest 2 (sep [text "original term:", nest 2 (pretty 0 t)]))
+    whenOption optShowFullTerms $ output (nest 2 (sep [text "full term", nest 2 (pretty 0 t)]))
 
   env <- getBindings
   let checkTopLevel typ =
@@ -181,11 +180,11 @@ processStmt (Bind n args typeAnnot body) = recover () $ do
 
       -- use declared type to typecheck push
       qq <- liftEval (eval qq)
-      t <- recover Nothing $ runEnvironmentT (traverse (flip typecheckPush qq) t) env
-      return (t, qq, s)
+      maybeT <- recover Nothing $ runEnvironmentT (traverse (flip typecheckPush qq) maybeT) env
+      return (maybeT, qq, s)
     Nothing -> do
       -- typecheck pull
-      case t of
+      case maybeT of
         Just t -> do
           t <- runEnvironmentT (typecheckPull t) env
           q <- liftEval (reify (typeOf t))

From e0506704a15cf011b792f35c8717732d254ff662 Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <p.giarrusso@gmail.com>
Date: Tue, 10 Feb 2015 13:30:07 +0100
Subject: [PATCH 17/18] Revise example

In response to
https://github.com/Blaisorblade/pts/commit/59a0613f5ace1ce56eb4c9c555ddafa989334cd7#commitcomment-9673662
---
 examples/Pair1WithPostulates.lpts | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

diff --git a/examples/Pair1WithPostulates.lpts b/examples/Pair1WithPostulates.lpts
index 19d9cdb..25cf65d 100644
--- a/examples/Pair1WithPostulates.lpts
+++ b/examples/Pair1WithPostulates.lpts
@@ -14,10 +14,11 @@ even though it's easy to define it:
 
 > cons1impl (A B : *) : A -> B -> Pair1 A B = lambda a b R k . k a b;
 
-Notice how postulates admit telescopes -- we don't have to desugar them by hand:
+Notice how postulates admit telescopes, which are desugared to Pi-types:
+
+> assert cons1 : Pi (A B : *) . A -> B -> Pair1 A B;
+
 
-> postulate cons1 : Pi (A B : *). A -> B -> Pair1 A B;
-> assert cons1 : Pi  (A B : *) . A -> B -> Pair1 A B;
 
 > fst1 (A B : *) : Pair1 A B -> A = lambda p . p A (lambda a b . a);
 > snd1 (A B : *) : Pair1 A B -> B = lambda p . p B (lambda a b . b);

From 2fa8f0868350a92750585a74e8bff1b4fc508244 Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <p.giarrusso@gmail.com>
Date: Tue, 10 Feb 2015 14:16:11 +0100
Subject: [PATCH 18/18] Update keyword list in pts-mode.el

As requested in
https://github.com/Blaisorblade/pts/commit/3d98ef51b6d719256c9cff85bab6aac4e19dcac0
---
 emacs/pts-mode.el            | 2 +-
 src-lib/PTS/Syntax/Parser.hs | 1 +
 2 files changed, 2 insertions(+), 1 deletion(-)

diff --git a/emacs/pts-mode.el b/emacs/pts-mode.el
index bec82bb..b991f7d 100644
--- a/emacs/pts-mode.el
+++ b/emacs/pts-mode.el
@@ -1,5 +1,5 @@
 (defvar pts-keywords
-  '("language" "module" "import" "export" "assert"
+  '("language" "module" "import" "export" "postulate" "assert"
     "Lambda" "lambda" "Pi" "->"
     "if0" "then" "else")
   "Keywords of PTS, that is, reserved words with special
diff --git a/src-lib/PTS/Syntax/Parser.hs b/src-lib/PTS/Syntax/Parser.hs
index 43968d5..27351d2 100644
--- a/src-lib/PTS/Syntax/Parser.hs
+++ b/src-lib/PTS/Syntax/Parser.hs
@@ -170,6 +170,7 @@ pragma = lexem $ do
     -- LEXER --
      ---------
 
+-- When updating, please also update emacs/pts-mode.el.
 keywords = ["Lambda", "lambda", "Pi", "if0", "then", "else", "->", "add", "mul", "sub", "div", "module", "import", "export", "assert", "language", "postulate", "_("]
 
 identChar x = not (isSpace x) && x `notElem` ".:=;/()[]$"