idris-0.12.3: Functional Programming Language with Dependent Types

CopyrightLicense : BSD3
MaintainerThe Idris Community.
Safe HaskellNone
LanguageHaskell98

IRTS.Lang

Description

 

Documentation

data LVar Source #

Constructors

Loc Int 
Glob Name 

Instances

Eq LVar Source # 

Methods

(==) :: LVar -> LVar -> Bool #

(/=) :: LVar -> LVar -> Bool #

Show LVar Source # 

Methods

showsPrec :: Int -> LVar -> ShowS #

show :: LVar -> String #

showList :: [LVar] -> ShowS #

data FDesc Source #

Instances

Eq FDesc Source # 

Methods

(==) :: FDesc -> FDesc -> Bool #

(/=) :: FDesc -> FDesc -> Bool #

Show FDesc Source # 

Methods

showsPrec :: Int -> FDesc -> ShowS #

show :: FDesc -> String #

showList :: [FDesc] -> ShowS #

data PrimFn Source #

Instances

Eq PrimFn Source # 

Methods

(==) :: PrimFn -> PrimFn -> Bool #

(/=) :: PrimFn -> PrimFn -> Bool #

Show PrimFn Source # 
Generic PrimFn Source # 

Associated Types

type Rep PrimFn :: * -> * #

Methods

from :: PrimFn -> Rep PrimFn x #

to :: Rep PrimFn x -> PrimFn #

type Rep PrimFn Source # 
type Rep PrimFn = D1 (MetaData "PrimFn" "IRTS.Lang" "idris-0.12.3-7kqdN3SqLCzDGiFd89aCg" False) ((:+:) ((:+:) ((:+:) ((:+:) ((:+:) ((:+:) (C1 (MetaCons "LPlus" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 ArithTy))) (C1 (MetaCons "LMinus" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 ArithTy)))) ((:+:) (C1 (MetaCons "LTimes" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 ArithTy))) (C1 (MetaCons "LUDiv" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 IntTy))))) ((:+:) ((:+:) (C1 (MetaCons "LSDiv" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 ArithTy))) (C1 (MetaCons "LURem" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 IntTy)))) ((:+:) (C1 (MetaCons "LSRem" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 ArithTy))) (C1 (MetaCons "LAnd" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 IntTy)))))) ((:+:) ((:+:) ((:+:) (C1 (MetaCons "LOr" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 IntTy))) (C1 (MetaCons "LXOr" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 IntTy)))) ((:+:) (C1 (MetaCons "LCompl" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 IntTy))) (C1 (MetaCons "LSHL" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 IntTy))))) ((:+:) ((:+:) (C1 (MetaCons "LLSHR" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 IntTy))) (C1 (MetaCons "LASHR" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 IntTy)))) ((:+:) (C1 (MetaCons "LEq" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 ArithTy))) (C1 (MetaCons "LLt" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 IntTy))))))) ((:+:) ((:+:) ((:+:) ((:+:) (C1 (MetaCons "LLe" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 IntTy))) (C1 (MetaCons "LGt" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 IntTy)))) ((:+:) (C1 (MetaCons "LGe" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 IntTy))) (C1 (MetaCons "LSLt" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 ArithTy))))) ((:+:) ((:+:) (C1 (MetaCons "LSLe" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 ArithTy))) (C1 (MetaCons "LSGt" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 ArithTy)))) ((:+:) (C1 (MetaCons "LSGe" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 ArithTy))) (C1 (MetaCons "LSExt" PrefixI False) ((:*:) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 IntTy)) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 IntTy))))))) ((:+:) ((:+:) ((:+:) (C1 (MetaCons "LZExt" PrefixI False) ((:*:) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 IntTy)) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 IntTy)))) (C1 (MetaCons "LTrunc" PrefixI False) ((:*:) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 IntTy)) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 IntTy))))) ((:+:) (C1 (MetaCons "LStrConcat" PrefixI False) U1) (C1 (MetaCons "LStrLt" PrefixI False) U1))) ((:+:) ((:+:) (C1 (MetaCons "LStrEq" PrefixI False) U1) (C1 (MetaCons "LStrLen" PrefixI False) U1)) ((:+:) (C1 (MetaCons "LIntFloat" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 IntTy))) (C1 (MetaCons "LFloatInt" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 IntTy)))))))) ((:+:) ((:+:) ((:+:) ((:+:) ((:+:) (C1 (MetaCons "LIntStr" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 IntTy))) (C1 (MetaCons "LStrInt" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 IntTy)))) ((:+:) (C1 (MetaCons "LFloatStr" PrefixI False) U1) (C1 (MetaCons "LStrFloat" PrefixI False) U1))) ((:+:) ((:+:) (C1 (MetaCons "LChInt" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 IntTy))) (C1 (MetaCons "LIntCh" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 IntTy)))) ((:+:) (C1 (MetaCons "LBitCast" PrefixI False) ((:*:) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 ArithTy)) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 ArithTy)))) (C1 (MetaCons "LFExp" PrefixI False) U1)))) ((:+:) ((:+:) ((:+:) (C1 (MetaCons "LFLog" PrefixI False) U1) (C1 (MetaCons "LFSin" PrefixI False) U1)) ((:+:) (C1 (MetaCons "LFCos" PrefixI False) U1) (C1 (MetaCons "LFTan" PrefixI False) U1))) ((:+:) ((:+:) (C1 (MetaCons "LFASin" PrefixI False) U1) (C1 (MetaCons "LFACos" PrefixI False) U1)) ((:+:) (C1 (MetaCons "LFATan" PrefixI False) U1) (C1 (MetaCons "LFSqrt" PrefixI False) U1))))) ((:+:) ((:+:) ((:+:) ((:+:) (C1 (MetaCons "LFFloor" PrefixI False) U1) (C1 (MetaCons "LFCeil" PrefixI False) U1)) ((:+:) (C1 (MetaCons "LFNegate" PrefixI False) U1) (C1 (MetaCons "LStrHead" PrefixI False) U1))) ((:+:) ((:+:) (C1 (MetaCons "LStrTail" PrefixI False) U1) (C1 (MetaCons "LStrCons" PrefixI False) U1)) ((:+:) (C1 (MetaCons "LStrIndex" PrefixI False) U1) (C1 (MetaCons "LStrRev" PrefixI False) U1)))) ((:+:) ((:+:) ((:+:) (C1 (MetaCons "LStrSubstr" PrefixI False) U1) (C1 (MetaCons "LReadStr" PrefixI False) U1)) ((:+:) (C1 (MetaCons "LWriteStr" PrefixI False) U1) (C1 (MetaCons "LSystemInfo" PrefixI False) U1))) ((:+:) ((:+:) (C1 (MetaCons "LFork" PrefixI False) U1) (C1 (MetaCons "LPar" PrefixI False) U1)) ((:+:) (C1 (MetaCons "LExternal" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Name))) (C1 (MetaCons "LNoOp" PrefixI False) U1)))))))

