{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE TupleSections   #-}

module Wingman.Machinery where

import           Control.Applicative (empty)
import           Control.Lens ((<>~))
import           Control.Monad.Reader
import           Control.Monad.State.Class (gets, modify, MonadState)
import           Control.Monad.State.Strict (StateT (..), execStateT)
import           Control.Monad.Trans.Maybe
import           Data.Coerce
import           Data.Foldable
import           Data.Functor ((<&>))
import           Data.Generics (everything, gcount, mkQ)
import           Data.Generics.Product (field')
import           Data.List (sortBy)
import qualified Data.Map as M
import           Data.Maybe (mapMaybe)
import           Data.Monoid (getSum)
import           Data.Ord (Down (..), comparing)
import qualified Data.Set as S
import           Data.Traversable (for)
import           Development.IDE.Core.Compile (lookupName)
import           Development.IDE.GHC.Compat
import           GhcPlugins (GlobalRdrElt (gre_name), lookupOccEnv, varType)
import           Refinery.ProofState
import           Refinery.Tactic
import           Refinery.Tactic.Internal
import           TcType
import           Type (tyCoVarsOfTypeWellScoped)
import           Wingman.Context (getInstance)
import           Wingman.GHC (tryUnifyUnivarsButNotSkolems, updateSubst, tacticsGetDataCons)
import           Wingman.Judgements
import           Wingman.Simplify (simplify)
import           Wingman.Types


substCTy :: TCvSubst -> CType -> CType
substCTy :: TCvSubst -> CType -> CType
substCTy TCvSubst
subst = Type -> CType
coerce (Type -> CType) -> (CType -> Type) -> CType -> CType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HasCallStack => TCvSubst -> Type -> Type
TCvSubst -> Type -> Type
substTy TCvSubst
subst (Type -> Type) -> (CType -> Type) -> CType -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CType -> Type
coerce


getSubstForJudgement
    :: MonadState TacticState m
    => Judgement
    -> m TCvSubst
getSubstForJudgement :: Judgement -> m TCvSubst
getSubstForJudgement Judgement
j = do
  -- NOTE(sandy): It's OK to use mempty here, because coercions _can_ give us
  -- substitutions for skolems.
  let coercions :: TCvSubst
coercions = Judgement -> TCvSubst
forall a. Judgement' a -> TCvSubst
j_coercion Judgement
j
  TCvSubst
unifier <- (TacticState -> TCvSubst) -> m TCvSubst
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets TacticState -> TCvSubst
ts_unifier
  TCvSubst -> m TCvSubst
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TCvSubst -> m TCvSubst) -> TCvSubst -> m TCvSubst
forall a b. (a -> b) -> a -> b
$ TCvSubst -> TCvSubst -> TCvSubst
unionTCvSubst TCvSubst
unifier TCvSubst
coercions

------------------------------------------------------------------------------
-- | Produce a subgoal that must be solved before we can solve the original
-- goal.
newSubgoal
    :: Judgement
    -> Rule
newSubgoal :: Judgement -> Rule
newSubgoal Judgement
j = do
  Context
ctx <- RuleT
  Judgement
  (Synthesized (LHsExpr GhcPs))
  TacticError
  TacticState
  ExtractM
  Context
forall r (m :: * -> *). MonadReader r m => m r
ask
  TCvSubst
unifier <- Judgement
-> RuleT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     TCvSubst
forall (m :: * -> *).
MonadState TacticState m =>
Judgement -> m TCvSubst
getSubstForJudgement Judgement
j
  Judgement -> Rule
forall jdg ext err s (m :: * -> *).
jdg -> RuleT jdg ext err s m ext
subgoal
    (Judgement -> Rule) -> Judgement -> Rule
forall a b. (a -> b) -> a -> b
$ Context -> Judgement -> Judgement
forall (f :: * -> *). Functor f => Context -> f CType -> f CType
normalizeJudgement Context
ctx
    (Judgement -> Judgement) -> Judgement -> Judgement
forall a b. (a -> b) -> a -> b
$ TCvSubst -> Judgement -> Judgement
substJdg TCvSubst
unifier
    (Judgement -> Judgement) -> Judgement -> Judgement
forall a b. (a -> b) -> a -> b
$ Judgement -> Judgement
forall a. Judgement' a -> Judgement' a
unsetIsTopHole
    (Judgement -> Judgement) -> Judgement -> Judgement
forall a b. (a -> b) -> a -> b
$ Context -> Judgement -> Judgement
forall (f :: * -> *). Functor f => Context -> f CType -> f CType
normalizeJudgement Context
ctx Judgement
j


tacticToRule :: Judgement -> TacticsM () -> Rule
tacticToRule :: Judgement -> TacticsM () -> Rule
tacticToRule Judgement
jdg (TacticT StateT
  Judgement
  (ProofStateT
     (Synthesized (LHsExpr GhcPs))
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM)
  ()
tt) = ProofStateT
  (Synthesized (LHsExpr GhcPs))
  (Synthesized (LHsExpr GhcPs))
  TacticError
  TacticState
  ExtractM
  Judgement
-> Rule
forall jdg ext err s (m :: * -> *) a.
ProofStateT ext a err s m jdg -> RuleT jdg ext err s m a
RuleT (ProofStateT
   (Synthesized (LHsExpr GhcPs))
   (Synthesized (LHsExpr GhcPs))
   TacticError
   TacticState
   ExtractM
   Judgement
 -> Rule)
-> ProofStateT
     (Synthesized (LHsExpr GhcPs))
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     Judgement
-> Rule
forall a b. (a -> b) -> a -> b
$ (StateT
   Judgement
   (ProofStateT
      (Synthesized (LHsExpr GhcPs))
      (Synthesized (LHsExpr GhcPs))
      TacticError
      TacticState
      ExtractM)
   ()
 -> Judgement
 -> ProofStateT
      (Synthesized (LHsExpr GhcPs))
      (Synthesized (LHsExpr GhcPs))
      TacticError
      TacticState
      ExtractM
      Judgement)
-> Judgement
-> StateT
     Judgement
     (ProofStateT
        (Synthesized (LHsExpr GhcPs))
        (Synthesized (LHsExpr GhcPs))
        TacticError
        TacticState
        ExtractM)
     ()
-> ProofStateT
     (Synthesized (LHsExpr GhcPs))
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     Judgement
forall a b c. (a -> b -> c) -> b -> a -> c
flip StateT
  Judgement
  (ProofStateT
     (Synthesized (LHsExpr GhcPs))
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM)
  ()
-> Judgement
-> ProofStateT
     (Synthesized (LHsExpr GhcPs))
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     Judgement
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m s
execStateT Judgement
jdg StateT
  Judgement
  (ProofStateT
     (Synthesized (LHsExpr GhcPs))
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM)
  ()
tt ProofStateT
  (Synthesized (LHsExpr GhcPs))
  (Synthesized (LHsExpr GhcPs))
  TacticError
  TacticState
  ExtractM
  Judgement
-> (Judgement
    -> ProofStateT
         (Synthesized (LHsExpr GhcPs))
         (Synthesized (LHsExpr GhcPs))
         TacticError
         TacticState
         ExtractM
         Judgement)
-> ProofStateT
     (Synthesized (LHsExpr GhcPs))
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     Judgement
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (Judgement
 -> (Synthesized (LHsExpr GhcPs)
     -> ProofStateT
          (Synthesized (LHsExpr GhcPs))
          (Synthesized (LHsExpr GhcPs))
          TacticError
          TacticState
          ExtractM
          Judgement)
 -> ProofStateT
      (Synthesized (LHsExpr GhcPs))
      (Synthesized (LHsExpr GhcPs))
      TacticError
      TacticState
      ExtractM
      Judgement)
-> (Synthesized (LHsExpr GhcPs)
    -> ProofStateT
         (Synthesized (LHsExpr GhcPs))
         (Synthesized (LHsExpr GhcPs))
         TacticError
         TacticState
         ExtractM
         Judgement)
-> Judgement
-> ProofStateT
     (Synthesized (LHsExpr GhcPs))
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     Judgement
forall a b c. (a -> b -> c) -> b -> a -> c
flip Judgement
-> (Synthesized (LHsExpr GhcPs)
    -> ProofStateT
         (Synthesized (LHsExpr GhcPs))
         (Synthesized (LHsExpr GhcPs))
         TacticError
         TacticState
         ExtractM
         Judgement)
-> ProofStateT
     (Synthesized (LHsExpr GhcPs))
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     Judgement
forall ext' ext err s (m :: * -> *) goal.
goal
-> (ext' -> ProofStateT ext' ext err s m goal)
-> ProofStateT ext' ext err s m goal
Subgoal Synthesized (LHsExpr GhcPs)
-> ProofStateT
     (Synthesized (LHsExpr GhcPs))
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     Judgement
forall ext' ext err s (m :: * -> *) goal.
ext -> ProofStateT ext' ext err s m goal
Axiom


------------------------------------------------------------------------------
-- | Attempt to generate a term of the right type using in-scope bindings, and
-- a given tactic.
runTactic
    :: Context
    -> Judgement
    -> TacticsM ()       -- ^ Tactic to use
    -> IO (Either [TacticError] RunTacticResults)
runTactic :: Context
-> Judgement
-> TacticsM ()
-> IO (Either [TacticError] RunTacticResults)
runTactic Context
ctx Judgement
jdg TacticsM ()
t = do
    let skolems :: Set TyVar
skolems = [TyVar] -> Set TyVar
forall a. Ord a => [a] -> Set a
S.fromList
                ([TyVar] -> Set TyVar) -> [TyVar] -> Set TyVar
forall a b. (a -> b) -> a -> b
$ (CType -> [TyVar]) -> [CType] -> [TyVar]
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (Type -> [TyVar]
tyCoVarsOfTypeWellScoped (Type -> [TyVar]) -> (CType -> Type) -> CType -> [TyVar]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CType -> Type
unCType)
                ([CType] -> [TyVar]) -> [CType] -> [TyVar]
forall a b. (a -> b) -> a -> b
$ (:) (Judgement -> CType
forall a. Judgement' a -> a
jGoal Judgement
jdg)
                ([CType] -> [CType]) -> [CType] -> [CType]
forall a b. (a -> b) -> a -> b
$ (HyInfo CType -> CType) -> [HyInfo CType] -> [CType]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap HyInfo CType -> CType
forall a. HyInfo a -> a
hi_type
                ([HyInfo CType] -> [CType]) -> [HyInfo CType] -> [CType]
forall a b. (a -> b) -> a -> b
$ Map OccName (HyInfo CType) -> [HyInfo CType]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList
                (Map OccName (HyInfo CType) -> [HyInfo CType])
-> Map OccName (HyInfo CType) -> [HyInfo CType]
forall a b. (a -> b) -> a -> b
$ Hypothesis CType -> Map OccName (HyInfo CType)
forall a. Hypothesis a -> Map OccName (HyInfo a)
hyByName
                (Hypothesis CType -> Map OccName (HyInfo CType))
-> Hypothesis CType -> Map OccName (HyInfo CType)
forall a b. (a -> b) -> a -> b
$ Judgement -> Hypothesis CType
forall a. Judgement' a -> Hypothesis a
jHypothesis Judgement
jdg
        tacticState :: TacticState
tacticState =
          TacticState
defaultTacticState
            { ts_skolems :: Set TyVar
ts_skolems = Set TyVar
skolems
            }
    Either
  [TacticError]
  [Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))]
