module Agda.Syntax.Internal
( module Agda.Syntax.Internal
, module Agda.Syntax.Abstract.Name
, module Agda.Utils.Pointer
) where
import Prelude hiding (foldr, mapM, null)
import Control.Arrow ((***))
import Control.Applicative hiding (empty)
import Control.Monad.Identity hiding (mapM)
import Control.Monad.State hiding (mapM)
import Control.Parallel
import Data.Foldable ( Foldable, foldMap )
import Data.Function
import qualified Data.List as List
import Data.Maybe
import Data.Monoid
#if !(MIN_VERSION_base(4,7,0))
import Data.Orphans ()
#endif
import Data.Traversable
import Data.Typeable (Typeable)
import Agda.Syntax.Position
import Agda.Syntax.Common hiding (Arg, Dom, NamedArg, ArgInfo)
import qualified Agda.Syntax.Common as Common
import Agda.Syntax.Literal
import Agda.Syntax.Abstract.Name
import Agda.Utils.Empty
import Agda.Utils.Functor
import Agda.Utils.Geniplate
import Agda.Utils.Lens
import Agda.Utils.List
import Agda.Utils.Null
import Agda.Utils.Permutation
import Agda.Utils.Pointer
import Agda.Utils.Size
import Agda.Utils.Pretty
#include "undefined.h"
import Agda.Utils.Impossible
type Color = Term
type ArgInfo = Common.ArgInfo Color
type Arg a = Common.Arg Color a
type Dom a = Common.Dom Color a
type NamedArg a = Common.NamedArg Color a
type Args = [Arg Term]
type NamedArgs = [NamedArg Term]
data ConHead = ConHead
{ conName :: QName
, conInductive :: Induction
, conFields :: [QName]
} deriving (Typeable)
instance Eq ConHead where
(==) = (==) `on` conName
instance Ord ConHead where
(<=) = (<=) `on` conName
instance Show ConHead where
show (ConHead c i fs) = show c ++ "(" ++ show i ++ ")" ++ show fs
instance HasRange ConHead where
getRange = getRange . conName
instance SetRange ConHead where
setRange r = mapConName (setRange r)
class LensConName a where
getConName :: a -> QName
setConName :: QName -> a -> a
setConName = mapConName . const
mapConName :: (QName -> QName) -> a -> a
mapConName f a = setConName (f (getConName a)) a
instance LensConName ConHead where
getConName = conName
setConName c con = con { conName = c }
data Term = Var !Int Elims
| Lam ArgInfo (Abs Term)
| ExtLam [Clause] Args
| Lit Literal
| Def QName Elims
| Con ConHead Args
| Pi (Dom Type) (Abs Type)
| Sort Sort
| Level Level
| MetaV !MetaId Elims
| DontCare Term
| Shared !(Ptr Term)
deriving (Typeable, Show)
data Elim' a = Apply (Arg a) | Proj QName
deriving (Typeable, Show, Functor, Foldable, Traversable)
type Elim = Elim' Term
type Elims = [Elim]
type ArgName = String
argNameToString :: ArgName -> String
argNameToString = id
stringToArgName :: String -> ArgName
stringToArgName = id
appendArgNames :: ArgName -> ArgName -> ArgName
appendArgNames = (++)
nameToArgName :: Name -> ArgName
nameToArgName = stringToArgName . prettyShow
data Abs a = Abs { absName :: ArgName, unAbs :: a }
| NoAbs { absName :: ArgName, unAbs :: a }
deriving (Typeable, Functor, Foldable, Traversable)
instance Decoration Abs where
traverseF f (Abs x a) = Abs x <$> f a
traverseF f (NoAbs x a) = NoAbs x <$> f a
data Type' a = El { _getSort :: Sort, unEl :: a }
deriving (Typeable, Show, Functor, Foldable, Traversable)
type Type = Type' Term
instance Decoration Type' where
traverseF f (El s a) = El s <$> f a
class LensSort a where
lensSort :: Lens' Sort a
getSort :: a -> Sort
getSort a = a ^. lensSort
instance LensSort (Type' a) where
lensSort f (El s a) = f s <&> \ s' -> El s' a
instance LensSort a => LensSort (Common.Dom c a) where
lensSort = traverseF . lensSort
instance LensSort a => LensSort (Abs a) where
lensSort = traverseF . lensSort
data Tele a = EmptyTel
| ExtendTel a (Abs (Tele a))
deriving (Typeable, Show, Functor, Foldable, Traversable)
type Telescope = Tele (Dom Type)
mapAbsNamesM :: Applicative m => (ArgName -> m ArgName) -> Tele a -> m (Tele a)
mapAbsNamesM f EmptyTel = pure EmptyTel
mapAbsNamesM f (ExtendTel a ( Abs x b)) = ExtendTel a <$> ( Abs <$> f x <*> mapAbsNamesM f b)
mapAbsNamesM f (ExtendTel a (NoAbs x b)) = ExtendTel a <$> (NoAbs <$> f x <*> mapAbsNamesM f b)
mapAbsNames :: (ArgName -> ArgName) -> Tele a -> Tele a
mapAbsNames f = runIdentity . mapAbsNamesM (Identity . f)
replaceEmptyName :: ArgName -> Tele a -> Tele a
replaceEmptyName x = mapAbsNames $ \ y -> if null y then x else y
data Sort
= Type Level
| Prop
| Inf
| SizeUniv
| DLub Sort (Abs Sort)
deriving (Typeable, Show)
newtype Level = Max [PlusLevel]
deriving (Show, Typeable)
data PlusLevel
= ClosedLevel Integer
| Plus Integer LevelAtom
deriving (Show, Typeable)
data LevelAtom
= MetaLevel MetaId Elims
| BlockedLevel MetaId Term
| NeutralLevel NotBlocked Term
| UnreducedLevel Term
deriving (Show, Typeable)
newtype MetaId = MetaId { metaId :: Nat }
deriving (Eq, Ord, Num, Real, Enum, Integral, Typeable)
data NotBlocked
= StuckOn Elim
| Underapplied
| AbsurdMatch
| MissingClauses
| ReallyNotBlocked
deriving (Show, Typeable)
instance Monoid NotBlocked where
mempty = ReallyNotBlocked
ReallyNotBlocked `mappend` b = b
b@MissingClauses `mappend` _ = b
_ `mappend` b@MissingClauses = b
b@StuckOn{} `mappend` _ = b
_ `mappend` b@StuckOn{} = b
b `mappend` _ = b
data Blocked t
= Blocked { theBlockingMeta :: MetaId , ignoreBlocking :: t }
| NotBlocked { blockingStatus :: NotBlocked, ignoreBlocking :: t }
deriving (Typeable, Show, Functor, Foldable, Traversable)
instance Applicative Blocked where
pure = notBlocked
f <*> e = ((f $> ()) `mappend` (e $> ())) $> ignoreBlocking f (ignoreBlocking e)
type Blocked_ = Blocked ()
instance Monoid Blocked_ where
mempty = notBlocked ()
NotBlocked ReallyNotBlocked _ `mappend` b = b
b `mappend` NotBlocked ReallyNotBlocked _ = b
b@(NotBlocked StuckOn{} _) `mappend` _ = b
_ `mappend` b@(NotBlocked StuckOn{} _) = b
b@Blocked{} `mappend` Blocked{} = b
Blocked{} `mappend` b = b
b `mappend` Blocked{} = b
b `mappend` _ = b
stuckOn :: Elim -> NotBlocked -> NotBlocked
stuckOn e r =
case r of
MissingClauses -> r
StuckOn{} -> r
Underapplied -> r'
AbsurdMatch -> r'
ReallyNotBlocked -> r'
where r' = StuckOn e
data Clause = Clause
{ clauseRange :: Range
, clauseTel :: Telescope
, clausePerm :: Permutation
, namedClausePats :: [NamedArg Pattern]
, clauseBody :: ClauseBody
, clauseType :: Maybe (Arg Type)
}
deriving (Typeable, Show)
clausePats :: Clause -> [Arg Pattern]
clausePats = map (fmap namedThing) . namedClausePats
data ClauseBodyF a = Body a
| Bind (Abs (ClauseBodyF a))
| NoBody
deriving (Typeable, Show, Functor, Foldable, Traversable)
type ClauseBody = ClauseBodyF Term
instance HasRange Clause where
getRange = clauseRange
type PatVarName = ArgName
patVarNameToString :: PatVarName -> String
patVarNameToString = argNameToString
nameToPatVarName :: Name -> PatVarName
nameToPatVarName = nameToArgName
data Pattern' x
= VarP x
| DotP Term
| ConP ConHead ConPatternInfo [NamedArg (Pattern' x)]
| LitP Literal
| ProjP QName
deriving (Typeable, Show, Functor, Foldable, Traversable)
type Pattern = Pattern' PatVarName
type DeBruijnPattern = Pattern' (Int, PatVarName)
namedVarP :: PatVarName -> Named (Ranged PatVarName) Pattern
namedVarP x = Named named $ VarP x
where named = if isUnderscore x then Nothing else Just $ unranged x
data ConPatternInfo = ConPatternInfo
{ conPRecord :: Maybe Bool
, conPType :: Maybe (Arg Type)
}
deriving (Typeable, Show)
noConPatternInfo :: ConPatternInfo
noConPatternInfo = ConPatternInfo Nothing Nothing
patternVars :: Arg Pattern -> [Arg (Either PatVarName Term)]
patternVars (Common.Arg i (VarP x) ) = [Common.Arg i $ Left x]
patternVars (Common.Arg i (DotP t) ) = [Common.Arg i $ Right t]
patternVars (Common.Arg i (ConP _ _ ps)) = List.concat $ map (patternVars . fmap namedThing) ps
patternVars (Common.Arg i (LitP l) ) = []
patternVars (Common.Arg i ProjP{} ) = []
properlyMatching :: Pattern -> Bool
properlyMatching VarP{} = False
properlyMatching DotP{} = False
properlyMatching LitP{} = True
properlyMatching (ConP _ ci ps) = isNothing (conPRecord ci) ||
List.any (properlyMatching . namedArg) ps
properlyMatching ProjP{} = True
data Substitution
= IdS
| EmptyS
| Term :# Substitution
| Strengthen Empty Substitution
| Wk !Int Substitution
| Lift !Int Substitution
deriving (Show)
infixr 4 :#
absurdBody :: Abs Term
absurdBody = Abs absurdPatternName $ Var 0 []
isAbsurdBody :: Abs Term -> Bool
isAbsurdBody (Abs x (Var 0 [])) = isAbsurdPatternName x
isAbsurdBody _ = False
absurdPatternName :: PatVarName
absurdPatternName = "()"
isAbsurdPatternName :: PatVarName -> Bool
isAbsurdPatternName x = x == absurdPatternName
ignoreSharing :: Term -> Term
ignoreSharing v = v
ignoreSharingType :: Type -> Type
ignoreSharingType v = v
shared :: Term -> Term
shared v = v
sharedType :: Type -> Type
sharedType v = v
updateSharedFM :: (Monad m, Applicative m, Traversable f) => (Term -> m (f Term)) -> Term -> m (f Term)
updateSharedFM f v0@(Shared p) = do
fv <- f (derefPtr p)
flip traverse fv $ \v ->
case derefPtr (setPtr v p) of
Var _ [] -> return v
_ -> compressPointerChain v0 `pseq` return v0
updateSharedFM f v = f v
updateSharedM :: Monad m => (Term -> m Term) -> Term -> m Term
updateSharedM f v0@(Shared p) = do
v <- f (derefPtr p)
case derefPtr (setPtr v p) of
Var _ [] -> return v
_ -> compressPointerChain v0 `pseq` return v0
updateSharedM f v = f v
updateShared :: (Term -> Term) -> Term -> Term
updateShared f v0@(Shared p) =
case derefPtr (setPtr (f $ derefPtr p) p) of
v@(Var _ []) -> v
_ -> compressPointerChain v0 `pseq` v0
updateShared f v = f v
pointerChain :: Term -> [Ptr Term]
pointerChain (Shared p) = p : pointerChain (derefPtr p)
pointerChain _ = []
compressPointerChain :: Term -> Term
compressPointerChain v =
case reverse $ pointerChain v of
p:_:ps@(_:_) -> setPointers (Shared p) ps
_ -> v
where
setPointers _ [] = v
setPointers u (p : ps) =
setPtr u p `seq` setPointers u ps
var :: Nat -> Term
var i | i >= 0 = Var i []
| otherwise = __IMPOSSIBLE__
dontCare :: Term -> Term
dontCare v =
case ignoreSharing v of
DontCare{} -> v
_ -> DontCare v
typeDontCare :: Type
typeDontCare = El Prop (Sort Prop)
topSort :: Type
topSort = El Inf (Sort Inf)
prop :: Type
prop = sort Prop
sort :: Sort -> Type
sort s = El (sSuc s) $ Sort s
varSort :: Int -> Sort
varSort n = Type $ Max [Plus 0 $ NeutralLevel mempty $ Var n []]
sSuc :: Sort -> Sort
sSuc Prop = mkType 1
sSuc Inf = Inf
sSuc SizeUniv = SizeUniv
sSuc (DLub a b) = DLub (sSuc a) (fmap sSuc b)
sSuc (Type l) = Type $ levelSuc l
levelSuc :: Level -> Level
levelSuc (Max []) = Max [ClosedLevel 1]
levelSuc (Max as) = Max $ map inc as
where inc (ClosedLevel n) = ClosedLevel (n + 1)
inc (Plus n l) = Plus (n + 1) l
mkType :: Integer -> Sort
mkType n = Type $ Max [ClosedLevel n | n > 0]
impossibleTerm :: String -> Int -> Term
impossibleTerm file line = Lit $ LitString noRange $ unlines
[ "An internal error has occurred. Please report this as a bug."
, "Location of the error: " ++ file ++ ":" ++ show line
]
class SgTel a where
sgTel :: a -> Telescope
instance SgTel (ArgName, Dom Type) where
sgTel (x, dom) = ExtendTel dom $ Abs x EmptyTel
instance SgTel (Dom (ArgName, Type)) where
sgTel (Common.Dom ai (x, t)) = ExtendTel (Common.Dom ai t) $ Abs x EmptyTel
hackReifyToMeta :: Term
hackReifyToMeta = DontCare $ Lit $ LitInt noRange (42)
isHackReifyToMeta :: Term -> Bool
isHackReifyToMeta (DontCare (Lit (LitInt r (42)))) = r == noRange
isHackReifyToMeta _ = False
blockingMeta :: Blocked t -> Maybe MetaId
blockingMeta (Blocked m _) = Just m
blockingMeta NotBlocked{} = Nothing
blocked :: MetaId -> a -> Blocked a
blocked x = Blocked x
notBlocked :: a -> Blocked a
notBlocked = NotBlocked ReallyNotBlocked
stripDontCare :: Term -> Term
stripDontCare v = case ignoreSharing v of
DontCare v -> v
_ -> v
arity :: Type -> Nat
arity t = case ignoreSharing $ unEl t of
Pi _ b -> 1 + arity (unAbs b)
_ -> 0
argName :: Type -> String
argName = argN . ignoreSharing . unEl
where
argN (Pi _ b) = "." ++ argNameToString (absName b)
argN _ = __IMPOSSIBLE__
class Suggest a b where
suggest :: a -> b -> String
instance Suggest String String where
suggest "_" y = y
suggest x _ = x
instance Suggest (Abs a) (Abs b) where
suggest b1 b2 = suggest (absName b1) (absName b2)
instance Suggest String (Abs b) where
suggest x b = suggest x (absName b)
instance Suggest Name (Abs b) where
suggest n b = suggest (nameToArgName n) (absName b)
unSpine :: Term -> Term
unSpine v =
case hasElims v of
Just (h, es) -> unSpine' h [] es
Nothing -> v
where
unSpine' :: (Elims -> Term) -> Elims -> Elims -> Term
unSpine' h res es =
case es of
[] -> v
e@(Apply a) : es' -> unSpine' h (e : res) es'
Proj f : es' -> unSpine' (Def f) [Apply (defaultArg v)] es'
where v = h $ reverse res
hasElims :: Term -> Maybe (Elims -> Term, Elims)
hasElims v =
case ignoreSharing v of
Var i es -> Just (Var i, es)
Def f es -> Just (Def f, es)
MetaV x es -> Just (MetaV x, es)
Con{} -> Nothing
Lit{} -> Nothing
Lam{} -> Nothing
Pi{} -> Nothing
Sort{} -> Nothing
Level{} -> Nothing
DontCare{} -> Nothing
ExtLam{} -> Nothing
Shared{} -> __IMPOSSIBLE__
argFromElim :: Elim -> Arg Term
argFromElim (Apply u) = u
argFromElim Proj{} = __IMPOSSIBLE__
isApplyElim :: Elim -> Maybe (Arg Term)
isApplyElim (Apply u) = Just u
isApplyElim Proj{} = Nothing
allApplyElims :: Elims -> Maybe Args
allApplyElims = mapM isApplyElim
splitApplyElims :: Elims -> (Args, Elims)
splitApplyElims (Apply u : es) = (u :) *** id $ splitApplyElims es
splitApplyElims es = ([], es)
class IsProjElim e where
isProjElim :: e -> Maybe QName
instance IsProjElim Elim where
isProjElim (Proj d) = Just d
isProjElim Apply{} = Nothing
dropProjElims :: IsProjElim e => [e] -> [e]
dropProjElims = filter (isNothing . isProjElim)
argsFromElims :: Elims -> Args
argsFromElims = map argFromElim . dropProjElims
instance Null (Tele a) where
empty = EmptyTel
null EmptyTel = True
null ExtendTel{} = False
instance Null ClauseBody where
empty = NoBody
null NoBody = True
null _ = False
instance Null Clause where
empty = Clause empty empty empty empty empty empty
null (Clause r tel perm pats body t)
= null tel
&& null pats
&& null body
instance Show a => Show (Abs a) where
showsPrec p (Abs x a) = showParen (p > 0) $
showString "Abs " . shows x . showString " " . showsPrec 10 a
showsPrec p (NoAbs x a) = showParen (p > 0) $
showString "NoAbs " . shows x . showString " " . showsPrec 10 a
instance Show MetaId where
showsPrec p (MetaId n) = showParen (p > 0) $
showString "MetaId " . shows n
instance Sized (Tele a) where
size EmptyTel = 0
size (ExtendTel _ tel) = 1 + size tel
instance Sized a => Sized (Abs a) where
size = size . unAbs
class TermSize a where
termSize :: a -> Int
termSize = getSum . tsize
tsize :: a -> Sum Int
instance (Foldable t, TermSize a) => TermSize (t a) where
tsize = foldMap tsize
instance TermSize Term where
tsize v = case v of
Var _ vs -> 1 + tsize vs
Def _ vs -> 1 + tsize vs
Con _ vs -> 1 + tsize vs
MetaV _ vs -> 1 + tsize vs
Level l -> tsize l
Lam _ f -> 1 + tsize f
Lit _ -> 1
Pi a b -> 1 + tsize a + tsize b
Sort s -> tsize s
DontCare mv -> tsize mv
Shared p -> tsize (derefPtr p)
ExtLam{} -> __IMPOSSIBLE__
instance TermSize Sort where
tsize s = case s of
Type l -> 1 + tsize l
Prop -> 1
Inf -> 1
SizeUniv -> 1
DLub s s' -> 1 + tsize s + tsize s'
instance TermSize Level where
tsize (Max as) = 1 + tsize as
instance TermSize PlusLevel where
tsize (ClosedLevel _) = 1
tsize (Plus _ a) = tsize a
instance TermSize LevelAtom where
tsize (MetaLevel _ vs) = 1 + tsize vs
tsize (BlockedLevel _ v) = tsize v
tsize (NeutralLevel _ v) = tsize v
tsize (UnreducedLevel v) = tsize v
instance TermSize Substitution where
tsize IdS = 1
tsize EmptyS = 1
tsize (Wk _ rho) = 1 + tsize rho
tsize (t :# rho) = 1 + tsize t + tsize rho
tsize (Strengthen _ rho) = 1 + tsize rho
tsize (Lift _ rho) = 1 + tsize rho
instance KillRange ConHead where
killRange (ConHead c i fs) = killRange3 ConHead c i fs
instance KillRange Term where
killRange v = case v of
Var i vs -> killRange1 (Var i) vs
Def c vs -> killRange2 Def c vs
Con c vs -> killRange2 Con c vs
MetaV m vs -> killRange1 (MetaV m) vs
Lam i f -> killRange1 Lam i f
Lit l -> killRange1 Lit l
Level l -> killRange1 Level l
Pi a b -> killRange2 Pi a b
Sort s -> killRange1 Sort s
DontCare mv -> killRange1 DontCare mv
Shared p -> Shared $ updatePtr killRange p
ExtLam{} -> __IMPOSSIBLE__
instance KillRange Level where
killRange (Max as) = killRange1 Max as
instance KillRange PlusLevel where
killRange l@ClosedLevel{} = l
killRange (Plus n l) = killRange1 (Plus n) l
instance KillRange LevelAtom where
killRange (MetaLevel n as) = killRange1 (MetaLevel n) as
killRange (BlockedLevel m v) = killRange1 (BlockedLevel m) v
killRange (NeutralLevel r v) = killRange1 (NeutralLevel r) v
killRange (UnreducedLevel v) = killRange1 UnreducedLevel v
instance KillRange Type where
killRange (El s v) = killRange2 El s v
instance KillRange Sort where
killRange s = case s of
Prop -> Prop
Inf -> Inf
SizeUniv -> SizeUniv
Type a -> killRange1 Type a
DLub s1 s2 -> killRange2 DLub s1 s2
instance KillRange Substitution where
killRange IdS = IdS
killRange EmptyS = EmptyS
killRange (Wk n rho) = killRange1 (Wk n) rho
killRange (t :# rho) = killRange2 (:#) t rho
killRange (Strengthen err rho) = killRange1 (Strengthen err) rho
killRange (Lift n rho) = killRange1 (Lift n) rho
instance KillRange ConPatternInfo where
killRange (ConPatternInfo mr mt) = killRange1 (ConPatternInfo mr) mt
instance KillRange Pattern where
killRange p =
case p of
VarP{} -> p
DotP v -> killRange1 DotP v
ConP con info ps -> killRange3 ConP con info ps
LitP l -> killRange1 LitP l
ProjP q -> killRange1 ProjP q
instance KillRange Permutation where
killRange = id
instance KillRange Clause where
killRange (Clause r tel perm ps body t) = killRange6 Clause r tel perm ps body t
instance KillRange a => KillRange (ClauseBodyF a) where
killRange = fmap killRange
instance KillRange a => KillRange (Tele a) where
killRange = fmap killRange
instance KillRange a => KillRange (Blocked a) where
killRange = fmap killRange
instance KillRange a => KillRange (Abs a) where
killRange = fmap killRange
instance KillRange a => KillRange (Elim' a) where
killRange = fmap killRange
instanceUniverseBiT' [] [t| (([Type], [Clause]), Pattern) |]
instanceUniverseBiT' [] [t| (Args, Pattern) |]
instanceUniverseBiT' [] [t| (Elims, Pattern) |]
instanceUniverseBiT' [] [t| (([Type], [Clause]), Term) |]
instanceUniverseBiT' [] [t| (Args, Term) |]
instanceUniverseBiT' [] [t| (Elims, Term) |]
instanceUniverseBiT' [] [t| ([Term], Term) |]
instance Pretty MetaId where
pretty (MetaId n) = text $ "_" ++ show n
instance Pretty Substitution where
prettyPrec p rho = brackets $ pr rho
where
pr rho = case rho of
IdS -> text "idS"
EmptyS -> text "ε"
t :# rho -> prettyPrec 1 t <+> text ":#" <+> pr rho
Strengthen _ rho -> text "↓" <+> pr rho
Wk n rho -> text ("↑" ++ show n) <+> pr rho
Lift n rho -> text ("⇑" ++ show n) <+> pr rho
instance Pretty Term where
prettyPrec p v =
case ignoreSharing v of
Var x els -> text ("@" ++ show x) `pApp` els
Lam _ b ->
mparens (p > 0) $
sep [ text ("λ " ++ show (absName b) ++ " ->")
, nest 2 $ pretty (unAbs b) ]
Lit l -> pretty l
Def q els -> text (show q) `pApp` els
Con c vs -> text (show $ conName c) `pApp` map Apply vs
Pi a (NoAbs _ b) -> mparens (p > 0) $
sep [ prettyPrec 1 (unDom a) <+> text "->"
, nest 2 $ pretty b ]
Pi a b -> mparens (p > 0) $
sep [ pDom (domInfo a) (text (absName b) <+> text ":" <+> pretty (unDom a)) <+> text "->"
, nest 2 $ pretty (unAbs b) ]
Sort s -> pretty s
Level l -> pretty l
MetaV x els -> pretty x `pApp` els
DontCare v -> pretty v
Shared{} -> __IMPOSSIBLE__
ExtLam{} -> __IMPOSSIBLE__
where
pApp d els = mparens (not (null els) && p > 9) $
d <+> fsep (map (prettyPrec 10) els)
pDom i =
case getHiding i of
NotHidden -> parens
Hidden -> braces
Instance -> braces . braces
instance Pretty Level where
prettyPrec p (Max as) =
case as of
[] -> prettyPrec p (ClosedLevel 0)
[a] -> prettyPrec p a
_ -> mparens (p > 9) $ List.foldr1 (\a b -> text "lub" <+> a <+> b) $ map (prettyPrec 10) as
instance Pretty PlusLevel where
prettyPrec p l =
case l of
ClosedLevel n -> sucs p n $ \_ -> text "lzero"
Plus n a -> sucs p n $ \p -> prettyPrec p a
where
sucs p 0 d = d p
sucs p n d = mparens (p > 9) $ text "lsuc" <+> sucs 10 (n 1) d
instance Pretty LevelAtom where
prettyPrec p a =
case a of
MetaLevel x els -> prettyPrec p (MetaV x els)
BlockedLevel _ v -> prettyPrec p v
NeutralLevel _ v -> prettyPrec p v
UnreducedLevel v -> prettyPrec p v
instance Pretty Sort where
prettyPrec p s =
case s of
Type (Max []) -> text "Set"
Type (Max [ClosedLevel n]) -> text $ "Set" ++ show n
Type l -> mparens (p > 9) $ text "Set" <+> prettyPrec 10 l
Prop -> text "Prop"
Inf -> text "Setω"
SizeUniv -> text "SizeUniv"
DLub s b -> mparens (p > 9) $
text "dlub" <+> prettyPrec 10 s
<+> parens (sep [ text ("λ " ++ show (absName b) ++ " ->")
, nest 2 $ pretty (unAbs b) ])
instance Pretty Type where
prettyPrec p (El _ a) = prettyPrec p a
instance Pretty Elim where
prettyPrec p (Apply v) = prettyPrec p v
prettyPrec _ (Proj x) = text ("." ++ show x)
instance Pretty a => Pretty (Arg a) where
prettyPrec p a =
($ unArg a) $
case getHiding a of
NotHidden -> prettyPrec p
Hidden -> braces . pretty
Instance -> braces . braces . pretty