{-# LANGUAGE CPP           #-}
{-# LANGUAGE RankNTypes    #-}
{-# LANGUAGE TupleSections #-}

module Wingman.Machinery where

import           Control.Applicative (empty)
import           Control.Concurrent.Chan.Unagi.NoBlocking (newChan, writeChan, OutChan, tryRead, tryReadChan)
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, isNothing)
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 hiding (isTopLevel, empty)
import           Refinery.Future
import           Refinery.ProofState
import           Refinery.Tactic
import           Refinery.Tactic.Internal
import           System.Timeout (timeout)
import           Wingman.Context (getInstance)
import           Wingman.GHC (tryUnifyUnivarsButNotSkolems, updateSubst, tacticsGetDataCons, freshTyvars, tryUnifyUnivarsButNotSkolemsMany)
import           Wingman.Judgements
import           Wingman.Simplify (simplify)
import           Wingman.Types

#if __GLASGOW_HASKELL__ < 900
import FunDeps (fd_eqs, improveFromInstEnv)
import Pair (unPair)
#else
import GHC.Tc.Instance.FunDeps (fd_eqs, improveFromInstEnv)
import GHC.Data.Pair (unPair)
#endif


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
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m s
execStateT StateT
  Judgement
  (ProofStateT
     (Synthesized (LHsExpr GhcPs))
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM)
  ()
tt Judgement
jdg 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


consumeChan :: OutChan (Maybe a) -> IO [a]
consumeChan :: OutChan (Maybe a) -> IO [a]
consumeChan OutChan (Maybe a)
chan = do
  OutChan (Maybe a) -> IO (Element (Maybe a))
forall a. OutChan a -> IO (Element a)
tryReadChan OutChan (Maybe a)
chan IO (Element (Maybe a))
-> (Element (Maybe a) -> IO (Maybe (Maybe a)))
-> IO (Maybe (Maybe a))
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Element (Maybe a) -> IO (Maybe (Maybe a))
forall a. Element a -> IO (Maybe a)
tryRead IO (Maybe (Maybe a)) -> (Maybe (Maybe a) -> IO [a]) -> IO [a]
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Maybe (Maybe a)
Nothing -> [a] -> IO [a]
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
    Just (Just a
a) -> (a
aa -> [a] -> [a]
forall a. a -> [a] -> [a]
:) ([a] -> [a]) -> IO [a] -> IO [a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> OutChan (Maybe a) -> IO [a]
forall a. OutChan (Maybe a) -> IO [a]
consumeChan OutChan (Maybe a)
chan
    Just Maybe a
Nothing -> [a] -> IO [a]
forall (f :: * -> *) a. Applicative f => a -> f a
pure []


------------------------------------------------------------------------------
-- | Attempt to generate a term of the right type using in-scope bindings, and
-- a given tactic.
runTactic
    :: Int          -- ^ Timeout
    -> Context
    -> Judgement
    -> TacticsM ()  -- ^ Tactic to use
    -> IO (Either [TacticError] RunTacticResults)
runTactic :: Int
-> Context
-> Judgement
-> TacticsM ()
-> IO (Either [TacticError] RunTacticResults)
runTactic Int
duration 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
            }

    let stream :: ListT
  IO
  (Either
     TacticError
     (Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))))
stream = (forall x. ExtractM x -> IO x)
-> ListT
     ExtractM
     (Either
        TacticError
        (Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))))
-> ListT
     IO
     (Either
        TacticError
        (Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))))
forall (m :: * -> *) (n :: * -> *) a.
Functor m =>
(forall x. m x -> n x) -> ListT m a -> ListT n a
hoistListT ((ReaderT Context IO x -> Context -> IO x)
-> Context -> ReaderT Context IO x -> IO x
forall a b c. (a -> b -> c) -> b -> a -> c
flip ReaderT Context IO x -> Context -> IO x
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT Context
ctx (ReaderT Context IO x -> IO x)
-> (ExtractM x -> ReaderT Context IO x) -> ExtractM x -> IO x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ExtractM x -> ReaderT Context IO x
forall a. ExtractM a -> ReaderT Context IO a
unExtractM)
               (ListT
   ExtractM
   (Either
      TacticError
      (Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))))
 -> ListT
      IO
      (Either
         TacticError
         (Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs)))))
-> ListT
     ExtractM
     (Either
        TacticError
        (Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))))
