2 | module Core.CompileExpr

  4 | import Core.TT

  6 | import Data.List

  7 | import Data.Vect

  9 | import Libraries.Data.List.SizeOf

 10 | import Libraries.Data.SnocList.SizeOf

 12 | %default covering

 17 | public export

 18 | data ConInfo = DATACON -- normal data constructor

 19 |              | TYCON -- normal type constructor

 20 |              | NIL -- nil of a list or option shaped thing

 21 |              | CONS -- cons of a list shaped thing

 22 |              | ENUM Nat -- part of an enumeration with the given number of constructors

 23 |              | NOTHING -- nothing of an option shaped thing

 24 |              | JUST -- just of an option shaped thing

 25 |              | RECORD -- record constructor (no tag)

 26 |              | ZERO -- zero of a nat-like type

 27 |              | SUCC -- successor of a nat-like type

 28 |              | UNIT -- unit

 31 | Show ConInfo where

 32 |   show DATACON = "[datacon]"

 33 |   show TYCON   = "[tycon]"

 34 |   show NIL     = "[nil]"

 35 |   show CONS    = "[cons]"

 36 |   show (ENUM n) = "[enum " ++ show n ++ "]"

 37 |   show NOTHING = "[nothing]"

 38 |   show JUST    = "[just]"

 39 |   show RECORD  = "[record]"

 40 |   show ZERO    = "[zero]"

 41 |   show SUCC    = "[succ]"

 42 |   show UNIT    = "[unit]"

 45 | Eq ConInfo where

 46 |   DATACON == DATACON = True

 47 |   TYCON == TYCON = True

 48 |   NIL == NIL = True

 49 |   CONS == CONS = True

 50 |   ENUM x == ENUM y = x == y

 51 |   NOTHING == NOTHING = True

 52 |   JUST == JUST = True

 53 |   RECORD == RECORD = True

 54 |   ZERO == ZERO = True

 55 |   SUCC == SUCC = True

 56 |   UNIT == UNIT = True

 57 |   _ == _ = False

 60 | public export

 61 | data InlineOk = YesInline | NotInline

 64 | Eq InlineOk where

 65 |   YesInline == YesInline = True

 66 |   NotInline == NotInline = True

 67 |   _ == _ = False

 70 |   ||| CExp - an expression ready for compiling.

 71 |   public export

 72 |   data CExp : Scoped where

 73 |        CLocal : {idx : Nat} -> FC -> (0 p : IsVar x idx vars) -> CExp vars

 74 |        CRef : FC -> Name -> CExp vars

 75 |        -- Lambda expression

 76 |        CLam : FC -> (x : Name) -> CExp (x :: vars) -> CExp vars

 77 |        -- Let bindings

 78 |        CLet : FC -> (x : Name) ->

 79 |               InlineOk -> -- Don't inline if set

 80 |               CExp vars -> CExp (x :: vars) -> CExp vars

 81 |        -- Application of a defined function. The length of the argument list is

 82 |        -- exactly the same length as expected by its definition (so saturate with

 83 |        -- lambdas if necessary, or overapply with additional CApps)

 84 |        CApp : FC -> CExp vars -> List (CExp vars) -> CExp vars

 85 |        -- A saturated constructor application

 86 |        -- 'ConInfo' gives additional information about the constructor that

 87 |        -- a back end might be able to use. It is ignorable.

 88 |        CCon : FC -> Name -> ConInfo -> (tag : Maybe Int) ->

 89 |               List (CExp vars) -> CExp vars

 90 |        -- Internally defined primitive operations

 91 |        COp : {arity : _} ->

 92 |              FC -> PrimFn arity -> Vect arity (CExp vars) -> CExp vars

 93 |        -- Externally defined primitive operations

 94 |        CExtPrim : FC -> (p : Name) -> List (CExp vars) -> CExp vars

 95 |        -- A forced (evaluated) value

 96 |        CForce : FC -> LazyReason -> CExp vars -> CExp vars

 97 |        -- A delayed value

 98 |        CDelay : FC -> LazyReason -> CExp vars -> CExp vars

 99 |        -- A case match statement

100 |        CConCase : FC -> (sc : CExp vars) -> List (CConAlt vars) -> Maybe (CExp vars) -> CExp vars

101 |        CConstCase : FC -> (sc : CExp vars) -> List (CConstAlt vars) -> Maybe (CExp vars) -> CExp vars

102 |        -- A primitive value

103 |        CPrimVal : FC -> Constant -> CExp vars

