{-# LANGUAGE LambdaCase      #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE ViewPatterns    #-}
{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}
{-# HLINT ignore "Use ++" #-}
-- | Template Haskell generation for Free Foil (generic scope-safe representation of syntax).
module Control.Monad.Free.Foil.TH.MkFreeFoil (
  FreeFoilConfig(..),
  FreeFoilTermConfig(..),
  mkFreeFoil,
  mkFreeFoilConversions,
) where

import           Language.Haskell.TH
import           Language.Haskell.TH.Syntax (addModFinalizer)

import           Control.Monad              (forM, forM_, when)
import qualified Control.Monad.Foil         as Foil
import           Control.Monad.Foil.TH.Util
import qualified Control.Monad.Free.Foil    as Foil
import           Data.Bifunctor
import           Data.List                  (find, unzip4, (\\), nub)
import           Data.Maybe                 (catMaybes, mapMaybe)
import Data.Map (Map)
import qualified Data.Map as Map
import qualified GHC.Generics               as GHC

-- | Config for the Template Haskell generation of data types,
-- pattern synonyms, and conversion functions for the Free Foil representation,
-- based on a raw recursive representation.
data FreeFoilConfig = FreeFoilConfig
  { 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.
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)@.
  }

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))

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
            Type
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 :: Type
argType = Sort -> FreeFoilConfig -> Type -> Type -> Type -> Type
toFreeFoilType Sort
SortBinder FreeFoilConfig
config Type
outerScope Type
innerScope Type
rawArgType
            (Type
theInnerScope, [BangType]
argTypes) <- Int -> Type -> [BangType] -> Q (Type, [BangType])
goTypeArgs (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) Type
innerScope [BangType]
rawArgs
            (Type, [BangType]) -> Q (Type, [BangType])
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
theInnerScope, ((Bang
bang_, Type
argType) BangType -> [BangType] -> [BangType]
forall a. a -> [a] -> [a]
: [BangType]
argTypes))

          | Just FreeFoilTermConfig
_ <- Name -> [FreeFoilTermConfig] -> Maybe FreeFoilTermConfig
lookupBindingName Name
rawTypeName (FreeFoilConfig -> [FreeFoilTermConfig]
freeFoilTermConfigs FreeFoilConfig
config) -> do
            Type
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 :: Type
argType = Sort -> FreeFoilConfig -> Type -> Type -> Type -> Type
toFreeFoilType Sort
SortBinder FreeFoilConfig
config Type
outerScope Type
innerScope Type
rawArgType
            (Type
theInnerScope, [BangType]
argTypes) <- Int -> Type -> [BangType] -> Q (Type, [BangType])
goTypeArgs (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) Type
innerScope [BangType]
rawArgs
            (Type, [BangType]) -> Q (Type, [BangType])
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
theInnerScope, ((Bang
bang_, Type
argType) BangType -> [BangType] -> [BangType]
forall a. a -> [a] -> [a]
: [BangType]
argTypes))

        Type
_ -> do
          let argType :: Type
argType = Sort -> FreeFoilConfig -> Type -> Type -> Type -> Type
toFreeFoilType Sort
SortBinder FreeFoilConfig
config Type
outerScope Type
outerScope Type
rawArgType
          (Type
theInnerScope, [BangType]
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
          (Type, [BangType]) -> Q (Type, [BangType])
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
theInnerScope, ((Bang
bang_, Type
argType) BangType -> [BangType] -> [BangType]
forall a. a -> [a] -> [a]
: [BangType]
argTypes))

    go :: Con -> Q Con
    go :: Con -> Q Con
go = \case
      GadtC [Name]
conNames [BangType]
argTypes Type
retType -> do
        (Type
theInnerScope, [BangType]
newArgs) <- Int -> Type -> [BangType] -> Q (Type, [BangType])
goTypeArgs Int
0 Type
theOuterScope [BangType]
argTypes
        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]
newArgs (Type -> Type -> Type
goType Type
theInnerScope 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)

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
            Name
binder <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"binder"
            Name
body <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"body"
            ([Name], [Pat], [Pat], [Exp]) -> Q ([Name], [Pat], [Pat], [Exp])
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Name
binder, Name
body], [Name -> [Type] -> [Pat] -> Pat
ConP 'Foil.ScopedAST [] [Name -> Pat
VarP Name
binder, Name -> Pat
VarP Name
body]], [[Pat] -> Pat
TupP [Name -> Pat
VarP Name
binder, Name -> Pat
VarP Name
body]], [Name -> Exp
VarE Name
binder, Name -> Exp
VarE Name
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
            Name
x <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"x"
            ([Name], [Pat], [Pat], [Exp]) -> Q ([Name], [Pat], [Pat], [Exp])
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Name
x], [Name -> Pat
VarP Name
x], [Name -> Pat
VarP Name
x], [Exp -> Exp -> Exp
AppE (Name -> Exp
VarE Name
funName) (Name -> Exp
VarE Name
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
            Name
x <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"x"
            ([Name], [Pat], [Pat], [Exp]) -> Q ([Name], [Pat], [Pat], [Exp])
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Name
x], [Name -> Pat
VarP Name
x], [Name -> Pat
VarP Name
x], [Exp -> Exp -> Exp
AppE (Name -> Exp
VarE Name
funName) (Name -> Exp
VarE Name
x)])
        | Name
typeName Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== '[] -> do
            Name
x <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"x"
            ([Name], [Pat], [Pat], [Exp]) -> Q ([Name], [Pat], [Pat], [Exp])
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Name
x], [Name -> Pat
VarP Name
x], [Name -> Pat
VarP Name
x], [Name -> Exp
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
            Name
x <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"x"
            ([Name], [Pat], [Pat], [Exp]) -> Q ([Name], [Pat], [Pat], [Exp])
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Name
x], [Name -> Pat
VarP Name
x], [Name -> Pat
VarP Name
x], [Exp -> Exp -> Exp
AppE (Exp -> Exp -> Exp
AppE (Name -> Exp
VarE 'fmap) (Name -> Exp
VarE Name
funName)) (Name -> Exp
VarE Name
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
            Name
x <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"x"
            ([Name], [Pat], [Pat], [Exp]) -> Q ([Name], [Pat], [Pat], [Exp])
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Name
x], [Name -> Pat
VarP Name
x], [Name -> Pat
VarP Name
x], [Exp -> Exp -> Exp
AppE (Exp -> Exp -> Exp
AppE (Name -> Exp
VarE 'fmap) (Name -> Exp
VarE Name
funName)) (Name -> Exp
VarE Name
x)])
      Type
_ -> do
        Name
