Switch to Substitution, document new code

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

@@ -47,7 +47,10 @@ module Control.Monad.Foil (
   Substitution,
   lookupSubst,
   identitySubst,
+  voidSubst,
   addSubst,
+  addSubstPattern,
+  addSubstList,
   addRename,
   -- * Unification of binders
   UnifyNameBinders(..),

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

@@ -708,11 +708,14 @@ class CoSinkable (pattern :: S -> S -> Type) where
     -- ^ Continuation, accepting result for the entire pattern and a (possibly refreshed) pattern.
     -> r
 
+-- | Auxiliary data structure for collecting name binders. Used in 'nameBinderListOf'.
 newtype WithNameBinderList r n l (o :: S) (o' :: S) = WithNameBinderList (NameBinderList l r -> NameBinderList n r)
 
+-- | Empty list of name binders (identity).
 idWithNameBinderList :: DExt o o' => WithNameBinderList r n n o o'
 idWithNameBinderList = WithNameBinderList id
 
+-- | Concatenating lists of name binders (compose).
 compWithNameBinderList
   :: (DExt o o', DExt o' o'')
   => WithNameBinderList r n i o o'
@@ -721,6 +724,8 @@ compWithNameBinderList
 compWithNameBinderList (WithNameBinderList f) (WithNameBinderList g) =
   WithNameBinderList (f . g)
 
+-- | Collect name binders of a generalized pattern into a name binder list,
+-- which can be more easily traversed.
 nameBinderListOf :: (CoSinkable binder) => binder n l -> NameBinderList n l
 nameBinderListOf pat = withPattern
   (\_scope' binder k ->
@@ -757,6 +762,10 @@ identitySubst
   :: InjectName e => Substitution e i i
 identitySubst = UnsafeSubstitution IntMap.empty
 
+-- | An empty substitution from an empty scope.
+voidSubst :: Substitution e VoidS n
+voidSubst = UnsafeSubstitution IntMap.empty
+
 -- | Extend substitution with a particular mapping.
 addSubst
   :: Substitution e i o
@@ -766,6 +775,24 @@ addSubst
 addSubst (UnsafeSubstitution env) (UnsafeNameBinder (UnsafeName name)) ex
   = UnsafeSubstitution (IntMap.insert name ex env)
 
+addSubstPattern
+  :: CoSinkable binder
+  => Substitution e i o
+  -> binder i i'
+  -> [e o]
+  -> Substitution e i' o
+addSubstPattern subst pat = addSubstList subst (nameBinderListOf pat)
+
+addSubstList
+  :: Substitution e i o
+  -> NameBinderList i i'
+  -> [e o]
+  -> Substitution e i' o
+addSubstList subst NameBinderListEmpty _ = subst
+addSubstList subst (NameBinderListCons binder binders) (x:xs) =
+  addSubstList (addSubst subst binder x) binders xs
+addSubstList _ _ [] = error "cannot add a binder to Substitution since the value list does not have enough elements"
+
 -- | Add variable renaming to a substitution.
 -- This includes the performance optimization of eliding names mapped to themselves.
 addRename :: InjectName e => Substitution e i o -> NameBinder i i' -> Name o -> Substitution e i' o
@@ -791,13 +818,24 @@ emptyNameMap = NameMap IntMap.empty
 nameMapToSubstitution :: NameMap i (e o) -> Substitution e i o
 nameMapToSubstitution (NameMap m) = (UnsafeSubstitution m)
 
+-- | Extend a map with multiple mappings (by repeatedly applying 'addNameBinder').
+--
+-- Note that the input list is expected to have __at least__ the same number of elements
+-- as there are binders in the input pattern (generalized binder).
 addNameBinders :: CoSinkable binder => binder n l -> [a] -> NameMap n a -> NameMap l a
 addNameBinders pat = addNameBinderList (nameBinderListOf pat)
 
+-- | Extend a map with multiple mappings (by repeatedly applying 'addNameBinder').
+--
+-- Note that the input list is expected to have __at least__ the same number of elements
+-- as there are binders in the input name binder list.
+--
+-- See also 'addNameBinders' for a generalized version.
 addNameBinderList :: NameBinderList n l -> [a] -> NameMap n a -> NameMap l a
-addNameBinderList NameBinderListEmpty [] = id
+addNameBinderList NameBinderListEmpty _ = id
 addNameBinderList (NameBinderListCons binder binders) (x:xs) =
   addNameBinderList binders xs . addNameBinder binder x
+addNameBinderList _ [] = error "cannot add a binder to NameMap since the value list does not have enough elements"
 
 -- | Looking up a name should always succeed.
 --

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

@@ -122,18 +122,19 @@ instance (Bifunctor sig, Foil.CoSinkable binder) => Foil.RelMonad Foil.Name (AST
               subst' = extendSubst subst
            in ScopedAST binder' (Foil.rbind scope' body subst')
 
+-- | Substitution for a single generalized pattern.
 substitutePattern
   :: (Bifunctor sig, Foil.Distinct o, Foil.CoSinkable binder', Foil.CoSinkable binder)
-  => Foil.Scope o
-  -> Foil.NameMap n (AST binder sig o)
-  -> binder' n i
-  -> [AST binder sig o]
+  => Foil.Scope o                           -- ^ Resulting scope.
+  -> Foil.Substitution (AST binder sig) n o -- ^ Environment mapping names in scope @n@.
+  -> binder' n i                            -- ^ Binders that extend scope @n@ to scope @i@.
+  -> [AST binder sig o]                     -- ^ A list of terms intended to serve as
   -> AST binder sig i
   -> AST binder sig o
 substitutePattern scope env binders args body =
-  substitute scope substs' body
+  substitute scope env' body
   where
-    substs' = Foil.nameMapToSubstitution (Foil.addNameBinders binders args env)
+    env' = Foil.addSubstPattern env binders args
 
 -- * \(\alpha\)-equivalence
 

haskell/soas/src/Language/SOAS/Impl.hs

@@ -106,14 +106,16 @@ instance ZipMatchK a => ZipMatch (Type'Sig a) where zipMatch = genericZipMatch2
 type Subst = Subst' Raw.BNFC'Position Foil.VoidS
 type Term = Term' Raw.BNFC'Position
 
+-- | Lookup a substitution by its 'Raw.MetaVarIdent'.
 lookupSubst :: Raw.MetaVarIdent -> [Subst] -> Maybe Subst
 lookupSubst m = find $ \(Subst _loc m' _ _) -> m == m'
 
+-- | Apply meta variable substitutions to a term.
 applySubsts :: Foil.Distinct n => Foil.Scope n -> [Subst] -> Term n -> Term n
 applySubsts scope substs term =
   case term of
     MetaVar _loc m args | Just (Subst _ _ binders body) <- lookupSubst m substs ->
-      substitutePattern scope Foil.emptyNameMap binders args body
+      substitutePattern scope Foil.voidSubst binders args body
     Var{} -> term
     Node node -> Node (bimap goScoped (applySubsts scope substs) node)
   where