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

import Prelude hiding (null)

import Control.DeepSeq

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

import GHC.Generics (Generic)

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

import Agda.TypeChecking.Positivity.Occurrence

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

import Agda.Utils.Impossible

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

newtype BindName = BindName { BindName -> Name
unBind :: Name }
  deriving (Int -> BindName -> ShowS
[BindName] -> ShowS
BindName -> 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
text String
s, Int -> Doc -> Doc
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
<+> Doc
"->" Doc -> Doc -> Doc
<+> 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 ModuleName GeneralizeTelescope [Declaration]
  | Apply      ModuleInfo ModuleName ModuleApplication ScopeCopyInfo ImportDirective
    -- ^ The @ImportDirective@ is for highlighting purposes.
  | Import     ModuleInfo ModuleName ImportDirective
    -- ^ The @ImportDirective@ is for highlighting purposes.
  | Pragma     Range      Pragma
  | Open       ModuleInfo ModuleName ImportDirective
    -- ^ only retained for highlighting purposes
  | FunDef     DefInfo QName Delayed [Clause] -- ^ sequence of function clauses
  | DataSig    DefInfo QName GeneralizeTelescope Type -- ^ lone data signature
  | DataDef    DefInfo QName UniverseCheck DataDefParams [Constructor]
  | RecSig     DefInfo QName GeneralizeTelescope Type -- ^ lone record signature
  | RecDef     DefInfo QName UniverseCheck RecordDirectives DataDefParams Type [Declaration]
      -- ^ The 'Type' gives the constructor type telescope, @(x1 : A1)..(xn : An) -> Prop@,
      --   and the optional name is the constructor's name.
      --   The optional 'Range' is for the @pattern@ attribute.
  | PatternSynDef QName [Arg BindName] (Pattern' Void)
      -- ^ Only for highlighting purposes
  | UnquoteDecl MutualInfo [DefInfo] [QName] Expr
  | UnquoteDef  [DefInfo] [QName] Expr
  | UnquoteData [DefInfo] QName UniverseCheck [DefInfo] [QName] Expr
  | ScopedDecl ScopeInfo [Declaration]  -- ^ scope annotation
  deriving (Int -> Declaration -> ShowS
[Declaration] -> ShowS
Declaration -> 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 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 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] [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 [Clause]
c    == WithRHS QName
a' [WithExpr]
b' [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
&& ([Clause]
c [Clause] -> [Clause] -> Bool
forall a. Eq a => a -> a -> Bool
== [Clause]
c')
  RewriteRHS [RewriteEqn]
a [ProblemEq]
b RHS
c WhereDeclarations
d == RewriteRHS [RewriteEqn]
a' [ProblemEq]
b' RHS
c' WhereDeclarations
d' = [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 ModuleName
b1 GeneralizeTelescope
c1 [Declaration]
d1            == Section Range
a2 ModuleName
b2 GeneralizeTelescope
c2 [Declaration]
d2            = (Range
a1, ModuleName
b1, GeneralizeTelescope
c1, [Declaration]
d1) (Range, ModuleName, GeneralizeTelescope, [Declaration])
-> (Range, ModuleName, GeneralizeTelescope, [Declaration]) -> Bool
forall a. Eq a => a -> a -> Bool
== (Range
a2, ModuleName
b2, GeneralizeTelescope
c2, [Declaration]
d2)
  Apply ModuleInfo
a1 ModuleName
b1 ModuleApplication
c1 ScopeCopyInfo
d1 ImportDirective
e1           == Apply ModuleInfo
a2 ModuleName
b2 ModuleApplication
c2 ScopeCopyInfo
d2 ImportDirective
e2           = (ModuleInfo
a1, ModuleName
b1, ModuleApplication
c1, ScopeCopyInfo
d1, ImportDirective
e1) (ModuleInfo, ModuleName, ModuleApplication, ScopeCopyInfo,
 ImportDirective)
-> (ModuleInfo, ModuleName, ModuleApplication, ScopeCopyInfo,
    ImportDirective)
-> Bool
forall a. Eq a => a -> a -> Bool
== (ModuleInfo
a2, ModuleName
b2, ModuleApplication
c2, ScopeCopyInfo
d2, ImportDirective
e2)
  Import ModuleInfo
a1 ModuleName
b1 ImportDirective
c1                == Import ModuleInfo
a2 ModuleName
b2 ImportDirective
c2                = (ModuleInfo
a1, ModuleName
b1, ImportDirective
c1) (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 Delayed
c1 [Clause]
d1             == FunDef DefInfo
a2 QName
b2 Delayed
c2 [Clause]
d2             = (DefInfo
a1, QName
b1, Delayed
c1, [Clause]
d1) (DefInfo, QName, Delayed, [Clause])
-> (DefInfo, QName, Delayed, [Clause]) -> Bool
forall a. Eq a => a -> a -> Bool
== (DefInfo
a2, QName
b2, Delayed
c2, [Clause]
d2)
  DataSig DefInfo
a1 QName
b1 GeneralizeTelescope
c1 Expr
d1            == DataSig DefInfo
a2 QName
b2 GeneralizeTelescope
c2 Expr
d2            = (DefInfo
a1, QName
b1, GeneralizeTelescope
c1, Expr
d1) (DefInfo, QName, GeneralizeTelescope, Expr)
-> (DefInfo, QName, GeneralizeTelescope, Expr) -> Bool
forall a. Eq a => a -> a -> Bool
== (DefInfo
a2, QName
b2, GeneralizeTelescope
c2, Expr
d2)
  DataDef DefInfo
a1 QName
b1 UniverseCheck
c1 DataDefParams
d1 [Declaration]
e1         == DataDef DefInfo
a2 QName
b2 UniverseCheck
c2 DataDefParams
d2 [Declaration]
e2         = (DefInfo
a1, QName
b1, UniverseCheck
c1, DataDefParams
d1, [Declaration]
e1) (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 QName
b1 GeneralizeTelescope
c1 Expr
d1             == RecSig DefInfo
a2 QName
b2 GeneralizeTelescope
c2 Expr
d2             = (DefInfo
a1, QName
b1, GeneralizeTelescope
c1, Expr
d1) (DefInfo, QName, GeneralizeTelescope, Expr)
-> (DefInfo, QName, GeneralizeTelescope, Expr) -> Bool
forall a. Eq a => a -> a -> Bool
== (DefInfo
a2, QName
b2, GeneralizeTelescope
c2, Expr
d2)
  RecDef DefInfo
a1 QName
b1 UniverseCheck
c1 RecordDirectives
d1 DataDefParams
e1 Expr
f1 [Declaration]
g1    == RecDef DefInfo
a2 QName
b2 UniverseCheck
c2 RecordDirectives
d2 DataDefParams
e2 Expr
f2 [Declaration]
g2    = (DefInfo
a1, QName
b1, UniverseCheck
c1, RecordDirectives
d1, DataDefParams
e1, Expr
f1, [Declaration]
g1) (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)

  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 ModuleName
_ GeneralizeTelescope
_ [Declaration]
_    ) = Range -> Range
forall a. HasRange a => a -> Range
getRange Range
i
    getRange (Apply      ModuleInfo
i 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
_ Delayed
_ [Clause]
_    ) = DefInfo -> Range
forall a. HasRange a => a -> Range
getRange DefInfo
i
    getRange (DataSig    DefInfo
i 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 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)

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 [Clause]
cs)          = [WithExpr] -> [Clause] -> Range
forall u t. (HasRange u, HasRange t) => u -> t -> Range
fuseRange [WithExpr]
e [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 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 a b c.
(KillRange a, KillRange b) =>
(a -> b -> c) -> a -> b -> c
killRange2 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 a b c.
(KillRange a, KillRange b) =>
(a -> b -> c) -> a -> b -> c
killRange2 TacticAttr -> NamedArg Binder -> LamBinding
DomainFree TacticAttr
t NamedArg Binder
x
  killRange (DomainFull TypedBinding
b)   = (TypedBinding -> LamBinding) -> TypedBinding -> LamBinding
forall a b. KillRange a => (a -> b) -> a -> b
killRange1 TypedBinding -> LamBinding
DomainFull TypedBinding
b

instance KillRange GeneralizeTelescope where
  killRange :: KillRangeT GeneralizeTelescope
killRange (GeneralizeTel Map QName Name
s Telescope
tel) = Map QName Name -> Telescope -> GeneralizeTelescope
GeneralizeTel Map QName Name
s (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 a b c.
(KillRange a, KillRange b) =>
(a -> b -> c) -> a -> b -> c
killRange2 TacticAttr -> Bool -> TypedBindingInfo
TypedBindingInfo TacticAttr
a Bool
b

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

instance KillRange Expr where
  killRange :: Expr -> Expr
killRange (Var Name
x)                  = (Name -> Expr) -> Name -> Expr
forall a b. KillRange a => (a -> b) -> a -> b
killRange1 Name -> Expr
Var Name
x
  killRange (Def' QName
x Suffix
v)               = (QName -> Suffix -> Expr) -> QName -> Suffix -> Expr
forall a b c.
(KillRange a, KillRange b) =>
(a -> b -> c) -> a -> b -> c
killRange2 QName -> Suffix -> Expr
Def' QName
x Suffix
v
  killRange (Proj ProjOrigin
o AmbiguousQName
x)               = (AmbiguousQName -> Expr) -> AmbiguousQName -> Expr
forall a b. KillRange a => (a -> b) -> a -> b
killRange1 (ProjOrigin -> AmbiguousQName -> Expr
Proj ProjOrigin
o) AmbiguousQName
x
  killRange (Con AmbiguousQName
x)                  = (AmbiguousQName -> Expr) -> AmbiguousQName -> Expr
forall a b. KillRange a => (a -> b) -> a -> b
killRange1 AmbiguousQName -> Expr
Con AmbiguousQName
x
  killRange (Lit ExprInfo
i Literal
l)                = (ExprInfo -> Literal -> Expr) -> ExprInfo -> Literal -> Expr
forall a b c.
(KillRange a, KillRange b) =>
(a -> b -> c) -> a -> b -> c
killRange2 ExprInfo -> Literal -> Expr
Lit ExprInfo
i Literal
l
  killRange (QuestionMark MetaInfo
i InteractionId
ii)      = (MetaInfo -> InteractionId -> Expr)
-> MetaInfo -> InteractionId -> Expr
forall a b c.
(KillRange a, KillRange b) =>
(a -> b -> c) -> a -> b -> c
killRange2 MetaInfo -> InteractionId -> Expr
QuestionMark MetaInfo
i InteractionId
ii
  killRange (Underscore  MetaInfo
i)          = (MetaInfo -> Expr) -> MetaInfo -> Expr
forall a b. KillRange a => (a -> b) -> a -> b
killRange1 MetaInfo -> Expr
Underscore MetaInfo
i
  killRange (Dot ExprInfo
i Expr
e)                = (ExprInfo -> Expr -> Expr) -> ExprInfo -> Expr -> Expr
forall a b c.
(KillRange a, KillRange b) =>
(a -> b -> c) -> a -> b -> c
killRange2 ExprInfo -> Expr -> Expr
Dot ExprInfo
i Expr
e
  killRange (App AppInfo
i Expr
e1 NamedArg Expr
e2)            = (AppInfo -> Expr -> NamedArg Expr -> Expr)
-> AppInfo -> Expr -> NamedArg Expr -> Expr
forall a b c d.
(KillRange a, KillRange b, KillRange c) =>
(a -> b -> c -> d) -> a -> b -> c -> d
killRange3 AppInfo -> Expr -> NamedArg Expr -> Expr
App AppInfo
i Expr
e1 NamedArg Expr
e2
  killRange (WithApp ExprInfo
i Expr
e [Expr]
es)         = (ExprInfo -> Expr -> [Expr] -> Expr)
-> ExprInfo -> Expr -> [Expr] -> Expr
forall a b c d.
(KillRange a, KillRange b, KillRange c) =>
(a -> b -> c -> d) -> a -> b -> c -> d
killRange3 ExprInfo -> Expr -> [Expr] -> Expr
WithApp ExprInfo
i Expr
e [Expr]
es
  killRange (Lam ExprInfo
i LamBinding
b Expr
e)              = (ExprInfo -> LamBinding -> Expr -> Expr)
-> ExprInfo -> LamBinding -> Expr -> Expr
forall a b c d.
(KillRange a, KillRange b, KillRange c) =>
(a -> b -> c -> d) -> a -> b -> c -> d
killRange3 ExprInfo -> LamBinding -> Expr -> Expr
Lam ExprInfo
i LamBinding
b Expr
e
  killRange (AbsurdLam ExprInfo
i Hiding
h)          = (ExprInfo -> Hiding -> Expr) -> ExprInfo -> Hiding -> Expr
forall a b c.
(KillRange a, KillRange b) =>
(a -> b -> c) -> a -> b -> c
killRange2 ExprInfo -> Hiding -> Expr
AbsurdLam ExprInfo
i Hiding
h
  killRange (ExtendedLam ExprInfo
i DefInfo
n Erased
e QName
d List1 Clause
ps) = (ExprInfo -> DefInfo -> Erased -> QName -> List1 Clause -> Expr)
-> ExprInfo -> DefInfo -> Erased -> QName -> List1 Clause -> Expr
forall a b c d e f.
(KillRange a, KillRange b, KillRange c, KillRange d,
 KillRange e) =>
(a -> b -> c -> d -> e -> f) -> a -> b -> c -> d -> e -> f
killRange5 ExprInfo -> DefInfo -> Erased -> QName -> List1 Clause -> Expr
ExtendedLam ExprInfo
i DefInfo
n Erased
e QName
d List1 Clause
ps
  killRange (Pi ExprInfo
i Telescope1
a Expr
b)               = (ExprInfo -> Telescope1 -> Expr -> Expr)
-> ExprInfo -> Telescope1 -> Expr -> Expr
forall a b c d.
(KillRange a, KillRange b, KillRange c) =>
(a -> b -> c -> d) -> a -> b -> c -> d
killRange3 ExprInfo -> Telescope1 -> Expr -> Expr
Pi ExprInfo
i Telescope1
a Expr
b
  killRange (Generalized Set QName
s Expr
x)        = (Expr -> Expr) -> Expr -> Expr
forall a b. KillRange a => (a -> b) -> a -> b
killRange1 (Set QName -> Expr -> Expr
Generalized Set QName
s) Expr
x
  killRange (Fun ExprInfo
i Arg Expr
a Expr
b)              = (ExprInfo -> Arg Expr -> Expr -> Expr)
-> ExprInfo -> Arg Expr -> Expr -> Expr
forall a b c d.
(KillRange a, KillRange b, KillRange c) =>
(a -> b -> c -> d) -> a -> b -> c -> d
killRange3 ExprInfo -> Arg Expr -> Expr -> Expr
Fun ExprInfo
i Arg Expr
a Expr
b
  killRange (Let ExprInfo
i List1 LetBinding
ds Expr
e)             = (ExprInfo -> List1 LetBinding -> Expr -> Expr)
-> ExprInfo -> List1 LetBinding -> Expr -> Expr
forall a b c d.
(KillRange a, KillRange b, KillRange c) =>
(a -> b -> c -> d) -> a -> b -> c -> d
killRange3 ExprInfo -> List1 LetBinding -> Expr -> Expr
Let ExprInfo
i List1 LetBinding
ds Expr
e
  killRange (Rec ExprInfo
i RecordAssigns
fs)               = (ExprInfo -> RecordAssigns -> Expr)
-> ExprInfo -> RecordAssigns -> Expr
forall a b c.
(KillRange a, KillRange b) =>
(a -> b -> c) -> a -> b -> c
killRange2 ExprInfo -> RecordAssigns -> Expr
Rec ExprInfo
i RecordAssigns
fs
  killRange (RecUpdate ExprInfo
i Expr
e Assigns
fs)       = (ExprInfo -> Expr -> Assigns -> Expr)
-> ExprInfo -> Expr -> Assigns -> Expr
forall a b c d.
(KillRange a, KillRange b, KillRange c) =>
(a -> b -> c -> d) -> a -> b -> c -> d
killRange3 ExprInfo -> Expr -> Assigns -> Expr
RecUpdate ExprInfo
i Expr
e Assigns
fs
  killRange (ScopedExpr ScopeInfo
s Expr
e)         = (Expr -> Expr) -> Expr -> Expr
forall a b. KillRange a => (a -> b) -> a -> b
killRange1 (ScopeInfo -> Expr -> Expr
ScopedExpr ScopeInfo
s) Expr
e
  killRange (Quote ExprInfo
i)                = (ExprInfo -> Expr) -> ExprInfo -> Expr
forall a b. KillRange a => (a -> b) -> a -> b
killRange1 ExprInfo -> Expr
Quote ExprInfo
i
  killRange (QuoteTerm ExprInfo
i)            = (ExprInfo -> Expr) -> ExprInfo -> Expr
forall a b. KillRange a => (a -> b) -> a -> b
killRange1 ExprInfo -> Expr
QuoteTerm ExprInfo
i
  killRange (Unquote ExprInfo
i)              = (ExprInfo -> Expr) -> ExprInfo -> Expr
forall a b. KillRange a => (a -> b) -> a -> b
killRange1 ExprInfo -> Expr
Unquote ExprInfo
i
  killRange (DontCare Expr
e)             = (Expr -> Expr) -> Expr -> Expr
forall a b. KillRange a => (a -> b) -> a -> b
killRange1 Expr -> Expr
DontCare Expr
e
  killRange (PatternSyn AmbiguousQName
x)           = (AmbiguousQName -> Expr) -> AmbiguousQName -> Expr
forall a b. KillRange a => (a -> b) -> a -> b
killRange1 AmbiguousQName -> Expr
PatternSyn AmbiguousQName
x
  killRange (Macro QName
x)                = (QName -> Expr) -> QName -> Expr
forall a b. KillRange a => (a -> b) -> a -> b
killRange1 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 a b c d e.
(KillRange a, KillRange b, KillRange c, KillRange d) =>
(a -> b -> c -> d -> e) -> a -> b -> c -> d -> e
killRange4 (\DefInfo
i ArgInfo
a QName
c Expr
d -> KindOfName
-> DefInfo
-> ArgInfo
-> Maybe [Occurrence]
-> QName
-> Expr
-> Declaration
Axiom KindOfName
p DefInfo
i ArgInfo
a Maybe [Occurrence]
b QName
c Expr
d) DefInfo
i ArgInfo
a QName
c Expr
d
  killRange (Generalize Set QName
s DefInfo
i ArgInfo
j QName
x Expr
e     ) = (DefInfo -> ArgInfo -> QName -> Expr -> Declaration)
-> DefInfo -> ArgInfo -> QName -> Expr -> Declaration
forall a b c d e.
(KillRange a, KillRange b, KillRange c, KillRange d) =>
(a -> b -> c -> d -> e) -> a -> b -> c -> d -> e
killRange4 (Set QName -> DefInfo -> ArgInfo -> QName -> Expr -> Declaration
Generalize Set QName
s) DefInfo
i ArgInfo
j QName
x Expr
e
  killRange (Field      DefInfo
i QName
a Arg Expr
b         ) = (DefInfo -> QName -> Arg Expr -> Declaration)
-> DefInfo -> QName -> Arg Expr -> Declaration
forall a b c d.
(KillRange a, KillRange b, KillRange c) =>
(a -> b -> c -> d) -> a -> b -> c -> d
killRange3 DefInfo -> QName -> Arg Expr -> Declaration
Field      DefInfo
i QName
a Arg Expr
b
  killRange (Mutual     MutualInfo
i [Declaration]
a           ) = (MutualInfo -> [Declaration] -> Declaration)
-> MutualInfo -> [Declaration] -> Declaration
forall a b c.
(KillRange a, KillRange b) =>
(a -> b -> c) -> a -> b -> c
killRange2 MutualInfo -> [Declaration] -> Declaration
Mutual     MutualInfo
i [Declaration]
a
  killRange (Section    Range
i ModuleName
a GeneralizeTelescope
b [Declaration]
c       ) = (Range
 -> ModuleName
 -> GeneralizeTelescope
 -> [Declaration]
 -> Declaration)
-> Range
-> ModuleName
-> GeneralizeTelescope
-> [Declaration]
-> Declaration
forall a b c d e.
(KillRange a, KillRange b, KillRange c, KillRange d) =>
(a -> b -> c -> d -> e) -> a -> b -> c -> d -> e
killRange4 Range
-> ModuleName
-> GeneralizeTelescope
-> [Declaration]
-> Declaration
Section    Range
i ModuleName
a GeneralizeTelescope
b [Declaration]
c
  killRange (Apply      ModuleInfo
i ModuleName
a ModuleApplication
b ScopeCopyInfo
c ImportDirective
d     ) = (ModuleInfo
 -> ModuleName
 -> ModuleApplication
 -> ScopeCopyInfo
 -> ImportDirective
 -> Declaration)
-> ModuleInfo
-> ModuleName
-> ModuleApplication
-> ScopeCopyInfo
-> ImportDirective
-> Declaration
forall a b c d e f.
(KillRange a, KillRange b, KillRange c, KillRange d,
 KillRange e) =>
(a -> b -> c -> d -> e -> f) -> a -> b -> c -> d -> e -> f
killRange5 ModuleInfo
-> ModuleName
-> ModuleApplication
-> ScopeCopyInfo
-> ImportDirective
-> Declaration
Apply      ModuleInfo
i ModuleName
a ModuleApplication
b ScopeCopyInfo
c ImportDirective
d
  killRange (Import     ModuleInfo
i ModuleName
a ImportDirective
b         ) = (ModuleInfo -> ModuleName -> ImportDirective -> Declaration)
-> ModuleInfo -> ModuleName -> ImportDirective -> Declaration
forall a b c d.
(KillRange a, KillRange b, KillRange c) =>
(a -> b -> c -> d) -> a -> b -> c -> d
killRange3 ModuleInfo -> ModuleName -> ImportDirective -> Declaration
Import     ModuleInfo
i ModuleName
a ImportDirective
b
  killRange (Primitive  DefInfo
i QName
a Arg Expr
b         ) = (DefInfo -> QName -> Arg Expr -> Declaration)
-> DefInfo -> QName -> Arg Expr -> Declaration
forall a b c d.
(KillRange a, KillRange b, KillRange c) =>
(a -> b -> c -> d) -> a -> b -> c -> d
killRange3 DefInfo -> QName -> Arg Expr -> Declaration
Primitive  DefInfo
i QName
a Arg Expr
b
  killRange (Pragma     Range
i Pragma
a           ) = Range -> Pragma -> Declaration
Pragma (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 a b c d.
(KillRange a, KillRange b, KillRange c) =>
(a -> b -> c -> d) -> a -> b -> c -> d
killRange3 ModuleInfo -> ModuleName -> ImportDirective -> Declaration
Open       ModuleInfo
i ModuleName
x ImportDirective
dir
  killRange (ScopedDecl ScopeInfo
a [Declaration]
d           ) = ([Declaration] -> Declaration) -> [Declaration] -> Declaration
forall a b. KillRange a => (a -> b) -> a -> b
killRange1 (ScopeInfo -> [Declaration] -> Declaration
ScopedDecl ScopeInfo
a) [Declaration]
d
  killRange (FunDef  DefInfo
i QName
a Delayed
b [Clause]
c          ) = (DefInfo -> QName -> Delayed -> [Clause] -> Declaration)
-> DefInfo -> QName -> Delayed -> [Clause] -> Declaration
forall a b c d e.
(KillRange a, KillRange b, KillRange c, KillRange d) =>
(a -> b -> c -> d -> e) -> a -> b -> c -> d -> e
killRange4 DefInfo -> QName -> Delayed -> [Clause] -> Declaration
FunDef  DefInfo
i QName
a Delayed
b [Clause]
c
  killRange (DataSig DefInfo
i QName
a GeneralizeTelescope
b Expr
c          ) = (DefInfo -> QName -> GeneralizeTelescope -> Expr -> Declaration)
-> DefInfo -> QName -> GeneralizeTelescope -> Expr -> Declaration
forall a b c d e.
(KillRange a, KillRange b, KillRange c, KillRange d) =>
(a -> b -> c -> d -> e) -> a -> b -> c -> d -> e
killRange4 DefInfo -> QName -> GeneralizeTelescope -> Expr -> Declaration
DataSig DefInfo
i QName
a GeneralizeTelescope
b Expr
c
  killRange (DataDef DefInfo
i QName
a UniverseCheck
b DataDefParams
c [Declaration]
d        ) = (DefInfo
 -> QName
 -> UniverseCheck
 -> DataDefParams
 -> [Declaration]
 -> Declaration)
-> DefInfo
-> QName
-> UniverseCheck
-> DataDefParams
-> [Declaration]
-> Declaration
forall a b c d e f.
(KillRange a, KillRange b, KillRange c, KillRange d,
 KillRange e) =>
(a -> b -> c -> d -> e -> f) -> a -> b -> c -> d -> e -> f
killRange5 DefInfo
-> QName
-> UniverseCheck
-> DataDefParams
-> [Declaration]
-> Declaration
DataDef DefInfo
i QName
a UniverseCheck
b DataDefParams
c [Declaration]
d
  killRange (RecSig  DefInfo
i QName
a GeneralizeTelescope
b Expr
c          ) = (DefInfo -> QName -> GeneralizeTelescope -> Expr -> Declaration)
-> DefInfo -> QName -> GeneralizeTelescope -> Expr -> Declaration
forall a b c d e.
(KillRange a, KillRange b, KillRange c, KillRange d) =>
(a -> b -> c -> d -> e) -> a -> b -> c -> d -> e
killRange4 DefInfo -> QName -> GeneralizeTelescope -> Expr -> Declaration
RecSig  DefInfo
i QName
a GeneralizeTelescope
b Expr
c
  killRange (RecDef  DefInfo
i QName
a UniverseCheck
b RecordDirectives
c DataDefParams
d Expr
e [Declaration]
f    ) = (DefInfo
 -> QName
 -> UniverseCheck
 -> RecordDirectives
 -> DataDefParams
 -> Expr
 -> [Declaration]
 -> Declaration)
-> DefInfo
-> QName
-> UniverseCheck
-> RecordDirectives
-> DataDefParams
-> Expr
-> [Declaration]
-> Declaration
forall a b c d e f g h.
(KillRange a, KillRange b, KillRange c, KillRange d, KillRange e,
 KillRange f, KillRange g) =>
(a -> b -> c -> d -> e -> f -> g -> h)
-> a -> b -> c -> d -> e -> f -> g -> h
killRange7 DefInfo
-> QName
-> UniverseCheck
-> RecordDirectives
-> DataDefParams
-> Expr
-> [Declaration]
-> Declaration
RecDef  DefInfo
i QName
a UniverseCheck
b RecordDirectives
c DataDefParams
d Expr
e [Declaration]
f
  killRange (PatternSynDef QName
x [Arg BindName]
xs Pattern' Void
p     ) = (QName -> [Arg BindName] -> Pattern' Void -> Declaration)
-> QName -> [Arg BindName] -> Pattern' Void -> Declaration
forall a b c d.
(KillRange a, KillRange b, KillRange c) =>
(a -> b -> c -> d) -> a -> b -> c -> d
killRange3 QName -> [Arg BindName] -> Pattern' Void -> Declaration
PatternSynDef QName
x [Arg BindName]
xs Pattern' Void
p
  killRange (UnquoteDecl MutualInfo
mi [DefInfo]
i [QName]
x Expr
e     ) = (MutualInfo -> [DefInfo] -> [QName] -> Expr -> Declaration)
-> MutualInfo -> [DefInfo] -> [QName] -> Expr -> Declaration
forall a b c d e.
(KillRange a, KillRange b, KillRange c, KillRange d) =>
(a -> b -> c -> d -> e) -> a -> b -> c -> d -> e
killRange4 MutualInfo -> [DefInfo] -> [QName] -> Expr -> Declaration
UnquoteDecl MutualInfo
mi [DefInfo]
i [QName]
x Expr
e
  killRange (UnquoteDef [DefInfo]
i [QName]
x Expr
e         ) = ([DefInfo] -> [QName] -> Expr -> Declaration)
-> [DefInfo] -> [QName] -> Expr -> Declaration
forall a b c d.
(KillRange a, KillRange b, KillRange c) =>
(a -> b -> c -> d) -> a -> b -> c -> d
killRange3 [DefInfo] -> [QName] -> Expr -> Declaration
UnquoteDef [DefInfo]
i [QName]
x Expr
e
  killRange (UnquoteData [DefInfo]
i QName
xs UniverseCheck
uc [DefInfo]
j [QName]
cs Expr
e) = ([DefInfo]
 -> QName
 -> UniverseCheck
 -> [DefInfo]
 -> [QName]
 -> Expr
 -> Declaration)
-> [DefInfo]
-> QName
-> UniverseCheck
-> [DefInfo]
-> [QName]
-> Expr
-> Declaration
forall a b c d e f g.
(KillRange a, KillRange b, KillRange c, KillRange d, KillRange e,
 KillRange f) =>
(a -> b -> c -> d -> e -> f -> g)
-> a -> b -> c -> d -> e -> f -> g
killRange6 [DefInfo]
-> QName
-> UniverseCheck
-> [DefInfo]
-> [QName]
-> Expr
-> Declaration
UnquoteData [DefInfo]
i QName
xs UniverseCheck
uc [DefInfo]
j [QName]
cs Expr
e

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

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

instance KillRange e => KillRange (Pattern' e) where
  killRange :: KillRangeT (Pattern' e)
killRange (VarP BindName
x)           = (BindName -> Pattern' e) -> BindName -> Pattern' e
forall a b. KillRange a => (a -> b) -> a -> b
killRange1 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 a b c d.
(KillRange a, KillRange b, KillRange c) =>
(a -> b -> c -> d) -> a -> b -> c -> d
killRange3 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 a b c d.
(KillRange a, KillRange b, KillRange c) =>
(a -> b -> c -> d) -> a -> b -> c -> d
killRange3 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 a b c d.
(KillRange a, KillRange b, KillRange c) =>
(a -> b -> c -> d) -> a -> b -> c -> d
killRange3 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 a b. KillRange a => (a -> b) -> a -> b
killRange1 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 a b c d.
(KillRange a, KillRange b, KillRange c) =>
(a -> b -> c -> d) -> a -> b -> c -> d
killRange3 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 a b c.
(KillRange a, KillRange b) =>
(a -> b -> c) -> a -> b -> c
killRange2 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 a b. KillRange a => (a -> b) -> a -> b
killRange1 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 a b c.
(KillRange a, KillRange b) =>
(a -> b -> c) -> a -> b -> c
killRange2 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 a b c d.
(KillRange a, KillRange b, KillRange c) =>
(a -> b -> c -> d) -> a -> b -> c -> d
killRange3 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 a b c.
(KillRange a, KillRange b) =>
(a -> b -> c) -> a -> b -> c
killRange2 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 a b c.
(KillRange a, KillRange b) =>
(a -> b -> c) -> a -> b -> c
killRange2 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 a b c.
(KillRange a, KillRange b) =>
(a -> b -> c) -> a -> b -> c
killRange2 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 a b c d.
(KillRange a, KillRange b, KillRange c) =>
(a -> b -> c -> d) -> a -> b -> c -> d
killRange3 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 a b c d.
(KillRange a, KillRange b, KillRange c) =>
(a -> b -> c -> d) -> a -> b -> c -> d
killRange3 LHSInfo -> QName -> [NamedArg Pattern] -> SpineLHS
SpineLHS LHSInfo
i QName
a [NamedArg Pattern]
b

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

instance KillRange e => KillRange (LHSCore' e) where
  killRange :: KillRangeT (LHSCore' e)
killRange (LHSHead QName
a [NamedArg (Pattern' e)]
b)   = (QName -> [NamedArg (Pattern' e)] -> LHSCore' e)
-> QName -> [NamedArg (Pattern' e)] -> LHSCore' e
forall a b c.
(KillRange a, KillRange b) =>
(a -> b -> c) -> a -> b -> c
killRange2 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 a b c d.
(KillRange a, KillRange b, KillRange c) =>
(a -> b -> c -> d) -> a -> b -> c -> d
killRange3 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 a b c d.
(KillRange a, KillRange b, KillRange c) =>
(a -> b -> c -> d) -> a -> b -> c -> d
killRange3 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 a b c d e f.
(KillRange a, KillRange b, KillRange c, KillRange d,
 KillRange e) =>
(a -> b -> c -> d -> e -> f) -> a -> b -> c -> d -> e -> f
killRange5 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 a b c d.
(KillRange a, KillRange b, KillRange c) =>
(a -> b -> c -> d) -> a -> b -> c -> d
killRange3 Pattern -> Term -> Dom Type -> ProblemEq
ProblemEq Pattern
p Term
v Dom Type
a

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

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

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

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

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

-- class AllNames moved to Abstract.Views.DeclaredNames

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

axiomName :: Declaration -> QName
axiomName :: Declaration -> QName
axiomName (Axiom KindOfName
_ DefInfo
_ ArgInfo
_ Maybe [Occurrence]
_ QName
q Expr
_)  = QName
q
axiomName (ScopedDecl ScopeInfo
_ (Declaration
d:[Declaration]
_)) = Declaration -> QName
axiomName Declaration
d
axiomName Declaration
_                    = 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
_ ModuleName
_ GeneralizeTelescope
_ [Declaration]
ds)     = [Declaration] -> Bool
forall a. AnyAbstract a => a -> Bool
anyAbstract [Declaration]
ds
  anyAbstract (FunDef DefInfo
i QName
_ Delayed
_ [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 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 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 -> TacticAttr -> Expr
forall a. a -> Maybe a -> a
fromMaybe Expr
e (Name -> [(Name, Expr)] -> TacticAttr
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]
  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 [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
_ 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
_ ModuleName
_ ModuleApplication
_ ScopeCopyInfo
_ ImportDirective
_         -> DeclarationSpine
ApplyS
  Import ModuleInfo
_ ModuleName
_ ImportDirective
_            -> DeclarationSpine
ImportS
  Pragma Range
_ Pragma
_              -> DeclarationSpine
PragmaS
  Open ModuleInfo
_ ModuleName
_ ImportDirective
_              -> DeclarationSpine
OpenS
  FunDef DefInfo
_ QName
_ Delayed
_ [Clause]
cs         -> [ClauseSpine] -> DeclarationSpine
FunDefS ((Clause -> ClauseSpine) -> [Clause] -> [ClauseSpine]
forall a b. (a -> b) -> [a] -> [b]
map Clause -> ClauseSpine
clauseSpine [Clause]
cs)
  DataSig DefInfo
_ QName
_ GeneralizeTelescope
_ Expr
_         -> DeclarationSpine
DataSigS
  DataDef DefInfo
_ QName
_ UniverseCheck
_ DataDefParams
_ [Declaration]
_       -> DeclarationSpine
DataDefS
  RecSig DefInfo
_ QName
_ GeneralizeTelescope
_ Expr
_          -> DeclarationSpine
RecSigS
  RecDef DefInfo
_ QName
_ UniverseCheck
_ RecordDirectives
_ DataDefParams
_ Expr
_ [Declaration]
ds   -> [DeclarationSpine] -> DeclarationSpine
RecDefS ((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)

-- | The clause spine corresponding to a clause.

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

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

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

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

whereDeclarationsSpine :: WhereDeclarations -> WhereDeclarationsSpine
whereDeclarationsSpine :: WhereDeclarations -> WhereDeclarationsSpine
whereDeclarationsSpine (WhereDecls Maybe ModuleName
_ Bool
_ Maybe Declaration
md) =
  Maybe DeclarationSpine -> WhereDeclarationsSpine
WhereDeclsS ((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)