module Render.Interaction where

import qualified Data.Set                      as Set

import           Agda.Interaction.Base
import           Agda.Syntax.Internal           ( Blocker(..) )
import           Agda.TypeChecking.Monad
import           Render.Class
import           Render.Concrete                ( )
import           Render.Internal                ( )
import           Render.Name                    ( )
import           Render.Position                ( )
import           Render.RichText
import           Render.TypeChecking            ( )

--------------------------------------------------------------------------------

-- | OutputForm

instance (Render a, Render b) => Render (OutputForm a b) where
  render :: OutputForm a b -> Inlines
render (OutputForm Range
r [ProblemId]
pids Blocker
unblock OutputConstraint a b
c) = [Inlines] -> Inlines
fsep
    [forall a. Render a => a -> Inlines
render OutputConstraint a b
c, forall a. Render a => a -> Inlines
prange Range
r, Inlines -> Inlines
parens ([Inlines] -> Inlines
sep [Blocker -> Inlines
blockedOn Blocker
unblock, forall {a}. Render a => [a] -> Inlines
prPids [ProblemId]
pids])]
   where
    prPids :: [a] -> Inlines
prPids []    = forall a. Monoid a => a
mempty
    prPids [a
pid] = Inlines -> Inlines
parens forall a b. (a -> b) -> a -> b
$ Inlines
"belongs to problem" Inlines -> Inlines -> Inlines
<+> forall a. Render a => a -> Inlines
render a
pid
    prPids [a]
pids' = Inlines -> Inlines
parens forall a b. (a -> b) -> a -> b
$ Inlines
"belongs to problems" Inlines -> Inlines -> Inlines
<+> [Inlines] -> Inlines
fsep
      (Inlines -> [Inlines] -> [Inlines]
punctuate Inlines
"," forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. Render a => a -> Inlines
render [a]
pids')

    comma :: Inlines
comma | forall (t :: * -> *) a. Foldable t => t a -> Bool
null [ProblemId]
pids = forall a. Monoid a => a
mempty
          | Bool
otherwise = Inlines
","

    blockedOn :: Blocker -> Inlines
blockedOn (UnblockOnAll Set Blocker
bs) | forall a. Set a -> Bool
Set.null Set Blocker
bs = forall a. Monoid a => a
mempty
    blockedOn (UnblockOnAny Set Blocker
bs) | forall a. Set a -> Bool
Set.null Set Blocker
bs = Inlines
"stuck" forall a. Semigroup a => a -> a -> a
<> Inlines
comma
    blockedOn Blocker
u = Inlines
"blocked on" Inlines -> Inlines -> Inlines
<+> (forall a. Render a => a -> Inlines
render Blocker
u forall a. Semigroup a => a -> a -> a
<> Inlines
comma)

    prange :: p -> Inlines
prange p
rr | forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Char]
s    = forall a. Monoid a => a
mempty
              | Bool
otherwise = [Char] -> Inlines
text forall a b. (a -> b) -> a -> b
$ [Char]
" [ at " forall a. [a] -> [a] -> [a]
++ [Char]
s forall a. [a] -> [a] -> [a]
++ [Char]
" ]"
      where s :: [Char]
s = forall a. Show a => a -> [Char]
show forall a b. (a -> b) -> a -> b
$ forall a. Render a => a -> Inlines
render p
rr

-- | OutputConstraint
instance (Render a, Render b) => Render (OutputConstraint a b) where
  render :: OutputConstraint a b -> Inlines
render (OfType b
name a
expr) = forall a. Render a => a -> Inlines
render b
name forall a. Semigroup a => a -> a -> a
<> Inlines
" : " forall a. Semigroup a => a -> a -> a
<> forall a. Render a => a -> Inlines
render a
expr
  render (JustType b
name   ) = Inlines
"Type " forall a. Semigroup a => a -> a -> a
<> forall a. Render a => a -> Inlines
render b
name
  render (JustSort b
name   ) = Inlines
"Sort " forall a. Semigroup a => a -> a -> a
<> forall a. Render a => a -> Inlines
render b
name
  render (CmpInType Comparison
cmp a
expr b
name1 b
name2) =
    forall a. Render a => a -> Inlines
render b
name1
      forall a. Semigroup a => a -> a -> a
<> Inlines
" "
      forall a. Semigroup a => a -> a -> a
<> forall a. Render a => a -> Inlines
render Comparison
cmp
      forall a. Semigroup a => a -> a -> a
<> Inlines
" "
      forall a. Semigroup a => a -> a -> a
