packages feed

free-foil (empty) → 0.0.2

raw patch · 18 files changed

+1896/−0 lines, 18 filesdep +arraydep +basedep +bifunctorssetup-changed

Dependencies added: array, base, bifunctors, containers, deepseq, doctest-parallel, free-foil, template-haskell, text

Files

+ LICENSE view
@@ -0,0 +1,28 @@+BSD 3-Clause License++Copyright (c) 2023, Nikolai Kudasov++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are met:++1. Redistributions of source code must retain the above copyright notice, this+   list of conditions and the following disclaimer.++2. Redistributions in binary form must reproduce the above copyright notice,+   this list of conditions and the following disclaimer in the documentation+   and/or other materials provided with the distribution.++3. Neither the name of the copyright holder nor the names of its+   contributors may be used to endorse or promote products derived from+   this software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"+AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE+IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE+DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE+FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL+DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR+SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER+CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,+OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ README.md view
@@ -0,0 +1,2 @@+# free-foil+Efficient Type-Safe Capture-Avoiding Substitution for Free (Scoped Monads).
+ Setup.hs view
@@ -0,0 +1,6 @@+module Main (main) where++import Distribution.Simple (defaultMain)++main :: IO ()+main = defaultMain
+ free-foil.cabal view
@@ -0,0 +1,93 @@+cabal-version: 1.12++-- This file has been generated from package.yaml by hpack version 0.36.0.+--+-- see: https://github.com/sol/hpack++name:           free-foil+version:        0.0.2+synopsis:       Efficient Type-Safe Capture-Avoiding Substitution for Free (Scoped Monads)+description:    Please see the README on GitHub at <https://github.com/fizruk/free-foil#readme>+category:       Parsing+homepage:       https://github.com/fizruk/free-foil#readme+bug-reports:    https://github.com/fizruk/free-foil/issues+author:         Nikolai Kudasov+maintainer:     nickolay.kudasov@gmail.com+copyright:      2023–2024 Nikolai Kudasov, Renata Shakirova, Egor Shalagin, Karina Tyulebaeva+license:        BSD3+license-file:   LICENSE+build-type:     Simple+extra-source-files:+    README.md+    LICENSE++source-repository head+  type: git+  location: https://github.com/fizruk/free-foil++library+  exposed-modules:+      Control.Monad.Foil+      Control.Monad.Foil.Example+      Control.Monad.Foil.Internal+      Control.Monad.Foil.Relative+      Control.Monad.Foil.TH+      Control.Monad.Foil.TH.MkFoilData+      Control.Monad.Foil.TH.MkFromFoil+      Control.Monad.Foil.TH.MkInstancesFoil+      Control.Monad.Foil.TH.MkToFoil+      Control.Monad.Foil.TH.Util+      Control.Monad.Free.Foil+      Control.Monad.Free.Foil.Example+  other-modules:+      Paths_free_foil+  hs-source-dirs:+      src+  ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints -optP-Wno-nonportable-include-path+  build-depends:+      array >=0.5.3.0+    , base >=4.7 && <5+    , bifunctors+    , containers+    , deepseq+    , template-haskell >=2.21.0.0+    , text >=1.2.3.1+  default-language: Haskell2010++test-suite doctests+  type: exitcode-stdio-1.0+  main-is: Main.hs+  hs-source-dirs:+      src/+      test/doctests+  ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints -optP-Wno-nonportable-include-path+  build-depends:+      array >=0.5.3.0+    , base >=4.7 && <5+    , bifunctors+    , containers+    , deepseq+    , doctest-parallel+    , free-foil+    , template-haskell >=2.21.0.0+    , text >=1.2.3.1+  default-language: Haskell2010++test-suite spec+  type: exitcode-stdio-1.0+  main-is: Spec.hs+  other-modules:+      Paths_free_foil+  hs-source-dirs:+      test+  ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints -optP-Wno-nonportable-include-path -threaded -rtsopts -with-rtsopts=-N+  build-depends:+      array >=0.5.3.0+    , base >=4.7 && <5+    , bifunctors+    , containers+    , deepseq+    , free-foil+    , template-haskell >=2.21.0.0+    , text >=1.2.3.1+  default-language: Haskell2010
+ src/Control/Monad/Foil.hs view
@@ -0,0 +1,58 @@+-- | Main definitions of the foil that can be+-- reused for specific implementations.+--+-- The original description of this approach+-- is described in the IFL 2022 paper by Maclaurin, Radul, and Paszke+-- [«The Foil: Capture-Avoiding Substitution With No Sharp Edges»](https://doi.org/10.1145/3587216.3587224).+-- This module also introduces 'CoSinkable' class,+-- generalizing handling of patterns, as described in+-- [«Free Foil: Generating Efficient and Scope-Safe Abstract Syntax»](https://arxiv.org/abs/2405.16384).+--+-- Since the representation of scopes and substitutions+-- is either 'IntMap' or 'IntSet', many of the operations+-- have a worst-case complexity of \(O(\min(n,W))\).+-- This means that the operation can become linear in the size of the scope \(n\) with a maximum of \(W\)+-- — the number of bits in an 'Int' (32 or 64).+module Control.Monad.Foil (+  -- * Safe scopes, names, and binders+  S(..),+  Scope,+  Name,+  NameBinder,+  emptyScope,+  extendScope,+  member,+  nameOf,+  nameId,+  withFreshBinder,+  withFresh,+  withRefreshed,+  unsinkName,+  -- * Safe (co)sinking+  Sinkable(..),+  CoSinkable(..),+  sink,+  extendRenaming,+  extendRenamingNameBinder,+  -- * Safe substitutions+  Substitution,+  lookupSubst,+  identitySubst,+  addSubst,+  addRename,+  -- * Name maps+  NameMap,+  emptyNameMap,+  lookupName,+  addNameBinder,+  -- * Constraints+  Ext,+  ExtEvidence(..),+  Distinct,+  DistinctEvidence(..),+  assertDistinct,+  DExt,+  InjectName(..),+) where++import           Control.Monad.Foil.Internal
+ src/Control/Monad/Foil/Example.hs view
@@ -0,0 +1,155 @@+{-# LANGUAGE DataKinds             #-}+{-# LANGUAGE GADTs                 #-}+{-# LANGUAGE LambdaCase            #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE RankNTypes            #-}+-- | Example implementation of untyped \(\lambda\)-calculus with the foil.+module Control.Monad.Foil.Example where++import           Control.DeepSeq+import           Control.Monad.Foil+import           Control.Monad.Foil.Relative++-- $setup+-- >>> import Control.Monad.Foil++-- | Untyped \(\lambda\)-terms in scope @n@.+data Expr n where+  -- | Variables are names in scope @n@: \(x\)+  VarE :: Name n -> Expr n+  -- | Application of one term to another: \((t_1, t_2)\)+  AppE :: Expr n -> Expr n -> Expr n+  -- | \(\lambda\)-abstraction introduces a binder and a term in an extended scope: \(\lambda x. t\)+  LamE :: NameBinder n l -> Expr l -> Expr n++-- | Use 'ppExpr' to show \(\lambda\)-terms.+instance Show (Expr n) where+  show = ppExpr++instance NFData (Expr l) where+  rnf (LamE binder body) = rnf binder `seq` rnf body+  rnf (AppE fun arg)     = rnf fun `seq` rnf arg+  rnf (VarE name)        = rnf name++-- | This instance serves as a proof+-- that sinking of 'Expr' is safe.+instance Sinkable Expr where+  sinkabilityProof rename (VarE v) = VarE (rename v)+  sinkabilityProof rename (AppE f e) = AppE (sinkabilityProof rename f) (sinkabilityProof rename e)+  sinkabilityProof rename (LamE binder body) = extendRenaming rename binder $ \rename' binder' ->+    LamE binder' (sinkabilityProof rename' body)++instance InjectName Expr where+  injectName = VarE++-- | 'Expr' is a monad relative to 'Name'.+instance RelMonad Name Expr where+  rreturn = VarE+  rbind scope term subst =+    case term of+      VarE name -> subst name+      AppE x y  -> AppE (rbind scope x subst) (rbind scope y subst)+      LamE binder body ->+        withRefreshed scope (nameOf binder) $ \binder' ->+          let scope' = extendScope binder' scope+              subst' name = case unsinkName binder name of+                          Nothing -> rreturn (nameOf binder')+                          Just n  -> sink (subst n)+           in LamE binder' (rbind scope' body subst')++-- | Substitution for untyped \(\lambda\)-terms.+-- The foil helps implement this function without forgetting scope extensions and renaming.+substitute :: Distinct o => Scope o -> Substitution Expr i o -> Expr i -> Expr o+substitute scope subst = \case+    VarE name -> lookupSubst subst name+    AppE f x -> AppE (substitute scope subst f) (substitute scope subst x)+    LamE binder body -> withRefreshed scope (nameOf binder) $ \binder' ->+      let subst' = addRename (sink subst) binder (nameOf binder')+          scope' = extendScope binder' scope+          body' = substitute scope' subst' body+       in LamE binder' body'++-- | Compute weak head normal form (WHNF) of a \(\lambda\)-term.+--+-- >>> whnf emptyScope (AppE (churchN 2) (churchN 2))+-- λx1. (λx0. λx1. (x0 (x0 x1)) (λx0. λx1. (x0 (x0 x1)) x1))+whnf :: Distinct n => Scope n -> Expr n -> Expr n+whnf scope = \case+  AppE fun arg ->+    case whnf scope fun of+      LamE binder body ->+        let subst = addSubst identitySubst binder arg+        in whnf scope (substitute scope subst body)+      fun' -> AppE fun' arg+  t -> t++-- | Compute weak head normal form (WHNF) of a __closed__ \(\lambda\)-term.+--+-- >>> whnf' (AppE (churchN 2) (churchN 2))+-- λx1. (λx0. λx1. (x0 (x0 x1)) (λx0. λx1. (x0 (x0 x1)) x1))+whnf' :: Expr VoidS -> Expr VoidS+whnf' = whnf emptyScope++-- | Compute normal form (NF) of a \(\lambda\)-term.+--+-- >>> nf emptyScope (AppE (churchN 2) (churchN 2))+-- λx1. λx2. (x1 (x1 (x1 (x1 x2))))+nf :: Distinct n => Scope n -> Expr n -> Expr n+nf scope expr = case expr of+  LamE binder body ->+    -- Instead of using 'assertDistinct',+    -- another option is to add 'Distinct l' constraint+    -- to the definition of 'LamE'.+    case assertDistinct binder of+      Distinct ->+        let scope' = extendScope binder scope+        in LamE binder (nf scope' body)+  AppE fun arg ->+    case whnf scope fun of+      LamE binder body ->+        let subst = addSubst identitySubst binder arg+        in nf scope (substitute scope subst body)+      fun' -> AppE (nf scope fun') (nf scope arg)+  t -> t++-- | Compute normal form (NF) of a __closed__ \(\lambda\)-term.+--+-- >>> nf' (AppE (churchN 2) (churchN 2))+-- λx1. λx2. (x1 (x1 (x1 (x1 x2))))+nf' :: Expr VoidS -> Expr VoidS+nf' = nf emptyScope++-- | Pretty print a name.+ppName :: Name n -> String+ppName name = "x" <> show (nameId name)++-- | Pretty-print a \(\lambda\)-term.+--+-- >>> ppExpr (churchN 3)+-- "\955x0. \955x1. (x0 (x0 (x0 x1)))"+ppExpr :: Expr n -> String+ppExpr = \case+  VarE name -> ppName name+  AppE x y -> "(" <> ppExpr x <> " " <> ppExpr y <> ")"+  LamE binder body -> "λ" <> ppName (nameOf binder) <> ". " <> ppExpr body++-- | A helper for constructing \(\lambda\)-abstractions.+lam :: Distinct n => Scope n -> (forall l. DExt n l => Scope l -> NameBinder n l -> Expr l) -> Expr n+lam scope mkBody = withFresh scope $ \x ->+  let scope' = extendScope x scope+   in LamE x (mkBody scope' x)++-- | Church-encoding of a natural number \(n\).+--+-- >>> churchN 0+-- λx0. λx1. x1+--+-- >>> churchN 3+-- λx0. λx1. (x0 (x0 (x0 x1)))+churchN :: Int -> Expr VoidS+churchN n =+  lam emptyScope $ \sx nx ->+    lam sx $ \_sxy ny ->+      let x = sink (VarE (nameOf nx))+          y = VarE (nameOf ny)+       in iterate (AppE x) y !! n
+ src/Control/Monad/Foil/Internal.hs view
@@ -0,0 +1,359 @@+{-# LANGUAGE BlockArguments             #-}+{-# LANGUAGE ConstraintKinds            #-}+{-# LANGUAGE DataKinds                  #-}+{-# LANGUAGE FlexibleInstances          #-}+{-# LANGUAGE GADTs                      #-}+{-# LANGUAGE KindSignatures             #-}+{-# LANGUAGE MultiParamTypeClasses      #-}+{-# LANGUAGE QuantifiedConstraints      #-}+{-# LANGUAGE RankNTypes                 #-}+{-# LANGUAGE ScopedTypeVariables        #-}+{-# LANGUAGE TypeApplications           #-}+{-# LANGUAGE UndecidableInstances       #-}+{-# OPTIONS_GHC -Wno-incomplete-patterns #-}+{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}+{-# LANGUAGE DerivingStrategies         #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# OPTIONS_GHC -Wno-redundant-constraints #-}+-- | Main definitions of the foil that can be+-- reused for specific implementations.+-- This is an internal module, so it also contains implementation details of the foil.+--+-- The original description of this approach+-- is described in the IFL 2022 paper by Maclaurin, Radul, and Paszke+-- [«The Foil: Capture-Avoiding Substitution With No Sharp Edges»](https://doi.org/10.1145/3587216.3587224).+-- This module also introduces 'CoSinkable' class,+-- generalizing handling of patterns, as described in+-- [«Free Foil: Generating Efficient and Scope-Safe Abstract Syntax»](https://arxiv.org/abs/2405.16384).+--+-- Since the representation of scopes and substitutions+-- is either 'IntMap' or 'IntSet', many of the operations+-- have a worst-case complexity of \(O(\min(n,W))\).+-- This means that the operation can become linear in the size of the scope \(n\) with a maximum of \(W\)+-- — the number of bits in an 'Int' (32 or 64).+module Control.Monad.Foil.Internal where++import           Control.DeepSeq (NFData (..))+import           Data.IntMap+import qualified Data.IntMap     as IntMap+import           Data.IntSet+import qualified Data.IntSet     as IntSet+import           Data.Kind       (Type)+import           Unsafe.Coerce++-- * Safe types and operations++-- | 'S' is a data kind of scope indices.+data S+  = VoidS -- ^ 'VoidS' is the only explicit scope available to the users, representing an empty scope.+          -- All other scopes are represented with type variables,+          -- bound in rank-2 polymophic functions like 'withFreshBinder'.++-- | A safe scope, indexed by a type-level scope index 'n'.+newtype Scope (n :: S) = UnsafeScope RawScope+  deriving newtype NFData++-- | A name in a safe scope, indexed by a type-level scope index 'n'.+newtype Name (n :: S) = UnsafeName RawName+  deriving newtype (NFData, Eq, Ord, Show)++-- | A name binder is a name that extends scope @n@ to a (larger) scope @l@.+newtype NameBinder (n :: S) (l :: S) =+  UnsafeNameBinder (Name l)+    deriving newtype (NFData, Eq, Ord, Show)++-- | An empty scope (without any names).+emptyScope :: Scope VoidS+emptyScope = UnsafeScope IntSet.empty++-- | \(O(\min(n,W))\).+-- Extend a scope with one name (safely).+-- Note that as long as the foil is used as intended,+-- the name binder is guaranteed to introduce a name+-- that does not appear in the initial scope.+extendScope :: NameBinder n l -> Scope n -> Scope l+extendScope (UnsafeNameBinder (UnsafeName name)) (UnsafeScope scope) =+  UnsafeScope (IntSet.insert name scope)++-- | A runtime check for potential name capture.+member :: Name l -> Scope n -> Bool+member (UnsafeName name) (UnsafeScope s) = rawMember name s++-- | Extract name from a name binder.+nameOf :: NameBinder n l -> Name l+nameOf (UnsafeNameBinder name) = name++-- | Convert 'Name' into an identifier.+-- This may be useful for printing and debugging.+nameId :: Name l -> Id+nameId (UnsafeName i) = i++-- | Allocate a fresh binder for a given scope.+withFreshBinder+  :: Scope n+  -> (forall l. NameBinder n l -> r) -> r+withFreshBinder (UnsafeScope scope) cont =+  cont binder+  where+    binder = UnsafeNameBinder (UnsafeName (rawFreshName scope))++-- | Evidence that scope @n@ contains distinct names.+data DistinctEvidence (n :: S) where+  Distinct :: Distinct n => DistinctEvidence n++-- | Unsafely declare that scope @n@ is distinct.+-- Used in 'unsafeAssertFresh'.+unsafeDistinct :: DistinctEvidence n+unsafeDistinct = unsafeCoerce (Distinct :: DistinctEvidence VoidS)++-- | Evidence that scope @l@ extends scope @n@.+data ExtEvidence (n :: S) (l :: S) where+  Ext :: Ext n l => ExtEvidence n l++-- | Unsafely declare that scope @l@ extends scope @n@.+-- Used in 'unsafeAssertFresh'.+unsafeExt :: ExtEvidence n l+unsafeExt = unsafeCoerce (Ext :: ExtEvidence VoidS VoidS)++-- | Safely produce a fresh name binder with respect to a given scope.+withFresh+  :: Distinct n => Scope n+  -> (forall l. DExt n l => NameBinder n l -> r) -> r+withFresh scope cont = withFreshBinder scope (`unsafeAssertFresh` cont)++-- | Unsafely declare that a given name (binder)+-- is already fresh in any scope @n'@.+unsafeAssertFresh :: forall n l n' l' r. NameBinder n l+  -> (DExt n' l' => NameBinder n' l' -> r) -> r+unsafeAssertFresh binder cont =+  case unsafeDistinct @l' of+    Distinct -> case unsafeExt @n' @l' of+      Ext -> cont (unsafeCoerce binder)++-- | A distinct scope extended with a 'NameBinder' is also distinct.+assertDistinct :: Distinct n => NameBinder n l -> DistinctEvidence l+assertDistinct _ = unsafeDistinct++-- | Safely rename (if necessary) a given name to extend a given scope.+-- This is similar to 'withFresh', except if the name does not clash with+-- the scope, it can be used immediately, without renaming.+withRefreshed+  :: Distinct o+  => Scope o    -- ^ Ambient scope.+  -> Name i     -- ^ Name to refresh (if it clashes with the ambient scope).+  -> (forall o'. DExt o o' => NameBinder o o' -> r)+  -- ^ Continuation, accepting the refreshed name.+  -> r+withRefreshed scope@(UnsafeScope rawScope) name@(UnsafeName rawName) cont+  | IntSet.member rawName rawScope = withFresh scope cont+  | otherwise = unsafeAssertFresh (UnsafeNameBinder name) cont++-- | Try coercing the name back to the (smaller) scope,+-- given a binder that extends that scope.+unsinkName :: NameBinder n l -> Name l -> Maybe (Name n)+unsinkName binder name@(UnsafeName raw)+  | nameOf binder == name = Nothing+  | otherwise = Just (UnsafeName raw)++-- * Safe sinking++-- | Sinking an expression from scope @n@ into a (usualy extended) scope @l@,+-- given the renaming (injection from scope @n@ to scope @l@).+class Sinkable (e :: S -> Type) where+  -- | An implementation of this method that typechecks+  -- proves to the compiler that the expression is indeed+  -- 'Sinkable'. However, instead of this implementation, 'sink'+  -- should be used at all call sites for efficiency.+  sinkabilityProof+    :: (Name n -> Name l)   -- ^ Map names from scope @n@ to a (possibly larger) scope @l@.+    -> e n                  -- ^ Expression with free variables in scope @n@.+    -> e l++-- | Sinking a 'Name' is as simple as applying the renaming.+instance Sinkable Name where+  sinkabilityProof rename = rename++-- | Efficient version of 'sinkabilityProof'.+-- In fact, once 'sinkabilityProof' typechecks,+-- it is safe to 'sink' by coercion.+-- See Section 3.5 in [«The Foil: Capture-Avoiding Substitution With No Sharp Edges»](https://doi.org/10.1145/3587216.3587224) for the details.+sink :: (Sinkable e, DExt n l) => e n -> e l+sink = unsafeCoerce++-- | Extend renaming when going under a 'CoSinkable' pattern (generalized binder).+-- Note that the scope under pattern is independent of the codomain of the renaming.+--+-- This function is used to go under binders when implementing 'sinkabilityProof'+-- and is both a generalization of 'extendRenamingNameBinder' and an efficient implementation of 'coSinkabilityProof'.+extendRenaming+  :: CoSinkable pattern+  => (Name n -> Name n')  -- ^ Map names from scope @n@ to a (possibly larger) scope @n'@.+  -> pattern n l          -- ^ A pattern that extends scope @n@ to another scope @l@.+  -> (forall l'. (Name l -> Name l') -> pattern n' l' -> r )+  -- ^ A continuation, accepting an extended renaming from @l@ to @l'@ (which itself extends @n'@)+  -- and a (possibly refreshed) pattern that extends @n'@ to @l'@.+  -> r+extendRenaming _ pattern cont =+  cont unsafeCoerce (unsafeCoerce pattern)++-- | Extend renaming when going under a 'NameBinder'.+-- Note that the scope under binder is independent of the codomain of the renaming.+--+-- Semantically, this function may need to rename the binder (resulting in the new scope @l'@),+-- to make sure it does not clash with scope @n'@.+-- However, as it turns out, the foil makes it safe+-- to implement this function as a coercion.+-- See Appendix A in [«The Foil: Capture-Avoiding Substitution With No Sharp Edges»](https://doi.org/10.1145/3587216.3587224) for the details.+--+-- This function is used to go under binders when implementing 'sinkabilityProof'.+-- A generalization of this function is 'extendRenaming' (which is an efficient version of 'coSinkabilityProof').+extendRenamingNameBinder+  :: (Name n -> Name n')  -- ^ Map names from scope @n@ to a (possibly larger) scope @n'@.+  -> NameBinder n l       -- ^ A name binder that extends scope @n@ to another scope @l@.+  -> (forall l'. (Name l -> Name l') -> NameBinder n' l' -> r )+  -- ^ A continuation, accepting an extended renaming from @l@ to @l'@ (which itself extends @n'@)+  -- and a (possibly refreshed) binder that extends @n'@ to @l'@.+  -> r+extendRenamingNameBinder _ (UnsafeNameBinder name) cont =+  cont unsafeCoerce (UnsafeNameBinder name)++-- | 'CoSinkable' is to patterns (generalized binders)+-- what 'Sinkable' is to expressions.+--+-- See Section 2.3 of [«Free Foil: Generating Efficient and Scope-Safe Abstract Syntax»](https://arxiv.org/abs/2405.16384) for more details.+class CoSinkable (pattern :: S -> S -> Type) where+  -- | An implementation of this method that typechecks+  -- proves to the compiler that the pattern is indeed+  -- 'CoSinkable'. However, instead of this implementation,+  -- 'extendRenaming' should be used at all call sites for efficiency.+  coSinkabilityProof+    :: (Name n -> Name n')  -- ^ Map names from scope @n@ to a (possibly larger) scope @n'@.+    -> pattern n l          -- ^ A pattern that extends scope @n@ to another scope @l@.+    -> (forall l'. (Name l -> Name l') -> pattern n' l' -> r)+    -- ^ A continuation, accepting an extended renaming from @l@ to @l'@ (which itself extends @n'@)+    -- and a (possibly refreshed) pattern that extends @n'@ to @l'@.+    -> r++instance CoSinkable NameBinder where+  coSinkabilityProof _rename (UnsafeNameBinder name) cont =+    cont unsafeCoerce (UnsafeNameBinder name)++-- * Safe substitions++-- | A substitution is a mapping from names in scope @i@+-- to expressions @e o@ in scope @o@.+newtype Substitution (e :: S -> Type) (i :: S) (o :: S) =+  UnsafeSubstitution (IntMap (e o))++-- | Apply substitution to a given name.+lookupSubst :: InjectName e => Substitution e i o -> Name i -> e o+lookupSubst (UnsafeSubstitution env) (UnsafeName name) =+    case IntMap.lookup name env of+        Just ex -> ex+        Nothing -> injectName (UnsafeName name)++-- | Identity substitution maps all names to expresion-variables.+identitySubst+  :: InjectName e => Substitution e i i+identitySubst = UnsafeSubstitution IntMap.empty++-- | Extend substitution with a particular mapping.+addSubst+  :: Substitution e i o+  -> NameBinder i i'+  -> e o+  -> Substitution e i' o+addSubst (UnsafeSubstitution env) (UnsafeNameBinder (UnsafeName name)) ex+  = UnsafeSubstitution (IntMap.insert name ex env)++-- | 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+addRename s@(UnsafeSubstitution env) b@(UnsafeNameBinder (UnsafeName name1)) n@(UnsafeName name2)+    | name1 == name2 = UnsafeSubstitution (IntMap.delete name1 env)+    | otherwise = addSubst s b (injectName n)++-- | Substitutions are sinkable as long as corresponding expressions are.+instance (Sinkable e) => Sinkable (Substitution e i) where+  sinkabilityProof rename (UnsafeSubstitution env) =+    UnsafeSubstitution (fmap (sinkabilityProof rename) env)++-- * 'Name' maps++-- | A /total/ map from names in scope @n@ to elements of type @a@.+newtype NameMap (n :: S) a = NameMap { getNameMap :: IntMap a }++-- | An empty map belongs in the empty scope.+emptyNameMap :: NameMap VoidS a+emptyNameMap = NameMap IntMap.empty++-- | 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@.+lookupName :: Name n -> NameMap n a -> a+lookupName name (NameMap m) =+  case IntMap.lookup (nameId name) m of+    Nothing -> error "impossible: unknown name in a NameMap"+    Just x  -> x++-- | Extending a map with a single mapping.+--+-- Note that the scope parameter of the result differs from the initial map.+addNameBinder :: NameBinder n l -> a -> NameMap n a -> NameMap l a+addNameBinder name x (NameMap m) = NameMap (IntMap.insert (nameId (nameOf name)) x m)++-- * Raw types and operations++-- | We will use 'Int' for efficient representation of identifiers.+type Id = Int++-- | Raw name is simply an identifier.+type RawName = Id++-- | A raw scope is a set of raw names.+type RawScope = IntSet++-- | \(O(\min(n, W))\).+-- Generate a fresh raw name that+-- does not appear in a given raw scope.+rawFreshName :: RawScope -> RawName+rawFreshName scope | IntSet.null scope = 0+                   | otherwise = IntSet.findMax scope + 1++-- | Check if a raw name is contained in a raw scope.+rawMember :: RawName -> RawScope -> Bool+rawMember = IntSet.member++-- * Constraints++-- | Every scope is a (trivial) extension of itself.+--+-- __Important__: this class exists to assist tracking scope extensions+-- for type variables of kind 'S'.+-- Users of the foil are not supposed to implement any instances of 'ExtEndo'.+class ExtEndo (n :: S)++-- | Some scopes are extensions of other scopes.+--+-- __Important__: this class exists to assist tracking scope extensions+-- for type variables of kind 'S'.+-- Users of the foil are not supposed to implement any instances of 'Ext'.+class (ExtEndo n => ExtEndo l ) => Ext (n :: S) (l :: S)+instance ( ExtEndo n => ExtEndo l ) => Ext n l++-- | Scopes with distinct names.+--+-- __Important__: this class exists to explicitly+-- mark scopes with distinct names.+-- Users of the foil are not supposed to implement any instances of 'Distinct'.+class Distinct (n :: S)+instance Distinct VoidS++-- | Scope extensions with distinct names.+type DExt n l = (Distinct l, Ext n l)++-- | Instances of this typeclass possess the ability to inject names.+-- Usually, this is a variable data constructor.+class InjectName (e :: S -> Type) where+  -- | Inject names into expressions.+  injectName :: Name n -> e n
+ src/Control/Monad/Foil/Relative.hs view
@@ -0,0 +1,23 @@+{-# LANGUAGE KindSignatures        #-}+{-# LANGUAGE MultiParamTypeClasses #-}+module Control.Monad.Foil.Relative where++import           Control.Monad.Foil+import           Data.Kind          (Type)++-- | Relative monads, restricted to types indexed by scopes in kind 'S'.+class RelMonad (f :: S -> Type) (m :: S -> Type) where+  -- | Relative version of 'return'.+  rreturn :: f a -> m a++  -- | Relative version of '>>='.+  --+  -- Note the two special additions to the usual definition of a relative binding operation:+  --+  -- 1. @'Scope' b@ is added since is corresponds to the runtime counterpart of the type parameter @b@.+  -- 2. @t'Distinct' b@ constraint helps to ensure we only work with scopes that are distinct.+  --+  -- Technically, it is also possible add similar components for @a@ parameter.+  -- Also, we could probably treat types in 'S' as singletons and extract distinct scopes that way,+  -- preserving the more general type signature for 'rbind'.+  rbind :: Distinct b => Scope b -> m a -> (f a -> m b) -> m b
+ src/Control/Monad/Foil/TH.hs view
@@ -0,0 +1,11 @@+module Control.Monad.Foil.TH (+  module Control.Monad.Foil.TH.MkFoilData,+  module Control.Monad.Foil.TH.MkToFoil,+  module Control.Monad.Foil.TH.MkFromFoil,+  module Control.Monad.Foil.TH.MkInstancesFoil+) where++import           Control.Monad.Foil.TH.MkFoilData+import           Control.Monad.Foil.TH.MkFromFoil+import           Control.Monad.Foil.TH.MkInstancesFoil+import           Control.Monad.Foil.TH.MkToFoil
+ src/Control/Monad/Foil/TH/MkFoilData.hs view
@@ -0,0 +1,107 @@+{-# LANGUAGE GADTs                 #-}+{-# LANGUAGE QuasiQuotes           #-}+{-# LANGUAGE TemplateHaskellQuotes #-}+{-# OPTIONS_GHC -Wno-incomplete-patterns #-}+{-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}+module Control.Monad.Foil.TH.MkFoilData (mkFoilData) where++import           Language.Haskell.TH++import qualified Control.Monad.Foil.Internal as Foil+import Control.Monad.Foil.TH.Util++-- | Generate scope-safe variants given names of types for the raw representation.+mkFoilData+  :: Name -- ^ Type name for raw terms.+  -> Name -- ^ Type name for raw variable identifiers.+  -> Name -- ^ Type name for raw scoped terms.+  -> Name -- ^ Type name for raw patterns.+  -> Q [Dec]+mkFoilData termT nameT scopeT patternT = do+  n <- newName "n"+  l <- newName "l"+  TyConI (DataD _ctx _name patternTVars _kind patternCons _deriv) <- reify patternT+  TyConI (DataD _ctx _name scopeTVars _kind scopeCons _deriv) <- reify scopeT+  TyConI (DataD _ctx _name termTVars _kind termCons _deriv) <- reify termT++  foilPatternCons <- mapM (toPatternCon patternTVars n) patternCons+  let foilScopeCons = map (toScopeCon scopeTVars n) scopeCons+  let foilTermCons = map (toTermCon termTVars n l) termCons++  return+    [ DataD [] foilTermT (termTVars ++ [KindedTV n BndrReq (PromotedT ''Foil.S)]) Nothing foilTermCons []+    , DataD [] foilScopeT (scopeTVars ++ [KindedTV n BndrReq (PromotedT ''Foil.S)]) Nothing foilScopeCons []+    , DataD [] foilPatternT (patternTVars ++ [KindedTV n BndrReq (PromotedT ''Foil.S), KindedTV l BndrReq (PromotedT ''Foil.S)]) Nothing foilPatternCons []+    ]+  where+    foilTermT = mkName ("Foil" ++ nameBase termT)+    foilScopeT = mkName ("Foil" ++ nameBase scopeT)+    foilPatternT = mkName ("Foil" ++ nameBase patternT)++    -- | Convert a constructor declaration for a raw pattern type+    -- into a constructor for the scope-safe pattern type.+    toPatternCon+      :: [TyVarBndr BndrVis]+      -> Name   -- ^ Name for the starting scope type variable.+      -> Con    -- ^ Raw pattern constructor.+      -> Q Con+    toPatternCon tvars n (NormalC conName params) = do+      (lastScopeName, foilParams) <- toPatternConParams 1 n params+      let foilConName = mkName ("Foil" ++ nameBase conName)+      return (GadtC [foilConName] foilParams (PeelConT foilPatternT (map (VarT . tvarName) tvars ++ [VarT n, VarT lastScopeName])))+      where+        -- | Process type parameters of a pattern,+        -- introducing (existential) type variables for the intermediate scopes,+        -- if necessary.+        toPatternConParams+          :: Int                  -- ^ Index of the component in the constructor.+          -> Name                 -- ^ Current scope (after processing any previous bindings).+          -> [BangType]           -- ^ Leftover pattern components.+          -> Q (Name, [BangType]) -- ^ Resulting extended scope and a list of corresponding scope-safe components.+        toPatternConParams _ p [] = return (p, [])+        toPatternConParams i p (param@(bang_, type_) : conParams) =+          case type_ of+            -- if the current component is a variable identifier+            -- then treat it as a single name binder (see 'Foil.NameBinder')+            PeelConT tyName _tyParams | tyName == nameT -> do+              l <- newName ("n" <> show i)+              let type' = AppT (AppT (ConT ''Foil.NameBinder) (VarT p)) (VarT l)+              (l', conParams') <- toPatternConParams (i+1) l conParams+              return (l', (bang_, type') : conParams')+            -- if the current component is a raw pattern+            -- then convert it into a scope-safe pattern+            PeelConT tyName tyParams | tyName == patternT -> do+              l <- newName ("n" <> show i)+              let type' = PeelConT foilPatternT (tyParams ++ [VarT p, VarT l])+              (l', conParams') <- toPatternConParams (i+1) l conParams+              return (l', (bang_, type') : conParams')+            -- otherwise, ignore the component as non-binding+            _ -> do+              (l, conParams') <- toPatternConParams (i+1) p conParams+              return (l, param : conParams')++    -- | Convert a constructor declaration for a raw scoped term+    -- into a constructor for the scope-safe scoped term.+    toScopeCon :: [TyVarBndr BndrVis] -> Name -> Con -> Con+    toScopeCon _tvars n (NormalC conName params) =+      NormalC foilConName (map toScopeParam params)+      where+        foilConName = mkName ("Foil" ++ nameBase conName)+        toScopeParam (_bang, PeelConT tyName tyParams)+          | tyName == termT = (_bang, PeelConT foilTermT (tyParams ++ [VarT n]))+        toScopeParam _bangType = _bangType++    -- | Convert a constructor declaration for a raw term+    -- into a constructor for the scope-safe term.+    toTermCon :: [TyVarBndr BndrVis] -> Name -> Name -> Con -> Con+    toTermCon tvars n l (NormalC conName params) =+      GadtC [foilConName] (map toTermParam params) (PeelConT foilTermT (map (VarT . tvarName) tvars ++ [VarT n]))+      where+        foilNames = [n, l]+        foilConName = mkName ("Foil" ++ nameBase conName)+        toTermParam (_bang, PeelConT tyName tyParams)+          | tyName == patternT = (_bang, PeelConT foilPatternT (tyParams ++ map VarT foilNames))+          | tyName == nameT = (_bang, AppT (ConT ''Foil.Name) (VarT n))+          | tyName == scopeT = (_bang, PeelConT foilScopeT (tyParams ++ [VarT l]))+          | tyName == termT = (_bang, PeelConT foilTermT (tyParams ++ [VarT n]))+        toTermParam _bangType = _bangType
+ src/Control/Monad/Foil/TH/MkFromFoil.hs view
@@ -0,0 +1,232 @@+{-# OPTIONS_GHC -fno-warn-type-defaults #-}+{-# LANGUAGE GADTs                 #-}+{-# LANGUAGE LambdaCase            #-}+{-# LANGUAGE RankNTypes            #-}+{-# LANGUAGE QuasiQuotes           #-}+{-# LANGUAGE TemplateHaskellQuotes #-}+module Control.Monad.Foil.TH.MkFromFoil (mkFromFoil) where++import           Language.Haskell.TH+import Language.Haskell.TH.Syntax (addModFinalizer)++import qualified Control.Monad.Foil  as Foil+import Control.Monad.Foil.TH.Util++-- | Generate conversion functions from raw to scope-safe representation.+mkFromFoil+  :: Name -- ^ Type name for raw terms.+  -> Name -- ^ Type name for raw variable identifiers.+  -> Name -- ^ Type name for raw scoped terms.+  -> Name -- ^ Type name for raw patterns.+  -> Q [Dec]+mkFromFoil termT nameT scopeT patternT = do+  n <- newName "n"+  let ntype = return (VarT n)+  l <- newName "l"+  let ltype = return (VarT l)+  r <- newName "r"+  let rtype = return (VarT r)+  TyConI (DataD _ctx _name patternTVars _kind patternCons _deriv) <- reify patternT+  TyConI (DataD _ctx _name scopeTVars _kind scopeCons _deriv) <- reify scopeT+  TyConI (DataD _ctx _name termTVars _kind termCons _deriv) <- reify termT++  let termParams = map (VarT . tvarName) termTVars+  let scopeParams = map (VarT . tvarName) scopeTVars+  let patternParams = map (VarT . tvarName) patternTVars++  fromFoilTermSignature <-+    SigD fromFoilTermT <$>+      [t| [$(return (ConT nameT))]+          -> Foil.NameMap $ntype $(return (ConT nameT))+          -> $(return (PeelConT foilTermT termParams)) $ntype+          -> $(return (PeelConT termT termParams))+        |]+  fromFoilScopedSignature <-+    SigD fromFoilScopedT <$>+      [t| [$(return (ConT nameT))]+          -> Foil.NameMap $ntype $(return (ConT nameT))+          -> $(return (PeelConT foilScopeT scopeParams)) $ntype+          -> $(return (PeelConT scopeT scopeParams))+        |]+  fromFoilPatternSignature <-+    SigD fromFoilPatternT <$>+      [t| [$(return (ConT nameT))]+          -> Foil.NameMap $ntype $(return (ConT nameT))+          -> $(return (PeelConT foilPatternT patternParams)) $ntype $ltype+          -> ([$(return (ConT nameT))] -> Foil.NameMap $ltype $(return (ConT nameT)) -> $(return (PeelConT patternT patternParams)) -> $rtype)+          -> $rtype+        |]++  addModFinalizer $ putDoc (DeclDoc fromFoilTermT)+    "Convert a scope-safe term into a raw term."+  addModFinalizer $ putDoc (DeclDoc fromFoilPatternT)+    "Convert a scope-safe pattern into a raw pattern."+  addModFinalizer $ putDoc (DeclDoc fromFoilScopedT)+    "Convert a scope-safe scoped term into a raw scoped term."++  return+    [ fromFoilTermSignature+    , fromFoilTermBody termCons+    , fromFoilPatternSignature+    , fromFoilPatternBody patternCons+    , fromFoilScopedSignature+    , fromFoilScopedBody scopeCons+    ]+  where+    foilTermT = mkName ("Foil" ++ nameBase termT)+    foilScopeT = mkName ("Foil" ++ nameBase scopeT)+    foilPatternT = mkName ("Foil" ++ nameBase patternT)++    fromFoilTermT = mkName ("fromFoil" ++ nameBase termT)+    fromFoilPatternT = mkName ("fromFoil" ++ nameBase patternT)+    fromFoilScopedT = mkName ("fromFoil" ++ nameBase scopeT)++    fromFoilTermBody termCons = FunD fromFoilTermT+      [Clause [VarP freshVars, VarP env, VarP term] (NormalB (CaseE (VarE term) (map toMatch termCons))) []]+      where+        freshVars = mkName "freshVars"+        env = mkName "env"+        term = mkName "term"++        toMatch (NormalC conName params) =+          Match (ConP foilConName [] conParamPatterns) (NormalB conMatchBody) []+          where+            conMatchBody = go 1 (VarE freshVars) (VarE env) (ConE conName) params++            go _i _freshVars' _env' p [] = p+            go i freshVars' env' p ((_bang, PeelConT tyName _tyParams) : conParams)+              | tyName == nameT =+                  go (i+1) freshVars' env' (AppE p (AppE (AppE (VarE 'Foil.lookupName) (VarE xi)) env')) conParams+              | tyName == termT =+                  go (i+1) freshVars' env' (AppE p (AppE (AppE (AppE (VarE fromFoilTermT) (VarE freshVars)) (VarE env)) (VarE xi))) conParams+              | tyName == scopeT =+                  go (i+1) freshVars' env' (AppE p (AppE (AppE (AppE (VarE fromFoilScopedT) freshVars') env') (VarE xi))) conParams+              | tyName == patternT =+                  AppE+                    (AppE (AppE (AppE (VarE fromFoilPatternT) freshVars') env') (VarE xi))+                    (LamE [VarP freshVarsi, VarP envi, VarP xi']+                      (go (i+1) (VarE freshVarsi) (VarE envi) (AppE p (VarE xi')) conParams))+              where+                xi = mkName ("x" <> show i)+                xi' = mkName ("x" <> show i <> "'")+                freshVarsi = mkName ("freshVars" <> show i)+                envi = mkName ("env" <> show i)+            go i freshVars' env' p (_ : conParams) =+              go (i + 1) freshVars' env' (AppE p (VarE xi)) conParams+              where+                xi = mkName ("x" <> show i)++            foilConName = mkName ("Foil" ++ nameBase conName)+            conParamPatterns = map VarP conParamVars++            conParamVars = zipWith mkConParamVar params [1..]++            mkConParamVar :: BangType -> Int -> Name+            mkConParamVar _ty i = mkName ("x" <> show i)+        toMatch RecC{} = error "Record constructors (RecC) are not supported yet!"+        toMatch InfixC{} = error "Infix constructors (InfixC) are not supported yet!"+        toMatch ForallC{} = error "Existential constructors (ForallC) are not supported yet!"+        toMatch GadtC{} = error "GADT constructors (GadtC) are not supported yet!"+        toMatch RecGadtC{} = error "Record GADT constructors (RecGadtC) are not supported yet!"++    fromFoilPatternBody patternCons = FunD fromFoilPatternT+      [Clause [VarP freshVars, VarP env, VarP pattern, VarP cont] (NormalB (CaseE (VarE pattern) (map toMatch patternCons))) []]+      where+        freshVars = mkName "freshVars"+        env = mkName "env"+        pattern = mkName "pattern"+        cont = mkName "cont"++        toMatch (NormalC conName params) =+          Match (ConP foilConName [] conParamPatterns) (NormalB conMatchBody) []+          where+            conMatchBody = go 1 (VarE freshVars) (VarE env) (ConE conName) params++            go _i freshVars' env' p [] = AppE (AppE (AppE (VarE cont) freshVars') env') p+            go i freshVars' env' p ((_bang, PeelConT tyName _tyParams) : conParams)+              | tyName == nameT =+                  CaseE freshVars'+                    [ Match (ListP []) (NormalB (AppE (VarE 'error) (LitE (StringL "not enough fresh variables")))) []+                    , Match (InfixP (VarP var) '(:) (VarP vars))+                        (NormalB (LetE+                          [ValD (VarP envi) (NormalB (AppE (AppE (AppE (VarE 'Foil.addNameBinder) (VarE xi)) (VarE var)) env')) []]+                          (go (i + 1) (VarE vars) (VarE envi) (AppE p (VarE var)) conParams)))+                        []+                    ]+              | tyName == patternT =+                  AppE+                    (AppE (AppE (AppE (VarE fromFoilPatternT) freshVars') env') (VarE xi))+                    (LamE [VarP freshVarsi, VarP envi, VarP xi']+                      (go (i+1) (VarE freshVarsi) (VarE envi) (AppE p (VarE xi')) conParams))+              where+                var = mkName "var"+                vars = mkName "vars"+                xi = mkName ("x" <> show i)+                xi' = mkName ("x" <> show i <> "'")+                freshVarsi = mkName ("freshVars" <> show i)+                envi = mkName ("env" <> show i)+            go i freshVars' env' p (_ : conParams) =+              go (i + 1) freshVars' env' (AppE p (VarE xi)) conParams+              where+                xi = mkName ("x" <> show i)++            foilConName = mkName ("Foil" ++ nameBase conName)+            conParamPatterns = map VarP conParamVars++            conParamVars = zipWith mkConParamVar params [1..]++            mkConParamVar :: BangType -> Int -> Name+            mkConParamVar _ i = mkName ("x" <> show i)+        toMatch RecC{} = error "Record constructors (RecC) are not supported yet!"+        toMatch InfixC{} = error "Infix constructors (InfixC) are not supported yet!"+        toMatch ForallC{} = error "Existential constructors (ForallC) are not supported yet!"+        toMatch GadtC{} = error "GADT constructors (GadtC) are not supported yet!"+        toMatch RecGadtC{} = error "Record GADT constructors (RecGadtC) are not supported yet!"++    fromFoilScopedBody freshVarsCons = FunD fromFoilScopedT+      [Clause [VarP freshVars, VarP env, VarP term] (NormalB (CaseE (VarE term) (map toMatch freshVarsCons))) []]+      where+        freshVars = mkName "freshVars"+        env = mkName "env"+        term = mkName "term"++        toMatch (NormalC conName params) =+          Match (ConP foilConName [] conParamPatterns) (NormalB conMatchBody) []+          where+            conMatchBody = go 1 (VarE freshVars) (VarE env) (ConE conName) params++            go _i _freshVars' _env' p [] = p+            go i freshVars' env' p ((_bang, PeelConT tyName _tyParams) : conParams)+              | tyName == nameT =+                  go (i+1) freshVars' env' (AppE p (AppE (AppE (VarE 'Foil.lookupName) (VarE xi)) env')) conParams+              | tyName == termT =+                  go (i+1) freshVars' env' (AppE p (AppE (AppE (AppE (VarE fromFoilTermT) (VarE freshVars)) (VarE env)) (VarE xi))) conParams+              | tyName == scopeT =+                  go (i+1) freshVars' env' (AppE p (AppE (AppE (AppE (VarE fromFoilScopedT) freshVars') env') (VarE xi))) conParams+              | tyName == patternT =+                  AppE+                    (AppE (AppE (AppE (VarE fromFoilPatternT) freshVars') env') (VarE xi))+                    (LamE [VarP freshVarsi, VarP envi, VarP xi']+                      (go (i+1) (VarE freshVarsi) (VarE envi) (AppE p (VarE xi')) conParams))+              where+                xi = mkName ("x" <> show i)+                xi' = mkName ("x" <> show i <> "'")+                freshVarsi = mkName ("freshVars" <> show i)+                envi = mkName ("env" <> show i)+            go i freshVars' env' p (_ : conParams) =+              go (i + 1) freshVars' env' (AppE p (VarE xi)) conParams+              where+                xi = mkName ("x" <> show i)++            foilConName = mkName ("Foil" ++ nameBase conName)+            conParamPatterns = map VarP conParamVars++            conParamVars = zipWith mkConParamVar params [1..]++            mkConParamVar :: BangType -> Int -> Name+            mkConParamVar _ty i = mkName ("x" <> show i)+        toMatch RecC{} = error "Record constructors (RecC) are not supported yet!"+        toMatch InfixC{} = error "Infix constructors (InfixC) are not supported yet!"+        toMatch ForallC{} = error "Existential constructors (ForallC) are not supported yet!"+        toMatch GadtC{} = error "GADT constructors (GadtC) are not supported yet!"+        toMatch RecGadtC{} = error "Record GADT constructors (RecGadtC) are not supported yet!"
+ src/Control/Monad/Foil/TH/MkInstancesFoil.hs view
@@ -0,0 +1,115 @@+{-# LANGUAGE GADTs                 #-}+{-# LANGUAGE LambdaCase            #-}+{-# LANGUAGE QuasiQuotes           #-}+{-# LANGUAGE TemplateHaskellQuotes #-}+{-# OPTIONS_GHC -fno-warn-type-defaults #-}+module Control.Monad.Foil.TH.MkInstancesFoil (mkInstancesFoil) where++import           Language.Haskell.TH++import qualified Control.Monad.Foil  as Foil+import Control.Monad.Foil.TH.Util++-- | Generate 'Foil.Sinkable' and 'Foil.CoSinkable' instances.+mkInstancesFoil+  :: Name -- ^ Type name for raw terms.+  -> Name -- ^ Type name for raw variable identifiers.+  -> Name -- ^ Type name for raw scoped terms.+  -> Name -- ^ Type name for raw patterns.+  -> Q [Dec]+mkInstancesFoil termT nameT scopeT patternT = do+  TyConI (DataD _ctx _name patternTVars _kind patternCons _deriv) <- reify patternT+  TyConI (DataD _ctx _name scopeTVars _kind scopeCons _deriv) <- reify scopeT+  TyConI (DataD _ctx _name termTVars _kind termCons _deriv) <- reify termT++  return+    [ InstanceD Nothing [] (AppT (ConT ''Foil.Sinkable) (PeelConT foilScopeT (map (VarT . tvarName) scopeTVars)))+        [ FunD 'Foil.sinkabilityProof (map clauseScopedTerm scopeCons) ]++    , InstanceD Nothing [] (AppT (ConT ''Foil.CoSinkable) (PeelConT foilPatternT (map (VarT . tvarName) patternTVars)))+        [ FunD 'Foil.coSinkabilityProof (map clausePattern patternCons) ]++    , InstanceD Nothing [] (AppT (ConT ''Foil.Sinkable) (PeelConT foilTermT (map (VarT . tvarName) termTVars)))+        [ FunD 'Foil.sinkabilityProof (map clauseTerm termCons)]+    ]++  where+    foilTermT = mkName ("Foil" ++ nameBase termT)+    foilScopeT = mkName ("Foil" ++ nameBase scopeT)+    foilPatternT = mkName ("Foil" ++ nameBase patternT)++    clauseScopedTerm :: Con -> Clause+    clauseScopedTerm = clauseTerm++    clauseTerm :: Con -> Clause+    clauseTerm RecC{} = error "Record constructors (RecC) are not supported yet!"+    clauseTerm InfixC{} = error "Infix constructors (InfixC) are not supported yet!"+    clauseTerm ForallC{} = error "Existential constructors (ForallC) are not supported yet!"+    clauseTerm GadtC{} = error "GADT constructors (GadtC) are not supported yet!"+    clauseTerm RecGadtC{} = error "Record GADT constructors (RecGadtC) are not supported yet!"+    clauseTerm (NormalC conName params) =+      Clause+        [VarP rename, ConP foilConName [] conParamPatterns]+        (NormalB (go 1 (VarE rename) (ConE foilConName) params))+        []+      where+        foilConName = mkName ("Foil" ++ nameBase conName)+        rename = mkName "rename"+        conParamPatterns = zipWith mkConParamPattern params [1..]+        mkConParamPattern _ i = VarP (mkName ("x" ++ show i))++        go _i _rename' p [] = p+        go i rename' p ((_bang, PeelConT tyName _tyParams) : conParams)+          | tyName == nameT =+              go (i + 1) rename' (AppE p (AppE (VarE rename) (VarE xi))) conParams+          | tyName == termT =+              go (i + 1) rename' (AppE p (AppE (AppE (VarE 'Foil.sinkabilityProof) (VarE rename)) (VarE xi))) conParams+          | tyName == scopeT =+              go (i + 1) rename' (AppE p (AppE (AppE (VarE 'Foil.sinkabilityProof) rename') (VarE xi))) conParams+          | tyName == patternT =+              AppE+                (AppE (AppE (VarE 'Foil.coSinkabilityProof) rename') (VarE xi))+                (LamE [VarP renamei, VarP xi']+                  (go (i + 1) (VarE renamei) (AppE p (VarE xi')) conParams))+          where+            xi = mkName ("x" ++ show i)+            xi' = mkName ("x" ++ show i ++ "'")+            renamei = mkName ("rename" ++ show i)+        go i rename' p (_ : conPatterns) =+          go (i + 1) rename' (AppE p (VarE xi)) conPatterns+          where+            xi = mkName ("x" ++ show i)++    clausePattern :: Con -> Clause+    clausePattern RecC{} = error "Record constructors (RecC) are not supported yet!"+    clausePattern InfixC{} = error "Infix constructors (InfixC) are not supported yet!"+    clausePattern ForallC{} = error "Existential constructors (ForallC) are not supported yet!"+    clausePattern GadtC{} = error "GADT constructors (GadtC) are not supported yet!"+    clausePattern RecGadtC{} = error "Record GADT constructors (RecGadtC) are not supported yet!"+    clausePattern (NormalC conName params) =+      Clause+        [VarP rename, ConP foilConName [] conParamPatterns, VarP cont]+        (NormalB (go 1 (VarE rename) (ConE foilConName) params))+        []+      where+        foilConName = mkName ("Foil" ++ nameBase conName)+        rename = mkName "rename"+        cont = mkName "cont"+        conParamPatterns = zipWith mkConParamPattern params [1..]+        mkConParamPattern _ i = VarP (mkName ("x" ++ show i))++        go _i rename' p [] = AppE (AppE (VarE cont) rename') p+        go i rename' p ((_bang, PeelConT tyName _tyParams) : conParams)+          | tyName == nameT || tyName == patternT =+              AppE+                (AppE (AppE (VarE 'Foil.coSinkabilityProof) rename') (VarE xi))+                (LamE [VarP renamei, VarP xi']+                  (go (i + 1) (VarE renamei) (AppE p (VarE xi')) conParams))+          where+            xi = mkName ("x" ++ show i)+            xi' = mkName ("x" ++ show i ++ "'")+            renamei = mkName ("rename" ++ show i)+        go i rename' p (_ : conPatterns) =+          go (i + 1) rename' (AppE p (VarE xi)) conPatterns+          where+            xi = mkName ("x" ++ show i)
+ src/Control/Monad/Foil/TH/MkToFoil.hs view
@@ -0,0 +1,458 @@+{-# OPTIONS_GHC -fno-warn-type-defaults #-}+{-# LANGUAGE GADTs                 #-}+{-# LANGUAGE LambdaCase            #-}+{-# LANGUAGE RankNTypes            #-}+{-# LANGUAGE QuasiQuotes           #-}+{-# LANGUAGE TemplateHaskellQuotes #-}+module Control.Monad.Foil.TH.MkToFoil (mkToFoil) where++import           Language.Haskell.TH+import Language.Haskell.TH.Syntax (addModFinalizer)++import qualified Control.Monad.Foil  as Foil+import           Data.Maybe          (catMaybes)+import Data.Map (Map)+import qualified Data.Map as Map+import Control.Monad.Foil.TH.Util++-- | Generate conversion functions from raw to scope-safe representation.+mkToFoil+  :: Name -- ^ Type name for raw terms.+  -> Name -- ^ Type name for raw variable identifiers.+  -> Name -- ^ Type name for raw scoped terms.+  -> Name -- ^ Type name for raw patterns.+  -> Q [Dec]+mkToFoil termT nameT scopeT patternT = do+  extendScopeFoilPattenD <- mkExtendScopeFoilPattern nameT patternT+  withRefreshedFoilPatternD <- mkWithRefreshedFoilPattern nameT patternT+  toFoilTermD <- mkToFoilTerm termT nameT scopeT patternT+  return (+    extendScopeFoilPattenD +++    withRefreshedFoilPatternD +++    toFoilTermD+    )++-- | Generate a function to extend scope with variables from a given pattern.+mkExtendScopeFoilPattern+  :: Name -- ^ Type name for raw variable identifiers.+  -> Name -- ^ Type name for raw patterns.+  -> Q [Dec]+mkExtendScopeFoilPattern nameT patternT = do+  n <- newName "n"+  l <- newName "l"+  TyConI (DataD _ctx _name patternTVars _kind patternCons _deriv) <- reify patternT++  let extendScopePatternSignature =+        SigD extendScopePatternFunName $+          ForallT ([ PlainTV name SpecifiedSpec | name <- (map tvarName patternTVars ++ [n, l]) ]) []+            (AppT (AppT ArrowT+              (PeelConT foilPatternT [ VarT name | name <- (map tvarName patternTVars ++ [n, l]) ]))+              (AppT (AppT ArrowT+                (AppT (ConT ''Foil.Scope) (VarT n)))+                (AppT (ConT ''Foil.Scope) (VarT l))))++  composefun <- [e| (.) |]+  idfun <- [e| id |]+  extendScopeFun <- [e| Foil.extendScope |]++  addModFinalizer $ putDoc (DeclDoc extendScopePatternFunName)+    "Extend a scope with the names bound by the given pattern.\nThis is a more flexible version of 'Control.Monad.Foil.extendScope'."++  return+    [ extendScopePatternSignature+    , extendScopePatternBody extendScopeFun composefun idfun patternCons+    ]+  where+    foilPatternT = mkName ("Foil" ++ nameBase patternT)++    extendScopePatternFunName = mkName ("extendScopeFoil" ++ nameBase patternT)+    extendScopePatternBody extendScopeFun composefun idfun patternCons = FunD extendScopePatternFunName+      [Clause [VarP p] (NormalB (CaseE (VarE p) (map toMatch patternCons))) []]+      where+        p = mkName "pattern"+        toMatch (NormalC conName conParams) =+          Match (ConP foilConName [] conParamPatterns) (NormalB conMatchBody) []+          where+            foilConName = mkName ("Foil" ++ nameBase conName)+            conParamPatterns = map toConParamPattern conParamVars+            conMatchExts = map snd (catMaybes conParamVars)+            conMatchBody = foldr (\f g -> InfixE (Just g) composefun (Just f)) idfun conMatchExts++            toConParamPattern Nothing = WildP+            toConParamPattern (Just (x, _f)) = VarP x++            conParamVars = zipWith mkConParamVar conParams [1..]++            mkConParamVar :: BangType -> Int -> Maybe (Name, Exp)+            mkConParamVar (_bang, PeelConT tyName _tyParams) i+              | tyName == nameT    = Just (x, AppE extendScopeFun (VarE x))+              | tyName == patternT = Just (x, AppE (VarE extendScopePatternFunName) (VarE x))+              where+                x = mkName ("x" <> show i)+            mkConParamVar (_bang, _type) _i = Nothing+        toMatch RecC{} = error "Record constructors (RecC) are not supported yet!"+        toMatch InfixC{} = error "Infix constructors (InfixC) are not supported yet!"+        toMatch ForallC{} = error "Existential constructors (ForallC) are not supported yet!"+        toMatch GadtC{} = error "GADT constructors (GadtC) are not supported yet!"+        toMatch RecGadtC{} = error "Record GADT constructors (RecGadtC) are not supported yet!"++-- | Generate a function to extend scope with variables from a given pattern.+mkWithRefreshedFoilPattern+  :: Name -- ^ Type name for raw variable identifiers.+  -> Name -- ^ Type name for raw patterns.+  -> Q [Dec]+mkWithRefreshedFoilPattern nameT patternT = do+  o <- newName "o"+  o' <- newName "o'"+  e <- newName "e"+  n <- newName "n"+  l <- newName "l"+  r <- newName "r"+  TyConI (DataD _ctx _name patternTVars _kind patternCons _deriv) <- reify patternT++  let withRefreshedFoilPatternSignature =+        SigD withRefreshedFoilPatternFunName $+          ForallT+            [ PlainTV name SpecifiedSpec | name <- map tvarName patternTVars ++ [o, e, n, l, r] ]+            [ AppT (ConT ''Foil.Distinct) (VarT o)+            , AppT (ConT ''Foil.InjectName) (VarT e)+            , AppT (ConT ''Foil.Sinkable) (VarT e)+            ]+            (AppT (AppT ArrowT (PeelConT ''Foil.Scope [VarT o]))+              (AppT (AppT ArrowT (PeelConT foilPatternT (map (VarT . tvarName) patternTVars ++ [VarT n, VarT l])))+                (AppT (AppT ArrowT+                  (ForallT [PlainTV o' SpecifiedSpec] [PeelConT ''Foil.DExt [VarT o, VarT o']]+                    (AppT (AppT ArrowT (AppT (AppT ArrowT (PeelConT ''Foil.Substitution [VarT e, VarT n, VarT o])) (PeelConT ''Foil.Substitution [VarT e, VarT l, VarT o'])))+                      (AppT (AppT ArrowT (PeelConT foilPatternT (map (VarT . tvarName) patternTVars ++ [VarT o, VarT o'])))+                        (VarT r)))))+                  (VarT r))))++        --           [t| ( Foil.Distinct o, Foil.InjectName e, Foil.Sinkable e )+        --     => Foil.Scope o+        --     -> $(return (PeelConT foilPatternT (map (VarT . tyName patternTVars)))) n l+        --     -> (forall o'. Foil.DExt o o'+        --           => (Foil.Substitution e n o -> Foil.Substitution e l o')+        --           -> $(return (ConT foilPatternT)) o o'+        --           -> r)+        --     -> r+        -- |]++  composefun <- [e| (.) |]+  addRenameFun <- [e| Foil.addRename |]+  nameOfFun <- [e| Foil.nameOf |]+  sinkFun <- [e| Foil.sink |]+  withRefreshedFun <- [e| Foil.withRefreshed |]+  extendScopeFun <- [e| Foil.extendScope |]++  addModFinalizer $ putDoc (DeclDoc withRefreshedFoilPatternFunName)+    "Refresh (if needed) bound variables introduced in a pattern.\nThis is a more flexible version of 'Control.Monad.Foil.withRefreshed'."++  return+    [ withRefreshedFoilPatternSignature+    , withRefreshedFoilPatternBody composefun addRenameFun nameOfFun sinkFun withRefreshedFun extendScopeFun patternCons+    ]+  where+    foilPatternT = mkName ("Foil" ++ nameBase patternT)++    extendScopePatternFunName = mkName ("extendScopeFoil" ++ nameBase patternT)+    extendScopePatternFun = VarE extendScopePatternFunName++    withRefreshedFoilPatternFunName = mkName ("withRefreshedFoil" ++ nameBase patternT)+    withRefreshedFoilPatternFun = VarE withRefreshedFoilPatternFunName++    withRefreshedFoilPatternBody composefun addRenameFun nameOfFun sinkFun withRefreshedFun extendScopeFun patternCons = FunD withRefreshedFoilPatternFunName+      [Clause [VarP scope, VarP pattern, VarP cont] (NormalB (CaseE (VarE pattern) (map toMatch patternCons))) []]+      where+        scope = mkName "scope"+        pattern = mkName "pattern"+        cont = mkName "cont"++        toMatch (NormalC conName params) =+          Match (ConP foilConName [] conParamPatterns) (NormalB conMatchBody) []+          where+            conMatchBody = go 1 (VarE scope) sinkFun (ConE foilConName) params++            go _i _scope' f p [] = AppE (AppE (VarE cont) f) p+            go i scope' f p ((_bang, PeelConT tyName _tyParams) : conParams)+              | tyName == nameT =+                  AppE+                    (AppE (AppE withRefreshedFun scope') (AppE nameOfFun (VarE xi)))+                    (LamE [VarP xi']+                      (LetE [ValD (VarP scopei) (NormalB (AppE (AppE extendScopeFun (VarE xi')) scope')) []]+                        (go (i+1) (VarE scopei) (InfixE (Just fi) composefun (Just f)) (AppE p (VarE xi')) conParams)))+              | tyName == patternT =+                  AppE+                    (AppE (AppE withRefreshedFoilPatternFun scope') (VarE xi))+                    (LamE [VarP xsubst, VarP xi']+                      (LetE [ValD (VarP scopei) (NormalB (AppE (AppE extendScopePatternFun (VarE xi')) scope')) []]+                        (go (i+1) (VarE scopei) (InfixE (Just (VarE xsubst)) composefun (Just f)) (AppE p (VarE xi')) conParams)))+              where+                xi = mkName ("x" <> show i)+                xi' = mkName ("x" <> show i <> "'")+                scopei = mkName ("scope" <> show i)+                xsubst = mkName ("subst" <> show i)+                subst = mkName "subst"+                fi = LamE [VarP subst]+                      (AppE (AppE (AppE addRenameFun+                        (VarE subst))+                        (VarE xi))+                        (AppE nameOfFun (VarE xi')))+            go i scope' f p (_ : conParams) =+              go (i + 1) scope' f (AppE p (VarE xi)) conParams+              where+                xi = mkName ("x" <> show i)++            foilConName = mkName ("Foil" ++ nameBase conName)+            conParamPatterns = map VarP conParamVars++            conParamVars = zipWith mkConParamVar params [1..]++            mkConParamVar :: BangType -> Int -> Name+            mkConParamVar _ i = mkName ("x" <> show i)++        toMatch RecC{} = error "Record constructors (RecC) are not supported yet!"+        toMatch InfixC{} = error "Infix constructors (InfixC) are not supported yet!"+        toMatch ForallC{} = error "Existential constructors (ForallC) are not supported yet!"+        toMatch GadtC{} = error "GADT constructors (GadtC) are not supported yet!"+        toMatch RecGadtC{} = error "Record GADT constructors (RecGadtC) are not supported yet!"++-- | Generate a conversion function from raw terms to scope-safe terms.+mkToFoilTerm+  :: Name -- ^ Type name for raw terms.+  -> Name -- ^ Type name for raw variable identifiers.+  -> Name -- ^ Type name for raw scoped terms.+  -> Name -- ^ Type name for raw patterns.+  -> Q [Dec]+mkToFoilTerm termT nameT scopeT patternT = do+  n <- newName "n"+  let ntype = return (VarT n)+  r <- newName "r"+  let rtype = return (VarT r)+  TyConI (DataD _ctx _name patternTVars _kind patternCons _deriv) <- reify patternT+  TyConI (DataD _ctx _name scopeTVars _kind scopeCons _deriv) <- reify scopeT+  TyConI (DataD _ctx _name termTVars _kind termCons _deriv) <- reify termT++  toFoilTermSignature <-+    SigD toFoilTermT <$>+      [t| Foil.Distinct $ntype+          => Foil.Scope $ntype+          -> Map $(return (ConT nameT)) (Foil.Name $ntype)+          -> $(return (PeelConT termT (map (VarT . tvarName) termTVars )))+          -> $(return (PeelConT foilTermT (map (VarT . tvarName) termTVars))) $ntype+        |]+  toFoilScopedSignature <-+    SigD toFoilScopedT <$>+      [t| Foil.Distinct $ntype+          => Foil.Scope $ntype+          -> Map $(return (ConT nameT)) (Foil.Name $ntype)+          -> $(return (PeelConT scopeT (map (VarT . tvarName) scopeTVars)))+          -> $(return (PeelConT foilScopeT (map (VarT . tvarName) scopeTVars))) $ntype+        |]+  toFoilPatternSignature <-+    SigD toFoilPatternT <$>+      [t| Foil.Distinct $ntype+          => Foil.Scope $ntype+          -> Map $(return (ConT nameT)) (Foil.Name $ntype)+          -> $(return (PeelConT patternT (map (VarT . tvarName) patternTVars)))+          -> (forall l. Foil.DExt $ntype l => $(return (PeelConT foilPatternT (map (VarT . tvarName) patternTVars))) $ntype l -> Map $(return (ConT nameT)) (Foil.Name l) -> $rtype)+          -> $rtype+        |]++  addModFinalizer $ putDoc (DeclDoc toFoilTermT)+    "Convert a raw term into a scope-safe term."+  addModFinalizer $ putDoc (DeclDoc toFoilPatternT)+    "Convert a raw pattern into a scope-safe pattern."+  addModFinalizer $ putDoc (DeclDoc toFoilScopedT)+    "Convert a raw scoped term into a scope-safe scoped term."++  return+    [ toFoilTermSignature+    , toFoilTermBody termCons+    , toFoilPatternSignature+    , toFoilPatternBody patternCons+    , toFoilScopedSignature+    , toFoilScopedBody scopeCons+    ]+  where+    foilTermT = mkName ("Foil" ++ nameBase termT)+    foilScopeT = mkName ("Foil" ++ nameBase scopeT)+    foilPatternT = mkName ("Foil" ++ nameBase patternT)++    toFoilTermT = mkName ("toFoil" ++ nameBase termT)+    toFoilPatternT = mkName ("toFoil" ++ nameBase patternT)+    toFoilScopedT = mkName ("toFoil" ++ nameBase scopeT)++    extendScopePatternFunName = mkName ("extendScopeFoil" ++ nameBase patternT)+    extendScopePatternFun = VarE extendScopePatternFunName++    toFoilTermBody termCons = FunD toFoilTermT+      [Clause [VarP scope, VarP env, VarP term] (NormalB (CaseE (VarE term) (map toMatch termCons))) []]+      where+        scope = mkName "scope"+        env = mkName "env"+        term = mkName "term"++        toMatch (NormalC conName params) =+          Match (ConP conName [] conParamPatterns) (NormalB conMatchBody) [toFoilVarD]+          where+            toFoilVarFunName = mkName "lookupRawVar"+            toFoilVarFun = VarE toFoilVarFunName+            x = mkName "x"+            name = mkName "name"+            toFoilVarD = FunD toFoilVarFunName [Clause [VarP x]+              (NormalB (CaseE (AppE (AppE (VarE 'Map.lookup) (VarE x)) (VarE env))+                [ Match (ConP 'Just [] [VarP name]) (NormalB (VarE name)) []+                , Match (ConP 'Nothing [] []) (NormalB (AppE (VarE 'error) (LitE (StringL "undefined variable")))) []]))+              []]++            conMatchBody = go 1 (VarE scope) (VarE env) (ConE foilConName) params++            go _i _scope' _env' p [] = p+            go i scope' env' p ((_bang, PeelConT tyName _tyParams) : conParams)+              | tyName == nameT =+                  go (i+1) scope' env' (AppE p (AppE toFoilVarFun (VarE xi))) conParams+              | tyName == termT =+                  go (i+1) scope' env' (AppE p (AppE (AppE (AppE (VarE toFoilTermT) (VarE scope)) (VarE env)) (VarE xi))) conParams+              | tyName == scopeT =+                  go (i+1) scope' env' (AppE p (AppE (AppE (AppE (VarE toFoilScopedT) scope') env') (VarE xi))) conParams+              | tyName == patternT =+                  AppE+                    (AppE (AppE (AppE (VarE toFoilPatternT) scope') env') (VarE xi))+                    (LamE [VarP xi', VarP envi]+                      (LetE [ValD (VarP scopei) (NormalB (AppE (AppE extendScopePatternFun (VarE xi')) scope')) []]+                        (go (i+1) (VarE scopei) (VarE envi) (AppE p (VarE xi')) conParams)))+              where+                xi = mkName ("x" <> show i)+                xi' = mkName ("x" <> show i <> "'")+                scopei = mkName ("scope" <> show i)+                envi = mkName ("env" <> show i)+            go i scope' env' p (_ : conParams) =+              go (i + 1) scope' env' (AppE p (VarE xi)) conParams+              where+                xi = mkName ("x" <> show i)++            foilConName = mkName ("Foil" ++ nameBase conName)+            conParamPatterns = map VarP conParamVars++            conParamVars = zipWith mkConParamVar params [1..]++            mkConParamVar :: BangType -> Int -> Name+            mkConParamVar _ty i = mkName ("x" <> show i)+        toMatch RecC{} = error "Record constructors (RecC) are not supported yet!"+        toMatch InfixC{} = error "Infix constructors (InfixC) are not supported yet!"+        toMatch ForallC{} = error "Existential constructors (ForallC) are not supported yet!"+        toMatch GadtC{} = error "GADT constructors (GadtC) are not supported yet!"+        toMatch RecGadtC{} = error "Record GADT constructors (RecGadtC) are not supported yet!"++    toFoilPatternBody patternCons = FunD toFoilPatternT+      [Clause [VarP scope, VarP env, VarP pattern, VarP cont] (NormalB (CaseE (VarE pattern) (map toMatch patternCons))) []]+      where+        scope = mkName "scope"+        env = mkName "env"+        pattern = mkName "pattern"+        cont = mkName "cont"++        toMatch (NormalC conName params) =+          Match (ConP conName [] conParamPatterns) (NormalB conMatchBody) []+          where+            conMatchBody = go 1 (VarE scope) (VarE env) (ConE foilConName) params++            go _i _scope' env' p [] = AppE (AppE (VarE cont) p) env'+            go i scope' env' p ((_bang, PeelConT tyName _tyParams) : conParams)+              | tyName == nameT =+                  AppE (AppE (VarE 'Foil.withFresh) scope')+                    (LamE [VarP xi']+                      (LetE [ ValD (VarP scopei) (NormalB (AppE (AppE (VarE 'Foil.extendScope) (VarE xi')) scope')) []+                            , ValD (VarP envi) (NormalB+                                (AppE (AppE (AppE (VarE 'Map.insert) (VarE xi))+                                  (AppE (VarE 'Foil.nameOf) (VarE xi')))+                                  (InfixE (Just (VarE 'Foil.sink)) (VarE '(<$>)) (Just (VarE envi))))) []]+                        (go (i+1) (VarE scopei) (VarE envi) (AppE p (VarE xi')) conParams)))+              | tyName == patternT =+                  AppE+                    (AppE (AppE (AppE (VarE toFoilPatternT) scope') env') (VarE xi))+                    (LamE [VarP xi', VarP envi]+                      (LetE [ValD (VarP scopei) (NormalB (AppE (AppE extendScopePatternFun (VarE xi')) scope')) []]+                        (go (i+1) (VarE scopei) (VarE envi) (AppE p (VarE xi')) conParams)))+              where+                xi = mkName ("x" <> show i)+                xi' = mkName ("x" <> show i <> "'")+                scopei = mkName ("scope" <> show i)+                envi = mkName ("env" <> show i)+            go i scope' env' p (_ : conParams) =+              go (i + 1) scope' env' (AppE p (VarE xi)) conParams+              where+                xi = mkName ("x" <> show i)++            foilConName = mkName ("Foil" ++ nameBase conName)+            conParamPatterns = map VarP conParamVars++            conParamVars = zipWith mkConParamVar params [1..]++            mkConParamVar :: BangType -> Int -> Name+            mkConParamVar _ i = mkName ("x" <> show i)+        toMatch RecC{} = error "Record constructors (RecC) are not supported yet!"+        toMatch InfixC{} = error "Infix constructors (InfixC) are not supported yet!"+        toMatch ForallC{} = error "Existential constructors (ForallC) are not supported yet!"+        toMatch GadtC{} = error "GADT constructors (GadtC) are not supported yet!"+        toMatch RecGadtC{} = error "Record GADT constructors (RecGadtC) are not supported yet!"++    toFoilScopedBody scopeCons = FunD toFoilScopedT+      [Clause [VarP scope, VarP env, VarP term] (NormalB (CaseE (VarE term) (map toMatch scopeCons))) []]+      where+        scope = mkName "scope"+        env = mkName "env"+        term = mkName "term"++        toMatch (NormalC conName params) =+          Match (ConP conName [] conParamPatterns) (NormalB conMatchBody) [toFoilVarD]+          where+            toFoilVarFunName = mkName "lookupRawVar"+            toFoilVarFun = VarE toFoilVarFunName+            x = mkName "x"+            name = mkName "name"+            toFoilVarD = FunD toFoilVarFunName [Clause [VarP x]+              (NormalB (CaseE (AppE (AppE (VarE 'Map.lookup) (VarE x)) (VarE env))+                [ Match (ConP 'Just [] [VarP name]) (NormalB (VarE name)) []+                , Match (ConP 'Nothing [] []) (NormalB (AppE (VarE 'error) (LitE (StringL "undefined variable")))) []]))+              []]++            conMatchBody = go 1 (VarE scope) (VarE env) (ConE foilConName) params++            go _i _scope' _env' p [] = p+            go i scope' env' p ((_bang, PeelConT tyName _tyParams) : conParams)+              | tyName == nameT =+                  go (i+1) scope' env' (AppE p (AppE toFoilVarFun (VarE xi))) conParams+              | tyName == termT =+                  go (i+1) scope' env' (AppE p (AppE (AppE (AppE (VarE toFoilTermT) (VarE scope)) (VarE env)) (VarE xi))) conParams+              | tyName == scopeT =+                  go (i+1) scope' env' (AppE p (AppE (AppE (AppE (VarE toFoilScopedT) scope') env') (VarE xi))) conParams+              | tyName == patternT =+                  AppE+                    (AppE (AppE (AppE (VarE toFoilPatternT) scope') env') (VarE xi))+                    (LamE [VarP xi', VarP envi]+                      (LetE [ValD (VarP scopei) (NormalB (AppE (AppE extendScopePatternFun (VarE xi')) scope')) []]+                        (go (i+1) (VarE scopei) (VarE envi) (AppE p (VarE xi')) conParams)))+              where+                xi = mkName ("x" <> show i)+                xi' = mkName ("x" <> show i <> "'")+                scopei = mkName ("scope" <> show i)+                envi = mkName ("env" <> show i)+            go i scope' env' p (_ : conParams) =+              go (i + 1) scope' env' (AppE p (VarE xi)) conParams+              where+                xi = mkName ("x" <> show i)++            foilConName = mkName ("Foil" ++ nameBase conName)+            conParamPatterns = map VarP conParamVars++            conParamVars = zipWith mkConParamVar params [1..]++            mkConParamVar :: BangType -> Int -> Name+            mkConParamVar _ty i = mkName ("x" <> show i)++        toMatch RecC{} = error "Record constructors (RecC) are not supported yet!"+        toMatch InfixC{} = error "Infix constructors (InfixC) are not supported yet!"+        toMatch ForallC{} = error "Existential constructors (ForallC) are not supported yet!"+        toMatch GadtC{} = error "GADT constructors (GadtC) are not supported yet!"+        toMatch RecGadtC{} = error "Record GADT constructors (RecGadtC) are not supported yet!"
+ src/Control/Monad/Foil/TH/Util.hs view
@@ -0,0 +1,26 @@+{-# LANGUAGE PatternSynonyms                 #-}+{-# LANGUAGE ViewPatterns                 #-}+{-# LANGUAGE LambdaCase            #-}+module Control.Monad.Foil.TH.Util where++import Language.Haskell.TH++peelConT :: Type -> Maybe (Name, [Type])+peelConT (ConT name) = Just (name, [])+peelConT (AppT f x) =+  case peelConT f of+    Just (g, xs) -> Just (g, xs ++ [x])+    Nothing -> Nothing+peelConT _ = Nothing++unpeelConT :: Name -> [Type] -> Type+unpeelConT = foldl AppT . ConT++pattern PeelConT :: Name -> [Type] -> Type+pattern PeelConT name types <- (peelConT -> Just (name, types)) where+  PeelConT name types = unpeelConT name types++tvarName :: TyVarBndr a -> Name+tvarName = \case+  PlainTV name _ -> name+  KindedTV name _ _ -> name
+ src/Control/Monad/Free/Foil.hs view
@@ -0,0 +1,89 @@+{-# LANGUAGE DataKinds             #-}+{-# LANGUAGE DeriveAnyClass        #-}+{-# LANGUAGE DeriveGeneric         #-}+{-# LANGUAGE FlexibleContexts      #-}+{-# LANGUAGE FlexibleInstances     #-}+{-# LANGUAGE GADTs                 #-}+{-# LANGUAGE LambdaCase            #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE PolyKinds             #-}+{-# LANGUAGE QuantifiedConstraints #-}+{-# LANGUAGE StandaloneDeriving    #-}+{-# LANGUAGE UndecidableInstances  #-}+-- | This module defines a variation of+-- free scoped (relative) monads relying on the foil for+-- the scope-safe efficient handling of the binders.+--+-- See description of the approach in [«Free Foil: Generating Efficient and Scope-Safe Abstract Syntax»](https://arxiv.org/abs/2405.16384).+module Control.Monad.Free.Foil where++import           Control.DeepSeq+import qualified Control.Monad.Foil.Internal as Foil+import qualified Control.Monad.Foil.Relative as Foil+import           Data.Bifunctor+import           GHC.Generics                (Generic)++-- | Scoped term under a (single) name binder.+data ScopedAST sig n where+  ScopedAST :: Foil.NameBinder n l -> AST sig l -> ScopedAST sig n++instance (forall l. NFData (AST sig l)) => NFData (ScopedAST sig n) where+  rnf (ScopedAST binder body) = rnf binder `seq` rnf body++-- | A term, generated by a signature 'Bifunctor' @sig@,+-- with (free) variables in scope @n@.+data AST sig n where+  -- | A (free) variable in scope @n@.+  Var :: Foil.Name n -> AST sig n+  -- | A non-variable syntactic construction specified by the signature 'Bifunctor' @sig@.+  Node :: sig (ScopedAST sig n) (AST sig n) -> AST sig n++deriving instance Generic (AST sig n)+deriving instance (forall scope term. (NFData scope, NFData term) => NFData (sig scope term)) => NFData (AST sig n)++instance Bifunctor sig => Foil.Sinkable (AST sig) where+  sinkabilityProof rename = \case+    Var name -> Var (rename name)+    Node node -> Node (bimap f (Foil.sinkabilityProof rename) node)+    where+      f (ScopedAST binder body) =+        Foil.extendRenaming rename binder $ \rename' binder' ->+          ScopedAST binder' (Foil.sinkabilityProof rename' body)++instance Foil.InjectName (AST sig) where+  injectName = Var++-- | Substitution for free (scoped monads).+substitute+  :: (Bifunctor sig, Foil.Distinct o)+  => Foil.Scope o+  -> Foil.Substitution (AST sig) i o+  -> AST sig i+  -> AST sig o+substitute scope subst = \case+  Var name -> Foil.lookupSubst subst name+  Node node -> Node (bimap f (substitute scope subst) node)+  where+    f (ScopedAST binder body) =+      Foil.withRefreshed scope (Foil.nameOf binder) $ \binder' ->+        let subst' = Foil.addRename (Foil.sink subst) binder (Foil.nameOf binder')+            scope' = Foil.extendScope binder' scope+            body' = substitute scope' subst' body+        in ScopedAST binder' body'++-- | @'AST' sig@ is a monad relative to 'Foil.Name'.+instance Bifunctor sig => Foil.RelMonad Foil.Name (AST sig) where+  rreturn = Var+  rbind scope term subst =+    case term of+      Var name  -> subst name+      Node node -> Node (bimap g' g node)+    where+      g x = Foil.rbind scope x subst+      g' (ScopedAST binder body) =+        Foil.withRefreshed scope (Foil.nameOf binder) $ \binder' ->+          let scope' = Foil.extendScope binder' scope+              subst' name = case Foil.unsinkName binder name of+                          Nothing -> Foil.rreturn (Foil.nameOf binder')+                          Just n  -> Foil.sink (subst n)+           in ScopedAST binder' (Foil.rbind scope' body subst')
+ src/Control/Monad/Free/Foil/Example.hs view
@@ -0,0 +1,125 @@+{-# LANGUAGE DataKinds         #-}+{-# LANGUAGE DeriveFunctor     #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GADTs             #-}+{-# LANGUAGE LambdaCase        #-}+{-# LANGUAGE PatternSynonyms   #-}+{-# LANGUAGE RankNTypes        #-}+{-# LANGUAGE TemplateHaskell   #-}+-- | Example implementation of untyped \(\lambda\)-calculus with the foil.+module Control.Monad.Free.Foil.Example where++import           Control.Monad.Foil+import           Control.Monad.Free.Foil+import           Data.Bifunctor.TH++-- $setup+-- >>> import Control.Monad.Foil++-- | Untyped \(\lambda\)-terms in scope @n@.+data ExprF scope term+  -- | Application of one term to another: \((t_1, t_2)\)+  = AppF term term+  -- | \(\lambda\)-abstraction introduces a binder and a term in an extended scope: \(\lambda x. t\)+  | LamF scope+  deriving (Functor)+deriveBifunctor ''ExprF++pattern AppE :: AST ExprF n -> AST ExprF n -> AST ExprF n+pattern AppE x y = Node (AppF x y)++pattern LamE :: NameBinder n l -> AST ExprF l -> AST ExprF n+pattern LamE binder body = Node (LamF (ScopedAST binder body))++{-# COMPLETE Var, AppE, LamE #-}++type Expr = AST ExprF++-- | Use 'ppExpr' to show \(\lambda\)-terms.+instance Show (Expr n) where+  show = ppExpr++-- | Compute weak head normal form (WHNF) of a \(\lambda\)-term.+--+-- >>> whnf emptyScope (AppE (churchN 2) (churchN 2))+-- λx1. (λx0. λx1. (x0 (x0 x1)) (λx0. λx1. (x0 (x0 x1)) x1))+whnf :: Distinct n => Scope n -> Expr n -> Expr n+whnf scope = \case+  AppE fun arg ->+    case whnf scope fun of+      LamE binder body ->+        let subst = addSubst identitySubst binder arg+        in whnf scope (substitute scope subst body)+      fun' -> AppE fun' arg+  t -> t++-- | Compute weak head normal form (WHNF) of a __closed__ \(\lambda\)-term.+--+-- >>> whnf' (AppE (churchN 2) (churchN 2))+-- λx1. (λx0. λx1. (x0 (x0 x1)) (λx0. λx1. (x0 (x0 x1)) x1))+whnf' :: Expr VoidS -> Expr VoidS+whnf' = whnf emptyScope++-- | Compute normal form (NF) of a \(\lambda\)-term.+--+-- >>> nf emptyScope (AppE (churchN 2) (churchN 2))+-- λx1. λx2. (x1 (x1 (x1 (x1 x2))))+nf :: Distinct n => Scope n -> Expr n -> Expr n+nf scope expr = case expr of+  LamE binder body ->+    -- Instead of using 'assertDistinct',+    -- another option is to add 'Distinct l' constraint+    -- to the definition of 'LamE'.+    case assertDistinct binder of+      Distinct ->+        let scope' = extendScope binder scope+        in LamE binder (nf scope' body)+  AppE fun arg ->+    case whnf scope fun of+      LamE binder body ->+        let subst = addSubst identitySubst binder arg+        in nf scope (substitute scope subst body)+      fun' -> AppE (nf scope fun') (nf scope arg)+  t -> t++-- | Compute normal form (NF) of a __closed__ \(\lambda\)-term.+--+-- >>> nf' (AppE (churchN 2) (churchN 2))+-- λx1. λx2. (x1 (x1 (x1 (x1 x2))))+nf' :: Expr VoidS -> Expr VoidS+nf' = nf emptyScope++-- | Pretty print a name.+ppName :: Name n -> String+ppName name = "x" <> show (nameId name)++-- | Pretty-print a \(\lambda\)-term.+--+-- >>> ppExpr (churchN 3)+-- "\955x0. \955x1. (x0 (x0 (x0 x1)))"+ppExpr :: Expr n -> String+ppExpr = \case+  Var name -> ppName name+  AppE x y -> "(" <> ppExpr x <> " " <> ppExpr y <> ")"+  LamE binder body -> "λ" <> ppName (nameOf binder) <> ". " <> ppExpr body++-- | A helper for constructing \(\lambda\)-abstractions.+lam :: Distinct n => Scope n -> (forall l. DExt n l => Scope l -> NameBinder n l -> Expr l) -> Expr n+lam scope mkBody = withFresh scope $ \x ->+  let scope' = extendScope x scope+   in LamE x (mkBody scope' x)++-- | Church-encoding of a natural number \(n\).+--+-- >>> churchN 0+-- λx0. λx1. x1+--+-- >>> churchN 3+-- λx0. λx1. (x0 (x0 (x0 x1)))+churchN :: Int -> Expr VoidS+churchN n =+  lam emptyScope $ \sx nx ->+    lam sx $ \_sxy ny ->+      let x = sink (Var (nameOf nx))+          y = Var (nameOf ny)+       in iterate (AppE x) y !! n
+ test/Spec.hs view
@@ -0,0 +1,2 @@+main :: IO ()+main = putStrLn "Test suite not yet implemented"
+ test/doctests/Main.hs view
@@ -0,0 +1,7 @@+module Main where++import System.Environment (getArgs)+import Test.DocTest (mainFromCabal)++main :: IO ()+main = mainFromCabal "free-foil" =<< getArgs