{-# LANGUAGE OverloadedStrings    #-}
{-# LANGUAGE RecordWildCards      #-}
{-# LANGUAGE UndecidableInstances #-}

{-# OPTIONS_GHC -fno-warn-orphans #-}

module Wingman.Types
  ( module Wingman.Types
  , module Wingman.Debug
  , OccName
  , Name
  , Type
  , TyVar
  , Span
  ) where

import           ConLike (ConLike)
import           Control.Lens hiding (Context)
import           Control.Monad.Reader
import           Control.Monad.State
import qualified Control.Monad.State.Strict as Strict
import           Data.Coerce
import           Data.Function
import           Data.Generics (mkM, everywhereM, Data, Typeable)
import           Data.Generics.Labels ()
import           Data.Generics.Product (field)
import           Data.List.NonEmpty (NonEmpty (..))
import           Data.Semigroup
import           Data.Set (Set)
import           Data.Text (Text)
import qualified Data.Text as T
import           Data.Tree
import           Development.IDE (Range)
import           Development.IDE.Core.UseStale
import           Development.IDE.GHC.Compat hiding (Node)
import           Development.IDE.GHC.Orphans ()
import           FamInstEnv (FamInstEnvs)
import           GHC.Exts (fromString)
import           GHC.Generics
import           GHC.SourceGen (var)
import           GhcPlugins (GlobalRdrElt, mkRdrUnqual)
import           InstEnv (InstEnvs(..))
import           OccName
import           Refinery.ProofState
import           Refinery.Tactic
import           Refinery.Tactic.Internal (TacticT(TacticT), RuleT (RuleT))
import           System.IO.Unsafe (unsafePerformIO)
import           Type (TCvSubst, Var, eqType, nonDetCmpType, emptyTCvSubst)
import           UniqSupply (takeUniqFromSupply, mkSplitUniqSupply, UniqSupply)
import           Unique (nonDetCmpUnique, Uniquable, getUnique, Unique, mkUnique)
import           Wingman.Debug
import Data.IORef


------------------------------------------------------------------------------
-- | The list of tactics exposed to the outside world. These are attached to
-- actual tactics via 'commandTactic' and are contextually provided to the
-- editor via 'commandProvider'.
data TacticCommand
  = Auto
  | Intros
  | IntroAndDestruct
  | Destruct
  | DestructPun
  | Homomorphism
  | DestructLambdaCase
  | HomomorphismLambdaCase
  | DestructAll
  | UseDataCon
  | Refine
  | BeginMetaprogram
  | RunMetaprogram
  deriving (TacticCommand -> TacticCommand -> Bool
(TacticCommand -> TacticCommand -> Bool)
-> (TacticCommand -> TacticCommand -> Bool) -> Eq TacticCommand
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: TacticCommand -> TacticCommand -> Bool
$c/= :: TacticCommand -> TacticCommand -> Bool
== :: TacticCommand -> TacticCommand -> Bool
$c== :: TacticCommand -> TacticCommand -> Bool
Eq, Eq TacticCommand
Eq TacticCommand
-> (TacticCommand -> TacticCommand -> Ordering)
-> (TacticCommand -> TacticCommand -> Bool)
-> (TacticCommand -> TacticCommand -> Bool)
-> (TacticCommand -> TacticCommand -> Bool)
-> (TacticCommand -> TacticCommand -> Bool)
-> (TacticCommand -> TacticCommand -> TacticCommand)
-> (TacticCommand -> TacticCommand -> TacticCommand)
-> Ord TacticCommand
TacticCommand -> TacticCommand -> Bool
TacticCommand -> TacticCommand -> Ordering
TacticCommand -> TacticCommand -> TacticCommand
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 :: TacticCommand -> TacticCommand -> TacticCommand
$cmin :: TacticCommand -> TacticCommand -> TacticCommand
max :: TacticCommand -> TacticCommand -> TacticCommand
$cmax :: TacticCommand -> TacticCommand -> TacticCommand
>= :: TacticCommand -> TacticCommand -> Bool
$c>= :: TacticCommand -> TacticCommand -> Bool
> :: TacticCommand -> TacticCommand -> Bool
$c> :: TacticCommand -> TacticCommand -> Bool
<= :: TacticCommand -> TacticCommand -> Bool
$c<= :: TacticCommand -> TacticCommand -> Bool
< :: TacticCommand -> TacticCommand -> Bool
$c< :: TacticCommand -> TacticCommand -> Bool
compare :: TacticCommand -> TacticCommand -> Ordering
$ccompare :: TacticCommand -> TacticCommand -> Ordering
$cp1Ord :: Eq TacticCommand
Ord, Int -> TacticCommand -> ShowS
[TacticCommand] -> ShowS
TacticCommand -> String
(Int -> TacticCommand -> ShowS)
-> (TacticCommand -> String)
-> ([TacticCommand] -> ShowS)
-> Show TacticCommand
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [TacticCommand] -> ShowS
$cshowList :: [TacticCommand] -> ShowS
show :: TacticCommand -> String
$cshow :: TacticCommand -> String
showsPrec :: Int -> TacticCommand -> ShowS
$cshowsPrec :: Int -> TacticCommand -> ShowS
Show, Int -> TacticCommand
TacticCommand -> Int
TacticCommand -> [TacticCommand]
TacticCommand -> TacticCommand
TacticCommand -> TacticCommand -> [TacticCommand]
TacticCommand -> TacticCommand -> TacticCommand -> [TacticCommand]
(TacticCommand -> TacticCommand)
-> (TacticCommand -> TacticCommand)
-> (Int -> TacticCommand)
-> (TacticCommand -> Int)
-> (TacticCommand -> [TacticCommand])
-> (TacticCommand -> TacticCommand -> [TacticCommand])
-> (TacticCommand -> TacticCommand -> [TacticCommand])
-> (TacticCommand
    -> TacticCommand -> TacticCommand -> [TacticCommand])
-> Enum TacticCommand
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
enumFromThenTo :: TacticCommand -> TacticCommand -> TacticCommand -> [TacticCommand]
$cenumFromThenTo :: TacticCommand -> TacticCommand -> TacticCommand -> [TacticCommand]
enumFromTo :: TacticCommand -> TacticCommand -> [TacticCommand]
$cenumFromTo :: TacticCommand -> TacticCommand -> [TacticCommand]
enumFromThen :: TacticCommand -> TacticCommand -> [TacticCommand]
$cenumFromThen :: TacticCommand -> TacticCommand -> [TacticCommand]
enumFrom :: TacticCommand -> [TacticCommand]
$cenumFrom :: TacticCommand -> [TacticCommand]
fromEnum :: TacticCommand -> Int
$cfromEnum :: TacticCommand -> Int
toEnum :: Int -> TacticCommand
$ctoEnum :: Int -> TacticCommand
pred :: TacticCommand -> TacticCommand
$cpred :: TacticCommand -> TacticCommand
succ :: TacticCommand -> TacticCommand
$csucc :: TacticCommand -> TacticCommand
Enum, TacticCommand
TacticCommand -> TacticCommand -> Bounded TacticCommand
forall a. a -> a -> Bounded a
maxBound :: TacticCommand
$cmaxBound :: TacticCommand
minBound :: TacticCommand
$cminBound :: TacticCommand
Bounded)

-- | Generate a title for the command.
tacticTitle :: TacticCommand -> T.Text -> T.Text
tacticTitle :: TacticCommand -> Text -> Text
tacticTitle = (Text -> Text -> Text
forall a. Monoid a => a -> a -> a
mappend Text
"Wingman: " (Text -> Text) -> (Text -> Text) -> Text -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
.) ((Text -> Text) -> Text -> Text)
-> (TacticCommand -> Text -> Text) -> TacticCommand -> Text -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TacticCommand -> Text -> Text
forall a. (IsString a, Semigroup a) => TacticCommand -> a -> a
go
  where
    go :: TacticCommand -> a -> a
go TacticCommand
Auto a
_                   = a
"Attempt to fill hole"
    go TacticCommand
Intros a
_                 = a
"Introduce lambda"
    go TacticCommand
IntroAndDestruct a
_       = a
"Introduce and destruct term"
    go TacticCommand
Destruct a
var             = a
"Case split on " a -> a -> a
forall a. Semigroup a => a -> a -> a
<> a
var
    go TacticCommand
DestructPun a
var          = a
"Split on " a -> a -> a
forall a. Semigroup a => a -> a -> a
<> a
var a -> a -> a
forall a. Semigroup a => a -> a -> a
<> a
" with NamedFieldPuns"
    go TacticCommand
Homomorphism a
var         = a
"Homomorphic case split on " a -> a -> a
forall a. Semigroup a => a -> a -> a
<> a
var
    go TacticCommand
DestructLambdaCase a
_     = a
"Lambda case split"
    go TacticCommand
HomomorphismLambdaCase a
_ = a
"Homomorphic lambda case split"
    go TacticCommand
DestructAll a
_            = a
"Split all function arguments"
    go TacticCommand
UseDataCon a
dcon          = a
"Use constructor " a -> a -> a
forall a. Semigroup a => a -> a -> a
<> a
dcon
    go TacticCommand
Refine a
_                 = a
"Refine hole"
    go TacticCommand
BeginMetaprogram a
_       = a
"Use custom tactic block"
    go TacticCommand
RunMetaprogram a
_         = a
"Run custom tactic"


------------------------------------------------------------------------------
-- | Plugin configuration for tactics
data Config = Config
  { Config -> Int
cfg_max_use_ctor_actions :: Int
  , Config -> Int
cfg_timeout_seconds      :: Int
  , Config -> Int
cfg_auto_gas             :: Int
  , Config -> Bool
cfg_proofstate_styling   :: Bool
  }
  deriving (Config -> Config -> Bool
(Config -> Config -> Bool)
-> (Config -> Config -> Bool) -> Eq Config
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Config -> Config -> Bool
$c/= :: Config -> Config -> Bool
== :: Config -> Config -> Bool
$c== :: Config -> Config -> Bool
Eq, Eq Config
Eq Config
-> (Config -> Config -> Ordering)
-> (Config -> Config -> Bool)
-> (Config -> Config -> Bool)
-> (Config -> Config -> Bool)
-> (Config -> Config -> Bool)
-> (Config -> Config -> Config)
-> (Config -> Config -> Config)
-> Ord Config
Config -> Config -> Bool
Config -> Config -> Ordering
Config -> Config -> Config
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 :: Config -> Config -> Config
$cmin :: Config -> Config -> Config
max :: Config -> Config -> Config
$cmax :: Config -> Config -> Config
>= :: Config -> Config -> Bool
$c>= :: Config -> Config -> Bool
> :: Config -> Config -> Bool
$c> :: Config -> Config -> Bool
<= :: Config -> Config -> Bool
$c<= :: Config -> Config -> Bool
< :: Config -> Config -> Bool
$c< :: Config -> Config -> Bool
compare :: Config -> Config -> Ordering
$ccompare :: Config -> Config -> Ordering
$cp1Ord :: Eq Config
Ord, Int -> Config -> ShowS
[Config] -> ShowS
Config -> String
(Int -> Config -> ShowS)
-> (Config -> String) -> ([Config] -> ShowS) -> Show Config
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Config] -> ShowS
$cshowList :: [Config] -> ShowS
show :: Config -> String
$cshow :: Config -> String
showsPrec :: Int -> Config -> ShowS
$cshowsPrec :: Int -> Config -> ShowS
Show)

emptyConfig :: Config
emptyConfig :: Config
emptyConfig = Config :: Int -> Int -> Int -> Bool -> Config
Config
  { cfg_max_use_ctor_actions :: Int
cfg_max_use_ctor_actions = Int
5
  , cfg_timeout_seconds :: Int
cfg_timeout_seconds = Int
2
  , cfg_auto_gas :: Int
cfg_auto_gas = Int
4
  , cfg_proofstate_styling :: Bool
cfg_proofstate_styling = Bool
True
  }

------------------------------------------------------------------------------
-- | A wrapper around 'Type' which supports equality and ordering.
newtype CType = CType { CType -> Type
unCType :: Type }
  deriving stock (Typeable CType
DataType
Constr
Typeable CType
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> CType -> c CType)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c CType)
-> (CType -> Constr)
-> (CType -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c CType))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c CType))
-> ((forall b. Data b => b -> b) -> CType -> CType)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> CType -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> CType -> r)
-> (forall u. (forall d. Data d => d -> u) -> CType -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> CType -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> CType -> m CType)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> CType -> m CType)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> CType -> m CType)
-> Data CType
CType -> DataType
CType -> Constr
(forall b. Data b => b -> b) -> CType -> CType
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> CType -> c CType
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c CType
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> CType -> u
forall u. (forall d. Data d => d -> u) -> CType -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> CType -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> CType -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> CType -> m CType
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> CType -> m CType
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c CType
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> CType -> c CType
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c CType)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c CType)
$cCType :: Constr
$tCType :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> CType -> m CType
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> CType -> m CType
gmapMp :: (forall d. Data d => d -> m d) -> CType -> m CType
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> CType -> m CType
gmapM :: (forall d. Data d => d -> m d) -> CType -> m CType
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> CType -> m CType
gmapQi :: Int -> (forall d. Data d => d -> u) -> CType -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> CType -> u
gmapQ :: (forall d. Data d => d -> u) -> CType -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> CType -> [u]
gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> CType -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> CType -> r
gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> CType -> r
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> CType -> r
gmapT :: (forall b. Data b => b -> b) -> CType -> CType
$cgmapT :: (forall b. Data b => b -> b) -> CType -> CType
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c CType)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c CType)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c CType)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c CType)
dataTypeOf :: CType -> DataType
$cdataTypeOf :: CType -> DataType
toConstr :: CType -> Constr
$ctoConstr :: CType -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c CType
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c CType
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> CType -> c CType
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> CType -> c CType
$cp1Data :: Typeable CType
Data, Typeable)

instance Eq CType where
  == :: CType -> CType -> Bool
(==) = Type -> Type -> Bool
eqType (Type -> Type -> Bool) -> (CType -> Type) -> CType -> CType -> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` CType -> Type
unCType

instance Ord CType where
  compare :: CType -> CType -> Ordering
compare = Type -> Type -> Ordering
nonDetCmpType (Type -> Type -> Ordering)
-> (CType -> Type) -> CType -> CType -> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` CType -> Type
unCType

instance Show CType where
  show :: CType -> String
show  = Type -> String
forall a. Outputable a => a -> String
unsafeRender (Type -> String) -> (CType -> Type) -> CType -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CType -> Type
unCType

instance Show Name where
  show :: Name -> String
show  = Name -> String
forall a. Outputable a => a -> String
unsafeRender

instance Show Type where
  show :: Type -> String
show  = Type -> String
forall a. Outputable a => a -> String
unsafeRender

instance Show Var where
  show :: Var -> String
show  = Var -> String
forall a. Outputable a => a -> String
unsafeRender

instance Show TCvSubst where
  show :: TCvSubst -> String
show  = TCvSubst -> String
forall a. Outputable a => a -> String
unsafeRender

instance Show DataCon where
  show :: DataCon -> String
show  = DataCon -> String
forall a. Outputable a => a -> String
unsafeRender

instance Show Class where
  show :: Class -> String
show  = Class -> String
forall a. Outputable a => a -> String
unsafeRender

instance Show (HsExpr GhcPs) where
  show :: HsExpr GhcPs -> String
show  = HsExpr GhcPs -> String
forall a. Outputable a => a -> String
unsafeRender

instance Show (HsExpr GhcTc) where
  show :: HsExpr GhcTc -> String
show  = HsExpr GhcTc -> String
forall a. Outputable a => a -> String
unsafeRender

instance Show (HsDecl GhcPs) where
  show :: HsDecl GhcPs -> String
show  = HsDecl GhcPs -> String
forall a. Outputable a => a -> String
unsafeRender

instance Show (Pat GhcPs) where
  show :: Pat GhcPs -> String
show  = Pat GhcPs -> String
forall a. Outputable a => a -> String
unsafeRender

instance Show (LHsSigType GhcPs) where
  show :: LHsSigType GhcPs -> String
show  = LHsSigType GhcPs -> String
forall a. Outputable a => a -> String
unsafeRender