<> forall a. Render a => a -> Inlines
render b
name2
      forall a. Semigroup a => a -> a -> a
<> Inlines
" : "
      forall a. Semigroup a => a -> a -> a
<> forall a. Render a => a -> Inlines
render a
expr
  render (CmpElim [Polarity]
pols a
expr [b]
names1 [b]
names2) =
    forall a. Render a => a -> Inlines
render [b]
names1
      forall a. Semigroup a => a -> a -> a
<> Inlines
" "
      forall a. Semigroup a => a -> a -> a
<> forall a. Render a => a -> Inlines
render [Polarity]
pols
      forall a. Semigroup a => a -> a -> a
<> Inlines
" "
      forall a. Semigroup a => a -> a -> a
<> forall a. Render a => a -> Inlines
render [b]
names2
      forall a. Semigroup a => a -> a -> a
<> Inlines
" : "
      forall a. Semigroup a => a -> a -> a
<> forall a. Render a => a -> Inlines
render a
expr
  render (CmpTypes Comparison
cmp b
name1 b
name2) =
    forall a. Render a => a -> Inlines
render b
name1 forall a. Semigroup a => a -> a -> a
<> Inlines
" " forall a. Semigroup a => a -> a -> a
<> forall a. Render a => a -> Inlines
render Comparison
cmp forall a. Semigroup a => a -> a -> a
<> Inlines
" " forall a. Semigroup a => a -> a -> a
<> forall a. Render a => a -> Inlines
render b
name2
  render (CmpLevels Comparison
cmp b
name1 b
name2) =
    forall a. Render a => a -> Inlines
render b
name1 forall a. Semigroup a => a -> a -> a
<> Inlines
" " forall a. Semigroup a => a -> a -> a
<> forall a. Render a => a -> Inlines
render Comparison
cmp forall a. Semigroup a => a -> a -> a
<> Inlines
" " forall a. Semigroup a => a -> a -> a
<> forall a. Render a => a -> Inlines
render b
name2
  render (CmpTeles Comparison
cmp b
name1 b
name2) =
    forall a. Render a => a -> Inlines
render b
name1 forall a. Semigroup a => a -> a -> a
<> Inlines
" " forall a. Semigroup a => a -> a -> a
<> forall a. Render a => a -> Inlines
render Comparison
cmp forall a. Semigroup a => a -> a -> a
<> Inlines
" " forall a. Semigroup a => a -> a -> a
<> forall a. Render a => a -> Inlines
render b
name2
  render (CmpSorts Comparison
cmp b
name1 b
name2) =
    forall a. Render a => a -> Inlines
render b
name1 forall a. Semigroup a => a -> a -> a
<> Inlines
" " forall a. Semigroup a => a -> a -> a
<> forall a. Render a => a -> Inlines
render Comparison
cmp forall a. Semigroup a => a -> a -> a
<> Inlines
" " forall a. Semigroup a => a -> a -> a
<> forall a. Render a => a -> Inlines
render b
name2
  render (Assign b
name a
expr) = forall a. Render a => a -> Inlines
render b
name forall a. Semigroup a => a -> a -> a
<> Inlines
" := " forall a. Semigroup a => a -> a -> a
<> forall a. Render a => a -> Inlines
render a
expr
  render (TypedAssign b
name a
expr1 a
expr2) =
    forall a. Render a => a -> Inlines
render b
name forall a. Semigroup a => a -> a -> a
<> Inlines
" := " forall a. Semigroup a => a -> a -> a
<> forall a. Render a => a -> Inlines
render a
expr1 forall a. Semigroup a => a -> a -> a
<> Inlines
" :? " forall a. Semigroup a => a -> a -> a
<> forall a. Render a => a -> Inlines
render a
expr2
  render (PostponedCheckArgs b
name [a]
exprs a
expr1 a
expr2) =
    let exprs' :: [Inlines]
exprs' = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Inlines -> Inlines
parens forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Render a => a -> Inlines
render) [a]
exprs
    in  forall a. Render a => a -> Inlines
render b
name
          forall a. Semigroup a => a -> a -> a
<> Inlines
" := "
          forall a. Semigroup a => a -> a -> a
<> Inlines -> Inlines
parens (Inlines
"_ : " forall a. Semigroup a => a -> a -> a
<> forall a. Render a => a -> Inlines
render a
expr1)
          forall a. Semigroup a => a -> a -> a
<> Inlines
" "
          forall a. Semigroup a => a -> a -> a
