0 | module Core.Binary.Prims

  2 | import Core.Context.Context

  3 | import Core.Core

  5 | import Data.Buffer

  6 | import Data.List.Elem

  7 | import Data.List1

  8 | import Data.String

  9 | import Data.Vect

 11 | import Libraries.Data.NatSet

 12 | import Libraries.Data.PosMap

 13 | import public Libraries.Utils.Binary

 14 | import public Libraries.Utils.String

 15 | import Libraries.Data.WithDefault

 17 | import System.Info

 18 | import System.File

 22 | data Bin : Type where

 26 | data ResID : Type where

 28 | public export

 29 | interface TTC a where -- TTC = TT intermediate code/interface file

 30 |   -- Add binary data representing the value to the given buffer

 31 |   toBuf : Ref Bin Binary => a -> Core ()

 32 |   -- Return the data representing a thing of type 'a' from the given buffer.

 33 |   -- Throws if the data can't be parsed as an 'a'

 34 |   fromBuf : Ref Bin Binary => Core a

 38 | initBinary : Core (Ref Bin Binary)

 40 |     = do Just buf <- coreLift $ newBuffer blockSize

 41 |              | Nothing => throw (InternalError "Buffer creation failed")

 42 |          newRef Bin (newBinary buf (cast blockSize))

 45 | initBinaryS : Int -> Core (Ref Bin Binary)

 46 | initBinaryS s

 47 |     = do Just buf <- coreLift $ newBuffer s

 48 |              | Nothing => throw (InternalError "Buffer creation failed")

 49 |          newRef Bin (newBinary buf (cast s))

 51 | extendBinary : Integer -> Binary -> Core Binary

 52 | extendBinary need (MkBin buf l s u)

 53 |     = do let newsize = s * 2

 54 |          let s' = if (newsize - l) < need

 55 |                      then newsize + need

 56 |                      else newsize

 57 |          Just buf' <- coreLift $ resizeBuffer buf (cast s')

 58 |              | Nothing => throw (InternalError "Buffer expansion failed")

 59 |          pure (MkBin buf' l s' u)

 62 | corrupt : String -> Core a

 63 | corrupt ty = throw (TTCError (Corrupt ty))

 68 | tag : {auto b : Ref Bin Binary} -> Int -> Core ()

 69 | tag {b} val

 70 |     = do chunk <- get Bin

 71 |          if avail chunk >= 1

 72 |             then

 73 |               do coreLift $ setBits8 (buf chunk) (cast $ loc chunk) $ cast val

 74 |                  put Bin (appended 1 chunk)

 75 |             else do chunk' <- extendBinary 1 chunk

 76 |                     coreLift $ setBits8 (buf chunk') (cast $ loc chunk') $ cast val

 77 |                     put Bin (appended 1 chunk')

 80 | getTag : {auto b : Ref Bin Binary} -> Core Int

 81 | getTag {b}

 82 |     = do chunk <- get Bin

 83 |          if toRead chunk >= 1

 84 |             then

 85 |               do val <- coreLift $ getBits8 (buf chunk) (cast $ loc chunk)

 86 |                  put Bin (incLoc 1 chunk)

 87 |                  pure $ cast val

 88 |               else throw (TTCError (EndOfBuffer "Bits8"))

 96 | [Wasteful] TTC Int where

 97 |   toBuf val

 98 |     = do chunk <- get Bin

 99 |          if avail chunk >= 8

100 |             then

101 |               do coreLift $ setInt (buf chunk) (cast $ loc chunk) val

102 |                  put Bin (appended 8 chunk)

103 |             else do chunk' <- extendBinary 8 chunk

104 |                     coreLift $ setInt (buf chunk') (cast $ loc chunk') val

105 |                     put Bin (appended 8 chunk')

107 |   fromBuf

108 |     = do chunk <- get Bin

109 |          if toRead chunk >= 8

110 |             then

111 |               do val <- coreLift $ getInt (buf chunk) (cast $ loc chunk)

112 |                  put Bin (incLoc 8 chunk)

113 |                  pure val

114 |               else throw (TTCError (EndOfBuffer ("Int " ++ show (loc chunk, Binary.size chunk))))

117 | TTC Int where

118 |   toBuf val

119 |     = if val >= -127 && val < 128

120 |          then tag (val + 127)

121 |          else do tag 255

122 |                  chunk <- get Bin

123 |                  if avail chunk >= 8

124 |                     then

125 |                       do coreLift $ setInt (buf chunk) (cast $ loc chunk) val

126 |                          put Bin (appended 8 chunk)

127 |                     else do chunk' <- extendBinary 8 chunk

128 |                             coreLift $ setInt (buf chunk') (cast $ loc chunk') val

129 |                             put Bin (appended 8 chunk')

131 |   fromBuf

132 |     = case !getTag of

133 |            255 => do chunk <- get Bin

134 |                      if toRead chunk >= 8

135 |                        then

136 |                          do val <- coreLift $ getInt (buf chunk) (cast $ loc chunk)

137 |                             put Bin (incLoc 8 chunk)

138 |                             pure val

139 |                        else throw (TTCError (EndOfBuffer ("Int " ++ show (loc chunk, Binary.size chunk))))

140 |            t => pure (t - 127)

143 | TTC String where

144 |   toBuf val

145 |       -- To support UTF-8 strings, this has to get the length of the string

146 |       -- in bytes, not the length in characters.

147 |       = do let ireq = stringByteLength val

148 |            let req : Integer = cast ireq

149 |            toBuf ireq

150 |            chunk <- get Bin

151 |            if avail chunk >= req

152 |               then

153 |                 do coreLift $ setString (buf chunk) (cast $ loc chunk) val

154 |                    put Bin (appended req chunk)

155 |               else do chunk' <- extendBinary req chunk

156 |                       coreLift $ setString (buf chunk') (cast $ loc chunk') val

157 |                       put Bin (appended req chunk')

159 |   fromBuf

160 |       = do ilen <- fromBuf {a = Int}

161 |            chunk <- get Bin

162 |            let len = cast ilen

163 |            when (len < 0) $ corrupt "String"

164 |            if toRead chunk >= len

165 |               then

166 |                 do val <- coreLift $ getString (buf chunk) (cast $ loc chunk) ilen

167 |                    put Bin (incLoc len chunk)

168 |                    pure val

169 |               else throw (TTCError (EndOfBuffer ("String length " ++ show len ++

170 |                                                  " at " ++ show (loc chunk))))

173 | TTC Binary where

174 |   toBuf val

175 |     = do let len = used val

176 |          let ilen : Int = cast len

177 |          toBuf ilen

178 |          chunk <- get Bin

179 |          if avail chunk >= len

180 |             then

181 |               do coreLift $ copyData (buf val) 0 ilen

182 |                                      (buf chunk) (cast $ loc chunk)

183 |                  put Bin (appended len chunk)

184 |             else do chunk' <- extendBinary len chunk

185 |                     coreLift $ copyData (buf val) 0 ilen

186 |                                         (buf chunk') (cast $ loc chunk')

187 |                     put Bin (appended len chunk')

189 |   fromBuf

190 |     = do ilen <- fromBuf

191 |          let len : Integer = cast ilen

192 |          chunk <- get Bin

193 |          if toRead chunk >= len

194 |             then

195 |               do Just newbuf <- coreLift $ newBuffer ilen

196 |                       | Nothing => corrupt "Binary"

197 |                  coreLift $ copyData (buf chunk) (cast $ loc chunk) ilen

198 |                                      newbuf 0

199 |                  put Bin (incLoc len chunk)

200 |                  pure (MkBin newbuf 0 len len)

201 |             else throw (TTCError (EndOfBuffer "Binary"))

204 | TTC Bool where

205 |   toBuf False = tag 0

206 |   toBuf True = tag 1

207 |   fromBuf

208 |       = case !getTag of

209 |              0 => pure False

210 |              1 => pure True

211 |              _ => corrupt "Bool"

214 | TTC Char where

215 |   toBuf c = toBuf (cast {to=Int} c)

216 |   fromBuf

217 |       = do i <- fromBuf

218 |            pure (cast {from=Int} i)

221 | TTC Double where

222 |   toBuf val

223 |     = do chunk <- get Bin

224 |          if avail chunk >= 8

225 |             then

226 |               do coreLift $ setDouble (buf chunk) (cast $ loc chunk) val

227 |                  put Bin (appended 8 chunk)

228 |             else do chunk' <- extendBinary 8 chunk

229 |                     coreLift $ setDouble (buf chunk') (cast $ loc chunk') val

230 |                     put Bin (appended 8 chunk')

232 |   fromBuf

233 |     = do chunk <- get Bin

234 |          if toRead chunk >= 8

235 |             then

236 |               do val <- coreLift $ getDouble (buf chunk) (cast $ loc chunk)

237 |                  put Bin (incLoc 8 chunk)

238 |                  pure val

239 |               else throw (TTCError (EndOfBuffer "Double"))

242 | (TTC a, TTC b) => TTC (a, b) where

243 |   toBuf (x, y)

244 |      = do toBuf x

245 |           toBuf y

246 |   fromBuf

247 |      = do x <- fromBuf

248 |           y <- fromBuf

249 |           pure (x, y)

252 | TTC () where

253 |   toBuf () = pure ()

254 |   fromBuf = pure ()

257 | (TTC a, {y : a} -> TTC (p y)) => TTC (DPair a p) where

258 |   toBuf (vs ** tm)

259 |       = do toBuf vs

260 |            toBuf tm

262 |   fromBuf

263 |       = do x <- fromBuf

264 |            p <- fromBuf

265 |            pure (x ** p)

268 | TTC a => TTC (Maybe a) where

269 |   toBuf Nothing

270 |      = tag 0

271 |   toBuf (Just val)

272 |      = do tag 1

273 |           toBuf val

275 |   fromBuf

276 |      = case !getTag of

277 |             0 => pure Nothing

278 |             1 => do val <- fromBuf

279 |                     pure (Just val)

280 |             _ => corrupt "Maybe"

283 | TTC a => TTC (WithDefault a def) where

284 |   toBuf def = onWithDefault

285 |                   (tag 0)

286 |                   (\v => do tag 1

287 |                             toBuf v)

288 |                   def

290 |   fromBuf

291 |      = case !getTag of

292 |             0 => pure defaulted

293 |             1 => do val <- fromBuf

294 |                     pure (specified val)

295 |             _ => corrupt "WithDefault"

298 | (TTC a, TTC b) => TTC (Either a b) where

299 |   toBuf (Left val)

300 |      = do tag 0

301 |           toBuf val

302 |   toBuf (Right val)

303 |      = do tag 1

304 |           toBuf val

306 |   fromBuf

307 |      = case !getTag of

308 |             0 => do val <- fromBuf

309 |                     pure (Left val)

310 |             1 => do val <- fromBuf

311 |                     pure (Right val)

312 |             _ => corrupt "Either"

315 | TTC a => TTC (List a) where

316 |   toBuf xs

317 |       = do toBuf (TailRec_length xs)

318 |            traverse_ (toBuf) xs

319 |     where

320 |       ||| Tail-recursive length as buffer sizes can get large

323 |       length_aux : List a -> Int -> Int

324 |       length_aux [] len = len

325 |       length_aux (_::xs) len = length_aux xs (1 + len)

327 |       TailRec_length : List a -> Int

328 |       TailRec_length xs = length_aux xs 0

330 |   fromBuf

331 |       = do len <- fromBuf {a = Int}

332 |            readElems [] (integerToNat (cast len))

333 |     where

334 |       readElems : List a -> Nat -> Core (List a)

335 |       readElems xs Z = pure (reverse xs)

336 |       readElems xs (S k)

337 |           = do val <- fromBuf

338 |                readElems (val :: xs) k

341 | TTC a => TTC (List1 a) where

342 |   toBuf xxs

343 |      = do toBuf (head xxs)

344 |           toBuf (tail xxs)

346 |   fromBuf = do

347 |     x <- fromBuf

348 |     xs <- fromBuf

349 |     pure (x ::: xs)

352 | {n : Nat} -> TTC a => TTC (Vect n a) where

353 |   toBuf xs = writeAll xs

354 |     where

355 |       writeAll : forall n . Vect n a -> Core ()

356 |       writeAll [] = pure ()

357 |       writeAll (x :: xs) = do toBuf x; writeAll xs

359 |   fromBuf {n} = rewrite sym (plusZeroRightNeutral n) in readElems [] n

360 |     where

361 |       readElems : Vect done a -> (todo : Nat) -> Core (Vect (todo + done) a)

362 |       readElems {done} xs Z

363 |           = pure (reverse xs)

364 |       readElems {done} xs (S k)

365 |           = do val <- fromBuf

366 |                rewrite (plusSuccRightSucc k done)

367 |                readElems (val :: xs) k

370 | (TTC a, Measure a) => TTC (PosMap a) where

371 |   toBuf = toBuf . toList

372 |   fromBuf = fromList <$> fromBuf

374 | %hide Fin.fromInteger

376 | count : List.Elem.Elem x xs -> Int

377 | count Here = 0

378 | count (There p) = 1 + count p

380 | toLimbs : Integer -> List Int

381 | toLimbs x

382 |     = if x == 0

383 |          then []

384 |          else if x == -1 then [-1]

385 |               else fromInteger (prim__and_Integer x 0xffffffff) ::

386 |                    toLimbs (prim__shr_Integer x 32)

388 | fromLimbs : List Int -> Integer

389 | fromLimbs [] = 0

390 | fromLimbs (x :: xs) = cast x + prim__shl_Integer (fromLimbs xs) 32

393 | TTC Integer where

394 |   toBuf val

395 |     = assert_total $ if val < 0

396 |          then do tag 0

397 |                  toBuf (toLimbs (-val))

398 |          else do tag 1

399 |                  toBuf (toLimbs val)

400 |   fromBuf

401 |     = do val <- getTag

402 |          case val of

403 |               0 => do val <- fromBuf

404 |                       pure (-(fromLimbs val))

405 |               1 => do val <- fromBuf

406 |                       pure (fromLimbs val)

407 |               _ => corrupt "Integer"

410 | TTC Bits8 where

411 |   toBuf x = toBuf $ cast {to = Int} x

412 |   fromBuf = cast {from = Int} <$> fromBuf

415 | TTC Bits16 where

416 |   toBuf x = toBuf $ cast {to = Int} x

417 |   fromBuf = cast {from = Int} <$> fromBuf

420 | TTC Bits32 where

421 |   toBuf x = toBuf $ cast {to = Integer} x

422 |   fromBuf = cast {from = Integer} <$> fromBuf

425 | TTC Bits64 where

426 |   toBuf x = toBuf $ cast {to = Integer} x

427 |   fromBuf = cast {from = Integer} <$> fromBuf

430 | TTC Int8 where

431 |   toBuf x = toBuf $ cast {to = Int} x

432 |   fromBuf = cast {from = Int} <$> fromBuf

435 | TTC Int16 where

436 |   toBuf x = toBuf $ cast {to = Int} x

437 |   fromBuf = cast {from = Int} <$> fromBuf

440 | TTC Int32 where

441 |   toBuf x = toBuf $ cast {to = Int} x

442 |   fromBuf = cast {from = Int} <$> fromBuf

445 | TTC Int64 where

446 |   toBuf x = toBuf $ cast {to = Integer} x

447 |   fromBuf = cast {from = Integer} <$> fromBuf

450 | TTC Nat where

451 |   toBuf val = toBuf (cast {to=Integer} val)

452 |   fromBuf

453 |      = do val <- fromBuf

454 |           pure (fromInteger val)

457 | TTC NatSet where

458 |   toBuf ns = toBuf (cast {to=Integer} ns)

459 |   fromBuf = cast {from=Integer} <$> fromBuf

463 | modTime : String -> Core Timestamp

464 | modTime fname

465 |   = do Right f <- coreLift $ openFile fname Read

466 |          | Left err => pure $ MkTimestamp 0 0 -- Beginning of Time :)

467 |        Right t <- coreLift $ fileTime f

468 |          | Left err => do coreLift $ closeFile f

469 |                           pure $ MkTimestamp 0 0

470 |        coreLift $ closeFile f

471 |        pure $ t.mtime

474 | hashFileWith : Maybe String -> String -> Core (Maybe String)

475 | hashFileWith Nothing _ = pure Nothing

476 | hashFileWith (Just sha256sum) fileName

477 |   = do Right fileHandle <- coreLift $ popen

478 |             (sha256sum ++ " \"" ++ osEscape fileName ++ "\"") Read

479 |          | Left _ => err

480 |        Right hashLine <- coreLift $ fGetLine fileHandle

481 |          | Left _ =>

482 |            do ignore $ coreLift $ pclose fileHandle

483 |               err

484 |        ignore $ coreLift $ pclose fileHandle

485 |        let w@(_::_) = words hashLine

486 |          | Nil => err

487 |        pure $ Just $ last w

488 |   where

489 |     err : Core a

490 |     err = coreFail $ InternalError ("Can't get " ++ sha256sum ++ " of " ++ fileName)

491 |     osEscape : String -> String

492 |     osEscape = if isWindows

493 |       then id

494 |       else escapeStringUnix

497 | TTC a => TTC (SnocList a) where

498 |   toBuf xs

499 |       = do toBuf (TailRec_length xs)

500 |            traverse_ toBuf xs

501 |     where

502 |       ||| Tail-recursive length as buffer sizes can get large

505 |       length_aux : SnocList a -> Int -> Int

506 |       length_aux [<] len = len

507 |       length_aux (xs :< _) len = length_aux xs (1 + len)

509 |       TailRec_length : SnocList a -> Int

510 |       TailRec_length xs = length_aux xs 0

512 |   fromBuf

513 |       = do len <- fromBuf {a = Int}

514 |            readElems [<] (integerToNat (cast len))

515 |     where

516 |       readElems : SnocList a -> Nat -> Core (SnocList a)

517 |       readElems xs Z = pure (reverse xs)

518 |       readElems xs (S k)

519 |           = do val <- fromBuf

520 |                readElems (xs :< val) k