idris-1.3.4: Functional Programming Language with Dependent Types
LicenseBSD3
MaintainerThe Idris Community.
Safe HaskellSafe-Inferred
LanguageHaskell2010

Idris.Core.TT

Description

TT is the core language of Idris. The language has:

  • Full dependent types
  • A hierarchy of universes, with cumulativity: Type : Type1, Type1 : Type2, ...
  • Pattern matching letrec binding
  • (primitive types defined externally)

Some technical stuff:

  • Typechecker is kept as simple as possible - no unification, just a checker for incomplete terms.
  • We have a simple collection of tactics which we use to elaborate source programs with implicit syntax into fully explicit terms.
Synopsis

Documentation

data AppStatus n Source #

Constructors

Complete 
MaybeHoles 
Holes [n] 

Instances

Instances details
Functor AppStatus Source # 
Instance details

Defined in Idris.Core.TT

Methods

fmap :: (a -> b) -> AppStatus a -> AppStatus b

(<$) :: a -> AppStatus b -> AppStatus a

ToJSON t => ToJSON (AppStatus t) 
Instance details

Defined in IRTS.Portable

Methods

toJSON :: AppStatus t -> Value

toEncoding :: AppStatus t -> Encoding

toJSONList :: [AppStatus t] -> Value

toEncodingList :: [AppStatus t] -> Encoding

Data n => Data (AppStatus n) Source # 
Instance details

Defined in Idris.Core.TT

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> AppStatus n -> c (AppStatus n)

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (AppStatus n)

toConstr :: AppStatus n -> Constr

dataTypeOf :: AppStatus n -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (AppStatus n))

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (AppStatus n))

gmapT :: (forall b. Data b => b -> b) -> AppStatus n -> AppStatus n

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> AppStatus n -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> AppStatus n -> r

gmapQ :: (forall d. Data d => d -> u) -> AppStatus n -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> AppStatus n -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> AppStatus n -> m (AppStatus n)

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> AppStatus n -> m (AppStatus n)

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> AppStatus n -> m (AppStatus n)

Generic (AppStatus n) Source # 
Instance details

Defined in Idris.Core.TT

Associated Types

type Rep (AppStatus n) :: Type -> Type

Methods

from :: AppStatus n -> Rep (AppStatus n) x

to :: Rep (AppStatus n) x -> AppStatus n

Show n => Show (AppStatus n) Source # 
Instance details

Defined in Idris.Core.TT

Methods

showsPrec :: Int -> AppStatus n -> ShowS

show :: AppStatus n -> String

showList :: [AppStatus n] -> ShowS

NFData a => NFData (AppStatus a) 
Instance details

Defined in Idris.Core.DeepSeq

Methods

rnf :: AppStatus a -> ()

Eq n => Eq (AppStatus n) Source # 
Instance details

Defined in Idris.Core.TT

Methods

(==) :: AppStatus n -> AppStatus n -> Bool

(/=) :: AppStatus n -> AppStatus n -> Bool

Ord n => Ord (AppStatus n) Source # 
Instance details

Defined in Idris.Core.TT

Methods

compare :: AppStatus n -> AppStatus n -> Ordering

(<) :: AppStatus n -> AppStatus n -> Bool

(<=) :: AppStatus n -> AppStatus n -> Bool

(>) :: AppStatus n -> AppStatus n -> Bool

(>=) :: AppStatus n -> AppStatus n -> Bool

max :: AppStatus n -> AppStatus n -> AppStatus n

min :: AppStatus n -> AppStatus n -> AppStatus n

type Rep (AppStatus n) Source # 
Instance details

Defined in Idris.Core.TT

type Rep (AppStatus n) = D1 ('MetaData "AppStatus" "Idris.Core.TT" "idris-1.3.4-3WzTclJnDGuF9nqMis99Gw" 'False) (C1 ('MetaCons "Complete" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "MaybeHoles" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Holes" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [n]))))

data ArithTy Source #

Constructors

ATInt IntTy 
ATFloat 

Instances

Instances details
ToJSON ArithTy 
Instance details

Defined in IRTS.Portable

Methods

toJSON :: ArithTy -> Value

toEncoding :: ArithTy -> Encoding

toJSONList :: [ArithTy] -> Value

toEncodingList :: [ArithTy] -> Encoding

Data ArithTy Source # 
Instance details

Defined in Idris.Core.TT

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ArithTy -> c ArithTy

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ArithTy

toConstr :: ArithTy -> Constr

dataTypeOf :: ArithTy -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ArithTy)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ArithTy)

gmapT :: (forall b. Data b => b -> b) -> ArithTy -> ArithTy

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ArithTy -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ArithTy -> r

gmapQ :: (forall d. Data d => d -> u) -> ArithTy -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> ArithTy -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> ArithTy -> m ArithTy

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ArithTy -> m ArithTy

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ArithTy -> m ArithTy

Generic ArithTy Source # 
Instance details

Defined in Idris.Core.TT

Associated Types

type Rep ArithTy :: Type -> Type

Methods

from :: ArithTy -> Rep ArithTy x

to :: Rep ArithTy x -> ArithTy

Show ArithTy Source # 
Instance details

Defined in Idris.Core.TT

Methods

showsPrec :: Int -> ArithTy -> ShowS

show :: ArithTy -> String

showList :: [ArithTy] -> ShowS

NFData ArithTy 
Instance details

Defined in Idris.Core.DeepSeq

Methods

rnf :: ArithTy -> ()

Eq ArithTy Source # 
Instance details

Defined in Idris.Core.TT

Methods

(==) :: ArithTy -> ArithTy -> Bool

(/=) :: ArithTy -> ArithTy -> Bool

Ord ArithTy Source # 
Instance details

Defined in Idris.Core.TT

Methods

compare :: ArithTy -> ArithTy -> Ordering

(<) :: ArithTy -> ArithTy -> Bool

(<=) :: ArithTy -> ArithTy -> Bool

(>) :: ArithTy -> ArithTy -> Bool

(>=) :: ArithTy -> ArithTy -> Bool

max :: ArithTy -> ArithTy -> ArithTy

min :: ArithTy -> ArithTy -> ArithTy

type Rep ArithTy Source # 
Instance details

Defined in Idris.Core.TT

type Rep ArithTy = D1 ('MetaData "ArithTy" "Idris.Core.TT" "idris-1.3.4-3WzTclJnDGuF9nqMis99Gw" 'False) (C1 ('MetaCons "ATInt" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 IntTy)) :+: C1 ('MetaCons "ATFloat" 'PrefixI 'False) (U1 :: Type -> Type))

data Binder b Source #

All binding forms are represented in a uniform fashion. This type only represents the types of bindings (and their values, if any); the attached identifiers are part of the Bind constructor for the TT type.

Constructors

Lam 

Fields

Pi

A binding that occurs in a function type expression, e.g. (x:Int) -> ... The binderImpl flag says whether it was a scoped implicit (i.e. forall bound) in the high level Idris, but otherwise has no relevance in TT.

Fields

Let 

Fields

NLet

NLet is an intermediate product in the evaluator that's used for temporarily naming locals during reduction. It won't occur outside the evaluator.

Fields

  • binderTy :: !b

    type annotation for bound variable

  • binderVal :: b

    value for bound variable

Hole

A hole in a term under construction in the elaborator. If this is not filled during elaboration, it is an error.

Fields

  • binderTy :: !b

    type annotation for bound variable

GHole

A saved TT hole that will later be converted to a top-level Idris metavariable applied to all elements of its local environment.

Fields

Guess

A provided value for a hole. It will later be substituted - the guess is to keep it computationally inert while working on other things if necessary.

Fields

  • binderTy :: !b

    type annotation for bound variable

  • binderVal :: b

    value for bound variable

PVar

A pattern variable (these are bound around terms that make up pattern-match clauses)

Fields

PVTy

The type of a pattern binding

Fields

  • binderTy :: !b

    type annotation for bound variable

Instances

Instances details
Foldable Binder Source # 
Instance details

Defined in Idris.Core.TT

Methods

fold :: Monoid m => Binder m -> m

foldMap :: Monoid m => (a -> m) -> Binder a -> m

foldMap' :: Monoid m => (a -> m) -> Binder a -> m

foldr :: (a -> b -> b) -> b -> Binder a -> b

foldr' :: (a -> b -> b) -> b -> Binder a -> b

foldl :: (b -> a -> b) -> b -> Binder a -> b

foldl' :: (b -> a -> b) -> b -> Binder a -> b

foldr1 :: (a -> a -> a) -> Binder a -> a

foldl1 :: (a -> a -> a) -> Binder a -> a

toList :: Binder a -> [a]

null :: Binder a -> Bool

length :: Binder a -> Int

elem :: Eq a => a -> Binder a -> Bool

maximum :: Ord a => Binder a -> a

minimum :: Ord a => Binder a -> a

sum :: Num a => Binder a -> a

product :: Num a => Binder a -> a

Traversable Binder Source # 
Instance details

Defined in Idris.Core.TT

Methods

traverse :: Applicative f => (a -> f b) -> Binder a -> f (Binder b)

sequenceA :: Applicative f => Binder (f a) -> f (Binder a)

mapM :: Monad m => (a -> m b) -> Binder a -> m (Binder b)

sequence :: Monad m => Binder (m a) -> m (Binder a)

Functor Binder Source # 
Instance details

Defined in Idris.Core.TT

Methods

fmap :: (a -> b) -> Binder a -> Binder b

(<$) :: a -> Binder b -> Binder a

ToJSON t => ToJSON (Binder t) 
Instance details

Defined in IRTS.Portable

Methods

toJSON :: Binder t -> Value

toEncoding :: Binder t -> Encoding

toJSONList :: [Binder t] -> Value

toEncodingList :: [Binder t] -> Encoding

Data b => Data (Binder b) Source # 
Instance details

Defined in Idris.Core.TT

Methods

gfoldl :: (forall d b0. Data d => c (d -> b0) -> d -> c b0) -> (forall g. g -> c g) -> Binder b -> c (Binder b)

gunfold :: (forall b0 r. Data b0 => c (b0 -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Binder b)

toConstr :: Binder b -> Constr

dataTypeOf :: Binder b -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Binder b))

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Binder b))

gmapT :: (forall b0. Data b0 => b0 -> b0) -> Binder b -> Binder b

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Binder b -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Binder b -> r

gmapQ :: (forall d. Data d => d -> u) -> Binder b -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Binder b -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Binder b -> m (Binder b)

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Binder b -> m (Binder b)

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Binder b -> m (Binder b)

Generic (Binder b) Source # 
Instance details

Defined in Idris.Core.TT

Associated Types

type Rep (Binder b) :: Type -> Type

Methods

from :: Binder b -> Rep (Binder b) x

to :: Rep (Binder b) x -> Binder b

Show b => Show (Binder b) Source # 
Instance details

Defined in Idris.Core.TT

Methods

showsPrec :: Int -> Binder b -> ShowS

show :: Binder b -> String

showList :: [Binder b] -> ShowS

Binary b => Binary (Binder b) 
Instance details

Defined in Idris.Core.Binary

Methods

put :: Binder b -> Put

get :: Get (Binder b)

putList :: [Binder b] -> Put

NFData b => NFData (Binder b) 
Instance details

Defined in Idris.Core.DeepSeq

Methods

rnf :: Binder b -> ()

Eq b => Eq (Binder b) Source # 
Instance details

Defined in Idris.Core.TT

Methods

(==) :: Binder b -> Binder b -> Bool

(/=) :: Binder b -> Binder b -> Bool

Ord b => Ord (Binder b) Source # 
Instance details

