3 | import Data.List.Quantifiers
10 | interface Expression a where
13 | interface Statement a where
16 | interface Specification a where
19 | interface Declaration a where
22 | interface GoType a where
25 | record Comment where
26 | constructor MkComment
30 | record CommentGroup where
31 | constructor MkCommentGroup
32 | comments : List1 Comment
38 | record Field t {auto 0 tt : GoType t} where
40 | doc : Maybe CommentGroup
41 | names : List Identifier
43 | tag : Maybe BasicLiteral
44 | comment : Maybe CommentGroup
47 | data FieldList : (ts : List Type) -> Type where
49 | (::) : {auto tt : GoType t} -> Field t -> FieldList ts -> FieldList (t::ts)
52 | record TypeIdentifier where
53 | constructor MkTypeIdentifier
54 | package : Maybe Identifier
58 | implementation GoType TypeIdentifier where
61 | record ArrayType l e where
62 | constructor MkArrayType
67 | implementation Expression l => GoType e => GoType (ArrayType l e) where
70 | record StructType ts where
71 | constructor MkStructType
72 | fields : FieldList ts
75 | implementation GoType (StructType ts) where
78 | record FunctionType ts ps rs where
79 | constructor MkFunctionType
80 | typeParams : FieldList ts
81 | params : FieldList ps
82 | results : FieldList rs
85 | implementation GoType (FunctionType ts ps rs) where
88 | record InterfaceType ts where
89 | constructor MkInterfaceType
90 | methods : FieldList ts
93 | implementation GoType (InterfaceType ts) where
96 | record MapType k v where
97 | constructor MkMapType
102 | implementation GoType k => GoType v => GoType (MapType k v) where
111 | record ChanType e where
112 | constructor MkChanType
113 | direction : ChanDirection
117 | implementation GoType e => GoType (ChanType e) where
120 | record BadStatement where
121 | constructor MkBadStatement
124 | implementation Statement BadStatement where
127 | record DeclarationStatement t where
128 | constructor MkDeclarationStatement
132 | implementation Declaration t => Statement (DeclarationStatement t) where
135 | record EmptyStatement where
136 | constructor MkEmptyStatement
140 | implementation Statement EmptyStatement where
143 | record LabeledStatement t where
144 | constructor MkLabeledStatement
149 | implementation Statement t => Statement (LabeledStatement t) where
152 | record ExpressionStatement e where
153 | constructor MkExpressionStatement
154 | doc : Maybe CommentGroup
156 | comment : Maybe CommentGroup
159 | implementation Expression e => Statement (ExpressionStatement e) where
162 | record SendStatement c v where
163 | constructor MkSendStatement
168 | implementation Expression c => Expression v => Expression (SendStatement c v) where
171 | data IncOrDec : Operator -> Type where
172 | Inc : IncOrDec MkInc
173 | Dec : IncOrDec MkDec
176 | implementation Show (IncOrDec MkInc) where
177 | show _ = show MkInc
180 | implementation Show (IncOrDec MkDec) where
181 | show _ = show MkDec
184 | record IncDecStatement e o where
185 | constructor MkIncDecStatement
190 | implementation Expression e => Statement (IncDecStatement e o) where
193 | record AssignmentStatement ls rs where
194 | constructor MkAssignmentStatement
195 | doc : Maybe CommentGroup
199 | comment : Maybe CommentGroup
202 | implementation All Expression ls => All Expression rs => NonEmpty ls => NonEmpty rs => Statement (AssignmentStatement ls rs) where
206 | record Ellipsis t where
207 | constructor MkEllipsis
208 | elementType : Maybe t
211 | implementation Expression t => Expression (Ellipsis t) where
215 | record CallExpression f as e where
216 | constructor MkCallExpression
219 | ellipsis : Maybe $
Ellipsis e
222 | implementation Expression f => All Expression as => Expression e => Expression (CallExpression f as e) where
225 | record GoStatement f as e where
226 | constructor MkGoStatement
227 | call : CallExpression f as e
230 | implementation Expression f => All Expression as => Expression e => Statement (GoStatement f as e) where
233 | record DeferStatement f as e where
234 | constructor MkDeferStatement
235 | call : CallExpression f as e
239 | implementation Expression f => All Expression as => Expression e => Statement (DeferStatement f as e) where
242 | record ReturnStatement rs where
243 | constructor MkReturnStatement
244 | doc : Maybe CommentGroup
248 | implementation All Expression rs => Statement (ReturnStatement rs) where
251 | data BranchStatementToken : Keyword -> Type where
252 | IsBreak : BranchStatementToken MkBreak
253 | IsContinue : BranchStatementToken MkContinue
254 | IsGoto : BranchStatementToken MkBreak
255 | IsFallthrough : BranchStatementToken MkFallthrough
258 | record BranchStatement (kw : Keyword) where
259 | constructor MkBranchStatement
260 | token : BranchStatementToken kw
261 | label : Maybe Identifier
264 | implementation Statement (BranchStatement kw) where
267 | record BlockStatement sts where
268 | constructor MkBlockStatement
269 | statements : HList sts
272 | implementation All Statement sts => Statement (BlockStatement sts) where
275 | record IfStatement i c sts e where
276 | constructor MkIfStatement
279 | body : BlockStatement sts
280 | elseBranch : Maybe e
283 | implementation Statement i => Expression c => All Statement sts => Statement (IfStatement i c sts e) where
286 | record CaseClause es sts where
287 | constructor MkCaseClause
292 | implementation All Expression es => NonEmpty sts => All Statement sts => Statement (CaseClause es sts) where
295 | data IsCaseClause : Type -> Type where
296 | ItIsCaseClause : All Expression es => NonEmpty sts => All Statement sts => IsCaseClause (CaseClause es sts)
299 | record SwitchStatement i e sts where
300 | constructor MkSwitchStatement
303 | body : BlockStatement sts
306 | implementation Statement i => Expression e => All Statement sts => All IsCaseClause sts => Statement (SwitchStatement i e sts) where
309 | record TypeSwitchStatement i a sts where
310 | constructor MkTypeSwitchStatement
313 | body : BlockStatement sts
316 | implementation Statement i => Statement a => All Statement sts => Statement (TypeSwitchStatement i a sts) where
319 | data IsSendStatement : Type -> Type where
320 | ItIsSendStatement : Expression c => Expression v => IsSendStatement (SendStatement c v)
323 | record CommClause s sts where
324 | constructor MkCommClause
329 | implementation IsSendStatement s => All Statement sts => Statement (CommClause s sts) where
332 | record SelectStatement sts where
333 | constructor MkSelectStatement
334 | body : BlockStatement sts
337 | implementation All Statement sts => Statement (SelectStatement sts) where
340 | record ForStatement i c p sts where
341 | constructor MkForStatement
343 | condition : Maybe c
345 | body : BlockStatement sts
348 | implementation Statement i => Expression c => Statement p => All Statement sts => Statement (ForStatement i c p sts) where
351 | data AssignOrDefine : Operator -> Type where
352 | ItIsAssign : AssignOrDefine MkAssign
353 | ItIsDefine : AssignOrDefine MkDefine
356 | implementation Show (AssignOrDefine MkAssign) where
357 | show _ = show MkAssign
360 | implementation Show (AssignOrDefine MkDefine) where
361 | show _ = show MkDefine
364 | record KeyValueRangeStatement k v a e sts where
365 | constructor MkKeyValueRangeStatement
368 | token : AssignOrDefine a
370 | body : BlockStatement sts
373 | implementation Expression k => Expression v => AssignOrDefine a => Expression e => All Statement sts => Statement (KeyValueRangeStatement k v a e sts) where
376 | record ValueRangeStatement v a e sts where
377 | constructor MkValueRangeStatement
379 | token : AssignOrDefine a
381 | body : BlockStatement sts
384 | implementation Expression v => AssignOrDefine a => Expression e => All Statement sts => Statement (ValueRangeStatement v a e sts) where
387 | record RangeStatement e sts where
388 | constructor MkRangeStatement
390 | body : BlockStatement sts
393 | implementation Expression e => All Statement sts => Statement (RangeStatement e sts) where
398 | record BadExpression where
399 | constructor MkBadExpression
402 | implementation Expression BadExpression where
405 | record Identifier where
406 | constructor MkIdentifier
411 | implementation Expression Identifier where
414 | record BasicLiteral where
415 | constructor MkBasicLiteral
416 | kind : Token.Literal
420 | implementation Expression BasicLiteral where
423 | record FunctionLiteral ts ps rs sts where
424 | constructor MkFunctionLiteral
425 | type : FunctionType ts ps rs
426 | body : BlockStatement sts
429 | implementation All Statement sts => GoType (FunctionType ts ps rs) => Expression (FunctionLiteral ts ps rs sts) where
432 | record CompositLiteral t es where
433 | constructor MkCompositLiteral
435 | expressions : HList es
438 | implementation GoType t => All Expression es => Expression (CompositLiteral t es) where
441 | record ParenExpression e where
442 | constructor MkParenExpression
446 | implementation Expression e => Expression (ParenExpression e) where
449 | record SelectorExpression e where
450 | constructor MkSelectorExpression
452 | selector : Identifier
455 | implementation Expression e => Expression (SelectorExpression e) where
458 | record CastExpression t e where
459 | constructor MkCastExpression
464 | implementation GoType t => Expression e => Expression (CastExpression t e) where
467 | record MakeExpression t es where
468 | constructor MkMakeExpression
470 | expressions : HList es
473 | implementation GoType t => All Expression es => Expression (MakeExpression t es) where
476 | record IndexExpression e i where
477 | constructor MkIndexExpression
482 | implementation Expression e => Expression i => Expression (IndexExpression e i) where
485 | record IndexListExpression e is where
486 | constructor MkIndexListExpression
491 | implementation Expression e => All Expression is => Expression (IndexListExpression e is) where
494 | record SliceExpression e l h m where
495 | constructor MkSliceExpression
502 | implementation Expression e => Expression l => Expression h => Expression m => Expression (SliceExpression e l h m) where
505 | record TypeAssertExpression e t where
506 | constructor MkTypeAssertExpression
511 | implementation Expression e => GoType t => Expression (TypeAssertExpression e t) where
514 | record StarExpression e where
515 | constructor MkStarExpression
519 | implementation Expression e => Expression (StarExpression e) where
522 | record UnaryExpression e where
523 | constructor MkUnaryExpression
524 | operator : Operator
528 | implementation Expression e => Expression (UnaryExpression e) where
531 | record BinaryExpression x y where
532 | constructor MkBinaryExpression
534 | operator : Operator
538 | implementation Expression x => Expression y => Expression (BinaryExpression x y) where
541 | record KeyValueExpression k v where
542 | constructor MkKeyValueExpression
547 | implementation Expression k => Expression v => Expression (KeyValueExpression k v) where
552 | record ImportSpec where
553 | constructor MkImportSpec
554 | doc : Maybe CommentGroup
555 | name : Maybe Identifier
556 | path : BasicLiteral
557 | comment : Maybe CommentGroup
560 | implementation Specification ImportSpec where
563 | record ValueSpec t es where
564 | constructor MkValueSpec
565 | doc : Maybe CommentGroup
566 | names : List1 Identifier
569 | comment : Maybe CommentGroup
572 | implementation GoType t => All Expression es => Specification (ValueSpec t es) where
575 | record TypeSpec ts t where
576 | constructor MkTypeSpec
577 | doc : Maybe CommentGroup
579 | typeParams : FieldList ts
581 | comment : Maybe CommentGroup
584 | implementation GoType t => Specification (TypeSpec ts t) where
589 | record BadDeclaration where
590 | constructor MkBadDeclaration
593 | implementation Declaration BadDeclaration where
596 | data GenericDeclarationToken : Keyword -> Type where
597 | Import : GenericDeclarationToken MkImport
598 | Const : GenericDeclarationToken MkConst
599 | Type' : GenericDeclarationToken MkType
600 | Var : GenericDeclarationToken MkVar
603 | implementation Show (GenericDeclarationToken MkImport) where
604 | show _ = show MkImport
607 | implementation Show (GenericDeclarationToken MkConst) where
608 | show _ = show MkConst
611 | implementation Show (GenericDeclarationToken MkType) where
612 | show _ = show MkType
615 | implementation Show (GenericDeclarationToken MkVar) where
616 | show _ = show MkVar
619 | record GenericDeclaration (t : Keyword) xs where
620 | constructor MkGenericDeclaration
621 | doc : Maybe CommentGroup
622 | token : GenericDeclarationToken t
626 | implementation NonEmpty xs => All Specification xs => Declaration (GenericDeclaration t xs) where
629 | record FuncDeclaration rcs ts ps rs sts where
630 | constructor MkFuncDeclaration
631 | doc : Maybe CommentGroup
632 | reciever : FieldList rcs
634 | type : FunctionType ts ps rs
635 | body : BlockStatement sts
638 | implementation All Statement sts => Declaration (FuncDeclaration rcs ts ps rs sts) where
641 | record File ds {auto 0 dsd : All Declaration ds} where
643 | doc : Maybe CommentGroup
645 | packageName : Identifier
647 | imports : List ImportSpec
648 | unresolved : List Identifier
649 | comments : List CommentGroup
652 | data BadType = MkBadType
655 | implementation GoType BadType where