module Agda.Syntax.Abstract
( module Agda.Syntax.Abstract
, module Agda.Syntax.Abstract.Name
) where
import Prelude hiding (null)
import Control.DeepSeq
import Data.Bifunctor
import qualified Data.Foldable as Fold
import Data.Function (on)
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Maybe
import qualified Data.Set as Set
import Data.Set (Set)
import Data.Void
import GHC.Generics (Generic)
import Agda.Syntax.Concrete (FieldAssignment'(..))
import qualified Agda.Syntax.Concrete as C
import Agda.Syntax.Abstract.Name
import qualified Agda.Syntax.Internal as I
import Agda.Syntax.Common
import Agda.Syntax.Info
import Agda.Syntax.Literal
import Agda.Syntax.Position
import Agda.Syntax.Scope.Base
import Agda.TypeChecking.Positivity.Occurrence
import Agda.Utils.List1 (List1, pattern (:|))
import qualified Agda.Utils.List1 as List1
import Agda.Utils.Null
import Agda.Syntax.Common.Pretty
import Agda.Utils.Impossible
newtype BindName = BindName { BindName -> Name
unBind :: Name }
deriving (Int -> BindName -> ShowS
[BindName] -> ShowS
BindName -> ArgName
forall a.
(Int -> a -> ShowS) -> (a -> ArgName) -> ([a] -> ShowS) -> Show a
showList :: [BindName] -> ShowS
$cshowList :: [BindName] -> ShowS
show :: BindName -> ArgName
$cshow :: BindName -> ArgName
showsPrec :: Int -> BindName -> ShowS
$cshowsPrec :: Int -> BindName -> ShowS
Show, BindName -> Range
forall a. (a -> Range) -> HasRange a
getRange :: BindName -> Range
$cgetRange :: BindName -> Range
HasRange, KillRangeT BindName
forall a. KillRangeT a -> KillRange a
killRange :: KillRangeT BindName
$ckillRange :: KillRangeT BindName
KillRange, HasRange BindName
Range -> KillRangeT BindName
forall a. HasRange a -> (Range -> a -> a) -> SetRange a
setRange :: Range -> KillRangeT BindName
$csetRange :: Range -> KillRangeT BindName
SetRange, BindName -> ()
forall a. (a -> ()) -> NFData a
rnf :: BindName -> ()
$crnf :: BindName -> ()
NFData)
mkBindName :: Name -> BindName
mkBindName :: Name -> BindName
mkBindName Name
x = Name -> BindName
BindName Name
x
instance Eq BindName where
BindName Name
n == :: BindName -> BindName -> Bool
== BindName Name
m
= (forall a. Eq a => a -> a -> Bool
(==) forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` Name -> NameId
nameId) Name
n Name
m
Bool -> Bool -> Bool
&& (forall a. Eq a => a -> a -> Bool
(==) forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` Name -> Name
nameConcrete) Name
n Name
m
instance Ord BindName where
BindName Name
n compare :: BindName -> BindName -> Ordering
`compare` BindName Name
m
= (forall a. Ord a => a -> a -> Ordering
compare forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` Name -> NameId
nameId) Name
n Name
m
forall a. Monoid a => a -> a -> a
`mappend` (forall a. Ord a => a -> a -> Ordering
compare forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` Name -> Name
nameConcrete) Name
n Name
m
type Args = [NamedArg Expr]
type Type = Expr
data Expr
= Var Name
| Def' QName Suffix
| Proj ProjOrigin AmbiguousQName
| Con AmbiguousQName
| PatternSyn AmbiguousQName
| Macro QName
| Lit ExprInfo Literal
| QuestionMark MetaInfo InteractionId
| Underscore MetaInfo
| Dot ExprInfo Expr
| App AppInfo Expr (NamedArg Expr)
| WithApp ExprInfo Expr [Expr]
| Lam ExprInfo LamBinding Expr
| AbsurdLam ExprInfo Hiding
| ExtendedLam ExprInfo DefInfo Erased QName (List1 Clause)
| Pi ExprInfo Telescope1 Type
| Generalized (Set QName) Type
| Fun ExprInfo (Arg Type) Type
| Let ExprInfo (List1 LetBinding) Expr
| Rec ExprInfo RecordAssigns
| RecUpdate ExprInfo Expr Assigns
| ScopedExpr ScopeInfo Expr
| Quote ExprInfo
| QuoteTerm ExprInfo
| Unquote ExprInfo
| DontCare Expr
deriving (Int -> Expr -> ShowS
[Expr] -> ShowS
Expr -> ArgName
forall a.
(Int -> a -> ShowS) -> (a -> ArgName) -> ([a] -> ShowS) -> Show a
showList :: [Expr] -> ShowS
$cshowList :: [Expr] -> ShowS
show :: Expr -> ArgName
$cshow :: Expr -> ArgName
showsPrec :: Int -> Expr -> ShowS
$cshowsPrec :: Int -> Expr -> ShowS
Show, forall x. Rep Expr x -> Expr
forall x. Expr -> Rep Expr x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Expr x -> Expr
$cfrom :: forall x. Expr -> Rep Expr x
Generic)
pattern Def :: QName -> Expr
pattern $bDef :: QName -> Expr
$mDef :: forall {r}. Expr -> (QName -> r) -> ((# #) -> r) -> r
Def x = Def' x NoSuffix
generalized :: Set QName -> Type -> Type
generalized :: Set QName -> Expr -> Expr
generalized Set QName
s Expr
e
| forall a. Null a => a -> Bool
null Set QName
s = Expr
e
| Bool
otherwise = Set QName -> Expr -> Expr
Generalized Set QName
s Expr
e
type Assign = FieldAssignment' Expr
type Assigns = [Assign]
type RecordAssign = Either Assign ModuleName
type RecordAssigns = [RecordAssign]
type Ren a = Map a (List1 a)
data ScopeCopyInfo = ScopeCopyInfo
{ ScopeCopyInfo -> Ren ModuleName
renModules :: Ren ModuleName
, ScopeCopyInfo -> Ren QName
renNames :: Ren QName }
deriving (ScopeCopyInfo -> ScopeCopyInfo -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ScopeCopyInfo -> ScopeCopyInfo -> Bool
$c/= :: ScopeCopyInfo -> ScopeCopyInfo -> Bool
== :: ScopeCopyInfo -> ScopeCopyInfo -> Bool
$c== :: ScopeCopyInfo -> ScopeCopyInfo -> Bool
Eq, Int -> ScopeCopyInfo -> ShowS
[ScopeCopyInfo] -> ShowS
ScopeCopyInfo -> ArgName
forall a.
(Int -> a -> ShowS) -> (a -> ArgName) -> ([a] -> ShowS) -> Show a
showList :: [ScopeCopyInfo] -> ShowS
$cshowList :: [ScopeCopyInfo] -> ShowS
show :: ScopeCopyInfo -> ArgName
$cshow :: ScopeCopyInfo -> ArgName
showsPrec :: Int -> ScopeCopyInfo -> ShowS
$cshowsPrec :: Int -> ScopeCopyInfo -> ShowS
Show, forall x. Rep ScopeCopyInfo x -> ScopeCopyInfo
forall x. ScopeCopyInfo -> Rep ScopeCopyInfo x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep ScopeCopyInfo x -> ScopeCopyInfo
$cfrom :: forall x. ScopeCopyInfo -> Rep ScopeCopyInfo x
Generic)
initCopyInfo :: ScopeCopyInfo
initCopyInfo :: ScopeCopyInfo
initCopyInfo = ScopeCopyInfo
{ renModules :: Ren ModuleName
renModules = forall a. Monoid a => a
mempty
, renNames :: Ren QName
renNames = forall a. Monoid a => a
mempty
}
instance Pretty ScopeCopyInfo where
pretty :: ScopeCopyInfo -> Doc
pretty ScopeCopyInfo
i = forall (t :: * -> *). Foldable t => t Doc -> Doc
vcat [ forall {l} {a}.
(IsList l, Pretty a, Pretty (Item l)) =>
ArgName -> Map a l -> Doc
prRen ArgName
"renModules =" (ScopeCopyInfo -> Ren ModuleName
renModules ScopeCopyInfo
i)
, forall {l} {a}.
(IsList l, Pretty a, Pretty (Item l)) =>
ArgName -> Map a l -> Doc
prRen ArgName
"renNames =" (ScopeCopyInfo -> Ren QName
renNames ScopeCopyInfo
i) ]
where
prRen :: ArgName -> Map a l -> Doc
prRen ArgName
s Map a l
r = forall (t :: * -> *). Foldable t => t Doc -> Doc
sep [ forall a. ArgName -> Doc a
text ArgName
s, forall a. Int -> Doc a -> Doc a
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *). Foldable t => t Doc -> Doc
vcat (forall a b. (a -> b) -> [a] -> [b]
map forall {a} {a}. (Pretty a, Pretty a) => (a, a) -> Doc
pr [(a, Item l)]
xs) ]
where
xs :: [(a, Item l)]
xs = [ (a
k, Item l
v) | (a
k, l
vs) <- forall k a. Map k a -> [(k, a)]
Map.toList Map a l
r, Item l
v <- forall l. IsList l => l -> [Item l]
List1.toList l
vs ]
pr :: (a, a) -> Doc
pr (a
x, a
y) = forall a. Pretty a => a -> Doc
pretty a
x forall a. Doc a -> Doc a -> Doc a
<+> Doc
"->" forall a. Doc a -> Doc a -> Doc a
<+> forall a. Pretty a => a -> Doc
pretty a
y
type RecordDirectives = RecordDirectives' QName
data Declaration
= Axiom KindOfName DefInfo ArgInfo (Maybe [Occurrence]) QName Type
| Generalize (Set QName) DefInfo ArgInfo QName Type
| Field DefInfo QName (Arg Type)
| Primitive DefInfo QName (Arg Type)
| Mutual MutualInfo [Declaration]
| Section Range Erased ModuleName GeneralizeTelescope [Declaration]
| Apply ModuleInfo Erased ModuleName ModuleApplication
ScopeCopyInfo ImportDirective
| Import ModuleInfo ModuleName ImportDirective
| Pragma Range Pragma
| Open ModuleInfo ModuleName ImportDirective
| FunDef DefInfo QName [Clause]
| DataSig DefInfo Erased QName GeneralizeTelescope Type
| DataDef DefInfo QName UniverseCheck DataDefParams [Constructor]
| RecSig DefInfo Erased QName GeneralizeTelescope Type
| RecDef DefInfo QName UniverseCheck RecordDirectives DataDefParams Type [Declaration]
| PatternSynDef QName [Arg BindName] (Pattern' Void)
| UnquoteDecl MutualInfo [DefInfo] [QName] Expr
| UnquoteDef [DefInfo] [QName] Expr
| UnquoteData [DefInfo] QName UniverseCheck [DefInfo] [QName] Expr
| ScopedDecl ScopeInfo [Declaration]
| UnfoldingDecl Range [QName]
deriving (Int -> Declaration -> ShowS
[Declaration] -> ShowS
Declaration -> ArgName
forall a.
(Int -> a -> ShowS) -> (a -> ArgName) -> ([a] -> ShowS) -> Show a
showList :: [Declaration] -> ShowS
$cshowList :: [Declaration] -> ShowS
show :: Declaration -> ArgName
$cshow :: Declaration -> ArgName
showsPrec :: Int -> Declaration -> ShowS
$cshowsPrec :: Int -> Declaration -> ShowS
Show, forall x. Rep Declaration x -> Declaration
forall x. Declaration -> Rep Declaration x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Declaration x -> Declaration
$cfrom :: forall x. Declaration -> Rep Declaration x
Generic)
type DefInfo = DefInfo' Expr
type ImportDirective = ImportDirective' QName ModuleName
type Renaming = Renaming' QName ModuleName
type ImportedName = ImportedName' QName ModuleName
data ModuleApplication
= SectionApp Telescope ModuleName [NamedArg Expr]
| RecordModuleInstance ModuleName
deriving (Int -> ModuleApplication -> ShowS
[ModuleApplication] -> ShowS
ModuleApplication -> ArgName
forall a.
(Int -> a -> ShowS) -> (a -> ArgName) -> ([a] -> ShowS) -> Show a
showList :: [ModuleApplication] -> ShowS
$cshowList :: [ModuleApplication] -> ShowS
show :: ModuleApplication -> ArgName
$cshow :: ModuleApplication -> ArgName
showsPrec :: Int -> ModuleApplication -> ShowS
$cshowsPrec :: Int -> ModuleApplication -> ShowS
Show, ModuleApplication -> ModuleApplication -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ModuleApplication -> ModuleApplication -> Bool
$c/= :: ModuleApplication -> ModuleApplication -> Bool
== :: ModuleApplication -> ModuleApplication -> Bool
$c== :: ModuleApplication -> ModuleApplication -> Bool
Eq, forall x. Rep ModuleApplication x -> ModuleApplication
forall x. ModuleApplication -> Rep ModuleApplication x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep ModuleApplication x -> ModuleApplication
$cfrom :: forall x. ModuleApplication -> Rep ModuleApplication x
Generic)
data Pragma
= OptionsPragma [String]
| BuiltinPragma RString ResolvedName
| BuiltinNoDefPragma RString KindOfName QName
| RewritePragma Range [QName]
| CompilePragma RString QName String
| StaticPragma QName
| EtaPragma QName
| InjectivePragma QName
| InlinePragma Bool QName
| NotProjectionLikePragma QName
| DisplayPragma QName [NamedArg Pattern] Expr
deriving (Int -> Pragma -> ShowS
[Pragma] -> ShowS
Pragma -> ArgName
forall a.
(Int -> a -> ShowS) -> (a -> ArgName) -> ([a] -> ShowS) -> Show a
showList :: [Pragma] -> ShowS
$cshowList :: [Pragma] -> ShowS
show :: Pragma -> ArgName
$cshow :: Pragma -> ArgName
showsPrec :: Int -> Pragma -> ShowS
$cshowsPrec :: Int -> Pragma -> ShowS
Show, Pragma -> Pragma -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Pragma -> Pragma -> Bool
$c/= :: Pragma -> Pragma -> Bool
== :: Pragma -> Pragma -> Bool
$c== :: Pragma -> Pragma -> Bool
Eq, forall x. Rep Pragma x -> Pragma
forall x. Pragma -> Rep Pragma x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Pragma x -> Pragma
$cfrom :: forall x. Pragma -> Rep Pragma x
Generic)
data LetBinding
= LetBind LetInfo ArgInfo BindName Type Expr
| LetPatBind LetInfo Pattern Expr
| LetApply ModuleInfo Erased ModuleName ModuleApplication
ScopeCopyInfo ImportDirective
| LetOpen ModuleInfo ModuleName ImportDirective
| LetDeclaredVariable BindName
deriving (Int -> LetBinding -> ShowS
[LetBinding] -> ShowS
LetBinding -> ArgName
forall a.
(Int -> a -> ShowS) -> (a -> ArgName) -> ([a] -> ShowS) -> Show a
showList :: [LetBinding] -> ShowS
$cshowList :: [LetBinding] -> ShowS
show :: LetBinding -> ArgName
$cshow :: LetBinding -> ArgName
showsPrec :: Int -> LetBinding -> ShowS
$cshowsPrec :: Int -> LetBinding -> ShowS
Show, LetBinding -> LetBinding -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: LetBinding -> LetBinding -> Bool
$c/= :: LetBinding -> LetBinding -> Bool
== :: LetBinding -> LetBinding -> Bool
$c== :: LetBinding -> LetBinding -> Bool
Eq, forall x. Rep LetBinding x -> LetBinding
forall x. LetBinding -> Rep LetBinding x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep LetBinding x -> LetBinding
$cfrom :: forall x. LetBinding -> Rep LetBinding x
Generic)
type TypeSignature = Declaration
type Constructor = TypeSignature
type Field = TypeSignature
type TacticAttr = Maybe (Ranged Expr)
data Binder' a = Binder
{ forall a. Binder' a -> Maybe Pattern
binderPattern :: Maybe Pattern
, forall a. Binder' a -> a
binderName :: a
} deriving (Int -> Binder' a -> ShowS
forall a. Show a => Int -> Binder' a -> ShowS
forall a. Show a => [Binder' a] -> ShowS
forall a. Show a => Binder' a -> ArgName
forall a.
(Int -> a -> ShowS) -> (a -> ArgName) -> ([a] -> ShowS) -> Show a
showList :: [Binder' a] -> ShowS
$cshowList :: forall a. Show a => [Binder' a] -> ShowS
show :: Binder' a -> ArgName
$cshow :: forall a. Show a => Binder' a -> ArgName
showsPrec :: Int -> Binder' a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> Binder' a -> ShowS
Show, Binder' a -> Binder' a -> Bool
forall a. Eq a => Binder' a -> Binder' a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Binder' a -> Binder' a -> Bool
$c/= :: forall a. Eq a => Binder' a -> Binder' a -> Bool
== :: Binder' a -> Binder' a -> Bool
$c== :: forall a. Eq a => Binder' a -> Binder' a -> Bool
Eq, forall a b. a -> Binder' b -> Binder' a
forall a b. (a -> b) -> Binder' a -> Binder' b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> Binder' b -> Binder' a
$c<$ :: forall a b. a -> Binder' b -> Binder' a
fmap :: forall a b. (a -> b) -> Binder' a -> Binder' b
$cfmap :: forall a b. (a -> b) -> Binder' a -> Binder' b
Functor, forall a. Eq a => a -> Binder' a -> Bool
forall a. Num a => Binder' a -> a
forall a. Ord a => Binder' a -> a
forall m. Monoid m => Binder' m -> m
forall a. Binder' a -> Bool
forall a. Binder' a -> Int
forall a. Binder' a -> [a]
forall a. (a -> a -> a) -> Binder' a -> a
forall m a. Monoid m => (a -> m) -> Binder' a -> m
forall b a. (b -> a -> b) -> b -> Binder' a -> b
forall a b. (a -> b -> b) -> b -> Binder' a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
product :: forall a. Num a => Binder' a -> a
$cproduct :: forall a. Num a => Binder' a -> a
sum :: forall a. Num a => Binder' a -> a
$csum :: forall a. Num a => Binder' a -> a
minimum :: forall a. Ord a => Binder' a -> a
$cminimum :: forall a. Ord a => Binder' a -> a
maximum :: forall a. Ord a => Binder' a -> a
$cmaximum :: forall a. Ord a => Binder' a -> a
elem :: forall a. Eq a => a -> Binder' a -> Bool
$celem :: forall a. Eq a => a -> Binder' a -> Bool
length :: forall a. Binder' a -> Int
$clength :: forall a. Binder' a -> Int
null :: forall a. Binder' a -> Bool
$cnull :: forall a. Binder' a -> Bool
toList :: forall a. Binder' a -> [a]
$ctoList :: forall a. Binder' a -> [a]
foldl1 :: forall a. (a -> a -> a) -> Binder' a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> Binder' a -> a
foldr1 :: forall a. (a -> a -> a) -> Binder' a -> a
$cfoldr1 :: forall a. (a -> a -> a) -> Binder' a -> a
foldl' :: forall b a. (b -> a -> b) -> b -> Binder' a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> Binder' a -> b
foldl :: forall b a. (b -> a -> b) -> b -> Binder' a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> Binder' a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> Binder' a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> Binder' a -> b
foldr :: forall a b. (a -> b -> b) -> b -> Binder' a -> b
$cfoldr :: forall a b. (a -> b -> b) -> b -> Binder' a -> b
foldMap' :: forall m a. Monoid m => (a -> m) -> Binder' a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> Binder' a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> Binder' a -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> Binder' a -> m
fold :: forall m. Monoid m => Binder' m -> m
$cfold :: forall m. Monoid m => Binder' m -> m
Foldable, Functor Binder'
Foldable Binder'
forall (t :: * -> *).
Functor t
-> Foldable t
-> (forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: * -> *) a. Monad m => Binder' (m a) -> m (Binder' a)
forall (f :: * -> *) a.
Applicative f =>
Binder' (f a) -> f (Binder' a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Binder' a -> m (Binder' b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Binder' a -> f (Binder' b)
sequence :: forall (m :: * -> *) a. Monad m => Binder' (m a) -> m (Binder' a)
$csequence :: forall (m :: * -> *) a. Monad m => Binder' (m a) -> m (Binder' a)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Binder' a -> m (Binder' b)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Binder' a -> m (Binder' b)
sequenceA :: forall (f :: * -> *) a.
Applicative f =>
Binder' (f a) -> f (Binder' a)
$csequenceA :: forall (f :: * -> *) a.
Applicative f =>
Binder' (f a) -> f (Binder' a)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Binder' a -> f (Binder' b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Binder' a -> f (Binder' b)
Traversable, forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (Binder' a) x -> Binder' a
forall a x. Binder' a -> Rep (Binder' a) x
$cto :: forall a x. Rep (Binder' a) x -> Binder' a
$cfrom :: forall a x. Binder' a -> Rep (Binder' a) x
Generic)
type Binder = Binder' BindName
mkBinder :: a -> Binder' a
mkBinder :: forall a. a -> Binder' a
mkBinder = forall a. Maybe Pattern -> a -> Binder' a
Binder forall a. Maybe a
Nothing
mkBinder_ :: Name -> Binder
mkBinder_ :: Name -> Binder
mkBinder_ = forall a. a -> Binder' a
mkBinder forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> BindName
mkBindName
extractPattern :: Binder' a -> Maybe (Pattern, a)
(Binder Maybe Pattern
p a
a) = (,a
a) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Pattern
p
data LamBinding
= DomainFree TacticAttr (NamedArg Binder)
| DomainFull TypedBinding
deriving (Int -> LamBinding -> ShowS
[LamBinding] -> ShowS
LamBinding -> ArgName
forall a.
(Int -> a -> ShowS) -> (a -> ArgName) -> ([a] -> ShowS) -> Show a
showList :: [LamBinding] -> ShowS
$cshowList :: [LamBinding] -> ShowS
show :: LamBinding -> ArgName
$cshow :: LamBinding -> ArgName
showsPrec :: Int -> LamBinding -> ShowS
$cshowsPrec :: Int -> LamBinding -> ShowS
Show, LamBinding -> LamBinding -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: LamBinding -> LamBinding -> Bool
$c/= :: LamBinding -> LamBinding -> Bool
== :: LamBinding -> LamBinding -> Bool
$c== :: LamBinding -> LamBinding -> Bool
Eq, forall x. Rep LamBinding x -> LamBinding
forall x. LamBinding -> Rep LamBinding x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep LamBinding x -> LamBinding
$cfrom :: forall x. LamBinding -> Rep LamBinding x
Generic)
mkDomainFree :: NamedArg Binder -> LamBinding
mkDomainFree :: NamedArg Binder -> LamBinding
mkDomainFree = TacticAttr -> NamedArg Binder -> LamBinding
DomainFree forall a. Maybe a
Nothing
data TypedBindingInfo
= TypedBindingInfo
{ TypedBindingInfo -> TacticAttr
tbTacticAttr :: TacticAttr
, TypedBindingInfo -> Bool
tbFinite :: Bool
}
deriving (Int -> TypedBindingInfo -> ShowS
[TypedBindingInfo] -> ShowS
TypedBindingInfo -> ArgName
forall a.
(Int -> a -> ShowS) -> (a -> ArgName) -> ([a] -> ShowS) -> Show a
showList :: [TypedBindingInfo] -> ShowS
$cshowList :: [TypedBindingInfo] -> ShowS
show :: TypedBindingInfo -> ArgName
$cshow :: TypedBindingInfo -> ArgName
showsPrec :: Int -> TypedBindingInfo -> ShowS
$cshowsPrec :: Int -> TypedBindingInfo -> ShowS
Show, TypedBindingInfo -> TypedBindingInfo -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: TypedBindingInfo -> TypedBindingInfo -> Bool
$c/= :: TypedBindingInfo -> TypedBindingInfo -> Bool
== :: TypedBindingInfo -> TypedBindingInfo -> Bool
$c== :: TypedBindingInfo -> TypedBindingInfo -> Bool
Eq, forall x. Rep TypedBindingInfo x -> TypedBindingInfo
forall x. TypedBindingInfo -> Rep TypedBindingInfo x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep TypedBindingInfo x -> TypedBindingInfo
$cfrom :: forall x. TypedBindingInfo -> Rep TypedBindingInfo x
Generic)
defaultTbInfo :: TypedBindingInfo
defaultTbInfo :: TypedBindingInfo
defaultTbInfo = TypedBindingInfo
{ tbTacticAttr :: TacticAttr
tbTacticAttr = forall a. Maybe a
Nothing
, tbFinite :: Bool
tbFinite = Bool
False
}
data TypedBinding
= TBind Range TypedBindingInfo (List1 (NamedArg Binder)) Type
| TLet Range (List1 LetBinding)
deriving (Int -> TypedBinding -> ShowS
Telescope -> ShowS
TypedBinding -> ArgName
forall a.
(Int -> a -> ShowS) -> (a -> ArgName) -> ([a] -> ShowS) -> Show a
showList :: Telescope -> ShowS
$cshowList :: Telescope -> ShowS
show :: TypedBinding -> ArgName
$cshow :: TypedBinding -> ArgName
showsPrec :: Int -> TypedBinding -> ShowS
$cshowsPrec :: Int -> TypedBinding -> ShowS
Show, TypedBinding -> TypedBinding -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: TypedBinding -> TypedBinding -> Bool
$c/= :: TypedBinding -> TypedBinding -> Bool
== :: TypedBinding -> TypedBinding -> Bool
$c== :: TypedBinding -> TypedBinding -> Bool
Eq, forall x. Rep TypedBinding x -> TypedBinding
forall x. TypedBinding -> Rep TypedBinding x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep TypedBinding x -> TypedBinding
$cfrom :: forall x. TypedBinding -> Rep TypedBinding x
Generic)
mkTBind :: Range -> List1 (NamedArg Binder) -> Type -> TypedBinding
mkTBind :: Range -> List1 (NamedArg Binder) -> Expr -> TypedBinding
mkTBind Range
r = Range
-> TypedBindingInfo
-> List1 (NamedArg Binder)
-> Expr
-> TypedBinding
TBind Range
r TypedBindingInfo
defaultTbInfo
mkTLet :: Range -> [LetBinding] -> Maybe TypedBinding
mkTLet :: Range -> [LetBinding] -> Maybe TypedBinding
mkTLet Range
_ [] = forall a. Maybe a
Nothing
mkTLet Range
r (LetBinding
d:[LetBinding]
ds) = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Range -> List1 LetBinding -> TypedBinding
TLet Range
r (LetBinding
d forall a. a -> [a] -> NonEmpty a
:| [LetBinding]
ds)
type Telescope1 = List1 TypedBinding
type Telescope = [TypedBinding]
mkPi :: ExprInfo -> Telescope -> Type -> Type
mkPi :: ExprInfo -> Telescope -> Expr -> Expr
mkPi ExprInfo
i [] Expr
e = Expr
e
mkPi ExprInfo
i (TypedBinding
x:Telescope
xs) Expr
e = ExprInfo -> Telescope1 -> Expr -> Expr
Pi ExprInfo
i (TypedBinding
x forall a. a -> [a] -> NonEmpty a
:| Telescope
xs) Expr
e
data GeneralizeTelescope = GeneralizeTel
{ GeneralizeTelescope -> Map QName Name
generalizeTelVars :: Map QName Name
, GeneralizeTelescope -> Telescope
generalizeTel :: Telescope }
deriving (Int -> GeneralizeTelescope -> ShowS
[GeneralizeTelescope] -> ShowS
GeneralizeTelescope -> ArgName
forall a.
(Int -> a -> ShowS) -> (a -> ArgName) -> ([a] -> ShowS) -> Show a
showList :: [GeneralizeTelescope] -> ShowS
$cshowList :: [GeneralizeTelescope] -> ShowS
show :: GeneralizeTelescope -> ArgName
$cshow :: GeneralizeTelescope -> ArgName
showsPrec :: Int -> GeneralizeTelescope -> ShowS
$cshowsPrec :: Int -> GeneralizeTelescope -> ShowS
Show, GeneralizeTelescope -> GeneralizeTelescope -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: GeneralizeTelescope -> GeneralizeTelescope -> Bool
$c/= :: GeneralizeTelescope -> GeneralizeTelescope -> Bool
== :: GeneralizeTelescope -> GeneralizeTelescope -> Bool
$c== :: GeneralizeTelescope -> GeneralizeTelescope -> Bool
Eq, forall x. Rep GeneralizeTelescope x -> GeneralizeTelescope
forall x. GeneralizeTelescope -> Rep GeneralizeTelescope x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep GeneralizeTelescope x -> GeneralizeTelescope
$cfrom :: forall x. GeneralizeTelescope -> Rep GeneralizeTelescope x
Generic)
data DataDefParams = DataDefParams
{ DataDefParams -> Set Name
dataDefGeneralizedParams :: Set Name
, DataDefParams -> [LamBinding]
dataDefParams :: [LamBinding]
}
deriving (Int -> DataDefParams -> ShowS
[DataDefParams] -> ShowS
DataDefParams -> ArgName
forall a.
(Int -> a -> ShowS) -> (a -> ArgName) -> ([a] -> ShowS) -> Show a
showList :: [DataDefParams] -> ShowS
$cshowList :: [DataDefParams] -> ShowS
show :: DataDefParams -> ArgName
$cshow :: DataDefParams -> ArgName
showsPrec :: Int -> DataDefParams -> ShowS
$cshowsPrec :: Int -> DataDefParams -> ShowS
Show, DataDefParams -> DataDefParams -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: DataDefParams -> DataDefParams -> Bool
$c/= :: DataDefParams -> DataDefParams -> Bool
== :: DataDefParams -> DataDefParams -> Bool
$c== :: DataDefParams -> DataDefParams -> Bool
Eq, forall x. Rep DataDefParams x -> DataDefParams
forall x. DataDefParams -> Rep DataDefParams x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep DataDefParams x -> DataDefParams
$cfrom :: forall x. DataDefParams -> Rep DataDefParams x
Generic)
noDataDefParams :: DataDefParams
noDataDefParams :: DataDefParams
noDataDefParams = Set Name -> [LamBinding] -> DataDefParams
DataDefParams forall a. Set a
Set.empty []
data ProblemEq = ProblemEq
{ ProblemEq -> Pattern
problemInPat :: Pattern
, ProblemEq -> Term
problemInst :: I.Term
, ProblemEq -> Dom Type
problemType :: I.Dom I.Type
} deriving (Int -> ProblemEq -> ShowS
[ProblemEq] -> ShowS
ProblemEq -> ArgName
forall a.
(Int -> a -> ShowS) -> (a -> ArgName) -> ([a] -> ShowS) -> Show a
showList :: [ProblemEq] -> ShowS
$cshowList :: [ProblemEq] -> ShowS
show :: ProblemEq -> ArgName
$cshow :: ProblemEq -> ArgName
showsPrec :: Int -> ProblemEq -> ShowS
$cshowsPrec :: Int -> ProblemEq -> ShowS
Show, forall x. Rep ProblemEq x -> ProblemEq
forall x. ProblemEq -> Rep ProblemEq x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep ProblemEq x -> ProblemEq
$cfrom :: forall x. ProblemEq -> Rep ProblemEq x
Generic)
instance Eq ProblemEq where ProblemEq
_ == :: ProblemEq -> ProblemEq -> Bool
== ProblemEq
_ = Bool
True
data Clause' lhs = Clause
{ forall lhs. Clause' lhs -> lhs
clauseLHS :: lhs
, forall lhs. Clause' lhs -> [ProblemEq]
clauseStrippedPats :: [ProblemEq]
, forall lhs. Clause' lhs -> RHS
clauseRHS :: RHS
, forall lhs. Clause' lhs -> WhereDeclarations
clauseWhereDecls :: WhereDeclarations
, forall lhs. Clause' lhs -> Bool
clauseCatchall :: Bool
} deriving (Int -> Clause' lhs -> ShowS
forall lhs. Show lhs => Int -> Clause' lhs -> ShowS
forall lhs. Show lhs => [Clause' lhs] -> ShowS
forall lhs. Show lhs => Clause' lhs -> ArgName
forall a.
(Int -> a -> ShowS) -> (a -> ArgName) -> ([a] -> ShowS) -> Show a
showList :: [Clause' lhs] -> ShowS
$cshowList :: forall lhs. Show lhs => [Clause' lhs] -> ShowS
show :: Clause' lhs -> ArgName
$cshow :: forall lhs. Show lhs => Clause' lhs -> ArgName
showsPrec :: Int -> Clause' lhs -> ShowS
$cshowsPrec :: forall lhs. Show lhs => Int -> Clause' lhs -> ShowS
Show, forall a b. a -> Clause' b -> Clause' a
forall a b. (a -> b) -> Clause' a -> Clause' b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> Clause' b -> Clause' a
$c<$ :: forall a b. a -> Clause' b -> Clause' a
fmap :: forall a b. (a -> b) -> Clause' a -> Clause' b
$cfmap :: forall a b. (a -> b) -> Clause' a -> Clause' b
Functor, forall a. Eq a => a -> Clause' a -> Bool
forall a. Num a => Clause' a -> a
forall a. Ord a => Clause' a -> a
forall m. Monoid m => Clause' m -> m
forall lhs. Clause' lhs -> Bool
forall a. Clause' a -> Int
forall a. Clause' a -> [a]
forall a. (a -> a -> a) -> Clause' a -> a
forall m a. Monoid m => (a -> m) -> Clause' a -> m
forall b a. (b -> a -> b) -> b -> Clause' a -> b
forall a b. (a -> b -> b) -> b -> Clause' a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
product :: forall a. Num a => Clause' a -> a
$cproduct :: forall a. Num a => Clause' a -> a
sum :: forall a. Num a => Clause' a -> a
$csum :: forall a. Num a => Clause' a -> a
minimum :: forall a. Ord a => Clause' a -> a
$cminimum :: forall a. Ord a => Clause' a -> a
maximum :: forall a. Ord a => Clause' a -> a
$cmaximum :: forall a. Ord a => Clause' a -> a
elem :: forall a. Eq a => a -> Clause' a -> Bool
$celem :: forall a. Eq a => a -> Clause' a -> Bool
length :: forall a. Clause' a -> Int
$clength :: forall a. Clause' a -> Int
null :: forall lhs. Clause' lhs -> Bool
$cnull :: forall lhs. Clause' lhs -> Bool
toList :: forall a. Clause' a -> [a]
$ctoList :: forall a. Clause' a -> [a]
foldl1 :: forall a. (a -> a -> a) -> Clause' a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> Clause' a -> a
foldr1 :: forall a. (a -> a -> a) -> Clause' a -> a
$cfoldr1 :: forall a. (a -> a -> a) -> Clause' a -> a
foldl' :: forall b a. (b -> a -> b) -> b -> Clause' a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> Clause' a -> b
foldl :: forall b a. (b -> a -> b) -> b -> Clause' a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> Clause' a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> Clause' a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> Clause' a -> b
foldr :: forall a b. (a -> b -> b) -> b -> Clause' a -> b
$cfoldr :: forall a b. (a -> b -> b) -> b -> Clause' a -> b
foldMap' :: forall m a. Monoid m => (a -> m) -> Clause' a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> Clause' a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> Clause' a -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> Clause' a -> m
fold :: forall m. Monoid m => Clause' m -> m
$cfold :: forall m. Monoid m => Clause' m -> m
Foldable, Functor Clause'
Foldable Clause'
forall (t :: * -> *).
Functor t
-> Foldable t
-> (forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: * -> *) a. Monad m => Clause' (m a) -> m (Clause' a)
forall (f :: * -> *) a.
Applicative f =>
Clause' (f a) -> f (Clause' a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Clause' a -> m (Clause' b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Clause' a -> f (Clause' b)
sequence :: forall (m :: * -> *) a. Monad m => Clause' (m a) -> m (Clause' a)
$csequence :: forall (m :: * -> *) a. Monad m => Clause' (m a) -> m (Clause' a)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Clause' a -> m (Clause' b)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Clause' a -> m (Clause' b)
sequenceA :: forall (f :: * -> *) a.
Applicative f =>
Clause' (f a) -> f (Clause' a)
$csequenceA :: forall (f :: * -> *) a.
Applicative f =>
Clause' (f a) -> f (Clause' a)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Clause' a -> f (Clause' b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Clause' a -> f (Clause' b)
Traversable, Clause' lhs -> Clause' lhs -> Bool
forall lhs. Eq lhs => Clause' lhs -> Clause' lhs -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Clause' lhs -> Clause' lhs -> Bool
$c/= :: forall lhs. Eq lhs => Clause' lhs -> Clause' lhs -> Bool
== :: Clause' lhs -> Clause' lhs -> Bool
$c== :: forall lhs. Eq lhs => Clause' lhs -> Clause' lhs -> Bool
Eq, forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall lhs x. Rep (Clause' lhs) x -> Clause' lhs
forall lhs x. Clause' lhs -> Rep (Clause' lhs) x
$cto :: forall lhs x. Rep (Clause' lhs) x -> Clause' lhs
$cfrom :: forall lhs x. Clause' lhs -> Rep (Clause' lhs) x
Generic)
data WhereDeclarations = WhereDecls
{ WhereDeclarations -> Maybe ModuleName
whereModule :: Maybe ModuleName
, WhereDeclarations -> Bool
whereAnywhere :: Bool
, WhereDeclarations -> Maybe Declaration
whereDecls :: Maybe Declaration
} deriving (Int -> WhereDeclarations -> ShowS
[WhereDeclarations] -> ShowS
WhereDeclarations -> ArgName
forall a.
(Int -> a -> ShowS) -> (a -> ArgName) -> ([a] -> ShowS) -> Show a
showList :: [WhereDeclarations] -> ShowS
$cshowList :: [WhereDeclarations] -> ShowS
show :: WhereDeclarations -> ArgName
$cshow :: WhereDeclarations -> ArgName
showsPrec :: Int -> WhereDeclarations -> ShowS
$cshowsPrec :: Int -> WhereDeclarations -> ShowS
Show, WhereDeclarations -> WhereDeclarations -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: WhereDeclarations -> WhereDeclarations -> Bool
$c/= :: WhereDeclarations -> WhereDeclarations -> Bool
== :: WhereDeclarations -> WhereDeclarations -> Bool
$c== :: WhereDeclarations -> WhereDeclarations -> Bool
Eq, forall x. Rep WhereDeclarations x -> WhereDeclarations
forall x. WhereDeclarations -> Rep WhereDeclarations x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep WhereDeclarations x -> WhereDeclarations
$cfrom :: forall x. WhereDeclarations -> Rep WhereDeclarations x
Generic)
instance Null WhereDeclarations where
empty :: WhereDeclarations
empty = Maybe ModuleName -> Bool -> Maybe Declaration -> WhereDeclarations
WhereDecls forall a. Null a => a
empty Bool
False forall a. Null a => a
empty
noWhereDecls :: WhereDeclarations
noWhereDecls :: WhereDeclarations
noWhereDecls = forall a. Null a => a
empty
type Clause = Clause' LHS
type SpineClause = Clause' SpineLHS
type RewriteEqn = RewriteEqn' QName BindName Pattern Expr
type WithExpr' e = Named BindName (Arg e)
type WithExpr = WithExpr' Expr
data RHS
= RHS
{ RHS -> Expr
rhsExpr :: Expr
, RHS -> Maybe Expr
rhsConcrete :: Maybe C.Expr
}
| AbsurdRHS
| WithRHS QName [WithExpr] (List1 Clause)
| RewriteRHS
{ RHS -> [RewriteEqn]
rewriteExprs :: [RewriteEqn]
, RHS -> [ProblemEq]
rewriteStrippedPats :: [ProblemEq]
, RHS -> RHS
rewriteRHS :: RHS
, RHS -> WhereDeclarations
rewriteWhereDecls :: WhereDeclarations
}
deriving (Int -> RHS -> ShowS
[RHS] -> ShowS
RHS -> ArgName
forall a.
(Int -> a -> ShowS) -> (a -> ArgName) -> ([a] -> ShowS) -> Show a
showList :: [RHS] -> ShowS
$cshowList :: [RHS] -> ShowS
show :: RHS -> ArgName
$cshow :: RHS -> ArgName
showsPrec :: Int -> RHS -> ShowS
$cshowsPrec :: Int -> RHS -> ShowS
Show, forall x. Rep RHS x -> RHS
forall x. RHS -> Rep RHS x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep RHS x -> RHS
$cfrom :: forall x. RHS -> Rep RHS x
Generic)
instance Eq RHS where
RHS Expr
e Maybe Expr
_ == :: RHS -> RHS -> Bool
== RHS Expr
e' Maybe Expr
_ = Expr
e forall a. Eq a => a -> a -> Bool
== Expr
e'
RHS
AbsurdRHS == RHS
AbsurdRHS = Bool
True
WithRHS QName
a [WithExpr]
b List1 Clause
c == WithRHS QName
a' [WithExpr]
b' List1 Clause
c' = (QName
a forall a. Eq a => a -> a -> Bool
== QName
a') Bool -> Bool -> Bool
&& ([WithExpr]
b forall a. Eq a => a -> a -> Bool
== [WithExpr]
b') Bool -> Bool -> Bool
&& (List1 Clause
c forall a. Eq a => a -> a -> Bool
== List1 Clause
c')
RewriteRHS [RewriteEqn]
a [ProblemEq]
b RHS
c WhereDeclarations
d == RewriteRHS [RewriteEqn]
a' [ProblemEq]
b' RHS
c' WhereDeclarations
d' = forall (t :: * -> *). Foldable t => t Bool -> Bool
and [ [RewriteEqn]
a forall a. Eq a => a -> a -> Bool
== [RewriteEqn]
a', [ProblemEq]
b forall a. Eq a => a -> a -> Bool
== [ProblemEq]
b', RHS
c forall a. Eq a => a -> a -> Bool
== RHS
c' , WhereDeclarations
d forall a. Eq a => a -> a -> Bool
== WhereDeclarations
d' ]
RHS
_ == RHS
_ = Bool
False
data SpineLHS = SpineLHS
{ SpineLHS -> LHSInfo
spLhsInfo :: LHSInfo
, SpineLHS -> QName
spLhsDefName :: QName
, SpineLHS -> [NamedArg Pattern]
spLhsPats :: [NamedArg Pattern]
}
deriving (Int -> SpineLHS -> ShowS
[SpineLHS] -> ShowS
SpineLHS -> ArgName
forall a.
(Int -> a -> ShowS) -> (a -> ArgName) -> ([a] -> ShowS) -> Show a
showList :: [SpineLHS] -> ShowS
$cshowList :: [SpineLHS] -> ShowS
show :: SpineLHS -> ArgName
$cshow :: SpineLHS -> ArgName
showsPrec :: Int -> SpineLHS -> ShowS
$cshowsPrec :: Int -> SpineLHS -> ShowS
Show, SpineLHS -> SpineLHS -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: SpineLHS -> SpineLHS -> Bool
$c/= :: SpineLHS -> SpineLHS -> Bool
== :: SpineLHS -> SpineLHS -> Bool
$c== :: SpineLHS -> SpineLHS -> Bool
Eq, forall x. Rep SpineLHS x -> SpineLHS
forall x. SpineLHS -> Rep SpineLHS x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep SpineLHS x -> SpineLHS
$cfrom :: forall x. SpineLHS -> Rep SpineLHS x
Generic)
instance Eq LHS where
LHS LHSInfo
_ LHSCore
core == :: LHS -> LHS -> Bool
== LHS LHSInfo
_ LHSCore
core' = LHSCore
core forall a. Eq a => a -> a -> Bool
== LHSCore
core'
data LHS = LHS
{ LHS -> LHSInfo
lhsInfo :: LHSInfo
, LHS -> LHSCore
lhsCore :: LHSCore
}
deriving (Int -> LHS -> ShowS
[LHS] -> ShowS
LHS -> ArgName
forall a.
(Int -> a -> ShowS) -> (a -> ArgName) -> ([a] -> ShowS) -> Show a
showList :: [LHS] -> ShowS
$cshowList :: [LHS] -> ShowS
show :: LHS -> ArgName
$cshow :: LHS -> ArgName
showsPrec :: Int -> LHS -> ShowS
$cshowsPrec :: Int -> LHS -> ShowS
Show, forall x. Rep LHS x -> LHS
forall x. LHS -> Rep LHS x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep LHS x -> LHS
$cfrom :: forall x. LHS -> Rep LHS x
Generic)
data LHSCore' e
= LHSHead { forall e. LHSCore' e -> QName
lhsDefName :: QName
, forall e. LHSCore' e -> [NamedArg (Pattern' e)]
lhsPats :: [NamedArg (Pattern' e)]
}
| LHSProj { forall e. LHSCore' e -> AmbiguousQName
lhsDestructor :: AmbiguousQName
, forall e. LHSCore' e -> NamedArg (LHSCore' e)
lhsFocus :: NamedArg (LHSCore' e)
, lhsPats :: [NamedArg (Pattern' e)]
}
| LHSWith { forall e. LHSCore' e -> LHSCore' e
lhsHead :: LHSCore' e
, forall e. LHSCore' e -> [Arg (Pattern' e)]
lhsWithPatterns :: [Arg (Pattern' e)]
, lhsPats :: [NamedArg (Pattern' e)]
}
deriving (Int -> LHSCore' e -> ShowS
forall e. Show e => Int -> LHSCore' e -> ShowS
forall e. Show e => [LHSCore' e] -> ShowS
forall e. Show e => LHSCore' e -> ArgName
forall a.
(Int -> a -> ShowS) -> (a -> ArgName) -> ([a] -> ShowS) -> Show a
showList :: [LHSCore' e] -> ShowS
$cshowList :: forall e. Show e => [LHSCore' e] -> ShowS
show :: LHSCore' e -> ArgName
$cshow :: forall e. Show e => LHSCore' e -> ArgName
showsPrec :: Int -> LHSCore' e -> ShowS
$cshowsPrec :: forall e. Show e => Int -> LHSCore' e -> ShowS
Show, forall a b. a -> LHSCore' b -> LHSCore' a
forall a b. (a -> b) -> LHSCore' a -> LHSCore' b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> LHSCore' b -> LHSCore' a
$c<$ :: forall a b. a -> LHSCore' b -> LHSCore' a
fmap :: forall a b. (a -> b) -> LHSCore' a -> LHSCore' b
$cfmap :: forall a b. (a -> b) -> LHSCore' a -> LHSCore' b
Functor, forall a. Eq a => a -> LHSCore' a -> Bool
forall a. Num a => LHSCore' a -> a
forall a. Ord a => LHSCore' a -> a
forall m. Monoid m => LHSCore' m -> m
forall a. LHSCore' a -> Bool
forall a. LHSCore' a -> Int
forall a. LHSCore' a -> [a]
forall a. (a -> a -> a) -> LHSCore' a -> a
forall m a. Monoid m => (a -> m) -> LHSCore' a -> m
forall b a. (b -> a -> b) -> b -> LHSCore' a -> b
forall a b. (a -> b -> b) -> b -> LHSCore' a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
product :: forall a. Num a => LHSCore' a -> a
$cproduct :: forall a. Num a => LHSCore' a -> a
sum :: forall a. Num a => LHSCore' a -> a
$csum :: forall a. Num a => LHSCore' a -> a
minimum :: forall a. Ord a => LHSCore' a -> a
$cminimum :: forall a. Ord a => LHSCore' a -> a
maximum :: forall a. Ord a => LHSCore' a -> a
$cmaximum :: forall a. Ord a => LHSCore' a -> a
elem :: forall a. Eq a => a -> LHSCore' a -> Bool
$celem :: forall a. Eq a => a -> LHSCore' a -> Bool
length :: forall a. LHSCore' a -> Int
$clength :: forall a. LHSCore' a -> Int
null :: forall a. LHSCore' a -> Bool
$cnull :: forall a. LHSCore' a -> Bool
toList :: forall a. LHSCore' a -> [a]
$ctoList :: forall a. LHSCore' a -> [a]
foldl1 :: forall a. (a -> a -> a) -> LHSCore' a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> LHSCore' a -> a
foldr1 :: forall a. (a -> a -> a) -> LHSCore' a -> a
$cfoldr1 :: forall a. (a -> a -> a) -> LHSCore' a -> a
foldl' :: forall b a. (b -> a -> b) -> b -> LHSCore' a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> LHSCore' a -> b
foldl :: forall b a. (b -> a -> b) -> b -> LHSCore' a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> LHSCore' a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> LHSCore' a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> LHSCore' a -> b
foldr :: forall a b. (a -> b -> b) -> b -> LHSCore' a -> b
$cfoldr :: forall a b. (a -> b -> b) -> b -> LHSCore' a -> b
foldMap' :: forall m a. Monoid m => (a -> m) -> LHSCore' a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> LHSCore' a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> LHSCore' a -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> LHSCore' a -> m
fold :: forall m. Monoid m => LHSCore' m -> m
$cfold :: forall m. Monoid m => LHSCore' m -> m
Foldable, Functor LHSCore'
Foldable LHSCore'
forall (t :: * -> *).
Functor t
-> Foldable t
-> (forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: * -> *) a. Monad m => LHSCore' (m a) -> m (LHSCore' a)
forall (f :: * -> *) a.
Applicative f =>
LHSCore' (f a) -> f (LHSCore' a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> LHSCore' a -> m (LHSCore' b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> LHSCore' a -> f (LHSCore' b)
sequence :: forall (m :: * -> *) a. Monad m => LHSCore' (m a) -> m (LHSCore' a)
$csequence :: forall (m :: * -> *) a. Monad m => LHSCore' (m a) -> m (LHSCore' a)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> LHSCore' a -> m (LHSCore' b)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> LHSCore' a -> m (LHSCore' b)
sequenceA :: forall (f :: * -> *) a.
Applicative f =>
LHSCore' (f a) -> f (LHSCore' a)
$csequenceA :: forall (f :: * -> *) a.
Applicative f =>
LHSCore' (f a) -> f (LHSCore' a)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> LHSCore' a -> f (LHSCore' b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> LHSCore' a -> f (LHSCore' b)
Traversable, LHSCore' e -> LHSCore' e -> Bool
forall e. Eq e => LHSCore' e -> LHSCore' e -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: LHSCore' e -> LHSCore' e -> Bool
$c/= :: forall e. Eq e => LHSCore' e -> LHSCore' e -> Bool
== :: LHSCore' e -> LHSCore' e -> Bool
$c== :: forall e. Eq e => LHSCore' e -> LHSCore' e -> Bool
Eq, forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall e x. Rep (LHSCore' e) x -> LHSCore' e
forall e x. LHSCore' e -> Rep (LHSCore' e) x
$cto :: forall e x. Rep (LHSCore' e) x -> LHSCore' e
$cfrom :: forall e x. LHSCore' e -> Rep (LHSCore' e) x
Generic)
type LHSCore = LHSCore' Expr
data Pattern' e
= VarP BindName
| ConP ConPatInfo AmbiguousQName (NAPs e)
| ProjP PatInfo ProjOrigin AmbiguousQName
| DefP PatInfo AmbiguousQName (NAPs e)
| WildP PatInfo
| AsP PatInfo BindName (Pattern' e)
| DotP PatInfo e
| AbsurdP PatInfo
| LitP PatInfo Literal
| PatternSynP PatInfo AmbiguousQName (NAPs e)
| RecP PatInfo [FieldAssignment' (Pattern' e)]
| EqualP PatInfo [(e, e)]
| WithP PatInfo (Pattern' e)
| AnnP PatInfo e (Pattern' e)
deriving (Int -> Pattern' e -> ShowS
forall e. Show e => Int -> Pattern' e -> ShowS
forall e. Show e => [Pattern' e] -> ShowS
forall e. Show e => Pattern' e -> ArgName
forall a.
(Int -> a -> ShowS) -> (a -> ArgName) -> ([a] -> ShowS) -> Show a
showList :: [Pattern' e] -> ShowS
$cshowList :: forall e. Show e => [Pattern' e] -> ShowS
show :: Pattern' e -> ArgName
$cshow :: forall e. Show e => Pattern' e -> ArgName
showsPrec :: Int -> Pattern' e -> ShowS
$cshowsPrec :: forall e. Show e => Int -> Pattern' e -> ShowS
Show, forall a b. a -> Pattern' b -> Pattern' a
forall a b. (a -> b) -> Pattern' a -> Pattern' b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> Pattern' b -> Pattern' a
$c<$ :: forall a b. a -> Pattern' b -> Pattern' a
fmap :: forall a b. (a -> b) -> Pattern' a -> Pattern' b
$cfmap :: forall a b. (a -> b) -> Pattern' a -> Pattern' b
Functor, forall a. Eq a => a -> Pattern' a -> Bool
forall a. Num a => Pattern' a -> a
forall a. Ord a => Pattern' a -> a
forall m. Monoid m => Pattern' m -> m
forall a. Pattern' a -> Bool
forall a. Pattern' a -> Int
forall a. Pattern' a -> [a]
forall a. (a -> a -> a) -> Pattern' a -> a
forall m a. Monoid m => (a -> m) -> Pattern' a -> m
forall b a. (b -> a -> b) -> b -> Pattern' a -> b
forall a b. (a -> b -> b) -> b -> Pattern' a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
product :: forall a. Num a => Pattern' a -> a
$cproduct :: forall a. Num a => Pattern' a -> a
sum :: forall a. Num a => Pattern' a -> a
$csum :: forall a. Num a => Pattern' a -> a
minimum :: forall a. Ord a => Pattern' a -> a
$cminimum :: forall a. Ord a => Pattern' a -> a
maximum :: forall a. Ord a => Pattern' a -> a
$cmaximum :: forall a. Ord a => Pattern' a -> a
elem :: forall a. Eq a => a -> Pattern' a -> Bool
$celem :: forall a. Eq a => a -> Pattern' a -> Bool
length :: forall a. Pattern' a -> Int
$clength :: forall a. Pattern' a -> Int
null :: forall a. Pattern' a -> Bool
$cnull :: forall a. Pattern' a -> Bool
toList :: forall a. Pattern' a -> [a]
$ctoList :: forall a. Pattern' a -> [a]
foldl1 :: forall a. (a -> a -> a) -> Pattern' a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> Pattern' a -> a
foldr1 :: forall a. (a -> a -> a) -> Pattern' a -> a
$cfoldr1 :: forall a. (a -> a -> a) -> Pattern' a -> a
foldl' :: forall b a. (b -> a -> b) -> b -> Pattern' a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> Pattern' a -> b
foldl :: forall b a. (b -> a -> b) -> b -> Pattern' a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> Pattern' a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> Pattern' a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> Pattern' a -> b
foldr :: forall a b. (a -> b -> b) -> b -> Pattern' a -> b
$cfoldr :: forall a b. (a -> b -> b) -> b -> Pattern' a -> b
foldMap' :: forall m a. Monoid m => (a -> m) -> Pattern' a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> Pattern' a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> Pattern' a -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> Pattern' a -> m
fold :: forall m. Monoid m => Pattern' m -> m
$cfold :: forall m. Monoid m => Pattern' m -> m
Foldable, Functor Pattern'
Foldable Pattern'
forall (t :: * -> *).
Functor t
-> Foldable t
-> (forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: * -> *) a. Monad m => Pattern' (m a) -> m (Pattern' a)
forall (f :: * -> *) a.
Applicative f =>
Pattern' (f a) -> f (Pattern' a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Pattern' a -> m (Pattern' b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Pattern' a -> f (Pattern' b)
sequence :: forall (m :: * -> *) a. Monad m => Pattern' (m a) -> m (Pattern' a)
$csequence :: forall (m :: * -> *) a. Monad m => Pattern' (m a) -> m (Pattern' a)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Pattern' a -> m (Pattern' b)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Pattern' a -> m (Pattern' b)
sequenceA :: forall (f :: * -> *) a.
Applicative f =>
Pattern' (f a) -> f (Pattern' a)
$csequenceA :: forall (f :: * -> *) a.
Applicative f =>
Pattern' (f a) -> f (Pattern' a)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Pattern' a -> f (Pattern' b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Pattern' a -> f (Pattern' b)
Traversable, Pattern' e -> Pattern' e -> Bool
forall e. Eq e => Pattern' e -> Pattern' e -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Pattern' e -> Pattern' e -> Bool
$c/= :: forall e. Eq e => Pattern' e -> Pattern' e -> Bool
== :: Pattern' e -> Pattern' e -> Bool
$c== :: forall e. Eq e => Pattern' e -> Pattern' e -> Bool
Eq, forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall e x. Rep (Pattern' e) x -> Pattern' e
forall e x. Pattern' e -> Rep (Pattern' e) x
$cto :: forall e x. Rep (Pattern' e) x -> Pattern' e
$cfrom :: forall e x. Pattern' e -> Rep (Pattern' e) x
Generic)
type NAPs e = [NamedArg (Pattern' e)]
type NAPs1 e = List1 (NamedArg (Pattern' e))
type Pattern = Pattern' Expr
type Patterns = [NamedArg Pattern]
instance IsProjP (Pattern' e) where
isProjP :: Pattern' e -> Maybe (ProjOrigin, AmbiguousQName)
isProjP (ProjP PatInfo
_ ProjOrigin
o AmbiguousQName
d) = forall a. a -> Maybe a
Just (ProjOrigin
o, AmbiguousQName
d)
isProjP Pattern' e
_ = forall a. Maybe a
Nothing
instance IsProjP Expr where
isProjP :: Expr -> Maybe (ProjOrigin, AmbiguousQName)
isProjP (Proj ProjOrigin
o AmbiguousQName
ds) = forall a. a -> Maybe a
Just (ProjOrigin
o, AmbiguousQName
ds)
isProjP (ScopedExpr ScopeInfo
_ Expr
e) = forall a. IsProjP a => a -> Maybe (ProjOrigin, AmbiguousQName)
isProjP Expr
e
isProjP Expr
_ = forall a. Maybe a
Nothing
type HoleContent = C.HoleContent' () BindName Pattern Expr
instance Eq Expr where
ScopedExpr ScopeInfo
_ Expr
a1 == :: Expr -> Expr -> Bool
== ScopedExpr ScopeInfo
_ Expr
a2 = Expr
a1 forall a. Eq a => a -> a -> Bool
== Expr
a2
Var Name
a1 == Var Name
a2 = Name
a1 forall a. Eq a => a -> a -> Bool
== Name
a2
Def' QName
a1 Suffix
s1 == Def' QName
a2 Suffix
s2 = (QName
a1, Suffix
s1) forall a. Eq a => a -> a -> Bool
== (QName
a2, Suffix
s2)
Proj ProjOrigin
_ AmbiguousQName
a1 == Proj ProjOrigin
_ AmbiguousQName
a2 = AmbiguousQName
a1 forall a. Eq a => a -> a -> Bool
== AmbiguousQName
a2
Con AmbiguousQName
a1 == Con AmbiguousQName
a2 = AmbiguousQName
a1 forall a. Eq a => a -> a -> Bool
== AmbiguousQName
a2
PatternSyn AmbiguousQName
a1 == PatternSyn AmbiguousQName
a2 = AmbiguousQName
a1 forall a. Eq a => a -> a -> Bool
== AmbiguousQName
a2
Macro QName
a1 == Macro QName
a2 = QName
a1 forall a. Eq a => a -> a -> Bool
== QName
a2
Lit ExprInfo
r1 Literal
a1 == Lit ExprInfo
r2 Literal
a2 = (ExprInfo
r1, Literal
a1) forall a. Eq a => a -> a -> Bool
== (ExprInfo
r2, Literal
a2)
QuestionMark MetaInfo
a1 InteractionId
b1 == QuestionMark MetaInfo
a2 InteractionId
b2 = (MetaInfo
a1, InteractionId
b1) forall a. Eq a => a -> a -> Bool
== (MetaInfo
a2, InteractionId
b2)
Underscore MetaInfo
a1 == Underscore MetaInfo
a2 = MetaInfo
a1 forall a. Eq a => a -> a -> Bool
== MetaInfo
a2
Dot ExprInfo
r1 Expr
e1 == Dot ExprInfo
r2 Expr
e2 = (ExprInfo
r1, Expr
e1) forall a. Eq a => a -> a -> Bool
== (ExprInfo
r2, Expr
e2)
App AppInfo
a1 Expr
b1 NamedArg Expr
c1 == App AppInfo
a2 Expr
b2 NamedArg Expr
c2 = (AppInfo
a1, Expr
b1, NamedArg Expr
c1) forall a. Eq a => a -> a -> Bool
== (AppInfo
a2, Expr
b2, NamedArg Expr
c2)
WithApp ExprInfo
a1 Expr
b1 [Expr]
c1 == WithApp ExprInfo
a2 Expr
b2 [Expr]
c2 = (ExprInfo
a1, Expr
b1, [Expr]
c1) forall a. Eq a => a -> a -> Bool
== (ExprInfo
a2, Expr
b2, [Expr]
c2)
Lam ExprInfo
a1 LamBinding
b1 Expr
c1 == Lam ExprInfo
a2 LamBinding
b2 Expr
c2 = (ExprInfo
a1, LamBinding
b1, Expr
c1) forall a. Eq a => a -> a -> Bool
== (ExprInfo
a2, LamBinding
b2, Expr
c2)
AbsurdLam ExprInfo
a1 Hiding
b1 == AbsurdLam ExprInfo
a2 Hiding
b2 = (ExprInfo
a1, Hiding
b1) forall a. Eq a => a -> a -> Bool
== (ExprInfo
a2, Hiding
b2)
ExtendedLam ExprInfo
a1 DefInfo
b1 Erased
c1 QName
d1 List1 Clause
e1 == ExtendedLam ExprInfo
a2 DefInfo
b2 Erased
c2 QName
d2 List1 Clause
e2 = (ExprInfo
a1, DefInfo
b1, Erased
c1, QName
d1, List1 Clause
e1) forall a. Eq a => a -> a -> Bool
==
(ExprInfo
a2, DefInfo
b2, Erased
c2, QName
d2, List1 Clause
e2)
Pi ExprInfo
a1 Telescope1
b1 Expr
c1 == Pi ExprInfo
a2 Telescope1
b2 Expr
c2 = (ExprInfo
a1, Telescope1
b1, Expr
c1) forall a. Eq a => a -> a -> Bool
== (ExprInfo
a2, Telescope1
b2, Expr
c2)
Generalized Set QName
a1 Expr
b1 == Generalized Set QName
a2 Expr
b2 = (Set QName
a1, Expr
b1) forall a. Eq a => a -> a -> Bool
== (Set QName
a2, Expr
b2)
Fun ExprInfo
a1 Arg Expr
b1 Expr
c1 == Fun ExprInfo
a2 Arg Expr
b2 Expr
c2 = (ExprInfo
a1, Arg Expr
b1, Expr
c1) forall a. Eq a => a -> a -> Bool
== (ExprInfo
a2, Arg Expr
b2, Expr
c2)
Let ExprInfo
a1 List1 LetBinding
b1 Expr
c1 == Let ExprInfo
a2 List1 LetBinding
b2 Expr
c2 = (ExprInfo
a1, List1 LetBinding
b1, Expr
c1) forall a. Eq a => a -> a -> Bool
== (ExprInfo
a2, List1 LetBinding
b2, Expr
c2)
Rec ExprInfo
a1 RecordAssigns
b1 == Rec ExprInfo
a2 RecordAssigns
b2 = (ExprInfo
a1, RecordAssigns
b1) forall a. Eq a => a -> a -> Bool
== (ExprInfo
a2, RecordAssigns
b2)
RecUpdate ExprInfo
a1 Expr
b1 Assigns
c1 == RecUpdate ExprInfo
a2 Expr
b2 Assigns
c2 = (ExprInfo
a1, Expr
b1, Assigns
c1) forall a. Eq a => a -> a -> Bool
== (ExprInfo
a2, Expr
b2, Assigns
c2)
Quote ExprInfo
a1 == Quote ExprInfo
a2 = ExprInfo
a1 forall a. Eq a => a -> a -> Bool
== ExprInfo
a2
QuoteTerm ExprInfo
a1 == QuoteTerm ExprInfo
a2 = ExprInfo
a1 forall a. Eq a => a -> a -> Bool
== ExprInfo
a2
Unquote ExprInfo
a1 == Unquote ExprInfo
a2 = ExprInfo
a1 forall a. Eq a => a -> a -> Bool
== ExprInfo
a2
DontCare Expr
a1 == DontCare Expr
a2 = Expr
a1 forall a. Eq a => a -> a -> Bool
== Expr
a2
Expr
_ == Expr
_ = Bool
False
instance Eq Declaration where
ScopedDecl ScopeInfo
_ [Declaration]
a1 == :: Declaration -> Declaration -> Bool
== ScopedDecl ScopeInfo
_ [Declaration]
a2 = [Declaration]
a1 forall a. Eq a => a -> a -> Bool
== [Declaration]
a2
Axiom KindOfName
a1 DefInfo
b1 ArgInfo
c1 Maybe [Occurrence]
d1 QName
e1 Expr
f1 == Axiom KindOfName
a2 DefInfo
b2 ArgInfo
c2 Maybe [Occurrence]
d2 QName
e2 Expr
f2 = (KindOfName
a1, DefInfo
b1, ArgInfo
c1, Maybe [Occurrence]
d1, QName
e1, Expr
f1) forall a. Eq a => a -> a -> Bool
== (KindOfName
a2, DefInfo
b2, ArgInfo
c2, Maybe [Occurrence]
d2, QName
e2, Expr
f2)
Generalize Set QName
a1 DefInfo
b1 ArgInfo
c1 QName
d1 Expr
e1 == Generalize Set QName
a2 DefInfo
b2 ArgInfo
c2 QName
d2 Expr
e2 = (Set QName
a1, DefInfo
b1, ArgInfo
c1, QName
d1, Expr
e1) forall a. Eq a => a -> a -> Bool
== (Set QName
a2, DefInfo
b2, ArgInfo
c2, QName
d2, Expr
e2)
Field DefInfo
a1 QName
b1 Arg Expr
c1 == Field DefInfo
a2 QName
b2 Arg Expr
c2 = (DefInfo
a1, QName
b1, Arg Expr
c1) forall a. Eq a => a -> a -> Bool
== (DefInfo
a2, QName
b2, Arg Expr
c2)
Primitive DefInfo
a1 QName
b1 Arg Expr
c1 == Primitive DefInfo
a2 QName
b2 Arg Expr
c2 = (DefInfo
a1, QName
b1, Arg Expr
c1) forall a. Eq a => a -> a -> Bool
== (DefInfo
a2, QName
b2, Arg Expr
c2)
Mutual MutualInfo
a1 [Declaration]
b1 == Mutual MutualInfo
a2 [Declaration]
b2 = (MutualInfo
a1, [Declaration]
b1) forall a. Eq a => a -> a -> Bool
== (MutualInfo
a2, [Declaration]
b2)
Section Range
a1 Erased
b1 ModuleName
c1 GeneralizeTelescope
d1 [Declaration]
e1 == Section Range
a2 Erased
b2 ModuleName
c2 GeneralizeTelescope
d2 [Declaration]
e2 = (Range
a1, Erased
b1, ModuleName
c1, GeneralizeTelescope
d1, [Declaration]
e1) forall a. Eq a => a -> a -> Bool
== (Range
a2, Erased
b2, ModuleName
c2, GeneralizeTelescope
d2, [Declaration]
e2)
Apply ModuleInfo
a1 Erased
b1 ModuleName
c1 ModuleApplication
d1 ScopeCopyInfo
e1 ImportDirective
f1 == Apply ModuleInfo
a2 Erased
b2 ModuleName
c2 ModuleApplication
d2 ScopeCopyInfo
e2 ImportDirective
f2 = (ModuleInfo
a1, Erased
b1, ModuleName
c1, ModuleApplication
d1, ScopeCopyInfo
e1, ImportDirective
f1) forall a. Eq a => a -> a -> Bool
== (ModuleInfo
a2, Erased
b2, ModuleName
c2, ModuleApplication
d2, ScopeCopyInfo
e2, ImportDirective
f2)
Import ModuleInfo
a1 ModuleName
b1 ImportDirective
c1 == Import ModuleInfo
a2 ModuleName
b2 ImportDirective
c2 = (ModuleInfo
a1, ModuleName
b1, ImportDirective
c1) forall a. Eq a => a -> a -> Bool
== (ModuleInfo
a2, ModuleName
b2, ImportDirective
c2)
Pragma Range
a1 Pragma
b1 == Pragma Range
a2 Pragma
b2 = (Range
a1, Pragma
b1) forall a. Eq a => a -> a -> Bool
== (Range
a2, Pragma
b2)
Open ModuleInfo
a1 ModuleName
b1 ImportDirective
c1 == Open ModuleInfo
a2 ModuleName
b2 ImportDirective
c2 = (ModuleInfo
a1, ModuleName
b1, ImportDirective
c1) forall a. Eq a => a -> a -> Bool
== (ModuleInfo
a2, ModuleName
b2, ImportDirective
c2)
FunDef DefInfo
a1 QName
b1 [Clause]
c1 == FunDef DefInfo
a2 QName
b2 [Clause]
c2 = (DefInfo
a1, QName
b1, [Clause]
c1) forall a. Eq a => a -> a -> Bool
== (DefInfo
a2, QName
b2, [Clause]
c2)
DataSig DefInfo
a1 Erased
b1 QName
c1 GeneralizeTelescope
d1 Expr
e1 == DataSig DefInfo
a2 Erased
b2 QName
c2 GeneralizeTelescope
d2 Expr
e2 = (DefInfo
a1, Erased
b1, QName
c1, GeneralizeTelescope
d1, Expr
e1) forall a. Eq a => a -> a -> Bool
== (DefInfo
a2, Erased
b2, QName
c2, GeneralizeTelescope
d2, Expr
e2)
DataDef DefInfo
a1 QName
b1 UniverseCheck
c1 DataDefParams
d1 [Declaration]
e1 == DataDef DefInfo
a2 QName
b2 UniverseCheck
c2 DataDefParams
d2 [Declaration]
e2 = (DefInfo
a1, QName
b1, UniverseCheck
c1, DataDefParams
d1, [Declaration]
e1) forall a. Eq a => a -> a -> Bool
== (DefInfo
a2, QName
b2, UniverseCheck
c2, DataDefParams
d2, [Declaration]
e2)
RecSig DefInfo
a1 Erased
b1 QName
c1 GeneralizeTelescope
d1 Expr
e1 == RecSig DefInfo
a2 Erased
b2 QName
c2 GeneralizeTelescope
d2 Expr
e2 = (DefInfo
a1, Erased
b1, QName
c1, GeneralizeTelescope
d1, Expr
e1) forall a. Eq a => a -> a -> Bool
== (DefInfo
a2, Erased
b2, QName
c2, GeneralizeTelescope
d2, Expr
e2)
RecDef DefInfo
a1 QName
b1 UniverseCheck
c1 RecordDirectives
d1 DataDefParams
e1 Expr
f1 [Declaration]
g1 == RecDef DefInfo
a2 QName
b2 UniverseCheck
c2 RecordDirectives
d2 DataDefParams
e2 Expr
f2 [Declaration]
g2 = (DefInfo
a1, QName
b1, UniverseCheck
c1, RecordDirectives
d1, DataDefParams
e1, Expr
f1, [Declaration]
g1) forall a. Eq a => a -> a -> Bool
== (DefInfo
a2, QName
b2, UniverseCheck
c2, RecordDirectives
d2, DataDefParams
e2, Expr
f2, [Declaration]
g2)
PatternSynDef QName
a1 [Arg BindName]
b1 Pattern' Void
c1 == PatternSynDef QName
a2 [Arg BindName]
b2 Pattern' Void
c2 = (QName
a1, [Arg BindName]
b1, Pattern' Void
c1) forall a. Eq a => a -> a -> Bool
== (QName
a2, [Arg BindName]
b2, Pattern' Void
c2)
UnquoteDecl MutualInfo
a1 [DefInfo]
b1 [QName]
c1 Expr
d1 == UnquoteDecl MutualInfo
a2 [DefInfo]
b2 [QName]
c2 Expr
d2 = (MutualInfo
a1, [DefInfo]
b1, [QName]
c1, Expr
d1) forall a. Eq a => a -> a -> Bool
== (MutualInfo
a2, [DefInfo]
b2, [QName]
c2, Expr
d2)
UnquoteDef [DefInfo]
a1 [QName]
b1 Expr
c1 == UnquoteDef [DefInfo]
a2 [QName]
b2 Expr
c2 = ([DefInfo]
a1, [QName]
b1, Expr
c1) forall a. Eq a => a -> a -> Bool
== ([DefInfo]
a2, [QName]
b2, Expr
c2)
UnfoldingDecl Range
a1 [QName]
b1 == UnfoldingDecl Range
a2 [QName]
b2 = (Range
a1,[QName]
b1) forall a. Eq a => a -> a -> Bool
== (Range
a2,[QName]
b2)
Declaration
_ == Declaration
_ = Bool
False
instance Underscore Expr where
underscore :: Expr
underscore = MetaInfo -> Expr
Underscore MetaInfo
emptyMetaInfo
isUnderscore :: Expr -> Bool
isUnderscore = forall a. HasCallStack => a
__IMPOSSIBLE__
instance LensHiding LamBinding where
getHiding :: LamBinding -> Hiding
getHiding (DomainFree TacticAttr
_ NamedArg Binder
x) = forall a. LensHiding a => a -> Hiding
getHiding NamedArg Binder
x
getHiding (DomainFull TypedBinding
tb) = forall a. LensHiding a => a -> Hiding
getHiding TypedBinding
tb
mapHiding :: (Hiding -> Hiding) -> LamBinding -> LamBinding
mapHiding Hiding -> Hiding
f (DomainFree TacticAttr
t NamedArg Binder
x) = TacticAttr -> NamedArg Binder -> LamBinding
DomainFree TacticAttr
t forall a b. (a -> b) -> a -> b
$ forall a. LensHiding a => (Hiding -> Hiding) -> a -> a
mapHiding Hiding -> Hiding
f NamedArg Binder
x
mapHiding Hiding -> Hiding
f (DomainFull TypedBinding
tb) = TypedBinding -> LamBinding
DomainFull forall a b. (a -> b) -> a -> b
$ forall a. LensHiding a => (Hiding -> Hiding) -> a -> a
mapHiding Hiding -> Hiding
f TypedBinding
tb
instance LensHiding TypedBinding where
getHiding :: TypedBinding -> Hiding
getHiding (TBind Range
_ TypedBindingInfo
_ (NamedArg Binder
x :| [NamedArg Binder]
_) Expr
_) = forall a. LensHiding a => a -> Hiding
getHiding NamedArg Binder
x
getHiding TLet{} = forall a. Monoid a => a
mempty
mapHiding :: (Hiding -> Hiding) -> TypedBinding -> TypedBinding
mapHiding Hiding -> Hiding
f (TBind Range
r TypedBindingInfo
t List1 (NamedArg Binder)
xs Expr
e) = Range
-> TypedBindingInfo
-> List1 (NamedArg Binder)
-> Expr
-> TypedBinding
TBind Range
r TypedBindingInfo
t ((forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. LensHiding a => (Hiding -> Hiding) -> a -> a
mapHiding) Hiding -> Hiding
f List1 (NamedArg Binder)
xs) Expr
e
mapHiding Hiding -> Hiding
f b :: TypedBinding
b@TLet{} = TypedBinding
b
instance HasRange a => HasRange (Binder' a) where
getRange :: Binder' a -> Range
getRange (Binder Maybe Pattern
p a
n) = forall u t. (HasRange u, HasRange t) => u -> t -> Range
fuseRange Maybe Pattern
p a
n
instance HasRange LamBinding where
getRange :: LamBinding -> Range
getRange (DomainFree TacticAttr
_ NamedArg Binder
x) = forall a. HasRange a => a -> Range
getRange NamedArg Binder
x
getRange (DomainFull TypedBinding
b) = forall a. HasRange a => a -> Range
getRange TypedBinding
b
instance HasRange TypedBinding where
getRange :: TypedBinding -> Range
getRange (TBind Range
r TypedBindingInfo
_ List1 (NamedArg Binder)
_ Expr
_) = Range
r
getRange (TLet Range
r List1 LetBinding
_) = Range
r
instance HasRange Expr where
getRange :: Expr -> Range
getRange (Var Name
x) = forall a. HasRange a => a -> Range
getRange Name
x
getRange (Def' QName
x Suffix
_) = forall a. HasRange a => a -> Range
getRange QName
x
getRange (Proj ProjOrigin
_ AmbiguousQName
x) = forall a. HasRange a => a -> Range
getRange AmbiguousQName
x
getRange (Con AmbiguousQName
x) = forall a. HasRange a => a -> Range
getRange AmbiguousQName
x
getRange (Lit ExprInfo
i Literal
_) = forall a. HasRange a => a -> Range
getRange ExprInfo
i
getRange (QuestionMark MetaInfo
i InteractionId
_) = forall a. HasRange a => a -> Range
getRange MetaInfo
i
getRange (Underscore MetaInfo
i) = forall a. HasRange a => a -> Range
getRange MetaInfo
i
getRange (Dot ExprInfo
i Expr
_) = forall a. HasRange a => a -> Range
getRange ExprInfo
i
getRange (App AppInfo
i Expr
_ NamedArg Expr
_) = forall a. HasRange a => a -> Range
getRange AppInfo
i
getRange (WithApp ExprInfo
i Expr
_ [Expr]
_) = forall a. HasRange a => a -> Range
getRange ExprInfo
i
getRange (Lam ExprInfo
i LamBinding
_ Expr
_) = forall a. HasRange a => a -> Range
getRange ExprInfo
i
getRange (AbsurdLam ExprInfo
i Hiding
_) = forall a. HasRange a => a -> Range
getRange ExprInfo
i
getRange (ExtendedLam ExprInfo
i DefInfo
_ Erased
_ QName
_ List1 Clause
_) = forall a. HasRange a => a -> Range
getRange ExprInfo
i
getRange (Pi ExprInfo
i Telescope1
_ Expr
_) = forall a. HasRange a => a -> Range
getRange ExprInfo
i
getRange (Generalized Set QName
_ Expr
x) = forall a. HasRange a => a -> Range
getRange Expr
x
getRange (Fun ExprInfo
i Arg Expr
_ Expr
_) = forall a. HasRange a => a -> Range
getRange ExprInfo
i
getRange (Let ExprInfo
i List1 LetBinding
_ Expr
_) = forall a. HasRange a => a -> Range
getRange ExprInfo
i
getRange (Rec ExprInfo
i RecordAssigns
_) = forall a. HasRange a => a -> Range
getRange ExprInfo
i
getRange (RecUpdate ExprInfo
i Expr
_ Assigns
_) = forall a. HasRange a => a -> Range
getRange ExprInfo
i
getRange (ScopedExpr ScopeInfo
_ Expr
e) = forall a. HasRange a => a -> Range
getRange Expr
e
getRange (Quote ExprInfo
i) = forall a. HasRange a => a -> Range
getRange ExprInfo
i
getRange (QuoteTerm ExprInfo
i) = forall a. HasRange a => a -> Range
getRange ExprInfo
i
getRange (Unquote ExprInfo
i) = forall a. HasRange a => a -> Range
getRange ExprInfo
i
getRange (DontCare{}) = forall a. Range' a
noRange
getRange (PatternSyn AmbiguousQName
x) = forall a. HasRange a => a -> Range
getRange AmbiguousQName
x
getRange (Macro QName
x) = forall a. HasRange a => a -> Range
getRange QName
x
instance HasRange Declaration where
getRange :: Declaration -> Range
getRange (Axiom KindOfName
_ DefInfo
i ArgInfo
_ Maybe [Occurrence]
_ QName
_ Expr
_ ) = forall a. HasRange a => a -> Range
getRange DefInfo
i
getRange (Generalize Set QName
_ DefInfo
i ArgInfo
_ QName
_ Expr
_) = forall a. HasRange a => a -> Range
getRange DefInfo
i
getRange (Field DefInfo
i QName
_ Arg Expr
_ ) = forall a. HasRange a => a -> Range
getRange DefInfo
i
getRange (Mutual MutualInfo
i [Declaration]
_ ) = forall a. HasRange a => a -> Range
getRange MutualInfo
i
getRange (Section Range
i Erased
_ ModuleName
_ GeneralizeTelescope
_ [Declaration]
_ ) = forall a. HasRange a => a -> Range
getRange Range
i
getRange (Apply ModuleInfo
i Erased
_ ModuleName
_ ModuleApplication
_ ScopeCopyInfo
_ ImportDirective
_) = forall a. HasRange a => a -> Range
getRange ModuleInfo
i
getRange (Import ModuleInfo
i ModuleName
_ ImportDirective
_ ) = forall a. HasRange a => a -> Range
getRange ModuleInfo
i
getRange (Primitive DefInfo
i QName
_ Arg Expr
_ ) = forall a. HasRange a => a -> Range
getRange DefInfo
i
getRange (Pragma Range
i Pragma
_ ) = forall a. HasRange a => a -> Range
getRange Range
i
getRange (Open ModuleInfo
i ModuleName
_ ImportDirective
_ ) = forall a. HasRange a => a -> Range
getRange ModuleInfo
i
getRange (ScopedDecl ScopeInfo
_ [Declaration]
d ) = forall a. HasRange a => a -> Range
getRange [Declaration]
d
getRange (FunDef DefInfo
i QName
_ [Clause]
_ ) = forall a. HasRange a => a -> Range
getRange DefInfo
i
getRange (DataSig DefInfo
i Erased
_ QName
_ GeneralizeTelescope
_ Expr
_ ) = forall a. HasRange a => a -> Range
getRange DefInfo
i
getRange (DataDef DefInfo
i QName
_ UniverseCheck
_ DataDefParams
_ [Declaration]
_ ) = forall a. HasRange a => a -> Range
getRange DefInfo
i
getRange (RecSig DefInfo
i Erased
_ QName
_ GeneralizeTelescope
_ Expr
_ ) = forall a. HasRange a => a -> Range
getRange DefInfo
i
getRange (RecDef DefInfo
i QName
_ UniverseCheck
_ RecordDirectives
_ DataDefParams
_ Expr
_ [Declaration]
_) = forall a. HasRange a => a -> Range
getRange DefInfo
i
getRange (PatternSynDef QName
x [Arg BindName]
_ Pattern' Void
_ ) = forall a. HasRange a => a -> Range
getRange QName
x
getRange (UnquoteDecl MutualInfo
_ [DefInfo]
i [QName]
_ Expr
_) = forall a. HasRange a => a -> Range
getRange [DefInfo]
i
getRange (UnquoteDef [DefInfo]
i [QName]
_ Expr
_) = forall a. HasRange a => a -> Range
getRange [DefInfo]
i
getRange (UnquoteData [DefInfo]
i QName
_ UniverseCheck
_ [DefInfo]
j [QName]
_ Expr
_) = forall a. HasRange a => a -> Range
getRange ([DefInfo]
i, [DefInfo]
j)
getRange (UnfoldingDecl Range
r [QName]
_) = Range
r
instance HasRange (Pattern' e) where
getRange :: Pattern' e -> Range
getRange (VarP BindName
x) = forall a. HasRange a => a -> Range
getRange BindName
x
getRange (ConP ConPatInfo
i AmbiguousQName
_ NAPs e
_) = forall a. HasRange a => a -> Range
getRange ConPatInfo
i
getRange (ProjP PatInfo
i ProjOrigin
_ AmbiguousQName
_) = forall a. HasRange a => a -> Range
getRange PatInfo
i
getRange (DefP PatInfo
i AmbiguousQName
_ NAPs e
_) = forall a. HasRange a => a -> Range
getRange PatInfo
i
getRange (WildP PatInfo
i) = forall a. HasRange a => a -> Range
getRange PatInfo
i
getRange (AsP PatInfo
i BindName
_ Pattern' e
_) = forall a. HasRange a => a -> Range
getRange PatInfo
i
getRange (DotP PatInfo
i e
_) = forall a. HasRange a => a -> Range
getRange PatInfo
i
getRange (AbsurdP PatInfo
i) = forall a. HasRange a => a -> Range
getRange PatInfo
i
getRange (LitP PatInfo
i Literal
l) = forall a. HasRange a => a -> Range
getRange PatInfo
i
getRange (PatternSynP PatInfo
i AmbiguousQName
_ NAPs e
_) = forall a. HasRange a => a -> Range
getRange PatInfo
i
getRange (RecP PatInfo
i [FieldAssignment' (Pattern' e)]
_) = forall a. HasRange a => a -> Range
getRange PatInfo
i
getRange (EqualP PatInfo
i [(e, e)]
_) = forall a. HasRange a => a -> Range
getRange PatInfo
i
getRange (WithP PatInfo
i Pattern' e
_) = forall a. HasRange a => a -> Range
getRange PatInfo
i
getRange (AnnP PatInfo
i e
_ Pattern' e
_) = forall a. HasRange a => a -> Range
getRange PatInfo
i
instance HasRange SpineLHS where
getRange :: SpineLHS -> Range
getRange (SpineLHS LHSInfo
i QName
_ [NamedArg Pattern]
_) = forall a. HasRange a => a -> Range
getRange LHSInfo
i
instance HasRange LHS where
getRange :: LHS -> Range
getRange (LHS LHSInfo
i LHSCore
_) = forall a. HasRange a => a -> Range
getRange LHSInfo
i
instance HasRange (LHSCore' e) where
getRange :: LHSCore' e -> Range
getRange (LHSHead QName
f [NamedArg (Pattern' e)]
ps) = forall u t. (HasRange u, HasRange t) => u -> t -> Range
fuseRange QName
f [NamedArg (Pattern' e)]
ps
getRange (LHSProj AmbiguousQName
d NamedArg (LHSCore' e)
lhscore [NamedArg (Pattern' e)]
ps) = AmbiguousQName
d forall u t. (HasRange u, HasRange t) => u -> t -> Range
`fuseRange` NamedArg (LHSCore' e)
lhscore forall u t. (HasRange u, HasRange t) => u -> t -> Range
`fuseRange` [NamedArg (Pattern' e)]
ps
getRange (LHSWith LHSCore' e
h [Arg (Pattern' e)]
wps [NamedArg (Pattern' e)]
ps) = LHSCore' e
h forall u t. (HasRange u, HasRange t) => u -> t -> Range
`fuseRange` [Arg (Pattern' e)]
wps forall u t. (HasRange u, HasRange t) => u -> t -> Range
`fuseRange` [NamedArg (Pattern' e)]
ps
instance HasRange a => HasRange (Clause' a) where
getRange :: Clause' a -> Range
getRange (Clause a
lhs [ProblemEq]
_ RHS
rhs WhereDeclarations
ds Bool
catchall) = forall a. HasRange a => a -> Range
getRange (a
lhs, RHS
rhs, WhereDeclarations
ds)
instance HasRange RHS where
getRange :: RHS -> Range
getRange RHS
AbsurdRHS = forall a. Range' a
noRange
getRange (RHS Expr
e Maybe Expr
_) = forall a. HasRange a => a -> Range
getRange Expr
e
getRange (WithRHS QName
_ [WithExpr]
e List1 Clause
cs) = forall u t. (HasRange u, HasRange t) => u -> t -> Range
fuseRange [WithExpr]
e List1 Clause
cs
getRange (RewriteRHS [RewriteEqn]
xes [ProblemEq]
_ RHS
rhs WhereDeclarations
wh) = forall a. HasRange a => a -> Range
getRange ([RewriteEqn]
xes, RHS
rhs, WhereDeclarations
wh)
instance HasRange WhereDeclarations where
getRange :: WhereDeclarations -> Range
getRange (WhereDecls Maybe ModuleName
_ Bool
_ Maybe Declaration
ds) = forall a. HasRange a => a -> Range
getRange Maybe Declaration
ds
instance HasRange LetBinding where
getRange :: LetBinding -> Range
getRange (LetBind LetInfo
i ArgInfo
_ BindName
_ Expr
_ Expr
_ ) = forall a. HasRange a => a -> Range
getRange LetInfo
i
getRange (LetPatBind LetInfo
i Pattern
_ Expr
_ ) = forall a. HasRange a => a -> Range
getRange LetInfo
i
getRange (LetApply ModuleInfo
i Erased
_ ModuleName
_ ModuleApplication
_ ScopeCopyInfo
_ ImportDirective
_ ) = forall a. HasRange a => a -> Range
getRange ModuleInfo
i
getRange (LetOpen ModuleInfo
i ModuleName
_ ImportDirective
_ ) = forall a. HasRange a => a -> Range
getRange ModuleInfo
i
getRange (LetDeclaredVariable BindName
x) = forall a. HasRange a => a -> Range
getRange BindName
x
instance SetRange (Pattern' a) where
setRange :: Range -> Pattern' a -> Pattern' a
setRange Range
r (VarP BindName
x) = forall e. BindName -> Pattern' e
VarP (forall a. SetRange a => Range -> a -> a
setRange Range
r BindName
x)
setRange Range
r (ConP ConPatInfo
i AmbiguousQName
ns NAPs a
as) = forall e. ConPatInfo -> AmbiguousQName -> NAPs e -> Pattern' e
ConP (forall a. SetRange a => Range -> a -> a
setRange Range
r ConPatInfo
i) AmbiguousQName
ns NAPs a
as
setRange Range
r (ProjP PatInfo
_ ProjOrigin
o AmbiguousQName
ns) = forall e. PatInfo -> ProjOrigin -> AmbiguousQName -> Pattern' e
ProjP (Range -> PatInfo
PatRange Range
r) ProjOrigin
o AmbiguousQName
ns
setRange Range
r (DefP PatInfo
_ AmbiguousQName
ns NAPs a
as) = forall e. PatInfo -> AmbiguousQName -> NAPs e -> Pattern' e
DefP (Range -> PatInfo
PatRange Range
r) AmbiguousQName
ns NAPs a
as
setRange Range
r (WildP PatInfo
_) = forall e. PatInfo -> Pattern' e
WildP (Range -> PatInfo
PatRange Range
r)
setRange Range
r (AsP PatInfo
_ BindName
n Pattern' a
p) = forall e. PatInfo -> BindName -> Pattern' e -> Pattern' e
AsP (Range -> PatInfo
PatRange Range
r) (forall a. SetRange a => Range -> a -> a
setRange Range
r BindName
n) Pattern' a
p
setRange Range
r (DotP PatInfo
_ a
e) = forall e. PatInfo -> e -> Pattern' e
DotP (Range -> PatInfo
PatRange Range
r) a
e
setRange Range
r (AbsurdP PatInfo
_) = forall e. PatInfo -> Pattern' e
AbsurdP (Range -> PatInfo
PatRange Range
r)
setRange Range
r (LitP PatInfo
_ Literal
l) = forall e. PatInfo -> Literal -> Pattern' e
LitP (Range -> PatInfo
PatRange Range
r) Literal
l
setRange Range
r (PatternSynP PatInfo
_ AmbiguousQName
n NAPs a
as) = forall e. PatInfo -> AmbiguousQName -> NAPs e -> Pattern' e
PatternSynP (Range -> PatInfo
PatRange Range
r) AmbiguousQName
n NAPs a
as
setRange Range
r (RecP PatInfo
i [FieldAssignment' (Pattern' a)]
as) = forall e. PatInfo -> [FieldAssignment' (Pattern' e)] -> Pattern' e
RecP (Range -> PatInfo
PatRange Range
r) [FieldAssignment' (Pattern' a)]
as
setRange Range
r (EqualP PatInfo
_ [(a, a)]
es) = forall e. PatInfo -> [(e, e)] -> Pattern' e
EqualP (Range -> PatInfo
PatRange Range
r) [(a, a)]
es
setRange Range
r (WithP PatInfo
i Pattern' a
p) = forall e. PatInfo -> Pattern' e -> Pattern' e
WithP (forall a. SetRange a => Range -> a -> a
setRange Range
r PatInfo
i) Pattern' a
p
setRange Range
r (AnnP PatInfo
i a
a Pattern' a
p) = forall e. PatInfo -> e -> Pattern' e -> Pattern' e
AnnP (forall a. SetRange a => Range -> a -> a
setRange Range
r PatInfo
i) a
a Pattern' a
p
instance KillRange a => KillRange (Binder' a) where
killRange :: KillRangeT (Binder' a)
killRange (Binder Maybe Pattern
a a
b) = forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN forall a. Maybe Pattern -> a -> Binder' a
Binder Maybe Pattern
a a
b
instance KillRange LamBinding where
killRange :: LamBinding -> LamBinding
killRange (DomainFree TacticAttr
t NamedArg Binder
x) = forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN TacticAttr -> NamedArg Binder -> LamBinding
DomainFree TacticAttr
t NamedArg Binder
x
killRange (DomainFull TypedBinding
b) = forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN TypedBinding -> LamBinding
DomainFull TypedBinding
b
instance KillRange GeneralizeTelescope where
killRange :: KillRangeT GeneralizeTelescope
killRange (GeneralizeTel Map QName Name
s Telescope
tel) = Map QName Name -> Telescope -> GeneralizeTelescope
GeneralizeTel Map QName Name
s (forall a. KillRange a => KillRangeT a
killRange Telescope
tel)
instance KillRange DataDefParams where
killRange :: KillRangeT DataDefParams
killRange (DataDefParams Set Name
s [LamBinding]
tel) = Set Name -> [LamBinding] -> DataDefParams
DataDefParams Set Name
s (forall a. KillRange a => KillRangeT a
killRange [LamBinding]
tel)
instance KillRange TypedBindingInfo where
killRange :: KillRangeT TypedBindingInfo
killRange (TypedBindingInfo TacticAttr
a Bool
b) = forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN TacticAttr -> Bool -> TypedBindingInfo
TypedBindingInfo TacticAttr
a Bool
b
instance KillRange TypedBinding where
killRange :: TypedBinding -> TypedBinding
killRange (TBind Range
r TypedBindingInfo
t List1 (NamedArg Binder)
xs Expr
e) = forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN Range
-> TypedBindingInfo
-> List1 (NamedArg Binder)
-> Expr
-> TypedBinding
TBind Range
r TypedBindingInfo
t List1 (NamedArg Binder)
xs Expr
e
killRange (TLet Range
r List1 LetBinding
lbs) = forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN Range -> List1 LetBinding -> TypedBinding
TLet Range
r List1 LetBinding
lbs
instance KillRange Expr where
killRange :: Expr -> Expr
killRange (Var Name
x) = forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN Name -> Expr
Var Name
x
killRange (Def' QName
x Suffix
v) = forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN QName -> Suffix -> Expr
Def' QName
x Suffix
v
killRange (Proj ProjOrigin
o AmbiguousQName
x) = forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN (ProjOrigin -> AmbiguousQName -> Expr
Proj ProjOrigin
o) AmbiguousQName
x
killRange (Con AmbiguousQName
x) = forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN AmbiguousQName -> Expr
Con AmbiguousQName
x
killRange (Lit ExprInfo
i Literal
l) = forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN ExprInfo -> Literal -> Expr
Lit ExprInfo
i Literal
l
killRange (QuestionMark MetaInfo
i InteractionId
ii) = forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN MetaInfo -> InteractionId -> Expr
QuestionMark MetaInfo
i InteractionId
ii
killRange (Underscore MetaInfo
i) = forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN MetaInfo -> Expr
Underscore MetaInfo
i
killRange (Dot ExprInfo
i Expr
e) = forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN ExprInfo -> Expr -> Expr
Dot ExprInfo
i Expr
e
killRange (App AppInfo
i Expr
e1 NamedArg Expr
e2) = forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN AppInfo -> Expr -> NamedArg Expr -> Expr
App AppInfo
i Expr
e1 NamedArg Expr
e2
killRange (WithApp ExprInfo
i Expr
e [Expr]
es) = forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN ExprInfo -> Expr -> [Expr] -> Expr
WithApp ExprInfo
i Expr
e [Expr]
es
killRange (Lam ExprInfo
i LamBinding
b Expr
e) = forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN ExprInfo -> LamBinding -> Expr -> Expr
Lam ExprInfo
i LamBinding
b Expr
e
killRange (AbsurdLam ExprInfo
i Hiding
h) = forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN ExprInfo -> Hiding -> Expr
AbsurdLam ExprInfo
i Hiding
h
killRange (ExtendedLam ExprInfo
i DefInfo
n Erased
e QName
d List1 Clause
ps) = forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN ExprInfo -> DefInfo -> Erased -> QName -> List1 Clause -> Expr
ExtendedLam ExprInfo
i DefInfo
n Erased
e QName
d List1 Clause
ps
killRange (Pi ExprInfo
i Telescope1
a Expr
b) = forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN ExprInfo -> Telescope1 -> Expr -> Expr
Pi ExprInfo
i Telescope1
a Expr
b
killRange (Generalized Set QName
s Expr
x) = forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN (Set QName -> Expr -> Expr
Generalized Set QName
s) Expr
x
killRange (Fun ExprInfo
i Arg Expr
a Expr
b) = forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN ExprInfo -> Arg Expr -> Expr -> Expr
Fun ExprInfo
i Arg Expr
a Expr
b
killRange (Let ExprInfo
i List1 LetBinding
ds Expr
e) = forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN ExprInfo -> List1 LetBinding -> Expr -> Expr
Let ExprInfo
i List1 LetBinding
ds Expr
e
killRange (Rec ExprInfo
i RecordAssigns
fs) = forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN ExprInfo -> RecordAssigns -> Expr
Rec ExprInfo
i RecordAssigns
fs
killRange (RecUpdate ExprInfo
i Expr
e Assigns
fs) = forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN ExprInfo -> Expr -> Assigns -> Expr
RecUpdate ExprInfo
i Expr
e Assigns
fs
killRange (ScopedExpr ScopeInfo
s Expr
e) = forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN (ScopeInfo -> Expr -> Expr
ScopedExpr ScopeInfo
s) Expr
e
killRange (Quote ExprInfo
i) = forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN ExprInfo -> Expr
Quote ExprInfo
i
killRange (QuoteTerm ExprInfo
i) = forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN ExprInfo -> Expr
QuoteTerm ExprInfo
i
killRange (Unquote ExprInfo
i) = forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN ExprInfo -> Expr
Unquote ExprInfo
i
killRange (DontCare Expr
e) = forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN Expr -> Expr
DontCare Expr
e
killRange (PatternSyn AmbiguousQName
x) = forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN AmbiguousQName -> Expr
PatternSyn AmbiguousQName
x
killRange (Macro QName
x) = forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN QName -> Expr
Macro QName
x
instance KillRange Suffix where
killRange :: KillRangeT Suffix
killRange = forall a. a -> a
id
instance KillRange Declaration where
killRange :: KillRangeT Declaration
killRange (Axiom KindOfName
p DefInfo
i ArgInfo
a Maybe [Occurrence]
b QName
c Expr
d ) = forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN (\DefInfo
i ArgInfo
a QName
c Expr
d -> KindOfName
-> DefInfo
-> ArgInfo
-> Maybe [Occurrence]
-> QName
-> Expr
-> Declaration
Axiom KindOfName
p DefInfo
i ArgInfo
a Maybe [Occurrence]
b QName
c Expr
d) DefInfo
i ArgInfo
a QName
c Expr
d
killRange (Generalize Set QName
s DefInfo
i ArgInfo
j QName
x Expr
e ) = forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN (Set QName -> DefInfo -> ArgInfo -> QName -> Expr -> Declaration
Generalize Set QName
s) DefInfo
i ArgInfo
j QName
x Expr
e
killRange (Field DefInfo
i QName
a Arg Expr
b ) = forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN DefInfo -> QName -> Arg Expr -> Declaration
Field DefInfo
i QName
a Arg Expr
b
killRange (Mutual MutualInfo
i [Declaration]
a ) = forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN MutualInfo -> [Declaration] -> Declaration
Mutual MutualInfo
i [Declaration]
a
killRange (Section Range
i Erased
a ModuleName
b GeneralizeTelescope
c [Declaration]
d ) = forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN Range
-> Erased
-> ModuleName
-> GeneralizeTelescope
-> [Declaration]
-> Declaration
Section Range
i Erased
a ModuleName
b GeneralizeTelescope
c [Declaration]
d
killRange (Apply ModuleInfo
i Erased
a ModuleName
b ModuleApplication
c ScopeCopyInfo
d ImportDirective
e ) = forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN ModuleInfo
-> Erased
-> ModuleName
-> ModuleApplication
-> ScopeCopyInfo
-> ImportDirective
-> Declaration
Apply ModuleInfo
i Erased
a ModuleName
b ModuleApplication
c ScopeCopyInfo
d ImportDirective
e
killRange (Import ModuleInfo
i ModuleName
a ImportDirective
b ) = forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN ModuleInfo -> ModuleName -> ImportDirective -> Declaration
Import ModuleInfo
i ModuleName
a ImportDirective
b
killRange (Primitive DefInfo
i QName
a Arg Expr
b ) = forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN DefInfo -> QName -> Arg Expr -> Declaration
Primitive DefInfo
i QName
a Arg Expr
b
killRange (Pragma Range
i Pragma
a ) = Range -> Pragma -> Declaration
Pragma (forall a. KillRange a => KillRangeT a
killRange Range
i) Pragma
a
killRange (Open ModuleInfo
i ModuleName
x ImportDirective
dir ) = forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN ModuleInfo -> ModuleName -> ImportDirective -> Declaration
Open ModuleInfo
i ModuleName
x ImportDirective
dir
killRange (ScopedDecl ScopeInfo
a [Declaration]
d ) = forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN (ScopeInfo -> [Declaration] -> Declaration
ScopedDecl ScopeInfo
a) [Declaration]
d
killRange (FunDef DefInfo
i QName
a [Clause]
b ) = forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN DefInfo -> QName -> [Clause] -> Declaration
FunDef DefInfo
i QName
a [Clause]
b
killRange (DataSig DefInfo
i Erased
a QName
b GeneralizeTelescope
c Expr
d ) = forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN DefInfo
-> Erased -> QName -> GeneralizeTelescope -> Expr -> Declaration
DataSig DefInfo
i Erased
a QName
b GeneralizeTelescope
c Expr
d
killRange (DataDef DefInfo
i QName
a UniverseCheck
b DataDefParams
c [Declaration]
d ) = forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN DefInfo
-> QName
-> UniverseCheck
-> DataDefParams
-> [Declaration]
-> Declaration
DataDef DefInfo
i QName
a UniverseCheck
b DataDefParams
c [Declaration]
d
killRange (RecSig DefInfo
i Erased
a QName
b GeneralizeTelescope
c Expr
d ) = forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN DefInfo
-> Erased -> QName -> GeneralizeTelescope -> Expr -> Declaration
RecSig DefInfo
i Erased
a QName
b GeneralizeTelescope
c Expr
d
killRange (RecDef DefInfo
i QName
a UniverseCheck
b RecordDirectives
c DataDefParams
d Expr
e [Declaration]
f ) = forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN DefInfo
-> QName
-> UniverseCheck
-> RecordDirectives
-> DataDefParams
-> Expr
-> [Declaration]
-> Declaration
RecDef DefInfo
i QName
a UniverseCheck
b RecordDirectives
c DataDefParams
d Expr
e [Declaration]
f
killRange (PatternSynDef QName
x [Arg BindName]
xs Pattern' Void
p ) = forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN QName -> [Arg BindName] -> Pattern' Void -> Declaration
PatternSynDef QName
x [Arg BindName]
xs Pattern' Void
p
killRange (UnquoteDecl MutualInfo
mi [DefInfo]
i [QName]
x Expr
e ) = forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN MutualInfo -> [DefInfo] -> [QName] -> Expr -> Declaration
UnquoteDecl MutualInfo
mi [DefInfo]
i [QName]
x Expr
e
killRange (UnquoteDef [DefInfo]
i [QName]
x Expr
e ) = forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN [DefInfo] -> [QName] -> Expr -> Declaration
UnquoteDef [DefInfo]
i [QName]
x Expr
e
killRange (UnquoteData [DefInfo]
i QName
xs UniverseCheck
uc [DefInfo]
j [QName]
cs Expr
e) = forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN [DefInfo]
-> QName
-> UniverseCheck
-> [DefInfo]
-> [QName]
-> Expr
-> Declaration
UnquoteData [DefInfo]
i QName
xs UniverseCheck
uc [DefInfo]
j [QName]
cs Expr
e
killRange (UnfoldingDecl Range
r [QName]
xs) = forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN Range -> [QName] -> Declaration
UnfoldingDecl Range
r [QName]
xs
instance KillRange ModuleApplication where
killRange :: KillRangeT ModuleApplication
killRange (SectionApp Telescope
a ModuleName
b [NamedArg Expr]
c ) = forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN Telescope -> ModuleName -> [NamedArg Expr] -> ModuleApplication
SectionApp Telescope
a ModuleName
b [NamedArg Expr]
c
killRange (RecordModuleInstance ModuleName
a) = forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN ModuleName -> ModuleApplication
RecordModuleInstance ModuleName
a
instance KillRange ScopeCopyInfo where
killRange :: KillRangeT ScopeCopyInfo
killRange (ScopeCopyInfo Ren ModuleName
a Ren QName
b) = forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN Ren ModuleName -> Ren QName -> ScopeCopyInfo
ScopeCopyInfo Ren ModuleName
a Ren QName
b
instance KillRange e => KillRange (Pattern' e) where
killRange :: KillRangeT (Pattern' e)
killRange (VarP BindName
x) = forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN forall e. BindName -> Pattern' e
VarP BindName
x
killRange (ConP ConPatInfo
i AmbiguousQName
a NAPs e
b) = forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN forall e. ConPatInfo -> AmbiguousQName -> NAPs e -> Pattern' e
ConP ConPatInfo
i AmbiguousQName
a NAPs e
b
killRange (ProjP PatInfo
i ProjOrigin
o AmbiguousQName
a) = forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN forall e. PatInfo -> ProjOrigin -> AmbiguousQName -> Pattern' e
ProjP PatInfo
i ProjOrigin
o AmbiguousQName
a
killRange (DefP PatInfo
i AmbiguousQName
a NAPs e
b) = forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN forall e. PatInfo -> AmbiguousQName -> NAPs e -> Pattern' e
DefP PatInfo
i AmbiguousQName
a NAPs e
b
killRange (WildP PatInfo
i) = forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN forall e. PatInfo -> Pattern' e
WildP PatInfo
i
killRange (AsP PatInfo
i BindName
a Pattern' e
b) = forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN forall e. PatInfo -> BindName -> Pattern' e -> Pattern' e
AsP PatInfo
i BindName
a Pattern' e
b
killRange (DotP PatInfo
i e
a) = forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN forall e. PatInfo -> e -> Pattern' e
DotP PatInfo
i e
a
killRange (AbsurdP PatInfo
i) = forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN forall e. PatInfo -> Pattern' e
AbsurdP PatInfo
i
killRange (LitP PatInfo
i Literal
l) = forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN forall e. PatInfo -> Literal -> Pattern' e
LitP PatInfo
i Literal
l
killRange (PatternSynP PatInfo
i AmbiguousQName
a NAPs e
p) = forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN forall e. PatInfo -> AmbiguousQName -> NAPs e -> Pattern' e
PatternSynP PatInfo
i AmbiguousQName
a NAPs e
p
killRange (RecP PatInfo
i [FieldAssignment' (Pattern' e)]
as) = forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN forall e. PatInfo -> [FieldAssignment' (Pattern' e)] -> Pattern' e
RecP PatInfo
i [FieldAssignment' (Pattern' e)]
as
killRange (EqualP PatInfo
i [(e, e)]
es) = forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN forall e. PatInfo -> [(e, e)] -> Pattern' e
EqualP PatInfo
i [(e, e)]
es
killRange (WithP PatInfo
i Pattern' e
p) = forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN forall e. PatInfo -> Pattern' e -> Pattern' e
WithP PatInfo
i Pattern' e
p
killRange (AnnP PatInfo
i e
a Pattern' e
p) = forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN forall e. PatInfo -> e -> Pattern' e -> Pattern' e
AnnP PatInfo
i e
a Pattern' e
p
instance KillRange SpineLHS where
killRange :: KillRangeT SpineLHS
killRange (SpineLHS LHSInfo
i QName
a [NamedArg Pattern]
b) = forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN LHSInfo -> QName -> [NamedArg Pattern] -> SpineLHS
SpineLHS LHSInfo
i QName
a [NamedArg Pattern]
b
instance KillRange LHS where
killRange :: KillRangeT LHS
killRange (LHS LHSInfo
i LHSCore
a) = forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN LHSInfo -> LHSCore -> LHS
LHS LHSInfo
i LHSCore
a
instance KillRange e => KillRange (LHSCore' e) where
killRange :: KillRangeT (LHSCore' e)
killRange (LHSHead QName
a [NamedArg (Pattern' e)]
b) = forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN forall e. QName -> [NamedArg (Pattern' e)] -> LHSCore' e
LHSHead QName
a [NamedArg (Pattern' e)]
b
killRange (LHSProj AmbiguousQName
a NamedArg (LHSCore' e)
b [NamedArg (Pattern' e)]
c) = forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN forall e.
AmbiguousQName
-> NamedArg (LHSCore' e) -> [NamedArg (Pattern' e)] -> LHSCore' e
LHSProj AmbiguousQName
a NamedArg (LHSCore' e)
b [NamedArg (Pattern' e)]
c
killRange (LHSWith LHSCore' e
a [Arg (Pattern' e)]
b [NamedArg (Pattern' e)]
c) = forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN forall e.
LHSCore' e
-> [Arg (Pattern' e)] -> [NamedArg (Pattern' e)] -> LHSCore' e
LHSWith LHSCore' e
a [Arg (Pattern' e)]
b [NamedArg (Pattern' e)]
c
instance KillRange a => KillRange (Clause' a) where
killRange :: KillRangeT (Clause' a)
killRange (Clause a
lhs [ProblemEq]
spats RHS
rhs WhereDeclarations
ds Bool
catchall) = forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN forall lhs.
lhs
-> [ProblemEq] -> RHS -> WhereDeclarations -> Bool -> Clause' lhs
Clause a
lhs [ProblemEq]
spats RHS
rhs WhereDeclarations
ds Bool
catchall
instance KillRange ProblemEq where
killRange :: KillRangeT ProblemEq
killRange (ProblemEq Pattern
p Term
v Dom Type
a) = forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN Pattern -> Term -> Dom Type -> ProblemEq
ProblemEq Pattern
p Term
v Dom Type
a
instance KillRange RHS where
killRange :: RHS -> RHS
killRange RHS
AbsurdRHS = RHS
AbsurdRHS
killRange (RHS Expr
e Maybe Expr
c) = forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN Expr -> Maybe Expr -> RHS
RHS Expr
e Maybe Expr
c
killRange (WithRHS QName
q [WithExpr]
e List1 Clause
cs) = forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN QName -> [WithExpr] -> List1 Clause -> RHS
WithRHS QName
q [WithExpr]
e List1 Clause
cs
killRange (RewriteRHS [RewriteEqn]
xes [ProblemEq]
spats RHS
rhs WhereDeclarations
wh) = forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN [RewriteEqn] -> [ProblemEq] -> RHS -> WhereDeclarations -> RHS
RewriteRHS [RewriteEqn]
xes [ProblemEq]
spats RHS
rhs WhereDeclarations
wh
instance KillRange WhereDeclarations where
killRange :: KillRangeT WhereDeclarations
killRange (WhereDecls Maybe ModuleName
a Bool
b Maybe Declaration
c) = forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN Maybe ModuleName -> Bool -> Maybe Declaration -> WhereDeclarations
WhereDecls Maybe ModuleName
a Bool
b Maybe Declaration
c
instance KillRange LetBinding where
killRange :: KillRangeT LetBinding
killRange (LetBind LetInfo
i ArgInfo
info BindName
a Expr
b Expr
c) = forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN LetInfo -> ArgInfo -> BindName -> Expr -> Expr -> LetBinding
LetBind LetInfo
i ArgInfo
info BindName
a Expr
b Expr
c
killRange (LetPatBind LetInfo
i Pattern
a Expr
b ) = forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN LetInfo -> Pattern -> Expr -> LetBinding
LetPatBind LetInfo
i Pattern
a Expr
b
killRange (LetApply ModuleInfo
i Erased
a ModuleName
b ModuleApplication
c ScopeCopyInfo
d ImportDirective
e ) = forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN ModuleInfo
-> Erased
-> ModuleName
-> ModuleApplication
-> ScopeCopyInfo
-> ImportDirective
-> LetBinding
LetApply ModuleInfo
i Erased
a ModuleName
b ModuleApplication
c ScopeCopyInfo
d ImportDirective
e
killRange (LetOpen ModuleInfo
i ModuleName
x ImportDirective
dir ) = forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN ModuleInfo -> ModuleName -> ImportDirective -> LetBinding
LetOpen ModuleInfo
i ModuleName
x ImportDirective
dir
killRange (LetDeclaredVariable BindName
x) = forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN BindName -> LetBinding
LetDeclaredVariable BindName
x
instance NFData Expr
instance NFData ScopeCopyInfo
instance NFData Declaration
instance NFData ModuleApplication
instance NFData Pragma
instance NFData LetBinding
instance NFData a => NFData (Binder' a)
instance NFData LamBinding
instance NFData TypedBinding
instance NFData TypedBindingInfo
instance NFData GeneralizeTelescope
instance NFData DataDefParams
instance NFData ProblemEq
instance NFData lhs => NFData (Clause' lhs)
instance NFData WhereDeclarations
instance NFData RHS
instance NFData SpineLHS
instance NFData LHS
instance NFData e => NFData (LHSCore' e)
instance NFData e => NFData (Pattern' e)
axiomName :: Declaration -> QName
axiomName :: Declaration -> QName
axiomName (Axiom KindOfName
_ DefInfo
_ ArgInfo
_ Maybe [Occurrence]
_ QName
q Expr
_) = QName
q
axiomName (ScopedDecl ScopeInfo
_ (Declaration
d:[Declaration]
_)) = Declaration -> QName
axiomName Declaration
d
axiomName Declaration
_ = forall a. HasCallStack => a
__IMPOSSIBLE__
class AnyAbstract a where
anyAbstract :: a -> Bool
instance AnyAbstract a => AnyAbstract [a] where
anyAbstract :: [a] -> Bool
anyAbstract = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
Fold.any forall a. AnyAbstract a => a -> Bool
anyAbstract
instance AnyAbstract Declaration where
anyAbstract :: Declaration -> Bool
anyAbstract (Axiom KindOfName
_ DefInfo
i ArgInfo
_ Maybe [Occurrence]
_ QName
_ Expr
_) = forall t. DefInfo' t -> IsAbstract
defAbstract DefInfo
i forall a. Eq a => a -> a -> Bool
== IsAbstract
AbstractDef
anyAbstract (Field DefInfo
i QName
_ Arg Expr
_) = forall t. DefInfo' t -> IsAbstract
defAbstract DefInfo
i forall a. Eq a => a -> a -> Bool
== IsAbstract
AbstractDef
anyAbstract (Mutual MutualInfo
_ [Declaration]
ds) = forall a. AnyAbstract a => a -> Bool
anyAbstract [Declaration]
ds
anyAbstract (ScopedDecl ScopeInfo
_ [Declaration]
ds) = forall a. AnyAbstract a => a -> Bool
anyAbstract [Declaration]
ds
anyAbstract (Section Range
_ Erased
_ ModuleName
_ GeneralizeTelescope
_ [Declaration]
ds) = forall a. AnyAbstract a => a -> Bool
anyAbstract [Declaration]
ds
anyAbstract (FunDef DefInfo
i QName
_ [Clause]
_) = forall t. DefInfo' t -> IsAbstract
defAbstract DefInfo
i forall a. Eq a => a -> a -> Bool
== IsAbstract
AbstractDef
anyAbstract (DataDef DefInfo
i QName
_ UniverseCheck
_ DataDefParams
_ [Declaration]
_) = forall t. DefInfo' t -> IsAbstract
defAbstract DefInfo
i forall a. Eq a => a -> a -> Bool
== IsAbstract
AbstractDef
anyAbstract (RecDef DefInfo
i QName
_ UniverseCheck
_ RecordDirectives
_ DataDefParams
_ Expr
_ [Declaration]
_) = forall t. DefInfo' t -> IsAbstract
defAbstract DefInfo
i forall a. Eq a => a -> a -> Bool
== IsAbstract
AbstractDef
anyAbstract (DataSig DefInfo
i Erased
_ QName
_ GeneralizeTelescope
_ Expr
_) = forall t. DefInfo' t -> IsAbstract
defAbstract DefInfo
i forall a. Eq a => a -> a -> Bool
== IsAbstract
AbstractDef
anyAbstract (RecSig DefInfo
i Erased
_ QName
_ GeneralizeTelescope
_ Expr
_) = forall t. DefInfo' t -> IsAbstract
defAbstract DefInfo
i forall a. Eq a => a -> a -> Bool
== IsAbstract
AbstractDef
anyAbstract Declaration
_ = forall a. HasCallStack => a
__IMPOSSIBLE__
class NameToExpr a where
nameToExpr :: a -> Expr
instance NameToExpr AbstractName where
nameToExpr :: AbstractName -> Expr
nameToExpr AbstractName
d =
case AbstractName -> KindOfName
anameKind AbstractName
d of
KindOfName
DataName -> QName -> Expr
Def QName
x
KindOfName
RecName -> QName -> Expr
Def QName
x
KindOfName
AxiomName -> QName -> Expr
Def QName
x
KindOfName
PrimName -> QName -> Expr
Def QName
x
KindOfName
FunName -> QName -> Expr
Def QName
x
KindOfName
OtherDefName -> QName -> Expr
Def QName
x
KindOfName
GeneralizeName -> QName -> Expr
Def QName
x
KindOfName
DisallowedGeneralizeName -> QName -> Expr
Def QName
x
KindOfName
FldName -> ProjOrigin -> AmbiguousQName -> Expr
Proj ProjOrigin
ProjSystem AmbiguousQName
ux
KindOfName
ConName -> AmbiguousQName -> Expr
Con AmbiguousQName
ux
KindOfName
CoConName -> AmbiguousQName -> Expr
Con AmbiguousQName
ux
KindOfName
PatternSynName -> AmbiguousQName -> Expr
PatternSyn AmbiguousQName
ux
KindOfName
MacroName -> QName -> Expr
Macro QName
x
KindOfName
QuotableName -> AppInfo -> Expr -> NamedArg Expr -> Expr
App (Range -> AppInfo
defaultAppInfo Range
r) (ExprInfo -> Expr
Quote ExprInfo
i) (forall a. a -> NamedArg a
defaultNamedArg forall a b. (a -> b) -> a -> b
$ QName -> Expr
Def QName
x)
where
x :: QName
x = AbstractName -> QName
anameName AbstractName
d
ux :: AmbiguousQName
ux = QName -> AmbiguousQName
unambiguous QName
x
r :: Range
r = forall a. HasRange a => a -> Range
getRange QName
x
i :: ExprInfo
i = Range -> ExprInfo
ExprRange Range
r
instance NameToExpr ResolvedName where
nameToExpr :: ResolvedName -> Expr
nameToExpr = \case
VarName Name
x BindingSource
_ -> Name -> Expr
Var Name
x
DefinedName Access
_ AbstractName
x Suffix
s -> Suffix -> Expr -> Expr
withSuffix Suffix
s forall a b. (a -> b) -> a -> b
$ forall a. NameToExpr a => a -> Expr
nameToExpr AbstractName
x
FieldName List1 AbstractName
xs -> ProjOrigin -> AmbiguousQName -> Expr
Proj ProjOrigin
ProjSystem forall b c a. (b -> c) -> (a -> b) -> a -> c
. NonEmpty QName -> AmbiguousQName
AmbQ forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap AbstractName -> QName
anameName forall a b. (a -> b) -> a -> b
$ List1 AbstractName
xs
ConstructorName Set Induction
_ List1 AbstractName
xs -> AmbiguousQName -> Expr
Con forall b c a. (b -> c) -> (a -> b) -> a -> c
. NonEmpty QName -> AmbiguousQName
AmbQ forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap AbstractName -> QName
anameName forall a b. (a -> b) -> a -> b
$ List1 AbstractName
xs
PatternSynResName List1 AbstractName
xs -> AmbiguousQName -> Expr
PatternSyn forall b c a. (b -> c) -> (a -> b) -> a -> c
. NonEmpty QName -> AmbiguousQName
AmbQ forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap AbstractName -> QName
anameName forall a b. (a -> b) -> a -> b
$ List1 AbstractName
xs
ResolvedName
UnknownName -> forall a. HasCallStack => a
__IMPOSSIBLE__
where
withSuffix :: Suffix -> Expr -> Expr
withSuffix Suffix
NoSuffix Expr
e = Expr
e
withSuffix s :: Suffix
s@Suffix{} (Def QName
x) = QName -> Suffix -> Expr
Def' QName
x Suffix
s
withSuffix Suffix
_ Expr
_ = forall a. HasCallStack => a
__IMPOSSIBLE__
app :: Expr -> [NamedArg Expr] -> Expr
app :: Expr -> [NamedArg Expr] -> Expr
app = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (AppInfo -> Expr -> NamedArg Expr -> Expr
App AppInfo
defaultAppInfo_)
mkLet :: ExprInfo -> [LetBinding] -> Expr -> Expr
mkLet :: ExprInfo -> [LetBinding] -> Expr -> Expr
mkLet ExprInfo
_ [] Expr
e = Expr
e
mkLet ExprInfo
i (LetBinding
d:[LetBinding]
ds) Expr
e = ExprInfo -> List1 LetBinding -> Expr -> Expr
Let ExprInfo
i (LetBinding
d forall a. a -> [a] -> NonEmpty a
:| [LetBinding]
ds) Expr
e
patternToExpr :: Pattern -> Expr
patternToExpr :: Pattern -> Expr
patternToExpr = \case
VarP BindName
x -> Name -> Expr
Var (BindName -> Name
unBind BindName
x)
ConP ConPatInfo
_ AmbiguousQName
c [NamedArg Pattern]
ps -> AmbiguousQName -> Expr
Con AmbiguousQName
c Expr -> [NamedArg Expr] -> Expr
`app` forall a b. (a -> b) -> [a] -> [b]
map (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Pattern -> Expr
patternToExpr)) [NamedArg Pattern]
ps
ProjP PatInfo
_ ProjOrigin
o AmbiguousQName
ds -> ProjOrigin -> AmbiguousQName -> Expr
Proj ProjOrigin
o AmbiguousQName
ds
DefP PatInfo
_ AmbiguousQName
fs [NamedArg Pattern]
ps -> QName -> Expr
Def (AmbiguousQName -> QName
headAmbQ AmbiguousQName
fs) Expr -> [NamedArg Expr] -> Expr
`app` forall a b. (a -> b) -> [a] -> [b]
map (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Pattern -> Expr
patternToExpr)) [NamedArg Pattern]
ps
WildP PatInfo
_ -> MetaInfo -> Expr
Underscore MetaInfo
emptyMetaInfo
AsP PatInfo
_ BindName
_ Pattern
p -> Pattern -> Expr
patternToExpr Pattern
p
DotP PatInfo
_ Expr
e -> Expr
e
AbsurdP PatInfo
_ -> MetaInfo -> Expr
Underscore MetaInfo
emptyMetaInfo
LitP (PatRange Range
r) Literal
l-> ExprInfo -> Literal -> Expr
Lit (Range -> ExprInfo
ExprRange Range
r) Literal
l
PatternSynP PatInfo
_ AmbiguousQName
c [NamedArg Pattern]
ps -> AmbiguousQName -> Expr
PatternSyn AmbiguousQName
c Expr -> [NamedArg Expr] -> Expr
`app` (forall a b. (a -> b) -> [a] -> [b]
map forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap) Pattern -> Expr
patternToExpr [NamedArg Pattern]
ps
RecP PatInfo
_ [FieldAssignment' Pattern]
as -> ExprInfo -> RecordAssigns -> Expr
Rec ExprInfo
exprNoRange forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (forall a b. a -> Either a b
Left forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Pattern -> Expr
patternToExpr) [FieldAssignment' Pattern]
as
EqualP{} -> forall a. HasCallStack => a
__IMPOSSIBLE__
WithP PatInfo
r Pattern
p -> forall a. HasCallStack => a
__IMPOSSIBLE__
AnnP PatInfo
_ Expr
_ Pattern
p -> Pattern -> Expr
patternToExpr Pattern
p
type PatternSynDefn = ([Arg Name], Pattern' Void)
type PatternSynDefns = Map QName PatternSynDefn
lambdaLiftExpr :: [Name] -> Expr -> Expr
lambdaLiftExpr :: [Name] -> Expr -> Expr
lambdaLiftExpr [Name]
ns Expr
e
= forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr
(\ Name
n -> ExprInfo -> LamBinding -> Expr -> Expr
Lam ExprInfo
exprNoRange (NamedArg Binder -> LamBinding
mkDomainFree forall a b. (a -> b) -> a -> b
$ forall a. a -> NamedArg a
defaultNamedArg forall a b. (a -> b) -> a -> b
$ Name -> Binder
mkBinder_ Name
n))
Expr
e
[Name]
ns
class SubstExpr a where
substExpr :: [(Name, Expr)] -> a -> a
default substExpr
:: (Functor t, SubstExpr b, t b ~ a)
=> [(Name, Expr)] -> a -> a
substExpr = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. SubstExpr a => [(Name, Expr)] -> a -> a
substExpr
instance SubstExpr a => SubstExpr (Maybe a)
instance SubstExpr a => SubstExpr [a]
instance SubstExpr a => SubstExpr (List1 a)
instance SubstExpr a => SubstExpr (Arg a)
instance SubstExpr a => SubstExpr (Named name a)
instance SubstExpr a => SubstExpr (FieldAssignment' a)
instance (SubstExpr a, SubstExpr b) => SubstExpr (a, b) where
substExpr :: [(Name, Expr)] -> (a, b) -> (a, b)
substExpr [(Name, Expr)]
s (a
x, b
y) = (forall a. SubstExpr a => [(Name, Expr)] -> a -> a
substExpr [(Name, Expr)]
s a
x, forall a. SubstExpr a => [(Name, Expr)] -> a -> a
substExpr [(Name, Expr)]
s b
y)
instance (SubstExpr a, SubstExpr b) => SubstExpr (Either a b) where
substExpr :: [(Name, Expr)] -> Either a b -> Either a b
substExpr [(Name, Expr)]
s (Left a
x) = forall a b. a -> Either a b
Left (forall a. SubstExpr a => [(Name, Expr)] -> a -> a
substExpr [(Name, Expr)]
s a
x)
substExpr [(Name, Expr)]
s (Right b
y) = forall a b. b -> Either a b
Right (forall a. SubstExpr a => [(Name, Expr)] -> a -> a
substExpr [(Name, Expr)]
s b
y)
instance SubstExpr C.Name where
substExpr :: [(Name, Expr)] -> Name -> Name
substExpr [(Name, Expr)]
_ = forall a. a -> a
id
instance SubstExpr ModuleName where
substExpr :: [(Name, Expr)] -> ModuleName -> ModuleName
substExpr [(Name, Expr)]
_ = forall a. a -> a
id
instance SubstExpr Expr where
substExpr :: [(Name, Expr)] -> Expr -> Expr
substExpr [(Name, Expr)]
s Expr
e = case Expr
e of
Var Name
n -> forall a. a -> Maybe a -> a
fromMaybe Expr
e (forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Name
n [(Name, Expr)]
s)
Con AmbiguousQName
_ -> Expr
e
Proj{} -> Expr
e
Def' QName
_ Suffix
_ -> Expr
e
PatternSyn{} -> Expr
e
Lit ExprInfo
_ Literal
_ -> Expr
e
Underscore MetaInfo
_ -> Expr
e
App AppInfo
i Expr
e NamedArg Expr
e' -> AppInfo -> Expr -> NamedArg Expr -> Expr
App AppInfo
i (forall a. SubstExpr a => [(Name, Expr)] -> a -> a
substExpr [(Name, Expr)]
s Expr
e) (forall a. SubstExpr a => [(Name, Expr)] -> a -> a
substExpr [(Name, Expr)]
s NamedArg Expr
e')
Rec ExprInfo
i RecordAssigns
nes -> ExprInfo -> RecordAssigns -> Expr
Rec ExprInfo
i (forall a. SubstExpr a => [(Name, Expr)] -> a -> a
substExpr [(Name, Expr)]
s RecordAssigns
nes)
ScopedExpr ScopeInfo
si Expr
e -> ScopeInfo -> Expr -> Expr
ScopedExpr ScopeInfo
si (forall a. SubstExpr a => [(Name, Expr)] -> a -> a
substExpr [(Name, Expr)]
s Expr
e)
QuestionMark{} -> forall a. HasCallStack => a
__IMPOSSIBLE__
Dot{} -> forall a. HasCallStack => a
__IMPOSSIBLE__
WithApp{} -> forall a. HasCallStack => a
__IMPOSSIBLE__
Lam{} -> forall a. HasCallStack => a
__IMPOSSIBLE__
AbsurdLam{} -> forall a. HasCallStack => a
__IMPOSSIBLE__
ExtendedLam{} -> forall a. HasCallStack => a
__IMPOSSIBLE__
Pi{} -> forall a. HasCallStack => a
__IMPOSSIBLE__
Generalized{} -> forall a. HasCallStack => a
__IMPOSSIBLE__
Fun{} -> forall a. HasCallStack => a
__IMPOSSIBLE__
Let{} -> forall a. HasCallStack => a
__IMPOSSIBLE__
RecUpdate{} -> forall a. HasCallStack => a
__IMPOSSIBLE__
Quote{} -> forall a. HasCallStack => a
__IMPOSSIBLE__
QuoteTerm{} -> forall a. HasCallStack => a
__IMPOSSIBLE__
Unquote{} -> forall a. HasCallStack => a
__IMPOSSIBLE__
DontCare{} -> forall a. HasCallStack => a
__IMPOSSIBLE__
Macro{} -> forall a. HasCallStack => a
__IMPOSSIBLE__
insertImplicitPatSynArgs
:: HasRange a
=> (Range -> a)
-> Range
-> [Arg Name]
-> [NamedArg a]
-> Maybe ([(Name, a)], [Arg Name])
insertImplicitPatSynArgs :: forall a.
HasRange a =>
(Range -> a)
-> Range
-> [Arg Name]
-> [NamedArg a]
-> Maybe ([(Name, a)], [Arg Name])
insertImplicitPatSynArgs Range -> a
wild Range
r [Arg Name]
ns [Arg (Named_ a)]
as = Range
-> [Arg Name]
-> [Arg (Named_ a)]
-> Maybe ([(Name, a)], [Arg Name])
matchArgs Range
r [Arg Name]
ns [Arg (Named_ a)]
as
where
matchNextArg :: Range
-> Arg Name -> [Arg (Named_ a)] -> Maybe (a, [Arg (Named_ a)])
matchNextArg Range
r Arg Name
n as :: [Arg (Named_ a)]
as@(~(Arg (Named_ a)
a : [Arg (Named_ a)]
as'))
| forall {a}.
(NameOf a ~ NamedName, LensHiding a, LensNamed a) =>
Arg Name -> [a] -> Bool
matchNext Arg Name
n [Arg (Named_ a)]
as = forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. NamedArg a -> a
namedArg Arg (Named_ a)
a, [Arg (Named_ a)]
as')
| forall a. LensHiding a => a -> Bool
visible Arg Name
n = forall a. Maybe a
Nothing
| Bool
otherwise = forall (m :: * -> *) a. Monad m => a -> m a
return (Range -> a
wild Range
r, [Arg (Named_ a)]
as)
matchNext :: Arg Name -> [a] -> Bool
matchNext Arg Name
_ [] = Bool
False
matchNext Arg Name
n (a
a:[a]
as) = forall a b. (LensHiding a, LensHiding b) => a -> b -> Bool
sameHiding Arg Name
n a
a Bool -> Bool -> Bool
&& forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
True (ArgName
x forall a. Eq a => a -> a -> Bool
==) (forall a. (LensNamed a, NameOf a ~ NamedName) => a -> Maybe ArgName
bareNameOf a
a)
where
x :: ArgName
x = Name -> ArgName
C.nameToRawName forall a b. (a -> b) -> a -> b
$ Name -> Name
nameConcrete forall a b. (a -> b) -> a -> b
$ forall e. Arg e -> e
unArg Arg Name
n
matchArgs :: Range
-> [Arg Name]
-> [Arg (Named_ a)]
-> Maybe ([(Name, a)], [Arg Name])
matchArgs Range
r [] [] = forall (m :: * -> *) a. Monad m => a -> m a
return ([], [])
matchArgs Range
r [] [Arg (Named_ a)]
as = forall a. Maybe a
Nothing
matchArgs Range
r (Arg Name
n:[Arg Name]
ns) [] | forall a. LensHiding a => a -> Bool
visible Arg Name
n = forall (m :: * -> *) a. Monad m => a -> m a
return ([], Arg Name
n forall a. a -> [a] -> [a]
: [Arg Name]
ns)
matchArgs Range
r (Arg Name
n:[Arg Name]
ns) [Arg (Named_ a)]
as = do
(a
p, [Arg (Named_ a)]
as) <- Range
-> Arg Name -> [Arg (Named_ a)] -> Maybe (a, [Arg (Named_ a)])
matchNextArg Range
r Arg Name
n [Arg (Named_ a)]
as
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first ((forall e. Arg e -> e
unArg Arg Name
n, a
p) forall a. a -> [a] -> [a]
:) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Range
-> [Arg Name]
-> [Arg (Named_ a)]
-> Maybe ([(Name, a)], [Arg Name])
matchArgs (forall a. HasRange a => a -> Range
getRange a
p) [Arg Name]
ns [Arg (Named_ a)]
as
data DeclarationSpine
= AxiomS
| GeneralizeS
| FieldS
| PrimitiveS
| MutualS [DeclarationSpine]
| SectionS [DeclarationSpine]
| ApplyS
| ImportS
| PragmaS
| OpenS
| FunDefS [ClauseSpine]
| DataSigS
| DataDefS
| RecSigS
| RecDefS [DeclarationSpine]
| PatternSynDefS
| UnquoteDeclS
| UnquoteDefS
| UnquoteDataS
| ScopedDeclS [DeclarationSpine]
| UnfoldingDeclS
deriving Int -> DeclarationSpine -> ShowS
[DeclarationSpine] -> ShowS
DeclarationSpine -> ArgName
forall a.
(Int -> a -> ShowS) -> (a -> ArgName) -> ([a] -> ShowS) -> Show a
showList :: [DeclarationSpine] -> ShowS
$cshowList :: [DeclarationSpine] -> ShowS
show :: DeclarationSpine -> ArgName
$cshow :: DeclarationSpine -> ArgName
showsPrec :: Int -> DeclarationSpine -> ShowS
$cshowsPrec :: Int -> DeclarationSpine -> ShowS
Show
data ClauseSpine = ClauseS RHSSpine WhereDeclarationsSpine
deriving Int -> ClauseSpine -> ShowS
[ClauseSpine] -> ShowS
ClauseSpine -> ArgName
forall a.
(Int -> a -> ShowS) -> (a -> ArgName) -> ([a] -> ShowS) -> Show a
showList :: [ClauseSpine] -> ShowS
$cshowList :: [ClauseSpine] -> ShowS
show :: ClauseSpine -> ArgName
$cshow :: ClauseSpine -> ArgName
showsPrec :: Int -> ClauseSpine -> ShowS
$cshowsPrec :: Int -> ClauseSpine -> ShowS
Show
data RHSSpine
= RHSS
| AbsurdRHSS
| WithRHSS (List1 ClauseSpine)
| RewriteRHSS RHSSpine WhereDeclarationsSpine
deriving Int -> RHSSpine -> ShowS
[RHSSpine] -> ShowS
RHSSpine -> ArgName
forall a.
(Int -> a -> ShowS) -> (a -> ArgName) -> ([a] -> ShowS) -> Show a
showList :: [RHSSpine] -> ShowS
$cshowList :: [RHSSpine] -> ShowS
show :: RHSSpine -> ArgName
$cshow :: RHSSpine -> ArgName
showsPrec :: Int -> RHSSpine -> ShowS
$cshowsPrec :: Int -> RHSSpine -> ShowS
Show
data WhereDeclarationsSpine = WhereDeclsS (Maybe DeclarationSpine)
deriving Int -> WhereDeclarationsSpine -> ShowS
[WhereDeclarationsSpine] -> ShowS
WhereDeclarationsSpine -> ArgName
forall a.
(Int -> a -> ShowS) -> (a -> ArgName) -> ([a] -> ShowS) -> Show a
showList :: [WhereDeclarationsSpine] -> ShowS
$cshowList :: [WhereDeclarationsSpine] -> ShowS
show :: WhereDeclarationsSpine -> ArgName
$cshow :: WhereDeclarationsSpine -> ArgName
showsPrec :: Int -> WhereDeclarationsSpine -> ShowS
$cshowsPrec :: Int -> WhereDeclarationsSpine -> ShowS
Show
declarationSpine :: Declaration -> DeclarationSpine
declarationSpine :: Declaration -> DeclarationSpine
declarationSpine = \case
Axiom KindOfName
_ DefInfo
_ ArgInfo
_ Maybe [Occurrence]
_ QName
_ Expr
_ -> DeclarationSpine
AxiomS
Generalize Set QName
_ DefInfo
_ ArgInfo
_ QName
_ Expr
_ -> DeclarationSpine
GeneralizeS
Field DefInfo
_ QName
_ Arg Expr
_ -> DeclarationSpine
FieldS
Primitive DefInfo
_ QName
_ Arg Expr
_ -> DeclarationSpine
PrimitiveS
Mutual MutualInfo
_ [Declaration]
ds -> [DeclarationSpine] -> DeclarationSpine
MutualS (forall a b. (a -> b) -> [a] -> [b]
map Declaration -> DeclarationSpine
declarationSpine [Declaration]
ds)
Section Range
_ Erased
_ ModuleName
_ GeneralizeTelescope
_ [Declaration]
ds -> [DeclarationSpine] -> DeclarationSpine
SectionS (forall a b. (a -> b) -> [a] -> [b]
map Declaration -> DeclarationSpine
declarationSpine [Declaration]
ds)
Apply ModuleInfo
_ Erased
_ ModuleName
_ ModuleApplication
_ ScopeCopyInfo
_ ImportDirective
_ -> DeclarationSpine
ApplyS
Import ModuleInfo
_ ModuleName
_ ImportDirective
_ -> DeclarationSpine
ImportS
Pragma Range
_ Pragma
_ -> DeclarationSpine
PragmaS
Open ModuleInfo
_ ModuleName
_ ImportDirective
_ -> DeclarationSpine
OpenS
FunDef DefInfo
_ QName
_ [Clause]
cs -> [ClauseSpine] -> DeclarationSpine
FunDefS (forall a b. (a -> b) -> [a] -> [b]
map Clause -> ClauseSpine
clauseSpine [Clause]
cs)
DataSig DefInfo
_ Erased
_ QName
_ GeneralizeTelescope
_ Expr
_ -> DeclarationSpine
DataSigS
DataDef DefInfo
_ QName
_ UniverseCheck
_ DataDefParams
_ [Declaration]
_ -> DeclarationSpine
DataDefS
RecSig DefInfo
_ Erased
_ QName
_ GeneralizeTelescope
_ Expr
_ -> DeclarationSpine
RecSigS
RecDef DefInfo
_ QName
_ UniverseCheck
_ RecordDirectives
_ DataDefParams
_ Expr
_ [Declaration]
ds -> [DeclarationSpine] -> DeclarationSpine
RecDefS (forall a b. (a -> b) -> [a] -> [b]
map Declaration -> DeclarationSpine
declarationSpine [Declaration]
ds)
PatternSynDef QName
_ [Arg BindName]
_ Pattern' Void
_ -> DeclarationSpine
PatternSynDefS
UnquoteDecl MutualInfo
_ [DefInfo]
_ [QName]
_ Expr
_ -> DeclarationSpine
UnquoteDeclS
UnquoteDef [DefInfo]
_ [QName]
_ Expr
_ -> DeclarationSpine
UnquoteDefS
UnquoteData [DefInfo]
_ QName
_ UniverseCheck
_ [DefInfo]
_ [QName]
_ Expr
_ -> DeclarationSpine
UnquoteDataS
ScopedDecl ScopeInfo
_ [Declaration]
ds -> [DeclarationSpine] -> DeclarationSpine
ScopedDeclS (forall a b. (a -> b) -> [a] -> [b]
map Declaration -> DeclarationSpine
declarationSpine [Declaration]
ds)
UnfoldingDecl Range
_ [QName]
_ -> DeclarationSpine
UnquoteDeclS
clauseSpine :: Clause -> ClauseSpine
clauseSpine :: Clause -> ClauseSpine
clauseSpine (Clause LHS
_ [ProblemEq]
_ RHS
rhs WhereDeclarations
ws Bool
_) =
RHSSpine -> WhereDeclarationsSpine -> ClauseSpine
ClauseS (RHS -> RHSSpine
rhsSpine RHS
rhs) (WhereDeclarations -> WhereDeclarationsSpine
whereDeclarationsSpine WhereDeclarations
ws)
rhsSpine :: RHS -> RHSSpine
rhsSpine :: RHS -> RHSSpine
rhsSpine = \case
RHS Expr
_ Maybe Expr
_ -> RHSSpine
RHSS
RHS
AbsurdRHS -> RHSSpine
AbsurdRHSS
WithRHS QName
_ [WithExpr]
_ List1 Clause
cs -> List1 ClauseSpine -> RHSSpine
WithRHSS forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Clause -> ClauseSpine
clauseSpine List1 Clause
cs
RewriteRHS [RewriteEqn]
_ [ProblemEq]
_ RHS
rhs WhereDeclarations
ws ->
RHSSpine -> WhereDeclarationsSpine -> RHSSpine
RewriteRHSS (RHS -> RHSSpine
rhsSpine RHS
rhs) (WhereDeclarations -> WhereDeclarationsSpine
whereDeclarationsSpine WhereDeclarations
ws)
whereDeclarationsSpine :: WhereDeclarations -> WhereDeclarationsSpine
whereDeclarationsSpine :: WhereDeclarations -> WhereDeclarationsSpine
whereDeclarationsSpine (WhereDecls Maybe ModuleName
_ Bool
_ Maybe Declaration
md) =
Maybe DeclarationSpine -> WhereDeclarationsSpine
WhereDeclsS (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Declaration -> DeclarationSpine
declarationSpine Maybe Declaration
md)