{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TupleSections #-}

module Wingman.Tactics
  ( module Wingman.Tactics
  , runTactic
  ) where

import           Control.Applicative (Alternative(empty), (<|>))
import           Control.Lens ((&), (%~), (<>~))
import           Control.Monad (filterM, unless)
import           Control.Monad (when)
import           Control.Monad.Extra (anyM)
import           Control.Monad.Reader.Class (MonadReader (ask))
import           Control.Monad.State.Strict (StateT(..), runStateT, execStateT)
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           Development.IDE.GHC.Compat hiding (empty)
import           GHC.Exts
import           GHC.SourceGen ((@@))
import           GHC.SourceGen.Expr
import           Refinery.Tactic
import           Refinery.Tactic.Internal
import           Wingman.CodeGen
import           Wingman.GHC
import           Wingman.Judgements
import           Wingman.Machinery
import           Wingman.Naming
import           Wingman.StaticPlugin (pattern MetaprogramSyntax)
import           Wingman.Types


------------------------------------------------------------------------------
-- | Use something in the hypothesis to fill the hole.
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


------------------------------------------------------------------------------
-- | Use something named in the hypothesis to fill the hole.
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
$
        -- This slightly terrible construct is producing a mostly-empty
        -- 'Synthesized'; but there is no monoid instance to do something more
        -- reasonable for a default value.
        (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


------------------------------------------------------------------------------
-- | Like 'apply', but uses an 'OccName' available in the context
-- or the module
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 ()
-- TODO(sandy): This tactic doesn't fire for the @AutoThetaFix@ golden test,
-- presumably due to running afoul of 'requireConcreteHole'. Look into this!
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
    -- Peek allows us to look at the extract produced by this block.
    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
        -- Make sure that the recursive call contains at least one already-bound
        -- pattern value. This ensures it is structurally smaller, and thus
        -- suggests termination.
        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
  -- NOTE(sandy): Safe use of head; context is guaranteed to have a defining
  -- binding
  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..]


------------------------------------------------------------------------------
-- | Introduce a lambda binding every variable.
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)


------------------------------------------------------------------------------
-- | Introduce a lambda binding every variable.
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 -- failure $ GoalMismatch "intros" g
    ([TyVar]
_, ThetaType
_, ThetaType
scaledArgs, Type
res) -> do
      let args :: ThetaType
args = (Type -> Type) -> ThetaType -> ThetaType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Type -> Type
forall a. Scaled a -> Scaled a
scaledThing ThetaType
scaledArgs
      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
mkVisFunTys (Int -> ThetaType -> ThetaType
forall a. Int -> [a] -> [a]
drop Int
num_occs ThetaType
scaledArgs) 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


------------------------------------------------------------------------------
-- | Introduce a single lambda argument, and immediately destruct it.
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
  -- This case should never happen, but I'm validating instead of parsing.
  -- Adding a log to be reminded if the invariant ever goes false.
  --
  -- But note that this isn't a game-ending bug. In the worst case, we'll
  -- accidentally bind too many variables, and incorrectly unify between them.
  -- Which means some GADT cases that should be eliminated won't be --- not the
  -- end of the world.
  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


------------------------------------------------------------------------------
-- | Case split, and leave holes in the matches.
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


------------------------------------------------------------------------------
-- | When running auto, in order to prune the auto search tree, we try
-- a homomorphic destruct whenever possible. If that produces any results, we
-- can probably just prune the other side.
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


------------------------------------------------------------------------------
-- | Case split, and leave holes in the matches.
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


------------------------------------------------------------------------------
-- | Case split, and leave holes in the matches. Performs record punning.
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


------------------------------------------------------------------------------
-- | Case split, using the same data constructor in the matches.
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

  -- Ensure that every data constructor in the domain type is covered in the
  -- codomain; otherwise 'homo' will produce an ill-typed program.
  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
hi


------------------------------------------------------------------------------
-- | LambdaCase split, and leave holes in the matches.
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)


------------------------------------------------------------------------------
-- | LambdaCase split, using the same data constructor in the matches.
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


newtype 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
theta, 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
mkVisFunTys ThetaType
unsaturated_args Type
ret)
    ThetaType -> RuleM ()
