License | BSD3 |
---|---|
Maintainer | The Idris Community. |
Safe Haskell | Safe-Inferred |
Language | Haskell2010 |
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
- data AppStatus n
- = Complete
- | MaybeHoles
- | Holes [n]
- data ArithTy
- data Binder b
- = Lam {
- binderCount :: RigCount
- binderTy :: !b
- | Pi {
- binderCount :: RigCount
- binderImpl :: Maybe ImplicitInfo
- binderTy :: !b
- binderKind :: !b
- | Let {
- binderCount :: RigCount
- binderTy :: !b
- binderVal :: b
- | NLet { }
- | Hole {
- binderTy :: !b
- | GHole {
- envlen :: Int
- localnames :: [Name]
- binderTy :: !b
- | Guess { }
- | PVar {
- binderCount :: RigCount
- binderTy :: !b
- | PVTy {
- binderTy :: !b
- = Lam {
- data Const
- type Ctxt a = Map Name (Map Name a)
- data ConstraintFC = ConstraintFC {
- uconstraint :: UConstraint
- ufc :: FC
- data DataOpt
- = Codata
- | DataErrRev
- type DataOpts = [DataOpt]
- data Datatype n = Data {}
- type Env = EnvTT Name
- type EnvTT n = [(n, RigCount, Binder (TT n))]
- type Err = Err' Term
- data Err' t
- = 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]
- | 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)])]
- | ElabScriptStuck t
- | RunningElabScript (Err' t)
- | ElabScriptStaging Name
- | FancyMsg [ErrorReportPart]
- data ErrorReportPart
- data FC
- newtype FC' = FC' {}
- data ImplicitInfo = Impl {
- tcimplementation :: Bool
- toplevel_imp :: Bool
- machine_gen :: Bool
- data IntTy
- data Name
- data NameOutput
- data NameType
- data NativeTy
- data OutputAnnotation
- = AnnName Name (Maybe NameOutput) (Maybe String) (Maybe String)
- | AnnBoundName Name Bool
- | AnnConst Const
- | AnnData String String
- | AnnType String String
- | AnnKeyword
- | AnnFC FC
- | AnnTextFmt TextFormatting
- | AnnLink String
- | AnnTerm [(Name, Bool)] (TT Name)
- | AnnSearchResult Ordering
- | AnnErr Err
- | AnnNamespace [Text] (Maybe FilePath)
- | AnnQuasiquote
- | AnnAntiquote
- | AnnSyntax String
- data Provenance
- data Raw
- data RigCount
- data SpecialName
- data TC a
- type Term = TT Name
- class TermSize a where
- data TextFormatting
- data TT n
- type Type = Term
- data TypeInfo = TI {
- con_names :: [Name]
- codata :: Bool
- data_opts :: DataOpts
- param_pos :: [Int]
- mutual_types :: [Name]
- linear_con :: Bool
- data UConstraint
- type UCs = (Int, [UConstraint])
- data UExp
- data Universe
- addAlist :: [(Name, a)] -> Ctxt a -> Ctxt a
- addBinder :: TT n -> TT n
- addDef :: Name -> a -> Ctxt a -> Ctxt a
- allTTNames :: Eq n => TT n -> [n]
- arity :: TT n -> Int
- bindAll :: [(n, Binder (TT n))] -> TT n -> TT n
- bindingOf :: Name -> Bool -> Doc OutputAnnotation
- bindTyArgs :: (TT n -> Binder (TT n)) -> [(n, TT n)] -> TT n -> TT n
- caseName :: Name -> Bool
- constDocs :: Const -> String
- constIsType :: Const -> Bool
- deleteDefExact :: Name -> Ctxt a -> Ctxt a
- discard :: Monad m => m a -> m ()
- emptyContext :: Map k a
- emptyFC :: FC
- explicitNames :: TT n -> TT n
- fc_end :: FC -> (Int, Int)
- fc_fname :: FC -> String
- fc_start :: FC -> (Int, Int)
- fcIn :: FC -> FC -> Bool
- fileFC :: String -> FC
- finalise :: Eq n => TT n -> TT n
- fmapMB :: Monad m => (a -> m b) -> Binder a -> m (Binder b)
- forget :: TT Name -> Raw
- forgetEnv :: [Name] -> TT Name -> Raw
- freeNames :: Eq n => TT n -> [n]
- getArgTys :: TT n -> [(n, TT n)]
- getRetTy :: TT n -> TT n
- substRetTy :: TT n -> TT n
- implicitable :: Name -> Bool
- instantiate :: TT n -> TT n -> TT n
- internalNS :: String
- intTyName :: IntTy -> String
- isInjective :: TT n -> Bool
- isTypeConst :: Const -> Bool
- lookupCtxt :: Name -> Ctxt a -> [a]
- lookupCtxtExact :: Name -> Ctxt a -> Maybe a
- lookupCtxtName :: Name -> Ctxt a -> [(Name, a)]
- mapCtxt :: (a -> b) -> Ctxt a -> Ctxt b
- mkApp :: TT n -> [TT n] -> TT n
- nativeTyWidth :: NativeTy -> Int
- nextName :: Name -> Name
- noOccurrence :: Eq n => n -> TT n -> Bool
- nsroot :: Name -> Name
- occurrences :: Eq n => n -> TT n -> Int
- pEraseType :: TT n -> TT n
- pmap :: (t -> b) -> (t, t) -> (b, b)
- pprintRaw :: [Name] -> Raw -> Doc OutputAnnotation
- pprintTT :: [Name] -> TT Name -> Doc OutputAnnotation
- pprintTTClause :: [(Name, Type)] -> Term -> Term -> Doc OutputAnnotation
- prettyEnv :: Env -> Term -> Doc OutputAnnotation
- psubst :: Eq n => n -> TT n -> TT n -> TT n
- pToV :: Eq n => n -> TT n -> TT n
- pToVs :: Eq n => [n] -> TT n -> TT n
- pureTerm :: TT Name -> Bool
- raw_apply :: Raw -> [Raw] -> Raw
- raw_unapply :: Raw -> (Raw, [Raw])
- refsIn :: TT Name -> [Name]
- safeForget :: TT Name -> Maybe Raw
- safeForgetEnv :: [Name] -> TT Name -> Maybe Raw
- showCG :: Name -> String
- showEnv :: (Eq n, Show n) => EnvTT n -> TT n -> String
- showEnvDbg :: (Show a, Eq a) => [(a, RigCount, Binder (TT a))] -> TT a -> [Char]
- showSep :: String -> [String] -> String
- sImplementationN :: Name -> [String] -> SpecialName
- sMN :: Int -> String -> Name
- sNS :: Name -> [String] -> Name
- str :: Text -> String
- subst :: Eq n => n -> TT n -> TT n -> TT n
- substNames :: Eq n => [(n, TT n)] -> TT n -> TT n
- substTerm :: Eq n => TT n -> TT n -> TT n -> TT n
- substV :: TT n -> TT n -> TT n
- sUN :: String -> Name
- tcname :: Name -> Bool
- termSmallerThan :: Int -> Term -> Bool
- tfail :: Err -> TC a
- thead :: Text -> Char
- tnull :: Text -> Bool
- toAlist :: Ctxt a -> [(Name, a)]
- traceWhen :: Bool -> String -> a -> a
- txt :: String -> Text
- unApply :: TT n -> (TT n, [TT n])
- uniqueBinders :: [Name] -> TT Name -> TT Name
- uniqueName :: Name -> [Name] -> Name
- uniqueNameFrom :: [Name] -> [Name] -> Name
- uniqueNameSet :: Name -> Set Name -> Name
- unList :: Term -> Maybe [Term]
- updateDef :: Name -> (a -> a) -> Ctxt a -> Ctxt a
- vToP :: TT n -> TT n
- weakenTm :: Int -> TT n -> TT n
- rigPlus :: RigCount -> RigCount -> RigCount
- rigMult :: RigCount -> RigCount -> RigCount
- fstEnv :: (a, b, c) -> a
- rigEnv :: (a, b, c) -> b
- sndEnv :: (a, b, c) -> c
- lookupBinder :: Eq n => n -> EnvTT n -> Maybe (Binder (TT n))
- envBinders :: [(a, b, b)] -> [(a, b)]
- envZero :: [(a, b, c)] -> [(a, RigCount, c)]
Documentation
Constructors
Complete | |
MaybeHoles | |
Holes [n] |
Instances
Functor AppStatus Source # | |
ToJSON t => ToJSON (AppStatus t) | |
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 # | |
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 # | |
Show n => Show (AppStatus n) Source # | |
NFData a => NFData (AppStatus a) | |
Defined in Idris.Core.DeepSeq | |
Eq n => Eq (AppStatus n) Source # | |
Ord n => Ord (AppStatus n) Source # | |
type Rep (AppStatus n) Source # | |
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])))) |
Instances
ToJSON ArithTy | |
Defined in IRTS.Portable Methods toEncoding :: ArithTy -> Encoding toJSONList :: [ArithTy] -> Value toEncodingList :: [ArithTy] -> Encoding | |
Data ArithTy Source # | |
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 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 # | |
Show ArithTy Source # | |
NFData ArithTy | |
Defined in Idris.Core.DeepSeq | |
Eq ArithTy Source # | |
Ord ArithTy Source # | |
type Rep ArithTy Source # | |
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)) |
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. |
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. |
Hole | A hole in a term under construction in the elaborator. If this is not filled during elaboration, it is an error. |
Fields
| |
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. |
PVar | A pattern variable (these are bound around terms that make up pattern-match clauses) |
Fields
| |
PVTy | The type of a pattern binding |
Fields
|
Instances
Foldable Binder Source # | |
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 elem :: Eq a => a -> Binder a -> Bool maximum :: Ord a => Binder a -> a | |
Traversable Binder Source # | |
Functor Binder Source # | |
ToJSON t => ToJSON (Binder t) | |
Defined in IRTS.Portable Methods toEncoding :: Binder t -> Encoding toJSONList :: [Binder t] -> Value toEncodingList :: [Binder t] -> Encoding | |
Data b => Data (Binder b) Source # | |
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 # | |
Show b => Show (Binder b) Source # | |
Binary b => Binary (Binder b) | |
NFData b => NFData (Binder b) | |
Defined in Idris.Core.DeepSeq | |
Eq b => Eq (Binder b) Source # | |
Ord b => Ord (Binder b) Source # | |
type Rep (Binder b) Source # | |
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)))))) |
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
ToJSON Const | |
Defined in IRTS.Portable Methods toEncoding :: Const -> Encoding toJSONList :: [Const] -> Value toEncodingList :: [Const] -> Encoding | |
Data Const Source # | |
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 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 # | |
Show Const Source # | |
Binary Const | |
NFData Const | |
Defined in Idris.Core.DeepSeq | |
Eq Const Source # | |
Ord Const Source # | |
type Rep Const Source # | |
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
Data ConstraintFC Source # | |
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 # | |
Defined in Idris.Core.TT Associated Types type Rep ConstraintFC :: Type -> Type | |
Show ConstraintFC Source # | |
Defined in Idris.Core.TT Methods showsPrec :: Int -> ConstraintFC -> ShowS show :: ConstraintFC -> String showList :: [ConstraintFC] -> ShowS | |
Binary ConstraintFC | |
Defined in Idris.Core.Binary | |
NFData ConstraintFC | |
Defined in Idris.Core.DeepSeq Methods rnf :: ConstraintFC -> () | |
Eq ConstraintFC Source # | |
Defined in Idris.Core.TT | |
Ord ConstraintFC Source # | |
Defined in Idris.Core.TT Methods compare :: ConstraintFC -> ConstraintFC -> Ordering (<) :: ConstraintFC -> ConstraintFC -> Bool (<=) :: ConstraintFC -> ConstraintFC -> Bool (>) :: ConstraintFC -> ConstraintFC -> Bool (>=) :: ConstraintFC -> ConstraintFC -> Bool max :: ConstraintFC -> ConstraintFC -> ConstraintFC min :: ConstraintFC -> ConstraintFC -> ConstraintFC | |
type Rep ConstraintFC Source # | |
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 declaration options
Constructors
Codata | Set if the the data-type is coinductive |
DataErrRev |
Instances
Generic DataOpt Source # | |
Show DataOpt Source # | |
Binary DataOpt | |
NFData DataOpt | |
Defined in Idris.DeepSeq | |
Eq DataOpt Source # | |
type Rep DataOpt Source # | |
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)) |
Constructors
Data | |
Idris errors. Used as exceptions in the compiler, but reported to users if they reach the top level.
Constructors
Instances
Functor Err' Source # | |
Show Err Source # | |
NFData Err | |
Defined in Idris.Core.DeepSeq | |
Data t => Data (Err' t) Source # | |
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) 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 # | |
Binary a => Binary (Err' a) | |
Eq t => Eq (Err' t) Source # | |
Ord t => Ord (Err' t) Source # | |
type Rep (Err' t) Source # | |
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
Data ErrorReportPart Source # | |
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 # | |
Defined in Idris.Core.TT Associated Types type Rep ErrorReportPart :: Type -> Type Methods from :: ErrorReportPart -> Rep ErrorReportPart x to :: Rep ErrorReportPart x -> ErrorReportPart | |
Show ErrorReportPart Source # | |
Defined in Idris.Core.TT Methods showsPrec :: Int -> ErrorReportPart -> ShowS show :: ErrorReportPart -> String showList :: [ErrorReportPart] -> ShowS | |
Binary ErrorReportPart | |
Defined in Idris.Core.Binary | |
NFData ErrorReportPart | |
Defined in Idris.Core.DeepSeq Methods rnf :: ErrorReportPart -> () | |
Eq ErrorReportPart Source # | |
Defined in Idris.Core.TT Methods (==) :: ErrorReportPart -> ErrorReportPart -> Bool (/=) :: ErrorReportPart -> ErrorReportPart -> Bool | |
Ord ErrorReportPart Source # | |
Defined in Idris.Core.TT Methods compare :: ErrorReportPart -> ErrorReportPart -> Ordering (<) :: ErrorReportPart -> ErrorReportPart -> Bool (<=) :: ErrorReportPart -> ErrorReportPart -> Bool (>) :: ErrorReportPart -> ErrorReportPart -> Bool (>=) :: ErrorReportPart -> ErrorReportPart -> Bool max :: ErrorReportPart -> ErrorReportPart -> ErrorReportPart min :: ErrorReportPart -> ErrorReportPart -> ErrorReportPart | |
type Rep ErrorReportPart Source # | |
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]))))) |
Source location. These are typically produced by withExtent
Constructors
FC | |
NoFC | Locations for machine-generated terms |
FileFC | Locations with file only |
Fields
|
Instances
Data FC Source # | |
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 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 # | |
Semigroup FC Source # | |
Generic FC Source # | |
Show FC Source # | |
Binary FC | |
NFData FC | |
Defined in Idris.Core.DeepSeq | |
Eq FC Source # | Ignore source location equality (so deriving classes do not compare FCs) |
Ord FC Source # | |
SExpable FC Source # | |
type Rep FC Source # | |
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)))) |
FC with equality
Instances
Data FC' Source # | |
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' 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 # | |
Show FC' Source # | |
Binary FC' | |
NFData FC' | |
Defined in Idris.Core.DeepSeq | |
Eq FC' Source # | |
Ord FC' Source # | |
type Rep FC' Source # | |
Defined in Idris.Core.TT |
data ImplicitInfo Source #
Constructors
Impl | |
Fields
|
Instances
ToJSON ImplicitInfo | |
Defined in IRTS.Portable Methods toJSON :: ImplicitInfo -> Value toEncoding :: ImplicitInfo -> Encoding toJSONList :: [ImplicitInfo] -> Value toEncodingList :: [ImplicitInfo] -> Encoding | |
Data ImplicitInfo Source # | |
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 # | |
Defined in Idris.Core.TT Associated Types type Rep ImplicitInfo :: Type -> Type | |
Show ImplicitInfo Source # | |
Defined in Idris.Core.TT Methods showsPrec :: Int -> ImplicitInfo -> ShowS show :: ImplicitInfo -> String showList :: [ImplicitInfo] -> ShowS | |
Binary ImplicitInfo | |
Defined in Idris.Core.Binary | |
NFData ImplicitInfo | |
Defined in Idris.Core.DeepSeq Methods rnf :: ImplicitInfo -> () | |
Eq ImplicitInfo Source # | |
Defined in Idris.Core.TT | |
Ord ImplicitInfo Source # | |
Defined in Idris.Core.TT Methods compare :: ImplicitInfo -> ImplicitInfo -> Ordering (<) :: ImplicitInfo -> ImplicitInfo -> Bool (<=) :: ImplicitInfo -> ImplicitInfo -> Bool (>) :: ImplicitInfo -> ImplicitInfo -> Bool (>=) :: ImplicitInfo -> ImplicitInfo -> Bool max :: ImplicitInfo -> ImplicitInfo -> ImplicitInfo min :: ImplicitInfo -> ImplicitInfo -> ImplicitInfo | |
type Rep ImplicitInfo Source # | |
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)))) |
Instances
ToJSON IntTy | |
Defined in IRTS.Portable Methods toEncoding :: IntTy -> Encoding toJSONList :: [IntTy] -> Value toEncodingList :: [IntTy] -> Encoding | |
Data IntTy Source # | |
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 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 # | |
Show IntTy Source # | |
NFData IntTy | |
Defined in Idris.Core.DeepSeq | |
Eq IntTy Source # | |
Ord IntTy Source # | |
type Rep IntTy Source # | |
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))) |
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
ToJSON Name | |
Defined in IRTS.Portable Methods toEncoding :: Name -> Encoding toJSONList :: [Name] -> Value toEncodingList :: [Name] -> Encoding | |
Data Name Source # | |
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 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 # | |
Show Err Source # | |
Show Name Source # | |
Binary CaseAlt | |
Binary SC | |
Binary Name | |
NFData Err | |
Defined in Idris.Core.DeepSeq | |
NFData Name | |
Defined in Idris.Core.DeepSeq | |
Eq Name Source # | |
Ord Name Source # | |
TermSize CaseAlt Source # | |
TermSize SC Source # | |
SExpable Name Source # | |
Binary (TT Name) | |
TermSize (TT Name) Source # | |
type Rep Name Source # | |
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
Constructors
TypeOutput | |
FunOutput | |
DataOutput | |
MetavarOutput | |
PostulateOutput |
Instances
Generic NameOutput Source # | |
Defined in Idris.Core.TT Associated Types type Rep NameOutput :: Type -> Type | |
Show NameOutput Source # | |
Defined in Idris.Core.TT Methods showsPrec :: Int -> NameOutput -> ShowS show :: NameOutput -> String showList :: [NameOutput] -> ShowS | |
NFData NameOutput | |
Defined in Idris.Core.DeepSeq Methods rnf :: NameOutput -> () | |
Eq NameOutput Source # | |
Defined in Idris.Core.TT | |
Ord NameOutput Source # | |
Defined in Idris.Core.TT Methods compare :: NameOutput -> NameOutput -> Ordering (<) :: NameOutput -> NameOutput -> Bool (<=) :: NameOutput -> NameOutput -> Bool (>) :: NameOutput -> NameOutput -> Bool (>=) :: NameOutput -> NameOutput -> Bool max :: NameOutput -> NameOutput -> NameOutput min :: NameOutput -> NameOutput -> NameOutput | |
SExpable NameOutput Source # | |
Defined in Idris.IdeMode Methods toSExp :: NameOutput -> SExp Source # | |
type Rep NameOutput Source # | |
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)))) |
Instances
ToJSON NameType | |
Defined in IRTS.Portable Methods toEncoding :: NameType -> Encoding toJSONList :: [NameType] -> Value toEncodingList :: [NameType] -> Encoding | |
Data NameType Source # | |
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 # | |
Show NameType Source # | |
Binary NameType | |
NFData NameType | |
Defined in Idris.Core.DeepSeq | |
Eq NameType Source # | |
Ord NameType Source # | |
type Rep NameType Source # | |
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)))) |
Instances
Data NativeTy Source # | |
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 # | |
Defined in Idris.Core.TT | |
Generic NativeTy Source # | |
Show NativeTy Source # | |
NFData NativeTy | |
Defined in Idris.Core.DeepSeq | |
Eq NativeTy Source # | |
Ord NativeTy Source # | |
type Rep NativeTy Source # | |
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
Generic OutputAnnotation Source # | |
Defined in Idris.Core.TT Associated Types type Rep OutputAnnotation :: Type -> Type Methods from :: OutputAnnotation -> Rep OutputAnnotation x to :: Rep OutputAnnotation x -> OutputAnnotation | |
Show OutputAnnotation Source # | |
Defined in Idris.Core.TT Methods showsPrec :: Int -> OutputAnnotation -> ShowS show :: OutputAnnotation -> String showList :: [OutputAnnotation] -> ShowS | |
NFData OutputAnnotation | |
Defined in Idris.Core.DeepSeq Methods rnf :: OutputAnnotation -> () | |
Eq OutputAnnotation Source # | |
Defined in Idris.Core.TT Methods (==) :: OutputAnnotation -> OutputAnnotation -> Bool (/=) :: OutputAnnotation -> OutputAnnotation -> Bool | |
Ord OutputAnnotation Source # | |
Defined in Idris.Core.TT Methods compare :: OutputAnnotation -> OutputAnnotation -> Ordering (<) :: OutputAnnotation -> OutputAnnotation -> Bool (<=) :: OutputAnnotation -> OutputAnnotation -> Bool (>) :: OutputAnnotation -> OutputAnnotation -> Bool (>=) :: OutputAnnotation -> OutputAnnotation -> Bool max :: OutputAnnotation -> OutputAnnotation -> OutputAnnotation min :: OutputAnnotation -> OutputAnnotation -> OutputAnnotation | |
SExpable OutputAnnotation Source # | |
Defined in Idris.IdeMode Methods toSExp :: OutputAnnotation -> SExp Source # | |
type Rep OutputAnnotation Source # | |
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 #
Constructors
ExpectedType | |
TooManyArgs Term | |
InferredVal | |
GivenVal | |
SourceTerm Term |
Instances
Data Provenance Source # | |
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 # | |
Defined in Idris.Core.TT Associated Types type Rep Provenance :: Type -> Type | |
Show Provenance Source # | |
Defined in Idris.Core.TT Methods showsPrec :: Int -> Provenance -> ShowS show :: Provenance -> String showList :: [Provenance] -> ShowS | |
Binary Provenance | |
Defined in Idris.Core.Binary | |
NFData Provenance | |
Defined in Idris.Core.DeepSeq Methods rnf :: Provenance -> () | |
Eq Provenance Source # | |
Defined in Idris.Core.TT | |
Ord Provenance Source # | |
Defined in Idris.Core.TT Methods compare :: Provenance -> Provenance -> Ordering (<) :: Provenance -> Provenance -> Bool (<=) :: Provenance -> Provenance -> Bool (>) :: Provenance -> Provenance -> Bool (>=) :: Provenance -> Provenance -> Bool max :: Provenance -> Provenance -> Provenance min :: Provenance -> Provenance -> Provenance | |
type Rep Provenance Source # | |
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))))) |
Instances
Data Raw Source # | |
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 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 # | |
Show Raw Source # | |
Binary Raw | |
NFData Raw | |
Defined in Idris.Core.DeepSeq | |
Eq Raw Source # | |
Ord Raw Source # | |
type Rep Raw Source # | |
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))))) |
Instances
ToJSON RigCount | |
Defined in IRTS.Portable Methods toEncoding :: RigCount -> Encoding toJSONList :: [RigCount] -> Value toEncodingList :: [RigCount] -> Encoding | |
Data RigCount Source # | |
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 # | |
Show RigCount Source # | |
Binary RigCount | |
NFData RigCount | |
Defined in Idris.Core.DeepSeq | |
Eq RigCount Source # | |
Ord RigCount Source # | |
type Rep RigCount Source # | |
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 #
Constructors
WhereN !Int !Name !Name | |
WithN !Int !Name | |
ImplementationN !Name [Text] | |
ParentN !Name !Text | |
MethodN !Name | |
CaseN !FC' !Name | |
ImplementationCtorN !Name | |
MetaN !Name !Name |
Instances
Data SpecialName Source # | |
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 # | |
Defined in Idris.Core.TT Associated Types type Rep SpecialName :: Type -> Type | |
Show SpecialName Source # | |
Defined in Idris.Core.TT Methods showsPrec :: Int -> SpecialName -> ShowS show :: SpecialName -> String showList :: [SpecialName] -> ShowS | |
Binary SpecialName | |
Defined in Idris.Core.Binary | |
NFData SpecialName | |
Defined in Idris.Core.DeepSeq Methods rnf :: SpecialName -> () | |
Eq SpecialName Source # | |
Defined in Idris.Core.TT | |
Ord SpecialName Source # | |
Defined in Idris.Core.TT Methods compare :: SpecialName -> SpecialName -> Ordering (<) :: SpecialName -> SpecialName -> Bool (<=) :: SpecialName -> SpecialName -> Bool (>) :: SpecialName -> SpecialName -> Bool (>=) :: SpecialName -> SpecialName -> Bool max :: SpecialName -> SpecialName -> SpecialName min :: SpecialName -> SpecialName -> SpecialName | |
type Rep SpecialName Source # | |
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 TextFormatting Source #
Text formatting output
Constructors
BoldText | |
ItalicText | |
UnderlineText |
Instances
Generic TextFormatting Source # | |
Defined in Idris.Core.TT Associated Types type Rep TextFormatting :: Type -> Type | |
Show TextFormatting Source # | |
Defined in Idris.Core.TT Methods showsPrec :: Int -> TextFormatting -> ShowS show :: TextFormatting -> String showList :: [TextFormatting] -> ShowS | |
NFData TextFormatting | |
Defined in Idris.Core.DeepSeq Methods rnf :: TextFormatting -> () | |
Eq TextFormatting Source # | |
Defined in Idris.Core.TT Methods (==) :: TextFormatting -> TextFormatting -> Bool (/=) :: TextFormatting -> TextFormatting -> Bool | |
Ord TextFormatting Source # | |
Defined in Idris.Core.TT Methods compare :: TextFormatting -> TextFormatting -> Ordering (<) :: TextFormatting -> TextFormatting -> Bool (<=) :: TextFormatting -> TextFormatting -> Bool (>) :: TextFormatting -> TextFormatting -> Bool (>=) :: TextFormatting -> TextFormatting -> Bool max :: TextFormatting -> TextFormatting -> TextFormatting min :: TextFormatting -> TextFormatting -> TextFormatting | |
type Rep TextFormatting Source # | |
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))) |
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
Functor TT Source # | |
Show Err Source # | |
Binary CaseAlt | |
Binary SC | |
NFData Err | |
Defined in Idris.Core.DeepSeq | |
TermSize CaseAlt Source # | |
TermSize SC Source # | |
ToJSON t => ToJSON (TT t) | |
Defined in IRTS.Portable Methods toEncoding :: TT t -> Encoding toJSONList :: [TT t] -> Value toEncodingList :: [TT t] -> Encoding | |
Data n => Data (TT n) Source # | |
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) 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 # | |
(Eq n, Show n) => Show (TT n) Source # | |
Binary (TT Name) | |
NFData n => NFData (TT n) | |
Defined in Idris.Core.DeepSeq | |
Eq n => Eq (TT n) Source # | |
Ord n => Ord (TT n) Source # | |
TermSize (TT Name) Source # | |
type Rep (TT n) Source # | |
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)))))) |
Constructors
TI | |
Fields
|
Instances
Generic TypeInfo Source # | |
Show TypeInfo Source # | |
Binary TypeInfo | |
NFData TypeInfo | |
Defined in Idris.DeepSeq | |
type Rep TypeInfo Source # | |
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
Instances
Data UConstraint Source # | |
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 # | |
Defined in Idris.Core.TT Associated Types type Rep UConstraint :: Type -> Type | |
Show UConstraint Source # | |
Defined in Idris.Core.TT Methods showsPrec :: Int -> UConstraint -> ShowS show :: UConstraint -> String showList :: [UConstraint] -> ShowS | |
Binary UConstraint | |
Defined in Idris.Core.Binary | |
NFData UConstraint | |
Defined in Idris.Core.DeepSeq Methods rnf :: UConstraint -> () | |
Eq UConstraint Source # | |
Defined in Idris.Core.TT | |
Ord UConstraint Source # | |
Defined in Idris.Core.TT Methods compare :: UConstraint -> UConstraint -> Ordering (<) :: UConstraint -> UConstraint -> Bool (<=) :: UConstraint -> UConstraint -> Bool (>) :: UConstraint -> UConstraint -> Bool (>=) :: UConstraint -> UConstraint -> Bool max :: UConstraint -> UConstraint -> UConstraint min :: UConstraint -> UConstraint -> UConstraint | |
type Rep UConstraint Source # | |
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 #
Universe expressions for universe checking
Constructors
UVar String Int | universe variable, with source file to disambiguate |
UVal Int | explicit universe level |
Instances
ToJSON UExp | |
Defined in IRTS.Portable Methods toEncoding :: UExp -> Encoding toJSONList :: [UExp] -> Value toEncodingList :: [UExp] -> Encoding | |
Data UExp Source # | |
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 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 # | |
Show UExp Source # | |
Binary UExp | |
NFData UExp | |
Defined in Idris.Core.DeepSeq | |
Eq UExp Source # | |
Ord UExp Source # | |
type Rep UExp Source # | |
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))) |
Constructors
NullType | |
UniqueType | |
AllTypes |
Instances
Data Universe Source # | |
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 # | |
Show Universe Source # | |
Binary Universe | |
NFData Universe | |
Defined in Idris.Core.DeepSeq | |
Eq Universe Source # | |
Ord Universe Source # | |
type Rep Universe Source # | |
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))) |
allTTNames :: Eq n => TT n -> [n] Source #
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.
Arguments
:: Name | ^ the bound name |
-> Bool | ^ whether the name is implicit |
-> Doc OutputAnnotation |
Pretty-printer helper for the binding site of a name
constIsType :: Const -> Bool Source #
Determines whether the input constant represents a type
emptyContext :: Map k a Source #
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.
fcIn :: FC -> FC -> Bool Source #
Determine whether the first argument is completely contained in the second
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.
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.
substRetTy :: TT n -> TT n Source #
As getRetTy but substitutes names for de Bruijn indices
implicitable :: Name -> Bool Source #
instantiate :: TT n -> TT n -> TT n Source #
Replace the outermost (index 0) de Bruijn variable with the given term
internalNS :: 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.
isTypeConst :: Const -> Bool Source #
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.
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.
nativeTyWidth :: NativeTy -> Int Source #
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 #
Arguments
:: [Name] | Bound names, for highlighting |
-> Raw | The term to pretty-print |
-> Doc OutputAnnotation |
Pretty-print a raw term.
Arguments
:: [Name] | The bound names (for highlighting and de Bruijn indices) |
-> TT Name | The term to be printed |
-> Doc OutputAnnotation |
Pretty-print a term
pprintTTClause :: [(Name, Type)] -> Term -> Term -> Doc OutputAnnotation 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
sImplementationN :: Name -> [String] -> SpecialName 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
,
replace references to the given V
0Name
-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
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.
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
unApply :: TT n -> (TT n, [TT n]) Source #
Deconstruct an application; returns the function and a list of arguments
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)
envBinders :: [(a, b, b)] -> [(a, b)] Source #