| License | BSD3 |
|---|---|
| Maintainer | The Idris Community. |
| Safe Haskell | None |
| 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 {}
- 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 {}
- 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 -> p -> p
- 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, b1, b2)] -> [(a, b2)]
- envZero :: [(a, b, c)] -> [(a, RigCount, c)]
Documentation
Constructors
| Complete | |
| MaybeHoles | |
| Holes [n] |
Instances
| Functor AppStatus Source # | |
| Eq n => Eq (AppStatus n) Source # | |
| 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 :: (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) # | |
| Ord n => Ord (AppStatus n) Source # | |
Defined in Idris.Core.TT | |
| Show n => Show (AppStatus n) Source # | |
| Generic (AppStatus n) Source # | |
| ToJSON t => ToJSON (AppStatus t) Source # | |
Defined in IRTS.Portable | |
| NFData a => NFData (AppStatus a) Source # | |
Defined in Idris.Core.DeepSeq | |
| type Rep (AppStatus n) Source # | |
Defined in Idris.Core.TT type Rep (AppStatus n) = D1 (MetaData "AppStatus" "Idris.Core.TT" "idris-1.3.2-3LpOXLFJmzJ3DT7fAtaO1v" 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
| Eq ArithTy Source # | |
| 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 # toConstr :: ArithTy -> Constr # dataTypeOf :: ArithTy -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ArithTy) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ArithTy) # gmapT :: (forall b. Data b => b -> b) -> ArithTy -> ArithTy # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ArithTy -> r # gmapQr :: (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 # | |
| Ord ArithTy Source # | |
| Show ArithTy Source # | |
| Generic ArithTy Source # | |
| ToJSON ArithTy Source # | |
Defined in IRTS.Portable | |
| NFData ArithTy Source # | |
Defined in Idris.Core.DeepSeq | |
| type Rep ArithTy Source # | |
Defined in Idris.Core.TT type Rep ArithTy = D1 (MetaData "ArithTy" "Idris.Core.TT" "idris-1.3.2-3LpOXLFJmzJ3DT7fAtaO1v" 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 | A function binding |
Fields
| |
| Pi | A binding that occurs in a function type
expression, e.g. |
Fields
| |
| Let | A binding that occurs in a |
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
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
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 declaration options
Constructors
| Codata | Set if the the data-type is coinductive |
| DataErrRev |
Constructors
| Data | |
Idris errors. Used as exceptions in the compiler, but reported to users if they reach the top level.
Constructors
Instances
data ErrorReportPart Source #
Used for error reflection
Instances
Source location. These are typically produced by withExtent
Instances
| Eq FC Source # | Ignore source location equality (so deriving classes do not compare FCs) |
| 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 :: (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 # | |
| Ord FC Source # | |
| Show FC Source # | |
| Generic FC Source # | |
| Semigroup FC Source # | |
| Monoid FC Source # | |
| Binary FC Source # | |
| NFData FC Source # | |
Defined in Idris.Core.DeepSeq | |
| SExpable FC Source # | |
| type Rep FC Source # | |
Defined in Idris.Core.TT type Rep FC = D1 (MetaData "FC" "Idris.Core.TT" "idris-1.3.2-3LpOXLFJmzJ3DT7fAtaO1v" 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
| Eq FC' Source # | |
| 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 :: (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' # | |
| Ord FC' Source # | |
| Show FC' Source # | |
| Generic FC' Source # | |
| Binary FC' Source # | |
| NFData FC' Source # | |
Defined in Idris.Core.DeepSeq | |
| type Rep FC' Source # | |
Defined in Idris.Core.TT | |
data ImplicitInfo Source #
Constructors
| Impl | |
Fields
| |
Instances
Instances
| Eq IntTy Source # | |
| 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 :: (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 # | |
| Ord IntTy Source # | |
| Show IntTy Source # | |
| Generic IntTy Source # | |
| ToJSON IntTy Source # | |
Defined in IRTS.Portable | |
| NFData IntTy Source # | |
Defined in Idris.Core.DeepSeq | |
| type Rep IntTy Source # | |
Defined in Idris.Core.TT type Rep IntTy = D1 (MetaData "IntTy" "Idris.Core.TT" "idris-1.3.2-3LpOXLFJmzJ3DT7fAtaO1v" 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
data NameOutput Source #
Output annotation for pretty-printed name - decides colour
Constructors
| TypeOutput | |
| FunOutput | |
| DataOutput | |
| MetavarOutput | |
| PostulateOutput |
Instances
Instances
Instances
| Enum NativeTy Source # | |
| Eq NativeTy Source # | |
| 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 :: (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 # | |
| Ord NativeTy Source # | |
Defined in Idris.Core.TT | |
| Show NativeTy Source # | |
| Generic NativeTy Source # | |
| NFData NativeTy Source # | |
Defined in Idris.Core.DeepSeq | |
| type Rep NativeTy Source # | |
Defined in Idris.Core.TT type Rep NativeTy = D1 (MetaData "NativeTy" "Idris.Core.TT" "idris-1.3.2-3LpOXLFJmzJ3DT7fAtaO1v" 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
data Provenance Source #
Constructors
| ExpectedType | |
| TooManyArgs Term | |
| InferredVal | |
| GivenVal | |
| SourceTerm Term |
Instances
Instances
Instances
| Eq RigCount Source # | |
| 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 :: (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 # | |
| Ord RigCount Source # | |
Defined in Idris.Core.TT | |
| Show RigCount Source # | |
| Generic RigCount Source # | |
| ToJSON RigCount Source # | |
Defined in IRTS.Portable | |
| Binary RigCount Source # | |
| NFData RigCount Source # | |
Defined in Idris.Core.DeepSeq | |
| type Rep RigCount Source # | |
Defined in Idris.Core.TT | |
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 TextFormatting Source #
Text formatting output
Constructors
| BoldText | |
| ItalicText | |
| UnderlineText |
Instances
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
Constructors
| TI | |
Instances
| Show TypeInfo Source # | |
| Generic TypeInfo Source # | |
| Binary TypeInfo Source # | |
| NFData TypeInfo Source # | |
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.2-3LpOXLFJmzJ3DT7fAtaO1v" 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
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
| Eq UExp Source # | |
| 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 :: (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 # | |
| Ord UExp Source # | |
| Show UExp Source # | |
| Generic UExp Source # | |
| ToJSON UExp Source # | |
Defined in IRTS.Portable | |
| Binary UExp Source # | |
| NFData UExp Source # | |
Defined in Idris.Core.DeepSeq | |
| type Rep UExp Source # | |
Defined in Idris.Core.TT type Rep UExp = D1 (MetaData "UExp" "Idris.Core.TT" "idris-1.3.2-3LpOXLFJmzJ3DT7fAtaO1v" 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
| Eq Universe Source # | |
| 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 :: (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 # | |
| Ord Universe Source # | |
Defined in Idris.Core.TT | |
| Show Universe Source # | |
| Generic Universe Source # | |
| Binary Universe Source # | |
| NFData Universe Source # | |
Defined in Idris.Core.DeepSeq | |
| type Rep Universe Source # | |
Defined in Idris.Core.TT | |
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 #
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 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, b1, b2)] -> [(a, b2)] Source #