res <- (ReaderT
   Context
   IO
   (Either
      [TacticError]
      [Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))])
 -> Context
 -> IO
      (Either
         [TacticError]
         [Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))]))
-> Context
-> ReaderT
     Context
     IO
     (Either
        [TacticError]
        [Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))])
-> IO
     (Either
        [TacticError]
        [Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))])
forall a b c. (a -> b -> c) -> b -> a -> c
flip ReaderT
  Context
  IO
  (Either
     [TacticError]
     [Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))])
-> Context
-> IO
     (Either
        [TacticError]
        [Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))])
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT Context
ctx
         (ReaderT
   Context
   IO
   (Either
      [TacticError]
      [Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))])
 -> IO
      (Either
         [TacticError]
         [Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))]))
-> (ExtractM
      (Either
         [TacticError]
         [Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))])
    -> ReaderT
         Context
         IO
         (Either
            [TacticError]
            [Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))]))
-> ExtractM
     (Either
        [TacticError]
        [Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))])
-> IO
     (Either
        [TacticError]
        [Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ExtractM
  (Either
     [TacticError]
     [Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))])
-> ReaderT
     Context
     IO
     (Either
        [TacticError]
        [Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))])
forall a. ExtractM a -> ReaderT Context IO a
unExtractM
         (ExtractM
   (Either
      [TacticError]
      [Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))])
 -> IO
      (Either
         [TacticError]
         [Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))]))
-> ExtractM
     (Either
        [TacticError]
        [Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))])
-> IO
     (Either
        [TacticError]
        [Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))])
forall a b. (a -> b) -> a -> b
$ TacticsM ()
-> Judgement
-> TacticState
-> ExtractM
     (Either
        [TacticError]
        [Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))])
forall meta ext err s (m :: * -> *) jdg.
MonadExtract meta ext err s m =>
TacticT jdg ext err s m ()
-> jdg -> s -> m (Either [err] [Proof s meta jdg ext])
runTacticT TacticsM ()
t Judgement
jdg TacticState
tacticState
    Either [TacticError] RunTacticResults
-> IO (Either [TacticError] RunTacticResults)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either [TacticError] RunTacticResults
 -> IO (Either [TacticError] RunTacticResults))
-> Either [TacticError] RunTacticResults
-> IO (Either [TacticError] RunTacticResults)
forall a b. (a -> b) -> a -> b
$ case Either
  [TacticError]
  [Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))]
res of
      (Left [TacticError]
errs) -> [TacticError] -> Either [TacticError] RunTacticResults
forall a b. a -> Either a b
Left ([TacticError] -> Either [TacticError] RunTacticResults)
-> [TacticError] -> Either [TacticError] RunTacticResults
forall a b. (a -> b) -> a -> b
$ Int -> [TacticError] -> [TacticError]
forall a. Int -> [a] -> [a]
take Int
50 [TacticError]
errs
      (Right [Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))]
solns) -> do
        let sorted :: [Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))]
sorted =
              ((Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))
  -> Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))
  -> Ordering)
 -> [Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))]
 -> [Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))])
-> [Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))]
-> (Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))
    -> Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))
    -> Ordering)
-> [Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))]
forall a b c. (a -> b -> c) -> b -> a -> c
flip (Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))
 -> Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))
 -> Ordering)
-> [Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))]
-> [Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy [Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))]
solns ((Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))
  -> Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))
  -> Ordering)
 -> [Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))])
-> (Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))
    -> Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))
    -> Ordering)
-> [Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))]
forall a b. (a -> b) -> a -> b
$ (Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))
 -> Down
      (Penalize Int, Reward Bool, Penalize Int, Penalize Int, Reward Int,
       Penalize Int, Penalize Int))
-> Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))
-> Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))
-> Ordering
forall a b. Ord a => (b -> a) -> b -> b -> Ordering
comparing ((Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))
  -> Down
       (Penalize Int, Reward Bool, Penalize Int, Penalize Int, Reward Int,
        Penalize Int, Penalize Int))
 -> Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))
 -> Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))
 -> Ordering)
-> (Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))
    -> Down
         (Penalize Int, Reward Bool, Penalize Int, Penalize Int, Reward Int,
          Penalize Int, Penalize Int))
-> Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))
-> Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))
-> Ordering
forall a b. (a -> b) -> a -> b
$ \(Proof Synthesized (LHsExpr GhcPs)
ext TacticState
_ [(Int, Judgement)]
holes) ->
                (Penalize Int, Reward Bool, Penalize Int, Penalize Int, Reward Int,
 Penalize Int, Penalize Int)
-> Down
     (Penalize Int, Reward Bool, Penalize Int, Penalize Int, Reward Int,
      Penalize Int, Penalize Int)
forall a. a -> Down a
Down ((Penalize Int, Reward Bool, Penalize Int, Penalize Int,
  Reward Int, Penalize Int, Penalize Int)
 -> Down
      (Penalize Int, Reward Bool, Penalize Int, Penalize Int, Reward Int,
       Penalize Int, Penalize Int))
-> (Penalize Int, Reward Bool, Penalize Int, Penalize Int,
    Reward Int, Penalize Int, Penalize Int)
-> Down
     (Penalize Int, Reward Bool, Penalize Int, Penalize Int, Reward Int,
      Penalize Int, Penalize Int)
forall a b. (a -> b) -> a -> b
$ Synthesized (LHsExpr GhcPs)
-> Judgement
-> [Judgement]
-> (Penalize Int, Reward Bool, Penalize Int, Penalize Int,
    Reward Int, Penalize Int, Penalize Int)
