5 | module Language.IntrinsicTyping.Krivine

  7 | import Control.Function

  8 | import Data.DPair

  9 | import Data.List.Elem

 11 | %default total

 16 | public export

 17 | data Ty = Base | Arr Ty Ty

 19 | %name Ty a, b

 21 | public export

 22 | Context : Type

 23 | Context = List Ty

 25 | public export

 26 | data Term : Context -> Ty -> Type where

 27 |   Lam : Term (a :: g) b -> Term g (Arr a b)

 28 |   App : {a : Ty} -> Term g (Arr a b) -> Term g a -> Term g b

 29 |   Var : Elem a g -> Term g a

 31 | data Closed : Ty -> Type

 32 | data Env : Context -> Type

 34 | public export

 35 | data Closed : Ty -> Type where

 36 |   Closure : Term g a -> Env g -> Closed a

 37 |   ClApp : {a : Ty} -> Closed (Arr a b) -> Closed a -> Closed b

 39 | public export

 40 | data Env : Context -> Type where

 41 |   Nil : Env []

 42 |   (::) : {a : Ty} -> Closed a -> Env g -> Env (a :: g)

 44 | namespace Value

 46 |   public export

 47 |   data IsValue : Closed g -> Type where

 48 |     Lam : IsValue (Closure (Lam b) env)

 50 |   public export

 51 |   data Value : Ty -> Type where

 52 |     Val : (c : Closed a) -> IsValue c -> Value a

 57 | public export

 58 | data Redex : Ty -> Type where

 59 |   RVar : Elem a g -> Env g -> Redex a

 60 |   RApp : {a : Ty} -> Term g (Arr a b) -> Term g a -> Env g -> Redex b

 61 |   Beta : {a : Ty} -> Term (a :: g) b -> Env g -> Closed a -> Redex b

 63 | public export

 64 | redex : Redex a -> Closed a

 65 | redex (RVar v env) = Closure (Var v) env

 66 | redex (RApp f t env) = Closure (App f t) env

 67 | redex (Beta b env arg) = ClApp (Closure (Lam b) env) arg

 69 | public export

 70 | lookup : Env g -> Elem a g -> Closed a

 71 | lookup (v :: _) Here = v

 72 | lookup (_ :: vs) (There p) = lookup vs p

 74 | public export

 75 | contract : Redex a -> Closed a

 76 | contract (RVar v env) = lookup env v

 77 | contract (RApp f t env) = ClApp (Closure f env) (Closure t env)

 78 | contract (Beta b env arg) = Closure b (arg :: env)

 80 | namespace EvalContext

 82 |   public export

 83 |   data EvalContext : (inner, outer : Ty) -> Type where

 84 |     Nil : EvalContext inner inner

 85 |     (::) : Closed a -> EvalContext inner outer -> EvalContext (Arr a inner) outer

 87 |   public export

 88 |   snoc : EvalContext inner (Arr dom outer) -> Closed dom -> EvalContext inner outer

 89 |   snoc [] t = [t]

 90 |   snoc (hd :: ctx) t = hd :: snoc ctx t

 92 |   public export

 93 |   data SnocView : EvalContext inner outer -> Type where

 94 |     Lin : SnocView []

 95 |     (:<) : (ctx : EvalContext inner (Arr dom outer)) ->

 96 |            (t : Closed dom) ->

 97 |            SnocView (snoc ctx t)

 99 |   public export

100 |   snocView : (ctx : EvalContext inner outer) -> SnocView ctx

101 |   snocView [] = [<]

102 |   snocView (hd :: ctx@_) with (snocView ctx)

103 |     _ | [<] = [] :< hd

104 |     _ | ctx' :< t = (hd :: ctx') :< t

106 | public export

107 | plug : {a : Ty} -> EvalContext a b -> Closed a -> Closed b

108 | plug [] f = f

109 | plug (t :: ts) f = plug ts (ClApp f t)

111 | public export

112 | 0 plugSnoc : (ctx : EvalContext a (Arr dom b)) ->

113 |            (t : Closed dom) ->

114 |            (f : Closed a) ->

115 |            plug (snoc ctx t) f === ClApp (plug ctx f) t

116 | plugSnoc [] _ _ = Refl

117 | plugSnoc (t :: ctx) _ _ = plugSnoc ctx _ _

