{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TupleSections #-}
module Wingman.Tactics
( module Wingman.Tactics
, runTactic
) where
import ConLike (ConLike(RealDataCon))
import Control.Applicative (Alternative(empty), (<|>))
import Control.Lens ((&), (%~), (<>~))
import Control.Monad (filterM)
import Control.Monad (unless)
import Control.Monad.Extra (anyM)
import Control.Monad.Reader.Class (MonadReader (ask))
import Control.Monad.State.Strict (StateT(..), runStateT)
import Data.Bool (bool)
import Data.Foldable
import Data.Functor ((<&>))
import Data.Generics.Labels ()
import Data.List
import Data.List.Extra (dropEnd, takeEnd)
import qualified Data.Map as M
import Data.Maybe
import Data.Set (Set)
import qualified Data.Set as S
import Data.Traversable (for)
import DataCon
import Development.IDE.GHC.Compat
import GHC.Exts
import GHC.SourceGen ((@@))
import GHC.SourceGen.Expr
import Name (occNameString, occName)
import OccName (mkVarOcc)
import Refinery.Tactic
import Refinery.Tactic.Internal
import TcType
import Type hiding (Var)
import Wingman.CodeGen
import Wingman.GHC
import Wingman.Judgements
import Wingman.Machinery
import Wingman.Naming
import Wingman.StaticPlugin (pattern MetaprogramSyntax)
import Wingman.Types
assumption :: TacticsM ()
assumption :: TacticsM ()
assumption = (Judgement -> [OccName]) -> (OccName -> TacticsM ()) -> TacticsM ()
forall a. (Judgement -> [a]) -> (a -> TacticsM ()) -> TacticsM ()
attemptOn (Set OccName -> [OccName]
forall a. Set a -> [a]
S.toList (Set OccName -> [OccName])
-> (Judgement -> Set OccName) -> Judgement -> [OccName]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Judgement -> Set OccName
allNames) OccName -> TacticsM ()
assume
assume :: OccName -> TacticsM ()
assume :: OccName -> TacticsM ()
assume OccName
name = (Judgement
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized (LHsExpr GhcPs)))
-> 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
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized (LHsExpr GhcPs)))
-> TacticsM ())
-> (Judgement
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized (LHsExpr GhcPs)))
-> TacticsM ()
forall a b. (a -> b) -> a -> b
$ \Judgement
jdg -> do
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 -> 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 of
Just (HyInfo CType -> CType
forall a. HyInfo a -> a
hi_type -> CType
ty) -> do
CType -> CType -> RuleM ()
unify CType
ty (CType -> RuleM ()) -> CType -> RuleM ()
forall a b. (a -> b) -> a -> b
$ Judgement -> CType
forall a. Judgement' a -> a
jGoal Judgement
jdg
Synthesized (LHsExpr GhcPs)
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized (LHsExpr GhcPs))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Synthesized (LHsExpr GhcPs)
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized (LHsExpr GhcPs)))
-> Synthesized (LHsExpr GhcPs)
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized (LHsExpr GhcPs))
forall a b. (a -> b) -> a -> b
$
(LHsExpr GhcPs -> Synthesized (LHsExpr GhcPs)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SrcSpanLess (LHsExpr GhcPs) -> LHsExpr GhcPs
forall a. HasSrcSpan a => SrcSpanLess a -> a
noLoc (SrcSpanLess (LHsExpr GhcPs) -> LHsExpr GhcPs)
-> SrcSpanLess (LHsExpr GhcPs) -> LHsExpr GhcPs
forall a b. (a -> b) -> a -> b
$ OccName -> HsExpr GhcPs
forall a. Var a => OccName -> a
var' OccName
name))
{ syn_trace :: Trace
syn_trace = String -> Trace
tracePrim (String -> Trace) -> String -> Trace
forall a b. (a -> b) -> a -> b
$ String
"assume " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> OccName -> String
occNameString OccName
name
, syn_used_vals :: Set OccName
syn_used_vals = OccName -> Set OccName
forall a. a -> Set a
S.singleton OccName
name Set OccName -> Set OccName -> Set OccName
forall a. Semigroup a => a -> a -> a
<> Judgement -> OccName -> Set OccName
forall a. Judgement' a -> OccName -> Set OccName
getAncestry Judgement
jdg OccName
name
}
Maybe (HyInfo CType)
Nothing -> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized (LHsExpr GhcPs))
forall jdg ext err s (m :: * -> *) a. RuleT jdg ext err s m a
cut
use :: Saturation -> OccName -> TacticsM ()
use :: Saturation -> OccName -> TacticsM ()
use Saturation
sat OccName
occ = do
Context
ctx <- TacticT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
Context
forall r (m :: * -> *). MonadReader r m => m r
ask
CType
ty <- case OccName -> Context -> Maybe CType
forall (m :: * -> *).
MonadReader Context m =>
OccName -> m (Maybe CType)
lookupNameInContext OccName
occ Context
ctx of
Just CType
ty -> CType
-> TacticT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
CType
forall (f :: * -> *) a. Applicative f => a -> f a
pure CType
ty
Maybe CType
Nothing -> Type -> CType
CType (Type -> CType)
-> TacticT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
Type
-> TacticT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
CType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> OccName
-> TacticT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
Type
getOccNameType OccName
occ
Saturation -> HyInfo CType -> TacticsM ()
apply Saturation
sat (HyInfo CType -> TacticsM ()) -> HyInfo CType -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ OccName -> CType -> HyInfo CType
createImportedHyInfo OccName
occ CType
ty
recursion :: TacticsM ()
recursion :: TacticsM ()
recursion = TacticsM () -> TacticsM ()
forall a. TacticsM a -> TacticsM a
requireConcreteHole (TacticsM () -> TacticsM ()) -> TacticsM () -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ String -> TacticsM () -> TacticsM ()
forall (m :: * -> *) jdg ext err s a.
Functor m =>
String
-> TacticT jdg (Synthesized ext) err s m a
-> TacticT jdg (Synthesized ext) err s m a
tracing String
"recursion" (TacticsM () -> TacticsM ()) -> TacticsM () -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ do
[(OccName, CType)]
defs <- TacticsM [(OccName, CType)]
getCurrentDefinitions
(Judgement -> [(OccName, CType)])
-> ((OccName, CType) -> TacticsM ()) -> TacticsM ()
forall a. (Judgement -> [a]) -> (a -> TacticsM ()) -> TacticsM ()
attemptOn ([(OccName, CType)] -> Judgement -> [(OccName, CType)]
forall a b. a -> b -> a
const [(OccName, CType)]
defs) (((OccName, CType) -> TacticsM ()) -> TacticsM ())
-> ((OccName, CType) -> TacticsM ()) -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ \(OccName
name, CType
ty) -> TacticsM () -> TacticsM ()
forall (m :: * -> *) jdg ext err s a.
Functor m =>
TacticT jdg (Synthesized ext) err s m a
-> TacticT jdg (Synthesized ext) err s m a
markRecursion (TacticsM () -> TacticsM ()) -> TacticsM () -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ 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
TacticsM ()
-> (Synthesized (LHsExpr GhcPs) -> Maybe TacticError)
-> TacticsM ()
forall meta ext err s (m :: * -> *) jdg.
(MetaSubst meta ext, MonadExtract meta ext err s m) =>
TacticT jdg ext err s m ()
-> (ext -> Maybe err) -> TacticT jdg ext err s m ()
peek
( do
let hy' :: Hypothesis CType
hy' = [(OccName, CType)] -> Hypothesis CType
forall a. [(OccName, a)] -> Hypothesis a
recursiveHypothesis [(OccName, CType)]
defs
Context
ctx <- TacticT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
Context
forall r (m :: * -> *). MonadReader r m => m r
ask
TacticsM () -> (Judgement -> Judgement) -> TacticsM ()
forall a. TacticsM a -> (Judgement -> Judgement) -> TacticsM a
localTactic (Saturation -> HyInfo CType -> TacticsM ()
apply Saturation
Saturated (HyInfo CType -> TacticsM ()) -> HyInfo CType -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ OccName -> Provenance -> CType -> HyInfo CType
forall a. OccName -> Provenance -> a -> HyInfo a
HyInfo OccName
name Provenance
RecursivePrv CType
ty) (Context -> Hypothesis CType -> Judgement -> Judgement
introduce Context
ctx Hypothesis CType
hy')
TacticsM () -> [TacticsM ()] -> TacticsM ()
forall (m :: * -> *) jdg ext err s a.
Functor m =>
TacticT jdg ext err s m a
-> [TacticT jdg ext err s m a] -> TacticT jdg ext err s m a
<@> (Int -> TacticsM ()) -> [Int] -> [TacticsM ()]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (TacticsM () -> (Judgement -> Judgement) -> TacticsM ()
forall a. TacticsM a -> (Judgement -> Judgement) -> TacticsM a
localTactic TacticsM ()
assumption ((Judgement -> Judgement) -> TacticsM ())
-> (Int -> Judgement -> Judgement) -> Int -> TacticsM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OccName -> Int -> Judgement -> Judgement
filterPosition OccName
name) [Int
0..]
) ((Synthesized (LHsExpr GhcPs) -> Maybe TacticError) -> TacticsM ())
-> (Synthesized (LHsExpr GhcPs) -> Maybe TacticError)
-> TacticsM ()
forall a b. (a -> b) -> a -> b
$ \Synthesized (LHsExpr GhcPs)
ext -> do
let pat_vals :: Map OccName PatVal
pat_vals = Judgement -> Map OccName PatVal
forall a. Judgement' a -> Map OccName PatVal
jPatHypothesis Judgement
jdg
case ((OccName -> Bool) -> Set OccName -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any ((OccName -> Map OccName PatVal -> Bool)
-> Map OccName PatVal -> OccName -> Bool
forall a b c. (a -> b -> c) -> b -> a -> c
flip OccName -> Map OccName PatVal -> Bool
forall k a. Ord k => k -> Map k a -> Bool
M.member Map OccName PatVal
pat_vals) (Set OccName -> Bool) -> Set OccName -> Bool
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) of
Bool
True -> Maybe TacticError
forall a. Maybe a
Nothing
Bool
False -> TacticError -> Maybe TacticError
forall a. a -> Maybe a
Just TacticError
UnhelpfulRecursion
restrictPositionForApplication :: TacticsM () -> TacticsM () -> TacticsM ()
restrictPositionForApplication :: TacticsM () -> TacticsM () -> TacticsM ()
restrictPositionForApplication TacticsM ()
f TacticsM ()
app = do
OccName
name <- [OccName] -> OccName
forall a. [a] -> a
head ([OccName] -> OccName)
-> ([(OccName, CType)] -> [OccName])
-> [(OccName, CType)]
-> OccName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((OccName, CType) -> OccName) -> [(OccName, CType)] -> [OccName]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (OccName, CType) -> OccName
forall a b. (a, b) -> a
fst ([(OccName, CType)] -> OccName)
-> TacticsM [(OccName, CType)]
-> TacticT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
OccName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TacticsM [(OccName, CType)]
getCurrentDefinitions
TacticsM ()
f TacticsM () -> [TacticsM ()] -> TacticsM ()
forall (m :: * -> *) jdg ext err s a.
Functor m =>
TacticT jdg ext err s m a
-> [TacticT jdg ext err s m a] -> TacticT jdg ext err s m a
<@>
(Int -> TacticsM ()) -> [Int] -> [TacticsM ()]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap
(TacticsM () -> (Judgement -> Judgement) -> TacticsM ()
forall a. TacticsM a -> (Judgement -> Judgement) -> TacticsM a
localTactic TacticsM ()
app ((Judgement -> Judgement) -> TacticsM ())
-> (Int -> Judgement -> Judgement) -> Int -> TacticsM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OccName -> Int -> Judgement -> Judgement
filterPosition OccName
name) [Int
0..]
intros :: TacticsM ()
intros :: TacticsM ()
intros = IntroParams -> TacticsM ()
intros' IntroParams
IntroduceAllUnnamed
data IntroParams
= IntroduceAllUnnamed
| IntroduceOnlyNamed [OccName]
| IntroduceOnlyUnnamed Int
deriving stock (IntroParams -> IntroParams -> Bool
(IntroParams -> IntroParams -> Bool)
-> (IntroParams -> IntroParams -> Bool) -> Eq IntroParams
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: IntroParams -> IntroParams -> Bool
$c/= :: IntroParams -> IntroParams -> Bool
== :: IntroParams -> IntroParams -> Bool
$c== :: IntroParams -> IntroParams -> Bool
Eq, Eq IntroParams
Eq IntroParams
-> (IntroParams -> IntroParams -> Ordering)
-> (IntroParams -> IntroParams -> Bool)
-> (IntroParams -> IntroParams -> Bool)
-> (IntroParams -> IntroParams -> Bool)
-> (IntroParams -> IntroParams -> Bool)
-> (IntroParams -> IntroParams -> IntroParams)
-> (IntroParams -> IntroParams -> IntroParams)
-> Ord IntroParams
IntroParams -> IntroParams -> Bool
IntroParams -> IntroParams -> Ordering
IntroParams -> IntroParams -> IntroParams
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
min :: IntroParams -> IntroParams -> IntroParams
$cmin :: IntroParams -> IntroParams -> IntroParams
max :: IntroParams -> IntroParams -> IntroParams
$cmax :: IntroParams -> IntroParams -> IntroParams
>= :: IntroParams -> IntroParams -> Bool
$c>= :: IntroParams -> IntroParams -> Bool
> :: IntroParams -> IntroParams -> Bool
$c> :: IntroParams -> IntroParams -> Bool
<= :: IntroParams -> IntroParams -> Bool
$c<= :: IntroParams -> IntroParams -> Bool
< :: IntroParams -> IntroParams -> Bool
$c< :: IntroParams -> IntroParams -> Bool
compare :: IntroParams -> IntroParams -> Ordering
$ccompare :: IntroParams -> IntroParams -> Ordering
$cp1Ord :: Eq IntroParams
Ord, Int -> IntroParams -> String -> String
[IntroParams] -> String -> String
IntroParams -> String
(Int -> IntroParams -> String -> String)
-> (IntroParams -> String)
-> ([IntroParams] -> String -> String)
-> Show IntroParams
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
showList :: [IntroParams] -> String -> String
$cshowList :: [IntroParams] -> String -> String
show :: IntroParams -> String
$cshow :: IntroParams -> String
showsPrec :: Int -> IntroParams -> String -> String
$cshowsPrec :: Int -> IntroParams -> String -> String
Show)
intros'
:: IntroParams
-> TacticsM ()
intros' :: IntroParams -> TacticsM ()
intros' IntroParams
params = (Judgement
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized (LHsExpr GhcPs)))
-> 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
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized (LHsExpr GhcPs)))
-> TacticsM ())
-> (Judgement
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized (LHsExpr GhcPs)))
-> TacticsM ()
forall a b. (a -> b) -> a -> b
$ \Judgement
jdg -> do
let g :: CType
g = Judgement -> CType
forall a. Judgement' a -> a
jGoal Judgement
jdg
case Type -> ([TyVar], ThetaType, ThetaType, Type)
tacticsSplitFunTy (Type -> ([TyVar], ThetaType, ThetaType, Type))
-> Type -> ([TyVar], ThetaType, ThetaType, Type)
forall a b. (a -> b) -> a -> b
$ CType -> Type
unCType CType
g of
([TyVar]
_, ThetaType
_, [], Type
_) -> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized (LHsExpr GhcPs))
forall jdg ext err s (m :: * -> *) a. RuleT jdg ext err s m a
cut
([TyVar]
_, ThetaType
_, ThetaType
args, Type
res) -> do
Context
ctx <- RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
Context
forall r (m :: * -> *). MonadReader r m => m r
ask
let gen_names :: [OccName]
gen_names = Set OccName -> ThetaType -> [OccName]
forall (t :: * -> *).
Traversable t =>
Set OccName -> t Type -> t OccName
mkManyGoodNames (Hypothesis CType -> Set OccName
forall a. Hypothesis a -> Set OccName
hyNamesInScope (Hypothesis CType -> Set OccName)
-> Hypothesis CType -> Set OccName
forall a b. (a -> b) -> a -> b
$ Judgement -> Hypothesis CType
forall a. Judgement' a -> Hypothesis a
jEntireHypothesis Judgement
jdg) ThetaType
args
occs :: [OccName]
occs = case IntroParams
params of
IntroParams
IntroduceAllUnnamed -> [OccName]
gen_names
IntroduceOnlyNamed [OccName]
names -> [OccName]
names
IntroduceOnlyUnnamed Int
n -> Int -> [OccName] -> [OccName]
forall a. Int -> [a] -> [a]
take Int
n [OccName]
gen_names
num_occs :: Int
num_occs = [OccName] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [OccName]
occs
top_hole :: Maybe OccName
top_hole = Context -> Judgement -> Maybe OccName
forall a. Context -> Judgement' a -> Maybe OccName
isTopHole Context
ctx Judgement
jdg
bindings :: [(OccName, CType)]
bindings = [OccName] -> [CType] -> [(OccName, CType)]
forall a b. [a] -> [b] -> [(a, b)]
zip [OccName]
occs ([CType] -> [(OccName, CType)]) -> [CType] -> [(OccName, CType)]
forall a b. (a -> b) -> a -> b
$ ThetaType -> [CType]
coerce ThetaType
args
bound_occs :: [OccName]
bound_occs = ((OccName, CType) -> OccName) -> [(OccName, CType)] -> [OccName]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (OccName, CType) -> OccName
forall a b. (a, b) -> a
fst [(OccName, CType)]
bindings
hy' :: Hypothesis CType
hy' = Maybe OccName -> [(OccName, CType)] -> Hypothesis CType
forall a. Maybe OccName -> [(OccName, a)] -> Hypothesis a
lambdaHypothesis Maybe OccName
top_hole [(OccName, CType)]
bindings
jdg' :: Judgement
jdg' = Context -> Hypothesis CType -> Judgement -> Judgement
introduce Context
ctx Hypothesis CType
hy'
(Judgement -> Judgement) -> Judgement -> Judgement
forall a b. (a -> b) -> a -> b
$ CType -> Judgement -> Judgement
forall a. a -> Judgement' a -> Judgement' a
withNewGoal (Type -> CType
CType (Type -> CType) -> Type -> CType
forall a b. (a -> b) -> a -> b
$ ThetaType -> Type -> Type
mkFunTys' (Int -> ThetaType -> ThetaType
forall a. Int -> [a] -> [a]
drop Int
num_occs ThetaType
args) Type
res) Judgement
jdg
Synthesized (LHsExpr GhcPs)
ext <- Judgement
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized (LHsExpr GhcPs))
newSubgoal Judgement
jdg'
Synthesized (LHsExpr GhcPs)
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized (LHsExpr GhcPs))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Synthesized (LHsExpr GhcPs)
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized (LHsExpr GhcPs)))
-> Synthesized (LHsExpr GhcPs)
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized (LHsExpr GhcPs))
forall a b. (a -> b) -> a -> b
$
Synthesized (LHsExpr GhcPs)
ext
Synthesized (LHsExpr GhcPs)
-> (Synthesized (LHsExpr GhcPs) -> Synthesized (LHsExpr GhcPs))
-> Synthesized (LHsExpr GhcPs)
forall a b. a -> (a -> b) -> b
& IsLabel
"syn_trace"
(ASetter
(Synthesized (LHsExpr GhcPs))
(Synthesized (LHsExpr GhcPs))
Trace
Trace)
ASetter
(Synthesized (LHsExpr GhcPs))
(Synthesized (LHsExpr GhcPs))
Trace
Trace
#syn_trace ASetter
(Synthesized (LHsExpr GhcPs))
(Synthesized (LHsExpr GhcPs))
Trace
Trace
-> (Trace -> Trace)
-> Synthesized (LHsExpr GhcPs)
-> Synthesized (LHsExpr GhcPs)
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ String -> [Trace] -> Trace
forall a. (Eq a, Monoid a) => a -> [Rose a] -> Rose a
rose (String
"intros {" String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
", " ((OccName -> String) -> [OccName] -> [String]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap OccName -> String
forall a. Show a => a -> String
show [OccName]
bound_occs) String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
"}")
([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
Synthesized (LHsExpr GhcPs)
-> (Synthesized (LHsExpr GhcPs) -> Synthesized (LHsExpr GhcPs))
-> Synthesized (LHsExpr GhcPs)
forall a b. a -> (a -> b) -> b
& IsLabel
"syn_scoped"
(ASetter
(Synthesized (LHsExpr GhcPs))
(Synthesized (LHsExpr GhcPs))
(Hypothesis CType)
(Hypothesis CType))
ASetter
(Synthesized (LHsExpr GhcPs))
(Synthesized (LHsExpr GhcPs))
(Hypothesis CType)
(Hypothesis CType)
#syn_scoped ASetter
(Synthesized (LHsExpr GhcPs))
(Synthesized (LHsExpr GhcPs))
(Hypothesis CType)
(Hypothesis CType)
-> Hypothesis CType
-> Synthesized (LHsExpr GhcPs)
-> Synthesized (LHsExpr GhcPs)
forall a s t. Semigroup a => ASetter s t a a -> a -> s -> t
<>~ Hypothesis CType
hy'
Synthesized (LHsExpr GhcPs)
-> (Synthesized (LHsExpr GhcPs) -> Synthesized (LHsExpr GhcPs))
-> Synthesized (LHsExpr GhcPs)
forall a b. a -> (a -> b) -> b
& IsLabel
"syn_val"
(ASetter
(Synthesized (LHsExpr GhcPs))
(Synthesized (LHsExpr GhcPs))
(LHsExpr GhcPs)
(LHsExpr GhcPs))
ASetter
(Synthesized (LHsExpr GhcPs))
(Synthesized (LHsExpr GhcPs))
(LHsExpr GhcPs)
(LHsExpr GhcPs)
#syn_val ASetter
(Synthesized (LHsExpr GhcPs))
(Synthesized (LHsExpr GhcPs))
(LHsExpr GhcPs)
(LHsExpr GhcPs)
-> (LHsExpr GhcPs -> LHsExpr GhcPs)
-> Synthesized (LHsExpr GhcPs)
-> Synthesized (LHsExpr GhcPs)
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ HsExpr GhcPs -> LHsExpr GhcPs
forall a. HasSrcSpan a => SrcSpanLess a -> a
noLoc (HsExpr GhcPs -> LHsExpr GhcPs)
-> (LHsExpr GhcPs -> HsExpr GhcPs)
-> LHsExpr GhcPs
-> LHsExpr GhcPs
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Pat'] -> HsExpr GhcPs -> HsExpr GhcPs
lambda ((OccName -> Pat') -> [OccName] -> [Pat']
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap OccName -> Pat'
forall a. BVar a => OccName -> a
bvar' [OccName]
bound_occs) (HsExpr GhcPs -> HsExpr GhcPs)
-> (LHsExpr GhcPs -> HsExpr GhcPs) -> LHsExpr GhcPs -> HsExpr GhcPs
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LHsExpr GhcPs -> HsExpr GhcPs
forall a. HasSrcSpan a => a -> SrcSpanLess a
unLoc
introAndDestruct :: TacticsM ()
introAndDestruct :: TacticsM ()
introAndDestruct = do
[HyInfo CType]
hy <- (Hypothesis CType -> [HyInfo CType])
-> TacticT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Hypothesis CType)
-> TacticT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
[HyInfo CType]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Hypothesis CType -> [HyInfo CType]
forall a. Hypothesis a -> [HyInfo a]
unHypothesis (TacticT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Hypothesis CType)
-> TacticT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
[HyInfo CType])
-> TacticT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Hypothesis CType)
-> TacticT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
[HyInfo CType]
forall a b. (a -> b) -> a -> b
$ TacticsM ()
-> TacticT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Hypothesis CType)
hyDiff (TacticsM ()
-> TacticT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Hypothesis CType))
-> TacticsM ()
-> TacticT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Hypothesis CType)
forall a b. (a -> b) -> a -> b
$ IntroParams -> TacticsM ()
intros' (IntroParams -> TacticsM ()) -> IntroParams -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ Int -> IntroParams
IntroduceOnlyUnnamed Int
1
Bool -> TacticsM () -> TacticsM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([HyInfo CType] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [HyInfo CType]
hy Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1) (TacticsM () -> TacticsM ()) -> TacticsM () -> TacticsM ()
forall a b. (a -> b) -> a -> b
$
String -> [HyInfo CType] -> TacticsM ()
forall (m :: * -> *) a. (Monad m, Show a) => String -> a -> m ()
traceMX String
"BUG: Introduced too many variables for introAndDestruct! Please report me if you see this! " [HyInfo CType]
hy
[HyInfo CType] -> (HyInfo CType -> TacticsM ()) -> TacticsM ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
t a -> (a -> f b) -> f ()
for_ [HyInfo CType]
hy HyInfo CType -> TacticsM ()
destruct
destructAuto :: HyInfo CType -> TacticsM ()
destructAuto :: HyInfo CType -> TacticsM ()
destructAuto HyInfo CType
hi = TacticsM () -> TacticsM ()
forall a. TacticsM a -> TacticsM a
requireConcreteHole (TacticsM () -> TacticsM ()) -> TacticsM () -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ String -> TacticsM () -> TacticsM ()
forall (m :: * -> *) jdg ext err s a.
Functor m =>
String
-> TacticT jdg (Synthesized ext) err s m a
-> TacticT jdg (Synthesized ext) err s m a
tracing String
"destruct(auto)" (TacticsM () -> TacticsM ()) -> TacticsM () -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ 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
let subtactic :: TacticsM ()
subtactic = HyInfo CType -> TacticsM ()
destructOrHomoAuto HyInfo CType
hi
case Provenance -> Bool
isPatternMatch (Provenance -> Bool) -> Provenance -> Bool
forall a b. (a -> b) -> a -> b
$ HyInfo CType -> Provenance
forall a. HyInfo a -> Provenance
hi_provenance HyInfo CType
hi of
Bool
True ->
TacticsM () -> ([Judgement] -> Maybe TacticError) -> TacticsM ()
forall meta ext err s (m :: * -> *) jdg.
(MetaSubst meta ext, MonadExtract meta ext err s m) =>
TacticT jdg ext err s m ()
-> ([jdg] -> Maybe err) -> TacticT jdg ext err s m ()
pruning TacticsM ()
subtactic (([Judgement] -> Maybe TacticError) -> TacticsM ())
-> ([Judgement] -> Maybe TacticError) -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ \[Judgement]
jdgs ->
let getHyTypes :: Judgement -> Set CType
getHyTypes = [CType] -> Set CType
forall a. Ord a => [a] -> Set a
S.fromList ([CType] -> Set CType)
-> (Judgement -> [CType]) -> Judgement -> Set CType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (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])
-> (Judgement -> [HyInfo CType]) -> Judgement -> [CType]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Hypothesis CType -> [HyInfo CType]
forall a. Hypothesis a -> [HyInfo a]
unHypothesis (Hypothesis CType -> [HyInfo CType])
-> (Judgement -> Hypothesis CType) -> Judgement -> [HyInfo CType]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Judgement -> Hypothesis CType
forall a. Judgement' a -> Hypothesis a
jHypothesis
new_hy :: Set CType
new_hy = (Judgement -> Set CType) -> [Judgement] -> Set CType
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Judgement -> Set CType
getHyTypes [Judgement]
jdgs
old_hy :: Set CType
old_hy = Judgement -> Set CType
getHyTypes Judgement
jdg
in case Set CType -> Bool
forall a. Set a -> Bool
S.null (Set CType -> Bool) -> Set CType -> Bool
forall a b. (a -> b) -> a -> b
$ Set CType
new_hy Set CType -> Set CType -> Set CType
forall a. Ord a => Set a -> Set a -> Set a
S.\\ Set CType
old_hy of
Bool
True -> TacticError -> Maybe TacticError
forall a. a -> Maybe a
Just (TacticError -> Maybe TacticError)
-> TacticError -> Maybe TacticError
forall a b. (a -> b) -> a -> b
$ OccName -> TacticError
UnhelpfulDestruct (OccName -> TacticError) -> OccName -> TacticError
forall a b. (a -> b) -> a -> b
$ HyInfo CType -> OccName
forall a. HyInfo a -> OccName
hi_name HyInfo CType
hi
Bool
False -> Maybe TacticError
forall a. Maybe a
Nothing
Bool
False -> TacticsM ()
subtactic
destructOrHomoAuto :: HyInfo CType -> TacticsM ()
destructOrHomoAuto :: HyInfo CType -> TacticsM ()
destructOrHomoAuto HyInfo CType
hi = String -> TacticsM () -> TacticsM ()
forall (m :: * -> *) jdg ext err s a.
Functor m =>
String
-> TacticT jdg (Synthesized ext) err s m a
-> TacticT jdg (Synthesized ext) err s m a
tracing String
"destructOrHomoAuto" (TacticsM () -> TacticsM ()) -> TacticsM () -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ 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
let g :: Type
g = CType -> Type
unCType (CType -> Type) -> CType -> Type
forall a b. (a -> b) -> a -> b
$ Judgement -> CType
forall a. Judgement' a -> a
jGoal Judgement
jdg
ty :: Type
ty = CType -> Type
unCType (CType -> Type) -> CType -> Type
forall a b. (a -> b) -> a -> b
$ HyInfo CType -> CType
forall a. HyInfo a -> a
hi_type HyInfo CType
hi
TacticsM () -> TacticsM () -> Bool -> TacticsM ()
forall a. TacticsM a -> TacticsM a -> Bool -> TacticsM a
attemptWhen
((Judgement
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized (LHsExpr GhcPs)))
-> 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
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized (LHsExpr GhcPs)))
-> TacticsM ())
-> (Judgement
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized (LHsExpr GhcPs)))
-> TacticsM ()
forall a b. (a -> b) -> a -> b
$ Bool
-> (ConLike
-> Judgement
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized (LHsExpr GhcPs)))
-> HyInfo CType
-> Judgement
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized (LHsExpr GhcPs))
destruct' Bool
False (\ConLike
dc Judgement
jdg ->
Bool
-> Judgement
-> ConLike
-> ThetaType
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized (LHsExpr GhcPs))
buildDataCon Bool
False Judgement
jdg ConLike
dc (ThetaType
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized (LHsExpr GhcPs)))
-> ThetaType
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized (LHsExpr GhcPs))
forall a b. (a -> b) -> a -> b
$ (Type, ThetaType) -> ThetaType
forall a b. (a, b) -> b
snd ((Type, ThetaType) -> ThetaType) -> (Type, ThetaType) -> ThetaType
forall a b. (a -> b) -> a -> b
$ Type -> (Type, ThetaType)
splitAppTys Type
g) HyInfo CType
hi)
((Judgement
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized (LHsExpr GhcPs)))
-> 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
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized (LHsExpr GhcPs)))
-> TacticsM ())
-> (Judgement
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized (LHsExpr GhcPs)))
-> TacticsM ()
forall a b. (a -> b) -> a -> b
$ Bool
-> (ConLike
-> Judgement
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized (LHsExpr GhcPs)))
-> HyInfo CType
-> Judgement
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized (LHsExpr GhcPs))
destruct' Bool
False ((Judgement
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized (LHsExpr GhcPs)))
-> ConLike
-> Judgement
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized (LHsExpr GhcPs))
forall a b. a -> b -> a
const Judgement
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized (LHsExpr GhcPs))
newSubgoal) HyInfo CType
hi)
(Bool -> TacticsM ()) -> Bool -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ case (HasDebugCallStack => Type -> Maybe (TyCon, ThetaType)
Type -> Maybe (TyCon, ThetaType)
splitTyConApp_maybe Type
g, HasDebugCallStack => Type -> Maybe (TyCon, ThetaType)
Type -> Maybe (TyCon, ThetaType)
splitTyConApp_maybe Type
ty) of
(Just (TyCon
gtc, ThetaType
_), Just (TyCon
tytc, ThetaType
_)) -> TyCon
gtc TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
tytc
(Maybe (TyCon, ThetaType), Maybe (TyCon, ThetaType))
_ -> Bool
False
destruct :: HyInfo CType -> TacticsM ()
destruct :: HyInfo CType -> TacticsM ()
destruct HyInfo CType
hi = TacticsM () -> TacticsM ()
forall a. TacticsM a -> TacticsM a
requireConcreteHole (TacticsM () -> TacticsM ()) -> TacticsM () -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ String -> TacticsM () -> TacticsM ()
forall (m :: * -> *) jdg ext err s a.
Functor m =>
String
-> TacticT jdg (Synthesized ext) err s m a
-> TacticT jdg (Synthesized ext) err s m a
tracing String
"destruct(user)" (TacticsM () -> TacticsM ()) -> TacticsM () -> TacticsM ()
forall a b. (a -> b) -> a -> b
$
(Judgement
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized (LHsExpr GhcPs)))
-> 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
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized (LHsExpr GhcPs)))
-> TacticsM ())
-> (Judgement
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized (LHsExpr GhcPs)))
-> TacticsM ()
forall a b. (a -> b) -> a -> b
$ Bool
-> (ConLike
-> Judgement
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized (LHsExpr GhcPs)))
-> HyInfo CType
-> Judgement
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized (LHsExpr GhcPs))
destruct' Bool
False ((Judgement
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized (LHsExpr GhcPs)))
-> ConLike
-> Judgement
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized (LHsExpr GhcPs))
forall a b. a -> b -> a
const Judgement
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized (LHsExpr GhcPs))
newSubgoal) HyInfo CType
hi
destructPun :: HyInfo CType -> TacticsM ()
destructPun :: HyInfo CType -> TacticsM ()
destructPun HyInfo CType
hi = TacticsM () -> TacticsM ()
forall a. TacticsM a -> TacticsM a
requireConcreteHole (TacticsM () -> TacticsM ()) -> TacticsM () -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ String -> TacticsM () -> TacticsM ()
forall (m :: * -> *) jdg ext err s a.
Functor m =>
String
-> TacticT jdg (Synthesized ext) err s m a
-> TacticT jdg (Synthesized ext) err s m a
tracing String
"destructPun(user)" (TacticsM () -> TacticsM ()) -> TacticsM () -> TacticsM ()
forall a b. (a -> b) -> a -> b
$
(Judgement
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized (LHsExpr GhcPs)))
-> 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
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized (LHsExpr GhcPs)))
-> TacticsM ())
-> (Judgement
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized (LHsExpr GhcPs)))
-> TacticsM ()
forall a b. (a -> b) -> a -> b
$ Bool
-> (ConLike
-> Judgement
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized (LHsExpr GhcPs)))
-> HyInfo CType
-> Judgement
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized (LHsExpr GhcPs))
destruct' Bool
True ((Judgement
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized (LHsExpr GhcPs)))
-> ConLike
-> Judgement
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized (LHsExpr GhcPs))
forall a b. a -> b -> a
const Judgement
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized (LHsExpr GhcPs))
newSubgoal) HyInfo CType
hi
homo :: HyInfo CType -> TacticsM ()
homo :: HyInfo CType -> TacticsM ()
homo HyInfo CType
hi = TacticsM () -> TacticsM ()
forall a. TacticsM a -> TacticsM a
requireConcreteHole (TacticsM () -> TacticsM ())
-> (TacticsM () -> TacticsM ()) -> TacticsM () -> TacticsM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> TacticsM () -> TacticsM ()
forall (m :: * -> *) jdg ext err s a.
Functor m =>
String
-> TacticT jdg (Synthesized ext) err s m a
-> TacticT jdg (Synthesized ext) err s m a
tracing String
"homo" (TacticsM () -> TacticsM ()) -> TacticsM () -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ 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
let g :: CType
g = Judgement -> CType
forall a. Judgement' a -> a
jGoal Judgement
jdg
case (Type -> Type -> Maybe (Set (Uniquely DataCon))
uncoveredDataCons (CType -> Type
coerce (CType -> Type) -> CType -> Type
forall a b. (a -> b) -> a -> b
$ HyInfo CType -> CType
forall a. HyInfo a -> a
hi_type HyInfo CType
hi) (CType -> Type
coerce CType
g)) of
Just Set (Uniquely DataCon)
uncovered_dcs ->
Bool -> TacticsM () -> TacticsM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Set (Uniquely DataCon) -> Bool
forall a. Set a -> Bool
S.null Set (Uniquely DataCon)
uncovered_dcs) (TacticsM () -> TacticsM ()) -> TacticsM () -> TacticsM ()
forall a b. (a -> b) -> a -> b
$
TacticError -> TacticsM ()
forall err jdg ext s (m :: * -> *) a.
err -> TacticT jdg ext err s m a
failure (TacticError -> TacticsM ()) -> TacticError -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ String -> TacticError
TacticPanic String
"Can't cover every datacon in domain"
Maybe (Set (Uniquely DataCon))
_ -> TacticError -> TacticsM ()
forall err jdg ext s (m :: * -> *) a.
err -> TacticT jdg ext err s m a
failure (TacticError -> TacticsM ()) -> TacticError -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ String -> TacticError
TacticPanic String
"Unable to fetch datacons"
(Judgement
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized (LHsExpr GhcPs)))
-> 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
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized (LHsExpr GhcPs)))
-> TacticsM ())
-> (Judgement
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized (LHsExpr GhcPs)))
-> TacticsM ()
forall a b. (a -> b) -> a -> b
$ Bool
-> (ConLike
-> Judgement
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized (LHsExpr GhcPs)))
-> HyInfo CType
-> Judgement
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized (LHsExpr GhcPs))
destruct'
Bool
False
(\ConLike
dc Judgement
jdg -> Bool
-> Judgement
-> ConLike
-> ThetaType
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized (LHsExpr GhcPs))
buildDataCon Bool
False Judgement
jdg ConLike
dc (ThetaType
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized (LHsExpr GhcPs)))
-> ThetaType
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized (LHsExpr GhcPs))
forall a b. (a -> b) -> a -> b
$ (Type, ThetaType) -> ThetaType
forall a b. (a, b) -> b
snd ((Type, ThetaType) -> ThetaType) -> (Type, ThetaType) -> ThetaType
forall a b. (a -> b) -> a -> b
$ Type -> (Type, ThetaType)
splitAppTys (Type -> (Type, ThetaType)) -> Type -> (Type, ThetaType)
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)
(HyInfo CType
-> Judgement
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized (LHsExpr GhcPs)))
-> HyInfo CType
-> Judgement
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized (LHsExpr GhcPs))
forall a b. (a -> b) -> a -> b
$ HyInfo CType
hi
destructLambdaCase :: TacticsM ()
destructLambdaCase :: TacticsM ()
destructLambdaCase =
String -> TacticsM () -> TacticsM ()
forall (m :: * -> *) jdg ext err s a.
Functor m =>
String
-> TacticT jdg (Synthesized ext) err s m a
-> TacticT jdg (Synthesized ext) err s m a
tracing String
"destructLambdaCase" (TacticsM () -> TacticsM ()) -> TacticsM () -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ (Judgement
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized (LHsExpr GhcPs)))
-> 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
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized (LHsExpr GhcPs)))
-> TacticsM ())
-> (Judgement
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized (LHsExpr GhcPs)))
-> TacticsM ()
forall a b. (a -> b) -> a -> b
$ Bool
-> (ConLike
-> Judgement
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized (LHsExpr GhcPs)))
-> Judgement
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized (LHsExpr GhcPs))
destructLambdaCase' Bool
False ((Judgement
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized (LHsExpr GhcPs)))
-> ConLike
-> Judgement
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized (LHsExpr GhcPs))
forall a b. a -> b -> a
const Judgement
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized (LHsExpr GhcPs))
newSubgoal)
homoLambdaCase :: TacticsM ()
homoLambdaCase :: TacticsM ()
homoLambdaCase =
String -> TacticsM () -> TacticsM ()
forall (m :: * -> *) jdg ext err s a.
Functor m =>
String
-> TacticT jdg (Synthesized ext) err s m a
-> TacticT jdg (Synthesized ext) err s m a
tracing String
"homoLambdaCase" (TacticsM () -> TacticsM ()) -> TacticsM () -> TacticsM ()
forall a b. (a -> b) -> a -> b
$
(Judgement
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized (LHsExpr GhcPs)))
-> 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
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized (LHsExpr GhcPs)))
-> TacticsM ())
-> (Judgement
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized (LHsExpr GhcPs)))
-> TacticsM ()
forall a b. (a -> b) -> a -> b
$ Bool
-> (ConLike
-> Judgement
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized (LHsExpr GhcPs)))
-> Judgement
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized (LHsExpr GhcPs))
destructLambdaCase' Bool
False ((ConLike
-> Judgement
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized (LHsExpr GhcPs)))
-> Judgement
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized (LHsExpr GhcPs)))
-> (ConLike
-> Judgement
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized (LHsExpr GhcPs)))
-> Judgement
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized (LHsExpr GhcPs))
forall a b. (a -> b) -> a -> b
$ \ConLike
dc Judgement
jdg ->
Bool
-> Judgement
-> ConLike
-> ThetaType
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized (LHsExpr GhcPs))
buildDataCon Bool
False Judgement
jdg ConLike
dc
(ThetaType
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized (LHsExpr GhcPs)))
-> (CType -> ThetaType)
-> CType
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized (LHsExpr GhcPs))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Type, ThetaType) -> ThetaType
forall a b. (a, b) -> b
snd
((Type, ThetaType) -> ThetaType)
-> (CType -> (Type, ThetaType)) -> CType -> ThetaType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> (Type, ThetaType)
splitAppTys
(Type -> (Type, ThetaType))
-> (CType -> Type) -> CType -> (Type, ThetaType)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CType -> Type
unCType
(CType
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized (LHsExpr GhcPs)))
-> CType
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized (LHsExpr GhcPs))
forall a b. (a -> b) -> a -> b
$ Judgement -> CType
forall a. Judgement' a -> a
jGoal Judgement
jdg
data Saturation = Unsaturated Int
deriving (Saturation -> Saturation -> Bool
(Saturation -> Saturation -> Bool)
-> (Saturation -> Saturation -> Bool) -> Eq Saturation
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Saturation -> Saturation -> Bool
$c/= :: Saturation -> Saturation -> Bool
== :: Saturation -> Saturation -> Bool
$c== :: Saturation -> Saturation -> Bool
Eq, Eq Saturation
Eq Saturation
-> (Saturation -> Saturation -> Ordering)
-> (Saturation -> Saturation -> Bool)
-> (Saturation -> Saturation -> Bool)
-> (Saturation -> Saturation -> Bool)
-> (Saturation -> Saturation -> Bool)
-> (Saturation -> Saturation -> Saturation)
-> (Saturation -> Saturation -> Saturation)
-> Ord Saturation
Saturation -> Saturation -> Bool
Saturation -> Saturation -> Ordering
Saturation -> Saturation -> Saturation
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
min :: Saturation -> Saturation -> Saturation
$cmin :: Saturation -> Saturation -> Saturation
max :: Saturation -> Saturation -> Saturation
$cmax :: Saturation -> Saturation -> Saturation
>= :: Saturation -> Saturation -> Bool
$c>= :: Saturation -> Saturation -> Bool
> :: Saturation -> Saturation -> Bool
$c> :: Saturation -> Saturation -> Bool
<= :: Saturation -> Saturation -> Bool
$c<= :: Saturation -> Saturation -> Bool
< :: Saturation -> Saturation -> Bool
$c< :: Saturation -> Saturation -> Bool
compare :: Saturation -> Saturation -> Ordering
$ccompare :: Saturation -> Saturation -> Ordering
$cp1Ord :: Eq Saturation
Ord, Int -> Saturation -> String -> String
[Saturation] -> String -> String
Saturation -> String
(Int -> Saturation -> String -> String)
-> (Saturation -> String)
-> ([Saturation] -> String -> String)
-> Show Saturation
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
showList :: [Saturation] -> String -> String
$cshowList :: [Saturation] -> String -> String
show :: Saturation -> String
$cshow :: Saturation -> String
showsPrec :: Int -> Saturation -> String -> String
$cshowsPrec :: Int -> Saturation -> String -> String
Show)
pattern Saturated :: Saturation
pattern $bSaturated :: Saturation
$mSaturated :: forall r. Saturation -> (Void# -> r) -> (Void# -> r) -> r
Saturated = Unsaturated 0
apply :: Saturation -> HyInfo CType -> TacticsM ()
apply :: Saturation -> HyInfo CType -> TacticsM ()
apply (Unsaturated Int
n) HyInfo CType
hi = String -> TacticsM () -> TacticsM ()
forall (m :: * -> *) jdg ext err s a.
Functor m =>
String
-> TacticT jdg (Synthesized ext) err s m a
-> TacticT jdg (Synthesized ext) err s m a
tracing (String
"apply' " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> OccName -> String
forall a. Show a => a -> String
show (HyInfo CType -> OccName
forall a. HyInfo a -> OccName
hi_name HyInfo CType
hi)) (TacticsM () -> TacticsM ()) -> TacticsM () -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ 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
let g :: CType
g = Judgement -> CType
forall a. Judgement' a -> a
jGoal Judgement
jdg
ty :: Type
ty = CType -> Type
unCType (CType -> Type) -> CType -> Type
forall a b. (a -> b) -> a -> b
$ HyInfo CType -> CType
forall a. HyInfo a -> a
hi_type HyInfo CType
hi
func :: OccName
func = HyInfo CType -> OccName
forall a. HyInfo a -> OccName
hi_name HyInfo CType
hi
Type
ty' <- Type
-> TacticT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
Type
forall (m :: * -> *). MonadState TacticState m => Type -> m Type
freshTyvars Type
ty
let ([TyVar]
_, ThetaType
_, ThetaType
all_args, Type
ret) = Type -> ([TyVar], ThetaType, ThetaType, Type)
tacticsSplitFunTy Type
ty'
saturated_args :: ThetaType
saturated_args = Int -> ThetaType -> ThetaType
forall a. Int -> [a] -> [a]
dropEnd Int
n ThetaType
all_args
unsaturated_args :: ThetaType
unsaturated_args = Int -> ThetaType -> ThetaType
forall a. Int -> [a] -> [a]
takeEnd Int
n ThetaType
all_args
(Judgement
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized (LHsExpr GhcPs)))
-> 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
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized (LHsExpr GhcPs)))
-> TacticsM ())
-> (Judgement
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized (LHsExpr GhcPs)))
-> TacticsM ()
forall a b. (a -> b) -> a -> b
$ \Judgement
jdg -> do
CType -> CType -> RuleM ()
unify CType
g (Type -> CType
CType (Type -> CType) -> Type -> CType
forall a b. (a -> b) -> a -> b
$ ThetaType -> Type -> Type
mkFunTys' ThetaType
unsaturated_args Type
ret)
Synthesized [LHsExpr GhcPs]
ext
<- ([Synthesized (LHsExpr GhcPs)] -> Synthesized [LHsExpr GhcPs])
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
[Synthesized (LHsExpr GhcPs)]
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized [LHsExpr GhcPs])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [Synthesized (LHsExpr GhcPs)] -> Synthesized [LHsExpr GhcPs]
forall a. [Synthesized a] -> Synthesized [a]
unzipTrace
(RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
[Synthesized (LHsExpr GhcPs)]
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized [LHsExpr GhcPs]))
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
[Synthesized (LHsExpr GhcPs)]
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized [LHsExpr GhcPs])
forall a b. (a -> b) -> a -> b
$ (Type
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized (LHsExpr GhcPs)))
-> ThetaType
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
[Synthesized (LHsExpr GhcPs)]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse ( Judgement
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized (LHsExpr GhcPs))
newSubgoal
(Judgement
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized (LHsExpr GhcPs)))
-> (Type -> Judgement)
-> Type
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized (LHsExpr GhcPs))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Judgement -> Judgement
blacklistingDestruct
(Judgement -> Judgement)
-> (Type -> Judgement) -> Type -> Judgement
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (CType -> Judgement -> Judgement)
-> Judgement -> CType -> Judgement
forall a b c. (a -> b -> c) -> b -> a -> c
flip CType -> Judgement -> Judgement
forall a. a -> Judgement' a -> Judgement' a
withNewGoal Judgement
jdg
(CType -> Judgement) -> (Type -> CType) -> Type -> Judgement
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> CType
CType
) ThetaType
saturated_args
Synthesized (LHsExpr GhcPs)
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized (LHsExpr GhcPs))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Synthesized (LHsExpr GhcPs)
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized (LHsExpr GhcPs)))
-> Synthesized (LHsExpr GhcPs)
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized (LHsExpr GhcPs))
forall a b. (a -> b) -> a -> b
$
Synthesized [LHsExpr GhcPs]
ext
Synthesized [LHsExpr GhcPs]
-> (Synthesized [LHsExpr GhcPs] -> Synthesized [LHsExpr GhcPs])
-> Synthesized [LHsExpr GhcPs]
forall a b. a -> (a -> b) -> b
& IsLabel
"syn_used_vals"
(ASetter
(Synthesized [LHsExpr GhcPs])
(Synthesized [LHsExpr GhcPs])
(Set OccName)
(Set OccName))
ASetter
(Synthesized [LHsExpr GhcPs])
(Synthesized [LHsExpr GhcPs])
(Set OccName)
(Set OccName)
#syn_used_vals ASetter
(Synthesized [LHsExpr GhcPs])
(Synthesized [LHsExpr GhcPs])
(Set OccName)
(Set OccName)
-> (Set OccName -> Set OccName)
-> Synthesized [LHsExpr GhcPs]
-> Synthesized [LHsExpr GhcPs]
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ (\Set OccName
x -> OccName -> Set OccName -> Set OccName
forall a. Ord a => a -> Set a -> Set a
S.insert OccName
func Set OccName
x Set OccName -> Set OccName -> Set OccName
forall a. Semigroup a => a -> a -> a
<> Judgement -> OccName -> Set OccName
forall a. Judgement' a -> OccName -> Set OccName
getAncestry Judgement
jdg OccName
func)
Synthesized [LHsExpr GhcPs]
-> (Synthesized [LHsExpr GhcPs] -> Synthesized (LHsExpr GhcPs))
-> Synthesized (LHsExpr GhcPs)
forall a b. a -> (a -> b) -> b
& IsLabel
"syn_val"
(ASetter
(Synthesized [LHsExpr GhcPs])
(Synthesized (LHsExpr GhcPs))
[LHsExpr GhcPs]
(LHsExpr GhcPs))
ASetter
(Synthesized [LHsExpr GhcPs])
(Synthesized (LHsExpr GhcPs))
[LHsExpr GhcPs]
(LHsExpr GhcPs)
#syn_val ASetter
(Synthesized [LHsExpr GhcPs])
(Synthesized (LHsExpr GhcPs))
[LHsExpr GhcPs]
(LHsExpr GhcPs)
-> ([LHsExpr GhcPs] -> LHsExpr GhcPs)
-> Synthesized [LHsExpr GhcPs]
-> Synthesized (LHsExpr GhcPs)
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ OccName -> [HsExpr GhcPs] -> LHsExpr GhcPs
mkApply OccName
func ([HsExpr GhcPs] -> LHsExpr GhcPs)
-> ([LHsExpr GhcPs] -> [HsExpr GhcPs])
-> [LHsExpr GhcPs]
-> LHsExpr GhcPs
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (LHsExpr GhcPs -> HsExpr GhcPs)
-> [LHsExpr GhcPs] -> [HsExpr GhcPs]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap LHsExpr GhcPs -> HsExpr GhcPs
forall a. HasSrcSpan a => a -> SrcSpanLess a
unLoc
application :: TacticsM ()
application :: TacticsM ()
application = (HyInfo CType -> TacticsM ()) -> TacticsM ()
overFunctions ((HyInfo CType -> TacticsM ()) -> TacticsM ())
-> (HyInfo CType -> TacticsM ()) -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ Saturation -> HyInfo CType -> TacticsM ()
apply Saturation
Saturated
split :: TacticsM ()
split :: TacticsM ()
split = String -> TacticsM () -> TacticsM ()
forall (m :: * -> *) jdg ext err s a.
Functor m =>
String
-> TacticT jdg (Synthesized ext) err s m a
-> TacticT jdg (Synthesized ext) err s m a
tracing String
"split(user)" (TacticsM () -> TacticsM ()) -> TacticsM () -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ 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
let g :: CType
g = Judgement -> CType
forall a. Judgement' a -> a
jGoal Judgement
jdg
case Type -> Maybe ([DataCon], ThetaType)
tacticsGetDataCons (Type -> Maybe ([DataCon], ThetaType))
-> Type -> Maybe ([DataCon], ThetaType)
forall a b. (a -> b) -> a -> b
$ CType -> Type
unCType CType
g of
Maybe ([DataCon], ThetaType)
Nothing -> TacticError -> TacticsM ()
forall err jdg ext s (m :: * -> *) a.
err -> TacticT jdg ext err s m a
failure (TacticError -> TacticsM ()) -> TacticError -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ String -> CType -> TacticError
GoalMismatch String
"split" CType
g
Just ([DataCon]
dcs, ThetaType
_) -> [TacticsM ()] -> TacticsM ()
forall (m :: * -> *) jdg ext err s a.
Monad m =>
[TacticT jdg ext err s m a] -> TacticT jdg ext err s m a
choice ([TacticsM ()] -> TacticsM ()) -> [TacticsM ()] -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ (DataCon -> TacticsM ()) -> [DataCon] -> [TacticsM ()]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap DataCon -> TacticsM ()
splitDataCon [DataCon]
dcs
splitAuto :: TacticsM ()
splitAuto :: TacticsM ()
splitAuto = TacticsM () -> TacticsM ()
forall a. TacticsM a -> TacticsM a
requireConcreteHole (TacticsM () -> TacticsM ()) -> TacticsM () -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ String -> TacticsM () -> TacticsM ()
forall (m :: * -> *) jdg ext err s a.
Functor m =>
String
-> TacticT jdg (Synthesized ext) err s m a
-> TacticT jdg (Synthesized ext) err s m a
tracing String
"split(auto)" (TacticsM () -> TacticsM ()) -> TacticsM () -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ 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
let g :: CType
g = Judgement -> CType
forall a. Judgement' a -> a
jGoal Judgement
jdg
case Type -> Maybe ([DataCon], ThetaType)
tacticsGetDataCons (Type -> Maybe ([DataCon], ThetaType))
-> Type -> Maybe ([DataCon], ThetaType)
forall a b. (a -> b) -> a -> b
$ CType -> Type
unCType CType
g of
Maybe ([DataCon], ThetaType)
Nothing -> TacticError -> TacticsM ()
forall err jdg ext s (m :: * -> *) a.
err -> TacticT jdg ext err s m a
failure (TacticError -> TacticsM ()) -> TacticError -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ String -> CType -> TacticError
GoalMismatch String
"split" CType
g
Just ([DataCon]
dcs, ThetaType
_) -> do
case Judgement -> Bool
isSplitWhitelisted Judgement
jdg of
Bool
True -> [TacticsM ()] -> TacticsM ()
forall (m :: * -> *) jdg ext err s a.
Monad m =>
[TacticT jdg ext err s m a] -> TacticT jdg ext err s m a
choice ([TacticsM ()] -> TacticsM ()) -> [TacticsM ()] -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ (DataCon -> TacticsM ()) -> [DataCon] -> [TacticsM ()]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap DataCon -> TacticsM ()
splitDataCon [DataCon]
dcs
Bool
False -> do
[TacticsM ()] -> TacticsM ()
forall (m :: * -> *) jdg ext err s a.
Monad m =>
[TacticT jdg ext err s m a] -> TacticT jdg ext err s m a
choice ([TacticsM ()] -> TacticsM ()) -> [TacticsM ()] -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ ((DataCon -> TacticsM ()) -> [DataCon] -> [TacticsM ()])
-> [DataCon] -> (DataCon -> TacticsM ()) -> [TacticsM ()]
forall a b c. (a -> b -> c) -> b -> a -> c
flip (DataCon -> TacticsM ()) -> [DataCon] -> [TacticsM ()]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [DataCon]
dcs ((DataCon -> TacticsM ()) -> [TacticsM ()])
-> (DataCon -> TacticsM ()) -> [TacticsM ()]
forall a b. (a -> b) -> a -> b
$ \DataCon
dc -> TacticsM () -> TacticsM ()
requireNewHoles (TacticsM () -> TacticsM ()) -> TacticsM () -> TacticsM ()
forall a b. (a -> b) -> a -> b
$
DataCon -> TacticsM ()
splitDataCon DataCon
dc
splitSingle :: TacticsM ()
splitSingle :: TacticsM ()
splitSingle = String -> TacticsM () -> TacticsM ()
forall (m :: * -> *) jdg ext err s a.
Functor m =>
String
-> TacticT jdg (Synthesized ext) err s m a
-> TacticT jdg (Synthesized ext) err s m a
tracing String
"splitSingle" (TacticsM () -> TacticsM ()) -> TacticsM () -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ 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
let g :: CType
g = Judgement -> CType
forall a. Judgement' a -> a
jGoal Judgement
jdg
case Type -> Maybe ([DataCon], ThetaType)
tacticsGetDataCons (Type -> Maybe ([DataCon], ThetaType))
-> Type -> Maybe ([DataCon], ThetaType)
forall a b. (a -> b) -> a -> b
$ CType -> Type
unCType CType
g of
Just ([DataCon
dc], ThetaType
_) -> do
DataCon -> TacticsM ()
splitDataCon DataCon
dc
Maybe ([DataCon], ThetaType)
_ -> TacticError -> TacticsM ()
forall err jdg ext s (m :: * -> *) a.
err -> TacticT jdg ext err s m a
failure (TacticError -> TacticsM ()) -> TacticError -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ String -> CType -> TacticError
GoalMismatch String
"splitSingle" CType
g
obvious :: TacticsM ()
obvious :: TacticsM ()
obvious = String -> TacticsM () -> TacticsM ()
forall (m :: * -> *) jdg ext err s a.
Functor m =>
String
-> TacticT jdg (Synthesized ext) err s m a
-> TacticT jdg (Synthesized ext) err s m a
tracing String
"obvious" (TacticsM () -> TacticsM ()) -> TacticsM () -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ do
TacticsM () -> ([Judgement] -> Maybe TacticError) -> TacticsM ()
forall meta ext err s (m :: * -> *) jdg.
(MetaSubst meta ext, MonadExtract meta ext err s m) =>
TacticT jdg ext err s m ()
-> ([jdg] -> Maybe err) -> TacticT jdg ext err s m ()
pruning TacticsM ()
split (([Judgement] -> Maybe TacticError) -> TacticsM ())
-> ([Judgement] -> Maybe TacticError) -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ Maybe TacticError -> Maybe TacticError -> Bool -> Maybe TacticError
forall a. a -> a -> Bool -> a
bool (TacticError -> Maybe TacticError
forall a. a -> Maybe a
Just TacticError
NoProgress) Maybe TacticError
forall a. Maybe a
Nothing (Bool -> Maybe TacticError)
-> ([Judgement] -> Bool) -> [Judgement] -> Maybe TacticError
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Judgement] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null
sorry :: TacticsM ()
sorry :: TacticsM ()
sorry = HsExpr GhcPs -> TacticsM ()
exact (HsExpr GhcPs -> TacticsM ()) -> HsExpr GhcPs -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ OccName -> HsExpr GhcPs
forall a. Var a => OccName -> a
var' (OccName -> HsExpr GhcPs) -> OccName -> HsExpr GhcPs
forall a b. (a -> b) -> a -> b
$ String -> OccName
mkVarOcc String
"_"
metaprogram :: TacticsM ()
metaprogram :: TacticsM ()
metaprogram = HsExpr GhcPs -> TacticsM ()
exact (HsExpr GhcPs -> TacticsM ()) -> HsExpr GhcPs -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ FastString -> HsExpr GhcPs
MetaprogramSyntax FastString
""
requireNewHoles :: TacticsM () -> TacticsM ()
requireNewHoles :: TacticsM () -> TacticsM ()
requireNewHoles TacticsM ()
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
TacticsM () -> ([Judgement] -> Maybe TacticError) -> TacticsM ()
forall meta ext err s (m :: * -> *) jdg.
(MetaSubst meta ext, MonadExtract meta ext err s m) =>
TacticT jdg ext err s m ()
-> ([jdg] -> Maybe err) -> TacticT jdg ext err s m ()
pruning TacticsM ()
m (([Judgement] -> Maybe TacticError) -> TacticsM ())
-> ([Judgement] -> Maybe TacticError) -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ \[Judgement]
jdgs ->
case [Judgement] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Judgement]
jdgs Bool -> Bool -> Bool
|| (CType -> Bool) -> [CType] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (CType -> CType -> Bool
forall a. Eq a => a -> a -> Bool
/= Judgement -> CType
forall a. Judgement' a -> a
jGoal Judgement
jdg) ((Judgement -> CType) -> [Judgement] -> [CType]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Judgement -> CType
forall a. Judgement' a -> a
jGoal [Judgement]
jdgs) of
Bool
True -> Maybe TacticError
forall a. Maybe a
Nothing
Bool
False -> TacticError -> Maybe TacticError
forall a. a -> Maybe a
Just TacticError
NoProgress
splitConLike :: ConLike -> TacticsM ()
splitConLike :: ConLike -> TacticsM ()
splitConLike ConLike
dc =
TacticsM () -> TacticsM ()
forall a. TacticsM a -> TacticsM a
requireConcreteHole (TacticsM () -> TacticsM ()) -> TacticsM () -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ String -> TacticsM () -> TacticsM ()
forall (m :: * -> *) jdg ext err s a.
Functor m =>
String
-> TacticT jdg (Synthesized ext) err s m a
-> TacticT jdg (Synthesized ext) err s m a
tracing (String
"splitDataCon:" String -> String -> String
forall a. Semigroup a => a -> a -> a
<> ConLike -> String
forall a. Show a => a -> String
show ConLike
dc) (TacticsM () -> TacticsM ()) -> TacticsM () -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ (Judgement
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized (LHsExpr GhcPs)))
-> 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
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized (LHsExpr GhcPs)))
-> TacticsM ())
-> (Judgement
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized (LHsExpr GhcPs)))
-> TacticsM ()
forall a b. (a -> b) -> a -> b
$ \Judgement
jdg -> do
let g :: CType
g = Judgement -> CType
forall a. Judgement' a -> a
jGoal Judgement
jdg
case HasDebugCallStack => Type -> Maybe (TyCon, ThetaType)
Type -> Maybe (TyCon, ThetaType)
splitTyConApp_maybe (Type -> Maybe (TyCon, ThetaType))
-> Type -> Maybe (TyCon, ThetaType)
forall a b. (a -> b) -> a -> b
$ CType -> Type
unCType CType
g of
Just (TyCon
_, ThetaType
apps) -> do
Bool
-> Judgement
-> ConLike
-> ThetaType
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized (LHsExpr GhcPs))
buildDataCon Bool
True (Judgement -> Judgement
unwhitelistingSplit Judgement
jdg) ConLike
dc ThetaType
apps
Maybe (TyCon, ThetaType)
Nothing -> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized (LHsExpr GhcPs))
forall jdg ext err s (m :: * -> *) a. RuleT jdg ext err s m a
cut
splitDataCon :: DataCon -> TacticsM ()
splitDataCon :: DataCon -> TacticsM ()
splitDataCon = ConLike -> TacticsM ()
splitConLike (ConLike -> TacticsM ())
-> (DataCon -> ConLike) -> DataCon -> TacticsM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DataCon -> ConLike
RealDataCon
destructAll :: TacticsM ()
destructAll :: TacticsM ()
destructAll = 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
let args :: [HyInfo CType]
args = ((HyInfo CType, Int) -> HyInfo CType)
-> [(HyInfo CType, Int)] -> [HyInfo CType]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (HyInfo CType, Int) -> HyInfo CType
forall a b. (a, b) -> a
fst
([(HyInfo CType, Int)] -> [HyInfo CType])
-> [(HyInfo CType, Int)] -> [HyInfo CType]
forall a b. (a -> b) -> a -> b
$ ((HyInfo CType, Int) -> Int)
-> [(HyInfo CType, Int)] -> [(HyInfo CType, Int)]
forall b a. Ord b => (a -> b) -> [a] -> [a]
sortOn (HyInfo CType, Int) -> Int
forall a b. (a, b) -> b
snd
([(HyInfo CType, Int)] -> [(HyInfo CType, Int)])
-> [(HyInfo CType, Int)] -> [(HyInfo CType, Int)]
forall a b. (a -> b) -> a -> b
$ ((HyInfo CType, Provenance) -> Maybe (HyInfo CType, Int))
-> [(HyInfo CType, Provenance)] -> [(HyInfo CType, Int)]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (\(HyInfo CType
hi, Provenance
prov) ->
case Provenance
prov of
TopLevelArgPrv OccName
_ Int
idx Int
_ -> (HyInfo CType, Int) -> Maybe (HyInfo CType, Int)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (HyInfo CType
hi, Int
idx)
Provenance
_ -> Maybe (HyInfo CType, Int)
forall a. Maybe a
Nothing
)
([(HyInfo CType, Provenance)] -> [(HyInfo CType, Int)])
-> [(HyInfo CType, Provenance)] -> [(HyInfo CType, Int)]
forall a b. (a -> b) -> a -> b
$ (HyInfo CType -> (HyInfo CType, Provenance))
-> [HyInfo CType] -> [(HyInfo CType, Provenance)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\HyInfo CType
hi -> (HyInfo CType
hi, HyInfo CType -> Provenance
forall a. HyInfo a -> Provenance
hi_provenance HyInfo CType
hi))
([HyInfo CType] -> [(HyInfo CType, Provenance)])
-> [HyInfo CType] -> [(HyInfo CType, Provenance)]
forall a b. (a -> b) -> a -> b
$ (HyInfo CType -> Bool) -> [HyInfo CType] -> [HyInfo CType]
forall a. (a -> Bool) -> [a] -> [a]
filter (Type -> Bool
isAlgType (Type -> Bool) -> (HyInfo CType -> Type) -> HyInfo CType -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CType -> Type
unCType (CType -> Type) -> (HyInfo CType -> CType) -> HyInfo CType -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HyInfo CType -> CType
forall a. HyInfo a -> a
hi_type)
([HyInfo CType] -> [HyInfo CType])
-> [HyInfo CType] -> [HyInfo CType]
forall a b. (a -> b) -> a -> b
$ Hypothesis CType -> [HyInfo CType]
forall a. Hypothesis a -> [HyInfo a]
unHypothesis
(Hypothesis CType -> [HyInfo CType])
-> Hypothesis CType -> [HyInfo CType]
forall a b. (a -> b) -> a -> b
$ Judgement -> Hypothesis CType
forall a. Judgement' a -> Hypothesis a
jHypothesis Judgement
jdg
[HyInfo CType] -> (HyInfo CType -> TacticsM ()) -> TacticsM ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
t a -> (a -> f b) -> f ()
for_ [HyInfo CType]
args ((HyInfo CType -> TacticsM ()) -> TacticsM ())
-> (HyInfo CType -> TacticsM ()) -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ \HyInfo CType
arg -> do
TCvSubst
subst <- Judgement
-> TacticT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
TCvSubst
forall (m :: * -> *).
MonadState TacticState m =>
Judgement -> m TCvSubst
getSubstForJudgement (Judgement
-> TacticT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
TCvSubst)
-> TacticT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
Judgement
-> TacticT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
TCvSubst
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m 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
HyInfo CType -> TacticsM ()
destruct (HyInfo CType -> TacticsM ()) -> HyInfo CType -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ (CType -> CType) -> HyInfo CType -> HyInfo CType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((TCvSubst -> Type -> Type) -> TCvSubst -> CType -> CType
coerce HasCallStack => TCvSubst -> Type -> Type
TCvSubst -> Type -> Type
substTy TCvSubst
subst) HyInfo CType
arg
userSplit :: OccName -> TacticsM ()
userSplit :: OccName -> TacticsM ()
userSplit OccName
occ = 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
let g :: CType
g = Judgement -> CType
forall a. Judgement' a -> a
jGoal Judgement
jdg
case HasDebugCallStack => Type -> Maybe (TyCon, ThetaType)
Type -> Maybe (TyCon, ThetaType)
splitTyConApp_maybe (Type -> Maybe (TyCon, ThetaType))
-> Type -> Maybe (TyCon, ThetaType)
forall a b. (a -> b) -> a -> b
$ CType -> Type
unCType CType
g of
Just (TyCon
tc, ThetaType
_) -> do
case (DataCon -> Bool) -> [DataCon] -> Maybe DataCon
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find (OccName -> OccName -> Bool
sloppyEqOccName OccName
occ (OccName -> Bool) -> (DataCon -> OccName) -> DataCon -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> OccName
forall name. HasOccName name => name -> OccName
occName (Name -> OccName) -> (DataCon -> Name) -> DataCon -> OccName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DataCon -> Name
dataConName)
([DataCon] -> Maybe DataCon) -> [DataCon] -> Maybe DataCon
forall a b. (a -> b) -> a -> b
$ TyCon -> [DataCon]
tyConDataCons TyCon
tc of
Just DataCon
dc -> DataCon -> TacticsM ()
splitDataCon DataCon
dc
Maybe DataCon
Nothing -> TacticError -> TacticsM ()
forall err jdg ext s (m :: * -> *) a.
err -> TacticT jdg ext err s m a
failure (TacticError -> TacticsM ()) -> TacticError -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ OccName -> TacticError
NotInScope OccName
occ
Maybe (TyCon, ThetaType)
Nothing -> TacticError -> TacticsM ()
forall err jdg ext s (m :: * -> *) a.
err -> TacticT jdg ext err s m a
failure (TacticError -> TacticsM ()) -> TacticError -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ OccName -> TacticError
NotInScope OccName
occ
matching :: (Judgement -> TacticsM ()) -> TacticsM ()
matching :: (Judgement -> TacticsM ()) -> TacticsM ()
matching Judgement -> TacticsM ()
f = StateT
Judgement
(ProofStateT
(Synthesized (LHsExpr GhcPs))
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM)
()
-> TacticsM ()
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
Judgement
(ProofStateT
(Synthesized (LHsExpr GhcPs))
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM)
()
-> TacticsM ())
-> StateT
Judgement
(ProofStateT
(Synthesized (LHsExpr GhcPs))
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM)
()
-> TacticsM ()
forall a b. (a -> b) -> a -> b
$ (Judgement
-> ProofStateT
(Synthesized (LHsExpr GhcPs))
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
((), Judgement))
-> StateT
Judgement
(ProofStateT
(Synthesized (LHsExpr GhcPs))
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM)
()
forall s (m :: * -> *) a. (s -> m (a, s)) -> StateT s m a
StateT ((Judgement
-> ProofStateT
(Synthesized (LHsExpr GhcPs))
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
((), Judgement))
-> StateT
Judgement
(ProofStateT
(Synthesized (LHsExpr GhcPs))
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM)
())
-> (Judgement
-> ProofStateT
(Synthesized (LHsExpr GhcPs))
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
((), Judgement))
-> StateT
Judgement
(ProofStateT
(Synthesized (LHsExpr GhcPs))
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM)
()
forall a b. (a -> b) -> a -> b
$ \Judgement
s -> 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 s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT (TacticsM ()
-> StateT
Judgement
(ProofStateT
(Synthesized (LHsExpr GhcPs))
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM)
()
forall jdg ext err s (m :: * -> *) a.
TacticT jdg ext err s m a
-> StateT jdg (ProofStateT ext ext err s m) a
unTacticT (TacticsM ()
-> StateT
Judgement
(ProofStateT
(Synthesized (LHsExpr GhcPs))
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM)
())
-> TacticsM ()
-> StateT
Judgement
(ProofStateT
(Synthesized (LHsExpr GhcPs))
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM)
()
forall a b. (a -> b) -> a -> b
$ Judgement -> TacticsM ()
f Judgement
s) Judgement
s
attemptOn :: (Judgement -> [a]) -> (a -> TacticsM ()) -> TacticsM ()
attemptOn :: (Judgement -> [a]) -> (a -> TacticsM ()) -> TacticsM ()
attemptOn Judgement -> [a]
getNames a -> TacticsM ()
tac = (Judgement -> TacticsM ()) -> TacticsM ()
matching ([TacticsM ()] -> TacticsM ()
forall (m :: * -> *) jdg ext err s a.
Monad m =>
[TacticT jdg ext err s m a] -> TacticT jdg ext err s m a
choice ([TacticsM ()] -> TacticsM ())
-> (Judgement -> [TacticsM ()]) -> Judgement -> TacticsM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> TacticsM ()) -> [a] -> [TacticsM ()]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\a
s -> a -> TacticsM ()
tac a
s) ([a] -> [TacticsM ()])
-> (Judgement -> [a]) -> Judgement -> [TacticsM ()]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Judgement -> [a]
getNames)
localTactic :: TacticsM a -> (Judgement -> Judgement) -> TacticsM a
localTactic :: TacticsM a -> (Judgement -> Judgement) -> TacticsM a
localTactic TacticsM a
t Judgement -> Judgement
f = do
StateT
Judgement
(ProofStateT
(Synthesized (LHsExpr GhcPs))
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM)
a
-> TacticsM 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
Judgement
(ProofStateT
(Synthesized (LHsExpr GhcPs))
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM)
a
-> TacticsM a)
-> StateT
Judgement
(ProofStateT
(Synthesized (LHsExpr GhcPs))
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM)
a
-> TacticsM a
forall a b. (a -> b) -> a -> b
$ (Judgement
-> ProofStateT
(Synthesized (LHsExpr GhcPs))
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(a, Judgement))
-> StateT
Judgement
(ProofStateT
(Synthesized (LHsExpr GhcPs))
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM)
a
forall s (m :: * -> *) a. (s -> m (a, s)) -> StateT s m a
StateT ((Judgement
-> ProofStateT
(Synthesized (LHsExpr GhcPs))
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(a, Judgement))
-> StateT
Judgement
(ProofStateT
(Synthesized (LHsExpr GhcPs))
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM)
a)
-> (Judgement
-> ProofStateT
(Synthesized (LHsExpr GhcPs))
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(a, Judgement))
-> StateT
Judgement
(ProofStateT
(Synthesized (LHsExpr GhcPs))
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM)
a
forall a b. (a -> b) -> a -> b
$ \Judgement
jdg ->
StateT
Judgement
(ProofStateT
(Synthesized (LHsExpr GhcPs))
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM)
a
-> Judgement
-> ProofStateT
(Synthesized (LHsExpr GhcPs))
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(a, Judgement)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT (TacticsM a
-> StateT
Judgement
(ProofStateT
(Synthesized (LHsExpr GhcPs))
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM)
a
forall jdg ext err s (m :: * -> *) a.
TacticT jdg ext err s m a
-> StateT jdg (ProofStateT ext ext err s m) a
unTacticT TacticsM a
t) (Judgement
-> ProofStateT
(Synthesized (LHsExpr GhcPs))
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(a, Judgement))
-> Judgement
-> ProofStateT
(Synthesized (LHsExpr GhcPs))
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(a, Judgement)
forall a b. (a -> b) -> a -> b
$ Judgement -> Judgement
f Judgement
jdg
refine :: TacticsM ()
refine :: TacticsM ()
refine = TacticsM ()
intros TacticsM () -> TacticsM () -> TacticsM ()
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
<%> TacticsM ()
splitSingle
auto' :: Int -> TacticsM ()
auto' :: Int -> TacticsM ()
auto' Int
0 = TacticError -> TacticsM ()
forall err jdg ext s (m :: * -> *) a.
err -> TacticT jdg ext err s m a
failure TacticError
OutOfGas
auto' Int
n = do
let loop :: TacticsM ()
loop = Int -> TacticsM ()
auto' (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)
TacticsM () -> TacticsM ()
forall (m :: * -> *) jdg ext err s.
Monad m =>
TacticT jdg ext err s m () -> TacticT jdg ext err s m ()
try TacticsM ()
intros
TacticsM ()
assumption TacticsM () -> TacticsM () -> TacticsM ()
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|>
[TacticsM ()] -> TacticsM ()
forall (m :: * -> *) jdg ext err s a.
Monad m =>
[TacticT jdg ext err s m a] -> TacticT jdg ext err s m a
choice
[ (HyInfo CType -> TacticsM ()) -> TacticsM ()
overFunctions ((HyInfo CType -> TacticsM ()) -> TacticsM ())
-> (HyInfo CType -> TacticsM ()) -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ \HyInfo CType
fname -> do
TacticsM () -> TacticsM ()
forall a. TacticsM a -> TacticsM a
requireConcreteHole (TacticsM () -> TacticsM ()) -> TacticsM () -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ Saturation -> HyInfo CType -> TacticsM ()
apply Saturation
Saturated HyInfo CType
fname
TacticsM ()
loop
, (HyInfo CType -> TacticsM ()) -> TacticsM ()
overAlgebraicTerms ((HyInfo CType -> TacticsM ()) -> TacticsM ())
-> (HyInfo CType -> TacticsM ()) -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ \HyInfo CType
aname -> do
HyInfo CType -> TacticsM ()
destructAuto HyInfo CType
aname
TacticsM ()
loop
, TacticsM ()
splitAuto TacticsM () -> TacticsM () -> TacticsM ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> TacticsM ()
loop
, TacticsM ()
recursion
]
overFunctions :: (HyInfo CType -> TacticsM ()) -> TacticsM ()
overFunctions :: (HyInfo CType -> TacticsM ()) -> TacticsM ()
overFunctions =
(Judgement -> [HyInfo CType])
-> (HyInfo CType -> TacticsM ()) -> TacticsM ()
forall a. (Judgement -> [a]) -> (a -> TacticsM ()) -> TacticsM ()
attemptOn ((Judgement -> [HyInfo CType])
-> (HyInfo CType -> TacticsM ()) -> TacticsM ())
-> (Judgement -> [HyInfo CType])
-> (HyInfo CType -> TacticsM ())
-> TacticsM ()
forall a b. (a -> b) -> a -> b
$ (HyInfo CType -> Bool) -> [HyInfo CType] -> [HyInfo CType]
forall a. (a -> Bool) -> [a] -> [a]
filter (Type -> Bool
isFunction (Type -> Bool) -> (HyInfo CType -> Type) -> HyInfo CType -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CType -> Type
unCType (CType -> Type) -> (HyInfo CType -> CType) -> HyInfo CType -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HyInfo CType -> CType
forall a. HyInfo a -> a
hi_type)
([HyInfo CType] -> [HyInfo CType])
-> (Judgement -> [HyInfo CType]) -> Judgement -> [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 -> [HyInfo CType])
-> (Judgement -> Hypothesis CType) -> Judgement -> [HyInfo CType]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Judgement -> Hypothesis CType
forall a. Judgement' a -> Hypothesis a
jHypothesis
overAlgebraicTerms :: (HyInfo CType -> TacticsM ()) -> TacticsM ()
overAlgebraicTerms :: (HyInfo CType -> TacticsM ()) -> TacticsM ()
overAlgebraicTerms =
(Judgement -> [HyInfo CType])
-> (HyInfo CType -> TacticsM ()) -> TacticsM ()
forall a. (Judgement -> [a]) -> (a -> TacticsM ()) -> TacticsM ()
attemptOn Judgement -> [HyInfo CType]
jAcceptableDestructTargets
allNames :: Judgement -> Set OccName
allNames :: Judgement -> Set OccName
allNames = Hypothesis CType -> Set OccName
forall a. Hypothesis a -> Set OccName
hyNamesInScope (Hypothesis CType -> Set OccName)
-> (Judgement -> Hypothesis CType) -> Judgement -> Set OccName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Judgement -> Hypothesis CType
forall a. Judgement' a -> Hypothesis a
jHypothesis
applyMethod :: Class -> PredType -> OccName -> TacticsM ()
applyMethod :: Class -> Type -> OccName -> TacticsM ()
applyMethod Class
cls Type
df OccName
method_name = do
case (TyVar -> Bool) -> [TyVar] -> Maybe TyVar
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find ((OccName -> OccName -> Bool
forall a. Eq a => a -> a -> Bool
== OccName
method_name) (OccName -> Bool) -> (TyVar -> OccName) -> TyVar -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyVar -> OccName
forall name. HasOccName name => name -> OccName
occName) ([TyVar] -> Maybe TyVar) -> [TyVar] -> Maybe TyVar
forall a b. (a -> b) -> a -> b
$ Class -> [TyVar]
classMethods Class
cls of
Just TyVar
method -> do
let (Type
_, ThetaType
apps) = Type -> (Type, ThetaType)
splitAppTys Type
df
let ty :: Type
ty = HasDebugCallStack => Type -> ThetaType -> Type
Type -> ThetaType -> Type
piResultTys (TyVar -> Type
idType TyVar
method) ThetaType
apps
Saturation -> HyInfo CType -> TacticsM ()
apply Saturation
Saturated (HyInfo CType -> TacticsM ()) -> HyInfo CType -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ OccName -> Provenance -> CType -> HyInfo CType
forall a. OccName -> Provenance -> a -> HyInfo a
HyInfo OccName
method_name (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
ty
Maybe TyVar
Nothing -> TacticError -> TacticsM ()
forall err jdg ext s (m :: * -> *) a.
err -> TacticT jdg ext err s m a
failure (TacticError -> TacticsM ()) -> TacticError -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ OccName -> TacticError
NotInScope OccName
method_name
applyByName :: OccName -> TacticsM ()
applyByName :: OccName -> TacticsM ()
applyByName OccName
name = do
Judgement
g <- 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
[TacticsM ()] -> TacticsM ()
forall (m :: * -> *) jdg ext err s a.
Monad m =>
[TacticT jdg ext err s m a] -> TacticT jdg ext err s m a
choice ([TacticsM ()] -> TacticsM ()) -> [TacticsM ()] -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ (Hypothesis CType -> [HyInfo CType]
forall a. Hypothesis a -> [HyInfo a]
unHypothesis (Judgement -> Hypothesis CType
forall a. Judgement' a -> Hypothesis a
jHypothesis Judgement
g)) [HyInfo CType] -> (HyInfo CType -> TacticsM ()) -> [TacticsM ()]
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \HyInfo CType
hi ->
case HyInfo CType -> OccName
forall a. HyInfo a -> OccName
hi_name HyInfo CType
hi OccName -> OccName -> Bool
forall a. Eq a => a -> a -> Bool
== OccName
name of
Bool
True -> Saturation -> HyInfo CType -> TacticsM ()
apply Saturation
Saturated HyInfo CType
hi
Bool
False -> TacticsM ()
forall (f :: * -> *) a. Alternative f => f a
empty
applyByType :: Type -> TacticsM ()
applyByType :: Type -> TacticsM ()
applyByType Type
ty = String -> TacticsM () -> TacticsM ()
forall (m :: * -> *) jdg ext err s a.
Functor m =>
String
-> TacticT jdg (Synthesized ext) err s m a
-> TacticT jdg (Synthesized ext) err s m a
tracing (String
"applyByType " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Type -> String
forall a. Show a => a -> String
show Type
ty) (TacticsM () -> TacticsM ()) -> TacticsM () -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ 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
let g :: CType
g = Judgement -> CType
forall a. Judgement' a -> a
jGoal Judgement
jdg
Type
ty' <- Type
-> TacticT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
Type
forall (m :: * -> *). MonadState TacticState m => Type -> m Type
freshTyvars Type
ty
let ([TyVar]
_, ThetaType
_, ThetaType
args, Type
ret) = Type -> ([TyVar], ThetaType, ThetaType, Type)
tacticsSplitFunTy Type
ty'
(Judgement
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized (LHsExpr GhcPs)))
-> 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
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized (LHsExpr GhcPs)))
-> TacticsM ())
-> (Judgement
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized (LHsExpr GhcPs)))
-> TacticsM ()
forall a b. (a -> b) -> a -> b
$ \Judgement
jdg -> do
CType -> CType -> RuleM ()
unify CType
g (Type -> CType
CType Type
ret)
Synthesized [LHsExpr GhcPs]
ext
<- ([Synthesized (LHsExpr GhcPs)] -> Synthesized [LHsExpr GhcPs])
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
[Synthesized (LHsExpr GhcPs)]
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized [LHsExpr GhcPs])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [Synthesized (LHsExpr GhcPs)] -> Synthesized [LHsExpr GhcPs]
forall a. [Synthesized a] -> Synthesized [a]
unzipTrace
(RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
[Synthesized (LHsExpr GhcPs)]
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized [LHsExpr GhcPs]))
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
[Synthesized (LHsExpr GhcPs)]
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized [LHsExpr GhcPs])
forall a b. (a -> b) -> a -> b
$ (Type
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized (LHsExpr GhcPs)))
-> ThetaType
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
[Synthesized (LHsExpr GhcPs)]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse ( Judgement
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized (LHsExpr GhcPs))
newSubgoal
(Judgement
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized (LHsExpr GhcPs)))
-> (Type -> Judgement)
-> Type
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized (LHsExpr GhcPs))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Judgement -> Judgement
blacklistingDestruct
(Judgement -> Judgement)
-> (Type -> Judgement) -> Type -> Judgement
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (CType -> Judgement -> Judgement)
-> Judgement -> CType -> Judgement
forall a b c. (a -> b -> c) -> b -> a -> c
flip CType -> Judgement -> Judgement
forall a. a -> Judgement' a -> Judgement' a
withNewGoal Judgement
jdg
(CType -> Judgement) -> (Type -> CType) -> Type -> Judgement
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> CType
CType
) ThetaType
args
Synthesized (LHsExpr GhcPs)
app <- Judgement
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized (LHsExpr GhcPs))
newSubgoal (Judgement
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized (LHsExpr GhcPs)))
-> (Judgement -> Judgement)
-> Judgement
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized (LHsExpr GhcPs))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Judgement -> Judgement
blacklistingDestruct (Judgement
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized (LHsExpr GhcPs)))
-> Judgement
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized (LHsExpr GhcPs))
forall a b. (a -> b) -> a -> b
$ CType -> Judgement -> Judgement
forall a. a -> Judgement' a -> Judgement' a
withNewGoal (Type -> CType
CType Type
ty) Judgement
jdg
Synthesized (LHsExpr GhcPs)
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized (LHsExpr GhcPs))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Synthesized (LHsExpr GhcPs)
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized (LHsExpr GhcPs)))
-> Synthesized (LHsExpr GhcPs)
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized (LHsExpr GhcPs))
forall a b. (a -> b) -> a -> b
$
(HsExpr GhcPs -> LHsExpr GhcPs)
-> Synthesized (HsExpr GhcPs) -> Synthesized (LHsExpr GhcPs)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap HsExpr GhcPs -> LHsExpr GhcPs
forall a. HasSrcSpan a => SrcSpanLess a -> a
noLoc (Synthesized (HsExpr GhcPs) -> Synthesized (LHsExpr GhcPs))
-> Synthesized (HsExpr GhcPs) -> Synthesized (LHsExpr GhcPs)
forall a b. (a -> b) -> a -> b
$
(HsExpr GhcPs -> HsExpr GhcPs -> HsExpr GhcPs)
-> HsExpr GhcPs -> [HsExpr GhcPs] -> HsExpr GhcPs
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' HsExpr GhcPs -> HsExpr GhcPs -> HsExpr GhcPs
forall e. App e => e -> e -> e
(@@)
(HsExpr GhcPs -> [HsExpr GhcPs] -> HsExpr GhcPs)
-> Synthesized (HsExpr GhcPs)
-> Synthesized ([HsExpr GhcPs] -> HsExpr GhcPs)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (LHsExpr GhcPs -> HsExpr GhcPs)
-> Synthesized (LHsExpr GhcPs) -> Synthesized (HsExpr GhcPs)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap LHsExpr GhcPs -> HsExpr GhcPs
forall a. HasSrcSpan a => a -> SrcSpanLess a
unLoc Synthesized (LHsExpr GhcPs)
app
Synthesized ([HsExpr GhcPs] -> HsExpr GhcPs)
-> Synthesized [HsExpr GhcPs] -> Synthesized (HsExpr GhcPs)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ([LHsExpr GhcPs] -> [HsExpr GhcPs])
-> Synthesized [LHsExpr GhcPs] -> Synthesized [HsExpr GhcPs]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((LHsExpr GhcPs -> HsExpr GhcPs)
-> [LHsExpr GhcPs] -> [HsExpr GhcPs]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap LHsExpr GhcPs -> HsExpr GhcPs
forall a. HasSrcSpan a => a -> SrcSpanLess a
unLoc) Synthesized [LHsExpr GhcPs]
ext
nary :: Int -> TacticsM ()
nary :: Int -> TacticsM ()
nary Int
n = do
Type
a <- TacticT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
Type
forall (m :: * -> *). MonadState TacticState m => m Type
newUnivar
Type
b <- TacticT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
Type
forall (m :: * -> *). MonadState TacticState m => m Type
newUnivar
Type -> TacticsM ()
applyByType (Type -> TacticsM ()) -> Type -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ ThetaType -> Type -> Type
mkFunTys' (Int -> Type -> ThetaType
forall a. Int -> a -> [a]
replicate Int
n Type
a) Type
b
self :: TacticsM ()
self :: TacticsM ()
self =
([(OccName, CType)] -> Maybe (OccName, CType))
-> TacticsM [(OccName, CType)]
-> TacticT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Maybe (OccName, CType))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [(OccName, CType)] -> Maybe (OccName, CType)
forall a. [a] -> Maybe a
listToMaybe TacticsM [(OccName, CType)]
getCurrentDefinitions TacticT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Maybe (OccName, CType))
-> (Maybe (OccName, CType) -> TacticsM ()) -> TacticsM ()
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
Just (OccName
self, CType
_) -> (HyInfo CType -> TacticsM ()) -> OccName -> TacticsM ()
forall a. (HyInfo CType -> TacticsM a) -> OccName -> TacticsM a
useNameFromContext (Saturation -> HyInfo CType -> TacticsM ()
apply Saturation
Saturated) OccName
self
Maybe (OccName, CType)
Nothing -> TacticError -> TacticsM ()
forall err jdg ext s (m :: * -> *) a.
err -> TacticT jdg ext err s m a
failure (TacticError -> TacticsM ()) -> TacticError -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ String -> TacticError
TacticPanic String
"no defining function"
cata :: HyInfo CType -> TacticsM ()
cata :: HyInfo CType -> TacticsM ()
cata HyInfo CType
hi = do
([TyVar]
_, ThetaType
_, ThetaType
calling_args, Type
_)
<- Type -> ([TyVar], ThetaType, ThetaType, Type)
tacticsSplitFunTy (Type -> ([TyVar], ThetaType, ThetaType, Type))
-> (CType -> Type)
-> CType
-> ([TyVar], ThetaType, ThetaType, Type)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CType -> Type
unCType (CType -> ([TyVar], ThetaType, ThetaType, Type))
-> TacticT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
CType
-> TacticT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
([TyVar], ThetaType, ThetaType, Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TacticT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
CType
getDefiningType
ThetaType
freshened_args <- (Type
-> TacticT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
Type)
-> ThetaType
-> TacticT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
ThetaType
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse Type
-> TacticT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
Type
forall (m :: * -> *). MonadState TacticState m => Type -> m Type
freshTyvars ThetaType
calling_args
Hypothesis CType
diff <- TacticsM ()
-> TacticT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Hypothesis CType)
hyDiff (TacticsM ()
-> TacticT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Hypothesis CType))
-> TacticsM ()
-> TacticT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Hypothesis CType)
forall a b. (a -> b) -> a -> b
$ HyInfo CType -> TacticsM ()
destruct HyInfo CType
hi
[HyInfo CType]
unifiable_diff <- ((HyInfo CType
-> TacticT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
Bool)
-> [HyInfo CType]
-> TacticT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
[HyInfo CType])
-> [HyInfo CType]
-> (HyInfo CType
-> TacticT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
Bool)
-> TacticT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
[HyInfo CType]
forall a b c. (a -> b -> c) -> b -> a -> c
flip (HyInfo CType
-> TacticT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
Bool)
-> [HyInfo CType]
-> TacticT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
[HyInfo CType]
forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
filterM (Hypothesis CType -> [HyInfo CType]
forall a. Hypothesis a -> [HyInfo a]
unHypothesis Hypothesis CType
diff) ((HyInfo CType
-> TacticT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
Bool)
-> TacticT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
[HyInfo CType])
-> (HyInfo CType
-> TacticT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
Bool)
-> TacticT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
[HyInfo CType]
forall a b. (a -> b) -> a -> b
$ \HyInfo CType
hi ->
((Type
-> TacticT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
Bool)
-> ThetaType
-> TacticT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
Bool)
-> ThetaType
-> (Type
-> TacticT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
Bool)
-> TacticT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
Bool
forall a b c. (a -> b -> c) -> b -> a -> c
flip (Type
-> TacticT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
Bool)
-> ThetaType
-> TacticT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
Bool
forall (m :: * -> *) a. Monad m => (a -> m Bool) -> [a] -> m Bool
anyM ThetaType
freshened_args ((Type
-> TacticT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
Bool)
-> TacticT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
Bool)
-> (Type
-> TacticT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
Bool)
-> TacticT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
Bool
forall a b. (a -> b) -> a -> b
$ \Type
ty ->
CType
-> CType
-> TacticT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
Bool
forall (m :: * -> *).
MonadState TacticState m =>
CType -> CType -> m Bool
canUnify (HyInfo CType -> CType
forall a. HyInfo a -> a
hi_type HyInfo CType
hi) (CType
-> TacticT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
Bool)
-> CType
-> TacticT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
Bool
forall a b. (a -> b) -> a -> b
$ Type -> CType
CType Type
ty
(Judgement
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized (LHsExpr GhcPs)))
-> 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
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized (LHsExpr GhcPs)))
-> TacticsM ())
-> (Judgement
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized (LHsExpr GhcPs)))
-> TacticsM ()
forall a b. (a -> b) -> a -> b
$
(OccName -> OccName)
-> (HyInfo CType -> TacticsM ())
-> Hypothesis CType
-> Judgement
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized (LHsExpr GhcPs))
letForEach
(String -> OccName
mkVarOcc (String -> OccName) -> (OccName -> String) -> OccName -> OccName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String -> String -> String) -> String -> String -> String
forall a b c. (a -> b -> c) -> b -> a -> c
flip String -> String -> String
forall a. Monoid a => a -> a -> a
mappend String
"_c" (String -> String) -> (OccName -> String) -> OccName -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OccName -> String
occNameString)
(\HyInfo CType
hi -> TacticsM ()
self TacticsM () -> TacticsM () -> TacticsM ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> TacticsM () -> TacticsM () -> TacticsM ()
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 (OccName -> TacticsM ()
assume (OccName -> TacticsM ()) -> OccName -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ HyInfo CType -> OccName
forall a. HyInfo a -> OccName
hi_name HyInfo CType
hi) TacticsM ()
assumption)
(Hypothesis CType
-> Judgement
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized (LHsExpr GhcPs)))
-> Hypothesis CType
-> Judgement
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized (LHsExpr GhcPs))
forall a b. (a -> b) -> a -> b
$ [HyInfo CType] -> Hypothesis CType
forall a. [HyInfo a] -> Hypothesis a
Hypothesis [HyInfo CType]
unifiable_diff
letBind :: [OccName] -> TacticsM ()
letBind :: [OccName] -> TacticsM ()
letBind [OccName]
occs = 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
[(OccName, Judgement)]
occ_tys <- [OccName]
-> (OccName
-> TacticT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(OccName, Judgement))
-> TacticT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
[(OccName, Judgement)]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for [OccName]
occs
((OccName
-> TacticT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(OccName, Judgement))
-> TacticT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
[(OccName, Judgement)])
-> (OccName
-> TacticT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(OccName, Judgement))
-> TacticT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
[(OccName, Judgement)]
forall a b. (a -> b) -> a -> b
$ \OccName
occ
-> (Judgement -> (OccName, Judgement))
-> TacticT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
Judgement
-> TacticT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(OccName, Judgement)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (OccName
occ, )
(TacticT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
Judgement
-> TacticT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(OccName, Judgement))
-> TacticT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
Judgement
-> TacticT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(OccName, Judgement)
forall a b. (a -> b) -> a -> b
$ (CType -> Judgement)
-> TacticT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
CType
-> TacticT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
Judgement
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (CType -> Judgement -> Judgement
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Judgement
jdg)
(TacticT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
CType
-> TacticT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
Judgement)
-> TacticT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
CType
-> TacticT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
Judgement
forall a b. (a -> b) -> a -> b
$ (Type -> CType)
-> TacticT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
Type
-> TacticT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
CType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Type -> CType
CType
(TacticT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
Type
-> TacticT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
CType)
-> TacticT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
Type
-> TacticT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
CType
forall a b. (a -> b) -> a -> b
$ TacticT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
Type
forall (m :: * -> *). MonadState TacticState m => m Type
newUnivar
(Judgement
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized (LHsExpr GhcPs)))
-> 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
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized (LHsExpr GhcPs)))
-> TacticsM ())
-> (Judgement
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized (LHsExpr GhcPs)))
-> TacticsM ()
forall a b. (a -> b) -> a -> b
$ [(OccName, Judgement)]
-> Judgement
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized (LHsExpr GhcPs))
nonrecLet [(OccName, Judgement)]
occ_tys
nested :: OccName -> TacticsM ()
nested :: OccName -> TacticsM ()
nested = TacticsM () -> TacticsM ()
deepening (TacticsM () -> TacticsM ())
-> (OccName -> TacticsM ()) -> OccName -> TacticsM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Saturation -> OccName -> TacticsM ()
use (Int -> Saturation
Unsaturated Int
1)
deep :: Int -> TacticsM () -> TacticsM ()
deep :: Int -> TacticsM () -> TacticsM ()
deep Int
0 TacticsM ()
_ = () -> TacticsM ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
deep Int
n TacticsM ()
t = (TacticsM () -> TacticsM () -> TacticsM ())
-> [TacticsM ()] -> TacticsM ()
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 TacticsM () -> TacticsM () -> TacticsM ()
forall a. TacticsM a -> TacticsM a -> TacticsM a
bindOne ([TacticsM ()] -> TacticsM ()) -> [TacticsM ()] -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ Int -> TacticsM () -> [TacticsM ()]
forall a. Int -> a -> [a]
replicate Int
n TacticsM ()
t
deepening :: TacticsM () -> TacticsM ()
deepening :: TacticsM () -> TacticsM ()
deepening TacticsM ()
t =
[TacticsM ()] -> TacticsM ()
forall (t :: * -> *) (f :: * -> *) a.
(Foldable t, Alternative f) =>
t (f a) -> f a
asum ([TacticsM ()] -> TacticsM ()) -> [TacticsM ()] -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ (Int -> TacticsM ()) -> [Int] -> [TacticsM ()]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Int -> TacticsM () -> TacticsM ())
-> TacticsM () -> Int -> TacticsM ()
forall a b c. (a -> b -> c) -> b -> a -> c
flip Int -> TacticsM () -> TacticsM ()
deep TacticsM ()
t) [Int
0 .. Int
100]
bindOne :: TacticsM a -> TacticsM a -> TacticsM a
bindOne :: TacticsM a -> TacticsM a -> TacticsM a
bindOne TacticsM a
t TacticsM a
t1 = TacticsM a
t TacticsM a -> [TacticsM a] -> TacticsM a
forall (m :: * -> *) jdg ext err s a.
Functor m =>
TacticT jdg ext err s m a
-> [TacticT jdg ext err s m a] -> TacticT jdg ext err s m a
<@> [TacticsM a
t1]
collapse :: TacticsM ()
collapse :: TacticsM ()
collapse = do
Judgement
g <- 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
let terms :: [HyInfo CType]
terms = Hypothesis CType -> [HyInfo CType]
forall a. Hypothesis a -> [HyInfo a]
unHypothesis (Hypothesis CType -> [HyInfo CType])
-> Hypothesis CType -> [HyInfo CType]
forall a b. (a -> b) -> a -> b
$ (HyInfo CType -> Bool) -> Hypothesis CType -> Hypothesis CType
forall a. (HyInfo a -> Bool) -> Hypothesis a -> Hypothesis a
hyFilter ((Judgement -> CType
forall a. Judgement' a -> a
jGoal Judgement
g CType -> CType -> Bool
forall a. Eq a => a -> a -> Bool
==) (CType -> Bool) -> (HyInfo CType -> CType) -> HyInfo CType -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HyInfo CType -> CType
forall a. HyInfo a -> a
hi_type) (Hypothesis CType -> Hypothesis CType)
-> Hypothesis CType -> Hypothesis CType
forall a b. (a -> b) -> a -> b
$ Judgement -> Hypothesis CType
forall a. Judgement' a -> Hypothesis a
jLocalHypothesis Judgement
g
case [HyInfo CType]
terms of
[HyInfo CType
hi] -> OccName -> TacticsM ()
assume (OccName -> TacticsM ()) -> OccName -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ HyInfo CType -> OccName
forall a. HyInfo a -> OccName
hi_name HyInfo CType
hi
[HyInfo CType]
_ -> Int -> TacticsM ()
nary ([HyInfo CType] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [HyInfo CType]
terms) TacticsM () -> [TacticsM ()] -> TacticsM ()
forall (m :: * -> *) jdg ext err s a.
Functor m =>
TacticT jdg ext err s m a
-> [TacticT jdg ext err s m a] -> TacticT jdg ext err s m a
<@> (HyInfo CType -> TacticsM ()) -> [HyInfo CType] -> [TacticsM ()]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (OccName -> TacticsM ()
assume (OccName -> TacticsM ())
-> (HyInfo CType -> OccName) -> HyInfo CType -> TacticsM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HyInfo CType -> OccName
forall a. HyInfo a -> OccName
hi_name) [HyInfo CType]
terms
with_arg :: TacticsM ()
with_arg :: TacticsM ()
with_arg = (Judgement
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized (LHsExpr GhcPs)))
-> 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
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized (LHsExpr GhcPs)))
-> TacticsM ())
-> (Judgement
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized (LHsExpr GhcPs)))
-> TacticsM ()
forall a b. (a -> b) -> a -> b
$ \Judgement
jdg -> do
let g :: CType
g = Judgement -> CType
forall a. Judgement' a -> a
jGoal Judgement
jdg
Type
fresh_ty <- RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
Type
forall (m :: * -> *). MonadState TacticState m => m Type
newUnivar
Synthesized (LHsExpr GhcPs)
a <- Judgement
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized (LHsExpr GhcPs))
newSubgoal (Judgement
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized (LHsExpr GhcPs)))
-> Judgement
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized (LHsExpr GhcPs))
forall a b. (a -> b) -> a -> b
$ CType -> Judgement -> Judgement
forall a. a -> Judgement' a -> Judgement' a
withNewGoal (Type -> CType
CType Type
fresh_ty) Judgement
jdg
Synthesized (LHsExpr GhcPs)
f <- Judgement
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized (LHsExpr GhcPs))
newSubgoal (Judgement
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized (LHsExpr GhcPs)))
-> Judgement
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized (LHsExpr GhcPs))
forall a b. (a -> b) -> a -> b
$ CType -> Judgement -> Judgement
forall a. a -> Judgement' a -> Judgement' a
withNewGoal ((ThetaType -> Type -> Type) -> ThetaType -> CType -> CType
coerce ThetaType -> Type -> Type
mkFunTys' [Type
fresh_ty] CType
g) Judgement
jdg
Synthesized (LHsExpr GhcPs)
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized (LHsExpr GhcPs))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Synthesized (LHsExpr GhcPs)
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized (LHsExpr GhcPs)))
-> Synthesized (LHsExpr GhcPs)
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized (LHsExpr GhcPs))
forall a b. (a -> b) -> a -> b
$ (HsExpr GhcPs -> LHsExpr GhcPs)
-> Synthesized (HsExpr GhcPs) -> Synthesized (LHsExpr GhcPs)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap HsExpr GhcPs -> LHsExpr GhcPs
forall a. HasSrcSpan a => SrcSpanLess a -> a
noLoc (Synthesized (HsExpr GhcPs) -> Synthesized (LHsExpr GhcPs))
-> Synthesized (HsExpr GhcPs) -> Synthesized (LHsExpr GhcPs)
forall a b. (a -> b) -> a -> b
$ HsExpr GhcPs -> HsExpr GhcPs -> HsExpr GhcPs
forall e. App e => e -> e -> e
(@@) (HsExpr GhcPs -> HsExpr GhcPs -> HsExpr GhcPs)
-> Synthesized (HsExpr GhcPs)
-> Synthesized (HsExpr GhcPs -> HsExpr GhcPs)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (LHsExpr GhcPs -> HsExpr GhcPs)
-> Synthesized (LHsExpr GhcPs) -> Synthesized (HsExpr GhcPs)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap LHsExpr GhcPs -> HsExpr GhcPs
forall a. HasSrcSpan a => a -> SrcSpanLess a
unLoc Synthesized (LHsExpr GhcPs)
f Synthesized (HsExpr GhcPs -> HsExpr GhcPs)
-> Synthesized (HsExpr GhcPs) -> Synthesized (HsExpr GhcPs)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (LHsExpr GhcPs -> HsExpr GhcPs)
-> Synthesized (LHsExpr GhcPs) -> Synthesized (HsExpr GhcPs)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap LHsExpr GhcPs -> HsExpr GhcPs
forall a. HasSrcSpan a => a -> SrcSpanLess a
unLoc Synthesized (LHsExpr GhcPs)
a
hyDiff :: TacticsM () -> TacticsM (Hypothesis CType)
hyDiff :: TacticsM ()
-> TacticT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Hypothesis CType)
hyDiff TacticsM ()
m = do
[HyInfo CType]
g <- Hypothesis CType -> [HyInfo CType]
forall a. Hypothesis a -> [HyInfo a]
unHypothesis (Hypothesis CType -> [HyInfo CType])
-> (Judgement -> Hypothesis CType) -> Judgement -> [HyInfo CType]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Judgement -> Hypothesis CType
forall a. Judgement' a -> Hypothesis a
jEntireHypothesis (Judgement -> [HyInfo CType])
-> TacticT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
Judgement
-> TacticT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
[HyInfo 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
let g_len :: Int
g_len = [HyInfo CType] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [HyInfo CType]
g
TacticsM ()
m
[HyInfo CType]
g' <- Hypothesis CType -> [HyInfo CType]
forall a. Hypothesis a -> [HyInfo a]
unHypothesis (Hypothesis CType -> [HyInfo CType])
-> (Judgement -> Hypothesis CType) -> Judgement -> [HyInfo CType]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Judgement -> Hypothesis CType
forall a. Judgement' a -> Hypothesis a
jEntireHypothesis (Judgement -> [HyInfo CType])
-> TacticT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
Judgement
-> TacticT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
[HyInfo 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
Hypothesis CType
-> TacticT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Hypothesis CType)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Hypothesis CType
-> TacticT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Hypothesis CType))
-> Hypothesis CType
-> TacticT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Hypothesis CType)
forall a b. (a -> b) -> a -> b
$ [HyInfo CType] -> Hypothesis CType
forall a. [HyInfo a] -> Hypothesis a
Hypothesis ([HyInfo CType] -> Hypothesis CType)
-> [HyInfo CType] -> Hypothesis CType
forall a b. (a -> b) -> a -> b
$ Int -> [HyInfo CType] -> [HyInfo CType]
forall a. Int -> [a] -> [a]
take ([HyInfo CType] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [HyInfo CType]
g' Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
g_len) [HyInfo CType]
g'