{-# 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
  { FreeFoilConfig -> [Name]
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)
  , FreeFoilConfig -> [FreeFoilTermConfig]
freeFoilTermConfigs       :: [FreeFoilTermConfig]
  -- ^ Configurations for each term (e.g. expressions, types) group.
  , FreeFoilConfig -> String -> String
freeFoilNameModifier      :: String -> String
  -- ^ Name modifier for the Free Foil conterpart of a raw type name.
  -- Normally, this is just 'id'.
  , FreeFoilConfig -> String -> String
freeFoilScopeNameModifier :: String -> String
  -- ^ Name modifier for the scoped Free Foil conterpart of a raw type name.
  -- Normally, this is something like @("Scoped" ++)@.
  , FreeFoilConfig -> String -> String
signatureNameModifier     :: String -> String
  -- ^ Name modifier for the signature conterpart of a raw type name or raw constructor name.
  -- Normally, this is something like @(++ "Sig")@.
  , FreeFoilConfig -> String -> String
freeFoilConNameModifier   :: String -> String
  -- ^ Name modifier for the Free Foil conterpart (pattern synonym) of a raw constructor name.
  -- Normally, this is just 'id'.
  , FreeFoilConfig -> String -> String
freeFoilConvertToName     :: String -> String
  -- ^ Name of a conversion function (from raw to scope-safe) for a raw type name.
  -- Normally, this is something like @("to" ++)@.
  , FreeFoilConfig -> String -> String
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
  { FreeFoilTermConfig -> Name
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).
  , FreeFoilTermConfig -> Name
rawTermName           :: Name
    -- ^ The type name for the term.
    -- This will be the main recursive type to be converted into an 'Foil.AST'.
  , FreeFoilTermConfig -> Name
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.
  , FreeFoilTermConfig -> Name
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.
  , FreeFoilTermConfig -> Name
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'.
  , FreeFoilTermConfig -> [Name]
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.
  , FreeFoilTermConfig -> [Name]
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.
  , FreeFoilTermConfig -> Name
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.
  , FreeFoilTermConfig -> Name
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.
  , FreeFoilTermConfig -> Name
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.
  , FreeFoilTermConfig -> Name
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 :: String -> String
capitalizeFirst []       = []
capitalizeFirst (Char
c : String
cs) = Char -> Char
toUpper Char
c Char -> String -> String
forall a. a -> [a] -> [a]
: String
cs

toFreeFoilName :: FreeFoilConfig -> Name -> Name
toFreeFoilName :: FreeFoilConfig -> Name -> Name
toFreeFoilName FreeFoilConfig{[Name]
[FreeFoilTermConfig]
String -> String
rawQuantifiedNames :: FreeFoilConfig -> [Name]
freeFoilTermConfigs :: FreeFoilConfig -> [FreeFoilTermConfig]
freeFoilNameModifier :: FreeFoilConfig -> String -> String
freeFoilScopeNameModifier :: FreeFoilConfig -> String -> String
signatureNameModifier :: FreeFoilConfig -> String -> String
freeFoilConNameModifier :: FreeFoilConfig -> String -> String
freeFoilConvertToName :: FreeFoilConfig -> String -> String
freeFoilConvertFromName :: FreeFoilConfig -> String -> String
rawQuantifiedNames :: [Name]
freeFoilTermConfigs :: [FreeFoilTermConfig]
freeFoilNameModifier :: String -> String
freeFoilScopeNameModifier :: String -> String
signatureNameModifier :: String -> String
freeFoilConNameModifier :: String -> String
freeFoilConvertToName :: String -> String
freeFoilConvertFromName :: String -> String
..} Name
name = String -> Name
mkName (String -> String
freeFoilNameModifier (Name -> String
nameBase Name
name))

toFreeFoilNameFrom :: FreeFoilConfig -> Name -> Name
toFreeFoilNameFrom :: FreeFoilConfig -> Name -> Name
toFreeFoilNameFrom FreeFoilConfig{[Name]
[FreeFoilTermConfig]
String -> String
rawQuantifiedNames :: FreeFoilConfig -> [Name]
freeFoilTermConfigs :: FreeFoilConfig -> [FreeFoilTermConfig]
freeFoilNameModifier :: FreeFoilConfig -> String -> String
freeFoilScopeNameModifier :: FreeFoilConfig -> String -> String
signatureNameModifier :: FreeFoilConfig -> String -> String
freeFoilConNameModifier :: FreeFoilConfig -> String -> String
freeFoilConvertToName :: FreeFoilConfig -> String -> String
freeFoilConvertFromName :: FreeFoilConfig -> String -> String
rawQuantifiedNames :: [Name]
freeFoilTermConfigs :: [FreeFoilTermConfig]
freeFoilNameModifier :: String -> String
freeFoilScopeNameModifier :: String -> String
signatureNameModifier :: String -> String
freeFoilConNameModifier :: String -> String
freeFoilConvertToName :: String -> String
freeFoilConvertFromName :: String -> String
..} Name
name = String -> Name
mkName (String -> String
freeFoilConvertFromName (Name -> String
nameBase Name
name))

toFreeFoilNameTo :: FreeFoilConfig -> Name -> Name
toFreeFoilNameTo :: FreeFoilConfig -> Name -> Name
toFreeFoilNameTo FreeFoilConfig{[Name]
[FreeFoilTermConfig]
String -> String
rawQuantifiedNames :: FreeFoilConfig -> [Name]
freeFoilTermConfigs :: FreeFoilConfig -> [FreeFoilTermConfig]
freeFoilNameModifier :: FreeFoilConfig -> String -> String
freeFoilScopeNameModifier :: FreeFoilConfig -> String -> String
signatureNameModifier :: FreeFoilConfig -> String -> String
freeFoilConNameModifier :: FreeFoilConfig -> String -> String
freeFoilConvertToName :: FreeFoilConfig -> String -> String
freeFoilConvertFromName :: FreeFoilConfig -> String -> String
rawQuantifiedNames :: [Name]
freeFoilTermConfigs :: [FreeFoilTermConfig]
freeFoilNameModifier :: String -> String
freeFoilScopeNameModifier :: String -> String
signatureNameModifier :: String -> String
freeFoilConNameModifier :: String -> String
freeFoilConvertToName :: String -> String
freeFoilConvertFromName :: String -> String
..} Name
name = String -> Name
mkName (String -> String
freeFoilConvertToName (Name -> String
nameBase Name
name))

-- | The name of the range-parametric sibling of a generated definition
-- (see 'Foil.withFreshIn'): @toPatternIn@ beside @toPattern@.
toNameIn :: Name -> Name
toNameIn :: Name -> Name
toNameIn Name
name = String -> Name
mkName (Name -> String
nameBase Name
name String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"In")

-- | The name of the naming-parametric sibling of a generated definition:
-- @fromPatternWith@ beside @fromPattern@.
toNameWith :: Name -> Name
toNameWith :: Name -> Name
toNameWith Name
name = String -> Name
mkName (Name -> String
nameBase Name
name String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"With")

toFreeFoilScopedName :: FreeFoilConfig -> Name -> Name
toFreeFoilScopedName :: FreeFoilConfig -> Name -> Name
toFreeFoilScopedName FreeFoilConfig{[Name]
[FreeFoilTermConfig]
String -> String
rawQuantifiedNames :: FreeFoilConfig -> [Name]
freeFoilTermConfigs :: FreeFoilConfig -> [FreeFoilTermConfig]
freeFoilNameModifier :: FreeFoilConfig -> String -> String
freeFoilScopeNameModifier :: FreeFoilConfig -> String -> String
signatureNameModifier :: FreeFoilConfig -> String -> String
freeFoilConNameModifier :: FreeFoilConfig -> String -> String
freeFoilConvertToName :: FreeFoilConfig -> String -> String
freeFoilConvertFromName :: FreeFoilConfig -> String -> String
rawQuantifiedNames :: [Name]
freeFoilTermConfigs :: [FreeFoilTermConfig]
freeFoilNameModifier :: String -> String
freeFoilScopeNameModifier :: String -> String
signatureNameModifier :: String -> String
freeFoilConNameModifier :: String -> String
freeFoilConvertToName :: String -> String
freeFoilConvertFromName :: String -> String
..} Name
name = String -> Name
mkName (String -> String
freeFoilScopeNameModifier (Name -> String
nameBase Name
name))

toSignatureName :: FreeFoilConfig -> Name -> Name
toSignatureName :: FreeFoilConfig -> Name -> Name
toSignatureName FreeFoilConfig{[Name]
[FreeFoilTermConfig]
String -> String
rawQuantifiedNames :: FreeFoilConfig -> [Name]
freeFoilTermConfigs :: FreeFoilConfig -> [FreeFoilTermConfig]
freeFoilNameModifier :: FreeFoilConfig -> String -> String
freeFoilScopeNameModifier :: FreeFoilConfig -> String -> String
signatureNameModifier :: FreeFoilConfig -> String -> String
freeFoilConNameModifier :: FreeFoilConfig -> String -> String
freeFoilConvertToName :: FreeFoilConfig -> String -> String
freeFoilConvertFromName :: FreeFoilConfig -> String -> String
rawQuantifiedNames :: [Name]
freeFoilTermConfigs :: [FreeFoilTermConfig]
freeFoilNameModifier :: String -> String
freeFoilScopeNameModifier :: String -> String
signatureNameModifier :: String -> String
freeFoilConNameModifier :: String -> String
freeFoilConvertToName :: String -> String
freeFoilConvertFromName :: String -> String
..} Name
name = String -> Name
mkName (String -> String
signatureNameModifier (Name -> String
nameBase Name
name))

toConName :: FreeFoilConfig -> Name -> Name
toConName :: FreeFoilConfig -> Name -> Name
toConName FreeFoilConfig{[Name]
[FreeFoilTermConfig]
String -> String
rawQuantifiedNames :: FreeFoilConfig -> [Name]
freeFoilTermConfigs :: FreeFoilConfig -> [FreeFoilTermConfig]
freeFoilNameModifier :: FreeFoilConfig -> String -> String
freeFoilScopeNameModifier :: FreeFoilConfig -> String -> String
signatureNameModifier :: FreeFoilConfig -> String -> String
freeFoilConNameModifier :: FreeFoilConfig -> String -> String
freeFoilConvertToName :: FreeFoilConfig -> String -> String
freeFoilConvertFromName :: FreeFoilConfig -> String -> String
rawQuantifiedNames :: [Name]
freeFoilTermConfigs :: [FreeFoilTermConfig]
freeFoilNameModifier :: String -> String
freeFoilScopeNameModifier :: String -> String
signatureNameModifier :: String -> String
freeFoilConNameModifier :: String -> String
freeFoilConvertToName :: String -> String
freeFoilConvertFromName :: String -> String
..} Name
name = String -> Name
mkName (String -> String
freeFoilConNameModifier (Name -> String
nameBase Name
name))

lookupIdentName :: Name -> [FreeFoilTermConfig] -> Maybe FreeFoilTermConfig
lookupIdentName :: Name -> [FreeFoilTermConfig] -> Maybe FreeFoilTermConfig
lookupIdentName Name
name = (FreeFoilTermConfig -> Bool)
-> [FreeFoilTermConfig] -> Maybe FreeFoilTermConfig
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find (\FreeFoilTermConfig{[Name]
Name
rawIdentName :: FreeFoilTermConfig -> Name
rawTermName :: FreeFoilTermConfig -> Name
rawBindingName :: FreeFoilTermConfig -> Name
rawScopeName :: FreeFoilTermConfig -> Name
rawVarConName :: FreeFoilTermConfig -> Name
rawSubTermNames :: FreeFoilTermConfig -> [Name]
rawSubScopeNames :: FreeFoilTermConfig -> [Name]
intToRawIdentName :: FreeFoilTermConfig -> Name
rawVarIdentToTermName :: FreeFoilTermConfig -> Name
rawTermToScopeName :: FreeFoilTermConfig -> Name
rawScopeToTermName :: FreeFoilTermConfig -> Name
rawIdentName :: Name
rawTermName :: Name
rawBindingName :: Name
rawScopeName :: Name
rawVarConName :: Name
rawSubTermNames :: [Name]
rawSubScopeNames :: [Name]
intToRawIdentName :: Name
rawVarIdentToTermName :: Name
rawTermToScopeName :: Name
rawScopeToTermName :: Name
..} -> Name
rawIdentName Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
name)

lookupTermName :: Name -> [FreeFoilTermConfig] -> Maybe FreeFoilTermConfig
lookupTermName :: Name -> [FreeFoilTermConfig] -> Maybe FreeFoilTermConfig
lookupTermName Name
name = (FreeFoilTermConfig -> Bool)
-> [FreeFoilTermConfig] -> Maybe FreeFoilTermConfig
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find (\FreeFoilTermConfig{[Name]
Name
rawIdentName :: FreeFoilTermConfig -> Name
rawTermName :: FreeFoilTermConfig -> Name
rawBindingName :: FreeFoilTermConfig -> Name
rawScopeName :: FreeFoilTermConfig -> Name
rawVarConName :: FreeFoilTermConfig -> Name
rawSubTermNames :: FreeFoilTermConfig -> [Name]
rawSubScopeNames :: FreeFoilTermConfig -> [Name]
intToRawIdentName :: FreeFoilTermConfig -> Name
rawVarIdentToTermName :: FreeFoilTermConfig -> Name
rawTermToScopeName :: FreeFoilTermConfig -> Name
rawScopeToTermName :: FreeFoilTermConfig -> Name
rawIdentName :: Name
rawTermName :: Name
rawBindingName :: Name
rawScopeName :: Name
rawVarConName :: Name
rawSubTermNames :: [Name]
rawSubScopeNames :: [Name]
intToRawIdentName :: Name
rawVarIdentToTermName :: Name
rawTermToScopeName :: Name
rawScopeToTermName :: Name
..} -> Name
rawTermName Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
name)

lookupSubTermName :: Name -> [FreeFoilTermConfig] -> Maybe FreeFoilTermConfig
lookupSubTermName :: Name -> [FreeFoilTermConfig] -> Maybe FreeFoilTermConfig
lookupSubTermName Name
name = (FreeFoilTermConfig -> Bool)
-> [FreeFoilTermConfig] -> Maybe FreeFoilTermConfig
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find (\FreeFoilTermConfig{[Name]
Name
rawIdentName :: FreeFoilTermConfig -> Name
rawTermName :: FreeFoilTermConfig -> Name
rawBindingName :: FreeFoilTermConfig -> Name
rawScopeName :: FreeFoilTermConfig -> Name
rawVarConName :: FreeFoilTermConfig -> Name
rawSubTermNames :: FreeFoilTermConfig -> [Name]
rawSubScopeNames :: FreeFoilTermConfig -> [Name]
intToRawIdentName :: FreeFoilTermConfig -> Name
rawVarIdentToTermName :: FreeFoilTermConfig -> Name
rawTermToScopeName :: FreeFoilTermConfig -> Name
rawScopeToTermName :: FreeFoilTermConfig -> Name
rawIdentName :: Name
rawTermName :: Name
rawBindingName :: Name
rawScopeName :: Name
rawVarConName :: Name
rawSubTermNames :: [Name]
rawSubScopeNames :: [Name]
intToRawIdentName :: Name
rawVarIdentToTermName :: Name
rawTermToScopeName :: Name
rawScopeToTermName :: Name
..} -> Name
name Name -> [Name] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
rawSubTermNames)

lookupSubScopeName :: Name -> [FreeFoilTermConfig] -> Maybe FreeFoilTermConfig
lookupSubScopeName :: Name -> [FreeFoilTermConfig] -> Maybe FreeFoilTermConfig
lookupSubScopeName Name
name = (FreeFoilTermConfig -> Bool)
-> [FreeFoilTermConfig] -> Maybe FreeFoilTermConfig
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find (\FreeFoilTermConfig{[Name]
Name
rawIdentName :: FreeFoilTermConfig -> Name
rawTermName :: FreeFoilTermConfig -> Name
rawBindingName :: FreeFoilTermConfig -> Name
rawScopeName :: FreeFoilTermConfig -> Name
rawVarConName :: FreeFoilTermConfig -> Name
rawSubTermNames :: FreeFoilTermConfig -> [Name]
rawSubScopeNames :: FreeFoilTermConfig -> [Name]
intToRawIdentName :: FreeFoilTermConfig -> Name
rawVarIdentToTermName :: FreeFoilTermConfig -> Name
rawTermToScopeName :: FreeFoilTermConfig -> Name
rawScopeToTermName :: FreeFoilTermConfig -> Name
rawIdentName :: Name
rawTermName :: Name
rawBindingName :: Name
rawScopeName :: Name
rawVarConName :: Name
rawSubTermNames :: [Name]
rawSubScopeNames :: [Name]
intToRawIdentName :: Name
rawVarIdentToTermName :: Name
rawTermToScopeName :: Name
rawScopeToTermName :: Name
..} -> Name
name Name -> [Name] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
rawSubScopeNames)

lookupBindingName :: Name -> [FreeFoilTermConfig] -> Maybe FreeFoilTermConfig
lookupBindingName :: Name -> [FreeFoilTermConfig] -> Maybe FreeFoilTermConfig
lookupBindingName Name
name = (FreeFoilTermConfig -> Bool)
-> [FreeFoilTermConfig] -> Maybe FreeFoilTermConfig
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find (\FreeFoilTermConfig{[Name]
Name
rawIdentName :: FreeFoilTermConfig -> Name
rawTermName :: FreeFoilTermConfig -> Name
rawBindingName :: FreeFoilTermConfig -> Name
rawScopeName :: FreeFoilTermConfig -> Name
rawVarConName :: FreeFoilTermConfig -> Name
rawSubTermNames :: FreeFoilTermConfig -> [Name]
rawSubScopeNames :: FreeFoilTermConfig -> [Name]
intToRawIdentName :: FreeFoilTermConfig -> Name
rawVarIdentToTermName :: FreeFoilTermConfig -> Name
rawTermToScopeName :: FreeFoilTermConfig -> Name
rawScopeToTermName :: FreeFoilTermConfig -> Name
rawIdentName :: Name
rawTermName :: Name
rawBindingName :: Name
rawScopeName :: Name
rawVarConName :: Name
rawSubTermNames :: [Name]
rawSubScopeNames :: [Name]
intToRawIdentName :: Name
rawVarIdentToTermName :: Name
rawTermToScopeName :: Name
rawScopeToTermName :: Name
..} -> Name
rawBindingName Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
name)

lookupScopeName :: Name -> [FreeFoilTermConfig] -> Maybe FreeFoilTermConfig
lookupScopeName :: Name -> [FreeFoilTermConfig] -> Maybe FreeFoilTermConfig
lookupScopeName Name
name = (FreeFoilTermConfig -> Bool)
-> [FreeFoilTermConfig] -> Maybe FreeFoilTermConfig
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find (\FreeFoilTermConfig{[Name]
Name
rawIdentName :: FreeFoilTermConfig -> Name
rawTermName :: FreeFoilTermConfig -> Name
rawBindingName :: FreeFoilTermConfig -> Name
rawScopeName :: FreeFoilTermConfig -> Name
rawVarConName :: FreeFoilTermConfig -> Name
rawSubTermNames :: FreeFoilTermConfig -> [Name]
rawSubScopeNames :: FreeFoilTermConfig -> [Name]
intToRawIdentName :: FreeFoilTermConfig -> Name
rawVarIdentToTermName :: FreeFoilTermConfig -> Name
rawTermToScopeName :: FreeFoilTermConfig -> Name
rawScopeToTermName :: FreeFoilTermConfig -> Name
rawIdentName :: Name
rawTermName :: Name
rawBindingName :: Name
rawScopeName :: Name
rawVarConName :: Name
rawSubTermNames :: [Name]
rawSubScopeNames :: [Name]
intToRawIdentName :: Name
rawVarIdentToTermName :: Name
rawTermToScopeName :: Name
rawScopeToTermName :: Name
..} -> Name
rawScopeName Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
name)

data Sort
  = SortBinder | SortTerm | SortSubTerm

toFreeFoilType :: Sort -> FreeFoilConfig -> Type -> Type -> Type -> Type
toFreeFoilType :: Sort -> FreeFoilConfig -> Type -> Type -> Type -> Type
toFreeFoilType Sort
isBinder config :: FreeFoilConfig
config@FreeFoilConfig{[Name]
[FreeFoilTermConfig]
String -> String
rawQuantifiedNames :: FreeFoilConfig -> [Name]
freeFoilTermConfigs :: FreeFoilConfig -> [FreeFoilTermConfig]
freeFoilNameModifier :: FreeFoilConfig -> String -> String
freeFoilScopeNameModifier :: FreeFoilConfig -> String -> String
signatureNameModifier :: FreeFoilConfig -> String -> String
freeFoilConNameModifier :: FreeFoilConfig -> String -> String
freeFoilConvertToName :: FreeFoilConfig -> String -> String
freeFoilConvertFromName :: FreeFoilConfig -> String -> String
rawQuantifiedNames :: [Name]
freeFoilTermConfigs :: [FreeFoilTermConfig]
freeFoilNameModifier :: String -> String
freeFoilScopeNameModifier :: String -> String
signatureNameModifier :: String -> String
freeFoilConNameModifier :: String -> String
freeFoilConvertToName :: String -> String
freeFoilConvertFromName :: String -> String
..} Type
outerScope Type
innerScope = Type -> Type
go
  where
    go :: Type -> Type
go = \case
      PeelConT Name
typeName ((Type -> Type) -> [Type] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Type -> Type
go -> [Type]
typeParams)
        | Name
typeName Name -> [Name] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
rawQuantifiedNames ->
            Name -> [Type] -> Type
PeelConT (FreeFoilConfig -> Name -> Name
toFreeFoilName FreeFoilConfig
config Name
typeName) ([Type]
typeParams [Type] -> [Type] -> [Type]
forall a. [a] -> [a] -> [a]
++ [Type
outerScope])
        | Name
typeName Name -> [Name] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` (FreeFoilTermConfig -> Name) -> [FreeFoilTermConfig] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map FreeFoilTermConfig -> Name
rawIdentName [FreeFoilTermConfig]
freeFoilTermConfigs ->
            case Sort
isBinder of
              Sort
SortBinder -> Name -> [Type] -> Type
PeelConT ''Foil.NameBinder [Type
outerScope, Type
innerScope]
              Sort
_          -> Name -> [Type] -> Type
PeelConT ''Foil.Name [Type
outerScope]
        | Just FreeFoilTermConfig
_ <- Name -> [FreeFoilTermConfig] -> Maybe FreeFoilTermConfig
lookupTermName Name
typeName [FreeFoilTermConfig]
freeFoilTermConfigs ->
            Name -> [Type] -> Type
PeelConT (FreeFoilConfig -> Name -> Name
toFreeFoilName FreeFoilConfig
config Name
typeName) ([Type]
typeParams [Type] -> [Type] -> [Type]
forall a. [a] -> [a] -> [a]
++ [Type
outerScope])
        | Just FreeFoilTermConfig
_ <- Name -> [FreeFoilTermConfig] -> Maybe FreeFoilTermConfig
lookupBindingName Name
typeName [FreeFoilTermConfig]
freeFoilTermConfigs ->
            Name -> [Type] -> Type
PeelConT (FreeFoilConfig -> Name -> Name
toFreeFoilName FreeFoilConfig
config Name
typeName) ([Type]
typeParams [Type] -> [Type] -> [Type]
forall a. [a] -> [a] -> [a]
++ [Type
outerScope, Type
innerScope])
        | Just FreeFoilTermConfig{[Name]
Name
rawIdentName :: FreeFoilTermConfig -> Name
rawTermName :: FreeFoilTermConfig -> Name
rawBindingName :: FreeFoilTermConfig -> Name
rawScopeName :: FreeFoilTermConfig -> Name
rawVarConName :: FreeFoilTermConfig -> Name
rawSubTermNames :: FreeFoilTermConfig -> [Name]
rawSubScopeNames :: FreeFoilTermConfig -> [Name]
intToRawIdentName :: FreeFoilTermConfig -> Name
rawVarIdentToTermName :: FreeFoilTermConfig -> Name
rawTermToScopeName :: FreeFoilTermConfig -> Name
rawScopeToTermName :: FreeFoilTermConfig -> Name
rawIdentName :: Name
rawTermName :: Name
rawBindingName :: Name
rawScopeName :: Name
rawVarConName :: Name
rawSubTermNames :: [Name]
rawSubScopeNames :: [Name]
intToRawIdentName :: Name
rawVarIdentToTermName :: Name
rawTermToScopeName :: Name
rawScopeToTermName :: Name
..} <- Name -> [FreeFoilTermConfig] -> Maybe FreeFoilTermConfig
lookupScopeName Name
typeName [FreeFoilTermConfig]
freeFoilTermConfigs ->
            Name -> [Type] -> Type
PeelConT (FreeFoilConfig -> Name -> Name
toFreeFoilName FreeFoilConfig
config Name
rawTermName) ([Type]
typeParams [Type] -> [Type] -> [Type]
forall a. [a] -> [a] -> [a]
++ [Type
innerScope])
        | Just FreeFoilTermConfig
_ <- Name -> [FreeFoilTermConfig] -> Maybe FreeFoilTermConfig
lookupSubTermName Name
typeName [FreeFoilTermConfig]
freeFoilTermConfigs ->
            Name -> [Type] -> Type
PeelConT (FreeFoilConfig -> Name -> Name
toFreeFoilName FreeFoilConfig
config Name
typeName) ([Type]
typeParams [Type] -> [Type] -> [Type]
forall a. [a] -> [a] -> [a]
++ [Type
outerScope])
        | Just FreeFoilTermConfig
_ <- Name -> [FreeFoilTermConfig] -> Maybe FreeFoilTermConfig
lookupSubScopeName Name
typeName [FreeFoilTermConfig]
freeFoilTermConfigs ->
            Name -> [Type] -> Type
PeelConT (FreeFoilConfig -> Name -> Name
toFreeFoilName FreeFoilConfig
config Name
typeName) ([Type]
typeParams [Type] -> [Type] -> [Type]
forall a. [a] -> [a] -> [a]
++ [Type
innerScope])
      ForallT [TyVarBndr Specificity]
bndrs [Type]
ctx Type
type_ -> [TyVarBndr Specificity] -> [Type] -> Type -> Type
ForallT [TyVarBndr Specificity]
bndrs [Type]
ctx (Type -> Type
go Type
type_)
      ForallVisT [TyVarBndr ()]
bndrs Type
type_ -> [TyVarBndr ()] -> Type -> Type
ForallVisT [TyVarBndr ()]
bndrs (Type -> Type
go Type
type_)
      AppT Type
f Type
x -> Type -> Type -> Type
AppT (Type -> Type
go Type
f) (Type -> Type
go Type
x)
      AppKindT Type
f Type
k -> Type -> Type -> Type
AppKindT (Type -> Type
go Type
f) Type
k
      SigT Type
t Type
k -> Type -> Type -> Type
SigT (Type -> Type
go Type
t) Type
k
      t :: Type
t@ConT{} -> Type
t
      t :: Type
t@VarT{} -> Type
t
      t :: Type
t@PromotedT{} -> Type
t
      InfixT Type
l Name
op Type
r -> Type -> Name -> Type -> Type
InfixT (Type -> Type
go Type
l) Name
op (Type -> Type
go Type
r)
      UInfixT Type
l Name
op Type
r -> Type -> Name -> Type -> Type
UInfixT (Type -> Type
go Type
l) Name
op (Type -> Type
go Type
r)
      PromotedInfixT Type
l Name
op Type
r -> Type -> Name -> Type -> Type
PromotedInfixT (Type -> Type
go Type
l) Name
op (Type -> Type
go Type
r)
      PromotedUInfixT Type
l Name
op Type
r -> Type -> Name -> Type -> Type
PromotedUInfixT (Type -> Type
go Type
l) Name
op (Type -> Type
go Type
r)
      ParensT Type
t -> Type -> Type
ParensT (Type -> Type
go Type
t)
      t :: Type
t@TupleT{} -> Type
t
      t :: Type
t@UnboxedTupleT{} -> Type
t
      t :: Type
t@UnboxedSumT{} -> Type
t
      t :: Type
t@ArrowT{} -> Type
t
      t :: Type
t@MulArrowT{} -> Type
t
      t :: Type
t@EqualityT{} -> Type
t
      t :: Type
t@ListT{} -> Type
t
      t :: Type
t@PromotedTupleT{} -> Type
t
      t :: Type
t@PromotedNilT{} -> Type
t
      t :: Type
t@PromotedConsT{} -> Type
t
      t :: Type
t@StarT{} -> Type
t
      t :: Type
t@ConstraintT{} -> Type
t
      t :: Type
t@LitT{} -> Type
t
      t :: Type
t@WildCardT{} -> Type
t
      ImplicitParamT String
s Type
t -> String -> Type -> Type
ImplicitParamT String
s (Type -> Type
go Type
t)

toFreeFoilSigType :: Sort -> FreeFoilConfig -> Type -> Type -> Type -> Maybe Type
toFreeFoilSigType :: Sort -> FreeFoilConfig -> Type -> Type -> Type -> Maybe Type
toFreeFoilSigType Sort
sort config :: FreeFoilConfig
config@FreeFoilConfig{[Name]
[FreeFoilTermConfig]
String -> String
rawQuantifiedNames :: FreeFoilConfig -> [Name]
freeFoilTermConfigs :: FreeFoilConfig -> [FreeFoilTermConfig]
freeFoilNameModifier :: FreeFoilConfig -> String -> String
freeFoilScopeNameModifier :: FreeFoilConfig -> String -> String
signatureNameModifier :: FreeFoilConfig -> String -> String
freeFoilConNameModifier :: FreeFoilConfig -> String -> String
freeFoilConvertToName :: FreeFoilConfig -> String -> String
freeFoilConvertFromName :: FreeFoilConfig -> String -> String
rawQuantifiedNames :: [Name]
freeFoilTermConfigs :: [FreeFoilTermConfig]
freeFoilNameModifier :: String -> String
freeFoilScopeNameModifier :: String -> String
signatureNameModifier :: String -> String
freeFoilConNameModifier :: String -> String
freeFoilConvertToName :: String -> String
freeFoilConvertFromName :: String -> String
..} Type
scope Type
term = Type -> Maybe Type
go
  where
    go :: Type -> Maybe Type
    go :: Type -> Maybe Type
go = \case
      PeelConT Name
_typeName ((Type -> Maybe Type) -> [Type] -> Maybe [Type]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Type -> Maybe Type
go -> Maybe [Type]
Nothing) ->
        String -> Maybe Type
forall a. HasCallStack => String -> a
error String
"bad type params"
      PeelConT Name
typeName ((Type -> Maybe Type) -> [Type] -> Maybe [Type]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Type -> Maybe Type
go -> Just [Type]
typeParams)
        | Just FreeFoilTermConfig
_ <- Name -> [FreeFoilTermConfig] -> Maybe FreeFoilTermConfig
lookupTermName Name
typeName [FreeFoilTermConfig]
freeFoilTermConfigs ->
            case Sort
sort of
              Sort
SortSubTerm -> Type -> Maybe Type
forall a. a -> Maybe a
Just (Name -> [Type] -> Type
PeelConT (FreeFoilConfig -> Name -> Name
toSignatureName FreeFoilConfig
config Name
typeName) ([Type]
typeParams [Type] -> [Type] -> [Type]
forall a. [a] -> [a] -> [a]
++ [Type
scope, Type
term]))
              Sort
_           -> Type -> Maybe Type
forall a. a -> Maybe a
Just Type
term
        | Just FreeFoilTermConfig
_ <- Name -> [FreeFoilTermConfig] -> Maybe FreeFoilTermConfig
lookupBindingName Name
typeName [FreeFoilTermConfig]
freeFoilTermConfigs ->
            Maybe Type
forall a. Maybe a
Nothing
        | Just FreeFoilTermConfig
_ <- Name -> [FreeFoilTermConfig] -> Maybe FreeFoilTermConfig
lookupScopeName Name
typeName [FreeFoilTermConfig]
freeFoilTermConfigs ->
            Type -> Maybe Type
forall a. a -> Maybe a
Just Type
scope
        | Just FreeFoilTermConfig
_ <- Name -> [FreeFoilTermConfig] -> Maybe FreeFoilTermConfig
lookupSubTermName Name
typeName [FreeFoilTermConfig]
freeFoilTermConfigs ->
            Type -> Maybe Type
forall a. a -> Maybe a
Just (Name -> [Type] -> Type
PeelConT (FreeFoilConfig -> Name -> Name
toSignatureName FreeFoilConfig
config Name
typeName) ([Type]
typeParams [Type] -> [Type] -> [Type]
forall a. [a] -> [a] -> [a]
++ [Type
scope, Type
term]))
        | Just FreeFoilTermConfig
_ <- Name -> [FreeFoilTermConfig] -> Maybe FreeFoilTermConfig
lookupSubScopeName Name
typeName [FreeFoilTermConfig]
freeFoilTermConfigs ->
            Type -> Maybe Type
forall a. a -> Maybe a
Just (Name -> [Type] -> Type
PeelConT (FreeFoilConfig -> Name -> Name
toSignatureName FreeFoilConfig
config Name
typeName) ([Type]
typeParams [Type] -> [Type] -> [Type]
forall a. [a] -> [a] -> [a]
++ [Type
scope, Type
term]))
      ForallT [TyVarBndr Specificity]
bndrs [Type]
ctx Type
type_ -> [TyVarBndr Specificity] -> [Type] -> Type -> Type
ForallT [TyVarBndr Specificity]
bndrs [Type]
ctx (Type -> Type) -> Maybe Type -> Maybe Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> Maybe Type
go Type
type_
      ForallVisT [TyVarBndr ()]
bndrs Type
type_ -> [TyVarBndr ()] -> Type -> Type
ForallVisT [TyVarBndr ()]
bndrs (Type -> Type) -> Maybe Type -> Maybe Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> Maybe Type
go Type
type_
      AppT Type
f Type
x -> Type -> Type -> Type
AppT (Type -> Type -> Type) -> Maybe Type -> Maybe (Type -> Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> Maybe Type
go Type
f Maybe (Type -> Type) -> Maybe Type -> Maybe Type
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type -> Maybe Type
go Type
x
      AppKindT Type
f Type
k -> Type -> Type -> Type
AppKindT (Type -> Type -> Type) -> Maybe Type -> Maybe (Type -> Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> Maybe Type
go Type
f Maybe (Type -> Type) -> Maybe Type -> Maybe Type
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type -> Maybe Type
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type
k
      SigT Type
t Type
k -> Type -> Type -> Type
SigT (Type -> Type -> Type) -> Maybe Type -> Maybe (Type -> Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> Maybe Type
go Type
t Maybe (Type -> Type) -> Maybe Type -> Maybe Type
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type -> Maybe Type
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type
k
      t :: Type
t@ConT{} -> Type -> Maybe Type
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type
t
      t :: Type
t@VarT{} -> Type -> Maybe Type
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type
t
      t :: Type
t@PromotedT{} -> Type -> Maybe Type
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type
t
      InfixT Type
l Name
op Type
r -> Type -> Name -> Type -> Type
InfixT (Type -> Name -> Type -> Type)
-> Maybe Type -> Maybe (Name -> Type -> Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> Maybe Type
go Type
l Maybe (Name -> Type -> Type) -> Maybe Name -> Maybe (Type -> Type)
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Name -> Maybe Name
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Name
op Maybe (Type -> Type) -> Maybe Type -> Maybe Type
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type -> Maybe Type
go Type
r
      UInfixT Type
l Name
op Type
r -> Type -> Name -> Type -> Type
UInfixT (Type -> Name -> Type -> Type)
-> Maybe Type -> Maybe (Name -> Type -> Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> Maybe Type
go Type
l Maybe (Name -> Type -> Type) -> Maybe Name -> Maybe (Type -> Type)
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Name -> Maybe Name
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Name
op Maybe (Type -> Type) -> Maybe Type -> Maybe Type
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type -> Maybe Type
go Type
r
      PromotedInfixT Type
l Name
op Type
r -> Type -> Name -> Type -> Type
PromotedInfixT (Type -> Name -> Type -> Type)
-> Maybe Type -> Maybe (Name -> Type -> Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> Maybe Type
go Type
l Maybe (Name -> Type -> Type) -> Maybe Name -> Maybe (Type -> Type)
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Name -> Maybe Name
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Name
op Maybe (Type -> Type) -> Maybe Type -> Maybe Type
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type -> Maybe Type
go Type
r
      PromotedUInfixT Type
l Name
op Type
r -> Type -> Name -> Type -> Type
PromotedUInfixT (Type -> Name -> Type -> Type)
-> Maybe Type -> Maybe (Name -> Type -> Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> Maybe Type
go Type
l Maybe (Name -> Type -> Type) -> Maybe Name -> Maybe (Type -> Type)
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Name -> Maybe Name
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Name
op Maybe (Type -> Type) -> Maybe Type -> Maybe Type
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type -> Maybe Type
go Type
r
      ParensT Type
t -> Type -> Type
ParensT (Type -> Type) -> Maybe Type -> Maybe Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> Maybe Type
go Type
t
      t :: Type
t@TupleT{} -> Type -> Maybe Type
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type
t
      t :: Type
t@UnboxedTupleT{} -> Type -> Maybe Type
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type
t
      t :: Type
t@UnboxedSumT{} -> Type -> Maybe Type
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type
t
      t :: Type
t@ArrowT{} -> Type -> Maybe Type
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type
t
      t :: Type
t@MulArrowT{} -> Type -> Maybe Type
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type
t
      t :: Type
t@EqualityT{} -> Type -> Maybe Type
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type
t
      t :: Type
t@ListT{} -> Type -> Maybe Type
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type
t
      t :: Type
t@PromotedTupleT{} -> Type -> Maybe Type
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type
t
      t :: Type
t@PromotedNilT{} -> Type -> Maybe Type
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type
t
      t :: Type
t@PromotedConsT{} -> Type -> Maybe Type
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type
t
      t :: Type
t@StarT{} -> Type -> Maybe Type
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type
t
      t :: Type
t@ConstraintT{} -> Type -> Maybe Type
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type
t
      t :: Type
t@LitT{} -> Type -> Maybe Type
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type
t
      t :: Type
t@WildCardT{} -> Type -> Maybe Type
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type
t
      ImplicitParamT String
s Type
t -> String -> Type -> Type
ImplicitParamT String
s (Type -> Type) -> Maybe Type -> Maybe Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> Maybe Type
go Type
t

toFreeFoilCon :: FreeFoilConfig -> Type -> Type -> Type -> Con -> Q Con
toFreeFoilCon :: FreeFoilConfig -> Type -> Type -> Type -> Con -> Q Con
toFreeFoilCon FreeFoilConfig
config Type
rawRetType Type
outerScope Type
innerScope = Con -> Q Con
go
  where
    goType :: Type -> Type
goType = Sort -> FreeFoilConfig -> Type -> Type -> Type -> Type
toFreeFoilType Sort
SortTerm FreeFoilConfig
config Type
outerScope Type
innerScope
    go :: Con -> Q Con
go = \case
      GadtC [Name]
conNames [BangType]
argTypes Type
retType -> do
        let newConNames :: [Name]
newConNames = (Name -> Name) -> [Name] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (FreeFoilConfig -> Name -> Name
toConName FreeFoilConfig
config) [Name]
conNames
        [(Name, Name)] -> ((Name, Name) -> Q ()) -> Q ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ ([Name] -> [Name] -> [(Name, Name)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Name]
conNames [Name]
newConNames) (((Name, Name) -> Q ()) -> Q ()) -> ((Name, Name) -> Q ()) -> Q ()
forall a b. (a -> b) -> a -> b
$ \(Name
conName, Name
newConName) ->
          Q () -> Q ()
addModFinalizer (Q () -> Q ()) -> Q () -> Q ()
forall a b. (a -> b) -> a -> b
$ DocLoc -> String -> Q ()
putDoc (Name -> DocLoc
DeclDoc Name
newConName)
            (String
"Corresponds to '" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
conName String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"'.")
        Con -> Q Con
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Name] -> [BangType] -> Type -> Con
GadtC [Name]
newConNames ((BangType -> BangType) -> [BangType] -> [BangType]
forall a b. (a -> b) -> [a] -> [b]
map ((Type -> Type) -> BangType -> BangType
forall a b. (a -> b) -> (Bang, a) -> (Bang, b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Type -> Type
goType) [BangType]
argTypes) (Type -> Type
goType Type
retType))
      NormalC Name
conName [BangType]
types -> Con -> Q Con
go ([Name] -> [BangType] -> Type -> Con
GadtC [Name
conName] [BangType]
types Type
rawRetType)
      RecC Name
conName [VarBangType]
types -> Con -> Q Con
go (Name -> [BangType] -> Con
NormalC Name
conName ((VarBangType -> BangType) -> [VarBangType] -> [BangType]
forall a b. (a -> b) -> [a] -> [b]
map VarBangType -> BangType
removeName [VarBangType]
types))
      InfixC BangType
l Name
conName BangType
r -> Con -> Q Con
go ([Name] -> [BangType] -> Type -> Con
GadtC [Name
conName] [BangType
l, BangType
r] Type
rawRetType)
      ForallC [TyVarBndr Specificity]
params [Type]
ctx Con
con -> [TyVarBndr Specificity] -> [Type] -> Con -> Con
ForallC [TyVarBndr Specificity]
params [Type]
ctx (Con -> Con) -> Q Con -> Q Con
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Con -> Q Con
go Con
con
      RecGadtC [Name]
conNames [VarBangType]
argTypes Type
retType -> Con -> Q Con
go ([Name] -> [BangType] -> Type -> Con
GadtC [Name]
conNames ((VarBangType -> BangType) -> [VarBangType] -> [BangType]
forall a b. (a -> b) -> [a] -> [b]
map VarBangType -> BangType
removeName [VarBangType]
argTypes) Type
retType)

toFreeFoilSigCon :: FreeFoilConfig -> FreeFoilTermConfig -> Name -> Type -> Type -> Type -> Con -> Q (Maybe Con)
toFreeFoilSigCon :: FreeFoilConfig
-> FreeFoilTermConfig
-> Name
-> Type
-> Type
-> Type
-> Con
-> Q (Maybe Con)
toFreeFoilSigCon FreeFoilConfig
config FreeFoilTermConfig{[Name]
Name
rawIdentName :: FreeFoilTermConfig -> Name
rawTermName :: FreeFoilTermConfig -> Name
rawBindingName :: FreeFoilTermConfig -> Name
rawScopeName :: FreeFoilTermConfig -> Name
rawVarConName :: FreeFoilTermConfig -> Name
rawSubTermNames :: FreeFoilTermConfig -> [Name]
rawSubScopeNames :: FreeFoilTermConfig -> [Name]
intToRawIdentName :: FreeFoilTermConfig -> Name
rawVarIdentToTermName :: FreeFoilTermConfig -> Name
rawTermToScopeName :: FreeFoilTermConfig -> Name
rawScopeToTermName :: FreeFoilTermConfig -> Name
rawIdentName :: Name
rawTermName :: Name
rawBindingName :: Name
rawScopeName :: Name
rawVarConName :: Name
rawSubTermNames :: [Name]
rawSubScopeNames :: [Name]
intToRawIdentName :: Name
rawVarIdentToTermName :: Name
rawTermToScopeName :: Name
rawScopeToTermName :: Name
..} Name
sigName Type
rawRetType Type
scope Type
term = Con -> Q (Maybe Con)
go
  where
    goType :: Type -> Maybe Type
goType = Sort -> FreeFoilConfig -> Type -> Type -> Type -> Maybe Type
toFreeFoilSigType Sort
SortTerm FreeFoilConfig
config Type
scope Type
term
    go :: Con -> Q (Maybe Con)
go = \case
      GadtC [Name]
conNames [BangType]
argTypes Type
retType
        | [Name] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Name]
newConNames -> Maybe Con -> Q (Maybe Con)
forall a. a -> Q a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe Con
forall a. Maybe a
Nothing
        | Bool
otherwise -> do
            [(Name, Name)] -> ((Name, Name) -> Q ()) -> Q ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ ([Name] -> [Name] -> [(Name, Name)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Name]
conNames [Name]
newConNames) (((Name, Name) -> Q ()) -> Q ()) -> ((Name, Name) -> Q ()) -> Q ()
forall a b. (a -> b) -> a -> b
$ \(Name
conName, Name
newConName) ->
              Q () -> Q ()
addModFinalizer (Q () -> Q ()) -> Q () -> Q ()
forall a b. (a -> b) -> a -> b
$ DocLoc -> String -> Q ()
putDoc (Name -> DocLoc
DeclDoc Name
newConName)
                (String
"Corresponds to '" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
conName String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"'.")
            Maybe Con -> Q (Maybe Con)
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return (Con -> Maybe Con
forall a. a -> Maybe a
Just ([Name] -> [BangType] -> Type -> Con
GadtC [Name]
newConNames [BangType]
newArgTypes Type
theRetType))
        where
          newArgTypes :: [BangType]
newArgTypes = (BangType -> Maybe BangType) -> [BangType] -> [BangType]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe ((Type -> Maybe Type) -> BangType -> Maybe BangType
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> (Bang, a) -> f (Bang, b)
traverse Type -> Maybe Type
goType) [BangType]
argTypes
          newConNames :: [Name]
newConNames =
            [ FreeFoilConfig -> Name -> Name
toSignatureName FreeFoilConfig
config Name
rawConName
            | Name
rawConName <- [Name]
conNames
            , Name
rawConName Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
/= Name
rawVarConName ]
          theRetType :: Type
theRetType =
            case Type
retType of
              PeelConT Name
_rawTypeName ((Type -> Maybe Type) -> [Type] -> Maybe [Type]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Type -> Maybe Type
goType -> Just [Type]
params) ->
                Name -> [Type] -> Type
PeelConT Name
sigName ([Type]
params [Type] -> [Type] -> [Type]
forall a. [a] -> [a] -> [a]
++ [Type
scope, Type
term])
              Type
_ -> String -> Type
forall a. HasCallStack => String -> a
error String
"unexpected return type!"
      NormalC Name
conName [BangType]
types -> Con -> Q (Maybe Con)
go ([Name] -> [BangType] -> Type -> Con
GadtC [Name
conName] [BangType]
types Type
rawRetType)
      RecC Name
conName [VarBangType]
types -> Con -> Q (Maybe Con)
go (Name -> [BangType] -> Con
NormalC Name
conName ((VarBangType -> BangType) -> [VarBangType] -> [BangType]
forall a b. (a -> b) -> [a] -> [b]
map VarBangType -> BangType
removeName [VarBangType]
types))
      InfixC BangType
l Name
conName BangType
r -> Con -> Q (Maybe Con)
go ([Name] -> [BangType] -> Type -> Con
GadtC [Name
conName] [BangType
l, BangType
r] Type
rawRetType)
      ForallC [TyVarBndr Specificity]
params [Type]
ctx Con
con -> (Con -> Con) -> Maybe Con -> Maybe Con
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([TyVarBndr Specificity] -> [Type] -> Con -> Con
ForallC [TyVarBndr Specificity]
params [Type]
ctx) (Maybe Con -> Maybe Con) -> Q (Maybe Con) -> Q (Maybe Con)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Con -> Q (Maybe Con)
go Con
con
      RecGadtC [Name]
conNames [VarBangType]
argTypes Type
retType -> Con -> Q (Maybe Con)
go ([Name] -> [BangType] -> Type -> Con
GadtC [Name]
conNames ((VarBangType -> BangType) -> [VarBangType] -> [BangType]
forall a b. (a -> b) -> [a] -> [b]
map VarBangType -> BangType
removeName [VarBangType]
argTypes) Type
retType)

toFreeFoilBindingCon :: FreeFoilConfig -> Type -> Type -> Con -> Q Con
toFreeFoilBindingCon :: FreeFoilConfig -> Type -> Type -> Con -> Q Con
toFreeFoilBindingCon FreeFoilConfig
config Type
rawRetType Type
theOuterScope = Con -> Q Con
go
  where
    goType :: Type -> Type -> Type
goType = Sort -> FreeFoilConfig -> Type -> Type -> Type -> Type
toFreeFoilType Sort
SortBinder FreeFoilConfig
config Type
theOuterScope

    goTypeArgs :: Int -> Type -> [BangType] -> Q (Type, [BangType])
    goTypeArgs :: Int -> Type -> [BangType] -> Q (Type, [BangType])
goTypeArgs Int
_ Type
outerScope [] = (Type, [BangType]) -> Q (Type, [BangType])
forall a. a -> Q a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Type
outerScope, [])
    goTypeArgs Int
i Type
outerScope ((Bang
bang_, Type
rawArgType) : [BangType]
rawArgs) = do
      case Type
rawArgType of
        PeelConT Name
rawTypeName [Type]
_rawTypeParams
          | Name
rawTypeName Name -> [Name] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` (FreeFoilTermConfig -> Name) -> [FreeFoilTermConfig] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map FreeFoilTermConfig -> Name
rawIdentName (FreeFoilConfig -> [FreeFoilTermConfig]
freeFoilTermConfigs FreeFoilConfig
config) -> do
            innerScope <- Name -> Type
VarT (Name -> Type) -> Q Name -> Q Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName (String
"i" String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Int -> String
forall a. Show a => a -> String
show Int
i)
            let argType = Sort -> FreeFoilConfig -> Type -> Type -> Type -> Type
toFreeFoilType Sort
SortBinder FreeFoilConfig
config Type
outerScope Type
innerScope Type
rawArgType
            (theInnerScope, argTypes) <- goTypeArgs (i + 1) innerScope rawArgs
            return (theInnerScope, ((bang_, argType) : argTypes))

          | Just FreeFoilTermConfig
_ <- Name -> [FreeFoilTermConfig] -> Maybe FreeFoilTermConfig
lookupBindingName Name
rawTypeName (FreeFoilConfig -> [FreeFoilTermConfig]
freeFoilTermConfigs FreeFoilConfig
config) -> do
            innerScope <- Name -> Type
VarT (Name -> Type) -> Q Name -> Q Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName (String
"i" String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Int -> String
forall a. Show a => a -> String
show Int
i)
            let argType = Sort -> FreeFoilConfig -> Type -> Type -> Type -> Type
toFreeFoilType Sort
SortBinder FreeFoilConfig
config Type
outerScope Type
innerScope Type
rawArgType
            (theInnerScope, argTypes) <- goTypeArgs (i + 1) innerScope rawArgs
            return (theInnerScope, ((bang_, argType) : argTypes))

        Type
_ -> do
          let argType :: Type
argType = Sort -> FreeFoilConfig -> Type -> Type -> Type -> Type
toFreeFoilType Sort
SortBinder FreeFoilConfig
config Type
outerScope Type
outerScope Type
rawArgType
          (theInnerScope, argTypes) <- Int -> Type -> [BangType] -> Q (Type, [BangType])
goTypeArgs (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) Type
outerScope [BangType]
rawArgs
          return (theInnerScope, ((bang_, argType) : argTypes))

    go :: Con -> Q Con
    go :: Con -> Q Con
go = \case
      GadtC [Name]
conNames [BangType]
argTypes Type
retType -> do
        (theInnerScope, newArgs) <- Int -> Type -> [BangType] -> Q (Type, [BangType])
goTypeArgs Int
0 Type
theOuterScope [BangType]
argTypes
        let newConNames = (Name -> Name) -> [Name] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (FreeFoilConfig -> Name -> Name
toConName FreeFoilConfig
config) [Name]
conNames
        forM_ (zip conNames newConNames) $ \(Name
conName, Name
newConName) ->
          Q () -> Q ()
addModFinalizer (Q () -> Q ()) -> Q () -> Q ()
forall a b. (a -> b) -> a -> b
$ DocLoc -> String -> Q ()
putDoc (Name -> DocLoc
DeclDoc Name
newConName)
            (String
"Corresponds to '" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
conName String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"'.")
        return (GadtC newConNames newArgs (goType theInnerScope retType))
      NormalC Name
conName [BangType]
types -> Con -> Q Con
go ([Name] -> [BangType] -> Type -> Con
GadtC [Name
conName] [BangType]
types Type
rawRetType)
      RecC Name
conName [VarBangType]
types -> Con -> Q Con
go (Name -> [BangType] -> Con
NormalC Name
conName ((VarBangType -> BangType) -> [VarBangType] -> [BangType]
forall a b. (a -> b) -> [a] -> [b]
map VarBangType -> BangType
removeName [VarBangType]
types))
      InfixC BangType
l Name
conName BangType
r -> Con -> Q Con
go ([Name] -> [BangType] -> Type -> Con
GadtC [Name
conName] [BangType
l, BangType
r] Type
rawRetType)
      ForallC [TyVarBndr Specificity]
params [Type]
ctx Con
con -> [TyVarBndr Specificity] -> [Type] -> Con -> Con
ForallC [TyVarBndr Specificity]
params [Type]
ctx (Con -> Con) -> Q Con -> Q Con
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Con -> Q Con
go Con
con
      RecGadtC [Name]
conNames [VarBangType]
argTypes Type
retType -> Con -> Q Con
go ([Name] -> [BangType] -> Type -> Con
GadtC [Name]
conNames ((VarBangType -> BangType) -> [VarBangType] -> [BangType]
forall a b. (a -> b) -> [a] -> [b]
map VarBangType -> BangType
removeName [VarBangType]
argTypes) Type
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 -> Type -> Bool
isBindingField FreeFoilConfig{[Name]
[FreeFoilTermConfig]
String -> String
rawQuantifiedNames :: FreeFoilConfig -> [Name]
freeFoilTermConfigs :: FreeFoilConfig -> [FreeFoilTermConfig]
freeFoilNameModifier :: FreeFoilConfig -> String -> String
freeFoilScopeNameModifier :: FreeFoilConfig -> String -> String
signatureNameModifier :: FreeFoilConfig -> String -> String
freeFoilConNameModifier :: FreeFoilConfig -> String -> String
freeFoilConvertToName :: FreeFoilConfig -> String -> String
freeFoilConvertFromName :: FreeFoilConfig -> String -> String
rawQuantifiedNames :: [Name]
freeFoilTermConfigs :: [FreeFoilTermConfig]
freeFoilNameModifier :: String -> String
freeFoilScopeNameModifier :: String -> String
signatureNameModifier :: String -> String
freeFoilConNameModifier :: String -> String
freeFoilConvertToName :: String -> String
freeFoilConvertFromName :: String -> String
..} = \case
  PeelConT Name
typeName [Type]
_ | Just FreeFoilTermConfig
_ <- Name -> [FreeFoilTermConfig] -> Maybe FreeFoilTermConfig
lookupBindingName Name
typeName [FreeFoilTermConfig]
freeFoilTermConfigs -> Bool
True
  Type
_ -> Bool
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 -> Type -> Bool
isScopeField FreeFoilConfig{[Name]
[FreeFoilTermConfig]
String -> String
rawQuantifiedNames :: FreeFoilConfig -> [Name]
freeFoilTermConfigs :: FreeFoilConfig -> [FreeFoilTermConfig]
freeFoilNameModifier :: FreeFoilConfig -> String -> String
freeFoilScopeNameModifier :: FreeFoilConfig -> String -> String
signatureNameModifier :: FreeFoilConfig -> String -> String
freeFoilConNameModifier :: FreeFoilConfig -> String -> String
freeFoilConvertToName :: FreeFoilConfig -> String -> String
freeFoilConvertFromName :: FreeFoilConfig -> String -> String
rawQuantifiedNames :: [Name]
freeFoilTermConfigs :: [FreeFoilTermConfig]
freeFoilNameModifier :: String -> String
freeFoilScopeNameModifier :: String -> String
signatureNameModifier :: String -> String
freeFoilConNameModifier :: String -> String
freeFoilConvertToName :: String -> String
freeFoilConvertFromName :: String -> String
..} = \case
  PeelConT Name
typeName [Type]
_ | Just FreeFoilTermConfig
_ <- Name -> [FreeFoilTermConfig] -> Maybe FreeFoilTermConfig
lookupScopeName Name
typeName [FreeFoilTermConfig]
freeFoilTermConfigs -> Bool
True
  Type
_ -> Bool
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 (BindingFieldSort -> BindingFieldSort -> Bool
(BindingFieldSort -> BindingFieldSort -> Bool)
-> (BindingFieldSort -> BindingFieldSort -> Bool)
-> Eq BindingFieldSort
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: BindingFieldSort -> BindingFieldSort -> Bool
== :: BindingFieldSort -> BindingFieldSort -> Bool
$c/= :: BindingFieldSort -> BindingFieldSort -> Bool
/= :: BindingFieldSort -> BindingFieldSort -> Bool
Eq)

bindingFieldSortOf :: FreeFoilConfig -> Type -> BindingFieldSort
bindingFieldSortOf :: FreeFoilConfig -> Type -> BindingFieldSort
bindingFieldSortOf FreeFoilConfig{[Name]
[FreeFoilTermConfig]
String -> String
rawQuantifiedNames :: FreeFoilConfig -> [Name]
freeFoilTermConfigs :: FreeFoilConfig -> [FreeFoilTermConfig]
freeFoilNameModifier :: FreeFoilConfig -> String -> String
freeFoilScopeNameModifier :: FreeFoilConfig -> String -> String
signatureNameModifier :: FreeFoilConfig -> String -> String
freeFoilConNameModifier :: FreeFoilConfig -> String -> String
freeFoilConvertToName :: FreeFoilConfig -> String -> String
freeFoilConvertFromName :: FreeFoilConfig -> String -> String
rawQuantifiedNames :: [Name]
freeFoilTermConfigs :: [FreeFoilTermConfig]
freeFoilNameModifier :: String -> String
freeFoilScopeNameModifier :: String -> String
signatureNameModifier :: String -> String
freeFoilConNameModifier :: String -> String
freeFoilConvertToName :: String -> String
freeFoilConvertFromName :: String -> String
..} = \case
  PeelConT Name
typeName [Type]
_typeParams
    | Name
typeName Name -> [Name] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` (FreeFoilTermConfig -> Name) -> [FreeFoilTermConfig] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map FreeFoilTermConfig -> Name
rawIdentName [FreeFoilTermConfig]
freeFoilTermConfigs -> BindingFieldSort
FieldBinder
    | Just FreeFoilTermConfig
_ <- Name -> [FreeFoilTermConfig] -> Maybe FreeFoilTermConfig
lookupBindingName Name
typeName [FreeFoilTermConfig]
freeFoilTermConfigs -> BindingFieldSort
FieldPattern
  Type
_ -> BindingFieldSort
FieldPayload

-- | Does this field introduce binders (and so thread the scope)?
isBindingFieldSort :: BindingFieldSort -> Bool
isBindingFieldSort :: BindingFieldSort -> Bool
isBindingFieldSort = \case
  BindingFieldSort
FieldPayload -> Bool
False
  BindingFieldSort
_ -> Bool
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 -> Type -> Bool
mentionsScopeIndexed FreeFoilConfig{[Name]
[FreeFoilTermConfig]
String -> String
rawQuantifiedNames :: FreeFoilConfig -> [Name]
freeFoilTermConfigs :: FreeFoilConfig -> [FreeFoilTermConfig]
freeFoilNameModifier :: FreeFoilConfig -> String -> String
freeFoilScopeNameModifier :: FreeFoilConfig -> String -> String
signatureNameModifier :: FreeFoilConfig -> String -> String
freeFoilConNameModifier :: FreeFoilConfig -> String -> String
freeFoilConvertToName :: FreeFoilConfig -> String -> String
freeFoilConvertFromName :: FreeFoilConfig -> String -> String
rawQuantifiedNames :: [Name]
freeFoilTermConfigs :: [FreeFoilTermConfig]
freeFoilNameModifier :: String -> String
freeFoilScopeNameModifier :: String -> String
signatureNameModifier :: String -> String
freeFoilConNameModifier :: String -> String
freeFoilConvertToName :: String -> String
freeFoilConvertFromName :: String -> String
..} = Type -> Bool
go
  where
    isIndexedName :: Name -> Bool
isIndexedName Name
typeName = [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
or
      [ Name
typeName Name -> [Name] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
rawQuantifiedNames
      , Name
typeName Name -> [Name] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` (FreeFoilTermConfig -> Name) -> [FreeFoilTermConfig] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map FreeFoilTermConfig -> Name
rawIdentName [FreeFoilTermConfig]
freeFoilTermConfigs
      , Maybe FreeFoilTermConfig -> Bool
forall a. Maybe a -> Bool
isJust (Name -> [FreeFoilTermConfig] -> Maybe FreeFoilTermConfig
lookupTermName Name
typeName [FreeFoilTermConfig]
freeFoilTermConfigs)
      , Maybe FreeFoilTermConfig -> Bool
forall a. Maybe a -> Bool
isJust (Name -> [FreeFoilTermConfig] -> Maybe FreeFoilTermConfig
lookupSubTermName Name
typeName [FreeFoilTermConfig]
freeFoilTermConfigs)
      , Maybe FreeFoilTermConfig -> Bool
forall a. Maybe a -> Bool
isJust (Name -> [FreeFoilTermConfig] -> Maybe FreeFoilTermConfig
lookupScopeName Name
typeName [FreeFoilTermConfig]
freeFoilTermConfigs)
      , Maybe FreeFoilTermConfig -> Bool
forall a. Maybe a -> Bool
isJust (Name -> [FreeFoilTermConfig] -> Maybe FreeFoilTermConfig
lookupSubScopeName Name
typeName [FreeFoilTermConfig]
freeFoilTermConfigs)
      , Maybe FreeFoilTermConfig -> Bool
forall a. Maybe a -> Bool
isJust (Name -> [FreeFoilTermConfig] -> Maybe FreeFoilTermConfig
lookupBindingName Name
typeName [FreeFoilTermConfig]
freeFoilTermConfigs)
      ]
    go :: Type -> Bool
go = \case
      PeelConT Name
typeName [Type]
typeParams -> Name -> Bool
isIndexedName Name
typeName Bool -> Bool -> Bool
|| (Type -> Bool) -> [Type] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Type -> Bool
go [Type]
typeParams
      AppT Type
f Type
x -> Type -> Bool
go Type
f Bool -> Bool -> Bool
|| Type -> Bool
go Type
x
      SigT Type
t Type
_ -> Type -> Bool
go Type
t
      ParensT Type
t -> Type -> Bool
go Type
t
      Type
_ -> Bool
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 :: [Con] -> [(Name, [Type])]
flattenCons = (Con -> [(Name, [Type])]) -> [Con] -> [(Name, [Type])]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Con -> [(Name, [Type])]
go
  where
    go :: Con -> [(Name, [Type])]
go = \case
      NormalC Name
name [BangType]
types -> [(Name
name, (BangType -> Type) -> [BangType] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map BangType -> Type
forall a b. (a, b) -> b
snd [BangType]
types)]
      RecC Name
name [VarBangType]
types -> [(Name
name, (VarBangType -> Type) -> [VarBangType] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (\(Name
_, Bang
_, Type
t) -> Type
t) [VarBangType]
types)]
      InfixC BangType
l Name
name BangType
r -> [(Name
name, [BangType -> Type
forall a b. (a, b) -> b
snd BangType
l, BangType -> Type
forall a b. (a, b) -> b
snd BangType
r])]
      GadtC [Name]
names [BangType]
types Type
_retType -> [ (Name
name, (BangType -> Type) -> [BangType] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map BangType -> Type
forall a b. (a, b) -> b
snd [BangType]
types) | Name
name <- [Name]
names ]
      RecGadtC [Name]
names [VarBangType]
types Type
_retType -> [ (Name
name, (VarBangType -> Type) -> [VarBangType] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (\(Name
_, Bang
_, Type
t) -> Type
t) [VarBangType]
types) | Name
name <- [Name]
names ]
      ForallC [TyVarBndr Specificity]
_ [Type]
_ Con
con -> Con -> [(Name, [Type])]
go Con
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 :: FreeFoilConfig -> (Name, [Type]) -> Q Clause
mkCoSinkabilityProofClause FreeFoilConfig
config (Name
rawConName, [Type]
rawFieldTypes) = do
  let conName :: Name
conName = FreeFoilConfig -> Name -> Name
toConName FreeFoilConfig
config Name
rawConName
      sorts :: [BindingFieldSort]
sorts = (Type -> BindingFieldSort) -> [Type] -> [BindingFieldSort]
forall a b. (a -> b) -> [a] -> [b]
map (FreeFoilConfig -> Type -> BindingFieldSort
bindingFieldSortOf FreeFoilConfig
config) [Type]
rawFieldTypes
      -- Underscore-prefix the binders the clause will not use, so that the
      -- generated code triggers no -Wunused-matches in the client module.
      hasBinding :: Bool
hasBinding = (BindingFieldSort -> Bool) -> [BindingFieldSort] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any BindingFieldSort -> Bool
isBindingFieldSort [BindingFieldSort]
sorts
  rename <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName (if Bool
hasBinding then String
"rename" else String
"_rename")
  cont <- newName "cont"
  xs <- mapM (\Int
i -> String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName (String
"x" String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Int -> String
forall a. Show a => a -> String
show Int
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 Name
renameCur [] [Exp] -> t Exp
fields =
        Exp -> m Exp
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> Exp
VarE Name
cont Exp -> Exp -> Exp
`AppE` Name -> Exp
VarE Name
renameCur
                  Exp -> Exp -> Exp
`AppE` (Exp -> Exp -> Exp) -> Exp -> t Exp -> Exp
forall b a. (b -> a -> b) -> b -> t a -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Exp -> Exp -> Exp
AppE (Name -> Exp
ConE Name
conName) ([Exp] -> t Exp
fields []))
      go Name
renameCur ((BindingFieldSort
FieldPayload, Name
x) : [(BindingFieldSort, Name)]
rest) [Exp] -> t Exp
fields =
        Name -> [(BindingFieldSort, Name)] -> ([Exp] -> t Exp) -> m Exp
go Name
renameCur [(BindingFieldSort, Name)]
rest ([Exp] -> t Exp
fields ([Exp] -> t Exp) -> ([Exp] -> [Exp]) -> [Exp] -> t Exp
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name -> Exp
VarE Name
x Exp -> [Exp] -> [Exp]
forall a. a -> [a] -> [a]
:))
      go Name
renameCur ((BindingFieldSort
_, Name
x) : [(BindingFieldSort, Name)]
rest) [Exp] -> t Exp
fields = do
        x' <- String -> m Name
forall (m :: * -> *). Quote m => String -> m Name
newName (Name -> String
nameBase Name
x String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
"'")
        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 :: FreeFoilConfig -> (Name, [Type]) -> Q Clause
mkWithPatternClause FreeFoilConfig
config (Name
rawConName, [Type]
rawFieldTypes) = do
  let conName :: Name
conName = FreeFoilConfig -> Name -> Name
toConName FreeFoilConfig
config Name
rawConName
      sorts :: [BindingFieldSort]
sorts = (Type -> BindingFieldSort) -> [Type] -> [BindingFieldSort]
forall a b. (a -> b) -> [a] -> [b]
map (FreeFoilConfig -> Type -> BindingFieldSort
bindingFieldSortOf FreeFoilConfig
config) [Type]
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 :: Int
nBinding = [BindingFieldSort] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ((BindingFieldSort -> Bool)
-> [BindingFieldSort] -> [BindingFieldSort]
forall a. (a -> Bool) -> [a] -> [a]
filter BindingFieldSort -> Bool
isBindingFieldSort [BindingFieldSort]
sorts)
      hasNested :: Bool
hasNested = BindingFieldSort
FieldPattern BindingFieldSort -> [BindingFieldSort] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [BindingFieldSort]
sorts
      usedIf :: Bool -> String -> String
usedIf Bool
b String
n = if Bool
b then String
n else Char
'_' Char -> String -> String
forall a. a -> [a] -> [a]
: String
n
  withBinder <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName (Bool -> String -> String
usedIf (Int
nBinding Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0) String
"withBinder")
  unit_ <- newName (usedIf (nBinding == 0 || hasNested) "unit_")
  comp_ <- newName (usedIf (nBinding >= 2 || hasNested) "comp_")
  scope <- newName "scope"
  cont <- newName "cont"
  xs <- mapM (\Int
i -> String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName (String
"x" String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Int -> String
forall a. Show a => a -> String
show Int
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 Name
scopeCur Maybe Exp
acc [] [Exp] -> t Exp
fields =
        Exp -> m Exp
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> Exp
VarE Name
cont Exp -> Exp -> Exp
`AppE` Exp -> Maybe Exp -> Exp
forall a. a -> Maybe a -> a
fromMaybe (Name -> Exp
VarE Name
unit_) Maybe Exp
acc
                  Exp -> Exp -> Exp
`AppE` (Exp -> Exp -> Exp) -> Exp -> t Exp -> Exp
forall b a. (b -> a -> b) -> b -> t a -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Exp -> Exp -> Exp
AppE (Name -> Exp
ConE Name
conName) ([Exp] -> t Exp
fields [])
                  Exp -> Exp -> Exp
`AppE` Name -> Exp
VarE Name
scopeCur)
      go Name
scopeCur Maybe Exp
acc ((BindingFieldSort
FieldPayload, Name
x) : [(BindingFieldSort, Name)]
rest) [Exp] -> t Exp
fields =
        Name
-> Maybe Exp
-> [(BindingFieldSort, Name)]
-> ([Exp] -> t Exp)
-> m Exp
go Name
scopeCur Maybe Exp
acc [(BindingFieldSort, Name)]
rest ([Exp] -> t Exp
fields ([Exp] -> t Exp) -> ([Exp] -> [Exp]) -> [Exp] -> t Exp
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name -> Exp
VarE Name
x Exp -> [Exp] -> [Exp]
forall a. a -> [a] -> [a]
:))
      go Name
scopeCur Maybe Exp
acc ((BindingFieldSort
sort, Name
x) : [(BindingFieldSort, Name)]
rest) [Exp] -> t Exp
fields = do
        x' <- String -> m Name
forall (m :: * -> *). Quote m => String -> m Name
newName (Name -> String
nameBase Name
x String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
"'")
        f <- newName "f"
        scopeNext <- newName "scope'"
        let acc' = case Maybe Exp
acc of
              Maybe Exp
Nothing -> Name -> Exp
VarE Name
f
              Just Exp
a  -> Name -> Exp
VarE Name
comp_ Exp -> Exp -> Exp
`AppE` Exp
a Exp -> Exp -> Exp
`AppE` Name -> Exp
VarE Name
f
        body <- go scopeNext (Just acc') rest (fields . (VarE x' :))
        return $ case sort of
          BindingFieldSort
