{-# LANGUAGE CPP #-}
{-# LANGUAGE ApplicativeDo #-}
module Agda.Syntax.Concrete
(
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
, 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
, 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 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
| 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 }
data Expr
= Ident QName
| Lit Range Literal
| QuestionMark Range (Maybe Nat)
| Underscore Range (Maybe String)
| RawApp Range (List2 Expr)
| App Range Expr (NamedArg Expr)
| OpApp Range QName (Set A.Name) OpAppArgs
| WithApp Range Expr [Expr]
| HiddenArg Range (Named_ Expr)
| InstanceArg Range (Named_ Expr)
| Lam Range (List1 LamBinding) Expr
| AbsurdLam Range Hiding
| ExtendedLam Range Erased
(List1 LamClause)
| Fun Range (Arg Expr) Expr
| Pi Telescope1 Expr
| Rec Range RecordAssignments
| RecUpdate Range Expr [FieldAssignment]
| Let Range (List1 Declaration) (Maybe Expr)
| Paren Range Expr
| IdiomBrackets Range [Expr]
| DoBlock Range (List1 DoStmt)
| Absurd Range
| As Range Name Expr
| Dot Range Expr
| DoubleDot Range Expr
| Quote Range
| QuoteTerm Range
| Tactic Range Expr
| Unquote Range
| DontCare Expr
| Equal Range Expr Expr
| Ellipsis Range
| KnownIdent NameKind QName
| KnownOpApp NameKind Range QName (Set A.Name) OpAppArgs
| 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))]
data Pattern
= IdentP Bool QName
| QuoteP Range
| AppP Pattern (NamedArg Pattern)
| RawAppP Range (List2 Pattern)
| OpAppP Range QName (Set A.Name)
[NamedArg Pattern]
| HiddenP Range (Named_ Pattern)
| InstanceP Range (Named_ Pattern)
| ParenP Range Pattern
| WildP Range
| AbsurdP Range
| AsP Range Name Pattern
| DotP Range Expr
| LitP Range Literal
| RecP Range [FieldAssignment' Pattern]
| EqualP Range [(Expr,Expr)]
| EllipsisP Range (Maybe Pattern)
| WithP Range Pattern
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]
| 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
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
type LamBinding = LamBinding' TypedBinding
data LamBinding' a
= DomainFree (NamedArg Binder)
| DomainFull a
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)
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
, BoundName -> Bool
bnameIsFinite :: Bool
}
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
type TypedBinding = TypedBinding' Expr
data TypedBinding' e
= TBind Range (List1 (NamedArg Binder)) e
| TLet Range (List1 Declaration)
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)
type Telescope1 = List1 TypedBinding
type Telescope = [TypedBinding]
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
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)
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
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)
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)
data LHS = LHS
{ LHS -> Pattern
lhsOriginalPattern :: Pattern
, LHS -> [RewriteEqn]
lhsRewriteEqn :: [RewriteEqn]
, LHS -> [WithExpr]
lhsWithExpr :: [WithExpr]
}
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)
data LHSCore
= LHSHead { LHSCore -> QName
lhsDefName :: QName
, LHSCore -> [NamedArg Pattern]
lhsPats :: [NamedArg Pattern]
}
| LHSProj { LHSCore -> QName
lhsDestructor :: QName
, LHSCore -> [NamedArg Pattern]
lhsPatsLeft :: [NamedArg Pattern]
, LHSCore -> NamedArg LHSCore
lhsFocus :: NamedArg LHSCore
, lhsPats :: [NamedArg Pattern]
}
| LHSWith { LHSCore -> LHSCore
lhsHead :: LHSCore
, LHSCore -> [Pattern]
lhsWithPatterns :: [Pattern]
, lhsPats :: [NamedArg Pattern]
}
| LHSEllipsis
{ LHSCore -> Range
lhsEllipsisRange :: Range
, LHSCore -> LHSCore
lhsEllipsisPat :: LHSCore
}
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
| 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)
type WhereClause = WhereClause' [Declaration]
data WhereClause' decls
= NoWhere
| AnyWhere Range decls
| SomeWhere Range Erased Name Access decls
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]
, 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
data ExprWhere = ExprWhere Expr WhereClause
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
type ImportedName = ImportedName' Name Name
data AsName' a = AsName
{ forall a. AsName' a -> a
asName :: a
, forall a. AsName' a -> Range
asRange :: Range
}
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)
type AsName = AsName' (Either Expr Name)
type TypeSignature = Declaration
type FieldSignature = Declaration
type TypeSignatureOrInstanceBlock = Declaration
data RecordDirective
= Induction (Ranged Induction)
| Constructor Name IsInstance
| Eta (Ranged HasEta0)
| PatternOrCopattern 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
]
data Declaration
= TypeSig ArgInfo TacticAttribute Name Expr
| FieldSig IsInstance TacticAttribute Name (Arg Expr)
| Generalize KwRange [TypeSignature]
| Field KwRange [FieldSignature]
| FunClause LHS RHS WhereClause Bool
| DataSig Range Erased Name [LamBinding] Expr
| Data Range Erased Name [LamBinding] Expr
[TypeSignatureOrInstanceBlock]
| DataDef Range Name [LamBinding] [TypeSignatureOrInstanceBlock]
| RecordSig Range Erased Name [LamBinding] Expr
| RecordDef Range Name [RecordDirective] [LamBinding] [Declaration]
| Record Range Erased Name [RecordDirective] [LamBinding] Expr
[Declaration]
| Infix Fixity (List1 Name)
| Syntax Name Notation
| PatternSyn Range Name [WithHiding Name] Pattern
| Mutual KwRange [Declaration]
| InterleavedMutual KwRange [Declaration]
| Abstract KwRange [Declaration]
| Private KwRange Origin [Declaration]
| InstanceB KwRange [Declaration]
| 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
| UnquoteDef Range [Name] Expr
| UnquoteData Range Name [Name] Expr
| Pragma Pragma
| Opaque KwRange [Declaration]
| Unfolding KwRange [QName]
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
{-# 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
| RecordModuleInstance Range QName
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)
data Pragma
= OptionsPragma Range [String]
| BuiltinPragma Range RString QName
| RewritePragma Range Range [QName]
| ForeignPragma Range RString String
| CompilePragma Range RString QName String
| StaticPragma Range QName
| InlinePragma Range Bool QName
| ImpossiblePragma Range [String]
| EtaPragma Range QName
| WarningOnUsage Range QName Text
| WarningOnImport Range Text
| InjectivePragma Range QName
| InjectiveForInferencePragma Range QName
| DisplayPragma Range Pattern Expr
| CatchallPragma Range
| TerminationCheckPragma Range (TerminationCheck Name)
| NoCoverageCheckPragma Range
| NoPositivityCheckPragma Range
| PolarityPragma Range Name [Occurrence]
| NoUniverseCheckPragma Range
| NotProjectionLikePragma Range QName
| OverlapPragma Range [QName] OverlapMode
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
data Module = Mod
{ Module -> [Pragma]
modPragmas :: [Pragma]
, Module -> [Declaration]
modDecls :: [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
data HoleContent' qn nm p e
= HoleContentExpr e
| HoleContentRewrite [RewriteEqn' qn nm p e]
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
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
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
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
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)
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
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)
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)
exprToPattern :: Applicative m
=> (Expr -> m Pattern)
-> Expr
-> m Pattern
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
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)
| 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 Range
r Expr
e [Expr]
es -> do
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
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
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
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
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
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
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
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 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
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
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
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
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
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
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
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
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
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
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
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