#if __GLASGOW_HASKELL__ <= 708
#endif
module Agda.Syntax.Internal
( module Agda.Syntax.Internal
, module Agda.Syntax.Abstract.Name
, module Agda.Utils.Pointer
, MetaId(..)
) where
import Prelude hiding (foldr, mapM, null)
import Control.Applicative hiding (empty)
import Control.Monad.Identity hiding (mapM)
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
import Agda.Syntax.Literal
import Agda.Syntax.Abstract (IsProjP(..))
import Agda.Syntax.Abstract.Name
import Agda.Utils.Empty
#if !MIN_VERSION_transformers(0,4,1)
import Agda.Utils.Except ( Error(noMsg) )
#endif
import Agda.Utils.Functor
import Agda.Utils.Geniplate
import Agda.Utils.Lens
import Agda.Utils.List
import Agda.Utils.Maybe
import Agda.Utils.Null
import Agda.Utils.Permutation
import Agda.Utils.Pointer
import Agda.Utils.Size
import Agda.Utils.Pretty as P
import Agda.Utils.Tuple
#include "undefined.h"
import Agda.Utils.Impossible
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)
| 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 (Dom 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)
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 ()
b@Blocked{} `mappend` _ = b
_ `mappend` b@Blocked{} = b
NotBlocked x _ `mappend` NotBlocked y _ = NotBlocked (x `mappend` y) ()
#if !MIN_VERSION_transformers(0,4,1)
instance Error Blocked_ where
noMsg = mempty
#endif
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
, namedClausePats :: [NamedArg DeBruijnPattern]
, clauseBody :: ClauseBody
, clauseType :: Maybe (Arg Type)
, clauseCatchall :: Bool
}
deriving (Typeable, Show)
clausePats :: Clause -> [Arg DeBruijnPattern]
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
imapClauseBody :: (Nat -> a -> b) -> ClauseBodyF a -> ClauseBodyF b
imapClauseBody f b = go 0 b
where
go i (Body x) = Body (f i x)
go _ NoBody = NoBody
go !i (Bind b) = Bind $ go (i + 1) <$> b
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
namedDBVarP :: Int -> PatVarName -> Named (Ranged PatVarName) DeBruijnPattern
namedDBVarP m = (fmap . fmap) (m,) . namedVarP
data ConPatternInfo = ConPatternInfo
{ conPRecord :: Maybe ConPOrigin
, conPType :: Maybe (Arg Type)
}
deriving (Typeable, Show)
noConPatternInfo :: ConPatternInfo
noConPatternInfo = ConPatternInfo Nothing Nothing
patternVars :: Arg (Pattern' a) -> [Arg (Either a Term)]
patternVars (Arg i (VarP x) ) = [Arg i $ Left x]
patternVars (Arg i (DotP t) ) = [Arg i $ Right t]
patternVars (Arg i (ConP _ _ ps)) = List.concat $ map (patternVars . fmap namedThing) ps
patternVars (Arg i (LitP l) ) = []
patternVars (Arg i ProjP{} ) = []
properlyMatching :: Pattern' a -> 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
instance IsProjP (Pattern' a) where
isProjP (ProjP d) = Just d
isProjP _ = Nothing
data Substitution' a
= IdS
| EmptyS
| a :# Substitution' a
| Strengthen Empty (Substitution' a)
| Wk !Int (Substitution' a)
| Lift !Int (Substitution' a)
deriving (Show, Functor, Foldable, Traversable)
type Substitution = Substitution' Term
type PatternSubstitution = Substitution' DeBruijnPattern
infixr 4 :#
data EqualityView
= EqualityType
{ eqtSort :: Sort
, eqtName :: QName
, eqtLevel :: Arg Term
, eqtType :: Arg Term
, eqtLhs :: Arg Term
, eqtRhs :: Arg Term
}
| OtherType Type
isEqualityType :: EqualityView -> Bool
isEqualityType EqualityType{} = True
isEqualityType OtherType{} = False
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 (Shared p) = ignoreSharing $ derefPtr p
ignoreSharing v = v
ignoreSharingType :: Type -> Type
ignoreSharingType (El s v) = El s (ignoreSharing v)
shared_ :: Term -> Term
shared_ v@Shared{} = v
shared_ v@(Var _ []) = v
shared_ v@(Con _ []) = v
shared_ v = Shared (newPtr v)
updateSharedFM
#if __GLASGOW_HASKELL__ <= 708
:: (Applicative m, Monad m, Traversable f)
#else
:: (Monad m, Traversable f)
#endif
=> (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
_ -> return $! compressPointerChain 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
_ -> return $! compressPointerChain 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
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
p:_:_ -> (Shared p)
_ -> v
where
setPointers u [] = u
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)
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 (Dom ai (x, t)) = ExtendTel (Dom ai t) $ Abs x EmptyTel
instance SgTel (Dom Type) where
sgTel dom = sgTel (stringToArgName "_", dom)
hackReifyToMeta :: Term
hackReifyToMeta = DontCare $ Lit $ LitNat noRange (42)
isHackReifyToMeta :: Term -> Bool
isHackReifyToMeta (DontCare (Lit (LitNat 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
notInScopeName :: ArgName -> ArgName
notInScopeName = stringToArgName . ("." ++) . argNameToString
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 _ (Abs _ v) -> case ignoreSharing v of
Var 0 [Proj f] -> Just (Def f, [])
_ -> Nothing
Lam{} -> Nothing
Pi{} -> Nothing
Sort{} -> Nothing
Level{} -> Nothing
DontCare{} -> 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) = mapFst (u :) $ 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
allProjElims :: Elims -> Maybe [QName]
allProjElims = mapM isProjElim
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 False
null (Clause r tel pats body t catchall)
= 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 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
#if __GLASGOW_HASKELL__ >= 710
instance (Foldable t, TermSize a) => TermSize (t a) where
#else
instance (Foldable t, TermSize a) => TermSize (t a) where
#endif
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)
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 a => TermSize (Substitution' a) 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 -> killRange2 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
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 a) => KillRange (Type' a) 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 a => KillRange (Pattern' a) where
killRange p =
case p of
VarP x -> killRange1 VarP x
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 Clause where
killRange (Clause r tel ps body t catchall) = killRange6 Clause r tel ps body t catchall
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 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__
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 (Pattern' a) where
prettyPrec n (VarP x) = prettyPrec n x
prettyPrec _ (DotP t) = text "." P.<> prettyPrec 10 t
prettyPrec n (ConP c i ps) = mparens (n > 0) $
text (show $ conName c) <+> fsep (map (pretty . namedArg) ps)
prettyPrec _ (LitP l) = text (show l)
prettyPrec _ (ProjP q) = text (show q)
instance Pretty a => Pretty (ClauseBodyF a) where
pretty b = case b of
Bind (NoAbs _ b) -> pretty b
Bind (Abs x b) -> text (show x ++ ".") <+> pretty b
Body t -> pretty t
NoBody -> text "()"