{-# OPTIONS_GHC -fno-warn-type-defaults #-}
{-# LANGUAGE GADTs                 #-}
{-# LANGUAGE LambdaCase            #-}
{-# LANGUAGE RankNTypes            #-}
{-# LANGUAGE QuasiQuotes           #-}
{-# LANGUAGE TemplateHaskellQuotes #-}
module Control.Monad.Foil.TH.MkFromFoil where

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

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

-- | Generate conversion functions from raw to scope-safe representation.
--
-- @since 0.0.1
mkFromFoil
  :: 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]
mkFromFoil :: Name -> Name -> Name -> Name -> Q [Dec]
mkFromFoil Name
termT Name
nameT Name
scopeT Name
patternT = do
  n <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"n"
  let ntype = Type -> Q Type
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> Type
VarT Name
n)
  l <- newName "l"
  let ltype = Type -> Q Type
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> Type
VarT Name
l)
  r <- newName "r"
  let rtype = Type -> Q Type
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> Type
VarT Name
r)
  TyConI (DataD _ctx _name patternTVars _kind patternCons _deriv) <- reify patternT
  TyConI (DataD _ctx _name scopeTVars _kind scopeCons _deriv) <- reify scopeT
  TyConI (DataD _ctx _name termTVars _kind termCons _deriv) <- reify termT

  let termParams = (TyVarBndr BndrVis -> Type) -> [TyVarBndr BndrVis] -> Cxt
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]
termTVars
  let scopeParams = (TyVarBndr BndrVis -> Type) -> [TyVarBndr BndrVis] -> Cxt
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]
scopeTVars
  let patternParams = (TyVarBndr BndrVis -> Type) -> [TyVarBndr BndrVis] -> Cxt
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]
patternTVars

  fromFoilTermSignature <-
    SigD fromFoilTermT <$>
      [t| [$(return (ConT nameT))]
          -> Foil.NameMap $ntype $(return (ConT nameT))
          -> $(return (PeelConT foilTermT termParams)) $ntype
          -> $(return (PeelConT termT termParams))
        |]
  fromFoilScopedSignature <-
    SigD fromFoilScopedT <$>
      [t| [$(return (ConT nameT))]
          -> Foil.NameMap $ntype $(return (ConT nameT))
          -> $(return (PeelConT foilScopeT scopeParams)) $ntype
          -> $(return (PeelConT scopeT scopeParams))
        |]
  fromFoilPatternSignature <-
    SigD fromFoilPatternT <$>
      [t| [$(return (ConT nameT))]
          -> Foil.NameMap $ntype $(return (ConT nameT))
          -> $(return (PeelConT foilPatternT patternParams)) $ntype $ltype
          -> ([$(return (ConT nameT))] -> Foil.NameMap $ltype $(return (ConT nameT)) -> $(return (PeelConT patternT patternParams)) -> $rtype)
          -> $rtype
        |]

  addModFinalizer $ putDoc (DeclDoc fromFoilTermT) $
    "/Generated/ with '" ++ show 'mkFromFoil ++ "'. Convert a scope-safe term into a raw term."
  addModFinalizer $ putDoc (DeclDoc fromFoilPatternT) $
    "/Generated/ with '" ++ show 'mkFromFoil ++ "'. Convert a scope-safe pattern into a raw pattern."
  addModFinalizer $ putDoc (DeclDoc fromFoilScopedT) $
    "/Generated/ with '" ++ show 'mkFromFoil ++ "'. Convert a scope-safe scoped term into a raw scoped term."

  return
    [ fromFoilTermSignature
    , fromFoilTermBody termCons
    , fromFoilPatternSignature
    , fromFoilPatternBody patternCons
    , fromFoilScopedSignature
    , fromFoilScopedBody scopeCons
    ]
  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)

    fromFoilTermT :: Name
fromFoilTermT = String -> Name
mkName (String
"fromFoil" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
nameBase Name
termT)
    fromFoilPatternT :: Name
fromFoilPatternT = String -> Name
mkName (String
"fromFoil" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
nameBase Name
patternT)
    fromFoilScopedT :: Name
fromFoilScopedT = String -> Name
mkName (String
"fromFoil" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
nameBase Name
scopeT)

    fromFoilTermBody :: [Con] -> Dec