scoreSolution Synthesized (LHsExpr GhcPs)
ext Judgement
jdg ([Judgement]
 -> (Penalize Int, Reward Bool, Penalize Int, Penalize Int,
     Reward Int, Penalize Int, Penalize Int))
-> [Judgement]
-> (Penalize Int, Reward Bool, Penalize Int, Penalize Int,
    Reward Int, Penalize Int, Penalize Int)
forall a b. (a -> b) -> a -> b
$ ((Int, Judgement) -> Judgement)
-> [(Int, Judgement)] -> [Judgement]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Int, Judgement) -> Judgement
forall a b. (a, b) -> b
snd [(Int, Judgement)]
holes
        case [Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))]
sorted of
          ((Proof Synthesized (LHsExpr GhcPs)
syn TacticState
_ [(Int, Judgement)]
subgoals) : [Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))]
_) ->
            RunTacticResults -> Either [TacticError] RunTacticResults
forall a b. b -> Either a b
Right (RunTacticResults -> Either [TacticError] RunTacticResults)
-> RunTacticResults -> Either [TacticError] RunTacticResults
forall a b. (a -> b) -> a -> b
$
              RunTacticResults :: Trace
-> LHsExpr GhcPs
-> [Judgement]
-> [Synthesized (LHsExpr GhcPs)]
-> Judgement
-> Context
-> RunTacticResults
RunTacticResults
                { rtr_trace :: Trace
rtr_trace    = Synthesized (LHsExpr GhcPs) -> Trace
forall a. Synthesized a -> Trace
syn_trace Synthesized (LHsExpr GhcPs)
syn
                , rtr_extract :: LHsExpr GhcPs
rtr_extract  = LHsExpr GhcPs -> LHsExpr GhcPs
simplify (LHsExpr GhcPs -> LHsExpr GhcPs) -> LHsExpr GhcPs -> LHsExpr GhcPs
forall a b. (a -> b) -> a -> b
$ Synthesized (LHsExpr GhcPs) -> LHsExpr GhcPs
forall a. Synthesized a -> a
syn_val Synthesized (LHsExpr GhcPs)
syn
                , rtr_subgoals :: [Judgement]
rtr_subgoals = ((Int, Judgement) -> Judgement)
-> [(Int, Judgement)] -> [Judgement]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Int, Judgement) -> Judgement
forall a b. (a, b) -> b
snd [(Int, Judgement)]
subgoals
                , rtr_other_solns :: [Synthesized (LHsExpr GhcPs)]
rtr_other_solns = [Synthesized (LHsExpr GhcPs)] -> [Synthesized (LHsExpr GhcPs)]
forall a. [a] -> [a]
reverse ([Synthesized (LHsExpr GhcPs)] -> [Synthesized (LHsExpr GhcPs)])
-> ([Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))]
    -> [Synthesized (LHsExpr GhcPs)])
-> [Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))]
-> [Synthesized (LHsExpr GhcPs)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))
 -> Synthesized (LHsExpr GhcPs))
-> [Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))]
-> [Synthesized (LHsExpr GhcPs)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))
-> Synthesized (LHsExpr GhcPs)
forall s meta goal ext. Proof s meta goal ext -> ext
pf_extract ([Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))]
 -> [Synthesized (LHsExpr GhcPs)])
-> [Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))]
-> [Synthesized (LHsExpr GhcPs)]
forall a b. (a -> b) -> a -> b
$ [Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))]
sorted
                , rtr_jdg :: Judgement
rtr_jdg = Judgement
jdg
                , rtr_ctx :: Context
rtr_ctx = Context
ctx
                }
          -- guaranteed to not be empty
          [Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))]
_ -> [TacticError] -> Either [TacticError] RunTacticResults
forall a b. a -> Either a b
Left []

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


tracePrim :: String -> Trace
tracePrim :: String -> Trace
tracePrim = (String -> [Trace] -> Trace) -> [Trace] -> String -> Trace
forall a b c. (a -> b -> c) -> b -> a -> c
flip String -> [Trace] -> Trace
forall a. (Eq a, Monoid a) => a -> [Rose a] -> Rose a
rose []


------------------------------------------------------------------------------
-- | Mark that a tactic used the given string in its extract derivation. Mainly
-- used for debugging the search when things go terribly wrong.
tracing
    :: Functor m
    => String
    -> TacticT jdg (Synthesized ext) err s m a
    -> TacticT jdg (Synthesized ext) err s m a
tracing :: String
-> TacticT jdg (Synthesized ext) err s m a
-> TacticT jdg (Synthesized ext) err s m a
tracing String
s = (Synthesized ext -> Synthesized ext)
-> TacticT jdg (Synthesized ext) err s m a
-> TacticT jdg (Synthesized ext) err s m a
forall (m :: * -> *) ext jdg err s a.
Functor m =>
(ext -> ext)
-> TacticT jdg ext err s m a -> TacticT jdg ext err s m a
mappingExtract ((Trace -> Trace) -> Synthesized ext -> Synthesized ext
forall a. (Trace -> Trace) -> Synthesized a -> Synthesized a
mapTrace ((Trace -> Trace) -> Synthesized ext -> Synthesized ext)
-> (Trace -> Trace) -> Synthesized ext -> Synthesized ext
forall a b. (a -> b) -> a -> b
$ String -> [Trace] -> Trace
forall a. (Eq a, Monoid a) => a -> [Rose a] -> Rose a
rose String
s ([Trace] -> Trace) -> (Trace -> [Trace]) -> Trace -> Trace
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Trace -> [Trace]
forall (f :: * -> *) a. Applicative f => a -> f a
pure)


------------------------------------------------------------------------------
-- | Mark that a tactic performed recursion. Doing so incurs a small penalty in
-- the score.
markRecursion
    :: Functor m
    => TacticT jdg (Synthesized ext) err s m a
    -> TacticT jdg (Synthesized ext) err s m a
markRecursion :: TacticT jdg (Synthesized ext) err s m a
-> TacticT jdg (Synthesized ext) err s m a
markRecursion = (Synthesized ext -> Synthesized ext)
-> TacticT jdg (Synthesized ext) err s m a
-> TacticT jdg (Synthesized ext) err s m a
forall (m :: * -> *) ext jdg err s a.
Functor m =>
(ext -> ext)
-> TacticT jdg ext err s m a -> TacticT jdg ext err s m a
mappingExtract (forall s a. HasField' "syn_recursion_count" s a => Lens s s a a
forall (field :: Symbol) s a. HasField' field s a => Lens s s a a
field' @"syn_recursion_count" ((Sum Int -> Identity (Sum Int))
 -> Synthesized ext -> Identity (Synthesized ext))
-> Sum Int -> Synthesized ext -> Synthesized ext
forall a s t. Semigroup a => ASetter s t a a -> a -> s -> t
<>~ Sum Int
1)


------------------------------------------------------------------------------
-- | Map a function over the extract created by a tactic.
mappingExtract
    :: Functor m
    => (ext -> ext)
    -> TacticT jdg ext err s m a
    -> TacticT jdg ext err s m a
mappingExtract :: (ext -> ext)
-> TacticT jdg ext err s m a -> TacticT jdg ext err s m a
mappingExtract ext -> ext
f (TacticT StateT jdg (ProofStateT ext ext err s m) a
m)
  = StateT jdg (ProofStateT ext ext err s m) a
-> TacticT jdg ext err s m a
forall jdg ext err s (m :: * -> *) a.
StateT jdg (ProofStateT ext ext err s m) a
-> TacticT jdg ext err s m a
TacticT (StateT jdg (ProofStateT ext ext err s m) a
 -> TacticT jdg ext err s m a)
-> StateT jdg (ProofStateT ext ext err s m) a
-> TacticT jdg ext err s m a
forall a b. (a -> b) -> a -> b
$ (jdg -> ProofStateT ext ext err s m (a, jdg))
-> StateT jdg (ProofStateT ext ext err s m) a
forall s (m :: * -> *) a. (s -> m (a, s)) -> StateT s m a
StateT ((jdg -> ProofStateT ext ext err s m (a, jdg))
 -> StateT jdg (ProofStateT ext ext err s m) a)
-> (jdg -> ProofStateT ext ext err s m (a, jdg))
-> StateT jdg (ProofStateT ext ext err s m) a
forall a b. (a -> b) -> a -> b
$ \jdg
jdg ->
      (ext -> ext)
