0 | module TTImp.TTImp.TTC

  2 | import Core.Binary

  3 | import Core.TTC

  5 | import Core.Context

  6 | import Core.Context.TTC

  8 | import TTImp.TTImp

 10 | import Libraries.Data.NatSet

 11 | import Libraries.Data.WithDefault

 13 | %default covering

 16 |   export

 17 |   TTC RawImp where

 18 |     toBuf (IVar fc n) = do tag 0; toBuf fc; toBuf n

 19 |     toBuf (IPi fc r p n argTy retTy)

 20 |         = do tag 1; toBuf fc; toBuf r; toBuf p; toBuf n

 21 |              toBuf argTy; toBuf retTy

 22 |     toBuf (ILam fc r p n argTy scope)

 23 |         = do tag 2; toBuf fc; toBuf r; toBuf p; toBuf n;

 24 |              toBuf argTy; toBuf scope

 25 |     toBuf (ILet fc lhsFC r n nTy nVal scope)

 26 |         = do tag 3; toBuf fc; toBuf lhsFC; toBuf r; toBuf n;

 27 |              toBuf nTy; toBuf nVal; toBuf scope

 28 |     toBuf (ICase fc opts y ty xs)

 29 |         = do tag 4; toBuf fc; toBuf opts; toBuf y; toBuf ty; toBuf xs

 30 |     toBuf (ILocal fc xs sc)

 31 |         = do tag 5; toBuf fc; toBuf xs; toBuf sc

 32 |     toBuf (ICaseLocal fc _ _ _ sc)

 33 |         = toBuf sc

 34 |     toBuf (IUpdate fc fs rec)

 35 |         = do tag 6; toBuf fc; toBuf fs; toBuf rec

 36 |     toBuf (IApp fc fn arg)

 37 |         = do tag 7; toBuf fc; toBuf fn; toBuf arg

 38 |     toBuf (INamedApp fc fn y arg)

 39 |         = do tag 8; toBuf fc; toBuf fn; toBuf y; toBuf arg

 40 |     toBuf (IWithApp fc fn arg)

 41 |         = do tag 9; toBuf fc; toBuf fn; toBuf arg

 42 |     toBuf (ISearch fc depth)

 43 |         = do tag 10; toBuf fc; toBuf depth

 44 |     toBuf (IAlternative fc y xs)

 45 |         = do tag 11; toBuf fc; toBuf y; toBuf xs

 46 |     toBuf (IRewrite fc x y)

 47 |         = do tag 12; toBuf fc; toBuf x; toBuf y

 48 |     toBuf (ICoerced fc y)

 49 |         = do tag 13; toBuf fc; toBuf y

 51 |     toBuf (IBindHere fc m y)

 52 |         = do tag 14; toBuf fc; toBuf m; toBuf y

 53 |     toBuf (IBindVar fc y)

 54 |         = do tag 15; toBuf fc; toBuf y

 55 |     toBuf (IAs fc nameFC s y pattern)

 56 |         = do tag 16; toBuf fc; toBuf nameFC; toBuf s; toBuf y;

 57 |              toBuf pattern

 58 |     toBuf (IMustUnify fc r pattern)

 59 |         -- No need to record 'r', it's for type errors only

 60 |         = do tag 17; toBuf fc; toBuf pattern

 62 |     toBuf (IDelayed fc r y)

 63 |         = do tag 18; toBuf fc; toBuf r; toBuf y

 64 |     toBuf (IDelay fc t)

 65 |         = do tag 19; toBuf fc; toBuf t

 66 |     toBuf (IForce fc t)

 67 |         = do tag 20; toBuf fc; toBuf t

 69 |     toBuf (IQuote fc t)

 70 |         = do tag 21; toBuf fc; toBuf t

 71 |     toBuf (IQuoteName fc t)

 72 |         = do tag 22; toBuf fc; toBuf t

 73 |     toBuf (IQuoteDecl fc t)

 74 |         = do tag 23; toBuf fc; toBuf t

 75 |     toBuf (IUnquote fc t)

 76 |         = do tag 24; toBuf fc; toBuf t

 77 |     toBuf (IRunElab fc re t)

 78 |         = do tag 25; toBuf fc; toBuf re; toBuf t

 80 |     toBuf (IPrimVal fc y)

 81 |         = do tag 26; toBuf fc; toBuf y

 82 |     toBuf (IType fc)

 83 |         = do tag 27; toBuf fc

 84 |     toBuf (IHole fc y)

 85 |         = do tag 28; toBuf fc; toBuf y

 86 |     toBuf (IUnifyLog fc lvl x) = toBuf x

 88 |     toBuf (Implicit fc i)

 89 |         = do tag 29; toBuf fc; toBuf i

 90 |     toBuf (IWithUnambigNames fc ns rhs)

 91 |         = do tag 30; toBuf fc; toBuf ns; toBuf rhs

 92 |     toBuf (IAutoApp fc fn arg)

 93 |         = do tag 31; toBuf fc; toBuf fn; toBuf arg

 95 |     fromBuf

 96 |         = case !getTag of

 97 |                0 => do fc <- fromBuf; n <- fromBuf;

 98 |                        pure (IVar fc n)

 99 |                1 => do fc <- fromBuf;

