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
@@ -58,9 +59,10 @@ notInScope = WrapTypeError .: NotInScope
 
 export
 Located Error where
-  (CompileTimeOnly _ s).loc = s.loc
+  (CompileTimeOnly _ s).loc  = s.loc
-  (WrapTypeError err).loc   = err.loc
+  (WrapTypeError err).loc    = err.loc
-  (Postulate loc _).loc     = 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,85 +73,94 @@ public export
 Definitions = SortedMap Name Definition
 
 
-parameters {opts : LayoutOpts}
+export
-  export
+prettyTerm : {opts : LayoutOpts} -> BContext n ->
-  prettyTerm : BContext n -> Term n -> Eff Pretty (Doc opts)
+             Term n -> Eff Pretty (Doc opts)
 
-  export
+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
+prettyArg xs arg = withPrec Arg $ prettyTerm xs arg
 
-  export
+export
-  prettyApp' : Context' BindName n -> Doc opts -> Term n -> Eff Pretty (Doc opts)
+prettyApp' : {opts : LayoutOpts} -> BContext n -> Doc opts ->
-  prettyApp' xs fun arg =
+             Term n -> Eff Pretty (Doc opts)
-    parensIfM App =<< do
+prettyApp' xs fun arg =
-      arg <- prettyArg xs arg
+  parensIfM App =<< do
-      pure $ sep [fun, arg]
+    arg <- prettyArg xs arg
+    pure $ sep [fun, arg]
 
-  export
+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
+public export
-  PrettyCaseArm : Nat -> Type
+record PrettyCaseArm a n where
-  PrettyCaseArm n = Exists $ \s => (Vect s BindName, Term (s + n))
+  constructor MkPrettyCaseArm
+  lhs : a
+  {len : Nat}
+  vars : Vect len BindName
+  rhs : Term (len + n)
 
-  export %inline
+export
-  caseArm : Vect s BindName -> Term (s + n) -> PrettyCaseArm n
+prettyCase : {opts : LayoutOpts} -> BContext n ->
-  caseArm xs t = Evidence _ (xs, t)
+             (a -> Eff Pretty (Doc opts)) ->
+             Term n -> List (PrettyCaseArm a n) ->
+             Eff Pretty (Doc opts)
+prettyCase xs f head arms =
+  parensIfM Outer =<< do
+    header <- hsep <$> sequence [caseD, prettyTerm xs head, ofD]
+    cases  <- for arms $ \(MkPrettyCaseArm lhs ys rhs) => do
+      lhs <- hsep <$> sequence [f lhs, darrowD]
+      rhs <- withPrec Outer $ prettyTerm (xs <>< ys) rhs
+      hangDSingle lhs rhs
+    lb <- hl Delim "{"; sc <- semiD; rb <- hl Delim "}"; d <- askAt INDENT
+    pure $ ifMultiline
+      (hsep [header, lb, separateTight sc cases, rb])
+      (vsep [hsep [header, lb], indent d $ vsep (map (<+> sc) cases), rb])
 
-  export
+prettyTerm _  (F x _) = prettyFree x
-  prettyCase : Context' BindName n ->
+prettyTerm xs (B i _) = prettyTBind $ xs !!! i
-               (a -> Eff Pretty (Doc opts)) ->
+prettyTerm xs (Lam x body _) =
-               Term n -> List (a, PrettyCaseArm n) ->
+  parensIfM Outer =<< do
-               Eff Pretty (Doc opts)
+    header <- hsep <$> sequence [lamD, prettyTBind x, darrowD]
-  prettyCase xs f head arms =
+    body   <- withPrec Outer $ prettyTerm (xs :< x) body
-    parensIfM Outer =<< Prelude.do
+    hangDSingle header body
-      header <- hsep <$> sequence [caseD, prettyTerm xs head, ofD]
+prettyTerm xs (App fun arg _) = prettyApp xs fun arg
-      cases  <- for arms $ \(lhs, (Evidence s (ys, rhs))) => do
+prettyTerm xs (Pair fst snd _) =
-        lhs <- hsep <$> sequence [f lhs, darrowD]
+  parens =<< separateTight !commaD <$>
-        rhs <- withPrec Outer $ prettyTerm (xs <>< ys) rhs
+    sequence {t = List} [prettyTerm xs fst, prettyTerm xs snd]
-        hangDSingle lhs rhs
+prettyTerm xs (Fst pair _) = prettyApp' xs !fstD pair
-      body <- braces $ separateLoose !semiD cases
+prettyTerm xs (Snd pair _) = prettyApp' xs !sndD pair
-      pure $ sep [header, body]
+prettyTerm xs (Tag tag _) = prettyTag tag
+prettyTerm xs (CaseEnum tag 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
+  prettyCase xs pure nat
+    [MkPrettyCaseArm !zeroD  []      zer,
+     MkPrettyCaseArm !sucPat [x, ih] suc]
+where
+  sucPat = pure $
+    hsep [!succD, !(prettyTBind x) <+> !commaD, !(prettyTBind ih)]
+prettyTerm _ (Erased _) =
+  hl Syntax =<< ifUnicode "⌷" "[]"
 
-  prettyTerm _  (F x _) = prettyFree x
+export
-  prettyTerm xs (B i _) = prettyTBind $ xs !!! i
+prettyDef : {opts : LayoutOpts} -> Name ->
-  prettyTerm xs (Lam x body _) =
+            Definition -> Eff Pretty (Maybe (Doc opts))
-    parensIfM Outer =<< do
+prettyDef _    ErasedDef     = [|Nothing|]
-      header <- hsep <$> sequence [lamD, prettyTBind x, darrowD]
+prettyDef name (KeptDef rhs) = map Just $ do
-      body   <- withPrec Outer $ prettyTerm (xs :< x) body
+  name <- prettyFree name
-      hangDSingle header body
+  eq   <- cstD
-  prettyTerm xs (App fun arg _) = prettyApp xs fun arg
+  rhs  <- prettyTerm [<] rhs
-  prettyTerm xs (Pair fst snd _) =
+  hangDSingle (name <++> eq) rhs
-    parens =<< separateTight !commaD <$>
-      sequence {t = List} [prettyTerm xs fst, prettyTerm xs snd]
-  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
-    prettyCase xs prettyTag tag $ map (mapSnd $ caseArm []) 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
-    prettyCase xs pure nat
-      [(!zeroD,  caseArm []      zer),
-       (!sucPat, caseArm [x, ih] suc)]
-    where
-      sucPat = separateTight {t = List} !commaD <$>
-               sequence [[|succD <++> prettyTBind x|], prettyTBind ih]
-  prettyTerm _ (Erased _) =
-    hl Syntax =<< ifUnicode "⌷" "[]"
-
-  export
-  prettyDef : Name -> Definition -> Eff Pretty (Maybe (Doc opts))
-  prettyDef _    ErasedDef     = [|Nothing|]
-  prettyDef name (KeptDef rhs) = map Just $ do
-    name <- prettyFree name
-    eq   <- cstD
-    rhs  <- prettyTerm [<] rhs
-    hangDSingle (name <++> eq) rhs
 
 
 public export