free-foil 0.1.0 → 0.2.0

raw patch · 9 files changed

+1705/−24 lines, 9 filesdep +kind-genericsPVP ok

version bump matches the API change (PVP)

Dependencies added: kind-generics

API changes (from Hackage documentation)

Files

• ChangeLog.md +6/−0
• free-foil.cabal +7/−2
• src/Control/Monad/Foil.hs +7/−0
• src/Control/Monad/Foil/Internal.hs +74/−0
• src/Control/Monad/Free/Foil.hs +18/−4
• src/Control/Monad/Free/Foil/Generic.hs +196/−0
• src/Control/Monad/Free/Foil/TH/MkFreeFoil.hs +1310/−0
• src/Control/Monad/Free/Foil/TH/PatternSynonyms.hs +52/−14
• src/Control/Monad/Free/Foil/TH/Signature.hs +35/−4

@@ -1,5 +1,11 @@ # CHANGELOG for `free-foil` +# 0.2.0 — 2024-10-27++- Generate [`COMPLETE` pragma](https://ghc.gitlab.haskell.org/ghc/doc/users_guide/exts/pragmas.html#complete-pragmas) in `mkPatternSynonyms` (see [#26](https://github.com/fizruk/free-foil/pull/26))+- Polykind `ZipMatchK` class with default generic implementation via [`kind-generics`](https://hackage.haskell.org/package/kind-generics) (see [#27](https://github.com/fizruk/free-foil/pull/27))+- New experimental TH generation for Free Foil with support for rich syntax in `Control.Monad.Free.Foil.TH.MkFreeFoil` (see [#28](https://github.com/fizruk/free-foil/pull/28))+ # 0.1.0 — 2024-08-18  - Generalize functions for binders, support general patterns (see [#16](https://github.com/fizruk/free-foil/pull/16))

@@ -1,11 +1,11 @@ cabal-version: 1.12 --- This file has been generated from package.yaml by hpack version 0.36.0.+-- This file has been generated from package.yaml by hpack version 0.37.0. -- -- see: https://github.com/sol/hpack  name:           free-foil-version:        0.1.0+version:        0.2.0 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@@ -40,8 +40,10 @@       Control.Monad.Foil.TH.Util       Control.Monad.Free.Foil       Control.Monad.Free.Foil.Example+      Control.Monad.Free.Foil.Generic       Control.Monad.Free.Foil.TH       Control.Monad.Free.Foil.TH.Convert+      Control.Monad.Free.Foil.TH.MkFreeFoil       Control.Monad.Free.Foil.TH.PatternSynonyms       Control.Monad.Free.Foil.TH.Signature       Control.Monad.Free.Foil.TH.ZipMatch@@ -56,6 +58,7 @@     , bifunctors     , containers     , deepseq+    , kind-generics >=0.5.0     , template-haskell >=2.21.0.0     , text >=1.2.3.1   default-language: Haskell2010@@ -75,6 +78,7 @@     , deepseq     , doctest-parallel     , free-foil+    , kind-generics >=0.5.0     , template-haskell >=2.21.0.0     , text >=1.2.3.1   default-language: Haskell2010@@ -94,6 +98,7 @@     , containers     , deepseq     , free-foil+    , kind-generics >=0.5.0     , template-haskell >=2.21.0.0     , text >=1.2.3.1   default-language: Haskell2010

@@ -47,7 +47,10 @@   Substitution,   lookupSubst,   identitySubst,+  voidSubst,   addSubst,+  addSubstPattern,+  addSubstList,   addRename,   -- * Unification of binders   UnifyNameBinders(..),@@ -66,6 +69,10 @@   emptyNameMap,   lookupName,   addNameBinder,+  nameMapToSubstitution,+  addNameBinders,+  addNameBinderList,+  NameBinderList(..),   -- * Constraints   Ext,   ExtEvidence(..),

