0 | module Core.SchemeEval.Compile

 13 | import Core.Case.CaseTree

 14 | import Core.Context

 15 | import Core.Directory

 16 | import Core.SchemeEval.Builtins

 17 | import Core.SchemeEval.ToScheme

 19 | import Data.List.Quantifiers

 21 | import Libraries.Utils.Scheme

 22 | import System.Info

 24 | import Libraries.Data.WithDefault

 26 | schString : String -> String

 27 | schString s = concatMap okchar (unpack s)

 28 |   where

 29 |     okchar : Char -> String

 30 |     okchar c = if isAlphaNum c || c =='_'

 31 |                   then cast c

 32 |                   else "C-" ++ show (cast {to=Int} c)

 34 | schVarUN : UserName -> String

 35 | schVarUN (Basic n) = schString n

 36 | schVarUN (Field n) = "rf--" ++ schString n

 37 | schVarUN Underscore = "_US_"

 39 | schVarName : Name -> String

 40 | schVarName (NS ns (UN n))

 41 |    = schString (showNSWithSep "-" ns) ++ "-" ++ schVarUN n

 42 | schVarName (NS ns n) = schString (showNSWithSep "-" ns) ++ "-" ++ schVarName n

 43 | schVarName (UN n) = "u--" ++ schVarUN n

 44 | schVarName (MN n i) = schString n ++ "-" ++ show i

 45 | schVarName (PV n d) = "pat--" ++ schVarName n

 46 | schVarName (DN _ n) = schVarName n

 47 | schVarName (Nested (i, x) n) = "n--" ++ show i ++ "-" ++ show x ++ "-" ++ schVarName n

 48 | schVarName (CaseBlock x y) = "case--" ++ schString x ++ "-" ++ show y

 49 | schVarName (WithBlock x y) = "with--" ++ schString x ++ "-" ++ show y

 50 | schVarName (Resolved i) = "fn--" ++ show i

 52 | schName : Name -> String

 53 | schName n = "ct-" ++ schVarName n

 56 | data Sym : Type where

 59 | nextName : Ref Sym Integer => Core Integer

 61 |     = do n <- get Sym

 62 |          put Sym (n + 1)

 63 |          pure n

 65 | public export

 66 | data SVar = Bound String | Free String

 68 | Show SVar where

 69 |   show (Bound x) = x

 70 |   show (Free x) = "'" ++ x

 73 | getName : SVar -> String

 74 | getName (Bound x) = x

 75 | getName (Free x) = x

 77 | public export

 78 | SchVars : Scoped

 79 | SchVars = All (\_ => SVar)

 81 | Show (SchVars ns) where

 82 |   show xs = show (toList xs)

 83 |     where

 84 |       -- TODO move to Data.List.Quantifiers

 85 |       toList : forall ns . SchVars ns -> List String

 86 |       toList [] = []

 87 |       toList (Bound x :: xs) = x :: toList xs

 88 |       toList (Free x :: xs) = "'x" :: toList xs

 90 | getSchVar : {idx : _} -> (0 _ : IsVar n idx vars) -> SchVars vars -> String

 91 | getSchVar First (Bound x :: xs) = x

 92 | getSchVar First (Free x :: xs) = "'" ++ x

 93 | getSchVar (Later p) (x :: xs) = getSchVar p xs

123 | blockedAppWith : Name -> List (SchemeObj Write) -> SchemeObj Write

124 | blockedAppWith n args = Vector (-2) [toScheme n, vars args]

125 |   where

126 |     vars : List (SchemeObj Write) -> SchemeObj Write

127 |     vars [] = Null

128 |     vars (x :: xs) = Cons x (vars xs)

130 | blockedMetaApp : Name -> SchemeObj Write

131 | blockedMetaApp n

132 |     = Lambda ["arity-0"] (Vector (-10) [Cons (toScheme n) (Var "arity-0"),

133 |                                         Null])

135 | unload : SchemeObj Write -> List (SchemeObj Write) -> SchemeObj Write

136 | unload f [] = f

137 | unload f (a :: as) = unload (Apply (Var "ct-app") [f, a]) as

139 | compileConstant : FC -> Constant -> SchemeObj Write

140 | compileConstant fc (I x) = Vector (-100) [IntegerVal (cast x)]