-> ListT
     IO
     (Either
        TacticError
        (Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))))
forall a b. (a -> b) -> a -> b
$ TacticsM ()
-> Judgement
-> TacticState
-> ListT
     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 -> ListT m (Either err (Proof s meta jdg ext))
runStreamingTacticT TacticsM ()
t Judgement
jdg TacticState
tacticState
    (InChan
  (Maybe
     (Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))))
in_proofs, OutChan
  (Maybe
     (Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))))
out_proofs) <- IO
  (InChan
     (Maybe
        (Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs)))),
   OutChan
     (Maybe
        (Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs)))))
forall a. IO (InChan a, OutChan a)
newChan
    (InChan (Maybe TacticError)
in_errs, OutChan (Maybe TacticError)
out_errs) <- IO (InChan (Maybe TacticError), OutChan (Maybe TacticError))
forall a. IO (InChan a, OutChan a)
newChan
    Bool
timed_out <-
      (Maybe () -> Bool) -> IO (Maybe ()) -> IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Maybe () -> Bool
forall a. Maybe a -> Bool
isNothing (IO (Maybe ()) -> IO Bool) -> IO (Maybe ()) -> IO Bool
forall a b. (a -> b) -> a -> b
$ Int -> IO () -> IO (Maybe ())
forall a. Int -> IO a -> IO (Maybe a)
timeout Int
duration (IO () -> IO (Maybe ())) -> IO () -> IO (Maybe ())
forall a b. (a -> b) -> a -> b
$ ListT
  IO
  (Either
     TacticError
     (Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))))
-> (Either
      TacticError
      (Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs)))
    -> IO ())
-> IO ()
forall (m :: * -> *) a. Monad m => ListT m a -> (a -> m ()) -> m ()
consume ListT
  IO
  (Either
     TacticError
     (Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))))
stream ((Either
    TacticError
    (Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs)))
  -> IO ())
 -> IO ())
-> (Either
      TacticError
      (Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs)))
    -> IO ())
-> IO ()
forall a b. (a -> b) -> a -> b
$ \case
        Left TacticError
err -> InChan (Maybe TacticError) -> Maybe TacticError -> IO ()
forall a. InChan a -> a -> IO ()
writeChan InChan (Maybe TacticError)
in_errs (Maybe TacticError -> IO ()) -> Maybe TacticError -> IO ()
forall a b. (a -> b) -> a -> b
$ TacticError -> Maybe TacticError
forall a. a -> Maybe a
Just TacticError
err
        Right Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))
proof -> InChan
  (Maybe
     (Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))))
-> Maybe
     (Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs)))
-> IO ()
forall a. InChan a -> a -> IO ()
writeChan InChan
  (Maybe
     (Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))))
in_proofs (Maybe
   (Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs)))
 -> IO ())
-> Maybe
     (Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs)))
-> IO ()
forall a b. (a -> b) -> a -> b
$ Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))
-> Maybe
     (Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs)))
forall a. a -> Maybe a
Just Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))
proof
    InChan
  (Maybe
     (Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))))
-> Maybe
     (Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs)))
-> IO ()
forall a. InChan a -> a -> IO ()
writeChan InChan
  (Maybe
     (Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))))
in_proofs Maybe
  (Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs)))
forall a. Maybe a
Nothing

    [Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))]
solns <- OutChan
  (Maybe
     (Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))))
-> IO
     [Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))]
forall a. OutChan (Maybe a) -> IO [a]
consumeChan OutChan
  (Maybe
     (Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))))
out_proofs
    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))]
_) ->
        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
$ 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
-> Bool
-> 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
            , rtr_timed_out :: Bool
rtr_timed_out = Bool
timed_out
            }
      [Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))]
_ -> ([TacticError] -> Either [TacticError] RunTacticResults)
-> IO [TacticError] -> IO (Either [TacticError] RunTacticResults)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [TacticError] -> Either [TacticError] RunTacticResults
forall a b. a -> Either a b
Left (IO [TacticError] -> IO (Either [TacticError] RunTacticResults))
-> IO [TacticError] -> IO (Either [TacticError] RunTacticResults)
forall a b. (a -> b) -> a -> b
$ OutChan (Maybe TacticError) -> IO [TacticError]
forall a. OutChan (Maybe a) -> IO [a]
consumeChan OutChan (Maybe TacticError)
out_errs


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