FieldBinder ->
            Name -> Exp
VarE Name
withBinder Exp -> Exp -> Exp
`AppE` Name -> Exp
VarE Name
scopeCur Exp -> Exp -> Exp
`AppE` Name -> Exp
VarE Name
x
              Exp -> Exp -> Exp
`AppE` [Pat] -> Exp -> Exp
LamE [Name -> Pat
VarP Name
f, Name -> Pat
VarP Name
x']
                  ([Dec] -> Exp -> Exp
LetE [Pat -> Body -> [Dec] -> Dec
ValD (Name -> Pat
VarP Name
scopeNext)
                           (Exp -> Body
NormalB (Name -> Exp
VarE 'Foil.extendScope Exp -> Exp -> Exp
`AppE` Name -> Exp
VarE Name
x' Exp -> Exp -> Exp
`AppE` Name -> Exp
VarE Name
scopeCur)) []]
                     Exp
body)
          BindingFieldSort
_ ->
            Name -> Exp
VarE 'Foil.withPattern Exp -> Exp -> Exp
`AppE` Name -> Exp
VarE Name
withBinder Exp -> Exp -> Exp
`AppE` Name -> Exp
VarE Name
unit_
              Exp -> Exp -> Exp
`AppE` Name -> Exp
VarE Name
comp_ Exp -> Exp -> Exp
`AppE` Name -> Exp
VarE Name
scopeCur Exp -> Exp -> Exp
`AppE` Name -> Exp
VarE Name
x
              Exp -> Exp -> Exp
`AppE` [Pat] -> Exp -> Exp
LamE [Name -> Pat
VarP Name
f, Name -> Pat
VarP Name
x', Name -> Pat
VarP Name
scopeNext] Exp
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 :: Name
-> FreeFoilConfig
-> FreeFoilTermConfig
-> Con
-> Q [([Name], Pat, Pat, [Exp])]
termConToPat Name
rawTypeName config :: FreeFoilConfig
config@FreeFoilConfig{[Name]
[FreeFoilTermConfig]
String -> String
rawQuantifiedNames :: FreeFoilConfig -> [Name]
freeFoilTermConfigs :: FreeFoilConfig -> [FreeFoilTermConfig]
freeFoilNameModifier :: FreeFoilConfig -> String -> String
freeFoilScopeNameModifier :: FreeFoilConfig -> String -> String
signatureNameModifier :: FreeFoilConfig -> String -> String
freeFoilConNameModifier :: FreeFoilConfig -> String -> String
freeFoilConvertToName :: FreeFoilConfig -> String -> String
freeFoilConvertFromName :: FreeFoilConfig -> String -> String
rawQuantifiedNames :: [Name]
freeFoilTermConfigs :: [FreeFoilTermConfig]
freeFoilNameModifier :: String -> String
freeFoilScopeNameModifier :: String -> String
signatureNameModifier :: String -> String
freeFoilConNameModifier :: String -> String
freeFoilConvertToName :: String -> String
freeFoilConvertFromName :: String -> String
..} FreeFoilTermConfig{[Name]
Name
rawIdentName :: FreeFoilTermConfig -> Name
rawTermName :: FreeFoilTermConfig -> Name
rawBindingName :: FreeFoilTermConfig -> Name
rawScopeName :: FreeFoilTermConfig -> Name
rawVarConName :: FreeFoilTermConfig -> Name
rawSubTermNames :: FreeFoilTermConfig -> [Name]
rawSubScopeNames :: FreeFoilTermConfig -> [Name]
intToRawIdentName :: FreeFoilTermConfig -> Name
rawVarIdentToTermName :: FreeFoilTermConfig -> Name
rawTermToScopeName :: FreeFoilTermConfig -> Name
rawScopeToTermName :: FreeFoilTermConfig -> Name
rawIdentName :: Name
rawTermName :: Name
rawBindingName :: Name
rawScopeName :: Name
rawVarConName :: Name
rawSubTermNames :: [Name]
rawSubScopeNames :: [Name]
intToRawIdentName :: Name
rawVarIdentToTermName :: Name
rawTermToScopeName :: Name
rawScopeToTermName :: Name
..} = Con -> Q [([Name], Pat, Pat, [Exp])]
go
  where
    rawRetType :: a
rawRetType = String -> a
forall a. HasCallStack => String -> a
error String
"impossible happened!"

    fromArgType :: Type -> Q ([Name], [Pat], [Pat], [Exp])
    fromArgType :: Type -> Q ([Name], [Pat], [Pat], [Exp])
fromArgType = \case
      PeelConT Name
typeName [Type]
_params
        | Just FreeFoilTermConfig
_ <- Name -> [FreeFoilTermConfig] -> Maybe FreeFoilTermConfig
lookupBindingName Name
typeName [FreeFoilTermConfig]
freeFoilTermConfigs -> do
            ([Name], [Pat], [Pat], [Exp]) -> Q ([Name], [Pat], [Pat], [Exp])
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return ([], [], [], [])
        | Just FreeFoilTermConfig
_ <- Name -> [FreeFoilTermConfig] -> Maybe FreeFoilTermConfig
lookupScopeName Name
typeName [FreeFoilTermConfig]
freeFoilTermConfigs -> do
            binder <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"binder"
            body <- newName "body"
            return ([binder, body], [ConP 'Foil.ScopedAST [] [VarP binder, VarP body]], [TupP [VarP binder, VarP body]], [VarE binder, VarE body])
        | Just FreeFoilTermConfig
_ <- Name -> [FreeFoilTermConfig] -> Maybe FreeFoilTermConfig
lookupSubTermName Name
typeName [FreeFoilTermConfig]
freeFoilTermConfigs -> do
            let rawSigName :: Name
rawSigName = FreeFoilConfig -> Name -> Name
toSignatureName FreeFoilConfig
config Name
typeName
                funName :: Name
funName = FreeFoilConfig -> Name -> Name
toFreeFoilNameFrom FreeFoilConfig
config Name
rawSigName
            x <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"x"
            return ([x], [VarP x], [VarP x], [AppE (VarE funName) (VarE x)])
        | Just FreeFoilTermConfig
_ <- Name -> [FreeFoilTermConfig] -> Maybe FreeFoilTermConfig
lookupSubScopeName Name
typeName [FreeFoilTermConfig]
freeFoilTermConfigs -> do
            let rawSigName :: Name
rawSigName = FreeFoilConfig -> Name -> Name
toSignatureName FreeFoilConfig
config Name
typeName
                funName :: Name
funName = FreeFoilConfig -> Name -> Name
toFreeFoilNameFrom FreeFoilConfig
config Name
rawSigName
            x <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"x"
            return ([x], [VarP x], [VarP x], [AppE (VarE funName) (VarE x)])
        | Name
typeName Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== '[] -> do
            x <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"x"
            return ([x], [VarP x], [VarP x], [ConE 'False])
      AppT Type
_ (PeelConT Name
typeName [Type]
_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 FreeFoilTermConfig
_ <- Name -> [FreeFoilTermConfig] -> Maybe FreeFoilTermConfig
lookupSubTermName Name
typeName [FreeFoilTermConfig]
freeFoilTermConfigs -> do
            let rawSigName :: Name
rawSigName = FreeFoilConfig -> Name -> Name
toSignatureName FreeFoilConfig
config Name
typeName
                funName :: Name
funName = FreeFoilConfig -> Name -> Name
toFreeFoilNameFrom FreeFoilConfig
config Name
rawSigName
            x <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"x"
            return ([x], [VarP x], [VarP x], [AppE (AppE (VarE 'fmap) (VarE funName)) (VarE x)])
        | Just FreeFoilTermConfig
_ <- Name -> [FreeFoilTermConfig] -> Maybe FreeFoilTermConfig
lookupSubScopeName Name
typeName [FreeFoilTermConfig]
freeFoilTermConfigs -> do
            let rawSigName :: Name
rawSigName = FreeFoilConfig -> Name -> Name
toSignatureName FreeFoilConfig
config Name
typeName
                funName :: Name
funName = FreeFoilConfig -> Name -> Name
toFreeFoilNameFrom FreeFoilConfig
config Name
rawSigName
            x <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"x"
            return ([x], [VarP x], [VarP x], [AppE (AppE (VarE 'fmap) (VarE funName)) (VarE x)])
      Type
_ -> do
        x <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"x"
        return ([x], [VarP x], [VarP x], [VarE x])

    go :: Con -> Q [([Name], Pat, Pat, [Exp])]
    go :: Con -> Q [([Name], Pat, Pat, [Exp])]
go = \case
      GadtC [Name]
conNames [BangType]
rawArgTypes Type
_rawRetType -> [[([Name], Pat, Pat, [Exp])]] -> [([Name], Pat, Pat, [Exp])]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[([Name], Pat, Pat, [Exp])]] -> [([Name], Pat, Pat, [Exp])])
-> Q [[([Name], Pat, Pat, [Exp])]] -> Q [([Name], Pat, Pat, [Exp])]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
        [Name]
-> (Name -> Q [([Name], Pat, Pat, [Exp])])
-> Q [[([Name], Pat, Pat, [Exp])]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Name]
conNames ((Name -> Q [([Name], Pat, Pat, [Exp])])
 -> Q [[([Name], Pat, Pat, [Exp])]])
-> (Name -> Q [([Name], Pat, Pat, [Exp])])
-> Q [[([Name], Pat, Pat, [Exp])]]
forall a b. (a -> b) -> a -> b
$ \Name
conName -> do
          let newConName :: Name
newConName = FreeFoilConfig -> Name -> Name
toSignatureName FreeFoilConfig
config Name
conName
          perField <- (BangType -> Q ([Name], [Pat], [Pat], [Exp]))
-> [BangType] -> Q [([Name], [Pat], [Pat], [Exp])]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Type -> Q ([Name], [Pat], [Pat], [Exp])
fromArgType (Type -> Q ([Name], [Pat], [Pat], [Exp]))
-> (BangType -> Type)
-> BangType
-> Q ([Name], [Pat], [Pat], [Exp])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BangType -> Type
forall a b. (a, b) -> b
snd) [BangType]
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 = [Name] -> Maybe Name
forall a. [a] -> Maybe a
listToMaybe
                [ Name
binder
                | (Type
rawArgType, (Name
binder : [Name]
_, [Pat]
_, [Pat]
_, [Exp]
_)) <- [Type]
-> [([Name], [Pat], [Pat], [Exp])]
-> [(Type, ([Name], [Pat], [Pat], [Exp]))]
forall a b. [a] -> [b] -> [(a, b)]
zip ((BangType -> Type) -> [BangType] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map BangType -> Type
forall a b. (a, b) -> b
snd [BangType]
rawArgTypes) [([Name], [Pat], [Pat], [Exp])]
perField
                , FreeFoilConfig -> Type -> Bool
isScopeField FreeFoilConfig
config Type
rawArgType ]
              rawFieldExp Type
rawArgType (a
_, b
_, c
_, [Exp]
fieldExps)
                | FreeFoilConfig -> Type -> Bool
isBindingField FreeFoilConfig
config Type
rawArgType = (Name -> Exp) -> [Name] -> [Exp]
forall a b. (a -> b) -> [a] -> [b]
map Name -> Exp
VarE (Maybe Name -> [Name]
forall a. Maybe a -> [a]
maybeToList Maybe Name
firstScopeBinder)
                | FreeFoilConfig -> Type -> Bool
isScopeField FreeFoilConfig
config Type
rawArgType   = Int -> [Exp] -> [Exp]
forall a. Int -> [a] -> [a]
drop Int
1 [Exp]
fieldExps  -- the body; the binder is not a raw field
                | Bool
otherwise                        = [Exp]
fieldExps
              exps = [[Exp]] -> [Exp]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ((Type -> ([Name], [Pat], [Pat], [Exp]) -> [Exp])
-> [Type] -> [([Name], [Pat], [Pat], [Exp])] -> [[Exp]]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Type -> ([Name], [Pat], [Pat], [Exp]) -> [Exp]
forall {a} {b} {c}. Type -> (a, b, c, [Exp]) -> [Exp]
rawFieldExp ((BangType -> Type) -> [BangType] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map BangType -> Type
forall a b. (a, b) -> b
snd [BangType]
rawArgTypes) [([Name], [Pat], [Pat], [Exp])]
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 = Bool -> [(Type, ([Name], [Pat], [Pat], [Exp]))] -> [Pat]
forall {a} {b} {d}. Bool -> [(Type, (a, b, [Pat], d))] -> [Pat]
goSigPats Bool
True ([Type]
-> [([Name], [Pat], [Pat], [Exp])]
-> [(Type, ([Name], [Pat], [Pat], [Exp]))]
forall a b. [a] -> [b] -> [(a, b)]
zip ((BangType -> Type) -> [BangType] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map BangType -> Type
forall a b. (a, b) -> b
snd [BangType]
rawArgTypes) [([Name], [Pat], [Pat], [Exp])]
perField)
              goSigPats Bool
_ [] = []
              goSigPats Bool
isFirstScope ((Type
rawArgType, (a
_, b
_, [Pat]
fieldPats, d
_)) : [(Type, (a, b, [Pat], d))]
rest)
                | FreeFoilConfig -> Type -> Bool
isScopeField FreeFoilConfig
config Type
rawArgType =
                    (if Bool
isFirstScope then [Pat]
fieldPats else (Pat -> Pat) -> [Pat] -> [Pat]
forall a b. (a -> b) -> [a] -> [b]
map Pat -> Pat
ignoreBinder [Pat]
fieldPats)
                      [Pat] -> [Pat] -> [Pat]
forall a. [a] -> [a] -> [a]
++ Bool -> [(Type, (a, b, [Pat], d))] -> [Pat]
goSigPats Bool
False [(Type, (a, b, [Pat], d))]
rest
                | Bool
otherwise = [Pat]
fieldPats [Pat] -> [Pat] -> [Pat]
forall a. [a] -> [a] -> [a]
++ Bool -> [(Type, (a, b, [Pat], d))] -> [Pat]
goSigPats Bool
isFirstScope [(Type, (a, b, [Pat], d))]
rest
              ignoreBinder = \case
                TupP [Pat
_binder, Pat
body] -> [Pat] -> Pat
TupP [Pat
WildP, Pat
body]
                Pat
p                    -> Pat
p
              pats' = [Pat]
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 Name
conName [BangType]
types -> Con -> Q [([Name], Pat, Pat, [Exp])]
go ([Name] -> [BangType] -> Type -> Con
GadtC [Name
conName] [BangType]
types Type
forall {a}. a
rawRetType)
      RecC Name
conName [VarBangType]
types -> Con -> Q [([Name], Pat, Pat, [Exp])]
go (Name -> [BangType] -> Con
NormalC Name
conName ((VarBangType -> BangType) -> [VarBangType] -> [BangType]
forall a b. (a -> b) -> [a] -> [b]
map VarBangType -> BangType
removeName [VarBangType]
types))
      InfixC BangType
l Name
conName BangType
r -> Con -> Q [([Name], Pat, Pat, [Exp])]
go ([Name] -> [BangType] -> Type -> Con
GadtC [Name
conName] [BangType
l, BangType
r] Type
forall {a}. a
rawRetType)
      ForallC [TyVarBndr Specificity]
_params [Type]
_ctx Con
con -> Con -> Q [([Name], Pat, Pat, [Exp])]
go Con
con
      RecGadtC [Name]
conNames [VarBangType]
argTypes Type
retType -> Con -> Q [([Name], Pat, Pat, [Exp])]
go ([Name] -> [BangType] -> Type -> Con
GadtC [Name]
conNames ((VarBangType -> BangType) -> [VarBangType] -> [BangType]
forall a b. (a -> b) -> [a] -> [b]
map VarBangType -> BangType
removeName [VarBangType]
argTypes) Type
retType)

termConToPatBinding :: Name -> Name -> FreeFoilConfig -> FreeFoilTermConfig -> Con -> Q [([Name], Pat, Pat, [Exp])]
termConToPatBinding :: Name
-> Name
-> FreeFoilConfig
-> FreeFoilTermConfig
-> Con
-> Q [([Name], Pat, Pat, [Exp])]
termConToPatBinding Name
named Name
rawTypeName config :: FreeFoilConfig
config@FreeFoilConfig{[Name]
[FreeFoilTermConfig]
String -> String
rawQuantifiedNames :: FreeFoilConfig -> [Name]
freeFoilTermConfigs :: FreeFoilConfig -> [FreeFoilTermConfig]
freeFoilNameModifier :: FreeFoilConfig -> String -> String
freeFoilScopeNameModifier :: FreeFoilConfig -> String -> String
signatureNameModifier :: FreeFoilConfig -> String -> String
freeFoilConNameModifier :: FreeFoilConfig -> String -> String
freeFoilConvertToName :: FreeFoilConfig -> String -> String
freeFoilConvertFromName :: FreeFoilConfig -> String -> String
rawQuantifiedNames :: [Name]
freeFoilTermConfigs :: [FreeFoilTermConfig]
freeFoilNameModifier :: String -> String
freeFoilScopeNameModifier :: String -> String
signatureNameModifier :: String -> String
freeFoilConNameModifier :: String -> String
freeFoilConvertToName :: String -> String
freeFoilConvertFromName :: String -> String
..} FreeFoilTermConfig{[Name]
Name
rawIdentName :: FreeFoilTermConfig -> Name
rawTermName :: FreeFoilTermConfig -> Name
rawBindingName :: FreeFoilTermConfig -> Name
rawScopeName :: FreeFoilTermConfig -> Name
rawVarConName :: FreeFoilTermConfig -> Name
rawSubTermNames :: FreeFoilTermConfig -> [Name]
rawSubScopeNames :: FreeFoilTermConfig -> [Name]
intToRawIdentName :: FreeFoilTermConfig -> Name
rawVarIdentToTermName :: FreeFoilTermConfig -> Name
rawTermToScopeName :: FreeFoilTermConfig -> Name
rawScopeToTermName :: FreeFoilTermConfig -> Name
rawIdentName :: Name
rawTermName :: Name
rawBindingName :: Name
rawScopeName :: Name
rawVarConName :: Name
rawSubTermNames :: [Name]
rawSubScopeNames :: [Name]
intToRawIdentName :: Name
rawVarIdentToTermName :: Name
rawTermToScopeName :: Name
rawScopeToTermName :: Name
..} = Con -> Q [([Name], Pat, Pat, [Exp])]
go
  where
    rawRetType :: a
rawRetType = String -> a
forall a. HasCallStack => String -> a
error String
"impossible happened!"

    fromArgType :: Type -> Q ([Name], [Pat], [Pat], [Exp])
    fromArgType :: Type -> Q ([Name], [Pat], [Pat], [Exp])
fromArgType = \case
      PeelConT Name
typeName [Type]
_params
        | Name
typeName Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
rawIdentName -> do
            x <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"x"
            return ([x], [VarP x], [VarP x], [VarE named `AppE` (VarE 'Foil.nameId `AppE` (VarE 'Foil.nameOf `AppE` VarE x))])
        | Just FreeFoilTermConfig
_ <- Name -> [FreeFoilTermConfig] -> Maybe FreeFoilTermConfig
lookupBindingName Name
typeName [FreeFoilTermConfig]
freeFoilTermConfigs -> do
            let funName :: Name
funName = Name -> Name
toNameWith (FreeFoilConfig -> Name -> Name
toFreeFoilNameFrom FreeFoilConfig
config Name
typeName)
            x <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"x"
            return ([x], [VarP x], [VarP x], [VarE funName `AppE` VarE named `AppE` VarE x])
        | Just FreeFoilTermConfig
_ <- Name -> [FreeFoilTermConfig] -> Maybe FreeFoilTermConfig
lookupScopeName Name
typeName [FreeFoilTermConfig]
freeFoilTermConfigs -> do
            binder <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"binder"
            body <- newName "body"
            return ([binder, body], [ConP 'Foil.ScopedAST [] [VarP binder, VarP body]], [TupP [VarP binder, VarP body]], [VarE binder, VarE body])
        | Just FreeFoilTermConfig
_ <- Name -> [FreeFoilTermConfig] -> Maybe FreeFoilTermConfig
lookupSubTermName Name
typeName [FreeFoilTermConfig]
freeFoilTermConfigs -> do
            let rawSigName :: Name
rawSigName = FreeFoilConfig -> Name -> Name
toSignatureName FreeFoilConfig
config Name
typeName
                funName :: Name
funName = FreeFoilConfig -> Name -> Name
toFreeFoilNameFrom FreeFoilConfig
config Name
rawSigName
            x <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"x"
            return ([x], [VarP x], [VarP x], [AppE (VarE funName) (VarE x)])
        | Just FreeFoilTermConfig
_ <- Name -> [FreeFoilTermConfig] -> Maybe FreeFoilTermConfig
lookupSubScopeName Name
typeName [FreeFoilTermConfig]
freeFoilTermConfigs -> do
            let rawSigName :: Name
rawSigName = FreeFoilConfig -> Name -> Name
toSignatureName FreeFoilConfig
config Name
typeName
                funName :: Name
funName = FreeFoilConfig -> Name -> Name
toFreeFoilNameFrom FreeFoilConfig
config Name
rawSigName
            x <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"x"
            return ([x], [VarP x], [VarP x], [AppE (VarE funName) (VarE x)])
      AppT Type
_ (PeelConT Name
typeName [Type]
_params)
        | Just FreeFoilTermConfig
_ <- Name -> [FreeFoilTermConfig] -> Maybe FreeFoilTermConfig
lookupSubTermName Name
typeName [FreeFoilTermConfig]
freeFoilTermConfigs -> do
            let rawSigName :: Name
rawSigName = FreeFoilConfig -> Name -> Name
toSignatureName FreeFoilConfig
config Name
typeName
                funName :: Name
funName = FreeFoilConfig -> Name -> Name
toFreeFoilNameFrom FreeFoilConfig
config Name
rawSigName
            x <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"x"
            return ([x], [VarP x], [VarP x], [AppE (AppE (VarE 'fmap) (VarE funName)) (VarE x)])
        | Just FreeFoilTermConfig
_ <- Name -> [FreeFoilTermConfig] -> Maybe FreeFoilTermConfig
lookupSubScopeName Name
typeName [FreeFoilTermConfig]
freeFoilTermConfigs -> do
            let rawSigName :: Name
rawSigName = FreeFoilConfig -> Name -> Name
toSignatureName FreeFoilConfig
config Name
typeName
                funName :: Name
funName = FreeFoilConfig -> Name -> Name
toFreeFoilNameFrom FreeFoilConfig
config Name
rawSigName
            x <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"x"
            return ([x], [VarP x], [VarP x], [AppE (AppE (VarE 'fmap) (VarE funName)) (VarE x)])
      Type
_ -> do
        x <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"x"
        return ([x], [VarP x], [VarP x], [VarE x])

    go :: Con -> Q [([Name], Pat, Pat, [Exp])]
    go :: Con -> Q [([Name], Pat, Pat, [Exp])]
go = \case
      GadtC [Name]
conNames [BangType]
rawArgTypes Type
_rawRetType -> [[([Name], Pat, Pat, [Exp])]] -> [([Name], Pat, Pat, [Exp])]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[([Name], Pat, Pat, [Exp])]] -> [([Name], Pat, Pat, [Exp])])
-> Q [[([Name], Pat, Pat, [Exp])]] -> Q [([Name], Pat, Pat, [Exp])]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
        [Name]
-> (Name -> Q [([Name], Pat, Pat, [Exp])])
-> Q [[([Name], Pat, Pat, [Exp])]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Name]
conNames ((Name -> Q [([Name], Pat, Pat, [Exp])])
 -> Q [[([Name], Pat, Pat, [Exp])]])
-> (Name -> Q [([Name], Pat, Pat, [Exp])])
-> Q [[([Name], Pat, Pat, [Exp])]]
forall a b. (a -> b) -> a -> b
$ \Name
conName -> do
          let newConName :: Name
newConName = FreeFoilConfig -> Name -> Name
toFreeFoilName FreeFoilConfig
config Name
conName
          (concat -> vars, concat -> pats, concat -> pats', concat -> exps) <- [([Name], [Pat], [Pat], [Exp])]
-> ([[Name]], [[Pat]], [[Pat]], [[Exp]])
forall a b c d. [(a, b, c, d)] -> ([a], [b], [c], [d])
unzip4 ([([Name], [Pat], [Pat], [Exp])]
 -> ([[Name]], [[Pat]], [[Pat]], [[Exp]]))
-> Q [([Name], [Pat], [Pat], [Exp])]
-> Q ([[Name]], [[Pat]], [[Pat]], [[Exp]])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
            (BangType -> Q ([Name], [Pat], [Pat], [Exp]))
-> [BangType] -> Q [([Name], [Pat], [Pat], [Exp])]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Type -> Q ([Name], [Pat], [Pat], [Exp])
fromArgType (Type -> Q ([Name], [Pat], [Pat], [Exp]))
-> (BangType -> Type)
-> BangType
-> Q ([Name], [Pat], [Pat], [Exp])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BangType -> Type
forall a b. (a, b) -> b
snd) [BangType]
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 Name
conName [BangType]
types -> Con -> Q [([Name], Pat, Pat, [Exp])]
go ([Name] -> [BangType] -> Type -> Con
GadtC [Name
conName] [BangType]
types Type
forall {a}. a
rawRetType)
      RecC Name
conName [VarBangType]
types -> Con -> Q [([Name], Pat, Pat, [Exp])]
go (Name -> [BangType] -> Con
NormalC Name
conName ((VarBangType -> BangType) -> [VarBangType] -> [BangType]
forall a b. (a -> b) -> [a] -> [b]
map VarBangType -> BangType
removeName [VarBangType]
types))
      InfixC BangType
l Name
conName BangType
r -> Con -> Q [([Name], Pat, Pat, [Exp])]
go ([Name] -> [BangType] -> Type -> Con
GadtC [Name
conName] [BangType
l, BangType
r] Type
forall {a}. a
rawRetType)
      ForallC [TyVarBndr Specificity]
_params [Type]
_ctx Con
con -> Con -> Q [([Name], Pat, Pat, [Exp])]
go Con
con
      RecGadtC [Name]
conNames [VarBangType]
argTypes Type
retType -> Con -> Q [([Name], Pat, Pat, [Exp])]
go ([Name] -> [BangType] -> Type -> Con
GadtC [Name]
conNames ((VarBangType -> BangType) -> [VarBangType] -> [BangType]
forall a b. (a -> b) -> [a] -> [b]
map VarBangType -> BangType
removeName [VarBangType]
argTypes) Type
retType)

termConToPatQuantified :: FreeFoilConfig -> Con -> Q [([Name], Pat, Pat, [Exp])]
termConToPatQuantified :: FreeFoilConfig -> Con -> Q [([Name], Pat, Pat, [Exp])]
termConToPatQuantified config :: FreeFoilConfig
config@FreeFoilConfig{[Name]
[FreeFoilTermConfig]
String -> String
rawQuantifiedNames :: FreeFoilConfig -> [Name]
freeFoilTermConfigs :: FreeFoilConfig -> [FreeFoilTermConfig]
freeFoilNameModifier :: FreeFoilConfig -> String -> String
freeFoilScopeNameModifier :: FreeFoilConfig -> String -> String
signatureNameModifier :: FreeFoilConfig -> String -> String
freeFoilConNameModifier :: FreeFoilConfig -> String -> String
freeFoilConvertToName :: FreeFoilConfig -> String -> String
freeFoilConvertFromName :: FreeFoilConfig -> String -> String
rawQuantifiedNames :: [Name]
freeFoilTermConfigs :: [FreeFoilTermConfig]
freeFoilNameModifier :: String -> String
freeFoilScopeNameModifier :: String -> String
signatureNameModifier :: String -> String
freeFoilConNameModifier :: String -> String
freeFoilConvertToName :: String -> String
freeFoilConvertFromName :: String -> String
..} = Con -> Q [([Name], Pat, Pat, [Exp])]
go
  where
    rawRetType :: a
rawRetType = String -> a
forall a. HasCallStack => String -> a
error String
"impossible happened!"

    fromArgType :: Type -> Q ([Name], [Pat], [Pat], [Exp])
    fromArgType :: Type -> Q ([Name], [Pat], [Pat], [Exp])
fromArgType = \case
      PeelConT Name
typeName [Type]
_params
        | Just FreeFoilTermConfig
_ <- Name -> [FreeFoilTermConfig] -> Maybe FreeFoilTermConfig
lookupTermName Name
typeName [FreeFoilTermConfig]
freeFoilTermConfigs -> do
            let funName :: Name
funName = FreeFoilConfig -> Name -> Name
toFreeFoilNameFrom FreeFoilConfig
config Name
typeName
            x <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"x"
            return ([x], [VarP x], [VarP x], [VarE funName `AppE` VarE x])
        | Just FreeFoilTermConfig{[Name]
Name
rawIdentName :: FreeFoilTermConfig -> Name
rawTermName :: FreeFoilTermConfig -> Name
rawBindingName :: FreeFoilTermConfig -> Name
rawScopeName :: FreeFoilTermConfig -> Name
rawVarConName :: FreeFoilTermConfig -> Name
rawSubTermNames :: FreeFoilTermConfig -> [Name]
rawSubScopeNames :: FreeFoilTermConfig -> [Name]
intToRawIdentName :: FreeFoilTermConfig -> Name
rawVarIdentToTermName :: FreeFoilTermConfig -> Name
rawTermToScopeName :: FreeFoilTermConfig -> Name
rawScopeToTermName :: FreeFoilTermConfig -> Name
rawIdentName :: Name
rawTermName :: Name
rawBindingName :: Name
rawScopeName :: Name
rawVarConName :: Name
rawSubTermNames :: [Name]
rawSubScopeNames :: [Name]
intToRawIdentName :: Name
rawVarIdentToTermName :: Name
rawTermToScopeName :: Name
rawScopeToTermName :: Name
..} <- Name -> [FreeFoilTermConfig] -> Maybe FreeFoilTermConfig
lookupScopeName Name
typeName [FreeFoilTermConfig]
freeFoilTermConfigs -> do
            let funName :: Name
funName = FreeFoilConfig -> Name -> Name
toFreeFoilNameFrom FreeFoilConfig
config Name
rawTermName
            x <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"x"
            return ([x], [VarP x], [VarP x], [VarE rawTermToScopeName `AppE` (VarE funName `AppE` VarE x)])
        | Just FreeFoilTermConfig{[Name]
Name
rawIdentName :: FreeFoilTermConfig -> Name
rawTermName :: FreeFoilTermConfig -> Name
rawBindingName :: FreeFoilTermConfig -> Name
rawScopeName :: FreeFoilTermConfig -> Name
rawVarConName :: FreeFoilTermConfig -> Name
rawSubTermNames :: FreeFoilTermConfig -> [Name]
rawSubScopeNames :: FreeFoilTermConfig -> [Name]
intToRawIdentName :: FreeFoilTermConfig -> Name
rawVarIdentToTermName :: FreeFoilTermConfig -> Name
rawTermToScopeName :: FreeFoilTermConfig -> Name
rawScopeToTermName :: FreeFoilTermConfig -> Name
rawIdentName :: Name
rawTermName :: Name
rawBindingName :: Name
rawScopeName :: Name
rawVarConName :: Name
rawSubTermNames :: [Name]
rawSubScopeNames :: [Name]
intToRawIdentName :: Name
rawVarIdentToTermName :: Name
rawTermToScopeName :: Name
rawScopeToTermName :: Name
..} <- Name -> [FreeFoilTermConfig] -> Maybe FreeFoilTermConfig
lookupIdentName Name
typeName [FreeFoilTermConfig]
freeFoilTermConfigs -> do
            x <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"x"
            return ([x], [VarP x], [VarP x], [VarE intToRawIdentName `AppE` (VarE 'Foil.nameId `AppE` VarE x)])
        | Just FreeFoilTermConfig
_ <- Name -> [FreeFoilTermConfig] -> Maybe FreeFoilTermConfig
lookupBindingName Name
typeName [FreeFoilTermConfig]
freeFoilTermConfigs -> do
            let funName :: Name
funName = FreeFoilConfig -> Name -> Name
toFreeFoilNameFrom FreeFoilConfig
config Name
typeName
            x <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"x"
            return ([x], [VarP x], [VarP x], [VarE funName `AppE` VarE x])
        | Just FreeFoilTermConfig
_ <- Name -> [FreeFoilTermConfig] -> Maybe FreeFoilTermConfig
lookupSubTermName Name
typeName [FreeFoilTermConfig]
freeFoilTermConfigs -> do
            let rawSigName :: Name
rawSigName = FreeFoilConfig -> Name -> Name
toSignatureName FreeFoilConfig
config Name
typeName
                funName :: Name
funName = FreeFoilConfig -> Name -> Name
toFreeFoilNameFrom FreeFoilConfig
config Name
rawSigName
            x <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"x"
            return ([x], [VarP x], [VarP x], [AppE (VarE funName) (VarE x)])
        | Just FreeFoilTermConfig
_ <- Name -> [FreeFoilTermConfig] -> Maybe FreeFoilTermConfig
lookupSubScopeName Name
typeName [FreeFoilTermConfig]
freeFoilTermConfigs -> do
            let rawSigName :: Name
rawSigName = FreeFoilConfig -> Name -> Name
toSignatureName FreeFoilConfig
config Name
typeName
                funName :: Name
funName = FreeFoilConfig -> Name -> Name
toFreeFoilNameFrom FreeFoilConfig
config Name
rawSigName
            x <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"x"
            return ([x], [VarP x], [VarP x], [AppE (VarE funName) (VarE x)])
      AppT Type
_ (PeelConT Name
typeName [Type]
_params)
        | Just FreeFoilTermConfig
_ <- Name -> [FreeFoilTermConfig] -> Maybe FreeFoilTermConfig
lookupSubTermName Name
typeName [FreeFoilTermConfig]
freeFoilTermConfigs -> do
            let funName :: Name
funName = FreeFoilConfig -> Name -> Name
toFreeFoilNameFrom FreeFoilConfig
config Name
typeName
            x <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"x"
            return ([x], [VarP x], [VarP x], [AppE (AppE (VarE 'fmap) (VarE funName)) (VarE x)])
        | Just FreeFoilTermConfig
_ <- Name -> [FreeFoilTermConfig] -> Maybe FreeFoilTermConfig
lookupSubScopeName Name
typeName [FreeFoilTermConfig]
freeFoilTermConfigs -> do
            let funName :: Name
funName = FreeFoilConfig -> Name -> Name
toFreeFoilNameFrom FreeFoilConfig
config Name
typeName
            x <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"x"
            return ([x], [VarP x], [VarP x], [AppE (AppE (VarE 'fmap) (VarE funName)) (VarE x)])
        | Just FreeFoilTermConfig
_ <- Name -> [FreeFoilTermConfig] -> Maybe FreeFoilTermConfig
lookupTermName Name
typeName [FreeFoilTermConfig]
freeFoilTermConfigs -> do
            let funName :: Name
funName = FreeFoilConfig -> Name -> Name
toFreeFoilNameFrom FreeFoilConfig
config Name
typeName
            x <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"x"
            return ([x], [VarP x], [VarP x], [AppE (AppE (VarE 'fmap) (VarE funName)) (VarE x)])
      Type
_ -> do
        x <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"x"
        return ([x], [VarP x], [VarP x], [VarE x])

    go :: Con -> Q [([Name], Pat, Pat, [Exp])]
    go :: Con -> Q [([Name], Pat, Pat, [Exp])]
go = \case
      GadtC [Name]
conNames [BangType]
rawArgTypes Type
_rawRetType -> [[([Name], Pat, Pat, [Exp])]] -> [([Name], Pat, Pat, [Exp])]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[([Name], Pat, Pat, [Exp])]] -> [([Name], Pat, Pat, [Exp])])
-> Q [[([Name], Pat, Pat, [Exp])]] -> Q [([Name], Pat, Pat, [Exp])]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
        [Name]
-> (Name -> Q [([Name], Pat, Pat, [Exp])])
-> Q [[([Name], Pat, Pat, [Exp])]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Name]
conNames ((Name -> Q [([Name], Pat, Pat, [Exp])])
 -> Q [[([Name], Pat, Pat, [Exp])]])
-> (Name -> Q [([Name], Pat, Pat, [Exp])])
-> Q [[([Name], Pat, Pat, [Exp])]]
forall a b. (a -> b) -> a -> b
$ \Name
conName -> do
          let newConName :: Name
newConName = FreeFoilConfig -> Name -> Name
toFreeFoilName FreeFoilConfig
config Name
conName
          (concat -> vars, concat -> pats, concat -> pats', concat -> exps) <- [([Name], [Pat], [Pat], [Exp])]
-> ([[Name]], [[Pat]], [[Pat]], [[Exp]])
forall a b c d. [(a, b, c, d)] -> ([a], [b], [c], [d])
unzip4 ([([Name], [Pat], [Pat], [Exp])]
 -> ([[Name]], [[Pat]], [[Pat]], [[Exp]]))
-> Q [([Name], [Pat], [Pat], [Exp])]
-> Q ([[Name]], [[Pat]], [[Pat]], [[Exp]])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
            (BangType -> Q ([Name], [Pat], [Pat], [Exp]))
-> [BangType] -> Q [([Name], [Pat], [Pat], [Exp])]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Type -> Q ([Name], [Pat], [Pat], [Exp])
fromArgType (Type -> Q ([Name], [Pat], [Pat], [Exp]))
-> (BangType -> Type)
-> BangType
-> Q ([Name], [Pat], [Pat], [Exp])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BangType -> Type
forall a b. (a, b) -> b
snd) [BangType]
rawArgTypes
          return [ (vars, ConP newConName [] pats, ConP newConName [] pats', exps) ]
      NormalC Name
conName [BangType]
types -> Con -> Q [([Name], Pat, Pat, [Exp])]
go ([Name] -> [BangType] -> Type -> Con
GadtC [Name
conName] [BangType]
types Type
forall {a}. a
rawRetType)
      RecC Name
conName [VarBangType]
types -> Con -> Q [([Name], Pat, Pat, [Exp])]
go (Name -> [BangType] -> Con
NormalC Name
conName ((VarBangType -> BangType) -> [VarBangType] -> [BangType]
forall a b. (a -> b) -> [a] -> [b]
map VarBangType -> BangType
removeName [VarBangType]
types))
      InfixC BangType
l Name
conName BangType
r -> Con -> Q [([Name], Pat, Pat, [Exp])]
go ([Name] -> [BangType] -> Type -> Con
GadtC [Name
conName] [BangType
l, BangType
r] Type
forall {a}. a
rawRetType)
      ForallC [TyVarBndr Specificity]
_params [Type]
_ctx Con
con -> Con -> Q [([Name], Pat, Pat, [Exp])]
go Con
con
      RecGadtC [Name]
conNames [VarBangType]
argTypes Type
retType -> Con -> Q [([Name], Pat, Pat, [Exp])]
go ([Name] -> [BangType] -> Type -> Con
GadtC [Name]
conNames ((VarBangType -> BangType) -> [VarBangType] -> [BangType]
forall a b. (a -> b) -> [a] -> [b]
map VarBangType -> BangType
removeName [VarBangType]
argTypes) Type
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 :: FreeFoilConfig -> Type -> Type -> [Type] -> [Type]
patternSynonymArgTypes config :: FreeFoilConfig
config@FreeFoilConfig{[Name]
[FreeFoilTermConfig]
String -> String
rawQuantifiedNames :: FreeFoilConfig -> [Name]
freeFoilTermConfigs :: FreeFoilConfig -> [FreeFoilTermConfig]
freeFoilNameModifier :: FreeFoilConfig -> String -> String
freeFoilScopeNameModifier :: FreeFoilConfig -> String -> String
signatureNameModifier :: FreeFoilConfig -> String -> String
freeFoilConNameModifier :: FreeFoilConfig -> String -> String
freeFoilConvertToName :: FreeFoilConfig -> String -> String
freeFoilConvertFromName :: FreeFoilConfig -> String -> String
rawQuantifiedNames :: [Name]
freeFoilTermConfigs :: [FreeFoilTermConfig]
freeFoilNameModifier :: String -> String
freeFoilScopeNameModifier :: String -> String
signatureNameModifier :: String -> String
freeFoilConNameModifier :: String -> String
freeFoilConvertToName :: String -> String
freeFoilConvertFromName :: String -> String
..} Type
outerScope Type
innerScope [Type]
rawArgTypes =
    Int -> [Type] -> [Type]
forall {t}. (Num t, Show t) => t -> [Type] -> [Type]
go (Int
1 :: Int) [Type]
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 :: Int
scopeCount = [Type] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ((Type -> Bool) -> [Type] -> [Type]
forall a. (a -> Bool) -> [a] -> [a]
filter (FreeFoilConfig -> Type -> Bool
isScopeField FreeFoilConfig
config) [Type]
rawArgTypes)
    innerScopeFor :: a -> Type
innerScopeFor a
k
      | Int
scopeCount Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
1 = Type
innerScope
      | Bool
otherwise       = Name -> Type
VarT (String -> Name
mkName (String
"i" String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
k))

    go :: t -> [Type] -> [Type]
go t
_ [] = []
    go t
k (Type
rawArgType : [Type]
rest) = case Type
rawArgType of
      PeelConT Name
typeName [Type]
_params
        -- The binder is an argument of the ScopedAST, not of the node.
        | Just FreeFoilTermConfig
_ <- Name -> [FreeFoilTermConfig] -> Maybe FreeFoilTermConfig
lookupBindingName Name
typeName [FreeFoilTermConfig]
freeFoilTermConfigs -> t -> [Type] -> [Type]
go t
k [Type]
rest
        -- A scoped child: its own binder, then its body, in its own scope.
        | Just FreeFoilTermConfig{[Name]
Name
rawIdentName :: FreeFoilTermConfig -> Name
rawTermName :: FreeFoilTermConfig -> Name
rawBindingName :: FreeFoilTermConfig -> Name
rawScopeName :: FreeFoilTermConfig -> Name
rawVarConName :: FreeFoilTermConfig -> Name
rawSubTermNames :: FreeFoilTermConfig -> [Name]
rawSubScopeNames :: FreeFoilTermConfig -> [Name]
intToRawIdentName :: FreeFoilTermConfig -> Name
rawVarIdentToTermName :: FreeFoilTermConfig -> Name
rawTermToScopeName :: FreeFoilTermConfig -> Name
rawScopeToTermName :: FreeFoilTermConfig -> Name
rawIdentName :: Name
rawTermName :: Name
rawBindingName :: Name
rawScopeName :: Name
rawVarConName :: Name
rawSubTermNames :: [Name]
rawSubScopeNames :: [Name]
intToRawIdentName :: Name
rawVarIdentToTermName :: Name
rawTermToScopeName :: Name
rawScopeToTermName :: Name
..} <- Name -> [FreeFoilTermConfig] -> Maybe FreeFoilTermConfig
lookupScopeName Name
typeName [FreeFoilTermConfig]
freeFoilTermConfigs ->
            let inner :: Type
inner = t -> Type
forall {a}. Show a => a -> Type
innerScopeFor t
k
                rawBindingType :: Type
rawBindingType = Name -> [Type] -> Type
PeelConT Name
rawBindingName (Type -> [Type]
typeParamsOf Type
rawArgType)
             in Sort -> FreeFoilConfig -> Type -> Type -> Type -> Type
toFreeFoilType Sort
SortTerm FreeFoilConfig
config Type
outerScope Type
inner Type
rawBindingType
                  Type -> [Type] -> [Type]
forall a. a -> [a] -> [a]
: Sort -> FreeFoilConfig -> Type -> Type -> Type -> Type
toFreeFoilType Sort
SortTerm FreeFoilConfig
config Type
outerScope Type
inner Type
rawArgType
                  Type -> [Type] -> [Type]
forall a. a -> [a] -> [a]
: t -> [Type] -> [Type]
go (t
k t -> t -> t
forall a. Num a => a -> a -> a
+ t
1) [Type]
rest
      Type
_ -> Sort -> FreeFoilConfig -> Type -> Type -> Type -> Type
toFreeFoilType Sort
SortTerm FreeFoilConfig
config Type
outerScope Type
innerScope Type
rawArgType Type -> [Type] -> [Type]
forall a. a -> [a] -> [a]
: t -> [Type] -> [Type]
go t
k [Type]
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 :: Type -> [Type]
typeParamsOf = \case
      PeelConT Name
_ [Type]
params -> [Type]
params
      Type
_                 -> []

mkPatternSynonym :: Name -> FreeFoilConfig -> FreeFoilTermConfig -> Type -> Con -> Q [(Name, [Dec])]
mkPatternSynonym :: Name
-> FreeFoilConfig
-> FreeFoilTermConfig
-> Type
-> Con
-> Q [(Name, [Dec])]
mkPatternSynonym Name
rawTypeName FreeFoilConfig
config termConfig :: FreeFoilTermConfig
termConfig@FreeFoilTermConfig{[Name]
Name
rawIdentName :: FreeFoilTermConfig -> Name
rawTermName :: FreeFoilTermConfig -> Name
rawBindingName :: FreeFoilTermConfig -> Name
rawScopeName :: FreeFoilTermConfig -> Name
rawVarConName :: FreeFoilTermConfig -> Name
rawSubTermNames :: FreeFoilTermConfig -> [Name]
rawSubScopeNames :: FreeFoilTermConfig -> [Name]
intToRawIdentName :: FreeFoilTermConfig -> Name
rawVarIdentToTermName :: FreeFoilTermConfig -> Name
rawTermToScopeName :: FreeFoilTermConfig -> Name
rawScopeToTermName :: FreeFoilTermConfig -> Name
rawIdentName :: Name
rawTermName :: Name
rawBindingName :: Name
rawScopeName :: Name
rawVarConName :: Name
rawSubTermNames :: [Name]
rawSubScopeNames :: [Name]
intToRawIdentName :: Name
rawVarIdentToTermName :: Name
rawTermToScopeName :: Name
rawScopeToTermName :: Name
..} Type
rawRetType = Con -> Q [(Name, [Dec])]
go
  where
    go :: Con -> Q [(Name, [Dec])]
    go :: Con -> Q [(Name, [Dec])]
go = \case
      GadtC [Name]
conNames [BangType]
rawArgTypes Type
_rawRetType -> [[(Name, [Dec])]] -> [(Name, [Dec])]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[(Name, [Dec])]] -> [(Name, [Dec])])
-> Q [[(Name, [Dec])]] -> Q [(Name, [Dec])]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
        [Name] -> (Name -> Q [(Name, [Dec])]) -> Q [[(Name, [Dec])]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM ([Name]
conNames [Name] -> [Name] -> [Name]
forall a. Eq a => [a] -> [a] -> [a]
\\ [Name
rawVarConName]) ((Name -> Q [(Name, [Dec])]) -> Q [[(Name, [Dec])]])
-> (Name -> Q [(Name, [Dec])]) -> Q [[(Name, [Dec])]]
forall a b. (a -> b) -> a -> b
$ \Name
conName -> do
          let patName :: Name
patName = FreeFoilConfig -> Name -> Name
toConName FreeFoilConfig
config Name
conName
              outerScope :: Type
outerScope = Name -> Type
VarT (String -> Name
mkName String
"o")
              innerScope :: Type
innerScope
                | Name
rawTypeName Name -> [Name] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
rawSubScopeNames = Type
outerScope
                | Bool
otherwise = Name -> Type
VarT (String -> Name
mkName String
"i")
              synType :: Type
synType = (Type -> Type -> Type) -> Type -> [Type] -> Type
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\Type
x Type
y -> Type -> Type -> Type
AppT (Type -> Type -> Type
AppT Type
ArrowT Type
x) Type
y)
                (Sort -> FreeFoilConfig -> Type -> Type -> Type -> Type
toFreeFoilType Sort
SortTerm FreeFoilConfig
config Type
outerScope Type
innerScope Type
rawRetType)
                (FreeFoilConfig -> Type -> Type -> [Type] -> [Type]
patternSynonymArgTypes FreeFoilConfig
config Type
outerScope Type
innerScope ((BangType -> Type) -> [BangType] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map BangType -> Type
forall a b. (a, b) -> b
snd [BangType]
rawArgTypes))
          [(vars, pat, _, _)] <- Name
-> FreeFoilConfig
-> FreeFoilTermConfig
-> Con
-> Q [([Name], Pat, Pat, [Exp])]
termConToPat Name
rawTypeName FreeFoilConfig
config FreeFoilTermConfig
termConfig ([Name] -> [BangType] -> Type -> Con
GadtC [Name
conName] [BangType]
rawArgTypes Type
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 Name
conName [BangType]
types -> Con -> Q [(Name, [Dec])]
go ([Name] -> [BangType] -> Type -> Con
GadtC [Name
conName] [BangType]
types Type
rawRetType)
      RecC Name
conName [VarBangType]
types -> Con -> Q [(Name, [Dec])]
go (Name -> [BangType] -> Con
NormalC Name
conName ((VarBangType -> BangType) -> [VarBangType] -> [BangType]
forall a b. (a -> b) -> [a] -> [b]
map VarBangType -> BangType
removeName [VarBangType]
types))
      InfixC BangType
l Name
conName BangType
r -> Con -> Q [(Name, [Dec])]
go ([Name] -> [BangType] -> Type -> Con
GadtC [Name
conName] [BangType
l, BangType
r] Type
rawRetType)
      ForallC [TyVarBndr Specificity]
_params [Type]
_ctx Con
con -> Con -> Q [(Name, [Dec])]
go Con
con  -- FIXME: params and ctx!
      RecGadtC [Name]
conNames [VarBangType]
argTypes Type
retType -> Con -> Q [(Name, [Dec])]
go ([Name] -> [BangType] -> Type -> Con
GadtC [Name]
conNames ((VarBangType -> BangType) -> [VarBangType] -> [BangType]
forall a b. (a -> b) -> [a] -> [b]
map VarBangType -> BangType
removeName [VarBangType]
argTypes) Type
retType)

toFreeFoilClauseFrom :: Name -> FreeFoilConfig -> FreeFoilTermConfig -> Type -> Con -> Q [Clause]
toFreeFoilClauseFrom :: Name
-> FreeFoilConfig
-> FreeFoilTermConfig
-> Type
-> Con
-> Q [Clause]
toFreeFoilClauseFrom Name
rawTypeName FreeFoilConfig
config termConfig :: FreeFoilTermConfig
termConfig@FreeFoilTermConfig{[Name]
Name
rawIdentName :: FreeFoilTermConfig -> Name
rawTermName :: FreeFoilTermConfig -> Name
rawBindingName :: FreeFoilTermConfig -> Name
rawScopeName :: FreeFoilTermConfig -> Name
rawVarConName :: FreeFoilTermConfig -> Name
rawSubTermNames :: FreeFoilTermConfig -> [Name]
rawSubScopeNames :: FreeFoilTermConfig -> [Name]
intToRawIdentName :: FreeFoilTermConfig -> Name
rawVarIdentToTermName :: FreeFoilTermConfig -> Name
rawTermToScopeName :: FreeFoilTermConfig -> Name
rawScopeToTermName :: FreeFoilTermConfig -> Name
rawIdentName :: Name
rawTermName :: Name
rawBindingName :: Name
rawScopeName :: Name
rawVarConName :: Name
rawSubTermNames :: [Name]
rawSubScopeNames :: [Name]
intToRawIdentName :: Name
rawVarIdentToTermName :: Name
rawTermToScopeName :: Name
rawScopeToTermName :: Name
..} Type
rawRetType = Con -> Q [Clause]
go
  where
    go :: Con -> Q [Clause]
go = \case
      GadtC [Name]
conNames [BangType]
rawArgTypes Type
rawRetType' -> [[Clause]] -> [Clause]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[Clause]] -> [Clause]) -> Q [[Clause]] -> Q [Clause]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
        [Name] -> (Name -> Q [Clause]) -> Q [[Clause]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM ([Name]
conNames [Name] -> [Name] -> [Name]
forall a. Eq a => [a] -> [a] -> [a]
\\ [Name
rawVarConName]) ((Name -> Q [Clause]) -> Q [[Clause]])
-> (Name -> Q [Clause]) -> Q [[Clause]]
forall a b. (a -> b) -> a -> b
$ \Name
conName -> do
          [(_vars, _pat, pat, exps)] <- Name
-> FreeFoilConfig
-> FreeFoilTermConfig
-> Con
-> Q [([Name], Pat, Pat, [Exp])]
termConToPat Name
rawTypeName FreeFoilConfig
config FreeFoilTermConfig
termConfig
            ([Name] -> [BangType] -> Type -> Con
GadtC [Name
conName] [BangType]
rawArgTypes Type
rawRetType')    -- FIXME: unsafe matching!
          return [ Clause [pat] (NormalB (foldl AppE (ConE conName) exps)) [] ]

      NormalC Name
conName [BangType]
types -> Con -> Q [Clause]
go ([Name] -> [BangType] -> Type -> Con
GadtC [Name
conName] [BangType]
types Type
rawRetType)
      RecC Name
conName [VarBangType]
types -> Con -> Q [Clause]
go (Name -> [BangType] -> Con
NormalC Name
conName ((VarBangType -> BangType) -> [VarBangType] -> [BangType]
forall a b. (a -> b) -> [a] -> [b]
map VarBangType -> BangType
removeName [VarBangType]
types))
      InfixC BangType
l Name
conName BangType
r -> Con -> Q [Clause]
go ([Name] -> [BangType] -> Type -> Con
GadtC [Name
conName] [BangType
l, BangType
r] Type
rawRetType)
      ForallC [TyVarBndr Specificity]
_params [Type]
_ctx Con
con -> Con -> Q [Clause]
go Con
con
      RecGadtC [Name]
conNames [VarBangType]
argTypes Type
retType -> Con -> Q [Clause]
go ([Name] -> [BangType] -> Type -> Con
GadtC [Name]
conNames ((VarBangType -> BangType) -> [VarBangType] -> [BangType]
forall a b. (a -> b) -> [a] -> [b]
map VarBangType -> BangType
removeName [VarBangType]
argTypes) Type
retType)

toFreeFoilClauseFromBinding :: Name -> FreeFoilConfig -> FreeFoilTermConfig -> Type -> Con -> Q [Clause]
toFreeFoilClauseFromBinding :: Name
-> FreeFoilConfig
-> FreeFoilTermConfig
-> Type
-> Con
-> Q [Clause]
toFreeFoilClauseFromBinding Name
named FreeFoilConfig
config termConfig :: FreeFoilTermConfig
termConfig@FreeFoilTermConfig{[Name]
Name
rawIdentName :: FreeFoilTermConfig -> Name
rawTermName :: FreeFoilTermConfig -> Name
rawBindingName :: FreeFoilTermConfig -> Name
rawScopeName :: FreeFoilTermConfig -> Name
rawVarConName :: FreeFoilTermConfig -> Name
rawSubTermNames :: FreeFoilTermConfig -> [Name]
rawSubScopeNames :: FreeFoilTermConfig -> [Name]
intToRawIdentName :: FreeFoilTermConfig -> Name
rawVarIdentToTermName :: FreeFoilTermConfig -> Name
rawTermToScopeName :: FreeFoilTermConfig -> Name
rawScopeToTermName :: FreeFoilTermConfig -> Name
rawIdentName :: Name
rawTermName :: Name
rawBindingName :: Name
rawScopeName :: Name
rawVarConName :: Name
rawSubTermNames :: [Name]
rawSubScopeNames :: [Name]
intToRawIdentName :: Name
rawVarIdentToTermName :: Name
rawTermToScopeName :: Name
rawScopeToTermName :: Name
..} Type
rawRetType = Con -> Q [Clause]
go
  where
    go :: Con -> Q [Clause]
go = \case
      GadtC [Name]
conNames [BangType]
rawArgTypes Type
rawRetType' -> [[Clause]] -> [Clause]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[Clause]] -> [Clause]) -> Q [[Clause]] -> Q [Clause]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
        [Name] -> (Name -> Q [Clause]) -> Q [[Clause]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM ([Name]
conNames [Name] -> [Name] -> [Name]
forall a. Eq a => [a] -> [a] -> [a]
\\ [Name
rawVarConName]) ((Name -> Q [Clause]) -> Q [[Clause]])
-> (Name -> Q [Clause]) -> Q [[Clause]]
forall a b. (a -> b) -> a -> b
$ \Name
conName -> do
          [(_vars, _pat, pat, exps)] <- Name
-> Name
-> FreeFoilConfig
-> FreeFoilTermConfig
-> Con
-> Q [([Name], Pat, Pat, [Exp])]
termConToPatBinding Name
named Name
rawBindingName FreeFoilConfig
config FreeFoilTermConfig
termConfig
            ([Name] -> [BangType] -> Type -> Con
GadtC [Name
conName] [BangType]
rawArgTypes Type
rawRetType')    -- FIXME: unsafe matching!
          return [ Clause [VarP named, pat] (NormalB (foldl AppE (ConE conName) exps)) [] ]

      NormalC Name
conName [BangType]
types -> Con -> Q [Clause]
go ([Name] -> [BangType] -> Type -> Con
GadtC [Name
conName] [BangType]
types Type
rawRetType)
      RecC Name
conName [VarBangType]
types -> Con -> Q [Clause]
go (Name -> [BangType] -> Con
NormalC Name
conName ((VarBangType -> BangType) -> [VarBangType] -> [BangType]
forall a b. (a -> b) -> [a] -> [b]
map VarBangType -> BangType
removeName [VarBangType]
types))
      InfixC BangType
l Name
conName BangType
r -> Con -> Q [Clause]
go ([Name] -> [BangType] -> Type -> Con
GadtC [Name
conName] [BangType
l, BangType
r] Type
rawRetType)
      ForallC [TyVarBndr Specificity]
_params [Type]
_ctx Con
con -> Con -> Q [Clause]
go Con
con
      RecGadtC [Name]
conNames [VarBangType]
argTypes Type
retType -> Con -> Q [Clause]
go ([Name] -> [BangType] -> Type -> Con
GadtC [Name]
conNames ((VarBangType -> BangType) -> [VarBangType] -> [BangType]
forall a b. (a -> b) -> [a] -> [b]
map VarBangType -> BangType
removeName [VarBangType]
argTypes) Type
retType)

toFreeFoilClauseFromQuantified :: FreeFoilConfig -> Type -> Con -> Q [Clause]
toFreeFoilClauseFromQuantified :: FreeFoilConfig -> Type -> Con -> Q [Clause]
toFreeFoilClauseFromQuantified FreeFoilConfig
config Type
rawRetType = Con -> Q [Clause]
go
  where
    go :: Con -> Q [Clause]
go = \case
      GadtC [Name]
conNames [BangType]
rawArgTypes Type
rawRetType' -> [[Clause]] -> [Clause]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[Clause]] -> [Clause]) -> Q [[Clause]] -> Q [Clause]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
        [Name] -> (Name -> Q [Clause]) -> Q [[Clause]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Name]
conNames ((Name -> Q [Clause]) -> Q [[Clause]])
-> (Name -> Q [Clause]) -> Q [[Clause]]
forall a b. (a -> b) -> a -> b
$ \Name
conName -> do
          [(_vars, _pat, pat, exps)] <- FreeFoilConfig -> Con -> Q [([Name], Pat, Pat, [Exp])]
termConToPatQuantified FreeFoilConfig
config
            ([Name] -> [BangType] -> Type -> Con
GadtC [Name
conName] [BangType]
rawArgTypes Type
rawRetType')    -- FIXME: unsafe matching!
          return [ Clause [pat] (NormalB (foldl AppE (ConE conName) exps)) [] ]

      NormalC Name
conName [BangType]
types -> Con -> Q [Clause]
go ([Name] -> [BangType] -> Type -> Con
GadtC [Name
conName] [BangType]
types Type
rawRetType)
      RecC Name
conName [VarBangType]
types -> Con -> Q [Clause]
go (Name -> [BangType] -> Con
NormalC Name
conName ((VarBangType -> BangType) -> [VarBangType] -> [BangType]
forall a b. (a -> b) -> [a] -> [b]
map VarBangType -> BangType
removeName [VarBangType]
types))
      InfixC BangType
l Name
conName BangType
r -> Con -> Q [Clause]
go ([Name] -> [BangType] -> Type -> Con
GadtC [Name
conName] [BangType
l, BangType
r] Type
rawRetType)
      ForallC [TyVarBndr Specificity]
_params [Type]
_ctx Con
con -> Con -> Q [Clause]
go Con
con
      RecGadtC [Name]
conNames [VarBangType]
argTypes Type
retType -> Con -> Q [Clause]
go ([Name] -> [BangType] -> Type -> Con
GadtC [Name]
conNames ((VarBangType -> BangType) -> [VarBangType] -> [BangType]
forall a b. (a -> b) -> [a] -> [b]
map VarBangType -> BangType
removeName [VarBangType]
argTypes) Type
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 :: FreeFoilConfig -> Q [Dec]
mkFreeFoil config :: FreeFoilConfig
config@FreeFoilConfig{[Name]
[FreeFoilTermConfig]
String -> String
rawQuantifiedNames :: FreeFoilConfig -> [Name]
freeFoilTermConfigs :: FreeFoilConfig -> [FreeFoilTermConfig]
freeFoilNameModifier :: FreeFoilConfig -> String -> String
freeFoilScopeNameModifier :: FreeFoilConfig -> String -> String
signatureNameModifier :: FreeFoilConfig -> String -> String
freeFoilConNameModifier :: FreeFoilConfig -> String -> String
freeFoilConvertToName :: FreeFoilConfig -> String -> String
freeFoilConvertFromName :: FreeFoilConfig -> String -> String
rawQuantifiedNames :: [Name]
freeFoilTermConfigs :: [FreeFoilTermConfig]
freeFoilNameModifier :: String -> String
freeFoilScopeNameModifier :: String -> String
signatureNameModifier :: String -> String
freeFoilConNameModifier :: String -> String
freeFoilConvertToName :: String -> String
freeFoilConvertFromName :: String -> String
..} = [[Dec]] -> [Dec]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[Dec]] -> [Dec]) -> Q [[Dec]] -> Q [Dec]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Q [Dec]] -> Q [[Dec]]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a. Monad m => [m a] -> m [a]
sequence
  [ (Name -> Q Dec) -> [Name] -> Q [Dec]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Name -> Q Dec
mkQuantifiedType [Name]
rawQuantifiedNames
  , (FreeFoilTermConfig -> Q Dec) -> [FreeFoilTermConfig] -> Q [Dec]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM FreeFoilTermConfig -> Q Dec
mkBindingType [FreeFoilTermConfig]
freeFoilTermConfigs
  , [[Dec]] -> [Dec]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[Dec]] -> [Dec]) -> Q [[Dec]] -> Q [Dec]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (FreeFoilTermConfig -> Q [Dec])
-> [FreeFoilTermConfig] -> Q [[Dec]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM FreeFoilTermConfig -> Q [Dec]
mkPatternCoSinkable [FreeFoilTermConfig]
freeFoilTermConfigs
  , [[Dec]] -> [Dec]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[Dec]] -> [Dec]) -> Q [[Dec]] -> Q [Dec]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (FreeFoilTermConfig -> Q [Dec])
-> [FreeFoilTermConfig] -> Q [[Dec]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM FreeFoilTermConfig -> Q [Dec]
mkSignatureTypes [FreeFoilTermConfig]
freeFoilTermConfigs
  , [[Dec]] -> [Dec]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[Dec]] -> [Dec]) -> Q [[Dec]] -> Q [Dec]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (FreeFoilTermConfig -> Q [Dec])
-> [FreeFoilTermConfig] -> Q [[Dec]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM FreeFoilTermConfig -> Q [Dec]
mkPatternSynonyms [FreeFoilTermConfig]
freeFoilTermConfigs
  ]
  where
    scope :: Name
scope = String -> Name
mkName String
"scope"
    term :: Name
term = String -> Name
mkName String
"term"
    outerScope :: Name
outerScope = String -> Name
mkName String
"o"
    innerScope :: Name
innerScope = String -> Name
mkName String
"i"

    mkPatternSynonyms :: FreeFoilTermConfig -> Q [Dec]
mkPatternSynonyms termConfig :: FreeFoilTermConfig
termConfig@FreeFoilTermConfig{[Name]
Name
rawIdentName :: FreeFoilTermConfig -> Name
rawTermName :: FreeFoilTermConfig -> Name
rawBindingName :: FreeFoilTermConfig -> Name
rawScopeName :: FreeFoilTermConfig -> Name
rawVarConName :: FreeFoilTermConfig -> Name
rawSubTermNames :: FreeFoilTermConfig -> [Name]
rawSubScopeNames :: FreeFoilTermConfig -> [Name]
intToRawIdentName :: FreeFoilTermConfig -> Name
rawVarIdentToTermName :: FreeFoilTermConfig -> Name
rawTermToScopeName :: FreeFoilTermConfig -> Name
rawScopeToTermName :: FreeFoilTermConfig -> Name
rawIdentName :: Name
rawTermName :: Name
rawBindingName :: Name
rawScopeName :: Name
rawVarConName :: Name
rawSubTermNames :: [Name]
rawSubScopeNames :: [Name]
intToRawIdentName :: Name
rawVarIdentToTermName :: Name
rawTermToScopeName :: Name
rawScopeToTermName :: Name
..} = do
      ds <- FreeFoilTermConfig -> Name -> Q [Dec]
mkPatternSynonyms' FreeFoilTermConfig
termConfig Name
rawTermName
      ds' <- concat <$> mapM (mkPatternSynonyms' termConfig) (rawSubTermNames <> rawSubScopeNames)
      return (ds <> ds')

    mkPatternSynonyms' :: FreeFoilTermConfig -> Name -> Q [Dec]
mkPatternSynonyms' FreeFoilTermConfig{[Name]
Name
rawIdentName :: FreeFoilTermConfig -> Name
rawTermName :: FreeFoilTermConfig -> Name
rawBindingName :: FreeFoilTermConfig -> Name
rawScopeName :: FreeFoilTermConfig -> Name
rawVarConName :: FreeFoilTermConfig -> Name
rawSubTermNames :: FreeFoilTermConfig -> [Name]
rawSubScopeNames :: FreeFoilTermConfig -> [Name]
intToRawIdentName :: FreeFoilTermConfig -> Name
rawVarIdentToTermName :: FreeFoilTermConfig -> Name
rawTermToScopeName :: FreeFoilTermConfig -> Name
rawScopeToTermName :: FreeFoilTermConfig -> Name
rawIdentName :: Name
rawTermName :: Name
rawBindingName :: Name
rawScopeName :: Name
rawVarConName :: Name
rawSubTermNames :: [Name]
rawSubScopeNames :: [Name]
intToRawIdentName :: Name
rawVarIdentToTermName :: Name
rawTermToScopeName :: Name
rawScopeToTermName :: Name
..} Name
rawName = do
      (tvars, cons) <- Name -> Q ([TyVarBndr BndrVis], [Con])
reifyDataOrNewtype Name
rawName
      let rawRetType = Name -> [Type] -> Type
PeelConT Name
rawName ((TyVarBndr BndrVis -> Type) -> [TyVarBndr BndrVis] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (Name -> Type
VarT (Name -> Type)
-> (TyVarBndr BndrVis -> Name) -> TyVarBndr BndrVis -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyVarBndr BndrVis -> Name
forall a. TyVarBndr a -> Name
tvarName) [TyVarBndr BndrVis]
tvars)
      (unzip -> (patNames, decls)) <- concat <$> mapM (mkPatternSynonym rawName config FreeFoilTermConfig{..} rawRetType) cons
      let completeDecl
            | Name
rawName Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
rawTermName = Pragma -> Dec
PragmaD ([Name] -> Maybe Name -> Pragma
CompleteP ('Foil.Var Name -> [Name] -> [Name]
forall a. a -> [a] -> [a]
: [Name]
patNames) Maybe Name
forall a. Maybe a
Nothing)
            | Bool
otherwise = Pragma -> Dec
PragmaD ([Name] -> Maybe Name -> Pragma
CompleteP [Name]
patNames Maybe Name
forall a. Maybe a
Nothing)
      return (concat decls ++ [completeDecl])

    mkQuantifiedType :: Name -> Q Dec
mkQuantifiedType Name
rawName = do
      (tvars, cons) <- Name -> Q ([TyVarBndr BndrVis], [Con])
reifyDataOrNewtype Name
rawName
      let name = FreeFoilConfig -> Name -> Name
toFreeFoilName FreeFoilConfig
config Name
rawName
          rawRetType = Name -> [Type] -> Type
PeelConT Name
rawName ((TyVarBndr BndrVis -> Type) -> [TyVarBndr BndrVis] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (Name -> Type
VarT (Name -> Type)
-> (TyVarBndr BndrVis -> Name) -> TyVarBndr BndrVis -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyVarBndr BndrVis -> Name
forall a. TyVarBndr a -> Name
tvarName) [TyVarBndr BndrVis]
tvars)
          newParams = [TyVarBndr BndrVis]
tvars [TyVarBndr BndrVis] -> [TyVarBndr BndrVis] -> [TyVarBndr BndrVis]
forall a. [a] -> [a] -> [a]
++ [Name -> BndrVis -> TyVarBndr BndrVis
forall flag. Name -> flag -> TyVarBndr flag
PlainTV Name
outerScope BndrVis
BndrReq]
          toCon = FreeFoilConfig -> Type -> Type -> Type -> Con -> Q Con
toFreeFoilCon FreeFoilConfig
config Type
rawRetType (Name -> Type
VarT Name
outerScope) (Name -> Type
VarT Name
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 -> Q Dec
mkBindingType FreeFoilTermConfig{[Name]
Name
rawIdentName :: FreeFoilTermConfig -> Name
rawTermName :: FreeFoilTermConfig -> Name
rawBindingName :: FreeFoilTermConfig -> Name
rawScopeName :: FreeFoilTermConfig -> Name
rawVarConName :: FreeFoilTermConfig -> Name
rawSubTermNames :: FreeFoilTermConfig -> [Name]
rawSubScopeNames :: FreeFoilTermConfig -> [Name]
intToRawIdentName :: FreeFoilTermConfig -> Name
rawVarIdentToTermName :: FreeFoilTermConfig -> Name
rawTermToScopeName :: FreeFoilTermConfig -> Name
rawScopeToTermName :: FreeFoilTermConfig -> Name
rawIdentName :: Name
rawTermName :: Name
rawBindingName :: Name
rawScopeName :: Name
rawVarConName :: Name
rawSubTermNames :: [Name]
rawSubScopeNames :: [Name]
intToRawIdentName :: Name
rawVarIdentToTermName :: Name
rawTermToScopeName :: Name
rawScopeToTermName :: Name
..} = do
      (tvars, cons) <- Name -> Q ([TyVarBndr BndrVis], [Con])
reifyDataOrNewtype Name
rawBindingName
      let bindingName = FreeFoilConfig -> Name -> Name
toFreeFoilName FreeFoilConfig
config Name
rawBindingName
          rawRetType = Name -> [Type] -> Type
PeelConT Name
rawBindingName ((TyVarBndr BndrVis -> Type) -> [TyVarBndr BndrVis] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (Name -> Type
VarT (Name -> Type)
-> (TyVarBndr BndrVis -> Name) -> TyVarBndr BndrVis -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyVarBndr BndrVis -> Name
forall a. TyVarBndr a -> Name
tvarName) [TyVarBndr BndrVis]
tvars)
          newParams = [TyVarBndr BndrVis]
tvars [TyVarBndr BndrVis] -> [TyVarBndr BndrVis] -> [TyVarBndr BndrVis]
forall a. [a] -> [a] -> [a]
++ [Name -> BndrVis -> TyVarBndr BndrVis
forall flag. Name -> flag -> TyVarBndr flag
PlainTV Name
outerScope BndrVis
BndrReq, Name -> BndrVis -> TyVarBndr BndrVis
forall flag. Name -> flag -> TyVarBndr flag
PlainTV Name
innerScope BndrVis
BndrReq]
          toCon = FreeFoilConfig -> Type -> Type -> Con -> Q Con
toFreeFoilBindingCon FreeFoilConfig
config Type
rawRetType (Name -> Type
VarT Name
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 -> Q [Dec]
mkPatternCoSinkable FreeFoilTermConfig{[Name]
Name
rawIdentName :: FreeFoilTermConfig -> Name
rawTermName :: FreeFoilTermConfig -> Name
rawBindingName :: FreeFoilTermConfig -> Name
rawScopeName :: FreeFoilTermConfig -> Name
rawVarConName :: FreeFoilTermConfig -> Name
rawSubTermNames :: FreeFoilTermConfig -> [Name]
rawSubScopeNames :: FreeFoilTermConfig -> [Name]
intToRawIdentName :: FreeFoilTermConfig -> Name
rawVarIdentToTermName :: FreeFoilTermConfig -> Name
rawTermToScopeName :: FreeFoilTermConfig -> Name
rawScopeToTermName :: FreeFoilTermConfig -> Name
rawIdentName :: Name
rawTermName :: Name
rawBindingName :: Name
rawScopeName :: Name
rawVarConName :: Name
rawSubTermNames :: [Name]
rawSubScopeNames :: [Name]
intToRawIdentName :: Name
rawVarIdentToTermName :: Name
rawTermToScopeName :: Name
rawScopeToTermName :: Name
..} = do
      (tvars, cons) <- Name -> Q ([TyVarBndr BndrVis], [Con])
reifyDataOrNewtype Name
rawBindingName
      let bindingName = FreeFoilConfig -> Name -> Name
toFreeFoilName FreeFoilConfig
config Name
rawBindingName
          bindingT = Name -> [Type] -> Type
PeelConT Name
bindingName ((TyVarBndr BndrVis -> Type) -> [TyVarBndr BndrVis] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (Name -> Type
VarT (Name -> Type)
-> (TyVarBndr BndrVis -> Name) -> TyVarBndr BndrVis -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyVarBndr BndrVis -> Name
forall a. TyVarBndr a -> Name
tvarName) [TyVarBndr BndrVis]
tvars)
          flatCons = [Con] -> [(Name, [Type])]
flattenCons [Con]
cons
      forM_ flatCons $ \(Name
conName, [Type]
fieldTypes) ->
        [Type] -> (Type -> Q ()) -> Q ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [Type]
fieldTypes ((Type -> Q ()) -> Q ()) -> (Type -> Q ()) -> Q ()
forall a b. (a -> b) -> a -> b
$ \Type
fieldType ->
          case FreeFoilConfig -> Type -> BindingFieldSort
bindingFieldSortOf FreeFoilConfig
config Type
fieldType of
            BindingFieldSort
FieldPayload | FreeFoilConfig -> Type -> Bool
mentionsScopeIndexed FreeFoilConfig
config Type
fieldType -> String -> Q ()
forall a. String -> Q a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> Q ()) -> String -> Q ()
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines
              [ String
"mkFreeFoil: cannot generate a CoSinkable instance for " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Name -> String
forall a. Show a => a -> String
show Name
bindingName
              , String
"  constructor " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Name -> String
forall a. Show a => a -> String
show Name
conName String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
" has a payload of raw type " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Type -> String
forall a. Ppr a => a -> String
pprint Type
fieldType
              , String
"  which becomes scope-indexed; write the instance by hand"
              , String
"  (transportPayload is the sanctioned way to rebuild such a field)"
              ]
            BindingFieldSort
_ -> () -> Q ()
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
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 :: FreeFoilTermConfig -> Q [Dec]
mkSignatureTypes termConfig :: FreeFoilTermConfig
termConfig@FreeFoilTermConfig{[Name]
Name
rawIdentName :: FreeFoilTermConfig -> Name
rawTermName :: FreeFoilTermConfig -> Name
rawBindingName :: FreeFoilTermConfig -> Name
rawScopeName :: FreeFoilTermConfig -> Name
rawVarConName :: FreeFoilTermConfig -> Name
rawSubTermNames :: FreeFoilTermConfig -> [Name]
rawSubScopeNames :: FreeFoilTermConfig -> [Name]
intToRawIdentName :: FreeFoilTermConfig -> Name
rawVarIdentToTermName :: FreeFoilTermConfig -> Name
rawTermToScopeName :: FreeFoilTermConfig -> Name
rawScopeToTermName :: FreeFoilTermConfig -> Name
rawIdentName :: Name
rawTermName :: Name
rawBindingName :: Name
rawScopeName :: Name
rawVarConName :: Name
rawSubTermNames :: [Name]
rawSubScopeNames :: [Name]
intToRawIdentName :: Name
rawVarIdentToTermName :: Name
rawTermToScopeName :: Name
rawScopeToTermName :: Name
..} = do
      sig <- FreeFoilTermConfig -> Name -> Q [Dec]
mkSignatureType FreeFoilTermConfig
termConfig Name
rawTermName
      subsigs <- concat <$> mapM (mkSignatureType termConfig) (rawSubTermNames <> rawSubScopeNames)
      return (sig ++ subsigs)

    mkSignatureType :: FreeFoilTermConfig -> Name -> Q [Dec]
mkSignatureType termConfig :: FreeFoilTermConfig
termConfig@FreeFoilTermConfig{[Name]
Name
rawIdentName :: FreeFoilTermConfig -> Name
rawTermName :: FreeFoilTermConfig -> Name
rawBindingName :: FreeFoilTermConfig -> Name
rawScopeName :: FreeFoilTermConfig -> Name
rawVarConName :: FreeFoilTermConfig -> Name
rawSubTermNames :: FreeFoilTermConfig -> [Name]
rawSubScopeNames :: FreeFoilTermConfig -> [Name]
intToRawIdentName :: FreeFoilTermConfig -> Name
rawVarIdentToTermName :: FreeFoilTermConfig -> Name
rawTermToScopeName :: FreeFoilTermConfig -> Name
rawScopeToTermName :: FreeFoilTermConfig -> Name
rawIdentName :: Name
rawTermName :: Name
rawBindingName :: Name
rawScopeName :: Name
rawVarConName :: Name
rawSubTermNames :: [Name]
rawSubScopeNames :: [Name]
intToRawIdentName :: Name
rawVarIdentToTermName :: Name
rawTermToScopeName :: Name
rawScopeToTermName :: Name
..} Name
rawName = do
      (tvars, cons) <- Name -> Q ([TyVarBndr BndrVis], [Con])
reifyDataOrNewtype Name
rawName
      let sigName = FreeFoilConfig -> Name -> Name
toSignatureName FreeFoilConfig
config Name
rawName
          tvars' = (TyVarBndr BndrVis -> Type) -> [TyVarBndr BndrVis] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (Name -> Type
VarT (Name -> Type)
-> (TyVarBndr BndrVis -> Name) -> TyVarBndr BndrVis -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyVarBndr BndrVis -> Name
forall a. TyVarBndr a -> Name
tvarName) [TyVarBndr BndrVis]
tvars
          rawRetType = Name -> [Type] -> Type
PeelConT Name
rawName [Type]
tvars'
          newParams = [TyVarBndr BndrVis]
tvars [TyVarBndr BndrVis] -> [TyVarBndr BndrVis] -> [TyVarBndr BndrVis]
forall a. [a] -> [a] -> [a]
++ [Name -> BndrVis -> TyVarBndr BndrVis
forall flag. Name -> flag -> TyVarBndr flag
PlainTV Name
scope BndrVis
BndrReq, Name -> BndrVis -> TyVarBndr BndrVis
forall flag. Name -> flag -> TyVarBndr flag
PlainTV Name
term BndrVis
BndrReq]
          toCon = FreeFoilConfig
-> FreeFoilTermConfig
-> Name
-> Type
-> Type
-> Type
-> Con
-> Q (Maybe Con)
toFreeFoilSigCon FreeFoilConfig
config FreeFoilTermConfig
termConfig Name
sigName Type
rawRetType (Name -> Type
VarT Name
scope) (Name -> Type
VarT Name
term)
      newCons <- catMaybes <$> mapM toCon cons
      let bindingT = Name -> [Type] -> Type
PeelConT (FreeFoilConfig -> Name -> Name
toFreeFoilName FreeFoilConfig
config Name
rawBindingName) [Type]
tvars'
          sigNameT = Name -> [Type] -> Type
PeelConT (FreeFoilConfig -> Name -> Name
toSignatureName FreeFoilConfig
config Name
rawTermName) [Type]
tvars'
          astName = FreeFoilConfig -> Name -> Name
toFreeFoilName FreeFoilConfig
config Name
rawName
          scopeName = FreeFoilConfig -> Name -> Name
toFreeFoilScopedName FreeFoilConfig
config Name
rawName
          termAST = Name -> [Type] -> Type
PeelConT ''Foil.AST [Type
bindingT, Type
sigNameT]
          scopedTermAST = Name -> [Type] -> Type
PeelConT ''Foil.ScopedAST [Type
bindingT, Type
sigNameT]
          n = String -> Name
mkName String
"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
Type
a --> :: Type -> Type -> Type
--> Type
b = Type -> Type -> Type
AppT (Type -> Type -> Type
AppT Type
ArrowT Type
a) Type
b

reifyDataOrNewtype :: Name -> Q ([TyVarBndr BndrVis], [Con])
reifyDataOrNewtype :: Name -> Q ([TyVarBndr BndrVis], [Con])
reifyDataOrNewtype Name
name = Name -> Q Info
reify Name
name Q Info
-> (Info -> Q ([TyVarBndr BndrVis], [Con]))
-> Q ([TyVarBndr BndrVis], [Con])
forall a b. Q a -> (a -> Q b) -> Q b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
  TyConI (DataD [Type]
_ctx Name
_name [TyVarBndr BndrVis]
tvars Maybe Type
_kind [Con]
cons [DerivClause]
_deriv) -> ([TyVarBndr BndrVis], [Con]) -> Q ([TyVarBndr BndrVis], [Con])
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return ([TyVarBndr BndrVis]
tvars, [Con]
cons)
  TyConI (NewtypeD [Type]
_ctx Name
_name [TyVarBndr BndrVis]
tvars Maybe Type
_kind Con
con [DerivClause]
_deriv) -> ([TyVarBndr BndrVis], [Con]) -> Q ([TyVarBndr BndrVis], [Con])
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return ([TyVarBndr BndrVis]
tvars, [Con
con])
  Info
_ -> String -> Q ([TyVarBndr BndrVis], [Con])
forall a. HasCallStack => String -> a
error (String
"not a data or newtype: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
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 :: FreeFoilConfig -> Q [Dec]
mkFreeFoilConversions config :: FreeFoilConfig
config@FreeFoilConfig{[Name]
[FreeFoilTermConfig]
String -> String
rawQuantifiedNames :: FreeFoilConfig -> [Name]
freeFoilTermConfigs :: FreeFoilConfig -> [FreeFoilTermConfig]
freeFoilNameModifier :: FreeFoilConfig -> String -> String
freeFoilScopeNameModifier :: FreeFoilConfig -> String -> String
signatureNameModifier :: FreeFoilConfig -> String -> String
freeFoilConNameModifier :: FreeFoilConfig -> String -> String
freeFoilConvertToName :: FreeFoilConfig -> String -> String
freeFoilConvertFromName :: FreeFoilConfig -> String -> String
rawQuantifiedNames :: [Name]
freeFoilTermConfigs :: [FreeFoilTermConfig]
freeFoilNameModifier :: String -> String
freeFoilScopeNameModifier :: String -> String
signatureNameModifier :: String -> String
freeFoilConNameModifier :: String -> String
freeFoilConvertToName :: String -> String
freeFoilConvertFromName :: String -> String
..} = [[Dec]] -> [Dec]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[Dec]] -> [Dec]) -> Q [[Dec]] -> Q [Dec]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Q [Dec]] -> Q [[Dec]]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a. Monad m => [m a] -> m [a]
sequence
  [ [[Dec]] -> [Dec]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[Dec]] -> [Dec]) -> Q [[Dec]] -> Q [Dec]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (FreeFoilTermConfig -> Q [Dec])
-> [FreeFoilTermConfig] -> Q [[Dec]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM FreeFoilTermConfig -> Q [Dec]
mkConvertFrom [FreeFoilTermConfig]
freeFoilTermConfigs
  , [[Dec]] -> [Dec]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[Dec]] -> [Dec]) -> Q [[Dec]] -> Q [Dec]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Name -> Q [Dec]) -> [Name] -> Q [[Dec]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Name -> Q [Dec]
mkConvertFromQuantified [Name]
rawQuantifiedNames
  , [[Dec]] -> [Dec]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[Dec]] -> [Dec]) -> Q [[Dec]] -> Q [Dec]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (FreeFoilTermConfig -> Q [Dec])
-> [FreeFoilTermConfig] -> Q [[Dec]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM FreeFoilTermConfig -> Q [Dec]
mkConvertTo [FreeFoilTermConfig]
freeFoilTermConfigs
  , [[Dec]] -> [Dec]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[Dec]] -> [Dec]) -> Q [[Dec]] -> Q [Dec]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Name -> Q [Dec]) -> [Name] -> Q [[Dec]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Name -> Q [Dec]
mkConvertToQuantified [Name]
rawQuantifiedNames
  ]
  where
    outerScope :: Name
outerScope = String -> Name
mkName String
"o"
    innerScope :: Name
innerScope = String -> Name
mkName String
"i"

    mkConvertFrom :: FreeFoilTermConfig -> Q [Dec]
mkConvertFrom termConfig :: FreeFoilTermConfig
termConfig@FreeFoilTermConfig{[Name]
Name
rawIdentName :: FreeFoilTermConfig -> Name
rawTermName :: FreeFoilTermConfig -> Name
rawBindingName :: FreeFoilTermConfig -> Name
rawScopeName :: FreeFoilTermConfig -> Name
rawVarConName :: FreeFoilTermConfig -> Name
rawSubTermNames :: FreeFoilTermConfig -> [Name]
rawSubScopeNames :: FreeFoilTermConfig -> [Name]
intToRawIdentName :: FreeFoilTermConfig -> Name
rawVarIdentToTermName :: FreeFoilTermConfig -> Name
rawTermToScopeName :: FreeFoilTermConfig -> Name
rawScopeToTermName :: FreeFoilTermConfig -> Name
rawIdentName :: Name
rawTermName :: Name
rawBindingName :: Name
rawScopeName :: Name
rawVarConName :: Name
rawSubTermNames :: [Name]
rawSubScopeNames :: [Name]
intToRawIdentName :: Name
rawVarIdentToTermName :: Name
rawTermToScopeName :: Name
rawScopeToTermName :: Name
..} = [[Dec]] -> [Dec]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[Dec]] -> [Dec]) -> Q [[Dec]] -> Q [Dec]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Q [Dec]] -> Q [[Dec]]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a. Monad m => [m a] -> m [a]
sequence
      [ [[Dec]] -> [Dec]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[Dec]] -> [Dec]) -> Q [[Dec]] -> Q [Dec]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Name -> Q [Dec]) -> [Name] -> Q [[Dec]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (FreeFoilTermConfig -> Name -> Q [Dec]
mkConvertFromSig FreeFoilTermConfig
termConfig) (Name
rawTermName Name -> [Name] -> [Name]
forall a. a -> [a] -> [a]
: ([Name]
rawSubTermNames [Name] -> [Name] -> [Name]
forall a. Semigroup a => a -> a -> a
<> [Name]
rawSubScopeNames))
      , FreeFoilTermConfig -> Q [Dec]
mkConvertFromBinding FreeFoilTermConfig
termConfig
      , [[Dec]] -> [Dec]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[Dec]] -> [Dec]) -> Q [[Dec]] -> Q [Dec]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Name -> Q [Dec]) -> [Name] -> Q [[Dec]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (FreeFoilTermConfig -> Name -> Q [Dec]
mkConvertFromSubTerm FreeFoilTermConfig
termConfig) ([Name]
rawSubTermNames [Name] -> [Name] -> [Name]
forall a. Semigroup a => a -> a -> a
<> [Name]
rawSubScopeNames)
      , FreeFoilTermConfig -> Q [Dec]
mkConvertFromTerm FreeFoilTermConfig
termConfig
      ]

    mkConvertFromSig :: FreeFoilTermConfig -> Name -> Q [Dec]
mkConvertFromSig termConfig :: FreeFoilTermConfig
termConfig@FreeFoilTermConfig{[Name]
Name
rawIdentName :: FreeFoilTermConfig -> Name
rawTermName :: FreeFoilTermConfig -> Name
rawBindingName :: FreeFoilTermConfig -> Name
rawScopeName :: FreeFoilTermConfig -> Name
rawVarConName :: FreeFoilTermConfig -> Name
rawSubTermNames :: FreeFoilTermConfig -> [Name]
rawSubScopeNames :: FreeFoilTermConfig -> [Name]
intToRawIdentName :: FreeFoilTermConfig -> Name
rawVarIdentToTermName :: FreeFoilTermConfig -> Name
rawTermToScopeName :: FreeFoilTermConfig -> Name
rawScopeToTermName :: FreeFoilTermConfig -> Name
rawIdentName :: Name
rawTermName :: Name
rawBindingName :: Name
rawScopeName :: Name
rawVarConName :: Name
rawSubTermNames :: [Name]
rawSubScopeNames :: [Name]
intToRawIdentName :: Name
rawVarIdentToTermName :: Name
rawTermToScopeName :: Name
rawScopeToTermName :: Name
..} Name
rawName = do
      (tvars, cons) <- Name -> Q ([TyVarBndr BndrVis], [Con])
reifyDataOrNewtype Name
rawName
      let rawSigName = FreeFoilConfig -> Name -> Name
toSignatureName FreeFoilConfig
config Name
rawName
          funName = FreeFoilConfig -> Name -> Name
toFreeFoilNameFrom FreeFoilConfig
config Name
rawSigName
          rawRetType = Name -> [Type] -> Type
PeelConT Name
rawName ((TyVarBndr BndrVis -> Type) -> [TyVarBndr BndrVis] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (Name -> Type
VarT (Name -> Type)
-> (TyVarBndr BndrVis -> Name) -> TyVarBndr BndrVis -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyVarBndr BndrVis -> Name
forall a. TyVarBndr a -> Name
tvarName) [TyVarBndr BndrVis]
tvars)
          rawTermType = Name -> [Type] -> Type
PeelConT Name
rawTermName ((TyVarBndr BndrVis -> Type) -> [TyVarBndr BndrVis] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (Name -> Type
VarT (Name -> Type)
-> (TyVarBndr BndrVis -> Name) -> TyVarBndr BndrVis -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyVarBndr BndrVis -> Name
forall a. TyVarBndr a -> Name
tvarName) [TyVarBndr BndrVis]
tvars)
          rawScopedTermType = Name -> [Type] -> Type
PeelConT Name
rawScopeName ((TyVarBndr BndrVis -> Type) -> [TyVarBndr BndrVis] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (Name -> Type
VarT (Name -> Type)
-> (TyVarBndr BndrVis -> Name) -> TyVarBndr BndrVis -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyVarBndr BndrVis -> Name
forall a. TyVarBndr a -> Name
tvarName) [TyVarBndr BndrVis]
tvars)
          rawBindingType = Name -> [Type] -> Type
PeelConT Name
rawBindingName ((TyVarBndr BndrVis -> Type) -> [TyVarBndr BndrVis] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (Name -> Type
VarT (Name -> Type)
-> (TyVarBndr BndrVis -> Name) -> TyVarBndr BndrVis -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyVarBndr BndrVis -> Name
forall a. TyVarBndr a -> Name
tvarName) [TyVarBndr BndrVis]
tvars)
          rawScopeType = Int -> Type
TupleT Int
2 Type -> Type -> Type
`AppT` Type
rawBindingType Type -> Type -> Type
`AppT` Type
rawScopedTermType
      case toFreeFoilSigType SortSubTerm config rawScopeType rawTermType rawRetType of
        Just Type
termType -> do
          clauses <- [[Clause]] -> [Clause]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[Clause]] -> [Clause]) -> Q [[Clause]] -> Q [Clause]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Con -> Q [Clause]) -> [Con] -> Q [[Clause]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Name
-> FreeFoilConfig
-> FreeFoilTermConfig
-> Type
-> Con
-> Q [Clause]
toFreeFoilClauseFrom Name
rawSigName FreeFoilConfig
config FreeFoilTermConfig
termConfig Type
rawRetType) [Con]
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 ]
        Maybe Type
Nothing -> String -> Q [Dec]
forall a. HasCallStack => String -> a
error String
"impossible happened"

    mkConvertFromTerm :: FreeFoilTermConfig -> Q [Dec]
mkConvertFromTerm FreeFoilTermConfig{[Name]
Name
rawIdentName :: FreeFoilTermConfig -> Name
rawTermName :: FreeFoilTermConfig -> Name
rawBindingName :: FreeFoilTermConfig -> Name
rawScopeName :: FreeFoilTermConfig -> Name
rawVarConName :: FreeFoilTermConfig -> Name
rawSubTermNames :: FreeFoilTermConfig -> [Name]
rawSubScopeNames :: FreeFoilTermConfig -> [Name]
intToRawIdentName :: FreeFoilTermConfig -> Name
rawVarIdentToTermName :: FreeFoilTermConfig -> Name
rawTermToScopeName :: FreeFoilTermConfig -> Name
rawScopeToTermName :: FreeFoilTermConfig -> Name
rawIdentName :: Name
rawTermName :: Name
rawBindingName :: Name
rawScopeName :: Name
rawVarConName :: Name
rawSubTermNames :: [Name]
rawSubScopeNames :: [Name]
intToRawIdentName :: Name
rawVarIdentToTermName :: Name
rawTermToScopeName :: Name
rawScopeToTermName :: Name
..} = do
      (tvars, _cons) <- Name -> Q ([TyVarBndr BndrVis], [Con])
reifyDataOrNewtype Name
rawTermName
      let funName = FreeFoilConfig -> Name -> Name
toFreeFoilNameFrom FreeFoilConfig
config Name
rawTermName
          rawSigName = FreeFoilConfig -> Name -> Name
toSignatureName FreeFoilConfig
config Name
rawTermName
          funSigName = FreeFoilConfig -> Name -> Name
toFreeFoilNameFrom FreeFoilConfig
config Name
rawSigName
          funBindingName = FreeFoilConfig -> Name -> Name
toFreeFoilNameFrom FreeFoilConfig
config Name
rawBindingName
          rawTermType = Name -> [Type] -> Type
PeelConT Name
rawTermName ((TyVarBndr BndrVis -> Type) -> [TyVarBndr BndrVis] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (Name -> Type
VarT (Name -> Type)
-> (TyVarBndr BndrVis -> Name) -> TyVarBndr BndrVis -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyVarBndr BndrVis -> Name
forall a. TyVarBndr a -> Name
tvarName) [TyVarBndr BndrVis]
tvars)
          termType =  Sort -> FreeFoilConfig -> Type -> Type -> Type -> Type
toFreeFoilType Sort
SortTerm FreeFoilConfig
config (Name -> Type
VarT Name
outerScope) (Name -> Type
VarT Name
innerScope) Type
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 -> Name -> Q [Dec]
mkConvertFromSubTerm FreeFoilTermConfig{[Name]
Name
rawIdentName :: FreeFoilTermConfig -> Name
rawTermName :: FreeFoilTermConfig -> Name
rawBindingName :: FreeFoilTermConfig -> Name
rawScopeName :: FreeFoilTermConfig -> Name
rawVarConName :: FreeFoilTermConfig -> Name
rawSubTermNames :: FreeFoilTermConfig -> [Name]
rawSubScopeNames :: FreeFoilTermConfig -> [Name]
intToRawIdentName :: FreeFoilTermConfig -> Name
rawVarIdentToTermName :: FreeFoilTermConfig -> Name
rawTermToScopeName :: FreeFoilTermConfig -> Name
rawScopeToTermName :: FreeFoilTermConfig -> Name
rawIdentName :: Name
rawTermName :: Name
rawBindingName :: Name
rawScopeName :: Name
rawVarConName :: Name
rawSubTermNames :: [Name]
rawSubScopeNames :: [Name]
intToRawIdentName :: Name
rawVarIdentToTermName :: Name
rawTermToScopeName :: Name
rawScopeToTermName :: Name
..} Name
rawName = do
      (tvars, _cons) <- Name -> Q ([TyVarBndr BndrVis], [Con])
reifyDataOrNewtype Name
rawName
      let funName = FreeFoilConfig -> Name -> Name
toFreeFoilNameFrom FreeFoilConfig
config Name
rawName
          funSigName = FreeFoilConfig -> Name -> Name
toFreeFoilNameFrom FreeFoilConfig
config (FreeFoilConfig -> Name -> Name
toSignatureName FreeFoilConfig
config Name
rawName)
          funTermName = FreeFoilConfig -> Name -> Name
toFreeFoilNameFrom FreeFoilConfig
config Name
rawTermName
          funBindingName = FreeFoilConfig -> Name -> Name
toFreeFoilNameFrom FreeFoilConfig
config Name
rawBindingName
          rawType = Name -> [Type] -> Type
PeelConT Name
rawName ((TyVarBndr BndrVis -> Type) -> [TyVarBndr BndrVis] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (Name -> Type
VarT (Name -> Type)
-> (TyVarBndr BndrVis -> Name) -> TyVarBndr BndrVis -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyVarBndr BndrVis -> Name
forall a. TyVarBndr a -> Name
tvarName) [TyVarBndr BndrVis]
tvars)
          safeType =  Sort -> FreeFoilConfig -> Type -> Type -> Type -> Type
toFreeFoilType Sort
SortTerm FreeFoilConfig
config (Name -> Type
VarT Name
outerScope) (Name -> Type
VarT Name
innerScope) Type
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 :: Name -> Q [Dec]
mkConvertFromQuantified Name
rawName = do
      (tvars, cons) <- Name -> Q ([TyVarBndr BndrVis], [Con])
reifyDataOrNewtype Name
rawName
      let funName = FreeFoilConfig -> Name -> Name
toFreeFoilNameFrom FreeFoilConfig
config Name
rawName
          rawType = Name -> [Type] -> Type
PeelConT Name
rawName ((TyVarBndr BndrVis -> Type) -> [TyVarBndr BndrVis] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (Name -> Type
VarT (Name -> Type)
-> (TyVarBndr BndrVis -> Name) -> TyVarBndr BndrVis -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyVarBndr BndrVis -> Name
forall a. TyVarBndr a -> Name
tvarName) [TyVarBndr BndrVis]
tvars)
          safeType = Sort -> FreeFoilConfig -> Type -> Type -> Type -> Type
toFreeFoilType Sort
SortTerm FreeFoilConfig
config (Name -> Type
VarT Name
outerScope) (Name -> Type
VarT Name
innerScope) Type
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 :: FreeFoilTermConfig -> Q [Dec]
mkConvertFromBinding termConfig :: FreeFoilTermConfig
termConfig@FreeFoilTermConfig{[Name]
Name
rawIdentName :: FreeFoilTermConfig -> Name
rawTermName :: FreeFoilTermConfig -> Name
rawBindingName :: FreeFoilTermConfig -> Name
rawScopeName :: FreeFoilTermConfig -> Name
rawVarConName :: FreeFoilTermConfig -> Name
rawSubTermNames :: FreeFoilTermConfig -> [Name]
rawSubScopeNames :: FreeFoilTermConfig -> [Name]
intToRawIdentName :: FreeFoilTermConfig -> Name
rawVarIdentToTermName :: FreeFoilTermConfig -> Name
rawTermToScopeName :: FreeFoilTermConfig -> Name
rawScopeToTermName :: FreeFoilTermConfig -> Name
rawIdentName :: Name
rawTermName :: Name
rawBindingName :: Name
rawScopeName :: Name
rawVarConName :: Name
rawSubTermNames :: [Name]
rawSubScopeNames :: [Name]
intToRawIdentName :: Name
rawVarIdentToTermName :: Name
rawTermToScopeName :: Name
rawScopeToTermName :: Name
..} = do
      (tvars, cons) <- Name -> Q ([TyVarBndr BndrVis], [Con])
reifyDataOrNewtype Name
rawBindingName
      (itvars, _cons) <- reifyDataOrNewtype rawIdentName
      named <- newName "_named"
      let funName = FreeFoilConfig -> Name -> Name
toFreeFoilNameFrom FreeFoilConfig
config Name
rawBindingName
          funWithName = Name -> Name
toNameWith Name
funName
          rawRetType = Name -> [Type] -> Type
PeelConT Name
rawBindingName ((TyVarBndr BndrVis -> Type) -> [TyVarBndr BndrVis] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (Name -> Type
VarT (Name -> Type)
-> (TyVarBndr BndrVis -> Name) -> TyVarBndr BndrVis -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyVarBndr BndrVis -> Name
forall a. TyVarBndr a -> Name
tvarName) [TyVarBndr BndrVis]
tvars)
          rawIdentType = Name -> [Type] -> Type
PeelConT Name
rawIdentName ((TyVarBndr BndrVis -> Type) -> [TyVarBndr BndrVis] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (Name -> Type
VarT (Name -> Type)
-> (TyVarBndr BndrVis -> Name) -> TyVarBndr BndrVis -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyVarBndr BndrVis -> Name
forall a. TyVarBndr a -> Name
tvarName) (Int -> [TyVarBndr BndrVis] -> [TyVarBndr BndrVis]
forall a. Int -> [a] -> [a]
take ([TyVarBndr BndrVis] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [TyVarBndr BndrVis]
itvars) [TyVarBndr BndrVis]
tvars)) -- FIXME: undocumented hack :(
          bindingType = Sort -> FreeFoilConfig -> Type -> Type -> Type -> Type
toFreeFoilType Sort
SortBinder FreeFoilConfig
config (Name -> Type
VarT Name
outerScope) (Name -> Type
VarT Name
innerScope) Type
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 :: FreeFoilTermConfig -> Q [Dec]
mkConvertTo termConfig :: FreeFoilTermConfig
termConfig@FreeFoilTermConfig{[Name]
Name
rawIdentName :: FreeFoilTermConfig -> Name
rawTermName :: FreeFoilTermConfig -> Name
rawBindingName :: FreeFoilTermConfig -> Name
rawScopeName :: FreeFoilTermConfig -> Name
rawVarConName :: FreeFoilTermConfig -> Name
rawSubTermNames :: FreeFoilTermConfig -> [Name]
rawSubScopeNames :: FreeFoilTermConfig -> [Name]
intToRawIdentName :: FreeFoilTermConfig -> Name
rawVarIdentToTermName :: FreeFoilTermConfig -> Name
rawTermToScopeName :: FreeFoilTermConfig -> Name
rawScopeToTermName :: FreeFoilTermConfig -> Name
rawIdentName :: Name
rawTermName :: Name
rawBindingName :: Name
rawScopeName :: Name
rawVarConName :: Name
rawSubTermNames :: [Name]
rawSubScopeNames :: [Name]
intToRawIdentName :: Name
rawVarIdentToTermName :: Name
rawTermToScopeName :: Name
rawScopeToTermName :: Name
..} = [[Dec]] -> [Dec]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[Dec]] -> [Dec]) -> Q [[Dec]] -> Q [Dec]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Q [Dec]] -> Q [[Dec]]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a. Monad m => [m a] -> m [a]
sequence
      [ Sort -> FreeFoilTermConfig -> Name -> Q [Dec]
mkConvertToSig Sort
SortTerm FreeFoilTermConfig
termConfig Name
rawTermName
      , [[Dec]] -> [Dec]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[Dec]] -> [Dec]) -> Q [[Dec]] -> Q [Dec]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Name -> Q [Dec]) -> [Name] -> Q [[Dec]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Sort -> FreeFoilTermConfig -> Name -> Q [Dec]
mkConvertToSig Sort
SortSubTerm FreeFoilTermConfig
termConfig) ([Name]
rawSubTermNames [Name] -> [Name] -> [Name]
forall a. Semigroup a => a -> a -> a
<> [Name]
rawSubScopeNames)
      , FreeFoilTermConfig -> Q [Dec]
mkConvertToBinding FreeFoilTermConfig
termConfig
      , [[Dec]] -> [Dec]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[Dec]] -> [Dec]) -> Q [[Dec]] -> Q [Dec]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Name -> Q [Dec]) -> [Name] -> Q [[Dec]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (FreeFoilTermConfig -> Name -> Q [Dec]
mkConvertToSubTerm FreeFoilTermConfig
termConfig) ([Name]
rawSubTermNames [Name] -> [Name] -> [Name]
forall a. Semigroup a => a -> a -> a
<> [Name]
rawSubScopeNames)
      , FreeFoilTermConfig -> Q [Dec]
mkConvertToTerm FreeFoilTermConfig
termConfig
      ]

    mkConvertToSubTerm :: FreeFoilTermConfig -> Name -> Q [Dec]
mkConvertToSubTerm termConfig :: FreeFoilTermConfig
termConfig@FreeFoilTermConfig{[Name]
Name
rawIdentName :: FreeFoilTermConfig -> Name
rawTermName :: FreeFoilTermConfig -> Name
rawBindingName :: FreeFoilTermConfig -> Name
rawScopeName :: FreeFoilTermConfig -> Name
rawVarConName :: FreeFoilTermConfig -> Name
rawSubTermNames :: FreeFoilTermConfig -> [Name]
rawSubScopeNames :: FreeFoilTermConfig -> [Name]
intToRawIdentName :: FreeFoilTermConfig -> Name
rawVarIdentToTermName :: FreeFoilTermConfig -> Name
rawTermToScopeName :: FreeFoilTermConfig -> Name
rawScopeToTermName :: FreeFoilTermConfig -> Name
rawIdentName :: Name
rawTermName :: Name
rawBindingName :: Name
rawScopeName :: Name
rawVarConName :: Name
rawSubTermNames :: [Name]
rawSubScopeNames :: [Name]
intToRawIdentName :: Name
rawVarIdentToTermName :: Name
rawTermToScopeName :: Name
rawScopeToTermName :: Name
..} Name
rawName = do
      (tvars, cons) <- Name -> Q ([TyVarBndr BndrVis], [Con])
reifyDataOrNewtype Name
rawName
      (itvars, _cons) <- reifyDataOrNewtype rawIdentName
      let funName = FreeFoilConfig -> Name -> Name
toFreeFoilNameTo FreeFoilConfig
config Name
rawName
          rawIdentType = Name -> [Type] -> Type
PeelConT Name
rawIdentName ((TyVarBndr BndrVis -> Type) -> [TyVarBndr BndrVis] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (Name -> Type
VarT (Name -> Type)
-> (TyVarBndr BndrVis -> Name) -> TyVarBndr BndrVis -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyVarBndr BndrVis -> Name
forall a. TyVarBndr a -> Name
tvarName) (Int -> [TyVarBndr BndrVis] -> [TyVarBndr BndrVis]
forall a. Int -> [a] -> [a]
take ([TyVarBndr BndrVis] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [TyVarBndr BndrVis]
itvars) [TyVarBndr BndrVis]
tvars)) -- FIXME: undocumented hack :(
          rawType = Name -> [Type] -> Type
PeelConT Name
rawName ((TyVarBndr BndrVis -> Type) -> [TyVarBndr BndrVis] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (Name -> Type
VarT (Name -> Type)
-> (TyVarBndr BndrVis -> Name) -> TyVarBndr BndrVis -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyVarBndr BndrVis -> Name
forall a. TyVarBndr a -> Name
tvarName) [TyVarBndr BndrVis]
tvars)
          safeType =  Sort -> FreeFoilConfig -> Type -> Type -> Type -> Type
toFreeFoilType Sort
SortTerm FreeFoilConfig
config (Name -> Type
VarT Name
outerScope) (Name -> Type
VarT Name
innerScope) Type
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
            | Name
rawName Name -> [Name] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
rawSubTermNames = Name
outerScope
            | Bool
otherwise = Name
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 -> Q [Dec]
mkConvertToTerm FreeFoilTermConfig{[Name]
Name
rawIdentName :: FreeFoilTermConfig -> Name
rawTermName :: FreeFoilTermConfig -> Name
rawBindingName :: FreeFoilTermConfig -> Name
rawScopeName :: FreeFoilTermConfig -> Name
rawVarConName :: FreeFoilTermConfig -> Name
rawSubTermNames :: FreeFoilTermConfig -> [Name]
rawSubScopeNames :: FreeFoilTermConfig -> [Name]
intToRawIdentName :: FreeFoilTermConfig -> Name
rawVarIdentToTermName :: FreeFoilTermConfig -> Name
rawTermToScopeName :: FreeFoilTermConfig -> Name
rawScopeToTermName :: FreeFoilTermConfig -> Name
rawIdentName :: Name
rawTermName :: Name
rawBindingName :: Name
rawScopeName :: Name
rawVarConName :: Name
rawSubTermNames :: [Name]
rawSubScopeNames :: [Name]
intToRawIdentName :: Name
rawVarIdentToTermName :: Name
rawTermToScopeName :: Name
rawScopeToTermName :: Name
..} = do
      (tvars, _cons) <- Name -> Q ([TyVarBndr BndrVis], [Con])
reifyDataOrNewtype Name
rawTermName
      (itvars, _cons) <- reifyDataOrNewtype rawIdentName
      let funName = FreeFoilConfig -> Name -> Name
toFreeFoilNameTo FreeFoilConfig
config Name
rawTermName
          rawSigName = FreeFoilConfig -> Name -> Name
toSignatureName FreeFoilConfig
config Name
rawTermName
          rawIdentType = Name -> [Type] -> Type
PeelConT Name
rawIdentName ((TyVarBndr BndrVis -> Type) -> [TyVarBndr BndrVis] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (Name -> Type
VarT (Name -> Type)
-> (TyVarBndr BndrVis -> Name) -> TyVarBndr BndrVis -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyVarBndr BndrVis -> Name
forall a. TyVarBndr a -> Name
tvarName) (Int -> [TyVarBndr BndrVis] -> [TyVarBndr BndrVis]
forall a. Int -> [a] -> [a]
take ([TyVarBndr BndrVis] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [TyVarBndr BndrVis]
itvars) [TyVarBndr BndrVis]
tvars)) -- FIXME: undocumented hack :(
          funSigName = FreeFoilConfig -> Name -> Name
toFreeFoilNameTo FreeFoilConfig
config Name
rawSigName
          funBindingName = FreeFoilConfig -> Name -> Name
toFreeFoilNameTo FreeFoilConfig
config Name
rawBindingName
          rawTermType = Name -> [Type] -> Type
PeelConT Name
rawTermName ((TyVarBndr BndrVis -> Type) -> [TyVarBndr BndrVis] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (Name -> Type
VarT (Name -> Type)
-> (TyVarBndr BndrVis -> Name) -> TyVarBndr BndrVis -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyVarBndr BndrVis -> Name
forall a. TyVarBndr a -> Name
tvarName) [TyVarBndr BndrVis]
tvars)
          termType =  Sort -> FreeFoilConfig -> Type -> Type -> Type -> Type
toFreeFoilType Sort
SortTerm FreeFoilConfig
config (Name -> Type
VarT Name
outerScope) (Name -> Type
VarT Name
innerScope) Type
rawTermType
          tryFunName = String -> Name
mkName (String
"try" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
capitalizeFirst (Name -> String
nameBase Name
funName))
          tryWithFunName = String -> Name
mkName (Name -> String
nameBase Name
tryFunName String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"With")
          unresolvedType = Name -> Type
ConT ''Foil.UnresolvedName Type -> Type -> Type
`AppT` Type
rawIdentType
          tryTermType = Name -> Type
ConT ''Either Type -> Type -> Type
`AppT` Type
unresolvedType Type -> Type -> Type
`AppT` Type
termType
          convertArgs Name
f = Name -> Exp
VarE Name
f
            Exp -> Exp -> Exp
`AppE` Name -> Exp
VarE Name
funSigName
            Exp -> Exp -> Exp
`AppE` Name -> Exp
VarE Name
funBindingName
            Exp -> Exp -> Exp
`AppE` Name -> Exp
VarE Name
rawScopeToTermName
          convertArgsIn Name
f Name
range = Name -> Exp
VarE Name
f
            Exp -> Exp -> Exp
`AppE` Name -> Exp
VarE Name
funSigName
            Exp -> Exp -> Exp
`AppE` (Name -> Exp
VarE (Name -> Name
toNameIn Name
funBindingName) Exp -> Exp -> Exp
`AppE` Name -> Exp
VarE Name
range)
            Exp -> Exp -> Exp
`AppE` Name -> Exp
VarE Name
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 Type
body =
            [TyVarBndr Specificity] -> [Type] -> Type -> Type
ForallT
              (Name -> Specificity -> TyVarBndr Specificity
forall flag. Name -> flag -> TyVarBndr flag
PlainTV Name
outerScope Specificity
SpecifiedSpec TyVarBndr Specificity
-> [TyVarBndr Specificity] -> [TyVarBndr Specificity]
forall a. a -> [a] -> [a]
: (TyVarBndr BndrVis -> TyVarBndr Specificity)
-> [TyVarBndr BndrVis] -> [TyVarBndr Specificity]
forall a b. (a -> b) -> [a] -> [b]
map (Specificity
SpecifiedSpec Specificity -> TyVarBndr BndrVis -> TyVarBndr Specificity
forall a b. a -> TyVarBndr b -> TyVarBndr a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$) [TyVarBndr BndrVis]
tvars)
              [ Name -> Type
ConT ''Foil.Distinct Type -> Type -> Type
`AppT` Name -> Type
VarT Name
outerScope
              , Name -> Type
ConT ''Ord Type -> Type -> Type
`AppT` Type
rawIdentType ]
              Type
body
          plainSigTail =
                (Name -> Type
ConT ''Foil.Scope Type -> Type -> Type
`AppT` Name -> Type
VarT Name
outerScope)
                Type -> Type -> Type
--> (Name -> Type
ConT ''Map Type -> Type -> Type
`AppT` Type
rawIdentType Type -> Type -> Type
`AppT` (Name -> Type
ConT ''Foil.Name Type -> Type -> Type
`AppT` Name -> Type
VarT Name
outerScope))
                Type -> Type -> Type
--> Type
rawTermType
                Type -> Type -> Type
--> Type
termType
          trySigTail =
                (Name -> Type
ConT ''Foil.Scope Type -> Type -> Type
`AppT` Name -> Type
VarT Name
outerScope)
                Type -> Type -> Type
--> (Name -> Type
ConT ''Map Type -> Type -> Type
`AppT` Type
rawIdentType Type -> Type -> Type
`AppT` (Name -> Type
ConT ''Foil.Name Type -> Type -> Type
`AppT` Name -> Type
VarT Name
outerScope))
                Type -> Type -> Type
--> Type
rawTermType
                Type -> Type -> Type
--> Type
tryTermType
          tryWithSigTail =
                (Name -> Type
ConT ''Foil.Scope Type -> Type -> Type
`AppT` Name -> Type
VarT Name
outerScope)
                Type -> Type -> Type
--> (Name -> Type
ConT ''Map Type -> Type -> Type
`AppT` Type
rawIdentType Type -> Type -> Type
`AppT` (Name -> Type
ConT ''Foil.Name Type -> Type -> Type
`AppT` Name -> Type
VarT Name
outerScope))
                Type -> Type -> Type
--> (Name -> Type
ConT ''Map Type -> Type -> Type
`AppT` Type
rawIdentType Type -> Type -> Type
`AppT` Type
termType)
                Type -> Type -> Type
--> Type
rawTermType
                Type -> Type -> Type
--> Type
tryTermType
      forM_ [funName, tryFunName, tryWithFunName] $ \Name
name ->
        Q () -> Q ()
addModFinalizer (Q () -> Q ()) -> Q () -> Q ()
forall a b. (a -> b) -> a -> b
$ DocLoc -> String -> Q ()
putDoc (Name -> DocLoc
DeclDoc (Name -> Name
toNameIn Name
name))
          (String
"/Generated/ with '" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show 'mkFreeFoil String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"'. Same as '" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
nameBase Name
name String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"', 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 = Name -> Name
toNameIn Name
name
        ]

    mkConvertToSig :: Sort -> FreeFoilTermConfig -> Name -> Q [Dec]
mkConvertToSig Sort
sort termConfig :: FreeFoilTermConfig
termConfig@FreeFoilTermConfig{[Name]
Name
rawIdentName :: FreeFoilTermConfig -> Name
rawTermName :: FreeFoilTermConfig -> Name
rawBindingName :: FreeFoilTermConfig -> Name
rawScopeName :: FreeFoilTermConfig -> Name
rawVarConName :: FreeFoilTermConfig -> Name
rawSubTermNames :: FreeFoilTermConfig -> [Name]
rawSubScopeNames :: FreeFoilTermConfig -> [Name]
intToRawIdentName :: FreeFoilTermConfig -> Name
rawVarIdentToTermName :: FreeFoilTermConfig -> Name
rawTermToScopeName :: FreeFoilTermConfig -> Name
rawScopeToTermName :: FreeFoilTermConfig -> Name
rawIdentName :: Name
rawTermName :: Name
rawBindingName :: Name
rawScopeName :: Name
rawVarConName :: Name
rawSubTermNames :: [Name]
rawSubScopeNames :: [Name]
intToRawIdentName :: Name
rawVarIdentToTermName :: Name
rawTermToScopeName :: Name
rawScopeToTermName :: Name
..} Name
rawName = do
      (tvars, cons) <- Name -> Q ([TyVarBndr BndrVis], [Con])
reifyDataOrNewtype Name
rawName
      (itvars, _cons) <- reifyDataOrNewtype rawIdentName
      let rawSigName = FreeFoilConfig -> Name -> Name
toSignatureName FreeFoilConfig
config Name
rawName
          funName = FreeFoilConfig -> Name -> Name
toFreeFoilNameTo FreeFoilConfig
config Name
rawSigName
          rawType = Name -> [Type] -> Type
PeelConT Name
rawName ((TyVarBndr BndrVis -> Type) -> [TyVarBndr BndrVis] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (Name -> Type
VarT (Name -> Type)
-> (TyVarBndr BndrVis -> Name) -> TyVarBndr BndrVis -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyVarBndr BndrVis -> Name
forall a. TyVarBndr a -> Name
tvarName) [TyVarBndr BndrVis]
tvars)
          rawIdentType = Name -> [Type] -> Type
PeelConT Name
rawIdentName ((TyVarBndr BndrVis -> Type) -> [TyVarBndr BndrVis] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (Name -> Type
VarT (Name -> Type)
-> (TyVarBndr BndrVis -> Name) -> TyVarBndr BndrVis -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyVarBndr BndrVis -> Name
forall a. TyVarBndr a -> Name
tvarName) (Int -> [TyVarBndr BndrVis] -> [TyVarBndr BndrVis]
forall a. Int -> [a] -> [a]
take ([TyVarBndr BndrVis] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [TyVarBndr BndrVis]
itvars) [TyVarBndr BndrVis]
tvars)) -- FIXME: undocumented hack :(
          rawTermType = Name -> [Type] -> Type
PeelConT Name
rawTermName ((TyVarBndr BndrVis -> Type) -> [TyVarBndr BndrVis] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (Name -> Type
VarT (Name -> Type)
-> (TyVarBndr BndrVis -> Name) -> TyVarBndr BndrVis -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyVarBndr BndrVis -> Name
forall a. TyVarBndr a -> Name
tvarName) [TyVarBndr BndrVis]
tvars)
          rawScopedTermType = Name -> [Type] -> Type
PeelConT Name
rawScopeName ((TyVarBndr BndrVis -> Type) -> [TyVarBndr BndrVis] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (Name -> Type
VarT (Name -> Type)
-> (TyVarBndr BndrVis -> Name) -> TyVarBndr BndrVis -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyVarBndr BndrVis -> Name
forall a. TyVarBndr a -> Name
tvarName) [TyVarBndr BndrVis]
tvars)
          rawBindingType = Name -> [Type] -> Type
PeelConT Name
rawBindingName ((TyVarBndr BndrVis -> Type) -> [TyVarBndr BndrVis] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (Name -> Type
VarT (Name -> Type)
-> (TyVarBndr BndrVis -> Name) -> TyVarBndr BndrVis -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyVarBndr BndrVis -> Name
forall a. TyVarBndr a -> Name
tvarName) [TyVarBndr BndrVis]
tvars)
          rawScopeType = Int -> Type
TupleT Int
2 Type -> Type -> Type
`AppT` Type
rawBindingType Type -> Type -> Type
`AppT` Type
rawScopedTermType
      case toFreeFoilSigType SortSubTerm config rawScopeType rawTermType rawType of
        Just Type
safeType -> do
          let retType :: Type
retType = case Sort
sort of
                Sort
SortTerm -> Name -> Type
ConT ''Either Type -> Type -> Type
`AppT` Type
rawIdentType Type -> Type -> Type
`AppT` Type
safeType
                Sort
_        -> Type
safeType
          clauses <- [[Clause]] -> [Clause]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[Clause]] -> [Clause]) -> Q [[Clause]] -> Q [Clause]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Con -> Q [Clause]) -> [Con] -> Q [[Clause]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Sort
-> Type
-> FreeFoilConfig
-> FreeFoilTermConfig
-> Con
-> Q [Clause]
sigConToClause Sort
sort Type
rawType FreeFoilConfig
config FreeFoilTermConfig
termConfig) [Con]
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 ]
        Maybe Type
Nothing -> String -> Q [Dec]
forall a. HasCallStack => String -> a
error String
"impossible happened"

    mkConvertToBinding :: FreeFoilTermConfig -> Q [Dec]
mkConvertToBinding termConfig :: FreeFoilTermConfig
termConfig@FreeFoilTermConfig{[Name]
Name
rawIdentName :: FreeFoilTermConfig -> Name
rawTermName :: FreeFoilTermConfig -> Name
rawBindingName :: FreeFoilTermConfig -> Name
rawScopeName :: FreeFoilTermConfig -> Name
rawVarConName :: FreeFoilTermConfig -> Name
rawSubTermNames :: FreeFoilTermConfig -> [Name]
rawSubScopeNames :: FreeFoilTermConfig -> [Name]
intToRawIdentName :: FreeFoilTermConfig -> Name
rawVarIdentToTermName :: FreeFoilTermConfig -> Name
rawTermToScopeName :: FreeFoilTermConfig -> Name
rawScopeToTermName :: FreeFoilTermConfig -> Name
rawIdentName :: Name
rawTermName :: Name
rawBindingName :: Name
rawScopeName :: Name
rawVarConName :: Name
rawSubTermNames :: [Name]
rawSubScopeNames :: [Name]
intToRawIdentName :: Name
rawVarIdentToTermName :: Name
rawTermToScopeName :: Name
rawScopeToTermName :: Name
..} = do
      (tvars, cons) <- Name -> Q ([TyVarBndr BndrVis], [Con])
reifyDataOrNewtype Name
rawBindingName
      (itvars, _cons) <- reifyDataOrNewtype rawIdentName
      let funName = FreeFoilConfig -> Name -> Name
toFreeFoilNameTo FreeFoilConfig
config Name
rawBindingName
          rawBindingType = Name -> [Type] -> Type
PeelConT Name
rawBindingName ((TyVarBndr BndrVis -> Type) -> [TyVarBndr BndrVis] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (Name -> Type
VarT (Name -> Type)
-> (TyVarBndr BndrVis -> Name) -> TyVarBndr BndrVis -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyVarBndr BndrVis -> Name
forall a. TyVarBndr a -> Name
tvarName) [TyVarBndr BndrVis]
tvars)
          rawIdentType = Name -> [Type] -> Type
PeelConT Name
rawIdentName ((TyVarBndr BndrVis -> Type) -> [TyVarBndr BndrVis] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (Name -> Type
VarT (Name -> Type)
-> (TyVarBndr BndrVis -> Name) -> TyVarBndr BndrVis -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyVarBndr BndrVis -> Name
forall a. TyVarBndr a -> Name
tvarName) (Int -> [TyVarBndr BndrVis] -> [TyVarBndr BndrVis]
forall a. Int -> [a] -> [a]
take ([TyVarBndr BndrVis] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [TyVarBndr BndrVis]
itvars) [TyVarBndr BndrVis]
tvars)) -- FIXME: undocumented hack :(
          safeType = Sort -> FreeFoilConfig -> Type -> Type -> Type -> Type
toFreeFoilType Sort
SortBinder FreeFoilConfig
config (Name -> Type
VarT Name
outerScope) (Name -> Type
VarT Name
innerScope) Type
rawBindingType
      clauses <- concat <$> mapM (bindingConToClause rawBindingType config termConfig) cons
      r <- newName "r"
      let funInName = Name -> Name
toNameIn Name
funName
          bindingSigTail =
                (Name -> Type
ConT ''Foil.Scope Type -> Type -> Type
`AppT` Name -> Type
VarT Name
outerScope)
                Type -> Type -> Type
--> (Name -> Type
ConT ''Map Type -> Type -> Type
`AppT` Type
rawIdentType Type -> Type -> Type
`AppT` (Name -> Type
ConT ''Foil.Name Type -> Type -> Type
`AppT` Name -> Type
VarT Name
outerScope))
                Type -> Type -> Type
--> Type
rawBindingType
                Type -> Type -> Type
--> [TyVarBndr Specificity] -> [Type] -> Type -> Type
ForallT [Name -> Specificity -> TyVarBndr Specificity
forall flag. Name -> flag -> TyVarBndr flag
PlainTV Name
innerScope Specificity
SpecifiedSpec]
                      [Name -> Type
ConT ''Foil.DExt Type -> Type -> Type
`AppT` Name -> Type
VarT Name
outerScope Type -> Type -> Type
`AppT` Name -> Type
VarT Name
innerScope]
                      (Type
safeType
                        Type -> Type -> Type
--> (Name -> Type
ConT ''Map Type -> Type -> Type
`AppT` Type
rawIdentType Type -> Type -> Type
`AppT` (Name -> Type
ConT ''Foil.Name Type -> Type -> Type
`AppT` Name -> Type
VarT Name
innerScope))
                        Type -> Type -> Type
--> Name -> Type
VarT Name
r)
                Type -> Type -> Type
--> Name -> Type
VarT Name
r
          bindingForall Type
body =
            [TyVarBndr Specificity] -> [Type] -> Type -> Type
ForallT
              (Name -> Specificity -> TyVarBndr Specificity
forall flag. Name -> flag -> TyVarBndr flag
PlainTV Name
outerScope Specificity
SpecifiedSpec TyVarBndr Specificity
-> [TyVarBndr Specificity] -> [TyVarBndr Specificity]
forall a. a -> [a] -> [a]
: (TyVarBndr BndrVis -> TyVarBndr Specificity)
-> [TyVarBndr BndrVis] -> [TyVarBndr Specificity]
forall a b. (a -> b) -> [a] -> [b]
map (Specificity
SpecifiedSpec Specificity -> TyVarBndr BndrVis -> TyVarBndr Specificity
forall a b. a -> TyVarBndr b -> TyVarBndr a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$) [TyVarBndr BndrVis]
tvars [TyVarBndr Specificity]
-> [TyVarBndr Specificity] -> [TyVarBndr Specificity]
forall a. [a] -> [a] -> [a]
++ [Name -> Specificity -> TyVarBndr Specificity
forall flag. Name -> flag -> TyVarBndr flag
PlainTV Name
r Specificity
SpecifiedSpec])
              [ Name -> Type
ConT ''Foil.Distinct Type -> Type -> Type
`AppT` Name -> Type
VarT Name
outerScope
              , Name -> Type
ConT ''Ord Type -> Type -> Type
`AppT` Type
rawIdentType ]
              Type
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 :: Name -> Q [Dec]
mkConvertToQuantified Name
rawName = do
      (tvars, cons) <- Name -> Q ([TyVarBndr BndrVis], [Con])
reifyDataOrNewtype Name
rawName
      rawIdentNamesOfQuantifiedName rawName config >>= \case
        [] -> String -> Q [Dec]
forall a. HasCallStack => String -> a
error String
"unexpected: quantified type not connected to any known terms"
        [Name
rawIdentName'] -> do
          (itvars, _cons) <- Name -> Q ([TyVarBndr BndrVis], [Con])
reifyDataOrNewtype Name
rawIdentName'
          let funName = FreeFoilConfig -> Name -> Name
toFreeFoilNameTo FreeFoilConfig
config Name
rawName
              rawIdentType = Name -> [Type] -> Type
PeelConT Name
rawIdentName' ((TyVarBndr BndrVis -> Type) -> [TyVarBndr BndrVis] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (Name -> Type
VarT (Name -> Type)
-> (TyVarBndr BndrVis -> Name) -> TyVarBndr BndrVis -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyVarBndr BndrVis -> Name
forall a. TyVarBndr a -> Name
tvarName) (Int -> [TyVarBndr BndrVis] -> [TyVarBndr BndrVis]
forall a. Int -> [a] -> [a]
take ([TyVarBndr BndrVis] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [TyVarBndr BndrVis]
itvars) [TyVarBndr BndrVis]
tvars)) -- FIXME: undocumented hack :(
              rawType = Name -> [Type] -> Type
PeelConT Name
rawName ((TyVarBndr BndrVis -> Type) -> [TyVarBndr BndrVis] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (Name -> Type
VarT (Name -> Type)
-> (TyVarBndr BndrVis -> Name) -> TyVarBndr BndrVis -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyVarBndr BndrVis -> Name
forall a. TyVarBndr a -> Name
tvarName) [TyVarBndr BndrVis]
tvars)
              safeType = Sort -> FreeFoilConfig -> Type -> Type -> Type -> Type
toFreeFoilType Sort
SortTerm FreeFoilConfig
config (Name -> Type
VarT Name
outerScope) (Name -> Type
VarT Name
innerScope) Type
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
            ]
        [Name]
_ -> do
          -- error ("unsupported: more than one known term connected to the quantified type: " <> show rawName)
          [Dec] -> Q [Dec]
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return []

quantifiedConToClause :: Type -> FreeFoilConfig -> Con -> Q [Clause]
quantifiedConToClause :: Type -> FreeFoilConfig -> Con -> Q [Clause]
quantifiedConToClause Type
rawType config :: FreeFoilConfig
config@FreeFoilConfig{[Name]
[FreeFoilTermConfig]
String -> String
rawQuantifiedNames :: FreeFoilConfig -> [Name]
freeFoilTermConfigs :: FreeFoilConfig -> [FreeFoilTermConfig]
freeFoilNameModifier :: FreeFoilConfig -> String -> String
freeFoilScopeNameModifier :: FreeFoilConfig -> String -> String
signatureNameModifier :: FreeFoilConfig -> String -> String
freeFoilConNameModifier :: FreeFoilConfig -> String -> String
freeFoilConvertToName :: FreeFoilConfig -> String -> String
freeFoilConvertFromName :: FreeFoilConfig -> String -> String
rawQuantifiedNames :: [Name]
freeFoilTermConfigs :: [FreeFoilTermConfig]
freeFoilNameModifier :: String -> String
freeFoilScopeNameModifier :: String -> String
signatureNameModifier :: String -> String
freeFoilConNameModifier :: String -> String
freeFoilConvertToName :: String -> String
freeFoilConvertFromName :: String -> String
..} = Con -> Q [Clause]
go
  where
    goArgTypes :: Name -> Name -> Name -> Name -> [Type] -> Q ([Pat], [Exp], Exp -> Exp, Name, Name)
    goArgTypes :: Name
-> Name
-> Name
-> Name
-> [Type]
-> Q ([Pat], [Exp], Exp -> Exp, Name, Name)
goArgTypes Name
_theScope Name
_theEnv Name
scope Name
env [] = ([Pat], [Exp], Exp -> Exp, Name, Name)
-> Q ([Pat], [Exp], Exp -> Exp, Name, Name)
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return ([], [], Exp -> Exp
forall a. a -> a
id, Name
scope, Name
env)
    goArgTypes Name
theScope Name
theEnv Name
scope Name
env (Type
t:[Type]
ts) = case Type
t of
      PeelConT Name
typeName [Type]
_params
        | Name
typeName Name -> [Name] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` (FreeFoilTermConfig -> Name) -> [FreeFoilTermConfig] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map FreeFoilTermConfig -> Name
rawIdentName [FreeFoilTermConfig]
freeFoilTermConfigs -> do
            x <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"_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 FreeFoilTermConfig
_ <- Name -> [FreeFoilTermConfig] -> Maybe FreeFoilTermConfig
lookupBindingName Name
typeName [FreeFoilTermConfig]
freeFoilTermConfigs -> do
            x <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"_x"
            x' <- newName "_x'"
            scope' <- newName "_scope"
            env' <- newName "_env"
            let funName = FreeFoilConfig -> Name -> Name
toFreeFoilNameTo FreeFoilConfig
config Name
typeName
            (pats, exps, wrap, scope'', env'') <- goArgTypes theScope theEnv scope' env' ts
            return (VarP x : pats, VarE x' : exps, \Exp
e ->
              Name -> Exp
VarE Name
funName Exp -> Exp -> Exp
`AppE` Name -> Exp
VarE Name
scope Exp -> Exp -> Exp
`AppE` Name -> Exp
VarE Name
env Exp -> Exp -> Exp
`AppE` Name -> Exp
VarE Name
x Exp -> Exp -> Exp
`AppE`
                [Pat] -> Exp -> Exp
LamE [Name -> Pat
VarP Name
x', Name -> Pat
VarP Name
env']
                  ([Dec] -> Exp -> Exp
LetE [ Pat -> Body -> [Dec] -> Dec
ValD (Name -> Pat
VarP Name
scope') (Exp -> Body
NormalB (Name -> Exp
VarE 'Foil.extendScopePattern Exp -> Exp -> Exp
`AppE` Name -> Exp
VarE Name
x' Exp -> Exp -> Exp
`AppE` Name -> Exp
VarE Name
scope)) []]
                    (Exp -> Exp
wrap Exp
e)), scope'', env'')
        | Just FreeFoilTermConfig{[Name]
Name
rawIdentName :: FreeFoilTermConfig -> Name
rawTermName :: FreeFoilTermConfig -> Name
rawBindingName :: FreeFoilTermConfig -> Name
rawScopeName :: FreeFoilTermConfig -> Name
rawVarConName :: FreeFoilTermConfig -> Name
rawSubTermNames :: FreeFoilTermConfig -> [Name]
rawSubScopeNames :: FreeFoilTermConfig -> [Name]
intToRawIdentName :: FreeFoilTermConfig -> Name
rawVarIdentToTermName :: FreeFoilTermConfig -> Name
rawTermToScopeName :: FreeFoilTermConfig -> Name
rawScopeToTermName :: FreeFoilTermConfig -> Name
rawIdentName :: Name
rawTermName :: Name
rawBindingName :: Name
rawScopeName :: Name
rawVarConName :: Name
rawSubTermNames :: [Name]
rawSubScopeNames :: [Name]
intToRawIdentName :: Name
rawVarIdentToTermName :: Name
rawTermToScopeName :: Name
rawScopeToTermName :: Name
..} <- Name -> [FreeFoilTermConfig] -> Maybe FreeFoilTermConfig
lookupScopeName Name
typeName [FreeFoilTermConfig]
freeFoilTermConfigs -> do
            x <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"_x"
            let funName = FreeFoilConfig -> Name -> Name
toFreeFoilNameTo FreeFoilConfig
config Name
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 FreeFoilTermConfig
_ <- Name -> [FreeFoilTermConfig] -> Maybe FreeFoilTermConfig
lookupTermName Name
typeName [FreeFoilTermConfig]
freeFoilTermConfigs -> do
            let funName :: Name
funName = FreeFoilConfig -> Name -> Name
toFreeFoilNameTo FreeFoilConfig
config Name
typeName
            x <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"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 Type
_ (PeelConT Name
typeName [Type]
_params)
        | Just FreeFoilTermConfig
_ <- Name -> [FreeFoilTermConfig] -> Maybe FreeFoilTermConfig
lookupTermName Name
typeName [FreeFoilTermConfig]
freeFoilTermConfigs -> do
            let funName :: Name
funName = FreeFoilConfig -> Name -> Name
toFreeFoilNameTo FreeFoilConfig
config Name
typeName
            x <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"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 FreeFoilTermConfig
_ <- Name -> [FreeFoilTermConfig] -> Maybe FreeFoilTermConfig
lookupSubTermName Name
typeName [FreeFoilTermConfig]
freeFoilTermConfigs -> do
            let funName :: Name
funName = FreeFoilConfig -> Name -> Name
toFreeFoilNameTo FreeFoilConfig
config Name
typeName
            x <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"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 FreeFoilTermConfig
_ <- Name -> [FreeFoilTermConfig] -> Maybe FreeFoilTermConfig
lookupSubScopeName Name
typeName [FreeFoilTermConfig]
freeFoilTermConfigs -> do
            let funName :: Name
funName = FreeFoilConfig -> Name -> Name
toFreeFoilNameTo FreeFoilConfig
config Name
typeName
            x <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"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{[Name]
Name
rawIdentName :: FreeFoilTermConfig -> Name
rawTermName :: FreeFoilTermConfig -> Name
rawBindingName :: FreeFoilTermConfig -> Name
rawScopeName :: FreeFoilTermConfig -> Name
rawVarConName :: FreeFoilTermConfig -> Name
rawSubTermNames :: FreeFoilTermConfig -> [Name]
rawSubScopeNames :: FreeFoilTermConfig -> [Name]
intToRawIdentName :: FreeFoilTermConfig -> Name
rawVarIdentToTermName :: FreeFoilTermConfig -> Name
rawTermToScopeName :: FreeFoilTermConfig -> Name
rawScopeToTermName :: FreeFoilTermConfig -> Name
rawIdentName :: Name
rawTermName :: Name
rawBindingName :: Name
rawScopeName :: Name
rawVarConName :: Name
rawSubTermNames :: [Name]
rawSubScopeNames :: [Name]
intToRawIdentName :: Name
rawVarIdentToTermName :: Name
rawTermToScopeName :: Name
rawScopeToTermName :: Name
..} <- Name -> [FreeFoilTermConfig] -> Maybe FreeFoilTermConfig
lookupScopeName Name
typeName [FreeFoilTermConfig]
freeFoilTermConfigs -> do
            let funName :: Name
funName = FreeFoilConfig -> Name -> Name
toFreeFoilNameTo FreeFoilConfig
config Name
rawTermName
            x <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"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')
      Type
_ -> do
        x <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"_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 :: Con -> Q [Clause]
go = \case
      GadtC [Name]
conNames [BangType]
rawArgTypes Type
_rawRetType -> [[Clause]] -> [Clause]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[Clause]] -> [Clause]) -> Q [[Clause]] -> Q [Clause]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
        scope <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"_scope"
        env <- newName "_env"
        forM conNames $ \Name
conName -> do
          let newConName :: Name
newConName = FreeFoilConfig -> Name -> Name
toConName FreeFoilConfig
config Name
conName
          (pats, exps, wrap, _scope', _env') <- Name
-> Name
-> Name
-> Name
-> [Type]
-> Q ([Pat], [Exp], Exp -> Exp, Name, Name)
goArgTypes Name
scope Name
env Name
scope Name
env ((BangType -> Type) -> [BangType] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map BangType -> Type
forall a b. (a, b) -> b
snd [BangType]
rawArgTypes)
          return
            [ Clause [VarP scope, VarP env, ConP conName [] pats]
                (NormalB (wrap (foldl AppE (ConE newConName) exps))) [] ]
      NormalC Name
conName [BangType]
types -> Con -> Q [Clause]
go ([Name] -> [BangType] -> Type -> Con
GadtC [Name
conName] [BangType]
types Type
rawType)
      RecC Name
conName [VarBangType]
types -> Con -> Q [Clause]
go (Name -> [BangType] -> Con
NormalC Name
conName ((VarBangType -> BangType) -> [VarBangType] -> [BangType]
forall a b. (a -> b) -> [a] -> [b]
map VarBangType -> BangType
removeName [VarBangType]
types))
      InfixC BangType
l Name
conName BangType
r -> Con -> Q [Clause]
go ([Name] -> [BangType] -> Type -> Con
GadtC [Name
conName] [BangType
l, BangType
r] Type
rawType)
      ForallC [TyVarBndr Specificity]
_params [Type]
_ctx Con
con -> Con -> Q [Clause]
go Con
con
      RecGadtC [Name]
conNames [VarBangType]
argTypes Type
retType -> Con -> Q [Clause]
go ([Name] -> [BangType] -> Type -> Con
GadtC [Name]
conNames ((VarBangType -> BangType) -> [VarBangType] -> [BangType]
forall a b. (a -> b) -> [a] -> [b]
map VarBangType -> BangType
removeName [VarBangType]
argTypes) Type
retType)

subTermConToClause :: Type -> FreeFoilConfig -> FreeFoilTermConfig -> Con -> Q [Clause]
subTermConToClause :: Type -> FreeFoilConfig -> FreeFoilTermConfig -> Con -> Q [Clause]
subTermConToClause Type
rawType FreeFoilConfig
config FreeFoilTermConfig{[Name]
Name
rawIdentName :: FreeFoilTermConfig -> Name
rawTermName :: FreeFoilTermConfig -> Name
rawBindingName :: FreeFoilTermConfig -> Name
rawScopeName :: FreeFoilTermConfig -> Name
rawVarConName :: FreeFoilTermConfig -> Name
rawSubTermNames :: FreeFoilTermConfig -> [Name]
rawSubScopeNames :: FreeFoilTermConfig -> [Name]
intToRawIdentName :: FreeFoilTermConfig -> Name
rawVarIdentToTermName :: FreeFoilTermConfig -> Name
rawTermToScopeName :: FreeFoilTermConfig -> Name
rawScopeToTermName :: FreeFoilTermConfig -> Name
rawIdentName :: Name
rawTermName :: Name
rawBindingName :: Name
rawScopeName :: Name
rawVarConName :: Name
rawSubTermNames :: [Name]
rawSubScopeNames :: [Name]
intToRawIdentName :: Name
rawVarIdentToTermName :: Name
rawTermToScopeName :: Name
rawScopeToTermName :: Name
..} = Con -> Q [Clause]
go
  where
    goArgTypes :: Name -> Name -> [Type] -> Q ([Pat], [Exp], Exp -> Exp, Name, Name)
    goArgTypes :: Name -> Name -> [Type] -> Q ([Pat], [Exp], Exp -> Exp, Name, Name)
goArgTypes Name
scope Name
env [] = ([Pat], [Exp], Exp -> Exp, Name, Name)
-> Q ([Pat], [Exp], Exp -> Exp, Name, Name)
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return ([], [], Exp -> Exp
forall a. a -> a
id, Name
scope, Name
env)
    goArgTypes Name
scope Name
env (Type
t:[Type]
ts) = case Type
t of
      PeelConT Name
typeName [Type]
_params
        | Name
typeName Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
rawBindingName -> do
            x <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"_x"
            x' <- newName "_x'"
            scope' <- newName "_scope"
            env' <- newName "_env"
            let funName = FreeFoilConfig -> Name -> Name
toFreeFoilNameTo FreeFoilConfig
config Name
typeName
            (pats, exps, wrap, scope'', env'') <- goArgTypes scope' env' ts
            return (VarP x : pats, VarE x' : exps, \Exp
e ->
              Name -> Exp
VarE Name
funName Exp -> Exp -> Exp
`AppE` Name -> Exp
VarE Name
scope Exp -> Exp -> Exp
`AppE` Name -> Exp
VarE Name
env Exp -> Exp -> Exp
`AppE` Name -> Exp
VarE Name
x Exp -> Exp -> Exp
`AppE`
                [Pat] -> Exp -> Exp
LamE [Name -> Pat
VarP Name
x', Name -> Pat
VarP Name
env']
                  ([Dec] -> Exp -> Exp
LetE [ Pat -> Body -> [Dec] -> Dec
ValD (Name -> Pat
VarP Name
scope') (Exp -> Body
NormalB (Name -> Exp
VarE 'Foil.extendScopePattern Exp -> Exp -> Exp
`AppE` Name -> Exp
VarE Name
x' Exp -> Exp -> Exp
`AppE` Name -> Exp
VarE Name
scope)) []]
                    (Exp -> Exp
wrap Exp
e)), scope'', env'')
        | Name
typeName Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
rawScopeName -> do
            x <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"_x"
            let funName = FreeFoilConfig -> Name -> Name
toFreeFoilNameTo FreeFoilConfig
config Name
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')
        | Name
typeName Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
rawTermName -> do
            x <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"_x"
            let funName = FreeFoilConfig -> Name -> Name
toFreeFoilNameTo FreeFoilConfig
config Name
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')
        | Name
typeName Name -> [Name] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
rawSubTermNames -> do
            x <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"_x"
            let funName = FreeFoilConfig -> Name -> Name
toFreeFoilNameTo FreeFoilConfig
config Name
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 Type
_ (PeelConT Name
typeName [Type]
_params)
        | Name
typeName Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
rawTermName -> do
            let funName :: Name
funName = FreeFoilConfig -> Name -> Name
toFreeFoilNameTo FreeFoilConfig
config Name
typeName
            x <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"_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')
        | Name
typeName Name -> [Name] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
rawSubTermNames -> do
            let rawSigName :: Name
rawSigName = FreeFoilConfig -> Name -> Name
toSignatureName FreeFoilConfig
config Name
typeName
                funName :: Name
funName = FreeFoilConfig -> Name -> Name
toFreeFoilNameTo FreeFoilConfig
config Name
rawSigName
            x <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"_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')
        | Name
typeName Name -> [Name] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
rawSubScopeNames -> do
            let rawSigName :: Name
rawSigName = FreeFoilConfig -> Name -> Name
toSignatureName FreeFoilConfig
config Name
typeName
                funName :: Name
funName = FreeFoilConfig -> Name -> Name
toFreeFoilNameTo FreeFoilConfig
config Name
rawSigName
            x <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"_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')
      Type
_ -> do
        x <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"_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 :: Con -> Q [Clause]
go = \case
      GadtC [Name]
conNames [BangType]
rawArgTypes Type
_rawRetType -> [[Clause]] -> [Clause]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[Clause]] -> [Clause]) -> Q [[Clause]] -> Q [Clause]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
        scope <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"_scope"
        env <- newName "_env"
        forM conNames $ \Name
conName -> do
          let newConName :: Name
newConName = FreeFoilConfig -> Name -> Name
toConName FreeFoilConfig
config Name
conName
          (pats, exps, wrap, _scope', _env') <- Name -> Name -> [Type] -> Q ([Pat], [Exp], Exp -> Exp, Name, Name)
goArgTypes Name
scope Name
env ((BangType -> Type) -> [BangType] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map BangType -> Type
forall a b. (a, b) -> b
snd [BangType]
rawArgTypes)
          return
            [ Clause [VarP scope, VarP env, ConP conName [] pats]
                (NormalB (wrap (foldl AppE (ConE newConName) exps))) [] ]
      NormalC Name
conName [BangType]
types -> Con -> Q [Clause]
go ([Name] -> [BangType] -> Type -> Con
GadtC [Name
conName] [BangType]
types Type
rawType)
      RecC Name
conName [VarBangType]
types -> Con -> Q [Clause]
go (Name -> [BangType] -> Con
NormalC Name
conName ((VarBangType -> BangType) -> [VarBangType] -> [BangType]
forall a b. (a -> b) -> [a] -> [b]
map VarBangType -> BangType
removeName [VarBangType]
types))
      InfixC BangType
l Name
conName BangType
r -> Con -> Q [Clause]
go ([Name] -> [BangType] -> Type -> Con
GadtC [Name
conName] [BangType
l, BangType
r] Type
rawType)
      ForallC [TyVarBndr Specificity]
_params [Type]
_ctx Con
con -> Con -> Q [Clause]
go Con
con
      RecGadtC [Name]
conNames [VarBangType]
argTypes Type
retType -> Con -> Q [Clause]
go ([Name] -> [BangType] -> Type -> Con
GadtC [Name]
conNames ((VarBangType -> BangType) -> [VarBangType] -> [BangType]
forall a b. (a -> b) -> [a] -> [b]
map VarBangType -> BangType
removeName [VarBangType]
argTypes) Type
retType)

bindingConToClause :: Type -> FreeFoilConfig -> FreeFoilTermConfig -> Con -> Q [Clause]
bindingConToClause :: Type -> FreeFoilConfig -> FreeFoilTermConfig -> Con -> Q [Clause]
bindingConToClause Type
rawType FreeFoilConfig
config FreeFoilTermConfig{[Name]
Name
rawIdentName :: FreeFoilTermConfig -> Name
rawTermName :: FreeFoilTermConfig -> Name
rawBindingName :: FreeFoilTermConfig -> Name
rawScopeName :: FreeFoilTermConfig -> Name
rawVarConName :: FreeFoilTermConfig -> Name
rawSubTermNames :: FreeFoilTermConfig -> [Name]
rawSubScopeNames :: FreeFoilTermConfig -> [Name]
intToRawIdentName :: FreeFoilTermConfig -> Name
rawVarIdentToTermName :: FreeFoilTermConfig -> Name
rawTermToScopeName :: FreeFoilTermConfig -> Name
rawScopeToTermName :: FreeFoilTermConfig -> Name
rawIdentName :: Name
rawTermName :: Name
rawBindingName :: Name
rawScopeName :: Name
rawVarConName :: Name
rawSubTermNames :: [Name]
rawSubScopeNames :: [Name]
intToRawIdentName :: Name
rawVarIdentToTermName :: Name
rawTermToScopeName :: Name
rawScopeToTermName :: Name
..} = Con -> Q [Clause]
go
  where
    goArgTypes :: Name -> Name -> Name -> [Type] -> Q ([Pat], [Exp], Exp -> Exp, Name)
    goArgTypes :: Name
-> Name -> Name -> [Type] -> Q ([Pat], [Exp], Exp -> Exp, Name)
goArgTypes Name
_range Name
_scope Name
env [] = ([Pat], [Exp], Exp -> Exp, Name)
-> Q ([Pat], [Exp], Exp -> Exp, Name)
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return ([], [], Exp -> Exp
forall a. a -> a
id, Name
env)
    goArgTypes Name
range Name
scope Name
env (Type
t:[Type]
ts) = case Type
t of
      PeelConT Name
typeName [Type]
_params
        | Name
typeName Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
rawIdentName -> do
            x <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"_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, \Exp
e ->
              Name -> Exp
VarE 'Foil.withFreshIn Exp -> Exp -> Exp
`AppE` Name -> Exp
VarE Name
range Exp -> Exp -> Exp
`AppE` Name -> Exp
VarE Name
scope Exp -> Exp -> Exp
`AppE`
                [Pat] -> Exp -> Exp
LamE [Name -> Pat
VarP Name
x']
                  ([Dec] -> Exp -> Exp
LetE [ Pat -> Body -> [Dec] -> Dec
ValD (Name -> Pat
VarP Name
scope') (Exp -> Body
NormalB (Name -> Exp
VarE 'Foil.extendScope Exp -> Exp -> Exp
`AppE` Name -> Exp
VarE Name
x' Exp -> Exp -> Exp
`AppE` Name -> Exp
VarE Name
scope)) []
                        , Pat -> Body -> [Dec] -> Dec
ValD (Name -> Pat
VarP Name
env') (Exp -> Body
NormalB (Name -> Exp
VarE 'Map.insert Exp -> Exp -> Exp
`AppE` Name -> Exp
VarE Name
x Exp -> Exp -> Exp
`AppE` (Name -> Exp
VarE 'Foil.nameOf Exp -> Exp -> Exp
`AppE` Name -> Exp
VarE Name
x') Exp -> Exp -> Exp
`AppE` (Name -> Exp
VarE 'fmap Exp -> Exp -> Exp
`AppE` Name -> Exp
VarE 'Foil.sink Exp -> Exp -> Exp
`AppE` Name -> Exp
VarE Name
env))) []]
                    (Exp -> Exp
wrap Exp
e)), env'')
        | Name
typeName Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
rawBindingName -> do
            x <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"_x"
            x' <- newName "_x'"
            scope' <- newName "_scope"
            env' <- newName "_env"
            let funName = Name -> Name
toNameIn (FreeFoilConfig -> Name -> Name
toFreeFoilNameTo FreeFoilConfig
config Name
typeName)
            (pats, exps, wrap, env'') <- goArgTypes range scope' env' ts
            return (VarP x : pats, VarE x' : exps, \Exp
e ->
              Name -> Exp
VarE Name
funName Exp -> Exp -> Exp
`AppE` Name -> Exp
VarE Name
range Exp -> Exp -> Exp
`AppE` Name -> Exp
VarE Name
scope Exp -> Exp -> Exp
`AppE` Name -> Exp
VarE Name
env Exp -> Exp -> Exp
`AppE` Name -> Exp
VarE Name
x Exp -> Exp -> Exp
`AppE`
                [Pat] -> Exp -> Exp
LamE [Name -> Pat
VarP Name
x', Name -> Pat
VarP Name
env']
                  ([Dec] -> Exp -> Exp
LetE [ Pat -> Body -> [Dec] -> Dec
ValD (Name -> Pat
VarP Name
scope') (Exp -> Body
NormalB (Name -> Exp
VarE 'Foil.extendScopePattern Exp -> Exp -> Exp
`AppE` Name -> Exp
VarE Name
x' Exp -> Exp -> Exp
`AppE` Name -> Exp
VarE Name
scope)) []]
                    (Exp -> Exp
wrap Exp
e)), env'')
      Type
_ -> do
        x <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"_x"
        (pats, exps, wrap, env') <- goArgTypes range scope env ts
        return (VarP x : pats, VarE x : exps, wrap, env')

    go :: Con -> Q [Clause]
    go :: Con -> Q [Clause]
go = \case
      GadtC [Name]
conNames [BangType]
rawArgTypes Type
_rawRetType -> [[Clause]] -> [Clause]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[Clause]] -> [Clause]) -> Q [[Clause]] -> Q [Clause]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
        range <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"_range"
        scope <- newName "_scope"
        env <- newName "_env"
        cont <- newName "_cont"
        forM conNames $ \Name
conName -> do
          let newConName :: Name
newConName = FreeFoilConfig -> Name -> Name
toConName FreeFoilConfig
config Name
conName
          (pats, exps, wrap, env') <- Name
-> Name -> Name -> [Type] -> Q ([Pat], [Exp], Exp -> Exp, Name)
goArgTypes Name
range Name
scope Name
env ((BangType -> Type) -> [BangType] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map BangType -> Type
forall a b. (a, b) -> b
snd [BangType]
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 Name
conName [BangType]
types -> Con -> Q [Clause]
go ([Name] -> [BangType] -> Type -> Con
GadtC [Name
conName] [BangType]
types Type
rawType)
      RecC Name
conName [VarBangType]
types -> Con -> Q [Clause]
go (Name -> [BangType] -> Con
NormalC Name
conName ((VarBangType -> BangType) -> [VarBangType] -> [BangType]
forall a b. (a -> b) -> [a] -> [b]
map VarBangType -> BangType
removeName [VarBangType]
types))
      InfixC BangType
l Name
conName BangType
r -> Con -> Q [Clause]
go ([Name] -> [BangType] -> Type -> Con
GadtC [Name
conName] [BangType
l, BangType
r] Type
rawType)
      ForallC [TyVarBndr Specificity]
_params [Type]
_ctx Con
con -> Con -> Q [Clause]
go Con
con
      RecGadtC [Name]
conNames [VarBangType]
argTypes Type
retType -> Con -> Q [Clause]
go ([Name] -> [BangType] -> Type -> Con
GadtC [Name]
conNames ((VarBangType -> BangType) -> [VarBangType] -> [BangType]
forall a b. (a -> b) -> [a] -> [b]
map VarBangType -> BangType
removeName [VarBangType]
argTypes) Type
retType)


sigConToClause :: Sort -> Type -> FreeFoilConfig -> FreeFoilTermConfig -> Con -> Q [Clause]
sigConToClause :: Sort
-> Type
-> FreeFoilConfig
-> FreeFoilTermConfig
-> Con
-> Q [Clause]
sigConToClause Sort
sort Type
rawRetType config :: FreeFoilConfig
config@FreeFoilConfig{[Name]
[FreeFoilTermConfig]
String -> String
rawQuantifiedNames :: FreeFoilConfig -> [Name]
freeFoilTermConfigs :: FreeFoilConfig -> [FreeFoilTermConfig]
freeFoilNameModifier :: FreeFoilConfig -> String -> String
freeFoilScopeNameModifier :: FreeFoilConfig -> String -> String
signatureNameModifier :: FreeFoilConfig -> String -> String
freeFoilConNameModifier :: FreeFoilConfig -> String -> String
freeFoilConvertToName :: FreeFoilConfig -> String -> String
freeFoilConvertFromName :: FreeFoilConfig -> String -> String
rawQuantifiedNames :: [Name]
freeFoilTermConfigs :: [FreeFoilTermConfig]
freeFoilNameModifier :: String -> String
freeFoilScopeNameModifier :: String -> String
signatureNameModifier :: String -> String
freeFoilConNameModifier :: String -> String
freeFoilConvertToName :: String -> String
freeFoilConvertFromName :: String -> String
..} FreeFoilTermConfig{[Name]
Name
rawIdentName :: FreeFoilTermConfig -> Name
rawTermName :: FreeFoilTermConfig -> Name
rawBindingName :: FreeFoilTermConfig -> Name
rawScopeName :: FreeFoilTermConfig -> Name
rawVarConName :: FreeFoilTermConfig -> Name
rawSubTermNames :: FreeFoilTermConfig -> [Name]
rawSubScopeNames :: FreeFoilTermConfig -> [Name]
intToRawIdentName :: FreeFoilTermConfig -> Name
rawVarIdentToTermName :: FreeFoilTermConfig -> Name
rawTermToScopeName :: FreeFoilTermConfig -> Name
rawScopeToTermName :: FreeFoilTermConfig -> Name
rawIdentName :: Name
rawTermName :: Name
rawBindingName :: Name
rawScopeName :: Name
rawVarConName :: Name
rawSubTermNames :: [Name]
rawSubScopeNames :: [Name]
intToRawIdentName :: Name
rawVarIdentToTermName :: Name
rawTermToScopeName :: Name
rawScopeToTermName :: Name
..} = Con -> Q [Clause]
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 :: Bool -> Name -> Name -> Type -> Q ([Pat], [Exp])
fromRawArgType Bool
isVarCon Name
theIdent Name
theBinder Type
rawArgType
      | FreeFoilConfig -> Type -> Bool
isBindingField FreeFoilConfig
config Type
rawArgType = ([Pat], [Exp]) -> Q ([Pat], [Exp])
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Name -> Pat
VarP Name
theBinder], [])
      | FreeFoilConfig -> Type -> Bool
isScopeField FreeFoilConfig
config Type
rawArgType = do
          body <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"body"
          return ([VarP body], [TupE [Just (VarE theBinder), Just (VarE body)]])
      | Bool
otherwise = Bool -> Name -> Type -> Q ([Pat], [Exp])
fromArgType Bool
isVarCon Name
theIdent Type
rawArgType

    fromArgType :: Bool -> Name -> Type -> Q ([Pat], [Exp])
    fromArgType :: Bool -> Name -> Type -> Q ([Pat], [Exp])
fromArgType Bool
isVarCon Name
theIdent = \case
      PeelConT Name
typeName [Type]
_params
        | Name
typeName Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
rawIdentName, Sort
SortTerm <- Sort
sort, Bool
isVarCon -> do
            ([Pat], [Exp]) -> Q ([Pat], [Exp])
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Name -> Pat
VarP Name
theIdent], [Name -> Exp
VarE Name
theIdent])
        | Just FreeFoilTermConfig
_ <- Name -> [FreeFoilTermConfig] -> Maybe FreeFoilTermConfig
lookupBindingName Name
typeName [FreeFoilTermConfig]
freeFoilTermConfigs -> do
            ([Pat], [Exp]) -> Q ([Pat], [Exp])
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return ([], [])
        | Just FreeFoilTermConfig
_ <- Name -> [FreeFoilTermConfig] -> Maybe FreeFoilTermConfig
lookupScopeName Name
typeName [FreeFoilTermConfig]
freeFoilTermConfigs -> do
            binder <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"binder"
            body <- newName "body"
            return ([VarP binder, VarP body], [TupE [Just (VarE binder), Just (VarE body)]])
        | Just FreeFoilTermConfig
_ <- Name -> [FreeFoilTermConfig] -> Maybe FreeFoilTermConfig
lookupSubTermName Name
typeName [FreeFoilTermConfig]
freeFoilTermConfigs -> do
            let rawSigName :: Name
rawSigName = FreeFoilConfig -> Name -> Name
toSignatureName FreeFoilConfig
config Name
typeName
                funName :: Name
funName = FreeFoilConfig -> Name -> Name
toFreeFoilNameTo FreeFoilConfig
config Name
rawSigName
            x <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"_x"
            return ([VarP x], [AppE (VarE funName) (VarE x)])
        | Just FreeFoilTermConfig
_ <- Name -> [FreeFoilTermConfig] -> Maybe FreeFoilTermConfig
lookupSubScopeName Name
typeName [FreeFoilTermConfig]
freeFoilTermConfigs -> do
            let rawSigName :: Name
rawSigName = FreeFoilConfig -> Name -> Name
toSignatureName FreeFoilConfig
config Name
typeName
                funName :: Name
funName = FreeFoilConfig -> Name -> Name
toFreeFoilNameTo FreeFoilConfig
config Name
rawSigName
            x <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"_x"
            return ([VarP x], [AppE (VarE funName) (VarE x)])
      AppT Type
_ (PeelConT Name
typeName [Type]
_params)
        | Just FreeFoilTermConfig
_ <- Name -> [FreeFoilTermConfig] -> Maybe FreeFoilTermConfig
lookupSubTermName Name
typeName [FreeFoilTermConfig]
freeFoilTermConfigs -> do
            let rawSigName :: Name
rawSigName = FreeFoilConfig -> Name -> Name
toSignatureName FreeFoilConfig
config Name
typeName
                funName :: Name
funName = FreeFoilConfig -> Name -> Name
toFreeFoilNameTo FreeFoilConfig
config Name
rawSigName
            x <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"_x"
            return ([VarP x], [AppE (AppE (VarE 'fmap) (VarE funName)) (VarE x)])
        | Just FreeFoilTermConfig
_ <- Name -> [FreeFoilTermConfig] -> Maybe FreeFoilTermConfig
lookupSubScopeName Name
typeName [FreeFoilTermConfig]
freeFoilTermConfigs -> do
            let rawSigName :: Name
rawSigName = FreeFoilConfig -> Name -> Name
toSignatureName FreeFoilConfig
config Name
typeName
                funName :: Name
funName = FreeFoilConfig -> Name -> Name
toFreeFoilNameTo FreeFoilConfig
config Name
rawSigName
            x <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"_x"
            return ([VarP x], [AppE (AppE (VarE 'fmap) (VarE funName)) (VarE x)])
      Type
_ -> do
        x <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"_x"
        return ([VarP x], [VarE x])

    go :: Con -> Q [Clause]
    go :: Con -> Q [Clause]
go = \case
      GadtC [Name]
conNames [BangType]
rawArgTypes Type
_rawRetType -> [[Clause]] -> [Clause]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[Clause]] -> [Clause]) -> Q [[Clause]] -> Q [Clause]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
        theIdent <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"_theRawIdent"
        theBinder <- newName "binder"
        forM conNames $ \Name
conName -> do
          let newConName :: Name
newConName = FreeFoilConfig -> Name -> Name
toSignatureName FreeFoilConfig
config Name
conName
              isVarCon :: Bool
isVarCon = Name
conName Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
rawVarConName
          (concat -> pats, concat -> exps) <- [([Pat], [Exp])] -> ([[Pat]], [[Exp]])
forall a b. [(a, b)] -> ([a], [b])
unzip ([([Pat], [Exp])] -> ([[Pat]], [[Exp]]))
-> Q [([Pat], [Exp])] -> Q ([[Pat]], [[Exp]])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
            (BangType -> Q ([Pat], [Exp])) -> [BangType] -> Q [([Pat], [Exp])]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Bool -> Name -> Name -> Type -> Q ([Pat], [Exp])
fromRawArgType Bool
isVarCon Name
theIdent Name
theBinder (Type -> Q ([Pat], [Exp]))
-> (BangType -> Type) -> BangType -> Q ([Pat], [Exp])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BangType -> Type
forall a b. (a, b) -> b
snd) [BangType]
rawArgTypes
          case sort of
            Sort
SortTerm
              | Bool
isVarCon -> [Clause] -> Q [Clause]
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return
                  [ [Pat] -> Body -> [Dec] -> Clause
Clause [Name -> [Type] -> [Pat] -> Pat
ConP Name
conName [] [Pat]
pats] (Exp -> Body
NormalB (Name -> Exp
ConE 'Left Exp -> Exp -> Exp
`AppE` Name -> Exp
VarE Name
theIdent)) [] ]  -- FIXME!
              | Bool
otherwise -> [Clause] -> Q [Clause]
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return
                  [ [Pat] -> Body -> [Dec] -> Clause
Clause [Name -> [Type] -> [Pat] -> Pat
ConP Name
conName [] [Pat]
pats] (Exp -> Body
NormalB (Name -> Exp
ConE 'Right Exp -> Exp -> Exp
`AppE` ((Exp -> Exp -> Exp) -> Exp -> [Exp] -> Exp
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Exp -> Exp -> Exp
AppE (Name -> Exp
ConE Name
newConName) [Exp]
exps))) [] ]
            Sort
_ -> [Clause] -> Q [Clause]
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return
              [ [Pat] -> Body -> [Dec] -> Clause
Clause [Name -> [Type] -> [Pat] -> Pat
ConP Name
conName [] [Pat]
pats] (Exp -> Body
NormalB ((Exp -> Exp -> Exp) -> Exp -> [Exp] -> Exp
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Exp -> Exp -> Exp
AppE (Name -> Exp
ConE Name
newConName) [Exp]
exps)) [] ]
      NormalC Name
conName [BangType]
types -> Con -> Q [Clause]
go ([Name] -> [BangType] -> Type -> Con
GadtC [Name
conName] [BangType]
types Type
rawRetType)
      RecC Name
conName [VarBangType]
types -> Con -> Q [Clause]
go (Name -> [BangType] -> Con
NormalC Name
conName ((VarBangType -> BangType) -> [VarBangType] -> [BangType]
forall a b. (a -> b) -> [a] -> [b]
map VarBangType -> BangType
removeName [VarBangType]
types))
      InfixC BangType
l Name
conName BangType
r -> Con -> Q [Clause]
go ([Name] -> [BangType] -> Type -> Con
GadtC [Name
conName] [BangType
l, BangType
r] Type
rawRetType)
      ForallC [TyVarBndr Specificity]
_params [Type]
_ctx Con
con -> Con -> Q [Clause]
go Con
con
      RecGadtC [Name]
conNames [VarBangType]
argTypes Type
retType -> Con -> Q [Clause]
go ([Name] -> [BangType] -> Type -> Con
GadtC [Name]
conNames ((VarBangType -> BangType) -> [VarBangType] -> [BangType]
forall a b. (a -> b) -> [a] -> [b]
map VarBangType -> BangType
removeName [VarBangType]
argTypes) Type
retType)

rawIdentNamesOfQuantifiedName :: Name -> FreeFoilConfig -> Q [Name]
rawIdentNamesOfQuantifiedName :: Name -> FreeFoilConfig -> Q [Name]
rawIdentNamesOfQuantifiedName Name
rawName FreeFoilConfig
config = do
  (_tvars, cons) <- Name -> Q ([TyVarBndr BndrVis], [Con])
reifyDataOrNewtype Name
rawName
  return (nub (concatMap go cons))
  where
    rawRetType :: a
rawRetType = String -> a
forall a. HasCallStack => String -> a
error String
"impossible happened!"

    go :: Con -> [Name]
    go :: Con -> [Name]
go = \case
      GadtC [Name]
_conNames [BangType]
rawArgTypes Type
_rawRetType ->
        (BangType -> [Name]) -> [BangType] -> [Name]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (FreeFoilConfig -> Type -> [Name]
rawIdentNamesOfType FreeFoilConfig
config (Type -> [Name]) -> (BangType -> Type) -> BangType -> [Name]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BangType -> Type
forall a b. (a, b) -> b
snd) [BangType]
rawArgTypes
      NormalC Name
conName [BangType]
types -> Con -> [Name]
go ([Name] -> [BangType] -> Type -> Con
GadtC [Name
conName] [BangType]
types Type
forall {a}. a
rawRetType)
      RecC Name
conName [VarBangType]
types -> Con -> [Name]
go (Name -> [BangType] -> Con
NormalC Name
conName ((VarBangType -> BangType) -> [VarBangType] -> [BangType]
forall a b. (a -> b) -> [a] -> [b]
map VarBangType -> BangType
removeName [VarBangType]
types))
      InfixC BangType
l Name
conName BangType
r -> Con -> [Name]
go ([Name] -> [BangType] -> Type -> Con
GadtC [Name
conName] [BangType
l, BangType
r] Type
forall {a}. a
rawRetType)
      ForallC [TyVarBndr Specificity]
_params [Type]
_ctx Con
con -> Con -> [Name]
go Con
con
      RecGadtC [Name]
conNames [VarBangType]
argTypes Type
retType -> Con -> [Name]
go ([Name] -> [BangType] -> Type -> Con
GadtC [Name]
conNames ((VarBangType -> BangType) -> [VarBangType] -> [BangType]
forall a b. (a -> b) -> [a] -> [b]
map VarBangType -> BangType
removeName [VarBangType]
argTypes) Type
retType)

rawIdentNamesOfType :: FreeFoilConfig -> Type -> [Name]
rawIdentNamesOfType :: FreeFoilConfig -> Type -> [Name]
rawIdentNamesOfType FreeFoilConfig{[Name]
[FreeFoilTermConfig]
String -> String
rawQuantifiedNames :: FreeFoilConfig -> [Name]
freeFoilTermConfigs :: FreeFoilConfig -> [FreeFoilTermConfig]
freeFoilNameModifier :: FreeFoilConfig -> String -> String
freeFoilScopeNameModifier :: FreeFoilConfig -> String -> String
signatureNameModifier :: FreeFoilConfig -> String -> String
freeFoilConNameModifier :: FreeFoilConfig -> String -> String
freeFoilConvertToName :: FreeFoilConfig -> String -> String
freeFoilConvertFromName :: FreeFoilConfig -> String -> String
rawQuantifiedNames :: [Name]
freeFoilTermConfigs :: [FreeFoilTermConfig]
freeFoilNameModifier :: String -> String
freeFoilScopeNameModifier :: String -> String
signatureNameModifier :: String -> String
freeFoilConNameModifier :: String -> String
freeFoilConvertToName :: String -> String
freeFoilConvertFromName :: String -> String
..} = Type -> [Name]
go
  where
    go :: Type -> [Name]
go = \case
      PeelConT Name
typeName [Type]
_params
        | Name
typeName Name -> [Name] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
rawQuantifiedNames -> []
        | Name
typeName Name -> [Name] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` (FreeFoilTermConfig -> Name) -> [FreeFoilTermConfig] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map FreeFoilTermConfig -> Name
rawIdentName [FreeFoilTermConfig]
freeFoilTermConfigs -> [Name
typeName]
        | Just FreeFoilTermConfig{[Name]
Name
rawIdentName :: FreeFoilTermConfig -> Name
rawTermName :: FreeFoilTermConfig -> Name
rawBindingName :: FreeFoilTermConfig -> Name
rawScopeName :: FreeFoilTermConfig -> Name
rawVarConName :: FreeFoilTermConfig -> Name
rawSubTermNames :: FreeFoilTermConfig -> [Name]
rawSubScopeNames :: FreeFoilTermConfig -> [Name]
intToRawIdentName :: FreeFoilTermConfig -> Name
rawVarIdentToTermName :: FreeFoilTermConfig -> Name
rawTermToScopeName :: FreeFoilTermConfig -> Name
rawScopeToTermName :: FreeFoilTermConfig -> Name
rawIdentName :: Name
rawTermName :: Name
rawBindingName :: Name
rawScopeName :: Name
rawVarConName :: Name
rawSubTermNames :: [Name]
rawSubScopeNames :: [Name]
intToRawIdentName :: Name
rawVarIdentToTermName :: Name
rawTermToScopeName :: Name
rawScopeToTermName :: Name
..} <- Name -> [FreeFoilTermConfig] -> Maybe FreeFoilTermConfig
lookupTermName Name
typeName [FreeFoilTermConfig]
freeFoilTermConfigs ->
            [Name
rawIdentName]
        | Just FreeFoilTermConfig{[Name]
Name
rawIdentName :: FreeFoilTermConfig -> Name
rawTermName :: FreeFoilTermConfig -> Name
rawBindingName :: FreeFoilTermConfig -> Name
rawScopeName :: FreeFoilTermConfig -> Name
rawVarConName :: FreeFoilTermConfig -> Name
rawSubTermNames :: FreeFoilTermConfig -> [Name]
rawSubScopeNames :: FreeFoilTermConfig -> [Name]
intToRawIdentName :: FreeFoilTermConfig -> Name
rawVarIdentToTermName :: FreeFoilTermConfig -> Name
rawTermToScopeName :: FreeFoilTermConfig -> Name
rawScopeToTermName :: FreeFoilTermConfig -> Name
rawIdentName :: Name
rawTermName :: Name
rawBindingName :: Name
rawScopeName :: Name
rawVarConName :: Name
rawSubTermNames :: [Name]
rawSubScopeNames :: [Name]
intToRawIdentName :: Name
rawVarIdentToTermName :: Name
rawTermToScopeName :: Name
rawScopeToTermName :: Name
..} <- Name -> [FreeFoilTermConfig] -> Maybe FreeFoilTermConfig
lookupBindingName Name
typeName [FreeFoilTermConfig]
freeFoilTermConfigs ->
            [Name
rawIdentName]
        | Just FreeFoilTermConfig{[Name]
Name
rawIdentName :: FreeFoilTermConfig -> Name
rawTermName :: FreeFoilTermConfig -> Name
rawBindingName :: FreeFoilTermConfig -> Name
rawScopeName :: FreeFoilTermConfig -> Name
rawVarConName :: FreeFoilTermConfig -> Name
rawSubTermNames :: FreeFoilTermConfig -> [Name]
rawSubScopeNames :: FreeFoilTermConfig -> [Name]
intToRawIdentName :: FreeFoilTermConfig -> Name
rawVarIdentToTermName :: FreeFoilTermConfig -> Name
rawTermToScopeName :: FreeFoilTermConfig -> Name
rawScopeToTermName :: FreeFoilTermConfig -> Name
rawIdentName :: Name
rawTermName :: Name
rawBindingName :: Name
rawScopeName :: Name
rawVarConName :: Name
rawSubTermNames :: [Name]
rawSubScopeNames :: [Name]
intToRawIdentName :: Name
rawVarIdentToTermName :: Name
rawTermToScopeName :: Name
rawScopeToTermName :: Name
..} <- Name -> [FreeFoilTermConfig] -> Maybe FreeFoilTermConfig
lookupScopeName Name
typeName [FreeFoilTermConfig]
freeFoilTermConfigs ->
            [Name
rawIdentName]
        | Just FreeFoilTermConfig{[Name]
Name
rawIdentName :: FreeFoilTermConfig -> Name
rawTermName :: FreeFoilTermConfig -> Name
rawBindingName :: FreeFoilTermConfig -> Name
rawScopeName :: FreeFoilTermConfig -> Name
rawVarConName :: FreeFoilTermConfig -> Name
rawSubTermNames :: FreeFoilTermConfig -> [Name]
rawSubScopeNames :: FreeFoilTermConfig -> [Name]
intToRawIdentName :: FreeFoilTermConfig -> Name
rawVarIdentToTermName :: FreeFoilTermConfig -> Name
rawTermToScopeName :: FreeFoilTermConfig -> Name
rawScopeToTermName :: FreeFoilTermConfig -> Name
rawIdentName :: Name
rawTermName :: Name
rawBindingName :: Name
rawScopeName :: Name
rawVarConName :: Name
rawSubTermNames :: [Name]
rawSubScopeNames :: [Name]
intToRawIdentName :: Name
rawVarIdentToTermName :: Name
rawTermToScopeName :: Name
rawScopeToTermName :: Name
..} <- Name -> [FreeFoilTermConfig] -> Maybe FreeFoilTermConfig
lookupSubTermName Name
typeName [FreeFoilTermConfig]
freeFoilTermConfigs ->
            [Name
rawIdentName]
        | Just FreeFoilTermConfig{[Name]
Name
rawIdentName :: FreeFoilTermConfig -> Name
rawTermName :: FreeFoilTermConfig -> Name
rawBindingName :: FreeFoilTermConfig -> Name
rawScopeName :: FreeFoilTermConfig -> Name
rawVarConName :: FreeFoilTermConfig -> Name
rawSubTermNames :: FreeFoilTermConfig -> [Name]
rawSubScopeNames :: FreeFoilTermConfig -> [Name]
intToRawIdentName :: FreeFoilTermConfig -> Name
rawVarIdentToTermName :: FreeFoilTermConfig -> Name
rawTermToScopeName :: FreeFoilTermConfig -> Name
rawScopeToTermName :: FreeFoilTermConfig -> Name
rawIdentName :: Name
rawTermName :: Name
rawBindingName :: Name
rawScopeName :: Name
rawVarConName :: Name
rawSubTermNames :: [Name]
rawSubScopeNames :: [Name]
intToRawIdentName :: Name
rawVarIdentToTermName :: Name
rawTermToScopeName :: Name
rawScopeToTermName :: Name
..} <- Name -> [FreeFoilTermConfig] -> Maybe FreeFoilTermConfig
lookupSubScopeName Name
typeName [FreeFoilTermConfig]
freeFoilTermConfigs ->
            [Name
rawIdentName]
      ForallT [TyVarBndr Specificity]
_bndrs [Type]
_ctx Type
type_ -> Type -> [Name]
go Type
type_
      ForallVisT [TyVarBndr ()]
_bndrs Type
type_ -> Type -> [Name]
go Type
type_
      AppT Type
f Type
x -> Type -> [Name]
go Type
f [Name] -> [Name] -> [Name]
forall a. Semigroup a => a -> a -> a
<> Type -> [Name]
go Type
x
      AppKindT Type
f Type
_k -> Type -> [Name]
go Type
f
      SigT Type
t Type
_k -> Type -> [Name]
go Type
t
      ConT{} -> []
      VarT{} -> []
      PromotedT{} -> []
      InfixT Type
l Name
_op Type
r -> Type -> [Name]
go Type
l [Name] -> [Name] -> [Name]
forall a. Semigroup a => a -> a -> a
<> Type -> [Name]
go Type
r
      UInfixT Type
l Name
_op Type
r -> Type -> [Name]
go Type
l [Name] -> [Name] -> [Name]
forall a. Semigroup a => a -> a -> a
<> Type -> [Name]
go Type
r
      PromotedInfixT Type
l Name
_op Type
r -> Type -> [Name]
go Type
l [Name] -> [Name] -> [Name]
forall a. Semigroup a => a -> a -> a
<> Type -> [Name]
go Type
r
      PromotedUInfixT Type
l Name
_op Type
r -> Type -> [Name]
go Type
l [Name] -> [Name] -> [Name]
forall a. Semigroup a => a -> a -> a
<> Type -> [Name]
go Type
r
      ParensT Type
t -> Type -> [Name]
go Type
t
      TupleT{} -> []
      UnboxedTupleT{} -> []
      UnboxedSumT{} -> []
      ArrowT{} -> []
      MulArrowT{} -> []
      EqualityT{} -> []
      ListT{} -> []
      PromotedTupleT{} -> []
      PromotedNilT{} -> []
      PromotedConsT{} -> []
      StarT{} -> []
      ConstraintT{} -> []
      LitT{} -> []
      WildCardT{} -> []
      ImplicitParamT String
_s Type
t -> Type -> [Name]
go Type
t