0 | module Go.AST.Printer

  2 | import Control.Monad.Either

  3 | import Data.List

  4 | import Data.List.All

  5 | import Data.List1

  6 | import Data.List.Quantifiers

  7 | import Go.AST as Go

  8 | import Go.Token

  9 | import System.File

 11 | %default total

 12 | %hide Prelude.print

 14 | public export

 15 | data PrintError

 16 |   = PrintFileError FileError

 19 | implementation Show PrintError where

 20 |   show = \case

 21 |     PrintFileError e => show e

 23 | public export

 24 | PrinterMonad : (Type -> Type) -> Type -> Type

 25 | PrinterMonad io a = EitherT PrintError io a

 27 | public export

 28 | data Indent = MkIndent Nat

 31 | zeroIndent : Indent

 32 | zeroIndent = MkIndent 0

 35 | increaseIndent : Indent -> Indent

 36 | increaseIndent (MkIndent i) = MkIndent (i+1)

 38 | public export

 39 | interface Printer a where

 40 |   constructor MkPrinter

 41 |   print : HasIO io => File -> {auto indent : Indent} -> a -> PrinterMonad io ()

 43 | pPutStr : HasIO io => {auto file : File} -> String -> PrinterMonad io ()

 44 | pPutStr {file} str = MkEitherT $ fPutStr file str >>= \case

 45 |   Left e => pure $ Left $ PrintFileError e

 46 |   Right a => pure $ Right a

 48 | printNewLine : HasIO io => {auto file : File} -> PrinterMonad io ()

 49 | printNewLine = pPutStr "\n"

 51 | printIndent : HasIO io => {auto file : File} -> {auto indent : Indent} -> PrinterMonad io ()

 52 | printIndent {indent = (MkIndent i)} =

 53 |   let str = concat $ replicate i "\t"

 54 |   in pPutStr str

 56 | printComments : HasIO io => {auto file : File} -> {auto indent : Indent} -> List Comment -> PrinterMonad io ()

 57 | printComments [] = pure ()

 58 | printComments [x] = do

 59 |     pPutStr "//"

 60 |     pPutStr x.text

 61 | printComments (x::xs) = do

 62 |     pPutStr "//"

 63 |     pPutStr x.text

 64 |     printNewLine

 65 |     printIndent

 66 |     printComments xs

 71 | implementation Printer BadExpression where

 72 |   print file be = pPutStr "/* Evaluated BadExpression */"

 75 | implementation Printer Identifier where

 76 |   print file i = pPutStr i.name

 79 | implementation Printer BasicLiteral where

 80 |   print file bl =

 81 |     let value = case bl.kind of

 82 |                   MkString => "\"\{bl.value}\""

 83 |                   MkChar => "'\{bl.value}'"

 84 |                   _ => bl.value

 85 |     in pPutStr value

 88 | implementation Expression (CompositLiteral t es) => Printer t => All Printer es => Printer (CompositLiteral t es) where

 89 |   print file cl = do

 90 |       case cl.type of

 91 |         Nothing => pure ()

 92 |         Just t => print file t

 93 |       case cl.expressions of

 94 |         x1::x2::x3::xs => do

 95 |           pPutStr "{"

 96 |           multiLine cl.expressions

 97 |           printNewLine

 98 |           printIndent

 99 |           pPutStr "}"

100 |         _ => do

101 |           pPutStr "{"

102 |           singleLine cl.expressions

103 |           pPutStr "}"

104 |     where

105 |       singleLine : {0 ts : List Type} -> {auto ps : All Printer ts} -> HList ts -> PrinterMonad io ()

106 |       singleLine [] = pure ()

107 |       singleLine {ps = [p]} [x] = print file x

108 |       singleLine {ps = (p::ps)} (x::xs) = do

109 |         print file x

110 |         pPutStr ", "

111 |         singleLine xs

113 |       inci : Indent

114 |       inci = increaseIndent indent

116 |       multiLine : {0 ts : List Type} -> {auto ps : All Printer ts} -> HList ts -> PrinterMonad io ()

