idris-1.3.4: Functional Programming Language with Dependent Types
LicenseBSD3
MaintainerThe Idris Community.
Safe HaskellSafe-Inferred
LanguageHaskell2010

Idris.Core.Evaluate

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

convEq :: Context -> [Name] -> TT Name -> TT Name -> StateT UCs TC Bool Source #

convEq' :: Context -> [Name] -> TT Name -> TT Name -> TC Bool Source #

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

Constructors

Function !Type !Term 
TyDecl NameType !Type 
Operator Type Int ([Value] -> Maybe Value) 
CaseOp CaseInfo !Type ![(Type, Bool)] ![Either Term (Term, Term)] ![([Name], Term, Term)] !CaseDefs 

Instances

Instances details
ToJSON Def 
Instance details

Defined in IRTS.Portable

Methods

toJSON :: Def -> Value

toEncoding :: Def -> Encoding

toJSONList :: [Def] -> Value

toEncodingList :: [Def] -> Encoding

Generic Def Source # 
Instance details

Defined in Idris.Core.Evaluate

Associated Types

type Rep Def :: Type -> Type

Methods

from :: Def -> Rep Def x

to :: Rep Def x -> Def

Show Def Source # 
Instance details

Defined in Idris.Core.Evaluate

Methods

showsPrec :: Int -> Def -> ShowS

show :: Def -> String

showList :: [Def] -> ShowS

Binary Def 
Instance details

Defined in Idris.IBC

Methods

put :: Def -> Put

get :: Get Def

putList :: [Def] -> Put

NFData Def 
Instance details

Defined in Idris.Core.DeepSeq

Methods

rnf :: Def -> ()

type Rep Def Source # 
Instance details

Defined in Idris.Core.Evaluate

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

data CaseInfo Source #

Constructors

CaseInfo 

Fields

Instances

Instances details
ToJSON CaseInfo 
Instance details

Defined in IRTS.Portable

Methods

toJSON :: CaseInfo -> Value

toEncoding :: CaseInfo -> Encoding

toJSONList :: [CaseInfo] -> Value

toEncodingList :: [CaseInfo] -> Encoding

Generic CaseInfo Source # 
Instance details

Defined in Idris.Core.Evaluate

Associated Types

type Rep CaseInfo :: Type -> Type

Methods

from :: CaseInfo -> Rep CaseInfo x

to :: Rep CaseInfo x -> CaseInfo

Binary CaseInfo 
Instance details

Defined in Idris.IBC

Methods

put :: CaseInfo -> Put

get :: Get CaseInfo

putList :: [CaseInfo] -> Put

NFData CaseInfo 
Instance details

Defined in Idris.Core.DeepSeq

Methods

rnf :: CaseInfo -> ()

type Rep CaseInfo Source # 
Instance details

Defined in Idris.Core.Evaluate

