hls-tactics-plugin-1.6.2.0: Wingman plugin for Haskell Language Server
Safe HaskellNone
LanguageHaskell2010

Wingman.Types

Synopsis

Documentation

data HoleSort Source #

Constructors

Hole 
Metaprogram Text 

Instances

Instances details
Eq HoleSort Source # 
Instance details

Defined in Wingman.Types

Ord HoleSort Source # 
Instance details

Defined in Wingman.Types

Show HoleSort Source # 
Instance details

Defined in Wingman.Types

data AgdaMatch Source #

Constructors

AgdaMatch 

Fields

Instances

Instances details
Show AgdaMatch Source # 
Instance details

Defined in Wingman.Types

newtype Rose a Source #

Constructors

Rose (Tree a) 

Instances

Instances details
Functor Rose Source # 
Instance details

Defined in Wingman.Types

Methods

fmap :: (a -> b) -> Rose a -> Rose b #

(<$) :: a -> Rose b -> Rose a #

Eq a => Eq (Rose a) Source # 
Instance details

Defined in Wingman.Types

Methods

(==) :: Rose a -> Rose a -> Bool #

(/=) :: Rose a -> Rose a -> Bool #

Data a => Data (Rose a) Source # 
Instance details

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 # 
Instance details

Defined in Wingman.Types

Generic (Rose a) Source # 
Instance details

Defined in Wingman.Types

Associated Types

type Rep (Rose a) :: Type -> Type #

Methods

from :: Rose a -> Rep (Rose a) x #

to :: Rep (Rose a) x -> Rose a #

(Eq a, Monoid a) => Semigroup (Rose a) Source #

This might not be lawful! I didn't check, and it feels sketchy.

Instance details

Defined in Wingman.Types

Methods

(<>) :: Rose a -> Rose a -> Rose a #

sconcat :: NonEmpty (Rose a) -> Rose a #

stimes :: Integral b => b -> Rose a -> Rose a #

(Eq a, Monoid a) => Monoid (Rose a) Source # 
Instance details

Defined in Wingman.Types

Methods

mempty :: Rose a #

mappend :: Rose a -> Rose a -> Rose a #

mconcat :: [Rose a] -> Rose a #

type Rep (Rose a) Source # 
Instance details

Defined in Wingman.Types