instance Show TyCon where
  show :: TyCon -> String
show  = TyCon -> String
forall a. Outputable a => a -> String
unsafeRender

instance Show ConLike where
  show :: ConLike -> String
show  = ConLike -> String
forall a. Outputable a => a -> String
unsafeRender

instance Show LexicalFixity where
  show :: LexicalFixity -> String
show  = LexicalFixity -> String
forall a. Outputable a => a -> String
unsafeRender


------------------------------------------------------------------------------
-- | The state that should be shared between subgoals. Extracts move towards
-- the root, judgments move towards the leaves, and the state moves *sideways*.
data TacticState = TacticState
    { TacticState -> Set Var
ts_skolems         :: !(Set TyVar)
      -- ^ The known skolems.
    , TacticState -> TCvSubst
ts_unifier         :: !TCvSubst
    , TacticState -> UniqSupply
ts_unique_gen :: !UniqSupply
    } deriving stock (Int -> TacticState -> ShowS
[TacticState] -> ShowS
TacticState -> String
(Int -> TacticState -> ShowS)
-> (TacticState -> String)
-> ([TacticState] -> ShowS)
-> Show TacticState
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [TacticState] -> ShowS
$cshowList :: [TacticState] -> ShowS
show :: TacticState -> String
$cshow :: TacticState -> String
showsPrec :: Int -> TacticState -> ShowS
$cshowsPrec :: Int -> TacticState -> ShowS
Show, (forall x. TacticState -> Rep TacticState x)
-> (forall x. Rep TacticState x -> TacticState)
-> Generic TacticState
forall x. Rep TacticState x -> TacticState
forall x. TacticState -> Rep TacticState x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep TacticState x -> TacticState
$cfrom :: forall x. TacticState -> Rep TacticState x
Generic)

instance Show UniqSupply where
  show :: UniqSupply -> String
show UniqSupply
_ = String
"<uniqsupply>"


------------------------------------------------------------------------------
-- | A 'UniqSupply' to use in 'defaultTacticState'
unsafeDefaultUniqueSupply :: UniqSupply
unsafeDefaultUniqueSupply :: UniqSupply
unsafeDefaultUniqueSupply =
  IO UniqSupply -> UniqSupply
forall a. IO a -> a
unsafePerformIO (IO UniqSupply -> UniqSupply) -> IO UniqSupply -> UniqSupply
forall a b. (a -> b) -> a -> b
$ Char -> IO UniqSupply
mkSplitUniqSupply Char
'w'
{-# NOINLINE unsafeDefaultUniqueSupply #-}


defaultTacticState :: TacticState
defaultTacticState :: TacticState
defaultTacticState =
  TacticState :: Set Var -> TCvSubst -> UniqSupply -> TacticState
TacticState
    { ts_skolems :: Set Var
ts_skolems         = Set Var
forall a. Monoid a => a
mempty
    , ts_unifier :: TCvSubst
ts_unifier         = TCvSubst
emptyTCvSubst
    , ts_unique_gen :: UniqSupply
ts_unique_gen      = UniqSupply
unsafeDefaultUniqueSupply
    }


------------------------------------------------------------------------------
-- | Generate a new 'Unique'
freshUnique :: MonadState TacticState m => m Unique
freshUnique :: m Unique
freshUnique = do
  (Unique
uniq, UniqSupply
supply) <- (TacticState -> (Unique, UniqSupply)) -> m (Unique, UniqSupply)
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets ((TacticState -> (Unique, UniqSupply)) -> m (Unique, UniqSupply))
-> (TacticState -> (Unique, UniqSupply)) -> m (Unique, UniqSupply)
forall a b. (a -> b) -> a -> b
$ UniqSupply -> (Unique, UniqSupply)
takeUniqFromSupply (UniqSupply -> (Unique, UniqSupply))
-> (TacticState -> UniqSupply)
-> TacticState
-> (Unique, UniqSupply)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TacticState -> UniqSupply
ts_unique_gen
  (TacticState -> TacticState) -> m ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify' ((TacticState -> TacticState) -> m ())
-> (TacticState -> TacticState) -> m ()
forall a b. (a -> b) -> a -> b
$! forall s t a b. HasField "ts_unique_gen" s t a b => Lens s t a b
forall (field :: Symbol) s t a b.
HasField field s t a b =>
Lens s t a b
field @"ts_unique_gen" ((UniqSupply -> Identity UniqSupply)
 -> TacticState -> Identity TacticState)
-> UniqSupply -> TacticState -> TacticState
forall s t a b. ASetter s t a b -> b -> s -> t
.~ UniqSupply
supply
  Unique -> m Unique
forall (f :: * -> *) a. Applicative f => a -> f a
pure Unique
uniq


------------------------------------------------------------------------------
-- | Describes where hypotheses came from. Used extensively to prune stupid
-- solutions from the search space.
data Provenance
  = -- | An argument given to the topmost function that contains the current
    -- hole. Recursive calls are restricted to values whose provenance lines up
    -- with the same argument.
    TopLevelArgPrv
      OccName   -- ^ Binding function
      Int       -- ^ Argument Position
      Int       -- ^ of how many arguments total?
    -- | A binding created in a pattern match.
  | PatternMatchPrv PatVal
    -- | A class method from the given context.
  | ClassMethodPrv
      (Uniquely Class)     -- ^ Class
    -- | A binding explicitly written by the user.
  | UserPrv
    -- | A binding explicitly imported by the user.
  | ImportPrv
    -- | The recursive hypothesis. Present only in the context of the recursion
    -- tactic.
  | RecursivePrv
    -- | A hypothesis which has been disallowed for some reason. It's important
    -- to keep these in the hypothesis set, rather than filtering it, in order
    -- to continue tracking downstream provenance.
  | DisallowedPrv DisallowReason Provenance
  deriving stock (Provenance -> Provenance -> Bool
(Provenance -> Provenance -> Bool)
-> (Provenance -> Provenance -> Bool) -> Eq Provenance
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Provenance -> Provenance -> Bool
$c/= :: Provenance -> Provenance -> Bool
== :: Provenance -> Provenance -> Bool
$c== :: Provenance -> Provenance -> Bool
Eq, Int -> Provenance -> ShowS
[Provenance] -> ShowS
Provenance -> String
(Int -> Provenance -> ShowS)
-> (Provenance -> String)
-> ([Provenance] -> ShowS)
-> Show Provenance
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Provenance] -> ShowS
$cshowList :: [Provenance] -> ShowS
show :: Provenance -> String
$cshow :: Provenance -> String
showsPrec :: Int -> Provenance -> ShowS
$cshowsPrec :: Int -> Provenance -> ShowS
Show, (forall x. Provenance -> Rep Provenance x)
-> (forall x. Rep Provenance x -> Provenance) -> Generic Provenance
forall x. Rep Provenance x -> Provenance
forall x. Provenance -> Rep Provenance x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Provenance x -> Provenance
$cfrom :: forall x. Provenance -> Rep Provenance x
Generic, Eq Provenance
Eq Provenance
-> (Provenance -> Provenance -> Ordering)
-> (Provenance -> Provenance -> Bool)
-> (Provenance -> Provenance -> Bool)
-> (Provenance -> Provenance -> Bool)
-> (Provenance -> Provenance -> Bool)
-> (Provenance -> Provenance -> Provenance)
-> (Provenance -> Provenance -> Provenance)
-> Ord Provenance
Provenance -> Provenance -> Bool
Provenance -> Provenance -> Ordering
Provenance -> Provenance -> Provenance
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 :: Provenance -> Provenance -> Provenance
$cmin :: Provenance -> Provenance -> Provenance
max :: Provenance -> Provenance -> Provenance
$cmax :: Provenance -> Provenance -> Provenance
>= :: Provenance -> Provenance -> Bool
$c>= :: Provenance -> Provenance -> Bool
> :: Provenance -> Provenance -> Bool
$c> :: Provenance -> Provenance -> Bool
<= :: Provenance -> Provenance -> Bool
$c<= :: Provenance -> Provenance -> Bool
< :: Provenance -> Provenance -> Bool
$c< :: Provenance -> Provenance -> Bool
compare :: Provenance -> Provenance -> Ordering
$ccompare :: Provenance -> Provenance -> Ordering
$cp1Ord :: Eq Provenance
Ord, Typeable Provenance
DataType
Constr
Typeable Provenance
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Provenance -> c Provenance)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Provenance)
-> (Provenance -> Constr)
-> (Provenance -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c Provenance))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c Provenance))
-> ((forall b. Data b => b -> b) -> Provenance -> Provenance)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> Provenance -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> Provenance -> r)
-> (forall u. (forall d. Data d => d -> u) -> Provenance -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> Provenance -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Provenance -> m Provenance)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Provenance -> m Provenance)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Provenance -> m Provenance)
-> Data Provenance
Provenance -> DataType
Provenance -> Constr
(forall b. Data b => b -> b) -> Provenance -> Provenance
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Provenance -> c Provenance
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Provenance
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> Provenance -> u
forall u. (forall d. Data d => d -> u) -> Provenance -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Provenance -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Provenance -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Provenance -> m Provenance
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Provenance -> m Provenance
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Provenance
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Provenance -> c Provenance
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Provenance)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Provenance)
$cDisallowedPrv :: Constr
$cRecursivePrv :: Constr
$cImportPrv :: Constr
$cUserPrv :: Constr
$cClassMethodPrv :: Constr
$cPatternMatchPrv :: Constr
$cTopLevelArgPrv :: Constr
$tProvenance :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> Provenance -> m Provenance
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Provenance -> m Provenance
gmapMp :: (forall d. Data d => d -> m d) -> Provenance -> m Provenance
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Provenance -> m Provenance
gmapM :: (forall d. Data d => d -> m d) -> Provenance -> m Provenance
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Provenance -> m Provenance
gmapQi :: Int -> (forall d. Data d => d -> u) -> Provenance -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Provenance -> u
gmapQ :: (forall d. Data d => d -> u) -> Provenance -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Provenance -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Provenance -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Provenance -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Provenance -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Provenance -> r
gmapT :: (forall b. Data b => b -> b) -> Provenance -> Provenance
$cgmapT :: (forall b. Data b => b -> b) -> Provenance -> Provenance
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Provenance)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Provenance)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c Provenance)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Provenance)
dataTypeOf :: Provenance -> DataType
$cdataTypeOf :: Provenance -> DataType
toConstr :: Provenance -> Constr
$ctoConstr :: Provenance -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Provenance
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Provenance
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Provenance -> c Provenance
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Provenance -> c Provenance
$cp1Data :: Typeable Provenance
Data, Typeable)


------------------------------------------------------------------------------
-- | Why was a hypothesis disallowed?
data DisallowReason
  = WrongBranch Int
  | Shadowed
  | RecursiveCall
  | AlreadyDestructed
  deriving stock (DisallowReason -> DisallowReason -> Bool
(DisallowReason -> DisallowReason -> Bool)
-> (DisallowReason -> DisallowReason -> Bool) -> Eq DisallowReason
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: DisallowReason -> DisallowReason -> Bool
$c/= :: DisallowReason -> DisallowReason -> Bool
== :: DisallowReason -> DisallowReason -> Bool
$c== :: DisallowReason -> DisallowReason -> Bool
Eq, Int -> DisallowReason -> ShowS
[DisallowReason] -> ShowS
DisallowReason -> String
(Int -> DisallowReason -> ShowS)
-> (DisallowReason -> String)
-> ([DisallowReason] -> ShowS)
-> Show DisallowReason
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [DisallowReason] -> ShowS
$cshowList :: [DisallowReason] -> ShowS
show :: DisallowReason -> String
$cshow :: DisallowReason -> String
showsPrec :: Int -> DisallowReason -> ShowS
$cshowsPrec :: Int -> DisallowReason -> ShowS
Show, (forall x. DisallowReason -> Rep DisallowReason x)
-> (forall x. Rep DisallowReason x -> DisallowReason)
-> Generic DisallowReason
forall x. Rep DisallowReason x -> DisallowReason
forall x. DisallowReason -> Rep DisallowReason x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep DisallowReason x -> DisallowReason
$cfrom :: forall x. DisallowReason -> Rep DisallowReason x
Generic, Eq DisallowReason
Eq DisallowReason
-> (DisallowReason -> DisallowReason -> Ordering)
-> (DisallowReason -> DisallowReason -> Bool)
-> (DisallowReason -> DisallowReason -> Bool)
-> (DisallowReason -> DisallowReason -> Bool)
-> (DisallowReason -> DisallowReason -> Bool)
-> (DisallowReason -> DisallowReason -> DisallowReason)
-> (DisallowReason -> DisallowReason -> DisallowReason)
-> Ord DisallowReason
DisallowReason -> DisallowReason -> Bool
DisallowReason -> DisallowReason -> Ordering
DisallowReason -> DisallowReason -> DisallowReason
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 :: DisallowReason -> DisallowReason -> DisallowReason
$cmin :: DisallowReason -> DisallowReason -> DisallowReason
max :: DisallowReason -> DisallowReason -> DisallowReason
$cmax :: DisallowReason -> DisallowReason -> DisallowReason
>= :: DisallowReason -> DisallowReason -> Bool
$c>= :: DisallowReason -> DisallowReason -> Bool
> :: DisallowReason -> DisallowReason -> Bool
$c> :: DisallowReason -> DisallowReason -> Bool
<= :: DisallowReason -> DisallowReason -> Bool
$c<= :: DisallowReason -> DisallowReason -> Bool
< :: DisallowReason -> DisallowReason -> Bool
$c< :: DisallowReason -> DisallowReason -> Bool
compare :: DisallowReason -> DisallowReason -> Ordering
$ccompare :: DisallowReason -> DisallowReason -> Ordering
$cp1Ord :: Eq DisallowReason
Ord, Typeable DisallowReason
DataType
Constr
Typeable DisallowReason
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> DisallowReason -> c DisallowReason)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c DisallowReason)
-> (DisallowReason -> Constr)
-> (DisallowReason -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c DisallowReason))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c DisallowReason))
-> ((forall b. Data b => b -> b)
    -> DisallowReason -> DisallowReason)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> DisallowReason -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> DisallowReason -> r)
-> (forall u.
    (forall d. Data d => d -> u) -> DisallowReason -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> DisallowReason -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d)
    -> DisallowReason -> m DisallowReason)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> DisallowReason -> m DisallowReason)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> DisallowReason -> m DisallowReason)
-> Data DisallowReason
DisallowReason -> DataType
DisallowReason -> Constr
(forall b. Data b => b -> b) -> DisallowReason -> DisallowReason
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> DisallowReason -> c DisallowReason
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c DisallowReason
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u.
Int -> (forall d. Data d => d -> u) -> DisallowReason -> u
forall u. (forall d. Data d => d -> u) -> DisallowReason -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> DisallowReason -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> DisallowReason -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> DisallowReason -> m DisallowReason
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> DisallowReason -> m DisallowReason
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c DisallowReason
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> DisallowReason -> c DisallowReason
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c DisallowReason)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c DisallowReason)
$cAlreadyDestructed :: Constr
$cRecursiveCall :: Constr
$cShadowed :: Constr
$cWrongBranch :: Constr
$tDisallowReason :: DataType
gmapMo :: (forall d. Data d => d -> m d)
-> DisallowReason -> m DisallowReason
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> DisallowReason -> m DisallowReason
gmapMp :: (forall d. Data d => d -> m d)
-> DisallowReason -> m DisallowReason
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> DisallowReason -> m DisallowReason
gmapM :: (forall d. Data d => d -> m d)
-> DisallowReason -> m DisallowReason
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> DisallowReason -> m DisallowReason
gmapQi :: Int -> (forall d. Data d => d -> u) -> DisallowReason -> u
$cgmapQi :: forall u.
Int -> (forall d. Data d => d -> u) -> DisallowReason -> u
gmapQ :: (forall d. Data d => d -> u) -> DisallowReason -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> DisallowReason -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> DisallowReason -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> DisallowReason -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> DisallowReason -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> DisallowReason -> r
gmapT :: (forall b. Data b => b -> b) -> DisallowReason -> DisallowReason
$cgmapT :: (forall b. Data b => b -> b) -> DisallowReason -> DisallowReason
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c DisallowReason)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c DisallowReason)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c DisallowReason)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c DisallowReason)
dataTypeOf :: DisallowReason -> DataType
$cdataTypeOf :: DisallowReason -> DataType
toConstr :: DisallowReason -> Constr
$ctoConstr :: DisallowReason -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c DisallowReason
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c DisallowReason
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> DisallowReason -> c DisallowReason
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> DisallowReason -> c DisallowReason
$cp1Data :: Typeable DisallowReason
Data, Typeable)


