18
18
--
19
19
-- > import HsBindgen.Hs.AST qualified as Hs
20
20
module HsBindgen.Hs.AST (
21
+ -- * Passes and Annotations
22
+ Pass (.. )
23
+ , Ann
21
24
-- * Information about generated code
22
- Struct (.. )
25
+ , Struct (.. )
23
26
, Newtype (.. )
24
27
-- * Types
25
28
, HsType (.. )
@@ -52,37 +55,65 @@ module HsBindgen.Hs.AST (
52
55
, makeElimStruct
53
56
) where
54
57
55
- import HsBindgen.C.AST qualified as C (MFun (.. ))
56
- import HsBindgen.C.Tc.Macro qualified as C
57
58
import Data.Type.Nat as Nat
59
+ import GHC.Base (Symbol )
58
60
61
+ import HsBindgen.C.AST qualified as C (MFun (.. ))
62
+ import HsBindgen.C.Tc.Macro qualified as C
59
63
import HsBindgen.Imports
60
64
import HsBindgen.NameHint
61
65
import HsBindgen.Hs.AST.Name
62
66
import HsBindgen.Hs.AST.Type
63
67
64
68
import DeBruijn
65
69
70
+ {- ------------------------------------------------------------------------------
71
+ Passes and annotations
72
+ -------------------------------------------------------------------------------}
73
+
74
+ -- | Passes for the Haskell AST phase
75
+ data Pass = Placeholder
76
+
77
+ -- | Symbol-indexed annotations for a given pass
78
+ type family Ann (pass :: Pass ) (s :: Symbol ) where
79
+ Ann Placeholder s = AnnPlaceholder s
80
+
81
+ -- | Symbol-indexed annotations for the 'Placeholder' pass
82
+ type family AnnPlaceholder (s :: Symbol ) where
83
+ AnnPlaceholder s = ()
84
+
85
+ -- Class alias to work around GHC limitation that type family synonym
86
+ -- applications cannot be used in quantified constraints
87
+ class Show (Ann pass s ) => ShowAnn pass s
88
+ instance Show (Ann pass s ) => ShowAnn pass s
89
+
90
+ -- All annotations must have a 'Show' instance (quantified constraint)
91
+ class (forall s . ShowAnn pass s ) => AllAnnShow pass
92
+ instance (forall s . ShowAnn pass s ) => AllAnnShow pass
93
+
66
94
{- ------------------------------------------------------------------------------
67
95
Information about generated code
68
96
-------------------------------------------------------------------------------}
69
97
70
- data Struct (n :: Nat ) = Struct {
71
- structName :: HsName NsTypeConstr
98
+ data Struct (pass :: Pass ) (n :: Nat ) = Struct {
99
+ structAnn :: Ann pass " Struct"
100
+ , structName :: HsName NsTypeConstr
72
101
, structConstr :: HsName NsConstr
73
- , structFields :: Vec n (HsName NsVar , HsType )
102
+ , structFields :: Vec n (Ann pass " StructField " , ( HsName NsVar , HsType ) )
74
103
}
75
104
76
- deriving stock instance Show (Struct n )
105
+ deriving stock instance AllAnnShow pass => Show (Struct pass n )
77
106
78
- data Newtype = Newtype {
79
- newtypeName :: HsName NsTypeConstr
80
- , newtypeConstr :: HsName NsConstr
81
- , newtypeField :: HsName NsVar
82
- , newtypeType :: HsType
107
+ data Newtype (pass :: Pass ) = Newtype {
108
+ newtypeAnn :: Ann pass " Newtype"
109
+ , newtypeName :: HsName NsTypeConstr
110
+ , newtypeConstr :: HsName NsConstr
111
+ , newtypeFieldAnn :: Ann pass " NewtypeField"
112
+ , newtypeField :: HsName NsVar
113
+ , newtypeType :: HsType
83
114
}
84
115
85
- deriving stock instance Show Newtype
116
+ deriving stock instance AllAnnShow pass => Show ( Newtype pass )
86
117
87
118
{- ------------------------------------------------------------------------------
88
119
Variable binding
@@ -106,28 +137,31 @@ data Ap pure xs ctx = Ap (pure ctx) [xs ctx]
106
137
-------------------------------------------------------------------------------}
107
138
108
139
-- | Top-level declaration
109
- type Decl :: Star
110
- data Decl where
111
- DeclData :: SNatI n => Struct n -> Decl
112
- DeclEmpty :: HsName NsTypeConstr -> Decl
113
- DeclNewtype :: Newtype -> Decl
114
- DeclInstance :: InstanceDecl -> Decl
115
- DeclNewtypeInstance :: TypeClass -> HsName NsTypeConstr -> Decl
116
- DeclVar :: VarDecl -> Decl
140
+ type Decl :: Pass -> Star
141
+ data Decl pass where
142
+ DeclData :: SNatI n => Struct pass n -> Decl pass
143
+ DeclEmpty :: HsName NsTypeConstr -> Decl pass
144
+ DeclNewtype :: Newtype pass -> Decl pass
145
+ DeclInstance :: InstanceDecl pass -> Decl pass
146
+ DeclNewtypeInstance :: TypeClass -> HsName NsTypeConstr -> Decl pass
147
+ DeclVar :: VarDecl -> Decl pass
117
148
118
- deriving instance Show Decl
149
+ deriving instance AllAnnShow pass => Show ( Decl pass )
119
150
120
151
-- | Class instance names
121
152
data TypeClass =
122
153
Storable
123
154
deriving stock (Show )
124
155
125
156
-- | Class instance declaration
126
- type InstanceDecl :: Star
127
- data InstanceDecl where
128
- InstanceStorable :: Struct n -> StorableInstance -> InstanceDecl
157
+ type InstanceDecl :: Pass -> Star
158
+ data InstanceDecl pass where
159
+ InstanceStorable ::
160
+ Struct pass n
161
+ -> StorableInstance pass
162
+ -> InstanceDecl pass
129
163
130
- deriving instance Show InstanceDecl
164
+ deriving instance AllAnnShow pass => Show ( InstanceDecl pass )
131
165
132
166
-- | Variable or function declaration.
133
167
type VarDecl :: Star
@@ -214,15 +248,16 @@ deriving stock instance Show VarDeclRHSAppHead
214
248
-- Currently this models storable instances for structs /only/.
215
249
--
216
250
-- <https://hackage.haskell.org/package/base/docs/Foreign-Storable.html#t:Storable>
217
- type StorableInstance :: Star
218
- data StorableInstance = StorableInstance
251
+ type StorableInstance :: Pass -> Star
252
+ data StorableInstance pass = StorableInstance
219
253
{ storableSizeOf :: Int
220
254
, storableAlignment :: Int
221
- , storablePeek :: Lambda (Ap StructCon PeekByteOff ) EmptyCtx
222
- , storablePoke :: Lambda (Lambda (ElimStruct (Seq PokeByteOff ))) EmptyCtx
255
+ , storablePeek :: Lambda (Ap (StructCon pass ) PeekByteOff ) EmptyCtx
256
+ , storablePoke ::
257
+ Lambda (Lambda (ElimStruct pass (Seq PokeByteOff ))) EmptyCtx
223
258
}
224
259
225
- deriving instance Show StorableInstance
260
+ deriving instance AllAnnShow pass => Show ( StorableInstance pass )
226
261
227
262
-- | Call to 'peekByteOff'
228
263
--
@@ -252,28 +287,48 @@ newtype Seq t ctx = Seq [t ctx]
252
287
Structs
253
288
-------------------------------------------------------------------------------}
254
289
255
- type StructCon :: Ctx -> Star
256
- data StructCon ctx where
257
- StructCon :: Struct n -> StructCon ctx
290
+ type StructCon :: Pass -> Ctx -> Star
291
+ data StructCon pass ctx where
292
+ StructCon :: Struct pass n -> StructCon pass ctx
258
293
259
- deriving instance Show (StructCon ctx )
294
+ deriving instance AllAnnShow pass => Show (StructCon pass ctx )
260
295
261
296
-- | Case split for a struct
262
- type ElimStruct :: (Ctx -> Star ) -> (Ctx -> Star )
263
- data ElimStruct t ctx where
264
- ElimStruct :: Idx ctx -> Struct n -> Add n ctx ctx' -> t ctx' -> ElimStruct t ctx
265
-
266
- deriving instance (forall ctx' . Show (t ctx' )) => Show (ElimStruct t ctx )
297
+ type ElimStruct :: Pass -> (Ctx -> Star ) -> (Ctx -> Star )
298
+ data ElimStruct pass t ctx where
299
+ ElimStruct ::
300
+ Idx ctx
301
+ -> Struct pass n
302
+ -> Add n ctx ctx'
303
+ -> t ctx'
304
+ -> ElimStruct pass t ctx
305
+
306
+ deriving instance
307
+ (AllAnnShow pass , forall ctx' . Show (t ctx' ))
308
+ => Show (ElimStruct pass t ctx )
267
309
268
310
-- | Create 'ElimStruct' using kind-of HOAS interface.
269
311
--
270
- makeElimStruct :: forall n ctx t . SNatI n => Idx ctx -> Struct n -> (forall ctx' . Wk ctx ctx' -> Vec n (Idx ctx' ) -> t ctx' ) -> ElimStruct t ctx
312
+ makeElimStruct :: forall n ctx t pass .
313
+ SNatI n
314
+ => Idx ctx
315
+ -> Struct pass n
316
+ -> (forall ctx' . Wk ctx ctx' -> Vec n (Idx ctx' ) -> t ctx' )
317
+ -> ElimStruct pass t ctx
271
318
makeElimStruct s struct kont = makeElimStruct' (snat :: SNat n ) $ \ add wk xs ->
272
319
ElimStruct s struct add (kont wk xs)
273
320
274
321
--
275
322
-- TODO: use Data.Type.Nat.induction instead of explicit recursion.
276
323
-- TODO: verify that we bind fields in right order.
277
- makeElimStruct' :: forall m ctx t . SNat m -> (forall ctx' . Add m ctx ctx' -> Wk ctx ctx' -> Vec m (Idx ctx' ) -> ElimStruct t ctx ) -> ElimStruct t ctx
324
+ makeElimStruct' :: forall m ctx t pass .
325
+ SNat m
326
+ -> ( forall ctx' .
327
+ Add m ctx ctx'
328
+ -> Wk ctx ctx'
329
+ -> Vec m (Idx ctx' )
330
+ -> ElimStruct pass t ctx
331
+ )
332
+ -> ElimStruct pass t ctx
278
333
makeElimStruct' Nat. SZ kont = kont AZ IdWk VNil
279
334
makeElimStruct' (Nat. SS' n) kont = makeElimStruct' n $ \ add wk xs -> kont (AS add) (SkipWk wk) (IZ ::: fmap IS xs)
0 commit comments