summaryrefslogtreecommitdiff
path: root/src/full/Agda/Syntax/Concrete/Pretty.hs
diff options
context:
space:
mode:
Diffstat (limited to 'src/full/Agda/Syntax/Concrete/Pretty.hs')
-rw-r--r--src/full/Agda/Syntax/Concrete/Pretty.hs117
1 files changed, 57 insertions, 60 deletions
diff --git a/src/full/Agda/Syntax/Concrete/Pretty.hs b/src/full/Agda/Syntax/Concrete/Pretty.hs
index c2fe806..aa86a7b 100644
--- a/src/full/Agda/Syntax/Concrete/Pretty.hs
+++ b/src/full/Agda/Syntax/Concrete/Pretty.hs
@@ -1,13 +1,14 @@
-{-# LANGUAGE CPP #-}
-{-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE TypeSynonymInstances #-}
-
{-# OPTIONS_GHC -fno-warn-orphans #-}
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE FlexibleInstances #-}
+
{-| Pretty printer for the concrete syntax.
-}
module Agda.Syntax.Concrete.Pretty where
+import Prelude hiding (null)
+
import Data.Char
import Data.Functor
import Data.Maybe
@@ -20,6 +21,8 @@ import Agda.Syntax.Literal
import Agda.Syntax.Notation
import Agda.Syntax.Position
+import Agda.Utils.Functor
+import Agda.Utils.Null
import Agda.Utils.Pretty
import Agda.Utils.String
@@ -64,28 +67,19 @@ arrow, lambda :: Doc
arrow = text "\x2192"
lambda = text "\x03bb"
-pHidden :: Pretty a => ArgInfo -> a -> Doc
-pHidden i = bracks h . pretty
- where bracks Hidden = braces'
- bracks Instance = dbraces
- bracks NotHidden= id
- h = argInfoHiding i
-
-pRelevance :: Pretty a => ArgInfo -> a -> Doc
-pRelevance i a =
- let d = pretty a
- in if render d == "_" then d else pretty (argInfoRelevance i) <> d
-{-
-pRelevance Forced a = pretty a
-pRelevance UnusedArg a = pretty a
-pRelevance Relevant a = pretty a
-pRelevance Irrelevant a =
- let d = pretty a
- in if render d == "_" then d else text "." <> d
-pRelevance NonStrict a =
- let d = pretty a
- in if render d == "_" then d else text ".." <> d
--}
+-- | @prettyHiding info visible doc@ puts the correct braces
+-- around @doc@ according to info @info@ and returns
+-- @visible doc@ if the we deal with a visible thing.
+prettyHiding :: LensHiding a => a -> (Doc -> Doc) -> Doc -> Doc
+prettyHiding a parens =
+ case getHiding a of
+ Hidden -> braces'
+ Instance -> dbraces
+ NotHidden -> parens
+
+prettyRelevance :: LensRelevance a => a -> Doc -> Doc
+prettyRelevance a d =
+ if render d == "_" then d else pretty (getRelevance a) <> d
instance (Pretty a, Pretty b) => Pretty (a, b) where
pretty (a, b) = parens $ pretty a <> comma <+> pretty b
@@ -93,8 +87,11 @@ instance (Pretty a, Pretty b) => Pretty (a, b) where
instance Pretty (ThingWithFixity Name) where
pretty (ThingWithFixity n _) = pretty n
+instance Pretty a => Pretty (WithHiding a) where
+ pretty w = prettyHiding w id $ pretty $ dget w
+
instance Pretty Relevance where
- pretty Forced = empty
+ pretty Forced{} = empty
pretty UnusedArg = empty
pretty Relevant = empty
pretty Irrelevant = text "."
@@ -123,8 +120,8 @@ instance Pretty Expr where
-- sep [ pretty e1
-- , nest 2 $ fsep $ map pretty args
-- ]
- RawApp _ es -> fsep $ map pretty es
- OpApp _ q es -> fsep $ prettyOpApp q es
+ RawApp _ es -> fsep $ map pretty es
+ OpApp _ q _ es -> fsep $ prettyOpApp q es
WithApp _ e es -> fsep $
pretty e : map ((text "|" <+>) . pretty) es
@@ -193,21 +190,18 @@ instance Pretty BoundName where
instance Pretty LamBinding where
-- TODO guilhem: colors are unused (colored syntax disallowed)
- pretty (DomainFree i x) = pRelevance i $ pHidden i $ pretty x
+ pretty (DomainFree i x) = prettyRelevance i $ prettyHiding i id $ pretty x
pretty (DomainFull b) = pretty b
instance Pretty TypedBindings where
- pretty (TypedBindings _ a) =
- pRelevance (argInfo a) $ bracks $ pretty $ WithColors (argColors a) $ unArg a
+ pretty (TypedBindings _ a) = prettyRelevance a $ prettyHiding a p $
+ pretty $ WithColors (argColors a) $ unArg a
where
- bracks = case getHiding a of
- Hidden -> braces'
- Instance -> dbraces
- NotHidden | isMeta (unArg a) -> id
- | otherwise -> parens
+ p | isUnderscore (unArg a) = id
+ | otherwise = parens
- isMeta (TBind _ _ (Underscore _ Nothing)) = True
- isMeta _ = False
+ isUnderscore (TBind _ _ (Underscore _ Nothing)) = True
+ isUnderscore _ = False
newtype Tel = Tel Telescope
@@ -247,7 +241,7 @@ instance Pretty TypedBinding where
smashTel :: Telescope -> Telescope
smashTel (TypedBindings r (Common.Arg i (TBind r' xs e)) :
TypedBindings _ (Common.Arg i' (TBind _ ys e')) : tel)
- | show i == show i' && show e == show e' && all isUnnamed (xs ++ ys) =
+ | show i == show i' && show e == show e' && all (isUnnamed . dget) (xs ++ ys) =
smashTel (TypedBindings r (Common.Arg i (TBind r' (xs ++ ys) e)) : tel)
where
isUnnamed x = boundLabel x == boundName x
@@ -305,13 +299,13 @@ instance Pretty Declaration where
pretty d =
case d of
TypeSig i x e ->
- sep [ pRelevance i $ pretty x <+> pColors ":" (argInfoColors i)
+ sep [ prettyRelevance i $ pretty x <+> pColors ":" (argInfoColors i)
, nest 2 $ pretty e
]
Field x (Common.Arg i e) ->
sep [ text "field"
- , nest 2 $ pRelevance i $ pHidden i $
- TypeSig (i {argInfoRelevance = Relevant}) x e
+ , nest 2 $ prettyRelevance i $ prettyHiding i id $
+ pretty $ TypeSig (i {argInfoRelevance = Relevant}) x e
]
FunClause lhs rhs wh ->
sep [ pretty lhs
@@ -456,9 +450,12 @@ instance Pretty Pragma where
TerminationMeasure _ x -> hsep $ [text "MEASURE", pretty x]
instance Pretty Fixity where
- pretty (LeftAssoc _ n) = text "infixl" <+> text (show n)
- pretty (RightAssoc _ n) = text "infixr" <+> text (show n)
- pretty (NonAssoc _ n) = text "infix" <+> text (show n)
+ pretty (Fixity _ n ass) = text s <+> text (show n)
+ where
+ s = case ass of
+ LeftAssoc -> "infixl"
+ RightAssoc -> "infixr"
+ NonAssoc -> "infix"
instance Pretty GenPart where
pretty (IdPart x) = text x
@@ -478,7 +475,7 @@ instance Pretty e => Pretty (Arg e) where
-- Andreas 2010-09-24: and in record fields
pretty a = -- pRelevance r $
-- TODO guilhem: print colors
- pHidden (argInfo a) $ unArg a
+ prettyHiding (argInfo a) id $ pretty $ unArg a
instance Pretty e => Pretty (Named_ e) where
pretty (Named Nothing e) = pretty e
@@ -490,19 +487,19 @@ instance Pretty [Pattern] where
instance Pretty Pattern where
pretty p =
case p of
- IdentP x -> pretty x
- AppP p1 p2 -> sep [ pretty p1, nest 2 $ pretty p2 ]
- RawAppP _ ps -> fsep $ map pretty ps
- OpAppP _ q ps -> fsep $ prettyOpApp q ps
- HiddenP _ p -> braces' $ pretty p
- InstanceP _ p -> dbraces $ pretty p
- ParenP _ p -> parens $ pretty p
- WildP _ -> underscore
- AsP _ x p -> pretty x <> text "@" <> pretty p
- DotP _ p -> text "." <> pretty p
- AbsurdP _ -> text "()"
- LitP l -> pretty l
- QuoteP _ -> text "quote"
+ IdentP x -> pretty x
+ AppP p1 p2 -> sep [ pretty p1, nest 2 $ pretty p2 ]
+ RawAppP _ ps -> fsep $ map pretty ps
+ OpAppP _ q _ ps -> fsep $ prettyOpApp q ps
+ HiddenP _ p -> braces' $ pretty p
+ InstanceP _ p -> dbraces $ pretty p
+ ParenP _ p -> parens $ pretty p
+ WildP _ -> underscore
+ AsP _ x p -> pretty x <> text "@" <> pretty p
+ DotP _ p -> text "." <> pretty p
+ AbsurdP _ -> text "()"
+ LitP l -> pretty l
+ QuoteP _ -> text "quote"
prettyOpApp :: Pretty a => QName -> [a] -> [Doc]
prettyOpApp q es = prOp ms xs es