Defined in Idris.Core.TT

Methods

compare :: Binder b -> Binder b -> Ordering

(<) :: Binder b -> Binder b -> Bool

(<=) :: Binder b -> Binder b -> Bool

(>) :: Binder b -> Binder b -> Bool

(>=) :: Binder b -> Binder b -> Bool

max :: Binder b -> Binder b -> Binder b

min :: Binder b -> Binder b -> Binder b

type Rep (Binder b) Source # 
Instance details

Defined in Idris.Core.TT

type Rep (Binder b) = D1 ('MetaData "Binder" "Idris.Core.TT" "idris-1.3.4-3WzTclJnDGuF9nqMis99Gw" 'False) (((C1 ('MetaCons "Lam" 'PrefixI 'True) (S1 ('MetaSel ('Just "binderCount") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 RigCount) :*: S1 ('MetaSel ('Just "binderTy") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 b)) :+: C1 ('MetaCons "Pi" 'PrefixI 'True) ((S1 ('MetaSel ('Just "binderCount") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 RigCount) :*: S1 ('MetaSel ('Just "binderImpl") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe ImplicitInfo))) :*: (S1 ('MetaSel ('Just "binderTy") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 b) :*: S1 ('MetaSel ('Just "binderKind") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 b)))) :+: (C1 ('MetaCons "Let" 'PrefixI 'True) (S1 ('MetaSel ('Just "binderCount") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 RigCount) :*: (S1 ('MetaSel ('Just "binderTy") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 b) :*: S1 ('MetaSel ('Just "binderVal") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 b))) :+: C1 ('MetaCons "NLet" 'PrefixI 'True) (S1 ('MetaSel ('Just "binderTy") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 b) :*: S1 ('MetaSel ('Just "binderVal") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 b)))) :+: ((C1 ('MetaCons "Hole" 'PrefixI 'True) (S1 ('MetaSel ('Just "binderTy") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 b)) :+: C1 ('MetaCons "GHole" 'PrefixI 'True) (S1 ('MetaSel ('Just "envlen") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int) :*: (S1 ('MetaSel ('Just "localnames") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Name]) :*: S1 ('MetaSel ('Just "binderTy") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 b)))) :+: (C1 ('MetaCons "Guess" 'PrefixI 'True) (S1 ('MetaSel ('Just "binderTy") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 b) :*: S1 ('MetaSel ('Just "binderVal") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 b)) :+: (C1 ('MetaCons "PVar" 'PrefixI 'True) (S1 ('MetaSel ('Just "binderCount") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 RigCount) :*: S1 ('MetaSel ('Just "binderTy") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 b)) :+: C1 ('MetaCons "PVTy" 'PrefixI 'True) (S1 ('MetaSel ('Just "binderTy") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 b))))))

data Const Source #

Constructors

I Int 
BI Integer 
Fl Double 
Ch Char 
Str String 
B8 Word8 
B16 Word16 
B32 Word32 
B64 Word64 
AType ArithTy 
StrType 
WorldType 
TheWorld 
VoidType 
Forgot 

Instances

Instances details
ToJSON Const 
Instance details

Defined in IRTS.Portable

Methods

toJSON :: Const -> Value

toEncoding :: Const -> Encoding

toJSONList :: [Const] -> Value

toEncodingList :: [Const] -> Encoding

Data Const Source # 
Instance details

Defined in Idris.Core.TT

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Const -> c Const

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Const

toConstr :: Const -> Constr

dataTypeOf :: Const -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Const)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Const)

gmapT :: (forall b. Data b => b -> b) -> Const -> Const

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Const -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Const -> r

gmapQ :: (forall d. Data d => d -> u) -> Const -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Const -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Const -> m Const

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Const -> m Const

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Const -> m Const

Generic Const Source # 
Instance details

Defined in Idris.Core.TT

Associated Types

type Rep Const :: Type -> Type

Methods

from :: Const -> Rep Const x

to :: Rep Const x -> Const

Show Const Source # 
Instance details

Defined in Idris.Core.TT

Methods

showsPrec :: Int -> Const -> ShowS

show :: Const -> String

showList :: [Const] -> ShowS

Binary Const 
Instance details

Defined in Idris.Core.Binary

Methods

put :: Const -> Put

get :: Get Const

putList :: [Const] -> Put

NFData Const 
Instance details

Defined in Idris.Core.DeepSeq

Methods

rnf :: Const -> ()

Eq Const Source # 
Instance details

Defined in Idris.Core.TT

Methods

(==) :: Const -> Const -> Bool

(/=) :: Const -> Const -> Bool

Ord Const Source # 
Instance details

Defined in Idris.Core.TT

Methods

compare :: Const -> Const -> Ordering

(<) :: Const -> Const -> Bool

(<=) :: Const -> Const -> Bool

(>) :: Const -> Const -> Bool

(>=) :: Const -> Const -> Bool

max :: Const -> Const -> Const

min :: Const -> Const -> Const

type Rep Const Source # 
Instance details

Defined in Idris.Core.TT

type Rep Const = D1 ('MetaData "Const" "Idris.Core.TT" "idris-1.3.4-3WzTclJnDGuF9nqMis99Gw" 'False) (((C1 ('MetaCons "I" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int)) :+: (C1 ('MetaCons "BI" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Integer)) :+: C1 ('MetaCons "Fl" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Double)))) :+: ((C1 ('MetaCons "Ch" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Char)) :+: C1 ('MetaCons "Str" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String))) :+: (C1 ('MetaCons "B8" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Word8)) :+: C1 ('MetaCons "B16" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Word16))))) :+: (((C1 ('MetaCons "B32" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Word32)) :+: C1 ('MetaCons "B64" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Word64))) :+: (C1 ('MetaCons "AType" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ArithTy)) :+: C1 ('MetaCons "StrType" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "WorldType" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "TheWorld" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "VoidType" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Forgot" 'PrefixI 'False) (U1 :: Type -> Type)))))

type Ctxt a = Map Name (Map Name a) Source #

Contexts allow us to map names to things. A root name maps to a collection of things in different namespaces with that name.

data ConstraintFC Source #

Constructors

ConstraintFC 

Fields

Instances

Instances details
Data ConstraintFC Source # 
Instance details

Defined in Idris.Core.TT

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ConstraintFC -> c ConstraintFC

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ConstraintFC

toConstr :: ConstraintFC -> Constr

dataTypeOf :: ConstraintFC -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ConstraintFC)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ConstraintFC)

gmapT :: (forall b. Data b => b -> b) -> ConstraintFC -> ConstraintFC

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ConstraintFC -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ConstraintFC -> r

gmapQ :: (forall d. Data d => d -> u) -> ConstraintFC -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> ConstraintFC -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> ConstraintFC -> m ConstraintFC

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ConstraintFC -> m ConstraintFC

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ConstraintFC -> m ConstraintFC

Generic ConstraintFC Source # 
Instance details

Defined in Idris.Core.TT

Associated Types

type Rep ConstraintFC :: Type -> Type

Show ConstraintFC Source # 
Instance details

Defined in Idris.Core.TT

Methods

showsPrec :: Int -> ConstraintFC -> ShowS

show :: ConstraintFC -> String

showList :: [ConstraintFC] -> ShowS

Binary ConstraintFC 
Instance details

Defined in Idris.Core.Binary

Methods

put :: ConstraintFC -> Put

get :: Get ConstraintFC

putList :: [ConstraintFC] -> Put

NFData ConstraintFC 
Instance details

Defined in Idris.Core.DeepSeq

Methods

rnf :: ConstraintFC -> ()

Eq ConstraintFC Source # 
Instance details

Defined in Idris.Core.TT

Methods

(==) :: ConstraintFC -> ConstraintFC -> Bool

(/=) :: ConstraintFC -> ConstraintFC -> Bool

Ord ConstraintFC Source # 
Instance details

Defined in Idris.Core.TT

type Rep ConstraintFC Source # 
Instance details

Defined in Idris.Core.TT

