Safe Haskell | None |
---|---|
Language | Haskell2010 |
Synopsis
- data UserFacingMessage
- data AgdaMatch = AgdaMatch {}
- data RunTacticResults = RunTacticResults {
- rtr_trace :: Trace
- rtr_extract :: LHsExpr GhcPs
- rtr_other_solns :: [Synthesized (LHsExpr GhcPs)]
- rtr_jdg :: Judgement
- rtr_ctx :: Context
- newtype Rose a = Rose (Tree a)
- data KnownThings = KnownThings {
- kt_semigroup :: Class
- kt_monoid :: Class
- data Context = Context {
- ctxDefiningFuncs :: [(OccName, CType)]
- ctxModuleFuncs :: [(OccName, CType)]
- ctxFeatureSet :: FeatureSet
- ctxKnownThings :: KnownThings
- ctxInstEnvs :: InstEnvs
- ctxTheta :: Set CType
- 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
- = UndefinedHypothesis OccName
- | GoalMismatch String CType
- | UnsolvedSubgoals [Judgement]
- | UnificationError CType CType
- | NoProgress
- | NoApplicableTactic
- | IncorrectDataCon DataCon
- | RecursionOnWrongParam OccName Int OccName
- | UnhelpfulDestruct OccName
- | UnhelpfulSplit OccName
- | TooPolymorphic
- | NotInScope OccName
- newtype ExtractM a = ExtractM {
- unExtractM :: Reader Context a
- type Judgement = Judgement' CType
- data Judgement' a = Judgement {
- _jHypothesis :: !(Hypothesis a)
- _jBlacklistDestruct :: !Bool
- _jWhitelistSplit :: !Bool
- _jIsTopHole :: !Bool
- _jGoal :: !a
- 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
- unsafeDefaultUniqueSupply :: UniqSupply
- defaultTacticState :: TacticState
- freshUnique :: MonadState TacticState m => m Unique
- overProvenance :: (Provenance -> Provenance) -> HyInfo a -> HyInfo a
- 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 UserFacingMessage Source #
Instances
Eq UserFacingMessage Source # | |
Defined in Wingman.Types (==) :: UserFacingMessage -> UserFacingMessage -> Bool # (/=) :: UserFacingMessage -> UserFacingMessage -> Bool # | |
Show UserFacingMessage Source # | |
Defined in Wingman.Types showsPrec :: Int -> UserFacingMessage -> ShowS # show :: UserFacingMessage -> String # showList :: [UserFacingMessage] -> ShowS # |
data RunTacticResults Source #
The results of runTactic
RunTacticResults | |
|
Instances
Show RunTacticResults Source # | |
Defined in Wingman.Types showsPrec :: Int -> RunTacticResults -> ShowS # show :: RunTacticResults -> String # showList :: [RunTacticResults] -> ShowS # |
Instances
Functor Rose Source # | |
Eq a => Eq (Rose a) Source # | |
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 |
data KnownThings Source #
Things we'd like to look up, that don't exist in TysWiredIn.
The Reader context of tactics and rules
Context | |
|
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
).
Synthesized | |
|
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.
Instances
Eq TacticError Source # | |
Defined in Wingman.Types (==) :: TacticError -> TacticError -> Bool # (/=) :: TacticError -> TacticError -> Bool # | |
Show TacticError Source # | |
Defined in Wingman.Types showsPrec :: Int -> TacticError -> ShowS # show :: TacticError -> String # showList :: [TacticError] -> ShowS # |
ExtractM | |
|
Instances
Monad ExtractM Source # | |
Functor ExtractM Source # | |
Applicative ExtractM Source # | |
MonadReader Context ExtractM Source # | |
MonadExtract (Synthesized (LHsExpr GhcPs)) ExtractM Source # | Orphan instance for producing holes when attempting to solve tactics. |
Defined in Wingman.Types |
type Judgement = Judgement' CType Source #
data Judgement' a Source #
The current bindings and goal for a hole to be filled by refinery.
Judgement | |
|
Instances
The provenance and type of a hypothesis term.
HyInfo | |
|
Instances
Functor HyInfo Source # | |
Eq a => Eq (HyInfo a) Source # | |
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.1.0.0-ITRFbiNlHtpDlAKYR1El4c" '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 #
Hypothesis | |
|
Instances
Uniquely | |
|
Instances
Uniquable a => Eq (Uniquely a) Source # | |
Uniquable a => Ord (Uniquely a) Source # | |
Show a => Show (Uniquely a) Source # | |
Provenance of a pattern value.
PatVal | |
|
Instances
Eq PatVal Source # | |
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.1.0.0-ITRFbiNlHtpDlAKYR1El4c" '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?
Instances
data Provenance Source #
Describes where hypotheses came from. Used extensively to prune stupid solutions from the search space.
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 | |
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*.
TacticState | |
|
Instances
Show TacticState Source # | |
Defined in Wingman.Types showsPrec :: Int -> TacticState -> ShowS # show :: TacticState -> String # showList :: [TacticState] -> ShowS # | |
Generic TacticState Source # | |
Defined in Wingman.Types type Rep TacticState :: Type -> Type # from :: TacticState -> Rep TacticState x # to :: Rep TacticState x -> TacticState # | |
type Rep TacticState Source # | |
Defined in Wingman.Types type Rep TacticState = D1 ('MetaData "TacticState" "Wingman.Types" "hls-tactics-plugin-1.1.0.0-ITRFbiNlHtpDlAKYR1El4c" 'False) (C1 ('MetaCons "TacticState" 'PrefixI 'True) (S1 ('MetaSel ('Just "ts_skolems") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (Set TyVar)) :*: (S1 ('MetaSel ('Just "ts_unifier") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 TCvSubst) :*: S1 ('MetaSel ('Just "ts_unique_gen") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 UniqSupply)))) |
A wrapper around Type
which supports equality and ordering.
Plugin configuration for tactics
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
.
Auto | |
Intros | |
Destruct | |
Homomorphism | |
DestructLambdaCase | |
HomomorphismLambdaCase | |
DestructAll | |
UseDataCon | |
Refine |
Instances
tacticTitle :: TacticCommand -> Text -> Text Source #
Generate a title for the command.
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.
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 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 | |
Show OccName Source # | |
NFData OccName | |
HasOccName OccName | |
Binary OccName | |
Uniquable OccName | |
Outputable OccName | |
OutputableBndr OccName | |
Defined in OccName 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 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 composeSrcSpan :: Located (SrcSpanLess Name) -> Name # decomposeSrcSpan :: Name -> Located (SrcSpanLess Name) # | |
Outputable Name | |
OutputableBndr Name | |
Defined in Name 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 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 # | |
showsPrec :: Int -> UniqSupply -> ShowS # show :: UniqSupply -> String # showList :: [UniqSupply] -> ShowS # | |
Show TyCon Source # | |
Show OccName Source # | |
Show Name Source # | |
Show (HsDecl GhcPs) Source # | |
Show (LHsSigType GhcPs) Source # | |
Show (HsExpr GhcPs) Source # | |
Show (Pat GhcPs) Source # | |