data LAlt' e Source #

Instances

Functor LAlt' Source # 

Methods

fmap :: (a -> b) -> LAlt' a -> LAlt' b #

(<$) :: a -> LAlt' b -> LAlt' a #

Eq e => Eq (LAlt' e) Source # 

Methods

(==) :: LAlt' e -> LAlt' e -> Bool #

(/=) :: LAlt' e -> LAlt' e -> Bool #

Show e => Show (LAlt' e) Source # 

Methods

showsPrec :: Int -> LAlt' e -> ShowS #

show :: LAlt' e -> String #

showList :: [LAlt' e] -> ShowS #

data LDecl Source #

Instances

Eq LDecl Source # 

Methods

(==) :: LDecl -> LDecl -> Bool #

(/=) :: LDecl -> LDecl -> Bool #

Show LDecl Source # 

Methods

showsPrec :: Int -> LDecl -> ShowS #

show :: LDecl -> String #

showList :: [LDecl] -> ShowS #

data LOpt Source #

Constructors

Inline 
NoInline 

Instances

Eq LOpt Source # 

Methods

(==) :: LOpt -> LOpt -> Bool #

(/=) :: LOpt -> LOpt -> Bool #

Show LOpt Source # 

Methods

showsPrec :: Int -> LOpt -> ShowS #

show :: LOpt -> String #

showList :: [LOpt] -> ShowS #

addTags :: Int -> [(Name, LDecl)] -> (Int, [(Name, LDecl)]) Source #

data LiftState Source #

Constructors

LS Name Int [(Name, LDecl)] 

liftAll :: [(Name, LDecl)] -> [(Name, LDecl)] Source #

usedArg :: (Foldable t, Eq t1) => t t1 -> t1 -> [t1] Source #

usedIn :: [Name] -> LExp -> [Name] Source #