117 |       multiLine [] = pure ()

118 |       multiLine {ps = [p]} [x] = do

119 |         printNewLine

120 |         printIndent {indent = inci}

121 |         print {indent = inci} file x

122 |         pPutStr ","

123 |       multiLine {ps = (p::ps)} (x::xs) = do

124 |         printNewLine

125 |         printIndent {indent = inci}

126 |         print {indent = inci} file x

127 |         pPutStr ","

128 |         multiLine xs

131 | implementation Expression (FunctionLiteral ts ps rs sts) => Printer (FunctionType ts ps rs) => Printer (BlockStatement sts) => Printer (FunctionLiteral ts ps rs sts) where

132 |   print file fl = do

133 |     print file fl.type

134 |     pPutStr " "

135 |     print file fl.body

138 | implementation Expression (CallExpression f as e) => Printer f => All Printer as => Printer (CallExpression f as e) where

139 |   print file ce = do

140 |       print file ce.function

141 |       pPutStr "("

142 |       many ce.args

143 |       pPutStr ")"

144 |     where

145 |       many : { 0 ts : List Type } -> {auto ps : All Printer ts} -> HList ts -> PrinterMonad io ()

146 |       many [] = pure ()

147 |       many {ps = [p]} [x] = print file x

148 |       many {ps = [p1,p2]} [x,y] = do

149 |         print file x

150 |         pPutStr ", "

151 |         print file y

152 |       many {ps = (p::ps)} (x::xs) = do

153 |         print file x

154 |         pPutStr ", "

155 |         many xs

158 | implementation Expression (ParenExpression e) => Printer e => Printer (ParenExpression e) where

159 |   print file pe = do

160 |     pPutStr "("

161 |     print file pe.expression

162 |     pPutStr ")"

165 | implementation Expression (CastExpression t e) => Printer t => Printer e => Printer (CastExpression t e) where

166 |   print file ce = do

167 |     print file ce.type

168 |     pPutStr "("

169 |     print file ce.expression

170 |     pPutStr ")"

173 | implementation Expression (TypeAssertExpression e t) => Printer e => Printer t => Printer (TypeAssertExpression e t) where

174 |   print file tae = do

175 |     print file tae.expression

176 |     pPutStr ".("

177 |     print file tae.type

178 |     pPutStr ")"

181 | implementation Expression (MakeExpression t es) => Printer t => All Printer es => Printer (MakeExpression t es) where

182 |   print file me = do

183 |       pPutStr "make("

184 |       print file me.type

185 |       many me.expressions

186 |       pPutStr ")"

187 |     where

188 |       many : { 0 ts : List Type } -> {auto ps : All Printer ts} -> HList ts -> PrinterMonad io ()

189 |       many [] = pure ()

190 |       many {ps = [p]} [x] = do

191 |         pPutStr ", "

192 |         print file x

193 |       many {ps = (p::ps)} (x::xs) = do

194 |         pPutStr ", "

195 |         print file x

196 |         many xs

199 | implementation Expression (SelectorExpression e) => Printer e => Printer (SelectorExpression e) where

200 |   print file se = do

201 |     print file se.expression

202 |     pPutStr "."

203 |     print file se.selector

206 | implementation Expression (IndexExpression e i) => Printer e => Printer i => Printer (IndexExpression e i) where

207 |   print file ie = do

208 |     print file ie.expression

209 |     pPutStr "["

210 |     print file ie.index

211 |     pPutStr "]"

214 | implementation Expression (SliceExpression e l h m) => Printer e => Printer l => Printer h => Printer m => Printer (SliceExpression e l h m) where

215 |   print file se = do

216 |     print file se.expression

217 |     pPutStr "["

218 |     case se.low of

219 |       Nothing => pPutStr ":"

220 |       Just l => do

221 |         print file l

222 |         pPutStr ":"

223 |     case se.high of

224 |       Nothing => pure ()

225 |       Just h => print file h

226 |     case se.max of

227 |       Nothing => pure ()

228 |       Just m => do

229 |         pPutStr ":"

