more erasure

lib/Quox/Untyped/Erase.idr

@@ -50,6 +50,7 @@ data Error =
   CompileTimeOnly (ErasureContext d n) (Q.Term d n)
 | WrapTypeError   TypeError
 | Postulate       Loc Name
+| WhileErasing    Name Q.Definition Error
 %name Error err
 
 private %inline
@@ -61,6 +62,7 @@ Located Error where
   (CompileTimeOnly _ s).loc  = s.loc
   (WrapTypeError err).loc    = err.loc
   (Postulate loc _).loc      = loc
+  (WhileErasing _ def e).loc = e.loc `or` def.loc
 
 
 parameters {opts : LayoutOpts} (showContext : Bool)
@@ -74,6 +76,9 @@ parameters {opts : LayoutOpts} (showContext : Bool)
     prettyErrorNoLoc showContext err
   prettyErrorNoLoc (Postulate _ x) =
     pure $ sep [!(prettyFree x), "is a postulate with no definition"]
+  prettyErrorNoLoc (WhileErasing name def err) = pure $
+    vsep [hsep ["while erasing the definition", !(prettyFree name)],
+          !(prettyErrorNoLoc err)]
 
   export
   prettyError : Error -> Eff Pretty (Doc opts)
@@ -147,7 +152,8 @@ eraseTerm ctx _ s@(Pi {}) =
 -- to preserve expected evaluation order
 eraseTerm ctx ty (Lam body loc) = do
   (qty, arg, res) <- wrapExpect `(expectPi) ctx loc ty
-  let x = body.name
+  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
 
@@ -346,7 +352,7 @@ eraseElim ctx (CaseNat qty qtyIH nat ret zero succ loc) = do
 eraseElim ctx (CaseBox qty box ret body loc) = do
   tbox <- computeElimType ctx SOne box -- [fixme] is there any way to avoid this?
   (pi, tinner) <- wrapExpect `(expectBOX) ctx loc tbox
