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

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

import           ConLike (ConLike(RealDataCon))
import           Control.Applicative (Alternative(empty), (<|>))
import           Control.Lens ((&), (%~), (<>~))
import           Control.Monad (filterM)
import           Control.Monad (unless)
import           Control.Monad.Extra (anyM)
import           Control.Monad.Reader.Class (MonadReader (ask))
import           Control.Monad.State.Strict (StateT(..), runStateT)
import           Data.Bool (bool)
import           Data.Foldable
import           Data.Functor ((<&>))
import           Data.Generics.Labels ()
import           Data.List
import           Data.List.Extra (dropEnd, takeEnd)
import qualified Data.Map as M
import           Data.Maybe
import           Data.Set (Set)
import qualified Data.Set as S
import           Data.Traversable (for)
import           DataCon
import           Development.IDE.GHC.Compat
import           GHC.Exts
import           GHC.SourceGen ((@@))
import           GHC.SourceGen.Expr
import           Name (occNameString, occName)
import           OccName (mkVarOcc)
import           Refinery.Tactic
import           Refinery.Tactic.Internal
import           TcType
import           Type hiding (Var)
import           Wingman.CodeGen
import           Wingman.GHC
import           Wingman.Judgements
import           Wingman.Machinery
import           Wingman.Naming
import           Wingman.StaticPlugin (pattern MetaprogramSyntax)
import           Wingman.Types


------------------------------------------------------------------------------
-- | Use something in the hypothesis to fill the hole.
assumption :: TacticsM ()
assumption :: TacticsM ()
assumption = (Judgement -> [OccName]) -> (OccName -> TacticsM ()) -> TacticsM ()
forall a. (Judgement -> [a]) -> (a -> TacticsM ()) -> TacticsM ()
attemptOn (Set OccName -> [OccName]
forall a. Set a -> [a]
S.toList (Set OccName -> [OccName])
-> (Judgement -> Set OccName) -> Judgement -> [OccName]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Judgement -> Set OccName
allNames) OccName -> TacticsM ()
assume


------------------------------------------------------------------------------
-- | Use something named in the hypothesis to fill the hole.
assume :: OccName -> TacticsM ()
assume :: OccName -> TacticsM ()
assume OccName
name = (Judgement
 -> RuleT
      Judgement
      (Synthesized (LHsExpr GhcPs))
      TacticError
      TacticState
      ExtractM
      (Synthesized (LHsExpr GhcPs)))
-> TacticsM ()
forall (m :: * -> *) jdg ext err s.
Monad m =>
(jdg -> RuleT jdg ext err s m ext) -> TacticT jdg ext err s m ()
rule ((Judgement
  -> RuleT
       Judgement
       (Synthesized (LHsExpr GhcPs))
       TacticError
       TacticState
       ExtractM
       (Synthesized (LHsExpr GhcPs)))
 -> TacticsM ())
-> (Judgement
    -> RuleT
         Judgement
         (Synthesized (LHsExpr GhcPs))
         TacticError
         TacticState
         ExtractM
         (Synthesized (LHsExpr GhcPs)))
-> TacticsM ()
forall a b. (a -> b) -> a -> b
$ \Judgement
jdg -> do
  case OccName -> Map OccName (HyInfo CType) -> Maybe (HyInfo CType)
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup OccName
name (Map OccName (HyInfo CType) -> Maybe (HyInfo CType))
-> Map OccName (HyInfo CType) -> Maybe (HyInfo CType)
forall a b. (a -> b) -> a -> b
$ Hypothesis CType -> Map OccName (HyInfo CType)
forall a. Hypothesis a -> Map OccName (HyInfo a)
hyByName (Hypothesis CType -> Map OccName (HyInfo CType))
-> Hypothesis CType -> Map OccName (HyInfo CType)
forall a b. (a -> b) -> a -> b
$ Judgement -> Hypothesis CType
forall a. Judgement' a -> Hypothesis a
jHypothesis Judgement
jdg of
    Just (HyInfo CType -> CType
forall a. HyInfo a -> a
hi_type -> CType
ty) -> do
      CType -> CType -> RuleM ()
unify CType
ty (CType -> RuleM ()) -> CType -> RuleM ()
forall a b. (a -> b) -> a -> b
$ Judgement -> CType
forall a. Judgement' a -> a
jGoal Judgement
jdg
      Synthesized (LHsExpr GhcPs)
-> RuleT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     (Synthesized (LHsExpr GhcPs))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Synthesized (LHsExpr GhcPs)
 -> RuleT
      Judgement
      (Synthesized (LHsExpr GhcPs))
      TacticError
      TacticState
      ExtractM
      (Synthesized (LHsExpr GhcPs)))
-> Synthesized (LHsExpr GhcPs)
-> RuleT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     (Synthesized (LHsExpr GhcPs))
forall a b. (a -> b) -> a -> b
$
        -- This slightly terrible construct is producing a mostly-empty
        -- 'Synthesized'; but there is no monoid instance to do something more
        -- reasonable for a default value.
        (LHsExpr GhcPs -> Synthesized (LHsExpr GhcPs)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SrcSpanLess (LHsExpr GhcPs) -> LHsExpr GhcPs
forall a. HasSrcSpan a => SrcSpanLess a -> a
noLoc (SrcSpanLess (LHsExpr GhcPs) -> LHsExpr GhcPs)
-> SrcSpanLess (LHsExpr GhcPs) -> LHsExpr GhcPs
forall a b. (a -> b) -> a -> b
$ OccName -> HsExpr GhcPs
forall a. Var a => OccName -> a
var' OccName
name))
          { syn_trace :: Trace
syn_trace = String -> Trace
tracePrim (String -> Trace) -> String -> Trace
forall a b. (a -> b) -> a -> b
$ String
"assume " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> OccName -> String
occNameString OccName
name
          , syn_used_vals :: Set OccName
syn_used_vals = OccName -> Set OccName
forall a. a -> Set a
S.singleton OccName
name Set OccName -> Set OccName -> Set OccName
forall a. Semigroup a => a -> a -> a
<> Judgement -> OccName -> Set OccName
forall a. Judgement' a -> OccName -> Set OccName
getAncestry Judgement
jdg OccName
name
          }
    Maybe (HyInfo CType)
Nothing -> RuleT
  Judgement
  (Synthesized (LHsExpr GhcPs))
  TacticError
  TacticState
  ExtractM
  (Synthesized (LHsExpr GhcPs))
forall jdg ext err s (m :: * -> *) a. RuleT jdg ext err s m a
cut


------------------------------------------------------------------------------
-- | Like 'apply', but uses an 'OccName' available in the context
-- or the module
use :: Saturation -> OccName -> TacticsM ()
use :: Saturation -> OccName -> TacticsM ()
use Saturation
sat OccName
occ = do
  Context
ctx <- TacticT
  Judgement
  (Synthesized (LHsExpr GhcPs))
  TacticError
  TacticState
  ExtractM
  Context
forall r (m :: * -> *). MonadReader r m => m r
ask
  CType
ty <- case OccName -> Context -> Maybe CType
forall (m :: * -> *).
MonadReader Context m =>
OccName -> m (Maybe CType)
lookupNameInContext OccName
occ Context
ctx of
    Just CType
ty -> CType
-> TacticT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     CType
forall (f :: * -> *) a. Applicative f => a -> f a
pure CType
ty
    Maybe CType
Nothing -> Type -> CType
CType (Type -> CType)
-> TacticT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     Type
-> TacticT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     CType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> OccName
-> TacticT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     Type
getOccNameType OccName
occ
  Saturation -> HyInfo CType -> TacticsM ()
apply Saturation
sat (HyInfo CType -> TacticsM ()) -> HyInfo CType -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ OccName -> CType -> HyInfo CType
createImportedHyInfo OccName
occ CType
ty


recursion :: TacticsM ()
-- TODO(sandy): This tactic doesn't fire for the @AutoThetaFix@ golden test,
-- presumably due to running afoul of 'requireConcreteHole'. Look into this!
recursion :: TacticsM ()
recursion = TacticsM () -> TacticsM ()
forall a. TacticsM a -> TacticsM a
requireConcreteHole (TacticsM () -> TacticsM ()) -> TacticsM () -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ String -> TacticsM () -> TacticsM ()
forall (m :: * -> *) jdg ext err s a.
Functor m =>
String
-> TacticT jdg (Synthesized ext) err s m a
-> TacticT jdg (Synthesized ext) err s m a
tracing String
"recursion" (TacticsM () -> TacticsM ()) -> TacticsM () -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ do
  [(OccName, CType)]
defs <- TacticsM [(OccName, CType)]
getCurrentDefinitions
  (Judgement -> [(OccName, CType)])
-> ((OccName, CType) -> TacticsM ()) -> TacticsM ()
forall a. (Judgement -> [a]) -> (a -> TacticsM ()) -> TacticsM ()
attemptOn ([(OccName, CType)] -> Judgement -> [(OccName, CType)]
forall a b. a -> b -> a
const [(OccName, CType)]
defs) (((OccName, CType) -> TacticsM ()) -> TacticsM ())
-> ((OccName, CType) -> TacticsM ()) -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ \(OccName
name, CType
ty) -> TacticsM () -> TacticsM ()
forall (m :: * -> *) jdg ext err s a.
Functor m =>
TacticT jdg (Synthesized ext) err s m a
-> TacticT jdg (Synthesized ext) err s m a
markRecursion (TacticsM () -> TacticsM ()) -> TacticsM () -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ do
    Judgement
jdg <- TacticT
  Judgement
  (Synthesized (LHsExpr GhcPs))
  TacticError
  TacticState
  ExtractM
  Judgement
forall (m :: * -> *) jdg ext err s.
Functor m =>
TacticT jdg ext err s m jdg
goal
    -- Peek allows us to look at the extract produced by this block.
    TacticsM ()
-> (Synthesized (LHsExpr GhcPs) -> Maybe TacticError)
-> TacticsM ()
forall meta ext err s (m :: * -> *) jdg.
(MetaSubst meta ext, MonadExtract meta ext err s m) =>
TacticT jdg ext err s m ()
-> (ext -> Maybe err) -> TacticT jdg ext err s m ()
peek
      ( do
          let hy' :: Hypothesis CType
hy' = [(OccName, CType)] -> Hypothesis CType
forall a. [(OccName, a)] -> Hypothesis a
recursiveHypothesis [(OccName, CType)]
defs
          Context
ctx <- TacticT
  Judgement
  (Synthesized (LHsExpr GhcPs))
  TacticError
  TacticState
  ExtractM
  Context
forall r (m :: * -> *). MonadReader r m => m r
ask
          TacticsM () -> (Judgement -> Judgement) -> TacticsM ()
forall a. TacticsM a -> (Judgement -> Judgement) -> TacticsM a
localTactic (Saturation -> HyInfo CType -> TacticsM ()
apply Saturation
Saturated (HyInfo CType -> TacticsM ()) -> HyInfo CType -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ OccName -> Provenance -> CType -> HyInfo CType
forall a. OccName -> Provenance -> a -> HyInfo a
HyInfo OccName
name Provenance
RecursivePrv CType
ty) (Context -> Hypothesis CType -> Judgement -> Judgement
introduce Context
ctx Hypothesis CType
hy')
            TacticsM () -> [TacticsM ()] -> TacticsM ()
forall (m :: * -> *) jdg ext err s a.
Functor m =>
TacticT jdg ext err s m a
-> [TacticT jdg ext err s m a] -> TacticT jdg ext err s m a
<@> (Int -> TacticsM ()) -> [Int] -> [TacticsM ()]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (TacticsM () -> (Judgement -> Judgement) -> TacticsM ()
forall a. TacticsM a -> (Judgement -> Judgement) -> TacticsM a
localTactic TacticsM ()
assumption ((Judgement -> Judgement) -> TacticsM ())
-> (Int -> Judgement -> Judgement) -> Int -> TacticsM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OccName -> Int -> Judgement -> Judgement
filterPosition OccName
name) [Int
0..]
      ) ((Synthesized (LHsExpr GhcPs) -> Maybe TacticError) -> TacticsM ())
-> (Synthesized (LHsExpr GhcPs) -> Maybe TacticError)
-> TacticsM ()
forall a b. (a -> b) -> a -> b
$ \Synthesized (LHsExpr GhcPs)
ext -> do
        let pat_vals :: Map OccName PatVal
pat_vals = Judgement -> Map OccName PatVal
forall a. Judgement' a -> Map OccName PatVal
jPatHypothesis Judgement
jdg
        -- Make sure that the recursive call contains at least one already-bound
        -- pattern value. This ensures it is structurally smaller, and thus
        -- suggests termination.
        case ((OccName -> Bool) -> Set OccName -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any ((OccName -> Map OccName PatVal -> Bool)
-> Map OccName PatVal -> OccName -> Bool
forall a b c. (a -> b -> c) -> b -> a -> c
flip OccName -> Map OccName PatVal -> Bool
forall k a. Ord k => k -> Map k a -> Bool
M.member Map OccName PatVal
pat_vals) (Set OccName -> Bool) -> Set OccName -> Bool
forall a b. (a -> b) -> a -> b
$ Synthesized (LHsExpr GhcPs) -> Set OccName
forall a. Synthesized a -> Set OccName
syn_used_vals Synthesized (LHsExpr GhcPs)
ext) of
          Bool
True -> Maybe TacticError
forall a. Maybe a
Nothing
          Bool
False -> TacticError -> Maybe TacticError
forall a. a -> Maybe a
Just TacticError
UnhelpfulRecursion


restrictPositionForApplication :: TacticsM () -> TacticsM () -> TacticsM ()
restrictPositionForApplication :: TacticsM () -> TacticsM () -> TacticsM ()
restrictPositionForApplication TacticsM ()
f TacticsM ()
app = do
  -- NOTE(sandy): Safe use of head; context is guaranteed to have a defining
  -- binding
  OccName
name <- [OccName] -> OccName
forall a. [a] -> a
head ([OccName] -> OccName)
-> ([(OccName, CType)] -> [OccName])
-> [(OccName, CType)]
-> OccName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((OccName, CType) -> OccName) -> [(OccName, CType)] -> [OccName]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (OccName, CType) -> OccName
forall a b. (a, b) -> a
fst ([(OccName, CType)] -> OccName)
-> TacticsM [(OccName, CType)]
-> TacticT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     OccName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TacticsM [(OccName, CType)]
getCurrentDefinitions
  TacticsM ()
f TacticsM () -> [TacticsM ()] -> TacticsM ()
forall (m :: * -> *) jdg ext err s a.
Functor m =>
TacticT jdg ext err s m a
-> [TacticT jdg ext err s m a] -> TacticT jdg ext err s m a
<@>
    (Int -> TacticsM ()) -> [Int] -> [TacticsM ()]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap
      (TacticsM () -> (Judgement -> Judgement) -> TacticsM ()
forall a. TacticsM a -> (Judgement -> Judgement) -> TacticsM a
localTactic TacticsM ()
app ((Judgement -> Judgement) -> TacticsM ())
-> (Int -> Judgement -> Judgement) -> Int -> TacticsM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OccName -> Int -> Judgement -> Judgement
filterPosition OccName
name) [Int
0..]


------------------------------------------------------------------------------
-- | Introduce a lambda binding every variable.
intros :: TacticsM ()
intros :: TacticsM ()
intros = IntroParams -> TacticsM ()
intros' IntroParams
IntroduceAllUnnamed


data IntroParams
  = IntroduceAllUnnamed
  | IntroduceOnlyNamed [OccName]
  | IntroduceOnlyUnnamed Int
  deriving stock (IntroParams -> IntroParams -> Bool
(IntroParams -> IntroParams -> Bool)
-> (IntroParams -> IntroParams -> Bool) -> Eq IntroParams
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: IntroParams -> IntroParams -> Bool
$c/= :: IntroParams -> IntroParams -> Bool
== :: IntroParams -> IntroParams -> Bool
$c== :: IntroParams -> IntroParams -> Bool
Eq, Eq IntroParams
Eq IntroParams
-> (IntroParams -> IntroParams -> Ordering)
-> (IntroParams -> IntroParams -> Bool)
-> (IntroParams -> IntroParams -> Bool)
-> (IntroParams -> IntroParams -> Bool)
-> (IntroParams -> IntroParams -> Bool)
-> (IntroParams -> IntroParams -> IntroParams)
-> (IntroParams -> IntroParams -> IntroParams)
-> Ord IntroParams
IntroParams -> IntroParams -> Bool
IntroParams -> IntroParams -> Ordering
IntroParams -> IntroParams -> IntroParams
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: IntroParams -> IntroParams -> IntroParams
$cmin :: IntroParams -> IntroParams -> IntroParams
max :: IntroParams -> IntroParams -> IntroParams
$cmax :: IntroParams -> IntroParams -> IntroParams
>= :: IntroParams -> IntroParams -> Bool
$c>= :: IntroParams -> IntroParams -> Bool
> :: IntroParams -> IntroParams -> Bool
$c> :: IntroParams -> IntroParams -> Bool
<= :: IntroParams -> IntroParams -> Bool
$c<= :: IntroParams -> IntroParams -> Bool
< :: IntroParams -> IntroParams -> Bool
$c< :: IntroParams -> IntroParams -> Bool
compare :: IntroParams -> IntroParams -> Ordering
$ccompare :: IntroParams -> IntroParams -> Ordering
$cp1Ord :: Eq IntroParams
Ord, Int -> IntroParams -> String -> String
[IntroParams] -> String -> String
IntroParams -> String
(Int -> IntroParams -> String -> String)
-> (IntroParams -> String)
-> ([IntroParams] -> String -> String)
-> Show IntroParams
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
showList :: [IntroParams] -> String -> String
$cshowList :: [IntroParams] -> String -> String
show :: IntroParams -> String
$cshow :: IntroParams -> String
showsPrec :: Int -> IntroParams -> String -> String
$cshowsPrec :: Int -> IntroParams -> String -> String
Show)


------------------------------------------------------------------------------
-- | Introduce a lambda binding every variable.
intros'
    :: IntroParams
    -> TacticsM ()
intros' :: IntroParams -> TacticsM ()
intros' IntroParams
params = (Judgement
 -> RuleT
      Judgement
      (Synthesized (LHsExpr GhcPs))
      TacticError
      TacticState
      ExtractM
      (Synthesized (LHsExpr GhcPs)))
-> TacticsM ()
forall (m :: * -> *) jdg ext err s.
Monad m =>
(jdg -> RuleT jdg ext err s m ext) -> TacticT jdg ext err s m ()
rule ((Judgement
  -> RuleT
       Judgement
       (Synthesized (LHsExpr GhcPs))
       TacticError
       TacticState
       ExtractM
       (Synthesized (LHsExpr GhcPs)))
 -> TacticsM ())
-> (Judgement
    -> RuleT
         Judgement
         (Synthesized (LHsExpr GhcPs))
         TacticError
         TacticState
         ExtractM
         (Synthesized (LHsExpr GhcPs)))
-> TacticsM ()
forall a b. (a -> b) -> a -> b
$ \Judgement
jdg -> do
  let g :: CType
g  = Judgement -> CType
forall a. Judgement' a -> a
jGoal Judgement
jdg
  case Type -> ([TyVar], ThetaType, ThetaType, Type)
tacticsSplitFunTy (Type -> ([TyVar], ThetaType, ThetaType, Type))
-> Type -> ([TyVar], ThetaType, ThetaType, Type)
forall a b. (a -> b) -> a -> b
$ CType -> Type
unCType CType
g of
    ([TyVar]
_, ThetaType
_, [], Type
_) -> RuleT
  Judgement
  (Synthesized (LHsExpr GhcPs))
  TacticError
  TacticState
  ExtractM
  (Synthesized (LHsExpr GhcPs))
forall jdg ext err s (m :: * -> *) a. RuleT jdg ext err s m a
cut -- failure $ GoalMismatch "intros" g
    ([TyVar]
_, ThetaType
_, ThetaType
args, Type
res) -> do
      Context
ctx <- RuleT
  Judgement
  (Synthesized (LHsExpr GhcPs))
  TacticError
  TacticState
  ExtractM
  Context
forall r (m :: * -> *). MonadReader r m => m r
ask
      let gen_names :: [OccName]
gen_names = Set OccName -> ThetaType -> [OccName]
forall (t :: * -> *).
Traversable t =>
Set OccName -> t Type -> t OccName
mkManyGoodNames (Hypothesis CType -> Set OccName
forall a. Hypothesis a -> Set OccName
hyNamesInScope (Hypothesis CType -> Set OccName)
-> Hypothesis CType -> Set OccName
forall a b. (a -> b) -> a -> b
$ Judgement -> Hypothesis CType
forall a. Judgement' a -> Hypothesis a
jEntireHypothesis Judgement
jdg) ThetaType
args
          occs :: [OccName]
occs = case IntroParams
params of
            IntroParams
IntroduceAllUnnamed -> [OccName]
gen_names
            IntroduceOnlyNamed [OccName]
names -> [OccName]
names
            IntroduceOnlyUnnamed Int
n -> Int -> [OccName] -> [OccName]
forall a. Int -> [a] -> [a]
take Int
n [OccName]
gen_names
          num_occs :: Int
num_occs = [OccName] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [OccName]
occs
          top_hole :: Maybe OccName
top_hole = Context -> Judgement -> Maybe OccName
forall a. Context -> Judgement' a -> Maybe OccName
isTopHole Context
ctx Judgement
jdg
          bindings :: [(OccName, CType)]
bindings = [OccName] -> [CType] -> [(OccName, CType)]
forall a b. [a] -> [b] -> [(a, b)]
zip [OccName]
occs ([CType] -> [(OccName, CType)]) -> [CType] -> [(OccName, CType)]
forall a b. (a -> b) -> a -> b
$ ThetaType -> [CType]
coerce ThetaType
args
          bound_occs :: [OccName]
bound_occs = ((OccName, CType) -> OccName) -> [(OccName, CType)] -> [OccName]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (OccName, CType) -> OccName
forall a b. (a, b) -> a
fst [(OccName, CType)]
bindings
          hy' :: Hypothesis CType
hy' = Maybe OccName -> [(OccName, CType)] -> Hypothesis CType
forall a. Maybe OccName -> [(OccName, a)] -> Hypothesis a
lambdaHypothesis Maybe OccName
top_hole [(OccName, CType)]
bindings
          jdg' :: Judgement
jdg' = Context -> Hypothesis CType -> Judgement -> Judgement
introduce Context
ctx Hypothesis CType
hy'
               (Judgement -> Judgement) -> Judgement -> Judgement
forall a b. (a -> b) -> a -> b
$ CType -> Judgement -> Judgement
forall a. a -> Judgement' a -> Judgement' a
withNewGoal (Type -> CType
CType (Type -> CType) -> Type -> CType
forall a b. (a -> b) -> a -> b
$ ThetaType -> Type -> Type
mkFunTys' (Int -> ThetaType -> ThetaType
forall a. Int -> [a] -> [a]
drop Int
num_occs ThetaType
args) Type
res) Judgement
jdg
      Synthesized (LHsExpr GhcPs)
