{-# LANGUAGE OverloadedStrings #-}

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

import           ConLike (ConLike(RealDataCon))
import           Control.Applicative (Alternative(empty))
import           Control.Lens ((&), (%~), (<>~))
import           Control.Monad (unless)
import           Control.Monad.Except (throwError)
import           Control.Monad.Reader.Class (MonadReader (ask))
import           Control.Monad.State.Strict (StateT(..), runStateT, gets)
import           Data.Bool (bool)
import           Data.Foldable
import           Data.Functor ((<&>))
import           Data.Generics.Labels ()
import           Data.List
import qualified Data.Map as M
import           Data.Maybe
import           Data.Set (Set)
import qualified Data.Set as S
import           DataCon
import           Development.IDE.GHC.Compat
import           GHC.Exts
import           GHC.SourceGen ((@@))
import           GHC.SourceGen.Expr
import           Name (occNameString, occName)
import           OccName (mkVarOcc)
import           Refinery.Tactic
import           Refinery.Tactic.Internal
import           TcType
import           Type hiding (Var)
import           TysPrim (betaTy, alphaTy, betaTyVar, alphaTyVar)
import           Wingman.CodeGen
import           Wingman.Context
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
          }
    Maybe (HyInfo CType)
Nothing -> TacticError
-> RuleT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     (Synthesized (LHsExpr GhcPs))
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (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
$ OccName -> TacticError
UndefinedHypothesis OccName
name


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 <- TacticT
  Judgement
  (Synthesized (LHsExpr GhcPs))
  TacticError
  TacticState
  ExtractM
  [(OccName, CType)]
forall (m :: * -> *). MonadReader Context m => m [(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
    -- Peek allows us to look at the extract produced by this block.
    (Synthesized (LHsExpr GhcPs) -> TacticsM ()) -> TacticsM ()
forall ext jdg err s (m :: * -> *).
(ext -> TacticT jdg ext err s m ()) -> TacticT jdg ext err s m ()
peek ((Synthesized (LHsExpr GhcPs) -> TacticsM ()) -> TacticsM ())
-> (Synthesized (LHsExpr GhcPs) -> TacticsM ()) -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ \Synthesized (LHsExpr GhcPs)
ext -> 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 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.
      Bool -> TacticsM () -> TacticsM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ((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) TacticsM ()
forall (f :: * -> *) a. Alternative f => f a
empty

    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 (HyInfo CType -> TacticsM ()
apply (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..]


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)
-> TacticT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     [(OccName, CType)]
-> TacticT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     OccName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TacticT
  Judgement
  (Synthesized (LHsExpr GhcPs))
  TacticError
  TacticState
  ExtractM
  [(OccName, CType)]
forall (m :: * -> *). MonadReader Context m => m [(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 = Maybe [OccName] -> TacticsM ()
intros' Maybe [OccName]
forall a. Maybe a
Nothing

------------------------------------------------------------------------------
-- | Introduce a lambda binding every variable.
intros'
    :: Maybe [OccName]  -- ^ When 'Nothing', generate a new name for every
                        -- variable. Otherwise, only bind the variables named.
    -> TacticsM ()
intros' :: Maybe [OccName] -> TacticsM ()
intros' Maybe [OccName]
names = (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
_) -> TacticError
-> RuleT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     (Synthesized (LHsExpr GhcPs))
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (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
"intros" CType
g
    ([TyVar]
_, ThetaType
_, ThetaType
as, Type
b) -> do
      Context
ctx <- RuleT
  Judgement
  (Synthesized (LHsExpr GhcPs))
  TacticError
  TacticState
  ExtractM
  Context
forall r (m :: * -> *). MonadReader r m => m r
ask
      let vs :: [OccName]
vs = [OccName] -> Maybe [OccName] -> [OccName]
forall a. a -> Maybe a -> a
fromMaybe (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
as) Maybe [OccName]
names
          num_args :: Int
num_args = [OccName] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [OccName]
vs
          top_hole :: Maybe OccName
top_hole = Context -> Judgement -> Maybe OccName
forall a. Context -> Judgement' a -> Maybe OccName
isTopHole Context
ctx Judgement
jdg
          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)] -> Hypothesis CType)
-> [(OccName, CType)] -> Hypothesis CType
forall a b. (a -> b) -> a -> b
$ [OccName] -> [CType] -> [(OccName, CType)]
forall a b. [a] -> [b] -> [(a, b)]
zip [OccName]
vs ([CType] -> [(OccName, CType)]) -> [CType] -> [(OccName, CType)]
forall a b. (a -> b) -> a -> b
$ ThetaType -> [CType]
coerce ThetaType
as
          jdg' :: Judgement
jdg' = Context -> Hypothesis CType -> Judgement -> Judgement
introduce Context
ctx Hypothesis CType
hy'
               (Judgement -> Judgement) -> Judgement -> Judgement
forall a b. (a -> b) -> a -> b
$ CType -> Judgement -> Judgement
forall a. a -> Judgement' a -> Judgement' a
withNewGoal (Type -> CType
CType (Type -> CType) -> Type -> CType
forall a b. (a -> b) -> a -> b
$ ThetaType -> Type -> Type
mkFunTys' (Int -> ThetaType -> ThetaType
forall a. Int -> [a] -> [a]
drop Int
num_args ThetaType
as) Type
b) 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]
vs) 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]
vs) (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


------------------------------------------------------------------------------
-- | 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 ext (m :: * -> *) jdg err s.
MonadExtract ext 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 = TacticsM () -> TacticsM ()
forall a. TacticsM a -> TacticsM a
requireConcreteHole (TacticsM () -> TacticsM ())
-> (HyInfo CType -> TacticsM ()) -> HyInfo CType -> 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 ())
-> (HyInfo CType -> TacticsM ()) -> HyInfo CType -> TacticsM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (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 ())
-> (HyInfo CType
    -> Judgement
    -> RuleT
         Judgement
         (Synthesized (LHsExpr GhcPs))
         TacticError
         TacticState
         ExtractM
         (Synthesized (LHsExpr GhcPs)))