type Rep ConstraintFC = D1 ('MetaData "ConstraintFC" "Idris.Core.TT" "idris-1.3.4-3WzTclJnDGuF9nqMis99Gw" 'False) (C1 ('MetaCons "ConstraintFC" 'PrefixI 'True) (S1 ('MetaSel ('Just "uconstraint") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 UConstraint) :*: S1 ('MetaSel ('Just "ufc") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FC)))

data DataOpt Source #

Data declaration options

Constructors

Codata

Set if the the data-type is coinductive

DataErrRev 

Instances

Instances details
Generic DataOpt Source # 
Instance details

Defined in Idris.Core.TT

Associated Types

type Rep DataOpt :: Type -> Type

Methods

from :: DataOpt -> Rep DataOpt x

to :: Rep DataOpt x -> DataOpt

Show DataOpt Source # 
Instance details

Defined in Idris.Core.TT

Methods

showsPrec :: Int -> DataOpt -> ShowS

show :: DataOpt -> String

showList :: [DataOpt] -> ShowS

Binary DataOpt 
Instance details

Defined in Idris.IBC

Methods

put :: DataOpt -> Put

get :: Get DataOpt

putList :: [DataOpt] -> Put

NFData DataOpt 
Instance details

Defined in Idris.DeepSeq

Methods

rnf :: DataOpt -> ()

Eq DataOpt Source # 
Instance details

Defined in Idris.Core.TT

Methods

(==) :: DataOpt -> DataOpt -> Bool

(/=) :: DataOpt -> DataOpt -> Bool

type Rep DataOpt Source # 
Instance details

Defined in Idris.Core.TT

type Rep DataOpt = D1 ('MetaData "DataOpt" "Idris.Core.TT" "idris-1.3.4-3WzTclJnDGuF9nqMis99Gw" 'False) (C1 ('MetaCons "Codata" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "DataErrRev" 'PrefixI 'False) (U1 :: Type -> Type))

data Datatype n Source #

Constructors

Data 

Fields

Instances

Instances details
Functor Datatype Source # 
Instance details

Defined in Idris.Core.TT

Methods

fmap :: (a -> b) -> Datatype a -> Datatype b

(<$) :: a -> Datatype b -> Datatype a

(Show n, Eq n) => Show (Datatype n) Source # 
Instance details

Defined in Idris.Core.TT

Methods

showsPrec :: Int -> Datatype n -> ShowS

show :: Datatype n -> String

showList :: [Datatype n] -> ShowS

Eq n => Eq (Datatype n) Source # 
Instance details

Defined in Idris.Core.TT

Methods

(==) :: Datatype n -> Datatype n -> Bool

(/=) :: Datatype n -> Datatype n -> Bool

type EnvTT n = [(n, RigCount, Binder (TT n))] Source #

data Err' t Source #

Idris errors. Used as exceptions in the compiler, but reported to users if they reach the top level.

Constructors

Msg String 
InternalMsg String 
CantUnify Bool (t, Maybe Provenance) (t, Maybe Provenance) (Err' t) [(Name, t)] Int 
InfiniteUnify Name t [(Name, t)] 
CantConvert t t [(Name, t)] 
CantSolveGoal t [(Name, t)] 
UnifyScope Name Name t [(Name, t)] 
CantInferType String 
NonFunctionType t t 
NotEquality t t 
TooManyArguments Name 
CantIntroduce t 
NoSuchVariable Name 
WithFnType t 
NoTypeDecl Name 
NotInjective t t t 
CantResolve Bool t (Err' t) 
InvalidTCArg Name t 
CantResolveAlts [Name] 
NoValidAlts [Name] 
IncompleteTerm t 
UniverseError FC UExp (Int, Int) (Int, Int) [ConstraintFC]

Location, bad universe, old domain, new domain, suspects

UniqueError Universe Name 
UniqueKindError Universe Name 
ProgramLineComment 
Inaccessible Name 
UnknownImplicit Name Name 
CantMatch t 
NonCollapsiblePostulate Name 
AlreadyDefined Name 
ProofSearchFail (Err' t) 
NoRewriting t t t 
At FC (Err' t) 
Elaborating String Name (Maybe t) (Err' t) 
ElaboratingArg Name Name [(Name, Name)] (Err' t) 
ProviderError String 
LoadingFailed String (Err' t) 
ReflectionError [[ErrorReportPart]] (Err' t) 
ReflectionFailed String (Err' t) 
ElabScriptDebug [ErrorReportPart] t [(Name, t, [(Name, Binder t)])]

User-specified message, proof term, goals with context (first goal is focused)

ElabScriptStuck t 
RunningElabScript (Err' t)

The error occurred during a top-level elaboration script

ElabScriptStaging Name 
FancyMsg [ErrorReportPart] 

Instances

Instances details
Functor Err' Source # 
Instance details

Defined in Idris.Core.TT

Methods

fmap :: (a -> b) -> Err' a -> Err' b

(<$) :: a -> Err' b -> Err' a

Show Err Source # 
Instance details

Defined in Idris.Core.TT

Methods

showsPrec :: Int -> Err -> ShowS

show :: Err -> String

showList :: [Err] -> ShowS

NFData Err 
Instance details

Defined in Idris.Core.DeepSeq

Methods

rnf :: Err -> ()

Data t => Data (Err' t) Source # 
Instance details

Defined in Idris.Core.TT

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Err' t -> c (Err' t)

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Err' t)

toConstr :: Err' t -> Constr

dataTypeOf :: Err' t -> DataType

dataCast1 :: Typeable t0 => (forall d. Data d => c (t0 d)) -> Maybe (c (Err' t))

dataCast2 :: Typeable t0 => (forall d e. (Data d, Data e) => c (t0 d e)) -> Maybe (c (Err' t))

gmapT :: (forall b. Data b => b -> b) -> Err' t -> Err' t

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Err' t -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Err' t -> r

gmapQ :: (forall d. Data d => d -> u) -> Err' t -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Err' t -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Err' t -> m (Err' t)

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Err' t -> m (Err' t)

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Err' t -> m (Err' t)

Generic (Err' t) Source # 
Instance details

Defined in Idris.Core.TT

Associated Types

type Rep (Err' t) :: Type -> Type

Methods

from :: Err' t -> Rep (Err' t) x

to :: Rep (Err' t) x -> Err' t

Binary a => Binary (Err' a) 
Instance details

Defined in Idris.Core.Binary

Methods

put :: Err' a -> Put

get :: Get (Err' a)

putList :: [Err' a] -> Put

Eq t => Eq (Err' t) Source # 
Instance details

Defined in Idris.Core.TT

Methods

(==) :: Err' t -> Err' t -> Bool

(/=) :: Err' t -> Err' t -> Bool

Ord t => Ord (Err' t) Source # 
Instance details

Defined in Idris.Core.TT

Methods

compare :: Err' t -> Err' t -> Ordering

(<) :: Err' t -> Err' t -> Bool

(<=) :: Err' t -> Err' t -> Bool

(>) :: Err' t -> Err' t -> Bool

(>=) :: Err' t -> Err' t -> Bool

max :: Err' t -> Err' t -> Err' t

min :: Err' t -> Err' t -> Err' t

type Rep (Err' t) Source # 
Instance details

Defined in Idris.Core.TT

type Rep (Err' t) = D1 ('MetaData "Err'" "Idris.Core.TT" "idris-1.3.4-3WzTclJnDGuF9nqMis99Gw" 'False) (((((C1 ('MetaCons "Msg" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String)) :+: C1 ('MetaCons "InternalMsg" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String))) :+: (C1 ('MetaCons "CantUnify" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (t, Maybe Provenance)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (t, Maybe Provenance)))) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Err' t)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [(Name, t)]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int)))) :+: (C1 ('MetaCons "InfiniteUnify" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 t) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [(Name, t)]))) :+: C1 ('MetaCons "CantConvert" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 t) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 t) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [(Name, t)])))))) :+: ((C1 ('MetaCons "CantSolveGoal" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 t) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [(Name, t)])) :+: (C1 ('MetaCons "UnifyScope" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 t) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [(Name, t)]))) :+: C1 ('MetaCons "CantInferType" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String)))) :+: (C1 ('MetaCons "NonFunctionType" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 t) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 t)) :+: (C1 ('MetaCons "NotEquality" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 t) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 t)) :+: C1 ('MetaCons "TooManyArguments" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name)))))) :+: (((C1 ('MetaCons "CantIntroduce" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 t)) :+: C1 ('MetaCons "NoSuchVariable" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name))) :+: (C1 ('MetaCons "WithFnType" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 t)) :+: (C1 ('MetaCons "NoTypeDecl" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name)) :+: C1 ('MetaCons "NotInjective" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 t) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 t) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 t)))))) :+: ((C1 ('MetaCons "CantResolve" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 t) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Err' t)))) :+: (C1 ('MetaCons "InvalidTCArg" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 t)) :+: C1 ('MetaCons "CantResolveAlts" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Name])))) :+: (C1 ('MetaCons "NoValidAlts" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Name])) :+: (C1 ('MetaCons "IncompleteTerm" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 t)) :+: C1 ('MetaCons "UniverseError" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FC) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 UExp)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Int, Int)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Int, Int)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [ConstraintFC]))))))))) :+: ((((C1 ('MetaCons "UniqueError" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Universe) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name)) :+: C1 ('MetaCons "UniqueKindError" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Universe) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name))) :+: (C1 ('MetaCons "ProgramLineComment" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "Inaccessible" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name)) :+: C1 ('MetaCons "UnknownImplicit" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name))))) :+: ((C1 ('MetaCons "CantMatch" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 t)) :+: (C1 ('MetaCons "NonCollapsiblePostulate" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name)) :+: C1 ('MetaCons "AlreadyDefined" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name)))) :+: (C1 ('MetaCons "ProofSearchFail" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Err' t))) :+: (C1 ('MetaCons "NoRewriting" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 t) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 t) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 t))) :+: C1 ('MetaCons "At" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FC) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Err' t))))))) :+: (((C1 ('MetaCons "Elaborating" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe t)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Err' t)))) :+: C1 ('MetaCons "ElaboratingArg" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [(Name, Name)]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Err' t))))) :+: (C1 ('MetaCons "ProviderError" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String)) :+: (C1 ('MetaCons "LoadingFailed" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Err' t))) :+: C1 ('MetaCons "ReflectionError" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [[ErrorReportPart]]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Err' t)))))) :+: ((C1 ('MetaCons "ReflectionFailed" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Err' t))) :+: (C1 ('MetaCons "ElabScriptDebug" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [ErrorReportPart]) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 t) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [(Name, t, [(Name, Binder t)])]))) :+: C1 ('MetaCons "ElabScriptStuck" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 t)))) :+: (C1 ('MetaCons "RunningElabScript" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Err' t))) :+: (C1 ('MetaCons "ElabScriptStaging" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name)) :+: C1 ('MetaCons "FancyMsg" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [ErrorReportPart]))))))))

data ErrorReportPart Source #

Used for error reflection

Instances

Instances details
Data ErrorReportPart Source # 
Instance details

Defined in Idris.Core.TT

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ErrorReportPart -> c ErrorReportPart

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ErrorReportPart

toConstr :: ErrorReportPart -> Constr

dataTypeOf :: ErrorReportPart -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ErrorReportPart)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ErrorReportPart)

gmapT :: (forall b. Data b => b -> b) -> ErrorReportPart -> ErrorReportPart

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ErrorReportPart -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ErrorReportPart -> r

gmapQ :: (forall d. Data d => d -> u) -> ErrorReportPart -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> ErrorReportPart -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> ErrorReportPart -> m ErrorReportPart

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ErrorReportPart -> m ErrorReportPart

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ErrorReportPart -> m ErrorReportPart

Generic ErrorReportPart Source # 
Instance details

Defined in Idris.Core.TT

Associated Types

type Rep ErrorReportPart :: Type -> Type

Show ErrorReportPart Source # 
Instance details

Defined in Idris.Core.TT

Methods

showsPrec :: Int -> ErrorReportPart -> ShowS

show :: ErrorReportPart -> String

showList :: [ErrorReportPart] -> ShowS

Binary ErrorReportPart 
Instance details

Defined in Idris.Core.Binary

Methods

put :: ErrorReportPart -> Put

get :: Get ErrorReportPart

putList :: [ErrorReportPart] -> Put

NFData ErrorReportPart 
Instance details

Defined in Idris.Core.DeepSeq

Methods

rnf :: ErrorReportPart -> ()

Eq ErrorReportPart Source # 
Instance details

Defined in Idris.Core.TT

Ord ErrorReportPart Source # 
Instance details

Defined in Idris.Core.TT

type Rep ErrorReportPart Source # 
Instance details

Defined in Idris.Core.TT

type Rep ErrorReportPart = D1 ('MetaData "ErrorReportPart" "Idris.Core.TT" "idris-1.3.4-3WzTclJnDGuF9nqMis99Gw" 'False) ((C1 ('MetaCons "TextPart" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String)) :+: C1 ('MetaCons "NamePart" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name))) :+: (C1 ('MetaCons "TermPart" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Term)) :+: (C1 ('MetaCons "RawPart" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Raw)) :+: C1 ('MetaCons "SubReport" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [ErrorReportPart])))))

data FC Source #

Source location. These are typically produced by withExtent

Constructors

FC 

Fields

  • _fc_fname :: String

    Filename

  • _fc_start :: (Int, Int)

    Line and column numbers for the start of the location span

  • _fc_end :: (Int, Int)

    Line and column numbers for the end of the location span

NoFC

Locations for machine-generated terms

FileFC

Locations with file only

Fields

Instances

Instances details
Data FC Source # 
Instance details

Defined in Idris.Core.TT

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> FC -> c FC

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c FC

toConstr :: FC -> Constr

dataTypeOf :: FC -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c FC)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c FC)

gmapT :: (forall b. Data b => b -> b) -> FC -> FC

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> FC -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> FC -> r

gmapQ :: (forall d. Data d => d -> u) -> FC -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> FC -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> FC -> m FC

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> FC -> m FC

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> FC -> m FC

Monoid FC Source # 
Instance details

Defined in Idris.Core.TT

Methods

mempty :: FC

mappend :: FC -> FC -> FC

mconcat :: [FC] -> FC

Semigroup FC Source # 
Instance details

Defined in Idris.Core.TT

Methods

(<>) :: FC -> FC -> FC

sconcat :: NonEmpty FC -> FC

stimes :: Integral b => b -> FC -> FC

Generic FC Source # 
Instance details

Defined in Idris.Core.TT

Associated Types

type Rep FC :: Type -> Type

Methods

from :: FC -> Rep FC x

to :: Rep FC x -> FC

Show FC Source # 
Instance details

Defined in Idris.Core.TT

Methods

showsPrec :: Int -> FC -> ShowS

show :: FC -> String

showList :: [FC] -> ShowS

Binary FC 
Instance details

Defined in Idris.Core.Binary

Methods

put :: FC -> Put

get :: Get FC

putList :: [FC] -> Put

NFData FC 
Instance details

Defined in Idris.Core.DeepSeq

Methods

rnf :: FC -> ()

Eq FC Source #

Ignore source location equality (so deriving classes do not compare FCs)

Instance details

Defined in Idris.Core.TT