------------------------------------------------------------------------------
-- | Provenance of a pattern value.
data PatVal = PatVal
  { PatVal -> Maybe OccName
pv_scrutinee :: Maybe OccName
    -- ^ Original scrutinee which created this PatVal. Nothing, for lambda
    -- case.
  , PatVal -> Set OccName
pv_ancestry  :: Set OccName
    -- ^ The set of values which had to be destructed to discover this term.
    -- Always contains the scrutinee.
  , PatVal -> Uniquely ConLike
pv_datacon   :: Uniquely ConLike
    -- ^ The datacon which introduced this term.
  , PatVal -> Int
pv_position  :: Int
    -- ^ The position of this binding in the datacon's arguments.
  } deriving stock (PatVal -> PatVal -> Bool
(PatVal -> PatVal -> Bool)
-> (PatVal -> PatVal -> Bool) -> Eq PatVal
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: PatVal -> PatVal -> Bool
$c/= :: PatVal -> PatVal -> Bool
== :: PatVal -> PatVal -> Bool
$c== :: PatVal -> PatVal -> Bool
Eq, Int -> PatVal -> ShowS
[PatVal] -> ShowS
PatVal -> String
(Int -> PatVal -> ShowS)
-> (PatVal -> String) -> ([PatVal] -> ShowS) -> Show PatVal
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [PatVal] -> ShowS
$cshowList :: [PatVal] -> ShowS
show :: PatVal -> String
$cshow :: PatVal -> String
showsPrec :: Int -> PatVal -> ShowS
$cshowsPrec :: Int -> PatVal -> ShowS
Show, (forall x. PatVal -> Rep PatVal x)
-> (forall x. Rep PatVal x -> PatVal) -> Generic PatVal
forall x. Rep PatVal x -> PatVal
forall x. PatVal -> Rep PatVal x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep PatVal x -> PatVal
$cfrom :: forall x. PatVal -> Rep PatVal x
Generic, Eq PatVal
Eq PatVal
-> (PatVal -> PatVal -> Ordering)
-> (PatVal -> PatVal -> Bool)
-> (PatVal -> PatVal -> Bool)
-> (PatVal -> PatVal -> Bool)
-> (PatVal -> PatVal -> Bool)
-> (PatVal -> PatVal -> PatVal)
-> (PatVal -> PatVal -> PatVal)
-> Ord PatVal
PatVal -> PatVal -> Bool
PatVal -> PatVal -> Ordering
PatVal -> PatVal -> PatVal
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 :: PatVal -> PatVal -> PatVal
$cmin :: PatVal -> PatVal -> PatVal
max :: PatVal -> PatVal -> PatVal
$cmax :: PatVal -> PatVal -> PatVal
>= :: PatVal -> PatVal -> Bool
$c>= :: PatVal -> PatVal -> Bool
> :: PatVal -> PatVal -> Bool
$c> :: PatVal -> PatVal -> Bool
<= :: PatVal -> PatVal -> Bool
$c<= :: PatVal -> PatVal -> Bool
< :: PatVal -> PatVal -> Bool
$c< :: PatVal -> PatVal -> Bool
compare :: PatVal -> PatVal -> Ordering
$ccompare :: PatVal -> PatVal -> Ordering
$cp1Ord :: Eq PatVal
Ord, Typeable PatVal
DataType
Constr
Typeable PatVal
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> PatVal -> c PatVal)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c PatVal)
-> (PatVal -> Constr)
-> (PatVal -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c PatVal))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c PatVal))
-> ((forall b. Data b => b -> b) -> PatVal -> PatVal)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> PatVal -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> PatVal -> r)
-> (forall u. (forall d. Data d => d -> u) -> PatVal -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> PatVal -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> PatVal -> m PatVal)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> PatVal -> m PatVal)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> PatVal -> m PatVal)
-> Data PatVal
PatVal -> DataType
PatVal -> Constr
(forall b. Data b => b -> b) -> PatVal -> PatVal
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> PatVal -> c PatVal
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c PatVal
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> PatVal -> u
forall u. (forall d. Data d => d -> u) -> PatVal -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> PatVal -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> PatVal -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> PatVal -> m PatVal
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> PatVal -> m PatVal
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c PatVal
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> PatVal -> c PatVal
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c PatVal)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c PatVal)
$cPatVal :: Constr
$tPatVal :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> PatVal -> m PatVal
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> PatVal -> m PatVal
gmapMp :: (forall d. Data d => d -> m d) -> PatVal -> m PatVal
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> PatVal -> m PatVal
gmapM :: (forall d. Data d => d -> m d) -> PatVal -> m PatVal
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> PatVal -> m PatVal
gmapQi :: Int -> (forall d. Data d => d -> u) -> PatVal -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> PatVal -> u
gmapQ :: (forall d. Data d => d -> u) -> PatVal -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> PatVal -> [u]
gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> PatVal -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> PatVal -> r
gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> PatVal -> r
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> PatVal -> r
gmapT :: (forall b. Data b => b -> b) -> PatVal -> PatVal
$cgmapT :: (forall b. Data b => b -> b) -> PatVal -> PatVal
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c PatVal)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c PatVal)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c PatVal)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c PatVal)
dataTypeOf :: PatVal -> DataType
$cdataTypeOf :: PatVal -> DataType
toConstr :: PatVal -> Constr
$ctoConstr :: PatVal -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c PatVal
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c PatVal
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> PatVal -> c PatVal
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> PatVal -> c PatVal
$cp1Data :: Typeable PatVal
Data, Typeable)


------------------------------------------------------------------------------
-- | A wrapper which uses a 'Uniquable' constraint for providing 'Eq' and 'Ord'
-- instances.
newtype Uniquely a = Uniquely { Uniquely a -> a
getViaUnique :: a }
  deriving Int -> Uniquely a -> ShowS
[Uniquely a] -> ShowS
Uniquely a -> String
(Int -> Uniquely a -> ShowS)
-> (Uniquely a -> String)
-> ([Uniquely a] -> ShowS)
-> Show (Uniquely a)
forall a. Show a => Int -> Uniquely a -> ShowS
forall a. Show a => [Uniquely a] -> ShowS
forall a. Show a => Uniquely a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Uniquely a] -> ShowS
$cshowList :: forall a. Show a => [Uniquely a] -> ShowS
show :: Uniquely a -> String
$cshow :: forall a. Show a => Uniquely a -> String
showsPrec :: Int -> Uniquely a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> Uniquely a -> ShowS
Show via a
  deriving stock (Typeable (Uniquely a)
DataType
Constr
Typeable (Uniquely a)
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Uniquely a -> c (Uniquely a))
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c (Uniquely a))
-> (Uniquely a -> Constr)
-> (Uniquely a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c (Uniquely a)))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c (Uniquely a)))
-> ((forall b. Data b => b -> b) -> Uniquely a -> Uniquely a)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> Uniquely a -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> Uniquely a -> r)
-> (forall u. (forall d. Data d => d -> u) -> Uniquely a -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> Uniquely a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Uniquely a -> m (Uniquely a))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Uniquely a -> m (Uniquely a))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Uniquely a -> m (Uniquely a))
-> Data (Uniquely a)
Uniquely a -> DataType
Uniquely a -> Constr
(forall d. Data d => c (t d)) -> Maybe (c (Uniquely a))
(forall b. Data b => b -> b) -> Uniquely a -> Uniquely a
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Uniquely a -> c (Uniquely a)
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Uniquely a)
forall a. Data a => Typeable (Uniquely a)
forall a. Data a => Uniquely a -> DataType
forall a. Data a => Uniquely a -> Constr
forall a.
Data a =>
(forall b. Data b => b -> b) -> Uniquely a -> Uniquely a
forall a u.
Data a =>
Int -> (forall d. Data d => d -> u) -> Uniquely a -> u
forall a u.
Data a =>
(forall d. Data d => d -> u) -> Uniquely a -> [u]
forall a r r'.
Data a =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Uniquely a -> r
forall a r r'.
Data a =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Uniquely a -> r
forall a (m :: * -> *).
(Data a, Monad m) =>
(forall d. Data d => d -> m d) -> Uniquely a -> m (Uniquely a)
forall a (m :: * -> *).
(Data a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Uniquely a -> m (Uniquely a)
forall a (c :: * -> *).
Data a =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Uniquely a)
forall a (c :: * -> *).
Data a =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Uniquely a -> c (Uniquely a)
forall a (t :: * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Uniquely a))
forall a (t :: * -> * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (Uniquely a))
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> Uniquely a -> u
forall u. (forall d. Data d => d -> u) -> Uniquely a -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Uniquely a -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Uniquely a -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Uniquely a -> m (Uniquely a)
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Uniquely a -> m (Uniquely a)
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Uniquely a)
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Uniquely a -> c (Uniquely a)
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (Uniquely a))
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (Uniquely a))
$cUniquely :: Constr
$tUniquely :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> Uniquely a -> m (Uniquely a)
$cgmapMo :: forall a (m :: * -> *).
(Data a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Uniquely a -> m (Uniquely a)
gmapMp :: (forall d. Data d => d -> m d) -> Uniquely a -> m (Uniquely a)
$cgmapMp :: forall a (m :: * -> *).
(Data a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Uniquely a -> m (Uniquely a)
gmapM :: (forall d. Data d => d -> m d) -> Uniquely a -> m (Uniquely a)
$cgmapM :: forall a (m :: * -> *).
(Data a, Monad m) =>
(forall d. Data d => d -> m d) -> Uniquely a -> m (Uniquely a)
gmapQi :: Int -> (forall d. Data d => d -> u) -> Uniquely a -> u
$cgmapQi :: forall a u.
Data a =>
Int -> (forall d. Data d => d -> u) -> Uniquely a -> u
gmapQ :: (forall d. Data d => d -> u) -> Uniquely a -> [u]
$cgmapQ :: forall a u.
Data a =>
(forall d. Data d => d -> u) -> Uniquely a -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Uniquely a -> r
$cgmapQr :: forall a r r'.
Data a =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Uniquely a -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Uniquely a -> r
$cgmapQl :: forall a r r'.
Data a =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Uniquely a -> r
gmapT :: (forall b. Data b => b -> b) -> Uniquely a -> Uniquely a
$cgmapT :: forall a.
Data a =>
(forall b. Data b => b -> b) -> Uniquely a -> Uniquely a
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (Uniquely a))
$cdataCast2 :: forall a (t :: * -> * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (Uniquely a))
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c (Uniquely a))
$cdataCast1 :: forall a (t :: * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Uniquely a))
dataTypeOf :: Uniquely a -> DataType
$cdataTypeOf :: forall a. Data a => Uniquely a -> DataType
toConstr :: Uniquely a -> Constr
$ctoConstr :: forall a. Data a => Uniquely a -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Uniquely a)
$cgunfold :: forall a (c :: * -> *).
Data a =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Uniquely a)
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Uniquely a -> c (Uniquely a)
$cgfoldl :: forall a (c :: * -> *).
Data a =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Uniquely a -> c (Uniquely a)
$cp1Data :: forall a. Data a => Typeable (Uniquely a)
Data, Typeable)

instance Uniquable a => Eq (Uniquely a) where
  == :: Uniquely a -> Uniquely a -> Bool
(==) = Unique -> Unique -> Bool
forall a. Eq a => a -> a -> Bool
(==) (Unique -> Unique -> Bool)
-> (Uniquely a -> Unique) -> Uniquely a -> Uniquely a -> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` a -> Unique
forall a. Uniquable a => a -> Unique
getUnique (a -> Unique) -> (Uniquely a -> a) -> Uniquely a -> Unique
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Uniquely a -> a
forall a. Uniquely a -> a
getViaUnique

instance Uniquable a => Ord (Uniquely a) where
  compare :: Uniquely a -> Uniquely a -> Ordering
compare = Unique -> Unique -> Ordering
nonDetCmpUnique (Unique -> Unique -> Ordering)
-> (Uniquely a -> Unique) -> Uniquely a -> Uniquely a -> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` a -> Unique
forall a. Uniquable a => a -> Unique
getUnique (a -> Unique) -> (Uniquely a -> a) -> Uniquely a -> Unique
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Uniquely a -> a
forall a. Uniquely a -> a
getViaUnique


