{-# LANGUAGE TupleSections #-}
{-# LANGUAGE FlexibleContexts      #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ViewPatterns          #-}

module Ide.Plugin.Tactic.Tactics
  ( module Ide.Plugin.Tactic.Tactics
  , runTactic
  ) where

import           Control.Monad (when)
import           Control.Monad.Except (throwError)
import           Control.Monad.Reader.Class (MonadReader(ask))
import           Control.Monad.State.Class
import           Control.Monad.State.Strict (StateT(..), runStateT)
import           Data.Bool (bool)
import           Data.Foldable
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.Expr
import           GHC.SourceGen.Overloaded
import           Ide.Plugin.Tactic.CodeGen
import           Ide.Plugin.Tactic.Context
import           Ide.Plugin.Tactic.GHC
import           Ide.Plugin.Tactic.Judgements
import           Ide.Plugin.Tactic.Machinery
import           Ide.Plugin.Tactic.Naming
import           Ide.Plugin.Tactic.Types
import           Name (occNameString)
import           Refinery.Tactic
import           Refinery.Tactic.Internal
import           TcType
import           Type hiding (Var)


------------------------------------------------------------------------------
-- | 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
      (Trace, LHsExpr GhcPs)
      TacticError
      TacticState
      ExtractM
      (Trace, 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
       (Trace, LHsExpr GhcPs)
       TacticError
       TacticState
       ExtractM
       (Trace, LHsExpr GhcPs))
 -> TacticsM ())
-> (Judgement
    -> RuleT
         Judgement
         (Trace, LHsExpr GhcPs)
         TacticError
         TacticState
         ExtractM
         (Trace, 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 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
      Maybe PatVal -> (PatVal -> RuleM ()) -> RuleM ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
t a -> (a -> f b) -> f ()
for_ (OccName -> Map OccName PatVal -> Maybe PatVal
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup OccName
name (Map OccName PatVal -> Maybe PatVal)
-> Map OccName PatVal -> Maybe PatVal
forall a b. (a -> b) -> a -> b
$ Judgement -> Map OccName PatVal
forall a. Judgement' a -> Map OccName PatVal
jPatHypothesis Judgement
jdg) PatVal -> RuleM ()
forall (m :: * -> *). MonadState TacticState m => PatVal -> m ()
markStructuralySmallerRecursion
      Judgement -> OccName -> RuleM ()
forall (m :: * -> *).
MonadState TacticState m =>
Judgement -> OccName -> m ()
useOccName Judgement
jdg OccName
name
      (Trace, LHsExpr GhcPs)
-> RuleT
     Judgement
     (Trace, LHsExpr GhcPs)
     TacticError
     TacticState
     ExtractM
     (Trace, LHsExpr GhcPs)
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((Trace, LHsExpr GhcPs)
 -> RuleT
      Judgement
      (Trace, LHsExpr GhcPs)
      TacticError
      TacticState
      ExtractM
      (Trace, LHsExpr GhcPs))
-> (Trace, LHsExpr GhcPs)
-> RuleT
     Judgement
     (Trace, LHsExpr GhcPs)
     TacticError
     TacticState
     ExtractM
     (Trace, LHsExpr GhcPs)
forall a b. (a -> b) -> a -> b
$ (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, ) (LHsExpr GhcPs -> (Trace, LHsExpr GhcPs))
-> LHsExpr GhcPs -> (Trace, LHsExpr GhcPs)
forall a b. (a -> b) -> a -> b
$ 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
    Maybe (HyInfo CType)
Nothing -> TacticError
-> RuleT
     Judgement
     (Trace, LHsExpr GhcPs)
     TacticError
     TacticState
     ExtractM
     (Trace, LHsExpr GhcPs)
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TacticError
 -> RuleT
      Judgement
      (Trace, LHsExpr GhcPs)
      TacticError
      TacticState
      ExtractM
      (Trace, LHsExpr GhcPs))
-> TacticError
-> RuleT
     Judgement
     (Trace, LHsExpr GhcPs)
     TacticError
     TacticState
     ExtractM
     (Trace, LHsExpr GhcPs)
forall a b. (a -> b) -> a -> b
$ OccName -> TacticError
UndefinedHypothesis OccName
name


recursion :: TacticsM ()
recursion :: TacticsM ()
recursion = TacticsM () -> TacticsM ()
forall a. TacticsM a -> TacticsM a
requireConcreteHole (TacticsM () -> TacticsM ()) -> TacticsM () -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ String -> TacticsM () -> TacticsM ()
forall (m :: * -> *) jdg ext err s a.
Functor m =>
String
-> TacticT jdg (Trace, ext) err s m a
-> TacticT jdg (Trace, 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
  (Trace, 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) -> do
    (TacticState -> TacticState) -> TacticsM ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((TacticState -> TacticState) -> TacticsM ())
-> (TacticState -> TacticState) -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ TacticState -> TacticState
pushRecursionStack (TacticState -> TacticState)
-> (TacticState -> TacticState) -> TacticState -> TacticState
forall b c a. (b -> c) -> (a -> b) -> a -> c
.  TacticState -> TacticState
countRecursiveCall
    (TacticState -> Maybe TacticError)
-> (TacticState -> TacticState) -> TacticsM () -> TacticsM ()
forall (m :: * -> *) s err jdg ext.
Monad m =>
(s -> Maybe err)
-> (s -> s)
-> TacticT jdg ext err s m ()
-> TacticT jdg ext err s m ()
ensure TacticState -> Maybe TacticError
guardStructurallySmallerRecursion TacticState -> TacticState
popRecursionStack (TacticsM () -> TacticsM ()) -> TacticsM () -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ do
      (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) ((Judgement -> Judgement) -> TacticsM ())
-> (Judgement -> Judgement) -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ [(OccName, CType)] -> Judgement -> Judgement
forall a. [(OccName, a)] -> Judgement' a -> Judgement' a
introducingRecursively [(OccName, CType)]
defs)
        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..]


------------------------------------------------------------------------------
-- | Introduce a lambda binding every variable.
intros :: TacticsM ()
intros :: TacticsM ()
intros = (Judgement
 -> RuleT
      Judgement
      (Trace, LHsExpr GhcPs)
      TacticError
      TacticState
      ExtractM
      (Trace, 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
       (Trace, LHsExpr GhcPs)
       TacticError
       TacticState
       ExtractM
       (Trace, LHsExpr GhcPs))
 -> TacticsM ())
-> (Judgement
    -> RuleT
         Judgement
         (Trace, LHsExpr GhcPs)
         TacticError
         TacticState
         ExtractM
         (Trace, LHsExpr GhcPs))
-> TacticsM ()
forall a b. (a -> b) -> a -> b
$ \Judgement
jdg -> do
  let hy :: Hypothesis CType
hy = Judgement -> Hypothesis CType
forall a. Judgement' a -> Hypothesis a
jHypothesis Judgement
jdg
      g :: CType
g  = Judgement -> CType
forall a. Judgement' a -> a
jGoal Judgement
jdg
  Context
ctx <- RuleT
  Judgement
  (Trace, LHsExpr GhcPs)
  TacticError
  TacticState
  ExtractM
  Context
forall r (m :: * -> *). MonadReader r m => m r
ask
  case Type -> ([Type], Type)
tcSplitFunTys (Type -> ([Type], Type)) -> Type -> ([Type], Type)
forall a b. (a -> b) -> a -> b
$ CType -> Type
unCType CType
g of
    ([], Type
_) -> TacticError
-> RuleT
     Judgement
     (Trace, LHsExpr GhcPs)
     TacticError
     TacticState
     ExtractM
     (Trace, LHsExpr GhcPs)
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TacticError
 -> RuleT
      Judgement
      (Trace, LHsExpr GhcPs)
      TacticError
      TacticState
      ExtractM
      (Trace, LHsExpr GhcPs))
