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

Wingman.Machinery

Synopsis

Documentation

newSubgoal :: Judgement -> Rule Source #

Produce a subgoal that must be solved before we can solve the original goal.

runTactic Source #

Arguments

:: Int

Timeout

-> Context 
-> Judgement 
-> TacticsM ()

Tactic to use

-> IO (Either [TacticError] RunTacticResults) 

Attempt to generate a term of the right type using in-scope bindings, and a given tactic.

tracing :: Functor m => String -> TacticT jdg (Synthesized ext) err s m a -> TacticT jdg (Synthesized ext) err s m a Source #

Mark that a tactic used the given string in its extract derivation. Mainly used for debugging the search when things go terribly wrong.

markRecursion :: Functor m => TacticT jdg (Synthesized ext) err s m a -> TacticT jdg (Synthesized ext) err s m a Source #

Mark that a tactic performed recursion. Doing so incurs a small penalty in the score.

mappingExtract :: Functor m => (ext -> ext) -> TacticT jdg ext err s m a -> TacticT jdg ext err s m a Source #

Map a function over the extract created by a tactic.

scoreSolution :: Synthesized (LHsExpr GhcPs) -> Judgement -> [Judgement] -> (Penalize Int, Reward Bool, Penalize Int, Penalize Int, Reward Int, Penalize Int, Penalize Int) Source #

Given the results of running a tactic, score the solutions by desirability.

NOTE: This function is completely unprincipled and was just hacked together to produce the right test results.

solutionSize :: LHsExpr GhcPs -> Int Source #

Compute the number of LHsExpr nodes; used as a rough metric for code size.

newtype Penalize a Source #

Constructors

Penalize a 

Instances

Instances details
Eq a => Eq (Penalize a) Source # 
Instance details

Defined in Wingman.Machinery

Methods

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

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

Ord a => Ord (Penalize a) Source # 
Instance details

Defined in Wingman.Machinery

Methods

compare :: Penalize a -> Penalize a -> Ordering #

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

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

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

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

max :: Penalize a -> Penalize a -> Penalize a #

min :: Penalize a -> Penalize a -> Penalize a #

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

Defined in Wingman.Machinery

Methods

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

show :: Penalize a -> String #

showList :: [Penalize a] -> ShowS #

newtype Reward a Source #

Constructors

Reward a 

Instances

Instances details
Eq a => Eq (Reward a) Source # 
Instance details

Defined in Wingman.Machinery

Methods

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

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

Ord a => Ord (Reward a) Source # 
Instance details

Defined in Wingman.Machinery

Methods

compare :: Reward a -> Reward a -> Ordering #

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

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

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

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

max :: Reward a -> Reward a -> Reward a #

min :: Reward a -> Reward a -> Reward a #

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

Defined in Wingman.Machinery

Methods

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

show :: Reward a -> String #

showList :: [Reward a] -> ShowS #

newUnivar :: MonadState TacticState m => m Type Source #

Generate a unique unification variable.

unify Source #

Arguments

:: CType

The goal type

-> CType

The type we are trying unify the goal type with

-> RuleM () 

Attempt to unify two types.

learnFromFundeps :: ThetaType -> RuleM () Source #

Get a substition out of a theta's fundeps

cut :: RuleT jdg ext err s m a Source #

canUnify Source #

Arguments

:: MonadState TacticState m 
=> CType

The goal type

-> CType

The type we are trying unify the goal type with

-> m Bool 

Attempt to unify two types.

attemptWhen :: TacticsM a -> TacticsM a -> Bool -> TacticsM a Source #

Prefer the first tactic to the second, if the bool is true. Otherwise, just run the second tactic.

This is useful when you have a clever pruning solution that isn't always applicable.

requireConcreteHole :: TacticsM a -> TacticsM a Source #

Run the given tactic iff the current hole contains no univars. Skolems and already decided univars are OK though.

try' :: Functor m => TacticT jdg ext err s m () -> TacticT jdg ext err s m () Source #

The try that comes in refinery 0.3 causes unnecessary backtracking and balloons the search space. This thing just tries it, but doesn't backtrack if it fails.

NOTE(sandy): But there's a bug! Or at least, something not understood here. Using this everywhere breaks te tests, and neither I nor TOTBWF are sure why. Prefer try if you can, and only try this as a last resort.

TODO(sandy): Remove this when we upgrade to 0.4

exact :: HsExpr GhcPs -> TacticsM () Source #

Sorry leaves a hole in its extract

useNameFromHypothesis :: (HyInfo CType -> TacticsM a) -> OccName -> TacticsM a Source #

Lift a function over HyInfos to one that takes an OccName and tries to look it up in the hypothesis.

useNameFromContext :: (HyInfo CType -> TacticsM a) -> OccName -> TacticsM a Source #

Lift a function over HyInfos to one that takes an OccName and tries to look it up in the hypothesis.

lookupNameInContext :: MonadReader Context m => OccName -> m (Maybe CType) Source #

Find the type of an OccName that is defined in the current module.

createImportedHyInfo :: OccName -> CType -> HyInfo CType Source #

Build a HyInfo for an imported term.

knownClass :: OccName -> TacticsM (Maybe Class) Source #

Like getTyThing but specialized to classes.

getKnownInstance :: OccName -> [Type] -> TacticsM (Maybe (Class, PredType)) Source #

Like getInstance, but uses a class that it just looked up.

getOccNameType :: OccName -> TacticsM Type Source #

Lookup the type of any OccName that was imported. Necessarily done in IO, so we only expose this functionality to the parser. Internal Haskell code that wants to lookup terms should do it via KnownThings.

uncoveredDataCons :: Type -> Type -> Maybe (Set (Uniquely DataCon)) Source #

Given two types, see if we can construct a homomorphism by mapping every data constructor in the domain to the same in the codomain. This function returns Just when all the lookups succeeded, and a non-empty value if the homomorphism *is not* possible.