119 | public export

120 | data Decomposition : Closed a -> Type where

121 |   Val : (sc : Term (a :: g) b) -> (env : Env g) ->

122 |         Decomposition {a = Arr a b} (Closure (Lam sc) env)

123 |   Red : {s : Ty} -> (r : Redex s) -> (ctx : EvalContext s t) ->

124 |         Decomposition {a = t} (plug ctx (redex r))

126 | public export

127 | load : {a : Ty} -> (ctx : EvalContext a b) -> (c : Closed a) -> Decomposition (plug ctx c)

128 | public export

129 | unload : {a, b : Ty} -> (ctx : EvalContext (Arr a b) outer) ->

130 |          (sc : Term (a :: g) b) ->

131 |          (env : Env g) ->

132 |          Decomposition (plug ctx (Closure (Lam sc) env))

134 | load ctx (ClApp f t) = load (t :: ctx) f

135 | load ctx (Closure (Var v) env) = Red (RVar v env) ctx

136 | load ctx (Closure (App f t) env) = Red (RApp f t env) ctx

137 | load ctx (Closure (Lam sc) env) = unload ctx sc env

139 | unload [] sc env = Val sc env

140 | unload (arg :: ctx) sc env = Red (Beta sc env arg) ctx

142 | public export

143 | decompose : {a : Ty} -> (c : Closed a) -> Decomposition c

144 | decompose = load []

146 | public export

147 | decomposePlug : {a : Ty} -> (ctx : EvalContext a b) -> (c : Closed a) ->

148 |                 decompose (plug ctx c) === load ctx c

149 | decomposePlug [] c = Refl

150 | decomposePlug (t :: ctx) c = decomposePlug ctx (ClApp c t)

152 | public export

153 | recompose : Decomposition {a} c -> Closed a

154 | recompose (Red r ctx) = plug ctx (contract r)

155 | recompose (Val sc env) = Closure (Lam sc) env

157 | public export

158 | headReduce : {a : Ty} -> Closed a -> Closed a

159 | headReduce c = recompose (decompose c)

161 | public export

162 | loadRedex :

163 |   (ctx : EvalContext a b) -> (r : Redex a) ->

164 |   load ctx (redex r) === Red r ctx

165 | loadRedex ctx (RVar _ _) = Refl

166 | loadRedex ctx (RApp _ _ _) = Refl

167 | loadRedex ctx (Beta _ _ _) = Refl

170 | public export

171 | headReducePlug :

172 |   (ctx : EvalContext a b) -> (r : Redex a) ->

173 |   headReduce (plug ctx (redex r)) === plug ctx (contract r)

174 | headReducePlug ctx r

175 |   = rewrite decomposePlug ctx (redex r) in

176 |     rewrite loadRedex ctx r in

177 |     Refl

179 | headReduceNeutral :

180 |   (ctx : EvalContext s b) -> (r : Redex s) ->

181 |   (f : Closed (Arr a b)) -> Not (IsValue f) ->

182 |   ClApp f t === plug ctx (redex r) ->

183 |   plug ctx (contract r) === ClApp (headReduce f) t

184 | headReduceNeutral ctx@_ r f nv with (snocView ctx)

185 |   headReduceNeutral ctx@_ (RVar _ _) f nv | [<] = \case Refl impossible

186 |   headReduceNeutral ctx@_ (RApp _ _ _) f nv | [<] = \case Refl impossible

187 |   headReduceNeutral ctx@_ (Beta _ _ _) f nv | [<] = \Refl => absurd (nv Lam)

188 |   _ | ctx' :< arg

189 |     = rewrite plugSnoc ctx' arg (contract r) in

190 |       rewrite plugSnoc ctx' arg (redex r) in

191 |       \Refl =>

192 |       rewrite headReducePlug ctx' r in

193 |       Refl

195 | public export

196 | headReduceClApp : {a, b : Ty} ->

197 |                   (f : Closed (Arr a b)) -> Not (IsValue f) -> (t : Closed a) ->

198 |                   headReduce (ClApp f t) === ClApp (headReduce f) t

199 | headReduceClApp f nv t with (decompose (ClApp f t)) | (ClApp f t) proof eq

200 |   _ | Val sc env | .(Closure (Lam sc) env)