-> TacticError
-> RuleT
     Judgement
     (Trace, LHsExpr GhcPs)
     TacticError
     TacticState
     ExtractM
     (Trace, LHsExpr GhcPs)
forall a b. (a -> b) -> a -> b
$ String -> CType -> TacticError
GoalMismatch String
"intros" CType
g
    ([Type]
as, Type
b) -> do
      [OccName]
vs <- Set OccName
-> [Type]
-> RuleT
     Judgement
     (Trace, LHsExpr GhcPs)
     TacticError
     TacticState
     ExtractM
     [OccName]
forall (t :: * -> *) (m :: * -> *).
(Traversable t, Monad m) =>
Set OccName -> t Type -> m (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) [Type]
as
      let top_hole :: Maybe OccName
top_hole = Context -> Judgement -> Maybe OccName
forall a. Context -> Judgement' a -> Maybe OccName
isTopHole Context
ctx Judgement
jdg
          jdg' :: Judgement
jdg' = Maybe OccName -> [(OccName, CType)] -> Judgement -> Judgement
forall a.
Maybe OccName -> [(OccName, a)] -> Judgement' a -> Judgement' a
introducingLambda Maybe OccName
top_hole ([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
$ [Type] -> [CType]
coerce [Type]
as)
               (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
b) Judgement
jdg
      (TacticState -> TacticState) -> RuleM ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((TacticState -> TacticState) -> RuleM ())
-> (TacticState -> TacticState) -> RuleM ()
forall a b. (a -> b) -> a -> b
$ (Set OccName -> Set OccName) -> TacticState -> TacticState
withIntroducedVals ((Set OccName -> Set OccName) -> TacticState -> TacticState)
-> (Set OccName -> Set OccName) -> TacticState -> TacticState
forall a b. (a -> b) -> a -> b
$ Set OccName -> Set OccName -> Set OccName
forall a. Monoid a => a -> a -> a
mappend (Set OccName -> Set OccName -> Set OccName)
-> Set OccName -> Set OccName -> Set OccName
forall a b. (a -> b) -> a -> b
$ [OccName] -> Set OccName
forall a. Ord a => [a] -> Set a
S.fromList [OccName]
vs
      Bool -> RuleM () -> RuleM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Maybe OccName -> Bool
forall a. Maybe a -> Bool
isJust Maybe OccName
top_hole) (RuleM () -> RuleM ()) -> RuleM () -> RuleM ()
forall a b. (a -> b) -> a -> b
$ Set OccName -> RuleM ()
forall (m :: * -> *).
MonadState TacticState m =>
Set OccName -> m ()
addUnusedTopVals (Set OccName -> RuleM ()) -> Set OccName -> RuleM ()
forall a b. (a -> b) -> a -> b
$ [OccName] -> Set OccName
forall a. Ord a => [a] -> Set a
S.fromList [OccName]
vs
      (Trace
tr, LHsExpr GhcPs
sg) <- Judgement
-> RuleT
     Judgement
     (Trace, LHsExpr GhcPs)
     TacticError
     TacticState
     ExtractM
     (Trace, LHsExpr GhcPs)