fromFoilTermBody [Con]
termCons = Name -> [Clause] -> Dec
FunD Name
fromFoilTermT
      [[Pat] -> Body -> [Dec] -> Clause
Clause [Name -> Pat
VarP Name
freshVars, Name -> Pat
VarP Name
env, Name -> Pat
VarP Name
term] (Exp -> Body
NormalB (Exp -> [Match] -> Exp
CaseE (Name -> Exp
VarE Name
term) ((Con -> Match) -> [Con] -> [Match]
forall a b. (a -> b) -> [a] -> [b]
map Con -> Match
toMatch [Con]
termCons))) []]
      where
        freshVars :: Name
freshVars = String -> Name
mkName String
"freshVars"
        env :: Name
env = String -> Name
mkName String
"env"
        term :: Name
term = String -> Name
mkName String
"term"

        toMatch :: Con -> Match
toMatch (NormalC Name
conName [BangType]
params) =
          Pat -> Body -> [Dec] -> Match
Match (Name -> Cxt -> [Pat] -> Pat
ConP Name
foilConName [] [Pat]
conParamPatterns) (Exp -> Body
NormalB Exp
conMatchBody) []
          where
            conMatchBody :: Exp
conMatchBody = Integer -> Exp -> Exp -> Exp -> [BangType] -> Exp
go Integer
1 (Name -> Exp
VarE Name
freshVars) (Name -> Exp
VarE Name
env) (Name -> Exp
ConE Name
conName) [BangType]
params

            go :: Integer -> Exp -> Exp -> Exp -> [BangType] -> Exp
go Integer
_i Exp
_freshVars' Exp
_env' Exp
p [] = Exp
p
            go Integer
i Exp
freshVars' Exp
env' 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 -> Exp -> [BangType] -> Exp
go (Integer
iInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
+Integer
1) Exp
freshVars' Exp
env' (Exp -> Exp -> Exp
AppE Exp
p (Exp -> Exp -> Exp
AppE (Exp -> Exp -> Exp
AppE (Name -> Exp
VarE 'Foil.lookupName) (Name -> Exp
VarE Name
xi)) Exp
env')) [BangType]
conParams
              | Name
tyName Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
termT =
                  Integer -> Exp -> Exp -> Exp -> [BangType] -> Exp
go (Integer
iInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
+Integer
1) Exp
freshVars' Exp
env' (Exp -> Exp -> Exp
AppE Exp
p (Exp -> Exp -> Exp
AppE (Exp -> Exp -> Exp
AppE (Exp -> Exp -> Exp
AppE (Name -> Exp
VarE Name
fromFoilTermT) (Name -> Exp
VarE Name
freshVars)) (Name -> Exp
VarE Name
env)) (Name -> Exp
VarE Name
xi))) [BangType]
conParams
              | Name
tyName Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
scopeT =
                  Integer -> Exp -> Exp -> Exp -> [BangType] -> Exp
