Update documentation

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.

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]

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

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
 

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

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)