Methods

(==) :: FC -> FC -> Bool

(/=) :: FC -> FC -> Bool

Ord FC Source # 
Instance details

Defined in Idris.Core.TT

Methods

compare :: FC -> FC -> Ordering

(<) :: FC -> FC -> Bool

(<=) :: FC -> FC -> Bool

(>) :: FC -> FC -> Bool

(>=) :: FC -> FC -> Bool

max :: FC -> FC -> FC

min :: FC -> FC -> FC

SExpable FC Source # 
Instance details

Defined in Idris.IdeMode

Methods

toSExp :: FC -> SExp Source #

type Rep FC Source # 
Instance details

Defined in Idris.Core.TT

type Rep FC = D1 ('MetaData "FC" "Idris.Core.TT" "idris-1.3.4-3WzTclJnDGuF9nqMis99Gw" 'False) (C1 ('MetaCons "FC" 'PrefixI 'True) (S1 ('MetaSel ('Just "_fc_fname") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String) :*: (S1 ('MetaSel ('Just "_fc_start") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Int, Int)) :*: S1 ('MetaSel ('Just "_fc_end") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Int, Int)))) :+: (C1 ('MetaCons "NoFC" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "FileFC" 'PrefixI 'True) (S1 ('MetaSel ('Just "_fc_fname") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String))))

newtype FC' Source #

FC with equality

Constructors

FC' 

Fields

Instances

Instances details
Data FC' Source # 
Instance details

Defined in Idris.Core.TT

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> FC' -> c FC'

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c FC'

toConstr :: FC' -> Constr

dataTypeOf :: FC' -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c FC')

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c FC')

gmapT :: (forall b. Data b => b -> b) -> FC' -> FC'

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> FC' -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> FC' -> r

gmapQ :: (forall d. Data d => d -> u) -> FC' -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> FC' -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> FC' -> m FC'

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> FC' -> m FC'

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> FC' -> m FC'

Generic FC' Source # 
Instance details

Defined in Idris.Core.TT

Associated Types

type Rep FC' :: Type -> Type

Methods

from :: FC' -> Rep FC' x

to :: Rep FC' x -> FC'

Show FC' Source # 
Instance details

Defined in Idris.Core.TT

Methods

showsPrec :: Int -> FC' -> ShowS

show :: FC' -> String

showList :: [FC'] -> ShowS

Binary FC' 
Instance details

Defined in Idris.Core.Binary

Methods

put :: FC' -> Put

get :: Get FC'

putList :: [FC'] -> Put

NFData FC' 
Instance details

Defined in Idris.Core.DeepSeq

Methods

rnf :: FC' -> ()

Eq FC' Source # 
Instance details

Defined in Idris.Core.TT

Methods

(==) :: FC' -> FC' -> Bool

(/=) :: FC' -> FC' -> Bool

Ord FC' Source # 
Instance details

Defined in Idris.Core.TT

Methods

compare :: FC' -> FC' -> Ordering

(<) :: FC' -> FC' -> Bool

(<=) :: FC' -> FC' -> Bool

(>) :: FC' -> FC' -> Bool

(>=) :: FC' -> FC' -> Bool

max :: FC' -> FC' -> FC'

min :: FC' -> FC' -> FC'

type Rep FC' Source # 
Instance details

Defined in Idris.Core.TT

type Rep FC' = D1 ('MetaData "FC'" "Idris.Core.TT" "idris-1.3.4-3WzTclJnDGuF9nqMis99Gw" 'True) (C1 ('MetaCons "FC'" 'PrefixI 'True) (S1 ('MetaSel ('Just "unwrapFC") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FC)))

data ImplicitInfo Source #

Constructors

Impl 

Fields

Instances

Instances details
ToJSON ImplicitInfo 
Instance details

Defined in IRTS.Portable

Methods

toJSON :: ImplicitInfo -> Value

toEncoding :: ImplicitInfo -> Encoding

toJSONList :: [ImplicitInfo] -> Value

toEncodingList :: [ImplicitInfo] -> Encoding

Data ImplicitInfo Source # 
Instance details

Defined in Idris.Core.TT

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ImplicitInfo -> c ImplicitInfo

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ImplicitInfo

toConstr :: ImplicitInfo -> Constr

dataTypeOf :: ImplicitInfo -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ImplicitInfo)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ImplicitInfo)

gmapT :: (forall b. Data b => b -> b) -> ImplicitInfo -> ImplicitInfo

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ImplicitInfo -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ImplicitInfo -> r

gmapQ :: (forall d. Data d => d -> u) -> ImplicitInfo -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> ImplicitInfo -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> ImplicitInfo -> m ImplicitInfo

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ImplicitInfo -> m ImplicitInfo

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ImplicitInfo -> m ImplicitInfo

Generic ImplicitInfo Source # 
Instance details

Defined in Idris.Core.TT

Associated Types

type Rep ImplicitInfo :: Type -> Type

Show ImplicitInfo Source # 
Instance details

Defined in Idris.Core.TT

Methods

showsPrec :: Int -> ImplicitInfo -> ShowS

show :: ImplicitInfo -> String

showList :: [ImplicitInfo] -> ShowS

Binary ImplicitInfo 
Instance details

Defined in Idris.Core.Binary

Methods

put :: ImplicitInfo -> Put

get :: Get ImplicitInfo

putList :: [ImplicitInfo] -> Put

NFData ImplicitInfo 
Instance details

Defined in Idris.Core.DeepSeq

Methods

rnf :: ImplicitInfo -> ()

Eq ImplicitInfo Source # 
Instance details

Defined in Idris.Core.TT

Methods

(==) :: ImplicitInfo -> ImplicitInfo -> Bool

(/=) :: ImplicitInfo -> ImplicitInfo -> Bool

Ord ImplicitInfo Source # 
Instance details

Defined in Idris.Core.TT

type Rep ImplicitInfo Source # 
Instance details

Defined in Idris.Core.TT