ext <- Judgement
-> RuleT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     (Synthesized (LHsExpr GhcPs))
newSubgoal Judgement
jdg'
      Synthesized (LHsExpr GhcPs)
-> RuleT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     (Synthesized (LHsExpr GhcPs))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Synthesized (LHsExpr GhcPs)
 -> RuleT
      Judgement
      (Synthesized (LHsExpr GhcPs))
      TacticError
      TacticState
      ExtractM
      (Synthesized (LHsExpr GhcPs)))
-> Synthesized (LHsExpr GhcPs)
-> RuleT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     (Synthesized (LHsExpr GhcPs))
forall a b. (a -> b) -> a -> b
$
        Synthesized (LHsExpr GhcPs)
ext
          Synthesized (LHsExpr GhcPs)
-> (Synthesized (LHsExpr GhcPs) -> Synthesized (LHsExpr GhcPs))
-> Synthesized (LHsExpr GhcPs)
forall a b. a -> (a -> b) -> b
& IsLabel
  "syn_trace"
  (ASetter
     (Synthesized (LHsExpr GhcPs))
     (Synthesized (LHsExpr GhcPs))
     Trace
     Trace)
ASetter
  (Synthesized (LHsExpr GhcPs))
  (Synthesized (LHsExpr GhcPs))
  Trace
  Trace
#syn_trace ASetter
  (Synthesized (LHsExpr GhcPs))
  (Synthesized (LHsExpr GhcPs))
  Trace
  Trace
-> (Trace -> Trace)
-> Synthesized (LHsExpr GhcPs)
-> Synthesized (LHsExpr GhcPs)
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ String -> [Trace] -> Trace
forall a. (Eq a, Monoid a) => a -> [Rose a] -> Rose a
rose (String
"intros {" String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
", " ((OccName -> String) -> [OccName] -> [String]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap OccName -> String
forall a. Show a => a -> String
show [OccName]
bound_occs) String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
"}")
                        ([Trace] -> Trace) -> (Trace -> [Trace]) -> Trace -> Trace
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Trace -> [Trace]
forall (f :: * -> *) a. Applicative f => a -> f a
pure
          Synthesized (LHsExpr GhcPs)
-> (Synthesized (LHsExpr GhcPs) -> Synthesized (LHsExpr GhcPs))
-> Synthesized (LHsExpr GhcPs)
forall a b. a -> (a -> b) -> b
& IsLabel
  "syn_scoped"
  (ASetter
     (Synthesized (LHsExpr GhcPs))
     (Synthesized (LHsExpr GhcPs))
     (Hypothesis CType)
     (Hypothesis CType))
ASetter
  (Synthesized (LHsExpr GhcPs))
  (Synthesized (LHsExpr GhcPs))
  (Hypothesis CType)
  (Hypothesis CType)
#syn_scoped ASetter
  (Synthesized (LHsExpr GhcPs))
  (Synthesized (LHsExpr GhcPs))
  (Hypothesis CType)
  (Hypothesis CType)
-> Hypothesis CType
-> Synthesized (LHsExpr GhcPs)
-> Synthesized (LHsExpr GhcPs)
forall a s t. Semigroup a => ASetter s t a a -> a -> s -> t
<>~ Hypothesis CType
hy'
          Synthesized (LHsExpr GhcPs)
-> (Synthesized (LHsExpr GhcPs) -> Synthesized (LHsExpr GhcPs))
-> Synthesized (LHsExpr GhcPs)
forall a b. a -> (a -> b) -> b
& IsLabel
  "syn_val"
  (ASetter
     (Synthesized (LHsExpr GhcPs))
     (Synthesized (LHsExpr GhcPs))
     (LHsExpr GhcPs)
     (LHsExpr GhcPs))
ASetter
  (Synthesized (LHsExpr GhcPs))
  (Synthesized (LHsExpr GhcPs))
  (LHsExpr GhcPs)
  (LHsExpr GhcPs)
#syn_val   ASetter
  (Synthesized (LHsExpr GhcPs))
  (Synthesized (LHsExpr GhcPs))
  (LHsExpr GhcPs)
  (LHsExpr GhcPs)
-> (LHsExpr GhcPs -> LHsExpr GhcPs)
-> Synthesized (LHsExpr GhcPs)
-> Synthesized (LHsExpr GhcPs)
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ HsExpr GhcPs -> LHsExpr GhcPs
forall a. HasSrcSpan a => SrcSpanLess a -> a
noLoc (HsExpr GhcPs -> LHsExpr GhcPs)
-> (LHsExpr GhcPs -> HsExpr GhcPs)
-> LHsExpr GhcPs
-> LHsExpr GhcPs
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Pat'] -> HsExpr GhcPs -> HsExpr GhcPs
lambda ((OccName -> Pat') -> [OccName] -> [Pat']
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap OccName -> Pat'
forall a. BVar a => OccName -> a
bvar' [OccName]
bound_occs) (HsExpr GhcPs -> HsExpr GhcPs)
-> (LHsExpr GhcPs -> HsExpr GhcPs) -> LHsExpr GhcPs -> HsExpr GhcPs
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LHsExpr GhcPs -> HsExpr GhcPs
forall a. HasSrcSpan a => a -> SrcSpanLess a
unLoc


------------------------------------------------------------------------------
-- | Introduce a single lambda argument, and immediately destruct it.
introAndDestruct :: TacticsM ()
introAndDestruct :: TacticsM ()
introAndDestruct = do
  [HyInfo CType]
hy <- (Hypothesis CType -> [HyInfo CType])
-> TacticT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     (Hypothesis CType)
-> TacticT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     [HyInfo CType]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Hypothesis CType -> [HyInfo CType]
forall a. Hypothesis a -> [HyInfo a]
unHypothesis (TacticT
   Judgement
   (Synthesized (LHsExpr GhcPs))
   TacticError
   TacticState
   ExtractM
   (Hypothesis CType)
 -> TacticT
      Judgement
      (Synthesized (LHsExpr GhcPs))
      TacticError
      TacticState
      ExtractM
      [HyInfo CType])
-> TacticT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     (Hypothesis CType)
-> TacticT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     [HyInfo CType]
forall a b. (a -> b) -> a -> b
$ TacticsM ()
-> TacticT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     (Hypothesis CType)
hyDiff (TacticsM ()
 -> TacticT
      Judgement
      (Synthesized (LHsExpr GhcPs))
      TacticError
      TacticState
      ExtractM
      (Hypothesis CType))
-> TacticsM ()
-> TacticT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     (Hypothesis CType)
forall a b. (a -> b) -> a -> b
$ IntroParams -> TacticsM ()
intros' (IntroParams -> TacticsM ()) -> IntroParams -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ Int -> IntroParams
IntroduceOnlyUnnamed Int
1
  -- This case should never happen, but I'm validating instead of parsing.
  -- Adding a log to be reminded if the invariant ever goes false.
  --
  -- But note that this isn't a game-ending bug. In the worst case, we'll
  -- accidentally bind too many variables, and incorrectly unify between them.
  -- Which means some GADT cases that should be eliminated won't be --- not the
  -- end of the world.
  Bool -> TacticsM () -> TacticsM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([HyInfo CType] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [HyInfo CType]
hy Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1) (TacticsM () -> TacticsM ()) -> TacticsM () -> TacticsM ()
forall a b. (a -> b) -> a -> b
$
    String -> [HyInfo CType] -> TacticsM ()
forall (m :: * -> *) a. (Monad m, Show a) => String -> a -> m ()
traceMX String
"BUG: Introduced too many variables for introAndDestruct! Please report me if you see this! " [HyInfo CType]
hy

  [HyInfo CType] -> (HyInfo CType -> TacticsM ()) -> TacticsM ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
t a -> (a -> f b) -> f ()
for_ [HyInfo CType]
hy HyInfo CType -> TacticsM ()
destruct


------------------------------------------------------------------------------
-- | Case split, and leave holes in the matches.
destructAuto :: HyInfo CType -> TacticsM ()
destructAuto :: HyInfo CType -> TacticsM ()
destructAuto HyInfo CType
hi = TacticsM () -> TacticsM ()
forall a. TacticsM a -> TacticsM a
requireConcreteHole (TacticsM () -> TacticsM ()) -> TacticsM () -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ String -> TacticsM () -> TacticsM ()
forall (m :: * -> *) jdg ext err s a.
Functor m =>
String
-> TacticT jdg (Synthesized ext) err s m a
-> TacticT jdg (Synthesized ext) err s m a
tracing String
"destruct(auto)" (TacticsM () -> TacticsM ()) -> TacticsM () -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ do
  Judgement
jdg <- TacticT
  Judgement
  (Synthesized (LHsExpr GhcPs))
  TacticError
  TacticState
  ExtractM
  Judgement
forall (m :: * -> *) jdg ext err s.
Functor m =>
TacticT jdg ext err s m jdg
goal
  let subtactic :: TacticsM ()
subtactic = HyInfo CType -> TacticsM ()
destructOrHomoAuto HyInfo CType
hi
  case Provenance -> Bool
isPatternMatch (Provenance -> Bool) -> Provenance -> Bool
forall a b. (a -> b) -> a -> b
$ HyInfo CType -> Provenance
forall a. HyInfo a -> Provenance
hi_provenance HyInfo CType
hi of
    Bool
True ->
      TacticsM () -> ([Judgement] -> Maybe TacticError) -> TacticsM ()
forall meta ext err s (m :: * -> *) jdg.
(MetaSubst meta ext, MonadExtract meta ext err s m) =>
TacticT jdg ext err s m ()
-> ([jdg] -> Maybe err) -> TacticT jdg ext err s m ()
pruning TacticsM ()
subtactic (([Judgement] -> Maybe TacticError) -> TacticsM ())
-> ([Judgement] -> Maybe TacticError) -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ \[Judgement]
jdgs ->
        let getHyTypes :: Judgement -> Set CType
getHyTypes = [CType] -> Set CType
forall a. Ord a => [a] -> Set a
S.fromList ([CType] -> Set CType)
-> (Judgement -> [CType]) -> Judgement -> Set CType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (HyInfo CType -> CType) -> [HyInfo CType] -> [CType]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap HyInfo CType -> CType
forall a. HyInfo a -> a
hi_type ([HyInfo CType] -> [CType])
-> (Judgement -> [HyInfo CType]) -> Judgement -> [CType]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Hypothesis CType -> [HyInfo CType]
forall a. Hypothesis a -> [HyInfo a]
unHypothesis (Hypothesis CType -> [HyInfo CType])
-> (Judgement -> Hypothesis CType) -> Judgement -> [HyInfo CType]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Judgement -> Hypothesis CType
forall a. Judgement' a -> Hypothesis a
jHypothesis
            new_hy :: Set CType
new_hy = (Judgement -> Set CType) -> [Judgement] -> Set CType
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Judgement -> Set CType
getHyTypes [Judgement]
jdgs
            old_hy :: Set CType
old_hy = Judgement -> Set CType
getHyTypes Judgement
jdg
        in case Set CType -> Bool
forall a. Set a -> Bool
S.null (Set CType -> Bool) -> Set CType -> Bool
forall a b. (a -> b) -> a -> b
$ Set CType
new_hy Set CType -> Set CType -> Set CType
forall a. Ord a => Set a -> Set a -> Set a
S.\\ Set CType
old_hy of
              Bool
True  -> TacticError -> Maybe TacticError
forall a. a -> Maybe a
Just (TacticError -> Maybe TacticError)
-> TacticError -> Maybe TacticError
forall a b. (a -> b) -> a -> b
$ OccName -> TacticError
UnhelpfulDestruct (OccName -> TacticError) -> OccName -> TacticError
forall a b. (a -> b) -> a -> b
$ HyInfo CType -> OccName
forall a. HyInfo a -> OccName
hi_name HyInfo CType
hi
              Bool
False -> Maybe TacticError
forall a. Maybe a
Nothing
    Bool
False -> TacticsM ()
subtactic


------------------------------------------------------------------------------
-- | When running auto, in order to prune the auto search tree, we try
-- a homomorphic destruct whenever possible. If that produces any results, we
-- can probably just prune the other side.
destructOrHomoAuto :: HyInfo CType -> TacticsM ()
destructOrHomoAuto :: HyInfo CType -> TacticsM ()
destructOrHomoAuto HyInfo CType
hi = String -> TacticsM () -> TacticsM ()
forall (m :: * -> *) jdg ext err s a.
Functor m =>
String
-> TacticT jdg (Synthesized ext) err s m a
-> TacticT jdg (Synthesized ext) err s m a
tracing String
"destructOrHomoAuto" (TacticsM () -> TacticsM ()) -> TacticsM () -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ do
  Judgement
