0 | module Core.SchemeEval.Evaluate

  2 | import Core.Context.Log

  3 | import Core.Env

  4 | import Core.SchemeEval.Compile

  5 | import Core.SchemeEval.ToScheme

  7 | import Libraries.Data.NameMap

  8 | import Libraries.Utils.Scheme

 10 | public export

 11 | data SObj : Scoped where

 12 |      MkSObj : ForeignObj -> SchVars vars -> SObj vars

 20 |   public export

 21 |   data SHead : Scoped where

 22 |        SLocal : (idx : Nat) -> (0 p : IsVar nm idx vars) -> SHead vars

 23 |        SRef : NameType -> Name -> SHead vars

 24 |        SMeta : Name -> Int -> List (Core (SNF vars)) -> SHead vars

 26 |   public export

 27 |   data SNF : Scoped where

 28 |        SBind    : FC -> (x : Name) -> Binder (SNF vars) ->

 29 |                   (SObj vars -> Core (SNF vars)) -> SNF vars

 30 |        SApp     : FC -> SHead vars -> List (Core (SNF vars)) -> SNF vars

 31 |        SDCon    : FC -> Name -> (tag : Int) -> (arity : Nat) ->

 32 |                   List (Core (SNF vars)) -> SNF vars

 33 |        STCon    : FC -> Name -> (arity : Nat) ->

 34 |                   List (Core (SNF vars)) -> SNF vars

 35 |        SDelayed : FC -> LazyReason -> SNF vars -> SNF vars

 36 |        SDelay   : FC -> LazyReason -> Core (SNF vars) -> Core (SNF vars) ->

 37 |                   SNF vars

 38 |        SForce   : FC -> LazyReason -> SNF vars -> SNF vars

 39 |        SPrimVal : FC -> Constant -> SNF vars

 40 |        SErased  : FC -> WhyErased (SNF vars) -> SNF vars

 41 |        SType    : FC -> Name -> SNF vars

 43 | getAllNames : {auto c : Ref Ctxt Defs} ->

 44 |               NameMap () -> List Name -> Core (NameMap ())

 45 | getAllNames done [] = pure done

 46 | getAllNames done (x :: xs)

 47 |     = do let Nothing = lookup x done

 48 |              | _ => getAllNames done xs

 49 |          defs <- get Ctxt

 50 |          Just gdef <- lookupCtxtExact x (gamma defs)

 51 |              | _ => getAllNames done xs

 52 |          getAllNames (insert x () done) (xs ++ keys (refersTo gdef))

 58 | seval : {auto c : Ref Ctxt Defs} ->

 59 |         SchemeMode -> Env Term vars -> Term vars -> Core (SObj vars)

 60 | seval mode env tm

 61 |     = do -- Check the evaluator is initialised. This will fail if the backend

 62 |          -- doesn't support scheme evaluation.

 63 |          True <- logTimeWhen False 0 "Scheme eval" initialiseSchemeEval

 64 |               | False => throw (InternalError "Loading scheme support failed")

 66 |          -- make sure all the names in the term are compiled

 67 |          -- We need to recheck in advance, since definitions might have changed

 68 |          -- since we last evaluated a name, and we might have evaluated the

 69 |          -- name in a different mode

 70 |          let ms = getRefs (MN "" 0) tm

 71 |          let rs = addMetas False ms tm

 72 |          names <- getAllNames empty (keys rs)

 73 |          traverse_ (compileDef mode) (keys names)

 75 |          i <- newRef Sym 0

 76 |          (bind, schEnv) <- mkEnv env id

 77 |          stm <- compile schEnv !(toFullNames tm)

 78 |          Just res <- coreLift $ evalSchemeObj (bind stm)

 79 |               | Nothing => throw (InternalError "Compiling expression failed")

 80 |          pure (MkSObj res schEnv)

 81 |   where

 82 |     mkEnv : forall vars . Ref Sym Integer =>

 83 |             Env Term vars ->

 84 |             (SchemeObj Write -> SchemeObj Write) ->

 85 |             Core (SchemeObj Write -> SchemeObj Write, SchVars vars)

 86 |     mkEnv [] k = pure (k, [])

 87 |     mkEnv (Let fc c val ty :: es) k

 88 |         = do i <- nextName

 89 |              (bind, vs) <- mkEnv es k

 90 |              val' <- compile vs val

 91 |              let n = "let-var-" ++ show i

 92 |              pure (\x => Let n val' (bind x), Bound n :: vs)

 93 |     mkEnv (_ :: es) k

 94 |         = do i <- nextName

 95 |              (bind, vs) <- mkEnv es k

 96 |              pure (bind, Free ("free-" ++ show i) :: vs)

 98 | invalid : Core (Term vs)

 99 | invalid = pure (Erased emptyFC Placeholder)

101 | invalidS : Core (SNF vs)

102 | invalidS = pure (SErased emptyFC Placeholder)

104 | getArgList : ForeignObj -> List ForeignObj

105 | getArgList obj

106 |     = if isPair obj

107 |          then unsafeFst obj :: getArgList (unsafeSnd obj)

108 |          else []

110 | quoteFC : ForeignObj -> FC

111 | quoteFC fc_in = fromMaybe emptyFC (fromScheme (decodeObj fc_in))

113 | quoteLazyReason : ForeignObj -> LazyReason

114 | quoteLazyReason r_in = fromMaybe LUnknown (fromScheme (decodeObj r_in))

116 | quoteTypeLevel : ForeignObj -> Name

117 | quoteTypeLevel u_in = fromMaybe (MN "top" 0) (fromScheme (decodeObj u_in))

119 | quoteRigCount : ForeignObj -> RigCount

120 | quoteRigCount rig_in = fromMaybe top (fromScheme (decodeObj rig_in))

122 | quoteBinderName : ForeignObj -> Name

123 | quoteBinderName nm_in

124 |   = fromMaybe (UN (Basic "x")) (fromScheme (decodeObj nm_in))

126 | quoteOrInvalid : Scheme x =>

127 |               ForeignObj -> (x -> Core (Term vars)) -> Core (Term vars)

128 | quoteOrInvalid obj_in k = do

129 |   let Just obj = fromScheme (decodeObj obj_in)

130 |     | Nothing => invalid

131 |   k obj

133 | quoteOrInvalidS : Scheme x =>

134 |                  ForeignObj -> (x -> Core (SNF vars)) -> Core (SNF vars)

135 | quoteOrInvalidS obj_in k = do

136 |   let Just obj = fromScheme (decodeObj obj_in)

137 |     | Nothing => invalidS

138 |   k obj

142 |   -- We don't use decodeObj because then we have to traverse the term twice.

143 |   -- Instead, decode the ForeignObj directly, which is uglier but faster.

144 |   quoteVector : Ref Sym Integer =>

145 |                 Ref Ctxt Defs =>

146 |                 SchVars (outer ++ vars) ->

147 |                 Integer -> List ForeignObj ->

148 |                 Core (Term (outer ++ vars))

149 |   quoteVector svs (-2) [_, fname_in, args_in] -- Blocked app

150 |       = quoteOrInvalid fname_in $ \ fname => do

151 |            let argList = getArgList args_in

152 |            args <- traverse (quote' svs) argList

153 |            pure (apply emptyFC (Ref emptyFC Func fname) args)

154 |   quoteVector svs (-10) [_, fn_arity, args_in] -- Blocked meta app

155 |       = quoteOrInvalid {x = (Name, Integer)} fn_arity $ \ (fname, arity_in) => do

156 |            let arity : Nat = cast arity_in

157 |            let argList = getArgList args_in

158 |            args <- traverse (quote' svs) argList

159 |            defs <- get Ctxt

160 |            fnameF <- toFullNames fname

161 |            (idx, _) <- getPosition fname (gamma defs)

162 |            pure (apply emptyFC (Meta emptyFC fnameF idx (take arity args))

163 |                                (drop arity args))

164 |   quoteVector svs (-11) [_, loc_in, args_in] -- Blocked local var application

165 |       = do loc <- quote' svs loc_in

166 |            let argList = getArgList args_in

167 |            args <- traverse (quote' svs) argList

168 |            pure (apply emptyFC loc args)

169 |   quoteVector svs (-1) (_ :: strtag :: cname_in :: fc_in :: args_in) -- TyCon

170 |       = quoteOrInvalid cname_in $ \ cname => do

171 |            let fc = emptyFC -- quoteFC fc_in

172 |            args <- traverse (quote' svs) args_in

173 |            pure (apply fc (Ref fc (TyCon (length args)) cname)

174 |                            args)

175 |   quoteVector svs (-15) [_, r_in, ty_in] -- Delayed

176 |       = do ty <- quote' svs ty_in

177 |            let r = quoteLazyReason r_in

178 |            pure (TDelayed emptyFC r ty)

179 |   quoteVector svs (-4) [_, r_in, fc_in, ty_in, tm_in] -- Delay

180 |       = do -- Block further reduction under tm_in

181 |            Just _ <- coreLift $ evalSchemeStr "(ct-setBlockAll #t)"

182 |                 | Nothing => invalid

183 |            let Procedure tmproc = decodeObj tm_in

184 |                 | _ => invalid

185 |            let Procedure typroc = decodeObj ty_in

186 |                 | _ => invalid

187 |            tm <- quote' svs (unsafeForce tmproc)

188 |            ty <- quote' svs (unsafeForce typroc)

189 |            -- Turn blocking off again

190 |            Just _ <- coreLift $ evalSchemeStr "(ct-setBlockAll #f)"

191 |                 | Nothing => invalid

192 |            let fc = quoteFC fc_in

193 |            let r = quoteLazyReason r_in

194 |            pure (TDelay fc r ty tm)

195 |   quoteVector svs (-5) [_, r_in, fc_in, tm_in] -- Force

196 |       = do -- The thing we were trying to force was stuck. Corresponding to

197 |            -- Core.Normalise, reduce it anyway here (so no ct-blockAll like above)

198 |            tm <- quote' svs tm_in

199 |            let fc = quoteFC fc_in

200 |            let r = quoteLazyReason r_in

201 |            pure (TForce fc r tm)

202 |   quoteVector svs (-6) [_, fc_in, imp_in] -- Erased

203 |       = do let fc = quoteFC fc_in

204 |            imp <- quoteWhyErased (quote' svs) imp_in

205 |            pure (Erased fc imp)

206 |   quoteVector svs (-7) [_, fc_in, u_in] -- Type

207 |       = do let fc = quoteFC fc_in

208 |            let u = quoteTypeLevel u_in

209 |            pure (TType fc u)

210 |   quoteVector svs (-8) [_, proc_in, rig_in, pi_in, ty_in, name_in] -- Lambda

211 |       = do let name = quoteBinderName name_in

212 |            let rig = quoteRigCount rig_in

213 |            ty <- quote' svs ty_in

214 |            pi <- quotePiInfo svs pi_in

215 |            quoteBinder svs Lam proc_in rig pi ty name

216 |   quoteVector svs (-3) [_, proc_in, rig_in, pi_in, ty_in, name_in] -- Pi

217 |       = do let name = quoteBinderName name_in

218 |            let rig = quoteRigCount rig_in

219 |            ty <- quote' svs ty_in

220 |            pi <- quotePiInfo svs pi_in

221 |            quoteBinder svs Pi proc_in rig pi ty name

222 |   quoteVector svs (-12) [_, proc_in, rig_in, pi_in, ty_in, name_in] -- PVar

223 |       = do let name = quoteBinderName name_in

224 |            let rig = quoteRigCount rig_in

225 |            ty <- quote' svs ty_in

226 |            pi <- quotePiInfo svs pi_in

227 |            quoteBinder svs PVar proc_in rig pi ty name

228 |   quoteVector svs (-13) [_, proc_in, rig_in, ty_in, name_in] -- PVTy

229 |       = do let name = quoteBinderName name_in

230 |            let rig = quoteRigCount rig_in

231 |            ty <- quote' svs ty_in

232 |            quoteBinder svs (\fc, r, p, t => PVTy fc r t) proc_in rig Explicit ty name

233 |   quoteVector svs (-14) [_, proc_in, rig_in, val_in, ty_in, name_in] -- PLet

234 |       = do let name = quoteBinderName name_in

235 |            let rig = quoteRigCount rig_in

236 |            ty <- quote' svs ty_in

237 |            val <- quote' svs val_in

238 |            quotePLet svs proc_in rig val ty name

239 |   quoteVector svs (-9) [_, blocked, _] -- Blocked top level lambda

240 |       = quote' svs blocked

241 |   quoteVector svs (-100) [_, x]

242 |       = quoteOrInvalid x $ \ x' => pure $ PrimVal emptyFC (I x')

243 |   quoteVector svs (-101) [_, x]

244 |       = quoteOrInvalid x $ \ x' => pure $ PrimVal emptyFC (I8 x')

245 |   quoteVector svs (-102) [_, x]

246 |       = quoteOrInvalid x $ \ x' => pure $ PrimVal emptyFC (I16 x')

247 |   quoteVector svs (-103) [_, x]

248 |       = quoteOrInvalid x $ \ x' => pure $ PrimVal emptyFC (I32 x')

249 |   quoteVector svs (-104) [_, x]

250 |       = quoteOrInvalid x $ \ x' => pure $ PrimVal emptyFC (I64 x')

251 |   quoteVector svs (-105) [_, x]

252 |       = quoteOrInvalid x $ \ x' => pure $ PrimVal emptyFC (BI x')