-- NOTE(sandy): The usage of list here is mostly for convenience, but if it's
-- ever changed, make sure to correspondingly update
-- 'jAcceptableDestructTargets' so that it correctly identifies newly
-- introduced terms.
newtype Hypothesis a = Hypothesis
  { Hypothesis a -> [HyInfo a]
unHypothesis :: [HyInfo a]
  }
  deriving stock (a -> Hypothesis b -> Hypothesis a
(a -> b) -> Hypothesis a -> Hypothesis b
(forall a b. (a -> b) -> Hypothesis a -> Hypothesis b)
-> (forall a b. a -> Hypothesis b -> Hypothesis a)
-> Functor Hypothesis
forall a b. a -> Hypothesis b -> Hypothesis a
forall a b. (a -> b) -> Hypothesis a -> Hypothesis b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> Hypothesis b -> Hypothesis a
$c<$ :: forall a b. a -> Hypothesis b -> Hypothesis a
fmap :: (a -> b) -> Hypothesis a -> Hypothesis b
$cfmap :: forall a b. (a -> b) -> Hypothesis a -> Hypothesis b
Functor, Hypothesis a -> Hypothesis a -> Bool
(Hypothesis a -> Hypothesis a -> Bool)
-> (Hypothesis a -> Hypothesis a -> Bool) -> Eq (Hypothesis a)
forall a. Eq a => Hypothesis a -> Hypothesis a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Hypothesis a -> Hypothesis a -> Bool
$c/= :: forall a. Eq a => Hypothesis a -> Hypothesis a -> Bool
== :: Hypothesis a -> Hypothesis a -> Bool
$c== :: forall a. Eq a => Hypothesis a -> Hypothesis a -> Bool
Eq, Int -> Hypothesis a -> ShowS
[Hypothesis a] -> ShowS
Hypothesis a -> String
(Int -> Hypothesis a -> ShowS)
-> (Hypothesis a -> String)
-> ([Hypothesis a] -> ShowS)
-> Show (Hypothesis a)
forall a. Show a => Int -> Hypothesis a -> ShowS
forall a. Show a => [Hypothesis a] -> ShowS
forall a. Show a => Hypothesis a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Hypothesis a] -> ShowS
$cshowList :: forall a. Show a => [Hypothesis a] -> ShowS
show :: Hypothesis a -> String
$cshow :: forall a. Show a => Hypothesis a -> String
showsPrec :: Int -> Hypothesis a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> Hypothesis a -> ShowS
Show, (forall x. Hypothesis a -> Rep (Hypothesis a) x)
-> (forall x. Rep (Hypothesis a) x -> Hypothesis a)
-> Generic (Hypothesis a)
forall x. Rep (Hypothesis a) x -> Hypothesis a
forall x. Hypothesis a -> Rep (Hypothesis a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (Hypothesis a) x -> Hypothesis a
forall a x. Hypothesis a -> Rep (Hypothesis a) x
$cto :: forall a x. Rep (Hypothesis a) x -> Hypothesis a
$cfrom :: forall a x. Hypothesis a -> Rep (Hypothesis a) x
Generic, Eq (Hypothesis a)
Eq (Hypothesis a)
-> (Hypothesis a -> Hypothesis a -> Ordering)
-> (Hypothesis a -> Hypothesis a -> Bool)
-> (Hypothesis a -> Hypothesis a -> Bool)
-> (Hypothesis a -> Hypothesis a -> Bool)
-> (Hypothesis a -> Hypothesis a -> Bool)
-> (Hypothesis a -> Hypothesis a -> Hypothesis a)
-> (Hypothesis a -> Hypothesis a -> Hypothesis a)
-> Ord (Hypothesis a)
Hypothesis a -> Hypothesis a -> Bool
Hypothesis a -> Hypothesis a -> Ordering
Hypothesis a -> Hypothesis a -> Hypothesis a
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
forall a. Ord a => Eq (Hypothesis a)
forall a. Ord a => Hypothesis a -> Hypothesis a -> Bool
forall a. Ord a => Hypothesis a -> Hypothesis a -> Ordering
forall a. Ord a => Hypothesis a -> Hypothesis a -> Hypothesis a
min :: Hypothesis a -> Hypothesis a -> Hypothesis a
$cmin :: forall a. Ord a => Hypothesis a -> Hypothesis a -> Hypothesis a
max :: Hypothesis a -> Hypothesis a -> Hypothesis a
$cmax :: forall a. Ord a => Hypothesis a -> Hypothesis a -> Hypothesis a
>= :: Hypothesis a -> Hypothesis a -> Bool
$c>= :: forall a. Ord a => Hypothesis a -> Hypothesis a -> Bool
> :: Hypothesis a -> Hypothesis a -> Bool
$c> :: forall a. Ord a => Hypothesis a -> Hypothesis a -> Bool
<= :: Hypothesis a -> Hypothesis a -> Bool
$c<= :: forall a. Ord a => Hypothesis a -> Hypothesis a -> Bool
< :: Hypothesis a -> Hypothesis a -> Bool
$c< :: forall a. Ord a => Hypothesis a -> Hypothesis a -> Bool
compare :: Hypothesis a -> Hypothesis a -> Ordering
$ccompare :: forall a. Ord a => Hypothesis a -> Hypothesis a -> Ordering
$cp1Ord :: forall a. Ord a => Eq (Hypothesis a)
Ord, Typeable (Hypothesis a)
DataType
Constr
Typeable (Hypothesis a)
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Hypothesis a -> c (Hypothesis a))
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c (Hypothesis a))
-> (Hypothesis a -> Constr)
-> (Hypothesis a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c (Hypothesis a)))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c (Hypothesis a)))
-> ((forall b. Data b => b -> b) -> Hypothesis a -> Hypothesis a)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> Hypothesis a -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> Hypothesis a -> r)
-> (forall u. (forall d. Data d => d -> u) -> Hypothesis a -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> Hypothesis a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Hypothesis a -> m (Hypothesis a))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Hypothesis a -> m (Hypothesis a))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Hypothesis a -> m (Hypothesis a))
-> Data (Hypothesis a)
Hypothesis a -> DataType
Hypothesis a -> Constr
(forall d. Data d => c (t d)) -> Maybe (c (Hypothesis a))
(forall b. Data b => b -> b) -> Hypothesis a -> Hypothesis a
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Hypothesis a -> c (Hypothesis a)
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Hypothesis a)
forall a. Data a => Typeable (Hypothesis a)
forall a. Data a => Hypothesis a -> DataType
forall a. Data a => Hypothesis a -> Constr
forall a.
Data a =>
(forall b. Data b => b -> b) -> Hypothesis a -> Hypothesis a
forall a u.
Data a =>
Int -> (forall d. Data d => d -> u) -> Hypothesis a -> u
forall a u.
Data a =>
(forall d. Data d => d -> u) -> Hypothesis a -> [u]
forall a r r'.
Data a =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Hypothesis a -> r
forall a r r'.
Data a =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Hypothesis a -> r
forall a (m :: * -> *).
(Data a, Monad m) =>
(forall d. Data d => d -> m d) -> Hypothesis a -> m (Hypothesis a)
forall a (m :: * -> *).
(Data a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Hypothesis a -> m (Hypothesis a)
forall a (c :: * -> *).
Data a =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Hypothesis a)
forall a (c :: * -> *).
Data a =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Hypothesis a -> c (Hypothesis a)
forall a (t :: * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Hypothesis a))
forall a (t :: * -> * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (Hypothesis a))
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> Hypothesis a -> u
forall u. (forall d. Data d => d -> u) -> Hypothesis a -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Hypothesis a -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Hypothesis a -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Hypothesis a -> m (Hypothesis a)
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Hypothesis a -> m (Hypothesis a)
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Hypothesis a)
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Hypothesis a -> c (Hypothesis a)
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (Hypothesis a))
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (Hypothesis a))
$cHypothesis :: Constr
$tHypothesis :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> Hypothesis a -> m (Hypothesis a)
$cgmapMo :: forall a (m :: * -> *).
(Data a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Hypothesis a -> m (Hypothesis a)
gmapMp :: (forall d. Data d => d -> m d) -> Hypothesis a -> m (Hypothesis a)
$cgmapMp :: forall a (m :: * -> *).
(Data a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Hypothesis a -> m (Hypothesis a)
gmapM :: (forall d. Data d => d -> m d) -> Hypothesis a -> m (Hypothesis a)
$cgmapM :: forall a (m :: * -> *).
(Data a, Monad m) =>
(forall d. Data d => d -> m d) -> Hypothesis a -> m (Hypothesis a)
gmapQi :: Int -> (forall d. Data d => d -> u) -> Hypothesis a -> u
$cgmapQi :: forall a u.
Data a =>
Int -> (forall d. Data d => d -> u) -> Hypothesis a -> u
gmapQ :: (forall d. Data d => d -> u) -> Hypothesis a -> [u]
$cgmapQ :: forall a u.
Data a =>
(forall d. Data d => d -> u) -> Hypothesis a -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Hypothesis a -> r
$cgmapQr :: forall a r r'.
Data a =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Hypothesis a -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Hypothesis a -> r
$cgmapQl :: forall a r r'.
Data a =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Hypothesis a -> r
gmapT :: (forall b. Data b => b -> b) -> Hypothesis a -> Hypothesis a
$cgmapT :: forall a.
Data a =>
(forall b. Data b => b -> b) -> Hypothesis a -> Hypothesis a
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (Hypothesis a))
$cdataCast2 :: forall a (t :: * -> * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (Hypothesis a))
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c (Hypothesis a))
$cdataCast1 :: forall a (t :: * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Hypothesis a))
dataTypeOf :: Hypothesis a -> DataType
$cdataTypeOf :: forall a. Data a => Hypothesis a -> DataType
toConstr :: Hypothesis a -> Constr
$ctoConstr :: forall a. Data a => Hypothesis a -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Hypothesis a)
$cgunfold :: forall a (c :: * -> *).
Data a =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Hypothesis a)
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Hypothesis a -> c (Hypothesis a)
$cgfoldl :: forall a (c :: * -> *).
Data a =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Hypothesis a -> c (Hypothesis a)
$cp1Data :: forall a. Data a => Typeable (Hypothesis a)
Data, Typeable)
  deriving newtype (b -> Hypothesis a -> Hypothesis a
NonEmpty (Hypothesis a) -> Hypothesis a
Hypothesis a -> Hypothesis a -> Hypothesis a
(Hypothesis a -> Hypothesis a -> Hypothesis a)
-> (NonEmpty (Hypothesis a) -> Hypothesis a)
-> (forall b. Integral b => b -> Hypothesis a -> Hypothesis a)
-> Semigroup (Hypothesis a)
forall b. Integral b => b -> Hypothesis a -> Hypothesis a
forall a. NonEmpty (Hypothesis a) -> Hypothesis a
forall a. Hypothesis a -> Hypothesis a -> Hypothesis a
forall a.
(a -> a -> a)
-> (NonEmpty a -> a)
-> (forall b. Integral b => b -> a -> a)
-> Semigroup a
forall a b. Integral b => b -> Hypothesis a -> Hypothesis a
stimes :: b -> Hypothesis a -> Hypothesis a
$cstimes :: forall a b. Integral b => b -> Hypothesis a -> Hypothesis a
sconcat :: NonEmpty (Hypothesis a) -> Hypothesis a
$csconcat :: forall a. NonEmpty (Hypothesis a) -> Hypothesis a
<> :: Hypothesis a -> Hypothesis a -> Hypothesis a
$c<> :: forall a. Hypothesis a -> Hypothesis a -> Hypothesis a
Semigroup, Semigroup (Hypothesis a)
Hypothesis a
Semigroup (Hypothesis a)
-> Hypothesis a
-> (Hypothesis a -> Hypothesis a -> Hypothesis a)
-> ([Hypothesis a] -> Hypothesis a)
-> Monoid (Hypothesis a)
[Hypothesis a] -> Hypothesis a
Hypothesis a -> Hypothesis a -> Hypothesis a
forall a. Semigroup (Hypothesis a)
forall a. Hypothesis a
forall a.
Semigroup a -> a -> (a -> a -> a) -> ([a] -> a) -> Monoid a
forall a. [Hypothesis a] -> Hypothesis a
forall a. Hypothesis a -> Hypothesis a -> Hypothesis a
mconcat :: [Hypothesis a] -> Hypothesis a
$cmconcat :: forall a. [Hypothesis a] -> Hypothesis a
mappend :: Hypothesis a -> Hypothesis a -> Hypothesis a
$cmappend :: forall a. Hypothesis a -> Hypothesis a -> Hypothesis a
mempty :: Hypothesis a
$cmempty :: forall a. Hypothesis a
$cp1Monoid :: forall a. Semigroup (Hypothesis a)
Monoid)


------------------------------------------------------------------------------
-- | The provenance and type of a hypothesis term.
data HyInfo a = HyInfo
  { HyInfo a -> OccName
hi_name       :: OccName
  , HyInfo a -> Provenance
hi_provenance :: Provenance
  , HyInfo a -> a
hi_type       :: a
  }
  deriving stock (a -> HyInfo b -> HyInfo a
(a -> b) -> HyInfo a -> HyInfo b
(forall a b. (a -> b) -> HyInfo a -> HyInfo b)
-> (forall a b. a -> HyInfo b -> HyInfo a) -> Functor HyInfo
forall a b. a -> HyInfo b -> HyInfo a
forall a b. (a -> b) -> HyInfo a -> HyInfo b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> HyInfo b -> HyInfo a
$c<$ :: forall a b. a -> HyInfo b -> HyInfo a
fmap :: (a -> b) -> HyInfo a -> HyInfo b
$cfmap :: forall a b. (a -> b) -> HyInfo a -> HyInfo b
Functor, HyInfo a -> HyInfo a -> Bool
(HyInfo a -> HyInfo a -> Bool)
-> (HyInfo a -> HyInfo a -> Bool) -> Eq (HyInfo a)
forall a. Eq a => HyInfo a -> HyInfo a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: HyInfo a -> HyInfo a -> Bool
$c/= :: forall a. Eq a => HyInfo a -> HyInfo a -> Bool
== :: HyInfo a -> HyInfo a -> Bool
$c== :: forall a. Eq a => HyInfo a -> HyInfo a -> Bool
Eq, Int -> HyInfo a -> ShowS
[HyInfo a] -> ShowS
HyInfo a -> String
(Int -> HyInfo a -> ShowS)
-> (HyInfo a -> String) -> ([HyInfo a] -> ShowS) -> Show (HyInfo a)
forall a. Show a => Int -> HyInfo a -> ShowS
forall a. Show a => [HyInfo a] -> ShowS
forall a. Show a => HyInfo a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [HyInfo a] -> ShowS
$cshowList :: forall a. Show a => [HyInfo a] -> ShowS
show :: HyInfo a -> String
$cshow :: forall a. Show a => HyInfo a -> String
showsPrec :: Int -> HyInfo a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> HyInfo a -> ShowS
Show, (forall x. HyInfo a -> Rep (HyInfo a) x)
-> (forall x. Rep (HyInfo a) x -> HyInfo a) -> Generic (HyInfo a)
forall x. Rep (HyInfo a) x -> HyInfo a
forall x. HyInfo a -> Rep (HyInfo a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (HyInfo a) x -> HyInfo a
forall a x. HyInfo a -> Rep (HyInfo a) x
$cto :: forall a x. Rep (HyInfo a) x -> HyInfo a
$cfrom :: forall a x. HyInfo a -> Rep (HyInfo a) x
Generic, Eq (HyInfo a)
Eq (HyInfo a)
-> (HyInfo a -> HyInfo a -> Ordering)
-> (HyInfo a -> HyInfo a -> Bool)
-> (HyInfo a -> HyInfo a -> Bool)
-> (HyInfo a -> HyInfo a -> Bool)
-> (HyInfo a -> HyInfo a -> Bool)
-> (HyInfo a -> HyInfo a -> HyInfo a)
-> (HyInfo a -> HyInfo a -> HyInfo a)
-> Ord (HyInfo a)
HyInfo a -> HyInfo a -> Bool
HyInfo a -> HyInfo a -> Ordering
HyInfo a -> HyInfo a -> HyInfo a
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
forall a. Ord a => Eq (HyInfo a)
forall a. Ord a => HyInfo a -> HyInfo a -> Bool
forall a. Ord a => HyInfo a -> HyInfo a -> Ordering
forall a. Ord a => HyInfo a -> HyInfo a -> HyInfo a
min :: HyInfo a -> HyInfo a -> HyInfo a
$cmin :: forall a. Ord a => HyInfo a -> HyInfo a -> HyInfo a
max :: HyInfo a -> HyInfo a -> HyInfo a
$cmax :: forall a. Ord a => HyInfo a -> HyInfo a -> HyInfo a
>= :: HyInfo a -> HyInfo a -> Bool
$c>= :: forall a. Ord a => HyInfo a -> HyInfo a -> Bool
> :: HyInfo a -> HyInfo a -> Bool
$c> :: forall a. Ord a => HyInfo a -> HyInfo a -> Bool
<= :: HyInfo a -> HyInfo a -> Bool
$c<= :: forall a. Ord a => HyInfo a -> HyInfo a -> Bool
< :: HyInfo a -> HyInfo a -> Bool
$c< :: forall a. Ord a => HyInfo a -> HyInfo a -> Bool
compare :: HyInfo a -> HyInfo a -> Ordering
$ccompare :: forall a. Ord a => HyInfo a -> HyInfo a -> Ordering
$cp1Ord :: forall a. Ord a => Eq (HyInfo a)
Ord, Typeable (HyInfo a)
DataType
Constr
Typeable (HyInfo a)
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> HyInfo a -> c (HyInfo a))
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c (HyInfo a))
-> (HyInfo a -> Constr)
-> (HyInfo a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c (HyInfo a)))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c (HyInfo a)))
-> ((forall b. Data b => b -> b) -> HyInfo a -> HyInfo a)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> HyInfo a -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> HyInfo a -> r)
-> (forall u. (forall d. Data d => d -> u) -> HyInfo a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> HyInfo a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> HyInfo a -> m (HyInfo a))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> HyInfo a -> m (HyInfo a))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> HyInfo a -> m (HyInfo a))
-> Data (HyInfo a)
HyInfo a -> DataType
HyInfo a -> Constr
(forall d. Data d => c (t d)) -> Maybe (c (HyInfo a))
(forall b. Data b => b -> b) -> HyInfo a -> HyInfo a
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> HyInfo a -> c (HyInfo a)
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (HyInfo a)
forall a. Data a => Typeable (HyInfo a)
forall a. Data a => HyInfo a -> DataType
forall a. Data a => HyInfo a -> Constr
forall a.
Data a =>
(forall b. Data b => b -> b) -> HyInfo a -> HyInfo a
forall a u.
Data a =>
Int -> (forall d. Data d => d -> u) -> HyInfo a -> u
forall a u.
Data a =>
(forall d. Data d => d -> u) -> HyInfo a -> [u]
forall a r r'.
Data a =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> HyInfo a -> r
forall a r r'.
Data a =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> HyInfo a -> r
forall a (m :: * -> *).
(Data a, Monad m) =>
(forall d. Data d => d -> m d) -> HyInfo a -> m (HyInfo a)
forall a (m :: * -> *).
(Data a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> HyInfo a -> m (HyInfo a)
forall a (c :: * -> *).
Data a =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (HyInfo a)
forall a (c :: * -> *).
Data a =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> HyInfo a -> c (HyInfo a)
forall a (t :: * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (HyInfo a))
forall a (t :: * -> * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (HyInfo a))
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> HyInfo a -> u
forall u. (forall d. Data d => d -> u) -> HyInfo a -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> HyInfo a -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> HyInfo a -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> HyInfo a -> m (HyInfo a)
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> HyInfo a -> m (HyInfo a)
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (HyInfo a)
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> HyInfo a -> c (HyInfo a)
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (HyInfo a))
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (HyInfo a))
$cHyInfo :: Constr
$tHyInfo :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> HyInfo a -> m (HyInfo a)
$cgmapMo :: forall a (m :: * -> *).
(Data a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> HyInfo a -> m (HyInfo a)
gmapMp :: (forall d. Data d => d -> m d) -> HyInfo a -> m (HyInfo a)
$cgmapMp :: forall a (m :: * -> *).
(Data a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> HyInfo a -> m (HyInfo a)
gmapM :: (forall d. Data d => d -> m d) -> HyInfo a -> m (HyInfo a)
$cgmapM :: forall a (m :: * -> *).
(Data a, Monad m) =>
(forall d. Data d => d -> m d) -> HyInfo a -> m (HyInfo a)
gmapQi :: Int -> (forall d. Data d => d -> u) -> HyInfo a -> u
$cgmapQi :: forall a u.
Data a =>
Int -> (forall d. Data d => d -> u) -> HyInfo a -> u
gmapQ :: (forall d. Data d => d -> u) -> HyInfo a -> [u]
$cgmapQ :: forall a u.
Data a =>
(forall d. Data d => d -> u) -> HyInfo a -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> HyInfo a -> r
$cgmapQr :: forall a r r'.
Data a =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> HyInfo a -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> HyInfo a -> r
$cgmapQl :: forall a r r'.
Data a =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> HyInfo a -> r
gmapT :: (forall b. Data b => b -> b) -> HyInfo a -> HyInfo a
$cgmapT :: forall a.
Data a =>
(forall b. Data b => b -> b) -> HyInfo a -> HyInfo a
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (HyInfo a))
$cdataCast2 :: forall a (t :: * -> * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (HyInfo a))
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c (HyInfo a))
$cdataCast1 :: forall a (t :: * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (HyInfo a))
dataTypeOf :: HyInfo a -> DataType
$cdataTypeOf :: forall a. Data a => HyInfo a -> DataType
toConstr :: HyInfo a -> Constr
$ctoConstr :: forall a. Data a => HyInfo a -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (HyInfo a)
$cgunfold :: forall a (c :: * -> *).
Data a =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (HyInfo a)
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> HyInfo a -> c (HyInfo a)
$cgfoldl :: forall a (c :: * -> *).
Data a =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> HyInfo a -> c (HyInfo a)
$cp1Data :: forall a. Data a => Typeable (HyInfo a)
Data, Typeable)


