Ide.Plugin.Tactic.Machinery

Documentation

newtype Reward a

Constructors

Reward a

Instances

Eq a => Eq (Reward a)

Defined in Ide.Plugin.Tactic.Machinery

Methods

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

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

Ord a => Ord (Reward a)

Defined in Ide.Plugin.Tactic.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 Ide.Plugin.Tactic.Machinery

Methods

showsPrec :: Int -> Reward a -> ShowS

show :: Reward a -> String

showList :: [Reward a] -> ShowS

newtype Penalize a

Constructors

Penalize a

Instances

Eq a => Eq (Penalize a)

Defined in Ide.Plugin.Tactic.Machinery

Methods

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

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

Ord a => Ord (Penalize a)

Defined in Ide.Plugin.Tactic.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 Ide.Plugin.Tactic.Machinery

Methods

showsPrec :: Int -> Penalize a -> ShowS

show :: Penalize a -> String

showList :: [Penalize a] -> ShowS

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 (Trace, ext) err s m a -> TacticT jdg (Trace, ext) err s m a

guardStructurallySmallerRecursion :: TacticState -> Maybe TacticError

Recursion is allowed only when we can prove it is on a structurally smaller argument. The top of the ts_recursion_stack witnesses the smaller pattern val.

markStructuralySmallerRecursion :: MonadState TacticState m => PatVal -> m ()

Mark that the current recursive call is structurally smaller, due to having been matched on a pattern value.

Implemented by setting the top of the ts_recursion_stack.

scoreSolution :: LHsExpr GhcPs -> TacticState -> [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.

TODO(sandy): 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.

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

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

unify

Arguments

:: CType

The goal type

-> CType

The type we are trying unify the goal type with

-> RuleM ()

Attempt to unify two types.

methodHypothesis :: PredType -> Maybe [(OccName, HyInfo CType)]

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

requireConcreteHole :: TacticsM a -> TacticsM a

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