rhi/quox
rhi/quox
1
0
Fork 0
Code Issues 15 Pull requests 1 Releases Wiki Activity

use names when pretty printing contexts

Browse source
This commit is contained in:
rhiannon morris 2023-03-31 19:30:55 +02:00
parent ad942b2fd8
commit c8fbd73ea4
1 changed files with 10 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

17
lib/Quox/Typing/Context.idr
View file

@ -220,26 +220,29 @@ parameters {auto _ : (Eq q, PrettyHL q, IsQty q)} (unicode : Bool)
pipeD = hl Syntax "|" pipeD = hl Syntax "|"
export covering export covering
prettyTContext : QContext q n -> NContext n -> TContext q d n -> Doc HL prettyTContext : NContext d ->
prettyTContext qs ns ctx = separate comma $ toList $ go qs ns ctx where QContext q n -> NContext n ->
TContext q d n -> Doc HL
prettyTContext ds qs xs ctx = separate comma $ toList $ go qs xs ctx where
go : QContext q m -> NContext m -> TContext q d m -> SnocList (Doc HL) go : QContext q m -> NContext m -> TContext q d m -> SnocList (Doc HL)
go [<] [<] [<] = [<] go [<] [<] [<] = [<]
go (qs :< q) (xs :< x) (ctx :< t) = go (qs :< q) (xs :< x) (ctx :< t) =
let bind = MkWithQty q $ MkCtxBinder x t in let bind = MkWithQty q $ MkCtxBinder x t in
go qs xs ctx :< runPretty unicode (pretty0M bind) go qs xs ctx :<
runPrettyWith unicode (toSnocList' ds) (toSnocList' xs) (pretty0M bind)
export covering export covering
prettyTyContext : TyContext q d n -> Doc HL prettyTyContext : TyContext q d n -> Doc HL
prettyTyContext (MkTyContext dctx dnames tctx tnames qtys) = prettyTyContext (MkTyContext dctx dnames tctx tnames qtys) =
case dctx of case dctx of
C [<] => prettyTContext qtys tnames tctx C [<] => prettyTContext dnames qtys tnames tctx
_ => sep [prettyDimEq dnames dctx <++> pipeD, _ => sep [prettyDimEq dnames dctx <++> pipeD,
prettyTContext qtys tnames tctx] prettyTContext dnames qtys tnames tctx]
export covering export covering
prettyEqContext : EqContext q n -> Doc HL prettyEqContext : EqContext q n -> Doc HL
prettyEqContext (MkEqContext dassign dnames tctx tnames qtys) = prettyEqContext (MkEqContext dassign dnames tctx tnames qtys) =
case dassign of case dassign of
[<] => prettyTContext qtys tnames tctx [<] => prettyTContext [<] qtys tnames tctx
_ => sep [prettyDimEq dnames (fromGround dassign) <++> pipeD, _ => sep [prettyDimEq dnames (fromGround dassign) <++> pipeD,
prettyTContext qtys tnames tctx] prettyTContext [<] qtys tnames tctx]