201 |     = case eq of { Refl impossible }

202 |   _ | Red r ctx | plug ctx (redex r)

203 |     = headReduceNeutral ctx r f nv eq

208 | namespace Naïve

210 |   covering

211 |   evaluate : {a : Ty} -> Closed a -> Value a

212 |   evaluate c = iterate (decompose c) where

214 |     iterate : {a : Ty} -> {0 c : Closed a} -> Decomposition c -> Value a

215 |     iterate (Val b env)

216 |        -- there's a typo in the paper for this case

217 |       = Val (Closure (Lam b) env) Lam

218 |     iterate (Red r ctx) = iterate (decompose (plug ctx (contract r)))

222 | public export

223 | data Trace : Decomposition c -> Type where

224 |   Done : (sc, env : _) -> Trace (Val sc env)

225 |   Step : (ctx : EvalContext a b) -> (r : Redex a) ->

226 |          Trace (decompose (plug ctx (contract r))) -> Trace (Red r ctx)

228 | public export

229 | iterate : {a : Ty} -> {0 c : Closed a} -> {d : Decomposition {a} c} ->

230 |           (0 _ : Trace d) -> Value a

231 | iterate (Done sc env) = Val (Closure (Lam sc) env) Lam

232 | iterate (Step r ctx tr) = iterate tr

234 | public export

235 | Reducible : (a : Ty) -> Closed a -> Type

236 | Reducible Base t = Trace (decompose t)

237 | Reducible (Arr a b) t

238 |   = (Trace (decompose t)

239 |   , (x : Closed a) -> Reducible a x -> Reducible b (ClApp t x))

241 | namespace ReducibleEnv

243 |   public export

244 |   data ReducibleEnv : Env g -> Type where

245 |     Nil : ReducibleEnv []

246 |     (::) : Reducible a t -> ReducibleEnv env -> ReducibleEnv (t :: env)

248 |   public export

249 |   lookup : ReducibleEnv env -> (v : Elem a g) -> Reducible a (lookup env v)

250 |   lookup (red :: _) Here = red

251 |   lookup (_ :: reds) (There v) = lookup reds v

253 | public export

254 | step : {a : Ty} -> {c : Closed a} -> Trace (decompose (headReduce c)) -> Trace (decompose c)

255 | step {c = c@_} tr with (decompose c)

256 |   _ | Val sc env = tr

257 |   _ | Red r ctx = Step ctx r tr

259 | public export

260 | expand : {a : Ty} -> {c : Closed a} -> Reducible a (headReduce c) -> Reducible a c

261 | expand {a = Base} tr = step tr

262 | expand {a = Arr a b} {c = Closure (Lam x) env} (tr, hored) = (step tr, hored)

263 | expand {a = Arr a b} {c = Closure (App x t) env} (tr, hored)

264 |   = (step tr, \ arg, red => expand (hored arg red))

265 | expand {a = Arr a b} {c = Closure (Var x) env} (tr, hored)

266 |   = (step tr, \ arg, red => expand (hored arg red))

267 | expand {a = Arr a b} {c = ClApp f t} (tr, hored)

268 |   = MkPair (step tr)

269 |   $ \ arg, red =>

270 |     let 0 eq = headReduceClApp (ClApp f t) (\case Lam impossible) arg in

271 |     let red = replace {p = Reducible b} (sym eq) (hored arg red) in

272 |     expand {c = ClApp (ClApp f t) arg} red

274 | public export

275 | closure : {a : Ty} -> (t : Term g a) -> {env : Env g} ->

276 |           ReducibleEnv env -> Reducible _ (Closure t env)

277 | closure (Lam b) reds = (Done b _, \ arg, red => expand (closure b (red :: reds)))

278 | closure (App f t) reds = expand (snd (closure f reds) (Closure t env) (closure t reds))

279 | closure (Var v) reds = expand (lookup reds v)

281 | public export

282 | theorem : {a : Ty} -> (c : Closed a) -> Reducible a c

283 | public export

284 | theoremEnv : (env : Env g) -> ReducibleEnv env

286 | theorem (Closure t env) = closure t (theoremEnv env)

287 | theorem (ClApp f t) = snd (theorem f) t (theorem t)

289 | theoremEnv [] = []