230 |         print file m

231 |     pPutStr "]"

234 | implementation Expression (UnaryExpression e) => Printer e => Printer (UnaryExpression e) where

235 |   print file ue = do

236 |     pPutStr $ show ue.operator

237 |     print file ue.expression

240 | implementation Expression (StarExpression e) => Printer e => Printer (StarExpression e) where

241 |   print file se = do

242 |     pPutStr "*"

243 |     print file se.expression

246 | implementation Expression (BinaryExpression e1 e2) => Printer e1 => Printer e2 => Printer (BinaryExpression e1 e2) where

247 |   print file bo = do

248 |       print file bo.first

249 |       pPutStr " "

250 |       pPutStr $ show bo.operator

251 |       pPutStr " "

252 |       print file bo.last

255 | implementation Expression (KeyValueExpression e1 e2) => Printer e1 => Printer e2 => Printer (KeyValueExpression e1 e2) where

256 |   print file kve = do

257 |     print file kve.key

258 |     pPutStr ": "

259 |     print file kve.value

264 | implementation Printer ImportSpec where

265 |   print file is = case is.name of

266 |     Nothing => print file is.path

267 |     Just i => do

268 |       print file i

269 |       pPutStr " "

270 |       print file is.path

273 | implementation Specification (TypeSpec ts t) => Printer (FieldList ts) => Printer t => Printer (TypeSpec ts t) where

274 |   print file ts = do

275 |     print file ts.name

276 |     case ts.typeParams of

277 |       [] => pure ()

278 |       xs => do

279 |         pPutStr "["

280 |         print file xs

281 |         pPutStr "]"

282 |     pPutStr " "

283 |     print file ts.type

286 | implementation Specification (ValueSpec t es) => Printer t => All Printer es => Printer (ValueSpec t es) where

287 |   print file vs = do

288 |       case vs.doc of

289 |         Nothing => pure ()

290 |         Just (MkCommentGroup cs) => do

291 |           printComments $ forget cs

292 |           printNewLine

293 |           printIndent

294 |       printNames $ List1.forget vs.names

295 |       case vs.type of

296 |         Nothing => pure ()

297 |         Just t => do

298 |           pPutStr " "

299 |           print file t

300 |       when (not $ null vs.values) $ do

301 |         pPutStr " = "

302 |         printValues vs.values

303 |       case vs.comment of

304 |         Nothing => pure ()

305 |         Just cg => do

306 |           pPutStr " "

307 |           printComments $ forget cg.comments

308 |     where

309 |       printNames : List Identifier -> PrinterMonad io ()

310 |       printNames [] = pure ()

311 |       printNames [x] = print file x

312 |       printNames (x::xs) = do

313 |           print file x

314 |           pPutStr ", "

315 |           printNames xs

317 |       printValues : { 0 ts : List Type } -> {auto ps : All Printer ts } -> HList ts -> PrinterMonad io ()

318 |       printValues [] = pure ()

319 |       printValues {ps = [p]} [x] = print file x

320 |       printValues {ps = (p::ps)} (x::xs) = do

321 |         print file x

322 |         pPutStr ", "

323 |         printValues xs

328 | implementation Printer BadStatement where

329 |   print file be = pPutStr "/* Evaluated BadStatement */"

332 | implementation Statement (ExpressionStatement e) => Printer e => Printer (ExpressionStatement e) where

333 |   print file es = do

334 |     case es.doc of

335 |       Nothing => pure ()

336 |       Just cg => do

337 |         printComments $ forget cg.comments

338 |         printNewLine

339 |         printIndent

340 |     print file es.expression

341 |     case es.comment of

342 |       Nothing => pure ()

343 |       Just cg => do

344 |         pPutStr " "

345 |         printComments $ forget cg.comments

348 | implementation Statement (DeclarationStatement d) => Printer d => Printer (DeclarationStatement d) where

349 |   print file d = print file d.declaration

352 | implementation Statement (BlockStatement sts) => All Printer sts => Printer (BlockStatement sts) where

353 |   print file bs @{stss} @{ps} = do