type Rep (Rose a) = D1 ('MetaData "Rose" "Wingman.Types" "hls-tactics-plugin-1.6.2.0-F0S9kfzWGRh6ZnCEvC7DkD" 'True) (C1 ('MetaCons "Rose" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Tree a))))

data Context Source #

The Reader context of tactics and rules

Constructors

Context 

Fields

Instances

Instances details
Show Context Source # 
Instance details

Defined in Wingman.Types

MonadReader Context ExtractM Source # 
Instance details

Defined in Wingman.Types

Methods

ask :: ExtractM Context #

local :: (Context -> Context) -> ExtractM a -> ExtractM a #

reader :: (Context -> a) -> ExtractM a #

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

Instances details
Monad Synthesized Source # 
Instance details

Defined in Wingman.Types

Methods

(>>=) :: Synthesized a -> (a -> Synthesized b) -> Synthesized b #

(>>) :: Synthesized a -> Synthesized b -> Synthesized b #

return :: a -> Synthesized a #

Functor Synthesized Source # 
Instance details

Defined in Wingman.Types

Methods

fmap :: (a -> b) -> Synthesized a -> Synthesized b #

(<$) :: a -> Synthesized b -> Synthesized a #

Applicative Synthesized Source #

This might not be lawful, due to the semigroup on Trace maybe not being lawful. But that's only for debug output, so it's not anything I'm concerned about.

Instance details

Defined in Wingman.Types

Methods

pure :: a -> Synthesized a #

(<*>) :: Synthesized (a -> b) -> Synthesized a -> Synthesized b #

liftA2 :: (a -> b -> c) -> Synthesized a -> Synthesized b -> Synthesized c #

(*>) :: Synthesized a -> Synthesized b -> Synthesized b #

(<*) :: Synthesized a -> Synthesized b -> Synthesized a #

Foldable Synthesized Source # 
Instance details

Defined in Wingman.Types

Methods

fold :: Monoid m => Synthesized m -> m #

foldMap :: Monoid m => (a -> m) -> Synthesized a -> m #

foldMap' :: Monoid m => (a -> m) -> Synthesized a -> m #

foldr :: (a -> b -> b) -> b -> Synthesized a -> b #

foldr' :: (a -> b -> b) -> b -> Synthesized a -> b #

foldl :: (b -> a -> b) -> b -> Synthesized a -> b #

foldl' :: (b -> a -> b) -> b -> Synthesized a -> b #

foldr1 :: (a -> a -> a) -> Synthesized a -> a #

foldl1 :: (a -> a -> a) -> Synthesized a -> a #

toList :: Synthesized a -> [a] #

null :: Synthesized a -> Bool #

length :: Synthesized a -> Int #

elem :: Eq a => a -> Synthesized a -> Bool #

maximum :: Ord a => Synthesized a -> a #

minimum :: Ord a => Synthesized a -> a #

sum :: Num a => Synthesized a -> a #

product :: Num a => Synthesized a -> a #

Traversable Synthesized Source # 
Instance details

Defined in Wingman.Types

Methods

traverse :: Applicative f => (a -> f b) -> Synthesized a -> f (Synthesized b) #

sequenceA :: Applicative f => Synthesized (f a) -> f (Synthesized a) #

mapM :: Monad m => (a -> m b) -> Synthesized a -> m (Synthesized b) #

sequence :: Monad m => Synthesized (m a) -> m (Synthesized a) #

MetaSubst Int (Synthesized (LHsExpr GhcPs)) Source # 
Instance details

Defined in Wingman.Types

MonadExtract Int (Synthesized (LHsExpr GhcPs)) TacticError TacticState ExtractM Source # 
Instance details

Defined in Wingman.Types

Eq a => Eq (Synthesized a) Source # 
Instance details

Defined in Wingman.Types

Data a => Data (Synthesized a) Source # 
Instance details

Defined in Wingman.Types

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Synthesized a -> c (Synthesized a) #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Synthesized a) #

toConstr :: Synthesized a -> Constr #

dataTypeOf :: Synthesized a -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Synthesized a)) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Synthesized a)) #

gmapT :: (forall b. Data b => b -> b) -> Synthesized a -> Synthesized a #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Synthesized a -> r #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Synthesized a -> r #

gmapQ :: (forall d. Data d => d -> u) -> Synthesized a -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Synthesized a -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Synthesized a -> m (Synthesized a) #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Synthesized a -> m (Synthesized a) #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Synthesized a -> m (Synthesized a) #

Show a => Show (Synthesized a) Source # 
Instance details

Defined in Wingman.Types

Generic (Synthesized a) Source # 
Instance details

Defined in Wingman.Types

Associated Types

type Rep (Synthesized a) :: Type -> Type #

Methods

from :: Synthesized a -> Rep (Synthesized a) x #

to :: Rep (Synthesized a) x -> Synthesized a #

type Rep (Synthesized a) Source # 
Instance details

Defined in Wingman.Types