newSubgoal Judgement
jdg'
      (Trace, LHsExpr GhcPs)
-> RuleT
     Judgement
     (Trace, LHsExpr GhcPs)
     TacticError
     TacticState
     ExtractM
     (Trace, LHsExpr GhcPs)
forall (f :: * -> *) a. Applicative f => a -> f a
pure
        ((Trace, LHsExpr GhcPs)
 -> RuleT
      Judgement
      (Trace, LHsExpr GhcPs)
      TacticError
      TacticState
      ExtractM
      (Trace, LHsExpr GhcPs))
-> (HsExpr GhcPs -> (Trace, LHsExpr GhcPs))
-> HsExpr GhcPs
-> RuleT
     Judgement
     (Trace, LHsExpr GhcPs)
     TacticError
     TacticState
     ExtractM
     (Trace, LHsExpr GhcPs)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (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
forall a b. (a -> b) -> a -> b
$ Trace -> [Trace]
forall (f :: * -> *) a. Applicative f => a -> f a
pure Trace
tr, )
        (LHsExpr GhcPs -> (Trace, LHsExpr GhcPs))
-> (HsExpr GhcPs -> LHsExpr GhcPs)
-> HsExpr GhcPs
-> (Trace, LHsExpr GhcPs)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HsExpr GhcPs -> LHsExpr GhcPs
forall a. HasSrcSpan a => SrcSpanLess a -> a
noLoc
        (HsExpr GhcPs -> LHsExpr GhcPs)
-> (HsExpr GhcPs -> HsExpr GhcPs) -> HsExpr 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
 -> RuleT
      Judgement
      (Trace, LHsExpr GhcPs)
      TacticError
      TacticState
      ExtractM
      (Trace, LHsExpr GhcPs))
-> HsExpr GhcPs
-> RuleT
     Judgement
     (Trace, LHsExpr GhcPs)
     TacticError
     TacticState
     ExtractM
     (Trace, LHsExpr GhcPs)
forall a b. (a -> b) -> a -> b
$ LHsExpr GhcPs -> SrcSpanLess (LHsExpr GhcPs)
forall a. HasSrcSpan a => a -> SrcSpanLess a
unLoc LHsExpr GhcPs
sg


------------------------------------------------------------------------------
-- | 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 (Trace, ext) err s m a
-> TacticT jdg (Trace, 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
  (Trace, 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 = (Judgement
 -> RuleT
      Judgement
      (Trace, LHsExpr GhcPs)
      TacticError
      TacticState
      ExtractM
      (Trace, 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
       (Trace, LHsExpr GhcPs)
       TacticError
       TacticState
       ExtractM
       (Trace, LHsExpr GhcPs))
 -> TacticsM ())
-> (Judgement
    -> RuleT
         Judgement
         (Trace, LHsExpr GhcPs)
         TacticError
         TacticState
         ExtractM
         (Trace, LHsExpr GhcPs))
-> TacticsM ()
forall a b. (a -> b) -> a -> b
$ (DataCon
 -> Judgement
 -> RuleT
      Judgement
      (Trace, LHsExpr GhcPs)
      TacticError
      TacticState
      ExtractM
      (Trace, LHsExpr GhcPs))
-> HyInfo CType
-> Judgement
-> RuleT
     Judgement
     (Trace, LHsExpr GhcPs)
     TacticError
     TacticState
     ExtractM
     (Trace, LHsExpr GhcPs)
destruct' ((Judgement
 -> RuleT
      Judgement
      (Trace, LHsExpr GhcPs)
      TacticError
      TacticState
      ExtractM
      (Trace, LHsExpr GhcPs))
-> DataCon
-> Judgement
-> RuleT
     Judgement
     (Trace, LHsExpr GhcPs)
     TacticError
     TacticState
     ExtractM
     (Trace, LHsExpr GhcPs)
forall a b. a -> b -> a
const Judgement
-> RuleT
     Judgement
     (Trace, LHsExpr GhcPs)
     TacticError
     TacticState
     ExtractM
     (Trace, LHsExpr GhcPs)
forall jdg ext (m :: * -> *). MonadRule jdg ext m => jdg -> m ext
subgoal) 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


------------------------------------------------------------------------------
-- | 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 (Trace, ext) err s m a
-> TacticT jdg (Trace, ext) err s m a
tracing String
"destruct(user)" (TacticsM () -> TacticsM ()) -> TacticsM () -> TacticsM ()
forall a b. (a -> b) -> a -> b
$
  (Judgement
 -> RuleT
      Judgement
      (Trace, LHsExpr GhcPs)
      TacticError
      TacticState
      ExtractM
      (Trace, 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
       (Trace, LHsExpr GhcPs)
       TacticError
       TacticState
       ExtractM
       (Trace, LHsExpr GhcPs))
 -> TacticsM ())
-> (Judgement
    -> RuleT
         Judgement
         (Trace, LHsExpr GhcPs)
         TacticError
         TacticState
         ExtractM
         (Trace, LHsExpr GhcPs))
-> TacticsM ()
forall a b. (a -> b) -> a -> b
$ (DataCon
 -> Judgement
 -> RuleT
      Judgement
      (Trace, LHsExpr GhcPs)
      TacticError
      TacticState
      ExtractM
      (Trace, LHsExpr GhcPs))
