Wingman.Types

Documentation

data HoleJudgment

Constructors

HoleJudgment

Fields

• hj_range :: Tracked 'Current Range
• hj_jdg :: Judgement
• hj_ctx :: Context
• hj_dflags :: DynFlags
• hj_hole_sort :: HoleSort

data HoleSort

Constructors

Hole

Metaprogram Text

Instances

Eq HoleSort

Defined in Wingman.Types

Methods

(==) :: HoleSort -> HoleSort -> Bool

(/=) :: HoleSort -> HoleSort -> Bool

Ord HoleSort

Defined in Wingman.Types

Methods

compare :: HoleSort -> HoleSort -> Ordering

(<) :: HoleSort -> HoleSort -> Bool

(<=) :: HoleSort -> HoleSort -> Bool

(>) :: HoleSort -> HoleSort -> Bool

(>=) :: HoleSort -> HoleSort -> Bool

max :: HoleSort -> HoleSort -> HoleSort

min :: HoleSort -> HoleSort -> HoleSort

Show HoleSort

Defined in Wingman.Types

Methods

showsPrec :: Int -> HoleSort -> ShowS

show :: HoleSort -> String

showList :: [HoleSort] -> ShowS

data UserFacingMessage

Constructors

TacticErrors

TimedOut

NothingToDo

InfrastructureError Text

Instances

Eq UserFacingMessage

Defined in Wingman.Types

Methods

(==) :: UserFacingMessage -> UserFacingMessage -> Bool

(/=) :: UserFacingMessage -> UserFacingMessage -> Bool

Show UserFacingMessage

Defined in Wingman.Types

Methods

showsPrec :: Int -> UserFacingMessage -> ShowS

show :: UserFacingMessage -> String

showList :: [UserFacingMessage] -> ShowS

data AgdaMatch

Constructors

AgdaMatch

Fields

• amPats :: [Pat GhcPs]
• amBody :: HsExpr GhcPs

Instances

Show AgdaMatch

Defined in Wingman.Types

Methods

showsPrec :: Int -> AgdaMatch -> ShowS

show :: AgdaMatch -> String

showList :: [AgdaMatch] -> ShowS

data RunTacticResults

The results of runTactic

Constructors

RunTacticResults

Fields

• rtr_trace :: Trace
• rtr_extract :: LHsExpr GhcPs
• rtr_subgoals :: [Judgement]
• rtr_other_solns :: [Synthesized (LHsExpr GhcPs)]
• rtr_jdg :: Judgement
• rtr_ctx :: Context

Instances

Show RunTacticResults

Defined in Wingman.Types

Methods

showsPrec :: Int -> RunTacticResults -> ShowS

show :: RunTacticResults -> String

showList :: [RunTacticResults] -> ShowS

newtype Rose a

Constructors

Rose (Tree a)

Instances

Functor Rose

Defined in Wingman.Types

Methods

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

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

Eq a => Eq (Rose a)

Defined in Wingman.Types

Methods

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

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

Show (Rose String)

Defined in Wingman.Types

Methods

showsPrec :: Int -> Rose String -> ShowS

show :: Rose String -> String

showList :: [Rose String] -> ShowS

Generic (Rose a)

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)

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

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)

Defined in Wingman.Types

Methods

mempty :: Rose a

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

mconcat :: [Rose a] -> Rose a

type Rep (Rose a)

Defined in Wingman.Types

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

data KnownThings

Things we'd like to look up, that don't exist in TysWiredIn.

Constructors

KnownThings

Fields

• kt_semigroup :: Class
• kt_monoid :: Class

data Context

The Reader context of tactics and rules

Constructors

Context

Fields

• ctxDefiningFuncs :: [(OccName, CType)]

  The functions currently being defined

• ctxModuleFuncs :: [(OccName, CType)]

  Everything defined in the current module

• ctxConfig :: Config
• ctxKnownThings :: KnownThings
• ctxInstEnvs :: InstEnvs
• ctxFamInstEnvs :: FamInstEnvs
• ctxTheta :: Set CType

Instances

Show Context

Defined in Wingman.Types

Methods

showsPrec :: Int -> Context -> ShowS