type Rep ImplicitInfo = D1 ('MetaData "ImplicitInfo" "Idris.Core.TT" "idris-1.3.4-3WzTclJnDGuF9nqMis99Gw" 'False) (C1 ('MetaCons "Impl" 'PrefixI 'True) (S1 ('MetaSel ('Just "tcimplementation") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: (S1 ('MetaSel ('Just "toplevel_imp") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: S1 ('MetaSel ('Just "machine_gen") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool))))

data IntTy Source #

Instances

Instances details
ToJSON IntTy 
Instance details

Defined in IRTS.Portable

Methods

toJSON :: IntTy -> Value

toEncoding :: IntTy -> Encoding

toJSONList :: [IntTy] -> Value

toEncodingList :: [IntTy] -> Encoding

Data IntTy Source # 
Instance details

Defined in Idris.Core.TT

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> IntTy -> c IntTy

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c IntTy

toConstr :: IntTy -> Constr

dataTypeOf :: IntTy -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c IntTy)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c IntTy)

gmapT :: (forall b. Data b => b -> b) -> IntTy -> IntTy

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> IntTy -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> IntTy -> r

gmapQ :: (forall d. Data d => d -> u) -> IntTy -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> IntTy -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> IntTy -> m IntTy

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> IntTy -> m IntTy

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> IntTy -> m IntTy

Generic IntTy Source # 
Instance details

Defined in Idris.Core.TT

Associated Types

type Rep IntTy :: Type -> Type

Methods

from :: IntTy -> Rep IntTy x

to :: Rep IntTy x -> IntTy

Show IntTy Source # 
Instance details

Defined in Idris.Core.TT

Methods

showsPrec :: Int -> IntTy -> ShowS

show :: IntTy -> String

showList :: [IntTy] -> ShowS

NFData IntTy 
Instance details

Defined in Idris.Core.DeepSeq

Methods

rnf :: IntTy -> ()

Eq IntTy Source # 
Instance details

Defined in Idris.Core.TT

Methods

(==) :: IntTy -> IntTy -> Bool

(/=) :: IntTy -> IntTy -> Bool

Ord IntTy Source # 
Instance details

Defined in Idris.Core.TT

Methods

compare :: IntTy -> IntTy -> Ordering

(<) :: IntTy -> IntTy -> Bool

(<=) :: IntTy -> IntTy -> Bool

(>) :: IntTy -> IntTy -> Bool

(>=) :: IntTy -> IntTy -> Bool

max :: IntTy -> IntTy -> IntTy

min :: IntTy -> IntTy -> IntTy

type Rep IntTy Source # 
Instance details

Defined in Idris.Core.TT

type Rep IntTy = D1 ('MetaData "IntTy" "Idris.Core.TT" "idris-1.3.4-3WzTclJnDGuF9nqMis99Gw" 'False) ((C1 ('MetaCons "ITFixed" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 NativeTy)) :+: C1 ('MetaCons "ITNative" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "ITBig" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ITChar" 'PrefixI 'False) (U1 :: Type -> Type)))

data Name Source #

Names are hierarchies of strings, describing scope (so no danger of duplicate names, but need to be careful on lookup).

Constructors

UN !Text

User-provided name

NS !Name [Text]

Root, namespaces

MN !Int !Text

Machine chosen names

SN !SpecialName

Decorated function names

SymRef Int

Reference to IBC file symbol table (used during serialisation)

Instances

Instances details
ToJSON Name 
Instance details

Defined in IRTS.Portable

Methods

toJSON :: Name -> Value

toEncoding :: Name -> Encoding

toJSONList :: [Name] -> Value

toEncodingList :: [Name] -> Encoding

Data Name Source # 
Instance details

Defined in Idris.Core.TT

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Name -> c Name

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Name

toConstr :: Name -> Constr

dataTypeOf :: Name -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Name)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Name)

gmapT :: (forall b. Data b => b -> b) -> Name -> Name

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Name -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Name -> r

gmapQ :: (forall d. Data d => d -> u) -> Name -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Name -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Name -> m Name

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Name -> m Name

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Name -> m Name

Generic Name Source # 
Instance details

Defined in Idris.Core.TT

Associated Types

type Rep Name :: Type -> Type

Methods

from :: Name -> Rep Name x

to :: Rep Name x -> Name

Show Err Source # 
Instance details

Defined in Idris.Core.TT

Methods

showsPrec :: Int -> Err -> ShowS

show :: Err -> String

showList :: [Err] -> ShowS

Show Name Source # 
Instance details

Defined in Idris.Core.TT

Methods

showsPrec :: Int -> Name -> ShowS

show :: Name -> String

showList :: [Name] -> ShowS

Binary CaseAlt 
Instance details

Defined in Idris.IBC

Methods

put :: CaseAlt -> Put

get :: Get CaseAlt

putList :: [CaseAlt] -> Put

Binary SC 
Instance details

Defined in Idris.IBC

Methods

put :: SC -> Put

get :: Get SC

putList :: [SC] -> Put

Binary Name 
Instance details

Defined in Idris.Core.Binary

Methods

put :: Name -> Put

get :: Get Name

putList :: [Name] -> Put

NFData Err 
Instance details

Defined in Idris.Core.DeepSeq

Methods

rnf :: Err -> ()

NFData Name 
Instance details

Defined in Idris.Core.DeepSeq

Methods

rnf :: Name -> ()

Eq Name Source # 
Instance details

Defined in Idris.Core.TT

Methods

(==) :: Name -> Name -> Bool

(/=) :: Name -> Name -> Bool

Ord Name Source # 
Instance details

Defined in Idris.Core.TT

Methods

compare :: Name -> Name -> Ordering

(<) :: Name -> Name -> Bool

(<=) :: Name -> Name -> Bool

(>) :: Name -> Name -> Bool

(>=) :: Name -> Name -> Bool

max :: Name -> Name -> Name

min :: Name -> Name -> Name

TermSize CaseAlt Source # 
Instance details

Defined in Idris.Core.CaseTree

Methods

termsize :: Name -> CaseAlt -> Int Source #

TermSize SC Source # 
Instance details

Defined in Idris.Core.CaseTree

Methods

termsize :: Name -> SC -> Int Source #

SExpable Name Source # 
Instance details

Defined in Idris.IdeMode

Methods

toSExp :: Name -> SExp Source #

Binary (TT Name) 
Instance details

Defined in Idris.Core.Binary

Methods

put :: TT Name -> Put

get :: Get (TT Name)

putList :: [TT Name] -> Put

TermSize (TT Name) Source # 
Instance details

Defined in Idris.Core.TT

Methods

termsize :: Name -> TT Name -> Int Source #

type Rep Name Source # 
Instance details

Defined in Idris.Core.TT

type Rep Name = D1 ('MetaData "Name" "Idris.Core.TT" "idris-1.3.4-3WzTclJnDGuF9nqMis99Gw" 'False) ((C1 ('MetaCons "UN" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Text)) :+: C1 ('MetaCons "NS" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Name) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Text]))) :+: (C1 ('MetaCons "MN" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Int) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Text)) :+: (C1 ('MetaCons "SN" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 SpecialName)) :+: C1 ('MetaCons "SymRef" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int)))))

data NameOutput Source #

Output annotation for pretty-printed name - decides colour

Instances

Instances details
Generic NameOutput Source # 
Instance details

Defined in Idris.Core.TT

Associated Types

type Rep NameOutput :: Type -> Type

Methods

from :: NameOutput -> Rep NameOutput x

to :: Rep NameOutput x -> NameOutput

Show NameOutput Source # 
Instance details

Defined in Idris.Core.TT

Methods

showsPrec :: Int -> NameOutput -> ShowS

show :: NameOutput -> String

showList :: [NameOutput] -> ShowS

NFData NameOutput 
Instance details

Defined in Idris.Core.DeepSeq

Methods

rnf :: NameOutput -> ()

Eq NameOutput Source # 
Instance details

Defined in Idris.Core.TT

Methods

(==) :: NameOutput -> NameOutput -> Bool

(/=) :: NameOutput -> NameOutput -> Bool

Ord NameOutput Source # 
Instance details

Defined in Idris.Core.TT

SExpable NameOutput Source # 
Instance details

Defined in Idris.IdeMode

type Rep NameOutput Source # 
Instance details

Defined in Idris.Core.TT

type Rep NameOutput = D1 ('MetaData "NameOutput" "Idris.Core.TT" "idris-1.3.4-3WzTclJnDGuF9nqMis99Gw" 'False) ((C1 ('MetaCons "TypeOutput" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "FunOutput" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "DataOutput" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "MetavarOutput" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PostulateOutput" 'PrefixI 'False) (U1 :: Type -> Type))))

data NameType Source #

Constructors

Bound 
Ref 
DCon

Data constructor

Fields

TCon

Type constructor

Fields

Instances

Instances details
ToJSON NameType 
Instance details

Defined in IRTS.Portable

Methods

toJSON :: NameType -> Value

toEncoding :: NameType -> Encoding

toJSONList :: [NameType] -> Value

toEncodingList :: [NameType] -> Encoding

Data NameType Source # 
Instance details

Defined in Idris.Core.TT

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> NameType -> c NameType

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c NameType

toConstr :: NameType -> Constr

dataTypeOf :: NameType -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c NameType)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c NameType)

gmapT :: (forall b. Data b => b -> b) -> NameType -> NameType

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> NameType -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> NameType -> r

gmapQ :: (forall d. Data d => d -> u) -> NameType -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> NameType -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> NameType -> m NameType

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> NameType -> m NameType

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> NameType -> m NameType

Generic NameType Source # 
Instance details

Defined in Idris.Core.TT

Associated Types

type Rep NameType :: Type -> Type

Methods

from :: NameType -> Rep NameType x

to :: Rep NameType x -> NameType

Show NameType Source # 
Instance details

Defined in Idris.Core.TT

Methods

showsPrec :: Int -> NameType -> ShowS

show :: NameType -> String

showList :: [NameType] -> ShowS

Binary NameType 
Instance details

Defined in Idris.Core.Binary

Methods

put :: NameType -> Put

get :: Get NameType

putList :: [NameType] -> Put

NFData NameType 
Instance details

Defined in Idris.Core.DeepSeq

Methods

rnf :: NameType -> ()

Eq NameType Source # 
Instance details

Defined in Idris.Core.TT

Methods

(==) :: NameType -> NameType -> Bool

(/=) :: NameType -> NameType -> Bool

Ord NameType Source # 
Instance details

Defined in Idris.Core.TT

Methods

compare :: NameType -> NameType -> Ordering

(<) :: NameType -> NameType -> Bool

(<=) :: NameType -> NameType -> Bool

(>) :: NameType -> NameType -> Bool

(>=) :: NameType -> NameType -> Bool

max :: NameType -> NameType -> NameType

min :: NameType -> NameType -> NameType

type Rep NameType Source # 
Instance details

Defined in Idris.Core.TT

type Rep NameType = D1 ('MetaData "NameType" "Idris.Core.TT" "idris-1.3.4-3WzTclJnDGuF9nqMis99Gw" 'False) ((C1 ('MetaCons "Bound" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Ref" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "DCon" 'PrefixI 'True) (S1 ('MetaSel ('Just "nt_tag") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int) :*: (S1 ('MetaSel ('Just "nt_arity") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int) :*: S1 ('MetaSel ('Just "nt_unique") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool))) :+: C1 ('MetaCons "TCon" 'PrefixI 'True) (S1 ('MetaSel ('Just "nt_tag") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int) :*: S1 ('MetaSel ('Just "nt_arity") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int))))

data NativeTy Source #

Constructors

IT8 
IT16 
IT32 
IT64 

Instances

Instances details
Data NativeTy Source # 
Instance details

Defined in Idris.Core.TT

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> NativeTy -> c NativeTy

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c NativeTy

toConstr :: NativeTy -> Constr

dataTypeOf :: NativeTy -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c NativeTy)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c NativeTy)

gmapT :: (forall b. Data b => b -> b) -> NativeTy -> NativeTy

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> NativeTy -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> NativeTy -> r

gmapQ :: (forall d. Data d => d -> u) -> NativeTy -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> NativeTy -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> NativeTy -> m NativeTy

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> NativeTy -> m NativeTy

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> NativeTy -> m NativeTy

Enum NativeTy Source # 
Instance details

Defined in Idris.Core.TT

Generic NativeTy Source # 
Instance details

Defined in Idris.Core.TT

Associated Types

type Rep NativeTy :: Type -> Type

Methods

from :: NativeTy -> Rep NativeTy x

to :: Rep NativeTy x -> NativeTy

Show NativeTy Source # 
Instance details

Defined in Idris.Core.TT

Methods

showsPrec :: Int -> NativeTy -> ShowS

show :: NativeTy -> String

showList :: [NativeTy] -> ShowS

NFData NativeTy 
Instance details

Defined in Idris.Core.DeepSeq

Methods

rnf :: NativeTy -> ()

Eq NativeTy Source # 
Instance details

Defined in Idris.Core.TT

Methods

(==) :: NativeTy -> NativeTy -> Bool

(/=) :: NativeTy -> NativeTy -> Bool

Ord NativeTy Source # 
Instance details

Defined in Idris.Core.TT

Methods

compare :: NativeTy -> NativeTy -> Ordering

(<) :: NativeTy -> NativeTy -> Bool

(<=) :: NativeTy -> NativeTy -> Bool

(>) :: NativeTy -> NativeTy -> Bool

(>=) :: NativeTy -> NativeTy -> Bool

max :: NativeTy -> NativeTy -> NativeTy

min :: NativeTy -> NativeTy -> NativeTy

type Rep NativeTy Source # 
Instance details

Defined in Idris.Core.TT

type Rep NativeTy = D1 ('MetaData "NativeTy" "Idris.Core.TT" "idris-1.3.4-3WzTclJnDGuF9nqMis99Gw" 'False) ((C1 ('MetaCons "IT8" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "IT16" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "IT32" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "IT64" 'PrefixI 'False) (U1 :: Type -> Type)))

data OutputAnnotation Source #

Output annotations for pretty-printing

Constructors

AnnName Name (Maybe NameOutput) (Maybe String) (Maybe String)

^ The name, classification, docs overview, and pretty-printed type

AnnBoundName Name Bool

^ The name and whether it is implicit

AnnConst Const 
AnnData String String

type, doc overview

AnnType String String

name, doc overview

AnnKeyword 
AnnFC FC 
AnnTextFmt TextFormatting 
AnnLink String

A link to this URL

AnnTerm [(Name, Bool)] (TT Name)

pprint bound vars, original term

AnnSearchResult Ordering

more general, isomorphic, or more specific

AnnErr Err 
AnnNamespace [Text] (Maybe FilePath)

A namespace (e.g. on an import line or in a namespace declaration). Stored starting at the root, with the hierarchy fully resolved. If a file path is present, then the namespace represents a module imported from that file.

AnnQuasiquote 
AnnAntiquote 
AnnSyntax String

type of syntax element: backslash or braces etc.

Instances

Instances details
Generic OutputAnnotation Source # 
Instance details

Defined in Idris.Core.TT

Associated Types

type Rep OutputAnnotation :: Type -> Type

Show OutputAnnotation Source # 
Instance details

Defined in Idris.Core.TT

Methods

showsPrec :: Int -> OutputAnnotation -> ShowS

show :: OutputAnnotation -> String

showList :: [OutputAnnotation] -> ShowS

NFData OutputAnnotation 
Instance details

Defined in Idris.Core.DeepSeq

Methods

rnf :: OutputAnnotation -> ()

Eq OutputAnnotation Source # 
Instance details

Defined in Idris.Core.TT

Ord OutputAnnotation Source # 
Instance details

Defined in Idris.Core.TT

SExpable OutputAnnotation Source # 
Instance details

Defined in Idris.IdeMode

type Rep OutputAnnotation Source # 
Instance details

Defined in Idris.Core.TT

type Rep OutputAnnotation = D1 ('MetaData "OutputAnnotation" "Idris.Core.TT" "idris-1.3.4-3WzTclJnDGuF9nqMis99Gw" 'False) ((((C1 ('MetaCons "AnnName" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe NameOutput))) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe String)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe String)))) :+: C1 ('MetaCons "AnnBoundName" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool))) :+: (C1 ('MetaCons "AnnConst" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Const)) :+: C1 ('MetaCons "AnnData" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String)))) :+: ((C1 ('MetaCons "AnnType" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String)) :+: C1 ('MetaCons "AnnKeyword" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "AnnFC" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FC)) :+: C1 ('MetaCons "AnnTextFmt" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TextFormatting))))) :+: (((C1 ('MetaCons "AnnLink" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String)) :+: C1 ('MetaCons "AnnTerm" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [(Name, Bool)]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (TT Name)))) :+: (C1 ('MetaCons "AnnSearchResult" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Ordering)) :+: C1 ('MetaCons "AnnErr" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Err)))) :+: ((C1 ('MetaCons "AnnNamespace" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Text]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe FilePath))) :+: C1 ('MetaCons "AnnQuasiquote" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "AnnAntiquote" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "AnnSyntax" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String))))))

data Provenance Source #

Instances

Instances details
Data Provenance Source # 
Instance details

Defined in Idris.Core.TT

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Provenance -> c Provenance

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Provenance

toConstr :: Provenance -> Constr

dataTypeOf :: Provenance -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Provenance)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Provenance)

gmapT :: (forall b. Data b => b -> b) -> Provenance -> Provenance

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Provenance -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Provenance -> r

gmapQ :: (forall d. Data d => d -> u) -> Provenance -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Provenance -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Provenance -> m Provenance

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Provenance -> m Provenance

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Provenance -> m Provenance

Generic Provenance Source # 
Instance details

Defined in Idris.Core.TT

Associated Types

type Rep Provenance :: Type -> Type

Methods

from :: Provenance -> Rep Provenance x

to :: Rep Provenance x -> Provenance

Show Provenance Source # 
Instance details

Defined in Idris.Core.TT

Methods

showsPrec :: Int -> Provenance -> ShowS

show :: Provenance -> String

showList :: [Provenance] -> ShowS

Binary Provenance 
Instance details

Defined in Idris.Core.Binary

Methods

put :: Provenance -> Put

get :: Get Provenance

putList :: [Provenance] -> Put

NFData Provenance 
Instance details

Defined in Idris.Core.DeepSeq

Methods

rnf :: Provenance -> ()

Eq Provenance Source # 
Instance details

Defined in Idris.Core.TT

Methods

(==) :: Provenance -> Provenance -> Bool

(/=) :: Provenance -> Provenance -> Bool

Ord Provenance Source # 
Instance details

Defined in Idris.Core.TT

type Rep Provenance Source # 
Instance details

Defined in Idris.Core.TT

type Rep Provenance = D1 ('MetaData "Provenance" "Idris.Core.TT" "idris-1.3.4-3WzTclJnDGuF9nqMis99Gw" 'False) ((C1 ('MetaCons "ExpectedType" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "TooManyArgs" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Term))) :+: (C1 ('MetaCons "InferredVal" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "GivenVal" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "SourceTerm" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Term)))))

