{-# LANGUAGE GADTs                 #-}
{-# LANGUAGE LambdaCase            #-}
{-# LANGUAGE QuasiQuotes           #-}
{-# LANGUAGE TemplateHaskellQuotes #-}
{-# OPTIONS_GHC -fno-warn-type-defaults #-}
module Control.Monad.Foil.TH.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.
--
-- @since 0.0.1
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 _ctx _name scopeTVars _kind scopeCons _deriv) <- Name -> Q Info
reify Name
scopeT
  TyConI (DataD _ctx _name termTVars _kind termCons _deriv) <- reify termT

  coSinkablePatternD <- deriveCoSinkable nameT patternT

  return $
    [ InstanceD Nothing [] (AppT (ConT ''Foil.Sinkable) (PeelConT foilScopeT (map (VarT . tvarName) scopeTVars)))
        [ FunD 'Foil.sinkabilityProof (map clauseScopedTerm scopeCons) ]

    , InstanceD Nothing [] (AppT (ConT ''Foil.Sinkable) (PeelConT foilTermT (map (VarT . tvarName) termTVars)))
        [ FunD 'Foil.sinkabilityProof (map clauseTerm termCons)]
    ] ++ coSinkablePatternD

  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)

    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)

-- | Generate 'Foil.Sinkable' and 'Foil.CoSinkable' instances.
--
-- @since 0.1.0
deriveCoSinkable
  :: Name -- ^ Type name for raw variable identifiers.
  -> Name -- ^ Type name for raw patterns.
  -> Q [Dec]
deriveCoSinkable :: Name -> Name -> Q [Dec]
deriveCoSinkable Name
nameT Name
patternT = do
  TyConI (DataD _ctx _name patternTVars _kind patternCons _deriv) <- Name -> Q Info
reify Name
patternT

  return
    [ InstanceD Nothing [] (AppT (ConT ''Foil.CoSinkable) (PeelConT foilPatternT (map (VarT . tvarName) patternTVars)))
        [ FunD 'Foil.coSinkabilityProof (map clausePattern patternCons)
        , FunD 'Foil.withPattern (map clauseWithPattern patternCons) ]
    ]

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

    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)

    clauseWithPattern :: Con -> Clause
    clauseWithPattern :: Con -> Clause
clauseWithPattern RecC{} = String -> Clause
forall a. HasCallStack => String -> a
error String
"Record constructors (RecC) are not supported yet!"
    clauseWithPattern InfixC{} = String -> Clause
forall a. HasCallStack => String -> a
error String
"Infix constructors (InfixC) are not supported yet!"
    clauseWithPattern ForallC{} = String -> Clause
forall a. HasCallStack => String -> a
error String
"Existential constructors (ForallC) are not supported yet!"
    clauseWithPattern GadtC{} = String -> Clause
forall a. HasCallStack => String -> a
error String
"GADT constructors (GadtC) are not supported yet!"
    clauseWithPattern RecGadtC{} = String -> Clause
forall a. HasCallStack => String -> a
error String
"Record GADT constructors (RecGadtC) are not supported yet!"
    clauseWithPattern (NormalC Name
conName [BangType]
params) =
      [Pat] -> Body -> [Dec] -> Clause
Clause
        [Name -> Pat
VarP Name
withNameBinder, Name -> Pat
VarP Name
id', Name -> Pat
VarP Name
comp, Name -> Pat
VarP Name
scope, Name -> Cxt -> [Pat] -> Pat
ConP Name
foilConName [] [Pat]
conParamPatterns, Name -> Pat
VarP Name
cont]
        (Exp -> Body
NormalB (Integer -> Name -> Exp -> Exp -> [BangType] -> Exp
go Integer
1 Name
scope (Name -> Exp
VarE Name
id') (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)
        withNameBinder :: Name
withNameBinder = String -> Name
mkName String
"_withNameBinder"
        id' :: Name
id' = String -> Name
mkName String
"id'"
        comp :: Name
comp = String -> Name
mkName String
"_comp"
        scope :: Name
scope = String -> Name
mkName String
"_scope"
        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 -> Name -> Exp -> Exp -> [BangType] -> Exp
go Integer
_i Name
scope' Exp
rename' Exp
p [] = Exp -> Exp -> Exp
AppE (Exp -> Exp -> Exp
AppE (Exp -> Exp -> Exp
AppE (Name -> Exp
VarE Name
cont) Exp
rename') Exp
p) (Name -> Exp
VarE Name
scope')
        go Integer
i Name
scope' 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) -> 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
VarE 'Foil.withPattern) [Name -> Exp
VarE Name
withNameBinder, Name -> Exp
VarE Name
id', Name -> Exp
VarE Name
comp, Name -> Exp
VarE Name
scope', Name -> Exp
VarE Name
xi])
                ([Pat] -> Exp -> Exp
LamE [Name -> Pat
VarP Name
renamei, Name -> Pat
VarP Name
xi', Name -> Pat
VarP Name
scopei]
                  (Integer -> Name -> Exp -> Exp -> [BangType] -> Exp
go (Integer
i Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1) Name
scopei ((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
VarE Name
comp) [Exp
rename', 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
"f" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
i)
            scopei :: Name
scopei = String -> Name
mkName (String
"scope" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
i)
        go Integer
i Name
scope' Exp
rename' Exp
p (BangType
_ : [BangType]
conPatterns) =
          Integer -> Name -> Exp -> Exp -> [BangType] -> Exp
go (Integer
i Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1) Name
scope' 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)