diff --git a/haskell/free-foil/src/Control/Monad/Free/Foil/TH/Convert.hs b/haskell/free-foil/src/Control/Monad/Free/Foil/TH/Convert.hs index 024c5088..e52bb957 100644 --- a/haskell/free-foil/src/Control/Monad/Free/Foil/TH/Convert.hs +++ b/haskell/free-foil/src/Control/Monad/Free/Foil/TH/Convert.hs @@ -8,6 +8,10 @@ import Language.Haskell.TH.Syntax import Control.Monad.Foil.TH.Util +-- * Bulk generators + +-- | Generate helpers for conversion to scope-safe representation. +-- Includes 'mkConvertToSig', 'mkGetPatternBinder', and 'mkGetScopedTerm'. mkConvertToFreeFoil :: Name -- ^ Type name for raw terms. -> Name -- ^ Type name for raw variable identifiers. @@ -20,6 +24,8 @@ mkConvertToFreeFoil termT nameT scopeT patternT = concat <$> sequence , mkGetScopedTerm termT scopeT ] +-- | Generate helpers for conversion from scope-safe representation. +-- Includes 'mkConvertFromSig'. mkConvertFromFreeFoil :: Name -- ^ Type name for raw terms. -> Name -- ^ Type name for raw variable identifiers. @@ -30,6 +36,9 @@ mkConvertFromFreeFoil termT nameT scopeT patternT = concat <$> sequence [ mkConvertFromSig termT nameT scopeT patternT ] +-- * Individual generators + +-- | Generate conversion helper that goes unpeels one node from a raw term. mkConvertToSig :: Name -- ^ Type name for raw terms. -> Name -- ^ Type name for raw variable identifiers. @@ -99,6 +108,7 @@ mkConvertToSig termT nameT scopeT patternT = do , let x = mkName ("x" ++ show i) ] +-- | Generate conversion helper that peels back one node to a raw term. mkConvertFromSig :: Name -- ^ Type name for raw terms. -> Name -- ^ Type name for raw variable identifiers. @@ -158,6 +168,7 @@ mkConvertFromSig termT nameT scopeT patternT = do , let x = mkName ("x" ++ show i) ] +-- | Generate a helper that extracts at most one binder from a pattern. mkGetPatternBinder :: Name -- ^ Type name for raw variable identifiers. -> Name -- ^ Type name for raw patterns. @@ -209,6 +220,7 @@ mkGetPatternBinder nameT patternT = do | (_bang, type_) <- types ] +-- | Generate a helper that extracts a term from a scoped term. mkGetScopedTerm :: Name -- ^ Type name for raw terms. -> Name -- ^ Type name for raw scoped terms. diff --git a/haskell/free-foil/src/Control/Monad/Free/Foil/TH/ZipMatch.hs b/haskell/free-foil/src/Control/Monad/Free/Foil/TH/ZipMatch.hs index dfba2261..2a15ff1c 100644 --- a/haskell/free-foil/src/Control/Monad/Free/Foil/TH/ZipMatch.hs +++ b/haskell/free-foil/src/Control/Monad/Free/Foil/TH/ZipMatch.hs @@ -9,7 +9,7 @@ import Language.Haskell.TH import Control.Monad.Foil.TH.Util import Control.Monad.Free.Foil --- | Generate helpful pattern synonyms given a signature bifunctor. +-- | Generate 'ZipMatch' instance for a given bifunctor. deriveZipMatch :: Name -- ^ Type name for the signature bifunctor. -> Q [Dec] diff --git a/haskell/lambda-pi/src/Language/LambdaPi/Impl/Foil.hs b/haskell/lambda-pi/src/Language/LambdaPi/Impl/Foil.hs index 2ff23239..f3218528 100644 --- a/haskell/lambda-pi/src/Language/LambdaPi/Impl/Foil.hs +++ b/haskell/lambda-pi/src/Language/LambdaPi/Impl/Foil.hs @@ -13,21 +13,23 @@ {-# LANGUAGE UndecidableInstances #-} -- | Foil implementation of the \(\lambda\Pi\)-calculus (with pairs). -- --- The following is implemented manually in this module: +-- The following is implemented __manually__ in this module: -- -- 1. Scope-safe AST for \(\lambda\Pi\)-terms. -- 2. Correct capture-avoiding substitution (see 'substitute'). -- 3. Conversion between scope-safe and raw term representation (the latter is generated via BNFC), see 'toFoilTerm' and 'fromFoilTerm'. -- 4. Helper functions for patterns. See 'extendScopePattern' and 'withRefreshedPattern'. --- 5. Computation of weak head normal form (WHNF) and normal form (NF), see 'whnf' and 'nf'. --- 6. Entry point, gluing everything together. See 'defaultMain'. +-- 5. α-equivalence checks ('alphaEquiv' and 'alphaEquivRefreshed') and α-normalization helpers ('refreshExpr'). +-- 6. Computation of weak head normal form (WHNF) and normal form (NF), see 'whnf' and 'nf'. +-- 7. Entry point, gluing everything together. See 'defaultMain'. -- -- This implementation supports (nested) patterns for pairs. -- -- This is a baseline implementation, see other examples for partial automation: -- --- 1. "Language.LambdaPi.Impl.FreeFoil" allows to define substitution (and, in theory, more complicated algorithms) once for a large class of syntax with binders. +-- 1. "Language.LambdaPi.Impl.FreeFoil" allows to reuse generalized substitution and α-equivalence (and, in theory, more complicated algorithms). -- 2. "Language.LambdaPi.Impl.FoilTH" works well with patterns and generates conversion functions and helpers for patterns. +-- 3. "Language.LambdaPi.Impl.FreeFoilTH" combines the benefits of the above, when it is possible to generate the signature automatically. module Language.LambdaPi.Impl.Foil where import Control.Monad.Foil diff --git a/haskell/lambda-pi/src/Language/LambdaPi/Impl/FoilTH.hs b/haskell/lambda-pi/src/Language/LambdaPi/Impl/FoilTH.hs index e7ac3bef..833d096f 100644 --- a/haskell/lambda-pi/src/Language/LambdaPi/Impl/FoilTH.hs +++ b/haskell/lambda-pi/src/Language/LambdaPi/Impl/FoilTH.hs @@ -18,18 +18,22 @@ -- | Foil implementation of the \(\lambda\Pi\)-calculus (with pairs) -- using Template Haskell to reduce boilerplate. -- --- Template Haskell generation provides the following: +-- Template Haskell helpers __generate__ the following: -- -- 1. Scope-safe AST, generated from a raw definition. See 'FoilTerm', 'FoilScopedTerm', and 'FoilPattern'. -- 2. Conversion between scope-safe and raw term representation (the latter is generated via BNFC), see 'toFoilTerm' and 'fromFoilTerm'. -- 3. Helper functions for patterns. See 'extendScopeFoilPattern' and 'withRefreshedFoilPattern'. -- --- The following is implemented manually in this module: +-- The following is implemented __manually__ in this module: -- -- 1. Correct capture-avoiding substitution (see 'substitute'). -- 2. Computation of weak head normal form (WHNF), see 'whnf'. -- 3. Entry point, gluing everything together. See 'defaultMain'. -- +-- The following is __not implemented__: +-- +-- 1. α-equivalence checks and α-normalization helpers. +-- -- This implementation supports (nested) patterns for pairs. module Language.LambdaPi.Impl.FoilTH where diff --git a/haskell/lambda-pi/src/Language/LambdaPi/Impl/FreeFoil.hs b/haskell/lambda-pi/src/Language/LambdaPi/Impl/FreeFoil.hs index 66ae8dbf..968dd637 100644 --- a/haskell/lambda-pi/src/Language/LambdaPi/Impl/FreeFoil.hs +++ b/haskell/lambda-pi/src/Language/LambdaPi/Impl/FreeFoil.hs @@ -8,20 +8,25 @@ {-# LANGUAGE TypeOperators #-} -- | Free foil implementation of the \(\lambda\Pi\)-calculus (with pairs). -- --- Free foil provides the following: +-- Free foil provides __general__ definitions or implementations for the following: -- -- 1. Freely generated (from a simple signature) scope-safe AST. -- 2. Correct capture-avoiding substitution (see 'substitute'). --- 3. Convenient pattern synonyms (FIXME: use TH to generate those). +-- 3. Correct α-equivalence checks (see 'alphaEquiv' and 'alphaEquivRefreshed') as well as α-normalization (see 'refreshAST'). +-- 4. Conversion helpers (see 'convertToAST' and 'convertFromAST'). -- --- The following is implemented manually in this module: +-- The following is implemented __manually__ in this module: -- --- 1. Conversion between scope-safe and raw term representation (the latter is generated via BNFC), see 'toLambdaPi' and 'fromLambdaPi'. --- 2. Computation of weak head normal form (WHNF), see 'whnf'. --- 3. Entry point, gluing everything together. See 'defaultMain'. +-- 1. Convenient pattern synonyms. +-- 2. 'ZipMatch' instances (enabling general α-equivalence). +-- 3. Conversion between scope-safe and raw term representation (the latter is generated via BNFC), see 'toLambdaPi' and 'fromLambdaPi'. +-- 4. Computation of weak head normal form (WHNF), see 'whnf'. +-- 5. Entry point, gluing everything together. See 'defaultMain'. -- -- __Note:__ free foil does not (easily) support patterns at the moment, -- so only wildcard patterns and variable patterns are handled in this implementation. +-- +-- See "Language.LambdaPi.Impl.FreeFoilTH" for a variation of this with more automation via Template Haskell. module Language.LambdaPi.Impl.FreeFoil where import qualified Control.Monad.Foil as Foil diff --git a/haskell/lambda-pi/src/Language/LambdaPi/Impl/FreeFoilTH.hs b/haskell/lambda-pi/src/Language/LambdaPi/Impl/FreeFoilTH.hs index c09366b9..6d2c6bfc 100644 --- a/haskell/lambda-pi/src/Language/LambdaPi/Impl/FreeFoilTH.hs +++ b/haskell/lambda-pi/src/Language/LambdaPi/Impl/FreeFoilTH.hs @@ -5,6 +5,28 @@ {-# LANGUAGE LambdaCase #-} {-# LANGUAGE PatternSynonyms #-} {-# LANGUAGE TemplateHaskell #-} +-- | Free foil implementation of the \(\lambda\Pi\)-calculus (with pairs). +-- +-- Free foil provides __general__ definitions or implementations for the following: +-- +-- 1. Freely generated (from a simple signature) scope-safe AST. +-- 2. Correct capture-avoiding substitution (see 'substitute'). +-- 3. Correct α-equivalence checks (see 'alphaEquiv' and 'alphaEquivRefreshed') as well as α-normalization (see 'refreshAST'). +-- 4. Conversion helpers (see 'convertToAST' and 'convertFromAST'). +-- +-- The following is __generated__ using Template Haskell: +-- +-- 1. Convenient pattern synonyms. +-- 2. 'ZipMatch' instances (enabling general α-equivalence). +-- 3. Conversion between scope-safe and raw term representation. +-- +-- The following is implemented __manually__ in this module: +-- +-- 1. Computation of weak head normal form (WHNF), see 'whnf'. +-- 2. Entry point, gluing everything together. See 'defaultMain'. +-- +-- __Note:__ free foil does not (easily) support patterns at the moment, +-- so only wildcard patterns and variable patterns are handled in this implementation. module Language.LambdaPi.Impl.FreeFoilTH where import System.Exit (exitFailure)