-> HyInfo CType
-> Judgement
-> RuleT
     Judgement
     (Trace, LHsExpr GhcPs)
     TacticError
     TacticState
     ExtractM
     (Trace, LHsExpr GhcPs)
destruct' ((Judgement
 -> RuleT
      Judgement
      (Trace, LHsExpr GhcPs)
      TacticError
      TacticState
      ExtractM
      (Trace, LHsExpr GhcPs))
-> DataCon
-> Judgement
-> RuleT
     Judgement
     (Trace, LHsExpr GhcPs)
     TacticError
     TacticState
     ExtractM
     (Trace, LHsExpr GhcPs)
forall a b. a -> b -> a
const Judgement
-> RuleT
     Judgement
     (Trace, LHsExpr GhcPs)
     TacticError
     TacticState
     ExtractM
     (Trace, LHsExpr GhcPs)
forall jdg ext (m :: * -> *). MonadRule jdg ext m => jdg -> m ext
subgoal) 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 (Trace, ext) err s m a
-> TacticT jdg (Trace, 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
      (Trace, LHsExpr GhcPs)
      TacticError
      TacticState
      ExtractM
      (Trace, 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
       (Trace, LHsExpr GhcPs)
       TacticError
       TacticState
       ExtractM
       (Trace, LHsExpr GhcPs))
 -> TacticsM ())
-> (HyInfo CType
    -> Judgement
    -> RuleT
         Judgement
         (Trace, LHsExpr GhcPs)
         TacticError
         TacticState
         ExtractM
         (Trace, LHsExpr GhcPs))
-> HyInfo CType
-> TacticsM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (DataCon
 -> Judgement
 -> RuleT
      Judgement
      (Trace, LHsExpr GhcPs)
      TacticError
      TacticState
      ExtractM
      (Trace, LHsExpr GhcPs))
-> HyInfo CType
-> Judgement
-> RuleT
     Judgement
     (Trace, LHsExpr GhcPs)
     TacticError
     TacticState
     ExtractM
     (Trace, LHsExpr GhcPs)
destruct' (\DataCon
dc Judgement
jdg ->
  Judgement
-> DataCon
-> [Type]
-> RuleT
     Judgement
     (Trace, LHsExpr GhcPs)
     TacticError
     TacticState
     ExtractM
     (Trace, LHsExpr GhcPs)
buildDataCon Judgement
jdg DataCon
dc ([Type]
 -> RuleT
      Judgement
      (Trace, LHsExpr GhcPs)
      TacticError
      TacticState
      ExtractM
      (Trace, LHsExpr GhcPs))
-> [Type]
-> RuleT
     Judgement
     (Trace, LHsExpr GhcPs)
     TacticError
     TacticState
     ExtractM
     (Trace, LHsExpr GhcPs)
forall a b. (a -> b) -> a -> b
$ (Type, [Type]) -> [Type]
forall a b. (a, b) -> b
snd ((Type, [Type]) -> [Type]) -> (Type, [Type]) -> [Type]
forall a b. (a -> b) -> a -> b
$ Type -> (Type, [Type])
splitAppTys (Type -> (Type, [Type])) -> Type -> (Type, [Type])
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 (Trace, ext) err s m a
-> TacticT jdg (Trace, ext) err s m a
tracing String
"destructLambdaCase" (TacticsM () -> TacticsM ()) -> TacticsM () -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ (Judgement
 -> RuleT
      Judgement
      (Trace, LHsExpr GhcPs)
      TacticError
      TacticState
      ExtractM
      (Trace, 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
       (Trace, LHsExpr GhcPs)
       TacticError
       TacticState
       ExtractM
       (Trace, LHsExpr GhcPs))
 -> TacticsM ())
-> (Judgement
    -> RuleT
         Judgement
         (Trace, LHsExpr GhcPs)
         TacticError
         TacticState
         ExtractM
         (Trace, LHsExpr GhcPs))
-> TacticsM ()
forall a b. (a -> b) -> a -> b
$ (DataCon
 -> Judgement
 -> RuleT
      Judgement
      (Trace, LHsExpr GhcPs)
      TacticError
      TacticState
      ExtractM
      (Trace, LHsExpr GhcPs))
-> Judgement
-> RuleT
     Judgement
     (Trace, LHsExpr GhcPs)
     TacticError
     TacticState
     ExtractM
     (Trace, LHsExpr GhcPs)
destructLambdaCase' ((Judgement
 -> RuleT
      Judgement
      (Trace, LHsExpr GhcPs)
      TacticError
      TacticState
      ExtractM
      (Trace, LHsExpr GhcPs))
-> DataCon
-> Judgement
-> RuleT
     Judgement
     (Trace, LHsExpr GhcPs)
     TacticError
     TacticState
     ExtractM
     (Trace, LHsExpr GhcPs)
forall a b. a -> b -> a
const Judgement
-> RuleT
     Judgement
     (Trace, LHsExpr GhcPs)
     TacticError
     TacticState
     ExtractM
     (Trace, LHsExpr GhcPs)
forall jdg ext (m :: * -> *). MonadRule jdg ext m => jdg -> m ext
subgoal)


------------------------------------------------------------------------------
-- | 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 (Trace, ext) err s m a
-> TacticT jdg (Trace, ext) err s m a
tracing String
"homoLambdaCase" (TacticsM () -> TacticsM ()) -> TacticsM () -> TacticsM ()
forall a b. (a -> b) -> a -> b
$
    (Judgement
 -> RuleT
      Judgement
      (Trace, LHsExpr GhcPs)
      TacticError
      TacticState
      ExtractM
      (Trace, 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
       (Trace, LHsExpr GhcPs)
       TacticError
       TacticState
       ExtractM
       (Trace, LHsExpr GhcPs))
 -> TacticsM ())