jdg <- TacticT
  Judgement
  (Synthesized (LHsExpr GhcPs))
  TacticError
  TacticState
  ExtractM
  Judgement
forall (m :: * -> *) jdg ext err s.
Functor m =>
TacticT jdg ext err s m jdg
goal
  let g :: Type
g  = CType -> Type
unCType (CType -> Type) -> CType -> Type
forall a b. (a -> b) -> a -> b
$ Judgement -> CType
forall a. Judgement' a -> a
jGoal Judgement
jdg
      ty :: Type
ty = CType -> Type
unCType (CType -> Type) -> CType -> Type
forall a b. (a -> b) -> a -> b
$ HyInfo CType -> CType
forall a. HyInfo a -> a
hi_type HyInfo CType
hi

  TacticsM () -> TacticsM () -> Bool -> TacticsM ()
forall a. TacticsM a -> TacticsM a -> Bool -> TacticsM a
attemptWhen
      ((Judgement
 -> RuleT
      Judgement
      (Synthesized (LHsExpr GhcPs))
      TacticError
      TacticState
      ExtractM
      (Synthesized (LHsExpr GhcPs)))
-> TacticsM ()
forall (m :: * -> *) jdg ext err s.
Monad m =>
(jdg -> RuleT jdg ext err s m ext) -> TacticT jdg ext err s m ()
rule ((Judgement
  -> RuleT
       Judgement
       (Synthesized (LHsExpr GhcPs))
       TacticError
       TacticState
       ExtractM
       (Synthesized (LHsExpr GhcPs)))
 -> TacticsM ())
-> (Judgement
    -> RuleT
         Judgement
         (Synthesized (LHsExpr GhcPs))
         TacticError
         TacticState
         ExtractM
         (Synthesized (LHsExpr GhcPs)))
-> TacticsM ()
forall a b. (a -> b) -> a -> b
$ Bool
-> (ConLike
    -> Judgement
    -> RuleT
         Judgement
         (Synthesized (LHsExpr GhcPs))
         TacticError
         TacticState
         ExtractM
         (Synthesized (LHsExpr GhcPs)))
-> HyInfo CType
-> Judgement
-> RuleT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     (Synthesized (LHsExpr GhcPs))
destruct' Bool
False (\ConLike
dc Judgement
jdg ->
        Bool
-> Judgement
-> ConLike
-> ThetaType
-> RuleT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     (Synthesized (LHsExpr GhcPs))
buildDataCon Bool
False Judgement
jdg ConLike
dc (ThetaType
 -> RuleT
      Judgement
      (Synthesized (LHsExpr GhcPs))
      TacticError
      TacticState
      ExtractM
      (Synthesized (LHsExpr GhcPs)))
-> ThetaType
-> RuleT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     (Synthesized (LHsExpr GhcPs))
forall a b. (a -> b) -> a -> b
$ (Type, ThetaType) -> ThetaType
forall a b. (a, b) -> b
snd ((Type, ThetaType) -> ThetaType) -> (Type, ThetaType) -> ThetaType
forall a b. (a -> b) -> a -> b
$ Type -> (Type, ThetaType)
splitAppTys Type
g) HyInfo CType
hi)
      ((Judgement
 -> RuleT
      Judgement
      (Synthesized (LHsExpr GhcPs))
      TacticError
      TacticState
      ExtractM
      (Synthesized (LHsExpr GhcPs)))
-> TacticsM ()
forall (m :: * -> *) jdg ext err s.
Monad m =>
(jdg -> RuleT jdg ext err s m ext) -> TacticT jdg ext err s m ()
rule ((Judgement
  -> RuleT
       Judgement
       (Synthesized (LHsExpr GhcPs))
       TacticError
       TacticState
       ExtractM
       (Synthesized (LHsExpr GhcPs)))
 -> TacticsM ())
-> (Judgement
    -> RuleT
         Judgement
         (Synthesized (LHsExpr GhcPs))
         TacticError
         TacticState
         ExtractM
         (Synthesized (LHsExpr GhcPs)))
-> TacticsM ()
forall a b. (a -> b) -> a -> b
$ Bool
-> (ConLike
    -> Judgement
    -> RuleT
         Judgement
         (Synthesized (LHsExpr GhcPs))
         TacticError
         TacticState
         ExtractM
         (Synthesized (LHsExpr GhcPs)))
-> HyInfo CType
-> Judgement
-> RuleT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     (Synthesized (LHsExpr GhcPs))
destruct' Bool
False ((Judgement
 -> RuleT
      Judgement
      (Synthesized (LHsExpr GhcPs))
      TacticError
      TacticState
      ExtractM
      (Synthesized (LHsExpr GhcPs)))
-> ConLike
-> Judgement
-> RuleT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     (Synthesized (LHsExpr GhcPs))
forall a b. a -> b -> a
const Judgement
-> RuleT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     (Synthesized (LHsExpr GhcPs))
newSubgoal) HyInfo CType
hi)
    (Bool -> TacticsM ()) -> Bool -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ case (HasDebugCallStack => Type -> Maybe (TyCon, ThetaType)
Type -> Maybe (TyCon, ThetaType)
splitTyConApp_maybe Type
g, HasDebugCallStack => Type -> Maybe (TyCon, ThetaType)
Type -> Maybe (TyCon, ThetaType)
splitTyConApp_maybe Type
ty) of
        (Just (TyCon
gtc, ThetaType
_), Just (TyCon
tytc, ThetaType
_)) -> TyCon
gtc TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
tytc
        (Maybe (TyCon, ThetaType), Maybe (TyCon, ThetaType))
_ -> Bool
False


------------------------------------------------------------------------------
-- | Case split, and leave holes in the matches.
destruct :: HyInfo CType -> TacticsM ()
destruct :: HyInfo CType -> TacticsM ()
destruct HyInfo CType
hi = TacticsM () -> TacticsM ()
forall a. TacticsM a -> TacticsM a
requireConcreteHole (TacticsM () -> TacticsM ()) -> TacticsM () -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ String -> TacticsM () -> TacticsM ()
forall (m :: * -> *) jdg ext err s a.
Functor m =>
String
-> TacticT jdg (Synthesized ext) err s m a
-> TacticT jdg (Synthesized ext) err s m a
tracing String
"destruct(user)" (TacticsM () -> TacticsM ()) -> TacticsM () -> TacticsM ()
forall a b. (a -> b) -> a -> b
$
  (Judgement
 -> RuleT
      Judgement
      (Synthesized (LHsExpr GhcPs))
      TacticError
      TacticState
      ExtractM
      (Synthesized (LHsExpr GhcPs)))
-> TacticsM ()
forall (m :: * -> *) jdg ext err s.
Monad m =>
(jdg -> RuleT jdg ext err s m ext) -> TacticT jdg ext err s m ()
rule ((Judgement
  -> RuleT
       Judgement
       (Synthesized (LHsExpr GhcPs))
       TacticError
       TacticState
       ExtractM
       (Synthesized (LHsExpr GhcPs)))
 -> TacticsM ())
-> (Judgement
    -> RuleT
         Judgement
         (Synthesized (LHsExpr GhcPs))
         TacticError
         TacticState
         ExtractM
         (Synthesized (LHsExpr GhcPs)))
-> TacticsM ()
forall a b. (a -> b) -> a -> b
$ Bool
-> (ConLike
    -> Judgement
    -> RuleT
         Judgement
         (Synthesized (LHsExpr GhcPs))
         TacticError
         TacticState
         ExtractM
         (Synthesized (LHsExpr GhcPs)))
-> HyInfo CType
-> Judgement
-> RuleT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     (Synthesized (LHsExpr GhcPs))
destruct' Bool
False ((Judgement
 -> RuleT
      Judgement
      (Synthesized (LHsExpr GhcPs))
      TacticError
      TacticState
      ExtractM
      (Synthesized (LHsExpr GhcPs)))
-> ConLike
-> Judgement
-> RuleT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     (Synthesized (LHsExpr GhcPs))
forall a b. a -> b -> a
const Judgement
-> RuleT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     (Synthesized (LHsExpr GhcPs))
newSubgoal) HyInfo CType
hi


------------------------------------------------------------------------------
-- | Case split, and leave holes in the matches. Performs record punning.
destructPun :: HyInfo CType -> TacticsM ()
destructPun :: HyInfo CType -> TacticsM ()
destructPun HyInfo CType
hi = TacticsM () -> TacticsM ()
forall a. TacticsM a -> TacticsM a
requireConcreteHole (TacticsM () -> TacticsM ()) -> TacticsM () -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ String -> TacticsM () -> TacticsM ()
forall (m :: * -> *) jdg ext err s a.
Functor m =>
String
-> TacticT jdg (Synthesized ext) err s m a
-> TacticT jdg (Synthesized ext) err s m a
tracing String
"destructPun(user)" (TacticsM () -> TacticsM ()) -> TacticsM () -> TacticsM ()
forall a b. (a -> b) -> a -> b
$
  (Judgement
 -> RuleT
      Judgement
      (Synthesized (LHsExpr GhcPs))
      TacticError
      TacticState
      ExtractM
      (Synthesized (LHsExpr GhcPs)))
-> TacticsM ()
forall (m :: * -> *) jdg ext err s.
Monad m =>
(jdg -> RuleT jdg ext err s m ext) -> TacticT jdg ext err s m ()
rule ((Judgement
  -> RuleT
       Judgement
       (Synthesized (LHsExpr GhcPs))
       TacticError
       TacticState
       ExtractM
       (Synthesized (LHsExpr GhcPs)))
 -> TacticsM ())
-> (Judgement
    -> RuleT
         Judgement
         (Synthesized (LHsExpr GhcPs))
         TacticError
         TacticState
         ExtractM
         (Synthesized (LHsExpr GhcPs)))
-> TacticsM ()
forall a b. (a -> b) -> a -> b
$ Bool
-> (ConLike
    -> Judgement
    -> RuleT
         Judgement
         (Synthesized (LHsExpr GhcPs))
         TacticError
         TacticState
         ExtractM
         (Synthesized (LHsExpr GhcPs)))
-> HyInfo CType
-> Judgement
-> RuleT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     (Synthesized (LHsExpr GhcPs))
destruct' Bool
True ((Judgement
 -> RuleT
      Judgement
      (Synthesized (LHsExpr GhcPs))
      TacticError
      TacticState
      ExtractM
      (Synthesized (LHsExpr GhcPs)))
-> ConLike
-> Judgement
-> RuleT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     (Synthesized (LHsExpr GhcPs))
forall a b. a -> b -> a
const Judgement
-> RuleT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     (Synthesized (LHsExpr GhcPs))
newSubgoal) HyInfo CType
hi


------------------------------------------------------------------------------
-- | Case split, using the same data constructor in the matches.
homo :: HyInfo CType -> TacticsM ()
homo :: HyInfo CType -> TacticsM ()
homo HyInfo CType
hi = TacticsM () -> TacticsM ()
forall a. TacticsM a -> TacticsM a
requireConcreteHole (TacticsM () -> TacticsM ())
-> (TacticsM () -> TacticsM ()) -> TacticsM () -> TacticsM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> TacticsM () -> TacticsM ()
forall (m :: * -> *) jdg ext err s a.
Functor m =>
String
-> TacticT jdg (Synthesized ext) err s m a
-> TacticT jdg (Synthesized ext) err s m a
tracing String
"homo" (TacticsM () -> TacticsM ()) -> TacticsM () -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ do
  Judgement
jdg <- TacticT
  Judgement
  (Synthesized (LHsExpr GhcPs))
  TacticError
  TacticState
  ExtractM
  Judgement
forall (m :: * -> *) jdg ext err s.
Functor m =>
TacticT jdg ext err s m jdg
goal
  let g :: CType
g = Judgement -> CType
forall a. Judgement' a -> a
jGoal Judgement
jdg

  -- Ensure that every data constructor in the domain type is covered in the
  -- codomain; otherwise 'homo' will produce an ill-typed program.
  case (Type -> Type -> Maybe (Set (Uniquely DataCon))
uncoveredDataCons (CType -> Type
coerce (CType -> Type) -> CType -> Type
forall a b. (a -> b) -> a -> b
$ HyInfo CType -> CType
forall a. HyInfo a -> a
hi_type HyInfo CType
hi) (CType -> Type
coerce CType
g)) of
    Just Set (Uniquely DataCon)
uncovered_dcs ->
      Bool -> TacticsM () -> TacticsM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Set (Uniquely DataCon) -> Bool
forall a. Set a -> Bool
S.null Set (Uniquely DataCon)
uncovered_dcs) (TacticsM () -> TacticsM ()) -> TacticsM () -> TacticsM ()
forall a b. (a -> b) -> a -> b
$
        TacticError -> TacticsM ()
forall err jdg ext s (m :: * -> *) a.
err -> TacticT jdg ext err s m a
failure  (TacticError -> TacticsM ()) -> TacticError -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ String -> TacticError
TacticPanic String
"Can't cover every datacon in domain"
    Maybe (Set (Uniquely DataCon))
_ -> TacticError -> TacticsM ()
forall err jdg ext s (m :: * -> *) a.
err -> TacticT jdg ext err s m a
failure (TacticError -> TacticsM ()) -> TacticError -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ String -> TacticError
TacticPanic String
"Unable to fetch datacons"

  (Judgement
 -> RuleT
      Judgement
      (Synthesized (LHsExpr GhcPs))
      TacticError
      TacticState
      ExtractM
      (Synthesized (LHsExpr GhcPs)))
-> TacticsM ()
forall (m :: * -> *) jdg ext err s.
Monad m =>
(jdg -> RuleT jdg ext err s m ext) -> TacticT jdg ext err s m ()
rule
    ((Judgement
  -> RuleT
       Judgement
       (Synthesized (LHsExpr GhcPs))
       TacticError
       TacticState
       ExtractM
       (Synthesized (LHsExpr GhcPs)))
 -> TacticsM ())
-> (Judgement
    -> RuleT
         Judgement
         (Synthesized (LHsExpr GhcPs))
         TacticError
         TacticState
         ExtractM
         (Synthesized (LHsExpr GhcPs)))
-> TacticsM ()
forall a b. (a -> b) -> a -> b
$ Bool
-> (ConLike
    -> Judgement
    -> RuleT
         Judgement
         (Synthesized (LHsExpr GhcPs))
         TacticError
         TacticState
         ExtractM
         (Synthesized (LHsExpr GhcPs)))
-> HyInfo CType
-> Judgement
-> RuleT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     (Synthesized (LHsExpr GhcPs))
destruct'
        Bool
False
        (\ConLike
dc Judgement
jdg -> Bool
-> Judgement
-> ConLike
-> ThetaType
-> RuleT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     (Synthesized (LHsExpr GhcPs))
buildDataCon Bool
False Judgement
jdg ConLike
dc (ThetaType
 -> RuleT
      Judgement
      (Synthesized (LHsExpr GhcPs))
      TacticError
      TacticState
      ExtractM
      (Synthesized (LHsExpr GhcPs)))
-> ThetaType
-> RuleT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     (Synthesized (LHsExpr GhcPs))
forall a b. (a -> b) -> a -> b
$ (Type, ThetaType) -> ThetaType
forall a b. (a, b) -> b
snd ((Type, ThetaType) -> ThetaType) -> (Type, ThetaType) -> ThetaType
forall a b. (a -> b) -> a -> b
$ Type -> (Type, ThetaType)
splitAppTys (Type -> (Type, ThetaType)) -> Type -> (Type, ThetaType)
forall a b. (a -> b) -> a -> b
$ CType -> Type
unCType (CType -> Type) -> CType -> Type
forall a b. (a -> b) -> a -> b
$ Judgement -> CType
forall a. Judgement' a -> a
jGoal Judgement
jdg)
    (HyInfo CType
 -> Judgement
 -> RuleT
      Judgement
      (Synthesized (LHsExpr GhcPs))
      TacticError
      TacticState
      ExtractM
      (Synthesized (LHsExpr GhcPs)))
-> HyInfo CType
-> Judgement
-> RuleT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     (Synthesized (LHsExpr GhcPs))
forall a b. (a -> b) -> a -> b
$ HyInfo CType
hi


------------------------------------------------------------------------------
-- | LambdaCase split, and leave holes in the matches.
destructLambdaCase :: TacticsM ()
destructLambdaCase :: TacticsM ()
destructLambdaCase =
  String -> TacticsM () -> TacticsM ()
forall (m :: * -> *) jdg ext err s a.
Functor m =>
String
-> TacticT jdg (Synthesized ext) err s m a
-> TacticT jdg (Synthesized ext) err s m a
tracing String
"destructLambdaCase" (TacticsM () -> TacticsM ()) -> TacticsM () -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ (Judgement
 -> RuleT
      Judgement
      (Synthesized (LHsExpr GhcPs))
      TacticError
      TacticState
      ExtractM
      (Synthesized (LHsExpr GhcPs)))
-> TacticsM ()
forall (m :: * -> *) jdg ext err s.
Monad m =>
(jdg -> RuleT jdg ext err s m ext) -> TacticT jdg ext err s m ()
rule ((Judgement
  -> RuleT
       Judgement
       (Synthesized (LHsExpr GhcPs))
       TacticError
       TacticState
       ExtractM
       (Synthesized (LHsExpr GhcPs)))
 -> TacticsM ())
-> (Judgement
    -> RuleT
         Judgement
         (Synthesized (LHsExpr GhcPs))
         TacticError
         TacticState
         ExtractM
         (Synthesized (LHsExpr GhcPs)))
