{-| The abstract syntax. This is what you get after desugaring and scope
    analysis of the concrete syntax. The type checker works on abstract syntax,
    producing internal syntax ("Agda.Syntax.Internal").
-}
module Agda.Syntax.Abstract
    ( module Agda.Syntax.Abstract
    , module Agda.Syntax.Abstract.Name
    ) where

import Prelude hiding (null)

import Control.DeepSeq

import Data.Bifunctor
import qualified Data.Foldable as Fold
import Data.Function (on)
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Maybe
import Data.Sequence (Seq, (<|), (><))
import qualified Data.Sequence as Seq
import qualified Data.Set as Set
import Data.Set (Set)
import Data.Void

import GHC.Generics (Generic)

import Agda.Syntax.Concrete (FieldAssignment'(..), exprFieldA)--, HoleContent'(..))
import qualified Agda.Syntax.Concrete as C
import Agda.Syntax.Abstract.Name
import qualified Agda.Syntax.Internal as I
import Agda.Syntax.Common
import Agda.Syntax.Info
import Agda.Syntax.Literal
import Agda.Syntax.Position
import Agda.Syntax.Scope.Base

import Agda.TypeChecking.Positivity.Occurrence

import Agda.Utils.Lens
import Agda.Utils.List1 (List1, pattern (:|))
import qualified Agda.Utils.List1 as List1
import Agda.Utils.Null
import Agda.Utils.Pretty

import Agda.Utils.Impossible

-- | A name in a binding position: we also compare the nameConcrete
-- when comparing the binders for equality.
--
-- With @--caching@ on we compare abstract syntax to determine if we can
-- reuse previous typechecking results: during that comparison two
-- names can have the same nameId but be semantically different,
-- e.g. in @{_ : A} -> ..@ vs. @{r : A} -> ..@.

newtype BindName = BindName { BindName -> Name
unBind :: Name }
  deriving (Int -> BindName -> ShowS
[BindName] -> ShowS
BindName -> ArgName
forall a.
(Int -> a -> ShowS) -> (a -> ArgName) -> ([a] -> ShowS) -> Show a
showList :: [BindName] -> ShowS
$cshowList :: [BindName] -> ShowS
show :: BindName -> ArgName
$cshow :: BindName -> ArgName
showsPrec :: Int -> BindName -> ShowS
$cshowsPrec :: Int -> BindName -> ShowS
Show, BindName -> Range
forall a. (a -> Range) -> HasRange a
getRange :: BindName -> Range
$cgetRange :: BindName -> Range
HasRange, KillRangeT BindName
forall a. KillRangeT a -> KillRange a
killRange :: KillRangeT BindName
$ckillRange :: KillRangeT BindName
KillRange, HasRange BindName
Range -> KillRangeT BindName
forall a. HasRange a -> (Range -> a -> a) -> SetRange a
setRange :: Range -> KillRangeT BindName
$csetRange :: Range -> KillRangeT BindName
SetRange, BindName -> ()
forall a. (a -> ()) -> NFData a
rnf :: BindName -> ()
$crnf :: BindName -> ()
NFData)

mkBindName :: Name -> BindName
mkBindName :: Name -> BindName
mkBindName Name
x = Name -> BindName
BindName Name
x

instance Eq BindName where
  BindName Name
n == :: BindName -> BindName -> Bool
== BindName Name
m
    = (forall a. Eq a => a -> a -> Bool
(==) forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` Name -> NameId
nameId) Name
n Name
m
      Bool -> Bool -> Bool
&& (forall a. Eq a => a -> a -> Bool
(==) forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` Name -> Name
nameConcrete) Name
n Name
m

instance Ord BindName where
  BindName Name
n compare :: BindName -> BindName -> Ordering
`compare` BindName Name
m
    = (forall a. Ord a => a -> a -> Ordering
compare forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` Name -> NameId
nameId) Name
n Name
m
      forall a. Monoid a => a -> a -> a
`mappend` (forall a. Ord a => a -> a -> Ordering
compare forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` Name -> Name
nameConcrete) Name
n Name
m

type Args = [NamedArg Expr]

-- | Types are just expressions.
-- Use this type synonym for hinting that an expression should be a type.
type Type = Expr

-- | Expressions after scope checking (operators parsed, names resolved).
data Expr
  = Var  Name                          -- ^ Bound variable.
  | Def'  QName Suffix                 -- ^ Constant: axiom, function, data or record type,
                                       --   with a possible suffix.
  | Proj ProjOrigin AmbiguousQName     -- ^ Projection (overloaded).
  | Con  AmbiguousQName                -- ^ Constructor (overloaded).
  | PatternSyn AmbiguousQName          -- ^ Pattern synonym.
  | Macro QName                        -- ^ Macro.
  | Lit ExprInfo Literal               -- ^ Literal.
  | QuestionMark MetaInfo InteractionId
    -- ^ Meta variable for interaction.
    --   The 'InteractionId' is usually identical with the
    --   'metaNumber' of 'MetaInfo'.
    --   However, if you want to print an interaction meta as
    --   just @?@ instead of @?n@, you should set the
    --   'metaNumber' to 'Nothing' while keeping the 'InteractionId'.
  | Underscore   MetaInfo
    -- ^ Meta variable for hidden argument (must be inferred locally).
  | Dot ExprInfo Expr                  -- ^ @.e@, for postfix projection.
  | App  AppInfo Expr (NamedArg Expr)  -- ^ Ordinary (binary) application.
  | WithApp ExprInfo Expr [Expr]       -- ^ With application.
  | Lam  ExprInfo LamBinding Expr      -- ^ @λ bs → e@.
  | AbsurdLam ExprInfo Hiding          -- ^ @λ()@ or @λ{}@.
  | ExtendedLam ExprInfo DefInfo Erased QName (List1 Clause)
  | Pi   ExprInfo Telescope1 Type      -- ^ Dependent function space @Γ → A@.
  | Generalized (Set QName) Type       -- ^ Like a Pi, but the ordering is not known
  | Fun  ExprInfo (Arg Type) Type      -- ^ Non-dependent function space.
  | Let  ExprInfo (List1 LetBinding) Expr
                                       -- ^ @let bs in e@.
  | Rec  ExprInfo RecordAssigns        -- ^ Record construction.
  | RecUpdate ExprInfo Expr Assigns    -- ^ Record update.
  | ScopedExpr ScopeInfo Expr          -- ^ Scope annotation.
  | Quote ExprInfo                     -- ^ Quote an identifier 'QName'.
  | QuoteTerm ExprInfo                 -- ^ Quote a term.
  | Unquote ExprInfo                   -- ^ The splicing construct: unquote ...
  | DontCare Expr                      -- ^ For printing @DontCare@ from @Syntax.Internal@.
  deriving (Int -> Expr -> ShowS
[Expr] -> ShowS
Expr -> ArgName
forall a.
(Int -> a -> ShowS) -> (a -> ArgName) -> ([a] -> ShowS) -> Show a
showList :: [Expr] -> ShowS
$cshowList :: [Expr] -> ShowS
show :: Expr -> ArgName
$cshow :: Expr -> ArgName
showsPrec :: Int -> Expr -> ShowS
$cshowsPrec :: Int -> Expr -> ShowS
Show, forall x. Rep Expr x -> Expr
forall x. Expr -> Rep Expr x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Expr x -> Expr
$cfrom :: forall x. Expr -> Rep Expr x
Generic)

-- | Pattern synonym for regular 'Def'.
pattern Def :: QName -> Expr
pattern $bDef :: QName -> Expr
$mDef :: forall {r}. Expr -> (QName -> r) -> ((# #) -> r) -> r
Def x = Def' x NoSuffix

-- | Smart constructor for 'Generalized'.
generalized :: Set QName -> Type -> Type
generalized :: Set QName -> Expr -> Expr
generalized Set QName
s Expr
e
    | forall a. Null a => a -> Bool
null Set QName
s    = Expr
e
    | Bool
otherwise = Set QName -> Expr -> Expr
Generalized Set QName
s Expr
e

-- | Record field assignment @f = e@.
type Assign  = FieldAssignment' Expr
type Assigns = [Assign]
type RecordAssign  = Either Assign ModuleName
type RecordAssigns = [RecordAssign]

-- | Renaming (generic).
type Ren a = Map a (List1 a)

data ScopeCopyInfo = ScopeCopyInfo
  { ScopeCopyInfo -> Ren ModuleName
renModules :: Ren ModuleName
  , ScopeCopyInfo -> Ren QName
renNames   :: Ren QName }
  deriving (ScopeCopyInfo -> ScopeCopyInfo -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ScopeCopyInfo -> ScopeCopyInfo -> Bool
$c/= :: ScopeCopyInfo -> ScopeCopyInfo -> Bool
== :: ScopeCopyInfo -> ScopeCopyInfo -> Bool
$c== :: ScopeCopyInfo -> ScopeCopyInfo -> Bool
Eq, Int -> ScopeCopyInfo -> ShowS
[ScopeCopyInfo] -> ShowS
ScopeCopyInfo -> ArgName
forall a.
(Int -> a -> ShowS) -> (a -> ArgName) -> ([a] -> ShowS) -> Show a
showList :: [ScopeCopyInfo] -> ShowS
$cshowList :: [ScopeCopyInfo] -> ShowS
show :: ScopeCopyInfo -> ArgName
$cshow :: ScopeCopyInfo -> ArgName
showsPrec :: Int -> ScopeCopyInfo -> ShowS
$cshowsPrec :: Int -> ScopeCopyInfo -> ShowS
Show, forall x. Rep ScopeCopyInfo x -> ScopeCopyInfo
forall x. ScopeCopyInfo -> Rep ScopeCopyInfo x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep ScopeCopyInfo x -> ScopeCopyInfo
$cfrom :: forall x. ScopeCopyInfo -> Rep ScopeCopyInfo x
Generic)

initCopyInfo :: ScopeCopyInfo
initCopyInfo :: ScopeCopyInfo
initCopyInfo = ScopeCopyInfo
  { renModules :: Ren ModuleName
renModules = forall a. Monoid a => a
mempty
  , renNames :: Ren QName
renNames   = forall a. Monoid a => a
mempty
  }

instance Pretty ScopeCopyInfo where
  pretty :: ScopeCopyInfo -> Doc
pretty ScopeCopyInfo
i = forall (t :: * -> *). Foldable t => t Doc -> Doc
vcat [ forall {l} {a}.
(IsList l, Pretty a, Pretty (Item l)) =>
ArgName -> Map a l -> Doc
prRen ArgName
"renModules =" (ScopeCopyInfo -> Ren ModuleName
renModules ScopeCopyInfo
i)
                  , forall {l} {a}.
(IsList l, Pretty a, Pretty (Item l)) =>
ArgName -> Map a l -> Doc
prRen ArgName
"renNames   =" (ScopeCopyInfo -> Ren QName
renNames ScopeCopyInfo
i) ]
    where
      prRen :: ArgName -> Map a l -> Doc
prRen ArgName
s Map a l
r = forall (t :: * -> *). Foldable t => t Doc -> Doc
sep [ ArgName -> Doc
text ArgName
s, Int -> Doc -> Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *). Foldable t => t Doc -> Doc
vcat (forall a b. (a -> b) -> [a] -> [b]
map forall {a} {a}. (Pretty a, Pretty a) => (a, a) -> Doc
pr [(a, Item l)]
xs) ]
        where
          xs :: [(a, Item l)]
xs = [ (a
k, Item l
v) | (a
k, l
vs) <- forall k a. Map k a -> [(k, a)]
Map.toList Map a l
r, Item l
v <- forall l. IsList l => l -> [Item l]
List1.toList l
vs ]
      pr :: (a, a) -> Doc
pr (a
x, a
y) = forall a. Pretty a => a -> Doc
pretty a
x Doc -> Doc -> Doc
<+> Doc
"->" Doc -> Doc -> Doc
<+> forall a. Pretty a => a -> Doc
pretty a
y

type RecordDirectives = RecordDirectives' QName

data Declaration
  = Axiom      KindOfName DefInfo ArgInfo (Maybe [Occurrence]) QName Type
    -- ^ Type signature (can be irrelevant, but not hidden).
    --
    -- The fourth argument contains an optional assignment of
    -- polarities to arguments.
  | Generalize (Set QName) DefInfo ArgInfo QName Type
    -- ^ First argument is set of generalizable variables used in the type.
  | Field      DefInfo QName (Arg Type)              -- ^ record field
  | Primitive  DefInfo QName (Arg Type)              -- ^ primitive function
  | Mutual     MutualInfo [Declaration]              -- ^ a bunch of mutually recursive definitions
  | Section    Range ModuleName GeneralizeTelescope [Declaration]
  | Apply      ModuleInfo ModuleName ModuleApplication ScopeCopyInfo ImportDirective
    -- ^ The @ImportDirective@ is for highlighting purposes.
  | Import     ModuleInfo ModuleName ImportDirective
    -- ^ The @ImportDirective@ is for highlighting purposes.
  | Pragma     Range      Pragma
  | Open       ModuleInfo ModuleName ImportDirective
    -- ^ only retained for highlighting purposes
  | FunDef     DefInfo QName Delayed [Clause] -- ^ sequence of function clauses
  | DataSig    DefInfo QName GeneralizeTelescope Type -- ^ lone data signature
  | DataDef    DefInfo QName UniverseCheck DataDefParams [Constructor]
  | RecSig     DefInfo QName GeneralizeTelescope Type -- ^ lone record signature
  | RecDef     DefInfo QName UniverseCheck RecordDirectives DataDefParams Type [Declaration]
      -- ^ The 'Type' gives the constructor type telescope, @(x1 : A1)..(xn : An) -> Prop@,
      --   and the optional name is the constructor's name.
      --   The optional 'Range' is for the @pattern@ attribute.
  | PatternSynDef QName [Arg BindName] (Pattern' Void)
      -- ^ Only for highlighting purposes
  | UnquoteDecl MutualInfo [DefInfo] [QName] Expr
  | UnquoteDef  [DefInfo] [QName] Expr
  | UnquoteData [DefInfo] QName UniverseCheck [DefInfo] [QName] Expr
  | ScopedDecl ScopeInfo [Declaration]  -- ^ scope annotation
  deriving (Int -> Declaration -> ShowS
[Declaration] -> ShowS
Declaration -> ArgName
forall a.
(Int -> a -> ShowS) -> (a -> ArgName) -> ([a] -> ShowS) -> Show a
showList :: [Declaration] -> ShowS
$cshowList :: [Declaration] -> ShowS
show :: Declaration -> ArgName
$cshow :: Declaration -> ArgName
showsPrec :: Int -> Declaration -> ShowS
$cshowsPrec :: Int -> Declaration -> ShowS
Show, forall x. Rep Declaration x -> Declaration
forall x. Declaration -> Rep Declaration x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Declaration x -> Declaration
$cfrom :: forall x. Declaration -> Rep Declaration x
Generic)

type DefInfo = DefInfo' Expr

type ImportDirective = ImportDirective' QName ModuleName
type Renaming        = Renaming'        QName ModuleName
type ImportedName    = ImportedName'    QName ModuleName

data ModuleApplication
    = SectionApp Telescope ModuleName [NamedArg Expr]
      -- ^ @tel. M args@:  applies @M@ to @args@ and abstracts @tel@.
    | RecordModuleInstance ModuleName
      -- ^ @M {{...}}@
  deriving (Int -> ModuleApplication -> ShowS
[ModuleApplication] -> ShowS
ModuleApplication -> ArgName
forall a.
(Int -> a -> ShowS) -> (a -> ArgName) -> ([a] -> ShowS) -> Show a
showList :: [ModuleApplication] -> ShowS
$cshowList :: [ModuleApplication] -> ShowS
show :: ModuleApplication -> ArgName
$cshow :: ModuleApplication -> ArgName
showsPrec :: Int -> ModuleApplication -> ShowS
$cshowsPrec :: Int -> ModuleApplication -> ShowS
Show, ModuleApplication -> ModuleApplication -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ModuleApplication -> ModuleApplication -> Bool
$c/= :: ModuleApplication -> ModuleApplication -> Bool
== :: ModuleApplication -> ModuleApplication -> Bool
$c== :: ModuleApplication -> ModuleApplication -> Bool
Eq, forall x. Rep ModuleApplication x -> ModuleApplication
forall x. ModuleApplication -> Rep ModuleApplication x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep ModuleApplication x -> ModuleApplication
$cfrom :: forall x. ModuleApplication -> Rep ModuleApplication x
Generic)

data Pragma
  = OptionsPragma [String]
  | BuiltinPragma RString ResolvedName
    -- ^ 'ResolvedName' is not 'UnknownName'.
    --   Name can be ambiguous e.g. for built-in constructors.
  | BuiltinNoDefPragma RString KindOfName QName
    -- ^ Builtins that do not come with a definition,
    --   but declare a name for an Agda concept.
  | RewritePragma Range [QName]
    -- ^ Range is range of REWRITE keyword.
  | CompilePragma RString QName String
  | StaticPragma QName
  | EtaPragma QName
    -- ^ For coinductive records, use pragma instead of regular
    --   @eta-equality@ definition (as it is might make Agda loop).
  | InjectivePragma QName
  | InlinePragma Bool QName -- INLINE or NOINLINE
  | NotProjectionLikePragma QName
    -- Mark the definition as not being projection-like
  | DisplayPragma QName [NamedArg Pattern] Expr
  deriving (Int -> Pragma -> ShowS
[Pragma] -> ShowS
Pragma -> ArgName
forall a.
(Int -> a -> ShowS) -> (a -> ArgName) -> ([a] -> ShowS) -> Show a
showList :: [Pragma] -> ShowS
$cshowList :: [Pragma] -> ShowS
show :: Pragma -> ArgName
$cshow :: Pragma -> ArgName
showsPrec :: Int -> Pragma -> ShowS
$cshowsPrec :: Int -> Pragma -> ShowS
Show, Pragma -> Pragma -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Pragma -> Pragma -> Bool
$c/= :: Pragma -> Pragma -> Bool
== :: Pragma -> Pragma -> Bool
$c== :: Pragma -> Pragma -> Bool
Eq, forall x. Rep Pragma x -> Pragma
forall x. Pragma -> Rep Pragma x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Pragma x -> Pragma
$cfrom :: forall x. Pragma -> Rep Pragma x
Generic)

-- | Bindings that are valid in a @let@.
data LetBinding
  = LetBind LetInfo ArgInfo BindName Type Expr
    -- ^ @LetBind info rel name type defn@
  | LetPatBind LetInfo Pattern Expr
    -- ^ Irrefutable pattern binding.
  | LetApply ModuleInfo ModuleName ModuleApplication ScopeCopyInfo ImportDirective
    -- ^ @LetApply mi newM (oldM args) renamings dir@.
    -- The @ImportDirective@ is for highlighting purposes.
  | LetOpen ModuleInfo ModuleName ImportDirective
    -- ^ only for highlighting and abstractToConcrete
  | LetDeclaredVariable BindName
    -- ^ Only used for highlighting. Refers to the first occurrence of
    -- @x@ in @let x : A; x = e@.
  deriving (Int -> LetBinding -> ShowS
[LetBinding] -> ShowS
LetBinding -> ArgName
forall a.
(Int -> a -> ShowS) -> (a -> ArgName) -> ([a] -> ShowS) -> Show a
showList :: [LetBinding] -> ShowS
$cshowList :: [LetBinding] -> ShowS
show :: LetBinding -> ArgName
$cshow :: LetBinding -> ArgName
showsPrec :: Int -> LetBinding -> ShowS
$cshowsPrec :: Int -> LetBinding -> ShowS
Show, LetBinding -> LetBinding -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: LetBinding -> LetBinding -> Bool
$c/= :: LetBinding -> LetBinding -> Bool
== :: LetBinding -> LetBinding -> Bool
$c== :: LetBinding -> LetBinding -> Bool
Eq, forall x. Rep LetBinding x -> LetBinding
forall x. LetBinding -> Rep LetBinding x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep LetBinding x -> LetBinding
$cfrom :: forall x. LetBinding -> Rep LetBinding x
Generic)

-- | Only 'Axiom's.
type TypeSignature  = Declaration
type Constructor    = TypeSignature
type Field          = TypeSignature

type TacticAttr = Maybe Expr

-- A Binder @x\@p@, the pattern is optional
data Binder' a = Binder
  { forall a. Binder' a -> Maybe Pattern
binderPattern :: Maybe Pattern
  , forall a. Binder' a -> a
binderName    :: a
  } deriving (Int -> Binder' a -> ShowS
forall a. Show a => Int -> Binder' a -> ShowS
forall a. Show a => [Binder' a] -> ShowS
forall a. Show a => Binder' a -> ArgName
forall a.
(Int -> a -> ShowS) -> (a -> ArgName) -> ([a] -> ShowS) -> Show a
showList :: [Binder' a] -> ShowS
$cshowList :: forall a. Show a => [Binder' a] -> ShowS
show :: Binder' a -> ArgName
$cshow :: forall a. Show a => Binder' a -> ArgName
showsPrec :: Int -> Binder' a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> Binder' a -> ShowS
Show, Binder' a -> Binder' a -> Bool
forall a. Eq a => Binder' a -> Binder' a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Binder' a -> Binder' a -> Bool
$c/= :: forall a. Eq a => Binder' a -> Binder' a -> Bool
== :: Binder' a -> Binder' a -> Bool
$c== :: forall a. Eq a => Binder' a -> Binder' a -> Bool
Eq, forall a b. a -> Binder' b -> Binder' a
forall a b. (a -> b) -> Binder' a -> Binder' b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> Binder' b -> Binder' a
$c<$ :: forall a b. a -> Binder' b -> Binder' a
fmap :: forall a b. (a -> b) -> Binder' a -> Binder' b
$cfmap :: forall a b. (a -> b) -> Binder' a -> Binder' b
Functor, forall a. Eq a => a -> Binder' a -> Bool
forall a. Num a => Binder' a -> a
forall a. Ord a => Binder' a -> a
forall m. Monoid m => Binder' m -> m
forall a. Binder' a -> Bool
forall a. Binder' a -> Int
forall a. Binder' a -> [a]
forall a. (a -> a -> a) -> Binder' a -> a
forall m a. Monoid m => (a -> m) -> Binder' a -> m
forall b a. (b -> a -> b) -> b -> Binder' a -> b
forall a b. (a -> b -> b) -> b -> Binder' a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
product :: forall a. Num a => Binder' a -> a
$cproduct :: forall a. Num a => Binder' a -> a
sum :: forall a. Num a => Binder' a -> a
$csum :: forall a. Num a => Binder' a -> a
minimum :: forall a. Ord a => Binder' a -> a
$cminimum :: forall a. Ord a => Binder' a -> a
maximum :: forall a. Ord a => Binder' a -> a
$cmaximum :: forall a. Ord a => Binder' a -> a
elem :: forall a. Eq a => a -> Binder' a -> Bool
$celem :: forall a. Eq a => a -> Binder' a -> Bool
length :: forall a. Binder' a -> Int
$clength :: forall a. Binder' a -> Int
null :: forall a. Binder' a -> Bool
$cnull :: forall a. Binder' a -> Bool
toList :: forall a. Binder' a -> [a]
$ctoList :: forall a. Binder' a -> [a]
foldl1 :: forall a. (a -> a -> a) -> Binder' a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> Binder' a -> a
foldr1 :: forall a. (a -> a -> a) -> Binder' a -> a
$cfoldr1 :: forall a. (a -> a -> a) -> Binder' a -> a
foldl' :: forall b a. (b -> a -> b) -> b -> Binder' a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> Binder' a -> b
foldl :: forall b a. (b -> a -> b) -> b -> Binder' a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> Binder' a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> Binder' a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> Binder' a -> b
foldr :: forall a b. (a -> b -> b) -> b -> Binder' a -> b
$cfoldr :: forall a b. (a -> b -> b) -> b -> Binder' a -> b
foldMap' :: forall m a. Monoid m => (a -> m) -> Binder' a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> Binder' a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> Binder' a -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> Binder' a -> m
fold :: forall m. Monoid m => Binder' m -> m
$cfold :: forall m. Monoid m => Binder' m -> m
Foldable, Functor Binder'
Foldable Binder'
forall (t :: * -> *).
Functor t
-> Foldable t
-> (forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: * -> *) a. Monad m => Binder' (m a) -> m (Binder' a)
forall (f :: * -> *) a.
Applicative f =>
Binder' (f a) -> f (Binder' a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Binder' a -> m (Binder' b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Binder' a -> f (Binder' b)
sequence :: forall (m :: * -> *) a. Monad m => Binder' (m a) -> m (Binder' a)
$csequence :: forall (m :: * -> *) a. Monad m => Binder' (m a) -> m (Binder' a)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Binder' a -> m (Binder' b)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Binder' a -> m (Binder' b)
sequenceA :: forall (f :: * -> *) a.
Applicative f =>
Binder' (f a) -> f (Binder' a)
$csequenceA :: forall (f :: * -> *) a.
Applicative f =>
Binder' (f a) -> f (Binder' a)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Binder' a -> f (Binder' b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Binder' a -> f (Binder' b)
Traversable, forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (Binder' a) x -> Binder' a
forall a x. Binder' a -> Rep (Binder' a) x
$cto :: forall a x. Rep (Binder' a) x -> Binder' a
$cfrom :: forall a x. Binder' a -> Rep (Binder' a) x
Generic)

