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

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

import qualified Control.Monad.Foil  as Foil
import           Data.Maybe          (catMaybes)
import Data.Map (Map)
import qualified Data.Map as Map
import Control.Monad.Foil.TH.Util

-- | Generate conversion functions from raw to scope-safe representation.
mkToFoil
  :: 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]
mkToFoil :: Name -> Name -> Name -> Name -> Q [Dec]
mkToFoil Name
termT Name
nameT Name
scopeT Name
patternT = do
  [Dec]
extendScopeFoilPattenD <- Name -> Name -> Q [Dec]
mkExtendScopeFoilPattern Name
nameT Name
patternT
  [Dec]
withRefreshedFoilPatternD <- Name -> Name -> Q [Dec]
mkWithRefreshedFoilPattern Name
nameT Name
patternT
  [Dec]
toFoilTermD <- Name -> Name -> Name -> Name -> Q [Dec]
mkToFoilTerm Name
termT Name
nameT Name
scopeT Name
patternT
  [Dec] -> Q [Dec]
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return (
    [Dec]
extendScopeFoilPattenD [Dec] -> [Dec] -> [Dec]
forall a. [a] -> [a] -> [a]
++
    [Dec]
withRefreshedFoilPatternD [Dec] -> [Dec] -> [Dec]
forall a. [a] -> [a] -> [a]
++
    [Dec]
toFoilTermD
    )

-- | Generate a function to extend scope with variables from a given pattern.
mkExtendScopeFoilPattern
  :: Name -- ^ Type name for raw variable identifiers.
  -> Name -- ^ Type name for raw patterns.
  -> Q [Dec]
mkExtendScopeFoilPattern :: Name -> Name -> Q [Dec]
mkExtendScopeFoilPattern Name
nameT Name
patternT = do
  Name
n <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"n"
  Name
l <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"l"
  TyConI (DataD Cxt
_ctx Name
_name [TyVarBndr BndrVis]
patternTVars Maybe Kind
_kind [Con]
patternCons [DerivClause]
_deriv) <- Name -> Q Info
reify Name
patternT

  let extendScopePatternSignature :: Dec
extendScopePatternSignature =
        Name -> Kind -> Dec
SigD Name
extendScopePatternFunName (Kind -> Dec) -> Kind -> Dec
forall a b. (a -> b) -> a -> b
$
          [TyVarBndr Specificity] -> Cxt -> Kind -> Kind