type Rep (Synthesized a) = D1 ('MetaData "Synthesized" "Wingman.Types" "hls-tactics-plugin-1.6.2.0-F0S9kfzWGRh6ZnCEvC7DkD" 'False) (C1 ('MetaCons "Synthesized" 'PrefixI 'True) ((S1 ('MetaSel ('Just "syn_trace") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Trace) :*: S1 ('MetaSel ('Just "syn_scoped") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Hypothesis CType))) :*: (S1 ('MetaSel ('Just "syn_used_vals") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Set OccName)) :*: (S1 ('MetaSel ('Just "syn_recursion_count") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Sum Int)) :*: S1 ('MetaSel ('Just "syn_val") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a)))))

newtype ExtractM a Source #

Constructors

ExtractM 

Instances

Instances details
Monad ExtractM Source # 
Instance details

Defined in Wingman.Types

Methods

(>>=) :: ExtractM a -> (a -> ExtractM b) -> ExtractM b #

(>>) :: ExtractM a -> ExtractM b -> ExtractM b #

return :: a -> ExtractM a #

Functor ExtractM Source # 
Instance details

Defined in Wingman.Types

Methods

fmap :: (a -> b) -> ExtractM a -> ExtractM b #

(<$) :: a -> ExtractM b -> ExtractM a #

Applicative ExtractM Source # 
Instance details

Defined in Wingman.Types

Methods

pure :: a -> ExtractM a #

(<*>) :: ExtractM (a -> b) -> ExtractM a -> ExtractM b #

liftA2 :: (a -> b -> c) -> ExtractM a -> ExtractM b -> ExtractM c #

(*>) :: ExtractM a -> ExtractM b -> ExtractM b #

(<*) :: ExtractM a -> ExtractM b -> ExtractM a #

MonadReader Context ExtractM Source # 
Instance details

Defined in Wingman.Types

Methods

ask :: ExtractM Context #

local :: (Context -> Context) -> ExtractM a -> ExtractM a #

reader :: (Context -> a) -> ExtractM a #

MonadExtract Int (Synthesized (LHsExpr GhcPs)) TacticError TacticState ExtractM Source # 
Instance details

Defined in Wingman.Types

data Judgement' a Source #

The current bindings and goal for a hole to be filled by refinery.

Instances

Instances details
Functor Judgement' Source # 
Instance details

Defined in Wingman.Types

Methods

fmap :: (a -> b) -> Judgement' a -> Judgement' b #

(<$) :: a -> Judgement' b -> Judgement' a #

Show a => Show (Judgement' a) Source # 
Instance details

Defined in Wingman.Types

Generic (Judgement' a) Source # 
Instance details

Defined in Wingman.Types

Associated Types

type Rep (Judgement' a) :: Type -> Type #

Methods

from :: Judgement' a -> Rep (Judgement' a) x #

to :: Rep (Judgement' a) x -> Judgement' a #

type Rep (Judgement' a) Source # 
Instance details

Defined in Wingman.Types

type Rep (Judgement' a) = D1 ('MetaData "Judgement'" "Wingman.Types" "hls-tactics-plugin-1.6.2.0-F0S9kfzWGRh6ZnCEvC7DkD" 'False) (C1 ('MetaCons "Judgement" 'PrefixI 'True) ((S1 ('MetaSel ('Just "_jHypothesis") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (Hypothesis a)) :*: (S1 ('MetaSel ('Just "_jBlacklistDestruct") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Bool) :*: S1 ('MetaSel ('Just "_jWhitelistSplit") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Bool))) :*: (S1 ('MetaSel ('Just "_jIsTopHole") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Bool) :*: (S1 ('MetaSel ('Just "_jGoal") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 a) :*: S1 ('MetaSel ('Just "j_coercion") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TCvSubst)))))

data HyInfo a Source #

The provenance and type of a hypothesis term.

Constructors

HyInfo 

Instances

Instances details
Functor HyInfo Source # 
Instance details

Defined in Wingman.Types

Methods

fmap :: (a -> b) -> HyInfo a -> HyInfo b #

(<$) :: a -> HyInfo b -> HyInfo a #

Eq a => Eq (HyInfo a) Source # 
Instance details

Defined in Wingman.Types

Methods

(==) :: HyInfo a -> HyInfo a -> Bool #

(/=) :: HyInfo a -> HyInfo a -> Bool #

Data a => Data (HyInfo a) Source # 
Instance details

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 # 
Instance details

Defined in Wingman.Types

Methods

compare :: HyInfo a -> HyInfo a -> Ordering #

(<) :: HyInfo a -> HyInfo a -> Bool #

(<=) :: HyInfo a -> HyInfo a -> Bool #

(>) :: HyInfo a -> HyInfo a -> Bool #

(>=) :: HyInfo a -> HyInfo a -> Bool #

max :: HyInfo a -> HyInfo a -> HyInfo a #

min :: HyInfo a -> HyInfo a -> HyInfo a #

Show a => Show (HyInfo a) Source # 
Instance details

Defined in Wingman.Types

Methods

showsPrec :: Int -> HyInfo a -> ShowS #

show :: HyInfo a -> String #

showList :: [HyInfo a] -> ShowS #

Generic (HyInfo a) Source # 
Instance details

Defined in Wingman.Types

Associated Types

type Rep (HyInfo a) :: Type -> Type #

Methods

from :: HyInfo a -> Rep (HyInfo a) x #

to :: Rep (HyInfo a) x -> HyInfo a #

type Rep (HyInfo a) Source # 
Instance details

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

Instances details
Functor Hypothesis Source # 
Instance details

Defined in Wingman.Types

Methods

fmap :: (a -> b) -> Hypothesis a -> Hypothesis b #

(<$) :: a -> Hypothesis b -> Hypothesis a #

Eq a => Eq (Hypothesis a) Source # 
Instance details

Defined in Wingman.Types

Methods

(==) :: Hypothesis a -> Hypothesis a -> Bool #

(/=) :: Hypothesis a -> Hypothesis a -> Bool #

Data a => Data (Hypothesis a) Source # 
Instance details

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 # 
Instance details

Defined in Wingman.Types

Show a => Show (Hypothesis a) Source # 
Instance details

Defined in Wingman.Types

Generic (Hypothesis a) Source # 
Instance details

Defined in Wingman.Types

Associated Types

type Rep (Hypothesis a) :: Type -> Type #

Methods

from :: Hypothesis a -> Rep (Hypothesis a) x #

to :: Rep (Hypothesis a) x -> Hypothesis a #

Semigroup (Hypothesis a) Source # 
Instance details

Defined in Wingman.Types

Monoid (Hypothesis a) Source # 
Instance details

Defined in Wingman.Types

type Rep (Hypothesis a) Source # 
Instance details

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])))