------------------------------------------------------------------------------
-- | Map a function over the provenance.
overProvenance :: (Provenance -> Provenance) -> HyInfo a -> HyInfo a
overProvenance :: (Provenance -> Provenance) -> HyInfo a -> HyInfo a
overProvenance Provenance -> Provenance
f (HyInfo OccName
name Provenance
prv a
ty) = OccName -> Provenance -> a -> HyInfo a
forall a. OccName -> Provenance -> a -> HyInfo a
HyInfo OccName
name (Provenance -> Provenance
f Provenance
prv) a
ty


------------------------------------------------------------------------------
-- | The current bindings and goal for a hole to be filled by refinery.
data Judgement' a = Judgement
  { Judgement' a -> Hypothesis a
_jHypothesis        :: !(Hypothesis a)
  , Judgement' a -> Bool
_jBlacklistDestruct :: !Bool
  , Judgement' a -> Bool
_jWhitelistSplit    :: !Bool
  , Judgement' a -> Bool
_jIsTopHole         :: !Bool
  , Judgement' a -> a
_jGoal              :: !a
  , Judgement' a -> TCvSubst
j_coercion          :: TCvSubst
  }
  deriving stock ((forall x. Judgement' a -> Rep (Judgement' a) x)
-> (forall x. Rep (Judgement' a) x -> Judgement' a)
-> Generic (Judgement' a)
forall x. Rep (Judgement' a) x -> Judgement' a
forall x. Judgement' a -> Rep (Judgement' a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (Judgement' a) x -> Judgement' a
forall a x. Judgement' a -> Rep (Judgement' a) x
$cto :: forall a x. Rep (Judgement' a) x -> Judgement' a
$cfrom :: forall a x. Judgement' a -> Rep (Judgement' a) x
Generic, a -> Judgement' b -> Judgement' a
(a -> b) -> Judgement' a -> Judgement' b
(forall a b. (a -> b) -> Judgement' a -> Judgement' b)
-> (forall a b. a -> Judgement' b -> Judgement' a)
-> Functor Judgement'
forall a b. a -> Judgement' b -> Judgement' a
forall a b. (a -> b) -> Judgement' a -> Judgement' b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> Judgement' b -> Judgement' a
$c<$ :: forall a b. a -> Judgement' b -> Judgement' a
fmap :: (a -> b) -> Judgement' a -> Judgement' b
$cfmap :: forall a b. (a -> b) -> Judgement' a -> Judgement' b
Functor, Int -> Judgement' a -> ShowS
[Judgement' a] -> ShowS
Judgement' a -> String
(Int -> Judgement' a -> ShowS)
-> (Judgement' a -> String)
-> ([Judgement' a] -> ShowS)
-> Show (Judgement' a)
forall a. Show a => Int -> Judgement' a -> ShowS
forall a. Show a => [Judgement' a] -> ShowS
forall a. Show a => Judgement' a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Judgement' a] -> ShowS
$cshowList :: forall a. Show a => [Judgement' a] -> ShowS
show :: Judgement' a -> String
$cshow :: forall a. Show a => Judgement' a -> String
showsPrec :: Int -> Judgement' a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> Judgement' a -> ShowS
Show)

type Judgement = Judgement' CType


newtype ExtractM a = ExtractM { ExtractM a -> ReaderT Context IO a
unExtractM :: ReaderT Context IO a }
    deriving newtype (a -> ExtractM b -> ExtractM a
(a -> b) -> ExtractM a -> ExtractM b
(forall a b. (a -> b) -> ExtractM a -> ExtractM b)
-> (forall a b. a -> ExtractM b -> ExtractM a) -> Functor ExtractM
forall a b. a -> ExtractM b -> ExtractM a
forall a b. (a -> b) -> ExtractM a -> ExtractM b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> ExtractM b -> ExtractM a
$c<$ :: forall a b. a -> ExtractM b -> ExtractM a
fmap :: (a -> b) -> ExtractM a -> ExtractM b
$cfmap :: forall a b. (a -> b) -> ExtractM a -> ExtractM b
Functor, Functor ExtractM
a -> ExtractM a
Functor ExtractM
-> (forall a. a -> ExtractM a)
-> (forall a b. ExtractM (a -> b) -> ExtractM a -> ExtractM b)
-> (forall a b c.
    (a -> b -> c) -> ExtractM a -> ExtractM b -> ExtractM c)
-> (forall a b. ExtractM a -> ExtractM b -> ExtractM b)
-> (forall a b. ExtractM a -> ExtractM b -> ExtractM a)
-> Applicative ExtractM
ExtractM a -> ExtractM b -> ExtractM b
ExtractM a -> ExtractM b -> ExtractM a
ExtractM (a -> b) -> ExtractM a -> ExtractM b
(a -> b -> c) -> ExtractM a -> ExtractM b -> ExtractM c
forall a. a -> ExtractM a
forall a b. ExtractM a -> ExtractM b -> ExtractM a
forall a b. ExtractM a -> ExtractM b -> ExtractM b
forall a b. ExtractM (a -> b) -> ExtractM a -> ExtractM b
forall a b c.
(a -> b -> c) -> ExtractM a -> ExtractM b -> ExtractM c
forall (f :: * -> *).
Functor f
-> (forall a. a -> f a)
-> (forall a b. f (a -> b) -> f a -> f b)
-> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
-> (forall a b. f a -> f b -> f b)
-> (forall a b. f a -> f b -> f a)
-> Applicative f
<* :: ExtractM a -> ExtractM b -> ExtractM a
$c<* :: forall a b. ExtractM a -> ExtractM b -> ExtractM a
*> :: ExtractM a -> ExtractM b -> ExtractM b
$c*> :: forall a b. ExtractM a -> ExtractM b -> ExtractM b
liftA2 :: (a -> b -> c) -> ExtractM a -> ExtractM b -> ExtractM c
$cliftA2 :: forall a b c.
(a -> b -> c) -> ExtractM a -> ExtractM b -> ExtractM c
<*> :: ExtractM (a -> b) -> ExtractM a -> ExtractM b
$c<*> :: forall a b. ExtractM (a -> b) -> ExtractM a -> ExtractM b
pure :: a -> ExtractM a
$cpure :: forall a. a -> ExtractM a
$cp1Applicative :: Functor ExtractM
Applicative, Applicative ExtractM
a -> ExtractM a
Applicative ExtractM
-> (forall a b. ExtractM a -> (a -> ExtractM b) -> ExtractM b)
-> (forall a b. ExtractM a -> ExtractM b -> ExtractM b)
-> (forall a. a -> ExtractM a)
-> Monad ExtractM
ExtractM a -> (a -> ExtractM b) -> ExtractM b
ExtractM a -> ExtractM b -> ExtractM b
forall a. a -> ExtractM a
forall a b. ExtractM a -> ExtractM b -> ExtractM b
forall a b. ExtractM a -> (a -> ExtractM b) -> ExtractM b
forall (m :: * -> *).
Applicative m
-> (forall a b. m a -> (a -> m b) -> m b)
-> (forall a b. m a -> m b -> m b)
-> (forall a. a -> m a)
-> Monad m
return :: a -> ExtractM a
$creturn :: forall a. a -> ExtractM a
>> :: ExtractM a -> ExtractM b -> ExtractM b
$c>> :: forall a b. ExtractM a -> ExtractM b -> ExtractM b
>>= :: ExtractM a -> (a -> ExtractM b) -> ExtractM b
$c>>= :: forall a b. ExtractM a -> (a -> ExtractM b) -> ExtractM b
$cp1Monad :: Applicative ExtractM
Monad, MonadReader Context)

------------------------------------------------------------------------------
-- | Used to ensure hole names are unique across invocations of runTactic
globalHoleRef :: IORef Int
globalHoleRef :: IORef Int
globalHoleRef = IO (IORef Int) -> IORef Int
forall a. IO a -> a
unsafePerformIO (IO (IORef Int) -> IORef Int) -> IO (IORef Int) -> IORef Int
forall a b. (a -> b) -> a -> b
$ Int -> IO (IORef Int)
forall a. a -> IO (IORef a)
newIORef Int
10
{-# NOINLINE globalHoleRef #-}

instance MonadExtract Int (Synthesized (LHsExpr GhcPs)) TacticError TacticState ExtractM where
  hole :: StateT TacticState ExtractM (Int, Synthesized (LHsExpr GhcPs))
hole = do
    Int
u <- ExtractM Int -> StateT TacticState ExtractM Int
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (ExtractM Int -> StateT TacticState ExtractM Int)
-> ExtractM Int -> StateT TacticState ExtractM Int
forall a b. (a -> b) -> a -> b
$ ReaderT Context IO Int -> ExtractM Int
forall a. ReaderT Context IO a -> ExtractM a
ExtractM (ReaderT Context IO Int -> ExtractM Int)
-> ReaderT Context IO Int -> ExtractM Int
forall a b. (a -> b) -> a -> b
$ IO Int -> ReaderT Context IO Int
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO Int -> ReaderT Context IO Int)
-> IO Int -> ReaderT Context IO Int
forall a b. (a -> b) -> a -> b
$
          IORef Int -> IO Int
forall a. IORef a -> IO a
readIORef IORef Int
globalHoleRef IO Int -> IO () -> IO Int
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* IORef Int -> (Int -> Int) -> IO ()
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef' IORef Int
globalHoleRef (Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)
    (Int, Synthesized (LHsExpr GhcPs))
-> StateT TacticState ExtractM (Int, Synthesized (LHsExpr GhcPs))
forall (f :: * -> *) a. Applicative f => a -> f a
pure
      ( Int
u
      , LHsExpr GhcPs -> Synthesized (LHsExpr GhcPs)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (LHsExpr GhcPs -> Synthesized (LHsExpr GhcPs))
-> (HsExpr GhcPs -> LHsExpr GhcPs)
-> HsExpr GhcPs
-> Synthesized (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 -> Synthesized (LHsExpr GhcPs))
-> HsExpr GhcPs -> Synthesized (LHsExpr GhcPs)
forall a b. (a -> b) -> a -> b
$ RdrNameStr -> HsExpr GhcPs
forall a. Var a => RdrNameStr -> a
var (RdrNameStr -> HsExpr GhcPs) -> RdrNameStr -> HsExpr GhcPs
forall a b. (a -> b) -> a -> b
$ String -> RdrNameStr
forall a. IsString a => String -> a
fromString (String -> RdrNameStr) -> String -> RdrNameStr
forall a b. (a -> b) -> a -> b
$ OccName -> String
occNameString (OccName -> String) -> OccName -> String
forall a b. (a -> b) -> a -> b
$ RdrName -> OccName
forall name. HasOccName name => name -> OccName
occName (RdrName -> OccName) -> RdrName -> OccName
forall a b. (a -> b) -> a -> b
$ Int -> RdrName
mkMetaHoleName Int
u
      )

  unsolvableHole :: TacticError
-> StateT TacticState ExtractM (Int, Synthesized (LHsExpr GhcPs))
unsolvableHole TacticError
_ = StateT TacticState ExtractM (Int, Synthesized (LHsExpr GhcPs))
forall meta ext err s (m :: * -> *).
MonadExtract meta ext err s m =>
StateT s m (meta, ext)
hole


instance MonadReader r m => MonadReader r (TacticT jdg ext err s m) where
  ask :: TacticT jdg ext err s m r
ask = StateT jdg (ProofStateT ext ext err s m) r
-> TacticT jdg ext err s m r
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 jdg (ProofStateT ext ext err s m) r
 -> TacticT jdg ext err s m r)
-> StateT jdg (ProofStateT ext ext err s m) r
-> TacticT jdg ext err s m r
forall a b. (a -> b) -> a -> b
$ ProofStateT ext ext err s m r
-> StateT jdg (ProofStateT ext ext err s m) r
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (ProofStateT ext ext err s m r
 -> StateT jdg (ProofStateT ext ext err s m) r)
-> ProofStateT ext ext err s m r
-> StateT jdg (ProofStateT ext ext err s m) r
forall a b. (a -> b) -> a -> b
$ m (ProofStateT ext ext err s m r) -> ProofStateT ext ext err s m r
forall ext' ext err s (m :: * -> *) goal.
m (ProofStateT ext' ext err s m goal)
-> ProofStateT ext' ext err s m goal
Effect (m (ProofStateT ext ext err s m r)
 -> ProofStateT ext ext err s m r)
-> m (ProofStateT ext ext err s m r)
-> ProofStateT ext ext err s m r
forall a b. (a -> b) -> a -> b
$ (r -> ProofStateT ext ext err s m r)
-> m r -> m (ProofStateT ext ext err s m r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap r -> ProofStateT ext ext err s m r
forall (f :: * -> *) a. Applicative f => a -> f a
pure m r
forall r (m :: * -> *). MonadReader r m => m r
ask
  local :: (r -> r) -> TacticT jdg ext err s m a -> TacticT jdg ext err s m a
local r -> r
f (TacticT StateT jdg (ProofStateT ext ext err s m) a
m) = StateT jdg (ProofStateT ext ext err s m) a
-> TacticT jdg ext err s m 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 jdg (ProofStateT ext ext err s m) a
 -> TacticT jdg ext err s m a)
-> StateT jdg (ProofStateT ext ext err s m) a
-> TacticT jdg ext err s m a
forall a b. (a -> b) -> a -> b
$ (jdg -> ProofStateT ext ext err s m (a, jdg))
-> StateT jdg (ProofStateT ext ext err s m) a
forall s (m :: * -> *) a. (s -> m (a, s)) -> StateT s m a
Strict.StateT ((jdg -> ProofStateT ext ext err s m (a, jdg))
 -> StateT jdg (ProofStateT ext ext err s m) a)
-> (jdg -> ProofStateT ext ext err s m (a, jdg))
-> StateT jdg (ProofStateT ext ext err s m) a
forall a b. (a -> b) -> a -> b
$ \jdg
jdg ->
    m (ProofStateT ext ext err s m (a, jdg))
-> ProofStateT ext ext err s m (a, jdg)
forall ext' ext err s (m :: * -> *) goal.
m (ProofStateT ext' ext err s m goal)
-> ProofStateT ext' ext err s m goal
Effect (m (ProofStateT ext ext err s m (a, jdg))
 -> ProofStateT ext ext err s m (a, jdg))
-> m (ProofStateT ext ext err s m (a, jdg))
-> ProofStateT ext ext err s m (a, jdg)
forall a b. (a -> b) -> a -> b
$ (r -> r)
-> m (ProofStateT ext ext err s m (a, jdg))
-> m (ProofStateT ext ext err s m (a, jdg))
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local r -> r
f (m (ProofStateT ext ext err s m (a, jdg))
 -> m (ProofStateT ext ext err s m (a, jdg)))
-> m (ProofStateT ext ext err s m (a, jdg))
-> m (ProofStateT ext ext err s m (a, jdg))
forall a b. (a -> b) -> a -> b
$ ProofStateT ext ext err s m (a, jdg)
-> m (ProofStateT ext ext err s m (a, jdg))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ProofStateT ext ext err s m (a, jdg)
 -> m (ProofStateT ext ext err s m (a, jdg)))
-> ProofStateT ext ext err s m (a, jdg)
-> m (ProofStateT ext ext err s m (a, jdg))
forall a b. (a -> b) -> a -> b
$ StateT jdg (ProofStateT ext ext err s m) a
-> jdg -> ProofStateT ext ext err s m (a, jdg)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
Strict.runStateT StateT jdg (ProofStateT ext ext err s m) a
m jdg
jdg

instance MonadReader r m => MonadReader r (RuleT jdg ext err s m) where
  ask :: RuleT jdg ext err s m r
ask = ProofStateT ext r err s m jdg -> RuleT jdg ext err s m r
forall jdg ext err s (m :: * -> *) a.
ProofStateT ext a err s m jdg -> RuleT jdg ext err s m a
RuleT (ProofStateT ext r err s m jdg -> RuleT jdg ext err s m r)
-> ProofStateT ext r err s m jdg -> RuleT jdg ext err s m r
forall a b. (a -> b) -> a -> b
$ m (ProofStateT ext r err s m jdg) -> ProofStateT ext r err s m jdg
forall ext' ext err s (m :: * -> *) goal.
m (ProofStateT ext' ext err s m goal)
-> ProofStateT ext' ext err s m goal
Effect (m (ProofStateT ext r err s m jdg)
 -> ProofStateT ext r err s m jdg)
-> m (ProofStateT ext r err s m jdg)
-> ProofStateT ext r err s m jdg
forall a b. (a -> b) -> a -> b
$ (r -> ProofStateT ext r err s m jdg)
-> m r -> m (ProofStateT ext r err s m jdg)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap r -> ProofStateT ext r err s m jdg
forall ext' ext err s (m :: * -> *) goal.
ext -> ProofStateT ext' ext err s m goal
Axiom m r
forall r (m :: * -> *). MonadReader r m => m r
ask
  local :: (r -> r) -> RuleT jdg ext err s m a -> RuleT jdg ext err s m a
local r -> r
f (RuleT ProofStateT ext a err s m jdg
m) = ProofStateT ext a err s m jdg -> RuleT jdg ext err s m a
forall jdg ext err s (m :: * -> *) a.
ProofStateT ext a err s m jdg -> RuleT jdg ext err s m a
RuleT (ProofStateT ext a err s m jdg -> RuleT jdg ext err s m a)
-> ProofStateT ext a err s m jdg -> RuleT jdg ext err s m a
forall a b. (a -> b) -> a -> b
$ m (ProofStateT ext a err s m jdg) -> ProofStateT ext a err s m jdg
forall ext' ext err s (m :: * -> *) goal.
m (ProofStateT ext' ext err s m goal)
-> ProofStateT ext' ext err s m goal
Effect (m (ProofStateT ext a err s m jdg)
 -> ProofStateT ext a err s m jdg)
-> m (ProofStateT ext a err s m jdg)
-> ProofStateT ext a err s m jdg
forall a b. (a -> b) -> a -> b
$ (r -> r)
-> m (ProofStateT ext a err s m jdg)
-> m (ProofStateT ext a err s m jdg)
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local r -> r
f (m (ProofStateT ext a err s m jdg)
 -> m (ProofStateT ext a err s m jdg))
-> m (ProofStateT ext a err s m jdg)
-> m (ProofStateT ext a err s m jdg)
forall a b. (a -> b) -> a -> b
$ ProofStateT ext a err s m jdg -> m (ProofStateT ext a err s m jdg)
forall (f :: * -> *) a. Applicative f => a -> f a
pure ProofStateT ext a err s m jdg
m

mkMetaHoleName :: Int -> RdrName
mkMetaHoleName :: Int -> RdrName
mkMetaHoleName Int
u = OccName -> RdrName
mkRdrUnqual (OccName -> RdrName) -> OccName -> RdrName
forall a b. (a -> b) -> a -> b
$ String -> OccName
mkVarOcc (String -> OccName) -> String -> OccName
forall a b. (a -> b) -> a -> b
$ String
"_" String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Unique -> String
forall a. Show a => a -> String
show (Char -> Int -> Unique
mkUnique Char
'w' Int
u)

instance MetaSubst Int (Synthesized (LHsExpr GhcPs)) where
  -- TODO(sandy): This join is to combine the synthesizeds
  substMeta :: Int
-> Synthesized (LHsExpr GhcPs)
-> Synthesized (LHsExpr GhcPs)
-> Synthesized (LHsExpr GhcPs)
substMeta Int
u Synthesized (LHsExpr GhcPs)
val Synthesized (LHsExpr GhcPs)
a =  Synthesized (Synthesized (LHsExpr GhcPs))
-> Synthesized (LHsExpr GhcPs)
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join (Synthesized (Synthesized (LHsExpr GhcPs))
 -> Synthesized (LHsExpr GhcPs))
-> Synthesized (Synthesized (LHsExpr GhcPs))
-> Synthesized (LHsExpr GhcPs)
forall a b. (a -> b) -> a -> b
$ Synthesized (LHsExpr GhcPs)
a Synthesized (LHsExpr GhcPs)
-> (LHsExpr GhcPs -> Synthesized (LHsExpr GhcPs))
-> Synthesized (Synthesized (LHsExpr GhcPs))
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&>
    GenericM Synthesized -> GenericM Synthesized
forall (m :: * -> *). Monad m => GenericM m -> GenericM m
everywhereM ((LHsExpr GhcPs -> Synthesized (LHsExpr GhcPs))
-> a -> Synthesized a
forall (m :: * -> *) a b.
(Monad m, Typeable a, Typeable b) =>
(b -> m b) -> a -> m a
mkM ((LHsExpr GhcPs -> Synthesized (LHsExpr GhcPs))
 -> a -> Synthesized a)
-> (LHsExpr GhcPs -> Synthesized (LHsExpr GhcPs))
-> a
-> Synthesized a
forall a b. (a -> b) -> a -> b
$ \case
      (L SrcSpan
_ (HsVar XVar GhcPs
_ (L SrcSpan
_ IdP GhcPs
name)))
        | IdP GhcPs
RdrName
name RdrName -> RdrName -> Bool
forall a. Eq a => a -> a -> Bool
== Int -> RdrName
mkMetaHoleName Int
u -> Synthesized (LHsExpr GhcPs)
val
      (LHsExpr GhcPs
t :: LHsExpr GhcPs) -> LHsExpr GhcPs -> Synthesized (LHsExpr GhcPs)
forall (f :: * -> *) a. Applicative f => a -> f a
pure LHsExpr GhcPs
t)


------------------------------------------------------------------------------
-- | Reasons a tactic might fail.
data TacticError
  = OutOfGas
  | GoalMismatch String CType
  | NoProgress
  | NoApplicableTactic
  | UnhelpfulRecursion
  | UnhelpfulDestruct OccName
  | TooPolymorphic
  | NotInScope OccName
  | TacticPanic String
  deriving (TacticError -> TacticError -> Bool
(TacticError -> TacticError -> Bool)
-> (TacticError -> TacticError -> Bool) -> Eq TacticError
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: TacticError -> TacticError -> Bool
$c/= :: TacticError -> TacticError -> Bool
== :: TacticError -> TacticError -> Bool
$c== :: TacticError -> TacticError -> Bool
Eq)

instance Show TacticError where
    show :: TacticError -> String
show TacticError
OutOfGas = String
"Auto ran out of gas"
    show (GoalMismatch String
tac (CType Type
typ)) =
      [String] -> String
forall a. Monoid a => [a] -> a
mconcat
        [ String
"The tactic "
        , String
tac
        , String
" doesn't apply to goal type "
        , Type -> String
forall a. Outputable a => a -> String
unsafeRender Type
typ
        ]
    show TacticError
NoProgress =
      String
"Unable to make progress"
    show TacticError
NoApplicableTactic =
      String
"No tactic could be applied"
    show TacticError
UnhelpfulRecursion =
      String
"Recursion wasn't productive"
    show (UnhelpfulDestruct OccName
n) =
      String
"Destructing patval " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> OccName -> String
forall a. Show a => a -> String
show OccName
n String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" leads to no new types"
    show TacticError
TooPolymorphic =
      String
"The tactic isn't applicable because the goal is too polymorphic"
    show (NotInScope OccName
name) =
      String
"Tried to do something with the out of scope name " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> OccName -> String
forall a. Show a => a -> String
show OccName
name
    show (TacticPanic String
err) =
      String
"Tactic panic: " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
err


------------------------------------------------------------------------------
type TacticsM  = TacticT Judgement (Synthesized (LHsExpr GhcPs)) TacticError TacticState ExtractM
type RuleM     = RuleT Judgement (Synthesized (LHsExpr GhcPs)) TacticError TacticState ExtractM
type Rule      = RuleM (Synthesized (LHsExpr GhcPs))

type Trace = Rose String

------------------------------------------------------------------------------
-- | The extract for refinery. Represents a "synthesized attribute" in the
-- context of attribute grammars. In essence, 'Synthesized' describes
-- information we'd like to pass from leaves of the tactics search upwards.
-- This includes the actual AST we've generated (in 'syn_val').
data Synthesized a = Synthesized
  { Synthesized a -> Trace
syn_trace  :: Trace
    -- ^ A tree describing which tactics were used produce the 'syn_val'.
    -- Mainly for debugging when you get the wrong answer, to see the other
    -- things it tried.
  , Synthesized a -> Hypothesis CType
syn_scoped :: Hypothesis CType
    -- ^ All of the bindings created to produce the 'syn_val'.
  , Synthesized a -> Set OccName
syn_used_vals :: Set OccName
    -- ^ The values used when synthesizing the 'syn_val'.
  , Synthesized a -> Sum Int
syn_recursion_count :: Sum Int
    -- ^ The number of recursive calls
  , Synthesized a -> a
syn_val    :: a
  }
  deriving stock (Synthesized a -> Synthesized a -> Bool
(Synthesized a -> Synthesized a -> Bool)
-> (Synthesized a -> Synthesized a -> Bool) -> Eq (Synthesized a)
forall a. Eq a => Synthesized a -> Synthesized a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Synthesized a -> Synthesized a -> Bool
$c/= :: forall a. Eq a => Synthesized a -> Synthesized a -> Bool
== :: Synthesized a -> Synthesized a -> Bool
$c== :: forall a. Eq a => Synthesized a -> Synthesized a -> Bool
Eq, Int -> Synthesized a -> ShowS
[Synthesized a] -> ShowS
Synthesized a -> String
(Int -> Synthesized a -> ShowS)
-> (Synthesized a -> String)
-> ([Synthesized a] -> ShowS)
-> Show (Synthesized a)
forall a. Show a => Int -> Synthesized a -> ShowS
forall a. Show a => [Synthesized a] -> ShowS
forall a. Show a => Synthesized a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Synthesized a] -> ShowS
$cshowList :: forall a. Show a => [Synthesized a] -> ShowS
show :: Synthesized a -> String
$cshow :: forall a. Show a => Synthesized a -> String
showsPrec :: Int -> Synthesized a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> Synthesized a -> ShowS
Show, a -> Synthesized b -> Synthesized a
(a -> b) -> Synthesized a -> Synthesized b
(forall a b. (a -> b) -> Synthesized a -> Synthesized b)
-> (forall a b. a -> Synthesized b -> Synthesized a)
-> Functor Synthesized
forall a b. a -> Synthesized b -> Synthesized a
forall a b. (a -> b) -> Synthesized a -> Synthesized b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> Synthesized b -> Synthesized a
$c<$ :: forall a b. a -> Synthesized b -> Synthesized a
fmap :: (a -> b) -> Synthesized a -> Synthesized b
$cfmap :: forall a b. (a -> b) -> Synthesized a -> Synthesized b
Functor, Synthesized a -> Bool
(a -> m) -> Synthesized a -> m
(a -> b -> b) -> b -> Synthesized a -> b
(forall m. Monoid m => Synthesized m -> m)
-> (forall m a. Monoid m => (a -> m) -> Synthesized a -> m)
-> (forall m a. Monoid m => (a -> m) -> Synthesized a -> m)
-> (forall a b. (a -> b -> b) -> b -> Synthesized a -> b)
-> (forall a b. (a -> b -> b) -> b -> Synthesized a -> b)
-> (forall b a. (b -> a -> b) -> b -> Synthesized a -> b)
-> (forall b a. (b -> a -> b) -> b -> Synthesized a -> b)
-> (forall a. (a -> a -> a) -> Synthesized a -> a)
-> (forall a. (a -> a -> a) -> Synthesized a -> a)
-> (forall a. Synthesized a -> [a])
-> (forall a. Synthesized a -> Bool)
-> (forall a. Synthesized a -> Int)
-> (forall a. Eq a => a -> Synthesized a -> Bool)
-> (forall a. Ord a => Synthesized a -> a)
-> (forall a. Ord a => Synthesized a -> a)
-> (forall a. Num a => Synthesized a -> a)
-> (forall a. Num a => Synthesized a -> a)
-> Foldable Synthesized
forall a. Eq a => a -> Synthesized a -> Bool
forall a. Num a => Synthesized a -> a
forall a. Ord a => Synthesized a -> a
forall m. Monoid m => Synthesized m -> m
forall a. Synthesized a -> Bool
forall a. Synthesized a -> Int
forall a. Synthesized a -> [a]
forall a. (a -> a -> a) -> Synthesized a -> a
forall m a. Monoid m => (a -> m) -> Synthesized a -> m
forall b a. (b -> a -> b) -> b -> Synthesized a -> b
forall a b. (a -> b -> b) -> b -> Synthesized a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
product :: Synthesized a -> a
$cproduct :: forall a. Num a => Synthesized a -> a
sum :: Synthesized a -> a
$csum :: forall a. Num a => Synthesized a -> a
minimum :: Synthesized a -> a
$cminimum :: forall a. Ord a => Synthesized a -> a
maximum :: Synthesized a -> a
$cmaximum :: forall a. Ord a => Synthesized a -> a
elem :: a -> Synthesized a -> Bool
$celem :: forall a. Eq a => a -> Synthesized a -> Bool
length :: Synthesized a -> Int
$clength :: forall a. Synthesized a -> Int
null :: Synthesized a -> Bool
$cnull :: forall a. Synthesized a -> Bool
toList :: Synthesized a -> [a]
$ctoList :: forall a. Synthesized a -> [a]
foldl1 :: (a -> a -> a) -> Synthesized a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> Synthesized a -> a
foldr1 :: (a -> a -> a) -> Synthesized a -> a
$cfoldr1 :: forall a. (a -> a -> a) -> Synthesized a -> a
foldl' :: (b -> a -> b) -> b -> Synthesized a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> Synthesized a -> b
foldl :: (b -> a -> b) -> b -> Synthesized a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> Synthesized a -> b
foldr' :: (a -> b -> b) -> b -> Synthesized a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> Synthesized a -> b
foldr :: (a -> b -> b) -> b -> Synthesized a -> b
$cfoldr :: forall a b. (a -> b -> b) -> b -> Synthesized a -> b
foldMap' :: (a -> m) -> Synthesized a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> Synthesized a -> m
foldMap :: (a -> m) -> Synthesized a -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> Synthesized a -> m
fold :: Synthesized m -> m
$cfold :: forall m. Monoid m => Synthesized m -> m
Foldable, Functor Synthesized
Foldable Synthesized
Functor Synthesized
-> Foldable Synthesized
-> (forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Synthesized a -> f (Synthesized b))
-> (forall (f :: * -> *) a.
    Applicative f =>
    Synthesized (f a) -> f (Synthesized a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> Synthesized a -> m (Synthesized b))
-> (forall (m :: * -> *) a.
    Monad m =>
    Synthesized (m a) -> m (Synthesized a))
-> Traversable Synthesized
(a -> f b) -> Synthesized a -> f (Synthesized b)
forall (t :: * -> *).
Functor t
-> Foldable t
-> (forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: * -> *) a.
Monad m =>
Synthesized (m a) -> m (Synthesized a)
forall (f :: * -> *) a.
Applicative f =>
Synthesized (f a) -> f (Synthesized a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Synthesized a -> m (Synthesized b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Synthesized a -> f (Synthesized b)
sequence :: Synthesized (m a) -> m (Synthesized a)
$csequence :: forall (m :: * -> *) a.
Monad m =>
Synthesized (m a) -> m (Synthesized a)
mapM :: (a -> m b) -> Synthesized a -> m (Synthesized b)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Synthesized a -> m (Synthesized b)
sequenceA :: Synthesized (f a) -> f (Synthesized a)
$csequenceA :: forall (f :: * -> *) a.
Applicative f =>
Synthesized (f a) -> f (Synthesized a)
traverse :: (a -> f b) -> Synthesized a -> f (Synthesized b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Synthesized a -> f (Synthesized b)
$cp2Traversable :: Foldable Synthesized
$cp1Traversable :: Functor Synthesized
Traversable, (forall x. Synthesized a -> Rep (Synthesized a) x)
-> (forall x. Rep (Synthesized a) x -> Synthesized a)
-> Generic (Synthesized a)
forall x. Rep (Synthesized a) x -> Synthesized a
forall x. Synthesized a -> Rep (Synthesized a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (Synthesized a) x -> Synthesized a
forall a x. Synthesized a -> Rep (Synthesized a) x
$cto :: forall a x. Rep (Synthesized a) x -> Synthesized a
$cfrom :: forall a x. Synthesized a -> Rep (Synthesized a) x
Generic, Typeable (Synthesized a)
DataType
Constr
Typeable (Synthesized a)
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Synthesized a -> c (Synthesized a))
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c (Synthesized a))
-> (Synthesized a -> Constr)
-> (Synthesized a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c (Synthesized a)))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c (Synthesized a)))
-> ((forall b. Data b => b -> b) -> Synthesized a -> Synthesized a)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> Synthesized a -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> Synthesized a -> r)
-> (forall u. (forall d. Data d => d -> u) -> Synthesized a -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> Synthesized a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d)
    -> Synthesized a -> m (Synthesized a))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> Synthesized a -> m (Synthesized a))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> Synthesized a -> m (Synthesized a))
-> Data (Synthesized a)
Synthesized a -> DataType
Synthesized a -> Constr
(forall d. Data d => c (t d)) -> Maybe (c (Synthesized a))
(forall b. Data b => b -> b) -> Synthesized a -> Synthesized a
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Synthesized a -> c (Synthesized a)
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Synthesized a)
forall a. Data a => Typeable (Synthesized a)
forall a. Data a => Synthesized a -> DataType
forall a. Data a => Synthesized a -> Constr
forall a.
Data a =>
(forall b. Data b => b -> b) -> Synthesized a -> Synthesized a
forall a u.
Data a =>
Int -> (forall d. Data d => d -> u) -> Synthesized a -> u
forall a u.
Data a =>
(forall d. Data d => d -> u) -> Synthesized a -> [u]
forall a r r'.
Data a =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Synthesized a -> r
forall a r r'.
Data a =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Synthesized a -> r
forall a (m :: * -> *).
(Data a, Monad m) =>
(forall d. Data d => d -> m d)
-> Synthesized a -> m (Synthesized a)
forall a (m :: * -> *).
(Data a, MonadPlus m) =>
(forall d. Data d => d -> m d)
-> Synthesized a -> m (Synthesized a)
forall a (c :: * -> *).
Data a =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Synthesized a)
forall a (c :: * -> *).
Data a =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Synthesized a -> c (Synthesized a)
forall a (t :: * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Synthesized a))
forall a (t :: * -> * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (Synthesized a))
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> Synthesized a -> u
forall u. (forall d. Data d => d -> u) -> Synthesized a -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Synthesized a -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Synthesized a -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> Synthesized a -> m (Synthesized a)
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> Synthesized a -> m (Synthesized a)
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Synthesized a)
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Synthesized a -> c (Synthesized a)
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (Synthesized a))
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (Synthesized a))
$cSynthesized :: Constr
$tSynthesized :: DataType
gmapMo :: (forall d. Data d => d -> m d)
-> Synthesized a -> m (Synthesized a)
$cgmapMo :: forall a (m :: * -> *).
(Data a, MonadPlus m) =>
(forall d. Data d => d -> m d)
-> Synthesized a -> m (Synthesized a)
gmapMp :: (forall d. Data d => d -> m d)
-> Synthesized a -> m (Synthesized a)
$cgmapMp :: forall a (m :: * -> *).
(Data a, MonadPlus m) =>
(forall d. Data d => d -> m d)
-> Synthesized a -> m (Synthesized a)
gmapM :: (forall d. Data d => d -> m d)
-> Synthesized a -> m (Synthesized a)
$cgmapM :: forall a (m :: * -> *).
(Data a, Monad m) =>
(forall d. Data d => d -> m d)
-> Synthesized a -> m (Synthesized a)
gmapQi :: Int -> (forall d. Data d => d -> u) -> Synthesized a -> u
$cgmapQi :: forall a u.
Data a =>
Int -> (forall d. Data d => d -> u) -> Synthesized a -> u
gmapQ :: (forall d. Data d => d -> u) -> Synthesized a -> [u]
$cgmapQ :: forall a u.
Data a =>
(forall d. Data d => d -> u) -> Synthesized a -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Synthesized a -> r
$cgmapQr :: forall a r r'.
Data a =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Synthesized a -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Synthesized a -> r
$cgmapQl :: forall a r r'.
Data a =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Synthesized a -> r
gmapT :: (forall b. Data b => b -> b) -> Synthesized a -> Synthesized a
$cgmapT :: forall a.
Data a =>
(forall b. Data b => b -> b) -> Synthesized a -> Synthesized a
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (Synthesized a))
$cdataCast2 :: forall a (t :: * -> * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (Synthesized a))
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c (Synthesized a))
$cdataCast1 :: forall a (t :: * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Synthesized a))
dataTypeOf :: Synthesized a -> DataType
$cdataTypeOf :: forall a. Data a => Synthesized a -> DataType
toConstr :: Synthesized a -> Constr
$ctoConstr :: forall a. Data a => Synthesized a -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Synthesized a)
$cgunfold :: forall a (c :: * -> *).
Data a =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Synthesized a)
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Synthesized a -> c (Synthesized a)
$cgfoldl :: forall a (c :: * -> *).
Data a =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Synthesized a -> c (Synthesized a)
$cp1Data :: forall a. Data a => Typeable (Synthesized a)
Data, Typeable)

