0 | module Compiler.CompileExpr

  2 | import Compiler.Opts.Constructor

  3 | import Core.Case.CaseTree

  4 | import public Core.CompileExpr

  5 | import Core.Context.Log

  6 | import Core.Env

  7 | import Core.Normalise

  8 | import Core.Options

  9 | import Core.Value

 11 | import Data.List.HasLength

 12 | import Data.Vect

 14 | import Libraries.Data.NatSet

 15 | import Libraries.Data.List.SizeOf

 17 | %default covering

 19 | data Args

 20 |     = NewTypeBy Nat Nat

 21 |     | EraseArgs Nat NatSet

 22 |     | Arity Nat

 26 | numArgs : Defs -> Term vars -> Core Args

 27 | numArgs defs (Ref _ (TyCon arity) n) = pure (Arity arity)

 28 | numArgs defs (Ref _ _ n)

 29 |     = do Just gdef <- lookupCtxtExact n (gamma defs)

 30 |               | Nothing => pure (Arity 0)

 31 |          case definition gdef of

 32 |            DCon _ arity Nothing => pure (EraseArgs arity (eraseArgs gdef))

 33 |            DCon _ arity (Just (_, pos)) => pure (NewTypeBy arity pos)

 34 |            PMDef _ args _ _ _ => pure (EraseArgs (length args) (eraseArgs gdef))

 35 |            ExternDef arity => pure (Arity arity)

 36 |            ForeignDef arity _ => pure (Arity arity)

 37 |            Builtin {arity} f => pure (Arity arity)

 38 |            _ => pure (Arity 0)

 39 | numArgs _ tm = pure (Arity 0)

 41 | weakenVar : Var ns -> Var (a :: ns)

 42 | weakenVar (MkVar p) = (MkVar (Later p))

 44 | etaExpand : Int -> Nat -> CExp vars -> List (Var vars) -> CExp vars

 45 | etaExpand i Z exp args = mkApp exp (map (mkLocal (getFC exp)) (reverse args))

 46 |   where

 47 |     mkLocal : FC -> (Var vars) -> CExp vars

 48 |     mkLocal fc (MkVar p) = CLocal fc p

 50 |     mkApp : CExp vars -> List (CExp vars) -> CExp vars

 51 |     mkApp tm [] = tm

 52 |     mkApp (CApp fc f args) args' = CApp fc f (args ++ args')

 53 |     mkApp (CCon fc n ci t args) args' = CCon fc n ci t (args ++ args')

 54 |     mkApp (CExtPrim fc p args) args' = CExtPrim fc p (args ++ args')

 55 |     mkApp tm args = CApp (getFC tm) tm args

 56 | etaExpand i (S k) exp args

 57 |     = CLam (getFC exp) (MN "eta" i)

 58 |              (etaExpand (i + 1) k (weaken exp)

 59 |                   (first :: map weakenVar args))

 62 | expandToArity : Nat -> CExp vars -> List (CExp vars) -> CExp vars

 64 | expandToArity _ (CErased fc) _ = CErased fc

 66 | expandToArity Z f args = applyAll f args

 67 |   where

 68 |     applyAll : CExp vars -> List (CExp vars) -> CExp vars

 69 |     applyAll fn [] = fn

 70 |     applyAll fn (a :: args) = applyAll (CApp (getFC fn) fn [a]) args

 71 | expandToArity (S k) f (a :: args) = expandToArity k (addArg f a) args

 72 |   where

 73 |     addArg : CExp vars -> CExp vars -> CExp vars

 74 |     addArg (CApp fc fn args) a = CApp fc fn (args ++ [a])

 75 |     addArg (CCon fc n ci tag args) a = CCon fc n ci tag (args ++ [a])

 76 |     addArg (CExtPrim fc p args) a = CExtPrim fc p (args ++ [a])

 77 |     addArg f a = CApp (getFC f) f [a]

 79 | expandToArity num fn [] = etaExpand 0 num fn []

 81 | applyNewType : Nat -> Nat -> CExp vars -> List (CExp vars) -> CExp vars

 82 | applyNewType arity pos fn args

 83 |     = let fn' = expandToArity arity fn args in

 84 |           keepArg fn' -- fn' might be lambdas, after eta expansion

 85 |   where

 86 |     keep : Nat -> List (CExp vs) -> CExp vs

 87 |     keep i [] = CErased (getFC fn) -- can't happen if all is well!

 88 |     keep i (x :: xs)

 89 |         = if i == pos

 90 |              then x

 91 |              else keep (1 + i) xs

 93 |     keepArg : CExp vs -> CExp vs

 94 |     keepArg (CLam fc x sc) = CLam fc x (keepArg sc)

 95 |     keepArg (CCon fc _ _ _ args) = keep 0 args

 96 |     keepArg tm = CErased (getFC fn)

 98 | dropPos : NatSet -> CExp vs -> CExp vs

 99 | dropPos epos (CLam fc x sc) = CLam fc x (dropPos epos sc)

