{-# LANGUAGE RecordWildCards       #-}

module Wingman.Machinery where

import           Class (Class (classTyVars))
import           Control.Lens ((<>~))
import           Control.Monad.Error.Class
import           Control.Monad.Reader
import           Control.Monad.State.Class (gets, modify)
import           Control.Monad.State.Strict (StateT (..))
import           Data.Bool (bool)
import           Data.Coerce
import           Data.Either
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           Data.Set (Set)
import qualified Data.Set as S
import           Development.IDE.GHC.Compat
import           OccName (HasOccName (occName))
import           Refinery.ProofState
import           Refinery.Tactic
import           Refinery.Tactic.Internal
import           TcType
import           Type
import           Unify
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


------------------------------------------------------------------------------
-- | Produce a subgoal that must be solved before we can solve the original
-- goal.
newSubgoal
    :: Judgement
    -> Rule
newSubgoal :: Judgement -> Rule
newSubgoal Judgement
j = do
    TCvSubst
unifier <- (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
    Judgement -> Rule
forall jdg ext (m :: * -> *). MonadRule jdg ext m => jdg -> m ext
subgoal
      (Judgement -> Rule) -> Judgement -> Rule
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
j


------------------------------------------------------------------------------
-- | Attempt to generate a term of the right type using in-scope bindings, and
-- a given tactic.
runTactic
    :: Context
    -> Judgement
    -> TacticsM ()       -- ^ Tactic to use
    -> Either [TacticError] RunTacticResults
runTactic :: Context
-> Judgement
-> TacticsM ()
-> Either [TacticError] RunTacticResults
runTactic Context
ctx Judgement
jdg TacticsM ()
t =
    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
            }
    in case [Either
   TacticError
   (Synthesized (LHsExpr GhcPs), TacticState, [Judgement])]
-> ([TacticError],
    [(Synthesized (LHsExpr GhcPs), TacticState, [Judgement])])
forall a b. [Either a b] -> ([a], [b])
partitionEithers
          ([Either
    TacticError
    (Synthesized (LHsExpr GhcPs), TacticState, [Judgement])]
 -> ([TacticError],
     [(Synthesized (LHsExpr GhcPs), TacticState, [Judgement])]))
-> (ExtractM
      [Either
         TacticError
         (Synthesized (LHsExpr GhcPs), TacticState, [Judgement])]
    -> [Either
          TacticError
          (Synthesized (LHsExpr GhcPs), TacticState, [Judgement])])
-> ExtractM
     [Either
        TacticError
        (Synthesized (LHsExpr GhcPs), TacticState, [Judgement])]
-> ([TacticError],
    [(Synthesized (LHsExpr GhcPs), TacticState, [Judgement])])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Reader
   Context
   [Either
      TacticError
      (Synthesized (LHsExpr GhcPs), TacticState, [Judgement])]
 -> Context
 -> [Either
       TacticError
       (Synthesized (LHsExpr GhcPs), TacticState, [Judgement])])
-> Context
-> Reader
     Context
     [Either
        TacticError
        (Synthesized (LHsExpr GhcPs), TacticState, [Judgement])]
-> [Either
      TacticError
      (Synthesized (LHsExpr GhcPs), TacticState, [Judgement])]
forall a b c. (a -> b -> c) -> b -> a -> c
flip Reader
  Context
  [Either
     TacticError
     (Synthesized (LHsExpr GhcPs), TacticState, [Judgement])]
-> Context
-> [Either
      TacticError
      (Synthesized (LHsExpr GhcPs), TacticState, [Judgement])]
forall r a. Reader r a -> r -> a
runReader Context
ctx
          (Reader
   Context
   [Either
      TacticError
      (Synthesized (LHsExpr GhcPs), TacticState, [Judgement])]
 -> [Either
       TacticError
       (Synthesized (LHsExpr GhcPs), TacticState, [Judgement])])
