Agda-2.3.2: A dependently typed functional programming language and proof assistant

Safe Haskell | None

Agda.Compiler.Epic.Interface

Description

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

Synopsis

- type Var = String
- data Tag
  - = Tag Int
  - | PrimTag Var
- data Forced
  - = NotForced
  - | Forced
- pairwiseFilter :: [Bool] -> [a] -> [a]
- notForced :: ForcedArgs -> [a] -> [a]
- forced :: ForcedArgs -> [a] -> [a]
- data Relevance
  - = Irr
  - | Rel
- type ForcedArgs = [Forced]
- type RelevantArgs = [Relevance]
- data InjectiveFun = InjectiveFun {
  - injArg :: Nat
  - injArity :: Nat
  }
- data EInterface = EInterface {
  - 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
  }

# Documentation

type Var = String

data Tag

Constructors

Tag Int |
PrimTag Var |

Instances

Eq Tag |
Ord Tag |
Show Tag |
Typeable Tag |
EmbPrj Tag |

data Forced

Constructors

NotForced |
Forced |

Instances

Eq Forced |
Show Forced |
Typeable Forced |
EmbPrj Forced |

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 |
Ord Relevance |
Show Relevance |
Typeable Relevance |
EmbPrj Relevance |

type ForcedArgs = [Forced]

type RelevantArgs = [Relevance]

data InjectiveFun

Constructors

InjectiveFun |

Fields

injArg :: Nat
injArity :: Nat

Instances

Eq InjectiveFun |
Show InjectiveFun |
Typeable InjectiveFun |
EmbPrj InjectiveFun |

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 |
Typeable EInterface |
Monoid EInterface |
EmbPrj EInterface |