141 | compileConstant fc (I8 x) = Vector (-101) [IntegerVal (cast x)]

142 | compileConstant fc (I16 x) = Vector (-102) [IntegerVal (cast x)]

143 | compileConstant fc (I32 x) = Vector (-103) [IntegerVal (cast x)]

144 | compileConstant fc (I64 x) = Vector (-104) [IntegerVal (cast x)]

145 | compileConstant fc (BI x) = Vector (-105) [IntegerVal x]

146 | compileConstant fc (B8 x) = Vector (-106) [IntegerVal (cast x)]

147 | compileConstant fc (B16 x) = Vector (-107) [IntegerVal (cast x)]

148 | compileConstant fc (B32 x) = Vector (-108) [IntegerVal (cast x)]

149 | compileConstant fc (B64 x) = Vector (-109) [IntegerVal (cast x)]

150 | compileConstant fc (Str x) = StringVal x

151 | compileConstant fc (Ch x) = CharVal x

152 | compileConstant fc (Db x) = FloatVal x

153 | compileConstant fc (PrT t) -- Constant types get compiled as TyCon names, for matching purposes

154 |     = Vector (-1) [IntegerVal (cast (primTypeTag t)),

155 |                    StringVal (show t),

156 |                    toScheme (UN (Basic (show t))),

157 |                    toScheme fc]

158 | compileConstant fc WorldVal = Null

160 | compileStk : Ref Sym Integer =>

161 |              {auto c : Ref Ctxt Defs} ->

162 |              SchVars vars -> List (SchemeObj Write) -> Term vars ->

163 |              Core (SchemeObj Write)

165 | compilePiInfo : Ref Sym Integer =>

166 |                 {auto c : Ref Ctxt Defs} ->

167 |                 SchVars vars -> PiInfo (Term vars) ->

168 |                 Core (PiInfo (SchemeObj Write))

169 | compilePiInfo svs Implicit = pure Implicit

170 | compilePiInfo svs Explicit = pure Explicit

171 | compilePiInfo svs AutoImplicit = pure AutoImplicit

172 | compilePiInfo svs (DefImplicit t)

173 |     = do t' <- compileStk svs [] t