-> (ExtractM
      [Either
         TacticError
         (Synthesized (LHsExpr GhcPs), TacticState, [Judgement])]
    -> Reader
         Context
         [Either
            TacticError
            (Synthesized (LHsExpr GhcPs), TacticState, [Judgement])])
-> ExtractM
     [Either
        TacticError
        (Synthesized (LHsExpr GhcPs), TacticState, [Judgement])]
-> [Either
      TacticError
      (Synthesized (LHsExpr GhcPs), TacticState, [Judgement])]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ExtractM
  [Either
     TacticError
     (Synthesized (LHsExpr GhcPs), TacticState, [Judgement])]
-> Reader
     Context
     [Either
        TacticError
        (Synthesized (LHsExpr GhcPs), TacticState, [Judgement])]
forall a. ExtractM a -> Reader Context a
unExtractM
          (ExtractM
   [Either
      TacticError
      (Synthesized (LHsExpr GhcPs), TacticState, [Judgement])]
 -> ([TacticError],
     [(Synthesized (LHsExpr GhcPs), TacticState, [Judgement])]))
-> ExtractM
     [Either
        TacticError
        (Synthesized (LHsExpr GhcPs), TacticState, [Judgement])]
-> ([TacticError],
    [(Synthesized (LHsExpr GhcPs), TacticState, [Judgement])])
forall a b. (a -> b) -> a -> b
$ TacticsM ()
-> Judgement
-> TacticState
-> ExtractM
     [Either
        TacticError
        (Synthesized (LHsExpr GhcPs), TacticState, [Judgement])]
