Generalize substitutePattern, nameBinderListOf

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

@@ -66,6 +66,10 @@ module Control.Monad.Foil (
   emptyNameMap,
   lookupName,
   addNameBinder,
+  nameMapToSubstitution,
+  addNameBinders,
+  addNameBinderList,
+  NameBinderList(..),
   -- * Constraints
   Ext,
   ExtEvidence(..),

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

@@ -708,6 +708,30 @@ class CoSinkable (pattern :: S -> S -> Type) where
     -- ^ Continuation, accepting result for the entire pattern and a (possibly refreshed) pattern.
     -> r
 
+newtype WithNameBinderList r n l (o :: S) (o' :: S) = WithNameBinderList (NameBinderList l r -> NameBinderList n r)
+
+idWithNameBinderList :: DExt o o' => WithNameBinderList r n n o o'
+idWithNameBinderList = WithNameBinderList id
+
+compWithNameBinderList
+  :: (DExt o o', DExt o' o'')
+  => WithNameBinderList r n i o o'
+  -> WithNameBinderList r i l o' o''
+  -> WithNameBinderList r n l o o''
+compWithNameBinderList (WithNameBinderList f) (WithNameBinderList g) =
+  WithNameBinderList (f . g)
+
+nameBinderListOf :: (CoSinkable binder) => binder n l -> NameBinderList n l
+nameBinderListOf pat = withPattern
+  (\_scope' binder k ->
+    unsafeAssertFresh binder $ \binder' ->
+      k (WithNameBinderList (NameBinderListCons binder)) binder')
+  idWithNameBinderList
+  compWithNameBinderList
+  emptyScope
+  pat
+  (\(WithNameBinderList f) _ -> f NameBinderListEmpty)
+
 instance CoSinkable NameBinder where
   coSinkabilityProof _rename (UnsafeNameBinder name) cont =
     cont unsafeCoerce (UnsafeNameBinder name)
@@ -763,6 +787,18 @@ newtype NameMap (n :: S) a = NameMap { getNameMap :: IntMap a }
 emptyNameMap :: NameMap VoidS a
 emptyNameMap = NameMap IntMap.empty
 
+-- | Convert a 'NameMap' of expressions into a 'Substitution'.
+nameMapToSubstitution :: NameMap i (e o) -> Substitution e i o
+nameMapToSubstitution (NameMap m) = (UnsafeSubstitution m)
+
+addNameBinders :: CoSinkable binder => binder n l -> [a] -> NameMap n a -> NameMap l a
+addNameBinders pat = addNameBinderList (nameBinderListOf pat)
+
+addNameBinderList :: NameBinderList n l -> [a] -> NameMap n a -> NameMap l a
+addNameBinderList NameBinderListEmpty [] = id
+addNameBinderList (NameBinderListCons binder binders) (x:xs) =
+  addNameBinderList binders xs . addNameBinder binder x
+
 -- | Looking up a name should always succeed.
 --
 -- Note that since 'Name' is 'Sinkable', you can lookup a name from scope @n@ in a 'NameMap' for scope @l@ whenever @l@ extends @n@.

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

@@ -122,6 +122,19 @@ instance (Bifunctor sig, Foil.CoSinkable binder) => Foil.RelMonad Foil.Name (AST
               subst' = extendSubst subst
            in ScopedAST binder' (Foil.rbind scope' body subst')
 
+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]
+  -> AST binder sig i
+  -> AST binder sig o
+substitutePattern scope env binders args body =
+  substitute scope substs' body
+  where
+    substs' = Foil.nameMapToSubstitution (Foil.addNameBinders binders args env)
+
 -- * \(\alpha\)-equivalence
 
 -- | Refresh (force) all binders in a term, minimizing the used indices.

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

@@ -77,7 +77,7 @@ toFreeFoilType isBinder config@FreeFoilConfig{..} outerScope innerScope = go
         | Just _ <- lookupBindingName typeName freeFoilTermConfigs ->
             PeelConT (toFreeFoilName config typeName) (typeParams ++ [outerScope, innerScope])
         | Just FreeFoilTermConfig{..} <- lookupScopeName typeName freeFoilTermConfigs ->
-            PeelConT (toFreeFoilScopedName config rawTermName) (typeParams ++ [outerScope])
+            PeelConT (toFreeFoilName config rawTermName) (typeParams ++ [innerScope])
         | Just _ <- lookupSubTermName typeName freeFoilTermConfigs ->
             PeelConT (toFreeFoilName config typeName) (typeParams ++ [outerScope])
       ForallT bndrs ctx type_ -> ForallT bndrs ctx (go type_)

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

@@ -1,5 +1,6 @@
 {-# OPTIONS_GHC -Wno-orphans #-}
 {-# LANGUAGE DataKinds         #-}
+{-# LANGUAGE ScopedTypeVariables         #-}
 {-# LANGUAGE TypeFamilies         #-}
 {-# LANGUAGE DeriveGeneric         #-}
 {-# LANGUAGE StandaloneDeriving         #-}
@@ -13,6 +14,10 @@
 {-# LANGUAGE TemplateHaskell   #-}
 module Language.SOAS.Impl where
 
+import Data.List (find)
+import Data.Bifunctor
+import Data.Bifunctor.TH
+import qualified Control.Monad.Foil as Foil
 import           Control.Monad.Free.Foil.TH.MkFreeFoil
 import           Control.Monad.Free.Foil
 import qualified Language.SOAS.Syntax.Abs    as Raw
@@ -73,6 +78,15 @@ deriveGenericK ''Term'Sig
 deriveGenericK ''OpArg'Sig
 deriveGenericK ''Type'Sig
 
+deriving instance Functor (Term'Sig a scope)
+deriving instance Functor (OpArg'Sig a scope)
+deriving instance Functor (Type'Sig a scope)
+deriveBifunctor ''OpArg'Sig
+deriveBifunctor ''Term'Sig
+deriveBifunctor ''Type'Sig
+
+instance Foil.CoSinkable  (Binders' a)  -- FIXME: derive via GenericK?
+
 -- | Ignore 'Raw.BNFC'Position' when matching terms.
 instance ZipMatchK Raw.BNFC'Position where zipMatchWithK = zipMatchViaChooseLeft
 -- | Match 'Raw.OpIdent' via 'Eq'.
@@ -87,6 +101,28 @@ instance ZipMatchK a => ZipMatchK (Type'Sig a)
 instance ZipMatchK a => ZipMatch (Term'Sig a) where zipMatch = genericZipMatch2
 instance ZipMatchK a => ZipMatch (Type'Sig a) where zipMatch = genericZipMatch2
 
+-- * User-defined code
+
+type Subst = Subst' Raw.BNFC'Position Foil.VoidS
+type Term = Term' Raw.BNFC'Position
+
+lookupSubst :: Raw.MetaVarIdent -> [Subst] -> Maybe Subst
+lookupSubst m = find $ \(Subst _loc m' _ _) -> m == m'
+
+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
+    Var{} -> term
+    Node node -> Node (bimap goScoped (applySubsts scope substs) node)
+  where
+    goScoped (ScopedAST binders body) =
+      case Foil.assertDistinct binders of
+        Foil.Distinct ->
+          let scope' = Foil.extendScopePattern binders scope
+           in ScopedAST binders (applySubsts scope' substs body)
+
 -- | A SOAS interpreter implemented via the free foil.
 defaultMain :: IO ()
 defaultMain = do