data Raw Source #

Instances

Instances details
Data Raw Source # 
Instance details

Defined in Idris.Core.TT

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Raw -> c Raw

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Raw

toConstr :: Raw -> Constr

dataTypeOf :: Raw -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Raw)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Raw)

gmapT :: (forall b. Data b => b -> b) -> Raw -> Raw

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Raw -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Raw -> r

gmapQ :: (forall d. Data d => d -> u) -> Raw -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Raw -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Raw -> m Raw

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Raw -> m Raw

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Raw -> m Raw

Generic Raw Source # 
Instance details

Defined in Idris.Core.TT

Associated Types

type Rep Raw :: Type -> Type

Methods

from :: Raw -> Rep Raw x

to :: Rep Raw x -> Raw

Show Raw Source # 
Instance details

Defined in Idris.Core.TT

Methods

showsPrec :: Int -> Raw -> ShowS

show :: Raw -> String

showList :: [Raw] -> ShowS

Binary Raw 
Instance details

Defined in Idris.Core.Binary

Methods

put :: Raw -> Put

get :: Get Raw

putList :: [Raw] -> Put

NFData Raw 
Instance details

Defined in Idris.Core.DeepSeq

Methods

rnf :: Raw -> ()

Eq Raw Source # 
Instance details

Defined in Idris.Core.TT

Methods

(==) :: Raw -> Raw -> Bool

(/=) :: Raw -> Raw -> Bool

Ord Raw Source # 
Instance details

Defined in Idris.Core.TT

Methods

compare :: Raw -> Raw -> Ordering

(<) :: Raw -> Raw -> Bool

(<=) :: Raw -> Raw -> Bool

(>) :: Raw -> Raw -> Bool

(>=) :: Raw -> Raw -> Bool

max :: Raw -> Raw -> Raw

min :: Raw -> Raw -> Raw

type Rep Raw Source # 
Instance details

Defined in Idris.Core.TT

type Rep Raw = D1 ('MetaData "Raw" "Idris.Core.TT" "idris-1.3.4-3WzTclJnDGuF9nqMis99Gw" 'False) ((C1 ('MetaCons "Var" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name)) :+: (C1 ('MetaCons "RBind" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Binder Raw)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Raw))) :+: C1 ('MetaCons "RApp" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Raw) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Raw)))) :+: (C1 ('MetaCons "RType" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "RUType" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Universe)) :+: C1 ('MetaCons "RConstant" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Const)))))

data RigCount Source #

Constructors

Rig0 
Rig1 
RigW 

Instances

Instances details
ToJSON RigCount 
Instance details

Defined in IRTS.Portable

Methods

toJSON :: RigCount -> Value

toEncoding :: RigCount -> Encoding

toJSONList :: [RigCount] -> Value

toEncodingList :: [RigCount] -> Encoding

Data RigCount Source # 
Instance details

Defined in Idris.Core.TT

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> RigCount -> c RigCount

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c RigCount

toConstr :: RigCount -> Constr

dataTypeOf :: RigCount -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c RigCount)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c RigCount)

gmapT :: (forall b. Data b => b -> b) -> RigCount -> RigCount

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> RigCount -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> RigCount -> r

gmapQ :: (forall d. Data d => d -> u) -> RigCount -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> RigCount -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> RigCount -> m RigCount

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> RigCount -> m RigCount

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> RigCount -> m RigCount

Generic RigCount Source # 
Instance details

Defined in Idris.Core.TT

Associated Types

type Rep RigCount :: Type -> Type

Methods

from :: RigCount -> Rep RigCount x

to :: Rep RigCount x -> RigCount

Show RigCount Source # 
Instance details

Defined in Idris.Core.TT

Methods

showsPrec :: Int -> RigCount -> ShowS

show :: RigCount -> String

showList :: [RigCount] -> ShowS

Binary RigCount 
Instance details

Defined in Idris.Core.Binary

Methods

put :: RigCount -> Put

get :: Get RigCount

putList :: [RigCount] -> Put

NFData RigCount 
Instance details

Defined in Idris.Core.DeepSeq

Methods

rnf :: RigCount -> ()

Eq RigCount Source # 
Instance details

Defined in Idris.Core.TT

Methods

(==) :: RigCount -> RigCount -> Bool

(/=) :: RigCount -> RigCount -> Bool

Ord RigCount Source # 
Instance details

Defined in Idris.Core.TT

Methods

compare :: RigCount -> RigCount -> Ordering

(<) :: RigCount -> RigCount -> Bool

(<=) :: RigCount -> RigCount -> Bool

(>) :: RigCount -> RigCount -> Bool

(>=) :: RigCount -> RigCount -> Bool

max :: RigCount -> RigCount -> RigCount

min :: RigCount -> RigCount -> RigCount

type Rep RigCount Source # 
Instance details

Defined in Idris.Core.TT

type Rep RigCount = D1 ('MetaData "RigCount" "Idris.Core.TT" "idris-1.3.4-3WzTclJnDGuF9nqMis99Gw" 'False) (C1 ('MetaCons "Rig0" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "Rig1" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "RigW" 'PrefixI 'False) (U1 :: Type -> Type)))

data SpecialName Source #

Instances

Instances details
Data SpecialName Source # 
Instance details

Defined in Idris.Core.TT

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> SpecialName -> c SpecialName

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c SpecialName

toConstr :: SpecialName -> Constr

dataTypeOf :: SpecialName -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c SpecialName)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SpecialName)

gmapT :: (forall b. Data b => b -> b) -> SpecialName -> SpecialName

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SpecialName -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SpecialName -> r

gmapQ :: (forall d. Data d => d -> u) -> SpecialName -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> SpecialName -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> SpecialName -> m SpecialName

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> SpecialName -> m SpecialName

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> SpecialName -> m SpecialName

Generic SpecialName Source # 
Instance details

Defined in Idris.Core.TT

Associated Types

type Rep SpecialName :: Type -> Type

Methods

from :: SpecialName -> Rep SpecialName x

to :: Rep SpecialName x -> SpecialName

Show SpecialName Source # 
Instance details

Defined in Idris.Core.TT

Methods

showsPrec :: Int -> SpecialName -> ShowS

show :: SpecialName -> String

showList :: [SpecialName] -> ShowS

Binary SpecialName 
Instance details

Defined in Idris.Core.Binary

Methods

put :: SpecialName -> Put

get :: Get SpecialName

putList :: [SpecialName] -> Put

NFData SpecialName 
Instance details

Defined in Idris.Core.DeepSeq

Methods

rnf :: SpecialName -> ()

Eq SpecialName Source # 
Instance details

Defined in Idris.Core.TT

Methods

(==) :: SpecialName -> SpecialName -> Bool

(/=) :: SpecialName -> SpecialName -> Bool

Ord SpecialName Source # 
Instance details

Defined in Idris.Core.TT

type Rep SpecialName Source # 
Instance details

Defined in Idris.Core.TT