forall ext (m :: * -> *) jdg err s.
MonadExtract ext m =>
TacticT jdg ext err s m ()
-> jdg -> s -> m [Either err (ext, s, [jdg])]
runTacticT TacticsM ()
t Judgement
jdg TacticState
tacticState of
      ([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
      ([TacticError]
_, ((Synthesized (LHsExpr GhcPs), TacticState, [Judgement])
 -> (Synthesized (LHsExpr GhcPs), (TacticState, [Judgement])))
-> [(Synthesized (LHsExpr GhcPs), TacticState, [Judgement])]
-> [(Synthesized (LHsExpr GhcPs), (TacticState, [Judgement]))]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Synthesized (LHsExpr GhcPs), TacticState, [Judgement])
-> (Synthesized (LHsExpr GhcPs), (TacticState, [Judgement]))
forall a b c. (a, b, c) -> (a, (b, c))
assoc23 -> [(Synthesized (LHsExpr GhcPs), (TacticState, [Judgement]))]
solns) -> do
        let sorted :: [(Synthesized (LHsExpr GhcPs), (TacticState, [Judgement]))]
sorted =
              (((Synthesized (LHsExpr GhcPs), (TacticState, [Judgement]))
  -> (Synthesized (LHsExpr GhcPs), (TacticState, [Judgement]))
  -> Ordering)
 -> [(Synthesized (LHsExpr GhcPs), (TacticState, [Judgement]))]
 -> [(Synthesized (LHsExpr GhcPs), (TacticState, [Judgement]))])
-> [(Synthesized (LHsExpr GhcPs), (TacticState, [Judgement]))]
-> ((Synthesized (LHsExpr GhcPs), (TacticState, [Judgement]))
    -> (Synthesized (LHsExpr GhcPs), (TacticState, [Judgement]))
    -> Ordering)
-> [(Synthesized (LHsExpr GhcPs), (TacticState, [Judgement]))]
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((Synthesized (LHsExpr GhcPs), (TacticState, [Judgement]))
 -> (Synthesized (LHsExpr GhcPs), (TacticState, [Judgement]))
 -> Ordering)
-> [(Synthesized (LHsExpr GhcPs), (TacticState, [Judgement]))]
-> [(Synthesized (LHsExpr GhcPs), (TacticState, [Judgement]))]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy [(Synthesized (LHsExpr GhcPs), (TacticState, [Judgement]))]
solns (((Synthesized (LHsExpr GhcPs), (TacticState, [Judgement]))
  -> (Synthesized (LHsExpr GhcPs), (TacticState, [Judgement]))
  -> Ordering)
 -> [(Synthesized (LHsExpr GhcPs), (TacticState, [Judgement]))])
-> ((Synthesized (LHsExpr GhcPs), (TacticState, [Judgement]))
    -> (Synthesized (LHsExpr GhcPs), (TacticState, [Judgement]))
    -> Ordering)
-> [(Synthesized (LHsExpr GhcPs), (TacticState, [Judgement]))]
forall a b. (a -> b) -> a -> b
$ ((Synthesized (LHsExpr GhcPs), (TacticState, [Judgement]))
 -> Down
      (Penalize Int, Reward Bool, Penalize Int, Penalize Int, Reward Int,
       Penalize Int, Penalize Int))
-> (Synthesized (LHsExpr GhcPs), (TacticState, [Judgement]))
-> (Synthesized (LHsExpr GhcPs), (TacticState, [Judgement]))
-> Ordering
forall a b. Ord a => (b -> a) -> b -> b -> Ordering
comparing (((Synthesized (LHsExpr GhcPs), (TacticState, [Judgement]))
  -> Down
       (Penalize Int, Reward Bool, Penalize Int, Penalize Int, Reward Int,
        Penalize Int, Penalize Int))
 -> (Synthesized (LHsExpr GhcPs), (TacticState, [Judgement]))
 -> (Synthesized (LHsExpr GhcPs), (TacticState, [Judgement]))
 -> Ordering)
-> ((Synthesized (LHsExpr GhcPs), (TacticState, [Judgement]))
    -> Down
         (Penalize Int, Reward Bool, Penalize Int, Penalize Int, Reward Int,
          Penalize Int, Penalize Int))
-> (Synthesized (LHsExpr GhcPs), (TacticState, [Judgement]))
-> (Synthesized (LHsExpr GhcPs), (TacticState, [Judgement]))
-> Ordering
forall a b. (a -> b) -> a -> b
$ \(Synthesized (LHsExpr GhcPs)
ext, (TacticState
_, [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]
holes
        case [(Synthesized (LHsExpr GhcPs), (TacticState, [Judgement]))]
sorted of
          ((Synthesized (LHsExpr GhcPs)
syn, (TacticState, [Judgement])
_) : [(Synthesized (LHsExpr GhcPs), (TacticState, [Judgement]))]
_) ->
            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
-> [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_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)])
-> ([(Synthesized (LHsExpr GhcPs), (TacticState, [Judgement]))]
    -> [Synthesized (LHsExpr GhcPs)])
-> [(Synthesized (LHsExpr GhcPs), (TacticState, [Judgement]))]
-> [Synthesized (LHsExpr GhcPs)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Synthesized (LHsExpr GhcPs), (TacticState, [Judgement]))
 -> Synthesized (LHsExpr GhcPs))
-> [(Synthesized (LHsExpr GhcPs), (TacticState, [Judgement]))]
-> [Synthesized (LHsExpr GhcPs)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Synthesized (LHsExpr GhcPs), (TacticState, [Judgement]))
-> Synthesized (LHsExpr GhcPs)
forall a b. (a, b) -> a
fst ([(Synthesized (LHsExpr GhcPs), (TacticState, [Judgement]))]
 -> [Synthesized (LHsExpr GhcPs)])
-> [(Synthesized (LHsExpr GhcPs), (TacticState, [Judgement]))]
-> [Synthesized (LHsExpr GhcPs)]
forall a b. (a -> b) -> a -> b
$ [(Synthesized (LHsExpr GhcPs), (TacticState, [Judgement]))]
sorted
                , rtr_jdg :: Judgement
rtr_jdg = Judgement
jdg
                , rtr_ctx :: Context