290 | theoremEnv (t :: env) = theorem t :: theoremEnv env

292 | public export

293 | termination : {a : Ty} -> (c : Closed a) -> Trace (decompose c)

294 | termination {a = Base} c = theorem c

295 | termination {a = Arr a b} c = fst (theorem c)

297 | public export

298 | evaluate : {a : Ty} -> Closed a -> Value a

299 | evaluate c = iterate (termination c)

304 | public export

305 | refocus : {a : Ty} -> (ctx : EvalContext a b) -> (c : Closed a) -> Decomposition (plug ctx c)

306 | refocus ctx (ClApp f t) = refocus (t :: ctx) f

307 | refocus ctx (Closure (App f t) env) = Red (RApp f t env) ctx

308 | refocus ctx (Closure (Var v) env) = Red (RVar v env) ctx

309 | refocus [] (Closure (Lam b) env) = Val b env

310 | refocus (t :: ctx) (Closure (Lam b) env) = Red (Beta b env t) ctx

312 | public export

313 | refocusCorrect : {a : Ty} -> (ctx : EvalContext a b) -> (c : Closed a) ->

314 |                  refocus ctx c === decompose (plug ctx c)

315 | refocusCorrect ctx (ClApp f t) = refocusCorrect (t :: ctx) f

316 | refocusCorrect ctx (Closure (App f t) env) = sym $ decomposePlug ctx (Closure (App f t) env)

317 | refocusCorrect ctx (Closure (Var v) env) = sym $ decomposePlug ctx (Closure (Var v) env)

318 | refocusCorrect [] (Closure (Lam b) env) = Refl

319 | refocusCorrect (t :: ctx) (Closure (Lam b) env) = sym $ decomposePlug (t :: ctx) (Closure (Lam b) env)

321 | namespace Refocus

323 |   public export

324 |   data Trace : {c : Closed a} -> Decomposition c -> Type where

325 |     Done : (0 sc, env : _) -> Trace (Val sc env)

326 |     Step : (0 ctx : EvalContext a b) -> (0 r : Redex a) ->

327 |            Refocus.Trace (refocus ctx (contract r)) -> Trace (Red r ctx)

329 |   public export

330 |   trace : {0 c : Closed a} -> {0 d, e : Decomposition c} ->

331 |           Krivine.Trace d -> (0 _ : e === d) -> Refocus.Trace e

332 |   trace (Done sc env) Refl = Done sc env

333 |   trace (Step ctx r tr) Refl

334 |     = Step ctx r $ trace tr (refocusCorrect ctx (contract r))

336 |   public export

337 |   termination : {a : Ty} -> (c : Closed a) -> Refocus.Trace (decompose c)

338 |   termination c = trace (termination c) Refl

340 |   public export

341 |   iterate : {d : Decomposition {a} c} -> (0 _ : Refocus.Trace d) -> Value a

342 |   iterate (Done sc env) = Val (Closure (Lam sc) env) Lam

343 |   iterate (Step ctx r tr) = iterate tr

345 |   public export

346 |   evaluate : {a : Ty} -> Closed a -> Value a

347 |   evaluate c = iterate (Refocus.termination c)

352 | public export

353 | IsValidEnv : Env g -> Type

355 | public export

356 | IsValidClosed : Closed a -> Type

358 | IsValidClosed (Closure t env) = IsValidEnv env

359 | IsValidClosed _ = Void

361 | IsValidEnv [] = ()

362 | IsValidEnv (t :: env) = (IsValidClosed t, IsValidEnv env)

364 | public export

365 | ValidEnv : Context -> Type

366 | ValidEnv g = Subset (Env g) IsValidEnv

368 | public export

369 | ValidClosed : Ty -> Type

370 | ValidClosed a = Subset (Closed a) IsValidClosed

372 | namespace ValidClosed

374 |   public export

375 |   Closure : Term g a -> ValidEnv g -> ValidClosed a

376 |   Closure t (Element env pr) = Element (Closure t env) pr

378 |   public export

379 |   fstClosure : (t : Term g a) -> (env : ValidEnv g) ->

380 |                fst (Closure t env) === Closure t (fst env)

381 |   fstClosure t (Element env p) = Refl

383 |   public export

384 |   0 getContext : ValidClosed a -> Context

385 |   getContext (Element (Closure {g} t env) _) = g

