idris-0.12.2: Functional Programming Language with Dependent Types

CopyrightLicense : BSD3
MaintainerThe Idris Community.
Safe HaskellNone
LanguageHaskell98

Idris.Core.Evaluate

Contents

Description

 

Synopsis

Documentation

normaliseC :: Context -> Env -> TT Name -> TT Name Source #

Normalise fully type checked terms (so, assume all names/let bindings resolved)

normaliseAll :: Context -> Env -> TT Name -> TT Name Source #

Normalise everything, whether abstract, private or public

normaliseBlocking :: Context -> Env -> [Name] -> TT Name -> TT Name Source #

As normaliseAll, but with an explicit list of names *not* to reduce

rt_simplify :: Context -> Env -> TT Name -> TT Name Source #

Simplify for run-time (i.e. basic inlining)

simplify :: Context -> Env -> TT Name -> TT Name Source #

Like normalise, but we only reduce functions that are marked as okay to inline (and probably shouldn't reduce lets?) 20130908: now only used to reduce for totality checking. Inlining should be done elsewhere.

specialise :: Context -> Env -> [(Name, Int)] -> TT Name -> (TT Name, [(Name, Int)]) Source #

hnf :: Context -> Env -> TT Name -> TT Name Source #

Reduce a term to head normal form

data Def Source #

A definition is either a simple function (just an expression with a type), a constant, which could be a data or type constructor, an axiom or as an yet undefined function, or an Operator. An Operator is a function which explains how to reduce. A CaseOp is a function defined by a simple case tree

Instances

Show Def Source # 

Methods

showsPrec :: Int -> Def -> ShowS #

show :: Def -> String #

showList :: [Def] -> ShowS #

Generic Def Source # 

Associated Types

type Rep Def :: * -> * #

Methods

from :: Def -> Rep Def x #

to :: Rep Def x -> Def #

type Rep Def Source # 
type Rep Def = D1 (MetaData "Def" "Idris.Core.Evaluate" "idris-0.12.2-B6CfTCKeTUh4MfL5ICL0mo" False) ((:+:) ((:+:) (C1 (MetaCons "Function" PrefixI False) ((:*:) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 Type)) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 Term)))) (C1 (MetaCons "TyDecl" PrefixI False) ((:*:) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 NameType)) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 Type))))) ((:+:) (C1 (MetaCons "Operator" PrefixI False) ((:*:) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Type)) ((:*:) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Int)) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 ([Value] -> Maybe Value)))))) (C1 (MetaCons "CaseOp" PrefixI False) ((:*:) ((:*:) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 CaseInfo)) ((:*:) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 Type)) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 [(Type, Bool)])))) ((:*:) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 [Either Term (Term, Term)])) ((:*:) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 [([Name], Term, Term)])) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 CaseDefs))))))))

data CaseInfo Source #

Instances

Generic CaseInfo Source # 

Associated Types

type Rep CaseInfo :: * -> * #

Methods

from :: CaseInfo -> Rep CaseInfo x #

to :: Rep CaseInfo x -> CaseInfo #

type Rep CaseInfo Source # 
type Rep CaseInfo = D1 (MetaData "CaseInfo" "Idris.Core.Evaluate" "idris-0.12.2-B6CfTCKeTUh4MfL5ICL0mo" False) (C1 (MetaCons "CaseInfo" PrefixI True) ((:*:) (S1 (MetaSel (Just Symbol "case_inlinable") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Bool)) ((:*:) (S1 (MetaSel (Just Symbol "case_alwaysinline") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Bool)) (S1 (MetaSel (Just Symbol "tc_dictionary") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Bool)))))

data CaseDefs Source #

Constructors

CaseDefs 

Fields

Instances

Generic CaseDefs Source # 

Associated Types

type Rep CaseDefs :: * -> * #

Methods

from :: CaseDefs -> Rep CaseDefs x #

to :: Rep CaseDefs x -> CaseDefs #

type Rep CaseDefs Source # 
type Rep CaseDefs = D1 (MetaData "CaseDefs" "Idris.Core.Evaluate" "idris-0.12.2-B6CfTCKeTUh4MfL5ICL0mo" False) (C1 (MetaCons "CaseDefs" PrefixI True) ((:*:) ((:*:) (S1 (MetaSel (Just Symbol "cases_totcheck") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 ([Name], SC))) (S1 (MetaSel (Just Symbol "cases_compiletime") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 ([Name], SC)))) ((:*:) (S1 (MetaSel (Just Symbol "cases_inlined") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 ([Name], SC))) (S1 (MetaSel (Just Symbol "cases_runtime") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 ([Name], SC))))))

data Totality Source #

The result of totality checking

Constructors

Total [Int]

well-founded arguments

Productive

productive

Partial PReason 
Unchecked 
Generated 

Instances

Eq Totality Source # 
Show Totality Source # 
Generic Totality Source # 

Associated Types

type Rep Totality :: * -> * #

Methods

from :: Totality -> Rep Totality x #

to :: Rep Totality x -> Totality #

