{-# LANGUAGE GADTs                 #-}
{-# LANGUAGE LambdaCase            #-}
{-# LANGUAGE QuasiQuotes           #-}
{-# LANGUAGE TemplateHaskellQuotes #-}
{-# OPTIONS_GHC -fno-warn-type-defaults #-}
module Control.Monad.Foil.TH.MkInstancesFoil (mkInstancesFoil) where

import           Language.Haskell.TH

import qualified Control.Monad.Foil  as Foil
import Control.Monad.Foil.TH.Util

-- | Generate 'Foil.Sinkable' and 'Foil.CoSinkable' instances.
mkInstancesFoil
  :: 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]
mkInstancesFoil :: Name -> Name -> Name -> Name -> Q [Dec]
mkInstancesFoil Name
termT Name
nameT Name
scopeT Name
patternT = do
  TyConI (DataD Cxt
_ctx Name
_name [TyVarBndr BndrVis]
patternTVars Maybe Kind
_kind [Con]
patternCons [DerivClause]
_deriv) <- Name -> Q Info
reify Name
patternT
  TyConI (DataD Cxt
_ctx Name
_name [TyVarBndr BndrVis]
scopeTVars Maybe Kind
_kind [Con]
scopeCons [DerivClause]
_deriv) <- Name -> Q Info
reify Name
scopeT
  TyConI (DataD Cxt
_ctx Name
_name [TyVarBndr BndrVis]
termTVars Maybe Kind
_kind [Con]
termCons [DerivClause]
_deriv) <- Name -> Q Info
reify Name
termT

  [Dec] -> Q [Dec]
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return
    [ Maybe Overlap -> Cxt -> Kind -> [Dec] -> Dec
InstanceD Maybe Overlap
forall a. Maybe a
Nothing [] (Kind -> Kind -> Kind
AppT (Name -> Kind
ConT ''Foil.Sinkable) (Name -> Cxt -> Kind
PeelConT Name
foilScopeT ((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]
scopeTVars)))
        [ Name -> [Clause] -> Dec
FunD 'Foil.sinkabilityProof ((Con -> Clause) -> [Con] -> [Clause]
forall a b. (a -> b) -> [a] -> [b]
map Con -> Clause
clauseScopedTerm [Con]
scopeCons) ]

    , Maybe Overlap -> Cxt -> Kind -> [Dec] -> Dec
InstanceD Maybe Overlap
forall a. Maybe a
Nothing [] (Kind -> Kind -> Kind
AppT (Name -> Kind
ConT ''Foil.CoSinkable) (Name -> Cxt -> Kind
PeelConT Name
foilPatternT ((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)))
        [ Name -> [Clause] -> Dec
FunD 'Foil.coSinkabilityProof ((Con -> Clause) -> [Con] -> [Clause]
forall a b. (a -> b) -> [a] -> [b]
map Con -> Clause
clausePattern [Con]
patternCons) ]

    , Maybe Overlap -> Cxt -> Kind -> [Dec] -> Dec
InstanceD Maybe Overlap
forall a. Maybe a
Nothing [] (Kind -> Kind -> Kind
AppT (Name -> Kind
ConT ''Foil.Sinkable) (Name -> Cxt -> Kind
PeelConT Name
foilTermT ((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)))
        [ Name -> [Clause] -> Dec
FunD 'Foil.sinkabilityProof ((Con -> Clause) -> [Con] -> [Clause]
forall a b. (a -> b) -> [a] -> [b]
map Con -> Clause
clauseTerm [Con]
termCons)]
    ]

  where
    foilTermT :: Name
foilTermT = String -> Name
mkName (String
"Foil" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
nameBase Name
termT)
    foilScopeT :: Name
foilScopeT = String -> Name
mkName (String
"Foil" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
nameBase Name
scopeT)
    foilPatternT :: Name
foilPatternT = String -> Name
mkName (String
"Foil" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
nameBase Name
patternT)

    clauseScopedTerm :: Con -> Clause
    clauseScopedTerm :: Con -> Clause
clauseScopedTerm = Con -> Clause
clauseTerm

    clauseTerm :: Con -> Clause
    clauseTerm :: Con -> Clause
clauseTerm RecC{} = String -> Clause
forall a. HasCallStack => String -> a
error String
"Record constructors (RecC) are not supported yet!"
    clauseTerm InfixC{} = String -> Clause
forall a. HasCallStack => String -> a
error String
"Infix constructors (InfixC) are not supported yet!"
    clauseTerm ForallC{} = String -> Clause
forall a. HasCallStack => String -> a
error String
"Existential constructors (ForallC) are not supported yet!"
    clauseTerm GadtC{} = String -> Clause
forall a. HasCallStack => String -> a
error String
"GADT constructors (GadtC) are not supported yet!"
    clauseTerm RecGadtC{} = String -> Clause
forall a. HasCallStack => String -> a
error String
"Record GADT constructors (RecGadtC) are not supported yet!"
    clauseTerm (NormalC Name
conName [BangType]
params) =
      [Pat] -> Body -> [Dec] -> Clause
Clause
        [Name -> Pat
VarP Name
rename, Name -> Cxt -> [Pat] -> Pat
ConP Name
foilConName [] [Pat]
conParamPatterns]
        (Exp -> Body
NormalB (Integer -> Exp -> Exp -> [BangType] -> Exp
go Integer
1 (Name -> Exp
VarE Name
rename) (Name -> Exp
ConE Name
foilConName) [BangType]
params))
        []
      where
        foilConName :: Name
foilConName = String -> Name
mkName (String
"Foil" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
nameBase Name
conName)
        rename :: Name
rename = String -> Name
mkName String
"rename"
        conParamPatterns :: [Pat]
conParamPatterns = (BangType -> Integer -> Pat) -> [BangType] -> [Integer] -> [Pat]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith BangType -> Integer -> Pat
forall {a} {p}. Show a => p -> a -> Pat
mkConParamPattern [BangType]
params [Integer
1..]
        mkConParamPattern :: p -> a -> Pat
mkConParamPattern p
_ a
i = Name -> Pat
VarP (String -> Name
mkName (String
"x" String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
i))

        go :: Integer -> Exp -> Exp -> [BangType] -> Exp
go Integer
_i Exp
_rename' Exp
p [] = Exp
p
        go Integer
i Exp
rename' Exp
p ((Bang
_bang, PeelConT Name
tyName Cxt
_tyParams) : [BangType]
conParams)
          | Name
tyName Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
nameT =
              Integer -> Exp -> Exp -> [BangType] -> Exp
go (Integer
i Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1) Exp
rename' (Exp -> Exp -> Exp
AppE Exp
p (Exp -> Exp -> Exp
AppE (Name -> Exp
VarE Name
rename) (Name -> Exp
VarE Name
xi))) [BangType]
conParams
          | Name
tyName Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
termT =
              Integer -> Exp -> Exp -> [BangType] -> Exp
go (Integer
i Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1) Exp
rename' (Exp -> Exp -> Exp
AppE Exp
p (Exp -> Exp -> Exp
AppE (Exp -> Exp -> Exp
AppE (Name -> Exp
VarE 'Foil.sinkabilityProof) (Name -> Exp
VarE Name
rename)) (Name -> Exp
VarE Name
xi))) [BangType]
conParams
          | Name
tyName Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
scopeT =
              Integer -> Exp -> Exp -> [BangType] -> Exp
go (Integer
i Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1) Exp
rename' (Exp -> Exp -> Exp
AppE Exp
p (Exp -> Exp -> Exp
AppE (Exp -> Exp -> Exp
AppE (Name -> Exp
VarE 'Foil.sinkabilityProof) Exp
rename') (Name -> Exp
VarE Name
xi))) [BangType]
conParams
          | Name
tyName Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
patternT =
              Exp -> Exp -> Exp
AppE
                (Exp -> Exp -> Exp
AppE (Exp -> Exp -> Exp
AppE (Name -> Exp
VarE 'Foil.coSinkabilityProof) Exp
rename') (Name -> Exp
VarE Name
xi))
                ([Pat] -> Exp -> Exp
LamE [Name -> Pat
VarP Name
renamei, Name -> Pat
VarP Name
xi']
                  (Integer -> Exp -> Exp -> [BangType] -> Exp
go (Integer
i Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1) (Name -> Exp
VarE Name
renamei) (Exp -> Exp -> Exp
AppE Exp
p (Name -> Exp
VarE Name
xi')) [BangType]
conParams))
          where
            xi :: Name
xi = String -> Name
mkName (String
"x" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
i)
            xi' :: Name
xi' = String -> Name
mkName (String
"x" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
i String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"'")
            renamei :: Name
renamei = String -> Name
mkName (String
"rename" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
i)
        go Integer
i Exp
rename' Exp
p (BangType
_ : [BangType]
conPatterns) =
          Integer -> Exp -> Exp -> [BangType] -> Exp
go (Integer
i Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1) Exp
rename' (Exp -> Exp -> Exp
AppE Exp
p (Name -> Exp
VarE Name
xi)) [BangType]
conPatterns
          where
            xi :: Name
xi = String -> Name
mkName (String
"x" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
i)

    clausePattern :: Con -> Clause
    clausePattern :: Con -> Clause
clausePattern RecC{} = String -> Clause
forall a. HasCallStack => String -> a
error String
"Record constructors (RecC) are not supported yet!"
    clausePattern InfixC{} = String -> Clause
forall a. HasCallStack => String -> a
error String
"Infix constructors (InfixC) are not supported yet!"
    clausePattern ForallC{} = String -> Clause
forall a. HasCallStack => String -> a
error String
"Existential constructors (ForallC) are not supported yet!"
    clausePattern GadtC{} = String -> Clause
forall a. HasCallStack => String -> a
error String
"GADT constructors (GadtC) are not supported yet!"
    clausePattern RecGadtC{} = String -> Clause
forall a. HasCallStack => String -> a
error String
"Record GADT constructors (RecGadtC) are not supported yet!"
    clausePattern (NormalC Name
conName [BangType]
params) =
      [Pat] -> Body -> [Dec] -> Clause
Clause
        [Name -> Pat
VarP Name
rename, Name -> Cxt -> [Pat] -> Pat
ConP Name
foilConName [] [Pat]
conParamPatterns, Name -> Pat
VarP Name
cont]
        (Exp -> Body
NormalB (Integer -> Exp -> Exp -> [BangType] -> Exp
go Integer
1 (Name -> Exp
VarE Name
rename) (Name -> Exp
ConE Name
foilConName) [BangType]
params))
        []
      where
        foilConName :: Name
foilConName = String -> Name
mkName (String
"Foil" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
nameBase Name
conName)
        rename :: Name
rename = String -> Name
mkName String
"rename"
        cont :: Name
cont = String -> Name
mkName String
"cont"
        conParamPatterns :: [Pat]
conParamPatterns = (BangType -> Integer -> Pat) -> [BangType] -> [Integer] -> [Pat]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith BangType -> Integer -> Pat
forall {a} {p}. Show a => p -> a -> Pat
mkConParamPattern [BangType]
params [Integer
1..]
        mkConParamPattern :: p -> a -> Pat
mkConParamPattern p
_ a
i = Name -> Pat
VarP (String -> Name
mkName (String
"x" String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
i))

        go :: Integer -> Exp -> Exp -> [BangType] -> Exp
go Integer
_i Exp
rename' Exp
p [] = Exp -> Exp -> Exp
AppE (Exp -> Exp -> Exp
AppE (Name -> Exp
VarE Name
cont) Exp
rename') Exp
p
        go Integer
i Exp
rename' Exp
p ((Bang
_bang, PeelConT Name
tyName Cxt
_tyParams) : [BangType]
conParams)
          | Name
tyName Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
nameT Bool -> Bool -> Bool
|| Name
tyName Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
patternT =
              Exp -> Exp -> Exp
AppE
                (Exp -> Exp -> Exp
AppE (Exp -> Exp -> Exp
AppE (Name -> Exp
VarE 'Foil.coSinkabilityProof) Exp
rename') (Name -> Exp
VarE Name
xi))
                ([Pat] -> Exp -> Exp
LamE [Name -> Pat
VarP Name
renamei, Name -> Pat
VarP Name
xi']
                  (Integer -> Exp -> Exp -> [BangType] -> Exp
go (Integer
i Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1) (Name -> Exp
VarE Name
renamei) (Exp -> Exp -> Exp
AppE Exp
p (Name -> Exp
VarE Name
xi')) [BangType]
conParams))
          where
            xi :: Name
xi = String -> Name
mkName (String
"x" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
i)
            xi' :: Name
xi' = String -> Name
mkName (String
"x" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
i String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"'")
            renamei :: Name
renamei = String -> Name
mkName (String
"rename" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
i)
        go Integer
i Exp
rename' Exp
p (BangType
_ : [BangType]
conPatterns) =
          Integer -> Exp -> Exp -> [BangType] -> Exp
go (Integer
i Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1) Exp
rename' (Exp -> Exp -> Exp
AppE Exp
p (Name -> Exp
VarE Name
xi)) [BangType]
conPatterns
          where
            xi :: Name
xi = String -> Name
mkName (String
"x" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
i)