show :: Context -> String

showList :: [Context] -> ShowS

MonadReader Context ExtractM

Defined in Wingman.Types

Methods

ask :: ExtractM Context

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

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

data Synthesized a

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

• syn_trace :: Trace

  A tree describing which tactics were used produce the syn_val. Mainly for debugging when you get the wrong answer, to see the other things it tried.

• syn_scoped :: Hypothesis CType

  All of the bindings created to produce the syn_val.

• syn_used_vals :: Set OccName

  The values used when synthesizing the syn_val.

• syn_recursion_count :: Sum Int

  The number of recursive calls

• syn_val :: a

Instances

Functor Synthesized

Defined in Wingman.Types

Methods

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

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

Applicative Synthesized

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.

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

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

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)

Eq a => Eq (Synthesized a)

Defined in Wingman.Types

Methods

(==) :: Synthesized a -> Synthesized a -> Bool

(/=) :: Synthesized a -> Synthesized a -> Bool

Show a => Show (Synthesized a)

Defined in Wingman.Types

Methods

showsPrec :: Int -> Synthesized a -> ShowS

show :: Synthesized a -> String

showList :: [Synthesized a] -> ShowS

Generic (Synthesized a)

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

MonadExtract (Synthesized (LHsExpr GhcPs)) ExtractM

Orphan instance for producing holes when attempting to solve tactics.

Defined in Wingman.Types

Methods

hole :: ExtractM (Synthesized (LHsExpr GhcPs))

type Rep (Synthesized a)

Defined in Wingman.Types

type Rep (Synthesized a) = D1 ('MetaData "Synthesized" "Wingman.Types" "hls-tactics-plugin-1.2.0.0-ISyG8qIj9D072QqyrjxihH" '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)))))

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

Reasons a tactic might fail.

Constructors

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

TacticPanic String

Instances

Eq TacticError

Defined in Wingman.Types

Methods

(==) :: TacticError -> TacticError -> Bool

(/=) :: TacticError -> TacticError -> Bool

Show TacticError

Defined in Wingman.Types

Methods

showsPrec :: Int -> TacticError -> ShowS

show :: TacticError -> String

showList :: [TacticError] -> ShowS

newtype ExtractM a

Constructors

ExtractM

Fields

• unExtractM :: Reader Context a

Instances

Monad ExtractM

Defined in Wingman.Types

Methods

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

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

return :: a -> ExtractM a

Functor ExtractM

Defined in Wingman.Types

Methods

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

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

Applicative ExtractM

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

Defined in Wingman.Types

Methods

ask :: ExtractM Context

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

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

MonadExtract (Synthesized (LHsExpr GhcPs)) ExtractM

Orphan instance for producing holes when attempting to solve tactics.

Defined in Wingman.Types

Methods

hole :: ExtractM (Synthesized (LHsExpr GhcPs))

type Judgement = Judgement' CType

data Judgement' a

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

Constructors

Judgement

Fields

• _jHypothesis :: !(Hypothesis a)
• _jBlacklistDestruct :: !Bool
• _jWhitelistSplit :: !Bool
• _jIsTopHole :: !Bool
• _jGoal :: !a

Instances

Functor Judgement'

Defined in Wingman.Types

Methods

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

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

