| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Wingman.Types
Contents
Synopsis
- data HoleJudgment = HoleJudgment {}
- data HoleSort
- = Hole
- | Metaprogram Text
- data UserFacingMessage
- data AgdaMatch = AgdaMatch {}
- data RunTacticResults = RunTacticResults {
- rtr_trace :: Trace
- rtr_extract :: LHsExpr GhcPs
- rtr_subgoals :: [Judgement]
- rtr_other_solns :: [Synthesized (LHsExpr GhcPs)]
- rtr_jdg :: Judgement
- rtr_ctx :: Context
- rtr_timed_out :: Bool
- newtype Rose a = Rose (Tree a)
- data Context = Context {
- ctxDefiningFuncs :: [(OccName, CType)]
- ctxModuleFuncs :: [(OccName, CType)]
- ctxConfig :: Config
- ctxInstEnvs :: InstEnvs
- ctxFamInstEnvs :: FamInstEnvs
- ctxTheta :: Set CType
- ctx_hscEnv :: HscEnv
- ctx_occEnv :: OccEnv [GlobalRdrElt]
- ctx_module :: Module
- data Synthesized a = Synthesized {
- syn_trace :: Trace
- syn_scoped :: Hypothesis CType
- syn_used_vals :: Set OccName
- syn_recursion_count :: Sum Int
- syn_val :: a
- type Trace = Rose String
- type Rule = RuleM (Synthesized (LHsExpr GhcPs))
- type RuleM = RuleT Judgement (Synthesized (LHsExpr GhcPs)) TacticError TacticState ExtractM
- type TacticsM = TacticT Judgement (Synthesized (LHsExpr GhcPs)) TacticError TacticState ExtractM
- data TacticError
- newtype ExtractM a = ExtractM {
- unExtractM :: ReaderT Context IO a
- type Judgement = Judgement' CType
- data Judgement' a = Judgement {
- _jHypothesis :: !(Hypothesis a)
- _jBlacklistDestruct :: !Bool
- _jWhitelistSplit :: !Bool
- _jIsTopHole :: !Bool
- _jGoal :: !a
- j_coercion :: TCvSubst
- data HyInfo a = HyInfo {
- hi_name :: OccName
- hi_provenance :: Provenance
- hi_type :: a
- newtype Hypothesis a = Hypothesis {
- unHypothesis :: [HyInfo a]
- newtype Uniquely a = Uniquely {
- getViaUnique :: a
- data PatVal = PatVal {}
- data DisallowReason
- data Provenance
- data TacticState = TacticState {
- ts_skolems :: !(Set TyVar)
- ts_unifier :: !TCvSubst
- ts_unique_gen :: !UniqSupply
- newtype CType = CType {}
- data Config = Config {}
- data TacticCommand
- tacticTitle :: TacticCommand -> Text -> Text
- emptyConfig :: Config
- unsafeDefaultUniqueSupply :: UniqSupply
- defaultTacticState :: TacticState
- freshUnique :: MonadState TacticState m => m Unique
- overProvenance :: (Provenance -> Provenance) -> HyInfo a -> HyInfo a
- globalHoleRef :: IORef Int
- mkMetaHoleName :: Int -> RdrName
- mapTrace :: (Trace -> Trace) -> Synthesized a -> Synthesized a
- emptyContext :: Context
- dropEveryOther :: [a] -> [a]
- rose :: (Eq a, Monoid a) => a -> [Rose a] -> Rose a
- module Wingman.Debug
- data OccName
- data Name
- data Type
- type TyVar = Var
- type Span = RealSrcSpan
Documentation
data HoleJudgment Source #
Constructors
| Hole | |
| Metaprogram Text |
data UserFacingMessage Source #
Constructors
| NotEnoughGas | |
| TacticErrors | |
| TimedOut | |
| NothingToDo | |
| InfrastructureError Text |
Instances
| Eq UserFacingMessage Source # | |
Defined in Wingman.Types Methods (==) :: UserFacingMessage -> UserFacingMessage -> Bool # (/=) :: UserFacingMessage -> UserFacingMessage -> Bool # | |
| Show UserFacingMessage Source # | |
Defined in Wingman.Types Methods showsPrec :: Int -> UserFacingMessage -> ShowS # show :: UserFacingMessage -> String # showList :: [UserFacingMessage] -> ShowS # | |
data RunTacticResults Source #
The results of runTactic
Constructors
| RunTacticResults | |
Fields
| |
Instances
| Show RunTacticResults Source # | |
Defined in Wingman.Types Methods showsPrec :: Int -> RunTacticResults -> ShowS # show :: RunTacticResults -> String # showList :: [RunTacticResults] -> ShowS # | |
Instances
| Functor Rose Source # | |
| Eq a => Eq (Rose a) Source # | |
| Data a => Data (Rose a) Source # | |
Defined in Wingman.Types Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Rose a -> c (Rose a) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Rose a) # toConstr :: Rose a -> Constr # dataTypeOf :: Rose a -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Rose a)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Rose a)) # gmapT :: (forall b. Data b => b -> b) -> Rose a -> Rose a # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Rose a -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Rose a -> r # gmapQ :: (forall d. Data d => d -> u) -> Rose a -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Rose a -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Rose a -> m (Rose a) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Rose a -> m (Rose a) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Rose a -> m (Rose a) # | |
| Show (Rose String) Source # | |
| Generic (Rose a) Source # | |
| (Eq a, Monoid a) => Semigroup (Rose a) Source # | This might not be lawful! I didn't check, and it feels sketchy. |
| (Eq a, Monoid a) => Monoid (Rose a) Source # | |
| type Rep (Rose a) Source # | |
Defined in Wingman.Types | |
The Reader context of tactics and rules
Constructors
| Context | |
Fields
| |
data Synthesized a Source #
The extract for refinery. Represents a "synthesized attribute" in the
context of attribute grammars. In essence, Synthesized describes
information we'd like to pass from leaves of the tactics search upwards.
This includes the actual AST we've generated (in syn_val).
Constructors
| Synthesized | |
Fields
| |
Instances
type RuleM = RuleT Judgement (Synthesized (LHsExpr GhcPs)) TacticError TacticState ExtractM Source #
type TacticsM = TacticT Judgement (Synthesized (LHsExpr GhcPs)) TacticError TacticState ExtractM Source #
data TacticError Source #
Reasons a tactic might fail.
Constructors
| OutOfGas | |
| GoalMismatch String CType | |
| NoProgress | |
| NoApplicableTactic | |
| UnhelpfulRecursion | |
| UnhelpfulDestruct OccName | |
| TooPolymorphic | |
| NotInScope OccName | |
| TacticPanic String |
Instances
| Eq TacticError Source # | |
Defined in Wingman.Types | |
| Show TacticError Source # | |
Defined in Wingman.Types Methods showsPrec :: Int -> TacticError -> ShowS # show :: TacticError -> String # showList :: [TacticError] -> ShowS # | |
| MonadExtract Int (Synthesized (LHsExpr GhcPs)) TacticError TacticState ExtractM Source # | |
Defined in Wingman.Types Methods hole :: StateT TacticState ExtractM (Int, Synthesized (LHsExpr GhcPs)) # unsolvableHole :: TacticError -> StateT TacticState ExtractM (Int, Synthesized (LHsExpr GhcPs)) # | |
Constructors
| ExtractM | |
Fields
| |
Instances
| Monad ExtractM Source # | |
| Functor ExtractM Source # | |
| Applicative ExtractM Source # | |
| MonadReader Context ExtractM Source # | |
| MonadExtract Int (Synthesized (LHsExpr GhcPs)) TacticError TacticState ExtractM Source # | |
Defined in Wingman.Types Methods hole :: StateT TacticState ExtractM (Int, Synthesized (LHsExpr GhcPs)) # unsolvableHole :: TacticError -> StateT TacticState ExtractM (Int, Synthesized (LHsExpr GhcPs)) # | |
type Judgement = Judgement' CType Source #
data Judgement' a Source #
The current bindings and goal for a hole to be filled by refinery.
Constructors
| Judgement | |
Fields
| |
Instances
The provenance and type of a hypothesis term.
Constructors
| HyInfo | |
Fields
| |
Instances
| Functor HyInfo Source # | |
| Eq a => Eq (HyInfo a) Source # | |
| Data a => Data (HyInfo a) Source # | |
Defined in Wingman.Types Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> HyInfo a -> c (HyInfo a) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (HyInfo a) # toConstr :: HyInfo a -> Constr # dataTypeOf :: HyInfo a -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (HyInfo a)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (HyInfo a)) # gmapT :: (forall b. Data b => b -> b) -> HyInfo a -> HyInfo a # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> HyInfo a -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> HyInfo a -> r # gmapQ :: (forall d. Data d => d -> u) -> HyInfo a -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> HyInfo a -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> HyInfo a -> m (HyInfo a) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> HyInfo a -> m (HyInfo a) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> HyInfo a -> m (HyInfo a) # | |
| Ord a => Ord (HyInfo a) Source # | |
Defined in Wingman.Types | |
| Show a => Show (HyInfo a) Source # | |
| Generic (HyInfo a) Source # | |
| type Rep (HyInfo a) Source # | |
Defined in Wingman.Types type Rep (HyInfo a) = D1 ('MetaData "HyInfo" "Wingman.Types" "hls-tactics-plugin-1.6.2.0-F0S9kfzWGRh6ZnCEvC7DkD" 'False) (C1 ('MetaCons "HyInfo" 'PrefixI 'True) (S1 ('MetaSel ('Just "hi_name") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 OccName) :*: (S1 ('MetaSel ('Just "hi_provenance") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Provenance) :*: S1 ('MetaSel ('Just "hi_type") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a)))) | |
newtype Hypothesis a Source #
Constructors
| Hypothesis | |
Fields
| |
Instances
| Functor Hypothesis Source # | |
Defined in Wingman.Types Methods fmap :: (a -> b) -> Hypothesis a -> Hypothesis b # (<$) :: a -> Hypothesis b -> Hypothesis a # | |
| Eq a => Eq (Hypothesis a) Source # | |
Defined in Wingman.Types | |
| Data a => Data (Hypothesis a) Source # | |
Defined in Wingman.Types Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Hypothesis a -> c (Hypothesis a) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Hypothesis a) # toConstr :: Hypothesis a -> Constr # dataTypeOf :: Hypothesis a -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Hypothesis a)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Hypothesis a)) # gmapT :: (forall b. Data b => b -> b) -> Hypothesis a -> Hypothesis a # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Hypothesis a -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Hypothesis a -> r # gmapQ :: (forall d. Data d => d -> u) -> Hypothesis a -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Hypothesis a -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Hypothesis a -> m (Hypothesis a) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Hypothesis a -> m (Hypothesis a) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Hypothesis a -> m (Hypothesis a) # | |
| Ord a => Ord (Hypothesis a) Source # | |
Defined in Wingman.Types Methods compare :: Hypothesis a -> Hypothesis a -> Ordering # (<) :: Hypothesis a -> Hypothesis a -> Bool # (<=) :: Hypothesis a -> Hypothesis a -> Bool # (>) :: Hypothesis a -> Hypothesis a -> Bool # (>=) :: Hypothesis a -> Hypothesis a -> Bool # max :: Hypothesis a -> Hypothesis a -> Hypothesis a # min :: Hypothesis a -> Hypothesis a -> Hypothesis a # | |
| Show a => Show (Hypothesis a) Source # | |
Defined in Wingman.Types Methods showsPrec :: Int -> Hypothesis a -> ShowS # show :: Hypothesis a -> String # showList :: [Hypothesis a] -> ShowS # | |
| Generic (Hypothesis a) Source # | |
Defined in Wingman.Types Associated Types type Rep (Hypothesis a) :: Type -> Type # | |
| Semigroup (Hypothesis a) Source # | |
Defined in Wingman.Types Methods (<>) :: Hypothesis a -> Hypothesis a -> Hypothesis a # sconcat :: NonEmpty (Hypothesis a) -> Hypothesis a # stimes :: Integral b => b -> Hypothesis a -> Hypothesis a # | |
| Monoid (Hypothesis a) Source # | |
Defined in Wingman.Types Methods mempty :: Hypothesis a # mappend :: Hypothesis a -> Hypothesis a -> Hypothesis a # mconcat :: [Hypothesis a] -> Hypothesis a # | |
| type Rep (Hypothesis a) Source # | |
Defined in Wingman.Types type Rep (Hypothesis a) = D1 ('MetaData "Hypothesis" "Wingman.Types" "hls-tactics-plugin-1.6.2.0-F0S9kfzWGRh6ZnCEvC7DkD" 'True) (C1 ('MetaCons "Hypothesis" 'PrefixI 'True) (S1 ('MetaSel ('Just "unHypothesis") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [HyInfo a]))) | |
Constructors
| Uniquely | |
Fields
| |
Instances
| Uniquable a => Eq (Uniquely a) Source # | |
| Data a => Data (Uniquely a) Source # | |
Defined in Wingman.Types Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Uniquely a -> c (Uniquely a) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Uniquely a) # toConstr :: Uniquely a -> Constr # dataTypeOf :: Uniquely a -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Uniquely a)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Uniquely a)) # gmapT :: (forall b. Data b => b -> b) -> Uniquely a -> Uniquely a # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Uniquely a -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Uniquely a -> r # gmapQ :: (forall d. Data d => d -> u) -> Uniquely a -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Uniquely a -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Uniquely a -> m (Uniquely a) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Uniquely a -> m (Uniquely a) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Uniquely a -> m (Uniquely a) # | |
| Uniquable a => Ord (Uniquely a) Source # | |
| Show a => Show (Uniquely a) Source # | |
Provenance of a pattern value.
Constructors
| PatVal | |
Fields
| |
Instances
| Eq PatVal Source # | |
| Data PatVal Source # | |
Defined in Wingman.Types Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> PatVal -> c PatVal # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c PatVal # toConstr :: PatVal -> Constr # dataTypeOf :: PatVal -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c PatVal) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c PatVal) # gmapT :: (forall b. Data b => b -> b) -> PatVal -> PatVal # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> PatVal -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> PatVal -> r # gmapQ :: (forall d. Data d => d -> u) -> PatVal -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> PatVal -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> PatVal -> m PatVal # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> PatVal -> m PatVal # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> PatVal -> m PatVal # | |
| Ord PatVal Source # | |
| Show PatVal Source # | |
| Generic PatVal Source # | |
| type Rep PatVal Source # | |
Defined in Wingman.Types type Rep PatVal = D1 ('MetaData "PatVal" "Wingman.Types" "hls-tactics-plugin-1.6.2.0-F0S9kfzWGRh6ZnCEvC7DkD" 'False) (C1 ('MetaCons "PatVal" 'PrefixI 'True) ((S1 ('MetaSel ('Just "pv_scrutinee") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe OccName)) :*: S1 ('MetaSel ('Just "pv_ancestry") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Set OccName))) :*: (S1 ('MetaSel ('Just "pv_datacon") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Uniquely ConLike)) :*: S1 ('MetaSel ('Just "pv_position") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int)))) | |
data DisallowReason Source #
Why was a hypothesis disallowed?
Constructors
| WrongBranch Int | |
| Shadowed | |
| RecursiveCall | |
| AlreadyDestructed |
Instances
data Provenance Source #
Describes where hypotheses came from. Used extensively to prune stupid solutions from the search space.
Constructors
| TopLevelArgPrv | An argument given to the topmost function that contains the current hole. Recursive calls are restricted to values whose provenance lines up with the same argument. |
| PatternMatchPrv PatVal | |
| ClassMethodPrv (Uniquely Class) | Class | A binding explicitly written by the user. |
| UserPrv | |
| ImportPrv | A binding explicitly imported by the user. |
| RecursivePrv | The recursive hypothesis. Present only in the context of the recursion tactic. |
| DisallowedPrv DisallowReason Provenance | A hypothesis which has been disallowed for some reason. It's important to keep these in the hypothesis set, rather than filtering it, in order to continue tracking downstream provenance. |
Instances
data TacticState Source #
The state that should be shared between subgoals. Extracts move towards the root, judgments move towards the leaves, and the state moves *sideways*.
Constructors
| TacticState | |
Fields
| |
Instances
A wrapper around Type which supports equality and ordering.
Instances
| Eq CType Source # | |
| Data CType Source # | |
Defined in Wingman.Types Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> CType -> c CType # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c CType # dataTypeOf :: CType -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c CType) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c CType) # gmapT :: (forall b. Data b => b -> b) -> CType -> CType # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> CType -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> CType -> r # gmapQ :: (forall d. Data d => d -> u) -> CType -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> CType -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> CType -> m CType # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> CType -> m CType # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> CType -> m CType # | |
| Ord CType Source # | |
| Show CType Source # | |
Plugin configuration for tactics
Constructors
| Config | |
Fields | |
data TacticCommand Source #
The list of tactics exposed to the outside world. These are attached to
actual tactics via commandTactic and are contextually provided to the
editor via commandProvider.
Constructors
| Auto | |
| Intros | |
| IntroAndDestruct | |
| Destruct | |
| DestructPun | |
| Homomorphism | |
| DestructLambdaCase | |
| HomomorphismLambdaCase | |
| DestructAll | |
| UseDataCon | |
| Refine | |
| BeginMetaprogram | |
| RunMetaprogram |
Instances
tacticTitle :: TacticCommand -> Text -> Text Source #
Generate a title for the command.
emptyConfig :: Config Source #
unsafeDefaultUniqueSupply :: UniqSupply Source #
A UniqSupply to use in defaultTacticState
freshUnique :: MonadState TacticState m => m Unique Source #
Generate a new Unique
overProvenance :: (Provenance -> Provenance) -> HyInfo a -> HyInfo a Source #
Map a function over the provenance.
globalHoleRef :: IORef Int Source #
Used to ensure hole names are unique across invocations of runTactic
mkMetaHoleName :: Int -> RdrName Source #
mapTrace :: (Trace -> Trace) -> Synthesized a -> Synthesized a Source #
emptyContext :: Context Source #
An empty context
dropEveryOther :: [a] -> [a] Source #
module Wingman.Debug
Occurrence Name
In this context that means: "classified (i.e. as a type name, value name, etc) but not qualified and not yet resolved"
Instances
| Eq OccName | |
| Data OccName | |
Defined in OccName Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> OccName -> c OccName # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c OccName # toConstr :: OccName -> Constr # dataTypeOf :: OccName -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c OccName) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c OccName) # gmapT :: (forall b. Data b => b -> b) -> OccName -> OccName # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> OccName -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> OccName -> r # gmapQ :: (forall d. Data d => d -> u) -> OccName -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> OccName -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> OccName -> m OccName # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> OccName -> m OccName # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> OccName -> m OccName # | |
| Ord OccName | |
| NFData OccName | |
| HasOccName OccName | |
| Binary OccName | |
| Uniquable OccName | |
| Outputable OccName | |
| OutputableBndr OccName | |
Defined in OccName Methods pprBndr :: BindingSite -> OccName -> SDoc # pprPrefixOcc :: OccName -> SDoc # pprInfixOcc :: OccName -> SDoc # bndrIsJoin_maybe :: OccName -> Maybe Int # | |
A unique, unambiguous name for something, containing information about where that thing originated.
Instances
| Eq Name | |
| Data Name | |
Defined in Name Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Name -> c Name # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Name # dataTypeOf :: Name -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Name) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Name) # gmapT :: (forall b. Data b => b -> b) -> Name -> Name # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Name -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Name -> r # gmapQ :: (forall d. Data d => d -> u) -> Name -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Name -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Name -> m Name # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Name -> m Name # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Name -> m Name # | |
| Ord Name | Caution: This instance is implemented via See |
| Show Name Source # | |
| NFData Name | |
| NamedThing Name | |
| HasOccName Name | |
| Binary Name | Assumes that the |
| Uniquable Name | |
| HasSrcSpan Name | |
Defined in Name Methods composeSrcSpan :: Located (SrcSpanLess Name) -> Name # decomposeSrcSpan :: Name -> Located (SrcSpanLess Name) # | |
| Outputable Name | |
| OutputableBndr Name | |
Defined in Name Methods pprBndr :: BindingSite -> Name -> SDoc # pprPrefixOcc :: Name -> SDoc # pprInfixOcc :: Name -> SDoc # bndrIsJoin_maybe :: Name -> Maybe Int # | |
| type SrcSpanLess Name | |
Defined in Name | |
Instances
| Data Type | |
Defined in TyCoRep Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Type -> c Type # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Type # dataTypeOf :: Type -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Type) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Type) # gmapT :: (forall b. Data b => b -> b) -> Type -> Type # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Type -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Type -> r # gmapQ :: (forall d. Data d => d -> u) -> Type -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Type -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Type -> m Type # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Type -> m Type # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Type -> m Type # | |
| Show Type Source # | |
| Outputable Type | |
| Eq (DeBruijn Type) | |
type Span = RealSrcSpan #
Orphan instances
| Show TCvSubst Source # | |
| Show Class Source # | |
| Show ConLike Source # | |
| Show DataCon Source # | |
| Show Type Source # | |
| Show Var Source # | |
| Show UniqSupply Source # | |
Methods showsPrec :: Int -> UniqSupply -> ShowS # show :: UniqSupply -> String # showList :: [UniqSupply] -> ShowS # | |
| Show LexicalFixity Source # | |
Methods showsPrec :: Int -> LexicalFixity -> ShowS # show :: LexicalFixity -> String # showList :: [LexicalFixity] -> ShowS # | |
| Show TyCon Source # | |
| Show Name Source # | |
| MonadReader r m => MonadReader r (RuleT jdg ext err s m) Source # | |
| MonadReader r m => MonadReader r (TacticT jdg ext err s m) Source # | |
| Show (HsDecl GhcPs) Source # | |
| Show (LHsSigType GhcPs) Source # | |
| Show (HsExpr GhcPs) Source # | |
| Show (HsExpr GhcTc) Source # | |
| Show (Pat GhcPs) Source # | |