Wingman.Machinery

Documentation

substCTy :: TCvSubst -> CType -> CType

getSubstForJudgement :: MonadState TacticState m => Judgement -> m TCvSubst

newSubgoal :: Judgement -> Rule

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

tacticToRule :: Judgement -> TacticsM () -> Rule

consumeChan :: OutChan (Maybe a) -> IO [a]

runTactic

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.

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

newUnivar :: MonadState TacticState m => m Type

Generate a unique unification variable.

unify

Arguments

:: CType

The goal type

-> CType

The type we are trying unify the goal type with

-> RuleM ()

Attempt to unify two types.

cut :: RuleT jdg ext err s m a

canUnify

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

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

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

exact :: HsExpr GhcPs -> TacticsM ()

Sorry leaves a hole in its extract

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

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

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)

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

getDefiningType :: TacticsM CType

createImportedHyInfo :: OccName -> CType -> HyInfo CType

Build a HyInfo for an imported term.

getTyThing :: OccName -> TacticsM (Maybe TyThing)

knownClass :: OccName -> TacticsM (Maybe Class)

Like getTyThing but specialized to classes.

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

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

getOccNameType :: OccName -> TacticsM Type

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.

getCurrentDefinitions :: TacticsM [(OccName, CType)]

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

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.