module Agda.TypeChecking.SizedTypes.Pretty where

import Control.Monad
import Data.Maybe

import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.TypeChecking.Monad.Base.Types
import Agda.TypeChecking.Monad.Builtin (HasBuiltins, builtinSizeInf, getBuiltin')
import Agda.TypeChecking.Monad.Context (unsafeModifyContext)
import Agda.TypeChecking.Monad.SizedTypes
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.SizedTypes.Syntax

import Agda.Utils.Function
import Agda.Utils.Impossible

-- | Turn a size expression into a term.
unSizeExpr :: HasBuiltins m => DBSizeExpr -> m Term
unSizeExpr :: forall (m :: * -> *). HasBuiltins m => DBSizeExpr -> m Term
unSizeExpr DBSizeExpr
a =
  case DBSizeExpr
a of
    DBSizeExpr
Infty         -> Term -> Maybe Term -> Term
forall a. a -> Maybe a -> a
fromMaybe Term
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Term -> Term) -> m (Maybe Term) -> m Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BuiltinId -> m (Maybe Term)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
getBuiltin' BuiltinId
builtinSizeInf
    Rigid NamedRigid
r (O Int
n) -> do
      Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
0) m ()
forall a. HasCallStack => a
__IMPOSSIBLE__
      Int -> Term -> m Term
forall (m :: * -> *). HasBuiltins m => Int -> Term -> m Term
sizeSuc Int
n (Term -> m Term) -> Term -> m Term
forall a b. (a -> b) -> a -> b
$ Int -> Term
var (Int -> Term) -> Int -> Term
forall a b. (a -> b) -> a -> b
$ NamedRigid -> Int
rigidIndex NamedRigid
r
    Flex (SizeMeta MetaId
x [Int]
es) (O Int
n) -> do
      Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
0) m ()
forall a. HasCallStack => a
__IMPOSSIBLE__
      Int -> Term -> m Term
forall (m :: * -> *). HasBuiltins m => Int -> Term -> m Term
sizeSuc Int
n (Term -> m Term) -> Term -> m Term
forall a b. (a -> b) -> a -> b
$ MetaId -> Elims -> Term
MetaV MetaId
x (Elims -> Term) -> Elims -> Term
forall a b. (a -> b) -> a -> b
$ (Int -> Elim) -> [Int] -> Elims
forall a b. (a -> b) -> [a] -> [b]
map (Arg Term -> Elim
forall a. Arg a -> Elim' a
Apply (Arg Term -> Elim) -> (Int -> Arg Term) -> Int -> Elim
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Arg Term
forall a. a -> Arg a
defaultArg (Term -> Arg Term) -> (Int -> Term) -> Int -> Arg Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Term
var) [Int]
es
    Const{} -> m Term
forall a. HasCallStack => a
__IMPOSSIBLE__

instance PrettyTCM SizeMeta where
  prettyTCM :: forall (m :: * -> *). MonadPretty m => SizeMeta -> m Doc
prettyTCM (SizeMeta MetaId
x [Int]
es) = Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM (MetaId -> Elims -> Term
MetaV MetaId
x (Elims -> Term) -> Elims -> Term
forall a b. (a -> b) -> a -> b
$ (Int -> Elim) -> [Int] -> Elims
forall a b. (a -> b) -> [a] -> [b]
map (Arg Term -> Elim
forall a. Arg a -> Elim' a
Apply (Arg Term -> Elim) -> (Int -> Arg Term) -> Int -> Elim
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Arg Term
forall a. a -> Arg a
defaultArg (Term -> Arg Term) -> (Int -> Term) -> Int -> Arg Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Term
var) [Int]
es)

-- | Assumes we are in the right context.
instance PrettyTCM (SizeConstraint) where
  prettyTCM :: forall (m :: * -> *). MonadPretty m => SizeConstraint -> m Doc
prettyTCM (Constraint DBSizeExpr
a Cmp
cmp DBSizeExpr
b) = do
    Term
u <- DBSizeExpr -> m Term
forall (m :: * -> *). HasBuiltins m => DBSizeExpr -> m Term
unSizeExpr DBSizeExpr
a
    Term
v <- DBSizeExpr -> m Term
forall (m :: * -> *). HasBuiltins m => DBSizeExpr -> m Term
unSizeExpr DBSizeExpr
b
    Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
u m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Cmp -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Cmp
cmp m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
v

instance PrettyTCM HypSizeConstraint where
  prettyTCM :: forall (m :: * -> *). MonadPretty m => HypSizeConstraint -> m Doc
prettyTCM (HypSizeConstraint Context
cxt [Int]
_ [SizeConstraint]
hs SizeConstraint
c) =
    (Context -> Context) -> m Doc -> m Doc
forall (tcm :: * -> *) a.
MonadTCEnv tcm =>
(Context -> Context) -> tcm a -> tcm a
unsafeModifyContext (Context -> Context -> Context
forall a b. a -> b -> a
const Context
cxt) (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ do
      let cxtNames :: [Name]
cxtNames = [Name] -> [Name]
forall a. [a] -> [a]
reverse ([Name] -> [Name]) -> [Name] -> [Name]
forall a b. (a -> b) -> a -> b
$ (Dom' Term (Name, Type) -> Name) -> Context -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map ((Name, Type) -> Name
forall a b. (a, b) -> a
fst ((Name, Type) -> Name)
-> (Dom' Term (Name, Type) -> (Name, Type))
-> Dom' Term (Name, Type)
-> Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Dom' Term (Name, Type) -> (Name, Type)
forall t e. Dom' t e -> e
unDom) Context
cxt
      -- text ("[#cxt=" ++ show (size cxt) ++ "]") <+> do
      [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList ((Name -> m Doc) -> [Name] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map Name -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Name -> m Doc
prettyTCM [Name]
cxtNames) m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> do
        Bool -> (m Doc -> m Doc) -> m Doc -> m Doc
forall b a. IsBool b => b -> (a -> a) -> a -> a
applyUnless ([SizeConstraint] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [SizeConstraint]
hs)
          (([m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
hcat (m Doc -> [m Doc] -> [m Doc]
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
m Doc -> t (m Doc) -> [m Doc]
punctuate m Doc
", " ([m Doc] -> [m Doc]) -> [m Doc] -> [m Doc]
forall a b. (a -> b) -> a -> b
$ (SizeConstraint -> m Doc) -> [SizeConstraint] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map SizeConstraint -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => SizeConstraint -> m Doc
prettyTCM [SizeConstraint]
hs) m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> m Doc
"|-") m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>)
          (SizeConstraint -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => SizeConstraint -> m Doc
prettyTCM SizeConstraint
c)