{-# OPTIONS_GHC -fno-warn-orphans #-}

{-# LANGUAGE CPP #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}

{-| Pretty printer for the concrete syntax.
-}
module Agda.Syntax.Concrete.Pretty where

import Prelude hiding (null)

import Data.Functor
import Data.Maybe
import qualified Data.Strict.Maybe as Strict

import Agda.Syntax.Common
import Agda.Syntax.Concrete
import Agda.Syntax.Fixity
import Agda.Syntax.Notation
import Agda.Syntax.Position

import Agda.Utils.Functor
import Agda.Utils.Null
import Agda.Utils.Pretty
import Agda.Utils.String

#include "undefined.h"
import Agda.Utils.Impossible

instance Show Expr            where show = show . pretty
instance Show Declaration     where show = show . pretty
instance Show Pattern         where show = show . pretty
instance Show TypedBinding    where show = show . pretty
instance Show TypedBindings   where show = show . pretty
instance Show LamBinding      where show = show . pretty
instance (Pretty a, Pretty b) => Show (ImportDirective' a b)
                              where show = show . pretty
instance Show Pragma          where show = show . pretty
instance Show RHS             where show = show . pretty

braces' :: Doc -> Doc
braces' d = case render d of
  -- Add space to avoid starting a comment
  '-':_ -> braces (text " " <> d)
  _     -> braces d

-- double braces...
dbraces :: Doc -> Doc
dbraces = braces . braces'

-- Lays out a list of documents [d₁, d₂, …] in the following way:
-- @
--   { d₁
--   ; d₂
--   ⋮
--   }
-- @
-- If the list is empty, then the notation @{}@ is used.

bracesAndSemicolons :: [Doc] -> Doc
bracesAndSemicolons []       = text "{}"
bracesAndSemicolons (d : ds) =
  sep ([text "{" <+> d] ++ map (text ";" <+>) ds ++ [text "}"])

arrow, lambda :: Doc
arrow  = text "\x2192"
lambda = text "\x03bb"

-- | @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

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 UnusedArg  = empty
  pretty Relevant   = empty
  pretty Irrelevant = text "."
  pretty NonStrict  = text ".."

instance Pretty Induction where
  pretty Inductive = text "data"
  pretty CoInductive = text "codata"

instance Pretty (OpApp Expr) where
  pretty (Ordinary e) = pretty e
  pretty (SyntaxBindingLambda r bs e) = pretty (Lam r bs e)

instance Pretty a => Pretty (MaybePlaceholder a) where
  pretty Placeholder{}       = text "_"
  pretty (NoPlaceholder _ e) = pretty e

instance Pretty Expr where
    pretty e =
        case e of
            Ident x          -> pretty x
            Lit l            -> pretty l
            QuestionMark _ n -> text "?" <> maybe empty (text . show) n
            Underscore _ n   -> maybe underscore text n
--          Underscore _ n   -> underscore <> maybe empty (text . show) n
            App _ _ _        ->
                case appView e of
                    AppView e1 args     ->
                        fsep $ pretty e1 : map pretty args
--                      sep [ pretty e1
--                          , nest 2 $ fsep $ map pretty args
--                          ]
            RawApp _ es    -> fsep $ map pretty es
            OpApp _ q _ es -> fsep $ prettyOpApp q es

            WithApp _ e es -> fsep $
              pretty e : map ((text "|" <+>) . pretty) es

            HiddenArg _ e -> braces' $ pretty e
            InstanceArg _ e -> dbraces $ pretty e
            Lam _ bs e ->
                sep [ lambda <+> fsep (map pretty bs) <+> arrow
                    , nest 2 $ pretty e
                    ]
            AbsurdLam _ NotHidden -> lambda <+> text "()"
            AbsurdLam _ Instance -> lambda <+> text "{{}}"
            AbsurdLam _ Hidden -> lambda <+> text "{}"
            ExtendedLam _ pes ->
              lambda <+> bracesAndSemicolons (map (\(x,y,z,_) -> prettyClause x y z) pes)
                   where prettyClause lhs rhs wh = sep [ pretty lhs
                                                       , nest 2 $ pretty' rhs
                                                       ] $$ nest 2 (pretty wh)
                         pretty' (RHS e)   = arrow <+> pretty e
                         pretty' AbsurdRHS = empty
            Fun _ e1 e2 ->
                sep [ pretty e1 <+> arrow
                    , pretty e2
                    ]
            Pi tel e ->
                sep [ pretty (Tel $ smashTel tel) <+> arrow
                    , pretty e
                    ]
            Set _   -> text "Set"
            Prop _  -> text "Prop"
            SetN _ n    -> text "Set" <> text (showIndex n)
            Let _ ds e  ->
                sep [ text "let" <+> vcat (map pretty ds)
                    , text "in" <+> pretty e
                    ]
            Paren _ e -> parens $ pretty e
            As _ x e  -> pretty x <> text "@" <> pretty e
            Dot _ e   -> text "." <> pretty e
            Absurd _  -> text "()"
            Rec _ xs  -> sep [text "record", bracesAndSemicolons (map pretty xs)]
            RecUpdate _ e xs ->
              sep [text "record" <+> pretty e, bracesAndSemicolons (map pretty xs)]
            ETel []  -> text "()"
            ETel tel -> fsep $ map pretty tel
            QuoteGoal _ x e -> sep [text "quoteGoal" <+> pretty x <+> text "in",
                                    nest 2 $ pretty e]
            QuoteContext _ -> text "quoteContext"
            Quote _ -> text "quote"
            QuoteTerm _ -> text "quoteTerm"
            Unquote _ -> text "unquote"
            Tactic _ t es ->
              sep [ text "tactic" <+> pretty t
                  , fsep [ text "|" <+> pretty e | e <- es ]
                  ]
            -- Andreas, 2011-10-03 print irrelevant things as .(e)
            DontCare e -> text "." <> parens (pretty e)
            Equal _ a b -> pretty a <+> text "=" <+> pretty b

instance (Pretty a, Pretty b) => Pretty (Either a b) where
  pretty = either pretty pretty

instance Pretty a => Pretty (FieldAssignment' a) where
  pretty (FieldAssignment x e) = sep [ pretty x <+> text "=" , nest 2 $ pretty e ]

instance Pretty ModuleAssignment where
  pretty (ModuleAssignment m es i) = (fsep $ pretty m : map pretty es) <+> pretty i

instance Pretty BoundName where
  pretty BName{ boundName = x, boundLabel = l }
    | x == l    = pretty x
    | otherwise = pretty l <+> text "=" <+> pretty x

instance Pretty LamBinding where
    -- TODO guilhem: colors are unused (colored syntax disallowed)
    pretty (DomainFree i x) = prettyRelevance i $ prettyHiding i id $ pretty x
    pretty (DomainFull b)   = pretty b

instance Pretty TypedBindings where
  pretty (TypedBindings _ a) = prettyRelevance a $ prettyHiding a p $
    pretty $ unArg a
      where
        p | isUnderscore (unArg a) = id
          | otherwise        = parens

        isUnderscore (TBind _ _ (Underscore _ Nothing)) = True
        isUnderscore _ = False

newtype Tel = Tel Telescope

instance Pretty Tel where
    pretty (Tel tel)
      | any isMeta tel = text "∀" <+> fsep (map pretty tel)
      | otherwise      = fsep (map pretty tel)
      where
        isMeta (TypedBindings _ (Arg _ (TBind _ _ (Underscore _ Nothing)))) = True
        isMeta _ = False


instance Pretty TypedBinding where
    pretty (TBind _ xs (Underscore _ Nothing)) =
      fsep (map pretty xs)
    pretty (TBind _ xs e) =
        sep [ fsep (map pretty xs)
            , text ":" <+> pretty e
            ]
    pretty (TLet _ ds) =
        text "let" <+> vcat (map pretty ds)

smashTel :: Telescope -> Telescope
smashTel (TypedBindings r (Arg i  (TBind r' xs e)) :
          TypedBindings _ (Arg i' (TBind _  ys e')) : tel)
  | show i == show i' && show e == show e' && all (isUnnamed . dget) (xs ++ ys) =
    smashTel (TypedBindings r (Arg i (TBind r' (xs ++ ys) e)) : tel)
  where
    isUnnamed x = boundLabel x == boundName x
smashTel (b : tel) = b : smashTel tel
smashTel [] = []


instance Pretty RHS where
    pretty (RHS e)   = text "=" <+> pretty e
    pretty AbsurdRHS = empty

instance Show WhereClause where show = show . pretty
instance Pretty WhereClause where
  pretty  NoWhere = empty
  pretty (AnyWhere [Module _ x [] ds]) | isNoName (unqualify x)
                       = vcat [ text "where", nest 2 (vcat $ map pretty ds) ]
  pretty (AnyWhere ds) = vcat [ text "where", nest 2 (vcat $ map pretty ds) ]
  pretty (SomeWhere m ds) =
    vcat [ hsep [ text "module", pretty m, text "where" ]
         , nest 2 (vcat $ map pretty ds)
         ]

instance Show LHS where show = show . pretty
instance Pretty LHS where
  pretty lhs = case lhs of
    LHS p ps eqs es  -> pr (pretty p) ps eqs es
    Ellipsis _ ps eqs es -> pr (text "...") ps eqs es
    where
      pr d ps eqs es =
        sep [ d
            , nest 2 $ fsep $ map ((text "|" <+>) . pretty) ps
            , nest 2 $ pThing "rewrite" eqs
            , nest 2 $ pThing "with" es
            ]
      pThing thing []       = empty
      pThing thing (e : es) = fsep $ (text thing <+> pretty e)
                                   : map ((text "|" <+>) . pretty) es

instance Show LHSCore where show = show . pretty
instance Pretty LHSCore where
  pretty (LHSHead f ps) = sep $ pretty f : map (parens . pretty) ps
  pretty (LHSProj d ps lhscore ps') = sep $
    pretty d : map (parens . pretty) ps ++
    parens (pretty lhscore) : map (parens . pretty) ps'

instance Pretty [Declaration] where
  pretty = vcat . map pretty

instance Show ModuleApplication where show = show . pretty
instance Pretty ModuleApplication where
  pretty (SectionApp _ bs e) = fsep (map pretty bs) <+> text "=" <+> pretty e
  pretty (RecordModuleIFS _ rec) = text "=" <+> pretty rec <+> text "{{...}}"

instance Pretty Declaration where
    pretty d =
        case d of
            TypeSig i x e ->
                sep [ prettyRelevance i $ pretty x <+> text ":"
                    , nest 2 $ pretty e
                    ]
            Field inst x (Arg i e) ->
                sep [ text "field"
                    , nest 2 $ mkInst inst $
                      prettyRelevance i $ prettyHiding i id $
                        pretty $ TypeSig (i {argInfoRelevance = Relevant}) x e
                    ]
                where
                  mkInst InstanceDef    d = sep [ text "instance", nest 2 d ]
                  mkInst NotInstanceDef d = d
            FunClause lhs rhs wh _ ->
                sep [ pretty lhs
                    , nest 2 $ pretty rhs
                    ] $$ nest 2 (pretty wh)
            DataSig _ ind x tel e ->
                sep [ hsep  [ pretty ind
                            , pretty x
                            , fcat (map pretty tel)
                            ]
                    , nest 2 $ hsep
                            [ text ":"
                            , pretty e
                            ]
                    ]
            Data _ ind x tel (Just e) cs ->
                sep [ hsep  [ pretty ind
                            , pretty x
                            , fcat (map pretty tel)
                            ]
                    , nest 2 $ hsep
                            [ text ":"
                            , pretty e
                            , text "where"
                            ]
                    ] $$ nest 2 (vcat $ map pretty cs)
            Data _ ind x tel Nothing cs ->
                sep [ hsep  [ pretty ind
                            , pretty x
                            , fcat (map pretty tel)
                            ]
                    , nest 2 $ text "where"
                    ] $$ nest 2 (vcat $ map pretty cs)
            RecordSig _ x tel e ->
                sep [ hsep  [ text "record"
                            , pretty x
                            , fcat (map pretty tel)
                            ]
                    , nest 2 $ hsep
                            [ text ":"
                            , pretty e
                            ]
                    ]
            Record _ x ind eta con tel me cs ->
                sep [ hsep  [ text "record"
                            , pretty x
                            , fcat (map pretty tel)
                            ]
                    , nest 2 $ pType me
                    ] $$ nest 2 (vcat $ pInd ++
                                        pEta ++
                                        pCon ++
                                        map pretty cs)
              where pType (Just e) = hsep
                            [ text ":"
                            , pretty e
                            , text "where"
                            ]
                    pType Nothing  =
                              text "where"
                    pInd = maybeToList $ text . show . rangedThing <$> ind
                    pEta = maybeToList $ (\x -> if x then text "eta-equality" else text "no-eta-equality") <$> eta
                    pCon = maybeToList $ (text "constructor" <+>) . pretty <$> fst <$> con
            Infix f xs  ->
                pretty f <+> (fsep $ punctuate comma $ map pretty xs)
            Syntax n xs -> text "syntax" <+> pretty n <+> text "..."
            PatternSyn _ n as p -> text "pattern" <+> pretty n <+> fsep (map pretty as)
                                     <+> text "=" <+> pretty p
            Mutual _ ds     -> namedBlock "mutual" ds
            Abstract _ ds   -> namedBlock "abstract" ds
            Private _ ds    -> namedBlock "private" ds
            InstanceB _ ds  -> namedBlock "instance" ds
            Macro _ ds      -> namedBlock "macro" ds
            Postulate _ ds  -> namedBlock "postulate" ds
            Primitive _ ds  -> namedBlock "primitive" ds
            Module _ x tel ds ->
                hsep [ text "module"
                     , pretty x
                     , fcat (map pretty tel)
                     , text "where"
                     ] $$ nest 2 (vcat $ map pretty ds)
            ModuleMacro _ x (SectionApp _ [] e) DoOpen i | isNoName x ->
                sep [ pretty DoOpen
                    , nest 2 $ pretty e
                    , nest 4 $ pretty i
                    ]
            ModuleMacro _ x (SectionApp _ tel e) open i ->
                sep [ pretty open <+> text "module" <+> pretty x <+> fcat (map pretty tel)
                    , nest 2 $ text "=" <+> pretty e <+> pretty i
                    ]
            ModuleMacro _ x (RecordModuleIFS _ rec) open i ->
                sep [ pretty open <+> text "module" <+> pretty x
                    , nest 2 $ text "=" <+> pretty rec <+> text "{{...}}"
                    ]
            Open _ x i  -> hsep [ text "open", pretty x, pretty i ]
            Import _ x rn open i   ->
                hsep [ pretty open, text "import", pretty x, as rn, pretty i ]
                where
                    as Nothing  = empty
                    as (Just x) = text "as" <+> pretty (asName x)
            UnquoteDecl _ xs t ->
              sep [ text "unquoteDecl" <+> fsep (map pretty xs) <+> text "=", nest 2 $ pretty t ]
            UnquoteDef _ xs t ->
              sep [ text "unquoteDef" <+> fsep (map pretty xs) <+> text "=", nest 2 $ pretty t ]
            Pragma pr   -> sep [ text "{-#" <+> pretty pr, text "#-}" ]
        where
            namedBlock s ds =
                sep [ text s
                    , nest 2 $ vcat $ map pretty ds
                    ]

instance Pretty OpenShortHand where
    pretty DoOpen = text "open"
    pretty DontOpen = empty

instance Pretty Pragma where
    pretty (OptionsPragma _ opts) = fsep $ map text $ "OPTIONS" : opts
    pretty (BuiltinPragma _ b x)  = hsep [ text "BUILTIN", text b, pretty x ]
    pretty (RewritePragma _ x)    =
      hsep [ text "REWRITE", pretty x ]
    pretty (CompiledPragma _ x hs) =
      hsep [ text "COMPILED", pretty x, text hs ]
    pretty (CompiledExportPragma _ x hs) =
      hsep [ text "COMPILED_EXPORT", pretty x, text hs ]
    pretty (CompiledTypePragma _ x hs) =
      hsep [ text "COMPILED_TYPE", pretty x, text hs ]
    pretty (CompiledDeclareDataPragma _ x hs) =
      hsep [ text "COMPILED_DECLARE_DATA", pretty x, text hs ]
    pretty (CompiledDataPragma _ x hs hcs) =
      hsep $ [text "COMPILED_DATA", pretty x] ++ map text (hs : hcs)
    pretty (CompiledEpicPragma _ x e) =
      hsep [ text "COMPILED_EPIC", pretty x, text e ]
    pretty (CompiledJSPragma _ x e) =
      hsep [ text "COMPILED_JS", pretty x, text e ]
    pretty (CompiledUHCPragma _ x e) =
      hsep [ text "COMPILED_UHC", pretty x, text e ]
    pretty (CompiledDataUHCPragma _ x crd crcs) =
      hsep $ [ text "COMPILED_DATA_UHC", pretty x] ++ map text (crd : crcs)
    pretty (HaskellCodePragma _ s) =
      vcat (text "HASKELL" : map text (lines s))
    pretty (NoSmashingPragma _ i) =
      hsep $ [text "NO_SMASHING", pretty i]
    pretty (StaticPragma _ i) =
      hsep $ [text "STATIC", pretty i]
    pretty (InlinePragma _ i) =
      hsep $ [text "INLINE", pretty i]
    pretty (ImportPragma _ i) =
      hsep $ [text "IMPORT", text i]
    pretty (ImportUHCPragma _ i) =
      hsep $ [text "IMPORT_UHC", text i]
    pretty (ImpossiblePragma _) =
      hsep $ [text "IMPOSSIBLE"]
    pretty (TerminationCheckPragma _ tc) =
      case tc of
        TerminationCheck       -> __IMPOSSIBLE__
        NoTerminationCheck     -> text "NO_TERMINATION_CHECK"
        NonTerminating         -> text "NON_TERMINATING"
        Terminating            -> text "TERMINATING"
        TerminationMeasure _ x -> hsep $ [text "MEASURE", pretty x]
    pretty (CatchallPragma _) = text "CATCHALL"
    pretty (DisplayPragma _ lhs rhs) = text "DISPLAY" <+> sep [ pretty lhs <+> text "=", nest 2 $ pretty rhs ]
    pretty (NoPositivityCheckPragma _) = text "NO_POSITIVITY_CHECK"

instance Pretty Fixity where
    pretty (Fixity _ Unrelated   _)   = __IMPOSSIBLE__
    pretty (Fixity _ (Related 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
    pretty BindHole{}   = underscore
    pretty NormalHole{} = underscore
    pretty WildHole{}   = underscore

instance Pretty Notation where
    pretty = hcat . map pretty

instance Pretty Fixity' where
    pretty (Fixity' fix nota)
      | nota == noNotation = pretty fix
      | otherwise          = text "syntax" <+> pretty nota

instance Pretty e => Pretty (Arg e) where
 -- Andreas 2010-09-21: do not print relevance in general, only in function types!
 -- Andreas 2010-09-24: and in record fields
    pretty a = -- pRelevance r $
               -- TODO guilhem: print colors
               prettyHiding (argInfo a) id $ pretty $ unArg a

instance Pretty e => Pretty (Named_ e) where
    pretty (Named Nothing e) = pretty e
    pretty (Named (Just s) e) = sep [ text (rawNameToString $ rangedThing s) <+> text "=", pretty e ]

instance Pretty [Pattern] where
    pretty = fsep . map pretty

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 (fmap (fmap (fmap (NoPlaceholder Strict.Nothing))) 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"
            RecP _ fs       -> sep [ text "record", bracesAndSemicolons (map pretty fs) ]

prettyOpApp ::
  Pretty a => QName -> [NamedArg (MaybePlaceholder a)] -> [Doc]
prettyOpApp q es = merge [] $ prOp ms xs es
  where
    ms = init (qnameParts q)
    xs = case unqualify q of
           Name _ xs -> xs
           NoName{}  -> __IMPOSSIBLE__

    prOp ms (Hole : xs) (e : es) = (pretty e, case namedArg e of
                                                Placeholder p -> Just p
                                                _             -> Nothing) :
                                   prOp ms xs es
    prOp _  (Hole : _)  []       = __IMPOSSIBLE__
    prOp ms (Id x : xs) es       = ( pretty (foldr Qual (QName (Name noRange $ [Id x])) ms)
                                   , Nothing
                                   ) : prOp [] xs es
    prOp _  []       []          = []
    prOp _  []       es          = map (\e -> (pretty e, Nothing)) es

    -- Section underscores should be printed without surrounding
    -- whitespace. This function takes care of that.
    merge :: [Doc] -> [(Doc, Maybe PositionInName)] -> [Doc]
    merge before []                            = reverse before
    merge before ((d, Nothing) : after)        = merge (d : before) after
    merge before ((d, Just Beginning) : after) = mergeRight before d after
    merge before ((d, Just End)       : after) = case mergeLeft d before of
                                                   (d, bs) -> merge (d : bs) after
    merge before ((d, Just Middle)    : after) = case mergeLeft d before of
                                                   (d, bs) -> mergeRight bs d after

    mergeRight before d after =
      reverse before ++
      case merge [] after of
        []     -> [d]
        a : as -> (d <> a) : as

    mergeLeft d before = case before of
      []     -> (d,      [])
      b : bs -> (b <> d, bs)

instance (Pretty a, Pretty b) => Pretty (ImportDirective' a b) where
    pretty i =
        sep [ public (publicOpen i)
            , pretty $ using i
            , prettyHiding $ hiding i
            , rename $ impRenaming i
            ]
        where
            public True  = text "public"
            public False = empty

            prettyHiding [] = empty
            prettyHiding xs = text "hiding" <+> parens (fsep $ punctuate (text ";") $ map pretty xs)

            rename [] = empty
            rename xs = hsep [ text "renaming"
                             , parens $ fsep $ punctuate (text ";") $ map pr xs
                             ]

            pr r = hsep [ pretty (renFrom r), text "to", pretty (renTo r) ]

instance (Pretty a, Pretty b) => Pretty (Using' a b) where
    pretty UseEverything = empty
    pretty (Using xs)    =
        text "using" <+> parens (fsep $ punctuate (text ";") $ map pretty xs)

instance (Pretty a, Pretty b) => Pretty (ImportedName' a b) where
    pretty (ImportedName x)     = pretty x
    pretty (ImportedModule x)   = text "module" <+> pretty x