------------------------------------------------------------------------------
-- | Generate a unique unification variable.
newUnivar :: MonadState TacticState m => m Type
newUnivar :: m Type
newUnivar = do
  Type -> m Type
forall (m :: * -> *). MonadState TacticState m => Type -> m Type
freshTyvars (Type -> m Type) -> Type -> m Type
forall a b. (a -> b) -> a -> b
$
    [TyVar] -> Type -> Type
mkInfForAllTys [TyVar
alphaTyVar] Type
alphaTy


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

------------------------------------------------------------------------------
-- | Get a substition out of a theta's fundeps
learnFromFundeps
    :: ThetaType
    -> RuleM ()
learnFromFundeps :: ThetaType -> RuleM ()
learnFromFundeps ThetaType
theta = do
  InstEnvs
inst_envs <- (Context -> InstEnvs)
-> RuleT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     InstEnvs
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks Context -> InstEnvs
ctxInstEnvs
  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
  TCvSubst
subst <- (TacticState -> TCvSubst)
-> RuleT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     TCvSubst
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets TacticState -> TCvSubst
ts_unifier
  let theta' :: ThetaType
theta' = HasCallStack => TCvSubst -> ThetaType -> ThetaType
TCvSubst -> ThetaType -> ThetaType
substTheta TCvSubst
subst ThetaType
theta
      fundeps :: [TypeEqn]
fundeps = (Type -> [TypeEqn]) -> ThetaType -> [TypeEqn]
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap ((FunDepEqn () -> [TypeEqn]) -> [FunDepEqn ()] -> [TypeEqn]
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap FunDepEqn () -> [TypeEqn]
forall loc. FunDepEqn loc -> [TypeEqn]
fd_eqs ([FunDepEqn ()] -> [TypeEqn])
-> (Type -> [FunDepEqn ()]) -> Type -> [TypeEqn]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. InstEnvs -> (Type -> SrcSpan -> ()) -> Type -> [FunDepEqn ()]
forall loc.
InstEnvs -> (Type -> SrcSpan -> loc) -> Type -> [FunDepEqn loc]
improveFromInstEnv InstEnvs
inst_envs (\Type
_ SrcSpan
_ -> ())) ThetaType
theta'
  case Set TyVar -> [(Type, Type)] -> Maybe TCvSubst
tryUnifyUnivarsButNotSkolemsMany Set TyVar
skolems ([(Type, Type)] -> Maybe TCvSubst)
-> [(Type, Type)] -> Maybe TCvSubst
forall a b. (a -> b) -> a -> b
$ (TypeEqn -> (Type, Type)) -> [TypeEqn] -> [(Type, Type)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap TypeEqn -> (Type, Type)
forall a. Pair a -> (a, a)
unPair [TypeEqn]
fundeps 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 <- (Context -> OccName)
-> TacticT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     OccName
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks ((OccName, CType) -> OccName
forall a b. (a, b) -> a
fst ((OccName, CType) -> OccName)
-> (Context -> (OccName, CType)) -> Context -> OccName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(OccName, CType)] -> (OccName, CType)
forall a. [a] -> a
head ([(OccName, CType)] -> (OccName, CType))
-> (Context -> [(OccName, CType)]) -> Context -> (OccName, CType)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 -> ThetaType -> TacticsM (Maybe (Class, Type))
getKnownInstance OccName
f ThetaType
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 -> ThetaType -> TacticsM (Maybe (Class, Type))
forall (m :: * -> *).
MonadReader Context m =>
Class -> ThetaType -> m (Maybe (Class, Type))
getInstance Class
cls ThetaType
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 :: TacticsM [(OccName, CType)]
getCurrentDefinitions = do
  [(OccName, CType)]
ctx_funcs <- (Context -> [(OccName, CType)]) -> TacticsM [(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))
-> TacticsM [(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))
 -> TacticsM [(OccName, CType)])
-> ((OccName, CType)
    -> TacticT
         Judgement
         (Synthesized (LHsExpr GhcPs))
         TacticError
         TacticState
         ExtractM
         (OccName, CType))
-> TacticsM [(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, ThetaType
_) <- Type -> Maybe ([DataCon], ThetaType)
tacticsGetDataCons Type
codomain
  ([DataCon]
hi_dcs, ThetaType
_) <- Type -> Maybe ([DataCon], ThetaType)
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)