go (Integer
iInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
+Integer
1) Exp
freshVars' Exp
env' (Exp -> Exp -> Exp
AppE Exp
p (Exp -> Exp -> Exp
AppE (Exp -> Exp -> Exp
AppE (Exp -> Exp -> Exp
AppE (Name -> Exp
VarE Name
fromFoilScopedT) Exp
freshVars') Exp
env') (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 (Exp -> Exp -> Exp
AppE (Name -> Exp
VarE Name
fromFoilPatternT) Exp
freshVars') Exp
env') (Name -> Exp
VarE Name
xi))
                    ([Pat] -> Exp -> Exp
LamE [Name -> Pat
VarP Name
freshVarsi, Name -> Pat
VarP Name
envi, Name -> Pat
VarP Name
xi']
                      (Integer -> Exp -> Exp -> Exp -> [BangType] -> Exp
go (Integer
iInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
+Integer
1) (Name -> Exp
VarE Name
freshVarsi) (Name -> Exp
VarE Name
envi) (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. Semigroup 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. Semigroup a => a -> a -> a
<> Integer -> String
forall a. Show a => a -> String
show Integer
i String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
"'")
                freshVarsi :: Name
freshVarsi = String -> Name
mkName (String
"freshVars" String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Integer -> String
forall a. Show a => a -> String
show Integer
i)
                envi :: Name
envi = String -> Name
mkName (String
"env" String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Integer -> String
forall a. Show a => a -> String
show Integer
i)
            go Integer
i Exp
freshVars' Exp
env' Exp
p (BangType
_ : [BangType]
conParams) =
              Integer -> Exp -> Exp -> Exp -> [BangType] -> Exp
go (Integer
i Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1) Exp
freshVars' Exp
env' (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. Semigroup a => a -> a -> a
<> Integer -> String
forall a. Show a => a -> String
show Integer
i)

            foilConName :: Name
foilConName = String -> Name
mkName (String
"Foil" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
nameBase Name
conName)
            conParamPatterns :: [Pat]
conParamPatterns = (Name -> Pat) -> [Name] -> [Pat]
forall a b. (a -> b) -> [a] -> [b]
map Name -> Pat
VarP [Name]
conParamVars

            conParamVars :: [Name]
conParamVars = (BangType -> Int -> Name) -> [BangType] -> [Int] -> [Name]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith BangType -> Int -> Name
mkConParamVar [BangType]
params [Int
1..]

            mkConParamVar :: BangType -> Int -> Name
            mkConParamVar :: BangType -> Int -> Name
mkConParamVar BangType
_ty Int
i = String -> Name
mkName (String
"x" String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Int -> String
forall a. Show a => a -> String
show Int
i)
        toMatch RecC{} = String -> Match
forall a. HasCallStack => String -> a
error String
"Record constructors (RecC) are not supported yet!"
        toMatch InfixC{} = String -> Match
forall a. HasCallStack => String -> a
error String
"Infix constructors (InfixC) are not supported yet!"
        toMatch ForallC{} = String -> Match
forall a. HasCallStack => String -> a
error String
"Existential constructors (ForallC) are not supported yet!"
        toMatch GadtC{} = String -> Match
forall a. HasCallStack => String -> a
error String
"GADT constructors (GadtC) are not supported yet!"
        toMatch RecGadtC{} = String -> Match
forall a. HasCallStack => String -> a
error String
"Record GADT constructors (RecGadtC) are not supported yet!"

    fromFoilPatternBody :: [Con] -> Dec
fromFoilPatternBody [Con]
patternCons = Name -> [Clause] -> Dec
FunD Name
fromFoilPatternT
      [[Pat] -> Body -> [Dec] -> Clause
Clause [Name -> Pat
VarP Name
freshVars, Name -> Pat
VarP Name
env, Name -> Pat
VarP Name
pattern, Name -> Pat
VarP Name
cont] (Exp -> Body
NormalB (Exp -> [Match] -> Exp
CaseE (Name -> Exp
VarE Name
pattern) ((Con -> Match) -> [Con] -> [Match]
forall a b. (a -> b) -> [a] -> [b]
map Con -> Match
toMatch [Con]
patternCons))) []]
      where
        freshVars :: Name
freshVars = String -> Name
mkName String
"freshVars"
        env :: Name
env = String -> Name
mkName String
"env"
        pattern :: Name
pattern = String -> Name
mkName String
"pattern"
        cont :: Name
cont = String -> Name
mkName String
"cont"

        toMatch :: Con -> Match
toMatch (NormalC Name
conName [BangType]
params) =
          Pat -> Body -> [Dec] -> Match
Match (Name -> Cxt -> [Pat] -> Pat
ConP Name
foilConName [] [Pat]
conParamPatterns) (Exp -> Body
NormalB Exp
conMatchBody) []
          where
            conMatchBody :: Exp
conMatchBody = Integer -> Exp -> Exp -> Exp -> [BangType] -> Exp
go Integer
1 (Name -> Exp
VarE Name
freshVars) (Name -> Exp
VarE Name
env) (Name -> Exp
ConE Name
conName) [BangType]
params

            go :: Integer -> Exp -> Exp -> Exp -> [BangType] -> Exp
go Integer
_i Exp
freshVars' Exp
env' Exp
p [] = Exp -> Exp -> Exp
AppE (Exp -> Exp -> Exp
AppE (Exp -> Exp -> Exp
AppE (Name -> Exp
VarE Name
cont) Exp
freshVars') Exp
env') Exp
p
            go Integer
i Exp
freshVars' Exp
env' 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 =
                  Exp -> [Match] -> Exp
CaseE Exp
freshVars'
                    [ Pat -> Body -> [Dec] -> Match
Match ([Pat] -> Pat
ListP []) (Exp -> Body
NormalB (Exp -> Exp -> Exp
AppE (Name -> Exp
VarE 'error) (Lit -> Exp
LitE (String -> Lit
StringL String
"not enough fresh variables")))) []
                    , Pat -> Body -> [Dec] -> Match
Match (Pat -> Name -> Pat -> Pat
InfixP (Name -> Pat
VarP Name
var) '(:) (Name -> Pat
VarP Name
vars))
                        (Exp -> Body
NormalB ([Dec] -> Exp -> Exp
LetE
                          [Pat -> Body -> [Dec] -> Dec
ValD (Name -> Pat
VarP Name
envi) (Exp -> Body
NormalB (Exp -> Exp -> Exp
AppE (Exp -> Exp -> Exp
AppE (Exp -> Exp -> Exp
AppE (Name -> Exp
VarE 'Foil.addNameBinder) (Name -> Exp
VarE Name
xi)) (Name -> Exp
VarE Name
var)) Exp
env')) []]
                          (Integer -> Exp -> Exp -> Exp -> [BangType] -> Exp
go (Integer
i Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1) (Name -> Exp
VarE Name
vars) (Name -> Exp
VarE Name
envi) (Exp -> Exp -> Exp
AppE Exp
p (Name -> Exp
VarE Name
var)) [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 (Exp -> Exp -> Exp
AppE (Name -> Exp
VarE Name
fromFoilPatternT) Exp
freshVars') Exp
env') (Name -> Exp
VarE Name
xi))
                    ([Pat] -> Exp -> Exp
LamE [Name -> Pat
VarP Name
freshVarsi, Name -> Pat
VarP Name
envi, Name -> Pat
VarP Name
xi']
                      (Integer -> Exp -> Exp -> Exp -> [BangType] -> Exp
go (Integer
iInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
+Integer
1) (Name -> Exp
VarE Name
freshVarsi) (Name -> Exp
VarE Name
envi) (Exp -> Exp -> Exp
AppE Exp
p (Name -> Exp
VarE Name
xi')) [BangType]
conParams))
              where
                var :: Name
var = String -> Name
mkName String
"var"
                vars :: Name
vars = String -> Name
mkName String
"vars"
                xi :: Name
xi = String -> Name
mkName (String
"x" String -> String -> String
forall a. Semigroup 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. Semigroup a => a -> a -> a
<> Integer -> String
forall a. Show a => a -> String
show Integer
i String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
"'")
                freshVarsi :: Name
freshVarsi = String -> Name
mkName (String
"freshVars" String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Integer -> String
forall a. Show a => a -> String
show Integer
i)
                envi :: Name
envi = String -> Name
mkName (String
"env" String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Integer -> String
forall a. Show a => a -> String
show Integer
i)
            go Integer
i Exp
freshVars' Exp
env' Exp
p (BangType
_ : [BangType]
conParams) =
              Integer -> Exp -> Exp -> Exp -> [BangType] -> Exp
go (Integer
i Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1) Exp
freshVars' Exp
env' (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. Semigroup a => a -> a -> a
<> Integer -> String
forall a. Show a => a -> String
show Integer
i)

            foilConName :: Name
foilConName = String -> Name
mkName (String
"Foil" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
nameBase Name
conName)
            conParamPatterns :: [Pat]
conParamPatterns = (Name -> Pat) -> [Name] -> [Pat]
forall a b. (a -> b) -> [a] -> [b]
map Name -> Pat
VarP [Name]
conParamVars

            conParamVars :: [Name]
conParamVars = (BangType -> Int -> Name) -> [BangType] -> [Int] -> [Name]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith BangType -> Int -> Name
mkConParamVar [BangType]
params [Int
1..]

            mkConParamVar :: BangType -> Int -> Name
            mkConParamVar :: BangType -> Int -> Name
mkConParamVar BangType
_ Int
i = String -> Name
mkName (String
"x" String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Int -> String
forall a. Show a => a -> String
show Int
i)
        toMatch RecC{} = String -> Match
forall a. HasCallStack => String -> a
error String
"Record constructors (RecC) are not supported yet!"
        toMatch InfixC{} = String -> Match
forall a. HasCallStack => String -> a
error String
"Infix constructors (InfixC) are not supported yet!"
        toMatch ForallC{} = String -> Match
forall a. HasCallStack => String -> a
error String
"Existential constructors (ForallC) are not supported yet!"
        toMatch GadtC{} = String -> Match
forall a. HasCallStack => String -> a
error String
"GADT constructors (GadtC) are not supported yet!"
        toMatch RecGadtC{} = String -> Match
forall a. HasCallStack => String -> a
error String
"Record GADT constructors (RecGadtC) are not supported yet!"

    fromFoilScopedBody :: [Con] -> Dec
fromFoilScopedBody [Con]
freshVarsCons = Name -> [Clause] -> Dec
FunD Name
fromFoilScopedT
      [[Pat] -> Body -> [Dec] -> Clause
Clause [Name -> Pat
VarP Name
freshVars, Name -> Pat
VarP Name
env, Name -> Pat
VarP Name
term] (Exp -> Body
NormalB (Exp -> [Match] -> Exp
CaseE (Name -> Exp
VarE Name
term) ((Con -> Match) -> [Con] -> [Match]
forall a b. (a -> b) -> [a] -> [b]
map Con -> Match
toMatch [Con]
freshVarsCons))) []]
      where
        freshVars :: Name
freshVars = String -> Name
mkName String
"freshVars"
        env :: Name
env = String -> Name
mkName String
"env"
        term :: Name
term = String -> Name
mkName String
"term"

        toMatch :: Con -> Match
toMatch (NormalC Name
conName [BangType]
params) =
          Pat -> Body -> [Dec] -> Match
Match (Name -> Cxt -> [Pat] -> Pat
ConP Name
foilConName [] [Pat]
conParamPatterns) (Exp -> Body
NormalB Exp
conMatchBody) []
          where
            conMatchBody :: Exp
conMatchBody = Integer -> Exp -> Exp -> Exp -> [BangType] -> Exp
go Integer
1 (Name -> Exp
VarE Name
freshVars) (Name -> Exp
VarE Name
env) (Name -> Exp
ConE Name
conName) [BangType]
params

            go :: Integer -> Exp -> Exp -> Exp -> [BangType] -> Exp
go Integer
_i Exp
_freshVars' Exp
_env' Exp
p [] = Exp
p
            go Integer
i Exp
freshVars' Exp
env' 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 -> Exp -> [BangType] -> Exp
go (Integer
iInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
+Integer
1) Exp
freshVars' Exp
env' (Exp -> Exp -> Exp
AppE Exp
p (Exp -> Exp -> Exp
AppE (Exp -> Exp -> Exp
AppE (Name -> Exp
VarE 'Foil.lookupName) (Name -> Exp
VarE Name
xi)) Exp
env')) [BangType]
conParams
              | Name
tyName Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
termT =
                  Integer -> Exp -> Exp -> Exp -> [BangType] -> Exp
go (Integer
iInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
+Integer
1) Exp
freshVars' Exp
env' (Exp -> Exp -> Exp
AppE Exp
p (Exp -> Exp -> Exp
AppE (Exp -> Exp -> Exp
AppE (Exp -> Exp -> Exp
AppE (Name -> Exp
VarE Name
fromFoilTermT) (Name -> Exp
VarE Name
freshVars)) (Name -> Exp
VarE Name
env)) (Name -> Exp
VarE Name
xi))) [BangType]
conParams
              | Name
tyName Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
scopeT =
                  Integer -> Exp -> Exp -> Exp -> [BangType] -> Exp
go (Integer
iInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
+Integer
1) Exp
freshVars' Exp
env' (Exp -> Exp -> Exp
AppE Exp
p (Exp -> Exp -> Exp
AppE (Exp -> Exp -> Exp
AppE (Exp -> Exp -> Exp
AppE (Name -> Exp
VarE Name
fromFoilScopedT) Exp
freshVars') Exp
env') (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 (Exp -> Exp -> Exp
AppE (Name -> Exp
VarE Name
fromFoilPatternT) Exp
freshVars') Exp
env') (Name -> Exp
VarE Name
xi))
                    ([Pat] -> Exp -> Exp
LamE [Name -> Pat
VarP Name
freshVarsi, Name -> Pat
VarP Name
envi, Name -> Pat
VarP Name
xi']
                      (Integer -> Exp -> Exp -> Exp -> [BangType] -> Exp
go (Integer
iInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
+Integer
1) (Name -> Exp
VarE Name
freshVarsi) (Name -> Exp
VarE Name
envi) (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. Semigroup 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. Semigroup a => a -> a -> a
<> Integer -> String
forall a. Show a => a -> String
show Integer
i String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
"'")
                freshVarsi :: Name
freshVarsi = String -> Name
mkName (String
"freshVars" String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Integer -> String
forall a. Show a => a -> String
show Integer
i)
                envi :: Name
envi = String -> Name
mkName (String
"env" String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Integer -> String
forall a. Show a => a -> String
show Integer
i)
            go Integer
i Exp
freshVars' Exp
env' Exp
p (BangType
_ : [BangType]
conParams) =
              Integer -> Exp -> Exp -> Exp -> [BangType] -> Exp
go (Integer
i Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1) Exp
freshVars' Exp
env' (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. Semigroup a => a -> a -> a
<> Integer -> String
forall a. Show a => a -> String
show Integer
i)

            foilConName :: Name
foilConName = String -> Name
mkName (String
"Foil" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
nameBase Name
conName)
            conParamPatterns :: [Pat]
conParamPatterns = (Name -> Pat) -> [Name] -> [Pat]
forall a b. (a -> b) -> [a] -> [b]
map Name -> Pat
VarP [Name]
conParamVars

            conParamVars :: [Name]
conParamVars = (BangType -> Int -> Name) -> [BangType] -> [Int] -> [Name]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith BangType -> Int -> Name
mkConParamVar [BangType]
params [Int
1..]

            mkConParamVar :: BangType -> Int -> Name
            mkConParamVar :: BangType -> Int -> Name
mkConParamVar BangType
_ty Int
i = String -> Name
mkName (String
"x" String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Int -> String
forall a. Show a => a -> String
show Int
i)
        toMatch RecC{} = String -> Match
forall a. HasCallStack => String -> a
error String
"Record constructors (RecC) are not supported yet!"
        toMatch InfixC{} = String -> Match
forall a. HasCallStack => String -> a
error String
"Infix constructors (InfixC) are not supported yet!"
        toMatch ForallC{} = String -> Match
forall a. HasCallStack => String -> a
error String
"Existential constructors (ForallC) are not supported yet!"
        toMatch GadtC{} = String -> Match
forall a. HasCallStack => String -> a
error String
"GADT constructors (GadtC) are not supported yet!"
        toMatch RecGadtC{} = String -> Match
forall a. HasCallStack => String -> a
error String
"Record GADT constructors (RecGadtC) are not supported yet!"

-- | Generate conversion function from raw to scope-safe pattern.
--
-- @since 0.1.0
mkFromFoilPattern
  :: Name -- ^ Type name for raw variable identifiers.
  -> Name -- ^ Type name for raw patterns.
  -> Q [Dec]
mkFromFoilPattern :: Name -> Name -> Q [Dec]
mkFromFoilPattern Name
nameT Name
patternT = do
  n <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"n"
  let ntype = Type -> Q Type
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> Type
VarT Name
n)
  l <- newName "l"
  let ltype = Type -> Q Type
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> Type
VarT Name
l)
  TyConI (DataD _ctx _name patternTVars _kind patternCons _deriv) <- reify patternT

  let patternParams = (TyVarBndr BndrVis -> Type) -> [TyVarBndr BndrVis] -> Cxt
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]
patternTVars

  fromFoilPatternSignature <-
    SigD fromFoilPatternT <$>
      [t| (Int -> $(return (ConT nameT)))
          -> $(return (PeelConT foilPatternT patternParams)) $ntype $ltype
          -> $(return (PeelConT patternT patternParams))
        |]

  addModFinalizer $ putDoc (DeclDoc fromFoilPatternT) $
    "/Generated/ with '" ++ show 'mkFromFoilPattern ++ "'. Convert a scope-safe pattern into a raw pattern."

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

    fromFoilPatternT :: Name
fromFoilPatternT = String -> Name
mkName (String
"fromFoil" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
nameBase Name
patternT)

    fromFoilPatternBody :: [Con] -> Dec
fromFoilPatternBody [Con]
patternCons = Name -> [Clause] -> Dec
FunD Name
fromFoilPatternT
      [[Pat] -> Body -> [Dec] -> Clause
Clause [Name -> Pat
VarP Name
toRawIdent, Name -> Pat
VarP Name
pattern] (Exp -> Body
NormalB (Exp -> [Match] -> Exp
CaseE (Name -> Exp
VarE Name
pattern) ((Con -> Match) -> [Con] -> [Match]
forall a b. (a -> b) -> [a] -> [b]
map Con -> Match
toMatch [Con]
patternCons))) []]
      where
        toRawIdent :: Name
toRawIdent = String -> Name
mkName String
"toRawIdent"
        pattern :: Name
pattern = String -> Name
mkName String
"pattern"

        toMatch :: Con -> Match
toMatch (NormalC Name
conName [BangType]
params) =
          Pat -> Body -> [Dec] -> Match
Match (Name -> Cxt -> [Pat] -> Pat
ConP Name
foilConName [] [Pat]
conParamPatterns) (Exp -> Body
NormalB Exp
conMatchBody) []
          where
            conMatchBody :: Exp
conMatchBody = Integer -> Exp -> [BangType] -> Exp
go Integer
1 (Name -> Exp
ConE Name
conName) [BangType]
params

            go :: Integer -> Exp -> [BangType] -> Exp
go Integer
_i Exp
p [] = Exp
p
            go Integer
i 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 -> [BangType] -> Exp
go (Integer
i Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1)
                  (Exp -> Exp -> Exp
AppE Exp
p (Exp -> Exp -> Exp
AppE (Name -> Exp
VarE Name
toRawIdent) (Exp -> Exp -> Exp
AppE (Name -> Exp
VarE 'Foil.nameId) (Exp -> Exp -> Exp
AppE (Name -> Exp
VarE 'Foil.nameOf) (Name -> Exp
VarE Name
xi)))))
                  [BangType]
conParams
              | Name
tyName Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
patternT = Integer -> Exp -> [BangType] -> Exp
go (Integer
iInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
+Integer
1)
                  (Exp -> Exp -> Exp
AppE Exp
p ((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
fromFoilPatternT) [Name -> Exp
VarE Name
toRawIdent, Name -> Exp
VarE Name
xi]))
                  [BangType]
conParams
              where
                xi :: Name
xi = String -> Name
mkName (String
"x" String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Integer -> String
forall a. Show a => a -> String
show Integer
i)
            go Integer
i Exp
p (BangType
_ : [BangType]
conParams) =
              Integer -> Exp -> [BangType] -> Exp
go (Integer
i Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1) (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. Semigroup a => a -> a -> a
<> Integer -> String
forall a. Show a => a -> String
show Integer
i)

            foilConName :: Name
foilConName = String -> Name
mkName (String
"Foil" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
nameBase Name
conName)
            conParamPatterns :: [Pat]
conParamPatterns = (Name -> Pat) -> [Name] -> [Pat]
forall a b. (a -> b) -> [a] -> [b]
map Name -> Pat
VarP [Name]
conParamVars

            conParamVars :: [Name]
conParamVars = (BangType -> Int -> Name) -> [BangType] -> [Int] -> [Name]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith BangType -> Int -> Name
mkConParamVar [BangType]
params [Int
1..]

            mkConParamVar :: BangType -> Int -> Name
            mkConParamVar :: BangType -> Int -> Name
mkConParamVar BangType
_ Int
i = String -> Name
mkName (String
"x" String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Int -> String
forall a. Show a => a -> String
show Int
i)
        toMatch RecC{} = String -> Match
forall a. HasCallStack => String -> a
error String
"Record constructors (RecC) are not supported yet!"
        toMatch InfixC{} = String -> Match
forall a. HasCallStack => String -> a
error String
"Infix constructors (InfixC) are not supported yet!"
        toMatch ForallC{} = String -> Match
forall a. HasCallStack => String -> a
error String
"Existential constructors (ForallC) are not supported yet!"
        toMatch GadtC{} = String -> Match
forall a. HasCallStack => String -> a
error String
"GADT constructors (GadtC) are not supported yet!"
        toMatch RecGadtC{} = String -> Match
forall a. HasCallStack => String -> a
error String
"Record GADT constructors (RecGadtC) are not supported yet!"