Merge pull request #9 from fizruk/fix-doctests

Fix doctests

.gitattributes

@@ -1,4 +1 @@
-haskell/free-foil/src/Language/LambdaPi/Syntax/Abs.hs linguist-generated=true
-haskell/free-foil/src/Language/LambdaPi/Syntax/Doc.txt linguist-generated=true
-haskell/free-foil/src/Language/LambdaPi/Syntax/Layout.hs linguist-generated=true
-haskell/free-foil/src/Language/LambdaPi/Syntax/Layout.hs linguist-generated=true
+haskell/free-foil/src/Language/LambdaPi/Syntax/* linguist-generated=true

.gitignore

@@ -1,6 +1,9 @@
-haskell/free-foil/src/Language/**/Test.hs
-haskell/free-foil/src/Language/**/Skel.hs
-haskell/free-foil/src/Language/**/ErrM.hs
+haskell/free-foil/src/Language/LambdaPi/Syntax/Lex.hs
+haskell/free-foil/src/Language/LambdaPi/Syntax/Par.hs
+haskell/free-foil/src/Language/LambdaPi/Syntax/Test
+haskell/free-foil/src/Language/LambdaPi/Syntax/Test.hs
+haskell/free-foil/src/Language/LambdaPi/Syntax/Skel.hs
+haskell/free-foil/src/Language/LambdaPi/Syntax/ErrM.hs
 
 scala/free-foil/src/main/scala/.scala-build/
 

haskell/free-foil/Setup.hs

