{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE TupleSections #-}
module Wingman.Machinery where
import Control.Applicative (empty)
import Control.Lens ((<>~))
import Control.Monad.Reader
import Control.Monad.State.Class (gets, modify, MonadState)
import Control.Monad.State.Strict (StateT (..), execStateT)
import Control.Monad.Trans.Maybe
import Data.Coerce
import Data.Foldable
import Data.Functor ((<&>))
import Data.Generics (everything, gcount, mkQ)
import Data.Generics.Product (field')
import Data.List (sortBy)
import qualified Data.Map as M
import Data.Maybe (mapMaybe)
import Data.Monoid (getSum)
import Data.Ord (Down (..), comparing)
import qualified Data.Set as S
import Data.Traversable (for)
import Development.IDE.Core.Compile (lookupName)
import Development.IDE.GHC.Compat
import GhcPlugins (GlobalRdrElt (gre_name), lookupOccEnv, varType)
import Refinery.ProofState
import Refinery.Tactic
import Refinery.Tactic.Internal
import TcType
import Type (tyCoVarsOfTypeWellScoped)
import Wingman.Context (getInstance)
import Wingman.GHC (tryUnifyUnivarsButNotSkolems, updateSubst, tacticsGetDataCons)
import Wingman.Judgements
import Wingman.Simplify (simplify)
import Wingman.Types
substCTy :: TCvSubst -> CType -> CType
substCTy :: TCvSubst -> CType -> CType
substCTy TCvSubst
subst = Type -> CType
coerce (Type -> CType) -> (CType -> Type) -> CType -> CType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HasCallStack => TCvSubst -> Type -> Type
TCvSubst -> Type -> Type
substTy TCvSubst
subst (Type -> Type) -> (CType -> Type) -> CType -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CType -> Type
coerce
getSubstForJudgement
:: MonadState TacticState m
=> Judgement
-> m TCvSubst
getSubstForJudgement :: Judgement -> m TCvSubst
getSubstForJudgement Judgement
j = do
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
newSubgoal
:: Judgement
-> Rule
newSubgoal :: Judgement -> Rule
newSubgoal Judgement
j = do
Context
ctx <- RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
Context
forall r (m :: * -> *). MonadReader r m => m r
ask
TCvSubst
unifier <- Judgement
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
TCvSubst
forall (m :: * -> *).
MonadState TacticState m =>
Judgement -> m TCvSubst
getSubstForJudgement Judgement
j
Judgement -> Rule
forall jdg ext err s (m :: * -> *).
jdg -> RuleT jdg ext err s m ext
subgoal
(Judgement -> Rule) -> Judgement -> Rule
forall a b. (a -> b) -> a -> b
$ Context -> Judgement -> Judgement
forall (f :: * -> *). Functor f => Context -> f CType -> f CType
normalizeJudgement Context
ctx
(Judgement -> Judgement) -> Judgement -> Judgement
forall a b. (a -> b) -> a -> b
$ TCvSubst -> Judgement -> Judgement
substJdg TCvSubst
unifier
(Judgement -> Judgement) -> Judgement -> Judgement
forall a b. (a -> b) -> a -> b
$ Judgement -> Judgement
forall a. Judgement' a -> Judgement' a
unsetIsTopHole
(Judgement -> Judgement) -> Judgement -> Judgement
forall a b. (a -> b) -> a -> b
$ Context -> Judgement -> Judgement
forall (f :: * -> *). Functor f => Context -> f CType -> f CType
normalizeJudgement Context
ctx Judgement
j
tacticToRule :: Judgement -> TacticsM () -> Rule
tacticToRule :: Judgement -> TacticsM () -> Rule
tacticToRule Judgement
jdg (TacticT StateT
Judgement
(ProofStateT
(Synthesized (LHsExpr GhcPs))
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM)
()
tt) = ProofStateT
(Synthesized (LHsExpr GhcPs))
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
Judgement
-> Rule
forall jdg ext err s (m :: * -> *) a.
ProofStateT ext a err s m jdg -> RuleT jdg ext err s m a
RuleT (ProofStateT
(Synthesized (LHsExpr GhcPs))
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
Judgement
-> Rule)
-> ProofStateT
(Synthesized (LHsExpr GhcPs))
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
Judgement
-> Rule
forall a b. (a -> b) -> a -> b
$ (StateT
Judgement
(ProofStateT
(Synthesized (LHsExpr GhcPs))
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM)
()
-> Judgement
-> ProofStateT
(Synthesized (LHsExpr GhcPs))
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
Judgement)
-> Judgement
-> StateT
Judgement
(ProofStateT
(Synthesized (LHsExpr GhcPs))
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM)
()
-> ProofStateT
(Synthesized (LHsExpr GhcPs))
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
Judgement
forall a b c. (a -> b -> c) -> b -> a -> c
flip StateT
Judgement
(ProofStateT
(Synthesized (LHsExpr GhcPs))
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM)
()
-> Judgement
-> ProofStateT
(Synthesized (LHsExpr GhcPs))
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
Judgement
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m s
execStateT Judgement
jdg StateT
Judgement
(ProofStateT
(Synthesized (LHsExpr GhcPs))
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM)
()
tt ProofStateT
(Synthesized (LHsExpr GhcPs))
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
Judgement
-> (Judgement
-> ProofStateT
(Synthesized (LHsExpr GhcPs))
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
Judgement)
-> ProofStateT
(Synthesized (LHsExpr GhcPs))
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
Judgement
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (Judgement
-> (Synthesized (LHsExpr GhcPs)
-> ProofStateT
(Synthesized (LHsExpr GhcPs))
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
Judgement)
-> ProofStateT
(Synthesized (LHsExpr GhcPs))
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
Judgement)
-> (Synthesized (LHsExpr GhcPs)
-> ProofStateT
(Synthesized (LHsExpr GhcPs))
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
Judgement)
-> Judgement
-> ProofStateT
(Synthesized (LHsExpr GhcPs))
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
Judgement
forall a b c. (a -> b -> c) -> b -> a -> c
flip Judgement
-> (Synthesized (LHsExpr GhcPs)
-> ProofStateT
(Synthesized (LHsExpr GhcPs))
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
Judgement)
-> ProofStateT
(Synthesized (LHsExpr GhcPs))
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
Judgement
forall ext' ext err s (m :: * -> *) goal.
goal
-> (ext' -> ProofStateT ext' ext err s m goal)
-> ProofStateT ext' ext err s m goal
Subgoal Synthesized (LHsExpr GhcPs)
-> ProofStateT
(Synthesized (LHsExpr GhcPs))
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
Judgement
forall ext' ext err s (m :: * -> *) goal.
ext -> ProofStateT ext' ext err s m goal
Axiom
runTactic
:: Context
-> Judgement
-> TacticsM ()
-> IO (Either [TacticError] RunTacticResults)
runTactic :: Context
-> Judgement
-> TacticsM ()
-> IO (Either [TacticError] RunTacticResults)
runTactic Context
ctx Judgement
jdg TacticsM ()
t = do
let skolems :: Set TyVar
skolems = [TyVar] -> Set TyVar
forall a. Ord a => [a] -> Set a
S.fromList
([TyVar] -> Set TyVar) -> [TyVar] -> Set TyVar
forall a b. (a -> b) -> a -> b
$ (CType -> [TyVar]) -> [CType] -> [TyVar]
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (Type -> [TyVar]
tyCoVarsOfTypeWellScoped (Type -> [TyVar]) -> (CType -> Type) -> CType -> [TyVar]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CType -> Type
unCType)
([CType] -> [TyVar]) -> [CType] -> [TyVar]
forall a b. (a -> b) -> a -> b
$ (:) (Judgement -> CType
forall a. Judgement' a -> a
jGoal Judgement
jdg)
([CType] -> [CType]) -> [CType] -> [CType]
forall a b. (a -> b) -> a -> b
$ (HyInfo CType -> CType) -> [HyInfo CType] -> [CType]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap HyInfo CType -> CType
forall a. HyInfo a -> a
hi_type
([HyInfo CType] -> [CType]) -> [HyInfo CType] -> [CType]
forall a b. (a -> b) -> a -> b
$ Map OccName (HyInfo CType) -> [HyInfo CType]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList
(Map OccName (HyInfo CType) -> [HyInfo CType])
-> Map OccName (HyInfo CType) -> [HyInfo CType]
forall a b. (a -> b) -> a -> b
$ Hypothesis CType -> Map OccName (HyInfo CType)
forall a. Hypothesis a -> Map OccName (HyInfo a)
hyByName
(Hypothesis CType -> Map OccName (HyInfo CType))
-> Hypothesis CType -> Map OccName (HyInfo CType)
forall a b. (a -> b) -> a -> b
$ Judgement -> Hypothesis CType
forall a. Judgement' a -> Hypothesis a
jHypothesis Judgement
jdg
tacticState :: TacticState
tacticState =
TacticState
defaultTacticState
{ ts_skolems :: Set TyVar
ts_skolems = Set TyVar
skolems
}
Either
[TacticError]
[Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))]
res <- (ReaderT
Context
IO
(Either
[TacticError]
[Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))])
-> Context
-> IO
(Either
[TacticError]
[Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))]))
-> Context
-> ReaderT
Context
IO
(Either
[TacticError]
[Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))])
-> IO
(Either
[TacticError]
[Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))])
forall a b c. (a -> b -> c) -> b -> a -> c
flip ReaderT
Context
IO
(Either
[TacticError]
[Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))])
-> Context
-> IO
(Either
[TacticError]
[Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))])
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT Context
ctx
(ReaderT
Context
IO
(Either
[TacticError]
[Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))])
-> IO
(Either
[TacticError]
[Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))]))
-> (ExtractM
(Either
[TacticError]
[Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))])
-> ReaderT
Context
IO
(Either
[TacticError]
[Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))]))
-> ExtractM
(Either
[TacticError]
[Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))])
-> IO
(Either
[TacticError]
[Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ExtractM
(Either
[TacticError]
[Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))])
-> ReaderT
Context
IO
(Either
[TacticError]
[Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))])
forall a. ExtractM a -> ReaderT Context IO a
unExtractM
(ExtractM
(Either
[TacticError]
[Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))])
-> IO
(Either
[TacticError]
[Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))]))
-> ExtractM
(Either
[TacticError]
[Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))])
-> IO
(Either
[TacticError]
[Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))])
forall a b. (a -> b) -> a -> b
$ TacticsM ()
-> Judgement
-> TacticState
-> ExtractM
(Either
[TacticError]
[Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))])
forall meta ext err s (m :: * -> *) jdg.
MonadExtract meta ext err s m =>
TacticT jdg ext err s m ()
-> jdg -> s -> m (Either [err] [Proof s meta jdg ext])
runTacticT TacticsM ()
t Judgement
jdg TacticState
tacticState
Either [TacticError] RunTacticResults
-> IO (Either [TacticError] RunTacticResults)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either [TacticError] RunTacticResults
-> IO (Either [TacticError] RunTacticResults))
-> Either [TacticError] RunTacticResults
-> IO (Either [TacticError] RunTacticResults)
forall a b. (a -> b) -> a -> b
$ case Either
[TacticError]
[Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))]
res of
(Left [TacticError]
errs) -> [TacticError] -> Either [TacticError] RunTacticResults
forall a b. a -> Either a b
Left ([TacticError] -> Either [TacticError] RunTacticResults)
-> [TacticError] -> Either [TacticError] RunTacticResults
forall a b. (a -> b) -> a -> b
$ Int -> [TacticError] -> [TacticError]
forall a. Int -> [a] -> [a]
take Int
50 [TacticError]
errs
(Right [Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))]
solns) -> do
let sorted :: [Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))]
sorted =
((Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))
-> Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))
-> Ordering)
-> [Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))]
-> [Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))])
-> [Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))]
-> (Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))
-> Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))
-> Ordering)
-> [Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))]
forall a b c. (a -> b -> c) -> b -> a -> c
flip (Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))
-> Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))
-> Ordering)
-> [Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))]
-> [Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy [Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))]
solns ((Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))
-> Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))
-> Ordering)
-> [Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))])
-> (Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))
-> Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))
-> Ordering)
-> [Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))]
forall a b. (a -> b) -> a -> b
$ (Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))
-> Down
(Penalize Int, Reward Bool, Penalize Int, Penalize Int, Reward Int,
Penalize Int, Penalize Int))
-> Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))
-> Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))
-> Ordering
forall a b. Ord a => (b -> a) -> b -> b -> Ordering
comparing ((Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))
-> Down
(Penalize Int, Reward Bool, Penalize Int, Penalize Int, Reward Int,
Penalize Int, Penalize Int))
-> Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))
-> Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))
-> Ordering)
-> (Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))
-> Down
(Penalize Int, Reward Bool, Penalize Int, Penalize Int, Reward Int,
Penalize Int, Penalize Int))
-> Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))
-> Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))
-> Ordering
forall a b. (a -> b) -> a -> b
$ \(Proof Synthesized (LHsExpr GhcPs)
ext TacticState
_ [(Int, Judgement)]
holes) ->
(Penalize Int, Reward Bool, Penalize Int, Penalize Int, Reward Int,
Penalize Int, Penalize Int)
-> Down
(Penalize Int, Reward Bool, Penalize Int, Penalize Int, Reward Int,
Penalize Int, Penalize Int)
forall a. a -> Down a
Down ((Penalize Int, Reward Bool, Penalize Int, Penalize Int,
Reward Int, Penalize Int, Penalize Int)
-> Down
(Penalize Int, Reward Bool, Penalize Int, Penalize Int, Reward Int,
Penalize Int, Penalize Int))
-> (Penalize Int, Reward Bool, Penalize Int, Penalize Int,
Reward Int, Penalize Int, Penalize Int)
-> Down
(Penalize Int, Reward Bool, Penalize Int, Penalize Int, Reward Int,
Penalize Int, Penalize Int)
forall a b. (a -> b) -> a -> b
$ Synthesized (LHsExpr GhcPs)
-> Judgement
-> [Judgement]
-> (Penalize Int, Reward Bool, Penalize Int, Penalize Int,
Reward Int, Penalize Int, Penalize Int)
scoreSolution Synthesized (LHsExpr GhcPs)
ext Judgement
jdg ([Judgement]
-> (Penalize Int, Reward Bool, Penalize Int, Penalize Int,
Reward Int, Penalize Int, Penalize Int))
-> [Judgement]
-> (Penalize Int, Reward Bool, Penalize Int, Penalize Int,
Reward Int, Penalize Int, Penalize Int)
forall a b. (a -> b) -> a -> b
$ ((Int, Judgement) -> Judgement)
-> [(Int, Judgement)] -> [Judgement]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Int, Judgement) -> Judgement
forall a b. (a, b) -> b
snd [(Int, Judgement)]
holes
case [Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))]
sorted of
((Proof Synthesized (LHsExpr GhcPs)
syn TacticState
_ [(Int, Judgement)]
subgoals) : [Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))]
_) ->
RunTacticResults -> Either [TacticError] RunTacticResults
forall a b. b -> Either a b
Right (RunTacticResults -> Either [TacticError] RunTacticResults)
-> RunTacticResults -> Either [TacticError] RunTacticResults
forall a b. (a -> b) -> a -> b
$
RunTacticResults :: Trace
-> LHsExpr GhcPs
-> [Judgement]
-> [Synthesized (LHsExpr GhcPs)]
-> Judgement
-> Context
-> RunTacticResults
RunTacticResults
{ rtr_trace :: Trace
rtr_trace = Synthesized (LHsExpr GhcPs) -> Trace
forall a. Synthesized a -> Trace
syn_trace Synthesized (LHsExpr GhcPs)
syn
, rtr_extract :: LHsExpr GhcPs
rtr_extract = LHsExpr GhcPs -> LHsExpr GhcPs
simplify (LHsExpr GhcPs -> LHsExpr GhcPs) -> LHsExpr GhcPs -> LHsExpr GhcPs
forall a b. (a -> b) -> a -> b
$ Synthesized (LHsExpr GhcPs) -> LHsExpr GhcPs
forall a. Synthesized a -> a
syn_val Synthesized (LHsExpr GhcPs)
syn
, rtr_subgoals :: [Judgement]
rtr_subgoals = ((Int, Judgement) -> Judgement)
-> [(Int, Judgement)] -> [Judgement]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Int, Judgement) -> Judgement
forall a b. (a, b) -> b
snd [(Int, Judgement)]
subgoals
, rtr_other_solns :: [Synthesized (LHsExpr GhcPs)]
rtr_other_solns = [Synthesized (LHsExpr GhcPs)] -> [Synthesized (LHsExpr GhcPs)]
forall a. [a] -> [a]
reverse ([Synthesized (LHsExpr GhcPs)] -> [Synthesized (LHsExpr GhcPs)])
-> ([Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))]
-> [Synthesized (LHsExpr GhcPs)])
-> [Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))]
-> [Synthesized (LHsExpr GhcPs)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))
-> Synthesized (LHsExpr GhcPs))
-> [Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))]
-> [Synthesized (LHsExpr GhcPs)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))
-> Synthesized (LHsExpr GhcPs)
forall s meta goal ext. Proof s meta goal ext -> ext
pf_extract ([Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))]
-> [Synthesized (LHsExpr GhcPs)])
-> [Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))]
-> [Synthesized (LHsExpr GhcPs)]
forall a b. (a -> b) -> a -> b
$ [Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))]
sorted
, rtr_jdg :: Judgement
rtr_jdg = Judgement
jdg
, rtr_ctx :: Context
rtr_ctx = Context
ctx
}
[Proof TacticState Int Judgement (Synthesized (LHsExpr GhcPs))]
_ -> [TacticError] -> Either [TacticError] RunTacticResults
forall a b. a -> Either a b
Left []
assoc23 :: (a, b, c) -> (a, (b, c))
assoc23 :: (a, b, c) -> (a, (b, c))
assoc23 (a
a, b
b, c
c) = (a
a, (b
b, c
c))
tracePrim :: String -> Trace
tracePrim :: String -> Trace
tracePrim = (String -> [Trace] -> Trace) -> [Trace] -> String -> Trace
forall a b c. (a -> b -> c) -> b -> a -> c
flip String -> [Trace] -> Trace
forall a. (Eq a, Monoid a) => a -> [Rose a] -> Rose a
rose []
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)
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)
mappingExtract
:: Functor m
=> (ext -> ext)
-> TacticT jdg ext err s m a
-> TacticT jdg ext err s m a
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
scoreSolution
:: Synthesized (LHsExpr GhcPs)
-> Judgement
-> [Judgement]
-> ( Penalize Int
, Reward Bool
, Penalize Int
, Penalize Int
, Reward Int
, Penalize Int
, Penalize Int
)
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
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
unify :: CType
-> CType
-> RuleM ()
unify :: CType -> CType -> RuleM ()
unify CType
goal CType
inst = do
Set TyVar
skolems <- (TacticState -> Set TyVar)
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Set TyVar)
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets TacticState -> Set TyVar
ts_skolems
case Set TyVar -> CType -> CType -> Maybe TCvSubst
tryUnifyUnivarsButNotSkolems Set TyVar
skolems CType
goal CType
inst of
Just TCvSubst
subst ->
(TacticState -> TacticState) -> RuleM ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((TacticState -> TacticState) -> RuleM ())
-> (TacticState -> TacticState) -> RuleM ()
forall a b. (a -> b) -> a -> b
$ TCvSubst -> TacticState -> TacticState
updateSubst TCvSubst
subst
Maybe TCvSubst
Nothing -> RuleM ()
forall jdg ext err s (m :: * -> *) a. RuleT jdg ext err s m a
cut
cut :: RuleT jdg ext err s m a
cut :: RuleT jdg ext err s m a
cut = ProofStateT ext a err s m jdg -> RuleT jdg ext err s m a
forall jdg ext err s (m :: * -> *) a.
ProofStateT ext a err s m jdg -> RuleT jdg ext err s m a
RuleT ProofStateT ext a err s m jdg
forall ext' ext err s (m :: * -> *) goal.
ProofStateT ext' ext err s m goal
Empty
canUnify
:: MonadState TacticState m
=> CType
-> CType
-> 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
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
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
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 ()
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
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
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
lookupNameInContext :: MonadReader Context m => OccName -> m (Maybe CType)
lookupNameInContext :: OccName -> m (Maybe CType)
lookupNameInContext OccName
name = do
[(OccName, CType)]
ctx <- (Context -> [(OccName, CType)]) -> m [(OccName, CType)]
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks Context -> [(OccName, CType)]
ctxModuleFuncs
Maybe CType -> m (Maybe CType)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe CType -> m (Maybe CType)) -> Maybe CType -> m (Maybe CType)
forall a b. (a -> b) -> a -> b
$ case ((OccName, CType) -> Bool)
-> [(OccName, CType)] -> Maybe (OccName, CType)
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find ((OccName -> OccName -> Bool
forall a. Eq a => a -> a -> Bool
== OccName
name) (OccName -> Bool)
-> ((OccName, CType) -> OccName) -> (OccName, CType) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (OccName, CType) -> OccName
forall a b. (a, b) -> a
fst) [(OccName, CType)]
ctx of
Just (OccName
_, CType
ty) -> CType -> Maybe CType
forall (f :: * -> *) a. Applicative f => a -> f a
pure CType
ty
Maybe (OccName, CType)
Nothing -> Maybe CType
forall (f :: * -> *) a. Alternative f => f a
empty
getDefiningType
:: TacticsM CType
getDefiningType :: TacticsM CType
getDefiningType = do
OccName
calling_fun_name <- (OccName, CType) -> OccName
forall a b. (a, b) -> a
fst ((OccName, CType) -> OccName)
-> ([(OccName, CType)] -> (OccName, CType))
-> [(OccName, CType)]
-> OccName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(OccName, CType)] -> (OccName, CType)
forall a. [a] -> a
head ([(OccName, CType)] -> OccName)
-> TacticT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
[(OccName, CType)]
-> TacticT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
OccName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Context -> [(OccName, CType)])
-> TacticT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
[(OccName, CType)]
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks Context -> [(OccName, CType)]
ctxDefiningFuncs
TacticsM CType
-> (CType -> TacticsM CType) -> Maybe CType -> TacticsM CType
forall b a. b -> (a -> b) -> Maybe a -> b
maybe
(TacticError -> TacticsM CType
forall err jdg ext s (m :: * -> *) a.
err -> TacticT jdg ext err s m a
failure (TacticError -> TacticsM CType) -> TacticError -> TacticsM CType
forall a b. (a -> b) -> a -> b
$ OccName -> TacticError
NotInScope OccName
calling_fun_name)
CType -> TacticsM CType
forall (f :: * -> *) a. Applicative f => a -> f a
pure
(Maybe CType -> TacticsM CType)
-> TacticT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Maybe CType)
-> TacticsM CType
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< OccName
-> TacticT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Maybe CType)
forall (m :: * -> *).
MonadReader Context m =>
OccName -> m (Maybe CType)
lookupNameInContext OccName
calling_fun_name
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
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
getKnownInstance :: OccName -> [Type] -> TacticsM (Maybe (Class, PredType))
getKnownInstance :: OccName -> [Type] -> TacticsM (Maybe (Class, Type))
getKnownInstance OccName
f [Type]
tys = MaybeT
(TacticT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM)
(Class, Type)
-> TacticsM (Maybe (Class, Type))
forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT (MaybeT
(TacticT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM)
(Class, Type)
-> TacticsM (Maybe (Class, Type)))
-> MaybeT
(TacticT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM)
(Class, Type)
-> TacticsM (Maybe (Class, Type))
forall a b. (a -> b) -> a -> b
$ do
Class
cls <- TacticsM (Maybe Class)
-> MaybeT
(TacticT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM)
Class
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (TacticsM (Maybe Class)
-> MaybeT
(TacticT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM)
Class)
-> TacticsM (Maybe Class)
-> MaybeT
(TacticT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM)
Class
forall a b. (a -> b) -> a -> b
$ OccName -> TacticsM (Maybe Class)
knownClass OccName
f
TacticsM (Maybe (Class, Type))
-> MaybeT
(TacticT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM)
(Class, Type)
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (TacticsM (Maybe (Class, Type))
-> MaybeT
(TacticT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM)
(Class, Type))
-> TacticsM (Maybe (Class, Type))
-> MaybeT
(TacticT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM)
(Class, Type)
forall a b. (a -> b) -> a -> b
$ Class -> [Type] -> TacticsM (Maybe (Class, Type))
forall (m :: * -> *).
MonadReader Context m =>
Class -> [Type] -> m (Maybe (Class, Type))
getInstance Class
cls [Type]
tys
getOccNameType
:: OccName
-> TacticsM Type
getOccNameType :: OccName -> TacticsM Type
getOccNameType OccName
occ = do
OccName -> TacticsM (Maybe TyThing)
getTyThing OccName
occ TacticsM (Maybe TyThing)
-> (Maybe TyThing -> TacticsM Type) -> TacticsM Type
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
Just (AnId TyVar
v) -> Type -> TacticsM Type
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Type -> TacticsM Type) -> Type -> TacticsM Type
forall a b. (a -> b) -> a -> b
$ TyVar -> Type
varType TyVar
v
Maybe TyThing
_ -> TacticError -> TacticsM Type
forall err jdg ext s (m :: * -> *) a.
err -> TacticT jdg ext err s m a
failure (TacticError -> TacticsM Type) -> TacticError -> TacticsM Type
forall a b. (a -> b) -> a -> b
$ OccName -> TacticError
NotInScope OccName
occ
getCurrentDefinitions :: TacticsM [(OccName, CType)]
getCurrentDefinitions :: TacticT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
[(OccName, CType)]
getCurrentDefinitions = do
[(OccName, CType)]
ctx_funcs <- (Context -> [(OccName, CType)])
-> TacticT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
[(OccName, CType)]
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks Context -> [(OccName, CType)]
ctxDefiningFuncs
[(OccName, CType)]
-> ((OccName, CType)
-> TacticT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(OccName, CType))
-> TacticT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
[(OccName, CType)]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for [(OccName, CType)]
ctx_funcs (((OccName, CType)
-> TacticT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(OccName, CType))
-> TacticT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
[(OccName, CType)])
-> ((OccName, CType)
-> TacticT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(OccName, CType))
-> TacticT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
[(OccName, CType)]
forall a b. (a -> b) -> a -> b
$ \res :: (OccName, CType)
res@(OccName
occ, CType
_) ->
(OccName, CType)
-> TacticT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(OccName, CType)
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((OccName, CType)
-> TacticT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(OccName, CType))
-> (Maybe CType -> (OccName, CType))
-> Maybe CType
-> TacticT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(OccName, CType)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (OccName, CType)
-> (CType -> (OccName, CType)) -> Maybe CType -> (OccName, CType)
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (OccName, CType)
res (OccName
occ,) (Maybe CType
-> TacticT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(OccName, CType))
-> TacticT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Maybe CType)
-> TacticT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(OccName, CType)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< OccName
-> TacticT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Maybe CType)
forall (m :: * -> *).
MonadReader Context m =>
OccName -> m (Maybe CType)
lookupNameInContext OccName
occ
uncoveredDataCons :: Type -> Type -> Maybe (S.Set (Uniquely DataCon))
uncoveredDataCons :: Type -> Type -> Maybe (Set (Uniquely DataCon))
uncoveredDataCons Type
domain Type
codomain = do
([DataCon]
g_dcs, [Type]
_) <- Type -> Maybe ([DataCon], [Type])
tacticsGetDataCons Type
codomain
([DataCon]
hi_dcs, [Type]
_) <- Type -> Maybe ([DataCon], [Type])
tacticsGetDataCons Type
domain
Set (Uniquely DataCon) -> Maybe (Set (Uniquely DataCon))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Set (Uniquely DataCon) -> Maybe (Set (Uniquely DataCon)))
-> Set (Uniquely DataCon) -> Maybe (Set (Uniquely DataCon))
forall a b. (a -> b) -> a -> b
$ [Uniquely DataCon] -> Set (Uniquely DataCon)
forall a. Ord a => [a] -> Set a
S.fromList ([DataCon] -> [Uniquely DataCon]
coerce [DataCon]
hi_dcs) Set (Uniquely DataCon)
-> Set (Uniquely DataCon) -> Set (Uniquely DataCon)
forall a. Ord a => Set a -> Set a -> Set a
S.\\ [Uniquely DataCon] -> Set (Uniquely DataCon)
forall a. Ord a => [a] -> Set a
S.fromList ([DataCon] -> [Uniquely DataCon]
coerce [DataCon]
g_dcs)