253 |   quoteVector svs (-106) [_, x]

254 |       = quoteOrInvalid x $ \ x' => pure $ PrimVal emptyFC (B8 x')

255 |   quoteVector svs (-107) [_, x]

256 |       = quoteOrInvalid x $ \ x' => pure $ PrimVal emptyFC (B16 x')

257 |   quoteVector svs (-108) [_, x]

258 |       = quoteOrInvalid x $ \ x' => pure $ PrimVal emptyFC (B32 x')

259 |   quoteVector svs (-109) [_, x]

260 |       = quoteOrInvalid x $ \ x' => pure $ PrimVal emptyFC (B64 x')

261 |   quoteVector svs tag (_ :: cname_in :: fc_in :: args_in) -- DataCon

262 |       = if tag >= 0

263 |            then quoteOrInvalid cname_in $ \ cname =>  do

264 |              let fc = emptyFC -- quoteFC fc_in

265 |              args <- traverse (quote' svs) args_in

266 |              pure (apply fc (Ref fc (DataCon (cast tag) (length args)) cname)

267 |                             args)

268 |            else invalid

269 |   quoteVector _ _ _ = invalid

271 |   quotePiInfo : Ref Sym Integer =>

272 |                 Ref Ctxt Defs =>

273 |                 SchVars (outer ++ vars) ->

274 |                 ForeignObj ->

275 |                 Core (PiInfo (Term (outer ++ vars)))

276 |   quotePiInfo svs obj

277 |       = if isInteger obj

278 |            then case unsafeGetInteger obj of

279 |                      0 => pure Implicit

280 |                      1 => pure Explicit

281 |                      2 => pure AutoImplicit

282 |                      _ => pure Explicit

283 |            else if isBox obj

284 |                    then do t' <- quote' svs (unsafeUnbox obj)

285 |                            pure (DefImplicit t')

286 |            else pure Explicit

288 |   quoteWhyErased : (ForeignObj -> Core a) ->

289 |                    ForeignObj ->

290 |                    Core (WhyErased a)

291 |   quoteWhyErased qt obj

292 |       = if isInteger obj

293 |            then case unsafeGetInteger obj of

294 |                      0 => pure Impossible

295 |                      _ => pure Placeholder

296 |            else if isBox obj

297 |                    then do t' <- qt (unsafeUnbox obj)

298 |                            pure (Dotted t')

299 |            else pure Placeholder

301 |   quoteBinder : Ref Sym Integer =>

302 |                 Ref Ctxt Defs =>

303 |                 SchVars (outer ++ vars) ->

304 |                 (forall ty . FC -> RigCount -> PiInfo ty -> ty -> Binder ty) ->

305 |                 ForeignObj -> -- body of binder, represented as a function

306 |                 RigCount ->

307 |                 PiInfo (Term (outer ++ vars)) ->

308 |                 Term (outer ++ vars) -> -- decoded type

309 |                 Name -> -- bound name

310 |                 Core (Term (outer ++ vars))

311 |   quoteBinder svs binder proc_in r pi ty name

312 |       = do let Procedure proc = decodeObj proc_in

313 |                     | _ => invalid

314 |            i <- nextName

315 |            let n = show name ++ "-" ++ show i

316 |            let sc = unsafeApply proc (makeSymbol n)

317 |            sc' <- quote' {outer = name :: outer} (Bound n :: svs) sc

318 |            pure (Bind emptyFC name

319 |                       (binder emptyFC r pi ty)

320 |                       sc')

322 |   quotePLet : Ref Sym Integer =>

323 |               Ref Ctxt Defs =>

324 |               SchVars (outer ++ vars) ->

325 |               ForeignObj -> -- body of binder, represented as a function

326 |               RigCount ->

327 |               Term (outer ++ vars) -> -- decoded type

328 |               Term (outer ++ vars) -> -- decoded value

329 |               Name -> -- bound name

330 |               Core (Term (outer ++ vars))

331 |   quotePLet svs proc_in r val ty name

332 |       = do let Procedure proc = decodeObj proc_in

333 |                     | _ => invalid

334 |            i <- nextName

335 |            let n = show name ++ "-" ++ show i

336 |            let sc = unsafeApply proc (makeSymbol n)

337 |            sc' <- quote' {outer = name :: outer} (Bound n :: svs) sc

338 |            pure (Bind emptyFC name

339 |                       (PLet emptyFC r val ty)

340 |                       sc')

342 |   quote' : Ref Sym Integer =>

343 |            Ref Ctxt Defs =>

344 |            SchVars (outer ++ vars) -> ForeignObj ->

345 |            Core (Term (outer ++ vars))

346 |   quote' svs obj

347 |       = if isVector obj

348 |            then quoteVector svs (unsafeGetInteger (unsafeVectorRef obj 0))

349 |                                 (unsafeVectorToList obj)

350 |         else if isProcedure obj then quoteBinder svs Lam obj top

351 |                                               Explicit

352 |                                               (Erased emptyFC Placeholder)

353 |                                               (UN (Basic "x"))

354 |         else if isSymbol obj then pure $ findName svs (unsafeReadSymbol obj)

355 |         else if isFloat obj then pure $ PrimVal emptyFC (Db (unsafeGetFloat obj))

356 |         else if isInteger obj then pure $ PrimVal emptyFC (I (cast (unsafeGetInteger obj)))

357 |         else if isString obj then pure $ PrimVal emptyFC (Str (unsafeGetString obj))

358 |         else if isChar obj then pure $ PrimVal emptyFC (Ch (unsafeGetChar obj))

359 |         else invalid

360 |     where

361 |       findName : forall vars . SchVars vars -> String -> Term vars

362 |       findName [] n = Ref emptyFC Func (UN (Basic n))

363 |       findName (x :: xs) n

364 |           = if getName x == n

365 |                then Local emptyFC Nothing _ First

366 |                else let Local fc loc _ p = findName xs n

367 |                            | _ => Ref emptyFC Func (UN (Basic n)) in

368 |                         Local fc loc _ (Later p)

370 |       readVector : Integer -> Integer -> ForeignObj -> List ForeignObj

371 |       readVector len i obj

372 |           = if len == i

373 |                then []

374 |                else unsafeVectorRef obj i :: readVector len (i + 1) obj

380 | quoteObj : {auto c : Ref Ctxt Defs} ->

381 |            SObj vars -> Core (Term vars)

382 | quoteObj (MkSObj val schEnv)

383 |     = do i <- newRef Sym 0

384 |          quote' {outer = Scope.empty} schEnv val

387 |   snfVector : Ref Ctxt Defs =>

388 |               SchVars vars ->

389 |               Integer -> List ForeignObj ->

390 |               Core (SNF vars)

391 |   snfVector svs (-2) [_, fname_in, args_in] -- Blocked application

392 |       = quoteOrInvalidS fname_in $ \ fname => do

393 |            let args = map (snf' svs) (getArgList args_in)

394 |            pure (SApp emptyFC (SRef Func fname) args)

395 |   snfVector svs (-10) [_, fn_arity, args_in] -- Block meta app

396 |       = quoteOrInvalidS {x = (Name, Integer)} fn_arity $ \ (fname, arity_in) => do

397 |            let arity : Nat = cast arity_in

398 |            let args = map (snf' svs) (getArgList args_in)

399 |            defs <- get Ctxt

400 |            fnameF <- toFullNames fname

401 |            (idx, _) <- getPosition fnameF (gamma defs)

402 |            pure (SApp emptyFC (SMeta fnameF idx (take arity args))

403 |                                (drop arity args))

404 |   snfVector svs (-11) [_, loc_in, args_in] -- Blocked local var application

405 |       = do SApp fc loc args <- snf' svs loc_in

406 |                 | _ => invalidS

407 |            let args' = map (snf' svs) (getArgList args_in)

408 |            pure (SApp fc loc (args ++ args'))

409 |   snfVector svs (-1) (_ :: strtag :: cname_in :: fc_in :: args_in) -- TyCon

410 |       = quoteOrInvalidS cname_in $ \ cname => do

411 |            let fc = quoteFC fc_in

412 |            let args = map (snf' svs) args_in

413 |            pure (STCon fc cname (length args) args)

414 |   snfVector svs (-15) [_, r_in, ty_in] -- Delayed

415 |       = do ty <- snf' svs ty_in

416 |            let r = quoteLazyReason r_in

417 |            pure (SDelayed emptyFC r ty)

418 |   snfVector svs (-4) [_, r_in, fc_in, ty_in, tm_in] -- Delay

419 |       = do let Procedure tmproc = decodeObj tm_in

420 |                 | _ => invalidS

421 |            let Procedure typroc = decodeObj ty_in

422 |                 | _ => invalidS

423 |            -- Block further reduction under tm_in

424 |            let tm = do Just _ <- coreLift $ evalSchemeStr "(ct-setBlockAll #t)"

425 |                             | Nothing => invalidS

426 |                        res <- snf' svs (unsafeForce tmproc)

427 |                        Just _ <- coreLift $ evalSchemeStr "(ct-setBlockAll #f)"

428 |                             | Nothing => invalidS

429 |                        pure res

430 |            let ty = snf' svs (unsafeForce typroc)

431 |            let fc = quoteFC fc_in

432 |            let r = quoteLazyReason r_in

433 |            pure (SDelay fc r ty tm)

434 |   snfVector svs (-5) [_, r_in, fc_in, tm_in] -- Force

435 |       = do -- The thing we were trying to force was stuck. Corresponding to

436 |            -- Core.Normalise, reduce it anyway here (so no ct-blockAll like above)

437 |            tm <- snf' svs tm_in

438 |            let fc = quoteFC fc_in

439 |            let r = quoteLazyReason r_in

440 |            pure (SForce fc r tm)

441 |   snfVector svs (-6) [_, fc_in, imp_in] -- Erased

442 |       = do let fc = quoteFC fc_in

443 |            imp <- quoteWhyErased (snf' svs) imp_in

444 |            pure (SErased fc imp)

445 |   snfVector svs (-7) [_, fc_in, u_in] -- Type

446 |       = do let fc = quoteFC fc_in

447 |            let u = quoteTypeLevel u_in

448 |            pure (SType fc u)

449 |   snfVector svs (-8) [_, proc_in, rig_in, pi_in, ty_in, name_in] -- Lambda

450 |       = do let name = quoteBinderName name_in

451 |            let rig = quoteRigCount rig_in

452 |            ty <- snf' svs ty_in

453 |            pi <- snfPiInfo svs pi_in

454 |            snfBinder svs Lam proc_in rig pi ty name

455 |   snfVector svs (-3) [_, proc_in, rig_in, pi_in, ty_in, name_in] -- Pi

456 |       = do let name = quoteBinderName name_in

457 |            let rig = quoteRigCount rig_in

458 |            ty <- snf' svs ty_in

459 |            pi <- snfPiInfo svs pi_in

460 |            snfBinder svs Pi proc_in rig pi ty name

461 |   snfVector svs (-12) [_, proc_in, rig_in, pi_in, ty_in, name_in] -- PVar

462 |       = do let name = quoteBinderName name_in

463 |            let rig = quoteRigCount rig_in

464 |            ty <- snf' svs ty_in

465 |            pi <- snfPiInfo svs pi_in

466 |            snfBinder svs PVar proc_in rig pi ty name

467 |   snfVector svs (-13) [_, proc_in, rig_in, ty_in, name_in] -- PVTy

468 |       = do let name = quoteBinderName name_in

469 |            let rig = quoteRigCount rig_in

470 |            ty <- snf' svs ty_in

471 |            snfBinder svs (\fc, r, p, t => PVTy fc r t) proc_in rig Explicit ty name

472 |   snfVector svs (-14) [_, proc_in, rig_in, val_in, ty_in, name_in] -- PLet

473 |       = do let name = quoteBinderName name_in

474 |            let rig = quoteRigCount rig_in

475 |            ty <- snf' svs ty_in

476 |            val <- snf' svs val_in

477 |            snfPLet svs proc_in rig val ty name

478 |   snfVector svs (-9) [_, blocked, _] -- Blocked top level lambda

479 |       = snf' svs blocked

481 |   -- constants here

482 |   snfVector svs (-100) [_, x]

483 |       = quoteOrInvalidS x $ \ x' => pure $ SPrimVal emptyFC (I x')

484 |   snfVector svs (-101) [_, x]

485 |       = quoteOrInvalidS x $ \ x' => pure $ SPrimVal emptyFC (I8 x')

486 |   snfVector svs (-102) [_, x]

487 |       = quoteOrInvalidS x $ \ x' => pure $ SPrimVal emptyFC (I16 x')

488 |   snfVector svs (-103) [_, x]

489 |       = quoteOrInvalidS x $ \ x' => pure $ SPrimVal emptyFC (I32 x')

490 |   snfVector svs (-104) [_, x]

491 |       = quoteOrInvalidS x $ \ x' => pure $ SPrimVal emptyFC (I64 x')

492 |   snfVector svs (-105) [_, x]

493 |       = quoteOrInvalidS x $ \ x' => pure $ SPrimVal emptyFC (BI x')

494 |   snfVector svs (-106) [_, x]

495 |       = quoteOrInvalidS x $ \ x' => pure $ SPrimVal emptyFC (B8 x')

496 |   snfVector svs (-107) [_, x]

497 |       = quoteOrInvalidS x $ \ x' => pure $ SPrimVal emptyFC (B16 x')

498 |   snfVector svs (-108) [_, x]

499 |       = quoteOrInvalidS x $ \ x' => pure $ SPrimVal emptyFC (B32 x')

500 |   snfVector svs (-109) [_, x]

501 |       = quoteOrInvalidS x $ \ x' => pure $ SPrimVal emptyFC (B64 x')