-> HyInfo CType
-> TacticsM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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)


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


apply :: HyInfo CType -> TacticsM ()
apply :: HyInfo CType -> TacticsM ()
apply HyInfo CType
hi = String -> TacticsM () -> TacticsM ()
forall (m :: * -> *) jdg ext err s a.
Functor m =>
String
-> TacticT jdg (Synthesized ext) err s m a
-> TacticT jdg (Synthesized ext) err s m a
tracing (String
"apply' " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> OccName -> String
forall a. Show a => a -> String
show (HyInfo CType -> OccName
forall a. HyInfo a -> OccName
hi_name HyInfo CType
hi)) (TacticsM () -> TacticsM ()) -> TacticsM () -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ do
  Judgement
jdg <- TacticT
  Judgement
  (Synthesized (LHsExpr GhcPs))
  TacticError
  TacticState
  ExtractM
  Judgement
forall (m :: * -> *) jdg ext err s.
Functor m =>
TacticT jdg ext err s m jdg
goal
  let g :: CType
g  = Judgement -> CType
forall a. Judgement' a -> a
jGoal Judgement
jdg
      ty :: Type
ty = CType -> Type
unCType (CType -> Type) -> CType -> Type
forall a b. (a -> b) -> a -> b
$ HyInfo CType -> CType
forall a. HyInfo a -> a
hi_type HyInfo CType
hi
      func :: OccName
func = HyInfo CType -> OccName
forall a. HyInfo a -> OccName
hi_name HyInfo CType
hi
  Type