rtr_ctx = Context
ctx
                }
          -- guaranteed to not be empty
          [(Synthesized (LHsExpr GhcPs), (TacticState, [Judgement]))]
_ -> [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)
-> ProofStateT ext ext err s m (a, jdg)
-> ProofStateT ext ext err s m (a, jdg)
forall (m :: * -> *) a b ext' err s jdg.
Functor m =>
(a -> b)
-> ProofStateT ext' a err s m jdg -> ProofStateT ext' b err s m jdg
mapExtract' 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


------------------------------------------------------------------------------
-- | Like 'tcUnifyTy', but takes a list of skolems to prevent unification of.
tryUnifyUnivarsButNotSkolems :: Set TyVar -> CType -> CType -> Maybe TCvSubst
tryUnifyUnivarsButNotSkolems :: Set TyVar -> CType -> CType -> Maybe TCvSubst
tryUnifyUnivarsButNotSkolems Set TyVar
skolems CType
goal CType
inst =
  case (TyVar -> BindFlag) -> [Type] -> [Type] -> UnifyResult
tcUnifyTysFG
         (BindFlag -> BindFlag -> Bool -> BindFlag
forall a. a -> a -> Bool -> a
bool BindFlag
BindMe BindFlag
Skolem (Bool -> BindFlag) -> (TyVar -> Bool) -> TyVar -> BindFlag
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TyVar -> Set TyVar -> Bool) -> Set TyVar -> TyVar -> Bool
forall a b c. (a -> b -> c) -> b -> a -> c
flip TyVar -> Set TyVar -> Bool
forall a. Ord a => a -> Set a -> Bool
S.member Set TyVar
skolems)
         [CType -> Type
unCType CType
inst]
         [CType -> Type
unCType CType
goal] of
    Unifiable TCvSubst
subst -> TCvSubst -> Maybe TCvSubst
forall (f :: * -> *) a. Applicative f => a -> f a
pure TCvSubst
subst
    UnifyResult
_               -> Maybe TCvSubst
forall a. Maybe a
Nothing


updateSubst :: TCvSubst -> TacticState -> TacticState
updateSubst :: TCvSubst -> TacticState -> TacticState
updateSubst TCvSubst
subst TacticState
s = TacticState
s { ts_unifier :: TCvSubst
ts_unifier = TCvSubst -> TCvSubst -> TCvSubst
unionTCvSubst TCvSubst
subst (TacticState -> TCvSubst
ts_unifier TacticState
s) }



------------------------------------------------------------------------------
-- | 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 -> TacticError -> RuleM ()
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (CType -> CType -> TacticError
UnificationError CType
inst CType
goal)


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


------------------------------------------------------------------------------
-- | Get the class methods of a 'PredType', correctly dealing with
-- instantiation of quantified class types.
methodHypothesis :: PredType -> Maybe [HyInfo CType]
methodHypothesis :: Type -> Maybe [HyInfo CType]
methodHypothesis Type
ty = do
  (TyCon
tc, [Type]
apps) <- HasDebugCallStack => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe Type
ty
  Class
cls <- TyCon -> Maybe Class
tyConClass_maybe TyCon
tc
  let methods :: [TyVar]
methods = Class -> [TyVar]
classMethods Class
cls
      tvs :: [TyVar]
tvs     = Class -> [TyVar]
classTyVars Class
cls
      subst :: TCvSubst