x <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"x"
        ([Name], [Pat], [Pat], [Exp]) -> Q ([Name], [Pat], [Pat], [Exp])
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Name
x], [Name -> Pat
VarP Name
x], [Name -> Pat
VarP Name
x], [Name -> Exp
VarE Name
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
          ([[Name]] -> [Name]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat -> [Name]
vars, [[Pat]] -> [Pat]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat -> [Pat]
pats, [[Pat]] -> [Pat]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat -> [Pat]
pats', [[Exp]] -> [Exp]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat -> [Exp]
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
          [([Name], Pat, Pat, [Exp])] -> Q [([Name], Pat, Pat, [Exp])]
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return ([([Name], Pat, Pat, [Exp])] -> Q [([Name], Pat, Pat, [Exp])])
-> [([Name], Pat, Pat, [Exp])] -> Q [([Name], Pat, Pat, [Exp])]
forall a b. (a -> b) -> a -> b
$
            if Name
rawTypeName Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
rawTermName
              then [ ([Name]
vars, Name -> [Type] -> [Pat] -> Pat
ConP 'Foil.Node [] [Name -> [Type] -> [Pat] -> Pat
ConP Name
newConName [] [Pat]
pats], Name -> [Type] -> [Pat] -> Pat
ConP Name
newConName [] [Pat]
pats', [Exp]
exps) ]
              else [ ([Name]
vars, Name -> [Type] -> [Pat] -> Pat
ConP Name
newConName [] [Pat]
pats, Name -> [Type] -> [Pat] -> Pat
ConP Name
newConName [] [Pat]
pats', [Exp]
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 -> FreeFoilConfig -> FreeFoilTermConfig -> Con -> Q [([Name], Pat, Pat, [Exp])]
termConToPatBinding :: Name
-> FreeFoilConfig
-> FreeFoilTermConfig
-> Con
-> Q [([Name], Pat, Pat, [Exp])]
termConToPatBinding 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
            Name
x <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"x"
            ([Name], [Pat], [Pat], [Exp]) -> Q ([Name], [Pat], [Pat], [Exp])
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Name
x], [Name -> Pat
VarP Name
x], [Name -> Pat
VarP Name
x], [Name -> Exp
VarE Name
intToRawIdentName Exp -> Exp -> Exp
`AppE` (Name -> Exp
VarE 'Foil.nameId Exp -> Exp -> Exp
`AppE` (Name -> Exp
VarE 'Foil.nameOf Exp -> Exp -> Exp
`AppE` Name -> Exp
VarE Name
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
            Name
x <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"x"
            ([Name], [Pat], [Pat], [Exp]) -> Q ([Name], [Pat], [Pat], [Exp])
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Name
x], [Name -> Pat
VarP Name
x], [Name -> Pat
VarP Name
x], [Name -> Exp
VarE Name
funName Exp -> Exp -> Exp
`AppE` Name -> Exp
VarE Name
x])
        | Just FreeFoilTermConfig
_ <- Name -> [FreeFoilTermConfig] -> Maybe FreeFoilTermConfig
lookupScopeName Name
typeName [FreeFoilTermConfig]
freeFoilTermConfigs -> do
            Name
binder <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"binder"
            Name
body <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"body"
            ([Name], [Pat], [Pat], [Exp]) -> Q ([Name], [Pat], [Pat], [Exp])
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Name
binder, Name
body], [Name -> [Type] -> [Pat] -> Pat
ConP 'Foil.ScopedAST [] [Name -> Pat
VarP Name
binder, Name -> Pat
VarP Name
body]], [[Pat] -> Pat
TupP [Name -> Pat
VarP Name
binder, Name -> Pat
VarP Name
body]], [Name -> Exp
VarE Name
binder, Name -> Exp
VarE Name
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
            Name
x <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"x"
            ([Name], [Pat], [Pat], [Exp]) -> Q ([Name], [Pat], [Pat], [Exp])
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Name
x], [Name -> Pat
VarP Name
x], [Name -> Pat
VarP Name
x], [Exp -> Exp -> Exp
AppE (Name -> Exp
VarE Name
funName) (Name -> Exp
VarE Name
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
            Name
x <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"x"
            ([Name], [Pat], [Pat], [Exp]) -> Q ([Name], [Pat], [Pat], [Exp])
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Name
x], [Name -> Pat
VarP Name
x], [Name -> Pat
VarP Name
x], [Exp -> Exp -> Exp
AppE (Name -> Exp
VarE Name
funName) (Name -> Exp
VarE Name
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
            Name
x <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"x"
            ([Name], [Pat], [Pat], [Exp]) -> Q ([Name], [Pat], [Pat], [Exp])
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Name
x], [Name -> Pat
VarP Name
x], [Name -> Pat
VarP Name
x], [Exp -> Exp -> Exp
AppE (Exp -> Exp -> Exp
AppE (Name -> Exp
VarE 'fmap) (Name -> Exp
VarE Name
funName)) (Name -> Exp
VarE Name
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
            Name
x <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"x"
            ([Name], [Pat], [Pat], [Exp]) -> Q ([Name], [Pat], [Pat], [Exp])
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Name
x], [Name -> Pat
VarP Name
x], [Name -> Pat
VarP Name
x], [Exp -> Exp -> Exp
AppE (Exp -> Exp -> Exp
AppE (Name -> Exp
VarE 'fmap) (Name -> Exp
VarE Name
funName)) (Name -> Exp
VarE Name
x)])
      Type
_ -> do
        Name
x <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"x"
        ([Name], [Pat], [Pat], [Exp]) -> Q ([Name], [Pat], [Pat], [Exp])
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Name
x], [Name -> Pat
VarP Name
x], [Name -> Pat
VarP Name
x], [Name -> Exp
VarE Name
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
          ([[Name]] -> [Name]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat -> [Name]
vars, [[Pat]] -> [Pat]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat -> [Pat]
pats, [[Pat]] -> [Pat]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat -> [Pat]
pats', [[Exp]] -> [Exp]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat -> [Exp]
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
          [([Name], Pat, Pat, [Exp])] -> Q [([Name], Pat, Pat, [Exp])]
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return ([([Name], Pat, Pat, [Exp])] -> Q [([Name], Pat, Pat, [Exp])])
-> [([Name], Pat, Pat, [Exp])] -> Q [([Name], Pat, Pat, [Exp])]
forall a b. (a -> b) -> a -> b
$
            if Name
rawTypeName Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
rawTermName
              then [ ([Name]
vars, Name -> [Type] -> [Pat] -> Pat
ConP 'Foil.Node [] [Name -> [Type] -> [Pat] -> Pat
ConP Name
newConName [] [Pat]
pats], Name -> [Type] -> [Pat] -> Pat
ConP Name
newConName [] [Pat]
pats', [Exp]
exps) ]
              else [ ([Name]
vars, Name -> [Type] -> [Pat] -> Pat
ConP Name
newConName [] [Pat]
pats, Name -> [Type] -> [Pat] -> Pat
ConP Name
newConName [] [Pat]
pats', [Exp]
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
            Name
x <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"x"
            ([Name], [Pat], [Pat], [Exp]) -> Q ([Name], [Pat], [Pat], [Exp])
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Name
x], [Name -> Pat
VarP Name
x], [Name -> Pat
VarP Name
x], [Name -> Exp
VarE Name
funName Exp -> Exp -> Exp
`AppE` Name -> Exp
VarE Name
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
            Name
x <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"x"
            ([Name], [Pat], [Pat], [Exp]) -> Q ([Name], [Pat], [Pat], [Exp])
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Name
x], [Name -> Pat
VarP Name
x], [Name -> Pat
VarP Name
x], [Name -> Exp
VarE Name
rawTermToScopeName Exp -> Exp -> Exp
`AppE` (Name -> Exp
VarE Name
funName Exp -> Exp -> Exp
`AppE` Name -> Exp
VarE Name
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
            Name
x <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"x"
            ([Name], [Pat], [Pat], [Exp]) -> Q ([Name], [Pat], [Pat], [Exp])
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Name
x], [Name -> Pat
VarP Name
x], [Name -> Pat
VarP Name
x], [Name -> Exp
VarE Name
intToRawIdentName Exp -> Exp -> Exp
`AppE` (Name -> Exp
VarE 'Foil.nameId Exp -> Exp -> Exp
`AppE` Name -> Exp
VarE Name
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
            Name
x <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"x"
            ([Name], [Pat], [Pat], [Exp]) -> Q ([Name], [Pat], [Pat], [Exp])
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Name
x], [Name -> Pat
VarP Name
x], [Name -> Pat
VarP Name
x], [Name -> Exp
VarE Name
funName Exp -> Exp -> Exp
`AppE` Name -> Exp
VarE Name
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
            Name
x <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"x"
            ([Name], [Pat], [Pat], [Exp]) -> Q ([Name], [Pat], [Pat], [Exp])
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Name
x], [Name -> Pat
VarP Name
x], [Name -> Pat
VarP Name
x], [Exp -> Exp -> Exp
AppE (Name -> Exp
VarE Name
funName) (Name -> Exp
VarE Name
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
            Name
x <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"x"
            ([Name], [Pat], [Pat], [Exp]) -> Q ([Name], [Pat], [Pat], [Exp])
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Name
x], [Name -> Pat
VarP Name
x], [Name -> Pat
VarP Name
x], [Exp -> Exp -> Exp
AppE (Name -> Exp
VarE Name
funName) (Name -> Exp
VarE Name
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
            Name
x <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"x"
            ([Name], [Pat], [Pat], [Exp]) -> Q ([Name], [Pat], [Pat], [Exp])
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Name
x], [Name -> Pat
VarP Name
x], [Name -> Pat
VarP Name
x], [Exp -> Exp -> Exp
AppE (Exp -> Exp -> Exp
AppE (Name -> Exp
VarE 'fmap) (Name -> Exp
VarE Name
funName)) (Name -> Exp
VarE Name
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
            Name
x <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"x"
            ([Name], [Pat], [Pat], [Exp]) -> Q ([Name], [Pat], [Pat], [Exp])
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Name
x], [Name -> Pat
VarP Name
x], [Name -> Pat
VarP Name
x], [Exp -> Exp -> Exp
AppE (Exp -> Exp -> Exp
AppE (Name -> Exp
VarE 'fmap) (Name -> Exp
VarE Name
funName)) (Name -> Exp
VarE Name
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
            Name
x <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"x"
            ([Name], [Pat], [Pat], [Exp]) -> Q ([Name], [Pat], [Pat], [Exp])
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Name
x], [Name -> Pat
VarP Name
x], [Name -> Pat
VarP Name
x], [Exp -> Exp -> Exp
AppE (Exp -> Exp -> Exp
AppE (Name -> Exp
VarE 'fmap) (Name -> Exp
VarE Name
funName)) (Name -> Exp
VarE Name
x)])
      Type
_ -> do
        Name
x <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"x"
        ([Name], [Pat], [Pat], [Exp]) -> Q ([Name], [Pat], [Pat], [Exp])
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Name
x], [Name -> Pat
VarP Name
x], [Name -> Pat
VarP Name
x], [Name -> Exp
VarE Name
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
          ([[Name]] -> [Name]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat -> [Name]
vars, [[Pat]] -> [Pat]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat -> [Pat]
pats, [[Pat]] -> [Pat]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat -> [Pat]
pats', [[Exp]] -> [Exp]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat -> [Exp]
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
          [([Name], Pat, Pat, [Exp])] -> Q [([Name], Pat, Pat, [Exp])]
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return [ ([Name]
vars, Name -> [Type] -> [Pat] -> Pat
ConP Name
newConName [] [Pat]
pats, Name -> [Type] -> [Pat] -> Pat
ConP Name
newConName [] [Pat]
pats', [Exp]
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)

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
              rawConType :: Type
rawConType = (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) Type
rawRetType ((BangType -> Type) -> [BangType] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map BangType -> Type
forall a b. (a, b) -> b
snd [BangType]
rawArgTypes)
              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")
          [([Name]
vars, Pat
pat, Pat
_, [Exp]
_)] <- 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!
          Q () -> Q ()
addModFinalizer (Q () -> Q ()) -> Q () -> Q ()
forall a b. (a -> b) -> a -> b
$ DocLoc -> String -> Q ()
putDoc (Name -> DocLoc
DeclDoc Name
patName)
            (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
"'. Pattern synonym for an '" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show ''Foil.AST String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"' node of type '" 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
"'.")
          [(Name, [Dec])] -> Q [(Name, [Dec])]
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return [(Name
patName,
            [ Name -> Type -> Dec
PatSynSigD Name
patName (Sort -> FreeFoilConfig -> Type -> Type -> Type -> Type
toFreeFoilType Sort
SortTerm FreeFoilConfig
config Type
outerScope Type
innerScope Type
rawConType)
            , Name -> PatSynArgs -> PatSynDir -> Pat -> Dec
PatSynD Name
patName ([Name] -> PatSynArgs
PrefixPatSyn [Name]
vars) PatSynDir
ImplBidir Pat
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
          [([Name]
_vars, Pat
_pat, Pat
pat, [Exp]
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!
          [Clause] -> Q [Clause]
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return [ [Pat] -> Body -> [Dec] -> Clause
Clause [Pat
pat] (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
conName) [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)

toFreeFoilClauseFromBinding :: FreeFoilConfig -> FreeFoilTermConfig -> Type -> Con -> Q [Clause]
toFreeFoilClauseFromBinding :: FreeFoilConfig -> FreeFoilTermConfig -> Type -> Con -> Q [Clause]
toFreeFoilClauseFromBinding 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
          [([Name]
_vars, Pat
_pat, Pat
pat, [Exp]
exps)] <- Name
-> FreeFoilConfig
-> FreeFoilTermConfig
-> Con
-> Q [([Name], Pat, Pat, [Exp])]
termConToPatBinding Name
rawBindingName FreeFoilConfig
config FreeFoilTermConfig
termConfig
            ([Name] -> [BangType] -> Type -> Con
GadtC [Name
conName] [BangType]
rawArgTypes Type
rawRetType')    -- FIXME: unsafe matching!
          [Clause] -> Q [Clause]
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return [ [Pat] -> Body -> [Dec] -> Clause
Clause [Pat
pat] (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
conName) [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)

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
          [([Name]
_vars, Pat
_pat, Pat
pat, [Exp]
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!
          [Clause] -> Q [Clause]
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return [ [Pat] -> Body -> [Dec] -> Clause
Clause [Pat
pat] (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
conName) [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)

-- | Generate scope-safe types and pattern synonyms for a given raw set of types:
--
--  1. Scope-safe quantified types (e.g. type schemas, defining equations of functions, unification constraints, data/type declarations)
--  2. Scope-safe terms, scoped terms, subterms, scoped subterms.
--  3. Scope-safe patterns.
--  4. Signatures for terms, subterms, and scoped subterms.
--  5. Pattern synonyms for terms, subterms, and scoped subterms.
mkFreeFoil :: FreeFoilConfig -> Q [Dec]
mkFreeFoil :: 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]
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
      [Dec]
ds <- FreeFoilTermConfig -> Name -> Q [Dec]
mkPatternSynonyms' FreeFoilTermConfig
termConfig Name
rawTermName
      [Dec]
ds' <- [[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]
mkPatternSynonyms' FreeFoilTermConfig
termConfig) ([Name]
rawSubTermNames [Name] -> [Name] -> [Name]
forall a. Semigroup a => a -> a -> a
<> [Name]
rawSubScopeNames)
      [Dec] -> Q [Dec]
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Dec]
ds [Dec] -> [Dec] -> [Dec]
forall a. Semigroup a => a -> a -> a
<> [Dec]
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
      ([TyVarBndr BndrVis]
tvars, [Con]
cons) <- Name -> Q ([TyVarBndr BndrVis], [Con])
reifyDataOrNewtype Name
rawName
      let rawRetType :: Type
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)
      ([(Name, [Dec])] -> ([Name], [[Dec]])
forall a b. [(a, b)] -> ([a], [b])
unzip -> ([Name]
patNames, [[Dec]]
decls)) <- [[(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
<$> (Con -> Q [(Name, [Dec])]) -> [Con] -> Q [[(Name, [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
-> FreeFoilConfig
-> FreeFoilTermConfig
-> Type
-> Con
-> Q [(Name, [Dec])]
mkPatternSynonym Name
rawName FreeFoilConfig
config FreeFoilTermConfig{[Name]
Name
rawIdentName :: Name
rawTermName :: Name
rawBindingName :: Name
rawScopeName :: Name
rawVarConName :: Name
rawSubTermNames :: [Name]
rawSubScopeNames :: [Name]
intToRawIdentName :: Name
rawVarIdentToTermName :: Name
rawTermToScopeName :: Name
rawScopeToTermName :: 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]
cons
      let completeDecl :: Dec
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)
      [Dec] -> Q [Dec]
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return ([[Dec]] -> [Dec]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[Dec]]
decls [Dec] -> [Dec] -> [Dec]
forall a. [a] -> [a] -> [a]
++ [Dec
completeDecl])

    mkQuantifiedType :: Name -> Q Dec
mkQuantifiedType Name
rawName = do
      ([TyVarBndr BndrVis]
tvars, [Con]
cons) <- Name -> Q ([TyVarBndr BndrVis], [Con])
reifyDataOrNewtype Name
rawName
      let name :: Name
name = FreeFoilConfig -> Name -> Name
toFreeFoilName FreeFoilConfig
config Name
rawName
          rawRetType :: Type
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]
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 :: Con -> Q Con
toCon = FreeFoilConfig -> Type -> Type -> Type -> Con -> Q Con
toFreeFoilCon FreeFoilConfig
config Type
rawRetType (Name -> Type
VarT Name
outerScope) (Name -> Type
VarT Name
innerScope)
      [Con]
newCons <- (Con -> Q Con) -> [Con] -> Q [Con]
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 Con -> Q Con
toCon [Con]
cons
      Q () -> Q ()
addModFinalizer (Q () -> Q ()) -> Q () -> Q ()
forall a b. (a -> b) -> a -> b
$ DocLoc -> String -> Q ()
putDoc (Name -> DocLoc
DeclDoc 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
"'. A scope-safe version of '" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
rawName String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"'.")
      Dec -> Q Dec
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Type]
-> Name
-> [TyVarBndr BndrVis]
-> Maybe Type
-> [Con]
-> [DerivClause]
-> Dec
DataD [] Name
name [TyVarBndr BndrVis]
newParams Maybe Type
forall a. Maybe a
Nothing [Con]
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
      ([TyVarBndr BndrVis]
tvars, [Con]
cons) <- Name -> Q ([TyVarBndr BndrVis], [Con])
reifyDataOrNewtype Name
rawBindingName
      let bindingName :: Name
bindingName = FreeFoilConfig -> Name -> Name
toFreeFoilName FreeFoilConfig
config Name
rawBindingName
          rawRetType :: Type
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]
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 :: Con -> Q Con
toCon = FreeFoilConfig -> Type -> Type -> Con -> Q Con
toFreeFoilBindingCon FreeFoilConfig
config Type
rawRetType (Name -> Type
VarT Name
outerScope)
      [Con]
newCons <- (Con -> Q Con) -> [Con] -> Q [Con]
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 Con -> Q Con
toCon [Con]
cons
      Q () -> Q ()
addModFinalizer (Q () -> Q ()) -> Q () -> Q ()
forall a b. (a -> b) -> a -> b
$ DocLoc -> String -> Q ()
putDoc (Name -> DocLoc
DeclDoc Name
bindingName)
        (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
"'. A binding type, scope-safe version of '" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
rawBindingName String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"'.")
      Dec -> Q Dec
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Type]
-> Name
-> [TyVarBndr BndrVis]
-> Maybe Type
-> [Con]
-> [DerivClause]
-> Dec
DataD [] Name
bindingName [TyVarBndr BndrVis]
newParams Maybe Type
forall a. Maybe a
Nothing [Con]
newCons [])

    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
      [Dec]
sig <- FreeFoilTermConfig -> Name -> Q [Dec]
mkSignatureType FreeFoilTermConfig
termConfig Name
rawTermName
      [Dec]
subsigs <- [[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]
mkSignatureType FreeFoilTermConfig
termConfig) ([Name]
rawSubTermNames [Name] -> [Name] -> [Name]
forall a. Semigroup a => a -> a -> a
<> [Name]
rawSubScopeNames)
      [Dec] -> Q [Dec]
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Dec]
sig [Dec] -> [Dec] -> [Dec]
forall a. [a] -> [a] -> [a]
++ [Dec]
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
      ([TyVarBndr BndrVis]
tvars, [Con]
cons) <- Name -> Q ([TyVarBndr BndrVis], [Con])
reifyDataOrNewtype Name
rawName
      let sigName :: Name
sigName = FreeFoilConfig -> Name -> Name
toSignatureName FreeFoilConfig
config Name
rawName
          tvars' :: [Type]
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 :: Type
rawRetType = Name -> [Type] -> Type
PeelConT Name
rawName [Type]
tvars'
          newParams :: [TyVarBndr BndrVis]
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 :: Con -> Q (Maybe Con)
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)
      [Con]
newCons <- [Maybe Con] -> [Con]
forall a. [Maybe a] -> [a]
catMaybes ([Maybe Con] -> [Con]) -> Q [Maybe Con] -> Q [Con]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Con -> Q (Maybe Con)) -> [Con] -> Q [Maybe Con]
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 Con -> Q (Maybe Con)
toCon [Con]
cons
      let bindingT :: Type
bindingT = Name -> [Type] -> Type
PeelConT (FreeFoilConfig -> Name -> Name
toFreeFoilName FreeFoilConfig
config Name
rawBindingName) [Type]
tvars'
          sigNameT :: Type
sigNameT = Name -> [Type] -> Type
PeelConT (FreeFoilConfig -> Name -> Name
toSignatureName FreeFoilConfig
config Name
rawTermName) [Type]
tvars'
          astName :: Name
astName = FreeFoilConfig -> Name -> Name
toFreeFoilName FreeFoilConfig
config Name
rawName
          scopeName :: Name
scopeName = FreeFoilConfig -> Name -> Name
toFreeFoilScopedName FreeFoilConfig
config Name
rawName
          termAST :: Type
termAST = Name -> [Type] -> Type
PeelConT ''Foil.AST [Type
bindingT, Type
sigNameT]
          scopedTermAST :: Type
scopedTermAST = Name -> [Type] -> Type
PeelConT ''Foil.ScopedAST [Type
bindingT, Type
sigNameT]
          n :: Name
n = String -> Name
mkName String
"n"
      Q () -> Q ()
addModFinalizer (Q () -> Q ()) -> Q () -> Q ()
forall a b. (a -> b) -> a -> b
$ DocLoc -> String -> Q ()
putDoc (Name -> DocLoc
DeclDoc Name
sigName)
        (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
"'. A signature based on '" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
rawName String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"'.")
      Q () -> Q ()
addModFinalizer (Q () -> Q ()) -> Q () -> Q ()
forall a b. (a -> b) -> a -> b
$ DocLoc -> String -> Q ()
putDoc (Name -> DocLoc
DeclDoc Name
astName)
        (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
"'. A scope-safe version of '" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
rawName String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"'.")
      Bool -> Q () -> Q ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Name
rawTermName Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
rawName) (Q () -> Q ()) -> Q () -> Q ()
forall a b. (a -> b) -> a -> b
$ do
        Q () -> Q ()
addModFinalizer (Q () -> Q ()) -> Q () -> Q ()
forall a b. (a -> b) -> a -> b
$ DocLoc -> String -> Q ()
putDoc (Name -> DocLoc
DeclDoc Name
scopeName)
          (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
"'. A scoped (and scope-safe) version of '" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
rawName String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"'.")
      [Dec] -> Q [Dec]
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Dec] -> Q [Dec]) -> [Dec] -> Q [Dec]
forall a b. (a -> b) -> a -> b
$ [[Dec]] -> [Dec]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
        [ [ [Type]
-> Name
-> [TyVarBndr BndrVis]
-> Maybe Type
-> [Con]
-> [DerivClause]
-> Dec
DataD [] Name
sigName [TyVarBndr BndrVis]
newParams Maybe Type
forall a. Maybe a
Nothing [Con]
newCons [Maybe DerivStrategy -> [Type] -> DerivClause
DerivClause Maybe DerivStrategy
forall a. Maybe a
Nothing [Name -> Type
ConT ''GHC.Generic, Name -> Type
ConT ''Functor, Name -> Type
ConT ''Foldable, Name -> Type
ConT ''Traversable]] ]
        , if Name
rawTermName Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
rawName
            then [ Name -> [TyVarBndr BndrVis] -> Type -> Dec
TySynD Name
astName   [TyVarBndr BndrVis]
tvars Type
termAST
                 , Name -> [TyVarBndr BndrVis] -> Type -> Dec
TySynD Name
scopeName [TyVarBndr BndrVis]
tvars Type
scopedTermAST ]
            else [ Name -> [TyVarBndr BndrVis] -> Type -> Dec
TySynD Name
astName   ([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
n BndrVis
BndrReq])
                    (Name -> [Type] -> Type
PeelConT Name
sigName
                      ([Type]
tvars' [Type] -> [Type] -> [Type]
forall a. [a] -> [a] -> [a]
++
                      [ Type -> Type -> Type
AppT Type
scopedTermAST (Name -> Type
VarT Name
n)
                      , Type -> Type -> Type
AppT Type
termAST (Name -> Type
VarT Name
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.
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
      ([TyVarBndr BndrVis]
tvars, [Con]
cons) <- Name -> Q ([TyVarBndr BndrVis], [Con])
reifyDataOrNewtype Name
rawName
      let rawSigName :: Name
rawSigName = FreeFoilConfig -> Name -> Name
toSignatureName FreeFoilConfig
config Name
rawName
          funName :: Name
funName = FreeFoilConfig -> Name -> Name
toFreeFoilNameFrom FreeFoilConfig
config Name
rawSigName
          rawRetType :: Type
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 :: Type
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 :: Type
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 :: Type
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 :: Type
rawScopeType = Int -> Type
TupleT Int
2 Type -> Type -> Type
`AppT` Type
rawBindingType Type -> Type -> Type
`AppT` Type
rawScopedTermType
      case Sort -> FreeFoilConfig -> Type -> Type -> Type -> Maybe Type
toFreeFoilSigType Sort
SortSubTerm FreeFoilConfig
config Type
rawScopeType Type
rawTermType Type
rawRetType of
        Just Type
termType -> do
          [Clause]
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
          Q () -> Q ()
addModFinalizer (Q () -> Q ()) -> Q () -> Q ()
forall a b. (a -> b) -> a -> b
$ DocLoc -> String -> Q ()
putDoc (Name -> DocLoc
DeclDoc Name
funName)
            (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
"'. A helper used to convert from scope-safe to raw representation.")
          [Dec] -> Q [Dec]
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return
            [ Name -> Type -> Dec
SigD Name
funName (Type -> Type -> Type
AppT (Type -> Type -> Type
AppT Type
ArrowT Type
termType) Type
rawRetType)
            , Name -> [Clause] -> Dec
FunD Name
funName [Clause]
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
      ([TyVarBndr BndrVis]
tvars, [Con]
_cons) <- Name -> Q ([TyVarBndr BndrVis], [Con])
reifyDataOrNewtype Name
rawTermName
      let funName :: Name
funName = FreeFoilConfig -> Name -> Name
toFreeFoilNameFrom FreeFoilConfig
config Name
rawTermName
          rawSigName :: Name
rawSigName = FreeFoilConfig -> Name -> Name
toSignatureName FreeFoilConfig
config Name
rawTermName
          funSigName :: Name
funSigName = FreeFoilConfig -> Name -> Name
toFreeFoilNameFrom FreeFoilConfig
config Name
rawSigName
          funBindingName :: Name
funBindingName = FreeFoilConfig -> Name -> Name
toFreeFoilNameFrom FreeFoilConfig
config Name
rawBindingName
          rawTermType :: Type
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 :: Type
termType =  Sort -> FreeFoilConfig -> Type -> Type -> Type -> Type
toFreeFoilType Sort
SortTerm FreeFoilConfig
config (Name -> Type
VarT Name
outerScope) (Name -> Type
VarT Name
innerScope) Type
rawTermType
      Q () -> Q ()
addModFinalizer (Q () -> Q ()) -> Q () -> Q ()
forall a b. (a -> b) -> a -> b
$ DocLoc -> String -> Q ()
putDoc (Name -> DocLoc
DeclDoc Name
funName)
        (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
"'. Convert from scope-safe to raw representation.")
      [Dec] -> Q [Dec]
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return
        [ Name -> Type -> Dec
SigD Name
funName (Type -> Type -> Type
AppT (Type -> Type -> Type
AppT Type
ArrowT Type
termType) Type
rawTermType)
        , Name -> [Clause] -> Dec
FunD Name
funName [
            [Pat] -> Body -> [Dec] -> Clause
Clause [] (Exp -> Body
NormalB
              (Name -> Exp
VarE 'Foil.convertFromAST
                Exp -> Exp -> Exp
`AppE` Name -> Exp
VarE Name
funSigName
                Exp -> Exp -> Exp
`AppE` Name -> Exp
VarE Name
rawVarIdentToTermName
                Exp -> Exp -> Exp
`AppE` Name -> Exp
VarE Name
funBindingName
                Exp -> Exp -> Exp
`AppE` Name -> Exp
VarE Name
rawTermToScopeName
                Exp -> Exp -> Exp
`AppE` Name -> Exp
VarE Name
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
      ([TyVarBndr BndrVis]
tvars, [Con]
_cons) <- Name -> Q ([TyVarBndr BndrVis], [Con])
reifyDataOrNewtype Name
rawName
      let funName :: Name
funName = FreeFoilConfig -> Name -> Name
toFreeFoilNameFrom FreeFoilConfig
config Name
rawName
          funSigName :: Name
funSigName = FreeFoilConfig -> Name -> Name
toFreeFoilNameFrom FreeFoilConfig
config (FreeFoilConfig -> Name -> Name
toSignatureName FreeFoilConfig
config Name
rawName)
          funTermName :: Name
funTermName = FreeFoilConfig -> Name -> Name
toFreeFoilNameFrom FreeFoilConfig
config Name
rawTermName
          funBindingName :: Name
funBindingName = FreeFoilConfig -> Name -> Name
toFreeFoilNameFrom FreeFoilConfig
config Name
rawBindingName
          rawType :: Type
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 :: Type
safeType =  Sort -> FreeFoilConfig -> Type -> Type -> Type -> Type
toFreeFoilType Sort
SortTerm FreeFoilConfig
config (Name -> Type
VarT Name
outerScope) (Name -> Type
VarT Name
innerScope) Type
rawType
      Name
binders <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"binders"
      Name
body <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"body"
      Q () -> Q ()
addModFinalizer (Q () -> Q ()) -> Q () -> Q ()
forall a b. (a -> b) -> a -> b
$ DocLoc -> String -> Q ()
putDoc (Name -> DocLoc
DeclDoc Name
funName)
        (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
"'. Convert from scope-safe to raw representation.")
      [Dec] -> Q [Dec]
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return
        [ Name -> Type -> Dec
SigD Name
funName (Type -> Type -> Type
AppT (Type -> Type -> Type
AppT Type
ArrowT Type
safeType) Type
rawType)
        , Name -> [Clause] -> Dec
FunD Name
funName [
            [Pat] -> Body -> [Dec] -> Clause
Clause [] (Exp -> Body
NormalB (Exp -> Body) -> Exp -> Body
forall a b. (a -> b) -> a -> b
$
              Maybe Exp -> Exp -> Maybe Exp -> Exp
InfixE
              (Exp -> Maybe Exp
forall a. a -> Maybe a
Just (Name -> Exp
VarE Name
funSigName))
              (Name -> Exp
VarE '(.))
              (Exp -> Maybe Exp
forall a. a -> Maybe a
Just (Name -> Exp
VarE 'bimap
                Exp -> Exp -> Exp
`AppE` [Pat] -> Exp -> Exp
LamE [Name -> [Type] -> [Pat] -> Pat
ConP 'Foil.ScopedAST [] [Name -> Pat
VarP Name
binders, Name -> Pat
VarP Name
body]]
                  ([Maybe Exp] -> Exp
TupE [ Exp -> Maybe Exp
forall a. a -> Maybe a
Just (Name -> Exp
VarE Name
funBindingName Exp -> Exp -> Exp
`AppE` Name -> Exp
VarE Name
binders)
                        , Exp -> Maybe Exp
forall a. a -> Maybe a
Just (Name -> Exp
VarE Name
rawTermToScopeName Exp -> Exp -> Exp
`AppE` (Name -> Exp
VarE Name
funTermName Exp -> Exp -> Exp
`AppE` Name -> Exp
VarE Name
body))])
                Exp -> Exp -> Exp
`AppE` Name -> Exp
VarE Name
funTermName))) []
          ]
        ]

    mkConvertFromQuantified :: Name -> Q [Dec]
mkConvertFromQuantified Name
rawName = do
      ([TyVarBndr BndrVis]
tvars, [Con]
cons) <- Name -> Q ([TyVarBndr BndrVis], [Con])
reifyDataOrNewtype Name
rawName
      let funName :: Name
funName = FreeFoilConfig -> Name -> Name
toFreeFoilNameFrom FreeFoilConfig
config Name
rawName
          rawType :: Type
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 :: Type
safeType = Sort -> FreeFoilConfig -> Type -> Type -> Type -> Type
toFreeFoilType Sort
SortTerm FreeFoilConfig
config (Name -> Type
VarT Name
outerScope) (Name -> Type
VarT Name
innerScope) Type
rawType
      Q () -> Q ()
addModFinalizer (Q () -> Q ()) -> Q () -> Q ()
forall a b. (a -> b) -> a -> b
$ DocLoc -> String -> Q ()
putDoc (Name -> DocLoc
DeclDoc Name
funName)
        (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
"'. Convert from scope-safe to raw representation.")
      [Clause]
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 (FreeFoilConfig -> Type -> Con -> Q [Clause]
toFreeFoilClauseFromQuantified FreeFoilConfig
config Type
rawType) [Con]
cons
      [Dec] -> Q [Dec]
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return
        [ Name -> Type -> Dec
SigD Name
funName (Type -> Type -> Type
AppT (Type -> Type -> Type
AppT Type
ArrowT Type
safeType) Type
rawType)
        , Name -> [Clause] -> Dec
FunD Name
funName [Clause]
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
      ([TyVarBndr BndrVis]
tvars, [Con]
cons) <- Name -> Q ([TyVarBndr BndrVis], [Con])
reifyDataOrNewtype Name
rawBindingName
      let funName :: Name
funName = FreeFoilConfig -> Name -> Name
toFreeFoilNameFrom FreeFoilConfig
config Name
rawBindingName
          rawRetType :: Type
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)
          bindingType :: Type
bindingType = Sort -> FreeFoilConfig -> Type -> Type -> Type -> Type
toFreeFoilType Sort
SortBinder FreeFoilConfig
config (Name -> Type
VarT Name
outerScope) (Name -> Type
VarT Name
innerScope) Type
rawRetType
      [Clause]
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 (FreeFoilConfig -> FreeFoilTermConfig -> Type -> Con -> Q [Clause]
toFreeFoilClauseFromBinding FreeFoilConfig
config FreeFoilTermConfig
termConfig Type
rawRetType) [Con]
cons
      Q () -> Q ()
addModFinalizer (Q () -> Q ()) -> Q () -> Q ()
forall a b. (a -> b) -> a -> b
$ DocLoc -> String -> Q ()
putDoc (Name -> DocLoc
DeclDoc Name
funName)
        (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
"'. Convert a scope-safe to a raw binding.")
      [Dec] -> Q [Dec]
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return
        [ Name -> Type -> Dec
SigD Name
funName (Type
bindingType Type -> Type -> Type
--> Type
rawRetType)
        , Name -> [Clause] -> Dec
FunD Name
funName [Clause]
clauses ]

    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
      ([TyVarBndr BndrVis]
tvars, [Con]
cons) <- Name -> Q ([TyVarBndr BndrVis], [Con])
reifyDataOrNewtype Name
rawName
      ([TyVarBndr BndrVis]
itvars, [Con]
_cons) <- Name -> Q ([TyVarBndr BndrVis], [Con])
reifyDataOrNewtype Name
rawIdentName
      let funName :: Name
funName = FreeFoilConfig -> Name -> Name
toFreeFoilNameTo FreeFoilConfig
config Name
rawName
          rawIdentType :: Type
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 :: Type
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 :: Type
safeType =  Sort -> FreeFoilConfig -> Type -> Type -> Type -> Type
toFreeFoilType Sort
SortTerm FreeFoilConfig
config (Name -> Type
VarT Name
outerScope) (Name -> Type
VarT Name
innerScope) Type
rawType
      [Clause]
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 (Type -> FreeFoilConfig -> FreeFoilTermConfig -> Con -> Q [Clause]
subTermConToClause Type
rawType FreeFoilConfig
config FreeFoilTermConfig
termConfig) [Con]
cons
      Q () -> Q ()
addModFinalizer (Q () -> Q ()) -> Q () -> Q ()
forall a b. (a -> b) -> a -> b
$ DocLoc -> String -> Q ()
putDoc (Name -> DocLoc
DeclDoc Name
funName)
        (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
"'. Convert from scope-safe to raw representation.")
      let scope :: Name
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
      [Dec] -> Q [Dec]
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return
        [ Name -> Type -> Dec
SigD Name
funName (Type -> Dec) -> Type -> Dec
forall a b. (a -> b) -> a -> b
$
            [TyVarBndr Specificity] -> [Type] -> Type -> Type
ForallT
              (Name -> Specificity -> TyVarBndr Specificity
forall flag. Name -> flag -> TyVarBndr flag
PlainTV Name
scope 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
scope
              , Name -> Type
ConT ''Ord Type -> Type -> Type
`AppT` Type
rawIdentType ] (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$
                (Name -> Type
ConT ''Foil.Scope Type -> Type -> Type
`AppT` Name -> Type
VarT Name
scope)
                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
scope))
                Type -> Type -> Type
--> Type
rawType
                Type -> Type -> Type
--> Type
safeType
        , Name -> [Clause] -> Dec
FunD Name
funName [Clause]
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
      ([TyVarBndr BndrVis]
tvars, [Con]
_cons) <- Name -> Q ([TyVarBndr BndrVis], [Con])
reifyDataOrNewtype Name
rawTermName
      ([TyVarBndr BndrVis]
itvars, [Con]
_cons) <- Name -> Q ([TyVarBndr BndrVis], [Con])
reifyDataOrNewtype Name
rawIdentName
      let funName :: Name
funName = FreeFoilConfig -> Name -> Name
toFreeFoilNameTo FreeFoilConfig
config Name
rawTermName
          rawSigName :: Name
rawSigName = FreeFoilConfig -> Name -> Name
toSignatureName FreeFoilConfig
config Name
rawTermName
          rawIdentType :: Type
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 :: Name
funSigName = FreeFoilConfig -> Name -> Name
toFreeFoilNameTo FreeFoilConfig
config Name
rawSigName
          funBindingName :: Name
funBindingName = FreeFoilConfig -> Name -> Name
toFreeFoilNameTo FreeFoilConfig
config Name
rawBindingName
          rawTermType :: Type
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 :: Type
termType =  Sort -> FreeFoilConfig -> Type -> Type -> Type -> Type
toFreeFoilType Sort
SortTerm FreeFoilConfig
config (Name -> Type
VarT Name
outerScope) (Name -> Type
VarT Name
innerScope) Type
rawTermType
      Q () -> Q ()
addModFinalizer (Q () -> Q ()) -> Q () -> Q ()
forall a b. (a -> b) -> a -> b
$ DocLoc -> String -> Q ()
putDoc (Name -> DocLoc
DeclDoc Name
funName)
        (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
"'. Convert from scope-safe to raw representation.")
      [Dec] -> Q [Dec]
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return
        [ Name -> Type -> Dec
SigD Name
funName (Type -> Dec) -> Type -> Dec
forall a b. (a -> b) -> a -> b
$
            [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 -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$
                (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
        , Name -> [Clause] -> Dec
FunD Name
funName [
            [Pat] -> Body -> [Dec] -> Clause
Clause [] (Exp -> Body
NormalB
              (Name -> Exp
VarE 'Foil.convertToAST
                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)) []
          ]
        ]

    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
      ([TyVarBndr BndrVis]
tvars, [Con]
cons) <- Name -> Q ([TyVarBndr BndrVis], [Con])
reifyDataOrNewtype Name
rawName
      ([TyVarBndr BndrVis]
itvars, [Con]
_cons) <- Name -> Q ([TyVarBndr BndrVis], [Con])
reifyDataOrNewtype Name
rawIdentName
      let rawSigName :: Name
rawSigName = FreeFoilConfig -> Name -> Name
toSignatureName FreeFoilConfig
config Name
rawName
          funName :: Name
funName = FreeFoilConfig -> Name -> Name
toFreeFoilNameTo FreeFoilConfig
config Name
rawSigName
          rawType :: Type
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 :: Type
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 :: Type
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 :: Type
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 :: Type
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 :: Type
rawScopeType = Int -> Type
TupleT Int
2 Type -> Type -> Type
`AppT` Type
rawBindingType Type -> Type -> Type
`AppT` Type
rawScopedTermType
      case Sort -> FreeFoilConfig -> Type -> Type -> Type -> Maybe Type
toFreeFoilSigType Sort
SortSubTerm FreeFoilConfig
config Type
rawScopeType Type
rawTermType Type
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
          [Clause]
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
          Q () -> Q ()
addModFinalizer (Q () -> Q ()) -> Q () -> Q ()
forall a b. (a -> b) -> a -> b
$ DocLoc -> String -> Q ()
putDoc (Name -> DocLoc
DeclDoc Name
funName)
            (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
"'. A helper used to convert from raw to scope-safe representation.")
          [Dec] -> Q [Dec]
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return
            [ Name -> Type -> Dec
SigD Name
funName (Type -> Type -> Type
AppT (Type -> Type -> Type
AppT Type
ArrowT Type
rawType) Type
retType)
            , Name -> [Clause] -> Dec
FunD Name
funName [Clause]
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
      ([TyVarBndr BndrVis]
tvars, [Con]
cons) <- Name -> Q ([TyVarBndr BndrVis], [Con])
reifyDataOrNewtype Name
rawBindingName
      ([TyVarBndr BndrVis]
itvars, [Con]
_cons) <- Name -> Q ([TyVarBndr BndrVis], [Con])
reifyDataOrNewtype Name
rawIdentName
      let funName :: Name
funName = FreeFoilConfig -> Name -> Name
toFreeFoilNameTo FreeFoilConfig
config Name
rawBindingName
          rawBindingType :: Type
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 :: Type
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 :: Type
safeType = Sort -> FreeFoilConfig -> Type -> Type -> Type -> Type
toFreeFoilType Sort
SortBinder FreeFoilConfig
config (Name -> Type
VarT Name
outerScope) (Name -> Type
VarT Name
innerScope) Type
rawBindingType
      [Clause]
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 (Type -> FreeFoilConfig -> FreeFoilTermConfig -> Con -> Q [Clause]
bindingConToClause Type
rawBindingType FreeFoilConfig
config FreeFoilTermConfig
termConfig) [Con]
cons
      Name
r <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"r"
      Q () -> Q ()
addModFinalizer (Q () -> Q ()) -> Q () -> Q ()
forall a b. (a -> b) -> a -> b
$ DocLoc -> String -> Q ()
putDoc (Name -> DocLoc
DeclDoc Name
funName)
        (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
"'. Convert from raw to scope-safe binding (CPS-style).")
      [Dec] -> Q [Dec]
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return
        [ Name -> Type -> Dec
SigD Name
funName (Type -> Dec) -> Type -> Dec
forall a b. (a -> b) -> a -> b
$
            [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 -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$
                (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
        , Name -> [Clause] -> Dec
FunD Name
funName [Clause]
clauses ]

    mkConvertToQuantified :: Name -> Q [Dec]
mkConvertToQuantified Name
rawName = do
      ([TyVarBndr BndrVis]
tvars, [Con]
cons) <- Name -> Q ([TyVarBndr BndrVis], [Con])
reifyDataOrNewtype Name
rawName
      Name -> FreeFoilConfig -> Q [Name]
rawIdentNamesOfQuantifiedName Name
rawName FreeFoilConfig
config Q [Name] -> ([Name] -> Q [Dec]) -> Q [Dec]
forall a b. Q a -> (a -> Q b) -> Q b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        [] -> String -> Q [Dec]
forall a. HasCallStack => String -> a
error String
"unexpected: quantified type not connected to any known terms"
        [Name
rawIdentName'] -> do
          ([TyVarBndr BndrVis]
itvars, [Con]
_cons) <- Name -> Q ([TyVarBndr BndrVis], [Con])
reifyDataOrNewtype Name
rawIdentName'
          let funName :: Name
funName = FreeFoilConfig -> Name -> Name
toFreeFoilNameTo FreeFoilConfig
config Name
rawName
              rawIdentType :: Type
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 :: Type
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 :: Type
safeType = Sort -> FreeFoilConfig -> Type -> Type -> Type -> Type
toFreeFoilType Sort
SortTerm FreeFoilConfig
config (Name -> Type
VarT Name
outerScope) (Name -> Type
VarT Name
innerScope) Type
rawType
          Q () -> Q ()
addModFinalizer (Q () -> Q ()) -> Q () -> Q ()
forall a b. (a -> b) -> a -> b
$ DocLoc -> String -> Q ()
putDoc (Name -> DocLoc
DeclDoc Name
funName)
            (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
"'. Convert from scope-safe to raw representation.")
          [Clause]
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 (Type -> FreeFoilConfig -> Con -> Q [Clause]
quantifiedConToClause Type
rawType FreeFoilConfig
config) [Con]
cons
          [Dec] -> Q [Dec]
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return
            [ Name -> Type -> Dec
SigD Name
funName (Type -> Dec) -> Type -> Dec
forall a b. (a -> b) -> a -> b
$
                [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 -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$
                    (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
rawType
                    Type -> Type -> Type
--> Type
safeType
            , Name -> [Clause] -> Dec
FunD Name
funName [Clause]
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
            Name
x <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"_x"
            ([Pat]
pats, [Exp]
exps, Exp -> Exp
wrap, Name
scope', Name
env') <- Name
-> Name
-> Name
-> Name
-> [Type]
-> Q ([Pat], [Exp], Exp -> Exp, Name, Name)
goArgTypes Name
theScope Name
theEnv Name
scope Name
env [Type]
ts
            ([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 (Name -> Pat
VarP Name
x Pat -> [Pat] -> [Pat]
forall a. a -> [a] -> [a]
: [Pat]
pats, (Maybe Exp -> Exp -> Maybe Exp -> Exp
InfixE (Exp -> Maybe Exp
forall a. a -> Maybe a
Just (Name -> Exp
VarE Name
env)) (Name -> Exp
VarE '(Map.!)) (Exp -> Maybe Exp
forall a. a -> Maybe a
Just (Name -> Exp
VarE Name
x))) Exp -> [Exp] -> [Exp]
forall a. a -> [a] -> [a]
: [Exp]
exps, Exp -> Exp
wrap, Name
scope', Name
env')
        | Just FreeFoilTermConfig
_ <- Name -> [FreeFoilTermConfig] -> Maybe FreeFoilTermConfig
lookupBindingName Name
typeName [FreeFoilTermConfig]
freeFoilTermConfigs -> do
            Name
x <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"_x"
            Name
x' <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"_x'"
            Name
scope' <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"_scope"
            Name
env' <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"_env"
            let funName :: Name
funName = FreeFoilConfig -> Name -> Name
toFreeFoilNameTo FreeFoilConfig
config Name
typeName
            ([Pat]
pats, [Exp]
exps, Exp -> Exp
wrap, Name
scope'', Name
env'') <- Name
-> Name
-> Name
-> Name
-> [Type]
-> Q ([Pat], [Exp], Exp -> Exp, Name, Name)
goArgTypes Name
theScope Name
theEnv Name
scope' Name
env' [Type]
ts
            ([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 (Name -> Pat
VarP Name
x Pat -> [Pat] -> [Pat]
forall a. a -> [a] -> [a]
: [Pat]
pats, Name -> Exp
VarE Name
x' Exp -> [Exp] -> [Exp]
forall a. a -> [a] -> [a]
: [Exp]
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)), Name
scope'', Name
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
            Name
x <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"_x"
            let funName :: Name
funName = FreeFoilConfig -> Name -> Name
toFreeFoilNameTo FreeFoilConfig
config Name
rawTermName
            ([Pat]
pats, [Exp]
exps, Exp -> Exp
wrap, Name
scope', Name
env') <- Name
-> Name
-> Name
-> Name
-> [Type]
-> Q ([Pat], [Exp], Exp -> Exp, Name, Name)
goArgTypes Name
theScope Name
theEnv Name
scope Name
env [Type]
ts
            ([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 (Name -> Pat
VarP Name
x Pat -> [Pat] -> [Pat]
forall a. a -> [a] -> [a]
: [Pat]
pats,
              (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
rawScopeToTermName Exp -> Exp -> Exp
`AppE` Name -> Exp
VarE Name
x)) Exp -> [Exp] -> [Exp]
forall a. a -> [a] -> [a]
: [Exp]
exps,
              Exp -> Exp
wrap, Name
scope', Name
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
            Name
x <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"x"
            ([Pat]
pats, [Exp]
exps, Exp -> Exp
wrap, Name
scope', Name
env') <- Name
-> Name
-> Name
-> Name
-> [Type]
-> Q ([Pat], [Exp], Exp -> Exp, Name, Name)
goArgTypes Name
theScope Name
theEnv Name
scope Name
env [Type]
ts
            ([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 (Name -> Pat
VarP Name
x Pat -> [Pat] -> [Pat]
forall a. a -> [a] -> [a]
: [Pat]
pats, (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]
forall a. a -> [a] -> [a]
: [Exp]
exps, Exp -> Exp
wrap, Name
scope', Name
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
            Name
x <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"x"
            ([Pat]
pats, [Exp]
exps, Exp -> Exp
wrap, Name
scope', Name
env') <- Name
-> Name
-> Name
-> Name
-> [Type]
-> Q ([Pat], [Exp], Exp -> Exp, Name, Name)
goArgTypes Name
theScope Name
theEnv Name
scope Name
env [Type]
ts
            ([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 (Name -> Pat
VarP Name
x Pat -> [Pat] -> [Pat]
forall a. a -> [a] -> [a]
: [Pat]
pats, Exp -> Exp -> Exp
AppE (Exp -> Exp -> Exp
AppE (Name -> Exp
VarE 'fmap) (Name -> Exp
VarE Name
funName Exp -> Exp -> Exp
`AppE` Name -> Exp
VarE Name
theScope Exp -> Exp -> Exp
`AppE` Name -> Exp
VarE Name
theEnv)) (Name -> Exp
VarE Name
x) Exp -> [Exp] -> [Exp]
forall a. a -> [a] -> [a]
: [Exp]
exps, Exp -> Exp
wrap, Name
scope', Name
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
            Name
x <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"x"
            ([Pat]
pats, [Exp]
exps, Exp -> Exp
wrap, Name
scope', Name
env') <- Name
-> Name
-> Name
-> Name
-> [Type]
-> Q ([Pat], [Exp], Exp -> Exp, Name, Name)
goArgTypes Name
theScope Name
theEnv Name
scope Name
env [Type]
ts
            ([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 (Name -> Pat
VarP Name
x Pat -> [Pat] -> [Pat]
forall a. a -> [a] -> [a]
: [Pat]
pats, Exp -> Exp -> Exp
AppE (Exp -> Exp -> Exp
AppE (Name -> Exp
VarE 'fmap) (Name -> Exp
VarE Name
funName Exp -> Exp -> Exp
`AppE` Name -> Exp
VarE Name
theScope Exp -> Exp -> Exp
`AppE` Name -> Exp
VarE Name
theEnv)) (Name -> Exp
VarE Name
x) Exp -> [Exp] -> [Exp]
forall a. a -> [a] -> [a]
: [Exp]
exps, Exp -> Exp
wrap, Name
scope', Name
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
            Name
x <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"x"
            ([Pat]
pats, [Exp]
exps, Exp -> Exp
wrap, Name
scope', Name
env') <- Name
-> Name
-> Name
-> Name
-> [Type]
-> Q ([Pat], [Exp], Exp -> Exp, Name, Name)
goArgTypes Name
theScope Name
theEnv Name
scope Name
env [Type]
ts
            ([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 (Name -> Pat
VarP Name
x Pat -> [Pat] -> [Pat]
forall a. a -> [a] -> [a]
: [Pat]
pats, Exp -> Exp -> Exp
AppE (Exp -> Exp -> Exp
AppE (Name -> Exp
VarE 'fmap) (Name -> Exp
VarE Name
funName Exp -> Exp -> Exp
`AppE` Name -> Exp
VarE Name
scope' Exp -> Exp -> Exp
`AppE` Name -> Exp
VarE Name
env')) (Name -> Exp
VarE Name
x) Exp -> [Exp] -> [Exp]
forall a. a -> [a] -> [a]
: [Exp]
exps, Exp -> Exp
wrap, Name
scope', Name
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
            Name
x <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"x"
            ([Pat]
pats, [Exp]
exps, Exp -> Exp
wrap, Name
scope', Name
env') <- Name
-> Name
-> Name
-> Name
-> [Type]
-> Q ([Pat], [Exp], Exp -> Exp, Name, Name)
goArgTypes Name
theScope Name
theEnv Name
scope Name
env [Type]
ts
            ([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 (Name -> Pat
VarP Name
x Pat -> [Pat] -> [Pat]
forall a. a -> [a] -> [a]
: [Pat]
pats, Exp -> Exp -> Exp
AppE (Exp -> Exp -> Exp
AppE (Name -> Exp
VarE 'fmap) (Name -> Exp
VarE Name
funName Exp -> Exp -> Exp
`AppE` Name -> Exp
VarE Name
scope' Exp -> Exp -> Exp
`AppE` Name -> Exp
VarE Name
env')) (Name -> Exp
VarE Name
x) Exp -> [Exp] -> [Exp]
forall a. a -> [a] -> [a]
: [Exp]
exps, Exp -> Exp
wrap, Name
scope', Name
env')
      Type
_ -> do
        Name
x <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"_x"
        ([Pat]
pats, [Exp]
exps, Exp -> Exp
wrap, Name
scope', Name
env') <- Name
-> Name
-> Name
-> Name
-> [Type]
-> Q ([Pat], [Exp], Exp -> Exp, Name, Name)
goArgTypes Name
theScope Name
theEnv Name
scope Name
env [Type]
ts
        ([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 (Name -> Pat
VarP Name
x Pat -> [Pat] -> [Pat]
forall a. a -> [a] -> [a]
: [Pat]
pats, Name -> Exp
VarE Name
x Exp -> [Exp] -> [Exp]
forall a. a -> [a] -> [a]
: [Exp]
exps, Exp -> Exp
wrap, Name
scope', Name
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
        Name
scope <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"_scope"
        Name
env <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"_env"
        [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
          let newConName :: Name
newConName = FreeFoilConfig -> Name -> Name
toConName FreeFoilConfig
config Name
conName
          ([Pat]
pats, [Exp]
exps, Exp -> Exp
wrap, Name
_scope', Name
_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)
          [Clause] -> Q [Clause]
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return
            [ [Pat] -> Body -> [Dec] -> Clause
Clause [Name -> Pat
VarP Name
scope, Name -> Pat
VarP Name
env, Name -> [Type] -> [Pat] -> Pat
ConP Name
conName [] [Pat]
pats]
                (Exp -> Body
NormalB (Exp -> Exp
wrap ((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
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
            Name
x <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"_x"
            Name
x' <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"_x'"
            Name
scope' <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"_scope"
            Name
env' <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"_env"
            let funName :: Name
funName = FreeFoilConfig -> Name -> Name
toFreeFoilNameTo FreeFoilConfig
config Name
typeName
            ([Pat]
pats, [Exp]
exps, Exp -> Exp
wrap, Name
scope'', Name
env'') <- Name -> Name -> [Type] -> Q ([Pat], [Exp], Exp -> Exp, Name, Name)
goArgTypes Name
scope' Name
env' [Type]
ts
            ([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 (Name -> Pat
VarP Name
x Pat -> [Pat] -> [Pat]
forall a. a -> [a] -> [a]
: [Pat]
pats, Name -> Exp
VarE Name
x' Exp -> [Exp] -> [Exp]
forall a. a -> [a] -> [a]
: [Exp]
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)), Name
scope'', Name
env'')
        | Name
typeName Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
rawScopeName -> do
            Name
x <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"_x"
            let funName :: Name
funName = FreeFoilConfig -> Name -> Name
toFreeFoilNameTo FreeFoilConfig
config Name
rawTermName
            ([Pat]
pats, [Exp]
exps, Exp -> Exp
wrap, Name
scope', Name
env') <- Name -> Name -> [Type] -> Q ([Pat], [Exp], Exp -> Exp, Name, Name)
goArgTypes Name
scope Name
env [Type]
ts
            ([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 (Name -> Pat
VarP Name
x Pat -> [Pat] -> [Pat]
forall a. a -> [a] -> [a]
: [Pat]
pats,
              (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
rawScopeToTermName Exp -> Exp -> Exp
`AppE` Name -> Exp
VarE Name
x)) Exp -> [Exp] -> [Exp]
forall a. a -> [a] -> [a]
: [Exp]
exps,
              Exp -> Exp
wrap, Name
scope', Name
env')
        | Name
typeName Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
rawTermName -> do
            Name
x <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"_x"
            let funName :: Name
funName = FreeFoilConfig -> Name -> Name
toFreeFoilNameTo FreeFoilConfig
config Name
rawTermName
            ([Pat]
pats, [Exp]
exps, Exp -> Exp
wrap, Name
scope', Name
env') <- Name -> Name -> [Type] -> Q ([Pat], [Exp], Exp -> Exp, Name, Name)
goArgTypes Name
scope Name
env [Type]
ts
            ([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 (Name -> Pat
VarP Name
x Pat -> [Pat] -> [Pat]
forall a. a -> [a] -> [a]
: [Pat]
pats,
              (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]
forall a. a -> [a] -> [a]
: [Exp]
exps,
              Exp -> Exp
wrap, Name
scope', Name
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
            Name
x <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"_x"
            let funName :: Name
funName = FreeFoilConfig -> Name -> Name
toFreeFoilNameTo FreeFoilConfig
config Name
typeName
            ([Pat]
pats, [Exp]
exps, Exp -> Exp
wrap, Name
scope', Name
env') <- Name -> Name -> [Type] -> Q ([Pat], [Exp], Exp -> Exp, Name, Name)
goArgTypes Name
scope Name
env [Type]
ts
            ([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 (Name -> Pat
VarP Name
x Pat -> [Pat] -> [Pat]
forall a. a -> [a] -> [a]
: [Pat]
pats,
              (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]
forall a. a -> [a] -> [a]
: [Exp]
exps,
              Exp -> Exp
wrap, Name
scope', Name
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
            Name
x <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"_x"
            ([Pat]
pats, [Exp]
exps, Exp -> Exp
wrap, Name
scope', Name
env') <- Name -> Name -> [Type] -> Q ([Pat], [Exp], Exp -> Exp, Name, Name)
goArgTypes Name
scope Name
env [Type]
ts
            ([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 (Name -> Pat
VarP Name
x Pat -> [Pat] -> [Pat]
forall a. a -> [a] -> [a]
: [Pat]
pats,
              (Name -> Exp
VarE 'fmap Exp -> Exp -> Exp
`AppE` (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]
forall a. a -> [a] -> [a]
: [Exp]
exps,
              Exp -> Exp
wrap, Name
scope', Name
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
            Name
x <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"_x"
            ([Pat]
pats, [Exp]
exps, Exp -> Exp
wrap, Name
scope', Name
env') <- Name -> Name -> [Type] -> Q ([Pat], [Exp], Exp -> Exp, Name, Name)
goArgTypes Name
scope Name
env [Type]
ts
            ([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 (Name -> Pat
VarP Name
x Pat -> [Pat] -> [Pat]
forall a. a -> [a] -> [a]
: [Pat]
pats,
              (Name -> Exp
VarE 'fmap Exp -> Exp -> Exp
`AppE` (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]
forall a. a -> [a] -> [a]
: [Exp]
exps,
              Exp -> Exp
wrap, Name
scope', Name
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
            Name
x <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"_x"
            ([Pat]
pats, [Exp]
exps, Exp -> Exp
wrap, Name
scope', Name
env') <- Name -> Name -> [Type] -> Q ([Pat], [Exp], Exp -> Exp, Name, Name)
goArgTypes Name
scope Name
env [Type]
ts
            ([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 (Name -> Pat
VarP Name
x Pat -> [Pat] -> [Pat]
forall a. a -> [a] -> [a]
: [Pat]
pats,
              (Name -> Exp
VarE 'fmap Exp -> Exp -> Exp
`AppE` (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]
forall a. a -> [a] -> [a]
: [Exp]
exps,
              Exp -> Exp
wrap, Name
scope', Name
env')
      Type
_ -> do
        Name
x <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"_x"
        ([Pat]
pats, [Exp]
exps, Exp -> Exp
wrap, Name
scope', Name
env') <- Name -> Name -> [Type] -> Q ([Pat], [Exp], Exp -> Exp, Name, Name)
goArgTypes Name
scope Name
env [Type]
ts
        ([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 (Name -> Pat
VarP Name
x Pat -> [Pat] -> [Pat]
forall a. a -> [a] -> [a]
: [Pat]
pats, Name -> Exp
VarE Name
x Exp -> [Exp] -> [Exp]
forall a. a -> [a] -> [a]
: [Exp]
exps, Exp -> Exp
wrap, Name
scope', Name
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
        Name
scope <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"_scope"
        Name
env <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"_env"
        [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
          let newConName :: Name
newConName = FreeFoilConfig -> Name -> Name
toConName FreeFoilConfig
config Name
conName
          ([Pat]
pats, [Exp]
exps, Exp -> Exp
wrap, Name
_scope', Name
_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)
          [Clause] -> Q [Clause]
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return
            [ [Pat] -> Body -> [Dec] -> Clause
Clause [Name -> Pat
VarP Name
scope, Name -> Pat
VarP Name
env, Name -> [Type] -> [Pat] -> Pat
ConP Name
conName [] [Pat]
pats]
                (Exp -> Body
NormalB (Exp -> Exp
wrap ((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
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 -> [Type] -> Q ([Pat], [Exp], Exp -> Exp, Name)
    goArgTypes :: Name -> Name -> [Type] -> Q ([Pat], [Exp], Exp -> Exp, Name)
goArgTypes 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
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
            Name
x <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"_x"
            Name
x' <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"_x'"
            Name
scope' <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"_scope"
            Name
env' <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"_env"
            ([Pat]
pats, [Exp]
exps, Exp -> Exp
wrap, Name
env'') <- Name -> Name -> [Type] -> Q ([Pat], [Exp], Exp -> Exp, Name)
goArgTypes Name
scope' Name
env' [Type]
ts
            ([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 (Name -> Pat
VarP Name
x Pat -> [Pat] -> [Pat]
forall a. a -> [a] -> [a]
: [Pat]
pats, Name -> Exp
VarE Name
x' Exp -> [Exp] -> [Exp]
forall a. a -> [a] -> [a]
: [Exp]
exps, \Exp
e ->
              Name -> Exp
VarE 'Foil.withFresh 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)), Name
env'')
        | Name
typeName Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
rawBindingName -> do
            Name
x <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"_x"
            Name
x' <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"_x'"
            Name
scope' <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"_scope"
            Name
env' <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"_env"
            let funName :: Name
funName = FreeFoilConfig -> Name -> Name
toFreeFoilNameTo FreeFoilConfig
config Name
typeName
            ([Pat]
pats, [Exp]
exps, Exp -> Exp
wrap, Name
env'') <- Name -> Name -> [Type] -> Q ([Pat], [Exp], Exp -> Exp, Name)
goArgTypes Name
scope' Name
env' [Type]
ts
            ([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 (Name -> Pat
VarP Name
x Pat -> [Pat] -> [Pat]
forall a. a -> [a] -> [a]
: [Pat]
pats, Name -> Exp
VarE Name
x' Exp -> [Exp] -> [Exp]
forall a. a -> [a] -> [a]
: [Exp]
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)), Name
env'')
      Type
_ -> do
        Name
x <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"_x"
        ([Pat]
pats, [Exp]
exps, Exp -> Exp
wrap, Name
env') <- Name -> Name -> [Type] -> Q ([Pat], [Exp], Exp -> Exp, Name)
goArgTypes Name
scope Name
env [Type]
ts
        ([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 (Name -> Pat
VarP Name
x Pat -> [Pat] -> [Pat]
forall a. a -> [a] -> [a]
: [Pat]
pats, Name -> Exp
VarE Name
x Exp -> [Exp] -> [Exp]
forall a. a -> [a] -> [a]
: [Exp]
exps, Exp -> Exp
wrap, Name
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
        Name
scope <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"_scope"
        Name
env <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"_env"
        Name
cont <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"_cont"
        [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
          let newConName :: Name
newConName = FreeFoilConfig -> Name -> Name
toConName FreeFoilConfig
config Name
conName
          ([Pat]
pats, [Exp]
exps, Exp -> Exp
wrap, Name
env') <- Name -> Name -> [Type] -> Q ([Pat], [Exp], Exp -> Exp, 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)
          [Clause] -> Q [Clause]
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return
            [ [Pat] -> Body -> [Dec] -> Clause
Clause [Name -> Pat
VarP Name
scope, Name -> Pat
VarP Name
env, Name -> [Type] -> [Pat] -> Pat
ConP Name
conName [] [Pat]
pats, Name -> Pat
VarP Name
cont]
                (Exp -> Body
NormalB (Exp -> Exp
wrap (Name -> Exp
VarE Name
cont 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 Exp -> Exp -> Exp
`AppE` Name -> Exp
VarE Name
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
    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
            Name
binder <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"binder"
            Name
body <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"body"
            ([Pat], [Exp]) -> Q ([Pat], [Exp])
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Name -> Pat
VarP Name
binder, Name -> Pat
VarP Name
body], [[Maybe Exp] -> Exp
TupE [Exp -> Maybe Exp
forall a. a -> Maybe a
Just (Name -> Exp
VarE Name
binder), Exp -> Maybe Exp
forall a. a -> Maybe a
Just (Name -> Exp
VarE Name
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
            Name
x <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"_x"
            ([Pat], [Exp]) -> Q ([Pat], [Exp])
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Name -> Pat
VarP Name
x], [Exp -> Exp -> Exp
AppE (Name -> Exp
VarE Name
funName) (Name -> Exp
VarE Name
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
            Name
x <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"_x"
            ([Pat], [Exp]) -> Q ([Pat], [Exp])
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Name -> Pat
VarP Name
x], [Exp -> Exp -> Exp
AppE (Name -> Exp
VarE Name
funName) (Name -> Exp
VarE Name
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
            Name
x <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"_x"
            ([Pat], [Exp]) -> Q ([Pat], [Exp])
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Name -> Pat
VarP Name
x], [Exp -> Exp -> Exp
AppE (Exp -> Exp -> Exp
AppE (Name -> Exp
VarE 'fmap) (Name -> Exp
VarE Name
funName)) (Name -> Exp
VarE Name
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
            Name
x <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"_x"
            ([Pat], [Exp]) -> Q ([Pat], [Exp])
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Name -> Pat
VarP Name
x], [Exp -> Exp -> Exp
AppE (Exp -> Exp -> Exp
AppE (Name -> Exp
VarE 'fmap) (Name -> Exp
VarE Name
funName)) (Name -> Exp
VarE Name
x)])
      Type
_ -> do
        Name
x <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"_x"
        ([Pat], [Exp]) -> Q ([Pat], [Exp])
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Name -> Pat
VarP Name
x], [Name -> Exp
VarE Name
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
        Name
theIdent <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"_theRawIdent"
        [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
          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
          ([[Pat]] -> [Pat]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat -> [Pat]
pats, [[Exp]] -> [Exp]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat -> [Exp]
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 -> Type -> Q ([Pat], [Exp])
fromArgType Bool
isVarCon Name
theIdent (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
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
  ([TyVarBndr BndrVis]
_tvars, [Con]
cons) <- Name -> Q ([TyVarBndr BndrVis], [Con])
reifyDataOrNewtype Name
rawName
  [Name] -> Q [Name]
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Name] -> [Name]
forall a. Eq a => [a] -> [a]
nub ((Con -> [Name]) -> [Con] -> [Name]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Con -> [Name]
go [Con]
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