{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE UndecidableInstances #-}
module Agda.Syntax.Internal
( module Agda.Syntax.Internal
, module Agda.Syntax.Abstract.Name
, MetaId(..)
) where
import Prelude hiding (foldr, mapM, null)
import Control.Applicative hiding (empty)
import Control.Monad.Identity hiding (mapM)
import Control.DeepSeq
import Data.Foldable ( Foldable, foldMap )
import Data.Function
import qualified Data.List as List
import Data.Maybe
import Data.Monoid ( Monoid, mempty, mappend )
import Data.Semigroup ( Semigroup, (<>), Sum(..) )
import Data.Traversable
import Data.Data (Data)
import Agda.Syntax.Position
import Agda.Syntax.Common
import Agda.Syntax.Literal
import Agda.Syntax.Concrete.Pretty (prettyHiding)
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.Maybe
import Agda.Utils.NonemptyList
import Agda.Utils.Null
import Agda.Utils.Permutation
import Agda.Utils.Size
import qualified Agda.Utils.Pretty as P
import Agda.Utils.Pretty hiding ((<>))
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 (Data, Show)
instance Eq ConHead where
(==) = (==) `on` conName
instance Ord ConHead where
(<=) = (<=) `on` conName
instance Pretty ConHead where
pretty = pretty . conName
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 {-# UNPACK #-} !Int Elims
| Lam ArgInfo (Abs Term)
| Lit Literal
| Def QName Elims
| Con ConHead ConInfo Elims
| Pi (Dom Type) (Abs Type)
| Sort Sort
| Level Level
| MetaV {-# UNPACK #-} !MetaId Elims
| DontCare Term
deriving (Data, Show)
type ConInfo = ConOrigin
data Elim' a
= Apply (Arg a)
| Proj ProjOrigin QName
deriving (Data, Show, Functor, Foldable, Traversable)
type Elim = Elim' Term
type Elims = [Elim]
instance LensOrigin (Elim' a) where
getOrigin (Apply a) = getOrigin a
getOrigin Proj{} = UserWritten
mapOrigin f (Apply a) = Apply $ mapOrigin f a
mapOrigin f e@Proj{} = e
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 (Data, 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 (Data, 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 (Data, Show, Functor, Foldable, Traversable)
type Telescope = Tele (Dom Type)
data Sort
= Type Level
| Prop
| Inf
| SizeUniv
| PiSort Sort (Abs Sort)
| UnivSort Sort
| MetaS {-# UNPACK #-} !MetaId Elims
deriving (Data, Show)
newtype Level = Max [PlusLevel]
deriving (Show, Data)
data PlusLevel
= ClosedLevel Integer
| Plus Integer LevelAtom
deriving (Show, Data)
data LevelAtom
= MetaLevel MetaId Elims
| BlockedLevel MetaId Term
| NeutralLevel NotBlocked Term
| UnreducedLevel Term
deriving (Show, Data)
data NotBlocked
= StuckOn Elim
| Underapplied
| AbsurdMatch
| MissingClauses
| ReallyNotBlocked
deriving (Show, Data)
instance Semigroup NotBlocked where
ReallyNotBlocked <> b = b
b@MissingClauses <> _ = b
_ <> b@MissingClauses = b
b@StuckOn{} <> _ = b
_ <> b@StuckOn{} = b
b <> _ = b
instance Monoid NotBlocked where
mempty = ReallyNotBlocked
mappend = (<>)
data Blocked t
= Blocked { theBlockingMeta :: MetaId , ignoreBlocking :: t }
| NotBlocked { blockingStatus :: NotBlocked, ignoreBlocking :: t }
deriving (Show, Functor, Foldable, Traversable)
instance Applicative Blocked where
pure = notBlocked
f <*> e = ((f $> ()) `mappend` (e $> ())) $> ignoreBlocking f (ignoreBlocking e)
type Blocked_ = Blocked ()
instance Semigroup Blocked_ where
b@Blocked{} <> _ = b
_ <> b@Blocked{} = b
NotBlocked x _ <> NotBlocked y _ = NotBlocked (x <> y) ()
instance Monoid Blocked_ where
mempty = notBlocked ()
mappend = (<>)
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
{ clauseLHSRange :: Range
, clauseFullRange :: Range
, clauseTel :: Telescope
, namedClausePats :: [NamedArg DeBruijnPattern]
, clauseBody :: Maybe Term
, clauseType :: Maybe (Arg Type)
, clauseCatchall :: Bool
, clauseUnreachable :: Maybe Bool
}
deriving (Data, Show)
clausePats :: Clause -> [Arg DeBruijnPattern]
clausePats = map (fmap namedThing) . namedClausePats
instance HasRange Clause where
getRange = clauseLHSRange
type PatVarName = ArgName
patVarNameToString :: PatVarName -> String
patVarNameToString = argNameToString
nameToPatVarName :: Name -> PatVarName
nameToPatVarName = nameToArgName
data PatOrigin
= PatOSystem
| PatOSplit
| PatOVar Name
| PatODot
| PatOWild
| PatOCon
| PatORec
| PatOLit
| PatOAbsurd
deriving (Data, Show, Eq)
data Pattern' x
= VarP PatOrigin x
| DotP PatOrigin Term
| ConP ConHead ConPatternInfo [NamedArg (Pattern' x)]
| LitP Literal
| ProjP ProjOrigin QName
deriving (Data, Show, Functor, Foldable, Traversable)
type Pattern = Pattern' PatVarName
varP :: a -> Pattern' a
varP = VarP PatOSystem
dotP :: Term -> Pattern' a
dotP = DotP PatOSystem
data DBPatVar = DBPatVar
{ dbPatVarName :: PatVarName
, dbPatVarIndex :: Int
} deriving (Data, Show, Eq)
type DeBruijnPattern = Pattern' DBPatVar
namedVarP :: PatVarName -> Named_ Pattern
namedVarP x = Named named $ varP x
where named = if isUnderscore x then Nothing else Just $ unranged x
namedDBVarP :: Int -> PatVarName -> Named_ DeBruijnPattern
namedDBVarP m = (fmap . fmap) (\x -> DBPatVar x m) . namedVarP
data ConPatternInfo = ConPatternInfo
{ conPRecord :: Maybe PatOrigin
, conPType :: Maybe (Arg Type)
, conPLazy :: Bool
}
deriving (Data, Show)
noConPatternInfo :: ConPatternInfo
noConPatternInfo = ConPatternInfo Nothing Nothing False
toConPatternInfo :: ConInfo -> ConPatternInfo
toConPatternInfo ConORec = noConPatternInfo{ conPRecord = Just PatORec }
toConPatternInfo _ = noConPatternInfo
fromConPatternInfo :: ConPatternInfo -> ConInfo
fromConPatternInfo = fromMaybe ConOCon . fmap patToConO . conPRecord
where
patToConO :: PatOrigin -> ConOrigin
patToConO = \case
PatOSystem -> ConOSystem
PatOSplit -> ConOSplit
PatOVar{} -> ConOSystem
PatODot -> ConOSystem
PatOWild -> ConOSystem
PatOCon -> ConOCon
PatORec -> ConORec
PatOLit -> __IMPOSSIBLE__
PatOAbsurd -> ConOSystem
class PatternVars a b | b -> a where
patternVars :: b -> [Arg (Either a Term)]
instance PatternVars a (Arg (Pattern' a)) where
patternVars (Arg i (VarP _ x) ) = [Arg i $ Left x]
patternVars (Arg i (DotP _ t) ) = [Arg i $ Right t]
patternVars (Arg _ (ConP _ _ ps)) = patternVars ps
patternVars (Arg _ (LitP _) ) = []
patternVars (Arg _ ProjP{} ) = []
instance PatternVars a (NamedArg (Pattern' a)) where
patternVars = patternVars . fmap namedThing
instance PatternVars a b => PatternVars a [b] where
patternVars = concatMap patternVars
patternOrigin :: Pattern' x -> Maybe PatOrigin
patternOrigin (VarP o _) = Just o
patternOrigin (DotP o _) = Just o
patternOrigin LitP{} = Nothing
patternOrigin (ConP _ ci _) = conPRecord ci
patternOrigin ProjP{} = Nothing
properlyMatching :: DeBruijnPattern -> Bool
properlyMatching p
| patternOrigin p == Just PatOAbsurd = True
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 o d) = Just (o, unambiguous d)
isProjP _ = Nothing
data Substitution' a
= IdS
| EmptyS Empty
| a :# Substitution' a
| Strengthen Empty (Substitution' a)
| Wk !Int (Substitution' a)
| Lift !Int (Substitution' a)
deriving ( Show
, Functor
, Foldable
, Traversable
, Data
)
type Substitution = Substitution' Term
type PatternSubstitution = Substitution' DeBruijnPattern
infixr 4 :#
instance Null (Substitution' a) where
empty = IdS
null IdS = True
null _ = False
data EqualityView
= EqualityType
{ eqtSort :: Sort
, eqtName :: QName
, eqtParams :: [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
var :: Nat -> Term
var i | i >= 0 = Var i []
| otherwise = __IMPOSSIBLE__
dontCare :: Term -> Term
dontCare v =
case v of
DontCare{} -> v
_ -> DontCare v
typeDontCare :: Type
typeDontCare = sort Prop
topSort :: Type
topSort = sort Inf
sort :: Sort -> Type
sort s = El (UnivSort s) $ Sort s
varSort :: Int -> Sort
varSort n = Type $ Max [Plus 0 $ NeutralLevel mempty $ var n]
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]
isSort :: Term -> Maybe Sort
isSort v = case v of
Sort s -> Just s
_ -> Nothing
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
]
hackReifyToMeta :: Term
hackReifyToMeta = DontCare $ Lit $ LitNat noRange (-42)
isHackReifyToMeta :: Term -> Bool
isHackReifyToMeta (DontCare (Lit (LitNat r (-42)))) = r == noRange
isHackReifyToMeta _ = False
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
type ListTel' a = [Dom (a, Type)]
type ListTel = ListTel' ArgName
telFromList' :: (a -> ArgName) -> ListTel' a -> Telescope
telFromList' f = List.foldr extTel EmptyTel
where
extTel (Dom info (x, a)) = ExtendTel (Dom info a) . Abs (f x)
telFromList :: ListTel -> Telescope
telFromList = telFromList' id
telToList :: Telescope -> ListTel
telToList EmptyTel = []
telToList (ExtendTel arg (Abs x tel)) = fmap (x,) arg : telToList tel
telToList (ExtendTel _ NoAbs{} ) = __IMPOSSIBLE__
class TelToArgs a where
telToArgs :: a -> [Arg ArgName]
instance TelToArgs ListTel where
telToArgs = map $ \ dom -> Arg (domInfo dom) (fst $ unDom dom)
instance TelToArgs Telescope where
telToArgs = telToArgs . telToList
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)
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 v of
DontCare v -> v
_ -> v
arity :: Type -> Nat
arity t = case unEl t of
Pi _ b -> 1 + arity (unAbs b)
_ -> 0
notInScopeName :: ArgName -> ArgName
notInScopeName = stringToArgName . ("." ++) . argNameToString
unNotInScopeName :: ArgName -> ArgName
unNotInScopeName = stringToArgName . undot . argNameToString
where undot ('.':s) = s
undot s = s
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 = unSpine' $ const True
unSpine' :: (ProjOrigin -> Bool) -> Term -> Term
unSpine' p v =
case hasElims v of
Just (h, es) -> loop h [] es
Nothing -> v
where
loop :: (Elims -> Term) -> Elims -> Elims -> Term
loop h res es =
case es of
[] -> v
Proj o f : es' | p o -> loop (Def f) [Apply (defaultArg v)] es'
e : es' -> loop h (e : res) es'
where v = h $ reverse res
hasElims :: Term -> Maybe (Elims -> Term, Elims)
hasElims v =
case 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 v of
Var 0 [Proj _o f] -> Just (Def f, [])
_ -> Nothing
Lam{} -> Nothing
Pi{} -> Nothing
Sort{} -> Nothing
Level{} -> Nothing
DontCare{} -> Nothing
argFromElim :: Elim' a -> Arg a
argFromElim (Apply u) = u
argFromElim Proj{} = __IMPOSSIBLE__
isApplyElim :: Elim' a -> Maybe (Arg a)
isApplyElim (Apply u) = Just u
isApplyElim Proj{} = Nothing
isApplyElim' :: Empty -> Elim' a -> Arg a
isApplyElim' e = fromMaybe (absurd e) . isApplyElim
allApplyElims :: [Elim' a] -> Maybe [Arg a]
allApplyElims = mapM isApplyElim
splitApplyElims :: [Elim' a] -> ([Arg a], [Elim' a])
splitApplyElims (Apply u : es) = mapFst (u :) $ splitApplyElims es
splitApplyElims es = ([], es)
class IsProjElim e where
isProjElim :: e -> Maybe (ProjOrigin, QName)
instance IsProjElim Elim where
isProjElim (Proj o d) = Just (o, d)
isProjElim Apply{} = Nothing
dropProjElims :: IsProjElim e => [e] -> [e]
dropProjElims = filter (isNothing . isProjElim)
argsFromElims :: Elims -> Args
argsFromElims = map argFromElim . dropProjElims
allProjElims :: Elims -> Maybe [(ProjOrigin, QName)]
allProjElims = mapM isProjElim
instance Null (Tele a) where
empty = EmptyTel
null EmptyTel = True
null ExtendTel{} = False
instance Null Clause where
empty = Clause empty empty empty empty empty empty False Nothing
null (Clause _ _ tel pats body _ _ _)
= 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
instance {-# OVERLAPPABLE #-} (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
instance TermSize Sort where
tsize s = case s of
Type l -> 1 + tsize l
Prop -> 1
Inf -> 1
SizeUniv -> 1
PiSort s s' -> 1 + tsize s + tsize s'
UnivSort s -> 1 + tsize s
MetaS _ es -> 1 + tsize es
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 ci vs -> killRange3 Con c ci 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
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
PiSort s1 s2 -> killRange2 PiSort s1 s2
UnivSort s -> killRange1 UnivSort s
MetaS x es -> killRange1 (MetaS x) es
instance KillRange Substitution where
killRange IdS = IdS
killRange (EmptyS err) = EmptyS err
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 PatOrigin where
killRange = id
instance KillRange ConPatternInfo where
killRange (ConPatternInfo mr mt lz) = killRange1 (ConPatternInfo mr) mt lz
instance KillRange DBPatVar where
killRange (DBPatVar x i) = killRange2 DBPatVar x i
instance KillRange a => KillRange (Pattern' a) where
killRange p =
case p of
VarP o x -> killRange2 VarP o x
DotP o v -> killRange2 DotP o v
ConP con info ps -> killRange3 ConP con info ps
LitP l -> killRange1 LitP l
ProjP o q -> killRange1 (ProjP o) q
instance KillRange Clause where
killRange (Clause rl rf tel ps body t catchall unreachable) =
killRange8 Clause rl rf tel ps body t catchall unreachable
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 a => Pretty (Substitution' a) where
prettyPrec p rho = pr p rho
where
pr p rho = case rho of
IdS -> text "idS"
EmptyS err -> text "emptyS"
t :# rho -> mparens (p > 2) $ sep [ pr 2 rho P.<> text ",", prettyPrec 3 t ]
Strengthen _ rho -> mparens (p > 9) $ text "strS" <+> pr 10 rho
Wk n rho -> mparens (p > 9) $ text ("wkS " ++ show n) <+> pr 10 rho
Lift n rho -> mparens (p > 9) $ text ("liftS " ++ show n) <+> pr 10 rho
instance Pretty Term where
prettyPrec p v =
case v of
Var x els -> text ("@" ++ show x) `pApp` els
Lam ai b ->
mparens (p > 0) $
sep [ text "λ" <+> prettyHiding ai id (text . absName $ b) <+> text "->"
, nest 2 $ pretty (unAbs b) ]
Lit l -> pretty l
Def q els -> pretty q `pApp` els
Con c ci vs -> pretty (conName c) `pApp` 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 -> prettyPrec p s
Level l -> prettyPrec p l
MetaV x els -> pretty x `pApp` els
DontCare v -> prettyPrec p v
where
pApp d els = mparens (not (null els) && p > 9) $
sep [d, nest 2 $ fsep (map (prettyPrec 10) els)]
pDom :: LensHiding a => a -> Doc -> Doc
pDom i =
case getHiding i of
NotHidden -> parens
Hidden -> braces
Instance{} -> braces . braces
instance Pretty Clause where
pretty Clause{clauseTel = tel, namedClausePats = ps, clauseBody = b, clauseType = t} =
sep [ pretty tel <+> text "|-"
, nest 2 $ sep [ fsep (map (prettyPrec 10) ps) <+> text "="
, nest 2 $ pBody b t ] ]
where
pBody Nothing _ = text "(absurd)"
pBody (Just b) Nothing = pretty b
pBody (Just b) (Just t) = sep [ pretty b <+> text ":", nest 2 $ pretty t ]
instance Pretty a => Pretty (Tele (Dom a)) where
pretty tel = fsep [ pDom a (text x <+> text ":" <+> pretty (unDom a)) | (x, a) <- telToList tel ]
where
telToList EmptyTel = []
telToList (ExtendTel a tel) = (absName tel, a) : telToList (unAbs tel)
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"
PiSort s b -> mparens (p > 9) $
text "piSort" <+> prettyPrec 10 s
<+> parens (sep [ text ("λ " ++ absName b ++ " ->")
, nest 2 $ pretty (unAbs b) ])
UnivSort s -> mparens (p > 9) $ text "univSort" <+> prettyPrec 10 s
MetaS x es -> prettyPrec p $ MetaV x es
instance Pretty Type where
prettyPrec p (El _ a) = prettyPrec p a
instance Pretty tm => Pretty (Elim' tm) where
prettyPrec p (Apply v) = prettyPrec p v
prettyPrec _ (Proj _o x) = text ("." ++ prettyShow x)
instance Pretty DBPatVar where
prettyPrec _ x = text $ patVarNameToString (dbPatVarName x) ++ "@" ++ show (dbPatVarIndex x)
instance Pretty a => Pretty (Pattern' a) where
prettyPrec n (VarP _o x) = prettyPrec n x
prettyPrec _ (DotP _o t) = text "." P.<> prettyPrec 10 t
prettyPrec n (ConP c i nps)= mparens (n > 0 && not (null nps)) $
pretty (conName c) <+> fsep (map (prettyPrec 10) ps)
where ps = map (fmap namedThing) nps
prettyPrec _ (LitP l) = pretty l
prettyPrec _ (ProjP _o q) = text ("." ++ prettyShow q)
instance NFData Term where
rnf v = case v of
Var _ es -> rnf es
Lam _ b -> rnf (unAbs b)
Lit l -> rnf l
Def _ es -> rnf es
Con _ _ vs -> rnf vs
Pi a b -> rnf (unDom a, unAbs b)
Sort s -> rnf s
Level l -> rnf l
MetaV _ es -> rnf es
DontCare v -> rnf v
instance NFData Type where
rnf (El s v) = rnf (s, v)
instance NFData Sort where
rnf s = case s of
Type l -> rnf l
Prop -> ()
Inf -> ()
SizeUniv -> ()
PiSort a b -> rnf (a, unAbs b)
UnivSort a -> rnf a
MetaS _ es -> rnf es
instance NFData Level where
rnf (Max as) = rnf as
instance NFData PlusLevel where
rnf (ClosedLevel n) = rnf n
rnf (Plus n l) = rnf (n, l)
instance NFData LevelAtom where
rnf (MetaLevel _ es) = rnf es
rnf (BlockedLevel _ v) = rnf v
rnf (NeutralLevel _ v) = rnf v
rnf (UnreducedLevel v) = rnf v
instance NFData a => NFData (Elim' a) where
rnf (Apply x) = rnf x
rnf Proj{} = ()