subst   = [TyVar] -> [Type] -> TCvSubst
HasDebugCallStack => [TyVar] -> [Type] -> TCvSubst
zipTvSubst [TyVar]
tvs [Type]
apps
  [HyInfo CType] -> Maybe [HyInfo CType]
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([HyInfo CType] -> Maybe [HyInfo CType])
-> [HyInfo CType] -> Maybe [HyInfo CType]
forall a b. (a -> b) -> a -> b
$ [TyVar]
methods [TyVar] -> (TyVar -> HyInfo CType) -> [HyInfo CType]
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \TyVar
method ->
    let ([TyVar]
_, [Type]
_, Type
ty) = Type -> ([TyVar], [Type], Type)
tcSplitSigmaTy (Type -> ([TyVar], [Type], Type))
-> Type -> ([TyVar], [Type], Type)
forall a b. (a -> b) -> a -> b
$ TyVar -> Type
idType TyVar
method
    in ( OccName -> Provenance -> CType -> HyInfo CType
forall a. OccName -> Provenance -> a -> HyInfo a
HyInfo (TyVar -> OccName
forall name. HasOccName name => name -> OccName
occName TyVar
method) (Uniquely Class -> Provenance
ClassMethodPrv (Uniquely Class -> Provenance) -> Uniquely Class -> Provenance
forall a b. (a -> b) -> a -> b
$ Class -> Uniquely Class
forall a. a -> Uniquely a
Uniquely Class
cls) (CType -> HyInfo CType) -> CType -> HyInfo CType
forall a b. (a -> b) -> a -> b
$ Type -> CType
CType (Type -> CType) -> Type -> CType
forall a b. (a -> b) -> a -> b
$ HasCallStack => TCvSubst -> Type -> Type
TCvSubst -> Type -> Type
substTy TCvSubst
subst Type
ty
       )


------------------------------------------------------------------------------
-- | Mystical time-traveling combinator for inspecting the extracts produced by
-- a tactic. We can use it to guard that extracts match certain predicates, for
-- example.
--
-- Note, that this thing is WEIRD. To illustrate:
--
-- @@
-- peek f
-- blah
-- @@
--
-- Here, @f@ can inspect the extract _produced by @blah@,_  which means the
-- causality appears to go backwards.
--
-- 'peek' should be exposed directly by @refinery@ in the next release.
peek :: (ext -> TacticT jdg ext err s m ()) -> TacticT jdg ext err s m ()
peek :: (ext -> TacticT jdg ext err s m ()) -> TacticT jdg ext err s m ()
peek ext -> TacticT jdg ext err s m ()
k = (jdg -> ProofStateT ext ext err s m ((), jdg))
-> TacticT jdg ext err s m ()
forall jdg ext err s (m :: * -> *) a.
(jdg -> ProofStateT ext ext err s m (a, jdg))
-> TacticT jdg ext err s m a
tactic ((jdg -> ProofStateT ext ext err s m ((), jdg))
 -> TacticT jdg ext err s m ())
-> (jdg -> ProofStateT ext ext err s m ((), jdg))
-> TacticT jdg ext err s m ()
forall a b. (a -> b) -> a -> b
$ \jdg
j -> ((), jdg)
-> (ext -> ProofStateT ext ext err s m ((), jdg))
-> ProofStateT ext ext err s m ((), jdg)
forall ext' ext err s (m :: * -> *) goal.
goal
-> (ext' -> ProofStateT ext' ext err s m goal)
-> ProofStateT ext' ext err s m goal
Subgoal ((), jdg
j) ((ext -> ProofStateT ext ext err s m ((), jdg))
 -> ProofStateT ext ext err s m ((), jdg))
-> (ext -> ProofStateT ext ext err s m ((), jdg))
-> ProofStateT ext ext err s m ((), jdg)
forall a b. (a -> b) -> a -> b
$ \ext
e -> TacticT jdg ext err s m ()
-> jdg -> ProofStateT ext ext err s m ((), jdg)
forall jdg ext err s (m :: * -> *) a.
TacticT jdg ext err s m a
-> jdg -> ProofStateT ext ext err s m (a, jdg)
proofState (ext -> TacticT jdg ext err s m ()
k ext
e) jdg
j


------------------------------------------------------------------------------
-- | 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 e (m :: * -> *) a. MonadError e m => e -> m a
throwError 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 ()