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

WIP: quantity polymorphism #44

Draft
rhi wants to merge 9 commits from qpoly into 🐉
pull from: qpoly
merge into: rhi:🐉
Conversation 0 Commits 9 Files changed 34 +3 -7
1 changed files with 3 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files
Showing only changes of commit d9a383d8bb - Show all commits

10
lib/Quox/Pretty.idr
View file

@ -37,8 +37,8 @@ data PPrec
public export public export
data HL data HL
= Delim = Delim
| Free | TVar | TVarErr | Free | TVar
| Dim | DVar | DVarErr | Dim | DVar
| Qty | Universe | Qty | Universe
| Syntax | Syntax
| Constant | Constant
@ -79,10 +79,8 @@ toSGR : HL -> List SGR
toSGR Delim = [] toSGR Delim = []
toSGR Free = [SetForeground BrightBlue] toSGR Free = [SetForeground BrightBlue]
toSGR TVar = [SetForeground BrightYellow] toSGR TVar = [SetForeground BrightYellow]
toSGR TVarErr = [SetForeground BrightYellow, SetStyle SingleUnderline]
toSGR Dim = [SetForeground BrightGreen] toSGR Dim = [SetForeground BrightGreen]
toSGR DVar = [SetForeground BrightGreen] toSGR DVar = [SetForeground BrightGreen]
toSGR DVarErr = [SetForeground BrightGreen, SetStyle SingleUnderline]
toSGR Qty = [SetForeground BrightMagenta] toSGR Qty = [SetForeground BrightMagenta]
toSGR Universe = [SetForeground BrightRed] toSGR Universe = [SetForeground BrightRed]
toSGR Syntax = [SetForeground BrightCyan] toSGR Syntax = [SetForeground BrightCyan]
@ -97,10 +95,8 @@ toClass : HL -> String
toClass Delim = "dl" toClass Delim = "dl"
toClass Free = "fr" toClass Free = "fr"
toClass TVar = "tv" toClass TVar = "tv"
toClass TVarErr = "tv err"
toClass Dim = "dc" toClass Dim = "dc"
toClass DVar = "dv" toClass DVar = "dv"
toClass DVarErr = "dv err"
toClass Qty = "qt" toClass Qty = "qt"
toClass Universe = "un" toClass Universe = "un"
toClass Syntax = "sy" toClass Syntax = "sy"
@ -345,7 +341,7 @@ prettyBounds (MkBounds l1 c1 l2 c2) =
export export
prettyLoc : {opts : LayoutOpts} -> Loc -> Eff Pretty (Doc opts) prettyLoc : {opts : LayoutOpts} -> Loc -> Eff Pretty (Doc opts)
prettyLoc (L NoLoc) = prettyLoc (L NoLoc) =
hcat <$> sequence [hl TVarErr "no location", colonD] hcat <$> sequence [hl TVar "no location", colonD]
prettyLoc (L (YesLoc file b)) = prettyLoc (L (YesLoc file b)) =
hcat <$> sequence [hl Free $ text file, colonD, prettyBounds b] hcat <$> sequence [hl Free $ text file, colonD, prettyBounds b]