... | ... | @@ -33,12 +33,18 @@ In general, a TTG-idiom data type has |
|
|
|
|
|
For example:
|
|
|
|
|
|
|
|
|
```
|
|
|
dataExp x
|
|
|
=Var(XVar x)(IdP x)|Lam(XLam x)(IdP x)(Exp x)|App(XApp x)(Exp x)(Exp x)|New(XNew x)typefamilyXVar x
|
|
|
typefamilyXLam x
|
|
|
typefamilyXApp x
|
|
|
typefamilyXNew x
|
|
|
data Exp x
|
|
|
= Var (XVar x) (IdP x)
|
|
|
| Lam (XLam x) (IdP x) (Exp x)
|
|
|
| App (XApp x) (Exp x) (Exp x)
|
|
|
| New (XNew x)
|
|
|
|
|
|
type family XVar x
|
|
|
type family XLam x
|
|
|
type family XApp x
|
|
|
type family XNew x
|
|
|
```
|
|
|
|
|
|
|
... | ... | @@ -57,8 +63,10 @@ The design of TTG [HsSyn](implementing-trees-that-grow/hs-syn) follows these pri |
|
|
1. Note, however, that the type of a payload field of a constructor may vary with phase. For example, in `Lam` above, the first payload field has type `Id x`, and that may vary with phase:
|
|
|
|
|
|
```
|
|
|
typefamilyIdP x
|
|
|
typeinstanceIdPGhcPs=RdrNametypeinstanceIdPGhcRn=NametypeinstanceIdPGhcTc=Id
|
|
|
type family IdP x
|
|
|
type instance IdP GhcPs = RdrName
|
|
|
type instance IdP GhcRn = Name
|
|
|
type instance IdP GhcTc = Id
|
|
|
```
|
|
|
|
|
|
But it is still a payload field, because every instantiation of `Exp` has a lambda with a binder; albeit the type of that binder field varies. This happens in [HsSyn](implementing-trees-that-grow/hs-syn): for example, the type of the common (payload) field of the common constructor `HsVar`of `HsExpr x` is `IdP x` where `IdP` is a type family and `x` the phase descriptor.
|
... | ... | @@ -67,61 +75,163 @@ The design of TTG [HsSyn](implementing-trees-that-grow/hs-syn) follows these pri |
|
|
|
|
|
1. The instantiation of TTG [HsSyn](implementing-trees-that-grow/hs-syn), for a particular phase, should result in a tree that has no redundant fields and constructors.
|
|
|
|
|
|
>
|
|
|
>
|
|
|
> For example, the `HsExpr GhsPs` expressions of AST GhcPs should not have the constructor `HsUnboundVar` of the post-renaming phases, or its `HsMultiIf` constructor should also not have an unused field (of the type `Type`) to store the related type produced in the typechecking phase.
|
|
|
>
|
|
|
>
|
|
|
|
|
|
>
|
|
|
>
|
|
|
> As a result, the instantiated TTG [HsSyn](implementing-trees-that-grow/hs-syn) should not depend on the code from the other phases. Hence, the base (uninstantiated) TTG [HsSyn](implementing-trees-that-grow/hs-syn) should not depend on any GHC/TH/HSE-specific code.
|
|
|
>
|
|
|
>
|
|
|
|
|
|
>
|
|
|
>
|
|
|
> For example, if `HsExpr GhsPs` expressions of AST GhcPs had the constructor `HsUnboundVar` then it had to depend on the code defining `UnboundVar` (a field of `HsUnboundVar`) in the renaming phase, or if its constructor `MultiIf` had a field of type `Type` then it had to depend on the code defining `Type` in the typechecking phase.
|
|
|
>
|
|
|
>
|
|
|
|
|
|
## Example
|
|
|
|
|
|
|
|
|
|
|
|
Consider the following three simple datatypes `ExpPs`, `ExpRn`, and `ExpTc` representing correspondingly expressions in a parsing, renaming and typechecking phase:
|
|
|
|
|
|
|
|
|
```
|
|
|
moduleParsingwhere-- the definition of RdrName-- ...dataExpPs=VarRdrName|LamRdrNameExpPs|AppExpPsExpPs
|
|
|
module Parsing where
|
|
|
|
|
|
-- the definition of RdrName
|
|
|
-- ...
|
|
|
|
|
|
data ExpPs
|
|
|
= Var RdrName
|
|
|
| Lam RdrName ExpPs
|
|
|
| App ExpPs ExpPs
|
|
|
```
|
|
|
|
|
|
```
|
|
|
moduleRenamingwhere-- the definition of `Name` and `UnboundVar`-- ...dataExpRn=VarName|LamNameExpRn|AppExpRnExpRn|UVarUnboundVar
|
|
|
module Renaming where
|
|
|
|
|
|
-- the definition of `Name` and `UnboundVar`
|
|
|
-- ...
|
|
|
|
|
|
data ExpRn
|
|
|
= Var Name
|
|
|
| Lam Name ExpRn
|
|
|
| App ExpRn ExpRn
|
|
|
| UVar UnboundVar
|
|
|
```
|
|
|
|
|
|
```
|
|
|
moduleTypecheckingwhere-- the definition of `Id`, `UnboundVar`, and `Type`-- ...dataExpTc=VarId|LamIdExpTc|AppTypeExpTcExpTc|UVarUnboundVar
|
|
|
module Typechecking where
|
|
|
|
|
|
-- the definition of `Id`, `UnboundVar`, and `Type`
|
|
|
-- ...
|
|
|
|
|
|
data ExpTc
|
|
|
= Var Id
|
|
|
| Lam Id ExpTc
|
|
|
| App Type ExpTc ExpTc
|
|
|
| UVar UnboundVar
|
|
|
```
|
|
|
|
|
|
|
|
|
Based on the TTG idiom, we will have a base declaration such as the following.
|
|
|
|
|
|
|
|
|
```
|
|
|
{-# LANGUAGE TypeFamilies , EmptyCase #-}moduleASTwheredataExp x
|
|
|
=Var(XVar x)(XId x)|Abs(XAbs x)(XId x)(Exp x)|App(XApp x)(Exp x)(Exp x)|New(XNew x)typefamilyXVar x
|
|
|
typefamilyXAbs x
|
|
|
typefamilyXApp x
|
|
|
typefamilyXNew x
|
|
|
{-# LANGUAGE TypeFamilies , EmptyCase #-}
|
|
|
module AST where
|
|
|
|
|
|
data Exp x
|
|
|
= Var (XVar x) (XId x)
|
|
|
| Abs (XAbs x) (XId x) (Exp x)
|
|
|
| App (XApp x) (Exp x) (Exp x)
|
|
|
| New (XNew x)
|
|
|
|
|
|
type family XVar x
|
|
|
type family XAbs x
|
|
|
type family XApp x
|
|
|
type family XNew x
|
|
|
|
|
|
typefamilyXId x
|
|
|
type family XId x
|
|
|
|
|
|
dataNoExt=NoExt-- no field extensiondataNoNewCon-- no constructor extensionnoNewCon::NoNewCon-> a
|
|
|
noNewCon x =case x of{}
|
|
|
data NoExt = NoExt -- no field extension
|
|
|
|
|
|
data NoNewCon -- no constructor extension
|
|
|
|
|
|
noNewCon :: NoNewCon -> a
|
|
|
noNewCon x = case x of {}
|
|
|
```
|
|
|
|
|
|
|
|
|
and the following three instantiations:
|
|
|
|
|
|
|
|
|
```
|
|
|
{-# LANGUAGE TypeFamilies #-}moduleParsingwhereimportASTdataRdrName-- = ...dataPstypeExpPs=ExpPstypeinstanceXVarPs=NoExttypeinstanceXAbsPs=NoExttypeinstanceXAppPs=NoExttypeinstanceXNewPs=NoNewContypeinstanceXIdPs=RdrName
|
|
|
{-# LANGUAGE TypeFamilies #-}
|
|
|
module Parsing where
|
|
|
|
|
|
import AST
|
|
|
|
|
|
data RdrName -- = ...
|
|
|
|
|
|
data Ps
|
|
|
|
|
|
type ExpPs = Exp Ps
|
|
|
|
|
|
type instance XVar Ps = NoExt
|
|
|
type instance XAbs Ps = NoExt
|
|
|
type instance XApp Ps = NoExt
|
|
|
type instance XNew Ps = NoNewCon
|
|
|
|
|
|
type instance XId Ps = RdrName
|
|
|
```
|
|
|
|
|
|
```
|
|
|
{-# LANGUAGE TypeFamilies #-}moduleRenamingwhereimportASTdataName-- = ...dataUnboundVar-- = ...dataRntypeExpRn=ExpRntypeinstanceXVarRn=NoExttypeinstanceXAbsRn=NoExttypeinstanceXAppRn=NoExttypeinstanceXNewRn=UnboundVartypeinstanceXIdRn=Name
|
|
|
{-# LANGUAGE TypeFamilies #-}
|
|
|
module Renaming where
|
|
|
|
|
|
import AST
|
|
|
|
|
|
data Name -- = ...
|
|
|
data UnboundVar -- = ...
|
|
|
|
|
|
data Rn
|
|
|
|
|
|
type ExpRn = Exp Rn
|
|
|
|
|
|
type instance XVar Rn = NoExt
|
|
|
type instance XAbs Rn = NoExt
|
|
|
type instance XApp Rn = NoExt
|
|
|
type instance XNew Rn = UnboundVar
|
|
|
|
|
|
type instance XId Rn = Name
|
|
|
```
|
|
|
|
|
|
```
|
|
|
{-# LANGUAGE TypeFamilies #-}moduleTypecheckingwhereimportASTdataId-- = ...dataUnboundVar-- = ...dataType-- = ...dataTctypeExpTc=ExpTctypeinstanceXVarTc=NoExttypeinstanceXAbsTc=NoExttypeinstanceXAppTc=TypetypeinstanceXNewTc=UnboundVartypeinstanceXIdTc=Id
|
|
|
{-# LANGUAGE TypeFamilies #-}
|
|
|
module Typechecking where
|
|
|
|
|
|
import AST
|
|
|
|
|
|
data Id -- = ...
|
|
|
data UnboundVar -- = ...
|
|
|
data Type -- = ...
|
|
|
|
|
|
data Tc
|
|
|
|
|
|
type ExpTc = Exp Tc
|
|
|
|
|
|
type instance XVar Tc = NoExt
|
|
|
type instance XAbs Tc = NoExt
|
|
|
type instance XApp Tc = Type
|
|
|
type instance XNew Tc = UnboundVar
|
|
|
|
|
|
type instance XId Tc = Id
|
|
|
```
|
|
|
|
|
|
|
... | ... | |