174 |          pure (DefImplicit t')

176 | compileWhyErased : Ref Sym Integer =>

177 |                 {auto c : Ref Ctxt Defs} ->

178 |                 SchVars vars -> List (SchemeObj Write) -> WhyErased (Term vars) ->

179 |                 Core (WhyErased (SchemeObj Write))

180 | compileWhyErased svs stk Impossible = pure Impossible

181 | compileWhyErased svs stk Placeholder = pure Placeholder

182 | compileWhyErased svs stk (Dotted t)

183 |     = do t' <- compileStk svs stk t

184 |          pure (Dotted t')

186 | compileStk svs stk (Local fc isLet idx p)

187 |     = pure $ unload (Var (getSchVar p svs)) stk

190 | compileStk svs stk (Ref fc Bound name)

191 |     = pure $ unload (Symbol (show name)) stk

192 | compileStk svs stk (Ref fc (DataCon t a) name)

193 |     = if length stk == a -- inline it if it's fully applied

194 |          then pure $ Vector (cast t)

195 |                        (toScheme !(toResolvedNames name) ::

196 |                         toScheme fc :: stk)

197 |          else pure $ unload (Apply (Var (schName name)) []) stk

198 | compileStk svs stk (Ref fc (TyCon a) name)

199 |     = if length stk == a -- inline it if it's fully applied

200 |          then pure $ Vector (-1)

201 |                        (StringVal (show name) ::

202 |                         toScheme !(toResolvedNames name) ::

203 |                         toScheme fc :: stk)

204 |          else pure $ unload (Apply (Var (schName name)) []) stk

205 | compileStk svs stk (Ref fc x name)

206 |     = pure $ unload (Apply (Var (schName name)) []) stk

207 | compileStk svs stk (Meta fc name i xs)

208 |     = do xs' <- traverse (compileStk svs stk) xs

209 |          -- we encode the arity as first argument to the hole definition, which

210 |          -- helps in readback, so we have to apply the hole function to the

211 |          -- length of xs to be able to restore the Meta properly

212 |          pure $ unload (Apply (Var (schName name)) [])

213 |                        (IntegerVal (cast (length xs)) :: stk ++ xs')

214 | compileStk svs stk (Bind fc x (Let _ _ val _) scope)

215 |     = do i <- nextName

216 |          let x' = schVarName x ++ "-" ++ show i

217 |          val' <- compileStk svs [] val

218 |          sc' <- compileStk (Bound x' :: svs) [] scope

219 |          pure $ unload (Let x' val' sc') stk

220 | compileStk svs stk (Bind fc x (Pi _ rig p ty) scope)

221 |     = do i <- nextName

222 |          let x' = schVarName x ++ "-" ++ show i

223 |          ty' <- compileStk svs [] ty

224 |          sc' <- compileStk (Bound x' :: svs) [] scope

225 |          p' <- compilePiInfo svs p

226 |          pure $ Vector (-3) [Lambda [x'] sc', toScheme rig, toSchemePi p',

227 |                                               ty', toScheme x]

228 | compileStk svs stk (Bind fc x (PVar _ rig p ty) scope)

229 |     = do i <- nextName

230 |          let x' = schVarName x ++ "-" ++ show i

231 |          ty' <- compileStk svs [] ty

232 |          sc' <- compileStk (Bound x' :: svs) [] scope

233 |          p' <- compilePiInfo svs p

234 |          pure $ Vector (-12) [Lambda [x'] sc', toScheme rig, toSchemePi p',

235 |                                                ty', toScheme x]

236 | compileStk svs stk (Bind fc x (PVTy _ rig ty) scope)

237 |     = do i <- nextName

238 |          let x' = schVarName x ++ "-" ++ show i

239 |          ty' <- compileStk svs [] ty

240 |          sc' <- compileStk (Bound x' :: svs) [] scope

241 |          pure $ Vector (-13) [Lambda [x'] sc', toScheme rig, ty', toScheme x]

242 | compileStk svs stk (Bind fc x (PLet _ rig val ty) scope) -- we only see this on LHS

243 |     = do i <- nextName

244 |          let x' = schVarName x ++ "-" ++ show i

245 |          val' <- compileStk svs [] val

246 |          ty' <- compileStk svs [] ty

247 |          sc' <- compileStk (Bound x' :: svs) [] scope

248 |          pure $ Vector (-14) [Lambda [x'] sc', toScheme rig, val', ty', toScheme x]

249 | compileStk svs [] (Bind fc x (Lam _ rig p ty) scope)

250 |     = do i <- nextName

251 |          let x' = schVarName x ++ "-" ++ show i

252 |          ty' <- compileStk svs [] ty

253 |          sc' <- compileStk (Bound x' :: svs) [] scope

254 |          p' <- compilePiInfo svs p

255 |          pure $ Vector (-8) [Lambda [x'] sc', toScheme rig, toSchemePi p',

256 |                                               ty', toScheme x]

257 | compileStk svs (s :: stk) (Bind fc x (Lam {}) scope)

258 |     = do i <- nextName

259 |          let x' = schVarName x ++ "-" ++ show i

260 |          sc' <- compileStk (Bound x' :: svs) stk scope

261 |          pure $ Apply (Lambda [x'] sc') [s]

262 | compileStk svs stk (App fc fn arg)

263 |     = compileStk svs (!(compileStk svs [] arg) :: stk) fn

266 | compileStk svs stk (As fc x as pat) = compileStk svs stk pat

267 | compileStk svs stk (TDelayed fc r ty)

268 |     = do ty' <- compileStk svs stk ty

269 |          pure $ Vector (-15) [toScheme r, ty']

270 | compileStk svs stk (TDelay fc r ty arg)

271 |     = do ty' <- compileStk svs [] ty

272 |          arg' <- compileStk svs [] arg

273 |          pure $ Vector (-4) [toScheme r, toScheme fc,

274 |                              Lambda [] ty', Lambda [] arg']

275 | compileStk svs stk (TForce fc x tm)

276 |     = do tm' <- compileStk svs [] tm

277 |          pure $ Apply (Var "ct-doForce")

278 |                       [tm',

279 |                       Vector (-5) [toScheme x, toScheme fc, Lambda [] tm']]

280 | compileStk svs stk (PrimVal fc c) = pure $ compileConstant fc c

281 | compileStk svs stk (Erased fc why)

282 |   = do why' <- compileWhyErased svs stk why

283 |        pure $ Vector (-6) [toScheme fc, toSchemeWhy why']

284 | compileStk svs stk (TType fc u) = pure $ Vector (-7) [toScheme fc, toScheme u]

287 | compile : Ref Sym Integer =>

288 |           {auto c : Ref Ctxt Defs} ->

289 |           SchVars vars -> Term vars -> Core (SchemeObj Write)

290 | compile vars tm = compileStk vars [] tm

292 | getArgName : Ref Sym Integer =>

293 |              Core Name

295 |     = do i <- nextName

296 |          pure (MN "carg" (cast i))

298 | extend : Ref Sym Integer =>

299 |          (args : List Name) -> SchVars vars ->

300 |          Core (List Name, SchVars (args ++ vars))

301 | extend [] svs = pure ([], svs)

302 | extend (arg :: args) svs

303 |     = do n <- getArgName

304 |          (args', svs') <- extend args svs

305 |          pure (n :: args', Bound (schVarName n) :: svs')

307 | compileCase : Ref Sym Integer =>

308 |               {auto c : Ref Ctxt Defs} ->

309 |               (blocked : SchemeObj Write) ->

310 |               SchVars vars -> CaseTree vars -> Core (SchemeObj Write)

311 | compileCase blk svs (Case idx p scTy xs)

312 |     = case !(caseType xs) of

313 |            CON => toSchemeConCases idx p xs

314 |            TYCON => toSchemeTyConCases idx p xs

315 |            DELAY => toSchemeDelayCases idx p xs

316 |            CONST => toSchemeConstCases idx p xs

317 |   where

318 |     data CaseType = CON | TYCON | DELAY | CONST

320 |     caseType : List (CaseAlt vs) -> Core CaseType

321 |     caseType [] = pure CON

322 |     caseType (ConCase x tag args y :: xs)

323 |         = do defs <- get Ctxt

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

325 |                   | Nothing => pure TYCON -- primitive type match

326 |              case definition gdef of

327 |                   DCon {} => pure CON

328 |                   TCon {} => pure TYCON

329 |                   _ => pure CON -- or maybe throw?

330 |     caseType (DelayCase ty arg x :: xs) = pure DELAY

331 |     caseType (ConstCase x y :: xs) = pure CONST

332 |     caseType (DefaultCase x :: xs) = caseType xs

334 |     makeDefault : List (CaseAlt vars) -> Core (SchemeObj Write)

335 |     makeDefault [] = pure blk

336 |     makeDefault (DefaultCase sc :: xs) = compileCase blk svs sc

337 |     makeDefault (_ :: xs) = makeDefault xs

339 |     toSchemeConCases : (idx : Nat) -> (0 p : IsVar n idx vars) ->

340 |                        List (CaseAlt vars) -> Core (SchemeObj Write)

341 |     toSchemeConCases idx p alts

342 |         = do let var = getSchVar p svs

343 |              alts' <- traverse (makeAlt var) alts

344 |              let caseblock

345 |                     = Case (Apply (Var "vector-ref") [Var var, IntegerVal 0])

346 |                            (mapMaybe id alts')

347 |                            (Just !(makeDefault alts))

348 |              pure $ If (Apply (Var "ct-isDataCon") [Var var])

349 |                        caseblock

350 |                        blk

351 |       where

352 |         project : Int -> String -> List Name ->

353 |                   SchemeObj Write -> SchemeObj Write

354 |         project i var [] body = body

355 |         project i var (n :: ns) body

356 |             = Let (schVarName n)

357 |                   (Apply (Var "vector-ref") [Var var, IntegerVal (cast i)])

358 |                   (project (i + 1) var ns body)

360 |         bindArgs : String -> (args : List Name) -> CaseTree (args ++ vars) ->

361 |                    Core (SchemeObj Write)

362 |         bindArgs var args sc

363 |             = do (bind, svs') <- extend args svs

364 |                  project 3 var bind <$> compileCase blk svs' sc

366 |         makeAlt : String -> CaseAlt vars ->

367 |                   Core (Maybe (SchemeObj Write, SchemeObj Write))

368 |         makeAlt var (ConCase n t args sc)

369 |             = pure $ Just (IntegerVal (cast t), !(bindArgs var args sc))

370 |         -- TODO: Matching on types, including ->

371 |         makeAlt var _ = pure Nothing

373 |     toSchemeTyConCases : (idx : Nat) -> (0 p : IsVar n idx vars) ->

374 |                          List (CaseAlt vars) -> Core (SchemeObj Write)

375 |     toSchemeTyConCases idx p alts

376 |         = do let var = getSchVar p svs

377 |              alts' <- traverse (makeAlt var) alts

378 |              caseblock <- addPiMatch var alts

379 |                       -- work on the name, so the 2nd arg

380 |                             (Case (Apply (Var "vector-ref") [Var var, IntegerVal 2])

381 |                                (mapMaybe id alts')

382 |                                (Just !(makeDefault alts)))

383 |              pure $ If (Apply (Var "ct-isTypeMatchable") [Var var])

384 |                        caseblock

385 |                        blk

386 |       where

387 |         project : Int -> String -> List Name ->

388 |                   SchemeObj Write -> SchemeObj Write

389 |         project i var [] body = body

390 |         project i var (n :: ns) body

391 |             = Let (schVarName n)

392 |                   (Apply (Var "vector-ref") [Var var, IntegerVal (cast i)])

393 |                   (project (i + 1) var ns body)

395 |         bindArgs : String -> (args : List Name) -> CaseTree (args ++ vars) ->

396 |                    Core (SchemeObj Write)

397 |         bindArgs var args sc

398 |             = do (bind, svs') <- extend args svs

399 |                  project 5 var bind <$> compileCase blk svs' sc

401 |         makeAlt : String -> CaseAlt vars ->

402 |                   Core (Maybe (SchemeObj Write, SchemeObj Write))

403 |         makeAlt var (ConCase (UN (Basic "->")) t [_, _] sc)

404 |             = pure Nothing -- do this in 'addPiMatch' below, since the

405 |                            -- representation is different

406 |         makeAlt var (ConCase n t args sc)

407 |             = pure $ Just (StringVal (show n), !(bindArgs var args sc))

408 |         makeAlt var _ = pure Nothing

410 |         addPiMatch : String -> List (CaseAlt vars) -> SchemeObj Write ->

411 |                      Core (SchemeObj Write)

412 |         addPiMatch var [] def = pure def

413 |         -- t is a function type, and conveniently the scope of a pi

414 |         -- binding is represented as a function. Lucky us! So we just need

415 |         -- to extract it then evaluate the scope

416 |         addPiMatch var (ConCase (UN (Basic "->")) _ [s, t] sc :: _) def

417 |             = do sn <- getArgName

418 |                  tn <- getArgName

419 |                  let svs' = Bound (schVarName sn) ::

420 |                               Bound (schVarName tn) :: svs

421 |                  sc' <- compileCase blk svs' sc

422 |                  pure $ If (Apply (Var "ct-isPi") [Var var])

423 |                            (Let (schVarName sn) (Apply (Var "vector-ref") [Var var, IntegerVal 4]) $

424 |                             Let (schVarName tn) (Apply (Var "vector-ref") [Var var, IntegerVal 1]) $

425 |                             sc')

426 |                            def

427 |         addPiMatch var (x :: xs) def = addPiMatch var xs def

429 |     toSchemeConstCases : (idx : Nat) -> (0 p : IsVar n idx vars) ->

430 |                          List (CaseAlt vars) -> Core (SchemeObj Write)

431 |     toSchemeConstCases x p alts

432 |         = do let var = getSchVar p svs

433 |              alts' <- traverse (makeAlt var) alts

434 |              let caseblock

435 |                     = Cond (mapMaybe id alts')

436 |                            (Just !(makeDefault alts))

437 |              pure $ If (Apply (Var "ct-isConstant") [Var var])

438 |                        caseblock

439 |                        blk

440 |      where

441 |         makeAlt : String -> CaseAlt vars ->

442 |                   Core (Maybe (SchemeObj Write, SchemeObj Write))

443 |         makeAlt var (ConstCase c sc)

444 |             = do sc' <- compileCase blk svs sc

445 |                  pure (Just (Apply (Var "equal?")

446 |                                [Var var, compileConstant emptyFC c], sc'))

447 |         makeAlt var _ = pure Nothing

449 |     toSchemeDelayCases : (idx : Nat) -> (0 p : IsVar n idx vars) ->

450 |                          List (CaseAlt vars) -> Core (SchemeObj Write)

451 |     -- there will only ever be one, or a default case

452 |     toSchemeDelayCases idx p (DelayCase ty arg sc :: rest)

453 |         = do let var = getSchVar p svs

454 |              tyn <- getArgName

455 |              argn <- getArgName

456 |              let svs' = Bound (schVarName tyn) ::

457 |                           Bound (schVarName argn) :: svs

458 |              sc' <- compileCase blk svs' sc

459 |              pure $ If (Apply (Var "ct-isDelay") [Var var])

460 |                        (Let (schVarName tyn)

461 |                            (Apply (Apply (Var "vector-ref") [Var var, IntegerVal 3]) []) $

462 |                         Let (schVarName argn)

463 |                            (Apply (Apply (Var "vector-ref") [Var var, IntegerVal 4]) []) $

464 |                          sc')

465 |                        blk

466 |     toSchemeDelayCases idx p (_ :: rest) = toSchemeDelayCases idx p rest

467 |     toSchemeDelayCases idx p _ = pure Null

469 | compileCase blk vars (STerm _ tm) = compile vars tm

470 | compileCase blk vars _ = pure blk

472 | varObjs : SchVars ns -> List (SchemeObj Write)

473 | varObjs [] = []

474 | varObjs (x :: xs) = Var (show x) :: varObjs xs

476 | mkArgs : (ns : Scope) -> Core (SchVars ns)

477 | mkArgs [] = pure []

478 | mkArgs (x :: xs)

479 |     = pure $ Bound (schVarName x) :: !(mkArgs xs)

481 | bindArgs : Name ->

482 |            (todo : SchVars ns) ->

483 |            (done : List (SchemeObj Write)) ->

484 |            SchemeObj Write -> SchemeObj Write

485 | bindArgs n [] done body = body

486 | bindArgs n (x :: xs) done body

487 |     = Vector (-9) [blockedAppWith n (reverse done),

488 |                    Lambda [show x]

489 |                       (bindArgs n xs (Var (show x) :: done) body)]

491 | compileBody : {auto c : Ref Ctxt Defs} ->

492 |               Bool -> -- okay to reduce (if False, block)

493 |               Name -> Def -> Core (SchemeObj Write)

494 | compileBody _ n None = pure $ blockedAppWith n []

495 | compileBody redok n (PMDef pminfo args treeCT treeRT pats)

496 |     = do i <- newRef Sym 0

497 |          argvs <- mkArgs args

498 |          let blk = blockedAppWith n (varObjs argvs)

499 |          body <- compileCase blk argvs treeCT

500 |          let body' = if redok

501 |                         then If (Apply (Var "ct-isBlockAll") []) blk body

502 |                         else blk

503 |          -- If it arose from a hole, we need to take an extra argument for

504 |          -- the arity since that's what Meta gets applied to

505 |          case holeInfo pminfo of

506 |               NotHole => pure (bindArgs n argvs [] body')

507 |               SolvedHole _ => pure (Lambda ["h-0"] (bindArgs n argvs [] body'))

508 | compileBody _ n (ExternDef arity) = pure $ blockedAppWith n []

509 | compileBody _ n (ForeignDef arity xs) = pure $ blockedAppWith n []

510 | compileBody _ n (Builtin x) = pure $ compileBuiltin n x

511 | compileBody _ n (DCon tag Z newtypeArg)

512 |     = pure $ Vector (cast tag) [toScheme !(toResolvedNames n), toScheme emptyFC]

513 | compileBody _ n (DCon tag arity newtypeArg)

514 |     = do let args = mkArgNs 0 arity

515 |          argvs <- mkArgs args

516 |          let body

517 |                = Vector (cast tag)

518 |                         (toScheme n :: toScheme emptyFC ::

519 |                              map (Var . schVarName) args)

520 |          pure (bindArgs n argvs [] body)

521 |   where

522 |     mkArgNs : Int -> Nat -> List Name

523 |     mkArgNs i Z = []

524 |     mkArgNs i (S k) = MN "arg" i :: mkArgNs (i+1) k

525 | compileBody _ n (TCon Z parampos detpos flags mutwith datacons detagabbleBy)

526 |     = pure $ Vector (-1) [StringVal (show n), toScheme n, toScheme emptyFC]

527 | compileBody _ n (TCon arity parampos detpos flags mutwith datacons detagabbleBy)

528 |     = do let args = mkArgNs 0 arity

529 |          argvs <- mkArgs args

530 |          let body

531 |                = Vector (-1)

532 |                         (StringVal (show n) ::

533 |                           toScheme n :: toScheme emptyFC ::

534 |                             map (Var . schVarName) args)

535 |          pure (bindArgs n argvs [] body)

536 |   where

537 |     mkArgNs : Int -> Nat -> List Name

538 |     mkArgNs i Z = []

539 |     mkArgNs i (S k) = MN "arg" i :: mkArgNs (i+1) k

540 | compileBody _ n (Hole numlocs x) = pure $ blockedMetaApp n

541 | compileBody _ n (BySearch x maxdepth defining) = pure $ blockedMetaApp n

542 | compileBody _ n (Guess guess envbind constraints) = pure $ blockedMetaApp n

543 | compileBody _ n ImpBind = pure $ blockedMetaApp n

544 | compileBody _ n (UniverseLevel _) = pure $ blockedMetaApp n

545 | compileBody _ n Delayed = pure $ blockedMetaApp n

548 | compileDef : {auto c : Ref Ctxt Defs} -> SchemeMode -> Name -> Core ()

549 | compileDef mode n_in

550 |     = do n <- toFullNames n_in -- this is handy for readability of generated names

551 |                      -- we used resolved names for blocked names, though, as

552 |                      -- that's a bit better for performance

553 |          defs <- get Ctxt

554 |          Just def <- lookupCtxtExact n (gamma defs)

555 |               | Nothing => throw (UndefinedName emptyFC n)

557 |          let True = case schemeExpr def of

558 |                          Nothing => True

559 |                          Just (cmode, def) => cmode /= mode

560 |                | _ => pure () -- already done

561 |          -- If we're in BlockExport mode, check whether the name is

562 |          -- available for reduction.

563 |          let redok = mode == EvalAll ||

564 |                        reducibleInAny (currentNS defs :: nestedNS defs)

565 |                                       (fullname def)

566 |                                       (collapseDefault $ visibility def)

567 |          -- 'n' is used in compileBody for generating names for readback,

568 |          -- and reading back resolved names is quicker because it's just

569 |          -- an integer

570 |          b <- compileBody redok !(toResolvedNames n) !(toFullNames (definition def))

571 |          let schdef = Define (schName n) b

573 |          -- Add the new definition to the current scheme runtime

574 |          Just obj <- coreLift $ evalSchemeObj schdef

575 |               | Nothing => throw (InternalError ("Compiling " ++ show n ++ " failed"))

577 |          -- Record that this one is done

578 |          ignore $ addDef n ({ schemeExpr := Just (mode, schdef) } def)

580 | initEvalWith : {auto c : Ref Ctxt Defs} ->

581 |                String -> Core Bool

582 | initEvalWith "chez"

583 |     = do defs <- get Ctxt

584 |          if defs.schemeEvalLoaded

585 |             then pure True

586 |             else

587 |              catch (do f <- readDataFile "chez/ct-support.ss"

588 |                        Just _ <- coreLift $ evalSchemeStr $ "(begin " ++ f ++ ")"

589 |                             | Nothing => pure False

590 |                        put Ctxt ({ schemeEvalLoaded := True } defs)

591 |                        pure True)

592 |                 (\err => pure False)

593 | initEvalWith "racket"

594 |     = do defs <- get Ctxt

595 |          if defs.schemeEvalLoaded

596 |             then pure True

597 |             else

598 |              catch (do f <- readDataFile "racket/ct-support.rkt"

599 |                        Just _ <- coreLift $ evalSchemeStr $ "(begin " ++ f ++ ")"

600 |                             | Nothing => pure False

601 |                        put Ctxt ({ schemeEvalLoaded := True } defs)

602 |                        pure True)

603 |                 (\err => do coreLift $ printLn err

604 |                             pure False)

605 | initEvalWith _ = pure False -- only works on Chez for now

613 | initialiseSchemeEval : {auto c : Ref Ctxt Defs} ->

614 |                        Core Bool

615 | initialiseSchemeEval = initEvalWith codegen