type Binder = Binder' BindName

mkBinder :: a -> Binder' a
mkBinder :: forall a. a -> Binder' a
mkBinder = forall a. Maybe Pattern -> a -> Binder' a
Binder forall a. Maybe a
Nothing

mkBinder_ :: Name -> Binder
mkBinder_ :: Name -> Binder
mkBinder_ = forall a. a -> Binder' a
mkBinder forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> BindName
mkBindName

extractPattern :: Binder' a -> Maybe (Pattern, a)
extractPattern :: forall a. Binder' a -> Maybe (Pattern, a)
extractPattern (Binder Maybe Pattern
p a
a) = (,a
a) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Pattern
p

-- | A lambda binding is either domain free or typed.
data LamBinding
  = DomainFree TacticAttr (NamedArg Binder)
    -- ^ . @x@ or @{x}@ or @.x@ or @{x = y}@ or @x\@p@ or @(p)@
  | DomainFull TypedBinding
    -- ^ . @(xs:e)@ or @{xs:e}@ or @(let Ds)@
  deriving (Int -> LamBinding -> ShowS
[LamBinding] -> ShowS
LamBinding -> ArgName
forall a.
(Int -> a -> ShowS) -> (a -> ArgName) -> ([a] -> ShowS) -> Show a
showList :: [LamBinding] -> ShowS
$cshowList :: [LamBinding] -> ShowS
show :: LamBinding -> ArgName
$cshow :: LamBinding -> ArgName
showsPrec :: Int -> LamBinding -> ShowS
$cshowsPrec :: Int -> LamBinding -> ShowS
Show, LamBinding -> LamBinding -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: LamBinding -> LamBinding -> Bool
$c/= :: LamBinding -> LamBinding -> Bool
== :: LamBinding -> LamBinding -> Bool
$c== :: LamBinding -> LamBinding -> Bool
Eq, forall x. Rep LamBinding x -> LamBinding
forall x. LamBinding -> Rep LamBinding x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep LamBinding x -> LamBinding
$cfrom :: forall x. LamBinding -> Rep LamBinding x
Generic)

mkDomainFree :: NamedArg Binder -> LamBinding
mkDomainFree :: NamedArg Binder -> LamBinding
mkDomainFree = TacticAttr -> NamedArg Binder -> LamBinding
DomainFree forall a. Maybe a
Nothing

-- | Extra information that is attached to a typed binding, that plays a
-- role during type checking but strictly speaking is not part of the
-- @name : type@" relation which a makes up a binding.
data TypedBindingInfo
  = TypedBindingInfo
    { TypedBindingInfo -> TacticAttr
tbTacticAttr :: TacticAttr
      -- ^ Does this binding have a tactic annotation?
    , TypedBindingInfo -> Bool
tbFinite     :: Bool
      -- ^ Does this binding correspond to a Partial binder, rather than
      -- to a Pi binder? Must be present here to be reflected into
      -- abstract syntax later (and to be printed to the user later).
    }
  deriving (Int -> TypedBindingInfo -> ShowS
[TypedBindingInfo] -> ShowS
TypedBindingInfo -> ArgName
forall a.
(Int -> a -> ShowS) -> (a -> ArgName) -> ([a] -> ShowS) -> Show a
showList :: [TypedBindingInfo] -> ShowS
$cshowList :: [TypedBindingInfo] -> ShowS
show :: TypedBindingInfo -> ArgName
$cshow :: TypedBindingInfo -> ArgName
showsPrec :: Int -> TypedBindingInfo -> ShowS
$cshowsPrec :: Int -> TypedBindingInfo -> ShowS
Show, TypedBindingInfo -> TypedBindingInfo -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: TypedBindingInfo -> TypedBindingInfo -> Bool
$c/= :: TypedBindingInfo -> TypedBindingInfo -> Bool
== :: TypedBindingInfo -> TypedBindingInfo -> Bool
$c== :: TypedBindingInfo -> TypedBindingInfo -> Bool
Eq, forall x. Rep TypedBindingInfo x -> TypedBindingInfo
forall x. TypedBindingInfo -> Rep TypedBindingInfo x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep TypedBindingInfo x -> TypedBindingInfo
$cfrom :: forall x. TypedBindingInfo -> Rep TypedBindingInfo x
Generic)

defaultTbInfo :: TypedBindingInfo
defaultTbInfo :: TypedBindingInfo
defaultTbInfo = TypedBindingInfo
  { tbTacticAttr :: TacticAttr
tbTacticAttr = forall a. Maybe a
Nothing
  , tbFinite :: Bool
tbFinite = Bool
False
  }

-- | A typed binding.  Appears in dependent function spaces, typed lambdas, and
--   telescopes.  It might be tempting to simplify this to only bind a single
--   name at a time, and translate, say, @(x y : A)@ to @(x : A)(y : A)@
--   before type-checking.  However, this would be slightly problematic:
--
--     1. We would have to typecheck the type @A@ several times.
--
--     2. If @A@ contains a meta variable or hole, it would be duplicated
--        by such a translation.
--
--   While 1. is only slightly inefficient, 2. would be an outright bug.
--   Duplicating @A@ could not be done naively, we would have to make sure
--   that the metas of the copy are aliases of the metas of the original.

data TypedBinding
  = TBind Range TypedBindingInfo (List1 (NamedArg Binder)) Type
    -- ^ As in telescope @(x y z : A)@ or type @(x y z : A) -> B@.
  | TLet Range (List1 LetBinding)
    -- ^ E.g. @(let x = e)@ or @(let open M)@.
  deriving (Int -> TypedBinding -> ShowS
Telescope -> ShowS
TypedBinding -> ArgName
forall a.
(Int -> a -> ShowS) -> (a -> ArgName) -> ([a] -> ShowS) -> Show a
showList :: Telescope -> ShowS
$cshowList :: Telescope -> ShowS
show :: TypedBinding -> ArgName
$cshow :: TypedBinding -> ArgName
showsPrec :: Int -> TypedBinding -> ShowS
$cshowsPrec :: Int -> TypedBinding -> ShowS
Show, TypedBinding -> TypedBinding -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: TypedBinding -> TypedBinding -> Bool
$c/= :: TypedBinding -> TypedBinding -> Bool
== :: TypedBinding -> TypedBinding -> Bool
$c== :: TypedBinding -> TypedBinding -> Bool
Eq, forall x. Rep TypedBinding x -> TypedBinding
forall x. TypedBinding -> Rep TypedBinding x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep TypedBinding x -> TypedBinding
$cfrom :: forall x. TypedBinding -> Rep TypedBinding x
Generic)

mkTBind :: Range -> List1 (NamedArg Binder) -> Type -> TypedBinding
mkTBind :: Range -> List1 (NamedArg Binder) -> Expr -> TypedBinding
mkTBind Range
r = Range
-> TypedBindingInfo
-> List1 (NamedArg Binder)
-> Expr
-> TypedBinding
TBind Range
r TypedBindingInfo
defaultTbInfo

mkTLet :: Range -> [LetBinding] -> Maybe TypedBinding
mkTLet :: Range -> [LetBinding] -> Maybe TypedBinding
mkTLet Range
_ []     = forall a. Maybe a
Nothing
mkTLet Range
r (LetBinding
d:[LetBinding]
ds) = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Range -> List1 LetBinding -> TypedBinding
TLet Range
r (LetBinding
d forall a. a -> [a] -> NonEmpty a
:| [LetBinding]
ds)

type Telescope1 = List1 TypedBinding
type Telescope  = [TypedBinding]

mkPi :: ExprInfo -> Telescope -> Type -> Type
mkPi :: ExprInfo -> Telescope -> Expr -> Expr
mkPi ExprInfo
i []     Expr
e = Expr
e
mkPi ExprInfo
i (TypedBinding
x:Telescope
xs) Expr
e = ExprInfo -> Telescope1 -> Expr -> Expr
Pi ExprInfo
i (TypedBinding
x forall a. a -> [a] -> NonEmpty a
:| Telescope
xs) Expr
e

data GeneralizeTelescope = GeneralizeTel
  { GeneralizeTelescope -> Map QName Name
generalizeTelVars :: Map QName Name
    -- ^ Maps generalize variables to the corresponding bound variable (to be
    --   introduced by the generalisation).
  , GeneralizeTelescope -> Telescope
generalizeTel     :: Telescope }
  deriving (Int -> GeneralizeTelescope -> ShowS
[GeneralizeTelescope] -> ShowS
GeneralizeTelescope -> ArgName
forall a.
(Int -> a -> ShowS) -> (a -> ArgName) -> ([a] -> ShowS) -> Show a
showList :: [GeneralizeTelescope] -> ShowS
$cshowList :: [GeneralizeTelescope] -> ShowS
show :: GeneralizeTelescope -> ArgName
$cshow :: GeneralizeTelescope -> ArgName
showsPrec :: Int -> GeneralizeTelescope -> ShowS
$cshowsPrec :: Int -> GeneralizeTelescope -> ShowS
Show, GeneralizeTelescope -> GeneralizeTelescope -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: GeneralizeTelescope -> GeneralizeTelescope -> Bool
$c/= :: GeneralizeTelescope -> GeneralizeTelescope -> Bool
== :: GeneralizeTelescope -> GeneralizeTelescope -> Bool
$c== :: GeneralizeTelescope -> GeneralizeTelescope -> Bool
Eq, forall x. Rep GeneralizeTelescope x -> GeneralizeTelescope
forall x. GeneralizeTelescope -> Rep GeneralizeTelescope x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep GeneralizeTelescope x -> GeneralizeTelescope
$cfrom :: forall x. GeneralizeTelescope -> Rep GeneralizeTelescope x
Generic)

data DataDefParams = DataDefParams
  { DataDefParams -> Set Name
dataDefGeneralizedParams :: Set Name
    -- ^ We don't yet know the position of generalized parameters from the data
    --   sig, so we keep these in a set on the side.
  , DataDefParams -> [LamBinding]
dataDefParams :: [LamBinding]
  }
  deriving (Int -> DataDefParams -> ShowS
[DataDefParams] -> ShowS
DataDefParams -> ArgName
forall a.
(Int -> a -> ShowS) -> (a -> ArgName) -> ([a] -> ShowS) -> Show a
showList :: [DataDefParams] -> ShowS
$cshowList :: [DataDefParams] -> ShowS
show :: DataDefParams -> ArgName
$cshow :: DataDefParams -> ArgName
showsPrec :: Int -> DataDefParams -> ShowS
$cshowsPrec :: Int -> DataDefParams -> ShowS
Show, DataDefParams -> DataDefParams -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: DataDefParams -> DataDefParams -> Bool
$c/= :: DataDefParams -> DataDefParams -> Bool
== :: DataDefParams -> DataDefParams -> Bool
$c== :: DataDefParams -> DataDefParams -> Bool
Eq, forall x. Rep DataDefParams x -> DataDefParams
forall x. DataDefParams -> Rep DataDefParams x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep DataDefParams x -> DataDefParams
$cfrom :: forall x. DataDefParams -> Rep DataDefParams x
Generic)

noDataDefParams :: DataDefParams
noDataDefParams :: DataDefParams
noDataDefParams = Set Name -> [LamBinding] -> DataDefParams
DataDefParams forall a. Set a
Set.empty []

-- | A user pattern together with an internal term that it should be equal to
--   after splitting is complete.
--   Special cases:
--    * User pattern is a variable but internal term isn't:
--      this will be turned into an as pattern.
--    * User pattern is a dot pattern:
--      this pattern won't trigger any splitting but will be checked
--      for equality after all splitting is complete and as patterns have
--      been bound.
--    * User pattern is an absurd pattern:
--      emptiness of the type will be checked after splitting is complete.
--    * User pattern is an annotated wildcard:
--      type annotation will be checked after splitting is complete.
data ProblemEq = ProblemEq
  { ProblemEq -> Pattern
problemInPat :: Pattern
  , ProblemEq -> Term
problemInst  :: I.Term
  , ProblemEq -> Dom Type
problemType  :: I.Dom I.Type
  } deriving (Int -> ProblemEq -> ShowS
[ProblemEq] -> ShowS
ProblemEq -> ArgName
forall a.
(Int -> a -> ShowS) -> (a -> ArgName) -> ([a] -> ShowS) -> Show a
showList :: [ProblemEq] -> ShowS
$cshowList :: [ProblemEq] -> ShowS
show :: ProblemEq -> ArgName
$cshow :: ProblemEq -> ArgName
showsPrec :: Int -> ProblemEq -> ShowS
$cshowsPrec :: Int -> ProblemEq -> ShowS
Show, forall x. Rep ProblemEq x -> ProblemEq
forall x. ProblemEq -> Rep ProblemEq x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep ProblemEq x -> ProblemEq
$cfrom :: forall x. ProblemEq -> Rep ProblemEq x
Generic)

-- These are not relevant for caching purposes
instance Eq ProblemEq where ProblemEq
_ == :: ProblemEq -> ProblemEq -> Bool
== ProblemEq
_ = Bool
True

-- | We could throw away @where@ clauses at this point and translate them to
--   @let@. It's not obvious how to remember that the @let@ was really a
--   @where@ clause though, so for the time being we keep it here.
data Clause' lhs = Clause
  { forall lhs. Clause' lhs -> lhs
clauseLHS        :: lhs
  , forall lhs. Clause' lhs -> [ProblemEq]
clauseStrippedPats :: [ProblemEq]
      -- ^ Only in with-clauses where we inherit some already checked patterns from the parent.
      --   These live in the context of the parent clause left-hand side.
  , forall lhs. Clause' lhs -> RHS
clauseRHS        :: RHS
  , forall lhs. Clause' lhs -> WhereDeclarations
clauseWhereDecls :: WhereDeclarations
  , forall lhs. Clause' lhs -> Bool
clauseCatchall   :: Bool
  } deriving (Int -> Clause' lhs -> ShowS
forall lhs. Show lhs => Int -> Clause' lhs -> ShowS
forall lhs. Show lhs => [Clause' lhs] -> ShowS
forall lhs. Show lhs => Clause' lhs -> ArgName
forall a.
(Int -> a -> ShowS) -> (a -> ArgName) -> ([a] -> ShowS) -> Show a
showList :: [Clause' lhs] -> ShowS
$cshowList :: forall lhs. Show lhs => [Clause' lhs] -> ShowS
show :: Clause' lhs -> ArgName
$cshow :: forall lhs. Show lhs => Clause' lhs -> ArgName
showsPrec :: Int -> Clause' lhs -> ShowS
$cshowsPrec :: forall lhs. Show lhs => Int -> Clause' lhs -> ShowS
Show, forall a b. a -> Clause' b -> Clause' a
forall a b. (a -> b) -> Clause' a -> Clause' b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> Clause' b -> Clause' a
$c<$ :: forall a b. a -> Clause' b -> Clause' a
fmap :: forall a b. (a -> b) -> Clause' a -> Clause' b
$cfmap :: forall a b. (a -> b) -> Clause' a -> Clause' b
Functor, forall a. Eq a => a -> Clause' a -> Bool
forall a. Num a => Clause' a -> a
forall a. Ord a => Clause' a -> a
forall m. Monoid m => Clause' m -> m
forall lhs. Clause' lhs -> Bool
forall a. Clause' a -> Int
forall a. Clause' a -> [a]
forall a. (a -> a -> a) -> Clause' a -> a
forall m a. Monoid m => (a -> m) -> Clause' a -> m
forall b a. (b -> a -> b) -> b -> Clause' a -> b
forall a b. (a -> b -> b) -> b -> Clause' a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
product :: forall a. Num a => Clause' a -> a
$cproduct :: forall a. Num a => Clause' a -> a
sum :: forall a. Num a => Clause' a -> a
$csum :: forall a. Num a => Clause' a -> a
minimum :: forall a. Ord a => Clause' a -> a
$cminimum :: forall a. Ord a => Clause' a -> a
maximum :: forall a. Ord a => Clause' a -> a
$cmaximum :: forall a. Ord a => Clause' a -> a
elem :: forall a. Eq a => a -> Clause' a -> Bool
$celem :: forall a. Eq a => a -> Clause' a -> Bool
length :: forall a. Clause' a -> Int
$clength :: forall a. Clause' a -> Int
null :: forall lhs. Clause' lhs -> Bool
$cnull :: forall lhs. Clause' lhs -> Bool
toList :: forall a. Clause' a -> [a]
$ctoList :: forall a. Clause' a -> [a]
foldl1 :: forall a. (a -> a -> a) -> Clause' a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> Clause' a -> a
foldr1 :: forall a. (a -> a -> a) -> Clause' a -> a
$cfoldr1 :: forall a. (a -> a -> a) -> Clause' a -> a
foldl' :: forall b a. (b -> a -> b) -> b -> Clause' a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> Clause' a -> b
foldl :: forall b a. (b -> a -> b) -> b -> Clause' a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> Clause' a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> Clause' a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> Clause' a -> b
foldr :: forall a b. (a -> b -> b) -> b -> Clause' a -> b
$cfoldr :: forall a b. (a -> b -> b) -> b -> Clause' a -> b
foldMap' :: forall m a. Monoid m => (a -> m) -> Clause' a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> Clause' a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> Clause' a -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> Clause' a -> m
fold :: forall m. Monoid m => Clause' m -> m
$cfold :: forall m. Monoid m => Clause' m -> m
Foldable, Functor Clause'
Foldable Clause'
forall (t :: * -> *).
Functor t
-> Foldable t
-> (forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: * -> *) a. Monad m => Clause' (m a) -> m (Clause' a)
forall (f :: * -> *) a.
Applicative f =>
Clause' (f a) -> f (Clause' a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Clause' a -> m (Clause' b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Clause' a -> f (Clause' b)
sequence :: forall (m :: * -> *) a. Monad m => Clause' (m a) -> m (Clause' a)
$csequence :: forall (m :: * -> *) a. Monad m => Clause' (m a) -> m (Clause' a)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Clause' a -> m (Clause' b)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Clause' a -> m (Clause' b)
sequenceA :: forall (f :: * -> *) a.
Applicative f =>
Clause' (f a) -> f (Clause' a)
$csequenceA :: forall (f :: * -> *) a.
Applicative f =>
Clause' (f a) -> f (Clause' a)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Clause' a -> f (Clause' b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Clause' a -> f (Clause' b)
Traversable, Clause' lhs -> Clause' lhs -> Bool
forall lhs. Eq lhs => Clause' lhs -> Clause' lhs -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Clause' lhs -> Clause' lhs -> Bool
$c/= :: forall lhs. Eq lhs => Clause' lhs -> Clause' lhs -> Bool
== :: Clause' lhs -> Clause' lhs -> Bool
$c== :: forall lhs. Eq lhs => Clause' lhs -> Clause' lhs -> Bool
Eq, forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall lhs x. Rep (Clause' lhs) x -> Clause' lhs
forall lhs x. Clause' lhs -> Rep (Clause' lhs) x
$cto :: forall lhs x. Rep (Clause' lhs) x -> Clause' lhs
$cfrom :: forall lhs x. Clause' lhs -> Rep (Clause' lhs) x
Generic)

