diff --git a/lib/Quox/Parser/FromParser/Error.idr b/lib/Quox/Parser/FromParser/Error.idr index f1afbff..16a3592 100644 --- a/lib/Quox/Parser/FromParser/Error.idr +++ b/lib/Quox/Parser/FromParser/Error.idr @@ -139,7 +139,7 @@ parameters {opts : LayoutOpts} (showContext : Bool) prettyError (WrongFail str err loc) = pure $ vsep [!(prettyLoc loc), - "wrong error, expected to match", !(hl Tag $ text "\"\{str}\""), + "wrong error, expected to match", !(hl Constant $ text "\"\{str}\""), "but got", !(prettyError err)] prettyError (WrapParseError file err) = diff --git a/lib/Quox/Pretty.idr b/lib/Quox/Pretty.idr index b2ab4b9..e6f4a17 100644 --- a/lib/Quox/Pretty.idr +++ b/lib/Quox/Pretty.idr @@ -41,7 +41,7 @@ data HL | Dim | DVar | DVarErr | Qty | Universe | Syntax -| Tag +| Constant %runElab derive "HL" [Eq, Ord, Show] @@ -86,7 +86,7 @@ toSGR DVarErr = [SetForeground BrightGreen, SetStyle SingleUnderline] toSGR Qty = [SetForeground BrightMagenta] toSGR Universe = [SetForeground BrightRed] toSGR Syntax = [SetForeground BrightCyan] -toSGR Tag = [SetForeground BrightRed] +toSGR Constant = [SetForeground BrightRed] export %inline highlightSGR : HL -> Highlight @@ -262,25 +262,25 @@ eqndD = hl Delim . text =<< ifUnicode "≡" "==" dlamD = hl Syntax . text =<< ifUnicode "δ" "dfun" annD = hl Delim . text =<< ifUnicode "∷" "::" natD = hl Syntax . text =<< ifUnicode "ℕ" "Nat" -stringD = hl Syntax $ text "String" -eqD = hl Syntax $ text "Eq" -colonD = hl Delim $ text ":" -commaD = hl Delim $ text "," -semiD = hl Delim $ text ";" -caseD = hl Syntax $ text "case" -typecaseD = hl Syntax $ text "type-case" -ofD = hl Syntax $ text "of" -returnD = hl Syntax $ text "return" -dotD = hl Delim $ text "." -zeroD = hl Syntax $ text "zero" -succD = hl Syntax $ text "succ" -coeD = hl Syntax $ text "coe" -compD = hl Syntax $ text "comp" -undD = hl Syntax $ text "_" -cstD = hl Syntax $ text "=" -pipeD = hl Syntax $ text "|" -fstD = hl Syntax $ text "fst" -sndD = hl Syntax $ text "snd" +stringD = hl Syntax $ text "String" +eqD = hl Syntax $ text "Eq" +colonD = hl Delim $ text ":" +commaD = hl Delim $ text "," +semiD = hl Delim $ text ";" +caseD = hl Syntax $ text "case" +typecaseD = hl Syntax $ text "type-case" +ofD = hl Syntax $ text "of" +returnD = hl Syntax $ text "return" +dotD = hl Delim $ text "." +zeroD = hl Constant $ text "zero" +succD = hl Constant $ text "succ" +coeD = hl Syntax $ text "coe" +compD = hl Syntax $ text "comp" +undD = hl Syntax $ text "_" +cstD = hl Syntax $ text "=" +pipeD = hl Syntax $ text "|" +fstD = hl Syntax $ text "fst" +sndD = hl Syntax $ text "snd" export @@ -330,13 +330,13 @@ prettyLoc (L (YesLoc file b)) = export prettyTag : {opts : _} -> String -> Eff Pretty (Doc opts) -prettyTag tag = hl Tag $ text $ "'" ++ quoteTag tag +prettyTag tag = hl Constant $ text $ "'" ++ quoteTag tag export prettyStrLit : {opts : _} -> String -> Eff Pretty (Doc opts) prettyStrLit s = let s = concatMap esc1 $ unpack s in - hl Syntax $ hcat ["\"", text s, "\""] + hl Constant $ hcat ["\"", text s, "\""] where esc1 : Char -> String esc1 '"' = "\""; esc1 '\\' = "\\" diff --git a/lib/Quox/Syntax/Term/Pretty.idr b/lib/Quox/Syntax/Term/Pretty.idr index a2629de..ffdb3e9 100644 --- a/lib/Quox/Syntax/Term/Pretty.idr +++ b/lib/Quox/Syntax/Term/Pretty.idr @@ -287,7 +287,7 @@ prettyEnum : {opts : _} -> List String -> Eff Pretty (Doc opts) prettyEnum cases = tightBraces =<< fillSeparateTight !commaD <$> - traverse (hl Tag . Doc.text . quoteTag) cases + traverse (hl Constant . Doc.text . quoteTag) cases private prettyCaseRet : {opts : _} -> diff --git a/lib/Quox/Untyped/Scheme.idr b/lib/Quox/Untyped/Scheme.idr index 3379267..61ca482 100644 --- a/lib/Quox/Untyped/Scheme.idr +++ b/lib/Quox/Untyped/Scheme.idr @@ -363,9 +363,9 @@ prettySexp (L (x :: xs)) = do parens $ ifMultiline (hsep $ d :: ds) (hsep [d, vsep ds] <|> vsep (d :: map (indent 2) ds)) -prettySexp (Q (V x)) = hl Tag $ "'" <+> prettyId' x -prettySexp (Q x) = pure $ hcat [!(hl Tag "'"), !(prettySexp x)] -prettySexp (N n) = hl Tag $ pshow n +prettySexp (Q (V x)) = hl Constant $ "'" <+> prettyId' x +prettySexp (Q x) = pure $ hcat [!(hl Constant "'"), !(prettySexp x)] +prettySexp (N n) = hl Constant $ pshow n prettySexp (S s) = prettyStrLit $ escape s prettySexp (Lambda xs e) = prettyLambda "lambda" xs e prettySexp (LambdaC xs e) = prettyLambda "lambda%" xs e diff --git a/lib/Quox/Untyped/Syntax.idr b/lib/Quox/Untyped/Syntax.idr index 1697a66..da660cd 100644 --- a/lib/Quox/Untyped/Syntax.idr +++ b/lib/Quox/Untyped/Syntax.idr @@ -226,7 +226,7 @@ prettyTerm xs (CaseEnum tag cases _) = prettyCase xs prettyTag tag $ map (\(t, rhs) => MkPrettyCaseArm t [] rhs) $ toList cases prettyTerm xs (Absurd _) = hl Syntax "absurd" -prettyTerm xs (Nat n _) = hl Tag $ pshow n +prettyTerm xs (Nat n _) = hl Constant $ pshow n prettyTerm xs (Succ nat _) = prettyApp xs !succD [< nat] prettyTerm xs (CaseNat nat zer suc _) = prettyCase xs pure nat [MkPrettyCaseArm !zeroD [] zer, !(sucCaseArm suc)]