{-# LANGUAGE CPP #-}
{-# LANGUAGE ApplicativeDo #-}  -- see exprToPattern

{-| The concrete syntax is a raw representation of the program text
    without any desugaring at all.  This is what the parser produces.
    The idea is that if we figure out how to keep the concrete syntax
    around, it can be printed exactly as the user wrote it.
-}
module Agda.Syntax.Concrete
  ( -- * Expressions
    Expr(..)
  , OpApp(..), fromOrdinary
  , OpAppArgs, OpAppArgs'
  , module Agda.Syntax.Concrete.Name
  , AppView(..), appView, unAppView
  , rawApp, rawAppP
  , isSingleIdentifierP, removeParenP
  , isPattern, isAbsurdP, isBinderP
  , observeHiding
  , observeRelevance
  , observeModifiers
  , exprToPatternWithHoles
  , returnExpr
    -- * Bindings
  , Binder'(..)
  , Binder
  , mkBinder_
  , mkBinder
  , LamBinding
  , LamBinding'(..)
  , dropTypeAndModality
  , TypedBinding
  , TypedBinding'(..)
  , RecordAssignment
  , RecordAssignments
  , FieldAssignment, FieldAssignment'(..), nameFieldA, exprFieldA
  , ModuleAssignment(..)
  , BoundName(..), mkBoundName_, mkBoundName
  , TacticAttribute
  , TacticAttribute'(..)
  , Telescope, Telescope1
  , lamBindingsToTelescope
  , makePi
  , mkLam, mkLet, mkTLet
    -- * Declarations
  , Declaration(..)
  , isPragma
  , RecordDirective(..)
  , RecordDirectives
  , ModuleApplication(..)
  , TypeSignature
  , TypeSignatureOrInstanceBlock
  , ImportDirective, Using, ImportedName
  , Renaming, RenamingDirective, HidingDirective
  , AsName'(..), AsName
  , OpenShortHand(..), RewriteEqn, WithExpr
  , LHS(..), Pattern(..), LHSCore(..)
  , LamClause(..)
  , RHS, RHS'(..), WhereClause, WhereClause'(..), ExprWhere(..)
  , DoStmt(..)
  , Pragma(..)
  , Module(..)
  , ThingWithFixity(..)
  , HoleContent, HoleContent'(..)
  , spanAllowedBeforeModule
  , ungatherRecordDirectives
  )
  where

import Prelude hiding (null)

import Control.DeepSeq

import Data.Bifunctor   ( second )
import Data.DList       ( DList )
import qualified Data.DList as DL
import Data.Function    ( (&) )
import Data.Functor.Identity
import Data.Maybe
import Data.Set         ( Set  )
import Data.Text        ( Text )
-- import Data.Traversable ( forM )

import GHC.Generics     ( Generic )

import Agda.Syntax.Position
import Agda.Syntax.Common
import Agda.Syntax.Fixity
import Agda.Syntax.Literal

import Agda.Syntax.Concrete.Name
import qualified Agda.Syntax.Abstract.Name as A

import Agda.TypeChecking.Positivity.Occurrence

import Agda.Utils.Applicative ( forA )
import Agda.Utils.Either      ( maybeLeft )
import Agda.Utils.Lens
import Agda.Utils.List1       ( List1, pattern (:|) )
import qualified Agda.Utils.List1 as List1
import Agda.Utils.List2       ( List2, pattern List2 )
import Agda.Syntax.Common.Aspect (NameKind)
import Agda.Utils.Null
import Agda.Utils.Singleton

import Agda.Utils.Impossible

data OpApp e
  = SyntaxBindingLambda Range (List1 LamBinding) e
    -- ^ An abstraction inside a special syntax declaration
    --   (see Issue 358 why we introduce this).
  | Ordinary e
  deriving ((forall a b. (a -> b) -> OpApp a -> OpApp b)
-> (forall a b. a -> OpApp b -> OpApp a) -> Functor OpApp
forall a b. a -> OpApp b -> OpApp a
forall a b. (a -> b) -> OpApp a -> OpApp 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) -> OpApp a -> OpApp b
fmap :: forall a b. (a -> b) -> OpApp a -> OpApp b
$c<$ :: forall a b. a -> OpApp b -> OpApp a
<$ :: forall a b. a -> OpApp b -> OpApp a
Functor, (forall m. Monoid m => OpApp m -> m)
-> (forall m a. Monoid m => (a -> m) -> OpApp a -> m)
-> (forall m a. Monoid m => (a -> m) -> OpApp a -> m)
-> (forall a b. (a -> b -> b) -> b -> OpApp a -> b)
-> (forall a b. (a -> b -> b) -> b -> OpApp a -> b)
-> (forall b a. (b -> a -> b) -> b -> OpApp a -> b)
-> (forall b a. (b -> a -> b) -> b -> OpApp a -> b)
-> (forall a. (a -> a -> a) -> OpApp a -> a)
-> (forall a. (a -> a -> a) -> OpApp a -> a)
-> (forall a. OpApp a -> [a])
-> (forall a. OpApp a -> Bool)
-> (forall a. OpApp a -> Int)
-> (forall a. Eq a => a -> OpApp a -> Bool)
-> (forall a. Ord a => OpApp a -> a)
-> (forall a. Ord a => OpApp a -> a)
-> (forall a. Num a => OpApp a -> a)
-> (forall a. Num a => OpApp a -> a)
-> Foldable OpApp
forall a. Eq a => a -> OpApp a -> Bool
forall a. Num a => OpApp a -> a
forall a. Ord a => OpApp a -> a
forall m. Monoid m => OpApp m -> m
forall a. OpApp a -> Bool
forall a. OpApp a -> Int
forall a. OpApp a -> [a]
forall a. (a -> a -> a) -> OpApp a -> a
forall m a. Monoid m => (a -> m) -> OpApp a -> m
forall b a. (b -> a -> b) -> b -> OpApp a -> b
forall a b. (a -> b -> b) -> b -> OpApp 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 => OpApp m -> m
fold :: forall m. Monoid m => OpApp m -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> OpApp a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> OpApp a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> OpApp a -> m
foldMap' :: forall m a. Monoid m => (a -> m) -> OpApp a -> m
$cfoldr :: forall a b. (a -> b -> b) -> b -> OpApp a -> b
foldr :: forall a b. (a -> b -> b) -> b -> OpApp a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> OpApp a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> OpApp a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> OpApp a -> b
foldl :: forall b a. (b -> a -> b) -> b -> OpApp a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> OpApp a -> b
foldl' :: forall b a. (b -> a -> b) -> b -> OpApp a -> b
$cfoldr1 :: forall a. (a -> a -> a) -> OpApp a -> a
foldr1 :: forall a. (a -> a -> a) -> OpApp a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> OpApp a -> a
foldl1 :: forall a. (a -> a -> a) -> OpApp a -> a
$ctoList :: forall a. OpApp a -> [a]
toList :: forall a. OpApp a -> [a]
$cnull :: forall a. OpApp a -> Bool
null :: forall a. OpApp a -> Bool
$clength :: forall a. OpApp a -> Int
length :: forall a. OpApp a -> Int
$celem :: forall a. Eq a => a -> OpApp a -> Bool
elem :: forall a. Eq a => a -> OpApp a -> Bool
$cmaximum :: forall a. Ord a => OpApp a -> a
maximum :: forall a. Ord a => OpApp a -> a
$cminimum :: forall a. Ord a => OpApp a -> a
minimum :: forall a. Ord a => OpApp a -> a
$csum :: forall a. Num a => OpApp a -> a
sum :: forall a. Num a => OpApp a -> a
$cproduct :: forall a. Num a => OpApp a -> a
product :: forall a. Num a => OpApp a -> a
Foldable, Functor OpApp
Foldable OpApp
(Functor OpApp, Foldable OpApp) =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> OpApp a -> f (OpApp b))
-> (forall (f :: * -> *) a.
    Applicative f =>
    OpApp (f a) -> f (OpApp a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> OpApp a -> m (OpApp b))
-> (forall (m :: * -> *) a. Monad m => OpApp (m a) -> m (OpApp a))
-> Traversable OpApp
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 => OpApp (m a) -> m (OpApp a)
forall (f :: * -> *) a. Applicative f => OpApp (f a) -> f (OpApp a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> OpApp a -> m (OpApp b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> OpApp a -> f (OpApp b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> OpApp a -> f (OpApp b)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> OpApp a -> f (OpApp b)
$csequenceA :: forall (f :: * -> *) a. Applicative f => OpApp (f a) -> f (OpApp a)
sequenceA :: forall (f :: * -> *) a. Applicative f => OpApp (f a) -> f (OpApp a)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> OpApp a -> m (OpApp b)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> OpApp a -> m (OpApp b)
$csequence :: forall (m :: * -> *) a. Monad m => OpApp (m a) -> m (OpApp a)
sequence :: forall (m :: * -> *) a. Monad m => OpApp (m a) -> m (OpApp a)
Traversable, OpApp e -> OpApp e -> Bool
(OpApp e -> OpApp e -> Bool)
-> (OpApp e -> OpApp e -> Bool) -> Eq (OpApp e)
forall e. Eq e => OpApp e -> OpApp e -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall e. Eq e => OpApp e -> OpApp e -> Bool
== :: OpApp e -> OpApp e -> Bool
$c/= :: forall e. Eq e => OpApp e -> OpApp e -> Bool
/= :: OpApp e -> OpApp e -> Bool
Eq)

fromOrdinary :: e -> OpApp e -> e
fromOrdinary :: forall e. e -> OpApp e -> e
fromOrdinary e
d (Ordinary e
e) = e
e
fromOrdinary e
d OpApp e
_            = e
d

data FieldAssignment' a = FieldAssignment { forall a. FieldAssignment' a -> Name
_nameFieldA :: Name, forall a. FieldAssignment' a -> a
_exprFieldA :: a }
  deriving ((forall a b. (a -> b) -> FieldAssignment' a -> FieldAssignment' b)
-> (forall a b. a -> FieldAssignment' b -> FieldAssignment' a)
-> Functor FieldAssignment'
forall a b. a -> FieldAssignment' b -> FieldAssignment' a
forall a b. (a -> b) -> FieldAssignment' a -> FieldAssignment' 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) -> FieldAssignment' a -> FieldAssignment' b
fmap :: forall a b. (a -> b) -> FieldAssignment' a -> FieldAssignment' b
$c<$ :: forall a b. a -> FieldAssignment' b -> FieldAssignment' a
<$ :: forall a b. a -> FieldAssignment' b -> FieldAssignment' a
Functor, (forall m. Monoid m => FieldAssignment' m -> m)
-> (forall m a. Monoid m => (a -> m) -> FieldAssignment' a -> m)
-> (forall m a. Monoid m => (a -> m) -> FieldAssignment' a -> m)
-> (forall a b. (a -> b -> b) -> b -> FieldAssignment' a -> b)
-> (forall a b. (a -> b -> b) -> b -> FieldAssignment' a -> b)
-> (forall b a. (b -> a -> b) -> b -> FieldAssignment' a -> b)
-> (forall b a. (b -> a -> b) -> b -> FieldAssignment' a -> b)
-> (forall a. (a -> a -> a) -> FieldAssignment' a -> a)
-> (forall a. (a -> a -> a) -> FieldAssignment' a -> a)
-> (forall a. FieldAssignment' a -> [a])
-> (forall a. FieldAssignment' a -> Bool)
-> (forall a. FieldAssignment' a -> Int)
-> (forall a. Eq a => a -> FieldAssignment' a -> Bool)
-> (forall a. Ord a => FieldAssignment' a -> a)
-> (forall a. Ord a => FieldAssignment' a -> a)
-> (forall a. Num a => FieldAssignment' a -> a)
-> (forall a. Num a => FieldAssignment' a -> a)
-> Foldable FieldAssignment'
forall a. Eq a => a -> FieldAssignment' a -> Bool
forall a. Num a => FieldAssignment' a -> a
forall a. Ord a => FieldAssignment' a -> a
forall m. Monoid m => FieldAssignment' m -> m
forall a. FieldAssignment' a -> Bool
forall a. FieldAssignment' a -> Int
forall a. FieldAssignment' a -> [a]
forall a. (a -> a -> a) -> FieldAssignment' a -> a
forall m a. Monoid m => (a -> m) -> FieldAssignment' a -> m
forall b a. (b -> a -> b) -> b -> FieldAssignment' a -> b
forall a b. (a -> b -> b) -> b -> FieldAssignment' 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 => FieldAssignment' m -> m
fold :: forall m. Monoid m => FieldAssignment' m -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> FieldAssignment' a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> FieldAssignment' a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> FieldAssignment' a -> m
foldMap' :: forall m a. Monoid m => (a -> m) -> FieldAssignment' a -> m
$cfoldr :: forall a b. (a -> b -> b) -> b -> FieldAssignment' a -> b
foldr :: forall a b. (a -> b -> b) -> b -> FieldAssignment' a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> FieldAssignment' a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> FieldAssignment' a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> FieldAssignment' a -> b
foldl :: forall b a. (b -> a -> b) -> b -> FieldAssignment' a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> FieldAssignment' a -> b
foldl' :: forall b a. (b -> a -> b) -> b -> FieldAssignment' a -> b
$cfoldr1 :: forall a. (a -> a -> a) -> FieldAssignment' a -> a
foldr1 :: forall a. (a -> a -> a) -> FieldAssignment' a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> FieldAssignment' a -> a
foldl1 :: forall a. (a -> a -> a) -> FieldAssignment' a -> a
$ctoList :: forall a. FieldAssignment' a -> [a]
toList :: forall a. FieldAssignment' a -> [a]
$cnull :: forall a. FieldAssignment' a -> Bool
null :: forall a. FieldAssignment' a -> Bool
$clength :: forall a. FieldAssignment' a -> Int
length :: forall a. FieldAssignment' a -> Int
$celem :: forall a. Eq a => a -> FieldAssignment' a -> Bool
elem :: forall a. Eq a => a -> FieldAssignment' a -> Bool
$cmaximum :: forall a. Ord a => FieldAssignment' a -> a
maximum :: forall a. Ord a => FieldAssignment' a -> a
$cminimum :: forall a. Ord a => FieldAssignment' a -> a
minimum :: forall a. Ord a => FieldAssignment' a -> a
$csum :: forall a. Num a => FieldAssignment' a -> a
sum :: forall a. Num a => FieldAssignment' a -> a
$cproduct :: forall a. Num a => FieldAssignment' a -> a
product :: forall a. Num a => FieldAssignment' a -> a
Foldable, Functor FieldAssignment'
Foldable FieldAssignment'
(Functor FieldAssignment', Foldable FieldAssignment') =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> FieldAssignment' a -> f (FieldAssignment' b))
-> (forall (f :: * -> *) a.
    Applicative f =>
    FieldAssignment' (f a) -> f (FieldAssignment' a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> FieldAssignment' a -> m (FieldAssignment' b))
-> (forall (m :: * -> *) a.
    Monad m =>
    FieldAssignment' (m a) -> m (FieldAssignment' a))
-> Traversable FieldAssignment'
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 =>
FieldAssignment' (m a) -> m (FieldAssignment' a)
forall (f :: * -> *) a.
Applicative f =>
FieldAssignment' (f a) -> f (FieldAssignment' a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> FieldAssignment' a -> m (FieldAssignment' b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> FieldAssignment' a -> f (FieldAssignment' b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> FieldAssignment' a -> f (FieldAssignment' b)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> FieldAssignment' a -> f (FieldAssignment' b)
$csequenceA :: forall (f :: * -> *) a.
Applicative f =>
FieldAssignment' (f a) -> f (FieldAssignment' a)
sequenceA :: forall (f :: * -> *) a.
Applicative f =>
FieldAssignment' (f a) -> f (FieldAssignment' a)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> FieldAssignment' a -> m (FieldAssignment' b)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> FieldAssignment' a -> m (FieldAssignment' b)
$csequence :: forall (m :: * -> *) a.
Monad m =>
FieldAssignment' (m a) -> m (FieldAssignment' a)
sequence :: forall (m :: * -> *) a.
Monad m =>
FieldAssignment' (m a) -> m (FieldAssignment' a)
Traversable, Int -> FieldAssignment' a -> ShowS
[FieldAssignment' a] -> ShowS
FieldAssignment' a -> String
(Int -> FieldAssignment' a -> ShowS)
-> (FieldAssignment' a -> String)
-> ([FieldAssignment' a] -> ShowS)
-> Show (FieldAssignment' a)
forall a. Show a => Int -> FieldAssignment' a -> ShowS
forall a. Show a => [FieldAssignment' a] -> ShowS
forall a. Show a => FieldAssignment' a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Show a => Int -> FieldAssignment' a -> ShowS
showsPrec :: Int -> FieldAssignment' a -> ShowS
$cshow :: forall a. Show a => FieldAssignment' a -> String
show :: FieldAssignment' a -> String
$cshowList :: forall a. Show a => [FieldAssignment' a] -> ShowS
showList :: [FieldAssignment' a] -> ShowS
Show, FieldAssignment' a -> FieldAssignment' a -> Bool
(FieldAssignment' a -> FieldAssignment' a -> Bool)
-> (FieldAssignment' a -> FieldAssignment' a -> Bool)
-> Eq (FieldAssignment' a)
forall a. Eq a => FieldAssignment' a -> FieldAssignment' a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall a. Eq a => FieldAssignment' a -> FieldAssignment' a -> Bool
== :: FieldAssignment' a -> FieldAssignment' a -> Bool
$c/= :: forall a. Eq a => FieldAssignment' a -> FieldAssignment' a -> Bool
/= :: FieldAssignment' a -> FieldAssignment' a -> Bool
Eq)

type FieldAssignment = FieldAssignment' Expr

data ModuleAssignment  = ModuleAssignment
                           { ModuleAssignment -> QName
_qnameModA     :: QName
                           , ModuleAssignment -> [Expr]
_exprModA      :: [Expr]
                           , ModuleAssignment -> ImportDirective
_importDirModA :: ImportDirective
                           }
  deriving ModuleAssignment -> ModuleAssignment -> Bool
(ModuleAssignment -> ModuleAssignment -> Bool)
-> (ModuleAssignment -> ModuleAssignment -> Bool)
-> Eq ModuleAssignment
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: ModuleAssignment -> ModuleAssignment -> Bool
== :: ModuleAssignment -> ModuleAssignment -> Bool
$c/= :: ModuleAssignment -> ModuleAssignment -> Bool
/= :: ModuleAssignment -> ModuleAssignment -> Bool
Eq

type RecordAssignment  = Either FieldAssignment ModuleAssignment
type RecordAssignments = [RecordAssignment]

nameFieldA :: Lens' (FieldAssignment' a) Name
nameFieldA :: forall a (f :: * -> *).
Functor f =>
(Name -> f Name) -> FieldAssignment' a -> f (FieldAssignment' a)
nameFieldA Name -> f Name
f FieldAssignment' a
r = Name -> f Name
f (FieldAssignment' a -> Name
forall a. FieldAssignment' a -> Name
_nameFieldA FieldAssignment' a
r) f Name -> (Name -> FieldAssignment' a) -> f (FieldAssignment' a)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \Name
x -> FieldAssignment' a
r { _nameFieldA = x }

exprFieldA :: Lens' (FieldAssignment' a) a
exprFieldA :: forall a (f :: * -> *).
Functor f =>
(a -> f a) -> FieldAssignment' a -> f (FieldAssignment' a)
exprFieldA a -> f a
f FieldAssignment' a
r = a -> f a
f (FieldAssignment' a -> a
forall a. FieldAssignment' a -> a
_exprFieldA FieldAssignment' a
r) f a -> (a -> FieldAssignment' a) -> f (FieldAssignment' a)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \a
x -> FieldAssignment' a
r { _exprFieldA = x }

-- UNUSED Liang-Ting Chen 2019-07-16
--qnameModA :: Lens' ModuleAssignment QName
--qnameModA f r = f (_qnameModA r) <&> \x -> r { _qnameModA = x }
--
--exprModA :: Lens' [Expr] ModuleAssignment
--exprModA f r = f (_exprModA r) <&> \x -> r { _exprModA = x }
--
--importDirModA :: Lens' ModuleAssignment ImportDirective
--importDirModA f r = f (_importDirModA r) <&> \x -> r { _importDirModA = x }

-- | Concrete expressions. Should represent exactly what the user wrote.
data Expr
  = Ident QName                                -- ^ ex: @x@
  | Lit Range Literal                          -- ^ ex: @1@ or @\"foo\"@
  | QuestionMark Range (Maybe Nat)             -- ^ ex: @?@ or @{! ... !}@
  | Underscore Range (Maybe String)            -- ^ ex: @_@ or @_A_5@
  | RawApp Range (List2 Expr)                  -- ^ before parsing operators
  | App Range Expr (NamedArg Expr)             -- ^ ex: @e e@, @e {e}@, or @e {x = e}@
  | OpApp Range QName (Set A.Name) OpAppArgs   -- ^ ex: @e + e@
                                               -- The 'QName' is possibly ambiguous,
                                               -- but it must correspond to one of the names in the set.
  | WithApp Range Expr [Expr]                  -- ^ ex: @e | e1 | .. | en@
  | HiddenArg Range (Named_ Expr)              -- ^ ex: @{e}@ or @{x=e}@
  | InstanceArg Range (Named_ Expr)            -- ^ ex: @{{e}}@ or @{{x=e}}@
  | Lam Range (List1 LamBinding) Expr          -- ^ ex: @\\x {y} -> e@ or @\\(x:A){y:B} -> e@
  | AbsurdLam Range Hiding                     -- ^ ex: @\\ ()@
  | ExtendedLam Range Erased
      (List1 LamClause)                        -- ^ ex: @\\ { p11 .. p1a -> e1 ; .. ; pn1 .. pnz -> en }@
  | Fun Range (Arg Expr) Expr                  -- ^ ex: @e -> e@ or @.e -> e@ (NYI: @{e} -> e@)
  | Pi Telescope1 Expr                         -- ^ ex: @(xs:e) -> e@ or @{xs:e} -> e@
  | Rec Range RecordAssignments                -- ^ ex: @record {x = a; y = b}@, or @record { x = a; M1; M2 }@
  | RecUpdate Range Expr [FieldAssignment]     -- ^ ex: @record e {x = a; y = b}@
  | Let Range (List1 Declaration) (Maybe Expr) -- ^ ex: @let Ds in e@, missing body when parsing do-notation let
  | Paren Range Expr                           -- ^ ex: @(e)@
  | IdiomBrackets Range [Expr]                 -- ^ ex: @(| e1 | e2 | .. | en |)@ or @(|)@
  | DoBlock Range (List1 DoStmt)               -- ^ ex: @do x <- m1; m2@
  | Absurd Range                               -- ^ ex: @()@ or @{}@, only in patterns
  | As Range Name Expr                         -- ^ ex: @x\@p@, only in patterns
  | Dot Range Expr                             -- ^ ex: @.p@, only in patterns
  | DoubleDot Range Expr                       -- ^ ex: @..A@, used for parsing @..A -> B@
  | Quote Range                                -- ^ ex: @quote@, should be applied to a name
  | QuoteTerm Range                            -- ^ ex: @quoteTerm@, should be applied to a term
  | Tactic Range Expr                          -- ^ ex: @\@(tactic t)@, used to declare tactic arguments
  | Unquote Range                              -- ^ ex: @unquote@, should be applied to a term of type @Term@
  | DontCare Expr                              -- ^ to print irrelevant things
  | Equal Range Expr Expr                      -- ^ ex: @a = b@, used internally in the parser
  | Ellipsis Range                             -- ^ @...@, used internally to parse patterns.
  | KnownIdent NameKind QName
    -- ^ An identifier coming from abstract syntax, for which we know a
    -- precise syntactic highlighting class (used in printing).
  | KnownOpApp NameKind Range QName (Set A.Name) OpAppArgs
    -- ^ An operator application coming from abstract syntax, for which
    -- we know a precise syntactic highlighting class (used in
    -- printing).
  | Generalized Expr
  deriving Expr -> Expr -> Bool
(Expr -> Expr -> Bool) -> (Expr -> Expr -> Bool) -> Eq Expr
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Expr -> Expr -> Bool
== :: Expr -> Expr -> Bool
$c/= :: Expr -> Expr -> Bool
/= :: Expr -> Expr -> Bool
Eq

type OpAppArgs = OpAppArgs' Expr
type OpAppArgs' e = [NamedArg (MaybePlaceholder (OpApp e))]

-- | Concrete patterns. No literals in patterns at the moment.
data Pattern
  = IdentP Bool QName                      -- ^ @c@ or @x@
                                           --
                                           -- If the boolean is
                                           -- 'False', then the
                                           -- 'QName' must not refer
                                           -- to a constructor or a
                                           -- pattern synonym. The
                                           -- value 'False' is used
                                           -- when a hidden argument
                                           -- pun is expanded.
  | QuoteP Range                           -- ^ @quote@
  | AppP Pattern (NamedArg Pattern)        -- ^ @p p'@ or @p {x = p'}@
  | RawAppP Range (List2 Pattern)          -- ^ @p1..pn@ before parsing operators
  | OpAppP Range QName (Set A.Name)
           [NamedArg Pattern]              -- ^ eg: @p => p'@ for operator @_=>_@
                                           -- The 'QName' is possibly
                                           -- ambiguous, but it must
                                           -- correspond to one of
                                           -- the names in the set.
  | HiddenP Range (Named_ Pattern)         -- ^ @{p}@ or @{x = p}@
  | InstanceP Range (Named_ Pattern)       -- ^ @{{p}}@ or @{{x = p}}@
  | ParenP Range Pattern                   -- ^ @(p)@
  | WildP Range                            -- ^ @_@
  | AbsurdP Range                          -- ^ @()@
  | AsP Range Name Pattern                 -- ^ @x\@p@ unused
  | DotP Range Expr                        -- ^ @.e@
  | LitP Range Literal                     -- ^ @0@, @1@, etc.
  | RecP Range [FieldAssignment' Pattern]  -- ^ @record {x = p; y = q}@
  | EqualP Range [(Expr,Expr)]             -- ^ @i = i1@ i.e. cubical face lattice generator
  | EllipsisP Range (Maybe Pattern)        -- ^ @...@, only as left-most pattern.
                                           --   Second arg is @Nothing@ before expansion, and
                                           --   @Just p@ after expanding ellipsis to @p@.
  | WithP Range Pattern                    -- ^ @| p@, for with-patterns.
  deriving Pattern -> Pattern -> Bool
(Pattern -> Pattern -> Bool)
-> (Pattern -> Pattern -> Bool) -> Eq Pattern
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Pattern -> Pattern -> Bool
== :: Pattern -> Pattern -> Bool
$c/= :: Pattern -> Pattern -> Bool
/= :: Pattern -> Pattern -> Bool
Eq

data DoStmt
  = DoBind Range Pattern Expr [LamClause]   -- ^ @p ← e where cs@
  | DoThen Expr
  | DoLet Range (List1 Declaration)
  deriving DoStmt -> DoStmt -> Bool
(DoStmt -> DoStmt -> Bool)
-> (DoStmt -> DoStmt -> Bool) -> Eq DoStmt
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: DoStmt -> DoStmt -> Bool
== :: DoStmt -> DoStmt -> Bool
$c/= :: DoStmt -> DoStmt -> Bool
/= :: DoStmt -> DoStmt -> Bool
Eq

-- | 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 (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)

type Binder = Binder' BoundName

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

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

-- | A lambda binding is either domain free or typed.

type LamBinding = LamBinding' TypedBinding
data LamBinding' a
  = DomainFree (NamedArg Binder)
    -- ^ . @x@ or @{x}@ or @.x@ or @.{x}@ or @{.x}@ or @x\@p@ or @(p)@
  | DomainFull a
    -- ^ . @(xs : e)@ or @{xs : e}@
  deriving ((forall a b. (a -> b) -> LamBinding' a -> LamBinding' b)
-> (forall a b. a -> LamBinding' b -> LamBinding' a)
-> Functor LamBinding'
forall a b. a -> LamBinding' b -> LamBinding' a
forall a b. (a -> b) -> LamBinding' a -> LamBinding' 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) -> LamBinding' a -> LamBinding' b
fmap :: forall a b. (a -> b) -> LamBinding' a -> LamBinding' b
$c<$ :: forall a b. a -> LamBinding' b -> LamBinding' a
<$ :: forall a b. a -> LamBinding' b -> LamBinding' a
Functor, (forall m. Monoid m => LamBinding' m -> m)
-> (forall m a. Monoid m => (a -> m) -> LamBinding' a -> m)
-> (forall m a. Monoid m => (a -> m) -> LamBinding' a -> m)
-> (forall a b. (a -> b -> b) -> b -> LamBinding' a -> b)
-> (forall a b. (a -> b -> b) -> b -> LamBinding' a -> b)
-> (forall b a. (b -> a -> b) -> b -> LamBinding' a -> b)
-> (forall b a. (b -> a -> b) -> b -> LamBinding' a -> b)
-> (forall a. (a -> a -> a) -> LamBinding' a -> a)
-> (forall a. (a -> a -> a) -> LamBinding' a -> a)
-> (forall a. LamBinding' a -> [a])
-> (forall a. LamBinding' a -> Bool)
-> (forall a. LamBinding' a -> Int)
-> (forall a. Eq a => a -> LamBinding' a -> Bool)
-> (forall a. Ord a => LamBinding' a -> a)
-> (forall a. Ord a => LamBinding' a -> a)
-> (forall a. Num a => LamBinding' a -> a)
-> (forall a. Num a => LamBinding' a -> a)
-> Foldable LamBinding'
forall a. Eq a => a -> LamBinding' a -> Bool
forall a. Num a => LamBinding' a -> a
forall a. Ord a => LamBinding' a -> a
forall m. Monoid m => LamBinding' m -> m
forall a. LamBinding' a -> Bool
forall a. LamBinding' a -> Int
forall a. LamBinding' a -> [a]
forall a. (a -> a -> a) -> LamBinding' a -> a
forall m a. Monoid m => (a -> m) -> LamBinding' a -> m
forall b a. (b -> a -> b) -> b -> LamBinding' a -> b
forall a b. (a -> b -> b) -> b -> LamBinding' 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 => LamBinding' m -> m
fold :: forall m. Monoid m => LamBinding' m -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> LamBinding' a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> LamBinding' a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> LamBinding' a -> m
foldMap' :: forall m a. Monoid m => (a -> m) -> LamBinding' a -> m
$cfoldr :: forall a b. (a -> b -> b) -> b -> LamBinding' a -> b
foldr :: forall a b. (a -> b -> b) -> b -> LamBinding' a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> LamBinding' a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> LamBinding' a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> LamBinding' a -> b
foldl :: forall b a. (b -> a -> b) -> b -> LamBinding' a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> LamBinding' a -> b
foldl' :: forall b a. (b -> a -> b) -> b -> LamBinding' a -> b
$cfoldr1 :: forall a. (a -> a -> a) -> LamBinding' a -> a
foldr1 :: forall a. (a -> a -> a) -> LamBinding' a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> LamBinding' a -> a
foldl1 :: forall a. (a -> a -> a) -> LamBinding' a -> a
$ctoList :: forall a. LamBinding' a -> [a]
toList :: forall a. LamBinding' a -> [a]
$cnull :: forall a. LamBinding' a -> Bool
null :: forall a. LamBinding' a -> Bool
$clength :: forall a. LamBinding' a -> Int
length :: forall a. LamBinding' a -> Int
$celem :: forall a. Eq a => a -> LamBinding' a -> Bool
elem :: forall a. Eq a => a -> LamBinding' a -> Bool
$cmaximum :: forall a. Ord a => LamBinding' a -> a
maximum :: forall a. Ord a => LamBinding' a -> a
$cminimum :: forall a. Ord a => LamBinding' a -> a
minimum :: forall a. Ord a => LamBinding' a -> a
$csum :: forall a. Num a => LamBinding' a -> a
sum :: forall a. Num a => LamBinding' a -> a
$cproduct :: forall a. Num a => LamBinding' a -> a
product :: forall a. Num a => LamBinding' a -> a
Foldable, Functor LamBinding'
Foldable LamBinding'
(Functor LamBinding', Foldable LamBinding') =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> LamBinding' a -> f (LamBinding' b))
-> (forall (f :: * -> *) a.
    Applicative f =>
    LamBinding' (f a) -> f (LamBinding' a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> LamBinding' a -> m (LamBinding' b))
-> (forall (m :: * -> *) a.
    Monad m =>
    LamBinding' (m a) -> m (LamBinding' a))
-> Traversable LamBinding'
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 =>
LamBinding' (m a) -> m (LamBinding' a)
forall (f :: * -> *) a.
Applicative f =>
LamBinding' (f a) -> f (LamBinding' a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> LamBinding' a -> m (LamBinding' b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> LamBinding' a -> f (LamBinding' b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> LamBinding' a -> f (LamBinding' b)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> LamBinding' a -> f (LamBinding' b)
$csequenceA :: forall (f :: * -> *) a.
Applicative f =>
LamBinding' (f a) -> f (LamBinding' a)
sequenceA :: forall (f :: * -> *) a.
Applicative f =>
LamBinding' (f a) -> f (LamBinding' a)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> LamBinding' a -> m (LamBinding' b)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> LamBinding' a -> m (LamBinding' b)
$csequence :: forall (m :: * -> *) a.
Monad m =>
LamBinding' (m a) -> m (LamBinding' a)
sequence :: forall (m :: * -> *) a.
Monad m =>
LamBinding' (m a) -> m (LamBinding' a)
Traversable, LamBinding' a -> LamBinding' a -> Bool
(LamBinding' a -> LamBinding' a -> Bool)
-> (LamBinding' a -> LamBinding' a -> Bool) -> Eq (LamBinding' a)
forall a. Eq a => LamBinding' a -> LamBinding' a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall a. Eq a => LamBinding' a -> LamBinding' a -> Bool
== :: LamBinding' a -> LamBinding' a -> Bool
$c/= :: forall a. Eq a => LamBinding' a -> LamBinding' a -> Bool
/= :: LamBinding' a -> LamBinding' a -> Bool
Eq)

-- | Drop type annotations and lets from bindings.
dropTypeAndModality :: LamBinding -> [LamBinding]
dropTypeAndModality :: LamBinding -> [LamBinding]
dropTypeAndModality (DomainFull (TBind Range
_ List1 (NamedArg Binder)
xs Expr
_)) =
  (NamedArg Binder -> LamBinding)
-> [NamedArg Binder] -> [LamBinding]
forall a b. (a -> b) -> [a] -> [b]
map (NamedArg Binder -> LamBinding
forall a. NamedArg Binder -> LamBinding' a
DomainFree (NamedArg Binder -> LamBinding)
-> (NamedArg Binder -> NamedArg Binder)
-> NamedArg Binder
-> LamBinding
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Modality -> NamedArg Binder -> NamedArg Binder
forall a. LensModality a => Modality -> a -> a
setModality Modality
defaultModality) ([NamedArg Binder] -> [LamBinding])
-> [NamedArg Binder] -> [LamBinding]
forall a b. (a -> b) -> a -> b
$ List1 (NamedArg Binder) -> [Item (List1 (NamedArg Binder))]
forall l. IsList l => l -> [Item l]
List1.toList List1 (NamedArg Binder)
xs
dropTypeAndModality (DomainFull TLet{}) = []
dropTypeAndModality (DomainFree NamedArg Binder
x) = [NamedArg Binder -> LamBinding
forall a. NamedArg Binder -> LamBinding' a
DomainFree (NamedArg Binder -> LamBinding) -> NamedArg Binder -> LamBinding
forall a b. (a -> b) -> a -> b
$ Modality -> NamedArg Binder -> NamedArg Binder
forall a. LensModality a => Modality -> a -> a
setModality Modality
defaultModality NamedArg Binder
x]

data BoundName = BName
  { BoundName -> Name
boundName       :: Name
  , BoundName -> Fixity'
bnameFixity     :: Fixity'
  , BoundName -> TacticAttribute
bnameTactic     :: TacticAttribute
      -- ^ From @\@tactic@ attribute.
  , BoundName -> Bool
bnameIsFinite   :: Bool
      -- ^ The @\@finite@ cannot be parsed, it comes from the builtin @Partial@ only.
  }
  deriving BoundName -> BoundName -> Bool
(BoundName -> BoundName -> Bool)
-> (BoundName -> BoundName -> Bool) -> Eq BoundName
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: BoundName -> BoundName -> Bool
== :: BoundName -> BoundName -> Bool
$c/= :: BoundName -> BoundName -> Bool
/= :: BoundName -> BoundName -> Bool
Eq

newtype TacticAttribute' a = TacticAttribute { forall a. TacticAttribute' a -> Maybe (Ranged a)
theTacticAttribute :: Maybe (Ranged a) }
  deriving (TacticAttribute' a -> TacticAttribute' a -> Bool
(TacticAttribute' a -> TacticAttribute' a -> Bool)
-> (TacticAttribute' a -> TacticAttribute' a -> Bool)
-> Eq (TacticAttribute' a)
forall a. Eq a => TacticAttribute' a -> TacticAttribute' a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall a. Eq a => TacticAttribute' a -> TacticAttribute' a -> Bool
== :: TacticAttribute' a -> TacticAttribute' a -> Bool
$c/= :: forall a. Eq a => TacticAttribute' a -> TacticAttribute' a -> Bool
/= :: TacticAttribute' a -> TacticAttribute' a -> Bool
Eq, Int -> TacticAttribute' a -> ShowS
[TacticAttribute' a] -> ShowS
TacticAttribute' a -> String
(Int -> TacticAttribute' a -> ShowS)
-> (TacticAttribute' a -> String)
-> ([TacticAttribute' a] -> ShowS)
-> Show (TacticAttribute' a)
forall a. Show a => Int -> TacticAttribute' a -> ShowS
forall a. Show a => [TacticAttribute' a] -> ShowS
forall a. Show a => TacticAttribute' a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Show a => Int -> TacticAttribute' a -> ShowS
showsPrec :: Int -> TacticAttribute' a -> ShowS
$cshow :: forall a. Show a => TacticAttribute' a -> String
show :: TacticAttribute' a -> String
$cshowList :: forall a. Show a => [TacticAttribute' a] -> ShowS
showList :: [TacticAttribute' a] -> ShowS
Show, TacticAttribute' a -> ()
(TacticAttribute' a -> ()) -> NFData (TacticAttribute' a)
forall a. NFData a => TacticAttribute' a -> ()
forall a. (a -> ()) -> NFData a
$crnf :: forall a. NFData a => TacticAttribute' a -> ()
rnf :: TacticAttribute' a -> ()
NFData, (forall a b. (a -> b) -> TacticAttribute' a -> TacticAttribute' b)
-> (forall a b. a -> TacticAttribute' b -> TacticAttribute' a)
-> Functor TacticAttribute'
forall a b. a -> TacticAttribute' b -> TacticAttribute' a
forall a b. (a -> b) -> TacticAttribute' a -> TacticAttribute' 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) -> TacticAttribute' a -> TacticAttribute' b
fmap :: forall a b. (a -> b) -> TacticAttribute' a -> TacticAttribute' b
$c<$ :: forall a b. a -> TacticAttribute' b -> TacticAttribute' a
<$ :: forall a b. a -> TacticAttribute' b -> TacticAttribute' a
Functor, (forall m. Monoid m => TacticAttribute' m -> m)
-> (forall m a. Monoid m => (a -> m) -> TacticAttribute' a -> m)
-> (forall m a. Monoid m => (a -> m) -> TacticAttribute' a -> m)
-> (forall a b. (a -> b -> b) -> b -> TacticAttribute' a -> b)
-> (forall a b. (a -> b -> b) -> b -> TacticAttribute' a -> b)
-> (forall b a. (b -> a -> b) -> b -> TacticAttribute' a -> b)
-> (forall b a. (b -> a -> b) -> b -> TacticAttribute' a -> b)
-> (forall a. (a -> a -> a) -> TacticAttribute' a -> a)
-> (forall a. (a -> a -> a) -> TacticAttribute' a -> a)
-> (forall a. TacticAttribute' a -> [a])
-> (forall a. TacticAttribute' a -> Bool)
-> (forall a. TacticAttribute' a -> Int)
-> (forall a. Eq a => a -> TacticAttribute' a -> Bool)
-> (forall a. Ord a => TacticAttribute' a -> a)
-> (forall a. Ord a => TacticAttribute' a -> a)
-> (forall a. Num a => TacticAttribute' a -> a)
-> (forall a. Num a => TacticAttribute' a -> a)
-> Foldable TacticAttribute'
forall a. Eq a => a -> TacticAttribute' a -> Bool
forall a. Num a => TacticAttribute' a -> a
forall a. Ord a => TacticAttribute' a -> a
forall m. Monoid m => TacticAttribute' m -> m
forall a. TacticAttribute' a -> Bool
forall a. TacticAttribute' a -> Int
forall a. TacticAttribute' a -> [a]
forall a. (a -> a -> a) -> TacticAttribute' a -> a
forall m a. Monoid m => (a -> m) -> TacticAttribute' a -> m
forall b a. (b -> a -> b) -> b -> TacticAttribute' a -> b
forall a b. (a -> b -> b) -> b -> TacticAttribute' 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 => TacticAttribute' m -> m
fold :: forall m. Monoid m => TacticAttribute' m -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> TacticAttribute' a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> TacticAttribute' a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> TacticAttribute' a -> m
foldMap' :: forall m a. Monoid m => (a -> m) -> TacticAttribute' a -> m
$cfoldr :: forall a b. (a -> b -> b) -> b -> TacticAttribute' a -> b
foldr :: forall a b. (a -> b -> b) -> b -> TacticAttribute' a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> TacticAttribute' a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> TacticAttribute' a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> TacticAttribute' a -> b
foldl :: forall b a. (b -> a -> b) -> b -> TacticAttribute' a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> TacticAttribute' a -> b
foldl' :: forall b a. (b -> a -> b) -> b -> TacticAttribute' a -> b
$cfoldr1 :: forall a. (a -> a -> a) -> TacticAttribute' a -> a
foldr1 :: forall a. (a -> a -> a) -> TacticAttribute' a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> TacticAttribute' a -> a
foldl1 :: forall a. (a -> a -> a) -> TacticAttribute' a -> a
$ctoList :: forall a. TacticAttribute' a -> [a]
toList :: forall a. TacticAttribute' a -> [a]
$cnull :: forall a. TacticAttribute' a -> Bool
null :: forall a. TacticAttribute' a -> Bool
$clength :: forall a. TacticAttribute' a -> Int
length :: forall a. TacticAttribute' a -> Int
$celem :: forall a. Eq a => a -> TacticAttribute' a -> Bool
elem :: forall a. Eq a => a -> TacticAttribute' a -> Bool
$cmaximum :: forall a. Ord a => TacticAttribute' a -> a
maximum :: forall a. Ord a => TacticAttribute' a -> a
$cminimum :: forall a. Ord a => TacticAttribute' a -> a
minimum :: forall a. Ord a => TacticAttribute' a -> a
$csum :: forall a. Num a => TacticAttribute' a -> a
sum :: forall a. Num a => TacticAttribute' a -> a
$cproduct :: forall a. Num a => TacticAttribute' a -> a
product :: forall a. Num a => TacticAttribute' a -> a
Foldable, Functor TacticAttribute'
Foldable TacticAttribute'
(Functor TacticAttribute', Foldable TacticAttribute') =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> TacticAttribute' a -> f (TacticAttribute' b))
-> (forall (f :: * -> *) a.
    Applicative f =>
    TacticAttribute' (f a) -> f (TacticAttribute' a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> TacticAttribute' a -> m (TacticAttribute' b))
-> (forall (m :: * -> *) a.
    Monad m =>
    TacticAttribute' (m a) -> m (TacticAttribute' a))
-> Traversable TacticAttribute'
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 =>
TacticAttribute' (m a) -> m (TacticAttribute' a)
forall (f :: * -> *) a.
Applicative f =>
TacticAttribute' (f a) -> f (TacticAttribute' a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> TacticAttribute' a -> m (TacticAttribute' b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> TacticAttribute' a -> f (TacticAttribute' b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> TacticAttribute' a -> f (TacticAttribute' b)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> TacticAttribute' a -> f (TacticAttribute' b)
$csequenceA :: forall (f :: * -> *) a.
Applicative f =>
TacticAttribute' (f a) -> f (TacticAttribute' a)
sequenceA :: forall (f :: * -> *) a.
Applicative f =>
TacticAttribute' (f a) -> f (TacticAttribute' a)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> TacticAttribute' a -> m (TacticAttribute' b)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> TacticAttribute' a -> m (TacticAttribute' b)
$csequence :: forall (m :: * -> *) a.
Monad m =>
TacticAttribute' (m a) -> m (TacticAttribute' a)
sequence :: forall (m :: * -> *) a.
Monad m =>
TacticAttribute' (m a) -> m (TacticAttribute' a)
Traversable, KillRangeT (TacticAttribute' a)
KillRangeT (TacticAttribute' a) -> KillRange (TacticAttribute' a)
forall a. KillRangeT (TacticAttribute' a)
forall a. KillRangeT a -> KillRange a
$ckillRange :: forall a. KillRangeT (TacticAttribute' a)
killRange :: KillRangeT (TacticAttribute' a)
KillRange)
type TacticAttribute = TacticAttribute' Expr

instance Null (TacticAttribute' a) where
  null :: TacticAttribute' a -> Bool
null = Maybe (Ranged a) -> Bool
forall a. Maybe a -> Bool
isNothing (Maybe (Ranged a) -> Bool)
-> (TacticAttribute' a -> Maybe (Ranged a))
-> TacticAttribute' a
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TacticAttribute' a -> Maybe (Ranged a)
forall a. TacticAttribute' a -> Maybe (Ranged a)
theTacticAttribute
  empty :: TacticAttribute' a
empty = Maybe (Ranged a) -> TacticAttribute' a
forall a. Maybe (Ranged a) -> TacticAttribute' a
TacticAttribute Maybe (Ranged a)
forall a. Maybe a
Nothing

mkBoundName_ :: Name -> BoundName
mkBoundName_ :: Name -> BoundName
mkBoundName_ Name
x = Name -> Fixity' -> BoundName
mkBoundName Name
x Fixity'
noFixity'

mkBoundName :: Name -> Fixity' -> BoundName
mkBoundName :: Name -> Fixity' -> BoundName
mkBoundName Name
x Fixity'
f = Name -> Fixity' -> TacticAttribute -> Bool -> BoundName
BName Name
x Fixity'
f TacticAttribute
forall a. Null a => a
empty Bool
False

-- | A typed binding.

type TypedBinding = TypedBinding' Expr

data TypedBinding' e
  = TBind Range (List1 (NamedArg Binder)) e
    -- ^ Binding @(x1\@p1 ... xn\@pn : A)@.
  | TLet  Range (List1 Declaration)
    -- ^ Let binding @(let Ds)@ or @(open M args)@.
  deriving ((forall a b. (a -> b) -> TypedBinding' a -> TypedBinding' b)
-> (forall a b. a -> TypedBinding' b -> TypedBinding' a)
-> Functor TypedBinding'
forall a b. a -> TypedBinding' b -> TypedBinding' a
forall a b. (a -> b) -> TypedBinding' a -> TypedBinding' 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) -> TypedBinding' a -> TypedBinding' b
fmap :: forall a b. (a -> b) -> TypedBinding' a -> TypedBinding' b
$c<$ :: forall a b. a -> TypedBinding' b -> TypedBinding' a
<$ :: forall a b. a -> TypedBinding' b -> TypedBinding' a
Functor, (forall m. Monoid m => TypedBinding' m -> m)
-> (forall m a. Monoid m => (a -> m) -> TypedBinding' a -> m)
-> (forall m a. Monoid m => (a -> m) -> TypedBinding' a -> m)
-> (forall a b. (a -> b -> b) -> b -> TypedBinding' a -> b)
-> (forall a b. (a -> b -> b) -> b -> TypedBinding' a -> b)
-> (forall b a. (b -> a -> b) -> b -> TypedBinding' a -> b)
-> (forall b a. (b -> a -> b) -> b -> TypedBinding' a -> b)
-> (forall a. (a -> a -> a) -> TypedBinding' a -> a)
-> (forall a. (a -> a -> a) -> TypedBinding' a -> a)
-> (forall a. TypedBinding' a -> [a])
-> (forall a. TypedBinding' a -> Bool)
-> (forall a. TypedBinding' a -> Int)
-> (forall a. Eq a => a -> TypedBinding' a -> Bool)
-> (forall a. Ord a => TypedBinding' a -> a)
-> (forall a. Ord a => TypedBinding' a -> a)
-> (forall a. Num a => TypedBinding' a -> a)
-> (forall a. Num a => TypedBinding' a -> a)
-> Foldable TypedBinding'
forall a. Eq a => a -> TypedBinding' a -> Bool
forall a. Num a => TypedBinding' a -> a
forall a. Ord a => TypedBinding' a -> a
forall m. Monoid m => TypedBinding' m -> m
forall a. TypedBinding' a -> Bool
forall a. TypedBinding' a -> Int
forall a. TypedBinding' a -> [a]
forall a. (a -> a -> a) -> TypedBinding' a -> a
forall m a. Monoid m => (a -> m) -> TypedBinding' a -> m
forall b a. (b -> a -> b) -> b -> TypedBinding' a -> b
forall a b. (a -> b -> b) -> b -> TypedBinding' 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 => TypedBinding' m -> m
fold :: forall m. Monoid m => TypedBinding' m -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> TypedBinding' a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> TypedBinding' a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> TypedBinding' a -> m
foldMap' :: forall m a. Monoid m => (a -> m) -> TypedBinding' a -> m
$cfoldr :: forall a b. (a -> b -> b) -> b -> TypedBinding' a -> b
foldr :: forall a b. (a -> b -> b) -> b -> TypedBinding' a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> TypedBinding' a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> TypedBinding' a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> TypedBinding' a -> b
foldl :: forall b a. (b -> a -> b) -> b -> TypedBinding' a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> TypedBinding' a -> b
foldl' :: forall b a. (b -> a -> b) -> b -> TypedBinding' a -> b
$cfoldr1 :: forall a. (a -> a -> a) -> TypedBinding' a -> a
foldr1 :: forall a. (a -> a -> a) -> TypedBinding' a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> TypedBinding' a -> a
foldl1 :: forall a. (a -> a -> a) -> TypedBinding' a -> a
$ctoList :: forall a. TypedBinding' a -> [a]
toList :: forall a. TypedBinding' a -> [a]
$cnull :: forall a. TypedBinding' a -> Bool
null :: forall a. TypedBinding' a -> Bool
$clength :: forall a. TypedBinding' a -> Int
length :: forall a. TypedBinding' a -> Int
$celem :: forall a. Eq a => a -> TypedBinding' a -> Bool
elem :: forall a. Eq a => a -> TypedBinding' a -> Bool
$cmaximum :: forall a. Ord a => TypedBinding' a -> a
maximum :: forall a. Ord a => TypedBinding' a -> a
$cminimum :: forall a. Ord a => TypedBinding' a -> a
minimum :: forall a. Ord a => TypedBinding' a -> a
$csum :: forall a. Num a => TypedBinding' a -> a
sum :: forall a. Num a => TypedBinding' a -> a
$cproduct :: forall a. Num a => TypedBinding' a -> a
product :: forall a. Num a => TypedBinding' a -> a
Foldable, Functor TypedBinding'
Foldable TypedBinding'
(Functor TypedBinding', Foldable TypedBinding') =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> TypedBinding' a -> f (TypedBinding' b))
-> (forall (f :: * -> *) a.
    Applicative f =>
    TypedBinding' (f a) -> f (TypedBinding' a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> TypedBinding' a -> m (TypedBinding' b))
-> (forall (m :: * -> *) a.
    Monad m =>
    TypedBinding' (m a) -> m (TypedBinding' a))
-> Traversable TypedBinding'
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 =>
TypedBinding' (m a) -> m (TypedBinding' a)
forall (f :: * -> *) a.
Applicative f =>
TypedBinding' (f a) -> f (TypedBinding' a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> TypedBinding' a -> m (TypedBinding' b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> TypedBinding' a -> f (TypedBinding' b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> TypedBinding' a -> f (TypedBinding' b)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> TypedBinding' a -> f (TypedBinding' b)
$csequenceA :: forall (f :: * -> *) a.
Applicative f =>
TypedBinding' (f a) -> f (TypedBinding' a)
sequenceA :: forall (f :: * -> *) a.
Applicative f =>
TypedBinding' (f a) -> f (TypedBinding' a)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> TypedBinding' a -> m (TypedBinding' b)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> TypedBinding' a -> m (TypedBinding' b)
$csequence :: forall (m :: * -> *) a.
Monad m =>
TypedBinding' (m a) -> m (TypedBinding' a)
sequence :: forall (m :: * -> *) a.
Monad m =>
TypedBinding' (m a) -> m (TypedBinding' a)
Traversable, TypedBinding' e -> TypedBinding' e -> Bool
(TypedBinding' e -> TypedBinding' e -> Bool)
-> (TypedBinding' e -> TypedBinding' e -> Bool)
-> Eq (TypedBinding' e)
forall e. Eq e => TypedBinding' e -> TypedBinding' e -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall e. Eq e => TypedBinding' e -> TypedBinding' e -> Bool
== :: TypedBinding' e -> TypedBinding' e -> Bool
$c/= :: forall e. Eq e => TypedBinding' e -> TypedBinding' e -> Bool
/= :: TypedBinding' e -> TypedBinding' e -> Bool
Eq)

-- | A telescope is a sequence of typed bindings. Bound variables are in scope
--   in later types.
type Telescope1 = List1 TypedBinding
type Telescope  = [TypedBinding]

-- | We can try to get a @Telescope@ from a @[LamBinding]@.
--   If we have a type annotation already, we're happy.
--   Otherwise we manufacture a binder with an underscore for the type.
lamBindingsToTelescope :: Range -> [LamBinding] -> Telescope
lamBindingsToTelescope :: Range -> [LamBinding] -> Telescope
lamBindingsToTelescope Range
r = (LamBinding -> TypedBinding' Expr) -> [LamBinding] -> Telescope
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((LamBinding -> TypedBinding' Expr) -> [LamBinding] -> Telescope)
-> (LamBinding -> TypedBinding' Expr) -> [LamBinding] -> Telescope
forall a b. (a -> b) -> a -> b
$ \case
  DomainFull TypedBinding' Expr
ty -> TypedBinding' Expr
ty
  DomainFree NamedArg Binder
nm -> Range -> List1 (NamedArg Binder) -> Expr -> TypedBinding' Expr
forall e. Range -> List1 (NamedArg Binder) -> e -> TypedBinding' e
TBind Range
r (NamedArg Binder -> List1 (NamedArg Binder)
forall a. a -> NonEmpty a
List1.singleton NamedArg Binder
nm) (Expr -> TypedBinding' Expr) -> Expr -> TypedBinding' Expr
forall a b. (a -> b) -> a -> b
$ Range -> Maybe String -> Expr
Underscore Range
r Maybe String
forall a. Maybe a
Nothing

-- | Smart constructor for @Pi@: check whether the @Telescope@ is empty

makePi :: Telescope -> Expr -> Expr
makePi :: Telescope -> Expr -> Expr
makePi []     = Expr -> Expr
forall a. a -> a
id
makePi (TypedBinding' Expr
b:Telescope
bs) = Telescope1 -> Expr -> Expr
Pi (TypedBinding' Expr
b TypedBinding' Expr -> Telescope -> Telescope1
forall a. a -> [a] -> NonEmpty a
:| Telescope
bs)

-- | Smart constructor for @Lam@: check for non-zero bindings.

mkLam :: Range -> [LamBinding] -> Expr -> Expr
mkLam :: Range -> [LamBinding] -> Expr -> Expr
mkLam Range
r []     Expr
e = Expr
e
mkLam Range
r (LamBinding
x:[LamBinding]
xs) Expr
e = Range -> List1 LamBinding -> Expr -> Expr
Lam Range
r (LamBinding
x LamBinding -> [LamBinding] -> List1 LamBinding
forall a. a -> [a] -> NonEmpty a
:| [LamBinding]
xs) Expr
e

-- | Smart constructor for @Let@: check for non-zero let bindings.

mkLet :: Range -> [Declaration] -> Expr -> Expr
mkLet :: Range -> [Declaration] -> Expr -> Expr
mkLet Range
r []     Expr
e = Expr
e
mkLet Range
r (Declaration
d:[Declaration]
ds) Expr
e = Range -> List1 Declaration -> Maybe Expr -> Expr
Let Range
r (Declaration
d Declaration -> [Declaration] -> List1 Declaration
forall a. a -> [a] -> NonEmpty a
:| [Declaration]
ds) (Expr -> Maybe Expr
forall a. a -> Maybe a
Just Expr
e)

-- | Smart constructor for @TLet@: check for non-zero let bindings.

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

{-| Left hand sides can be written in infix style. For example:

    > n + suc m = suc (n + m)
    > (f ∘ g) x = f (g x)

   We use fixity information to see which name is actually defined.
-}
data LHS = LHS  -- ^ Original pattern (including with-patterns), rewrite equations and with-expressions.
  { LHS -> Pattern
lhsOriginalPattern :: Pattern
    -- ^ e.g. @f ps | wps@
  , LHS -> [RewriteEqn]
lhsRewriteEqn      :: [RewriteEqn]
    -- ^ @(rewrite e | with p <- e in eq)@ (many)
  , LHS -> [WithExpr]
lhsWithExpr        :: [WithExpr]
    -- ^ @with e1 in eq | {e2} | ...@ (many)
  }
  deriving LHS -> LHS -> Bool
(LHS -> LHS -> Bool) -> (LHS -> LHS -> Bool) -> Eq LHS
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: LHS -> LHS -> Bool
== :: LHS -> LHS -> Bool
$c/= :: LHS -> LHS -> Bool
/= :: LHS -> LHS -> Bool
Eq

type RewriteEqn = RewriteEqn' () Name Pattern Expr
type WithExpr   = Named Name (Arg Expr)

-- | Processed (operator-parsed) intermediate form of the core @f ps@ of 'LHS'.
--   Corresponds to 'lhsOriginalPattern'.
data LHSCore
  = LHSHead  { LHSCore -> QName
lhsDefName      :: QName               -- ^ @f@
             , LHSCore -> [NamedArg Pattern]
lhsPats         :: [NamedArg Pattern]  -- ^ @ps@
             }
  | LHSProj  { LHSCore -> QName
lhsDestructor   :: QName               -- ^ Record projection.
             , LHSCore -> [NamedArg Pattern]
lhsPatsLeft     :: [NamedArg Pattern]  -- ^ Patterns for record indices (currently none).
             , LHSCore -> NamedArg LHSCore
lhsFocus        :: NamedArg LHSCore    -- ^ Main argument.
             , lhsPats         :: [NamedArg Pattern]  -- ^ More application patterns.
             }
  | LHSWith  { LHSCore -> LHSCore
lhsHead         :: LHSCore
             , LHSCore -> [Pattern]
lhsWithPatterns :: [Pattern]          -- ^ Non-empty; at least one @(| p)@.
             , lhsPats         :: [NamedArg Pattern] -- ^ More application patterns.
             }
  | LHSEllipsis
             { LHSCore -> Range
lhsEllipsisRange :: Range
             , LHSCore -> LHSCore
lhsEllipsisPat   :: LHSCore           -- ^ Pattern that was expanded from an ellipsis @...@.
             }
  deriving LHSCore -> LHSCore -> Bool
(LHSCore -> LHSCore -> Bool)
-> (LHSCore -> LHSCore -> Bool) -> Eq LHSCore
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: LHSCore -> LHSCore -> Bool
== :: LHSCore -> LHSCore -> Bool
$c/= :: LHSCore -> LHSCore -> Bool
/= :: LHSCore -> LHSCore -> Bool
Eq

type RHS = RHS' Expr
data RHS' e
  = AbsurdRHS -- ^ No right hand side because of absurd match.
  | RHS e
  deriving ((forall a b. (a -> b) -> RHS' a -> RHS' b)
-> (forall a b. a -> RHS' b -> RHS' a) -> Functor RHS'
forall a b. a -> RHS' b -> RHS' a
forall a b. (a -> b) -> RHS' a -> RHS' 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) -> RHS' a -> RHS' b
fmap :: forall a b. (a -> b) -> RHS' a -> RHS' b
$c<$ :: forall a b. a -> RHS' b -> RHS' a
<$ :: forall a b. a -> RHS' b -> RHS' a
Functor, (forall m. Monoid m => RHS' m -> m)
-> (forall m a. Monoid m => (a -> m) -> RHS' a -> m)
-> (forall m a. Monoid m => (a -> m) -> RHS' a -> m)
-> (forall a b. (a -> b -> b) -> b -> RHS' a -> b)
-> (forall a b. (a -> b -> b) -> b -> RHS' a -> b)
-> (forall b a. (b -> a -> b) -> b -> RHS' a -> b)
-> (forall b a. (b -> a -> b) -> b -> RHS' a -> b)
-> (forall a. (a -> a -> a) -> RHS' a -> a)
-> (forall a. (a -> a -> a) -> RHS' a -> a)
-> (forall a. RHS' a -> [a])
-> (forall a. RHS' a -> Bool)
-> (forall a. RHS' a -> Int)
-> (forall a. Eq a => a -> RHS' a -> Bool)
-> (forall a. Ord a => RHS' a -> a)
-> (forall a. Ord a => RHS' a -> a)
-> (forall a. Num a => RHS' a -> a)
-> (forall a. Num a => RHS' a -> a)
-> Foldable RHS'
forall a. Eq a => a -> RHS' a -> Bool
forall a. Num a => RHS' a -> a
forall a. Ord a => RHS' a -> a
forall m. Monoid m => RHS' m -> m
forall a. RHS' a -> Bool
forall a. RHS' a -> Int
forall a. RHS' a -> [a]
forall a. (a -> a -> a) -> RHS' a -> a
forall m a. Monoid m => (a -> m) -> RHS' a -> m
forall b a. (b -> a -> b) -> b -> RHS' a -> b
forall a b. (a -> b -> b) -> b -> RHS' 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 => RHS' m -> m
fold :: forall m. Monoid m => RHS' m -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> RHS' a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> RHS' a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> RHS' a -> m
foldMap' :: forall m a. Monoid m => (a -> m) -> RHS' a -> m
$cfoldr :: forall a b. (a -> b -> b) -> b -> RHS' a -> b
foldr :: forall a b. (a -> b -> b) -> b -> RHS' a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> RHS' a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> RHS' a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> RHS' a -> b
foldl :: forall b a. (b -> a -> b) -> b -> RHS' a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> RHS' a -> b
foldl' :: forall b a. (b -> a -> b) -> b -> RHS' a -> b
$cfoldr1 :: forall a. (a -> a -> a) -> RHS' a -> a
foldr1 :: forall a. (a -> a -> a) -> RHS' a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> RHS' a -> a
foldl1 :: forall a. (a -> a -> a) -> RHS' a -> a
$ctoList :: forall a. RHS' a -> [a]
toList :: forall a. RHS' a -> [a]
$cnull :: forall a. RHS' a -> Bool
null :: forall a. RHS' a -> Bool
$clength :: forall a. RHS' a -> Int
length :: forall a. RHS' a -> Int
$celem :: forall a. Eq a => a -> RHS' a -> Bool
elem :: forall a. Eq a => a -> RHS' a -> Bool
$cmaximum :: forall a. Ord a => RHS' a -> a
maximum :: forall a. Ord a => RHS' a -> a
$cminimum :: forall a. Ord a => RHS' a -> a
minimum :: forall a. Ord a => RHS' a -> a
$csum :: forall a. Num a => RHS' a -> a
sum :: forall a. Num a => RHS' a -> a
$cproduct :: forall a. Num a => RHS' a -> a
product :: forall a. Num a => RHS' a -> a
Foldable, Functor RHS'
Foldable RHS'
(Functor RHS', Foldable RHS') =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> RHS' a -> f (RHS' b))
-> (forall (f :: * -> *) a.
    Applicative f =>
    RHS' (f a) -> f (RHS' a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> RHS' a -> m (RHS' b))
-> (forall (m :: * -> *) a. Monad m => RHS' (m a) -> m (RHS' a))
-> Traversable RHS'
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 => RHS' (m a) -> m (RHS' a)
forall (f :: * -> *) a. Applicative f => RHS' (f a) -> f (RHS' a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> RHS' a -> m (RHS' b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> RHS' a -> f (RHS' b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> RHS' a -> f (RHS' b)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> RHS' a -> f (RHS' b)
$csequenceA :: forall (f :: * -> *) a. Applicative f => RHS' (f a) -> f (RHS' a)
sequenceA :: forall (f :: * -> *) a. Applicative f => RHS' (f a) -> f (RHS' a)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> RHS' a -> m (RHS' b)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> RHS' a -> m (RHS' b)
$csequence :: forall (m :: * -> *) a. Monad m => RHS' (m a) -> m (RHS' a)
sequence :: forall (m :: * -> *) a. Monad m => RHS' (m a) -> m (RHS' a)
Traversable, RHS' e -> RHS' e -> Bool
(RHS' e -> RHS' e -> Bool)
-> (RHS' e -> RHS' e -> Bool) -> Eq (RHS' e)
forall e. Eq e => RHS' e -> RHS' e -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall e. Eq e => RHS' e -> RHS' e -> Bool
== :: RHS' e -> RHS' e -> Bool
$c/= :: forall e. Eq e => RHS' e -> RHS' e -> Bool
/= :: RHS' e -> RHS' e -> Bool
Eq)

-- | @where@ block following a clause.
type WhereClause = WhereClause' [Declaration]

-- The generalization @WhereClause'@ is for the sake of Concrete.Generic.
data WhereClause' decls
  = NoWhere
      -- ^ No @where@ clauses.
  | AnyWhere Range decls
      -- ^ Ordinary @where@.  'Range' of the @where@ keyword.
      --   List of declarations can be empty.
  | SomeWhere Range Erased Name Access decls
      -- ^ Named where: @module M where ds@.
      --   'Range' of the keywords @module@ and @where@.
      --   The 'Access' flag applies to the 'Name' (not the module contents!)
      --   and is propagated from the parent function.
      --   List of declarations can be empty.
  deriving (WhereClause' decls -> WhereClause' decls -> Bool
(WhereClause' decls -> WhereClause' decls -> Bool)
-> (WhereClause' decls -> WhereClause' decls -> Bool)
-> Eq (WhereClause' decls)
forall decls.
Eq decls =>
WhereClause' decls -> WhereClause' decls -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall decls.
Eq decls =>
WhereClause' decls -> WhereClause' decls -> Bool
== :: WhereClause' decls -> WhereClause' decls -> Bool
$c/= :: forall decls.
Eq decls =>
WhereClause' decls -> WhereClause' decls -> Bool
/= :: WhereClause' decls -> WhereClause' decls -> Bool
Eq, (forall a b. (a -> b) -> WhereClause' a -> WhereClause' b)
-> (forall a b. a -> WhereClause' b -> WhereClause' a)
-> Functor WhereClause'
forall a b. a -> WhereClause' b -> WhereClause' a
forall a b. (a -> b) -> WhereClause' a -> WhereClause' 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) -> WhereClause' a -> WhereClause' b
fmap :: forall a b. (a -> b) -> WhereClause' a -> WhereClause' b
$c<$ :: forall a b. a -> WhereClause' b -> WhereClause' a
<$ :: forall a b. a -> WhereClause' b -> WhereClause' a
Functor, (forall m. Monoid m => WhereClause' m -> m)
-> (forall m a. Monoid m => (a -> m) -> WhereClause' a -> m)
-> (forall m a. Monoid m => (a -> m) -> WhereClause' a -> m)
-> (forall a b. (a -> b -> b) -> b -> WhereClause' a -> b)
-> (forall a b. (a -> b -> b) -> b -> WhereClause' a -> b)
-> (forall b a. (b -> a -> b) -> b -> WhereClause' a -> b)
-> (forall b a. (b -> a -> b) -> b -> WhereClause' a -> b)
-> (forall a. (a -> a -> a) -> WhereClause' a -> a)
-> (forall a. (a -> a -> a) -> WhereClause' a -> a)
-> (forall a. WhereClause' a -> [a])
-> (forall a. WhereClause' a -> Bool)
-> (forall a. WhereClause' a -> Int)
-> (forall a. Eq a => a -> WhereClause' a -> Bool)
-> (forall a. Ord a => WhereClause' a -> a)
-> (forall a. Ord a => WhereClause' a -> a)
-> (forall a. Num a => WhereClause' a -> a)
-> (forall a. Num a => WhereClause' a -> a)
-> Foldable WhereClause'
forall a. Eq a => a -> WhereClause' a -> Bool
forall a. Num a => WhereClause' a -> a
forall a. Ord a => WhereClause' a -> a
forall m. Monoid m => WhereClause' m -> m
forall a. WhereClause' a -> Bool
forall a. WhereClause' a -> Int
forall a. WhereClause' a -> [a]
forall a. (a -> a -> a) -> WhereClause' a -> a
forall m a. Monoid m => (a -> m) -> WhereClause' a -> m
forall b a. (b -> a -> b) -> b -> WhereClause' a -> b
forall a b. (a -> b -> b) -> b -> WhereClause' 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 => WhereClause' m -> m
fold :: forall m. Monoid m => WhereClause' m -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> WhereClause' a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> WhereClause' a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> WhereClause' a -> m
foldMap' :: forall m a. Monoid m => (a -> m) -> WhereClause' a -> m
$cfoldr :: forall a b. (a -> b -> b) -> b -> WhereClause' a -> b
foldr :: forall a b. (a -> b -> b) -> b -> WhereClause' a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> WhereClause' a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> WhereClause' a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> WhereClause' a -> b
foldl :: forall b a. (b -> a -> b) -> b -> WhereClause' a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> WhereClause' a -> b
foldl' :: forall b a. (b -> a -> b) -> b -> WhereClause' a -> b
$cfoldr1 :: forall a. (a -> a -> a) -> WhereClause' a -> a
foldr1 :: forall a. (a -> a -> a) -> WhereClause' a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> WhereClause' a -> a
foldl1 :: forall a. (a -> a -> a) -> WhereClause' a -> a
$ctoList :: forall a. WhereClause' a -> [a]
toList :: forall a. WhereClause' a -> [a]
$cnull :: forall a. WhereClause' a -> Bool
null :: forall a. WhereClause' a -> Bool
$clength :: forall a. WhereClause' a -> Int
length :: forall a. WhereClause' a -> Int
$celem :: forall a. Eq a => a -> WhereClause' a -> Bool
elem :: forall a. Eq a => a -> WhereClause' a -> Bool
$cmaximum :: forall a. Ord a => WhereClause' a -> a
maximum :: forall a. Ord a => WhereClause' a -> a
$cminimum :: forall a. Ord a => WhereClause' a -> a
minimum :: forall a. Ord a => WhereClause' a -> a
$csum :: forall a. Num a => WhereClause' a -> a
sum :: forall a. Num a => WhereClause' a -> a
$cproduct :: forall a. Num a => WhereClause' a -> a
product :: forall a. Num a => WhereClause' a -> a
Foldable, Functor WhereClause'
Foldable WhereClause'
(Functor WhereClause', Foldable WhereClause') =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> WhereClause' a -> f (WhereClause' b))
-> (forall (f :: * -> *) a.
    Applicative f =>
    WhereClause' (f a) -> f (WhereClause' a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> WhereClause' a -> m (WhereClause' b))
-> (forall (m :: * -> *) a.
    Monad m =>
    WhereClause' (m a) -> m (WhereClause' a))
-> Traversable WhereClause'
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 =>
WhereClause' (m a) -> m (WhereClause' a)
forall (f :: * -> *) a.
Applicative f =>
WhereClause' (f a) -> f (WhereClause' a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> WhereClause' a -> m (WhereClause' b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> WhereClause' a -> f (WhereClause' b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> WhereClause' a -> f (WhereClause' b)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> WhereClause' a -> f (WhereClause' b)
$csequenceA :: forall (f :: * -> *) a.
Applicative f =>
WhereClause' (f a) -> f (WhereClause' a)
sequenceA :: forall (f :: * -> *) a.
Applicative f =>
WhereClause' (f a) -> f (WhereClause' a)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> WhereClause' a -> m (WhereClause' b)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> WhereClause' a -> m (WhereClause' b)
$csequence :: forall (m :: * -> *) a.
Monad m =>
WhereClause' (m a) -> m (WhereClause' a)
sequence :: forall (m :: * -> *) a.
Monad m =>
WhereClause' (m a) -> m (WhereClause' a)
Traversable)

data LamClause = LamClause
  { LamClause -> [Pattern]
lamLHS      :: [Pattern]   -- ^ Possibly empty sequence.
  , LamClause -> RHS
lamRHS      :: RHS
  , LamClause -> Bool
lamCatchAll :: Bool
  }
  deriving LamClause -> LamClause -> Bool
(LamClause -> LamClause -> Bool)
-> (LamClause -> LamClause -> Bool) -> Eq LamClause
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: LamClause -> LamClause -> Bool
== :: LamClause -> LamClause -> Bool
$c/= :: LamClause -> LamClause -> Bool
/= :: LamClause -> LamClause -> Bool
Eq

-- | An expression followed by a where clause.
--   Currently only used to give better a better error message in interaction.
data ExprWhere = ExprWhere Expr WhereClause

-- | The things you are allowed to say when you shuffle names between name
--   spaces (i.e. in @import@, @namespace@, or @open@ declarations).
type ImportDirective = ImportDirective' Name Name
type Using           = Using'           Name Name
type Renaming        = Renaming'        Name Name
type RenamingDirective = RenamingDirective' Name Name
type HidingDirective   = HidingDirective'   Name Name  -- 'Hiding' is already taken

-- | An imported name can be a module or a defined name.
type ImportedName = ImportedName' Name Name

-- | The content of the @as@-clause of the import statement.
data AsName' a = AsName
  { forall a. AsName' a -> a
asName  :: a
    -- ^ The \"as\" name.
  , forall a. AsName' a -> Range
asRange :: Range
    -- ^ The range of the \"as\" keyword.  Retained for highlighting purposes.
  }
  deriving (Int -> AsName' a -> ShowS
[AsName' a] -> ShowS
AsName' a -> String
(Int -> AsName' a -> ShowS)
-> (AsName' a -> String)
-> ([AsName' a] -> ShowS)
-> Show (AsName' a)
forall a. Show a => Int -> AsName' a -> ShowS
forall a. Show a => [AsName' a] -> ShowS
forall a. Show a => AsName' a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Show a => Int -> AsName' a -> ShowS
showsPrec :: Int -> AsName' a -> ShowS
$cshow :: forall a. Show a => AsName' a -> String
show :: AsName' a -> String
$cshowList :: forall a. Show a => [AsName' a] -> ShowS
showList :: [AsName' a] -> ShowS
Show, (forall a b. (a -> b) -> AsName' a -> AsName' b)
-> (forall a b. a -> AsName' b -> AsName' a) -> Functor AsName'
forall a b. a -> AsName' b -> AsName' a
forall a b. (a -> b) -> AsName' a -> AsName' 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) -> AsName' a -> AsName' b
fmap :: forall a b. (a -> b) -> AsName' a -> AsName' b
$c<$ :: forall a b. a -> AsName' b -> AsName' a
<$ :: forall a b. a -> AsName' b -> AsName' a
Functor, (forall m. Monoid m => AsName' m -> m)
-> (forall m a. Monoid m => (a -> m) -> AsName' a -> m)
-> (forall m a. Monoid m => (a -> m) -> AsName' a -> m)
-> (forall a b. (a -> b -> b) -> b -> AsName' a -> b)
-> (forall a b. (a -> b -> b) -> b -> AsName' a -> b)
-> (forall b a. (b -> a -> b) -> b -> AsName' a -> b)
-> (forall b a. (b -> a -> b) -> b -> AsName' a -> b)
-> (forall a. (a -> a -> a) -> AsName' a -> a)
-> (forall a. (a -> a -> a) -> AsName' a -> a)
-> (forall a. AsName' a -> [a])
-> (forall a. AsName' a -> Bool)
-> (forall a. AsName' a -> Int)
-> (forall a. Eq a => a -> AsName' a -> Bool)
-> (forall a. Ord a => AsName' a -> a)
-> (forall a. Ord a => AsName' a -> a)
-> (forall a. Num a => AsName' a -> a)
-> (forall a. Num a => AsName' a -> a)
-> Foldable AsName'
forall a. Eq a => a -> AsName' a -> Bool
forall a. Num a => AsName' a -> a
forall a. Ord a => AsName' a -> a
forall m. Monoid m => AsName' m -> m
forall a. AsName' a -> Bool
forall a. AsName' a -> Int
forall a. AsName' a -> [a]
forall a. (a -> a -> a) -> AsName' a -> a
forall m a. Monoid m => (a -> m) -> AsName' a -> m
forall b a. (b -> a -> b) -> b -> AsName' a -> b
forall a b. (a -> b -> b) -> b -> AsName' 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 => AsName' m -> m
fold :: forall m. Monoid m => AsName' m -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> AsName' a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> AsName' a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> AsName' a -> m
foldMap' :: forall m a. Monoid m => (a -> m) -> AsName' a -> m
$cfoldr :: forall a b. (a -> b -> b) -> b -> AsName' a -> b
foldr :: forall a b. (a -> b -> b) -> b -> AsName' a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> AsName' a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> AsName' a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> AsName' a -> b
foldl :: forall b a. (b -> a -> b) -> b -> AsName' a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> AsName' a -> b
foldl' :: forall b a. (b -> a -> b) -> b -> AsName' a -> b
$cfoldr1 :: forall a. (a -> a -> a) -> AsName' a -> a
foldr1 :: forall a. (a -> a -> a) -> AsName' a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> AsName' a -> a
foldl1 :: forall a. (a -> a -> a) -> AsName' a -> a
$ctoList :: forall a. AsName' a -> [a]
toList :: forall a. AsName' a -> [a]
$cnull :: forall a. AsName' a -> Bool
null :: forall a. AsName' a -> Bool
$clength :: forall a. AsName' a -> Int
length :: forall a. AsName' a -> Int
$celem :: forall a. Eq a => a -> AsName' a -> Bool
elem :: forall a. Eq a => a -> AsName' a -> Bool
$cmaximum :: forall a. Ord a => AsName' a -> a
maximum :: forall a. Ord a => AsName' a -> a
$cminimum :: forall a. Ord a => AsName' a -> a
minimum :: forall a. Ord a => AsName' a -> a
$csum :: forall a. Num a => AsName' a -> a
sum :: forall a. Num a => AsName' a -> a
$cproduct :: forall a. Num a => AsName' a -> a
product :: forall a. Num a => AsName' a -> a
Foldable, Functor AsName'
Foldable AsName'
(Functor AsName', Foldable AsName') =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> AsName' a -> f (AsName' b))
-> (forall (f :: * -> *) a.
    Applicative f =>
    AsName' (f a) -> f (AsName' a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> AsName' a -> m (AsName' b))
-> (forall (m :: * -> *) a.
    Monad m =>
    AsName' (m a) -> m (AsName' a))
-> Traversable AsName'
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 => AsName' (m a) -> m (AsName' a)
forall (f :: * -> *) a.
Applicative f =>
AsName' (f a) -> f (AsName' a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> AsName' a -> m (AsName' b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> AsName' a -> f (AsName' b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> AsName' a -> f (AsName' b)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> AsName' a -> f (AsName' b)
$csequenceA :: forall (f :: * -> *) a.
Applicative f =>
AsName' (f a) -> f (AsName' a)
sequenceA :: forall (f :: * -> *) a.
Applicative f =>
AsName' (f a) -> f (AsName' a)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> AsName' a -> m (AsName' b)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> AsName' a -> m (AsName' b)
$csequence :: forall (m :: * -> *) a. Monad m => AsName' (m a) -> m (AsName' a)
sequence :: forall (m :: * -> *) a. Monad m => AsName' (m a) -> m (AsName' a)
Traversable, AsName' a -> AsName' a -> Bool
(AsName' a -> AsName' a -> Bool)
-> (AsName' a -> AsName' a -> Bool) -> Eq (AsName' a)
forall a. Eq a => AsName' a -> AsName' a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall a. Eq a => AsName' a -> AsName' a -> Bool
== :: AsName' a -> AsName' a -> Bool
$c/= :: forall a. Eq a => AsName' a -> AsName' a -> Bool
/= :: AsName' a -> AsName' a -> Bool
Eq)

-- | From the parser, we get an expression for the @as@-'Name', which
--   we have to parse into a 'Name'.
type AsName = AsName' (Either Expr Name)

{--------------------------------------------------------------------------
    Declarations
 --------------------------------------------------------------------------}

-- | Just type signatures.
type TypeSignature = Declaration

-- | Just field signatures
type FieldSignature = Declaration

-- | Just type signatures or instance blocks.
type TypeSignatureOrInstanceBlock = Declaration

-- | Isolated record directives parsed as Declarations
data RecordDirective
   = Induction (Ranged Induction)
       -- ^ Range of keyword @[co]inductive@.
   | Constructor Name IsInstance
   | Eta         (Ranged HasEta0)
       -- ^ Range of @[no-]eta-equality@ keyword.
   | PatternOrCopattern Range
       -- ^ If declaration @pattern@ is present, give its range.
   deriving (RecordDirective -> RecordDirective -> Bool
(RecordDirective -> RecordDirective -> Bool)
-> (RecordDirective -> RecordDirective -> Bool)
-> Eq RecordDirective
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: RecordDirective -> RecordDirective -> Bool
== :: RecordDirective -> RecordDirective -> Bool
$c/= :: RecordDirective -> RecordDirective -> Bool
/= :: RecordDirective -> RecordDirective -> Bool
Eq, Int -> RecordDirective -> ShowS
[RecordDirective] -> ShowS
RecordDirective -> String
(Int -> RecordDirective -> ShowS)
-> (RecordDirective -> String)
-> ([RecordDirective] -> ShowS)
-> Show RecordDirective
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> RecordDirective -> ShowS
showsPrec :: Int -> RecordDirective -> ShowS
$cshow :: RecordDirective -> String
show :: RecordDirective -> String
$cshowList :: [RecordDirective] -> ShowS
showList :: [RecordDirective] -> ShowS
Show)

type RecordDirectives = RecordDirectives' (Name, IsInstance)

ungatherRecordDirectives :: RecordDirectives -> [RecordDirective]
ungatherRecordDirectives :: RecordDirectives -> [RecordDirective]
ungatherRecordDirectives (RecordDirectives Maybe (Ranged Induction)
ind Maybe (Ranged HasEta0)
eta Maybe Range
pat Maybe (Name, IsInstance)
con) = [Maybe RecordDirective] -> [RecordDirective]
forall a. [Maybe a] -> [a]
catMaybes
  [ Ranged Induction -> RecordDirective
Induction (Ranged Induction -> RecordDirective)
-> Maybe (Ranged Induction) -> Maybe RecordDirective
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (Ranged Induction)
ind
  , Ranged HasEta0 -> RecordDirective
Eta (Ranged HasEta0 -> RecordDirective)
-> Maybe (Ranged HasEta0) -> Maybe RecordDirective
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (Ranged HasEta0)
eta
  , Range -> RecordDirective
PatternOrCopattern (Range -> RecordDirective) -> Maybe Range -> Maybe RecordDirective
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Range
pat
  , (Name -> IsInstance -> RecordDirective)
-> (Name, IsInstance) -> RecordDirective
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Name -> IsInstance -> RecordDirective
Constructor ((Name, IsInstance) -> RecordDirective)
-> Maybe (Name, IsInstance) -> Maybe RecordDirective
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (Name, IsInstance)
con
  ]


{-| The representation type of a declaration. The comments indicate
    which type in the intended family the constructor targets.
-}

data Declaration
  = TypeSig ArgInfo TacticAttribute Name Expr
      -- ^ Axioms and functions can be irrelevant. (Hiding should be NotHidden)
  | FieldSig IsInstance TacticAttribute Name (Arg Expr)
  | Generalize KwRange [TypeSignature] -- ^ Variables to be generalized, can be hidden and/or irrelevant.
  | Field KwRange [FieldSignature]
  | FunClause LHS RHS WhereClause Bool
  | DataSig     Range Erased Name [LamBinding] Expr -- ^ lone data signature in mutual block
  | Data        Range Erased Name [LamBinding] Expr
                [TypeSignatureOrInstanceBlock]
  | DataDef     Range Name [LamBinding] [TypeSignatureOrInstanceBlock]
  | RecordSig   Range Erased Name [LamBinding] Expr -- ^ lone record signature in mutual block
  | RecordDef   Range Name [RecordDirective] [LamBinding] [Declaration]
  | Record      Range Erased Name [RecordDirective] [LamBinding] Expr
                [Declaration]
  | Infix Fixity (List1 Name)
  | Syntax      Name Notation -- ^ notation declaration for a name
  | PatternSyn  Range Name [WithHiding Name] Pattern
  | Mutual      KwRange [Declaration]
  | InterleavedMutual KwRange [Declaration]
  | Abstract    KwRange [Declaration]
  | Private     KwRange Origin [Declaration]
    -- ^ In "Agda.Syntax.Concrete.Definitions" we generate private blocks
    --   temporarily, which should be treated different that user-declared
    --   private blocks.  Thus the 'Origin'.
  | InstanceB   KwRange [Declaration]
    -- ^ The 'KwRange' here only refers to the range of the
    --   @instance@ keyword.  The range of the whole block @InstanceB r ds@
    --   is @fuseRange r ds@.
  | LoneConstructor KwRange [Declaration]
  | Macro       KwRange [Declaration]
  | Postulate   KwRange [TypeSignatureOrInstanceBlock]
  | Primitive   KwRange [TypeSignature]
  | Open        Range QName ImportDirective
  | Import      Range QName (Maybe AsName) !OpenShortHand ImportDirective
  | ModuleMacro Range Erased  Name ModuleApplication !OpenShortHand
                ImportDirective
  | Module      Range Erased QName Telescope [Declaration]
  | UnquoteDecl Range [Name] Expr
      -- ^ @unquoteDecl xs = e@
  | UnquoteDef  Range [Name] Expr
      -- ^ @unquoteDef xs = e@
  | UnquoteData Range Name [Name] Expr
      -- ^ @unquoteDecl data d constructor xs = e@
  | Pragma      Pragma
  | Opaque      KwRange [Declaration]
    -- ^ @opaque ...@
  | Unfolding   KwRange [QName]
    -- ^ @unfolding ...@
  deriving Declaration -> Declaration -> Bool
(Declaration -> Declaration -> Bool)
-> (Declaration -> Declaration -> Bool) -> Eq Declaration
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Declaration -> Declaration -> Bool
== :: Declaration -> Declaration -> Bool
$c/= :: Declaration -> Declaration -> Bool
/= :: Declaration -> Declaration -> Bool
Eq

-- | Return 'Pragma' if 'Declaration' is 'Pragma'.
{-# SPECIALIZE isPragma :: Declaration -> Maybe Pragma #-}
{-# SPECIALIZE isPragma :: Declaration -> [Pragma] #-}
isPragma :: CMaybe Pragma m => Declaration -> m
isPragma :: forall m. CMaybe Pragma m => Declaration -> m
isPragma = \case
    Pragma Pragma
p                -> Pragma -> m
forall el coll. Singleton el coll => el -> coll
singleton Pragma
p
    Private  KwRange
_ Origin
_ [Declaration]
_          -> m
forall a. Null a => a
empty
    Abstract KwRange
_ [Declaration]
_            -> m
forall a. Null a => a
empty
    InstanceB KwRange
_ [Declaration]
_           -> m
forall a. Null a => a
empty
    Mutual KwRange
_ [Declaration]
_              -> m
forall a. Null a => a
empty
    Module Range
_ Erased
_ QName
_ Telescope
_ [Declaration]
_        -> m
forall a. Null a => a
empty
    Macro KwRange
_ [Declaration]
_               -> m
forall a. Null a => a
empty
    Record Range
_ Erased
_ Name
_ [RecordDirective]
_ [LamBinding]
_ Expr
_ [Declaration]
_    -> m
forall a. Null a => a
empty
    RecordDef Range
_ Name
_ [RecordDirective]
_ [LamBinding]
_ [Declaration]
_     -> m
forall a. Null a => a
empty
    TypeSig ArgInfo
_ TacticAttribute
_ Name
_ Expr
_         -> m
forall a. Null a => a
empty
    FieldSig IsInstance
_ TacticAttribute
_ Name
_ Arg Expr
_        -> m
forall a. Null a => a
empty
    Generalize KwRange
_ [Declaration]
_          -> m
forall a. Null a => a
empty
    Field KwRange
_ [Declaration]
_               -> m
forall a. Null a => a
empty
    FunClause LHS
_ RHS
_ WhereClause
_ Bool
_       -> m
forall a. Null a => a
empty
    DataSig Range
_ Erased
_ Name
_ [LamBinding]
_ Expr
_       -> m
forall a. Null a => a
empty
    Data Range
_ Erased
_ Name
_ [LamBinding]
_ Expr
_ [Declaration]
_        -> m
forall a. Null a => a
empty
    DataDef Range
_ Name
_ [LamBinding]
_ [Declaration]
_         -> m
forall a. Null a => a
empty
    RecordSig Range
_ Erased
_ Name
_ [LamBinding]
_ Expr
_     -> m
forall a. Null a => a
empty
    Infix Fixity
_ List1 Name
_               -> m
forall a. Null a => a
empty
    Syntax Name
_ Notation
_              -> m
forall a. Null a => a
empty
    PatternSyn Range
_ Name
_ [WithHiding Name]
_ Pattern
_      -> m
forall a. Null a => a
empty
    InterleavedMutual KwRange
_ [Declaration]
_   -> m
forall a. Null a => a
empty
    LoneConstructor KwRange
_ [Declaration]
_     -> m
forall a. Null a => a
empty
    Postulate KwRange
_ [Declaration]
_           -> m
forall a. Null a => a
empty
    Primitive KwRange
_ [Declaration]
_           -> m
forall a. Null a => a
empty
    Open Range
_ QName
_ ImportDirective
_              -> m
forall a. Null a => a
empty
    Import Range
_ QName
_ Maybe AsName
_ OpenShortHand
_ ImportDirective
_        -> m
forall a. Null a => a
empty
    ModuleMacro Range
_ Erased
_ Name
_ ModuleApplication
_ OpenShortHand
_ ImportDirective
_ -> m
forall a. Null a => a
empty
    UnquoteDecl Range
_ [Name]
_ Expr
_       -> m
forall a. Null a => a
empty
    UnquoteDef Range
_ [Name]
_ Expr
_        -> m
forall a. Null a => a
empty
    UnquoteData Range
_ Name
_ [Name]
_ Expr
_     -> m
forall a. Null a => a
empty
    Opaque KwRange
_ [Declaration]
_              -> m
forall a. Null a => a
empty
    Unfolding KwRange
_ [QName]
_           -> m
forall a. Null a => a
empty

data ModuleApplication
  = SectionApp Range Telescope Expr
    -- ^ @tel. M args@
  | RecordModuleInstance Range QName
    -- ^ @M {{...}}@
  deriving 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

data OpenShortHand = DoOpen | DontOpen
  deriving (OpenShortHand -> OpenShortHand -> Bool
(OpenShortHand -> OpenShortHand -> Bool)
-> (OpenShortHand -> OpenShortHand -> Bool) -> Eq OpenShortHand
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: OpenShortHand -> OpenShortHand -> Bool
== :: OpenShortHand -> OpenShortHand -> Bool
$c/= :: OpenShortHand -> OpenShortHand -> Bool
/= :: OpenShortHand -> OpenShortHand -> Bool
Eq, Int -> OpenShortHand -> ShowS
[OpenShortHand] -> ShowS
OpenShortHand -> String
(Int -> OpenShortHand -> ShowS)
-> (OpenShortHand -> String)
-> ([OpenShortHand] -> ShowS)
-> Show OpenShortHand
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> OpenShortHand -> ShowS
showsPrec :: Int -> OpenShortHand -> ShowS
$cshow :: OpenShortHand -> String
show :: OpenShortHand -> String
$cshowList :: [OpenShortHand] -> ShowS
showList :: [OpenShortHand] -> ShowS
Show, (forall x. OpenShortHand -> Rep OpenShortHand x)
-> (forall x. Rep OpenShortHand x -> OpenShortHand)
-> Generic OpenShortHand
forall x. Rep OpenShortHand x -> OpenShortHand
forall x. OpenShortHand -> Rep OpenShortHand x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. OpenShortHand -> Rep OpenShortHand x
from :: forall x. OpenShortHand -> Rep OpenShortHand x
$cto :: forall x. Rep OpenShortHand x -> OpenShortHand
to :: forall x. Rep OpenShortHand x -> OpenShortHand
Generic)

-- Pragmas ----------------------------------------------------------------

data Pragma
  = OptionsPragma               Range [String]
  | BuiltinPragma               Range RString QName
  | RewritePragma               Range Range [QName]        -- ^ Second Range is for REWRITE keyword.
  | ForeignPragma               Range RString String       -- ^ first string is backend name
  | CompilePragma               Range RString QName String -- ^ first string is backend name
  | StaticPragma                Range QName
  | InlinePragma                Range Bool QName  -- ^ INLINE or NOINLINE

  | ImpossiblePragma            Range [String]
    -- ^ Throws an internal error in the scope checker.
    --   The 'String's are words to be displayed with the error.
  | EtaPragma                   Range QName
    -- ^ For coinductive records, use pragma instead of regular
    --   @eta-equality@ definition (as it is might make Agda loop).
  | WarningOnUsage              Range QName Text
    -- ^ Applies to the named function
  | WarningOnImport             Range Text
    -- ^ Applies to the current module
  | InjectivePragma             Range QName
    -- ^ Mark a definition as injective for the pattern matching unifier.
  | InjectiveForInferencePragma Range QName
    -- ^ Mark a definition as injective for the conversion checker
  | DisplayPragma               Range Pattern Expr
    -- ^ Display lhs as rhs (modifies the printer).

  -- Attached (more or less) pragmas handled in the nicifier (Concrete.Definitions):
  | CatchallPragma              Range
    -- ^ Applies to the following function clause.
  | TerminationCheckPragma      Range (TerminationCheck Name)
    -- ^ Applies to the following function (and all that are mutually recursive with it)
    --   or to the functions in the following mutual block.
  | NoCoverageCheckPragma       Range
    -- ^ Applies to the following function (and all that are mutually recursive with it)
    --   or to the functions in the following mutual block.
  | NoPositivityCheckPragma     Range
    -- ^ Applies to the following data/record type or mutual block.
  | PolarityPragma              Range Name [Occurrence]
  | NoUniverseCheckPragma       Range
    -- ^ Applies to the following data/record type.
  | NotProjectionLikePragma     Range QName
    -- ^ Applies to the stated function
  | OverlapPragma             Range [QName] OverlapMode
    -- ^ Applies to the given name(s), which must be instance names
    -- (checked by the type checker).
  deriving 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

---------------------------------------------------------------------------

-- | Modules: Top-level pragmas plus other top-level declarations.

data Module = Mod
  { Module -> [Pragma]
modPragmas :: [Pragma]
  , Module -> [Declaration]
modDecls   :: [Declaration]
  }

-- | Splits off allowed (= import) declarations before the first
--   non-allowed declaration.
--   After successful parsing, the first non-allowed declaration
--   should be a module declaration.
spanAllowedBeforeModule :: [Declaration] -> ([Declaration], [Declaration])
spanAllowedBeforeModule :: [Declaration] -> ([Declaration], [Declaration])
spanAllowedBeforeModule = (Declaration -> Bool)
-> [Declaration] -> ([Declaration], [Declaration])
forall a. (a -> Bool) -> [a] -> ([a], [a])
span Declaration -> Bool
isAllowedBeforeModule
  where
    isAllowedBeforeModule :: Declaration -> Bool
isAllowedBeforeModule (Pragma OptionsPragma{}) = Bool
True
    isAllowedBeforeModule (Pragma BuiltinPragma{}) = Bool
True
    isAllowedBeforeModule (Private KwRange
_ Origin
_ [Declaration]
ds) = (Declaration -> Bool) -> [Declaration] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Declaration -> Bool
isAllowedBeforeModule [Declaration]
ds
    isAllowedBeforeModule Import{}       = Bool
True
    isAllowedBeforeModule ModuleMacro{}  = Bool
True
    isAllowedBeforeModule Open{}         = Bool
True
    isAllowedBeforeModule Declaration
_              = Bool
False

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

-- | Extended content of an interaction hole.
data HoleContent' qn nm p e
  = HoleContentExpr    e                       -- ^ @e@
  | HoleContentRewrite [RewriteEqn' qn nm p e] -- ^ @(rewrite | invert) e0 | ... | en@
  deriving ((forall a b.
 (a -> b) -> HoleContent' qn nm p a -> HoleContent' qn nm p b)
-> (forall a b.
    a -> HoleContent' qn nm p b -> HoleContent' qn nm p a)
-> Functor (HoleContent' qn nm p)
forall a b. a -> HoleContent' qn nm p b -> HoleContent' qn nm p a
forall a b.
(a -> b) -> HoleContent' qn nm p a -> HoleContent' qn nm p b
forall qn nm p a b.
a -> HoleContent' qn nm p b -> HoleContent' qn nm p a
forall qn nm p a b.
(a -> b) -> HoleContent' qn nm p a -> HoleContent' qn nm p b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall qn nm p a b.
(a -> b) -> HoleContent' qn nm p a -> HoleContent' qn nm p b
fmap :: forall a b.
(a -> b) -> HoleContent' qn nm p a -> HoleContent' qn nm p b
$c<$ :: forall qn nm p a b.
a -> HoleContent' qn nm p b -> HoleContent' qn nm p a
<$ :: forall a b. a -> HoleContent' qn nm p b -> HoleContent' qn nm p a
Functor, (forall m. Monoid m => HoleContent' qn nm p m -> m)
-> (forall m a.
    Monoid m =>
    (a -> m) -> HoleContent' qn nm p a -> m)
-> (forall m a.
    Monoid m =>
    (a -> m) -> HoleContent' qn nm p a -> m)
-> (forall a b. (a -> b -> b) -> b -> HoleContent' qn nm p a -> b)
-> (forall a b. (a -> b -> b) -> b -> HoleContent' qn nm p a -> b)
-> (forall b a. (b -> a -> b) -> b -> HoleContent' qn nm p a -> b)
-> (forall b a. (b -> a -> b) -> b -> HoleContent' qn nm p a -> b)
-> (forall a. (a -> a -> a) -> HoleContent' qn nm p a -> a)
-> (forall a. (a -> a -> a) -> HoleContent' qn nm p a -> a)
-> (forall a. HoleContent' qn nm p a -> [a])
-> (forall a. HoleContent' qn nm p a -> Bool)
-> (forall a. HoleContent' qn nm p a -> Int)
-> (forall a. Eq a => a -> HoleContent' qn nm p a -> Bool)
-> (forall a. Ord a => HoleContent' qn nm p a -> a)
-> (forall a. Ord a => HoleContent' qn nm p a -> a)
-> (forall a. Num a => HoleContent' qn nm p a -> a)
-> (forall a. Num a => HoleContent' qn nm p a -> a)
-> Foldable (HoleContent' qn nm p)
forall a. Eq a => a -> HoleContent' qn nm p a -> Bool
forall a. Num a => HoleContent' qn nm p a -> a
forall a. Ord a => HoleContent' qn nm p a -> a
forall m. Monoid m => HoleContent' qn nm p m -> m
forall a. HoleContent' qn nm p a -> Bool
forall a. HoleContent' qn nm p a -> Int
forall a. HoleContent' qn nm p a -> [a]
forall a. (a -> a -> a) -> HoleContent' qn nm p a -> a
forall m a. Monoid m => (a -> m) -> HoleContent' qn nm p a -> m
forall b a. (b -> a -> b) -> b -> HoleContent' qn nm p a -> b
forall a b. (a -> b -> b) -> b -> HoleContent' qn nm p a -> b
forall qn nm p a. Eq a => a -> HoleContent' qn nm p a -> Bool
forall qn nm p a. Num a => HoleContent' qn nm p a -> a
forall qn nm p a. Ord a => HoleContent' qn nm p a -> a
forall qn nm p m. Monoid m => HoleContent' qn nm p m -> m
forall qn nm p a. HoleContent' qn nm p a -> Bool
forall qn nm p a. HoleContent' qn nm p a -> Int
forall qn nm p a. HoleContent' qn nm p a -> [a]
forall qn nm p a. (a -> a -> a) -> HoleContent' qn nm p a -> a
forall qn nm p m a.
Monoid m =>
(a -> m) -> HoleContent' qn nm p a -> m
forall qn nm p b a.
(b -> a -> b) -> b -> HoleContent' qn nm p a -> b
forall qn nm p a b.
(a -> b -> b) -> b -> HoleContent' qn nm p 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 qn nm p m. Monoid m => HoleContent' qn nm p m -> m
fold :: forall m. Monoid m => HoleContent' qn nm p m -> m
$cfoldMap :: forall qn nm p m a.
Monoid m =>
(a -> m) -> HoleContent' qn nm p a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> HoleContent' qn nm p a -> m
$cfoldMap' :: forall qn nm p m a.
Monoid m =>
(a -> m) -> HoleContent' qn nm p a -> m
foldMap' :: forall m a. Monoid m => (a -> m) -> HoleContent' qn nm p a -> m
$cfoldr :: forall qn nm p a b.
(a -> b -> b) -> b -> HoleContent' qn nm p a -> b
foldr :: forall a b. (a -> b -> b) -> b -> HoleContent' qn nm p a -> b
$cfoldr' :: forall qn nm p a b.
(a -> b -> b) -> b -> HoleContent' qn nm p a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> HoleContent' qn nm p a -> b
$cfoldl :: forall qn nm p b a.
(b -> a -> b) -> b -> HoleContent' qn nm p a -> b
foldl :: forall b a. (b -> a -> b) -> b -> HoleContent' qn nm p a -> b
$cfoldl' :: forall qn nm p b a.
(b -> a -> b) -> b -> HoleContent' qn nm p a -> b
foldl' :: forall b a. (b -> a -> b) -> b -> HoleContent' qn nm p a -> b
$cfoldr1 :: forall qn nm p a. (a -> a -> a) -> HoleContent' qn nm p a -> a
foldr1 :: forall a. (a -> a -> a) -> HoleContent' qn nm p a -> a
$cfoldl1 :: forall qn nm p a. (a -> a -> a) -> HoleContent' qn nm p a -> a
foldl1 :: forall a. (a -> a -> a) -> HoleContent' qn nm p a -> a
$ctoList :: forall qn nm p a. HoleContent' qn nm p a -> [a]
toList :: forall a. HoleContent' qn nm p a -> [a]
$cnull :: forall qn nm p a. HoleContent' qn nm p a -> Bool
null :: forall a. HoleContent' qn nm p a -> Bool
$clength :: forall qn nm p a. HoleContent' qn nm p a -> Int
length :: forall a. HoleContent' qn nm p a -> Int
$celem :: forall qn nm p a. Eq a => a -> HoleContent' qn nm p a -> Bool
elem :: forall a. Eq a => a -> HoleContent' qn nm p a -> Bool
$cmaximum :: forall qn nm p a. Ord a => HoleContent' qn nm p a -> a
maximum :: forall a. Ord a => HoleContent' qn nm p a -> a
$cminimum :: forall qn nm p a. Ord a => HoleContent' qn nm p a -> a
minimum :: forall a. Ord a => HoleContent' qn nm p a -> a
$csum :: forall qn nm p a. Num a => HoleContent' qn nm p a -> a
sum :: forall a. Num a => HoleContent' qn nm p a -> a
$cproduct :: forall qn nm p a. Num a => HoleContent' qn nm p a -> a
product :: forall a. Num a => HoleContent' qn nm p a -> a
Foldable, Functor (HoleContent' qn nm p)
Foldable (HoleContent' qn nm p)
(Functor (HoleContent' qn nm p),
 Foldable (HoleContent' qn nm p)) =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> HoleContent' qn nm p a -> f (HoleContent' qn nm p b))
-> (forall (f :: * -> *) a.
    Applicative f =>
    HoleContent' qn nm p (f a) -> f (HoleContent' qn nm p a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> HoleContent' qn nm p a -> m (HoleContent' qn nm p b))
-> (forall (m :: * -> *) a.
    Monad m =>
    HoleContent' qn nm p (m a) -> m (HoleContent' qn nm p a))
-> Traversable (HoleContent' qn nm p)
forall qn nm p. Functor (HoleContent' qn nm p)
forall qn nm p. Foldable (HoleContent' qn nm p)
forall qn nm p (m :: * -> *) a.
Monad m =>
HoleContent' qn nm p (m a) -> m (HoleContent' qn nm p a)
forall qn nm p (f :: * -> *) a.
Applicative f =>
HoleContent' qn nm p (f a) -> f (HoleContent' qn nm p a)
forall qn nm p (m :: * -> *) a b.
Monad m =>
(a -> m b) -> HoleContent' qn nm p a -> m (HoleContent' qn nm p b)
forall qn nm p (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> HoleContent' qn nm p a -> f (HoleContent' qn nm p b)
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 =>
HoleContent' qn nm p (m a) -> m (HoleContent' qn nm p a)
forall (f :: * -> *) a.
Applicative f =>
HoleContent' qn nm p (f a) -> f (HoleContent' qn nm p a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> HoleContent' qn nm p a -> m (HoleContent' qn nm p b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> HoleContent' qn nm p a -> f (HoleContent' qn nm p b)
$ctraverse :: forall qn nm p (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> HoleContent' qn nm p a -> f (HoleContent' qn nm p b)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> HoleContent' qn nm p a -> f (HoleContent' qn nm p b)
$csequenceA :: forall qn nm p (f :: * -> *) a.
Applicative f =>
HoleContent' qn nm p (f a) -> f (HoleContent' qn nm p a)
sequenceA :: forall (f :: * -> *) a.
Applicative f =>
HoleContent' qn nm p (f a) -> f (HoleContent' qn nm p a)
$cmapM :: forall qn nm p (m :: * -> *) a b.
Monad m =>
(a -> m b) -> HoleContent' qn nm p a -> m (HoleContent' qn nm p b)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> HoleContent' qn nm p a -> m (HoleContent' qn nm p b)
$csequence :: forall qn nm p (m :: * -> *) a.
Monad m =>
HoleContent' qn nm p (m a) -> m (HoleContent' qn nm p a)
sequence :: forall (m :: * -> *) a.
Monad m =>
HoleContent' qn nm p (m a) -> m (HoleContent' qn nm p a)
Traversable)

type HoleContent = HoleContent' () Name Pattern Expr

---------------------------------------------------------------------------
-- * Smart constructors
---------------------------------------------------------------------------

rawApp :: List1 Expr -> Expr
rawApp :: List1 Expr -> Expr
rawApp es :: List1 Expr
es@(Expr
e1 :| Expr
e2 : [Expr]
rest) = Range -> List2 Expr -> Expr
RawApp (List1 Expr -> Range
forall a. HasRange a => a -> Range
getRange List1 Expr
es) (List2 Expr -> Expr) -> List2 Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Expr -> Expr -> [Expr] -> List2 Expr
forall a. a -> a -> [a] -> List2 a
List2 Expr
e1 Expr
e2 [Expr]
rest
rawApp (Expr
e :| []) = Expr
e

rawAppP :: List1 Pattern -> Pattern
rawAppP :: List1 Pattern -> Pattern
rawAppP ps :: List1 Pattern
ps@(Pattern
p1 :| Pattern
p2 : [Pattern]
rest) = Range -> List2 Pattern -> Pattern
RawAppP (List1 Pattern -> Range
forall a. HasRange a => a -> Range
getRange List1 Pattern
ps) (List2 Pattern -> Pattern) -> List2 Pattern -> Pattern
forall a b. (a -> b) -> a -> b
$ Pattern -> Pattern -> [Pattern] -> List2 Pattern
forall a. a -> a -> [a] -> List2 a
List2 Pattern
p1 Pattern
p2 [Pattern]
rest
rawAppP (Pattern
p :| []) = Pattern
p

{--------------------------------------------------------------------------
    Views
 --------------------------------------------------------------------------}

-- | The 'Expr' is not an application.
data AppView = AppView Expr [NamedArg Expr]

appView :: Expr -> AppView
appView :: Expr -> AppView
appView Expr
e = [NamedArg Expr] -> AppView
f (DList (NamedArg Expr) -> [NamedArg Expr]
forall a. DList a -> [a]
DL.toList DList (NamedArg Expr)
ess)
  where
    ([NamedArg Expr] -> AppView
f, DList (NamedArg Expr)
ess) = Expr -> ([NamedArg Expr] -> AppView, DList (NamedArg Expr))
appView' Expr
e

    appView' :: Expr -> ([NamedArg Expr] -> AppView, DList (NamedArg Expr))
    appView' :: Expr -> ([NamedArg Expr] -> AppView, DList (NamedArg Expr))
appView' = \case
      App Range
r Expr
e1 NamedArg Expr
e2      -> Expr -> ([NamedArg Expr] -> AppView, DList (NamedArg Expr))
appView' Expr
e1 ([NamedArg Expr] -> AppView, DList (NamedArg Expr))
-> (([NamedArg Expr] -> AppView, DList (NamedArg Expr))
    -> ([NamedArg Expr] -> AppView, DList (NamedArg Expr)))
-> ([NamedArg Expr] -> AppView, DList (NamedArg Expr))
forall a b. a -> (a -> b) -> b
& (DList (NamedArg Expr) -> DList (NamedArg Expr))
-> ([NamedArg Expr] -> AppView, DList (NamedArg Expr))
-> ([NamedArg Expr] -> AppView, DList (NamedArg Expr))
forall b c a. (b -> c) -> (a, b) -> (a, c)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second (DList (NamedArg Expr) -> NamedArg Expr -> DList (NamedArg Expr)
forall a. DList a -> a -> DList a
`DL.snoc` NamedArg Expr
e2)
      RawApp Range
_ (List2 Expr
e1 Expr
e2 [Expr]
es)
                       -> (Expr -> [NamedArg Expr] -> AppView
AppView Expr
e1, [NamedArg Expr] -> DList (NamedArg Expr)
forall a. [a] -> DList a
DL.fromList ((Expr -> NamedArg Expr) -> [Expr] -> [NamedArg Expr]
forall a b. (a -> b) -> [a] -> [b]
map Expr -> NamedArg Expr
arg (Expr
e2 Expr -> [Expr] -> [Expr]
forall a. a -> [a] -> [a]
: [Expr]
es)))
      Expr
e                -> (Expr -> [NamedArg Expr] -> AppView
AppView Expr
e, DList (NamedArg Expr)
forall a. Monoid a => a
mempty)

    arg :: Expr -> NamedArg Expr
arg (HiddenArg   Range
_ Named_ Expr
e) = NamedArg Expr -> NamedArg Expr
forall a. LensHiding a => a -> a
hide         (NamedArg Expr -> NamedArg Expr) -> NamedArg Expr -> NamedArg Expr
forall a b. (a -> b) -> a -> b
$ Named_ Expr -> NamedArg Expr
forall a. a -> Arg a
defaultArg Named_ Expr
e
    arg (InstanceArg Range
_ Named_ Expr
e) = NamedArg Expr -> NamedArg Expr
forall a. LensHiding a => a -> a
makeInstance (NamedArg Expr -> NamedArg Expr) -> NamedArg Expr -> NamedArg Expr
forall a b. (a -> b) -> a -> b
$ Named_ Expr -> NamedArg Expr
forall a. a -> Arg a
defaultArg Named_ Expr
e
    arg Expr
e                 = Named_ Expr -> NamedArg Expr
forall a. a -> Arg a
defaultArg (Expr -> Named_ Expr
forall a name. a -> Named name a
unnamed Expr
e)

unAppView :: AppView -> Expr
unAppView :: AppView -> Expr
unAppView (AppView Expr
e [NamedArg Expr]
nargs) = List1 Expr -> Expr
rawApp (Expr
e Expr -> [Expr] -> List1 Expr
forall a. a -> [a] -> NonEmpty a
:| (NamedArg Expr -> Expr) -> [NamedArg Expr] -> [Expr]
forall a b. (a -> b) -> [a] -> [b]
map NamedArg Expr -> Expr
unNamedArg [NamedArg Expr]
nargs)

  where
    unNamedArg :: NamedArg Expr -> Expr
unNamedArg NamedArg Expr
narg = ((Named_ Expr -> Expr) -> Named_ Expr -> Expr
forall a b. (a -> b) -> a -> b
$ NamedArg Expr -> Named_ Expr
forall e. Arg e -> e
unArg NamedArg Expr
narg) ((Named_ Expr -> Expr) -> Expr) -> (Named_ Expr -> Expr) -> Expr
forall a b. (a -> b) -> a -> b
$ case NamedArg Expr -> Hiding
forall a. LensHiding a => a -> Hiding
getHiding NamedArg Expr
narg of
      Hiding
Hidden     -> Range -> Named_ Expr -> Expr
HiddenArg (NamedArg Expr -> Range
forall a. HasRange a => a -> Range
getRange NamedArg Expr
narg)
      Hiding
NotHidden  -> Named_ Expr -> Expr
forall name a. Named name a -> a
namedThing
      Instance{} -> Range -> Named_ Expr -> Expr
InstanceArg (NamedArg Expr -> Range
forall a. HasRange a => a -> Range
getRange NamedArg Expr
narg)

isSingleIdentifierP :: Pattern -> Maybe Name
isSingleIdentifierP :: Pattern -> Maybe Name
isSingleIdentifierP = \case
  IdentP Bool
_ (QName Name
x) -> Name -> Maybe Name
forall a. a -> Maybe a
Just Name
x
  WildP Range
r            -> Name -> Maybe Name
forall a. a -> Maybe a
Just (Name -> Maybe Name) -> Name -> Maybe Name
forall a b. (a -> b) -> a -> b
$ Range -> Name
noName Range
r
  ParenP Range
_ Pattern
p         -> Pattern -> Maybe Name
isSingleIdentifierP Pattern
p
  Pattern
_                  -> Maybe Name
forall a. Maybe a
Nothing

removeParenP :: Pattern -> Pattern
removeParenP :: Pattern -> Pattern
removeParenP = \case
    ParenP Range
_ Pattern
p -> Pattern -> Pattern
removeParenP Pattern
p
    Pattern
p -> Pattern
p

-- | Observe the hiding status of an expression
observeHiding :: Expr -> WithHiding Expr
observeHiding :: Expr -> WithHiding Expr
observeHiding = \case
  HiddenArg Range
_   (Named Maybe (WithOrigin (Ranged String))
Nothing Expr
e) -> Hiding -> Expr -> WithHiding Expr
forall a. Hiding -> a -> WithHiding a
WithHiding Hiding
Hidden Expr
e
  InstanceArg Range
_ (Named Maybe (WithOrigin (Ranged String))
Nothing Expr
e) -> Hiding -> Expr -> WithHiding Expr
forall a. Hiding -> a -> WithHiding a
WithHiding (Overlappable -> Hiding
Instance Overlappable
NoOverlap) Expr
e
  Expr
e                               -> Hiding -> Expr -> WithHiding Expr
forall a. Hiding -> a -> WithHiding a
WithHiding Hiding
NotHidden Expr
e

-- | Observe the relevance status of an expression
observeRelevance :: Expr -> (Relevance, Expr)
observeRelevance :: Expr -> (Relevance, Expr)
observeRelevance = \case
  Dot Range
_ Expr
e       -> (Relevance
Irrelevant, Expr
e)
  DoubleDot Range
_ Expr
e -> (Relevance
NonStrict, Expr
e)
  Expr
e             -> (Relevance
Relevant, Expr
e)

-- | Observe various modifiers applied to an expression
observeModifiers :: Expr -> Arg Expr
observeModifiers :: Expr -> Arg Expr
observeModifiers Expr
e =
  let (Relevance
rel, WithHiding Hiding
hid Expr
e') = (Expr -> WithHiding Expr)
-> (Relevance, Expr) -> (Relevance, WithHiding Expr)
forall a b. (a -> b) -> (Relevance, a) -> (Relevance, b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Expr -> WithHiding Expr
observeHiding (Expr -> (Relevance, Expr)
observeRelevance Expr
e) in
  Relevance -> Arg Expr -> Arg Expr
forall a. LensRelevance a => Relevance -> a -> a
setRelevance Relevance
rel (Arg Expr -> Arg Expr) -> Arg Expr -> Arg Expr
forall a b. (a -> b) -> a -> b
$ Hiding -> Arg Expr -> Arg Expr
forall a. LensHiding a => Hiding -> a -> a
setHiding Hiding
hid (Arg Expr -> Arg Expr) -> Arg Expr -> Arg Expr
forall a b. (a -> b) -> a -> b
$ Expr -> Arg Expr
forall a. a -> Arg a
defaultArg Expr
e'

returnExpr :: Expr -> Maybe Expr
returnExpr :: Expr -> Maybe Expr
returnExpr (Pi Telescope1
_ Expr
e)        = Expr -> Maybe Expr
returnExpr Expr
e
returnExpr (Fun Range
_ Arg Expr
_  Expr
e)    = Expr -> Maybe Expr
returnExpr Expr
e
returnExpr (Let Range
_ List1 Declaration
_ Maybe Expr
e)     = Expr -> Maybe Expr
returnExpr (Expr -> Maybe Expr) -> Maybe Expr -> Maybe Expr
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Maybe Expr
e
returnExpr (Paren Range
_ Expr
e)     = Expr -> Maybe Expr
returnExpr Expr
e
returnExpr (Generalized Expr
e) = Expr -> Maybe Expr
returnExpr Expr
e
returnExpr Expr
e               = Expr -> Maybe Expr
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Expr
e

-- | Turn an expression into a pattern. Fails if the expression is not a
--   valid pattern.

isPattern :: Expr -> Maybe Pattern
isPattern :: Expr -> Maybe Pattern
isPattern = (Expr -> Maybe Pattern) -> Expr -> Maybe Pattern
forall (m :: * -> *).
Applicative m =>
(Expr -> m Pattern) -> Expr -> m Pattern
exprToPattern (Maybe Pattern -> Expr -> Maybe Pattern
forall a b. a -> b -> a
const Maybe Pattern
forall a. Maybe a
Nothing)

-- | Turn an expression into a pattern, turning non-pattern subexpressions into 'WildP'.

exprToPatternWithHoles :: Expr -> Pattern
exprToPatternWithHoles :: Expr -> Pattern
exprToPatternWithHoles = Identity Pattern -> Pattern
forall a. Identity a -> a
runIdentity (Identity Pattern -> Pattern)
-> (Expr -> Identity Pattern) -> Expr -> Pattern
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr -> Identity Pattern) -> Expr -> Identity Pattern
forall (m :: * -> *).
Applicative m =>
(Expr -> m Pattern) -> Expr -> m Pattern
exprToPattern (Pattern -> Identity Pattern
forall a. a -> Identity a
Identity (Pattern -> Identity Pattern)
-> (Expr -> Pattern) -> Expr -> Identity Pattern
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Range -> Pattern
WildP (Range -> Pattern) -> (Expr -> Range) -> Expr -> Pattern
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> Range
forall a. HasRange a => a -> Range
getRange)

-- | Generic expression to pattern conversion.

exprToPattern :: Applicative m
  => (Expr -> m Pattern)  -- ^ Default result for non-pattern things.
  -> Expr                 -- ^ The expression to translate.
  -> m Pattern            -- ^ The translated pattern (maybe).
exprToPattern :: forall (m :: * -> *).
Applicative m =>
(Expr -> m Pattern) -> Expr -> m Pattern
exprToPattern Expr -> m Pattern
fallback = Expr -> m Pattern
loop
  where
  loop :: Expr -> m Pattern
loop = \case
    Ident       QName
x        -> Pattern -> m Pattern
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Pattern -> m Pattern) -> Pattern -> m Pattern
forall a b. (a -> b) -> a -> b
$ Bool -> QName -> Pattern
IdentP Bool
True QName
x
    App         Range
_ Expr
e1 NamedArg Expr
e2  -> Pattern -> NamedArg Pattern -> Pattern
AppP (Pattern -> NamedArg Pattern -> Pattern)
-> m Pattern -> m (NamedArg Pattern -> Pattern)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> m Pattern
loop Expr
e1 m (NamedArg Pattern -> Pattern)
-> m (NamedArg Pattern) -> m Pattern
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Named_ Expr -> m (Named_ Pattern))
-> NamedArg Expr -> m (NamedArg Pattern)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Arg a -> f (Arg b)
traverse ((Expr -> m Pattern) -> Named_ Expr -> m (Named_ Pattern)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b)
-> Named (WithOrigin (Ranged String)) a
-> f (Named (WithOrigin (Ranged String)) b)
traverse Expr -> m Pattern
loop) NamedArg Expr
e2
    Paren       Range
r Expr
e      -> Range -> Pattern -> Pattern
ParenP Range
r (Pattern -> Pattern) -> m Pattern -> m Pattern
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> m Pattern
loop Expr
e
    Underscore  Range
r Maybe String
_      -> Pattern -> m Pattern
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Pattern -> m Pattern) -> Pattern -> m Pattern
forall a b. (a -> b) -> a -> b
$ Range -> Pattern
WildP Range
r
    Absurd      Range
r        -> Pattern -> m Pattern
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Pattern -> m Pattern) -> Pattern -> m Pattern
forall a b. (a -> b) -> a -> b
$ Range -> Pattern
AbsurdP Range
r
    As          Range
r Name
x Expr
e    -> Range -> (Pattern -> Pattern) -> Pattern -> Pattern
pushUnderBracesP Range
r (Range -> Name -> Pattern -> Pattern
AsP Range
r Name
x) (Pattern -> Pattern) -> m Pattern -> m Pattern
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> m Pattern
loop Expr
e
    Dot         Range
r Expr
e      -> Pattern -> m Pattern
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Pattern -> m Pattern) -> Pattern -> m Pattern
forall a b. (a -> b) -> a -> b
$ Range -> (Expr -> Pattern) -> Expr -> Pattern
pushUnderBracesE Range
r (Range -> Expr -> Pattern
DotP Range
r) Expr
e
    -- Wen, 2020-08-27: We disallow Float patterns, since equality for floating
    -- point numbers is not stable across architectures and with different
    -- compiler flags.
    e :: Expr
e@(Lit Range
_ LitFloat{}) -> Expr -> m Pattern
fallback Expr
e
    Lit         Range
r Literal
l      -> Pattern -> m Pattern
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Pattern -> m Pattern) -> Pattern -> m Pattern
forall a b. (a -> b) -> a -> b
$ Range -> Literal -> Pattern
LitP Range
r Literal
l
    HiddenArg   Range
r Named_ Expr
e      -> Range -> Named_ Pattern -> Pattern
HiddenP   Range
r (Named_ Pattern -> Pattern) -> m (Named_ Pattern) -> m Pattern
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr -> m Pattern) -> Named_ Expr -> m (Named_ Pattern)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b)
-> Named (WithOrigin (Ranged String)) a
-> f (Named (WithOrigin (Ranged String)) b)
traverse Expr -> m Pattern
loop Named_ Expr
e
    InstanceArg Range
r Named_ Expr
e      -> Range -> Named_ Pattern -> Pattern
InstanceP Range
r (Named_ Pattern -> Pattern) -> m (Named_ Pattern) -> m Pattern
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr -> m Pattern) -> Named_ Expr -> m (Named_ Pattern)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b)
-> Named (WithOrigin (Ranged String)) a
-> f (Named (WithOrigin (Ranged String)) b)
traverse Expr -> m Pattern
loop Named_ Expr
e
    RawApp      Range
r List2 Expr
es     -> Range -> List2 Pattern -> Pattern
RawAppP   Range
r (List2 Pattern -> Pattern) -> m (List2 Pattern) -> m Pattern
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr -> m Pattern) -> List2 Expr -> m (List2 Pattern)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> List2 a -> f (List2 b)
traverse Expr -> m Pattern
loop List2 Expr
es
    Quote       Range
r        -> Pattern -> m Pattern
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Pattern -> m Pattern) -> Pattern -> m Pattern
forall a b. (a -> b) -> a -> b
$ Range -> Pattern
QuoteP Range
r
    Equal       Range
r Expr
e1 Expr
e2  -> Pattern -> m Pattern
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Pattern -> m Pattern) -> Pattern -> m Pattern
forall a b. (a -> b) -> a -> b
$ Range -> [(Expr, Expr)] -> Pattern
EqualP Range
r [(Expr
e1, Expr
e2)]
    Ellipsis    Range
r        -> Pattern -> m Pattern
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Pattern -> m Pattern) -> Pattern -> m Pattern
forall a b. (a -> b) -> a -> b
$ Range -> Maybe Pattern -> Pattern
EllipsisP Range
r Maybe Pattern
forall a. Maybe a
Nothing
    e :: Expr
e@(Rec Range
r RecordAssignments
es)
        -- We cannot translate record expressions with module parts.
      | Just [FieldAssignment]
fs <- (Either FieldAssignment ModuleAssignment -> Maybe FieldAssignment)
-> RecordAssignments -> Maybe [FieldAssignment]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Either FieldAssignment ModuleAssignment -> Maybe FieldAssignment
forall a b. Either a b -> Maybe a
maybeLeft RecordAssignments
es -> Range -> [FieldAssignment' Pattern] -> Pattern
RecP Range
r ([FieldAssignment' Pattern] -> Pattern)
-> m [FieldAssignment' Pattern] -> m Pattern
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (FieldAssignment -> m (FieldAssignment' Pattern))
-> [FieldAssignment] -> m [FieldAssignment' Pattern]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse ((Expr -> m Pattern)
-> FieldAssignment -> m (FieldAssignment' Pattern)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> FieldAssignment' a -> f (FieldAssignment' b)
traverse Expr -> m Pattern
loop) [FieldAssignment]
fs
      | Bool
otherwise -> Expr -> m Pattern
fallback Expr
e
    -- WithApp has already lost the range information of the bars '|'
    WithApp     Range
r Expr
e [Expr]
es   -> do -- ApplicativeDo
      Pattern
p  <- Expr -> m Pattern
loop Expr
e
      [NamedArg Pattern]
ps <- [Expr] -> (Expr -> m (NamedArg Pattern)) -> m [NamedArg Pattern]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
forA [Expr]
es ((Expr -> m (NamedArg Pattern)) -> m [NamedArg Pattern])
-> (Expr -> m (NamedArg Pattern)) -> m [NamedArg Pattern]
forall a b. (a -> b) -> a -> b
$ \ Expr
e -> do -- ApplicativeDo
        Pattern
p <- Expr -> m Pattern
loop Expr
e
        pure $ Pattern -> NamedArg Pattern
forall a. a -> NamedArg a
defaultNamedArg (Pattern -> NamedArg Pattern) -> Pattern -> NamedArg Pattern
forall a b. (a -> b) -> a -> b
$ Range -> Pattern -> Pattern
WithP (Expr -> Range
forall a. HasRange a => a -> Range
getRange Expr
e) Pattern
p   -- TODO #2822: Range!
      pure $ (Pattern -> NamedArg Pattern -> Pattern)
-> Pattern -> [NamedArg Pattern] -> Pattern
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Pattern -> NamedArg Pattern -> Pattern
AppP Pattern
p [NamedArg Pattern]
ps
    Expr
e -> Expr -> m Pattern
fallback Expr
e

  pushUnderBracesP :: Range -> (Pattern -> Pattern) -> (Pattern -> Pattern)
  pushUnderBracesP :: Range -> (Pattern -> Pattern) -> Pattern -> Pattern
pushUnderBracesP Range
r Pattern -> Pattern
f = \case
    HiddenP   Range
_ Named_ Pattern
p   -> Range -> Named_ Pattern -> Pattern
HiddenP   Range
r (Named_ Pattern -> Pattern) -> Named_ Pattern -> Pattern
forall a b. (a -> b) -> a -> b
$ (Pattern -> Pattern) -> Named_ Pattern -> Named_ Pattern
forall a b.
(a -> b)
-> Named (WithOrigin (Ranged String)) a
-> Named (WithOrigin (Ranged String)) b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Pattern -> Pattern
f Named_ Pattern
p
    InstanceP Range
_ Named_ Pattern
p   -> Range -> Named_ Pattern -> Pattern
InstanceP Range
r (Named_ Pattern -> Pattern) -> Named_ Pattern -> Pattern
forall a b. (a -> b) -> a -> b
$ (Pattern -> Pattern) -> Named_ Pattern -> Named_ Pattern
forall a b.
(a -> b)
-> Named (WithOrigin (Ranged String)) a
-> Named (WithOrigin (Ranged String)) b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Pattern -> Pattern
f Named_ Pattern
p
    Pattern
p               -> Pattern -> Pattern
f Pattern
p

  pushUnderBracesE :: Range -> (Expr -> Pattern) -> (Expr -> Pattern)
  pushUnderBracesE :: Range -> (Expr -> Pattern) -> Expr -> Pattern
pushUnderBracesE Range
r Expr -> Pattern
f = \case
    HiddenArg   Range
_ Named_ Expr
p -> Range -> Named_ Pattern -> Pattern
HiddenP   Range
r (Named_ Pattern -> Pattern) -> Named_ Pattern -> Pattern
forall a b. (a -> b) -> a -> b
$ (Expr -> Pattern) -> Named_ Expr -> Named_ Pattern
forall a b.
(a -> b)
-> Named (WithOrigin (Ranged String)) a
-> Named (WithOrigin (Ranged String)) b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Expr -> Pattern
f Named_ Expr
p
    InstanceArg Range
_ Named_ Expr
p -> Range -> Named_ Pattern -> Pattern
InstanceP Range
r (Named_ Pattern -> Pattern) -> Named_ Pattern -> Pattern
forall a b. (a -> b) -> a -> b
$ (Expr -> Pattern) -> Named_ Expr -> Named_ Pattern
forall a b.
(a -> b)
-> Named (WithOrigin (Ranged String)) a
-> Named (WithOrigin (Ranged String)) b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Expr -> Pattern
f Named_ Expr
p
    Expr
p               -> Expr -> Pattern
f Expr
p

isAbsurdP :: Pattern -> Maybe (Range, Hiding)
isAbsurdP :: Pattern -> Maybe (Range, Hiding)
isAbsurdP = \case
  AbsurdP Range
r      -> (Range, Hiding) -> Maybe (Range, Hiding)
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Range
r, Hiding
NotHidden)
  AsP Range
_ Name
_      Pattern
p -> Pattern -> Maybe (Range, Hiding)
isAbsurdP Pattern
p
  ParenP Range
_     Pattern
p -> Pattern -> Maybe (Range, Hiding)
isAbsurdP Pattern
p
  HiddenP   Range
_ Named_ Pattern
np -> (Hiding
Hidden Hiding -> (Range, Hiding) -> (Range, Hiding)
forall a b. a -> (Range, b) -> (Range, a)
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$)              ((Range, Hiding) -> (Range, Hiding))
-> Maybe (Range, Hiding) -> Maybe (Range, Hiding)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Pattern -> Maybe (Range, Hiding)
isAbsurdP (Named_ Pattern -> Pattern
forall name a. Named name a -> a
namedThing Named_ Pattern
np)
  InstanceP Range
_ Named_ Pattern
np -> (Overlappable -> Hiding
Instance Overlappable
YesOverlap Hiding -> (Range, Hiding) -> (Range, Hiding)
forall a b. a -> (Range, b) -> (Range, a)
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$) ((Range, Hiding) -> (Range, Hiding))
-> Maybe (Range, Hiding) -> Maybe (Range, Hiding)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Pattern -> Maybe (Range, Hiding)
isAbsurdP (Named_ Pattern -> Pattern
forall name a. Named name a -> a
namedThing Named_ Pattern
np)
  Pattern
_ -> Maybe (Range, Hiding)
forall a. Maybe a
Nothing

isBinderP :: Pattern -> Maybe Binder
isBinderP :: Pattern -> Maybe Binder
isBinderP = \case
  IdentP Bool
_ QName
qn
             -> Name -> Binder
mkBinder_ (Name -> Binder) -> Maybe Name -> Maybe Binder
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> Maybe Name
isUnqualified QName
qn
  WildP Range
r    -> Binder -> Maybe Binder
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Binder -> Maybe Binder) -> Binder -> Maybe Binder
forall a b. (a -> b) -> a -> b
$ Name -> Binder
mkBinder_ (Name -> Binder) -> Name -> Binder
forall a b. (a -> b) -> a -> b
$ Range -> Name -> Name
forall a. SetRange a => Range -> a -> a
setRange Range
r Name
simpleHole
  AsP Range
r Name
n Pattern
p  -> Binder -> Maybe Binder
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Binder -> Maybe Binder) -> Binder -> Maybe Binder
forall a b. (a -> b) -> a -> b
$ Maybe Pattern -> BoundName -> Binder
forall a. Maybe Pattern -> a -> Binder' a
Binder (Pattern -> Maybe Pattern
forall a. a -> Maybe a
Just Pattern
p) (BoundName -> Binder) -> BoundName -> Binder
forall a b. (a -> b) -> a -> b
$ Name -> BoundName
mkBoundName_ Name
n
  ParenP Range
r Pattern
p -> Binder -> Maybe Binder
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Binder -> Maybe Binder) -> Binder -> Maybe Binder
forall a b. (a -> b) -> a -> b
$ Maybe Pattern -> BoundName -> Binder
forall a. Maybe Pattern -> a -> Binder' a
Binder (Pattern -> Maybe Pattern
forall a. a -> Maybe a
Just Pattern
p) (BoundName -> Binder) -> BoundName -> Binder
forall a b. (a -> b) -> a -> b
$ Name -> BoundName
mkBoundName_ (Name -> BoundName) -> Name -> BoundName
forall a b. (a -> b) -> a -> b
$ Range -> Name -> Name
forall a. SetRange a => Range -> a -> a
setRange Range
r Name
simpleHole
  Pattern
_ -> Maybe Binder
forall a. Maybe a
Nothing

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

-- Null
------------------------------------------------------------------------

-- | A 'WhereClause' is 'null' when the @where@ keyword is absent.
--   An empty list of declarations does not count as 'null' here.

instance Null (WhereClause' a) where
  empty :: WhereClause' a
empty = WhereClause' a
forall a. WhereClause' a
NoWhere
  null :: WhereClause' a -> Bool
null WhereClause' a
NoWhere = Bool
True
  null AnyWhere{} = Bool
False
  null SomeWhere{} = Bool
False

-- Lenses
------------------------------------------------------------------------

instance LensHiding LamBinding where
  getHiding :: LamBinding -> Hiding
getHiding   (DomainFree NamedArg Binder
x) = NamedArg Binder -> Hiding
forall a. LensHiding a => a -> Hiding
getHiding NamedArg Binder
x
  getHiding   (DomainFull TypedBinding' Expr
a) = TypedBinding' Expr -> Hiding
forall a. LensHiding a => a -> Hiding
getHiding TypedBinding' Expr
a
  mapHiding :: (Hiding -> Hiding) -> LamBinding -> LamBinding
mapHiding Hiding -> Hiding
f (DomainFree NamedArg Binder
x) = NamedArg Binder -> LamBinding
forall a. NamedArg Binder -> LamBinding' a
DomainFree (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' Expr
a) = TypedBinding' Expr -> LamBinding
forall a. a -> LamBinding' a
DomainFull (TypedBinding' Expr -> LamBinding)
-> TypedBinding' Expr -> LamBinding
forall a b. (a -> b) -> a -> b
$ (Hiding -> Hiding) -> TypedBinding' Expr -> TypedBinding' Expr
forall a. LensHiding a => (Hiding -> Hiding) -> a -> a
mapHiding Hiding -> Hiding
f TypedBinding' Expr
a

instance LensHiding TypedBinding where
  getHiding :: TypedBinding' Expr -> Hiding
getHiding (TBind Range
_ (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' Expr -> TypedBinding' Expr
mapHiding Hiding -> Hiding
f (TBind Range
r List1 (NamedArg Binder)
xs Expr
e) = Range -> List1 (NamedArg Binder) -> Expr -> TypedBinding' Expr
forall e. Range -> List1 (NamedArg Binder) -> e -> TypedBinding' e
TBind Range
r ((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 ((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' Expr
b@TLet{}       = TypedBinding' Expr
b

instance LensRelevance TypedBinding where
  getRelevance :: TypedBinding' Expr -> Relevance
getRelevance (TBind Range
_ (NamedArg Binder
x :| [NamedArg Binder]
_) Expr
_) = NamedArg Binder -> Relevance
forall a. LensRelevance a => a -> Relevance
getRelevance NamedArg Binder
x   -- Slightly dubious
  getRelevance TLet{}               = Relevance
unitRelevance
  mapRelevance :: (Relevance -> Relevance)
-> TypedBinding' Expr -> TypedBinding' Expr
mapRelevance Relevance -> Relevance
f (TBind Range
r List1 (NamedArg Binder)
xs Expr
e) = Range -> List1 (NamedArg Binder) -> Expr -> TypedBinding' Expr
forall e. Range -> List1 (NamedArg Binder) -> e -> TypedBinding' e
TBind Range
r ((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 ((Relevance -> Relevance) -> NamedArg Binder -> NamedArg Binder
forall a. LensRelevance a => (Relevance -> Relevance) -> a -> a
mapRelevance Relevance -> Relevance
f) List1 (NamedArg Binder)
xs) Expr
e
  mapRelevance Relevance -> Relevance
f b :: TypedBinding' Expr
b@TLet{}       = TypedBinding' Expr
b

-- HasRange instances
------------------------------------------------------------------------

instance HasRange e => HasRange (OpApp e) where
  getRange :: OpApp e -> Range
getRange = \case
    Ordinary e
e -> e -> Range
forall a. HasRange a => a -> Range
getRange e
e
    SyntaxBindingLambda Range
r List1 LamBinding
_ e
_ -> Range
r

instance HasRange Expr where
  getRange :: Expr -> Range
getRange = \case
      Ident QName
x            -> QName -> Range
forall a. HasRange a => a -> Range
getRange QName
x
      Lit Range
r Literal
_            -> Range
r
      QuestionMark Range
r Maybe Int
_   -> Range
r
      Underscore Range
r Maybe String
_     -> Range
r
      App Range
r Expr
_ NamedArg Expr
_          -> Range
r
      RawApp Range
r List2 Expr
_         -> Range
r
      OpApp Range
r QName
_ Set Name
_ OpAppArgs
_      -> Range
r
      WithApp Range
r Expr
_ [Expr]
_      -> Range
r
      Lam Range
r List1 LamBinding
_ Expr
_          -> Range
r
      AbsurdLam Range
r Hiding
_      -> Range
r
      ExtendedLam Range
r Erased
_ List1 LamClause
_  -> Range
r
      Fun Range
r Arg Expr
_ Expr
_          -> Range
r
      Pi Telescope1
b Expr
e             -> Telescope1 -> Expr -> Range
forall u t. (HasRange u, HasRange t) => u -> t -> Range
fuseRange Telescope1
b Expr
e
      Let Range
r List1 Declaration
_ Maybe Expr
_          -> Range
r
      Paren Range
r Expr
_          -> Range
r
      IdiomBrackets Range
r [Expr]
_  -> Range
r
      DoBlock Range
r List1 DoStmt
_        -> Range
r
      As Range
r Name
_ Expr
_           -> Range
r
      Dot Range
r Expr
_            -> Range
r
      DoubleDot Range
r Expr
_      -> Range
r
      Absurd Range
r           -> Range
r
      HiddenArg Range
r Named_ Expr
_      -> Range
r
      InstanceArg Range
r Named_ Expr
_    -> Range
r
      Rec Range
r RecordAssignments
_            -> Range
r
      RecUpdate Range
r Expr
_ [FieldAssignment]
_    -> Range
r
      Quote Range
r            -> Range
r
      QuoteTerm Range
r        -> Range
r
      Unquote Range
r          -> Range
r
      Tactic Range
r Expr
_         -> Range
r
      DontCare{}         -> Range
forall a. Range' a
noRange
      Equal Range
r Expr
_ Expr
_        -> Range
r
      Ellipsis Range
r         -> Range
r
      Generalized Expr
e      -> Expr -> Range
forall a. HasRange a => a -> Range
getRange Expr
e
      KnownIdent NameKind
_ QName
q     -> QName -> Range
forall a. HasRange a => a -> Range
getRange QName
q
      KnownOpApp NameKind
_ Range
r QName
_ Set Name
_ OpAppArgs
_ -> Range
r

-- instance HasRange Telescope where
--     getRange (TeleBind bs) = getRange bs
--     getRange (TeleFun x y) = fuseRange x y

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

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

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

instance HasRange BoundName where
  getRange :: BoundName -> Range
getRange = Name -> Range
forall a. HasRange a => a -> Range
getRange (Name -> Range) -> (BoundName -> Name) -> BoundName -> Range
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BoundName -> Name
boundName

instance HasRange WhereClause where
  getRange :: WhereClause -> Range
getRange  WhereClause
NoWhere               = Range
forall a. Range' a
noRange
  getRange (AnyWhere Range
r [Declaration]
ds)        = (Range, [Declaration]) -> Range
forall a. HasRange a => a -> Range
getRange (Range
r, [Declaration]
ds)
  getRange (SomeWhere Range
r Erased
e Name
x Access
_ [Declaration]
ds) = (Range, Erased, Name, [Declaration]) -> Range
forall a. HasRange a => a -> Range
getRange (Range
r, Erased
e, Name
x, [Declaration]
ds)

instance HasRange ModuleApplication where
  getRange :: ModuleApplication -> Range
getRange (SectionApp Range
r Telescope
_ Expr
_) = Range
r
  getRange (RecordModuleInstance Range
r QName
_) = Range
r

instance HasRange a => HasRange (FieldAssignment' a) where
  getRange :: FieldAssignment' a -> Range
getRange (FieldAssignment Name
a a
b) = Name -> a -> Range
forall u t. (HasRange u, HasRange t) => u -> t -> Range
fuseRange Name
a a
b

instance HasRange ModuleAssignment where
  getRange :: ModuleAssignment -> Range
getRange (ModuleAssignment QName
a [Expr]
b ImportDirective
c) = QName -> [Expr] -> Range
forall u t. (HasRange u, HasRange t) => u -> t -> Range
fuseRange QName
a [Expr]
b Range -> ImportDirective -> Range
forall u t. (HasRange u, HasRange t) => u -> t -> Range
`fuseRange` ImportDirective
c

instance HasRange RecordDirective where
  getRange :: RecordDirective -> Range
getRange (Induction Ranged Induction
a)          = Ranged Induction -> Range
forall a. HasRange a => a -> Range
getRange Ranged Induction
a
  getRange (Eta Ranged HasEta0
a    )            = Ranged HasEta0 -> Range
forall a. HasRange a => a -> Range
getRange Ranged HasEta0
a
  getRange (Constructor Name
a IsInstance
b)      = (Name, IsInstance) -> Range
forall a. HasRange a => a -> Range
getRange (Name
a, IsInstance
b)
  getRange (PatternOrCopattern Range
r) = Range
r

instance HasRange Declaration where
  getRange :: Declaration -> Range
getRange (TypeSig ArgInfo
_ TacticAttribute
_ Name
x Expr
t)       = Name -> Expr -> Range
forall u t. (HasRange u, HasRange t) => u -> t -> Range
fuseRange Name
x Expr
t
  getRange (FieldSig IsInstance
_ TacticAttribute
_ Name
x Arg Expr
t)      = Name -> Arg Expr -> Range
forall u t. (HasRange u, HasRange t) => u -> t -> Range
fuseRange Name
x Arg Expr
t
  getRange (Field KwRange
kwr [Declaration]
ds)          = KwRange -> [Declaration] -> Range
forall u t. (HasRange u, HasRange t) => u -> t -> Range
fuseRange KwRange
kwr [Declaration]
ds
  getRange (FunClause LHS
lhs RHS
rhs WhereClause
wh Bool
_) = LHS -> RHS -> Range
forall u t. (HasRange u, HasRange t) => u -> t -> Range
fuseRange LHS
lhs RHS
rhs Range -> WhereClause -> Range
forall u t. (HasRange u, HasRange t) => u -> t -> Range
`fuseRange` WhereClause
wh
  getRange (DataSig Range
r Erased
_ Name
_ [LamBinding]
_ Expr
_)     = Range
r
  getRange (Data Range
r Erased
_ Name
_ [LamBinding]
_ Expr
_ [Declaration]
_)      = Range
r
  getRange (DataDef Range
r Name
_ [LamBinding]
_ [Declaration]
_)       = Range
r
  getRange (RecordSig Range
r Erased
_ Name
_ [LamBinding]
_ Expr
_)   = Range
r
  getRange (RecordDef Range
r Name
_ [RecordDirective]
_ [LamBinding]
_ [Declaration]
_)   = Range
r
  getRange (Record Range
r Erased
_ Name
_ [RecordDirective]
_ [LamBinding]
_ Expr
_ [Declaration]
_)  = Range
r
  getRange (Mutual KwRange
kwr [Declaration]
ds)         = KwRange -> [Declaration] -> Range
forall u t. (HasRange u, HasRange t) => u -> t -> Range
fuseRange KwRange
kwr [Declaration]
ds
  getRange (InterleavedMutual KwRange
kwr [Declaration]
ds) = KwRange -> [Declaration] -> Range
forall u t. (HasRange u, HasRange t) => u -> t -> Range
fuseRange KwRange
kwr [Declaration]
ds
  getRange (LoneConstructor KwRange
kwr [Declaration]
ds)= KwRange -> [Declaration] -> Range
forall u t. (HasRange u, HasRange t) => u -> t -> Range
fuseRange KwRange
kwr [Declaration]
ds
  getRange (Abstract KwRange
kwr [Declaration]
ds)       = KwRange -> [Declaration] -> Range
forall u t. (HasRange u, HasRange t) => u -> t -> Range
fuseRange KwRange
kwr [Declaration]
ds
  getRange (Generalize KwRange
kwr [Declaration]
ds)     = KwRange -> [Declaration] -> Range
forall u t. (HasRange u, HasRange t) => u -> t -> Range
fuseRange KwRange
kwr [Declaration]
ds
  getRange (Open Range
r QName
_ ImportDirective
_)            = Range
r
  getRange (ModuleMacro Range
r Erased
_ Name
_ ModuleApplication
_ OpenShortHand
_ ImportDirective
_)
                                   = Range
r
  getRange (Import Range
r QName
_ Maybe AsName
_ OpenShortHand
_ ImportDirective
_)      = Range
r
  getRange (InstanceB KwRange
kwr [Declaration]
_)       = KwRange -> Range
forall a. HasRange a => a -> Range
getRange KwRange
kwr
  getRange (Macro KwRange
kwr [Declaration]
ds)          = KwRange -> [Declaration] -> Range
forall u t. (HasRange u, HasRange t) => u -> t -> Range
fuseRange KwRange
kwr [Declaration]
ds
  getRange (Private KwRange
kwr Origin
_ [Declaration]
ds)      = KwRange -> [Declaration] -> Range
forall u t. (HasRange u, HasRange t) => u -> t -> Range
fuseRange KwRange
kwr [Declaration]
ds
  getRange (Postulate KwRange
kwr [Declaration]
ds)      = KwRange -> [Declaration] -> Range
forall u t. (HasRange u, HasRange t) => u -> t -> Range
fuseRange KwRange
kwr [Declaration]
ds
  getRange (Primitive KwRange
kwr [Declaration]
ds)      = KwRange -> [Declaration] -> Range
forall u t. (HasRange u, HasRange t) => u -> t -> Range
fuseRange KwRange
kwr [Declaration]
ds
  getRange (Module Range
r Erased
_ QName
_ Telescope
_ [Declaration]
_)      = Range
r
  getRange (Infix Fixity
f List1 Name
_)             = Fixity -> Range
forall a. HasRange a => a -> Range
getRange Fixity
f
  getRange (Syntax Name
n Notation
_)            = Name -> Range
forall a. HasRange a => a -> Range
getRange Name
n
  getRange (PatternSyn Range
r Name
_ [WithHiding Name]
_ Pattern
_)    = Range
r
  getRange (UnquoteDecl Range
r [Name]
_ Expr
_)     = Range
r
  getRange (UnquoteDef Range
r [Name]
_ Expr
_)      = Range
r
  getRange (UnquoteData Range
r Name
_ [Name]
_ Expr
_)   = Range
r
  getRange (Pragma Pragma
p)              = Pragma -> Range
forall a. HasRange a => a -> Range
getRange Pragma
p
  getRange (Opaque KwRange
kwr [Declaration]
ds)         = KwRange -> [Declaration] -> Range
forall u t. (HasRange u, HasRange t) => u -> t -> Range
fuseRange KwRange
kwr [Declaration]
ds
  getRange (Unfolding KwRange
kwr [QName]
ds)      = KwRange -> [QName] -> Range
forall u t. (HasRange u, HasRange t) => u -> t -> Range
fuseRange KwRange
kwr [QName]
ds

instance HasRange LHS where
  getRange :: LHS -> Range
getRange (LHS Pattern
p [RewriteEqn]
eqns [WithExpr]
ws) = Pattern
p Pattern -> [RewriteEqn] -> Range
forall u t. (HasRange u, HasRange t) => u -> t -> Range
`fuseRange` [RewriteEqn]
eqns Range -> [WithExpr] -> Range
forall u t. (HasRange u, HasRange t) => u -> t -> Range
`fuseRange` [WithExpr]
ws

instance HasRange LHSCore where
  getRange :: LHSCore -> Range
getRange (LHSHead QName
f [NamedArg Pattern]
ps)              = QName -> [NamedArg Pattern] -> Range
forall u t. (HasRange u, HasRange t) => u -> t -> Range
fuseRange QName
f [NamedArg Pattern]
ps
  getRange (LHSProj QName
d [NamedArg Pattern]
ps1 NamedArg LHSCore
lhscore [NamedArg Pattern]
ps2) = QName
d QName -> [NamedArg Pattern] -> Range
forall u t. (HasRange u, HasRange t) => u -> t -> Range
`fuseRange` [NamedArg Pattern]
ps1 Range -> NamedArg LHSCore -> Range
forall u t. (HasRange u, HasRange t) => u -> t -> Range
`fuseRange` NamedArg LHSCore
lhscore Range -> [NamedArg Pattern] -> Range
forall u t. (HasRange u, HasRange t) => u -> t -> Range
`fuseRange` [NamedArg Pattern]
ps2
  getRange (LHSWith LHSCore
f [Pattern]
wps [NamedArg Pattern]
ps)          = LHSCore
f LHSCore -> [Pattern] -> Range
forall u t. (HasRange u, HasRange t) => u -> t -> Range
`fuseRange` [Pattern]
wps Range -> [NamedArg Pattern] -> Range
forall u t. (HasRange u, HasRange t) => u -> t -> Range
`fuseRange` [NamedArg Pattern]
ps
  getRange (LHSEllipsis Range
r LHSCore
p)           = Range
r

instance HasRange RHS where
  getRange :: RHS -> Range
getRange RHS
AbsurdRHS = Range
forall a. Range' a
noRange
  getRange (RHS Expr
e)   = Expr -> Range
forall a. HasRange a => a -> Range
getRange Expr
e

instance HasRange LamClause where
  getRange :: LamClause -> Range
getRange (LamClause [Pattern]
lhs RHS
rhs Bool
_) = ([Pattern], RHS) -> Range
forall a. HasRange a => a -> Range
getRange ([Pattern]
lhs, RHS
rhs)

instance HasRange DoStmt where
  getRange :: DoStmt -> Range
getRange (DoBind Range
r Pattern
_ Expr
_ [LamClause]
_) = Range
r
  getRange (DoThen Expr
e)       = Expr -> Range
forall a. HasRange a => a -> Range
getRange Expr
e
  getRange (DoLet Range
r List1 Declaration
_)      = Range
r

instance HasRange Pragma where
  getRange :: Pragma -> Range
getRange (OptionsPragma Range
r [String]
_)               = Range
r
  getRange (BuiltinPragma Range
r Ranged String
_ QName
_)             = Range
r
  getRange (RewritePragma Range
r Range
_ [QName]
_)             = Range
r
  getRange (CompilePragma Range
r Ranged String
_ QName
_ String
_)           = Range
r
  getRange (ForeignPragma Range
r Ranged String
_ String
_)             = Range
r
  getRange (StaticPragma Range
r QName
_)                = Range
r
  getRange (InjectivePragma Range
r QName
_)             = Range
r
  getRange (InjectiveForInferencePragma Range
r QName
_) = Range
r
  getRange (InlinePragma Range
r Bool
_ QName
_)              = Range
r
  getRange (ImpossiblePragma Range
r [String]
_)            = Range
r
  getRange (EtaPragma Range
r QName
_)                   = Range
r
  getRange (TerminationCheckPragma Range
r TerminationCheck Name
_)      = Range
r
  getRange (NoCoverageCheckPragma Range
r)         = Range
r
  getRange (WarningOnUsage Range
r QName
_ Text
_)            = Range
r
  getRange (WarningOnImport Range
r Text
_)             = Range
r
  getRange (CatchallPragma Range
r)                = Range
r
  getRange (DisplayPragma Range
r Pattern
_ Expr
_)             = Range
r
  getRange (NoPositivityCheckPragma Range
r)       = Range
r
  getRange (PolarityPragma Range
r Name
_ [Occurrence]
_)            = Range
r
  getRange (NoUniverseCheckPragma Range
r)         = Range
r
  getRange (NotProjectionLikePragma Range
r QName
_)     = Range
r
  getRange (OverlapPragma Range
r [QName]
_ OverlapMode
_)             = Range
r

instance HasRange AsName where
  getRange :: AsName -> Range
getRange AsName
a = (Range, Either Expr Name) -> Range
forall a. HasRange a => a -> Range
getRange (AsName -> Range
forall a. AsName' a -> Range
asRange AsName
a, AsName -> Either Expr Name
forall a. AsName' a -> a
asName AsName
a)

instance HasRange Pattern where
  getRange :: Pattern -> Range
getRange (IdentP Bool
_ QName
x)       = QName -> Range
forall a. HasRange a => a -> Range
getRange QName
x
  getRange (AppP Pattern
p NamedArg Pattern
q)         = Pattern -> NamedArg Pattern -> Range
forall u t. (HasRange u, HasRange t) => u -> t -> Range
fuseRange Pattern
p NamedArg Pattern
q
  getRange (OpAppP Range
r QName
_ Set Name
_ [NamedArg Pattern]
_)   = Range
r
  getRange (RawAppP Range
r List2 Pattern
_)      = Range
r
  getRange (ParenP Range
r Pattern
_)       = Range
r
  getRange (WildP Range
r)          = Range
r
  getRange (AsP Range
r Name
_ Pattern
_)        = Range
r
  getRange (AbsurdP Range
r)        = Range
r
  getRange (LitP Range
r Literal
_)         = Range
r
  getRange (QuoteP Range
r)         = Range
r
  getRange (HiddenP Range
r Named_ Pattern
_)      = Range
r
  getRange (InstanceP Range
r Named_ Pattern
_)    = Range
r
  getRange (DotP Range
r Expr
_)         = Range
r
  getRange (RecP Range
r [FieldAssignment' Pattern]
_)         = Range
r
  getRange (EqualP Range
r [(Expr, Expr)]
_)       = Range
r
  getRange (EllipsisP Range
r Maybe Pattern
_)    = Range
r
  getRange (WithP Range
r Pattern
_)        = Range
r

-- SetRange instances
------------------------------------------------------------------------

instance SetRange Pattern where
  setRange :: Range -> Pattern -> Pattern
setRange Range
r (IdentP Bool
c QName
x)       = Bool -> QName -> Pattern
IdentP Bool
c (Range -> QName -> QName
forall a. SetRange a => Range -> a -> a
setRange Range
r QName
x)
  setRange Range
r (AppP Pattern
p NamedArg Pattern
q)         = Pattern -> NamedArg Pattern -> Pattern
AppP (Range -> Pattern -> Pattern
forall a. SetRange a => Range -> a -> a
setRange Range
r Pattern
p) (Range -> NamedArg Pattern -> NamedArg Pattern
forall a. SetRange a => Range -> a -> a
setRange Range
r NamedArg Pattern
q)
  setRange Range
r (OpAppP Range
_ QName
x Set Name
ns [NamedArg Pattern]
ps) = Range -> QName -> Set Name -> [NamedArg Pattern] -> Pattern
OpAppP Range
r QName
x Set Name
ns [NamedArg Pattern]
ps
  setRange Range
r (RawAppP Range
_ List2 Pattern
ps)     = Range -> List2 Pattern -> Pattern
RawAppP Range
r List2 Pattern
ps
  setRange Range
r (ParenP Range
_ Pattern
p)       = Range -> Pattern -> Pattern
ParenP Range
r Pattern
p
  setRange Range
r (WildP Range
_)          = Range -> Pattern
WildP Range
r
  setRange Range
r (AsP Range
_ Name
x Pattern
p)        = Range -> Name -> Pattern -> Pattern
AsP Range
r (Range -> Name -> Name
forall a. SetRange a => Range -> a -> a
setRange Range
r Name
x) Pattern
p
  setRange Range
r (AbsurdP Range
_)        = Range -> Pattern
AbsurdP Range
r
  setRange Range
r (LitP Range
_ Literal
l)         = Range -> Literal -> Pattern
LitP Range
r Literal
l
  setRange Range
r (QuoteP Range
_)         = Range -> Pattern
QuoteP Range
r
  setRange Range
r (HiddenP Range
_ Named_ Pattern
p)      = Range -> Named_ Pattern -> Pattern
HiddenP Range
r Named_ Pattern
p
  setRange Range
r (InstanceP Range
_ Named_ Pattern
p)    = Range -> Named_ Pattern -> Pattern
InstanceP Range
r Named_ Pattern
p
  setRange Range
r (DotP Range
_ Expr
e)         = Range -> Expr -> Pattern
DotP Range
r Expr
e
  setRange Range
r (RecP Range
_ [FieldAssignment' Pattern]
fs)        = Range -> [FieldAssignment' Pattern] -> Pattern
RecP Range
r [FieldAssignment' Pattern]
fs
  setRange Range
r (EqualP Range
_ [(Expr, Expr)]
es)      = Range -> [(Expr, Expr)] -> Pattern
EqualP Range
r [(Expr, Expr)]
es
  setRange Range
r (EllipsisP Range
_ Maybe Pattern
mp)   = Range -> Maybe Pattern -> Pattern
EllipsisP Range
r Maybe Pattern
mp
  setRange Range
r (WithP Range
_ Pattern
p)        = Range -> Pattern -> Pattern
WithP Range
r Pattern
p

instance SetRange TypedBinding where
  setRange :: Range -> TypedBinding' Expr -> TypedBinding' Expr
setRange Range
r (TBind Range
_ List1 (NamedArg Binder)
xs Expr
e) = Range -> List1 (NamedArg Binder) -> Expr -> TypedBinding' Expr
forall e. Range -> List1 (NamedArg Binder) -> e -> TypedBinding' e
TBind Range
r List1 (NamedArg Binder)
xs Expr
e
  setRange Range
r (TLet Range
_ List1 Declaration
ds)    = Range -> List1 Declaration -> TypedBinding' Expr
forall e. Range -> List1 Declaration -> TypedBinding' e
TLet Range
r List1 Declaration
ds

-- KillRange instances
------------------------------------------------------------------------

instance KillRange a => KillRange (FieldAssignment' a) where
  killRange :: KillRangeT (FieldAssignment' a)
killRange (FieldAssignment Name
a a
b) = (Name -> a -> FieldAssignment' a)
-> Name -> a -> FieldAssignment' a
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN Name -> a -> FieldAssignment' a
forall a. Name -> a -> FieldAssignment' a
FieldAssignment Name
a a
b

instance KillRange ModuleAssignment where
  killRange :: KillRangeT ModuleAssignment
killRange (ModuleAssignment QName
a [Expr]
b ImportDirective
c) = (QName -> [Expr] -> ImportDirective -> ModuleAssignment)
-> QName -> [Expr] -> ImportDirective -> ModuleAssignment
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN QName -> [Expr] -> ImportDirective -> ModuleAssignment
ModuleAssignment QName
a [Expr]
b ImportDirective
c

instance KillRange AsName where
  killRange :: KillRangeT AsName
killRange (AsName Either Expr Name
n Range
_) = (Either Expr Name -> AsName) -> Either Expr Name -> AsName
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN ((Either Expr Name -> Range -> AsName)
-> Range -> Either Expr Name -> AsName
forall a b c. (a -> b -> c) -> b -> a -> c
flip Either Expr Name -> Range -> AsName
forall a. a -> Range -> AsName' a
AsName Range
forall a. Range' a
noRange) Either Expr Name
n

instance KillRange Binder where
  killRange :: KillRangeT Binder
killRange (Binder Maybe Pattern
a BoundName
b) = (Maybe Pattern -> BoundName -> Binder)
-> Maybe Pattern -> BoundName -> Binder
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN Maybe Pattern -> BoundName -> Binder
forall a. Maybe Pattern -> a -> Binder' a
Binder Maybe Pattern
a BoundName
b

instance KillRange BoundName where
  killRange :: KillRangeT BoundName
killRange (BName Name
n Fixity'
f TacticAttribute
t Bool
b) = (Name -> Fixity' -> TacticAttribute -> Bool -> BoundName)
-> Name -> Fixity' -> TacticAttribute -> Bool -> BoundName
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN Name -> Fixity' -> TacticAttribute -> Bool -> BoundName
BName Name
n Fixity'
f TacticAttribute
t Bool
b

instance KillRange RecordDirective where
  killRange :: KillRangeT RecordDirective
killRange (Induction Ranged Induction
a)          = (Ranged Induction -> RecordDirective)
-> Ranged Induction -> RecordDirective
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN Ranged Induction -> RecordDirective
Induction Ranged Induction
a
  killRange (Eta Ranged HasEta0
a    )            = (Ranged HasEta0 -> RecordDirective)
-> Ranged HasEta0 -> RecordDirective
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN Ranged HasEta0 -> RecordDirective
Eta Ranged HasEta0
a
  killRange (Constructor Name
a IsInstance
b)      = (Name -> IsInstance -> RecordDirective)
-> Name -> IsInstance -> RecordDirective
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN Name -> IsInstance -> RecordDirective
Constructor Name
a IsInstance
b
  killRange (PatternOrCopattern Range
_) = Range -> RecordDirective
PatternOrCopattern Range
forall a. Range' a
noRange

instance KillRange Declaration where
  killRange :: KillRangeT Declaration
killRange (TypeSig ArgInfo
i TacticAttribute
t Name
n Expr
e)       = (TacticAttribute -> Name -> Expr -> Declaration)
-> TacticAttribute -> Name -> Expr -> Declaration
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN (ArgInfo -> TacticAttribute -> Name -> Expr -> Declaration
TypeSig ArgInfo
i) TacticAttribute
t Name
n Expr
e
  killRange (FieldSig IsInstance
i TacticAttribute
t Name
n Arg Expr
e)      = (IsInstance -> TacticAttribute -> Name -> Arg Expr -> Declaration)
-> IsInstance -> TacticAttribute -> Name -> Arg Expr -> Declaration
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN IsInstance -> TacticAttribute -> Name -> Arg Expr -> Declaration
FieldSig IsInstance
i TacticAttribute
t Name
n Arg Expr
e
  killRange (Generalize KwRange
r [Declaration]
ds )      = ([Declaration] -> Declaration) -> [Declaration] -> Declaration
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN (KwRange -> [Declaration] -> Declaration
Generalize KwRange
forall a. Null a => a
empty) [Declaration]
ds
  killRange (Field KwRange
r [Declaration]
fs)            = ([Declaration] -> Declaration) -> [Declaration] -> Declaration
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN (KwRange -> [Declaration] -> Declaration
Field KwRange
forall a. Null a => a
empty) [Declaration]
fs
  killRange (FunClause LHS
l RHS
r WhereClause
w Bool
ca)    = (LHS -> RHS -> WhereClause -> Bool -> Declaration)
-> LHS -> RHS -> WhereClause -> Bool -> Declaration
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN LHS -> RHS -> WhereClause -> Bool -> Declaration
FunClause LHS
l RHS
r WhereClause
w Bool
ca
  killRange (DataSig Range
_ Erased
er Name
n [LamBinding]
l Expr
e)    = (Erased -> Name -> [LamBinding] -> Expr -> Declaration)
-> Erased -> Name -> [LamBinding] -> Expr -> Declaration
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN (Range -> Erased -> Name -> [LamBinding] -> Expr -> Declaration
DataSig Range
forall a. Range' a
noRange) Erased
er Name
n [LamBinding]
l Expr
e
  killRange (Data Range
_ Erased
er Name
n [LamBinding]
l Expr
e [Declaration]
c)     = (Erased
 -> Name -> [LamBinding] -> Expr -> [Declaration] -> Declaration)
-> Erased
-> Name
-> [LamBinding]
-> Expr
-> [Declaration]
-> Declaration
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN (Range
-> Erased
-> Name
-> [LamBinding]
-> Expr
-> [Declaration]
-> Declaration
Data Range
forall a. Range' a
noRange) Erased
er Name
n [LamBinding]
l Expr
e [Declaration]
c
  killRange (DataDef Range
_ Name
n [LamBinding]
l [Declaration]
c)       = (Name -> [LamBinding] -> [Declaration] -> Declaration)
-> Name -> [LamBinding] -> [Declaration] -> Declaration
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN (Range -> Name -> [LamBinding] -> [Declaration] -> Declaration
DataDef Range
forall a. Range' a
noRange) Name
n [LamBinding]
l [Declaration]
c
  killRange (RecordSig Range
_ Erased
er Name
n [LamBinding]
l Expr
e)  = (Erased -> Name -> [LamBinding] -> Expr -> Declaration)
-> Erased -> Name -> [LamBinding] -> Expr -> Declaration
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN (Range -> Erased -> Name -> [LamBinding] -> Expr -> Declaration
RecordSig Range
forall a. Range' a
noRange) Erased
er Name
n [LamBinding]
l Expr
e
  killRange (RecordDef Range
_ Name
n [RecordDirective]
dir [LamBinding]
k [Declaration]
d) = (Name
 -> [RecordDirective]
 -> [LamBinding]
 -> [Declaration]
 -> Declaration)
-> Name
-> [RecordDirective]
-> [LamBinding]
-> [Declaration]
-> Declaration
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN (Range
-> Name
-> [RecordDirective]
-> [LamBinding]
-> [Declaration]
-> Declaration
RecordDef Range
forall a. Range' a
noRange) Name
n [RecordDirective]
dir [LamBinding]
k [Declaration]
d
  killRange (Record Range
_ Erased
er Name
n [RecordDirective]
dir [LamBinding]
k Expr
e [Declaration]
d)
                                    = (Erased
 -> Name
 -> [RecordDirective]
 -> [LamBinding]
 -> Expr
 -> [Declaration]
 -> Declaration)
-> Erased
-> Name
-> [RecordDirective]
-> [LamBinding]
-> Expr
-> [Declaration]
-> Declaration
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN (Range
-> Erased
-> Name
-> [RecordDirective]
-> [LamBinding]
-> Expr
-> [Declaration]
-> Declaration
Record Range
forall a. Range' a
noRange) Erased
er Name
n [RecordDirective]
dir [LamBinding]
k Expr
e [Declaration]
d
  killRange (Infix Fixity
f List1 Name
n)             = (Fixity -> List1 Name -> Declaration)
-> Fixity -> List1 Name -> Declaration
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN Fixity -> List1 Name -> Declaration
Infix Fixity
f List1 Name
n
  killRange (Syntax Name
n Notation
no)           = (Name -> Declaration) -> Name -> Declaration
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN (\Name
n -> Name -> Notation -> Declaration
Syntax Name
n Notation
no) Name
n
  killRange (PatternSyn Range
_ Name
n [WithHiding Name]
ns Pattern
p)   = (Name -> [WithHiding Name] -> Pattern -> Declaration)
-> Name -> [WithHiding Name] -> Pattern -> Declaration
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN (Range -> Name -> [WithHiding Name] -> Pattern -> Declaration
PatternSyn Range
forall a. Range' a
noRange) Name
n [WithHiding Name]
ns Pattern
p
  killRange (Mutual KwRange
_ [Declaration]
d)            = ([Declaration] -> Declaration) -> [Declaration] -> Declaration
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN (KwRange -> [Declaration] -> Declaration
Mutual KwRange
forall a. Null a => a
empty) [Declaration]
d
  killRange (InterleavedMutual KwRange
_ [Declaration]
d) = ([Declaration] -> Declaration) -> [Declaration] -> Declaration
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN (KwRange -> [Declaration] -> Declaration
InterleavedMutual KwRange
forall a. Null a => a
empty) [Declaration]
d
  killRange (LoneConstructor KwRange
_ [Declaration]
d)   = ([Declaration] -> Declaration) -> [Declaration] -> Declaration
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN (KwRange -> [Declaration] -> Declaration
LoneConstructor KwRange
forall a. Null a => a
empty) [Declaration]
d
  killRange (Abstract KwRange
_ [Declaration]
d)          = ([Declaration] -> Declaration) -> [Declaration] -> Declaration
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN (KwRange -> [Declaration] -> Declaration
Abstract KwRange
forall a. Null a => a
empty) [Declaration]
d
  killRange (Private KwRange
_ Origin
o [Declaration]
d)         = (Origin -> [Declaration] -> Declaration)
-> Origin -> [Declaration] -> Declaration
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN (KwRange -> Origin -> [Declaration] -> Declaration
Private KwRange
forall a. Null a => a
empty) Origin
o [Declaration]
d
  killRange (InstanceB KwRange
_ [Declaration]
d)         = ([Declaration] -> Declaration) -> [Declaration] -> Declaration
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN (KwRange -> [Declaration] -> Declaration
InstanceB KwRange
forall a. Null a => a
empty) [Declaration]
d
  killRange (Macro KwRange
_ [Declaration]
d)             = ([Declaration] -> Declaration) -> [Declaration] -> Declaration
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN (KwRange -> [Declaration] -> Declaration
Macro KwRange
forall a. Null a => a
empty) [Declaration]
d
  killRange (Postulate KwRange
_ [Declaration]
t)         = ([Declaration] -> Declaration) -> [Declaration] -> Declaration
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN (KwRange -> [Declaration] -> Declaration
Postulate KwRange
forall a. Null a => a
empty) [Declaration]
t
  killRange (Primitive KwRange
_ [Declaration]
t)         = ([Declaration] -> Declaration) -> [Declaration] -> Declaration
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN (KwRange -> [Declaration] -> Declaration
Primitive KwRange
forall a. Null a => a
empty) [Declaration]
t
  killRange (Open Range
_ QName
q ImportDirective
i)            = (QName -> ImportDirective -> Declaration)
-> QName -> ImportDirective -> Declaration
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN (Range -> QName -> ImportDirective -> Declaration
Open Range
forall a. Range' a
noRange) QName
q ImportDirective
i
  killRange (Import Range
_ QName
q Maybe AsName
a OpenShortHand
o ImportDirective
i)      = (QName -> Maybe AsName -> ImportDirective -> Declaration)
-> QName -> Maybe AsName -> ImportDirective -> Declaration
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN (\QName
q Maybe AsName
a -> Range
-> QName
-> Maybe AsName
-> OpenShortHand
-> ImportDirective
-> Declaration
Import Range
forall a. Range' a
noRange QName
q Maybe AsName
a OpenShortHand
o) QName
q Maybe AsName
a ImportDirective
i
  killRange (ModuleMacro Range
_ Erased
e Name
n ModuleApplication
m OpenShortHand
o ImportDirective
i)
                                    = (Erased
 -> Name -> ModuleApplication -> ImportDirective -> Declaration)
-> Erased
-> Name
-> ModuleApplication
-> ImportDirective
-> Declaration
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN
                                        (\Erased
e Name
n ModuleApplication
m -> Range
-> Erased
-> Name
-> ModuleApplication
-> OpenShortHand
-> ImportDirective
-> Declaration
ModuleMacro Range
forall a. Range' a
noRange Erased
e Name
n ModuleApplication
m OpenShortHand
o)
                                        Erased
e Name
n ModuleApplication
m ImportDirective
i
  killRange (Module Range
_ Erased
e QName
q Telescope
t [Declaration]
d)      = (Erased -> QName -> Telescope -> [Declaration] -> Declaration)
-> Erased -> QName -> Telescope -> [Declaration] -> Declaration
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN (Range
-> Erased -> QName -> Telescope -> [Declaration] -> Declaration
Module Range
forall a. Range' a
noRange) Erased
e QName
q Telescope
t [Declaration]
d
  killRange (UnquoteDecl Range
_ [Name]
x Expr
t)     = ([Name] -> Expr -> Declaration) -> [Name] -> Expr -> Declaration
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN (Range -> [Name] -> Expr -> Declaration
UnquoteDecl Range
forall a. Range' a
noRange) [Name]
x Expr
t
  killRange (UnquoteDef Range
_ [Name]
x Expr
t)      = ([Name] -> Expr -> Declaration) -> [Name] -> Expr -> Declaration
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN (Range -> [Name] -> Expr -> Declaration
UnquoteDef Range
forall a. Range' a
noRange) [Name]
x Expr
t
  killRange (UnquoteData Range
_ Name
xs [Name]
cs Expr
t) = (Name -> [Name] -> Expr -> Declaration)
-> Name -> [Name] -> Expr -> Declaration
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN (Range -> Name -> [Name] -> Expr -> Declaration
UnquoteData Range
forall a. Range' a
noRange) Name
xs [Name]
cs Expr
t
  killRange (Pragma Pragma
p)              = (Pragma -> Declaration) -> Pragma -> Declaration
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN Pragma -> Declaration
Pragma Pragma
p
  killRange (Opaque KwRange
r [Declaration]
xs)           = ([Declaration] -> Declaration) -> [Declaration] -> Declaration
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN (KwRange -> [Declaration] -> Declaration
Opaque KwRange
forall a. Null a => a
empty) [Declaration]
xs
  killRange (Unfolding KwRange
r [QName]
xs)        = ([QName] -> Declaration) -> [QName] -> Declaration
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN (KwRange -> [QName] -> Declaration
Unfolding KwRange
forall a. Null a => a
empty) [QName]
xs

instance KillRange Expr where
  killRange :: Expr -> Expr
killRange (Ident QName
q)              = (QName -> Expr) -> QName -> Expr
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN QName -> Expr
Ident QName
q
  killRange (Lit Range
_ Literal
l)              = (Literal -> Expr) -> Literal -> Expr
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN (Range -> Literal -> Expr
Lit Range
forall a. Range' a
noRange) Literal
l
  killRange (QuestionMark Range
_ Maybe Int
n)     = Range -> Maybe Int -> Expr
QuestionMark Range
forall a. Range' a
noRange Maybe Int
n
  killRange (Underscore Range
_ Maybe String
n)       = Range -> Maybe String -> Expr
Underscore Range
forall a. Range' a
noRange Maybe String
n
  killRange (RawApp Range
_ List2 Expr
e)           = (List2 Expr -> Expr) -> List2 Expr -> Expr
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN (Range -> List2 Expr -> Expr
RawApp Range
forall a. Range' a
noRange) List2 Expr
e
  killRange (App Range
_ Expr
e NamedArg Expr
a)            = (Expr -> NamedArg Expr -> Expr) -> Expr -> NamedArg Expr -> Expr
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN (Range -> Expr -> NamedArg Expr -> Expr
App Range
forall a. Range' a
noRange) Expr
e NamedArg Expr
a
  killRange (OpApp Range
_ QName
n Set Name
ns OpAppArgs
o)       = (QName -> Set Name -> OpAppArgs -> Expr)
-> QName -> Set Name -> OpAppArgs -> Expr
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN (Range -> QName -> Set Name -> OpAppArgs -> Expr
OpApp Range
forall a. Range' a
noRange) QName
n Set Name
ns OpAppArgs
o
  killRange (WithApp Range
_ Expr
e [Expr]
es)       = (Expr -> [Expr] -> Expr) -> Expr -> [Expr] -> Expr
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN (Range -> Expr -> [Expr] -> Expr
WithApp Range
forall a. Range' a
noRange) Expr
e [Expr]
es
  killRange (HiddenArg Range
_ Named_ Expr
n)        = (Named_ Expr -> Expr) -> Named_ Expr -> Expr
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN (Range -> Named_ Expr -> Expr
HiddenArg Range
forall a. Range' a
noRange) Named_ Expr
n
  killRange (InstanceArg Range
_ Named_ Expr
n)      = (Named_ Expr -> Expr) -> Named_ Expr -> Expr
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN (Range -> Named_ Expr -> Expr
InstanceArg Range
forall a. Range' a
noRange) Named_ Expr
n
  killRange (Lam Range
_ List1 LamBinding
l Expr
e)            = (List1 LamBinding -> Expr -> Expr)
-> List1 LamBinding -> Expr -> Expr
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN (Range -> List1 LamBinding -> Expr -> Expr
Lam Range
forall a. Range' a
noRange) List1 LamBinding
l Expr
e
  killRange (AbsurdLam Range
_ Hiding
h)        = (Hiding -> Expr) -> Hiding -> Expr
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN (Range -> Hiding -> Expr
AbsurdLam Range
forall a. Range' a
noRange) Hiding
h
  killRange (ExtendedLam Range
_ Erased
e List1 LamClause
lrw)  = (Erased -> List1 LamClause -> Expr)
-> Erased -> List1 LamClause -> Expr
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN (Range -> Erased -> List1 LamClause -> Expr
ExtendedLam Range
forall a. Range' a
noRange) Erased
e List1 LamClause
lrw
  killRange (Fun Range
_ Arg Expr
e1 Expr
e2)          = (Arg Expr -> Expr -> Expr) -> Arg Expr -> Expr -> Expr
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN (Range -> Arg Expr -> Expr -> Expr
Fun Range
forall a. Range' a
noRange) Arg Expr
e1 Expr
e2
  killRange (Pi Telescope1
t Expr
e)               = (Telescope1 -> Expr -> Expr) -> Telescope1 -> Expr -> Expr
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN Telescope1 -> Expr -> Expr
Pi Telescope1
t Expr
e
  killRange (Rec Range
_ RecordAssignments
ne)             = (RecordAssignments -> Expr) -> RecordAssignments -> Expr
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN (Range -> RecordAssignments -> Expr
Rec Range
forall a. Range' a
noRange) RecordAssignments
ne
  killRange (RecUpdate Range
_ Expr
e [FieldAssignment]
ne)     = (Expr -> [FieldAssignment] -> Expr)
-> Expr -> [FieldAssignment] -> Expr
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN (Range -> Expr -> [FieldAssignment] -> Expr
RecUpdate Range
forall a. Range' a
noRange) Expr
e [FieldAssignment]
ne
  killRange (Let Range
_ List1 Declaration
d Maybe Expr
e)            = (List1 Declaration -> Maybe Expr -> Expr)
-> List1 Declaration -> Maybe Expr -> Expr
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN (Range -> List1 Declaration -> Maybe Expr -> Expr
Let Range
forall a. Range' a
noRange) List1 Declaration
d Maybe Expr
e
  killRange (Paren Range
_ Expr
e)            = (Expr -> Expr) -> Expr -> Expr
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN (Range -> Expr -> Expr
Paren Range
forall a. Range' a
noRange) Expr
e
  killRange (IdiomBrackets Range
_ [Expr]
es)   = ([Expr] -> Expr) -> [Expr] -> Expr
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN (Range -> [Expr] -> Expr
IdiomBrackets Range
forall a. Range' a
noRange) [Expr]
es
  killRange (DoBlock Range
_ List1 DoStmt
ss)         = (List1 DoStmt -> Expr) -> List1 DoStmt -> Expr
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN (Range -> List1 DoStmt -> Expr
DoBlock Range
forall a. Range' a
noRange) List1 DoStmt
ss
  killRange (Absurd Range
_)             = Range -> Expr
Absurd Range
forall a. Range' a
noRange
  killRange (As Range
_ Name
n Expr
e)             = (Name -> Expr -> Expr) -> Name -> Expr -> Expr
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN (Range -> Name -> Expr -> Expr
As Range
forall a. Range' a
noRange) Name
n Expr
e
  killRange (Dot Range
_ Expr
e)              = (Expr -> Expr) -> Expr -> Expr
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN (Range -> Expr -> Expr
Dot Range
forall a. Range' a
noRange) Expr
e
  killRange (DoubleDot Range
_ Expr
e)        = (Expr -> Expr) -> Expr -> Expr
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN (Range -> Expr -> Expr
DoubleDot Range
forall a. Range' a
noRange) Expr
e
  killRange (Quote Range
_)              = Range -> Expr
Quote Range
forall a. Range' a
noRange
  killRange (QuoteTerm Range
_)          = Range -> Expr
QuoteTerm Range
forall a. Range' a
noRange
  killRange (Unquote Range
_)            = Range -> Expr
Unquote Range
forall a. Range' a
noRange
  killRange (Tactic Range
_ Expr
t)           = (Expr -> Expr) -> Expr -> Expr
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN (Range -> Expr -> Expr
Tactic Range
forall a. Range' a
noRange) Expr
t
  killRange (DontCare Expr
e)           = (Expr -> Expr) -> Expr -> Expr
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN Expr -> Expr
DontCare Expr
e
  killRange (Equal Range
_ Expr
x Expr
y)          = Range -> Expr -> Expr -> Expr
Equal Range
forall a. Range' a
noRange Expr
x Expr
y
  killRange (Ellipsis Range
_)           = Range -> Expr
Ellipsis Range
forall a. Range' a
noRange
  killRange (Generalized Expr
e)        = (Expr -> Expr) -> Expr -> Expr
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN Expr -> Expr
Generalized Expr
e
  killRange (KnownIdent NameKind
a QName
b)       = (QName -> Expr) -> QName -> Expr
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN (NameKind -> QName -> Expr
KnownIdent NameKind
a) QName
b
  killRange (KnownOpApp NameKind
a Range
b QName
c Set Name
d OpAppArgs
e) = (Range -> QName -> Set Name -> OpAppArgs -> Expr)
-> Range -> QName -> Set Name -> OpAppArgs -> Expr
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN (NameKind -> Range -> QName -> Set Name -> OpAppArgs -> Expr
KnownOpApp NameKind
a) Range
b QName
c Set Name
d OpAppArgs
e

instance KillRange LamBinding where
  killRange :: LamBinding -> LamBinding
killRange (DomainFree NamedArg Binder
b) = (NamedArg Binder -> LamBinding) -> NamedArg Binder -> LamBinding
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN NamedArg Binder -> LamBinding
forall a. NamedArg Binder -> LamBinding' a
DomainFree NamedArg Binder
b
  killRange (DomainFull TypedBinding' Expr
t) = (TypedBinding' Expr -> LamBinding)
-> TypedBinding' Expr -> LamBinding
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN TypedBinding' Expr -> LamBinding
forall a. a -> LamBinding' a
DomainFull TypedBinding' Expr
t

instance KillRange LHS where
  killRange :: KillRangeT LHS
killRange (LHS Pattern
p [RewriteEqn]
r [WithExpr]
w)  = (Pattern -> [RewriteEqn] -> [WithExpr] -> LHS)
-> Pattern -> [RewriteEqn] -> [WithExpr] -> LHS
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN Pattern -> [RewriteEqn] -> [WithExpr] -> LHS
LHS Pattern
p [RewriteEqn]
r [WithExpr]
w

instance KillRange LamClause where
  killRange :: KillRangeT LamClause
killRange (LamClause [Pattern]
a RHS
b Bool
c) = ([Pattern] -> RHS -> Bool -> LamClause)
-> [Pattern] -> RHS -> Bool -> LamClause
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN [Pattern] -> RHS -> Bool -> LamClause
LamClause [Pattern]
a RHS
b Bool
c

instance KillRange DoStmt where
  killRange :: KillRangeT DoStmt
killRange (DoBind Range
r Pattern
p Expr
e [LamClause]
w) = (Range -> Pattern -> Expr -> [LamClause] -> DoStmt)
-> Range -> Pattern -> Expr -> [LamClause] -> DoStmt
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN Range -> Pattern -> Expr -> [LamClause] -> DoStmt
DoBind Range
r Pattern
p Expr
e [LamClause]
w
  killRange (DoThen Expr
e)       = (Expr -> DoStmt) -> Expr -> DoStmt
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN Expr -> DoStmt
DoThen Expr
e
  killRange (DoLet Range
r List1 Declaration
ds)     = (Range -> List1 Declaration -> DoStmt)
-> Range -> List1 Declaration -> DoStmt
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN Range -> List1 Declaration -> DoStmt
DoLet Range
r List1 Declaration
ds

instance KillRange ModuleApplication where
  killRange :: KillRangeT ModuleApplication
killRange (SectionApp Range
_ Telescope
t Expr
e)    = (Telescope -> Expr -> ModuleApplication)
-> Telescope -> Expr -> ModuleApplication
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN (Range -> Telescope -> Expr -> ModuleApplication
SectionApp Range
forall a. Range' a
noRange) Telescope
t Expr
e
  killRange (RecordModuleInstance Range
_ QName
q) = (QName -> ModuleApplication) -> QName -> ModuleApplication
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN (Range -> QName -> ModuleApplication
RecordModuleInstance Range
forall a. Range' a
noRange) QName
q

instance KillRange e => KillRange (OpApp e) where
  killRange :: KillRangeT (OpApp e)
killRange (SyntaxBindingLambda Range
_ List1 LamBinding
l e
e) = (List1 LamBinding -> e -> OpApp e)
-> List1 LamBinding -> e -> OpApp e
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN (Range -> List1 LamBinding -> e -> OpApp e
forall e. Range -> List1 LamBinding -> e -> OpApp e
SyntaxBindingLambda Range
forall a. Range' a
noRange) List1 LamBinding
l e
e
  killRange (Ordinary e
e)                = (e -> OpApp e) -> e -> OpApp e
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN e -> OpApp e
forall e. e -> OpApp e
Ordinary e
e

instance KillRange Pattern where
  killRange :: Pattern -> Pattern
killRange (IdentP Bool
c QName
q)      = (Bool -> QName -> Pattern) -> Bool -> QName -> Pattern
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN Bool -> QName -> Pattern
IdentP Bool
c QName
q
  killRange (AppP Pattern
p NamedArg Pattern
ps)       = (Pattern -> NamedArg Pattern -> Pattern)
-> Pattern -> NamedArg Pattern -> Pattern
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN Pattern -> NamedArg Pattern -> Pattern
AppP Pattern
p NamedArg Pattern
ps
  killRange (RawAppP Range
_ List2 Pattern
p)     = (List2 Pattern -> Pattern) -> List2 Pattern -> Pattern
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN (Range -> List2 Pattern -> Pattern
RawAppP Range
forall a. Range' a
noRange) List2 Pattern
p
  killRange (OpAppP Range
_ QName
n Set Name
ns [NamedArg Pattern]
p) = (QName -> Set Name -> [NamedArg Pattern] -> Pattern)
-> QName -> Set Name -> [NamedArg Pattern] -> Pattern
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN (Range -> QName -> Set Name -> [NamedArg Pattern] -> Pattern
OpAppP Range
forall a. Range' a
noRange) QName
n Set Name
ns [NamedArg Pattern]
p
  killRange (HiddenP Range
_ Named_ Pattern
n)     = (Named_ Pattern -> Pattern) -> Named_ Pattern -> Pattern
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN (Range -> Named_ Pattern -> Pattern
HiddenP Range
forall a. Range' a
noRange) Named_ Pattern
n
  killRange (InstanceP Range
_ Named_ Pattern
n)   = (Named_ Pattern -> Pattern) -> Named_ Pattern -> Pattern
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN (Range -> Named_ Pattern -> Pattern
InstanceP Range
forall a. Range' a
noRange) Named_ Pattern
n
  killRange (ParenP Range
_ Pattern
p)      = (Pattern -> Pattern) -> Pattern -> Pattern
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN (Range -> Pattern -> Pattern
ParenP Range
forall a. Range' a
noRange) Pattern
p
  killRange (WildP Range
_)         = Range -> Pattern
WildP Range
forall a. Range' a
noRange
  killRange (AbsurdP Range
_)       = Range -> Pattern
AbsurdP Range
forall a. Range' a
noRange
  killRange (AsP Range
_ Name
n Pattern
p)       = (Name -> Pattern -> Pattern) -> Name -> Pattern -> Pattern
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN (Range -> Name -> Pattern -> Pattern
AsP Range
forall a. Range' a
noRange) Name
n Pattern
p
  killRange (DotP Range
_ Expr
e)        = (Expr -> Pattern) -> Expr -> Pattern
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN (Range -> Expr -> Pattern
DotP Range
forall a. Range' a
noRange) Expr
e
  killRange (LitP Range
_ Literal
l)        = (Literal -> Pattern) -> Literal -> Pattern
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN (Range -> Literal -> Pattern
LitP Range
forall a. Range' a
noRange) Literal
l
  killRange (QuoteP Range
_)        = Range -> Pattern
QuoteP Range
forall a. Range' a
noRange
  killRange (RecP Range
_ [FieldAssignment' Pattern]
fs)       = ([FieldAssignment' Pattern] -> Pattern)
-> [FieldAssignment' Pattern] -> Pattern
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN (Range -> [FieldAssignment' Pattern] -> Pattern
RecP Range
forall a. Range' a
noRange) [FieldAssignment' Pattern]
fs
  killRange (EqualP Range
_ [(Expr, Expr)]
es)     = ([(Expr, Expr)] -> Pattern) -> [(Expr, Expr)] -> Pattern
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN (Range -> [(Expr, Expr)] -> Pattern
EqualP Range
forall a. Range' a
noRange) [(Expr, Expr)]
es
  killRange (EllipsisP Range
_ Maybe Pattern
mp)  = (Maybe Pattern -> Pattern) -> Maybe Pattern -> Pattern
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN (Range -> Maybe Pattern -> Pattern
EllipsisP Range
forall a. Range' a
noRange) Maybe Pattern
mp
  killRange (WithP Range
_ Pattern
p)       = (Pattern -> Pattern) -> Pattern -> Pattern
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN (Range -> Pattern -> Pattern
WithP Range
forall a. Range' a
noRange) Pattern
p

instance KillRange Pragma where
  killRange :: KillRangeT Pragma
killRange (OptionsPragma Range
_ [String]
s)               = Range -> [String] -> Pragma
OptionsPragma Range
forall a. Range' a
noRange [String]
s
  killRange (BuiltinPragma Range
_ Ranged String
s QName
e)             = (QName -> Pragma) -> QName -> Pragma
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN (Range -> Ranged String -> QName -> Pragma
BuiltinPragma Range
forall a. Range' a
noRange Ranged String
s) QName
e
  killRange (RewritePragma Range
_ Range
_ [QName]
qs)            = ([QName] -> Pragma) -> [QName] -> Pragma
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN (Range -> Range -> [QName] -> Pragma
RewritePragma Range
forall a. Range' a
noRange Range
forall a. Range' a
noRange) [QName]
qs
  killRange (StaticPragma Range
_ QName
q)                = (QName -> Pragma) -> QName -> Pragma
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN (Range -> QName -> Pragma
StaticPragma Range
forall a. Range' a
noRange) QName
q
  killRange (InjectivePragma Range
_ QName
q)             = (QName -> Pragma) -> QName -> Pragma
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN (Range -> QName -> Pragma
InjectivePragma Range
forall a. Range' a
noRange) QName
q
  killRange (InjectiveForInferencePragma Range
_ QName
q) = (QName -> Pragma) -> QName -> Pragma
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN (Range -> QName -> Pragma
InjectiveForInferencePragma Range
forall a. Range' a
noRange) QName
q
  killRange (InlinePragma Range
_ Bool
b QName
q)              = (QName -> Pragma) -> QName -> Pragma
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN (Range -> Bool -> QName -> Pragma
InlinePragma Range
forall a. Range' a
noRange Bool
b) QName
q
  killRange (CompilePragma Range
_ Ranged String
b QName
q String
s)           = (QName -> Pragma) -> QName -> Pragma
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN (\ QName
q -> Range -> Ranged String -> QName -> String -> Pragma
CompilePragma Range
forall a. Range' a
noRange Ranged String
b QName
q String
s) QName
q
  killRange (ForeignPragma Range
_ Ranged String
b String
s)             = Range -> Ranged String -> String -> Pragma
ForeignPragma Range
forall a. Range' a
noRange Ranged String
b String
s
  killRange (ImpossiblePragma Range
_ [String]
strs)         = Range -> [String] -> Pragma
ImpossiblePragma Range
forall a. Range' a
noRange [String]
strs
  killRange (TerminationCheckPragma Range
_ TerminationCheck Name
t)      = Range -> TerminationCheck Name -> Pragma
TerminationCheckPragma Range
forall a. Range' a
noRange (KillRangeT (TerminationCheck Name)
forall a. KillRange a => KillRangeT a
killRange TerminationCheck Name
t)
  killRange (NoCoverageCheckPragma Range
_)         = Range -> Pragma
NoCoverageCheckPragma Range
forall a. Range' a
noRange
  killRange (WarningOnUsage Range
_ QName
nm Text
str)         = Range -> QName -> Text -> Pragma
WarningOnUsage Range
forall a. Range' a
noRange (QName -> QName
forall a. KillRange a => KillRangeT a
killRange QName
nm) Text
str
  killRange (WarningOnImport Range
_ Text
str)           = Range -> Text -> Pragma
WarningOnImport Range
forall a. Range' a
noRange Text
str
  killRange (CatchallPragma Range
_)                = Range -> Pragma
CatchallPragma Range
forall a. Range' a
noRange
  killRange (DisplayPragma Range
_ Pattern
lhs Expr
rhs)         = (Pattern -> Expr -> Pragma) -> Pattern -> Expr -> Pragma
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN (Range -> Pattern -> Expr -> Pragma
DisplayPragma Range
forall a. Range' a
noRange) Pattern
lhs Expr
rhs
  killRange (EtaPragma Range
_ QName
q)                   = (QName -> Pragma) -> QName -> Pragma
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN (Range -> QName -> Pragma
EtaPragma Range
forall a. Range' a
noRange) QName
q
  killRange (NoPositivityCheckPragma Range
_)       = Range -> Pragma
NoPositivityCheckPragma Range
forall a. Range' a
noRange
  killRange (PolarityPragma Range
_ Name
q [Occurrence]
occs)         = (Name -> Pragma) -> Name -> Pragma
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN (\Name
q -> Range -> Name -> [Occurrence] -> Pragma
PolarityPragma Range
forall a. Range' a
noRange Name
q [Occurrence]
occs) Name
q
  killRange (NoUniverseCheckPragma Range
_)         = Range -> Pragma
NoUniverseCheckPragma Range
forall a. Range' a
noRange
  killRange (NotProjectionLikePragma Range
_ QName
q)     = Range -> QName -> Pragma
NotProjectionLikePragma Range
forall a. Range' a
noRange QName
q
  killRange (OverlapPragma Range
_ [QName]
q OverlapMode
i)             = Range -> [QName] -> OverlapMode -> Pragma
OverlapPragma Range
forall a. Range' a
noRange [QName]
q OverlapMode
i

instance KillRange RHS where
  killRange :: KillRangeT RHS
killRange RHS
AbsurdRHS = RHS
forall e. RHS' e
AbsurdRHS
  killRange (RHS Expr
e)   = (Expr -> RHS) -> Expr -> RHS
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN Expr -> RHS
forall e. e -> RHS' e
RHS Expr
e

instance KillRange TypedBinding where
  killRange :: TypedBinding' Expr -> TypedBinding' Expr
killRange (TBind Range
_ List1 (NamedArg Binder)
b Expr
e) = (List1 (NamedArg Binder) -> Expr -> TypedBinding' Expr)
-> List1 (NamedArg Binder) -> Expr -> TypedBinding' Expr
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN (Range -> List1 (NamedArg Binder) -> Expr -> TypedBinding' Expr
forall e. Range -> List1 (NamedArg Binder) -> e -> TypedBinding' e
TBind Range
forall a. Range' a
noRange) List1 (NamedArg Binder)
b Expr
e
  killRange (TLet Range
r List1 Declaration
ds)   = (Range -> List1 Declaration -> TypedBinding' Expr)
-> Range -> List1 Declaration -> TypedBinding' Expr
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN Range -> List1 Declaration -> TypedBinding' Expr
forall e. Range -> List1 Declaration -> TypedBinding' e
TLet Range
r List1 Declaration
ds

instance KillRange WhereClause where
  killRange :: KillRangeT WhereClause
killRange WhereClause
NoWhere               = WhereClause
forall a. WhereClause' a
NoWhere
  killRange (AnyWhere Range
r [Declaration]
d)        = ([Declaration] -> WhereClause) -> [Declaration] -> WhereClause
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN (Range -> [Declaration] -> WhereClause
forall decls. Range -> decls -> WhereClause' decls
AnyWhere Range
forall a. Range' a
noRange) [Declaration]
d
  killRange (SomeWhere Range
r Erased
e Name
n Access
a [Declaration]
d) =
    (Erased -> Name -> Access -> [Declaration] -> WhereClause)
-> Erased -> Name -> Access -> [Declaration] -> WhereClause
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN (Range -> Erased -> Name -> Access -> [Declaration] -> WhereClause
forall decls.
Range -> Erased -> Name -> Access -> decls -> WhereClause' decls
SomeWhere Range
forall a. Range' a
noRange) Erased
e Name
n Access
a [Declaration]
d

------------------------------------------------------------------------
-- NFData instances

-- | Ranges are not forced.

instance NFData Expr where
  rnf :: Expr -> ()
rnf (Ident QName
a)           = QName -> ()
forall a. NFData a => a -> ()
rnf QName
a
  rnf (Lit Range
_ Literal
a)           = Literal -> ()
forall a. NFData a => a -> ()
rnf Literal
a
  rnf (QuestionMark Range
_ Maybe Int
a)  = Maybe Int -> ()
forall a. NFData a => a -> ()
rnf Maybe Int
a
  rnf (Underscore Range
_ Maybe String
a)    = Maybe String -> ()
forall a. NFData a => a -> ()
rnf Maybe String
a
  rnf (RawApp Range
_ List2 Expr
a)        = List2 Expr -> ()
forall a. NFData a => a -> ()
rnf List2 Expr
a
  rnf (App Range
_ Expr
a NamedArg Expr
b)         = Expr -> ()
forall a. NFData a => a -> ()
rnf Expr
a () -> () -> ()
forall a b. a -> b -> b
`seq` NamedArg Expr -> ()
forall a. NFData a => a -> ()
rnf NamedArg Expr
b
  rnf (OpApp Range
_ QName
a Set Name
b OpAppArgs
c)     = QName -> ()
forall a. NFData a => a -> ()
rnf QName
a () -> () -> ()
forall a b. a -> b -> b
`seq` Set Name -> ()
forall a. NFData a => a -> ()
rnf Set Name
b () -> () -> ()
forall a b. a -> b -> b
`seq` OpAppArgs -> ()
forall a. NFData a => a -> ()
rnf OpAppArgs
c
  rnf (WithApp Range
_ Expr
a [Expr]
b)     = Expr -> ()
forall a. NFData a => a -> ()
rnf Expr
a () -> () -> ()
forall a b. a -> b -> b
`seq` [Expr] -> ()
forall a. NFData a => a -> ()
rnf [Expr]
b
  rnf (HiddenArg Range
_ Named_ Expr
a)     = Named_ Expr -> ()
forall a. NFData a => a -> ()
rnf Named_ Expr
a
  rnf (InstanceArg Range
_ Named_ Expr
a)   = Named_ Expr -> ()
forall a. NFData a => a -> ()
rnf Named_ Expr
a
  rnf (Lam Range
_ List1 LamBinding
a Expr
b)         = List1 LamBinding -> ()
forall a. NFData a => a -> ()
rnf List1 LamBinding
a () -> () -> ()
forall a b. a -> b -> b
`seq` Expr -> ()
forall a. NFData a => a -> ()
rnf Expr
b
  rnf (AbsurdLam Range
_ Hiding
a)     = Hiding -> ()
forall a. NFData a => a -> ()
rnf Hiding
a
  rnf (ExtendedLam Range
_ Erased
a List1 LamClause
b) = Erased -> ()
forall a. NFData a => a -> ()
rnf Erased
a () -> () -> ()
forall a b. a -> b -> b
`seq` List1 LamClause -> ()
forall a. NFData a => a -> ()
rnf List1 LamClause
b
  rnf (Fun Range
_ Arg Expr
a Expr
b)         = Arg Expr -> ()
forall a. NFData a => a -> ()
rnf Arg Expr
a () -> () -> ()
forall a b. a -> b -> b
`seq` Expr -> ()
forall a. NFData a => a -> ()
rnf Expr
b
  rnf (Pi Telescope1
a Expr
b)            = Telescope1 -> ()
forall a. NFData a => a -> ()
rnf Telescope1
a () -> () -> ()
forall a b. a -> b -> b
`seq` Expr -> ()
forall a. NFData a => a -> ()
rnf Expr
b
  rnf (Rec Range
_ RecordAssignments
a)           = RecordAssignments -> ()
forall a. NFData a => a -> ()
rnf RecordAssignments
a
  rnf (RecUpdate Range
_ Expr
a [FieldAssignment]
b)   = Expr -> ()
forall a. NFData a => a -> ()
rnf Expr
a () -> () -> ()
forall a b. a -> b -> b
`seq` [FieldAssignment] -> ()
forall a. NFData a => a -> ()
rnf [FieldAssignment]
b
  rnf (Let Range
_ List1 Declaration
a Maybe Expr
b)         = List1 Declaration -> ()
forall a. NFData a => a -> ()
rnf List1 Declaration
a () -> () -> ()
forall a b. a -> b -> b
`seq` Maybe Expr -> ()
forall a. NFData a => a -> ()
rnf Maybe Expr
b
  rnf (Paren Range
_ Expr
a)         = Expr -> ()
forall a. NFData a => a -> ()
rnf Expr
a
  rnf (IdiomBrackets Range
_ [Expr]
a) = [Expr] -> ()
forall a. NFData a => a -> ()
rnf [Expr]
a
  rnf (DoBlock Range
_ List1 DoStmt
a)       = List1 DoStmt -> ()
forall a. NFData a => a -> ()
rnf List1 DoStmt
a
  rnf (Absurd Range
_)          = ()
  rnf (As Range
_ Name
a Expr
b)          = Name -> ()
forall a. NFData a => a -> ()
rnf Name
a () -> () -> ()
forall a b. a -> b -> b
`seq` Expr -> ()
forall a. NFData a => a -> ()
rnf Expr
b
  rnf (Dot Range
_ Expr
a)           = Expr -> ()
forall a. NFData a => a -> ()
rnf Expr
a
  rnf (DoubleDot Range
_ Expr
a)     = Expr -> ()
forall a. NFData a => a -> ()
rnf Expr
a
  rnf (Quote Range
_)           = ()
  rnf (QuoteTerm Range
_)       = ()
  rnf (Tactic Range
_ Expr
a)        = Expr -> ()
forall a. NFData a => a -> ()
rnf Expr
a
  rnf (Unquote Range
_)         = ()
  rnf (DontCare Expr
a)        = Expr -> ()
forall a. NFData a => a -> ()
rnf Expr
a
  rnf (Equal Range
_ Expr
a Expr
b)       = Expr -> ()
forall a. NFData a => a -> ()
rnf Expr
a () -> () -> ()
forall a b. a -> b -> b
`seq` Expr -> ()
forall a. NFData a => a -> ()
rnf Expr
b
  rnf (Ellipsis Range
_)        = ()
  rnf (Generalized Expr
e)     = Expr -> ()
forall a. NFData a => a -> ()
rnf Expr
e
  rnf (KnownIdent NameKind
a QName
b)    = QName -> ()
forall a. NFData a => a -> ()
rnf QName
b
  rnf (KnownOpApp NameKind
a Range
b QName
c Set Name
d OpAppArgs
e) = NameKind -> ()
forall a. NFData a => a -> ()
rnf NameKind
a () -> () -> ()
forall a b. a -> b -> b
`seq` Range -> ()
forall a. NFData a => a -> ()
rnf Range
b () -> () -> ()
forall a b. a -> b -> b
`seq` QName -> ()
forall a. NFData a => a -> ()
rnf QName
c () -> () -> ()
forall a b. a -> b -> b
`seq` Set Name -> ()
forall a. NFData a => a -> ()
rnf Set Name
d () -> () -> ()
forall a b. a -> b -> b
`seq` QName -> ()
forall a. NFData a => a -> ()
rnf QName
c

-- | Ranges are not forced.

instance NFData Pattern where
  rnf :: Pattern -> ()
rnf (IdentP Bool
a QName
b)     = Bool -> ()
forall a. NFData a => a -> ()
rnf Bool
a () -> () -> ()
forall a b. a -> b -> b
`seq` QName -> ()
forall a. NFData a => a -> ()
rnf QName
b
  rnf (QuoteP Range
_)       = ()
  rnf (AppP Pattern
a NamedArg Pattern
b)       = Pattern -> ()
forall a. NFData a => a -> ()
rnf Pattern
a () -> () -> ()
forall a b. a -> b -> b
`seq` NamedArg Pattern -> ()
forall a. NFData a => a -> ()
rnf NamedArg Pattern
b
  rnf (RawAppP Range
_ List2 Pattern
a)    = List2 Pattern -> ()
forall a. NFData a => a -> ()
rnf List2 Pattern
a
  rnf (OpAppP Range
_ QName
a Set Name
b [NamedArg Pattern]
c) = QName -> ()
forall a. NFData a => a -> ()
rnf QName
a () -> () -> ()
forall a b. a -> b -> b
`seq` Set Name -> ()
forall a. NFData a => a -> ()
rnf Set Name
b () -> () -> ()
forall a b. a -> b -> b
`seq` [NamedArg Pattern] -> ()
forall a. NFData a => a -> ()
rnf [NamedArg Pattern]
c
  rnf (HiddenP Range
_ Named_ Pattern
a)    = Named_ Pattern -> ()
forall a. NFData a => a -> ()
rnf Named_ Pattern
a
  rnf (InstanceP Range
_ Named_ Pattern
a)  = Named_ Pattern -> ()
forall a. NFData a => a -> ()
rnf Named_ Pattern
a
  rnf (ParenP Range
_ Pattern
a)     = Pattern -> ()
forall a. NFData a => a -> ()
rnf Pattern
a
  rnf (WildP Range
_)        = ()
  rnf (AbsurdP Range
_)      = ()
  rnf (AsP Range
_ Name
a Pattern
b)      = Name -> ()
forall a. NFData a => a -> ()
rnf Name
a () -> () -> ()
forall a b. a -> b -> b
`seq` Pattern -> ()
forall a. NFData a => a -> ()
rnf Pattern
b
  rnf (DotP Range
_ Expr
a)       = Expr -> ()
forall a. NFData a => a -> ()
rnf Expr
a
  rnf (LitP Range
_ Literal
a)       = Literal -> ()
forall a. NFData a => a -> ()
rnf Literal
a
  rnf (RecP Range
_ [FieldAssignment' Pattern]
a)       = [FieldAssignment' Pattern] -> ()
forall a. NFData a => a -> ()
rnf [FieldAssignment' Pattern]
a
  rnf (EqualP Range
_ [(Expr, Expr)]
es)    = [(Expr, Expr)] -> ()
forall a. NFData a => a -> ()
rnf [(Expr, Expr)]
es
  rnf (EllipsisP Range
_ Maybe Pattern
mp) = Maybe Pattern -> ()
forall a. NFData a => a -> ()
rnf Maybe Pattern
mp
  rnf (WithP Range
_ Pattern
a)      = Pattern -> ()
forall a. NFData a => a -> ()
rnf Pattern
a

-- | Ranges are not forced.

instance NFData RecordDirective where
  rnf :: RecordDirective -> ()
rnf (Induction Ranged Induction
a)          = Ranged Induction -> ()
forall a. NFData a => a -> ()
rnf Ranged Induction
a
  rnf (Eta Ranged HasEta0
a    )            = Ranged HasEta0 -> ()
forall a. NFData a => a -> ()
rnf Ranged HasEta0
a
  rnf (Constructor Name
a IsInstance
b)      = (Name, IsInstance) -> ()
forall a. NFData a => a -> ()
rnf (Name
a, IsInstance
b)
  rnf (PatternOrCopattern Range
_) = ()

instance NFData Declaration where
  rnf :: Declaration -> ()
rnf (TypeSig ArgInfo
a TacticAttribute
b Name
c Expr
d)       = ArgInfo -> ()
forall a. NFData a => a -> ()
rnf ArgInfo
a () -> () -> ()
forall a b. a -> b -> b
`seq` TacticAttribute -> ()
forall a. NFData a => a -> ()
rnf TacticAttribute
b () -> () -> ()
forall a b. a -> b -> b
`seq` Name -> ()
forall a. NFData a => a -> ()
rnf Name
c () -> () -> ()
forall a b. a -> b -> b
`seq` Expr -> ()
forall a. NFData a => a -> ()
rnf Expr
d
  rnf (FieldSig IsInstance
a TacticAttribute
b Name
c Arg Expr
d)      = IsInstance -> ()
forall a. NFData a => a -> ()
rnf IsInstance
a () -> () -> ()
forall a b. a -> b -> b
`seq` TacticAttribute -> ()
forall a. NFData a => a -> ()
rnf TacticAttribute
b () -> () -> ()
forall a b. a -> b -> b
`seq` Name -> ()
forall a. NFData a => a -> ()
rnf Name
c () -> () -> ()
forall a b. a -> b -> b
`seq` Arg Expr -> ()
forall a. NFData a => a -> ()
rnf Arg Expr
d
  rnf (Generalize KwRange
_ [Declaration]
a)        = [Declaration] -> ()
forall a. NFData a => a -> ()
rnf [Declaration]
a
  rnf (Field KwRange
_ [Declaration]
fs)            = [Declaration] -> ()
forall a. NFData a => a -> ()
rnf [Declaration]
fs
  rnf (FunClause LHS
a RHS
b WhereClause
c Bool
d)     = LHS -> ()
forall a. NFData a => a -> ()
rnf LHS
a () -> () -> ()
forall a b. a -> b -> b
`seq` RHS -> ()
forall a. NFData a => a -> ()
rnf RHS
b () -> () -> ()
forall a b. a -> b -> b
`seq` WhereClause -> ()
forall a. NFData a => a -> ()
rnf WhereClause
c () -> () -> ()
forall a b. a -> b -> b
`seq` Bool -> ()
forall a. NFData a => a -> ()
rnf Bool
d
  rnf (DataSig Range
_ Erased
a Name
b [LamBinding]
c Expr
d)     = Erased -> ()
forall a. NFData a => a -> ()
rnf Erased
a () -> () -> ()
forall a b. a -> b -> b
`seq` Name -> ()
forall a. NFData a => a -> ()
rnf Name
b () -> () -> ()
forall a b. a -> b -> b
`seq` [LamBinding] -> ()
forall a. NFData a => a -> ()
rnf [LamBinding]
c () -> () -> ()
forall a b. a -> b -> b
`seq` Expr -> ()
forall a. NFData a => a -> ()
rnf Expr
d
  rnf (Data Range
_ Erased
a Name
b [LamBinding]
c Expr
d [Declaration]
e)      = Erased -> ()
forall a. NFData a => a -> ()
rnf Erased
a () -> () -> ()
forall a b. a -> b -> b
`seq` Name -> ()
forall a. NFData a => a -> ()
rnf Name
b () -> () -> ()
forall a b. a -> b -> b
`seq` [LamBinding] -> ()
forall a. NFData a => a -> ()
rnf [LamBinding]
c () -> () -> ()
forall a b. a -> b -> b
`seq` Expr -> ()
forall a. NFData a => a -> ()
rnf Expr
d
                                      () -> () -> ()
forall a b. a -> b -> b
`seq` [Declaration] -> ()
forall a. NFData a => a -> ()
rnf [Declaration]
e
  rnf (DataDef Range
_ Name
a [LamBinding]
b [Declaration]
c)       = Name -> ()
forall a. NFData a => a -> ()
rnf Name
a () -> () -> ()
forall a b. a -> b -> b
`seq` [LamBinding] -> ()
forall a. NFData a => a -> ()
rnf [LamBinding]
b () -> () -> ()
forall a b. a -> b -> b
`seq` [Declaration] -> ()
forall a. NFData a => a -> ()
rnf [Declaration]
c
  rnf (RecordSig Range
_ Erased
a Name
b [LamBinding]
c Expr
d)   = Erased -> ()
forall a. NFData a => a -> ()
rnf Erased
a () -> () -> ()
forall a b. a -> b -> b
`seq` Name -> ()
forall a. NFData a => a -> ()
rnf Name
b () -> () -> ()
forall a b. a -> b -> b
`seq` [LamBinding] -> ()
forall a. NFData a => a -> ()
rnf [LamBinding]
c () -> () -> ()
forall a b. a -> b -> b
`seq` Expr -> ()
forall a. NFData a => a -> ()
rnf Expr
d
  rnf (RecordDef Range
_ Name
a [RecordDirective]
b [LamBinding]
c [Declaration]
d)   = (Name, [RecordDirective], [LamBinding], [Declaration]) -> ()
forall a. NFData a => a -> ()
rnf (Name
a, [RecordDirective]
b, [LamBinding]
c, [Declaration]
d)
  rnf (Record Range
_ Erased
a Name
b [RecordDirective]
c [LamBinding]
d Expr
e [Declaration]
f)  = (Erased, Name, [RecordDirective], [LamBinding], Expr,
 [Declaration])
-> ()
forall a. NFData a => a -> ()
rnf (Erased
a, Name
b, [RecordDirective]
c, [LamBinding]
d, Expr
e, [Declaration]
f)
  rnf (Infix Fixity
a List1 Name
b)             = Fixity -> ()
forall a. NFData a => a -> ()
rnf Fixity
a () -> () -> ()
forall a b. a -> b -> b
`seq` List1 Name -> ()
forall a. NFData a => a -> ()
rnf List1 Name
b
  rnf (Syntax Name
a Notation
b)            = Name -> ()
forall a. NFData a => a -> ()
rnf Name
a () -> () -> ()
forall a b. a -> b -> b
`seq` Notation -> ()
forall a. NFData a => a -> ()
rnf Notation
b
  rnf (PatternSyn Range
_ Name
a [WithHiding Name]
b Pattern
c)    = Name -> ()
forall a. NFData a => a -> ()
rnf Name
a () -> () -> ()
forall a b. a -> b -> b
`seq` [WithHiding Name] -> ()
forall a. NFData a => a -> ()
rnf [WithHiding Name]
b () -> () -> ()
forall a b. a -> b -> b
`seq` Pattern -> ()
forall a. NFData a => a -> ()
rnf Pattern
c
  rnf (Mutual KwRange
_ [Declaration]
a)            = [Declaration] -> ()
forall a. NFData a => a -> ()
rnf [Declaration]
a
  rnf (InterleavedMutual KwRange
_ [Declaration]
a) = [Declaration] -> ()
forall a. NFData a => a -> ()
rnf [Declaration]
a
  rnf (LoneConstructor KwRange
_ [Declaration]
a)   = [Declaration] -> ()
forall a. NFData a => a -> ()
rnf [Declaration]
a
  rnf (Abstract KwRange
_ [Declaration]
a)          = [Declaration] -> ()
forall a. NFData a => a -> ()
rnf [Declaration]
a
  rnf (Private KwRange
_ Origin
_ [Declaration]
a)         = [Declaration] -> ()
forall a. NFData a => a -> ()
rnf [Declaration]
a
  rnf (InstanceB KwRange
_ [Declaration]
a)         = [Declaration] -> ()
forall a. NFData a => a -> ()
rnf [Declaration]
a
  rnf (Macro KwRange
_ [Declaration]
a)             = [Declaration] -> ()
forall a. NFData a => a -> ()
rnf [Declaration]
a
  rnf (Postulate KwRange
_ [Declaration]
a)         = [Declaration] -> ()
forall a. NFData a => a -> ()
rnf [Declaration]
a
  rnf (Primitive KwRange
_ [Declaration]
a)         = [Declaration] -> ()
forall a. NFData a => a -> ()
rnf [Declaration]
a
  rnf (Open Range
_ QName
a ImportDirective
b)            = QName -> ()
forall a. NFData a => a -> ()
rnf QName
a () -> () -> ()
forall a b. a -> b -> b
`seq` ImportDirective -> ()
forall a. NFData a => a -> ()
rnf ImportDirective
b
  rnf (Import Range
_ QName
a Maybe AsName
b OpenShortHand
_ ImportDirective
c)      = QName -> ()
forall a. NFData a => a -> ()
rnf QName
a () -> () -> ()
forall a b. a -> b -> b
`seq` Maybe AsName -> ()
forall a. NFData a => a -> ()
rnf Maybe AsName
b () -> () -> ()
forall a b. a -> b -> b
`seq` ImportDirective -> ()
forall a. NFData a => a -> ()
rnf ImportDirective
c
  rnf (ModuleMacro Range
_ Erased
a Name
b ModuleApplication
c OpenShortHand
_ ImportDirective
d)
                              = Erased -> ()
forall a. NFData a => a -> ()
rnf Erased
a () -> () -> ()
forall a b. a -> b -> b
`seq` Name -> ()
forall a. NFData a => a -> ()
rnf Name
b () -> () -> ()
forall a b. a -> b -> b
`seq` ModuleApplication -> ()
forall a. NFData a => a -> ()
rnf ModuleApplication
c () -> () -> ()
forall a b. a -> b -> b
`seq` ImportDirective -> ()
forall a. NFData a => a -> ()
rnf ImportDirective
d
  rnf (Module Range
_ Erased
a QName
b Telescope
c [Declaration]
d)      = Erased -> ()
forall a. NFData a => a -> ()
rnf Erased
a () -> () -> ()
forall a b. a -> b -> b
`seq` QName -> ()
forall a. NFData a => a -> ()
rnf QName
b () -> () -> ()
forall a b. a -> b -> b
`seq` Telescope -> ()
forall a. NFData a => a -> ()
rnf Telescope
c () -> () -> ()
forall a b. a -> b -> b
`seq` [Declaration] -> ()
forall a. NFData a => a -> ()
rnf [Declaration]
d
  rnf (UnquoteDecl Range
_ [Name]
a Expr
b)     = [Name] -> ()
forall a. NFData a => a -> ()
rnf [Name]
a () -> () -> ()
forall a b. a -> b -> b
`seq` Expr -> ()
forall a. NFData a => a -> ()
rnf Expr
b
  rnf (UnquoteDef Range
_ [Name]
a Expr
b)      = [Name] -> ()
forall a. NFData a => a -> ()
rnf [Name]
a () -> () -> ()
forall a b. a -> b -> b
`seq` Expr -> ()
forall a. NFData a => a -> ()
rnf Expr
b
  rnf (UnquoteData Range
_ Name
a [Name]
b Expr
c)   = Name -> ()
forall a. NFData a => a -> ()
rnf Name
a () -> () -> ()
forall a b. a -> b -> b
`seq` [Name] -> ()
forall a. NFData a => a -> ()
rnf [Name]
b () -> () -> ()
forall a b. a -> b -> b
`seq` Expr -> ()
forall a. NFData a => a -> ()
rnf Expr
c
  rnf (Pragma Pragma
a)              = Pragma -> ()
forall a. NFData a => a -> ()
rnf Pragma
a
  rnf (Opaque KwRange
r [Declaration]
xs)           = KwRange -> ()
forall a. NFData a => a -> ()
rnf KwRange
r () -> () -> ()
forall a b. a -> b -> b
`seq` [Declaration] -> ()
forall a. NFData a => a -> ()
rnf [Declaration]
xs
  rnf (Unfolding KwRange
r [QName]
xs)        = KwRange -> ()
forall a. NFData a => a -> ()
rnf KwRange
r () -> () -> ()
forall a b. a -> b -> b
`seq` [QName] -> ()
forall a. NFData a => a -> ()
rnf [QName]
xs

instance NFData OpenShortHand

-- | Ranges are not forced.

instance NFData Pragma where
  rnf :: Pragma -> ()
rnf (OptionsPragma Range
_ [String]
a)               = [String] -> ()
forall a. NFData a => a -> ()
rnf [String]
a
  rnf (BuiltinPragma Range
_ Ranged String
a QName
b)             = Ranged String -> ()
forall a. NFData a => a -> ()
rnf Ranged String
a () -> () -> ()
forall a b. a -> b -> b
`seq` QName -> ()
forall a. NFData a => a -> ()
rnf QName
b
  rnf (RewritePragma Range
_ Range
_ [QName]
a)             = [QName] -> ()
forall a. NFData a => a -> ()
rnf [QName]
a
  rnf (CompilePragma Range
_ Ranged String
a QName
b String
c)           = Ranged String -> ()
forall a. NFData a => a -> ()
rnf Ranged String
a () -> () -> ()
forall a b. a -> b -> b
`seq` QName -> ()
forall a. NFData a => a -> ()
rnf QName
b () -> () -> ()
forall a b. a -> b -> b
`seq` String -> ()
forall a. NFData a => a -> ()
rnf String
c
  rnf (ForeignPragma Range
_ Ranged String
b String
s)             = Ranged String -> ()
forall a. NFData a => a -> ()
rnf Ranged String
b () -> () -> ()
forall a b. a -> b -> b
`seq` String -> ()
forall a. NFData a => a -> ()
rnf String
s
  rnf (StaticPragma Range
_ QName
a)                = QName -> ()
forall a. NFData a => a -> ()
rnf QName
a
  rnf (InjectivePragma Range
_ QName
a)             = QName -> ()
forall a. NFData a => a -> ()
rnf QName
a
  rnf (InjectiveForInferencePragma Range
_ QName
a) = QName -> ()
forall a. NFData a => a -> ()
rnf QName
a
  rnf (InlinePragma Range
_ Bool
_ QName
a)              = QName -> ()
forall a. NFData a => a -> ()
rnf QName
a
  rnf (ImpossiblePragma Range
_ [String]
a)            = [String] -> ()
forall a. NFData a => a -> ()
rnf [String]
a
  rnf (EtaPragma Range
_ QName
a)                   = QName -> ()
forall a. NFData a => a -> ()
rnf QName
a
  rnf (TerminationCheckPragma Range
_ TerminationCheck Name
a)      = TerminationCheck Name -> ()
forall a. NFData a => a -> ()
rnf TerminationCheck Name
a
  rnf (NoCoverageCheckPragma Range
_)         = ()
  rnf (WarningOnUsage Range
_ QName
a Text
b)            = QName -> ()
forall a. NFData a => a -> ()
rnf QName
a () -> () -> ()
forall a b. a -> b -> b
`seq` Text -> ()
forall a. NFData a => a -> ()
rnf Text
b
  rnf (WarningOnImport Range
_ Text
a)             = Text -> ()
forall a. NFData a => a -> ()
rnf Text
a
  rnf (CatchallPragma Range
_)                = ()
  rnf (DisplayPragma Range
_ Pattern
a Expr
b)             = Pattern -> ()
forall a. NFData a => a -> ()
rnf Pattern
a () -> () -> ()
forall a b. a -> b -> b
`seq` Expr -> ()
forall a. NFData a => a -> ()
rnf Expr
b
  rnf (NoPositivityCheckPragma Range
_)       = ()
  rnf (PolarityPragma Range
_ Name
a [Occurrence]
b)            = Name -> ()
forall a. NFData a => a -> ()
rnf Name
a () -> () -> ()
forall a b. a -> b -> b
`seq` [Occurrence] -> ()
forall a. NFData a => a -> ()
rnf [Occurrence]
b
  rnf (NoUniverseCheckPragma Range
_)         = ()
  rnf (NotProjectionLikePragma Range
_ QName
q)     = QName -> ()
forall a. NFData a => a -> ()
rnf QName
q
  rnf (OverlapPragma Range
_ [QName]
q OverlapMode
i)             = [QName] -> ()
forall a. NFData a => a -> ()
rnf [QName]
q () -> () -> ()
forall a b. a -> b -> b
`seq` OverlapMode -> ()
forall a. NFData a => a -> ()
rnf OverlapMode
i

-- | Ranges are not forced.

instance NFData AsName where
  rnf :: AsName -> ()
rnf (AsName Either Expr Name
a Range
_) = Either Expr Name -> ()
forall a. NFData a => a -> ()
rnf Either Expr Name
a

-- | Ranges are not forced.

instance NFData a => NFData (TypedBinding' a) where
  rnf :: TypedBinding' a -> ()
rnf (TBind Range
_ List1 (NamedArg Binder)
a a
b) = List1 (NamedArg Binder) -> ()
forall a. NFData a => a -> ()
rnf List1 (NamedArg Binder)
a () -> () -> ()
forall a b. a -> b -> b
`seq` a -> ()
forall a. NFData a => a -> ()
rnf a
b
  rnf (TLet Range
_ List1 Declaration
a)    = List1 Declaration -> ()
forall a. NFData a => a -> ()
rnf List1 Declaration
a

-- | Ranges are not forced.

instance NFData ModuleApplication where
  rnf :: ModuleApplication -> ()
rnf (SectionApp Range
_ Telescope
a Expr
b)    = Telescope -> ()
forall a. NFData a => a -> ()
rnf Telescope
a () -> () -> ()
forall a b. a -> b -> b
`seq` Expr -> ()
forall a. NFData a => a -> ()
rnf Expr
b
  rnf (RecordModuleInstance Range
_ QName
a) = QName -> ()
forall a. NFData a => a -> ()
rnf QName
a

-- | Ranges are not forced.

instance NFData a => NFData (OpApp a) where
  rnf :: OpApp a -> ()
rnf (SyntaxBindingLambda Range
_ List1 LamBinding
a a
b) = List1 LamBinding -> ()
forall a. NFData a => a -> ()
rnf List1 LamBinding
a () -> () -> ()
forall a b. a -> b -> b
`seq` a -> ()
forall a. NFData a => a -> ()
rnf a
b
  rnf (Ordinary a
a)                = a -> ()
forall a. NFData a => a -> ()
rnf a
a

-- | Ranges are not forced.

instance NFData LHS where
  rnf :: LHS -> ()
rnf (LHS Pattern
a [RewriteEqn]
b [WithExpr]
c) = Pattern -> ()
forall a. NFData a => a -> ()
rnf Pattern
a () -> () -> ()
forall a b. a -> b -> b
`seq` [RewriteEqn] -> ()
forall a. NFData a => a -> ()
rnf [RewriteEqn]
b () -> () -> ()
forall a b. a -> b -> b
`seq` [WithExpr] -> ()
forall a. NFData a => a -> ()
rnf [WithExpr]
c

instance NFData a => NFData (FieldAssignment' a) where
  rnf :: FieldAssignment' a -> ()
rnf (FieldAssignment Name
a a
b) = Name -> ()
forall a. NFData a => a -> ()
rnf Name
a () -> () -> ()
forall a b. a -> b -> b
`seq` a -> ()
forall a. NFData a => a -> ()
rnf a
b

instance NFData ModuleAssignment where
  rnf :: ModuleAssignment -> ()
rnf (ModuleAssignment QName
a [Expr]
b ImportDirective
c) = QName -> ()
forall a. NFData a => a -> ()
rnf QName
a () -> () -> ()
forall a b. a -> b -> b
`seq` [Expr] -> ()
forall a. NFData a => a -> ()
rnf [Expr]
b () -> () -> ()
forall a b. a -> b -> b
`seq` ImportDirective -> ()
forall a. NFData a => a -> ()
rnf ImportDirective
c

instance NFData a => NFData (WhereClause' a) where
  rnf :: WhereClause' a -> ()
rnf WhereClause' a
NoWhere               = ()
  rnf (AnyWhere Range
_ a
a)        = a -> ()
forall a. NFData a => a -> ()
rnf a
a
  rnf (SomeWhere Range
_ Erased
a Name
b Access
c a
d) = Erased -> ()
forall a. NFData a => a -> ()
rnf Erased
a () -> () -> ()
forall a b. a -> b -> b
`seq` Name -> ()
forall a. NFData a => a -> ()
rnf Name
b () -> () -> ()
forall a b. a -> b -> b
`seq` Access -> ()
forall a. NFData a => a -> ()
rnf Access
c () -> () -> ()
forall a b. a -> b -> b
`seq` a -> ()
forall a. NFData a => a -> ()
rnf a
d

instance NFData LamClause where
  rnf :: LamClause -> ()
rnf (LamClause [Pattern]
a RHS
b Bool
c) = ([Pattern], RHS, Bool) -> ()
forall a. NFData a => a -> ()
rnf ([Pattern]
a, RHS
b, Bool
c)

instance NFData a => NFData (LamBinding' a) where
  rnf :: LamBinding' a -> ()
rnf (DomainFree NamedArg Binder
a) = NamedArg Binder -> ()
forall a. NFData a => a -> ()
rnf NamedArg Binder
a
  rnf (DomainFull a
a) = a -> ()
forall a. NFData a => a -> ()
rnf a
a

instance NFData Binder where
  rnf :: Binder -> ()
rnf (Binder Maybe Pattern
a BoundName
b) = Maybe Pattern -> ()
forall a. NFData a => a -> ()
rnf Maybe Pattern
a () -> () -> ()
forall a b. a -> b -> b
`seq` BoundName -> ()
forall a. NFData a => a -> ()
rnf BoundName
b

instance NFData BoundName where
  rnf :: BoundName -> ()
rnf (BName Name
a Fixity'
b TacticAttribute
c Bool
d) = Name -> ()
forall a. NFData a => a -> ()
rnf Name
a () -> () -> ()
forall a b. a -> b -> b
`seq` Fixity' -> ()
forall a. NFData a => a -> ()
rnf Fixity'
b () -> () -> ()
forall a b. a -> b -> b
`seq` TacticAttribute -> ()
forall a. NFData a => a -> ()
rnf TacticAttribute
c () -> () -> ()
forall a b. a -> b -> b
`seq` Bool -> ()
forall a. NFData a => a -> ()
rnf Bool
d

instance NFData a => NFData (RHS' a) where
  rnf :: RHS' a -> ()
rnf RHS' a
AbsurdRHS = ()
  rnf (RHS a
a)   = a -> ()
forall a. NFData a => a -> ()
rnf a
a

instance NFData DoStmt where
  rnf :: DoStmt -> ()
rnf (DoBind Range
_ Pattern
p Expr
e [LamClause]
w) = (Pattern, Expr, [LamClause]) -> ()
forall a. NFData a => a -> ()
rnf (Pattern
p, Expr
e, [LamClause]
w)
  rnf (DoThen Expr
e)       = Expr -> ()
forall a. NFData a => a -> ()
rnf Expr
e
  rnf (DoLet Range
_ List1 Declaration
ds)     = List1 Declaration -> ()
forall a. NFData a => a -> ()
rnf List1 Declaration
ds