@@ -708,6 +708,35 @@     -- ^ 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'+  -> WithNameBinderList r i l o' o''+  -> WithNameBinderList r n l o o''+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 ->+    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)@@ -733,6 +762,10 @@   :: 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@@ -742,6 +775,24 @@ 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@@ -762,6 +813,29 @@ -- | An empty map belongs in the empty scope. 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)++-- | 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 (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. --

@@ -1,5 +1,4 @@ {-# LANGUAGE DataKinds             #-}-{-# LANGUAGE RankNTypes             #-} {-# LANGUAGE DeriveAnyClass        #-} {-# LANGUAGE DeriveGeneric         #-} {-# LANGUAGE FlexibleContexts      #-}@@ -9,6 +8,7 @@ {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE PolyKinds             #-} {-# LANGUAGE QuantifiedConstraints #-}+{-# LANGUAGE RankNTypes            #-} {-# LANGUAGE ScopedTypeVariables   #-} {-# LANGUAGE StandaloneDeriving    #-} {-# LANGUAGE UndecidableInstances  #-}@@ -122,6 +122,20 @@               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                           -- ^ 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 env' body+  where+    env' = Foil.addSubstPattern env binders args+ -- * \(\alpha\)-equivalence  -- | Refresh (force) all binders in a term, minimizing the used indices.@@ -338,7 +352,7 @@   -- ^ Peel back one layer of syntax.   -> (rawIdent -> rawTerm)   -- ^ Convert identifier into a raw variable term.-  -> (forall x y. (Int -> rawIdent) -> binder x y -> rawPattern)+  -> (forall x y. binder x y -> rawPattern)   -- ^ Convert scope-safe pattern into a raw pattern.   -> (rawTerm -> rawScopedTerm)   -- ^ Wrap raw term into a scoped term.@@ -362,7 +376,7 @@   -- ^ Peel back one layer of syntax.   -> (rawIdent -> rawTerm)   -- ^ Convert identifier into a raw variable term.-  -> (forall x y. (Int -> rawIdent) -> binder x y -> rawPattern)+  -> (forall x y. binder x y -> rawPattern)   -- ^ Convert scope-safe pattern into a raw pattern.   -> (rawTerm -> rawScopedTerm)   -- ^ Wrap raw term into a scoped term.@@ -373,5 +387,5 @@   -> (rawPattern, rawScopedTerm) convertFromScopedAST fromSig fromVar makePattern makeScoped f = \case   ScopedAST binder body ->-    ( makePattern f binder+    ( makePattern binder     , makeScoped (convertFromAST fromSig fromVar makePattern makeScoped f body))

@@ -0,0 +1,196 @@+{-# OPTIONS_GHC -Wno-missing-methods #-}+{-# LANGUAGE AllowAmbiguousTypes      #-}+{-# LANGUAGE ConstraintKinds          #-}+{-# LANGUAGE DataKinds                #-}+{-# LANGUAGE DefaultSignatures        #-}+{-# LANGUAGE FlexibleContexts         #-}+{-# LANGUAGE FlexibleInstances        #-}+{-# LANGUAGE GADTs                    #-}+{-# LANGUAGE InstanceSigs             #-}+{-# LANGUAGE MultiParamTypeClasses    #-}+{-# LANGUAGE PolyKinds                #-}+{-# LANGUAGE RankNTypes               #-}+{-# LANGUAGE ScopedTypeVariables      #-}+{-# LANGUAGE StandaloneKindSignatures #-}+{-# LANGUAGE TypeApplications         #-}+{-# LANGUAGE TypeFamilies             #-}+{-# LANGUAGE TypeOperators            #-}+{-# LANGUAGE UndecidableInstances     #-}+module Control.Monad.Free.Foil.Generic where++import           Data.Kind              (Constraint, Type)+import           Generics.Kind+import           Generics.Kind.Examples ()+import           GHC.TypeError++type ZipLoT :: LoT k -> LoT k -> LoT k+type family ZipLoT as bs where+  ZipLoT LoT0 LoT0 = LoT0+  ZipLoT (a :&&: as) (b :&&: bs) = ((a, b) :&&: ZipLoT as bs)++type Mappings :: LoT k -> LoT k -> LoT k -> Type+data Mappings (as :: LoT k) (bs :: LoT k) (cs :: LoT k) where+  M0 :: Mappings LoT0 LoT0 LoT0+  (:^:) :: (a -> b -> Maybe c) -> Mappings as bs cs -> Mappings (a :&&: as) (b :&&: bs) (c :&&: cs)++class PairMappings (as :: LoT k) (bs :: LoT k) where+  pairMappings :: Mappings as bs (ZipLoT as bs)++instance PairMappings LoT0 LoT0 where+  pairMappings = M0++instance PairMappings as bs => PairMappings ((a :: Type) :&&: as) ((b :: Type) :&&: bs) where+  pairMappings = (\x y -> Just (x, y)) :^: pairMappings++class ApplyMappings (v :: TyVar d Type) where+  applyMappings :: forall (as :: LoT d) (bs :: LoT d) (cs :: LoT d).+    Mappings as bs cs -> Interpret (Var v) as -> Interpret (Var v) bs -> Maybe (Interpret (Var v) cs)++instance ApplyMappings (VZ :: TyVar (Type -> tys) Type) where+  applyMappings (f :^: _) x y = f x y++instance ApplyMappings v => ApplyMappings (VS v :: TyVar (ty -> tys) Type) where+  applyMappings (_ :^: fs) x y = applyMappings @_ @v fs x y++genericZipMatchK :: forall f as bs.+    (GenericK f, GZipMatch (RepK f), ReqsZipMatch (RepK f) as bs, PairMappings as bs)+    => f :@@: as -> f :@@: bs -> Maybe (f :@@: (ZipLoT as bs))+genericZipMatchK = genericZipMatchWithK @f @as @bs pairMappings++genericZipMatchWithK :: forall f as bs cs.+    (GenericK f, GZipMatch (RepK f), ReqsZipMatchWith (RepK f) as bs cs)+    => Mappings as bs cs -> f :@@: as -> f :@@: bs -> Maybe (f :@@: cs)+genericZipMatchWithK mappings x y = toK @_ @f @cs <$> gzipMatchWith mappings+  (fromK @_ @f @as x)+  (fromK @_ @f @bs y)++genericZipMatch2+   :: forall sig scope scope' term term'.+   (GenericK sig, GZipMatch (RepK sig), ReqsZipMatch (RepK sig) (scope :&&: term :&&: 'LoT0) (scope' :&&: term' :&&: 'LoT0))+   => sig scope term -> sig scope' term' -> Maybe (sig (scope, scope') (term, term'))+genericZipMatch2 = genericZipMatchK @sig @(scope :&&: term :&&: 'LoT0) @(scope' :&&: term' :&&: 'LoT0)++zipMatchK :: forall f as bs. (ZipMatchK f, PairMappings as bs) => f :@@: as -> f :@@: bs -> Maybe (f :@@: ZipLoT as bs)+zipMatchK = zipMatchWithK @_ @f @as @bs pairMappings++class ZipMatchK (f :: k) where+  zipMatchWithK :: forall as bs cs. Mappings as bs cs -> f :@@: as -> f :@@: bs -> Maybe (f :@@: cs)+  default zipMatchWithK :: forall as bs cs.+    (GenericK f, GZipMatch (RepK f), ReqsZipMatchWith (RepK f) as bs cs)+    => Mappings as bs cs -> f :@@: as -> f :@@: bs -> Maybe (f :@@: cs)+  zipMatchWithK = genericZipMatchWithK @f @as @bs @cs++zipMatchViaEq :: Eq a => Mappings as bs cs -> a -> a -> Maybe a+zipMatchViaEq _ x y+  | x == y = Just x+  | otherwise = Nothing++zipMatchViaChooseLeft :: Mappings as bs cs -> a -> a -> Maybe a+zipMatchViaChooseLeft _ x _ = Just x++-- instance ZipMatchK (,)     -- missing GenericK instance upstream+instance ZipMatchK []+instance ZipMatchK Maybe+instance ZipMatchK Either+instance ZipMatchK a => ZipMatchK (Either a)++type ReqsZipMatch f as bs = ReqsZipMatchWith f as bs (ZipLoT as bs)+class GZipMatch (f :: LoT k -> Type) where+  type ReqsZipMatchWith f (as :: LoT k) (bs :: LoT k) (cs :: LoT k) :: Constraint+  gzipMatchWith :: ReqsZipMatchWith f as bs cs => Mappings as bs cs -> f as -> f bs -> Maybe (f cs)++instance GZipMatch V1 where+  type ReqsZipMatchWith V1 as bs cs = ()+  gzipMatchWith _ _ _ = error "impossible: Generics.Kind.V1 value!" -- FIXME: should be absurd++instance GZipMatch U1 where+  type ReqsZipMatchWith U1 as bs cs = ()+  gzipMatchWith _ U1 U1 = Just U1++instance GZipMatch f => GZipMatch (M1 i c f) where+  type ReqsZipMatchWith (M1 i c f) as bs cs = ReqsZipMatchWith f as bs cs+  gzipMatchWith g (M1 x) (M1 y) = M1 <$> gzipMatchWith g x y++instance (GZipMatch f, GZipMatch g) => GZipMatch (f :+: g) where+  type ReqsZipMatchWith (f :+: g) as bs cs = (ReqsZipMatchWith f as bs cs, ReqsZipMatchWith g as bs cs)+  gzipMatchWith g (L1 x) (L1 y) = L1 <$> gzipMatchWith g x y+  gzipMatchWith g (R1 x) (R1 y) = R1 <$> gzipMatchWith g x y+  gzipMatchWith _ _ _           = Nothing++instance (GZipMatch f, GZipMatch g) => GZipMatch (f :*: g) where+  type ReqsZipMatchWith (f :*: g) as bs cs = (ReqsZipMatchWith f as bs cs, ReqsZipMatchWith g as bs cs)+  gzipMatchWith g (x :*: y) (x' :*: y') =+    liftA2 (:*:) (gzipMatchWith g x x') (gzipMatchWith g y y')++instance ZipMatchFields t => GZipMatch (Field t) where+  type ReqsZipMatchWith (Field t) as bs cs = ReqsZipMatchFieldsWith t as bs cs+  gzipMatchWith f x y = zipMatchFieldsWith f x y++instance GZipMatch f => GZipMatch (c :=>: f) where+  type ReqsZipMatchWith (c :=>: f) as bs cs = (ReqsZipMatchWith f as bs cs, Interpret c cs)+  -- really we want          = (Interpret c as, Interpret c bs) => (ReqsZipMatch f as bs, Interpret c (ZipLoT as bs))+  gzipMatchWith g (SuchThat x) (SuchThat y) = SuchThat <$> gzipMatchWith g x y++instance TypeError ('Text "Existentials are not supported")+         => GZipMatch (Exists k f) where+  type ReqsZipMatchWith (Exists k f) as bs cs = TypeError ('Text "Existentials are not supported")+  gzipMatchWith = undefined++class ZipMatchFields (t :: Atom d Type) where+  type ReqsZipMatchFieldsWith t (as :: LoT d) (bs :: LoT d) (cs :: LoT d) :: Constraint+  zipMatchFieldsWith :: ReqsZipMatchFieldsWith t as bs cs => Mappings as bs cs -> Field t as -> Field t bs -> Maybe (Field t cs)++instance ApplyMappings v => ZipMatchFields (Var v) where+  -- this is always true, but GHC is not smart enough to know that, I think+  type ReqsZipMatchFieldsWith (Var v) as bs cs = () -- InterpretVar v cs ~ (InterpretVar v as, InterpretVar v bs))+  zipMatchFieldsWith g (Field x) (Field y) = Field <$> applyMappings @_ @v g x y++instance ZipMatchK k => ZipMatchFields (Kon k) where+  type ReqsZipMatchFieldsWith (Kon k) as bs cs = ()+  zipMatchFieldsWith _ (Field l) (Field r) = Field <$> zipMatchWithK @_ @k M0 l r++instance (ZipMatchFields t, ZipMatchK k) => ZipMatchFields (Kon k :@: t) where+  type ReqsZipMatchFieldsWith (Kon k :@: t) as bs cs = ReqsZipMatchFieldsWith t as bs cs++  zipMatchFieldsWith :: forall as bs cs. ReqsZipMatchFieldsWith (Kon k :@: t) as bs cs =>+    Mappings as bs cs -> Field (Kon k :@: t) as -> Field (Kon k :@: t) bs -> Maybe (Field (Kon k :@: t) cs)+  zipMatchFieldsWith g (Field l) (Field r) =+    Field <$> zipMatchWithK @_ @k @(Interpret t as :&&: LoT0) @(Interpret t bs :&&: LoT0) @(Interpret t cs :&&: LoT0)+      ((\ll rr -> unField @t <$> zipMatchFieldsWith g (Field ll) (Field rr)) :^: M0) l r++instance (ZipMatchFields t1, ZipMatchFields t2, ZipMatchK k) => ZipMatchFields ((Kon k :@: t1) :@: t2) where+  type ReqsZipMatchFieldsWith ((Kon k :@: t1) :@: t2) as bs cs = (ReqsZipMatchFieldsWith t1 as bs cs, ReqsZipMatchFieldsWith t2 as bs cs)++  zipMatchFieldsWith :: forall as bs cs. ReqsZipMatchFieldsWith ((Kon k :@: t1) :@: t2) as bs cs =>+    Mappings as bs cs -> Field ((Kon k :@: t1) :@: t2) as -> Field ((Kon k :@: t1) :@: t2) bs -> Maybe (Field ((Kon k :@: t1) :@: t2) cs)+  zipMatchFieldsWith g (Field l) (Field r) =+    Field <$> zipMatchWithK @_ @k @(Interpret t1 as :&&: Interpret t2 as :&&: LoT0) @(Interpret t1 bs :&&: Interpret t2 bs :&&: LoT0) @(Interpret t1 cs :&&: Interpret t2 cs :&&: LoT0)+      ((\ll rr -> unField @t1 <$> zipMatchFieldsWith g (Field ll) (Field rr))+        :^: ((\ll rr -> unField @t2 <$> zipMatchFieldsWith g (Field ll) (Field rr))+        :^: M0)) l r++instance {-# OVERLAPPABLE #-} TypeError ('Text "Atom :@: is not supported by ZipMatchFields is a general form") => ZipMatchFields (f :@: t) where+  -- type ReqsZipMatchFieldsWith (f :@: t) as bs cs = TypeError ('Text "Atom :@: is not supported by ZipMatchFields is a general form")+  zipMatchFieldsWith = undefined++instance TypeError ('Text "Atom ForAll is not supported by ZipMatchFields") => ZipMatchFields (ForAll a) where+  type ReqsZipMatchFieldsWith (ForAll a) as bs cs = TypeError ('Text "Atom ForAll is not supported by ZipMatchFields")+  zipMatchFieldsWith = undefined+instance TypeError ('Text "Atom :=>>: is not supported by ZipMatchFields") => ZipMatchFields (c :=>>: a) where+  type ReqsZipMatchFieldsWith (c :=>>: a) as bs cs = TypeError ('Text "Atom :=>>: is not supported by ZipMatchFields")+  zipMatchFieldsWith = undefined+instance TypeError ('Text "Atom Eval is not supported by ZipMatchFields") => ZipMatchFields (Eval a) where+  type ReqsZipMatchFieldsWith (Eval a) as bs cs = TypeError ('Text "Atom Eval is not supported by ZipMatchFields")+  zipMatchFieldsWith = undefined++-- instance ZipMatchFields (ForAll f) where+--   type ReqsZipMatchFields (ForAll f) as bs = ???+--   zipMatchFields = ???++-- instance ZipMatchFields (c :=>>: f) where+--   type ReqsZipMatchFields (c :=>>: f) as bs = ???+--   zipMatchFields = ???++-- instance ZipMatchFields (Eval f) where+--   type ReqsZipMatchFields (Eval f) as bs = ???+--   zipMatchFields = ???

@@ -0,0 +1,1310 @@+{-# LANGUAGE LambdaCase      #-}+{-# LANGUAGE RecordWildCards #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE ViewPatterns    #-}+{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}+{-# HLINT ignore "Use ++" #-}+-- | Template Haskell generation for Free Foil (generic scope-safe representation of syntax).+module Control.Monad.Free.Foil.TH.MkFreeFoil (+  FreeFoilConfig(..),+  FreeFoilTermConfig(..),+  mkFreeFoil,+  mkFreeFoilConversions,+) where++import           Language.Haskell.TH+import           Language.Haskell.TH.Syntax (addModFinalizer)++import           Control.Monad              (forM, forM_, when)+import qualified Control.Monad.Foil         as Foil+import           Control.Monad.Foil.TH.Util+import qualified Control.Monad.Free.Foil    as Foil+import           Data.Bifunctor+import           Data.List                  (find, unzip4, (\\), nub)+import           Data.Maybe                 (catMaybes, mapMaybe)+import Data.Map (Map)+import qualified Data.Map as Map+import qualified GHC.Generics               as GHC++-- | Config for the Template Haskell generation of data types,+-- pattern synonyms, and conversion functions for the Free Foil representation,+-- based on a raw recursive representation.+data FreeFoilConfig = FreeFoilConfig+  { rawQuantifiedNames        :: [Name]+  -- ^ Names of raw types that may include other binders and terms as components.+  -- Some examples of syntax that might be suitable here:+  --+  --  1. a type scheme in HM-style type system (to explicitly disallow nested forall)+  --  2. defining equation of a function (which itself is not a term)+  --  3. data or type synonym declaration (which itself is not a type)+  --  4. unification constraints (quantified or not)+  , freeFoilTermConfigs       :: [FreeFoilTermConfig]+  -- ^ Configurations for each term (e.g. expressions, types) group.+  , freeFoilNameModifier      :: String -> String+  -- ^ Name modifier for the Free Foil conterpart of a raw type name.+  -- Normally, this is just 'id'.+  , freeFoilScopeNameModifier :: String -> String+  -- ^ Name modifier for the scoped Free Foil conterpart of a raw type name.+  -- Normally, this is something like @("Scoped" ++)@.+  , signatureNameModifier     :: String -> String+  -- ^ Name modifier for the signature conterpart of a raw type name or raw constructor name.+  -- Normally, this is something like @(++ "Sig")@.+  , freeFoilConNameModifier   :: String -> String+  -- ^ Name modifier for the Free Foil conterpart (pattern synonym) of a raw constructor name.+  -- Normally, this is just 'id'.+  , freeFoilConvertToName     :: String -> String+  -- ^ Name of a conversion function (from raw to scope-safe) for a raw type name.+  -- Normally, this is something like @("to" ++)@.+  , freeFoilConvertFromName   :: String -> String+  -- ^ Name of a conversion function (from scope-safe to raw) for a raw type name.+  -- Normally, this is something like @("from" ++)@.+  }++-- | Config for a single term group,+-- for the Template Haskell generation of data types,+-- pattern synonyms, and conversion functions for the Free Foil representation,+-- based on a raw recursive representation.+data FreeFoilTermConfig = FreeFoilTermConfig+  { rawIdentName          :: Name+    -- ^ The type name for the identifiers.+    -- When identifiers occur in a term, they are converted to 'Foil.Name' (with an appropriate type-level scope parameter).+    -- When identifiers occur in a pattern, they are converted to 'Foil.NameBinder' (with appropriate type-level scope parameters).+  , rawTermName           :: Name+    -- ^ The type name for the term.+    -- This will be the main recursive type to be converted into an 'Foil.AST'.+  , rawBindingName        :: Name+    -- ^ The type name for the binders (patterns).+    -- This will be the main binder type to used in 'Foil.AST'-representation of the terms.+  , rawScopeName          :: Name+    -- ^ The type name for the scoped term.+    -- This will be replaced with either 'Foil.ScopedAST' (with outer scope) or 'Foil.AST' (with inner scope)+    -- depending on its occurrence in a regular (sub)term or some quantified syntax.+  , rawVarConName         :: Name+    -- ^ The constructor name for the variables in a term.+    -- This constructor will be replaced with the standard 'Foil.Var'.+    -- It is expected to have exactly one field of type 'rawIdentName'.+  , rawSubTermNames       :: [Name]+    -- ^ Type names for subterm syntax.+    -- This will rely on the main term type ('rawTermName') for recursive occurrences.+    -- Template Haskell will also generate signatures for these.+  , rawSubScopeNames      :: [Name]+    -- ^ Type names for scoped subterm syntax.+    -- This will rely on the main term type ('rawTermName') for recursive occurrences.+    -- Template Haskell will also generate signatures for these.+  , intToRawIdentName     :: Name+    -- ^ Name of a function that converts 'Int' to a raw identifier.+    -- Normally, this is something like @(\i -> VarIdent ("x" ++ show i))@.+    -- This is required to generate standard conversions from scope-safe to raw representation.+  , rawVarIdentToTermName :: Name+    -- ^ Name of a function that converts a raw identifier into a raw term.+    -- Normally, this is some kind of @Var@ or @TypeVar@ data constructor.+    -- This is required to generate standard conversions from scope-safe to raw representation.+  , rawTermToScopeName    :: Name+    -- ^ Name of a function that converts a raw term into a raw scoped term.+    -- Normally, this is some kind of @ScopedTerm@ or @ScopedType@ data constructor.+  , rawScopeToTermName    :: Name+    -- ^ Name of a function that extracts a raw term from a raw scoped term.+    -- Normally, this is something like @(\(ScopedTerm term) -> term)@.+  }++toFreeFoilName :: FreeFoilConfig -> Name -> Name+toFreeFoilName FreeFoilConfig{..} name = mkName (freeFoilNameModifier (nameBase name))++toFreeFoilNameFrom :: FreeFoilConfig -> Name -> Name+toFreeFoilNameFrom FreeFoilConfig{..} name = mkName (freeFoilConvertFromName (nameBase name))++toFreeFoilNameTo :: FreeFoilConfig -> Name -> Name+toFreeFoilNameTo FreeFoilConfig{..} name = mkName (freeFoilConvertToName (nameBase name))++toFreeFoilScopedName :: FreeFoilConfig -> Name -> Name+toFreeFoilScopedName FreeFoilConfig{..} name = mkName (freeFoilScopeNameModifier (nameBase name))++toSignatureName :: FreeFoilConfig -> Name -> Name+toSignatureName FreeFoilConfig{..} name = mkName (signatureNameModifier (nameBase name))++toConName :: FreeFoilConfig -> Name -> Name+toConName FreeFoilConfig{..} name = mkName (freeFoilConNameModifier (nameBase name))++lookupIdentName :: Name -> [FreeFoilTermConfig] -> Maybe FreeFoilTermConfig+lookupIdentName name = find (\FreeFoilTermConfig{..} -> rawIdentName == name)++lookupTermName :: Name -> [FreeFoilTermConfig] -> Maybe FreeFoilTermConfig+lookupTermName name = find (\FreeFoilTermConfig{..} -> rawTermName == name)++lookupSubTermName :: Name -> [FreeFoilTermConfig] -> Maybe FreeFoilTermConfig+lookupSubTermName name = find (\FreeFoilTermConfig{..} -> name `elem` rawSubTermNames)++lookupSubScopeName :: Name -> [FreeFoilTermConfig] -> Maybe FreeFoilTermConfig+lookupSubScopeName name = find (\FreeFoilTermConfig{..} -> name `elem` rawSubScopeNames)++lookupBindingName :: Name -> [FreeFoilTermConfig] -> Maybe FreeFoilTermConfig+lookupBindingName name = find (\FreeFoilTermConfig{..} -> rawBindingName == name)++lookupScopeName :: Name -> [FreeFoilTermConfig] -> Maybe FreeFoilTermConfig+lookupScopeName name = find (\FreeFoilTermConfig{..} -> rawScopeName == name)++data Sort+  = SortBinder | SortTerm | SortSubTerm++toFreeFoilType :: Sort -> FreeFoilConfig -> Type -> Type -> Type -> Type+toFreeFoilType isBinder config@FreeFoilConfig{..} outerScope innerScope = go+  where+    go = \case+      PeelConT typeName (map go -> typeParams)+        | typeName `elem` rawQuantifiedNames ->+            PeelConT (toFreeFoilName config typeName) (typeParams ++ [outerScope])+        | typeName `elem` map rawIdentName freeFoilTermConfigs ->+            case isBinder of+              SortBinder -> PeelConT ''Foil.NameBinder [outerScope, innerScope]+              _          -> PeelConT ''Foil.Name [outerScope]+        | Just _ <- lookupTermName typeName freeFoilTermConfigs ->+            PeelConT (toFreeFoilName config typeName) (typeParams ++ [outerScope])+        | Just _ <- lookupBindingName typeName freeFoilTermConfigs ->+            PeelConT (toFreeFoilName config typeName) (typeParams ++ [outerScope, innerScope])+        | Just FreeFoilTermConfig{..} <- lookupScopeName typeName freeFoilTermConfigs ->+            PeelConT (toFreeFoilName config rawTermName) (typeParams ++ [innerScope])+        | Just _ <- lookupSubTermName typeName freeFoilTermConfigs ->+            PeelConT (toFreeFoilName config typeName) (typeParams ++ [outerScope])+        | Just _ <- lookupSubScopeName typeName freeFoilTermConfigs ->+            PeelConT (toFreeFoilName config typeName) (typeParams ++ [innerScope])+      ForallT bndrs ctx type_ -> ForallT bndrs ctx (go type_)+      ForallVisT bndrs type_ -> ForallVisT bndrs (go type_)+      AppT f x -> AppT (go f) (go x)+      AppKindT f k -> AppKindT (go f) k+      SigT t k -> SigT (go t) k+      t@ConT{} -> t+      t@VarT{} -> t+      t@PromotedT{} -> t+      InfixT l op r -> InfixT (go l) op (go r)+      UInfixT l op r -> UInfixT (go l) op (go r)+      PromotedInfixT l op r -> PromotedInfixT (go l) op (go r)+      PromotedUInfixT l op r -> PromotedUInfixT (go l) op (go r)+      ParensT t -> ParensT (go t)+      t@TupleT{} -> t+      t@UnboxedTupleT{} -> t+      t@UnboxedSumT{} -> t+      t@ArrowT{} -> t+      t@MulArrowT{} -> t+      t@EqualityT{} -> t+      t@ListT{} -> t+      t@PromotedTupleT{} -> t+      t@PromotedNilT{} -> t+      t@PromotedConsT{} -> t+      t@StarT{} -> t+      t@ConstraintT{} -> t+      t@LitT{} -> t+      t@WildCardT{} -> t+      ImplicitParamT s t -> ImplicitParamT s (go t)++toFreeFoilSigType :: Sort -> FreeFoilConfig -> Type -> Type -> Type -> Maybe Type+toFreeFoilSigType sort config@FreeFoilConfig{..} scope term = go+  where+    go :: Type -> Maybe Type+    go = \case+      PeelConT _typeName (mapM go -> Nothing) ->+        error "bad type params"+      PeelConT typeName (mapM go -> Just typeParams)+        | Just _ <- lookupTermName typeName freeFoilTermConfigs ->+            case sort of+              SortSubTerm -> Just (PeelConT (toSignatureName config typeName) (typeParams ++ [scope, term]))+              _           -> Just term+        | Just _ <- lookupBindingName typeName freeFoilTermConfigs ->+            Nothing+        | Just _ <- lookupScopeName typeName freeFoilTermConfigs ->+            Just scope+        | Just _ <- lookupSubTermName typeName freeFoilTermConfigs ->+            Just (PeelConT (toSignatureName config typeName) (typeParams ++ [scope, term]))+        | Just _ <- lookupSubScopeName typeName freeFoilTermConfigs ->+            Just (PeelConT (toSignatureName config typeName) (typeParams ++ [scope, term]))+      ForallT bndrs ctx type_ -> ForallT bndrs ctx <$> go type_+      ForallVisT bndrs type_ -> ForallVisT bndrs <$> go type_+      AppT f x -> AppT <$> go f <*> go x+      AppKindT f k -> AppKindT <$> go f <*> pure k+      SigT t k -> SigT <$> go t <*> pure k+      t@ConT{} -> pure t+      t@VarT{} -> pure t+      t@PromotedT{} -> pure t+      InfixT l op r -> InfixT <$> go l <*> pure op <*> go r+      UInfixT l op r -> UInfixT <$> go l <*> pure op <*> go r+      PromotedInfixT l op r -> PromotedInfixT <$> go l <*> pure op <*> go r+      PromotedUInfixT l op r -> PromotedUInfixT <$> go l <*> pure op <*> go r+      ParensT t -> ParensT <$> go t+      t@TupleT{} -> pure t+      t@UnboxedTupleT{} -> pure t+      t@UnboxedSumT{} -> pure t+      t@ArrowT{} -> pure t+      t@MulArrowT{} -> pure t+      t@EqualityT{} -> pure t+      t@ListT{} -> pure t+      t@PromotedTupleT{} -> pure t+      t@PromotedNilT{} -> pure t+      t@PromotedConsT{} -> pure t+      t@StarT{} -> pure t+      t@ConstraintT{} -> pure t+      t@LitT{} -> pure t+      t@WildCardT{} -> pure t+      ImplicitParamT s t -> ImplicitParamT s <$> go t++toFreeFoilCon :: FreeFoilConfig -> Type -> Type -> Type -> Con -> Q Con+toFreeFoilCon config rawRetType outerScope innerScope = go+  where+    goType = toFreeFoilType SortTerm config outerScope innerScope+    go = \case+      GadtC conNames argTypes retType -> do+        let newConNames = map (toConName config) conNames+        forM_ (zip conNames newConNames) $ \(conName, newConName) ->+          addModFinalizer $ putDoc (DeclDoc newConName)+            ("Corresponds to '" ++ show conName ++ "'.")+        return (GadtC newConNames (map (fmap goType) argTypes) (goType retType))+      NormalC conName types -> go (GadtC [conName] types rawRetType)+      RecC conName types -> go (NormalC conName (map removeName types))+      InfixC l conName r -> go (GadtC [conName] [l, r] rawRetType)+      ForallC params ctx con -> ForallC params ctx <$> go con+      RecGadtC conNames argTypes retType -> go (GadtC conNames (map removeName argTypes) retType)++toFreeFoilSigCon :: FreeFoilConfig -> FreeFoilTermConfig -> Name -> Type -> Type -> Type -> Con -> Q (Maybe Con)+toFreeFoilSigCon config FreeFoilTermConfig{..} sigName rawRetType scope term = go+  where+    goType = toFreeFoilSigType SortTerm config scope term+    go = \case+      GadtC conNames argTypes retType+        | null newConNames -> pure Nothing+        | otherwise -> do+            forM_ (zip conNames newConNames) $ \(conName, newConName) ->+              addModFinalizer $ putDoc (DeclDoc newConName)+                ("Corresponds to '" ++ show conName ++ "'.")+            return (Just (GadtC newConNames newArgTypes theRetType))+        where+          newArgTypes = mapMaybe (traverse goType) argTypes+          newConNames =+            [ toSignatureName config rawConName+            | rawConName <- conNames+            , rawConName /= rawVarConName ]+          theRetType =+            case retType of+              PeelConT _rawTypeName (mapM goType -> Just params) ->+                PeelConT sigName (params ++ [scope, term])+              _ -> error "unexpected return type!"+      NormalC conName types -> go (GadtC [conName] types rawRetType)+      RecC conName types -> go (NormalC conName (map removeName types))+      InfixC l conName r -> go (GadtC [conName] [l, r] rawRetType)+      ForallC params ctx con -> fmap (ForallC params ctx) <$> go con+      RecGadtC conNames argTypes retType -> go (GadtC conNames (map removeName argTypes) retType)++toFreeFoilBindingCon :: FreeFoilConfig -> Type -> Type -> Con -> Q Con+toFreeFoilBindingCon config rawRetType theOuterScope = go+  where+    goType = toFreeFoilType SortBinder config theOuterScope++    goTypeArgs :: Int -> Type -> [BangType] -> Q (Type, [BangType])+    goTypeArgs _ outerScope [] = pure (outerScope, [])+    goTypeArgs i outerScope ((bang_, rawArgType) : rawArgs) = do+      case rawArgType of+        PeelConT rawTypeName _rawTypeParams+          | rawTypeName `elem` map rawIdentName (freeFoilTermConfigs config) -> do+            innerScope <- VarT <$> newName ("i" <> show i)+            let argType = toFreeFoilType SortBinder config outerScope innerScope rawArgType+            (theInnerScope, argTypes) <- goTypeArgs (i + 1) innerScope rawArgs+            return (theInnerScope, ((bang_, argType) : argTypes))++          | Just _ <- lookupBindingName rawTypeName (freeFoilTermConfigs config) -> do+            innerScope <- VarT <$> newName ("i" <> show i)+            let argType = toFreeFoilType SortBinder config outerScope innerScope rawArgType+            (theInnerScope, argTypes) <- goTypeArgs (i + 1) innerScope rawArgs+            return (theInnerScope, ((bang_, argType) : argTypes))++        _ -> do+          let argType = toFreeFoilType SortBinder config outerScope outerScope rawArgType+          (theInnerScope, argTypes) <- goTypeArgs (i + 1) outerScope rawArgs+          return (theInnerScope, ((bang_, argType) : argTypes))++    go :: Con -> Q Con+    go = \case+      GadtC conNames argTypes retType -> do+        (theInnerScope, newArgs) <- goTypeArgs 0 theOuterScope argTypes+        let newConNames = map (toConName config) conNames+        forM_ (zip conNames newConNames) $ \(conName, newConName) ->+          addModFinalizer $ putDoc (DeclDoc newConName)+            ("Corresponds to '" ++ show conName ++ "'.")+        return (GadtC newConNames newArgs (goType theInnerScope retType))+      NormalC conName types -> go (GadtC [conName] types rawRetType)+      RecC conName types -> go (NormalC conName (map removeName types))+      InfixC l conName r -> go (GadtC [conName] [l, r] rawRetType)+      ForallC params ctx con -> ForallC params ctx <$> go con+      RecGadtC conNames argTypes retType -> go (GadtC conNames (map removeName argTypes) retType)++termConToPat :: Name -> FreeFoilConfig -> FreeFoilTermConfig -> Con -> Q [([Name], Pat, Pat, [Exp])]+termConToPat rawTypeName config@FreeFoilConfig{..} FreeFoilTermConfig{..} = go+  where+    rawRetType = error "impossible happened!"++    fromArgType :: Type -> Q ([Name], [Pat], [Pat], [Exp])+    fromArgType = \case+      PeelConT typeName _params+        | Just _ <- lookupBindingName typeName freeFoilTermConfigs -> do+            return ([], [], [], [])+        | Just _ <- lookupScopeName typeName freeFoilTermConfigs -> do+            binder <- newName "binder"+            body <- newName "body"+            return ([binder, body], [ConP 'Foil.ScopedAST [] [VarP binder, VarP body]], [TupP [VarP binder, VarP body]], [VarE binder, VarE body])+        | Just _ <- lookupSubTermName typeName freeFoilTermConfigs -> do+            let rawSigName = toSignatureName config typeName+                funName = toFreeFoilNameFrom config rawSigName+            x <- newName "x"+            return ([x], [VarP x], [VarP x], [AppE (VarE funName) (VarE x)])+        | Just _ <- lookupSubScopeName typeName freeFoilTermConfigs -> do+            let rawSigName = toSignatureName config typeName+                funName = toFreeFoilNameFrom config rawSigName+            x <- newName "x"+            return ([x], [VarP x], [VarP x], [AppE (VarE funName) (VarE x)])+        | typeName == '[] -> do+            x <- newName "x"+            return ([x], [VarP x], [VarP x], [ConE 'False])+      AppT _ (PeelConT typeName _params)+        -- | Just _ <- lookupTermName typeName freeFoilTermConfigs -> do+        --     let funName = toFreeFoilNameFrom config typeName+        --     x <- newName "x"+        --     return ([x], [VarP x], [VarP x], [AppE (AppE (VarE 'fmap) (VarE funName)) (VarE x)])+        | Just _ <- lookupSubTermName typeName freeFoilTermConfigs -> do+            let rawSigName = toSignatureName config typeName+                funName = toFreeFoilNameFrom config rawSigName+            x <- newName "x"+            return ([x], [VarP x], [VarP x], [AppE (AppE (VarE 'fmap) (VarE funName)) (VarE x)])+        | Just _ <- lookupSubScopeName typeName freeFoilTermConfigs -> do+            let rawSigName = toSignatureName config typeName+                funName = toFreeFoilNameFrom config rawSigName+            x <- newName "x"+            return ([x], [VarP x], [VarP x], [AppE (AppE (VarE 'fmap) (VarE funName)) (VarE x)])+      _ -> do+        x <- newName "x"+        return ([x], [VarP x], [VarP x], [VarE x])++    go :: Con -> Q [([Name], Pat, Pat, [Exp])]+    go = \case+      GadtC conNames rawArgTypes _rawRetType -> concat <$> do+        forM conNames $ \conName -> do+          let newConName = toSignatureName config conName+          (concat -> vars, concat -> pats, concat -> pats', concat -> exps) <- unzip4 <$>+            mapM (fromArgType . snd) rawArgTypes+          return $+            if rawTypeName == rawTermName+              then [ (vars, ConP 'Foil.Node [] [ConP newConName [] pats], ConP newConName [] pats', exps) ]+              else [ (vars, ConP newConName [] pats, ConP newConName [] pats', exps) ]+      NormalC conName types -> go (GadtC [conName] types rawRetType)+      RecC conName types -> go (NormalC conName (map removeName types))+      InfixC l conName r -> go (GadtC [conName] [l, r] rawRetType)+      ForallC _params _ctx con -> go con+      RecGadtC conNames argTypes retType -> go (GadtC conNames (map removeName argTypes) retType)++termConToPatBinding :: Name -> FreeFoilConfig -> FreeFoilTermConfig -> Con -> Q [([Name], Pat, Pat, [Exp])]+termConToPatBinding rawTypeName config@FreeFoilConfig{..} FreeFoilTermConfig{..} = go+  where+    rawRetType = error "impossible happened!"++    fromArgType :: Type -> Q ([Name], [Pat], [Pat], [Exp])+    fromArgType = \case+      PeelConT typeName _params+        | typeName == rawIdentName -> do+            x <- newName "x"+            return ([x], [VarP x], [VarP x], [VarE intToRawIdentName `AppE` (VarE 'Foil.nameId `AppE` (VarE 'Foil.nameOf `AppE` VarE x))])+        | Just _ <- lookupBindingName typeName freeFoilTermConfigs -> do+            let funName = toFreeFoilNameFrom config typeName+            x <- newName "x"+            return ([x], [VarP x], [VarP x], [VarE funName `AppE` VarE x])+        | Just _ <- lookupScopeName typeName freeFoilTermConfigs -> do+            binder <- newName "binder"+            body <- newName "body"+            return ([binder, body], [ConP 'Foil.ScopedAST [] [VarP binder, VarP body]], [TupP [VarP binder, VarP body]], [VarE binder, VarE body])+        | Just _ <- lookupSubTermName typeName freeFoilTermConfigs -> do+            let rawSigName = toSignatureName config typeName+                funName = toFreeFoilNameFrom config rawSigName+            x <- newName "x"+            return ([x], [VarP x], [VarP x], [AppE (VarE funName) (VarE x)])+        | Just _ <- lookupSubScopeName typeName freeFoilTermConfigs -> do+            let rawSigName = toSignatureName config typeName+                funName = toFreeFoilNameFrom config rawSigName+            x <- newName "x"+            return ([x], [VarP x], [VarP x], [AppE (VarE funName) (VarE x)])+      AppT _ (PeelConT typeName _params)+        | Just _ <- lookupSubTermName typeName freeFoilTermConfigs -> do+            let rawSigName = toSignatureName config typeName+                funName = toFreeFoilNameFrom config rawSigName+            x <- newName "x"+            return ([x], [VarP x], [VarP x], [AppE (AppE (VarE 'fmap) (VarE funName)) (VarE x)])+        | Just _ <- lookupSubScopeName typeName freeFoilTermConfigs -> do+            let rawSigName = toSignatureName config typeName+                funName = toFreeFoilNameFrom config rawSigName+            x <- newName "x"+            return ([x], [VarP x], [VarP x], [AppE (AppE (VarE 'fmap) (VarE funName)) (VarE x)])+      _ -> do+        x <- newName "x"+        return ([x], [VarP x], [VarP x], [VarE x])++    go :: Con -> Q [([Name], Pat, Pat, [Exp])]+    go = \case+      GadtC conNames rawArgTypes _rawRetType -> concat <$> do+        forM conNames $ \conName -> do+          let newConName = toFreeFoilName config conName+          (concat -> vars, concat -> pats, concat -> pats', concat -> exps) <- unzip4 <$>+            mapM (fromArgType . snd) rawArgTypes+          return $+            if rawTypeName == rawTermName+              then [ (vars, ConP 'Foil.Node [] [ConP newConName [] pats], ConP newConName [] pats', exps) ]+              else [ (vars, ConP newConName [] pats, ConP newConName [] pats', exps) ]+      NormalC conName types -> go (GadtC [conName] types rawRetType)+      RecC conName types -> go (NormalC conName (map removeName types))+      InfixC l conName r -> go (GadtC [conName] [l, r] rawRetType)+      ForallC _params _ctx con -> go con+      RecGadtC conNames argTypes retType -> go (GadtC conNames (map removeName argTypes) retType)++termConToPatQuantified :: FreeFoilConfig -> Con -> Q [([Name], Pat, Pat, [Exp])]+termConToPatQuantified config@FreeFoilConfig{..} = go+  where+    rawRetType = error "impossible happened!"++    fromArgType :: Type -> Q ([Name], [Pat], [Pat], [Exp])+    fromArgType = \case+      PeelConT typeName _params+        | Just _ <- lookupTermName typeName freeFoilTermConfigs -> do+            let funName = toFreeFoilNameFrom config typeName+            x <- newName "x"+            return ([x], [VarP x], [VarP x], [VarE funName `AppE` VarE x])+        | Just FreeFoilTermConfig{..} <- lookupScopeName typeName freeFoilTermConfigs -> do+            let funName = toFreeFoilNameFrom config rawTermName+            x <- newName "x"+            return ([x], [VarP x], [VarP x], [VarE rawTermToScopeName `AppE` (VarE funName `AppE` VarE x)])+        | Just FreeFoilTermConfig{..} <- lookupIdentName typeName freeFoilTermConfigs -> do+            x <- newName "x"+            return ([x], [VarP x], [VarP x], [VarE intToRawIdentName `AppE` (VarE 'Foil.nameId `AppE` VarE x)])+        | Just _ <- lookupBindingName typeName freeFoilTermConfigs -> do+            let funName = toFreeFoilNameFrom config typeName+            x <- newName "x"+            return ([x], [VarP x], [VarP x], [VarE funName `AppE` VarE x])+        | Just _ <- lookupSubTermName typeName freeFoilTermConfigs -> do+            let rawSigName = toSignatureName config typeName+                funName = toFreeFoilNameFrom config rawSigName+            x <- newName "x"+            return ([x], [VarP x], [VarP x], [AppE (VarE funName) (VarE x)])+        | Just _ <- lookupSubScopeName typeName freeFoilTermConfigs -> do+            let rawSigName = toSignatureName config typeName+                funName = toFreeFoilNameFrom config rawSigName+            x <- newName "x"+            return ([x], [VarP x], [VarP x], [AppE (VarE funName) (VarE x)])+      AppT _ (PeelConT typeName _params)+        | Just _ <- lookupSubTermName typeName freeFoilTermConfigs -> do+            let funName = toFreeFoilNameFrom config typeName+            x <- newName "x"+            return ([x], [VarP x], [VarP x], [AppE (AppE (VarE 'fmap) (VarE funName)) (VarE x)])+        | Just _ <- lookupSubScopeName typeName freeFoilTermConfigs -> do+            let funName = toFreeFoilNameFrom config typeName+            x <- newName "x"+            return ([x], [VarP x], [VarP x], [AppE (AppE (VarE 'fmap) (VarE funName)) (VarE x)])+        | Just _ <- lookupTermName typeName freeFoilTermConfigs -> do+            let funName = toFreeFoilNameFrom config typeName+            x <- newName "x"+            return ([x], [VarP x], [VarP x], [AppE (AppE (VarE 'fmap) (VarE funName)) (VarE x)])+      _ -> do+        x <- newName "x"+        return ([x], [VarP x], [VarP x], [VarE x])++    go :: Con -> Q [([Name], Pat, Pat, [Exp])]+    go = \case+      GadtC conNames rawArgTypes _rawRetType -> concat <$> do+        forM conNames $ \conName -> do+          let newConName = toFreeFoilName config conName+          (concat -> vars, concat -> pats, concat -> pats', concat -> exps) <- unzip4 <$>+            mapM (fromArgType . snd) rawArgTypes+          return [ (vars, ConP newConName [] pats, ConP newConName [] pats', exps) ]+      NormalC conName types -> go (GadtC [conName] types rawRetType)+      RecC conName types -> go (NormalC conName (map removeName types))+      InfixC l conName r -> go (GadtC [conName] [l, r] rawRetType)+      ForallC _params _ctx con -> go con+      RecGadtC conNames argTypes retType -> go (GadtC conNames (map removeName argTypes) retType)++mkPatternSynonym :: Name -> FreeFoilConfig -> FreeFoilTermConfig -> Type -> Con -> Q [(Name, [Dec])]+mkPatternSynonym rawTypeName config termConfig@FreeFoilTermConfig{..} rawRetType = go+  where+    go :: Con -> Q [(Name, [Dec])]+    go = \case+      GadtC conNames rawArgTypes _rawRetType -> concat <$> do+        forM (conNames \\ [rawVarConName]) $ \conName -> do+          let patName = toConName config conName+              rawConType = foldr (\x y -> AppT (AppT ArrowT x) y) rawRetType (map snd rawArgTypes)+              outerScope = VarT (mkName "o")+              innerScope+                | rawTypeName `elem` rawSubScopeNames = outerScope+                | otherwise = VarT (mkName "i")+          [(vars, pat, _, _)] <- termConToPat rawTypeName config termConfig (GadtC [conName] rawArgTypes rawRetType)    -- FIXME: unsafe matching!+          addModFinalizer $ putDoc (DeclDoc patName)+            ("/Generated/ with '" ++ show 'mkFreeFoil ++ "'. Pattern synonym for an '" ++ show ''Foil.AST ++ "' node of type '" ++ show conName ++ "'.")+          return [(patName,+            [ PatSynSigD patName (toFreeFoilType SortTerm config outerScope innerScope rawConType)+            , PatSynD patName (PrefixPatSyn vars) ImplBidir pat+            ])]++      NormalC conName types -> go (GadtC [conName] types rawRetType)+      RecC conName types -> go (NormalC conName (map removeName types))+      InfixC l conName r -> go (GadtC [conName] [l, r] rawRetType)+      ForallC _params _ctx con -> go con  -- FIXME: params and ctx!+      RecGadtC conNames argTypes retType -> go (GadtC conNames (map removeName argTypes) retType)++toFreeFoilClauseFrom :: Name -> FreeFoilConfig -> FreeFoilTermConfig -> Type -> Con -> Q [Clause]+toFreeFoilClauseFrom rawTypeName config termConfig@FreeFoilTermConfig{..} rawRetType = go+  where+    go = \case+      GadtC conNames rawArgTypes rawRetType' -> concat <$> do+        forM (conNames \\ [rawVarConName]) $ \conName -> do+          [(_vars, _pat, pat, exps)] <- termConToPat rawTypeName config termConfig+            (GadtC [conName] rawArgTypes rawRetType')    -- FIXME: unsafe matching!+          return [ Clause [pat] (NormalB (foldl AppE (ConE conName) exps)) [] ]++      NormalC conName types -> go (GadtC [conName] types rawRetType)+      RecC conName types -> go (NormalC conName (map removeName types))+      InfixC l conName r -> go (GadtC [conName] [l, r] rawRetType)+      ForallC _params _ctx con -> go con+      RecGadtC conNames argTypes retType -> go (GadtC conNames (map removeName argTypes) retType)++toFreeFoilClauseFromBinding :: FreeFoilConfig -> FreeFoilTermConfig -> Type -> Con -> Q [Clause]+toFreeFoilClauseFromBinding config termConfig@FreeFoilTermConfig{..} rawRetType = go+  where+    go = \case+      GadtC conNames rawArgTypes rawRetType' -> concat <$> do+        forM (conNames \\ [rawVarConName]) $ \conName -> do+          [(_vars, _pat, pat, exps)] <- termConToPatBinding rawBindingName config termConfig+            (GadtC [conName] rawArgTypes rawRetType')    -- FIXME: unsafe matching!+          return [ Clause [pat] (NormalB (foldl AppE (ConE conName) exps)) [] ]++      NormalC conName types -> go (GadtC [conName] types rawRetType)+      RecC conName types -> go (NormalC conName (map removeName types))+      InfixC l conName r -> go (GadtC [conName] [l, r] rawRetType)+      ForallC _params _ctx con -> go con+      RecGadtC conNames argTypes retType -> go (GadtC conNames (map removeName argTypes) retType)++toFreeFoilClauseFromQuantified :: FreeFoilConfig -> Type -> Con -> Q [Clause]+toFreeFoilClauseFromQuantified config rawRetType = go+  where+    go = \case+      GadtC conNames rawArgTypes rawRetType' -> concat <$> do+        forM conNames $ \conName -> do+          [(_vars, _pat, pat, exps)] <- termConToPatQuantified config+            (GadtC [conName] rawArgTypes rawRetType')    -- FIXME: unsafe matching!+          return [ Clause [pat] (NormalB (foldl AppE (ConE conName) exps)) [] ]++      NormalC conName types -> go (GadtC [conName] types rawRetType)+      RecC conName types -> go (NormalC conName (map removeName types))+      InfixC l conName r -> go (GadtC [conName] [l, r] rawRetType)+      ForallC _params _ctx con -> go con+      RecGadtC conNames argTypes retType -> go (GadtC conNames (map removeName argTypes) retType)++-- | Generate scope-safe types and pattern synonyms for a given raw set of types:+--+--  1. Scope-safe quantified types (e.g. type schemas, defining equations of functions, unification constraints, data/type declarations)+--  2. Scope-safe terms, scoped terms, subterms, scoped subterms.+--  3. Scope-safe patterns.+--  4. Signatures for terms, subterms, and scoped subterms.+--  5. Pattern synonyms for terms, subterms, and scoped subterms.+mkFreeFoil :: FreeFoilConfig -> Q [Dec]+mkFreeFoil config@FreeFoilConfig{..} = concat <$> sequence+  [ mapM mkQuantifiedType rawQuantifiedNames+  , mapM mkBindingType freeFoilTermConfigs+  , concat <$> mapM mkSignatureTypes freeFoilTermConfigs+  , concat <$> mapM mkPatternSynonyms freeFoilTermConfigs+  ]+  where+    scope = mkName "scope"+    term = mkName "term"+    outerScope = mkName "o"+    innerScope = mkName "i"++    mkPatternSynonyms termConfig@FreeFoilTermConfig{..} = do+      ds <- mkPatternSynonyms' termConfig rawTermName+      ds' <- concat <$> mapM (mkPatternSynonyms' termConfig) (rawSubTermNames <> rawSubScopeNames)+      return (ds <> ds')++    mkPatternSynonyms' FreeFoilTermConfig{..} rawName = do+      (tvars, cons) <- reifyDataOrNewtype rawName+      let rawRetType = PeelConT rawName (map (VarT . tvarName) tvars)+      (unzip -> (patNames, decls)) <- concat <$> mapM (mkPatternSynonym rawName config FreeFoilTermConfig{..} rawRetType) cons+      let completeDecl+            | rawName == rawTermName = PragmaD (CompleteP ('Foil.Var : patNames) Nothing)+            | otherwise = PragmaD (CompleteP patNames Nothing)+      return (concat decls ++ [completeDecl])++    mkQuantifiedType rawName = do+      (tvars, cons) <- reifyDataOrNewtype rawName+      let name = toFreeFoilName config rawName+          rawRetType = PeelConT rawName (map (VarT . tvarName) tvars)+          newParams = tvars ++ [PlainTV outerScope BndrReq]+          toCon = toFreeFoilCon config rawRetType (VarT outerScope) (VarT innerScope)+      newCons <- mapM toCon cons+      addModFinalizer $ putDoc (DeclDoc name)+        ("/Generated/ with '" ++ show 'mkFreeFoil ++ "'. A scope-safe version of '" ++ show rawName ++ "'.")+      return (DataD [] name newParams Nothing newCons [])++    mkBindingType FreeFoilTermConfig{..} = do+      (tvars, cons) <- reifyDataOrNewtype rawBindingName+      let bindingName = toFreeFoilName config rawBindingName+          rawRetType = PeelConT rawBindingName (map (VarT . tvarName) tvars)+          newParams = tvars ++ [PlainTV outerScope BndrReq, PlainTV innerScope BndrReq]+          toCon = toFreeFoilBindingCon config rawRetType (VarT outerScope)+      newCons <- mapM toCon cons+      addModFinalizer $ putDoc (DeclDoc bindingName)+        ("/Generated/ with '" ++ show 'mkFreeFoil ++ "'. A binding type, scope-safe version of '" ++ show rawBindingName ++ "'.")+      return (DataD [] bindingName newParams Nothing newCons [])++    mkSignatureTypes termConfig@FreeFoilTermConfig{..} = do+      sig <- mkSignatureType termConfig rawTermName+      subsigs <- concat <$> mapM (mkSignatureType termConfig) (rawSubTermNames <> rawSubScopeNames)+      return (sig ++ subsigs)++    mkSignatureType termConfig@FreeFoilTermConfig{..} rawName = do+      (tvars, cons) <- reifyDataOrNewtype rawName+      let sigName = toSignatureName config rawName+          tvars' = map (VarT . tvarName) tvars+          rawRetType = PeelConT rawName tvars'+          newParams = tvars ++ [PlainTV scope BndrReq, PlainTV term BndrReq]+          toCon = toFreeFoilSigCon config termConfig sigName rawRetType (VarT scope) (VarT term)+      newCons <- catMaybes <$> mapM toCon cons+      let bindingT = PeelConT (toFreeFoilName config rawBindingName) tvars'+          sigNameT = PeelConT (toSignatureName config rawTermName) tvars'+          astName = toFreeFoilName config rawName+          scopeName = toFreeFoilScopedName config rawName+          termAST = PeelConT ''Foil.AST [bindingT, sigNameT]+          scopedTermAST = PeelConT ''Foil.ScopedAST [bindingT, sigNameT]+          n = mkName "n"+      addModFinalizer $ putDoc (DeclDoc sigName)+        ("/Generated/ with '" ++ show 'mkFreeFoil ++ "'. A signature based on '" ++ show rawName ++ "'.")+      addModFinalizer $ putDoc (DeclDoc astName)+        ("/Generated/ with '" ++ show 'mkFreeFoil ++ "'. A scope-safe version of '" ++ show rawName ++ "'.")+      when (rawTermName == rawName) $ do+        addModFinalizer $ putDoc (DeclDoc scopeName)+          ("/Generated/ with '" ++ show 'mkFreeFoil ++ "'. A scoped (and scope-safe) version of '" ++ show rawName ++ "'.")+      return $ concat+        [ [ DataD [] sigName newParams Nothing newCons [DerivClause Nothing [ConT ''GHC.Generic, ConT ''Functor, ConT ''Foldable, ConT ''Traversable]] ]+        , if rawTermName == rawName+            then [ TySynD astName   tvars termAST+                 , TySynD scopeName tvars scopedTermAST ]+            else [ TySynD astName   (tvars ++ [PlainTV n BndrReq])+                    (PeelConT sigName+                      (tvars' +++                      [ AppT scopedTermAST (VarT n)+                      , AppT termAST (VarT n) ])) ]+        ]++infixr 3 -->+(-->) :: Type -> Type -> Type+a --> b = AppT (AppT ArrowT a) b++reifyDataOrNewtype :: Name -> Q ([TyVarBndr BndrVis], [Con])+reifyDataOrNewtype name = reify name >>= \case+  TyConI (DataD _ctx _name tvars _kind cons _deriv) -> return (tvars, cons)+  TyConI (NewtypeD _ctx _name tvars _kind con _deriv) -> return (tvars, [con])+  _ -> error ("not a data or newtype: " ++ show name)++-- | Generate conversions to and from scope-safe representation:+--+--  1. Conversions for scope-safe quantified types (e.g. type schemas, defining equations of functions, unification constraints, data/type declarations)+--  2. Conversions for scope-safe terms, scoped terms, subterms, scoped subterms.+--  3. CPS-style conversions for scope-safe patterns.+--  4. Helpers for signatures of terms, subterms, and scoped subterms.+mkFreeFoilConversions :: FreeFoilConfig -> Q [Dec]+mkFreeFoilConversions config@FreeFoilConfig{..} = concat <$> sequence+  [ concat <$> mapM mkConvertFrom freeFoilTermConfigs+  , concat <$> mapM mkConvertFromQuantified rawQuantifiedNames+  , concat <$> mapM mkConvertTo freeFoilTermConfigs+  , concat <$> mapM mkConvertToQuantified rawQuantifiedNames+  ]+  where+    outerScope = mkName "o"+    innerScope = mkName "i"++    mkConvertFrom termConfig@FreeFoilTermConfig{..} = concat <$> sequence+      [ concat <$> mapM (mkConvertFromSig termConfig) (rawTermName : (rawSubTermNames <> rawSubScopeNames))+      , mkConvertFromBinding termConfig+      , concat <$> mapM (mkConvertFromSubTerm termConfig) (rawSubTermNames <> rawSubScopeNames)+      , mkConvertFromTerm termConfig+      ]++    mkConvertFromSig termConfig@FreeFoilTermConfig{..} rawName = do+      (tvars, cons) <- reifyDataOrNewtype rawName+      let rawSigName = toSignatureName config rawName+          funName = toFreeFoilNameFrom config rawSigName+          rawRetType = PeelConT rawName (map (VarT . tvarName) tvars)+          rawTermType = PeelConT rawTermName (map (VarT . tvarName) tvars)+          rawScopedTermType = PeelConT rawScopeName (map (VarT . tvarName) tvars)+          rawBindingType = PeelConT rawBindingName (map (VarT . tvarName) tvars)+          rawScopeType = TupleT 2 `AppT` rawBindingType `AppT` rawScopedTermType+      case toFreeFoilSigType SortSubTerm config rawScopeType rawTermType rawRetType of+        Just termType -> do+          clauses <- concat <$> mapM (toFreeFoilClauseFrom rawSigName config termConfig rawRetType) cons+          addModFinalizer $ putDoc (DeclDoc funName)+            ("/Generated/ with '" ++ show 'mkFreeFoil ++ "'. A helper used to convert from scope-safe to raw representation.")+          return+            [ SigD funName (AppT (AppT ArrowT termType) rawRetType)+            , FunD funName clauses ]+        Nothing -> error "impossible happened"++    mkConvertFromTerm FreeFoilTermConfig{..} = do+      (tvars, _cons) <- reifyDataOrNewtype rawTermName+      let funName = toFreeFoilNameFrom config rawTermName+          rawSigName = toSignatureName config rawTermName+          funSigName = toFreeFoilNameFrom config rawSigName+          funBindingName = toFreeFoilNameFrom config rawBindingName+          rawTermType = PeelConT rawTermName (map (VarT . tvarName) tvars)+          termType =  toFreeFoilType SortTerm config (VarT outerScope) (VarT innerScope) rawTermType+      addModFinalizer $ putDoc (DeclDoc funName)+        ("/Generated/ with '" ++ show 'mkFreeFoil ++ "'. Convert from scope-safe to raw representation.")+      return+        [ SigD funName (AppT (AppT ArrowT termType) rawTermType)+        , FunD funName [+            Clause [] (NormalB+              (VarE 'Foil.convertFromAST+                `AppE` VarE funSigName+                `AppE` VarE rawVarIdentToTermName+                `AppE` VarE funBindingName+                `AppE` VarE rawTermToScopeName+                `AppE` VarE intToRawIdentName)) []+          ]+        ]++    mkConvertFromSubTerm FreeFoilTermConfig{..} rawName = do+      (tvars, _cons) <- reifyDataOrNewtype rawName+      let funName = toFreeFoilNameFrom config rawName+          funSigName = toFreeFoilNameFrom config (toSignatureName config rawName)+          funTermName = toFreeFoilNameFrom config rawTermName+          funBindingName = toFreeFoilNameFrom config rawBindingName+          rawType = PeelConT rawName (map (VarT . tvarName) tvars)+          safeType =  toFreeFoilType SortTerm config (VarT outerScope) (VarT innerScope) rawType+      binders <- newName "binders"+      body <- newName "body"+      addModFinalizer $ putDoc (DeclDoc funName)+        ("/Generated/ with '" ++ show 'mkFreeFoil ++ "'. Convert from scope-safe to raw representation.")+      return+        [ SigD funName (AppT (AppT ArrowT safeType) rawType)+        , FunD funName [+            Clause [] (NormalB $+              InfixE+              (Just (VarE funSigName))+              (VarE '(.))+              (Just (VarE 'bimap+                `AppE` LamE [ConP 'Foil.ScopedAST [] [VarP binders, VarP body]]+                  (TupE [ Just (VarE funBindingName `AppE` VarE binders)+                        , Just (VarE rawTermToScopeName `AppE` (VarE funTermName `AppE` VarE body))])+                `AppE` VarE funTermName))) []+          ]+        ]++    mkConvertFromQuantified rawName = do+      (tvars, cons) <- reifyDataOrNewtype rawName+      let funName = toFreeFoilNameFrom config rawName+          rawType = PeelConT rawName (map (VarT . tvarName) tvars)+          safeType = toFreeFoilType SortTerm config (VarT outerScope) (VarT innerScope) rawType+      addModFinalizer $ putDoc (DeclDoc funName)+        ("/Generated/ with '" ++ show 'mkFreeFoil ++ "'. Convert from scope-safe to raw representation.")+      clauses <- concat <$> mapM (toFreeFoilClauseFromQuantified config rawType) cons+      return+        [ SigD funName (AppT (AppT ArrowT safeType) rawType)+        , FunD funName clauses+        ]++    mkConvertFromBinding termConfig@FreeFoilTermConfig{..} = do+      (tvars, cons) <- reifyDataOrNewtype rawBindingName+      let funName = toFreeFoilNameFrom config rawBindingName+          rawRetType = PeelConT rawBindingName (map (VarT . tvarName) tvars)+          bindingType = toFreeFoilType SortBinder config (VarT outerScope) (VarT innerScope) rawRetType+      clauses <- concat <$> mapM (toFreeFoilClauseFromBinding config termConfig rawRetType) cons+      addModFinalizer $ putDoc (DeclDoc funName)+        ("/Generated/ with '" ++ show 'mkFreeFoil ++ "'. Convert a scope-safe to a raw binding.")+      return+        [ SigD funName (bindingType --> rawRetType)+        , FunD funName clauses ]++    mkConvertTo termConfig@FreeFoilTermConfig{..} = concat <$> sequence+      [ mkConvertToSig SortTerm termConfig rawTermName+      , concat <$> mapM (mkConvertToSig SortSubTerm termConfig) (rawSubTermNames <> rawSubScopeNames)+      , mkConvertToBinding termConfig+      , concat <$> mapM (mkConvertToSubTerm termConfig) (rawSubTermNames <> rawSubScopeNames)+      , mkConvertToTerm termConfig+      ]++    mkConvertToSubTerm termConfig@FreeFoilTermConfig{..} rawName = do+      (tvars, cons) <- reifyDataOrNewtype rawName+      (itvars, _cons) <- reifyDataOrNewtype rawIdentName+      let funName = toFreeFoilNameTo config rawName+          rawIdentType = PeelConT rawIdentName (map (VarT . tvarName) (take (length itvars) tvars)) -- FIXME: undocumented hack :(+          rawType = PeelConT rawName (map (VarT . tvarName) tvars)+          safeType =  toFreeFoilType SortTerm config (VarT outerScope) (VarT innerScope) rawType+      clauses <- concat <$> mapM (subTermConToClause rawType config termConfig) cons+      addModFinalizer $ putDoc (DeclDoc funName)+        ("/Generated/ with '" ++ show 'mkFreeFoil ++ "'. Convert from scope-safe to raw representation.")+      let scope+            | rawName `elem` rawSubTermNames = outerScope+            | otherwise = innerScope+      return+        [ SigD funName $+            ForallT+              (PlainTV scope SpecifiedSpec : map (SpecifiedSpec <$) tvars)+              [ ConT ''Foil.Distinct `AppT` VarT scope+              , ConT ''Ord `AppT` rawIdentType ] $+                (ConT ''Foil.Scope `AppT` VarT scope)+                --> (ConT ''Map `AppT` rawIdentType `AppT` (ConT ''Foil.Name `AppT` VarT scope))+                --> rawType+                --> safeType+        , FunD funName clauses+        ]++    mkConvertToTerm FreeFoilTermConfig{..} = do+      (tvars, _cons) <- reifyDataOrNewtype rawTermName+      (itvars, _cons) <- reifyDataOrNewtype rawIdentName+      let funName = toFreeFoilNameTo config rawTermName+          rawSigName = toSignatureName config rawTermName+          rawIdentType = PeelConT rawIdentName (map (VarT . tvarName) (take (length itvars) tvars)) -- FIXME: undocumented hack :(+          funSigName = toFreeFoilNameTo config rawSigName+          funBindingName = toFreeFoilNameTo config rawBindingName+          rawTermType = PeelConT rawTermName (map (VarT . tvarName) tvars)+          termType =  toFreeFoilType SortTerm config (VarT outerScope) (VarT innerScope) rawTermType+      addModFinalizer $ putDoc (DeclDoc funName)+        ("/Generated/ with '" ++ show 'mkFreeFoil ++ "'. Convert from scope-safe to raw representation.")+      return+        [ SigD funName $+            ForallT+              (PlainTV outerScope SpecifiedSpec : map (SpecifiedSpec <$) tvars)+              [ ConT ''Foil.Distinct `AppT` VarT outerScope+              , ConT ''Ord `AppT` rawIdentType ] $+                (ConT ''Foil.Scope `AppT` VarT outerScope)+                --> (ConT ''Map `AppT` rawIdentType `AppT` (ConT ''Foil.Name `AppT` VarT outerScope))+                --> rawTermType+                --> termType+        , FunD funName [+            Clause [] (NormalB+              (VarE 'Foil.convertToAST+                `AppE` VarE funSigName+                `AppE` VarE funBindingName+                `AppE` VarE rawScopeToTermName)) []+          ]+        ]++    mkConvertToSig sort termConfig@FreeFoilTermConfig{..} rawName = do+      (tvars, cons) <- reifyDataOrNewtype rawName+      (itvars, _cons) <- reifyDataOrNewtype rawIdentName+      let rawSigName = toSignatureName config rawName+          funName = toFreeFoilNameTo config rawSigName+          rawType = PeelConT rawName (map (VarT . tvarName) tvars)+          rawIdentType = PeelConT rawIdentName (map (VarT . tvarName) (take (length itvars) tvars)) -- FIXME: undocumented hack :(+          rawTermType = PeelConT rawTermName (map (VarT . tvarName) tvars)+          rawScopedTermType = PeelConT rawScopeName (map (VarT . tvarName) tvars)+          rawBindingType = PeelConT rawBindingName (map (VarT . tvarName) tvars)+          rawScopeType = TupleT 2 `AppT` rawBindingType `AppT` rawScopedTermType+      case toFreeFoilSigType SortSubTerm config rawScopeType rawTermType rawType of+        Just safeType -> do+          let retType = case sort of+                SortTerm -> ConT ''Either `AppT` rawIdentType `AppT` safeType+                _        -> safeType+          clauses <- concat <$> mapM (sigConToClause sort rawType config termConfig) cons+          addModFinalizer $ putDoc (DeclDoc funName)+            ("/Generated/ with '" ++ show 'mkFreeFoil ++ "'. A helper used to convert from raw to scope-safe representation.")+          return+            [ SigD funName (AppT (AppT ArrowT rawType) retType)+            , FunD funName clauses ]+        Nothing -> error "impossible happened"++    mkConvertToBinding termConfig@FreeFoilTermConfig{..} = do+      (tvars, cons) <- reifyDataOrNewtype rawBindingName+      (itvars, _cons) <- reifyDataOrNewtype rawIdentName+      let funName = toFreeFoilNameTo config rawBindingName+          rawBindingType = PeelConT rawBindingName (map (VarT . tvarName) tvars)+          rawIdentType = PeelConT rawIdentName (map (VarT . tvarName) (take (length itvars) tvars)) -- FIXME: undocumented hack :(+          safeType = toFreeFoilType SortBinder config (VarT outerScope) (VarT innerScope) rawBindingType+      clauses <- concat <$> mapM (bindingConToClause rawBindingType config termConfig) cons+      r <- newName "r"+      addModFinalizer $ putDoc (DeclDoc funName)+        ("/Generated/ with '" ++ show 'mkFreeFoil ++ "'. Convert from raw to scope-safe binding (CPS-style).")+      return+        [ SigD funName $+            ForallT+              (PlainTV outerScope SpecifiedSpec : map (SpecifiedSpec <$) tvars ++ [PlainTV r SpecifiedSpec])+              [ ConT ''Foil.Distinct `AppT` VarT outerScope+              , ConT ''Ord `AppT` rawIdentType ] $+                (ConT ''Foil.Scope `AppT` VarT outerScope)+                --> (ConT ''Map `AppT` rawIdentType `AppT` (ConT ''Foil.Name `AppT` VarT outerScope))+                --> rawBindingType+                --> ForallT [PlainTV innerScope SpecifiedSpec]+                      [ConT ''Foil.DExt `AppT` VarT outerScope `AppT` VarT innerScope]+                      (safeType+                        --> (ConT ''Map `AppT` rawIdentType `AppT` (ConT ''Foil.Name `AppT` VarT innerScope))+                        --> VarT r)+                --> VarT r+        , FunD funName clauses ]++    mkConvertToQuantified rawName = do+      (tvars, cons) <- reifyDataOrNewtype rawName+      rawIdentNamesOfQuantifiedName rawName config >>= \case+        [] -> error "unexpected: quantified type not connected to any known terms"+        [rawIdentName'] -> do+          (itvars, _cons) <- reifyDataOrNewtype rawIdentName'+          let funName = toFreeFoilNameTo config rawName+              rawIdentType = PeelConT rawIdentName' (map (VarT . tvarName) (take (length itvars) tvars)) -- FIXME: undocumented hack :(+              rawType = PeelConT rawName (map (VarT . tvarName) tvars)+              safeType = toFreeFoilType SortTerm config (VarT outerScope) (VarT innerScope) rawType+          addModFinalizer $ putDoc (DeclDoc funName)+            ("/Generated/ with '" ++ show 'mkFreeFoil ++ "'. Convert from scope-safe to raw representation.")+          clauses <- concat <$> mapM (quantifiedConToClause rawType config) cons+          return+            [ SigD funName $+                ForallT+                  (PlainTV outerScope SpecifiedSpec : map (SpecifiedSpec <$) tvars)+                  [ ConT ''Foil.Distinct `AppT` VarT outerScope+                  , ConT ''Ord `AppT` rawIdentType ] $+                    (ConT ''Foil.Scope `AppT` VarT outerScope)+                    --> (ConT ''Map `AppT` rawIdentType `AppT` (ConT ''Foil.Name `AppT` VarT outerScope))+                    --> rawType+                    --> safeType+            , FunD funName clauses+            ]+        _ -> do+          -- error ("unsupported: more than one known term connected to the quantified type: " <> show rawName)+          return []++quantifiedConToClause :: Type -> FreeFoilConfig -> Con -> Q [Clause]+quantifiedConToClause rawType config@FreeFoilConfig{..} = go+  where+    goArgTypes :: Name -> Name -> Name -> Name -> [Type] -> Q ([Pat], [Exp], Exp -> Exp, Name, Name)+    goArgTypes _theScope _theEnv scope env [] = return ([], [], id, scope, env)+    goArgTypes theScope theEnv scope env (t:ts) = case t of+      PeelConT typeName _params+        | typeName `elem` map rawIdentName freeFoilTermConfigs -> do+            x <- newName "_x"+            (pats, exps, wrap, scope', env') <- goArgTypes theScope theEnv scope env ts+            return (VarP x : pats, (InfixE (Just (VarE env)) (VarE '(Map.!)) (Just (VarE x))) : exps, wrap, scope', env')+        | Just _ <- lookupBindingName typeName freeFoilTermConfigs -> do+            x <- newName "_x"+            x' <- newName "_x'"+            scope' <- newName "_scope"+            env' <- newName "_env"+            let funName = toFreeFoilNameTo config typeName+            (pats, exps, wrap, scope'', env'') <- goArgTypes theScope theEnv scope' env' ts+            return (VarP x : pats, VarE x' : exps, \e ->+              VarE funName `AppE` VarE scope `AppE` VarE env `AppE` VarE x `AppE`+                LamE [VarP x', VarP env']+                  (LetE [ ValD (VarP scope') (NormalB (VarE 'Foil.extendScopePattern `AppE` VarE x' `AppE` VarE scope)) []]+                    (wrap e)), scope'', env'')+        | Just FreeFoilTermConfig{..} <- lookupScopeName typeName freeFoilTermConfigs -> do+            x <- newName "_x"+            let funName = toFreeFoilNameTo config rawTermName+            (pats, exps, wrap, scope', env') <- goArgTypes theScope theEnv scope env ts+            return (VarP x : pats,+              (VarE funName `AppE` VarE scope' `AppE` VarE env' `AppE` (VarE rawScopeToTermName `AppE` VarE x)) : exps,+              wrap, scope', env')+        | Just _ <- lookupTermName typeName freeFoilTermConfigs -> do+            let funName = toFreeFoilNameTo config typeName+            x <- newName "x"+            (pats, exps, wrap, scope', env') <- goArgTypes theScope theEnv scope env ts+            return (VarP x : pats, (VarE funName `AppE` VarE scope' `AppE` VarE env' `AppE` VarE x) : exps, wrap, scope', env')+      AppT _ (PeelConT typeName _params)+        | Just _ <- lookupTermName typeName freeFoilTermConfigs -> do+            let funName = toFreeFoilNameTo config typeName+            x <- newName "x"+            (pats, exps, wrap, scope', env') <- goArgTypes theScope theEnv scope env ts+            return (VarP x : pats, AppE (AppE (VarE 'fmap) (VarE funName `AppE` VarE theScope `AppE` VarE theEnv)) (VarE x) : exps, wrap, scope', env')+        | Just _ <- lookupSubTermName typeName freeFoilTermConfigs -> do+            let funName = toFreeFoilNameTo config typeName+            x <- newName "x"+            (pats, exps, wrap, scope', env') <- goArgTypes theScope theEnv scope env ts+            return (VarP x : pats, AppE (AppE (VarE 'fmap) (VarE funName `AppE` VarE theScope `AppE` VarE theEnv)) (VarE x) : exps, wrap, scope', env')+        | Just _ <- lookupSubScopeName typeName freeFoilTermConfigs -> do+            let funName = toFreeFoilNameTo config typeName+            x <- newName "x"+            (pats, exps, wrap, scope', env') <- goArgTypes theScope theEnv scope env ts+            return (VarP x : pats, AppE (AppE (VarE 'fmap) (VarE funName `AppE` VarE scope' `AppE` VarE env')) (VarE x) : exps, wrap, scope', env')+        | Just FreeFoilTermConfig{..} <- lookupScopeName typeName freeFoilTermConfigs -> do+            let funName = toFreeFoilNameTo config rawTermName+            x <- newName "x"+            (pats, exps, wrap, scope', env') <- goArgTypes theScope theEnv scope env ts+            return (VarP x : pats, AppE (AppE (VarE 'fmap) (VarE funName `AppE` VarE scope' `AppE` VarE env')) (VarE x) : exps, wrap, scope', env')+      _ -> do+        x <- newName "_x"+        (pats, exps, wrap, scope', env') <- goArgTypes theScope theEnv scope env ts+        return (VarP x : pats, VarE x : exps, wrap, scope', env')++    go :: Con -> Q [Clause]+    go = \case+      GadtC conNames rawArgTypes _rawRetType -> concat <$> do+        scope <- newName "_scope"+        env <- newName "_env"+        forM conNames $ \conName -> do+          let newConName = toConName config conName+          (pats, exps, wrap, _scope', _env') <- goArgTypes scope env scope env (map snd rawArgTypes)+          return+            [ Clause [VarP scope, VarP env, ConP conName [] pats]+                (NormalB (wrap (foldl AppE (ConE newConName) exps))) [] ]+      NormalC conName types -> go (GadtC [conName] types rawType)+      RecC conName types -> go (NormalC conName (map removeName types))+      InfixC l conName r -> go (GadtC [conName] [l, r] rawType)+      ForallC _params _ctx con -> go con+      RecGadtC conNames argTypes retType -> go (GadtC conNames (map removeName argTypes) retType)++subTermConToClause :: Type -> FreeFoilConfig -> FreeFoilTermConfig -> Con -> Q [Clause]+subTermConToClause rawType config FreeFoilTermConfig{..} = go+  where+    goArgTypes :: Name -> Name -> [Type] -> Q ([Pat], [Exp], Exp -> Exp, Name, Name)+    goArgTypes scope env [] = return ([], [], id, scope, env)+    goArgTypes scope env (t:ts) = case t of+      PeelConT typeName _params+        | typeName == rawBindingName -> do+            x <- newName "_x"+            x' <- newName "_x'"+            scope' <- newName "_scope"+            env' <- newName "_env"+            let funName = toFreeFoilNameTo config typeName+            (pats, exps, wrap, scope'', env'') <- goArgTypes scope' env' ts+            return (VarP x : pats, VarE x' : exps, \e ->+              VarE funName `AppE` VarE scope `AppE` VarE env `AppE` VarE x `AppE`+                LamE [VarP x', VarP env']+                  (LetE [ ValD (VarP scope') (NormalB (VarE 'Foil.extendScopePattern `AppE` VarE x' `AppE` VarE scope)) []]+                    (wrap e)), scope'', env'')+        | typeName == rawScopeName -> do+            x <- newName "_x"+            let funName = toFreeFoilNameTo config rawTermName+            (pats, exps, wrap, scope', env') <- goArgTypes scope env ts+            return (VarP x : pats,+              (VarE funName `AppE` VarE scope' `AppE` VarE env' `AppE` (VarE rawScopeToTermName `AppE` VarE x)) : exps,+              wrap, scope', env')+        | typeName == rawTermName -> do+            x <- newName "_x"+            let funName = toFreeFoilNameTo config rawTermName+            (pats, exps, wrap, scope', env') <- goArgTypes scope env ts+            return (VarP x : pats,+              (VarE funName `AppE` VarE scope `AppE` VarE env `AppE` VarE x) : exps,+              wrap, scope', env')+        | typeName `elem` rawSubTermNames -> do+            x <- newName "_x"+            let funName = toFreeFoilNameTo config typeName+            (pats, exps, wrap, scope', env') <- goArgTypes scope env ts+            return (VarP x : pats,+              (VarE funName `AppE` VarE scope `AppE` VarE env `AppE` VarE x) : exps,+              wrap, scope', env')+      AppT _ (PeelConT typeName _params)+        | typeName == rawTermName -> do+            let funName = toFreeFoilNameTo config typeName+            x <- newName "_x"+            (pats, exps, wrap, scope', env') <- goArgTypes scope env ts+            return (VarP x : pats,+              (VarE 'fmap `AppE` (VarE funName `AppE` VarE scope `AppE` VarE env) `AppE` VarE x) : exps,+              wrap, scope', env')+        | typeName `elem` rawSubTermNames -> do+            let rawSigName = toSignatureName config typeName+                funName = toFreeFoilNameTo config rawSigName+            x <- newName "_x"+            (pats, exps, wrap, scope', env') <- goArgTypes scope env ts+            return (VarP x : pats,+              (VarE 'fmap `AppE` (VarE funName `AppE` VarE scope `AppE` VarE env) `AppE` VarE x) : exps,+              wrap, scope', env')+        | typeName `elem` rawSubScopeNames -> do+            let rawSigName = toSignatureName config typeName+                funName = toFreeFoilNameTo config rawSigName+            x <- newName "_x"+            (pats, exps, wrap, scope', env') <- goArgTypes scope env ts+            return (VarP x : pats,+              (VarE 'fmap `AppE` (VarE funName `AppE` VarE scope' `AppE` VarE env') `AppE` VarE x) : exps,+              wrap, scope', env')+      _ -> do+        x <- newName "_x"+        (pats, exps, wrap, scope', env') <- goArgTypes scope env ts+        return (VarP x : pats, VarE x : exps, wrap, scope', env')++    go :: Con -> Q [Clause]+    go = \case+      GadtC conNames rawArgTypes _rawRetType -> concat <$> do+        scope <- newName "_scope"+        env <- newName "_env"+        forM conNames $ \conName -> do+          let newConName = toConName config conName+          (pats, exps, wrap, _scope', _env') <- goArgTypes scope env (map snd rawArgTypes)+          return+            [ Clause [VarP scope, VarP env, ConP conName [] pats]+                (NormalB (wrap (foldl AppE (ConE newConName) exps))) [] ]+      NormalC conName types -> go (GadtC [conName] types rawType)+      RecC conName types -> go (NormalC conName (map removeName types))+      InfixC l conName r -> go (GadtC [conName] [l, r] rawType)+      ForallC _params _ctx con -> go con+      RecGadtC conNames argTypes retType -> go (GadtC conNames (map removeName argTypes) retType)++bindingConToClause :: Type -> FreeFoilConfig -> FreeFoilTermConfig -> Con -> Q [Clause]+bindingConToClause rawType config FreeFoilTermConfig{..} = go+  where+    goArgTypes :: Name -> Name -> [Type] -> Q ([Pat], [Exp], Exp -> Exp, Name)+    goArgTypes _scope env [] = return ([], [], id, env)+    goArgTypes scope env (t:ts) = case t of+      PeelConT typeName _params+        | typeName == rawIdentName -> do+            x <- newName "_x"+            x' <- newName "_x'"+            scope' <- newName "_scope"+            env' <- newName "_env"+            (pats, exps, wrap, env'') <- goArgTypes scope' env' ts+            return (VarP x : pats, VarE x' : exps, \e ->+              VarE 'Foil.withFresh `AppE` VarE scope `AppE`+                LamE [VarP x']+                  (LetE [ ValD (VarP scope') (NormalB (VarE 'Foil.extendScope `AppE` VarE x' `AppE` VarE scope)) []+                        , ValD (VarP env') (NormalB (VarE 'Map.insert `AppE` VarE x `AppE` (VarE 'Foil.nameOf `AppE` VarE x') `AppE` (VarE 'fmap `AppE` VarE 'Foil.sink `AppE` VarE env))) []]+                    (wrap e)), env'')+        | typeName == rawBindingName -> do+            x <- newName "_x"+            x' <- newName "_x'"+            scope' <- newName "_scope"+            env' <- newName "_env"+            let funName = toFreeFoilNameTo config typeName+            (pats, exps, wrap, env'') <- goArgTypes scope' env' ts+            return (VarP x : pats, VarE x' : exps, \e ->+              VarE funName `AppE` VarE scope `AppE` VarE env `AppE` VarE x `AppE`+                LamE [VarP x', VarP env']+                  (LetE [ ValD (VarP scope') (NormalB (VarE 'Foil.extendScopePattern `AppE` VarE x' `AppE` VarE scope)) []]+                    (wrap e)), env'')+      _ -> do+        x <- newName "_x"+        (pats, exps, wrap, env') <- goArgTypes scope env ts+        return (VarP x : pats, VarE x : exps, wrap, env')++    go :: Con -> Q [Clause]+    go = \case+      GadtC conNames rawArgTypes _rawRetType -> concat <$> do+        scope <- newName "_scope"+        env <- newName "_env"+        cont <- newName "_cont"+        forM conNames $ \conName -> do+          let newConName = toConName config conName+          (pats, exps, wrap, env') <- goArgTypes scope env (map snd rawArgTypes)+          return+            [ Clause [VarP scope, VarP env, ConP conName [] pats, VarP cont]+                (NormalB (wrap (VarE cont `AppE` foldl AppE (ConE newConName) exps `AppE` VarE env'))) [] ]+      NormalC conName types -> go (GadtC [conName] types rawType)+      RecC conName types -> go (NormalC conName (map removeName types))+      InfixC l conName r -> go (GadtC [conName] [l, r] rawType)+      ForallC _params _ctx con -> go con+      RecGadtC conNames argTypes retType -> go (GadtC conNames (map removeName argTypes) retType)+++sigConToClause :: Sort -> Type -> FreeFoilConfig -> FreeFoilTermConfig -> Con -> Q [Clause]+sigConToClause sort rawRetType config@FreeFoilConfig{..} FreeFoilTermConfig{..} = go+  where+    fromArgType :: Bool -> Name -> Type -> Q ([Pat], [Exp])+    fromArgType isVarCon theIdent = \case+      PeelConT typeName _params+        | typeName == rawIdentName, SortTerm <- sort, isVarCon -> do+            return ([VarP theIdent], [VarE theIdent])+        | Just _ <- lookupBindingName typeName freeFoilTermConfigs -> do+            return ([], [])+        | Just _ <- lookupScopeName typeName freeFoilTermConfigs -> do+            binder <- newName "binder"+            body <- newName "body"+            return ([VarP binder, VarP body], [TupE [Just (VarE binder), Just (VarE body)]])+        | Just _ <- lookupSubTermName typeName freeFoilTermConfigs -> do+            let rawSigName = toSignatureName config typeName+                funName = toFreeFoilNameTo config rawSigName+            x <- newName "_x"+            return ([VarP x], [AppE (VarE funName) (VarE x)])+        | Just _ <- lookupSubScopeName typeName freeFoilTermConfigs -> do+            let rawSigName = toSignatureName config typeName+                funName = toFreeFoilNameTo config rawSigName+            x <- newName "_x"+            return ([VarP x], [AppE (VarE funName) (VarE x)])+      AppT _ (PeelConT typeName _params)+        | Just _ <- lookupSubTermName typeName freeFoilTermConfigs -> do+            let rawSigName = toSignatureName config typeName+                funName = toFreeFoilNameTo config rawSigName+            x <- newName "_x"+            return ([VarP x], [AppE (AppE (VarE 'fmap) (VarE funName)) (VarE x)])+        | Just _ <- lookupSubScopeName typeName freeFoilTermConfigs -> do+            let rawSigName = toSignatureName config typeName+                funName = toFreeFoilNameTo config rawSigName+            x <- newName "_x"+            return ([VarP x], [AppE (AppE (VarE 'fmap) (VarE funName)) (VarE x)])+      _ -> do+        x <- newName "_x"+        return ([VarP x], [VarE x])++    go :: Con -> Q [Clause]+    go = \case+      GadtC conNames rawArgTypes _rawRetType -> concat <$> do+        theIdent <- newName "_theRawIdent"+        forM conNames $ \conName -> do+          let newConName = toSignatureName config conName+              isVarCon = conName == rawVarConName+          (concat -> pats, concat -> exps) <- unzip <$>+            mapM (fromArgType isVarCon theIdent . snd) rawArgTypes+          case sort of+            SortTerm+              | isVarCon -> return+                  [ Clause [ConP conName [] pats] (NormalB (ConE 'Left `AppE` VarE theIdent)) [] ]  -- FIXME!+              | otherwise -> return+                  [ Clause [ConP conName [] pats] (NormalB (ConE 'Right `AppE` (foldl AppE (ConE newConName) exps))) [] ]+            _ -> return+              [ Clause [ConP conName [] pats] (NormalB (foldl AppE (ConE newConName) exps)) [] ]+      NormalC conName types -> go (GadtC [conName] types rawRetType)+      RecC conName types -> go (NormalC conName (map removeName types))+      InfixC l conName r -> go (GadtC [conName] [l, r] rawRetType)+      ForallC _params _ctx con -> go con+      RecGadtC conNames argTypes retType -> go (GadtC conNames (map removeName argTypes) retType)++rawIdentNamesOfQuantifiedName :: Name -> FreeFoilConfig -> Q [Name]+rawIdentNamesOfQuantifiedName rawName config = do+  (_tvars, cons) <- reifyDataOrNewtype rawName+  return (nub (concatMap go cons))+  where+    rawRetType = error "impossible happened!"++    go :: Con -> [Name]+    go = \case+      GadtC _conNames rawArgTypes _rawRetType ->+        concatMap (rawIdentNamesOfType config . snd) rawArgTypes+      NormalC conName types -> go (GadtC [conName] types rawRetType)+      RecC conName types -> go (NormalC conName (map removeName types))+      InfixC l conName r -> go (GadtC [conName] [l, r] rawRetType)+      ForallC _params _ctx con -> go con+      RecGadtC conNames argTypes retType -> go (GadtC conNames (map removeName argTypes) retType)++rawIdentNamesOfType :: FreeFoilConfig -> Type -> [Name]+rawIdentNamesOfType FreeFoilConfig{..} = go+  where+    go = \case+      PeelConT typeName _params+        | typeName `elem` rawQuantifiedNames -> []+        | typeName `elem` map rawIdentName freeFoilTermConfigs -> [typeName]+        | Just FreeFoilTermConfig{..} <- lookupTermName typeName freeFoilTermConfigs ->+            [rawIdentName]+        | Just FreeFoilTermConfig{..} <- lookupBindingName typeName freeFoilTermConfigs ->+            [rawIdentName]+        | Just FreeFoilTermConfig{..} <- lookupScopeName typeName freeFoilTermConfigs ->+            [rawIdentName]+        | Just FreeFoilTermConfig{..} <- lookupSubTermName typeName freeFoilTermConfigs ->+            [rawIdentName]+        | Just FreeFoilTermConfig{..} <- lookupSubScopeName typeName freeFoilTermConfigs ->+            [rawIdentName]+      ForallT _bndrs _ctx type_ -> go type_+      ForallVisT _bndrs type_ -> go type_+      AppT f x -> go f <> go x+      AppKindT f _k -> go f+      SigT t _k -> go t+      ConT{} -> []+      VarT{} -> []+      PromotedT{} -> []+      InfixT l _op r -> go l <> go r+      UInfixT l _op r -> go l <> go r+      PromotedInfixT l _op r -> go l <> go r+      PromotedUInfixT l _op r -> go l <> go r+      ParensT t -> go t+      TupleT{} -> []+      UnboxedTupleT{} -> []+      UnboxedSumT{} -> []+      ArrowT{} -> []+      MulArrowT{} -> []+      EqualityT{} -> []+      ListT{} -> []+      PromotedTupleT{} -> []+      PromotedNilT{} -> []+      PromotedConsT{} -> []+      StarT{} -> []+      ConstraintT{} -> []+      LitT{} -> []+      WildCardT{} -> []+      ImplicitParamT _s t -> go t

@@ -1,13 +1,14 @@-{-# LANGUAGE LambdaCase      #-}+{-# LANGUAGE LambdaCase            #-} {-# OPTIONS_GHC -fno-warn-type-defaults      #-}-{-# LANGUAGE PatternSynonyms #-}-{-# LANGUAGE TemplateHaskell #-}-{-# LANGUAGE ViewPatterns    #-}+{-# LANGUAGE PatternSynonyms       #-}+{-# LANGUAGE TemplateHaskellQuotes #-}+{-# LANGUAGE ViewPatterns          #-} module Control.Monad.Free.Foil.TH.PatternSynonyms where  import           Control.Monad              (forM_) import           Control.Monad.Foil.TH.Util import           Control.Monad.Free.Foil+import           Data.List                  (nub) import           Language.Haskell.TH import           Language.Haskell.TH.Syntax @@ -20,10 +21,12 @@    case reverse signatureTVars of     (tvarName -> term) : (tvarName -> scope) : (reverse -> params) -> do-      concat <$> mapM (mkPatternSynonym (PeelConT signatureT (map (VarT . tvarName) params)) scope term) signatureCons+      (names, decs) <- unzip . concat <$> mapM (mkPatternSynonym (PeelConT signatureT (map (VarT . tvarName) params)) scope term) signatureCons+      return $ decs +++        [ PragmaD (CompleteP ('Var : nub names) Nothing)]     _ -> fail "cannot generate pattern synonyms" -mkPatternSynonym :: Type -> Name -> Name -> Con -> Q [Dec]+mkPatternSynonym :: Type -> Name -> Name -> Con -> Q [(Name, Dec)] mkPatternSynonym signatureType scope term = \case   NormalC conName types -> mkPatternSynonym signatureType scope term     (GadtC [conName] types (AppT (AppT signatureType (VarT scope)) (VarT term)))@@ -33,9 +36,9 @@   InfixC l conName r -> mkPatternSynonym signatureType scope term (NormalC conName [l, r])    ForallC params ctx con -> do-    [ PatSynSigD patName patType, patD ] <- mkPatternSynonym signatureType scope term con+    [ (name, PatSynSigD patName patType), patD ] <- mkPatternSynonym signatureType scope term con     return-      [ PatSynSigD patName (ForallT params ctx patType)+      [ (name, PatSynSigD patName (ForallT params ctx patType))       , patD       ] @@ -49,8 +52,8 @@       addModFinalizer $ putDoc (DeclDoc (mkPatternName conName))         ("/Generated/ with '" ++ show 'mkPatternSynonyms ++ "'. Pattern synonym for an '" ++ show ''AST ++ "' node of type '" ++ show conName ++ "'.")     return $ concat-      [ [ PatSynSigD patternName (foldr (AppT . AppT ArrowT) termType types')-        , PatSynD  patternName (PrefixPatSyn args) ImplBidir (ConP 'Node [] [ConP conName [] pats])+      [ [ (patternName, PatSynSigD patternName (foldr (AppT . AppT ArrowT) termType types'))+        , (patternName, PatSynD  patternName (PrefixPatSyn args) ImplBidir (ConP 'Node [] [ConP conName [] pats]))         ]       | conName <- conNames       , let patternName = mkPatternName conName@@ -66,17 +69,19 @@       Left ((b, _), (x, _)) -> ConP 'ScopedAST [] [VarP b, VarP x]       Right (x, _) -> VarP x -    toPatternArgType i (_bang, VarT typeName)+    toPatternArgType i (_bang, type_@(VarT typeName))       | typeName == scope =           Left             ( (mkName ("b" ++ show i), foldl AppT binderT [VarT n, VarT l])-            , (mkName ("x" ++ show i), PeelConT ''AST [binderT, signatureType, VarT l]))+            , (mkName ("x" ++ show i), replaceScopeTermInType l type_))       | typeName == term =-          Right (mkName ("x" ++ show i), PeelConT ''AST [binderT, signatureType, VarT n])+          Right (mkName ("x" ++ show i), replaceScopeTermInType l type_)       where         l = mkName ("l" ++ show i)     toPatternArgType i (_bang, type_)-      = Right (mkName ("z" ++ show i), type_)+      = Right (mkName ("z" ++ show i), replaceScopeTermInType l type_)+      where+        l = mkName ("l" ++ show i)      mkPatternName conName = mkName (dropEnd (length "Sig") (nameBase conName))     dropEnd k = reverse . drop k . reverse@@ -84,3 +89,36 @@     collapse = \case       Left (x, y) -> [x, y]       Right x -> [x]++    replaceScopeTermInType lscope = \case+      VarT typeName+        | typeName == scope -> PeelConT ''AST [binderT, signatureType, VarT lscope]+        | typeName == term  -> PeelConT ''AST [binderT, signatureType, VarT n]+      ForallT bndrs ctx type_ -> ForallT bndrs ctx (replaceScopeTermInType lscope type_)+      ForallVisT bndrs type_ -> ForallVisT bndrs (replaceScopeTermInType lscope type_)+      AppT f x -> AppT (replaceScopeTermInType lscope f) (replaceScopeTermInType lscope x)+      AppKindT f k -> AppKindT (replaceScopeTermInType lscope f) k+      SigT t k -> SigT (replaceScopeTermInType lscope t) k+      t@ConT{} -> t+      t@VarT{} -> t+      t@PromotedT{} -> t+      InfixT l op r -> InfixT (replaceScopeTermInType lscope l) op (replaceScopeTermInType lscope r)+      UInfixT l op r -> UInfixT (replaceScopeTermInType lscope l) op (replaceScopeTermInType lscope r)+      PromotedInfixT l op r -> PromotedInfixT (replaceScopeTermInType lscope l) op (replaceScopeTermInType lscope r)+      PromotedUInfixT l op r -> PromotedUInfixT (replaceScopeTermInType lscope l) op (replaceScopeTermInType lscope r)+      ParensT t -> ParensT (replaceScopeTermInType lscope t)+      t@TupleT{} -> t+      t@UnboxedTupleT{} -> t+      t@UnboxedSumT{} -> t+      t@ArrowT{} -> t+      t@MulArrowT{} -> t+      t@EqualityT{} -> t+      t@ListT{} -> t+      t@PromotedTupleT{} -> t+      t@PromotedNilT{} -> t+      t@PromotedConsT{} -> t+      t@StarT{} -> t+      t@ConstraintT{} -> t+      t@LitT{} -> t+      t@WildCardT{} -> t+      ImplicitParamT s t -> ImplicitParamT s (replaceScopeTermInType lscope t)

@@ -89,9 +89,40 @@           where             k (x, y) = (name, x, y) -        toSignatureParam (bang_, PeelConT typeName _typeParams)+        toSignatureParam (_bang, PeelConT typeName _typeParams)           | typeName == nameT = fail ("variable with other stuff in constructor: " ++ show con')           | typeName == patternT = pure Nothing -- skip binders, they will be inserted automatically with each scoped term-          | typeName == scopeT = pure (Just (bang_, VarT scope))-          | typeName == termT = pure (Just (bang_, VarT term))-        toSignatureParam bt = pure (Just bt)  -- everything else remains as is+        toSignatureParam (bang_, type_) = pure (Just (bang_, replaceScopeTermInType type_))++        replaceScopeTermInType = \case+          PeelConT typeName _typeParams+            | typeName == scopeT -> VarT scope+            | typeName == termT -> VarT term+          ForallT bndrs ctx type_ -> ForallT bndrs ctx (replaceScopeTermInType type_)+          ForallVisT bndrs type_ -> ForallVisT bndrs (replaceScopeTermInType type_)+          AppT f x -> AppT (replaceScopeTermInType f) (replaceScopeTermInType x)+          AppKindT f k -> AppKindT (replaceScopeTermInType f) k+          SigT t k -> SigT (replaceScopeTermInType t) k+          t@ConT{} -> t+          t@VarT{} -> t+          t@PromotedT{} -> t+          InfixT l op r -> InfixT (replaceScopeTermInType l) op (replaceScopeTermInType r)+          UInfixT l op r -> UInfixT (replaceScopeTermInType l) op (replaceScopeTermInType r)+          PromotedInfixT l op r -> PromotedInfixT (replaceScopeTermInType l) op (replaceScopeTermInType r)+          PromotedUInfixT l op r -> PromotedUInfixT (replaceScopeTermInType l) op (replaceScopeTermInType r)+          ParensT t -> ParensT (replaceScopeTermInType t)+          t@TupleT{} -> t+          t@UnboxedTupleT{} -> t+          t@UnboxedSumT{} -> t+          t@ArrowT{} -> t+          t@MulArrowT{} -> t+          t@EqualityT{} -> t+          t@ListT{} -> t+          t@PromotedTupleT{} -> t+          t@PromotedNilT{} -> t+          t@PromotedConsT{} -> t+          t@StarT{} -> t+          t@ConstraintT{} -> t+          t@LitT{} -> t+          t@WildCardT{} -> t+          ImplicitParamT s t -> ImplicitParamT s (replaceScopeTermInType t)