From 61908f3ae61aeb53d4b3661d87b6ca21e4d2e133 Mon Sep 17 00:00:00 2001
From: Nikolai Kudasov <nickolay.kudasov@gmail.com>
Date: Wed, 19 Jun 2024 15:37:18 +0300
Subject: [PATCH] Improve documentation in free-foil

---
 haskell/free-foil/src/Control/Monad/Foil.hs   |  2 +-
 .../src/Control/Monad/Foil/Internal.hs        |  2 +
 .../free-foil/src/Control/Monad/Free/Foil.hs  | 86 ++++++++++---------
 3 files changed, 50 insertions(+), 40 deletions(-)

diff --git a/haskell/free-foil/src/Control/Monad/Foil.hs b/haskell/free-foil/src/Control/Monad/Foil.hs
index 25cf4034..4288d015 100644
--- a/haskell/free-foil/src/Control/Monad/Foil.hs
+++ b/haskell/free-foil/src/Control/Monad/Foil.hs
@@ -28,7 +28,7 @@ module Control.Monad.Foil (
   withFresh,
   withRefreshed,
   unsinkName,
-  -- * Safe (co)sinking
+  -- * Safe (co)sinking and renaming
   Sinkable(..),
   CoSinkable(..),
   sink,
diff --git a/haskell/free-foil/src/Control/Monad/Foil/Internal.hs b/haskell/free-foil/src/Control/Monad/Foil/Internal.hs
index a64c32c4..420bc51e 100644
--- a/haskell/free-foil/src/Control/Monad/Foil/Internal.hs
+++ b/haskell/free-foil/src/Control/Monad/Foil/Internal.hs
@@ -177,6 +177,8 @@ data UnifyNameBinders n l r where
   -- to match the left one.
   RenameRightNameBinder :: (NameBinder n r -> NameBinder n l) -> UnifyNameBinders n l r
 
+-- | Unify binders either by asserting that they are the same,
+-- or by providing a /safe/ renaming function to convert one binder to another.
 unifyNameBinders
   :: forall i l r.
      NameBinder i l
diff --git a/haskell/free-foil/src/Control/Monad/Free/Foil.hs b/haskell/free-foil/src/Control/Monad/Free/Foil.hs
index c168826e..8754339c 100644
--- a/haskell/free-foil/src/Control/Monad/Free/Foil.hs
+++ b/haskell/free-foil/src/Control/Monad/Free/Foil.hs
@@ -58,6 +58,8 @@ instance Bifunctor sig => Foil.Sinkable (AST sig) where
 instance Foil.InjectName (AST sig) where
   injectName = Var
 
+-- * Substitution
+
 -- | Substitution for free (scoped monads).
 substitute
   :: (Bifunctor sig, Foil.Distinct o)
@@ -118,6 +120,8 @@ instance Bifunctor sig => Foil.RelMonad Foil.Name (AST sig) where
                           Just n  -> Foil.sink (subst n)
            in ScopedAST binder' (Foil.rbind scope' body subst')
 
+-- * \(\alpha\)-equivalence
+
 -- | Refresh (force) all binders in a term, minimizing the used indices.
 refreshAST
   :: (Bifunctor sig, Foil.Distinct n)
@@ -139,45 +143,6 @@ refreshScopedAST scope (ScopedAST binder body) =
         subst = Foil.addRename (Foil.sink Foil.identitySubst) binder (Foil.nameOf binder')
     in ScopedAST binder' (substituteRefreshed scope' subst body)
 
--- | Perform one-level matching for the two terms.
-class ZipMatch sig where
-  zipMatch
-    :: sig scope term
-    -> sig scope' term'
-    -> Maybe (sig (scope, scope') (term, term'))
-
-instance (ZipMatch f, ZipMatch g) => ZipMatch (Sum f g) where
-  zipMatch (L2 f) (L2 f') = L2 <$> zipMatch f f'
-  zipMatch (R2 g) (R2 g') = R2 <$> zipMatch g g'
-  zipMatch _ _ = Nothing
-
--- | /Unsafe/ equality check for two terms.
--- This check ignores the possibility that two terms might have different
--- scope extensions under binders (which might happen due to substitution
--- under a binder in absence of name conflicts).
-unsafeEqAST
-  :: (Bifoldable sig, ZipMatch sig)
-  => AST sig n
-  -> AST sig l
-  -> Bool
-unsafeEqAST (Var x) (Var y) = x == coerce y
-unsafeEqAST (Node t1) (Node t2) =
-  case zipMatch t1 t2 of
-    Nothing -> False
-    Just tt -> getAll (bifoldMap (All . uncurry unsafeEqScopedAST) (All . uncurry unsafeEqAST) tt)
-unsafeEqAST _ _ = False
-
--- | A version of 'unsafeEqAST' for scoped terms.
-unsafeEqScopedAST
-  :: (Bifoldable sig, ZipMatch sig)
-  => ScopedAST sig n
-  -> ScopedAST sig l
-  -> Bool
-unsafeEqScopedAST (ScopedAST binder1 body1) (ScopedAST binder2 body2) = and
-  [ binder1 == coerce binder2
-  , body1 `unsafeEqAST` body2
-  ]
-
 -- | \(\alpha\)-equivalence check for two terms in one scope
 -- via normalization of bound identifiers (via 'refreshAST').
 --
@@ -238,3 +203,46 @@ alphaEquivScoped scope
           Foil.Distinct ->
             let scope1 = Foil.extendScope binder1 scope
             in alphaEquiv scope1 body1 (Foil.liftRM scope1 (Foil.fromNameBinderRenaming rename2to1) body2)
+
+-- ** Unsafe equality checks
+
+-- | /Unsafe/ equality check for two terms.
+-- This check ignores the possibility that two terms might have different
+-- scope extensions under binders (which might happen due to substitution
+-- under a binder in absence of name conflicts).
+unsafeEqAST
+  :: (Bifoldable sig, ZipMatch sig)
+  => AST sig n
+  -> AST sig l
+  -> Bool
+unsafeEqAST (Var x) (Var y) = x == coerce y
+unsafeEqAST (Node t1) (Node t2) =
+  case zipMatch t1 t2 of
+    Nothing -> False
+    Just tt -> getAll (bifoldMap (All . uncurry unsafeEqScopedAST) (All . uncurry unsafeEqAST) tt)
+unsafeEqAST _ _ = False
+
+-- | A version of 'unsafeEqAST' for scoped terms.
+unsafeEqScopedAST
+  :: (Bifoldable sig, ZipMatch sig)
+  => ScopedAST sig n
+  -> ScopedAST sig l
+  -> Bool
+unsafeEqScopedAST (ScopedAST binder1 body1) (ScopedAST binder2 body2) = and
+  [ binder1 == coerce binder2
+  , body1 `unsafeEqAST` body2
+  ]
+
+-- ** Syntactic matching (unification)
+
+-- | Perform one-level matching for the two (non-variable) terms.
+class ZipMatch sig where
+  zipMatch
+    :: sig scope term     -- ^ Left non-variable term.
+    -> sig scope' term'   -- ^ Right non-variable term.
+    -> Maybe (sig (scope, scope') (term, term'))
+
+instance (ZipMatch f, ZipMatch g) => ZipMatch (Sum f g) where
+  zipMatch (L2 f) (L2 f') = L2 <$> zipMatch f f'
+  zipMatch (R2 g) (R2 g') = R2 <$> zipMatch g g'
+  zipMatch _ _ = Nothing