-> (ext -> ext)
-> ProofStateT ext ext err s m (a, jdg)
-> ProofStateT ext ext err s m (a, jdg)
forall (m :: * -> *) a ext' ext b err s jdg.
Functor m =>
(a -> ext')
-> (ext -> b)
-> ProofStateT ext' ext err s m jdg
-> ProofStateT a b err s m jdg
mapExtract ext -> ext
forall a. a -> a
id ext -> ext
f (ProofStateT ext ext err s m (a, jdg)
 -> ProofStateT ext ext err s m (a, jdg))
-> ProofStateT ext ext err s m (a, jdg)
-> ProofStateT ext ext err s m (a, jdg)
forall a b. (a -> b) -> a -> b
$ StateT jdg (ProofStateT ext ext err s m) a
-> jdg -> ProofStateT ext ext err s m (a, jdg)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT StateT jdg (ProofStateT ext ext err s m) a
m jdg
jdg


------------------------------------------------------------------------------
-- | 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.
scoreSolution
    :: Synthesized (LHsExpr GhcPs)
    -> Judgement
    -> [Judgement]
    -> ( Penalize Int  -- number of holes
       , Reward Bool   -- all bindings used
       , Penalize Int  -- unused top-level bindings
       , Penalize Int  -- number of introduced bindings
       , Reward Int    -- number used bindings
       , Penalize Int  -- number of recursive calls
       , Penalize Int  -- size of extract
       )
scoreSolution :: Synthesized (LHsExpr GhcPs)
-> Judgement
-> [Judgement]
-> (Penalize Int, Reward Bool, Penalize Int, Penalize Int,
    Reward Int, Penalize Int, Penalize Int)
scoreSolution Synthesized (LHsExpr GhcPs)
ext Judgement
goal [Judgement]
holes
  = ( Int -> Penalize Int
forall a. a -> Penalize a
Penalize (Int -> Penalize Int) -> Int -> Penalize Int
forall a b. (a -> b) -> a -> b
$ [Judgement] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Judgement]
holes
    , Bool -> Reward Bool
forall a. a -> Reward a
Reward   (Bool -> Reward Bool) -> Bool -> Reward Bool
forall a b. (a -> b) -> a -> b
$ Set OccName -> Bool
forall a. Set a -> Bool
S.null (Set OccName -> Bool) -> Set OccName -> Bool
forall a b. (a -> b) -> a -> b
$ Set OccName
intro_vals Set OccName -> Set OccName -> Set OccName
forall a. Ord a => Set a -> Set a -> Set a
S.\\ Set OccName
used_vals
    , Int -> Penalize Int
forall a. a -> Penalize a
Penalize (Int -> Penalize Int) -> Int -> Penalize Int
forall a b. (a -> b) -> a -> b
$ Set OccName -> Int
forall a. Set a -> Int
S.size Set OccName
unused_top_vals
    , Int -> Penalize Int
forall a. a -> Penalize a
Penalize (Int -> Penalize Int) -> Int -> Penalize Int
forall a b. (a -> b) -> a -> b
$ Set OccName -> Int
forall a. Set a -> Int
S.size Set OccName
intro_vals
    , Int -> Reward Int
forall a. a -> Reward a
Reward   (Int -> Reward Int) -> Int -> Reward Int
forall a b. (a -> b) -> a -> b
$ Set OccName -> Int
forall a. Set a -> Int
S.size Set OccName
used_vals Int -> Int -> Int
forall a. Num a => a -> a -> a
+ [HyInfo CType] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [HyInfo CType]
used_user_vals
    , Int -> Penalize Int
forall a. a -> Penalize a
Penalize (Int -> Penalize Int) -> Int -> Penalize Int
forall a b. (a -> b) -> a -> b
$ Sum Int -> Int
forall a. Sum a -> a
getSum (Sum Int -> Int) -> Sum Int -> Int
forall a b. (a -> b) -> a -> b
$ Synthesized (LHsExpr GhcPs) -> Sum Int
forall a. Synthesized a -> Sum Int
syn_recursion_count Synthesized (LHsExpr GhcPs)
ext
    , Int -> Penalize Int
forall a. a -> Penalize a
Penalize (Int -> Penalize Int) -> Int -> Penalize Int
forall a b. (a -> b) -> a -> b
$ LHsExpr GhcPs -> Int
solutionSize (LHsExpr GhcPs -> Int) -> LHsExpr GhcPs -> Int
forall a b. (a -> b) -> a -> b
$ Synthesized (LHsExpr GhcPs) -> LHsExpr GhcPs
forall a. Synthesized a -> a
syn_val Synthesized (LHsExpr GhcPs)
ext
    )
  where
    initial_scope :: Map OccName (HyInfo CType)
initial_scope = Hypothesis CType -> Map OccName (HyInfo CType)
forall a. Hypothesis a -> Map OccName (HyInfo a)
hyByName (Hypothesis CType -> Map OccName (HyInfo CType))
-> Hypothesis CType -> Map OccName (HyInfo CType)
forall a b. (a -> b) -> a -> b
$ Judgement -> Hypothesis CType
forall a. Judgement' a -> Hypothesis a
jEntireHypothesis Judgement
goal
    intro_vals :: Set OccName
intro_vals = Map OccName (HyInfo CType) -> Set OccName
forall k a. Map k a -> Set k
M.keysSet (Map OccName (HyInfo CType) -> Set OccName)
-> Map OccName (HyInfo CType) -> Set OccName
forall a b. (a -> b) -> a -> b
$ Hypothesis CType -> Map OccName (HyInfo CType)
forall a. Hypothesis a -> Map OccName (HyInfo a)
hyByName (Hypothesis CType -> Map OccName (HyInfo CType))
-> Hypothesis CType -> Map OccName (HyInfo CType)
forall a b. (a -> b) -> a -> b
$ Synthesized (LHsExpr GhcPs) -> Hypothesis CType
forall a. Synthesized a -> Hypothesis CType
syn_scoped Synthesized (LHsExpr GhcPs)
ext
    used_vals :: Set OccName
used_vals = Set OccName -> Set OccName -> Set OccName
forall a. Ord a => Set a -> Set a -> Set a
S.intersection Set OccName
intro_vals (Set OccName -> Set OccName) -> Set OccName -> Set OccName
forall a b. (a -> b) -> a -> b
$ Synthesized (LHsExpr GhcPs) -> Set OccName
forall a. Synthesized a -> Set OccName
syn_used_vals Synthesized (LHsExpr GhcPs)
ext
    used_user_vals :: [HyInfo CType]
used_user_vals = (HyInfo CType -> Bool) -> [HyInfo CType] -> [HyInfo CType]
forall a. (a -> Bool) -> [a] -> [a]
filter (Provenance -> Bool
isLocalHypothesis (Provenance -> Bool)
-> (HyInfo CType -> Provenance) -> HyInfo CType -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HyInfo CType -> Provenance
forall a. HyInfo a -> Provenance
hi_provenance)
                   ([HyInfo CType] -> [HyInfo CType])
-> [HyInfo CType] -> [HyInfo CType]
forall a b. (a -> b) -> a -> b
$ (OccName -> Maybe (HyInfo CType)) -> [OccName] -> [HyInfo CType]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe ((OccName -> Map OccName (HyInfo CType) -> Maybe (HyInfo CType))
-> Map OccName (HyInfo CType) -> OccName -> Maybe (HyInfo CType)
forall a b c. (a -> b -> c) -> b -> a -> c
flip OccName -> Map OccName (HyInfo CType) -> Maybe (HyInfo CType)
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Map OccName (HyInfo CType)
initial_scope)
                   ([OccName] -> [HyInfo CType]) -> [OccName] -> [HyInfo CType]
forall a b. (a -> b) -> a -> b
$ Set OccName -> [OccName]
forall a. Set a -> [a]
S.toList
                   (Set OccName -> [OccName]) -> Set OccName -> [OccName]
forall a b. (a -> b) -> a -> b
$ Synthesized (LHsExpr GhcPs) -> Set OccName
forall a. Synthesized a -> Set OccName
syn_used_vals Synthesized (LHsExpr GhcPs)
ext
    top_vals :: Set OccName
top_vals = [OccName] -> Set OccName
forall a. Ord a => [a] -> Set a
S.fromList
             ([OccName] -> Set OccName)
-> (Hypothesis CType -> [OccName])
-> Hypothesis CType
-> Set OccName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (HyInfo CType -> OccName) -> [HyInfo CType] -> [OccName]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap HyInfo CType -> OccName
forall a. HyInfo a -> OccName
hi_name
             ([HyInfo CType] -> [OccName])