newtype Uniquely a Source #

A wrapper which uses a Uniquable constraint for providing Eq and Ord instances.

Constructors

Uniquely 

Fields

Instances

Instances details
Uniquable a => Eq (Uniquely a) Source # 
Instance details

Defined in Wingman.Types

Methods

(==) :: Uniquely a -> Uniquely a -> Bool #

(/=) :: Uniquely a -> Uniquely a -> Bool #

Data a => Data (Uniquely a) Source # 
Instance details

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 # 
Instance details

Defined in Wingman.Types

Methods

compare :: Uniquely a -> Uniquely a -> Ordering #

(<) :: Uniquely a -> Uniquely a -> Bool #

(<=) :: Uniquely a -> Uniquely a -> Bool #

(>) :: Uniquely a -> Uniquely a -> Bool #

(>=) :: Uniquely a -> Uniquely a -> Bool #

max :: Uniquely a -> Uniquely a -> Uniquely a #

min :: Uniquely a -> Uniquely a -> Uniquely a #

Show a => Show (Uniquely a) Source # 
Instance details

Defined in Wingman.Types

Methods

showsPrec :: Int -> Uniquely a -> ShowS #

show :: Uniquely a -> String #

showList :: [Uniquely a] -> ShowS #

data PatVal Source #

Provenance of a pattern value.

Constructors

PatVal 

Fields

Instances

Instances details
Eq PatVal Source # 
Instance details

Defined in Wingman.Types

Methods

(==) :: PatVal -> PatVal -> Bool #

(/=) :: PatVal -> PatVal -> Bool #

Data PatVal Source # 
Instance details

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 # 
Instance details

