{-# LANGUAGE TupleSections #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE DeriveGeneric         #-}
{-# LANGUAGE FlexibleContexts      #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE LambdaCase            #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeSynonymInstances  #-}
{-# 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 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 Judgement -> [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
$ Judgement -> Map OccName (HyInfo CType)
forall a. Judgement' a -> Map OccName (HyInfo 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]) -> (OccName -> TacticsM ()) -> TacticsM ()
forall a. (Judgement -> [a]) -> (a -> TacticsM ()) -> TacticsM ()
attemptOn ([OccName] -> Judgement -> [OccName]
forall a b. a -> b -> a
const ([OccName] -> Judgement -> [OccName])
-> [OccName] -> Judgement -> [OccName]
forall a b. (a -> b) -> a -> b
$ ((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)]
defs) ((OccName -> TacticsM ()) -> TacticsM ())
-> (OccName -> TacticsM ()) -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ \OccName
name -> 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 (OccName -> TacticsM ()
apply OccName
name) ((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 :: Map OccName (HyInfo CType)
hy = Judgement -> Map OccName (HyInfo CType)
forall a. Judgement' a -> Map OccName (HyInfo 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 <- Map OccName (HyInfo CType)
-> [Type]
-> RuleT
     Judgement
     (Trace, LHsExpr GhcPs)
     TacticError
     TacticState
     ExtractM
     [OccName]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
Map OccName a -> t Type -> m (t OccName)
mkManyGoodNames (Judgement -> Map OccName (HyInfo CType)
forall a. Judgement' a -> Map OccName (HyInfo 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 :: OccName -> TacticsM ()
destructAuto :: OccName -> TacticsM ()
destructAuto OccName
name = 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
  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
$ Judgement -> Map OccName (HyInfo CType)
forall a. Judgement' a -> Map OccName (HyInfo a)
jHypothesis Judgement
jdg of
    Maybe (HyInfo 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
$ OccName -> TacticError
NotInScope OccName
name
    Just HyInfo CType
hi ->
      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))
-> OccName
-> 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) OccName
name
      in 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
. Map OccName (HyInfo CType) -> [HyInfo CType]
forall k a. Map k a -> [a]
M.elems (Map OccName (HyInfo CType) -> [HyInfo CType])
-> (Judgement -> Map OccName (HyInfo CType))
-> Judgement
-> [HyInfo CType]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Judgement -> Map OccName (HyInfo CType)
forall a. Judgement' a -> Map OccName (HyInfo 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
name
                      Bool
False -> Maybe TacticError
forall a. Maybe a
Nothing
            Bool
False -> TacticsM ()
subtactic


------------------------------------------------------------------------------
-- | Case split, and leave holes in the matches.
destruct :: OccName -> TacticsM ()
destruct :: OccName -> TacticsM ()
destruct OccName
name = 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))
-> OccName
-> 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) OccName
name


------------------------------------------------------------------------------
-- | Case split, using the same data constructor in the matches.
homo :: OccName -> TacticsM ()
homo :: OccName -> TacticsM ()
homo = TacticsM () -> TacticsM ()
forall a. TacticsM a -> TacticsM a
requireConcreteHole (TacticsM () -> TacticsM ())
-> (OccName -> TacticsM ()) -> OccName -> 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 ())
-> (OccName -> TacticsM ()) -> OccName -> 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 ())
-> (OccName
    -> Judgement
    -> RuleT
         Judgement
         (Trace, LHsExpr GhcPs)
         TacticError
         TacticState
         ExtractM
         (Trace, LHsExpr GhcPs))
-> OccName
-> TacticsM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (DataCon
 -> Judgement
 -> RuleT
      Judgement
      (Trace, LHsExpr GhcPs)
      TacticError
      TacticState
      ExtractM
      (Trace, LHsExpr GhcPs))