-> (Judgement
    -> RuleT
         Judgement
         (Trace, LHsExpr GhcPs)
         TacticError
         TacticState
         ExtractM
         (Trace, LHsExpr GhcPs))
-> TacticsM ()
forall a b. (a -> b) -> a -> b
$ (DataCon
 -> Judgement
 -> RuleT
      Judgement
      (Trace, LHsExpr GhcPs)
      TacticError
      TacticState
      ExtractM
      (Trace, LHsExpr GhcPs))
-> Judgement
-> RuleT
     Judgement
     (Trace, LHsExpr GhcPs)
     TacticError
     TacticState
     ExtractM
     (Trace, LHsExpr GhcPs)
destructLambdaCase' ((DataCon
  -> Judgement
  -> RuleT
       Judgement
       (Trace, LHsExpr GhcPs)
       TacticError
       TacticState
       ExtractM
       (Trace, LHsExpr GhcPs))
 -> Judgement
 -> RuleT
      Judgement
      (Trace, LHsExpr GhcPs)
      TacticError
      TacticState
      ExtractM
      (Trace, LHsExpr GhcPs))
-> (DataCon
    -> Judgement
    -> RuleT
         Judgement
         (Trace, LHsExpr GhcPs)
         TacticError
         TacticState
         ExtractM
         (Trace, LHsExpr GhcPs))
-> Judgement
-> RuleT
     Judgement
     (Trace, LHsExpr GhcPs)
     TacticError
     TacticState
     ExtractM
     (Trace, LHsExpr GhcPs)
forall a b. (a -> b) -> a -> b
$ \DataCon
dc Judgement
jdg ->
      Judgement
-> DataCon
-> [Type]
-> RuleT
     Judgement
     (Trace, LHsExpr GhcPs)
     TacticError
     TacticState
     ExtractM
     (Trace, LHsExpr GhcPs)
buildDataCon Judgement
jdg DataCon
dc
        ([Type]
 -> RuleT
      Judgement
      (Trace, LHsExpr GhcPs)
      TacticError
      TacticState
      ExtractM
      (Trace, LHsExpr GhcPs))
-> (CType -> [Type])
-> CType
-> RuleT
     Judgement
     (Trace, LHsExpr GhcPs)
     TacticError
     TacticState
     ExtractM
     (Trace, LHsExpr GhcPs)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Type, [Type]) -> [Type]
forall a b. (a, b) -> b
snd
        ((Type, [Type]) -> [Type])
-> (CType -> (Type, [Type])) -> CType -> [Type]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> (Type, [Type])
splitAppTys
        (Type -> (Type, [Type]))
-> (CType -> Type) -> CType -> (Type, [Type])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CType -> Type
unCType
        (CType
 -> RuleT
      Judgement
      (Trace, LHsExpr GhcPs)
      TacticError
      TacticState
      ExtractM
      (Trace, LHsExpr GhcPs))