Defined in Wingman.Types

Show PatVal Source # 
Instance details

Defined in Wingman.Types

Generic PatVal Source # 
Instance details

Defined in Wingman.Types

Associated Types

type Rep PatVal :: Type -> Type #

Methods

from :: PatVal -> Rep PatVal x #

to :: Rep PatVal x -> PatVal #

type Rep PatVal Source # 
Instance details

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?

Instances

Instances details
Eq DisallowReason Source # 
Instance details

Defined in Wingman.Types

Data DisallowReason Source # 
Instance details

Defined in Wingman.Types

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> DisallowReason -> c DisallowReason #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c DisallowReason #

toConstr :: DisallowReason -> Constr #

dataTypeOf :: DisallowReason -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c DisallowReason) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DisallowReason) #

gmapT :: (forall b. Data b => b -> b) -> DisallowReason -> DisallowReason #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> DisallowReason -> r #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> DisallowReason -> r #

gmapQ :: (forall d. Data d => d -> u) -> DisallowReason -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> DisallowReason -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> DisallowReason -> m DisallowReason #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> DisallowReason -> m DisallowReason #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> DisallowReason -> m DisallowReason #

Ord DisallowReason Source # 
Instance details

Defined in Wingman.Types

Show DisallowReason Source # 
Instance details

Defined in Wingman.Types

Generic DisallowReason Source # 
Instance details

Defined in Wingman.Types

Associated Types

type Rep DisallowReason :: Type -> Type #

type Rep DisallowReason Source # 
Instance details

Defined in Wingman.Types

type Rep DisallowReason = D1 ('MetaData "DisallowReason" "Wingman.Types" "hls-tactics-plugin-1.6.2.0-F0S9kfzWGRh6ZnCEvC7DkD" 'False) ((C1 ('MetaCons "WrongBranch" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int)) :+: C1 ('MetaCons "Shadowed" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "RecursiveCall" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "AlreadyDestructed" 'PrefixI 'False) (U1 :: Type -> Type)))

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.

Fields

  • OccName

    Binding function

  • Int

    Argument Position

  • Int

    of how many arguments total? | A binding created in a pattern match.

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

Instances details
Eq Provenance Source # 
Instance details

Defined in Wingman.Types

Data Provenance Source # 
Instance details

Defined in Wingman.Types

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Provenance -> c Provenance #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Provenance #

toConstr :: Provenance -> Constr #

dataTypeOf :: Provenance -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Provenance) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Provenance) #

gmapT :: (forall b. Data b => b -> b) -> Provenance -> Provenance #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Provenance -> r #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Provenance -> r #

gmapQ :: (forall d. Data d => d -> u) -> Provenance -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Provenance -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Provenance -> m Provenance #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Provenance -> m Provenance #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Provenance -> m Provenance #

Ord Provenance Source # 
Instance details

Defined in Wingman.Types

Show Provenance Source # 
Instance details

Defined in Wingman.Types

Generic Provenance Source # 
Instance details

Defined in Wingman.Types

Associated Types

type Rep Provenance :: Type -> Type #

type Rep Provenance Source # 
Instance details

Defined in Wingman.Types

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

Instances details
Show TacticState Source # 
Instance details

Defined in Wingman.Types

Generic TacticState Source # 
Instance details

Defined in Wingman.Types

Associated Types

type Rep TacticState :: Type -> Type #

MonadExtract Int (Synthesized (LHsExpr GhcPs)) TacticError TacticState ExtractM Source # 
Instance details

Defined in Wingman.Types

type Rep TacticState Source # 
Instance details

Defined in Wingman.Types

type Rep TacticState = D1 ('MetaData "TacticState" "Wingman.Types" "hls-tactics-plugin-1.6.2.0-F0S9kfzWGRh6ZnCEvC7DkD" '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))))

newtype CType Source #

A wrapper around Type which supports equality and ordering.

Constructors