-> (Hypothesis CType -> [HyInfo CType])
-> Hypothesis CType
-> [OccName]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (HyInfo CType -> Bool) -> [HyInfo CType] -> [HyInfo CType]
forall a. (a -> Bool) -> [a] -> [a]
filter (Provenance -> Bool
isTopLevel (Provenance -> Bool)
-> (HyInfo CType -> Provenance) -> HyInfo CType -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HyInfo CType -> Provenance
forall a. HyInfo a -> Provenance
hi_provenance)
             ([HyInfo CType] -> [HyInfo CType])
-> (Hypothesis CType -> [HyInfo CType])
-> Hypothesis CType
-> [HyInfo CType]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Hypothesis CType -> [HyInfo CType]
forall a. Hypothesis a -> [HyInfo a]
unHypothesis
             (Hypothesis CType -> Set OccName)
-> Hypothesis CType -> Set OccName
forall a b. (a -> b) -> a -> b
$ Synthesized (LHsExpr GhcPs) -> Hypothesis CType
forall a. Synthesized a -> Hypothesis CType
syn_scoped Synthesized (LHsExpr GhcPs)
ext
    unused_top_vals :: Set OccName
unused_top_vals = Set OccName
top_vals Set OccName -> Set OccName -> Set OccName
forall a. Ord a => Set a -> Set a -> Set a
S.\\ Set OccName
used_vals


------------------------------------------------------------------------------
-- | Compute the number of 'LHsExpr' nodes; used as a rough metric for code
-- size.
solutionSize :: LHsExpr GhcPs -> Int
solutionSize :: LHsExpr GhcPs -> Int
solutionSize = (Int -> Int -> Int) -> GenericQ Int -> GenericQ Int
forall r. (r -> r -> r) -> GenericQ r -> GenericQ r
everything Int -> Int -> Int
forall a. Num a => a -> a -> a
(+) (GenericQ Int -> GenericQ Int) -> GenericQ Int -> GenericQ Int
forall a b. (a -> b) -> a -> b
$ GenericQ Bool -> GenericQ Int
gcount (GenericQ Bool -> GenericQ Int) -> GenericQ Bool -> GenericQ Int
forall a b. (a -> b) -> a -> b
$ Bool -> (LHsExpr GhcPs -> Bool) -> a -> Bool
forall a b r. (Typeable a, Typeable b) => r -> (b -> r) -> a -> r
mkQ Bool
False ((LHsExpr GhcPs -> Bool) -> a -> Bool)
-> (LHsExpr GhcPs -> Bool) -> a -> Bool
forall a b. (a -> b) -> a -> b
$ \case
  (LHsExpr GhcPs
_ :: LHsExpr GhcPs) -> Bool
True


newtype Penalize a = Penalize a
  deriving (Penalize a -> Penalize a -> Bool
(Penalize a -> Penalize a -> Bool)
-> (Penalize a -> Penalize a -> Bool) -> Eq (Penalize a)
forall a. Eq a => Penalize a -> Penalize a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Penalize a -> Penalize a -> Bool
$c/= :: forall a. Eq a => Penalize a -> Penalize a -> Bool
== :: Penalize a -> Penalize a -> Bool
$c== :: forall a. Eq a => Penalize a -> Penalize a -> Bool
Eq, Eq (Penalize a)
Eq (Penalize a)
-> (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)
-> (Penalize a -> Penalize a -> Penalize a)
-> (Penalize a -> Penalize a -> Penalize a)
-> Ord (Penalize a)
Penalize a -> Penalize a -> Bool
Penalize a -> Penalize a -> Ordering
Penalize a -> Penalize a -> Penalize a
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall a. Ord a => Eq (Penalize a)
forall a. Ord a => Penalize a -> Penalize a -> Bool
forall a. Ord a => Penalize a -> Penalize a -> Ordering
forall a. Ord a => Penalize a -> Penalize a -> Penalize a
min :: Penalize a -> Penalize a -> Penalize a
$cmin :: forall a. Ord a => Penalize a -> Penalize a -> Penalize a
max :: Penalize a -> Penalize a -> Penalize a
$cmax :: forall a. Ord a => Penalize a -> Penalize a -> Penalize a
>= :: Penalize a -> Penalize a -> Bool
$c>= :: forall a. Ord a => Penalize a -> Penalize a -> Bool
> :: Penalize a -> Penalize a -> Bool
$c> :: forall a. Ord a => Penalize a -> Penalize a -> Bool
<= :: Penalize a -> Penalize a -> Bool
$c<= :: forall a. Ord a => Penalize a -> Penalize a -> Bool
< :: Penalize a -> Penalize a -> Bool
$c< :: forall a. Ord a => Penalize a -> Penalize a -> Bool
compare :: Penalize a -> Penalize a -> Ordering
$ccompare :: forall a. Ord a => Penalize a -> Penalize a -> Ordering
$cp1Ord :: forall a. Ord a => Eq (Penalize a)
Ord, Int -> Penalize a -> ShowS
[Penalize a] -> ShowS
Penalize a -> String
(Int -> Penalize a -> ShowS)
-> (Penalize a -> String)
-> ([Penalize a] -> ShowS)
-> Show (Penalize a)
forall a. Show a => Int -> Penalize a -> ShowS
forall a. Show a => [Penalize a] -> ShowS
forall a. Show a => Penalize a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Penalize a] -> ShowS
$cshowList :: forall a. Show a => [Penalize a] -> ShowS
show :: Penalize a -> String
$cshow :: forall a. Show a => Penalize a -> String
showsPrec :: Int -> Penalize a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> Penalize a -> ShowS
Show) via (Down a)

newtype Reward a = Reward a
  deriving (Reward a -> Reward a -> Bool
(Reward a -> Reward a -> Bool)
-> (Reward a -> Reward a -> Bool) -> Eq (Reward a)
forall a. Eq a => Reward a -> Reward a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Reward a -> Reward a -> Bool
$c/= :: forall a. Eq a => Reward a -> Reward a -> Bool
== :: Reward a -> Reward a -> Bool
$c== :: forall a. Eq a => Reward a -> Reward a -> Bool
Eq, Eq (Reward a)
Eq (Reward a)
-> (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)
-> (Reward a -> Reward a -> Reward a)
-> (Reward a -> Reward a -> Reward a)
-> Ord (Reward a)
Reward a -> Reward a -> Bool
Reward a -> Reward a -> Ordering
Reward a -> Reward a -> Reward a
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall a. Ord a => Eq (Reward a)
forall a. Ord a => Reward a -> Reward a -> Bool
forall a. Ord a => Reward a -> Reward a -> Ordering
forall a. Ord a => Reward a -> Reward a -> Reward a
min :: Reward a -> Reward a -> Reward a
$cmin :: forall a. Ord a => Reward a -> Reward a -> Reward a
max :: Reward a -> Reward a -> Reward a
$cmax :: forall a. Ord a => Reward a -> Reward a -> Reward a
>= :: Reward a -> Reward a -> Bool
$c>= :: forall a. Ord a => Reward a -> Reward a -> Bool
> :: Reward a -> Reward a -> Bool
$c> :: forall a. Ord a => Reward a -> Reward a -> Bool
<= :: Reward a -> Reward a -> Bool
$c<= :: forall a. Ord a => Reward a -> Reward a -> Bool
< :: Reward a -> Reward a -> Bool
$c< :: forall a. Ord a => Reward a -> Reward a -> Bool
compare :: Reward a -> Reward a -> Ordering
$ccompare :: forall a. Ord a => Reward a -> Reward a -> Ordering
$cp1Ord :: forall a. Ord a => Eq (Reward a)
Ord, Int -> Reward a -> ShowS
[Reward a] -> ShowS
Reward a -> String
(Int -> Reward a -> ShowS)
-> (Reward a -> String) -> ([Reward a] -> ShowS) -> Show (Reward a)
forall a. Show a => Int -> Reward a -> ShowS
forall a. Show a => [Reward a] -> ShowS
forall a. Show a => Reward a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Reward a] -> ShowS
$cshowList :: forall a. Show a => [Reward a] -> ShowS
show :: Reward a -> String
$cshow :: forall a. Show a => Reward a -> String
showsPrec :: Int -> Reward a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> Reward a -> ShowS
Show) via a




