| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Ide.Plugin.Tactic.Types
Contents
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
Constructors
| RunTacticResults | |
Instances
| Show RunTacticResults Source # | |
Defined in Ide.Plugin.Tactic.Types Methods 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
Constructors
| Context | |
Fields
| |
data TacticError Source #
Reasons a tactic might fail.
Constructors
Instances
| Eq TacticError Source # | |
Defined in Ide.Plugin.Tactic.Types | |
| Show TacticError Source # | |
Defined in Ide.Plugin.Tactic.Types Methods showsPrec :: Int -> TacticError -> ShowS # show :: TacticError -> String # showList :: [TacticError] -> ShowS # | |
Constructors
| ExtractM | |
Fields
| |
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 # | |
| 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 #
Constructors
| Hypothesis | |
Fields
| |
Instances
Constructors
| Uniquely | |
Fields
| |
Instances
| Uniquable a => Eq (Uniquely a) Source # | |
| Uniquable a => Ord (Uniquely a) Source # | |
Defined in Ide.Plugin.Tactic.Types | |
| Show a => Show (Uniquely a) Source # | |
Provenance of a pattern value.
Constructors
| PatVal | |
Fields
| |
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?
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 | |
| 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 #
Constructors
| TacticState | |
Fields
| |
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 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 | |
| Show OccName Source # | |
| 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 |
| 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 # | |
| 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))) | |