1{-# LANGUAGE CPP #-} 2{-# LANGUAGE ApplicativeDo #-} -- see exprToPattern 3 4{-| The concrete syntax is a raw representation of the program text 5 without any desugaring at all. This is what the parser produces. 6 The idea is that if we figure out how to keep the concrete syntax 7 around, it can be printed exactly as the user wrote it. 8-} 9module Agda.Syntax.Concrete 10 ( -- * Expressions 11 Expr(..) 12 , OpApp(..), fromOrdinary 13 , OpAppArgs, OpAppArgs' 14 , module Agda.Syntax.Concrete.Name 15 , AppView(..), appView, unAppView 16 , rawApp, rawAppP 17 , isSingleIdentifierP, removeParenP 18 , isPattern, isAbsurdP, isBinderP 19 , exprToPatternWithHoles 20 , returnExpr 21 -- * Bindings 22 , Binder'(..) 23 , Binder 24 , mkBinder_ 25 , mkBinder 26 , LamBinding 27 , LamBinding'(..) 28 , dropTypeAndModality 29 , TypedBinding 30 , TypedBinding'(..) 31 , RecordAssignment 32 , RecordAssignments 33 , FieldAssignment, FieldAssignment'(..), nameFieldA, exprFieldA 34 , ModuleAssignment(..) 35 , BoundName(..), mkBoundName_, mkBoundName 36 , TacticAttribute 37 , Telescope, Telescope1 38 , lamBindingsToTelescope 39 , makePi 40 , mkLam, mkLet, mkTLet 41 -- * Declarations 42 , RecordDirective(..) 43 , isRecordDirective 44 , RecordDirectives 45 , Declaration(..) 46 , ModuleApplication(..) 47 , TypeSignature 48 , TypeSignatureOrInstanceBlock 49 , ImportDirective, Using, ImportedName 50 , Renaming, RenamingDirective, HidingDirective 51 , AsName'(..), AsName 52 , OpenShortHand(..), RewriteEqn, WithExpr 53 , LHS(..), Pattern(..), LHSCore(..) 54 , observeHiding 55 , observeRelevance 56 , observeModifiers 57 , LamClause(..) 58 , RHS, RHS'(..), WhereClause, WhereClause'(..), ExprWhere(..) 59 , DoStmt(..) 60 , Pragma(..) 61 , Module(..) 62 , ThingWithFixity(..) 63 , HoleContent, HoleContent'(..) 64 , topLevelModuleName 65 , spanAllowedBeforeModule 66 ) 67 where 68 69import Prelude hiding (null) 70 71import Control.DeepSeq 72 73import Data.Data ( Data ) 74import Data.Functor.Identity 75import Data.Set ( Set ) 76import Data.Text ( Text ) 77-- import Data.Traversable ( forM ) 78 79import GHC.Generics ( Generic ) 80 81import Agda.Syntax.Position 82import Agda.Syntax.Common 83import Agda.Syntax.Fixity 84import Agda.Syntax.Literal 85 86import Agda.Syntax.Concrete.Name 87import qualified Agda.Syntax.Abstract.Name as A 88 89import Agda.TypeChecking.Positivity.Occurrence 90 91import Agda.Utils.Applicative ( forA ) 92import Agda.Utils.Either ( maybeLeft ) 93import Agda.Utils.Lens 94import Agda.Utils.List1 ( List1, pattern (:|) ) 95import qualified Agda.Utils.List1 as List1 96import Agda.Utils.List2 ( List2, pattern List2 ) 97import Agda.Utils.Null 98 99import Agda.Utils.Impossible 100 101data OpApp e 102 = SyntaxBindingLambda Range (List1 LamBinding) e 103 -- ^ An abstraction inside a special syntax declaration 104 -- (see Issue 358 why we introduce this). 105 | Ordinary e 106 deriving (Data, Functor, Foldable, Traversable, Eq) 107 108fromOrdinary :: e -> OpApp e -> e 109fromOrdinary d (Ordinary e) = e 110fromOrdinary d _ = d 111 112data FieldAssignment' a = FieldAssignment { _nameFieldA :: Name, _exprFieldA :: a } 113 deriving (Data, Functor, Foldable, Traversable, Show, Eq) 114 115type FieldAssignment = FieldAssignment' Expr 116 117data ModuleAssignment = ModuleAssignment 118 { _qnameModA :: QName 119 , _exprModA :: [Expr] 120 , _importDirModA :: ImportDirective 121 } 122 deriving (Data, Eq) 123 124type RecordAssignment = Either FieldAssignment ModuleAssignment 125type RecordAssignments = [RecordAssignment] 126 127nameFieldA :: Lens' Name (FieldAssignment' a) 128nameFieldA f r = f (_nameFieldA r) <&> \x -> r { _nameFieldA = x } 129 130exprFieldA :: Lens' a (FieldAssignment' a) 131exprFieldA f r = f (_exprFieldA r) <&> \x -> r { _exprFieldA = x } 132 133-- UNUSED Liang-Ting Chen 2019-07-16 134--qnameModA :: Lens' QName ModuleAssignment 135--qnameModA f r = f (_qnameModA r) <&> \x -> r { _qnameModA = x } 136-- 137--exprModA :: Lens' [Expr] ModuleAssignment 138--exprModA f r = f (_exprModA r) <&> \x -> r { _exprModA = x } 139-- 140--importDirModA :: Lens' ImportDirective ModuleAssignment 141--importDirModA f r = f (_importDirModA r) <&> \x -> r { _importDirModA = x } 142 143-- | Concrete expressions. Should represent exactly what the user wrote. 144data Expr 145 = Ident QName -- ^ ex: @x@ 146 | Lit Range Literal -- ^ ex: @1@ or @\"foo\"@ 147 | QuestionMark Range (Maybe Nat) -- ^ ex: @?@ or @{! ... !}@ 148 | Underscore Range (Maybe String) -- ^ ex: @_@ or @_A_5@ 149 | RawApp Range (List2 Expr) -- ^ before parsing operators 150 | App Range Expr (NamedArg Expr) -- ^ ex: @e e@, @e {e}@, or @e {x = e}@ 151 | OpApp Range QName (Set A.Name) OpAppArgs -- ^ ex: @e + e@ 152 -- The 'QName' is possibly ambiguous, 153 -- but it must correspond to one of the names in the set. 154 | WithApp Range Expr [Expr] -- ^ ex: @e | e1 | .. | en@ 155 | HiddenArg Range (Named_ Expr) -- ^ ex: @{e}@ or @{x=e}@ 156 | InstanceArg Range (Named_ Expr) -- ^ ex: @{{e}}@ or @{{x=e}}@ 157 | Lam Range (List1 LamBinding) Expr -- ^ ex: @\\x {y} -> e@ or @\\(x:A){y:B} -> e@ 158 | AbsurdLam Range Hiding -- ^ ex: @\\ ()@ 159 | ExtendedLam Range Erased 160 (List1 LamClause) -- ^ ex: @\\ { p11 .. p1a -> e1 ; .. ; pn1 .. pnz -> en }@ 161 | Fun Range (Arg Expr) Expr -- ^ ex: @e -> e@ or @.e -> e@ (NYI: @{e} -> e@) 162 | Pi Telescope1 Expr -- ^ ex: @(xs:e) -> e@ or @{xs:e} -> e@ 163 | Rec Range RecordAssignments -- ^ ex: @record {x = a; y = b}@, or @record { x = a; M1; M2 }@ 164 | RecUpdate Range Expr [FieldAssignment] -- ^ ex: @record e {x = a; y = b}@ 165 | Let Range (List1 Declaration) (Maybe Expr) -- ^ ex: @let Ds in e@, missing body when parsing do-notation let 166 | Paren Range Expr -- ^ ex: @(e)@ 167 | IdiomBrackets Range [Expr] -- ^ ex: @(| e1 | e2 | .. | en |)@ or @(|)@ 168 | DoBlock Range (List1 DoStmt) -- ^ ex: @do x <- m1; m2@ 169 | Absurd Range -- ^ ex: @()@ or @{}@, only in patterns 170 | As Range Name Expr -- ^ ex: @x\@p@, only in patterns 171 | Dot Range Expr -- ^ ex: @.p@, only in patterns 172 | DoubleDot Range Expr -- ^ ex: @..A@, used for parsing @..A -> B@ 173 | ETel Telescope -- ^ only used for printing telescopes 174 | Quote Range -- ^ ex: @quote@, should be applied to a name 175 | QuoteTerm Range -- ^ ex: @quoteTerm@, should be applied to a term 176 | Tactic Range Expr -- ^ ex: @\@(tactic t)@, used to declare tactic arguments 177 | Unquote Range -- ^ ex: @unquote@, should be applied to a term of type @Term@ 178 | DontCare Expr -- ^ to print irrelevant things 179 | Equal Range Expr Expr -- ^ ex: @a = b@, used internally in the parser 180 | Ellipsis Range -- ^ @...@, used internally to parse patterns. 181 | Generalized Expr 182 deriving (Data, Eq) 183 184type OpAppArgs = OpAppArgs' Expr 185type OpAppArgs' e = [NamedArg (MaybePlaceholder (OpApp e))] 186 187-- | Concrete patterns. No literals in patterns at the moment. 188data Pattern 189 = IdentP QName -- ^ @c@ or @x@ 190 | QuoteP Range -- ^ @quote@ 191 | AppP Pattern (NamedArg Pattern) -- ^ @p p'@ or @p {x = p'}@ 192 | RawAppP Range (List2 Pattern) -- ^ @p1..pn@ before parsing operators 193 | OpAppP Range QName (Set A.Name) 194 [NamedArg Pattern] -- ^ eg: @p => p'@ for operator @_=>_@ 195 -- The 'QName' is possibly 196 -- ambiguous, but it must 197 -- correspond to one of 198 -- the names in the set. 199 | HiddenP Range (Named_ Pattern) -- ^ @{p}@ or @{x = p}@ 200 | InstanceP Range (Named_ Pattern) -- ^ @{{p}}@ or @{{x = p}}@ 201 | ParenP Range Pattern -- ^ @(p)@ 202 | WildP Range -- ^ @_@ 203 | AbsurdP Range -- ^ @()@ 204 | AsP Range Name Pattern -- ^ @x\@p@ unused 205 | DotP Range Expr -- ^ @.e@ 206 | LitP Range Literal -- ^ @0@, @1@, etc. 207 | RecP Range [FieldAssignment' Pattern] -- ^ @record {x = p; y = q}@ 208 | EqualP Range [(Expr,Expr)] -- ^ @i = i1@ i.e. cubical face lattice generator 209 | EllipsisP Range (Maybe Pattern) -- ^ @...@, only as left-most pattern. 210 -- Second arg is @Nothing@ before expansion, and 211 -- @Just p@ after expanding ellipsis to @p@. 212 | WithP Range Pattern -- ^ @| p@, for with-patterns. 213 deriving (Data, Eq) 214 215data DoStmt 216 = DoBind Range Pattern Expr [LamClause] -- ^ @p ← e where cs@ 217 | DoThen Expr 218 | DoLet Range (List1 Declaration) 219 deriving (Data, Eq) 220 221-- | A Binder @x\@p@, the pattern is optional 222data Binder' a = Binder 223 { binderPattern :: Maybe Pattern 224 , binderName :: a 225 } deriving (Data, Eq, Functor, Foldable, Traversable) 226 227type Binder = Binder' BoundName 228 229mkBinder_ :: Name -> Binder 230mkBinder_ = mkBinder . mkBoundName_ 231 232mkBinder :: a -> Binder' a 233mkBinder = Binder Nothing 234 235-- | A lambda binding is either domain free or typed. 236 237type LamBinding = LamBinding' TypedBinding 238data LamBinding' a 239 = DomainFree (NamedArg Binder) 240 -- ^ . @x@ or @{x}@ or @.x@ or @.{x}@ or @{.x}@ or @x\@p@ or @(p)@ 241 | DomainFull a 242 -- ^ . @(xs : e)@ or @{xs : e}@ 243 deriving (Data, Functor, Foldable, Traversable, Eq) 244 245-- | Drop type annotations and lets from bindings. 246dropTypeAndModality :: LamBinding -> [LamBinding] 247dropTypeAndModality (DomainFull (TBind _ xs _)) = 248 map (DomainFree . setModality defaultModality) $ List1.toList xs 249dropTypeAndModality (DomainFull TLet{}) = [] 250dropTypeAndModality (DomainFree x) = [DomainFree $ setModality defaultModality x] 251 252data BoundName = BName 253 { boundName :: Name 254 , bnameFixity :: Fixity' 255 , bnameTactic :: TacticAttribute -- From @tactic attribute 256 } 257 deriving (Data, Eq) 258 259type TacticAttribute = Maybe Expr 260 261mkBoundName_ :: Name -> BoundName 262mkBoundName_ x = mkBoundName x noFixity' 263 264mkBoundName :: Name -> Fixity' -> BoundName 265mkBoundName x f = BName x f Nothing 266 267-- | A typed binding. 268 269type TypedBinding = TypedBinding' Expr 270 271data TypedBinding' e 272 = TBind Range (List1 (NamedArg Binder)) e 273 -- ^ Binding @(x1\@p1 ... xn\@pn : A)@. 274 | TLet Range (List1 Declaration) 275 -- ^ Let binding @(let Ds)@ or @(open M args)@. 276 deriving (Data, Functor, Foldable, Traversable, Eq) 277 278-- | A telescope is a sequence of typed bindings. Bound variables are in scope 279-- in later types. 280type Telescope1 = List1 TypedBinding 281type Telescope = [TypedBinding] 282 283-- | We can try to get a @Telescope@ from a @[LamBinding]@. 284-- If we have a type annotation already, we're happy. 285-- Otherwise we manufacture a binder with an underscore for the type. 286lamBindingsToTelescope :: Range -> [LamBinding] -> Telescope 287lamBindingsToTelescope r = fmap $ \case 288 DomainFull ty -> ty 289 DomainFree nm -> TBind r (List1.singleton nm) $ Underscore r Nothing 290 291-- | Smart constructor for @Pi@: check whether the @Telescope@ is empty 292 293makePi :: Telescope -> Expr -> Expr 294makePi [] = id 295makePi (b:bs) = Pi (b :| bs) 296 297-- | Smart constructor for @Lam@: check for non-zero bindings. 298 299mkLam :: Range -> [LamBinding] -> Expr -> Expr 300mkLam r [] e = e 301mkLam r (x:xs) e = Lam r (x :| xs) e 302 303-- | Smart constructor for @Let@: check for non-zero let bindings. 304 305mkLet :: Range -> [Declaration] -> Expr -> Expr 306mkLet r [] e = e 307mkLet r (d:ds) e = Let r (d :| ds) (Just e) 308 309-- | Smart constructor for @TLet@: check for non-zero let bindings. 310 311mkTLet :: Range -> [Declaration] -> Maybe (TypedBinding' e) 312mkTLet r [] = Nothing 313mkTLet r (d:ds) = Just $ TLet r (d :| ds) 314 315{-| Left hand sides can be written in infix style. For example: 316 317 > n + suc m = suc (n + m) 318 > (f ∘ g) x = f (g x) 319 320 We use fixity information to see which name is actually defined. 321-} 322data LHS = LHS -- ^ Original pattern (including with-patterns), rewrite equations and with-expressions. 323 { lhsOriginalPattern :: Pattern 324 -- ^ e.g. @f ps | wps@ 325 , lhsRewriteEqn :: [RewriteEqn] 326 -- ^ @(rewrite e | with p <- e in eq)@ (many) 327 , lhsWithExpr :: [WithExpr] 328 -- ^ @with e1 in eq | {e2} | ...@ (many) 329 } 330 deriving (Data, Eq) 331 332type RewriteEqn = RewriteEqn' () Name Pattern Expr 333type WithExpr = Named Name (Arg Expr) 334 335-- | Processed (operator-parsed) intermediate form of the core @f ps@ of 'LHS'. 336-- Corresponds to 'lhsOriginalPattern'. 337data LHSCore 338 = LHSHead { lhsDefName :: QName -- ^ @f@ 339 , lhsPats :: [NamedArg Pattern] -- ^ @ps@ 340 } 341 | LHSProj { lhsDestructor :: QName -- ^ Record projection. 342 , lhsPatsLeft :: [NamedArg Pattern] -- ^ Patterns for record indices (currently none). 343 , lhsFocus :: NamedArg LHSCore -- ^ Main argument. 344 , lhsPats :: [NamedArg Pattern] -- ^ More application patterns. 345 } 346 | LHSWith { lhsHead :: LHSCore 347 , lhsWithPatterns :: [Pattern] -- ^ Non-empty; at least one @(| p)@. 348 , lhsPats :: [NamedArg Pattern] -- ^ More application patterns. 349 } 350 | LHSEllipsis 351 { lhsEllipsisRange :: Range 352 , lhsEllipsisPat :: LHSCore -- ^ Pattern that was expanded from an ellipsis @...@. 353 } 354 deriving (Data, Eq) 355 356type RHS = RHS' Expr 357data RHS' e 358 = AbsurdRHS -- ^ No right hand side because of absurd match. 359 | RHS e 360 deriving (Data, Functor, Foldable, Traversable, Eq) 361 362-- | @where@ block following a clause. 363type WhereClause = WhereClause' [Declaration] 364 365-- The generalization @WhereClause'@ is for the sake of Concrete.Generic. 366data WhereClause' decls 367 = NoWhere 368 -- ^ No @where@ clauses. 369 | AnyWhere Range decls 370 -- ^ Ordinary @where@. 'Range' of the @where@ keyword. 371 -- List of declarations can be empty. 372 | SomeWhere Range Name Access decls 373 -- ^ Named where: @module M where ds@. 374 -- 'Range' of the keywords @module@ and @where@. 375 -- The 'Access' flag applies to the 'Name' (not the module contents!) 376 -- and is propagated from the parent function. 377 -- List of declarations can be empty. 378 deriving (Data, Eq, Functor, Foldable, Traversable) 379 380data LamClause = LamClause 381 { lamLHS :: [Pattern] -- ^ Possibly empty sequence. 382 , lamRHS :: RHS 383 , lamCatchAll :: Bool 384 } 385 deriving (Data, Eq) 386 387-- | An expression followed by a where clause. 388-- Currently only used to give better a better error message in interaction. 389data ExprWhere = ExprWhere Expr WhereClause 390 391-- | The things you are allowed to say when you shuffle names between name 392-- spaces (i.e. in @import@, @namespace@, or @open@ declarations). 393type ImportDirective = ImportDirective' Name Name 394type Using = Using' Name Name 395type Renaming = Renaming' Name Name 396type RenamingDirective = RenamingDirective' Name Name 397type HidingDirective = HidingDirective' Name Name -- 'Hiding' is already taken 398 399-- | An imported name can be a module or a defined name. 400type ImportedName = ImportedName' Name Name 401 402-- | The content of the @as@-clause of the import statement. 403data AsName' a = AsName 404 { asName :: a 405 -- ^ The \"as\" name. 406 , asRange :: Range 407 -- ^ The range of the \"as\" keyword. Retained for highlighting purposes. 408 } 409 deriving (Data, Show, Functor, Foldable, Traversable, Eq) 410 411-- | From the parser, we get an expression for the @as@-'Name', which 412-- we have to parse into a 'Name'. 413type AsName = AsName' (Either Expr Name) 414 415{-------------------------------------------------------------------------- 416 Declarations 417 --------------------------------------------------------------------------} 418 419-- | Just type signatures. 420type TypeSignature = Declaration 421 422-- | Just field signatures 423type FieldSignature = Declaration 424 425-- | Just type signatures or instance blocks. 426type TypeSignatureOrInstanceBlock = Declaration 427 428-- | Isolated record directives parsed as Declarations 429data RecordDirective 430 = Induction (Ranged Induction) 431 -- ^ Range of keyword @[co]inductive@. 432 | Constructor Name IsInstance 433 | Eta (Ranged HasEta0) 434 -- ^ Range of @[no-]eta-equality@ keyword. 435 | PatternOrCopattern Range 436 -- ^ If declaration @pattern@ is present, give its range. 437 deriving (Data,Eq,Show) 438 439type RecordDirectives = RecordDirectives' (Name, IsInstance) 440 441{-| The representation type of a declaration. The comments indicate 442 which type in the intended family the constructor targets. 443-} 444 445data Declaration 446 = TypeSig ArgInfo TacticAttribute Name Expr 447 | FieldSig IsInstance TacticAttribute Name (Arg Expr) 448 -- ^ Axioms and functions can be irrelevant. (Hiding should be NotHidden) 449 | Generalize Range [TypeSignature] -- ^ Variables to be generalized, can be hidden and/or irrelevant. 450 | Field Range [FieldSignature] 451 | FunClause LHS RHS WhereClause Bool 452 | DataSig Range Name [LamBinding] Expr -- ^ lone data signature in mutual block 453 | Data Range Name [LamBinding] Expr [TypeSignatureOrInstanceBlock] 454 | DataDef Range Name [LamBinding] [TypeSignatureOrInstanceBlock] 455 | RecordSig Range Name [LamBinding] Expr -- ^ lone record signature in mutual block 456 | RecordDef Range Name RecordDirectives [LamBinding] [Declaration] 457 | Record Range Name RecordDirectives [LamBinding] Expr [Declaration] 458 | RecordDirective RecordDirective -- ^ Should not survive beyond the parser 459 | Infix Fixity (List1 Name) 460 | Syntax Name Notation -- ^ notation declaration for a name 461 | PatternSyn Range Name [Arg Name] Pattern 462 | Mutual Range [Declaration] -- @Range@ of the whole @mutual@ block. 463 | InterleavedMutual Range [Declaration] 464 | Abstract Range [Declaration] 465 | Private Range Origin [Declaration] 466 -- ^ In "Agda.Syntax.Concrete.Definitions" we generate private blocks 467 -- temporarily, which should be treated different that user-declared 468 -- private blocks. Thus the 'Origin'. 469 | InstanceB Range [Declaration] 470 -- ^ The 'Range' here (exceptionally) only refers to the range of the 471 -- @instance@ keyword. The range of the whole block @InstanceB r ds@ 472 -- is @fuseRange r ds@. 473 | LoneConstructor Range [Declaration] 474 | Macro Range [Declaration] 475 | Postulate Range [TypeSignatureOrInstanceBlock] 476 | Primitive Range [TypeSignature] 477 | Open Range QName ImportDirective 478 | Import Range QName (Maybe AsName) !OpenShortHand ImportDirective 479 | ModuleMacro Range Name ModuleApplication !OpenShortHand ImportDirective 480 | Module Range QName Telescope [Declaration] 481 | UnquoteDecl Range [Name] Expr 482 | UnquoteDef Range [Name] Expr 483 | Pragma Pragma 484 deriving (Data, Eq) 485 486-- | Extract a record directive 487isRecordDirective :: Declaration -> Maybe RecordDirective 488isRecordDirective (RecordDirective r) = Just r 489isRecordDirective (InstanceB r [RecordDirective (Constructor n p)]) = Just (Constructor n (InstanceDef r)) 490isRecordDirective _ = Nothing 491 492data ModuleApplication 493 = SectionApp Range Telescope Expr 494 -- ^ @tel. M args@ 495 | RecordModuleInstance Range QName 496 -- ^ @M {{...}}@ 497 deriving (Data, Eq) 498 499data OpenShortHand = DoOpen | DontOpen 500 deriving (Data, Eq, Show, Generic) 501 502-- Pragmas ---------------------------------------------------------------- 503 504data Pragma 505 = OptionsPragma Range [String] 506 | BuiltinPragma Range RString QName 507 | RewritePragma Range Range [QName] -- ^ Second Range is for REWRITE keyword. 508 | ForeignPragma Range RString String -- ^ first string is backend name 509 | CompilePragma Range RString QName String -- ^ first string is backend name 510 | StaticPragma Range QName 511 | InlinePragma Range Bool QName -- ^ INLINE or NOINLINE 512 513 | ImpossiblePragma Range [String] 514 -- ^ Throws an internal error in the scope checker. 515 -- The 'String's are words to be displayed with the error. 516 | EtaPragma Range QName 517 -- ^ For coinductive records, use pragma instead of regular 518 -- @eta-equality@ definition (as it is might make Agda loop). 519 | WarningOnUsage Range QName Text 520 -- ^ Applies to the named function 521 | WarningOnImport Range Text 522 -- ^ Applies to the current module 523 | InjectivePragma Range QName 524 -- ^ Mark a definition as injective for the pattern matching unifier. 525 | DisplayPragma Range Pattern Expr 526 -- ^ Display lhs as rhs (modifies the printer). 527 528 -- Attached (more or less) pragmas handled in the nicifier (Concrete.Definitions): 529 | CatchallPragma Range 530 -- ^ Applies to the following function clause. 531 | TerminationCheckPragma Range (TerminationCheck Name) 532 -- ^ Applies to the following function (and all that are mutually recursive with it) 533 -- or to the functions in the following mutual block. 534 | NoCoverageCheckPragma Range 535 -- ^ Applies to the following function (and all that are mutually recursive with it) 536 -- or to the functions in the following mutual block. 537 | NoPositivityCheckPragma Range 538 -- ^ Applies to the following data/record type or mutual block. 539 | PolarityPragma Range Name [Occurrence] 540 | NoUniverseCheckPragma Range 541 -- ^ Applies to the following data/record type. 542 deriving (Data, Eq) 543 544--------------------------------------------------------------------------- 545 546-- | Modules: Top-level pragmas plus other top-level declarations. 547 548data Module = Mod 549 { modPragmas :: [Pragma] 550 , modDecls :: [Declaration] 551 } 552 553-- | Computes the top-level module name. 554-- 555-- Precondition: The 'Module' has to be well-formed. 556-- This means that there are only allowed declarations before the 557-- first module declaration, typically import declarations. 558-- See 'spanAllowedBeforeModule'. 559 560topLevelModuleName :: Module -> TopLevelModuleName 561topLevelModuleName (Mod _ []) = __IMPOSSIBLE__ 562topLevelModuleName (Mod _ ds) = case spanAllowedBeforeModule ds of 563 (_, Module _ n _ _ : _) -> toTopLevelModuleName n 564 _ -> __IMPOSSIBLE__ 565 566-- | Splits off allowed (= import) declarations before the first 567-- non-allowed declaration. 568-- After successful parsing, the first non-allowed declaration 569-- should be a module declaration. 570spanAllowedBeforeModule :: [Declaration] -> ([Declaration], [Declaration]) 571spanAllowedBeforeModule = span isAllowedBeforeModule 572 where 573 isAllowedBeforeModule (Pragma OptionsPragma{}) = True 574 isAllowedBeforeModule (Pragma BuiltinPragma{}) = True 575 isAllowedBeforeModule (Private _ _ ds) = all isAllowedBeforeModule ds 576 isAllowedBeforeModule Import{} = True 577 isAllowedBeforeModule ModuleMacro{} = True 578 isAllowedBeforeModule Open{} = True 579 isAllowedBeforeModule _ = False 580 581{-------------------------------------------------------------------------- 582 Things we parse but are not part of the Agda file syntax 583 --------------------------------------------------------------------------} 584 585-- | Extended content of an interaction hole. 586data HoleContent' qn nm p e 587 = HoleContentExpr e -- ^ @e@ 588 | HoleContentRewrite [RewriteEqn' qn nm p e] -- ^ @(rewrite | invert) e0 | ... | en@ 589 deriving (Functor, Foldable, Traversable) 590 591type HoleContent = HoleContent' () Name Pattern Expr 592 593--------------------------------------------------------------------------- 594-- * Smart constructors 595--------------------------------------------------------------------------- 596 597rawApp :: List1 Expr -> Expr 598rawApp es@(e1 :| e2 : rest) = RawApp (getRange es) $ List2 e1 e2 rest 599rawApp (e :| []) = e 600 601rawAppP :: List1 Pattern -> Pattern 602rawAppP ps@(p1 :| p2 : rest) = RawAppP (getRange ps) $ List2 p1 p2 rest 603rawAppP (p :| []) = p 604 605{-------------------------------------------------------------------------- 606 Views 607 --------------------------------------------------------------------------} 608 609-- | The 'Expr' is not an application. 610data AppView = AppView Expr [NamedArg Expr] 611 612appView :: Expr -> AppView 613appView = \case 614 App r e1 e2 -> vApp (appView e1) e2 615 RawApp _ (List2 e1 e2 es) 616 -> AppView e1 $ map arg (e2:es) 617 e -> AppView e [] 618 where 619 vApp (AppView e es) arg = AppView e (es ++ [arg]) 620 621 arg (HiddenArg _ e) = hide $ defaultArg e 622 arg (InstanceArg _ e) = makeInstance $ defaultArg e 623 arg e = defaultArg (unnamed e) 624 625unAppView :: AppView -> Expr 626unAppView (AppView e nargs) = rawApp (e :| map unNamedArg nargs) 627 628 where 629 unNamedArg narg = ($ unArg narg) $ case getHiding narg of 630 Hidden -> HiddenArg (getRange narg) 631 NotHidden -> namedThing 632 Instance{} -> InstanceArg (getRange narg) 633 634isSingleIdentifierP :: Pattern -> Maybe Name 635isSingleIdentifierP = \case 636 IdentP (QName x) -> Just x 637 WildP r -> Just $ noName r 638 ParenP _ p -> isSingleIdentifierP p 639 _ -> Nothing 640 641removeParenP :: Pattern -> Pattern 642removeParenP = \case 643 ParenP _ p -> removeParenP p 644 p -> p 645 646-- | Observe the hiding status of an expression 647observeHiding :: Expr -> WithHiding Expr 648observeHiding = \case 649 HiddenArg _ (Named Nothing e) -> WithHiding Hidden e 650 InstanceArg _ (Named Nothing e) -> WithHiding (Instance NoOverlap) e 651 e -> WithHiding NotHidden e 652 653-- | Observe the relevance status of an expression 654observeRelevance :: Expr -> (Relevance, Expr) 655observeRelevance = \case 656 Dot _ e -> (Irrelevant, e) 657 DoubleDot _ e -> (NonStrict, e) 658 e -> (Relevant, e) 659 660-- | Observe various modifiers applied to an expression 661observeModifiers :: Expr -> Arg Expr 662observeModifiers e = 663 let (rel, WithHiding hid e') = fmap observeHiding (observeRelevance e) in 664 setRelevance rel $ setHiding hid $ defaultArg e' 665 666returnExpr :: Expr -> Maybe Expr 667returnExpr (Pi _ e) = returnExpr e 668returnExpr (Fun _ _ e) = returnExpr e 669returnExpr (Let _ _ e) = returnExpr =<< e 670returnExpr (Paren _ e) = returnExpr e 671returnExpr (Generalized e) = returnExpr e 672returnExpr e = pure e 673 674-- | Turn an expression into a pattern. Fails if the expression is not a 675-- valid pattern. 676 677isPattern :: Expr -> Maybe Pattern 678isPattern = exprToPattern (const Nothing) 679 680-- | Turn an expression into a pattern, turning non-pattern subexpressions into 'WildP'. 681 682exprToPatternWithHoles :: Expr -> Pattern 683exprToPatternWithHoles = runIdentity . exprToPattern (Identity . WildP . getRange) 684 685-- | Generic expression to pattern conversion. 686 687exprToPattern :: Applicative m 688 => (Expr -> m Pattern) -- ^ Default result for non-pattern things. 689 -> Expr -- ^ The expression to translate. 690 -> m Pattern -- ^ The translated pattern (maybe). 691exprToPattern fallback = loop 692 where 693 loop = \case 694 Ident x -> pure $ IdentP x 695 App _ e1 e2 -> AppP <$> loop e1 <*> traverse (traverse loop) e2 696 Paren r e -> ParenP r <$> loop e 697 Underscore r _ -> pure $ WildP r 698 Absurd r -> pure $ AbsurdP r 699 As r x e -> pushUnderBracesP r (AsP r x) <$> loop e 700 Dot r e -> pure $ pushUnderBracesE r (DotP r) e 701 -- Wen, 2020-08-27: We disallow Float patterns, since equality for floating 702 -- point numbers is not stable across architectures and with different 703 -- compiler flags. 704 e@(Lit _ LitFloat{}) -> fallback e 705 Lit r l -> pure $ LitP r l 706 HiddenArg r e -> HiddenP r <$> traverse loop e 707 InstanceArg r e -> InstanceP r <$> traverse loop e 708 RawApp r es -> RawAppP r <$> traverse loop es 709 Quote r -> pure $ QuoteP r 710 Equal r e1 e2 -> pure $ EqualP r [(e1, e2)] 711 Ellipsis r -> pure $ EllipsisP r Nothing 712 e@(Rec r es) 713 -- We cannot translate record expressions with module parts. 714 | Just fs <- mapM maybeLeft es -> RecP r <$> traverse (traverse loop) fs 715 | otherwise -> fallback e 716 -- WithApp has already lost the range information of the bars '|' 717 WithApp r e es -> do -- ApplicativeDo 718 p <- loop e 719 ps <- forA es $ \ e -> do -- ApplicativeDo 720 p <- loop e 721 pure $ defaultNamedArg $ WithP (getRange e) p -- TODO #2822: Range! 722 pure $ foldl AppP p ps 723 e -> fallback e 724 725 pushUnderBracesP :: Range -> (Pattern -> Pattern) -> (Pattern -> Pattern) 726 pushUnderBracesP r f = \case 727 HiddenP _ p -> HiddenP r $ fmap f p 728 InstanceP _ p -> InstanceP r $ fmap f p 729 p -> f p 730 731 pushUnderBracesE :: Range -> (Expr -> Pattern) -> (Expr -> Pattern) 732 pushUnderBracesE r f = \case 733 HiddenArg _ p -> HiddenP r $ fmap f p 734 InstanceArg _ p -> InstanceP r $ fmap f p 735 p -> f p 736 737isAbsurdP :: Pattern -> Maybe (Range, Hiding) 738isAbsurdP = \case 739 AbsurdP r -> pure (r, NotHidden) 740 AsP _ _ p -> isAbsurdP p 741 ParenP _ p -> isAbsurdP p 742 HiddenP _ np -> (Hidden <$) <$> isAbsurdP (namedThing np) 743 InstanceP _ np -> (Instance YesOverlap <$) <$> isAbsurdP (namedThing np) 744 _ -> Nothing 745 746isBinderP :: Pattern -> Maybe Binder 747isBinderP = \case 748 IdentP qn -> mkBinder_ <$> isUnqualified qn 749 WildP r -> pure $ mkBinder_ $ setRange r simpleHole 750 AsP r n p -> pure $ Binder (Just p) $ mkBoundName_ n 751 ParenP r p -> pure $ Binder (Just p) $ mkBoundName_ $ setRange r simpleHole 752 _ -> Nothing 753 754{-------------------------------------------------------------------------- 755 Instances 756 --------------------------------------------------------------------------} 757 758-- Null 759------------------------------------------------------------------------ 760 761-- | A 'WhereClause' is 'null' when the @where@ keyword is absent. 762-- An empty list of declarations does not count as 'null' here. 763 764instance Null (WhereClause' a) where 765 empty = NoWhere 766 null NoWhere = True 767 null AnyWhere{} = False 768 null SomeWhere{} = False 769 770-- Lenses 771------------------------------------------------------------------------ 772 773instance LensHiding LamBinding where 774 getHiding (DomainFree x) = getHiding x 775 getHiding (DomainFull a) = getHiding a 776 mapHiding f (DomainFree x) = DomainFree $ mapHiding f x 777 mapHiding f (DomainFull a) = DomainFull $ mapHiding f a 778 779instance LensHiding TypedBinding where 780 getHiding (TBind _ (x :| _) _) = getHiding x -- Slightly dubious 781 getHiding TLet{} = mempty 782 mapHiding f (TBind r xs e) = TBind r (fmap (mapHiding f) xs) e 783 mapHiding f b@TLet{} = b 784 785instance LensRelevance TypedBinding where 786 getRelevance (TBind _ (x :|_) _) = getRelevance x -- Slightly dubious 787 getRelevance TLet{} = unitRelevance 788 mapRelevance f (TBind r xs e) = TBind r (fmap (mapRelevance f) xs) e 789 mapRelevance f b@TLet{} = b 790 791-- HasRange instances 792------------------------------------------------------------------------ 793 794instance HasRange e => HasRange (OpApp e) where 795 getRange = \case 796 Ordinary e -> getRange e 797 SyntaxBindingLambda r _ _ -> r 798 799instance HasRange Expr where 800 getRange = \case 801 Ident x -> getRange x 802 Lit r _ -> r 803 QuestionMark r _ -> r 804 Underscore r _ -> r 805 App r _ _ -> r 806 RawApp r _ -> r 807 OpApp r _ _ _ -> r 808 WithApp r _ _ -> r 809 Lam r _ _ -> r 810 AbsurdLam r _ -> r 811 ExtendedLam r _ _ -> r 812 Fun r _ _ -> r 813 Pi b e -> fuseRange b e 814 Let r _ _ -> r 815 Paren r _ -> r 816 IdiomBrackets r _ -> r 817 DoBlock r _ -> r 818 As r _ _ -> r 819 Dot r _ -> r 820 DoubleDot r _ -> r 821 Absurd r -> r 822 HiddenArg r _ -> r 823 InstanceArg r _ -> r 824 Rec r _ -> r 825 RecUpdate r _ _ -> r 826 ETel tel -> getRange tel 827 Quote r -> r 828 QuoteTerm r -> r 829 Unquote r -> r 830 Tactic r _ -> r 831 DontCare{} -> noRange 832 Equal r _ _ -> r 833 Ellipsis r -> r 834 Generalized e -> getRange e 835 836-- instance HasRange Telescope where 837-- getRange (TeleBind bs) = getRange bs 838-- getRange (TeleFun x y) = fuseRange x y 839 840instance HasRange Binder where 841 getRange (Binder a b) = fuseRange a b 842 843instance HasRange TypedBinding where 844 getRange (TBind r _ _) = r 845 getRange (TLet r _) = r 846 847instance HasRange LamBinding where 848 getRange (DomainFree x) = getRange x 849 getRange (DomainFull b) = getRange b 850 851instance HasRange BoundName where 852 getRange = getRange . boundName 853 854instance HasRange WhereClause where 855 getRange NoWhere = noRange 856 getRange (AnyWhere r ds) = getRange (r, ds) 857 getRange (SomeWhere r x _ ds) = getRange (r, x, ds) 858 859instance HasRange ModuleApplication where 860 getRange (SectionApp r _ _) = r 861 getRange (RecordModuleInstance r _) = r 862 863instance HasRange a => HasRange (FieldAssignment' a) where 864 getRange (FieldAssignment a b) = fuseRange a b 865 866instance HasRange ModuleAssignment where 867 getRange (ModuleAssignment a b c) = fuseRange a b `fuseRange` c 868 869instance HasRange RecordDirective where 870 getRange (Induction a) = getRange a 871 getRange (Eta a ) = getRange a 872 getRange (Constructor a b) = getRange (a, b) 873 getRange (PatternOrCopattern r) = r 874 875instance HasRange Declaration where 876 getRange (TypeSig _ _ x t) = fuseRange x t 877 getRange (FieldSig _ _ x t) = fuseRange x t 878 getRange (Field r _) = r 879 getRange (FunClause lhs rhs wh _) = fuseRange lhs rhs `fuseRange` wh 880 getRange (DataSig r _ _ _) = r 881 getRange (Data r _ _ _ _) = r 882 getRange (DataDef r _ _ _) = r 883 getRange (RecordSig r _ _ _) = r 884 getRange (RecordDef r _ _ _ _) = r 885 getRange (Record r _ _ _ _ _) = r 886 getRange (RecordDirective r) = getRange r 887 getRange (Mutual r _) = r 888 getRange (InterleavedMutual r _) = r 889 getRange (LoneConstructor r _) = r 890 getRange (Abstract r _) = r 891 getRange (Generalize r _) = r 892 getRange (Open r _ _) = r 893 getRange (ModuleMacro r _ _ _ _) = r 894 getRange (Import r _ _ _ _) = r 895 getRange (InstanceB r _) = r 896 getRange (Macro r _) = r 897 getRange (Private r _ _) = r 898 getRange (Postulate r _) = r 899 getRange (Primitive r _) = r 900 getRange (Module r _ _ _) = r 901 getRange (Infix f _) = getRange f 902 getRange (Syntax n _) = getRange n 903 getRange (PatternSyn r _ _ _) = r 904 getRange (UnquoteDecl r _ _) = r 905 getRange (UnquoteDef r _ _) = r 906 getRange (Pragma p) = getRange p 907 908instance HasRange LHS where 909 getRange (LHS p eqns ws) = p `fuseRange` eqns `fuseRange` ws 910 911instance HasRange LHSCore where 912 getRange (LHSHead f ps) = fuseRange f ps 913 getRange (LHSProj d ps1 lhscore ps2) = d `fuseRange` ps1 `fuseRange` lhscore `fuseRange` ps2 914 getRange (LHSWith f wps ps) = f `fuseRange` wps `fuseRange` ps 915 getRange (LHSEllipsis r p) = r 916 917instance HasRange RHS where 918 getRange AbsurdRHS = noRange 919 getRange (RHS e) = getRange e 920 921instance HasRange LamClause where 922 getRange (LamClause lhs rhs _) = getRange (lhs, rhs) 923 924instance HasRange DoStmt where 925 getRange (DoBind r _ _ _) = r 926 getRange (DoThen e) = getRange e 927 getRange (DoLet r _) = r 928 929instance HasRange Pragma where 930 getRange (OptionsPragma r _) = r 931 getRange (BuiltinPragma r _ _) = r 932 getRange (RewritePragma r _ _) = r 933 getRange (CompilePragma r _ _ _) = r 934 getRange (ForeignPragma r _ _) = r 935 getRange (StaticPragma r _) = r 936 getRange (InjectivePragma r _) = r 937 getRange (InlinePragma r _ _) = r 938 getRange (ImpossiblePragma r _) = r 939 getRange (EtaPragma r _) = r 940 getRange (TerminationCheckPragma r _) = r 941 getRange (NoCoverageCheckPragma r) = r 942 getRange (WarningOnUsage r _ _) = r 943 getRange (WarningOnImport r _) = r 944 getRange (CatchallPragma r) = r 945 getRange (DisplayPragma r _ _) = r 946 getRange (NoPositivityCheckPragma r) = r 947 getRange (PolarityPragma r _ _) = r 948 getRange (NoUniverseCheckPragma r) = r 949 950instance HasRange AsName where 951 getRange a = getRange (asRange a, asName a) 952 953instance HasRange Pattern where 954 getRange (IdentP x) = getRange x 955 getRange (AppP p q) = fuseRange p q 956 getRange (OpAppP r _ _ _) = r 957 getRange (RawAppP r _) = r 958 getRange (ParenP r _) = r 959 getRange (WildP r) = r 960 getRange (AsP r _ _) = r 961 getRange (AbsurdP r) = r 962 getRange (LitP r _) = r 963 getRange (QuoteP r) = r 964 getRange (HiddenP r _) = r 965 getRange (InstanceP r _) = r 966 getRange (DotP r _) = r 967 getRange (RecP r _) = r 968 getRange (EqualP r _) = r 969 getRange (EllipsisP r _) = r 970 getRange (WithP r _) = r 971 972-- SetRange instances 973------------------------------------------------------------------------ 974 975instance SetRange Pattern where 976 setRange r (IdentP x) = IdentP (setRange r x) 977 setRange r (AppP p q) = AppP (setRange r p) (setRange r q) 978 setRange r (OpAppP _ x ns ps) = OpAppP r x ns ps 979 setRange r (RawAppP _ ps) = RawAppP r ps 980 setRange r (ParenP _ p) = ParenP r p 981 setRange r (WildP _) = WildP r 982 setRange r (AsP _ x p) = AsP r (setRange r x) p 983 setRange r (AbsurdP _) = AbsurdP r 984 setRange r (LitP _ l) = LitP r l 985 setRange r (QuoteP _) = QuoteP r 986 setRange r (HiddenP _ p) = HiddenP r p 987 setRange r (InstanceP _ p) = InstanceP r p 988 setRange r (DotP _ e) = DotP r e 989 setRange r (RecP _ fs) = RecP r fs 990 setRange r (EqualP _ es) = EqualP r es 991 setRange r (EllipsisP _ mp) = EllipsisP r mp 992 setRange r (WithP _ p) = WithP r p 993 994instance SetRange TypedBinding where 995 setRange r (TBind _ xs e) = TBind r xs e 996 setRange r (TLet _ ds) = TLet r ds 997 998-- KillRange instances 999------------------------------------------------------------------------ 1000 1001instance KillRange a => KillRange (FieldAssignment' a) where 1002 killRange (FieldAssignment a b) = killRange2 FieldAssignment a b 1003 1004instance KillRange ModuleAssignment where 1005 killRange (ModuleAssignment a b c) = killRange3 ModuleAssignment a b c 1006 1007instance KillRange AsName where 1008 killRange (AsName n _) = killRange1 (flip AsName noRange) n 1009 1010instance KillRange Binder where 1011 killRange (Binder a b) = killRange2 Binder a b 1012 1013instance KillRange BoundName where 1014 killRange (BName n f t) = killRange3 BName n f t 1015 1016instance KillRange RecordDirective where 1017 killRange (Induction a) = killRange1 Induction a 1018 killRange (Eta a ) = killRange1 Eta a 1019 killRange (Constructor a b) = killRange2 Constructor a b 1020 killRange (PatternOrCopattern _) = PatternOrCopattern noRange 1021 1022instance KillRange Declaration where 1023 killRange (TypeSig i t n e) = killRange3 (TypeSig i) t n e 1024 killRange (FieldSig i t n e) = killRange4 FieldSig i t n e 1025 killRange (Generalize r ds ) = killRange1 (Generalize noRange) ds 1026 killRange (Field r fs) = killRange1 (Field noRange) fs 1027 killRange (FunClause l r w ca) = killRange4 FunClause l r w ca 1028 killRange (DataSig _ n l e) = killRange3 (DataSig noRange) n l e 1029 killRange (Data _ n l e c) = killRange4 (Data noRange) n l e c 1030 killRange (DataDef _ n l c) = killRange3 (DataDef noRange) n l c 1031 killRange (RecordSig _ n l e) = killRange3 (RecordSig noRange) n l e 1032 killRange (RecordDef _ n dir k d) = killRange4 (RecordDef noRange) n dir k d 1033 killRange (RecordDirective a) = killRange1 RecordDirective a 1034 killRange (Record _ n dir k e d) = killRange5 (Record noRange) n dir k e d 1035 killRange (Infix f n) = killRange2 Infix f n 1036 killRange (Syntax n no) = killRange1 (\n -> Syntax n no) n 1037 killRange (PatternSyn _ n ns p) = killRange3 (PatternSyn noRange) n ns p 1038 killRange (Mutual _ d) = killRange1 (Mutual noRange) d 1039 killRange (InterleavedMutual _ d) = killRange1 (InterleavedMutual noRange) d 1040 killRange (LoneConstructor _ d) = killRange1 (LoneConstructor noRange) d 1041 killRange (Abstract _ d) = killRange1 (Abstract noRange) d 1042 killRange (Private _ o d) = killRange2 (Private noRange) o d 1043 killRange (InstanceB _ d) = killRange1 (InstanceB noRange) d 1044 killRange (Macro _ d) = killRange1 (Macro noRange) d 1045 killRange (Postulate _ t) = killRange1 (Postulate noRange) t 1046 killRange (Primitive _ t) = killRange1 (Primitive noRange) t 1047 killRange (Open _ q i) = killRange2 (Open noRange) q i 1048 killRange (Import _ q a o i) = killRange3 (\q a -> Import noRange q a o) q a i 1049 killRange (ModuleMacro _ n m o i) = killRange3 (\n m -> ModuleMacro noRange n m o) n m i 1050 killRange (Module _ q t d) = killRange3 (Module noRange) q t d 1051 killRange (UnquoteDecl _ x t) = killRange2 (UnquoteDecl noRange) x t 1052 killRange (UnquoteDef _ x t) = killRange2 (UnquoteDef noRange) x t 1053 killRange (Pragma p) = killRange1 Pragma p 1054 1055instance KillRange Expr where 1056 killRange (Ident q) = killRange1 Ident q 1057 killRange (Lit _ l) = killRange1 (Lit noRange) l 1058 killRange (QuestionMark _ n) = QuestionMark noRange n 1059 killRange (Underscore _ n) = Underscore noRange n 1060 killRange (RawApp _ e) = killRange1 (RawApp noRange) e 1061 killRange (App _ e a) = killRange2 (App noRange) e a 1062 killRange (OpApp _ n ns o) = killRange3 (OpApp noRange) n ns o 1063 killRange (WithApp _ e es) = killRange2 (WithApp noRange) e es 1064 killRange (HiddenArg _ n) = killRange1 (HiddenArg noRange) n 1065 killRange (InstanceArg _ n) = killRange1 (InstanceArg noRange) n 1066 killRange (Lam _ l e) = killRange2 (Lam noRange) l e 1067 killRange (AbsurdLam _ h) = killRange1 (AbsurdLam noRange) h 1068 killRange (ExtendedLam _ e lrw) = killRange2 (ExtendedLam noRange) e lrw 1069 killRange (Fun _ e1 e2) = killRange2 (Fun noRange) e1 e2 1070 killRange (Pi t e) = killRange2 Pi t e 1071 killRange (Rec _ ne) = killRange1 (Rec noRange) ne 1072 killRange (RecUpdate _ e ne) = killRange2 (RecUpdate noRange) e ne 1073 killRange (Let _ d e) = killRange2 (Let noRange) d e 1074 killRange (Paren _ e) = killRange1 (Paren noRange) e 1075 killRange (IdiomBrackets _ es) = killRange1 (IdiomBrackets noRange) es 1076 killRange (DoBlock _ ss) = killRange1 (DoBlock noRange) ss 1077 killRange (Absurd _) = Absurd noRange 1078 killRange (As _ n e) = killRange2 (As noRange) n e 1079 killRange (Dot _ e) = killRange1 (Dot noRange) e 1080 killRange (DoubleDot _ e) = killRange1 (DoubleDot noRange) e 1081 killRange (ETel t) = killRange1 ETel t 1082 killRange (Quote _) = Quote noRange 1083 killRange (QuoteTerm _) = QuoteTerm noRange 1084 killRange (Unquote _) = Unquote noRange 1085 killRange (Tactic _ t) = killRange1 (Tactic noRange) t 1086 killRange (DontCare e) = killRange1 DontCare e 1087 killRange (Equal _ x y) = Equal noRange x y 1088 killRange (Ellipsis _) = Ellipsis noRange 1089 killRange (Generalized e) = killRange1 Generalized e 1090 1091instance KillRange LamBinding where 1092 killRange (DomainFree b) = killRange1 DomainFree b 1093 killRange (DomainFull t) = killRange1 DomainFull t 1094 1095instance KillRange LHS where 1096 killRange (LHS p r w) = killRange3 LHS p r w 1097 1098instance KillRange LamClause where 1099 killRange (LamClause a b c) = killRange3 LamClause a b c 1100 1101instance KillRange DoStmt where 1102 killRange (DoBind r p e w) = killRange4 DoBind r p e w 1103 killRange (DoThen e) = killRange1 DoThen e 1104 killRange (DoLet r ds) = killRange2 DoLet r ds 1105 1106instance KillRange ModuleApplication where 1107 killRange (SectionApp _ t e) = killRange2 (SectionApp noRange) t e 1108 killRange (RecordModuleInstance _ q) = killRange1 (RecordModuleInstance noRange) q 1109 1110instance KillRange e => KillRange (OpApp e) where 1111 killRange (SyntaxBindingLambda _ l e) = killRange2 (SyntaxBindingLambda noRange) l e 1112 killRange (Ordinary e) = killRange1 Ordinary e 1113 1114instance KillRange Pattern where 1115 killRange (IdentP q) = killRange1 IdentP q 1116 killRange (AppP p ps) = killRange2 AppP p ps 1117 killRange (RawAppP _ p) = killRange1 (RawAppP noRange) p 1118 killRange (OpAppP _ n ns p) = killRange3 (OpAppP noRange) n ns p 1119 killRange (HiddenP _ n) = killRange1 (HiddenP noRange) n 1120 killRange (InstanceP _ n) = killRange1 (InstanceP noRange) n 1121 killRange (ParenP _ p) = killRange1 (ParenP noRange) p 1122 killRange (WildP _) = WildP noRange 1123 killRange (AbsurdP _) = AbsurdP noRange 1124 killRange (AsP _ n p) = killRange2 (AsP noRange) n p 1125 killRange (DotP _ e) = killRange1 (DotP noRange) e 1126 killRange (LitP _ l) = killRange1 (LitP noRange) l 1127 killRange (QuoteP _) = QuoteP noRange 1128 killRange (RecP _ fs) = killRange1 (RecP noRange) fs 1129 killRange (EqualP _ es) = killRange1 (EqualP noRange) es 1130 killRange (EllipsisP _ mp) = killRange1 (EllipsisP noRange) mp 1131 killRange (WithP _ p) = killRange1 (WithP noRange) p 1132 1133instance KillRange Pragma where 1134 killRange (OptionsPragma _ s) = OptionsPragma noRange s 1135 killRange (BuiltinPragma _ s e) = killRange1 (BuiltinPragma noRange s) e 1136 killRange (RewritePragma _ _ qs) = killRange1 (RewritePragma noRange noRange) qs 1137 killRange (StaticPragma _ q) = killRange1 (StaticPragma noRange) q 1138 killRange (InjectivePragma _ q) = killRange1 (InjectivePragma noRange) q 1139 killRange (InlinePragma _ b q) = killRange1 (InlinePragma noRange b) q 1140 killRange (CompilePragma _ b q s) = killRange1 (\ q -> CompilePragma noRange b q s) q 1141 killRange (ForeignPragma _ b s) = ForeignPragma noRange b s 1142 killRange (ImpossiblePragma _ strs) = ImpossiblePragma noRange strs 1143 killRange (TerminationCheckPragma _ t) = TerminationCheckPragma noRange (killRange t) 1144 killRange (NoCoverageCheckPragma _) = NoCoverageCheckPragma noRange 1145 killRange (WarningOnUsage _ nm str) = WarningOnUsage noRange (killRange nm) str 1146 killRange (WarningOnImport _ str) = WarningOnImport noRange str 1147 killRange (CatchallPragma _) = CatchallPragma noRange 1148 killRange (DisplayPragma _ lhs rhs) = killRange2 (DisplayPragma noRange) lhs rhs 1149 killRange (EtaPragma _ q) = killRange1 (EtaPragma noRange) q 1150 killRange (NoPositivityCheckPragma _) = NoPositivityCheckPragma noRange 1151 killRange (PolarityPragma _ q occs) = killRange1 (\q -> PolarityPragma noRange q occs) q 1152 killRange (NoUniverseCheckPragma _) = NoUniverseCheckPragma noRange 1153 1154instance KillRange RHS where 1155 killRange AbsurdRHS = AbsurdRHS 1156 killRange (RHS e) = killRange1 RHS e 1157 1158instance KillRange TypedBinding where 1159 killRange (TBind _ b e) = killRange2 (TBind noRange) b e 1160 killRange (TLet r ds) = killRange2 TLet r ds 1161 1162instance KillRange WhereClause where 1163 killRange NoWhere = NoWhere 1164 killRange (AnyWhere r d) = killRange1 (AnyWhere noRange) d 1165 killRange (SomeWhere r n a d) = killRange3 (SomeWhere noRange) n a d 1166 1167------------------------------------------------------------------------ 1168-- NFData instances 1169 1170-- | Ranges are not forced. 1171 1172instance NFData Expr where 1173 rnf (Ident a) = rnf a 1174 rnf (Lit _ a) = rnf a 1175 rnf (QuestionMark _ a) = rnf a 1176 rnf (Underscore _ a) = rnf a 1177 rnf (RawApp _ a) = rnf a 1178 rnf (App _ a b) = rnf a `seq` rnf b 1179 rnf (OpApp _ a b c) = rnf a `seq` rnf b `seq` rnf c 1180 rnf (WithApp _ a b) = rnf a `seq` rnf b 1181 rnf (HiddenArg _ a) = rnf a 1182 rnf (InstanceArg _ a) = rnf a 1183 rnf (Lam _ a b) = rnf a `seq` rnf b 1184 rnf (AbsurdLam _ a) = rnf a 1185 rnf (ExtendedLam _ a b) = rnf a `seq` rnf b 1186 rnf (Fun _ a b) = rnf a `seq` rnf b 1187 rnf (Pi a b) = rnf a `seq` rnf b 1188 rnf (Rec _ a) = rnf a 1189 rnf (RecUpdate _ a b) = rnf a `seq` rnf b 1190 rnf (Let _ a b) = rnf a `seq` rnf b 1191 rnf (Paren _ a) = rnf a 1192 rnf (IdiomBrackets _ a) = rnf a 1193 rnf (DoBlock _ a) = rnf a 1194 rnf (Absurd _) = () 1195 rnf (As _ a b) = rnf a `seq` rnf b 1196 rnf (Dot _ a) = rnf a 1197 rnf (DoubleDot _ a) = rnf a 1198 rnf (ETel a) = rnf a 1199 rnf (Quote _) = () 1200 rnf (QuoteTerm _) = () 1201 rnf (Tactic _ a) = rnf a 1202 rnf (Unquote _) = () 1203 rnf (DontCare a) = rnf a 1204 rnf (Equal _ a b) = rnf a `seq` rnf b 1205 rnf (Ellipsis _) = () 1206 rnf (Generalized e) = rnf e 1207 1208-- | Ranges are not forced. 1209 1210instance NFData Pattern where 1211 rnf (IdentP a) = rnf a 1212 rnf (QuoteP _) = () 1213 rnf (AppP a b) = rnf a `seq` rnf b 1214 rnf (RawAppP _ a) = rnf a 1215 rnf (OpAppP _ a b c) = rnf a `seq` rnf b `seq` rnf c 1216 rnf (HiddenP _ a) = rnf a 1217 rnf (InstanceP _ a) = rnf a 1218 rnf (ParenP _ a) = rnf a 1219 rnf (WildP _) = () 1220 rnf (AbsurdP _) = () 1221 rnf (AsP _ a b) = rnf a `seq` rnf b 1222 rnf (DotP _ a) = rnf a 1223 rnf (LitP _ a) = rnf a 1224 rnf (RecP _ a) = rnf a 1225 rnf (EqualP _ es) = rnf es 1226 rnf (EllipsisP _ mp) = rnf mp 1227 rnf (WithP _ a) = rnf a 1228 1229-- | Ranges are not forced. 1230 1231instance NFData RecordDirective where 1232 rnf (Induction a) = rnf a 1233 rnf (Eta a ) = rnf a 1234 rnf (Constructor a b) = rnf (a, b) 1235 rnf (PatternOrCopattern _) = () 1236 1237instance NFData Declaration where 1238 rnf (TypeSig a b c d) = rnf a `seq` rnf b `seq` rnf c `seq` rnf d 1239 rnf (FieldSig a b c d) = rnf a `seq` rnf b `seq` rnf c `seq` rnf d 1240 rnf (Generalize _ a) = rnf a 1241 rnf (Field _ fs) = rnf fs 1242 rnf (FunClause a b c d) = rnf a `seq` rnf b `seq` rnf c `seq` rnf d 1243 rnf (DataSig _ a b c) = rnf a `seq` rnf b `seq` rnf c 1244 rnf (Data _ a b c d) = rnf a `seq` rnf b `seq` rnf c `seq` rnf d 1245 rnf (DataDef _ a b c) = rnf a `seq` rnf b `seq` rnf c 1246 rnf (RecordSig _ a b c) = rnf a `seq` rnf b `seq` rnf c 1247 rnf (RecordDef _ a b c d) = rnf (a, b, c, d) 1248 rnf (Record _ a b c d e) = rnf (a, b, c, d, e) 1249 rnf (RecordDirective a) = rnf a 1250 rnf (Infix a b) = rnf a `seq` rnf b 1251 rnf (Syntax a b) = rnf a `seq` rnf b 1252 rnf (PatternSyn _ a b c) = rnf a `seq` rnf b `seq` rnf c 1253 rnf (Mutual _ a) = rnf a 1254 rnf (InterleavedMutual _ a) = rnf a 1255 rnf (LoneConstructor _ a) = rnf a 1256 rnf (Abstract _ a) = rnf a 1257 rnf (Private _ _ a) = rnf a 1258 rnf (InstanceB _ a) = rnf a 1259 rnf (Macro _ a) = rnf a 1260 rnf (Postulate _ a) = rnf a 1261 rnf (Primitive _ a) = rnf a 1262 rnf (Open _ a b) = rnf a `seq` rnf b 1263 rnf (Import _ a b _ c) = rnf a `seq` rnf b `seq` rnf c 1264 rnf (ModuleMacro _ a b _ c) = rnf a `seq` rnf b `seq` rnf c 1265 rnf (Module _ a b c) = rnf a `seq` rnf b `seq` rnf c 1266 rnf (UnquoteDecl _ a b) = rnf a `seq` rnf b 1267 rnf (UnquoteDef _ a b) = rnf a `seq` rnf b 1268 rnf (Pragma a) = rnf a 1269 1270instance NFData OpenShortHand 1271 1272-- | Ranges are not forced. 1273 1274instance NFData Pragma where 1275 rnf (OptionsPragma _ a) = rnf a 1276 rnf (BuiltinPragma _ a b) = rnf a `seq` rnf b 1277 rnf (RewritePragma _ _ a) = rnf a 1278 rnf (CompilePragma _ a b c) = rnf a `seq` rnf b `seq` rnf c 1279 rnf (ForeignPragma _ b s) = rnf b `seq` rnf s 1280 rnf (StaticPragma _ a) = rnf a 1281 rnf (InjectivePragma _ a) = rnf a 1282 rnf (InlinePragma _ _ a) = rnf a 1283 rnf (ImpossiblePragma _ a) = rnf a 1284 rnf (EtaPragma _ a) = rnf a 1285 rnf (TerminationCheckPragma _ a) = rnf a 1286 rnf (NoCoverageCheckPragma _) = () 1287 rnf (WarningOnUsage _ a b) = rnf a `seq` rnf b 1288 rnf (WarningOnImport _ a) = rnf a 1289 rnf (CatchallPragma _) = () 1290 rnf (DisplayPragma _ a b) = rnf a `seq` rnf b 1291 rnf (NoPositivityCheckPragma _) = () 1292 rnf (PolarityPragma _ a b) = rnf a `seq` rnf b 1293 rnf (NoUniverseCheckPragma _) = () 1294 1295-- | Ranges are not forced. 1296 1297instance NFData AsName where 1298 rnf (AsName a _) = rnf a 1299 1300-- | Ranges are not forced. 1301 1302instance NFData a => NFData (TypedBinding' a) where 1303 rnf (TBind _ a b) = rnf a `seq` rnf b 1304 rnf (TLet _ a) = rnf a 1305 1306-- | Ranges are not forced. 1307 1308instance NFData ModuleApplication where 1309 rnf (SectionApp _ a b) = rnf a `seq` rnf b 1310 rnf (RecordModuleInstance _ a) = rnf a 1311 1312-- | Ranges are not forced. 1313 1314instance NFData a => NFData (OpApp a) where 1315 rnf (SyntaxBindingLambda _ a b) = rnf a `seq` rnf b 1316 rnf (Ordinary a) = rnf a 1317 1318-- | Ranges are not forced. 1319 1320instance NFData LHS where 1321 rnf (LHS a b c) = rnf a `seq` rnf b `seq` rnf c 1322 1323instance NFData a => NFData (FieldAssignment' a) where 1324 rnf (FieldAssignment a b) = rnf a `seq` rnf b 1325 1326instance NFData ModuleAssignment where 1327 rnf (ModuleAssignment a b c) = rnf a `seq` rnf b `seq` rnf c 1328 1329instance NFData a => NFData (WhereClause' a) where 1330 rnf NoWhere = () 1331 rnf (AnyWhere _ a) = rnf a 1332 rnf (SomeWhere _ a b c) = rnf a `seq` rnf b `seq` rnf c 1333 1334instance NFData LamClause where 1335 rnf (LamClause a b c) = rnf (a, b, c) 1336 1337instance NFData a => NFData (LamBinding' a) where 1338 rnf (DomainFree a) = rnf a 1339 rnf (DomainFull a) = rnf a 1340 1341instance NFData Binder where 1342 rnf (Binder a b) = rnf a `seq` rnf b 1343 1344instance NFData BoundName where 1345 rnf (BName a b c) = rnf a `seq` rnf b `seq` rnf c 1346 1347instance NFData a => NFData (RHS' a) where 1348 rnf AbsurdRHS = () 1349 rnf (RHS a) = rnf a 1350 1351instance NFData DoStmt where 1352 rnf (DoBind _ p e w) = rnf (p, e, w) 1353 rnf (DoThen e) = rnf e 1354 rnf (DoLet _ ds) = rnf ds 1355