100 | dropPos epos (CApp fc tm@(CApp {}) args')

101 |     = CApp fc (dropPos epos tm) args'

102 | dropPos epos (CApp fc f args) = CApp fc f (drop epos args)

103 | dropPos epos (CCon fc c ci a args) = CCon fc c ci a (drop epos args)

104 | dropPos epos tm = tm

106 | eraseConArgs : Nat -> NatSet -> CExp vars -> List (CExp vars) -> CExp vars

107 | eraseConArgs arity epos fn args

108 |     = let fn' = expandToArity arity fn args in

109 |           if isEmpty epos

110 |              then fn'

111 |              else dropPos epos fn' -- fn' might be lambdas, after eta expansion

113 | mkDropSubst : Nat -> NatSet ->

114 |               (rest : List Name) ->

115 |               (vars : List Name) ->

116 |               (vars' ** Thin (vars' ++ rest) (vars ++ rest))

117 | mkDropSubst i es rest [] = ([] ** Refl)

118 | mkDropSubst i es rest (x :: xs)

119 |     = let (vs ** sub) = mkDropSubst (1 + i) es rest xs in

120 |           if i `elem` es

121 |              then (vs ** Drop sub)

122 |              else (x :: vs ** Keep sub)

126 | dconFlag : {auto c : Ref Ctxt Defs} ->

127 |            Name -> Core ConInfo

128 | dconFlag n

129 |     = do defs <- get Ctxt

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

131 |               | Nothing => throw (InternalError ("Can't find " ++ show n))

132 |          pure (ciFlags (definition def) (flags def))

133 |   where

134 |     ciFlags : Def -> List DefFlag -> ConInfo

135 |     ciFlags def [] = case def of

136 |       TCon {} => TYCON

137 |       _ => DATACON

138 |     ciFlags def (ConType ci :: xs) = ci

139 |     ciFlags def (x :: xs) = ciFlags def xs

141 | toCExpTm : {auto c : Ref Ctxt Defs} ->

142 |            Name -> Term vars ->

143 |            Core (CExp vars)

144 | toCExp : {auto c : Ref Ctxt Defs} ->

145 |          Name -> Term vars ->

146 |          Core (CExp vars)

148 | toCExpTm n (Local fc _ _ prf)

149 |     = pure $ CLocal fc prf

150 | toCExpTm n (Ref fc (DataCon tag arity) fn)

151 |     = do -- get full name for readability, and %builtin Natural

152 |          cn <- getFullName fn

153 |          fl <- dconFlag cn

154 |          pure $ CCon fc cn fl (Just tag) []

155 | toCExpTm n (Ref fc (TyCon arity) fn)

156 |     = pure $ CCon fc fn TYCON Nothing []

157 | toCExpTm n (Ref fc _ fn)

158 |     = do full <- getFullName fn

159 |              -- ^ For readability of output code, and the Nat hack,

160 |          pure $ CApp fc (CRef fc full) []

161 | toCExpTm n (Meta fc mn i args)

162 |     = pure $ CApp fc (CRef fc mn) !(traverse (toCExp n) args)

163 | toCExpTm n (Bind fc x (Lam {}) sc)

164 |     = pure $ CLam fc x !(toCExp n sc)

165 | toCExpTm n (Bind fc x (Let _ rig val _) sc)

166 |     = do sc' <- toCExp n sc