type Rep SpecialName = D1 ('MetaData "SpecialName" "Idris.Core.TT" "idris-1.3.4-3WzTclJnDGuF9nqMis99Gw" 'False) (((C1 ('MetaCons "WhereN" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Int) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Name) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Name))) :+: C1 ('MetaCons "WithN" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Int) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Name))) :+: (C1 ('MetaCons "ImplementationN" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Name) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Text])) :+: C1 ('MetaCons "ParentN" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Name) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Text)))) :+: ((C1 ('MetaCons "MethodN" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Name)) :+: C1 ('MetaCons "CaseN" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 FC') :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Name))) :+: (C1 ('MetaCons "ImplementationCtorN" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Name)) :+: C1 ('MetaCons "MetaN" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Name) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Name)))))

data TC a Source #

Constructors

OK !a 
Error Err 

Instances

Instances details
MonadFail TC Source # 
Instance details

Defined in Idris.Core.TT

Methods

fail :: String -> TC a

Alternative TC Source # 
Instance details

Defined in Idris.Core.TT

Methods

empty :: TC a

(<|>) :: TC a -> TC a -> TC a

some :: TC a -> TC [a]

many :: TC a -> TC [a]

Applicative TC Source # 
Instance details

Defined in Idris.Core.TT

Methods

pure :: a -> TC a

(<*>) :: TC (a -> b) -> TC a -> TC b

liftA2 :: (a -> b -> c) -> TC a -> TC b -> TC c

(*>) :: TC a -> TC b -> TC b

(<*) :: TC a -> TC b -> TC a

Functor TC Source # 
Instance details

Defined in Idris.Core.TT

Methods

fmap :: (a -> b) -> TC a -> TC b

(<$) :: a -> TC b -> TC a

Monad TC Source # 
Instance details

Defined in Idris.Core.TT

Methods

(>>=) :: TC a -> (a -> TC b) -> TC b

(>>) :: TC a -> TC b -> TC b

return :: a -> TC a

MonadPlus TC Source # 
Instance details

Defined in Idris.Core.TT

Methods

mzero :: TC a

mplus :: TC a -> TC a -> TC a

Show a => Show (TC a) Source # 
Instance details

Defined in Idris.Core.TT

Methods

showsPrec :: Int -> TC a -> ShowS

show :: TC a -> String

showList :: [TC a] -> ShowS

Eq a => Eq (TC a) Source # 
Instance details

Defined in Idris.Core.TT

Methods

(==) :: TC a -> TC a -> Bool

(/=) :: TC a -> TC a -> Bool

class TermSize a where Source #

Methods

termsize :: Name -> a -> Int Source #

Instances

Instances details
TermSize CaseAlt Source # 
Instance details

Defined in Idris.Core.CaseTree

Methods

termsize :: Name -> CaseAlt -> Int Source #

TermSize SC Source # 
Instance details

Defined in Idris.Core.CaseTree

Methods

termsize :: Name -> SC -> Int Source #

TermSize (TT Name) Source # 
Instance details

Defined in Idris.Core.TT

Methods

termsize :: Name -> TT Name -> Int Source #

TermSize a => TermSize [a] Source # 
Instance details

Defined in Idris.Core.TT

Methods

termsize :: Name -> [a] -> Int Source #

data TextFormatting Source #

Text formatting output

Instances

Instances details
Generic TextFormatting Source # 
Instance details

Defined in Idris.Core.TT

Associated Types

type Rep TextFormatting :: Type -> Type

Show TextFormatting Source # 
Instance details

Defined in Idris.Core.TT

Methods

showsPrec :: Int -> TextFormatting -> ShowS

show :: TextFormatting -> String

showList :: [TextFormatting] -> ShowS

NFData TextFormatting 
Instance details

Defined in Idris.Core.DeepSeq

Methods

rnf :: TextFormatting -> ()

Eq TextFormatting Source # 
Instance details

Defined in Idris.Core.TT

Ord TextFormatting Source # 
Instance details

Defined in Idris.Core.TT

type Rep TextFormatting Source # 
Instance details

Defined in Idris.Core.TT

type Rep TextFormatting = D1 ('MetaData "TextFormatting" "Idris.Core.TT" "idris-1.3.4-3WzTclJnDGuF9nqMis99Gw" 'False) (C1 ('MetaCons "BoldText" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "ItalicText" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "UnderlineText" 'PrefixI 'False) (U1 :: Type -> Type)))

data TT n Source #

Terms in the core language. The type parameter is the type of identifiers used for bindings and explicit named references; usually we use TT Name.

Constructors

P NameType n (TT n)

named references with type (P for Parameter, motivated by McKinna and Pollack's Pure Type Systems Formalized)

V !Int

a resolved de Bruijn-indexed variable

Bind n !(Binder (TT n)) (TT n)

a binding

App (AppStatus n) !(TT n) (TT n)

function, function type, arg

Constant Const

constant

Proj (TT n) !Int

argument projection; runtime only (-1) is a special case for 'subtract one from BI'

Erased

an erased term

Impossible

special case for totality checking

Inferred (TT n)

For building case trees when coverage checkimg only. Marks a term as being inferred by the machine, rather than given by the programmer

TType UExp

the type of types at some level

UType Universe

Uniqueness type universe (disjoint from TType)

Instances

Instances details
Functor TT Source # 
Instance details

Defined in Idris.Core.TT

Methods

fmap :: (a -> b) -> TT a -> TT b

(<$) :: a -> TT b -> TT a

Show Err Source # 
Instance details

Defined in Idris.Core.TT

Methods

showsPrec :: Int -> Err -> ShowS

show :: Err -> String

showList :: [Err] -> ShowS

Binary CaseAlt 
Instance details

Defined in Idris.IBC

Methods

put :: CaseAlt -> Put

get :: Get CaseAlt

putList :: [CaseAlt] -> Put

Binary SC 
Instance details

Defined in Idris.IBC

Methods

put :: SC -> Put

get :: Get SC

putList :: [SC] -> Put

NFData Err 
Instance details

Defined in Idris.Core.DeepSeq

Methods

rnf :: Err -> ()

TermSize CaseAlt Source # 
Instance details

Defined in Idris.Core.CaseTree

Methods

termsize :: Name -> CaseAlt -> Int Source #

TermSize SC Source # 
Instance details

Defined in Idris.Core.CaseTree

Methods

termsize :: Name -> SC -> Int Source #

ToJSON t => ToJSON (TT t) 
Instance details

Defined in IRTS.Portable

Methods

toJSON :: TT t -> Value

toEncoding :: TT t -> Encoding

toJSONList :: [TT t] -> Value

toEncodingList :: [TT t] -> Encoding

Data n => Data (TT n) Source # 
Instance details

Defined in Idris.Core.TT

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> TT n -> c (TT n)

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (TT n)

toConstr :: TT n -> Constr

dataTypeOf :: TT n -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (TT n))

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (TT n))

gmapT :: (forall b. Data b => b -> b) -> TT n -> TT n

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TT n -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TT n -> r

gmapQ :: (forall d. Data d => d -> u) -> TT n -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> TT n -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> TT n -> m (TT n)

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TT n -> m (TT n)

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TT n -> m (TT n)

Generic (TT n) Source # 
Instance details

Defined in Idris.Core.TT

Associated Types

type Rep (TT n) :: Type -> Type

Methods

from :: TT n -> Rep (TT n) x

to :: Rep (TT n) x -> TT n

(Eq n, Show n) => Show (TT n) Source # 
Instance details

Defined in Idris.Core.TT

Methods

showsPrec :: Int -> TT n -> ShowS

show :: TT n -> String

showList :: [TT n] -> ShowS

Binary (TT Name) 
Instance details

Defined in Idris.Core.Binary

Methods

put :: TT Name -> Put

get :: Get (TT Name)

putList :: [TT Name] -> Put

NFData n => NFData (TT n) 
Instance details

Defined in Idris.Core.DeepSeq

Methods

rnf :: TT n -> ()

Eq n => Eq (TT n) Source # 
Instance details

Defined in Idris.Core.TT

Methods

(==) :: TT n -> TT n -> Bool

(/=) :: TT n -> TT n -> Bool

Ord n => Ord (TT n) Source # 
Instance details

Defined in Idris.Core.TT

Methods

compare :: TT n -> TT n -> Ordering

(<) :: TT n -> TT n -> Bool

(<=) :: TT n -> TT n -> Bool

(>) :: TT n -> TT n -> Bool

(>=) :: TT n -> TT n -> Bool

max :: TT n -> TT n -> TT n

min :: TT n -> TT n -> TT n

TermSize (TT Name) Source # 
Instance details

Defined in Idris.Core.TT

Methods

termsize :: Name -> TT Name -> Int Source #

type Rep (TT n) Source # 
Instance details

Defined in Idris.Core.TT

type Rep (TT n) = D1 ('MetaData "TT" "Idris.Core.TT" "idris-1.3.4-3WzTclJnDGuF9nqMis99Gw" 'False) (((C1 ('MetaCons "P" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 NameType) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 n) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (TT n)))) :+: C1 ('MetaCons "V" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Int))) :+: (C1 ('MetaCons "Bind" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 n) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (Binder (TT n))) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (TT n)))) :+: (C1 ('MetaCons "App" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (AppStatus n)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (TT n)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (TT n)))) :+: C1 ('MetaCons "Constant" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Const))))) :+: ((C1 ('MetaCons "Proj" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (TT n)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Int)) :+: (C1 ('MetaCons "Erased" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Impossible" 'PrefixI 'False) (U1 :: Type -> Type))) :+: (C1 ('MetaCons "Inferred" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (TT n))) :+: (C1 ('MetaCons "TType" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 UExp)) :+: C1 ('MetaCons "UType" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Universe))))))

type Type = Term Source #

data TypeInfo Source #

Constructors

TI 

Fields

Instances

Instances details
Generic TypeInfo Source # 
Instance details

Defined in Idris.Core.TT

Associated Types

type Rep TypeInfo :: Type -> Type

Methods

from :: TypeInfo -> Rep TypeInfo x

to :: Rep TypeInfo x -> TypeInfo

Show TypeInfo Source # 
Instance details

Defined in Idris.Core.TT

Methods

showsPrec :: Int -> TypeInfo -> ShowS

show :: TypeInfo -> String

showList :: [TypeInfo] -> ShowS

Binary TypeInfo 
Instance details

Defined in Idris.IBC

Methods

put :: TypeInfo -> Put

get :: Get TypeInfo

putList :: [TypeInfo] -> Put

NFData TypeInfo 
Instance details

Defined in Idris.DeepSeq

Methods

rnf :: TypeInfo -> ()

type Rep TypeInfo Source # 
Instance details

Defined in Idris.Core.TT

type Rep TypeInfo = D1 ('MetaData "TypeInfo" "Idris.Core.TT" "idris-1.3.4-3WzTclJnDGuF9nqMis99Gw" 'False) (C1 ('MetaCons "TI" 'PrefixI 'True) ((S1 ('MetaSel ('Just "con_names") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Name]) :*: (S1 ('MetaSel ('Just "codata") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: S1 ('MetaSel ('Just "data_opts") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DataOpts))) :*: (S1 ('MetaSel ('Just "param_pos") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Int]) :*: (S1 ('MetaSel ('Just "mutual_types") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Name]) :*: S1 ('MetaSel ('Just "linear_con") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)))))

data UConstraint Source #

Universe constraints

Constructors

ULT UExp UExp

Strictly less than

ULE UExp UExp

Less than or equal to

Instances

Instances details
Data UConstraint Source # 
Instance details

Defined in Idris.Core.TT

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> UConstraint -> c UConstraint

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c UConstraint

toConstr :: UConstraint -> Constr

dataTypeOf :: UConstraint -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c UConstraint)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c UConstraint)

gmapT :: (forall b. Data b => b -> b) -> UConstraint -> UConstraint

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> UConstraint -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> UConstraint -> r

gmapQ :: (forall d. Data d => d -> u) -> UConstraint -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> UConstraint -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> UConstraint -> m UConstraint

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> UConstraint -> m UConstraint

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> UConstraint -> m UConstraint

Generic UConstraint Source # 
Instance details

Defined in Idris.Core.TT

Associated Types

type Rep UConstraint :: Type -> Type

Methods

from :: UConstraint -> Rep UConstraint x

to :: Rep UConstraint x -> UConstraint

Show UConstraint Source # 
Instance details

Defined in Idris.Core.TT

Methods

showsPrec :: Int -> UConstraint -> ShowS

show :: UConstraint -> String

showList :: [UConstraint] -> ShowS

Binary UConstraint 
Instance details

Defined in Idris.Core.Binary

Methods

put :: UConstraint -> Put

get :: Get UConstraint

putList :: [UConstraint] -> Put

NFData UConstraint 
Instance details

Defined in Idris.Core.DeepSeq

Methods

rnf :: UConstraint -> ()

Eq UConstraint Source # 
Instance details

Defined in Idris.Core.TT

Methods

(==) :: UConstraint -> UConstraint -> Bool

(/=) :: UConstraint -> UConstraint -> Bool

Ord UConstraint Source # 
Instance details

Defined in Idris.Core.TT

type Rep UConstraint Source # 
Instance details

Defined in Idris.Core.TT

type Rep UConstraint = D1 ('MetaData "UConstraint" "Idris.Core.TT" "idris-1.3.4-3WzTclJnDGuF9nqMis99Gw" 'False) (C1 ('MetaCons "ULT" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 UExp) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 UExp)) :+: C1 ('MetaCons "ULE" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 UExp) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 UExp)))

type UCs = (Int, [UConstraint]) Source #

data UExp Source #

Universe expressions for universe checking

Constructors

UVar String Int

universe variable, with source file to disambiguate

UVal Int

explicit universe level

Instances

Instances details
ToJSON UExp 
Instance details

Defined in IRTS.Portable

Methods

toJSON :: UExp -> Value

toEncoding :: UExp -> Encoding

toJSONList :: [UExp] -> Value

toEncodingList :: [UExp] -> Encoding

Data UExp Source # 
Instance details

Defined in Idris.Core.TT

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> UExp -> c UExp

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c UExp

toConstr :: UExp -> Constr

dataTypeOf :: UExp -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c UExp)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c UExp)

gmapT :: (forall b. Data b => b -> b) -> UExp -> UExp

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> UExp -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> UExp -> r

gmapQ :: (forall d. Data d => d -> u) -> UExp -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> UExp -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> UExp -> m UExp

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> UExp -> m UExp

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> UExp -> m UExp

Generic UExp Source # 
Instance details

Defined in Idris.Core.TT

Associated Types

type Rep UExp :: Type -> Type

Methods

from :: UExp -> Rep UExp x

to :: Rep UExp x -> UExp

Show UExp Source # 
Instance details

Defined in Idris.Core.TT

Methods

showsPrec :: Int -> UExp -> ShowS

show :: UExp -> String

showList :: [UExp] -> ShowS

Binary UExp 
Instance details

Defined in Idris.Core.Binary

Methods

put :: UExp -> Put

get :: Get UExp

putList :: [UExp] -> Put

NFData UExp 
Instance details

Defined in Idris.Core.DeepSeq

Methods

rnf :: UExp -> ()

Eq UExp Source # 
Instance details

Defined in Idris.Core.TT

Methods

(==) :: UExp -> UExp -> Bool

(/=) :: UExp -> UExp -> Bool

Ord UExp Source # 
Instance details

Defined in Idris.Core.TT

Methods

compare :: UExp -> UExp -> Ordering

(<) :: UExp -> UExp -> Bool

(<=) :: UExp -> UExp -> Bool

(>) :: UExp -> UExp -> Bool

(>=) :: UExp -> UExp -> Bool

max :: UExp -> UExp -> UExp

min :: UExp -> UExp -> UExp

type Rep UExp Source # 
Instance details

Defined in Idris.Core.TT

type Rep UExp = D1 ('MetaData "UExp" "Idris.Core.TT" "idris-1.3.4-3WzTclJnDGuF9nqMis99Gw" 'False) (C1 ('MetaCons "UVar" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int)) :+: C1 ('MetaCons "UVal" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int)))

data Universe Source #

Constructors

NullType 
UniqueType 
AllTypes 

Instances

Instances details
Data Universe Source # 
Instance details

Defined in Idris.Core.TT

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Universe -> c Universe

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Universe

toConstr :: Universe -> Constr

dataTypeOf :: Universe -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Universe)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Universe)