@@ -1,32 +1,59 @@
 {-# LANGUAGE CPP #-}
+{-# LANGUAGE QuasiQuotes #-}
+
 -- Source: https://github.com/haskell/cabal/issues/6726#issuecomment-918663262
 
 -- | Custom Setup that runs bnfc to generate the language sub-libraries
 -- for the parsers included in Ogma.
 module Main (main) where
 
-import           Distribution.Simple         (defaultMainWithHooks,
-                                              hookedPrograms, postConf,
-                                              preBuild, simpleUserHooks)
-import           Distribution.Simple.Program (Program (..), findProgramVersion,
-                                              simpleProgram)
-import           System.Process              (system)
+import Data.List (intercalate)
+import Distribution.Simple (defaultMainWithHooks, hookedPrograms, postConf, preBuild, simpleUserHooks)
+import Distribution.Simple.Program (Program (..), findProgramVersion, simpleProgram)
+import PyF (fmt)
+import System.Exit (ExitCode (..))
+import System.Process (callCommand)
 
--- | Run BNFC on the grammar before the actual build step.
+-- | Run BNFC, happy, and alex on the grammar before the actual build step.
 --
 -- All options for bnfc are hard-coded here.
 main :: IO ()
-main = defaultMainWithHooks $ simpleUserHooks
-  { hookedPrograms = [ bnfcProgram ]
-  , postConf       = \args flags packageDesc localBuildInfo -> do
-#ifndef mingw32_HOST_OS
-      _ <- system "bnfc -d -p Language.LambdaPi --generic -o src/ grammar/LambdaPi/Syntax.cf"
+main =
+  defaultMainWithHooks $
+    simpleUserHooks
+      { hookedPrograms = [bnfcProgram]
+      , postConf = \args flags packageDesc localBuildInfo -> do
+          let
+            isWindows =
+#ifdef mingw32_HOST_OS
+                      True
+#else
+                      False
 #endif
-      postConf simpleUserHooks args flags packageDesc localBuildInfo
-  }
+            -- See the details on the command in https://github.com/objectionary/normalizer/issues/347#issuecomment-2117097070
+            command = intercalate "; " $
+                [ "set -ex" ] <>
+                [ "chcp.com" | isWindows ] <>
+                [ "chcp.com 65001" | isWindows ] <>
+                [ "bnfc --haskell -d -p Language.LambdaPi --generic -o src/ grammar/LambdaPi/Syntax.cf"
+                , "cd src/Language/LambdaPi/Syntax"
+                , "alex Lex.x"
+                , "happy Par.y"
+                , "true"
+                ]
+
+            fullCommand = [fmt|bash -c ' {command} '|]
+
+          putStrLn fullCommand
+
+          _ <- callCommand fullCommand
+
+          postConf simpleUserHooks args flags packageDesc localBuildInfo
+      }
 
--- | TODO: This should be in Cabal.Distribution.Simple.Program.Builtin.
+-- | NOTE: This should be in Cabal.Distribution.Simple.Program.Builtin.
 bnfcProgram :: Program
-bnfcProgram = (simpleProgram "bnfc")
-  { programFindVersion = findProgramVersion "--version" id
-  }
+bnfcProgram =
+  (simpleProgram "bnfc")
+    { programFindVersion = findProgramVersion "--version" id
+    }

haskell/free-foil/free-foil.cabal

@@ -29,6 +29,7 @@ source-repository head
 custom-setup
   setup-depends:
       Cabal >=2.4.0.1 && <4.0
+    , PyF
     , base >=4.11.0.0 && <5.0
     , process >=1.6.3.0
 
@@ -96,6 +97,30 @@ executable lambda-pi
     , text >=1.2.3.1
   default-language: Haskell2010
 
+test-suite doctests
+  type: exitcode-stdio-1.0
+  main-is: Main.hs
+  hs-source-dirs:
+      src/
+      test/doctests
+  ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints -optP-Wno-nonportable-include-path
+  build-tools:
+      alex >=3.2.4
+    , happy >=1.19.9
+  build-tool-depends:
+      BNFC:bnfc >=2.9.4.1
+  build-depends:
+      array >=0.5.3.0
+    , base >=4.7 && <5
+    , bifunctors
+    , containers
+    , deepseq
+    , doctest-parallel
+    , free-foil
+    , template-haskell
+    , text >=1.2.3.1
+  default-language: Haskell2010
+
 test-suite free-foil-test
   type: exitcode-stdio-1.0
   main-is: Spec.hs

haskell/free-foil/package.yaml

@@ -24,6 +24,7 @@ custom-setup:
     base: ">= 4.11.0.0 && < 5.0"
     Cabal: ">= 2.4.0.1 && < 4.0"
     process: ">= 1.6.3.0"
+    PyF:
 
 build-tools:
   alex: ">= 3.2.4"
@@ -82,18 +83,18 @@ tests:
     dependencies:
       - free-foil
 
-  # doctests:
-  #   source-dirs:
-  #     - src/
-  #     - test/doctests
-  #   main: Main.hs
-  #   other-modules: []
-  #   dependencies:
-  #     - free-foil
-  #     - doctest-parallel
-  #   when:
-  #     - condition: false
-  #       other-modules:
-  #         - Language.LambdaPi.Syntax.Test
-  #         - Language.LambdaPi.Syntax.ErrM
-  #         - Language.LambdaPi.Syntax.Skel
+  doctests:
+    source-dirs:
+      - src/
+      - test/doctests
+    main: Main.hs
+    other-modules: []
+    dependencies:
+      - free-foil
+      - doctest-parallel
+    when:
+      - condition: false
+        other-modules:
+          - Language.LambdaPi.Syntax.Test
+          - Language.LambdaPi.Syntax.ErrM
+          - Language.LambdaPi.Syntax.Skel

haskell/free-foil/src/Control/Monad/Foil/Example.hs

@@ -10,6 +10,9 @@ import           Control.DeepSeq
 import           Control.Monad.Foil
 import           Control.Monad.Foil.Relative
 
+-- $setup
+-- >>> import Control.Monad.Foil
+
 -- | Untyped \(\lambda\)-terms in scope @n@.
 data Expr n where
   -- | Variables are names in scope @n@: \(x\)

haskell/free-foil/src/Control/Monad/Free/Foil/Example.hs

@@ -13,6 +13,9 @@ import           Control.Monad.Foil
 import           Control.Monad.Free.Foil
 import           Data.Bifunctor.TH
 
+-- $setup
+-- >>> import Control.Monad.Foil
+
 -- | Untyped \(\lambda\)-terms in scope @n@.
 data ExprF scope term
   -- | Application of one term to another: \((t_1, t_2)\)

haskell/free-foil/src/Language/LambdaPi/Impl/Foil.hs

@@ -9,7 +9,6 @@
 {-# LANGUAGE QuantifiedConstraints #-}
 {-# LANGUAGE RankNTypes            #-}
 {-# LANGUAGE ScopedTypeVariables   #-}
-{-# LANGUAGE StandaloneDeriving    #-}
 {-# LANGUAGE UndecidableInstances  #-}
 -- | Foil implementation of the \(\lambda\Pi\)-calculus (with pairs).
 --
@@ -65,6 +64,9 @@ data Expr n where
   -- | Universe (type of types): \(\mathcal{U}\)
   UniverseE :: Expr n
 
+instance Show (Expr VoidS) where
+  show = ppExpr
+
 -- | Patterns.
 data Pattern n l where
   -- | Wildcard pattern: \(_\)
@@ -96,14 +98,14 @@ ppName name = "x" <> show (nameId name)
 
 -- | Pretty-print a \(\lambda\Pi\)-term directly (without converting to raw term).
 --
--- >>> putStrLn $ ppExpr identity
--- λx1. x1
--- >>> putStrLn $ ppExpr two
--- λx1. λx2. x1(x1(x2))
+-- >>> ppExpr identity
+-- "\955x0. x0"
+-- >>> ppExpr (churchN 2)
+-- "\955x0. \955x1. x0 (x0 (x1))"
 ppExpr :: Expr n -> String
 ppExpr = \case
   VarE name     -> ppName name
-  AppE e1 e2    -> ppExpr e1 ++ "(" ++ ppExpr e2 ++ ")"
+  AppE e1 e2    -> ppExpr e1 ++ " (" ++ ppExpr e2 ++ ")"
   LamE pat body -> "λ" ++ ppPattern pat ++ ". " ++ ppExpr body
   PiE pat a b -> "Π" ++ "(" ++ ppPattern pat ++ " : " ++ ppExpr a ++ "), " ++ ppExpr b
   PairE l r -> "(" ++ ppExpr l ++ "," ++ ppExpr r ++ ")"
@@ -342,3 +344,32 @@ defaultMain = do
       putStrLn err
       exitFailure
     Right program -> interpretProgram program
+
+-- | A helper for constructing \(\lambda\)-abstractions.
+lam :: Distinct n => Scope n -> (forall l. DExt n l => Scope l -> NameBinder n l -> Expr l) -> Expr n
+lam scope mkBody = withFresh scope $ \x ->
+  let scope' = extendScope x scope
+   in LamE (PatternVar x) (mkBody scope' x)
+
+-- | An identity function as a \(\lambda\)-term:
+--
+-- >>> identity
+-- λx0. x0
+identity :: Expr VoidS
+identity = lam emptyScope $ \_ nx ->
+  VarE (nameOf nx)
+
+-- | Church-encoding of a natural number \(n\).
+--
+-- >>> churchN 0
+-- λx0. λx1. x1
+--
+-- >>> churchN 3
+-- λx0. λx1. x0 (x0 (x0 (x1)))
+churchN :: Int -> Expr VoidS
+churchN n =
+  lam emptyScope $ \sx nx ->
+    lam sx $ \_sxy ny ->
+      let x = sink (VarE (nameOf nx))
+          y = VarE (nameOf ny)
+       in iterate (AppE x) y !! n

haskell/free-foil/src/Language/LambdaPi/Impl/FreeFoil.hs

@@ -1,12 +1,12 @@
-{-# LANGUAGE DataKinds       #-}
-{-# LANGUAGE TypeOperators       #-}
-{-# LANGUAGE TypeSynonymInstances       #-}
-{-# LANGUAGE FlexibleInstances       #-}
-{-# LANGUAGE DeriveFunctor   #-}
-{-# LANGUAGE GADTs           #-}
-{-# LANGUAGE LambdaCase      #-}
-{-# LANGUAGE PatternSynonyms #-}
-{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE DataKinds            #-}
+{-# LANGUAGE DeriveFunctor        #-}
+{-# LANGUAGE FlexibleInstances    #-}
+{-# LANGUAGE GADTs                #-}
+{-# LANGUAGE LambdaCase           #-}
+{-# LANGUAGE PatternSynonyms      #-}
+{-# LANGUAGE TemplateHaskell      #-}
+{-# LANGUAGE TypeOperators        #-}
+{-# LANGUAGE TypeSynonymInstances #-}
 -- | Free foil implementation of the \(\lambda\Pi\)-calculus (with pairs).
 --
 -- Free foil provides the following:
@@ -25,19 +25,23 @@
 -- so only wildcard patterns and variable patterns are handled in this implementation.
 module Language.LambdaPi.Impl.FreeFoil where
 
-import Data.String (IsString(..))
 import qualified Control.Monad.Foil              as Foil
 import           Control.Monad.Free.Foil
 import           Data.Bifunctor.TH
 import           Data.Map                        (Map)
 import qualified Data.Map                        as Map
+import           Data.String                     (IsString (..))
 import qualified Language.LambdaPi.Syntax.Abs    as Raw
 import qualified Language.LambdaPi.Syntax.Layout as Raw
 import qualified Language.LambdaPi.Syntax.Lex    as Raw
 import qualified Language.LambdaPi.Syntax.Par    as Raw
 import qualified Language.LambdaPi.Syntax.Print  as Raw
 import           System.Exit                     (exitFailure)
 
+-- $setup
+-- >>> import qualified Control.Monad.Foil as Foil
+-- >>> :set -XOverloadedStrings
+
 -- | The signature 'Bifunctor' for the \(\lambda\Pi\).
 data LambdaPiF scope term
   = AppF term term        -- ^ Application: \((t_1 \; t_2)\)
@@ -121,11 +125,11 @@ whnf scope = \case
   First t ->
     case whnf scope t of
       Pair l _r -> whnf scope l
-      t' -> First t'
+      t'        -> First t'
   Second t ->
     case whnf scope t of
       Pair _l r -> whnf scope r
-      t' -> Second t'
+      t'        -> Second t'
   t -> t
 
 -- | Convert a raw \(\lambda\)-abstraction into a scope-safe \(\lambda\Pi\)-term.