387 |   public export

388 |   getEnv : (c : ValidClosed a) -> ValidEnv (getContext c)

389 |   getEnv (Element (Closure {g} _ env) pr) = Element env pr

391 |   public export

392 |   getTerm : (c : ValidClosed a) -> Term (getContext c) a

393 |   getTerm (Element (Closure t _) _) = t

395 |   public export

396 |   etaValidClosed : (c : ValidClosed a) -> c === Closure (getTerm c) (getEnv c)

397 |   etaValidClosed (Element (Closure t env) _) = Refl

399 | namespace ValidEnv

401 |   public export

402 |   lookup : (env : ValidEnv g) -> Elem a g -> ValidClosed a

403 |   lookup (Element (t :: env) p) Here = Element t (fst p)

404 |   lookup (Element (t :: env) p) (There v) = lookup (Element env (snd p)) v

406 |   public export

407 |   fstLookup : (env : ValidEnv g) -> (v : Elem a g) ->

408 |               fst (lookup env v) === lookup (fst env) v

409 |   fstLookup (Element (t :: env) p) Here = Refl

410 |   fstLookup (Element (t :: env) p) (There v) = fstLookup (Element env (snd p)) v

412 |   public export

413 |   Nil : ValidEnv []

414 |   Nil = Element [] ()

416 |   public export

417 |   (::) : {a : Ty} -> ValidClosed a -> ValidEnv g -> ValidEnv (a :: g)

418 |   Element t p :: Element env q = Element (t :: env) (p, q)

420 | public export

421 | IsValidEvalContext : EvalContext a b -> Type

422 | IsValidEvalContext [] = ()

423 | IsValidEvalContext (t :: ctx) =  (IsValidClosed t, IsValidEvalContext ctx)

425 | public export

426 | ValidEvalContext : (a, b : Ty) -> Type

427 | ValidEvalContext a b = Subset (EvalContext a b) IsValidEvalContext

429 | namespace ValidEvalContext

431 |   public export

432 |   Nil : ValidEvalContext a a

433 |   Nil = Element [] ()

435 |   public export

436 |   (::) : ValidClosed a -> ValidEvalContext b c -> ValidEvalContext (Arr a b) c

437 |   Element t p :: Element ctx q = Element (t :: ctx) (p, q)

439 |   public export

440 |   fstCons : (t : ValidClosed a) -> (ctx : ValidEvalContext b c) ->

441 |             fst (t :: ctx) === fst t :: fst ctx

442 |   fstCons (Element t p) (Element ctx q) = Refl

444 |   public export

445 |   [CONS] Biinjective ValidEvalContext.(::) where

446 |     biinjective

447 |       {x = Element t p} {y = Element t p}

448 |       {v = Element ts ps} {w = Element ts ps}

449 |       Refl = (Refl, Refl)

451 | namespace ValidEvalContextView

453 |   public export

454 |   data View : ValidEvalContext a b -> Type where

455 |     Nil : View []

456 |     (::) : (t : ValidClosed a) -> (ctx : ValidEvalContext b c) ->

457 |            View (t :: ctx)

459 |   public export

460 |   irrelevantUnit : (t : ()) -> t === ()

461 |   irrelevantUnit () = Refl

463 |   public export

464 |   etaPair : (p : (a, b)) -> p === (fst p, snd p)

465 |   etaPair (x, y) = Refl

467 |   public export

468 |   view : (ctx : ValidEvalContext a b) -> View ctx

469 |   view (Element [] p) = rewrite irrelevantUnit p in []

470 |   view (Element (t :: ctx) p)

471 |     = rewrite etaPair p in

472 |       Element t (fst p) :: Element ctx (snd p)

474 | namespace Machine

476 |   public export

477 |   data Trace : Term g a -> ValidEnv g -> ValidEvalContext a b -> Type where

479 |     Var : {env : ValidEnv g} -> {v : Elem a g} ->

480 |           Trace (getTerm (lookup env v)) (getEnv (lookup env v)) ctx ->

481 |           Trace (Var v) env ctx

483 |     App : {f : Term g (Arr a b)} -> {t : Term g a} ->

484 |           Trace f env (Closure t env :: ctx) ->

485 |           Trace (App f t) env ctx