100 |                        r <- fromBuf; p <- fromBuf;

101 |                        n <- fromBuf

102 |                        argTy <- fromBuf; retTy <- fromBuf

103 |                        pure (IPi fc r p n argTy retTy)

104 |                2 => do fc <- fromBuf;

105 |                        r <- fromBuf; p <- fromBuf; n <- fromBuf

106 |                        argTy <- fromBuf; scope <- fromBuf

107 |                        pure (ILam fc r p n argTy scope)

108 |                3 => do fc <- fromBuf;

109 |                        lhsFC <- fromBuf;

110 |                        r <- fromBuf; n <- fromBuf

111 |                        nTy <- fromBuf; nVal <- fromBuf

112 |                        scope <- fromBuf

113 |                        pure (ILet fc lhsFC r n nTy nVal scope)

114 |                4 => do fc <- fromBuf; opts <- fromBuf; y <- fromBuf;

115 |                        ty <- fromBuf; xs <- fromBuf

116 |                        pure (ICase fc opts y ty xs)

117 |                5 => do fc <- fromBuf;

118 |                        xs <- fromBuf; sc <- fromBuf

119 |                        pure (ILocal fc xs sc)

120 |                6 => do fc <- fromBuf; fs <- fromBuf

121 |                        rec <- fromBuf

122 |                        pure (IUpdate fc fs rec)

123 |                7 => do fc <- fromBuf; fn <- fromBuf

124 |                        arg <- fromBuf

125 |                        pure (IApp fc fn arg)

126 |                8 => do fc <- fromBuf; fn <- fromBuf

127 |                        y <- fromBuf; arg <- fromBuf

128 |                        pure (INamedApp fc fn y arg)

129 |                9 => do fc <- fromBuf; fn <- fromBuf

130 |                        arg <- fromBuf

131 |                        pure (IWithApp fc fn arg)

132 |                10 => do fc <- fromBuf; depth <- fromBuf

133 |                         pure (ISearch fc depth)

134 |                11 => do fc <- fromBuf; y <- fromBuf

135 |                         xs <- fromBuf

136 |                         pure (IAlternative fc y xs)

137 |                12 => do fc <- fromBuf; x <- fromBuf; y <- fromBuf

138 |                         pure (IRewrite fc x y)

139 |                13 => do fc <- fromBuf; y <- fromBuf

140 |                         pure (ICoerced fc y)

141 |                14 => do fc <- fromBuf; m <- fromBuf; y <- fromBuf

142 |                         pure (IBindHere fc m y)

143 |                15 => do fc <- fromBuf; y <- fromBuf

144 |                         pure (IBindVar fc y)

145 |                16 => do fc <- fromBuf; nameFC <- fromBuf

146 |                         side <- fromBuf;

147 |                         y <- fromBuf; pattern <- fromBuf

148 |                         pure (IAs fc nameFC side y pattern)