104 |        -- An erased value

105 |        CErased : FC -> CExp vars

106 |        -- Some sort of crash?

107 |        CCrash : FC -> String -> CExp vars

109 |   public export

110 |   data CConAlt : Scoped where

111 |        -- If no tag, then match by constructor name. Back ends might want to

112 |        -- convert names to a unique integer for performance.

113 |        MkConAlt : Name -> ConInfo -> (tag : Maybe Int) -> (args : List Name) ->

114 |                   CExp (args ++ vars) -> CConAlt vars

116 |   public export

117 |   data CConstAlt : Scoped where

118 |        MkConstAlt : Constant -> CExp vars -> CConstAlt vars

120 | public export

121 | ClosedCExp : Type

122 | ClosedCExp = CExp []

125 |   ||| NamedCExp - as above, but without the name index, so with explicit

130 |   public export

131 |   data NamedCExp : Type where

132 |        NmLocal : FC -> Name -> NamedCExp

133 |        NmRef : FC -> Name -> NamedCExp

134 |        -- Lambda expression

135 |        NmLam : FC -> (x : Name) -> NamedCExp -> NamedCExp

136 |        -- Let bindings

137 |        NmLet : FC -> (x : Name) -> NamedCExp -> NamedCExp -> NamedCExp

138 |        -- Application of a defined function. The length of the argument list is

139 |        -- exactly the same length as expected by its definition (so saturate with

140 |        -- lambdas if necessary, or overapply with additional CApps)

141 |        NmApp : FC -> NamedCExp -> List NamedCExp -> NamedCExp

142 |        -- A saturated constructor application

143 |        -- 'ConInfo' gives additional information about the constructor that

144 |        -- a back end might be able to use. It is ignoreable.

145 |        NmCon : FC -> Name -> ConInfo -> (tag : Maybe Int) ->

146 |                List NamedCExp -> NamedCExp

147 |        -- Internally defined primitive operations

148 |        NmOp : {arity : _ } -> FC -> PrimFn arity -> Vect arity NamedCExp -> NamedCExp

149 |        -- Externally defined primitive operations

150 |        NmExtPrim : FC -> (p : Name) -> List NamedCExp -> NamedCExp

151 |        -- A forced (evaluated) value

152 |        NmForce : FC -> LazyReason -> NamedCExp -> NamedCExp

153 |        -- A delayed value

154 |        NmDelay : FC -> LazyReason -> NamedCExp -> NamedCExp

155 |        -- A case match statement

156 |        NmConCase : FC -> (sc : NamedCExp) -> List NamedConAlt -> Maybe NamedCExp -> NamedCExp

157 |        NmConstCase : FC -> (sc : NamedCExp) -> List NamedConstAlt -> Maybe NamedCExp -> NamedCExp

158 |        -- A primitive value

159 |        NmPrimVal : FC -> Constant -> NamedCExp

160 |        -- An erased value

161 |        NmErased : FC -> NamedCExp

162 |        -- Some sort of crash?

163 |        NmCrash : FC -> String -> NamedCExp

165 |   public export

166 |   data NamedConAlt : Type where

167 |        MkNConAlt : Name -> ConInfo -> (tag : Maybe Int) -> (args : List Name) ->

168 |                    NamedCExp -> NamedConAlt

170 |   public export

171 |   data NamedConstAlt : Type where

172 |        MkNConstAlt : Constant -> NamedCExp -> NamedConstAlt

175 | public export

176 | data CFType : Type where

177 |      CFUnit : CFType

178 |      CFInt : CFType

179 |      CFInteger : CFType

180 |      CFInt8 : CFType

181 |      CFInt16 : CFType

182 |      CFInt32 : CFType

183 |      CFInt64 : CFType

184 |      CFUnsigned8 : CFType

185 |      CFUnsigned16 : CFType

186 |      CFUnsigned32 : CFType

187 |      CFUnsigned64 : CFType

188 |      CFString : CFType

189 |      CFDouble : CFType

190 |      CFChar : CFType

191 |      CFPtr : CFType

192 |      CFGCPtr : CFType

193 |      CFBuffer : CFType

194 |      CFForeignObj : CFType

195 |      CFWorld : CFType

196 |      CFFun : CFType -> CFType -> CFType

197 |      CFIORes : CFType -> CFType

198 |      CFStruct : String -> List (String, CFType) -> CFType

199 |      CFUser : Name -> List CFType -> CFType

201 | public export