487 |     Beta : {sc : Term (a :: g) b} ->

488 |            {arg : ValidClosed a} ->

489 |            {ctx : ValidEvalContext b c} ->

490 |            Trace sc (arg :: env) ctx ->

491 |            Trace (Lam sc) env (arg :: ctx)

493 |     Done : Trace (Lam sc) env []

495 |   data View : Trace t env ctx -> Type where

496 |     VVar : {0 env : ValidEnv g} -> {0 v : Elem a g} ->

497 |            (0 tr : Trace (getTerm (lookup env v)) (getEnv (lookup env v)) ctx) ->

498 |            View {t = Var v, env, ctx} (Var tr)

499 |     VApp : {0 f : Term g (Arr a b)} -> {0 t : Term g a} ->

500 |            {0 ctx : ValidEvalContext b c} ->

501 |            (0 tr : Trace f env (Closure t env :: ctx)) ->

502 |            View (App {f, t, env, ctx} tr)

503 |     VBeta : {0 sc : Term (a :: g) b} ->

504 |             {arg : ValidClosed a} ->

505 |             {ctx : ValidEvalContext b c} ->

506 |             (0 tr : Trace sc (arg :: env) ctx) ->

507 |             View (Beta {sc, arg, env, ctx} tr)

508 |     VDone : (sc : Term (a :: g) b) ->

509 |             View (Done {sc})

511 |   public export

512 |   vvar : (tr : Trace (Var v) env ctx) ->

513 |          (tr' : Trace ? ? ctx ** tr = Var tr')

514 |   vvar (Var tr) = (tr ** Refl)

516 |   public export

517 |   vapp : (tr : Trace (App f t) env ctx) ->

518 |          (tr' : Trace f env (Closure t env :: ctx) ** tr = App tr')

519 |   vapp (App tr) = (tr ** Refl)

521 |   public export

522 |   vlam0 : (eq : ctx = []) -> (tr : Trace (Lam sc) env ctx) -> tr ~=~ Machine.Done {sc, env}

523 |   vlam0 eq Done = Refl

524 |   vlam0 eq (Beta {arg = Element _ _, ctx = Element _ _} _) impossible

526 |   public export

527 |   vlamS : {0 env : ValidEnv g} -> {0 arg : ValidClosed a} ->

