erasure refactor

lib/Quox/EffExtra.idr

@@ -80,6 +80,24 @@ catchMaybe : (Has (Except e) fs, Length fs) =>
              (e -> Eff fs a) -> Eff fs a -> Eff fs a
 catchMaybe = catchMaybeAt ()
 
+
+export
+rethrowAtWith : (0 lbl : tag) -> Has (ExceptL lbl e') fs =>
+                (e -> e') -> Either e a -> Eff fs a
+rethrowAtWith lbl f = rethrowAt lbl . mapFst f
+
+export
+rethrowWith : Has (Except e') fs => (e -> e') -> Either e a -> Eff fs a
+rethrowWith = rethrowAtWith ()
+
+export
+wrapErr' : Length fs => (e -> e') ->
+           Eff (ExceptL lbl e  :: fs) a ->
+           Eff (ExceptL lbl e' :: fs) a
+wrapErr' f act =
+  catchAt lbl (throwAt lbl . f) @{S Z} $
+  lift @{subsetTail _} act
+
 export
 wrapErrAt : (0 lbl : tag) -> (Has (ExceptL lbl e) fs, Length fs) =>
             (e -> e) -> Eff fs a -> Eff fs a

lib/Quox/Untyped/Erase.idr

@@ -1,11 +1,12 @@
 module Quox.Untyped.Erase
 
-import Quox.Definition
+import Quox.Definition as Q
 import Quox.Syntax.Term.Base as Q
 import Quox.Syntax.Term.Subst
 import Quox.Untyped.Syntax as U
-import Quox.Typing.Context
+import Quox.Typing
 import Quox.Whnf
+import Quox.Pretty
 
 import Quox.EffExtra
 import Data.Singleton
@@ -35,19 +36,8 @@ ifErased pi x y = case isErased pi of
 
 
 public export
-EContext : Nat -> Type
+ErasureContext : Nat -> Nat -> Type
-EContext = Context' IsErased
+ErasureContext = TyContext
-
-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
@@ -58,35 +48,46 @@ TypeError = 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
+| Postulate       Loc Name
+%name Error err
+
+private %inline
+notInScope : Loc -> Name -> Error
+notInScope = WrapTypeError .: NotInScope
+
+export
+Located Error where
+  (CompileTimeOnly _ s).loc = s.loc
+  (WrapTypeError err).loc   = err.loc
+  (Postulate loc _).loc     = loc
+
+
+parameters {opts : LayoutOpts} (showContext : Bool)
+  export
+  prettyErrorNoLoc : Error -> Eff Pretty (Doc opts)
+  prettyErrorNoLoc (CompileTimeOnly ctx s) =
+    inTContext showContext ctx $
+    sep ["the term", !(prettyTerm ctx.dnames ctx.tnames s),
+         "only exists at compile time"]
+  prettyErrorNoLoc (WrapTypeError err) =
+    prettyErrorNoLoc showContext err
+  prettyErrorNoLoc (Postulate _ x) =
+    pure $ sep [!(prettyFree x), "is a postulate with no definition"]
+
+  export
+  prettyError : Error -> Eff Pretty (Doc opts)
+  prettyError err = sep <$> sequence
+    [prettyLoc err.loc, indentD =<< prettyErrorNoLoc err]
+
 
 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
+liftWhnf act = lift $ wrapErr' WrapTypeError 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 = liftWhnf $ whnf0 !(askAt DEFS) (toWhnfContext ctx) sg tm
 
 export covering
 computeElimType : ErasureContext d n -> SQty -> Elim d n -> Eff Erase (Term d n)
@@ -98,72 +99,17 @@ computeElimType ctx sg e = do
     computeElimType defs ctx sg e
 
 
-parameters (ctx : ErasureContext d n) (loc : Loc)
+private %macro
-  private covering %macro
+wrapExpect : TTImp ->
-  expect : (forall d, n. Loc -> NameContexts d n -> Term d n -> TypeError) ->
+             Elab (TyContext d n -> Loc -> Term d n -> Eff Erase a)
-           TTImp -> TTImp -> Elab (Term d n -> Eff Erase a)
+wrapExpect f {a} = do
-  expect k l r = do
+  f' <- check `(\x => ~(f) x)
-    f <- check `(\case ~(l) => Just ~(r); _ => Nothing)
+  pure $ \ctx, loc, s => wrapExpect' f' ctx loc s
-    pure $ \t =>
+where
-      let err = throw $ WrapTypeError $ k loc ctx.names t in
+  wrapExpect' : (Q.Definitions -> TyContext d n -> SQty -> Loc -> Term d n ->
-      maybe err pure . f =<< whnf0 ctx SZero t
+                    Eff [Except TypeError, NameGen] a) ->
-
+                TyContext d n -> Loc -> Term d n -> Eff Erase a
-  export covering %inline
+  wrapExpect' f ctx loc s = liftWhnf $ f !(askAt DEFS) ctx SZero loc s
-  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
@@ -173,10 +119,16 @@ record EraseElimResult d n where
   term : U.Term n
 
 
+-- "Ψ | Γ | Σ ⊢ s ⤋ s' ⇐ A" for `s' <- eraseTerm (Ψ,Γ,Σ) A s`
+--
+-- in the below comments, Ψ, Γ, Σ are implicit and
+-- only their extensions are written
 export covering
 eraseTerm : ErasureContext d n ->
             (ty, tm : Q.Term d n) -> Eff Erase (U.Term n)
 
+
+-- "Ψ | Γ | Σ ⊢ e ⤋ e' ⇒ A" for `EraRes A e' <- eraseElim (Ψ,Γ,Σ) e`
 export covering
 eraseElim : ErasureContext d n -> (tm : Q.Elim d n) ->
             Eff Erase (EraseElimResult d n)
@@ -187,14 +139,14 @@ eraseTerm ctx _ s@(TYPE {}) =
 eraseTerm ctx _ s@(Pi {}) =
   throw $ CompileTimeOnly ctx s
 
---         π.x : A ⊢ s ⤋ s' ⇐ B
+--        x : A | π.x ⊢ 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
+  (qty, arg, res) <- wrapExpect `(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
@@ -206,7 +158,7 @@ eraseTerm ctx _ s@(Sig {}) =
 -- ---------------------------------
 --  (s, t) ⤋ (s', t') ⇐ (x : A) × B
 eraseTerm ctx ty (Pair fst snd loc) = do
-  (a, b) <- expectSig ctx loc ty
+  (a, b) <- wrapExpect `(expectSig) ctx loc ty
   let b = sub1 b (Ann fst a a.loc)
   fst <- eraseTerm ctx a fst
   snd <- eraseTerm ctx b snd
@@ -226,7 +178,7 @@ eraseTerm ctx ty s@(Eq {}) =
 -- ---------------------------------
 --  (δ 𝑖 ⇒ s) ⤋ s' ⇐ Eq (𝑖 ⇒ A) l r
 eraseTerm ctx ty (DLam body loc) = do
-  a <- fst <$> expectEq ctx loc ty
+  a <- fst <$> wrapExpect `(expectEq) ctx loc ty
   eraseTerm (extendDim body.name ctx) a.term body.term
 
 eraseTerm ctx _ s@(Nat {}) =
@@ -252,7 +204,7 @@ eraseTerm ctx ty s@(BOX {}) =
 -- --------------------
 --   [s] ⤋ s' ⇐ [π.A]
 eraseTerm ctx ty (Box val loc) = do
-  (qty, a) <- expectBOX ctx loc ty
+  (qty, a) <- wrapExpect `(expectBOX) ctx loc ty
   case isErased qty of
     Erased => pure $ Erased loc
     Kept   => eraseTerm ctx a val
@@ -274,16 +226,16 @@ eraseTerm ctx ty (DCloT (Sub term th)) =
 --    x ⤋ x ⇒ A
 eraseElim ctx e@(F x u loc) = do
   Just def <- asksAt DEFS $ lookup x
-    | Nothing => throw $ NotInScope x
+    | Nothing => throw $ notInScope loc x
   case isErased def.qty.qty of
     Erased => throw $ CompileTimeOnly ctx $ E e
     Kept   => pure $ EraRes (def.typeWith ctx.dimLen ctx.termLen) $ F x loc
 
---            π ≠ 0
+--  π.x ∈ Σ   π ≠ 0
--- ----------------------------
+-- -----------------
---  Γ, π.x : A, Γ' ⊢ x ⤋ x ⇒ A
+--     x ⤋ x ⇒ A
 eraseElim ctx e@(B i loc) = do
-  case ctx.erased !!! i of
+  case isErased $ ctx.qtys !!! i of
     Erased => throw $ CompileTimeOnly ctx $ E e
     Kept   => pure $ EraRes (ctx.tctx !! i) $ B i loc
 
@@ -296,7 +248,7 @@ eraseElim ctx e@(B i loc) = do
 --    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
+  (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
@@ -304,7 +256,7 @@ eraseElim ctx (App fun arg loc) = do
                  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 : A, y : B | ρ.x, ρ.y ⊢ 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]
@@ -312,7 +264,7 @@ 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
+  (tfst, tsnd) <- wrapExpect `(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
@@ -325,7 +277,7 @@ eraseElim ctx (CasePair qty pair ret body loc) = do
 --   fst e ⤋ fst e' ⇒ A
 eraseElim ctx (Fst pair loc) = do
   epair      <- eraseElim ctx pair
-  a          <- fst <$> expectSig ctx loc epair.type
+  a          <- fst <$> wrapExpect `(expectSig) ctx loc epair.type
   pure $ EraRes a $ Fst epair.term loc
 
 --     e ⤋ e' ⇒ (x : A) × B
@@ -333,7 +285,7 @@ eraseElim ctx (Fst pair loc) = do
 --  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
+  b          <- snd <$> wrapExpect `(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]
@@ -364,13 +316,13 @@ eraseElim ctx e@(CaseEnum qty tag ret arms loc) =
         pure (t, rhs')
       pure $ EraRes ty $ CaseEnum etag.term arms loc
 
---          n ⤋ n' ⇒ ℕ   z ⤋ z' ⇐ R[zero∷ℕ/z]
+--             n ⤋ n' ⇒ ℕ   z ⤋ z' ⇐ R[zero∷ℕ/z]
---  ρ.m : ℕ, ς.ih : R[m/z] ⊢ s ⤋ s' ⇐ R[(succ m)∷ℕ/z]
+--  m : ℕ, ih : R[m/z] | ρ.m, ς.ih ⊢ s ⤋ s' ⇐ R[(succ m)∷ℕ/z]
--- ---------------------------------------------------
+-- -----------------------------------------------------------
---  caseρ n return z ⇒ R of {0 ⇒ z; succ m, ς.ih ⇒ s}
+--      caseρ n return z ⇒ R of {0 ⇒ z; succ m, ς.ih ⇒ s}
---    ⤋
+--        ⤋
---  case n' of {0 ⇒ z'; succ m, ih ⇒ s'}
+--      case n' of {0 ⇒ z'; succ m, ih ⇒ s'}
---    ⇒ R[n/z]
+--        ⇒ R[n/z]
 eraseElim ctx (CaseNat qty qtyIH nat ret zero succ loc) = do
   let ty = sub1 ret nat
   enat <- eraseElim ctx nat
@@ -384,16 +336,16 @@ eraseElim ctx (CaseNat qty qtyIH nat ret zero succ loc) = do
   pure $ EraRes ty $ CaseNat enat.term zero p ih succ loc
 
 --                b ⤋ b' ⇒ [π.A]   π ≠ 0
---          πρ.x : A ⊢ s ⤋ s' ⇐ R[[x]∷[π.A]/z]
+--         x : A | πρ.x ⊢ 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]
+--    b ⇒ [0.A]   x : A | 0.x ⊢ 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
+  (pi, tinner) <- wrapExpect `(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
@@ -411,7 +363,7 @@ eraseElim ctx (CaseBox qty box ret body loc) = do
 --      f @r ⤋ f' ⇒ A‹r/𝑖›
 eraseElim ctx (DApp fun arg loc) = do
   efun <- eraseElim ctx fun
-  a    <- fst <$> expectEq ctx loc efun.type
+  a    <- fst <$> wrapExpect `(expectEq) ctx loc efun.type
   pure $ EraRes (dsub1 a arg) efun.term
 
 --    s ⤋ s' ⇐ A
@@ -430,9 +382,6 @@ eraseElim ctx (Coe ty p q val loc) = do
 --          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
 
@@ -444,3 +393,13 @@ eraseElim ctx (CloE (Sub term th)) =
 
 eraseElim ctx (DCloE (Sub term th)) =
   eraseElim ctx $ pushSubstsWith' th id term
+
+
+export covering
+eraseDef : Name -> Q.Definition -> Eff Erase U.Definition
+eraseDef name (MkDef qty type body loc) = do
+  case isErased qty.qty of
+    Erased => pure ErasedDef
+    Kept   => case body of
+      Concrete body => KeptDef <$> eraseTerm empty type body
+      Postulate     => throw $ Postulate loc name

lib/Quox/Untyped/Syntax.idr

@@ -65,9 +65,12 @@ Located (Term n) where
   (Erased loc).loc                   = loc
 
 
+public export
+data Definition = ErasedDef | KeptDef (Term 0)
+
 public export
 0 Definitions : Type
-Definitions = SortedMap Name $ Term 0
+Definitions = SortedMap Name Definition
 
 
 parameters {opts : LayoutOpts}

lib/Quox/Whnf/Interface.idr

@@ -13,7 +13,7 @@ import public Control.Eff
 
 public export
 Whnf : List (Type -> Type)
-Whnf = [NameGen, Except Error]
+Whnf = [Except Error, NameGen]
 
 
 public export