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

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

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

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

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