From 428397f42bfbd81470b47e49bbe38bbf0bb811c3 Mon Sep 17 00:00:00 2001 From: rhiannon morris Date: Sat, 30 Sep 2023 18:37:44 +0200 Subject: [PATCH] erasure to untyped syntax --- lib/Quox/Typing/Context.idr | 2 +- lib/Quox/Untyped/Erase.idr | 450 ++++++++++++++++++++++++++++++++++++ lib/quox-lib.ipkg | 3 +- 3 files changed, 453 insertions(+), 2 deletions(-) create mode 100644 lib/Quox/Untyped/Erase.idr diff --git a/lib/Quox/Typing/Context.idr b/lib/Quox/Typing/Context.idr index 385721f..52418e0 100644 --- a/lib/Quox/Typing/Context.idr +++ b/lib/Quox/Typing/Context.idr @@ -73,7 +73,7 @@ namespace TContext zeroFor : Context tm n -> QOutput n zeroFor ctx = Zero <$ ctx -private +public export extendLen : Telescope a n1 n2 -> Singleton n1 -> Singleton n2 extendLen [<] x = x extendLen (tel :< _) x = [|S $ extendLen tel x|] diff --git a/lib/Quox/Untyped/Erase.idr b/lib/Quox/Untyped/Erase.idr new file mode 100644 index 0000000..1330f03 --- /dev/null +++ b/lib/Quox/Untyped/Erase.idr @@ -0,0 +1,450 @@ +module Quox.Untyped.Erase + +import Quox.Definition +import Quox.Syntax.Term.Base as Q +import Quox.Syntax.Term.Subst +import Quox.Untyped.Syntax as U +import Quox.Typing.Context +import Quox.Whnf + +import Quox.EffExtra +import Data.Singleton +import Data.SnocVect +import Language.Reflection + +%default total +%language ElabReflection + +%hide TT.Name + + +public export +data IsErased = Erased | Kept + +public export +isErased : Qty -> IsErased +isErased Zero = Erased +isErased One = Kept +isErased Any = Kept + +public export +ifErased : Qty -> Lazy a -> Lazy a -> a +ifErased pi x y = case isErased pi of + Erased => x + Kept => y + + +public export +EContext : Nat -> Type +EContext = Context' IsErased + +public export +record ErasureContext d n where + constructor MkEContexts + {auto dimLen : Singleton d} + {auto termLen : Singleton n} + dnames : BContext d + tnames : BContext n + tctx : TContext d n + erased : EContext n +%name ErasureContext ctx + + +public export +TypeError : Type +TypeError = Typing.Error.Error +%hide Typing.Error.Error + +public export +data Error = + CompileTimeOnly (ErasureContext d n) (Q.Term d n) +| ErasedVar (ErasureContext d n) (Var n) +| NotInScope Name +| WrapTypeError TypeError + +public export +Erase : List (Type -> Type) +Erase = [Except Error, DefsReader, NameGen] + + +export +toWhnfContext : ErasureContext d n -> WhnfContext d n +toWhnfContext (MkEContexts {dnames, tnames, tctx, _}) = + MkWhnfContext {dnames, tnames, tctx} + +export +(.names) : ErasureContext d n -> NameContexts d n +ctx.names = MkNameContexts ctx.dnames ctx.tnames + + +export +liftWhnf : Eff Whnf a -> Eff Erase a +liftWhnf act = runEff act + [\x => send x, \case (Err e) => throw $ WrapTypeError e] + +export covering +whnf0 : {0 isRedex : RedexTest tm} -> CanWhnf tm isRedex => + ErasureContext d n -> SQty -> + tm d n -> Eff Erase (tm d n) +whnf0 ctx sg tm = do + let Val n = ctx.termLen; Val d = ctx.dimLen + liftWhnf $ whnf0 !(askAt DEFS) (toWhnfContext ctx) sg tm + +export covering +computeElimType : ErasureContext d n -> SQty -> Elim d n -> Eff Erase (Term d n) +computeElimType ctx sg e = do + let Val n = ctx.termLen; Val d = ctx.dimLen + ctx = toWhnfContext ctx + defs <- askAt DEFS + Element e enf <- liftWhnf $ whnf defs ctx sg e + liftWhnf $ computeElimType defs ctx sg e + + +parameters (ctx : ErasureContext d n) (loc : Loc) + private covering %macro + expect : (forall d, n. Loc -> NameContexts d n -> Term d n -> TypeError) -> + TTImp -> TTImp -> Elab (Term d n -> Eff Erase a) + expect k l r = do + f <- check `(\case ~(l) => Just ~(r); _ => Nothing) + pure $ \t => + let err = throw $ WrapTypeError $ k loc ctx.names t in + maybe err pure . f =<< whnf0 ctx SZero t + + export covering %inline + expectTYPE : Term d n -> Eff Erase Universe + expectTYPE = expect ExpectedTYPE `(TYPE {l, _}) `(l) + + export covering %inline + expectPi : Term d n -> Eff Erase (Qty, Term d n, ScopeTerm d n) + expectPi = expect ExpectedPi `(Pi {qty, arg, res, _}) `((qty, arg, res)) + + export covering %inline + expectSig : Term d n -> Eff Erase (Term d n, ScopeTerm d n) + expectSig = expect ExpectedSig `(Sig {fst, snd, _}) `((fst, snd)) + + export covering %inline + expectEnum : Term d n -> Eff Erase (SortedSet TagVal) + expectEnum = expect ExpectedEnum `(Enum {cases, _}) `(cases) + + export covering %inline + expectEq : Term d n -> Eff Erase (DScopeTerm d n, Term d n, Term d n) + expectEq = expect ExpectedEq `(Eq {ty, l, r, _}) `((ty, l, r)) + + export covering %inline + expectNat : Term d n -> Eff Erase () + expectNat = expect ExpectedNat `(Nat {}) `(()) + + export covering %inline + expectBOX : Term d n -> Eff Erase (Qty, Term d n) + expectBOX = expect ExpectedBOX `(BOX {qty, ty, _}) `((qty, ty)) + + +export +extendTyN : CtxExtension d n1 n2 -> + ErasureContext d n1 -> ErasureContext d n2 +extendTyN tel (MkEContexts {termLen, dnames, tnames, tctx, erased}) = + let (qs, xs, ss) = unzip3 tel in + MkEContexts { + dnames, + tnames = tnames . xs, + tctx = tctx . ss, + erased = erased . map isErased qs, + termLen = extendLen tel termLen + } + +export +extendTy : Qty -> BindName -> Term d n -> + ErasureContext d n -> ErasureContext d (S n) +extendTy pi x ty = extendTyN [< (pi, x, ty)] + +export +extendDim : BindName -> ErasureContext d n -> ErasureContext (S d) n +extendDim i (MkEContexts {dimLen, dnames, tnames, tctx, erased}) = + MkEContexts { + tnames, erased, + dimLen = [|S dimLen|], + dnames = dnames :< i, + tctx = map (dweakT 1) tctx + } + + +public export +record EraseElimResult d n where + constructor EraRes + type : Lazy (Q.Term d n) + term : U.Term n + + +export covering +eraseTerm : ErasureContext d n -> + (ty, tm : Q.Term d n) -> Eff Erase (U.Term n) + +export covering +eraseElim : ErasureContext d n -> (tm : Q.Elim d n) -> + Eff Erase (EraseElimResult d n) + +eraseTerm ctx _ s@(TYPE {}) = + throw $ CompileTimeOnly ctx s + +eraseTerm ctx _ s@(Pi {}) = + throw $ CompileTimeOnly ctx s + +-- π.x : A ⊢ s ⤋ s' ⇐ B +-- ---------------------------------------- +-- (λ 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 + (qty, arg, res) <- expectPi ctx loc ty + let x = body.name + body <- eraseTerm (extendTy qty x arg ctx) res.term body.term + pure $ U.Lam x body loc + +eraseTerm ctx _ s@(Sig {}) = + throw $ CompileTimeOnly ctx s + +-- s ⤋ s' ⇐ A t ⤋ t' ⇐ B[s/x] +-- --------------------------------- +-- (s, t) ⤋ (s', t') ⇐ (x : A) × B +eraseTerm ctx ty (Pair fst snd loc) = do + (a, b) <- expectSig ctx loc ty + let b = sub1 b (Ann fst a a.loc) + fst <- eraseTerm ctx a fst + snd <- eraseTerm ctx b snd + pure $ Pair fst snd loc + +eraseTerm ctx _ s@(Enum {}) = + throw $ CompileTimeOnly ctx s + +-- '𝐚 ⤋ '𝐚 ⇐ {⋯} +eraseTerm ctx _ (Tag tag loc) = + pure $ Tag tag loc + +eraseTerm ctx ty s@(Eq {}) = + throw $ CompileTimeOnly ctx s + +-- 𝑖 ⊢ s ⤋ s' ⇐ A +-- --------------------------------- +-- (δ 𝑖 ⇒ s) ⤋ s' ⇐ Eq (𝑖 ⇒ A) l r +eraseTerm ctx ty (DLam body loc) = do + a <- fst <$> expectEq ctx loc ty + eraseTerm (extendDim body.name ctx) a.term body.term + +eraseTerm ctx _ s@(Nat {}) = + throw $ CompileTimeOnly ctx s + +-- 0 ⤋ 0 ⇐ ℕ +eraseTerm _ _ (Zero loc) = + pure $ Zero loc + +-- s ⤋ s' ⇐ ℕ +-- ----------------------- +-- succ s ⤋ succ s' ⇐ ℕ +eraseTerm ctx ty (Succ p loc) = do + p <- eraseTerm ctx ty p + pure $ Succ p loc + +eraseTerm ctx ty s@(BOX {}) = + throw $ CompileTimeOnly ctx s + +-- [s] ⤋ ⌷ ⇐ [0.A] +-- +-- π ≠ 0 s ⤋ s' ⇐ A +-- -------------------- +-- [s] ⤋ s' ⇐ [π.A] +eraseTerm ctx ty (Box val loc) = do + (qty, a) <- expectBOX ctx loc ty + case isErased qty of + Erased => pure $ Erased loc + Kept => eraseTerm ctx a val + +-- e ⤋ e' ⇒ B +-- ------------ +-- e ⤋ e' ⇐ A +eraseTerm ctx ty (E e) = + term <$> eraseElim ctx e + +eraseTerm ctx ty (CloT (Sub term th)) = + eraseTerm ctx ty $ pushSubstsWith' id th term + +eraseTerm ctx ty (DCloT (Sub term th)) = + eraseTerm ctx ty $ pushSubstsWith' th id term + +-- defω x : A = s +-- ---------------- +-- x ⤋ x ⇒ A +eraseElim ctx e@(F x u loc) = do + Just def <- asksAt DEFS $ lookup x + | Nothing => throw $ NotInScope x + case isErased def.qty.qty of + Erased => throw $ CompileTimeOnly ctx $ E e + Kept => + let Val d = ctx.dimLen; Val n = ctx.termLen in + pure $ EraRes def.type $ F x loc + +-- π ≠ 0 +-- ---------------------------- +-- Γ, π.x : A, Γ' ⊢ x ⤋ x ⇒ A +eraseElim ctx e@(B i loc) = do + case ctx.erased !!! i of + Erased => throw $ CompileTimeOnly ctx $ E e + Kept => pure $ EraRes (ctx.tctx !! i) $ B i loc + +-- f ⤋ f' ⇒ π.(x : A) → B s ⤋ s' ⇒ A π ≠ 0 +-- --------------------------------------------- +-- f s ⤋ f' s' ⇒ B[s/x] +-- +-- f ⤋ f' ⇒ 0.(x : A) → B +-- ------------------------- +-- f s ⤋ f' ⌷ ⇒ B[s/x] +eraseElim ctx (App fun arg loc) = do + efun <- eraseElim ctx fun + (qty, targ, tres) <- 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 + Kept => do arg <- eraseTerm ctx targ arg + pure $ EraRes ty $ App efun.term arg loc + +-- e ⤋ e' ⇒ (x : A) × B +-- ρ.x : A, ρ.y : B ⊢ s ⤋ s' ⇐ R[((x,y) ∷ (x : A) × B)/z] +-- x̃ ≔ if ρ = 0 then ⌷ else fst e' ỹ ≔ if ρ = 0 then ⌷ else snd e' +-- ------------------------------------------------------------------- +-- (caseρ e return z ⇒ R of {(x, y) ⇒ s}) ⤋ s'[x̃/x, ỹ/y] ⇒ R[e/z] +eraseElim ctx (CasePair qty pair ret body loc) = do + epair <- eraseElim ctx pair + let ty = sub1 (ret // shift 2) $ + Ann (Pair (BVT 0 loc) (BVT 1 loc) loc) (weakT 2 epair.type) loc + (tfst, tsnd) <- expectSig ctx loc epair.type + let [< x, y] = body.names + let ctx' = extendTyN [< (qty, x, tfst), (qty, y, tsnd.term)] ctx + body' <- eraseTerm ctx' ty body.term + let x' = ifErased qty (Erased loc) (Fst epair.term loc) + y' = ifErased qty (Erased loc) (Snd epair.term loc) + pure $ EraRes (sub1 ret pair) $ body' // fromSnocVect [< x', y'] + +-- e ⤋ e' ⇒ (x : A) × B +-- ---------------------- +-- fst e ⤋ fst e' ⇒ A +eraseElim ctx (Fst pair loc) = do + epair <- eraseElim ctx pair + a <- fst <$> expectSig ctx loc epair.type + pure $ EraRes a $ Fst epair.term loc + +-- e ⤋ e' ⇒ (x : A) × B +-- ----------------------------- +-- snd e ⤋ snd e' ⇒ B[fst e/x] +eraseElim ctx (Snd pair loc) = do + epair <- eraseElim ctx pair + b <- snd <$> expectSig ctx loc epair.type + pure $ EraRes (sub1 b (Fst pair loc)) $ Snd epair.term loc + +-- case0 e return z ⇒ R of {} ⤋ absurd ⇒ R[e/z] +-- +-- s ⤋ s' ⇐ R[𝐚∷{𝐚}/z] +-- ----------------------------------------------- +-- case0 e return z ⇒ R of {𝐚 ⇒ s} ⤋ s' ⇒ R[e/z] +-- +-- e ⤋ e' ⇒ A ρ ≠ 0 sᵢ ⤋ s'ᵢ ⇐ R[𝐚ᵢ/z] +-- ------------------------------------------------------------------- +-- caseρ e return z ⇒ R of {𝐚ᵢ ⇒ sᵢ} ⤋ case e of {𝐚ᵢ ⇒ s'ᵢ} ⇒ R[e/z] +eraseElim ctx e@(CaseEnum qty tag ret arms loc) = + case isErased qty of + Erased => case SortedMap.toList arms of + [] => pure $ EraRes (sub1 ret tag) $ Absurd loc + [(t, arm)] => do + let ty = sub1 ret tag + ty' = sub1 ret (Ann (Tag t loc) (enum [t] loc) loc) + arm' <- eraseTerm ctx ty' arm + pure $ EraRes ty arm' + _ => throw $ CompileTimeOnly ctx $ E e + Kept => do + let ty = sub1 ret tag + etag <- eraseElim ctx tag + arms <- for (SortedMap.toList arms) $ \(t, rhs) => do + let ty' = sub1 ret (Ann (Tag t loc) etag.type loc) + rhs' <- eraseTerm ctx ty' rhs + pure (t, rhs') + pure $ EraRes ty $ CaseEnum etag.term arms loc + +-- n ⤋ n' ⇒ ℕ z ⤋ z' ⇐ R[zero∷ℕ/z] +-- ρ.m : ℕ, ς.ih : R[m/z] ⊢ s ⤋ s' ⇐ R[(succ m)∷ℕ/z] +-- --------------------------------------------------- +-- caseρ n return z ⇒ R of {0 ⇒ z; succ m, ς.ih ⇒ s} +-- ⤋ +-- case n' of {0 ⇒ z'; succ m, ih ⇒ s'} +-- ⇒ R[n/z] +eraseElim ctx (CaseNat qty qtyIH nat ret zero succ loc) = do + let ty = sub1 ret nat + enat <- eraseElim ctx nat + zero <- eraseTerm ctx (sub1 ret (Ann (Zero loc) (Nat loc) loc)) zero + let [< p, ih] = succ.names + succ <- eraseTerm + (extendTyN [< (qty, p, Nat loc), + (qtyIH, ih, sub1 (ret // shift 1) (BV 0 loc))] ctx) + (sub1 (ret // shift 2) (Ann (Succ (BVT 1 loc) loc) (Nat loc) loc)) + succ.term + pure $ EraRes ty $ CaseNat enat.term zero p ih succ loc + +-- b ⤋ b' ⇒ [π.A] π ≠ 0 +-- πρ.x : A ⊢ s ⤋ s' ⇐ R[[x]∷[π.A]/z] +-- ------------------------------------------------------- +-- caseρ b return z ⇒ R of {[x] ⇒ s} ⤋ s'[b'/x] ⇒ R[b/z] +-- +-- b ⇒ [0.A] 0.x : A ⊢ s ⤋ s' ⇐ R[[x]∷[0.A]/z] +-- ------------------------------------------------------- +-- caseρ b return z ⇒ R of {[x] ⇒ s} ⤋ s'[⌷/x] ⇒ R[b/z] +eraseElim ctx (CaseBox qty box ret body loc) = do + tbox <- computeElimType ctx SOne box -- [fixme] is there any way to avoid this? + (pi, tinner) <- expectBOX ctx loc tbox + let ctx' = extendTy Zero body.name tinner ctx + bty = sub1 (ret // shift 1) $ + Ann (Box (BVT 0 loc) loc) (weakT 1 tbox) loc + case isErased pi of + Kept => do + ebox <- eraseElim ctx box + ebody <- eraseTerm ctx' bty body.term + pure $ EraRes (sub1 ret box) $ ebody // one ebox.term + Erased => do + body' <- eraseTerm ctx' bty body.term + pure $ EraRes (sub1 ret box) $ body' // one (Erased loc) + +-- f ⤋ f' ⇒ Eq (𝑖 ⇒ A) l r +-- ------------------------------ +-- f @r ⤋ f' ⇒ A‹r/𝑖› +eraseElim ctx (DApp fun arg loc) = do + efun <- eraseElim ctx fun + a <- fst <$> expectEq ctx loc efun.type + pure $ EraRes (dsub1 a arg) efun.term + +-- s ⤋ s' ⇐ A +-- ---------------- +-- s ∷ A ⤋ s' ⇒ A +eraseElim ctx (Ann tm ty loc) = + EraRes ty <$> eraseTerm ctx ty tm + +-- s ⤋ s' ⇐ A‹p/𝑖› +-- ----------------------------------- +-- coe (𝑖 ⇒ A) @p @q s ⤋ s' ⇒ A‹q/𝑖› +eraseElim ctx (Coe ty p q val loc) = do + val <- eraseTerm ctx (dsub1 ty p) val + pure $ EraRes (dsub1 ty q) val + +-- s ⤋ s' ⇐ A +-- -------------------------------- +-- comp A @p @q s @r {⋯} ⤋ s' ⇒ A +-- +-- [todo] is this ok? they are equal, but even so, +-- maybe t₀ and t₁ have different performance characteristics +eraseElim ctx (Comp ty p q val r zero one loc) = + EraRes ty <$> eraseTerm ctx ty val + +eraseElim ctx t@(TypeCase ty ret arms def loc) = + throw $ CompileTimeOnly ctx $ E t + +eraseElim ctx (CloE (Sub term th)) = + eraseElim ctx $ pushSubstsWith' id th term + +eraseElim ctx (DCloE (Sub term th)) = + eraseElim ctx $ pushSubstsWith' th id term diff --git a/lib/quox-lib.ipkg b/lib/quox-lib.ipkg index 26d4b6f..de8d2f3 100644 --- a/lib/quox-lib.ipkg +++ b/lib/quox-lib.ipkg @@ -57,4 +57,5 @@ modules = Quox.Parser.FromParser, Quox.Parser.FromParser.Error, Quox.Parser, - Quox.Untyped.Syntax + Quox.Untyped.Syntax, + Quox.Untyped.Erase