Safe Haskell | None |
---|---|
Language | Haskell2010 |
Synopsis
- data AgdaMatch = AgdaMatch {}
- data RunTacticResults = RunTacticResults {}
- newtype Rose a = Rose (Tree a)
- data Context = Context {
- ctxDefiningFuncs :: [(OccName, CType)]
- ctxModuleFuncs :: [(OccName, CType)]
- ctxFeatureSet :: FeatureSet
- type Trace = Rose String
- type Rule = RuleM (Trace, LHsExpr GhcPs)
- type RuleM = RuleT Judgement (Trace, LHsExpr GhcPs) TacticError TacticState ExtractM
- type TacticsM = TacticT Judgement (Trace, 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_used_vals :: !(Set OccName)
- ts_intro_vals :: !(Set OccName)
- ts_unused_top_vals :: !(Set OccName)
- ts_recursion_stack :: ![Maybe PatVal]
- ts_recursion_count :: !Int
- ts_unique_gen :: !UniqSupply
- newtype CType = CType {}
- unsafeDefaultUniqueSupply :: UniqSupply
- defaultTacticState :: TacticState
- freshUnique :: MonadState TacticState m => m Unique
- withRecursionStack :: ([Maybe PatVal] -> [Maybe PatVal]) -> TacticState -> TacticState
- pushRecursionStack :: TacticState -> TacticState
- popRecursionStack :: TacticState -> TacticState
- withUsedVals :: (Set OccName -> Set OccName) -> TacticState -> TacticState
- withIntroducedVals :: (Set OccName -> Set OccName) -> TacticState -> TacticState
- overProvenance :: (Provenance -> Provenance) -> HyInfo a -> HyInfo a
- emptyContext :: Context
- dropEveryOther :: [a] -> [a]
- rose :: (Eq a, Monoid a) => a -> [Rose a] -> Rose a
- module Ide.Plugin.Tactic.Debug
- data OccName
- data Name
- data Type
- type TyVar = Var
- type Span = RealSrcSpan
- data Range
Documentation
data RunTacticResults Source #
The results of runTactic
Instances
Show RunTacticResults Source # | |
Defined in Ide.Plugin.Tactic.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 # | |
Semigroup a => Semigroup (Rose a) Source # | |
Monoid a => Monoid (Rose a) Source # | |
MonadExtract (Trace, LHsExpr GhcPs) ExtractM Source # | Orphan instance for producing holes when attempting to solve tactics. |
type Rep (Rose a) Source # | |
Defined in Ide.Plugin.Tactic.Types |
The Reader context of tactics and rules
Context | |
|
data TacticError Source #
Reasons a tactic might fail.
Instances
Eq TacticError Source # | |
Defined in Ide.Plugin.Tactic.Types (==) :: TacticError -> TacticError -> Bool # (/=) :: TacticError -> TacticError -> Bool # | |
Show TacticError Source # | |
Defined in Ide.Plugin.Tactic.Types showsPrec :: Int -> TacticError -> ShowS # show :: TacticError -> String # showList :: [TacticError] -> ShowS # |
ExtractM | |
|
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 Ide.Plugin.Tactic.Types | |
Show a => Show (HyInfo a) Source # | |
Generic (HyInfo a) Source # | |
type Rep (HyInfo a) Source # | |
Defined in Ide.Plugin.Tactic.Types type Rep (HyInfo a) = D1 ('MetaData "HyInfo" "Ide.Plugin.Tactic.Types" "hls-tactics-plugin-1.0.0.0-JjkuRbP5sBO2aDU4B9iK42" '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 Ide.Plugin.Tactic.Types type Rep PatVal = D1 ('MetaData "PatVal" "Ide.Plugin.Tactic.Types" "hls-tactics-plugin-1.0.0.0-JjkuRbP5sBO2aDU4B9iK42" '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 DataCon)) :*: 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 #
TacticState | |
|
Instances
A wrapper around Type
which supports equality and ordering.
unsafeDefaultUniqueSupply :: UniqSupply Source #
A UniqSupply
to use in defaultTacticState
freshUnique :: MonadState TacticState m => m Unique Source #
Generate a new Unique
withRecursionStack :: ([Maybe PatVal] -> [Maybe PatVal]) -> TacticState -> TacticState Source #
withUsedVals :: (Set OccName -> Set OccName) -> TacticState -> TacticState Source #
withIntroducedVals :: (Set OccName -> Set OccName) -> TacticState -> TacticState Source #
overProvenance :: (Provenance -> Provenance) -> HyInfo a -> HyInfo a Source #
Map a function over the provenance.
emptyContext :: Context Source #
An empty context
dropEveryOther :: [a] -> [a] Source #
module Ide.Plugin.Tactic.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 |
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 # | |
Outputable Type | |
Eq (DeBruijn Type) | |
type Span = RealSrcSpan #
Instances
Eq Range | |
Ord Range | |
Read Range | |
Show Range | |
Generic Range | |
ToJSON Range | |
Defined in Language.LSP.Types.Location | |
FromJSON Range | |
NFData Range | |
Defined in Language.LSP.Types.Location | |
type Rep Range | |
Defined in Language.LSP.Types.Location type Rep Range = D1 ('MetaData "Range" "Language.LSP.Types.Location" "lsp-types-1.1.0.0-6GA8X8rnyjX71RqllIS6to" 'False) (C1 ('MetaCons "Range" 'PrefixI 'True) (S1 ('MetaSel ('Just "_start") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Position) :*: S1 ('MetaSel ('Just "_end") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Position))) |