149 |                17 => do fc <- fromBuf

150 |                         pattern <- fromBuf

151 |                         pure (IMustUnify fc UnknownDot pattern)

153 |                18 => do fc <- fromBuf; r <- fromBuf

154 |                         y <- fromBuf

155 |                         pure (IDelayed fc r y)

156 |                19 => do fc <- fromBuf; y <- fromBuf

157 |                         pure (IDelay fc y)

158 |                20 => do fc <- fromBuf; y <- fromBuf

159 |                         pure (IForce fc y)

161 |                21 => do fc <- fromBuf; y <- fromBuf

162 |                         pure (IQuote fc y)

163 |                22 => do fc <- fromBuf; y <- fromBuf

164 |                         pure (IQuoteName fc y)

165 |                23 => do fc <- fromBuf; y <- fromBuf

166 |                         pure (IQuoteDecl fc y)

167 |                24 => do fc <- fromBuf; y <- fromBuf

168 |                         pure (IUnquote fc y)

169 |                25 => do fc <- fromBuf; re <- fromBuf; y <- fromBuf

170 |                         pure (IRunElab fc re y)

172 |                26 => do fc <- fromBuf; y <- fromBuf

173 |                         pure (IPrimVal fc y)

174 |                27 => do fc <- fromBuf

175 |                         pure (IType fc)

176 |                28 => do fc <- fromBuf; y <- fromBuf

177 |                         pure (IHole fc y)

178 |                29 => do fc <- fromBuf

179 |                         i <- fromBuf

180 |                         pure (Implicit fc i)

181 |                30 => do fc <- fromBuf

182 |                         ns <- fromBuf

183 |                         rhs <- fromBuf

184 |                         pure (IWithUnambigNames fc ns rhs)

185 |                31 => do fc <- fromBuf; fn <- fromBuf

186 |                         arg <- fromBuf

187 |                         pure (IAutoApp fc fn arg)

188 |                _ => corrupt "RawImp"

190 |   export

191 |   TTC IFieldUpdate where

192 |     toBuf (ISetField p val)

193 |         = do tag 0; toBuf p; toBuf val

194 |     toBuf (ISetFieldApp p val)

195 |         = do tag 1; toBuf p; toBuf val

197 |     fromBuf

198 |         = case !getTag of

199 |                0 => do p <- fromBuf; val <- fromBuf

200 |                        pure (ISetField p val)

201 |                1 => do p <- fromBuf; val <- fromBuf

202 |                        pure (ISetFieldApp p val)

203 |                _ => corrupt "IFieldUpdate"

205 |   export

206 |   TTC BindMode where

207 |     toBuf (PI r) = do tag 0; toBuf r

208 |     toBuf PATTERN = tag 1

209 |     toBuf NONE = tag 2

210 |     toBuf COVERAGE = tag 3

212 |     fromBuf

213 |         = case !getTag of

214 |                0 => do x <- fromBuf

215 |                        pure (PI x)

216 |                1 => pure PATTERN

217 |                2 => pure NONE

218 |                3 => pure COVERAGE

219 |                _ => corrupt "BindMode"

221 |   export

222 |   TTC AltType where

223 |     toBuf FirstSuccess = tag 0

224 |     toBuf Unique = tag 1

225 |     toBuf (UniqueDefault x) = do tag 2; toBuf x

227 |     fromBuf

228 |         = case !getTag of

229 |                0 => pure FirstSuccess

230 |                1 => pure Unique

231 |                2 => do x <- fromBuf

232 |                        pure (UniqueDefault x)

233 |                _ => corrupt "AltType"

235 |   export

236 |   TTC ImpClause where

237 |     toBuf (PatClause fc lhs rhs)

238 |         = do tag 0; toBuf fc; toBuf lhs; toBuf rhs

239 |     toBuf (ImpossibleClause fc lhs)

240 |         = do tag 1; toBuf fc; toBuf lhs

241 |     toBuf (WithClause fc lhs rig wval prf flags cs)

242 |         = do tag 2

243 |              toBuf fc

244 |              toBuf lhs

245 |              toBuf rig