CType 

Fields

Instances

Instances details
Eq CType Source # 
Instance details

Defined in Wingman.Types

Methods

(==) :: CType -> CType -> Bool #

(/=) :: CType -> CType -> Bool #

Data CType Source # 
Instance details

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 #

toConstr :: CType -> Constr #

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 # 
Instance details

Defined in Wingman.Types

Methods

compare :: CType -> CType -> Ordering #

(<) :: CType -> CType -> Bool #

(<=) :: CType -> CType -> Bool #

(>) :: CType -> CType -> Bool #

(>=) :: CType -> CType -> Bool #

max :: CType -> CType -> CType #

min :: CType -> CType -> CType #

Show CType Source # 
Instance details

Defined in Wingman.Types

Methods

showsPrec :: Int -> CType -> ShowS #

show :: CType -> String #

showList :: [CType] -> ShowS #

data Config Source #

Plugin configuration for tactics

Instances

Instances details
Eq Config Source # 
Instance details

Defined in Wingman.Types

Methods

(==) :: Config -> Config -> Bool #

(/=) :: Config -> Config -> Bool #

Ord Config Source # 
Instance details

Defined in Wingman.Types

Show Config Source # 
Instance details

Defined in Wingman.Types

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.

Instances

Instances details
Bounded TacticCommand Source # 
Instance details

Defined in Wingman.Types

Enum TacticCommand Source # 
Instance details

Defined in Wingman.Types

Eq TacticCommand Source # 
Instance details

Defined in Wingman.Types

Ord TacticCommand Source # 
Instance details

Defined in Wingman.Types

Show TacticCommand Source # 
Instance details

Defined in Wingman.Types

IsContinuationSort TacticCommand Source # 
Instance details

Defined in Wingman.LanguageServer.TacticProviders

tacticTitle :: TacticCommand -> Text -> Text Source #

Generate a title for the command.

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

emptyContext :: Context Source #

An empty context

dropEveryOther :: [a] -> [a] Source #

rose :: (Eq a, Monoid a) => a -> [Rose a] -> Rose a Source #

data OccName #

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

Instances details
Eq OccName 
Instance details

Defined in OccName

Methods

(==) :: OccName -> OccName -> Bool #

(/=) :: OccName -> OccName -> Bool #

Data OccName 
Instance details

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 
Instance details

Defined in OccName

NFData OccName 
Instance details

Defined in OccName

Methods

rnf :: OccName -> () #

HasOccName OccName 
Instance details

Defined in OccName

Methods

occName :: OccName -> OccName #

Binary OccName 
Instance details

Defined in OccName

Uniquable OccName 
Instance details

Defined in OccName

Methods

getUnique :: OccName -> Unique #

Outputable OccName 
Instance details

Defined in OccName

Methods

ppr :: OccName -> SDoc #

pprPrec :: Rational -> OccName -> SDoc #

OutputableBndr OccName 
Instance details

Defined in OccName

data Name #

A unique, unambiguous name for something, containing information about where that thing originated.

Instances

Instances details
Eq Name

The same comments as for Name's Ord instance apply.

Instance details

Defined in Name

Methods

(==) :: Name -> Name -> Bool #

(/=) :: Name -> Name -> Bool #

Data Name 
Instance details

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 #

toConstr :: Name -> Constr #

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 nonDetCmpUnique, which means that the ordering is not stable across deserialization or rebuilds.

See nonDetCmpUnique for further information, and trac #15240 for a bug caused by improper use of this instance.

Instance details

Defined in Name

Methods

compare :: Name -> Name -> Ordering #

(<) :: Name -> Name -> Bool #

(<=) :: Name -> Name -> Bool #

(>) :: Name -> Name -> Bool #

(>=) :: Name -> Name -> Bool #

max :: Name -> Name -> Name #

min :: Name -> Name -> Name #

Show Name Source # 
Instance details

Defined in Wingman.Types

Methods

