idris-1.2.0: Functional Programming Language with Dependent Types

LicenseBSD3
MaintainerThe Idris Community.
Safe HaskellNone
LanguageHaskell2010

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 #

Ord FDesc Source # 

Methods

compare :: FDesc -> FDesc -> Ordering #

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

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

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

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

max :: FDesc -> FDesc -> FDesc #

min :: FDesc -> FDesc -> FDesc #

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 #

Ord PrimFn Source # 
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-1.2.0-FcdjfAXrqrBWjK6eYRvw3" 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 "LFATan2" 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 "LCrash" PrefixI False) (U1 *)) (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 #

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

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> LAlt' e -> c (LAlt' e) #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (LAlt' e) #

toConstr :: LAlt' e -> Constr #

dataTypeOf :: LAlt' e -> DataType #

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c (LAlt' e)) #

dataCast2 :: Typeable (* -> * -> *) t => (forall d a. (Data d, Data a) => c (t d a)) -> Maybe (c (LAlt' e)) #

gmapT :: (forall b. Data b => b -> b) -> LAlt' e -> LAlt' e #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> LAlt' e -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> LAlt' e -> r #

gmapQ :: (forall d. Data d => d -> u) -> LAlt' e -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> LAlt' e -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> LAlt' e -> m (LAlt' e) #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> LAlt' e -> m (LAlt' e) #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> LAlt' e -> m (LAlt' e) #

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

Methods

compare :: LAlt' e -> LAlt' e -> Ordering #

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

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

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

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

max :: LAlt' e -> LAlt' e -> LAlt' e #

min :: LAlt' e -> LAlt' e -> LAlt' e #

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 #

Ord LDecl Source # 

Methods

compare :: LDecl -> LDecl -> Ordering #

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

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

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

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

max :: LDecl -> LDecl -> LDecl #

min :: LDecl -> LDecl -> LDecl #

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 #

Ord LOpt Source # 

Methods

compare :: LOpt -> LOpt -> Ordering #

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

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

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

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

max :: LOpt -> LOpt -> LOpt #

min :: LOpt -> LOpt -> LOpt #

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 (Maybe Name) Int [(Name, LDecl)] (Map ([Name], LExp) Name) 

renameArgs :: [Name] -> LExp -> ([Name], LExp) Source #

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

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

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

rename :: [(Name, Name)] -> LExp -> LExp Source #