erasure to untyped syntax

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|]

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

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