    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, contextNames)
    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
        u <- DBSizeExpr -> m Term
    forall (m :: * -> *). HasBuiltins m => DBSizeExpr -> m Term
    unSizeExpr DBSizeExpr
    a
        v <- unSizeExpr b
        prettyTCM u <+> pretty cmp <+> prettyTCM 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 = Context -> [Name]
    contextNames Context
    cxt
          -- text ("[#cxt=" ++ show (size cxt) ++ "]") <+> do
          [m Doc] -> m Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, 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)