type Rep CaseInfo = D1 ('MetaData "CaseInfo" "Idris.Core.Evaluate" "idris-1.3.4-3WzTclJnDGuF9nqMis99Gw" 'False) (C1 ('MetaCons "CaseInfo" 'PrefixI 'True) (S1 ('MetaSel ('Just "case_inlinable") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: (S1 ('MetaSel ('Just "case_alwaysinline") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: S1 ('MetaSel ('Just "tc_dictionary") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool))))

data CaseDefs Source #

Constructors

CaseDefs 

Fields

Instances

Instances details
ToJSON CaseDefs 
Instance details

Defined in IRTS.Portable

Methods

toJSON :: CaseDefs -> Value

toEncoding :: CaseDefs -> Encoding

toJSONList :: [CaseDefs] -> Value

toEncodingList :: [CaseDefs] -> Encoding

Generic CaseDefs Source # 
Instance details

Defined in Idris.Core.Evaluate

Associated Types

type Rep CaseDefs :: Type -> Type

Methods

from :: CaseDefs -> Rep CaseDefs x

to :: Rep CaseDefs x -> CaseDefs

Binary CaseDefs 
Instance details

Defined in Idris.IBC

Methods

put :: CaseDefs -> Put

get :: Get CaseDefs

putList :: [CaseDefs] -> Put

NFData CaseDefs 
Instance details

Defined in Idris.Core.DeepSeq

Methods

rnf :: CaseDefs -> ()

type Rep CaseDefs Source # 
Instance details

Defined in Idris.Core.Evaluate

type Rep CaseDefs = D1 ('MetaData "CaseDefs" "Idris.Core.Evaluate" "idris-1.3.4-3WzTclJnDGuF9nqMis99Gw" 'False) (C1 ('MetaCons "CaseDefs" 'PrefixI 'True) (S1 ('MetaSel ('Just "cases_compiletime") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 ([Name], SC)) :*: S1 ('MetaSel ('Just "cases_runtime") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 ([Name], SC))))

data Accessibility Source #

Constructors

Hidden 
Public 
Frozen 
Private 

Instances

Instances details
ToJSON Accessibility 
Instance details

Defined in IRTS.Portable

Methods

toJSON :: Accessibility -> Value

toEncoding :: Accessibility -> Encoding

toJSONList :: [Accessibility] -> Value

toEncodingList :: [Accessibility] -> Encoding

Generic Accessibility Source # 
Instance details

Defined in Idris.Core.Evaluate

Associated Types

type Rep Accessibility :: Type -> Type

Show Accessibility Source # 
Instance details

Defined in Idris.Core.Evaluate

Methods

showsPrec :: Int -> Accessibility -> ShowS

show :: Accessibility -> String

showList :: [Accessibility] -> ShowS

Binary Accessibility 
Instance details

Defined in Idris.IBC

Methods

put :: Accessibility -> Put

get :: Get Accessibility

putList :: [Accessibility] -> Put

NFData Accessibility 
Instance details

Defined in Idris.Core.DeepSeq

Methods

rnf :: Accessibility -> ()

Eq Accessibility Source # 
Instance details

Defined in Idris.Core.Evaluate

Ord Accessibility Source # 
Instance details

Defined in Idris.Core.Evaluate

type Rep Accessibility Source # 
Instance details

Defined in Idris.Core.Evaluate

type Rep Accessibility = D1 ('MetaData "Accessibility" "Idris.Core.Evaluate" "idris-1.3.4-3WzTclJnDGuF9nqMis99Gw" 'False) ((C1 ('MetaCons "Hidden" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Public" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "Frozen" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Private" 'PrefixI 'False) (U1 :: Type -> Type)))

type Injectivity = Bool Source #

data Totality Source #

The result of totality checking

Constructors

Total [Int]

well-founded arguments

Productive

productive

Partial PReason 
Unchecked 
Generated 

Instances

Instances details
ToJSON Totality 
Instance details

Defined in IRTS.Portable

Methods

toJSON :: Totality -> Value

toEncoding :: Totality -> Encoding

toJSONList :: [Totality] -> Value

toEncodingList :: [Totality] -> Encoding

Generic Totality Source # 
Instance details

Defined in Idris.Core.Evaluate

Associated Types

type Rep Totality :: Type -> Type

Methods

from :: Totality -> Rep Totality x

to :: Rep Totality x -> Totality

Show Totality Source # 
Instance details

Defined in Idris.Core.Evaluate

Methods

showsPrec :: Int -> Totality -> ShowS

show :: Totality -> String

showList :: [Totality] -> ShowS

Binary Totality 
Instance details

Defined in Idris.IBC

Methods

put :: Totality -> Put

get :: Get Totality

putList :: [Totality] -> Put

NFData Totality 
Instance details

Defined in Idris.Core.DeepSeq

Methods

rnf :: Totality -> ()

Eq Totality Source # 
Instance details

Defined in Idris.Core.Evaluate

Methods

(==) :: Totality -> Totality -> Bool

(/=) :: Totality -> Totality -> Bool

type Rep Totality Source # 
Instance details

Defined in Idris.Core.Evaluate

type Rep Totality = D1 ('MetaData "Totality" "Idris.Core.Evaluate" "idris-1.3.4-3WzTclJnDGuF9nqMis99Gw" 'False) ((C1 ('MetaCons "Total" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Int])) :+: C1 ('MetaCons "Productive" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "Partial" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PReason)) :+: (C1 ('MetaCons "Unchecked" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Generated" 'PrefixI 'False) (U1 :: Type -> Type))))

data PReason Source #

Reasons why a function may not be total

Instances

Instances details
Generic PReason Source # 
Instance details

Defined in Idris.Core.Evaluate

Associated Types

type Rep PReason :: Type -> Type

Methods

from :: PReason -> Rep PReason x

to :: Rep PReason x -> PReason

Show PReason Source # 
Instance details

Defined in Idris.Core.Evaluate

Methods

showsPrec :: Int -> PReason -> ShowS

show :: PReason -> String

showList :: [PReason] -> ShowS

Binary PReason 
Instance details

Defined in Idris.IBC

Methods

put :: PReason -> Put

get :: Get PReason

putList :: [PReason] -> Put

NFData PReason 
Instance details

Defined in Idris.Core.DeepSeq

Methods

rnf :: PReason -> ()

Eq PReason Source # 
Instance details

Defined in Idris.Core.Evaluate

Methods

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

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

type Rep PReason Source # 
Instance details

Defined in Idris.Core.Evaluate

type Rep PReason = D1 ('MetaData "PReason" "Idris.Core.Evaluate" "idris-1.3.4-3WzTclJnDGuF9nqMis99Gw" 'False) (((C1 ('MetaCons "Other" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Name])) :+: C1 ('MetaCons "Itself" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "NotCovering" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "NotPositive" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "UseUndef" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name)) :+: C1 ('MetaCons "ExternalIO" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "BelieveMe" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "Mutual" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Name])) :+: C1 ('MetaCons "NotProductive" 'PrefixI 'False) (U1 :: Type -> Type)))))

data MetaInformation Source #

Constructors

EmptyMI

No meta-information

DataMI [Int]

Meta information for a data declaration with position of parameters

Instances

Instances details
ToJSON MetaInformation 
Instance details

Defined in IRTS.Portable

Methods

toJSON :: MetaInformation -> Value

toEncoding :: MetaInformation -> Encoding

toJSONList :: [MetaInformation] -> Value

toEncodingList :: [MetaInformation] -> Encoding

Generic MetaInformation Source # 
Instance details

Defined in Idris.Core.Evaluate

Associated Types

type Rep MetaInformation :: Type -> Type

Show MetaInformation Source # 
Instance details

Defined in Idris.Core.Evaluate

Methods

showsPrec :: Int -> MetaInformation -> ShowS

show :: MetaInformation -> String

showList :: [MetaInformation] -> ShowS

Binary MetaInformation 
Instance details

Defined in Idris.IBC

Methods

put :: MetaInformation -> Put

get :: Get MetaInformation

putList :: [MetaInformation] -> Put

NFData MetaInformation 
Instance details

Defined in Idris.Core.DeepSeq

Methods

rnf :: MetaInformation -> ()

Eq MetaInformation Source # 
Instance details

Defined in Idris.Core.Evaluate

type Rep MetaInformation Source # 
Instance details

Defined in Idris.Core.Evaluate

type Rep MetaInformation = D1 ('MetaData "MetaInformation" "Idris.Core.Evaluate" "idris-1.3.4-3WzTclJnDGuF9nqMis99Gw" 'False) (C1 ('MetaCons "EmptyMI" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "DataMI" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Int])))

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

Instances details
Generic Context Source # 
Instance details

Defined in Idris.Core.Evaluate

Associated Types

type Rep Context :: Type -> Type

Methods

from :: Context -> Rep Context x

to :: Rep Context x -> Context

Show Context Source # 
Instance details

Defined in Idris.Core.Evaluate

Methods

showsPrec :: Int -> Context -> ShowS

show :: Context -> String

showList :: [Context] -> ShowS

NFData Context 
Instance details

Defined in Idris.Core.DeepSeq

Methods

rnf :: Context -> ()

type Rep Context Source # 
Instance details

Defined in Idris.Core.Evaluate

type Rep Context = D1 ('MetaData "Context" "Idris.Core.Evaluate" "idris-1.3.4-3WzTclJnDGuF9nqMis99Gw" 'False) (C1 ('MetaCons "MkContext" 'PrefixI 'True) (S1 ('MetaSel ('Just "next_tvar") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int) :*: S1 ('MetaSel ('Just "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 #

addOperator :: Name -> Type -> Int -> ([Value] -> Maybe Value) -> Context -> 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

lookupP_all :: Bool -> Bool -> Name -> Context -> [Term] Source #

lookupTyEnv :: Name -> Env -> Maybe (Int, RigCount, Type) Source #

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

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

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

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

conGuarded :: Context -> Name -> Term -> Bool Source #

data Value Source #

A HOAS representation of values

Instances

Instances details
Show Value Source # 
Instance details

Defined in Idris.Core.Evaluate

Methods

showsPrec :: Int -> Value -> ShowS

show :: Value -> String

showList :: [Value] -> ShowS

Eq Value Source # 
Instance details

Defined in Idris.Core.Evaluate

Methods

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

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

Quote Value Source # 
Instance details

Defined in Idris.Core.Evaluate

Methods

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

class Quote a where Source #

Methods

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

Instances

Instances details
Quote Value Source # 
Instance details

Defined in Idris.Core.Evaluate

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

isUniverse :: Term -> Bool Source #

Orphan instances

Show (a -> b) Source # 
Instance details

Methods

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

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

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