type Rep Totality Source # 
type Rep Totality = D1 (MetaData "Totality" "Idris.Core.Evaluate" "idris-0.12.2-B6CfTCKeTUh4MfL5ICL0mo" False) ((:+:) ((:+:) (C1 (MetaCons "Total" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [Int]))) (C1 (MetaCons "Productive" PrefixI False) U1)) ((:+:) (C1 (MetaCons "Partial" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 PReason))) ((:+:) (C1 (MetaCons "Unchecked" PrefixI False) U1) (C1 (MetaCons "Generated" PrefixI False) U1))))

data PReason Source #

Reasons why a function may not be total

Instances

Eq PReason Source # 

Methods

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

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

Show PReason Source # 
Generic PReason Source # 

Associated Types

type Rep PReason :: * -> * #

Methods

from :: PReason -> Rep PReason x #

to :: Rep PReason x -> PReason #

type Rep PReason Source # 
type Rep PReason = D1 (MetaData "PReason" "Idris.Core.Evaluate" "idris-0.12.2-B6CfTCKeTUh4MfL5ICL0mo" False) ((:+:) ((:+:) ((:+:) (C1 (MetaCons "Other" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [Name]))) (C1 (MetaCons "Itself" PrefixI False) U1)) ((:+:) (C1 (MetaCons "NotCovering" PrefixI False) U1) (C1 (MetaCons "NotPositive" PrefixI False) U1))) ((:+:) ((:+:) (C1 (MetaCons "UseUndef" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Name))) (C1 (MetaCons "ExternalIO" PrefixI False) U1)) ((:+:) (C1 (MetaCons "BelieveMe" PrefixI False) U1) ((:+:) (C1 (MetaCons "Mutual" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [Name]))) (C1 (MetaCons "NotProductive" PrefixI False) U1)))))

data MetaInformation Source #

Constructors

EmptyMI

No meta-information

DataMI [Int]

Meta information for a data declaration with position of parameters

data Context Source #

Contexts used for global definitions and for proof state. They contain universe constraints and existing definitions.

Instances

Show Context Source # 
Generic Context Source # 

Associated Types

type Rep Context :: * -> * #

Methods

from :: Context -> Rep Context x #

to :: Rep Context x -> Context #

type Rep Context Source # 
type Rep Context = D1 (MetaData "Context" "Idris.Core.Evaluate" "idris-0.12.2-B6CfTCKeTUh4MfL5ICL0mo" False) (C1 (MetaCons "MkContext" PrefixI True) ((:*:) (S1 (MetaSel (Just Symbol "next_tvar") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Int)) (S1 (MetaSel (Just Symbol "definitions") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Ctxt (Def, Injectivity, Accessibility, Totality, MetaInformation))))))

initContext :: Context Source #

The initial empty context

ctxtAlist :: Context -> [(Name, Def)] Source #

Get the definitions from a context

addCasedef :: Name -> ErasureInfo -> CaseInfo -> Bool -> SC -> Bool -> Bool -> [(Type, Bool)] -> [Int] -> [Either Term (Term, Term)] -> [([Name], Term, Term)] -> [([Name], Term, Term)] -> [([Name], Term, Term)] -> [([Name], Term, Term)] -> Type -> Context -> TC Context Source #

lookupTyName :: Name -> Context -> [(Name, Type)] Source #

Get the list of pairs of fully-qualified names and their types that match some name

lookupTyNameExact :: Name -> Context -> Maybe (Name, Type) Source #

Get the pair of a fully-qualified name and its type, if there is a unique one matching the name used as a key.

lookupTy :: Name -> Context -> [Type] Source #

Get the types that match some name

lookupTyExact :: Name -> Context -> Maybe Type Source #

Get the single type that matches some name precisely

isCanonical :: Type -> Context -> Bool Source #

Return true if the given type is a concrete type familyor primitive False it it's a function to compute a type or a variable

isDConName :: Name -> Context -> Bool Source #

Check whether a resolved name is certainly a data constructor

canBeDConName :: Name -> Context -> Bool Source #

Check whether any overloading of a name is a data constructor

data Value Source #

A HOAS representation of values

Instances

Eq Value Source # 

Methods

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

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

Show Value Source # 

Methods

showsPrec :: Int -> Value -> ShowS #

show :: Value -> String #

showList :: [Value] -> ShowS #

Quote Value Source # 

Methods

quote :: Int -> Value -> Eval (TT Name) Source #

class Quote a where Source #

Minimal complete definition

quote

Methods

quote :: Int -> a -> Eval (TT Name) Source #

Instances

Quote Value Source # 

Methods

quote :: Int -> Value -> Eval (TT Name) Source #

initEval :: EvalState Source #

uniqueNameCtxt :: Context -> Name -> [Name] -> Name Source #

Create a unique name given context and other existing names

Orphan instances

Show (a -> b) Source # 

Methods

showsPrec :: Int -> (a -> b) -> ShowS #

show :: (a -> b) -> String #

showList :: [a -> b] -> ShowS #