free-foil-0.4.0: src/Control/Monad/Free/Foil/TH/MkFreeFoil.hs
{-# 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.Char (toUpper)
import Data.List (find, unzip4, (\\), nub)
import Data.Maybe (fromMaybe, isJust, catMaybes, listToMaybe, mapMaybe,
maybeToList)
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.
--
-- @since 0.2.0
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.
--
-- @since 0.2.0
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)@.
}
-- | Capitalize the first letter, so that @toTerm'@ gives @tryToTerm'@.
capitalizeFirst :: String -> String
capitalizeFirst [] = []
capitalizeFirst (c : cs) = toUpper c : cs
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))
-- | The name of the range-parametric sibling of a generated definition
-- (see 'Foil.withFreshIn'): @toPatternIn@ beside @toPattern@.
toNameIn :: Name -> Name
toNameIn name = mkName (nameBase name ++ "In")
-- | The name of the naming-parametric sibling of a generated definition:
-- @fromPatternWith@ beside @fromPattern@.
toNameWith :: Name -> Name
toNameWith name = mkName (nameBase name ++ "With")
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)
-- | Is this raw field a binding (pattern) field?
--
-- Such a field has no counterpart in the free foil node: the binder it stands for
-- lives inside the 'Foil.ScopedAST' of each scoped child.
isBindingField :: FreeFoilConfig -> Type -> Bool
isBindingField FreeFoilConfig{..} = \case
PeelConT typeName _ | Just _ <- lookupBindingName typeName freeFoilTermConfigs -> True
_ -> False
-- | Is this raw field a scoped-term field?
--
-- Such a field becomes a 'Foil.ScopedAST', which carries a binder of its own.
isScopeField :: FreeFoilConfig -> Type -> Bool
isScopeField FreeFoilConfig{..} = \case
PeelConT typeName _ | Just _ <- lookupScopeName typeName freeFoilTermConfigs -> True
_ -> False
-- | What a raw binding constructor's field becomes in the scope-safe binding
-- type. Mirrors the classification in 'toFreeFoilBindingCon': an identifier
-- becomes a 'Foil.NameBinder' and threads the scope; a binding type becomes a
-- nested binding type and threads the scope; anything else is a payload that
-- binds nothing.
data BindingFieldSort = FieldBinder | FieldPattern | FieldPayload
deriving (Eq)
bindingFieldSortOf :: FreeFoilConfig -> Type -> BindingFieldSort
bindingFieldSortOf FreeFoilConfig{..} = \case
PeelConT typeName _typeParams
| typeName `elem` map rawIdentName freeFoilTermConfigs -> FieldBinder
| Just _ <- lookupBindingName typeName freeFoilTermConfigs -> FieldPattern
_ -> FieldPayload
-- | Does this field introduce binders (and so thread the scope)?
isBindingFieldSort :: BindingFieldSort -> Bool
isBindingFieldSort = \case
FieldPayload -> False
_ -> True
-- | Does this raw payload type mention anything that converts to a
-- scope-indexed type in the binding type (a term, a scoped term, an
-- identifier, or a nested binding under a type constructor)? Such a payload
-- cannot be rebuilt by the generated 'Foil.CoSinkable' instance, rebuilding it
-- at another scope being what 'Foil.transportPayload' exists for. Generation
-- refuses such a payload, matching the GenericK-side refusal for derived
-- patterns.
mentionsScopeIndexed :: FreeFoilConfig -> Type -> Bool
mentionsScopeIndexed FreeFoilConfig{..} = go
where
isIndexedName typeName = or
[ typeName `elem` rawQuantifiedNames
, typeName `elem` map rawIdentName freeFoilTermConfigs
, isJust (lookupTermName typeName freeFoilTermConfigs)
, isJust (lookupSubTermName typeName freeFoilTermConfigs)
, isJust (lookupScopeName typeName freeFoilTermConfigs)
, isJust (lookupSubScopeName typeName freeFoilTermConfigs)
, isJust (lookupBindingName typeName freeFoilTermConfigs)
]
go = \case
PeelConT typeName typeParams -> isIndexedName typeName || any go typeParams
AppT f x -> go f || go x
SigT t _ -> go t
ParensT t -> go t
_ -> False
-- | The constructors of a raw type as (name, field types), with every
-- constructor syntax flattened to the same shape.
flattenCons :: [Con] -> [(Name, [Type])]
flattenCons = concatMap go
where
go = \case
NormalC name types -> [(name, map snd types)]
RecC name types -> [(name, map (\(_, _, t) -> t) types)]
InfixC l name r -> [(name, [snd l, snd r])]
GadtC names types _retType -> [ (name, map snd types) | name <- names ]
RecGadtC names types _retType -> [ (name, map (\(_, _, t) -> t) types) | name <- names ]
ForallC _ _ con -> go con
-- | One 'Foil.coSinkabilityProof' clause for a generated binding constructor:
--
-- > coSinkabilityProof rename (Con x1 x2 x3) cont =
-- > coSinkabilityProof rename x1 $ \rename' x1' ->
-- > coSinkabilityProof rename' x2 $ \rename'' x2' ->
-- > cont rename'' (Con x1' x2' x3)
--
-- Binder and nested-pattern fields thread the renaming left to right (each via
-- its own 'Foil.CoSinkable' instance); payload fields pass through untouched.
mkCoSinkabilityProofClause :: FreeFoilConfig -> (Name, [Type]) -> Q Clause
mkCoSinkabilityProofClause config (rawConName, rawFieldTypes) = do
let conName = toConName config rawConName
sorts = map (bindingFieldSortOf config) rawFieldTypes
-- Underscore-prefix the binders the clause will not use, so that the
-- generated code triggers no -Wunused-matches in the client module.
hasBinding = any isBindingFieldSort sorts
rename <- newName (if hasBinding then "rename" else "_rename")
cont <- newName "cont"
xs <- mapM (\i -> newName ("x" <> show i)) [1 .. length sorts]
-- fields collects the rebuilt constructor arguments in order (as a
-- difference list, since each step appends on the right).
let go renameCur [] fields =
return (VarE cont `AppE` VarE renameCur
`AppE` foldl AppE (ConE conName) (fields []))
go renameCur ((FieldPayload, x) : rest) fields =
go renameCur rest (fields . (VarE x :))
go renameCur ((_, x) : rest) fields = do
x' <- newName (nameBase x <> "'")
renameNext <- newName "rename'"
body <- go renameNext rest (fields . (VarE x' :))
return (VarE 'Foil.coSinkabilityProof `AppE` VarE renameCur `AppE` VarE x
`AppE` LamE [VarP renameNext, VarP x'] body)
body <- go rename (zip sorts xs) id
return (Clause [VarP rename, ConP conName [] (map VarP xs), VarP cont] (NormalB body) [])
-- | One 'Foil.withPattern' clause for a generated binding constructor:
--
-- > withPattern withBinder unit_ comp_ scope (Con x1 x2 x3) cont =
-- > withBinder scope x1 $ \f1 x1' ->
-- > let scope' = extendScope x1' scope
-- > in withPattern withBinder unit_ comp_ scope' x2 $ \f2 x2' scope'' ->
-- > cont (comp_ f1 f2) (Con x1' x2' x3) scope''
--
-- A 'Foil.NameBinder' field is processed with @withBinder@ directly and
-- extends the ambient scope for the fields to its right; a nested binding
-- field recurses through its own 'Foil.withPattern', which hands the extended
-- scope to its continuation. Results compose left to right with @comp_@; the
-- final continuation receives the scope after the whole constructor, and a
-- constructor that binds nothing hands @unit_@ and the ambient scope over.
mkWithPatternClause :: FreeFoilConfig -> (Name, [Type]) -> Q Clause
mkWithPatternClause config (rawConName, rawFieldTypes) = do
let conName = toConName config rawConName
sorts = map (bindingFieldSortOf config) rawFieldTypes
-- Underscore-prefix the binders the clause will not use, so that the
-- generated code triggers no -Wunused-matches in the client module: a
-- nested binding field keeps everything alive (its recursive call takes
-- unit_ and comp_ along), otherwise usage depends on how many fields
-- bind at all.
nBinding = length (filter isBindingFieldSort sorts)
hasNested = FieldPattern `elem` sorts
usedIf b n = if b then n else '_' : n
withBinder <- newName (usedIf (nBinding > 0) "withBinder")
unit_ <- newName (usedIf (nBinding == 0 || hasNested) "unit_")
comp_ <- newName (usedIf (nBinding >= 2 || hasNested) "comp_")
scope <- newName "scope"
cont <- newName "cont"
xs <- mapM (\i -> newName ("x" <> show i)) [1 .. length sorts]
-- acc is the composition of the binder results so far (Nothing before the
-- first one), composed left to right as each field is passed; fields
-- collects the rebuilt constructor arguments in order (as a difference
-- list, since each step appends on the right).
let go scopeCur acc [] fields =
return (VarE cont `AppE` fromMaybe (VarE unit_) acc
`AppE` foldl AppE (ConE conName) (fields [])
`AppE` VarE scopeCur)
go scopeCur acc ((FieldPayload, x) : rest) fields =
go scopeCur acc rest (fields . (VarE x :))
go scopeCur acc ((sort, x) : rest) fields = do
x' <- newName (nameBase x <> "'")
f <- newName "f"
scopeNext <- newName "scope'"
let acc' = case acc of
Nothing -> VarE f
Just a -> VarE comp_ `AppE` a `AppE` VarE f
body <- go scopeNext (Just acc') rest (fields . (VarE x' :))
return $ case sort of
FieldBinder ->
VarE withBinder `AppE` VarE scopeCur `AppE` VarE x
`AppE` LamE [VarP f, VarP x']
(LetE [ValD (VarP scopeNext)
(NormalB (VarE 'Foil.extendScope `AppE` VarE x' `AppE` VarE scopeCur)) []]
body)
_ ->
VarE 'Foil.withPattern `AppE` VarE withBinder `AppE` VarE unit_
`AppE` VarE comp_ `AppE` VarE scopeCur `AppE` VarE x
`AppE` LamE [VarP f, VarP x', VarP scopeNext] body
body <- go scope Nothing (zip sorts xs) id
return (Clause
[VarP withBinder, VarP unit_, VarP comp_, VarP scope, ConP conName [] (map VarP xs), VarP cont]
(NormalB body) [])
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
perField <- mapM (fromArgType . snd) rawArgTypes
let (concat -> vars, concat -> pats, _, _) = unzip4 perField
-- These expressions rebuild the /raw/ constructor, whose fields are
-- shaped differently from the free foil node's: the raw constructor
-- has a single binding (pattern) field and its scoped fields carry
-- no binder of their own, whereas in the free foil every scoped
-- child carries its own binder. So a scoped child contributes only
-- its body here, and the binding field is filled from the first
-- scoped child's binder -- the raw syntax can name only one binder,
-- and a constructor that binds several scopes binds the same name
-- in each of them.
firstScopeBinder = listToMaybe
[ binder
| (rawArgType, (binder : _, _, _, _)) <- zip (map snd rawArgTypes) perField
, isScopeField config rawArgType ]
rawFieldExp rawArgType (_, _, _, fieldExps)
| isBindingField config rawArgType = map VarE (maybeToList firstScopeBinder)
| isScopeField config rawArgType = drop 1 fieldExps -- the body; the binder is not a raw field
| otherwise = fieldExps
exps = concat (zipWith rawFieldExp (map snd rawArgTypes) perField)
-- Only the first scoped child's binder makes it back into the raw
-- syntax (see above), so matching the others' binders would bind a
-- variable we never use.
sigPats = goSigPats True (zip (map snd rawArgTypes) perField)
goSigPats _ [] = []
goSigPats isFirstScope ((rawArgType, (_, _, fieldPats, _)) : rest)
| isScopeField config rawArgType =
(if isFirstScope then fieldPats else map ignoreBinder fieldPats)
++ goSigPats False rest
| otherwise = fieldPats ++ goSigPats isFirstScope rest
ignoreBinder = \case
TupP [_binder, body] -> TupP [WildP, body]
p -> p
pats' = sigPats
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 -> Name -> FreeFoilConfig -> FreeFoilTermConfig -> Con -> Q [([Name], Pat, Pat, [Exp])]
termConToPatBinding named 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 named `AppE` (VarE 'Foil.nameId `AppE` (VarE 'Foil.nameOf `AppE` VarE x))])
| Just _ <- lookupBindingName typeName freeFoilTermConfigs -> do
let funName = toNameWith (toFreeFoilNameFrom config typeName)
x <- newName "x"
return ([x], [VarP x], [VarP x], [VarE funName `AppE` VarE named `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)
-- | Argument types of a pattern synonym for a single raw constructor.
--
-- This has to agree with 'termConToPat', which decides what the synonym's
-- /arguments/ are, and the two used to disagree:
--
-- * a raw binding (pattern) field contributes __no__ argument, since a binder
-- in the free foil lives inside the 'Foil.ScopedAST' it binds, not beside it;
-- * a raw scoped-term field contributes __two__ arguments, a binder and a body;
-- * every other field contributes one argument, as before.
--
-- Crucially, each scoped-term field gets a __fresh__ inner scope: a constructor
-- with several scoped children (a recursive @let@, say) binds a separate name in
-- each of them, so sharing one scope variable between them is wrong. A
-- constructor with at most one scoped child keeps the inner scope named @i@,
-- so the generated code for such constructors is unchanged.
patternSynonymArgTypes :: FreeFoilConfig -> Type -> Type -> [Type] -> [Type]
patternSynonymArgTypes config@FreeFoilConfig{..} outerScope innerScope rawArgTypes =
go (1 :: Int) rawArgTypes
where
-- Only when there are several scoped children do we need to number the
-- scopes; with one child, @i@ keeps the generated code as it was.
scopeCount = length (filter (isScopeField config) rawArgTypes)
innerScopeFor k
| scopeCount <= 1 = innerScope
| otherwise = VarT (mkName ("i" ++ show k))
go _ [] = []
go k (rawArgType : rest) = case rawArgType of
PeelConT typeName _params
-- The binder is an argument of the ScopedAST, not of the node.
| Just _ <- lookupBindingName typeName freeFoilTermConfigs -> go k rest
-- A scoped child: its own binder, then its body, in its own scope.
| Just FreeFoilTermConfig{..} <- lookupScopeName typeName freeFoilTermConfigs ->
let inner = innerScopeFor k
rawBindingType = PeelConT rawBindingName (typeParamsOf rawArgType)
in toFreeFoilType SortTerm config outerScope inner rawBindingType
: toFreeFoilType SortTerm config outerScope inner rawArgType
: go (k + 1) rest
_ -> toFreeFoilType SortTerm config outerScope innerScope rawArgType : go k rest
-- A scoped type and its binding type are parametrised alike (both carry the
-- annotation type, if any), so the binder type reuses the scope's parameters.
typeParamsOf = \case
PeelConT _ params -> params
_ -> []
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
outerScope = VarT (mkName "o")
innerScope
| rawTypeName `elem` rawSubScopeNames = outerScope
| otherwise = VarT (mkName "i")
synType = foldr (\x y -> AppT (AppT ArrowT x) y)
(toFreeFoilType SortTerm config outerScope innerScope rawRetType)
(patternSynonymArgTypes config outerScope innerScope (map snd rawArgTypes))
[(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 synType
, 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 :: Name -> FreeFoilConfig -> FreeFoilTermConfig -> Type -> Con -> Q [Clause]
toFreeFoilClauseFromBinding named config termConfig@FreeFoilTermConfig{..} rawRetType = go
where
go = \case
GadtC conNames rawArgTypes rawRetType' -> concat <$> do
forM (conNames \\ [rawVarConName]) $ \conName -> do
[(_vars, _pat, pat, exps)] <- termConToPatBinding named rawBindingName config termConfig
(GadtC [conName] rawArgTypes rawRetType') -- FIXME: unsafe matching!
return [ Clause [VarP named, 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.
--
-- @since 0.2.0
mkFreeFoil :: FreeFoilConfig -> Q [Dec]
mkFreeFoil config@FreeFoilConfig{..} = concat <$> sequence
[ mapM mkQuantifiedType rawQuantifiedNames
, mapM mkBindingType freeFoilTermConfigs
, concat <$> mapM mkPatternCoSinkable 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 [])
-- A concrete 'Foil.CoSinkable' instance for the generated binding type,
-- one clause per constructor, delegating to the fields' instances. The
-- GenericK default routes every binder operation through a generic
-- representation traversal, which costs a measurable constant per binder
-- at runtime (see issue #82); the concrete instance removes it, and a
-- client no longer declares (or hand-writes) the instance itself.
mkPatternCoSinkable FreeFoilTermConfig{..} = do
(tvars, cons) <- reifyDataOrNewtype rawBindingName
let bindingName = toFreeFoilName config rawBindingName
bindingT = PeelConT bindingName (map (VarT . tvarName) tvars)
flatCons = flattenCons cons
forM_ flatCons $ \(conName, fieldTypes) ->
forM_ fieldTypes $ \fieldType ->
case bindingFieldSortOf config fieldType of
FieldPayload | mentionsScopeIndexed config fieldType -> fail $ unlines
[ "mkFreeFoil: cannot generate a CoSinkable instance for " <> show bindingName
, " constructor " <> show conName <> " has a payload of raw type " <> pprint fieldType
, " which becomes scope-indexed; write the instance by hand"
, " (transportPayload is the sanctioned way to rebuild such a field)"
]
_ -> return ()
coSinkClauses <- mapM (mkCoSinkabilityProofClause config) flatCons
withPatClauses <- mapM (mkWithPatternClause config) flatCons
return
[ InstanceD Nothing [] (AppT (ConT ''Foil.CoSinkable) bindingT)
[ FunD 'Foil.coSinkabilityProof coSinkClauses
, FunD 'Foil.withPattern withPatClauses
]
]
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.
--
-- @since 0.2.0
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
(itvars, _cons) <- reifyDataOrNewtype rawIdentName
named <- newName "_named"
let funName = toFreeFoilNameFrom config rawBindingName
funWithName = toNameWith funName
rawRetType = PeelConT rawBindingName (map (VarT . tvarName) tvars)
rawIdentType = PeelConT rawIdentName (map (VarT . tvarName) (take (length itvars) tvars)) -- FIXME: undocumented hack :(
bindingType = toFreeFoilType SortBinder config (VarT outerScope) (VarT innerScope) rawRetType
clauses <- concat <$> mapM (toFreeFoilClauseFromBinding named config termConfig rawRetType) cons
addModFinalizer $ putDoc (DeclDoc funWithName)
("/Generated/ with '" ++ show 'mkFreeFoil ++ "'. Convert a scope-safe to a raw binding, naming the binders from their indices with the given function. The same function must name the bound-variable references, or a reference comes out free of its own binder.")
addModFinalizer $ putDoc (DeclDoc funName)
("/Generated/ with '" ++ show 'mkFreeFoil ++ "'. Convert a scope-safe to a raw binding, with the display naming.")
return
[ SigD funWithName ((ConT ''Int --> rawIdentType) --> bindingType --> rawRetType)
, FunD funWithName clauses
, SigD funName (bindingType --> rawRetType)
, FunD funName [ Clause [] (NormalB (VarE funWithName `AppE` VarE intToRawIdentName)) [] ]
]
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
tryFunName = mkName ("try" ++ capitalizeFirst (nameBase funName))
tryWithFunName = mkName (nameBase tryFunName ++ "With")
unresolvedType = ConT ''Foil.UnresolvedName `AppT` rawIdentType
tryTermType = ConT ''Either `AppT` unresolvedType `AppT` termType
convertArgs f = VarE f
`AppE` VarE funSigName
`AppE` VarE funBindingName
`AppE` VarE rawScopeToTermName
convertArgsIn f range = VarE f
`AppE` VarE funSigName
`AppE` (VarE (toNameIn funBindingName) `AppE` VarE range)
`AppE` VarE rawScopeToTermName
addModFinalizer $ putDoc (DeclDoc funName)
("/Generated/ with '" ++ show 'mkFreeFoil ++ "'. Convert from raw to scope-safe representation, calling 'error' on an identifier that does not resolve. See '" ++ nameBase tryFunName ++ "'.")
addModFinalizer $ putDoc (DeclDoc tryFunName)
("/Generated/ with '" ++ show 'mkFreeFoil ++ "'. Convert from raw to scope-safe representation, reporting the first identifier that does not resolve.")
addModFinalizer $ putDoc (DeclDoc tryWithFunName)
("/Generated/ with '" ++ show 'mkFreeFoil ++ "'. Same as '" ++ nameBase tryFunName ++ "', except that some identifiers may resolve to a whole term rather than to a variable.")
range <- newName "range"
let mkSig body =
ForallT
(PlainTV outerScope SpecifiedSpec : map (SpecifiedSpec <$) tvars)
[ ConT ''Foil.Distinct `AppT` VarT outerScope
, ConT ''Ord `AppT` rawIdentType ]
body
plainSigTail =
(ConT ''Foil.Scope `AppT` VarT outerScope)
--> (ConT ''Map `AppT` rawIdentType `AppT` (ConT ''Foil.Name `AppT` VarT outerScope))
--> rawTermType
--> termType
trySigTail =
(ConT ''Foil.Scope `AppT` VarT outerScope)
--> (ConT ''Map `AppT` rawIdentType `AppT` (ConT ''Foil.Name `AppT` VarT outerScope))
--> rawTermType
--> tryTermType
tryWithSigTail =
(ConT ''Foil.Scope `AppT` VarT outerScope)
--> (ConT ''Map `AppT` rawIdentType `AppT` (ConT ''Foil.Name `AppT` VarT outerScope))
--> (ConT ''Map `AppT` rawIdentType `AppT` termType)
--> rawTermType
--> tryTermType
forM_ [funName, tryFunName, tryWithFunName] $ \name ->
addModFinalizer $ putDoc (DeclDoc (toNameIn name))
("/Generated/ with '" ++ show 'mkFreeFoil ++ "'. Same as '" ++ nameBase name ++ "', except that the binders introduced by the conversion are allocated within the given range; see 'Foil.withFreshIn'.")
return $
[ SigD funName (mkSig plainSigTail)
, FunD funName [ Clause [] (NormalB (convertArgs 'Foil.unsafeConvertToAST)) [] ]
, SigD tryFunName (mkSig trySigTail)
, FunD tryFunName [ Clause [] (NormalB (convertArgs 'Foil.tryConvertToAST)) [] ]
, SigD tryWithFunName (mkSig tryWithSigTail)
, FunD tryWithFunName [ Clause [] (NormalB (convertArgs 'Foil.tryConvertToASTWith)) [] ]
] ++ concat
[ [ SigD inName (mkSig (ConT ''Foil.NameRange --> sigTail))
, FunD inName [ Clause [VarP range] (NormalB (convertArgsIn f range)) [] ]
]
| (name, sigTail, f) <-
[ (funName, plainSigTail, 'Foil.unsafeConvertToAST)
, (tryFunName, trySigTail, 'Foil.tryConvertToAST)
, (tryWithFunName, tryWithSigTail, 'Foil.tryConvertToASTWith)
]
, let inName = toNameIn name
]
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"
let funInName = toNameIn funName
bindingSigTail =
(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
bindingForall body =
ForallT
(PlainTV outerScope SpecifiedSpec : map (SpecifiedSpec <$) tvars ++ [PlainTV r SpecifiedSpec])
[ ConT ''Foil.Distinct `AppT` VarT outerScope
, ConT ''Ord `AppT` rawIdentType ]
body
addModFinalizer $ putDoc (DeclDoc funInName)
("/Generated/ with '" ++ show 'mkFreeFoil ++ "'. Convert from raw to scope-safe binding (CPS-style), allocating the binders within a given range; see 'Foil.withFreshIn'.")
addModFinalizer $ putDoc (DeclDoc funName)
("/Generated/ with '" ++ show 'mkFreeFoil ++ "'. Convert from raw to scope-safe binding (CPS-style). This is '" ++ nameBase funInName ++ "' at 'Foil.fullNameRange'.")
return
[ SigD funInName (bindingForall (ConT ''Foil.NameRange --> bindingSigTail))
, FunD funInName clauses
, SigD funName (bindingForall bindingSigTail)
, FunD funName [ Clause [] (NormalB (VarE funInName `AppE` VarE 'Foil.fullNameRange)) [] ]
]
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 -> Name -> [Type] -> Q ([Pat], [Exp], Exp -> Exp, Name)
goArgTypes _range _scope env [] = return ([], [], id, env)
goArgTypes range 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 range scope' env' ts
return (VarP x : pats, VarE x' : exps, \e ->
VarE 'Foil.withFreshIn `AppE` VarE range `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 = toNameIn (toFreeFoilNameTo config typeName)
(pats, exps, wrap, env'') <- goArgTypes range scope' env' ts
return (VarP x : pats, VarE x' : exps, \e ->
VarE funName `AppE` VarE range `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 range scope env ts
return (VarP x : pats, VarE x : exps, wrap, env')
go :: Con -> Q [Clause]
go = \case
GadtC conNames rawArgTypes _rawRetType -> concat <$> do
range <- newName "_range"
scope <- newName "_scope"
env <- newName "_env"
cont <- newName "_cont"
forM conNames $ \conName -> do
let newConName = toConName config conName
(pats, exps, wrap, env') <- goArgTypes range scope env (map snd rawArgTypes)
return
[ Clause [VarP range, 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
-- Matching a raw constructor, we must bind exactly one variable per raw
-- field. The binding (pattern) field binds @theBinder@, and each scoped
-- field binds only a body -- and then every scoped child of the free foil
-- node is given /the same/ @theBinder@, since the raw syntax names one
-- binder and a constructor binding several scopes binds it in each of them.
fromRawArgType :: Bool -> Name -> Name -> Type -> Q ([Pat], [Exp])
fromRawArgType isVarCon theIdent theBinder rawArgType
| isBindingField config rawArgType = return ([VarP theBinder], [])
| isScopeField config rawArgType = do
body <- newName "body"
return ([VarP body], [TupE [Just (VarE theBinder), Just (VarE body)]])
| otherwise = fromArgType isVarCon theIdent rawArgType
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"
theBinder <- newName "binder"
forM conNames $ \conName -> do
let newConName = toSignatureName config conName
isVarCon = conName == rawVarConName
(concat -> pats, concat -> exps) <- unzip <$>
mapM (fromRawArgType isVarCon theIdent theBinder . 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