{-# OPTIONS_GHC -Wno-orphans #-} -- | This module contains 'Pretty' instances for the Agda AST. -- -- The Agda library has its own 'Agda.Pretty' class in "Agda.Utils.Pretty". -- Therefore we cannot instance every @a@ with an @Agda.Pretty@ instance with -- our 'Pretty' instance without generating overlapping instances for basic -- types (e.g. 'String'). -- We introduce the wrapper datatype 'PrettyAgda' to avoid the overlapping -- instances and explicitly declare 'Pretty' instances for common AST -- nodes. module FreeC.Backend.Agda.Pretty ( prettyAgda ) where -- We just need the pretty instances from 'Agda.Syntax.Concrete.Pretty'. import qualified Agda.Syntax.Concrete.Pretty () import qualified Agda.Utils.Pretty as Agda import qualified FreeC.Backend.Agda.Syntax as Agda import FreeC.Pretty -- | Wrapper data type that makes any 'Agda.Pretty' instance pretty printable. newtype PrettyAgda a = PrettyAgda { unPrettyAgda :: a } -- | Pretty instance for all Agda internal, pretty printable types. instance (Agda.Pretty a) => Pretty (PrettyAgda a) where pretty = prettyString . Agda.prettyShow . unPrettyAgda -- | Helper function for printing 'Agda.Pretty' printable types @a@ to a 'Doc' -- from the pretty printing library, which is used by the compiler. prettyAgda :: (Agda.Pretty a) => a -> Doc prettyAgda = pretty . PrettyAgda -- | 'Agda.Expr's are a common AST node. instance Pretty Agda.Expr where pretty = prettyAgda -- | 'Agda.Declaration's are a common AST node. instance Pretty Agda.Declaration where pretty = prettyAgda