<> [Inlines] -> Inlines
fsep [Inlines]
exprs'
          forall a. Semigroup a => a -> a -> a
<> Inlines
" : "
          forall a. Semigroup a => a -> a -> a
<> forall a. Render a => a -> Inlines
render a
expr2
  render (IsEmptyType a
expr) = Inlines
"Is empty: " forall a. Semigroup a => a -> a -> a
<> forall a. Render a => a -> Inlines
render a
expr
  render (SizeLtSat   a
expr) = Inlines
"Not empty type of sizes: " forall a. Semigroup a => a -> a -> a
<> forall a. Render a => a -> Inlines
render a
expr
  render (FindInstanceOF b
name a
expr [(a, a, a)]
exprs) =
    let exprs' :: [Inlines]
exprs' =
          (\(a
q, a
e, a
t) -> forall a. Render a => a -> Inlines
render a
q forall a. Semigroup a => a -> a -> a
<> Inlines
"=" forall a. Semigroup a => a -> a -> a
<> forall a. Render a => a -> Inlines
render a
e forall a. Semigroup a => a -> a -> a
<> Inlines
" : " forall a. Semigroup a => a -> a -> a
<> forall a. Render a => a -> Inlines
render a
t)
            forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(a, a, a)]
exprs
    in  [Inlines] -> Inlines
fsep
          [ Inlines
"Resolve instance argument "
          , forall a. Render a => a -> Inlines
render b
name forall a. Semigroup a => a -> a -> a
<> Inlines
" : " forall a. Semigroup a => a -> a -> a
<> forall a. Render a => a -> Inlines
render a
expr
          , Inlines
"Candidate:"
          , [Inlines] -> Inlines
vcat [Inlines]
exprs'
          ]
  render (PTSInstance b
name1 b
name2) =
    Inlines
"PTS instance for (" forall a. Semigroup a => a -> a -> a
<> forall a. Render a => a -> Inlines
render b
name1 forall a. Semigroup a => a -> a -> a
<> Inlines
", " forall a. Semigroup a => a -> a -> a
<> forall a. Render a => a -> Inlines
render b
name2 forall a. Semigroup a => a -> a -> a
<> Inlines
")"
  render (PostponedCheckFunDef QName
name a
expr TCErr
_err) =
    Inlines
"Check definition of " forall a. Semigroup a => a -> a -> a
<> forall a. Render a => a -> Inlines
render QName
name forall a. Semigroup a => a -> a -> a
<> Inlines
" : " forall a. Semigroup a => a -> a -> a
<> forall a. Render a => a -> Inlines
render a
expr
  render (CheckLock b
t b
lk) =
    Inlines
"Check lock" Inlines -> Inlines -> Inlines
<+> forall a. Render a => a -> Inlines
render b
lk Inlines -> Inlines -> Inlines
<+> Inlines
"allows" Inlines -> Inlines -> Inlines
<+> forall a. Render a => a -> Inlines
render b
t
  render (UsableAtMod Modality
modality b
t) =
    Inlines
"Is usable at" Inlines -> Inlines -> Inlines
<+> forall a. Render a => a -> Inlines
render Modality
modality Inlines -> Inlines -> Inlines
<+> forall a. Render a => a -> Inlines
render b
t

-- | IPBoundary'
instance Render c => Render (IPBoundary' c) where
  render :: IPBoundary' c -> Inlines
render (IPBoundary [(c, c)]
eqs c
val c
meta Overapplied
over) = do
    let xs :: [Inlines]
xs  = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\(c
l, c
r) -> forall a. Render a => a -> Inlines
render c
l Inlines -> Inlines -> Inlines
<+> Inlines
"=" Inlines -> Inlines -> Inlines
<+> forall a. Render a => a -> Inlines
render c
r) [(c, c)]
eqs
        rhs :: Inlines
rhs = case Overapplied
over of
          Overapplied
Overapplied    -> Inlines
"=" Inlines -> Inlines -> Inlines
<+> forall a. Render a => a -> Inlines
render c
meta
          Overapplied
NotOverapplied -> forall a. Monoid a => a
mempty
    [Inlines] -> Inlines
fsep (Inlines -> [Inlines] -> [Inlines]
punctuate Inlines
"," [Inlines]
xs) Inlines -> Inlines -> Inlines
<+> Inlines
"⊢" Inlines -> Inlines -> Inlines
<+> forall a. Render a => a -> Inlines
render c
val Inlines -> Inlines -> Inlines
<+> Inlines
rhs