Eq a => Eq (Judgement' a)

Defined in Wingman.Types

Methods

(==) :: Judgement' a -> Judgement' a -> Bool

(/=) :: Judgement' a -> Judgement' a -> Bool

Show a => Show (Judgement' a)

Defined in Wingman.Types

Methods

showsPrec :: Int -> Judgement' a -> ShowS

show :: Judgement' a -> String

showList :: [Judgement' a] -> ShowS

Generic (Judgement' a)

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)

Defined in Wingman.Types

type Rep (Judgement' a) = D1 ('MetaData "Judgement'" "Wingman.Types" "hls-tactics-plugin-1.2.0.0-ISyG8qIj9D072QqyrjxihH" '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)))))

data HyInfo a

The provenance and type of a hypothesis term.

Constructors

HyInfo

Fields

• hi_name :: OccName
• hi_provenance :: Provenance
• hi_type :: a

Instances

Functor HyInfo

Defined in Wingman.Types

Methods

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

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

Eq a => Eq (HyInfo a)

Defined in Wingman.Types

Methods

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

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

Ord a => Ord (HyInfo a)

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)

Defined in Wingman.Types

Methods

showsPrec :: Int -> HyInfo a -> ShowS

show :: HyInfo a -> String

showList :: [HyInfo a] -> ShowS

Generic (HyInfo a)

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)

Defined in Wingman.Types

type Rep (HyInfo a) = D1 ('MetaData "HyInfo" "Wingman.Types" "hls-tactics-plugin-1.2.0.0-ISyG8qIj9D072QqyrjxihH" '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

Constructors

Hypothesis

Fields

• unHypothesis :: [HyInfo a]

Instances

Functor Hypothesis

Defined in Wingman.Types

Methods

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

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

Eq a => Eq (Hypothesis a)

Defined in Wingman.Types

Methods

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

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

Ord a => Ord (Hypothesis a)

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)

Defined in Wingman.Types

Methods

showsPrec :: Int -> Hypothesis a -> ShowS

show :: Hypothesis a -> String

showList :: [Hypothesis a] -> ShowS

Generic (Hypothesis a)

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)

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)

Defined in Wingman.Types

Methods

mempty :: Hypothesis a

mappend :: Hypothesis a -> Hypothesis a -> Hypothesis a

mconcat :: [Hypothesis a] -> Hypothesis a

type Rep (Hypothesis a)

Defined in Wingman.Types

