diff --git a/ChangeLog.md b/ChangeLog.md --- a/ChangeLog.md +++ b/ChangeLog.md @@ -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)) diff --git a/free-foil.cabal b/free-foil.cabal --- a/free-foil.cabal +++ b/free-foil.cabal @@ -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 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 diff --git a/src/Control/Monad/Foil.hs b/src/Control/Monad/Foil.hs --- a/src/Control/Monad/Foil.hs +++ b/src/Control/Monad/Foil.hs @@ -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(..), diff --git a/src/Control/Monad/Foil/Internal.hs b/src/Control/Monad/Foil/Internal.hs --- a/src/Control/Monad/Foil/Internal.hs +++ b/src/Control/Monad/Foil/Internal.hs @@ -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. -- diff --git a/src/Control/Monad/Free/Foil.hs b/src/Control/Monad/Free/Foil.hs --- a/src/Control/Monad/Free/Foil.hs +++ b/src/Control/Monad/Free/Foil.hs @@ -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)) diff --git a/src/Control/Monad/Free/Foil/Generic.hs b/src/Control/Monad/Free/Foil/Generic.hs new file mode 100644 --- /dev/null +++ b/src/Control/Monad/Free/Foil/Generic.hs @@ -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 = ??? diff --git a/src/Control/Monad/Free/Foil/TH/MkFreeFoil.hs b/src/Control/Monad/Free/Foil/TH/MkFreeFoil.hs new file mode 100644 --- /dev/null +++ b/src/Control/Monad/Free/Foil/TH/MkFreeFoil.hs @@ -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 diff --git a/src/Control/Monad/Free/Foil/TH/PatternSynonyms.hs b/src/Control/Monad/Free/Foil/TH/PatternSynonyms.hs --- a/src/Control/Monad/Free/Foil/TH/PatternSynonyms.hs +++ b/src/Control/Monad/Free/Foil/TH/PatternSynonyms.hs @@ -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) diff --git a/src/Control/Monad/Free/Foil/TH/Signature.hs b/src/Control/Monad/Free/Foil/TH/Signature.hs --- a/src/Control/Monad/Free/Foil/TH/Signature.hs +++ b/src/Control/Monad/Free/Foil/TH/Signature.hs @@ -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)