Safe Haskell	None
Language	Haskell2010

Wingman.Machinery

Synopsis

substCTy :: TCvSubst -> CType -> CType
getSubstForJudgement :: MonadState TacticState m => Judgement -> m TCvSubst
newSubgoal :: Judgement -> Rule
tacticToRule :: Judgement -> TacticsM () -> Rule
consumeChan :: OutChan (Maybe a) -> IO [a]
runTactic :: Int -> Context -> Judgement -> TacticsM () -> IO (Either [TacticError] RunTacticResults)
tracePrim :: String -> Trace
tracing :: Functor m => String -> TacticT jdg (Synthesized ext) err s m a -> TacticT jdg (Synthesized ext) err s m a
markRecursion :: Functor m => TacticT jdg (Synthesized ext) err s m a -> TacticT jdg (Synthesized ext) err s m a
mappingExtract :: Functor m => (ext -> ext) -> TacticT jdg ext err s m a -> TacticT jdg ext err s m a
scoreSolution :: Synthesized (LHsExpr GhcPs) -> Judgement -> [Judgement] -> (Penalize Int, Reward Bool, Penalize Int, Penalize Int, Reward Int, Penalize Int, Penalize Int)
solutionSize :: LHsExpr GhcPs -> Int
newtype Penalize a = Penalize a
newtype Reward a = Reward a
newUnivar :: MonadState TacticState m => m Type
unify :: CType -> CType -> RuleM ()
learnFromFundeps :: ThetaType -> RuleM ()
cut :: RuleT jdg ext err s m a
canUnify :: MonadState TacticState m => CType -> CType -> m Bool
attemptWhen :: TacticsM a -> TacticsM a -> Bool -> TacticsM a
requireConcreteHole :: TacticsM a -> TacticsM a
try' :: Functor m => TacticT jdg ext err s m () -> TacticT jdg ext err s m ()
exact :: HsExpr GhcPs -> TacticsM ()
useNameFromHypothesis :: (HyInfo CType -> TacticsM a) -> OccName -> TacticsM a
useNameFromContext :: (HyInfo CType -> TacticsM a) -> OccName -> TacticsM a
lookupNameInContext :: MonadReader Context m => OccName -> m (Maybe CType)
getDefiningType :: TacticsM CType
createImportedHyInfo :: OccName -> CType -> HyInfo CType
getTyThing :: OccName -> TacticsM (Maybe TyThing)
knownClass :: OccName -> TacticsM (Maybe Class)
getKnownInstance :: OccName -> [Type] -> TacticsM (Maybe (Class, PredType))
getOccNameType :: OccName -> TacticsM Type
getCurrentDefinitions :: TacticsM [(OccName, CType)]
uncoveredDataCons :: Type -> Type -> Maybe (Set (Uniquely DataCon))

Documentation

substCTy :: TCvSubst -> CType -> CType Source #

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

newSubgoal :: Judgement -> Rule Source #

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

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

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

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.

tracePrim :: String -> Trace Source #

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.

getDefiningType :: TacticsM CType Source #

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

Build a HyInfo for an imported term.

getTyThing :: OccName -> TacticsM (Maybe TyThing) Source #

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.

getCurrentDefinitions :: TacticsM [(OccName, CType)] Source #

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.