learnFromFundeps ThetaType
theta
    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
                    (Type -> CType) -> (Type -> Type) -> Type -> CType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Type
forall a. Scaled a -> Scaled a
scaledThing
                    ) 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


------------------------------------------------------------------------------
-- | Choose between each of the goal's data constructors.
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


------------------------------------------------------------------------------
-- | Choose between each of the goal's data constructors. Different than
-- 'split' because it won't split a data con if it doesn't result in any new
-- goals.
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


------------------------------------------------------------------------------
-- | Like 'split', but only works if there is a single matching data
-- constructor for the goal.
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

------------------------------------------------------------------------------
-- | Like 'split', but prunes any data constructors which have holes.
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 leaves a hole in its extract
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
"_"


------------------------------------------------------------------------------
-- | Sorry leaves a hole in its extract
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
""


------------------------------------------------------------------------------
-- | Allow the given tactic to proceed if and only if it introduces holes that
-- have a different goal than current goal.
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


------------------------------------------------------------------------------
-- | Attempt to instantiate the given ConLike to solve the goal.
--
-- INVARIANT: Assumes the given ConLike is appropriate to construct the type
-- with.
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 -- failure $ GoalMismatch "splitDataCon" g

------------------------------------------------------------------------------
-- | Attempt to instantiate the given data constructor to solve the goal.
--
-- INVARIANT: Assumes the given datacon is appropriate to construct the type
-- with.
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


------------------------------------------------------------------------------
-- | Perform a case split on each top-level argument. Used to implement the
-- "Destruct all function arguments" action.
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

--------------------------------------------------------------------------------
-- | User-facing tactic to implement "Use constructor <x>"
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
  -- TODO(sandy): It's smelly that we need to find the datacon to generate the
  -- code action, send it as a string, and then look it up again. Can we push
  -- this over LSP somehow instead?
  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 f@ takes a function from a judgement to a @Tactic@, and