-> TacticsM ()
forall a b. (a -> b) -> a -> b
$ Bool
-> (ConLike
    -> Judgement
    -> RuleT
         Judgement
         (Synthesized (LHsExpr GhcPs))
         TacticError
         TacticState
         ExtractM
         (Synthesized (LHsExpr GhcPs)))
-> Judgement
-> RuleT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     (Synthesized (LHsExpr GhcPs))
destructLambdaCase' Bool
False ((Judgement
 -> RuleT
      Judgement
      (Synthesized (LHsExpr GhcPs))
      TacticError
      TacticState
      ExtractM
      (Synthesized (LHsExpr GhcPs)))
-> ConLike
-> Judgement
-> RuleT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     (Synthesized (LHsExpr GhcPs))
forall a b. a -> b -> a
const Judgement
-> RuleT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     (Synthesized (LHsExpr GhcPs))
newSubgoal)


------------------------------------------------------------------------------
-- | LambdaCase split, using the same data constructor in the matches.
homoLambdaCase :: TacticsM ()
homoLambdaCase :: TacticsM ()
homoLambdaCase =
  String -> TacticsM () -> TacticsM ()
forall (m :: * -> *) jdg ext err s a.
Functor m =>
String
-> TacticT jdg (Synthesized ext) err s m a
-> TacticT jdg (Synthesized ext) err s m a
tracing String
"homoLambdaCase" (TacticsM () -> TacticsM ()) -> TacticsM () -> TacticsM ()
forall a b. (a -> b) -> a -> b
$
    (Judgement
 -> RuleT
      Judgement
      (Synthesized (LHsExpr GhcPs))
      TacticError
      TacticState
      ExtractM
      (Synthesized (LHsExpr GhcPs)))
-> TacticsM ()
forall (m :: * -> *) jdg ext err s.
Monad m =>
(jdg -> RuleT jdg ext err s m ext) -> TacticT jdg ext err s m ()
rule ((Judgement
  -> RuleT
       Judgement
       (Synthesized (LHsExpr GhcPs))
       TacticError
       TacticState
       ExtractM
       (Synthesized (LHsExpr GhcPs)))
 -> TacticsM ())
-> (Judgement
    -> RuleT
         Judgement
         (Synthesized (LHsExpr GhcPs))
         TacticError
         TacticState
         ExtractM
         (Synthesized (LHsExpr GhcPs)))
-> TacticsM ()
forall a b. (a -> b) -> a -> b
$ Bool
-> (ConLike
    -> Judgement
    -> RuleT
         Judgement
         (Synthesized (LHsExpr GhcPs))
         TacticError
         TacticState
         ExtractM
         (Synthesized (LHsExpr GhcPs)))
-> Judgement
-> RuleT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     (Synthesized (LHsExpr GhcPs))
destructLambdaCase' Bool
False ((ConLike
  -> Judgement
  -> RuleT
       Judgement
       (Synthesized (LHsExpr GhcPs))
       TacticError
       TacticState
       ExtractM
       (Synthesized (LHsExpr GhcPs)))
 -> Judgement
 -> RuleT
      Judgement
      (Synthesized (LHsExpr GhcPs))
      TacticError
      TacticState
      ExtractM
      (Synthesized (LHsExpr GhcPs)))
-> (ConLike
    -> Judgement
    -> RuleT
         Judgement
         (Synthesized (LHsExpr GhcPs))
         TacticError
         TacticState
         ExtractM
         (Synthesized (LHsExpr GhcPs)))
-> Judgement
-> RuleT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     (Synthesized (LHsExpr GhcPs))
forall a b. (a -> b) -> a -> b
$ \ConLike
dc Judgement
jdg ->
      Bool
-> Judgement
-> ConLike
-> ThetaType
-> RuleT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     (Synthesized (LHsExpr GhcPs))
buildDataCon Bool
False Judgement
jdg ConLike
dc
        (ThetaType
 -> RuleT
      Judgement
      (Synthesized (LHsExpr GhcPs))
      TacticError
      TacticState
      ExtractM
      (Synthesized (LHsExpr GhcPs)))
-> (CType -> ThetaType)
-> CType
-> RuleT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     (Synthesized (LHsExpr GhcPs))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Type, ThetaType) -> ThetaType
forall a b. (a, b) -> b
snd
        ((Type, ThetaType) -> ThetaType)
-> (CType -> (Type, ThetaType)) -> CType -> ThetaType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> (Type, ThetaType)
splitAppTys
        (Type -> (Type, ThetaType))
-> (CType -> Type) -> CType -> (Type, ThetaType)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CType -> Type
unCType
        (CType
 -> RuleT
      Judgement
      (Synthesized (LHsExpr GhcPs))
      TacticError
      TacticState
      ExtractM
      (Synthesized (LHsExpr GhcPs)))
-> CType
-> RuleT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     (Synthesized (LHsExpr GhcPs))
forall a b. (a -> b) -> a -> b
$ Judgement -> CType
forall a. Judgement' a -> a
jGoal Judgement
jdg


data Saturation = Unsaturated Int
  deriving (Saturation -> Saturation -> Bool
(Saturation -> Saturation -> Bool)
-> (Saturation -> Saturation -> Bool) -> Eq Saturation
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Saturation -> Saturation -> Bool
$c/= :: Saturation -> Saturation -> Bool
== :: Saturation -> Saturation -> Bool
$c== :: Saturation -> Saturation -> Bool
Eq, Eq Saturation
Eq Saturation
-> (Saturation -> Saturation -> Ordering)
-> (Saturation -> Saturation -> Bool)
-> (Saturation -> Saturation -> Bool)
-> (Saturation -> Saturation -> Bool)
-> (Saturation -> Saturation -> Bool)
-> (Saturation -> Saturation -> Saturation)
-> (Saturation -> Saturation -> Saturation)
-> Ord Saturation
Saturation -> Saturation -> Bool
Saturation -> Saturation -> Ordering
Saturation -> Saturation -> Saturation
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Saturation -> Saturation -> Saturation
$cmin :: Saturation -> Saturation -> Saturation
max :: Saturation -> Saturation -> Saturation
$cmax :: Saturation -> Saturation -> Saturation
>= :: Saturation -> Saturation -> Bool
$c>= :: Saturation -> Saturation -> Bool
> :: Saturation -> Saturation -> Bool
$c> :: Saturation -> Saturation -> Bool
<= :: Saturation -> Saturation -> Bool
$c<= :: Saturation -> Saturation -> Bool
< :: Saturation -> Saturation -> Bool
$c< :: Saturation -> Saturation -> Bool
compare :: Saturation -> Saturation -> Ordering
$ccompare :: Saturation -> Saturation -> Ordering
$cp1Ord :: Eq Saturation
Ord, Int -> Saturation -> String -> String
[Saturation] -> String -> String
Saturation -> String
(Int -> Saturation -> String -> String)
-> (Saturation -> String)
-> ([Saturation] -> String -> String)
-> Show Saturation
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
showList :: [Saturation] -> String -> String
$cshowList :: [Saturation] -> String -> String
show :: Saturation -> String
$cshow :: Saturation -> String
showsPrec :: Int -> Saturation -> String -> String
$cshowsPrec :: Int -> Saturation -> String -> String
Show)

pattern Saturated :: Saturation
pattern $bSaturated :: Saturation
$mSaturated :: forall r. Saturation -> (Void# -> r) -> (Void# -> r) -> r
Saturated = Unsaturated 0


apply :: Saturation -> HyInfo CType -> TacticsM ()
apply :: Saturation -> HyInfo CType -> TacticsM ()
apply (Unsaturated Int
n) HyInfo CType
hi = String -> TacticsM () -> TacticsM ()
forall (m :: * -> *) jdg ext err s a.
Functor m =>
String
-> TacticT jdg (Synthesized ext) err s m a
-> TacticT jdg (Synthesized ext) err s m a
tracing (String
"apply' " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> OccName -> String
forall a. Show a => a -> String
show (HyInfo CType -> OccName
forall a. HyInfo a -> OccName
hi_name HyInfo CType
hi)) (TacticsM () -> TacticsM ()) -> TacticsM () -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ do
  Judgement
jdg <- TacticT
  Judgement
  (Synthesized (LHsExpr GhcPs))
  TacticError
  TacticState
  ExtractM
  Judgement
forall (m :: * -> *) jdg ext err s.
Functor m =>
TacticT jdg ext err s m jdg
goal
  let g :: CType
g  = Judgement -> CType
forall a. Judgement' a -> a
jGoal Judgement
jdg
      ty :: Type
ty = CType -> Type
unCType (CType -> Type) -> CType -> Type
forall a b. (a -> b) -> a -> b
$ HyInfo CType -> CType
forall a. HyInfo a -> a
hi_type HyInfo CType
hi
      func :: OccName
func = HyInfo CType -> OccName
forall a. HyInfo a -> OccName
hi_name HyInfo CType
hi
  Type
ty' <- Type
-> TacticT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     Type
forall (m :: * -> *). MonadState TacticState m => Type -> m Type
freshTyvars Type
ty
  let ([TyVar]
_, ThetaType
_, ThetaType
all_args, Type
ret) = Type -> ([TyVar], ThetaType, ThetaType, Type)
tacticsSplitFunTy Type
ty'
      saturated_args :: ThetaType
saturated_args = Int -> ThetaType -> ThetaType
forall a. Int -> [a] -> [a]
dropEnd Int
n ThetaType
all_args
      unsaturated_args :: ThetaType
unsaturated_args = Int -> ThetaType -> ThetaType
forall a. Int -> [a] -> [a]
takeEnd Int
n ThetaType
all_args
  (Judgement
 -> RuleT
      Judgement
      (Synthesized (LHsExpr GhcPs))
      TacticError
      TacticState
      ExtractM
      (Synthesized (LHsExpr GhcPs)))
-> TacticsM ()
forall (m :: * -> *) jdg ext err s.
Monad m =>
(jdg -> RuleT jdg ext err s m ext) -> TacticT jdg ext err s m ()
rule ((Judgement
  -> RuleT
       Judgement
       (Synthesized (LHsExpr GhcPs))
       TacticError
       TacticState
       ExtractM
       (Synthesized (LHsExpr GhcPs)))
 -> TacticsM ())
-> (Judgement
    -> RuleT
         Judgement
         (Synthesized (LHsExpr GhcPs))
         TacticError
         TacticState
         ExtractM
         (Synthesized (LHsExpr GhcPs)))
-> TacticsM ()
forall a b. (a -> b) -> a -> b
$ \Judgement
jdg -> do
    CType -> CType -> RuleM ()
unify CType
g (Type -> CType
CType (Type -> CType) -> Type -> CType
forall a b. (a -> b) -> a -> b
$ ThetaType -> Type -> Type
mkFunTys' ThetaType
unsaturated_args Type
ret)
    Synthesized [LHsExpr GhcPs]
ext
        <- ([Synthesized (LHsExpr GhcPs)] -> Synthesized [LHsExpr GhcPs])
-> RuleT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     [Synthesized (LHsExpr GhcPs)]
-> RuleT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     (Synthesized [LHsExpr GhcPs])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [Synthesized (LHsExpr GhcPs)] -> Synthesized [LHsExpr GhcPs]
forall a. [Synthesized a] -> Synthesized [a]
unzipTrace
        (RuleT
   Judgement
   (Synthesized (LHsExpr GhcPs))
   TacticError
   TacticState
   ExtractM
   [Synthesized (LHsExpr GhcPs)]
 -> RuleT
      Judgement
      (Synthesized (LHsExpr GhcPs))
      TacticError
      TacticState
      ExtractM
      (Synthesized [LHsExpr GhcPs]))
-> RuleT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     [Synthesized (LHsExpr GhcPs)]
-> RuleT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     (Synthesized [LHsExpr GhcPs])
forall a b. (a -> b) -> a -> b
$ (Type
 -> RuleT
      Judgement
      (Synthesized (LHsExpr GhcPs))
      TacticError
      TacticState
      ExtractM
      (Synthesized (LHsExpr GhcPs)))
-> ThetaType
-> RuleT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     [Synthesized (LHsExpr GhcPs)]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse ( Judgement
-> RuleT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     (Synthesized (LHsExpr GhcPs))
newSubgoal
                    (Judgement
 -> RuleT
      Judgement
      (Synthesized (LHsExpr GhcPs))
      TacticError
      TacticState
      ExtractM
      (Synthesized (LHsExpr GhcPs)))
-> (Type -> Judgement)
-> Type
-> RuleT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     (Synthesized (LHsExpr GhcPs))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Judgement -> Judgement
blacklistingDestruct
                    (Judgement -> Judgement)
-> (Type -> Judgement) -> Type -> Judgement
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (CType -> Judgement -> Judgement)
-> Judgement -> CType -> Judgement
forall a b c. (a -> b -> c) -> b -> a -> c
flip CType -> Judgement -> Judgement
forall a. a -> Judgement' a -> Judgement' a
withNewGoal Judgement
jdg
                    (CType -> Judgement) -> (Type -> CType) -> Type -> Judgement
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> CType
CType
                    ) ThetaType
saturated_args
    Synthesized (LHsExpr GhcPs)
-> RuleT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     (Synthesized (LHsExpr GhcPs))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Synthesized (LHsExpr GhcPs)
 -> RuleT
      Judgement
      (Synthesized (LHsExpr GhcPs))
      TacticError
      TacticState
      ExtractM
      (Synthesized (LHsExpr GhcPs)))
-> Synthesized (LHsExpr GhcPs)
-> RuleT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     (Synthesized (LHsExpr GhcPs))
forall a b. (a -> b) -> a -> b
$
      Synthesized [LHsExpr GhcPs]
ext
        Synthesized [LHsExpr GhcPs]
-> (Synthesized [LHsExpr GhcPs] -> Synthesized [LHsExpr GhcPs])
-> Synthesized [LHsExpr GhcPs]
forall a b. a -> (a -> b) -> b
& IsLabel
  "syn_used_vals"
  (ASetter
     (Synthesized [LHsExpr GhcPs])
     (Synthesized [LHsExpr GhcPs])
     (Set OccName)
     (Set OccName))
ASetter
  (Synthesized [LHsExpr GhcPs])
  (Synthesized [LHsExpr GhcPs])
  (Set OccName)
  (Set OccName)
#syn_used_vals ASetter
  (Synthesized [LHsExpr GhcPs])
  (Synthesized [LHsExpr GhcPs])
  (Set OccName)
  (Set OccName)
-> (Set OccName -> Set OccName)
-> Synthesized [LHsExpr GhcPs]
-> Synthesized [LHsExpr GhcPs]
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ (\Set OccName
x -> OccName -> Set OccName -> Set OccName
forall a. Ord a => a -> Set a -> Set a
S.insert OccName
func Set OccName
x Set OccName -> Set OccName -> Set OccName
forall a. Semigroup a => a -> a -> a
<> Judgement -> OccName -> Set OccName
forall a. Judgement' a -> OccName -> Set OccName
getAncestry Judgement
jdg OccName
func)
        Synthesized [LHsExpr GhcPs]
-> (Synthesized [LHsExpr GhcPs] -> Synthesized (LHsExpr GhcPs))
-> Synthesized (LHsExpr GhcPs)
forall a b. a -> (a -> b) -> b
& IsLabel
  "syn_val"
  (ASetter
     (Synthesized [LHsExpr GhcPs])
     (Synthesized (LHsExpr GhcPs))
     [LHsExpr GhcPs]
     (LHsExpr GhcPs))
ASetter
  (Synthesized [LHsExpr GhcPs])
  (Synthesized (LHsExpr GhcPs))
  [LHsExpr GhcPs]
  (LHsExpr GhcPs)
#syn_val       ASetter
  (Synthesized [LHsExpr GhcPs])
  (Synthesized (LHsExpr GhcPs))
  [LHsExpr GhcPs]
  (LHsExpr GhcPs)
-> ([LHsExpr GhcPs] -> LHsExpr GhcPs)
-> Synthesized [LHsExpr GhcPs]
-> Synthesized (LHsExpr GhcPs)
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ OccName -> [HsExpr GhcPs] -> LHsExpr GhcPs
mkApply OccName
func ([HsExpr GhcPs] -> LHsExpr GhcPs)
-> ([LHsExpr GhcPs] -> [HsExpr GhcPs])
-> [LHsExpr GhcPs]
-> LHsExpr GhcPs
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (LHsExpr GhcPs -> HsExpr GhcPs)
-> [LHsExpr GhcPs] -> [HsExpr GhcPs]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap LHsExpr GhcPs -> HsExpr GhcPs
forall a. HasSrcSpan a => a -> SrcSpanLess a
unLoc

application :: TacticsM ()
application :: TacticsM ()
application = (HyInfo CType -> TacticsM ()) -> TacticsM ()
overFunctions ((HyInfo CType -> TacticsM ()) -> TacticsM ())
-> (HyInfo CType -> TacticsM ()) -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ Saturation -> HyInfo CType -> TacticsM ()
apply Saturation
Saturated


------------------------------------------------------------------------------
-- | Choose between each of the goal's data constructors.
split :: TacticsM ()
split :: TacticsM ()
split = String -> TacticsM () -> TacticsM ()
forall (m :: * -> *) jdg ext err s a.
Functor m =>
String
-> TacticT jdg (Synthesized ext) err s m a
-> TacticT jdg (Synthesized ext) err s m a
tracing String
"split(user)" (TacticsM () -> TacticsM ()) -> TacticsM () -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ do
  Judgement
jdg <- TacticT
  Judgement
  (Synthesized (LHsExpr GhcPs))
  TacticError
  TacticState
  ExtractM
  Judgement
forall (m :: * -> *) jdg ext err s.
Functor m =>
TacticT jdg ext err s m jdg
goal
  let g :: CType
g = Judgement -> CType
forall a. Judgement' a -> a
jGoal Judgement
jdg
  case Type -> Maybe ([DataCon], ThetaType)
