{-# LANGUAGE TupleSections #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeSynonymInstances #-}
{-# LANGUAGE ViewPatterns #-}
module Ide.Plugin.Tactic.Tactics
( module Ide.Plugin.Tactic.Tactics
, runTactic
) where
import Control.Monad (when)
import Control.Monad.Except (throwError)
import Control.Monad.Reader.Class (MonadReader(ask))
import Control.Monad.State.Class
import Control.Monad.State.Strict (StateT(..), runStateT)
import Data.Bool (bool)
import Data.Foldable
import Data.List
import qualified Data.Map as M
import Data.Maybe
import qualified Data.Set as S
import DataCon
import Development.IDE.GHC.Compat
import GHC.Exts
import GHC.SourceGen.Expr
import GHC.SourceGen.Overloaded
import Ide.Plugin.Tactic.CodeGen
import Ide.Plugin.Tactic.Context
import Ide.Plugin.Tactic.GHC
import Ide.Plugin.Tactic.Judgements
import Ide.Plugin.Tactic.Machinery
import Ide.Plugin.Tactic.Naming
import Ide.Plugin.Tactic.Types
import Name (occNameString)
import Refinery.Tactic
import Refinery.Tactic.Internal
import TcType
import Type hiding (Var)
assumption :: TacticsM ()
assumption :: TacticsM ()
assumption = (Judgement -> [OccName]) -> (OccName -> TacticsM ()) -> TacticsM ()
forall a. (Judgement -> [a]) -> (a -> TacticsM ()) -> TacticsM ()
attemptOn Judgement -> [OccName]
allNames OccName -> TacticsM ()
assume
assume :: OccName -> TacticsM ()
assume :: OccName -> TacticsM ()
assume OccName
name = (Judgement
-> RuleT
Judgement
(Trace, LHsExpr GhcPs)
TacticError
TacticState
ExtractM
(Trace, LHsExpr GhcPs))
-> TacticsM ()
forall (m :: * -> *) jdg ext err s.
Monad m =>
(jdg -> RuleT jdg ext err s m ext) -> TacticT jdg ext err s m ()
rule ((Judgement
-> RuleT
Judgement
(Trace, LHsExpr GhcPs)
TacticError
TacticState
ExtractM
(Trace, LHsExpr GhcPs))
-> TacticsM ())
-> (Judgement
-> RuleT
Judgement
(Trace, LHsExpr GhcPs)
TacticError
TacticState
ExtractM
(Trace, LHsExpr GhcPs))
-> TacticsM ()
forall a b. (a -> b) -> a -> b
$ \Judgement
jdg -> do
let g :: CType
g = Judgement -> CType
forall a. Judgement' a -> a
jGoal Judgement
jdg
case OccName -> Map OccName (HyInfo CType) -> Maybe (HyInfo CType)
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup OccName
name (Map OccName (HyInfo CType) -> Maybe (HyInfo CType))
-> Map OccName (HyInfo CType) -> Maybe (HyInfo CType)
forall a b. (a -> b) -> a -> b
$ Judgement -> Map OccName (HyInfo CType)
forall a. Judgement' a -> Map OccName (HyInfo a)
jHypothesis Judgement
jdg of
Just (HyInfo CType -> CType
forall a. HyInfo a -> a
hi_type -> CType
ty) -> do
CType -> CType -> RuleM ()
unify CType
ty (CType -> RuleM ()) -> CType -> RuleM ()
forall a b. (a -> b) -> a -> b
$ Judgement -> CType
forall a. Judgement' a -> a
jGoal Judgement
jdg
Maybe PatVal -> (PatVal -> RuleM ()) -> RuleM ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
t a -> (a -> f b) -> f ()
for_ (OccName -> Map OccName PatVal -> Maybe PatVal
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup OccName
name (Map OccName PatVal -> Maybe PatVal)
-> Map OccName PatVal -> Maybe PatVal
forall a b. (a -> b) -> a -> b
$ Judgement -> Map OccName PatVal
forall a. Judgement' a -> Map OccName PatVal
jPatHypothesis Judgement
jdg) PatVal -> RuleM ()
forall (m :: * -> *). MonadState TacticState m => PatVal -> m ()
markStructuralySmallerRecursion
Judgement -> OccName -> RuleM ()
forall (m :: * -> *).
MonadState TacticState m =>
Judgement -> OccName -> m ()
useOccName Judgement
jdg OccName
name
(Trace, LHsExpr GhcPs)
-> RuleT
Judgement
(Trace, LHsExpr GhcPs)
TacticError
TacticState
ExtractM
(Trace, LHsExpr GhcPs)
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((Trace, LHsExpr GhcPs)
-> RuleT
Judgement
(Trace, LHsExpr GhcPs)
TacticError
TacticState
ExtractM
(Trace, LHsExpr GhcPs))
-> (Trace, LHsExpr GhcPs)
-> RuleT
Judgement
(Trace, LHsExpr GhcPs)
TacticError
TacticState
ExtractM
(Trace, LHsExpr GhcPs)
forall a b. (a -> b) -> a -> b
$ (String -> Trace
tracePrim (String -> Trace) -> String -> Trace
forall a b. (a -> b) -> a -> b
$ String
"assume " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> OccName -> String
occNameString OccName
name, ) (LHsExpr GhcPs -> (Trace, LHsExpr GhcPs))
-> LHsExpr GhcPs -> (Trace, LHsExpr GhcPs)
forall a b. (a -> b) -> a -> b
$ SrcSpanLess (LHsExpr GhcPs) -> LHsExpr GhcPs
forall a. HasSrcSpan a => SrcSpanLess a -> a
noLoc (SrcSpanLess (LHsExpr GhcPs) -> LHsExpr GhcPs)
-> SrcSpanLess (LHsExpr GhcPs) -> LHsExpr GhcPs
forall a b. (a -> b) -> a -> b
$ OccName -> HsExpr GhcPs
forall a. Var a => OccName -> a
var' OccName
name
Maybe (HyInfo CType)
Nothing -> TacticError
-> RuleT
Judgement
(Trace, LHsExpr GhcPs)
TacticError
TacticState
ExtractM
(Trace, LHsExpr GhcPs)
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TacticError
-> RuleT
Judgement
(Trace, LHsExpr GhcPs)
TacticError
TacticState
ExtractM
(Trace, LHsExpr GhcPs))
-> TacticError
-> RuleT
Judgement
(Trace, LHsExpr GhcPs)
TacticError
TacticState
ExtractM
(Trace, LHsExpr GhcPs)
forall a b. (a -> b) -> a -> b
$ OccName -> TacticError
UndefinedHypothesis OccName
name
recursion :: TacticsM ()
recursion :: TacticsM ()
recursion = TacticsM () -> TacticsM ()
forall a. TacticsM a -> TacticsM a
requireConcreteHole (TacticsM () -> TacticsM ()) -> TacticsM () -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ String -> TacticsM () -> TacticsM ()
forall (m :: * -> *) jdg ext err s a.
Functor m =>
String
-> TacticT jdg (Trace, ext) err s m a
-> TacticT jdg (Trace, ext) err s m a
tracing String
"recursion" (TacticsM () -> TacticsM ()) -> TacticsM () -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ do
[(OccName, CType)]
defs <- TacticT
Judgement
(Trace, LHsExpr GhcPs)
TacticError
TacticState
ExtractM
[(OccName, CType)]
forall (m :: * -> *). MonadReader Context m => m [(OccName, CType)]
getCurrentDefinitions
(Judgement -> [OccName]) -> (OccName -> TacticsM ()) -> TacticsM ()
forall a. (Judgement -> [a]) -> (a -> TacticsM ()) -> TacticsM ()
attemptOn ([OccName] -> Judgement -> [OccName]
forall a b. a -> b -> a
const ([OccName] -> Judgement -> [OccName])
-> [OccName] -> Judgement -> [OccName]
forall a b. (a -> b) -> a -> b
$ ((OccName, CType) -> OccName) -> [(OccName, CType)] -> [OccName]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (OccName, CType) -> OccName
forall a b. (a, b) -> a
fst [(OccName, CType)]
defs) ((OccName -> TacticsM ()) -> TacticsM ())
-> (OccName -> TacticsM ()) -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ \OccName
name -> do
(TacticState -> TacticState) -> TacticsM ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((TacticState -> TacticState) -> TacticsM ())
-> (TacticState -> TacticState) -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ TacticState -> TacticState
pushRecursionStack (TacticState -> TacticState)
-> (TacticState -> TacticState) -> TacticState -> TacticState
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TacticState -> TacticState
countRecursiveCall
(TacticState -> Maybe TacticError)
-> (TacticState -> TacticState) -> TacticsM () -> TacticsM ()
forall (m :: * -> *) s err jdg ext.
Monad m =>
(s -> Maybe err)
-> (s -> s)
-> TacticT jdg ext err s m ()
-> TacticT jdg ext err s m ()
ensure TacticState -> Maybe TacticError
guardStructurallySmallerRecursion TacticState -> TacticState
popRecursionStack (TacticsM () -> TacticsM ()) -> TacticsM () -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ do
(TacticsM () -> (Judgement -> Judgement) -> TacticsM ()
forall a. TacticsM a -> (Judgement -> Judgement) -> TacticsM a
localTactic (OccName -> TacticsM ()
apply OccName
name) ((Judgement -> Judgement) -> TacticsM ())
-> (Judgement -> Judgement) -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ [(OccName, CType)] -> Judgement -> Judgement
forall a. [(OccName, a)] -> Judgement' a -> Judgement' a
introducingRecursively [(OccName, CType)]
defs)
TacticsM () -> [TacticsM ()] -> TacticsM ()
forall (m :: * -> *) jdg ext err s a.
Functor m =>
TacticT jdg ext err s m a
-> [TacticT jdg ext err s m a] -> TacticT jdg ext err s m a
<@> (Int -> TacticsM ()) -> [Int] -> [TacticsM ()]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (TacticsM () -> (Judgement -> Judgement) -> TacticsM ()
forall a. TacticsM a -> (Judgement -> Judgement) -> TacticsM a
localTactic TacticsM ()
assumption ((Judgement -> Judgement) -> TacticsM ())
-> (Int -> Judgement -> Judgement) -> Int -> TacticsM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OccName -> Int -> Judgement -> Judgement
filterPosition OccName
name) [Int
0..]
intros :: TacticsM ()
intros :: TacticsM ()
intros = (Judgement
-> RuleT
Judgement
(Trace, LHsExpr GhcPs)
TacticError
TacticState
ExtractM
(Trace, LHsExpr GhcPs))
-> TacticsM ()
forall (m :: * -> *) jdg ext err s.
Monad m =>
(jdg -> RuleT jdg ext err s m ext) -> TacticT jdg ext err s m ()
rule ((Judgement
-> RuleT
Judgement
(Trace, LHsExpr GhcPs)
TacticError
TacticState
ExtractM
(Trace, LHsExpr GhcPs))
-> TacticsM ())
-> (Judgement
-> RuleT
Judgement
(Trace, LHsExpr GhcPs)
TacticError
TacticState
ExtractM
(Trace, LHsExpr GhcPs))
-> TacticsM ()
forall a b. (a -> b) -> a -> b
$ \Judgement
jdg -> do
let hy :: Map OccName (HyInfo CType)
hy = Judgement -> Map OccName (HyInfo CType)
forall a. Judgement' a -> Map OccName (HyInfo a)
jHypothesis Judgement
jdg
g :: CType
g = Judgement -> CType
forall a. Judgement' a -> a
jGoal Judgement
jdg
Context
ctx <- RuleT
Judgement
(Trace, LHsExpr GhcPs)
TacticError
TacticState
ExtractM
Context
forall r (m :: * -> *). MonadReader r m => m r
ask
case Type -> ([Type], Type)
tcSplitFunTys (Type -> ([Type], Type)) -> Type -> ([Type], Type)
forall a b. (a -> b) -> a -> b
$ CType -> Type
unCType CType
g of
([], Type
_) -> TacticError
-> RuleT
Judgement
(Trace, LHsExpr GhcPs)
TacticError
TacticState
ExtractM
(Trace, LHsExpr GhcPs)
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TacticError
-> RuleT
Judgement
(Trace, LHsExpr GhcPs)
TacticError
TacticState
ExtractM
(Trace, LHsExpr GhcPs))
-> TacticError
-> RuleT
Judgement
(Trace, LHsExpr GhcPs)
TacticError
TacticState
ExtractM
(Trace, LHsExpr GhcPs)
forall a b. (a -> b) -> a -> b
$ String -> CType -> TacticError
GoalMismatch String
"intros" CType
g
([Type]
as, Type
b) -> do
[OccName]
vs <- Map OccName (HyInfo CType)
-> [Type]
-> RuleT
Judgement
(Trace, LHsExpr GhcPs)
TacticError
TacticState
ExtractM
[OccName]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
Map OccName a -> t Type -> m (t OccName)
mkManyGoodNames (Judgement -> Map OccName (HyInfo CType)
forall a. Judgement' a -> Map OccName (HyInfo a)
jEntireHypothesis Judgement
jdg) [Type]
as
let top_hole :: Maybe OccName
top_hole = Context -> Judgement -> Maybe OccName
forall a. Context -> Judgement' a -> Maybe OccName
isTopHole Context
ctx Judgement
jdg
jdg' :: Judgement
jdg' = Maybe OccName -> [(OccName, CType)] -> Judgement -> Judgement
forall a.
Maybe OccName -> [(OccName, a)] -> Judgement' a -> Judgement' a
introducingLambda Maybe OccName
top_hole ([OccName] -> [CType] -> [(OccName, CType)]
forall a b. [a] -> [b] -> [(a, b)]
zip [OccName]
vs ([CType] -> [(OccName, CType)]) -> [CType] -> [(OccName, CType)]
forall a b. (a -> b) -> a -> b
$ [Type] -> [CType]
coerce [Type]
as)
(Judgement -> Judgement) -> Judgement -> Judgement
forall a b. (a -> b) -> a -> b
$ CType -> Judgement -> Judgement
forall a. a -> Judgement' a -> Judgement' a
withNewGoal (Type -> CType
CType Type
b) Judgement
jdg
(TacticState -> TacticState) -> RuleM ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((TacticState -> TacticState) -> RuleM ())
-> (TacticState -> TacticState) -> RuleM ()
forall a b. (a -> b) -> a -> b
$ (Set OccName -> Set OccName) -> TacticState -> TacticState
withIntroducedVals ((Set OccName -> Set OccName) -> TacticState -> TacticState)
-> (Set OccName -> Set OccName) -> TacticState -> TacticState
forall a b. (a -> b) -> a -> b
$ Set OccName -> Set OccName -> Set OccName
forall a. Monoid a => a -> a -> a
mappend (Set OccName -> Set OccName -> Set OccName)
-> Set OccName -> Set OccName -> Set OccName
forall a b. (a -> b) -> a -> b
$ [OccName] -> Set OccName
forall a. Ord a => [a] -> Set a
S.fromList [OccName]
vs
Bool -> RuleM () -> RuleM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Maybe OccName -> Bool
forall a. Maybe a -> Bool
isJust Maybe OccName
top_hole) (RuleM () -> RuleM ()) -> RuleM () -> RuleM ()
forall a b. (a -> b) -> a -> b
$ Set OccName -> RuleM ()
forall (m :: * -> *).
MonadState TacticState m =>
Set OccName -> m ()
addUnusedTopVals (Set OccName -> RuleM ()) -> Set OccName -> RuleM ()
forall a b. (a -> b) -> a -> b
$ [OccName] -> Set OccName
forall a. Ord a => [a] -> Set a
S.fromList [OccName]
vs
(Trace
tr, LHsExpr GhcPs
sg) <- Judgement
-> RuleT
Judgement
(Trace, LHsExpr GhcPs)
TacticError
TacticState
ExtractM
(Trace, LHsExpr GhcPs)
newSubgoal Judgement
jdg'
(Trace, LHsExpr GhcPs)
-> RuleT
Judgement
(Trace, LHsExpr GhcPs)
TacticError
TacticState
ExtractM
(Trace, LHsExpr GhcPs)
forall (f :: * -> *) a. Applicative f => a -> f a
pure
((Trace, LHsExpr GhcPs)
-> RuleT
Judgement
(Trace, LHsExpr GhcPs)
TacticError
TacticState
ExtractM
(Trace, LHsExpr GhcPs))
-> (HsExpr GhcPs -> (Trace, LHsExpr GhcPs))
-> HsExpr GhcPs
-> RuleT
Judgement
(Trace, LHsExpr GhcPs)
TacticError
TacticState
ExtractM
(Trace, LHsExpr GhcPs)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String -> [Trace] -> Trace
forall a. (Eq a, Monoid a) => a -> [Rose a] -> Rose a
rose (String
"intros {" String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
", " ((OccName -> String) -> [OccName] -> [String]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap OccName -> String
forall a. Show a => a -> String
show [OccName]
vs) String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
"}") ([Trace] -> Trace) -> [Trace] -> Trace
forall a b. (a -> b) -> a -> b
$ Trace -> [Trace]
forall (f :: * -> *) a. Applicative f => a -> f a
pure Trace
tr, )
(LHsExpr GhcPs -> (Trace, LHsExpr GhcPs))
-> (HsExpr GhcPs -> LHsExpr GhcPs)
-> HsExpr GhcPs
-> (Trace, LHsExpr GhcPs)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HsExpr GhcPs -> LHsExpr GhcPs
forall a. HasSrcSpan a => SrcSpanLess a -> a
noLoc
(HsExpr GhcPs -> LHsExpr GhcPs)
-> (HsExpr GhcPs -> HsExpr GhcPs) -> HsExpr GhcPs -> LHsExpr GhcPs
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Pat'] -> HsExpr GhcPs -> HsExpr GhcPs
lambda ((OccName -> Pat') -> [OccName] -> [Pat']
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap OccName -> Pat'
forall a. BVar a => OccName -> a
bvar' [OccName]
vs)
(HsExpr GhcPs
-> RuleT
Judgement
(Trace, LHsExpr GhcPs)
TacticError
TacticState
ExtractM
(Trace, LHsExpr GhcPs))
-> HsExpr GhcPs
-> RuleT
Judgement
(Trace, LHsExpr GhcPs)
TacticError
TacticState
ExtractM
(Trace, LHsExpr GhcPs)
forall a b. (a -> b) -> a -> b
$ LHsExpr GhcPs -> SrcSpanLess (LHsExpr GhcPs)
forall a. HasSrcSpan a => a -> SrcSpanLess a
unLoc LHsExpr GhcPs
sg
destructAuto :: OccName -> TacticsM ()
destructAuto :: OccName -> TacticsM ()
destructAuto OccName
name = TacticsM () -> TacticsM ()
forall a. TacticsM a -> TacticsM a
requireConcreteHole (TacticsM () -> TacticsM ()) -> TacticsM () -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ String -> TacticsM () -> TacticsM ()
forall (m :: * -> *) jdg ext err s a.
Functor m =>
String
-> TacticT jdg (Trace, ext) err s m a
-> TacticT jdg (Trace, ext) err s m a
tracing String
"destruct(auto)" (TacticsM () -> TacticsM ()) -> TacticsM () -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ do
Judgement
jdg <- TacticT
Judgement
(Trace, LHsExpr GhcPs)
TacticError
TacticState
ExtractM
Judgement
forall (m :: * -> *) jdg ext err s.
Functor m =>
TacticT jdg ext err s m jdg
goal
case OccName -> Map OccName (HyInfo CType) -> Maybe (HyInfo CType)
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup OccName
name (Map OccName (HyInfo CType) -> Maybe (HyInfo CType))
-> Map OccName (HyInfo CType) -> Maybe (HyInfo CType)
forall a b. (a -> b) -> a -> b
$ Judgement -> Map OccName (HyInfo CType)
forall a. Judgement' a -> Map OccName (HyInfo a)
jHypothesis Judgement
jdg of
Maybe (HyInfo CType)
Nothing -> TacticError -> TacticsM ()
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TacticError -> TacticsM ()) -> TacticError -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ OccName -> TacticError
NotInScope OccName
name
Just HyInfo CType
hi ->
let subtactic :: TacticsM ()
subtactic = (Judgement
-> RuleT
Judgement
(Trace, LHsExpr GhcPs)
TacticError
TacticState
ExtractM
(Trace, LHsExpr GhcPs))
-> TacticsM ()
forall (m :: * -> *) jdg ext err s.
Monad m =>
(jdg -> RuleT jdg ext err s m ext) -> TacticT jdg ext err s m ()
rule ((Judgement
-> RuleT
Judgement
(Trace, LHsExpr GhcPs)
TacticError
TacticState
ExtractM
(Trace, LHsExpr GhcPs))
-> TacticsM ())
-> (Judgement
-> RuleT
Judgement
(Trace, LHsExpr GhcPs)
TacticError
TacticState
ExtractM
(Trace, LHsExpr GhcPs))
-> TacticsM ()
forall a b. (a -> b) -> a -> b
$ (DataCon
-> Judgement
-> RuleT
Judgement
(Trace, LHsExpr GhcPs)
TacticError
TacticState
ExtractM
(Trace, LHsExpr GhcPs))
-> OccName
-> Judgement
-> RuleT
Judgement
(Trace, LHsExpr GhcPs)
TacticError
TacticState
ExtractM
(Trace, LHsExpr GhcPs)
destruct' ((Judgement
-> RuleT
Judgement
(Trace, LHsExpr GhcPs)
TacticError
TacticState
ExtractM
(Trace, LHsExpr GhcPs))
-> DataCon
-> Judgement
-> RuleT
Judgement
(Trace, LHsExpr GhcPs)
TacticError
TacticState
ExtractM
(Trace, LHsExpr GhcPs)
forall a b. a -> b -> a
const Judgement
-> RuleT
Judgement
(Trace, LHsExpr GhcPs)
TacticError
TacticState
ExtractM
(Trace, LHsExpr GhcPs)
forall jdg ext (m :: * -> *). MonadRule jdg ext m => jdg -> m ext
subgoal) OccName
name
in case Provenance -> Bool
isPatternMatch (Provenance -> Bool) -> Provenance -> Bool
forall a b. (a -> b) -> a -> b
$ HyInfo CType -> Provenance
forall a. HyInfo a -> Provenance
hi_provenance HyInfo CType
hi of
Bool
True ->
TacticsM () -> ([Judgement] -> Maybe TacticError) -> TacticsM ()
forall ext (m :: * -> *) jdg err s.
MonadExtract ext m =>
TacticT jdg ext err s m ()
-> ([jdg] -> Maybe err) -> TacticT jdg ext err s m ()
pruning TacticsM ()
subtactic (([Judgement] -> Maybe TacticError) -> TacticsM ())
-> ([Judgement] -> Maybe TacticError) -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ \[Judgement]
jdgs ->
let getHyTypes :: Judgement -> Set CType
getHyTypes = [CType] -> Set CType
forall a. Ord a => [a] -> Set a
S.fromList ([CType] -> Set CType)
-> (Judgement -> [CType]) -> Judgement -> Set CType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (HyInfo CType -> CType) -> [HyInfo CType] -> [CType]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap HyInfo CType -> CType
forall a. HyInfo a -> a
hi_type ([HyInfo CType] -> [CType])
-> (Judgement -> [HyInfo CType]) -> Judgement -> [CType]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map OccName (HyInfo CType) -> [HyInfo CType]
forall k a. Map k a -> [a]
M.elems (Map OccName (HyInfo CType) -> [HyInfo CType])
-> (Judgement -> Map OccName (HyInfo CType))
-> Judgement
-> [HyInfo CType]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Judgement -> Map OccName (HyInfo CType)
forall a. Judgement' a -> Map OccName (HyInfo a)
jHypothesis
new_hy :: Set CType
new_hy = (Judgement -> Set CType) -> [Judgement] -> Set CType
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Judgement -> Set CType
getHyTypes [Judgement]
jdgs
old_hy :: Set CType
old_hy = Judgement -> Set CType
getHyTypes Judgement
jdg
in case Set CType -> Bool
forall a. Set a -> Bool
S.null (Set CType -> Bool) -> Set CType -> Bool
forall a b. (a -> b) -> a -> b
$ Set CType
new_hy Set CType -> Set CType -> Set CType
forall a. Ord a => Set a -> Set a -> Set a
S.\\ Set CType
old_hy of
Bool
True -> TacticError -> Maybe TacticError
forall a. a -> Maybe a
Just (TacticError -> Maybe TacticError)
-> TacticError -> Maybe TacticError
forall a b. (a -> b) -> a -> b
$ OccName -> TacticError
UnhelpfulDestruct OccName
name
Bool
False -> Maybe TacticError
forall a. Maybe a
Nothing
Bool
False -> TacticsM ()
subtactic
destruct :: OccName -> TacticsM ()
destruct :: OccName -> TacticsM ()
destruct OccName
name = TacticsM () -> TacticsM ()
forall a. TacticsM a -> TacticsM a
requireConcreteHole (TacticsM () -> TacticsM ()) -> TacticsM () -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ String -> TacticsM () -> TacticsM ()
forall (m :: * -> *) jdg ext err s a.
Functor m =>
String
-> TacticT jdg (Trace, ext) err s m a
-> TacticT jdg (Trace, ext) err s m a
tracing String
"destruct(user)" (TacticsM () -> TacticsM ()) -> TacticsM () -> TacticsM ()
forall a b. (a -> b) -> a -> b
$
(Judgement
-> RuleT
Judgement
(Trace, LHsExpr GhcPs)
TacticError
TacticState
ExtractM
(Trace, LHsExpr GhcPs))
-> TacticsM ()
forall (m :: * -> *) jdg ext err s.
Monad m =>
(jdg -> RuleT jdg ext err s m ext) -> TacticT jdg ext err s m ()
rule ((Judgement
-> RuleT
Judgement
(Trace, LHsExpr GhcPs)
TacticError
TacticState
ExtractM
(Trace, LHsExpr GhcPs))
-> TacticsM ())
-> (Judgement
-> RuleT
Judgement
(Trace, LHsExpr GhcPs)
TacticError
TacticState
ExtractM
(Trace, LHsExpr GhcPs))
-> TacticsM ()
forall a b. (a -> b) -> a -> b
$ (DataCon
-> Judgement
-> RuleT
Judgement
(Trace, LHsExpr GhcPs)
TacticError
TacticState
ExtractM
(Trace, LHsExpr GhcPs))
-> OccName
-> Judgement
-> RuleT
Judgement
(Trace, LHsExpr GhcPs)
TacticError
TacticState
ExtractM
(Trace, LHsExpr GhcPs)
destruct' ((Judgement
-> RuleT
Judgement
(Trace, LHsExpr GhcPs)
TacticError
TacticState
ExtractM
(Trace, LHsExpr GhcPs))
-> DataCon
-> Judgement
-> RuleT
Judgement
(Trace, LHsExpr GhcPs)
TacticError
TacticState
ExtractM
(Trace, LHsExpr GhcPs)
forall a b. a -> b -> a
const Judgement
-> RuleT
Judgement
(Trace, LHsExpr GhcPs)
TacticError
TacticState
ExtractM
(Trace, LHsExpr GhcPs)
forall jdg ext (m :: * -> *). MonadRule jdg ext m => jdg -> m ext
subgoal) OccName
name
homo :: OccName -> TacticsM ()
homo :: OccName -> TacticsM ()
homo = TacticsM () -> TacticsM ()
forall a. TacticsM a -> TacticsM a
requireConcreteHole (TacticsM () -> TacticsM ())
-> (OccName -> TacticsM ()) -> OccName -> TacticsM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> TacticsM () -> TacticsM ()
forall (m :: * -> *) jdg ext err s a.
Functor m =>
String
-> TacticT jdg (Trace, ext) err s m a
-> TacticT jdg (Trace, ext) err s m a
tracing String
"homo" (TacticsM () -> TacticsM ())
-> (OccName -> TacticsM ()) -> OccName -> TacticsM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Judgement
-> RuleT
Judgement
(Trace, LHsExpr GhcPs)
TacticError
TacticState
ExtractM
(Trace, LHsExpr GhcPs))
-> TacticsM ()
forall (m :: * -> *) jdg ext err s.
Monad m =>
(jdg -> RuleT jdg ext err s m ext) -> TacticT jdg ext err s m ()
rule ((Judgement
-> RuleT
Judgement
(Trace, LHsExpr GhcPs)
TacticError
TacticState
ExtractM
(Trace, LHsExpr GhcPs))
-> TacticsM ())
-> (OccName
-> Judgement
-> RuleT
Judgement
(Trace, LHsExpr GhcPs)
TacticError
TacticState
ExtractM
(Trace, LHsExpr GhcPs))
-> OccName
-> TacticsM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (DataCon
-> Judgement
-> RuleT
Judgement
(Trace, LHsExpr GhcPs)
TacticError
TacticState
ExtractM
(Trace, LHsExpr GhcPs))
-> OccName
-> Judgement
-> RuleT
Judgement
(Trace, LHsExpr GhcPs)
TacticError
TacticState
ExtractM
(Trace, LHsExpr GhcPs)
destruct' (\DataCon
dc Judgement
jdg ->
Judgement
-> DataCon
-> [Type]
-> RuleT
Judgement
(Trace, LHsExpr GhcPs)
TacticError
TacticState
ExtractM
(Trace, LHsExpr GhcPs)
buildDataCon Judgement
jdg DataCon
dc ([Type]
-> RuleT
Judgement
(Trace, LHsExpr GhcPs)
TacticError
TacticState
ExtractM
(Trace, LHsExpr GhcPs))
-> [Type]
-> RuleT
Judgement
(Trace, LHsExpr GhcPs)
TacticError
TacticState
ExtractM
(Trace, LHsExpr GhcPs)
forall a b. (a -> b) -> a -> b
$ (Type, [Type]) -> [Type]
forall a b. (a, b) -> b
snd ((Type, [Type]) -> [Type]) -> (Type, [Type]) -> [Type]
forall a b. (a -> b) -> a -> b
$ Type -> (Type, [Type])
splitAppTys (Type -> (Type, [Type])) -> Type -> (Type, [Type])
forall a b. (a -> b) -> a -> b
$ CType -> Type
unCType (CType -> Type) -> CType -> Type
forall a b. (a -> b) -> a -> b
$ Judgement -> CType
forall a. Judgement' a -> a
jGoal Judgement
jdg)
destructLambdaCase :: TacticsM ()
destructLambdaCase :: TacticsM ()
destructLambdaCase = String -> TacticsM () -> TacticsM ()
forall (m :: * -> *) jdg ext err s a.
Functor m =>
String
-> TacticT jdg (Trace, ext) err s m a
-> TacticT jdg (Trace, ext) err s m a
tracing String
"destructLambdaCase" (TacticsM () -> TacticsM ()) -> TacticsM () -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ (Judgement
-> RuleT
Judgement
(Trace, LHsExpr GhcPs)
TacticError
TacticState
ExtractM
(Trace, LHsExpr GhcPs))
-> TacticsM ()
forall (m :: * -> *) jdg ext err s.
Monad m =>
(jdg -> RuleT jdg ext err s m ext) -> TacticT jdg ext err s m ()
rule ((Judgement
-> RuleT
Judgement
(Trace, LHsExpr GhcPs)
TacticError
TacticState
ExtractM
(Trace, LHsExpr GhcPs))
-> TacticsM ())
-> (Judgement
-> RuleT
Judgement
(Trace, LHsExpr GhcPs)
TacticError
TacticState
ExtractM
(Trace, LHsExpr GhcPs))
-> TacticsM ()
forall a b. (a -> b) -> a -> b
$ (DataCon
-> Judgement
-> RuleT
Judgement
(Trace, LHsExpr GhcPs)
TacticError
TacticState
ExtractM
(Trace, LHsExpr GhcPs))
-> Judgement
-> RuleT
Judgement
(Trace, LHsExpr GhcPs)
TacticError
TacticState
ExtractM
(Trace, LHsExpr GhcPs)
destructLambdaCase' ((Judgement
-> RuleT
Judgement
(Trace, LHsExpr GhcPs)
TacticError
TacticState
ExtractM
(Trace, LHsExpr GhcPs))
-> DataCon
-> Judgement
-> RuleT
Judgement
(Trace, LHsExpr GhcPs)
TacticError
TacticState
ExtractM
(Trace, LHsExpr GhcPs)
forall a b. a -> b -> a
const Judgement
-> RuleT
Judgement
(Trace, LHsExpr GhcPs)
TacticError
TacticState
ExtractM
(Trace, LHsExpr GhcPs)
forall jdg ext (m :: * -> *). MonadRule jdg ext m => jdg -> m ext
subgoal)
homoLambdaCase :: TacticsM ()
homoLambdaCase :: TacticsM ()
homoLambdaCase =
String -> TacticsM () -> TacticsM ()
forall (m :: * -> *) jdg ext err s a.
Functor m =>
String
-> TacticT jdg (Trace, ext) err s m a
-> TacticT jdg (Trace, ext) err s m a
tracing String
"homoLambdaCase" (TacticsM () -> TacticsM ()) -> TacticsM () -> TacticsM ()
forall a b. (a -> b) -> a -> b
$
(Judgement
-> RuleT
Judgement
(Trace, LHsExpr GhcPs)
TacticError
TacticState
ExtractM
(Trace, LHsExpr GhcPs))
-> TacticsM ()
forall (m :: * -> *) jdg ext err s.
Monad m =>
(jdg -> RuleT jdg ext err s m ext) -> TacticT jdg ext err s m ()
rule ((Judgement
-> RuleT
Judgement
(Trace, LHsExpr GhcPs)
TacticError
TacticState
ExtractM
(Trace, LHsExpr GhcPs))
-> TacticsM ())
-> (Judgement
-> RuleT
Judgement
(Trace, LHsExpr GhcPs)
TacticError
TacticState
ExtractM
(Trace, LHsExpr GhcPs))
-> TacticsM ()
forall a b. (a -> b) -> a -> b
$ (DataCon
-> Judgement
-> RuleT
Judgement
(Trace, LHsExpr GhcPs)
TacticError
TacticState
ExtractM
(Trace, LHsExpr GhcPs))
-> Judgement
-> RuleT
Judgement
(Trace, LHsExpr GhcPs)
TacticError
TacticState
ExtractM
(Trace, LHsExpr GhcPs)
destructLambdaCase' ((DataCon
-> Judgement
-> RuleT
Judgement
(Trace, LHsExpr GhcPs)
TacticError
TacticState
ExtractM
(Trace, LHsExpr GhcPs))
-> Judgement
-> RuleT
Judgement
(Trace, LHsExpr GhcPs)
TacticError
TacticState
ExtractM
(Trace, LHsExpr GhcPs))
-> (DataCon
-> Judgement
-> RuleT
Judgement
(Trace, LHsExpr GhcPs)
TacticError
TacticState
ExtractM
(Trace, LHsExpr GhcPs))
-> Judgement
-> RuleT
Judgement
(Trace, LHsExpr GhcPs)
TacticError
TacticState
ExtractM
(Trace, LHsExpr GhcPs)
forall a b. (a -> b) -> a -> b
$ \DataCon
dc Judgement
jdg ->
Judgement
-> DataCon
-> [Type]
-> RuleT
Judgement
(Trace, LHsExpr GhcPs)
TacticError
TacticState
ExtractM
(Trace, LHsExpr GhcPs)
buildDataCon Judgement
jdg DataCon
dc
([Type]
-> RuleT
Judgement
(Trace, LHsExpr GhcPs)
TacticError
TacticState
ExtractM
(Trace, LHsExpr GhcPs))
-> (CType -> [Type])
-> CType
-> RuleT
Judgement
(Trace, LHsExpr GhcPs)
TacticError
TacticState
ExtractM
(Trace, LHsExpr GhcPs)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Type, [Type]) -> [Type]
forall a b. (a, b) -> b
snd
((Type, [Type]) -> [Type])
-> (CType -> (Type, [Type])) -> CType -> [Type]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> (Type, [Type])
splitAppTys
(Type -> (Type, [Type]))
-> (CType -> Type) -> CType -> (Type, [Type])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CType -> Type
unCType
(CType
-> RuleT
Judgement
(Trace, LHsExpr GhcPs)
TacticError
TacticState
ExtractM
(Trace, LHsExpr GhcPs))
-> CType
-> RuleT
Judgement
(Trace, LHsExpr GhcPs)
TacticError
TacticState
ExtractM
(Trace, LHsExpr GhcPs)
forall a b. (a -> b) -> a -> b
$ Judgement -> CType
forall a. Judgement' a -> a
jGoal Judgement
jdg
apply :: OccName -> TacticsM ()
apply :: OccName -> TacticsM ()
apply OccName
func = TacticsM () -> TacticsM ()
forall a. TacticsM a -> TacticsM a
requireConcreteHole (TacticsM () -> TacticsM ()) -> TacticsM () -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ String -> TacticsM () -> TacticsM ()
forall (m :: * -> *) jdg ext err s a.
Functor m =>
String
-> TacticT jdg (Trace, ext) err s m a
-> TacticT jdg (Trace, ext) err s m a
tracing (String
"apply' " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> OccName -> String
forall a. Show a => a -> String
show OccName
func) (TacticsM () -> TacticsM ()) -> TacticsM () -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ do
Judgement
jdg <- TacticT
Judgement
(Trace, LHsExpr GhcPs)
TacticError
TacticState
ExtractM
Judgement
forall (m :: * -> *) jdg ext err s.
Functor m =>
TacticT jdg ext err s m jdg
goal
let hy :: Map OccName (HyInfo CType)
hy = Judgement -> Map OccName (HyInfo CType)
forall a. Judgement' a -> Map OccName (HyInfo a)
jHypothesis Judgement
jdg
g :: CType
g = Judgement -> CType
forall a. Judgement' a -> a
jGoal Judgement
jdg
case OccName -> Map OccName (HyInfo CType) -> Maybe (HyInfo CType)
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup OccName
func Map OccName (HyInfo CType)
hy of
Just (HyInfo CType -> CType
forall a. HyInfo a -> a
hi_type -> CType Type
ty) -> do
Type
ty' <- Type
-> TacticT
Judgement
(Trace, LHsExpr GhcPs)
TacticError
TacticState
ExtractM
Type
forall (m :: * -> *). MonadState TacticState m => Type -> m Type
freshTyvars Type
ty
let ([TyVar]
_, [Type]
_, [Type]
args, Type
ret) = Type -> ([TyVar], [Type], [Type], Type)
tacticsSplitFunTy Type
ty'
TacticsM () -> TacticsM ()
requireNewHoles (TacticsM () -> TacticsM ()) -> TacticsM () -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ (Judgement
-> RuleT
Judgement
(Trace, LHsExpr GhcPs)
TacticError
TacticState
ExtractM
(Trace, LHsExpr GhcPs))
-> TacticsM ()
forall (m :: * -> *) jdg ext err s.
Monad m =>
(jdg -> RuleT jdg ext err s m ext) -> TacticT jdg ext err s m ()
rule ((Judgement
-> RuleT
Judgement
(Trace, LHsExpr GhcPs)
TacticError
TacticState
ExtractM
(Trace, LHsExpr GhcPs))
-> TacticsM ())
-> (Judgement
-> RuleT
Judgement
(Trace, LHsExpr GhcPs)
TacticError
TacticState
ExtractM
(Trace, LHsExpr GhcPs))
-> TacticsM ()
forall a b. (a -> b) -> a -> b
$ \Judgement
jdg -> do
CType -> CType -> RuleM ()
unify CType
g (Type -> CType
CType Type
ret)
Judgement -> OccName -> RuleM ()
forall (m :: * -> *).
MonadState TacticState m =>
Judgement -> OccName -> m ()
useOccName Judgement
jdg OccName
func
(Trace
tr, [LHsExpr GhcPs]
sgs)
<- ([(Trace, LHsExpr GhcPs)] -> (Trace, [LHsExpr GhcPs]))
-> RuleT
Judgement
(Trace, LHsExpr GhcPs)
TacticError
TacticState
ExtractM
[(Trace, LHsExpr GhcPs)]
-> RuleT
Judgement
(Trace, LHsExpr GhcPs)
TacticError
TacticState
ExtractM
(Trace, [LHsExpr GhcPs])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [(Trace, LHsExpr GhcPs)] -> (Trace, [LHsExpr GhcPs])
forall a. [(Trace, a)] -> (Trace, [a])
unzipTrace
(RuleT
Judgement
(Trace, LHsExpr GhcPs)
TacticError
TacticState
ExtractM
[(Trace, LHsExpr GhcPs)]
-> RuleT
Judgement
(Trace, LHsExpr GhcPs)
TacticError
TacticState
ExtractM
(Trace, [LHsExpr GhcPs]))
-> RuleT
Judgement
(Trace, LHsExpr GhcPs)
TacticError
TacticState
ExtractM
[(Trace, LHsExpr GhcPs)]
-> RuleT
Judgement
(Trace, LHsExpr GhcPs)
TacticError
TacticState
ExtractM
(Trace, [LHsExpr GhcPs])
forall a b. (a -> b) -> a -> b
$ (Type
-> RuleT
Judgement
(Trace, LHsExpr GhcPs)
TacticError
TacticState
ExtractM
(Trace, LHsExpr GhcPs))
-> [Type]
-> RuleT
Judgement
(Trace, LHsExpr GhcPs)
TacticError
TacticState
ExtractM
[(Trace, LHsExpr GhcPs)]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse ( Judgement
-> RuleT
Judgement
(Trace, LHsExpr GhcPs)
TacticError
TacticState
ExtractM
(Trace, LHsExpr GhcPs)
newSubgoal
(Judgement
-> RuleT
Judgement
(Trace, LHsExpr GhcPs)
TacticError
TacticState
ExtractM
(Trace, LHsExpr GhcPs))
-> (Type -> Judgement)
-> Type
-> RuleT
Judgement
(Trace, LHsExpr GhcPs)
TacticError
TacticState
ExtractM
(Trace, LHsExpr GhcPs)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Judgement -> Judgement
blacklistingDestruct
(Judgement -> Judgement)
-> (Type -> Judgement) -> Type -> Judgement
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (CType -> Judgement -> Judgement)
-> Judgement -> CType -> Judgement
forall a b c. (a -> b -> c) -> b -> a -> c
flip CType -> Judgement -> Judgement
forall a. a -> Judgement' a -> Judgement' a
withNewGoal Judgement
jdg
(CType -> Judgement) -> (Type -> CType) -> Type -> Judgement
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> CType
CType
) [Type]
args
(Trace, LHsExpr GhcPs)
-> RuleT
Judgement
(Trace, LHsExpr GhcPs)
TacticError
TacticState
ExtractM
(Trace, LHsExpr GhcPs)
forall (f :: * -> *) a. Applicative f => a -> f a
pure
((Trace, LHsExpr GhcPs)
-> RuleT
Judgement
(Trace, LHsExpr GhcPs)
TacticError
TacticState
ExtractM
(Trace, LHsExpr GhcPs))
-> ([HsExpr GhcPs] -> (Trace, LHsExpr GhcPs))
-> [HsExpr GhcPs]
-> RuleT
Judgement
(Trace, LHsExpr GhcPs)
TacticError
TacticState
ExtractM
(Trace, LHsExpr GhcPs)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Trace
tr, )
(LHsExpr GhcPs -> (Trace, LHsExpr GhcPs))
-> ([HsExpr GhcPs] -> LHsExpr GhcPs)
-> [HsExpr GhcPs]
-> (Trace, LHsExpr GhcPs)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HsExpr GhcPs -> LHsExpr GhcPs
forall a. HasSrcSpan a => SrcSpanLess a -> a
noLoc
(HsExpr GhcPs -> LHsExpr GhcPs)
-> ([HsExpr GhcPs] -> HsExpr GhcPs)
-> [HsExpr GhcPs]
-> LHsExpr GhcPs
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (HsExpr GhcPs -> HsExpr GhcPs -> HsExpr GhcPs)
-> HsExpr GhcPs -> [HsExpr GhcPs] -> HsExpr GhcPs
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' HsExpr GhcPs -> HsExpr GhcPs -> HsExpr GhcPs
forall e. App e => e -> e -> e
(@@) (OccName -> HsExpr GhcPs
forall a. Var a => OccName -> a
var' OccName
func)
([HsExpr GhcPs]
-> RuleT
Judgement
(Trace, LHsExpr GhcPs)
TacticError
TacticState
ExtractM
(Trace, LHsExpr GhcPs))
-> [HsExpr GhcPs]
-> RuleT
Judgement
(Trace, LHsExpr GhcPs)
TacticError
TacticState
ExtractM
(Trace, LHsExpr GhcPs)
forall a b. (a -> b) -> a -> b
$ (LHsExpr GhcPs -> HsExpr GhcPs)
-> [LHsExpr GhcPs] -> [HsExpr GhcPs]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap LHsExpr GhcPs -> HsExpr GhcPs
forall a. HasSrcSpan a => a -> SrcSpanLess a
unLoc [LHsExpr GhcPs]
sgs
Maybe (HyInfo CType)
Nothing -> do
TacticError -> TacticsM ()
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TacticError -> TacticsM ()) -> TacticError -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ String -> CType -> TacticError
GoalMismatch String
"apply" CType
g
split :: TacticsM ()
split :: TacticsM ()
split = String -> TacticsM () -> TacticsM ()
forall (m :: * -> *) jdg ext err s a.
Functor m =>
String
-> TacticT jdg (Trace, ext) err s m a
-> TacticT jdg (Trace, ext) err s m a
tracing String
"split(user)" (TacticsM () -> TacticsM ()) -> TacticsM () -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ do
Judgement
jdg <- TacticT
Judgement
(Trace, LHsExpr GhcPs)
TacticError
TacticState
ExtractM
Judgement
forall (m :: * -> *) jdg ext err s.
Functor m =>
TacticT jdg ext err s m jdg
goal
let g :: CType
g = Judgement -> CType
forall a. Judgement' a -> a
jGoal Judgement
jdg
case HasDebugCallStack => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe (Type -> Maybe (TyCon, [Type])) -> Type -> Maybe (TyCon, [Type])
forall a b. (a -> b) -> a -> b
$ CType -> Type
unCType CType
g of
Maybe (TyCon, [Type])
Nothing -> TacticError -> TacticsM ()
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TacticError -> TacticsM ()) -> TacticError -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ String -> CType -> TacticError
GoalMismatch String
"split" CType
g
Just (TyCon
tc, [Type]
_) -> do
let dcs :: [DataCon]
dcs = TyCon -> [DataCon]
tyConDataCons TyCon
tc
[TacticsM ()] -> TacticsM ()
forall (m :: * -> *) jdg ext err s a.
Monad m =>
[TacticT jdg ext err s m a] -> TacticT jdg ext err s m a
choice ([TacticsM ()] -> TacticsM ()) -> [TacticsM ()] -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ (DataCon -> TacticsM ()) -> [DataCon] -> [TacticsM ()]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap DataCon -> TacticsM ()
splitDataCon [DataCon]
dcs
splitAuto :: TacticsM ()
splitAuto :: TacticsM ()
splitAuto = TacticsM () -> TacticsM ()
forall a. TacticsM a -> TacticsM a
requireConcreteHole (TacticsM () -> TacticsM ()) -> TacticsM () -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ String -> TacticsM () -> TacticsM ()
forall (m :: * -> *) jdg ext err s a.
Functor m =>
String
-> TacticT jdg (Trace, ext) err s m a
-> TacticT jdg (Trace, ext) err s m a
tracing String
"split(auto)" (TacticsM () -> TacticsM ()) -> TacticsM () -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ do
Judgement
jdg <- TacticT
Judgement
(Trace, LHsExpr GhcPs)
TacticError
TacticState
ExtractM
Judgement
forall (m :: * -> *) jdg ext err s.
Functor m =>
TacticT jdg ext err s m jdg
goal
let g :: CType
g = Judgement -> CType
forall a. Judgement' a -> a
jGoal Judgement
jdg
case HasDebugCallStack => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe (Type -> Maybe (TyCon, [Type])) -> Type -> Maybe (TyCon, [Type])
forall a b. (a -> b) -> a -> b
$ CType -> Type
unCType CType
g of
Maybe (TyCon, [Type])
Nothing -> TacticError -> TacticsM ()
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TacticError -> TacticsM ()) -> TacticError -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ String -> CType -> TacticError
GoalMismatch String
"split" CType
g
Just (TyCon
tc, [Type]
_) -> do
let dcs :: [DataCon]
dcs = TyCon -> [DataCon]
tyConDataCons TyCon
tc
case Judgement -> Bool
isSplitWhitelisted Judgement
jdg of
Bool
True -> [TacticsM ()] -> TacticsM ()
forall (m :: * -> *) jdg ext err s a.
Monad m =>
[TacticT jdg ext err s m a] -> TacticT jdg ext err s m a
choice ([TacticsM ()] -> TacticsM ()) -> [TacticsM ()] -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ (DataCon -> TacticsM ()) -> [DataCon] -> [TacticsM ()]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap DataCon -> TacticsM ()
splitDataCon [DataCon]
dcs
Bool
False -> do
[TacticsM ()] -> TacticsM ()
forall (m :: * -> *) jdg ext err s a.
Monad m =>
[TacticT jdg ext err s m a] -> TacticT jdg ext err s m a
choice ([TacticsM ()] -> TacticsM ()) -> [TacticsM ()] -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ ((DataCon -> TacticsM ()) -> [DataCon] -> [TacticsM ()])
-> [DataCon] -> (DataCon -> TacticsM ()) -> [TacticsM ()]
forall a b c. (a -> b -> c) -> b -> a -> c
flip (DataCon -> TacticsM ()) -> [DataCon] -> [TacticsM ()]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [DataCon]
dcs ((DataCon -> TacticsM ()) -> [TacticsM ()])
-> (DataCon -> TacticsM ()) -> [TacticsM ()]
forall a b. (a -> b) -> a -> b
$ \DataCon
dc -> TacticsM () -> TacticsM ()
requireNewHoles (TacticsM () -> TacticsM ()) -> TacticsM () -> TacticsM ()
forall a b. (a -> b) -> a -> b
$
DataCon -> TacticsM ()
splitDataCon DataCon
dc
requireNewHoles :: TacticsM () -> TacticsM ()
requireNewHoles :: TacticsM () -> TacticsM ()
requireNewHoles TacticsM ()
m = do
Judgement
jdg <- TacticT
Judgement
(Trace, LHsExpr GhcPs)
TacticError
TacticState
ExtractM
Judgement
forall (m :: * -> *) jdg ext err s.
Functor m =>
TacticT jdg ext err s m jdg
goal
TacticsM () -> ([Judgement] -> Maybe TacticError) -> TacticsM ()
forall ext (m :: * -> *) jdg err s.
MonadExtract ext m =>
TacticT jdg ext err s m ()
-> ([jdg] -> Maybe err) -> TacticT jdg ext err s m ()
pruning TacticsM ()
m (([Judgement] -> Maybe TacticError) -> TacticsM ())
-> ([Judgement] -> Maybe TacticError) -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ \[Judgement]
jdgs ->
case [Judgement] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Judgement]
jdgs Bool -> Bool -> Bool
|| (CType -> Bool) -> [CType] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (CType -> CType -> Bool
forall a. Eq a => a -> a -> Bool
/= Judgement -> CType
forall a. Judgement' a -> a
jGoal Judgement
jdg) ((Judgement -> CType) -> [Judgement] -> [CType]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Judgement -> CType
forall a. Judgement' a -> a
jGoal [Judgement]
jdgs) of
Bool
True -> Maybe TacticError
forall a. Maybe a
Nothing
Bool
False -> TacticError -> Maybe TacticError
forall a. a -> Maybe a
Just TacticError
NoProgress
splitDataCon :: DataCon -> TacticsM ()
splitDataCon :: DataCon -> TacticsM ()
splitDataCon DataCon
dc =
TacticsM () -> TacticsM ()
forall a. TacticsM a -> TacticsM a
requireConcreteHole (TacticsM () -> TacticsM ()) -> TacticsM () -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ String -> TacticsM () -> TacticsM ()
forall (m :: * -> *) jdg ext err s a.
Functor m =>
String
-> TacticT jdg (Trace, ext) err s m a
-> TacticT jdg (Trace, ext) err s m a
tracing (String
"splitDataCon:" String -> String -> String
forall a. Semigroup a => a -> a -> a
<> DataCon -> String
forall a. Show a => a -> String
show DataCon
dc) (TacticsM () -> TacticsM ()) -> TacticsM () -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ (Judgement
-> RuleT
Judgement
(Trace, LHsExpr GhcPs)
TacticError
TacticState
ExtractM
(Trace, LHsExpr GhcPs))
-> TacticsM ()
forall (m :: * -> *) jdg ext err s.
Monad m =>
(jdg -> RuleT jdg ext err s m ext) -> TacticT jdg ext err s m ()
rule ((Judgement
-> RuleT
Judgement
(Trace, LHsExpr GhcPs)
TacticError
TacticState
ExtractM
(Trace, LHsExpr GhcPs))
-> TacticsM ())
-> (Judgement
-> RuleT
Judgement
(Trace, LHsExpr GhcPs)
TacticError
TacticState
ExtractM
(Trace, LHsExpr GhcPs))
-> TacticsM ()
forall a b. (a -> b) -> a -> b
$ \Judgement
jdg -> do
let g :: CType
g = Judgement -> CType
forall a. Judgement' a -> a
jGoal Judgement
jdg
case HasDebugCallStack => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe (Type -> Maybe (TyCon, [Type])) -> Type -> Maybe (TyCon, [Type])
forall a b. (a -> b) -> a -> b
$ CType -> Type
unCType CType
g of
Just (TyCon
tc, [Type]
apps) -> do
case DataCon -> [DataCon] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem DataCon
dc ([DataCon] -> Bool) -> [DataCon] -> Bool
forall a b. (a -> b) -> a -> b
$ TyCon -> [DataCon]
tyConDataCons TyCon
tc of
Bool
True -> Judgement
-> DataCon
-> [Type]
-> RuleT
Judgement
(Trace, LHsExpr GhcPs)
TacticError
TacticState
ExtractM
(Trace, LHsExpr GhcPs)
buildDataCon (Judgement -> Judgement
unwhitelistingSplit Judgement
jdg) DataCon
dc [Type]
apps
Bool
False -> TacticError
-> RuleT
Judgement
(Trace, LHsExpr GhcPs)
TacticError
TacticState
ExtractM
(Trace, LHsExpr GhcPs)
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TacticError
-> RuleT
Judgement
(Trace, LHsExpr GhcPs)
TacticError
TacticState
ExtractM
(Trace, LHsExpr GhcPs))
-> TacticError
-> RuleT
Judgement
(Trace, LHsExpr GhcPs)
TacticError
TacticState
ExtractM
(Trace, LHsExpr GhcPs)
forall a b. (a -> b) -> a -> b
$ DataCon -> TacticError
IncorrectDataCon DataCon
dc
Maybe (TyCon, [Type])
Nothing -> TacticError
-> RuleT
Judgement
(Trace, LHsExpr GhcPs)
TacticError
TacticState
ExtractM
(Trace, LHsExpr GhcPs)
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TacticError
-> RuleT
Judgement
(Trace, LHsExpr GhcPs)
TacticError
TacticState
ExtractM
(Trace, LHsExpr GhcPs))
-> TacticError
-> RuleT
Judgement
(Trace, LHsExpr GhcPs)
TacticError
TacticState
ExtractM
(Trace, LHsExpr GhcPs)
forall a b. (a -> b) -> a -> b
$ String -> CType -> TacticError
GoalMismatch String
"splitDataCon" CType
g
matching :: (Judgement -> TacticsM ()) -> TacticsM ()
matching :: (Judgement -> TacticsM ()) -> TacticsM ()
matching Judgement -> TacticsM ()
f = StateT
Judgement
(ProofStateT
(Trace, LHsExpr GhcPs)
(Trace, LHsExpr GhcPs)
TacticError
TacticState
ExtractM)
()
-> TacticsM ()
forall jdg ext err s (m :: * -> *) a.
StateT jdg (ProofStateT ext ext err s m) a
-> TacticT jdg ext err s m a
TacticT (StateT
Judgement
(ProofStateT
(Trace, LHsExpr GhcPs)
(Trace, LHsExpr GhcPs)
TacticError
TacticState
ExtractM)
()
-> TacticsM ())
-> StateT
Judgement
(ProofStateT
(Trace, LHsExpr GhcPs)
(Trace, LHsExpr GhcPs)
TacticError
TacticState
ExtractM)
()
-> TacticsM ()
forall a b. (a -> b) -> a -> b
$ (Judgement
-> ProofStateT
(Trace, LHsExpr GhcPs)
(Trace, LHsExpr GhcPs)
TacticError
TacticState
ExtractM
((), Judgement))
-> StateT
Judgement
(ProofStateT
(Trace, LHsExpr GhcPs)
(Trace, LHsExpr GhcPs)
TacticError
TacticState
ExtractM)
()
forall s (m :: * -> *) a. (s -> m (a, s)) -> StateT s m a
StateT ((Judgement
-> ProofStateT
(Trace, LHsExpr GhcPs)
(Trace, LHsExpr GhcPs)
TacticError
TacticState
ExtractM
((), Judgement))
-> StateT
Judgement
(ProofStateT
(Trace, LHsExpr GhcPs)
(Trace, LHsExpr GhcPs)
TacticError
TacticState
ExtractM)
())
-> (Judgement
-> ProofStateT
(Trace, LHsExpr GhcPs)
(Trace, LHsExpr GhcPs)
TacticError
TacticState
ExtractM
((), Judgement))
-> StateT
Judgement
(ProofStateT
(Trace, LHsExpr GhcPs)
(Trace, LHsExpr GhcPs)
TacticError
TacticState
ExtractM)
()
forall a b. (a -> b) -> a -> b
$ \Judgement
s -> StateT
Judgement
(ProofStateT
(Trace, LHsExpr GhcPs)
(Trace, LHsExpr GhcPs)
TacticError
TacticState
ExtractM)
()
-> Judgement
-> ProofStateT
(Trace, LHsExpr GhcPs)
(Trace, LHsExpr GhcPs)
TacticError
TacticState
ExtractM
((), Judgement)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT (TacticsM ()
-> StateT
Judgement
(ProofStateT
(Trace, LHsExpr GhcPs)
(Trace, LHsExpr GhcPs)
TacticError
TacticState
ExtractM)
()
forall jdg ext err s (m :: * -> *) a.
TacticT jdg ext err s m a
-> StateT jdg (ProofStateT ext ext err s m) a
unTacticT (TacticsM ()
-> StateT
Judgement
(ProofStateT
(Trace, LHsExpr GhcPs)
(Trace, LHsExpr GhcPs)
TacticError
TacticState
ExtractM)
())
-> TacticsM ()
-> StateT
Judgement
(ProofStateT
(Trace, LHsExpr GhcPs)
(Trace, LHsExpr GhcPs)
TacticError
TacticState
ExtractM)
()
forall a b. (a -> b) -> a -> b
$ Judgement -> TacticsM ()
f Judgement
s) Judgement
s
attemptOn :: (Judgement -> [a]) -> (a -> TacticsM ()) -> TacticsM ()
attemptOn :: (Judgement -> [a]) -> (a -> TacticsM ()) -> TacticsM ()
attemptOn Judgement -> [a]
getNames a -> TacticsM ()
tac = (Judgement -> TacticsM ()) -> TacticsM ()
matching ([TacticsM ()] -> TacticsM ()
forall (m :: * -> *) jdg ext err s a.
Monad m =>
[TacticT jdg ext err s m a] -> TacticT jdg ext err s m a
choice ([TacticsM ()] -> TacticsM ())
-> (Judgement -> [TacticsM ()]) -> Judgement -> TacticsM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> TacticsM ()) -> [a] -> [TacticsM ()]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\a
s -> a -> TacticsM ()
tac a
s) ([a] -> [TacticsM ()])
-> (Judgement -> [a]) -> Judgement -> [TacticsM ()]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Judgement -> [a]
getNames)
localTactic :: TacticsM a -> (Judgement -> Judgement) -> TacticsM a
localTactic :: TacticsM a -> (Judgement -> Judgement) -> TacticsM a
localTactic TacticsM a
t Judgement -> Judgement
f = do
StateT
Judgement
(ProofStateT
(Trace, LHsExpr GhcPs)
(Trace, LHsExpr GhcPs)
TacticError
TacticState
ExtractM)
a
-> TacticsM a
forall jdg ext err s (m :: * -> *) a.
StateT jdg (ProofStateT ext ext err s m) a
-> TacticT jdg ext err s m a
TacticT (StateT
Judgement
(ProofStateT
(Trace, LHsExpr GhcPs)
(Trace, LHsExpr GhcPs)
TacticError
TacticState
ExtractM)
a
-> TacticsM a)
-> StateT
Judgement
(ProofStateT
(Trace, LHsExpr GhcPs)
(Trace, LHsExpr GhcPs)
TacticError
TacticState
ExtractM)
a
-> TacticsM a
forall a b. (a -> b) -> a -> b
$ (Judgement
-> ProofStateT
(Trace, LHsExpr GhcPs)
(Trace, LHsExpr GhcPs)
TacticError
TacticState
ExtractM
(a, Judgement))
-> StateT
Judgement
(ProofStateT
(Trace, LHsExpr GhcPs)
(Trace, LHsExpr GhcPs)
TacticError
TacticState
ExtractM)
a
forall s (m :: * -> *) a. (s -> m (a, s)) -> StateT s m a
StateT ((Judgement
-> ProofStateT
(Trace, LHsExpr GhcPs)
(Trace, LHsExpr GhcPs)
TacticError
TacticState
ExtractM
(a, Judgement))
-> StateT
Judgement
(ProofStateT
(Trace, LHsExpr GhcPs)
(Trace, LHsExpr GhcPs)
TacticError
TacticState
ExtractM)
a)
-> (Judgement
-> ProofStateT
(Trace, LHsExpr GhcPs)
(Trace, LHsExpr GhcPs)
TacticError
TacticState
ExtractM
(a, Judgement))
-> StateT
Judgement
(ProofStateT
(Trace, LHsExpr GhcPs)
(Trace, LHsExpr GhcPs)
TacticError
TacticState
ExtractM)
a
forall a b. (a -> b) -> a -> b
$ \Judgement
jdg ->
StateT
Judgement
(ProofStateT
(Trace, LHsExpr GhcPs)
(Trace, LHsExpr GhcPs)
TacticError
TacticState
ExtractM)
a
-> Judgement
-> ProofStateT
(Trace, LHsExpr GhcPs)
(Trace, LHsExpr GhcPs)
TacticError
TacticState
ExtractM
(a, Judgement)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT (TacticsM a
-> StateT
Judgement
(ProofStateT
(Trace, LHsExpr GhcPs)
(Trace, LHsExpr GhcPs)
TacticError
TacticState
ExtractM)
a
forall jdg ext err s (m :: * -> *) a.
TacticT jdg ext err s m a
-> StateT jdg (ProofStateT ext ext err s m) a
unTacticT TacticsM a
t) (Judgement
-> ProofStateT
(Trace, LHsExpr GhcPs)
(Trace, LHsExpr GhcPs)
TacticError
TacticState
ExtractM
(a, Judgement))
-> Judgement
-> ProofStateT
(Trace, LHsExpr GhcPs)
(Trace, LHsExpr GhcPs)
TacticError
TacticState
ExtractM
(a, Judgement)
forall a b. (a -> b) -> a -> b
$ Judgement -> Judgement
f Judgement
jdg
auto' :: Int -> TacticsM ()
auto' :: Int -> TacticsM ()
auto' Int
0 = TacticError -> TacticsM ()
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError TacticError
NoProgress
auto' Int
n = do
let loop :: TacticsM ()
loop = Int -> TacticsM ()
auto' (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)
TacticsM () -> TacticsM ()
forall (m :: * -> *) jdg ext err s.
Monad m =>
TacticT jdg ext err s m () -> TacticT jdg ext err s m ()
try TacticsM ()
intros
[TacticsM ()] -> TacticsM ()
forall (m :: * -> *) jdg ext err s a.
Monad m =>
[TacticT jdg ext err s m a] -> TacticT jdg ext err s m a
choice
[ (OccName -> TacticsM ()) -> TacticsM ()
overFunctions ((OccName -> TacticsM ()) -> TacticsM ())
-> (OccName -> TacticsM ()) -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ \OccName
fname -> do
OccName -> TacticsM ()
apply OccName
fname
TacticsM ()
loop
, (OccName -> TacticsM ()) -> TacticsM ()
overAlgebraicTerms ((OccName -> TacticsM ()) -> TacticsM ())
-> (OccName -> TacticsM ()) -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ \OccName
aname -> do
OccName -> TacticsM ()
destructAuto OccName
aname
TacticsM ()
loop
, TacticsM ()
splitAuto TacticsM () -> TacticsM () -> TacticsM ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> TacticsM ()
loop
, TacticsM ()
assumption TacticsM () -> TacticsM () -> TacticsM ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> TacticsM ()
loop
, TacticsM ()
recursion
]
overFunctions :: (OccName -> TacticsM ()) -> TacticsM ()
overFunctions :: (OccName -> TacticsM ()) -> TacticsM ()
overFunctions =
(Judgement -> [OccName]) -> (OccName -> TacticsM ()) -> TacticsM ()
forall a. (Judgement -> [a]) -> (a -> TacticsM ()) -> TacticsM ()
attemptOn ((Judgement -> [OccName])
-> (OccName -> TacticsM ()) -> TacticsM ())
-> (Judgement -> [OccName])
-> (OccName -> TacticsM ())
-> TacticsM ()
forall a b. (a -> b) -> a -> b
$ Map OccName (HyInfo CType) -> [OccName]
forall k a. Map k a -> [k]
M.keys (Map OccName (HyInfo CType) -> [OccName])
-> (Judgement -> Map OccName (HyInfo CType))
-> Judgement
-> [OccName]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (HyInfo CType -> Bool)
-> Map OccName (HyInfo CType) -> Map OccName (HyInfo CType)
forall a k. (a -> Bool) -> Map k a -> Map k a
M.filter (Type -> Bool
isFunction (Type -> Bool) -> (HyInfo CType -> Type) -> HyInfo CType -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CType -> Type
unCType (CType -> Type) -> (HyInfo CType -> CType) -> HyInfo CType -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HyInfo CType -> CType
forall a. HyInfo a -> a
hi_type) (Map OccName (HyInfo CType) -> Map OccName (HyInfo CType))
-> (Judgement -> Map OccName (HyInfo CType))
-> Judgement
-> Map OccName (HyInfo CType)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Judgement -> Map OccName (HyInfo CType)
forall a. Judgement' a -> Map OccName (HyInfo a)
jHypothesis
overAlgebraicTerms :: (OccName -> TacticsM ()) -> TacticsM ()
overAlgebraicTerms :: (OccName -> TacticsM ()) -> TacticsM ()
overAlgebraicTerms =
(Judgement -> [OccName]) -> (OccName -> TacticsM ()) -> TacticsM ()
forall a. (Judgement -> [a]) -> (a -> TacticsM ()) -> TacticsM ()
attemptOn ((Judgement -> [OccName])
-> (OccName -> TacticsM ()) -> TacticsM ())
-> (Judgement -> [OccName])
-> (OccName -> TacticsM ())
-> TacticsM ()
forall a b. (a -> b) -> a -> b
$
Map OccName (HyInfo CType) -> [OccName]
forall k a. Map k a -> [k]
M.keys (Map OccName (HyInfo CType) -> [OccName])
-> (Judgement -> Map OccName (HyInfo CType))
-> Judgement
-> [OccName]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (HyInfo CType -> Bool)
-> Map OccName (HyInfo CType) -> Map OccName (HyInfo CType)
forall a k. (a -> Bool) -> Map k a -> Map k a
M.filter (Maybe TyCon -> Bool
forall a. Maybe a -> Bool
isJust (Maybe TyCon -> Bool)
-> (HyInfo CType -> Maybe TyCon) -> HyInfo CType -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Maybe TyCon
algebraicTyCon (Type -> Maybe TyCon)
-> (HyInfo CType -> Type) -> HyInfo CType -> Maybe TyCon
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CType -> Type
unCType (CType -> Type) -> (HyInfo CType -> CType) -> HyInfo CType -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HyInfo CType -> CType
forall a. HyInfo a -> a
hi_type) (Map OccName (HyInfo CType) -> Map OccName (HyInfo CType))
-> (Judgement -> Map OccName (HyInfo CType))
-> Judgement
-> Map OccName (HyInfo CType)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Judgement -> Map OccName (HyInfo CType)
forall a. Judgement' a -> Map OccName (HyInfo a)
jHypothesis
allNames :: Judgement -> [OccName]
allNames :: Judgement -> [OccName]
allNames = Map OccName (HyInfo CType) -> [OccName]
forall k a. Map k a -> [k]
M.keys (Map OccName (HyInfo CType) -> [OccName])
-> (Judgement -> Map OccName (HyInfo CType))
-> Judgement
-> [OccName]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Judgement -> Map OccName (HyInfo CType)
forall a. Judgement' a -> Map OccName (HyInfo a)
jHypothesis