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

rename some things to get rid of warnings

Browse source
This commit is contained in:
rhiannon morris 2023-03-13 19:32:52 +01:00
parent 507eb79788
commit 90232dd1f8
4 changed files with 14 additions and 15 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
lib/Quox/Pretty.idr
View file

@ -226,15 +226,14 @@ prettyTermDef : PrettyHL a => a -> IO Unit
prettyTermDef = prettyTerm defPrettyOpts prettyTermDef = prettyTerm defPrettyOpts
infixr 6 <//> infixr 6 <%%>, <%>
export %inline export %inline
(<//>) : Doc a -> Doc a -> Doc a (<%%>) : Doc a -> Doc a -> Doc a
a <//> b = sep [a, b] a <%%> b = sep [a, b]
infixr 6 </>
export %inline export %inline
(</>) : Doc a -> Doc a -> Doc a (<%>) : Doc a -> Doc a -> Doc a
a </> b = cat [a, b] a <%> b = cat [a, b]

2
lib/Quox/Syntax/Dim.idr
View file

@ -86,7 +86,7 @@ public export FromVar Dim where fromVar = B
export export
inject : Dim d -> Dim (d + inj) inject : Dim d -> Dim (d + i)
inject (K e) = K e inject (K e) = K e
inject (B i) = B $ inject i inject (B i) = B $ inject i

14
lib/Quox/Syntax/Term/Pretty.idr
View file

@ -50,8 +50,8 @@ prettyBindType qtys x s arr t = do
var <- prettyQtyBinds qtys $ TV x var <- prettyQtyBinds qtys $ TV x
s <- withPrec Outer $ prettyM s s <- withPrec Outer $ prettyM s
t <- withPrec Outer $ under T x $ prettyM t t <- withPrec Outer $ under T x $ prettyM t
let bind = parens (var <++> colonD <//> hang 2 s) let bind = parens (var <++> colonD <%%> hang 2 s)
parensIfM Outer $ hang 2 $ bind <//> t parensIfM Outer $ hang 2 $ bind <%%> t
export export
prettyArm : PrettyHL a => Pretty.HasEnv m => prettyArm : PrettyHL a => Pretty.HasEnv m =>
@ -148,13 +148,13 @@ parameters (showSubsts : Bool)
prettyM (CloT s th) = prettyM (CloT s th) =
if showSubsts then if showSubsts then
parensIfM SApp . hang 2 =<< parensIfM SApp . hang 2 =<<
[|withPrec SApp (prettyM s) </> prettyTSubst th|] [|withPrec SApp (prettyM s) <%> prettyTSubst th|]
else else
prettyM $ pushSubstsWith' id th s prettyM $ pushSubstsWith' id th s
prettyM (DCloT s th) = prettyM (DCloT s th) =
if showSubsts then if showSubsts then
parensIfM SApp . hang 2 =<< parensIfM SApp . hang 2 =<<
[|withPrec SApp (prettyM s) </> prettyDSubst th|] [|withPrec SApp (prettyM s) <%> prettyDSubst th|]
else else
prettyM $ pushSubstsWith' th id s prettyM $ pushSubstsWith' th id s
@ -180,17 +180,17 @@ parameters (showSubsts : Bool)
prettyM (s :# a) = do prettyM (s :# a) = do
s <- withPrec AnnL $ prettyM s s <- withPrec AnnL $ prettyM s
a <- withPrec Ann $ prettyM a a <- withPrec Ann $ prettyM a
parensIfM Ann $ hang 2 $ s <++> !annD <//> a parensIfM Ann $ hang 2 $ s <++> !annD <%%> a
prettyM (CloE e th) = prettyM (CloE e th) =
if showSubsts then if showSubsts then
parensIfM SApp . hang 2 =<< parensIfM SApp . hang 2 =<<
[|withPrec SApp (prettyM e) </> prettyTSubst th|] [|withPrec SApp (prettyM e) <%> prettyTSubst th|]
else else
prettyM $ pushSubstsWith' id th e prettyM $ pushSubstsWith' id th e
prettyM (DCloE e th) = prettyM (DCloE e th) =
if showSubsts then if showSubsts then
parensIfM SApp . hang 2 =<< parensIfM SApp . hang 2 =<<
[|withPrec SApp (prettyM e) </> prettyDSubst th|] [|withPrec SApp (prettyM e) <%> prettyDSubst th|]
else else
prettyM $ pushSubstsWith' th id e prettyM $ pushSubstsWith' th id e

2
lib/Quox/Syntax/Var.idr
View file

@ -112,7 +112,7 @@ toFromNat (S k) (LTESucc x) = cong S $ toFromNat k x
export export
inject : Var m -> Var (m + inj) inject : Var m -> Var (m + i)
inject VZ = VZ inject VZ = VZ
inject (VS i) = VS $ inject i inject (VS i) = VS $ inject i