tacticsGetDataCons (Type -> Maybe ([DataCon], ThetaType))
-> Type -> Maybe ([DataCon], ThetaType)
forall a b. (a -> b) -> a -> b
$ CType -> Type
unCType CType
g of
    Maybe ([DataCon], ThetaType)
Nothing -> TacticError -> TacticsM ()
forall err jdg ext s (m :: * -> *) a.
err -> TacticT jdg ext err s m a
failure (TacticError -> TacticsM ()) -> TacticError -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ String -> CType -> TacticError
GoalMismatch String
"split" CType
g
    Just ([DataCon]
dcs, ThetaType
_) -> [TacticsM ()] -> TacticsM ()
forall (m :: * -> *) jdg ext err s a.
Monad m =>
[TacticT jdg ext err s m a] -> TacticT jdg ext err s m a
choice ([TacticsM ()] -> TacticsM ()) -> [TacticsM ()] -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ (DataCon -> TacticsM ()) -> [DataCon] -> [TacticsM ()]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap DataCon -> TacticsM ()
splitDataCon [DataCon]
dcs


------------------------------------------------------------------------------
-- | Choose between each of the goal's data constructors. Different than
-- 'split' because it won't split a data con if it doesn't result in any new
-- goals.
splitAuto :: TacticsM ()
splitAuto :: TacticsM ()
splitAuto = TacticsM () -> TacticsM ()
forall a. TacticsM a -> TacticsM a
requireConcreteHole (TacticsM () -> TacticsM ()) -> TacticsM () -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ String -> TacticsM () -> TacticsM ()
forall (m :: * -> *) jdg ext err s a.
Functor m =>
String
-> TacticT jdg (Synthesized ext) err s m a
-> TacticT jdg (Synthesized ext) err s m a
tracing String
"split(auto)" (TacticsM () -> TacticsM ()) -> TacticsM () -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ do
  Judgement
jdg <- TacticT
  Judgement
  (Synthesized (LHsExpr GhcPs))
  TacticError
  TacticState
  ExtractM
  Judgement
forall (m :: * -> *) jdg ext err s.
Functor m =>
TacticT jdg ext err s m jdg
goal
  let g :: CType
g = Judgement -> CType
forall a. Judgement' a -> a
jGoal Judgement
jdg
  case Type -> Maybe ([DataCon], ThetaType)
tacticsGetDataCons (Type -> Maybe ([DataCon], ThetaType))
-> Type -> Maybe ([DataCon], ThetaType)
forall a b. (a -> b) -> a -> b
$ CType -> Type
unCType CType
g of
    Maybe ([DataCon], ThetaType)
Nothing -> TacticError -> TacticsM ()
forall err jdg ext s (m :: * -> *) a.
err -> TacticT jdg ext err s m a
failure (TacticError -> TacticsM ()) -> TacticError -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ String -> CType -> TacticError
GoalMismatch String
"split" CType
g
    Just ([DataCon]
dcs, ThetaType
_) -> do
      case Judgement -> Bool
isSplitWhitelisted Judgement
jdg of
        Bool
True -> [TacticsM ()] -> TacticsM ()
forall (m :: * -> *) jdg ext err s a.
Monad m =>
[TacticT jdg ext err s m a] -> TacticT jdg ext err s m a
choice ([TacticsM ()] -> TacticsM ()) -> [TacticsM ()] -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ (DataCon -> TacticsM ()) -> [DataCon] -> [TacticsM ()]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap DataCon -> TacticsM ()
splitDataCon [DataCon]
dcs
        Bool
False -> do
          [TacticsM ()] -> TacticsM ()
forall (m :: * -> *) jdg ext err s a.
Monad m =>
[TacticT jdg ext err s m a] -> TacticT jdg ext err s m a
choice ([TacticsM ()] -> TacticsM ()) -> [TacticsM ()] -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ ((DataCon -> TacticsM ()) -> [DataCon] -> [TacticsM ()])
-> [DataCon] -> (DataCon -> TacticsM ()) -> [TacticsM ()]
forall a b c. (a -> b -> c) -> b -> a -> c
flip (DataCon -> TacticsM ()) -> [DataCon] -> [TacticsM ()]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [DataCon]
dcs ((DataCon -> TacticsM ()) -> [TacticsM ()])
-> (DataCon -> TacticsM ()) -> [TacticsM ()]
forall a b. (a -> b) -> a -> b
$ \DataCon
dc -> TacticsM () -> TacticsM ()
requireNewHoles (TacticsM () -> TacticsM ()) -> TacticsM () -> TacticsM ()
forall a b. (a -> b) -> a -> b
$
            DataCon -> TacticsM ()
splitDataCon DataCon
dc


------------------------------------------------------------------------------
-- | Like 'split', but only works if there is a single matching data
-- constructor for the goal.
splitSingle :: TacticsM ()
splitSingle :: TacticsM ()
splitSingle = String -> TacticsM () -> TacticsM ()
forall (m :: * -> *) jdg ext err s a.
Functor m =>
String
-> TacticT jdg (Synthesized ext) err s m a
-> TacticT jdg (Synthesized ext) err s m a
tracing String
"splitSingle" (TacticsM () -> TacticsM ()) -> TacticsM () -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ do
  Judgement
jdg <- TacticT
  Judgement
  (Synthesized (LHsExpr GhcPs))
  TacticError
  TacticState
  ExtractM
  Judgement
forall (m :: * -> *) jdg ext err s.
Functor m =>
TacticT jdg ext err s m jdg
goal
  let g :: CType
g = Judgement -> CType
forall a. Judgement' a -> a
jGoal Judgement
jdg
  case Type -> Maybe ([DataCon], ThetaType)
tacticsGetDataCons (Type -> Maybe ([DataCon], ThetaType))
-> Type -> Maybe ([DataCon], ThetaType)
forall a b. (a -> b) -> a -> b
$ CType -> Type
unCType CType
g of
    Just ([DataCon
dc], ThetaType
_) -> do
      DataCon -> TacticsM ()
splitDataCon DataCon
dc
    Maybe ([DataCon], ThetaType)
_ -> TacticError -> TacticsM ()
forall err jdg ext s (m :: * -> *) a.
err -> TacticT jdg ext err s m a
failure (TacticError -> TacticsM ()) -> TacticError -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ String -> CType -> TacticError
GoalMismatch String
"splitSingle" CType
g

------------------------------------------------------------------------------
-- | Like 'split', but prunes any data constructors which have holes.
obvious :: TacticsM ()
obvious :: TacticsM ()
obvious = String -> TacticsM () -> TacticsM ()
forall (m :: * -> *) jdg ext err s a.
Functor m =>
String
-> TacticT jdg (Synthesized ext) err s m a
-> TacticT jdg (Synthesized ext) err s m a
tracing String
"obvious" (TacticsM () -> TacticsM ()) -> TacticsM () -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ do
  TacticsM () -> ([Judgement] -> Maybe TacticError) -> TacticsM ()
forall meta ext err s (m :: * -> *) jdg.
(MetaSubst meta ext, MonadExtract meta ext err s m) =>
TacticT jdg ext err s m ()
-> ([jdg] -> Maybe err) -> TacticT jdg ext err s m ()
pruning TacticsM ()
split (([Judgement] -> Maybe TacticError) -> TacticsM ())
-> ([Judgement] -> Maybe TacticError) -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ Maybe TacticError -> Maybe TacticError -> Bool -> Maybe TacticError
forall a. a -> a -> Bool -> a
bool (TacticError -> Maybe TacticError
forall a. a -> Maybe a
Just TacticError
NoProgress) Maybe TacticError
forall a. Maybe a
Nothing (Bool -> Maybe TacticError)
-> ([Judgement] -> Bool) -> [Judgement] -> Maybe TacticError
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Judgement] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null


------------------------------------------------------------------------------
-- | Sorry leaves a hole in its extract
sorry :: TacticsM ()
sorry :: TacticsM ()
sorry = HsExpr GhcPs -> TacticsM ()
exact (HsExpr GhcPs -> TacticsM ()) -> HsExpr GhcPs -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ OccName -> HsExpr GhcPs
forall a. Var a => OccName -> a
var' (OccName -> HsExpr GhcPs) -> OccName -> HsExpr GhcPs
forall a b. (a -> b) -> a -> b
$ String -> OccName
mkVarOcc String
"_"


------------------------------------------------------------------------------
-- | Sorry leaves a hole in its extract
metaprogram :: TacticsM ()
metaprogram :: TacticsM ()
metaprogram = HsExpr GhcPs -> TacticsM ()
exact (HsExpr GhcPs -> TacticsM ()) -> HsExpr GhcPs -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ FastString -> HsExpr GhcPs
MetaprogramSyntax FastString
""


------------------------------------------------------------------------------
-- | Allow the given tactic to proceed if and only if it introduces holes that
-- have a different goal than current goal.
requireNewHoles :: TacticsM () -> TacticsM ()
requireNewHoles :: TacticsM () -> TacticsM ()
requireNewHoles TacticsM ()
m = do
  Judgement
jdg <- TacticT
  Judgement
  (Synthesized (LHsExpr GhcPs))
  TacticError
  TacticState
  ExtractM
  Judgement
forall (m :: * -> *) jdg ext err s.
Functor m =>
TacticT jdg ext err s m jdg
goal
  TacticsM () -> ([Judgement] -> Maybe TacticError) -> TacticsM ()
forall meta ext err s (m :: * -> *) jdg.
(MetaSubst meta ext, MonadExtract meta ext err s m) =>
TacticT jdg ext err s m ()
-> ([jdg] -> Maybe err) -> TacticT jdg ext err s m ()
pruning TacticsM ()
m (([Judgement] -> Maybe TacticError) -> TacticsM ())
-> ([Judgement] -> Maybe TacticError) -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ \[Judgement]
jdgs ->
    case [Judgement] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Judgement]
jdgs Bool -> Bool -> Bool
|| (CType -> Bool) -> [CType] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (CType -> CType -> Bool
forall a. Eq a => a -> a -> Bool
/= Judgement -> CType
forall a. Judgement' a -> a
jGoal Judgement
jdg) ((Judgement -> CType) -> [Judgement] -> [CType]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Judgement -> CType
forall a. Judgement' a -> a
jGoal [Judgement]
jdgs) of
      Bool
True  -> Maybe TacticError
forall a. Maybe a
Nothing
      Bool
False -> TacticError -> Maybe TacticError
forall a. a -> Maybe a
Just TacticError
NoProgress


------------------------------------------------------------------------------
-- | Attempt to instantiate the given ConLike to solve the goal.
--
-- INVARIANT: Assumes the given ConLike is appropriate to construct the type
-- with.
splitConLike :: ConLike -> TacticsM ()
splitConLike :: ConLike -> TacticsM ()
splitConLike ConLike
dc =
  TacticsM () -> TacticsM ()
forall a. TacticsM a -> TacticsM a
requireConcreteHole (TacticsM () -> TacticsM ()) -> TacticsM () -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ String -> TacticsM () -> TacticsM ()
forall (m :: * -> *) jdg ext err s a.
Functor m =>
String
-> TacticT jdg (Synthesized ext) err s m a
-> TacticT jdg (Synthesized ext) err s m a
tracing (String
"splitDataCon:" String -> String -> String
forall a. Semigroup a => a -> a -> a
<> ConLike -> String
forall a. Show a => a -> String
show ConLike
dc) (TacticsM () -> TacticsM ()) -> TacticsM () -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ (Judgement
 -> RuleT
      Judgement
      (Synthesized (LHsExpr GhcPs))
      TacticError
      TacticState
      ExtractM
      (Synthesized (LHsExpr GhcPs)))
-> TacticsM ()
forall (m :: * -> *) jdg ext err s.
Monad m =>
(jdg -> RuleT jdg ext err s m ext) -> TacticT jdg ext err s m ()
rule ((Judgement
  -> RuleT
       Judgement
       (Synthesized (LHsExpr GhcPs))
       TacticError
       TacticState
       ExtractM
       (Synthesized (LHsExpr GhcPs)))
 -> TacticsM ())
-> (Judgement
    -> RuleT
         Judgement
         (Synthesized (LHsExpr GhcPs))
         TacticError
         TacticState
         ExtractM
         (Synthesized (LHsExpr GhcPs)))
-> TacticsM ()
forall a b. (a -> b) -> a -> b
$ \Judgement
jdg -> do
    let g :: CType
g = Judgement -> CType
forall a. Judgement' a -> a
jGoal Judgement
jdg
    case HasDebugCallStack => Type -> Maybe (TyCon, ThetaType)
Type -> Maybe (TyCon, ThetaType)
splitTyConApp_maybe (Type -> Maybe (TyCon, ThetaType))
-> Type -> Maybe (TyCon, ThetaType)
forall a b. (a -> b) -> a -> b
$ CType -> Type
unCType CType
g of
      Just (TyCon
_, ThetaType
apps) -> do
        Bool
-> Judgement
-> ConLike
-> ThetaType
-> RuleT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     (Synthesized (LHsExpr GhcPs))
buildDataCon Bool
True (Judgement -> Judgement
unwhitelistingSplit Judgement
jdg) ConLike
dc ThetaType
apps
      Maybe (TyCon, ThetaType)
Nothing -> RuleT
  Judgement
  (Synthesized (LHsExpr GhcPs))
  TacticError
  TacticState
  ExtractM
  (Synthesized (LHsExpr GhcPs))
forall jdg ext err s (m :: * -> *) a. RuleT jdg ext err s m a
cut -- failure $ GoalMismatch "splitDataCon" g

------------------------------------------------------------------------------
-- | Attempt to instantiate the given data constructor to solve the goal.
--
-- INVARIANT: Assumes the given datacon is appropriate to construct the type
-- with.
splitDataCon :: DataCon -> TacticsM ()
splitDataCon :: DataCon -> TacticsM ()
splitDataCon = ConLike -> TacticsM ()
splitConLike (ConLike -> TacticsM ())
-> (DataCon -> ConLike) -> DataCon -> TacticsM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DataCon -> ConLike
RealDataCon


------------------------------------------------------------------------------
-- | Perform a case split on each top-level argument. Used to implement the
-- "Destruct all function arguments" action.
destructAll :: TacticsM ()
destructAll :: TacticsM ()
destructAll = do
  Judgement
jdg <- TacticT
  Judgement
  (Synthesized (LHsExpr GhcPs))
  TacticError
  TacticState
  ExtractM
  Judgement
forall (m :: * -> *) jdg ext err s.
Functor m =>
TacticT jdg ext err s m jdg
goal
  let args :: [HyInfo CType]
args = ((HyInfo CType, Int) -> HyInfo CType)
-> [(HyInfo CType, Int)] -> [HyInfo CType]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (HyInfo CType, Int) -> HyInfo CType
forall a b. (a, b) -> a
fst
           ([(HyInfo CType, Int)] -> [HyInfo CType])
-> [(HyInfo CType, Int)] -> [HyInfo CType]
forall a b. (a -> b) -> a -> b
$ ((HyInfo CType, Int) -> Int)
-> [(HyInfo CType, Int)] -> [(HyInfo CType, Int)]
forall b a. Ord b => (a -> b) -> [a] -> [a]
sortOn (HyInfo CType, Int) -> Int
forall a b. (a, b) -> b
snd
           ([(HyInfo CType, Int)] -> [(HyInfo CType, Int)])
-> [(HyInfo CType, Int)] -> [(HyInfo CType, Int)]
forall a b. (a -> b) -> a -> b
$ ((HyInfo CType, Provenance) -> Maybe (HyInfo CType, Int))
-> [(HyInfo CType, Provenance)] -> [(HyInfo CType, Int)]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (\(HyInfo CType
hi, Provenance
prov) ->
              case Provenance
prov of
                TopLevelArgPrv OccName
_ Int
idx Int
_ -> (HyInfo CType, Int) -> Maybe (HyInfo CType, Int)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (HyInfo CType
hi, Int
idx)
                Provenance
_ -> Maybe (HyInfo CType, Int)
forall a. Maybe a
Nothing
                )
           ([(HyInfo CType, Provenance)] -> [(HyInfo CType, Int)])
-> [(HyInfo CType, Provenance)] -> [(HyInfo CType, Int)]
forall a b. (a -> b) -> a -> b
$ (HyInfo CType -> (HyInfo CType, Provenance))
-> [HyInfo CType] -> [(HyInfo CType, Provenance)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\HyInfo CType
hi -> (HyInfo CType
hi, HyInfo CType -> Provenance
forall a. HyInfo a -> Provenance
hi_provenance HyInfo CType
hi))
           ([HyInfo CType] -> [(HyInfo CType, Provenance)])
-> [HyInfo CType] -> [(HyInfo CType, Provenance)]
forall a b. (a -> b) -> a -> b
$ (HyInfo CType -> Bool) -> [HyInfo CType] -> [HyInfo CType]
forall a. (a -> Bool) -> [a] -> [a]
filter (Type -> Bool
isAlgType (Type -> Bool) -> (HyInfo CType -> Type) -> HyInfo CType -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CType -> Type
unCType (CType -> Type) -> (HyInfo CType -> CType) -> HyInfo CType -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HyInfo CType -> CType
forall a. HyInfo a -> a
hi_type)
           ([HyInfo CType] -> [HyInfo CType])
-> [HyInfo CType] -> [HyInfo CType]
forall a b. (a -> b) -> a -> b
$ Hypothesis CType -> [HyInfo CType]
forall a. Hypothesis a -> [HyInfo a]
unHypothesis
           (Hypothesis CType -> [HyInfo CType])
-> Hypothesis CType -> [HyInfo CType]
forall a b. (a -> b) -> a -> b
$ Judgement -> Hypothesis CType
forall a. Judgement' a -> Hypothesis a
jHypothesis Judgement
jdg
  [HyInfo CType] -> (HyInfo CType -> TacticsM ()) -> TacticsM ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
