Create stuck bindings for fun and profit (type errors, postulates)

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

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;

examples/Pair1WithPostulates.lpts

@@ -0,0 +1,45 @@
+> 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, which are desugared to Pi-types:
+
+> 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;

examples/Syntax.lpts

@@ -4,3 +4,4 @@
 > bar =
 >	2;
 > baz = 3;
+> assert add bar baz = 5;

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
 
@@ -140,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

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

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, for)
 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, 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
@@ -149,46 +150,57 @@ 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
-  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 =
+        flip runEnvironmentT env $ do
+          typ <- typecheckPull typ
+          s <- checkProperType typ (text "in top-level binding of " <+> pretty 0 n) (text "")
+          return (typ, s)
 
-  t <- case typeAnnot of
+  (maybeT, tType, tSort) <- case typeAnnot of
     Just body' -> 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 <-
-        flip runEnvironmentT env $
-             do
-               qq <- typecheckPull t'
-               checkProperType qq (text "in top-level binding of " <+> pretty 0 n) (text "")
-               return qq
+      (qq, s) <- checkTopLevel t'
 
       -- use declared type to typecheck push
       qq <- liftEval (eval qq)
-      t <- runEnvironmentT (typecheckPush t qq) env
-      return t
+      maybeT <- recover Nothing $ runEnvironmentT (traverse (flip typecheckPush qq) maybeT) env
+      return (maybeT, qq, 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
+      case maybeT 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 = 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 (Just tSort)) : env)
 
 processStmt (Assertion t q' t') = recover () $ assert (showAssertion t q' t') $ do
   output (text "")

src-lib/PTS/Syntax/Parser.hs

@@ -112,8 +112,10 @@ 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) <*> telescope <*> (colon1 *> (Just <$> expr)) <*> pure Nothing <* 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)
 
@@ -168,7 +170,8 @@ pragma = lexem $ do
     -- LEXER --
      ---------
 
-keywords = ["Lambda", "lambda", "Pi", "if0", "then", "else", "->", "add", "mul", "sub", "div", "module", "import", "export", "assert", "language", "_("]
+-- 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` ".:=;/()[]$"
 

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' <+>
+           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

src-lib/PTS/Syntax/Statement.hs

@@ -8,7 +8,7 @@ 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

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)]
+                 _ -> []
+           ]

src-test/tests.hs

@@ -9,17 +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"] "Syntax.lpts"
-  ]
+tests = do
+  examples <- testDir "examples"
+  return $
+        [  PTS.Syntax.Parser.Tests.tests
+        ,  PTS.Syntax.Pretty.Tests.tests
+        ,  PTS.Syntax.Substitution.Tests.tests
+        ] ++ examples