data WhereDeclarations = WhereDecls
  { WhereDeclarations -> Maybe ModuleName
whereModule :: Maybe ModuleName
      -- #2897: we need to restrict named where modules in refined contexts,
      --        so remember whether it was named here
  , WhereDeclarations -> Bool
whereAnywhere :: Bool
      -- ^ is it an ordinary unnamed @where@?
  , WhereDeclarations -> Maybe Declaration
whereDecls :: Maybe Declaration
      -- ^ The declaration is a 'Section'.
  } deriving (Int -> WhereDeclarations -> ShowS
[WhereDeclarations] -> ShowS
WhereDeclarations -> ArgName
forall a.
(Int -> a -> ShowS) -> (a -> ArgName) -> ([a] -> ShowS) -> Show a
showList :: [WhereDeclarations] -> ShowS
$cshowList :: [WhereDeclarations] -> ShowS
show :: WhereDeclarations -> ArgName
$cshow :: WhereDeclarations -> ArgName
showsPrec :: Int -> WhereDeclarations -> ShowS
$cshowsPrec :: Int -> WhereDeclarations -> ShowS
Show, WhereDeclarations -> WhereDeclarations -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: WhereDeclarations -> WhereDeclarations -> Bool
$c/= :: WhereDeclarations -> WhereDeclarations -> Bool
== :: WhereDeclarations -> WhereDeclarations -> Bool
$c== :: WhereDeclarations -> WhereDeclarations -> Bool
Eq, forall x. Rep WhereDeclarations x -> WhereDeclarations
forall x. WhereDeclarations -> Rep WhereDeclarations x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep WhereDeclarations x -> WhereDeclarations
$cfrom :: forall x. WhereDeclarations -> Rep WhereDeclarations x
Generic)

instance Null WhereDeclarations where
  empty :: WhereDeclarations
empty = Maybe ModuleName -> Bool -> Maybe Declaration -> WhereDeclarations
WhereDecls forall a. Null a => a
empty Bool
False forall a. Null a => a
empty

noWhereDecls :: WhereDeclarations
noWhereDecls :: WhereDeclarations
noWhereDecls = forall a. Null a => a
empty

type Clause = Clause' LHS
type SpineClause = Clause' SpineLHS
type RewriteEqn  = RewriteEqn' QName BindName Pattern Expr
type WithExpr' e = Named BindName (Arg e)
type WithExpr    = WithExpr' Expr

data RHS
  = RHS
    { RHS -> Expr
rhsExpr     :: Expr
    , RHS -> Maybe Expr
rhsConcrete :: Maybe C.Expr
      -- ^ We store the original concrete expression in case
      --   we have to reproduce it during interactive case splitting.
      --   'Nothing' for internally generated rhss.
    }
  | AbsurdRHS
  | WithRHS QName [WithExpr] [Clause]
      -- ^ The 'QName' is the name of the with function.
  | RewriteRHS
    { RHS -> [RewriteEqn]
rewriteExprs      :: [RewriteEqn]
      -- ^ The 'QName's are the names of the generated with functions,
      --   one for each 'Expr'.
    , RHS -> [ProblemEq]
rewriteStrippedPats :: [ProblemEq]
      -- ^ The patterns stripped by with-desugaring. These are only present
      --   if this rewrite follows a with.
    , RHS -> RHS
rewriteRHS        :: RHS
      -- ^ The RHS should not be another @RewriteRHS@.
    , RHS -> WhereDeclarations
rewriteWhereDecls :: WhereDeclarations
      -- ^ The where clauses are attached to the @RewriteRHS@ by
      ---  the scope checker (instead of to the clause).
    }
  deriving (Int -> RHS -> ShowS
[RHS] -> ShowS
RHS -> ArgName
forall a.
(Int -> a -> ShowS) -> (a -> ArgName) -> ([a] -> ShowS) -> Show a
showList :: [RHS] -> ShowS
$cshowList :: [RHS] -> ShowS
show :: RHS -> ArgName
$cshow :: RHS -> ArgName
showsPrec :: Int -> RHS -> ShowS
$cshowsPrec :: Int -> RHS -> ShowS
Show, forall x. Rep RHS x -> RHS
forall x. RHS -> Rep RHS x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep RHS x -> RHS
$cfrom :: forall x. RHS -> Rep RHS x
Generic)

-- | Ignore 'rhsConcrete' when comparing 'RHS's.
instance Eq RHS where
  RHS Expr
e Maybe Expr
_          == :: RHS -> RHS -> Bool
== RHS Expr
e' Maybe Expr
_            = Expr
e forall a. Eq a => a -> a -> Bool
== Expr
e'
  RHS
AbsurdRHS        == RHS
AbsurdRHS           = Bool
True
  WithRHS QName
a [WithExpr]
b [Clause]
c    == WithRHS QName
a' [WithExpr]
b' [Clause]
c'    = (QName
a forall a. Eq a => a -> a -> Bool
== QName
a') Bool -> Bool -> Bool
&& ([WithExpr]
b forall a. Eq a => a -> a -> Bool
== [WithExpr]
b') Bool -> Bool -> Bool
&& ([Clause]
c forall a. Eq a => a -> a -> Bool
== [Clause]
c')
  RewriteRHS [RewriteEqn]
a [ProblemEq]
b RHS
c WhereDeclarations
d == RewriteRHS [RewriteEqn]
a' [ProblemEq]
b' RHS
c' WhereDeclarations
d' = forall (t :: * -> *). Foldable t => t Bool -> Bool
and [ [RewriteEqn]
a forall a. Eq a => a -> a -> Bool
== [RewriteEqn]
a', [ProblemEq]
b forall a. Eq a => a -> a -> Bool
== [ProblemEq]
b', RHS
c forall a. Eq a => a -> a -> Bool
== RHS
c' , WhereDeclarations
d forall a. Eq a => a -> a -> Bool
== WhereDeclarations
d' ]
  RHS
_                == RHS
_                   = Bool
False

-- | The lhs of a clause in spine view (inside-out).
--   Projection patterns are contained in @spLhsPats@,
--   represented as @ProjP d@.
data SpineLHS = SpineLHS
  { SpineLHS -> LHSInfo
spLhsInfo     :: LHSInfo             -- ^ Range.
  , SpineLHS -> QName
spLhsDefName  :: QName               -- ^ Name of function we are defining.
  , SpineLHS -> [NamedArg Pattern]
spLhsPats     :: [NamedArg Pattern]  -- ^ Elimination by pattern, projections, with-patterns.
  }
  deriving (Int -> SpineLHS -> ShowS
[SpineLHS] -> ShowS
SpineLHS -> ArgName
forall a.
(Int -> a -> ShowS) -> (a -> ArgName) -> ([a] -> ShowS) -> Show a
showList :: [SpineLHS] -> ShowS
$cshowList :: [SpineLHS] -> ShowS
show :: SpineLHS -> ArgName
$cshow :: SpineLHS -> ArgName
showsPrec :: Int -> SpineLHS -> ShowS
$cshowsPrec :: Int -> SpineLHS -> ShowS
Show, SpineLHS -> SpineLHS -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: SpineLHS -> SpineLHS -> Bool
$c/= :: SpineLHS -> SpineLHS -> Bool
== :: SpineLHS -> SpineLHS -> Bool
$c== :: SpineLHS -> SpineLHS -> Bool
Eq, forall x. Rep SpineLHS x -> SpineLHS
forall x. SpineLHS -> Rep SpineLHS x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep SpineLHS x -> SpineLHS
$cfrom :: forall x. SpineLHS -> Rep SpineLHS x
Generic)

-- | Ignore 'Range' when comparing 'LHS's.
instance Eq LHS where
  LHS LHSInfo
_ LHSCore
core == :: LHS -> LHS -> Bool
== LHS LHSInfo
_ LHSCore
core' = LHSCore
core forall a. Eq a => a -> a -> Bool
== LHSCore
core'

-- | The lhs of a clause in focused (projection-application) view (outside-in).
--   Projection patters are represented as 'LHSProj's.
data LHS = LHS
  { LHS -> LHSInfo
lhsInfo     :: LHSInfo               -- ^ Range.
  , LHS -> LHSCore
lhsCore     :: LHSCore               -- ^ Copatterns.
  }
  deriving (Int -> LHS -> ShowS
[LHS] -> ShowS
LHS -> ArgName
forall a.
(Int -> a -> ShowS) -> (a -> ArgName) -> ([a] -> ShowS) -> Show a
showList :: [LHS] -> ShowS
$cshowList :: [LHS] -> ShowS
show :: LHS -> ArgName
$cshow :: LHS -> ArgName
showsPrec :: Int -> LHS -> ShowS
$cshowsPrec :: Int -> LHS -> ShowS
Show, forall x. Rep LHS x -> LHS
forall x. LHS -> Rep LHS x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep LHS x -> LHS
$cfrom :: forall x. LHS -> Rep LHS x
Generic)

-- | The lhs in projection-application and with-pattern view.
--   Parameterised over the type @e@ of dot patterns.
data LHSCore' e
    -- | The head applied to ordinary patterns.
  = LHSHead  { forall e. LHSCore' e -> QName
lhsDefName  :: QName
                 -- ^ Head @f@.
             , forall e. LHSCore' e -> [NamedArg (Pattern' e)]
lhsPats     :: [NamedArg (Pattern' e)]
                 -- ^ Applied to patterns @ps@.
             }
    -- | Projection.
  | LHSProj  { forall e. LHSCore' e -> AmbiguousQName
lhsDestructor :: AmbiguousQName
                 -- ^ Record projection identifier.
             , forall e. LHSCore' e -> NamedArg (LHSCore' e)
lhsFocus      :: NamedArg (LHSCore' e)
                 -- ^ Main argument of projection.
             , lhsPats       :: [NamedArg (Pattern' e)]
                 -- ^ Further applied to patterns.
             }
    -- | With patterns.
  | LHSWith  { forall e. LHSCore' e -> LHSCore' e
lhsHead         :: LHSCore' e
                 -- ^ E.g. the 'LHSHead'.
             , forall e. LHSCore' e -> [Arg (Pattern' e)]
lhsWithPatterns :: [Arg (Pattern' e)]
                 -- ^ Applied to with patterns @| p1 | ... | pn@.
                 --   These patterns are not prefixed with @WithP@!
             , lhsPats         :: [NamedArg (Pattern' e)]
                 -- ^ Further applied to patterns.
             }
  deriving (Int -> LHSCore' e -> ShowS
forall e. Show e => Int -> LHSCore' e -> ShowS
forall e. Show e => [LHSCore' e] -> ShowS
forall e. Show e => LHSCore' e -> ArgName
forall a.
(Int -> a -> ShowS) -> (a -> ArgName) -> ([a] -> ShowS) -> Show a
showList :: [LHSCore' e] -> ShowS
$cshowList :: forall e. Show e => [LHSCore' e] -> ShowS
show :: LHSCore' e -> ArgName
$cshow :: forall e. Show e => LHSCore' e -> ArgName
showsPrec :: Int -> LHSCore' e -> ShowS
$cshowsPrec :: forall e. Show e => Int -> LHSCore' e -> ShowS
Show, forall a b. a -> LHSCore' b -> LHSCore' a
forall a b. (a -> b) -> LHSCore' a -> LHSCore' b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> LHSCore' b -> LHSCore' a
$c<$ :: forall a b. a -> LHSCore' b -> LHSCore' a
fmap :: forall a b. (a -> b) -> LHSCore' a -> LHSCore' b
$cfmap :: forall a b. (a -> b) -> LHSCore' a -> LHSCore' b
Functor, forall a. Eq a => a -> LHSCore' a -> Bool
forall a. Num a => LHSCore' a -> a
forall a. Ord a => LHSCore' a -> a
forall m. Monoid m => LHSCore' m -> m
forall a. LHSCore' a -> Bool
forall a. LHSCore' a -> Int
forall a. LHSCore' a -> [a]
forall a. (a -> a -> a) -> LHSCore' a -> a
forall m a. Monoid m => (a -> m) -> LHSCore' a -> m
forall b a. (b -> a -> b) -> b -> LHSCore' a -> b
forall a b. (a -> b -> b) -> b -> LHSCore' a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
product :: forall a. Num a => LHSCore' a -> a
$cproduct :: forall a. Num a => LHSCore' a -> a
sum :: forall a. Num a => LHSCore' a -> a
$csum :: forall a. Num a => LHSCore' a -> a
minimum :: forall a. Ord a => LHSCore' a -> a
$cminimum :: forall a. Ord a => LHSCore' a -> a
maximum :: forall a. Ord a => LHSCore' a -> a
$cmaximum :: forall a. Ord a => LHSCore' a -> a
elem :: forall a. Eq a => a -> LHSCore' a -> Bool
$celem :: forall a. Eq a => a -> LHSCore' a -> Bool
length :: forall a. LHSCore' a -> Int
$clength :: forall a. LHSCore' a -> Int
null :: forall a. LHSCore' a -> Bool
$cnull :: forall a. LHSCore' a -> Bool
toList :: forall a. LHSCore' a -> [a]
$ctoList :: forall a. LHSCore' a -> [a]
foldl1 :: forall a. (a -> a -> a) -> LHSCore' a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> LHSCore' a -> a
foldr1 :: forall a. (a -> a -> a) -> LHSCore' a -> a
$cfoldr1 :: forall a. (a -> a -> a) -> LHSCore' a -> a
foldl' :: forall b a. (b -> a -> b) -> b -> LHSCore' a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> LHSCore' a -> b
foldl :: forall b a. (b -> a -> b) -> b -> LHSCore' a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> LHSCore' a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> LHSCore' a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> LHSCore' a -> b
foldr :: forall a b. (a -> b -> b) -> b -> LHSCore' a -> b
$cfoldr :: forall a b. (a -> b -> b) -> b -> LHSCore' a -> b
foldMap' :: forall m a. Monoid m => (a -> m) -> LHSCore' a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> LHSCore' a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> LHSCore' a -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> LHSCore' a -> m
fold :: forall m. Monoid m => LHSCore' m -> m
$cfold :: forall m. Monoid m => LHSCore' m -> m
Foldable, Functor LHSCore'
Foldable LHSCore'
forall (t :: * -> *).
Functor t
-> Foldable t
-> (forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: * -> *) a. Monad m => LHSCore' (m a) -> m (LHSCore' a)
forall (f :: * -> *) a.
Applicative f =>
LHSCore' (f a) -> f (LHSCore' a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> LHSCore' a -> m (LHSCore' b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> LHSCore' a -> f (LHSCore' b)
sequence :: forall (m :: * -> *) a. Monad m => LHSCore' (m a) -> m (LHSCore' a)
$csequence :: forall (m :: * -> *) a. Monad m => LHSCore' (m a) -> m (LHSCore' a)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> LHSCore' a -> m (LHSCore' b)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> LHSCore' a -> m (LHSCore' b)
sequenceA :: forall (f :: * -> *) a.
Applicative f =>
LHSCore' (f a) -> f (LHSCore' a)
$csequenceA :: forall (f :: * -> *) a.
Applicative f =>
LHSCore' (f a) -> f (LHSCore' a)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> LHSCore' a -> f (LHSCore' b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> LHSCore' a -> f (LHSCore' b)
Traversable, LHSCore' e -> LHSCore' e -> Bool
forall e. Eq e => LHSCore' e -> LHSCore' e -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: LHSCore' e -> LHSCore' e -> Bool
$c/= :: forall e. Eq e => LHSCore' e -> LHSCore' e -> Bool
== :: LHSCore' e -> LHSCore' e -> Bool
$c== :: forall e. Eq e => LHSCore' e -> LHSCore' e -> Bool
Eq, forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall e x. Rep (LHSCore' e) x -> LHSCore' e
forall e x. LHSCore' e -> Rep (LHSCore' e) x
$cto :: forall e x. Rep (LHSCore' e) x -> LHSCore' e
$cfrom :: forall e x. LHSCore' e -> Rep (LHSCore' e) x
Generic)

type LHSCore = LHSCore' Expr

---------------------------------------------------------------------------
-- * Patterns
---------------------------------------------------------------------------

-- | Parameterised over the type of dot patterns.
data Pattern' e
  = VarP BindName
  | ConP ConPatInfo AmbiguousQName (NAPs e)
  | ProjP PatInfo ProjOrigin AmbiguousQName
    -- ^ Destructor pattern @d@.
  | DefP PatInfo AmbiguousQName (NAPs e)
    -- ^ Defined pattern: function definition @f ps@.
    --   It is also abused to convert destructor patterns into concrete syntax
    --   thus, we put AmbiguousQName here as well.
  | WildP PatInfo
    -- ^ Underscore pattern entered by user.
    --   Or generated at type checking for implicit arguments.
  | AsP PatInfo BindName (Pattern' e)
  | DotP PatInfo e
    -- ^ Dot pattern @.e@
  | AbsurdP PatInfo
  | LitP PatInfo Literal
  | PatternSynP PatInfo AmbiguousQName (NAPs e)
  | RecP PatInfo [FieldAssignment' (Pattern' e)]
  | EqualP PatInfo [(e, e)]
  | WithP PatInfo (Pattern' e)  -- ^ @| p@, for with-patterns.
  | AnnP PatInfo e (Pattern' e) -- ^ Pattern with type annotation
  deriving (Int -> Pattern' e -> ShowS
forall e. Show e => Int -> Pattern' e -> ShowS
forall e. Show e => [Pattern' e] -> ShowS
forall e. Show e => Pattern' e -> ArgName
forall a.
(Int -> a -> ShowS) -> (a -> ArgName) -> ([a] -> ShowS) -> Show a
showList :: [Pattern' e] -> ShowS
$cshowList :: forall e. Show e => [Pattern' e] -> ShowS
show :: Pattern' e -> ArgName
$cshow :: forall e. Show e => Pattern' e -> ArgName
showsPrec :: Int -> Pattern' e -> ShowS
$cshowsPrec :: forall e. Show e => Int -> Pattern' e -> ShowS
Show, forall a b. a -> Pattern' b -> Pattern' a
forall a b. (a -> b) -> Pattern' a -> Pattern' b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> Pattern' b -> Pattern' a
$c<$ :: forall a b. a -> Pattern' b -> Pattern' a
fmap :: forall a b. (a -> b) -> Pattern' a -> Pattern' b
$cfmap :: forall a b. (a -> b) -> Pattern' a -> Pattern' b
Functor, forall a. Eq a => a -> Pattern' a -> Bool
forall a. Num a => Pattern' a -> a
forall a. Ord a => Pattern' a -> a
forall m. Monoid m => Pattern' m -> m
forall a. Pattern' a -> Bool
forall a. Pattern' a -> Int
forall a. Pattern' a -> [a]
forall a. (a -> a -> a) -> Pattern' a -> a
forall m a. Monoid m => (a -> m) -> Pattern' a -> m
forall b a. (b -> a -> b) -> b -> Pattern' a -> b
forall a b. (a -> b -> b) -> b -> Pattern' a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
product :: forall a. Num a => Pattern' a -> a
$cproduct :: forall a. Num a => Pattern' a -> a
sum :: forall a. Num a => Pattern' a -> a
$csum :: forall a. Num a => Pattern' a -> a
minimum :: forall a. Ord a => Pattern' a -> a
$cminimum :: forall a. Ord a => Pattern' a -> a
maximum :: forall a. Ord a => Pattern' a -> a
$cmaximum :: forall a. Ord a => Pattern' a -> a
elem :: forall a. Eq a => a -> Pattern' a -> Bool
$celem :: forall a. Eq a => a -> Pattern' a -> Bool
length :: forall a. Pattern' a -> Int
$clength :: forall a. Pattern' a -> Int
null :: forall a. Pattern' a -> Bool
$cnull :: forall a. Pattern' a -> Bool
toList :: forall a. Pattern' a -> [a]
$ctoList :: forall a. Pattern' a -> [a]
foldl1 :: forall a. (a -> a -> a) -> Pattern' a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> Pattern' a -> a
foldr1 :: forall a. (a -> a -> a) -> Pattern' a -> a
$cfoldr1 :: forall a. (a -> a -> a) -> Pattern' a -> a
foldl' :: forall b a. (b -> a -> b) -> b -> Pattern' a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> Pattern' a -> b
foldl :: forall b a. (b -> a -> b) -> b -> Pattern' a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> Pattern' a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> Pattern' a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> Pattern' a -> b
foldr :: forall a b. (a -> b -> b) -> b -> Pattern' a -> b
$cfoldr :: forall a b. (a -> b -> b) -> b -> Pattern' a -> b
foldMap' :: forall m a. Monoid m => (a -> m) -> Pattern' a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> Pattern' a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> Pattern' a -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> Pattern' a -> m
fold :: forall m. Monoid m => Pattern' m -> m
$cfold :: forall m. Monoid m => Pattern' m -> m
Foldable, Functor Pattern'
Foldable Pattern'
forall (t :: * -> *).
Functor t
-> Foldable t
-> (forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: * -> *) a. Monad m => Pattern' (m a) -> m (Pattern' a)
forall (f :: * -> *) a.
Applicative f =>
Pattern' (f a) -> f (Pattern' a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Pattern' a -> m (Pattern' b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Pattern' a -> f (Pattern' b)
sequence :: forall (m :: * -> *) a. Monad m => Pattern' (m a) -> m (Pattern' a)
$csequence :: forall (m :: * -> *) a. Monad m => Pattern' (m a) -> m (Pattern' a)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Pattern' a -> m (Pattern' b)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Pattern' a -> m (Pattern' b)
sequenceA :: forall (f :: * -> *) a.
Applicative f =>
Pattern' (f a) -> f (Pattern' a)
$csequenceA :: forall (f :: * -> *) a.
Applicative f =>
Pattern' (f a) -> f (Pattern' a)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Pattern' a -> f (Pattern' b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Pattern' a -> f (Pattern' b)
Traversable, Pattern' e -> Pattern' e -> Bool
forall e. Eq e => Pattern' e -> Pattern' e -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Pattern' e -> Pattern' e -> Bool
$c/= :: forall e. Eq e => Pattern' e -> Pattern' e -> Bool
== :: Pattern' e -> Pattern' e -> Bool
$c== :: forall e. Eq e => Pattern' e -> Pattern' e -> Bool
Eq, forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall e x. Rep (Pattern' e) x -> Pattern' e
forall e x. Pattern' e -> Rep (Pattern' e) x
$cto :: forall e x. Rep (Pattern' e) x -> Pattern' e
$cfrom :: forall e x. Pattern' e -> Rep (Pattern' e) x
Generic)