ForallT ([ Name -> Specificity -> TyVarBndr Specificity
forall flag. Name -> flag -> TyVarBndr flag
PlainTV Name
name Specificity
SpecifiedSpec | Name
name <- ((TyVarBndr BndrVis -> Name) -> [TyVarBndr BndrVis] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map TyVarBndr BndrVis -> Name
forall a. TyVarBndr a -> Name
tvarName [TyVarBndr BndrVis]
patternTVars [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ [Name
n, Name
l]) ]) []
            (Kind -> Kind -> Kind
AppT (Kind -> Kind -> Kind
AppT Kind
ArrowT
              (Name -> Cxt -> Kind
PeelConT Name
foilPatternT [ Name -> Kind
VarT Name
name | Name
name <- ((TyVarBndr BndrVis -> Name) -> [TyVarBndr BndrVis] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map TyVarBndr BndrVis -> Name
forall a. TyVarBndr a -> Name
tvarName [TyVarBndr BndrVis]
patternTVars [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ [Name
n, Name
l]) ]))
              (Kind -> Kind -> Kind
AppT (Kind -> Kind -> Kind
AppT Kind
ArrowT
                (Kind -> Kind -> Kind
AppT (Name -> Kind
ConT ''Foil.Scope) (Name -> Kind
VarT Name
n)))
                (Kind -> Kind -> Kind
AppT (Name -> Kind
ConT ''Foil.Scope) (Name -> Kind
VarT Name
l))))

  Exp
composefun <- [e| (.) |]
  Exp
idfun <- [e| id |]
  Exp
extendScopeFun <- [e| Foil.extendScope |]

  Q () -> Q ()
addModFinalizer (Q () -> Q ()) -> Q () -> Q ()
forall a b. (a -> b) -> a -> b
$ DocLoc -> String -> Q ()
putDoc (Name -> DocLoc
DeclDoc Name
extendScopePatternFunName) (String -> Q ()) -> String -> Q ()
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines
    [ String
"/Generated/ with '" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show 'mkExtendScopeFoilPattern String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"'."
    , String
"Extend a scope with the names bound by the given pattern."
    , String
"This is a more flexible version of '" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show 'Foil.extendScope String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"'." ]

  [Dec] -> Q [Dec]
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return
    [ Dec
extendScopePatternSignature
    , Exp -> Exp -> Exp -> [Con] -> Dec
extendScopePatternBody Exp
extendScopeFun Exp
composefun Exp
idfun [Con]
patternCons
    ]
  where
    foilPatternT :: Name
foilPatternT = String -> Name
mkName (String
"Foil" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
nameBase Name
patternT)

    extendScopePatternFunName :: Name
extendScopePatternFunName = String -> Name
mkName (String
"extendScopeFoil" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
nameBase Name
patternT)
    extendScopePatternBody :: Exp -> Exp -> Exp -> [Con] -> Dec
extendScopePatternBody Exp
extendScopeFun Exp
composefun Exp
idfun [Con]
patternCons = Name -> [Clause] -> Dec
FunD Name
extendScopePatternFunName
      [[Pat] -> Body -> [Dec] -> Clause
Clause [Name -> Pat
VarP Name
p] (Exp -> Body
NormalB (Exp -> [Match] -> Exp
CaseE (Name -> Exp
VarE Name
p) ((Con -> Match) -> [Con] -> [Match]
forall a b. (a -> b) -> [a] -> [b]
map Con -> Match
toMatch [Con]
patternCons))) []]
      where
        p :: Name
p = String -> Name
mkName String
"pattern"
        toMatch :: Con -> Match
toMatch (NormalC Name
conName [BangType]
conParams) =
          Pat -> Body -> [Dec] -> Match
Match (Name -> Cxt -> [Pat] -> Pat
ConP Name
foilConName [] [Pat]
conParamPatterns) (Exp -> Body
NormalB Exp
conMatchBody) []
          where
            foilConName :: Name
foilConName = String -> Name
mkName (String
"Foil" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
nameBase Name
conName)
            conParamPatterns :: [Pat]
conParamPatterns = (Maybe (Name, Exp) -> Pat) -> [Maybe (Name, Exp)] -> [Pat]
forall a b. (a -> b) -> [a] -> [b]
map Maybe (Name, Exp) -> Pat
forall {b}. Maybe (Name, b) -> Pat
toConParamPattern [Maybe (Name, Exp)]
conParamVars
            conMatchExts :: [Exp]
conMatchExts = ((Name, Exp) -> Exp) -> [(Name, Exp)] -> [Exp]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Exp) -> Exp
forall a b. (a, b) -> b
snd ([Maybe (Name, Exp)] -> [(Name, Exp)]
forall a. [Maybe a] -> [a]
catMaybes [Maybe (Name, Exp)]
conParamVars)
            conMatchBody :: Exp
conMatchBody = (Exp -> Exp -> Exp) -> Exp -> [Exp] -> Exp
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\Exp
f Exp
g -> Maybe Exp -> Exp -> Maybe Exp -> Exp
InfixE (Exp -> Maybe Exp
forall a. a -> Maybe a
Just Exp
g) Exp
composefun (Exp -> Maybe Exp
forall a. a -> Maybe a
Just Exp
f)) Exp
idfun [Exp]
conMatchExts

            toConParamPattern :: Maybe (Name, b) -> Pat
toConParamPattern Maybe (Name, b)
Nothing = Pat
WildP
            toConParamPattern (Just (Name
x, b
_f)) = Name -> Pat
VarP Name
x

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

            mkConParamVar :: BangType -> Int -> Maybe (Name, Exp)
            mkConParamVar :: BangType -> Int -> Maybe (Name, Exp)
mkConParamVar (Bang
_bang, PeelConT Name
tyName Cxt
_tyParams) Int
i
              | Name
tyName Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
nameT    = (Name, Exp) -> Maybe (Name, Exp)
forall a. a -> Maybe a
Just (Name
x, Exp -> Exp -> Exp
AppE Exp
extendScopeFun (Name -> Exp
VarE Name
x))
              | Name
tyName Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
patternT = (Name, Exp) -> Maybe (Name, Exp)
forall a. a -> Maybe a
Just (Name
x, Exp -> Exp -> Exp
AppE (Name -> Exp
VarE Name
extendScopePatternFunName) (Name -> Exp
VarE Name
x))
              where
                x :: Name
x = 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)
            mkConParamVar (Bang
_bang, Kind
_type) Int
_i = Maybe (Name, Exp)
forall a. Maybe a
Nothing
        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 a function to extend scope with variables from a given pattern.
mkWithRefreshedFoilPattern
  :: Name -- ^ Type name for raw variable identifiers.
  -> Name -- ^ Type name for raw patterns.
  -> Q [Dec]
mkWithRefreshedFoilPattern :: Name -> Name -> Q [Dec]
mkWithRefreshedFoilPattern Name
nameT Name
patternT = do
  Name
o <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"o"
  Name
o' <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"o'"
  Name
e <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"e"
  Name
n <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"n"
  Name
l <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"l"
  Name
r <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"r"
  TyConI (DataD Cxt
_ctx Name
_name [TyVarBndr BndrVis]
patternTVars Maybe Kind
_kind [Con]
patternCons [DerivClause]
_deriv) <- Name -> Q Info
reify Name
patternT

  let withRefreshedFoilPatternSignature :: Dec
withRefreshedFoilPatternSignature =
        Name -> Kind -> Dec
SigD Name
withRefreshedFoilPatternFunName (Kind -> Dec) -> Kind -> Dec
forall a b. (a -> b) -> a -> b
$
          [TyVarBndr Specificity] -> Cxt -> Kind -> Kind