t a -> (a -> f b) -> f ()
for_ [HyInfo CType]
args ((HyInfo CType -> TacticsM ()) -> TacticsM ())
-> (HyInfo CType -> TacticsM ()) -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ \HyInfo CType
arg -> do
    TCvSubst
subst <- Judgement
-> TacticT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     TCvSubst
forall (m :: * -> *).
MonadState TacticState m =>
Judgement -> m TCvSubst
getSubstForJudgement (Judgement
 -> TacticT
      Judgement
      (Synthesized (LHsExpr GhcPs))
      TacticError
      TacticState
      ExtractM
      TCvSubst)
-> TacticT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     Judgement
-> TacticT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     TCvSubst
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TacticT
  Judgement
  (Synthesized (LHsExpr GhcPs))
  TacticError
  TacticState
  ExtractM
  Judgement
forall (m :: * -> *) jdg ext err s.
Functor m =>
TacticT jdg ext err s m jdg
goal
    HyInfo CType -> TacticsM ()
destruct (HyInfo CType -> TacticsM ()) -> HyInfo CType -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ (CType -> CType) -> HyInfo CType -> HyInfo CType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((TCvSubst -> Type -> Type) -> TCvSubst -> CType -> CType
coerce HasCallStack => TCvSubst -> Type -> Type
TCvSubst -> Type -> Type
substTy TCvSubst
subst) HyInfo CType
arg

--------------------------------------------------------------------------------
-- | User-facing tactic to implement "Use constructor <x>"
userSplit :: OccName -> TacticsM ()
userSplit :: OccName -> TacticsM ()
userSplit OccName
occ = do
  Judgement
jdg <- TacticT
  Judgement
  (Synthesized (LHsExpr GhcPs))
  TacticError
  TacticState
  ExtractM
  Judgement
forall (m :: * -> *) jdg ext err s.
Functor m =>
TacticT jdg ext err s m jdg
goal
  let g :: CType
g = Judgement -> CType
forall a. Judgement' a -> a
jGoal Judgement
jdg
  -- TODO(sandy): It's smelly that we need to find the datacon to generate the
  -- code action, send it as a string, and then look it up again. Can we push
  -- this over LSP somehow instead?
  case HasDebugCallStack => Type -> Maybe (TyCon, ThetaType)
Type -> Maybe (TyCon, ThetaType)
splitTyConApp_maybe (Type -> Maybe (TyCon, ThetaType))
-> Type -> Maybe (TyCon, ThetaType)
forall a b. (a -> b) -> a -> b
$ CType -> Type
unCType CType
g of
    Just (TyCon
tc, ThetaType
_) -> do
      case (DataCon -> Bool) -> [DataCon] -> Maybe DataCon
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find (OccName -> OccName -> Bool
sloppyEqOccName OccName
occ (OccName -> Bool) -> (DataCon -> OccName) -> DataCon -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> OccName
forall name. HasOccName name => name -> OccName
occName (Name -> OccName) -> (DataCon -> Name) -> DataCon -> OccName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DataCon -> Name
dataConName)
             ([DataCon] -> Maybe DataCon) -> [DataCon] -> Maybe DataCon
forall a b. (a -> b) -> a -> b
$ TyCon -> [DataCon]
tyConDataCons TyCon
tc of
        Just DataCon
dc -> DataCon -> TacticsM ()
splitDataCon DataCon
dc
        Maybe DataCon
Nothing -> TacticError -> TacticsM ()
forall err jdg ext s (m :: * -> *) a.
err -> TacticT jdg ext err s m a
failure (TacticError -> TacticsM ()) -> TacticError -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ OccName -> TacticError
NotInScope OccName
occ
    Maybe (TyCon, ThetaType)
Nothing -> TacticError -> TacticsM ()
forall err jdg ext s (m :: * -> *) a.
err -> TacticT jdg ext err s m a
failure (TacticError -> TacticsM ()) -> TacticError -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ OccName -> TacticError
NotInScope OccName
occ


------------------------------------------------------------------------------
-- | @matching f@ takes a function from a judgement to a @Tactic@, and
-- then applies the resulting @Tactic@.
matching :: (Judgement -> TacticsM ()) -> TacticsM ()
matching :: (Judgement -> TacticsM ()) -> TacticsM ()
matching Judgement -> TacticsM ()
f = StateT
  Judgement
  (ProofStateT
     (Synthesized (LHsExpr GhcPs))
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM)
  ()
-> TacticsM ()
forall jdg ext err s (m :: * -> *) a.
StateT jdg (ProofStateT ext ext err s m) a
-> TacticT jdg ext err s m a
TacticT (StateT
   Judgement
   (ProofStateT
      (Synthesized (LHsExpr GhcPs))
      (Synthesized (LHsExpr GhcPs))
      TacticError
      TacticState
      ExtractM)
   ()
 -> TacticsM ())
-> StateT
     Judgement
     (ProofStateT
        (Synthesized (LHsExpr GhcPs))
        (Synthesized (LHsExpr GhcPs))
        TacticError
        TacticState
        ExtractM)
     ()
-> TacticsM ()
forall a b. (a -> b) -> a -> b
$ (Judgement
 -> ProofStateT
      (Synthesized (LHsExpr GhcPs))
      (Synthesized (LHsExpr GhcPs))
      TacticError
      TacticState
      ExtractM
      ((), Judgement))
-> StateT
     Judgement
     (ProofStateT
        (Synthesized (LHsExpr GhcPs))
        (Synthesized (LHsExpr GhcPs))
        TacticError
        TacticState
        ExtractM)
     ()
forall s (m :: * -> *) a. (s -> m (a, s)) -> StateT s m a
StateT ((Judgement
  -> ProofStateT
       (Synthesized (LHsExpr GhcPs))
       (Synthesized (LHsExpr GhcPs))
       TacticError
       TacticState
       ExtractM
       ((), Judgement))
 -> StateT
      Judgement
      (ProofStateT
         (Synthesized (LHsExpr GhcPs))
         (Synthesized (LHsExpr GhcPs))
         TacticError
         TacticState
         ExtractM)
      ())
-> (Judgement
    -> ProofStateT
         (Synthesized (LHsExpr GhcPs))
         (Synthesized (LHsExpr GhcPs))
         TacticError
         TacticState
         ExtractM
         ((), Judgement))
-> StateT
     Judgement
     (ProofStateT
        (Synthesized (LHsExpr GhcPs))
        (Synthesized (LHsExpr GhcPs))
        TacticError
        TacticState
        ExtractM)
     ()
forall a b. (a -> b) -> a -> b
$ \Judgement
s -> StateT
  Judgement
  (ProofStateT
     (Synthesized (LHsExpr GhcPs))
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM)
  ()
-> Judgement
-> ProofStateT
     (Synthesized (LHsExpr GhcPs))
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     ((), Judgement)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT (TacticsM ()
-> StateT
     Judgement
     (ProofStateT
        (Synthesized (LHsExpr GhcPs))
        (Synthesized (LHsExpr GhcPs))
        TacticError
        TacticState
        ExtractM)
     ()
forall jdg ext err s (m :: * -> *) a.
TacticT jdg ext err s m a
-> StateT jdg (ProofStateT ext ext err s m) a
unTacticT (TacticsM ()
 -> StateT
      Judgement
      (ProofStateT
         (Synthesized (LHsExpr GhcPs))
         (Synthesized (LHsExpr GhcPs))
         TacticError
         TacticState
         ExtractM)
      ())
-> TacticsM ()
-> StateT
     Judgement
     (ProofStateT
        (Synthesized (LHsExpr GhcPs))
        (Synthesized (LHsExpr GhcPs))
        TacticError
        TacticState
        ExtractM)
     ()
forall a b. (a -> b) -> a -> b
$ Judgement -> TacticsM ()
f Judgement
s) Judgement
s


attemptOn :: (Judgement -> [a]) -> (a -> TacticsM ()) -> TacticsM ()
attemptOn :: (Judgement -> [a]) -> (a -> TacticsM ()) -> TacticsM ()
attemptOn Judgement -> [a]
getNames a -> TacticsM ()
tac = (Judgement -> TacticsM ()) -> TacticsM ()
matching ([TacticsM ()] -> TacticsM ()
forall (m :: * -> *) jdg ext err s a.
Monad m =>
[TacticT jdg ext err s m a] -> TacticT jdg ext err s m a
choice ([TacticsM ()] -> TacticsM ())
-> (Judgement -> [TacticsM ()]) -> Judgement -> TacticsM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> TacticsM ()) -> [a] -> [TacticsM ()]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\a
s -> a -> TacticsM ()
tac a
s) ([a] -> [TacticsM ()])
-> (Judgement -> [a]) -> Judgement -> [TacticsM ()]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Judgement -> [a]
getNames)


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


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


auto' :: Int -> TacticsM ()
auto' :: Int -> TacticsM ()
auto' Int
0 = TacticError -> TacticsM ()
forall err jdg ext s (m :: * -> *) a.
err -> TacticT jdg ext err s m a
failure TacticError
OutOfGas
auto' Int
n = do
  let loop :: TacticsM ()
loop = Int -> TacticsM ()
auto' (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)
  TacticsM () -> TacticsM ()
forall (m :: * -> *) jdg ext err s.
Monad m =>
TacticT jdg ext err s m () -> TacticT jdg ext err s m ()
try TacticsM ()
intros
  TacticsM ()
assumption TacticsM () -> TacticsM () -> TacticsM ()
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|>
    [TacticsM ()] -> TacticsM ()
forall (m :: * -> *) jdg ext err s a.
Monad m =>
[TacticT jdg ext err s m a] -> TacticT jdg ext err s m a
choice
      [ (HyInfo CType -> TacticsM ()) -> TacticsM ()
overFunctions ((HyInfo CType -> TacticsM ()) -> TacticsM ())
-> (HyInfo CType -> TacticsM ()) -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ \HyInfo CType
fname -> do
          TacticsM () -> TacticsM ()
forall a. TacticsM a -> TacticsM a
requireConcreteHole (TacticsM () -> TacticsM ()) -> TacticsM () -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ Saturation -> HyInfo CType -> TacticsM ()
apply Saturation
Saturated HyInfo CType
fname
          TacticsM ()
loop
      , (HyInfo CType -> TacticsM ()) -> TacticsM ()
overAlgebraicTerms ((HyInfo CType -> TacticsM ()) -> TacticsM ())
-> (HyInfo CType -> TacticsM ()) -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ \HyInfo CType
aname -> do
          HyInfo CType -> TacticsM ()
destructAuto HyInfo CType
aname
          TacticsM ()
loop
      , TacticsM ()
splitAuto TacticsM () -> TacticsM () -> TacticsM ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> TacticsM ()
loop
      , TacticsM ()
recursion
      ]

overFunctions :: (HyInfo CType -> TacticsM ()) -> TacticsM ()
overFunctions :: (HyInfo CType -> TacticsM ()) -> TacticsM ()
overFunctions =
  (Judgement -> [HyInfo CType])
-> (HyInfo CType -> TacticsM ()) -> TacticsM ()
forall a. (Judgement -> [a]) -> (a -> TacticsM ()) -> TacticsM ()
attemptOn ((Judgement -> [HyInfo CType])
 -> (HyInfo CType -> TacticsM ()) -> TacticsM ())
-> (Judgement -> [HyInfo CType])
-> (HyInfo CType -> TacticsM ())
-> TacticsM ()
forall a b. (a -> b) -> a -> b
$ (HyInfo CType -> Bool) -> [HyInfo CType] -> [HyInfo CType]
forall a. (a -> Bool) -> [a] -> [a]
filter (Type -> Bool
isFunction (Type -> Bool) -> (HyInfo CType -> Type) -> HyInfo CType -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CType -> Type
unCType (CType -> Type) -> (HyInfo CType -> CType) -> HyInfo CType -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HyInfo CType -> CType
forall a. HyInfo a -> a
hi_type)
           ([HyInfo CType] -> [HyInfo CType])
-> (Judgement -> [HyInfo CType]) -> Judgement -> [HyInfo CType]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Hypothesis CType -> [HyInfo CType]
forall a. Hypothesis a -> [HyInfo a]
unHypothesis
           (Hypothesis CType -> [HyInfo CType])
-> (Judgement -> Hypothesis CType) -> Judgement -> [HyInfo CType]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Judgement -> Hypothesis CType
forall a. Judgement' a -> Hypothesis a
jHypothesis

overAlgebraicTerms :: (HyInfo CType -> TacticsM ()) -> TacticsM ()
overAlgebraicTerms :: (HyInfo CType -> TacticsM ()) -> TacticsM ()
overAlgebraicTerms =
  (Judgement -> [HyInfo CType])
-> (HyInfo CType -> TacticsM ()) -> TacticsM ()
forall a. (Judgement -> [a]) -> (a -> TacticsM ()) -> TacticsM ()
attemptOn Judgement -> [HyInfo CType]
jAcceptableDestructTargets


allNames :: Judgement -> Set OccName
allNames :: Judgement -> Set OccName
allNames = Hypothesis CType -> Set OccName
forall a. Hypothesis a -> Set OccName
hyNamesInScope (Hypothesis CType -> Set OccName)
-> (Judgement -> Hypothesis CType) -> Judgement -> Set OccName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Judgement -> Hypothesis CType
forall a. Judgement' a -> Hypothesis a
jHypothesis


applyMethod :: Class -> PredType -> OccName -> TacticsM ()
applyMethod :: Class -> Type -> OccName -> TacticsM ()
applyMethod Class
cls Type
df OccName
method_name = do
  case (TyVar -> Bool) -> [TyVar] -> Maybe TyVar
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find ((OccName -> OccName -> Bool
forall a. Eq a => a -> a -> Bool
== OccName
method_name) (OccName -> Bool) -> (TyVar -> OccName) -> TyVar -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyVar -> OccName
forall name. HasOccName name => name -> OccName
occName) ([TyVar] -> Maybe TyVar) -> [TyVar] -> Maybe TyVar
forall a b. (a -> b) -> a -> b
$ Class -> [TyVar]
classMethods Class
cls of
    Just TyVar
method -> do
      let (Type
_, ThetaType
apps) = Type -> (Type, ThetaType)
splitAppTys Type
df
      let ty :: Type
ty = HasDebugCallStack => Type -> ThetaType -> Type
Type -> ThetaType -> Type
piResultTys (TyVar -> Type
idType TyVar
method) ThetaType
apps
      Saturation -> HyInfo CType -> TacticsM ()
apply Saturation
Saturated (HyInfo CType -> TacticsM ()) -> HyInfo CType -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ OccName -> Provenance -> CType -> HyInfo CType
forall a. OccName -> Provenance -> a -> HyInfo a
HyInfo OccName
method_name (Uniquely Class -> Provenance
ClassMethodPrv (Uniquely Class -> Provenance) -> Uniquely Class -> Provenance
forall a b. (a -> b) -> a -> b
$ Class -> Uniquely Class
forall a. a -> Uniquely a
Uniquely Class
cls) (CType -> HyInfo CType) -> CType -> HyInfo CType
forall a b. (a -> b) -> a -> b
$ Type -> CType
CType Type
ty
    Maybe TyVar
Nothing -> TacticError -> TacticsM ()
forall err jdg ext s (m :: * -> *) a.
err -> TacticT jdg ext err s m a
failure (TacticError -> TacticsM ()) -> TacticError -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ OccName -> TacticError
NotInScope OccName
method_name


applyByName :: OccName -> TacticsM ()
applyByName :: OccName -> TacticsM ()
applyByName OccName
name = do
  Judgement
g <- TacticT
  Judgement
  (Synthesized (LHsExpr GhcPs))
  TacticError
  TacticState
  ExtractM
  Judgement
forall (m :: * -> *) jdg ext err s.
Functor m =>
TacticT jdg ext err s m jdg
goal
  [TacticsM ()] -> TacticsM ()
forall (m :: * -> *) jdg ext err s a.
Monad m =>
[TacticT jdg ext err s m a] -> TacticT jdg ext err s m a
choice ([TacticsM ()] -> TacticsM ()) -> [TacticsM ()] -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ (Hypothesis CType -> [HyInfo CType]
forall a. Hypothesis a -> [HyInfo a]
unHypothesis (Judgement -> Hypothesis CType
forall a. Judgement' a -> Hypothesis a
jHypothesis Judgement
g)) [HyInfo CType] -> (HyInfo CType -> TacticsM ()) -> [TacticsM ()]
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \HyInfo CType
hi ->
    case HyInfo CType -> OccName
forall a. HyInfo a -> OccName
hi_name HyInfo CType
hi OccName -> OccName -> Bool
forall a. Eq a => a -> a -> Bool
== OccName
name of
      Bool
True  -> Saturation -> HyInfo CType -> TacticsM ()
apply Saturation
Saturated HyInfo CType
hi
      Bool
False -> TacticsM ()
forall (f :: * -> *) a. Alternative f => f a
empty


------------------------------------------------------------------------------
-- | Make a function application where the function being applied itself is
-- a hole.
applyByType :: Type -> TacticsM ()
applyByType :: Type -> TacticsM ()
applyByType Type
ty = String -> TacticsM () -> TacticsM ()
forall (m :: * -> *) jdg ext err s a.
Functor m =>
String
-> TacticT jdg (Synthesized ext) err s m a
-> TacticT jdg (Synthesized ext) err s m a
tracing (String
"applyByType " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Type -> String
forall a. Show a => a -> String
show Type
ty) (TacticsM () -> TacticsM ()) -> TacticsM () -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ do
  Judgement
jdg <- TacticT
  Judgement
  (Synthesized (LHsExpr GhcPs))
  TacticError
  TacticState
  ExtractM
  Judgement