-  let ctx' = extendTy Zero body.name tinner ctx
+  let ctx' = extendTy (pi * qty) body.name tinner ctx
       bty  = sub1 (ret // shift 1) $
              Ann (Box (BVT 0 loc) loc) (weakT 1 tbox) loc
   case isErased pi of
@@ -397,9 +403,10 @@ eraseElim ctx (DCloE (Sub term th)) =
 
 export covering
 eraseDef : Name -> Q.Definition -> Eff Erase U.Definition
-eraseDef name (MkDef qty type body loc) = do
+eraseDef name def@(MkDef qty type body loc) =
+  wrapErr (WhileErasing name def) $
   case isErased qty.qty of
     Erased => pure ErasedDef
     Kept   => case body of
-      Concrete body => KeptDef <$> eraseTerm empty type body
       Postulate     => throw $ Postulate loc name
+      Concrete body => KeptDef <$> eraseTerm empty type body

lib/Quox/Untyped/Syntax.idr

@@ -73,47 +73,52 @@ public export
 Definitions = SortedMap Name Definition
 
 
-parameters {opts : LayoutOpts}
 export
-  prettyTerm : BContext n -> Term n -> Eff Pretty (Doc opts)
+prettyTerm : {opts : LayoutOpts} -> BContext n ->
+             Term n -> Eff Pretty (Doc opts)
 
 export
-  prettyArg : BContext n -> Term n -> Eff Pretty (Doc opts)
+prettyArg : {opts : LayoutOpts} -> BContext n -> Term n -> Eff Pretty (Doc opts)
 prettyArg xs arg = withPrec Arg $ prettyTerm xs arg
 
 export
-  prettyApp' : Context' BindName n -> Doc opts -> Term n -> Eff Pretty (Doc opts)
+prettyApp' : {opts : LayoutOpts} -> BContext n -> Doc opts ->
+             Term n -> Eff Pretty (Doc opts)
 prettyApp' xs fun arg =
   parensIfM App =<< do
     arg <- prettyArg xs arg
     pure $ sep [fun, arg]
 
 export
-  prettyApp : Context' BindName n -> Term n -> Term n -> Eff Pretty (Doc opts)
+prettyApp : {opts : LayoutOpts} -> BContext n ->
-  prettyApp xs fun arg = prettyApp' xs !(prettyArg xs fun) arg
+            Term n -> Term n -> Eff Pretty (Doc opts)
+prettyApp xs fun arg =
+  prettyApp' xs !(withPrec App $ prettyTerm xs fun) arg
 
 public export
-  PrettyCaseArm : Nat -> Type
+record PrettyCaseArm a n where
-  PrettyCaseArm n = Exists $ \s => (Vect s BindName, Term (s + n))
+  constructor MkPrettyCaseArm
-
+  lhs : a
-  export %inline
+  {len : Nat}
-  caseArm : Vect s BindName -> Term (s + n) -> PrettyCaseArm n
+  vars : Vect len BindName
-  caseArm xs t = Evidence _ (xs, t)
+  rhs : Term (len + n)
 
 export
-  prettyCase : Context' BindName n ->
+prettyCase : {opts : LayoutOpts} -> BContext n ->
              (a -> Eff Pretty (Doc opts)) ->
-               Term n -> List (a, PrettyCaseArm n) ->
+             Term n -> List (PrettyCaseArm a n) ->
              Eff Pretty (Doc opts)
 prettyCase xs f head arms =
-    parensIfM Outer =<< Prelude.do
+  parensIfM Outer =<< do
     header <- hsep <$> sequence [caseD, prettyTerm xs head, ofD]
-      cases  <- for arms $ \(lhs, (Evidence s (ys, rhs))) => do
+    cases  <- for arms $ \(MkPrettyCaseArm lhs ys rhs) => do
       lhs <- hsep <$> sequence [f lhs, darrowD]
       rhs <- withPrec Outer $ prettyTerm (xs <>< ys) rhs
       hangDSingle lhs rhs
-      body <- braces $ separateLoose !semiD cases
+    lb <- hl Delim "{"; sc <- semiD; rb <- hl Delim "}"; d <- askAt INDENT
-      pure $ sep [header, body]
+    pure $ ifMultiline
+      (hsep [header, lb, separateTight sc cases, rb])
+      (vsep [hsep [header, lb], indent d $ vsep (map (<+> sc) cases), rb])
 
 prettyTerm _  (F x _) = prettyFree x
 prettyTerm xs (B i _) = prettyTBind $ xs !!! i
@@ -129,23 +134,27 @@ parameters {opts : LayoutOpts}
 prettyTerm xs (Fst pair _) = prettyApp' xs !fstD pair
 prettyTerm xs (Snd pair _) = prettyApp' xs !sndD pair
 prettyTerm xs (Tag tag _) = prettyTag tag
-  prettyTerm xs (CaseEnum tag cases _) = assert_total
+prettyTerm xs (CaseEnum tag cases _) =
-    prettyCase xs prettyTag tag $ map (mapSnd $ caseArm []) cases
+  assert_total
+  prettyCase xs prettyTag tag $
+    map (\(t, rhs) => MkPrettyCaseArm t [] rhs) cases
 prettyTerm xs (Absurd _) = hl Syntax "absurd"
 prettyTerm xs (Zero _) = zeroD
 prettyTerm xs (Succ nat _) = prettyApp' xs !succD nat
-  prettyTerm xs (CaseNat nat zer x ih suc _) = assert_total
+prettyTerm xs (CaseNat nat zer x ih suc _) =
+  assert_total
   prettyCase xs pure nat
-      [(!zeroD,  caseArm []      zer),
+    [MkPrettyCaseArm !zeroD  []      zer,
-       (!sucPat, caseArm [x, ih] suc)]
+     MkPrettyCaseArm !sucPat [x, ih] suc]
 where
-      sucPat = separateTight {t = List} !commaD <$>
+  sucPat = pure $
-               sequence [[|succD <++> prettyTBind x|], prettyTBind ih]
+    hsep [!succD, !(prettyTBind x) <+> !commaD, !(prettyTBind ih)]
 prettyTerm _ (Erased _) =
   hl Syntax =<< ifUnicode "⌷" "[]"
 
 export
-  prettyDef : Name -> Definition -> Eff Pretty (Maybe (Doc opts))
+prettyDef : {opts : LayoutOpts} -> Name ->
+            Definition -> Eff Pretty (Maybe (Doc opts))
 prettyDef _    ErasedDef     = [|Nothing|]
 prettyDef name (KeptDef rhs) = map Just $ do
   name <- prettyFree name