ForallT
            [ Name -> Specificity -> TyVarBndr Specificity
forall flag. Name -> flag -> TyVarBndr flag
PlainTV Name
name Specificity
SpecifiedSpec | Name
name <- (TyVarBndr BndrVis -> Name) -> [TyVarBndr BndrVis] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map TyVarBndr BndrVis -> Name
forall a. TyVarBndr a -> Name
tvarName [TyVarBndr BndrVis]
patternTVars [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ [Name
o, Name
e, Name
n, Name
l, Name
r] ]
            [ Kind -> Kind -> Kind
AppT (Name -> Kind
ConT ''Foil.Distinct) (Name -> Kind
VarT Name
o)
            , Kind -> Kind -> Kind
AppT (Name -> Kind
ConT ''Foil.InjectName) (Name -> Kind
VarT Name
e)
            , Kind -> Kind -> Kind
AppT (Name -> Kind
ConT ''Foil.Sinkable) (Name -> Kind
VarT Name
e)
            ]
            (Kind -> Kind -> Kind
AppT (Kind -> Kind -> Kind
AppT Kind
ArrowT (Name -> Cxt -> Kind
PeelConT ''Foil.Scope [Name -> Kind
VarT Name
o]))
              (Kind -> Kind -> Kind
AppT (Kind -> Kind -> Kind
AppT Kind
ArrowT (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 Cxt -> Cxt -> Cxt
forall a. [a] -> [a] -> [a]
++ [Name -> Kind
VarT Name
n, Name -> Kind
VarT Name
l])))
                (Kind -> Kind -> Kind
AppT (Kind -> Kind -> Kind
AppT Kind
ArrowT
                  ([TyVarBndr Specificity] -> Cxt -> Kind -> Kind
ForallT [Name -> Specificity -> TyVarBndr Specificity
forall flag. Name -> flag -> TyVarBndr flag
PlainTV Name
o' Specificity
SpecifiedSpec] [Name -> Cxt -> Kind
PeelConT ''Foil.DExt [Name -> Kind
VarT Name
o, Name -> Kind
VarT Name
o']]
                    (Kind -> Kind -> Kind
AppT (Kind -> Kind -> Kind
AppT Kind
ArrowT (Kind -> Kind -> Kind
AppT (Kind -> Kind -> Kind
AppT Kind
ArrowT (Name -> Cxt -> Kind
PeelConT ''Foil.Substitution [Name -> Kind
VarT Name
e, Name -> Kind
VarT Name
n, Name -> Kind
VarT Name
o])) (Name -> Cxt -> Kind
PeelConT ''Foil.Substitution [Name -> Kind
VarT Name
e, Name -> Kind
VarT Name
l, Name -> Kind
VarT Name
o'])))
                      (Kind -> Kind -> Kind
AppT (Kind -> Kind -> Kind
AppT Kind
ArrowT (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 Cxt -> Cxt -> Cxt
forall a. [a] -> [a] -> [a]
++ [Name -> Kind
VarT Name
o, Name -> Kind
VarT Name
o'])))
                        (Name -> Kind
VarT Name
r)))))
                  (Name -> Kind
VarT Name
r))))

        --           [t| ( Foil.Distinct o, Foil.InjectName e, Foil.Sinkable e )
        --     => Foil.Scope o
        --     -> $(return (PeelConT foilPatternT (map (VarT . tyName patternTVars)))) n l
        --     -> (forall o'. Foil.DExt o o'
        --           => (Foil.Substitution e n o -> Foil.Substitution e l o')
        --           -> $(return (ConT foilPatternT)) o o'
        --           -> r)
        --     -> r
        -- |]

  Exp
composefun <- [e| (.) |]
  Exp
addRenameFun <- [e| Foil.addRename |]
  Exp
nameOfFun <- [e| Foil.nameOf |]
  Exp
sinkFun <- [e| Foil.sink |]
  Exp
withRefreshedFun <- [e| Foil.withRefreshed |]
  Exp
extendScopeFun <- [e| Foil.extendScope |]

  Q () -> Q ()
addModFinalizer (Q () -> Q ()) -> Q () -> Q ()
forall a b. (a -> b) -> a -> b
$ DocLoc -> String -> Q ()
putDoc (Name -> DocLoc
DeclDoc Name
withRefreshedFoilPatternFunName) (String -> Q ()) -> String -> Q ()
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines
    [ String
"/Generated/ with '" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show 'mkWithRefreshedFoilPattern String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"'."
    , String
"Refresh (if needed) bound variables introduced in a pattern."
    , String
"This is a more flexible version of '" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show 'Foil.withRefreshed String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"'." ]

  [Dec] -> Q [Dec]
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return
    [ Dec
withRefreshedFoilPatternSignature
    , Exp -> Exp -> Exp -> Exp -> Exp -> Exp -> [Con] -> Dec
withRefreshedFoilPatternBody Exp
composefun Exp
addRenameFun Exp
nameOfFun Exp
sinkFun Exp
withRefreshedFun Exp
extendScopeFun [Con]
patternCons
    ]
  where
    foilPatternT :: Name
foilPatternT = String -> Name
mkName (String
"Foil" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
nameBase Name
patternT)

    extendScopePatternFunName :: Name
extendScopePatternFunName = String -> Name
mkName (String
"extendScopeFoil" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
nameBase Name
patternT)
    extendScopePatternFun :: Exp
extendScopePatternFun = Name -> Exp
VarE Name
extendScopePatternFunName

    withRefreshedFoilPatternFunName :: Name
withRefreshedFoilPatternFunName = String -> Name
mkName (String
"withRefreshedFoil" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
nameBase Name
patternT)
    withRefreshedFoilPatternFun :: Exp
withRefreshedFoilPatternFun = Name -> Exp
VarE Name
withRefreshedFoilPatternFunName

    withRefreshedFoilPatternBody :: Exp -> Exp -> Exp -> Exp -> Exp -> Exp -> [Con] -> Dec
withRefreshedFoilPatternBody Exp
composefun Exp
addRenameFun Exp
nameOfFun Exp
sinkFun Exp
withRefreshedFun Exp
extendScopeFun [Con]
patternCons = Name -> [Clause] -> Dec
FunD Name
withRefreshedFoilPatternFunName
      [[Pat] -> Body -> [Dec] -> Clause
Clause [Name -> Pat
VarP Name
scope, 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
        scope :: Name
scope = String -> Name
mkName String
"scope"
        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
scope) Exp
sinkFun (Name -> Exp
ConE Name
foilConName) [BangType]
params

            go :: Integer -> Exp -> Exp -> Exp -> [BangType] -> Exp
go Integer
_i Exp
_scope' Exp
f Exp
p [] = Exp -> Exp -> Exp
AppE (Exp -> Exp -> Exp
AppE (Name -> Exp
VarE Name
cont) Exp
f) Exp
p
            go Integer
i Exp
scope' Exp
f 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 -> Exp -> Exp
AppE
                    (Exp -> Exp -> Exp
AppE (Exp -> Exp -> Exp
AppE Exp
withRefreshedFun Exp
scope') (Exp -> Exp -> Exp
AppE Exp
nameOfFun (Name -> Exp
VarE Name
xi)))
                    ([Pat] -> Exp -> Exp
LamE [Name -> Pat
VarP Name
xi']
                      ([Dec] -> Exp -> Exp
LetE [Pat -> Body -> [Dec] -> Dec
ValD (Name -> Pat
VarP Name
scopei) (Exp -> Body
NormalB (Exp -> Exp -> Exp
AppE (Exp -> Exp -> Exp
AppE Exp
extendScopeFun (Name -> Exp
VarE Name
xi')) Exp
scope')) []]
                        (Integer -> Exp -> Exp -> Exp -> [BangType] -> Exp
go (Integer
iInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
+Integer
1) (Name -> Exp
VarE Name
scopei) (Maybe Exp -> Exp -> Maybe Exp -> Exp
InfixE (Exp -> Maybe Exp
forall a. a -> Maybe a
Just Exp
fi) Exp
composefun (Exp -> Maybe Exp
forall a. a -> Maybe a
Just Exp
f)) (Exp -> Exp -> Exp
AppE Exp
p (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
withRefreshedFoilPatternFun Exp
scope') (Name -> Exp
VarE Name
xi))
                    ([Pat] -> Exp -> Exp
LamE [Name -> Pat
VarP Name
xsubst, Name -> Pat
VarP Name
xi']
                      ([Dec] -> Exp -> Exp
LetE [Pat -> Body -> [Dec] -> Dec
ValD (Name -> Pat
VarP Name
scopei) (Exp -> Body
NormalB (Exp -> Exp -> Exp
AppE (Exp -> Exp -> Exp
AppE Exp
extendScopePatternFun (Name -> Exp
VarE Name
xi')) Exp
scope')) []]
                        (Integer -> Exp -> Exp -> Exp -> [BangType] -> Exp
go (Integer
iInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
+Integer
1) (Name -> Exp
VarE Name
scopei) (Maybe Exp -> Exp -> Maybe Exp -> Exp
InfixE (Exp -> Maybe Exp
forall a. a -> Maybe a
Just (Name -> Exp
VarE Name
xsubst)) Exp
composefun (Exp -> Maybe Exp
forall a. a -> Maybe a
Just Exp
f)) (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
"'")
                scopei :: Name
scopei = String -> Name
mkName (String
"_scope" String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Integer -> String
forall a. Show a => a -> String
show Integer
i)
                xsubst :: Name
xsubst = String -> Name
mkName (String
"subst" String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Integer -> String
forall a. Show a => a -> String
show Integer
i)
                subst :: Name
subst = String -> Name
mkName String
"subst"
                fi :: Exp
fi = [Pat] -> Exp -> Exp
LamE [Name -> Pat
VarP Name
subst]
                      (Exp -> Exp -> Exp
AppE (Exp -> Exp -> Exp
AppE (Exp -> Exp -> Exp
AppE Exp
addRenameFun
                        (Name -> Exp
VarE Name
subst))
                        (Name -> Exp
VarE Name
xi))
                        (Exp -> Exp -> Exp
AppE Exp
nameOfFun (Name -> Exp
VarE Name
xi')))
            go Integer
i Exp
scope' Exp
f 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
scope' Exp
f (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!"

-- | Generate a conversion function from raw terms to scope-safe terms.
mkToFoilTerm
  :: 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]
mkToFoilTerm :: Name -> Name -> Name -> Name -> Q [Dec]
mkToFoilTerm 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 Kind
ntype = Kind -> Q Kind
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> Kind
VarT Name
n)
  Name
r <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"r"
  let rtype :: Q Kind
rtype = Kind -> Q Kind
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> Kind
VarT Name
r)
  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
toFoilTermSignature <-
    Name -> Kind -> Dec
SigD Name
toFoilTermT (Kind -> Dec) -> Q Kind -> Q Dec
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
      [t| Foil.Distinct $Q Kind
ntype
          => Foil.Scope $Q Kind
ntype
          -> Map $(Kind -> Q Kind
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> Kind
ConT Name
nameT)) (Foil.Name $Q Kind
ntype)
          -> $(Kind -> Q Kind
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> Cxt -> Kind
PeelConT Name
termT ((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 )))
          -> $(Kind -> Q Kind
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return (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))) $Q Kind
ntype
        |]
  Dec
toFoilScopedSignature <-
    Name -> Kind -> Dec
SigD Name
toFoilScopedT (Kind -> Dec) -> Q Kind -> Q Dec
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
      [t| Foil.Distinct $Q Kind
ntype
          => Foil.Scope $Q Kind
ntype
          -> Map $(Kind -> Q Kind
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> Kind
ConT Name
nameT)) (Foil.Name $Q Kind
ntype)
          -> $(Kind -> Q Kind
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> Cxt -> Kind
PeelConT Name
scopeT ((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)))
          -> $(Kind -> Q Kind
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return (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))) $Q Kind
ntype
        |]
  Dec
toFoilPatternSignature <-
    Name -> Kind -> Dec
SigD Name
toFoilPatternT (Kind -> Dec) -> Q Kind -> Q Dec
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
      [t| Foil.Distinct $Q Kind
ntype
          => Foil.Scope $Q Kind
ntype
          -> Map $(Kind -> Q Kind
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> Kind
ConT Name
nameT)) (Foil.Name $Q Kind
ntype)
          -> $(Kind -> Q Kind
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> Cxt -> Kind
PeelConT Name
patternT ((TyVarBndr BndrVis -> Kind) -> [TyVarBndr BndrVis] -> Cxt
forall a b. (a -> b) -> [a] -> [b]
map (Name -> Kind
VarT (Name -> Kind)
-> (TyVarBndr BndrVis -> Name) -> TyVarBndr BndrVis -> Kind
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyVarBndr BndrVis -> Name
forall a. TyVarBndr a -> Name
tvarName) [TyVarBndr BndrVis]
patternTVars)))
          -> (forall l. Foil.DExt $Q Kind
ntype l => $(Kind -> Q Kind
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return (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))) $Q Kind
ntype l -> Map $(Kind -> Q Kind
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> Kind
ConT Name
nameT)) (Foil.Name l) -> $Q Kind
rtype)
          -> $Q Kind
rtype
        |]

  Q () -> Q ()
addModFinalizer (Q () -> Q ()) -> Q () -> Q ()
forall a b. (a -> b) -> a -> b
$ DocLoc -> String -> Q ()
putDoc (Name -> DocLoc
DeclDoc Name
toFoilTermT) (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 'mkToFoilTerm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"'. Convert a raw term into a scope-safe term."
  Q () -> Q ()
addModFinalizer (Q () -> Q ()) -> Q () -> Q ()
forall a b. (a -> b) -> a -> b
$ DocLoc -> String -> Q ()
putDoc (Name -> DocLoc
DeclDoc Name
toFoilPatternT) (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 'mkToFoilTerm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"'. Convert a raw pattern into a scope-safe pattern."
  Q () -> Q ()
addModFinalizer (Q () -> Q ()) -> Q () -> Q ()
forall a b. (a -> b) -> a -> b
$ DocLoc -> String -> Q ()
putDoc (Name -> DocLoc
DeclDoc Name
toFoilScopedT) (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 'mkToFoilTerm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"'. Convert a raw scoped term into a scope-safe scoped term."

  [Dec] -> Q [Dec]
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return
    [ Dec
toFoilTermSignature
    , [Con] -> Dec
toFoilTermBody [Con]
termCons
    , Dec
toFoilPatternSignature
    , [Con] -> Dec
toFoilPatternBody [Con]
patternCons
    , Dec
toFoilScopedSignature
    , [Con] -> Dec
toFoilScopedBody [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)

    toFoilTermT :: Name
toFoilTermT = String -> Name
mkName (String
"toFoil" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
nameBase Name
termT)
    toFoilPatternT :: Name
toFoilPatternT = String -> Name
mkName (String
"toFoil" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
nameBase Name
patternT)
    toFoilScopedT :: Name
toFoilScopedT = String -> Name
mkName (String
"toFoil" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
nameBase Name
scopeT)

    extendScopePatternFunName :: Name
extendScopePatternFunName = String -> Name
mkName (String
"extendScopeFoil" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
nameBase Name
patternT)
    extendScopePatternFun :: Exp
extendScopePatternFun = Name -> Exp
VarE Name
extendScopePatternFunName

    toFoilTermBody :: [Con] -> Dec
toFoilTermBody [Con]
termCons = Name -> [Clause] -> Dec
FunD Name
toFoilTermT
      [[Pat] -> Body -> [Dec] -> Clause
Clause [Name -> Pat
VarP Name
scope, 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
        scope :: Name
scope = String -> Name
mkName String
"scope"
        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
conName [] [Pat]
conParamPatterns) (Exp -> Body
NormalB Exp
conMatchBody) [Dec
toFoilVarD]
          where
            toFoilVarFunName :: Name
toFoilVarFunName = String -> Name
mkName String
"_lookupRawVar"
            toFoilVarFun :: Exp
toFoilVarFun = Name -> Exp
VarE Name
toFoilVarFunName
            x :: Name
x = String -> Name
mkName String
"x"
            name :: Name
name = String -> Name
mkName String
"name"
            toFoilVarD :: Dec
toFoilVarD = Name -> [Clause] -> Dec
FunD Name
toFoilVarFunName [[Pat] -> Body -> [Dec] -> Clause
Clause [Name -> Pat
VarP Name
x]
              (Exp -> Body
NormalB (Exp -> [Match] -> Exp
CaseE (Exp -> Exp -> Exp
AppE (Exp -> Exp -> Exp
AppE (Name -> Exp
VarE 'Map.lookup) (Name -> Exp
VarE Name
x)) (Name -> Exp
VarE Name
env))
                [ Pat -> Body -> [Dec] -> Match
Match (Name -> Cxt -> [Pat] -> Pat
ConP 'Just [] [Name -> Pat
VarP Name
name]) (Exp -> Body
NormalB (Name -> Exp
VarE Name
name)) []
                , Pat -> Body -> [Dec] -> Match
Match (Name -> Cxt -> [Pat] -> Pat
ConP 'Nothing [] []) (Exp -> Body
NormalB (Exp -> Exp -> Exp
AppE (Name -> Exp
VarE 'error) (Lit -> Exp
LitE (String -> Lit
StringL String
"undefined variable")))) []]))
              []]

            conMatchBody :: Exp
conMatchBody = Integer -> Exp -> Exp -> Exp -> [BangType] -> Exp
go Integer
1 (Name -> Exp
VarE Name
scope) (Name -> Exp
VarE Name
env) (Name -> Exp
ConE Name
foilConName) [BangType]
params

            go :: Integer -> Exp -> Exp -> Exp -> [BangType] -> Exp
go Integer
_i Exp
_scope' Exp
_env' Exp
p [] = Exp
p
            go Integer
i Exp
scope' 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
scope' Exp
env' (Exp -> Exp -> Exp
AppE Exp
p (Exp -> Exp -> Exp
AppE Exp
toFoilVarFun (Name -> Exp
VarE Name
xi))) [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
scope' Exp
env' (Exp -> Exp -> Exp
AppE Exp
p (Exp -> Exp -> Exp
AppE (Exp -> Exp -> Exp
AppE (Exp -> Exp -> Exp
AppE (Name -> Exp
VarE Name
toFoilTermT) (Name -> Exp
VarE Name
scope)) (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
scope' Exp
env' (Exp -> Exp -> Exp
AppE Exp
p (Exp -> Exp -> Exp
AppE (Exp -> Exp -> Exp
AppE (Exp -> Exp -> Exp
AppE (Name -> Exp
VarE Name
toFoilScopedT) Exp
scope') 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
toFoilPatternT) Exp
scope') Exp
env') (Name -> Exp
VarE Name
xi))
                    ([Pat] -> Exp -> Exp
LamE [Name -> Pat
VarP Name
xi', Name -> Pat
VarP Name
envi]
                      ([Dec] -> Exp -> Exp
LetE [Pat -> Body -> [Dec] -> Dec
ValD (Name -> Pat
VarP Name
scopei) (Exp -> Body
NormalB (Exp -> Exp -> Exp
AppE (Exp -> Exp -> Exp
AppE Exp
extendScopePatternFun (Name -> Exp
VarE Name
xi')) Exp
scope')) []]
                        (Integer -> Exp -> Exp -> Exp -> [BangType] -> Exp
go (Integer
iInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
+Integer
1) (Name -> Exp
VarE Name
scopei) (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
"'")
                scopei :: Name
scopei = String -> Name
mkName (String
"_scope" 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
scope' 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
scope' 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!"

    toFoilPatternBody :: [Con] -> Dec
toFoilPatternBody [Con]
patternCons = Name -> [Clause] -> Dec
FunD Name
toFoilPatternT
      [[Pat] -> Body -> [Dec] -> Clause
Clause [Name -> Pat
VarP Name
scope, 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
        scope :: Name
scope = String -> Name
mkName String
"scope"
        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
conName [] [Pat]
conParamPatterns) (Exp -> Body
NormalB Exp
conMatchBody) []
          where
            conMatchBody :: Exp
conMatchBody = Integer -> Exp -> Exp -> Exp -> [BangType] -> Exp
go Integer
1 (Name -> Exp
VarE Name
scope) (Name -> Exp
VarE Name
env) (Name -> Exp
ConE Name
foilConName) [BangType]
params

            go :: Integer -> Exp -> Exp -> Exp -> [BangType] -> Exp
go Integer
_i Exp
_scope' Exp
env' Exp
p [] = Exp -> Exp -> Exp
AppE (Exp -> Exp -> Exp
AppE (Name -> Exp
VarE Name
cont) Exp
p) Exp
env'
            go Integer
i Exp
scope' 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 -> Exp -> Exp
AppE (Exp -> Exp -> Exp
AppE (Name -> Exp
VarE 'Foil.withFresh) Exp
scope')
                    ([Pat] -> Exp -> Exp
LamE [Name -> Pat
VarP Name
xi']
                      ([Dec] -> Exp -> Exp
LetE [ Pat -> Body -> [Dec] -> Dec
ValD (Name -> Pat
VarP Name
scopei) (Exp -> Body
NormalB (Exp -> Exp -> Exp
AppE (Exp -> Exp -> Exp
AppE (Name -> Exp
VarE 'Foil.extendScope) (Name -> Exp
VarE Name
xi')) Exp
scope')) []
                            , 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 'Map.insert) (Name -> Exp
VarE Name
xi))
                                  (Exp -> Exp -> Exp
AppE (Name -> Exp
VarE 'Foil.nameOf) (Name -> Exp
VarE Name
xi')))
                                  (Maybe Exp -> Exp -> Maybe Exp -> Exp
InfixE (Exp -> Maybe Exp
forall a. a -> Maybe a
Just (Name -> Exp
VarE 'Foil.sink)) (Name -> Exp
VarE '(<$>)) (Exp -> Maybe Exp
forall a. a -> Maybe a
Just Exp
env')))) []]
                        (Integer -> Exp -> Exp -> Exp -> [BangType] -> Exp
go (Integer
iInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
+Integer
1) (Name -> Exp
VarE Name
scopei) (Name -> Exp
VarE Name
envi) (Exp -> Exp -> Exp
AppE Exp
p (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
toFoilPatternT) Exp
scope') Exp
env') (Name -> Exp
VarE Name
xi))
                    ([Pat] -> Exp -> Exp
LamE [Name -> Pat
VarP Name
xi', Name -> Pat
VarP Name
envi]
                      ([Dec] -> Exp -> Exp
LetE [Pat -> Body -> [Dec] -> Dec
ValD (Name -> Pat
VarP Name
scopei) (Exp -> Body
NormalB (Exp -> Exp -> Exp
AppE (Exp -> Exp -> Exp
AppE Exp
extendScopePatternFun (Name -> Exp
VarE Name
xi')) Exp
scope')) []]
                        (Integer -> Exp -> Exp -> Exp -> [BangType] -> Exp
go (Integer
iInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
+Integer
1) (Name -> Exp
VarE Name
scopei) (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
"'")
                scopei :: Name
scopei = String -> Name
mkName (String
"_scope" 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
scope' 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
scope' 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!"

    toFoilScopedBody :: [Con] -> Dec
toFoilScopedBody [Con]
scopeCons = Name -> [Clause] -> Dec
FunD Name
toFoilScopedT
      [[Pat] -> Body -> [Dec] -> Clause
Clause [Name -> Pat
VarP Name
scope, 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]
scopeCons))) []]
      where
        scope :: Name
scope = String -> Name
mkName String
"scope"
        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
conName [] [Pat]
conParamPatterns) (Exp -> Body
NormalB Exp
conMatchBody) [Dec
toFoilVarD]
          where
            toFoilVarFunName :: Name
toFoilVarFunName = String -> Name
mkName String
"_lookupRawVar"
            toFoilVarFun :: Exp
toFoilVarFun = Name -> Exp
VarE Name
toFoilVarFunName
            x :: Name
x = String -> Name
mkName String
"x"
            name :: Name
name = String -> Name
mkName String
"name"
            toFoilVarD :: Dec
toFoilVarD = Name -> [Clause] -> Dec
FunD Name
toFoilVarFunName [[Pat] -> Body -> [Dec] -> Clause
Clause [Name -> Pat
VarP Name
x]
              (Exp -> Body
NormalB (Exp -> [Match] -> Exp
CaseE (Exp -> Exp -> Exp
AppE (Exp -> Exp -> Exp
AppE (Name -> Exp
VarE 'Map.lookup) (Name -> Exp
VarE Name
x)) (Name -> Exp
VarE Name
env))
                [ Pat -> Body -> [Dec] -> Match
Match (Name -> Cxt -> [Pat] -> Pat
ConP 'Just [] [Name -> Pat
VarP Name
name]) (Exp -> Body
NormalB (Name -> Exp
VarE Name
name)) []
                , Pat -> Body -> [Dec] -> Match
Match (Name -> Cxt -> [Pat] -> Pat
ConP 'Nothing [] []) (Exp -> Body
NormalB (Exp -> Exp -> Exp
AppE (Name -> Exp
VarE 'error) (Lit -> Exp
LitE (String -> Lit
StringL String
"undefined variable")))) []]))
              []]

            conMatchBody :: Exp
conMatchBody = Integer -> Exp -> Exp -> Exp -> [BangType] -> Exp
go Integer
1 (Name -> Exp
VarE Name
scope) (Name -> Exp
VarE Name
env) (Name -> Exp
ConE Name
foilConName) [BangType]
params

            go :: Integer -> Exp -> Exp -> Exp -> [BangType] -> Exp
go Integer
_i Exp
_scope' Exp
_env' Exp
p [] = Exp
p
            go Integer
i Exp
scope' 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
scope' Exp
env' (Exp -> Exp -> Exp
AppE Exp
p (Exp -> Exp -> Exp
AppE Exp
toFoilVarFun (Name -> Exp
VarE Name
xi))) [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
scope' Exp
env' (Exp -> Exp -> Exp
AppE Exp
p (Exp -> Exp -> Exp
AppE (Exp -> Exp -> Exp
AppE (Exp -> Exp -> Exp
AppE (Name -> Exp
VarE Name
toFoilTermT) (Name -> Exp
VarE Name
scope)) (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
scope' Exp
env' (Exp -> Exp -> Exp
AppE Exp
p (Exp -> Exp -> Exp
AppE (Exp -> Exp -> Exp
AppE (Exp -> Exp -> Exp
AppE (Name -> Exp
VarE Name
toFoilScopedT) Exp
scope') 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
toFoilPatternT) Exp
scope') Exp
env') (Name -> Exp
VarE Name
xi))
                    ([Pat] -> Exp -> Exp
LamE [Name -> Pat
VarP Name
xi', Name -> Pat
VarP Name
envi]
                      ([Dec] -> Exp -> Exp
LetE [Pat -> Body -> [Dec] -> Dec
ValD (Name -> Pat
VarP Name
scopei) (Exp -> Body
NormalB (Exp -> Exp -> Exp
AppE (Exp -> Exp -> Exp
AppE Exp
extendScopePatternFun (Name -> Exp
VarE Name
xi')) Exp
scope')) []]
                        (Integer -> Exp -> Exp -> Exp -> [BangType] -> Exp
go (Integer
iInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
+Integer
1) (Name -> Exp
VarE Name
scopei) (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
"'")
                scopei :: Name
scopei = String -> Name
mkName (String
"_scope" 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
scope' 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
scope' 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 a conversion function from raw terms to scope-safe terms.
mkToFoilPattern
  :: Name -- ^ Type name for raw variable identifiers.
  -> Name -- ^ Type name for raw patterns.
  -> Q [Dec]
mkToFoilPattern :: Name -> Name -> Q [Dec]
mkToFoilPattern Name
nameT Name
patternT = do
  Name
n <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"n"
  let ntype :: Q Kind
ntype = Kind -> Q Kind
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> Kind
VarT Name
n)
  Name
r <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"r"
  let rtype :: Q Kind
rtype = Kind -> Q Kind
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> Kind
VarT Name
r)
  TyConI (DataD Cxt
_ctx Name
_name [TyVarBndr BndrVis]
patternTVars Maybe Kind
_kind [Con]
patternCons [DerivClause]
_deriv) <- Name -> Q Info
reify Name
patternT

  Dec
toFoilPatternSignature <-
    Name -> Kind -> Dec
SigD Name
toFoilPatternT (Kind -> Dec) -> Q Kind -> Q Dec
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
      [t| Foil.Distinct $Q Kind
ntype
          => Foil.Scope $Q Kind
ntype
          -> Map $(Kind -> Q Kind
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> Kind
ConT Name
nameT)) (Foil.Name $Q Kind
ntype)
          -> $(Kind -> Q Kind
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> Cxt -> Kind
PeelConT Name
patternT ((TyVarBndr BndrVis -> Kind) -> [TyVarBndr BndrVis] -> Cxt
forall a b. (a -> b) -> [a] -> [b]
map (Name -> Kind
VarT (Name -> Kind)
-> (TyVarBndr BndrVis -> Name) -> TyVarBndr BndrVis -> Kind
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyVarBndr BndrVis -> Name
forall a. TyVarBndr a -> Name
tvarName) [TyVarBndr BndrVis]
patternTVars)))
          -> (forall l. Foil.DExt $Q Kind
ntype l => $(Kind -> Q Kind
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return (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))) $Q Kind
ntype l -> Map $(Kind -> Q Kind
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> Kind
ConT Name
nameT)) (Foil.Name l) -> $Q Kind
rtype)
          -> $Q Kind
rtype
        |]

  Q () -> Q ()
addModFinalizer (Q () -> Q ()) -> Q () -> Q ()
forall a b. (a -> b) -> a -> b
$ DocLoc -> String -> Q ()
putDoc (Name -> DocLoc
DeclDoc Name
toFoilPatternT) (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 'mkToFoilPattern String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"'. Convert a raw pattern into a scope-safe pattern."

  [Dec] -> Q [Dec]
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return
    [ Dec
toFoilPatternSignature
    , [Con] -> Dec
toFoilPatternBody [Con]
patternCons
    ]
  where
    foilPatternT :: Name
foilPatternT = String -> Name
mkName (String
"Foil" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
nameBase Name
patternT)
    toFoilPatternT :: Name
toFoilPatternT = String -> Name
mkName (String
"toFoil" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
nameBase Name
patternT)

    toFoilPatternBody :: [Con] -> Dec
toFoilPatternBody [Con]
patternCons = Name -> [Clause] -> Dec
FunD Name
toFoilPatternT
      [[Pat] -> Body -> [Dec] -> Clause
Clause [Name -> Pat
VarP Name
scope, 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
        scope :: Name
scope = String -> Name
mkName String
"scope"
        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
conName [] [Pat]
conParamPatterns) (Exp -> Body
NormalB Exp
conMatchBody) []
          where
            conMatchBody :: Exp
conMatchBody = Integer -> Exp -> Exp -> Exp -> [BangType] -> Exp
go Integer
1 (Name -> Exp
VarE Name
scope) (Name -> Exp
VarE Name
env) (Name -> Exp
ConE Name
foilConName) [BangType]
params

            go :: Integer -> Exp -> Exp -> Exp -> [BangType] -> Exp
go Integer
_i Exp
_scope' Exp
env' Exp
p [] = Exp -> Exp -> Exp
AppE (Exp -> Exp -> Exp
AppE (Name -> Exp
VarE Name
cont) Exp
p) Exp
env'
            go Integer
i Exp
scope' 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 -> Exp -> Exp
AppE (Exp -> Exp -> Exp
AppE (Name -> Exp
VarE 'Foil.withFresh) Exp
scope')
                    ([Pat] -> Exp -> Exp
LamE [Name -> Pat
VarP Name
xi']
                      ([Dec] -> Exp -> Exp
LetE [ Pat -> Body -> [Dec] -> Dec
ValD (Name -> Pat
VarP Name
scopei) (Exp -> Body
NormalB (Exp -> Exp -> Exp
AppE (Exp -> Exp -> Exp
AppE (Name -> Exp
VarE 'Foil.extendScope) (Name -> Exp
VarE Name
xi')) Exp
scope')) []
                            , 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 'Map.insert) (Name -> Exp
VarE Name
xi))
                                  (Exp -> Exp -> Exp
AppE (Name -> Exp
VarE 'Foil.nameOf) (Name -> Exp
VarE Name
xi')))
                                  (Maybe Exp -> Exp -> Maybe Exp -> Exp
InfixE (Exp -> Maybe Exp
forall a. a -> Maybe a
Just (Name -> Exp
VarE 'Foil.sink)) (Name -> Exp
VarE '(<$>)) (Exp -> Maybe Exp
forall a. a -> Maybe a
Just Exp
env')))) []]
                        (Integer -> Exp -> Exp -> Exp -> [BangType] -> Exp
go (Integer
iInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
+Integer
1) (Name -> Exp
VarE Name
scopei) (Name -> Exp
VarE Name
envi) (Exp -> Exp -> Exp
AppE Exp
p (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
toFoilPatternT) Exp
scope') Exp
env') (Name -> Exp
VarE Name
xi))
                    ([Pat] -> Exp -> Exp
LamE [Name -> Pat
VarP Name
xi', Name -> Pat
VarP Name
envi]
                      ([Dec] -> Exp -> Exp
LetE [Pat -> Body -> [Dec] -> Dec
ValD (Name -> Pat
VarP Name
scopei) (Exp -> Body
NormalB (Exp -> Exp -> Exp
AppE (Exp -> Exp -> Exp
AppE (Name -> Exp
VarE 'Foil.extendScopePattern) (Name -> Exp
VarE Name
xi')) Exp
scope')) []]
                        (Integer -> Exp -> Exp -> Exp -> [BangType] -> Exp
go (Integer
iInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
+Integer
1) (Name -> Exp
VarE Name
scopei) (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
"'")
                scopei :: Name
scopei = String -> Name
mkName (String
"_scope" 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
scope' 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
scope' 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!"