forall (m :: * -> *) jdg ext err s.
Functor m =>
TacticT jdg ext err s m jdg
goal
  let g :: CType
g  = Judgement -> CType
forall a. Judgement' a -> a
jGoal Judgement
jdg
  Type
ty' <- Type
-> TacticT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     Type
forall (m :: * -> *). MonadState TacticState m => Type -> m Type
freshTyvars Type
ty
  let ([TyVar]
_, ThetaType
_, ThetaType
args, Type
ret) = Type -> ([TyVar], ThetaType, ThetaType, Type)
tacticsSplitFunTy Type
ty'
  (Judgement
 -> RuleT
      Judgement
      (Synthesized (LHsExpr GhcPs))
      TacticError
      TacticState
      ExtractM
      (Synthesized (LHsExpr GhcPs)))
-> TacticsM ()
forall (m :: * -> *) jdg ext err s.
Monad m =>
(jdg -> RuleT jdg ext err s m ext) -> TacticT jdg ext err s m ()
rule ((Judgement
  -> RuleT
       Judgement
       (Synthesized (LHsExpr GhcPs))
       TacticError
       TacticState
       ExtractM
       (Synthesized (LHsExpr GhcPs)))
 -> TacticsM ())
-> (Judgement
    -> RuleT
         Judgement
         (Synthesized (LHsExpr GhcPs))
         TacticError
         TacticState
         ExtractM
         (Synthesized (LHsExpr GhcPs)))
-> TacticsM ()
forall a b. (a -> b) -> a -> b
$ \Judgement
jdg -> do
    CType -> CType -> RuleM ()
unify CType
g (Type -> CType
CType Type
ret)
    Synthesized [LHsExpr GhcPs]
ext
        <- ([Synthesized (LHsExpr GhcPs)] -> Synthesized [LHsExpr GhcPs])
-> RuleT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     [Synthesized (LHsExpr GhcPs)]
-> RuleT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     (Synthesized [LHsExpr GhcPs])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [Synthesized (LHsExpr GhcPs)] -> Synthesized [LHsExpr GhcPs]
forall a. [Synthesized a] -> Synthesized [a]
unzipTrace
        (RuleT
   Judgement
   (Synthesized (LHsExpr GhcPs))
   TacticError
   TacticState
   ExtractM
   [Synthesized (LHsExpr GhcPs)]
 -> RuleT
      Judgement
      (Synthesized (LHsExpr GhcPs))
      TacticError
      TacticState
      ExtractM
      (Synthesized [LHsExpr GhcPs]))
-> RuleT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     [Synthesized (LHsExpr GhcPs)]
-> RuleT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     (Synthesized [LHsExpr GhcPs])
forall a b. (a -> b) -> a -> b
$ (Type
 -> RuleT
      Judgement
      (Synthesized (LHsExpr GhcPs))
      TacticError
      TacticState
      ExtractM
      (Synthesized (LHsExpr GhcPs)))
-> ThetaType
-> RuleT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     [Synthesized (LHsExpr GhcPs)]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse ( Judgement
-> RuleT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     (Synthesized (LHsExpr GhcPs))
newSubgoal
                    (Judgement
 -> RuleT
      Judgement
      (Synthesized (LHsExpr GhcPs))
      TacticError
      TacticState
      ExtractM
      (Synthesized (LHsExpr GhcPs)))
-> (Type -> Judgement)
-> Type
-> RuleT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     (Synthesized (LHsExpr GhcPs))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Judgement -> Judgement
blacklistingDestruct
                    (Judgement -> Judgement)
-> (Type -> Judgement) -> Type -> Judgement
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (CType -> Judgement -> Judgement)
-> Judgement -> CType -> Judgement
forall a b c. (a -> b -> c) -> b -> a -> c
flip CType -> Judgement -> Judgement
forall a. a -> Judgement' a -> Judgement' a
withNewGoal Judgement
jdg
                    (CType -> Judgement) -> (Type -> CType) -> Type -> Judgement
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> CType
CType
                    ) ThetaType
args
    Synthesized (LHsExpr GhcPs)
app <- Judgement
-> RuleT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     (Synthesized (LHsExpr GhcPs))
newSubgoal (Judgement
 -> RuleT
      Judgement
      (Synthesized (LHsExpr GhcPs))
      TacticError
      TacticState
      ExtractM
      (Synthesized (LHsExpr GhcPs)))
-> (Judgement -> Judgement)
-> Judgement
-> RuleT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     (Synthesized (LHsExpr GhcPs))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Judgement -> Judgement
blacklistingDestruct (Judgement
 -> RuleT
      Judgement
      (Synthesized (LHsExpr GhcPs))
      TacticError
      TacticState
      ExtractM
      (Synthesized (LHsExpr GhcPs)))
-> Judgement
-> RuleT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     (Synthesized (LHsExpr GhcPs))
forall a b. (a -> b) -> a -> b
$ CType -> Judgement -> Judgement
forall a. a -> Judgement' a -> Judgement' a
withNewGoal (Type -> CType
CType Type
ty) Judgement
jdg
    Synthesized (LHsExpr GhcPs)
-> RuleT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     (Synthesized (LHsExpr GhcPs))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Synthesized (LHsExpr GhcPs)
 -> RuleT
      Judgement
      (Synthesized (LHsExpr GhcPs))
      TacticError
      TacticState
      ExtractM
      (Synthesized (LHsExpr GhcPs)))
-> Synthesized (LHsExpr GhcPs)
-> RuleT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     (Synthesized (LHsExpr GhcPs))
forall a b. (a -> b) -> a -> b
$
      (HsExpr GhcPs -> LHsExpr GhcPs)
-> Synthesized (HsExpr GhcPs) -> Synthesized (LHsExpr GhcPs)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap HsExpr GhcPs -> LHsExpr GhcPs
forall a. HasSrcSpan a => SrcSpanLess a -> a
noLoc (Synthesized (HsExpr GhcPs) -> Synthesized (LHsExpr GhcPs))
-> Synthesized (HsExpr GhcPs) -> Synthesized (LHsExpr GhcPs)
forall a b. (a -> b) -> a -> b
$
        (HsExpr GhcPs -> HsExpr GhcPs -> HsExpr GhcPs)
-> HsExpr GhcPs -> [HsExpr GhcPs] -> HsExpr GhcPs
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' HsExpr GhcPs -> HsExpr GhcPs -> HsExpr GhcPs
forall e. App e => e -> e -> e
(@@)
          (HsExpr GhcPs -> [HsExpr GhcPs] -> HsExpr GhcPs)
-> Synthesized (HsExpr GhcPs)
-> Synthesized ([HsExpr GhcPs] -> HsExpr GhcPs)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (LHsExpr GhcPs -> HsExpr GhcPs)
-> Synthesized (LHsExpr GhcPs) -> Synthesized (HsExpr GhcPs)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap LHsExpr GhcPs -> HsExpr GhcPs
forall a. HasSrcSpan a => a -> SrcSpanLess a
unLoc Synthesized (LHsExpr GhcPs)
app
          Synthesized ([HsExpr GhcPs] -> HsExpr GhcPs)
-> Synthesized [HsExpr GhcPs] -> Synthesized (HsExpr GhcPs)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ([LHsExpr GhcPs] -> [HsExpr GhcPs])
-> Synthesized [LHsExpr GhcPs] -> Synthesized [HsExpr GhcPs]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((LHsExpr GhcPs -> HsExpr GhcPs)
-> [LHsExpr GhcPs] -> [HsExpr GhcPs]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap LHsExpr GhcPs -> HsExpr GhcPs
forall a. HasSrcSpan a => a -> SrcSpanLess a
unLoc) Synthesized [LHsExpr GhcPs]
ext


------------------------------------------------------------------------------
-- | Make an n-ary function call of the form
-- @(_ :: forall a b. a -> a -> b) _ _@.
nary :: Int -> TacticsM ()
nary :: Int -> TacticsM ()
nary Int
n = do
  Type
a <- TacticT
  Judgement
  (Synthesized (LHsExpr GhcPs))
  TacticError
  TacticState
  ExtractM
  Type
forall (m :: * -> *). MonadState TacticState m => m Type
newUnivar
  Type
b <- TacticT
  Judgement
  (Synthesized (LHsExpr GhcPs))
  TacticError
  TacticState
  ExtractM
  Type
forall (m :: * -> *). MonadState TacticState m => m Type
newUnivar
  Type -> TacticsM ()
applyByType (Type -> TacticsM ()) -> Type -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ ThetaType -> Type -> Type
mkFunTys' (Int -> Type -> ThetaType
forall a. Int -> a -> [a]
replicate Int
n Type
a) Type
b


self :: TacticsM ()
self :: TacticsM ()
self =
  ([(OccName, CType)] -> Maybe (OccName, CType))
-> TacticsM [(OccName, CType)]
-> TacticT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     (Maybe (OccName, CType))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [(OccName, CType)] -> Maybe (OccName, CType)
forall a. [a] -> Maybe a
listToMaybe TacticsM [(OccName, CType)]
getCurrentDefinitions TacticT
  Judgement
  (Synthesized (LHsExpr GhcPs))
  TacticError
  TacticState
  ExtractM
  (Maybe (OccName, CType))
-> (Maybe (OccName, CType) -> TacticsM ()) -> TacticsM ()
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Just (OccName
self, CType
_) -> (HyInfo CType -> TacticsM ()) -> OccName -> TacticsM ()
forall a. (HyInfo CType -> TacticsM a) -> OccName -> TacticsM a
useNameFromContext (Saturation -> HyInfo CType -> TacticsM ()
apply Saturation
Saturated) OccName
self
    Maybe (OccName, CType)
Nothing -> TacticError -> TacticsM ()
forall err jdg ext s (m :: * -> *) a.
err -> TacticT jdg ext err s m a
failure (TacticError -> TacticsM ()) -> TacticError -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ String -> TacticError
TacticPanic String
"no defining function"


------------------------------------------------------------------------------
-- | Perform a catamorphism when destructing the given 'HyInfo'. This will
-- result in let binding, making values that call the defining function on each
-- destructed value.
cata :: HyInfo CType -> TacticsM ()
cata :: HyInfo CType -> TacticsM ()
cata HyInfo CType
hi = do
  ([TyVar]
_, ThetaType
_, ThetaType
calling_args, Type
_)
      <- Type -> ([TyVar], ThetaType, ThetaType, Type)
tacticsSplitFunTy (Type -> ([TyVar], ThetaType, ThetaType, Type))
-> (CType -> Type)
-> CType
-> ([TyVar], ThetaType, ThetaType, Type)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CType -> Type
unCType (CType -> ([TyVar], ThetaType, ThetaType, Type))
-> TacticT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     CType
-> TacticT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     ([TyVar], ThetaType, ThetaType, Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TacticT
  Judgement
  (Synthesized (LHsExpr GhcPs))
  TacticError
  TacticState
  ExtractM
  CType
getDefiningType
  ThetaType
freshened_args <- (Type
 -> TacticT
      Judgement
      (Synthesized (LHsExpr GhcPs))
      TacticError
      TacticState
      ExtractM
      Type)
-> ThetaType
-> TacticT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     ThetaType
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse Type
-> TacticT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     Type
forall (m :: * -> *). MonadState TacticState m => Type -> m Type
freshTyvars ThetaType
calling_args
  Hypothesis CType
diff <- TacticsM ()
-> TacticT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     (Hypothesis CType)
hyDiff (TacticsM ()
 -> TacticT
      Judgement
      (Synthesized (LHsExpr GhcPs))
      TacticError
      TacticState
      ExtractM
      (Hypothesis CType))
-> TacticsM ()
-> TacticT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     (Hypothesis CType)
forall a b. (a -> b) -> a -> b
$ HyInfo CType -> TacticsM ()
destruct HyInfo CType
hi

  -- For for every destructed term, check to see if it can unify with any of
  -- the arguments to the calling function. If it doesn't, we don't try to
  -- perform a cata on it.
  [HyInfo CType]
unifiable_diff <- ((HyInfo CType
  -> TacticT
       Judgement
       (Synthesized (LHsExpr GhcPs))
       TacticError
       TacticState
       ExtractM
       Bool)
 -> [HyInfo CType]
 -> TacticT
      Judgement
      (Synthesized (LHsExpr GhcPs))
      TacticError
      TacticState
      ExtractM
      [HyInfo CType])
-> [HyInfo CType]
-> (HyInfo CType
    -> TacticT
         Judgement
         (Synthesized (LHsExpr GhcPs))
         TacticError
         TacticState
         ExtractM
         Bool)
-> TacticT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     [HyInfo CType]
forall a b c. (a -> b -> c) -> b -> a -> c
flip (HyInfo CType
 -> TacticT
      Judgement
      (Synthesized (LHsExpr GhcPs))
      TacticError
      TacticState
      ExtractM
      Bool)
-> [HyInfo CType]
-> TacticT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     [HyInfo CType]
forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
filterM (Hypothesis CType -> [HyInfo CType]
forall a. Hypothesis a -> [HyInfo a]
unHypothesis Hypothesis CType
diff) ((HyInfo CType
  -> TacticT
       Judgement
       (Synthesized (LHsExpr GhcPs))
       TacticError
       TacticState
       ExtractM
       Bool)
 -> TacticT
      Judgement
      (Synthesized (LHsExpr GhcPs))
      TacticError
      TacticState
      ExtractM
      [HyInfo CType])
-> (HyInfo CType
    -> TacticT
         Judgement
         (Synthesized (LHsExpr GhcPs))
         TacticError
         TacticState
         ExtractM
         Bool)
-> TacticT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     [HyInfo CType]
forall a b. (a -> b) -> a -> b
$ \HyInfo CType
hi ->
    ((Type
  -> TacticT
       Judgement
       (Synthesized (LHsExpr GhcPs))
       TacticError
       TacticState
       ExtractM
       Bool)
 -> ThetaType
 -> TacticT
      Judgement
      (Synthesized (LHsExpr GhcPs))
      TacticError
      TacticState
      ExtractM
      Bool)
-> ThetaType
-> (Type
    -> TacticT
         Judgement
         (Synthesized (LHsExpr GhcPs))
         TacticError
         TacticState
         ExtractM
         Bool)
-> TacticT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     Bool
forall a b c. (a -> b -> c) -> b -> a -> c
flip (Type
 -> TacticT
      Judgement
      (Synthesized (LHsExpr GhcPs))
      TacticError
      TacticState
      ExtractM
      Bool)
-> ThetaType
-> TacticT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     Bool
forall (m :: * -> *) a. Monad m => (a -> m Bool) -> [a] -> m Bool
anyM ThetaType
freshened_args ((Type
  -> TacticT
       Judgement
       (Synthesized (LHsExpr GhcPs))
       TacticError
       TacticState
       ExtractM
       Bool)
 -> TacticT
      Judgement
      (Synthesized (LHsExpr GhcPs))
      TacticError
      TacticState
      ExtractM
      Bool)
-> (Type
    -> TacticT
         Judgement
         (Synthesized (LHsExpr GhcPs))
         TacticError
         TacticState
         ExtractM
         Bool)
-> TacticT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     Bool
forall a b. (a -> b) -> a -> b
$ \Type
ty ->
      CType
-> CType
-> TacticT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     Bool
forall (m :: * -> *).
MonadState TacticState m =>
CType -> CType -> m Bool
canUnify (HyInfo CType -> CType
forall a. HyInfo a -> a
hi_type HyInfo CType
hi) (CType
 -> TacticT
      Judgement
      (Synthesized (LHsExpr GhcPs))
      TacticError
      TacticState
      ExtractM
      Bool)
-> CType
-> TacticT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     Bool
forall a b. (a -> b) -> a -> b
$ Type -> CType
CType Type
ty

  (Judgement
 -> RuleT
      Judgement
      (Synthesized (LHsExpr GhcPs))
      TacticError
      TacticState
      ExtractM
      (Synthesized (LHsExpr GhcPs)))
-> TacticsM ()
forall (m :: * -> *) jdg ext err s.
Monad m =>
(jdg -> RuleT jdg ext err s m ext) -> TacticT jdg ext err s m ()
rule ((Judgement
  -> RuleT
       Judgement
       (Synthesized (LHsExpr GhcPs))
       TacticError
       TacticState
       ExtractM
       (Synthesized (LHsExpr GhcPs)))
 -> TacticsM ())
-> (Judgement
    -> RuleT
         Judgement
         (Synthesized (LHsExpr GhcPs))
         TacticError
         TacticState
         ExtractM
         (Synthesized (LHsExpr GhcPs)))
-> TacticsM ()
forall a b. (a -> b) -> a -> b
$
    (OccName -> OccName)
-> (HyInfo CType -> TacticsM ())
-> Hypothesis CType
-> Judgement
-> RuleT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     (Synthesized (LHsExpr GhcPs))
letForEach
      (String -> OccName
mkVarOcc (String -> OccName) -> (OccName -> String) -> OccName -> OccName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String -> String -> String) -> String -> String -> String
forall a b c. (a -> b -> c) -> b -> a -> c
flip String -> String -> String
forall a. Monoid a => a -> a -> a
mappend String
"_c" (String -> String) -> (OccName -> String) -> OccName -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OccName -> String
occNameString)
      (\HyInfo CType
hi -> TacticsM ()
self TacticsM () -> TacticsM () -> TacticsM ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> TacticsM () -> TacticsM () -> TacticsM ()
forall jdg ext err s (m :: * -> *) a.
TacticT jdg ext err s m a
-> TacticT jdg ext err s m a -> TacticT jdg ext err s m a
commit (OccName -> TacticsM ()
assume (OccName -> TacticsM ()) -> OccName -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ HyInfo CType -> OccName
forall a. HyInfo a -> OccName
hi_name HyInfo CType
hi) TacticsM ()
assumption)
      (Hypothesis CType
 -> Judgement
 -> RuleT
      Judgement
      (Synthesized (LHsExpr GhcPs))
      TacticError
      TacticState
      ExtractM
      (Synthesized (LHsExpr GhcPs)))