354 |       pPutStr "{\n"

355 |       many bs.statements {ps}

356 |       printIndent

357 |       pPutStr "}"

358 |     where

359 |       inci : Indent

360 |       inci = increaseIndent indent

362 |       many : { 0 sts : List Type } -> { ps : All Printer sts } -> HList sts -> PrinterMonad io ()

363 |       many [] = pure ()

364 |       many {ps = [p]} [x] = do

365 |         printIndent {indent = inci}

366 |         print {indent = inci} file x

367 |         printNewLine

368 |       many {ps = (p::ps)} (x::xs) = do

369 |         printIndent {indent = inci}

370 |         print {indent = inci} file x

371 |         printNewLine

372 |         many xs {ps}

375 | implementation Statement (AssignmentStatement ls rs) => All Printer ls => All Printer rs => Printer (AssignmentStatement ls rs) where

376 |   print file as = do

377 |       case as.doc of

378 |         Nothing => pure ()

379 |         Just (MkCommentGroup cs) => do

380 |           printComments $ forget cs

381 |           printNewLine

382 |           printIndent

383 |       many as.left

384 |       pPutStr " "

385 |       pPutStr $ show as.token

386 |       pPutStr " "

387 |       many as.right

388 |       case as.comment of

389 |         Nothing => pure ()

390 |         Just (MkCommentGroup cs) => do

391 |           pPutStr " "

392 |           printComments $ forget cs

393 |           when (1 < length cs) printNewLine

394 |     where

395 |       many : {0 es : List Type} -> {auto ps : All Printer es} -> HList es -> PrinterMonad io ()

396 |       many [] = pure ()

397 |       many {ps = [p]} [x] = do

398 |         print file x

399 |       many {ps = (p::ps)} (x::xs) = do

400 |         print file x

401 |         pPutStr ", "

402 |         many xs

405 | implementation Statement (IncDecStatement e o) => Show (IncOrDec o) => Printer e => Printer (IncDecStatement e o) where

406 |   print file ids = do

407 |     print file ids.expression

408 |     pPutStr $ show ids.token

411 | implementation Statement (DeferStatement f as e) => Printer (CallExpression f as e) => Printer (DeferStatement f as e) where

412 |   print file ds = do

413 |     pPutStr "defer "

414 |     print file ds.call

417 | implementation Statement (LabeledStatement s) => Printer s => Printer (LabeledStatement s) where

418 |   print file ls = do

419 |     pPutStr $ ls.label.name ++ ": "

420 |     printNewLine

421 |     printIndent

422 |     print file ls.statement

425 | implementation Statement (BranchStatement kw) => Printer (BranchStatement kw) where

426 |   print file bs = do

427 |     let kw = case bs.token of

428 |                 IsBreak => "break"

429 |                 IsContinue => "continue"

430 |                 IsGoto => "goto"

431 |                 IsFallthrough => "fallthrough"

432 |         label = case bs.label of

433 |                   Just l => " " ++ l.name

434 |                   Nothing => ""

435 |     pPutStr $ kw ++ label

438 | implementation Statement (ForStatement i c p sts) => Printer i => Printer c => Printer p => Printer (BlockStatement sts) => Printer (ForStatement i c p sts) where

439 |   print file fs = do

440 |     pPutStr "for"

441 |     case (fs.init, fs.condition, fs.post) of

442 |       (Nothing, Nothing, Nothing) => pure ()

443 |       (Nothing, Just c, Nothing) => do

444 |         pPutStr " "

445 |         print file c

446 |       _ => do

447 |         pPutStr " "

448 |         maybe (pure ()) (print file) fs.init

449 |         pPutStr "; "

450 |         maybe (pure ()) (print file) fs.condition

451 |         pPutStr "; "

452 |         maybe (pure ()) (print file) fs.post

454 |     pPutStr " "

455 |     print file fs.body

458 | implementation Statement (KeyValueRangeStatement k v a r sts) => Printer k => Printer v => Show (AssignOrDefine a) => Printer r => Printer (BlockStatement sts) => Printer (KeyValueRangeStatement k v a r sts) where

