Wingman.Machinery

Documentation

substCTy :: TCvSubst -> CType -> CType

newSubgoal :: Judgement -> Rule

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

runTactic

Arguments

:: Context

-> Judgement

-> TacticsM ()

Tactic to use

-> Either [TacticError] RunTacticResults

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

assoc23 :: (a, b, c) -> (a, (b, c))

tracePrim :: String -> Trace

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

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

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

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)

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

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

newtype Penalize a

Constructors

Penalize a

Instances

Eq a => Eq (Penalize a)

Defined in Wingman.Machinery

Methods

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

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

Ord a => Ord (Penalize a)

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)

Defined in Wingman.Machinery

Methods

showsPrec :: Int -> Penalize a -> ShowS

show :: Penalize a -> String

showList :: [Penalize a] -> ShowS

newtype Reward a

Constructors

Reward a

Instances

Eq a => Eq (Reward a)

Defined in Wingman.Machinery

Methods

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

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

Ord a => Ord (Reward a)

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)

Defined in Wingman.Machinery

Methods

showsPrec :: Int -> Reward a -> ShowS

show :: Reward a -> String

showList :: [Reward a] -> ShowS

tryUnifyUnivarsButNotSkolems :: Set TyVar -> CType -> CType -> Maybe TCvSubst

Like tcUnifyTy, but takes a list of skolems to prevent unification of.

updateSubst :: TCvSubst -> TacticState -> TacticState

unify

Arguments

:: CType

The goal type

-> CType

The type we are trying unify the goal type with

-> RuleM ()

Attempt to unify two types.

attemptWhen :: TacticsM a -> TacticsM a -> Bool -> TacticsM a

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.

methodHypothesis :: PredType -> Maybe [HyInfo CType]

Get the class methods of a PredType, correctly dealing with instantiation of quantified class types.

peek :: (ext -> TacticT jdg ext err s m ()) -> TacticT jdg ext err s m ()

Mystical time-traveling combinator for inspecting the extracts produced by a tactic. We can use it to guard that extracts match certain predicates, for example.

Note, that this thing is WEIRD. To illustrate:

@ peek f blah @

Here, f can inspect the extract _produced by blah,_ which means the causality appears to go backwards.

peek should be exposed directly by refinery in the next release.

requireConcreteHole :: TacticsM a -> TacticsM a

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

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