Agda.Compiler.Epic.Interface

Epic interface data structure, which is serialisable and stored for each compiled file

Documentation

type Var = String

data Tag

Constructors

Tag Int

PrimTag Var

Instances

Eq Tag

Methods

(==) :: Tag -> Tag -> Bool

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

Ord Tag

Methods

compare :: Tag -> Tag -> Ordering

(<) :: Tag -> Tag -> Bool

(<=) :: Tag -> Tag -> Bool

(>) :: Tag -> Tag -> Bool

(>=) :: Tag -> Tag -> Bool

max :: Tag -> Tag -> Tag

min :: Tag -> Tag -> Tag

Show Tag

Methods

showsPrec :: Int -> Tag -> ShowS

show :: Tag -> String

showList :: [Tag] -> ShowS

data Forced

Constructors

NotForced

Forced

Instances

Eq Forced

Methods

(==) :: Forced -> Forced -> Bool

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

Show Forced

Methods

showsPrec :: Int -> Forced -> ShowS

show :: Forced -> String

showList :: [Forced] -> ShowS

pairwiseFilter :: [Bool] -> [a] -> [a]

Filter a list using a list of Bools specifying what to keep.

notForced :: ForcedArgs -> [a] -> [a]

forced :: ForcedArgs -> [a] -> [a]

data Relevance

Constructors

Irr

Rel

Instances

Eq Relevance

Methods

(==) :: Relevance -> Relevance -> Bool

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

Ord Relevance

Methods

compare :: Relevance -> Relevance -> Ordering

(<) :: Relevance -> Relevance -> Bool

(<=) :: Relevance -> Relevance -> Bool

(>) :: Relevance -> Relevance -> Bool

(>=) :: Relevance -> Relevance -> Bool

max :: Relevance -> Relevance -> Relevance

min :: Relevance -> Relevance -> Relevance

Show Relevance

Methods

showsPrec :: Int -> Relevance -> ShowS

show :: Relevance -> String

showList :: [Relevance] -> ShowS

type ForcedArgs = [Forced]

type RelevantArgs = [Relevance]

data InjectiveFun

Constructors

InjectiveFun

Fields

• injArg :: Nat
• injArity :: Nat

Instances

Eq InjectiveFun

Methods

(==) :: InjectiveFun -> InjectiveFun -> Bool

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

Show InjectiveFun

Methods

showsPrec :: Int -> InjectiveFun -> ShowS

show :: InjectiveFun -> String

showList :: [InjectiveFun] -> ShowS

data EInterface

Constructors

EInterface

Fields

• constrTags :: Map QName Tag
• definitions :: Set Var
• defDelayed :: Map QName Bool
• conArity :: Map QName Int
• mainName :: Maybe QName
• relevantArgs :: Map Var RelevantArgs
• forcedArgs :: Map QName ForcedArgs
• injectiveFuns :: Map QName InjectiveFun

Instances

Show EInterface

Methods

showsPrec :: Int -> EInterface -> ShowS

show :: EInterface -> String

showList :: [EInterface] -> ShowS

Semigroup EInterface

Methods

(<>) :: EInterface -> EInterface -> EInterface

sconcat :: NonEmpty EInterface -> EInterface

stimes :: Integral b => b -> EInterface -> EInterface

Monoid EInterface

Methods

mempty :: EInterface

mappend :: EInterface -> EInterface -> EInterface

mconcat :: [EInterface] -> EInterface