idris-1.3.0: Functional Programming Language with Dependent Types

LicenseBSD3
MaintainerThe Idris Community.
Safe HaskellNone
LanguageHaskell2010

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 lets

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

Like simplify, but we only reduce functions that are marked as okay to inline, and don't reduce lets

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

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

Unfold the given names in a term, the given number of times in a stack. Preserves 'let'. This is primarily to support inlining of the given names, and can also help with partial evaluation by allowing a rescursive definition to be unfolded once only. Specifically used to unfold definitions using interfaces before going to the totality checker (otherwise mutually recursive definitions in implementations will not work...)

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-1.3.0-sWdxO7YG1l525W5zQFBm8" 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-1.3.0-sWdxO7YG1l525W5zQFBm8" 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-1.3.0-sWdxO7YG1l525W5zQFBm8" False) (C1 * (MetaCons "CaseDefs" PrefixI True) ((:*:) * (S1 * (MetaSel (Just Symbol "cases_compiletime") 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-1.3.0-sWdxO7YG1l525W5zQFBm8" 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-1.3.0-sWdxO7YG1l525W5zQFBm8" 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. Also store maximum RigCount of the name (can't bind a name at multiplicity 1 in a RigW, for example)

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-1.3.0-sWdxO7YG1l525W5zQFBm8" 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 TTDecl)))))

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)] -> 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

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 #