Safe Haskell | None |
---|---|
Language | Haskell2010 |
CoAxiom
Description
Module for coercion axioms, used to represent type family instances and newtypes
- data BranchFlag
- type Branched = Branched
- type Unbranched = Unbranched
- type BranchIndex = Int
- data Branches br
- manyBranches :: [CoAxBranch] -> Branches Branched
- unbranched :: CoAxBranch -> Branches Unbranched
- fromBranches :: Branches br -> [CoAxBranch]
- numBranches :: Branches br -> Int
- mapAccumBranches :: ([CoAxBranch] -> CoAxBranch -> CoAxBranch) -> Branches br -> Branches br
- data CoAxiom br = CoAxiom {
- co_ax_unique :: Unique
- co_ax_name :: Name
- co_ax_role :: Role
- co_ax_tc :: TyCon
- co_ax_branches :: Branches br
- co_ax_implicit :: Bool
- data CoAxBranch = CoAxBranch {}
- toBranchedAxiom :: CoAxiom br -> CoAxiom Branched
- toUnbranchedAxiom :: CoAxiom br -> CoAxiom Unbranched
- coAxiomName :: CoAxiom br -> Name
- coAxiomArity :: CoAxiom br -> BranchIndex -> Arity
- coAxiomBranches :: CoAxiom br -> Branches br
- coAxiomTyCon :: CoAxiom br -> TyCon
- isImplicitCoAxiom :: CoAxiom br -> Bool
- coAxiomNumPats :: CoAxiom br -> Int
- coAxiomNthBranch :: CoAxiom br -> BranchIndex -> CoAxBranch
- coAxiomSingleBranch_maybe :: CoAxiom br -> Maybe CoAxBranch
- coAxiomRole :: CoAxiom br -> Role
- coAxiomSingleBranch :: CoAxiom Unbranched -> CoAxBranch
- coAxBranchTyVars :: CoAxBranch -> [TyVar]
- coAxBranchCoVars :: CoAxBranch -> [CoVar]
- coAxBranchRoles :: CoAxBranch -> [Role]
- coAxBranchLHS :: CoAxBranch -> [Type]
- coAxBranchRHS :: CoAxBranch -> Type
- coAxBranchSpan :: CoAxBranch -> SrcSpan
- coAxBranchIncomps :: CoAxBranch -> [CoAxBranch]
- placeHolderIncomps :: [CoAxBranch]
- data Role
- fsFromRole :: Role -> FastString
- data CoAxiomRule = CoAxiomRule {
- coaxrName :: FastString
- coaxrAsmpRoles :: [Role]
- coaxrRole :: Role
- coaxrProves :: [Eqn] -> Maybe Eqn
- type Eqn = Pair Type
- data BuiltInSynFamily = BuiltInSynFamily {
- sfMatchFam :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
- sfInteractTop :: [Type] -> Type -> [Eqn]
- sfInteractInert :: [Type] -> Type -> [Type] -> Type -> [Eqn]
- trivialBuiltInFamily :: BuiltInSynFamily
Documentation
data BranchFlag Source
type Unbranched = Unbranched Source
type BranchIndex = Int Source
manyBranches :: [CoAxBranch] -> Branches Branched Source
fromBranches :: Branches br -> [CoAxBranch] Source
numBranches :: Branches br -> Int Source
mapAccumBranches :: ([CoAxBranch] -> CoAxBranch -> CoAxBranch) -> Branches br -> Branches br Source
The [CoAxBranch]
passed into the mapping function is a list of
all previous branches, reversed
A CoAxiom
is a "coercion constructor", i.e. a named equality axiom.
Constructors
CoAxiom | |
Fields
|
Instances
Eq (CoAxiom br) | |
Typeable BranchFlag br => Data (CoAxiom br) | |
Ord (CoAxiom br) | |
Outputable (CoAxiom br) | |
Uniquable (CoAxiom br) | |
NamedThing (CoAxiom br) | |
toBranchedAxiom :: CoAxiom br -> CoAxiom Branched Source
toUnbranchedAxiom :: CoAxiom br -> CoAxiom Unbranched Source
coAxiomName :: CoAxiom br -> Name Source
coAxiomArity :: CoAxiom br -> BranchIndex -> Arity Source
coAxiomBranches :: CoAxiom br -> Branches br Source
coAxiomTyCon :: CoAxiom br -> TyCon Source
isImplicitCoAxiom :: CoAxiom br -> Bool Source
coAxiomNumPats :: CoAxiom br -> Int Source
coAxiomNthBranch :: CoAxiom br -> BranchIndex -> CoAxBranch Source
coAxiomRole :: CoAxiom br -> Role Source
coAxBranchTyVars :: CoAxBranch -> [TyVar] Source
coAxBranchCoVars :: CoAxBranch -> [CoVar] Source
coAxBranchRoles :: CoAxBranch -> [Role] Source
coAxBranchLHS :: CoAxBranch -> [Type] Source
coAxBranchRHS :: CoAxBranch -> Type Source
coAxBranchIncomps :: CoAxBranch -> [CoAxBranch] Source
Constructors
Nominal | |
Representational | |
Phantom |
fsFromRole :: Role -> FastString Source
data CoAxiomRule Source
For now, we work only with nominal equality.
Constructors
CoAxiomRule | |
Fields
|
data BuiltInSynFamily Source
Constructors
BuiltInSynFamily | |
Fields
|