make p,q in coe/comp optional and default to @0 @1

This commit is contained in:
rhiannon morris 2023-05-15 19:57:10 +02:00
parent 7b93a913c7
commit d631b86be3
7 changed files with 73 additions and 31 deletions

View File

@ -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

View File

@ -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 @𝑗 };

View File

@ -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 : ) =

View File

@ -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 ";"

View File

@ -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

View File

@ -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.

View File

@ -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 { }"