------------------------------------------------------------------------------
-- | Attempt to unify two types.
unify :: CType -- ^ The goal type
      -> CType -- ^ The type we are trying unify the goal type with
      -> RuleM ()
unify :: CType -> CType -> RuleM ()
unify CType
goal CType
inst = do
  Set TyVar
skolems <- (TacticState -> Set TyVar)
-> RuleT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     (Set TyVar)
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets TacticState -> Set TyVar
ts_skolems
  case Set TyVar -> CType -> CType -> Maybe TCvSubst
tryUnifyUnivarsButNotSkolems Set TyVar
skolems CType
goal CType
inst of
    Just TCvSubst
subst ->
      (TacticState -> TacticState) -> RuleM ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((TacticState -> TacticState) -> RuleM ())
-> (TacticState -> TacticState) -> RuleM ()
forall a b. (a -> b) -> a -> b
$ TCvSubst -> TacticState -> TacticState
updateSubst TCvSubst
subst
    Maybe TCvSubst
Nothing -> RuleM ()
forall jdg ext err s (m :: * -> *) a. RuleT jdg ext err s m a
cut

cut :: RuleT jdg ext err s m a
cut :: RuleT jdg ext err s m a
cut = ProofStateT ext a err s m jdg -> RuleT jdg ext err s m a
forall jdg ext err s (m :: * -> *) a.
ProofStateT ext a err s m jdg -> RuleT jdg ext err s m a
RuleT ProofStateT ext a err s m jdg
forall ext' ext err s (m :: * -> *) goal.
ProofStateT ext' ext err s m goal
Empty


------------------------------------------------------------------------------
-- | Attempt to unify two types.
canUnify
    :: MonadState TacticState m
    => CType -- ^ The goal type
    -> CType -- ^ The type we are trying unify the goal type with
    -> m Bool
canUnify :: CType -> CType -> m Bool
canUnify CType
goal CType
inst = do
  Set TyVar
skolems <- (TacticState -> Set TyVar) -> m (Set TyVar)
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets TacticState -> Set TyVar
ts_skolems
  case Set TyVar -> CType -> CType -> Maybe TCvSubst
tryUnifyUnivarsButNotSkolems Set TyVar
skolems CType
goal CType
inst of
    Just TCvSubst
_ -> Bool -> m Bool
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True
    Maybe TCvSubst
Nothing -> Bool -> m Bool
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
False


------------------------------------------------------------------------------
-- | 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.
attemptWhen :: TacticsM a -> TacticsM a -> Bool -> TacticsM a
attemptWhen :: TacticsM a -> TacticsM a -> Bool -> TacticsM a
attemptWhen TacticsM a
_  TacticsM a
t2 Bool
False = TacticsM a
t2
attemptWhen TacticsM a
t1 TacticsM a
t2 Bool
True  = TacticsM a -> TacticsM a -> TacticsM a
forall jdg ext err s (m :: * -> *) a.
TacticT jdg ext err s m a
-> TacticT jdg ext err s m a -> TacticT jdg ext err s m a
commit TacticsM a
t1 TacticsM a
t2


------------------------------------------------------------------------------
-- | Run the given tactic iff the current hole contains no univars. Skolems and
-- already decided univars are OK though.
requireConcreteHole :: TacticsM a -> TacticsM a
requireConcreteHole :: TacticsM a -> TacticsM a
requireConcreteHole TacticsM a
m = do
  Judgement
jdg     <- TacticT
  Judgement
  (Synthesized (LHsExpr GhcPs))
  TacticError
  TacticState
  ExtractM
  Judgement
forall (m :: * -> *) jdg ext err s.
Functor m =>
TacticT jdg ext err s m jdg
goal
  Set TyVar
skolems <- (TacticState -> Set TyVar)
-> TacticT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     (Set TyVar)
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets TacticState -> Set TyVar
ts_skolems
  let vars :: Set TyVar
vars = [TyVar] -> Set TyVar
forall a. Ord a => [a] -> Set a
S.fromList ([TyVar] -> Set TyVar) -> [TyVar] -> Set TyVar
forall a b. (a -> b) -> a -> b
$ Type -> [TyVar]
tyCoVarsOfTypeWellScoped (Type -> [TyVar]) -> Type -> [TyVar]
forall a b. (a -> b) -> a -> b
$ CType -> Type
unCType (CType -> Type) -> CType -> Type
forall a b. (a -> b) -> a -> b
$ Judgement -> CType
forall a. Judgement' a -> a
jGoal Judgement
jdg
  case Set TyVar -> Int
forall a. Set a -> Int
S.size (Set TyVar -> Int) -> Set TyVar -> Int
forall a b. (a -> b) -> a -> b
$ Set TyVar
vars Set TyVar -> Set TyVar -> Set TyVar
forall a. Ord a => Set a -> Set a -> Set a
S.\\ Set TyVar
skolems of
    Int
0 -> TacticsM a
m
    Int
_ -> TacticError -> TacticsM a
forall err jdg ext s (m :: * -> *) a.
err -> TacticT jdg ext err s m a
failure TacticError
TooPolymorphic


------------------------------------------------------------------------------
-- | 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
try'
    :: Functor m
    => TacticT jdg ext err s m ()
    -> TacticT jdg ext err s m ()
try' :: TacticT jdg ext err s m () -> TacticT jdg ext err s m ()
try' TacticT jdg ext err s m ()
t = TacticT jdg ext err s m ()
-> TacticT jdg ext err s m () -> TacticT jdg ext err s m ()
forall jdg ext err s (m :: * -> *) a.
TacticT jdg ext err s m a
-> TacticT jdg ext err s m a -> TacticT jdg ext err s m a
commit TacticT jdg ext err s m ()
t (TacticT jdg ext err s m () -> TacticT jdg ext err s m ())
-> TacticT jdg ext err s m () -> TacticT jdg ext err s m ()
forall a b. (a -> b) -> a -> b
$ () -> TacticT jdg ext err s m ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()


------------------------------------------------------------------------------
-- | Sorry leaves a hole in its extract
exact :: HsExpr GhcPs -> TacticsM ()
exact :: HsExpr GhcPs -> TacticsM ()
exact = (Judgement -> Rule) -> TacticsM ()
forall (m :: * -> *) jdg ext err s.
Monad m =>
(jdg -> RuleT jdg ext err s m ext) -> TacticT jdg ext err s m ()
rule ((Judgement -> Rule) -> TacticsM ())
-> (HsExpr GhcPs -> Judgement -> Rule)
-> HsExpr GhcPs
-> TacticsM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rule -> Judgement -> Rule
forall a b. a -> b -> a
const (Rule -> Judgement -> Rule)
-> (HsExpr GhcPs -> Rule) -> HsExpr GhcPs -> Judgement -> Rule
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Synthesized (LHsExpr GhcPs) -> Rule
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Synthesized (LHsExpr GhcPs) -> Rule)
-> (HsExpr GhcPs -> Synthesized (LHsExpr GhcPs))
-> HsExpr GhcPs
-> Rule
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LHsExpr GhcPs -> Synthesized (LHsExpr GhcPs)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (LHsExpr GhcPs -> Synthesized (LHsExpr GhcPs))
-> (HsExpr GhcPs -> LHsExpr GhcPs)
-> HsExpr GhcPs
-> Synthesized (LHsExpr GhcPs)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HsExpr GhcPs -> LHsExpr GhcPs
forall a. HasSrcSpan a => SrcSpanLess a -> a
noLoc

------------------------------------------------------------------------------
-- | Lift a function over 'HyInfo's to one that takes an 'OccName' and tries to
-- look it up in the hypothesis.
useNameFromHypothesis :: (HyInfo CType -> TacticsM a) -> OccName -> TacticsM a
useNameFromHypothesis :: (HyInfo CType -> TacticsM a) -> OccName -> TacticsM a
useNameFromHypothesis HyInfo CType -> TacticsM a
f OccName
name = do
  Hypothesis CType
hy <- Judgement -> Hypothesis CType
forall a. Judgement' a -> Hypothesis a
jHypothesis (Judgement -> Hypothesis CType)
-> TacticT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     Judgement
-> TacticT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     (Hypothesis CType)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TacticT
  Judgement
  (Synthesized (LHsExpr GhcPs))
  TacticError
  TacticState
  ExtractM
  Judgement
