1{-# LANGUAGE PatternSynonyms            #-}
2
3module Agda.Syntax.Internal
4    ( module Agda.Syntax.Internal
5    , module Agda.Syntax.Internal.Blockers
6    , module Agda.Syntax.Internal.Elim
7    , module Agda.Syntax.Abstract.Name
8    , MetaId(..), ProblemId(..)
9    ) where
10
11import Prelude hiding (null)
12
13import Control.Monad.Identity
14import Control.DeepSeq
15
16import Data.Function
17import qualified Data.List as List
18import Data.Maybe
19import Data.Semigroup ( Semigroup, (<>), Sum(..) )
20import qualified Data.Set as Set
21import Data.Set (Set)
22
23import Data.Traversable
24import Data.Data (Data)
25
26import GHC.Generics (Generic)
27
28import Agda.Syntax.Position
29import Agda.Syntax.Common
30import Agda.Syntax.Literal
31import Agda.Syntax.Concrete.Pretty (prettyHiding)
32import Agda.Syntax.Abstract.Name
33import Agda.Syntax.Internal.Blockers
34import Agda.Syntax.Internal.Elim
35
36import Agda.Utils.CallStack
37    ( CallStack
38    , HasCallStack
39    , prettyCallSite
40    , headCallSite
41    , withCallerCallStack
42    )
43
44import Agda.Utils.Empty
45
46import Agda.Utils.Functor
47import Agda.Utils.Lens
48import Agda.Utils.Null
49import Agda.Utils.Size
50import Agda.Utils.Pretty
51import Agda.Utils.Tuple
52
53import Agda.Utils.Impossible
54
55---------------------------------------------------------------------------
56-- * Function type domain
57---------------------------------------------------------------------------
58
59-- | Similar to 'Arg', but we need to distinguish
60--   an irrelevance annotation in a function domain
61--   (the domain itself is not irrelevant!)
62--   from an irrelevant argument.
63--
64--   @Dom@ is used in 'Pi' of internal syntax, in 'Context' and 'Telescope'.
65--   'Arg' is used for actual arguments ('Var', 'Con', 'Def' etc.)
66--   and in 'Abstract' syntax and other situations.
67--
68--   [ cubical ] When @domFinite = True@ for the domain of a 'Pi'
69--   type, the elements should be compared by tabulating the domain type.
70--   Only supported in case the domain type is primIsOne, to obtain
71--   the correct equality for partial elements.
72--
73data Dom' t e = Dom
74  { domInfo   :: ArgInfo
75  , domFinite :: !Bool
76  , domName   :: Maybe NamedName  -- ^ e.g. @x@ in @{x = y : A} -> B@.
77  , domTactic :: Maybe t        -- ^ "@tactic e".
78  , unDom     :: e
79  } deriving (Data, Show, Functor, Foldable, Traversable)
80
81type Dom = Dom' Term
82
83instance Decoration (Dom' t) where
84  traverseF f (Dom ai b x t a) = Dom ai b x t <$> f a
85
86instance HasRange a => HasRange (Dom' t a) where
87  getRange = getRange . unDom
88
89instance (KillRange t, KillRange a) => KillRange (Dom' t a) where
90  killRange (Dom info b x t a) = killRange5 Dom info b x t a
91
92-- | Ignores 'Origin' and 'FreeVariables' and tactic.
93instance Eq a => Eq (Dom' t a) where
94  Dom (ArgInfo h1 m1 _ _ a1) b1 s1 _ x1 == Dom (ArgInfo h2 m2 _ _ a2) b2 s2 _ x2 =
95    (h1, m1, a1, b1, s1, x1) == (h2, m2, a2, b2, s2, x2)
96
97instance LensNamed (Dom' t e) where
98  type NameOf (Dom' t e) = NamedName
99  lensNamed f dom = f (domName dom) <&> \ nm -> dom { domName = nm }
100
101instance LensArgInfo (Dom' t e) where
102  getArgInfo        = domInfo
103  setArgInfo ai dom = dom { domInfo = ai }
104  mapArgInfo f  dom = dom { domInfo = f $ domInfo dom }
105
106-- The other lenses are defined through LensArgInfo
107
108instance LensHiding        (Dom' t e) where
109instance LensModality      (Dom' t e) where
110instance LensOrigin        (Dom' t e) where
111instance LensFreeVariables (Dom' t e) where
112instance LensAnnotation    (Dom' t e) where
113
114-- Since we have LensModality, we get relevance and quantity by default
115
116instance LensRelevance (Dom' t e) where
117instance LensQuantity  (Dom' t e) where
118instance LensCohesion  (Dom' t e) where
119
120argFromDom :: Dom' t a -> Arg a
121argFromDom Dom{domInfo = i, unDom = a} = Arg i a
122
123namedArgFromDom :: Dom' t a -> NamedArg a
124namedArgFromDom Dom{domInfo = i, domName = s, unDom = a} = Arg i $ Named s a
125
126-- The following functions are less general than they could be:
127-- @Dom@ could be replaced by @Dom' t@.
128-- However, this causes problems with instance resolution in several places.
129-- often for class AddContext.
130
131domFromArg :: Arg a -> Dom a
132domFromArg (Arg i a) = Dom i False Nothing Nothing a
133
134domFromNamedArg :: NamedArg a -> Dom a
135domFromNamedArg (Arg i a) = Dom i False (nameOf a) Nothing (namedThing a)
136
137defaultDom :: a -> Dom a
138defaultDom = defaultArgDom defaultArgInfo
139
140defaultArgDom :: ArgInfo -> a -> Dom a
141defaultArgDom info x = domFromArg (Arg info x)
142
143defaultNamedArgDom :: ArgInfo -> String -> a -> Dom a
144defaultNamedArgDom info s x = (defaultArgDom info x) { domName = Just $ WithOrigin Inserted $ unranged s }
145
146-- | Type of argument lists.
147--
148type Args       = [Arg Term]
149type NamedArgs  = [NamedArg Term]
150
151data DataOrRecord
152  = IsData
153  | IsRecord PatternOrCopattern
154  deriving (Data, Show, Eq, Generic)
155
156-- | Store the names of the record fields in the constructor.
157--   This allows reduction of projection redexes outside of TCM.
158--   For instance, during substitution and application.
159data ConHead = ConHead
160  { conName       :: QName         -- ^ The name of the constructor.
161  , conDataRecord :: DataOrRecord  -- ^ Data or record constructor?
162  , conInductive  :: Induction     -- ^ Record constructors can be coinductive.
163  , conFields     :: [Arg QName]   -- ^ The name of the record fields.
164      --   'Arg' is stored since the info in the constructor args
165      --   might not be accurate because of subtyping (issue #2170).
166  } deriving (Data, Show, Generic)
167
168instance Eq ConHead where
169  (==) = (==) `on` conName
170
171instance Ord ConHead where
172  (<=) = (<=) `on` conName
173
174instance Pretty ConHead where
175  pretty = pretty . conName
176
177instance HasRange ConHead where
178  getRange = getRange . conName
179
180instance SetRange ConHead where
181  setRange r = mapConName (setRange r)
182
183class LensConName a where
184  getConName :: a -> QName
185  setConName :: QName -> a -> a
186  setConName = mapConName . const
187  mapConName :: (QName -> QName) -> a -> a
188  mapConName f a = setConName (f (getConName a)) a
189
190instance LensConName ConHead where
191  getConName = conName
192  setConName c con = con { conName = c }
193
194
195-- | Raw values.
196--
197--   @Def@ is used for both defined and undefined constants.
198--   Assume there is a type declaration and a definition for
199--     every constant, even if the definition is an empty
200--     list of clauses.
201--
202data Term = Var {-# UNPACK #-} !Int Elims -- ^ @x es@ neutral
203          | Lam ArgInfo (Abs Term)        -- ^ Terms are beta normal. Relevance is ignored
204          | Lit Literal
205          | Def QName Elims               -- ^ @f es@, possibly a delta/iota-redex
206          | Con ConHead ConInfo Elims
207          -- ^ @c es@ or @record { fs = es }@
208          --   @es@ allows only Apply and IApply eliminations,
209          --   and IApply only for data constructors.
210          | Pi (Dom Type) (Abs Type)      -- ^ dependent or non-dependent function space
211          | Sort Sort
212          | Level Level
213          | MetaV {-# UNPACK #-} !MetaId Elims
214          | DontCare Term
215            -- ^ Irrelevant stuff in relevant position, but created
216            --   in an irrelevant context.  Basically, an internal
217            --   version of the irrelevance axiom @.irrAx : .A -> A@.
218          | Dummy String Elims
219            -- ^ A (part of a) term or type which is only used for internal purposes.
220            --   Replaces the @Sort Prop@ hack.
221            --   The @String@ typically describes the location where we create this dummy,
222            --   but can contain other information as well.
223            --   The second field accumulates eliminations in case we
224            --   apply a dummy term to more of them.
225  deriving (Data, Show)
226
227type ConInfo = ConOrigin
228
229type Elim = Elim' Term
230type Elims = [Elim]  -- ^ eliminations ordered left-to-right.
231
232-- | Binder.
233--
234--   'Abs': The bound variable might appear in the body.
235--   'NoAbs' is pseudo-binder, it does not introduce a fresh variable,
236--      similar to the @const@ of Haskell.
237--
238data Abs a = Abs   { absName :: ArgName, unAbs :: a }
239               -- ^ The body has (at least) one free variable.
240               --   Danger: 'unAbs' doesn't shift variables properly
241           | NoAbs { absName :: ArgName, unAbs :: a }
242  deriving (Data, Functor, Foldable, Traversable, Generic)
243
244instance Decoration Abs where
245  traverseF f (Abs   x a) = Abs   x <$> f a
246  traverseF f (NoAbs x a) = NoAbs x <$> f a
247
248-- | Types are terms with a sort annotation.
249--
250data Type'' t a = El { _getSort :: Sort' t, unEl :: a }
251  deriving (Data, Show, Functor, Foldable, Traversable)
252
253type Type' a = Type'' Term a
254
255type Type = Type' Term
256
257instance Decoration (Type'' t) where
258  traverseF f (El s a) = El s <$> f a
259
260class LensSort a where
261  lensSort ::  Lens' Sort a
262  getSort  :: a -> Sort
263  getSort a = a ^. lensSort
264
265instance LensSort Sort where
266  lensSort f s = f s <&> \ s' -> s'
267
268instance LensSort (Type' a) where
269  lensSort f (El s a) = f s <&> \ s' -> El s' a
270
271-- General instance leads to overlapping instances.
272-- instance (Decoration f, LensSort a) => LensSort (f a) where
273instance LensSort a => LensSort (Dom a) where
274  lensSort = traverseF . lensSort
275
276instance LensSort a => LensSort (Arg a) where
277  lensSort = traverseF . lensSort
278
279
280-- | Sequence of types. An argument of the first type is bound in later types
281--   and so on.
282data Tele a = EmptyTel
283            | ExtendTel a (Abs (Tele a))  -- ^ 'Abs' is never 'NoAbs'.
284  deriving (Data, Show, Functor, Foldable, Traversable, Generic)
285
286type Telescope = Tele (Dom Type)
287
288data IsFibrant = IsFibrant | IsStrict
289  deriving (Data, Show, Eq, Ord, Generic)
290
291-- | Sorts.
292--
293data Sort' t
294  = Type (Level' t)  -- ^ @Set ℓ@.
295  | Prop (Level' t)  -- ^ @Prop ℓ@.
296  | Inf IsFibrant Integer      -- ^ @Setωᵢ@.
297  | SSet (Level' t)  -- ^ @SSet ℓ@.
298  | SizeUniv    -- ^ @SizeUniv@, a sort inhabited by type @Size@.
299  | LockUniv    -- ^ @LockUniv@, a sort for locks.
300  | PiSort (Dom' t t) (Sort' t) (Abs (Sort' t)) -- ^ Sort of the pi type.
301  | FunSort (Sort' t) (Sort' t) -- ^ Sort of a (non-dependent) function type.
302  | UnivSort (Sort' t) -- ^ Sort of another sort.
303  | MetaS {-# UNPACK #-} !MetaId [Elim' t]
304  | DefS QName [Elim' t] -- ^ A postulated sort.
305  | DummyS String
306    -- ^ A (part of a) term or type which is only used for internal purposes.
307    --   Replaces the abuse of @Prop@ for a dummy sort.
308    --   The @String@ typically describes the location where we create this dummy,
309    --   but can contain other information as well.
310  deriving (Data, Show)
311
312type Sort = Sort' Term
313
314-- | A level is a maximum expression of a closed level and 0..n
315--   'PlusLevel' expressions each of which is an atom plus a number.
316data Level' t = Max Integer [PlusLevel' t]
317  deriving (Show, Data, Functor, Foldable, Traversable)
318
319type Level = Level' Term
320
321data PlusLevel' t = Plus Integer t
322  deriving (Show, Data, Functor, Foldable, Traversable)
323
324type PlusLevel = PlusLevel' Term
325type LevelAtom = Term
326
327---------------------------------------------------------------------------
328-- * Brave Terms
329---------------------------------------------------------------------------
330
331-- | Newtypes for terms that produce a dummy, rather than crash, when
332--   applied to incompatible eliminations.
333newtype BraveTerm = BraveTerm { unBrave :: Term } deriving (Data, Show)
334
335---------------------------------------------------------------------------
336-- * Blocked Terms
337---------------------------------------------------------------------------
338
339type Blocked    = Blocked' Term
340type NotBlocked = NotBlocked' Term
341--
342-- | @'Blocked a@ without the @a@.
343type Blocked_ = Blocked ()
344
345---------------------------------------------------------------------------
346-- * Definitions
347---------------------------------------------------------------------------
348
349-- | Named pattern arguments.
350type NAPs = [NamedArg DeBruijnPattern]
351
352-- | A clause is a list of patterns and the clause body.
353--
354--  The telescope contains the types of the pattern variables and the
355--  de Bruijn indices say how to get from the order the variables occur in
356--  the patterns to the order they occur in the telescope. The body
357--  binds the variables in the order they appear in the telescope.
358--
359--  @clauseTel ~ permute clausePerm (patternVars namedClausePats)@
360--
361--  Terms in dot patterns are valid in the clause telescope.
362--
363--  For the purpose of the permutation and the body dot patterns count
364--  as variables. TODO: Change this!
365data Clause = Clause
366    { clauseLHSRange  :: Range
367    , clauseFullRange :: Range
368    , clauseTel       :: Telescope
369      -- ^ @Δ@: The types of the pattern variables in dependency order.
370    , namedClausePats :: NAPs
371      -- ^ @Δ ⊢ ps@.  The de Bruijn indices refer to @Δ@.
372    , clauseBody      :: Maybe Term
373      -- ^ @Just v@ with @Δ ⊢ v@ for a regular clause, or @Nothing@ for an
374      --   absurd one.
375    , clauseType      :: Maybe (Arg Type)
376      -- ^ @Δ ⊢ t@.  The type of the rhs under @clauseTel@.
377      --   Used, e.g., by @TermCheck@.
378      --   Can be 'Irrelevant' if we encountered an irrelevant projection
379      --   pattern on the lhs.
380    , clauseCatchall  :: Bool
381      -- ^ Clause has been labelled as CATCHALL.
382    , clauseExact       :: Maybe Bool
383      -- ^ Pattern matching of this clause is exact, no catch-all case.
384      --   Computed by the coverage checker.
385      --   @Nothing@ means coverage checker has not run yet (clause may be inexact).
386      --   @Just False@ means clause is not exact.
387      --   @Just True@ means clause is exact.
388    , clauseRecursive   :: Maybe Bool
389      -- ^ @clauseBody@ contains recursive calls; computed by termination checker.
390      --   @Nothing@ means that termination checker has not run yet,
391      --   or that @clauseBody@ contains meta-variables;
392      --   these could be filled with recursive calls later!
393      --   @Just False@ means definitely no recursive call.
394      --   @Just True@ means definitely a recursive call.
395    , clauseUnreachable :: Maybe Bool
396      -- ^ Clause has been labelled as unreachable by the coverage checker.
397      --   @Nothing@ means coverage checker has not run yet (clause may be unreachable).
398      --   @Just False@ means clause is not unreachable.
399      --   @Just True@ means clause is unreachable.
400    , clauseEllipsis  :: ExpandedEllipsis
401      -- ^ Was this clause created by expansion of an ellipsis?
402    }
403  deriving (Data, Show, Generic)
404
405clausePats :: Clause -> [Arg DeBruijnPattern]
406clausePats = map (fmap namedThing) . namedClausePats
407
408instance HasRange Clause where
409  getRange = clauseLHSRange
410
411-- | Pattern variables.
412type PatVarName = ArgName
413
414patVarNameToString :: PatVarName -> String
415patVarNameToString = argNameToString
416
417nameToPatVarName :: Name -> PatVarName
418nameToPatVarName = nameToArgName
419
420data PatternInfo = PatternInfo
421  { patOrigin :: PatOrigin
422  , patAsNames :: [Name]
423  } deriving (Data, Show, Eq, Generic)
424
425defaultPatternInfo :: PatternInfo
426defaultPatternInfo = PatternInfo PatOSystem []
427
428-- | Origin of the pattern: what did the user write in this position?
429data PatOrigin
430  = PatOSystem         -- ^ Pattern inserted by the system
431  | PatOSplit          -- ^ Pattern generated by case split
432  | PatOVar Name       -- ^ User wrote a variable pattern
433  | PatODot            -- ^ User wrote a dot pattern
434  | PatOWild           -- ^ User wrote a wildcard pattern
435  | PatOCon            -- ^ User wrote a constructor pattern
436  | PatORec            -- ^ User wrote a record pattern
437  | PatOLit            -- ^ User wrote a literal pattern
438  | PatOAbsurd         -- ^ User wrote an absurd pattern
439  deriving (Data, Show, Eq, Generic)
440
441-- | Patterns are variables, constructors, or wildcards.
442--   @QName@ is used in @ConP@ rather than @Name@ since
443--     a constructor might come from a particular namespace.
444--     This also meshes well with the fact that values (i.e.
445--     the arguments we are matching with) use @QName@.
446--
447data Pattern' x
448  = VarP PatternInfo x
449    -- ^ @x@
450  | DotP PatternInfo Term
451    -- ^ @.t@
452  | ConP ConHead ConPatternInfo [NamedArg (Pattern' x)]
453    -- ^ @c ps@
454    --   The subpatterns do not contain any projection copatterns.
455  | LitP PatternInfo Literal
456    -- ^ E.g. @5@, @"hello"@.
457  | ProjP ProjOrigin QName
458    -- ^ Projection copattern.  Can only appear by itself.
459  | IApplyP PatternInfo Term Term x
460    -- ^ Path elimination pattern, like @VarP@ but keeps track of endpoints.
461  | DefP PatternInfo QName [NamedArg (Pattern' x)]
462    -- ^ Used for HITs, the QName should be the one from primHComp.
463  deriving (Data, Show, Functor, Foldable, Traversable, Generic)
464
465type Pattern = Pattern' PatVarName
466    -- ^ The @PatVarName@ is a name suggestion.
467
468varP :: a -> Pattern' a
469varP = VarP defaultPatternInfo
470
471dotP :: Term -> Pattern' a
472dotP = DotP defaultPatternInfo
473
474litP :: Literal -> Pattern' a
475litP = LitP defaultPatternInfo
476
477-- | Type used when numbering pattern variables.
478data DBPatVar = DBPatVar
479  { dbPatVarName  :: PatVarName
480  , dbPatVarIndex :: Int
481  } deriving (Data, Show, Eq, Generic)
482
483type DeBruijnPattern = Pattern' DBPatVar
484
485namedVarP :: PatVarName -> Named_ Pattern
486namedVarP x = Named named $ varP x
487  where named = if isUnderscore x then Nothing else Just $ WithOrigin Inserted $ unranged x
488
489namedDBVarP :: Int -> PatVarName -> Named_ DeBruijnPattern
490namedDBVarP m = (fmap . fmap) (\x -> DBPatVar x m) . namedVarP
491
492-- | Make an absurd pattern with the given de Bruijn index.
493absurdP :: Int -> DeBruijnPattern
494absurdP = VarP (PatternInfo PatOAbsurd []) . DBPatVar absurdPatternName
495
496-- | The @ConPatternInfo@ states whether the constructor belongs to
497--   a record type (@True@) or data type (@False@).
498--   In the former case, the @PatOrigin@ of the @conPInfo@ says
499--   whether the record pattern orginates from the expansion of an
500--   implicit pattern.
501--   The @Type@ is the type of the whole record pattern.
502--   The scope used for the type is given by any outer scope
503--   plus the clause's telescope ('clauseTel').
504data ConPatternInfo = ConPatternInfo
505  { conPInfo   :: PatternInfo
506    -- ^ Information on the origin of the pattern.
507  , conPRecord :: Bool
508    -- ^ @False@ if data constructor.
509    --   @True@ if record constructor.
510  , conPFallThrough :: Bool
511    -- ^ Should the match block on non-canonical terms or can it
512    --   proceed to the catch-all clause?
513  , conPType   :: Maybe (Arg Type)
514    -- ^ The type of the whole constructor pattern.
515    --   Should be present (@Just@) if constructor pattern is
516    --   is generated ordinarily by type-checking.
517    --   Could be absent (@Nothing@) if pattern comes from some
518    --   plugin (like Agsy).
519    --   Needed e.g. for with-clause stripping.
520  , conPLazy :: Bool
521    -- ^ Lazy patterns are generated by the forcing translation in the unifier
522    --   ('Agda.TypeChecking.Rules.LHS.Unify.unifyStep') and are dropped by
523    --   the clause compiler (TODO: not yet)
524    --   ('Agda.TypeChecking.CompiledClause.Compile.compileClauses') when the
525    --   variables they bind are unused. The GHC backend compiles lazy matches
526    --   to lazy patterns in Haskell (TODO: not yet).
527  }
528  deriving (Data, Show, Generic)
529
530noConPatternInfo :: ConPatternInfo
531noConPatternInfo = ConPatternInfo defaultPatternInfo False False Nothing False
532
533-- | Build partial 'ConPatternInfo' from 'ConInfo'
534toConPatternInfo :: ConInfo -> ConPatternInfo
535toConPatternInfo ConORec = noConPatternInfo{ conPInfo = PatternInfo PatORec [] , conPRecord = True }
536toConPatternInfo _ = noConPatternInfo
537
538-- | Build 'ConInfo' from 'ConPatternInfo'.
539fromConPatternInfo :: ConPatternInfo -> ConInfo
540fromConPatternInfo i = patToConO $ patOrigin $ conPInfo i
541  where
542    patToConO :: PatOrigin -> ConOrigin
543    patToConO = \case
544      PatOSystem -> ConOSystem
545      PatOSplit  -> ConOSplit
546      PatOVar{}  -> ConOSystem
547      PatODot    -> ConOSystem
548      PatOWild   -> ConOSystem
549      PatOCon    -> ConOCon
550      PatORec    -> ConORec
551      PatOLit    -> ConOCon
552      PatOAbsurd -> ConOSystem
553
554-- | Extract pattern variables in left-to-right order.
555--   A 'DotP' is also treated as variable (see docu for 'Clause').
556class PatternVars a where
557  type PatternVarOut a
558  patternVars :: a -> [Arg (Either (PatternVarOut a) Term)]
559
560instance PatternVars (Arg (Pattern' a)) where
561  type PatternVarOut (Arg (Pattern' a)) = a
562
563  -- patternVars :: Arg (Pattern' a) -> [Arg (Either a Term)]
564  patternVars (Arg i (VarP _ x)   ) = [Arg i $ Left x]
565  patternVars (Arg i (DotP _ t)   ) = [Arg i $ Right t]
566  patternVars (Arg _ (ConP _ _ ps)) = patternVars ps
567  patternVars (Arg _ (DefP _ _ ps)) = patternVars ps
568  patternVars (Arg _ (LitP _ _)   ) = []
569  patternVars (Arg _ ProjP{}      ) = []
570  patternVars (Arg i (IApplyP _ _ _ x)) = [Arg i $ Left x]
571
572
573instance PatternVars (NamedArg (Pattern' a)) where
574  type PatternVarOut (NamedArg (Pattern' a)) = a
575
576  patternVars = patternVars . fmap namedThing
577
578instance PatternVars a => PatternVars [a] where
579  type PatternVarOut [a] = PatternVarOut a
580
581  patternVars = concatMap patternVars
582
583-- | Retrieve the PatternInfo from a pattern
584patternInfo :: Pattern' x -> Maybe PatternInfo
585patternInfo (VarP i _)        = Just i
586patternInfo (DotP i _)        = Just i
587patternInfo (LitP i _)        = Just i
588patternInfo (ConP _ ci _)     = Just $ conPInfo ci
589patternInfo ProjP{}           = Nothing
590patternInfo (IApplyP i _ _ _) = Just i
591patternInfo (DefP i _ _)      = Just i
592
593-- | Retrieve the origin of a pattern
594patternOrigin :: Pattern' x -> Maybe PatOrigin
595patternOrigin = fmap patOrigin . patternInfo
596
597-- | Does the pattern perform a match that could fail?
598properlyMatching :: Pattern' a -> Bool
599properlyMatching = properlyMatching' True True
600
601properlyMatching'
602  :: Bool       -- ^ Should absurd patterns count as proper match?
603  -> Bool       -- ^ Should projection patterns count as proper match?
604  -> Pattern' a -- ^ The pattern.
605  -> Bool
606properlyMatching' absP projP = \case
607  p | absP && patternOrigin p == Just PatOAbsurd -> True
608  ConP _ ci ps    -- record constructors do not count as proper matches themselves
609    | conPRecord ci -> List.any (properlyMatching . namedArg) ps
610    | otherwise     -> True
611  LitP{}    -> True
612  DefP{}    -> True
613  ProjP{}   -> projP
614  VarP{}    -> False
615  DotP{}    -> False
616  IApplyP{} -> False
617
618instance IsProjP (Pattern' a) where
619  isProjP = \case
620    ProjP o d -> Just (o, unambiguous d)
621    _ -> Nothing
622
623-----------------------------------------------------------------------------
624-- * Explicit substitutions
625-----------------------------------------------------------------------------
626
627-- | Substitutions.
628
629data Substitution' a
630
631  = IdS
632    -- ^ Identity substitution.
633    --   @Γ ⊢ IdS : Γ@
634
635  | EmptyS Impossible
636    -- ^ Empty substitution, lifts from the empty context. First argument is @__IMPOSSIBLE__@.
637    --   Apply this to closed terms you want to use in a non-empty context.
638    --   @Γ ⊢ EmptyS : ()@
639
640  | a :# Substitution' a
641    -- ^ Substitution extension, ``cons''.
642    --   @
643    --     Γ ⊢ u : Aρ   Γ ⊢ ρ : Δ
644    --     ----------------------
645    --     Γ ⊢ u :# ρ : Δ, A
646    --   @
647
648  | Strengthen Impossible (Substitution' a)
649    -- ^ Strengthening substitution.  First argument is @__IMPOSSIBLE__@.
650    --   Apply this to a term which does not contain variable 0
651    --   to lower all de Bruijn indices by one.
652    --   @
653    --             Γ ⊢ ρ : Δ
654    --     ---------------------------
655    --     Γ ⊢ Strengthen ρ : Δ, A
656    --   @
657
658  | Wk !Int (Substitution' a)
659    -- ^ Weakening substitution, lifts to an extended context.
660    --   @
661    --         Γ ⊢ ρ : Δ
662    --     -------------------
663    --     Γ, Ψ ⊢ Wk |Ψ| ρ : Δ
664    --   @
665
666
667  | Lift !Int (Substitution' a)
668    -- ^ Lifting substitution.  Use this to go under a binder.
669    --   @Lift 1 ρ == var 0 :# Wk 1 ρ@.
670    --   @
671    --            Γ ⊢ ρ : Δ
672    --     -------------------------
673    --     Γ, Ψρ ⊢ Lift |Ψ| ρ : Δ, Ψ
674    --   @
675
676  deriving ( Show
677           , Functor
678           , Foldable
679           , Traversable
680           , Generic
681           )
682
683type Substitution = Substitution' Term
684type PatternSubstitution = Substitution' DeBruijnPattern
685
686infixr 4 :#
687
688instance Null (Substitution' a) where
689  empty = IdS
690  null IdS = True
691  null _   = False
692
693
694---------------------------------------------------------------------------
695-- * Views
696---------------------------------------------------------------------------
697
698-- | View type as equality type.
699
700data EqualityView
701  = EqualityType
702    { eqtSort  :: Sort     -- ^ Sort of this type.
703    , eqtName  :: QName    -- ^ Builtin EQUALITY.
704    , eqtParams :: [Arg Term] -- ^ Hidden.  Empty or @Level@.
705    , eqtType  :: Arg Term -- ^ Hidden
706    , eqtLhs   :: Arg Term -- ^ NotHidden
707    , eqtRhs   :: Arg Term -- ^ NotHidden
708    }
709  | OtherType Type -- ^ reduced
710  | IdiomType Type -- ^ reduced
711
712isEqualityType :: EqualityView -> Bool
713isEqualityType EqualityType{} = True
714isEqualityType OtherType{}    = False
715isEqualityType IdiomType{}    = False
716
717-- | View type as path type.
718
719data PathView
720  = PathType
721    { pathSort  :: Sort     -- ^ Sort of this type.
722    , pathName  :: QName    -- ^ Builtin PATH.
723    , pathLevel :: Arg Term -- ^ Hidden
724    , pathType  :: Arg Term -- ^ Hidden
725    , pathLhs   :: Arg Term -- ^ NotHidden
726    , pathRhs   :: Arg Term -- ^ NotHidden
727    }
728  | OType Type -- ^ reduced
729
730isPathType :: PathView -> Bool
731isPathType PathType{} = True
732isPathType OType{}    = False
733
734data IntervalView
735      = IZero
736      | IOne
737      | IMin (Arg Term) (Arg Term)
738      | IMax (Arg Term) (Arg Term)
739      | INeg (Arg Term)
740      | OTerm Term
741      deriving Show
742
743isIOne :: IntervalView -> Bool
744isIOne IOne = True
745isIOne _ = False
746
747---------------------------------------------------------------------------
748-- * Absurd Lambda
749---------------------------------------------------------------------------
750
751-- | Absurd lambdas are internally represented as identity
752--   with variable name "()".
753absurdBody :: Abs Term
754absurdBody = Abs absurdPatternName $ Var 0 []
755
756isAbsurdBody :: Abs Term -> Bool
757isAbsurdBody (Abs x (Var 0 [])) = isAbsurdPatternName x
758isAbsurdBody _                  = False
759
760absurdPatternName :: PatVarName
761absurdPatternName = "()"
762
763isAbsurdPatternName :: PatVarName -> Bool
764isAbsurdPatternName x = x == absurdPatternName
765
766---------------------------------------------------------------------------
767-- * Smart constructors
768---------------------------------------------------------------------------
769
770-- | An unapplied variable.
771var :: Nat -> Term
772var i | i >= 0    = Var i []
773      | otherwise = __IMPOSSIBLE__
774
775-- | Add 'DontCare' is it is not already a @DontCare@.
776dontCare :: Term -> Term
777dontCare v =
778  case v of
779    DontCare{} -> v
780    _          -> DontCare v
781
782type DummyTermKind = String
783
784-- | Construct a string representing the call-site that created the dummy thing.
785dummyLocName :: CallStack -> String
786dummyLocName cs = maybe __IMPOSSIBLE__ prettyCallSite (headCallSite cs)
787
788-- | Aux: A dummy term to constitute a dummy term/level/sort/type.
789dummyTermWith :: DummyTermKind -> CallStack -> Term
790dummyTermWith kind cs = flip Dummy [] $ concat [kind, ": ", dummyLocName cs]
791
792-- | A dummy level to constitute a level/sort created at location.
793--   Note: use macro __DUMMY_LEVEL__ !
794dummyLevel :: CallStack -> Level
795dummyLevel = atomicLevel . dummyTermWith "dummyLevel"
796
797-- | A dummy term created at location.
798--   Note: use macro __DUMMY_TERM__ !
799dummyTerm :: CallStack -> Term
800dummyTerm = dummyTermWith "dummyTerm"
801
802__DUMMY_TERM__ :: HasCallStack => Term
803__DUMMY_TERM__ = withCallerCallStack dummyTerm
804
805__DUMMY_LEVEL__ :: HasCallStack => Level
806__DUMMY_LEVEL__ = withCallerCallStack dummyLevel
807
808-- | A dummy sort created at location.
809--   Note: use macro __DUMMY_SORT__ !
810dummySort :: CallStack -> Sort
811dummySort = DummyS . dummyLocName
812
813__DUMMY_SORT__ :: HasCallStack => Sort
814__DUMMY_SORT__ = withCallerCallStack dummySort
815
816-- | A dummy type created at location.
817--   Note: use macro __DUMMY_TYPE__ !
818dummyType :: CallStack -> Type
819dummyType cs = El (dummySort cs) $ dummyTermWith "dummyType" cs
820
821__DUMMY_TYPE__ :: HasCallStack => Type
822__DUMMY_TYPE__ = withCallerCallStack dummyType
823
824-- | Context entries without a type have this dummy type.
825--   Note: use macro __DUMMY_DOM__ !
826dummyDom :: CallStack -> Dom Type
827dummyDom = defaultDom . dummyType
828
829__DUMMY_DOM__ :: HasCallStack => Dom Type
830__DUMMY_DOM__ = withCallerCallStack dummyDom
831
832-- | Constant level @n@
833pattern ClosedLevel :: Integer -> Level
834pattern ClosedLevel n = Max n []
835
836atomicLevel :: t -> Level' t
837atomicLevel a = Max 0 [ Plus 0 a ]
838
839varSort :: Int -> Sort
840varSort n = Type $ atomicLevel $ var n
841
842tmSort :: Term -> Sort
843tmSort t = Type $ atomicLevel t
844
845tmSSort :: Term -> Sort
846tmSSort t = SSet $ atomicLevel t
847
848-- | Given a constant @m@ and level @l@, compute @m + l@
849levelPlus :: Integer -> Level -> Level
850levelPlus m (Max n as) = Max (m + n) $ map pplus as
851  where pplus (Plus n l) = Plus (m + n) l
852
853levelSuc :: Level -> Level
854levelSuc = levelPlus 1
855
856mkType :: Integer -> Sort
857mkType n = Type $ ClosedLevel n
858
859mkProp :: Integer -> Sort
860mkProp n = Prop $ ClosedLevel n
861
862mkSSet :: Integer -> Sort
863mkSSet n = SSet $ ClosedLevel n
864
865isSort :: Term -> Maybe Sort
866isSort = \case
867  Sort s -> Just s
868  _      -> Nothing
869
870impossibleTerm :: CallStack -> Term
871impossibleTerm = flip Dummy [] . show . Impossible
872
873---------------------------------------------------------------------------
874-- * Telescopes.
875---------------------------------------------------------------------------
876
877-- | A traversal for the names in a telescope.
878mapAbsNamesM :: Applicative m => (ArgName -> m ArgName) -> Tele a -> m (Tele a)
879mapAbsNamesM f EmptyTel                  = pure EmptyTel
880mapAbsNamesM f (ExtendTel a (  Abs x b)) = ExtendTel a <$> (  Abs <$> f x <*> mapAbsNamesM f b)
881mapAbsNamesM f (ExtendTel a (NoAbs x b)) = ExtendTel a <$> (NoAbs <$> f x <*> mapAbsNamesM f b)
882  -- Ulf, 2013-11-06: Last case is really impossible but I'd rather find out we
883  --                  violated that invariant somewhere other than here.
884
885mapAbsNames :: (ArgName -> ArgName) -> Tele a -> Tele a
886mapAbsNames f = runIdentity . mapAbsNamesM (Identity . f)
887
888-- Ulf, 2013-11-06
889-- The record parameter is named "" inside the record module so we can avoid
890-- printing it (issue 208), but we don't want that to show up in the type of
891-- the functions in the module (issue 892). This function is used on the record
892-- module telescope before adding it to a type in
893-- TypeChecking.Monad.Signature.addConstant (to handle functions defined in
894-- record modules) and TypeChecking.Rules.Record.checkProjection (to handle
895-- record projections).
896replaceEmptyName :: ArgName -> Tele a -> Tele a
897replaceEmptyName x = mapAbsNames $ \ y -> if null y then x else y
898
899-- | Telescope as list.
900type ListTel' a = [Dom (a, Type)]
901type ListTel = ListTel' ArgName
902
903telFromList' :: (a -> ArgName) -> ListTel' a -> Telescope
904telFromList' f = List.foldr extTel EmptyTel
905  where
906    extTel dom@Dom{unDom = (x, a)} = ExtendTel (dom{unDom = a}) . Abs (f x)
907
908-- | Convert a list telescope to a telescope.
909telFromList :: ListTel -> Telescope
910telFromList = telFromList' id
911
912-- | Convert a telescope to its list form.
913telToList :: Tele (Dom t) -> [Dom (ArgName,t)]
914telToList EmptyTel                    = []
915telToList (ExtendTel arg (Abs x tel)) = fmap (x,) arg : telToList tel
916telToList (ExtendTel _    NoAbs{}   ) = __IMPOSSIBLE__
917
918-- | Lens to edit a 'Telescope' as a list.
919listTel :: Lens' ListTel Telescope
920listTel f = fmap telFromList . f . telToList
921
922-- | Drop the types from a telescope.
923class TelToArgs a where
924  telToArgs :: a -> [Arg ArgName]
925
926instance TelToArgs ListTel where
927  telToArgs = map $ \ dom -> Arg (domInfo dom) (fst $ unDom dom)
928
929instance TelToArgs Telescope where
930  telToArgs = telToArgs . telToList
931
932-- | Constructing a singleton telescope.
933class SgTel a where
934  sgTel :: a -> Telescope
935
936instance SgTel (ArgName, Dom Type) where
937  sgTel (x, !dom) = ExtendTel dom $ Abs x EmptyTel
938
939instance SgTel (Dom (ArgName, Type)) where
940  sgTel dom = ExtendTel (snd <$> dom) $ Abs (fst $ unDom dom) EmptyTel
941
942instance SgTel (Dom Type) where
943  sgTel dom = sgTel (stringToArgName "_", dom)
944
945---------------------------------------------------------------------------
946-- * Simple operations on terms and types.
947---------------------------------------------------------------------------
948
949-- | Removing a topmost 'DontCare' constructor.
950stripDontCare :: Term -> Term
951stripDontCare = \case
952  DontCare v -> v
953  v          -> v
954
955-- | Doesn't do any reduction.
956arity :: Type -> Nat
957arity t = case unEl t of
958  Pi  _ b -> 1 + arity (unAbs b)
959  _       -> 0
960
961-- | Suggest a name if available (i.e. name is not "_")
962class Suggest a where
963  suggestName :: a -> Maybe String
964
965instance Suggest String where
966  suggestName "_" = Nothing
967  suggestName  x  = Just x
968
969instance Suggest (Abs b) where
970  suggestName = suggestName . absName
971
972instance Suggest Name where
973  suggestName = suggestName . nameToArgName
974
975instance Suggest Term where
976  suggestName (Lam _ v) = suggestName v
977  suggestName _         = Nothing
978
979-- Wrapping @forall a. (Suggest a) => a@ into a datatype because
980-- GHC doesn't support impredicative polymorphism
981data Suggestion = forall a. Suggest a => Suggestion a
982
983suggests :: [Suggestion] -> String
984suggests []     = "x"
985suggests (Suggestion x : xs) = fromMaybe (suggests xs) $ suggestName x
986
987---------------------------------------------------------------------------
988-- * Eliminations.
989---------------------------------------------------------------------------
990
991-- | Convert top-level postfix projections into prefix projections.
992unSpine :: Term -> Term
993unSpine = unSpine' $ const True
994
995-- | Convert 'Proj' projection eliminations
996--   according to their 'ProjOrigin' into
997--   'Def' projection applications.
998unSpine' :: (ProjOrigin -> Bool) -> Term -> Term
999unSpine' p v =
1000  case hasElims v of
1001    Just (h, es) -> loop h [] es
1002    Nothing      -> v
1003  where
1004    loop :: (Elims -> Term) -> Elims -> Elims -> Term
1005    loop h res es =
1006      case es of
1007        []                   -> v
1008        Proj o f : es' | p o -> loop (Def f) [Apply (defaultArg v)] es'
1009        e        : es'       -> loop h (e : res) es'
1010      where v = h $ reverse res
1011
1012-- | A view distinguishing the neutrals @Var@, @Def@, and @MetaV@ which
1013--   can be projected.
1014hasElims :: Term -> Maybe (Elims -> Term, Elims)
1015hasElims v =
1016  case v of
1017    Var   i es -> Just (Var   i, es)
1018    Def   f es -> Just (Def   f, es)
1019    MetaV x es -> Just (MetaV x, es)
1020    Con{}      -> Nothing
1021    Lit{}      -> Nothing
1022    -- Andreas, 2016-04-13, Issue 1932: We convert λ x → x .f  into f
1023    Lam h (Abs _ v) | visible h -> case v of
1024      Var 0 [Proj _o f] -> Just (Def f, [])
1025      _ -> Nothing
1026    Lam{}      -> Nothing
1027    Pi{}       -> Nothing
1028    Sort{}     -> Nothing
1029    Level{}    -> Nothing
1030    DontCare{} -> Nothing
1031    Dummy{}    -> Nothing
1032
1033---------------------------------------------------------------------------
1034-- * Null instances.
1035---------------------------------------------------------------------------
1036
1037instance Null (Tele a) where
1038  empty = EmptyTel
1039  null EmptyTel    = True
1040  null ExtendTel{} = False
1041
1042-- | A 'null' clause is one with no patterns and no rhs.
1043--   Should not exist in practice.
1044instance Null Clause where
1045  empty = Clause empty empty empty empty empty empty False Nothing Nothing Nothing empty
1046  null (Clause _ _ tel pats body _ _ _ _ _ _)
1047    =  null tel
1048    && null pats
1049    && null body
1050
1051
1052---------------------------------------------------------------------------
1053-- * Show instances.
1054---------------------------------------------------------------------------
1055
1056instance Show a => Show (Abs a) where
1057  showsPrec p (Abs x a) = showParen (p > 0) $
1058    showString "Abs " . shows x . showString " " . showsPrec 10 a
1059  showsPrec p (NoAbs x a) = showParen (p > 0) $
1060    showString "NoAbs " . shows x . showString " " . showsPrec 10 a
1061
1062-- instance Show t => Show (Blocked t) where
1063--   showsPrec p (Blocked m x) = showParen (p > 0) $
1064--     showString "Blocked " . shows m . showString " " . showsPrec 10 x
1065--   showsPrec p (NotBlocked x) = showsPrec p x
1066
1067---------------------------------------------------------------------------
1068-- * Sized instances and TermSize.
1069---------------------------------------------------------------------------
1070
1071-- | The size of a telescope is its length (as a list).
1072instance Sized (Tele a) where
1073  size  EmptyTel         = 0
1074  size (ExtendTel _ tel) = 1 + size tel
1075
1076instance Sized a => Sized (Abs a) where
1077  size = size . unAbs
1078
1079-- | The size of a term is roughly the number of nodes in its
1080--   syntax tree.  This number need not be precise for logical
1081--   correctness of Agda, it is only used for reporting
1082--   (and maybe decisions regarding performance).
1083--
1084--   Not counting towards the term size are:
1085--
1086--     * sort and color annotations,
1087--     * projections.
1088--
1089class TermSize a where
1090  termSize :: a -> Int
1091  termSize = getSum . tsize
1092
1093  tsize :: a -> Sum Int
1094
1095instance {-# OVERLAPPABLE #-} (Foldable t, TermSize a) => TermSize (t a) where
1096  tsize = foldMap tsize
1097
1098instance TermSize Term where
1099  tsize = \case
1100    Var _ vs    -> 1 + tsize vs
1101    Def _ vs    -> 1 + tsize vs
1102    Con _ _ vs    -> 1 + tsize vs
1103    MetaV _ vs  -> 1 + tsize vs
1104    Level l     -> tsize l
1105    Lam _ f     -> 1 + tsize f
1106    Lit _       -> 1
1107    Pi a b      -> 1 + tsize a + tsize b
1108    Sort s      -> tsize s
1109    DontCare mv -> tsize mv
1110    Dummy{}     -> 1
1111
1112instance TermSize Sort where
1113  tsize = \case
1114    Type l    -> 1 + tsize l
1115    Prop l    -> 1 + tsize l
1116    Inf _ _   -> 1
1117    SSet l    -> 1 + tsize l
1118    SizeUniv  -> 1
1119    LockUniv  -> 1
1120    PiSort a s1 s2 -> 1 + tsize a + tsize s1 + tsize s2
1121    FunSort s1 s2 -> 1 + tsize s1 + tsize s2
1122    UnivSort s -> 1 + tsize s
1123    MetaS _ es -> 1 + tsize es
1124    DefS _ es  -> 1 + tsize es
1125    DummyS{}   -> 1
1126
1127instance TermSize Level where
1128  tsize (Max _ as) = 1 + tsize as
1129
1130instance TermSize PlusLevel where
1131  tsize (Plus _ a)      = tsize a
1132
1133instance TermSize a => TermSize (Substitution' a) where
1134  tsize IdS                = 1
1135  tsize (EmptyS _)         = 1
1136  tsize (Wk _ rho)         = 1 + tsize rho
1137  tsize (t :# rho)         = 1 + tsize t + tsize rho
1138  tsize (Strengthen _ rho) = 1 + tsize rho
1139  tsize (Lift _ rho)       = 1 + tsize rho
1140
1141---------------------------------------------------------------------------
1142-- * KillRange instances.
1143---------------------------------------------------------------------------
1144
1145instance KillRange DataOrRecord where
1146  killRange = id
1147
1148instance KillRange ConHead where
1149  killRange (ConHead c d i fs) = killRange4 ConHead c d i fs
1150
1151instance KillRange Term where
1152  killRange = \case
1153    Var i vs    -> killRange1 (Var i) vs
1154    Def c vs    -> killRange2 Def c vs
1155    Con c ci vs -> killRange3 Con c ci vs
1156    MetaV m vs  -> killRange1 (MetaV m) vs
1157    Lam i f     -> killRange2 Lam i f
1158    Lit l       -> killRange1 Lit l
1159    Level l     -> killRange1 Level l
1160    Pi a b      -> killRange2 Pi a b
1161    Sort s      -> killRange1 Sort s
1162    DontCare mv -> killRange1 DontCare mv
1163    v@Dummy{}   -> v
1164
1165instance KillRange Level where
1166  killRange (Max n as) = killRange1 (Max n) as
1167
1168instance KillRange PlusLevel where
1169  killRange (Plus n l) = killRange1 (Plus n) l
1170
1171instance (KillRange a) => KillRange (Type' a) where
1172  killRange (El s v) = killRange2 El s v
1173
1174instance KillRange Sort where
1175  killRange = \case
1176    Inf f n    -> Inf f n
1177    SizeUniv   -> SizeUniv
1178    LockUniv   -> LockUniv
1179    Type a     -> killRange1 Type a
1180    Prop a     -> killRange1 Prop a
1181    SSet a     -> killRange1 SSet a
1182    PiSort a s1 s2 -> killRange3 PiSort a s1 s2
1183    FunSort s1 s2 -> killRange2 FunSort s1 s2
1184    UnivSort s -> killRange1 UnivSort s
1185    MetaS x es -> killRange1 (MetaS x) es
1186    DefS d es  -> killRange2 DefS d es
1187    s@DummyS{} -> s
1188
1189instance KillRange Substitution where
1190  killRange IdS                  = IdS
1191  killRange (EmptyS err)         = EmptyS err
1192  killRange (Wk n rho)           = killRange1 (Wk n) rho
1193  killRange (t :# rho)           = killRange2 (:#) t rho
1194  killRange (Strengthen err rho) = killRange1 (Strengthen err) rho
1195  killRange (Lift n rho)         = killRange1 (Lift n) rho
1196
1197instance KillRange PatOrigin where
1198  killRange = id
1199
1200instance KillRange PatternInfo where
1201  killRange (PatternInfo o xs) = killRange2 PatternInfo o xs
1202
1203instance KillRange ConPatternInfo where
1204  killRange (ConPatternInfo i mr b mt lz) = killRange1 (ConPatternInfo i mr b) mt lz
1205
1206instance KillRange DBPatVar where
1207  killRange (DBPatVar x i) = killRange2 DBPatVar x i
1208
1209instance KillRange a => KillRange (Pattern' a) where
1210  killRange p =
1211    case p of
1212      VarP o x         -> killRange2 VarP o x
1213      DotP o v         -> killRange2 DotP o v
1214      ConP con info ps -> killRange3 ConP con info ps
1215      LitP o l         -> killRange2 LitP o l
1216      ProjP o q        -> killRange1 (ProjP o) q
1217      IApplyP o u t x  -> killRange3 (IApplyP o) u t x
1218      DefP o q ps      -> killRange2 (DefP o) q ps
1219
1220instance KillRange Clause where
1221  killRange (Clause rl rf tel ps body t catchall exact recursive unreachable ell) =
1222    killRange10 Clause rl rf tel ps body t catchall exact recursive unreachable ell
1223
1224instance KillRange a => KillRange (Tele a) where
1225  killRange = fmap killRange
1226
1227instance KillRange a => KillRange (Blocked a) where
1228  killRange = fmap killRange
1229
1230instance KillRange a => KillRange (Abs a) where
1231  killRange = fmap killRange
1232
1233-----------------------------------------------------------------------------
1234-- * Simple pretty printing
1235-----------------------------------------------------------------------------
1236
1237instance Pretty a => Pretty (Substitution' a) where
1238  prettyPrec = pr
1239    where
1240    pr p rho = case rho of
1241      IdS              -> "idS"
1242      EmptyS err       -> "emptyS"
1243      t :# rho         -> mparens (p > 2) $ sep [ pr 2 rho <> ",", prettyPrec 3 t ]
1244      Strengthen _ rho -> mparens (p > 9) $ "strS" <+> pr 10 rho
1245      Wk n rho         -> mparens (p > 9) $ text ("wkS " ++ show n) <+> pr 10 rho
1246      Lift n rho       -> mparens (p > 9) $ text ("liftS " ++ show n) <+> pr 10 rho
1247
1248instance Pretty Term where
1249  prettyPrec p v =
1250    case v of
1251      Var x els -> text ("@" ++ show x) `pApp` els
1252      Lam ai b   ->
1253        mparens (p > 0) $
1254        sep [ "λ" <+> prettyHiding ai id (text . absName $ b) <+> "->"
1255            , nest 2 $ pretty (unAbs b) ]
1256      Lit l                -> pretty l
1257      Def q els            -> pretty q `pApp` els
1258      Con c ci vs          -> pretty (conName c) `pApp` vs
1259      Pi a (NoAbs _ b)     -> mparens (p > 0) $
1260        sep [ prettyPrec 1 (unDom a) <+> "->"
1261            , nest 2 $ pretty b ]
1262      Pi a b               -> mparens (p > 0) $
1263        sep [ pDom (domInfo a) (text (absName b) <+> ":" <+> pretty (unDom a)) <+> "->"
1264            , nest 2 $ pretty (unAbs b) ]
1265      Sort s      -> prettyPrec p s
1266      Level l     -> prettyPrec p l
1267      MetaV x els -> pretty x `pApp` els
1268      DontCare v  -> prettyPrec p v
1269      Dummy s es  -> parens (text s) `pApp` es
1270    where
1271      pApp d els = mparens (not (null els) && p > 9) $
1272                   sep [d, nest 2 $ fsep (map (prettyPrec 10) els)]
1273
1274instance Pretty t => Pretty (Abs t) where
1275  pretty (Abs   x t) = "Abs"   <+> (text x <> ".") <+> pretty t
1276  pretty (NoAbs x t) = "NoAbs" <+> (text x <> ".") <+> pretty t
1277
1278instance (Pretty t, Pretty e) => Pretty (Dom' t e) where
1279  pretty dom = pTac <+> pDom dom (pretty $ unDom dom)
1280    where
1281      pTac | Just t <- domTactic dom = "@" <> parens ("tactic" <+> pretty t)
1282           | otherwise               = empty
1283
1284pDom :: LensHiding a => a -> Doc -> Doc
1285pDom i =
1286  case getHiding i of
1287    NotHidden  -> parens
1288    Hidden     -> braces
1289    Instance{} -> braces . braces
1290
1291instance Pretty Clause where
1292  pretty Clause{clauseTel = tel, namedClausePats = ps, clauseBody = b, clauseType = t} =
1293    sep [ pretty tel <+> "|-"
1294        , nest 2 $ sep [ fsep (map (prettyPrec 10) ps) <+> "="
1295                       , nest 2 $ pBody b t ] ]
1296    where
1297      pBody Nothing _ = "(absurd)"
1298      pBody (Just b) Nothing  = pretty b
1299      pBody (Just b) (Just t) = sep [ pretty b <+> ":", nest 2 $ pretty t ]
1300
1301instance Pretty a => Pretty (Tele (Dom a)) where
1302  pretty tel = fsep [ pDom a (text x <+> ":" <+> pretty (unDom a)) | (x, a) <- telToList tel ]
1303    where
1304      telToList EmptyTel = []
1305      telToList (ExtendTel a tel) = (absName tel, a) : telToList (unAbs tel)
1306
1307prettyPrecLevelSucs :: Int -> Integer -> (Int -> Doc) -> Doc
1308prettyPrecLevelSucs p 0 d = d p
1309prettyPrecLevelSucs p n d = mparens (p > 9) $ "lsuc" <+> prettyPrecLevelSucs 10 (n - 1) d
1310
1311instance Pretty Level where
1312  prettyPrec p (Max n as) =
1313    case as of
1314      []  -> prettyN
1315      [a] | n == 0 -> prettyPrec p a
1316      _   -> mparens (p > 9) $ List.foldr1 (\a b -> "lub" <+> a <+> b) $
1317        [ prettyN | n > 0 ] ++ map (prettyPrec 10) as
1318    where
1319      prettyN = prettyPrecLevelSucs p n (const "lzero")
1320
1321instance Pretty PlusLevel where
1322  prettyPrec p (Plus n a) = prettyPrecLevelSucs p n $ \p -> prettyPrec p a
1323
1324instance Pretty Sort where
1325  prettyPrec p s =
1326    case s of
1327      Type (ClosedLevel 0) -> "Set"
1328      Type (ClosedLevel n) -> text $ "Set" ++ show n
1329      Type l -> mparens (p > 9) $ "Set" <+> prettyPrec 10 l
1330      Prop (ClosedLevel 0) -> "Prop"
1331      Prop (ClosedLevel n) -> text $ "Prop" ++ show n
1332      Prop l -> mparens (p > 9) $ "Prop" <+> prettyPrec 10 l
1333      Inf f 0 -> text $ addS f "Setω"
1334      Inf f n -> text $ addS f "Setω" ++ show n
1335      SSet l -> mparens (p > 9) $ "SSet" <+> prettyPrec 10 l
1336      SizeUniv -> "SizeUniv"
1337      LockUniv -> "LockUniv"
1338      PiSort a s1 s2 -> mparens (p > 9) $
1339        "piSort" <+> pDom (domInfo a) (text (absName s2) <+> ":" <+> pretty (unDom a))
1340                      <+> parens (sep [ text ("λ " ++ absName s2 ++ " ->")
1341                                      , nest 2 $ pretty (unAbs s2) ])
1342      FunSort a b -> mparens (p > 9) $
1343        "funSort" <+> prettyPrec 10 a <+> prettyPrec 10 b
1344      UnivSort s -> mparens (p > 9) $ "univSort" <+> prettyPrec 10 s
1345      MetaS x es -> prettyPrec p $ MetaV x es
1346      DefS d es  -> prettyPrec p $ Def d es
1347      DummyS s   -> parens $ text s
1348   where
1349     addS IsFibrant t = t
1350     addS IsStrict  t = "S" ++ t
1351
1352instance Pretty Type where
1353  prettyPrec p (El _ a) = prettyPrec p a
1354
1355instance Pretty DBPatVar where
1356  prettyPrec _ x = text $ patVarNameToString (dbPatVarName x) ++ "@" ++ show (dbPatVarIndex x)
1357
1358instance Pretty a => Pretty (Pattern' a) where
1359  prettyPrec n (VarP _o x)   = prettyPrec n x
1360  prettyPrec _ (DotP _o t)   = "." <> prettyPrec 10 t
1361  prettyPrec n (ConP c i nps)= mparens (n > 0 && not (null nps)) $
1362    (lazy <> pretty (conName c)) <+> fsep (map (prettyPrec 10) ps)
1363    where ps = map (fmap namedThing) nps
1364          lazy | conPLazy i = "~"
1365               | otherwise  = empty
1366  prettyPrec n (DefP o q nps)= mparens (n > 0 && not (null nps)) $
1367    pretty q <+> fsep (map (prettyPrec 10) ps)
1368    where ps = map (fmap namedThing) nps
1369  -- -- Version with printing record type:
1370  -- prettyPrec _ (ConP c i ps) = (if b then braces else parens) $ prTy $
1371  --   text (show $ conName c) <+> fsep (map (pretty . namedArg) ps)
1372  --   where
1373  --     b = maybe False (== ConOSystem) $ conPRecord i
1374  --     prTy d = caseMaybe (conPType i) d $ \ t -> d  <+> ":" <+> pretty t
1375  prettyPrec _ (LitP _ l)    = pretty l
1376  prettyPrec _ (ProjP _o q)  = text ("." ++ prettyShow q)
1377  prettyPrec n (IApplyP _o _ _ x) = prettyPrec n x
1378--  prettyPrec n (IApplyP _o u0 u1 x) = text "@[" <> prettyPrec 0 u0 <> text ", " <> prettyPrec 0 u1 <> text "]" <> prettyPrec n x
1379
1380-----------------------------------------------------------------------------
1381-- * NFData instances
1382-----------------------------------------------------------------------------
1383
1384-- Note: only strict in the shape of the terms.
1385
1386instance NFData Term where
1387  rnf = \case
1388    Var _ es   -> rnf es
1389    Lam _ b    -> rnf (unAbs b)
1390    Lit l      -> rnf l
1391    Def _ es   -> rnf es
1392    Con _ _ vs -> rnf vs
1393    Pi a b     -> rnf (unDom a, unAbs b)
1394    Sort s     -> rnf s
1395    Level l    -> rnf l
1396    MetaV _ es -> rnf es
1397    DontCare v -> rnf v
1398    Dummy _ es -> rnf es
1399
1400instance NFData Type where
1401  rnf (El s v) = rnf (s, v)
1402
1403instance NFData Sort where
1404  rnf = \case
1405    Type l   -> rnf l
1406    Prop l   -> rnf l
1407    Inf _ _  -> ()
1408    SSet l   -> rnf l
1409    SizeUniv -> ()
1410    LockUniv -> ()
1411    PiSort a b c -> rnf (a, b, unAbs c)
1412    FunSort a b -> rnf (a, b)
1413    UnivSort a -> rnf a
1414    MetaS _ es -> rnf es
1415    DefS _ es  -> rnf es
1416    DummyS _   -> ()
1417
1418instance NFData Level where
1419  rnf (Max n as) = rnf (n, as)
1420
1421instance NFData PlusLevel where
1422  rnf (Plus n l) = rnf (n, l)
1423
1424instance NFData e => NFData (Dom e) where
1425  rnf (Dom a b c d e) = rnf a `seq` rnf b `seq` rnf c `seq` rnf d `seq` rnf e
1426
1427instance NFData DataOrRecord
1428instance NFData ConHead
1429instance NFData a => NFData (Abs a)
1430instance NFData a => NFData (Tele a)
1431instance NFData IsFibrant
1432instance NFData Clause
1433instance NFData PatternInfo
1434instance NFData PatOrigin
1435instance NFData x => NFData (Pattern' x)
1436instance NFData DBPatVar
1437instance NFData ConPatternInfo
1438instance NFData a => NFData (Substitution' a)
1439