503 |   snfVector svs tag (_ :: cname_in :: fc_in :: args_in) -- DataCon

504 |       = if tag >= 0

505 |            then quoteOrInvalidS cname_in $ \ cname => do

506 |              let fc = quoteFC fc_in

507 |              let args = map (snf' svs) args_in

508 |              pure (SDCon fc cname (cast tag) (length args) args)

509 |            else invalidS

510 |   snfVector _ _ _ = invalidS

512 |   snfPiInfo : Ref Ctxt Defs =>

513 |               SchVars vars ->

514 |               ForeignObj ->

515 |               Core (PiInfo (SNF vars))

516 |   snfPiInfo svs obj

517 |       = if isInteger obj

518 |            then case unsafeGetInteger obj of

519 |                      0 => pure Implicit

520 |                      1 => pure Explicit

521 |                      2 => pure AutoImplicit

522 |                      _ => pure Explicit

523 |            else if isBox obj

524 |                    then do t' <- snf' svs (unsafeUnbox obj)

525 |                            pure (DefImplicit t')

526 |            else pure Explicit

528 |   snfBinder : Ref Ctxt Defs =>

529 |               SchVars vars ->

530 |               (forall ty . FC -> RigCount -> PiInfo ty -> ty -> Binder ty) ->

531 |               ForeignObj -> -- body of binder, represented as a function

532 |               RigCount ->

533 |               PiInfo (SNF vars) ->

534 |               SNF vars -> -- decoded type

535 |               Name -> -- bound name

536 |               Core (SNF vars)

537 |   snfBinder svs binder proc_in r pi ty name

538 |       = do let Procedure proc = decodeObj proc_in

539 |                     | _ => invalidS

540 |            pure (SBind emptyFC name (binder emptyFC r pi ty)

541 |                        (\tm => do let MkSObj arg _ = tm

542 |                                   let sc = unsafeApply proc arg

543 |                                   snf' svs sc))

545 |   snfPLet : Ref Ctxt Defs =>

546 |             SchVars vars ->

547 |             ForeignObj -> -- body of binder, represented as a function

548 |             RigCount ->

549 |             SNF vars -> -- decoded type

550 |             SNF vars -> -- decoded value

551 |             Name -> -- bound name

552 |             Core (SNF vars)

553 |   snfPLet svs proc_in r val ty name

554 |       = do let Procedure proc = decodeObj proc_in

555 |                     | _ => invalidS

556 |            pure (SBind emptyFC name (PLet emptyFC r val ty)

557 |                        (\tm => do let MkSObj arg _ = tm

558 |                                   let sc = unsafeApply proc arg

559 |                                   snf' svs sc))

561 |   snf' : Ref Ctxt Defs =>

562 |          SchVars vars -> ForeignObj ->

563 |          Core (SNF vars)

564 |   snf' svs obj

565 |       = if isVector obj

566 |            then snfVector svs (unsafeGetInteger (unsafeVectorRef obj 0))

567 |                               (unsafeVectorToList obj)

568 |            else if isProcedure obj then snfBinder svs Lam obj top

569 |                                                  Explicit

570 |                                                  (SErased emptyFC Placeholder)

571 |                                                  (UN (Basic "x"))

572 |            else if isSymbol obj then pure $ findName svs (unsafeReadSymbol obj)

573 |            else if isFloat obj then pure $ SPrimVal emptyFC (Db (unsafeGetFloat obj))

574 |            else if isInteger obj then pure $ SPrimVal emptyFC (I (cast (unsafeGetInteger obj)))

575 |            else if isString obj then pure $ SPrimVal emptyFC (Str (unsafeGetString obj))

576 |            else if isChar obj then pure $ SPrimVal emptyFC (Ch (unsafeGetChar obj))

577 |            else invalidS

578 |     where

579 |       findName : forall vars . SchVars vars -> String -> SNF vars

580 |       findName [] n = SApp emptyFC (SRef Func (UN (Basic n))) []

581 |       findName (x :: xs) n

582 |           = if getName x == n

583 |                then SApp emptyFC (SLocal _ First) []

584 |                else let SApp fc (SLocal _ p) args = findName xs n

585 |                            | _ => SApp emptyFC (SRef Func (UN (Basic n))) [] in

586 |                         SApp fc (SLocal _ (Later p)) []

588 |       readVector : Integer -> Integer -> ForeignObj -> List ForeignObj

589 |       readVector len i obj

590 |           = if len == i

591 |                then []

592 |                else unsafeVectorRef obj i :: readVector len (i + 1) obj

595 | toSNF : Ref Ctxt Defs =>

596 |         SObj vars -> Core (SNF vars)

597 | toSNF (MkSObj val schEnv) = snf' schEnv val