{-# 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.
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
  Name
n <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"n"
  let ntype :: Q Type
ntype = Type -> Q Type
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> Type
VarT Name
n)
  Name
l <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"l"
  let ltype :: Q Type
ltype = Type -> Q Type
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> Type
VarT Name
l)
  Name
r <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"r"
  let rtype :: Q Type
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 Cxt
_ctx Name
_name [TyVarBndr BndrVis]
patternTVars Maybe Type
_kind [Con]
patternCons [DerivClause]
_deriv) <- Name -> Q Info
reify Name
patternT
  TyConI (DataD Cxt
_ctx Name
_name [TyVarBndr BndrVis]
scopeTVars Maybe Type
_kind [Con]
scopeCons [DerivClause]
_deriv) <- Name -> Q Info
reify Name
scopeT
  TyConI (DataD Cxt
_ctx Name
_name [TyVarBndr BndrVis]
termTVars Maybe Type
_kind [Con]
termCons [DerivClause]
_deriv) <- Name -> Q Info
reify Name
termT

  let termParams :: Cxt
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 :: Cxt
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 :: Cxt
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

  Dec
fromFoilTermSignature <-
    Name -> Type -> Dec
SigD Name
fromFoilTermT (Type -> Dec) -> Q Type -> Q Dec
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
      [t| [$(Type -> Q Type
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> Type
ConT Name
nameT))]
          -> Foil.NameMap $Q Type
ntype $(Type -> Q Type
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> Type
ConT Name
nameT))
          -> $(Type -> Q Type
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> Cxt -> Type
PeelConT Name
foilTermT Cxt
termParams)) $Q Type
ntype
          -> $(Type -> Q Type
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> Cxt -> Type
PeelConT Name
termT Cxt
termParams))
        |]
  Dec
fromFoilScopedSignature <-
    Name -> Type -> Dec
SigD Name
fromFoilScopedT (Type -> Dec) -> Q Type -> Q Dec
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
      [t| [$(Type -> Q Type
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> Type
ConT Name
nameT))]
          -> Foil.NameMap $Q Type
ntype $(Type -> Q Type
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> Type
ConT Name
nameT))
          -> $(Type -> Q Type
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> Cxt -> Type
PeelConT Name
foilScopeT Cxt
scopeParams)) $Q Type
ntype
          -> $(Type -> Q Type
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> Cxt -> Type
PeelConT Name
scopeT Cxt
scopeParams))
        |]
  Dec
fromFoilPatternSignature <-
    Name -> Type -> Dec
SigD Name
fromFoilPatternT (Type -> Dec) -> Q Type -> Q Dec
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
      [t| [$(Type -> Q Type
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> Type
ConT Name
nameT))]
          -> Foil.NameMap $Q Type
ntype $(Type -> Q Type
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> Type
ConT Name
nameT))
          -> $(Type -> Q Type
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> Cxt -> Type
PeelConT Name
foilPatternT Cxt
patternParams)) $Q Type
ntype $Q Type
ltype
          -> ([$(Type -> Q Type
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> Type
ConT Name
nameT))] -> Foil.NameMap $Q Type
ltype $(Type -> Q Type
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> Type
ConT Name
nameT)) -> $(Type -> Q Type
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> Cxt -> Type
PeelConT Name
patternT Cxt
patternParams)) -> $Q Type
rtype)
          -> $Q Type
rtype
        |]

  Q () -> Q ()
addModFinalizer (Q () -> Q ()) -> Q () -> Q ()
forall a b. (a -> b) -> a -> b
$ DocLoc -> String -> Q ()
putDoc (Name -> DocLoc
DeclDoc Name
fromFoilTermT) (String -> Q ()) -> String -> Q ()
forall a b. (a -> b) -> a -> b
$
    String
"/Generated/ with '" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show 'mkFromFoil String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"'. Convert a scope-safe term into a raw term."
  Q () -> Q ()
addModFinalizer (Q () -> Q ()) -> Q () -> Q ()
forall a b. (a -> b) -> a -> b
$ DocLoc -> String -> Q ()
putDoc (Name -> DocLoc
DeclDoc Name
fromFoilPatternT) (String -> Q ()) -> String -> Q ()
forall a b. (a -> b) -> a -> b
$
    String
"/Generated/ with '" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show 'mkFromFoil String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"'. Convert a scope-safe pattern into a raw pattern."
  Q () -> Q ()
addModFinalizer (Q () -> Q ()) -> Q () -> Q ()
forall a b. (a -> b) -> a -> b
$ DocLoc -> String -> Q ()
putDoc (Name -> DocLoc
DeclDoc Name
fromFoilScopedT) (String -> Q ()) -> String -> Q ()
forall a b. (a -> b) -> a -> b
$
    String
"/Generated/ with '" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show 'mkFromFoil String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"'. Convert a scope-safe scoped term into a raw scoped term."

  [Dec] -> Q [Dec]
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return
    [ Dec
fromFoilTermSignature
    , [Con] -> Dec
fromFoilTermBody [Con]
termCons
    , Dec
fromFoilPatternSignature
    , [Con] -> Dec
fromFoilPatternBody [Con]
patternCons
    , Dec
fromFoilScopedSignature
    , [Con] -> Dec
fromFoilScopedBody [Con]
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.
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
  Name
n <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"n"
  let ntype :: Q Type
ntype = Type -> Q Type
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> Type
VarT Name
n)
  Name
l <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"l"
  let ltype :: Q Type
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 Cxt
_ctx Name
_name [TyVarBndr BndrVis]
patternTVars Maybe Type
_kind [Con]
patternCons [DerivClause]
_deriv) <- Name -> Q Info
reify Name
patternT

  let patternParams :: Cxt
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

  Dec
fromFoilPatternSignature <-
    Name -> Type -> Dec
SigD Name
fromFoilPatternT (Type -> Dec) -> Q Type -> Q Dec
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
      [t| (Int -> $(Type -> Q Type
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> Type
ConT Name
nameT)))
          -> $(Type -> Q Type
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> Cxt -> Type
PeelConT Name
foilPatternT Cxt
patternParams)) $Q Type
ntype $Q Type
ltype
          -> $(Type -> Q Type
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> Cxt -> Type
PeelConT Name
patternT Cxt
patternParams))
        |]

  Q () -> Q ()
addModFinalizer (Q () -> Q ()) -> Q () -> Q ()
forall a b. (a -> b) -> a -> b
$ DocLoc -> String -> Q ()
putDoc (Name -> DocLoc
DeclDoc Name
fromFoilPatternT) (String -> Q ()) -> String -> Q ()
forall a b. (a -> b) -> a -> b
$
    String
"/Generated/ with '" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show 'mkFromFoilPattern String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"'. Convert a scope-safe pattern into a raw pattern."

  [Dec] -> Q [Dec]
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return
    [ Dec
fromFoilPatternSignature
    , [Con] -> Dec
fromFoilPatternBody [Con]
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!"