ty' <- Type
-> TacticT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     Type
forall (m :: * -> *). MonadState TacticState m => Type -> m Type
freshTyvars Type
ty
  let ([TyVar]
_, ThetaType
_, ThetaType
args, Type
ret) = Type -> ([TyVar], ThetaType, ThetaType, Type)
tacticsSplitFunTy Type
ty'
  (Judgement
 -> RuleT
      Judgement
      (Synthesized (LHsExpr GhcPs))
      TacticError
      TacticState
      ExtractM
      (Synthesized (LHsExpr GhcPs)))
-> TacticsM ()
forall (m :: * -> *) jdg ext err s.
Monad m =>
(jdg -> RuleT jdg ext err s m ext) -> TacticT jdg ext err s m ()
rule ((Judgement
  -> RuleT
       Judgement
       (Synthesized (LHsExpr GhcPs))
       TacticError
       TacticState
       ExtractM
       (Synthesized (LHsExpr GhcPs)))
 -> TacticsM ())
-> (Judgement
    -> RuleT
         Judgement
         (Synthesized (LHsExpr GhcPs))
         TacticError
         TacticState
         ExtractM
         (Synthesized (LHsExpr GhcPs)))
-> TacticsM ()
forall a b. (a -> b) -> a -> b
$ \Judgement
jdg -> do
    CType -> CType -> RuleM ()
unify CType
g (Type -> CType
CType Type
ret)
    Synthesized [LHsExpr GhcPs]
ext
        <- ([Synthesized (LHsExpr GhcPs)] -> Synthesized [LHsExpr GhcPs])
-> RuleT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     [Synthesized (LHsExpr GhcPs)]
-> RuleT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     (Synthesized [LHsExpr GhcPs])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [Synthesized (LHsExpr GhcPs)] -> Synthesized [LHsExpr GhcPs]
forall a. [Synthesized a] -> Synthesized [a]
unzipTrace
        (RuleT
   Judgement
   (Synthesized (LHsExpr GhcPs))
   TacticError
   TacticState
   ExtractM
   [Synthesized (LHsExpr GhcPs)]
 -> RuleT
      Judgement
      (Synthesized (LHsExpr GhcPs))
      TacticError
      TacticState
      ExtractM
      (Synthesized [LHsExpr GhcPs]))
-> RuleT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     [Synthesized (LHsExpr GhcPs)]
-> RuleT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     (Synthesized [LHsExpr GhcPs])
forall a b. (a -> b) -> a -> b
$ (Type
 -> RuleT
      Judgement
      (Synthesized (LHsExpr GhcPs))
      TacticError
      TacticState
      ExtractM
      (Synthesized (LHsExpr GhcPs)))
-> ThetaType
-> RuleT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     [Synthesized (LHsExpr GhcPs)]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse ( Judgement
-> RuleT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     (Synthesized (LHsExpr GhcPs))
newSubgoal
                    (Judgement
 -> RuleT
      Judgement
      (Synthesized (LHsExpr GhcPs))
      TacticError
      TacticState
      ExtractM
      (Synthesized (LHsExpr GhcPs)))
-> (Type -> Judgement)
-> Type
-> RuleT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     (Synthesized (LHsExpr GhcPs))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Judgement -> Judgement
blacklistingDestruct
                    (Judgement -> Judgement)
-> (Type -> Judgement) -> Type -> Judgement
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (CType -> Judgement -> Judgement)
-> Judgement -> CType -> Judgement
forall a b c. (a -> b -> c) -> b -> a -> c
flip CType -> Judgement -> Judgement
forall a. a -> Judgement' a -> Judgement' a
withNewGoal Judgement
jdg
                    (CType -> Judgement) -> (Type -> CType) -> Type -> Judgement
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> CType
CType
                    ) ThetaType
args
    Synthesized (LHsExpr GhcPs)
-> 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
%~ OccName -> Set OccName -> Set OccName
forall a. Ord a => a -> Set a -> Set a
S.insert 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 ()
apply