459 |   print file rs = do

460 |     pPutStr "for "

461 |     print file rs.key

462 |     pPutStr ", "

463 |     print file rs.value

464 |     pPutStr " \{show rs.token} range "

465 |     print file rs.expression

466 |     pPutStr " "

467 |     print file rs.body

470 | implementation Statement (ValueRangeStatement v a r sts) => Printer v => Show (AssignOrDefine a) => Printer r => Printer (BlockStatement sts) => Printer (ValueRangeStatement v a r sts) where

471 |   print file rs = do

472 |     pPutStr "for "

473 |     print file rs.value

474 |     pPutStr " \{show rs.token} range "

475 |     print file rs.expression

476 |     pPutStr " "

477 |     print file rs.body

480 | implementation Statement (RangeStatement r sts) => Printer r => Printer (BlockStatement sts) => Printer (RangeStatement r sts) where

481 |   print file rs = do

482 |     pPutStr "for range "

483 |     print file rs.expression

484 |     pPutStr " "

485 |     print file rs.body

488 | implementation Statement (IfStatement i c sts e) => Printer i => Printer c => Printer (BlockStatement sts) => Printer e => Printer (IfStatement i c sts e) where

489 |   print file is = do

490 |     pPutStr "if "

491 |     case is.init of

492 |       Nothing => pure ()

493 |       Just i => do

494 |         print file i

495 |         pPutStr "; "

496 |     print file is.condition

497 |     pPutStr " "

498 |     print file is.body

499 |     case is.elseBranch of

500 |       Nothing => pure ()

501 |       Just e => do

502 |         pPutStr " else "

503 |         print file e

506 | implementation Statement (SwitchStatement i e sts) => Printer i => Printer e => All Printer sts => Printer (SwitchStatement i e sts) where

507 |   print file ss = do

508 |       pPutStr "switch "

509 |       case ss.init of

510 |         Nothing => pure ()

511 |         Just i => do

512 |           print file i

513 |           pPutStr "; "

514 |       case ss.tag of

515 |         Nothing => pure ()

516 |         Just e => do

517 |           print file e

518 |           pPutStr " "

519 |       pPutStr "{"

520 |       printBody ss.body.statements

521 |       printNewLine

522 |       printIndent

523 |       pPutStr "}"

524 |     where

525 |       printBody : { 0 sts : List Type } -> {auto ps : All Printer sts } -> HList sts -> PrinterMonad io ()

526 |       printBody [] = pure ()

527 |       printBody {ps = [p]} [x] = do

528 |         printNewLine

529 |         printIndent

530 |         print file x

531 |       printBody {ps = (p::ps)} (x::xs) = do

532 |         printNewLine

533 |         printIndent

534 |         print file x

535 |         printBody xs

538 | implementation Statement (CaseClause es sts) => All Printer es => All Printer sts => Printer (CaseClause es sts) where

539 |   print file cc = do

540 |       case cc.list of

541 |         [] => pPutStr "default"

542 |         _ => pPutStr "case "

543 |       printList cc.list

544 |       pPutStr ":"

545 |       printBody cc.body

546 |     where

547 |       printList : {0 ts : List Type} -> {auto ps : All Printer ts} -> HList ts -> PrinterMonad io ()

548 |       printList [] = pure ()

549 |       printList {ps = [p]} [x] = print file x

550 |       printList {ps = p::ps} (x::xs) = do

551 |         print file x

552 |         pPutStr ", "

553 |         printList xs

555 |       inci : Indent

556 |       inci = increaseIndent indent

558 |       printBody : {0 ts : List Type} -> {auto ps : All Printer ts} -> HList ts -> PrinterMonad io ()

559 |       printBody [] = pure ()

560 |       printBody {ps = [p]} [x] = do

561 |         printNewLine

562 |         printIndent {indent = inci}

563 |         print {indent = inci} file x

564 |       printBody {ps = p::ps} (x::xs) = do

565 |         printNewLine

566 |         printIndent {indent = inci}