246 |              toBuf wval

247 |              toBuf prf

248 |              toBuf cs

250 |     fromBuf

251 |         = case !getTag of

252 |                0 => do fc <- fromBuf; lhs <- fromBuf;

253 |                        rhs <- fromBuf

254 |                        pure (PatClause fc lhs rhs)

255 |                1 => do fc <- fromBuf; lhs <- fromBuf;

256 |                        pure (ImpossibleClause fc lhs)

257 |                2 => do fc <- fromBuf; lhs <- fromBuf;

258 |                        rig <- fromBuf; wval <- fromBuf;

259 |                        prf <- fromBuf;

260 |                        cs <- fromBuf

261 |                        pure (WithClause fc lhs rig wval prf [] cs)

262 |                _ => corrupt "ImpClause"

264 |   export

265 |   TTC DataOpt where

266 |     toBuf (SearchBy ns)

267 |         = do tag 0; toBuf ns

268 |     toBuf NoHints = tag 1

269 |     toBuf UniqueSearch = tag 2

270 |     toBuf External = tag 3

271 |     toBuf NoNewtype = tag 4

273 |     fromBuf

274 |         = case !getTag of

275 |                0 => do ns <- fromBuf

276 |                        pure (SearchBy ns)

277 |                1 => pure NoHints

278 |                2 => pure UniqueSearch

279 |                3 => pure External

280 |                4 => pure NoNewtype

281 |                _ => corrupt "DataOpt"

283 |   export

284 |   TTC ImpData where

285 |     toBuf (MkImpData fc n tycon opts cons)

286 |         = do tag 0; toBuf fc; toBuf n; toBuf tycon; toBuf opts

287 |              toBuf cons

288 |     toBuf (MkImpLater fc n tycon)

289 |         = do tag 1; toBuf fc; toBuf n; toBuf tycon

291 |     fromBuf

292 |         = case !getTag of

293 |                0 => do fc <- fromBuf; n <- fromBuf;

294 |                        tycon <- fromBuf; opts <- fromBuf

295 |                        cons <- fromBuf

296 |                        pure (MkImpData fc n tycon opts cons)

297 |                1 => do fc <- fromBuf; n <- fromBuf;

298 |                        tycon <- fromBuf

299 |                        pure (MkImpLater fc n tycon)

300 |                _ => corrupt "ImpData"

302 |   export

303 |   TTC (ImpRecordData Name) where

304 |     toBuf (MkImpRecord header body)

305 |         = do toBuf header; toBuf body;

307 |     fromBuf

308 |         = do header <- fromBuf; body <- fromBuf;

309 |              pure (MkImpRecord header body)

311 |   export

312 |   TTC FnOpt where

313 |     toBuf Inline = tag 0

314 |     toBuf (Hint t) = do tag 1; toBuf t

315 |     toBuf (GlobalHint t) = do tag 2; toBuf t

316 |     toBuf ExternFn = tag 3

317 |     toBuf (ForeignFn cs) = do tag 4; toBuf cs

318 |     toBuf Invertible = tag 5

319 |     toBuf (Totality Total) = tag 6

320 |     toBuf (Totality CoveringOnly) = tag 7

321 |     toBuf (Totality PartialOK) = tag 8

322 |     toBuf Macro = tag 9

323 |     toBuf (SpecArgs ns) = do tag 10; toBuf ns

324 |     toBuf TCInline = tag 11

325 |     toBuf NoInline = tag 12

326 |     toBuf Unsafe = tag 13

327 |     toBuf Deprecate = tag 14

328 |     toBuf (ForeignExport cs) = do tag 15; toBuf cs

330 |     fromBuf

331 |         = case !getTag of

332 |                0 => pure Inline

333 |                1 => do t <- fromBuf; pure (Hint t)

334 |                2 => do t <- fromBuf; pure (GlobalHint t)

335 |                3 => pure ExternFn

336 |                4 => do cs <- fromBuf; pure (ForeignFn cs)

337 |                5 => pure Invertible

338 |                6 => pure (Totality Total)

339 |                7 => pure (Totality CoveringOnly)

