From a7c2ff46856cd6250cdbf3e2a21b817a9c97e9ea Mon Sep 17 00:00:00 2001 From: Nikolai Kudasov Date: Fri, 14 Jun 2024 12:01:01 +0300 Subject: [PATCH 1/3] Fix running doctests with alex and happy --- haskell/free-foil/Setup.hs | 63 ++++++++++++++++++++++--------- haskell/free-foil/free-foil.cabal | 25 ++++++++++++ haskell/free-foil/package.yaml | 31 +++++++-------- 3 files changed, 86 insertions(+), 33 deletions(-) diff --git a/haskell/free-foil/Setup.hs b/haskell/free-foil/Setup.hs index 251630df..95a44090 100644 --- a/haskell/free-foil/Setup.hs +++ b/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 + } diff --git a/haskell/free-foil/free-foil.cabal b/haskell/free-foil/free-foil.cabal index 4f45fe55..5a741e8d 100644 --- a/haskell/free-foil/free-foil.cabal +++ b/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 diff --git a/haskell/free-foil/package.yaml b/haskell/free-foil/package.yaml index a5c5d352..c1e0ab99 100644 --- a/haskell/free-foil/package.yaml +++ b/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 From 70d6062e3c7eca4b2e9aa56970e0e4dc4e918ef5 Mon Sep 17 00:00:00 2001 From: Nikolai Kudasov Date: Fri, 14 Jun 2024 12:04:24 +0300 Subject: [PATCH 2/3] Update git info regarding generated files --- .gitattributes | 5 +---- .gitignore | 9 ++++++--- 2 files changed, 7 insertions(+), 7 deletions(-) diff --git a/.gitattributes b/.gitattributes index d40799c0..8726c774 100644 --- a/.gitattributes +++ b/.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 diff --git a/.gitignore b/.gitignore index 5266f531..0916e47f 100644 --- a/.gitignore +++ b/.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/ From 7ad97fa70b32a5db164fd712587ec9490d650ef6 Mon Sep 17 00:00:00 2001 From: Nikolai Kudasov Date: Fri, 14 Jun 2024 12:04:39 +0300 Subject: [PATCH 3/3] Fix doctests --- .../src/Control/Monad/Foil/Example.hs | 3 ++ .../src/Control/Monad/Free/Foil/Example.hs | 3 ++ .../src/Language/LambdaPi/Impl/Foil.hs | 43 ++++++++++++++++--- .../src/Language/LambdaPi/Impl/FreeFoil.hs | 28 ++++++------ 4 files changed, 59 insertions(+), 18 deletions(-) diff --git a/haskell/free-foil/src/Control/Monad/Foil/Example.hs b/haskell/free-foil/src/Control/Monad/Foil/Example.hs index 93ec382a..bfae3628 100644 --- a/haskell/free-foil/src/Control/Monad/Foil/Example.hs +++ b/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\) diff --git a/haskell/free-foil/src/Control/Monad/Free/Foil/Example.hs b/haskell/free-foil/src/Control/Monad/Free/Foil/Example.hs index a9c51f4a..82c52f80 100644 --- a/haskell/free-foil/src/Control/Monad/Free/Foil/Example.hs +++ b/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)\) diff --git a/haskell/free-foil/src/Language/LambdaPi/Impl/Foil.hs b/haskell/free-foil/src/Language/LambdaPi/Impl/Foil.hs index 52a32090..3b071b8b 100644 --- a/haskell/free-foil/src/Language/LambdaPi/Impl/Foil.hs +++ b/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 diff --git a/haskell/free-foil/src/Language/LambdaPi/Impl/FreeFoil.hs b/haskell/free-foil/src/Language/LambdaPi/Impl/FreeFoil.hs index c00cb976..db2db446 100644 --- a/haskell/free-foil/src/Language/LambdaPi/Impl/FreeFoil.hs +++ b/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,12 +25,12 @@ -- 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 @@ -38,6 +38,10 @@ 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.