From d631b86be35a864c25626272893aaa43d692eae1 Mon Sep 17 00:00:00 2001 From: rhiannon morris Date: Mon, 15 May 2023 19:57:10 +0200 Subject: [PATCH] make p,q in coe/comp optional and default to @0 @1 --- examples/bool.quox | 2 +- examples/misc.quox | 4 +-- examples/nat.quox | 2 +- lib/Quox/Parser/Parser.idr | 19 +++++++--- lib/Quox/Syntax/Term/Pretty.idr | 63 ++++++++++++++++++++++----------- syntax.ebnf | 6 ++-- tests/Tests/Parser.idr | 8 +++++ 7 files changed, 73 insertions(+), 31 deletions(-) diff --git a/examples/bool.quox b/examples/bool.quox index 5de0f0a..c8d7f2f 100644 --- a/examples/bool.quox +++ b/examples/bool.quox @@ -17,7 +17,7 @@ def0 If : 1.Bool → 0.★₀ → 0.★₀ → ★₀ = def0 T : ω.Bool → ★₀ = λ b ⇒ If b True False; def true-not-false : Not ('true ≡ 'false : Bool) = - λ eq ⇒ coe [i ⇒ T (eq @i)] @0 @1 'true; + λ eq ⇒ coe [i ⇒ T (eq @i)] 'true; -- [todo] infix diff --git a/examples/misc.quox b/examples/misc.quox index f6ba7d9..646168f 100644 --- a/examples/misc.quox +++ b/examples/misc.quox @@ -28,9 +28,9 @@ def funext : λ A P p q eq ⇒ δ 𝑖 ⇒ λ x ⇒ eq x @𝑖; def sym : 0.(A : ★₀) → 0.(x y : A) → 1.(x ≡ y : A) → y ≡ x : A = - λ A x y eq ⇒ δ 𝑖 ⇒ comp [A] @0 @1 (eq @0) @𝑖 { 0 𝑗 ⇒ eq @𝑗; 1 _ ⇒ eq @0 }; + λ A x y eq ⇒ δ 𝑖 ⇒ comp [A] (eq @0) @𝑖 { 0 𝑗 ⇒ eq @𝑗; 1 _ ⇒ eq @0 }; def trans : 0.(A : ★₀) → 0.(x y z : A) → ω.(x ≡ y : A) → ω.(y ≡ z : A) → x ≡ z : A = λ A x y z eq1 eq2 ⇒ δ 𝑖 ⇒ - comp [A] @0 @1 (eq1 @𝑖) @𝑖 { 0 _ ⇒ eq1 @0; 1 𝑗 ⇒ eq2 @𝑗 }; + comp [A] (eq1 @𝑖) @𝑖 { 0 _ ⇒ eq1 @0; 1 𝑗 ⇒ eq2 @𝑗 }; diff --git a/examples/nat.quox b/examples/nat.quox index 37acff0..7c2b538 100644 --- a/examples/nat.quox +++ b/examples/nat.quox @@ -51,7 +51,7 @@ def zero-not-succ : 0.(m : ℕ) → Not (zero ≡ succ m : ℕ) = λ m eq ⇒ coe [𝑖 ⇒ IsSucc (eq @𝑖)] @1 @0 'true; def succ-not-zero : 0.(m : ℕ) → Not (succ m ≡ zero : ℕ) = - λ m eq ⇒ coe [𝑖 ⇒ IsSucc (eq @𝑖)] @0 @1 'true; + λ m eq ⇒ coe [𝑖 ⇒ IsSucc (eq @𝑖)] 'true; def0 not-succ-self : 0.(m : ℕ) → Not (m ≡ succ m : ℕ) = diff --git a/lib/Quox/Parser/Parser.idr b/lib/Quox/Parser/Parser.idr index b27816f..7eaa5da 100644 --- a/lib/Quox/Parser/Parser.idr +++ b/lib/Quox/Parser/Parser.idr @@ -287,12 +287,22 @@ termArg fname = withLoc fname $ <|> [|V qname|] <|> const <$> tupleTerm fname +||| optionally, two dimension arguments. if absent default to `@0 @1` +private +optDirection : FileName -> Grammar False (PDim, PDim) +optDirection fname = withLoc fname $ do + dims <- optional [|(,) (dimArg fname) (dimArg fname)|] + pure $ \loc => fromMaybe (K Zero loc, K One loc) dims + export coeTerm : FileName -> Grammar True PTerm coeTerm fname = withLoc fname $ do resC "coe" - mustWork [|Coe (typeLine fname) (dimArg fname) (dimArg fname) - (termArg fname)|] + mustWork $ do + line <- typeLine fname + (p, q) <- optDirection fname + val <- termArg fname + pure $ Coe line p q val public export CompBranch : Type @@ -301,8 +311,7 @@ CompBranch = (DimConst, PatVar, PTerm) export compBranch : FileName -> Grammar True CompBranch compBranch fname = - [|(,,) dimConst (patVar fname) - (needRes "⇒" *> assert_total term fname)|] + [|(,,) dimConst (patVar fname) (needRes "⇒" *> assert_total term fname)|] private checkCompTermBody : (PatVar, PTerm) -> PDim -> PDim -> PTerm -> PDim -> @@ -321,7 +330,7 @@ compTerm fname = withLoc fname $ do resC "comp" mustWork $ do a <- typeLine fname - p <- dimArg fname; q <- dimArg fname + (p, q) <- optDirection fname s <- termArg fname; r <- dimArg fname bodyStart <- bounds $ needRes "{" s0 <- compBranch fname; needRes ";" diff --git a/lib/Quox/Syntax/Term/Pretty.idr b/lib/Quox/Syntax/Term/Pretty.idr index d24a854..a8b042e 100644 --- a/lib/Quox/Syntax/Term/Pretty.idr +++ b/lib/Quox/Syntax/Term/Pretty.idr @@ -253,6 +253,26 @@ private prettyCompPat : {opts : _} -> DimConst -> BindName -> Eff Pretty (Doc opts) prettyCompPat e x = [|prettyDimConst e <++> prettyDBind x|] +private +prettyCompArm : {opts : _} -> BContext d -> BContext n -> + DimConst -> DScopeTerm d n -> Eff Pretty (Doc opts) +prettyCompArm dnames tnames e s = prettyCaseArm dnames tnames $ + MkCaseArm !(prettyCompPat e s.name) [< s.name] [<] s.term + +private +layoutComp : {opts : _} -> + (typq : List (Doc opts)) -> (val, r : Doc opts) -> + (arms : List (Doc opts)) -> Eff Pretty (Doc opts) +layoutComp typq val r arms = do + comp <- compD; lb <- hl Delim "{"; rb <- hl Delim "}" + ind <- askAt INDENT + pure $ ifMultiline + (hsep $ concat {t = List} [[comp], typq, [val, r, lb], arms, [rb]]) $ + (comp <++> + vsep [sep typq, val, r <++> lb, indent ind $ vsep arms, rb]) <|> + (vsep $ (comp ::) $ map (indent ind) $ concat {t = List} + [typq, [val, r <++> lb], map (indent ind) arms, [rb]]) + export prettyTag : {opts : _} -> String -> Eff Pretty (Doc opts) @@ -296,6 +316,12 @@ prettyCase dnames tnames qty head ret body = prettyCase_ dnames tnames ![|caseD <+> prettyQty qty|] head ret body +private +isDefaultDir : Dim d -> Dim d -> Bool +isDefaultDir (K Zero _) (K One _) = True +isDefaultDir _ _ = False + + -- [fixme] use telescopes in Scoped private toTel : BContext s -> BTelescope n (s + n) @@ -477,33 +503,30 @@ prettyElim dnames tnames (Ann tm ty _) = !(withPrec Outer (prettyTerm dnames tnames ty)) prettyElim dnames tnames (Coe ty p q val _) = - parensIfM App =<< do - ty <- prettyTypeLine dnames tnames ty - p <- prettyDArg dnames p - q <- prettyDArg dnames q - val <- prettyTArg dnames tnames val - prettyAppD !coeD [ty, sep [p, q], val] + parensIfM App =<< + if isDefaultDir p q then do + ty <- prettyTypeLine dnames tnames ty + val <- prettyTArg dnames tnames val + prettyAppD !coeD [ty, val] + else do + ty <- prettyTypeLine dnames tnames ty + p <- prettyDArg dnames p + q <- prettyDArg dnames q + val <- prettyTArg dnames tnames val + prettyAppD !coeD [ty, sep [p, q], val] prettyElim dnames tnames e@(Comp ty p q val r zero one _) = parensIfM App =<< do ty <- prettyTypeLine dnames tnames $ assert_smaller e $ SN ty - p <- prettyDArg dnames p - q <- prettyDArg dnames q + pq <- sep <$> sequence [prettyDArg dnames p, prettyDArg dnames q] val <- prettyTArg dnames tnames val r <- prettyDArg dnames r - comp <- compD; lb <- hl Delim "{"; rb <- hl Delim "}"; sc <- semiD - arm0 <- map (<+> sc) $ prettyCaseArm dnames tnames $ - MkCaseArm !(prettyCompPat Zero zero.name) [< zero.name] [<] zero.term - arm1 <- prettyCaseArm dnames tnames $ - MkCaseArm !(prettyCompPat One one.name) [< one.name] [<] one.term + arm0 <- [|prettyCompArm dnames tnames Zero zero <+> semiD|] + arm1 <- prettyCompArm dnames tnames One one ind <- askAt INDENT - pure $ ifMultiline - (hsep [comp, ty, p, q, val, r, lb, arm0, arm1, rb]) - (comp <++> vsep [sep [ty, sep [p, q]], val, r <++> lb, - indent ind $ vsep [arm0, arm1], rb] <|> - vsep (comp :: map (indent ind) - [ty, sep [p, q], val, r <++> lb, - indent ind $ vsep [arm0, arm1], rb])) + if isDefaultDir p q + then layoutComp [ty] val r [arm0, arm1] + else layoutComp [ty, pq] val r [arm0, arm1] prettyElim dnames tnames (TypeCase ty ret arms def _) = do arms <- for (toList arms) $ \(k ** body) => do diff --git a/syntax.ebnf b/syntax.ebnf index 685e923..426416c 100644 --- a/syntax.ebnf +++ b/syntax.ebnf @@ -54,10 +54,12 @@ dep eq = "Eq", type line, term arg, term arg. succ = "succ", term arg. normal app = term arg, {term arg | dim arg}. -coe = "coe", type line, dim arg, dim arg, term arg. +(* direction defaults to @0 @1 *) +coe = "coe", type line, [dim arg, dim arg], term arg. type line = "[", [pat var, "⇒"], term, "]". -comp = "comp", type line, dim arg, dim arg, term arg, dim arg, comp body. +comp = "comp", type line, [dim arg, dim arg], + term arg, dim arg, comp body. comp body = "{", comp branch, ";", comp branch, [";"], "}". comp branch = dim const, name, "⇒", term. diff --git a/tests/Tests/Parser.idr b/tests/Tests/Parser.idr index 54d22b5..a41d32f 100644 --- a/tests/Tests/Parser.idr +++ b/tests/Tests/Parser.idr @@ -290,6 +290,8 @@ tests = "parser" :- [ `(Coe (Unused _, V "A" _) (V "p" _) (V "q" _) (V "x" _) _), parseMatch term "coe [i ⇒ A] @p @q x" `(Coe (PV "i" _, V "A" _) (V "p" _) (V "q" _) (V "x" _) _), + parseMatch term "coe [A] x" + `(Coe (Unused _, V "A" _) (K Zero _) (K One _) (V "x" _) _), parseFails term "coe [A] @p @q", parseFails term "coe A @p @q x", parseFails term "coe [i ⇒ A] @p q x" @@ -299,9 +301,15 @@ tests = "parser" :- [ parseMatch term "comp [A] @p @q s @r { 0 𝑗 ⇒ s₀; 1 𝑘 ⇒ s₁ }" `(Comp (Unused _, V "A" _) (V "p" _) (V "q" _) (V "s" _) (V "r" _) (PV "𝑗" _, V "s₀" _) (PV "𝑘" _, V "s₁" _) _), + parseMatch term "comp [𝑖 ⇒ A] @p @q s @r { 0 𝑗 ⇒ s₀; 1 𝑘 ⇒ s₁ }" + `(Comp (PV "𝑖" _, V "A" _) (V "p" _) (V "q" _) (V "s" _) (V "r" _) + (PV "𝑗" _, V "s₀" _) (PV "𝑘" _, V "s₁" _) _), parseMatch term "comp [A] @p @q s @r { 1 𝑗 ⇒ s₀; 0 𝑘 ⇒ s₁; }" `(Comp (Unused _, V "A" _) (V "p" _) (V "q" _) (V "s" _) (V "r" _) (PV "𝑘" _, V "s₁" _) (PV "𝑗" _, V "s₀" _) _), + parseMatch term "comp [A] s @r { 0 𝑗 ⇒ s₀; 1 𝑘 ⇒ s₁ }" + `(Comp (Unused _, V "A" _) (K Zero _) (K One _) (V "s" _) (V "r" _) + (PV "𝑗" _, V "s₀" _) (PV "𝑘" _, V "s₁" _) _), parseFails term "comp [A] @p @q s @r { 1 𝑗 ⇒ s₀; 1 𝑘 ⇒ s₁; }", parseFails term "comp [A] @p @q s @r { 0 𝑗 ⇒ s₀ }", parseFails term "comp [A] @p @q s @r { }"