202 | data CDef : Type where

203 |      -- Normal function definition

204 |      MkFun : (args : Scope) -> CExp args -> CDef

205 |      -- Constructor

206 |      MkCon : (tag : Maybe Int) -> (arity : Nat) -> (nt : Maybe Nat) -> CDef

207 |      -- Foreign definition

208 |      MkForeign : (ccs : List String) ->

209 |                  (fargs : List CFType) ->

210 |                  CFType ->

211 |                  CDef

212 |      -- A function which will fail at runtime (usually due to being a hole) so needs

213 |      -- to run, discarding arguments, no matter how many arguments are passed

214 |      MkError : ClosedCExp -> CDef

216 | public export

217 | data NamedDef : Type where

218 |      -- Normal function definition

219 |      MkNmFun : (args : List Name) -> NamedCExp -> NamedDef

220 |      -- Constructor

221 |      MkNmCon : (tag : Maybe Int) -> (arity : Nat) -> (nt : Maybe Nat) -> NamedDef

222 |      -- Foreign definition

223 |      MkNmForeign : (ccs : List String) ->

224 |                    (fargs : List CFType) ->

225 |                    CFType ->

226 |                    NamedDef

227 |      -- A function which will fail at runtime (usually due to being a hole) so needs

228 |      -- to run, discarding arguments, no matter how many arguments are passed

229 |      MkNmError : NamedCExp -> NamedDef

232 |   export

233 |   Show NamedCExp where

234 |     show (NmLocal _ x) = "!" ++ show x

235 |     show (NmRef _ x) = show x

236 |     show (NmLam _ x y) = "(%lam " ++ show x ++ " " ++ show y ++ ")"

237 |     show (NmLet _ x y z) = "(%let " ++ show x ++ " " ++ show y ++ " " ++ show z ++ ")"

238 |     show (NmApp _ x xs)

239 |         = assert_total $ "(" ++ show x ++ " " ++ show xs ++ ")"

240 |     show (NmCon _ x ci tag xs)

241 |         = assert_total $ "(%con " ++ showFlag ci ++ show x ++ " " ++ show tag ++ " " ++ show xs ++ ")"

242 |       where

243 |         showFlag : ConInfo -> String

244 |         showFlag DATACON = ""

245 |         showFlag f = show f ++ " "

246 |     show (NmOp _ op xs)

247 |         = assert_total $ "(" ++ show op ++ " " ++ show xs ++ ")"

248 |     show (NmExtPrim _ p xs)

249 |         = assert_total $ "(%extern " ++ show p ++ " " ++ show xs ++ ")"

250 |     show (NmForce _ lr x) = "(%force " ++ show lr ++ " " ++ show x ++ ")"

251 |     show (NmDelay _ lr x) = "(%delay " ++ show lr ++ " " ++ show x ++ ")"

252 |     show (NmConCase _ sc xs def)

253 |         = assert_total $ "(%case " ++ show sc ++ " " ++ show xs ++ " " ++ show def ++ ")"

254 |     show (NmConstCase _ sc xs def)

255 |         = assert_total $ "(%case " ++ show sc ++ " " ++ show xs ++ " " ++ show def ++ ")"

256 |     show (NmPrimVal _ x) = show x

257 |     show (NmErased _) = "___"

258 |     show (NmCrash _ x) = "(CRASH " ++ show x ++ ")"

260 |   export

261 |   Show NamedConAlt where

262 |     show (MkNConAlt x ci tag args exp)

263 |          = "(%concase " ++ showFlag ci ++ show x ++ " " ++ show tag ++ " " ++

264 |              show args ++ " " ++ show exp ++ ")"

265 |       where

266 |         showFlag : ConInfo -> String

267 |         showFlag DATACON = ""

268 |         showFlag f = show f ++ " "

270 |   export

271 |   Show NamedConstAlt where

272 |     show (MkNConstAlt x exp)

273 |          = "(%constcase " ++ show x ++ " " ++ show exp ++ ")"

276 | data Names : Scoped where

277 |      Nil : Names []

278 |      (::) : Name -> Names xs -> Names (x :: xs)

280 | elem : Name -> Names xs -> Bool

281 | elem n [] = False

282 | elem n (x :: xs) = n == x || elem n xs

284 | tryNext : Name -> Name

285 | tryNext (UN n) = MN (displayUserName n) 0

286 | tryNext (MN n i) = MN n (1 + i)

287 | tryNext n = MN (nameRoot n) 0