567 |         print {indent = inci} file x

568 |         printBody xs

571 | implementation Statement (ReturnStatement rs) => All Printer rs => Printer (ReturnStatement rs) where

572 |   print file rs = do

573 |       case rs.doc of

574 |         Nothing => pure ()

575 |         Just ds => do

576 |           printComments $ forget ds.comments

577 |           printNewLine

578 |           printIndent

579 |       pPutStr "return"

580 |       many rs.results

581 |     where

582 |       many : {0 es : List Type} -> {auto ps : All Printer es} -> HList es -> PrinterMonad io ()

583 |       many [] = pure ()

584 |       many {ps = [p]} [x] = do

585 |         pPutStr " "

586 |         print file x

587 |       many {ps = (p::ps)} (x::xs) = do

588 |         pPutStr " "

589 |         print file x

590 |         pPutStr ","

591 |         many xs

596 | implementation GoType t => Printer t => Printer (Field t) where

597 |   print file f = do

598 |     printNames f.names

599 |     case f.type of

600 |       Nothing => pure ()

601 |       Just t => do

602 |         when (not $ null f.names) $ pPutStr " "

603 |         print file t

604 |     where

605 |       printNames : List Identifier -> PrinterMonad io ()

606 |       printNames [] = pure ()

607 |       printNames [x] = print file x

608 |       printNames (x::xs) = do

609 |         print file x

610 |         pPutStr ", "

611 |         printNames xs

614 | implementation All Printer ts => Printer (FieldList ts) where

615 |   print file fl = many fl

616 |     where

617 |       many : { 0 ts : List Type } -> {auto ps : All Printer ts } -> FieldList ts -> PrinterMonad io ()

618 |       many [] = pure ()

619 |       many {ps = (p::ps)} [x] = print file x

620 |       many {ps = (p::ps)} (x::xs) = do

621 |         print file x

622 |         pPutStr ", "

623 |         many xs {ps = ps}

628 | implementation Printer BadType where

629 |   print file bt = pPutStr "/* Evaluating Bad Type */"

632 | implementation Printer TypeIdentifier where

633 |   print file ti = do

634 |     case ti.package of

635 |       Nothing => pure ()

636 |       Just p => do

637 |         print file p

638 |         pPutStr "."

639 |     print file ti.name

642 | implementation GoType (StructType es) => All Printer es => Printer (FieldList es) => Printer (StructType es) where

643 |   print file st = do

644 |       pPutStr "struct {\n"

645 |       many st.fields

646 |       printIndent

647 |       pPutStr "}" 

648 |     where

649 |       inci : Indent

650 |       inci = increaseIndent indent

652 |       many : { 0 ts : List Type } -> {auto ps : All Printer ts} -> FieldList ts -> PrinterMonad io ()

653 |       many [] = pure ()

654 |       many {ps = (p::ps)} (x::xs) = do

655 |         printIndent {indent = inci}

656 |         print {indent = inci} file x

657 |         pPutStr "\n"

658 |         many xs

661 | implementation GoType (ArrayType l e) => Printer l => Printer e => Printer (ArrayType l e) where

662 |   print file at = do

663 |     pPutStr "["

664 |     maybe (pure ()) (print file) at.length

665 |     pPutStr "]"

666 |     print file at.element

669 | implementation GoType (MapType k v) => Printer k => Printer v => Printer (MapType k v) where

670 |   print file mt = do

671 |     pPutStr "map["

672 |     print file mt.key

673 |     pPutStr "]"

674 |     print file mt.value

676 | printReturnTypes : HasIO io => All Printer rs => File -> FieldList rs -> PrinterMonad io ()

677 | printReturnTypes file fl = case fl of

678 |   [] => print file fl

679 |   [x] => do

680 |     let parens = 2 <= length x.names

681 |     pPutStr " "

682 |     when parens $ pPutStr "("

683 |     print file fl

684 |     when parens $ pPutStr ")"

685 |   xs => do

686 |     pPutStr " ("

687 |     print file fl

688 |     pPutStr ")"