167 |          pure $ branchZero (shrinkCExp (Drop Refl) sc')

168 |                         (CLet fc x YesInline !(toCExp n val) sc')

169 |                         rig

170 | toCExpTm n (Bind fc x (Pi _ c e ty) sc)

171 |     = pure $ CCon fc (UN (Basic "->")) TYCON Nothing

172 |                      [ !(toCExp n ty)

173 |                      , CLam fc x !(toCExp n sc)]

174 | toCExpTm n (Bind fc x b tm) = pure $ CErased fc

176 | toCExpTm n (App fc tm arg)

177 |     = pure $ CApp fc !(toCExp n tm) [!(toCExp n arg)]

179 | toCExpTm n (As _ _ _ p) = toCExpTm n p

181 | toCExpTm n (TDelayed fc _ _) = pure $ CErased fc

182 | toCExpTm n (TDelay fc lr _ arg)

183 |     = pure (CDelay fc lr !(toCExp n arg))

184 | toCExpTm n (TForce fc lr arg)

185 |     = pure (CForce fc lr !(toCExp n arg))

186 | toCExpTm n (PrimVal fc $ PrT c) = pure $ CCon fc (UN $ Basic $ show c) TYCON Nothing [] -- Primitive type constant

187 | toCExpTm n (PrimVal fc c) = pure $ CPrimVal fc c -- Non-type constant

188 | toCExpTm n (Erased fc _) = pure $ CErased fc

189 | toCExpTm n (TType fc _) = pure $ CCon fc (UN (Basic "Type")) TYCON Nothing []

191 | toCExp n tm

192 |     = case getFnArgs tm of

193 |            (f, args) =>

194 |               do args' <- traverse (toCExp n) args

195 |                  defs <- get Ctxt

196 |                  f' <- toCExpTm n f

197 |                  case !(numArgs defs f) of

198 |                       NewTypeBy arity pos =>

199 |                         pure $ applyNewType arity pos f' args'

200 |                       EraseArgs arity epos =>

201 |                         pure $ eraseConArgs arity epos f' args'

202 |                       Arity a =>

203 |                         pure $ expandToArity a f' args'

206 |   conCases : {vars : _} ->

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

208 |              Name -> List (CaseAlt vars) ->

209 |              Core (List (CConAlt vars))

210 |   conCases n [] = pure []

211 |   conCases {vars} n (ConCase x tag args sc :: ns)

212 |       = do defs <- get Ctxt

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

214 |                 | Nothing => -- primitive type match

215 |                      do xn <- getFullName x

216 |                         pure $ MkConAlt xn TYCON Nothing args !(toCExpTree n sc)

217 |                                   :: !(conCases n ns)

218 |            case (definition gdef) of

219 |                 DCon _ arity (Just pos) => conCases n ns -- skip it

220 |                 _ => do xn <- getFullName x

221 |                         let (args' ** sub)

222 |                             = mkDropSubst 0 (eraseArgs gdef) vars args

223 |                         sc' <- toCExpTree n sc

224 |                         ns' <- conCases n ns

225 |                         if dcon (definition gdef)

226 |                            then pure $ MkConAlt xn !(dconFlag xn) (Just tag) args' (shrinkCExp sub sc') :: ns'

227 |                            else pure $ MkConAlt xn !(dconFlag xn) Nothing args' (shrinkCExp sub sc') :: ns'

228 |     where

229 |       dcon : Def -> Bool

230 |       dcon (DCon {}) = True

231 |       dcon _ = False

232 |   conCases n (_ :: ns) = conCases n ns

234 |   constCases : {vars : _} ->

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

236 |                Name -> List (CaseAlt vars) ->

237 |                Core (List (CConstAlt vars))

238 |   constCases n [] = pure []

239 |   constCases n (ConstCase WorldVal sc :: ns)

240 |       = constCases n ns

241 |   constCases n (ConstCase x sc :: ns)

242 |       = pure $ MkConstAlt x !(toCExpTree n sc) ::

243 |                     !(constCases n ns)

244 |   constCases n (_ :: ns) = constCases n ns

246 |   -- If there's a case which matches on a 'newtype', return the RHS

247 |   -- without matching.

248 |   -- Take some care if the newtype involves a WorldVal - in that case we

249 |   -- still need to let bind the scrutinee to ensure it's evaluated exactly

250 |   -- once.

251 |   getNewType : {vars : _} ->

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

253 |                FC -> CExp vars ->

254 |                Name -> List (CaseAlt vars) ->

255 |                Core (Maybe (CExp vars))

256 |   getNewType fc scr n [] = pure Nothing

257 |   getNewType fc scr n (DefaultCase sc :: ns)

258 |       = pure $ Nothing

259 |   getNewType {vars} fc scr n (ConCase x tag args sc :: ns)

260 |       = do defs <- get Ctxt

261 |            case !(lookupDefExact x (gamma defs)) of

262 |                 -- If the flag is False, we still take the

263 |                 -- default, but need to evaluate the scrutinee of the

264 |                 -- case anyway - if the data structure contains a %World,

265 |                 -- that we've erased, it means it has interacted with the

266 |                 -- outside world, so we need to evaluate to keep the

267 |                 -- side effect.

268 |                 Just (DCon _ arity (Just (noworld, pos))) =>

275 |                      if noworld -- just substitute the scrutinee into

276 |                                 -- the RHS

277 |                         then

278 |                              let (s, env) : (SizeOf args, SubstCEnv args vars)

279 |                                      = mkSubst 0 scr pos args in

280 |                               do log "compiler.newtype.world" 50 "Inlining case on \{show n} (no world)"

281 |                                  pure $ Just (substs s env !(toCExpTree n sc))

282 |                         else -- let bind the scrutinee, and substitute the

283 |                              -- name into the RHS

284 |                              let (s, env) : (_, SubstCEnv args (MN "eff" 0 :: vars))

285 |                                      = mkSubst 0 (CLocal fc First) pos args in

286 |                              do sc' <- toCExpTree n sc

287 |                                 let scope = insertNames {outer=args}

288 |                                                         {inner=vars}

289 |                                                         {ns = [MN "eff" 0]}

290 |                                                         (mkSizeOf _) (mkSizeOf _) sc'

291 |                                 let tm = CLet fc (MN "eff" 0) NotInline scr (substs s env scope)

292 |                                 log "compiler.newtype.world" 50 "Kept the scrutinee \{show tm}"

293 |                                 pure (Just tm)

294 |                 _ => pure Nothing -- there's a normal match to do

295 |     where

296 |       mkSubst : Nat -> CExp vs ->

297 |                 Nat -> (args : List Name) -> (SizeOf args, SubstCEnv args vs)

298 |       mkSubst _ _ _ [] = (zero, Subst.empty)

299 |       mkSubst i scr pos (a :: as)

300 |           = let (s, env) = mkSubst (1 + i) scr pos as in

301 |             if i == pos

302 |                then (suc s, scr :: env)

303 |                else (suc s, CErased fc :: env)

304 |   getNewType fc scr n (_ :: ns) = getNewType fc scr n ns

306 |   getDef : {vars : _} ->

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

308 |            Name -> List (CaseAlt vars) ->

309 |            Core (Maybe (CExp vars))

310 |   getDef n [] = pure Nothing

311 |   getDef n (DefaultCase sc :: ns)

312 |       = pure $ Just !(toCExpTree n sc)

313 |   getDef n (ConstCase WorldVal sc :: ns)

314 |       = pure $ Just !(toCExpTree n sc)

315 |   getDef n (_ :: ns) = getDef n ns

317 |   toCExpTree : {vars : _} ->

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

319 |                Name -> CaseTree vars ->

320 |                Core (CExp vars)

321 |   toCExpTree n alts@(Case _ x scTy (DelayCase ty arg sc :: rest))

322 |       = let fc = getLoc scTy in

323 |             pure $

324 |               CLet fc arg YesInline (CForce fc LInf (CLocal (getLoc scTy) x)) $

325 |               CLet fc ty YesInline (CErased fc)

326 |                    !(toCExpTree n sc)

327 |   toCExpTree n alts

328 |       = toCExpTree' n alts

330 |   toCExpTree' : {vars : _} ->

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

332 |                 Name -> CaseTree vars ->

333 |                 Core (CExp vars)

334 |   toCExpTree' n (Case _ x scTy alts@(ConCase _ _ _ _ :: _))

335 |       = let fc = getLoc scTy in

336 |             do Nothing <- getNewType fc (CLocal fc x) n alts

337 |                    | Just def => pure def

338 |                defs <- get Ctxt

339 |                cases <- conCases n alts

340 |                def <- getDef n alts

341 |                if isNil cases

342 |                   then pure $ fromMaybe (CErased fc) def

343 |                   else pure $ CConCase fc (CLocal fc x) cases def

344 |   toCExpTree' n (Case _ x scTy alts@(DelayCase _ _ _ :: _))

345 |       = throw (InternalError "Unexpected DelayCase")

346 |   toCExpTree' n (Case fc x scTy alts@(ConstCase _ _ :: _))

347 |       = let fc = getLoc scTy in

348 |             do cases <- constCases n alts

349 |                def <- getDef n alts

350 |                if isNil cases

351 |                   then pure (fromMaybe (CErased fc) def)

352 |                   else pure $ CConstCase fc (CLocal fc x) cases def

353 |   toCExpTree' n (Case _ x scTy alts@(DefaultCase sc :: _))

354 |       = toCExpTree n sc

355 |   toCExpTree' n (Case _ x scTy [])

356 |       = pure $ CCrash (getLoc scTy) $ "Missing case tree in " ++ show n

357 |   toCExpTree' n (STerm _ tm) = toCExp n tm

358 |   toCExpTree' n (Unmatched msg)

359 |       = pure $ CCrash emptyFC msg

360 |   toCExpTree' n Impossible

361 |       = pure $ CCrash emptyFC ("Impossible case encountered in " ++ show n)

365 | ArgList : Nat -> Scope -> Type

366 | ArgList = HasLength

368 | mkArgList : Int -> (n : Nat) -> (ns ** ArgList n ns)

369 | mkArgList i Z = (_ ** Z)

370 | mkArgList i (S k)

371 |     = let (ns ** rec) = mkArgList (i + 1) k in

372 |           ((MN "arg" i) :: ns ** S rec)

375 | getVars : ArgList k ns -> Vect k (Var ns)

376 | getVars Z = []

377 | getVars (S rest) = first :: map weakenVar (getVars rest)

379 | data NArgs : Type where

380 |      User : Name -> List ClosedClosure -> NArgs

381 |      Struct : String -> List (String, ClosedClosure) -> NArgs

382 |      NUnit : NArgs

383 |      NPtr : NArgs

384 |      NGCPtr : NArgs

385 |      NBuffer : NArgs

386 |      NForeignObj : NArgs

387 |      NIORes : ClosedClosure -> NArgs

389 | getPArgs : {auto c : Ref Ctxt Defs} ->

390 |            Defs -> ClosedClosure -> Core (String, ClosedClosure)

391 | getPArgs defs cl

392 |     = do NDCon fc _ _ _ args <- evalClosure defs cl

393 |              | nf => throw (GenericMsg (getLoc nf) "Badly formed struct type")

394 |          case reverse (map snd args) of

395 |               (tydesc :: n :: _) =>

396 |                   do NPrimVal _ (Str n') <- evalClosure defs n

397 |                          | nf => throw (GenericMsg (getLoc nf) "Unknown field name")

398 |                      pure (n', tydesc)

399 |               _ => throw (GenericMsg fc "Badly formed struct type")

401 | getFieldArgs : {auto c : Ref Ctxt Defs} ->

402 |                Defs -> ClosedClosure -> Core (List (String, ClosedClosure))

403 | getFieldArgs defs cl

404 |     = do NDCon fc _ _ _ args <- evalClosure defs cl

405 |              | nf => throw (GenericMsg (getLoc nf) "Badly formed struct type")

406 |          case map snd args of

407 |               -- cons

408 |               [_, t, rest] =>

409 |                   do rest' <- getFieldArgs defs rest

410 |                      (n, ty) <- getPArgs defs t

411 |                      pure ((n, ty) :: rest')

412 |               -- nil

413 |               _ => pure []

415 | getNArgs : {auto c : Ref Ctxt Defs} ->

416 |            Defs -> Name -> List ClosedClosure -> Core NArgs

417 | getNArgs defs (NS _ (UN $ Basic "IORes")) [arg] = pure $ NIORes arg

418 | getNArgs defs (NS _ (UN $ Basic "Ptr")) [arg] = pure NPtr

419 | getNArgs defs (NS _ (UN $ Basic "AnyPtr")) [] = pure NPtr

420 | getNArgs defs (NS _ (UN $ Basic "GCPtr")) [arg] = pure NGCPtr

421 | getNArgs defs (NS _ (UN $ Basic "GCAnyPtr")) [] = pure NGCPtr

422 | getNArgs defs (NS _ (UN $ Basic "Buffer")) [] = pure NBuffer

423 | getNArgs defs (NS _ (UN $ Basic "ForeignObj")) [] = pure NForeignObj

424 | getNArgs defs (NS _ (UN $ Basic "Unit")) [] = pure NUnit

425 | getNArgs defs (NS _ (UN $ Basic "Struct")) [n, args]

426 |     = do NPrimVal _ (Str n') <- evalClosure defs n

427 |              | nf => throw (GenericMsg (getLoc nf) "Unknown name for struct")

428 |          pure (Struct n' !(getFieldArgs defs args))

429 | getNArgs defs n args = pure $ User n args

432 | nfToCFType : {auto c : Ref Ctxt Defs} ->

433 |              FC -> ClosedNF -> (inStruct : Bool) -> Core CFType

434 | nfToCFType _ (NPrimVal _ $ PrT IntType) _ = pure CFInt

435 | nfToCFType _ (NPrimVal _ $ PrT IntegerType) _ = pure CFInteger

436 | nfToCFType _ (NPrimVal _ $ PrT Bits8Type) _ = pure CFUnsigned8

437 | nfToCFType _ (NPrimVal _ $ PrT Bits16Type) _ = pure CFUnsigned16

438 | nfToCFType _ (NPrimVal _ $ PrT Bits32Type) _ = pure CFUnsigned32

439 | nfToCFType _ (NPrimVal _ $ PrT Bits64Type) _ = pure CFUnsigned64

440 | nfToCFType _ (NPrimVal _ $ PrT Int8Type) _ = pure CFInt8

441 | nfToCFType _ (NPrimVal _ $ PrT Int16Type) _ = pure CFInt16

442 | nfToCFType _ (NPrimVal _ $ PrT Int32Type) _ = pure CFInt32

443 | nfToCFType _ (NPrimVal _ $ PrT Int64Type) _ = pure CFInt64

444 | nfToCFType _ (NPrimVal _ $ PrT StringType) False = pure CFString

445 | nfToCFType fc (NPrimVal _ $ PrT StringType) True

446 |     = throw (GenericMsg fc "String not allowed in a foreign struct")

447 | nfToCFType _ (NPrimVal _ $ PrT DoubleType) _ = pure CFDouble

448 | nfToCFType _ (NPrimVal _ $ PrT CharType) _ = pure CFChar

449 | nfToCFType _ (NPrimVal _ $ PrT WorldType) _ = pure CFWorld

450 | nfToCFType _ (NBind fc _ (Pi _ _ _ ty) sc) False

451 |     = do defs <- get Ctxt

452 |          sty <- nfToCFType fc !(evalClosure defs ty) False

453 |          sc' <- sc defs (toClosure defaultOpts Env.empty (Erased fc Placeholder))

454 |          tty <- nfToCFType fc sc' False

455 |          pure (CFFun sty tty)

456 | nfToCFType _ (NBind fc _ _ _) True

457 |     = throw (GenericMsg fc "Function types not allowed in a foreign struct")

458 | nfToCFType _ (NTCon fc n_in _ args) s

459 |     = do defs <- get Ctxt

460 |          n <- toFullNames n_in

461 |          case !(getNArgs defs n $ map snd args) of

462 |               User un uargs =>

463 |                 do nargs <- traverse (evalClosure defs) uargs

464 |                    cargs <- traverse (\ arg => nfToCFType fc arg s) nargs

465 |                    pure (CFUser n cargs)

466 |               Struct n fs =>

467 |                 do fs' <- traverse

468 |                              (\ (n, ty) =>

469 |                                     do tynf <- evalClosure defs ty

470 |                                        tycf <- nfToCFType fc tynf False

471 |                                        pure (n, tycf)) fs

472 |                    pure (CFStruct n fs')

473 |               NUnit => pure CFUnit

474 |               NPtr => pure CFPtr

475 |               NGCPtr => pure CFGCPtr

476 |               NBuffer => pure CFBuffer

477 |               NForeignObj => pure CFForeignObj

478 |               NIORes uarg =>

479 |                 do narg <- evalClosure defs uarg

480 |                    carg <- nfToCFType fc narg s

481 |                    pure (CFIORes carg)

482 | nfToCFType _ (NType {}) s

483 |     = pure (CFUser (UN (Basic "Type")) [])

484 | nfToCFType _ (NErased {}) s

485 |     = pure (CFUser (UN (Basic "__")) [])

486 | nfToCFType fc t s

487 |     = do defs <- get Ctxt

488 |          ty <- quote defs Env.empty t

489 |          throw (GenericMsg (getLoc t)

490 |                        ("Can't marshal type for foreign call " ++

491 |                                       show !(toFullNames ty)))

493 | getCFTypes : {auto c : Ref Ctxt Defs} ->

494 |              List CFType -> ClosedNF ->

495 |              Core (List CFType, CFType)

496 | getCFTypes args (NBind fc _ (Pi _ _ _ ty) sc)

497 |     = do defs <- get Ctxt

498 |          aty <- nfToCFType fc !(evalClosure defs ty) False

499 |          sc' <- sc defs (toClosure defaultOpts Env.empty (Erased fc Placeholder))

500 |          getCFTypes (aty :: args) sc'

501 | getCFTypes args t

502 |     = pure (reverse args, !(nfToCFType (getLoc t) t False))

504 | lamRHSenv : Int -> FC -> (ns : Scope) -> (SizeOf ns, SubstCEnv ns Scope.empty)

505 | lamRHSenv i fc [] = (zero, Subst.empty)

506 | lamRHSenv i fc (n :: ns)

507 |     = let (s, env) = lamRHSenv (i + 1) fc ns in

508 |       (suc s, CRef fc (MN "x" i) :: env)

510 | mkBounds : (xs : _) -> Bounds xs

511 | mkBounds [] = None

512 | mkBounds (x :: xs) = Add x x (mkBounds xs)

514 | getNewArgs : {done : _} ->

515 |              SubstCEnv done args -> Scope

516 | getNewArgs [] = []

517 | getNewArgs (CRef _ n :: xs) = n :: getNewArgs xs

518 | getNewArgs {done = x :: xs} (_ :: sub) = x :: getNewArgs sub

524 | lamRHS : (ns : Scope) -> CExp ns -> ClosedCExp

525 | lamRHS ns tm

526 |     = let (s, env) = lamRHSenv 0 (getFC tm) ns

527 |           tmExp = substs s env (rewrite appendNilRightNeutral ns in tm)

528 |           newArgs = reverse $ getNewArgs env

529 |           bounds = mkBounds newArgs

530 |           expLocs = mkLocals zero {vars = Scope.empty} bounds tmExp in

531 |           lamBind (getFC tm) _ expLocs

532 |   where

533 |     lamBind : FC -> (ns : Scope) -> CExp ns -> ClosedCExp

534 |     lamBind fc [] tm = tm

535 |     lamBind fc (n :: ns) tm = lamBind fc ns (CLam fc n tm)

537 | toArgExp : (Var ns) -> CExp ns

538 | toArgExp (MkVar p) = CLocal emptyFC p

540 | toCDef : Ref Ctxt Defs => Ref NextMN Int =>

541 |          Name -> ClosedTerm -> NatSet -> Def ->

542 |          Core CDef

543 | toCDef n ty _ None

544 |     = pure $ MkError $ CCrash emptyFC ("Encountered undefined name " ++ show !(getFullName n))

545 | toCDef n ty erased (PMDef pi args _ tree _)

546 |     = do let (args' ** p) = fromNatSet erased args

547 |          comptree <- toCExpTree n tree

548 |          pure $ toLam (externalDecl pi) $ if isEmpty erased

549 |             then MkFun args comptree

550 |             else MkFun args' (shrinkCExp p comptree)

551 |   where

552 |     toLam : Bool -> CDef -> CDef

553 |     toLam True (MkFun args rhs) = MkFun Scope.empty (lamRHS args rhs)

554 |     toLam _ d = d

555 | toCDef n ty _ (ExternDef arity)

556 |     = let (ns ** args) = mkArgList 0 arity in

557 |           pure $ MkFun _ (CExtPrim emptyFC !(getFullName n) (map toArgExp (toList $ getVars args)))

559 | toCDef n ty _ (ForeignDef arity cs)

560 |     = do defs <- get Ctxt

561 |          (atys, retty) <- getCFTypes [] !(nf defs Env.empty ty)

562 |          pure $ MkForeign cs atys retty

563 | toCDef n ty _ (Builtin {arity} op)

564 |     = let (ns ** args) = mkArgList 0 arity in

565 |           pure $ MkFun _ (COp emptyFC op (map toArgExp (getVars args)))

567 | toCDef n _ _ (DCon tag arity pos)

568 |     = do let nt = snd <$> pos

569 |          defs <- get Ctxt

570 |          args <- numArgs {vars = Scope.empty} defs (Ref EmptyFC (DataCon tag arity) n)

571 |          let arity' = case args of

572 |                  NewTypeBy ar _ => ar

573 |                  EraseArgs ar erased => ar `minus` size erased

574 |                  Arity ar => ar

575 |          pure $ MkCon (Just tag) arity' nt

576 | toCDef n _ _ (TCon arity _ _ _ _ _ _)

577 |     = pure $ MkCon Nothing arity Nothing

580 | toCDef n ty _ (Hole {})

581 |     = pure $ MkError $ CCrash emptyFC ("Encountered unimplemented hole " ++

582 |                                        show !(getFullName n))

583 | toCDef n ty _ (Guess {})

584 |     = pure $ MkError $ CCrash emptyFC ("Encountered constrained hole " ++

585 |                                        show !(getFullName n))

586 | toCDef n ty _ (BySearch {})

587 |     = pure $ MkError $ CCrash emptyFC ("Encountered incomplete proof search " ++

588 |                                        show !(getFullName n))

589 | toCDef n ty _ def

590 |     = pure $ MkError $ CCrash emptyFC ("Encountered uncompilable name " ++

591 |                                        show (!(getFullName n), def))

594 | compileExp : {auto c : Ref Ctxt Defs} ->

595 |              ClosedTerm -> Core ClosedCExp

596 | compileExp tm

597 |     = do s <- newRef NextMN 0

598 |          exp <- toCExp (UN $ Basic "main") tm

599 |          constructorCExp exp

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

604 | compileDef n

605 |     = do defs <- get Ctxt

606 |          Just gdef <- lookupCtxtExact n (gamma defs)

607 |               | Nothing => throw (InternalError ("Trying to compile unknown name " ++ show n))

608 |          -- If we're incremental, and the name has no definition yet, it

609 |          -- might end up defined in another module, so leave it, but warn

610 |          if noDefYet (definition gdef) (incrementalCGs !getSession)

611 |            -- This won't be accurate if we have names declared in one module

612 |            -- and defined elsewhere. It's tricky to do the complete check that

613 |            -- we do for whole program compilation, though, since that involves

614 |            -- traversing everything from the main expression.

615 |            -- For now, consider it an incentive not to have cycles :).

616 |             then recordWarning (GenericWarn emptyFC ("Compiling hole " ++ show n))

617 |             else do s <- newRef NextMN 0

618 |                     ce <- toCDef n (type gdef) (eraseArgs gdef)

619 |                            !(toFullNames (definition gdef))

620 |                     ce <- constructorCDef ce

621 |                     setCompiled n ce

622 |   where

623 |     noDefYet : Def -> List CG -> Bool

624 |     noDefYet None (_ :: _) = True

625 |     noDefYet _ _ = False