{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE OverloadedStrings #-}
module Agda.Interaction.Command.ShowConstraints where

import Agda.Interaction.BasicOps (getConstraints)
import Agda.TypeChecking.Monad.Base (TCM)
import Agda.Utils.Pretty (prettyShow)
import Data.ByteString (ByteString)

import qualified Data.ByteString.Char8 as BS8
import qualified Data.List as List

showConstraints :: [ByteString] -> TCM ByteString
showConstraints :: [ByteString] -> TCM ByteString
showConstraints = \case
  [] -> TCM ByteString
constraints
  [ByteString
""] -> TCM ByteString
constraints
  [ByteString]
_  -> ByteString -> TCM ByteString
forall (f :: * -> *) a. Applicative f => a -> f a
pure ByteString
"/agda constraints [cid]"
  where
    constraintToBS :: [OutputForm Expr Expr] -> ByteString
constraintToBS = String -> ByteString
BS8.pack (String -> ByteString)
-> ([OutputForm Expr Expr] -> String)
-> [OutputForm Expr Expr]
-> ByteString
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [String] -> String
unlines ([String] -> String)
-> ([OutputForm Expr Expr] -> [String])
-> [OutputForm Expr Expr]
-> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (OutputForm Expr Expr -> String)
-> [OutputForm Expr Expr] -> [String]
forall a b. (a -> b) -> [a] -> [b]
List.map OutputForm Expr Expr -> String
forall a. Pretty a => a -> String
prettyShow
    constraints :: TCM ByteString
constraints = TCM [OutputForm Expr Expr]
getConstraints TCM [OutputForm Expr Expr]
-> ([OutputForm Expr Expr] -> TCM ByteString) -> TCM ByteString
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= ByteString -> TCM ByteString
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ByteString -> TCM ByteString)
-> ([OutputForm Expr Expr] -> ByteString)
-> [OutputForm Expr Expr]
-> TCM ByteString
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [OutputForm Expr Expr] -> ByteString
constraintToBS