{-# 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
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
runTactic
:: Context
-> Judgement
-> TacticsM ()
-> 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
}
[(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 []
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)
-> 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
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
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) }
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 -> TacticError -> RuleM ()
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (CType -> CType -> TacticError
UnificationError CType
inst CType
goal)
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
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
)
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
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
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 ()