type Rep (Hypothesis a) = D1 ('MetaData "Hypothesis" "Wingman.Types" "hls-tactics-plugin-1.2.0.0-ISyG8qIj9D072QqyrjxihH" 'True) (C1 ('MetaCons "Hypothesis" 'PrefixI 'True) (S1 ('MetaSel ('Just "unHypothesis") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [HyInfo a])))

newtype Uniquely a

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

Constructors

Uniquely

Fields

• getViaUnique :: a

Instances

Uniquable a => Eq (Uniquely a)

Defined in Wingman.Types

Methods

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

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

Uniquable a => Ord (Uniquely a)

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)

Defined in Wingman.Types

Methods

showsPrec :: Int -> Uniquely a -> ShowS

show :: Uniquely a -> String

showList :: [Uniquely a] -> ShowS

data PatVal

Provenance of a pattern value.

Constructors

PatVal

Fields

• pv_scrutinee :: Maybe OccName

  Original scrutinee which created this PatVal. Nothing, for lambda case.

• pv_ancestry :: Set OccName

  The set of values which had to be destructed to discover this term. Always contains the scrutinee.

• pv_datacon :: Uniquely ConLike

  The datacon which introduced this term.

• pv_position :: Int

  The position of this binding in the datacon's arguments.

Instances

Eq PatVal

Defined in Wingman.Types

Methods

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

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

Ord PatVal

Defined in Wingman.Types

Methods

compare :: PatVal -> PatVal -> Ordering

(<) :: PatVal -> PatVal -> Bool

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

(>) :: PatVal -> PatVal -> Bool

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

max :: PatVal -> PatVal -> PatVal

min :: PatVal -> PatVal -> PatVal

Show PatVal

Defined in Wingman.Types

Methods

showsPrec :: Int -> PatVal -> ShowS

show :: PatVal -> String

showList :: [PatVal] -> ShowS

Generic PatVal

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

Defined in Wingman.Types

type Rep PatVal = D1 ('MetaData "PatVal" "Wingman.Types" "hls-tactics-plugin-1.2.0.0-ISyG8qIj9D072QqyrjxihH" '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

Why was a hypothesis disallowed?

Constructors

WrongBranch Int

Shadowed

RecursiveCall

AlreadyDestructed

Instances

Eq DisallowReason

Defined in Wingman.Types

Methods

(==) :: DisallowReason -> DisallowReason -> Bool

(/=) :: DisallowReason -> DisallowReason -> Bool

Ord DisallowReason

Defined in Wingman.Types

Methods

compare :: DisallowReason -> DisallowReason -> Ordering

(<) :: DisallowReason -> DisallowReason -> Bool

(<=) :: DisallowReason -> DisallowReason -> Bool

(>) :: DisallowReason -> DisallowReason -> Bool

(>=) :: DisallowReason -> DisallowReason -> Bool

max :: DisallowReason -> DisallowReason -> DisallowReason

min :: DisallowReason -> DisallowReason -> DisallowReason

Show DisallowReason

Defined in Wingman.Types

Methods

showsPrec :: Int -> DisallowReason -> ShowS

show :: DisallowReason -> String

showList :: [DisallowReason] -> ShowS

Generic DisallowReason

Defined in Wingman.Types

Associated Types

type Rep DisallowReason :: Type -> Type

Methods

from :: DisallowReason -> Rep DisallowReason x

to :: Rep DisallowReason x -> DisallowReason

type Rep DisallowReason

Defined in Wingman.Types

type Rep DisallowReason = D1 ('MetaData "DisallowReason" "Wingman.Types" "hls-tactics-plugin-1.2.0.0-ISyG8qIj9D072QqyrjxihH" '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

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

Eq Provenance

Defined in Wingman.Types

Methods

(==) :: Provenance -> Provenance -> Bool

(/=) :: Provenance -> Provenance -> Bool

Ord Provenance

Defined in Wingman.Types

Methods

compare :: Provenance -> Provenance -> Ordering

(<) :: Provenance -> Provenance -> Bool

(<=) :: Provenance -> Provenance -> Bool

(>) :: Provenance -> Provenance -> Bool

(>=) :: Provenance -> Provenance -> Bool

max :: Provenance -> Provenance -> Provenance

min :: Provenance -> Provenance -> Provenance

Show Provenance

Defined in Wingman.Types

Methods

showsPrec :: Int -> Provenance -> ShowS

show :: Provenance -> String

showList :: [Provenance] -> ShowS

Generic Provenance

Defined in Wingman.Types

Associated Types

type Rep Provenance :: Type -> Type

Methods

from :: Provenance -> Rep Provenance x

to :: Rep Provenance x -> Provenance

type Rep Provenance

Defined in Wingman.Types

type Rep Provenance = D1 ('MetaData "Provenance" "Wingman.Types" "hls-tactics-plugin-1.2.0.0-ISyG8qIj9D072QqyrjxihH" 'False) ((C1 ('MetaCons "TopLevelArgPrv" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 OccName) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int))) :+: (C1 ('MetaCons "PatternMatchPrv" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PatVal)) :+: C1 ('MetaCons "ClassMethodPrv" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Uniquely Class))))) :+: ((C1 ('MetaCons "UserPrv" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ImportPrv" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "RecursivePrv" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "DisallowedPrv" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DisallowReason) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Provenance)))))

data TacticState

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

• ts_skolems :: !(Set TyVar)

  The known skolems.

• ts_unifier :: !TCvSubst
• ts_unique_gen :: !UniqSupply

Instances

Show TacticState

Defined in Wingman.Types

Methods

showsPrec :: Int -> TacticState -> ShowS

show :: TacticState -> String

showList :: [TacticState] -> ShowS

Generic TacticState

Defined in Wingman.Types

Associated Types

type Rep TacticState :: Type -> Type

Methods

from :: TacticState -> Rep TacticState x

to :: Rep TacticState x -> TacticState

type Rep TacticState

Defined in Wingman.Types

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

A wrapper around Type which supports equality and ordering.

Constructors

CType

Fields

• unCType :: Type

Instances

Eq CType

Defined in Wingman.Types

Methods

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

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

Ord CType

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

Defined in Wingman.Types

Methods

showsPrec :: Int -> CType -> ShowS

show :: CType -> String

showList :: [CType] -> ShowS

data Config

Plugin configuration for tactics

Constructors

Config

Fields

• cfg_max_use_ctor_actions :: Int
• cfg_timeout_seconds :: Int
• cfg_auto_gas :: Int

Instances

Eq Config

Defined in Wingman.Types

Methods

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

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

Ord Config

Defined in Wingman.Types

Methods

compare :: Config -> Config -> Ordering

(<) :: Config -> Config -> Bool

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

(>) :: Config -> Config -> Bool

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

max :: Config -> Config -> Config

min :: Config -> Config -> Config

Show Config

Defined in Wingman.Types

Methods

showsPrec :: Int -> Config -> ShowS

show :: Config -> String

showList :: [Config] -> ShowS

data TacticCommand

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

Destruct

DestructPun

Homomorphism

DestructLambdaCase

HomomorphismLambdaCase

DestructAll

UseDataCon

Refine

BeginMetaprogram

RunMetaprogram

Instances

Bounded TacticCommand

Defined in Wingman.Types

Methods

minBound :: TacticCommand

maxBound :: TacticCommand

Enum TacticCommand

Defined in Wingman.Types

Methods

succ :: TacticCommand -> TacticCommand

pred :: TacticCommand -> TacticCommand

toEnum :: Int -> TacticCommand

fromEnum :: TacticCommand -> Int

enumFrom :: TacticCommand -> [TacticCommand]

enumFromThen :: TacticCommand -> TacticCommand -> [TacticCommand]

enumFromTo :: TacticCommand -> TacticCommand -> [TacticCommand]

enumFromThenTo :: TacticCommand -> TacticCommand -> TacticCommand -> [TacticCommand]

Eq TacticCommand

Defined in Wingman.Types

Methods

(==) :: TacticCommand -> TacticCommand -> Bool

(/=) :: TacticCommand -> TacticCommand -> Bool

Ord TacticCommand

Defined in Wingman.Types

Methods

compare :: TacticCommand -> TacticCommand -> Ordering

(<) :: TacticCommand -> TacticCommand -> Bool

(<=) :: TacticCommand -> TacticCommand -> Bool

(>) :: TacticCommand -> TacticCommand -> Bool

(>=) :: TacticCommand -> TacticCommand -> Bool

max :: TacticCommand -> TacticCommand -> TacticCommand

min :: TacticCommand -> TacticCommand -> TacticCommand

Show TacticCommand

Defined in Wingman.Types

Methods

showsPrec :: Int -> TacticCommand -> ShowS

show :: TacticCommand -> String

showList :: [TacticCommand] -> ShowS

tacticTitle :: TacticCommand -> Text -> Text

Generate a title for the command.

emptyConfig :: Config

unsafeDefaultUniqueSupply :: UniqSupply

A UniqSupply to use in defaultTacticState

defaultTacticState :: TacticState

freshUnique :: MonadState TacticState m => m Unique

Generate a new Unique

overProvenance :: (Provenance -> Provenance) -> HyInfo a -> HyInfo a

Map a function over the provenance.

mapTrace :: (Trace -> Trace) -> Synthesized a -> Synthesized a

emptyContext :: Context

An empty context

dropEveryOther :: [a] -> [a]

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

module Wingman.Debug

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

Eq OccName

Defined in OccName

Methods

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

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

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

Defined in OccName

Methods

compare :: OccName -> OccName -> Ordering

(<) :: OccName -> OccName -> Bool

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

(>) :: OccName -> OccName -> Bool

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

max :: OccName -> OccName -> OccName

min :: OccName -> OccName -> OccName

Show OccName

Defined in Wingman.Types

Methods

showsPrec :: Int -> OccName -> ShowS

show :: OccName -> String

showList :: [OccName] -> ShowS

NFData OccName

Defined in OccName

Methods

rnf :: OccName -> ()

HasOccName OccName

Defined in OccName

Methods

occName :: OccName -> OccName

Binary OccName

Defined in OccName

Methods

put_ :: BinHandle -> OccName -> IO ()

put :: BinHandle -> OccName -> IO (Bin OccName)

get :: BinHandle -> IO OccName

Uniquable OccName

Defined in OccName

Methods

getUnique :: OccName -> Unique

Outputable OccName

Defined in OccName

Methods

ppr :: OccName -> SDoc

pprPrec :: Rational -> OccName -> SDoc

OutputableBndr OccName

Defined in OccName

Methods

pprBndr :: BindingSite -> OccName -> SDoc

pprPrefixOcc :: OccName -> SDoc

pprInfixOcc :: OccName -> SDoc

bndrIsJoin_maybe :: OccName -> Maybe Int

data Name

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

Instances

Eq Name

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

Defined in Name

Methods

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

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

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

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.

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

Defined in Wingman.Types

Methods

showsPrec :: Int -> Name -> ShowS

show :: Name -> String

showList :: [Name] -> ShowS

NFData Name

Defined in Name

Methods

rnf :: Name -> ()

NamedThing Name

Defined in Name

Methods

getOccName :: Name -> OccName

getName :: Name -> Name

HasOccName Name

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.

Defined in Name

Methods

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

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

get :: BinHandle -> IO Name

Uniquable Name

Defined in Name

Methods

getUnique :: Name -> Unique

HasSrcSpan Name

Defined in Name

Methods

composeSrcSpan :: Located (SrcSpanLess Name) -> Name

decomposeSrcSpan :: Name -> Located (SrcSpanLess Name)

Outputable Name

Defined in Name

Methods

ppr :: Name -> SDoc

pprPrec :: Rational -> Name -> SDoc

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

type SrcSpanLess Name = Name

data Type

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

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

Defined in Wingman.Types

Methods

showsPrec :: Int -> Type -> ShowS

show :: Type -> String

showList :: [Type] -> ShowS

Outputable Type

Defined in TyCoRep

Methods

ppr :: Type -> SDoc

pprPrec :: Rational -> Type -> SDoc

Eq (DeBruijn Type)

Defined in CoreMap

Methods

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

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

type TyVar = Var

Type or kind Variable

type Span = RealSrcSpan

Orphan instances

Show TCvSubst

Methods

showsPrec :: Int -> TCvSubst -> ShowS

show :: TCvSubst -> String

showList :: [TCvSubst] -> ShowS

Show Class

Methods

showsPrec :: Int -> Class -> ShowS

show :: Class -> String

showList :: [Class] -> ShowS

Show ConLike

Methods

showsPrec :: Int -> ConLike -> ShowS

show :: ConLike -> String

showList :: [ConLike] -> ShowS

Show DataCon

Methods

showsPrec :: Int -> DataCon -> ShowS

show :: DataCon -> String

showList :: [DataCon] -> ShowS

Show Type

Methods

showsPrec :: Int -> Type -> ShowS

show :: Type -> String

showList :: [Type] -> ShowS

Show Var

Methods

showsPrec :: Int -> Var -> ShowS

show :: Var -> String

showList :: [Var] -> ShowS

Show UniqSupply

Methods

showsPrec :: Int -> UniqSupply -> ShowS

show :: UniqSupply -> String

showList :: [UniqSupply] -> ShowS

Show TyCon

Methods

showsPrec :: Int -> TyCon -> ShowS

show :: TyCon -> String

showList :: [TyCon] -> ShowS

Show OccName

Methods

showsPrec :: Int -> OccName -> ShowS

show :: OccName -> String

showList :: [OccName] -> ShowS

Show Name

Methods

showsPrec :: Int -> Name -> ShowS

show :: Name -> String

showList :: [Name] -> ShowS

Show (HsDecl GhcPs)

Methods

showsPrec :: Int -> HsDecl GhcPs -> ShowS

show :: HsDecl GhcPs -> String

showList :: [HsDecl GhcPs] -> ShowS

Show (LHsSigType GhcPs)

Methods

showsPrec :: Int -> LHsSigType GhcPs -> ShowS

show :: LHsSigType GhcPs -> String

showList :: [LHsSigType GhcPs] -> ShowS

Show (HsExpr GhcPs)

Methods

showsPrec :: Int -> HsExpr GhcPs -> ShowS

show :: HsExpr GhcPs -> String

showList :: [HsExpr GhcPs] -> ShowS

Show (HsExpr GhcTc)

Methods

showsPrec :: Int -> HsExpr GhcTc -> ShowS

show :: HsExpr GhcTc -> String

showList :: [HsExpr GhcTc] -> ShowS

Show (Pat GhcPs)

Methods

showsPrec :: Int -> Pat GhcPs -> ShowS

show :: Pat GhcPs -> String

showList :: [Pat GhcPs] -> ShowS