{-# OPTIONS_GHC -fno-warn-type-defaults      #-}
{-# LANGUAGE LambdaCase      #-}
{-# LANGUAGE TemplateHaskell #-}
module Control.Monad.Free.Foil.TH.Convert where

import           Language.Haskell.TH
import           Language.Haskell.TH.Syntax

import           Control.Monad.Foil.TH.Util

-- * Bulk generators

-- | Generate helpers for conversion to scope-safe representation.
-- Includes 'mkConvertToSig', 'mkGetPatternBinder', and 'mkGetScopedTerm'.
mkConvertToFreeFoil
  :: Name -- ^ Type name for raw terms.
  -> Name -- ^ Type name for raw variable identifiers.
  -> Name -- ^ Type name for raw scoped terms.
  -> Name -- ^ Type name for raw patterns.
  -> Q [Dec]
mkConvertToFreeFoil :: Name -> Name -> Name -> Name -> Q [Dec]
mkConvertToFreeFoil Name
termT Name
nameT Name
scopeT Name
patternT = [[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 -> Name -> Name -> Name -> Q [Dec]
mkConvertToSig Name
termT Name
nameT Name
scopeT Name
patternT
  , Name -> Name -> Q [Dec]
mkGetPatternBinder Name
nameT Name
patternT
  , Name -> Name -> Q [Dec]
mkGetScopedTerm Name
termT Name
scopeT
  ]

-- | Generate helpers for conversion from scope-safe representation.
-- Includes 'mkConvertFromSig'.
mkConvertFromFreeFoil
  :: Name -- ^ Type name for raw terms.
  -> Name -- ^ Type name for raw variable identifiers.
  -> Name -- ^ Type name for raw scoped terms.
  -> Name -- ^ Type name for raw patterns.
  -> Q [Dec]
mkConvertFromFreeFoil :: Name -> Name -> Name -> Name -> Q [Dec]
mkConvertFromFreeFoil Name
termT Name
nameT Name
scopeT Name
patternT = [[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 -> Name -> Name -> Name -> Q [Dec]
mkConvertFromSig Name
termT Name
nameT Name
scopeT Name
patternT
  ]

-- * Individual generators

-- | Generate conversion helper that goes unpeels one node from a raw term.
mkConvertToSig
  :: Name -- ^ Type name for raw terms.
  -> Name -- ^ Type name for raw variable identifiers.
  -> Name -- ^ Type name for raw scoped terms.
  -> Name -- ^ Type name for raw patterns.
  -> Q [Dec]
mkConvertToSig :: Name -> Name -> Name -> Name -> Q [Dec]
mkConvertToSig Name
termT Name
nameT Name
scopeT Name
patternT = do
  TyConI (DataD Cxt
_ctx Name
_name [TyVarBndr BndrVis]
termTVars Maybe Kind
_kind [Con]
termCons [DerivClause]
_deriv) <- Name -> Q Info
reify Name
termT
  TyConI (NewtypeD Cxt
_ctx Name
_name [TyVarBndr BndrVis]
nameTVars Maybe Kind
_kind Con
_nameCons [DerivClause]
_deriv) <- Name -> Q Info
reify Name
nameT

  [Clause]
convertTermToSigClauses <- [[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 Con -> Q [Clause]
toClause [Con]
termCons

  let params :: Cxt
params = (TyVarBndr BndrVis -> Kind) -> [TyVarBndr BndrVis] -> Cxt
forall a b. (a -> b) -> [a] -> [b]
map (Name -> Kind
VarT (Name -> Kind)
-> (TyVarBndr BndrVis -> Name) -> TyVarBndr BndrVis -> Kind
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyVarBndr BndrVis -> Name
forall a. TyVarBndr a -> Name
tvarName) [TyVarBndr BndrVis]
termTVars
      termType :: Q Kind
termType = Kind -> Q Kind
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return (Kind -> Q Kind) -> Kind -> Q Kind
forall a b. (a -> b) -> a -> b
$ Name -> Cxt -> Kind
PeelConT Name
termT Cxt
params
      nameType :: Q Kind
nameType = Kind -> Q Kind
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return (Kind -> Q Kind) -> Kind -> Q Kind
forall a b. (a -> b) -> a -> b
$ Name -> Cxt -> Kind
PeelConT Name
nameT ((TyVarBndr BndrVis -> Kind) -> [TyVarBndr BndrVis] -> Cxt
forall a b. (a -> b) -> [a] -> [b]
map (Name -> Kind
VarT (Name -> Kind)
-> (TyVarBndr BndrVis -> Name) -> TyVarBndr BndrVis -> Kind
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyVarBndr BndrVis -> Name
forall a. TyVarBndr a -> Name
tvarName) [TyVarBndr BndrVis]
nameTVars)
      scopeType :: Q Kind
scopeType = Kind -> Q Kind
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return (Kind -> Q Kind) -> Kind -> Q Kind
forall a b. (a -> b) -> a -> b
$ Name -> Cxt -> Kind
PeelConT Name
scopeT Cxt
params
      patternType :: Q Kind
patternType = Kind -> Q Kind
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return (Kind -> Q Kind) -> Kind -> Q Kind
forall a b. (a -> b) -> a -> b
$ Name -> Cxt -> Kind
PeelConT Name
patternT Cxt
params
      signatureType :: Q Kind
signatureType = Kind -> Q Kind
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return (Kind -> Q Kind) -> Kind -> Q Kind
forall a b. (a -> b) -> a -> b
$ Name -> Cxt -> Kind
PeelConT Name
signatureT Cxt
params
  Kind
convertTermToSigClausesType <-
    [t| $Q Kind
termType -> Either $Q Kind
nameType ($Q Kind
signatureType ($Q Kind
patternType, $Q Kind
scopeType) $Q Kind
termType) |]

  Q () -> Q ()
addModFinalizer (Q () -> Q ()) -> Q () -> Q ()
forall a b. (a -> b) -> a -> b
$ DocLoc -> String -> Q ()
putDoc (Name -> DocLoc
DeclDoc Name
convertTermToSigT)
    (String
"/Generated/ with '" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show 'mkConvertToSig String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"'. Perform one step of converting '" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
termT String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"', peeling off one node of type '" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
signatureT 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
    [ Name -> Kind -> Dec
SigD Name
convertTermToSigT Kind
convertTermToSigClausesType
    , Name -> [Clause] -> Dec
FunD Name
convertTermToSigT [Clause]
convertTermToSigClauses
    ]
  where
    signatureT :: Name
signatureT = String -> Name
mkName (Name -> String
nameBase Name
termT String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"Sig")
    convertTermToSigT :: Name
convertTermToSigT = String -> Name
mkName (String
"convertTo" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
nameBase Name
signatureT)

    toClause :: Con -> Q [Clause]
    toClause :: Con -> Q [Clause]
toClause = \case
      NormalC Name
conName [BangType]
types | (Pat -> Bool) -> [Pat] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Pat -> Bool
isVarP [Pat]
pats
        -> [Clause] -> Q [Clause]
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return [[Pat] -> Body -> [Dec] -> Clause
Clause [Name -> Cxt -> [Pat] -> Pat
ConP Name
conName [] [Pat]
pats] (Exp -> Body
NormalB (Exp -> Exp -> Exp
AppE (Name -> Exp
ConE 'Left) (Name -> Exp
VarE Name
x))) []]
        where
          x :: Name
x = String -> Name
mkName String
"x"
          isVarP :: Pat -> Bool
isVarP VarP{} = Bool
True
          isVarP Pat
_      = Bool
False
          pats :: [Pat]
pats =
            [ case Kind
type_ of
                PeelConT Name
typeName Cxt
_ | Name
typeName Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
nameT -> Name -> Pat
VarP Name
x
                Kind
_                                       -> Pat
WildP
            | (Bang
_bang, Kind
type_) <- [BangType]
types ]
      NormalC Name
conName [BangType]
types -> Name -> Name -> [BangType] -> Q [Clause]
forall {m :: * -> *} {a}.
Monad m =>
Name -> Name -> [(a, Kind)] -> m [Clause]
mkClause Name
conName Name
conName' [BangType]
types
        where
          conName' :: Name
conName' = String -> Name
mkName (Name -> String
nameBase Name
conName String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"Sig")
      RecC Name
conName [VarBangType]
types -> Con -> Q [Clause]
toClause (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 -> Name -> Name -> [BangType] -> Q [Clause]
forall {m :: * -> *} {a}.
Monad m =>
Name -> Name -> [(a, Kind)] -> m [Clause]
mkClause Name
conName Name
conName' [BangType
l, BangType
r]
        where
          conName' :: Name
conName' = String -> Name
mkName (Name -> String
nameBase Name
conName String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"---")
      ForallC [TyVarBndr Specificity]
_ Cxt
_ Con
con -> Con -> Q [Clause]
toClause Con
con
      GadtC [Name]
conNames [BangType]
types Kind
_retType -> [[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
<$> (Name -> Q [Clause]) -> [Name] -> 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
conName -> Con -> Q [Clause]
toClause (Name -> [BangType] -> Con
NormalC Name
conName [BangType]
types)) [Name]
conNames
      RecGadtC [Name]
conNames [VarBangType]
types Kind
retType -> Con -> Q [Clause]
toClause ([Name] -> [BangType] -> Kind -> Con
GadtC [Name]
conNames ((VarBangType -> BangType) -> [VarBangType] -> [BangType]
forall a b. (a -> b) -> [a] -> [b]
map VarBangType -> BangType
removeName [VarBangType]
types) Kind
retType)

    mkClause :: Name -> Name -> [(a, Kind)] -> m [Clause]
mkClause Name
conName Name
conName' [(a, Kind)]
types = [Clause] -> m [Clause]
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return
      [ [Pat] -> Body -> [Dec] -> Clause
Clause [Name -> Cxt -> [Pat] -> Pat
ConP Name
conName [] [Pat]
pats] (Exp -> Body
NormalB (Exp -> Exp -> Exp
AppE (Name -> Exp
ConE 'Right) ((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]] -> [Exp]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[Exp]]
args)))) [] ]
      where
        p :: Name
p = String -> Name
mkName String
"p"
        ([Pat]
pats, [[Exp]]
args) = [(Pat, [Exp])] -> ([Pat], [[Exp]])
forall a b. [(a, b)] -> ([a], [b])
unzip
          [ case Kind
type_ of
              PeelConT Name
typeName Cxt
_
                | Name
typeName Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
patternT -> (Name -> Pat
VarP Name
p, [])
                | Name
typeName Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
scopeT -> (Name -> Pat
VarP Name
x, [[Maybe Exp] -> Exp
TupE [Exp -> Maybe Exp
forall a. a -> Maybe a
Just (Name -> Exp
VarE Name
p), Exp -> Maybe Exp
forall a. a -> Maybe a
Just (Name -> Exp
VarE Name
x)]])
              Kind
_ -> (Name -> Pat
VarP Name
x, [Name -> Exp
VarE Name
x])
          | (Integer
i, (a
_bang, Kind
type_)) <- [Integer] -> [(a, Kind)] -> [(Integer, (a, Kind))]
forall a b. [a] -> [b] -> [(a, b)]
zip [Integer
0..] [(a, Kind)]
types
          , let x :: Name
x = String -> Name
mkName (String
"x" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
i)
          ]

-- | Generate conversion helper that peels back one node to a raw term.
mkConvertFromSig
  :: Name -- ^ Type name for raw terms.
  -> Name -- ^ Type name for raw variable identifiers.
  -> Name -- ^ Type name for raw scoped terms.
  -> Name -- ^ Type name for raw patterns.
  -> Q [Dec]
mkConvertFromSig :: Name -> Name -> Name -> Name -> Q [Dec]
mkConvertFromSig Name
termT Name
nameT Name
scopeT Name
patternT = do
  TyConI (DataD Cxt
_ctx Name
_name [TyVarBndr BndrVis]
termTVars Maybe Kind
_kind [Con]
termCons [DerivClause]
_deriv) <- Name -> Q Info
reify Name
termT
  TyConI (NewtypeD Cxt
_ctx Name
_name [TyVarBndr BndrVis]
_nameTVars Maybe Kind
_kind Con
_nameCons [DerivClause]
_deriv) <- Name -> Q Info
reify Name
nameT

  [Clause]
convertTermFromSigClauses <- [[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 Con -> Q [Clause]
toClause [Con]
termCons

  let params :: Cxt
params = (TyVarBndr BndrVis -> Kind) -> [TyVarBndr BndrVis] -> Cxt
forall a b. (a -> b) -> [a] -> [b]
map (Name -> Kind
VarT (Name -> Kind)
-> (TyVarBndr BndrVis -> Name) -> TyVarBndr BndrVis -> Kind
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyVarBndr BndrVis -> Name
forall a. TyVarBndr a -> Name
tvarName) [TyVarBndr BndrVis]
termTVars
      termType :: Q Kind
termType = Kind -> Q Kind
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return (Kind -> Q Kind) -> Kind -> Q Kind
forall a b. (a -> b) -> a -> b
$ Name -> Cxt -> Kind
PeelConT Name
termT Cxt
params
      scopeType :: Q Kind
scopeType = Kind -> Q Kind
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return (Kind -> Q Kind) -> Kind -> Q Kind
forall a b. (a -> b) -> a -> b
$ Name -> Cxt -> Kind
PeelConT Name
scopeT Cxt
params
      patternType :: Q Kind
patternType = Kind -> Q Kind
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return (Kind -> Q Kind) -> Kind -> Q Kind
forall a b. (a -> b) -> a -> b
$ Name -> Cxt -> Kind
PeelConT Name
patternT Cxt
params
      signatureType :: Q Kind
signatureType = Kind -> Q Kind
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return (Kind -> Q Kind) -> Kind -> Q Kind
forall a b. (a -> b) -> a -> b
$ Name -> Cxt -> Kind
PeelConT Name
signatureT Cxt
params
  Kind
convertTermFromSigClausesType <-
    [t| $Q Kind
signatureType ($Q Kind
patternType, $Q Kind
scopeType) $Q Kind
termType -> $Q Kind
termType |]

  Q () -> Q ()
addModFinalizer (Q () -> Q ()) -> Q () -> Q ()
forall a b. (a -> b) -> a -> b
$ DocLoc -> String -> Q ()
putDoc (Name -> DocLoc
DeclDoc Name
convertTermFromSigT)
    (String
"/Generated/ with '" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show 'mkConvertFromSig String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"'. Perform one step of converting '" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
termT String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"', peeling off one node of type '" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
signatureT 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
    [ Name -> Kind -> Dec
SigD Name
convertTermFromSigT Kind
convertTermFromSigClausesType
    , Name -> [Clause] -> Dec
FunD Name
convertTermFromSigT [Clause]
convertTermFromSigClauses
    ]
  where
    signatureT :: Name
signatureT = String -> Name
mkName (Name -> String
nameBase Name
termT String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"Sig")
    convertTermFromSigT :: Name
convertTermFromSigT = String -> Name
mkName (String
"convertFrom" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
nameBase Name
signatureT)

    toClause :: Con -> Q [Clause]
    toClause :: Con -> Q [Clause]
toClause = \case
      NormalC Name
_conName [BangType]
types | [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
or [ Name
typeName Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
nameT | (Bang
_bang, PeelConT Name
typeName Cxt
_typeParams) <- [BangType]
types ]
        -> [Clause] -> Q [Clause]
forall a. a -> Q a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
      NormalC Name
conName [BangType]
types -> Name -> Name -> [BangType] -> Q [Clause]
forall {m :: * -> *} {a}.
Monad m =>
Name -> Name -> [(a, Kind)] -> m [Clause]
mkClause Name
conName Name
conName' [BangType]
types
        where
          conName' :: Name
conName' = String -> Name
mkName (Name -> String
nameBase Name
conName String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"Sig")
      RecC Name
conName [VarBangType]
types -> Con -> Q [Clause]
toClause (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 -> Name -> Name -> [BangType] -> Q [Clause]
forall {m :: * -> *} {a}.
Monad m =>
Name -> Name -> [(a, Kind)] -> m [Clause]
mkClause Name
conName Name
conName' [BangType
l, BangType
r]
        where
          conName' :: Name
conName' = String -> Name
mkName (Name -> String
nameBase Name
conName String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"---")
      ForallC [TyVarBndr Specificity]
_ Cxt
_ Con
con -> Con -> Q [Clause]
toClause Con
con
      GadtC [Name]
conNames [BangType]
types Kind
_retType -> [[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
<$> (Name -> Q [Clause]) -> [Name] -> 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
conName -> Con -> Q [Clause]
toClause (Name -> [BangType] -> Con
NormalC Name
conName [BangType]
types)) [Name]
conNames
      RecGadtC [Name]
conNames [VarBangType]
types Kind
retType -> Con -> Q [Clause]
toClause ([Name] -> [BangType] -> Kind -> Con
GadtC [Name]
conNames ((VarBangType -> BangType) -> [VarBangType] -> [BangType]
forall a b. (a -> b) -> [a] -> [b]
map VarBangType -> BangType
removeName [VarBangType]
types) Kind
retType)

    mkClause :: Name -> Name -> [(a, Kind)] -> m [Clause]
mkClause Name
conName Name
conName' [(a, Kind)]
types = [Clause] -> m [Clause]
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return
      [ [Pat] -> Body -> [Dec] -> Clause
Clause [Name -> Cxt -> [Pat] -> Pat
ConP Name
conName' [] ([[Pat]] -> [Pat]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[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
conName) [Exp]
args)) [] ]
      where
        p :: Name
p = String -> Name
mkName String
"p"
        ([Exp]
args, [[Pat]]
pats) = [(Exp, [Pat])] -> ([Exp], [[Pat]])
forall a b. [(a, b)] -> ([a], [b])
unzip
          [ case Kind
type_ of
              PeelConT Name
typeName Cxt
_
                | Name
typeName Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
patternT -> (Name -> Exp
VarE Name
p, [])
                | Name
typeName Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
scopeT -> (Name -> Exp
VarE Name
x, [[Pat] -> Pat
TupP [Name -> Pat
VarP Name
p, Name -> Pat
VarP Name
x]])
              Kind
_ -> (Name -> Exp
VarE Name
x, [Name -> Pat
VarP Name
x])
          | (Integer
i, (a
_bang, Kind
type_)) <- [Integer] -> [(a, Kind)] -> [(Integer, (a, Kind))]
forall a b. [a] -> [b] -> [(a, b)]
zip [Integer
0..] [(a, Kind)]
types
          , let x :: Name
x = String -> Name
mkName (String
"x" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
i)
          ]

-- | Generate a helper that extracts at most one binder from a pattern.
mkGetPatternBinder
  :: Name -- ^ Type name for raw variable identifiers.
  -> Name -- ^ Type name for raw patterns.
  -> Q [Dec]
mkGetPatternBinder :: Name -> Name -> Q [Dec]
mkGetPatternBinder Name
nameT Name
patternT = do
  TyConI (NewtypeD Cxt
_ctx Name
_name [TyVarBndr BndrVis]
nameTVars Maybe Kind
_kind Con
_nameCons [DerivClause]
_deriv) <- Name -> Q Info
reify Name
nameT
  TyConI (DataD Cxt
_ctx Name
_name [TyVarBndr BndrVis]
patternTVars Maybe Kind
_kind [Con]
patternCons [DerivClause]
_deriv) <- Name -> Q Info
reify Name
patternT

  [Clause]
getPatternBinderClauses <- [[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 Con -> Q [Clause]
toClause [Con]
patternCons

  let nameType :: Q Kind
nameType = Kind -> Q Kind
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return (Kind -> Q Kind) -> Kind -> Q Kind
forall a b. (a -> b) -> a -> b
$ Name -> Cxt -> Kind
PeelConT Name
nameT ((TyVarBndr BndrVis -> Kind) -> [TyVarBndr BndrVis] -> Cxt
forall a b. (a -> b) -> [a] -> [b]
map (Name -> Kind
VarT (Name -> Kind)
-> (TyVarBndr BndrVis -> Name) -> TyVarBndr BndrVis -> Kind
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyVarBndr BndrVis -> Name
forall a. TyVarBndr a -> Name
tvarName) [TyVarBndr BndrVis]
nameTVars)
      patternType :: Q Kind
patternType = Kind -> Q Kind
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return (Kind -> Q Kind) -> Kind -> Q Kind
forall a b. (a -> b) -> a -> b
$ Name -> Cxt -> Kind
PeelConT Name
patternT ((TyVarBndr BndrVis -> Kind) -> [TyVarBndr BndrVis] -> Cxt
forall a b. (a -> b) -> [a] -> [b]
map (Name -> Kind
VarT (Name -> Kind)
-> (TyVarBndr BndrVis -> Name) -> TyVarBndr BndrVis -> Kind
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyVarBndr BndrVis -> Name
forall a. TyVarBndr a -> Name
tvarName) [TyVarBndr BndrVis]
patternTVars)
  Kind
getPatternBinderClausesType <-
    [t| $Q Kind
patternType -> Maybe $Q Kind
nameType |]

  Q () -> Q ()
addModFinalizer (Q () -> Q ()) -> Q () -> Q ()
forall a b. (a -> b) -> a -> b
$ DocLoc -> String -> Q ()
putDoc (Name -> DocLoc
DeclDoc Name
getPatternBinderT)
    (String
"/Generated/ with '" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show 'mkGetPatternBinder String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"'. Extract at most one binder from a pattern or __crash__.")
  [Dec] -> Q [Dec]
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return
    [ Name -> Kind -> Dec
SigD Name
getPatternBinderT Kind
getPatternBinderClausesType
    , Name -> [Clause] -> Dec
FunD Name
getPatternBinderT [Clause]
getPatternBinderClauses
    ]
  where
    getPatternBinderT :: Name
getPatternBinderT = String -> Name
mkName (String
"get" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
nameBase Name
patternT String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"Binder")

    toClause :: Con -> Q [Clause]
    toClause :: Con -> Q [Clause]
toClause = \case
      NormalC Name
conName [BangType]
types -> Name -> [BangType] -> Q [Clause]
mkClause Name
conName [BangType]
types
      RecC Name
conName [VarBangType]
types -> Con -> Q [Clause]
toClause (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]
toClause (Name -> [BangType] -> Con
NormalC Name
conName [BangType
l, BangType
r])
      ForallC [TyVarBndr Specificity]
_ Cxt
_ Con
con -> Con -> Q [Clause]
toClause Con
con
      GadtC [Name]
conNames [BangType]
types Kind
_retType -> [[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
<$> (Name -> Q [Clause]) -> [Name] -> 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
conName -> Name -> [BangType] -> Q [Clause]
mkClause Name
conName [BangType]
types) [Name]
conNames
      RecGadtC [Name]
conNames [VarBangType]
types Kind
retType -> Con -> Q [Clause]
toClause ([Name] -> [BangType] -> Kind -> Con
GadtC [Name]
conNames ((VarBangType -> BangType) -> [VarBangType] -> [BangType]
forall a b. (a -> b) -> [a] -> [b]
map VarBangType -> BangType
removeName [VarBangType]
types) Kind
retType)

    mkClause :: Name -> [BangType] -> Q [Clause]
    mkClause :: Name -> [BangType] -> Q [Clause]
mkClause Name
conName [BangType]
types = do
      Exp
body <- case [[Maybe (Q Exp)]] -> [Maybe (Q Exp)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[Maybe (Q Exp)]]
vars of
        []       -> [e| Nothing |]
        [Just Q Exp
y] -> [e| Just $Q Exp
y |]
        [Maybe (Q Exp)]
_        -> [e| error "complex patterns are not supported" |]
      [Clause] -> Q [Clause]
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return [ [Pat] -> Body -> [Dec] -> Clause
Clause [Name -> Cxt -> [Pat] -> Pat
ConP Name
conName [] [Pat]
pats] (Exp -> Body
NormalB Exp
body) [] ]
      where
        x :: Name
x = String -> Name
mkName String
"x"
        ([Pat]
pats, [[Maybe (Q Exp)]]
vars) = [(Pat, [Maybe (Q Exp)])] -> ([Pat], [[Maybe (Q Exp)]])
forall a b. [(a, b)] -> ([a], [b])
unzip
          [ case Kind
type_ of
              PeelConT Name
typeName Cxt
_
                | Name
typeName Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
nameT -> (Name -> Pat
VarP Name
x, [Q Exp -> Maybe (Q Exp)
forall a. a -> Maybe a
Just (Exp -> Q Exp
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> Exp
VarE Name
x))])
                | Name
typeName Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
patternT -> (Pat
WildP, [Maybe (Q Exp)
forall a. Maybe a
Nothing])
              Kind
_ -> (Pat
WildP, [])
          | (Bang
_bang, Kind
type_) <- [BangType]
types
          ]

-- | Generate a helper that extracts a term from a scoped term.
mkGetScopedTerm
  :: Name -- ^ Type name for raw terms.
  -> Name -- ^ Type name for raw scoped terms.
  -> Q [Dec]
mkGetScopedTerm :: Name -> Name -> Q [Dec]
mkGetScopedTerm Name
termT Name
scopeT = do
  TyConI (DataD Cxt
_ctx Name
_name [TyVarBndr BndrVis]
termTVars Maybe Kind
_kind [Con]
_termCons [DerivClause]
_deriv) <- Name -> Q Info
reify Name
termT
  TyConI (DataD Cxt
_ctx Name
_name [TyVarBndr BndrVis]
_scopeTVars Maybe Kind
_kind [Con]
scopeCons [DerivClause]
_deriv) <- Name -> Q Info
reify Name
scopeT

  [Clause]
getScopedTermClauses <- [[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 Con -> Q [Clause]
toClause [Con]
scopeCons

  let params :: Cxt
params = (TyVarBndr BndrVis -> Kind) -> [TyVarBndr BndrVis] -> Cxt
forall a b. (a -> b) -> [a] -> [b]
map (Name -> Kind
VarT (Name -> Kind)
-> (TyVarBndr BndrVis -> Name) -> TyVarBndr BndrVis -> Kind
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyVarBndr BndrVis -> Name
forall a. TyVarBndr a -> Name
tvarName) [TyVarBndr BndrVis]
termTVars
      termType :: Q Kind
termType = Kind -> Q Kind
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return (Kind -> Q Kind) -> Kind -> Q Kind
forall a b. (a -> b) -> a -> b
$ Name -> Cxt -> Kind
PeelConT Name
termT Cxt
params
      scopeType :: Q Kind
scopeType = Kind -> Q Kind
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return (Kind -> Q Kind) -> Kind -> Q Kind
forall a b. (a -> b) -> a -> b
$ Name -> Cxt -> Kind
PeelConT Name
scopeT Cxt
params
  Kind
getScopedTermClausesType <-
    [t| $Q Kind
scopeType -> $Q Kind
termType |]

  Q () -> Q ()
addModFinalizer (Q () -> Q ()) -> Q () -> Q ()
forall a b. (a -> b) -> a -> b
$ DocLoc -> String -> Q ()
putDoc (Name -> DocLoc
DeclDoc Name
getScopedTermT)
    (String
"/Generated/ with '" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show 'mkGetScopedTerm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"'. Extract scoped term or __crash__.")
  [Dec] -> Q [Dec]
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return
    [ Name -> Kind -> Dec
SigD Name
getScopedTermT Kind
getScopedTermClausesType
    , Name -> [Clause] -> Dec
FunD Name
getScopedTermT [Clause]
getScopedTermClauses
    ]
  where
    getScopedTermT :: Name
getScopedTermT = String -> Name
mkName (String
"get" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
nameBase Name
termT String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"From" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
nameBase Name
scopeT)

    toClause :: Con -> Q [Clause]
    toClause :: Con -> Q [Clause]
toClause = \case
      NormalC Name
conName [BangType]
types -> Name -> [BangType] -> Q [Clause]
mkClause Name
conName [BangType]
types
      RecC Name
conName [VarBangType]
types -> Con -> Q [Clause]
toClause (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]
toClause (Name -> [BangType] -> Con
NormalC Name
conName [BangType
l, BangType
r])
      ForallC [TyVarBndr Specificity]
_ Cxt
_ Con
con -> Con -> Q [Clause]
toClause Con
con
      GadtC [Name]
conNames [BangType]
types Kind
_retType -> [[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
<$> (Name -> Q [Clause]) -> [Name] -> 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
conName -> Name -> [BangType] -> Q [Clause]
mkClause Name
conName [BangType]
types) [Name]
conNames
      RecGadtC [Name]
conNames [VarBangType]
types Kind
retType -> Con -> Q [Clause]
toClause ([Name] -> [BangType] -> Kind -> Con
GadtC [Name]
conNames ((VarBangType -> BangType) -> [VarBangType] -> [BangType]
forall a b. (a -> b) -> [a] -> [b]
map VarBangType -> BangType
removeName [VarBangType]
types) Kind
retType)

    mkClause :: Name -> [BangType] -> Q [Clause]
    mkClause :: Name -> [BangType] -> Q [Clause]
mkClause Name
conName [BangType]
types = do
      Exp
body <- case [[Q Exp]] -> [Q Exp]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[Q Exp]]
vars of
        [Q Exp
y] -> [e| $Q Exp
y |]
        [Q Exp]
_   -> [e| error "complex patterns are not supported" |]
      [Clause] -> Q [Clause]
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return [ [Pat] -> Body -> [Dec] -> Clause
Clause [Name -> Cxt -> [Pat] -> Pat
ConP Name
conName [] [Pat]
pats] (Exp -> Body
NormalB Exp
body) [] ]
      where
        x :: Name
x = String -> Name
mkName String
"x"
        ([Pat]
pats, [[Q Exp]]
vars) = [(Pat, [Q Exp])] -> ([Pat], [[Q Exp]])
forall a b. [(a, b)] -> ([a], [b])
unzip
          [ case Kind
type_ of
              PeelConT Name
typeName Cxt
_
                | Name
typeName Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
termT -> (Name -> Pat
VarP Name
x, [Exp -> Q Exp
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> Exp
VarE Name
x)])
              Kind
_ -> (Pat
WildP, [])
          | (Bang
_bang, Kind
type_) <- [BangType]
types
          ]