type NAPs e   = [NamedArg (Pattern' e)]
type NAPs1 e  = List1 (NamedArg (Pattern' e))
type Pattern  = Pattern' Expr
type Patterns = [NamedArg Pattern]

instance IsProjP (Pattern' e) where
  -- Andreas, 2018-06-19, issue #3130
  -- Do not interpret things like .(p) as projection pattern any more.
  -- maybePostfixProjP (DotP _ e)    = isProjP e <&> \ (_o, d) -> (ProjPostfix, d)
  isProjP :: Pattern' e -> Maybe (ProjOrigin, AmbiguousQName)
isProjP (ProjP PatInfo
_ ProjOrigin
o AmbiguousQName
d) = forall a. a -> Maybe a
Just (ProjOrigin
o, AmbiguousQName
d)
  isProjP Pattern' e
_ = forall a. Maybe a
Nothing

instance IsProjP Expr where
  isProjP :: Expr -> Maybe (ProjOrigin, AmbiguousQName)
isProjP (Proj ProjOrigin
o AmbiguousQName
ds)      = forall a. a -> Maybe a
Just (ProjOrigin
o, AmbiguousQName
ds)
  isProjP (ScopedExpr ScopeInfo
_ Expr
e) = forall a. IsProjP a => a -> Maybe (ProjOrigin, AmbiguousQName)
isProjP Expr
e
  isProjP Expr
_ = forall a. Maybe a
Nothing

{--------------------------------------------------------------------------
    Things we parse but are not part of the Agda file syntax
 --------------------------------------------------------------------------}

type HoleContent = C.HoleContent' () BindName Pattern Expr

{--------------------------------------------------------------------------
    Instances
 --------------------------------------------------------------------------}

-- | Does not compare 'ScopeInfo' fields.
--   Does not distinguish between prefix and postfix projections.

instance Eq Expr where
  ScopedExpr ScopeInfo
_ Expr
a1            == :: Expr -> Expr -> Bool
== ScopedExpr ScopeInfo
_ Expr
a2            = Expr
a1 forall a. Eq a => a -> a -> Bool
== Expr
a2

  Var Name
a1                     == Var Name
a2                     = Name
a1 forall a. Eq a => a -> a -> Bool
== Name
a2
  Def' QName
a1 Suffix
s1                 == Def' QName
a2 Suffix
s2                 = (QName
a1, Suffix
s1) forall a. Eq a => a -> a -> Bool
== (QName
a2, Suffix
s2)
  Proj ProjOrigin
_ AmbiguousQName
a1                  == Proj ProjOrigin
_ AmbiguousQName
a2                  = AmbiguousQName
a1 forall a. Eq a => a -> a -> Bool
== AmbiguousQName
a2
  Con AmbiguousQName
a1                     == Con AmbiguousQName
a2                     = AmbiguousQName
a1 forall a. Eq a => a -> a -> Bool
== AmbiguousQName
a2
  PatternSyn AmbiguousQName
a1              == PatternSyn AmbiguousQName
a2              = AmbiguousQName
a1 forall a. Eq a => a -> a -> Bool
== AmbiguousQName
a2
  Macro QName
a1                   == Macro QName
a2                   = QName
a1 forall a. Eq a => a -> a -> Bool
== QName
a2
  Lit ExprInfo
r1 Literal
a1                  == Lit ExprInfo
r2 Literal
a2                  = (ExprInfo
r1, Literal
a1) forall a. Eq a => a -> a -> Bool
== (ExprInfo
r2, Literal
a2)
  QuestionMark MetaInfo
a1 InteractionId
b1         == QuestionMark MetaInfo
a2 InteractionId
b2         = (MetaInfo
a1, InteractionId
b1) forall a. Eq a => a -> a -> Bool
== (MetaInfo
a2, InteractionId
b2)
  Underscore MetaInfo
a1              == Underscore MetaInfo
a2              = MetaInfo
a1 forall a. Eq a => a -> a -> Bool
== MetaInfo
a2
  Dot ExprInfo
r1 Expr
e1                  == Dot ExprInfo
r2 Expr
e2                  = (ExprInfo
r1, Expr
e1) forall a. Eq a => a -> a -> Bool
== (ExprInfo
r2, Expr
e2)
  App AppInfo
a1 Expr
b1 NamedArg Expr
c1               == App AppInfo
a2 Expr
b2 NamedArg Expr
c2               = (AppInfo
a1, Expr
b1, NamedArg Expr
c1) forall a. Eq a => a -> a -> Bool
== (AppInfo
a2, Expr
b2, NamedArg Expr
c2)
  WithApp ExprInfo
a1 Expr
b1 [Expr]
c1           == WithApp ExprInfo
a2 Expr
b2 [Expr]
c2           = (ExprInfo
a1, Expr
b1, [Expr]
c1) forall a. Eq a => a -> a -> Bool
== (ExprInfo
a2, Expr
b2, [Expr]
c2)
  Lam ExprInfo
a1 LamBinding
b1 Expr
c1               == Lam ExprInfo
a2 LamBinding
b2 Expr
c2               = (ExprInfo
a1, LamBinding
b1, Expr
c1) forall a. Eq a => a -> a -> Bool
== (ExprInfo
a2, LamBinding
b2, Expr
c2)
  AbsurdLam ExprInfo
a1 Hiding
b1            == AbsurdLam ExprInfo
a2 Hiding
b2            = (ExprInfo
a1, Hiding
b1) forall a. Eq a => a -> a -> Bool
== (ExprInfo
a2, Hiding
b2)
  ExtendedLam ExprInfo
a1 DefInfo
b1 Erased
c1 QName
d1 List1 Clause
e1 == ExtendedLam ExprInfo
a2 DefInfo
b2 Erased
c2 QName
d2 List1 Clause
e2 = (ExprInfo
a1, DefInfo
b1, Erased
c1, QName
d1, List1 Clause
e1) forall a. Eq a => a -> a -> Bool
==
                                                             (ExprInfo
a2, DefInfo
b2, Erased
c2, QName
d2, List1 Clause
e2)
  Pi ExprInfo
a1 Telescope1
b1 Expr
c1                == Pi ExprInfo
a2 Telescope1
b2 Expr
c2                = (ExprInfo
a1, Telescope1
b1, Expr
c1) forall a. Eq a => a -> a -> Bool
== (ExprInfo
a2, Telescope1
b2, Expr
c2)
  Generalized Set QName
a1 Expr
b1          == Generalized Set QName
a2 Expr
b2          = (Set QName
a1, Expr
b1) forall a. Eq a => a -> a -> Bool
== (Set QName
a2, Expr
b2)
  Fun ExprInfo
a1 Arg Expr
b1 Expr
c1               == Fun ExprInfo
a2 Arg Expr
b2 Expr
c2               = (ExprInfo
a1, Arg Expr
b1, Expr
c1) forall a. Eq a => a -> a -> Bool
== (ExprInfo
a2, Arg Expr
b2, Expr
c2)
  Let ExprInfo
a1 List1 LetBinding
b1 Expr
c1               == Let ExprInfo
a2 List1 LetBinding
b2 Expr
c2               = (ExprInfo
a1, List1 LetBinding
b1, Expr
c1) forall a. Eq a => a -> a -> Bool
== (ExprInfo
a2, List1 LetBinding
b2, Expr
c2)
  Rec ExprInfo
a1 RecordAssigns
b1                  == Rec ExprInfo
a2 RecordAssigns
b2                  = (ExprInfo
a1, RecordAssigns
b1) forall a. Eq a => a -> a -> Bool
== (ExprInfo
a2, RecordAssigns
b2)
  RecUpdate ExprInfo
a1 Expr
b1 Assigns
c1         == RecUpdate ExprInfo
a2 Expr
b2 Assigns
c2         = (ExprInfo
a1, Expr
b1, Assigns
c1) forall a. Eq a => a -> a -> Bool
== (ExprInfo
a2, Expr
b2, Assigns
c2)
  Quote ExprInfo
a1                   == Quote ExprInfo
a2                   = ExprInfo
a1 forall a. Eq a => a -> a -> Bool
== ExprInfo
a2
  QuoteTerm ExprInfo
a1               == QuoteTerm ExprInfo
a2               = ExprInfo
a1 forall a. Eq a => a -> a -> Bool
== ExprInfo
a2
  Unquote ExprInfo
a1                 == Unquote ExprInfo
a2                 = ExprInfo
a1 forall a. Eq a => a -> a -> Bool
== ExprInfo
a2
  DontCare Expr
a1                == DontCare Expr
a2                = Expr
a1 forall a. Eq a => a -> a -> Bool
== Expr
a2

  Expr
_                          == Expr
_                          = Bool
False

-- | Does not compare 'ScopeInfo' fields.

instance Eq Declaration where
  ScopedDecl ScopeInfo
_ [Declaration]
a1                == :: Declaration -> Declaration -> Bool
== ScopedDecl ScopeInfo
_ [Declaration]
a2                = [Declaration]
a1 forall a. Eq a => a -> a -> Bool
== [Declaration]
a2

  Axiom KindOfName
a1 DefInfo
b1 ArgInfo
c1 Maybe [Occurrence]
d1 QName
e1 Expr
f1        == Axiom KindOfName
a2 DefInfo
b2 ArgInfo
c2 Maybe [Occurrence]
d2 QName
e2 Expr
f2        = (KindOfName
a1, DefInfo
b1, ArgInfo
c1, Maybe [Occurrence]
d1, QName
e1, Expr
f1) forall a. Eq a => a -> a -> Bool
== (KindOfName
a2, DefInfo
b2, ArgInfo
c2, Maybe [Occurrence]
d2, QName
e2, Expr
f2)
  Generalize Set QName
a1 DefInfo
b1 ArgInfo
c1 QName
d1 Expr
e1      == Generalize Set QName
a2 DefInfo
b2 ArgInfo
c2 QName
d2 Expr
e2      = (Set QName
a1, DefInfo
b1, ArgInfo
c1, QName
d1, Expr
e1) forall a. Eq a => a -> a -> Bool
== (Set QName
a2, DefInfo
b2, ArgInfo
c2, QName
d2, Expr
e2)
  Field DefInfo
a1 QName
b1 Arg Expr
c1                 == Field DefInfo
a2 QName
b2 Arg Expr
c2                 = (DefInfo
a1, QName
b1, Arg Expr
c1) forall a. Eq a => a -> a -> Bool
== (DefInfo
a2, QName
b2, Arg Expr
c2)
  Primitive DefInfo
a1 QName
b1 Arg Expr
c1             == Primitive DefInfo
a2 QName
b2 Arg Expr
c2             = (DefInfo
a1, QName
b1, Arg Expr
c1) forall a. Eq a => a -> a -> Bool
== (DefInfo
a2, QName
b2, Arg Expr
c2)
  Mutual MutualInfo
a1 [Declaration]
b1                   == Mutual MutualInfo
a2 [Declaration]
b2                   = (MutualInfo
a1, [Declaration]
b1) forall a. Eq a => a -> a -> Bool
== (MutualInfo
a2, [Declaration]
b2)
  Section Range
a1 ModuleName
b1 GeneralizeTelescope
c1 [Declaration]
d1            == Section Range
a2 ModuleName
b2 GeneralizeTelescope
c2 [Declaration]
d2            = (Range
a1, ModuleName
b1, GeneralizeTelescope
c1, [Declaration]
d1) forall a. Eq a => a -> a -> Bool
== (Range
a2, ModuleName
b2, GeneralizeTelescope
c2, [Declaration]
d2)
  Apply ModuleInfo
a1 ModuleName
b1 ModuleApplication
c1 ScopeCopyInfo
d1 ImportDirective
e1           == Apply ModuleInfo
a2 ModuleName
b2 ModuleApplication
c2 ScopeCopyInfo
d2 ImportDirective
e2           = (ModuleInfo
a1, ModuleName
b1, ModuleApplication
c1, ScopeCopyInfo
d1, ImportDirective
e1) forall a. Eq a => a -> a -> Bool
== (ModuleInfo
a2, ModuleName
b2, ModuleApplication
c2, ScopeCopyInfo
d2, ImportDirective
e2)
  Import ModuleInfo
a1 ModuleName
b1 ImportDirective
c1                == Import ModuleInfo
a2 ModuleName
b2 ImportDirective
c2                = (ModuleInfo
a1, ModuleName
b1, ImportDirective
c1) forall a. Eq a => a -> a -> Bool
== (ModuleInfo
a2, ModuleName
b2, ImportDirective
c2)
  Pragma Range
a1 Pragma
b1                   == Pragma Range
a2 Pragma
b2                   = (Range
a1, Pragma
b1) forall a. Eq a => a -> a -> Bool
== (Range
a2, Pragma
b2)
  Open ModuleInfo
a1 ModuleName
b1 ImportDirective
c1                  == Open ModuleInfo
a2 ModuleName
b2 ImportDirective
c2                  = (ModuleInfo
a1, ModuleName
b1, ImportDirective
c1) forall a. Eq a => a -> a -> Bool
== (ModuleInfo
a2, ModuleName
b2, ImportDirective
c2)
  FunDef DefInfo
a1 QName
b1 Delayed
c1 [Clause]
d1             == FunDef DefInfo
a2 QName
b2 Delayed
c2 [Clause]
d2             = (DefInfo
a1, QName
b1, Delayed
c1, [Clause]
d1) forall a. Eq a => a -> a -> Bool
== (DefInfo
a2, QName
b2, Delayed
c2, [Clause]
d2)
  DataSig DefInfo
a1 QName
b1 GeneralizeTelescope
c1 Expr
d1            == DataSig DefInfo
a2 QName
b2 GeneralizeTelescope
c2 Expr
d2            = (DefInfo
a1, QName
b1, GeneralizeTelescope
c1, Expr
d1) forall a. Eq a => a -> a -> Bool
== (DefInfo
a2, QName
b2, GeneralizeTelescope
c2, Expr
d2)
  DataDef DefInfo
a1 QName
b1 UniverseCheck
c1 DataDefParams
d1 [Declaration]
e1         == DataDef DefInfo
a2 QName
b2 UniverseCheck
c2 DataDefParams
d2 [Declaration]
e2         = (DefInfo
a1, QName
b1, UniverseCheck
c1, DataDefParams
d1, [Declaration]
e1) forall a. Eq a => a -> a -> Bool
== (DefInfo
a2, QName
b2, UniverseCheck
c2, DataDefParams
d2, [Declaration]
e2)
  RecSig DefInfo
a1 QName
b1 GeneralizeTelescope
c1 Expr
d1             == RecSig DefInfo
a2 QName
b2 GeneralizeTelescope
c2 Expr
d2             = (DefInfo
a1, QName
b1, GeneralizeTelescope
c1, Expr
d1) forall a. Eq a => a -> a -> Bool
== (DefInfo
a2, QName
b2, GeneralizeTelescope
c2, Expr
d2)
  RecDef DefInfo
a1 QName
b1 UniverseCheck
c1 RecordDirectives
d1 DataDefParams
e1 Expr
f1 [Declaration]
g1    == RecDef DefInfo
a2 QName
b2 UniverseCheck
c2 RecordDirectives
d2 DataDefParams
e2 Expr
f2 [Declaration]
g2    = (DefInfo
a1, QName
b1, UniverseCheck
c1, RecordDirectives
d1, DataDefParams
e1, Expr
f1, [Declaration]
g1) forall a. Eq a => a -> a -> Bool
== (DefInfo
a2, QName
b2, UniverseCheck
c2, RecordDirectives
d2, DataDefParams
e2, Expr
f2, [Declaration]
g2)
  PatternSynDef QName
a1 [Arg BindName]
b1 Pattern' Void
c1         == PatternSynDef QName
a2 [Arg BindName]
b2 Pattern' Void
c2         = (QName
a1, [Arg BindName]
b1, Pattern' Void
c1) forall a. Eq a => a -> a -> Bool
== (QName
a2, [Arg BindName]
b2, Pattern' Void
c2)
  UnquoteDecl MutualInfo
a1 [DefInfo]
b1 [QName]
c1 Expr
d1        == UnquoteDecl MutualInfo
a2 [DefInfo]
b2 [QName]
c2 Expr
d2        = (MutualInfo
a1, [DefInfo]
b1, [QName]
c1, Expr
d1) forall a. Eq a => a -> a -> Bool
== (MutualInfo
a2, [DefInfo]
b2, [QName]
c2, Expr
d2)
  UnquoteDef [DefInfo]
a1 [QName]
b1 Expr
c1            == UnquoteDef [DefInfo]
a2 [QName]
b2 Expr
c2            = ([DefInfo]
a1, [QName]
b1, Expr
c1) forall a. Eq a => a -> a -> Bool
== ([DefInfo]
a2, [QName]
b2, Expr
c2)

  Declaration
_                              == Declaration
_                              = Bool
False

instance Underscore Expr where
  underscore :: Expr
underscore   = MetaInfo -> Expr
Underscore MetaInfo
emptyMetaInfo
  isUnderscore :: Expr -> Bool
isUnderscore = forall a. HasCallStack => a
__IMPOSSIBLE__

instance LensHiding LamBinding where
  getHiding :: LamBinding -> Hiding
getHiding   (DomainFree TacticAttr
_ NamedArg Binder
x) = forall a. LensHiding a => a -> Hiding
getHiding NamedArg Binder
x
  getHiding   (DomainFull TypedBinding
tb)  = forall a. LensHiding a => a -> Hiding
getHiding TypedBinding
tb
  mapHiding :: (Hiding -> Hiding) -> LamBinding -> LamBinding
mapHiding Hiding -> Hiding
f (DomainFree TacticAttr
t NamedArg Binder
x) = TacticAttr -> NamedArg Binder -> LamBinding
DomainFree TacticAttr
t forall a b. (a -> b) -> a -> b
$ forall a. LensHiding a => (Hiding -> Hiding) -> a -> a
mapHiding Hiding -> Hiding
f NamedArg Binder
x
  mapHiding Hiding -> Hiding
f (DomainFull TypedBinding
tb)  = TypedBinding -> LamBinding
DomainFull forall a b. (a -> b) -> a -> b
$ forall a. LensHiding a => (Hiding -> Hiding) -> a -> a
mapHiding Hiding -> Hiding
f TypedBinding
tb

instance LensHiding TypedBinding where
  getHiding :: TypedBinding -> Hiding
getHiding (TBind Range
_ TypedBindingInfo
_ (NamedArg Binder
x :|[NamedArg Binder]
_) Expr
_) = forall a. LensHiding a => a -> Hiding
getHiding NamedArg Binder
x   -- Slightly dubious
  getHiding TLet{}                = forall a. Monoid a => a
mempty
  mapHiding :: (Hiding -> Hiding) -> TypedBinding -> TypedBinding
mapHiding Hiding -> Hiding
f (TBind Range
r TypedBindingInfo
t List1 (NamedArg Binder)
xs Expr
e)    = Range
-> TypedBindingInfo
-> List1 (NamedArg Binder)
-> Expr
-> TypedBinding
TBind Range
r TypedBindingInfo
t ((forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. LensHiding a => (Hiding -> Hiding) -> a -> a
mapHiding) Hiding -> Hiding
f List1 (NamedArg Binder)
xs) Expr
e
  mapHiding Hiding -> Hiding
f b :: TypedBinding
b@TLet{}            = TypedBinding
b

instance HasRange a => HasRange (Binder' a) where
  getRange :: Binder' a -> Range
getRange (Binder Maybe Pattern
p a
n) = forall u t. (HasRange u, HasRange t) => u -> t -> Range
fuseRange Maybe Pattern
p a
n

instance HasRange LamBinding where
    getRange :: LamBinding -> Range
getRange (DomainFree TacticAttr
_ NamedArg Binder
x) = forall a. HasRange a => a -> Range
getRange NamedArg Binder
x
    getRange (DomainFull TypedBinding
b)   = forall a. HasRange a => a -> Range
getRange TypedBinding
b

instance HasRange TypedBinding where
    getRange :: TypedBinding -> Range
getRange (TBind Range
r TypedBindingInfo
_ List1 (NamedArg Binder)
_ Expr
_) = Range
r
    getRange (TLet Range
r List1 LetBinding
_)    = Range
r

instance HasRange Expr where
    getRange :: Expr -> Range
getRange (Var Name
x)                 = forall a. HasRange a => a -> Range
getRange Name
x
    getRange (Def' QName
x Suffix
_)              = forall a. HasRange a => a -> Range
getRange QName
x
    getRange (Proj ProjOrigin
_ AmbiguousQName
x)              = forall a. HasRange a => a -> Range
getRange AmbiguousQName
x
    getRange (Con AmbiguousQName
x)                 = forall a. HasRange a => a -> Range
getRange AmbiguousQName
x
    getRange (Lit ExprInfo
i Literal
_)               = forall a. HasRange a => a -> Range
getRange ExprInfo
i
    getRange (QuestionMark MetaInfo
i InteractionId
_)      = forall a. HasRange a => a -> Range
getRange MetaInfo
i
    getRange (Underscore  MetaInfo
i)         = forall a. HasRange a => a -> Range
getRange MetaInfo
i
    getRange (Dot ExprInfo
i Expr
_)               = forall a. HasRange a => a -> Range
getRange ExprInfo
i
    getRange (App AppInfo
i Expr
_ NamedArg Expr
_)             = forall a. HasRange a => a -> Range
getRange AppInfo
i
    getRange (WithApp ExprInfo
i Expr
_ [Expr]
_)         = forall a. HasRange a => a -> Range
getRange ExprInfo
i
    getRange (Lam ExprInfo
i LamBinding
_ Expr
_)             = forall a. HasRange a => a -> Range
getRange ExprInfo
i
    getRange (AbsurdLam ExprInfo
i Hiding
_)         = forall a. HasRange a => a -> Range
getRange ExprInfo
i
    getRange (ExtendedLam ExprInfo
i DefInfo
_ Erased
_ QName
_ List1 Clause
_) = forall a. HasRange a => a -> Range
getRange ExprInfo
i
    getRange (Pi ExprInfo
i Telescope1
_ Expr
_)              = forall a. HasRange a => a -> Range
getRange ExprInfo
i
    getRange (Generalized Set QName
_ Expr
x)       = forall a. HasRange a => a -> Range
getRange Expr
x
    getRange (Fun ExprInfo
i Arg Expr
_ Expr
_)             = forall a. HasRange a => a -> Range
getRange ExprInfo
i
    getRange (Let ExprInfo
i List1 LetBinding
_ Expr
_)             = forall a. HasRange a => a -> Range
getRange ExprInfo
i
    getRange (Rec ExprInfo
i RecordAssigns
_)               = forall a. HasRange a => a -> Range
getRange ExprInfo
i
    getRange (RecUpdate ExprInfo
i Expr
_ Assigns
_)       = forall a. HasRange a => a -> Range
getRange ExprInfo
i
    getRange (ScopedExpr ScopeInfo
_ Expr
e)        = forall a. HasRange a => a -> Range
getRange Expr
e
    getRange (Quote ExprInfo
i)               = forall a. HasRange a => a -> Range
getRange ExprInfo
i
    getRange (QuoteTerm ExprInfo
i)           = forall a. HasRange a => a -> Range
getRange ExprInfo
i
    getRange (Unquote ExprInfo
i)             = forall a. HasRange a => a -> Range
getRange ExprInfo
i
    getRange (DontCare{})            = forall a. Range' a
noRange
    getRange (PatternSyn AmbiguousQName
x)          = forall a. HasRange a => a -> Range
getRange AmbiguousQName
x
    getRange (Macro QName
x)               = forall a. HasRange a => a -> Range
getRange QName
x

instance HasRange Declaration where
    getRange :: Declaration -> Range
getRange (Axiom    KindOfName
_ DefInfo
i ArgInfo
_ Maybe [Occurrence]
_ QName
_ Expr
_  ) = forall a. HasRange a => a -> Range
getRange DefInfo
i
    getRange (Generalize Set QName
_ DefInfo
i ArgInfo
_ QName
_ Expr
_)   = forall a. HasRange a => a -> Range
getRange DefInfo
i
    getRange (Field      DefInfo
i QName
_ Arg Expr
_      ) = forall a. HasRange a => a -> Range
getRange DefInfo
i
    getRange (Mutual     MutualInfo
i [Declaration]
_        ) = forall a. HasRange a => a -> Range
getRange MutualInfo
i
    getRange (Section    Range
i ModuleName
_ GeneralizeTelescope
_ [Declaration]
_    ) = forall a. HasRange a => a -> Range
getRange Range
i
    getRange (Apply      ModuleInfo
i ModuleName
_ ModuleApplication
_ ScopeCopyInfo
_ ImportDirective
_)   = forall a. HasRange a => a -> Range
getRange ModuleInfo
i
    getRange (Import     ModuleInfo
i ModuleName
_ ImportDirective
_      ) = forall a. HasRange a => a -> Range
getRange ModuleInfo
i
    getRange (Primitive  DefInfo
i QName
_ Arg Expr
_      ) = forall a. HasRange a => a -> Range
getRange DefInfo
i
    getRange (Pragma     Range
i Pragma
_        ) = forall a. HasRange a => a -> Range
getRange Range
i
    getRange (Open       ModuleInfo
i ModuleName
_ ImportDirective
_      ) = forall a. HasRange a => a -> Range
getRange ModuleInfo
i
    getRange (ScopedDecl ScopeInfo
_ [Declaration]
d        ) = forall a. HasRange a => a -> Range
getRange [Declaration]
d
    getRange (FunDef     DefInfo
i QName
_ Delayed
_ [Clause]
_    ) = forall a. HasRange a => a -> Range
getRange DefInfo
i
    getRange (DataSig    DefInfo
i QName
_ GeneralizeTelescope
_ Expr
_    ) = forall a. HasRange a => a -> Range
getRange DefInfo
i
    getRange (DataDef    DefInfo
i QName
_ UniverseCheck
_ DataDefParams
_ [Declaration]
_  ) = forall a. HasRange a => a -> Range
getRange DefInfo
i
    getRange (RecSig     DefInfo
i QName
_ GeneralizeTelescope
_ Expr
_    ) = forall a. HasRange a => a -> Range
getRange DefInfo
i
    getRange (RecDef DefInfo
i QName
_ UniverseCheck
_ RecordDirectives
_ DataDefParams
_ Expr
_ [Declaration]
_)   = forall a. HasRange a => a -> Range
getRange DefInfo
i
    getRange (PatternSynDef QName
x [Arg BindName]
_ Pattern' Void
_   ) = forall a. HasRange a => a -> Range
getRange QName
x
    getRange (UnquoteDecl MutualInfo
_ [DefInfo]
i [QName]
_ Expr
_)    = forall a. HasRange a => a -> Range
getRange [DefInfo]
i
    getRange (UnquoteDef [DefInfo]
i [QName]
_ Expr
_)       = forall a. HasRange a => a -> Range
getRange [DefInfo]
i
    getRange (UnquoteData [DefInfo]
i QName
_ UniverseCheck
_ [DefInfo]
j [QName]
_ Expr
_) = forall a. HasRange a => a -> Range
getRange ([DefInfo]
i, [DefInfo]
j)

instance HasRange (Pattern' e) where
    getRange :: Pattern' e -> Range
getRange (VarP BindName
x)           = forall a. HasRange a => a -> Range
getRange BindName
x
    getRange (ConP ConPatInfo
i AmbiguousQName
_ NAPs e
_)        = forall a. HasRange a => a -> Range
getRange ConPatInfo
i
    getRange (ProjP PatInfo
i ProjOrigin
_ AmbiguousQName
_)       = forall a. HasRange a => a -> Range
getRange PatInfo
i
    getRange (DefP PatInfo
i AmbiguousQName
_ NAPs e
_)        = forall a. HasRange a => a -> Range
getRange PatInfo
i
    getRange (WildP PatInfo
i)           = forall a. HasRange a => a -> Range
getRange PatInfo
i
    getRange (AsP PatInfo
i BindName
_ Pattern' e
_)         = forall a. HasRange a => a -> Range
getRange PatInfo
i
    getRange (DotP PatInfo
i e
_)          = forall a. HasRange a => a -> Range
getRange PatInfo
i
    getRange (AbsurdP PatInfo
i)         = forall a. HasRange a => a -> Range
getRange PatInfo
i
    getRange (LitP PatInfo
i Literal
l)          = forall a. HasRange a => a -> Range
getRange PatInfo
i
    getRange (PatternSynP PatInfo
i AmbiguousQName
_ NAPs e
_) = forall a. HasRange a => a -> Range
getRange PatInfo
i
    getRange (RecP PatInfo
i [FieldAssignment' (Pattern' e)]
_)          = forall a. HasRange a => a -> Range
getRange PatInfo
i
    getRange (EqualP PatInfo
i [(e, e)]
_)        = forall a. HasRange a => a -> Range
getRange PatInfo
i
    getRange (WithP PatInfo
i Pattern' e
_)         = forall a. HasRange a => a -> Range
getRange PatInfo
i
    getRange (AnnP PatInfo
i e
_ Pattern' e
_)        = forall a. HasRange a => a -> Range
getRange PatInfo
i

instance HasRange SpineLHS where
    getRange :: SpineLHS -> Range
getRange (SpineLHS LHSInfo
i QName
_ [NamedArg Pattern]
_)  = forall a. HasRange a => a -> Range
getRange LHSInfo
i

instance HasRange LHS where
    getRange :: LHS -> Range
getRange (LHS LHSInfo
i LHSCore
_)   = forall a. HasRange a => a -> Range
getRange LHSInfo
i

instance HasRange (LHSCore' e) where
    getRange :: LHSCore' e -> Range
getRange (LHSHead QName
f [NamedArg (Pattern' e)]
ps)         = forall u t. (HasRange u, HasRange t) => u -> t -> Range
fuseRange QName
f [NamedArg (Pattern' e)]
ps
    getRange (LHSProj AmbiguousQName
d NamedArg (LHSCore' e)
lhscore [NamedArg (Pattern' e)]
ps) = AmbiguousQName
d forall u t. (HasRange u, HasRange t) => u -> t -> Range
`fuseRange` NamedArg (LHSCore' e)
lhscore forall u t. (HasRange u, HasRange t) => u -> t -> Range
`fuseRange` [NamedArg (Pattern' e)]
ps
    getRange (LHSWith LHSCore' e
h [Arg (Pattern' e)]
wps [NamedArg (Pattern' e)]
ps)     = LHSCore' e
h forall u t. (HasRange u, HasRange t) => u -> t -> Range
`fuseRange` [Arg (Pattern' e)]
wps forall u t. (HasRange u, HasRange t) => u -> t -> Range
`fuseRange` [NamedArg (Pattern' e)]
ps

instance HasRange a => HasRange (Clause' a) where
    getRange :: Clause' a -> Range
getRange (Clause a
lhs [ProblemEq]
_ RHS
rhs WhereDeclarations
ds Bool
catchall) = forall a. HasRange a => a -> Range
getRange (a
lhs, RHS
rhs, WhereDeclarations
ds)

instance HasRange RHS where
    getRange :: RHS -> Range
getRange RHS
AbsurdRHS                 = forall a. Range' a
noRange
    getRange (RHS Expr
e Maybe Expr
_)                 = forall a. HasRange a => a -> Range
getRange Expr
e
    getRange (WithRHS QName
_ [WithExpr]
e [Clause]
cs)          = forall u t. (HasRange u, HasRange t) => u -> t -> Range
fuseRange [WithExpr]
e [Clause]
cs
    getRange (RewriteRHS [RewriteEqn]
xes [ProblemEq]
_ RHS
rhs WhereDeclarations
wh) = forall a. HasRange a => a -> Range
getRange ([RewriteEqn]
xes, RHS
rhs, WhereDeclarations
wh)

instance HasRange WhereDeclarations where
  getRange :: WhereDeclarations -> Range
getRange (WhereDecls Maybe ModuleName
_ Bool
_ Maybe Declaration
ds) = forall a. HasRange a => a -> Range
getRange Maybe Declaration
ds

instance HasRange LetBinding where
    getRange :: LetBinding -> Range
getRange (LetBind LetInfo
i ArgInfo
_ BindName
_ Expr
_ Expr
_     ) = forall a. HasRange a => a -> Range
getRange LetInfo
i
    getRange (LetPatBind  LetInfo
i Pattern
_ Expr
_      ) = forall a. HasRange a => a -> Range
getRange LetInfo
i
    getRange (LetApply ModuleInfo
i ModuleName
_ ModuleApplication
_ ScopeCopyInfo
_ ImportDirective
_     ) = forall a. HasRange a => a -> Range
getRange ModuleInfo
i
    getRange (LetOpen  ModuleInfo
i ModuleName
_ ImportDirective
_         ) = forall a. HasRange a => a -> Range
getRange ModuleInfo
i
    getRange (LetDeclaredVariable BindName
x)  = forall a. HasRange a => a -> Range
getRange BindName
x

-- setRange for patterns applies the range to the outermost pattern constructor
instance SetRange (Pattern' a) where
    setRange :: Range -> Pattern' a -> Pattern' a
setRange Range
r (VarP BindName
x)            = forall e. BindName -> Pattern' e
VarP (forall a. SetRange a => Range -> a -> a
setRange Range
r BindName
x)
    setRange Range
r (ConP ConPatInfo
i AmbiguousQName
ns NAPs a
as)       = forall e. ConPatInfo -> AmbiguousQName -> NAPs e -> Pattern' e
ConP (forall a. SetRange a => Range -> a -> a
setRange Range
r ConPatInfo
i) AmbiguousQName
ns NAPs a
as
    setRange Range
r (ProjP PatInfo
_ ProjOrigin
o AmbiguousQName
ns)       = forall e. PatInfo -> ProjOrigin -> AmbiguousQName -> Pattern' e
ProjP (Range -> PatInfo
PatRange Range
r) ProjOrigin
o AmbiguousQName
ns
    setRange Range
r (DefP PatInfo
_ AmbiguousQName
ns NAPs a
as)       = forall e. PatInfo -> AmbiguousQName -> NAPs e -> Pattern' e
DefP (Range -> PatInfo
PatRange Range
r) AmbiguousQName
ns NAPs a
as -- (setRange r n) as
    setRange Range
r (WildP PatInfo
_)            = forall e. PatInfo -> Pattern' e
WildP (Range -> PatInfo
PatRange Range
r)
    setRange Range
r (AsP PatInfo
_ BindName
n Pattern' a
p)          = forall e. PatInfo -> BindName -> Pattern' e -> Pattern' e
AsP (Range -> PatInfo
PatRange Range
r) (forall a. SetRange a => Range -> a -> a
setRange Range
r BindName
n) Pattern' a
p
    setRange Range
r (DotP PatInfo
_ a
e)           = forall e. PatInfo -> e -> Pattern' e
DotP (Range -> PatInfo
PatRange Range
r) a
e
    setRange Range
r (AbsurdP PatInfo
_)          = forall e. PatInfo -> Pattern' e
AbsurdP (Range -> PatInfo
PatRange Range
r)
    setRange Range
r (LitP PatInfo
_ Literal
l)           = forall e. PatInfo -> Literal -> Pattern' e
LitP (Range -> PatInfo
PatRange Range
r) Literal
l
    setRange Range
r (PatternSynP PatInfo
_ AmbiguousQName
n NAPs a
as) = forall e. PatInfo -> AmbiguousQName -> NAPs e -> Pattern' e
PatternSynP (Range -> PatInfo
PatRange Range
r) AmbiguousQName
n NAPs a
as
    setRange Range
r (RecP PatInfo
i [FieldAssignment' (Pattern' a)]
as)          = forall e. PatInfo -> [FieldAssignment' (Pattern' e)] -> Pattern' e
RecP (Range -> PatInfo
PatRange Range
r) [FieldAssignment' (Pattern' a)]
as
    setRange Range
r (EqualP PatInfo
_ [(a, a)]
es)        = forall e. PatInfo -> [(e, e)] -> Pattern' e
EqualP (Range -> PatInfo
PatRange Range
r) [(a, a)]
es
    setRange Range
r (WithP PatInfo
i Pattern' a
p)          = forall e. PatInfo -> Pattern' e -> Pattern' e
WithP (forall a. SetRange a => Range -> a -> a
setRange Range
r PatInfo
i) Pattern' a
p
    setRange Range
r (AnnP PatInfo
i a
a Pattern' a
p)         = forall e. PatInfo -> e -> Pattern' e -> Pattern' e
AnnP (forall a. SetRange a => Range -> a -> a
setRange Range
r PatInfo
i) a
a Pattern' a
p

instance KillRange a => KillRange (Binder' a) where
  killRange :: KillRangeT (Binder' a)
killRange (Binder Maybe Pattern
a a
b) = forall a b c.
(KillRange a, KillRange b) =>
(a -> b -> c) -> a -> b -> c
killRange2 forall a. Maybe Pattern -> a -> Binder' a
Binder Maybe Pattern
a a
b

instance KillRange LamBinding where
  killRange :: LamBinding -> LamBinding
killRange (DomainFree TacticAttr
t NamedArg Binder
x) = forall a b c.
(KillRange a, KillRange b) =>
(a -> b -> c) -> a -> b -> c
killRange2 TacticAttr -> NamedArg Binder -> LamBinding
DomainFree TacticAttr
t NamedArg Binder
x
  killRange (DomainFull TypedBinding
b)   = forall a b. KillRange a => (a -> b) -> a -> b
killRange1 TypedBinding -> LamBinding
DomainFull TypedBinding
b

instance KillRange GeneralizeTelescope where
  killRange :: KillRangeT GeneralizeTelescope
killRange (GeneralizeTel Map QName Name
s Telescope
tel) = Map QName Name -> Telescope -> GeneralizeTelescope
GeneralizeTel Map QName Name
s (forall a. KillRange a => KillRangeT a
killRange Telescope
tel)

instance KillRange DataDefParams where
  killRange :: KillRangeT DataDefParams
killRange (DataDefParams Set Name
s [LamBinding]
tel) = Set Name -> [LamBinding] -> DataDefParams
DataDefParams Set Name
s (forall a. KillRange a => KillRangeT a
killRange [LamBinding]
tel)

instance KillRange TypedBindingInfo where
  killRange :: KillRangeT TypedBindingInfo
killRange (TypedBindingInfo TacticAttr
a Bool
b) = forall a b c.
(KillRange a, KillRange b) =>
(a -> b -> c) -> a -> b -> c
killRange2 TacticAttr -> Bool -> TypedBindingInfo
TypedBindingInfo TacticAttr
a Bool
b

instance KillRange TypedBinding where
  killRange :: TypedBinding -> TypedBinding
killRange (TBind Range
r TypedBindingInfo
t List1 (NamedArg Binder)
xs Expr
e) = forall a b c d e.
(KillRange a, KillRange b, KillRange c, KillRange d) =>
(a -> b -> c -> d -> e) -> a -> b -> c -> d -> e
killRange4 Range
-> TypedBindingInfo
-> List1 (NamedArg Binder)
-> Expr
-> TypedBinding
TBind Range
r TypedBindingInfo
t List1 (NamedArg Binder)
xs Expr
e
  killRange (TLet Range
r List1 LetBinding
lbs)     = forall a b c.
(KillRange a, KillRange b) =>
(a -> b -> c) -> a -> b -> c
killRange2 Range -> List1 LetBinding -> TypedBinding
TLet Range
r List1 LetBinding
lbs

instance KillRange Expr where
  killRange :: Expr -> Expr
killRange (Var Name
x)                  = forall a b. KillRange a => (a -> b) -> a -> b
killRange1 Name -> Expr
Var Name
x
  killRange (Def' QName
x Suffix
v)               = forall a b c.
(KillRange a, KillRange b) =>
(a -> b -> c) -> a -> b -> c
killRange2 QName -> Suffix -> Expr
Def' QName
x Suffix
v
  killRange (Proj ProjOrigin
o AmbiguousQName
x)               = forall a b. KillRange a => (a -> b) -> a -> b
killRange1 (ProjOrigin -> AmbiguousQName -> Expr
Proj ProjOrigin
o) AmbiguousQName
x
  killRange (Con AmbiguousQName
x)                  = forall a b. KillRange a => (a -> b) -> a -> b
killRange1 AmbiguousQName -> Expr
Con AmbiguousQName
x
  killRange (Lit ExprInfo
i Literal
l)                = forall a b c.
(KillRange a, KillRange b) =>
(a -> b -> c) -> a -> b -> c
killRange2 ExprInfo -> Literal -> Expr
Lit ExprInfo
i Literal
l
  killRange (QuestionMark MetaInfo
i InteractionId
ii)      = forall a b c.
(KillRange a, KillRange b) =>
(a -> b -> c) -> a -> b -> c
killRange2 MetaInfo -> InteractionId -> Expr
QuestionMark MetaInfo
i InteractionId
ii
  killRange (Underscore  MetaInfo
i)          = forall a b. KillRange a => (a -> b) -> a -> b
killRange1 MetaInfo -> Expr
Underscore MetaInfo
i
  killRange (Dot ExprInfo
i Expr
e)                = forall a b c.
(KillRange a, KillRange b) =>
(a -> b -> c) -> a -> b -> c
killRange2 ExprInfo -> Expr -> Expr
Dot ExprInfo
i Expr
e
  killRange (App AppInfo
i Expr
e1 NamedArg Expr
e2)            = forall a b c d.
(KillRange a, KillRange b, KillRange c) =>
(a -> b -> c -> d) -> a -> b -> c -> d
killRange3 AppInfo -> Expr -> NamedArg Expr -> Expr
App AppInfo
i Expr
e1 NamedArg Expr
e2
  killRange (WithApp ExprInfo
i Expr
e [Expr]
es)         = forall a b c d.
(KillRange a, KillRange b, KillRange c) =>
(a -> b -> c -> d) -> a -> b -> c -> d
killRange3 ExprInfo -> Expr -> [Expr] -> Expr
WithApp ExprInfo
i Expr
e [Expr]
es
  killRange (Lam ExprInfo
i LamBinding
b Expr
e)              = forall a b c d.
(KillRange a, KillRange b, KillRange c) =>
(a -> b -> c -> d) -> a -> b -> c -> d
killRange3 ExprInfo -> LamBinding -> Expr -> Expr
Lam ExprInfo
i LamBinding
b Expr
e
  killRange (AbsurdLam ExprInfo
i Hiding
h)          = forall a b c.
(KillRange a, KillRange b) =>
(a -> b -> c) -> a -> b -> c
killRange2 ExprInfo -> Hiding -> Expr
AbsurdLam ExprInfo
i Hiding
h
  killRange (ExtendedLam ExprInfo
i DefInfo
n Erased
e QName
d List1 Clause
ps) = forall a b c d e f.
(KillRange a, KillRange b, KillRange c, KillRange d,
 KillRange e) =>
(a -> b -> c -> d -> e -> f) -> a -> b -> c -> d -> e -> f
killRange5 ExprInfo -> DefInfo -> Erased -> QName -> List1 Clause -> Expr
ExtendedLam ExprInfo
i DefInfo
n Erased
e QName
d List1 Clause
ps
  killRange (Pi ExprInfo
i Telescope1
a Expr
b)               = forall a b c d.
(KillRange a, KillRange b, KillRange c) =>
(a -> b -> c -> d) -> a -> b -> c -> d
killRange3 ExprInfo -> Telescope1 -> Expr -> Expr
Pi ExprInfo
i Telescope1
a Expr
b
  killRange (Generalized Set QName
s Expr
x)        = forall a b. KillRange a => (a -> b) -> a -> b
killRange1 (Set QName -> Expr -> Expr
Generalized Set QName
s) Expr
x
  killRange (Fun ExprInfo
i Arg Expr
a Expr
b)              = forall a b c d.
(KillRange a, KillRange b, KillRange c) =>
(a -> b -> c -> d) -> a -> b -> c -> d
killRange3 ExprInfo -> Arg Expr -> Expr -> Expr
Fun ExprInfo
i Arg Expr
a Expr
b
  killRange (Let ExprInfo
i List1 LetBinding
ds Expr
e)             = forall a b c d.
(KillRange a, KillRange b, KillRange c) =>
(a -> b -> c -> d) -> a -> b -> c -> d
killRange3 ExprInfo -> List1 LetBinding -> Expr -> Expr
Let ExprInfo
i List1 LetBinding
ds Expr
e
  killRange (Rec ExprInfo
i RecordAssigns
fs)               = forall a b c.
(KillRange a, KillRange b) =>
(a -> b -> c) -> a -> b -> c
killRange2 ExprInfo -> RecordAssigns -> Expr
Rec ExprInfo
i RecordAssigns
fs
  killRange (RecUpdate ExprInfo
i Expr
e Assigns
fs)       = forall a b c d.
(KillRange a, KillRange b, KillRange c) =>
(a -> b -> c -> d) -> a -> b -> c -> d
killRange3 ExprInfo -> Expr -> Assigns -> Expr
RecUpdate ExprInfo
i Expr
e Assigns
fs
  killRange (ScopedExpr ScopeInfo
s Expr
e)         = forall a b. KillRange a => (a -> b) -> a -> b
killRange1 (ScopeInfo -> Expr -> Expr
ScopedExpr ScopeInfo
s) Expr
e
  killRange (Quote ExprInfo
i)                = forall a b. KillRange a => (a -> b) -> a -> b
killRange1 ExprInfo -> Expr
Quote ExprInfo
i
  killRange (QuoteTerm ExprInfo
i)            = forall a b. KillRange a => (a -> b) -> a -> b
killRange1 ExprInfo -> Expr
QuoteTerm ExprInfo
i
  killRange (Unquote ExprInfo
i)              = forall a b. KillRange a => (a -> b) -> a -> b
killRange1 ExprInfo -> Expr
Unquote ExprInfo
i
  killRange (DontCare Expr
e)             = forall a b. KillRange a => (a -> b) -> a -> b
killRange1 Expr -> Expr
DontCare Expr
e
  killRange (PatternSyn AmbiguousQName
x)           = forall a b. KillRange a => (a -> b) -> a -> b
killRange1 AmbiguousQName -> Expr
PatternSyn AmbiguousQName
x
  killRange (Macro QName
x)                = forall a b. KillRange a => (a -> b) -> a -> b
killRange1 QName -> Expr
Macro QName
x

instance KillRange Suffix where
  killRange :: KillRangeT Suffix
killRange = forall a. a -> a
id

instance KillRange Declaration where
  killRange :: KillRangeT Declaration
killRange (Axiom    KindOfName
p DefInfo
i ArgInfo
a Maybe [Occurrence]
b QName
c Expr
d     ) = forall a b c d e.
(KillRange a, KillRange b, KillRange c, KillRange d) =>
(a -> b -> c -> d -> e) -> a -> b -> c -> d -> e
killRange4 (\DefInfo
i ArgInfo
a QName
c Expr
d -> KindOfName
-> DefInfo
-> ArgInfo
-> Maybe [Occurrence]
-> QName
-> Expr
-> Declaration
Axiom KindOfName
p DefInfo
i ArgInfo
a Maybe [Occurrence]
b QName
c Expr
d) DefInfo
i ArgInfo
a QName
c Expr
d
  killRange (Generalize Set QName
s DefInfo
i ArgInfo
j QName
x Expr
e     ) = forall a b c d e.
(KillRange a, KillRange b, KillRange c, KillRange d) =>
(a -> b -> c -> d -> e) -> a -> b -> c -> d -> e
killRange4 (Set QName -> DefInfo -> ArgInfo -> QName -> Expr -> Declaration
Generalize Set QName
s) DefInfo
i ArgInfo
j QName
x Expr
e
  killRange (Field      DefInfo
i QName
a Arg Expr
b         ) = forall a b c d.
(KillRange a, KillRange b, KillRange c) =>
(a -> b -> c -> d) -> a -> b -> c -> d
killRange3 DefInfo -> QName -> Arg Expr -> Declaration
Field      DefInfo
i QName
a Arg Expr
b
  killRange (Mutual     MutualInfo
i [Declaration]
a           ) = forall a b c.
(KillRange a, KillRange b) =>
(a -> b -> c) -> a -> b -> c
killRange2 MutualInfo -> [Declaration] -> Declaration
Mutual     MutualInfo
i [Declaration]
a
  killRange (Section    Range
i ModuleName
a GeneralizeTelescope
b [Declaration]
c       ) = forall a b c d e.
(KillRange a, KillRange b, KillRange c, KillRange d) =>
(a -> b -> c -> d -> e) -> a -> b -> c -> d -> e
killRange4 Range
-> ModuleName
-> GeneralizeTelescope
-> [Declaration]
-> Declaration
Section    Range
i ModuleName
a GeneralizeTelescope
b [Declaration]
c
  killRange (Apply      ModuleInfo
i ModuleName
a ModuleApplication
b ScopeCopyInfo
c ImportDirective
d     ) = forall a b c d e f.
(KillRange a, KillRange b, KillRange c, KillRange d,
 KillRange e) =>
(a -> b -> c -> d -> e -> f) -> a -> b -> c -> d -> e -> f
killRange5 ModuleInfo
-> ModuleName
-> ModuleApplication
-> ScopeCopyInfo
-> ImportDirective
-> Declaration
Apply      ModuleInfo
i ModuleName
a ModuleApplication
b ScopeCopyInfo
c ImportDirective
d
  killRange (Import     ModuleInfo
i ModuleName
a ImportDirective
b         ) = forall a b c d.
(KillRange a, KillRange b, KillRange c) =>
(a -> b -> c -> d) -> a -> b -> c -> d
killRange3 ModuleInfo -> ModuleName -> ImportDirective -> Declaration
Import     ModuleInfo
i ModuleName
a ImportDirective
b
  killRange (Primitive  DefInfo
i QName
a Arg Expr
b         ) = forall a b c d.
(KillRange a, KillRange b, KillRange c) =>
(a -> b -> c -> d) -> a -> b -> c -> d
killRange3 DefInfo -> QName -> Arg Expr -> Declaration
Primitive  DefInfo
i QName
a Arg Expr
b
  killRange (Pragma     Range
i Pragma
a           ) = Range -> Pragma -> Declaration
Pragma (forall a. KillRange a => KillRangeT a
killRange Range
i) Pragma
a
  killRange (Open       ModuleInfo
i ModuleName
x ImportDirective
dir       ) = forall a b c d.
(KillRange a, KillRange b, KillRange c) =>
(a -> b -> c -> d) -> a -> b -> c -> d
killRange3 ModuleInfo -> ModuleName -> ImportDirective -> Declaration
Open       ModuleInfo
i ModuleName
x ImportDirective
dir
  killRange (ScopedDecl ScopeInfo
a [Declaration]
d           ) = forall a b. KillRange a => (a -> b) -> a -> b
killRange1 (ScopeInfo -> [Declaration] -> Declaration
ScopedDecl ScopeInfo
a) [Declaration]
d
  killRange (FunDef  DefInfo
i QName
a Delayed
b [Clause]
c          ) = forall a b c d e.
(KillRange a, KillRange b, KillRange c, KillRange d) =>
(a -> b -> c -> d -> e) -> a -> b -> c -> d -> e
killRange4 DefInfo -> QName -> Delayed -> [Clause] -> Declaration
FunDef  DefInfo
i QName
a Delayed
b [Clause]
c
  killRange (DataSig DefInfo
i QName
a GeneralizeTelescope
b Expr
c          ) = forall a b c d e.
(KillRange a, KillRange b, KillRange c, KillRange d) =>
(a -> b -> c -> d -> e) -> a -> b -> c -> d -> e
killRange4 DefInfo -> QName -> GeneralizeTelescope -> Expr -> Declaration
DataSig DefInfo
i QName
a GeneralizeTelescope
b Expr
c
  killRange (DataDef DefInfo
i QName
a UniverseCheck
b DataDefParams
c [Declaration]
d        ) = forall a b c d e f.
(KillRange a, KillRange b, KillRange c, KillRange d,
 KillRange e) =>
(a -> b -> c -> d -> e -> f) -> a -> b -> c -> d -> e -> f
killRange5 DefInfo
-> QName
-> UniverseCheck
-> DataDefParams
-> [Declaration]
-> Declaration
DataDef DefInfo
i QName
a UniverseCheck
b DataDefParams
c [Declaration]
d
  killRange (RecSig  DefInfo
i QName
a GeneralizeTelescope
b Expr
c          ) = forall a b c d e.
(KillRange a, KillRange b, KillRange c, KillRange d) =>
(a -> b -> c -> d -> e) -> a -> b -> c -> d -> e
killRange4 DefInfo -> QName -> GeneralizeTelescope -> Expr -> Declaration
RecSig  DefInfo
i QName
a GeneralizeTelescope
b Expr
c
  killRange (RecDef  DefInfo
i QName
a UniverseCheck
b RecordDirectives
c DataDefParams
d Expr
e [Declaration]
f    ) = forall a b c d e f g h.
(KillRange a, KillRange b, KillRange c, KillRange d, KillRange e,
 KillRange f, KillRange g) =>
(a -> b -> c -> d -> e -> f -> g -> h)
-> a -> b -> c -> d -> e -> f -> g -> h
killRange7 DefInfo
-> QName
-> UniverseCheck
-> RecordDirectives
-> DataDefParams
-> Expr
-> [Declaration]
-> Declaration
RecDef  DefInfo
i QName
a UniverseCheck
b RecordDirectives
c DataDefParams
d Expr
e [Declaration]
f
  killRange (PatternSynDef QName
x [Arg BindName]
xs Pattern' Void
p     ) = forall a b c d.
(KillRange a, KillRange b, KillRange c) =>
(a -> b -> c -> d) -> a -> b -> c -> d
killRange3 QName -> [Arg BindName] -> Pattern' Void -> Declaration
PatternSynDef QName
x [Arg BindName]
xs Pattern' Void
p
  killRange (UnquoteDecl MutualInfo
mi [DefInfo]
i [QName]
x Expr
e     ) = forall a b c d e.
(KillRange a, KillRange b, KillRange c, KillRange d) =>
(a -> b -> c -> d -> e) -> a -> b -> c -> d -> e
killRange4 MutualInfo -> [DefInfo] -> [QName] -> Expr -> Declaration
UnquoteDecl MutualInfo
mi [DefInfo]
i [QName]
x Expr
e
  killRange (UnquoteDef [DefInfo]
i [QName]
x Expr
e         ) = forall a b c d.
(KillRange a, KillRange b, KillRange c) =>
(a -> b -> c -> d) -> a -> b -> c -> d
killRange3 [DefInfo] -> [QName] -> Expr -> Declaration
UnquoteDef [DefInfo]
i [QName]
x Expr
e
  killRange (UnquoteData [DefInfo]
i QName
xs UniverseCheck
uc [DefInfo]
j [QName]
cs Expr
e) = forall a b c d e f g.
(KillRange a, KillRange b, KillRange c, KillRange d, KillRange e,
 KillRange f) =>
(a -> b -> c -> d -> e -> f -> g)
-> a -> b -> c -> d -> e -> f -> g
killRange6 [DefInfo]
-> QName
-> UniverseCheck
-> [DefInfo]
-> [QName]
-> Expr
-> Declaration
UnquoteData [DefInfo]
i QName
xs UniverseCheck
uc [DefInfo]
j [QName]
cs Expr
e

instance KillRange ModuleApplication where
  killRange :: KillRangeT ModuleApplication
killRange (SectionApp Telescope
a ModuleName
b [NamedArg Expr]
c  ) = forall a b c d.
(KillRange a, KillRange b, KillRange c) =>
(a -> b -> c -> d) -> a -> b -> c -> d
killRange3 Telescope -> ModuleName -> [NamedArg Expr] -> ModuleApplication
SectionApp Telescope
a ModuleName
b [NamedArg Expr]
c
  killRange (RecordModuleInstance ModuleName
a) = forall a b. KillRange a => (a -> b) -> a -> b
killRange1 ModuleName -> ModuleApplication
RecordModuleInstance ModuleName
a

instance KillRange ScopeCopyInfo where
  killRange :: KillRangeT ScopeCopyInfo
killRange (ScopeCopyInfo Ren ModuleName
a Ren QName
b) = forall a b c.
(KillRange a, KillRange b) =>
(a -> b -> c) -> a -> b -> c
killRange2 Ren ModuleName -> Ren QName -> ScopeCopyInfo
ScopeCopyInfo Ren ModuleName
a Ren QName
b

instance KillRange e => KillRange (Pattern' e) where
  killRange :: KillRangeT (Pattern' e)
killRange (VarP BindName
x)           = forall a b. KillRange a => (a -> b) -> a -> b
killRange1 forall e. BindName -> Pattern' e
VarP BindName
x
  killRange (ConP ConPatInfo
i AmbiguousQName
a NAPs e
b)        = forall a b c d.
(KillRange a, KillRange b, KillRange c) =>
(a -> b -> c -> d) -> a -> b -> c -> d
killRange3 forall e. ConPatInfo -> AmbiguousQName -> NAPs e -> Pattern' e
ConP ConPatInfo
i AmbiguousQName
a NAPs e
b
  killRange (ProjP PatInfo
i ProjOrigin
o AmbiguousQName
a)       = forall a b c d.
(KillRange a, KillRange b, KillRange c) =>
(a -> b -> c -> d) -> a -> b -> c -> d
killRange3 forall e. PatInfo -> ProjOrigin -> AmbiguousQName -> Pattern' e
ProjP PatInfo
i ProjOrigin
o AmbiguousQName
a
  killRange (DefP PatInfo
i AmbiguousQName
a NAPs e
b)        = forall a b c d.
(KillRange a, KillRange b, KillRange c) =>
(a -> b -> c -> d) -> a -> b -> c -> d
killRange3 forall e. PatInfo -> AmbiguousQName -> NAPs e -> Pattern' e
DefP PatInfo
i AmbiguousQName
a NAPs e
b
  killRange (WildP PatInfo
i)           = forall a b. KillRange a => (a -> b) -> a -> b
killRange1 forall e. PatInfo -> Pattern' e
WildP PatInfo
i
  killRange (AsP PatInfo
i BindName
a Pattern' e
b)         = forall a b c d.
(KillRange a, KillRange b, KillRange c) =>
(a -> b -> c -> d) -> a -> b -> c -> d
killRange3 forall e. PatInfo -> BindName -> Pattern' e -> Pattern' e
AsP PatInfo
i BindName
a Pattern' e
b
  killRange (DotP PatInfo
i e
a)          = forall a b c.
(KillRange a, KillRange b) =>
(a -> b -> c) -> a -> b -> c
killRange2 forall e. PatInfo -> e -> Pattern' e
DotP PatInfo
i e
a
  killRange (AbsurdP PatInfo
i)         = forall a b. KillRange a => (a -> b) -> a -> b
killRange1 forall e. PatInfo -> Pattern' e
AbsurdP PatInfo
i
  killRange (LitP PatInfo
i Literal
l)          = forall a b c.
(KillRange a, KillRange b) =>
(a -> b -> c) -> a -> b -> c
killRange2 forall e. PatInfo -> Literal -> Pattern' e
LitP PatInfo
i Literal
l
  killRange (PatternSynP PatInfo
i AmbiguousQName
a NAPs e
p) = forall a b c d.
(KillRange a, KillRange b, KillRange c) =>
(a -> b -> c -> d) -> a -> b -> c -> d
killRange3 forall e. PatInfo -> AmbiguousQName -> NAPs e -> Pattern' e
PatternSynP PatInfo
i AmbiguousQName
a NAPs e
p
  killRange (RecP PatInfo
i [FieldAssignment' (Pattern' e)]
as)         = forall a b c.
(KillRange a, KillRange b) =>
(a -> b -> c) -> a -> b -> c
killRange2 forall e. PatInfo -> [FieldAssignment' (Pattern' e)] -> Pattern' e
RecP PatInfo
i [FieldAssignment' (Pattern' e)]
as
  killRange (EqualP PatInfo
i [(e, e)]
es)       = forall a b c.
(KillRange a, KillRange b) =>
(a -> b -> c) -> a -> b -> c
killRange2 forall e. PatInfo -> [(e, e)] -> Pattern' e
EqualP PatInfo
i [(e, e)]
es
  killRange (WithP PatInfo
i Pattern' e
p)         = forall a b c.
(KillRange a, KillRange b) =>
(a -> b -> c) -> a -> b -> c
killRange2 forall e. PatInfo -> Pattern' e -> Pattern' e
WithP PatInfo
i Pattern' e
p
  killRange (AnnP PatInfo
i e
a Pattern' e
p)        = forall a b c d.
(KillRange a, KillRange b, KillRange c) =>
(a -> b -> c -> d) -> a -> b -> c -> d
killRange3 forall e. PatInfo -> e -> Pattern' e -> Pattern' e
AnnP PatInfo
i e
a Pattern' e
p

instance KillRange SpineLHS where
  killRange :: KillRangeT SpineLHS
killRange (SpineLHS LHSInfo
i QName
a [NamedArg Pattern]
b)  = forall a b c d.
(KillRange a, KillRange b, KillRange c) =>
(a -> b -> c -> d) -> a -> b -> c -> d
killRange3 LHSInfo -> QName -> [NamedArg Pattern] -> SpineLHS
SpineLHS LHSInfo
i QName
a [NamedArg Pattern]
b

instance KillRange LHS where
  killRange :: KillRangeT LHS
killRange (LHS LHSInfo
i LHSCore
a)   = forall a b c.
(KillRange a, KillRange b) =>
(a -> b -> c) -> a -> b -> c
killRange2 LHSInfo -> LHSCore -> LHS
LHS LHSInfo
i LHSCore
a

instance KillRange e => KillRange (LHSCore' e) where
  killRange :: KillRangeT (LHSCore' e)
killRange (LHSHead QName
a [NamedArg (Pattern' e)]
b)   = forall a b c.
(KillRange a, KillRange b) =>
(a -> b -> c) -> a -> b -> c
killRange2 forall e. QName -> [NamedArg (Pattern' e)] -> LHSCore' e
LHSHead QName
a [NamedArg (Pattern' e)]
b
  killRange (LHSProj AmbiguousQName
a NamedArg (LHSCore' e)
b [NamedArg (Pattern' e)]
c) = forall a b c d.
(KillRange a, KillRange b, KillRange c) =>
(a -> b -> c -> d) -> a -> b -> c -> d
killRange3 forall e.
AmbiguousQName
-> NamedArg (LHSCore' e) -> [NamedArg (Pattern' e)] -> LHSCore' e
LHSProj AmbiguousQName
a NamedArg (LHSCore' e)
b [NamedArg (Pattern' e)]
c
  killRange (LHSWith LHSCore' e
a [Arg (Pattern' e)]
b [NamedArg (Pattern' e)]
c) = forall a b c d.
(KillRange a, KillRange b, KillRange c) =>
(a -> b -> c -> d) -> a -> b -> c -> d
killRange3 forall e.
LHSCore' e
-> [Arg (Pattern' e)] -> [NamedArg (Pattern' e)] -> LHSCore' e
LHSWith LHSCore' e
a [Arg (Pattern' e)]
b [NamedArg (Pattern' e)]
c

instance KillRange a => KillRange (Clause' a) where
  killRange :: KillRangeT (Clause' a)
killRange (Clause a
lhs [ProblemEq]
spats RHS
rhs WhereDeclarations
ds Bool
catchall) = forall a b c d e f.
(KillRange a, KillRange b, KillRange c, KillRange d,
 KillRange e) =>
(a -> b -> c -> d -> e -> f) -> a -> b -> c -> d -> e -> f
killRange5 forall lhs.
lhs
-> [ProblemEq] -> RHS -> WhereDeclarations -> Bool -> Clause' lhs
Clause a
lhs [ProblemEq]
spats RHS
rhs WhereDeclarations
ds Bool
catchall

instance KillRange ProblemEq where
  killRange :: KillRangeT ProblemEq
killRange (ProblemEq Pattern
p Term
v Dom Type
a) = forall a b c d.
(KillRange a, KillRange b, KillRange c) =>
(a -> b -> c -> d) -> a -> b -> c -> d
killRange3 Pattern -> Term -> Dom Type -> ProblemEq
ProblemEq Pattern
p Term
v Dom Type
a

instance KillRange RHS where
  killRange :: RHS -> RHS
killRange RHS
AbsurdRHS                = RHS
AbsurdRHS
  killRange (RHS Expr
e Maybe Expr
c)                = forall a b c.
(KillRange a, KillRange b) =>
(a -> b -> c) -> a -> b -> c
killRange2 Expr -> Maybe Expr -> RHS
RHS Expr
e Maybe Expr
c
  killRange (WithRHS QName
q [WithExpr]
e [Clause]
cs)         = forall a b c d.
(KillRange a, KillRange b, KillRange c) =>
(a -> b -> c -> d) -> a -> b -> c -> d
killRange3 QName -> [WithExpr] -> [Clause] -> RHS
WithRHS QName
q [WithExpr]
e [Clause]
cs
  killRange (RewriteRHS [RewriteEqn]
xes [ProblemEq]
spats RHS
rhs WhereDeclarations
wh) = forall a b c d e.
(KillRange a, KillRange b, KillRange c, KillRange d) =>
(a -> b -> c -> d -> e) -> a -> b -> c -> d -> e
killRange4 [RewriteEqn] -> [ProblemEq] -> RHS -> WhereDeclarations -> RHS
RewriteRHS [RewriteEqn]
xes [ProblemEq]
spats RHS
rhs WhereDeclarations
wh

instance KillRange WhereDeclarations where
  killRange :: KillRangeT WhereDeclarations
killRange (WhereDecls Maybe ModuleName
a Bool
b Maybe Declaration
c) = forall a b c d.
(KillRange a, KillRange b, KillRange c) =>
(a -> b -> c -> d) -> a -> b -> c -> d
killRange3 Maybe ModuleName -> Bool -> Maybe Declaration -> WhereDeclarations
WhereDecls Maybe ModuleName
a Bool
b Maybe Declaration
c

instance KillRange LetBinding where
  killRange :: KillRangeT LetBinding
killRange (LetBind   LetInfo
i ArgInfo
info BindName
a Expr
b Expr
c) = forall a b c d e f.
(KillRange a, KillRange b, KillRange c, KillRange d,
 KillRange e) =>
(a -> b -> c -> d -> e -> f) -> a -> b -> c -> d -> e -> f
killRange5 LetInfo -> ArgInfo -> BindName -> Expr -> Expr -> LetBinding
LetBind LetInfo
i ArgInfo
info BindName
a Expr
b Expr
c
  killRange (LetPatBind LetInfo
i Pattern
a Expr
b       ) = forall a b c d.
(KillRange a, KillRange b, KillRange c) =>
(a -> b -> c -> d) -> a -> b -> c -> d
killRange3 LetInfo -> Pattern -> Expr -> LetBinding
LetPatBind LetInfo
i Pattern
a Expr
b
  killRange (LetApply   ModuleInfo
i ModuleName
a ModuleApplication
b ScopeCopyInfo
c ImportDirective
d   ) = forall a b c d e f.
(KillRange a, KillRange b, KillRange c, KillRange d,
 KillRange e) =>
(a -> b -> c -> d -> e -> f) -> a -> b -> c -> d -> e -> f
killRange5 ModuleInfo
-> ModuleName
-> ModuleApplication
-> ScopeCopyInfo
-> ImportDirective
-> LetBinding
LetApply ModuleInfo
i ModuleName
a ModuleApplication
b ScopeCopyInfo
c ImportDirective
d
  killRange (LetOpen    ModuleInfo
i ModuleName
x ImportDirective
dir     ) = forall a b c d.
(KillRange a, KillRange b, KillRange c) =>
(a -> b -> c -> d) -> a -> b -> c -> d
killRange3 ModuleInfo -> ModuleName -> ImportDirective -> LetBinding
LetOpen  ModuleInfo
i ModuleName
x ImportDirective
dir
  killRange (LetDeclaredVariable BindName
x)  = forall a b. KillRange a => (a -> b) -> a -> b
killRange1 BindName -> LetBinding
LetDeclaredVariable BindName
x

instance NFData Expr
instance NFData ScopeCopyInfo
instance NFData Declaration
instance NFData ModuleApplication
instance NFData Pragma
instance NFData LetBinding
instance NFData a => NFData (Binder' a)
instance NFData LamBinding
instance NFData TypedBinding
instance NFData TypedBindingInfo
instance NFData GeneralizeTelescope
instance NFData DataDefParams
instance NFData ProblemEq
instance NFData lhs => NFData (Clause' lhs)
instance NFData WhereDeclarations
instance NFData RHS
instance NFData SpineLHS
instance NFData LHS
instance NFData e => NFData (LHSCore' e)
instance NFData e => NFData (Pattern' e)

------------------------------------------------------------------------
-- Queries
------------------------------------------------------------------------

-- class AllNames moved to Abstract.Views.DeclaredNames

-- | The name defined by the given axiom.
--
-- Precondition: The declaration has to be a (scoped) 'Axiom'.

axiomName :: Declaration -> QName
axiomName :: Declaration -> QName
axiomName (Axiom KindOfName
_ DefInfo
_ ArgInfo
_ Maybe [Occurrence]
_ QName
q Expr
_)  = QName
q
axiomName (ScopedDecl ScopeInfo
_ (Declaration
d:[Declaration]
_)) = Declaration -> QName
axiomName Declaration
d
axiomName Declaration
_                    = forall a. HasCallStack => a
__IMPOSSIBLE__

-- | Are we in an abstract block?
--
--   In that case some definition is abstract.
class AnyAbstract a where
  anyAbstract :: a -> Bool

instance AnyAbstract a => AnyAbstract [a] where
  anyAbstract :: [a] -> Bool
anyAbstract = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
Fold.any forall a. AnyAbstract a => a -> Bool
anyAbstract

instance AnyAbstract Declaration where
  anyAbstract :: Declaration -> Bool
anyAbstract (Axiom KindOfName
_ DefInfo
i ArgInfo
_ Maybe [Occurrence]
_ QName
_ Expr
_)    = forall t. DefInfo' t -> IsAbstract
defAbstract DefInfo
i forall a. Eq a => a -> a -> Bool
== IsAbstract
AbstractDef
  anyAbstract (Field DefInfo
i QName
_ Arg Expr
_)          = forall t. DefInfo' t -> IsAbstract
defAbstract DefInfo
i forall a. Eq a => a -> a -> Bool
== IsAbstract
AbstractDef
  anyAbstract (Mutual     MutualInfo
_ [Declaration]
ds)      = forall a. AnyAbstract a => a -> Bool
anyAbstract [Declaration]
ds
  anyAbstract (ScopedDecl ScopeInfo
_ [Declaration]
ds)      = forall a. AnyAbstract a => a -> Bool
anyAbstract [Declaration]
ds
  anyAbstract (Section Range
_ ModuleName
_ GeneralizeTelescope
_ [Declaration]
ds)     = forall a. AnyAbstract a => a -> Bool
anyAbstract [Declaration]
ds
  anyAbstract (FunDef DefInfo
i QName
_ Delayed
_ [Clause]
_)       = forall t. DefInfo' t -> IsAbstract
defAbstract DefInfo
i forall a. Eq a => a -> a -> Bool
== IsAbstract
AbstractDef
  anyAbstract (DataDef DefInfo
i QName
_ UniverseCheck
_ DataDefParams
_ [Declaration]
_)    = forall t. DefInfo' t -> IsAbstract
defAbstract DefInfo
i forall a. Eq a => a -> a -> Bool
== IsAbstract
AbstractDef
  anyAbstract (RecDef DefInfo
i QName
_ UniverseCheck
_ RecordDirectives
_ DataDefParams
_ Expr
_ [Declaration]
_) = forall t. DefInfo' t -> IsAbstract
defAbstract DefInfo
i forall a. Eq a => a -> a -> Bool
== IsAbstract
AbstractDef
  anyAbstract (DataSig DefInfo
i QName
_ GeneralizeTelescope
_ Expr
_)      = forall t. DefInfo' t -> IsAbstract
defAbstract DefInfo
i forall a. Eq a => a -> a -> Bool
== IsAbstract
AbstractDef
  anyAbstract (RecSig DefInfo
i QName
_ GeneralizeTelescope
_ Expr
_)       = forall t. DefInfo' t -> IsAbstract
defAbstract DefInfo
i forall a. Eq a => a -> a -> Bool
== IsAbstract
AbstractDef
  anyAbstract Declaration
_                      = forall a. HasCallStack => a
__IMPOSSIBLE__

-- | Turn a name into an expression.

class NameToExpr a where
  nameToExpr :: a -> Expr

-- | Turn an 'AbstractName' into an expression.

instance NameToExpr AbstractName where
  nameToExpr :: AbstractName -> Expr
nameToExpr AbstractName
d =
    case AbstractName -> KindOfName
anameKind AbstractName
d of
      KindOfName
DataName                 -> QName -> Expr
Def QName
x
      KindOfName
RecName                  -> QName -> Expr
Def QName
x
      KindOfName
AxiomName                -> QName -> Expr
Def QName
x
      KindOfName
PrimName                 -> QName -> Expr
Def QName
x
      KindOfName
FunName                  -> QName -> Expr
Def QName
x
      KindOfName
OtherDefName             -> QName -> Expr
Def QName
x
      KindOfName
GeneralizeName           -> QName -> Expr
Def QName
x
      KindOfName
DisallowedGeneralizeName -> QName -> Expr
Def QName
x
      KindOfName
FldName                  -> ProjOrigin -> AmbiguousQName -> Expr
Proj ProjOrigin
ProjSystem AmbiguousQName
ux
      KindOfName
ConName                  -> AmbiguousQName -> Expr
Con AmbiguousQName
ux
      KindOfName
CoConName                -> AmbiguousQName -> Expr
Con AmbiguousQName
ux
      KindOfName
PatternSynName           -> AmbiguousQName -> Expr
PatternSyn AmbiguousQName
ux
      KindOfName
MacroName                -> QName -> Expr
Macro QName
x
      KindOfName
QuotableName             -> AppInfo -> Expr -> NamedArg Expr -> Expr
App (Range -> AppInfo
defaultAppInfo Range
r) (ExprInfo -> Expr
Quote ExprInfo
i) (forall a. a -> NamedArg a
defaultNamedArg forall a b. (a -> b) -> a -> b
$ QName -> Expr
Def QName
x)
    where
    x :: QName
x  = AbstractName -> QName
anameName AbstractName
d
    ux :: AmbiguousQName
ux = QName -> AmbiguousQName
unambiguous QName
x
    r :: Range
r  = forall a. HasRange a => a -> Range
getRange QName
x
    i :: ExprInfo
i  = Range -> ExprInfo
ExprRange Range
r

-- | Turn a 'ResolvedName' into an expression.
--
--   Assumes name is not 'UnknownName'.

instance NameToExpr ResolvedName where
  nameToExpr :: ResolvedName -> Expr
nameToExpr = \case
    VarName Name
x BindingSource
_          -> Name -> Expr
Var Name
x
    DefinedName Access
_ AbstractName
x Suffix
s    -> Suffix -> Expr -> Expr
withSuffix Suffix
s forall a b. (a -> b) -> a -> b
$ forall a. NameToExpr a => a -> Expr
nameToExpr AbstractName
x  -- Can be 'isDefName', 'MacroName', 'QuotableName'.
    FieldName List1 AbstractName
xs         -> ProjOrigin -> AmbiguousQName -> Expr
Proj ProjOrigin
ProjSystem forall b c a. (b -> c) -> (a -> b) -> a -> c
. NonEmpty QName -> AmbiguousQName
AmbQ forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap AbstractName -> QName
anameName forall a b. (a -> b) -> a -> b
$ List1 AbstractName
xs
    ConstructorName Set Induction
_ List1 AbstractName
xs -> AmbiguousQName -> Expr
Con forall b c a. (b -> c) -> (a -> b) -> a -> c
. NonEmpty QName -> AmbiguousQName
AmbQ forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap AbstractName -> QName
anameName forall a b. (a -> b) -> a -> b
$ List1 AbstractName
xs
    PatternSynResName List1 AbstractName
xs -> AmbiguousQName -> Expr
PatternSyn forall b c a. (b -> c) -> (a -> b) -> a -> c
. NonEmpty QName -> AmbiguousQName
AmbQ forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap AbstractName -> QName
anameName forall a b. (a -> b) -> a -> b
$ List1 AbstractName
xs
    ResolvedName
UnknownName          -> forall a. HasCallStack => a
__IMPOSSIBLE__
    where
      withSuffix :: Suffix -> Expr -> Expr
withSuffix Suffix
NoSuffix   Expr
e       = Expr
e
      withSuffix s :: Suffix
s@Suffix{} (Def QName
x) = QName -> Suffix -> Expr
Def' QName
x Suffix
s
      withSuffix Suffix
_          Expr
_       = forall a. HasCallStack => a
__IMPOSSIBLE__

app :: Expr -> [NamedArg Expr] -> Expr
app :: Expr -> [NamedArg Expr] -> Expr
app = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (AppInfo -> Expr -> NamedArg Expr -> Expr
App AppInfo
defaultAppInfo_)

mkLet :: ExprInfo -> [LetBinding] -> Expr -> Expr
mkLet :: ExprInfo -> [LetBinding] -> Expr -> Expr
mkLet ExprInfo
_ []     Expr
e = Expr
e
mkLet ExprInfo
i (LetBinding
d:[LetBinding]
ds) Expr
e = ExprInfo -> List1 LetBinding -> Expr -> Expr
Let ExprInfo
i (LetBinding
d forall a. a -> [a] -> NonEmpty a
:| [LetBinding]
ds) Expr
e

patternToExpr :: Pattern -> Expr
patternToExpr :: Pattern -> Expr
patternToExpr = \case
  VarP BindName
x             -> Name -> Expr
Var (BindName -> Name
unBind BindName
x)
  ConP ConPatInfo
_ AmbiguousQName
c [NamedArg Pattern]
ps        -> AmbiguousQName -> Expr
Con AmbiguousQName
c Expr -> [NamedArg Expr] -> Expr
`app` forall a b. (a -> b) -> [a] -> [b]
map (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Pattern -> Expr
patternToExpr)) [NamedArg Pattern]
ps
  ProjP PatInfo
_ ProjOrigin
o AmbiguousQName
ds       -> ProjOrigin -> AmbiguousQName -> Expr
Proj ProjOrigin
o AmbiguousQName
ds
  DefP PatInfo
_ AmbiguousQName
fs [NamedArg Pattern]
ps       -> QName -> Expr
Def (AmbiguousQName -> QName
headAmbQ AmbiguousQName
fs) Expr -> [NamedArg Expr] -> Expr
`app` forall a b. (a -> b) -> [a] -> [b]
map (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Pattern -> Expr
patternToExpr)) [NamedArg Pattern]
ps
  WildP PatInfo
_            -> MetaInfo -> Expr
Underscore MetaInfo
emptyMetaInfo
  AsP PatInfo
_ BindName
_ Pattern
p          -> Pattern -> Expr
patternToExpr Pattern
p
  DotP PatInfo
_ Expr
e           -> Expr
e
  AbsurdP PatInfo
_          -> MetaInfo -> Expr
Underscore MetaInfo
emptyMetaInfo  -- TODO: could this happen?
  LitP (PatRange Range
r) Literal
l-> ExprInfo -> Literal -> Expr
Lit (Range -> ExprInfo
ExprRange Range
r) Literal
l
  PatternSynP PatInfo
_ AmbiguousQName
c [NamedArg Pattern]
ps -> AmbiguousQName -> Expr
PatternSyn AmbiguousQName
c Expr -> [NamedArg Expr] -> Expr
`app` (forall a b. (a -> b) -> [a] -> [b]
map forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap) Pattern -> Expr
patternToExpr [NamedArg Pattern]
ps
  RecP PatInfo
_ [FieldAssignment' Pattern]
as          -> ExprInfo -> RecordAssigns -> Expr
Rec ExprInfo
exprNoRange forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (forall a b. a -> Either a b
Left forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Pattern -> Expr
patternToExpr) [FieldAssignment' Pattern]
as
  EqualP{}           -> forall a. HasCallStack => a
__IMPOSSIBLE__  -- Andrea TODO: where is this used?
  WithP PatInfo
r Pattern
p          -> forall a. HasCallStack => a
__IMPOSSIBLE__
  AnnP PatInfo
_ Expr
_ Pattern
p         -> Pattern -> Expr
patternToExpr Pattern
p

type PatternSynDefn = ([Arg Name], Pattern' Void)
type PatternSynDefns = Map QName PatternSynDefn

lambdaLiftExpr :: [Name] -> Expr -> Expr
lambdaLiftExpr :: [Name] -> Expr -> Expr
lambdaLiftExpr [Name]
ns Expr
e
  = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr
      (\ Name
n -> ExprInfo -> LamBinding -> Expr -> Expr
Lam ExprInfo
exprNoRange (NamedArg Binder -> LamBinding
mkDomainFree forall a b. (a -> b) -> a -> b
$ forall a. a -> NamedArg a
defaultNamedArg forall a b. (a -> b) -> a -> b
$ Name -> Binder
mkBinder_ Name
n))
      Expr
e
      [Name]
ns

-- NOTE: This is only used on expressions that come from right-hand sides of pattern synonyms, and
-- thus does not have to handle all forms of expressions.
class SubstExpr a where
  substExpr :: [(Name, Expr)] -> a -> a

  default substExpr
    :: (Functor t, SubstExpr b, t b ~ a)
    => [(Name, Expr)] -> a -> a
  substExpr = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. SubstExpr a => [(Name, Expr)] -> a -> a
substExpr

instance SubstExpr a => SubstExpr (Maybe a)
instance SubstExpr a => SubstExpr [a]
instance SubstExpr a => SubstExpr (List1 a)
instance SubstExpr a => SubstExpr (Arg a)
instance SubstExpr a => SubstExpr (Named name a)
instance SubstExpr a => SubstExpr (FieldAssignment' a)

instance (SubstExpr a, SubstExpr b) => SubstExpr (a, b) where
  substExpr :: [(Name, Expr)] -> (a, b) -> (a, b)
substExpr [(Name, Expr)]
s (a
x, b
y) = (forall a. SubstExpr a => [(Name, Expr)] -> a -> a
substExpr [(Name, Expr)]
s a
x, forall a. SubstExpr a => [(Name, Expr)] -> a -> a
substExpr [(Name, Expr)]
s b
y)

instance (SubstExpr a, SubstExpr b) => SubstExpr (Either a b) where
  substExpr :: [(Name, Expr)] -> Either a b -> Either a b
substExpr [(Name, Expr)]
s (Left a
x)  = forall a b. a -> Either a b
Left (forall a. SubstExpr a => [(Name, Expr)] -> a -> a
substExpr [(Name, Expr)]
s a
x)
  substExpr [(Name, Expr)]
s (Right b
y) = forall a b. b -> Either a b
Right (forall a. SubstExpr a => [(Name, Expr)] -> a -> a
substExpr [(Name, Expr)]
s b
y)

instance SubstExpr C.Name where
  substExpr :: [(Name, Expr)] -> Name -> Name
substExpr [(Name, Expr)]
_ = forall a. a -> a
id

instance SubstExpr ModuleName where
  substExpr :: [(Name, Expr)] -> ModuleName -> ModuleName
substExpr [(Name, Expr)]
_ = forall a. a -> a
id

instance SubstExpr Expr where
  substExpr :: [(Name, Expr)] -> Expr -> Expr
substExpr [(Name, Expr)]
s Expr
e = case Expr
e of
    Var Name
n           -> forall a. a -> Maybe a -> a
fromMaybe Expr
e (forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Name
n [(Name, Expr)]
s)
    Con AmbiguousQName
_           -> Expr
e
    Proj{}          -> Expr
e
    Def' QName
_ Suffix
_        -> Expr
e
    PatternSyn{}    -> Expr
e
    Lit ExprInfo
_ Literal
_         -> Expr
e
    Underscore   MetaInfo
_  -> Expr
e
    App  AppInfo
i Expr
e NamedArg Expr
e'     -> AppInfo -> Expr -> NamedArg Expr -> Expr
App AppInfo
i (forall a. SubstExpr a => [(Name, Expr)] -> a -> a
substExpr [(Name, Expr)]
s Expr
e) (forall a. SubstExpr a => [(Name, Expr)] -> a -> a
substExpr [(Name, Expr)]
s NamedArg Expr
e')
    Rec  ExprInfo
i RecordAssigns
nes      -> ExprInfo -> RecordAssigns -> Expr
Rec ExprInfo
i (forall a. SubstExpr a => [(Name, Expr)] -> a -> a
substExpr [(Name, Expr)]
s RecordAssigns
nes)
    ScopedExpr ScopeInfo
si Expr
e -> ScopeInfo -> Expr -> Expr
ScopedExpr ScopeInfo
si (forall a. SubstExpr a => [(Name, Expr)] -> a -> a
substExpr [(Name, Expr)]
s Expr
e)
    -- The below cannot appear in pattern synonym right-hand sides
    QuestionMark{}  -> forall a. HasCallStack => a
__IMPOSSIBLE__
    Dot{}           -> forall a. HasCallStack => a
__IMPOSSIBLE__
    WithApp{}       -> forall a. HasCallStack => a
__IMPOSSIBLE__
    Lam{}           -> forall a. HasCallStack => a
__IMPOSSIBLE__
    AbsurdLam{}     -> forall a. HasCallStack => a
__IMPOSSIBLE__
    ExtendedLam{}   -> forall a. HasCallStack => a
__IMPOSSIBLE__
    Pi{}            -> forall a. HasCallStack => a
__IMPOSSIBLE__
    Generalized{}   -> forall a. HasCallStack => a
__IMPOSSIBLE__
    Fun{}           -> forall a. HasCallStack => a
__IMPOSSIBLE__
    Let{}           -> forall a. HasCallStack => a
__IMPOSSIBLE__
    RecUpdate{}     -> forall a. HasCallStack => a
__IMPOSSIBLE__
    Quote{}         -> forall a. HasCallStack => a
__IMPOSSIBLE__
    QuoteTerm{}     -> forall a. HasCallStack => a
__IMPOSSIBLE__
    Unquote{}       -> forall a. HasCallStack => a
__IMPOSSIBLE__
    DontCare{}      -> forall a. HasCallStack => a
__IMPOSSIBLE__
    Macro{}         -> forall a. HasCallStack => a
__IMPOSSIBLE__

-- TODO: more informative failure
insertImplicitPatSynArgs
  :: HasRange a
  => (Range -> a)
  -> Range
  -> [Arg Name]
  -> [NamedArg a]
  -> Maybe ([(Name, a)], [Arg Name])
insertImplicitPatSynArgs :: forall a.
HasRange a =>
(Range -> a)
-> Range
-> [Arg Name]
-> [NamedArg a]
-> Maybe ([(Name, a)], [Arg Name])
insertImplicitPatSynArgs Range -> a
wild Range
r [Arg Name]
ns [Arg (Named_ a)]
as = Range
-> [Arg Name]
-> [Arg (Named_ a)]
-> Maybe ([(Name, a)], [Arg Name])
matchArgs Range
r [Arg Name]
ns [Arg (Named_ a)]
as
  where
    matchNextArg :: Range
-> Arg Name -> [Arg (Named_ a)] -> Maybe (a, [Arg (Named_ a)])
matchNextArg Range
r Arg Name
n as :: [Arg (Named_ a)]
as@(~(Arg (Named_ a)
a : [Arg (Named_ a)]
as'))
      | forall {a}.
(NameOf a ~ NamedName, LensHiding a, LensNamed a) =>
Arg Name -> [a] -> Bool
matchNext Arg Name
n [Arg (Named_ a)]
as = forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. NamedArg a -> a
namedArg Arg (Named_ a)
a, [Arg (Named_ a)]
as')
      | forall a. LensHiding a => a -> Bool
visible Arg Name
n      = forall a. Maybe a
Nothing
      | Bool
otherwise      = forall (m :: * -> *) a. Monad m => a -> m a
return (Range -> a
wild Range
r, [Arg (Named_ a)]
as)

    matchNext :: Arg Name -> [a] -> Bool
matchNext Arg Name
_ [] = Bool
False
    matchNext Arg Name
n (a
a:[a]
as) = forall a b. (LensHiding a, LensHiding b) => a -> b -> Bool
sameHiding Arg Name
n a
a Bool -> Bool -> Bool
&& forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
True (ArgName
x forall a. Eq a => a -> a -> Bool
==) (forall a. (LensNamed a, NameOf a ~ NamedName) => a -> Maybe ArgName
bareNameOf a
a)
      where
        x :: ArgName
x = Name -> ArgName
C.nameToRawName forall a b. (a -> b) -> a -> b
$ Name -> Name
nameConcrete forall a b. (a -> b) -> a -> b
$ forall e. Arg e -> e
unArg Arg Name
n

    matchArgs :: Range
-> [Arg Name]
-> [Arg (Named_ a)]
-> Maybe ([(Name, a)], [Arg Name])
matchArgs Range
r [] []     = forall (m :: * -> *) a. Monad m => a -> m a
return ([], [])
    matchArgs Range
r [] [Arg (Named_ a)]
as     = forall a. Maybe a
Nothing
    matchArgs Range
r (Arg Name
n:[Arg Name]
ns) [] | forall a. LensHiding a => a -> Bool
visible Arg Name
n = forall (m :: * -> *) a. Monad m => a -> m a
return ([], Arg Name
n forall a. a -> [a] -> [a]
: [Arg Name]
ns)    -- under-applied
    matchArgs Range
r (Arg Name
n:[Arg Name]
ns) [Arg (Named_ a)]
as = do
      (a
p, [Arg (Named_ a)]
as) <- Range
-> Arg Name -> [Arg (Named_ a)] -> Maybe (a, [Arg (Named_ a)])
matchNextArg Range
r Arg Name
n [Arg (Named_ a)]
as
      forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first ((forall e. Arg e -> e
unArg Arg Name
n, a
p) forall a. a -> [a] -> [a]
:) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Range
-> [Arg Name]
-> [Arg (Named_ a)]
-> Maybe ([(Name, a)], [Arg Name])
matchArgs (forall a. HasRange a => a -> Range
getRange a
p) [Arg Name]
ns [Arg (Named_ a)]
as

------------------------------------------------------------------------
-- Declaration spines
------------------------------------------------------------------------

-- | Declaration spines. Used in debugging to make it easy to see
-- where constructors such as 'ScopedDecl' and 'Mutual' are placed.

data DeclarationSpine
  = AxiomS
  | GeneralizeS
  | FieldS
  | PrimitiveS
  | MutualS [DeclarationSpine]
  | SectionS [DeclarationSpine]
  | ApplyS
  | ImportS
  | PragmaS
  | OpenS
  | FunDefS [ClauseSpine]
  | DataSigS
  | DataDefS
  | RecSigS
  | RecDefS [DeclarationSpine]
  | PatternSynDefS
  | UnquoteDeclS
  | UnquoteDefS
  | UnquoteDataS
  | ScopedDeclS [DeclarationSpine]
  deriving Int -> DeclarationSpine -> ShowS
[DeclarationSpine] -> ShowS
DeclarationSpine -> ArgName
forall a.
(Int -> a -> ShowS) -> (a -> ArgName) -> ([a] -> ShowS) -> Show a
showList :: [DeclarationSpine] -> ShowS
$cshowList :: [DeclarationSpine] -> ShowS
show :: DeclarationSpine -> ArgName
$cshow :: DeclarationSpine -> ArgName
showsPrec :: Int -> DeclarationSpine -> ShowS
$cshowsPrec :: Int -> DeclarationSpine -> ShowS
Show

-- | Clause spines.

data ClauseSpine = ClauseS RHSSpine WhereDeclarationsSpine
  deriving Int -> ClauseSpine -> ShowS
[ClauseSpine] -> ShowS
ClauseSpine -> ArgName
forall a.
(Int -> a -> ShowS) -> (a -> ArgName) -> ([a] -> ShowS) -> Show a
showList :: [ClauseSpine] -> ShowS
$cshowList :: [ClauseSpine] -> ShowS
show :: ClauseSpine -> ArgName
$cshow :: ClauseSpine -> ArgName
showsPrec :: Int -> ClauseSpine -> ShowS
$cshowsPrec :: Int -> ClauseSpine -> ShowS
Show

-- | Right-hand side spines.

data RHSSpine
  = RHSS
  | AbsurdRHSS
  | WithRHSS [ClauseSpine]
  | RewriteRHSS RHSSpine WhereDeclarationsSpine
  deriving Int -> RHSSpine -> ShowS
[RHSSpine] -> ShowS
RHSSpine -> ArgName
forall a.
(Int -> a -> ShowS) -> (a -> ArgName) -> ([a] -> ShowS) -> Show a
showList :: [RHSSpine] -> ShowS
$cshowList :: [RHSSpine] -> ShowS
show :: RHSSpine -> ArgName
$cshow :: RHSSpine -> ArgName
showsPrec :: Int -> RHSSpine -> ShowS
$cshowsPrec :: Int -> RHSSpine -> ShowS
Show

-- | Spines corresponding to 'WhereDeclarations' values.

data WhereDeclarationsSpine = WhereDeclsS (Maybe DeclarationSpine)
  deriving Int -> WhereDeclarationsSpine -> ShowS
[WhereDeclarationsSpine] -> ShowS
WhereDeclarationsSpine -> ArgName
forall a.
(Int -> a -> ShowS) -> (a -> ArgName) -> ([a] -> ShowS) -> Show a
showList :: [WhereDeclarationsSpine] -> ShowS
$cshowList :: [WhereDeclarationsSpine] -> ShowS
show :: WhereDeclarationsSpine -> ArgName
$cshow :: WhereDeclarationsSpine -> ArgName
showsPrec :: Int -> WhereDeclarationsSpine -> ShowS
$cshowsPrec :: Int -> WhereDeclarationsSpine -> ShowS
Show

-- | The declaration spine corresponding to a declaration.

declarationSpine :: Declaration -> DeclarationSpine
declarationSpine :: Declaration -> DeclarationSpine
declarationSpine = \case
  Axiom KindOfName
_ DefInfo
_ ArgInfo
_ Maybe [Occurrence]
_ QName
_ Expr
_       -> DeclarationSpine
AxiomS
  Generalize Set QName
_ DefInfo
_ ArgInfo
_ QName
_ Expr
_    -> DeclarationSpine
GeneralizeS
  Field DefInfo
_ QName
_ Arg Expr
_             -> DeclarationSpine
FieldS
  Primitive DefInfo
_ QName
_ Arg Expr
_         -> DeclarationSpine
PrimitiveS
  Mutual MutualInfo
_ [Declaration]
ds             -> [DeclarationSpine] -> DeclarationSpine
MutualS (forall a b. (a -> b) -> [a] -> [b]
map Declaration -> DeclarationSpine
declarationSpine [Declaration]
ds)
  Section Range
_ ModuleName
_ GeneralizeTelescope
_ [Declaration]
ds        -> [DeclarationSpine] -> DeclarationSpine
SectionS (forall a b. (a -> b) -> [a] -> [b]
map Declaration -> DeclarationSpine
declarationSpine [Declaration]
ds)
  Apply ModuleInfo
_ ModuleName
_ ModuleApplication
_ ScopeCopyInfo
_ ImportDirective
_         -> DeclarationSpine
ApplyS
  Import ModuleInfo
_ ModuleName
_ ImportDirective
_            -> DeclarationSpine
ImportS
  Pragma Range
_ Pragma
_              -> DeclarationSpine
PragmaS
  Open ModuleInfo
_ ModuleName
_ ImportDirective
_              -> DeclarationSpine
OpenS
  FunDef DefInfo
_ QName
_ Delayed
_ [Clause]
cs         -> [ClauseSpine] -> DeclarationSpine
FunDefS (forall a b. (a -> b) -> [a] -> [b]
map Clause -> ClauseSpine
clauseSpine [Clause]
cs)
  DataSig DefInfo
_ QName
_ GeneralizeTelescope
_ Expr
_         -> DeclarationSpine
DataSigS
  DataDef DefInfo
_ QName
_ UniverseCheck
_ DataDefParams
_ [Declaration]
_       -> DeclarationSpine
DataDefS
  RecSig DefInfo
_ QName
_ GeneralizeTelescope
_ Expr
_          -> DeclarationSpine
RecSigS
  RecDef DefInfo
_ QName
_ UniverseCheck
_ RecordDirectives
_ DataDefParams
_ Expr
_ [Declaration]
ds   -> [DeclarationSpine] -> DeclarationSpine
RecDefS (forall a b. (a -> b) -> [a] -> [b]
map Declaration -> DeclarationSpine
declarationSpine [Declaration]
ds)
  PatternSynDef QName
_ [Arg BindName]
_ Pattern' Void
_     -> DeclarationSpine
PatternSynDefS
  UnquoteDecl MutualInfo
_ [DefInfo]
_ [QName]
_ Expr
_     -> DeclarationSpine
UnquoteDeclS
  UnquoteDef [DefInfo]
_ [QName]
_ Expr
_        -> DeclarationSpine
UnquoteDefS
  UnquoteData [DefInfo]
_ QName
_ UniverseCheck
_ [DefInfo]
_ [QName]
_ Expr
_ -> DeclarationSpine
UnquoteDataS
  ScopedDecl ScopeInfo
_ [Declaration]
ds         -> [DeclarationSpine] -> DeclarationSpine
ScopedDeclS (forall a b. (a -> b) -> [a] -> [b]
map Declaration -> DeclarationSpine
declarationSpine [Declaration]
ds)

-- | The clause spine corresponding to a clause.

clauseSpine :: Clause -> ClauseSpine
clauseSpine :: Clause -> ClauseSpine
clauseSpine (Clause LHS
_ [ProblemEq]
_ RHS
rhs WhereDeclarations
ws Bool
_) =
  RHSSpine -> WhereDeclarationsSpine -> ClauseSpine
ClauseS (RHS -> RHSSpine
rhsSpine RHS
rhs) (WhereDeclarations -> WhereDeclarationsSpine
whereDeclarationsSpine WhereDeclarations
ws)

-- | The right-hand side spine corresponding to a right-hand side.

rhsSpine :: RHS -> RHSSpine
rhsSpine :: RHS -> RHSSpine
rhsSpine = \case
  RHS Expr
_ Maybe Expr
_               -> RHSSpine
RHSS
  RHS
AbsurdRHS             -> RHSSpine
AbsurdRHSS
  WithRHS QName
_ [WithExpr]
_ [Clause]
cs        -> [ClauseSpine] -> RHSSpine
WithRHSS (forall a b. (a -> b) -> [a] -> [b]
map Clause -> ClauseSpine
clauseSpine [Clause]
cs)
  RewriteRHS [RewriteEqn]
_ [ProblemEq]
_ RHS
rhs WhereDeclarations
ws ->
    RHSSpine -> WhereDeclarationsSpine -> RHSSpine
RewriteRHSS (RHS -> RHSSpine
rhsSpine RHS
rhs) (WhereDeclarations -> WhereDeclarationsSpine
whereDeclarationsSpine WhereDeclarations
ws)

-- | The spine corresponding to a 'WhereDeclarations' value.

whereDeclarationsSpine :: WhereDeclarations -> WhereDeclarationsSpine
whereDeclarationsSpine :: WhereDeclarations -> WhereDeclarationsSpine
whereDeclarationsSpine (WhereDecls Maybe ModuleName
_ Bool
_ Maybe Declaration
md) =
  Maybe DeclarationSpine -> WhereDeclarationsSpine
WhereDeclsS (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Declaration -> DeclarationSpine
declarationSpine Maybe Declaration
md)