instance Monad Synthesized where
  return :: a -> Synthesized a
return = a -> Synthesized a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
  Synthesized Trace
tr1 Hypothesis CType
sc1 Set OccName
uv1 Sum Int
rc1 a
a >>= :: Synthesized a -> (a -> Synthesized b) -> Synthesized b
>>= a -> Synthesized b
f =
    case a -> Synthesized b
f a
a of
      Synthesized Trace
tr2 Hypothesis CType
sc2 Set OccName
uv2 Sum Int
rc2 b
b ->
        Synthesized :: forall a.
Trace
-> Hypothesis CType -> Set OccName -> Sum Int -> a -> Synthesized a
Synthesized
          { syn_trace :: Trace
syn_trace = Trace
tr1 Trace -> Trace -> Trace
forall a. Semigroup a => a -> a -> a
<> Trace
tr2
          , syn_scoped :: Hypothesis CType
syn_scoped = Hypothesis CType
sc1 Hypothesis CType -> Hypothesis CType -> Hypothesis CType
forall a. Semigroup a => a -> a -> a
<> Hypothesis CType
sc2
          , syn_used_vals :: Set OccName
syn_used_vals = Set OccName
uv1 Set OccName -> Set OccName -> Set OccName
forall a. Semigroup a => a -> a -> a
<> Set OccName
uv2
          , syn_recursion_count :: Sum Int
syn_recursion_count = Sum Int
rc1 Sum Int -> Sum Int -> Sum Int
forall a. Semigroup a => a -> a -> a
<> Sum Int
rc2
          , syn_val :: b
syn_val = b
b
          }