289 | uniqueName : Name -> Names vs -> Name

290 | uniqueName s ns =

291 |     if s `elem` ns

292 |        then uniqueName (tryNext s) ns

293 |        else s

296 | getLocName : (idx : Nat) -> Names vars -> (0 p : IsVar name idx vars) -> Name

297 | getLocName Z (x :: xs) First = x

298 | getLocName (S k) (x :: xs) (Later p) = getLocName k xs p

301 | addLocs : (args : List Name) -> Names vars -> Names (args ++ vars)

302 | addLocs [] ns = ns

303 | addLocs (x :: xs) ns

304 |     = let rec = addLocs xs ns in

305 |           uniqueName x rec :: rec

307 | conArgs : (args : List Name) -> Names (args ++ vars) -> List Name

308 | conArgs [] ns = []

309 | conArgs (a :: as) (n :: ns) = n :: conArgs as ns

312 |   forgetExp : Names vars -> CExp vars -> NamedCExp

313 |   forgetExp locs (CLocal fc p) = NmLocal fc (getLocName _ locs p)

314 |   forgetExp locs (CRef fc n) = NmRef fc n

315 |   forgetExp locs (CLam fc x sc)

316 |       = let locs' = addLocs [x] locs in

317 |             NmLam fc (getLocName _ locs' First) (forgetExp locs' sc)

318 |   forgetExp locs (CLet fc x _ val sc)

319 |       = let locs' = addLocs [x] locs in