691 | implementation GoType (FunctionType ts ps rs) => All Printer ts => All Printer ps => All Printer rs => Printer (FunctionType ts ps rs) where

692 |   print file ft = do

693 |     pPutStr "func("

694 |     print file ft.params

695 |     pPutStr ")"

696 |     printReturnTypes file ft.results

701 | implementation Declaration (FuncDeclaration rcs ts ps rs sts) => All Printer ps => All Printer rs => Printer (BlockStatement sts) => Printer (FuncDeclaration rcs ts ps rs sts) where

702 |   print file fd = do

703 |     case fd.doc of

704 |       Nothing => pure ()

705 |       Just ds => do

706 |         printComments $ forget ds.comments

707 |         printNewLine

708 |         printIndent

709 |     pPutStr "func "

710 |     pPutStr fd.name.name

711 |     pPutStr "("

712 |     print file fd.type.params

713 |     pPutStr ")"

714 |     printReturnTypes file fd.type.results

715 |     pPutStr " "

716 |     print file fd.body

719 | implementation Declaration (GenericDeclaration k es) => All Printer es => Show (GenericDeclarationToken k) => Printer (GenericDeclaration k es) where

720 |   print file gd = do

721 |       let multiple = hasMany gd.specs

722 |           inci = if multiple then increaseIndent indent else indent

723 |       pPutStr $ show gd.token

724 |       pPutStr " "

725 |       when multiple $ do

726 |         pPutStr "(\n"

727 |         printIndent {indent=inci}

728 |       many inci gd.specs

729 |       when multiple $ pPutStr "\n)"

730 |     where

731 |       hasMany : {0 ts : List Type} -> HList ts -> Bool

732 |       hasMany [] = False

733 |       hasMany [_] = False

734 |       hasMany _ = True

736 |       many : {0 ts : List Type} -> {auto ps : All Printer ts} -> Indent -> HList ts -> PrinterMonad io ()

737 |       many _ [] = pure ()

738 |       many {ps = [p]} i [x] = print {indent=i} file x

739 |       many {ps = (p::ps)} i (x::xs) = do

740 |         print {indent=i} file x

741 |         printNewLine

742 |         printIndent {indent=i}

743 |         many i xs

748 | implementation All Declaration ds => All Printer ds => Printer (Go.File ds) where

749 |   print file f = do

750 |     printIndent

751 |     printPackage f.packageName

752 |     printNewLine

753 |     printNewLine

754 |     printIndent

755 |     printImports f.imports

756 |     printNewLine

757 |     printNewLine

758 |     printIndent

759 |     printDecls f.decls

760 |     printNewLine

762 |     where

763 |       printDecls : { 0 ds : List Type } -> { auto ps : All Printer ds } -> HList ds -> PrinterMonad io ()

764 |       printDecls {ds = []} Nil = pure ()

765 |       printDecls {ds = [x]} {ps = [p]} [d] = print file d

766 |       printDecls {ds = x::xs} {ps = p::ps} (d::ds) = do

767 |         print file d @{p}

768 |         printNewLine

769 |         printNewLine

770 |         printIndent

771 |         printDecls ds

773 |       printPackage : Identifier -> PrinterMonad io ()

774 |       printPackage i = pPutStr "package \{i.name}"

776 |       printImports : List ImportSpec -> PrinterMonad io ()

777 |       printImports = \case

778 |         [] => pure ()

779 |         [x] => do

780 |           pPutStr "import "

781 |           print file x

782 |         xs => do

783 |           pPutStr "import (\n"

784 |           ignore $ for xs $ \spec => do

785 |             printIndent {indent = increaseIndent indent}

786 |             print file spec

787 |             printNewLine

788 |           pPutStr ")"

791 | printFile : HasIO io => All Declaration ds => Printer (Go.File ds) => (folder : String) -> Go.File ds -> io (Either PrintError ())

792 | printFile folder f = do

793 |   withFile "\{folder}/\{f.name}" WriteTruncate (pure . PrintFileError) $ \h =>

794 |     runEitherT $ print h f