528 |           {0 sc : Term (a :: g) b} -> {0 ctx' : ValidEvalContext b c} ->

529 |           (eq : ctx = ValidEvalContext.(::) arg ctx') ->

530 |           (tr : Trace (Lam sc) env ctx) ->

531 |           (tr' : Trace sc (arg :: env) ctx' ** tr ~=~ Machine.Beta {sc, arg, env} tr')

532 |   vlamS {arg = (Element _ _)} {ctx' = (Element _ _)} eq Done impossible

533 |   vlamS eq (Beta tr) with 0 (fst (biinjective @{CONS} eq))

534 |     _ | Refl with 0 (snd (biinjective @{CONS} eq))

535 |       _ | Refl = (tr ** Refl)

537 |   public export

538 |   view : (t : Term g a) -> (env : ValidEnv g) -> (ctx : ValidEvalContext a b) ->

539 |          (0 tr : Trace t env ctx) -> View tr

540 |   view (Var v) env ctx tr = rewrite snd (vvar tr) in VVar _

541 |   view (App f t) env ctx tr = rewrite snd (vapp tr) in VApp _

542 |   view (Lam sc) env ctx@_ tr with (view ctx)

543 |     _ | [] = rewrite vlam0 Refl tr in VDone sc

544 |     _ | (arg :: ctx') = rewrite snd (vlamS {env, arg, sc, ctx'} Refl tr) in VBeta _

546 |   public export

547 |   refocus : {a : Ty} ->

548 |     {t : Term g a} -> {env : ValidEnv g} ->

549 |     {ctx : ValidEvalContext a b} ->

550 |     (0 _ : Trace t env ctx) -> Value b

551 |   refocus tr@_ with (view _ _ _ tr)

552 |     _ | VVar tr' = refocus tr'

553 |     _ | VApp tr' = refocus tr'

554 |     _ | VBeta tr' = refocus tr'

555 |     _ | VDone sc = Val (Closure (Lam sc) (fst env)) Lam

557 |   -- This is way TOO nasty because we don't have eta for records :((

558 |   public export

559 |   correctness :

560 |     {a : Ty} ->

561 |     (ctx : ValidEvalContext a b) ->

562 |     (t : Term g a) ->

563 |     (env : ValidEnv g) ->

564 |     (trold : Refocus.Trace (refocus (fst ctx) (Closure t (fst env)))) ->

565 |     (trnew : Machine.Trace t env ctx) ->

566 |     refocus trnew === Refocus.iterate trold

567 |   correctness ctx (Var v) env (Step (fst ctx) (RVar v (fst env)) trold) (Var trnew)

568 |     with (lookup env v) proof eq

569 |     _ | Element (Closure t' env') penv'

570 |     = correctness ctx t' (Element env' penv')

571 |         (rewrite sym (cong fst eq) in rewrite fstLookup env v in trold)

572 |         trnew

573 |   correctness ctx (App f t) env (Step (fst ctx) (RApp f t (fst env)) trold) (App trnew)

574 |     = correctness (Closure t env :: ctx) f env

575 |         (rewrite fstCons (Closure t env) ctx in rewrite fstClosure t env in trold)

576 |         trnew

577 |   correctness .(Element arg parg :: Element ctx pctx) (Lam sc) (Element env penv)

578 |     (Step ctx (Beta sc env arg) trold)

579 |     (Beta {arg = Element arg parg, ctx = Element ctx pctx} trnew)

580 |     = correctness (Element ctx pctx) sc (Element arg parg :: Element env penv)

581 |         trold

582 |         trnew

583 |   correctness (Element [] _) (Lam sc) env (Done _ _) tr

584 |     -- DISGUSTING

585 |     = case tr of

586 |         Beta {arg = Element _ _, ctx = Element _ _} _ impossible

587 |         Done => Refl

589 |   -- Another disgusgint proof because of a mix of:

590 |   --   * lack of eta and the coverage

591 |   --   * invalid "Dot pattern not valid here (Not LHS)" on the LHS

592 |   --   * coverage checker being confused

593 |   public export

594 |   trace : {a : Ty} -> (ctx : ValidEvalContext a b) ->

595 |           (t : Term g a) -> (env : ValidEnv g) ->

596 |           Refocus.Trace (refocus (fst ctx) (Closure t (fst env))) ->

597 |           Trace t env ctx

598 |   trace ctx (Var v) env (Step (fst ctx) (RVar v (fst env)) tr)

599 |     with (fstLookup env v) | (lookup env v) proof eq

600 |     _ | lemma | Element (Closure t' env') p

601 |       with (lookup (fst env) v)

602 |       trace ctx (Var v) env (Step (fst ctx) (RVar v (fst env)) tr)

603 |         | Refl | Element (Closure t' env') penv' | .(Closure t' env')

604 |         = Var (rewrite eq in trace ctx t' (Element env' penv') tr)

605 |   trace (Element ctx pctx) (App f t) (Element env penv) (Step .(ctx) (RApp f t env) tr)

606 |     = App (trace (Closure t (Element env penv) :: Element ctx pctx) f (Element env penv) tr)

607 |   trace (Element (arg :: ctx) pctx) (Lam sc) (Element env penv) tr

608 |     = case tr of

609 |         Done _ _ impossible

610 |         (Step ctx (Beta sc env arg) tr) =>

611 |           rewrite etaPair pctx in

612 |           Beta {arg = Element arg (fst pctx), ctx = Element ctx (snd pctx)}

613 |           (trace (Element ctx (snd pctx)) sc (Element (arg :: env) (fst pctx, penv)) tr)

614 |   trace (Element [] pctx) (Lam sc) env tr

615 |     = case tr of

616 |         Beta {arg = Element _ _, ctx = Element _ _} _ impossible

617 |         Done sc .(fst env) => rewrite irrelevantUnit pctx in Done

619 |   public export

620 |   termination : {a : Ty} -> (t : Term [] a) -> Trace t [] []

621 |   termination t

622 |     = trace [] t []

623 |     $ rewrite refocusCorrect [] (Closure t []) in

624 |       Refocus.termination (Closure t [])

626 |   public export

627 |   evaluate : {a : Ty} -> Term [] a -> Value a

628 |   evaluate t = Machine.refocus (termination t)