340 |                8 => pure (Totality PartialOK)

341 |                9 => pure Macro

342 |                10 => do ns <- fromBuf; pure (SpecArgs ns)

343 |                11 => pure TCInline

344 |                12 => pure NoInline

345 |                13 => pure Unsafe

346 |                14 => pure Deprecate

347 |                15 => do cs <- fromBuf; pure (ForeignExport cs)

348 |                _ => corrupt "FnOpt"

350 |   export

351 |   TTC (IClaimData Name) where

352 |     toBuf (MkIClaimData rig vis opts type)

353 |         = do toBuf rig; toBuf vis; toBuf opts; toBuf type

354 |     fromBuf

355 |         = do rig <- fromBuf

356 |              vis <- fromBuf

357 |              opts <- fromBuf

358 |              type <- fromBuf

359 |              pure $ MkIClaimData rig vis opts type

361 |   export

362 |   TTC ImpDecl where

363 |     toBuf (IClaim claim)

364 |         = do tag 0; toBuf claim

365 |     toBuf (IData fc vis mbtot d)

366 |         = do tag 1; toBuf fc; toBuf vis; toBuf mbtot; toBuf d

367 |     toBuf (IDef fc n xs)

368 |         = do tag 2; toBuf fc; toBuf n; toBuf xs

369 |     toBuf (IParameters fc vis d)

370 |         = do tag 3; toBuf fc; toBuf vis; toBuf d

371 |     toBuf (IRecord fc ns vis mbtot r)

372 |         = do tag 4; toBuf fc; toBuf ns; toBuf vis; toBuf mbtot; toBuf r

373 |     toBuf (INamespace fc xs ds)

374 |         = do tag 5; toBuf fc; toBuf xs; toBuf ds

375 |     toBuf (ITransform fc n lhs rhs)

376 |         = do tag 6; toBuf fc; toBuf n; toBuf lhs; toBuf rhs

377 |     toBuf (IRunElabDecl fc tm)

378 |         = do tag 7; toBuf fc; toBuf tm

379 |     toBuf (IPragma _ _ f) = throw (InternalError "Can't write Pragma")

380 |     toBuf (ILog n)

381 |         = do tag 8; toBuf n

382 |     toBuf (IBuiltin fc type name)

383 |         = do tag 9; toBuf fc; toBuf type; toBuf name

384 |     toBuf (IFail {})

385 |         = pure ()

387 |     fromBuf

388 |         = case !getTag of

389 |                0 => do claimData <- fromBuf

390 |                        pure (IClaim claimData)

391 |                1 => do fc <- fromBuf; vis <- fromBuf

392 |                        mbtot <- fromBuf; d <- fromBuf

393 |                        pure (IData fc vis mbtot d)

394 |                2 => do fc <- fromBuf; n <- fromBuf

395 |                        xs <- fromBuf

396 |                        pure (IDef fc n xs)

397 |                3 => do fc <- fromBuf; vis <- fromBuf

398 |                        d <- fromBuf

399 |                        pure (IParameters fc vis d)

400 |                4 => do fc <- fromBuf; ns <- fromBuf;

401 |                        vis <- fromBuf; mbtot <- fromBuf;

402 |                        r <- fromBuf

403 |                        pure (IRecord fc ns vis mbtot r)

404 |                5 => do fc <- fromBuf; xs <- fromBuf

405 |                        ds <- fromBuf

406 |                        pure (INamespace fc xs ds)

407 |                6 => do fc <- fromBuf; n <- fromBuf

408 |                        lhs <- fromBuf; rhs <- fromBuf

409 |                        pure (ITransform fc n lhs rhs)

410 |                7 => do fc <- fromBuf; tm <- fromBuf

411 |                        pure (IRunElabDecl fc tm)

412 |                8 => do n <- fromBuf

413 |                        pure (ILog n)

414 |                9 => do fc <- fromBuf

415 |                        type <- fromBuf

416 |                        name <- fromBuf

417 |                        pure (IBuiltin fc type name)

418 |                _ => corrupt "ImpDecl"