forall (m :: * -> *) jdg ext err s.
Functor m =>
TacticT jdg ext err s m jdg
goal
  case OccName -> Map OccName (HyInfo CType) -> Maybe (HyInfo CType)
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup OccName
name (Map OccName (HyInfo CType) -> Maybe (HyInfo CType))
-> Map OccName (HyInfo CType) -> Maybe (HyInfo CType)
forall a b. (a -> b) -> a -> b
$ Hypothesis CType -> Map OccName (HyInfo CType)
forall a. Hypothesis a -> Map OccName (HyInfo a)
hyByName Hypothesis CType
hy of
    Just HyInfo CType
hi -> HyInfo CType -> TacticsM a
f HyInfo CType
hi
    Maybe (HyInfo CType)
Nothing -> TacticError -> TacticsM a
forall err jdg ext s (m :: * -> *) a.
err -> TacticT jdg ext err s m a
failure (TacticError -> TacticsM a) -> TacticError -> TacticsM a
forall a b. (a -> b) -> a -> b
$ OccName -> TacticError
NotInScope OccName
name

------------------------------------------------------------------------------
-- | Lift a function over 'HyInfo's to one that takes an 'OccName' and tries to
-- look it up in the hypothesis.
useNameFromContext :: (HyInfo CType -> TacticsM a) -> OccName -> TacticsM a
useNameFromContext :: (HyInfo CType -> TacticsM a) -> OccName -> TacticsM a
useNameFromContext HyInfo CType -> TacticsM a
f OccName
name = do
  OccName
-> TacticT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     (Maybe CType)
forall (m :: * -> *).
MonadReader Context m =>
OccName -> m (Maybe CType)
lookupNameInContext OccName
name TacticT
  Judgement
  (Synthesized (LHsExpr GhcPs))
  TacticError
  TacticState
  ExtractM
  (Maybe CType)
-> (Maybe CType -> TacticsM a) -> TacticsM a
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Just CType
ty -> HyInfo CType -> TacticsM a
f (HyInfo CType -> TacticsM a) -> HyInfo CType -> TacticsM a
forall a b. (a -> b) -> a -> b
$ OccName -> CType -> HyInfo CType
createImportedHyInfo OccName
name CType
ty
    Maybe CType
Nothing -> TacticError -> TacticsM a
forall err jdg ext s (m :: * -> *) a.
err -> TacticT jdg ext err s m a
failure (TacticError -> TacticsM a) -> TacticError -> TacticsM a
forall a b. (a -> b) -> a -> b
$ OccName -> TacticError
NotInScope OccName
name


------------------------------------------------------------------------------
-- | Find the type of an 'OccName' that is defined in the current module.
lookupNameInContext :: MonadReader Context m => OccName -> m (Maybe CType)
lookupNameInContext :: OccName -> m (Maybe CType)
lookupNameInContext OccName
name = do
  [(OccName, CType)]
ctx <- (Context -> [(OccName, CType)]) -> m [(OccName, CType)]
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks Context -> [(OccName, CType)]
ctxModuleFuncs
  Maybe CType -> m (Maybe CType)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe CType -> m (Maybe CType)) -> Maybe CType -> m (Maybe CType)
forall a b. (a -> b) -> a -> b
$ case ((OccName, CType) -> Bool)
-> [(OccName, CType)] -> Maybe (OccName, CType)
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find ((OccName -> OccName -> Bool
forall a. Eq a => a -> a -> Bool
== OccName
name) (OccName -> Bool)
-> ((OccName, CType) -> OccName) -> (OccName, CType) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (OccName, CType) -> OccName
forall a b. (a, b) -> a
fst) [(OccName, CType)]
ctx of
    Just (OccName
_, CType
ty) -> CType -> Maybe CType
forall (f :: * -> *) a. Applicative f => a -> f a
pure CType
ty
    Maybe (OccName, CType)
Nothing      -> Maybe CType
forall (f :: * -> *) a. Alternative f => f a
empty


getDefiningType
    :: TacticsM CType
getDefiningType :: TacticsM CType
getDefiningType = do
  OccName
calling_fun_name <- (OccName, CType) -> OccName
forall a b. (a, b) -> a
fst ((OccName, CType) -> OccName)
-> ([(OccName, CType)] -> (OccName, CType))
-> [(OccName, CType)]
-> OccName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(OccName, CType)] -> (OccName, CType)
forall a. [a] -> a
head ([(OccName, CType)] -> OccName)
-> TacticT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     [(OccName, CType)]
-> TacticT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     OccName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Context -> [(OccName, CType)])
-> TacticT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     [(OccName, CType)]
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks Context -> [(OccName, CType)]
ctxDefiningFuncs
  TacticsM CType
-> (CType -> TacticsM CType) -> Maybe CType -> TacticsM CType
forall b a. b -> (a -> b) -> Maybe a -> b
maybe
    (TacticError -> TacticsM CType
forall err jdg ext s (m :: * -> *) a.
err -> TacticT jdg ext err s m a
failure (TacticError -> TacticsM CType) -> TacticError -> TacticsM CType
forall a b. (a -> b) -> a -> b
$ OccName -> TacticError
NotInScope OccName
calling_fun_name)
    CType -> TacticsM CType
forall (f :: * -> *) a. Applicative f => a -> f a
pure
      (Maybe CType -> TacticsM CType)
-> TacticT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     (Maybe CType)
-> TacticsM CType
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< OccName
-> TacticT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     (Maybe CType)
forall (m :: * -> *).
MonadReader Context m =>
OccName -> m (Maybe CType)
lookupNameInContext OccName
calling_fun_name


------------------------------------------------------------------------------
-- | Build a 'HyInfo' for an imported term.
createImportedHyInfo :: OccName -> CType -> HyInfo CType
createImportedHyInfo :: OccName -> CType -> HyInfo CType
createImportedHyInfo OccName
on CType
ty = HyInfo :: forall a. OccName -> Provenance -> a -> HyInfo a
HyInfo
  { hi_name :: OccName
hi_name = OccName
on
  , hi_provenance :: Provenance
hi_provenance = Provenance
ImportPrv
  , hi_type :: CType
hi_type = CType
ty
  }


getTyThing
    :: OccName
    -> TacticsM (Maybe TyThing)
getTyThing :: OccName -> TacticsM (Maybe TyThing)
getTyThing OccName
occ = do
  Context
ctx <- TacticT
  Judgement
  (Synthesized (LHsExpr GhcPs))
  TacticError
  TacticState
  ExtractM
  Context
forall r (m :: * -> *). MonadReader r m => m r
ask
  case OccEnv [GlobalRdrElt] -> OccName -> Maybe [GlobalRdrElt]
forall a. OccEnv a -> OccName -> Maybe a
lookupOccEnv (Context -> OccEnv [GlobalRdrElt]
ctx_occEnv Context
ctx) OccName
occ of
    Just (GlobalRdrElt
elt : [GlobalRdrElt]
_) -> do
      Maybe TyThing
mvar <- ExtractM (Maybe TyThing) -> TacticsM (Maybe TyThing)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift
            (ExtractM (Maybe TyThing) -> TacticsM (Maybe TyThing))
-> ExtractM (Maybe TyThing) -> TacticsM (Maybe TyThing)
forall a b. (a -> b) -> a -> b
$ ReaderT Context IO (Maybe TyThing) -> ExtractM (Maybe TyThing)
forall a. ReaderT Context IO a -> ExtractM a
ExtractM
            (ReaderT Context IO (Maybe TyThing) -> ExtractM (Maybe TyThing))
-> ReaderT Context IO (Maybe TyThing) -> ExtractM (Maybe TyThing)
forall a b. (a -> b) -> a -> b
$ IO (Maybe TyThing) -> ReaderT Context IO (Maybe TyThing)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift
            (IO (Maybe TyThing) -> ReaderT Context IO (Maybe TyThing))
-> IO (Maybe TyThing) -> ReaderT Context IO (Maybe TyThing)
forall a b. (a -> b) -> a -> b
$ HscEnv -> Module -> Name -> IO (Maybe TyThing)
lookupName (Context -> HscEnv
ctx_hscEnv Context
ctx) (Context -> Module
ctx_module Context
ctx)
            (Name -> IO (Maybe TyThing)) -> Name -> IO (Maybe TyThing)
forall a b. (a -> b) -> a -> b
$ GlobalRdrElt -> Name
gre_name GlobalRdrElt
elt
      Maybe TyThing -> TacticsM (Maybe TyThing)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe TyThing
mvar
    Maybe [GlobalRdrElt]
