From 6ab9637ab5383ebcc746d39f10bf7ebffe6852f2 Mon Sep 17 00:00:00 2001 From: rhiannon morris Date: Fri, 3 Nov 2023 17:47:55 +0100 Subject: [PATCH] don't keep erased applications actually --- lib/Quox/Untyped/Erase.idr | 22 ++++++++++++---------- 1 file changed, 12 insertions(+), 10 deletions(-) diff --git a/lib/Quox/Untyped/Erase.idr b/lib/Quox/Untyped/Erase.idr index 8118920..d5e4300 100644 --- a/lib/Quox/Untyped/Erase.idr +++ b/lib/Quox/Untyped/Erase.idr @@ -144,18 +144,20 @@ eraseTerm ctx _ s@(TYPE {}) = eraseTerm ctx _ s@(Pi {}) = throw $ CompileTimeOnly ctx s --- x : A | π.x ⊢ s ⤋ s' ⇐ B +-- x : A | 0.x ⊢ s ⤋ s' ⇐ B +-- ------------------------------------- +-- (λ x ⇒ s) ⤋ s'[⌷/x] ⇐ 0.(x : A) → B +-- +-- x : A | π.x ⊢ s ⤋ s' ⇐ B π ≠ 0 -- ---------------------------------------- -- (λ x ⇒ s) ⤋ (λ x ⇒ s') ⇐ π.(x : A) → B --- --- becomes a lambda even when π = 0, --- to preserve expected evaluation order eraseTerm ctx ty (Lam body loc) = do + let x = body.name (qty, arg, res) <- wrapExpect `(expectPi) ctx loc ty - let x = case isErased qty of Kept => body.name - Erased => BN Unused body.name.loc - body <- eraseTerm (extendTy qty x arg ctx) res.term body.term - pure $ U.Lam x body loc + body <- eraseTerm (extendTy qty x arg ctx) res.term body.term + pure $ case isErased qty of + Kept => U.Lam x body loc + Erased => sub1 (Erased loc) body eraseTerm ctx _ s@(Sig {}) = throw $ CompileTimeOnly ctx s @@ -251,13 +253,13 @@ eraseElim ctx e@(B i loc) = do -- -- f ⤋ f' ⇒ 0.(x : A) → B -- ------------------------- --- f s ⤋ f' ⌷ ⇒ B[s/x] +-- f s ⤋ f' ⇒ B[s/x] eraseElim ctx (App fun arg loc) = do efun <- eraseElim ctx fun (qty, targ, tres) <- wrapExpect `(expectPi) ctx loc efun.type let ty = sub1 tres (Ann arg targ arg.loc) case isErased qty of - Erased => pure $ EraRes ty $ App efun.term (Erased arg.loc) loc + Erased => pure $ EraRes ty efun.term Kept => do arg <- eraseTerm ctx targ arg pure $ EraRes ty $ App efun.term arg loc