mapTrace :: (Trace -> Trace) -> Synthesized a -> Synthesized a
mapTrace :: (Trace -> Trace) -> Synthesized a -> Synthesized a
mapTrace Trace -> Trace
f (Synthesized Trace
tr Hypothesis CType
sc Set OccName
uv Sum Int
rc a
a) = Trace
-> Hypothesis CType -> Set OccName -> Sum Int -> a -> Synthesized a
forall a.
Trace
-> Hypothesis CType -> Set OccName -> Sum Int -> a -> Synthesized a
Synthesized (Trace -> Trace
f Trace
tr) Hypothesis CType
sc Set OccName
uv Sum Int
rc a
a


------------------------------------------------------------------------------
-- | This might not be lawful, due to the semigroup on 'Trace' maybe not being
-- lawful. But that's only for debug output, so it's not anything I'm concerned
-- about.
instance Applicative Synthesized where
  pure :: a -> Synthesized a
pure = Trace
-> Hypothesis CType -> Set OccName -> Sum Int -> a -> Synthesized a
forall a.
Trace
-> Hypothesis CType -> Set OccName -> Sum Int -> a -> Synthesized a
Synthesized Trace
forall a. Monoid a => a
mempty Hypothesis CType
forall a. Monoid a => a
mempty Set OccName
forall a. Monoid a => a
mempty Sum Int
forall a. Monoid a => a
mempty
  Synthesized Trace
tr1 Hypothesis CType
sc1 Set OccName
uv1 Sum Int
rc1 a -> b
f <*> :: Synthesized (a -> b) -> Synthesized a -> Synthesized b
<*> Synthesized Trace
tr2 Hypothesis CType
sc2 Set OccName
uv2 Sum Int
rc2 a
a =
    Trace
-> Hypothesis CType -> Set OccName -> Sum Int -> b -> Synthesized b
forall a.
Trace
-> Hypothesis CType -> Set OccName -> Sum Int -> a -> Synthesized a
Synthesized (Trace
tr1 Trace -> Trace -> Trace
forall a. Semigroup a => a -> a -> a
<> Trace
tr2) (Hypothesis CType
sc1 Hypothesis CType -> Hypothesis CType -> Hypothesis CType
forall a. Semigroup a => a -> a -> a
<> Hypothesis CType
sc2) (Set OccName
uv1 Set OccName -> Set OccName -> Set OccName
forall a. Semigroup a => a -> a -> a
<> Set OccName
uv2) (Sum Int
rc1 Sum Int -> Sum Int -> Sum Int
forall a. Semigroup a => a -> a -> a
<> Sum Int
rc2) (b -> Synthesized b) -> b -> Synthesized b
forall a b. (a -> b) -> a -> b
$ a -> b
f a
a


------------------------------------------------------------------------------
-- | The Reader context of tactics and rules
data Context = Context
  { Context -> [(OccName, CType)]
ctxDefiningFuncs :: [(OccName, CType)]
    -- ^ The functions currently being defined
  , Context -> [(OccName, CType)]
ctxModuleFuncs   :: [(OccName, CType)]
    -- ^ Everything defined in the current module
  , Context -> Config
ctxConfig        :: Config
  , Context -> InstEnvs
ctxInstEnvs      :: InstEnvs
  , Context -> FamInstEnvs
ctxFamInstEnvs   :: FamInstEnvs
  , Context -> Set CType
ctxTheta         :: Set CType
  , Context -> HscEnv
ctx_hscEnv       :: HscEnv
  , Context -> OccEnv [GlobalRdrElt]
ctx_occEnv       :: OccEnv [GlobalRdrElt]
  , Context -> Module
ctx_module       :: Module
  }

instance Show Context where
  show :: Context -> String
show (Context {[(OccName, CType)]
FamInstEnvs
Set CType
HscEnv
InstEnvs
OccEnv [GlobalRdrElt]
Module
Config
ctx_module :: Module
ctx_occEnv :: OccEnv [GlobalRdrElt]
ctx_hscEnv :: HscEnv
ctxTheta :: Set CType
ctxFamInstEnvs :: FamInstEnvs
ctxInstEnvs :: InstEnvs
ctxConfig :: Config
ctxModuleFuncs :: [(OccName, CType)]
ctxDefiningFuncs :: [(OccName, CType)]
ctx_module :: Context -> Module
ctx_occEnv :: Context -> OccEnv [GlobalRdrElt]
ctx_hscEnv :: Context -> HscEnv
ctxTheta :: Context -> Set CType
ctxFamInstEnvs :: Context -> FamInstEnvs
ctxInstEnvs :: Context -> InstEnvs
ctxConfig :: Context -> Config
ctxModuleFuncs :: Context -> [(OccName, CType)]
ctxDefiningFuncs :: Context -> [(OccName, CType)]
..}) = [String] -> String
forall a. Monoid a => [a] -> a
mconcat
    [ String
"Context "
    , Int -> [(OccName, CType)] -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
10 [(OccName, CType)]
ctxDefiningFuncs String
""
    , Int -> [(OccName, CType)] -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
10 [(OccName, CType)]
ctxModuleFuncs String
""
    , Int -> Config -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
10 Config
ctxConfig String
""
    , Int -> Set CType -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
10 Set CType
ctxTheta String
""
    ]


------------------------------------------------------------------------------
-- | An empty context
emptyContext :: Context
emptyContext :: Context
emptyContext
  = Context :: [(OccName, CType)]
-> [(OccName, CType)]
-> Config
-> InstEnvs
-> FamInstEnvs
-> Set CType
-> HscEnv
-> OccEnv [GlobalRdrElt]
-> Module
-> Context
Context
      { ctxDefiningFuncs :: [(OccName, CType)]
ctxDefiningFuncs = [(OccName, CType)]
forall a. Monoid a => a
mempty
      , ctxModuleFuncs :: [(OccName, CType)]
ctxModuleFuncs = [(OccName, CType)]
forall a. Monoid a => a
mempty
      , ctxConfig :: Config
ctxConfig = Config
emptyConfig
      , ctxFamInstEnvs :: FamInstEnvs
ctxFamInstEnvs = FamInstEnvs
forall a. Monoid a => a
mempty
      , ctxInstEnvs :: InstEnvs
ctxInstEnvs = InstEnv -> InstEnv -> VisibleOrphanModules -> InstEnvs
InstEnvs InstEnv
forall a. Monoid a => a
mempty InstEnv
forall a. Monoid a => a
mempty VisibleOrphanModules
forall a. Monoid a => a
mempty
      , ctxTheta :: Set CType
ctxTheta = Set CType
forall a. Monoid a => a
mempty
      , ctx_hscEnv :: HscEnv
ctx_hscEnv = String -> HscEnv
forall a. HasCallStack => String -> a
error String
"empty hsc env from emptyContext"
      , ctx_occEnv :: OccEnv [GlobalRdrElt]
ctx_occEnv = OccEnv [GlobalRdrElt]
forall a. OccEnv a
emptyOccEnv
      , ctx_module :: Module
ctx_module = String -> Module
forall a. HasCallStack => String -> a
error String
"empty module from emptyContext"
      }