-> CType
-> RuleT
     Judgement
     (Trace, LHsExpr GhcPs)
     TacticError
     TacticState
     ExtractM
     (Trace, 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 = 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 (Trace, ext) err s m a
-> TacticT jdg (Trace, 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
  (Trace, LHsExpr GhcPs)
  TacticError
  TacticState
  ExtractM
  Judgement
forall (m :: * -> *) jdg ext err s.
Functor m =>
TacticT jdg ext err s m jdg
goal
  let hy :: Hypothesis CType
hy = Judgement -> Hypothesis CType
forall a. Judgement' a -> Hypothesis a
jHypothesis Judgement
jdg
      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
     (Trace, LHsExpr GhcPs)
     TacticError
     TacticState
     ExtractM
     Type
forall (m :: * -> *). MonadState TacticState m => Type -> m Type
freshTyvars Type
ty
  let ([TyVar]
_, [Type]
_, [Type]
args, Type
ret) = Type -> ([TyVar], [Type], [Type], Type)
tacticsSplitFunTy Type
ty'
  TacticsM () -> TacticsM ()
requireNewHoles (TacticsM () -> TacticsM ()) -> TacticsM () -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ (Judgement
 -> RuleT
      Judgement
      (Trace, LHsExpr GhcPs)
      TacticError
      TacticState
      ExtractM
      (Trace, 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
       (Trace, LHsExpr GhcPs)
       TacticError
       TacticState
       ExtractM
       (Trace, LHsExpr GhcPs))
 -> TacticsM ())
-> (Judgement
    -> RuleT
         Judgement
         (Trace, LHsExpr GhcPs)
         TacticError
         TacticState
         ExtractM
         (Trace, LHsExpr GhcPs))
-> TacticsM ()
forall a b. (a -> b) -> a -> b
$ \Judgement
jdg -> do
    CType -> CType -> RuleM ()
unify CType
g (Type -> CType
CType Type
ret)
    Judgement -> OccName -> RuleM ()
forall (m :: * -> *).
MonadState TacticState m =>
Judgement -> OccName -> m ()
useOccName Judgement
jdg OccName
func
    (Trace
tr, [LHsExpr GhcPs]
sgs)
        <- ([(Trace, LHsExpr GhcPs)] -> (Trace, [LHsExpr GhcPs]))
-> RuleT
     Judgement
     (Trace, LHsExpr GhcPs)
     TacticError
     TacticState
     ExtractM
     [(Trace, LHsExpr GhcPs)]
-> RuleT
     Judgement
     (Trace, LHsExpr GhcPs)
     TacticError
     TacticState
     ExtractM
     (Trace, [LHsExpr GhcPs])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [(Trace, LHsExpr GhcPs)] -> (Trace, [LHsExpr GhcPs])
forall a. [(Trace, a)] -> (Trace, [a])
unzipTrace
        (RuleT
   Judgement
   (Trace, LHsExpr GhcPs)
   TacticError
   TacticState
   ExtractM
   [(Trace, LHsExpr GhcPs)]
 -> RuleT
      Judgement
      (Trace, LHsExpr GhcPs)
      TacticError
      TacticState
      ExtractM
      (Trace, [LHsExpr GhcPs]))
-> RuleT
     Judgement
     (Trace, LHsExpr GhcPs)
     TacticError
     TacticState
     ExtractM
     [(Trace, LHsExpr GhcPs)]
-> RuleT
     Judgement
     (Trace, LHsExpr GhcPs)
     TacticError
     TacticState
     ExtractM
     (Trace, [LHsExpr GhcPs])
forall a b. (a -> b) -> a -> b
$ (Type
 -> RuleT
      Judgement
      (Trace, LHsExpr GhcPs)
      TacticError
      TacticState
      ExtractM
      (Trace, LHsExpr GhcPs))
-> [Type]
-> RuleT
     Judgement
     (Trace, LHsExpr GhcPs)
     TacticError
     TacticState
     ExtractM
     [(Trace, LHsExpr GhcPs)]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse ( Judgement
-> RuleT
     Judgement
     (Trace, LHsExpr GhcPs)
     TacticError
     TacticState
     ExtractM
     (Trace, LHsExpr GhcPs)
newSubgoal
                    (Judgement
 -> RuleT
      Judgement
      (Trace, LHsExpr GhcPs)
      TacticError
      TacticState
      ExtractM
      (Trace, LHsExpr GhcPs))
-> (Type -> Judgement)
-> Type
-> RuleT
     Judgement
     (Trace, LHsExpr GhcPs)
     TacticError
     TacticState
     ExtractM
     (Trace, LHsExpr GhcPs)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Judgement -> Judgement
blacklistingDestruct
                    (Judgement -> Judgement)
-> (Type -> Judgement) -> Type -> Judgement
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (CType -> Judgement -> Judgement)
-> Judgement -> CType -> Judgement
forall a b c. (a -> b -> c) -> b -> a -> c
flip CType -> Judgement -> Judgement
forall a. a -> Judgement' a -> Judgement' a
withNewGoal Judgement
jdg
                    (CType -> Judgement) -> (Type -> CType) -> Type -> Judgement
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> CType
CType
                    ) [Type]
args
    (Trace, LHsExpr GhcPs)
-> RuleT
     Judgement
     (Trace, LHsExpr GhcPs)
     TacticError
     TacticState
     ExtractM
     (Trace, LHsExpr GhcPs)
forall (f :: * -> *) a. Applicative f => a -> f a
pure
      ((Trace, LHsExpr GhcPs)
 -> RuleT
      Judgement
      (Trace, LHsExpr GhcPs)
      TacticError
      TacticState
      ExtractM
      (Trace, LHsExpr GhcPs))
-> ([HsExpr GhcPs] -> (Trace, LHsExpr GhcPs))
-> [HsExpr GhcPs]
-> RuleT
     Judgement
     (Trace, LHsExpr GhcPs)
     TacticError
     TacticState
     ExtractM
     (Trace, LHsExpr GhcPs)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Trace
tr, )
      (LHsExpr GhcPs -> (Trace, LHsExpr GhcPs))
-> ([HsExpr GhcPs] -> LHsExpr GhcPs)
-> [HsExpr GhcPs]
-> (Trace, LHsExpr GhcPs)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HsExpr GhcPs -> LHsExpr GhcPs
forall a. HasSrcSpan a => SrcSpanLess a -> a
noLoc
      (HsExpr GhcPs -> LHsExpr GhcPs)
-> ([HsExpr GhcPs] -> HsExpr GhcPs)
-> [HsExpr GhcPs]
-> LHsExpr GhcPs
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (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
(@@) (OccName -> HsExpr GhcPs
forall a. Var a => OccName -> a
var' OccName
func)
      ([HsExpr GhcPs]
 -> RuleT
      Judgement
      (Trace, LHsExpr GhcPs)
      TacticError
      TacticState
      ExtractM
      (Trace, LHsExpr GhcPs))
-> [HsExpr GhcPs]
-> RuleT
     Judgement
     (Trace, LHsExpr GhcPs)
     TacticError
     TacticState
     ExtractM
     (Trace, LHsExpr GhcPs)
forall a b. (a -> b) -> a -> b
$ (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 [LHsExpr GhcPs]
sgs


------------------------------------------------------------------------------
-- | 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 (Trace, ext) err s m a
-> TacticT jdg (Trace, 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
  (Trace, LHsExpr GhcPs)
  TacticError
  TacticState
  ExtractM
  Judgement
forall (m :: * -> *) jdg ext err s.
Functor m =>
TacticT jdg ext err s m jdg
goal
  let g :: CType
g = Judgement -> CType
forall a. Judgement' a -> a
jGoal Judgement
jdg
  case HasDebugCallStack => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe (Type -> Maybe (TyCon, [Type])) -> Type -> Maybe (TyCon, [Type])
forall a b. (a -> b) -> a -> b
$ CType -> Type
unCType CType
g of
    Maybe (TyCon, [Type])
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 (TyCon
tc, [Type]
_) -> do
      let dcs :: [DataCon]
dcs = TyCon -> [DataCon]
tyConDataCons TyCon
tc
      [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 (Trace, ext) err s m a
-> TacticT jdg (Trace, 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
  (Trace, LHsExpr GhcPs)
  TacticError
  TacticState
  ExtractM
  Judgement
forall (m :: * -> *) jdg ext err s.
Functor m =>
TacticT jdg ext err s m jdg
goal
  let g :: CType
g = Judgement -> CType
forall a. Judgement' a -> a
jGoal Judgement
jdg
  case HasDebugCallStack => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe (Type -> Maybe (TyCon, [Type])) -> Type -> Maybe (TyCon, [Type])
forall a b. (a -> b) -> a -> b
$ CType -> Type
unCType CType
g of
    Maybe (TyCon, [Type])
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 (TyCon
tc, [Type]
_) -> do
      let dcs :: [DataCon]
dcs = TyCon -> [DataCon]
tyConDataCons TyCon
tc
      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


------------------------------------------------------------------------------
-- | 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
  (Trace, 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 data constructor to solve the goal.
splitDataCon :: DataCon -> TacticsM ()
splitDataCon :: DataCon -> TacticsM ()
splitDataCon DataCon
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 (Trace, ext) err s m a
-> TacticT jdg (Trace, ext) err s m a
tracing (String
"splitDataCon:" String -> String -> String
forall a. Semigroup a => a -> a -> a
<> DataCon -> String
forall a. Show a => a -> String
show DataCon
dc) (TacticsM () -> TacticsM ()) -> TacticsM () -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ (Judgement
 -> RuleT
      Judgement
      (Trace, LHsExpr GhcPs)
      TacticError
      TacticState
      ExtractM
      (Trace, 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
       (Trace, LHsExpr GhcPs)
       TacticError
       TacticState
       ExtractM
       (Trace, LHsExpr GhcPs))
 -> TacticsM ())
-> (Judgement
    -> RuleT
         Judgement
         (Trace, LHsExpr GhcPs)
         TacticError
         TacticState
         ExtractM
         (Trace, 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, [Type])
Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe (Type -> Maybe (TyCon, [Type])) -> Type -> Maybe (TyCon, [Type])
forall a b. (a -> b) -> a -> b
$ CType -> Type
unCType CType
g of
      Just (TyCon
tc, [Type]
apps) -> do
        case DataCon -> [DataCon] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem DataCon
dc ([DataCon] -> Bool) -> [DataCon] -> Bool
forall a b. (a -> b) -> a -> b
$ TyCon -> [DataCon]
tyConDataCons TyCon
tc of
          Bool
True -> Judgement
-> DataCon
-> [Type]
-> RuleT
     Judgement
     (Trace, LHsExpr GhcPs)
     TacticError
     TacticState
     ExtractM
     (Trace, LHsExpr GhcPs)
buildDataCon (Judgement -> Judgement
unwhitelistingSplit Judgement
jdg) DataCon
dc [Type]
apps
          Bool
False -> TacticError
-> RuleT
     Judgement
     (Trace, LHsExpr GhcPs)
     TacticError
     TacticState
     ExtractM
     (Trace, LHsExpr GhcPs)
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TacticError
 -> RuleT
      Judgement
      (Trace, LHsExpr GhcPs)
      TacticError
      TacticState
      ExtractM
      (Trace, LHsExpr GhcPs))
-> TacticError
-> RuleT
     Judgement
     (Trace, LHsExpr GhcPs)
     TacticError
     TacticState
     ExtractM
     (Trace, LHsExpr GhcPs)
forall a b. (a -> b) -> a -> b
$ DataCon -> TacticError
IncorrectDataCon DataCon
dc
      Maybe (TyCon, [Type])
Nothing -> TacticError
-> RuleT
     Judgement
     (Trace, LHsExpr GhcPs)
     TacticError
     TacticState
     ExtractM
     (Trace, LHsExpr GhcPs)
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TacticError
 -> RuleT
      Judgement
      (Trace, LHsExpr GhcPs)
      TacticError
      TacticState
      ExtractM
      (Trace, LHsExpr GhcPs))
-> TacticError
-> RuleT
     Judgement
     (Trace, LHsExpr GhcPs)
     TacticError
     TacticState
     ExtractM
     (Trace, LHsExpr GhcPs)
forall a b. (a -> b) -> a -> b
$ String -> CType -> TacticError
GoalMismatch String
"splitDataCon" CType
g


------------------------------------------------------------------------------
-- | @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
     (Trace, LHsExpr GhcPs)
     (Trace, 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
      (Trace, LHsExpr GhcPs)
      (Trace, LHsExpr GhcPs)
      TacticError
      TacticState
      ExtractM)
   ()
 -> TacticsM ())
-> StateT
     Judgement
     (ProofStateT
        (Trace, LHsExpr GhcPs)
        (Trace, LHsExpr GhcPs)
        TacticError
        TacticState
        ExtractM)
     ()
-> TacticsM ()
forall a b. (a -> b) -> a -> b
$ (Judgement
 -> ProofStateT
      (Trace, LHsExpr GhcPs)
      (Trace, LHsExpr GhcPs)
      TacticError
      TacticState
      ExtractM
      ((), Judgement))
-> StateT
     Judgement
     (ProofStateT
        (Trace, LHsExpr GhcPs)
        (Trace, LHsExpr GhcPs)
        TacticError
        TacticState
        ExtractM)
     ()
forall s (m :: * -> *) a. (s -> m (a, s)) -> StateT s m a
StateT ((Judgement
  -> ProofStateT
       (Trace, LHsExpr GhcPs)
       (Trace, LHsExpr GhcPs)
       TacticError
       TacticState
       ExtractM
       ((), Judgement))
 -> StateT
      Judgement
      (ProofStateT
         (Trace, LHsExpr GhcPs)
         (Trace, LHsExpr GhcPs)
         TacticError
         TacticState
         ExtractM)
      ())
-> (Judgement
    -> ProofStateT
         (Trace, LHsExpr GhcPs)
         (Trace, LHsExpr GhcPs)
         TacticError
         TacticState
         ExtractM
         ((), Judgement))
-> StateT
     Judgement
     (ProofStateT
        (Trace, LHsExpr GhcPs)
        (Trace, LHsExpr GhcPs)
        TacticError
        TacticState
        ExtractM)
     ()
forall a b. (a -> b) -> a -> b
$ \Judgement
s -> StateT
  Judgement
  (ProofStateT
     (Trace, LHsExpr GhcPs)
     (Trace, LHsExpr GhcPs)
     TacticError
     TacticState
     ExtractM)
  ()
-> Judgement
-> ProofStateT
     (Trace, LHsExpr GhcPs)
     (Trace, LHsExpr GhcPs)
     TacticError
     TacticState
     ExtractM
     ((), Judgement)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT (TacticsM ()
-> StateT
     Judgement
     (ProofStateT
        (Trace, LHsExpr GhcPs)
        (Trace, 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
         (Trace, LHsExpr GhcPs)
         (Trace, LHsExpr GhcPs)
         TacticError
         TacticState
         ExtractM)
      ())
-> TacticsM ()
-> StateT
     Judgement
     (ProofStateT
        (Trace, LHsExpr GhcPs)
        (Trace, 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
     (Trace, LHsExpr GhcPs)
     (Trace, 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
      (Trace, LHsExpr GhcPs)
      (Trace, LHsExpr GhcPs)
      TacticError
      TacticState
      ExtractM)
   a
 -> TacticsM a)
-> StateT
     Judgement
     (ProofStateT
        (Trace, LHsExpr GhcPs)
        (Trace, LHsExpr GhcPs)
        TacticError
        TacticState
        ExtractM)
     a
-> TacticsM a
forall a b. (a -> b) -> a -> b
$ (Judgement
 -> ProofStateT
      (Trace, LHsExpr GhcPs)
      (Trace, LHsExpr GhcPs)
      TacticError
      TacticState
      ExtractM
      (a, Judgement))
-> StateT
     Judgement
     (ProofStateT
        (Trace, LHsExpr GhcPs)
        (Trace, LHsExpr GhcPs)
        TacticError
        TacticState
        ExtractM)
     a
forall s (m :: * -> *) a. (s -> m (a, s)) -> StateT s m a
StateT ((Judgement
  -> ProofStateT
       (Trace, LHsExpr GhcPs)
       (Trace, LHsExpr GhcPs)
       TacticError
       TacticState
       ExtractM
       (a, Judgement))
 -> StateT
      Judgement
      (ProofStateT
         (Trace, LHsExpr GhcPs)
         (Trace, LHsExpr GhcPs)
         TacticError
         TacticState
         ExtractM)
      a)
-> (Judgement
    -> ProofStateT
         (Trace, LHsExpr GhcPs)
         (Trace, LHsExpr GhcPs)
         TacticError
         TacticState
         ExtractM
         (a, Judgement))
-> StateT
     Judgement
     (ProofStateT
        (Trace, LHsExpr GhcPs)
        (Trace, LHsExpr GhcPs)
        TacticError
        TacticState
        ExtractM)
     a
forall a b. (a -> b) -> a -> b
$ \Judgement
jdg ->
    StateT
  Judgement
  (ProofStateT
     (Trace, LHsExpr GhcPs)
     (Trace, LHsExpr GhcPs)
     TacticError
     TacticState
     ExtractM)
  a
-> Judgement
-> ProofStateT
     (Trace, LHsExpr GhcPs)
     (Trace, 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
        (Trace, LHsExpr GhcPs)
        (Trace, 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
      (Trace, LHsExpr GhcPs)
      (Trace, LHsExpr GhcPs)
      TacticError
      TacticState
      ExtractM
      (a, Judgement))
-> Judgement
-> ProofStateT
     (Trace, LHsExpr GhcPs)
     (Trace, LHsExpr GhcPs)
     TacticError
     TacticState
     ExtractM
     (a, Judgement)
forall a b. (a -> b) -> a -> b
$ Judgement -> Judgement
f Judgement
jdg


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
        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])
 -> (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 (Maybe TyCon -> Bool
forall a. Maybe a -> Bool
isJust (Maybe TyCon -> Bool)
-> (HyInfo CType -> Maybe TyCon) -> HyInfo CType -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Maybe TyCon
algebraicTyCon (Type -> Maybe TyCon)
-> (HyInfo CType -> Type) -> HyInfo CType -> Maybe TyCon
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


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