{-| 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 qualified Data.Set as Set
import Data.Set (Set)
import Data.Void

import GHC.Generics (Generic)

import Agda.Syntax.Concrete (FieldAssignment'(..))
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.List1 (List1, pattern (:|))
import qualified Agda.Utils.List1 as List1
import Agda.Utils.Null
import Agda.Syntax.Common.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 -> String
(Int -> BindName -> ShowS)
-> (BindName -> String) -> ([BindName] -> ShowS) -> Show BindName
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> BindName -> ShowS
showsPrec :: Int -> BindName -> ShowS
$cshow :: BindName -> String
show :: BindName -> String
$cshowList :: [BindName] -> ShowS
showList :: [BindName] -> ShowS
Show, BindName -> Range
(BindName -> Range) -> HasRange BindName
forall a. (a -> Range) -> HasRange a
$cgetRange :: BindName -> Range
getRange :: BindName -> Range
HasRange, KillRangeT BindName
KillRangeT BindName -> KillRange BindName
forall a. KillRangeT a -> KillRange a
$ckillRange :: KillRangeT BindName
killRange :: KillRangeT BindName
KillRange, HasRange BindName
HasRange BindName =>
(Range -> KillRangeT BindName) -> SetRange BindName
Range -> KillRangeT BindName
forall a. HasRange a => (Range -> a -> a) -> SetRange a
$csetRange :: Range -> KillRangeT BindName
setRange :: Range -> KillRangeT BindName
SetRange, BindName -> ()
(BindName -> ()) -> NFData BindName
forall a. (a -> ()) -> NFData a
$crnf :: BindName -> ()
rnf :: 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
    = (NameId -> NameId -> Bool
forall a. Eq a => a -> a -> Bool
(==) (NameId -> NameId -> Bool)
-> (Name -> NameId) -> Name -> Name -> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` Name -> NameId
nameId) Name
n Name
m
      Bool -> Bool -> Bool
&& (Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
(==) (Name -> Name -> Bool) -> (Name -> Name) -> Name -> Name -> 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
    = (NameId -> NameId -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (NameId -> NameId -> Ordering)
-> (Name -> NameId) -> Name -> Name -> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` Name -> NameId
nameId) Name
n Name
m
      Ordering -> Ordering -> Ordering
forall a. Monoid a => a -> a -> a
`mappend` (Name -> Name -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Name -> Name -> Ordering)
-> (Name -> Name) -> Name -> Name -> Ordering
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 -> String
(Int -> Expr -> ShowS)
-> (Expr -> String) -> ([Expr] -> ShowS) -> Show Expr
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Expr -> ShowS
showsPrec :: Int -> Expr -> ShowS
$cshow :: Expr -> String
show :: Expr -> String
$cshowList :: [Expr] -> ShowS
showList :: [Expr] -> ShowS
Show, (forall x. Expr -> Rep Expr x)
-> (forall x. Rep Expr x -> Expr) -> Generic Expr
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
$cfrom :: forall x. Expr -> Rep Expr x
from :: forall x. Expr -> Rep Expr x
$cto :: forall x. Rep Expr x -> Expr
to :: forall x. Rep Expr x -> Expr
Generic)

-- | Pattern synonym for regular 'Def'.
pattern Def :: QName -> Expr
pattern $mDef :: forall {r}. Expr -> (QName -> r) -> ((# #) -> r) -> r
$bDef :: QName -> Expr
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
    | Set QName -> Bool
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
(ScopeCopyInfo -> ScopeCopyInfo -> Bool)
-> (ScopeCopyInfo -> ScopeCopyInfo -> Bool) -> Eq ScopeCopyInfo
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: ScopeCopyInfo -> ScopeCopyInfo -> Bool
== :: ScopeCopyInfo -> ScopeCopyInfo -> Bool
$c/= :: ScopeCopyInfo -> ScopeCopyInfo -> Bool
/= :: ScopeCopyInfo -> ScopeCopyInfo -> Bool
Eq, Int -> ScopeCopyInfo -> ShowS
[ScopeCopyInfo] -> ShowS
ScopeCopyInfo -> String
(Int -> ScopeCopyInfo -> ShowS)
-> (ScopeCopyInfo -> String)
-> ([ScopeCopyInfo] -> ShowS)
-> Show ScopeCopyInfo
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> ScopeCopyInfo -> ShowS
showsPrec :: Int -> ScopeCopyInfo -> ShowS
$cshow :: ScopeCopyInfo -> String
show :: ScopeCopyInfo -> String
$cshowList :: [ScopeCopyInfo] -> ShowS
showList :: [ScopeCopyInfo] -> ShowS
Show, (forall x. ScopeCopyInfo -> Rep ScopeCopyInfo x)
-> (forall x. Rep ScopeCopyInfo x -> ScopeCopyInfo)
-> Generic ScopeCopyInfo
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
$cfrom :: forall x. ScopeCopyInfo -> Rep ScopeCopyInfo x
from :: forall x. ScopeCopyInfo -> Rep ScopeCopyInfo x
$cto :: forall x. Rep ScopeCopyInfo x -> ScopeCopyInfo
to :: forall x. Rep ScopeCopyInfo x -> ScopeCopyInfo
Generic)

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

instance Pretty ScopeCopyInfo where
  pretty :: ScopeCopyInfo -> Doc
pretty ScopeCopyInfo
i = [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
vcat [ String -> Ren ModuleName -> Doc
forall {l} {a}.
(IsList l, Pretty a, Pretty (Item l)) =>
String -> Map a l -> Doc
prRen String
"renModules =" (ScopeCopyInfo -> Ren ModuleName
renModules ScopeCopyInfo
i)
                  , String -> Ren QName -> Doc
forall {l} {a}.
(IsList l, Pretty a, Pretty (Item l)) =>
String -> Map a l -> Doc
prRen String
"renNames   =" (ScopeCopyInfo -> Ren QName
renNames ScopeCopyInfo
i) ]
    where
      prRen :: String -> Map a l -> Doc
prRen String
s Map a l
r = [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
sep [ String -> Doc
forall a. String -> Doc a
text String
s, Int -> Doc -> Doc
forall a. Int -> Doc a -> Doc a
nest Int
2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
vcat (((a, Item l) -> Doc) -> [(a, Item l)] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (a, Item l) -> Doc
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) <- Map a l -> [(a, l)]
forall k a. Map k a -> [(k, a)]
Map.toList Map a l
r, Item l
v <- l -> [Item l]
forall l. IsList l => l -> [Item l]
List1.toList l
vs ]
      pr :: (a, a) -> Doc
pr (a
x, a
y) = a -> Doc
forall a. Pretty a => a -> Doc
pretty a
x Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> Doc
"->" Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> a -> 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 Erased ModuleName GeneralizeTelescope [Declaration]
  | Apply      ModuleInfo Erased 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
  | FunDef     DefInfo QName [Clause] -- ^ sequence of function clauses
  | DataSig    DefInfo Erased QName GeneralizeTelescope Type -- ^ lone data signature
  | DataDef    DefInfo QName UniverseCheck DataDefParams [Constructor]
  | RecSig     DefInfo Erased 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) -> Dummy@,
      --   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
  | UnfoldingDecl Range [QName]
    -- ^ Only for highlighting the unfolded names
  deriving (Int -> Declaration -> ShowS
[Declaration] -> ShowS
Declaration -> String
(Int -> Declaration -> ShowS)
-> (Declaration -> String)
-> ([Declaration] -> ShowS)
-> Show Declaration
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Declaration -> ShowS
showsPrec :: Int -> Declaration -> ShowS
$cshow :: Declaration -> String
show :: Declaration -> String
$cshowList :: [Declaration] -> ShowS
showList :: [Declaration] -> ShowS
Show, (forall x. Declaration -> Rep Declaration x)
-> (forall x. Rep Declaration x -> Declaration)
-> Generic Declaration
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
$cfrom :: forall x. Declaration -> Rep Declaration x
from :: forall x. Declaration -> Rep Declaration x
$cto :: forall x. Rep Declaration x -> Declaration
to :: forall x. Rep Declaration x -> Declaration
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 -> String
(Int -> ModuleApplication -> ShowS)
-> (ModuleApplication -> String)
-> ([ModuleApplication] -> ShowS)
-> Show ModuleApplication
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> ModuleApplication -> ShowS
showsPrec :: Int -> ModuleApplication -> ShowS
$cshow :: ModuleApplication -> String
show :: ModuleApplication -> String
$cshowList :: [ModuleApplication] -> ShowS
showList :: [ModuleApplication] -> ShowS
Show, ModuleApplication -> ModuleApplication -> Bool
(ModuleApplication -> ModuleApplication -> Bool)
-> (ModuleApplication -> ModuleApplication -> Bool)
-> Eq ModuleApplication
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: ModuleApplication -> ModuleApplication -> Bool
== :: ModuleApplication -> ModuleApplication -> Bool
$c/= :: ModuleApplication -> ModuleApplication -> Bool
/= :: ModuleApplication -> ModuleApplication -> Bool
Eq, (forall x. ModuleApplication -> Rep ModuleApplication x)
-> (forall x. Rep ModuleApplication x -> ModuleApplication)
-> Generic ModuleApplication
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
$cfrom :: forall x. ModuleApplication -> Rep ModuleApplication x
from :: forall x. ModuleApplication -> Rep ModuleApplication x
$cto :: forall x. Rep ModuleApplication x -> ModuleApplication
to :: forall x. Rep ModuleApplication x -> ModuleApplication
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 -> String
(Int -> Pragma -> ShowS)
-> (Pragma -> String) -> ([Pragma] -> ShowS) -> Show Pragma
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Pragma -> ShowS
showsPrec :: Int -> Pragma -> ShowS
$cshow :: Pragma -> String
show :: Pragma -> String
$cshowList :: [Pragma] -> ShowS
showList :: [Pragma] -> ShowS
Show, Pragma -> Pragma -> Bool
(Pragma -> Pragma -> Bool)
-> (Pragma -> Pragma -> Bool) -> Eq Pragma
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Pragma -> Pragma -> Bool
== :: Pragma -> Pragma -> Bool
$c/= :: Pragma -> Pragma -> Bool
/= :: Pragma -> Pragma -> Bool
Eq, (forall x. Pragma -> Rep Pragma x)
-> (forall x. Rep Pragma x -> Pragma) -> Generic Pragma
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
$cfrom :: forall x. Pragma -> Rep Pragma x
from :: forall x. Pragma -> Rep Pragma x
$cto :: forall x. Rep Pragma x -> Pragma
to :: forall x. Rep Pragma x -> Pragma
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 Erased 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 -> String
(Int -> LetBinding -> ShowS)
-> (LetBinding -> String)
-> ([LetBinding] -> ShowS)
-> Show LetBinding
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> LetBinding -> ShowS
showsPrec :: Int -> LetBinding -> ShowS
$cshow :: LetBinding -> String
show :: LetBinding -> String
$cshowList :: [LetBinding] -> ShowS
showList :: [LetBinding] -> ShowS
Show, LetBinding -> LetBinding -> Bool
(LetBinding -> LetBinding -> Bool)
-> (LetBinding -> LetBinding -> Bool) -> Eq LetBinding
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: LetBinding -> LetBinding -> Bool
== :: LetBinding -> LetBinding -> Bool
$c/= :: LetBinding -> LetBinding -> Bool
/= :: LetBinding -> LetBinding -> Bool
Eq, (forall x. LetBinding -> Rep LetBinding x)
-> (forall x. Rep LetBinding x -> LetBinding) -> Generic LetBinding
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
$cfrom :: forall x. LetBinding -> Rep LetBinding x
from :: forall x. LetBinding -> Rep LetBinding x
$cto :: forall x. Rep LetBinding x -> LetBinding
to :: forall x. Rep LetBinding x -> LetBinding
Generic)

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

type TacticAttr = Maybe (Ranged 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
[Binder' a] -> ShowS
Binder' a -> String
(Int -> Binder' a -> ShowS)
-> (Binder' a -> String)
-> ([Binder' a] -> ShowS)
-> Show (Binder' a)
forall a. Show a => Int -> Binder' a -> ShowS
forall a. Show a => [Binder' a] -> ShowS
forall a. Show a => Binder' a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Show a => Int -> Binder' a -> ShowS
showsPrec :: Int -> Binder' a -> ShowS
$cshow :: forall a. Show a => Binder' a -> String
show :: Binder' a -> String
$cshowList :: forall a. Show a => [Binder' a] -> ShowS
showList :: [Binder' a] -> ShowS
Show, Binder' a -> Binder' a -> Bool
(Binder' a -> Binder' a -> Bool)
-> (Binder' a -> Binder' a -> Bool) -> Eq (Binder' a)
forall a. Eq a => Binder' a -> Binder' a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$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
/= :: Binder' a -> Binder' a -> Bool
Eq, (forall a b. (a -> b) -> Binder' a -> Binder' b)
-> (forall a b. a -> Binder' b -> Binder' a) -> Functor Binder'
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
$cfmap :: forall a b. (a -> b) -> Binder' a -> Binder' b
fmap :: forall a b. (a -> b) -> Binder' a -> Binder' b
$c<$ :: forall a b. a -> Binder' b -> Binder' a
<$ :: forall a b. a -> Binder' b -> Binder' a
Functor, (forall m. Monoid m => Binder' m -> m)
-> (forall m a. Monoid m => (a -> m) -> Binder' a -> m)
-> (forall m a. Monoid m => (a -> m) -> Binder' a -> m)
-> (forall a b. (a -> b -> b) -> b -> Binder' a -> b)
-> (forall a b. (a -> b -> b) -> b -> Binder' a -> b)
-> (forall b a. (b -> a -> b) -> b -> Binder' a -> b)
-> (forall b a. (b -> a -> b) -> b -> Binder' a -> b)
-> (forall a. (a -> a -> a) -> Binder' a -> a)
-> (forall a. (a -> a -> a) -> Binder' a -> a)
-> (forall a. Binder' a -> [a])
-> (forall a. Binder' a -> Bool)
-> (forall a. Binder' a -> Int)
-> (forall a. Eq a => a -> Binder' a -> Bool)
-> (forall a. Ord a => Binder' a -> a)
-> (forall a. Ord a => Binder' a -> a)
-> (forall a. Num a => Binder' a -> a)
-> (forall a. Num a => Binder' a -> a)
-> Foldable Binder'
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
$cfold :: forall m. Monoid m => Binder' m -> m
fold :: forall m. Monoid m => Binder' m -> 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
foldMap' :: forall m a. Monoid m => (a -> m) -> Binder' a -> m
$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
foldr' :: forall a b. (a -> b -> 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
foldl' :: forall b a. (b -> a -> b) -> b -> Binder' a -> b
$cfoldr1 :: forall a. (a -> a -> a) -> Binder' a -> a
foldr1 :: forall a. (a -> a -> a) -> Binder' a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> Binder' a -> a
foldl1 :: forall a. (a -> a -> a) -> Binder' a -> a
$ctoList :: forall a. Binder' a -> [a]
toList :: forall a. Binder' a -> [a]
$cnull :: forall a. Binder' a -> Bool
null :: forall a. Binder' a -> Bool
$clength :: forall a. Binder' a -> Int
length :: forall a. Binder' a -> Int
$celem :: forall a. Eq a => a -> Binder' a -> Bool
elem :: forall a. Eq a => a -> Binder' a -> Bool
$cmaximum :: forall a. Ord a => Binder' a -> a
maximum :: forall a. Ord a => Binder' a -> a
$cminimum :: forall a. Ord a => Binder' a -> a
minimum :: forall a. Ord a => Binder' a -> a
$csum :: forall a. Num a => Binder' a -> a
sum :: forall a. Num a => Binder' a -> a
$cproduct :: forall a. Num a => Binder' a -> a
product :: forall a. Num a => Binder' a -> a
Foldable, Functor Binder'
Foldable Binder'
(Functor Binder', Foldable Binder') =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> Binder' a -> f (Binder' b))
-> (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 (m :: * -> *) a.
    Monad m =>
    Binder' (m a) -> m (Binder' a))
-> Traversable 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)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Binder' a -> f (Binder' b)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Binder' a -> f (Binder' b)
$csequenceA :: forall (f :: * -> *) a.
Applicative f =>
Binder' (f a) -> f (Binder' a)
sequenceA :: forall (f :: * -> *) a.
Applicative f =>
Binder' (f a) -> f (Binder' a)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Binder' a -> m (Binder' b)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Binder' a -> m (Binder' b)
$csequence :: forall (m :: * -> *) a. Monad m => Binder' (m a) -> m (Binder' a)
sequence :: forall (m :: * -> *) a. Monad m => Binder' (m a) -> m (Binder' a)
Traversable, (forall x. Binder' a -> Rep (Binder' a) x)
-> (forall x. Rep (Binder' a) x -> Binder' a)
-> Generic (Binder' a)
forall x. Rep (Binder' a) x -> Binder' a
forall x. Binder' a -> Rep (Binder' a) x
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
$cfrom :: forall a x. Binder' a -> Rep (Binder' a) x
from :: forall x. Binder' a -> Rep (Binder' a) x
$cto :: forall a x. Rep (Binder' a) x -> Binder' a
to :: forall x. Rep (Binder' a) x -> Binder' a
Generic)

type Binder = Binder' BindName

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

mkBinder_ :: Name -> Binder
mkBinder_ :: Name -> Binder
mkBinder_ = BindName -> Binder
forall a. a -> Binder' a
mkBinder (BindName -> Binder) -> (Name -> BindName) -> Name -> Binder
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) (Pattern -> (Pattern, a)) -> Maybe Pattern -> Maybe (Pattern, 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 -> String
(Int -> LamBinding -> ShowS)
-> (LamBinding -> String)
-> ([LamBinding] -> ShowS)
-> Show LamBinding
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> LamBinding -> ShowS
showsPrec :: Int -> LamBinding -> ShowS
$cshow :: LamBinding -> String
show :: LamBinding -> String
$cshowList :: [LamBinding] -> ShowS
showList :: [LamBinding] -> ShowS
Show, LamBinding -> LamBinding -> Bool
(LamBinding -> LamBinding -> Bool)
-> (LamBinding -> LamBinding -> Bool) -> Eq LamBinding
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: LamBinding -> LamBinding -> Bool
== :: LamBinding -> LamBinding -> Bool
$c/= :: LamBinding -> LamBinding -> Bool
/= :: LamBinding -> LamBinding -> Bool
Eq, (forall x. LamBinding -> Rep LamBinding x)
-> (forall x. Rep LamBinding x -> LamBinding) -> Generic LamBinding
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
$cfrom :: forall x. LamBinding -> Rep LamBinding x
from :: forall x. LamBinding -> Rep LamBinding x
$cto :: forall x. Rep LamBinding x -> LamBinding
to :: forall x. Rep LamBinding x -> LamBinding
Generic)

mkDomainFree :: NamedArg Binder -> LamBinding
mkDomainFree :: NamedArg Binder -> LamBinding
mkDomainFree = TacticAttr -> NamedArg Binder -> LamBinding
DomainFree TacticAttr
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 -> String
(Int -> TypedBindingInfo -> ShowS)
-> (TypedBindingInfo -> String)
-> ([TypedBindingInfo] -> ShowS)
-> Show TypedBindingInfo
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> TypedBindingInfo -> ShowS
showsPrec :: Int -> TypedBindingInfo -> ShowS
$cshow :: TypedBindingInfo -> String
show :: TypedBindingInfo -> String
$cshowList :: [TypedBindingInfo] -> ShowS
showList :: [TypedBindingInfo] -> ShowS
Show, TypedBindingInfo -> TypedBindingInfo -> Bool
(TypedBindingInfo -> TypedBindingInfo -> Bool)
-> (TypedBindingInfo -> TypedBindingInfo -> Bool)
-> Eq TypedBindingInfo
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: TypedBindingInfo -> TypedBindingInfo -> Bool
== :: TypedBindingInfo -> TypedBindingInfo -> Bool
$c/= :: TypedBindingInfo -> TypedBindingInfo -> Bool
/= :: TypedBindingInfo -> TypedBindingInfo -> Bool
Eq, (forall x. TypedBindingInfo -> Rep TypedBindingInfo x)
-> (forall x. Rep TypedBindingInfo x -> TypedBindingInfo)
-> Generic TypedBindingInfo
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
$cfrom :: forall x. TypedBindingInfo -> Rep TypedBindingInfo x
from :: forall x. TypedBindingInfo -> Rep TypedBindingInfo x
$cto :: forall x. Rep TypedBindingInfo x -> TypedBindingInfo
to :: forall x. Rep TypedBindingInfo x -> TypedBindingInfo
Generic)

defaultTbInfo :: TypedBindingInfo
defaultTbInfo :: TypedBindingInfo
defaultTbInfo = TypedBindingInfo
  { tbTacticAttr :: TacticAttr
tbTacticAttr = TacticAttr
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 -> String
(Int -> TypedBinding -> ShowS)
-> (TypedBinding -> String)
-> (Telescope -> ShowS)
-> Show TypedBinding
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> TypedBinding -> ShowS
showsPrec :: Int -> TypedBinding -> ShowS
$cshow :: TypedBinding -> String
show :: TypedBinding -> String
$cshowList :: Telescope -> ShowS
showList :: Telescope -> ShowS
Show, TypedBinding -> TypedBinding -> Bool
(TypedBinding -> TypedBinding -> Bool)
-> (TypedBinding -> TypedBinding -> Bool) -> Eq TypedBinding
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: TypedBinding -> TypedBinding -> Bool
== :: TypedBinding -> TypedBinding -> Bool
$c/= :: TypedBinding -> TypedBinding -> Bool
/= :: TypedBinding -> TypedBinding -> Bool
Eq, (forall x. TypedBinding -> Rep TypedBinding x)
-> (forall x. Rep TypedBinding x -> TypedBinding)
-> Generic TypedBinding
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
$cfrom :: forall x. TypedBinding -> Rep TypedBinding x
from :: forall x. TypedBinding -> Rep TypedBinding x
$cto :: forall x. Rep TypedBinding x -> TypedBinding
to :: forall x. Rep TypedBinding x -> TypedBinding
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
_ []     = Maybe TypedBinding
forall a. Maybe a
Nothing
mkTLet Range
r (LetBinding
d:[LetBinding]
ds) = TypedBinding -> Maybe TypedBinding
forall a. a -> Maybe a
Just (TypedBinding -> Maybe TypedBinding)
-> TypedBinding -> Maybe TypedBinding
forall a b. (a -> b) -> a -> b
$ Range -> List1 LetBinding -> TypedBinding
TLet Range
r (LetBinding
d LetBinding -> [LetBinding] -> List1 LetBinding
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 TypedBinding -> Telescope -> Telescope1
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 -> String
(Int -> GeneralizeTelescope -> ShowS)
-> (GeneralizeTelescope -> String)
-> ([GeneralizeTelescope] -> ShowS)
-> Show GeneralizeTelescope
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> GeneralizeTelescope -> ShowS
showsPrec :: Int -> GeneralizeTelescope -> ShowS
$cshow :: GeneralizeTelescope -> String
show :: GeneralizeTelescope -> String
$cshowList :: [GeneralizeTelescope] -> ShowS
showList :: [GeneralizeTelescope] -> ShowS
Show, GeneralizeTelescope -> GeneralizeTelescope -> Bool
(GeneralizeTelescope -> GeneralizeTelescope -> Bool)
-> (GeneralizeTelescope -> GeneralizeTelescope -> Bool)
-> Eq GeneralizeTelescope
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: GeneralizeTelescope -> GeneralizeTelescope -> Bool
== :: GeneralizeTelescope -> GeneralizeTelescope -> Bool
$c/= :: GeneralizeTelescope -> GeneralizeTelescope -> Bool
/= :: GeneralizeTelescope -> GeneralizeTelescope -> Bool
Eq, (forall x. GeneralizeTelescope -> Rep GeneralizeTelescope x)
-> (forall x. Rep GeneralizeTelescope x -> GeneralizeTelescope)
-> Generic GeneralizeTelescope
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
$cfrom :: forall x. GeneralizeTelescope -> Rep GeneralizeTelescope x
from :: forall x. GeneralizeTelescope -> Rep GeneralizeTelescope x
$cto :: forall x. Rep GeneralizeTelescope x -> GeneralizeTelescope
to :: forall x. Rep GeneralizeTelescope x -> GeneralizeTelescope
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 -> String
(Int -> DataDefParams -> ShowS)
-> (DataDefParams -> String)
-> ([DataDefParams] -> ShowS)
-> Show DataDefParams
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> DataDefParams -> ShowS
showsPrec :: Int -> DataDefParams -> ShowS
$cshow :: DataDefParams -> String
show :: DataDefParams -> String
$cshowList :: [DataDefParams] -> ShowS
showList :: [DataDefParams] -> ShowS
Show, DataDefParams -> DataDefParams -> Bool
(DataDefParams -> DataDefParams -> Bool)
-> (DataDefParams -> DataDefParams -> Bool) -> Eq DataDefParams
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: DataDefParams -> DataDefParams -> Bool
== :: DataDefParams -> DataDefParams -> Bool
$c/= :: DataDefParams -> DataDefParams -> Bool
/= :: DataDefParams -> DataDefParams -> Bool
Eq, (forall x. DataDefParams -> Rep DataDefParams x)
-> (forall x. Rep DataDefParams x -> DataDefParams)
-> Generic DataDefParams
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
$cfrom :: forall x. DataDefParams -> Rep DataDefParams x
from :: forall x. DataDefParams -> Rep DataDefParams x
$cto :: forall x. Rep DataDefParams x -> DataDefParams
to :: forall x. Rep DataDefParams x -> DataDefParams
Generic)

noDataDefParams :: DataDefParams
noDataDefParams :: DataDefParams
noDataDefParams = Set Name -> [LamBinding] -> DataDefParams
DataDefParams Set Name
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 -> String
(Int -> ProblemEq -> ShowS)
-> (ProblemEq -> String)
-> ([ProblemEq] -> ShowS)
-> Show ProblemEq
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> ProblemEq -> ShowS
showsPrec :: Int -> ProblemEq -> ShowS
$cshow :: ProblemEq -> String
show :: ProblemEq -> String
$cshowList :: [ProblemEq] -> ShowS
showList :: [ProblemEq] -> ShowS
Show, (forall x. ProblemEq -> Rep ProblemEq x)
-> (forall x. Rep ProblemEq x -> ProblemEq) -> Generic ProblemEq
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
$cfrom :: forall x. ProblemEq -> Rep ProblemEq x
from :: forall x. ProblemEq -> Rep ProblemEq x
$cto :: forall x. Rep ProblemEq x -> ProblemEq
to :: forall x. Rep ProblemEq x -> ProblemEq
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
[Clause' lhs] -> ShowS
Clause' lhs -> String
(Int -> Clause' lhs -> ShowS)
-> (Clause' lhs -> String)
-> ([Clause' lhs] -> ShowS)
-> Show (Clause' lhs)
forall lhs. Show lhs => Int -> Clause' lhs -> ShowS
forall lhs. Show lhs => [Clause' lhs] -> ShowS
forall lhs. Show lhs => Clause' lhs -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall lhs. Show lhs => Int -> Clause' lhs -> ShowS
showsPrec :: Int -> Clause' lhs -> ShowS
$cshow :: forall lhs. Show lhs => Clause' lhs -> String
show :: Clause' lhs -> String
$cshowList :: forall lhs. Show lhs => [Clause' lhs] -> ShowS
showList :: [Clause' lhs] -> ShowS
Show, (forall a b. (a -> b) -> Clause' a -> Clause' b)
-> (forall a b. a -> Clause' b -> Clause' a) -> Functor Clause'
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
$cfmap :: forall a b. (a -> b) -> Clause' a -> Clause' b
fmap :: forall a b. (a -> b) -> Clause' a -> Clause' b
$c<$ :: forall a b. a -> Clause' b -> Clause' a
<$ :: forall a b. a -> Clause' b -> Clause' a
Functor, (forall m. Monoid m => Clause' m -> m)
-> (forall m a. Monoid m => (a -> m) -> Clause' a -> m)
-> (forall m a. Monoid m => (a -> m) -> Clause' a -> m)
-> (forall a b. (a -> b -> b) -> b -> Clause' a -> b)
-> (forall a b. (a -> b -> b) -> b -> Clause' a -> b)
-> (forall b a. (b -> a -> b) -> b -> Clause' a -> b)
-> (forall b a. (b -> a -> b) -> b -> Clause' a -> b)
-> (forall a. (a -> a -> a) -> Clause' a -> a)
-> (forall a. (a -> a -> a) -> Clause' a -> a)
-> (forall a. Clause' a -> [a])
-> (forall lhs. Clause' lhs -> Bool)
-> (forall a. Clause' a -> Int)
-> (forall a. Eq a => a -> Clause' a -> Bool)
-> (forall a. Ord a => Clause' a -> a)
-> (forall a. Ord a => Clause' a -> a)
-> (forall a. Num a => Clause' a -> a)
-> (forall a. Num a => Clause' a -> a)
-> Foldable Clause'
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
$cfold :: forall m. Monoid m => Clause' m -> m
fold :: forall m. Monoid m => Clause' m -> 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
foldMap' :: forall m a. Monoid m => (a -> m) -> Clause' a -> m
$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
foldr' :: forall a b. (a -> b -> 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
foldl' :: forall b a. (b -> a -> b) -> b -> Clause' a -> b
$cfoldr1 :: forall a. (a -> a -> a) -> Clause' a -> a
foldr1 :: forall a. (a -> a -> a) -> Clause' a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> Clause' a -> a
foldl1 :: forall a. (a -> a -> a) -> Clause' a -> a
$ctoList :: forall a. Clause' a -> [a]
toList :: forall a. Clause' a -> [a]
$cnull :: forall lhs. Clause' lhs -> Bool
null :: forall lhs. Clause' lhs -> Bool
$clength :: forall a. Clause' a -> Int
length :: forall a. Clause' a -> Int
$celem :: forall a. Eq a => a -> Clause' a -> Bool
elem :: forall a. Eq a => a -> Clause' a -> Bool
$cmaximum :: forall a. Ord a => Clause' a -> a
maximum :: forall a. Ord a => Clause' a -> a
$cminimum :: forall a. Ord a => Clause' a -> a
minimum :: forall a. Ord a => Clause' a -> a
$csum :: forall a. Num a => Clause' a -> a
sum :: forall a. Num a => Clause' a -> a
$cproduct :: forall a. Num a => Clause' a -> a
product :: forall a. Num a => Clause' a -> a
Foldable, Functor Clause'
Foldable Clause'
(Functor Clause', Foldable Clause') =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> Clause' a -> f (Clause' b))
-> (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 (m :: * -> *) a.
    Monad m =>
    Clause' (m a) -> m (Clause' a))
-> Traversable 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)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Clause' a -> f (Clause' b)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Clause' a -> f (Clause' b)
$csequenceA :: forall (f :: * -> *) a.
Applicative f =>
Clause' (f a) -> f (Clause' a)
sequenceA :: forall (f :: * -> *) a.
Applicative f =>
Clause' (f a) -> f (Clause' a)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Clause' a -> m (Clause' b)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Clause' a -> m (Clause' b)
$csequence :: forall (m :: * -> *) a. Monad m => Clause' (m a) -> m (Clause' a)
sequence :: forall (m :: * -> *) a. Monad m => Clause' (m a) -> m (Clause' a)
Traversable, Clause' lhs -> Clause' lhs -> Bool
(Clause' lhs -> Clause' lhs -> Bool)
-> (Clause' lhs -> Clause' lhs -> Bool) -> Eq (Clause' lhs)
forall lhs. Eq lhs => Clause' lhs -> Clause' lhs -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$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
/= :: Clause' lhs -> Clause' lhs -> Bool
Eq, (forall x. Clause' lhs -> Rep (Clause' lhs) x)
-> (forall x. Rep (Clause' lhs) x -> Clause' lhs)
-> Generic (Clause' lhs)
forall x. Rep (Clause' lhs) x -> Clause' lhs
forall x. Clause' lhs -> Rep (Clause' lhs) x
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
$cfrom :: forall lhs x. Clause' lhs -> Rep (Clause' lhs) x
from :: forall x. Clause' lhs -> Rep (Clause' lhs) x
$cto :: forall lhs x. Rep (Clause' lhs) x -> Clause' lhs
to :: forall x. Rep (Clause' lhs) x -> Clause' lhs
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 -> String
(Int -> WhereDeclarations -> ShowS)
-> (WhereDeclarations -> String)
-> ([WhereDeclarations] -> ShowS)
-> Show WhereDeclarations
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> WhereDeclarations -> ShowS
showsPrec :: Int -> WhereDeclarations -> ShowS
$cshow :: WhereDeclarations -> String
show :: WhereDeclarations -> String
$cshowList :: [WhereDeclarations] -> ShowS
showList :: [WhereDeclarations] -> ShowS
Show, WhereDeclarations -> WhereDeclarations -> Bool
(WhereDeclarations -> WhereDeclarations -> Bool)
-> (WhereDeclarations -> WhereDeclarations -> Bool)
-> Eq WhereDeclarations
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: WhereDeclarations -> WhereDeclarations -> Bool
== :: WhereDeclarations -> WhereDeclarations -> Bool
$c/= :: WhereDeclarations -> WhereDeclarations -> Bool
/= :: WhereDeclarations -> WhereDeclarations -> Bool
Eq, (forall x. WhereDeclarations -> Rep WhereDeclarations x)
-> (forall x. Rep WhereDeclarations x -> WhereDeclarations)
-> Generic WhereDeclarations
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
$cfrom :: forall x. WhereDeclarations -> Rep WhereDeclarations x
from :: forall x. WhereDeclarations -> Rep WhereDeclarations x
$cto :: forall x. Rep WhereDeclarations x -> WhereDeclarations
to :: forall x. Rep WhereDeclarations x -> WhereDeclarations
Generic)

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

noWhereDecls :: WhereDeclarations
noWhereDecls :: WhereDeclarations
noWhereDecls = WhereDeclarations
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] (List1 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 -> String
(Int -> RHS -> ShowS)
-> (RHS -> String) -> ([RHS] -> ShowS) -> Show RHS
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> RHS -> ShowS
showsPrec :: Int -> RHS -> ShowS
$cshow :: RHS -> String
show :: RHS -> String
$cshowList :: [RHS] -> ShowS
showList :: [RHS] -> ShowS
Show, (forall x. RHS -> Rep RHS x)
-> (forall x. Rep RHS x -> RHS) -> Generic RHS
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
$cfrom :: forall x. RHS -> Rep RHS x
from :: forall x. RHS -> Rep RHS x
$cto :: forall x. Rep RHS x -> RHS
to :: forall x. Rep RHS x -> RHS
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 Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
== Expr
e'
  RHS
AbsurdRHS        == RHS
AbsurdRHS           = Bool
True
  WithRHS QName
a [WithExpr]
b List1 Clause
c    == WithRHS QName
a' [WithExpr]
b' List1 Clause
c'    = (QName
a QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
a') Bool -> Bool -> Bool
&& ([WithExpr]
b [WithExpr] -> [WithExpr] -> Bool
forall a. Eq a => a -> a -> Bool
== [WithExpr]
b') Bool -> Bool -> Bool
&& (List1 Clause
c List1 Clause -> List1 Clause -> Bool
forall a. Eq a => a -> a -> Bool
== List1 Clause
c')
  RewriteRHS [RewriteEqn]
a [ProblemEq]
b RHS
c WhereDeclarations
d == RewriteRHS [RewriteEqn]
a' [ProblemEq]
b' RHS
c' WhereDeclarations
d' = [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and [ [RewriteEqn]
a [RewriteEqn] -> [RewriteEqn] -> Bool
forall a. Eq a => a -> a -> Bool
== [RewriteEqn]
a', [ProblemEq]
b [ProblemEq] -> [ProblemEq] -> Bool
forall a. Eq a => a -> a -> Bool
== [ProblemEq]
b', RHS
c RHS -> RHS -> Bool
forall a. Eq a => a -> a -> Bool
== RHS
c' , WhereDeclarations
d WhereDeclarations -> WhereDeclarations -> Bool
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 -> String
(Int -> SpineLHS -> ShowS)
-> (SpineLHS -> String) -> ([SpineLHS] -> ShowS) -> Show SpineLHS
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> SpineLHS -> ShowS
showsPrec :: Int -> SpineLHS -> ShowS
$cshow :: SpineLHS -> String
show :: SpineLHS -> String
$cshowList :: [SpineLHS] -> ShowS
showList :: [SpineLHS] -> ShowS
Show, SpineLHS -> SpineLHS -> Bool
(SpineLHS -> SpineLHS -> Bool)
-> (SpineLHS -> SpineLHS -> Bool) -> Eq SpineLHS
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: SpineLHS -> SpineLHS -> Bool
== :: SpineLHS -> SpineLHS -> Bool
$c/= :: SpineLHS -> SpineLHS -> Bool
/= :: SpineLHS -> SpineLHS -> Bool
Eq, (forall x. SpineLHS -> Rep SpineLHS x)
-> (forall x. Rep SpineLHS x -> SpineLHS) -> Generic SpineLHS
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
$cfrom :: forall x. SpineLHS -> Rep SpineLHS x
from :: forall x. SpineLHS -> Rep SpineLHS x
$cto :: forall x. Rep SpineLHS x -> SpineLHS
to :: forall x. Rep SpineLHS x -> SpineLHS
Generic)

-- | Ignore 'Range' when comparing 'LHS's.
instance Eq LHS where
  LHS LHSInfo
_ LHSCore
core == :: LHS -> LHS -> Bool
== LHS LHSInfo
_ LHSCore
core' = LHSCore
core LHSCore -> LHSCore -> Bool
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 -> String
(Int -> LHS -> ShowS)
-> (LHS -> String) -> ([LHS] -> ShowS) -> Show LHS
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> LHS -> ShowS
showsPrec :: Int -> LHS -> ShowS
$cshow :: LHS -> String
show :: LHS -> String
$cshowList :: [LHS] -> ShowS
showList :: [LHS] -> ShowS
Show, (forall x. LHS -> Rep LHS x)
-> (forall x. Rep LHS x -> LHS) -> Generic LHS
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
$cfrom :: forall x. LHS -> Rep LHS x
from :: forall x. LHS -> Rep LHS x
$cto :: forall x. Rep LHS x -> LHS
to :: forall x. Rep LHS x -> LHS
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
[LHSCore' e] -> ShowS
LHSCore' e -> String
(Int -> LHSCore' e -> ShowS)
-> (LHSCore' e -> String)
-> ([LHSCore' e] -> ShowS)
-> Show (LHSCore' e)
forall e. Show e => Int -> LHSCore' e -> ShowS
forall e. Show e => [LHSCore' e] -> ShowS
forall e. Show e => LHSCore' e -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall e. Show e => Int -> LHSCore' e -> ShowS
showsPrec :: Int -> LHSCore' e -> ShowS
$cshow :: forall e. Show e => LHSCore' e -> String
show :: LHSCore' e -> String
$cshowList :: forall e. Show e => [LHSCore' e] -> ShowS
showList :: [LHSCore' e] -> ShowS
Show, (forall a b. (a -> b) -> LHSCore' a -> LHSCore' b)
-> (forall a b. a -> LHSCore' b -> LHSCore' a) -> Functor LHSCore'
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
$cfmap :: forall a b. (a -> b) -> LHSCore' a -> LHSCore' b
fmap :: forall a b. (a -> b) -> LHSCore' a -> LHSCore' b
$c<$ :: forall a b. a -> LHSCore' b -> LHSCore' a
<$ :: forall a b. a -> LHSCore' b -> LHSCore' a
Functor, (forall m. Monoid m => LHSCore' m -> m)
-> (forall m a. Monoid m => (a -> m) -> LHSCore' a -> m)
-> (forall m a. Monoid m => (a -> m) -> LHSCore' a -> m)
-> (forall a b. (a -> b -> b) -> b -> LHSCore' a -> b)
-> (forall a b. (a -> b -> b) -> b -> LHSCore' a -> b)
-> (forall b a. (b -> a -> b) -> b -> LHSCore' a -> b)
-> (forall b a. (b -> a -> b) -> b -> LHSCore' a -> b)
-> (forall a. (a -> a -> a) -> LHSCore' a -> a)
-> (forall a. (a -> a -> a) -> LHSCore' a -> a)
-> (forall a. LHSCore' a -> [a])
-> (forall a. LHSCore' a -> Bool)
-> (forall a. LHSCore' a -> Int)
-> (forall a. Eq a => a -> LHSCore' a -> Bool)
-> (forall a. Ord a => LHSCore' a -> a)
-> (forall a. Ord a => LHSCore' a -> a)
-> (forall a. Num a => LHSCore' a -> a)
-> (forall a. Num a => LHSCore' a -> a)
-> Foldable LHSCore'
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
$cfold :: forall m. Monoid m => LHSCore' m -> m
fold :: forall m. Monoid m => LHSCore' m -> 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
foldMap' :: forall m a. Monoid m => (a -> m) -> LHSCore' a -> m
$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
foldr' :: forall a b. (a -> b -> 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
foldl' :: forall b a. (b -> a -> b) -> b -> LHSCore' a -> b
$cfoldr1 :: forall a. (a -> a -> a) -> LHSCore' a -> a
foldr1 :: forall a. (a -> a -> a) -> LHSCore' a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> LHSCore' a -> a
foldl1 :: forall a. (a -> a -> a) -> LHSCore' a -> a
$ctoList :: forall a. LHSCore' a -> [a]
toList :: forall a. LHSCore' a -> [a]
$cnull :: forall a. LHSCore' a -> Bool
null :: forall a. LHSCore' a -> Bool
$clength :: forall a. LHSCore' a -> Int
length :: forall a. LHSCore' a -> Int
$celem :: forall a. Eq a => a -> LHSCore' a -> Bool
elem :: forall a. Eq a => a -> LHSCore' a -> Bool
$cmaximum :: forall a. Ord a => LHSCore' a -> a
maximum :: forall a. Ord a => LHSCore' a -> a
$cminimum :: forall a. Ord a => LHSCore' a -> a
minimum :: forall a. Ord a => LHSCore' a -> a
$csum :: forall a. Num a => LHSCore' a -> a
sum :: forall a. Num a => LHSCore' a -> a
$cproduct :: forall a. Num a => LHSCore' a -> a
product :: forall a. Num a => LHSCore' a -> a
Foldable, Functor LHSCore'
Foldable LHSCore'
(Functor LHSCore', Foldable LHSCore') =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> LHSCore' a -> f (LHSCore' b))
-> (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 (m :: * -> *) a.
    Monad m =>
    LHSCore' (m a) -> m (LHSCore' a))
-> Traversable 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)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> LHSCore' a -> f (LHSCore' b)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> LHSCore' a -> f (LHSCore' b)
$csequenceA :: forall (f :: * -> *) a.
Applicative f =>
LHSCore' (f a) -> f (LHSCore' a)
sequenceA :: forall (f :: * -> *) a.
Applicative f =>
LHSCore' (f a) -> f (LHSCore' a)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> LHSCore' a -> m (LHSCore' b)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> LHSCore' a -> m (LHSCore' b)
$csequence :: forall (m :: * -> *) a. Monad m => LHSCore' (m a) -> m (LHSCore' a)
sequence :: forall (m :: * -> *) a. Monad m => LHSCore' (m a) -> m (LHSCore' a)
Traversable, LHSCore' e -> LHSCore' e -> Bool
(LHSCore' e -> LHSCore' e -> Bool)
-> (LHSCore' e -> LHSCore' e -> Bool) -> Eq (LHSCore' e)
forall e. Eq e => LHSCore' e -> LHSCore' e -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$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
/= :: LHSCore' e -> LHSCore' e -> Bool
Eq, (forall x. LHSCore' e -> Rep (LHSCore' e) x)
-> (forall x. Rep (LHSCore' e) x -> LHSCore' e)
-> Generic (LHSCore' e)
forall x. Rep (LHSCore' e) x -> LHSCore' e
forall x. LHSCore' e -> Rep (LHSCore' e) x
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
$cfrom :: forall e x. LHSCore' e -> Rep (LHSCore' e) x
from :: forall x. LHSCore' e -> Rep (LHSCore' e) x
$cto :: forall e x. Rep (LHSCore' e) x -> LHSCore' e
to :: forall x. Rep (LHSCore' e) x -> LHSCore' e
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
[Pattern' e] -> ShowS
Pattern' e -> String
(Int -> Pattern' e -> ShowS)
-> (Pattern' e -> String)
-> ([Pattern' e] -> ShowS)
-> Show (Pattern' e)
forall e. Show e => Int -> Pattern' e -> ShowS
forall e. Show e => [Pattern' e] -> ShowS
forall e. Show e => Pattern' e -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall e. Show e => Int -> Pattern' e -> ShowS
showsPrec :: Int -> Pattern' e -> ShowS
$cshow :: forall e. Show e => Pattern' e -> String
show :: Pattern' e -> String
$cshowList :: forall e. Show e => [Pattern' e] -> ShowS
showList :: [Pattern' e] -> ShowS
Show, (forall a b. (a -> b) -> Pattern' a -> Pattern' b)
-> (forall a b. a -> Pattern' b -> Pattern' a) -> Functor Pattern'
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
$cfmap :: forall a b. (a -> b) -> Pattern' a -> Pattern' b
fmap :: forall a b. (a -> b) -> Pattern' a -> Pattern' b
$c<$ :: forall a b. a -> Pattern' b -> Pattern' a
<$ :: forall a b. a -> Pattern' b -> Pattern' a
Functor, (forall m. Monoid m => Pattern' m -> m)
-> (forall m a. Monoid m => (a -> m) -> Pattern' a -> m)
-> (forall m a. Monoid m => (a -> m) -> Pattern' a -> m)
-> (forall a b. (a -> b -> b) -> b -> Pattern' a -> b)
-> (forall a b. (a -> b -> b) -> b -> Pattern' a -> b)
-> (forall b a. (b -> a -> b) -> b -> Pattern' a -> b)
-> (forall b a. (b -> a -> b) -> b -> Pattern' a -> b)
-> (forall a. (a -> a -> a) -> Pattern' a -> a)
-> (forall a. (a -> a -> a) -> Pattern' a -> a)
-> (forall a. Pattern' a -> [a])
-> (forall a. Pattern' a -> Bool)
-> (forall a. Pattern' a -> Int)
-> (forall a. Eq a => a -> Pattern' a -> Bool)
-> (forall a. Ord a => Pattern' a -> a)
-> (forall a. Ord a => Pattern' a -> a)
-> (forall a. Num a => Pattern' a -> a)
-> (forall a. Num a => Pattern' a -> a)
-> Foldable Pattern'
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
$cfold :: forall m. Monoid m => Pattern' m -> m
fold :: forall m. Monoid m => Pattern' m -> 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
foldMap' :: forall m a. Monoid m => (a -> m) -> Pattern' a -> m
$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
foldr' :: forall a b. (a -> b -> 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
foldl' :: forall b a. (b -> a -> b) -> b -> Pattern' a -> b
$cfoldr1 :: forall a. (a -> a -> a) -> Pattern' a -> a
foldr1 :: forall a. (a -> a -> a) -> Pattern' a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> Pattern' a -> a
foldl1 :: forall a. (a -> a -> a) -> Pattern' a -> a
$ctoList :: forall a. Pattern' a -> [a]
toList :: forall a. Pattern' a -> [a]
$cnull :: forall a. Pattern' a -> Bool
null :: forall a. Pattern' a -> Bool
$clength :: forall a. Pattern' a -> Int
length :: forall a. Pattern' a -> Int
$celem :: forall a. Eq a => a -> Pattern' a -> Bool
elem :: forall a. Eq a => a -> Pattern' a -> Bool
$cmaximum :: forall a. Ord a => Pattern' a -> a
maximum :: forall a. Ord a => Pattern' a -> a
$cminimum :: forall a. Ord a => Pattern' a -> a
minimum :: forall a. Ord a => Pattern' a -> a
$csum :: forall a. Num a => Pattern' a -> a
sum :: forall a. Num a => Pattern' a -> a
$cproduct :: forall a. Num a => Pattern' a -> a
product :: forall a. Num a => Pattern' a -> a
Foldable, Functor Pattern'
Foldable Pattern'
(Functor Pattern', Foldable Pattern') =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> Pattern' a -> f (Pattern' b))
-> (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 (m :: * -> *) a.
    Monad m =>
    Pattern' (m a) -> m (Pattern' a))
-> Traversable 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)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Pattern' a -> f (Pattern' b)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Pattern' a -> f (Pattern' b)
$csequenceA :: forall (f :: * -> *) a.
Applicative f =>
Pattern' (f a) -> f (Pattern' a)
sequenceA :: forall (f :: * -> *) a.
Applicative f =>
Pattern' (f a) -> f (Pattern' a)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Pattern' a -> m (Pattern' b)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Pattern' a -> m (Pattern' b)
$csequence :: forall (m :: * -> *) a. Monad m => Pattern' (m a) -> m (Pattern' a)
sequence :: forall (m :: * -> *) a. Monad m => Pattern' (m a) -> m (Pattern' a)
Traversable, Pattern' e -> Pattern' e -> Bool
(Pattern' e -> Pattern' e -> Bool)
-> (Pattern' e -> Pattern' e -> Bool) -> Eq (Pattern' e)
forall e. Eq e => Pattern' e -> Pattern' e -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$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
/= :: Pattern' e -> Pattern' e -> Bool
Eq, (forall x. Pattern' e -> Rep (Pattern' e) x)
-> (forall x. Rep (Pattern' e) x -> Pattern' e)
-> Generic (Pattern' e)
forall x. Rep (Pattern' e) x -> Pattern' e
forall x. Pattern' e -> Rep (Pattern' e) x
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
$cfrom :: forall e x. Pattern' e -> Rep (Pattern' e) x
from :: forall x. Pattern' e -> Rep (Pattern' e) x
$cto :: forall e x. Rep (Pattern' e) x -> Pattern' e
to :: forall x. Rep (Pattern' e) x -> Pattern' e
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) = (ProjOrigin, AmbiguousQName) -> Maybe (ProjOrigin, AmbiguousQName)
forall a. a -> Maybe a
Just (ProjOrigin
o, AmbiguousQName
d)
  isProjP Pattern' e
_ = Maybe (ProjOrigin, AmbiguousQName)
forall a. Maybe a
Nothing

instance IsProjP Expr where
  isProjP :: Expr -> Maybe (ProjOrigin, AmbiguousQName)
isProjP (Proj ProjOrigin
o AmbiguousQName
ds)      = (ProjOrigin, AmbiguousQName) -> Maybe (ProjOrigin, AmbiguousQName)
forall a. a -> Maybe a
Just (ProjOrigin
o, AmbiguousQName
ds)
  isProjP (ScopedExpr ScopeInfo
_ Expr
e) = Expr -> Maybe (ProjOrigin, AmbiguousQName)
forall a. IsProjP a => a -> Maybe (ProjOrigin, AmbiguousQName)
isProjP Expr
e
  isProjP Expr
_ = Maybe (ProjOrigin, AmbiguousQName)
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 Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
== Expr
a2

  Var Name
a1                     == Var Name
a2                     = Name
a1 Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
a2
  Def' QName
a1 Suffix
s1                 == Def' QName
a2 Suffix
s2                 = (QName
a1, Suffix
s1) (QName, Suffix) -> (QName, Suffix) -> Bool
forall a. Eq a => a -> a -> Bool
== (QName
a2, Suffix
s2)
  Proj ProjOrigin
_ AmbiguousQName
a1                  == Proj ProjOrigin
_ AmbiguousQName
a2                  = AmbiguousQName
a1 AmbiguousQName -> AmbiguousQName -> Bool
forall a. Eq a => a -> a -> Bool
== AmbiguousQName
a2
  Con AmbiguousQName
a1                     == Con AmbiguousQName
a2                     = AmbiguousQName
a1 AmbiguousQName -> AmbiguousQName -> Bool
forall a. Eq a => a -> a -> Bool
== AmbiguousQName
a2
  PatternSyn AmbiguousQName
a1              == PatternSyn AmbiguousQName
a2              = AmbiguousQName
a1 AmbiguousQName -> AmbiguousQName -> Bool
forall a. Eq a => a -> a -> Bool
== AmbiguousQName
a2
  Macro QName
a1                   == Macro QName
a2                   = QName
a1 QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
a2
  Lit ExprInfo
r1 Literal
a1                  == Lit ExprInfo
r2 Literal
a2                  = (ExprInfo
r1, Literal
a1) (ExprInfo, Literal) -> (ExprInfo, Literal) -> Bool
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) (MetaInfo, InteractionId) -> (MetaInfo, InteractionId) -> Bool
forall a. Eq a => a -> a -> Bool
== (MetaInfo
a2, InteractionId
b2)
  Underscore MetaInfo
a1              == Underscore MetaInfo
a2              = MetaInfo
a1 MetaInfo -> MetaInfo -> Bool
forall a. Eq a => a -> a -> Bool
== MetaInfo
a2
  Dot ExprInfo
r1 Expr
e1                  == Dot ExprInfo
r2 Expr
e2                  = (ExprInfo
r1, Expr
e1) (ExprInfo, Expr) -> (ExprInfo, Expr) -> Bool
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) (AppInfo, Expr, NamedArg Expr)
-> (AppInfo, Expr, NamedArg Expr) -> Bool
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) (ExprInfo, Expr, [Expr]) -> (ExprInfo, Expr, [Expr]) -> Bool
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) (ExprInfo, LamBinding, Expr)
-> (ExprInfo, LamBinding, Expr) -> Bool
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) (ExprInfo, Hiding) -> (ExprInfo, Hiding) -> Bool
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) (ExprInfo, DefInfo, Erased, QName, List1 Clause)
-> (ExprInfo, DefInfo, Erased, QName, List1 Clause) -> Bool
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) (ExprInfo, Telescope1, Expr)
-> (ExprInfo, Telescope1, Expr) -> Bool
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) (Set QName, Expr) -> (Set QName, Expr) -> Bool
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) (ExprInfo, Arg Expr, Expr) -> (ExprInfo, Arg Expr, Expr) -> Bool
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) (ExprInfo, List1 LetBinding, Expr)
-> (ExprInfo, List1 LetBinding, Expr) -> Bool
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) (ExprInfo, RecordAssigns) -> (ExprInfo, RecordAssigns) -> Bool
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) (ExprInfo, Expr, Assigns) -> (ExprInfo, Expr, Assigns) -> Bool
forall a. Eq a => a -> a -> Bool
== (ExprInfo
a2, Expr
b2, Assigns
c2)
  Quote ExprInfo
a1                   == Quote ExprInfo
a2                   = ExprInfo
a1 ExprInfo -> ExprInfo -> Bool
forall a. Eq a => a -> a -> Bool
== ExprInfo
a2
  QuoteTerm ExprInfo
a1               == QuoteTerm ExprInfo
a2               = ExprInfo
a1 ExprInfo -> ExprInfo -> Bool
forall a. Eq a => a -> a -> Bool
== ExprInfo
a2
  Unquote ExprInfo
a1                 == Unquote ExprInfo
a2                 = ExprInfo
a1 ExprInfo -> ExprInfo -> Bool
forall a. Eq a => a -> a -> Bool
== ExprInfo
a2
  DontCare Expr
a1                == DontCare Expr
a2                = Expr
a1 Expr -> Expr -> Bool
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 [Declaration] -> [Declaration] -> Bool
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) (KindOfName, DefInfo, ArgInfo, Maybe [Occurrence], QName, Expr)
-> (KindOfName, DefInfo, ArgInfo, Maybe [Occurrence], QName, Expr)
-> Bool
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) (Set QName, DefInfo, ArgInfo, QName, Expr)
-> (Set QName, DefInfo, ArgInfo, QName, Expr) -> Bool
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) (DefInfo, QName, Arg Expr) -> (DefInfo, QName, Arg Expr) -> Bool
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) (DefInfo, QName, Arg Expr) -> (DefInfo, QName, Arg Expr) -> Bool
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) (MutualInfo, [Declaration]) -> (MutualInfo, [Declaration]) -> Bool
forall a. Eq a => a -> a -> Bool
== (MutualInfo
a2, [Declaration]
b2)
  Section Range
a1 Erased
b1 ModuleName
c1 GeneralizeTelescope
d1 [Declaration]
e1         == Section Range
a2 Erased
b2 ModuleName
c2 GeneralizeTelescope
d2 [Declaration]
e2         = (Range
a1, Erased
b1, ModuleName
c1, GeneralizeTelescope
d1, [Declaration]
e1) (Range, Erased, ModuleName, GeneralizeTelescope, [Declaration])
-> (Range, Erased, ModuleName, GeneralizeTelescope, [Declaration])
-> Bool
forall a. Eq a => a -> a -> Bool
== (Range
a2, Erased
b2, ModuleName
c2, GeneralizeTelescope
d2, [Declaration]
e2)
  Apply ModuleInfo
a1 Erased
b1 ModuleName
c1 ModuleApplication
d1 ScopeCopyInfo
e1 ImportDirective
f1        == Apply ModuleInfo
a2 Erased
b2 ModuleName
c2 ModuleApplication
d2 ScopeCopyInfo
e2 ImportDirective
f2        = (ModuleInfo
a1, Erased
b1, ModuleName
c1, ModuleApplication
d1, ScopeCopyInfo
e1, ImportDirective
f1) (ModuleInfo, Erased, ModuleName, ModuleApplication, ScopeCopyInfo,
 ImportDirective)
-> (ModuleInfo, Erased, ModuleName, ModuleApplication,
    ScopeCopyInfo, ImportDirective)
-> Bool
forall a. Eq a => a -> a -> Bool
== (ModuleInfo
a2, Erased
b2, ModuleName
c2, ModuleApplication
d2, ScopeCopyInfo
e2, ImportDirective
f2)
  Import ModuleInfo
a1 ModuleName
b1 ImportDirective
c1                == Import ModuleInfo
a2 ModuleName
b2 ImportDirective
c2                = (ModuleInfo
a1, ModuleName
b1, ImportDirective
c1) (ModuleInfo, ModuleName, ImportDirective)
-> (ModuleInfo, ModuleName, ImportDirective) -> Bool
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) (Range, Pragma) -> (Range, Pragma) -> Bool
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) (ModuleInfo, ModuleName, ImportDirective)
-> (ModuleInfo, ModuleName, ImportDirective) -> Bool
forall a. Eq a => a -> a -> Bool
== (ModuleInfo
a2, ModuleName
b2, ImportDirective
c2)
  FunDef DefInfo
a1 QName
b1 [Clause]
c1                == FunDef DefInfo
a2 QName
b2 [Clause]
c2                = (DefInfo
a1, QName
b1, [Clause]
c1) (DefInfo, QName, [Clause]) -> (DefInfo, QName, [Clause]) -> Bool
forall a. Eq a => a -> a -> Bool
== (DefInfo
a2, QName
b2, [Clause]
c2)
  DataSig DefInfo
a1 Erased
b1 QName
c1 GeneralizeTelescope
d1 Expr
e1         == DataSig DefInfo
a2 Erased
b2 QName
c2 GeneralizeTelescope
d2 Expr
e2         = (DefInfo
a1, Erased
b1, QName
c1, GeneralizeTelescope
d1, Expr
e1) (DefInfo, Erased, QName, GeneralizeTelescope, Expr)
-> (DefInfo, Erased, QName, GeneralizeTelescope, Expr) -> Bool
forall a. Eq a => a -> a -> Bool
== (DefInfo
a2, Erased
b2, QName
c2, GeneralizeTelescope
d2, Expr
e2)
  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) (DefInfo, QName, UniverseCheck, DataDefParams, [Declaration])
-> (DefInfo, QName, UniverseCheck, DataDefParams, [Declaration])
-> Bool
forall a. Eq a => a -> a -> Bool
== (DefInfo
a2, QName
b2, UniverseCheck
c2, DataDefParams
d2, [Declaration]
e2)
  RecSig DefInfo
a1 Erased
b1 QName
c1 GeneralizeTelescope
d1 Expr
e1          == RecSig DefInfo
a2 Erased
b2 QName
c2 GeneralizeTelescope
d2 Expr
e2          = (DefInfo
a1, Erased
b1, QName
c1, GeneralizeTelescope
d1, Expr
e1) (DefInfo, Erased, QName, GeneralizeTelescope, Expr)
-> (DefInfo, Erased, QName, GeneralizeTelescope, Expr) -> Bool
forall a. Eq a => a -> a -> Bool
== (DefInfo
a2, Erased
b2, QName
c2, GeneralizeTelescope
d2, Expr
e2)
  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) (DefInfo, QName, UniverseCheck, RecordDirectives, DataDefParams,
 Expr, [Declaration])
-> (DefInfo, QName, UniverseCheck, RecordDirectives, DataDefParams,
    Expr, [Declaration])
-> Bool
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) (QName, [Arg BindName], Pattern' Void)
-> (QName, [Arg BindName], Pattern' Void) -> Bool
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) (MutualInfo, [DefInfo], [QName], Expr)
-> (MutualInfo, [DefInfo], [QName], Expr) -> Bool
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) ([DefInfo], [QName], Expr) -> ([DefInfo], [QName], Expr) -> Bool
forall a. Eq a => a -> a -> Bool
== ([DefInfo]
a2, [QName]
b2, Expr
c2)
  UnfoldingDecl Range
a1 [QName]
b1            == UnfoldingDecl Range
a2 [QName]
b2            = (Range
a1,[QName]
b1) (Range, [QName]) -> (Range, [QName]) -> Bool
forall a. Eq a => a -> a -> Bool
== (Range
a2,[QName]
b2)

  Declaration
_                              == Declaration
_                              = Bool
False

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

instance LensHiding LamBinding where
  getHiding :: LamBinding -> Hiding
getHiding   (DomainFree TacticAttr
_ NamedArg Binder
x) = NamedArg Binder -> Hiding
forall a. LensHiding a => a -> Hiding
getHiding NamedArg Binder
x
  getHiding   (DomainFull TypedBinding
tb)  = TypedBinding -> Hiding
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 (NamedArg Binder -> LamBinding) -> NamedArg Binder -> LamBinding
forall a b. (a -> b) -> a -> b
$ (Hiding -> Hiding) -> NamedArg Binder -> NamedArg Binder
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 (TypedBinding -> LamBinding) -> TypedBinding -> LamBinding
forall a b. (a -> b) -> a -> b
$ (Hiding -> Hiding) -> TypedBinding -> TypedBinding
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
_) = NamedArg Binder -> Hiding
forall a. LensHiding a => a -> Hiding
getHiding NamedArg Binder
x   -- Slightly dubious
  getHiding TLet{}                = Hiding
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 (((NamedArg Binder -> NamedArg Binder)
-> List1 (NamedArg Binder) -> List1 (NamedArg Binder)
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((NamedArg Binder -> NamedArg Binder)
 -> List1 (NamedArg Binder) -> List1 (NamedArg Binder))
-> ((Hiding -> Hiding) -> NamedArg Binder -> NamedArg Binder)
-> (Hiding -> Hiding)
-> List1 (NamedArg Binder)
-> List1 (NamedArg Binder)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Hiding -> Hiding) -> NamedArg Binder -> NamedArg Binder
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) = Maybe Pattern -> a -> Range
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) = NamedArg Binder -> Range
forall a. HasRange a => a -> Range
getRange NamedArg Binder
x
    getRange (DomainFull TypedBinding
b)   = TypedBinding -> Range
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)                 = Name -> Range
forall a. HasRange a => a -> Range
getRange Name
x
    getRange (Def' QName
x Suffix
_)              = QName -> Range
forall a. HasRange a => a -> Range
getRange QName
x
    getRange (Proj ProjOrigin
_ AmbiguousQName
x)              = AmbiguousQName -> Range
forall a. HasRange a => a -> Range
getRange AmbiguousQName
x
    getRange (Con AmbiguousQName
x)                 = AmbiguousQName -> Range
forall a. HasRange a => a -> Range
getRange AmbiguousQName
x
    getRange (Lit ExprInfo
i Literal
_)               = ExprInfo -> Range
forall a. HasRange a => a -> Range
getRange ExprInfo
i
    getRange (QuestionMark MetaInfo
i InteractionId
_)      = MetaInfo -> Range
forall a. HasRange a => a -> Range
getRange MetaInfo
i
    getRange (Underscore  MetaInfo
i)         = MetaInfo -> Range
forall a. HasRange a => a -> Range
getRange MetaInfo
i
    getRange (Dot ExprInfo
i Expr
_)               = ExprInfo -> Range
forall a. HasRange a => a -> Range
getRange ExprInfo
i
    getRange (App AppInfo
i Expr
_ NamedArg Expr
_)             = AppInfo -> Range
forall a. HasRange a => a -> Range
getRange AppInfo
i
    getRange (WithApp ExprInfo
i Expr
_ [Expr]
_)         = ExprInfo -> Range
forall a. HasRange a => a -> Range
getRange ExprInfo
i
    getRange (Lam ExprInfo
i LamBinding
_ Expr
_)             = ExprInfo -> Range
forall a. HasRange a => a -> Range
getRange ExprInfo
i
    getRange (AbsurdLam ExprInfo
i Hiding
_)         = ExprInfo -> Range
forall a. HasRange a => a -> Range
getRange ExprInfo
i
    getRange (ExtendedLam ExprInfo
i DefInfo
_ Erased
_ QName
_ List1 Clause
_) = ExprInfo -> Range
forall a. HasRange a => a -> Range
getRange ExprInfo
i
    getRange (Pi ExprInfo
i Telescope1
_ Expr
_)              = ExprInfo -> Range
forall a. HasRange a => a -> Range
getRange ExprInfo
i
    getRange (Generalized Set QName
_ Expr
x)       = Expr -> Range
forall a. HasRange a => a -> Range
getRange Expr
x
    getRange (Fun ExprInfo
i Arg Expr
_ Expr
_)             = ExprInfo -> Range
forall a. HasRange a => a -> Range
getRange ExprInfo
i
    getRange (Let ExprInfo
i List1 LetBinding
_ Expr
_)             = ExprInfo -> Range
forall a. HasRange a => a -> Range
getRange ExprInfo
i
    getRange (Rec ExprInfo
i RecordAssigns
_)               = ExprInfo -> Range
forall a. HasRange a => a -> Range
getRange ExprInfo
i
    getRange (RecUpdate ExprInfo
i Expr
_ Assigns
_)       = ExprInfo -> Range
forall a. HasRange a => a -> Range
getRange ExprInfo
i
    getRange (ScopedExpr ScopeInfo
_ Expr
e)        = Expr -> Range
forall a. HasRange a => a -> Range
getRange Expr
e
    getRange (Quote ExprInfo
i)               = ExprInfo -> Range
forall a. HasRange a => a -> Range
getRange ExprInfo
i
    getRange (QuoteTerm ExprInfo
i)           = ExprInfo -> Range
forall a. HasRange a => a -> Range
getRange ExprInfo
i
    getRange (Unquote ExprInfo
i)             = ExprInfo -> Range
forall a. HasRange a => a -> Range
getRange ExprInfo
i
    getRange (DontCare{})            = Range
forall a. Range' a
noRange
    getRange (PatternSyn AmbiguousQName
x)          = AmbiguousQName -> Range
forall a. HasRange a => a -> Range
getRange AmbiguousQName
x
    getRange (Macro QName
x)               = QName -> Range
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
_  )  = DefInfo -> Range
forall a. HasRange a => a -> Range
getRange DefInfo
i
    getRange (Generalize Set QName
_ DefInfo
i ArgInfo
_ QName
_ Expr
_)    = DefInfo -> Range
forall a. HasRange a => a -> Range
getRange DefInfo
i
    getRange (Field      DefInfo
i QName
_ Arg Expr
_      )  = DefInfo -> Range
forall a. HasRange a => a -> Range
getRange DefInfo
i
    getRange (Mutual     MutualInfo
i [Declaration]
_        )  = MutualInfo -> Range
forall a. HasRange a => a -> Range
getRange MutualInfo
i
    getRange (Section    Range
i Erased
_ ModuleName
_ GeneralizeTelescope
_ [Declaration]
_  )  = Range -> Range
forall a. HasRange a => a -> Range
getRange Range
i
    getRange (Apply      ModuleInfo
i Erased
_ ModuleName
_ ModuleApplication
_ ScopeCopyInfo
_ ImportDirective
_)  = ModuleInfo -> Range
forall a. HasRange a => a -> Range
getRange ModuleInfo
i
    getRange (Import     ModuleInfo
i ModuleName
_ ImportDirective
_      )  = ModuleInfo -> Range
forall a. HasRange a => a -> Range
getRange ModuleInfo
i
    getRange (Primitive  DefInfo
i QName
_ Arg Expr
_      )  = DefInfo -> Range
forall a. HasRange a => a -> Range
getRange DefInfo
i
    getRange (Pragma     Range
i Pragma
_        )  = Range -> Range
forall a. HasRange a => a -> Range
getRange Range
i
    getRange (Open       ModuleInfo
i ModuleName
_ ImportDirective
_      )  = ModuleInfo -> Range
forall a. HasRange a => a -> Range
getRange ModuleInfo
i
    getRange (ScopedDecl ScopeInfo
_ [Declaration]
d        )  = [Declaration] -> Range
forall a. HasRange a => a -> Range
getRange [Declaration]
d
    getRange (FunDef     DefInfo
i QName
_ [Clause]
_      )  = DefInfo -> Range
forall a. HasRange a => a -> Range
getRange DefInfo
i
    getRange (DataSig    DefInfo
i Erased
_ QName
_ GeneralizeTelescope
_ Expr
_  )  = DefInfo -> Range
forall a. HasRange a => a -> Range
getRange DefInfo
i
    getRange (DataDef    DefInfo
i QName
_ UniverseCheck
_ DataDefParams
_ [Declaration]
_  )  = DefInfo -> Range
forall a. HasRange a => a -> Range
getRange DefInfo
i
    getRange (RecSig     DefInfo
i Erased
_ QName
_ GeneralizeTelescope
_ Expr
_  )  = DefInfo -> Range
forall a. HasRange a => a -> Range
getRange DefInfo
i
    getRange (RecDef DefInfo
i QName
_ UniverseCheck
_ RecordDirectives
_ DataDefParams
_ Expr
_ [Declaration]
_)    = DefInfo -> Range
forall a. HasRange a => a -> Range
getRange DefInfo
i
    getRange (PatternSynDef QName
x [Arg BindName]
_ Pattern' Void
_   )  = QName -> Range
forall a. HasRange a => a -> Range
getRange QName
x
    getRange (UnquoteDecl MutualInfo
_ [DefInfo]
i [QName]
_ Expr
_)     = [DefInfo] -> Range
forall a. HasRange a => a -> Range
getRange [DefInfo]
i
    getRange (UnquoteDef [DefInfo]
i [QName]
_ Expr
_)        = [DefInfo] -> Range
forall a. HasRange a => a -> Range
getRange [DefInfo]
i
    getRange (UnquoteData [DefInfo]
i QName
_ UniverseCheck
_ [DefInfo]
j [QName]
_ Expr
_) = ([DefInfo], [DefInfo]) -> Range
forall a. HasRange a => a -> Range
getRange ([DefInfo]
i, [DefInfo]
j)
    getRange (UnfoldingDecl Range
r [QName]
_)       = Range
r

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

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

instance HasRange LHS where
    getRange :: LHS -> Range
getRange (LHS LHSInfo
i LHSCore
_)   = LHSInfo -> Range
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)         = QName -> [NamedArg (Pattern' e)] -> Range
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 AmbiguousQName -> NamedArg (LHSCore' e) -> Range
forall u t. (HasRange u, HasRange t) => u -> t -> Range
`fuseRange` NamedArg (LHSCore' e)
lhscore Range -> [NamedArg (Pattern' e)] -> Range
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 LHSCore' e -> [Arg (Pattern' e)] -> Range
forall u t. (HasRange u, HasRange t) => u -> t -> Range
`fuseRange` [Arg (Pattern' e)]
wps Range -> [NamedArg (Pattern' e)] -> Range
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) = (a, RHS, WhereDeclarations) -> Range
forall a. HasRange a => a -> Range
getRange (a
lhs, RHS
rhs, WhereDeclarations
ds)

instance HasRange RHS where
    getRange :: RHS -> Range
getRange RHS
AbsurdRHS                 = Range
forall a. Range' a
noRange
    getRange (RHS Expr
e Maybe Expr
_)                 = Expr -> Range
forall a. HasRange a => a -> Range
getRange Expr
e
    getRange (WithRHS QName
_ [WithExpr]
e List1 Clause
cs)          = [WithExpr] -> List1 Clause -> Range
forall u t. (HasRange u, HasRange t) => u -> t -> Range
fuseRange [WithExpr]
e List1 Clause
cs
    getRange (RewriteRHS [RewriteEqn]
xes [ProblemEq]
_ RHS
rhs WhereDeclarations
wh) = ([RewriteEqn], RHS, WhereDeclarations) -> Range
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) = Maybe Declaration -> Range
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
_     ) = LetInfo -> Range
forall a. HasRange a => a -> Range
getRange LetInfo
i
    getRange (LetPatBind  LetInfo
i Pattern
_ Expr
_      ) = LetInfo -> Range
forall a. HasRange a => a -> Range
getRange LetInfo
i
    getRange (LetApply ModuleInfo
i Erased
_ ModuleName
_ ModuleApplication
_ ScopeCopyInfo
_ ImportDirective
_   ) = ModuleInfo -> Range
forall a. HasRange a => a -> Range
getRange ModuleInfo
i
    getRange (LetOpen  ModuleInfo
i ModuleName
_ ImportDirective
_         ) = ModuleInfo -> Range
forall a. HasRange a => a -> Range
getRange ModuleInfo
i
    getRange (LetDeclaredVariable BindName
x)  = BindName -> Range
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)            = BindName -> Pattern' a
forall e. BindName -> Pattern' e
VarP (Range -> KillRangeT BindName
forall a. SetRange a => Range -> a -> a
setRange Range
r BindName
x)
    setRange Range
r (ConP ConPatInfo
i AmbiguousQName
ns NAPs a
as)       = ConPatInfo -> AmbiguousQName -> NAPs a -> Pattern' a
forall e. ConPatInfo -> AmbiguousQName -> NAPs e -> Pattern' e
ConP (Range -> ConPatInfo -> ConPatInfo
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)       = PatInfo -> ProjOrigin -> AmbiguousQName -> Pattern' a
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)       = PatInfo -> AmbiguousQName -> NAPs a -> Pattern' a
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
_)            = PatInfo -> Pattern' a
forall e. PatInfo -> Pattern' e
WildP (Range -> PatInfo
PatRange Range
r)
    setRange Range
r (AsP PatInfo
_ BindName
n Pattern' a
p)          = PatInfo -> BindName -> Pattern' a -> Pattern' a
forall e. PatInfo -> BindName -> Pattern' e -> Pattern' e
AsP (Range -> PatInfo
PatRange Range
r) (Range -> KillRangeT BindName
forall a. SetRange a => Range -> a -> a
setRange Range
r BindName
n) Pattern' a
p
    setRange Range
r (DotP PatInfo
_ a
e)           = PatInfo -> a -> Pattern' a
forall e. PatInfo -> e -> Pattern' e
DotP (Range -> PatInfo
PatRange Range
r) a
e
    setRange Range
r (AbsurdP PatInfo
_)          = PatInfo -> Pattern' a
forall e. PatInfo -> Pattern' e
AbsurdP (Range -> PatInfo
PatRange Range
r)
    setRange Range
r (LitP PatInfo
_ Literal
l)           = PatInfo -> Literal -> Pattern' a
forall e. PatInfo -> Literal -> Pattern' e
LitP (Range -> PatInfo
PatRange Range
r) Literal
l
    setRange Range
r (PatternSynP PatInfo
_ AmbiguousQName
n NAPs a
as) = PatInfo -> AmbiguousQName -> NAPs a -> Pattern' a
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)          = PatInfo -> [FieldAssignment' (Pattern' a)] -> Pattern' a
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)        = PatInfo -> [(a, a)] -> Pattern' a
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)          = PatInfo -> Pattern' a -> Pattern' a
forall e. PatInfo -> Pattern' e -> Pattern' e
WithP (Range -> PatInfo -> PatInfo
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)         = PatInfo -> a -> Pattern' a -> Pattern' a
forall e. PatInfo -> e -> Pattern' e -> Pattern' e
AnnP (Range -> PatInfo -> PatInfo
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) = (Maybe Pattern -> a -> Binder' a)
-> Maybe Pattern -> a -> Binder' a
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN Maybe Pattern -> a -> Binder' a
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) = (TacticAttr -> NamedArg Binder -> LamBinding)
-> TacticAttr -> NamedArg Binder -> LamBinding
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN TacticAttr -> NamedArg Binder -> LamBinding
DomainFree TacticAttr
t NamedArg Binder
x
  killRange (DomainFull TypedBinding
b)   = (TypedBinding -> LamBinding) -> TypedBinding -> LamBinding
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN 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 (KillRangeT Telescope
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 (KillRangeT [LamBinding]
forall a. KillRange a => KillRangeT a
killRange [LamBinding]
tel)

instance KillRange TypedBindingInfo where
  killRange :: KillRangeT TypedBindingInfo
killRange (TypedBindingInfo TacticAttr
a Bool
b) = (TacticAttr -> Bool -> TypedBindingInfo)
-> TacticAttr -> Bool -> TypedBindingInfo
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN 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) = (Range
 -> TypedBindingInfo
 -> List1 (NamedArg Binder)
 -> Expr
 -> TypedBinding)
-> Range
-> TypedBindingInfo
-> List1 (NamedArg Binder)
-> Expr
-> TypedBinding
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN 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)     = (Range -> List1 LetBinding -> TypedBinding)
-> Range -> List1 LetBinding -> TypedBinding
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN Range -> List1 LetBinding -> TypedBinding
TLet Range
r List1 LetBinding
lbs

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

instance KillRange Suffix where
  killRange :: KillRangeT Suffix
killRange = KillRangeT Suffix
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     ) = (DefInfo -> ArgInfo -> QName -> Expr -> Declaration)
-> DefInfo -> ArgInfo -> QName -> Expr -> Declaration
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN (\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     ) = (DefInfo -> ArgInfo -> QName -> Expr -> Declaration)
-> DefInfo -> ArgInfo -> QName -> Expr -> Declaration
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN (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         ) = (DefInfo -> QName -> Arg Expr -> Declaration)
-> DefInfo -> QName -> Arg Expr -> Declaration
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN DefInfo -> QName -> Arg Expr -> Declaration
Field      DefInfo
i QName
a Arg Expr
b
  killRange (Mutual     MutualInfo
i [Declaration]
a           ) = (MutualInfo -> [Declaration] -> Declaration)
-> MutualInfo -> [Declaration] -> Declaration
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN MutualInfo -> [Declaration] -> Declaration
Mutual     MutualInfo
i [Declaration]
a
  killRange (Section    Range
i Erased
a ModuleName
b GeneralizeTelescope
c [Declaration]
d     ) = (Range
 -> Erased
 -> ModuleName
 -> GeneralizeTelescope
 -> [Declaration]
 -> Declaration)
-> Range
-> Erased
-> ModuleName
-> GeneralizeTelescope
-> [Declaration]
-> Declaration
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN Range
-> Erased
-> ModuleName
-> GeneralizeTelescope
-> [Declaration]
-> Declaration
Section    Range
i Erased
a ModuleName
b GeneralizeTelescope
c [Declaration]
d
  killRange (Apply      ModuleInfo
i Erased
a ModuleName
b ModuleApplication
c ScopeCopyInfo
d ImportDirective
e   ) = (ModuleInfo
 -> Erased
 -> ModuleName
 -> ModuleApplication
 -> ScopeCopyInfo
 -> ImportDirective
 -> Declaration)
-> ModuleInfo
-> Erased
-> ModuleName
-> ModuleApplication
-> ScopeCopyInfo
-> ImportDirective
-> Declaration
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN ModuleInfo
-> Erased
-> ModuleName
-> ModuleApplication
-> ScopeCopyInfo
-> ImportDirective
-> Declaration
Apply      ModuleInfo
i Erased
a ModuleName
b ModuleApplication
c ScopeCopyInfo
d ImportDirective
e
  killRange (Import     ModuleInfo
i ModuleName
a ImportDirective
b         ) = (ModuleInfo -> ModuleName -> ImportDirective -> Declaration)
-> ModuleInfo -> ModuleName -> ImportDirective -> Declaration
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN ModuleInfo -> ModuleName -> ImportDirective -> Declaration
Import     ModuleInfo
i ModuleName
a ImportDirective
b
  killRange (Primitive  DefInfo
i QName
a Arg Expr
b         ) = (DefInfo -> QName -> Arg Expr -> Declaration)
-> DefInfo -> QName -> Arg Expr -> Declaration
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN DefInfo -> QName -> Arg Expr -> Declaration
Primitive  DefInfo
i QName
a Arg Expr
b
  killRange (Pragma     Range
i Pragma
a           ) = Range -> Pragma -> Declaration
Pragma (Range -> Range
forall a. KillRange a => KillRangeT a
killRange Range
i) Pragma
a
  killRange (Open       ModuleInfo
i ModuleName
x ImportDirective
dir       ) = (ModuleInfo -> ModuleName -> ImportDirective -> Declaration)
-> ModuleInfo -> ModuleName -> ImportDirective -> Declaration
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN ModuleInfo -> ModuleName -> ImportDirective -> Declaration
Open       ModuleInfo
i ModuleName
x ImportDirective
dir
  killRange (ScopedDecl ScopeInfo
a [Declaration]
d           ) = ([Declaration] -> Declaration) -> [Declaration] -> Declaration
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN (ScopeInfo -> [Declaration] -> Declaration
ScopedDecl ScopeInfo
a) [Declaration]
d
  killRange (FunDef  DefInfo
i QName
a [Clause]
b            ) = (DefInfo -> QName -> [Clause] -> Declaration)
-> DefInfo -> QName -> [Clause] -> Declaration
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN DefInfo -> QName -> [Clause] -> Declaration
FunDef  DefInfo
i QName
a [Clause]
b
  killRange (DataSig DefInfo
i Erased
a QName
b GeneralizeTelescope
c Expr
d        ) = (DefInfo
 -> Erased -> QName -> GeneralizeTelescope -> Expr -> Declaration)
-> DefInfo
-> Erased
-> QName
-> GeneralizeTelescope
-> Expr
-> Declaration
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN DefInfo
-> Erased -> QName -> GeneralizeTelescope -> Expr -> Declaration
DataSig DefInfo
i Erased
a QName
b GeneralizeTelescope
c Expr
d
  killRange (DataDef DefInfo
i QName
a UniverseCheck
b DataDefParams
c [Declaration]
d        ) = (DefInfo
 -> QName
 -> UniverseCheck
 -> DataDefParams
 -> [Declaration]
 -> Declaration)
-> DefInfo
-> QName
-> UniverseCheck
-> DataDefParams
-> [Declaration]
-> Declaration
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN DefInfo
-> QName
-> UniverseCheck
-> DataDefParams
-> [Declaration]
-> Declaration
DataDef DefInfo
i QName
a UniverseCheck
b DataDefParams
c [Declaration]
d
  killRange (RecSig  DefInfo
i Erased
a QName
b GeneralizeTelescope
c Expr
d        ) = (DefInfo
 -> Erased -> QName -> GeneralizeTelescope -> Expr -> Declaration)
-> DefInfo
-> Erased
-> QName
-> GeneralizeTelescope
-> Expr
-> Declaration
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN DefInfo
-> Erased -> QName -> GeneralizeTelescope -> Expr -> Declaration
RecSig  DefInfo
i Erased
a QName
b GeneralizeTelescope
c Expr
d
  killRange (RecDef  DefInfo
i QName
a UniverseCheck
b RecordDirectives
c DataDefParams
d Expr
e [Declaration]
f    ) = (DefInfo
 -> QName
 -> UniverseCheck
 -> RecordDirectives
 -> DataDefParams
 -> Expr
 -> [Declaration]
 -> Declaration)
-> DefInfo
-> QName
-> UniverseCheck
-> RecordDirectives
-> DataDefParams
-> Expr
-> [Declaration]
-> Declaration
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN 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     ) = (QName -> [Arg BindName] -> Pattern' Void -> Declaration)
-> QName -> [Arg BindName] -> Pattern' Void -> Declaration
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN 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     ) = (MutualInfo -> [DefInfo] -> [QName] -> Expr -> Declaration)
-> MutualInfo -> [DefInfo] -> [QName] -> Expr -> Declaration
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN MutualInfo -> [DefInfo] -> [QName] -> Expr -> Declaration
UnquoteDecl MutualInfo
mi [DefInfo]
i [QName]
x Expr
e
  killRange (UnquoteDef [DefInfo]
i [QName]
x Expr
e         ) = ([DefInfo] -> [QName] -> Expr -> Declaration)
-> [DefInfo] -> [QName] -> Expr -> Declaration
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN [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) = ([DefInfo]
 -> QName
 -> UniverseCheck
 -> [DefInfo]
 -> [QName]
 -> Expr
 -> Declaration)
-> [DefInfo]
-> QName
-> UniverseCheck
-> [DefInfo]
-> [QName]
-> Expr
-> Declaration
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN [DefInfo]
-> QName
-> UniverseCheck
-> [DefInfo]
-> [QName]
-> Expr
-> Declaration
UnquoteData [DefInfo]
i QName
xs UniverseCheck
uc [DefInfo]
j [QName]
cs Expr
e
  killRange (UnfoldingDecl Range
r [QName]
xs)         = (Range -> [QName] -> Declaration)
-> Range -> [QName] -> Declaration
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN Range -> [QName] -> Declaration
UnfoldingDecl Range
r [QName]
xs

instance KillRange ModuleApplication where
  killRange :: KillRangeT ModuleApplication
killRange (SectionApp Telescope
a ModuleName
b [NamedArg Expr]
c  ) = (Telescope -> ModuleName -> [NamedArg Expr] -> ModuleApplication)
-> Telescope -> ModuleName -> [NamedArg Expr] -> ModuleApplication
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN Telescope -> ModuleName -> [NamedArg Expr] -> ModuleApplication
SectionApp Telescope
a ModuleName
b [NamedArg Expr]
c
  killRange (RecordModuleInstance ModuleName
a) = (ModuleName -> ModuleApplication)
-> ModuleName -> ModuleApplication
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN ModuleName -> ModuleApplication
RecordModuleInstance ModuleName
a

instance KillRange ScopeCopyInfo where
  killRange :: KillRangeT ScopeCopyInfo
killRange (ScopeCopyInfo Ren ModuleName
a Ren QName
b) = (Ren ModuleName -> Ren QName -> ScopeCopyInfo)
-> Ren ModuleName -> Ren QName -> ScopeCopyInfo
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN 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)           = (BindName -> Pattern' e) -> BindName -> Pattern' e
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN BindName -> Pattern' e
forall e. BindName -> Pattern' e
VarP BindName
x
  killRange (ConP ConPatInfo
i AmbiguousQName
a NAPs e
b)        = (ConPatInfo -> AmbiguousQName -> NAPs e -> Pattern' e)
-> ConPatInfo -> AmbiguousQName -> NAPs e -> Pattern' e
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN ConPatInfo -> AmbiguousQName -> NAPs e -> Pattern' e
forall e. ConPatInfo -> AmbiguousQName -> NAPs e -> Pattern' e
ConP ConPatInfo
i AmbiguousQName
a NAPs e
b
  killRange (ProjP PatInfo
i ProjOrigin
o AmbiguousQName
a)       = (PatInfo -> ProjOrigin -> AmbiguousQName -> Pattern' e)
-> PatInfo -> ProjOrigin -> AmbiguousQName -> Pattern' e
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN PatInfo -> ProjOrigin -> AmbiguousQName -> Pattern' e
forall e. PatInfo -> ProjOrigin -> AmbiguousQName -> Pattern' e
ProjP PatInfo
i ProjOrigin
o AmbiguousQName
a
  killRange (DefP PatInfo
i AmbiguousQName
a NAPs e
b)        = (PatInfo -> AmbiguousQName -> NAPs e -> Pattern' e)
-> PatInfo -> AmbiguousQName -> NAPs e -> Pattern' e
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN PatInfo -> AmbiguousQName -> NAPs e -> Pattern' e
forall e. PatInfo -> AmbiguousQName -> NAPs e -> Pattern' e
DefP PatInfo
i AmbiguousQName
a NAPs e
b
  killRange (WildP PatInfo
i)           = (PatInfo -> Pattern' e) -> PatInfo -> Pattern' e
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN PatInfo -> Pattern' e
forall e. PatInfo -> Pattern' e
WildP PatInfo
i
  killRange (AsP PatInfo
i BindName
a Pattern' e
b)         = (PatInfo -> BindName -> KillRangeT (Pattern' e))
-> PatInfo -> BindName -> KillRangeT (Pattern' e)
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN PatInfo -> BindName -> KillRangeT (Pattern' e)
forall e. PatInfo -> BindName -> Pattern' e -> Pattern' e
AsP PatInfo
i BindName
a Pattern' e
b
  killRange (DotP PatInfo
i e
a)          = (PatInfo -> e -> Pattern' e) -> PatInfo -> e -> Pattern' e
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN PatInfo -> e -> Pattern' e
forall e. PatInfo -> e -> Pattern' e
DotP PatInfo
i e
a
  killRange (AbsurdP PatInfo
i)         = (PatInfo -> Pattern' e) -> PatInfo -> Pattern' e
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN PatInfo -> Pattern' e
forall e. PatInfo -> Pattern' e
AbsurdP PatInfo
i
  killRange (LitP PatInfo
i Literal
l)          = (PatInfo -> Literal -> Pattern' e)
-> PatInfo -> Literal -> Pattern' e
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN PatInfo -> Literal -> Pattern' e
forall e. PatInfo -> Literal -> Pattern' e
LitP PatInfo
i Literal
l
  killRange (PatternSynP PatInfo
i AmbiguousQName
a NAPs e
p) = (PatInfo -> AmbiguousQName -> NAPs e -> Pattern' e)
-> PatInfo -> AmbiguousQName -> NAPs e -> Pattern' e
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN PatInfo -> AmbiguousQName -> NAPs e -> Pattern' e
forall e. PatInfo -> AmbiguousQName -> NAPs e -> Pattern' e
PatternSynP PatInfo
i AmbiguousQName
a NAPs e
p
  killRange (RecP PatInfo
i [FieldAssignment' (Pattern' e)]
as)         = (PatInfo -> [FieldAssignment' (Pattern' e)] -> Pattern' e)
-> PatInfo -> [FieldAssignment' (Pattern' e)] -> Pattern' e
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN PatInfo -> [FieldAssignment' (Pattern' e)] -> Pattern' e
forall e. PatInfo -> [FieldAssignment' (Pattern' e)] -> Pattern' e
RecP PatInfo
i [FieldAssignment' (Pattern' e)]
as
  killRange (EqualP PatInfo
i [(e, e)]
es)       = (PatInfo -> [(e, e)] -> Pattern' e)
-> PatInfo -> [(e, e)] -> Pattern' e
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN PatInfo -> [(e, e)] -> Pattern' e
forall e. PatInfo -> [(e, e)] -> Pattern' e
EqualP PatInfo
i [(e, e)]
es
  killRange (WithP PatInfo
i Pattern' e
p)         = (PatInfo -> KillRangeT (Pattern' e))
-> PatInfo -> KillRangeT (Pattern' e)
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN PatInfo -> KillRangeT (Pattern' e)
forall e. PatInfo -> Pattern' e -> Pattern' e
WithP PatInfo
i Pattern' e
p
  killRange (AnnP PatInfo
i e
a Pattern' e
p)        = (PatInfo -> e -> KillRangeT (Pattern' e))
-> PatInfo -> e -> KillRangeT (Pattern' e)
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN PatInfo -> e -> KillRangeT (Pattern' e)
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)  = (LHSInfo -> QName -> [NamedArg Pattern] -> SpineLHS)
-> LHSInfo -> QName -> [NamedArg Pattern] -> SpineLHS
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN 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)   = (LHSInfo -> LHSCore -> LHS) -> LHSInfo -> LHSCore -> LHS
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN 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)   = (QName -> [NamedArg (Pattern' e)] -> LHSCore' e)
-> QName -> [NamedArg (Pattern' e)] -> LHSCore' e
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN QName -> [NamedArg (Pattern' e)] -> LHSCore' e
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) = (AmbiguousQName
 -> NamedArg (LHSCore' e) -> [NamedArg (Pattern' e)] -> LHSCore' e)
-> AmbiguousQName
-> NamedArg (LHSCore' e)
-> [NamedArg (Pattern' e)]
-> LHSCore' e
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN AmbiguousQName
-> NamedArg (LHSCore' e) -> [NamedArg (Pattern' e)] -> LHSCore' e
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) = (LHSCore' e
 -> [Arg (Pattern' e)] -> [NamedArg (Pattern' e)] -> LHSCore' e)
-> LHSCore' e
-> [Arg (Pattern' e)]
-> [NamedArg (Pattern' e)]
-> LHSCore' e
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN LHSCore' e
-> [Arg (Pattern' e)] -> [NamedArg (Pattern' e)] -> LHSCore' e
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) = (a -> [ProblemEq] -> RHS -> WhereDeclarations -> Bool -> Clause' a)
-> a
-> [ProblemEq]
-> RHS
-> WhereDeclarations
-> Bool
-> Clause' a
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN a -> [ProblemEq] -> RHS -> WhereDeclarations -> Bool -> Clause' a
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) = (Pattern -> Term -> Dom Type -> ProblemEq)
-> Pattern -> Term -> Dom Type -> ProblemEq
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN 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)                = (Expr -> Maybe Expr -> RHS) -> Expr -> Maybe Expr -> RHS
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN Expr -> Maybe Expr -> RHS
RHS Expr
e Maybe Expr
c
  killRange (WithRHS QName
q [WithExpr]
e List1 Clause
cs)         = (QName -> [WithExpr] -> List1 Clause -> RHS)
-> QName -> [WithExpr] -> List1 Clause -> RHS
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN QName -> [WithExpr] -> List1 Clause -> RHS
WithRHS QName
q [WithExpr]
e List1 Clause
cs
  killRange (RewriteRHS [RewriteEqn]
xes [ProblemEq]
spats RHS
rhs WhereDeclarations
wh) = ([RewriteEqn] -> [ProblemEq] -> RHS -> WhereDeclarations -> RHS)
-> [RewriteEqn] -> [ProblemEq] -> RHS -> WhereDeclarations -> RHS
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN [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) = (Maybe ModuleName
 -> Bool -> Maybe Declaration -> WhereDeclarations)
-> Maybe ModuleName
-> Bool
-> Maybe Declaration
-> WhereDeclarations
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN 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) = (LetInfo -> ArgInfo -> BindName -> Expr -> Expr -> LetBinding)
-> LetInfo -> ArgInfo -> BindName -> Expr -> Expr -> LetBinding
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN 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       ) = (LetInfo -> Pattern -> Expr -> LetBinding)
-> LetInfo -> Pattern -> Expr -> LetBinding
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN LetInfo -> Pattern -> Expr -> LetBinding
LetPatBind LetInfo
i Pattern
a Expr
b
  killRange (LetApply   ModuleInfo
i Erased
a ModuleName
b ModuleApplication
c ScopeCopyInfo
d ImportDirective
e ) = (ModuleInfo
 -> Erased
 -> ModuleName
 -> ModuleApplication
 -> ScopeCopyInfo
 -> ImportDirective
 -> LetBinding)
-> ModuleInfo
-> Erased
-> ModuleName
-> ModuleApplication
-> ScopeCopyInfo
-> ImportDirective
-> LetBinding
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN ModuleInfo
-> Erased
-> ModuleName
-> ModuleApplication
-> ScopeCopyInfo
-> ImportDirective
-> LetBinding
LetApply ModuleInfo
i Erased
a ModuleName
b ModuleApplication
c ScopeCopyInfo
d ImportDirective
e
  killRange (LetOpen    ModuleInfo
i ModuleName
x ImportDirective
dir     ) = (ModuleInfo -> ModuleName -> ImportDirective -> LetBinding)
-> ModuleInfo -> ModuleName -> ImportDirective -> LetBinding
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN ModuleInfo -> ModuleName -> ImportDirective -> LetBinding
LetOpen  ModuleInfo
i ModuleName
x ImportDirective
dir
  killRange (LetDeclaredVariable BindName
x)  = (BindName -> LetBinding) -> BindName -> LetBinding
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN 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
_                    = QName
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 = (a -> Bool) -> [a] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
Fold.any a -> Bool
forall a. AnyAbstract a => a -> Bool
anyAbstract

instance AnyAbstract Declaration where
  anyAbstract :: Declaration -> Bool
anyAbstract (Axiom KindOfName
_ DefInfo
i ArgInfo
_ Maybe [Occurrence]
_ QName
_ Expr
_)    = DefInfo -> IsAbstract
forall t. DefInfo' t -> IsAbstract
defAbstract DefInfo
i IsAbstract -> IsAbstract -> Bool
forall a. Eq a => a -> a -> Bool
== IsAbstract
AbstractDef
  anyAbstract (Field DefInfo
i QName
_ Arg Expr
_)          = DefInfo -> IsAbstract
forall t. DefInfo' t -> IsAbstract
defAbstract DefInfo
i IsAbstract -> IsAbstract -> Bool
forall a. Eq a => a -> a -> Bool
== IsAbstract
AbstractDef
  anyAbstract (Mutual     MutualInfo
_ [Declaration]
ds)      = [Declaration] -> Bool
forall a. AnyAbstract a => a -> Bool
anyAbstract [Declaration]
ds
  anyAbstract (ScopedDecl ScopeInfo
_ [Declaration]
ds)      = [Declaration] -> Bool
forall a. AnyAbstract a => a -> Bool
anyAbstract [Declaration]
ds
  anyAbstract (Section Range
_ Erased
_ ModuleName
_ GeneralizeTelescope
_ [Declaration]
ds)   = [Declaration] -> Bool
forall a. AnyAbstract a => a -> Bool
anyAbstract [Declaration]
ds
  anyAbstract (FunDef DefInfo
i QName
_ [Clause]
_)         = DefInfo -> IsAbstract
forall t. DefInfo' t -> IsAbstract
defAbstract DefInfo
i IsAbstract -> IsAbstract -> Bool
forall a. Eq a => a -> a -> Bool
== IsAbstract
AbstractDef
  anyAbstract (DataDef DefInfo
i QName
_ UniverseCheck
_ DataDefParams
_ [Declaration]
_)    = DefInfo -> IsAbstract
forall t. DefInfo' t -> IsAbstract
defAbstract DefInfo
i IsAbstract -> IsAbstract -> Bool
forall a. Eq a => a -> a -> Bool
== IsAbstract
AbstractDef
  anyAbstract (RecDef DefInfo
i QName
_ UniverseCheck
_ RecordDirectives
_ DataDefParams
_ Expr
_ [Declaration]
_) = DefInfo -> IsAbstract
forall t. DefInfo' t -> IsAbstract
defAbstract DefInfo
i IsAbstract -> IsAbstract -> Bool
forall a. Eq a => a -> a -> Bool
== IsAbstract
AbstractDef
  anyAbstract (DataSig DefInfo
i Erased
_ QName
_ GeneralizeTelescope
_ Expr
_)    = DefInfo -> IsAbstract
forall t. DefInfo' t -> IsAbstract
defAbstract DefInfo
i IsAbstract -> IsAbstract -> Bool
forall a. Eq a => a -> a -> Bool
== IsAbstract
AbstractDef
  anyAbstract (RecSig DefInfo
i Erased
_ QName
_ GeneralizeTelescope
_ Expr
_)     = DefInfo -> IsAbstract
forall t. DefInfo' t -> IsAbstract
defAbstract DefInfo
i IsAbstract -> IsAbstract -> Bool
forall a. Eq a => a -> a -> Bool
== IsAbstract
AbstractDef
  anyAbstract Declaration
_                      = Bool
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) (Expr -> NamedArg Expr
forall a. a -> NamedArg a
defaultNamedArg (Expr -> NamedArg Expr) -> Expr -> NamedArg Expr
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  = QName -> Range
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 (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ AbstractName -> Expr
forall a. NameToExpr a => a -> Expr
nameToExpr AbstractName
x  -- Can be 'isDefName', 'MacroName', 'QuotableName'.
    FieldName List1 AbstractName
xs         -> ProjOrigin -> AmbiguousQName -> Expr
Proj ProjOrigin
ProjSystem (AmbiguousQName -> Expr)
-> (List1 AbstractName -> AmbiguousQName)
-> List1 AbstractName
-> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NonEmpty QName -> AmbiguousQName
AmbQ (NonEmpty QName -> AmbiguousQName)
-> (List1 AbstractName -> NonEmpty QName)
-> List1 AbstractName
-> AmbiguousQName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (AbstractName -> QName) -> List1 AbstractName -> NonEmpty QName
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap AbstractName -> QName
anameName (List1 AbstractName -> Expr) -> List1 AbstractName -> Expr
forall a b. (a -> b) -> a -> b
$ List1 AbstractName
xs
    ConstructorName Set Induction
_ List1 AbstractName
xs -> AmbiguousQName -> Expr
Con (AmbiguousQName -> Expr)
-> (List1 AbstractName -> AmbiguousQName)
-> List1 AbstractName
-> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NonEmpty QName -> AmbiguousQName
AmbQ (NonEmpty QName -> AmbiguousQName)
-> (List1 AbstractName -> NonEmpty QName)
-> List1 AbstractName
-> AmbiguousQName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (AbstractName -> QName) -> List1 AbstractName -> NonEmpty QName
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap AbstractName -> QName
anameName (List1 AbstractName -> Expr) -> List1 AbstractName -> Expr
forall a b. (a -> b) -> a -> b
$ List1 AbstractName
xs
    PatternSynResName List1 AbstractName
xs -> AmbiguousQName -> Expr
PatternSyn (AmbiguousQName -> Expr)
-> (List1 AbstractName -> AmbiguousQName)
-> List1 AbstractName
-> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NonEmpty QName -> AmbiguousQName
AmbQ (NonEmpty QName -> AmbiguousQName)
-> (List1 AbstractName -> NonEmpty QName)
-> List1 AbstractName
-> AmbiguousQName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (AbstractName -> QName) -> List1 AbstractName -> NonEmpty QName
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap AbstractName -> QName
anameName (List1 AbstractName -> Expr) -> List1 AbstractName -> Expr
forall a b. (a -> b) -> a -> b
$ List1 AbstractName
xs
    ResolvedName
UnknownName          -> Expr
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
_       = Expr
forall a. HasCallStack => a
__IMPOSSIBLE__

app :: Expr -> [NamedArg Expr] -> Expr
app :: Expr -> [NamedArg Expr] -> Expr
app = (Expr -> NamedArg Expr -> Expr) -> Expr -> [NamedArg Expr] -> Expr
forall b a. (b -> a -> b) -> b -> [a] -> b
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 LetBinding -> [LetBinding] -> List1 LetBinding
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` (NamedArg Pattern -> NamedArg Expr)
-> [NamedArg Pattern] -> [NamedArg Expr]
forall a b. (a -> b) -> [a] -> [b]
map ((Named NamedName Pattern -> Named NamedName Expr)
-> NamedArg Pattern -> NamedArg Expr
forall a b. (a -> b) -> Arg a -> Arg b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Pattern -> Expr)
-> Named NamedName Pattern -> Named NamedName Expr
forall a b. (a -> b) -> Named NamedName a -> Named NamedName b
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` (NamedArg Pattern -> NamedArg Expr)
-> [NamedArg Pattern] -> [NamedArg Expr]
forall a b. (a -> b) -> [a] -> [b]
map ((Named NamedName Pattern -> Named NamedName Expr)
-> NamedArg Pattern -> NamedArg Expr
forall a b. (a -> b) -> Arg a -> Arg b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Pattern -> Expr)
-> Named NamedName Pattern -> Named NamedName Expr
forall a b. (a -> b) -> Named NamedName a -> Named NamedName b
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` ((NamedArg Pattern -> NamedArg Expr)
-> [NamedArg Pattern] -> [NamedArg Expr]
forall a b. (a -> b) -> [a] -> [b]
map ((NamedArg Pattern -> NamedArg Expr)
 -> [NamedArg Pattern] -> [NamedArg Expr])
-> ((Pattern -> Expr) -> NamedArg Pattern -> NamedArg Expr)
-> (Pattern -> Expr)
-> [NamedArg Pattern]
-> [NamedArg Expr]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Named NamedName Pattern -> Named NamedName Expr)
-> NamedArg Pattern -> NamedArg Expr
forall a b. (a -> b) -> Arg a -> Arg b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Named NamedName Pattern -> Named NamedName Expr)
 -> NamedArg Pattern -> NamedArg Expr)
-> ((Pattern -> Expr)
    -> Named NamedName Pattern -> Named NamedName Expr)
-> (Pattern -> Expr)
-> NamedArg Pattern
-> NamedArg Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Pattern -> Expr)
-> Named NamedName Pattern -> Named NamedName Expr
forall a b. (a -> b) -> Named NamedName a -> Named NamedName b
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 (RecordAssigns -> Expr) -> RecordAssigns -> Expr
forall a b. (a -> b) -> a -> b
$ (FieldAssignment' Pattern -> Either Assign ModuleName)
-> [FieldAssignment' Pattern] -> RecordAssigns
forall a b. (a -> b) -> [a] -> [b]
map (Assign -> Either Assign ModuleName
forall a b. a -> Either a b
Left (Assign -> Either Assign ModuleName)
-> (FieldAssignment' Pattern -> Assign)
-> FieldAssignment' Pattern
-> Either Assign ModuleName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Pattern -> Expr) -> FieldAssignment' Pattern -> Assign
forall a b. (a -> b) -> FieldAssignment' a -> FieldAssignment' b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Pattern -> Expr
patternToExpr) [FieldAssignment' Pattern]
as
  EqualP{}           -> Expr
forall a. HasCallStack => a
__IMPOSSIBLE__  -- Andrea TODO: where is this used?
  WithP PatInfo
r Pattern
p          -> Expr
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
  = (Name -> Expr -> Expr) -> Expr -> [Name] -> Expr
forall a b. (a -> b -> b) -> b -> [a] -> b
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 (NamedArg Binder -> LamBinding) -> NamedArg Binder -> LamBinding
forall a b. (a -> b) -> a -> b
$ Binder -> NamedArg Binder
forall a. a -> NamedArg a
defaultNamedArg (Binder -> NamedArg Binder) -> Binder -> NamedArg Binder
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 = (b -> b) -> a -> a
(b -> b) -> t b -> t b
forall a b. (a -> b) -> t a -> t b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((b -> b) -> a -> a)
-> ([(Name, Expr)] -> b -> b) -> [(Name, Expr)] -> a -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Name, Expr)] -> b -> b
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) = ([(Name, Expr)] -> a -> a
forall a. SubstExpr a => [(Name, Expr)] -> a -> a
substExpr [(Name, Expr)]
s a
x, [(Name, Expr)] -> b -> b
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)  = a -> Either a b
forall a b. a -> Either a b
Left ([(Name, Expr)] -> a -> a
forall a. SubstExpr a => [(Name, Expr)] -> a -> a
substExpr [(Name, Expr)]
s a
x)
  substExpr [(Name, Expr)]
s (Right b
y) = b -> Either a b
forall a b. b -> Either a b
Right ([(Name, Expr)] -> b -> b
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)]
_ = Name -> Name
forall a. a -> a
id

instance SubstExpr ModuleName where
  substExpr :: [(Name, Expr)] -> ModuleName -> ModuleName
substExpr [(Name, Expr)]
_ = ModuleName -> ModuleName
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           -> Expr -> Maybe Expr -> Expr
forall a. a -> Maybe a -> a
fromMaybe Expr
e (Name -> [(Name, Expr)] -> Maybe Expr
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 ([(Name, Expr)] -> Expr -> Expr
forall a. SubstExpr a => [(Name, Expr)] -> a -> a
substExpr [(Name, Expr)]
s Expr
e) ([(Name, Expr)] -> NamedArg Expr -> NamedArg Expr
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 ([(Name, Expr)] -> RecordAssigns -> RecordAssigns
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 ([(Name, Expr)] -> Expr -> Expr
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{}  -> Expr
forall a. HasCallStack => a
__IMPOSSIBLE__
    Dot{}           -> Expr
forall a. HasCallStack => a
__IMPOSSIBLE__
    WithApp{}       -> Expr
forall a. HasCallStack => a
__IMPOSSIBLE__
    Lam{}           -> Expr
forall a. HasCallStack => a
__IMPOSSIBLE__
    AbsurdLam{}     -> Expr
forall a. HasCallStack => a
__IMPOSSIBLE__
    ExtendedLam{}   -> Expr
forall a. HasCallStack => a
__IMPOSSIBLE__
    Pi{}            -> Expr
forall a. HasCallStack => a
__IMPOSSIBLE__
    Generalized{}   -> Expr
forall a. HasCallStack => a
__IMPOSSIBLE__
    Fun{}           -> Expr
forall a. HasCallStack => a
__IMPOSSIBLE__
    Let{}           -> Expr
forall a. HasCallStack => a
__IMPOSSIBLE__
    RecUpdate{}     -> Expr
forall a. HasCallStack => a
__IMPOSSIBLE__
    Quote{}         -> Expr
forall a. HasCallStack => a
__IMPOSSIBLE__
    QuoteTerm{}     -> Expr
forall a. HasCallStack => a
__IMPOSSIBLE__
    Unquote{}       -> Expr
forall a. HasCallStack => a
__IMPOSSIBLE__
    DontCare{}      -> Expr
forall a. HasCallStack => a
__IMPOSSIBLE__
    Macro{}         -> Expr
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'))
      | Arg Name -> [Arg (Named_ a)] -> Bool
forall {a}.
(NameOf a ~ NamedName, LensHiding a, LensNamed a) =>
Arg Name -> [a] -> Bool
matchNext Arg Name
n [Arg (Named_ a)]
as = (a, [Arg (Named_ a)]) -> Maybe (a, [Arg (Named_ a)])
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (Arg (Named_ a) -> a
forall a. NamedArg a -> a
namedArg Arg (Named_ a)
a, [Arg (Named_ a)]
as')
      | Arg Name -> Bool
forall a. LensHiding a => a -> Bool
visible Arg Name
n      = Maybe (a, [Arg (Named_ a)])
forall a. Maybe a
Nothing
      | Bool
otherwise      = (a, [Arg (Named_ a)]) -> Maybe (a, [Arg (Named_ a)])
forall a. a -> Maybe a
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) = Arg Name -> a -> Bool
forall a b. (LensHiding a, LensHiding b) => a -> b -> Bool
sameHiding Arg Name
n a
a Bool -> Bool -> Bool
&& Bool -> (String -> Bool) -> Maybe String -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
True (String
x String -> String -> Bool
forall a. Eq a => a -> a -> Bool
==) (a -> Maybe String
forall a. (LensNamed a, NameOf a ~ NamedName) => a -> Maybe String
bareNameOf a
a)
      where
        x :: String
x = Name -> String
C.nameToRawName (Name -> String) -> Name -> String
forall a b. (a -> b) -> a -> b
$ Name -> Name
nameConcrete (Name -> Name) -> Name -> Name
forall a b. (a -> b) -> a -> b
$ Arg Name -> Name
forall e. Arg e -> e
unArg Arg Name
n

    matchArgs :: Range
-> [Arg Name]
-> [Arg (Named_ a)]
-> Maybe ([(Name, a)], [Arg Name])
matchArgs Range
r [] []     = ([(Name, a)], [Arg Name]) -> Maybe ([(Name, a)], [Arg Name])
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return ([], [])
    matchArgs Range
r [] [Arg (Named_ a)]
as     = Maybe ([(Name, a)], [Arg Name])
forall a. Maybe a
Nothing
    matchArgs Range
r (Arg Name
n:[Arg Name]
ns) [] | Arg Name -> Bool
forall a. LensHiding a => a -> Bool
visible Arg Name
n = ([(Name, a)], [Arg Name]) -> Maybe ([(Name, a)], [Arg Name])
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return ([], Arg Name
n Arg Name -> [Arg Name] -> [Arg Name]
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
      ([(Name, a)] -> [(Name, a)])
-> ([(Name, a)], [Arg Name]) -> ([(Name, a)], [Arg Name])
forall a b c. (a -> b) -> (a, c) -> (b, c)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first ((Arg Name -> Name
forall e. Arg e -> e
unArg Arg Name
n, a
p) (Name, a) -> [(Name, a)] -> [(Name, a)]
forall a. a -> [a] -> [a]
:) (([(Name, a)], [Arg Name]) -> ([(Name, a)], [Arg Name]))
-> Maybe ([(Name, a)], [Arg Name])
-> Maybe ([(Name, a)], [Arg Name])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Range
-> [Arg Name]
-> [Arg (Named_ a)]
-> Maybe ([(Name, a)], [Arg Name])
matchArgs (a -> Range
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]
  | UnfoldingDeclS
  deriving Int -> DeclarationSpine -> ShowS
[DeclarationSpine] -> ShowS
DeclarationSpine -> String
(Int -> DeclarationSpine -> ShowS)
-> (DeclarationSpine -> String)
-> ([DeclarationSpine] -> ShowS)
-> Show DeclarationSpine
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> DeclarationSpine -> ShowS
showsPrec :: Int -> DeclarationSpine -> ShowS
$cshow :: DeclarationSpine -> String
show :: DeclarationSpine -> String
$cshowList :: [DeclarationSpine] -> ShowS
showList :: [DeclarationSpine] -> ShowS
Show

-- | Clause spines.

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

-- | Right-hand side spines.

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

-- | Spines corresponding to 'WhereDeclarations' values.

data WhereDeclarationsSpine = WhereDeclsS (Maybe DeclarationSpine)
  deriving Int -> WhereDeclarationsSpine -> ShowS
[WhereDeclarationsSpine] -> ShowS
WhereDeclarationsSpine -> String
(Int -> WhereDeclarationsSpine -> ShowS)
-> (WhereDeclarationsSpine -> String)
-> ([WhereDeclarationsSpine] -> ShowS)
-> Show WhereDeclarationsSpine
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> WhereDeclarationsSpine -> ShowS
showsPrec :: Int -> WhereDeclarationsSpine -> ShowS
$cshow :: WhereDeclarationsSpine -> String
show :: WhereDeclarationsSpine -> String
$cshowList :: [WhereDeclarationsSpine] -> ShowS
showList :: [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 ((Declaration -> DeclarationSpine)
-> [Declaration] -> [DeclarationSpine]
forall a b. (a -> b) -> [a] -> [b]
map Declaration -> DeclarationSpine
declarationSpine [Declaration]
ds)
  Section Range
_ Erased
_ ModuleName
_ GeneralizeTelescope
_ [Declaration]
ds      -> [DeclarationSpine] -> DeclarationSpine
SectionS ((Declaration -> DeclarationSpine)
-> [Declaration] -> [DeclarationSpine]
forall a b. (a -> b) -> [a] -> [b]
map Declaration -> DeclarationSpine
declarationSpine [Declaration]
ds)
  Apply ModuleInfo
_ Erased
_ 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
_ [Clause]
cs           -> [ClauseSpine] -> DeclarationSpine
FunDefS ((Clause -> ClauseSpine) -> [Clause] -> [ClauseSpine]
forall a b. (a -> b) -> [a] -> [b]
map Clause -> ClauseSpine
clauseSpine [Clause]
cs)
  DataSig DefInfo
_ Erased
_ QName
_ GeneralizeTelescope
_ Expr
_       -> DeclarationSpine
DataSigS
  DataDef DefInfo
_ QName
_ UniverseCheck
_ DataDefParams
_ [Declaration]
_       -> DeclarationSpine
DataDefS
  RecSig DefInfo
_ Erased
_ QName
_ GeneralizeTelescope
_ Expr
_        -> DeclarationSpine
RecSigS
  RecDef DefInfo
_ QName
_ UniverseCheck
_ RecordDirectives
_ DataDefParams
_ Expr
_ [Declaration]
ds   -> [DeclarationSpine] -> DeclarationSpine
RecDefS ((Declaration -> DeclarationSpine)
-> [Declaration] -> [DeclarationSpine]
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 ((Declaration -> DeclarationSpine)
-> [Declaration] -> [DeclarationSpine]
forall a b. (a -> b) -> [a] -> [b]
map Declaration -> DeclarationSpine
declarationSpine [Declaration]
ds)
  UnfoldingDecl Range
_ [QName]
_       -> DeclarationSpine
UnquoteDeclS

-- | 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]
_ List1 Clause
cs        -> List1 ClauseSpine -> RHSSpine
WithRHSS (List1 ClauseSpine -> RHSSpine) -> List1 ClauseSpine -> RHSSpine
forall a b. (a -> b) -> a -> b
$ (Clause -> ClauseSpine) -> List1 Clause -> List1 ClauseSpine
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Clause -> ClauseSpine
clauseSpine List1 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 ((Declaration -> DeclarationSpine)
-> Maybe Declaration -> Maybe DeclarationSpine
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Declaration -> DeclarationSpine
declarationSpine Maybe Declaration
md)