showsPrec :: Int -> Name -> ShowS #

show :: Name -> String #

showList :: [Name] -> ShowS #

NFData Name 
Instance details

Defined in Name

Methods

rnf :: Name -> () #

NamedThing Name 
Instance details

Defined in Name

HasOccName Name 
Instance details

Defined in Name

Methods

occName :: Name -> OccName #

Binary Name

Assumes that the Name is a non-binding one. See putIfaceTopBndr and getIfaceTopBndr for serializing binding Names. See UserData for the rationale for this distinction.

Instance details

Defined in Name

Methods

put_ :: BinHandle -> Name -> IO () #

put :: BinHandle -> Name -> IO (Bin Name) #

get :: BinHandle -> IO Name #

Uniquable Name 
Instance details

Defined in Name

Methods

getUnique :: Name -> Unique #

HasSrcSpan Name 
Instance details

Defined in Name

Outputable Name 
Instance details

Defined in Name

Methods

ppr :: Name -> SDoc #

pprPrec :: Rational -> Name -> SDoc #

OutputableBndr Name 
Instance details

Defined in Name

type SrcSpanLess Name 
Instance details

Defined in Name

data Type #

Instances

Instances details
Data Type 
Instance details

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 #

toConstr :: Type -> Constr #

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 # 
Instance details

Defined in Wingman.Types

Methods

showsPrec :: Int -> Type -> ShowS #

show :: Type -> String #

showList :: [Type] -> ShowS #

Outputable Type 
Instance details

Defined in TyCoRep

Methods

ppr :: Type -> SDoc #

pprPrec :: Rational -> Type -> SDoc #

Eq (DeBruijn Type) 
Instance details

Defined in CoreMap

Methods

(==) :: DeBruijn Type -> DeBruijn Type -> Bool #

(/=) :: DeBruijn Type -> DeBruijn Type -> Bool #

type TyVar = Var #

Type or kind Variable

Orphan instances

Show TCvSubst Source # 
Instance details

Show Class Source # 
Instance details

Methods

showsPrec :: Int -> Class -> ShowS #

show :: Class -> String #

showList :: [Class] -> ShowS #

Show ConLike Source # 
Instance details

Show DataCon Source # 
Instance details

Show Type Source # 
Instance details

Methods

showsPrec :: Int -> Type -> ShowS #

show :: Type -> String #

showList :: [Type] -> ShowS #

Show Var Source # 
Instance details

Methods

showsPrec :: Int -> Var -> ShowS #

show :: Var -> String #

showList :: [Var] -> ShowS #

Show UniqSupply Source # 
Instance details

Show LexicalFixity Source # 
Instance details

Show TyCon Source # 
Instance details

Methods

showsPrec :: Int -> TyCon -> ShowS #

show :: TyCon -> String #

showList :: [TyCon] -> ShowS #

Show Name Source # 
Instance details

Methods

showsPrec :: Int -> Name -> ShowS #

show :: Name -> String #

showList :: [Name] -> ShowS #

MonadReader r m => MonadReader r (RuleT jdg ext err s m) Source # 
Instance details

Methods

ask :: RuleT jdg ext err s m r #

local :: (r -> r) -> RuleT jdg ext err s m a -> RuleT jdg ext err s m a #

reader :: (r -> a) -> RuleT jdg ext err s m a #

MonadReader r m => MonadReader r (TacticT jdg ext err s m) Source # 
Instance details

Methods

ask :: TacticT jdg ext err s m r #

local :: (r -> r) -> TacticT jdg ext err s m a -> TacticT jdg ext err s m a #

reader :: (r -> a) -> TacticT jdg ext err s m a #

Show (HsDecl GhcPs) Source # 
Instance details

Show (LHsSigType GhcPs) Source # 
Instance details

Show (HsExpr GhcPs) Source # 
Instance details

Show (HsExpr GhcTc) Source # 
Instance details

Show (Pat GhcPs) Source # 
Instance details