{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE PatternSynonyms #-}
{-# 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 GHC.Stack (HasCallStack, freezeCallStack, callStack)
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.Lens
import Agda.Utils.Null
import Agda.Utils.Size
import Agda.Utils.Pretty
import Agda.Utils.Tuple
import Agda.Utils.Impossible
data Dom' t e = Dom
{ domInfo :: ArgInfo
, domFinite :: !Bool
, domName :: Maybe NamedName
, domTactic :: Maybe t
, unDom :: e
} deriving (Data, Show, Functor, Foldable, Traversable)
type Dom = Dom' Term
instance Decoration (Dom' t) where
traverseF f (Dom ai b x t a) = Dom ai b x t <$> f a
instance HasRange a => HasRange (Dom' t a) where
getRange = getRange . unDom
instance (KillRange t, KillRange a) => KillRange (Dom' t a) where
killRange (Dom info b x t a) = killRange5 Dom info b x t a
instance Eq a => Eq (Dom' t a) where
Dom (ArgInfo h1 m1 _ _) b1 s1 _ x1 == Dom (ArgInfo h2 m2 _ _) b2 s2 _ x2 =
(h1, m1, b1, s1, x1) == (h2, m2, b2, s2, x2)
instance LensNamed NamedName (Dom' t e) where
lensNamed f dom = f (domName dom) <&> \ nm -> dom { domName = nm }
instance LensArgInfo (Dom' t e) where
getArgInfo = domInfo
setArgInfo ai dom = dom { domInfo = ai }
mapArgInfo f dom = dom { domInfo = f $ domInfo dom }
instance LensHiding (Dom' t e) where
instance LensModality (Dom' t e) where
instance LensOrigin (Dom' t e) where
instance LensFreeVariables (Dom' t e) where
instance LensRelevance (Dom' t e) where
instance LensQuantity (Dom' t e) where
instance LensCohesion (Dom' t e) where
argFromDom :: Dom' t a -> Arg a
argFromDom Dom{domInfo = i, unDom = a} = Arg i a
namedArgFromDom :: Dom' t a -> NamedArg a
namedArgFromDom Dom{domInfo = i, domName = s, unDom = a} = Arg i $ Named s a
domFromArg :: Arg a -> Dom a
domFromArg (Arg i a) = Dom i False Nothing Nothing a
domFromNamedArg :: NamedArg a -> Dom a
domFromNamedArg (Arg i a) = Dom i False (nameOf a) Nothing (namedThing a)
defaultDom :: a -> Dom a
defaultDom = defaultArgDom defaultArgInfo
defaultArgDom :: ArgInfo -> a -> Dom a
defaultArgDom info x = domFromArg (Arg info x)
defaultNamedArgDom :: ArgInfo -> String -> a -> Dom a
defaultNamedArgDom info s x = (defaultArgDom info x) { domName = Just $ WithOrigin Inserted $ unranged s }
type Args = [Arg Term]
type NamedArgs = [NamedArg Term]
data ConHead = ConHead
{ conName :: QName
, conInductive :: Induction
, conFields :: [Arg 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
| Dummy String Elims
deriving (Data, Show)
type ConInfo = ConOrigin
data Elim' a
= Apply (Arg a)
| Proj ProjOrigin QName
| IApply a a a
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
getOrigin IApply{} = UserWritten
mapOrigin f (Apply a) = Apply $ mapOrigin f a
mapOrigin f e@Proj{} = e
mapOrigin f e@IApply{} = e
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'' t a = El { _getSort :: Sort' t, unEl :: a }
deriving (Data, Show, Functor, Foldable, Traversable)
type Type' a = Type'' Term a
type Type = Type' Term
instance Decoration (Type'' t) 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 (Arg 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' t
= Type (Level' t)
| Prop (Level' t)
| Inf
| SizeUniv
| PiSort (Dom' t (Type'' t t)) (Abs (Sort' t))
| FunSort (Sort' t) (Sort' t)
| UnivSort (Sort' t)
| MetaS {-# UNPACK #-} !MetaId [Elim' t]
| DefS QName [Elim' t]
| DummyS String
deriving (Data, Show)
type Sort = Sort' Term
data Level' t = Max Integer [PlusLevel' t]
deriving (Show, Data)
type Level = Level' Term
data PlusLevel' t = Plus Integer (LevelAtom' t)
deriving (Show, Data)
type PlusLevel = PlusLevel' Term
data LevelAtom' t
= MetaLevel MetaId [Elim' t]
| BlockedLevel MetaId t
| NeutralLevel NotBlocked t
| UnreducedLevel t
deriving (Show, Data)
type LevelAtom = LevelAtom' Term
newtype BraveTerm = BraveTerm { unBrave :: Term } deriving (Data, Show)
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 (Data, 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
type NAPs = [NamedArg DeBruijnPattern]
data Clause = Clause
{ clauseLHSRange :: Range
, clauseFullRange :: Range
, clauseTel :: Telescope
, namedClausePats :: NAPs
, clauseBody :: Maybe Term
, clauseType :: Maybe (Arg Type)
, clauseCatchall :: Bool
, clauseRecursive :: Maybe Bool
, clauseUnreachable :: Maybe Bool
, clauseEllipsis :: ExpandedEllipsis
}
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 PatternInfo = PatternInfo
{ patOrigin :: PatOrigin
, patAsNames :: [Name]
} deriving (Data, Show, Eq)
defaultPatternInfo :: PatternInfo
defaultPatternInfo = PatternInfo PatOSystem []
data PatOrigin
= PatOSystem
| PatOSplit
| PatOVar Name
| PatODot
| PatOWild
| PatOCon
| PatORec
| PatOLit
| PatOAbsurd
deriving (Data, Show, Eq)
data Pattern' x
= VarP PatternInfo x
| DotP PatternInfo Term
| ConP ConHead ConPatternInfo [NamedArg (Pattern' x)]
| LitP PatternInfo Literal
| ProjP ProjOrigin QName
| IApplyP PatternInfo Term Term x
| DefP PatternInfo QName [NamedArg (Pattern' x)]
deriving (Data, Show, Functor, Foldable, Traversable)
type Pattern = Pattern' PatVarName
varP :: a -> Pattern' a
varP = VarP defaultPatternInfo
dotP :: Term -> Pattern' a
dotP = DotP defaultPatternInfo
litP :: Literal -> Pattern' a
litP = LitP defaultPatternInfo
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 $ WithOrigin Inserted $ unranged x
namedDBVarP :: Int -> PatVarName -> Named_ DeBruijnPattern
namedDBVarP m = (fmap . fmap) (\x -> DBPatVar x m) . namedVarP
absurdP :: Int -> DeBruijnPattern
absurdP = VarP (PatternInfo PatOAbsurd []) . DBPatVar absurdPatternName
data ConPatternInfo = ConPatternInfo
{ conPInfo :: PatternInfo
, conPRecord :: Bool
, conPFallThrough :: Bool
, conPType :: Maybe (Arg Type)
, conPLazy :: Bool
}
deriving (Data, Show)
noConPatternInfo :: ConPatternInfo
noConPatternInfo = ConPatternInfo defaultPatternInfo False False Nothing False
toConPatternInfo :: ConInfo -> ConPatternInfo
toConPatternInfo ConORec = noConPatternInfo{ conPInfo = PatternInfo PatORec [] , conPRecord = True }
toConPatternInfo _ = noConPatternInfo
fromConPatternInfo :: ConPatternInfo -> ConInfo
fromConPatternInfo i
| conPRecord i = patToConO $ patOrigin $ conPInfo i
| otherwise = ConOCon
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 _ (DefP _ _ ps)) = patternVars ps
patternVars (Arg _ (LitP _ _) ) = []
patternVars (Arg _ ProjP{} ) = []
patternVars (Arg i (IApplyP _ _ _ x)) = [Arg i $ Left x]
instance PatternVars a (NamedArg (Pattern' a)) where
patternVars = patternVars . fmap namedThing
instance PatternVars a b => PatternVars a [b] where
patternVars = concatMap patternVars
patternInfo :: Pattern' x -> Maybe PatternInfo
patternInfo (VarP i _) = Just i
patternInfo (DotP i _) = Just i
patternInfo (LitP i _) = Just i
patternInfo (ConP _ ci _) = Just $ conPInfo ci
patternInfo ProjP{} = Nothing
patternInfo (IApplyP i _ _ _) = Just i
patternInfo (DefP i _ _) = Just i
patternOrigin :: Pattern' x -> Maybe PatOrigin
patternOrigin = fmap patOrigin . patternInfo
properlyMatching :: Pattern' a -> Bool
properlyMatching = properlyMatching' True True
properlyMatching'
:: Bool
-> Bool
-> Pattern' a
-> Bool
properlyMatching' absP projP = \case
p | absP && patternOrigin p == Just PatOAbsurd -> True
ConP _ ci ps
| conPRecord ci -> List.any (properlyMatching . namedArg) ps
| otherwise -> True
LitP{} -> True
DefP{} -> True
ProjP{} -> projP
VarP{} -> False
DotP{} -> False
IApplyP{} -> False
instance IsProjP (Pattern' a) where
isProjP = \case
ProjP o d -> Just (o, unambiguous d)
_ -> 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
data PathView
= PathType
{ pathSort :: Sort
, pathName :: QName
, pathLevel :: Arg Term
, pathType :: Arg Term
, pathLhs :: Arg Term
, pathRhs :: Arg Term
}
| OType Type
isPathType :: PathView -> Bool
isPathType PathType{} = True
isPathType OType{} = False
data IntervalView
= IZero
| IOne
| IMin (Arg Term) (Arg Term)
| IMax (Arg Term) (Arg Term)
| INeg (Arg Term)
| OTerm Term
deriving Show
isIOne :: IntervalView -> Bool
isIOne IOne = True
isIOne _ = 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
dummyTerm' :: String -> Int -> Term
dummyTerm' file line = flip Dummy [] $ file ++ ":" ++ show line
dummyLevel' :: String -> Int -> Level
dummyLevel' file line = unreducedLevel $ dummyTerm' file line
dummyTerm :: String -> Int -> Term
dummyTerm file = dummyTerm' ("dummyTerm: " ++ file)
__DUMMY_TERM__ :: HasCallStack => Term
__DUMMY_TERM__ = withFileAndLine' (freezeCallStack callStack) dummyTerm
dummyLevel :: String -> Int -> Level
dummyLevel file = dummyLevel' ("dummyLevel: " ++ file)
__DUMMY_LEVEL__ :: HasCallStack => Level
__DUMMY_LEVEL__ = withFileAndLine' (freezeCallStack callStack) dummyLevel
dummySort :: String -> Int -> Sort
dummySort file line = DummyS $ file ++ ":" ++ show line
__DUMMY_SORT__ :: HasCallStack => Sort
__DUMMY_SORT__ = withFileAndLine' (freezeCallStack callStack) dummySort
dummyType :: String -> Int -> Type
dummyType file line = El (dummySort file line) $ dummyTerm' ("dummyType: " ++ file) line
__DUMMY_TYPE__ :: HasCallStack => Type
__DUMMY_TYPE__ = withFileAndLine' (freezeCallStack callStack) dummyType
dummyDom :: String -> Int -> Dom Type
dummyDom file line = defaultDom $ dummyType file line
__DUMMY_DOM__ :: HasCallStack => Dom Type
__DUMMY_DOM__ = withFileAndLine' (freezeCallStack callStack) dummyDom
pattern ClosedLevel :: Integer -> Level
pattern ClosedLevel n = Max n []
atomicLevel :: LevelAtom -> Level
atomicLevel a = Max 0 [ Plus 0 a ]
unreducedLevel :: Term -> Level
unreducedLevel v = atomicLevel $ UnreducedLevel v
topSort :: Type
topSort = sort Inf
sort :: Sort -> Type
sort s = El (UnivSort s) $ Sort s
varSort :: Int -> Sort
varSort n = Type $ atomicLevel $ NeutralLevel mempty $ var n
tmSort :: Term -> Sort
tmSort t = Type $ unreducedLevel t
levelPlus :: Integer -> Level -> Level
levelPlus m (Max n as) = Max (m + n) $ map pplus as
where pplus (Plus n l) = Plus (m + n) l
levelSuc :: Level -> Level
levelSuc = levelPlus 1
mkType :: Integer -> Sort
mkType n = Type $ ClosedLevel n
mkProp :: Integer -> Sort
mkProp n = Prop $ ClosedLevel n
isSort :: Term -> Maybe Sort
isSort v = case v of
Sort s -> Just s
_ -> Nothing
impossibleTerm :: String -> Int -> Term
impossibleTerm file line = flip Dummy [] $ unlines
[ "An internal error has occurred. Please report this as a bug."
, "Location of the error: " ++ file ++ ":" ++ show line
]
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@Dom{unDom = (x, a)} = ExtendTel (dom{unDom = a}) . Abs (f x)
telFromList :: ListTel -> Telescope
telFromList = telFromList' id
telToList :: Tele (Dom t) -> [Dom (ArgName,t)]
telToList EmptyTel = []
telToList (ExtendTel arg (Abs x tel)) = fmap (x,) arg : telToList tel
telToList (ExtendTel _ NoAbs{} ) = __IMPOSSIBLE__
listTel :: Lens' ListTel Telescope
listTel f = fmap telFromList . f . telToList
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 = ExtendTel (snd <$> dom) $ Abs (fst $ unDom dom) 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 = Blocked
notBlocked :: a -> Blocked a
notBlocked = NotBlocked ReallyNotBlocked
blocked_ :: MetaId -> Blocked_
blocked_ x = blocked x ()
notBlocked_ :: Blocked_
notBlocked_ = notBlocked ()
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
class Suggest a where
suggestName :: a -> Maybe String
instance Suggest String where
suggestName "_" = Nothing
suggestName x = Just x
instance Suggest (Abs b) where
suggestName = suggestName . absName
instance Suggest Name where
suggestName = suggestName . nameToArgName
instance Suggest Term where
suggestName (Lam _ v) = suggestName v
suggestName _ = Nothing
data Suggestion = forall a. Suggest a => Suggestion a
suggests :: [Suggestion] -> String
suggests [] = "x"
suggests (Suggestion x : xs) = fromMaybe (suggests xs) $ suggestName x
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
Dummy{} -> Nothing
isApplyElim :: Elim' a -> Maybe (Arg a)
isApplyElim (Apply u) = Just u
isApplyElim Proj{} = Nothing
isApplyElim (IApply _ _ r) = Just (defaultArg r)
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' a) where
isProjElim (Proj o d) = Just (o, d)
isProjElim Apply{} = Nothing
isProjElim IApply{} = Nothing
argsFromElims :: Elims -> Args
argsFromElims = mapMaybe isApplyElim
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 Nothing empty
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
Dummy{} -> 1
instance TermSize Sort where
tsize s = case s of
Type l -> 1 + tsize l
Prop l -> 1 + tsize l
Inf -> 1
SizeUniv -> 1
PiSort a s -> 1 + tsize a + tsize s
FunSort s1 s2 -> 1 + tsize s1 + tsize s2
UnivSort s -> 1 + tsize s
MetaS _ es -> 1 + tsize es
DefS _ es -> 1 + tsize es
DummyS{} -> 1
instance TermSize Level where
tsize (Max _ as) = 1 + tsize as
instance TermSize PlusLevel where
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
Dummy{} -> v
instance KillRange Level where
killRange (Max n as) = killRange1 (Max n) as
instance KillRange PlusLevel where
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
Inf -> Inf
SizeUniv -> SizeUniv
Type a -> killRange1 Type a
Prop a -> killRange1 Prop a
PiSort a s -> killRange2 PiSort a s
FunSort s1 s2 -> killRange2 FunSort s1 s2
UnivSort s -> killRange1 UnivSort s
MetaS x es -> killRange1 (MetaS x) es
DefS d es -> killRange2 DefS d es
DummyS{} -> s
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 PatternInfo where
killRange (PatternInfo o xs) = killRange2 PatternInfo o xs
instance KillRange ConPatternInfo where
killRange (ConPatternInfo i mr b mt lz) = killRange1 (ConPatternInfo i mr b) 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 o l -> killRange2 LitP o l
ProjP o q -> killRange1 (ProjP o) q
IApplyP o u t x -> killRange3 (IApplyP o) u t x
DefP o q ps -> killRange2 (DefP o) q ps
instance KillRange Clause where
killRange (Clause rl rf tel ps body t catchall recursive unreachable ell) =
killRange10 Clause rl rf tel ps body t catchall recursive unreachable ell
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
instance Pretty a => Pretty (Substitution' a) where
prettyPrec = pr
where
pr p rho = case rho of
IdS -> "idS"
EmptyS err -> "emptyS"
t :# rho -> mparens (p > 2) $ sep [ pr 2 rho <> ",", prettyPrec 3 t ]
Strengthen _ rho -> mparens (p > 9) $ "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 [ "λ" <+> prettyHiding ai id (text . absName $ b) <+> "->"
, 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) <+> "->"
, nest 2 $ pretty b ]
Pi a b -> mparens (p > 0) $
sep [ pDom (domInfo a) (text (absName b) <+> ":" <+> pretty (unDom a)) <+> "->"
, 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
Dummy s es -> parens (text s) `pApp` es
where
pApp d els = mparens (not (null els) && p > 9) $
sep [d, nest 2 $ fsep (map (prettyPrec 10) els)]
instance (Pretty t, Pretty e) => Pretty (Dom' t e) where
pretty dom = pTac <+> pDom dom (pretty $ unDom dom)
where
pTac | Just t <- domTactic dom = "@" <> parens ("tactic" <+> pretty t)
| otherwise = empty
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 <+> "|-"
, nest 2 $ sep [ fsep (map (prettyPrec 10) ps) <+> "="
, nest 2 $ pBody b t ] ]
where
pBody Nothing _ = "(absurd)"
pBody (Just b) Nothing = pretty b
pBody (Just b) (Just t) = sep [ pretty b <+> ":", nest 2 $ pretty t ]
instance Pretty a => Pretty (Tele (Dom a)) where
pretty tel = fsep [ pDom a (text x <+> ":" <+> pretty (unDom a)) | (x, a) <- telToList tel ]
where
telToList EmptyTel = []
telToList (ExtendTel a tel) = (absName tel, a) : telToList (unAbs tel)
prettyPrecLevelSucs :: Int -> Integer -> (Int -> Doc) -> Doc
prettyPrecLevelSucs p 0 d = d p
prettyPrecLevelSucs p n d = mparens (p > 9) $ "lsuc" <+> prettyPrecLevelSucs 10 (n - 1) d
instance Pretty Level where
prettyPrec p (Max n as) =
case as of
[] -> prettyN
[a] | n == 0 -> prettyPrec p a
_ -> mparens (p > 9) $ List.foldr1 (\a b -> "lub" <+> a <+> b) $
[ prettyN | n > 0 ] ++ map (prettyPrec 10) as
where
prettyN = prettyPrecLevelSucs p n (const "lzero")
instance Pretty PlusLevel where
prettyPrec p (Plus n a) = prettyPrecLevelSucs p n $ \p -> prettyPrec p a
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 (ClosedLevel 0) -> "Set"
Type (ClosedLevel n) -> text $ "Set" ++ show n
Type l -> mparens (p > 9) $ "Set" <+> prettyPrec 10 l
Prop (ClosedLevel 0) -> "Prop"
Prop (ClosedLevel n) -> text $ "Prop" ++ show n
Prop l -> mparens (p > 9) $ "Prop" <+> prettyPrec 10 l
Inf -> "Setω"
SizeUniv -> "SizeUniv"
PiSort a b -> mparens (p > 9) $
"piSort" <+> pDom (domInfo a) (text (absName b) <+> ":" <+> pretty (unDom a))
<+> parens (sep [ text ("λ " ++ absName b ++ " ->")
, nest 2 $ pretty (unAbs b) ])
FunSort a b -> mparens (p > 9) $
"funSort" <+> prettyPrec 10 a <+> prettyPrec 10 b
UnivSort s -> mparens (p > 9) $ "univSort" <+> prettyPrec 10 s
MetaS x es -> prettyPrec p $ MetaV x es
DefS d es -> prettyPrec p $ Def d es
DummyS s -> parens $ text s
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)
prettyPrec p (IApply x y r) = prettyPrec p r
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) = "." <> prettyPrec 10 t
prettyPrec n (ConP c i nps)= mparens (n > 0 && not (null nps)) $
(lazy <> pretty (conName c)) <+> fsep (map (prettyPrec 10) ps)
where ps = map (fmap namedThing) nps
lazy | conPLazy i = "~"
| otherwise = empty
prettyPrec n (DefP o q nps)= mparens (n > 0 && not (null nps)) $
pretty q <+> fsep (map (prettyPrec 10) ps)
where ps = map (fmap namedThing) nps
prettyPrec _ (LitP _ l) = pretty l
prettyPrec _ (ProjP _o q) = text ("." ++ prettyShow q)
prettyPrec n (IApplyP _o _ _ x) = prettyPrec n x
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
Dummy _ es -> rnf es
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 l -> rnf l
Inf -> ()
SizeUniv -> ()
PiSort a b -> rnf (a, unAbs b)
FunSort a b -> rnf (a, b)
UnivSort a -> rnf a
MetaS _ es -> rnf es
DefS _ es -> rnf es
DummyS _ -> ()
instance NFData Level where
rnf (Max n as) = rnf (n, as)
instance NFData PlusLevel where
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{} = ()
rnf (IApply x y r) = rnf x `seq` rnf y `seq` rnf r
instance NFData e => NFData (Dom e) where
rnf (Dom a b c d e) = rnf a `seq` rnf b `seq` rnf c `seq` rnf d `seq` rnf e