_ -> Maybe TyThing -> TacticsM (Maybe TyThing)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe TyThing
forall a. Maybe a
Nothing


------------------------------------------------------------------------------
-- | Like 'getTyThing' but specialized to classes.
knownClass :: OccName -> TacticsM (Maybe Class)
knownClass :: OccName -> TacticsM (Maybe Class)
knownClass OccName
occ =
  OccName -> TacticsM (Maybe TyThing)
getTyThing OccName
occ TacticsM (Maybe TyThing)
-> (Maybe TyThing -> Maybe Class) -> TacticsM (Maybe Class)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \case
    Just (ATyCon TyCon
tc) -> TyCon -> Maybe Class
tyConClass_maybe TyCon
tc
    Maybe TyThing
_                -> Maybe Class
forall a. Maybe a
Nothing


------------------------------------------------------------------------------
-- | Like 'getInstance', but uses a class that it just looked up.
getKnownInstance :: OccName -> [Type] -> TacticsM (Maybe (Class, PredType))
getKnownInstance :: OccName -> [Type] -> TacticsM (Maybe (Class, Type))
getKnownInstance OccName
f [Type]
tys = MaybeT
  (TacticT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM)
  (Class, Type)
-> TacticsM (Maybe (Class, Type))
forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT (MaybeT
   (TacticT
      Judgement
      (Synthesized (LHsExpr GhcPs))
      TacticError
      TacticState
      ExtractM)
   (Class, Type)
 -> TacticsM (Maybe (Class, Type)))
-> MaybeT
     (TacticT
        Judgement
        (Synthesized (LHsExpr GhcPs))
        TacticError
        TacticState
        ExtractM)
     (Class, Type)
-> TacticsM (Maybe (Class, Type))
forall a b. (a -> b) -> a -> b
$ do
  Class
cls <- TacticsM (Maybe Class)
-> MaybeT
     (TacticT
        Judgement
        (Synthesized (LHsExpr GhcPs))
        TacticError
        TacticState
        ExtractM)
     Class
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (TacticsM (Maybe Class)
 -> MaybeT
      (TacticT
         Judgement
         (Synthesized (LHsExpr GhcPs))
         TacticError
         TacticState
         ExtractM)
      Class)
-> TacticsM (Maybe Class)
-> MaybeT
     (TacticT
        Judgement
        (Synthesized (LHsExpr GhcPs))
        TacticError
        TacticState
        ExtractM)
     Class
forall a b. (a -> b) -> a -> b
$ OccName -> TacticsM (Maybe Class)
knownClass OccName
f
  TacticsM (Maybe (Class, Type))
-> MaybeT
     (TacticT
        Judgement
        (Synthesized (LHsExpr GhcPs))
        TacticError
        TacticState
        ExtractM)
     (Class, Type)
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (TacticsM (Maybe (Class, Type))
 -> MaybeT
      (TacticT
         Judgement
         (Synthesized (LHsExpr GhcPs))
         TacticError
         TacticState
         ExtractM)
      (Class, Type))
-> TacticsM (Maybe (Class, Type))
-> MaybeT
     (TacticT
        Judgement
        (Synthesized (LHsExpr GhcPs))
        TacticError
        TacticState
        ExtractM)
     (Class, Type)
forall a b. (a -> b) -> a -> b
$ Class -> [Type] -> TacticsM (Maybe (Class, Type))
forall (m :: * -> *).
MonadReader Context m =>
Class -> [Type] -> m (Maybe (Class, Type))
getInstance Class
cls [Type]
tys


------------------------------------------------------------------------------
-- | 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'.
getOccNameType
    :: OccName
    -> TacticsM Type
getOccNameType :: OccName -> TacticsM Type
getOccNameType OccName
occ = do
  OccName -> TacticsM (Maybe TyThing)
getTyThing OccName
occ TacticsM (Maybe TyThing)
-> (Maybe TyThing -> TacticsM Type) -> TacticsM Type
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Just (AnId TyVar
v) -> Type -> TacticsM Type
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Type -> TacticsM Type) -> Type -> TacticsM Type
forall a b. (a -> b) -> a -> b
$ TyVar -> Type
varType TyVar
v
    Maybe TyThing
_ -> TacticError -> TacticsM Type
forall err jdg ext s (m :: * -> *) a.
err -> TacticT jdg ext err s m a
failure (TacticError -> TacticsM Type) -> TacticError -> TacticsM Type
forall a b. (a -> b) -> a -> b
$ OccName -> TacticError
NotInScope OccName
occ


getCurrentDefinitions :: TacticsM [(OccName, CType)]
getCurrentDefinitions :: TacticT
  Judgement
  (Synthesized (LHsExpr GhcPs))
  TacticError
  TacticState
  ExtractM
  [(OccName, CType)]
getCurrentDefinitions = do
  [(OccName, CType)]
ctx_funcs <- (Context -> [(OccName, CType)])
-> TacticT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     [(OccName, CType)]
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks Context -> [(OccName, CType)]
ctxDefiningFuncs
  [(OccName, CType)]
-> ((OccName, CType)
    -> TacticT
         Judgement
         (Synthesized (LHsExpr GhcPs))
         TacticError
         TacticState
         ExtractM
         (OccName, CType))
-> TacticT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     [(OccName, CType)]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for [(OccName, CType)]
ctx_funcs (((OccName, CType)
  -> TacticT
       Judgement
       (Synthesized (LHsExpr GhcPs))
       TacticError
       TacticState
       ExtractM
       (OccName, CType))
 -> TacticT
      Judgement
      (Synthesized (LHsExpr GhcPs))
      TacticError
      TacticState
      ExtractM
      [(OccName, CType)])
-> ((OccName, CType)
    -> TacticT
         Judgement
         (Synthesized (LHsExpr GhcPs))
         TacticError
         TacticState
         ExtractM
         (OccName, CType))
-> TacticT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     [(OccName, CType)]
forall a b. (a -> b) -> a -> b
$ \res :: (OccName, CType)
res@(OccName
occ, CType
_) ->
    (OccName, CType)
-> TacticT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     (OccName, CType)
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((OccName, CType)
 -> TacticT
      Judgement
      (Synthesized (LHsExpr GhcPs))
      TacticError
      TacticState
      ExtractM
      (OccName, CType))
-> (Maybe CType -> (OccName, CType))
-> Maybe CType
-> TacticT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     (OccName, CType)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (OccName, CType)
-> (CType -> (OccName, CType)) -> Maybe CType -> (OccName, CType)
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (OccName, CType)
res (OccName
occ,) (Maybe CType
 -> TacticT
      Judgement
      (Synthesized (LHsExpr GhcPs))
      TacticError
      TacticState
      ExtractM
      (OccName, CType))
-> TacticT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     (Maybe CType)
-> TacticT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     (OccName, CType)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< OccName
-> TacticT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     (Maybe CType)
forall (m :: * -> *).
MonadReader Context m =>
OccName -> m (Maybe CType)
lookupNameInContext OccName
occ


------------------------------------------------------------------------------
-- | 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.
uncoveredDataCons :: Type -> Type -> Maybe (S.Set (Uniquely DataCon))
uncoveredDataCons :: Type -> Type -> Maybe (Set (Uniquely DataCon))
uncoveredDataCons Type
domain Type
codomain = do
  ([DataCon]
g_dcs, [Type]
_) <- Type -> Maybe ([DataCon], [Type])
tacticsGetDataCons Type
codomain
  ([DataCon]
hi_dcs, [Type]
_) <- Type -> Maybe ([DataCon], [Type])
tacticsGetDataCons Type
domain
  Set (Uniquely DataCon) -> Maybe (Set (Uniquely DataCon))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Set (Uniquely DataCon) -> Maybe (Set (Uniquely DataCon)))
-> Set (Uniquely DataCon) -> Maybe (Set (Uniquely DataCon))
forall a b. (a -> b) -> a -> b
$ [Uniquely DataCon] -> Set (Uniquely DataCon)
forall a. Ord a => [a] -> Set a
S.fromList ([DataCon] -> [Uniquely DataCon]
coerce [DataCon]
hi_dcs) Set (Uniquely DataCon)
-> Set (Uniquely DataCon) -> Set (Uniquely DataCon)
forall a. Ord a => Set a -> Set a -> Set a
S.\\ [Uniquely DataCon] -> Set (Uniquely DataCon)
forall a. Ord a => [a] -> Set a
S.fromList ([DataCon] -> [Uniquely DataCon]
coerce [DataCon]
g_dcs)