------------------------------------------------------------------------------
-- | 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 e (m :: * -> *) a. MonadError e m => e -> m a
throwError (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 e (m :: * -> *) a. MonadError e m => e -> m a
throwError (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 e (m :: * -> *) a. MonadError e m => e -> m a
throwError (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 ext (m :: * -> *) jdg err s.
MonadExtract ext 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 ext (m :: * -> *) jdg err s.
MonadExtract ext 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 -> TacticError
-> RuleT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     (Synthesized (LHsExpr GhcPs))
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (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
"splitDataCon" CType
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 <- (TacticState -> TCvSubst)
-> TacticT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     TCvSubst
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets TacticState -> TCvSubst
ts_unifier
    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 e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TacticError -> TacticsM ()) -> TacticError -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ OccName -> TacticError
NotInScope OccName
occ
    Maybe (TyCon, ThetaType)
Nothing -> TacticError -> TacticsM ()
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (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
s -> a -> TacticsM ()
tac a
s) ([a] -> [TacticsM ()])
-> (Judgement -> [a]) -> Judgement -> [TacticsM ()]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Judgement -> [a]
getNames)


localTactic :: TacticsM a -> (Judgement -> Judgement) -> TacticsM a
localTactic :: TacticsM a -> (Judgement -> Judgement) -> TacticsM a
localTactic TacticsM a
t Judgement -> Judgement
f = do
  StateT
  Judgement
  (ProofStateT
     (Synthesized (LHsExpr GhcPs))
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM)
  a
-> TacticsM a
forall jdg ext err s (m :: * -> *) a.
StateT jdg (ProofStateT ext ext err s m) a
-> TacticT jdg ext err s m a
TacticT (StateT
   Judgement
   (ProofStateT
      (Synthesized (LHsExpr GhcPs))
      (Synthesized (LHsExpr GhcPs))
      TacticError
      TacticState
      ExtractM)
   a
 -> TacticsM a)
-> StateT
     Judgement
     (ProofStateT
        (Synthesized (LHsExpr GhcPs))
        (Synthesized (LHsExpr GhcPs))
        TacticError
        TacticState
        ExtractM)
     a
-> TacticsM a
forall a b. (a -> b) -> a -> b
$ (Judgement
 -> ProofStateT
      (Synthesized (LHsExpr GhcPs))
      (Synthesized (LHsExpr GhcPs))
      TacticError
      TacticState
      ExtractM
      (a, Judgement))
-> StateT
     Judgement
     (ProofStateT
        (Synthesized (LHsExpr GhcPs))
        (Synthesized (LHsExpr GhcPs))
        TacticError
        TacticState
        ExtractM)
     a
forall s (m :: * -> *) a. (s -> m (a, s)) -> StateT s m a
StateT ((Judgement
  -> ProofStateT
       (Synthesized (LHsExpr GhcPs))
       (Synthesized (LHsExpr GhcPs))
       TacticError
       TacticState
       ExtractM
       (a, Judgement))
 -> StateT
      Judgement
      (ProofStateT
         (Synthesized (LHsExpr GhcPs))
         (Synthesized (LHsExpr GhcPs))
         TacticError
         TacticState
         ExtractM)
      a)
-> (Judgement
    -> ProofStateT
         (Synthesized (LHsExpr GhcPs))
         (Synthesized (LHsExpr GhcPs))
         TacticError
         TacticState
         ExtractM
         (a, Judgement))
-> StateT
     Judgement
     (ProofStateT
        (Synthesized (LHsExpr GhcPs))
        (Synthesized (LHsExpr GhcPs))
        TacticError
        TacticState
        ExtractM)
     a
forall a b. (a -> b) -> a -> b
$ \Judgement
jdg ->
    StateT
  Judgement
  (ProofStateT
     (Synthesized (LHsExpr GhcPs))
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM)
  a
-> Judgement
-> ProofStateT
     (Synthesized (LHsExpr GhcPs))
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     (a, Judgement)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT (TacticsM a
-> StateT
     Judgement
     (ProofStateT
        (Synthesized (LHsExpr GhcPs))
        (Synthesized (LHsExpr GhcPs))
        TacticError
        TacticState
        ExtractM)
     a
forall jdg ext err s (m :: * -> *) a.
TacticT jdg ext err s m a
-> StateT jdg (ProofStateT ext ext err s m) a
unTacticT TacticsM a
t) (Judgement
 -> ProofStateT
      (Synthesized (LHsExpr GhcPs))
      (Synthesized (LHsExpr GhcPs))
      TacticError
      TacticState
      ExtractM
      (a, Judgement))
-> Judgement
-> ProofStateT
     (Synthesized (LHsExpr GhcPs))
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     (a, Judgement)
forall a b. (a -> b) -> a -> b
$ Judgement -> Judgement
f Judgement
jdg


refine :: TacticsM ()
refine :: TacticsM ()
refine = TacticsM ()
intros TacticsM () -> TacticsM () -> TacticsM ()
forall jdg ext err s (m :: * -> *) a.
TacticT jdg ext err s m a
-> TacticT jdg ext err s m a -> TacticT jdg ext err s m a
<%> TacticsM ()
splitSingle


auto' :: Int -> TacticsM ()
auto' :: Int -> TacticsM ()
auto' Int
0 = TacticError -> TacticsM ()
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError TacticError
NoProgress
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 ()] -> 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
$ HyInfo CType -> TacticsM ()
apply 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 ()
assumption 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
      HyInfo CType -> TacticsM ()
apply (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 e (m :: * -> *) a. MonadError e m => e -> m a
throwError (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  -> HyInfo CType -> TacticsM ()
apply 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
                    ) 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 =
  Type -> TacticsM ()
applyByType (Type -> TacticsM ()) -> Type -> TacticsM ()
forall a b. (a -> b) -> a -> b
$
    [TyVar] -> Type -> Type
mkInvForAllTys [TyVar
alphaTyVar, TyVar
betaTyVar] (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$
      ThetaType -> Type -> Type
mkFunTys' (Int -> Type -> ThetaType
forall a. Int -> a -> [a]
replicate Int
n Type
alphaTy) Type
betaTy

self :: TacticsM ()
self :: TacticsM ()
self =
  ([(OccName, CType)] -> Maybe (OccName, CType))
-> TacticT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     [(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 TacticT
  Judgement
  (Synthesized (LHsExpr GhcPs))
  TacticError
  TacticState
  ExtractM
  [(OccName, CType)]
forall (m :: * -> *). MonadReader Context m => m [(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 HyInfo CType -> TacticsM ()
apply OccName
self
    Maybe (OccName, CType)
Nothing -> TacticError -> TacticsM ()
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TacticError -> TacticsM ()) -> TacticError -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ String -> TacticError
TacticPanic String
"no defining function"


cata :: HyInfo CType -> TacticsM ()
cata :: HyInfo CType -> TacticsM ()
cata HyInfo CType
hi = do
  Hypothesis CType
diff <- TacticsM () -> TacticsM (Hypothesis CType)
hyDiff (TacticsM () -> TacticsM (Hypothesis CType))
-> TacticsM () -> TacticsM (Hypothesis CType)
forall a b. (a -> b) -> a -> b
$ HyInfo CType -> TacticsM ()
destruct 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
$
    (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 (HyInfo CType -> TacticsM ()
apply HyInfo CType
hi) TacticsM ()
assumption)
      Hypothesis CType
diff

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


------------------------------------------------------------------------------
-- | Determine the difference in hypothesis due to running a tactic. Also, it
-- runs the tactic.
hyDiff :: TacticsM () -> TacticsM (Hypothesis CType)
hyDiff :: TacticsM () -> TacticsM (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 -> TacticsM (Hypothesis CType)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Hypothesis CType -> TacticsM (Hypothesis CType))
-> Hypothesis CType -> TacticsM (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'