-> Hypothesis CType
-> Judgement
-> RuleT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     (Synthesized (LHsExpr GhcPs))
forall a b. (a -> b) -> a -> b
$ [HyInfo CType] -> Hypothesis CType
forall a. [HyInfo a] -> Hypothesis a
Hypothesis [HyInfo CType]
unifiable_diff


letBind :: [OccName] -> TacticsM ()
letBind :: [OccName] -> TacticsM ()
letBind [OccName]
occs = do
  Judgement
jdg <- TacticT
  Judgement
  (Synthesized (LHsExpr GhcPs))
  TacticError
  TacticState
  ExtractM
  Judgement
forall (m :: * -> *) jdg ext err s.
Functor m =>
TacticT jdg ext err s m jdg
goal
  [(OccName, Judgement)]
occ_tys <- [OccName]
-> (OccName
    -> TacticT
         Judgement
         (Synthesized (LHsExpr GhcPs))
         TacticError
         TacticState
         ExtractM
         (OccName, Judgement))
-> TacticT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     [(OccName, Judgement)]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for [OccName]
occs
           ((OccName
  -> TacticT
       Judgement
       (Synthesized (LHsExpr GhcPs))
       TacticError
       TacticState
       ExtractM
       (OccName, Judgement))
 -> TacticT
      Judgement
      (Synthesized (LHsExpr GhcPs))
      TacticError
      TacticState
      ExtractM
      [(OccName, Judgement)])
-> (OccName
    -> TacticT
         Judgement
         (Synthesized (LHsExpr GhcPs))
         TacticError
         TacticState
         ExtractM
         (OccName, Judgement))
-> TacticT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     [(OccName, Judgement)]
forall a b. (a -> b) -> a -> b
$ \OccName
occ
          -> (Judgement -> (OccName, Judgement))
-> TacticT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     Judgement
-> TacticT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     (OccName, Judgement)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (OccName
occ, )
           (TacticT
   Judgement
   (Synthesized (LHsExpr GhcPs))
   TacticError
   TacticState
   ExtractM
   Judgement
 -> TacticT
      Judgement
      (Synthesized (LHsExpr GhcPs))
      TacticError
      TacticState
      ExtractM
      (OccName, Judgement))
-> TacticT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     Judgement
-> TacticT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     (OccName, Judgement)
forall a b. (a -> b) -> a -> b
$ (CType -> Judgement)
-> TacticT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     CType
-> TacticT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     Judgement
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (CType -> Judgement -> Judgement
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Judgement
jdg)
           (TacticT
   Judgement
   (Synthesized (LHsExpr GhcPs))
   TacticError
   TacticState
   ExtractM
   CType
 -> TacticT
      Judgement
      (Synthesized (LHsExpr GhcPs))
      TacticError
      TacticState
      ExtractM
      Judgement)
-> TacticT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     CType
-> TacticT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     Judgement
forall a b. (a -> b) -> a -> b
$ (Type -> CType)
-> TacticT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     Type
-> TacticT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     CType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Type -> CType
CType
           (TacticT
   Judgement
   (Synthesized (LHsExpr GhcPs))
   TacticError
   TacticState
   ExtractM
   Type
 -> TacticT
      Judgement
      (Synthesized (LHsExpr GhcPs))
      TacticError
      TacticState
      ExtractM
      CType)
-> TacticT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     Type
-> TacticT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     CType
forall a b. (a -> b) -> a -> b
$ TacticT
  Judgement
  (Synthesized (LHsExpr GhcPs))
  TacticError
  TacticState
  ExtractM
  Type
forall (m :: * -> *). MonadState TacticState m => m Type
newUnivar
  (Judgement
 -> RuleT
      Judgement
      (Synthesized (LHsExpr GhcPs))
      TacticError
      TacticState
      ExtractM
      (Synthesized (LHsExpr GhcPs)))
-> TacticsM ()
forall (m :: * -> *) jdg ext err s.
Monad m =>
(jdg -> RuleT jdg ext err s m ext) -> TacticT jdg ext err s m ()
rule ((Judgement
  -> RuleT
       Judgement
       (Synthesized (LHsExpr GhcPs))
       TacticError
       TacticState
       ExtractM
       (Synthesized (LHsExpr GhcPs)))
 -> TacticsM ())
-> (Judgement
    -> RuleT
         Judgement
         (Synthesized (LHsExpr GhcPs))
         TacticError
         TacticState
         ExtractM
         (Synthesized (LHsExpr GhcPs)))
-> TacticsM ()
forall a b. (a -> b) -> a -> b
$ [(OccName, Judgement)]
-> Judgement
-> RuleT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     (Synthesized (LHsExpr GhcPs))
nonrecLet [(OccName, Judgement)]
occ_tys


------------------------------------------------------------------------------
-- | Deeply nest an unsaturated function onto itself
nested :: OccName -> TacticsM ()
nested :: OccName -> TacticsM ()
nested = TacticsM () -> TacticsM ()
deepening (TacticsM () -> TacticsM ())
-> (OccName -> TacticsM ()) -> OccName -> TacticsM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Saturation -> OccName -> TacticsM ()
use (Int -> Saturation
Unsaturated Int
1)


------------------------------------------------------------------------------
-- | Repeatedly bind a tactic on its first hole
deep :: Int -> TacticsM () -> TacticsM ()
deep :: Int -> TacticsM () -> TacticsM ()
deep Int
0 TacticsM ()
_ = () -> TacticsM ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
deep Int
n TacticsM ()
t = (TacticsM () -> TacticsM () -> TacticsM ())
-> [TacticsM ()] -> TacticsM ()
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 TacticsM () -> TacticsM () -> TacticsM ()
forall a. TacticsM a -> TacticsM a -> TacticsM a
bindOne ([TacticsM ()] -> TacticsM ()) -> [TacticsM ()] -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ Int -> TacticsM () -> [TacticsM ()]
forall a. Int -> a -> [a]
replicate Int
n TacticsM ()
t


------------------------------------------------------------------------------
-- | Try 'deep' for arbitrary depths.
deepening :: TacticsM () -> TacticsM ()
deepening :: TacticsM () -> TacticsM ()
deepening TacticsM ()
t =
  [TacticsM ()] -> TacticsM ()
forall (t :: * -> *) (f :: * -> *) a.
(Foldable t, Alternative f) =>
t (f a) -> f a
asum ([TacticsM ()] -> TacticsM ()) -> [TacticsM ()] -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ (Int -> TacticsM ()) -> [Int] -> [TacticsM ()]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Int -> TacticsM () -> TacticsM ())
-> TacticsM () -> Int -> TacticsM ()
forall a b c. (a -> b -> c) -> b -> a -> c
flip Int -> TacticsM () -> TacticsM ()
deep TacticsM ()
t) [Int
0 .. Int
100]


bindOne :: TacticsM a -> TacticsM a -> TacticsM a
bindOne :: TacticsM a -> TacticsM a -> TacticsM a
bindOne TacticsM a
t TacticsM a
t1 = TacticsM a
t TacticsM a -> [TacticsM a] -> TacticsM a
forall (m :: * -> *) jdg ext err s a.
Functor m =>
TacticT jdg ext err s m a
-> [TacticT jdg ext err s m a] -> TacticT jdg ext err s m a
<@> [TacticsM a
t1]


collapse :: TacticsM ()
collapse :: TacticsM ()
collapse = do
  Judgement
g <- TacticT
  Judgement
  (Synthesized (LHsExpr GhcPs))
  TacticError
  TacticState
  ExtractM
  Judgement
forall (m :: * -> *) jdg ext err s.
Functor m =>
TacticT jdg ext err s m jdg
goal
  let terms :: [HyInfo CType]
terms = Hypothesis CType -> [HyInfo CType]
forall a. Hypothesis a -> [HyInfo a]
unHypothesis (Hypothesis CType -> [HyInfo CType])
-> Hypothesis CType -> [HyInfo CType]
forall a b. (a -> b) -> a -> b
$ (HyInfo CType -> Bool) -> Hypothesis CType -> Hypothesis CType
forall a. (HyInfo a -> Bool) -> Hypothesis a -> Hypothesis a
hyFilter ((Judgement -> CType
forall a. Judgement' a -> a
jGoal Judgement
g CType -> CType -> Bool
forall a. Eq a => a -> a -> Bool
==) (CType -> Bool) -> (HyInfo CType -> CType) -> HyInfo CType -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HyInfo CType -> CType
forall a. HyInfo a -> a
hi_type) (Hypothesis CType -> Hypothesis CType)
-> Hypothesis CType -> Hypothesis CType
forall a b. (a -> b) -> a -> b
$ Judgement -> Hypothesis CType
forall a. Judgement' a -> Hypothesis a
jLocalHypothesis Judgement
g
  case [HyInfo CType]
terms of
    [HyInfo CType
hi] -> OccName -> TacticsM ()
assume (OccName -> TacticsM ()) -> OccName -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ HyInfo CType -> OccName
forall a. HyInfo a -> OccName
hi_name HyInfo CType
hi
    [HyInfo CType]
_    -> Int -> TacticsM ()
nary ([HyInfo CType] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [HyInfo CType]
terms) TacticsM () -> [TacticsM ()] -> TacticsM ()
forall (m :: * -> *) jdg ext err s a.
Functor m =>
TacticT jdg ext err s m a
-> [TacticT jdg ext err s m a] -> TacticT jdg ext err s m a
<@> (HyInfo CType -> TacticsM ()) -> [HyInfo CType] -> [TacticsM ()]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (OccName -> TacticsM ()
assume (OccName -> TacticsM ())
-> (HyInfo CType -> OccName) -> HyInfo CType -> TacticsM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HyInfo CType -> OccName
forall a. HyInfo a -> OccName
hi_name) [HyInfo CType]
terms


with_arg :: TacticsM ()
with_arg :: TacticsM ()
with_arg = (Judgement
 -> RuleT
      Judgement
      (Synthesized (LHsExpr GhcPs))
      TacticError
      TacticState
      ExtractM
      (Synthesized (LHsExpr GhcPs)))
-> TacticsM ()
forall (m :: * -> *) jdg ext err s.
Monad m =>
(jdg -> RuleT jdg ext err s m ext) -> TacticT jdg ext err s m ()
rule ((Judgement
  -> RuleT
       Judgement
       (Synthesized (LHsExpr GhcPs))
       TacticError
       TacticState
       ExtractM
       (Synthesized (LHsExpr GhcPs)))
 -> TacticsM ())
-> (Judgement
    -> RuleT
         Judgement
         (Synthesized (LHsExpr GhcPs))
         TacticError
         TacticState
         ExtractM
         (Synthesized (LHsExpr GhcPs)))
-> TacticsM ()
forall a b. (a -> b) -> a -> b
$ \Judgement
jdg -> do
  let g :: CType
g = Judgement -> CType
forall a. Judgement' a -> a
jGoal Judgement
jdg
  Type
fresh_ty <- RuleT
  Judgement
  (Synthesized (LHsExpr GhcPs))
  TacticError
  TacticState
  ExtractM
  Type
forall (m :: * -> *). MonadState TacticState m => m Type
newUnivar
  Synthesized (LHsExpr GhcPs)
a <- Judgement
-> RuleT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     (Synthesized (LHsExpr GhcPs))
newSubgoal (Judgement
 -> RuleT
      Judgement
      (Synthesized (LHsExpr GhcPs))
      TacticError
      TacticState
      ExtractM
      (Synthesized (LHsExpr GhcPs)))
-> Judgement
-> RuleT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     (Synthesized (LHsExpr GhcPs))
forall a b. (a -> b) -> a -> b
$ CType -> Judgement -> Judgement
forall a. a -> Judgement' a -> Judgement' a
withNewGoal (Type -> CType
CType Type
fresh_ty) Judgement
jdg
  Synthesized (LHsExpr GhcPs)
f <- Judgement
-> RuleT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     (Synthesized (LHsExpr GhcPs))
newSubgoal (Judgement
 -> RuleT
      Judgement
      (Synthesized (LHsExpr GhcPs))
      TacticError
      TacticState
      ExtractM
      (Synthesized (LHsExpr GhcPs)))
-> Judgement
-> RuleT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     (Synthesized (LHsExpr GhcPs))
forall a b. (a -> b) -> a -> b
$ CType -> Judgement -> Judgement
forall a. a -> Judgement' a -> Judgement' a
withNewGoal ((ThetaType -> Type -> Type) -> ThetaType -> CType -> CType
coerce ThetaType -> Type -> Type
mkFunTys' [Type
fresh_ty] CType
g) Judgement
jdg
  Synthesized (LHsExpr GhcPs)
-> RuleT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     (Synthesized (LHsExpr GhcPs))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Synthesized (LHsExpr GhcPs)
 -> RuleT
      Judgement
      (Synthesized (LHsExpr GhcPs))
      TacticError
      TacticState
      ExtractM
      (Synthesized (LHsExpr GhcPs)))
-> Synthesized (LHsExpr GhcPs)
-> RuleT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     (Synthesized (LHsExpr GhcPs))
forall a b. (a -> b) -> a -> b
$ (HsExpr GhcPs -> LHsExpr GhcPs)
-> Synthesized (HsExpr GhcPs) -> Synthesized (LHsExpr GhcPs)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap HsExpr GhcPs -> LHsExpr GhcPs
forall a. HasSrcSpan a => SrcSpanLess a -> a
noLoc (Synthesized (HsExpr GhcPs) -> Synthesized (LHsExpr GhcPs))
-> Synthesized (HsExpr GhcPs) -> Synthesized (LHsExpr GhcPs)
forall a b. (a -> b) -> a -> b
$ HsExpr GhcPs -> HsExpr GhcPs -> HsExpr GhcPs
forall e. App e => e -> e -> e
(@@) (HsExpr GhcPs -> HsExpr GhcPs -> HsExpr GhcPs)
-> Synthesized (HsExpr GhcPs)
-> Synthesized (HsExpr GhcPs -> HsExpr GhcPs)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (LHsExpr GhcPs -> HsExpr GhcPs)
-> Synthesized (LHsExpr GhcPs) -> Synthesized (HsExpr GhcPs)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap LHsExpr GhcPs -> HsExpr GhcPs
forall a. HasSrcSpan a => a -> SrcSpanLess a
unLoc Synthesized (LHsExpr GhcPs)
f Synthesized (HsExpr GhcPs -> HsExpr GhcPs)
-> Synthesized (HsExpr GhcPs) -> Synthesized (HsExpr GhcPs)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (LHsExpr GhcPs -> HsExpr GhcPs)
-> Synthesized (LHsExpr GhcPs) -> Synthesized (HsExpr GhcPs)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap LHsExpr GhcPs -> HsExpr GhcPs
forall a. HasSrcSpan a => a -> SrcSpanLess a
unLoc Synthesized (LHsExpr GhcPs)
a


------------------------------------------------------------------------------
-- | Determine the difference in hypothesis due to running a tactic. Also, it
-- runs the tactic.
hyDiff :: TacticsM () -> TacticsM (Hypothesis CType)
hyDiff :: TacticsM ()
-> TacticT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     (Hypothesis CType)
hyDiff TacticsM ()
m = do
  [HyInfo CType]
g <- Hypothesis CType -> [HyInfo CType]
forall a. Hypothesis a -> [HyInfo a]
unHypothesis (Hypothesis CType -> [HyInfo CType])
-> (Judgement -> Hypothesis CType) -> Judgement -> [HyInfo CType]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Judgement -> Hypothesis CType
forall a. Judgement' a -> Hypothesis a
jEntireHypothesis (Judgement -> [HyInfo CType])
-> TacticT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     Judgement
-> TacticT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     [HyInfo CType]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TacticT
  Judgement
  (Synthesized (LHsExpr GhcPs))
  TacticError
  TacticState
  ExtractM
  Judgement
forall (m :: * -> *) jdg ext err s.
Functor m =>
TacticT jdg ext err s m jdg
goal
  let g_len :: Int
g_len = [HyInfo CType] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [HyInfo CType]
g
  TacticsM ()
m
  [HyInfo CType]
g' <- Hypothesis CType -> [HyInfo CType]
forall a. Hypothesis a -> [HyInfo a]
unHypothesis (Hypothesis CType -> [HyInfo CType])
-> (Judgement -> Hypothesis CType) -> Judgement -> [HyInfo CType]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Judgement -> Hypothesis CType
forall a. Judgement' a -> Hypothesis a
jEntireHypothesis (Judgement -> [HyInfo CType])
-> TacticT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     Judgement
-> TacticT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     [HyInfo CType]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TacticT
  Judgement
  (Synthesized (LHsExpr GhcPs))
  TacticError
  TacticState
  ExtractM
  Judgement
forall (m :: * -> *) jdg ext err s.
Functor m =>
TacticT jdg ext err s m jdg
goal
  Hypothesis CType
-> TacticT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     (Hypothesis CType)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Hypothesis CType
 -> TacticT
      Judgement
      (Synthesized (LHsExpr GhcPs))
      TacticError
      TacticState
      ExtractM
      (Hypothesis CType))
-> Hypothesis CType
-> TacticT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     (Hypothesis CType)
forall a b. (a -> b) -> a -> b
$ [HyInfo CType] -> Hypothesis CType
forall a. [HyInfo a] -> Hypothesis a
Hypothesis ([HyInfo CType] -> Hypothesis CType)
-> [HyInfo CType] -> Hypothesis CType
forall a b. (a -> b) -> a -> b
$ Int -> [HyInfo CType] -> [HyInfo CType]
forall a. Int -> [a] -> [a]
take ([HyInfo CType] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [HyInfo CType]
g' Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
g_len) [HyInfo CType]
g'