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