gmapT :: (forall b. Data b => b -> b) -> Universe -> Universe

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Universe -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Universe -> r

gmapQ :: (forall d. Data d => d -> u) -> Universe -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Universe -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Universe -> m Universe

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Universe -> m Universe

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Universe -> m Universe

Generic Universe Source # 
Instance details

Defined in Idris.Core.TT

Associated Types

type Rep Universe :: Type -> Type

Methods

from :: Universe -> Rep Universe x

to :: Rep Universe x -> Universe

Show Universe Source # 
Instance details

Defined in Idris.Core.TT

Methods

showsPrec :: Int -> Universe -> ShowS

show :: Universe -> String

showList :: [Universe] -> ShowS

Binary Universe 
Instance details

Defined in Idris.Core.Binary

Methods

put :: Universe -> Put

get :: Get Universe

putList :: [Universe] -> Put

NFData Universe 
Instance details

Defined in Idris.Core.DeepSeq

Methods

rnf :: Universe -> ()

Eq Universe Source # 
Instance details

Defined in Idris.Core.TT

Methods

(==) :: Universe -> Universe -> Bool

(/=) :: Universe -> Universe -> Bool

Ord Universe Source # 
Instance details

Defined in Idris.Core.TT

Methods

compare :: Universe -> Universe -> Ordering

(<) :: Universe -> Universe -> Bool

(<=) :: Universe -> Universe -> Bool

(>) :: Universe -> Universe -> Bool

(>=) :: Universe -> Universe -> Bool

max :: Universe -> Universe -> Universe

min :: Universe -> Universe -> Universe

type Rep Universe Source # 
Instance details

Defined in Idris.Core.TT

type Rep Universe = D1 ('MetaData "Universe" "Idris.Core.TT" "idris-1.3.4-3WzTclJnDGuF9nqMis99Gw" 'False) (C1 ('MetaCons "NullType" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "UniqueType" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "AllTypes" 'PrefixI 'False) (U1 :: Type -> Type)))

addAlist :: [(Name, a)] -> Ctxt a -> Ctxt a Source #

addBinder :: TT n -> TT n Source #

addDef :: Name -> a -> Ctxt a -> Ctxt a Source #

allTTNames :: Eq n => TT n -> [n] Source #

arity :: TT n -> Int Source #

Return the arity of a (normalised) type

bindAll :: [(n, Binder (TT n))] -> TT n -> TT n Source #

Introduce a Bind into the given term for each element of the given list of (name, binder) pairs.

bindingOf Source #

Arguments

:: Name

^ the bound name

-> Bool

^ whether the name is implicit

-> Doc OutputAnnotation 

Pretty-printer helper for the binding site of a name

bindTyArgs :: (TT n -> Binder (TT n)) -> [(n, TT n)] -> TT n -> TT n Source #

Like bindAll, but the Binders are TT terms instead. The first argument is a function to map TT terms to Binders. This function might often be something like Lam, which directly constructs a Binder from a TT term.

caseName :: Name -> Bool Source #

constDocs :: Const -> String Source #

Get the docstring for a Const

constIsType :: Const -> Bool Source #

Determines whether the input constant represents a type

discard :: Monad m => m a -> m () Source #

emptyContext :: Map k a Source #

emptyFC :: FC Source #

Empty source location

explicitNames :: TT n -> TT n Source #

Replace all non-free de Bruijn references in the given term with references to the name of their binding.

fc_end :: FC -> (Int, Int) Source #

Give a notion of end location associated with an FC

fc_fname :: FC -> String Source #

Give a notion of filename associated with an FC

fc_start :: FC -> (Int, Int) Source #

Give a notion of start location associated with an FC

fcIn :: FC -> FC -> Bool Source #

Determine whether the first argument is completely contained in the second

fileFC :: String -> FC Source #

Source location with file only

finalise :: Eq n => TT n -> TT n Source #

Replace every non-free reference to the name of a binding in the given term with a de Bruijn index.

fmapMB :: Monad m => (a -> m b) -> Binder a -> m (Binder b) Source #

forget :: TT Name -> Raw Source #

Cast a TT term to a Raw value, discarding universe information and the types of named references and replacing all de Bruijn indices with the corresponding name. It is an error if there are free de Bruijn indices.

freeNames :: Eq n => TT n -> [n] Source #

Returns all names used free in the term

getArgTys :: TT n -> [(n, TT n)] Source #

Return a list of pairs of the names of the outermost Pi-bound variables in the given term, together with their types.

getRetTy :: TT n -> TT n Source #

substRetTy :: TT n -> TT n Source #

As getRetTy but substitutes names for de Bruijn indices

instantiate :: TT n -> TT n -> TT n Source #

Replace the outermost (index 0) de Bruijn variable with the given term

internalNS :: String Source #

intTyName :: IntTy -> String Source #

isInjective :: TT n -> Bool Source #

A term is injective iff it is a data constructor, type constructor, constant, the type Type, pi-binding, or an application of an injective term.

lookupCtxt :: Name -> Ctxt a -> [a] Source #

lookupCtxtExact :: Name -> Ctxt a -> Maybe a Source #

lookupCtxtName :: Name -> Ctxt a -> [(Name, a)] Source #

Look up a name in the context, given an optional namespace. The name (n) may itself have a (partial) namespace given.

Rules for resolution:

  • if an explicit namespace is given, return the names which match it. If none match, return all names.
  • if the name has has explicit namespace given, return the names which match it and ignore the given namespace.
  • otherwise, return all names.

mapCtxt :: (a -> b) -> Ctxt a -> Ctxt b Source #

mkApp :: TT n -> [TT n] -> TT n Source #

Returns a term representing the application of the first argument (a function) to every element of the second argument.

noOccurrence :: Eq n => n -> TT n -> Bool Source #

Returns true if V 0 and bound name n do not occur in the term

occurrences :: Eq n => n -> TT n -> Int Source #

Return number of occurrences of V 0 or bound name i the term

pEraseType :: TT n -> TT n Source #

pmap :: (t -> b) -> (t, t) -> (b, b) Source #

pprintRaw Source #

Arguments

:: [Name]

Bound names, for highlighting

-> Raw

The term to pretty-print

-> Doc OutputAnnotation 

Pretty-print a raw term.

pprintTT Source #

Arguments

:: [Name]

The bound names (for highlighting and de Bruijn indices)

-> TT Name

The term to be printed

-> Doc OutputAnnotation 

Pretty-print a term

psubst :: Eq n => n -> TT n -> TT n -> TT n Source #

pToV :: Eq n => n -> TT n -> TT n Source #

Replace references to the given Name-like id with references to de Bruijn index 0.

pToVs :: Eq n => [n] -> TT n -> TT n Source #

Convert several names. First in the list comes out as V 0

pureTerm :: TT Name -> Bool Source #

Check whether a term has any hole bindings in it - impure if so

safeForgetEnv :: [Name] -> TT Name -> Maybe Raw Source #

showCG :: Name -> String Source #

showEnv :: (Eq n, Show n) => EnvTT n -> TT n -> String Source #

showEnvDbg :: (Show a, Eq a) => [(a, RigCount, Binder (TT a))] -> TT a -> [Char] Source #

showSep :: String -> [String] -> String Source #

sMN :: Int -> String -> Name Source #

sNS :: Name -> [String] -> Name Source #

str :: Text -> String Source #

subst Source #

Arguments

:: Eq n 
=> n

The id to replace

-> TT n

The replacement term

-> TT n

The term to replace in

-> TT n 

As instantiate, but in addition to replacing V 0, replace references to the given Name-like id.

substNames :: Eq n => [(n, TT n)] -> TT n -> TT n Source #

As subst, but takes a list of (name, substitution) pairs instead of a single name and substitution

substTerm Source #

Arguments

:: Eq n 
=> TT n

Old term

-> TT n

New term

-> TT n

template term

-> TT n 

Replaces all terms equal (in the sense of (==)) to the old term with the new term.

substV :: TT n -> TT n -> TT n Source #

As instantiate, but also decrement the indices of all de Bruijn variables remaining in the term, so that there are no more references to the variable that has been substituted.

sUN :: String -> Name Source #

tcname :: Name -> Bool Source #

Return True if the argument Name should be interpreted as the name of a interface.

termSmallerThan :: Int -> Term -> Bool Source #

Hard-code a heuristic maximum term size, to prevent attempts to serialize or force infinite or just gigantic terms

tfail :: Err -> TC a Source #

thead :: Text -> Char Source #

tnull :: Text -> Bool Source #

toAlist :: Ctxt a -> [(Name, a)] Source #

traceWhen :: Bool -> String -> a -> a Source #

txt :: String -> Text Source #

unApply :: TT n -> (TT n, [TT n]) Source #

Deconstruct an application; returns the function and a list of arguments

unList :: Term -> Maybe [Term] Source #

updateDef :: Name -> (a -> a) -> Ctxt a -> Ctxt a Source #

vToP :: TT n -> TT n Source #

Replace de Bruijn indices in the given term with explicit references to the names of the bindings they refer to. It is an error if the given term contains free de Bruijn indices.

weakenTm :: Int -> TT n -> TT n Source #

Weaken a term by adding i to each de Bruijn index (i.e. lift it over i bindings)

fstEnv :: (a, b, c) -> a Source #

rigEnv :: (a, b, c) -> b Source #

sndEnv :: (a, b, c) -> c Source #

lookupBinder :: Eq n => n -> EnvTT n -> Maybe (Binder (TT n)) Source #

envBinders :: [(a, b, b)] -> [(a, b)] Source #

envZero :: [(a, b, c)] -> [(a, RigCount, c)] Source #