-> OccName
-> 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 :: OccName -> TacticsM ()
apply :: OccName -> TacticsM ()
apply OccName
func = 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 OccName
func) (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 :: Map OccName (HyInfo CType)
hy = Judgement -> Map OccName (HyInfo CType)
forall a. Judgement' a -> Map OccName (HyInfo a)
jHypothesis Judgement
jdg
      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
func Map OccName (HyInfo CType)
hy of
    Just (HyInfo CType -> CType
forall a. HyInfo a -> a
hi_type -> CType Type
ty) -> do
      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
    Maybe (HyInfo CType)
Nothing -> do
      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
"apply" CType
g


------------------------------------------------------------------------------
-- | 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
    [ (OccName -> TacticsM ()) -> TacticsM ()
overFunctions ((OccName -> TacticsM ()) -> TacticsM ())
-> (OccName -> TacticsM ()) -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ \OccName
fname -> do
        OccName -> TacticsM ()
apply OccName
fname
        TacticsM ()
loop
    , (OccName -> TacticsM ()) -> TacticsM ()
overAlgebraicTerms ((OccName -> TacticsM ()) -> TacticsM ())
-> (OccName -> TacticsM ()) -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ \OccName
aname -> do
        OccName -> TacticsM ()
destructAuto OccName
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 :: (OccName -> TacticsM ()) -> TacticsM ()
overFunctions :: (OccName -> TacticsM ()) -> TacticsM ()
overFunctions =
  (Judgement -> [OccName]) -> (OccName -> TacticsM ()) -> TacticsM ()
forall a. (Judgement -> [a]) -> (a -> TacticsM ()) -> TacticsM ()
attemptOn ((Judgement -> [OccName])
 -> (OccName -> TacticsM ()) -> TacticsM ())
-> (Judgement -> [OccName])
-> (OccName -> TacticsM ())
-> TacticsM ()
forall a b. (a -> b) -> a -> b
$ Map OccName (HyInfo CType) -> [OccName]
forall k a. Map k a -> [k]
M.keys (Map OccName (HyInfo CType) -> [OccName])
-> (Judgement -> Map OccName (HyInfo CType))
-> Judgement
-> [OccName]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (HyInfo CType -> Bool)
-> Map OccName (HyInfo CType) -> Map OccName (HyInfo CType)
forall a k. (a -> Bool) -> Map k a -> Map k a
M.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) (Map OccName (HyInfo CType) -> Map OccName (HyInfo CType))
-> (Judgement -> Map OccName (HyInfo CType))
-> Judgement
-> Map OccName (HyInfo CType)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Judgement -> Map OccName (HyInfo CType)
forall a. Judgement' a -> Map OccName (HyInfo a)
jHypothesis

overAlgebraicTerms :: (OccName -> TacticsM ()) -> TacticsM ()
overAlgebraicTerms :: (OccName -> TacticsM ()) -> TacticsM ()
overAlgebraicTerms =
  (Judgement -> [OccName]) -> (OccName -> TacticsM ()) -> TacticsM ()
forall a. (Judgement -> [a]) -> (a -> TacticsM ()) -> TacticsM ()
attemptOn ((Judgement -> [OccName])
 -> (OccName -> TacticsM ()) -> TacticsM ())
-> (Judgement -> [OccName])
-> (OccName -> TacticsM ())
-> TacticsM ()
forall a b. (a -> b) -> a -> b
$
    Map OccName (HyInfo CType) -> [OccName]
forall k a. Map k a -> [k]
M.keys (Map OccName (HyInfo CType) -> [OccName])
-> (Judgement -> Map OccName (HyInfo CType))
-> Judgement
-> [OccName]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (HyInfo CType -> Bool)
-> Map OccName (HyInfo CType) -> Map OccName (HyInfo CType)
forall a k. (a -> Bool) -> Map k a -> Map k a
M.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) (Map OccName (HyInfo CType) -> Map OccName (HyInfo CType))
-> (Judgement -> Map OccName (HyInfo CType))
-> Judgement
-> Map OccName (HyInfo CType)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Judgement -> Map OccName (HyInfo CType)
forall a. Judgement' a -> Map OccName (HyInfo a)
jHypothesis


allNames :: Judgement -> [OccName]
allNames :: Judgement -> [OccName]
allNames = Map OccName (HyInfo CType) -> [OccName]
forall k a. Map k a -> [k]
M.keys (Map OccName (HyInfo CType) -> [OccName])
-> (Judgement -> Map OccName (HyInfo CType))
-> Judgement
-> [OccName]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Judgement -> Map OccName (HyInfo CType)
forall a. Judgement' a -> Map OccName (HyInfo a)
jHypothesis