From 8d7326917a1210b595bc13793236a1ade5a0ac7e Mon Sep 17 00:00:00 2001 From: rhiannon morris Date: Sat, 21 Oct 2023 20:49:29 +0200 Subject: [PATCH] more erasure --- lib/Quox/Untyped/Erase.idr | 21 +++-- lib/Quox/Untyped/Syntax.idr | 153 +++++++++++++++++++----------------- 2 files changed, 95 insertions(+), 79 deletions(-) diff --git a/lib/Quox/Untyped/Erase.idr b/lib/Quox/Untyped/Erase.idr index d14766d..8118920 100644 --- a/lib/Quox/Untyped/Erase.idr +++ b/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 - (WrapTypeError err).loc = err.loc - (Postulate loc _).loc = loc + (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 diff --git a/lib/Quox/Untyped/Syntax.idr b/lib/Quox/Untyped/Syntax.idr index daea0a7..e4f67e4 100644 --- a/lib/Quox/Untyped/Syntax.idr +++ b/lib/Quox/Untyped/Syntax.idr @@ -73,85 +73,94 @@ public export Definitions = SortedMap Name Definition -parameters {opts : LayoutOpts} - export - prettyTerm : BContext n -> Term n -> Eff Pretty (Doc opts) +export +prettyTerm : {opts : LayoutOpts} -> BContext n -> + Term n -> Eff Pretty (Doc opts) - export - prettyArg : BContext n -> Term n -> Eff Pretty (Doc opts) - prettyArg xs arg = withPrec Arg $ prettyTerm xs arg +export +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' xs fun arg = - parensIfM App =<< do - arg <- prettyArg xs arg - pure $ sep [fun, arg] +export +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 xs fun arg = prettyApp' xs !(prettyArg xs fun) arg +export +prettyApp : {opts : LayoutOpts} -> BContext n -> + 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 - PrettyCaseArm n = Exists $ \s => (Vect s BindName, Term (s + n)) +public export +record PrettyCaseArm a n where + constructor MkPrettyCaseArm + lhs : a + {len : Nat} + vars : Vect len BindName + rhs : Term (len + n) - export %inline - caseArm : Vect s BindName -> Term (s + n) -> PrettyCaseArm n - caseArm xs t = Evidence _ (xs, t) +export +prettyCase : {opts : LayoutOpts} -> BContext n -> + (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 - prettyCase : Context' BindName n -> - (a -> Eff Pretty (Doc opts)) -> - Term n -> List (a, PrettyCaseArm n) -> - Eff Pretty (Doc opts) - prettyCase xs f head arms = - parensIfM Outer =<< Prelude.do - header <- hsep <$> sequence [caseD, prettyTerm xs head, ofD] - cases <- for arms $ \(lhs, (Evidence s (ys, rhs))) => do - lhs <- hsep <$> sequence [f lhs, darrowD] - rhs <- withPrec Outer $ prettyTerm (xs <>< ys) rhs - hangDSingle lhs rhs - body <- braces $ separateLoose !semiD cases - pure $ sep [header, body] +prettyTerm _ (F x _) = prettyFree x +prettyTerm xs (B i _) = prettyTBind $ xs !!! i +prettyTerm xs (Lam x body _) = + parensIfM Outer =<< do + header <- hsep <$> sequence [lamD, prettyTBind x, darrowD] + body <- withPrec Outer $ prettyTerm (xs :< x) body + hangDSingle header body +prettyTerm xs (App fun arg _) = prettyApp xs fun arg +prettyTerm xs (Pair fst snd _) = + 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 (\(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 - prettyTerm xs (B i _) = prettyTBind $ xs !!! i - prettyTerm xs (Lam x body _) = - parensIfM Outer =<< do - header <- hsep <$> sequence [lamD, prettyTBind x, darrowD] - body <- withPrec Outer $ prettyTerm (xs :< x) body - hangDSingle header body - prettyTerm xs (App fun arg _) = prettyApp xs fun arg - prettyTerm xs (Pair fst snd _) = - 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 +export +prettyDef : {opts : LayoutOpts} -> 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