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
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)
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 = [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
[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)