-- then applies the resulting @Tactic@.
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 -> TacticsM ()
tac ([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


------------------------------------------------------------------------------
-- | Make a function application where the function being applied itself is
-- a hole.
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
                    (Type -> CType) -> (Type -> Type) -> Type -> CType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Type
forall a. Scaled a -> Scaled a
scaledThing
                    ) 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


------------------------------------------------------------------------------
-- | Make an n-ary function call of the form
-- @(_ :: forall a b. a -> a -> b) _ _@.
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
mkVisFunTys (Int -> Type -> ThetaType
forall a. Int -> a -> [a]
replicate Int
n (Type -> ThetaType) -> Type -> ThetaType
forall a b. (a -> b) -> a -> b
$ Type -> Type
forall a. Scaled a -> Scaled a
unrestricted 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"


------------------------------------------------------------------------------
-- | Perform a catamorphism when destructing the given 'HyInfo'. This will
-- result in let binding, making values that call the defining function on each
-- destructed value.
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 (Type
 -> TacticT
      Judgement
      (Synthesized (LHsExpr GhcPs))
      TacticError
      TacticState
      ExtractM
      Type)
-> (Type -> Type)
-> Type
-> TacticT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Type
forall a. Scaled a -> Scaled a
scaledThing) 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

  -- For for every destructed term, check to see if it can unify with any of
  -- the arguments to the calling function. If it doesn't, we don't try to
  -- perform a cata on it.
  [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
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


------------------------------------------------------------------------------
-- | Deeply nest an unsaturated function onto itself
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)


------------------------------------------------------------------------------
-- | Repeatedly bind a tactic on its first hole
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


------------------------------------------------------------------------------
-- | Try 'deep' for arbitrary depths.
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
mkVisFunTys [Type -> Type
forall a. Scaled a -> Scaled a
unrestricted 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


------------------------------------------------------------------------------
-- | Determine the difference in hypothesis due to running a tactic. Also, it
-- runs the tactic.
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'


------------------------------------------------------------------------------
-- | Attempt to run the given tactic in "idiom bracket" mode. For example, if
-- the current goal is
--
--    (_ :: [r])
--
-- then @idiom apply@ will remove the applicative context, resulting in a hole:
--
--    (_ :: r)
--
-- and then use @apply@ to solve it. Let's say this results in:
--
--    (f (_ :: a) (_ :: b))
--
-- Finally, @idiom@ lifts this back into the original applicative:
--
--    (f <$> (_ :: [a]) <*> (_ :: [b]))
--
-- Idiom will fail fast if the current goal doesn't have an applicative
-- instance.
idiom :: TacticsM () -> TacticsM ()
idiom :: TacticsM () -> TacticsM ()
idiom 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
  let hole :: Type
hole = CType -> Type
unCType (CType -> Type) -> CType -> Type
forall a b. (a -> b) -> a -> b
$ Judgement -> CType
forall a. Judgement' a -> a
jGoal Judgement
jdg
  Bool -> TacticsM () -> TacticsM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Type -> Bool
isFunction Type
hole) (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 -> CType -> TacticError
GoalMismatch String
"idiom" (CType -> TacticError) -> CType -> TacticError
forall a b. (a -> b) -> a -> b
$ Judgement -> CType
forall a. Judgement' a -> a
jGoal Judgement
jdg
  case Type -> Maybe (Type, Type)
splitAppTy_maybe Type
hole of
    Just (Type
applic, Type
ty) -> do
      Maybe (Class, Type)
minst <- OccName -> ThetaType -> TacticsM (Maybe (Class, Type))
getKnownInstance (String -> OccName
mkClsOcc String
"Applicative")
            (ThetaType -> TacticsM (Maybe (Class, Type)))
-> (Type -> ThetaType) -> Type -> TacticsM (Maybe (Class, Type))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> ThetaType
forall (f :: * -> *) a. Applicative f => a -> f a
pure
            (Type -> TacticsM (Maybe (Class, Type)))
-> Type -> TacticsM (Maybe (Class, Type))
forall a b. (a -> b) -> a -> b
$ Type
applic
      case Maybe (Class, Type)
minst of
        Maybe (Class, Type)
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
"idiom" (CType -> TacticError) -> CType -> TacticError
forall a b. (a -> b) -> a -> b
$ Type -> CType
CType Type
applic
        Just (Class
_, Type
_) -> do
          (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
            Synthesized (LHsExpr GhcPs)
expr <- Judgement
-> TacticsM ()
-> RuleT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     (Synthesized (LHsExpr GhcPs))
subgoalWith (CType -> Judgement -> Judgement
forall a. a -> Judgement' a -> Judgement' a
withNewGoal (Type -> CType
CType Type
ty) Judgement
jdg) TacticsM ()
m
            case LHsExpr GhcPs -> SrcSpanLess (LHsExpr GhcPs)
forall a. HasSrcSpan a => a -> SrcSpanLess a
unLoc (LHsExpr GhcPs -> SrcSpanLess (LHsExpr GhcPs))
-> LHsExpr GhcPs -> SrcSpanLess (LHsExpr GhcPs)
forall a b. (a -> b) -> a -> b
$ Synthesized (LHsExpr GhcPs) -> LHsExpr GhcPs
forall a. Synthesized a -> a
syn_val Synthesized (LHsExpr GhcPs)
expr of
              HsApp{}     -> 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 -> LHsExpr GhcPs)
-> Synthesized (LHsExpr GhcPs) -> Synthesized (LHsExpr GhcPs)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap LHsExpr GhcPs -> LHsExpr GhcPs
idiomize Synthesized (LHsExpr GhcPs)
expr
              RecordCon{} -> 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 -> LHsExpr GhcPs)
-> Synthesized (LHsExpr GhcPs) -> Synthesized (LHsExpr GhcPs)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap LHsExpr GhcPs -> LHsExpr GhcPs
idiomize Synthesized (LHsExpr GhcPs)
expr
              SrcSpanLess (LHsExpr GhcPs)
_       -> TacticError
-> RuleT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     (Synthesized (LHsExpr GhcPs))
forall err jdg ext s (m :: * -> *).
err -> RuleT jdg ext err s m ext
unsolvable (TacticError
 -> RuleT
      Judgement
      (Synthesized (LHsExpr GhcPs))
      TacticError
      TacticState
      ExtractM
      (Synthesized (LHsExpr GhcPs)))
-> TacticError
-> RuleT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     (Synthesized (LHsExpr GhcPs))
forall a b. (a -> b) -> a -> b
$ String -> CType -> TacticError
GoalMismatch String
"idiom" (CType -> TacticError) -> CType -> TacticError
forall a b. (a -> b) -> a -> b
$ Judgement -> CType
forall a. Judgement' a -> a
jGoal Judgement
jdg
          (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
-> 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
. (CType -> CType) -> Judgement -> Judgement
forall a. (a -> a) -> Judgement' a -> Judgement' a
withModifiedGoal (Type -> CType
CType (Type -> CType) -> (CType -> Type) -> CType -> CType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Type -> Type
mkAppTy Type
applic (Type -> Type) -> (CType -> Type) -> CType -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CType -> Type
unCType)
    Maybe (Type, Type)
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
"idiom" (CType -> TacticError) -> CType -> TacticError
forall a b. (a -> b) -> a -> b
$ Judgement -> CType
forall a. Judgement' a -> a
jGoal Judgement
jdg

subgoalWith :: Judgement -> TacticsM () -> RuleM (Synthesized (LHsExpr GhcPs))
subgoalWith :: Judgement
-> TacticsM ()
-> RuleT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     (Synthesized (LHsExpr GhcPs))
subgoalWith Judgement
jdg TacticsM ()
t = ProofStateT
  (Synthesized (LHsExpr GhcPs))
  (Synthesized (LHsExpr GhcPs))
  TacticError
  TacticState
  ExtractM
  Judgement
-> RuleT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     (Synthesized (LHsExpr GhcPs))
forall jdg ext err s (m :: * -> *) a.
ProofStateT ext a err s m jdg -> RuleT jdg ext err s m a
RuleT (ProofStateT
   (Synthesized (LHsExpr GhcPs))
   (Synthesized (LHsExpr GhcPs))
   TacticError
   TacticState
   ExtractM
   Judgement
 -> RuleT
      Judgement
      (Synthesized (LHsExpr GhcPs))
      TacticError
      TacticState
      ExtractM
      (Synthesized (LHsExpr GhcPs)))
-> ProofStateT
     (Synthesized (LHsExpr GhcPs))
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     Judgement
-> RuleT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     (Synthesized (LHsExpr GhcPs))
forall a b. (a -> b) -> a -> b
$ (StateT
   Judgement
   (ProofStateT
      (Synthesized (LHsExpr GhcPs))
      (Synthesized (LHsExpr GhcPs))
      TacticError
      TacticState
      ExtractM)
   ()
 -> Judgement
 -> ProofStateT
      (Synthesized (LHsExpr GhcPs))
      (Synthesized (LHsExpr GhcPs))
      TacticError
      TacticState
      ExtractM
      Judgement)
-> Judgement
-> StateT
     Judgement
     (ProofStateT
        (Synthesized (LHsExpr GhcPs))
        (Synthesized (LHsExpr GhcPs))
        TacticError
        TacticState
        ExtractM)
     ()
-> ProofStateT
     (Synthesized (LHsExpr GhcPs))
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     Judgement
forall a b c. (a -> b -> c) -> b -> a -> c
flip StateT
  Judgement
  (ProofStateT
     (Synthesized (LHsExpr GhcPs))
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM)
  ()
-> Judgement
-> ProofStateT
     (Synthesized (LHsExpr GhcPs))
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     Judgement
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m s
execStateT Judgement
jdg (StateT
   Judgement
   (ProofStateT
      (Synthesized (LHsExpr GhcPs))
      (Synthesized (LHsExpr GhcPs))
      TacticError
      TacticState
      ExtractM)
   ()
 -> ProofStateT
      (Synthesized (LHsExpr GhcPs))
      (Synthesized (LHsExpr GhcPs))
      TacticError
      TacticState
      ExtractM
      Judgement)
-> StateT
     Judgement
     (ProofStateT
        (Synthesized (LHsExpr GhcPs))
        (Synthesized (LHsExpr GhcPs))
        TacticError
        TacticState
        ExtractM)
     ()
-> ProofStateT
     (Synthesized (LHsExpr GhcPs))
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     Judgement
forall a b. (a -> b) -> a -> b
$ 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 ()
t