320 |             NmLet fc (getLocName _ locs' First)

321 |                      (forgetExp locs val)

322 |                      (forgetExp locs' sc)

323 |   forgetExp locs (CApp fc f args)

324 |       = NmApp fc (forgetExp locs f) (map (forgetExp locs) args)

325 |   forgetExp locs (CCon fc n ci t args)

326 |       = NmCon fc n ci t (map (forgetExp locs) args)

327 |   forgetExp locs (COp fc op args)

328 |       = NmOp fc op (map (forgetExp locs) args)

329 |   forgetExp locs (CExtPrim fc p args)

330 |       = NmExtPrim fc p (map (forgetExp locs) args)

331 |   forgetExp locs (CForce fc lr f)

332 |       = NmForce fc lr (forgetExp locs f)

333 |   forgetExp locs (CDelay fc lr f)

334 |       = NmDelay fc lr (forgetExp locs f)

335 |   forgetExp locs (CConCase fc sc alts def)

336 |       = NmConCase fc (forgetExp locs sc) (map (forgetConAlt locs) alts)

337 |                      (map (forgetExp locs) def)

338 |   forgetExp locs (CConstCase fc sc alts def)

339 |       = NmConstCase fc (forgetExp locs sc) (map (forgetConstAlt locs) alts)

340 |                        (map (forgetExp locs) def)

341 |   forgetExp locs (CPrimVal fc c) = NmPrimVal fc c

342 |   forgetExp locs (CErased fc) = NmErased fc

343 |   forgetExp locs (CCrash fc msg) = NmCrash fc msg

345 |   forgetConAlt : Names vars -> CConAlt vars -> NamedConAlt

346 |   forgetConAlt locs (MkConAlt n ci t args exp)

347 |       = let args' = addLocs args locs in

348 |             MkNConAlt n ci t (conArgs args args') (forgetExp args' exp)

350 |   forgetConstAlt : Names vars -> CConstAlt vars -> NamedConstAlt

351 |   forgetConstAlt locs (MkConstAlt c exp)

352 |       = MkNConstAlt c (forgetExp locs exp)

355 | forget : {vars : _} -> CExp vars -> NamedCExp

356 | forget {vars} exp

357 |     = forgetExp (addLocs vars [])

358 |                 (rewrite appendNilRightNeutral vars in exp)

361 | forgetDef : CDef -> NamedDef

362 | forgetDef (MkFun args def)

363 |     = let ns = addLocs args []

364 |           args' = conArgs {vars = Scope.empty} args ns in

365 |           MkNmFun args' (forget def)

366 | forgetDef (MkCon t a nt) = MkNmCon t a nt

367 | forgetDef (MkForeign ccs fargs ty) = MkNmForeign ccs fargs ty

368 | forgetDef (MkError err) = MkNmError (forget err)

372 | {vars : _} -> Show (CExp vars) where

373 |   show exp = show (forget exp)

377 | Show CFType where

378 |   show CFUnit = "Unit"

379 |   show CFInt = "Int"

380 |   show CFInteger = "Integer"

381 |   show CFInt8 = "Int_8"

382 |   show CFInt16 = "Int_16"

383 |   show CFInt32 = "Int_32"

384 |   show CFInt64 = "Int_64"

385 |   show CFUnsigned8 = "Bits_8"

386 |   show CFUnsigned16 = "Bits_16"

387 |   show CFUnsigned32 = "Bits_32"

388 |   show CFUnsigned64 = "Bits_64"

389 |   show CFString = "String"

390 |   show CFDouble = "Double"

391 |   show CFChar = "Char"

392 |   show CFPtr = "Ptr"

393 |   show CFGCPtr = "GCPtr"

394 |   show CFBuffer = "Buffer"

395 |   show CFForeignObj = "ForeignObj"

396 |   show CFWorld = "%World"

397 |   show (CFFun s t) = show s ++ " -> " ++ show t

398 |   show (CFIORes t) = "IORes " ++ show t

399 |   show (CFStruct n args) = "struct " ++ show n ++ " " ++ showSep " " (map show args)

400 |   show (CFUser n args) = show n ++ " " ++ showSep " " (map show args)

404 | Show CDef where

405 |   show (MkFun args exp) = show args ++ ": " ++ show exp

406 |   show (MkCon tag arity pos)

407 |       = "Constructor tag " ++ show tag ++ " arity " ++ show arity ++

408 |         maybe "" (\n => " (newtype by " ++ show n ++ ")") pos

409 |   show (MkForeign ccs args ret)

410 |       = "Foreign call " ++ show ccs ++ " " ++

411 |         show args ++ " -> " ++ show ret

412 |   show (MkError exp) = "Error: " ++ show exp

416 | Show NamedDef where

417 |   show (MkNmFun args exp) = show args ++ ": " ++ show exp

418 |   show (MkNmCon tag arity pos)

419 |       = "Constructor tag " ++ show tag ++ " arity " ++ show arity ++

420 |         maybe "" (\n => " (newtype by " ++ show n ++ ")") pos

421 |   show (MkNmForeign ccs args ret)

422 |       = "Foreign call " ++ show ccs ++ " " ++

423 |         show args ++ " -> " ++ show ret

424 |   show (MkNmError exp) = "Error: " ++ show exp

427 |   export

428 |   insertNames : SizeOf outer ->

429 |                 SizeOf ns ->

430 |                 CExp (outer ++ inner) ->

431 |                 CExp (outer ++ (ns ++ inner))

432 |   insertNames outer ns (CLocal fc prf)

433 |       = let MkNVar var' = insertNVarNames outer ns (MkNVar prf) in

434 |             CLocal fc var'

435 |   insertNames _ _ (CRef fc x) = CRef fc x

436 |   insertNames outer ns (CLam fc x sc)

437 |       = let sc' = insertNames (suc outer) ns sc in

438 |             CLam fc x sc'

439 |   insertNames outer ns (CLet fc x inl val sc)

440 |       = let sc' = insertNames (suc outer) ns sc in

441 |             CLet fc x inl (insertNames outer ns val) sc'

442 |   insertNames outer ns (CApp fc x xs)

443 |       = CApp fc (insertNames outer ns x) (assert_total (map (insertNames outer ns) xs))

444 |   insertNames outer ns (CCon fc ci x tag xs)

445 |       = CCon fc ci x tag (assert_total (map (insertNames outer ns) xs))

446 |   insertNames outer ns (COp fc x xs)

447 |       = COp fc x (assert_total (map (insertNames outer ns) xs))

448 |   insertNames outer ns (CExtPrim fc p xs)

449 |       = CExtPrim fc p (assert_total (map (insertNames outer ns) xs))

450 |   insertNames outer ns (CForce fc lr x) = CForce fc lr (insertNames outer ns x)

451 |   insertNames outer ns (CDelay fc lr x) = CDelay fc lr (insertNames outer ns x)

452 |   insertNames outer ns (CConCase fc sc xs def)

453 |       = CConCase fc (insertNames outer ns sc) (assert_total (map (insertNamesConAlt outer ns) xs))

454 |                  (assert_total (map (insertNames outer ns) def))

455 |   insertNames outer ns (CConstCase fc sc xs def)

456 |       = CConstCase fc (insertNames outer ns sc) (assert_total (map (insertNamesConstAlt outer ns) xs))

457 |                    (assert_total (map (insertNames outer ns) def))

458 |   insertNames _ _ (CPrimVal fc x) = CPrimVal fc x

459 |   insertNames _ _ (CErased fc) = CErased fc

460 |   insertNames _ _ (CCrash fc x) = CCrash fc x

462 |   insertNamesConAlt : SizeOf outer ->

463 |                       SizeOf ns ->

464 |                       CConAlt (outer ++ inner) ->

465 |                       CConAlt (outer ++ (ns ++ inner))

466 |   insertNamesConAlt {outer} {ns} p q (MkConAlt x ci tag args sc)

467 |         = let sc' : CExp ((args ++ outer) ++ inner)

468 |                   = rewrite sym (appendAssociative args outer inner) in sc in

469 |               MkConAlt x ci tag args

470 |                (rewrite appendAssociative args outer (ns ++ inner) in

471 |                         insertNames (mkSizeOf args + p) q sc')

473 |   insertNamesConstAlt : SizeOf outer ->

474 |                         SizeOf ns ->

475 |                         CConstAlt (outer ++ inner) ->

476 |                         CConstAlt (outer ++ (ns ++ inner))

477 |   insertNamesConstAlt outer ns (MkConstAlt x sc) = MkConstAlt x (insertNames outer ns sc)

480 | FreelyEmbeddable CExp where

483 |   -- Shrink the scope of a compiled expression, replacing any variables not

484 |   -- in the remaining set with Erased

485 |   export

486 |   shrinkCExp : Thin newvars vars -> CExp vars -> CExp newvars

487 |   shrinkCExp sub (CLocal fc prf)

488 |       = case shrinkIsVar prf sub of

489 |              Nothing => CErased fc

490 |              Just (MkVar prf') => CLocal fc prf'

491 |   shrinkCExp _ (CRef fc x) = CRef fc x

492 |   shrinkCExp sub (CLam fc x sc)

493 |       = let sc' = shrinkCExp (Keep sub) sc in

494 |             CLam fc x sc'

495 |   shrinkCExp sub (CLet fc x inl val sc)

496 |       = let sc' = shrinkCExp (Keep sub) sc in

497 |             CLet fc x inl (shrinkCExp sub val) sc'

498 |   shrinkCExp sub (CApp fc x xs)

499 |       = CApp fc (shrinkCExp sub x) (assert_total (map (shrinkCExp sub) xs))

500 |   shrinkCExp sub (CCon fc x ci tag xs)

501 |       = CCon fc x ci tag (assert_total (map (shrinkCExp sub) xs))

502 |   shrinkCExp sub (COp fc x xs)

503 |       = COp fc x (assert_total (map (shrinkCExp sub) xs))

504 |   shrinkCExp sub (CExtPrim fc p xs)

505 |       = CExtPrim fc p (assert_total (map (shrinkCExp sub) xs))

506 |   shrinkCExp sub (CForce fc lr x) = CForce fc lr (shrinkCExp sub x)

507 |   shrinkCExp sub (CDelay fc lr x) = CDelay fc lr (shrinkCExp sub x)

508 |   shrinkCExp sub (CConCase fc sc xs def)

509 |       = CConCase fc (shrinkCExp sub sc)

510 |                  (assert_total (map (shrinkConAlt sub) xs))

511 |                  (assert_total (map (shrinkCExp sub) def))

512 |   shrinkCExp sub (CConstCase fc sc xs def)

513 |       = CConstCase fc (shrinkCExp sub sc)

514 |                    (assert_total (map (shrinkConstAlt sub) xs))

515 |                    (assert_total (map (shrinkCExp sub) def))

516 |   shrinkCExp _ (CPrimVal fc x) = CPrimVal fc x

517 |   shrinkCExp _ (CErased fc) = CErased fc

518 |   shrinkCExp _ (CCrash fc x) = CCrash fc x

520 |   shrinkConAlt : Thin newvars vars -> CConAlt vars -> CConAlt newvars

521 |   shrinkConAlt sub (MkConAlt x ci tag args sc)

522 |         = MkConAlt x ci tag args (shrinkCExp (keeps args sub) sc)

524 |   shrinkConstAlt : Thin newvars vars -> CConstAlt vars -> CConstAlt newvars

525 |   shrinkConstAlt sub (MkConstAlt x sc) = MkConstAlt x (shrinkCExp sub sc)

528 | Weaken CExp where

529 |   weakenNs ns tm = insertNames zero ns tm

532 | Weaken CConAlt where

533 |   weakenNs ns tm = insertNamesConAlt zero ns tm

535 | public export

536 | SubstCEnv : Scope -> Scoped

537 | SubstCEnv = Subst CExp

540 |   substEnv : Substitutable CExp CExp

541 |   substEnv outer dropped env (CLocal fc prf)

542 |       = find (\ (MkVar p) => CLocal fc p) outer dropped (MkVar prf) env

543 |   substEnv _ _ _ (CRef fc x) = CRef fc x

544 |   substEnv outer dropped env (CLam fc x sc)

545 |       = let sc' = substEnv (suc outer) dropped env sc in

546 |             CLam fc x sc'

547 |   substEnv outer dropped env (CLet fc x inl val sc)

548 |       = let sc' = substEnv (suc outer) dropped env sc in

549 |             CLet fc x inl (substEnv outer dropped env val) sc'

550 |   substEnv outer dropped env (CApp fc x xs)

551 |       = CApp fc (substEnv outer dropped env x) (assert_total (map (substEnv outer dropped env) xs))

552 |   substEnv outer dropped env (CCon fc x ci tag xs)

553 |       = CCon fc x ci tag (assert_total (map (substEnv outer dropped env) xs))

554 |   substEnv outer dropped env (COp fc x xs)

555 |       = COp fc x (assert_total (map (substEnv outer dropped env) xs))

556 |   substEnv outer dropped env (CExtPrim fc p xs)

557 |       = CExtPrim fc p (assert_total (map (substEnv outer dropped env) xs))

558 |   substEnv outer dropped env (CForce fc lr x) = CForce fc lr (substEnv outer dropped env x)

559 |   substEnv outer dropped env (CDelay fc lr x) = CDelay fc lr (substEnv outer dropped env x)

560 |   substEnv outer dropped env (CConCase fc sc xs def)

561 |       = CConCase fc (substEnv outer dropped env sc)

562 |                  (assert_total (map (substConAlt outer dropped env) xs))

563 |                  (assert_total (map (substEnv outer dropped env) def))

564 |   substEnv outer dropped env (CConstCase fc sc xs def)

565 |       = CConstCase fc (substEnv outer dropped env sc)

566 |                    (assert_total (map (substConstAlt outer dropped env) xs))

567 |                    (assert_total (map (substEnv outer dropped env) def))

568 |   substEnv _ _ _ (CPrimVal fc x) = CPrimVal fc x

569 |   substEnv _ _ _ (CErased fc) = CErased fc

570 |   substEnv _ _ _ (CCrash fc x) = CCrash fc x

572 |   substConAlt : Substitutable CExp CConAlt

573 |   substConAlt {vars} {outer} {dropped} p q env (MkConAlt x ci tag args sc)

574 |       = MkConAlt x ci tag args

575 |            (rewrite appendAssociative args outer vars in

576 |                     substEnv (mkSizeOf args + p) q env

577 |                       (rewrite sym (appendAssociative args outer (dropped ++ vars)) in

578 |                                sc))

580 |   substConstAlt : Substitutable CExp CConstAlt

581 |   substConstAlt outer dropped env (MkConstAlt x sc) = MkConstAlt x (substEnv outer dropped env sc)

584 | substs : {dropped, vars : _} ->

585 |          SizeOf dropped ->

586 |          SubstCEnv dropped vars -> CExp (dropped ++ vars) -> CExp vars

587 | substs = substEnv zero

590 |   export

591 |   mkLocals : SizeOf outer ->

592 |              Bounds bound ->

593 |              CExp (outer ++ vars) ->

594 |              CExp (outer ++ (bound ++ vars))

595 |   mkLocals later bs (CLocal {idx} {x} fc p)

596 |       = let MkNVar p' = addVars later bs (MkNVar p) in CLocal {x} fc p'

597 |   mkLocals later bs (CRef fc var)

598 |       = fromMaybe (CRef fc var) $ do

599 |           MkVar p <- resolveRef later [<] bs fc var

600 |           pure (CLocal fc p)

601 |   mkLocals later bs (CLam fc x sc)

602 |       = let sc' = mkLocals (suc later) bs sc in

603 |             CLam fc x sc'

604 |   mkLocals later bs (CLet fc x inl val sc)

605 |       = let sc' = mkLocals (suc later) bs sc in

606 |             CLet fc x inl (mkLocals later bs val) sc'

607 |   mkLocals later bs (CApp fc f xs)

608 |       = CApp fc (mkLocals later bs f) (assert_total (map (mkLocals later bs) xs))

609 |   mkLocals later bs (CCon fc ci x tag xs)

610 |       = CCon fc ci x tag (assert_total (map (mkLocals later bs) xs))

611 |   mkLocals later bs (COp fc x xs)

612 |       = COp fc x (assert_total (map (mkLocals later bs) xs))

613 |   mkLocals later bs (CExtPrim fc x xs)

614 |       = CExtPrim fc x (assert_total (map (mkLocals later bs) xs))

615 |   mkLocals later bs (CForce fc lr x)

616 |       = CForce fc lr (mkLocals later bs x)

617 |   mkLocals later bs (CDelay fc lr x)

618 |       = CDelay fc lr (mkLocals later bs x)

619 |   mkLocals later bs (CConCase fc sc xs def)

620 |       = CConCase fc (mkLocals later bs sc)

621 |                  (assert_total (map (mkLocalsConAlt later bs) xs))

622 |                  (assert_total (map (mkLocals later bs) def))

623 |   mkLocals later bs (CConstCase fc sc xs def)

624 |       = CConstCase fc (mkLocals later bs sc)

625 |                  (assert_total (map (mkLocalsConstAlt later bs) xs))

626 |                  (assert_total (map (mkLocals later bs) def))

627 |   mkLocals later bs (CPrimVal fc x) = CPrimVal fc x

628 |   mkLocals later bs (CErased fc) = CErased fc

629 |   mkLocals later bs (CCrash fc x) = CCrash fc x

631 |   mkLocalsConAlt : SizeOf outer ->

632 |                    Bounds bound ->

633 |                    CConAlt (outer ++ vars) ->

634 |                    CConAlt (outer ++ (bound ++ vars))

635 |   mkLocalsConAlt {bound} {outer} {vars} p bs (MkConAlt x ci tag args sc)

636 |         = let sc' : CExp ((args ++ outer) ++ vars)

637 |                   = rewrite sym (appendAssociative args outer vars) in sc in

638 |               MkConAlt x ci tag args

639 |                (rewrite appendAssociative args outer (bound ++ vars) in

640 |                         mkLocals (mkSizeOf args + p) bs sc')

642 |   mkLocalsConstAlt : SizeOf outer ->

643 |                      Bounds bound ->

644 |                      CConstAlt (outer ++ vars) ->

645 |                      CConstAlt (outer ++ (bound ++ vars))

646 |   mkLocalsConstAlt later bs (MkConstAlt x sc) = MkConstAlt x (mkLocals later bs sc)

649 | refsToLocals : Bounds bound -> CExp vars -> CExp (bound ++ vars)

650 | refsToLocals None tm = tm

651 | refsToLocals bs y = mkLocals zero bs y

654 | getFC : CExp args -> FC

655 | getFC (CLocal fc _) = fc

656 | getFC (CRef fc _) = fc

657 | getFC (CLam fc _ _) = fc

658 | getFC (CLet fc _ _ _ _) = fc

659 | getFC (CApp fc _ _) = fc

660 | getFC (CCon fc _ _ _ _) = fc

661 | getFC (COp fc _ _) = fc

662 | getFC (CExtPrim fc _ _) = fc

663 | getFC (CForce fc _ _) = fc

664 | getFC (CDelay fc _ _) = fc

665 | getFC (CConCase fc _ _ _) = fc

666 | getFC (CConstCase fc _ _ _) = fc

667 | getFC (CPrimVal fc _) = fc

668 | getFC (CErased fc) = fc

669 | getFC (CCrash fc _) = fc

671 | namespace NamedCExp

672 |   export

673 |   getFC : NamedCExp -> FC

674 |   getFC (NmLocal fc _) = fc

675 |   getFC (NmRef fc _) = fc

676 |   getFC (NmLam fc _ _) = fc

677 |   getFC (NmLet fc _ _ _) = fc

678 |   getFC (NmApp fc _ _) = fc

679 |   getFC (NmCon fc _ _ _ _) = fc

680 |   getFC (NmOp fc _ _) = fc

681 |   getFC (NmExtPrim fc _ _) = fc

682 |   getFC (NmForce fc _ _) = fc

683 |   getFC (NmDelay fc _ _) = fc

684 |   getFC (NmConCase fc _ _ _) = fc

685 |   getFC (NmConstCase fc _ _ _) = fc

686 |   getFC (NmPrimVal fc _) = fc

687 |   getFC (NmErased fc) = fc

688 |   getFC (NmCrash fc _) = fc