1 2{-| The abstract syntax. This is what you get after desugaring and scope 3 analysis of the concrete syntax. The type checker works on abstract syntax, 4 producing internal syntax ("Agda.Syntax.Internal"). 5-} 6module Agda.Syntax.Abstract 7 ( module Agda.Syntax.Abstract 8 , module Agda.Syntax.Abstract.Name 9 ) where 10 11import Prelude hiding (null) 12 13import Control.DeepSeq 14 15import Data.Bifunctor 16import qualified Data.Foldable as Fold 17import Data.Function (on) 18import Data.Map (Map) 19import qualified Data.Map as Map 20import Data.Maybe 21import Data.Sequence (Seq, (<|), (><)) 22import qualified Data.Sequence as Seq 23import qualified Data.Set as Set 24import Data.Set (Set) 25import Data.Void 26import Data.Data (Data) 27 28import GHC.Generics (Generic) 29 30import Agda.Syntax.Concrete (FieldAssignment'(..), exprFieldA)--, HoleContent'(..)) 31import qualified Agda.Syntax.Concrete as C 32import Agda.Syntax.Abstract.Name 33import qualified Agda.Syntax.Internal as I 34import Agda.Syntax.Common 35import Agda.Syntax.Info 36import Agda.Syntax.Literal 37import Agda.Syntax.Position 38import Agda.Syntax.Scope.Base 39 40import Agda.TypeChecking.Positivity.Occurrence 41 42import Agda.Utils.Lens 43import Agda.Utils.List1 (List1, pattern (:|)) 44import qualified Agda.Utils.List1 as List1 45import Agda.Utils.Null 46import Agda.Utils.Pretty 47 48import Agda.Utils.Impossible 49 50-- | A name in a binding position: we also compare the nameConcrete 51-- when comparing the binders for equality. 52-- 53-- With @--caching@ on we compare abstract syntax to determine if we can 54-- reuse previous typechecking results: during that comparison two 55-- names can have the same nameId but be semantically different, 56-- e.g. in @{_ : A} -> ..@ vs. @{r : A} -> ..@. 57 58newtype BindName = BindName { unBind :: Name } 59 deriving (Show, Data, HasRange, KillRange, SetRange, NFData) 60 61mkBindName :: Name -> BindName 62mkBindName x = BindName x 63 64instance Eq BindName where 65 BindName n == BindName m 66 = ((==) `on` nameId) n m 67 && ((==) `on` nameConcrete) n m 68 69instance Ord BindName where 70 BindName n `compare` BindName m 71 = (compare `on` nameId) n m 72 `mappend` (compare `on` nameConcrete) n m 73 74type Args = [NamedArg Expr] 75 76-- | Expressions after scope checking (operators parsed, names resolved). 77data Expr 78 = Var Name -- ^ Bound variable. 79 | Def' QName Suffix -- ^ Constant: axiom, function, data or record type, 80 -- with a possible suffix. 81 | Proj ProjOrigin AmbiguousQName -- ^ Projection (overloaded). 82 | Con AmbiguousQName -- ^ Constructor (overloaded). 83 | PatternSyn AmbiguousQName -- ^ Pattern synonym. 84 | Macro QName -- ^ Macro. 85 | Lit ExprInfo Literal -- ^ Literal. 86 | QuestionMark MetaInfo InteractionId 87 -- ^ Meta variable for interaction. 88 -- The 'InteractionId' is usually identical with the 89 -- 'metaNumber' of 'MetaInfo'. 90 -- However, if you want to print an interaction meta as 91 -- just @?@ instead of @?n@, you should set the 92 -- 'metaNumber' to 'Nothing' while keeping the 'InteractionId'. 93 | Underscore MetaInfo 94 -- ^ Meta variable for hidden argument (must be inferred locally). 95 | Dot ExprInfo Expr -- ^ @.e@, for postfix projection. 96 | App AppInfo Expr (NamedArg Expr) -- ^ Ordinary (binary) application. 97 | WithApp ExprInfo Expr [Expr] -- ^ With application. 98 | Lam ExprInfo LamBinding Expr -- ^ @λ bs → e@. 99 | AbsurdLam ExprInfo Hiding -- ^ @λ()@ or @λ{}@. 100 | ExtendedLam ExprInfo DefInfo Erased QName (List1 Clause) 101 | Pi ExprInfo Telescope1 Expr -- ^ Dependent function space @Γ → A@. 102 | Generalized (Set QName) Expr -- ^ Like a Pi, but the ordering is not known 103 | Fun ExprInfo (Arg Expr) Expr -- ^ Non-dependent function space. 104 | Let ExprInfo (List1 LetBinding) Expr 105 -- ^ @let bs in e@. 106 | ETel Telescope -- ^ Only used when printing telescopes. 107 | Rec ExprInfo RecordAssigns -- ^ Record construction. 108 | RecUpdate ExprInfo Expr Assigns -- ^ Record update. 109 | ScopedExpr ScopeInfo Expr -- ^ Scope annotation. 110 | Quote ExprInfo -- ^ Quote an identifier 'QName'. 111 | QuoteTerm ExprInfo -- ^ Quote a term. 112 | Unquote ExprInfo -- ^ The splicing construct: unquote ... 113 | Tactic ExprInfo Expr [NamedArg Expr] 114 -- ^ @tactic e x1 .. xn@ 115 | DontCare Expr -- ^ For printing @DontCare@ from @Syntax.Internal@. 116 deriving (Data, Show, Generic) 117 118-- | Pattern synonym for regular Def 119pattern Def :: QName -> Expr 120pattern Def x = Def' x NoSuffix 121 122-- | Smart constructor for Generalized 123generalized :: Set QName -> Expr -> Expr 124generalized s e 125 | null s = e 126 | otherwise = Generalized s e 127 128-- | Record field assignment @f = e@. 129type Assign = FieldAssignment' Expr 130type Assigns = [Assign] 131type RecordAssign = Either Assign ModuleName 132type RecordAssigns = [RecordAssign] 133 134-- | Renaming (generic). 135type Ren a = Map a (List1 a) 136 137data ScopeCopyInfo = ScopeCopyInfo 138 { renModules :: Ren ModuleName 139 , renNames :: Ren QName } 140 deriving (Eq, Show, Data, Generic) 141 142initCopyInfo :: ScopeCopyInfo 143initCopyInfo = ScopeCopyInfo 144 { renModules = mempty 145 , renNames = mempty 146 } 147 148instance Pretty ScopeCopyInfo where 149 pretty i = vcat [ prRen "renModules =" (renModules i) 150 , prRen "renNames =" (renNames i) ] 151 where 152 prRen s r = sep [ text s, nest 2 $ vcat (map pr xs) ] 153 where 154 xs = [ (k, v) | (k, vs) <- Map.toList r, v <- List1.toList vs ] 155 pr (x, y) = pretty x <+> "->" <+> pretty y 156 157type RecordDirectives = RecordDirectives' QName 158 159data Declaration 160 = Axiom KindOfName DefInfo ArgInfo (Maybe [Occurrence]) QName Expr 161 -- ^ Type signature (can be irrelevant, but not hidden). 162 -- 163 -- The fourth argument contains an optional assignment of 164 -- polarities to arguments. 165 | Generalize (Set QName) DefInfo ArgInfo QName Expr 166 -- ^ First argument is set of generalizable variables used in the type. 167 | Field DefInfo QName (Arg Expr) -- ^ record field 168 | Primitive DefInfo QName (Arg Expr) -- ^ primitive function 169 | Mutual MutualInfo [Declaration] -- ^ a bunch of mutually recursive definitions 170 | Section Range ModuleName GeneralizeTelescope [Declaration] 171 | Apply ModuleInfo ModuleName ModuleApplication ScopeCopyInfo ImportDirective 172 -- ^ The @ImportDirective@ is for highlighting purposes. 173 | Import ModuleInfo ModuleName ImportDirective 174 -- ^ The @ImportDirective@ is for highlighting purposes. 175 | Pragma Range Pragma 176 | Open ModuleInfo ModuleName ImportDirective 177 -- ^ only retained for highlighting purposes 178 | FunDef DefInfo QName Delayed [Clause] -- ^ sequence of function clauses 179 | DataSig DefInfo QName GeneralizeTelescope Expr -- ^ lone data signature 180 | DataDef DefInfo QName UniverseCheck DataDefParams [Constructor] 181 | RecSig DefInfo QName GeneralizeTelescope Expr -- ^ lone record signature 182 | RecDef DefInfo QName UniverseCheck RecordDirectives DataDefParams Expr [Declaration] 183 -- ^ The 'Expr' gives the constructor type telescope, @(x1 : A1)..(xn : An) -> Prop@, 184 -- and the optional name is the constructor's name. 185 -- The optional 'Range' is for the @pattern@ attribute. 186 | PatternSynDef QName [Arg BindName] (Pattern' Void) 187 -- ^ Only for highlighting purposes 188 | UnquoteDecl MutualInfo [DefInfo] [QName] Expr 189 | UnquoteDef [DefInfo] [QName] Expr 190 | ScopedDecl ScopeInfo [Declaration] -- ^ scope annotation 191 deriving (Data, Show, Generic) 192 193type DefInfo = DefInfo' Expr 194 195type ImportDirective = ImportDirective' QName ModuleName 196type Renaming = Renaming' QName ModuleName 197type ImportedName = ImportedName' QName ModuleName 198 199data ModuleApplication 200 = SectionApp Telescope ModuleName [NamedArg Expr] 201 -- ^ @tel. M args@: applies @M@ to @args@ and abstracts @tel@. 202 | RecordModuleInstance ModuleName 203 -- ^ @M {{...}}@ 204 deriving (Data, Show, Eq, Generic) 205 206data Pragma 207 = OptionsPragma [String] 208 | BuiltinPragma RString ResolvedName 209 -- ^ 'ResolvedName' is not 'UnknownName'. 210 -- Name can be ambiguous e.g. for built-in constructors. 211 | BuiltinNoDefPragma RString KindOfName QName 212 -- ^ Builtins that do not come with a definition, 213 -- but declare a name for an Agda concept. 214 | RewritePragma Range [QName] 215 -- ^ Range is range of REWRITE keyword. 216 | CompilePragma RString QName String 217 | StaticPragma QName 218 | EtaPragma QName 219 -- ^ For coinductive records, use pragma instead of regular 220 -- @eta-equality@ definition (as it is might make Agda loop). 221 | InjectivePragma QName 222 | InlinePragma Bool QName -- INLINE or NOINLINE 223 | DisplayPragma QName [NamedArg Pattern] Expr 224 deriving (Data, Show, Eq, Generic) 225 226-- | Bindings that are valid in a @let@. 227data LetBinding 228 = LetBind LetInfo ArgInfo BindName Expr Expr 229 -- ^ @LetBind info rel name type defn@ 230 | LetPatBind LetInfo Pattern Expr 231 -- ^ Irrefutable pattern binding. 232 | LetApply ModuleInfo ModuleName ModuleApplication ScopeCopyInfo ImportDirective 233 -- ^ @LetApply mi newM (oldM args) renamings dir@. 234 -- The @ImportDirective@ is for highlighting purposes. 235 | LetOpen ModuleInfo ModuleName ImportDirective 236 -- ^ only for highlighting and abstractToConcrete 237 | LetDeclaredVariable BindName 238 -- ^ Only used for highlighting. Refers to the first occurrence of 239 -- @x@ in @let x : A; x = e@. 240-- | LetGeneralize DefInfo ArgInfo Expr 241 deriving (Data, Show, Eq, Generic) 242 243-- | Only 'Axiom's. 244type TypeSignature = Declaration 245type Constructor = TypeSignature 246type Field = TypeSignature 247 248type TacticAttr = Maybe Expr 249 250-- A Binder @x\@p@, the pattern is optional 251data Binder' a = Binder 252 { binderPattern :: Maybe Pattern 253 , binderName :: a 254 } deriving (Data, Show, Eq, Functor, Foldable, Traversable, Generic) 255 256type Binder = Binder' BindName 257 258mkBinder :: a -> Binder' a 259mkBinder = Binder Nothing 260 261mkBinder_ :: Name -> Binder 262mkBinder_ = mkBinder . mkBindName 263 264extractPattern :: Binder' a -> Maybe (Pattern, a) 265extractPattern (Binder p a) = (,a) <$> p 266 267-- | A lambda binding is either domain free or typed. 268data LamBinding 269 = DomainFree TacticAttr (NamedArg Binder) 270 -- ^ . @x@ or @{x}@ or @.x@ or @{x = y}@ or @x\@p@ or @(p)@ 271 | DomainFull TypedBinding 272 -- ^ . @(xs:e)@ or @{xs:e}@ or @(let Ds)@ 273 deriving (Data, Show, Eq, Generic) 274 275mkDomainFree :: NamedArg Binder -> LamBinding 276mkDomainFree = DomainFree Nothing 277 278-- | A typed binding. Appears in dependent function spaces, typed lambdas, and 279-- telescopes. It might be tempting to simplify this to only bind a single 280-- name at a time, and translate, say, @(x y : A)@ to @(x : A)(y : A)@ 281-- before type-checking. However, this would be slightly problematic: 282-- 283-- 1. We would have to typecheck the type @A@ several times. 284-- 285-- 2. If @A@ contains a meta variable or hole, it would be duplicated 286-- by such a translation. 287-- 288-- While 1. is only slightly inefficient, 2. would be an outright bug. 289-- Duplicating @A@ could not be done naively, we would have to make sure 290-- that the metas of the copy are aliases of the metas of the original. 291 292data TypedBinding 293 = TBind Range TacticAttr (List1 (NamedArg Binder)) Expr 294 -- ^ As in telescope @(x y z : A)@ or type @(x y z : A) -> B@. 295 | TLet Range (List1 LetBinding) 296 -- ^ E.g. @(let x = e)@ or @(let open M)@. 297 deriving (Data, Show, Eq, Generic) 298 299mkTBind :: Range -> List1 (NamedArg Binder) -> Expr -> TypedBinding 300mkTBind r = TBind r Nothing 301 302mkTLet :: Range -> [LetBinding] -> Maybe TypedBinding 303mkTLet _ [] = Nothing 304mkTLet r (d:ds) = Just $ TLet r (d :| ds) 305 306type Telescope1 = List1 TypedBinding 307type Telescope = [TypedBinding] 308 309mkPi :: ExprInfo -> Telescope -> Expr -> Expr 310mkPi i [] e = e 311mkPi i (x:xs) e = Pi i (x :| xs) e 312 313data GeneralizeTelescope = GeneralizeTel 314 { generalizeTelVars :: Map QName Name 315 -- ^ Maps generalize variables to the corresponding bound variable (to be 316 -- introduced by the generalisation). 317 , generalizeTel :: Telescope } 318 deriving (Data, Show, Eq, Generic) 319 320data DataDefParams = DataDefParams 321 { dataDefGeneralizedParams :: Set Name 322 -- ^ We don't yet know the position of generalized parameters from the data 323 -- sig, so we keep these in a set on the side. 324 , dataDefParams :: [LamBinding] 325 } 326 deriving (Data, Show, Eq, Generic) 327 328noDataDefParams :: DataDefParams 329noDataDefParams = DataDefParams Set.empty [] 330 331-- | A user pattern together with an internal term that it should be equal to 332-- after splitting is complete. 333-- Special cases: 334-- * User pattern is a variable but internal term isn't: 335-- this will be turned into an as pattern. 336-- * User pattern is a dot pattern: 337-- this pattern won't trigger any splitting but will be checked 338-- for equality after all splitting is complete and as patterns have 339-- been bound. 340-- * User pattern is an absurd pattern: 341-- emptiness of the type will be checked after splitting is complete. 342-- * User pattern is an annotated wildcard: 343-- type annotation will be checked after splitting is complete. 344data ProblemEq = ProblemEq 345 { problemInPat :: Pattern 346 , problemInst :: I.Term 347 , problemType :: I.Dom I.Type 348 } deriving (Data, Show, Generic) 349 350-- These are not relevant for caching purposes 351instance Eq ProblemEq where _ == _ = True 352 353-- | We could throw away @where@ clauses at this point and translate them to 354-- @let@. It's not obvious how to remember that the @let@ was really a 355-- @where@ clause though, so for the time being we keep it here. 356data Clause' lhs = Clause 357 { clauseLHS :: lhs 358 , clauseStrippedPats :: [ProblemEq] 359 -- ^ Only in with-clauses where we inherit some already checked patterns from the parent. 360 -- These live in the context of the parent clause left-hand side. 361 , clauseRHS :: RHS 362 , clauseWhereDecls :: WhereDeclarations 363 , clauseCatchall :: Bool 364 } deriving (Data, Show, Functor, Foldable, Traversable, Eq, Generic) 365 366data WhereDeclarations = WhereDecls 367 { whereModule :: Maybe ModuleName 368 -- #2897: we need to restrict named where modules in refined contexts, 369 -- so remember whether it was named here 370 , whereDecls :: Maybe Declaration 371 -- ^ The declaration is a 'Section'. 372 } deriving (Data, Show, Eq, Generic) 373 374instance Null WhereDeclarations where 375 empty = WhereDecls empty empty 376 377noWhereDecls :: WhereDeclarations 378noWhereDecls = empty 379 380type Clause = Clause' LHS 381type SpineClause = Clause' SpineLHS 382type RewriteEqn = RewriteEqn' QName BindName Pattern Expr 383type WithExpr' e = Named BindName (Arg e) 384type WithExpr = WithExpr' Expr 385 386data RHS 387 = RHS 388 { rhsExpr :: Expr 389 , rhsConcrete :: Maybe C.Expr 390 -- ^ We store the original concrete expression in case 391 -- we have to reproduce it during interactive case splitting. 392 -- 'Nothing' for internally generated rhss. 393 } 394 | AbsurdRHS 395 | WithRHS QName [WithExpr] [Clause] 396 -- ^ The 'QName' is the name of the with function. 397 | RewriteRHS 398 { rewriteExprs :: [RewriteEqn] 399 -- ^ The 'QName's are the names of the generated with functions, 400 -- one for each 'Expr'. 401 , rewriteStrippedPats :: [ProblemEq] 402 -- ^ The patterns stripped by with-desugaring. These are only present 403 -- if this rewrite follows a with. 404 , rewriteRHS :: RHS 405 -- ^ The RHS should not be another @RewriteRHS@. 406 , rewriteWhereDecls :: WhereDeclarations 407 -- ^ The where clauses are attached to the @RewriteRHS@ by 408 --- the scope checker (instead of to the clause). 409 } 410 deriving (Data, Show, Generic) 411 412-- | Ignore 'rhsConcrete' when comparing 'RHS's. 413instance Eq RHS where 414 RHS e _ == RHS e' _ = e == e' 415 AbsurdRHS == AbsurdRHS = True 416 WithRHS a b c == WithRHS a' b' c' = (a == a') && (b == b') && (c == c') 417 RewriteRHS a b c d == RewriteRHS a' b' c' d' = and [ a == a', b == b', c == c' , d == d' ] 418 _ == _ = False 419 420-- | The lhs of a clause in spine view (inside-out). 421-- Projection patterns are contained in @spLhsPats@, 422-- represented as @ProjP d@. 423data SpineLHS = SpineLHS 424 { spLhsInfo :: LHSInfo -- ^ Range. 425 , spLhsDefName :: QName -- ^ Name of function we are defining. 426 , spLhsPats :: [NamedArg Pattern] -- ^ Elimination by pattern, projections, with-patterns. 427 } 428 deriving (Data, Show, Eq, Generic) 429 430-- | Ignore 'Range' when comparing 'LHS's. 431instance Eq LHS where 432 LHS _ core == LHS _ core' = core == core' 433 434-- | The lhs of a clause in focused (projection-application) view (outside-in). 435-- Projection patters are represented as 'LHSProj's. 436data LHS = LHS 437 { lhsInfo :: LHSInfo -- ^ Range. 438 , lhsCore :: LHSCore -- ^ Copatterns. 439 } 440 deriving (Data, Show, Generic) 441 442-- | The lhs in projection-application and with-pattern view. 443-- Parameterised over the type @e@ of dot patterns. 444data LHSCore' e 445 -- | The head applied to ordinary patterns. 446 = LHSHead { lhsDefName :: QName 447 -- ^ Head @f@. 448 , lhsPats :: [NamedArg (Pattern' e)] 449 -- ^ Applied to patterns @ps@. 450 } 451 -- | Projection. 452 | LHSProj { lhsDestructor :: AmbiguousQName 453 -- ^ Record projection identifier. 454 , lhsFocus :: NamedArg (LHSCore' e) 455 -- ^ Main argument of projection. 456 , lhsPats :: [NamedArg (Pattern' e)] 457 -- ^ Further applied to patterns. 458 } 459 -- | With patterns. 460 | LHSWith { lhsHead :: LHSCore' e 461 -- ^ E.g. the 'LHSHead'. 462 , lhsWithPatterns :: [Arg (Pattern' e)] 463 -- ^ Applied to with patterns @| p1 | ... | pn@. 464 -- These patterns are not prefixed with @WithP@! 465 , lhsPats :: [NamedArg (Pattern' e)] 466 -- ^ Further applied to patterns. 467 } 468 deriving (Data, Show, Functor, Foldable, Traversable, Eq, Generic) 469 470type LHSCore = LHSCore' Expr 471 472--------------------------------------------------------------------------- 473-- * Patterns 474--------------------------------------------------------------------------- 475 476-- | Parameterised over the type of dot patterns. 477data Pattern' e 478 = VarP BindName 479 | ConP ConPatInfo AmbiguousQName (NAPs e) 480 | ProjP PatInfo ProjOrigin AmbiguousQName 481 -- ^ Destructor pattern @d@. 482 | DefP PatInfo AmbiguousQName (NAPs e) 483 -- ^ Defined pattern: function definition @f ps@. 484 -- It is also abused to convert destructor patterns into concrete syntax 485 -- thus, we put AmbiguousQName here as well. 486 | WildP PatInfo 487 -- ^ Underscore pattern entered by user. 488 -- Or generated at type checking for implicit arguments. 489 | AsP PatInfo BindName (Pattern' e) 490 | DotP PatInfo e 491 -- ^ Dot pattern @.e@ 492 | AbsurdP PatInfo 493 | LitP PatInfo Literal 494 | PatternSynP PatInfo AmbiguousQName (NAPs e) 495 | RecP PatInfo [FieldAssignment' (Pattern' e)] 496 | EqualP PatInfo [(e, e)] 497 | WithP PatInfo (Pattern' e) -- ^ @| p@, for with-patterns. 498 | AnnP PatInfo e (Pattern' e) -- ^ Pattern with type annotation 499 deriving (Data, Show, Functor, Foldable, Traversable, Eq, Generic) 500 501type NAPs e = [NamedArg (Pattern' e)] 502type NAPs1 e = List1 (NamedArg (Pattern' e)) 503type Pattern = Pattern' Expr 504type Patterns = [NamedArg Pattern] 505 506instance IsProjP (Pattern' e) where 507 -- Andreas, 2018-06-19, issue #3130 508 -- Do not interpret things like .(p) as projection pattern any more. 509 -- maybePostfixProjP (DotP _ e) = isProjP e <&> \ (_o, d) -> (ProjPostfix, d) 510 isProjP (ProjP _ o d) = Just (o, d) 511 isProjP _ = Nothing 512 513instance IsProjP Expr where 514 isProjP (Proj o ds) = Just (o, ds) 515 isProjP (ScopedExpr _ e) = isProjP e 516 isProjP _ = Nothing 517 518{-------------------------------------------------------------------------- 519 Things we parse but are not part of the Agda file syntax 520 --------------------------------------------------------------------------} 521 522type HoleContent = C.HoleContent' () BindName Pattern Expr 523 524{-------------------------------------------------------------------------- 525 Instances 526 --------------------------------------------------------------------------} 527 528-- | Does not compare 'ScopeInfo' fields. 529-- Does not distinguish between prefix and postfix projections. 530 531instance Eq Expr where 532 ScopedExpr _ a1 == ScopedExpr _ a2 = a1 == a2 533 534 Var a1 == Var a2 = a1 == a2 535 Def' a1 s1 == Def' a2 s2 = (a1, s1) == (a2, s2) 536 Proj _ a1 == Proj _ a2 = a1 == a2 537 Con a1 == Con a2 = a1 == a2 538 PatternSyn a1 == PatternSyn a2 = a1 == a2 539 Macro a1 == Macro a2 = a1 == a2 540 Lit r1 a1 == Lit r2 a2 = (r1, a1) == (r2, a2) 541 QuestionMark a1 b1 == QuestionMark a2 b2 = (a1, b1) == (a2, b2) 542 Underscore a1 == Underscore a2 = a1 == a2 543 Dot r1 e1 == Dot r2 e2 = (r1, e1) == (r2, e2) 544 App a1 b1 c1 == App a2 b2 c2 = (a1, b1, c1) == (a2, b2, c2) 545 WithApp a1 b1 c1 == WithApp a2 b2 c2 = (a1, b1, c1) == (a2, b2, c2) 546 Lam a1 b1 c1 == Lam a2 b2 c2 = (a1, b1, c1) == (a2, b2, c2) 547 AbsurdLam a1 b1 == AbsurdLam a2 b2 = (a1, b1) == (a2, b2) 548 ExtendedLam a1 b1 c1 d1 e1 == ExtendedLam a2 b2 c2 d2 e2 = (a1, b1, c1, d1, e1) == 549 (a2, b2, c2, d2, e2) 550 Pi a1 b1 c1 == Pi a2 b2 c2 = (a1, b1, c1) == (a2, b2, c2) 551 Generalized a1 b1 == Generalized a2 b2 = (a1, b1) == (a2, b2) 552 Fun a1 b1 c1 == Fun a2 b2 c2 = (a1, b1, c1) == (a2, b2, c2) 553 Let a1 b1 c1 == Let a2 b2 c2 = (a1, b1, c1) == (a2, b2, c2) 554 ETel a1 == ETel a2 = a1 == a2 555 Rec a1 b1 == Rec a2 b2 = (a1, b1) == (a2, b2) 556 RecUpdate a1 b1 c1 == RecUpdate a2 b2 c2 = (a1, b1, c1) == (a2, b2, c2) 557 Quote a1 == Quote a2 = a1 == a2 558 QuoteTerm a1 == QuoteTerm a2 = a1 == a2 559 Unquote a1 == Unquote a2 = a1 == a2 560 Tactic a1 b1 c1 == Tactic a2 b2 c2 = (a1, b1, c1) == (a2, b2, c2) 561 DontCare a1 == DontCare a2 = a1 == a2 562 563 _ == _ = False 564 565-- | Does not compare 'ScopeInfo' fields. 566 567instance Eq Declaration where 568 ScopedDecl _ a1 == ScopedDecl _ a2 = a1 == a2 569 570 Axiom a1 b1 c1 d1 e1 f1 == Axiom a2 b2 c2 d2 e2 f2 = (a1, b1, c1, d1, e1, f1) == (a2, b2, c2, d2, e2, f2) 571 Generalize a1 b1 c1 d1 e1 == Generalize a2 b2 c2 d2 e2 = (a1, b1, c1, d1, e1) == (a2, b2, c2, d2, e2) 572 Field a1 b1 c1 == Field a2 b2 c2 = (a1, b1, c1) == (a2, b2, c2) 573 Primitive a1 b1 c1 == Primitive a2 b2 c2 = (a1, b1, c1) == (a2, b2, c2) 574 Mutual a1 b1 == Mutual a2 b2 = (a1, b1) == (a2, b2) 575 Section a1 b1 c1 d1 == Section a2 b2 c2 d2 = (a1, b1, c1, d1) == (a2, b2, c2, d2) 576 Apply a1 b1 c1 d1 e1 == Apply a2 b2 c2 d2 e2 = (a1, b1, c1, d1, e1) == (a2, b2, c2, d2, e2) 577 Import a1 b1 c1 == Import a2 b2 c2 = (a1, b1, c1) == (a2, b2, c2) 578 Pragma a1 b1 == Pragma a2 b2 = (a1, b1) == (a2, b2) 579 Open a1 b1 c1 == Open a2 b2 c2 = (a1, b1, c1) == (a2, b2, c2) 580 FunDef a1 b1 c1 d1 == FunDef a2 b2 c2 d2 = (a1, b1, c1, d1) == (a2, b2, c2, d2) 581 DataSig a1 b1 c1 d1 == DataSig a2 b2 c2 d2 = (a1, b1, c1, d1) == (a2, b2, c2, d2) 582 DataDef a1 b1 c1 d1 e1 == DataDef a2 b2 c2 d2 e2 = (a1, b1, c1, d1, e1) == (a2, b2, c2, d2, e2) 583 RecSig a1 b1 c1 d1 == RecSig a2 b2 c2 d2 = (a1, b1, c1, d1) == (a2, b2, c2, d2) 584 RecDef a1 b1 c1 d1 e1 f1 g1 == RecDef a2 b2 c2 d2 e2 f2 g2 = (a1, b1, c1, d1, e1, f1, g1) == (a2, b2, c2, d2, e2, f2, g2) 585 PatternSynDef a1 b1 c1 == PatternSynDef a2 b2 c2 = (a1, b1, c1) == (a2, b2, c2) 586 UnquoteDecl a1 b1 c1 d1 == UnquoteDecl a2 b2 c2 d2 = (a1, b1, c1, d1) == (a2, b2, c2, d2) 587 UnquoteDef a1 b1 c1 == UnquoteDef a2 b2 c2 = (a1, b1, c1) == (a2, b2, c2) 588 589 _ == _ = False 590 591instance Underscore Expr where 592 underscore = Underscore emptyMetaInfo 593 isUnderscore = __IMPOSSIBLE__ 594 595instance LensHiding LamBinding where 596 getHiding (DomainFree _ x) = getHiding x 597 getHiding (DomainFull tb) = getHiding tb 598 mapHiding f (DomainFree t x) = DomainFree t $ mapHiding f x 599 mapHiding f (DomainFull tb) = DomainFull $ mapHiding f tb 600 601instance LensHiding TypedBinding where 602 getHiding (TBind _ _ (x :|_) _) = getHiding x -- Slightly dubious 603 getHiding TLet{} = mempty 604 mapHiding f (TBind r t xs e) = TBind r t ((fmap . mapHiding) f xs) e 605 mapHiding f b@TLet{} = b 606 607instance HasRange a => HasRange (Binder' a) where 608 getRange (Binder p n) = fuseRange p n 609 610instance HasRange LamBinding where 611 getRange (DomainFree _ x) = getRange x 612 getRange (DomainFull b) = getRange b 613 614instance HasRange TypedBinding where 615 getRange (TBind r _ _ _) = r 616 getRange (TLet r _) = r 617 618instance HasRange Expr where 619 getRange (Var x) = getRange x 620 getRange (Def' x _) = getRange x 621 getRange (Proj _ x) = getRange x 622 getRange (Con x) = getRange x 623 getRange (Lit i _) = getRange i 624 getRange (QuestionMark i _) = getRange i 625 getRange (Underscore i) = getRange i 626 getRange (Dot i _) = getRange i 627 getRange (App i _ _) = getRange i 628 getRange (WithApp i _ _) = getRange i 629 getRange (Lam i _ _) = getRange i 630 getRange (AbsurdLam i _) = getRange i 631 getRange (ExtendedLam i _ _ _ _) = getRange i 632 getRange (Pi i _ _) = getRange i 633 getRange (Generalized _ x) = getRange x 634 getRange (Fun i _ _) = getRange i 635 getRange (Let i _ _) = getRange i 636 getRange (Rec i _) = getRange i 637 getRange (RecUpdate i _ _) = getRange i 638 getRange (ETel tel) = getRange tel 639 getRange (ScopedExpr _ e) = getRange e 640 getRange (Quote i) = getRange i 641 getRange (QuoteTerm i) = getRange i 642 getRange (Unquote i) = getRange i 643 getRange (Tactic i _ _) = getRange i 644 getRange (DontCare{}) = noRange 645 getRange (PatternSyn x) = getRange x 646 getRange (Macro x) = getRange x 647 648instance HasRange Declaration where 649 getRange (Axiom _ i _ _ _ _ ) = getRange i 650 getRange (Generalize _ i _ _ _) = getRange i 651 getRange (Field i _ _ ) = getRange i 652 getRange (Mutual i _ ) = getRange i 653 getRange (Section i _ _ _ ) = getRange i 654 getRange (Apply i _ _ _ _) = getRange i 655 getRange (Import i _ _ ) = getRange i 656 getRange (Primitive i _ _ ) = getRange i 657 getRange (Pragma i _ ) = getRange i 658 getRange (Open i _ _ ) = getRange i 659 getRange (ScopedDecl _ d ) = getRange d 660 getRange (FunDef i _ _ _ ) = getRange i 661 getRange (DataSig i _ _ _ ) = getRange i 662 getRange (DataDef i _ _ _ _ ) = getRange i 663 getRange (RecSig i _ _ _ ) = getRange i 664 getRange (RecDef i _ _ _ _ _ _) = getRange i 665 getRange (PatternSynDef x _ _ ) = getRange x 666 getRange (UnquoteDecl _ i _ _) = getRange i 667 getRange (UnquoteDef i _ _) = getRange i 668 669instance HasRange (Pattern' e) where 670 getRange (VarP x) = getRange x 671 getRange (ConP i _ _) = getRange i 672 getRange (ProjP i _ _) = getRange i 673 getRange (DefP i _ _) = getRange i 674 getRange (WildP i) = getRange i 675 getRange (AsP i _ _) = getRange i 676 getRange (DotP i _) = getRange i 677 getRange (AbsurdP i) = getRange i 678 getRange (LitP i l) = getRange i 679 getRange (PatternSynP i _ _) = getRange i 680 getRange (RecP i _) = getRange i 681 getRange (EqualP i _) = getRange i 682 getRange (WithP i _) = getRange i 683 getRange (AnnP i _ _) = getRange i 684 685instance HasRange SpineLHS where 686 getRange (SpineLHS i _ _) = getRange i 687 688instance HasRange LHS where 689 getRange (LHS i _) = getRange i 690 691instance HasRange (LHSCore' e) where 692 getRange (LHSHead f ps) = fuseRange f ps 693 getRange (LHSProj d lhscore ps) = d `fuseRange` lhscore `fuseRange` ps 694 getRange (LHSWith h wps ps) = h `fuseRange` wps `fuseRange` ps 695 696instance HasRange a => HasRange (Clause' a) where 697 getRange (Clause lhs _ rhs ds catchall) = getRange (lhs, rhs, ds) 698 699instance HasRange RHS where 700 getRange AbsurdRHS = noRange 701 getRange (RHS e _) = getRange e 702 getRange (WithRHS _ e cs) = fuseRange e cs 703 getRange (RewriteRHS xes _ rhs wh) = getRange (xes, rhs, wh) 704 705instance HasRange WhereDeclarations where 706 getRange (WhereDecls _ ds) = getRange ds 707 708instance HasRange LetBinding where 709 getRange (LetBind i _ _ _ _ ) = getRange i 710 getRange (LetPatBind i _ _ ) = getRange i 711 getRange (LetApply i _ _ _ _ ) = getRange i 712 getRange (LetOpen i _ _ ) = getRange i 713 getRange (LetDeclaredVariable x) = getRange x 714 715-- setRange for patterns applies the range to the outermost pattern constructor 716instance SetRange (Pattern' a) where 717 setRange r (VarP x) = VarP (setRange r x) 718 setRange r (ConP i ns as) = ConP (setRange r i) ns as 719 setRange r (ProjP _ o ns) = ProjP (PatRange r) o ns 720 setRange r (DefP _ ns as) = DefP (PatRange r) ns as -- (setRange r n) as 721 setRange r (WildP _) = WildP (PatRange r) 722 setRange r (AsP _ n p) = AsP (PatRange r) (setRange r n) p 723 setRange r (DotP _ e) = DotP (PatRange r) e 724 setRange r (AbsurdP _) = AbsurdP (PatRange r) 725 setRange r (LitP _ l) = LitP (PatRange r) l 726 setRange r (PatternSynP _ n as) = PatternSynP (PatRange r) n as 727 setRange r (RecP i as) = RecP (PatRange r) as 728 setRange r (EqualP _ es) = EqualP (PatRange r) es 729 setRange r (WithP i p) = WithP (setRange r i) p 730 setRange r (AnnP i a p) = AnnP (setRange r i) a p 731 732instance KillRange a => KillRange (Binder' a) where 733 killRange (Binder a b) = killRange2 Binder a b 734 735instance KillRange LamBinding where 736 killRange (DomainFree t x) = killRange2 DomainFree t x 737 killRange (DomainFull b) = killRange1 DomainFull b 738 739instance KillRange GeneralizeTelescope where 740 killRange (GeneralizeTel s tel) = GeneralizeTel s (killRange tel) 741 742instance KillRange DataDefParams where 743 killRange (DataDefParams s tel) = DataDefParams s (killRange tel) 744 745instance KillRange TypedBinding where 746 killRange (TBind r t xs e) = killRange4 TBind r t xs e 747 killRange (TLet r lbs) = killRange2 TLet r lbs 748 749instance KillRange Expr where 750 killRange (Var x) = killRange1 Var x 751 killRange (Def' x v) = killRange2 Def' x v 752 killRange (Proj o x) = killRange1 (Proj o) x 753 killRange (Con x) = killRange1 Con x 754 killRange (Lit i l) = killRange2 Lit i l 755 killRange (QuestionMark i ii) = killRange2 QuestionMark i ii 756 killRange (Underscore i) = killRange1 Underscore i 757 killRange (Dot i e) = killRange2 Dot i e 758 killRange (App i e1 e2) = killRange3 App i e1 e2 759 killRange (WithApp i e es) = killRange3 WithApp i e es 760 killRange (Lam i b e) = killRange3 Lam i b e 761 killRange (AbsurdLam i h) = killRange2 AbsurdLam i h 762 killRange (ExtendedLam i n e d ps) = killRange5 ExtendedLam i n e d ps 763 killRange (Pi i a b) = killRange3 Pi i a b 764 killRange (Generalized s x) = killRange1 (Generalized s) x 765 killRange (Fun i a b) = killRange3 Fun i a b 766 killRange (Let i ds e) = killRange3 Let i ds e 767 killRange (Rec i fs) = killRange2 Rec i fs 768 killRange (RecUpdate i e fs) = killRange3 RecUpdate i e fs 769 killRange (ETel tel) = killRange1 ETel tel 770 killRange (ScopedExpr s e) = killRange1 (ScopedExpr s) e 771 killRange (Quote i) = killRange1 Quote i 772 killRange (QuoteTerm i) = killRange1 QuoteTerm i 773 killRange (Unquote i) = killRange1 Unquote i 774 killRange (Tactic i e xs) = killRange3 Tactic i e xs 775 killRange (DontCare e) = killRange1 DontCare e 776 killRange (PatternSyn x) = killRange1 PatternSyn x 777 killRange (Macro x) = killRange1 Macro x 778 779instance KillRange Suffix where 780 killRange = id 781 782instance KillRange Declaration where 783 killRange (Axiom p i a b c d ) = killRange4 (\i a c d -> Axiom p i a b c d) i a c d 784 killRange (Generalize s i j x e ) = killRange4 (Generalize s) i j x e 785 killRange (Field i a b ) = killRange3 Field i a b 786 killRange (Mutual i a ) = killRange2 Mutual i a 787 killRange (Section i a b c ) = killRange4 Section i a b c 788 killRange (Apply i a b c d ) = killRange5 Apply i a b c d 789 killRange (Import i a b ) = killRange3 Import i a b 790 killRange (Primitive i a b ) = killRange3 Primitive i a b 791 killRange (Pragma i a ) = Pragma (killRange i) a 792 killRange (Open i x dir ) = killRange3 Open i x dir 793 killRange (ScopedDecl a d ) = killRange1 (ScopedDecl a) d 794 killRange (FunDef i a b c ) = killRange4 FunDef i a b c 795 killRange (DataSig i a b c ) = killRange4 DataSig i a b c 796 killRange (DataDef i a b c d ) = killRange5 DataDef i a b c d 797 killRange (RecSig i a b c ) = killRange4 RecSig i a b c 798 killRange (RecDef i a b c d e f ) = killRange7 RecDef i a b c d e f 799 killRange (PatternSynDef x xs p ) = killRange3 PatternSynDef x xs p 800 killRange (UnquoteDecl mi i x e ) = killRange4 UnquoteDecl mi i x e 801 killRange (UnquoteDef i x e ) = killRange3 UnquoteDef i x e 802 803instance KillRange ModuleApplication where 804 killRange (SectionApp a b c ) = killRange3 SectionApp a b c 805 killRange (RecordModuleInstance a) = killRange1 RecordModuleInstance a 806 807instance KillRange ScopeCopyInfo where 808 killRange (ScopeCopyInfo a b) = killRange2 ScopeCopyInfo a b 809 810instance KillRange e => KillRange (Pattern' e) where 811 killRange (VarP x) = killRange1 VarP x 812 killRange (ConP i a b) = killRange3 ConP i a b 813 killRange (ProjP i o a) = killRange3 ProjP i o a 814 killRange (DefP i a b) = killRange3 DefP i a b 815 killRange (WildP i) = killRange1 WildP i 816 killRange (AsP i a b) = killRange3 AsP i a b 817 killRange (DotP i a) = killRange2 DotP i a 818 killRange (AbsurdP i) = killRange1 AbsurdP i 819 killRange (LitP i l) = killRange2 LitP i l 820 killRange (PatternSynP i a p) = killRange3 PatternSynP i a p 821 killRange (RecP i as) = killRange2 RecP i as 822 killRange (EqualP i es) = killRange2 EqualP i es 823 killRange (WithP i p) = killRange2 WithP i p 824 killRange (AnnP i a p) = killRange3 AnnP i a p 825 826instance KillRange SpineLHS where 827 killRange (SpineLHS i a b) = killRange3 SpineLHS i a b 828 829instance KillRange LHS where 830 killRange (LHS i a) = killRange2 LHS i a 831 832instance KillRange e => KillRange (LHSCore' e) where 833 killRange (LHSHead a b) = killRange2 LHSHead a b 834 killRange (LHSProj a b c) = killRange3 LHSProj a b c 835 killRange (LHSWith a b c) = killRange3 LHSWith a b c 836 837instance KillRange a => KillRange (Clause' a) where 838 killRange (Clause lhs spats rhs ds catchall) = killRange5 Clause lhs spats rhs ds catchall 839 840instance KillRange ProblemEq where 841 killRange (ProblemEq p v a) = killRange3 ProblemEq p v a 842 843instance KillRange RHS where 844 killRange AbsurdRHS = AbsurdRHS 845 killRange (RHS e c) = killRange2 RHS e c 846 killRange (WithRHS q e cs) = killRange3 WithRHS q e cs 847 killRange (RewriteRHS xes spats rhs wh) = killRange4 RewriteRHS xes spats rhs wh 848 849instance KillRange WhereDeclarations where 850 killRange (WhereDecls a b) = killRange2 WhereDecls a b 851 852instance KillRange LetBinding where 853 killRange (LetBind i info a b c) = killRange5 LetBind i info a b c 854 killRange (LetPatBind i a b ) = killRange3 LetPatBind i a b 855 killRange (LetApply i a b c d ) = killRange5 LetApply i a b c d 856 killRange (LetOpen i x dir ) = killRange3 LetOpen i x dir 857 killRange (LetDeclaredVariable x) = killRange1 LetDeclaredVariable x 858 859instance NFData Expr 860instance NFData ScopeCopyInfo 861instance NFData Declaration 862instance NFData ModuleApplication 863instance NFData Pragma 864instance NFData LetBinding 865instance NFData a => NFData (Binder' a) 866instance NFData LamBinding 867instance NFData TypedBinding 868instance NFData GeneralizeTelescope 869instance NFData DataDefParams 870instance NFData ProblemEq 871instance NFData lhs => NFData (Clause' lhs) 872instance NFData WhereDeclarations 873instance NFData RHS 874instance NFData SpineLHS 875instance NFData LHS 876instance NFData e => NFData (LHSCore' e) 877instance NFData e => NFData (Pattern' e) 878 879------------------------------------------------------------------------ 880-- Queries 881------------------------------------------------------------------------ 882 883-- class AllNames moved to Abstract.Views.DeclaredNames 884 885-- | The name defined by the given axiom. 886-- 887-- Precondition: The declaration has to be a (scoped) 'Axiom'. 888 889axiomName :: Declaration -> QName 890axiomName (Axiom _ _ _ _ q _) = q 891axiomName (ScopedDecl _ (d:_)) = axiomName d 892axiomName _ = __IMPOSSIBLE__ 893 894-- | Are we in an abstract block? 895-- 896-- In that case some definition is abstract. 897class AnyAbstract a where 898 anyAbstract :: a -> Bool 899 900instance AnyAbstract a => AnyAbstract [a] where 901 anyAbstract = Fold.any anyAbstract 902 903instance AnyAbstract Declaration where 904 anyAbstract (Axiom _ i _ _ _ _) = defAbstract i == AbstractDef 905 anyAbstract (Field i _ _) = defAbstract i == AbstractDef 906 anyAbstract (Mutual _ ds) = anyAbstract ds 907 anyAbstract (ScopedDecl _ ds) = anyAbstract ds 908 anyAbstract (Section _ _ _ ds) = anyAbstract ds 909 anyAbstract (FunDef i _ _ _) = defAbstract i == AbstractDef 910 anyAbstract (DataDef i _ _ _ _) = defAbstract i == AbstractDef 911 anyAbstract (RecDef i _ _ _ _ _ _) = defAbstract i == AbstractDef 912 anyAbstract (DataSig i _ _ _) = defAbstract i == AbstractDef 913 anyAbstract (RecSig i _ _ _) = defAbstract i == AbstractDef 914 anyAbstract _ = __IMPOSSIBLE__ 915 916-- | Turn a name into an expression. 917 918class NameToExpr a where 919 nameToExpr :: a -> Expr 920 921-- | Turn an 'AbstractName' into an expression. 922 923instance NameToExpr AbstractName where 924 nameToExpr d = 925 case anameKind d of 926 DataName -> Def x 927 RecName -> Def x 928 AxiomName -> Def x 929 PrimName -> Def x 930 FunName -> Def x 931 OtherDefName -> Def x 932 GeneralizeName -> Def x 933 DisallowedGeneralizeName -> Def x 934 FldName -> Proj ProjSystem ux 935 ConName -> Con ux 936 CoConName -> Con ux 937 PatternSynName -> PatternSyn ux 938 MacroName -> Macro x 939 QuotableName -> App (defaultAppInfo r) (Quote i) (defaultNamedArg $ Def x) 940 where 941 x = anameName d 942 ux = unambiguous x 943 r = getRange x 944 i = ExprRange r 945 946-- | Turn a 'ResolvedName' into an expression. 947-- 948-- Assumes name is not 'UnknownName'. 949 950instance NameToExpr ResolvedName where 951 nameToExpr = \case 952 VarName x _ -> Var x 953 DefinedName _ x s -> withSuffix s $ nameToExpr x -- Can be 'isDefName', 'MacroName', 'QuotableName'. 954 FieldName xs -> Proj ProjSystem . AmbQ . fmap anameName $ xs 955 ConstructorName _ xs -> Con . AmbQ . fmap anameName $ xs 956 PatternSynResName xs -> PatternSyn . AmbQ . fmap anameName $ xs 957 UnknownName -> __IMPOSSIBLE__ 958 where 959 withSuffix NoSuffix e = e 960 withSuffix s@Suffix{} (Def x) = Def' x s 961 withSuffix _ _ = __IMPOSSIBLE__ 962 963app :: Expr -> [NamedArg Expr] -> Expr 964app = foldl (App defaultAppInfo_) 965 966mkLet :: ExprInfo -> [LetBinding] -> Expr -> Expr 967mkLet _ [] e = e 968mkLet i (d:ds) e = Let i (d :| ds) e 969 970patternToExpr :: Pattern -> Expr 971patternToExpr = \case 972 VarP x -> Var (unBind x) 973 ConP _ c ps -> Con c `app` map (fmap (fmap patternToExpr)) ps 974 ProjP _ o ds -> Proj o ds 975 DefP _ fs ps -> Def (headAmbQ fs) `app` map (fmap (fmap patternToExpr)) ps 976 WildP _ -> Underscore emptyMetaInfo 977 AsP _ _ p -> patternToExpr p 978 DotP _ e -> e 979 AbsurdP _ -> Underscore emptyMetaInfo -- TODO: could this happen? 980 LitP (PatRange r) l-> Lit (ExprRange r) l 981 PatternSynP _ c ps -> PatternSyn c `app` (map . fmap . fmap) patternToExpr ps 982 RecP _ as -> Rec exprNoRange $ map (Left . fmap patternToExpr) as 983 EqualP{} -> __IMPOSSIBLE__ -- Andrea TODO: where is this used? 984 WithP r p -> __IMPOSSIBLE__ 985 AnnP _ _ p -> patternToExpr p 986 987type PatternSynDefn = ([Arg Name], Pattern' Void) 988type PatternSynDefns = Map QName PatternSynDefn 989 990lambdaLiftExpr :: [Name] -> Expr -> Expr 991lambdaLiftExpr ns e 992 = foldr 993 (\ n -> Lam exprNoRange (mkDomainFree $ defaultNamedArg $ mkBinder_ n)) 994 e 995 ns 996 997-- NOTE: This is only used on expressions that come from right-hand sides of pattern synonyms, and 998-- thus does not have to handle all forms of expressions. 999class SubstExpr a where 1000 substExpr :: [(Name, Expr)] -> a -> a 1001 1002 default substExpr 1003 :: (Functor t, SubstExpr b, t b ~ a) 1004 => [(Name, Expr)] -> a -> a 1005 substExpr = fmap . substExpr 1006 1007instance SubstExpr a => SubstExpr (Maybe a) 1008instance SubstExpr a => SubstExpr [a] 1009instance SubstExpr a => SubstExpr (List1 a) 1010instance SubstExpr a => SubstExpr (Arg a) 1011instance SubstExpr a => SubstExpr (Named name a) 1012instance SubstExpr a => SubstExpr (FieldAssignment' a) 1013 1014instance (SubstExpr a, SubstExpr b) => SubstExpr (a, b) where 1015 substExpr s (x, y) = (substExpr s x, substExpr s y) 1016 1017instance (SubstExpr a, SubstExpr b) => SubstExpr (Either a b) where 1018 substExpr s (Left x) = Left (substExpr s x) 1019 substExpr s (Right y) = Right (substExpr s y) 1020 1021instance SubstExpr C.Name where 1022 substExpr _ = id 1023 1024instance SubstExpr ModuleName where 1025 substExpr _ = id 1026 1027instance SubstExpr Expr where 1028 substExpr s e = case e of 1029 Var n -> fromMaybe e (lookup n s) 1030 Con _ -> e 1031 Proj{} -> e 1032 Def' _ _ -> e 1033 PatternSyn{} -> e 1034 Lit _ _ -> e 1035 Underscore _ -> e 1036 App i e e' -> App i (substExpr s e) (substExpr s e') 1037 Rec i nes -> Rec i (substExpr s nes) 1038 ScopedExpr si e -> ScopedExpr si (substExpr s e) 1039 -- The below cannot appear in pattern synonym right-hand sides 1040 QuestionMark{} -> __IMPOSSIBLE__ 1041 Dot{} -> __IMPOSSIBLE__ 1042 WithApp{} -> __IMPOSSIBLE__ 1043 Lam{} -> __IMPOSSIBLE__ 1044 AbsurdLam{} -> __IMPOSSIBLE__ 1045 ExtendedLam{} -> __IMPOSSIBLE__ 1046 Pi{} -> __IMPOSSIBLE__ 1047 Generalized{} -> __IMPOSSIBLE__ 1048 Fun{} -> __IMPOSSIBLE__ 1049 Let{} -> __IMPOSSIBLE__ 1050 ETel{} -> __IMPOSSIBLE__ 1051 RecUpdate{} -> __IMPOSSIBLE__ 1052 Quote{} -> __IMPOSSIBLE__ 1053 QuoteTerm{} -> __IMPOSSIBLE__ 1054 Unquote{} -> __IMPOSSIBLE__ 1055 Tactic{} -> __IMPOSSIBLE__ 1056 DontCare{} -> __IMPOSSIBLE__ 1057 Macro{} -> __IMPOSSIBLE__ 1058 1059-- TODO: more informative failure 1060insertImplicitPatSynArgs 1061 :: HasRange a 1062 => (Range -> a) 1063 -> Range 1064 -> [Arg Name] 1065 -> [NamedArg a] 1066 -> Maybe ([(Name, a)], [Arg Name]) 1067insertImplicitPatSynArgs wild r ns as = matchArgs r ns as 1068 where 1069 matchNextArg r n as@(~(a : as')) 1070 | matchNext n as = return (namedArg a, as') 1071 | visible n = Nothing 1072 | otherwise = return (wild r, as) 1073 1074 matchNext _ [] = False 1075 matchNext n (a:as) = sameHiding n a && maybe True (x ==) (bareNameOf a) 1076 where 1077 x = C.nameToRawName $ nameConcrete $ unArg n 1078 1079 matchArgs r [] [] = return ([], []) 1080 matchArgs r [] as = Nothing 1081 matchArgs r (n:ns) [] | visible n = return ([], n : ns) -- under-applied 1082 matchArgs r (n:ns) as = do 1083 (p, as) <- matchNextArg r n as 1084 first ((unArg n, p) :) <$> matchArgs (getRange p) ns as 1085