newtype Rose a = Rose (Tree a)
  deriving stock (Rose a -> Rose a -> Bool
(Rose a -> Rose a -> Bool)
-> (Rose a -> Rose a -> Bool) -> Eq (Rose a)
forall a. Eq a => Rose a -> Rose a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Rose a -> Rose a -> Bool
$c/= :: forall a. Eq a => Rose a -> Rose a -> Bool
== :: Rose a -> Rose a -> Bool
$c== :: forall a. Eq a => Rose a -> Rose a -> Bool
Eq, a -> Rose b -> Rose a
(a -> b) -> Rose a -> Rose b
(forall a b. (a -> b) -> Rose a -> Rose b)
-> (forall a b. a -> Rose b -> Rose a) -> Functor Rose
forall a b. a -> Rose b -> Rose a
forall a b. (a -> b) -> Rose a -> Rose b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> Rose b -> Rose a
$c<$ :: forall a b. a -> Rose b -> Rose a
fmap :: (a -> b) -> Rose a -> Rose b
$cfmap :: forall a b. (a -> b) -> Rose a -> Rose b
Functor, (forall x. Rose a -> Rep (Rose a) x)
-> (forall x. Rep (Rose a) x -> Rose a) -> Generic (Rose a)
forall x. Rep (Rose a) x -> Rose a
forall x. Rose a -> Rep (Rose a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (Rose a) x -> Rose a
forall a x. Rose a -> Rep (Rose a) x
$cto :: forall a x. Rep (Rose a) x -> Rose a
$cfrom :: forall a x. Rose a -> Rep (Rose a) x
Generic, Typeable (Rose a)
DataType
Constr
Typeable (Rose a)
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Rose a -> c (Rose a))
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c (Rose a))
-> (Rose a -> Constr)
-> (Rose a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c (Rose a)))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Rose a)))
-> ((forall b. Data b => b -> b) -> Rose a -> Rose a)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> Rose a -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> Rose a -> r)
-> (forall u. (forall d. Data d => d -> u) -> Rose a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> Rose a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Rose a -> m (Rose a))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Rose a -> m (Rose a))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Rose a -> m (Rose a))
-> Data (Rose a)
Rose a -> DataType
Rose a -> Constr
(forall d. Data d => c (t d)) -> Maybe (c (Rose a))
(forall b. Data b => b -> b) -> Rose a -> Rose a
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Rose a -> c (Rose a)
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Rose a)
forall a. Data a => Typeable (Rose a)
forall a. Data a => Rose a -> DataType
forall a. Data a => Rose a -> Constr
forall a.
Data a =>
(forall b. Data b => b -> b) -> Rose a -> Rose a
forall a u.
Data a =>
Int -> (forall d. Data d => d -> u) -> Rose a -> u
forall a u. Data a => (forall d. Data d => d -> u) -> Rose a -> [u]
forall a r r'.
Data a =>
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Rose a -> r
forall a r r'.
Data a =>
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Rose a -> r
forall a (m :: * -> *).
(Data a, Monad m) =>
(forall d. Data d => d -> m d) -> Rose a -> m (Rose a)
forall a (m :: * -> *).
(Data a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Rose a -> m (Rose a)
forall a (c :: * -> *).
Data a =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Rose a)
forall a (c :: * -> *).
Data a =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Rose a -> c (Rose a)
forall a (t :: * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Rose a))
forall a (t :: * -> * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Rose a))
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> Rose a -> u
forall u. (forall d. Data d => d -> u) -> Rose a -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Rose a -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Rose a -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Rose a -> m (Rose a)
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Rose a -> m (Rose a)
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Rose a)
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Rose a -> c (Rose a)
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (Rose a))
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Rose a))
$cRose :: Constr
$tRose :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> Rose a -> m (Rose a)
$cgmapMo :: forall a (m :: * -> *).
(Data a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Rose a -> m (Rose a)
gmapMp :: (forall d. Data d => d -> m d) -> Rose a -> m (Rose a)
$cgmapMp :: forall a (m :: * -> *).
(Data a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Rose a -> m (Rose a)
gmapM :: (forall d. Data d => d -> m d) -> Rose a -> m (Rose a)
$cgmapM :: forall a (m :: * -> *).
(Data a, Monad m) =>
(forall d. Data d => d -> m d) -> Rose a -> m (Rose a)
gmapQi :: Int -> (forall d. Data d => d -> u) -> Rose a -> u
$cgmapQi :: forall a u.
Data a =>
Int -> (forall d. Data d => d -> u) -> Rose a -> u
gmapQ :: (forall d. Data d => d -> u) -> Rose a -> [u]
$cgmapQ :: forall a u. Data a => (forall d. Data d => d -> u) -> Rose a -> [u]
gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Rose a -> r
$cgmapQr :: forall a r r'.
Data a =>
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Rose a -> r
gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Rose a -> r
$cgmapQl :: forall a r r'.
Data a =>
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Rose a -> r
gmapT :: (forall b. Data b => b -> b) -> Rose a -> Rose a
$cgmapT :: forall a.
Data a =>
(forall b. Data b => b -> b) -> Rose a -> Rose a
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Rose a))
$cdataCast2 :: forall a (t :: * -> * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Rose a))
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c (Rose a))
$cdataCast1 :: forall a (t :: * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Rose a))
dataTypeOf :: Rose a -> DataType
$cdataTypeOf :: forall a. Data a => Rose a -> DataType
toConstr :: Rose a -> Constr
$ctoConstr :: forall a. Data a => Rose a -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Rose a)
$cgunfold :: forall a (c :: * -> *).
Data a =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Rose a)
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Rose a -> c (Rose a)
$cgfoldl :: forall a (c :: * -> *).
Data a =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Rose a -> c (Rose a)
$cp1Data :: forall a. Data a => Typeable (Rose a)
Data, Typeable)

instance Show (Rose String) where
  show :: Trace -> String
show = [String] -> String
unlines ([String] -> String) -> (Trace -> [String]) -> Trace -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [String] -> [String]
forall a. [a] -> [a]
dropEveryOther ([String] -> [String]) -> (Trace -> [String]) -> Trace -> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> [String]
lines (String -> [String]) -> (Trace -> String) -> Trace -> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Tree String -> String
drawTree (Tree String -> String)
-> (Trace -> Tree String) -> Trace -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Trace -> Tree String
coerce

dropEveryOther :: [a] -> [a]
dropEveryOther :: [a] -> [a]
dropEveryOther []           = []
dropEveryOther [a
a]          = [a
a]
dropEveryOther (a
a : a
_ : [a]
as) = a
a a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a] -> [a]
forall a. [a] -> [a]
dropEveryOther [a]
as

------------------------------------------------------------------------------
-- | This might not be lawful! I didn't check, and it feels sketchy.
instance (Eq a, Monoid a) => Semigroup (Rose a) where
  Rose (Node a
a Forest a
as) <> :: Rose a -> Rose a -> Rose a
<> Rose (Node a
b Forest a
bs) = Tree a -> Rose a
forall a. Tree a -> Rose a
Rose (Tree a -> Rose a) -> Tree a -> Rose a
forall a b. (a -> b) -> a -> b
$ a -> Forest a -> Tree a
forall a. a -> Forest a -> Tree a
Node (a
a a -> a -> a
forall a. Semigroup a => a -> a -> a
<> a
b) (Forest a
as Forest a -> Forest a -> Forest a
forall a. Semigroup a => a -> a -> a
<> Forest a
bs)
  sconcat :: NonEmpty (Rose a) -> Rose a
sconcat (Rose a
a :| [Rose a]
as) = a -> [Rose a] -> Rose a
forall a. (Eq a, Monoid a) => a -> [Rose a] -> Rose a
rose a
forall a. Monoid a => a
mempty ([Rose a] -> Rose a) -> [Rose a] -> Rose a
forall a b. (a -> b) -> a -> b
$ Rose a
a Rose a -> [Rose a] -> [Rose a]
forall a. a -> [a] -> [a]
: [Rose a]
as

instance (Eq a, Monoid a) => Monoid (Rose a) where
  mempty :: Rose a
mempty = Tree a -> Rose a
forall a. Tree a -> Rose a
Rose (Tree a -> Rose a) -> Tree a -> Rose a
forall a b. (a -> b) -> a -> b
$ a -> Forest a -> Tree a
forall a. a -> Forest a -> Tree a
Node a
forall a. Monoid a => a
mempty Forest a
forall a. Monoid a => a
mempty

rose :: (Eq a, Monoid a) => a -> [Rose a] -> Rose a
rose :: a -> [Rose a] -> Rose a
rose a
a [Rose (Node a
a' Forest a
rs)] | a
a' a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
forall a. Monoid a => a
mempty = Tree a -> Rose a
forall a. Tree a -> Rose a
Rose (Tree a -> Rose a) -> Tree a -> Rose a
forall a b. (a -> b) -> a -> b
$ a -> Forest a -> Tree a
forall a. a -> Forest a -> Tree a
Node a
a Forest a
rs
rose a
a [Rose a]
rs = Tree a -> Rose a
forall a. Tree a -> Rose a
Rose (Tree a -> Rose a) -> Tree a -> Rose a
forall a b. (a -> b) -> a -> b
$ a -> Forest a -> Tree a
forall a. a -> Forest a -> Tree a
Node a
a (Forest a -> Tree a) -> Forest a -> Tree a
forall a b. (a -> b) -> a -> b
$ [Rose a] -> Forest a
coerce [Rose a]
rs


------------------------------------------------------------------------------
-- | The results of 'Wingman.Machinery.runTactic'
data RunTacticResults = RunTacticResults
  { RunTacticResults -> Trace
rtr_trace       :: Trace
  , RunTacticResults -> LHsExpr GhcPs
rtr_extract     :: LHsExpr GhcPs
  , RunTacticResults -> [Judgement]
rtr_subgoals    :: [Judgement]
  , RunTacticResults -> [Synthesized (LHsExpr GhcPs)]
rtr_other_solns :: [Synthesized (LHsExpr GhcPs)]
  , RunTacticResults -> Judgement
rtr_jdg         :: Judgement
  , RunTacticResults -> Context
rtr_ctx         :: Context
  , RunTacticResults -> Bool
rtr_timed_out   :: Bool
  } deriving Int -> RunTacticResults -> ShowS
[RunTacticResults] -> ShowS
RunTacticResults -> String
(Int -> RunTacticResults -> ShowS)
-> (RunTacticResults -> String)
-> ([RunTacticResults] -> ShowS)
-> Show RunTacticResults
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [RunTacticResults] -> ShowS
$cshowList :: [RunTacticResults] -> ShowS
show :: RunTacticResults -> String
$cshow :: RunTacticResults -> String
showsPrec :: Int -> RunTacticResults -> ShowS
$cshowsPrec :: Int -> RunTacticResults -> ShowS
Show


data AgdaMatch = AgdaMatch
  { AgdaMatch -> [Pat GhcPs]
amPats :: [Pat GhcPs]
  , AgdaMatch -> HsExpr GhcPs
amBody :: HsExpr GhcPs
  }
  deriving (Int -> AgdaMatch -> ShowS
[AgdaMatch] -> ShowS
AgdaMatch -> String
(Int -> AgdaMatch -> ShowS)
-> (AgdaMatch -> String)
-> ([AgdaMatch] -> ShowS)
-> Show AgdaMatch
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [AgdaMatch] -> ShowS
$cshowList :: [AgdaMatch] -> ShowS
show :: AgdaMatch -> String
$cshow :: AgdaMatch -> String
showsPrec :: Int -> AgdaMatch -> ShowS
$cshowsPrec :: Int -> AgdaMatch -> ShowS
Show)


data UserFacingMessage
  = NotEnoughGas
  | TacticErrors
  | TimedOut
  | NothingToDo
  | InfrastructureError Text
  deriving UserFacingMessage -> UserFacingMessage -> Bool
(UserFacingMessage -> UserFacingMessage -> Bool)
-> (UserFacingMessage -> UserFacingMessage -> Bool)
-> Eq UserFacingMessage
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: UserFacingMessage -> UserFacingMessage -> Bool
$c/= :: UserFacingMessage -> UserFacingMessage -> Bool
== :: UserFacingMessage -> UserFacingMessage -> Bool
$c== :: UserFacingMessage -> UserFacingMessage -> Bool
Eq

instance Show UserFacingMessage where
  show :: UserFacingMessage -> String
show UserFacingMessage
NotEnoughGas = String
"Wingman ran out of gas when trying to find a solution.  \nTry increasing the `auto_gas` setting."
  show UserFacingMessage
TacticErrors = String
"Wingman couldn't find a solution"
  show UserFacingMessage
TimedOut     = String
"Wingman timed out while finding a solution.  \nYou might get a better result if you increase the timeout duration."
  show UserFacingMessage
NothingToDo  = String
"Nothing to do"
  show (InfrastructureError Text
t) = String
"Internal error: " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Text -> String
T.unpack Text
t


data HoleSort = Hole | Metaprogram T.Text
  deriving (HoleSort -> HoleSort -> Bool
(HoleSort -> HoleSort -> Bool)
-> (HoleSort -> HoleSort -> Bool) -> Eq HoleSort
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: HoleSort -> HoleSort -> Bool
$c/= :: HoleSort -> HoleSort -> Bool
== :: HoleSort -> HoleSort -> Bool
$c== :: HoleSort -> HoleSort -> Bool
Eq, Eq HoleSort
Eq HoleSort
-> (HoleSort -> HoleSort -> Ordering)
-> (HoleSort -> HoleSort -> Bool)
-> (HoleSort -> HoleSort -> Bool)
-> (HoleSort -> HoleSort -> Bool)
-> (HoleSort -> HoleSort -> Bool)
-> (HoleSort -> HoleSort -> HoleSort)
-> (HoleSort -> HoleSort -> HoleSort)
-> Ord HoleSort
HoleSort -> HoleSort -> Bool
HoleSort -> HoleSort -> Ordering
HoleSort -> HoleSort -> HoleSort
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 :: HoleSort -> HoleSort -> HoleSort
$cmin :: HoleSort -> HoleSort -> HoleSort
max :: HoleSort -> HoleSort -> HoleSort
$cmax :: HoleSort -> HoleSort -> HoleSort
>= :: HoleSort -> HoleSort -> Bool
$c>= :: HoleSort -> HoleSort -> Bool
> :: HoleSort -> HoleSort -> Bool
$c> :: HoleSort -> HoleSort -> Bool
<= :: HoleSort -> HoleSort -> Bool
$c<= :: HoleSort -> HoleSort -> Bool
< :: HoleSort -> HoleSort -> Bool
$c< :: HoleSort -> HoleSort -> Bool
compare :: HoleSort -> HoleSort -> Ordering
$ccompare :: HoleSort -> HoleSort -> Ordering
$cp1Ord :: Eq HoleSort
Ord, Int -> HoleSort -> ShowS
[HoleSort] -> ShowS
HoleSort -> String
(Int -> HoleSort -> ShowS)
-> (HoleSort -> String) -> ([HoleSort] -> ShowS) -> Show HoleSort
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [HoleSort] -> ShowS
$cshowList :: [HoleSort] -> ShowS
show :: HoleSort -> String
$cshow :: HoleSort -> String
showsPrec :: Int -> HoleSort -> ShowS
$cshowsPrec :: Int -> HoleSort -> ShowS
Show)

data HoleJudgment = HoleJudgment
  { HoleJudgment -> Tracked 'Current Range
hj_range     :: Tracked 'Current Range
  , HoleJudgment -> Judgement
hj_jdg       :: Judgement
  , HoleJudgment -> Context
hj_ctx       :: Context
  , HoleJudgment -> DynFlags
hj_dflags    :: DynFlags
  , HoleJudgment -> HoleSort
hj_hole_sort :: HoleSort
  }