summaryrefslogtreecommitdiff
path: root/src/full/Agda/Syntax/Internal.hs
diff options
context:
space:
mode:
Diffstat (limited to 'src/full/Agda/Syntax/Internal.hs')
-rw-r--r--src/full/Agda/Syntax/Internal.hs326
1 files changed, 195 insertions, 131 deletions
diff --git a/src/full/Agda/Syntax/Internal.hs b/src/full/Agda/Syntax/Internal.hs
index 50a78fc..a39c4fe 100644
--- a/src/full/Agda/Syntax/Internal.hs
+++ b/src/full/Agda/Syntax/Internal.hs
@@ -1,15 +1,8 @@
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE DeriveDataTypeable #-}
-{-# LANGUAGE DeriveFoldable #-}
-{-# LANGUAGE DeriveFunctor #-}
-{-# LANGUAGE DeriveTraversable #-}
-{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
-{-# LANGUAGE MultiParamTypeClasses #-}
-{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TemplateHaskell #-}
-{-# LANGUAGE TupleSections #-}
#if __GLASGOW_HASKELL__ <= 708
{-# LANGUAGE OverlappingInstances #-}
#endif
@@ -25,12 +18,13 @@ 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
+import Data.Semigroup (Semigroup, Monoid, (<>), mempty, mappend, Sum(..))
-- base-4.7 defines the Num instance for Sum
#if !(MIN_VERSION_base(4,7,0))
@@ -43,7 +37,7 @@ import Data.Typeable (Typeable)
import Agda.Syntax.Position
import Agda.Syntax.Common
import Agda.Syntax.Literal
-import Agda.Syntax.Abstract (IsProjP(..))
+import Agda.Syntax.Concrete.Pretty (prettyHiding)
import Agda.Syntax.Abstract.Name
import Agda.Utils.Empty
@@ -62,7 +56,8 @@ import Agda.Utils.Null
import Agda.Utils.Permutation
import Agda.Utils.Pointer
import Agda.Utils.Size
-import Agda.Utils.Pretty as P
+import qualified Agda.Utils.Pretty as P
+import Agda.Utils.Pretty hiding ((<>))
import Agda.Utils.Tuple
#include "undefined.h"
@@ -123,7 +118,7 @@ data Term = Var {-# UNPACK #-} !Int Elims -- ^ @x es@ neutral
| Lam ArgInfo (Abs Term) -- ^ Terms are beta normal. Relevance is ignored
| Lit Literal
| Def QName Elims -- ^ @f es@, possibly a delta/iota-redex
- | Con ConHead Args -- ^ @c vs@
+ | Con ConHead ConInfo Args -- ^ @c vs@ or @record { fs = vs }@
| Pi (Dom Type) (Abs Type) -- ^ dependent or non-dependent function space
| Sort Sort
| Level Level
@@ -136,9 +131,13 @@ data Term = Var {-# UNPACK #-} !Int Elims -- ^ @x es@ neutral
-- ^ Explicit sharing
deriving (Typeable, Show)
+type ConInfo = ConOrigin
+
-- | Eliminations, subsuming applications and projections.
--
-data Elim' a = Apply (Arg a) | Proj QName -- ^ name of a record projection
+data Elim' a
+ = Apply (Arg a) -- ^ Application.
+ | Proj ProjOrigin QName -- ^ Projection. 'QName' is name of a record projection.
deriving (Typeable, Show, Functor, Foldable, Traversable)
type Elim = Elim' Term
@@ -295,17 +294,20 @@ data NotBlocked
-- | 'ReallyNotBlocked' is the unit.
-- 'MissingClauses' is dominant.
-- @'StuckOn'{}@ should be propagated, if tied, we take the left.
-instance Monoid NotBlocked where
- -- ReallyNotBlocked is neutral
- mempty = ReallyNotBlocked
- ReallyNotBlocked `mappend` b = b
+instance Semigroup NotBlocked where
+ ReallyNotBlocked <> b = b
-- MissingClauses is dominant (absorptive)
- b@MissingClauses `mappend` _ = b
- _ `mappend` b@MissingClauses = b
+ b@MissingClauses <> _ = b
+ _ <> b@MissingClauses = b
-- StuckOn is second strongest
- b@StuckOn{} `mappend` _ = b
- _ `mappend` b@StuckOn{} = b
- b `mappend` _ = b
+ b@StuckOn{} <> _ = b
+ _ <> b@StuckOn{} = b
+ b <> _ = b
+
+instance Monoid NotBlocked where
+ -- ReallyNotBlocked is neutral
+ mempty = ReallyNotBlocked
+ mappend = (<>)
-- | Something where a meta variable may block reduction.
data Blocked t
@@ -329,11 +331,14 @@ instance Applicative Blocked where
-- | @'Blocked' t@ without the @t@.
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 ()
- b@Blocked{} `mappend` _ = b
- _ `mappend` b@Blocked{} = b
- NotBlocked x _ `mappend` NotBlocked y _ = NotBlocked (x `mappend` y) ()
+ mappend = (<>)
-- See issues 1573 and 1674.
#if !MIN_VERSION_transformers(0,4,1)
@@ -379,12 +384,12 @@ stuckOn e r =
-- * Definitions
---------------------------------------------------------------------------
--- | A clause is a list of patterns and the clause body should @Bind@.
+-- | A clause is a list of patterns and the clause body.
--
-- The telescope contains the types of the pattern variables and the
-- de Bruijn indices say how to get from the order the variables occur in
-- the patterns to the order they occur in the telescope. The body
--- binds the variables in the order they appear in the patterns.
+-- binds the variables in the order they appear in the telescope.
--
-- @clauseTel ~ permute clausePerm (patternVars namedClausePats)@
--
@@ -395,37 +400,25 @@ stuckOn e r =
data Clause = Clause
{ clauseRange :: Range
, clauseTel :: Telescope
- -- ^ @Δ@: The types of the pattern variables.
+ -- ^ @Δ@: The types of the pattern variables in dependency order.
, namedClausePats :: [NamedArg DeBruijnPattern]
- -- ^ @let Γ = patternVars namedClausePats@
- , clauseBody :: ClauseBody
- -- ^ @λΓ.v@
+ -- ^ @Δ ⊢ ps@. The de Bruijn indices refer to @Δ@.
+ , clauseBody :: Maybe Term
+ -- ^ @Just v@ with @Δ ⊢ v@ for a regular clause, or @Nothing@ for an
+ -- absurd one.
, clauseType :: Maybe (Arg Type)
-- ^ @Δ ⊢ t@. The type of the rhs under @clauseTel@.
-- Used, e.g., by @TermCheck@.
-- Can be 'Irrelevant' if we encountered an irrelevant projection
-- pattern on the lhs.
, clauseCatchall :: Bool
+ -- ^ Clause has been labelled as CATCHALL.
}
deriving (Typeable, Show)
clausePats :: Clause -> [Arg DeBruijnPattern]
clausePats = map (fmap namedThing) . namedClausePats
-data ClauseBodyF a = Body a
- | Bind (Abs (ClauseBodyF a))
- | NoBody -- ^ for absurd clauses.
- 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
@@ -454,22 +447,30 @@ data Pattern' x
-- The subpatterns do not contain any projection copatterns.
| LitP Literal
-- ^ E.g. @5@, @"hello"@.
- | ProjP QName
+ | ProjP ProjOrigin QName
-- ^ Projection copattern. Can only appear by itself.
deriving (Typeable, Show, Functor, Foldable, Traversable)
type Pattern = Pattern' PatVarName
-- ^ The @PatVarName@ is a name suggestion.
+varP :: ArgName -> Pattern
+varP = VarP
+
-- | Type used when numbering pattern variables.
-type DeBruijnPattern = Pattern' (Int, PatVarName)
+data DBPatVar = DBPatVar
+ { dbPatVarName :: PatVarName
+ , dbPatVarIndex :: Int
+ } deriving (Typeable, Show)
-namedVarP :: PatVarName -> Named (Ranged PatVarName) Pattern
-namedVarP x = Named named $ VarP x
+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 (Ranged PatVarName) DeBruijnPattern
-namedDBVarP m = (fmap . fmap) (m,) . namedVarP
+namedDBVarP :: Int -> PatVarName -> Named_ DeBruijnPattern
+namedDBVarP m = (fmap . fmap) (\x -> DBPatVar x m) . namedVarP
-- | The @ConPatternInfo@ states whether the constructor belongs to
-- a record type (@Just@) or data type (@Nothing@).
@@ -479,7 +480,7 @@ namedDBVarP m = (fmap . fmap) (m,) . namedVarP
-- The scope used for the type is given by any outer scope
-- plus the clause's telescope ('clauseTel').
data ConPatternInfo = ConPatternInfo
- { conPRecord :: Maybe ConPOrigin
+ { conPRecord :: Maybe ConOrigin
-- ^ @Nothing@ if data constructor.
-- @Just@ if record constructor.
, conPType :: Maybe (Arg Type)
@@ -495,6 +496,15 @@ data ConPatternInfo = ConPatternInfo
noConPatternInfo :: ConPatternInfo
noConPatternInfo = ConPatternInfo Nothing Nothing
+-- | Build partial 'ConPatternInfo' from 'ConInfo'
+toConPatternInfo :: ConInfo -> ConPatternInfo
+toConPatternInfo ConORec = ConPatternInfo (Just ConORec) Nothing
+toConPatternInfo _ = noConPatternInfo
+
+-- | Build 'ConInfo' from 'ConPatternInfo'.
+fromConPatternInfo :: ConPatternInfo -> ConInfo
+fromConPatternInfo = fromMaybe ConOSystem . conPRecord
+
-- | Extract pattern variables in left-to-right order.
-- A 'DotP' is also treated as variable (see docu for 'Clause').
patternVars :: Arg (Pattern' a) -> [Arg (Either a Term)]
@@ -505,8 +515,8 @@ patternVars (Arg i (LitP l) ) = []
patternVars (Arg i ProjP{} ) = []
-- | Does the pattern perform a match that could fail?
-properlyMatching :: Pattern' a -> Bool
-properlyMatching VarP{} = False
+properlyMatching :: DeBruijnPattern -> Bool
+properlyMatching (VarP x) = isAbsurdPatternName $ dbPatVarName x
properlyMatching DotP{} = False
properlyMatching LitP{} = True
properlyMatching (ConP _ ci ps) = isNothing (conPRecord ci) || -- not a record cons
@@ -514,8 +524,8 @@ properlyMatching (ConP _ ci ps) = isNothing (conPRecord ci) || -- not a record c
properlyMatching ProjP{} = True
instance IsProjP (Pattern' a) where
- isProjP (ProjP d) = Just d
- isProjP _ = Nothing
+ isProjP (ProjP o d) = Just (o, AmbQ [d])
+ isProjP _ = Nothing
-----------------------------------------------------------------------------
-- * Explicit substitutions
@@ -577,6 +587,11 @@ type PatternSubstitution = Substitution' DeBruijnPattern
infixr 4 :#
+instance Null (Substitution' a) where
+ empty = IdS
+ null IdS = True
+ null _ = False
+
---------------------------------------------------------------------------
-- * Views
@@ -635,7 +650,7 @@ ignoreSharingType (El s v) = El s (ignoreSharing v)
shared_ :: Term -> Term
shared_ v@Shared{} = v
shared_ v@(Var _ []) = v
-shared_ v@(Con _ []) = v -- Issue 1691: sharing (zero : Nat) destroys constructorForm
+shared_ v@(Con _ _ []) = v -- Issue 1691: sharing (zero : Nat) destroys constructorForm
shared_ v = Shared (newPtr v)
-- | Typically m would be TCM and f would be Blocked.
@@ -817,17 +832,23 @@ instance Suggest Name (Abs b) where
-- | Convert top-level postfix projections into prefix projections.
unSpine :: Term -> Term
-unSpine v =
+unSpine = unSpine' $ const True
+
+-- | Convert 'Proj' projection eliminations
+-- according to their 'ProjOrigin' into
+-- 'Def' projection applications.
+unSpine' :: (ProjOrigin -> Bool) -> Term -> Term
+unSpine' p v =
case hasElims v of
- Just (h, es) -> unSpine' h [] es
+ Just (h, es) -> loop h [] es
Nothing -> v
where
- unSpine' :: (Elims -> Term) -> Elims -> Elims -> Term
- unSpine' h res es =
+ loop :: (Elims -> Term) -> Elims -> Elims -> Term
+ loop 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'
+ [] -> 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
-- | A view distinguishing the neutrals @Var@, @Def@, and @MetaV@ which
@@ -842,8 +863,8 @@ hasElims v =
Lit{} -> Nothing
-- Andreas, 2016-04-13, Issue 1932: We convert λ x → x .f into f
Lam _ (Abs _ v) -> case ignoreSharing v of
- Var 0 [Proj f] -> Just (Def f, [])
- _ -> Nothing
+ Var 0 [Proj _o f] -> Just (Def f, [])
+ _ -> Nothing
Lam{} -> Nothing
Pi{} -> Nothing
Sort{} -> Nothing
@@ -859,30 +880,30 @@ getElims v = maybe default id $ hasElims v
-}
-- | Drop 'Apply' constructor. (Unsafe!)
-argFromElim :: Elim -> Arg Term
+argFromElim :: Elim' a -> Arg a
argFromElim (Apply u) = u
argFromElim Proj{} = __IMPOSSIBLE__
-- | Drop 'Apply' constructor. (Safe)
-isApplyElim :: Elim -> Maybe (Arg Term)
+isApplyElim :: Elim' a -> Maybe (Arg a)
isApplyElim (Apply u) = Just u
isApplyElim Proj{} = Nothing
-- | Drop 'Apply' constructors. (Safe)
-allApplyElims :: Elims -> Maybe Args
+allApplyElims :: [Elim' a] -> Maybe [Arg a]
allApplyElims = mapM isApplyElim
-- | Split at first non-'Apply'
-splitApplyElims :: Elims -> (Args, Elims)
+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 QName
+ isProjElim :: e -> Maybe (ProjOrigin, QName)
instance IsProjElim Elim where
- isProjElim (Proj d) = Just d
- isProjElim Apply{} = Nothing
+ isProjElim (Proj o d) = Just (o, d)
+ isProjElim Apply{} = Nothing
-- | Discard @Proj f@ entries.
dropProjElims :: IsProjElim e => [e] -> [e]
@@ -893,23 +914,9 @@ argsFromElims :: Elims -> Args
argsFromElims = map argFromElim . dropProjElims
-- | Drop 'Proj' constructors. (Safe)
-allProjElims :: Elims -> Maybe [QName]
+allProjElims :: Elims -> Maybe [(ProjOrigin, QName)]
allProjElims = mapM isProjElim
-{- NOTE: Elim' already contains Arg.
-
--- | Commute functors 'Arg' and 'Elim\''.
-swapArgElim :: Arg (Elim' a) -> Elim' (Arg a)
-
-swapArgElim (Arg ai (Apply a)) = Apply (Arg ai a)
-swapArgElim (Arg ai (Proj d)) = Proj d
-
--- IMPOSSIBLE TO DEFINE
-swapElimArg :: Elim' (Arg a) -> Arg (Elim' a)
-swapElimArg (Apply (Arg ai a)) = Arg ai (Apply a)
-swapElimArg (Proj d) = defaultArg (Proj d)
--}
-
---------------------------------------------------------------------------
-- * Null instances.
---------------------------------------------------------------------------
@@ -919,11 +926,6 @@ instance Null (Tele a) where
null EmptyTel = True
null ExtendTel{} = False
-instance Null ClauseBody where
- empty = NoBody
- null NoBody = True
- null _ = False
-
-- | A 'null' clause is one with no patterns and no rhs.
-- Should not exist in practice.
instance Null Clause where
@@ -988,7 +990,7 @@ instance TermSize Term where
tsize v = case v of
Var _ vs -> 1 + tsize vs
Def _ vs -> 1 + tsize vs
- Con _ vs -> 1 + tsize vs
+ Con _ _ vs -> 1 + tsize vs
MetaV _ vs -> 1 + tsize vs
Level l -> tsize l
Lam _ f -> 1 + tsize f
@@ -1038,7 +1040,7 @@ 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
+ 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
@@ -1083,6 +1085,9 @@ instance KillRange Substitution where
instance KillRange ConPatternInfo where
killRange (ConPatternInfo mr mt) = killRange1 (ConPatternInfo mr) mt
+instance KillRange DBPatVar where
+ killRange (DBPatVar x i) = killRange2 DBPatVar x i
+
instance KillRange a => KillRange (Pattern' a) where
killRange p =
case p of
@@ -1090,14 +1095,11 @@ instance KillRange a => KillRange (Pattern' a) where
DotP v -> killRange1 DotP v
ConP con info ps -> killRange3 ConP con info ps
LitP l -> killRange1 LitP l
- ProjP q -> killRange1 ProjP q
+ ProjP o q -> killRange1 (ProjP o) 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
@@ -1126,48 +1128,65 @@ instanceUniverseBiT' [] [t| ([Term], Term) |]
-- * Simple pretty printing
-----------------------------------------------------------------------------
-instance Pretty Substitution where
- prettyPrec p rho = brackets $ pr rho
+instance Pretty a => Pretty (Substitution' a) where
+ prettyPrec p rho = pr p rho
where
- pr rho = case rho of
+ pr p 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
+ EmptyS -> 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 ignoreSharing v of
Var x els -> text ("@" ++ show x) `pApp` els
- Lam _ b ->
+ Lam ai b ->
mparens (p > 0) $
- sep [ text ("λ " ++ show (absName b) ++ " ->")
+ sep [ text "λ" <+> prettyHiding ai id (text . show . absName $ b) <+> text "->"
, 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
+ Con c ci 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
+ Sort s -> prettyPrec p s
+ Level l -> prettyPrec p l
MetaV x els -> pretty x `pApp` els
- DontCare v -> pretty v
+ DontCare v -> prettyPrec p v
Shared{} -> __IMPOSSIBLE__
where
pApp d els = mparens (not (null els) && p > 9) $
- d <+> fsep (map (prettyPrec 10) els)
+ 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 ]
- pDom i =
- case getHiding i of
- NotHidden -> parens
- Hidden -> braces
- Instance -> braces . braces
+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) =
@@ -1211,26 +1230,71 @@ 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)
+ prettyPrec p (Apply v) = prettyPrec p v
+ prettyPrec _ (Proj _o x) = text ("." ++ show x)
+
+instance Pretty DBPatVar where
+ prettyPrec _ x = text $ patVarNameToString (dbPatVarName x) ++ "@" ++ show (dbPatVarIndex 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 n (ConP c i nps)= mparens (n > 0) $
+ text (show $ conName c) <+> fsep (map pretty ps)
+ where ps = map (fmap namedThing) nps
-- -- Version with printing record type:
-- prettyPrec _ (ConP c i ps) = (if b then braces else parens) $ prTy $
-- text (show $ conName c) <+> fsep (map (pretty . namedArg) ps)
-- where
- -- b = maybe False (== ConPImplicit) $ conPRecord i
+ -- b = maybe False (== ConOSystem) $ conPRecord i
-- prTy d = caseMaybe (conPType i) d $ \ t -> d <+> text ":" <+> pretty t
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 "()"
+ prettyPrec _ (ProjP _o q) = text ("." ++ show q)
+
+-----------------------------------------------------------------------------
+-- * NFData instances
+-----------------------------------------------------------------------------
+
+-- Note: only strict in the shape of the terms.
+
+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
+ Shared{} -> ()
+
+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 -> ()
+ DLub a b -> rnf (a, unAbs b)
+
+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{} = ()